1 files changed, 123 insertions, 11 deletions

diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 00b5f28c..26a1066c 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -103,10 +103,28 @@ TACTIC EXTEND snewfunind
 END
 
 
+let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_coma prc
+
+ARGUMENT EXTEND constr_coma_sequence'
+  TYPED AS constr_list
+  PRINTED BY pr_constr_coma_sequence
+| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ]
+| [ constr(c) ] -> [ [c] ]
+END
+
+let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
+
+ARGUMENT EXTEND auto_using'
+  TYPED AS constr_list
+  PRINTED BY pr_auto_using
+| [ "using" constr_coma_sequence'(l) ] -> [ l ]
+| [ ] -> [ [] ]
+END
+
 VERNAC ARGUMENT EXTEND rec_annotation2
   [ "{"  "struct" ident(id)  "}"] -> [ Struct id ]
-| [ "{" "wf" constr(r) ident_opt(id) "}" ] -> [ Wf(r,id) ]
-| [ "{" "measure" constr(r) ident_opt(id) "}" ] -> [ Mes(r,id) ] 
+| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ]
+| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ] 
 END
 
 
@@ -131,8 +149,8 @@ VERNAC ARGUMENT EXTEND rec_definition2
      let check_exists_args an =
        try 
 	 let id = match an with 
-	   | Struct id -> id | Wf(_,Some id) -> id | Mes(_,Some id) -> id 
-	   | Wf(_,None) | Mes(_,None) -> failwith "check_exists_args" 
+	   | Struct id -> id | Wf(_,Some id,_) -> id | Mes(_,Some id,_) -> id 
+	   | Wf(_,None,_) | Mes(_,None,_) -> failwith "check_exists_args" 
 	 in 
 	 (try ignore(Util.list_index (Name id) names - 1); annot
 	  with Not_found ->  Util.user_err_loc
@@ -214,11 +232,17 @@ END
 (* FINDUCTION *)
 
 (* 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 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 "");
+  end
 
 
 
@@ -266,6 +290,55 @@ let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
     max_rel = max_rel; onlyvars = List.for_all isVar args } 
     ::subres
 
+let mkEq typ c1 c2 = 
+  mkApp (Coqlib.build_coq_eq(),[| typ; c1; c2|])
+
+
+let poseq_unsafe idunsafe cstr gl =
+  let typ = Tacmach.pf_type_of gl cstr in
+  tclTHEN
+    (Tactics.letin_tac true (Name idunsafe) cstr allClauses)
+    (tclTHENFIRST 
+      (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr)) 
+      Tactics.reflexivity)
+    gl
+  
+
+let poseq id cstr gl =
+  let x = Tactics.fresh_id [] id gl in
+  poseq_unsafe x cstr gl
+
+(* dirty? *)
+
+let list_constr_largs = ref []
+
+let rec poseq_list_ids_rec lcstr gl =
+  match lcstr with
+    | [] -> tclIDTAC gl
+    | c::lcstr' -> 
+	match kind_of_term c with
+	  | Var _ -> 
+	      (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl)
+	  | _ -> 
+	      let _ = prstr "c = " in
+	      let _ = prconstr c in
+	      let _ = prstr "\n" in
+	      let typ = Tacmach.pf_type_of gl c in
+	      let cname = Termops.id_of_name_using_hdchar (Global.env()) typ Anonymous in
+	      let x = Tactics.fresh_id [] cname gl in
+	      let _ = list_constr_largs:=mkVar x :: !list_constr_largs in
+	      let _ = prstr " list_constr_largs = " in
+	      let _ = prlistconstr !list_constr_largs in
+	      let _ = prstr "\n" in
+
+	      tclTHEN
+		(poseq_unsafe x c)
+		(poseq_list_ids_rec lcstr')
+		gl
+
+let poseq_list_ids lcstr gl = 
+  let _ = list_constr_largs := [] in
+  poseq_list_ids_rec lcstr gl
 
 (** [find_fapp test g] returns the list of [app_info] of all calls to
     functions that satisfy [test] in the conclusion of goal g. Trivial
@@ -296,11 +369,17 @@ let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info l
   if List.length ordered_info_list = 0 then Util.error "function not found in goal\n";
   let taclist: Proof_type.tactic list = 
     List.map 
-      (fun info -> 
-	(tclTHEN 
-	  (functional_induction true (applist (info.fname, info.largs)) 
-	    None IntroAnonymous) 
+      (fun info ->
+	(tclTHEN
+	  (tclTHEN (poseq_list_ids info.largs)
+	    (
+	      fun gl -> 
+		  (functional_induction 
+		    true (applist (info.fname, List.rev !list_constr_largs)) 
+		    None IntroAnonymous) gl)) 
 	  nexttac)) ordered_info_list in
+  (* we try each (f t u v) until one does not fail *)
+  (* TODO: try also to mix functional schemes *)
   tclFIRST taclist g
 
 
@@ -313,9 +392,8 @@ let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list =
   match oi with
     | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *)
     | None -> 
-	(* Default heuristic: keep only occurrence where all arguments
+	(* Default heuristic: put first occurrences where all arguments
 	   are *bound* (meaning already introduced) variables *)
-	(* TODO: put other funcalls at the end instead of deleting them *)
 	let ordering x y =
 	  if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *)
 	  else if x.free && x.onlyvars then -1
@@ -325,6 +403,7 @@ let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list =
 	List.sort ordering
 
 
+
 TACTIC EXTEND finduction
     ["finduction" ident(id) natural_opt(oi)] -> 
       [ 
@@ -353,3 +432,36 @@ TACTIC EXTEND fauto
 
 END
 
+
+TACTIC EXTEND poseq
+  [ "poseq" ident(x) constr(c) ] -> 
+      [ poseq x c ]
+END
+
+VERNAC COMMAND EXTEND Showindinfo
+  [ "showindinfo" ident(x) ] -> [ Merge.showind x ]
+END
+
+VERNAC COMMAND EXTEND MergeFunind
+  [ "Mergeschemes" lconstr(c) "with" lconstr(c') "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)
+     ]
+END