diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/autoinstance.ml | 316 | ||||
| -rw-r--r-- | toplevel/autoinstance.mli | 38 | ||||
| -rw-r--r-- | toplevel/command.ml | 11 | ||||
| -rw-r--r-- | toplevel/libtypes.ml | 109 | ||||
| -rw-r--r-- | toplevel/libtypes.mli | 32 | ||||
| -rw-r--r-- | toplevel/record.ml | 72 | ||||
| -rw-r--r-- | toplevel/record.mli | 5 | ||||
| -rw-r--r-- | toplevel/search.ml | 232 | ||||
| -rw-r--r-- | toplevel/search.mli | 52 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 23 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 5 |
11 files changed, 853 insertions, 42 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml new file mode 100644 index 0000000000..8a9646a174 --- /dev/null +++ b/toplevel/autoinstance.ml @@ -0,0 +1,316 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +(*i*) +open Pp +open Printer +open Names +open Term +open Evd +open Sign +open Libnames +(*i*) + +(*s + * Automatic detection of (some) record instances + *) + +(* Datatype for wannabe-instances: a signature is a typeclass along + with the collection of evars corresponding to the parameters/fields + of the class. Each evar can be uninstantiated (we're still looking + for them) or defined (the instance for the field is fixed) *) +type signature = global_reference * evar list * evar_map + +type instance_decl_function = global_reference -> rel_context -> constr list -> unit + +(* + * Search algorithm + *) + +let rec subst_evar evar def n c = + match kind_of_term c with + | Evar (e,_) when e=evar -> lift n def + | _ -> map_constr_with_binders (fun n->n+1) (subst_evar evar def) n c + +let subst_evar_in_evm evar def evm = + Evd.fold + (fun ev evi acc -> + let evar_body = match evi.evar_body with + | Evd.Evar_empty -> Evd.Evar_empty + | Evd.Evar_defined c -> Evd.Evar_defined (subst_evar evar def 0 c) in + let evar_concl = subst_evar evar def 0 evi.evar_concl in + Evd.add acc ev {evi with evar_body=evar_body; evar_concl=evar_concl} + ) evm empty + +(* Tries to define ev by c in evd. Fails if ev := c1 and c1 /= c ev : + * T1, c : T2 and T1 /= T2. Defines recursively all evars instantiated + * by this definition. *) + +let rec safe_evar_define evm ev c = + if not (closedn (-1) c) then raise Termops.CannotFilter else +(* msgnl(str"safe_evar_define "++pr_evar_map evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*) + let evi = (Evd.find evm ev) in + let define_subst evm sigma = + Util.Intmap.fold + ( fun ev (e,c) evm -> + match kind_of_term c with Evar (i,_) when i=ev -> evm | _ -> + safe_evar_define evm ev (lift (-List.length e) c) + ) sigma evm in + match evi.evar_body with + | Evd.Evar_defined def -> + define_subst evm (Termops.filtering [] Reduction.CUMUL def c) + | Evd.Evar_empty -> + let t = Libtypes.reduce (Typing.type_of (Global.env()) evm c) in + let u = Libtypes.reduce (evar_concl evi) in + let evm = subst_evar_in_evm ev c evm in + define_subst (Evd.define evm ev c) (Termops.filtering [] Reduction.CUMUL t u) + +let add_gen_ctx (cl,gen,evm) ctx : signature * constr list = + let rec really_new_evar () = + let ev = Evarutil.new_untyped_evar() in + if Evd.is_evar evm ev then really_new_evar() else ev in + let add_gen_evar (cl,gen,evm) ev ty : signature = + let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val ty) in + (cl,ev::gen,evm) in + let rec mksubst b = function + | [] -> [] + | a::tl -> b::(mksubst (a::b) tl) in + let evl = List.map (fun _ -> really_new_evar()) ctx in + let evcl = List.map (fun i -> mkEvar (i,[||])) evl in + let substl = List.rev (mksubst [] (evcl)) in + let ctx = List.map2 (fun s t -> substnl s 0 t) substl ctx in + let sign = List.fold_left2 add_gen_evar (cl,gen,evm) (List.rev evl) ctx in + sign,evcl + +(* TODO : for full proof-irrelevance in the search, provide a real + compare function for constr instead of Pervasive's one! *) +module SubstSet : Set.S with type elt = Termops.subst + = Set.Make (struct type t = Termops.subst + let compare = Util.Intmap.compare (Pervasives.compare) + end) + +(* searches instatiations in the library for just one evar [ev] of a + signature. [k] is called on each resulting signature *) +let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) = + let ev_typ = Libtypes.reduce (evar_concl evi) in + let sort_is_prop = is_Prop (Typing.type_of (Global.env()) evm (evar_concl evi)) in +(* msgnl(str"cherche "++pr_constr ev_typ++str" pour "++Util.pr_int ev);*) + let substs = ref SubstSet.empty in + try List.iter + ( fun (gr,(pat,_),s) -> + let (_,genl,_) = Termops.decompose_prod_letin pat in + let genl = List.map (fun (_,_,t) -> t) genl in + let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) genl in + let def = applistc (Libnames.constr_of_global gr) argl in +(* msgnl(str"essayons ?"++Util.pr_int ev++spc()++str":="++spc() + ++pr_constr def++spc()++str":"++spc()++pr_constr (Global.type_of_global gr)*) + (*++spc()++str"dans"++spc()++pr_evar_map evm++spc());*) + try + let evm = safe_evar_define evm ev def in + k (cl,gen,evm); + if sort_is_prop && SubstSet.mem s !substs then raise Exit; + substs := SubstSet.add s !substs + with Termops.CannotFilter -> () + ) (Libtypes.search_concl ev_typ) + with Exit -> () + +let evm_fold_rev f evm acc = + let l = Evd.fold (fun ev evi acc -> (ev,evi)::acc) evm [] in + List.fold_left (fun acc (ev,evi) -> f ev evi acc) acc l + +exception Continue of Evd.evar * Evd.evar_info + +(* searches matches for all the uninstantiated evars of evd in the + context. For each totally instantiated evar_map found, apply + k. *) +let rec complete_signature (k:signature -> unit) (cl,gen,evm:signature) = + try + evm_fold_rev + ( fun ev evi _ -> + if not (is_defined evm ev) && not (List.mem ev gen) then + raise (Continue (ev,evi)) + ) evm (); k (cl,gen,evm) + with Continue (ev,evi) -> complete_evar (cl,gen,evm) (ev,evi) (complete_signature k) + +(* define all permutations of the evars to evd and call k on the + resulting evd *) +let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit) : unit = + let rec aux evm = List.iter + ( fun (ctx,ev) -> + let tyl = List.map (fun (_,_,t) -> t) ctx in + let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) tyl in + let def = applistc c argl in +(* msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*) + try + if not (Evd.is_defined evm ev) then + let evm = safe_evar_define evm ev def in + aux evm; k (cl,gen,evm) + with Termops.CannotFilter -> () + ) evl in + aux evm + +let new_inst_no = + let cnt = ref 0 in + fun () -> incr cnt; string_of_int !cnt + +let make_instance_ident gr = + Nameops.add_suffix (Nametab.id_of_global gr) ("_autoinstance_"^new_inst_no()) + +let new_instance_message ident typ def = + Flags.if_verbose + msgnl (str"new instance"++spc() + ++Nameops.pr_id ident++spc()++str":"++spc() + ++pr_constr typ++spc()++str":="++spc() + ++pr_constr def) + +open Entries + +let rec deep_refresh_universes c = + match kind_of_term c with + | Sort (Type _) -> Termops.new_Type() + | _ -> map_constr deep_refresh_universes c + +let declare_record_instance gr ctx params = + let ident = make_instance_ident gr in + let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in + let def = deep_refresh_universes def in + let ce = { const_entry_body=def; const_entry_type=None; + const_entry_opaque=false; const_entry_boxed=false } in + let cst = Declare.declare_constant ident + (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in + new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def + +let declare_class_instance gr ctx params = + let ident = make_instance_ident gr in + let cl = Typeclasses.class_info gr in + let (def,typ) = Typeclasses.instance_constructor cl params in + let (def,typ) = it_mkLambda_or_LetIn def ctx, it_mkProd_or_LetIn typ ctx in + let def = deep_refresh_universes def in + let typ = deep_refresh_universes typ in + let ce = Entries.DefinitionEntry + { const_entry_type=Some typ; const_entry_body=def; + const_entry_opaque=false; const_entry_boxed=false } in + try + let cst = Declare.declare_constant ident + (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in + Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true cst); + new_instance_message ident typ def + with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Cerrors.explain_exn e) + +let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ctx t; + match kind_of_term t with + | Prod (n,t,c) -> iter_under_prod f ((n,None,t)::ctx) c + | _ -> () + +(* main search function: search for total instances containing gr, and + apply k to each of them *) +let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature -> unit) : unit = + let gr_c = Libnames.constr_of_global gr in + let (smap:(Libnames.global_reference * Evd.evar_map, + ('a * 'b * Term.constr) list * Evd.evar) + Gmapl.t ref) = ref Gmapl.empty in + iter_under_prod + ( fun ctx typ -> + List.iter + (fun ((cl,ev,evm),_,_) -> +(* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_map evm);*) + smap := Gmapl.add (cl,evm) (ctx,ev) !smap) + (Recordops.methods_matching typ) + ) [] deftyp; + Gmapl.iter + ( fun (cl,evm) evl -> + let f = if Typeclasses.is_class cl then + declare_class_instance else declare_record_instance in + complete_with_evars_permut (cl,[],evm) evl gr_c + (fun sign -> complete_signature (k f) sign) + ) !smap + +(* + * Interface with other parts: hooks & declaration + *) + + +let evar_definition evi = match evar_body evi with + Evar_empty -> assert false | Evar_defined c -> c + +let gen_sort_topo l evm = + let iter_evar f ev = + let rec aux c = match kind_of_term c with + Evar (e,_) -> f e + | _ -> iter_constr aux c in + aux (Evd.evar_concl (Evd.find evm ev)); + if Evd.is_defined evm ev then aux (evar_definition (Evd.find evm ev)) in + let r = ref [] in + let rec dfs ev = iter_evar dfs ev; + if not(List.mem ev !r) then r := ev::!r in + List.iter dfs l; List.rev !r + +(* register real typeclass instance given a totally defined evd *) +let declare_instance (k:global_reference -> rel_context -> constr list -> unit) + (cl,gen,evm:signature) = + let evm = Evarutil.nf_evars evm in + let gen = gen_sort_topo gen evm in + let (evm,gen) = List.fold_right + (fun ev (evm,gen) -> + if Evd.is_defined evm ev + then Evd.remove evm ev,gen + else evm,(ev::gen)) + gen (evm,[]) in +(* msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_map evm);*) + let ngen = List.length gen in + let (_,ctx,evm) = List.fold_left + ( fun (i,ctx,evm) ev -> + let ctx = (Anonymous,None,lift (-i) (Evd.evar_concl(Evd.find evm ev)))::ctx in + let evm = subst_evar_in_evm ev (mkRel i) (Evd.remove evm ev) in + (i-1,ctx,evm) + ) (ngen,[],evm) gen in + let fields = List.rev (Evd.fold ( fun ev evi l -> evar_definition evi::l ) evm []) in + k cl ctx fields + +let autoinstance_opt = ref true + +let search_declaration gr = + if !autoinstance_opt && + not (Lib.is_modtype()) then + let deftyp = Global.type_of_global gr in + complete_signature_with_def gr deftyp declare_instance + +let search_record k cons sign = + if !autoinstance_opt && not (Lib.is_modtype()) then + complete_signature (declare_instance k) (cons,[],sign) + +(* +let dh_key = Profile.declare_profile "declaration_hook" +let ch_key = Profile.declare_profile "class_decl_hook" +let declaration_hook = Profile.profile1 dh_key declaration_hook +let class_decl_hook = Profile.profile1 ch_key class_decl_hook +*) + +(* + * Options and bookeeping + *) + +let begin_autoinstance () = + if not !autoinstance_opt then ( + autoinstance_opt := true; + ) + +let end_autoinstance () = + if !autoinstance_opt then ( + autoinstance_opt := false; + ) + +let _ = + Goptions.declare_bool_option + { Goptions.optsync=true; + Goptions.optkey=Goptions.PrimaryTable("Autoinstance"); + Goptions.optname="automatic typeclass instance recognition"; + Goptions.optread=(fun () -> !autoinstance_opt); + Goptions.optwrite=(fun b -> if b then begin_autoinstance() else end_autoinstance()) } diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli new file mode 100644 index 0000000000..3866fff39f --- /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 8d480ef2f2..89739b9840 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 0000000000..6fd49b15b9 --- /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 0000000000..be5e9312a2 --- /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 9978d7bf6d..3ef7eccad9 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 3fe18e1926..564d4409f0 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/toplevel/search.ml b/toplevel/search.ml new file mode 100644 index 0000000000..e50af97332 --- /dev/null +++ b/toplevel/search.ml @@ -0,0 +1,232 @@ +(************************************************************************) +(* 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$ *) + +open Pp +open Util +open Names +open Nameops +open Term +open Rawterm +open Declarations +open Libobject +open Declare +open Environ +open Pattern +open Matching +open Printer +open Libnames +open Nametab + +(* The functions print_constructors and crible implement the behavior needed + for the Coq searching commands. + These functions take as first argument the procedure + that will be called to treat each entry. This procedure receives the name + of the object, the assumptions that will make it possible to print its type, + and the constr term that represent its type. *) + +let print_constructors indsp fn env nconstr = + for i = 1 to nconstr do + fn (ConstructRef (indsp,i)) env (Inductiveops.type_of_constructor env (indsp,i)) + done + +let rec head_const c = match kind_of_term c with + | Prod (_,_,d) -> head_const d + | LetIn (_,_,_,d) -> head_const d + | App (f,_) -> head_const f + | Cast (d,_,_) -> head_const d + | _ -> c + +(* General search, restricted to head constant if [only_head] *) + +let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = + let env = Global.env () in + let crible_rec (sp,_) lobj = match object_tag lobj with + | "VARIABLE" -> + (try + let (id,_,typ) = Global.lookup_named (basename sp) in + if refopt = None + || head_const typ = constr_of_global (Option.get refopt) + then + fn (VarRef id) env typ + with Not_found -> (* we are in a section *) ()) + | "CONSTANT" -> + let cst = locate_constant (qualid_of_sp sp) in + let typ = Typeops.type_of_constant env cst in + if refopt = None + || head_const typ = constr_of_global (Option.get refopt) + then + fn (ConstRef cst) env typ + | "INDUCTIVE" -> + let kn = locate_mind (qualid_of_sp sp) in + let mib = Global.lookup_mind kn in + (match refopt with + | Some (IndRef ((kn',tyi) as ind)) when kn=kn' -> + print_constructors ind fn env + (Array.length (mib.mind_packets.(tyi).mind_user_lc)) + | Some _ -> () + | _ -> + Array.iteri + (fun i mip -> print_constructors (kn,i) fn env + (Array.length mip.mind_user_lc)) mib.mind_packets) + | _ -> () + in + try + Declaremods.iter_all_segments crible_rec + with Not_found -> + () + +let crible ref = gen_crible (Some ref) + +(* Fine Search. By Yves Bertot. *) + +exception No_section_path + +let rec head c = + let c = strip_outer_cast c in + match kind_of_term c with + | Prod (_,_,c) -> head c + | LetIn (_,_,_,c) -> head c + | _ -> c + +let constr_to_section_path c = match kind_of_term c with + | Const sp -> sp + | _ -> raise No_section_path + +let xor a b = (a or b) & (not (a & b)) + +let plain_display ref a c = + let pc = pr_lconstr_env a c in + let pr = pr_global ref in + msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ()) + +let filter_by_module (module_list:dir_path list) (accept:bool) + (ref:global_reference) _ _ = + try + let sp = sp_of_global ref in + let sl = dirpath sp in + let rec filter_aux = function + | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl) + | [] -> true + in + xor accept (filter_aux module_list) + with No_section_path -> + false + +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 |]) + +let mk_rewrite_pattern2 eq pattern = + PApp (PRef eq, [| PMeta None; PMeta None; pattern |]) + +let pattern_filter pat _ a c = + try + try + is_matching pat (head c) + with _ -> + is_matching + pat (head (Typing.type_of (Global.env()) Evd.empty c)) + with UserError _ -> + false + +let filtered_search filter_function display_function ref = + crible ref + (fun s a c -> if filter_function s a c then display_function s a c) + +let rec id_from_pattern = function + | PRef gr -> gr +(* should be appear as a PRef (VarRef sp) !! + | PVar id -> Nametab.locate (make_qualid [] (string_of_id id)) + *) + | PApp (p,_) -> id_from_pattern p + | _ -> error "The pattern is not simple enough." + +let raw_pattern_search extra_filter display_function pat = + let name = id_from_pattern pat in + filtered_search + (fun s a c -> (pattern_filter pat s a c) & extra_filter s a c) + display_function name + +let raw_search_rewrite extra_filter display_function pattern = + filtered_search + (fun s a c -> + ((pattern_filter (mk_rewrite_pattern1 gref_eq pattern) s a c) || + (pattern_filter (mk_rewrite_pattern2 gref_eq pattern) s a c)) + && 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 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 + +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) + +(** SearchAbout *) + +let name_of_reference ref = string_of_id (id_of_global ref) + +type glob_search_about_item = + | GlobSearchSubPattern of constr_pattern + | GlobSearchString of string + +let search_about_item (itemref,typ) = function + | GlobSearchSubPattern pat -> is_matching_appsubterm ~closed:false pat typ + | GlobSearchString s -> string_string_contains (name_of_reference itemref) s + +let raw_search_about filter_modules display_function l = + let filter ref' env typ = + filter_modules ref' env typ && + List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l && + not (string_string_contains (name_of_reference ref') "_subproof") + in + gen_filtered_search filter display_function + +let search_about ref inout = + raw_search_about (filter_by_module_from_list inout) plain_display ref diff --git a/toplevel/search.mli b/toplevel/search.mli new file mode 100644 index 0000000000..5b978770b0 --- /dev/null +++ b/toplevel/search.mli @@ -0,0 +1,52 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id$ i*) + +open Pp +open Names +open Term +open Environ +open Pattern +open Libnames +open Nametab + +(*s Search facilities. *) + +type glob_search_about_item = + | GlobSearchSubPattern of constr_pattern + | GlobSearchString of string + +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. + It can be passed as argument to the raw search functions. + It is used in pcoq. *) + +val filter_by_module_from_list : + dir_path list * bool -> global_reference -> env -> 'a -> bool + +(* raw search functions can be used for various extensions. + They are also used for pcoq. *) +val gen_filtered_search : (global_reference -> env -> constr -> bool) -> + (global_reference -> env -> constr -> unit) -> unit +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 -> unit +val raw_search_rewrite : (global_reference -> env -> constr -> bool) -> + (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 a4d3e5458a..37e9cf22ae 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 5ea0235a5a..9412a5981c 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 |