summaryrefslogtreecommitdiff
path: root/plugins/funind/merge.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/merge.ml')
-rw-r--r--plugins/funind/merge.ml65
1 files changed, 34 insertions, 31 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 87d7ca76..de4210af 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -11,7 +11,7 @@
open Globnames
open Tactics
open Indfun_common
-open Errors
+open CErrors
open Util
open Constrexpr
open Vernacexpr
@@ -19,12 +19,12 @@ open Pp
open Names
open Term
open Vars
-open Context
open Termops
open Declarations
open Glob_term
open Glob_termops
open Decl_kinds
+open Context.Rel.Declaration
(** {1 Utilities} *)
@@ -73,7 +73,7 @@ let ident_global_exist id =
let ans = CRef (Libnames.Ident (Loc.ghost,id), None) in
let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
true
- with e when Errors.noncritical e -> false
+ with e when CErrors.noncritical e -> false
(** [next_ident_fresh id] returns a fresh identifier (ie not linked in
global env) with base [id]. *)
@@ -135,9 +135,9 @@ let showind (id:Id.t) =
let cstrid = Constrintern.global_reference id in
let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in
- List.iter (fun (nm, optcstr, tp) ->
- print_string (string_of_name nm^":");
- prconstr tp; print_string "\n")
+ List.iter (fun decl ->
+ print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");
+ prconstr (get_type decl); print_string "\n")
ib1.mind_arity_ctxt;
Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1);
Array.iteri
@@ -258,27 +258,27 @@ type merge_infos =
lnk2: int merged_arg array;
(** rec params which remain rec param (ie not linked) *)
- recprms1: rel_declaration list;
- recprms2: rel_declaration list;
+ recprms1: Context.Rel.Declaration.t list;
+ recprms2: Context.Rel.Declaration.t list;
nrecprms1: int;
nrecprms2: int;
(** rec parms which became non parm (either linked to something
or because after a rec parm that became non parm) *)
- otherprms1: rel_declaration list;
- otherprms2: rel_declaration list;
+ otherprms1: Context.Rel.Declaration.t list;
+ otherprms2: Context.Rel.Declaration.t list;
notherprms1:int;
notherprms2:int;
(** args which remain args in merge *)
- args1:rel_declaration list;
- args2:rel_declaration list;
+ args1:Context.Rel.Declaration.t list;
+ args2:Context.Rel.Declaration.t list;
nargs1:int;
nargs2:int;
(** functional result args *)
- funresprms1: rel_declaration list;
- funresprms2: rel_declaration list;
+ funresprms1: Context.Rel.Declaration.t list;
+ funresprms2: Context.Rel.Declaration.t list;
nfunresprms1:int;
nfunresprms2:int;
}
@@ -460,11 +460,12 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
let _ = prstr "\notherprms1:\n" in
let _ =
- List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n")
+ List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : ");
+ prconstr (get_type decl); prstr "\n")
otherprms1 in
let _ = prstr "\notherprms2:\n" in
let _ =
- List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n")
+ List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : "); prconstr (get_type decl); prstr "\n")
otherprms2 in
{
ident=id;
@@ -503,19 +504,19 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
let lnk = Array.append shift.lnk1 shift.lnk2 in
match c1 , c2 with
| GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
- let _ = prstr "\nICI1!\n";Pp.flush_all() in
+ let _ = prstr "\nICI1!\n" in
let args = filter_shift_stable lnk (arr1 @ arr2) in
GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args)
| GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge
| GLetIn(_,nme,bdy,trm) , _ ->
- let _ = prstr "\nICI2!\n";Pp.flush_all() in
+ let _ = prstr "\nICI2!\n" in
let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
GLetIn(Loc.ghost,nme,bdy,newtrm)
| _, GLetIn(_,nme,bdy,trm) ->
- let _ = prstr "\nICI3!\n";Pp.flush_all() in
+ let _ = prstr "\nICI3!\n" in
let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
GLetIn(Loc.ghost,nme,bdy,newtrm)
- | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in
+ | _ -> let _ = prstr "\nICI4!\n" in
raise NoMerge
let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
@@ -526,14 +527,14 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args)
(* FIXME: what if the function appears in the body of the let? *)
| GLetIn(_,nme,bdy,trm) , _ ->
- let _ = prstr "\nICI2 '!\n";Pp.flush_all() in
+ let _ = prstr "\nICI2 '!\n" in
let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
GLetIn(Loc.ghost,nme,bdy,newtrm)
| _, GLetIn(_,nme,bdy,trm) ->
- let _ = prstr "\nICI3 '!\n";Pp.flush_all() in
+ let _ = prstr "\nICI3 '!\n" in
let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
GLetIn(Loc.ghost,nme,bdy,newtrm)
- | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge
+ | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge
@@ -784,10 +785,10 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
let params1 =
try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
- with e when Errors.noncritical e -> [] in
+ with e when CErrors.noncritical e -> [] in
let params2 =
try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
- with e when Errors.noncritical e -> [] in
+ with e when CErrors.noncritical e -> [] in
let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in
let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in
@@ -824,9 +825,11 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in
let arity,_ =
List.fold_left
- (fun (acc,env) (nm,_,c) ->
+ (fun (acc,env) decl ->
+ let nm = Context.Rel.Declaration.get_name decl in
+ let c = get_type decl in
let typ = Constrextern.extern_constr false env Evd.empty c in
- let newenv = Environ.push_rel (nm,None,c) env in
+ let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
(concl,Global.env())
(shift.funresprms2 @ shift.funresprms1
@@ -851,12 +854,12 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
lident , bindlist , Some cstr_expr , lcstor_expr
-let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
+let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
match rdecl with
- | (nme,None,t) ->
+ | LocalAssum (nme,t) ->
let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
GProd (Loc.ghost,nme,Explicit,traw,t2)
- | (_,Some _,_) -> assert false
+ | LocalDef _ -> assert false
(** [merge_inductive ind1 ind2 lnk] merges two graphs, linking
@@ -970,7 +973,7 @@ let funify_branches relinfo nfuns branch =
| Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches)
| _ -> false in
(* FIXME: *)
- (Anonymous,Some mkProp,mkProp)
+ LocalDef (Anonymous,mkProp,mkProp)
let relprinctype_to_funprinctype relprinctype nfuns =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 09:07:00 +0000