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

7 files changed, 14 insertions, 274 deletions

diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index 3218781d12..4a5972cc71 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 open Pp
 open Util
diff --git a/parsing/g_string_syntax.ml b/parsing/g_string_syntax.ml
index 6b1faa76ce..a936485d9b 100644
--- a/parsing/g_string_syntax.ml
+++ b/parsing/g_string_syntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 open Pp
 open Util
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4b79113f3f..3a88a09f81 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -151,7 +151,7 @@ GEXTEND Gram
       (* Gallina inductive declarations *)
       | f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
-          VernacInductive (f,indl)
+          VernacInductive (f,false,indl)
       | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint (recs,true)
       | IDENT "Unboxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -165,13 +165,13 @@ GEXTEND Gram
 	l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ]
   ;
   gallina_ext:
-    [ [ b = record_token; oc = opt_coercion; name = identref;
+    [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref;
         ps = binders_let; 
 	s = OPT [ ":"; s = lconstr -> s ];
 	cfs = [ ":="; l = constructor_list_or_record_decl -> l
 	  | -> RecordDecl (None, []) ] ->
 	  let (recf,indf) = b in
-	    VernacInductive (indf,[((oc,name),ps,s,Some recf,cfs),None])
+	    VernacInductive (indf,infer,[((oc,name),ps,s,Some recf,cfs),None])
   ] ]
   ;
   typeclass_context:
@@ -217,6 +217,9 @@ GEXTEND Gram
     [ [ "Inductive" -> true
       | "CoInductive" -> false ] ]
   ;
+  infer_token:
+    [ [ "Infer" -> true | -> false ] ]
+  ;
   record_token:
     [ [ IDENT "Record" -> (Record,true)
       | IDENT "Structure" -> (Structure,true) 
@@ -597,8 +600,8 @@ GEXTEND Gram
       | IDENT "About"; qid = global -> VernacPrint (PrintAbout qid)
 
       (* Searching the environment *)
-      | IDENT "Search"; qid = global; l = in_or_out_modules -> 
-	  VernacSearch (SearchHead qid, l)
+      | IDENT "Search"; c = constr_pattern; l = in_or_out_modules -> 
+	  VernacSearch (SearchHead c, l)
       | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchPattern c, l)
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml
index 790b5c363f..31fd4561e6 100644
--- a/parsing/ppdecl_proof.ml
+++ b/parsing/ppdecl_proof.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 open Util 
 open Pp
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index df4eee8aa0..113b2f0402 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -140,7 +140,7 @@ let pr_search_about (b,c) =
   | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
 let pr_search a b pr_p = match a with
-  | SearchHead qid -> str"Search" ++ spc() ++ pr_reference qid ++ pr_in_out_modules b
+  | SearchHead c -> str"Search" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchPattern c -> str"SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b
@@ -576,7 +576,7 @@ let rec pr_vernac = function
       hov 2
         (pr_assumption_token (n > 1) stre ++ spc() ++ 
 	 pr_ne_params_list pr_lconstr_expr l)
-  | VernacInductive (f,l) ->
+  | VernacInductive (f,i,l) ->
 
       let pr_constructor (coe,(id,c)) =
         hov 2 (pr_lident id ++ str" " ++
@@ -601,6 +601,7 @@ let rec pr_vernac = function
 	in
 	  hov 0 (
 	    kw ++ spc() ++
+	      (if i then str"Infer" else str"") ++
               (if coe then str" > " else str" ") ++ pr_lident id ++
               pr_and_type_binders_arg indpar ++ spc() ++ 
 	      Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ 
diff --git a/parsing/search.ml b/parsing/search.ml
deleted file mode 100644
index 94270ee135..0000000000
--- a/parsing/search.ml
+++ /dev/null
@@ -1,214 +0,0 @@
-(************************************************************************)
-(*  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$ *)
-
-open Pp
-open Util
-open Names
-open Nameops
-open Term
-open Rawterm
-open Declarations
-open Libobject
-open Declare
-open Environ
-open Pattern
-open Matching
-open Printer
-open Libnames
-open Nametab
-
-(* The functions print_constructors and crible implement the behavior needed
-   for the Coq searching commands.
-   These functions take as first argument the procedure
-   that will be called to treat each entry.  This procedure receives the name
-   of the object, the assumptions that will make it possible to print its type,
-   and the constr term that represent its type. *)
-
-let print_constructors indsp fn env nconstr =
-  for i = 1 to nconstr do
-    fn (ConstructRef (indsp,i)) env (Inductiveops.type_of_constructor env (indsp,i))
-  done
-
-let rec head_const c = match kind_of_term c with
-  | Prod (_,_,d) -> head_const d
-  | LetIn (_,_,_,d) -> head_const d
-  | App (f,_)   -> head_const f
-  | Cast (d,_,_)   -> head_const d
-  | _            -> c
-
-(* General search, restricted to head constant if [only_head] *)
-
-let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
-  let env = Global.env () in
-  let crible_rec (sp,_) lobj = match object_tag lobj with
-    | "VARIABLE" ->
-	(try 
-	   let (id,_,typ) = Global.lookup_named (basename sp) in 
-           if refopt = None
-	     || head_const typ = constr_of_global (Option.get refopt)
-	   then
-	     fn (VarRef id) env typ
-	 with Not_found -> (* we are in a section *) ())
-    | "CONSTANT" ->
-	let cst = locate_constant (qualid_of_sp sp) in
-	let typ = Typeops.type_of_constant env cst in
-        if refopt = None
-	  || head_const typ = constr_of_global (Option.get refopt)
-	then
-	  fn (ConstRef cst) env typ
-    | "INDUCTIVE" -> 
-	let kn = locate_mind (qualid_of_sp sp) in
-        let mib = Global.lookup_mind kn in 
-        (match refopt with 
-	  | Some (IndRef ((kn',tyi) as ind)) when kn=kn' ->
-	      print_constructors ind fn env
-	        (Array.length (mib.mind_packets.(tyi).mind_user_lc))
-          | Some _ -> ()
-	  | _ ->
-              Array.iteri 
-	        (fun i mip -> print_constructors (kn,i) fn env
-	          (Array.length mip.mind_user_lc)) mib.mind_packets)
-    | _ -> ()
-  in 
-  try 
-    Declaremods.iter_all_segments crible_rec
-  with Not_found -> 
-    ()
-
-let crible ref = gen_crible (Some ref)
-
-(* Fine Search. By Yves Bertot. *)
-
-exception No_section_path
-
-let rec head c = 
-  let c = strip_outer_cast c in
-  match kind_of_term c with
-  | Prod (_,_,c) -> head c
-  | LetIn (_,_,_,c) -> head c
-  | _              -> c
-      
-let constr_to_section_path c = match kind_of_term c with
-  | Const sp -> sp
-  | _ -> raise No_section_path
-      
-let xor a b = (a or b) & (not (a & b))
-
-let plain_display ref a c =
-  let pc = pr_lconstr_env a c in
-  let pr = pr_global ref in
-  msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ())
-
-let filter_by_module (module_list:dir_path list) (accept:bool) 
-  (ref:global_reference) _ _ =
-  try
-    let sp = sp_of_global ref in
-    let sl = dirpath sp in
-    let rec filter_aux = function
-      | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl)
-      | [] -> true 
-    in
-    xor accept (filter_aux module_list)
-  with No_section_path -> 
-    false
-
-let gref_eq =
-  IndRef (Libnames.encode_kn Coqlib.logic_module (id_of_string "eq"), 0)
-let gref_eqT =
-  IndRef (Libnames.encode_kn Coqlib.logic_type_module (id_of_string "eqT"), 0)
-
-let mk_rewrite_pattern1 eq pattern =
-  PApp (PRef eq, [| PMeta None; pattern; PMeta None |])
-
-let mk_rewrite_pattern2 eq pattern =
-  PApp (PRef eq, [| PMeta None; PMeta None; pattern |])
-
-let pattern_filter pat _ a c =
-  try 
-    try
-      is_matching pat (head c) 
-    with _ -> 
-      is_matching
-	pat (head (Typing.type_of (Global.env()) Evd.empty c))
-    with UserError _ -> 
-      false
-
-let filtered_search filter_function display_function ref =
-  crible ref
-    (fun s a c -> if filter_function s a c then display_function s a c) 
-
-let rec id_from_pattern = function
-  | PRef gr -> gr
-(* should be appear as a PRef (VarRef sp) !!
-  | PVar id -> Nametab.locate (make_qualid [] (string_of_id id))
- *)
-  | PApp (p,_) -> id_from_pattern p
-  | _ -> error "The pattern is not simple enough."
-	
-let raw_pattern_search extra_filter display_function pat =
-  let name = id_from_pattern pat in
-  filtered_search 
-    (fun s a c -> (pattern_filter pat s a c) & extra_filter s a c) 
-    display_function name
-
-let raw_search_rewrite extra_filter display_function pattern =
-  filtered_search
-    (fun s a c ->
-       ((pattern_filter (mk_rewrite_pattern1 gref_eq pattern) s a c) ||
-        (pattern_filter (mk_rewrite_pattern2 gref_eq pattern) s a c)) 
-       && extra_filter s a c)
-    display_function gref_eq
-
-let text_pattern_search extra_filter =
-  raw_pattern_search extra_filter plain_display
-    
-let text_search_rewrite extra_filter =
-  raw_search_rewrite extra_filter plain_display
-
-let filter_by_module_from_list = function
-  | [], _ -> (fun _ _ _ -> true)
-  | l, outside -> filter_by_module l (not outside)
-
-let search_by_head ref inout = 
-  filtered_search (filter_by_module_from_list inout) plain_display ref
-
-let search_rewrite pat inout =
-  text_search_rewrite (filter_by_module_from_list inout) pat
-
-let search_pattern pat inout =
-  text_pattern_search (filter_by_module_from_list inout) pat
-
-
-let gen_filtered_search filter_function display_function =
-  gen_crible None
-    (fun s a c -> if filter_function s a c then display_function s a c) 
-
-(** SearchAbout *)
-
-let name_of_reference ref = string_of_id (id_of_global ref)
-
-type glob_search_about_item =
-  | GlobSearchSubPattern of constr_pattern
-  | GlobSearchString of string
-
-let search_about_item (itemref,typ) = function
-  | GlobSearchSubPattern pat -> is_matching_appsubterm ~closed:false pat typ
-  | GlobSearchString s -> string_string_contains (name_of_reference itemref) s
-
-let raw_search_about filter_modules display_function l =
-  let filter ref' env typ =
-    filter_modules ref' env typ &&
-    List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l && 
-    not (string_string_contains (name_of_reference ref') "_subproof")
-  in
-  gen_filtered_search filter display_function
-
-let search_about ref inout = 
-  raw_search_about (filter_by_module_from_list inout) plain_display ref
diff --git a/parsing/search.mli b/parsing/search.mli
deleted file mode 100644
index fc2ea925fe..0000000000
--- a/parsing/search.mli
+++ /dev/null
@@ -1,50 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-open Pp
-open Names
-open Term
-open Environ
-open Pattern
-open Libnames
-open Nametab
-
-(*s Search facilities. *)
-
-type glob_search_about_item =
-  | GlobSearchSubPattern of constr_pattern
-  | GlobSearchString of string
-
-val search_by_head : global_reference -> dir_path list * bool -> unit
-val search_rewrite : constr_pattern -> dir_path list * bool -> unit
-val search_pattern : constr_pattern -> dir_path list * bool -> unit
-val search_about : 
-  (bool * glob_search_about_item) list -> dir_path list * bool -> unit
-
-(* The filtering function that is by standard search facilities.
-   It can be passed as argument to the raw search functions.
-   It is used in pcoq. *)
-
-val filter_by_module_from_list :
-  dir_path list * bool -> global_reference -> env -> 'a -> bool
-
-(* raw search functions can be used for various extensions.
-   They are also used for pcoq. *)
-val gen_filtered_search : (global_reference -> env -> constr -> bool) ->
-      (global_reference -> env -> constr -> unit) -> unit
-val filtered_search : (global_reference -> env -> constr -> bool) -> 
-  (global_reference -> env -> constr -> unit) -> global_reference -> unit
-val raw_pattern_search : (global_reference -> env -> constr -> bool) ->
-  (global_reference -> env -> constr -> unit) -> constr_pattern -> unit
-val raw_search_rewrite : (global_reference -> env -> constr -> bool) ->
-  (global_reference -> env -> constr -> unit) -> constr_pattern -> unit
-val raw_search_about : (global_reference -> env -> constr -> bool) ->
-  (global_reference -> env -> constr -> unit) -> 
-      (bool * glob_search_about_item) list -> unit