diff options
Diffstat (limited to 'plugins/funind/merge.ml')
-rw-r--r-- | plugins/funind/merge.ml | 1032 |
1 files changed, 1032 insertions, 0 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml new file mode 100644 index 00000000..f596e2d7 --- /dev/null +++ b/plugins/funind/merge.ml @@ -0,0 +1,1032 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Merging of induction principles. *) + +(*i $Id: i*) +open Libnames +open Tactics +open Indfun_common +open Util +open Topconstr +open Vernacexpr +open Pp +open Names +open Term +open Termops +open Declarations +open Environ +open Rawterm +open Rawtermops + +(** {1 Utilities} *) + +(** {2 Useful operations on constr and rawconstr} *) + +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 + then true + else false + +let rec compare_constr' 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 + (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 + +let understand = Pretyping.Default.understand Evd.empty (Global.env()) + +(** Operations on names and identifiers *) +let id_of_name = function + Anonymous -> id_of_string "H" + | Name id -> id;; +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 = + match x with + | 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 ans = CRef (Libnames.Ident (dummy_loc,id)) in + let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in + true + 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 res = ref id in + while ident_global_exist !res do res := Nameops.lift_subscript !res done; + !res + + +(** {2 Debugging} *) +(* comment this line to see debug msgs *) +let msg x = () ;; let pr_lconstr c = str "" +(* uncomment this to see debugging *) +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 = + begin + msg(str ""); + msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} "); + msg(str ""); + end +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 = + begin + prstr "[§§§ "; + prstr s; + prNamedLConstr_aux lc; + prstr " §§§]\n"; + end +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 = + begin + prstr s; prstr "\n"; prstr "{§§ "; + 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 + | _ -> assert false + ) lc; + prstr " §§}\n"; + prstr "\n"; + end + +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) -> + print_string (string_of_name nm^":"); + 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 -> + Printf.printf "arity : universe?"); + Array.iteri + (fun i x -> Printf.printf"type constr %d :" i ; prconstr x) + ib1.mind_user_lc + +(** {2 Misc} *) + +exception Found of int + +(* Array scanning *) + +let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int = + try + for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done; + 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 res = f !i acc x in i := !i + 1; res) + acc arr + +(* Like list_chop but except that [i] is the size of the suffix of [l]. *) +let list_chop_end i l = + let size_prefix = List.length l -i in + 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 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 + List.filter (fun x -> let res = f !i x in i := !i + 1; res) l + + +(** Iteration module *) +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 = + 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 = + 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 + + +(** {1 Parameters shifting and linking information} *) + +(** This type is used to deal with debruijn linked indices. When a + variable is linked to a previous one, we will ignore it and refer + to previous one. *) +type linked_var = + | Linked of int + | Unlinked + | Funres + +(** When merging two graphs, parameters may become regular arguments, + and thus be shifted. This type describes the result of computing + the changes. *) +type 'a shifted_params = + { + nprm1:'a; + nprm2:'a; + prm2_unlinked:'a list; (* ranks of unlinked params in nprms2 *) + nuprm1:'a; + nuprm2:'a; + nargs1:'a; + nargs2:'a; + } + + +let prlinked x = + match x with + | Linked i -> Printf.sprintf "Linked %d" i + | Unlinked -> Printf.sprintf "Unlinked" + | Funres -> Printf.sprintf "Funres" + +let linkmonad f lnkvar = + match lnkvar with + | Linked i -> Linked (f i) + | Unlinked -> Unlinked + | Funres -> Funres + +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 = + Printf.printf "links:\n"; + Link.iter (fun k e -> Printf.printf "%d : %s\n" k (prlinked e)) l; + Printf.printf "_____________\n" + +type 'a merged_arg = + | Prm_stable of 'a + | Prm_linked of 'a + | Prm_arg of 'a + | Arg_stable of 'a + | Arg_linked of 'a + | Arg_funres + +(** 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; + mib2: mutual_inductive_body; + oib2: one_inductive_body; + + (** Array of links of the first inductive (should be all stable) *) + lnk1: int merged_arg array; + + (** Array of links of the second inductive (point to the first ind param/args) *) + lnk2: int merged_arg array; + + (** rec params which remain rec param (ie not linked) *) + recprms1: rel_declaration list; + recprms2: rel_declaration 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; + notherprms1:int; + notherprms2:int; + + (** args which remain args in merge *) + args1:rel_declaration list; + args2:rel_declaration list; + nargs1:int; + nargs2:int; + + (** functional result args *) + funresprms1: rel_declaration list; + funresprms2: rel_declaration list; + nfunresprms1:int; + nfunresprms2:int; + } + + +let pr_merginfo x = + let i,s= + match x with + | Prm_linked i -> Some i,"Prm_linked" + | Arg_linked i -> Some i,"Arg_linked" + | Prm_stable i -> Some i,"Prm_stable" + | Prm_arg i -> Some i,"Prm_arg" + | Arg_stable i -> Some i,"Arg_stable" + | Arg_funres -> None , "Arg_funres" in + match i with + | Some i -> Printf.sprintf "%s(%d)" s i + | None -> Printf.sprintf "%s" s + +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 = + match x with Arg_stable _ | Prm_stable _ | Prm_arg _ -> true | _ -> false + +let isArg_funres x = match x with Arg_funres -> true | _ -> false + +let filter_shift_stable (lnk:int merged_arg array) (l:'a list): 'a list = + let prms = list_filteri (fun i _ -> isPrm_stable lnk.(i)) l in + let args = list_filteri (fun i _ -> isArg_stable lnk.(i)) l in + let fres = list_filteri (fun i _ -> isArg_funres lnk.(i)) l in + prms@args@fres + +(** Reverse the link map, keeping only linked vars, elements are 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 -> + 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 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 -> + match x with + | Prm_linked i -> array_switch larr i j + | Arg_linked i -> array_switch larr i j + | Prm_stable i -> () + | Prm_arg i -> () + | Arg_stable i -> () + | Arg_funres -> () + ) lnk in + filter_shift_stable lnk (Array.to_list larr) + + + + +(** {1 Utilities for merging} *) + +let ind1name = id_of_string "__ind1" +let ind2name = id_of_string "__ind2" + +(** Performs verifications on two graphs before merging: they must not + be co-inductive, and for the moment they must not be mutual + either. *) +let verify_inds mib1 mib2 = + if not mib1.mind_finite then error "First argument is coinductive"; + if not mib2.mind_finite then error "Second argument is coinductive"; + if mib1.mind_ntypes <> 1 then error "First argument is mutual"; + if mib2.mind_ntypes <> 1 then error "Second argument is mutual"; + () + +(* +(** [build_raw_params prms_decl avoid] returns a list of variables + attributed to the list of decl [prms_decl], avoiding names in + [avoid]. *) +let build_raw_params prms_decl avoid = + let dummy_constr = compose_prod (List.map (fun (x,_,z) -> x,z) prms_decl) (mkRel 1) in + let _ = prNamedConstr "DUMMY" dummy_constr in + let dummy_rawconstr = Detyping.detype false avoid [] dummy_constr in + let _ = prNamedRConstr "RAWDUMMY" dummy_rawconstr in + let res,_ = raw_decompose_prod dummy_rawconstr in + let comblist = List.combine prms_decl res in + comblist, res , (avoid @ (Idset.elements (ids_of_rawterm dummy_rawconstr))) +*) + +let ids_of_rawlist avoid rawl = + List.fold_left Idset.union avoid (List.map ids_of_rawterm rawl) + + + +(** {1 Merging function graphs} *) + +(** [shift_linked_params mib1 mib2 lnk] Computes which parameters (rec + uniform and ordinary ones) of mutual inductives [mib1] and [mib2] + 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. + + (I x1 x2 ... xk ... xk' ... xn) + (J y1 y2 ... xl ... yl' ... ym) + + Problem is, if some rec unif params are linked to non rec unif + ones, they become non rec (and the following too). And functinal + argument have to be shifted at the end *) +let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array) id = + let _ = prstr "\nYOUHOU shift\n" in + 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 + List.exists (fun x -> not (is_param_of_mib2 x)) targets + with Not_found -> false in + let mlnk1 = + Array.mapi + (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 + | true , true , _ -> Prm_arg i (* recparam becoming ordinary *) + | true , false , _-> Prm_stable i (* recparam remains recparam*) + | false , false , Funres -> Arg_funres + | _ , _ , 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 = + Array.mapi + (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) -> + Prm_arg j (* recparam becoming ordinary *) + | true , Linked j -> Prm_linked j (*recparam linked to recparam*) + | true , Unlinked -> Prm_stable i (* recparam remains recparam*) + | false , Linked j -> Arg_linked j (* Args of lnk2 lost *) + | false , Unlinked -> Arg_stable i (* Args of lnk2 remains *) + | false , Funres -> Arg_funres + | true , Funres -> assert false (* fun res cannot be a rec param *) + ) + lnk2 in + let oib1 = mib1.mind_packets.(0) in + let oib2 = mib2.mind_packets.(0) in + (* 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 = + list_fold_lefti + (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 + | Prm_arg _ -> acc1 , x::acc2 , acc3, acc4 + | Arg_stable _ -> acc1 , acc2 , x::acc3, acc4 + | Arg_funres -> acc1 , acc2 , acc3, x::acc4 + | _ -> acc1 , acc2 , acc3, acc4) + ([],[],[],[]) arity_ctxt in +(* 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") + otherprms1 in + let _ = prstr "\notherprms2:\n" in + let _ = + List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n") + otherprms2 in + { + ident=id; + mib1=mib1; + oib1 = oib1; + mib2=mib2; + oib2 = oib2; + lnk1 = mlnk1; + lnk2 = mlnk2; + nrecprms1 = n_params1; + recprms1 = recprms1; + otherprms1 = otherprms1; + args1 = args1; + funresprms1 = funresprms1; + notherprms1 = Array.length mlnk1 - n_params1; + nfunresprms1 = List.length funresprms1; + nargs1 = List.length args1; + nrecprms2 = n_params2; + recprms2 = recprms2; + otherprms2 = otherprms2; + args2 = args2; + funresprms2 = funresprms2; + notherprms2 = Array.length mlnk2 - n_params2; + nargs2 = List.length args2; + nfunresprms2 = List.length funresprms2; + } + + + + +(** {1 Merging functions} *) + +exception NoMerge + +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 -> + 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 + 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 + 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 lnk = Array.append shift.lnk1 shift.lnk2 in + match c1 , c2 with + | 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 + 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 + 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 + + + +(* 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) + filter_shift_stable : (Names.name * rawconstr option * rawconstr option) list = + let mergeonehyp t reldecl = + match reldecl with + | (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,None) | (nme,Some _,Some _) -> assert false in + match ltyp with + | [] -> [] + | (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 = + List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec + + +let find_app (nme:identifier) ltyp = + try + ignore + (List.map + (fun x -> + match x with + | _,None,Some (RApp(_,f,_)) when isVarf nme f -> raise (Found 0) + | _ -> ()) + ltyp); + false + with Found _ -> true + +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 + (ltyp1:(name * rawconstr option * rawconstr option) list) + (concl1:rawconstr) (ltyp2:(name * rawconstr option * rawconstr option) list) concl2 + : (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 + let _ = prstr "\nltyp 2 : " in + let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp2 in + 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 + then (* merge_rec_hyps shift accrec1 ltyp2 filter_shift_stable *) + 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 + (* if rec calls in accrec1 and not in ltyp2, add one to ltyp2 *) + 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 + filter_shift_stable_right + else ltyp2 in + let _ = prstr"\nrechyps : " in + let _ = List.iter(fun (nm,lbdy,tp)-> prnt_prod_or_letin nm lbdy tp) rechyps in + let _ = prstr "MERGE CONCL : " in + let _ = prNamedRConstr "concl1" concl1 in + let _ = prstr " with " in + let _ = prNamedRConstr "concl2" concl2 in + let _ = prstr "\n" in + 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 -> + (match t1 with + | 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 -> + (* FIXME: what if ind1name appears in bd? *) + let recres, recconcl2 = + merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in + ((nme,Some bd,None) :: recres) , recconcl2 + | (_,None,None)::_ | (_,Some _,Some _)::_ -> assert false + in + res + + +(** [build_link_map_aux allargs1 allargs2 shift] returns the mapping of + linked args [allargs2] to target args of [allargs1] as specified + in [shift]. [allargs1] and [allargs2] are in reverse order. Also + returns the list of unlinked vars of [allargs2]. *) +let build_link_map_aux (allargs1:identifier array) (allargs2:identifier array) + (lnk:int merged_arg array) = + array_fold_lefti + (fun i acc e -> + if i = Array.length lnk - 1 then acc (* functional arg, not in allargs *) + else + match e with + | Prm_linked j | Arg_linked j -> Idmap.add allargs2.(i) allargs1.(j) acc + | _ -> acc) + Idmap.empty lnk + +let build_link_map allargs1 allargs2 lnk = + let allargs1 = + Array.of_list (List.rev (List.map (fun (x,_,_) -> id_of_name x) allargs1)) in + let allargs2 = + Array.of_list (List.rev (List.map (fun (x,_,_) -> id_of_name x) allargs2)) in + build_link_map_aux allargs1 allargs2 lnk + + +(** [merge_one_constructor lnk shift typcstr1 typcstr2] merges the two + constructor rawtypes [typcstr1] and [typcstr2]. [typcstr1] and + [typcstr2] contain all parameters (including rec. unif. ones) of + their inductive. + + if [typcstr1] and [typcstr2] are of the form: + + forall recparams1, forall ordparams1, H1a -> H2a... (I1 x1 y1 ... z1) + forall recparams2, forall ordparams2, H2b -> H2b... (I2 x2 y2 ... z2) + + we build: + + forall recparams1 (recparams2 without linked params), + forall ordparams1 (ordparams2 without linked params), + H1a' -> H2a' -> ... -> H2a' -> H2b'(shifted) -> ... + -> (newI x1 ... z1 x2 y2 ...z2 without linked params) + + 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 + experimental heuristic (in particular if n o rec calls for I1 + or I2 is found, we use the conclusion as a rec call). See + [merge_types] above. + + Precond: vars sets of [typcstr1] and [typcstr2] must be disjoint. + + TODO: return nothing if equalities (after linking) are contradictory. *) +let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr) + (typcstr2:rawconstr) : 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 = + 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 + (* 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 = + 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 = + 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 = + 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 + let typwithprms = + raw_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in + typwithprms + + +(** constructor numbering *) +let fresh_cstror_suffix , cstror_suffix_init = + let cstror_num = ref 0 in + (fun () -> + let res = string_of_int !cstror_num in + cstror_num := !cstror_num + 1; + res) , + (fun () -> cstror_num := 0) + +(** [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 id = string_of_id shift.ident ^ "_" ^ fresh_cstror_suffix () in + next_ident_fresh (id_of_string id) + + + +(** [merge_constructors lnk shift avoid] merges the two list of + 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) + (typcstr2:(identifier * rawconstr) list) : (identifier * rawconstr) list = + List.flatten + (List.map + (fun (id1,rawtyp1) -> + List.map + (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 = + (* 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 = + 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 = + 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)) + with _ -> [] in + 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 + let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in + + cstror_suffix_init(); + params1,params2,merge_constructors shift avoid3 lcstr1 lcstr2 + + +(** [merge_mutual_inductive_body lnk mib1 mib2 shift] merge mutual + inductive bodies [mib1] and [mib2] linking vars with + [lnk]. [shift] information on parameters of the new inductive. + For the moment, inductives are supposed to be non mutual. +*) +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) + + +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 params = prms2 @ prms1 in + let resparams = + List.fold_left + (fun acc (nme,tp) -> + let _ = prstr "param :" in + let _ = prNamedRConstr (string_of_name nme) tp in + let _ = prstr " ; " in + let typ = rawterm_to_constr_expr tp in + 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 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 + resparams,arity + + + +(** [rawterm_list_to_inductive_expr ident rawlist] returns the + induct_expr corresponding to the the list of constructor types + [rawlist], named ident. + FIXME: params et cstr_expr (arity) *) +let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift + (rawlist:(identifier * rawconstr) list) = + 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 = + List.map (* zeta_normalize t ? *) + (fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t)) + rawlist in + lident , bindlist , Some cstr_expr , lcstor_expr + + + +let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = + match rdecl with + | (nme,None,t) -> + let traw = Detyping.detype false [] [] t in + RProd (dummy_loc,nme,Explicit,traw,t2) + | (_,Some _,_) -> assert false + + + + +let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = + match rdecl with + | (nme,None,t) -> + let traw = Detyping.detype false [] [] t in + RProd (dummy_loc,nme,Explicit,traw,t2) + | (_,Some _,_) -> assert false + + +(** [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) + (lnk1: linked_var array) (lnk2: linked_var array) id = + let env = Global.env() in + let mib1,_ = Inductive.lookup_mind_specif env ind1 in + let mib2,_ = Inductive.lookup_mind_specif env ind2 in + let _ = verify_inds mib1 mib2 in (* raises an exception if something wrong *) + (* compute params that become ordinary args (because linked to ord. args) *) + 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 _ = + 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 = + { shift_prm with + recprms1=prms1; + recprms1=prms1; + } in *) + let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in + (* Declare inductive *) + let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in + let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in + (* Declare the mutual inductive block with its associated schemes *) + ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls) + + +(* Find infos on identifier id. *) +let find_Function_infos_safe (id:identifier): Indfun_common.function_info = + let kn_of_id x = + let f_ref = Libnames.Ident (dummy_loc,x) in + locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref) + locate_constant f_ref in + try find_Function_infos (kn_of_id id) + with Not_found -> + errorlabstrm "indfun" (Nameops.pr_id id ++ str " has no functional scheme") + +(** [merge id1 id2 args1 args2 id] builds and declares a new inductive + type called [id], representing the merged graphs of both graphs + [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) + (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 + as above: vars may be linked inside args2?? *) + Array.mapi + (fun i c -> + match array_find_i (fun i x -> x=c) args1 with + | Some j -> Linked j + | 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 _ = lnk2.(Array.length lnk2 - 1) <- Funres in + merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id + + +let remove_last_arg c = + let (x,y) = decompose_prod c in + let xnolast = List.rev (List.tl (List.rev x)) in + compose_prod xnolast y + +let rec remove_n_fst_list n l = if n=0 then l else remove_n_fst_list (n-1) (List.tl l) +let remove_n_last_list n l = List.rev (remove_n_fst_list n (List.rev l)) + +let remove_last_n_arg n c = + let (x,y) = decompose_prod c in + let xnolast = remove_n_last_list n x in + compose_prod xnolast y + +(* [funify_branches relinfo nfuns branch] returns the branch [branch] + of the relinfo [relinfo] modified to fit in a functional principle. + 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 = + match relinfo.indref with + | None -> assert false + | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind + | _ -> assert false in + let is_dom c = + match kind_of_term c with + | Ind((u,_)) | Construct((u,_),_) -> u = mut_induct + | _ -> false in + let _dom_i c = + assert (is_dom c); + match kind_of_term c with + | Ind((u,i)) | Construct((u,_),i) -> i + | _ -> assert false in + 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 + assert (not relinfo.farg_in_concl); + assert (relinfo.indarg_in_concl); + (* first remove indarg and indarg_in_concl *) + let relinfo_noindarg = { relinfo with + indarg_in_concl = false; indarg = None; + concl = remove_last_arg (pop relinfo.concl); } in + (* the nfuns last induction arguments are functional ones: remove them *) + let relinfo_argsok = { relinfo_noindarg with + nargs = relinfo_noindarg.nargs - nfuns; + (* args is in reverse order, so remove fst *) + args = remove_n_fst_list nfuns relinfo_noindarg.args; + concl = popn nfuns relinfo_noindarg.concl + } in + 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 + +(* @article{ bundy93rippling, + author = "Alan Bundy and Andrew Stevens and Frank van Harmelen and Andrew Ireland and Alan Smaill", + title = "Rippling: A Heuristic for Guiding Inductive Proofs", + journal = "Artificial Intelligence", + volume = "62", + number = "2", + pages = "185-253", + year = "1993", + url = "citeseer.ist.psu.edu/bundy93rippling.html" } + + *) +(* +*** Local Variables: *** +*** compile-command: "make -C ../.. plugins/funind/merge.cmo" *** +*** indent-tabs-mode: nil *** +*** End: *** +*) |