Fixes in experimental merging of functional graphs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9305 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 100 insertions, 39 deletions

diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index 63ceba624..1b796a817 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -56,7 +56,7 @@ 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) -> x = f 
+      | RVar (_,x) -> Pervasives.compare x f = 0 
       | _ -> false
 
 (** [ident_global_exist id] returns true if identifier [id] is linked
@@ -78,29 +78,31 @@ let next_ident_fresh (id:identifier) =
 
 (** {2 Debugging} *)
 (* comment this line to see debug msgs *)
-(* let msg x = () ;; let pr_lconstr c = str "" *)
+let msg x = () ;; let pr_lconstr c = str ""
 (* uncomment this to see debugging *)
-let prconstr c =  msg (str"  " ++ Printer.pr_lconstr c ++ str"\n")
+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^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n");
+    msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} ");
     msg(str "");
   end
 let prNamedRConstr s c = 
   begin
     msg(str "");
-    msg(str(s^"==>\n ") ++ Printer.pr_rawconstr c ++ str "\n<==\n");
+    msg(str(s^" {§ ") ++ Printer.pr_rawconstr c ++ str " §} ");
     msg(str "");
   end
-let prNamedLConstr_aux lc = 
-  List.iter (prNamedConstr "#>") lc
+let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc
 let prNamedLConstr s lc = 
   begin
+    prstr "[§§§ ";
     prstr s;
-    prNamedLConstr_aux lc
+    prNamedLConstr_aux lc;
+    prstr " §§§]\n";
   end
 let prNamedLDecl s lc = 
   begin
@@ -308,6 +310,23 @@ let revlinked lnk =
             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)
 
 
 
@@ -429,7 +448,7 @@ 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 = 
+let 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 -> 
@@ -438,7 +457,7 @@ let merge_app c1 c2 id1 id2 shift =
     | RApp(_,f1, arr1), RApp(_,f2,arr2)  -> raise NoMerge
     | _ -> raise NoMerge
 
-let merge_app_unsafe c1 c2 shift = 
+let 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) -> 
@@ -446,11 +465,15 @@ let merge_app_unsafe c1 c2 shift =
         RApp (dummy_loc,RVar(dummy_loc,shift.ident) , args)
     | _ -> raise NoMerge
 
-let onefoud = ref false
+
 
 (* Heuristic when merging two lists of hypothesis: merge every rec
    calls of nrach 1 with all rec calls of branch 2. *)
-let rec merge_rec_hyps shift accrec (ltyp:(Names.name * Rawterm.rawconstr) list) =
+(* 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 =
   match ltyp with
     | [] -> []
     | (nme,(RApp(_,f, largs) as t)) :: lt when isVarf ind2name f -> 
@@ -459,43 +482,81 @@ let rec merge_rec_hyps shift accrec (ltyp:(Names.name * Rawterm.rawconstr) list)
           List.map 
             (fun (nme,ind) -> 
               match ind with
-                | RApp(_,i,args) -> nme, merge_app_unsafe ind t shift
+                | RApp(_,i,args) -> 
+                    nme, merge_app_unsafe ind t shift filter_shift_stable
                 | _ -> assert false)
             accrec in
-        rechyps @ merge_rec_hyps shift accrec lt
-    | e::lt -> e :: merge_rec_hyps shift accrec lt
+        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
 
-(* TODO: reecrire cette heuristique *)
+
+let find_app (nme:identifier) (ltyp: (name * rawconstr) list) = 
+  try
+    ignore
+      (List.map
+          (fun x -> 
+            match x with
+              | _,(RApp(_,f,_)) when isVarf nme f -> raise (Found 0)
+              | _ -> ())
+          ltyp);
+    false
+  with Found _ -> true
+        
 let rec merge_types shift accrec1 (ltyp1:(name * rawconstr) list)
     concl1 (ltyp2:(name * rawconstr) list) concl2
     : (name * rawconstr) list * rawconstr = 
-  let res = 
-  match ltyp1 with
-    | [] -> 
-        let _ = onefoud := false in
-        let rechyps =(*If accrec1 is empty, use conlusion instead of accrec1 
-                       to merge rec calls*)
-          merge_rec_hyps shift
-            (if accrec1<>[] then accrec1 else [name_of_string "concl1",concl1])
-            ltyp2 in
-        (* If no reccalls has been found in ltyp2 and accrec1 is not
-           empty, create one with accrec1 + concl2  *)
-        let suppl_rechyps = 
-          if accrec1 = [] || !onefoud then []
-          else build_suppl_reccall accrec1 concl2 shift in
-        rechyps @ suppl_rechyps , merge_app concl1 concl2 ind1name ind2name shift
-    | (nme,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
+  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 _ = prstr "\nltyp 2 : " in
+  let _ = List.iter (fun (nm,tp) -> prNamedRConstr (string_of_name nm) 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
+            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
+            else if isrec2
+            then merge_rec_hyps shift [name_of_string "concl1",concl1] ltyp2
+              filter_shift_stable_right
+            else [] in
+          let _ = prstr"\nrechyps : " in
+          let _ = List.iter 
+            (fun (nm,tp) -> prNamedRConstr (string_of_name nm) 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,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
   in
   res