diff options
author | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-17 12:41:35 +0000 |
---|---|---|
committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-17 12:41:35 +0000 |
commit | bf9379dc09f413fab73464aaaef32f7d3d6975f2 (patch) | |
tree | 16d7e7fc47fd9838a6d15eef9c85a8c086f98eac /library | |
parent | 925e99db4166a97056e0ab3c314b452e1f2559cb (diff) |
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
Diffstat (limited to 'library')
-rw-r--r-- | library/declare.ml | 23 | ||||
-rw-r--r-- | library/declare.mli | 3 | ||||
-rw-r--r-- | library/declaremods.ml | 3 | ||||
-rw-r--r-- | library/declaremods.mli | 2 |
4 files changed, 23 insertions, 8 deletions
diff --git a/library/declare.ml b/library/declare.ml index 0fc9772da..2a4b2e403 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -39,6 +39,9 @@ let set_xml_declare_variable f = xml_declare_variable := if_xml f let set_xml_declare_constant f = xml_declare_constant := if_xml f let set_xml_declare_inductive f = xml_declare_inductive := if_xml f +let cache_hook = ref ignore +let add_cache_hook f = cache_hook := f + (** Declaration of section variables and local definitions *) type section_variable_entry = @@ -87,6 +90,7 @@ let declare_variable id obj = !xml_declare_variable oname; oname + (** Declaration of constants and parameters *) type constant_declaration = constant_entry * logical_kind @@ -114,7 +118,8 @@ let cache_constant ((sp,kn),(cdt,dhyps,kind)) = Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); add_section_constant kn' (Global.lookup_constant kn').const_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; - add_constant_kind (constant_of_kn kn) kind + add_constant_kind (constant_of_kn kn) kind; + !cache_hook sp let discharged_hyps kn sechyps = let (_,dir,_) = repr_kn kn in @@ -160,11 +165,11 @@ let hcons_constant_declaration = function let declare_constant_common id dhyps (cd,kind) = let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in - let kn = constant_of_kn kn in - declare_constant_implicits kn; - Heads.declare_head (EvalConstRef kn); - Notation.declare_ref_arguments_scope (ConstRef kn); - kn + let c = constant_of_kn kn in + declare_constant_implicits c; + Heads.declare_head (EvalConstRef c); + Notation.declare_ref_arguments_scope (ConstRef c); + c let declare_constant_gen internal id (cd,kind) = let cd = hcons_constant_declaration cd in @@ -215,7 +220,7 @@ let check_exists_inductive (sp,_) = let load_inductive i ((sp,kn),(_,mie)) = let names = inductive_names sp kn mie in List.iter check_exists_inductive names; - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref) names + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names let open_inductive i ((sp,kn),(_,mie)) = let names = inductive_names sp kn mie in @@ -230,7 +235,9 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = assert (kn'=kn); add_section_kn kn (Global.lookup_mind kn').mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names; + List.iter (fun (sp,_) -> !cache_hook sp) (inductive_names sp kn mie) + let discharge_inductive ((sp,kn),(dhyps,mie)) = let mie = Global.lookup_mind kn in diff --git a/library/declare.mli b/library/declare.mli index 93c8b9f91..38b1fa7b2 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -63,3 +63,6 @@ val declare_mind : bool -> mutual_inductive_entry -> object_name val set_xml_declare_variable : (object_name -> unit) -> unit val set_xml_declare_constant : (bool * constant -> unit) -> unit val set_xml_declare_inductive : (bool * object_name -> unit) -> unit + +(* hook for the cache function of constants and inductives *) +val add_cache_hook : (section_path -> unit) -> unit diff --git a/library/declaremods.ml b/library/declaremods.ml index 76487af68..16f9c9491 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -824,8 +824,11 @@ let start_library dir = Lib.start_compilation dir mp; Lib.add_frozen_state () +let end_library_hook = ref ignore +let set_end_library_hook f = end_library_hook := f let end_library dir = + !end_library_hook(); let prefix, lib_stack = Lib.end_compilation dir in let cenv = Global.export dir in let msid = msid_of_prefix prefix in diff --git a/library/declaremods.mli b/library/declaremods.mli index 1f7f6ada0..322078e9b 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -82,6 +82,8 @@ val start_library : library_name -> unit val end_library : library_name -> Safe_typing.compiled_library * library_objects +(* set a function to be executed at end_library *) +val set_end_library_hook : (unit -> unit) -> unit (* [really_import_module mp] opens the module [mp] (in a Caml sense). It modifies Nametab and performs the [open_object] function for |