module Explore générique et réécriture EAuto avec ce module; occur check dans clenv_merge

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

1 files changed, 117 insertions, 121 deletions

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index f325f5a863..a48f7d3c97 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -119,7 +119,7 @@ let vernac_prolog =
     gentac ((Integer n) :: (List.map (fun com -> (Constr com)) coms))
 
 let vernac_instantiate =
-  hide_tactic "Instantiate" instantiate_tac;;
+  hide_tactic "Instantiate" instantiate_tac
 
 let vernac_normevars =
   hide_atomic_tactic "NormEvars" normEvars
@@ -130,8 +130,6 @@ open Auto
 (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
 (***************************************************************************)
 
-(* A registered version of tactics in order to keep a trace *)
-
 let unify_e_resolve  (c,clenv) gls = 
   let (wc,kONT) = startWalk gls in
   let clenv' = connect_clenv wc clenv in
@@ -174,12 +172,16 @@ and e_my_find_search db_list local_db hdc concl =
 	 | Extern tacast -> Tacticals.conclPattern concl 
 	       (out_some p) tacast
        in tac)
-	 (*i fun gls -> pPNL (fmt_autotactic t); flush stdout; 
+         (*i
+	 fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); 
                      try tac gls
 		     with e when Logic.catchable_exception(e) -> 
-                            (print_string "Fail\n"; flush stdout; raise e)
-	   i*)
-  in List.map tac_of_hint hintl
+                            (Format.print_string "Fail\n"; 
+			     Format.print_flush (); 
+			     raise e)
+         i*)
+  in 
+  List.map tac_of_hint hintl
     
 and e_trivial_resolve db_list local_db gl = 
   try 
@@ -188,132 +190,126 @@ and e_trivial_resolve db_list local_db gl =
 	 (List.hd (head_constr_bound gl [])) gl)
   with Bound | Not_found -> []
 
-(***
-let vernac_e_trivial 
-   = hide_atomic_tactic "ETrivial" e_trivial_fail
-****)
-
 let e_possible_resolve db_list local_db gl =
   try List.map snd (e_my_find_search db_list local_db 
 		      (List.hd (head_constr_bound gl [])) gl)
   with Bound | Not_found -> []
 
-(* A depth-first version with correct (?) backtracking using operations on lists 
-   of goals *)
-
 let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
 
-exception Nogoals
-
 let find_first_goal gls = 
-  try first_goal gls with UserError _ -> raise Nogoals
-      
-let rec e_search_depth n db_list local_db lg =
-  try 
-    let g = find_first_goal lg in
-    if n = 0 then error "BOUND 2";
-    let assumption_tacs = 
-      List.map 
-	(fun id gls -> 
-	   then_tactic_list 
-	     (assumption_tac_list id)
-	     (e_search_depth n db_list local_db)
-	     gls)
-	(pf_ids_of_hyps g)
-    in
-    let intro_tac = 
-      apply_tac_list
-	(tclTHEN Tactics.intro 
-	   (fun g' -> 		   
-	      let hintl = make_resolve_hyp (pf_env g') (project g') 
-			    (pf_last_hyp g') in
-	      (tactic_list_tactic 
-		 (e_search_depth n db_list
-		    (Hint_db.add_list hintl local_db))) g')) 
-    in
-    let rec_tacs = 
-      List.map 
-	(fun ntac lg' -> 
-	   (then_tactic_list 
-	      (apply_tac_list ntac)
-	      (e_search_depth (n-1) db_list local_db) lg'))
-        (e_possible_resolve db_list local_db (pf_concl g)) 
-    in
-    tclFIRSTLIST (assumption_tacs @ (intro_tac :: rec_tacs)) lg
-  with Nogoals -> 
-    tclIDTAC_list lg
-
-(* Breadth-first search, a state is [(n,(lgls,val),hintl)] where 
-   [n] is the depth of search before failing
-   [lgls,val] is a non empty list of remaining goals and the current validation
-   hintl is a possible hints list to be added to the local hints database (after intro)
-   we manipulate a FILO of possible states.
-*) 
-type state = {depth : int; 
-	      tacres : goal list sigma * validation;
-              localdb :  Auto.Hint_db.t}
-
-type state_queue = state list * state list
-
-let empty_queue = ([],[])
-
-let push_state s (l1,l2) = (s::l1,l2)
-
-let decomp_states = function 
-    [],[] -> raise Not_found
-  | (l1,a::l2)->(a,(l1,l2))
-  | (l1,[])-> let l2 = List.rev l1 in (List.hd l2,([],List.tl l2))
-
-let add_state n tacr db sl = push_state {depth=n;tacres=tacr;localdb=db} sl
-
-let e_search (n,p) db_list local_db gl =
-  let state0 = add_state n (tclIDTAC gl) local_db empty_queue in
-  let rec process_state stateq =
-    let (fstate,restq) = try decomp_states stateq 
-    with Not_found -> error "BOUND 2" (* no more states *)
-    in 
-    let (glls,v) = fstate.tacres 
-    and n = fstate.depth
-    and local_db = fstate.localdb 
-    in 
-    let rec process_tacs tacl sq = 
-      match tacl with 
-	  [] -> (* no more tactics for the goal *)
-	     process_state sq (* continue with next state *)
-	| (b,tac)::tacrest ->
-            (try 
-	    let (lgls,ptl) = apply_tac_list tac glls in 
-	    let v' p = v (ptl p) in
-	    let k = List.length (sig_it lgls) in
-	      if k = 0 then (lgls,v') (* success *)
-	      else  let n' = if k < List.length (sig_it glls) or b then n else n-1 in
-		   let hintl = (* possible new hint list for assumptions *)
-		     if b then (* intro tactic *)
-		       let g' = first_goal lgls in 
-			 make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
-		     else []
-                   in let ldb = Hint_db.add_list hintl local_db
-		   in if n'=0 then 
-		     try 
-		       let (lgls1,ptl1) = e_search_depth p db_list ldb lgls 
-		       in let v1 p = v' (ptl1 p) in (lgls1,v1)
-		     with e when Logic.catchable_exception e -> process_tacs tacrest sq
-		     else let sq' = add_state n' (lgls, v') ldb sq
-		   in process_tacs tacrest sq'
-	     with e when Logic.catchable_exception e -> process_tacs tacrest sq)
-    in let g = first_goal glls in 
-    let tac1 = List.map (fun id -> (false, e_give_exact_constr (mkVar id))) (pf_ids_of_hyps g)
-    and tac2 = (true,Tactics.intro)
-    and tac3 = List.map (fun tac -> (false,tac)) 
-		 (e_possible_resolve db_list local_db (pf_concl g))
-    in process_tacs (tac1@tac2::tac3) restq
- in process_state state0
+  try first_goal gls with UserError _ -> assert false
 
+(*s The following module [SearchProblem] is used to instantiate the generic
+    exploration functor [Explore.Make]. *)
+      
+module SearchProblem = struct
+
+  type state = { 
+    depth : int; (*r depth of search before failing *)
+    tacres : goal list sigma * validation;
+    dblist : Auto.Hint_db.t list;
+    localdb :  Auto.Hint_db.t list }
+		 
+  let success s = (sig_it (fst s.tacres)) = []
+
+  let rec filter_tactics (glls,v) = function
+    | [] -> []
+    | tac :: tacl -> 
+	try 
+	  let (lgls,ptl) = apply_tac_list tac glls in 
+	  let v' p = v (ptl p) in
+	  (lgls,v') :: filter_tactics (glls,v) tacl
+	with e when Logic.catchable_exception e ->
+	  filter_tactics (glls,v) tacl
+
+  let rec list_addn n x l = 
+    if n = 0 then l else x :: (list_addn (pred n) x l)
+
+  let compare s s' =
+    let d = s.depth - s'.depth in
+    let nbgoals s = List.length (sig_it (fst s.tacres)) in
+    if d <> 0 then d else nbgoals s - nbgoals s'
+
+  let branching s = 
+    if s.depth = 0 then 
+      []
+    else      
+      let lg = fst s.tacres in
+      let nbgl = List.length (sig_it lg) in
+      assert (nbgl > 0);
+      let g = find_first_goal lg in
+      let assumption_tacs = 
+	let l = 
+	  filter_tactics s.tacres
+	    (List.map (fun id -> e_give_exact_constr (mkVar id)) 
+	       (pf_ids_of_hyps g))
+	in
+	List.map (fun res -> { depth = s.depth; tacres = res;
+			       dblist = s.dblist;
+			       localdb = List.tl s.localdb }) l
+      in
+      let intro_tac = 
+	List.map 
+	  (fun ((lgls,_) as res) -> 
+	     let g' = first_goal lgls in 
+	     let hintl = 
+	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
+	     in
+             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
+	     { depth = s.depth; tacres = res; dblist = s.dblist;
+	       localdb = ldb :: List.tl s.localdb })
+	  (filter_tactics s.tacres [Tactics.intro])
+      in
+      let rec_tacs = 
+	let l = 
+	  filter_tactics s.tacres
+	    (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
+	in
+	List.map 
+	  (fun ((lgls,_) as res) -> 
+	     let nbgl' = List.length (sig_it lgls) in
+	     if nbgl' < nbgl then
+	       { depth = s.depth; tacres = res; 
+		 dblist = s.dblist; localdb = List.tl s.localdb }
+	     else 
+	       { depth = pred s.depth; tacres = res; dblist = s.dblist;
+		 localdb = 
+		   list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
+	  l
+      in
+      List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
+
+  let pp s = Format.printf "(depth=%d)\n" s.depth; Format.print_flush ()
+
+end
+
+module Search = Explore.Make(SearchProblem)
+
+let make_initial_state n gl dblist localdb =
+  { SearchProblem.depth = n;
+    SearchProblem.tacres = tclIDTAC gl;
+    SearchProblem.dblist = dblist;
+    SearchProblem.localdb = [localdb] }
+
+let e_depth_search p db_list local_db gl =
+  try
+    let s = Search.depth_first (make_initial_state p gl db_list local_db) in
+    s.SearchProblem.tacres
+  with Not_found -> error "EAuto: depth first search failed"
+
+let e_breadth_search (n,_) db_list local_db gl =
+  try
+    let s = Search.breadth_first (make_initial_state n gl db_list local_db) in
+    s.SearchProblem.tacres
+  with Not_found -> error "EAuto: breadth first search failed"
 
 let e_search_auto (n,p) db_list gl = 
   let local_db = make_local_hint_db gl in 
-    if n = 0 then tactic_list_tactic (e_search_depth p db_list local_db) gl
-    else e_search (n,p) db_list local_db gl
+  if n = 0 then 
+    e_depth_search p db_list local_db gl
+  else 
+    e_breadth_search (n,p) db_list local_db gl
 
 let eauto np dbnames = 
   let db_list =