Better use of transparency information for local hypotheses:

- make hyps rigid in the dnet if they're not let-ins
- use existing typeclass-related transparency information for the new
hints.
Make the dnet better by indexing products, lambdas and sorts too.


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

8 files changed, 73 insertions, 29 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e70279a8d9..684f1dde2a 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -658,6 +658,9 @@ let print_applicable_hint () =
 let print_hint_db db =
   let (ids, csts) = Hint_db.transparent_state db in
   msg (hov 0
+	  ((if Hint_db.use_dn db then str"Discriminated database" 
+	    else str"Non-discriminated database") ++ fnl ()));
+  msg (hov 0
 	  (str"Unfoldable variable definitions: " ++ pr_idpred ids ++ fnl () ++
 	   str"Unfoldable constant definitions: " ++ pr_cpred csts ++ fnl ()));
   Hint_db.iter
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 007a116d19..1910bd139d 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -104,6 +104,8 @@ val print_hint_ref : global_reference -> unit
 
 val print_hint_db_by_name : hint_db_name -> unit
 
+val print_hint_db : Hint_db.t -> unit
+
 (* [make_exact_entry pri (c, ctyp)].
    [c] is the term given as an exact proof to solve the goal;
    [ctyp] is the type of [c]. *)
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index b409fc9b8d..e28a9e3c35 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -54,7 +54,7 @@ let bounded_constr_val_discr (t,depth) =
       | Dn.Nothing -> Dn.Nothing
       | Dn.Everything -> Dn.Everything
 
-type 'a t = (global_reference,constr_pattern * int,'a) Dn.t
+type 'a t = (term_label,constr_pattern * int,'a) Dn.t
 
 let create = Dn.create
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index be8b0fb805..6d1c916348 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -46,6 +46,8 @@ let typeclasses_db = "typeclass_instances"
 let _ = Auto.auto_init := (fun () ->
   Auto.create_hint_db false typeclasses_db full_transparent_state true)
 
+let run_on_evars_forward = ref (fun _ _ _ _ -> assert false)
+
 exception Found of evar_map
 
 let is_dependent ev evm =
@@ -80,7 +82,7 @@ let evars_to_goals p evm =
     else
       let goals = List.rev goals in
 	Some (goals, evm')
-
+	  
 (** Typeclasses instance search tactic / eauto *)
 
 let intersects s t =
@@ -107,6 +109,12 @@ let auto_unif_flags = {
   use_evars_pattern_unification = true;
 }
 
+let tac_on_evars p tac gl =
+  let db = searchtable_map typeclasses_db in
+    match !run_on_evars_forward [db] (Hint_db.transparent_state db) p (project gl)  with
+    | None -> tclIDTAC gl
+    | Some evm' -> Refiner.tclEVARS evm' gl
+
 let unify_e_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
   let clenv' = clenv_unique_resolver false ~flags clenv' gls in
@@ -273,7 +281,8 @@ let hints_tac hints =
       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");
+		    Printer.pr_constr_env (Evd.evar_env gl) concl ++ 
+		    spc () ++ int (List.length poss) ++ str" possibilities");
 	List.map possible_resolve l
     in
     let tacs = List.sort compare tacs in
@@ -354,6 +363,10 @@ let make_resolve_hyp env sigma st flags pri (id, _, cty) =
 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 st = List.fold_left (fun (ids, csts) (n, b, t) ->
+    (if b <> None then Idpred.add else Idpred.remove) n ids, csts)
+    st sign
+  in
   let hints = Hint_db.add_list hintlist (Hint_db.empty st true) in
     (g.it, { hints = hints ; auto_depth = []; auto_last_tac = mt() })
 
@@ -373,18 +386,21 @@ let run_on_evars ?(st=full_transparent_state) p evm tac =
 	  with Found evm' ->
 	    Some (Evd.evars_reset_evd evm' evm)
 
+
+let eauto_tac hints = fix (or_tac intro_tac (hints_tac hints)) 
+
+let () = run_on_evars_forward := (fun hints st p evd -> run_on_evars ~st p evd (eauto_tac hints))
+  
 let eauto hints g =
-  let tac = fix (or_tac intro_tac (hints_tac hints)) in
-  let gl = { it = make_autogoal g; sigma = project g } in
-    match run_tac tac gl with
+  let gl = { it = make_autogoal ~st:(Hint_db.transparent_state (List.hd hints)) g; sigma = project g } in
+    match run_tac (eauto_tac hints) gl with
     | None -> raise Not_found
     | Some ({it = goals; sigma = s}, valid) ->
 	{it = List.map fst goals; sigma = s}, valid s
 
 let real_eauto st hints p evd =
-  let tac = fix (or_tac intro_tac (hints_tac hints)) in
   let rec aux evd =
-    match run_on_evars ~st p evd tac with
+    match run_on_evars ~st p evd (eauto_tac hints) with
     | None -> evd
     | Some evd' -> aux evd'
   in aux evd
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 4e72d07080..3fd5236a81 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -29,11 +29,11 @@ open Libnames
 
 type ('na,'a) t = {
   mutable table : ('na,constr_pattern * 'a) Gmap.t;
-  mutable patterns : (global_reference option,'a Btermdn.t) Gmap.t }
+  mutable patterns : (Termdn.term_label option,'a Btermdn.t) Gmap.t }
 
 type ('na,'a) frozen_t =
     ('na,constr_pattern * 'a) Gmap.t
-    * (global_reference option,'a Btermdn.t) Gmap.t
+    * (Termdn.term_label option,'a Btermdn.t) Gmap.t
 
 let create () =
   { table = Gmap.empty;
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 350b53df71..e8279b76f4 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -35,4 +35,4 @@ val freeze : ('na,'a) t -> ('na,'a) frozen_t
 val unfreeze : ('na,'a) frozen_t -> ('na,'a) t -> unit
 val empty : ('na,'a) t -> unit
 val to2lists : ('na,'a) t -> ('na * (constr_pattern * 'a)) list *
-                             (global_reference option * 'a Btermdn.t) list
+                             (Termdn.term_label option * 'a Btermdn.t) list
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 32e65239dd..21806269af 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -21,7 +21,13 @@ open Nametab
    See the module dn.ml for further explanations.
    Eduardo (5/8/97) *)
 
-type 'a t = (global_reference,constr_pattern,'a) Dn.t
+type term_label = 
+  | GRLabel of global_reference
+  | ProdLabel 
+  | LambdaLabel
+  | SortLabel of sorts option
+
+type 'a t = (term_label,constr_pattern,'a) Dn.t
 
 (*If we have: f a b c ..., decomp gives: (f,[a;b;c;...])*)
 
@@ -46,20 +52,28 @@ let constr_pat_discr t =
   else
     match decomp_pat t with
     | PRef ((IndRef _) as ref), args
-    | PRef ((ConstructRef _ ) as ref), args -> Some (ref,args)
-    | PRef ((VarRef v) as ref), args -> Some(ref,args)
+    | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
+    | PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args)
     | _ -> None
 
 let constr_pat_discr_st (idpred,cpred) t =
   match decomp_pat t with
   | PRef ((IndRef _) as ref), args
-  | PRef ((ConstructRef _ ) as ref), args -> Some (ref,args)
+  | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
   | PRef ((VarRef v) as ref), args when not (Idpred.mem v idpred) ->
-      Some(ref,args)
+      Some(GRLabel ref,args)
   | PVar v, args when not (Idpred.mem v idpred) ->
-      Some(VarRef v,args)
+      Some(GRLabel (VarRef v),args)
   | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) ->
-      Some (ref, args)
+      Some (GRLabel ref, args)
+  | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c])
+  | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l)
+  | PSort s, [] -> 
+      let s' = match s with
+	| RProp c -> Some (Prop c)
+	| RType (Some c) -> Some (Type c)
+	| RType None -> None
+      in Some (SortLabel s', [])
   | _ -> None
 
 open Dn
@@ -67,19 +81,22 @@ open Dn
 let constr_val_discr t =
   let c, l = decomp t in
     match kind_of_term c with
-    | Ind ind_sp -> Label(IndRef ind_sp,l)
-    | Construct cstr_sp -> Label((ConstructRef cstr_sp),l)
-    | Var id -> Label(VarRef id,l)
+    | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l)
+    | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l)
+    | Var id -> Label(GRLabel (VarRef id),l)
     | Const _ -> Everything
     | _ -> Nothing
 
 let constr_val_discr_st (idpred,cpred) t =
   let c, l = decomp t in
     match kind_of_term c with
-    | Const c -> if Cpred.mem c cpred then Everything else Label(ConstRef c,l)
-    | Ind ind_sp -> Label(IndRef ind_sp,l)
-    | Construct cstr_sp -> Label((ConstructRef cstr_sp),l)
-    | Var id when not (Idpred.mem id idpred) -> Label(VarRef id,l)
+    | Const c -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l)
+    | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l)
+    | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l)
+    | Var id when not (Idpred.mem id idpred) -> Label(GRLabel (VarRef id),l)
+    | Prod (n, d, c) -> Label(ProdLabel, [d; c])
+    | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l)
+    | Sort s -> Label(SortLabel (Some s), [])
     | Evar _ -> Everything
     | _ -> Nothing
 
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 92a1b8c3ea..f3743b1280 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -48,12 +48,18 @@ val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit
 (*i*)
 (* These are for Nbtermdn *)
 
+type term_label = 
+  | GRLabel of global_reference
+  | ProdLabel 
+  | LambdaLabel
+  | SortLabel of sorts option
+
 val constr_pat_discr_st : transparent_state ->
-  constr_pattern -> (global_reference * constr_pattern list) option
+  constr_pattern -> (term_label * constr_pattern list) option
 val constr_val_discr_st : transparent_state ->
-  constr -> (global_reference * constr list) Dn.lookup_res
+  constr -> (term_label * constr list) Dn.lookup_res
 
-val constr_pat_discr : constr_pattern -> (global_reference * constr_pattern list) option
-val constr_val_discr : constr -> (global_reference * constr list) Dn.lookup_res
+val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option
+val constr_val_discr : constr -> (term_label * constr list) Dn.lookup_res
 
 (*i*)