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

6 files changed, 13 insertions, 13 deletions

diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 67ae85d648..f0e5c6256c 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1375,7 +1375,7 @@ let do_build_inductive
 	in
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,repacked_rel_inds))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1390,7 +1390,7 @@ let do_build_inductive
 	in
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,repacked_rel_inds)) 
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,repacked_rel_inds)) 
 	    ++ fnl () ++
 	    Cerrors.explain_exn e
 	in
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 2eb2c38126..c2035586fb 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -164,7 +164,7 @@ and ct_COMMAND =
   | CT_resume of ct_ID_OPT
   | CT_save of ct_THM_OPT * ct_ID_OPT
   | CT_scomments of ct_SCOMMENT_CONTENT_LIST
-  | CT_search of ct_ID * ct_IN_OR_OUT_MODULES
+  | CT_search of ct_FORMULA * ct_IN_OR_OUT_MODULES
   | CT_search_about of ct_ID_OR_STRING_NE_LIST * ct_IN_OR_OUT_MODULES
   | CT_search_pattern of ct_FORMULA * ct_IN_OR_OUT_MODULES
   | CT_search_rewrite of ct_FORMULA * ct_IN_OR_OUT_MODULES
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 51dce4f766..79fa912a66 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -565,14 +565,14 @@ let pcoq_search s l =
       raw_search_about (filter_by_module_from_list l) add_search
 	(List.map (on_snd interp_search_about_item) sl)
   | SearchPattern c ->
-      let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
+      let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
       raw_pattern_search (filter_by_module_from_list l) add_search pat
   | SearchRewrite c ->
-      let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
+      let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
       raw_search_rewrite (filter_by_module_from_list l) add_search pat;
-  | SearchHead locqid ->
-      filtered_search
-	(filter_by_module_from_list l) add_search (Nametab.global locqid)
+  | SearchHead c ->
+      let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
+      raw_search_by_head (filter_by_module_from_list l) add_search pat;
   end;
   search_output_results()
 
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index d6ef1ea3b6..5180bdad27 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -121,7 +121,7 @@ let mutual_to_ast_list sp mib =
   let _, l =
     Array.fold_right
       (fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in
-  VernacInductive (mib.mind_finite, l)
+  VernacInductive (mib.mind_finite, false, l)
   :: (implicit_args_to_ast_list sp mipv);;
 
 let constr_to_ast v = 
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 946090099e..b9daf63574 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -530,7 +530,7 @@ and fCOMMAND = function
    fSCOMMENT_CONTENT_LIST x1 ++
    fNODE "scomments" 1
 | CT_search(x1, x2) ->
-   fID x1 ++
+   fFORMULA x1 ++
    fIN_OR_OUT_MODULES x2 ++
    fNODE "search" 2
 | CT_search_about(x1, x2) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ee48ee53b7..6b65fbcc5f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1950,8 +1950,8 @@ let rec xlate_vernac =
       (match s with
 	| SearchPattern c ->
 	    CT_search_pattern(xlate_formula c, translated_restriction)
-	| SearchHead id ->
-	    CT_search(loc_qualid_to_ct_ID id, translated_restriction)
+	| SearchHead c ->
+	    CT_search(xlate_formula c, translated_restriction)
 	| SearchRewrite c ->
 	    CT_search_rewrite(xlate_formula c, translated_restriction)
 	| SearchAbout (a::l) ->
@@ -1984,7 +1984,7 @@ let rec xlate_vernac =
 (*         xlate_ident s, xlate_binder_list binders,  *)
 (* 	xlate_formula (Option.get c1), record_constructor, *)
 (*          build_record_field_list field_list) *)
-   | VernacInductive (isind, lmi) ->
+   | VernacInductive (isind, _, lmi) ->
       let co_or_ind = if isind then "Inductive" else "CoInductive" in
       let strip_mutind = function
           (((_, (_,s)), parameters, c, _, Constructors constructors), notopt) ->