diff options
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 99 |
1 files changed, 55 insertions, 44 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 9e3f3986..1b12cd42 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -333,20 +333,20 @@ let raw_push_named (na,raw_value,raw_typ) env = match na with | Anonymous -> env | Name id -> - let value = Option.map (fun x-> fst (Pretyping.understand env Evd.empty x)) raw_value in - let typ,ctx = Pretyping.understand env Evd.empty ~expected_type:Pretyping.IsType raw_typ in + let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in + let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in Environ.push_named (id,value,typ) env let add_pat_variables pat typ env : Environ.env = let rec add_pat_variables env pat typ : Environ.env = - observe (str "new rel env := " ++ Printer.pr_rel_context_of env Evd.empty); + observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); match pat with | PatVar(_,na) -> Environ.push_rel (na,None,typ) env | PatCstr(_,c,patl,na) -> let Inductiveops.IndType(indf,indargs) = - try Inductiveops.find_rectype env Evd.empty typ + try Inductiveops.find_rectype env (Evd.from_env env) typ with Not_found -> assert false in let constructors = Inductiveops.get_constructors env indf in @@ -376,7 +376,7 @@ let add_pat_variables pat typ env : Environ.env = ~init:(env,[]) ) in - observe (str "new var env := " ++ Printer.pr_named_context_of res Evd.empty); + observe (str "new var env := " ++ Printer.pr_named_context_of res (Evd.from_env env)); res @@ -393,7 +393,7 @@ let rec pattern_to_term_and_type env typ = function constr in let Inductiveops.IndType(indf,indargs) = - try Inductiveops.find_rectype env Evd.empty typ + try Inductiveops.find_rectype env (Evd.from_env env) typ with Not_found -> assert false in let constructors = Inductiveops.get_constructors env indf in @@ -405,7 +405,7 @@ let rec pattern_to_term_and_type env typ = function Array.to_list (Array.init (cst_narg - List.length patternl) - (fun i -> Detyping.detype false [] env Evd.empty csta.(i)) + (fun i -> Detyping.detype false [] env (Evd.from_env env) csta.(i)) ) in let patl_as_term = @@ -486,9 +486,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = a pseudo value "v1 ... vn". The "value" of this branch is then simply [res] *) - let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in - let rt_typ = Typing.type_of env Evd.empty rt_as_constr in - let res_raw_type = Detyping.detype false [] env Evd.empty rt_typ in + let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in + let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in + let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in let res_rt = mkGVar res in @@ -594,8 +594,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = and combine the two result *) let v_res = build_entry_lc env funnames avoid v in - let v_as_constr,ctx = Pretyping.understand env Evd.empty v in - let v_type = Typing.type_of env Evd.empty v_as_constr in + let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in + let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in let new_env = match n with Anonymous -> env @@ -610,10 +610,10 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let make_discr = make_discr_match brl in build_entry_lc_from_case env funnames make_discr el brl avoid | GIf(_,b,(na,e_option),lhs,rhs) -> - let b_as_constr,ctx = Pretyping.understand env Evd.empty b in - let b_typ = Typing.type_of env Evd.empty b_as_constr in + let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in + let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in let (ind,_) = - try Inductiveops.find_inductive env Evd.empty b_typ + try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> errorlabstrm "" (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ @@ -642,10 +642,10 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = ) nal in - let b_as_constr,ctx = Pretyping.understand env Evd.empty b in - let b_typ = Typing.type_of env Evd.empty b_as_constr in + let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in + let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in let (ind,_) = - try Inductiveops.find_inductive env Evd.empty b_typ + try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> errorlabstrm "" (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ @@ -689,8 +689,8 @@ and build_entry_lc_from_case env funname make_discr in let types = List.map (fun (case_arg,_) -> - let case_arg_as_constr,ctx = Pretyping.understand env Evd.empty case_arg in - Typing.type_of env Evd.empty case_arg_as_constr + let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in + Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr ) el in (****** The next works only if the match is not dependent ****) @@ -737,11 +737,11 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve List.fold_right (fun id acc -> let typ_of_id = - Typing.type_of env_with_pat_ids Evd.empty (mkVar id) + Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (mkVar id) in let raw_typ_of_id = Detyping.detype false [] - env_with_pat_ids Evd.empty typ_of_id + env_with_pat_ids (Evd.from_env env) typ_of_id in mkGProd (Name id,raw_typ_of_id,acc)) pat_ids @@ -785,15 +785,15 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve List.map3 (fun pat e typ_as_constr -> let this_pat_ids = ids_of_pat pat in - let typ = Detyping.detype false [] new_env Evd.empty typ_as_constr in + let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in let pat_as_term = pattern_to_term pat in List.fold_right (fun id acc -> if Id.Set.mem id this_pat_ids then (Prod (Name id), - let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in + let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (mkVar id) in let raw_typ_of_id = - Detyping.detype false [] new_env Evd.empty typ_of_id + Detyping.detype false [] new_env (Evd.from_env env) typ_of_id in raw_typ_of_id )::acc @@ -894,7 +894,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let new_t = mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt]) in - let t',ctx = Pretyping.understand env Evd.empty new_t in + let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -914,7 +914,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = try observe (str "computing new type for eq : " ++ pr_glob_constr rt); let t' = - try fst (Pretyping.understand env Evd.empty t)(*FIXME*) + try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*) with e when Errors.noncritical e -> raise Continue in let is_in_b = is_free_in id b in @@ -937,7 +937,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGProd(n,t,new_b),id_to_exclude with Continue -> let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in - let ty',ctx = Pretyping.understand env Evd.empty ty in + let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in let ind,args' = Inductive.find_inductive env ty' in let mib,_ = Global.lookup_inductive (fst ind) in let nparam = mib.Declarations.mind_nparams in @@ -949,7 +949,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = GRef (Loc.ghost,Globnames.IndRef (fst ind),None), (List.map (fun p -> Detyping.detype false [] - env Evd.empty + env (Evd.from_env env) p) params)@(Array.to_list (Array.make (List.length args' - nparam) @@ -959,7 +959,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt]) in observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); - let eq'_as_constr,ctx = Pretyping.understand env Evd.empty eq' in + let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in observe (str " computing new type for jmeq : done") ; let new_args = match kind_of_term eq'_as_constr with @@ -978,12 +978,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | Name id' -> (id',Detyping.detype false [] env - Evd.empty + (Evd.from_env env) arg)::acc else if isVar var_as_constr then (destVar var_as_constr,Detyping.detype false [] env - Evd.empty + (Evd.from_env env) arg)::acc else acc ) @@ -1009,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = if is_in_b then b else replace_var_by_term id rt b in let new_env = - let t',ctx = Pretyping.understand env Evd.empty eq' in + let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = @@ -1047,7 +1047,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = else raise Continue with Continue -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); - let t',ctx = Pretyping.understand env Evd.empty t in + let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1063,7 +1063,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = end | _ -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); - let t',ctx = Pretyping.understand env Evd.empty t in + let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1082,7 +1082,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in observe (str "computing new type for lambda : " ++ pr_glob_constr rt); - let t',ctx = Pretyping.understand env Evd.empty t in + let t',ctx = Pretyping.understand env (Evd.from_env env) t in match n with | Name id -> let new_env = Environ.push_rel (n,None,t') env in @@ -1104,8 +1104,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | GLetIn(_,n,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in - let t',ctx = Pretyping.understand env Evd.empty t in - let type_t' = Typing.type_of env Evd.empty t' in + let evd = (Evd.from_env env) in + let t',ctx = Pretyping.understand env evd t in + let evd = Evd.from_ctx ctx in + let type_t' = Typing.unsafe_type_of env evd t' in let new_env = Environ.push_rel (n,Some t',type_t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1129,7 +1131,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = args (crossed_types) depth t in - let t',ctx = Pretyping.understand env Evd.empty new_t in + let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in let new_env = Environ.push_rel (na,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1255,7 +1257,7 @@ let do_build_inductive let evd,env = Array.fold_right2 (fun id c (evd,env) -> - let evd,t = Typing.e_type_of env evd (mkConstU c) in + let evd,t = Typing.type_of env evd (mkConstU c) in evd, Environ.push_named (id,None,t) (* try *) @@ -1297,7 +1299,7 @@ let do_build_inductive let rel_arities = Array.mapi rel_arity funsargs in Util.Array.fold_left2 (fun env rel_name rel_ar -> Environ.push_named (rel_name,None, - fst (with_full_print (Constrintern.interp_constr env Evd.empty) rel_ar)) env) env relnames rel_arities + fst (with_full_print (Constrintern.interp_constr env evd) rel_ar)) env) env relnames rel_arities in (* and of the real constructors*) let constr i res = @@ -1395,7 +1397,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - ((Loc.ghost,relnames.(i)), + (((Loc.ghost,relnames.(i)), None), rel_params, Some rel_arities.(i), ext_rel_constructors),[] @@ -1460,8 +1462,17 @@ let do_build_inductive let build_inductive evd funconstants funsargs returned_types rtl = + let pu = !Detyping.print_universes in + let cu = !Constrextern.print_universes in try - do_build_inductive evd funconstants funsargs returned_types rtl - with e when Errors.noncritical e -> raise (Building_graph e) + Detyping.print_universes := true; + Constrextern.print_universes := true; + do_build_inductive evd funconstants funsargs returned_types rtl; + Detyping.print_universes := pu; + Constrextern.print_universes := cu + with e when Errors.noncritical e -> + Detyping.print_universes := pu; + Constrextern.print_universes := cu; + raise (Building_graph e) |