Cleaning code and comment.

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

1 files changed, 30 insertions, 33 deletions

diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index 5e894e47f..cf6246704 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -207,7 +207,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 =
     {
@@ -252,7 +252,7 @@ type 'a merged_arg =
     | Arg_funres
 
 (** Information about graph merging of two inductives. 
-   All rel_decl list are IN INVERSE ORDER (ie well suited for compose) *)
+   All rel_decl list are IN REVERSE ORDER (ie well suited for compose) *)
 
 type merge_infos =
     {
@@ -549,7 +549,7 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
 
 
 (* 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 rec merge_rec_hyps shift accrec 
     (ltyp:(Names.name * rawconstr option * rawconstr option) list) 
@@ -602,7 +602,6 @@ let rec merge_types shift accrec1
   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
       | [] -> 
@@ -618,24 +617,21 @@ let rec merge_types shift accrec1
             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
+              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 _ = 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
@@ -696,7 +692,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: 
@@ -738,7 +734,7 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr)
     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 = 
+  let typwithprms =
     raw_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in
   typwithprms
 
@@ -912,28 +908,29 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   Command.build_mutual [(indexpr,None)] true (* means: not coinductive *)
 
 
-let kn_of_id id =
-  let f_ref = Libnames.Ident (dummy_loc,id) in
-  locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref)
-    locate_constant
-    f_ref
-
+(* 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 =
-  let kn1 = kn_of_id id1 in
-  let kn2 = kn_of_id id2 in
-  let finfo1 = 
-    try find_Function_infos kn1 
-    with Not_found ->
-      errorlabstrm "indfun" (Nameops.pr_id id1 ++ str " has no functional scheme") in
-  let finfo2 = 
-    try find_Function_infos kn2 
-    with Not_found -> 
-      errorlabstrm "indfun" (Nameops.pr_id id2 ++ str " has no functional scheme") in
-  let ind1 = finfo1.graph_ind in
-  let ind2 = finfo2.graph_ind in
-  (* args1 are unlinked. FIXME? mergescheme (G x x) ?? *)
+    (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 
@@ -949,7 +946,7 @@ let merge (id1:identifier) (id2:identifier) (args1:identifier array)
   (* setting functional results *)
   let _ = lnk1.(Array.length lnk1 - 1) <- Funres in 
   let _ = lnk2.(Array.length lnk2 - 1) <- Funres in
-  merge_inductive ind1 ind2 lnk1 lnk2 id
+  merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id