diff options
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 |