Improvements in typeclasses eauto and generalized rewriting:

- Decorate proof search with depth/subgoal number information
- Add a tactic [autoapply foo using hints] to call the resolution tactic
with the [transparent_state] associated with a hint db, giving better
control over unfolding.
- Fix a bug in the Lambda case in the new rewrite
- More work on the [Proper] and [subrelation] hints to cut the search space
while retaining completeness.


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

2 files changed, 37 insertions, 15 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 222efb54e..890f3a086 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -205,7 +205,9 @@ let typeclasses_debug = ref false
 
 type validation = evar_map -> proof_tree list -> proof_tree
 
-type autoinfo = { hints : Auto.hint_db; auto_depth: int; auto_last_tac: std_ppcmds }
+let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l)
+
+type autoinfo = { hints : Auto.hint_db; auto_depth: int list; auto_last_tac: std_ppcmds }
 type autogoal = goal * autoinfo
 type 'ans fk = unit -> 'ans
 type ('a,'ans) sk = 'a -> 'ans fk -> 'ans
@@ -254,34 +256,38 @@ let solve_tac (x : 'a tac) : 'a tac =
       
 let hints_tac hints = 
   { skft = fun sk fk {it = gl,info; sigma = s} ->
-    if !typeclasses_debug then msgnl (str"depth=" ++ int info.auto_depth ++ str": " ++ info.auto_last_tac
-					 ++ spc () ++ str "->" ++ spc () ++ pr_ev s gl);
+(*     if !typeclasses_debug then msgnl (str"depth=" ++ int info.auto_depth ++ str": " ++ info.auto_last_tac *)
+(* 					 ++ spc () ++ str "->" ++ spc () ++ pr_ev s gl); *)
     let possible_resolve ((lgls,v) as res, pri, pp) =
       (pri, pp, res)
     in
     let tacs =
-      let poss = e_possible_resolve hints info.hints (Evarutil.nf_evar s gl.evar_concl) in
+      let concl = Evarutil.nf_evar s gl.evar_concl in
+      let poss = e_possible_resolve hints info.hints concl in
       let l =
 	Util.list_map_append (fun (tac, pri, pptac) ->
 	  try [tac {it = gl; sigma = s}, pri, pptac] with e when catchable e -> [])
 	  poss
       in
+	if l = [] && !typeclasses_debug then
+	  msgnl (pr_depth info.auto_depth ++ str": no match for " ++ 
+		    Printer.pr_constr_env (Evd.evar_env gl) concl ++ int (List.length poss) ++ str" possibilities");
 	List.map possible_resolve l
     in
     let tacs = List.sort compare tacs in
-    let info = { info with auto_depth = succ info.auto_depth } in
-    let rec aux = function
+    let rec aux i = function
       | (_, pp, ({it = gls; sigma = s}, v)) :: tl ->
-	  if !typeclasses_debug then msgnl (str"depth=" ++ int info.auto_depth ++ str": " ++ pp
-					       ++ spc () ++ str"succeeded on" ++ spc () ++ pr_ev s gl);
+	  if !typeclasses_debug then msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ pp
+					       ++ str" on" ++ spc () ++ pr_ev s gl);
 	  let fk =
-	    (fun () -> if !typeclasses_debug then msgnl (str"backtracked after " ++ pp ++ spc () ++ str"failed");
-	    aux tl) 
+	    (fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *)
+	    aux (succ i) tl) 
 	  in
-	  let glsv = {it = List.map (fun g -> g, { info with auto_last_tac = pp }) gls; sigma = s}, fun _ -> v in
+	  let glsv = {it = list_map_i (fun j g -> g, 
+	    { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp }) 1 gls; sigma = s}, fun _ -> v in
 	    sk glsv fk
       | [] -> fk ()
-    in aux tacs }
+    in aux 1 tacs }
     
 let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
   let rec aux s (acc : (autogoal list * validation) list) fk = function
@@ -344,10 +350,12 @@ let make_autogoal ?(st=full_transparent_state) g =
   let sign = pf_hyps g in
   let hintlist = list_map_append (pf_apply make_resolve_hyp g st (true,false,false) None) sign in
   let hints = Hint_db.add_list hintlist (Hint_db.empty st true) in
-    (g.it, { hints = hints ; auto_depth = 0; auto_last_tac = mt() })
+    (g.it, { hints = hints ; auto_depth = []; auto_last_tac = mt() })
       
 let make_autogoals ?(st=full_transparent_state) gs evm' =
-  { it = List.map (fun g -> make_autogoal ~st {it = snd g; sigma = evm'}) gs; sigma = evm' }
+  { it = list_map_i (fun i g -> 
+    let (gl, auto) = make_autogoal ~st {it = snd g; sigma = evm'} in
+      (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
     
 let run_on_evars ?(st=full_transparent_state) p evm tac =
   match evars_to_goals p evm with
@@ -642,3 +650,17 @@ TACTIC EXTEND not_evar
     | Evar _ -> tclFAIL 0 (str"Evar")
     | _ -> tclIDTAC ]
 END
+
+TACTIC EXTEND is_ground
+  [ "is_ground" constr(ty) ] -> [ fun gl ->
+    if Evarutil.is_ground_term (project gl) ty then tclIDTAC gl
+    else tclFAIL 0 (str"Not ground") gl ]
+END
+
+TACTIC EXTEND autoapply
+  [ "autoapply" constr(c) "using" preident(i) ] -> [ fun gl ->
+    let flags = flags_of_state (Auto.Hint_db.transparent_state (Auto.searchtable_map i)) in
+    let cty = pf_type_of gl c in
+    let ce = mk_clenv_from gl (c,cty) in
+      unify_e_resolve flags (c,ce) gl ]
+END
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 216beab54..213f0d11e 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -581,7 +581,7 @@ let subterm all flags (s : strategy) : strategy =
 	      
       | Lambda (n, t, b) when flags.under_lambdas ->
 	  let env' = Environ.push_rel (n, None, t) env in
-	  let b' = aux env' sigma b (Typing.type_of env' sigma b) (unlift_cstr env sigma cstr) evars in
+	  let b' = s env' sigma b (Typing.type_of env' sigma b) (unlift_cstr env sigma cstr) evars in
 	    (match b' with
 	    | Some (Some r) ->
 		Some (Some { r with