diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/command.ml | 63 | ||||
| -rw-r--r-- | vernac/command.mli | 7 | ||||
| -rw-r--r-- | vernac/declareDef.ml | 64 | ||||
| -rw-r--r-- | vernac/declareDef.mli | 19 | ||||
| -rw-r--r-- | vernac/obligations.ml | 11 | ||||
| -rw-r--r-- | vernac/obligations.mli | 11 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 1 |
8 files changed, 92 insertions, 86 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 007b70bc0..2e8ebb853 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -417,7 +417,7 @@ let context poly l = let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in let hook = Lemmas.mk_hook (fun _ gr -> gr) in - let _ = Command.declare_definition id decl entry [] [] hook in + let _ = DeclareDef.declare_definition id decl entry [] [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus diff --git a/vernac/command.ml b/vernac/command.ml index 68fa8ab88..fd49e5324 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -145,54 +145,6 @@ let check_definition (ce, evd, _, imps) = check_evars_are_solved (Global.env ()) evd Evd.empty; ce -let warn_local_declaration = - CWarnings.create ~name:"local-declaration" ~category:"scope" - (fun (id,kind) -> - pr_id id ++ strbrk " is declared as a local " ++ str kind) - -let get_locality id ~kind = function -| Discharge -> - (** If a Let is defined outside a section, then we consider it as a local definition *) - warn_local_declaration (id,kind); - true -| Local -> true -| Global -> false - -let declare_global_definition ident ce local k pl imps = - let local = get_locality ident ~kind:"definition" local in - let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in - let gr = ConstRef kn in - let () = maybe_declare_manual_implicits false gr imps in - let () = Universes.register_universe_binders gr pl in - let () = definition_message ident in - gr - -let warn_definition_not_visible = - CWarnings.create ~name:"definition-not-visible" ~category:"implicits" - (fun ident -> - strbrk "Section definition " ++ - pr_id ident ++ strbrk " is not visible from current goals") - -let declare_definition ident (local, p, k) ce pl imps hook = - let fix_exn = Future.fix_exn_of ce.const_entry_body in - let r = match local with - | Discharge when Lib.sections_are_opened () -> - let c = SectionLocalDef ce in - let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in - let () = definition_message ident in - let gr = VarRef ident in - let () = maybe_declare_manual_implicits false gr imps in - let () = if Proof_global.there_are_pending_proofs () then - warn_definition_not_visible ident - in - gr - | Discharge | Local | Global -> - declare_global_definition ident ce local k pl imps in - Lemmas.call_hook fix_exn hook local r - -let _ = Obligations.declare_definition_ref := - (fun i k c imps hook -> declare_definition i k c [] imps hook) - let do_definition ident k pl bl red_option c ctypopt hook = let (ce, evd, pl', imps as def) = interp_definition pl bl (pi2 k) red_option c ctypopt @@ -215,7 +167,7 @@ let do_definition ident k pl bl red_option c ctypopt hook = ignore(Obligations.add_definition ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in - ignore(declare_definition ident k ce pl' imps + ignore(DeclareDef.declare_definition ident k ce pl' imps (Lemmas.mk_hook (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) @@ -238,7 +190,7 @@ match local with (r,Univ.Instance.empty,true) | Global | Local | Discharge -> - let local = get_locality ident ~kind:"axiom" local in + let local = DeclareDef.get_locality ident ~kind:"axiom" local in let inl = match nl with | NoInline -> None | DefaultInline -> Some (Flags.get_inline_level()) @@ -871,13 +823,6 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl = let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx -let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = - let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in - declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) - -let _ = Obligations.declare_fix_ref := - (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps) - let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in let names = List.map (fun id -> Name id) fixnames in @@ -1221,7 +1166,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let evd = Evd.restrict_universe_context evd vars in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let pl, ctx = Evd.universe_context ?names:pl evd in - ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx) + ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) fixpoint_message (Some indexes) fixnames; @@ -1252,7 +1197,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in let pl, ctx = Evd.universe_context ?names:pl evd in - ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx) + ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames diff --git a/vernac/command.mli b/vernac/command.mli index f7d90ce60..1887885de 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -30,10 +30,6 @@ val interp_definition : constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Universes.universe_binders * Impargs.manual_implicits -val declare_definition : Id.t -> definition_kind -> - Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> - Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference - val do_definition : Id.t -> definition_kind -> lident list option -> local_binder_expr list -> red_expr option -> constr_expr -> constr_expr option -> unit Lemmas.declaration_hook -> unit @@ -165,6 +161,3 @@ val do_cofixpoint : (** Utils *) val check_mutuality : Environ.env -> Evd.evar_map -> bool -> (Id.t * types) list -> unit - -val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> - Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml new file mode 100644 index 000000000..d7a4fcca3 --- /dev/null +++ b/vernac/declareDef.ml @@ -0,0 +1,64 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Decl_kinds +open Declare +open Entries +open Globnames +open Impargs +open Nameops + +let warn_definition_not_visible = + CWarnings.create ~name:"definition-not-visible" ~category:"implicits" + Pp.(fun ident -> + strbrk "Section definition " ++ + pr_id ident ++ strbrk " is not visible from current goals") + +let warn_local_declaration = + CWarnings.create ~name:"local-declaration" ~category:"scope" + Pp.(fun (id,kind) -> + pr_id id ++ strbrk " is declared as a local " ++ str kind) + +let get_locality id ~kind = function +| Discharge -> + (** If a Let is defined outside a section, then we consider it as a local definition *) + warn_local_declaration (id,kind); + true +| Local -> true +| Global -> false + +let declare_global_definition ident ce local k pl imps = + let local = get_locality ident ~kind:"definition" local in + let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in + let gr = ConstRef kn in + let () = maybe_declare_manual_implicits false gr imps in + let () = Universes.register_universe_binders gr pl in + let () = definition_message ident in + gr + +let declare_definition ident (local, p, k) ce pl imps hook = + let fix_exn = Future.fix_exn_of ce.const_entry_body in + let r = match local with + | Discharge when Lib.sections_are_opened () -> + let c = SectionLocalDef ce in + let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in + let () = definition_message ident in + let gr = VarRef ident in + let () = maybe_declare_manual_implicits false gr imps in + let () = if Proof_global.there_are_pending_proofs () then + warn_definition_not_visible ident + in + gr + | Discharge | Local | Global -> + declare_global_definition ident ce local k pl imps in + Lemmas.call_hook fix_exn hook local r + +let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = + let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in + declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) + diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli new file mode 100644 index 000000000..5dea0ba27 --- /dev/null +++ b/vernac/declareDef.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Decl_kinds +open Names + +val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool + +val declare_definition : Id.t -> definition_kind -> + Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> + Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference + +val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> + Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 135e4c63a..c0acdaf57 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -22,9 +22,6 @@ open Util module NamedDecl = Context.Named.Declaration -let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false) -let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false) - let get_fix_exn, stm_get_fix_exn = Hook.make () let succfix (depth, fixrels) = @@ -496,14 +493,12 @@ let declare_definition prg = in let () = progmap_remove prg in let cst = - !declare_definition_ref prg.prg_name - prg.prg_kind ce prg.prg_implicits + DeclareDef.declare_definition prg.prg_name + prg.prg_kind ce [] prg.prg_implicits (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) in Universes.register_universe_binders cst pl; cst - -open Pp let rec lam_index n t acc = match kind_of_term t with @@ -569,7 +564,7 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let ctx = Evd.evar_context_universe_context first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx) + let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter Metasyntax.add_notation_interpretation first.prg_notations; diff --git a/vernac/obligations.mli b/vernac/obligations.mli index a276f9f9a..9cbbf6082 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -12,23 +12,12 @@ open Evd open Names open Pp open Globnames -open Decl_kinds - -(** Forward declaration. *) -val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> - Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref - -val declare_definition_ref : - (Id.t -> definition_kind -> - Safe_typing.private_constants Entries.definition_entry -> Impargs.manual_implicits - -> global_reference Lemmas.declaration_hook -> global_reference) ref (* This is a hack to make it possible for Obligations to craft a Qed * behind the scenes. The fix_exn the Stm attaches to the Future proof * is not available here, so we provide a side channel to get it *) val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t - val check_evars : env -> evar_map -> unit val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index d631fae8a..f74073e1f 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -8,6 +8,7 @@ Metasyntax Auto_ind_decl Search Indschemes +DeclareDef Obligations Command Classes |