From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- library/global.mli | 165 ++++++++++++++++++++++++++++++++--------------------- 1 file changed, 101 insertions(+), 64 deletions(-) (limited to 'library/global.mli') diff --git a/library/global.mli b/library/global.mli index e1cd5c7b..af23d9b7 100644 --- a/library/global.mli +++ b/library/global.mli @@ -1,106 +1,143 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* safe_environment +val safe_env : unit -> Safe_typing.safe_environment val env : unit -> Environ.env -val env_is_empty : unit -> bool +val env_is_initial : unit -> bool -val universes : unit -> universes +val universes : unit -> Univ.universes val named_context_val : unit -> Environ.named_context_val -val named_context : unit -> Sign.named_context +val named_context : unit -> Context.named_context -val env_is_empty : unit -> bool +(** {6 Enriching the global environment } *) -(** {6 Extending env with variables and local definitions } *) -val push_named_assum : (identifier * types) -> Univ.constraints -val push_named_def : (identifier * constr * types option) -> Univ.constraints +(** Changing the (im)predicativity of the system *) +val set_engagement : Declarations.engagement -> unit +val set_type_in_type : unit -> unit -(** {6 ... } *) -(** Adding constants, inductives, modules and module types. All these - functions verify that given names match those generated by kernel *) +(** Variables, Local definitions, constants, inductive types *) + +val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit +val push_named_def : (Id.t * Entries.definition_entry) -> unit val add_constant : - dir_path -> identifier -> global_declaration -> constant -val add_mind : - dir_path -> identifier -> mutual_inductive_entry -> mutual_inductive - -val add_module : - identifier -> module_entry -> inline -> module_path * delta_resolver -val add_modtype : - identifier -> module_struct_entry -> inline -> module_path -val add_include : - module_struct_entry -> bool -> inline -> delta_resolver + DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant +val add_mind : + DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive -val add_constraints : constraints -> unit +(** Extra universe constraints *) +val add_constraints : Univ.constraints -> unit -val set_engagement : engagement -> unit +val push_context : Univ.universe_context -> unit +val push_context_set : Univ.universe_context_set -> unit -(** {6 Interactive modules and module types } - Both [start_*] functions take the [dir_path] argument to create a - [mod_self_id]. This should be the name of the compilation unit. *) +(** Non-interactive modules and module types *) -(** [start_*] functions return the [module_path] valid for components - of the started module / module type *) +val add_module : + Id.t -> Entries.module_entry -> Declarations.inline -> + module_path * Mod_subst.delta_resolver +val add_modtype : + Id.t -> Entries.module_type_entry -> Declarations.inline -> module_path +val add_include : + Entries.module_struct_entry -> bool -> Declarations.inline -> + Mod_subst.delta_resolver -val start_module : identifier -> module_path +(** Interactive modules and module types *) -val end_module : Summary.frozen ->identifier -> - (module_struct_entry * inline) option -> module_path * delta_resolver +val start_module : Id.t -> module_path +val start_modtype : Id.t -> module_path -val add_module_parameter : - mod_bound_id -> module_struct_entry -> inline -> delta_resolver +val end_module : Summary.frozen -> Id.t -> + (Entries.module_struct_entry * Declarations.inline) option -> + module_path * MBId.t list * Mod_subst.delta_resolver -val start_modtype : identifier -> module_path -val end_modtype : Summary.frozen -> identifier -> module_path -val pack_module : unit -> module_body +val end_modtype : Summary.frozen -> Id.t -> module_path * MBId.t list +val add_module_parameter : + MBId.t -> Entries.module_struct_entry -> Declarations.inline -> + Mod_subst.delta_resolver + +(** {6 Queries in the global environment } *) + +val lookup_named : variable -> Context.named_declaration +val lookup_constant : constant -> Declarations.constant_body +val lookup_inductive : inductive -> + Declarations.mutual_inductive_body * Declarations.one_inductive_body +val lookup_pinductive : Constr.pinductive -> + Declarations.mutual_inductive_body * Declarations.one_inductive_body +val lookup_mind : mutual_inductive -> Declarations.mutual_inductive_body +val lookup_module : module_path -> Declarations.module_body +val lookup_modtype : module_path -> Declarations.module_type_body +val exists_objlabel : Label.t -> bool -(** Queries *) -val lookup_named : variable -> named_declaration -val lookup_constant : constant -> constant_body -val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body -val lookup_mind : mutual_inductive -> mutual_inductive_body -val lookup_module : module_path -> module_body -val lookup_modtype : module_path -> module_type_body val constant_of_delta_kn : kernel_name -> constant val mind_of_delta_kn : kernel_name -> mutual_inductive -val exists_objlabel : label -> bool -(** Compiled modules *) -val start_library : dir_path -> module_path -val export : dir_path -> module_path * compiled_library -val import : compiled_library -> Digest.t -> module_path +val opaque_tables : unit -> Opaqueproof.opaquetab +val body_of_constant : constant -> Term.constr option +val body_of_constant_body : Declarations.constant_body -> Term.constr option +val constraints_of_constant_body : + Declarations.constant_body -> Univ.constraints +val universes_of_constant_body : + Declarations.constant_body -> Univ.universe_context + +(** {6 Compiled libraries } *) + +val start_library : DirPath.t -> module_path +val export : ?except:Future.UUIDSet.t -> DirPath.t -> + module_path * Safe_typing.compiled_library * Safe_typing.native_library +val import : + Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest -> + module_path * Nativecode.symbol array + +(** {6 Misc } *) -(** {6 ... } *) (** Function to get an environment from the constants part of the global * environment and a given context. *) -val type_of_global : Libnames.global_reference -> types val env_of_context : Environ.named_context_val -> Environ.env +val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit + +val is_polymorphic : Globnames.global_reference -> bool +val is_template_polymorphic : Globnames.global_reference -> bool + +val type_of_global_in_context : Environ.env -> + Globnames.global_reference -> Constr.types Univ.in_universe_context +val type_of_global_unsafe : Globnames.global_reference -> Constr.types + +(** Returns the universe context of the global reference (whatever it's polymorphic status is). *) +val universes_of_global : Globnames.global_reference -> Univ.universe_context + +(** {6 Retroknowledge } *) + +val register : + Retroknowledge.field -> Term.constr -> Term.constr -> unit + +val register_inline : constant -> unit + +(** {6 Oracle } *) + +val set_strategy : Names.constant Names.tableKey -> Conv_oracle.level -> unit + +(* Modifies the global state, registering new universes *) + +val current_dirpath : unit -> Names.dir_path + +val with_global : (Environ.env -> Names.dir_path -> 'a Univ.in_universe_context_set) -> 'a -(** spiwack: register/unregister function for retroknowledge *) -val register : Retroknowledge.field -> constr -> constr -> unit +val global_env_summary_name : string -- cgit v1.2.3