summaryrefslogtreecommitdiff
path: root/plugins/funind/glob_term_to_relation.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
-rw-r--r--plugins/funind/glob_term_to_relation.ml99
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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 23:27:41 +0000