Ajout de tactiques expérimentales basée sur functional induction.

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

1 files changed, 148 insertions, 0 deletions

diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 5ba05a8e9b..cb51069dfc 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -14,6 +14,7 @@ open Indfun_common
 open Indfun
 open Genarg
 open Pcoq
+open Tacticals
 
 let pr_binding prc = function
   | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
@@ -198,3 +199,150 @@ END
 VERNAC COMMAND EXTEND GenerateGraph 
 ["Generate" "graph" "for" ident(c)] -> [ make_graph c ]
 END
+
+
+
+
+
+(* FINDUCTION *)
+
+(* comment this line to see debug msgs *)
+(* 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)
+
+
+
+(** Information about an occurrence of a function call (application)
+    inside a term. *)
+type fapp_info = {
+  fname: constr; (** The function applied *)
+  largs: constr list; (** List of arguments *)
+  free: bool; (** [true] if all arguments are debruijn free *)
+  max_rel: int; (** max debruijn index in the funcall *)
+  onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *)
+}
+
+
+(** [constr_head_match(a b c) a] returns true, false otherwise. *)
+let constr_head_match u t=
+  if isApp u 
+  then 
+    let uhd,args= destApp u in
+    uhd=t
+  else false
+
+(** [hdMatchSub inu t] returns the list of occurrences of [t] in
+    [inu]. DeBruijn are not pushed, so some of them may be unbound in
+    the result. *)
+let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
+  let subres = 
+    match kind_of_term inu with
+      | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> 
+	  hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test
+      | Fix (_,(lna,tl,bl))  -> (* not sure Fix is correct *)
+	  Array.fold_left 
+	    (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test) 
+	    [] bl
+      | _ -> (* Cofix will be wrong *)
+	  fold_constr 
+	    (fun l cstr -> 
+	      l @ hdMatchSub cstr test) [] inu in 
+  if not (test inu) then subres
+  else
+    let f,args = decompose_app inu in
+    let freeset = Termops.free_rels inu in
+    let max_rel = try Util.Intset.max_elt freeset with Not_found -> -1 in
+    {fname = f; largs = args; free = Util.Intset.is_empty freeset;
+    max_rel = max_rel; onlyvars = List.for_all isVar args } 
+    ::subres
+
+
+(** [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
+    repetition (not modulo conversion) are deleted. *)
+let find_fapp (test:constr -> bool) g : fapp_info list = 
+  let pre_res = hdMatchSub (Tacmach.pf_concl g) test in
+  let res = 
+    List.fold_right (fun x acc -> if List.mem x acc then acc else x::acc) pre_res [] in
+  (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res);
+  res)
+
+
+
+(** [finduction id filter g] tries to apply functional induction on
+    an occurence of function [id] in the conclusion of goal [g]. If
+    [id]=[None] then calls to any function are selected. In any case
+    [heuristic] is used to select the most pertinent occurrence. *)
+let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info list)
+    (nexttac:Proof_type.tactic) g =
+  let test = match oid with
+    | Some id -> 
+	let idconstr = mkConst (const_of_id id) in
+	(fun u -> constr_head_match u idconstr) (* select only id *)
+    | None -> (fun u -> isApp u) in (* select calls to any function *)
+  let info_list = find_fapp test g in
+  let ordered_info_list = heuristic info_list in
+  prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list); 
+  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) 
+	  nexttac)) ordered_info_list in
+  tclFIRST taclist g
+
+
+
+
+(** [chose_heuristic oi x] returns the heuristic for reordering
+    (and/or forgetting some elts of) a list of occurrences of
+     function calls infos to chose first with functional induction. *)
+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
+	   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
+	  else if y.free && y.onlyvars then 1
+	  else 0 (* both not pertinent *)
+	in
+	List.sort ordering
+
+
+TACTIC EXTEND finduction
+    ["finduction" ident(id) natural_opt(oi)] -> 
+      [ 
+	match oi with
+	  | Some(n) when n<=0 -> Util.error "numerical argument must be > 0"
+	  | _ -> 
+	      let heuristic = chose_heuristic oi in
+	      finduction (Some id) heuristic tclIDTAC
+      ]
+END
+
+
+
+TACTIC EXTEND fauto
+    [ "fauto" tactic(tac)] -> 
+      [
+	let heuristic = chose_heuristic None in
+	finduction None heuristic (snd tac)
+      ]
+  |
+    [ "fauto" ] -> 
+      [
+	let heuristic = chose_heuristic None in
+	finduction None heuristic tclIDTAC
+      ]
+
+END
+