From 4425c8d353ffdcbed966c253f9624b550626ae0a Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 11 Mar 2013 20:14:31 +0000 Subject: Added a Local Definition vernacular command. This type of definition has to be refered through its qualified name even when the module containing it is imported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16263 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declare.ml | 67 +++++++++++++++++++++++++++++++++++------------------ library/declare.mli | 4 ++-- library/kindops.ml | 56 ++++++++++++++++++++++++++++++++------------ 3 files changed, 87 insertions(+), 40 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index ee4656f75..ca18874d4 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -100,20 +100,30 @@ let declare_variable id obj = (** Declaration of constants and parameters *) +type constant_obj = { + cst_decl : global_declaration; + cst_hyps : Dischargedhypsmap.discharged_hyps; + cst_kind : logical_kind; + cst_locl : bool; +} + type constant_declaration = constant_entry * logical_kind (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) -let load_constant i ((sp,kn),(_,_,kind)) = +let load_constant i ((sp,kn), obj) = if Nametab.exists_cci sp then alreadydeclared (pr_id (basename sp) ++ str " already exists"); let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Until i) sp (ConstRef con); - add_constant_kind con kind + add_constant_kind con obj.cst_kind (* Opening means making the name without its module qualification available *) -let open_constant i ((sp,kn),_) = - let con = Global.constant_of_delta_kn kn in +let open_constant i ((sp,kn), obj) = + (** Never open a local definition *) + if obj.cst_locl then () + else + let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Exactly i) sp (ConstRef con) let exists_name id = @@ -123,16 +133,16 @@ let check_exists sp = let id = basename sp in if exists_name id then alreadydeclared (pr_id id ++ str " already exists") -let cache_constant ((sp,kn),(cdt,dhyps,kind)) = +let cache_constant ((sp,kn), obj) = let id = basename sp in let _,dir,_ = repr_kn kn in - check_exists sp; - let kn' = Global.add_constant dir id cdt in + let () = check_exists sp in + let kn' = Global.add_constant dir id obj.cst_decl in assert (eq_constant kn' (constant_of_kn kn)); 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; + Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; + add_constant_kind (constant_of_kn kn) obj.cst_kind; !cache_hook sp let discharged_hyps kn sechyps = @@ -140,24 +150,28 @@ let discharged_hyps kn sechyps = let args = Array.to_list (instance_from_variable_context sechyps) in List.rev_map (Libnames.make_path dir) args -let discharge_constant ((sp,kn),(cdt,dhyps,kind)) = +let discharge_constant ((sp, kn), obj) = let con = constant_of_kn kn in let cb = Global.lookup_constant con in let repl = replacement_context () in let sechyps = section_segment_of_constant con in let recipe = { d_from=cb; d_modlist=repl; d_abstract=named_of_variable_context sechyps } in - Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind) + let new_hyps = (discharged_hyps kn sechyps) @ obj.cst_hyps in + let new_decl = GlobalRecipe recipe in + Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry (ParameterEntry (None,mkProp,None)) -let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk +let dummy_constant cst = { + cst_decl = dummy_constant_entry; + cst_hyps = []; + cst_kind = cst.cst_kind; + cst_locl = cst.cst_locl; +} let classify_constant cst = Substitute (dummy_constant cst) -type constant_obj = - global_declaration * Dischargedhypsmap.discharged_hyps * logical_kind - let inConstant : constant_obj -> obj = declare_object { (default_object "CONSTANT") with cache_function = cache_constant; @@ -167,20 +181,27 @@ let inConstant : constant_obj -> obj = subst_function = ident_subst_function; discharge_function = discharge_constant } -let declare_constant_common id dhyps (cd,kind) = - let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in +let declare_constant_common id cst = + let (sp,kn) = add_leaf id (inConstant cst) in let c = Global.constant_of_delta_kn kn in declare_constant_implicits c; Heads.declare_head (EvalConstRef c); Notation.declare_ref_arguments_scope (ConstRef c); c -let declare_constant ?(internal = UserVerbose) id (cd,kind) = - let kn = declare_constant_common id [] (ConstantEntry cd,kind) in - !xml_declare_constant (internal,kn); +let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) = + let cst = { + cst_decl = ConstantEntry cd; + cst_hyps = [] ; + cst_kind = kind; + cst_locl = local; + } in + let kn = declare_constant_common id cst in + let () = !xml_declare_constant (internal, kn) in kn -let declare_definition ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds.Definition) +let declare_definition ?(internal=UserVerbose) + ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) id ?types body = let cb = { Entries.const_entry_body = body; @@ -189,8 +210,8 @@ let declare_definition ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds const_entry_inline_code = false; const_entry_secctx = None } in - declare_constant ~internal id - (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) + declare_constant ~internal ~local id + (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of inductive blocks *) diff --git a/library/declare.mli b/library/declare.mli index bcb72be58..fa9917a13 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -55,11 +55,11 @@ type internal_flag = | UserVerbose val declare_constant : - ?internal:internal_flag -> Id.t -> constant_declaration -> constant + ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> constant val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> - Id.t -> ?types:constr -> constr -> constant + ?local:bool -> Id.t -> ?types:constr -> constr -> constant (** [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of diff --git a/library/kindops.ml b/library/kindops.ml index 35aebc531..6e6c7527b 100644 --- a/library/kindops.ml +++ b/library/kindops.ml @@ -24,18 +24,44 @@ let string_of_theorem_kind = function | Corollary -> "Corollary" let string_of_definition_kind def = - match def with - | Local, Coercion -> "Coercion Local" - | Global, Coercion -> "Coercion" - | Local, Definition -> "Let" - | Global, Definition -> "Definition" - | Local, SubClass -> "Local SubClass" - | Global, SubClass -> "SubClass" - | Global, CanonicalStructure -> "Canonical Structure" - | Global, Example -> "Example" - | Local, (CanonicalStructure|Example) -> - Errors.anomaly (Pp.str "Unsupported local definition kind") - | Local, Instance -> "Instance" - | Global, Instance -> "Global Instance" - | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) - -> Errors.anomaly (Pp.str "Internal definition kind") + let (locality, kind) = def in + let error () = Errors.anomaly (Pp.str "Internal definition kind") in + match kind with + | Definition -> + begin match locality with + | Discharge -> "Let" + | Local -> "Local Definition" + | Global -> "Definition" + end + | Example -> + begin match locality with + | Discharge -> error () + | Local -> "Local Example" + | Global -> "Example" + end + | Coercion -> + begin match locality with + | Discharge -> error () + | Local -> "Local Coercion" + | Global -> "Coercion" + end + | SubClass -> + begin match locality with + | Discharge -> error () + | Local -> "Local SubClass" + | Global -> "SubClass" + end + | CanonicalStructure -> + begin match locality with + | Discharge -> error () + | Local -> error () + | Global -> "Canonical Structure" + end + | Instance -> + begin match locality with + | Discharge -> error () + | Local -> "Instance" + | Global -> "Global Instance" + end + | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> + Errors.anomaly (Pp.str "Internal definition kind") -- cgit v1.2.3