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, 316 insertions, 0 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
new file mode 100644
index 0000000000..8a9646a174
--- /dev/null
+++ b/toplevel/autoinstance.ml
@@ -0,0 +1,316 @@
+(************************************************************************)
+(*  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 Pp
+open Printer
+open Names
+open Term
+open Evd
+open Sign
+open Libnames
+(*i*)
+
+(*s 
+ * Automatic detection of (some) record instances
+ *)
+
+(* Datatype for wannabe-instances: a signature is a typeclass along
+   with the collection of evars corresponding to the parameters/fields
+   of the class. Each evar can be uninstantiated (we're still looking
+   for them) or defined (the instance for the field is fixed) *)
+type signature = global_reference * evar list * evar_map
+
+type instance_decl_function = global_reference -> rel_context -> constr list -> unit
+
+(* 
+ * Search algorithm
+ *) 
+
+let rec subst_evar evar def n c = 
+  match kind_of_term c with
+    | Evar (e,_) when e=evar -> lift n def
+    | _ -> map_constr_with_binders (fun n->n+1) (subst_evar evar def) n c
+
+let subst_evar_in_evm evar def evm = 
+  Evd.fold
+    (fun ev evi acc -> 
+       let evar_body = match evi.evar_body with 
+	 | Evd.Evar_empty -> Evd.Evar_empty
+	 | Evd.Evar_defined c -> Evd.Evar_defined (subst_evar evar def 0 c) in
+       let evar_concl = subst_evar evar def 0 evi.evar_concl in
+       Evd.add acc ev {evi with evar_body=evar_body; evar_concl=evar_concl}
+    ) evm empty
+    
+(* Tries to define ev by c in evd. Fails if ev := c1 and c1 /= c ev :
+ * T1, c : T2 and T1 /= T2. Defines recursively all evars instantiated
+ * by this definition. *)
+
+let rec safe_evar_define evm ev c =
+  if not (closedn (-1) c) then raise Termops.CannotFilter else
+(*  msgnl(str"safe_evar_define "++pr_evar_map evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*)
+  let evi = (Evd.find evm ev) in
+  let define_subst evm sigma =
+    Util.Intmap.fold
+      ( fun ev (e,c) evm -> 
+	  match kind_of_term c with Evar (i,_) when i=ev -> evm | _ ->
+	    safe_evar_define evm ev (lift (-List.length e) c)
+      ) sigma evm in
+  match evi.evar_body with
+    | Evd.Evar_defined def ->
+	define_subst evm (Termops.filtering [] Reduction.CUMUL def c)
+    | Evd.Evar_empty ->
+	let t = Libtypes.reduce (Typing.type_of (Global.env()) evm c) in
+	let u = Libtypes.reduce (evar_concl evi) in
+	let evm = subst_evar_in_evm ev c evm in
+	define_subst (Evd.define evm ev c) (Termops.filtering [] Reduction.CUMUL t u)
+
+let add_gen_ctx (cl,gen,evm) ctx : signature * constr list = 
+  let rec really_new_evar () =
+    let ev = Evarutil.new_untyped_evar() in
+    if Evd.is_evar evm ev then really_new_evar() else ev in
+  let add_gen_evar (cl,gen,evm) ev ty : signature =
+    let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val ty) in
+    (cl,ev::gen,evm) in
+  let rec mksubst b = function
+    | [] -> []
+    | a::tl -> b::(mksubst (a::b) tl) in
+  let evl = List.map (fun _ -> really_new_evar()) ctx in
+  let evcl = List.map (fun i -> mkEvar (i,[||])) evl in
+  let substl = List.rev (mksubst [] (evcl)) in
+  let ctx = List.map2 (fun s t -> substnl s 0 t) substl ctx in
+  let sign = List.fold_left2 add_gen_evar (cl,gen,evm) (List.rev evl) ctx in
+  sign,evcl
+
+(* TODO : for full proof-irrelevance in the search, provide a real
+   compare function for constr instead of Pervasive's one! *)
+module SubstSet : Set.S with type elt = Termops.subst
+  = Set.Make (struct type t = Termops.subst
+		     let compare = Util.Intmap.compare (Pervasives.compare)
+	      end)
+
+(* searches instatiations in the library for just one evar [ev] of a
+   signature. [k] is called on each resulting signature *)
+let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) =
+  let ev_typ = Libtypes.reduce (evar_concl evi) in
+  let sort_is_prop = is_Prop (Typing.type_of (Global.env()) evm (evar_concl evi)) in
+(*  msgnl(str"cherche "++pr_constr ev_typ++str" pour "++Util.pr_int ev);*)
+  let substs = ref SubstSet.empty in
+  try List.iter
+    ( fun (gr,(pat,_),s) -> 
+	let (_,genl,_) = Termops.decompose_prod_letin pat in
+	let genl = List.map (fun (_,_,t) -> t) genl in
+	let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) genl in
+	let def = applistc (Libnames.constr_of_global gr) argl in
+(*	msgnl(str"essayons  ?"++Util.pr_int ev++spc()++str":="++spc()
+	      ++pr_constr def++spc()++str":"++spc()++pr_constr (Global.type_of_global gr)*)
+	(*++spc()++str"dans"++spc()++pr_evar_map evm++spc());*)
+	try
+ 	  let evm = safe_evar_define evm ev def in
+	  k (cl,gen,evm);
+	  if sort_is_prop && SubstSet.mem s !substs then raise Exit;
+	  substs := SubstSet.add s !substs
+	with Termops.CannotFilter -> ()
+    ) (Libtypes.search_concl ev_typ)
+  with Exit -> ()
+
+let evm_fold_rev f evm acc =
+  let l = Evd.fold (fun ev evi acc -> (ev,evi)::acc) evm [] in
+  List.fold_left (fun acc (ev,evi) -> f ev evi acc) acc l
+
+exception Continue of Evd.evar * Evd.evar_info
+
+(* searches matches for all the uninstantiated evars of evd in the
+   context. For each totally instantiated evar_map found, apply
+   k. *)
+let rec complete_signature (k:signature -> unit) (cl,gen,evm:signature) =
+  try
+    evm_fold_rev
+      ( fun ev evi _ ->
+	  if not (is_defined evm ev) && not (List.mem ev gen) then
+	    raise (Continue (ev,evi))
+      ) evm (); k (cl,gen,evm)
+  with Continue (ev,evi) -> complete_evar (cl,gen,evm) (ev,evi) (complete_signature k)
+
+(* define all permutations of the evars to evd and call k on the
+   resulting evd *)
+let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit) : unit =
+  let rec aux evm = List.iter
+    ( fun (ctx,ev) ->
+	let tyl = List.map (fun (_,_,t) -> t) ctx in
+	let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) tyl in
+	let def = applistc c argl in	
+(*	msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*)
+	try
+	  if not (Evd.is_defined evm ev) then
+	    let evm = safe_evar_define evm ev def in
+	    aux evm; k (cl,gen,evm)
+	with Termops.CannotFilter -> ()
+    ) evl in
+  aux evm
+    
+let new_inst_no = 
+  let cnt = ref 0 in
+  fun () -> incr cnt; string_of_int !cnt
+
+let make_instance_ident gr =
+  Nameops.add_suffix (Nametab.id_of_global gr) ("_autoinstance_"^new_inst_no())
+
+let new_instance_message ident typ def =
+  Flags.if_verbose
+  msgnl (str"new instance"++spc()
+	 ++Nameops.pr_id ident++spc()++str":"++spc()
+	 ++pr_constr typ++spc()++str":="++spc()
+	 ++pr_constr def)
+
+open Entries
+
+let rec deep_refresh_universes c = 
+  match kind_of_term c with
+    | Sort (Type _) -> Termops.new_Type()
+    | _ -> map_constr deep_refresh_universes c
+
+let declare_record_instance gr ctx params =
+  let ident = make_instance_ident gr in
+  let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in
+  let def = deep_refresh_universes def in
+  let ce = { const_entry_body=def; const_entry_type=None;
+	     const_entry_opaque=false; const_entry_boxed=false } in 
+  let cst = Declare.declare_constant ident 
+    (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in
+  new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def
+
+let declare_class_instance gr ctx params = 
+  let ident = make_instance_ident gr in
+  let cl = Typeclasses.class_info gr in
+  let (def,typ) = Typeclasses.instance_constructor cl params in
+  let (def,typ) = it_mkLambda_or_LetIn def ctx, it_mkProd_or_LetIn typ ctx in
+  let def = deep_refresh_universes def in
+  let typ = deep_refresh_universes typ in
+  let ce = Entries.DefinitionEntry 
+    {  const_entry_type=Some typ; const_entry_body=def;
+       const_entry_opaque=false; const_entry_boxed=false } in 
+  try
+  let cst = Declare.declare_constant ident 
+    (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in
+  Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true cst);
+  new_instance_message ident typ def
+  with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str"  "++Cerrors.explain_exn e)
+
+let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ctx t;
+  match kind_of_term t with
+    | Prod (n,t,c) -> iter_under_prod f ((n,None,t)::ctx) c
+    | _ -> ()
+
+(* main search function: search for total instances containing gr, and
+   apply k to each of them *)
+let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature -> unit) : unit =
+  let gr_c = Libnames.constr_of_global gr in
+  let (smap:(Libnames.global_reference * Evd.evar_map,
+   ('a * 'b * Term.constr) list * Evd.evar)
+  Gmapl.t ref) = ref Gmapl.empty in
+  iter_under_prod
+    ( fun ctx typ -> 
+	List.iter
+	  (fun ((cl,ev,evm),_,_) -> 
+(*	     msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_map evm);*)
+	     smap := Gmapl.add (cl,evm) (ctx,ev) !smap)
+	  (Recordops.methods_matching typ)
+    ) [] deftyp;
+  Gmapl.iter 
+    ( fun (cl,evm) evl -> 
+	let f = if Typeclasses.is_class cl then 
+	  declare_class_instance else declare_record_instance in
+	complete_with_evars_permut (cl,[],evm) evl gr_c
+	  (fun sign -> complete_signature (k f) sign)
+    ) !smap
+
+(*
+ * Interface with other parts: hooks & declaration
+ *)
+
+
+let evar_definition evi = match evar_body evi with
+    Evar_empty -> assert false | Evar_defined c -> c
+ 
+let gen_sort_topo l evm = 
+  let iter_evar f ev =
+    let rec aux c = match kind_of_term c with
+	Evar (e,_) -> f e
+      | _ -> iter_constr aux c in
+    aux (Evd.evar_concl (Evd.find evm ev));
+    if Evd.is_defined evm ev then aux (evar_definition (Evd.find evm ev)) in
+  let r = ref [] in 
+  let rec dfs ev = iter_evar dfs ev;
+    if not(List.mem ev !r) then r := ev::!r in
+  List.iter dfs l; List.rev !r
+
+(* register real typeclass instance given a totally defined evd *)
+let declare_instance (k:global_reference -> rel_context -> constr list -> unit)
+    (cl,gen,evm:signature) =
+  let evm = Evarutil.nf_evars evm in
+  let gen = gen_sort_topo gen evm in
+  let (evm,gen) = List.fold_right
+    (fun ev (evm,gen) -> 
+       if Evd.is_defined evm ev 
+       then Evd.remove evm ev,gen 
+       else evm,(ev::gen))
+    gen (evm,[]) in
+(*  msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_map evm);*)
+  let ngen = List.length gen in
+  let (_,ctx,evm) = List.fold_left
+    ( fun (i,ctx,evm) ev -> 
+	let ctx = (Anonymous,None,lift (-i) (Evd.evar_concl(Evd.find evm ev)))::ctx in
+	let evm = subst_evar_in_evm ev (mkRel i) (Evd.remove evm ev) in
+	(i-1,ctx,evm)
+    ) (ngen,[],evm) gen in
+  let fields = List.rev (Evd.fold ( fun ev evi l -> evar_definition evi::l ) evm []) in
+  k cl ctx fields
+
+let autoinstance_opt = ref true
+
+let search_declaration gr =
+  if !autoinstance_opt && 
+    not (Lib.is_modtype()) then
+    let deftyp = Global.type_of_global gr in
+    complete_signature_with_def gr deftyp declare_instance
+
+let search_record k cons sign =
+  if !autoinstance_opt && not (Lib.is_modtype()) then
+    complete_signature (declare_instance k) (cons,[],sign)
+
+(*
+let dh_key = Profile.declare_profile "declaration_hook"
+let ch_key = Profile.declare_profile "class_decl_hook"
+let declaration_hook = Profile.profile1 dh_key declaration_hook
+let class_decl_hook = Profile.profile1 ch_key class_decl_hook
+*)
+
+(*
+ *  Options and bookeeping
+ *)
+
+let begin_autoinstance () =
+  if not !autoinstance_opt then (
+    autoinstance_opt := true;
+  )
+    
+let end_autoinstance () =
+  if !autoinstance_opt then (
+    autoinstance_opt := false;
+ )
+
+let _ =
+  Goptions.declare_bool_option
+    { Goptions.optsync=true;
+      Goptions.optkey=Goptions.PrimaryTable("Autoinstance");
+      Goptions.optname="automatic typeclass instance recognition";
+      Goptions.optread=(fun () -> !autoinstance_opt);
+      Goptions.optwrite=(fun b -> if b then begin_autoinstance() else end_autoinstance()) }