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, 39 insertions, 29 deletions

diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 1c95f7fdc6..995183dc90 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -41,43 +41,53 @@ let decomp_pat =
   decrec []   
 
 let constr_pat_discr t =
-  if not (occur_meta_pattern t) then 
+  if not (occur_meta_pattern t) then
     None
   else
     match decomp_pat t with
-      | PRef ((IndRef _) as ref), args
-      | PRef ((ConstructRef _ ) as ref), args
-      | PRef ((VarRef _) as ref), args -> Some(ref,args)
-      | _ -> None
-
-let constr_val_discr t =
-  let c, l = decomp t in
-  match kind_of_term c with
-    (* Const _,_) -> Some(TERM c,l) *)
-    | Ind ind_sp -> Some(IndRef ind_sp,l)
-    | Construct cstr_sp -> Some(ConstructRef cstr_sp,l)
-    | Var id -> Some(VarRef id,l)
+    | PRef ((IndRef _) as ref), args
+    | PRef ((ConstructRef _ ) as ref), args -> Some (ref,args)
+    | PRef ((VarRef v) as ref), args -> Some(ref,args)
     | _ -> None
 
-(* Les deux fonctions suivantes ecrasaient les precedentes, 
-   ajout d'un suffixe _nil CP 16/08 *) 
-
-let constr_pat_discr_nil t =
-  match constr_pat_discr t with
-    | None -> None
-    | Some (c,_) -> Some(c,[])
-
-let constr_val_discr_nil t =
-  match constr_val_discr t with
-    | None -> None
-    | Some (c,_) -> Some(c,[])
+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 ((VarRef v) as ref), args when not (Idpred.mem v idpred) -> 
+      Some(ref,args)
+  | PVar v, args when not (Idpred.mem v idpred) ->
+      Some(VarRef v,args)
+  | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) ->
+      Some (ref, args)
+  | _ -> None
+
+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)
+    | _ -> 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)
+    | Evar _ -> Everything
+    | _ -> Nothing
 
 let create = Dn.create 
 
-let add dn = Dn.add dn constr_pat_discr
-
-let rmv dn = Dn.rmv dn constr_pat_discr
+let add dn st = Dn.add dn (constr_pat_discr_st st)
 
-let lookup dn t = Dn.lookup dn constr_val_discr t
+let rmv dn st = Dn.rmv dn (constr_pat_discr_st st)
 
+let lookup dn st t = Dn.lookup dn (constr_val_discr_st st) t
+  
 let app f dn = Dn.app f dn