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, 36 insertions, 16 deletions

diff --git a/tactics/dn.ml b/tactics/dn.ml
index dbfafcd61c..0809c80ebb 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -32,6 +33,10 @@
 
 type ('lbl,'pat) decompose_fun = 'pat -> ('lbl * 'pat list) option
 
+type 'res lookup_res = Label of 'res | Nothing | Everything
+    
+type ('lbl,'tree) lookup_fun = 'tree -> ('lbl * 'tree list) lookup_res
+
 type ('lbl,'pat,'inf) t = (('lbl * int) option,'pat * 'inf) Tlm.t
 
 let create () = Tlm.empty
@@ -46,29 +51,44 @@ let path_of dna =
 	    
   and pathrec deferred t =
     match dna t with
-      | None -> 
-	  None :: (path_of_deferred deferred)
-      | Some (lbl,[]) ->
-	  (Some (lbl,0))::(path_of_deferred deferred)
-      | Some (lbl,(h::def_subl as v)) ->
-	  (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h)
+    | None -> 
+	None :: (path_of_deferred deferred)
+    | Some (lbl,[]) ->
+	(Some (lbl,0))::(path_of_deferred deferred)
+    | Some (lbl,(h::def_subl as v)) ->
+	(Some (lbl,List.length v))::(pathrec (def_subl@deferred) h)
   in 
   pathrec []
     
 let tm_of tm lbl =
-  try [Tlm.map tm lbl] with Not_found -> []
-
+  try [Tlm.map tm lbl, true] with Not_found -> []
+    
+let rec skip_arg n tm =
+  if n = 0 then [tm,true]
+  else
+    List.flatten 
+      (List.map 
+	  (fun a -> match a with
+	  | None -> skip_arg (pred n) (Tlm.map tm a)
+	  | Some (lbl,m) -> 
+	      skip_arg (pred n + m) (Tlm.map tm a)) 
+	  (Tlm.dom tm))
+      
 let lookup tm dna t =
   let rec lookrec t tm =
-    (tm_of tm None)@
-    (match dna t with
-       | None -> []
-       | Some(lbl,v) ->
-	   List.fold_left 
-	     (fun l c -> List.flatten(List.map (lookrec c) l))
-             (tm_of tm (Some(lbl,List.length v))) v)
+    match dna t with
+    | Nothing -> tm_of tm None
+    | Label(lbl,v) ->
+	tm_of tm None@
+	  (List.fold_left 
+	      (fun l c -> 
+		List.flatten(List.map (fun (tm, b) ->
+		  if b then lookrec c tm
+		  else [tm,b]) l))
+              (tm_of tm (Some(lbl,List.length v))) v)
+    | Everything -> skip_arg 1 tm
   in 
-  List.flatten(List.map Tlm.xtract (lookrec t tm))
+    List.flatten (List.map (fun (tm,b) -> Tlm.xtract tm) (lookrec t tm))
 
 let add tm dna (pat,inf) =
   let p = path_of dna pat in Tlm.add tm (p,(pat,inf))