Changing merging functional scheme syntax.

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

2 files changed, 30 insertions, 26 deletions

diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 26a1066c0..afc78fec0 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -443,25 +443,13 @@ VERNAC COMMAND EXTEND Showindinfo
 END
 
 VERNAC COMMAND EXTEND MergeFunind
-  [ "Mergeschemes" lconstr(c) "with" lconstr(c') "using" ident(id) ] -> 
+  [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")" 
+      "with" "(" ident(id2) ne_ident_list(cl2)  ")" "using" ident(id) ] -> 
      [ 
-       let c1 = Constrintern.interp_constr Evd.empty (Global.env()) c in
-       let c2 = Constrintern.interp_constr Evd.empty (Global.env()) c' in
-       let id1,args1 = 
-	 try 
-	   let hd,args = destApp c1 in
-	   if Term.isInd hd then hd , args 
-	   else raise (Util.error "Ill-formed (fst) argument")
-	 with Invalid_argument _ 
-	     -> Util.error ("Bad argument form for merging schemes") in
-       let id2,args2 = 
-	 try
- 	   let hd,args = destApp c2 in
-	   if isInd hd then hd , args 
-	   else raise (Util.error "Ill-formed (snd) argument")
-	 with Invalid_argument _ 
-	     -> Util.error ("Bad argument form for merging schemes") in
-       (* TOFO: enlever le ignore et declarer l'inductif *)
-       ignore(Merge.merge c1 c2 args1 args2 id)
+       let _ = Constrintern.interp_constr Evd.empty (Global.env()) 
+	 (CRef (Libnames.Ident (Util.dummy_loc,id1))) in
+       let _ = Constrintern.interp_constr Evd.empty (Global.env())
+	 (CRef (Libnames.Ident (Util.dummy_loc,id2)))in
+       Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2)  id
      ]
 END
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index 5ec600a47..376e6e5f5 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -10,6 +10,7 @@
 
 (*i $Id: i*)
 
+open Indfun_common
 open Util
 open Topconstr
 open Vernacexpr
@@ -78,7 +79,7 @@ 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)
 let prconstrnl c =  msg (str"  " ++ Printer.pr_lconstr c ++ str"\n")
@@ -797,11 +798,26 @@ 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 (Libnames.pr_reference f_ref ++ str ": Not found!")
+    locate_constant
+    f_ref
 
-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 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 " unknown") in
+  let finfo2 = 
+    try find_Function_infos kn2 
+    with Not_found -> errorlabstrm "indfun" (Nameops.pr_id id2 ++ str " unknown") in
+  let ind1 = finfo1.graph_ind in
+  let ind2 = finfo2.graph_ind 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 *)
@@ -814,8 +830,8 @@ let merge (cstr1:constr) (cstr2:constr) (args1:constr array) (args2:constr array
           | 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
+  let _ = merge_inductive ind1 ind2 lnk1 lnk2 id in
+  ()