DISCLAIMER

==========

This big patch is commited here with a HUGE experimental tag on it. It
is probably not a finished job. The aim of committing it now, as
agreed with Hugo, is to get some feedback from potential users to
identify more clearly the directions the implementation could take. So
please feel free to mail me any remarks, bug reports or advices at
<puech@cs.unibo.it>.

Here are the changes induced by it :

For the user
============

* Search tools have been reimplemented to be faster and more
  general. Affected are [SearchPattern], [SearchRewrite] and [Search]
  (not [SearchAbout] yet). Changes are:

  - All of them accept general constructions, and previous syntactical
    limitations are abolished. In particular, one can for example
    [SearchPattern (nat -> Prop)], which will find [isSucc], but also
    [le], [gt] etc.

  - Patterns are typed. This means that you cannot search mistyped
    expressions anymore. I'm not sure if it's a good or a bad thing
    though (especially regarding coercions)...

* New tool to automatically infer (some) Record/Typeclasses instances.
  Usage : [Record/Class *Infer* X := ...] flags a record/class as
  subject to instance search. There is also an option to
  activate/deactivate the search [Set/Unset Autoinstance].  It works
  by finding combinations of definitions (actually all kinds of
  objects) which forms a record instance, possibly parameterized. It
  is activated at two moments:

  - A complete search is done when defining a new record, to find all
    possible instances that could have been formed with past
    definitions. Example: 

      Require Import List.
      Record Infer Monoid A (op:A->A->A) e := 
        { assoc : forall x y z, op x (op y z) = op (op x y) z; 
          idl : forall x, x = op x e ; 
          idr : forall x, x = op e x }.

      new instance Monoid_autoinstance_1 : (Monoid nat plus 0)
      [...]

  - At each new declaration (Definition, Axiom, Inductive), a search
    is made to find instances involving the new object. Example:

      Parameter app_nil_beg : forall A (l:list A), l = nil ++ l.

      new instance Build_Monoid_autoinstance_12 :
      (forall H : Type, Monoid (list H) app nil) :=
      (fun H : Type =>
      Build_Monoid (list H) app nil ass_app (app_nil_beg H)
      (app_nil_end H))


For the developper
==================

* New yet-to-be-named datastructure in [lib/dnet.ml]. Should do
  efficient one-to-many or many-to-one non-linear first-order
  filtering, faster than traditional methods like discrimination nets
  (so yes, the name of the file should probably be changed).

* Comes with its application to Coq's terms
  [pretyping/term_dnet.ml]. Terms are represented so that you can
  search for patterns under products as fast as you would do not under
  products, and facilities are provided to express other kind of
  searches (head of application, under equality, whatever you need
  that can be expressed as a pattern)

* A global repository of all objects defined and imported is
  maintained [toplevel/libtypes.ml], with all search facilities
  described before.

* A certain kind of proof search in [toplevel/autoinstance.ml]. For
  the moment it is specialized on finding instances, but it should be
  generalizable and reusable (more on this in a few months :-).


The bad news
============

* Compile time should increase by 0 to 15% (depending on the size of
  the Requires done). This could be optimized greatly by not
  performing substitutions on modules which are not functors I
  think. There may also be some inefficiency sources left in my code
  though...

* Vo's also gain a little bit of weight (20%). That's inevitable if I
  wanted to store the big datastructure of objects, but could also be
  optimized some more.


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

11 files changed, 684 insertions, 8 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6ac857d5c8..dab5c79873 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -71,7 +71,10 @@ let nf_env_evar sigma env =
 let nf_evar_info evc info =
   { info with 
     evar_concl = Reductionops.nf_evar evc info.evar_concl;
-    evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps}
+    evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps;
+    evar_body = match info.evar_body with
+      | Evar_empty -> Evar_empty
+      | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) }
 
 let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
 		     evm Evd.empty
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index b29afc0cb3..a76df2dfb9 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -421,11 +421,27 @@ type evar_defs =
       history : (existential_key * (loc * hole_kind)) list;
       metas : clbinding Metamap.t }
 
+let subst_named_context_val s = map_named_val (subst_mps s)
+
+let subst_evar_info s evi = 
+  let subst_evb = function Evar_empty -> Evar_empty
+    | Evar_defined c -> Evar_defined (subst_mps s c) in
+  { evi with
+      evar_concl = subst_mps s evi.evar_concl;
+      evar_hyps = subst_named_context_val s evi.evar_hyps;
+      evar_body = subst_evb evi.evar_body }
+
+let subst_evar_map sub evm = 
+  assert (snd evm = UniverseMap.empty);
+  Evarmap.map (subst_evar_info sub) (fst evm), snd evm
+
 let subst_evar_defs_light sub evd =
-  assert (evd.evars = (Evarmap.empty,UniverseMap.empty));
+  assert (snd evd.evars = UniverseMap.empty);
   assert (evd.conv_pbs = []);
   { evd with
-    metas = Metamap.map (map_clb (subst_mps sub)) evd.metas }
+      metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
+      evars = Evarmap.map (subst_evar_info sub)  (fst evd.evars), snd evd.evars
+  }
 
 let create_evar_defs sigma =
   { evars=sigma; conv_pbs=[]; last_mods = []; history=[]; metas=Metamap.empty }
@@ -715,6 +731,7 @@ let pr_evar_defs evd =
     if evd.evars = empty then mt() else
       str"EVARS:"++brk(0,1)++pr_evar_map evd.evars++fnl() in
   let cstrs =
+    if evd.conv_pbs = [] then mt() else
     str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in
   let pp_met =
     if evd.metas = Metamap.empty then mt() else
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 825096acca..0e3212813d 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -156,7 +156,8 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding
 (* Unification state *)
 type evar_defs
 
-(* Assume empty [evar_map] and [conv_pbs] *)
+val subst_evar_map : substitution -> evar_map -> evar_map
+(* Assume empty universe constraints in [evar_map] and [conv_pbs] *)
 val subst_evar_defs_light : substitution -> evar_defs -> evar_defs
 
 (* create an [evar_defs] with empty meta map: *)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e8860c065c..b6749db198 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -93,6 +93,58 @@ let find_projection = function
   | ConstRef cst -> Cmap.find cst !projection_table
   | _ -> raise Not_found
 
+(* Management of a field store : each field + argument of the inferred
+ * records are stored in a discrimination tree *)
+
+let subst_id s (gr,ev,evm) = 
+  (fst(subst_global s gr),ev,Evd.subst_evar_map s evm)
+
+module MethodsDnet : Term_dnet.S 
+  with type ident = global_reference * Evd.evar * Evd.evar_map
+  = Term_dnet.Make
+  (struct 
+     type t = global_reference * Evd.evar * Evd.evar_map
+     let compare = Pervasives.compare
+     let subst = subst_id
+     let constr_of (_,ev,evm) = Evd.evar_concl (Evd.find evm ev)
+   end) 
+  (struct 
+     let reduce c = Reductionops.head_unfold_under_prod 
+       Names.full_transparent_state (Global.env()) Evd.empty c 
+     let direction = true
+   end)
+
+let meth_dnet = ref MethodsDnet.empty
+
+open Summary
+
+let _ = 
+  declare_summary "record-methods-state"
+    { freeze_function = (fun () -> !meth_dnet);
+      unfreeze_function = (fun m -> meth_dnet := m);
+      init_function = (fun () -> meth_dnet := MethodsDnet.empty);
+      survive_module = false;
+      survive_section = false }
+
+open Libobject
+
+let load_method (_,(ty,id)) =
+  meth_dnet := MethodsDnet.add ty id !meth_dnet
+
+let (in_method,out_method) = 
+  declare_object
+    { (default_object "RECMETHODS") with
+	load_function = (fun _ -> load_method);
+	cache_function = load_method;
+	subst_function = (fun (_,s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id);
+	export_function = (fun x -> Some x);
+	classify_function = (fun (_,x) -> Substitute x) 
+    }
+
+let methods_matching c = MethodsDnet.search_pattern !meth_dnet c
+
+let declare_method cons ev sign =
+  Lib.add_anonymous_leaf (in_method ((Evd.evar_concl (Evd.find sign ev)),(cons,ev,sign)))
 
 (************************************************************************)
 (*s A canonical structure declares "canonical" conversion hints between *)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 638cc4304e..4d28ee55b1 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -41,6 +41,15 @@ val find_projection_nparams : global_reference -> int
 (* raise [Not_found] if not a projection *)
 val find_projection : global_reference -> struc_typ
 
+(* we keep an index (dnet) of record's arguments + fields
+   (=methods). Here is how to declare them: *)
+val declare_method :
+  global_reference -> Evd.evar -> Evd.evar_map -> unit
+  (* and here is how to search for methods matched by a given term: *)
+val methods_matching : constr -> 
+  ((global_reference*Evd.evar*Evd.evar_map) * 
+     (constr*existential_key)*Termops.subst) list
+
 (*s A canonical structure declares "canonical" conversion hints between *)
 (*  the effective components of a structure and the projections of the  *)
 (*  structure *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f51820bf62..aadb36396a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -970,3 +970,21 @@ let meta_reducible_instance evd b =
     | _ -> map_constr irec u
   in 
   if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus
+
+
+let head_unfold_under_prod ts env _ c = 
+  let unfold cst = 
+    if Cpred.mem cst (snd ts) then
+      match constant_opt_value env cst with
+	| Some c -> c 
+	| None -> mkConst cst
+    else mkConst cst in
+  let rec aux c =
+    match kind_of_term c with
+      | Prod (n,t,c) -> mkProd (n,aux t, aux c)
+      | _ -> 
+	  let (h,l) = decompose_app c in
+	  match kind_of_term h with
+	    | Const cst -> beta_applist (unfold cst,l)
+	    | _ -> c in
+  aux c
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index edbb4f90ca..171967583e 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -215,6 +215,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env ->  evar_map -> constr
 val whd_meta : (metavariable * constr) list -> constr -> constr
 val plain_instance : (metavariable * constr) list -> constr -> constr
 val instance : (metavariable * constr) list -> constr -> constr
+val head_unfold_under_prod : transparent_state -> reduction_function
 
 (*s Heuristic for Conversion with Evar *)
 
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
new file mode 100644
index 0000000000..656a90c704
--- /dev/null
+++ b/pretyping/term_dnet.ml
@@ -0,0 +1,388 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+(*i*)
+open Util
+open Term
+open Sign
+open Names
+open Libnames
+open Mod_subst
+open Pp (* debug *)
+(*i*)
+
+
+(* Representation/approximation of terms to use in the dnet:
+ * 
+ * - no meta or evar (use ['a pattern] for that)
+ * 
+ * - [Rel]s and [Sort]s are not taken into account (that's why we need
+ *   a second pass of linear filterin on the results - it's not a perfect
+ *   term indexing structure)
+
+ * - Foralls and LetIns are represented by a context DCtx (a list of
+ *   generalization, similar to rel_context, and coded with DCons and
+ *   DNil). This allows for matching under an unfinished context
+ *)
+
+module DTerm =
+struct
+
+  type 't t =
+    | DRel
+    | DSort
+    | DRef    of global_reference
+    | DCtx    of 't * 't (* (binding list, subterm) = Prods and LetIns *)
+    | DLambda of 't * 't
+    | DApp    of 't * 't (* binary app *)
+    | DCase   of case_info * 't * 't * 't array
+    | DFix    of int array * int * 't array * 't array
+    | DCoFix  of int * 't array * 't array
+
+    (* special constructors only inside the left-hand side of DCtx or
+       DApp. Used to encode lists of foralls/letins/apps as contexts *)
+    | DCons   of ('t * 't option) * 't
+    | DNil
+
+  type dconstr = dconstr t
+      
+  (* debug *)
+  let rec pr_dconstr f : 'a t -> std_ppcmds = function
+    | DRel -> str "*"
+    | DSort -> str "Sort"
+    | DRef _ -> str "Ref"
+    | DCtx (ctx,t) -> f ctx ++ spc() ++ str "|-" ++ spc () ++ f t
+    | DLambda (t1,t2) -> str "fun"++ spc() ++ f t1 ++ spc() ++ str"->" ++ spc() ++ f t2
+    | DApp (t1,t2) -> f t1 ++ spc() ++ f t2
+    | DCase (_,t1,t2,ta) -> str "case"
+    | DFix _ -> str "fix"
+    | DCoFix _ -> str "cofix"
+    | DCons ((t,dopt),tl) -> f t ++ (match dopt with 
+	  Some t' -> str ":=" ++ f t'
+	| None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl
+    | DNil -> str "[]"
+
+  (*
+   * Functional iterators for the t datatype
+   * a.k.a boring and error-prone boilerplate code
+   *)
+
+  let map f = function
+    | (DRel | DSort | DNil | DRef _) as c -> c
+    | DCtx (ctx,c) -> DCtx (f ctx, f c)
+    | DLambda (t,c) -> DLambda (f t, f c)
+    | DApp (t,u) -> DApp (f t,f u)
+    | DCase (ci,p,c,bl) -> DCase (ci, f p, f c, Array.map f bl)
+    | DFix (ia,i,ta,ca) ->
+	DFix (ia,i,Array.map f ta,Array.map f ca)
+    | DCoFix(i,ta,ca) ->
+	DCoFix (i,Array.map f ta,Array.map f ca)
+    | DCons ((t,topt),u) -> DCons ((f t,Option.map f topt), f u)
+
+  let compare = Pervasives.compare
+
+  let fold f acc = function
+    | (DRel | DNil | DSort | DRef _) -> acc
+    | DCtx (ctx,c) -> f (f acc ctx) c
+    | DLambda (t,c) -> f (f acc t) c
+    | DApp (t,u) -> f (f acc t) u
+    | DCase (ci,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
+    | DFix (ia,i,ta,ca) ->
+	Array.fold_left f (Array.fold_left f acc ta) ca
+    | DCoFix(i,ta,ca) ->
+	Array.fold_left f (Array.fold_left f acc ta) ca
+    | DCons ((t,topt),u) -> f (Option.fold_left f (f acc t) topt) u
+
+  let choose f = function
+    | (DRel | DSort | DNil | DRef _) -> invalid_arg "choose"
+    | DCtx (ctx,c) -> f ctx
+    | DLambda (t,c) -> f t
+    | DApp (t,u) -> f u
+    | DCase (ci,p,c,bl) -> f c
+    | DFix (ia,i,ta,ca) -> f ta.(0)
+    | DCoFix (i,ta,ca) -> f ta.(0)
+    | DCons ((t,topt),u) -> f u
+
+  let fold2 (f:'a -> 'b -> 'c -> 'a) (acc:'a) (c1:'b t) (c2:'c t) : 'a =
+    let head w = map (fun _ -> ()) w in
+    if compare (head c1) (head c2) <> 0
+    then invalid_arg "fold2:compare" else
+      match c1,c2 with
+	| (DRel, DRel | DNil, DNil | DSort, DSort | DRef _, DRef _) -> acc
+	| (DCtx (c1,t1), DCtx (c2,t2) 
+	  | DApp (c1,t1), DApp (c2,t2)
+	  | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2
+	| DCase (ci,p1,c1,bl1),DCase (_,p2,c2,bl2) -> 
+	    array_fold_left2 f (f (f acc p1 p2) c1 c2) bl1 bl2
+	| DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) ->
+	    array_fold_left2 f (array_fold_left2 f acc ta1 ta2) ca1 ca2
+	| DCoFix(i,ta1,ca1), DCoFix(_,ta2,ca2) ->
+	    array_fold_left2 f (array_fold_left2 f acc ta1 ta2) ca1 ca2
+	| DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
+	    f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2
+	| _ -> assert false
+
+  let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t = 
+    let head w = map (fun _ -> ()) w in
+    if compare (head c1) (head c2) <> 0
+    then invalid_arg "map2_t:compare" else
+      match c1,c2 with
+	| (DRel, DRel | DSort, DSort | DNil, DNil | DRef _, DRef _) as cc ->
+	    let (c,_) = cc in c
+	| DCtx (c1,t1), DCtx (c2,t2) -> DCtx (f c1 c2, f t1 t2)
+	| DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2)
+	| DApp (t1,u1), DApp (t2,u2) -> DApp (f t1 t2,f u1 u2)
+	| DCase (ci,p1,c1,bl1), DCase (_,p2,c2,bl2) -> 
+	    DCase (ci, f p1 p2, f c1 c2, array_map2 f bl1 bl2)
+	| DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) ->
+	    DFix (ia,i,array_map2 f ta1 ta2,array_map2 f ca1 ca2)
+	| DCoFix (i,ta1,ca1), DCoFix (_,ta2,ca2) ->
+	    DCoFix (i,array_map2 f ta1 ta2,array_map2 f ca1 ca2)
+	| DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> 
+	    DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2)
+	| _ -> assert false
+
+  let terminal = function
+    | (DRel | DSort | DNil | DRef _) -> true
+    | _ -> false    
+end
+      
+(*
+ * Terms discrimination nets
+ * Uses the general dnet datatype on DTerm.t
+ * (here you can restart reading)
+ *)
+
+(* 
+ * Construction of the module 
+ *)
+
+module type IDENT =
+sig
+  type t
+  val compare : t -> t -> int
+  val subst : substitution -> t -> t
+  val constr_of : t -> constr
+end
+
+module type OPT =
+sig
+  val reduce : constr -> constr
+  val direction : bool
+end
+
+module Make =
+  functor (Ident : IDENT) ->
+  functor (Opt : OPT) ->
+struct
+
+  module TDnet : Dnet.S with type ident=Ident.t
+			and  type 'a structure = 'a DTerm.t
+			and  type meta = metavariable 
+    = Dnet.Make(DTerm)(Ident)
+    (struct
+       type t = metavariable
+       let compare = Pervasives.compare
+     end)
+
+  type t = TDnet.t
+      
+  type ident = TDnet.ident
+      
+  type 'a pattern = 'a TDnet.pattern
+  type term_pattern = term_pattern DTerm.t pattern
+      
+  type idset = TDnet.Idset.t
+
+  type result = ident * (constr*existential_key) * Termops.subst
+
+  open DTerm
+  open TDnet
+  
+  let rec pat_of_constr c : term_pattern = 
+    match kind_of_term c with
+      | Rel _          -> Term DRel
+      | Sort _         -> Term DSort
+      | Var i          -> Term (DRef (VarRef i))
+      | Const c        -> Term (DRef (ConstRef c))
+      | Ind i          -> Term (DRef (IndRef i))
+      | Construct c    -> Term (DRef (ConstructRef c))
+      | Term.Meta _    -> assert false
+      | Evar (i,_)     -> Meta i
+      | Case (ci,c1,c2,ca)     -> 
+	  Term(DCase(ci,pat_of_constr c1,pat_of_constr c2,Array.map pat_of_constr ca))
+      | Fix ((ia,i),(_,ta,ca)) -> 
+	  Term(DFix(ia,i,Array.map pat_of_constr ta, Array.map pat_of_constr ca))
+      | CoFix (i,(_,ta,ca))    -> 
+	  Term(DCoFix(i,Array.map pat_of_constr ta,Array.map pat_of_constr ca))
+      | Cast (c,_,_)   -> pat_of_constr c
+      | Lambda (_,t,c) -> Term(DLambda (pat_of_constr t, pat_of_constr c))
+      | (Prod (_,_,_) | LetIn(_,_,_,_))   -> 
+	  let (ctx,c) = ctx_of_constr (Term DNil) c in Term (DCtx (ctx,c))
+      | App (f,ca)     -> 
+	  Array.fold_left (fun c a -> Term (DApp (c,a)))
+	    (pat_of_constr f) (Array.map pat_of_constr ca)
+
+  and ctx_of_constr ctx c : term_pattern * term_pattern = 
+    match kind_of_term c with
+      | Prod (_,t,c)   -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c
+      | LetIn(_,d,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t, Some (pat_of_constr d)),ctx))) c
+      | _ -> ctx,pat_of_constr c
+	  
+  let empty_ctx : term_pattern -> term_pattern = function
+    | Meta _ as c -> c
+    | Term (DCtx(_,_)) as c -> c
+    | c -> Term (DCtx (Term DNil, c))
+	  
+  (* 
+   * Basic primitives
+   *)
+
+  let empty = TDnet.empty
+    
+  let subst s t = 
+    let sleaf id = Ident.subst s id in
+    let snode = function
+      | DTerm.DRef gr -> DTerm.DRef (fst (subst_global s gr))
+      | n -> n in
+    TDnet.map sleaf snode t
+      
+  let union = TDnet.union
+    
+  let add (c:constr) (id:Ident.t) (dn:t) =
+    let c = Opt.reduce c in
+    let c = empty_ctx (pat_of_constr c) in
+    TDnet.add dn c id
+
+  let new_meta_no =
+    let ctr = ref 0 in
+    fun () -> decr ctr; !ctr
+      
+  let new_meta_no = Evarutil.new_untyped_evar
+
+  let neutral_meta = new_meta_no()
+    
+  let new_meta () = Meta (new_meta_no())
+  let new_evar () = mkEvar(new_meta_no(),[||])
+
+  let rec remove_cap : term_pattern -> term_pattern = function
+    | Term (DCons (t,u)) -> Term (DCons (t,remove_cap u))
+    | Term DNil -> new_meta()
+    | _ -> assert false
+
+  let under_prod : term_pattern -> term_pattern = function
+    | Term (DCtx (t,u)) -> Term (DCtx (remove_cap t,u))
+    | Meta m -> Term (DCtx(new_meta(), Meta m))
+    | _ -> assert false
+
+  let init = let e = new_meta_no() in (mkEvar (e,[||]),e)
+
+  let rec e_subst_evar i (t:unit->constr) c =
+    match kind_of_term c with
+    | Evar (j,_) when i=j -> t()
+    | _ -> map_constr (e_subst_evar i t) c
+
+  let subst_evar i c = e_subst_evar i (fun _ -> c)
+
+  (* debug *)
+  let rec pr_term_pattern p = 
+    (fun pr_t -> function 
+       | Term t -> pr_t t
+       | Meta m -> str"["++Util.pr_int (Obj.magic m)++str"]"
+    ) (pr_dconstr pr_term_pattern) p
+
+  let search_pat cpat dpat dn (up,plug) = 
+    let whole_c = subst_evar plug cpat up in
+    TDnet.Idset.fold
+      (fun id acc -> 
+	 let c_id = Opt.reduce (Ident.constr_of id) in
+	 let (ctx,wc) = 
+	   try Termops.align_prod_letin whole_c c_id 
+	   with Invalid_argument _ -> [],c_id in
+	 let up = it_mkProd_or_LetIn up ctx in
+	 let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
+	 try (id,(up,plug),Termops.filtering ctx Reduction.CUMUL wc whole_c)::acc
+	 with Termops.CannotFilter -> acc
+      ) (TDnet.find_match dpat dn) []
+
+  let fold_pattern_neutral f =
+    fold_pattern (fun m dn acc -> if m=neutral_meta then acc else f m dn acc)
+
+  let fold_pattern_nonlin f =
+    let defined = ref Gmap.empty in
+    fold_pattern_neutral
+      ( fun m dn acc ->
+	 let dn = try TDnet.inter dn (Gmap.find m !defined) with Not_found -> dn in
+	 defined := Gmap.add m dn !defined;
+	 f m dn acc )
+
+  let fold_pattern_up f acc dpat cpat dn (up,plug) =
+    fold_pattern_nonlin
+      ( fun m dn acc ->
+	  f dn (subst_evar plug (e_subst_evar neutral_meta new_evar cpat) up, m) acc 
+      ) acc dpat dn
+
+  let possibly_under pat k dn (up,plug) = 
+    let rec aux fst dn (up,plug) acc = 
+      let cpat = pat() in
+      let dpat = pat_of_constr cpat in
+      let dpat = if fst then empty_ctx dpat else dpat in
+      snd (fold_pattern_up (aux false) acc dpat cpat dn (up,plug)) @
+	(k dn (up,plug)) in
+    aux true dn (up,plug) []
+
+  let eq_pat eq () = mkApp(eq,[|mkEvar(neutral_meta,[||]);new_evar();new_evar()|])
+  let app_pat () = mkApp(new_evar(),[|mkEvar(neutral_meta,[||])|])
+
+  (*
+   * High-level primitives describing specific search problems
+   *)
+
+  let search_pattern dn pat = 
+    let pat = Opt.reduce pat in
+    search_pat pat (empty_ctx (pat_of_constr pat)) dn init
+    
+  let search_concl dn pat =
+    let pat = Opt.reduce pat in
+    search_pat pat (under_prod (empty_ctx (pat_of_constr pat))) dn init
+
+  let search_eq_concl dn eq pat = 
+    let pat = Opt.reduce pat in
+    let eq_pat = eq_pat eq () in
+    let eq_dpat = under_prod (empty_ctx (pat_of_constr eq_pat)) in
+    snd (fold_pattern_up
+      (fun dn up acc -> 
+	 search_pat pat (pat_of_constr pat) dn up @ acc
+      ) [] eq_dpat eq_pat dn init)
+      
+   let search_head_concl dn pat = 
+    let pat = Opt.reduce pat in
+    possibly_under app_pat (search_pat pat (pat_of_constr pat)) dn init
+
+  let find_all dn = Idset.elements (TDnet.find_all dn)
+end
+    
+module type S =
+sig
+  type t
+  type ident
+    
+  type result = ident * (constr*existential_key) * Termops.subst
+
+  val empty : t
+  val add : constr -> ident -> t -> t
+  val union : t -> t -> t
+  val subst : substitution -> t -> t
+  val search_pattern : t -> constr -> result list
+  val search_concl : t -> constr -> result list
+  val search_head_concl : t -> constr -> result list
+  val search_eq_concl : t -> constr -> constr -> result list
+  val find_all : t -> ident list
+end
diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
new file mode 100644
index 0000000000..ccf9624814
--- /dev/null
+++ b/pretyping/term_dnet.mli
@@ -0,0 +1,110 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+(*i*)
+open Term
+open Sign
+open Libnames
+open Mod_subst
+(*i*)
+
+(* Dnets on constr terms. 
+   
+   An instantiation of Dnet on (an approximation of) constr. It
+   associates a term (possibly with Evar) with an
+   identifier. Identifiers must be unique (no two terms sharing the
+   same ident), and there must be a way to recover the full term from
+   the identifier (function constr_of).
+
+   Optionally, a pre-treatment on terms can be performed before adding
+   or searching (reduce). Practically, it is used to do some kind of
+   delta-reduction on terms before indexing them.
+
+   The results returned here are perfect, since post-filtering is done
+   inside here.
+
+   See lib/dnet.mli for more details.
+*)
+
+(* Identifiers to store (right hand side of the association) *)
+module type IDENT = sig
+  type t
+  val compare : t -> t -> int
+
+  (* how to substitute them for storage *)
+  val subst : substitution -> t -> t
+
+  (* how to recover the term from the identifier *)
+  val constr_of : t -> constr
+end
+
+(* Options : *)
+module type OPT = sig
+
+  (* pre-treatment to terms before adding or searching *)
+  val reduce : constr -> constr
+
+  (* direction of post-filtering w.r.t sort subtyping : 
+     - true means query <= terms in the structure
+     - false means terms <= query
+ *)
+  val direction : bool
+end
+
+module type S =
+sig
+  type t
+  type ident
+
+  (* results of filtering : identifier, a context (term with Evar
+     hole) and the substitution in that context*)
+  type result = ident * (constr*existential_key) * Termops.subst
+
+  val empty : t
+
+  (* [add c i dn] adds the binding [(c,i)] to [dn]. [c] can be a
+     closed term or a pattern (with untyped Evars). No Metas accepted *)
+  val add : constr -> ident -> t -> t
+
+  (* merge of dnets. Faster than re-adding all terms *)
+  val union : t -> t -> t
+
+  val subst : substitution -> t -> t
+
+  (* 
+   * High-level primitives describing specific search problems 
+   *)
+
+  (* [search_pattern dn c] returns all terms/patterns in dn
+     matching/matched by c *)
+  val search_pattern : t -> constr -> result list
+   
+  (* [search_concl dn c] returns all matches under products and
+     letins, i.e. it finds subterms whose conclusion matches c. The
+     complexity depends only on c ! *)
+  val search_concl : t -> constr -> result list
+
+  (* [search_head_concl dn c] matches under products and applications
+     heads. Finds terms of the form [forall H_1...H_n, C t_1...t_n]
+     where C matches c *)
+  val search_head_concl : t -> constr -> result list
+    
+  (* [search_eq_concl dn eq c] searches terms of the form [forall
+     H1...Hn, eq _ X1 X2] where either X1 or X2 matches c *)
+  val search_eq_concl : t -> constr -> constr -> result list
+
+  (* [find_all dn] returns all idents contained in dn *)
+  val find_all : t -> ident list
+end
+
+module Make :
+  functor (Ident : IDENT) ->
+  functor (Opt : OPT) ->
+    S with type ident = Ident.t
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 987db88b18..e3b8a166c7 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -951,16 +951,77 @@ let base_sort_cmp pb s0 s1 =
     | _ -> false
 
 (* eq_constr extended with universe erasure *)
-let rec constr_cmp cv_pb t1 t2 =
+let compare_constr_univ f cv_pb t1 t2 = 
   match kind_of_term t1, kind_of_term t2 with
       Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
     | Prod (_,t1,c1), Prod (_,t2,c2) -> 
-	constr_cmp Reduction.CONV t1 t2 & 
-	  constr_cmp cv_pb c1 c2
-    | _ -> compare_constr (constr_cmp Reduction.CONV) t1 t2
+	f Reduction.CONV t1 t2 & f cv_pb c1 c2
+    | _ -> compare_constr (f Reduction.CONV) t1 t2
+
+let rec constr_cmp cv_pb t1 t2 = compare_constr_univ constr_cmp cv_pb t1 t2
 
 let eq_constr = constr_cmp Reduction.CONV
 
+(* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn)
+   App(c,[||]) -> ([],c) *)
+let split_app c = match kind_of_term c with
+    App(c,l) -> 
+      let len = Array.length l in
+      if len=0 then ([],c) else
+	let last = Array.get l (len-1) in
+	let prev = Array.sub l 0 (len-1) in
+	c::(Array.to_list prev), last
+  | _ -> assert false
+
+let hdtl l = List.hd l, List.tl l
+
+type subst = (rel_context*constr) Intmap.t
+
+exception CannotFilter
+
+let filtering env cv_pb c1 c2 =
+  let evm = ref Intmap.empty in
+  let define cv_pb e1 ev c1 = 
+    try let (e2,c2) = Intmap.find ev !evm in
+    let shift = List.length e1 - List.length e2 in
+    if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter
+    with Not_found -> 
+      evm := Intmap.add ev (e1,c1) !evm
+  in
+  let rec aux env cv_pb c1 c2 =
+    match kind_of_term c1, kind_of_term c2 with
+      | App _, App _ -> 
+	  let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in
+	  aux env cv_pb l1 l2; if p1=[] & p2=[] then () else
+	      aux env cv_pb (applist (hdtl p1)) (applist (hdtl p2))
+      | Prod (n,t1,c1), Prod (_,t2,c2) ->
+	  aux env cv_pb t1 t2;
+	  aux ((n,None,t1)::env) cv_pb c1 c2
+      | _, Evar (ev,_) -> define cv_pb env ev c1
+      | Evar (ev,_), _ -> define cv_pb env ev c2
+      | _ -> 
+	  if compare_constr_univ 
+	  (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then () 
+	  else raise CannotFilter
+	  (* TODO: le reste des binders *)
+  in
+  aux env cv_pb c1 c2; !evm
+
+let decompose_prod_letin : constr -> int * rel_context * constr = 
+  let rec prodec_rec i l c = match kind_of_term c with
+    | Prod (n,t,c)    -> prodec_rec (succ i) ((n,None,t)::l) c
+    | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c
+    | Cast (c,_,_)    -> prodec_rec i l c
+    | _               -> i,l,c in
+  prodec_rec 0 []
+
+let align_prod_letin c a : rel_context * constr =
+  let (lc,_,_) = decompose_prod_letin c in
+  let (la,l,a) = decompose_prod_letin a in
+  if not (la >= lc) then invalid_arg "align_prod_letin";
+  let (l1,l2) = Util.list_chop lc l in
+  l2,it_mkProd_or_LetIn a l1
+    
 (* On reduit une serie d'eta-redex de tete ou rien du tout  *)
 (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
 (* Remplace 2 versions précédentes buggées                  *)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 9163a1d9e5..79fe908d7a 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -170,12 +170,28 @@ val error_invalid_occurrence : int list -> 'a
 
 (* Alternative term equalities *)
 val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
+val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) ->
+  Reduction.conv_pb -> constr -> constr -> bool
 val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool
 val eq_constr : constr -> constr -> bool
 
 val eta_reduce_head : constr -> constr
 val eta_eq_constr : constr -> constr -> bool
 
+exception CannotFilter
+
+(* Lightweight first-order filtering procedure. Unification
+   variables ar represented by (untyped) Evars.  
+   [filtering c1 c2] returns the substitution n'th evar ->
+   (context,term), or raises [CannotFilter].
+   Warning: Outer-kernel sort subtyping are taken into account: c1 has
+   to be smaller than c2 wrt. sorts. *)
+type subst = (rel_context*constr) Intmap.t
+val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst
+
+val decompose_prod_letin : constr -> int * rel_context * constr
+val align_prod_letin : constr -> constr -> rel_context * constr
+
 (* finding "intuitive" names to hypotheses *)
 val lowercase_first_char : identifier -> string
 val sort_hdchar : sorts -> string