Enhanced discrimination nets implementation, which can now work with

goals containing existentials and use transparency information on
constants (optionally). Only used by the typeclasses eauto engine for
now, but could be used for other hint bases easily (just switch a boolean).
Had to add a new "creation" hint to be able to set said boolean upon
creation of the typeclass_instances hint db.
Improve the proof-search algorithm for Morphism, up to 10 seconds
gained in e.g. Field_theory, Ring_polynom. Added a morphism
declaration for [compose].
One needs to declare more constants as being unfoldable using
the [Typeclasses unfold] command so that discrimination is done correctly, but
that amounts to only 6 declarations in the standard library.


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

1 files changed, 49 insertions, 11 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 7d41ebf9d..2412968a1 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -9,6 +9,7 @@
 (* $Id$ *)
 
 open Term
+open Names
 open Termdn
 open Pattern
 open Libnames
@@ -19,6 +20,23 @@ open Libnames
 
 let dnet_depth = ref 8
 		   
+let bounded_constr_pat_discr_st st (t,depth) =
+  if depth = 0 then 
+    None 
+  else
+    match constr_pat_discr_st st t with
+      | None -> None
+      | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
+	    
+let bounded_constr_val_discr_st st (t,depth) =
+  if depth = 0 then 
+    Dn.Nothing 
+  else
+    match constr_val_discr_st st t with
+      | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l)
+      | Dn.Nothing -> Dn.Nothing
+      | Dn.Everything -> Dn.Everything
+
 let bounded_constr_pat_discr (t,depth) =
   if depth = 0 then 
     None 
@@ -29,24 +47,44 @@ let bounded_constr_pat_discr (t,depth) =
 	    
 let bounded_constr_val_discr (t,depth) =
   if depth = 0 then 
-    None 
+    Dn.Nothing 
   else
     match constr_val_discr t with
-      | None -> None
-      | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
+      | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l)
+      | Dn.Nothing -> Dn.Nothing
+      | Dn.Everything -> Dn.Nothing
 
 type 'a t = (global_reference,constr_pattern * int,'a) Dn.t
-
+  
 let create = Dn.create
+  
+let add = function
+  | None -> 
+      (fun dn (c,v) -> 
+	Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v))
+  | Some st -> 
+      (fun dn (c,v) -> 
+	Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
 
-let add dn (c,v) = Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v)
-
-let rmv dn (c,v) = Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v)
+let rmv = function
+  | None -> 
+      (fun dn (c,v) -> 
+	Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v))
+  | Some st -> 
+      (fun dn (c,v) -> 
+	Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
 
-let lookup dn t =
-  List.map 
-    (fun ((c,_),v) -> (c,v)) 
-    (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth))
+let lookup = function
+  | None -> 
+      (fun dn t ->
+	List.map 
+	  (fun ((c,_),v) -> (c,v)) 
+	  (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth)))
+  | Some st -> 
+      (fun dn t ->
+	List.map 
+	  (fun ((c,_),v) -> (c,v)) 
+	  (Dn.lookup dn (bounded_constr_val_discr_st st) (t,!dnet_depth)))
 
 let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn