diff options
Diffstat (limited to 'plugins/funind/merge.ml')
| -rw-r--r-- | plugins/funind/merge.ml | 330 |
1 files changed, 165 insertions, 165 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 092830025..3538f6342 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -18,7 +18,7 @@ open Vernacexpr open Pp open Names open Term -open Termops +open Termops open Declarations open Environ open Rawterm @@ -32,19 +32,19 @@ let rec popn i c = if i<=0 then c else pop (popn (i-1) c) (** Substitutions in constr *) let compare_constr_nosub t1 t2 = - if compare_constr (fun _ _ -> false) t1 t2 + if compare_constr (fun _ _ -> false) t1 t2 then true else false let rec compare_constr' t1 t2 = - if compare_constr_nosub t1 t2 + if compare_constr_nosub t1 t2 then true else (compare_constr (compare_constr') t1 t2) let rec substitterm prof t by_t in_u = if (compare_constr' (lift prof t) in_u) then (lift prof by_t) - else map_constr_with_binders succ + else map_constr_with_binders succ (fun i -> substitterm i t by_t) prof in_u let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl @@ -59,23 +59,23 @@ let name_of_string str = Name (id_of_string str) let string_of_name nme = string_of_id (id_of_name nme) (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) -let isVarf f x = +let isVarf f x = match x with - | RVar (_,x) -> Pervasives.compare x f = 0 + | RVar (_,x) -> Pervasives.compare x f = 0 | _ -> false (** [ident_global_exist id] returns true if identifier [id] is linked in global environment. *) -let ident_global_exist id = - try +let ident_global_exist id = + try let ans = CRef (Libnames.Ident (dummy_loc,id)) in let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in true - with _ -> false + with _ -> false (** [next_ident_fresh id] returns a fresh identifier (ie not linked in global env) with base [id]. *) -let next_ident_fresh (id:identifier) = +let next_ident_fresh (id:identifier) = let res = ref id in while ident_global_exist !res do res := Nameops.lift_ident !res done; !res @@ -89,37 +89,37 @@ let prconstr c = msg (str" " ++ Printer.pr_lconstr c) let prconstrnl c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n") let prlistconstr lc = List.iter prconstr lc let prstr s = msg(str s) -let prNamedConstr s c = +let prNamedConstr s c = begin msg(str ""); msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} "); msg(str ""); end -let prNamedRConstr s c = +let prNamedRConstr s c = begin msg(str ""); msg(str(s^" {§ ") ++ Printer.pr_rawconstr c ++ str " §} "); msg(str ""); end let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc -let prNamedLConstr s lc = +let prNamedLConstr s lc = begin prstr "[§§§ "; prstr s; prNamedLConstr_aux lc; prstr " §§§]\n"; end -let prNamedLDecl s lc = +let prNamedLDecl s lc = begin prstr s; prstr "\n"; List.iter (fun (nm,_,tp) -> prNamedConstr (string_of_name nm) tp) lc; prstr "\n"; end -let prNamedRLDecl s lc = +let prNamedRLDecl s lc = begin prstr s; prstr "\n"; prstr "{§§ "; - List.iter - (fun x -> + List.iter + (fun x -> match x with | (nm,None,Some tp) -> prNamedRConstr (string_of_name nm) tp | (nm,Some bdy,None) -> prNamedRConstr ("(letin) "^string_of_name nm) bdy @@ -133,16 +133,16 @@ let showind (id:identifier) = let cstrid = Tacinterp.constr_of_id (Global.env()) id in let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in - List.iter (fun (nm, optcstr, tp) -> + List.iter (fun (nm, optcstr, tp) -> print_string (string_of_name nm^":"); - prconstr tp; print_string "\n") + prconstr tp; print_string "\n") ib1.mind_arity_ctxt; (match ib1.mind_arity with | Monomorphic x -> Printf.printf "arity :"; prconstr x.mind_user_arity - | Polymorphic x -> + | Polymorphic x -> Printf.printf "arity : universe?"); - Array.iteri + Array.iteri (fun i x -> Printf.printf"type constr %d :" i ; prconstr x) ib1.mind_user_lc @@ -151,7 +151,7 @@ let showind (id:identifier) = exception Found of int (* Array scanning *) -let array_find (arr: 'a array) (pred: int -> 'a -> bool): int option = +let array_find (arr: 'a array) (pred: int -> 'a -> bool): int option = try for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done; None @@ -163,10 +163,10 @@ let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int = Array.length arr (* all elt are positive *) with Found i -> i -let array_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b array): 'a = - let i = ref 0 in - Array.fold_left - (fun acc x -> +let array_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b array): 'a = + let i = ref 0 in + Array.fold_left + (fun acc x -> let res = f !i acc x in i := !i + 1; res) acc arr @@ -176,25 +176,25 @@ let list_chop_end i l = if size_prefix < 0 then failwith "list_chop_end" else list_chop size_prefix l -let list_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b list): 'a = - let i = ref 0 in - List.fold_left - (fun acc x -> +let list_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b list): 'a = + let i = ref 0 in + List.fold_left + (fun acc x -> let res = f !i acc x in i := !i + 1; res) acc arr -let list_filteri (f: int -> 'a -> bool) (l:'a list):'a list = - let i = ref 0 in +let list_filteri (f: int -> 'a -> bool) (l:'a list):'a list = + let i = ref 0 in List.filter (fun x -> let res = f !i x in i := !i + 1; res) l (** Iteration module *) -module For = +module For = struct let rec map i j (f: int -> 'a) = if i>j then [] else f i :: (map (i+1) j f) - let rec foldup i j (f: 'a -> int -> 'a) acc = + let rec foldup i j (f: 'a -> int -> 'a) acc = if i>j then acc else let newacc = f acc i in foldup (i+1) j f newacc - let rec folddown i j (f: 'a -> int -> 'a) acc = + let rec folddown i j (f: 'a -> int -> 'a) acc = if i>j then acc else let newacc = f acc j in folddown i (j-1) f newacc let fold i j = if i<j then foldup i j else folddown i j end @@ -231,7 +231,7 @@ let prlinked x = | Unlinked -> Printf.sprintf "Unlinked" | Funres -> Printf.sprintf "Funres" -let linkmonad f lnkvar = +let linkmonad f lnkvar = match lnkvar with | Linked i -> Linked (f i) | Unlinked -> Unlinked @@ -242,7 +242,7 @@ let linklift lnkvar i = linkmonad (fun x -> x+i) lnkvar (* This map is used to deal with debruijn linked indices. *) module Link = Map.Make (struct type t = int let compare = Pervasives.compare end) -let pr_links l = +let pr_links l = Printf.printf "links:\n"; Link.iter (fun k e -> Printf.printf "%d : %s\n" k (prlinked e)) l; Printf.printf "_____________\n" @@ -255,16 +255,16 @@ type 'a merged_arg = | Arg_linked of 'a | Arg_funres -(** Information about graph merging of two inductives. +(** Information about graph merging of two inductives. All rel_decl list are IN REVERSE ORDER (ie well suited for compose) *) type merge_infos = { ident:identifier; (** new inductive name *) mib1: mutual_inductive_body; - oib1: one_inductive_body; + oib1: one_inductive_body; mib2: mutual_inductive_body; - oib2: one_inductive_body; + oib2: one_inductive_body; (** Array of links of the first inductive (should be all stable) *) lnk1: int merged_arg array; @@ -275,24 +275,24 @@ type merge_infos = (** rec params which remain rec param (ie not linked) *) recprms1: rel_declaration list; recprms2: rel_declaration list; - nrecprms1: int; + 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; - notherprms1:int; + otherprms1: rel_declaration list; + otherprms2: rel_declaration list; + notherprms1:int; notherprms2:int; (** args which remain args in merge *) - args1:rel_declaration list; + args1:rel_declaration list; args2:rel_declaration list; nargs1:int; nargs2:int; (** functional result args *) - funresprms1: rel_declaration list; + funresprms1: rel_declaration list; funresprms2: rel_declaration list; nfunresprms1:int; nfunresprms2:int; @@ -301,7 +301,7 @@ type merge_infos = let pr_merginfo x = let i,s= - match x with + match x with | Prm_linked i -> Some i,"Prm_linked" | Arg_linked i -> Some i,"Arg_linked" | Prm_stable i -> Some i,"Prm_stable" @@ -317,7 +317,7 @@ let isPrm_stable x = match x with Prm_stable _ -> true | _ -> false (* ?? prm_linked?? *) let isArg_stable x = match x with Arg_stable _ | Prm_arg _ -> true | _ -> false -let is_stable x = +let is_stable x = match x with Arg_stable _ | Prm_stable _ | Prm_arg _ -> true | _ -> false let isArg_funres x = match x with Arg_funres -> true | _ -> false @@ -332,22 +332,22 @@ let filter_shift_stable (lnk:int merged_arg array) (l:'a list): 'a list = of int as several vars may be linked to the same var. *) let revlinked lnk = For.fold 0 (Array.length lnk - 1) - (fun acc k -> - match lnk.(k) with - | Unlinked | Funres -> acc - | Linked i -> + (fun acc k -> + match lnk.(k) with + | Unlinked | Funres -> acc + | Linked i -> let old = try Link.find i acc with Not_found -> [] in Link.add i (k::old) acc) Link.empty -let array_switch arr i j = +let array_switch arr i j = let aux = arr.(j) in arr.(j) <- arr.(i); arr.(i) <- aux let filter_shift_stable_right (lnk:int merged_arg array) (l:'a list): 'a list = let larr = Array.of_list l in let _ = Array.iteri - (fun j x -> + (fun j x -> match x with | Prm_linked i -> array_switch larr i j | Arg_linked i -> array_switch larr i j @@ -392,7 +392,7 @@ let build_raw_params prms_decl avoid = let ids_of_rawlist avoid rawl = List.fold_left Idset.union avoid (List.map ids_of_rawterm rawl) - + (** {1 Merging function graphs} *) @@ -402,7 +402,7 @@ let ids_of_rawlist avoid rawl = remain uniform when linked by [lnk]. All parameters are considered, ie we take parameters of the first inductive body of [mib1] and [mib2]. - + Explanation: The two inductives have parameters, some of the first are recursively uniform, some of the last are functional result of the functional graph. @@ -418,14 +418,14 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array let linked_targets = revlinked lnk2 in let is_param_of_mib1 x = x < mib1.mind_nparams_rec in let is_param_of_mib2 x = x < mib2.mind_nparams_rec in - let is_targetted_by_non_recparam_lnk1 i = - try - let targets = Link.find i linked_targets in + let is_targetted_by_non_recparam_lnk1 i = + try + let targets = Link.find i linked_targets in List.exists (fun x -> not (is_param_of_mib2 x)) targets with Not_found -> false in - let mlnk1 = + let mlnk1 = Array.mapi - (fun i lkv -> + (fun i lkv -> let isprm = is_param_of_mib1 i in let prmlost = is_targetted_by_non_recparam_lnk1 i in match isprm , prmlost, lnk1.(i) with @@ -435,13 +435,13 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array | _ , _ , Funres -> assert false (* fun res cannot be a rec param or lost *) | false , _ , _ -> Arg_stable i) (* Args of lnk1 are not linked *) lnk1 in - let mlnk2 = + let mlnk2 = Array.mapi - (fun i lkv -> + (fun i lkv -> (* Is this correct if some param of ind2 is lost? *) let isprm = is_param_of_mib2 i in match isprm , lnk2.(i) with - | true , Linked j when not (is_param_of_mib1 j) -> + | true , Linked j when not (is_param_of_mib1 j) -> Prm_arg j (* recparam becoming ordinary *) | true , Linked j -> Prm_linked j (*recparam linked to recparam*) | true , Unlinked -> Prm_stable i (* recparam remains recparam*) @@ -456,9 +456,9 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array (* count params remaining params *) let n_params1 = array_prfx mlnk1 (fun i x -> not (isPrm_stable x)) in let n_params2 = array_prfx mlnk2 (fun i x -> not (isPrm_stable x)) in - let bldprms arity_ctxt mlnk = + let bldprms arity_ctxt mlnk = list_fold_lefti - (fun i (acc1,acc2,acc3,acc4) x -> + (fun i (acc1,acc2,acc3,acc4) x -> prstr (pr_merginfo mlnk.(i));prstr "\n"; match mlnk.(i) with | Prm_stable _ -> x::acc1 , acc2 , acc3, acc4 @@ -467,19 +467,19 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array | Arg_funres -> acc1 , acc2 , acc3, x::acc4 | _ -> acc1 , acc2 , acc3, acc4) ([],[],[],[]) arity_ctxt in -(* let arity_ctxt2 = - build_raw_params oib2.mind_arity_ctxt +(* let arity_ctxt2 = + build_raw_params oib2.mind_arity_ctxt (Idset.elements (ids_of_rawterm oib1.mind_arity_ctxt)) in*) let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in let _ = prstr "\n\n\n" in 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") + let _ = + List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n") otherprms1 in let _ = prstr "\notherprms2:\n" in - let _ = - List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n") + let _ = + List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n") otherprms2 in { ident=id; @@ -514,38 +514,38 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array exception NoMerge -let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = +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 - | RApp(_,f1, arr1), RApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> + | RApp(_,f1, arr1), RApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> let _ = prstr "\nICI1!\n";Pp.flush_all() in let args = filter_shift_stable lnk (arr1 @ arr2) in RApp (dummy_loc,RVar (dummy_loc,shift.ident) , args) | RApp(_,f1, arr1), RApp(_,f2,arr2) -> raise NoMerge - | RLetIn(_,nme,bdy,trm) , _ -> - let _ = prstr "\nICI2!\n";Pp.flush_all() in + | RLetIn(_,nme,bdy,trm) , _ -> + let _ = prstr "\nICI2!\n";Pp.flush_all() in let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in RLetIn(dummy_loc,nme,bdy,newtrm) - | _, RLetIn(_,nme,bdy,trm) -> - let _ = prstr "\nICI3!\n";Pp.flush_all() in + | _, RLetIn(_,nme,bdy,trm) -> + let _ = prstr "\nICI3!\n";Pp.flush_all() in let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in RLetIn(dummy_loc,nme,bdy,newtrm) | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in raise NoMerge -let rec merge_app_unsafe c1 c2 shift filter_shift_stable = +let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in match c1 , c2 with - | RApp(_,f1, arr1), RApp(_,f2,arr2) -> + | RApp(_,f1, arr1), RApp(_,f2,arr2) -> let args = filter_shift_stable lnk (arr1 @ arr2) in RApp (dummy_loc,RVar(dummy_loc,shift.ident) , args) (* FIXME: what if the function appears in the body of the let? *) - | RLetIn(_,nme,bdy,trm) , _ -> - let _ = prstr "\nICI2 '!\n";Pp.flush_all() in + | RLetIn(_,nme,bdy,trm) , _ -> + let _ = prstr "\nICI2 '!\n";Pp.flush_all() in let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in RLetIn(dummy_loc,nme,bdy,newtrm) - | _, RLetIn(_,nme,bdy,trm) -> - let _ = prstr "\nICI3 '!\n";Pp.flush_all() in + | _, RLetIn(_,nme,bdy,trm) -> + let _ = prstr "\nICI3 '!\n";Pp.flush_all() in let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in RLetIn(dummy_loc,nme,bdy,newtrm) | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge @@ -555,33 +555,33 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = (* Heuristic when merging two lists of hypothesis: merge every rec calls of branch 1 with all rec calls of branch 2. *) (* TODO: reecrire cette heuristique (jusqu'a merge_types) *) -let rec merge_rec_hyps shift accrec - (ltyp:(Names.name * rawconstr option * rawconstr option) list) +let rec merge_rec_hyps shift accrec + (ltyp:(Names.name * rawconstr option * rawconstr option) list) filter_shift_stable : (Names.name * rawconstr option * rawconstr option) list = - let mergeonehyp t reldecl = + let mergeonehyp t reldecl = match reldecl with - | (nme,x,Some (RApp(_,i,args) as ind)) + | (nme,x,Some (RApp(_,i,args) as ind)) -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable) | (nme,Some _,None) -> error "letins with recursive calls not treated yet" - | (nme,None,Some _) -> assert false + | (nme,None,Some _) -> assert false | (nme,None,None) | (nme,Some _,Some _) -> assert false in match ltyp with | [] -> [] - | (nme,None,Some (RApp(_,f, largs) as t)) :: lt when isVarf ind2name f -> + | (nme,None,Some (RApp(_,f, largs) as t)) :: lt when isVarf ind2name f -> let rechyps = List.map (mergeonehyp t) accrec in rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable -let rec build_suppl_reccall (accrec:(name * rawconstr) list) concl2 shift = +let rec build_suppl_reccall (accrec:(name * rawconstr) list) concl2 shift = List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec -let find_app (nme:identifier) ltyp = +let find_app (nme:identifier) ltyp = try ignore (List.map - (fun x -> + (fun x -> match x with | _,None,Some (RApp(_,f,_)) when isVarf nme f -> raise (Found 0) | _ -> ()) @@ -589,17 +589,17 @@ let find_app (nme:identifier) ltyp = false with Found _ -> true -let prnt_prod_or_letin nm letbdy typ = +let prnt_prod_or_letin nm letbdy typ = match letbdy , typ with | Some lbdy , None -> prNamedRConstr ("(letin) " ^ string_of_name nm) lbdy | None , Some tp -> prNamedRConstr (string_of_name nm) tp | _ , _ -> assert false - -let rec merge_types shift accrec1 + +let rec merge_types shift accrec1 (ltyp1:(name * rawconstr option * rawconstr option) list) (concl1:rawconstr) (ltyp2:(name * rawconstr option * rawconstr option) list) concl2 - : (name * rawconstr option * rawconstr option) list * rawconstr = + : (name * rawconstr option * rawconstr option) list * rawconstr = let _ = prstr "MERGE_TYPES\n" in let _ = prstr "ltyp 1 : " in let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in @@ -608,20 +608,20 @@ let rec merge_types shift accrec1 let _ = prstr "\n" in let res = match ltyp1 with - | [] -> + | [] -> let isrec1 = (accrec1<>[]) in let isrec2 = find_app ind2name ltyp2 in let rechyps = - if isrec1 && isrec2 + if isrec1 && isrec2 then (* merge_rec_hyps shift accrec1 ltyp2 filter_shift_stable *) - merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2 + merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2 filter_shift_stable_right @ merge_rec_hyps shift accrec1 [name_of_string "concl2",None, Some concl2] filter_shift_stable - else if isrec1 + else if isrec1 (* if rec calls in accrec1 and not in ltyp2, add one to ltyp2 *) - then - merge_rec_hyps shift accrec1 + then + merge_rec_hyps shift accrec1 (ltyp2@[name_of_string "concl2",None,Some concl2]) filter_shift_stable else if isrec2 then merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2 @@ -634,22 +634,22 @@ let rec merge_types shift accrec1 let _ = prstr " with " in let _ = prNamedRConstr "concl2" concl2 in let _ = prstr "\n" in - let concl = + let concl = merge_app concl1 concl2 ind1name ind2name shift filter_shift_stable in let _ = prstr "FIN " in let _ = prNamedRConstr "concl" concl in let _ = prstr "\n" in rechyps , concl - | (nme,None, Some t1)as e ::lt1 -> + | (nme,None, Some t1)as e ::lt1 -> (match t1 with - | RApp(_,f,carr) when isVarf ind1name f -> - merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 - | _ -> + | RApp(_,f,carr) when isVarf ind1name f -> + merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 + | _ -> let recres, recconcl2 = merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in - ((nme,None,Some t1) :: recres) , recconcl2) - | (nme,Some bd, None) ::lt1 -> + ((nme,None,Some t1) :: recres) , recconcl2) + | (nme,Some bd, None) ::lt1 -> (* FIXME: what if ind1name appears in bd? *) let recres, recconcl2 = merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in @@ -666,10 +666,10 @@ let rec merge_types shift accrec1 let build_link_map_aux (allargs1:identifier array) (allargs2:identifier array) (lnk:int merged_arg array) = array_fold_lefti - (fun i acc e -> + (fun i acc e -> if i = Array.length lnk - 1 then acc (* functional arg, not in allargs *) - else - match e with + else + match e with | Prm_linked j | Arg_linked j -> Idmap.add allargs2.(i) allargs1.(j) acc | _ -> acc) Idmap.empty lnk @@ -696,10 +696,10 @@ let build_link_map allargs1 allargs2 lnk = forall recparams1 (recparams2 without linked params), forall ordparams1 (ordparams2 without linked params), - H1a' -> H2a' -> ... -> H2a' -> H2b'(shifted) -> ... + H1a' -> H2a' -> ... -> H2a' -> H2b'(shifted) -> ... -> (newI x1 ... z1 x2 y2 ...z2 without linked params) - where Hix' have been adapted, ie: + where Hix' have been adapted, ie: - linked vars have been changed, - rec calls to I1 and I2 have been replaced by rec calls to newI. More precisely calls to I1 and I2 have been merge by an @@ -715,26 +715,26 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr) (* FIXME: les noms des parametres corerspondent en principe au parametres du niveau mib, mais il faudrait s'en assurer *) (* shift.nfunresprmsx last args are functional result *) - let nargs1 = + let nargs1 = shift.mib1.mind_nparams + shift.oib1.mind_nrealargs - shift.nfunresprms1 in let nargs2 = shift.mib2.mind_nparams + shift.oib2.mind_nrealargs - shift.nfunresprms2 in let allargs1,rest1 = raw_decompose_prod_or_letin_n nargs1 typcstr1 in - let allargs2,rest2 = raw_decompose_prod_or_letin_n nargs2 typcstr2 in + let allargs2,rest2 = raw_decompose_prod_or_letin_n nargs2 typcstr2 in (* Build map of linked args of [typcstr2], and apply it to [typcstr2]. *) let linked_map = build_link_map allargs1 allargs2 shift.lnk2 in let rest2 = change_vars linked_map rest2 in let hyps1,concl1 = raw_decompose_prod_or_letin rest1 in let hyps2,concl2' = raw_decompose_prod_or_letin rest2 in - let ltyp,concl2 = + let ltyp,concl2 = merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in let _ = prNamedRLDecl "ltyp result:" ltyp in let typ = raw_compose_prod_or_letin concl2 (List.rev ltyp) in - let revargs1 = + let revargs1 = list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) in let _ = prNamedRLDecl "ltyp allargs1" allargs1 in let _ = prNamedRLDecl "ltyp revargs1" revargs1 in - let revargs2 = + let revargs2 = list_filteri (fun i _ -> isArg_stable shift.lnk2.(i)) (List.rev allargs2) in let _ = prNamedRLDecl "ltyp allargs2" allargs2 in let _ = prNamedRLDecl "ltyp revargs2" revargs2 in @@ -746,7 +746,7 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr) (** constructor numbering *) let fresh_cstror_suffix , cstror_suffix_init = let cstror_num = ref 0 in - (fun () -> + (fun () -> let res = string_of_int !cstror_num in cstror_num := !cstror_num + 1; res) , @@ -755,7 +755,7 @@ let fresh_cstror_suffix , cstror_suffix_init = (** [merge_constructor_id id1 id2 shift] returns the identifier of the new constructor from the id of the two merged constructor and the merging info. *) -let merge_constructor_id id1 id2 shift:identifier = +let merge_constructor_id id1 id2 shift:identifier = let id = string_of_id shift.ident ^ "_" ^ fresh_cstror_suffix () in next_ident_fresh (id_of_string id) @@ -765,43 +765,43 @@ let merge_constructor_id id1 id2 shift:identifier = constructor [(name*type)]. These are translated to rawterms first, each of them having distinct var names. *) let rec merge_constructors (shift:merge_infos) (avoid:Idset.t) - (typcstr1:(identifier * rawconstr) list) + (typcstr1:(identifier * rawconstr) list) (typcstr2:(identifier * rawconstr) list) : (identifier * rawconstr) list = - List.flatten + List.flatten (List.map - (fun (id1,rawtyp1) -> + (fun (id1,rawtyp1) -> List.map - (fun (id2,rawtyp2) -> + (fun (id2,rawtyp2) -> let typ = merge_one_constructor shift rawtyp1 rawtyp2 in let newcstror_id = merge_constructor_id id1 id2 shift in let _ = prstr "\n**************\n" in newcstror_id , typ) typcstr2) typcstr1) - + (** [merge_inductive_body lnk shift avoid oib1 oib2] merges two inductive bodies [oib1] and [oib2], linking with [lnk], params info in [shift], avoiding identifiers in [avoid]. *) let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) (oib2:one_inductive_body) = (* building rawconstr type of constructors *) - let mkrawcor nme avoid typ = + let mkrawcor nme avoid typ = (* first replace rel 1 by a varname *) let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in Detyping.detype false (Idset.elements avoid) [] substindtyp in - let lcstr1: rawconstr list = + let lcstr1: rawconstr list = Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in (* add to avoid all indentifiers of lcstr1 *) let avoid2 = Idset.union avoid (ids_of_rawlist avoid lcstr1) in - let lcstr2 = + let lcstr2 = Array.to_list (Array.map (mkrawcor ind2name avoid2) oib2.mind_user_lc) in let avoid3 = Idset.union avoid (ids_of_rawlist avoid lcstr2) in - let params1 = - try fst (raw_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) + let params1 = + try fst (raw_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) with _ -> [] in - let params2 = - try fst (raw_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) + let params2 = + try fst (raw_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) with _ -> [] in let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in @@ -819,17 +819,17 @@ let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) let rec merge_mutual_inductive_body (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) (shift:merge_infos) = (* Mutual not treated, we take first ind body of each. *) - merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0) + merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0) + - let rawterm_to_constr_expr x = (* build a constr_expr from a rawconstr *) Flags.with_option Flags.raw_print (Constrextern.extern_rawtype Idset.empty) x -let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = +let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let params = prms2 @ prms1 in let resparams = List.fold_left - (fun acc (nme,tp) -> + (fun acc (nme,tp) -> let _ = prstr "param :" in let _ = prNamedRConstr (string_of_name nme) tp in let _ = prstr " ; " in @@ -837,18 +837,18 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = LocalRawAssum ([(dummy_loc,nme)], Topconstr.default_binder_kind, typ) :: acc) [] params in let concl = Constrextern.extern_constr false (Global.env()) concl in - let arity,_ = - List.fold_left - (fun (acc,env) (nm,_,c) -> + let arity,_ = + List.fold_left + (fun (acc,env) (nm,_,c) -> let typ = Constrextern.extern_constr false env c in let newenv = Environ.push_rel (nm,None,c) env in CProdN (dummy_loc, [[(dummy_loc,nm)],Topconstr.default_binder_kind,typ] , acc) , newenv) (concl,Global.env()) - (shift.funresprms2 @ shift.funresprms1 - @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in + (shift.funresprms2 @ shift.funresprms1 + @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in resparams,arity - + (** [rawterm_list_to_inductive_expr ident rawlist] returns the induct_expr corresponding to the the list of constructor types @@ -859,17 +859,17 @@ let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift let lident = dummy_loc, shift.ident in let bindlist , cstr_expr = (* params , arities *) merge_rec_params_and_arity prms1 prms2 shift mkSet in - let lcstor_expr : (bool * (lident * constr_expr)) list = + let lcstor_expr : (bool * (lident * constr_expr)) list = List.map (* zeta_normalize t ? *) (fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t)) - rawlist in + rawlist in lident , bindlist , Some cstr_expr , lcstor_expr let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = match rdecl with - | (nme,None,t) -> + | (nme,None,t) -> let traw = Detyping.detype false [] [] t in RProd (dummy_loc,nme,Explicit,traw,t2) | (_,Some _,_) -> assert false @@ -879,7 +879,7 @@ let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = match rdecl with - | (nme,None,t) -> + | (nme,None,t) -> let traw = Detyping.detype false [] [] t in RProd (dummy_loc,nme,Explicit,traw,t2) | (_,Some _,_) -> assert false @@ -888,7 +888,7 @@ let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = (** [merge_inductive ind1 ind2 lnk] merges two graphs, linking variables specified in [lnk]. Graphs are not supposed to be mutual inductives for the moment. *) -let merge_inductive (ind1: inductive) (ind2: inductive) +let merge_inductive (ind1: inductive) (ind2: inductive) (lnk1: linked_var array) (lnk2: linked_var array) id = let env = Global.env() in let mib1,_ = Inductive.lookup_mind_specif env ind1 in @@ -898,14 +898,14 @@ let merge_inductive (ind1: inductive) (ind2: inductive) let shift_prm = shift_linked_params mib1 mib2 lnk1 lnk2 id in let prms1,prms2, rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in let _ = prstr "\nrawlist : " in - let _ = + let _ = List.iter (fun (nm,tp) -> prNamedRConstr (string_of_id nm) tp;prstr "\n") rawlist in let _ = prstr "\nend rawlist\n" in (* FIX: retransformer en constr ici - let shift_prm = + let shift_prm = { shift_prm with recprms1=prms1; - recprms1=prms1; + recprms1=prms1; } in *) let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) @@ -927,28 +927,28 @@ let find_Function_infos_safe (id:identifier): Indfun_common.function_info = [ind1] and [ind2]. identifiers occuring in both arrays [args1] and [args2] are considered linked (i.e. are the same variable) in the new graph. - + Warning: For the moment, repetitions of an id in [args1] or [args2] are not supported. *) -let merge (id1:identifier) (id2:identifier) (args1:identifier array) +let merge (id1:identifier) (id2:identifier) (args1:identifier array) (args2:identifier array) id : unit = let finfo1 = find_Function_infos_safe id1 in let finfo2 = find_Function_infos_safe id2 in (* FIXME? args1 are supposed unlinked. mergescheme (G x x) ?? *) (* We add one arg (functional arg of the graph) *) let lnk1 = Array.make (Array.length args1 + 1) Unlinked in - let lnk2' = (* args2 may be linked to args1 members. FIXME: same + let lnk2' = (* args2 may be linked to args1 members. FIXME: same as above: vars may be linked inside args2?? *) Array.mapi - (fun i c -> + (fun i c -> match array_find args1 (fun i x -> x=c) with | Some j -> Linked j - | None -> Unlinked) + | None -> Unlinked) args2 in (* We add one arg (functional arg of the graph) *) let lnk2 = Array.append lnk2' (Array.make 1 Unlinked) in (* setting functional results *) - let _ = lnk1.(Array.length lnk1 - 1) <- Funres in + let _ = lnk1.(Array.length lnk1 - 1) <- Funres in let _ = lnk2.(Array.length lnk2 - 1) <- Funres in merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id @@ -968,12 +968,12 @@ let remove_last_n_arg n c = (* [funify_branches relinfo nfuns branch] returns the branch [branch] of the relinfo [relinfo] modified to fit in a functional principle. - Things to do: + Things to do: - remove indargs from rel applications - replace *variables only* corresponding to function (recursive) results by the actual function application. *) -let funify_branches relinfo nfuns branch = - let mut_induct, induct = +let funify_branches relinfo nfuns branch = + let mut_induct, induct = match relinfo.indref with | None -> assert false | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind @@ -987,13 +987,13 @@ let funify_branches relinfo nfuns branch = match kind_of_term c with | Ind((u,i)) | Construct((u,_),i) -> i | _ -> assert false in - let _is_pred c shift = + let _is_pred c shift = match kind_of_term c with | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches) | _ -> false in (* FIXME: *) (Anonymous,Some mkProp,mkProp) - + let relprinctype_to_funprinctype relprinctype nfuns = let relinfo = compute_elim_sig relprinctype in @@ -1010,7 +1010,7 @@ let relprinctype_to_funprinctype relprinctype nfuns = args = remove_n_fst_list nfuns relinfo_noindarg.args; concl = popn nfuns relinfo_noindarg.concl } in - let new_branches = + let new_branches = List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in let relinfo_branches = { relinfo_argsok with branches = new_branches } in relinfo_branches @@ -1026,7 +1026,7 @@ let relprinctype_to_funprinctype relprinctype nfuns = url = "citeseer.ist.psu.edu/bundy93rippling.html" } *) -(* +(* *** Local Variables: *** *** compile-command: "make -C ../.. plugins/funind/merge.cmo" *** *** indent-tabs-mode: nil *** |