From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- plugins/funind/merge.ml | 65 ++++++++++++++++++++++++++----------------------- 1 file changed, 34 insertions(+), 31 deletions(-) (limited to 'plugins/funind/merge.ml') 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 false in (* FIXME: *) - (Anonymous,Some mkProp,mkProp) + LocalDef (Anonymous,mkProp,mkProp) let relprinctype_to_funprinctype relprinctype nfuns = -- cgit v1.2.3