aboutsummaryrefslogtreecommitdiff
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.ml76
1 files changed, 39 insertions, 37 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index dd02dfe8d1..4544f736ca 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -333,8 +333,8 @@ let raw_push_named (na,raw_value,raw_typ) env =
match na with
| Anonymous -> env
| Name id ->
- let value = Option.map (Pretyping.understand Evd.empty env) raw_value in
- let typ = Pretyping.understand Evd.empty env ~expected_type:Pretyping.IsType raw_typ in
+ let value = Option.map (fun x-> fst (Pretyping.understand Evd.empty env x)) raw_value in
+ let typ,ctx = Pretyping.understand Evd.empty env ~expected_type:Pretyping.IsType raw_typ in
Environ.push_named (id,value,typ) env
@@ -350,7 +350,7 @@ let add_pat_variables pat typ env : Environ.env =
with Not_found -> assert false
in
let constructors = Inductiveops.get_constructors env indf in
- let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c cs.Inductiveops.cs_cstr) (Array.to_list constructors) in
+ let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
in
@@ -397,7 +397,7 @@ let rec pattern_to_term_and_type env typ = function
with Not_found -> assert false
in
let constructors = Inductiveops.get_constructors env indf in
- let constructor = List.find (fun cs -> eq_constructor cs.Inductiveops.cs_cstr constr) (Array.to_list constructors) in
+ let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in
let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
let _,cstl = Inductiveops.dest_ind_family indf in
let csta = Array.of_list cstl in
@@ -486,7 +486,7 @@ 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 = Pretyping.understand Evd.empty env rt in
+ let rt_as_constr,ctx = Pretyping.understand Evd.empty env rt in
let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in
let res = fresh_id args_res.to_avoid "_res" in
@@ -559,6 +559,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
*)
build_entry_lc env funnames avoid (mkGApp(b,args))
| GRec _ -> error "Not handled GRec"
+ | GProj _ -> error "Not handled GProj"
| GProd _ -> error "Cannot apply a type"
end (* end of the application treatement *)
@@ -594,7 +595,7 @@ 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 = Pretyping.understand Evd.empty env v in
+ let v_as_constr,ctx = Pretyping.understand Evd.empty env v in
let v_type = Typing.type_of env Evd.empty v_as_constr in
let new_env =
match n with
@@ -610,7 +611,7 @@ 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 = Pretyping.understand Evd.empty env b in
+ let b_as_constr,ctx = Pretyping.understand Evd.empty env b in
let b_typ = Typing.type_of env Evd.empty b_as_constr in
let (ind,_) =
try Inductiveops.find_inductive env Evd.empty b_typ
@@ -619,7 +620,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
Printer.pr_glob_constr b ++ str " in " ++
Printer.pr_glob_constr rt ++ str ". try again with a cast")
in
- let case_pats = build_constructors_of_type ind [] in
+ let case_pats = build_constructors_of_type (fst ind) [] in
assert (Int.equal (Array.length case_pats) 2);
let brl =
List.map_i
@@ -642,7 +643,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
)
nal
in
- let b_as_constr = Pretyping.understand Evd.empty env b in
+ let b_as_constr,ctx = Pretyping.understand Evd.empty env b in
let b_typ = Typing.type_of env Evd.empty b_as_constr in
let (ind,_) =
try Inductiveops.find_inductive env Evd.empty b_typ
@@ -651,7 +652,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
Printer.pr_glob_constr b ++ str " in " ++
Printer.pr_glob_constr rt ++ str ". try again with a cast")
in
- let case_pats = build_constructors_of_type ind nal_as_glob_constr in
+ let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
assert (Int.equal (Array.length case_pats) 1);
let br =
(Loc.ghost,[],[case_pats.(0)],e)
@@ -661,6 +662,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
end
| GRec _ -> error "Not handled GRec"
+ | GProj _ -> error "Not handled GProj"
| GCast(_,b,_) ->
build_entry_lc env funnames avoid b
and build_entry_lc_from_case env funname make_discr
@@ -689,7 +691,7 @@ and build_entry_lc_from_case env funname make_discr
in
let types =
List.map (fun (case_arg,_) ->
- let case_arg_as_constr = Pretyping.understand Evd.empty env case_arg in
+ let case_arg_as_constr,ctx = Pretyping.understand Evd.empty env case_arg in
Typing.type_of env Evd.empty case_arg_as_constr
) el
in
@@ -844,7 +846,7 @@ let is_res id =
let same_raw_term rt1 rt2 =
match rt1,rt2 with
- | GRef(_,r1), GRef (_,r2) -> Globnames.eq_gr r1 r2
+ | GRef(_,r1,_), GRef (_,r2,_) -> Globnames.eq_gr r1 r2
| GHole _, GHole _ -> true
| _ -> false
let decompose_raw_eq lhs rhs =
@@ -894,7 +896,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' = Pretyping.understand Evd.empty env new_t in
+ let t',ctx = Pretyping.understand Evd.empty 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
@@ -907,14 +909,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| _ -> (* the first args is the name of the function! *)
assert false
end
- | GApp(loc1,GRef(loc2,eq_as_ref),[ty;GVar(loc3,id);rt])
+ | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;GVar(loc3,id);rt])
when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
->
begin
try
observe (str "computing new type for eq : " ++ pr_glob_constr rt);
let t' =
- try Pretyping.understand Evd.empty env t
+ try fst (Pretyping.understand Evd.empty env t)(*FIXME*)
with e when Errors.noncritical e -> raise Continue
in
let is_in_b = is_free_in id b in
@@ -936,17 +938,17 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
in
mkGProd(n,t,new_b),id_to_exclude
with Continue ->
- let jmeq = Globnames.IndRef (destInd (jmeq ())) in
- let ty' = Pretyping.understand Evd.empty env ty in
+ let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in
+ let ty',ctx = Pretyping.understand Evd.empty env ty in
let ind,args' = Inductive.find_inductive env ty' in
- let mib,_ = Global.lookup_inductive ind in
+ let mib,_ = Global.lookup_inductive (fst ind) in
let nparam = mib.Declarations.mind_nparams in
let params,arg' =
((Util.List.chop nparam args'))
in
let rt_typ =
GApp(Loc.ghost,
- GRef (Loc.ghost,Globnames.IndRef ind),
+ GRef (Loc.ghost,Globnames.IndRef (fst ind),None),
(List.map
(fun p -> Detyping.detype false []
(Termops.names_of_rel_context env)
@@ -956,10 +958,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
(mkGHole ()))))
in
let eq' =
- GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;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 = Pretyping.understand Evd.empty env eq' in
+ let eq'_as_constr,ctx = Pretyping.understand Evd.empty env eq' in
observe (str " computing new type for jmeq : done") ;
let new_args =
match kind_of_term eq'_as_constr with
@@ -1007,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' = Pretyping.understand Evd.empty env eq' in
+ let t',ctx = Pretyping.understand Evd.empty env eq' in
Environ.push_rel (n,None,t') env
in
let new_b,id_to_exclude =
@@ -1024,7 +1026,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
mkGProd(n,t,new_b),id_to_exclude
else new_b, Id.Set.add id id_to_exclude
*)
- | GApp(loc1,GRef(loc2,eq_as_ref),[ty;rt1;rt2])
+ | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;rt1;rt2])
when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
->
begin
@@ -1045,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' = Pretyping.understand Evd.empty env t in
+ let t',ctx = Pretyping.understand Evd.empty env t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1061,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' = Pretyping.understand Evd.empty env t in
+ let t',ctx = Pretyping.understand Evd.empty env t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1080,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' = Pretyping.understand Evd.empty env t in
+ let t',ctx = Pretyping.understand Evd.empty env t in
match n with
| Name id ->
let new_env = Environ.push_rel (n,None,t') env in
@@ -1102,7 +1104,7 @@ 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' = Pretyping.understand Evd.empty env t in
+ let t',ctx = Pretyping.understand Evd.empty env t in
let type_t' = Typing.type_of env Evd.empty t' in
let new_env = Environ.push_rel (n,Some t',type_t') env in
let new_b,id_to_exclude =
@@ -1127,7 +1129,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
args (crossed_types)
depth t
in
- let t' = Pretyping.understand Evd.empty env new_t in
+ let t',ctx = Pretyping.understand Evd.empty 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
@@ -1179,7 +1181,7 @@ let rec compute_cst_params relnames params = function
discriminitation ones *)
| GSort _ -> params
| GHole _ -> params
- | GIf _ | GRec _ | GCast _ ->
+ | GIf _ | GRec _ | GCast _ | GProj _->
raise (UserError("compute_cst_params", str "Not handled case"))
and compute_cst_params_from_app acc (params,rtl) =
match params,rtl with
@@ -1267,12 +1269,12 @@ let do_build_inductive
(fun (n,t,is_defined) acc ->
if is_defined
then
- Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t,
+ Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
acc)
else
Constrexpr.CProdN
(Loc.ghost,
- [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t],
+ [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
acc
)
)
@@ -1285,7 +1287,8 @@ 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, Constrintern.interp_constr Evd.empty env rel_ar) env) env relnames rel_arities
+ Environ.push_named (rel_name,None,
+ fst (with_full_print (Constrintern.interp_constr Evd.empty env) rel_ar)) env) env relnames rel_arities
in
(* and of the real constructors*)
let constr i res =
@@ -1333,12 +1336,12 @@ let do_build_inductive
(fun (n,t,is_defined) acc ->
if is_defined
then
- Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t,
+ Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
acc)
else
Constrexpr.CProdN
(Loc.ghost,
- [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t],
+ [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
acc
)
)
@@ -1366,8 +1369,7 @@ let do_build_inductive
Array.map (List.map
(fun (id,t) ->
false,((Loc.ghost,id),
- Flags.with_option
- Flags.raw_print
+ with_full_print
(Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) t)
)
))
@@ -1403,7 +1405,7 @@ let do_build_inductive
(* in *)
let _time2 = System.get_time () in
try
- with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds)) true
+ with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false)) true
with
| UserError(s,msg) as e ->
let _time3 = System.get_time () in
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 17:02:16 +0000