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 | |
| 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
43 files changed, 1742 insertions, 109 deletions
diff --git a/Makefile.common b/Makefile.common index 7ff2c6b05..debec248a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -133,7 +133,7 @@ LIBREP:=\ lib/util.cmo lib/bigint.cmo lib/hashcons.cmo lib/dyn.cmo lib/system.cmo \ lib/envars.cmo lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \ lib/tlm.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \ - lib/predicate.cmo lib/rtree.cmo lib/heap.cmo lib/option.cmo + lib/predicate.cmo lib/rtree.cmo lib/heap.cmo lib/option.cmo lib/dnet.cmo # Rem: Cygwin already uses variable LIB BYTERUN:=\ @@ -159,7 +159,8 @@ KERNEL:=\ LIBRARY:=\ library/nameops.cmo library/libnames.cmo library/libobject.cmo \ library/summary.cmo library/nametab.cmo library/global.cmo library/lib.cmo \ - library/declaremods.cmo library/library.cmo library/states.cmo \ + library/declaremods.cmo library/library.cmo \ + library/states.cmo \ library/decl_kinds.cmo library/dischargedhypsmap.cmo library/goptions.cmo \ library/decls.cmo library/heads.cmo @@ -167,8 +168,10 @@ PRETYPING:=\ pretyping/termops.cmo pretyping/evd.cmo \ pretyping/reductionops.cmo pretyping/vnorm.cmo pretyping/inductiveops.cmo \ pretyping/retyping.cmo pretyping/cbv.cmo \ - pretyping/pretype_errors.cmo pretyping/recordops.cmo pretyping/typing.cmo \ - pretyping/tacred.cmo pretyping/evarutil.cmo pretyping/evarconv.cmo \ + pretyping/pretype_errors.cmo \ + pretyping/typing.cmo pretyping/evarutil.cmo pretyping/term_dnet.cmo \ + pretyping/recordops.cmo \ + pretyping/tacred.cmo pretyping/evarconv.cmo \ pretyping/typeclasses_errors.cmo pretyping/typeclasses.cmo \ pretyping/classops.cmo pretyping/coercion.cmo \ pretyping/unification.cmo pretyping/clenv.cmo \ @@ -196,7 +199,7 @@ PARSING:=\ parsing/pcoq.cmo parsing/egrammar.cmo parsing/g_xml.cmo \ parsing/ppconstr.cmo parsing/printer.cmo \ parsing/pptactic.cmo parsing/ppdecl_proof.cmo parsing/tactic_printer.cmo \ - parsing/printmod.cmo parsing/prettyp.cmo parsing/search.cmo + parsing/printmod.cmo parsing/prettyp.cmo HIGHPARSING:=\ parsing/g_constr.cmo parsing/g_vernac.cmo parsing/g_prim.cmo \ @@ -221,8 +224,8 @@ TACTICS:=\ TOPLEVEL:=\ toplevel/himsg.cmo toplevel/cerrors.cmo \ toplevel/class.cmo toplevel/vernacexpr.cmo toplevel/metasyntax.cmo \ - toplevel/auto_ind_decl.cmo \ - toplevel/command.cmo toplevel/record.cmo \ + toplevel/auto_ind_decl.cmo toplevel/libtypes.cmo toplevel/search.cmo \ + toplevel/autoinstance.cmo toplevel/command.cmo toplevel/record.cmo \ parsing/ppvernac.cmo toplevel/classes.cmo \ toplevel/vernacinterp.cmo toplevel/mltop.cmo \ toplevel/vernacentries.cmo toplevel/whelp.cmo toplevel/vernac.cmo \ @@ -525,10 +528,11 @@ PRINTERSCMO:=\ library/libnames.cmo library/nametab.cmo library/libobject.cmo \ library/lib.cmo library/goptions.cmo library/decls.cmo library/heads.cmo \ pretyping/termops.cmo pretyping/evd.cmo pretyping/rawterm.cmo \ - pretyping/reductionops.cmo pretyping/inductiveops.cmo \ - pretyping/retyping.cmo pretyping/cbv.cmo \ - pretyping/pretype_errors.cmo pretyping/recordops.cmo pretyping/typing.cmo \ - pretyping/evarutil.cmo pretyping/evarconv.cmo pretyping/tacred.cmo \ + pretyping/reductionops.cmo pretyping/inductiveops.cmo \ + pretyping/retyping.cmo pretyping/cbv.cmo \ + pretyping/pretype_errors.cmo pretyping/typing.cmo pretyping/evarutil.cmo \ + pretyping/term_dnet.cmo pretyping/recordops.cmo \ + pretyping/evarconv.cmo pretyping/tacred.cmo \ pretyping/classops.cmo pretyping/typeclasses_errors.cmo pretyping/typeclasses.cmo \ pretyping/detyping.cmo pretyping/indrec.cmo pretyping/coercion.cmo \ pretyping/unification.cmo pretyping/cases.cmo \ @@ -883,8 +887,7 @@ LIBRARYMLI:=$(wildcard $(LIBRARY:.cmo=.mli)) PARSINGMLI:=$(wildcard $(PARSING:.cmo=.mli) $(HIGHPARSING:.cmo=.mli)) TACTICSMLI:=$(wildcard $(TACTICS:.cmo=.mli) $(HIGHTACTICS:.cmo=.mli)) COQMLI:=$(KERNELMLI) $(INTERPMLI) $(PRETYPINGMLI) $(TOPLEVELMLI) $(PROOFSMLI) \ - $(LIBRARYMLI) $(PARSINGMLI) $(TACTICSMLI) - + $(LIBRARYMLI) $(PARSINGMLI) $(TACTICSMLI) ########################################################################### # Miscellaneous diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 67ae85d64..f0e5c6256 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 2eb2c3812..c2035586f 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 51dce4f76..79fa912a6 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 d6ef1ea3b..5180bdad2 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 946090099..b9daf6357 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 ee48ee53b..6b65fbcc5 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) -> diff --git a/ide/coq.ml b/ide/coq.ml index 69d8f680f..e58a1bd19 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -375,7 +375,7 @@ let compute_reset_info = function | VernacDefinition (_, (_,id), DefineBody _, _) | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_) - | VernacInductive (_, (((_,(_,id)),_,_,_,_),_) :: _) -> + | VernacInductive (_,_, (((_,(_,id)),_,_,_,_),_) :: _) -> ResetAtRegisteredObject (reset_mark id), undo_info(), ref true | com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 357ce4377..c658faa0f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1236,6 +1236,24 @@ let interp_casted_constr sigma env ?(impls=([],[])) c typ = let interp_open_constr sigma env c = Default.understand_tcc sigma env (intern_constr sigma env c) +let interp_open_constr_patvar sigma env c = + let raw = intern_gen false sigma env c ~allow_patvar:true in + let sigma = ref (Evd.create_evar_defs sigma) in + let evars = ref (Gmap.empty : (identifier,rawconstr) Gmap.t) in + let rec patvar_to_evar r = match r with + | RPatVar (loc,(_,id)) -> + ( try Gmap.find id !evars + with Not_found -> + let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in + let ev = Evarutil.e_new_evar sigma env ev in + let rev = REvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in + evars := Gmap.add id rev !evars; + rev + ) + | _ -> map_rawconstr patvar_to_evar r in + let raw = patvar_to_evar raw in + Default.understand_tcc (Evd.evars_of !sigma) env raw + let interp_constr_judgment sigma env c = Default.understand_judgment sigma env (intern_constr sigma env c) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 6410c9b2e..126eff859 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -87,6 +87,8 @@ val interp_type : evar_map -> env -> ?impls:full_implicits_env -> val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr +val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * constr + val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> constr_expr -> types -> constr diff --git a/lib/dnet.ml b/lib/dnet.ml new file mode 100644 index 000000000..b5a7bb728 --- /dev/null +++ b/lib/dnet.ml @@ -0,0 +1,240 @@ +(************************************************************************) +(* 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 dnet implementation over non-recursive types *) + +module type Datatype = +sig + type 'a t + val map : ('a -> 'b) -> 'a t -> 'b t + val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t + val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a + val fold2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a + val compare : unit t -> unit t -> int + val terminal : 'a t -> bool + val choose : ('a -> 'b) -> 'a t -> 'b +end + +module type S = +sig + type t + type ident + type meta + type 'a structure + module Idset : Set.S with type elt=ident + type 'a pattern = + | Term of 'a + | Meta of meta + type term_pattern = ('a structure) pattern as 'a + val empty : t + val add : t -> term_pattern -> ident -> t + val find_all : t -> Idset.t + val fold_pattern : + (meta -> t -> 'a -> 'a) -> 'a -> term_pattern -> t -> Idset.t option * 'a + val find_match : term_pattern -> t -> Idset.t + val inter : t -> t -> t + val union : t -> t -> t + val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t +end + +module Make = + functor (T:Datatype) -> + functor (Ident:Set.OrderedType) -> + functor (Meta:Set.OrderedType) -> +struct + + type ident = Ident.t + type meta = Meta.t + + type 'a pattern = + | Term of 'a + | Meta of meta + + type 'a structure = 'a T.t + + module Idset = Set.Make(Ident) + module Mmap = Map.Make(Meta) + module Tmap = Map.Make(struct type t = unit structure + let compare = T.compare end) + + type term_pattern = term_pattern structure pattern + type idset = Idset.t + + + + (* we store identifiers at the leaf of the dnet *) + type node = + | Node of t structure + | Terminal of t structure * idset + + (* at each node, we have a bunch of nodes (actually a map between + the bare node and a subnet) and a bunch of metavariables *) + and t = Nodes of node Tmap.t * idset Mmap.t + + let empty : t = Nodes (Tmap.empty, Mmap.empty) + + (* the head of a data is of type unit structure *) + let head w = T.map (fun c -> ()) w + + (* given a node of the net and a word, returns the subnet with the + same head as the word (with the rest of the nodes) *) + let split l (w:'a structure) : node * node Tmap.t = + let elt : node = Tmap.find (head w) l in + (elt, Tmap.remove (head w) l) + + let select l w = Tmap.find (head w) l + + let rec add (Nodes (t,m):t) (w:term_pattern) (id:ident) : t = + match w with Term w -> + ( try + let (n,tl) = split t w in + let new_node = match n with + | Terminal (e,is) -> Terminal (e,Idset.add id is) + | Node e -> Node (T.map2 (fun t p -> add t p id) e w) in + Nodes ((Tmap.add (head w) new_node tl), m) + with Not_found -> + let new_content = T.map (fun p -> add empty p id) w in + let new_node = + if T.terminal w then + Terminal (new_content, Idset.singleton id) + else Node new_content in + Nodes ((Tmap.add (head w) new_node t), m) ) + | Meta i -> + let m = + try Mmap.add i (Idset.add id (Mmap.find i m)) m + with Not_found -> Mmap.add i (Idset.singleton id) m in + Nodes (t, m) + + let add t w id = add t w id + + let rec find_all (Nodes (t,m)) : idset = + Idset.union + (Mmap.fold (fun _ -> Idset.union) m Idset.empty) + (Tmap.fold + ( fun _ n acc -> + let s2 = match n with + | Terminal (_,is) -> is + | Node e -> T.choose find_all e in + Idset.union acc s2 + ) t Idset.empty) + + exception Empty + + (* optimization hack: Not_found is catched in fold_pattern *) + let fast_inter s1 s2 = + if Idset.is_empty s1 || Idset.is_empty s2 then raise Empty + else Idset.inter s1 s2 + + let option_any2 f s1 s2 = match s1,s2 with + | Some s1, Some s2 -> f s1 s2 + | (Some s, _ | _, Some s) -> s + | _ -> raise Not_found + + let fold_pattern ?(complete=true) f acc pat dn = + let deferred = ref [] in + let leafs,metas = ref None, ref None in + let leaf s = leafs := match !leafs with + | None -> Some s + | Some s' -> Some (fast_inter s s') in + let meta s = metas := match !metas with + | None -> Some s + | Some s' -> Some (Idset.union s s') in + let defer c = deferred := c::!deferred in + let rec fp_rec (p:term_pattern) (Nodes(t,m) as dn:t) = + Mmap.iter (fun _ -> meta) m; (* TODO: gérer patterns nonlin ici *) + match p with + | Meta m -> defer (m,dn) + | Term w -> + try match select t w with + | Terminal (_,is) -> leaf is + | Node e -> + if complete then T.fold2 (fun _ -> fp_rec) () w e else + if T.fold2 + (fun b p dn -> match p with + | Term _ -> fp_rec p dn; false + | Meta _ -> b + ) true w e + then T.choose (T.choose fp_rec w) e + with Not_found -> + if Mmap.is_empty m then raise Not_found else () + in try + fp_rec pat dn; + (try Some (option_any2 Idset.union !leafs !metas) with Not_found -> None), + List.fold_left (fun acc (m,dn) -> f m dn acc) acc !deferred + with Not_found | Empty -> None,acc + + (* intersection of two dnets. keep only the common pairs *) + let rec inter (t1:t) (t2:t) : t = + let inter_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t = + Nodes + (Tmap.fold + ( fun k e acc -> + try Tmap.add k (f e (Tmap.find k t2)) acc + with Not_found -> acc + ) t1 Tmap.empty, + Mmap.fold + ( fun m s acc -> + try Mmap.add m (Idset.inter s (Mmap.find m m2)) acc + with Not_found -> acc + ) m1 Mmap.empty + ) in + inter_map + (fun n1 n2 -> match n1,n2 with + | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.inter s1 s2) + | Node e1, Node e2 -> Node (T.map2 inter e1 e2) + | _ -> assert false + ) t1 t2 + + let rec union (t1:t) (t2:t) : t = + let union_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t = + Nodes + (Tmap.fold + ( fun k e acc -> + try Tmap.add k (f e (Tmap.find k acc)) acc + with Not_found -> Tmap.add k e acc + ) t1 t2, + Mmap.fold + ( fun m s acc -> + try Mmap.add m (Idset.inter s (Mmap.find m acc)) acc + with Not_found -> Mmap.add m s acc + ) m1 m2 + ) in + union_map + (fun n1 n2 -> match n1,n2 with + | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.union s1 s2) + | Node e1, Node e2 -> Node (T.map2 union e1 e2) + | _ -> assert false + ) t1 t2 + + let find_match (p:term_pattern) (t:t) : idset = + let metas = ref Mmap.empty in + let (mset,lset) = fold_pattern ~complete:false + (fun m t acc -> +(* Printf.printf "eval pat %d\n" (Obj.magic m:int);*) + Some (option_any2 fast_inter acc + (Some(let t = try inter t (Mmap.find m !metas) with Not_found -> t in + metas := Mmap.add m t !metas; + find_all t))) + ) None p t in + try option_any2 Idset.inter mset lset + with Not_found -> Idset.empty + + let fold_pattern f acc p dn = fold_pattern ~complete:true f acc p dn + + let idset_map f is = Idset.fold (fun e acc -> Idset.add (f e) acc) is Idset.empty + let tmap_map f g m = Tmap.fold (fun k e acc -> Tmap.add (f k) (g e) acc) m Tmap.empty + + let rec map sidset sterm (Nodes (t,m)) : t = + let snode = function + | Terminal (e,is) -> Terminal (e,idset_map sidset is) + | Node e -> Node (T.map (map sidset sterm) e) in + Nodes (tmap_map sterm snode t, Mmap.map (idset_map sidset) m) + +end diff --git a/lib/dnet.mli b/lib/dnet.mli new file mode 100644 index 000000000..a01bbb0e2 --- /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 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 diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml index 3218781d1..4a5972cc7 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 6b1faa76c..a936485d9 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 4b79113f3..3a88a09f8 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 790b5c363..31fd4561e 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 df4eee8aa..113b2f040 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/pretyping/evarutil.ml b/pretyping/evarutil.ml index 6ac857d5c..dab5c7987 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -71,7 +71,10 @@ let nf_env_evar sigma env = let nf_evar_info evc info = { info with evar_concl = Reductionops.nf_evar evc info.evar_concl; - evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps} + evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps; + evar_body = match info.evar_body with + | Evar_empty -> Evar_empty + | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) } let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi)) evm Evd.empty diff --git a/pretyping/evd.ml b/pretyping/evd.ml index b29afc0cb..a76df2dfb 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -421,11 +421,27 @@ type evar_defs = history : (existential_key * (loc * hole_kind)) list; metas : clbinding Metamap.t } +let subst_named_context_val s = map_named_val (subst_mps s) + +let subst_evar_info s evi = + let subst_evb = function Evar_empty -> Evar_empty + | Evar_defined c -> Evar_defined (subst_mps s c) in + { evi with + evar_concl = subst_mps s evi.evar_concl; + evar_hyps = subst_named_context_val s evi.evar_hyps; + evar_body = subst_evb evi.evar_body } + +let subst_evar_map sub evm = + assert (snd evm = UniverseMap.empty); + Evarmap.map (subst_evar_info sub) (fst evm), snd evm + let subst_evar_defs_light sub evd = - assert (evd.evars = (Evarmap.empty,UniverseMap.empty)); + assert (snd evd.evars = UniverseMap.empty); assert (evd.conv_pbs = []); { evd with - metas = Metamap.map (map_clb (subst_mps sub)) evd.metas } + metas = Metamap.map (map_clb (subst_mps sub)) evd.metas; + evars = Evarmap.map (subst_evar_info sub) (fst evd.evars), snd evd.evars + } let create_evar_defs sigma = { evars=sigma; conv_pbs=[]; last_mods = []; history=[]; metas=Metamap.empty } @@ -715,6 +731,7 @@ let pr_evar_defs evd = if evd.evars = empty then mt() else str"EVARS:"++brk(0,1)++pr_evar_map evd.evars++fnl() in let cstrs = + if evd.conv_pbs = [] then mt() else str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in let pp_met = if evd.metas = Metamap.empty then mt() else diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 825096acc..0e3212813 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -156,7 +156,8 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding (* Unification state *) type evar_defs -(* Assume empty [evar_map] and [conv_pbs] *) +val subst_evar_map : substitution -> evar_map -> evar_map +(* Assume empty universe constraints in [evar_map] and [conv_pbs] *) val subst_evar_defs_light : substitution -> evar_defs -> evar_defs (* create an [evar_defs] with empty meta map: *) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index e8860c065..b6749db19 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -93,6 +93,58 @@ let find_projection = function | ConstRef cst -> Cmap.find cst !projection_table | _ -> raise Not_found +(* Management of a field store : each field + argument of the inferred + * records are stored in a discrimination tree *) + +let subst_id s (gr,ev,evm) = + (fst(subst_global s gr),ev,Evd.subst_evar_map s evm) + +module MethodsDnet : Term_dnet.S + with type ident = global_reference * Evd.evar * Evd.evar_map + = Term_dnet.Make + (struct + type t = global_reference * Evd.evar * Evd.evar_map + let compare = Pervasives.compare + let subst = subst_id + let constr_of (_,ev,evm) = Evd.evar_concl (Evd.find evm ev) + end) + (struct + let reduce c = Reductionops.head_unfold_under_prod + Names.full_transparent_state (Global.env()) Evd.empty c + let direction = true + end) + +let meth_dnet = ref MethodsDnet.empty + +open Summary + +let _ = + declare_summary "record-methods-state" + { freeze_function = (fun () -> !meth_dnet); + unfreeze_function = (fun m -> meth_dnet := m); + init_function = (fun () -> meth_dnet := MethodsDnet.empty); + survive_module = false; + survive_section = false } + +open Libobject + +let load_method (_,(ty,id)) = + meth_dnet := MethodsDnet.add ty id !meth_dnet + +let (in_method,out_method) = + declare_object + { (default_object "RECMETHODS") with + load_function = (fun _ -> load_method); + cache_function = load_method; + subst_function = (fun (_,s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id); + export_function = (fun x -> Some x); + classify_function = (fun (_,x) -> Substitute x) + } + +let methods_matching c = MethodsDnet.search_pattern !meth_dnet c + +let declare_method cons ev sign = + Lib.add_anonymous_leaf (in_method ((Evd.evar_concl (Evd.find sign ev)),(cons,ev,sign))) (************************************************************************) (*s A canonical structure declares "canonical" conversion hints between *) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 638cc4304..4d28ee55b 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -41,6 +41,15 @@ val find_projection_nparams : global_reference -> int (* raise [Not_found] if not a projection *) val find_projection : global_reference -> struc_typ +(* we keep an index (dnet) of record's arguments + fields + (=methods). Here is how to declare them: *) +val declare_method : + global_reference -> Evd.evar -> Evd.evar_map -> unit + (* and here is how to search for methods matched by a given term: *) +val methods_matching : constr -> + ((global_reference*Evd.evar*Evd.evar_map) * + (constr*existential_key)*Termops.subst) list + (*s A canonical structure declares "canonical" conversion hints between *) (* the effective components of a structure and the projections of the *) (* structure *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f51820bf6..aadb36396 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -970,3 +970,21 @@ let meta_reducible_instance evd b = | _ -> map_constr irec u in if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus + + +let head_unfold_under_prod ts env _ c = + let unfold cst = + if Cpred.mem cst (snd ts) then + match constant_opt_value env cst with + | Some c -> c + | None -> mkConst cst + else mkConst cst in + let rec aux c = + match kind_of_term c with + | Prod (n,t,c) -> mkProd (n,aux t, aux c) + | _ -> + let (h,l) = decompose_app c in + match kind_of_term h with + | Const cst -> beta_applist (unfold cst,l) + | _ -> c in + aux c diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index edbb4f90c..171967583 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -215,6 +215,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr val whd_meta : (metavariable * constr) list -> constr -> constr val plain_instance : (metavariable * constr) list -> constr -> constr val instance : (metavariable * constr) list -> constr -> constr +val head_unfold_under_prod : transparent_state -> reduction_function (*s Heuristic for Conversion with Evar *) diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml new file mode 100644 index 000000000..656a90c70 --- /dev/null +++ b/pretyping/term_dnet.ml @@ -0,0 +1,388 @@ +(************************************************************************) +(* 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 Util +open Term +open Sign +open Names +open Libnames +open Mod_subst +open Pp (* debug *) +(*i*) + + +(* Representation/approximation of terms to use in the dnet: + * + * - no meta or evar (use ['a pattern] for that) + * + * - [Rel]s and [Sort]s are not taken into account (that's why we need + * a second pass of linear filterin on the results - it's not a perfect + * term indexing structure) + + * - Foralls and LetIns are represented by a context DCtx (a list of + * generalization, similar to rel_context, and coded with DCons and + * DNil). This allows for matching under an unfinished context + *) + +module DTerm = +struct + + type 't t = + | DRel + | DSort + | DRef of global_reference + | DCtx of 't * 't (* (binding list, subterm) = Prods and LetIns *) + | DLambda of 't * 't + | DApp of 't * 't (* binary app *) + | DCase of case_info * 't * 't * 't array + | DFix of int array * int * 't array * 't array + | DCoFix of int * 't array * 't array + + (* special constructors only inside the left-hand side of DCtx or + DApp. Used to encode lists of foralls/letins/apps as contexts *) + | DCons of ('t * 't option) * 't + | DNil + + type dconstr = dconstr t + + (* debug *) + let rec pr_dconstr f : 'a t -> std_ppcmds = function + | DRel -> str "*" + | DSort -> str "Sort" + | DRef _ -> str "Ref" + | DCtx (ctx,t) -> f ctx ++ spc() ++ str "|-" ++ spc () ++ f t + | DLambda (t1,t2) -> str "fun"++ spc() ++ f t1 ++ spc() ++ str"->" ++ spc() ++ f t2 + | DApp (t1,t2) -> f t1 ++ spc() ++ f t2 + | DCase (_,t1,t2,ta) -> str "case" + | DFix _ -> str "fix" + | DCoFix _ -> str "cofix" + | DCons ((t,dopt),tl) -> f t ++ (match dopt with + Some t' -> str ":=" ++ f t' + | None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl + | DNil -> str "[]" + + (* + * Functional iterators for the t datatype + * a.k.a boring and error-prone boilerplate code + *) + + let map f = function + | (DRel | DSort | DNil | DRef _) as c -> c + | DCtx (ctx,c) -> DCtx (f ctx, f c) + | DLambda (t,c) -> DLambda (f t, f c) + | DApp (t,u) -> DApp (f t,f u) + | DCase (ci,p,c,bl) -> DCase (ci, f p, f c, Array.map f bl) + | DFix (ia,i,ta,ca) -> + DFix (ia,i,Array.map f ta,Array.map f ca) + | DCoFix(i,ta,ca) -> + DCoFix (i,Array.map f ta,Array.map f ca) + | DCons ((t,topt),u) -> DCons ((f t,Option.map f topt), f u) + + let compare = Pervasives.compare + + let fold f acc = function + | (DRel | DNil | DSort | DRef _) -> acc + | DCtx (ctx,c) -> f (f acc ctx) c + | DLambda (t,c) -> f (f acc t) c + | DApp (t,u) -> f (f acc t) u + | DCase (ci,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl + | DFix (ia,i,ta,ca) -> + Array.fold_left f (Array.fold_left f acc ta) ca + | DCoFix(i,ta,ca) -> + Array.fold_left f (Array.fold_left f acc ta) ca + | DCons ((t,topt),u) -> f (Option.fold_left f (f acc t) topt) u + + let choose f = function + | (DRel | DSort | DNil | DRef _) -> invalid_arg "choose" + | DCtx (ctx,c) -> f ctx + | DLambda (t,c) -> f t + | DApp (t,u) -> f u + | DCase (ci,p,c,bl) -> f c + | DFix (ia,i,ta,ca) -> f ta.(0) + | DCoFix (i,ta,ca) -> f ta.(0) + | DCons ((t,topt),u) -> f u + + let fold2 (f:'a -> 'b -> 'c -> 'a) (acc:'a) (c1:'b t) (c2:'c t) : 'a = + let head w = map (fun _ -> ()) w in + if compare (head c1) (head c2) <> 0 + then invalid_arg "fold2:compare" else + match c1,c2 with + | (DRel, DRel | DNil, DNil | DSort, DSort | DRef _, DRef _) -> acc + | (DCtx (c1,t1), DCtx (c2,t2) + | DApp (c1,t1), DApp (c2,t2) + | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2 + | DCase (ci,p1,c1,bl1),DCase (_,p2,c2,bl2) -> + array_fold_left2 f (f (f acc p1 p2) c1 c2) bl1 bl2 + | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) -> + array_fold_left2 f (array_fold_left2 f acc ta1 ta2) ca1 ca2 + | DCoFix(i,ta1,ca1), DCoFix(_,ta2,ca2) -> + array_fold_left2 f (array_fold_left2 f acc ta1 ta2) ca1 ca2 + | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> + f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2 + | _ -> assert false + + let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t = + let head w = map (fun _ -> ()) w in + if compare (head c1) (head c2) <> 0 + then invalid_arg "map2_t:compare" else + match c1,c2 with + | (DRel, DRel | DSort, DSort | DNil, DNil | DRef _, DRef _) as cc -> + let (c,_) = cc in c + | DCtx (c1,t1), DCtx (c2,t2) -> DCtx (f c1 c2, f t1 t2) + | DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2) + | DApp (t1,u1), DApp (t2,u2) -> DApp (f t1 t2,f u1 u2) + | DCase (ci,p1,c1,bl1), DCase (_,p2,c2,bl2) -> + DCase (ci, f p1 p2, f c1 c2, array_map2 f bl1 bl2) + | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) -> + DFix (ia,i,array_map2 f ta1 ta2,array_map2 f ca1 ca2) + | DCoFix (i,ta1,ca1), DCoFix (_,ta2,ca2) -> + DCoFix (i,array_map2 f ta1 ta2,array_map2 f ca1 ca2) + | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> + DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2) + | _ -> assert false + + let terminal = function + | (DRel | DSort | DNil | DRef _) -> true + | _ -> false +end + +(* + * Terms discrimination nets + * Uses the general dnet datatype on DTerm.t + * (here you can restart reading) + *) + +(* + * Construction of the module + *) + +module type IDENT = +sig + type t + val compare : t -> t -> int + val subst : substitution -> t -> t + val constr_of : t -> constr +end + +module type OPT = +sig + val reduce : constr -> constr + val direction : bool +end + +module Make = + functor (Ident : IDENT) -> + functor (Opt : OPT) -> +struct + + module TDnet : Dnet.S with type ident=Ident.t + and type 'a structure = 'a DTerm.t + and type meta = metavariable + = Dnet.Make(DTerm)(Ident) + (struct + type t = metavariable + let compare = Pervasives.compare + end) + + type t = TDnet.t + + type ident = TDnet.ident + + type 'a pattern = 'a TDnet.pattern + type term_pattern = term_pattern DTerm.t pattern + + type idset = TDnet.Idset.t + + type result = ident * (constr*existential_key) * Termops.subst + + open DTerm + open TDnet + + let rec pat_of_constr c : term_pattern = + match kind_of_term c with + | Rel _ -> Term DRel + | Sort _ -> Term DSort + | Var i -> Term (DRef (VarRef i)) + | Const c -> Term (DRef (ConstRef c)) + | Ind i -> Term (DRef (IndRef i)) + | Construct c -> Term (DRef (ConstructRef c)) + | Term.Meta _ -> assert false + | Evar (i,_) -> Meta i + | Case (ci,c1,c2,ca) -> + Term(DCase(ci,pat_of_constr c1,pat_of_constr c2,Array.map pat_of_constr ca)) + | Fix ((ia,i),(_,ta,ca)) -> + Term(DFix(ia,i,Array.map pat_of_constr ta, Array.map pat_of_constr ca)) + | CoFix (i,(_,ta,ca)) -> + Term(DCoFix(i,Array.map pat_of_constr ta,Array.map pat_of_constr ca)) + | Cast (c,_,_) -> pat_of_constr c + | Lambda (_,t,c) -> Term(DLambda (pat_of_constr t, pat_of_constr c)) + | (Prod (_,_,_) | LetIn(_,_,_,_)) -> + let (ctx,c) = ctx_of_constr (Term DNil) c in Term (DCtx (ctx,c)) + | App (f,ca) -> + Array.fold_left (fun c a -> Term (DApp (c,a))) + (pat_of_constr f) (Array.map pat_of_constr ca) + + and ctx_of_constr ctx c : term_pattern * term_pattern = + match kind_of_term c with + | Prod (_,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c + | LetIn(_,d,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t, Some (pat_of_constr d)),ctx))) c + | _ -> ctx,pat_of_constr c + + let empty_ctx : term_pattern -> term_pattern = function + | Meta _ as c -> c + | Term (DCtx(_,_)) as c -> c + | c -> Term (DCtx (Term DNil, c)) + + (* + * Basic primitives + *) + + let empty = TDnet.empty + + let subst s t = + let sleaf id = Ident.subst s id in + let snode = function + | DTerm.DRef gr -> DTerm.DRef (fst (subst_global s gr)) + | n -> n in + TDnet.map sleaf snode t + + let union = TDnet.union + + let add (c:constr) (id:Ident.t) (dn:t) = + let c = Opt.reduce c in + let c = empty_ctx (pat_of_constr c) in + TDnet.add dn c id + + let new_meta_no = + let ctr = ref 0 in + fun () -> decr ctr; !ctr + + let new_meta_no = Evarutil.new_untyped_evar + + let neutral_meta = new_meta_no() + + let new_meta () = Meta (new_meta_no()) + let new_evar () = mkEvar(new_meta_no(),[||]) + + let rec remove_cap : term_pattern -> term_pattern = function + | Term (DCons (t,u)) -> Term (DCons (t,remove_cap u)) + | Term DNil -> new_meta() + | _ -> assert false + + let under_prod : term_pattern -> term_pattern = function + | Term (DCtx (t,u)) -> Term (DCtx (remove_cap t,u)) + | Meta m -> Term (DCtx(new_meta(), Meta m)) + | _ -> assert false + + let init = let e = new_meta_no() in (mkEvar (e,[||]),e) + + let rec e_subst_evar i (t:unit->constr) c = + match kind_of_term c with + | Evar (j,_) when i=j -> t() + | _ -> map_constr (e_subst_evar i t) c + + let subst_evar i c = e_subst_evar i (fun _ -> c) + + (* debug *) + let rec pr_term_pattern p = + (fun pr_t -> function + | Term t -> pr_t t + | Meta m -> str"["++Util.pr_int (Obj.magic m)++str"]" + ) (pr_dconstr pr_term_pattern) p + + let search_pat cpat dpat dn (up,plug) = + let whole_c = subst_evar plug cpat up in + TDnet.Idset.fold + (fun id acc -> + let c_id = Opt.reduce (Ident.constr_of id) in + let (ctx,wc) = + try Termops.align_prod_letin whole_c c_id + with Invalid_argument _ -> [],c_id in + let up = it_mkProd_or_LetIn up ctx in + let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in + try (id,(up,plug),Termops.filtering ctx Reduction.CUMUL wc whole_c)::acc + with Termops.CannotFilter -> acc + ) (TDnet.find_match dpat dn) [] + + let fold_pattern_neutral f = + fold_pattern (fun m dn acc -> if m=neutral_meta then acc else f m dn acc) + + let fold_pattern_nonlin f = + let defined = ref Gmap.empty in + fold_pattern_neutral + ( fun m dn acc -> + let dn = try TDnet.inter dn (Gmap.find m !defined) with Not_found -> dn in + defined := Gmap.add m dn !defined; + f m dn acc ) + + let fold_pattern_up f acc dpat cpat dn (up,plug) = + fold_pattern_nonlin + ( fun m dn acc -> + f dn (subst_evar plug (e_subst_evar neutral_meta new_evar cpat) up, m) acc + ) acc dpat dn + + let possibly_under pat k dn (up,plug) = + let rec aux fst dn (up,plug) acc = + let cpat = pat() in + let dpat = pat_of_constr cpat in + let dpat = if fst then empty_ctx dpat else dpat in + snd (fold_pattern_up (aux false) acc dpat cpat dn (up,plug)) @ + (k dn (up,plug)) in + aux true dn (up,plug) [] + + let eq_pat eq () = mkApp(eq,[|mkEvar(neutral_meta,[||]);new_evar();new_evar()|]) + let app_pat () = mkApp(new_evar(),[|mkEvar(neutral_meta,[||])|]) + + (* + * High-level primitives describing specific search problems + *) + + let search_pattern dn pat = + let pat = Opt.reduce pat in + search_pat pat (empty_ctx (pat_of_constr pat)) dn init + + let search_concl dn pat = + let pat = Opt.reduce pat in + search_pat pat (under_prod (empty_ctx (pat_of_constr pat))) dn init + + let search_eq_concl dn eq pat = + let pat = Opt.reduce pat in + let eq_pat = eq_pat eq () in + let eq_dpat = under_prod (empty_ctx (pat_of_constr eq_pat)) in + snd (fold_pattern_up + (fun dn up acc -> + search_pat pat (pat_of_constr pat) dn up @ acc + ) [] eq_dpat eq_pat dn init) + + let search_head_concl dn pat = + let pat = Opt.reduce pat in + possibly_under app_pat (search_pat pat (pat_of_constr pat)) dn init + + let find_all dn = Idset.elements (TDnet.find_all dn) +end + +module type S = +sig + type t + type ident + + type result = ident * (constr*existential_key) * Termops.subst + + val empty : t + val add : constr -> ident -> t -> t + val union : t -> t -> t + val subst : substitution -> t -> t + val search_pattern : t -> constr -> result list + val search_concl : t -> constr -> result list + val search_head_concl : t -> constr -> result list + val search_eq_concl : t -> constr -> constr -> result list + val find_all : t -> ident list +end diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli new file mode 100644 index 000000000..ccf962481 --- /dev/null +++ b/pretyping/term_dnet.mli @@ -0,0 +1,110 @@ +(************************************************************************) +(* 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 Term +open Sign +open Libnames +open Mod_subst +(*i*) + +(* Dnets on constr terms. + + An instantiation of Dnet on (an approximation of) constr. It + associates a term (possibly with Evar) with an + identifier. Identifiers must be unique (no two terms sharing the + same ident), and there must be a way to recover the full term from + the identifier (function constr_of). + + Optionally, a pre-treatment on terms can be performed before adding + or searching (reduce). Practically, it is used to do some kind of + delta-reduction on terms before indexing them. + + The results returned here are perfect, since post-filtering is done + inside here. + + See lib/dnet.mli for more details. +*) + +(* Identifiers to store (right hand side of the association) *) +module type IDENT = sig + type t + val compare : t -> t -> int + + (* how to substitute them for storage *) + val subst : substitution -> t -> t + + (* how to recover the term from the identifier *) + val constr_of : t -> constr +end + +(* Options : *) +module type OPT = sig + + (* pre-treatment to terms before adding or searching *) + val reduce : constr -> constr + + (* direction of post-filtering w.r.t sort subtyping : + - true means query <= terms in the structure + - false means terms <= query + *) + val direction : bool +end + +module type S = +sig + type t + type ident + + (* results of filtering : identifier, a context (term with Evar + hole) and the substitution in that context*) + type result = ident * (constr*existential_key) * Termops.subst + + val empty : t + + (* [add c i dn] adds the binding [(c,i)] to [dn]. [c] can be a + closed term or a pattern (with untyped Evars). No Metas accepted *) + val add : constr -> ident -> t -> t + + (* merge of dnets. Faster than re-adding all terms *) + val union : t -> t -> t + + val subst : substitution -> t -> t + + (* + * High-level primitives describing specific search problems + *) + + (* [search_pattern dn c] returns all terms/patterns in dn + matching/matched by c *) + val search_pattern : t -> constr -> result list + + (* [search_concl dn c] returns all matches under products and + letins, i.e. it finds subterms whose conclusion matches c. The + complexity depends only on c ! *) + val search_concl : t -> constr -> result list + + (* [search_head_concl dn c] matches under products and applications + heads. Finds terms of the form [forall H_1...H_n, C t_1...t_n] + where C matches c *) + val search_head_concl : t -> constr -> result list + + (* [search_eq_concl dn eq c] searches terms of the form [forall + H1...Hn, eq _ X1 X2] where either X1 or X2 matches c *) + val search_eq_concl : t -> constr -> constr -> result list + + (* [find_all dn] returns all idents contained in dn *) + val find_all : t -> ident list +end + +module Make : + functor (Ident : IDENT) -> + functor (Opt : OPT) -> + S with type ident = Ident.t diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 987db88b1..e3b8a166c 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -951,16 +951,77 @@ let base_sort_cmp pb s0 s1 = | _ -> false (* eq_constr extended with universe erasure *) -let rec constr_cmp cv_pb t1 t2 = +let compare_constr_univ f cv_pb t1 t2 = match kind_of_term t1, kind_of_term t2 with Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2 | Prod (_,t1,c1), Prod (_,t2,c2) -> - constr_cmp Reduction.CONV t1 t2 & - constr_cmp cv_pb c1 c2 - | _ -> compare_constr (constr_cmp Reduction.CONV) t1 t2 + f Reduction.CONV t1 t2 & f cv_pb c1 c2 + | _ -> compare_constr (f Reduction.CONV) t1 t2 + +let rec constr_cmp cv_pb t1 t2 = compare_constr_univ constr_cmp cv_pb t1 t2 let eq_constr = constr_cmp Reduction.CONV +(* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn) + App(c,[||]) -> ([],c) *) +let split_app c = match kind_of_term c with + App(c,l) -> + let len = Array.length l in + if len=0 then ([],c) else + let last = Array.get l (len-1) in + let prev = Array.sub l 0 (len-1) in + c::(Array.to_list prev), last + | _ -> assert false + +let hdtl l = List.hd l, List.tl l + +type subst = (rel_context*constr) Intmap.t + +exception CannotFilter + +let filtering env cv_pb c1 c2 = + let evm = ref Intmap.empty in + let define cv_pb e1 ev c1 = + try let (e2,c2) = Intmap.find ev !evm in + let shift = List.length e1 - List.length e2 in + if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter + with Not_found -> + evm := Intmap.add ev (e1,c1) !evm + in + let rec aux env cv_pb c1 c2 = + match kind_of_term c1, kind_of_term c2 with + | App _, App _ -> + let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in + aux env cv_pb l1 l2; if p1=[] & p2=[] then () else + aux env cv_pb (applist (hdtl p1)) (applist (hdtl p2)) + | Prod (n,t1,c1), Prod (_,t2,c2) -> + aux env cv_pb t1 t2; + aux ((n,None,t1)::env) cv_pb c1 c2 + | _, Evar (ev,_) -> define cv_pb env ev c1 + | Evar (ev,_), _ -> define cv_pb env ev c2 + | _ -> + if compare_constr_univ + (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then () + else raise CannotFilter + (* TODO: le reste des binders *) + in + aux env cv_pb c1 c2; !evm + +let decompose_prod_letin : constr -> int * rel_context * constr = + let rec prodec_rec i l c = match kind_of_term c with + | Prod (n,t,c) -> prodec_rec (succ i) ((n,None,t)::l) c + | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c + | Cast (c,_,_) -> prodec_rec i l c + | _ -> i,l,c in + prodec_rec 0 [] + +let align_prod_letin c a : rel_context * constr = + let (lc,_,_) = decompose_prod_letin c in + let (la,l,a) = decompose_prod_letin a in + if not (la >= lc) then invalid_arg "align_prod_letin"; + let (l1,l2) = Util.list_chop lc l in + l2,it_mkProd_or_LetIn a l1 + (* On reduit une serie d'eta-redex de tete ou rien du tout *) (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *) (* Remplace 2 versions précédentes buggées *) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 9163a1d9e..79fe908d7 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -170,12 +170,28 @@ val error_invalid_occurrence : int list -> 'a (* Alternative term equalities *) val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool +val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) -> + Reduction.conv_pb -> constr -> constr -> bool val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool val eq_constr : constr -> constr -> bool val eta_reduce_head : constr -> constr val eta_eq_constr : constr -> constr -> bool +exception CannotFilter + +(* Lightweight first-order filtering procedure. Unification + variables ar represented by (untyped) Evars. + [filtering c1 c2] returns the substitution n'th evar -> + (context,term), or raises [CannotFilter]. + Warning: Outer-kernel sort subtyping are taken into account: c1 has + to be smaller than c2 wrt. sorts. *) +type subst = (rel_context*constr) Intmap.t +val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst + +val decompose_prod_letin : constr -> int * rel_context * constr +val align_prod_letin : constr -> constr -> rel_context * constr + (* finding "intuitive" names to hypotheses *) val lowercase_first_char : identifier -> string val sort_hdchar : sorts -> string diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml new file mode 100644 index 000000000..8a9646a17 --- /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()) } diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli new file mode 100644 index 000000000..3866fff39 --- /dev/null +++ b/toplevel/autoinstance.mli @@ -0,0 +1,38 @@ +(************************************************************************) +(* 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 Term +open Libnames +open Typeclasses +open Names +open Evd +open Sign +(*i*) + +(*s Automatic detection of (some) record instances *) + +(* What to do if we find an instance. Passed are : the reference + * representing the record/class (definition or constructor) *) +type instance_decl_function = global_reference -> rel_context -> constr list -> unit + +(* [search_declaration gr] Search in the library if the (new) + * declaration gr can form an instance of a registered record/class *) +val search_declaration : global_reference -> unit + +(* [search_record declf gr evm] Search the library for instances of + the (new) record/class declaration [gr], and register them using + [declf]. [evm] is the signature of the record (to avoid recomputing + it) *) +val search_record : instance_decl_function -> global_reference -> evar_map -> unit + +(* Instance declaration for both scenarios *) +val declare_record_instance : instance_decl_function +val declare_class_instance : instance_decl_function diff --git a/toplevel/command.ml b/toplevel/command.ml index 8d480ef2f..89739b984 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -143,6 +143,7 @@ let declare_global_definition ident ce local imps = if local = Local && Flags.is_verbose() then msg_warning (pr_id ident ++ str" is declared as a global definition"); definition_message ident; + Autoinstance.search_declaration (ConstRef kn); gr let declare_definition_hook = ref ignore @@ -198,6 +199,7 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) = if local=Local & Flags.is_verbose () then msg_warning (pr_id ident ++ str" is declared as a parameter" ++ str" because it is at a global level"); + Autoinstance.search_declaration (ConstRef kn); gr in if is_coe then Class.try_add_new_coercion r local @@ -374,6 +376,7 @@ let save id const do_guard (locality,kind) hook = (Local, VarRef id) | Local | Global -> let kn = declare_constant id (DefinitionEntry const, k) in + Autoinstance.search_declaration (ConstRef kn); (Global, ConstRef kn) in Pfedit.delete_current_proof (); definition_message id; @@ -644,9 +647,11 @@ let declare_mutual_with_eliminations isrecord mie impls = let (_,kn) = declare_mind isrecord mie in list_iter_i (fun i (indimpls, constrimpls) -> let ind = (kn,i) in + Autoinstance.search_declaration (IndRef ind); maybe_declare_manual_implicits false (IndRef ind) indimpls; list_iter_i (fun j impls -> +(* Autoinstance.search_declaration (ConstructRef (ind,j));*) maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls) constrimpls) impls; @@ -802,8 +807,9 @@ let declare_fix boxed kind f def t imps = } in let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in let gr = ConstRef kn in - maybe_declare_manual_implicits false gr imps; - gr + Autoinstance.search_declaration (ConstRef kn); + maybe_declare_manual_implicits false gr imps; + gr let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in @@ -1260,4 +1266,3 @@ let get_current_context () = with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) - diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml new file mode 100644 index 000000000..6fd49b15b --- /dev/null +++ b/toplevel/libtypes.ml @@ -0,0 +1,109 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +open Term +open Summary +open Libobject + +(* + * Module construction + *) + +let reduce c = Reductionops.head_unfold_under_prod + (Auto.Hint_db.transparent_state (Auto.searchtable_map "typeclass_instances")) + (Global.env()) Evd.empty c + +module TypeDnet = Term_dnet.Make(struct + type t = Libnames.global_reference + let compare = Pervasives.compare + let subst s gr = fst (Libnames.subst_global s gr) + let constr_of = Global.type_of_global + end) + (struct let reduce = reduce + let direction = false end) + +type result = Libnames.global_reference * (constr*existential_key) * Termops.subst + +let all_types = ref TypeDnet.empty +let defined_types = ref TypeDnet.empty + +(* + * Bookeeping & States + *) + +let freeze () = + (!all_types,!defined_types) + +let unfreeze (lt,dt) = + all_types := lt; + defined_types := dt + +let init () = + all_types := TypeDnet.empty; + defined_types := TypeDnet.empty + +let _ = + declare_summary "type-library-state" + { freeze_function = freeze; + unfreeze_function = unfreeze; + init_function = init; + survive_module = false; + survive_section = false } + +let load (_,d) = +(* Profile.print_logical_stats !all_types; + Profile.print_logical_stats d;*) + all_types := TypeDnet.union d !all_types + +let subst s t = TypeDnet.subst s t +(* +let subst_key = Profile.declare_profile "subst" +let subst a b = Profile.profile2 subst_key TypeDnet.subst a b + +let load_key = Profile.declare_profile "load" +let load a = Profile.profile1 load_key load a +*) +let (input,output) = + declare_object + { (default_object "LIBTYPES") with + load_function = (fun _ -> load); + subst_function = (fun (_,s,t) -> subst s t); + export_function = (fun x -> Some x); + classify_function = (fun (_,x) -> Substitute x) + } + +let update () = Lib.add_anonymous_leaf (input !defined_types) + +(* + * Search interface + *) + +let search_pattern pat = TypeDnet.search_pattern !all_types pat +let search_concl pat = TypeDnet.search_concl !all_types pat +let search_head_concl pat = TypeDnet.search_head_concl !all_types pat +let search_eq_concl eq pat = TypeDnet.search_eq_concl !all_types eq pat + +let add typ gr = + defined_types := TypeDnet.add typ gr !defined_types; + all_types := TypeDnet.add typ gr !all_types +(* +let add_key = Profile.declare_profile "add" +let add a b = Profile.profile1 add_key add a b +*) + +(* + * Hooks declaration + *) + +let _ = Declare.add_cache_hook + ( fun sp -> + let gr = Nametab.absolute_reference sp in + let ty = Global.type_of_global gr in + add ty gr ) + +let _ = Declaremods.set_end_library_hook update diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli new file mode 100644 index 000000000..be5e9312a --- /dev/null +++ b/toplevel/libtypes.mli @@ -0,0 +1,32 @@ +(************************************************************************) +(* 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 Term +(*i*) + +(* + * Persistent library of all declared object, + * indexed by their types (uses Dnets) + *) + +(* results are the reference of the object, together with a context +(constr+evar) and a substitution under this context *) +type result = Libnames.global_reference * (constr*existential_key) * Termops.subst + +(* this is the reduction function used in the indexing process *) +val reduce : types -> types + +(* The different types of search available. + * See term_dnet.mli for more explanations *) +val search_pattern : types -> result list +val search_concl : types -> result list +val search_head_concl : types -> result list +val search_eq_concl : constr -> types -> result list diff --git a/toplevel/record.ml b/toplevel/record.ml index 9978d7bf6..3ef7eccad 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -222,8 +222,24 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls) in (kinds,sp_projs) -let declare_structure finite id idbuild paramimpls params arity fieldimpls fields - ?(kind=StructureComponent) ?name is_coe coers = +let structure_signature ctx = + let rec deps_to_evar evm l = + match l with [] -> Evd.empty + | [(_,_,typ)] -> Evd.add evm (Evarutil.new_untyped_evar()) + (Evd.make_evar Environ.empty_named_context_val typ) + | (_,_,typ)::tl -> + let ev = Evarutil.new_untyped_evar() in + let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val typ) in + let new_tl = Util.list_map_i + (fun pos (n,c,t) -> n,c, + Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) 1 tl in + deps_to_evar evm new_tl in + deps_to_evar Evd.empty (List.rev ctx) + +open Typeclasses + +let declare_structure finite infer id idbuild paramimpls params arity fieldimpls fields + ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in let args = extended_rel_list nfields params in let ind = applist (mkRel (1+nparams+nfields), args) in @@ -241,11 +257,14 @@ let declare_structure finite id idbuild paramimpls params arity fieldimpls field mind_entry_inds = [mie_ind] } in let kn = Command.declare_mutual_with_eliminations true mie [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) + let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in - let build = ConstructRef (rsp,1) in - if is_coe then Class.try_add_new_coercion build Global; - Recordops.declare_structure(rsp,(rsp,1),List.rev kinds,List.rev sp_projs); - kn,0 + let build = ConstructRef cstr in + if is_coe then Class.try_add_new_coercion build Global; + Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); + if infer then + Evd.fold (fun ev evi () -> Recordops.declare_method (ConstructRef cstr) ev sign) sign (); + rsp let implicits_of_context ctx = list_map_i (fun i name -> @@ -256,8 +275,6 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true)) 1 (List.rev (Anonymous :: (List.map pi1 ctx))) -open Typeclasses - let typeclasses_db = "typeclass_instances" let qualid_of_con c = @@ -274,8 +291,8 @@ let declare_instance_cst glob con = | Some tc -> add_instance (new_instance tc None glob con) | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.") -let declare_class finite def id idbuild paramimpls params arity fieldimpls fields - ?(kind=StructureComponent) ?name is_coe coers = +let declare_class finite def infer id idbuild paramimpls params arity fieldimpls fields + ?(kind=StructureComponent) ?name is_coe coers sign = let fieldimpls = (* Make the class and all params implicits in the projections *) let ctx_impls = implicits_of_context params in @@ -309,15 +326,16 @@ let declare_class finite def id idbuild paramimpls params arity fieldimpls field (DefinitionEntry proj_entry, IsDefinition Definition) in let cref = ConstRef cst in - Impargs.declare_manual_implicits false cref paramimpls; - Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls); - set_rigid cst; (* set_rigid proj_cst; *) - cref, [proj_name, Some proj_cst] + Impargs.declare_manual_implicits false cref paramimpls; + Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls); + set_rigid cst; (* set_rigid proj_cst; *) + if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign (); + cref, [proj_name, Some proj_cst] | _ -> let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in - let ind = declare_structure true (snd id) idbuild paramimpls + let ind = declare_structure true infer (snd id) idbuild paramimpls params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields - ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) + ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign in (* List.iter (Option.iter (declare_interning_data ((),[]))) notations; *) IndRef ind, (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y)) @@ -339,7 +357,7 @@ let declare_class finite def id idbuild paramimpls params arity fieldimpls field List.iter2 (fun p sub -> if sub then match snd p with Some p -> declare_instance_cst true p | None -> ()) k.cl_projs coers; - add_class k; impl + add_class k; impl let interp_and_check_sort sort = Option.map (fun sort -> @@ -349,10 +367,11 @@ let interp_and_check_sort sort = else user_err_loc (constr_loc sort,"", str"Sort expected.")) sort open Vernacexpr +open Autoinstance (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean list telling if the corresponding fields must me declared as coercion *) -let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = +let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in let coers,fs = List.split cfs in let extract_name acc = function @@ -365,13 +384,18 @@ let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = let sc = interp_and_check_sort s in let implpars, params, implfs, fields = States.with_heavy_rollback (fun () -> - typecheck_params_and_fields idstruc sc ps notations fs) () - in + typecheck_params_and_fields idstruc sc ps notations fs) () in + let sign = structure_signature (fields@params) in match kind with | Record | Structure -> let arity = Option.default (new_Type ()) sc in let implfs = List.map - (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs - in IndRef (declare_structure finite idstruc idbuild implpars params arity implfs fields is_coe coers) - | Class b -> - declare_class finite b (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers + (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in + let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe coers sign in + if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign; + IndRef ind + | Class def -> + let gr = declare_class finite def infer (loc,idstruc) idbuild + implpars params sc implfs fields is_coe coers sign in + if infer then search_record declare_class_instance gr sign; + gr diff --git a/toplevel/record.mli b/toplevel/record.mli index 3fe18e192..564d4409f 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -27,15 +27,16 @@ val declare_projections : bool list -> manual_explicitation list list -> rel_context -> (name * bool) list * constant option list -val declare_structure : bool (*coinductive?*)-> identifier -> identifier -> +val declare_structure : bool (*coinductive?*)-> bool (*infer?*) -> identifier -> identifier -> manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *) Impargs.manual_explicitation list list -> rel_context -> (* fields *) ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool -> (* coercion? *) bool list -> (* field coercions *) + Evd.evar_map -> inductive val definition_structure : - record_kind * bool (*coinductive?*)*lident with_coercion * local_binder list * + record_kind * bool (*coinductive?*) * bool(*infer?*)* lident with_coercion * local_binder list * (local_decl_expr with_coercion with_notation) list * identifier * constr_expr option -> global_reference diff --git a/parsing/search.ml b/toplevel/search.ml index 94270ee13..e50af9733 100644 --- a/parsing/search.ml +++ b/toplevel/search.ml @@ -119,10 +119,9 @@ let filter_by_module (module_list:dir_path list) (accept:bool) 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 ref_eq = Libnames.encode_kn Coqlib.logic_module (id_of_string "eq"), 0 +let c_eq = mkInd ref_eq +let gref_eq = IndRef ref_eq let mk_rewrite_pattern1 eq pattern = PApp (PRef eq, [| PMeta None; pattern; PMeta None |]) @@ -166,18 +165,38 @@ let raw_search_rewrite extra_filter display_function pattern = && extra_filter s a c) display_function gref_eq +(* + * functions to use the new Libtypes facility + *) + +let raw_search search_function extra_filter display_function pat = + let env = Global.env() in + List.iter + (fun (gr,_,_) -> + let typ = Global.type_of_global gr in + if extra_filter gr env typ then + display_function gr env typ + ) (search_function pat) + +let raw_pattern_search = raw_search Libtypes.search_concl +let raw_search_rewrite = raw_search (Libtypes.search_eq_concl c_eq) +let raw_search_by_head = raw_search Libtypes.search_head_concl + 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 text_search_by_head extra_filter = + raw_search_by_head 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_by_head pat inout = + text_search_by_head (filter_by_module_from_list inout) pat let search_rewrite pat inout = text_search_rewrite (filter_by_module_from_list inout) pat @@ -185,7 +204,6 @@ let search_rewrite pat inout = 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) diff --git a/parsing/search.mli b/toplevel/search.mli index fc2ea925f..5b978770b 100644 --- a/parsing/search.mli +++ b/toplevel/search.mli @@ -22,10 +22,10 @@ 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 : +val search_by_head : constr -> dir_path list * bool -> unit +val search_rewrite : constr -> dir_path list * bool -> unit +val search_pattern : constr -> 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. @@ -42,9 +42,11 @@ val gen_filtered_search : (global_reference -> env -> constr -> bool) -> 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 + (global_reference -> env -> constr -> unit) -> constr -> unit val raw_search_rewrite : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> constr_pattern -> unit + (global_reference -> env -> constr -> unit) -> constr -> unit val raw_search_about : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> (bool * glob_search_about_item) list -> unit +val raw_search_by_head : (global_reference -> env -> constr -> bool) -> + (global_reference -> env -> constr -> unit) -> constr -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a4d3e5458..37e9cf22a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -375,7 +375,7 @@ let vernac_assumption kind l nl= else Dumpglob.dump_definition lid true "var") idl; declare_assumption idl is_coe kind [] c false false nl) l -let vernac_record k finite struc binders sort nameopt cfs = +let vernac_record k finite infer struc binders sort nameopt cfs = let const = match nameopt with | None -> add_prefix "Build_" (snd (snd struc)) | Some (_,id as lid) -> @@ -386,9 +386,9 @@ let vernac_record k finite struc binders sort nameopt cfs = match x with | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" | _ -> ()) cfs); - ignore(Record.definition_structure (k,finite,struc,binders,cfs,const,sort)) + ignore(Record.definition_structure (k,finite,infer,struc,binders,cfs,const,sort)) -let vernac_inductive finite indl = +let vernac_inductive finite infer indl = if Dumpglob.dump () then List.iter (fun (((coe,lid), _, _, _, cstrs), _) -> match cstrs with @@ -401,12 +401,12 @@ let vernac_inductive finite indl = match indl with | [ ( id , bl , c , Some b, RecordDecl (oc,fs) ), None ] -> vernac_record (match b with Class true -> Class false | _ -> b) - finite id bl c oc fs + finite infer id bl c oc fs | [ ( id , bl , c , Some (Class true), Constructors [l]), _ ] -> let f = let (coe, ((loc, id), ce)) = l in ((coe, AssumExpr ((loc, Name id), ce)), None) - in vernac_record (Class true) finite id bl c None [f] + in vernac_record (Class true) finite infer id bl c None [f] | [ ( id , bl , c , Some (Class true), _), _ ] -> Util.error "Definitional classes must have a single method" | [ ( id , bl , c , Some (Class false), Constructors _), _ ] -> @@ -1143,13 +1143,14 @@ let vernac_search s r = if !pcoq <> None then (Option.get !pcoq).search s r else match s with | SearchPattern c -> - let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in - Search.search_pattern pat r + let (_,c) = interp_open_constr_patvar Evd.empty (Global.env()) c in + Search.search_pattern c r | 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 Search.search_rewrite pat r - | SearchHead ref -> - Search.search_by_head (global_with_alias ref) r + | SearchHead c -> + let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in + Search.search_by_head pat r | SearchAbout sl -> Search.search_about (List.map (on_snd interp_search_about_item) sl) r @@ -1310,7 +1311,7 @@ let interp c = match c with | VernacEndProof e -> vernac_end_proof e | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl - | VernacInductive (finite,l) -> vernac_inductive finite l + | VernacInductive (finite,infer,l) -> vernac_inductive finite infer l | VernacFixpoint (l,b) -> vernac_fixpoint l b | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b | VernacScheme l -> vernac_scheme l diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 5ea0235a5..9412a5981 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -75,7 +75,7 @@ type search_about_item = type searchable = | SearchPattern of constr_pattern_expr | SearchRewrite of constr_pattern_expr - | SearchHead of reference + | SearchHead of constr_pattern_expr | SearchAbout of (bool * search_about_item) list type locatable = @@ -143,6 +143,7 @@ type export_flag = bool (* true = Export; false = Import *) type specif_flag = bool (* true = Specification; false = Implementation *) type inductive_flag = bool (* true = Inductive; false = CoInductive *) type onlyparsing_flag = bool (* true = Parse only; false = Print also *) +type infer_flag = bool (* true = try to Infer record; false = nothing *) type sort_expr = Rawterm.rawsort @@ -211,7 +212,7 @@ type vernac_expr = | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list - | VernacInductive of inductive_flag * (inductive_expr * decl_notation) list + | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation) list | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool | VernacScheme of (lident option * scheme) list |