summaryrefslogtreecommitdiff
path: root/contrib/funind/merge.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind/merge.ml')
-rw-r--r--contrib/funind/merge.ml514
1 files changed, 361 insertions, 153 deletions
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index 1b796a81..ec456aae 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -9,13 +9,16 @@
(* 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
@@ -25,6 +28,8 @@ open Rawtermops
(** {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
@@ -110,6 +115,19 @@ let prNamedLDecl s lc =
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
@@ -193,7 +211,7 @@ type linked_var =
| Funres
(** When merging two graphs, parameters may become regular arguments,
- and thus be shifted. This type describe the result of computing
+ and thus be shifted. This type describes the result of computing
the changes. *)
type 'a shifted_params =
{
@@ -237,39 +255,47 @@ type 'a merged_arg =
| 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 *)
+ 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) *)
+
+ (** 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) *)
+
+ (** Array of links of the second inductive (point to the first ind param/args) *)
lnk2: int merged_arg array;
- (* number of rec params of ind1 which remai rec param in merge *)
- nrecprms1: int;
- (* number of other rec params of ind1 (which become non parm) *)
- notherprms1:int;
- (* number of functional result params of ind2 (which become non parm) *)
- nfunresprms1:int;
- (* list of decl of rec parms from ind1 which remain parms *)
+
+ (** rec params which remain rec param (ie not linked) *)
recprms1: rel_declaration list;
- (* List of other rec parms from ind1 *)
- otherprms1: rel_declaration list; (* parms that became args *)
- funresprms1: rel_declaration list; (* parms that are functional result args *)
- (* number of rec params of ind2 which remain rec param in merge (and not linked) *)
+ recprms2: rel_declaration list;
+ nrecprms1: int;
nrecprms2: int;
- (* number of other params of ind2 (which become non rec parm) *)
+
+ (** 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;
- (* number of functional result params of ind2 (which become non parm) *)
+
+ (** 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;
- (* list of decl of rec parms from ind2 which remain parms (and not linked) *)
- recprms2: rel_declaration list;
- (* List of other rec parms from ind2 (which are linked or become non parm) *)
- otherprms2: rel_declaration list;
- funresprms2: rel_declaration list; (* parms that are functional result args *)
}
@@ -288,7 +314,11 @@ let pr_merginfo x =
let isPrm_stable x = match x with Prm_stable _ -> true | _ -> false
-let isArg_stable x = match x with Arg_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
@@ -346,6 +376,24 @@ let verify_inds mib1 mib2 =
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} *)
@@ -366,6 +414,7 @@ let verify_inds mib1 mib2 =
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
@@ -409,15 +458,29 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
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) 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
- | Prm_arg _ | Arg_stable _ -> acc1 , x::acc2 , acc3
- | Arg_funres -> acc1 , acc2 , x::acc3
- | _ -> acc1 , acc2 , acc3) (* Prm_linked and Arg_xxx = forget it *)
- ([],[],[]) arity_ctxt in
- let recprms1,otherprms1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in
- let recprms2,otherprms2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
+ | 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;
@@ -429,14 +492,18 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
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;
}
@@ -447,45 +514,61 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
exception NoMerge
-(* lnk is an link array of *all* args (from 1 and 2) *)
-let 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 ->
+ 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
- | _ -> raise NoMerge
-
-let merge_app_unsafe c1 c2 shift filter_shift_stable =
+ | 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)
- | _ -> raise NoMerge
+ (* 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 nrach 1 with all rec calls of branch 2. *)
+ calls of branch 1 with all rec calls of branch 2. *)
(* TODO: reecrire cette heuristique (jusqu'a merge_types) *)
-let onefoud = ref false (* Ugly *)
-
-let rec merge_rec_hyps shift accrec (ltyp:(Names.name * Rawterm.rawconstr) list)
- filter_shift_stable =
+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,(RApp(_,f, largs) as t)) :: lt when isVarf ind2name f ->
- let _ = onefoud := true in
- let rechyps =
- List.map
- (fun (nme,ind) ->
- match ind with
- | RApp(_,i,args) ->
- nme, merge_app_unsafe ind t shift filter_shift_stable
- | _ -> assert false)
- accrec in
+ | (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
@@ -494,50 +577,58 @@ 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: (name * rawconstr) list) =
+let find_app (nme:identifier) ltyp =
try
ignore
(List.map
(fun x ->
match x with
- | _,(RApp(_,f,_)) when isVarf nme f -> raise (Found 0)
+ | _,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) list)
- concl1 (ltyp2:(name * rawconstr) list) concl2
- : (name * rawconstr) list * rawconstr =
+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,tp) -> prNamedRConstr (string_of_name nm) tp) ltyp1 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,tp) -> prNamedRConstr (string_of_name nm) tp) ltyp2 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 _ = if isrec2 then prstr " ISREC2 TRUE" else prstr " ISREC2 FALSE" in
- let _ = if isrec1 then prstr " ISREC1 TRUE\n" else prstr " ISREC1 FALSE\n" in
let rechyps =
if isrec1 && isrec2
- then merge_rec_hyps shift accrec1 ltyp2 filter_shift_stable
+ 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",concl2])
- filter_shift_stable
+ 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",concl1] ltyp2
+ then merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2
filter_shift_stable_right
- else [] in
+ else ltyp2 in
let _ = prstr"\nrechyps : " in
- let _ = List.iter
- (fun (nm,tp) -> prNamedRConstr (string_of_name nm) tp) rechyps 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
@@ -548,15 +639,22 @@ let rec merge_types shift accrec1 (ltyp1:(name * rawconstr) list)
let _ = prstr "FIN " in
let _ = prNamedRConstr "concl" concl in
let _ = prstr "\n" in
+
rechyps , concl
- | (nme,t1)as e ::lt1 ->
- match t1 with
+ | (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,t1) :: recres) , recconcl2
+ ((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
@@ -578,9 +676,9 @@ let build_link_map_aux (allargs1:identifier array) (allargs2:identifier array)
let build_link_map allargs1 allargs2 lnk =
let allargs1 =
- Array.of_list (List.rev (List.map (fun (x,y) -> id_of_name x) allargs1)) in
+ 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,y) -> id_of_name x) allargs2)) in
+ Array.of_list (List.rev (List.map (fun (x,_,_) -> id_of_name x) allargs2)) in
build_link_map_aux allargs1 allargs2 lnk
@@ -598,7 +696,7 @@ let build_link_map allargs1 allargs2 lnk =
forall recparams1 (recparams2 without linked params),
forall ordparams1 (ordparams2 without linked params),
- H1a' -> H2a' -> ... -> H2a' -> H2b' -> ...
+ H1a' -> H2a' -> ... -> H2a' -> H2b'(shifted) -> ...
-> (newI x1 ... z1 x2 y2 ...z2 without linked params)
where Hix' have been adapted, ie:
@@ -621,21 +719,27 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr)
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_n nargs1 typcstr1 in
- let allargs2,rest2 = raw_decompose_prod_n nargs2 typcstr2 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 rest1 in
- let hyps2,concl2' = raw_decompose_prod 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 typ = raw_compose_prod concl2 (List.rev ltyp) 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 typwithprms = raw_compose_prod typ (List.rev revargs2 @ List.rev revargs1) 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
@@ -661,22 +765,16 @@ 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 * types) list)
- (typcstr2:(identifier * types) list) : (identifier * rawconstr) list =
+ (typcstr1:(identifier * rawconstr) list)
+ (typcstr2:(identifier * rawconstr) list) : (identifier * rawconstr) list =
List.flatten
(List.map
- (fun (id1,typ1) ->
- let typ1 = substitterm 0 (mkRel 1) (mkVar ind1name) typ1 in
- let rawtyp1 = Detyping.detype false (Idset.elements avoid) [] typ1 in
- let idsoftyp1:Idset.t = ids_of_rawterm rawtyp1 in
+ (fun (id1,rawtyp1) ->
List.map
- (fun (id2,typ2) ->
- let typ2 = substitterm 0 (mkRel 1) (mkVar ind2name) typ2 in
- (* Avoid also rawtyp1 names *)
- let avoid2 = Idset.union avoid idsoftyp1 in
- let rawtyp2 = Detyping.detype false (Idset.elements avoid2) [] typ2 in
+ (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)
@@ -685,22 +783,33 @@ let rec merge_constructors (shift:merge_infos) (avoid:Idset.t)
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) : (identifier * rawconstr) list =
- let lcstr1 = Array.to_list oib1.mind_user_lc in
- let lcstr2 = Array.to_list oib2.mind_user_lc in
+ (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();
- merge_constructors shift avoid lcstr1 lcstr2
+ params1,params2,merge_constructors shift avoid3 lcstr1 lcstr2
-(** [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 prms_decl mkProp in
- let dummy_rawconstr = Detyping.detype false avoid [] dummy_constr in
- let res,_ = raw_decompose_prod dummy_rawconstr in
- res , (avoid @ (Idset.elements (ids_of_rawterm dummy_rawconstr)))
(** [merge_mutual_inductive_body lnk mib1 mib2 shift] merge mutual
inductive bodies [mib1] and [mib2] linking vars with
@@ -708,42 +817,35 @@ let build_raw_params prms_decl avoid =
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) =
+ (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) (shift:merge_infos) =
(* Mutual not treated, we take first ind body of each. *)
- let nprms1 = mib1.mind_nparams_rec in (* n# of rec uniform parms of mib1 *)
- let prms1 = (* rec uniform parms of mib1 *)
- List.map (fun (x,_,y) -> x,y) (fst (list_chop nprms1 mib1.mind_params_ctxt)) in
-
- (* useless: *)
- let prms1_named,avoid' = build_raw_params prms1 [] in
- let prms2_named,avoid = build_raw_params prms1 avoid' in
- let avoid:Idset.t = List.fold_right Idset.add avoid Idset.empty in
- (* *** *)
-
- merge_inductive_body shift avoid 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 params1 params2 shift (concl:constr) =
- let params = shift.recprms1 @ shift.recprms2 in
- let resparams, _ =
+let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
+ let params = prms2 @ prms1 in
+ let resparams =
List.fold_left
- (fun (acc,env) (nme,_,tp) ->
- let typ = Constrextern.extern_constr false env tp in
- let newenv = Environ.push_rel (nme,None,tp) env in
- LocalRawAssum ([(dummy_loc,nme)] , typ) :: acc , newenv)
- ([],Global.env())
- params in
+ (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)],typ] , acc) , newenv)
+ CProdN (dummy_loc, [[(dummy_loc,nm)],Topconstr.default_binder_kind,typ] , acc) , newenv)
(concl,Global.env())
- (shift.otherprms1@shift.otherprms2@shift.funresprms1@shift.funresprms2) in
+ (shift.funresprms2 @ shift.funresprms1
+ @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in
resparams,arity
@@ -752,20 +854,37 @@ let merge_rec_params_and_arity params1 params2 shift (concl:constr) =
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 mib1 mib2 shift
+let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
(rawlist:(identifier * rawconstr) list):inductive_expr =
- let rawterm_to_constr_expr x = (* build a constr_expr from a rawconstr *)
- Options.with_option Options.raw_print (Constrextern.extern_rawtype Idset.empty) x in
let lident = dummy_loc, shift.ident in
let bindlist , cstr_expr = (* params , arities *)
- merge_rec_params_and_arity
- mib1.mind_params_ctxt mib2.mind_params_ctxt shift mkSet in
+ 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 , 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. *)
@@ -777,35 +896,124 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
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 rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in
- let indexpr = rawterm_list_to_inductive_expr mib1 mib2 shift_prm rawlist 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 *)
Command.build_mutual [(indexpr,None)] true (* means: not coinductive *)
-
-let merge (cstr1:constr) (cstr2:constr) (args1:constr array) (args2:constr array) id =
- let env = Global.env() in
- let ind1,_cstrlist1 = Inductiveops.find_inductive env Evd.empty cstr1 in
- let ind2,_cstrlist2 = Inductiveops.find_inductive env Evd.empty cstr2 in
- let lnk1 = (* args1 are unlinked. FIXME? mergescheme (G x x) ?? *)
- Array.mapi (fun i c -> Unlinked) args1 in
- let _ = lnk1.(Array.length lnk1 - 1) <- Funres in (* last arg is functional result *)
- let lnk2 = (* args2 may be linked to args1 members. FIXME: same
- as above: vars may be linked inside args2?? *)
+(* 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 args1 (fun i x -> x=c) with
| Some j -> Linked j
| None -> Unlinked)
args2 in
- let _ = lnk2.(Array.length lnk2 - 1) <- Funres in (* last arg is functional result *)
- let resa = merge_inductive ind1 ind2 lnk1 lnk2 id in
- resa
-
-
-
+ (* 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",
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-16 17:45:11 +0000