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

1 files changed, 128 insertions, 0 deletions

diff --git a/lib/dnet.mli b/lib/dnet.mli
new file mode 100644
index 0000000000..a01bbb0e2e
--- /dev/null
+++ b/lib/dnet.mli
@@ -0,0 +1,128 @@
+(************************************************************************)
+(*  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:$ *)
+
+(* Generic discrimination net implementation over recursive
+   types. This module implements a association data structure similar
+   to tries but working on any types (not just lists). It is a term
+   indexing datastructure, a generalization of the discrimination nets
+   described for example in W.W.McCune, 1992, related also to
+   generalized tries [Hinze, 2000].
+
+   You can add pairs of (term,identifier) into a dnet, where the
+   identifier is *unique*, and search terms in a dnet filtering a
+   given pattern (retrievial of instances). It returns all identifiers
+   associated with terms matching the pattern. It also works the other
+   way around : You provide a set of patterns and a term, and it
+   returns all patterns which the term matches (retrievial of
+   generalizations). That's why you provide *patterns* everywhere.
+
+   Warning 1: Full unification doesn't work as for now. Make sure the
+   set of metavariables in the structure and in the queries are
+   distincts, or you'll get unexpected behaviours.
+
+   Warning 2: This structure is perfect, i.e. the set of candidates
+   returned is equal to the set of solutions. Beware of DeBruijn
+   shifts and sorts subtyping though (which makes the comparison not
+   symmetric, see term_dnet.ml).
+
+   The complexity of the search is (almost) the depth of the term.
+   
+   To use it, you have to provide a module (Datatype) with the datatype
+   parametrized on the recursive argument. example:
+
+   type btree =                      type 'a btree0 =
+   | Leaf                    ===>    | Leaf
+   | Node of btree * btree           | Node of 'a * 'a
+
+*)
+
+(* datatype you want to build a dnet on *)
+module type Datatype =
+sig
+  (* parametric datatype. ['a] is morally the recursive argument *)
+  type 'a t
+
+  (* non-recursive mapping of subterms *)
+  val map : ('a -> 'b) -> 'a t -> 'b t
+  val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
+
+  (* non-recursive folding of subterms *)
+  val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
+  val fold2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a
+
+  (* comparison of constructors *)
+  val compare : unit t -> unit t -> int
+
+  (* for each constructor, is it not-parametric on 'a? *)
+  val terminal : 'a t -> bool
+
+  (* [choose f w] applies f on ONE of the subterms of w *)
+  val choose : ('a -> 'b) -> 'a t -> 'b
+end
+
+module type S =
+sig
+  type t
+    
+  (* provided identifier type *)
+  type ident
+
+  (* provided metavariable type *)
+  type meta
+    
+  (* provided parametrized datastructure *)
+  type 'a structure
+
+  (* returned sets of solutions *)
+  module Idset : Set.S with type elt=ident
+
+  (* a pattern is a term where each node can be a unification
+     variable *)
+  type 'a pattern =
+    | Term of 'a
+    | Meta of meta
+
+  type term_pattern = 'a structure pattern as 'a
+
+  val empty : t
+    
+  (* [add t w i] adds a new association (w,i) in t. *)
+  val add : t -> term_pattern -> ident -> t
+    
+  (* [find_all t] returns all identifiers contained in t. *)
+  val find_all : t -> Idset.t
+    
+  (* [fold_pattern f acc p dn] folds f on each meta of p, passing the
+     meta and the sub-dnet under it. The result includes:
+     - Some set if identifiers were gathered on the leafs of the term
+     - None if the pattern contains no leaf (only Metas at the leafs).
+  *)
+  val fold_pattern :
+    (meta -> t -> 'a -> 'a) -> 'a -> term_pattern -> t -> Idset.t option * 'a
+
+  (* [find_match p t] returns identifiers of all terms matching p in
+     t. *)
+  val find_match : term_pattern -> t -> Idset.t
+
+  (* set operations on dnets *)
+  val inter : t -> t -> t
+  val union : t -> t -> t
+
+  (* apply a function on each identifier and node of terms in a dnet *)
+  val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t
+end
+  
+module Make :
+  functor (T:Datatype) -> 
+  functor (Ident:Set.OrderedType) -> 
+  functor (Meta:Set.OrderedType) ->
+    S with type ident = Ident.t
+      and  type meta = Meta.t
+      and  type 'a structure = 'a T.t