diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/coqlib.ml | 34 | ||||
| -rw-r--r-- | library/coqlib.mli | 123 | ||||
| -rw-r--r-- | library/decl_kinds.ml | 87 | ||||
| -rw-r--r-- | library/declaremods.ml | 16 | ||||
| -rw-r--r-- | library/declaremods.mli | 16 | ||||
| -rw-r--r-- | library/global.mli | 12 | ||||
| -rw-r--r-- | library/globnames.ml | 13 | ||||
| -rw-r--r-- | library/globnames.mli | 55 | ||||
| -rw-r--r-- | library/keys.ml | 7 | ||||
| -rw-r--r-- | library/keys.mli | 4 | ||||
| -rw-r--r-- | library/lib.ml | 25 | ||||
| -rw-r--r-- | library/lib.mli | 72 | ||||
| -rw-r--r-- | library/libnames.ml | 3 | ||||
| -rw-r--r-- | library/libnames.mli | 2 | ||||
| -rw-r--r-- | library/library.mllib | 2 | ||||
| -rw-r--r-- | library/misctypes.ml | 130 | ||||
| -rw-r--r-- | library/nametab.ml | 1 | ||||
| -rw-r--r-- | library/nametab.mli | 22 |
18 files changed, 423 insertions, 201 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index 3f01c617c5..408e259196 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -171,16 +171,16 @@ let jmeq_kn = make_ind jmeq_module "JMeq" let glob_jmeq = IndRef (jmeq_kn,0) type coq_sigma_data = { - proj1 : global_reference; - proj2 : global_reference; - elim : global_reference; - intro : global_reference; - typ : global_reference } + proj1 : GlobRef.t; + proj2 : GlobRef.t; + elim : GlobRef.t; + intro : GlobRef.t; + typ : GlobRef.t } type coq_bool_data = { - andb : global_reference; - andb_prop : global_reference; - andb_true_intro : global_reference} + andb : GlobRef.t; + andb_prop : GlobRef.t; + andb_true_intro : GlobRef.t} let build_bool_type () = { andb = init_reference ["Datatypes"] "andb"; @@ -213,18 +213,18 @@ let build_prod () = (* Equalities *) type coq_eq_data = { - eq : global_reference; - ind : global_reference; - refl : global_reference; - sym : global_reference; - trans: global_reference; - congr: global_reference } + eq : GlobRef.t; + ind : GlobRef.t; + refl : GlobRef.t; + sym : GlobRef.t; + trans: GlobRef.t; + congr: GlobRef.t } (* Data needed for discriminate and injection *) type coq_inversion_data = { - inv_eq : global_reference; (* : forall params, t -> Prop *) - inv_ind : global_reference; (* : forall params P y, eq params y -> P y *) - inv_congr: global_reference (* : forall params B (f:t->B) y, eq params y -> f c=f y *) + inv_eq : GlobRef.t; (* : forall params, t -> Prop *) + inv_ind : GlobRef.t; (* : forall params P y, eq params y -> P y *) + inv_congr: GlobRef.t (* : forall params B (f:t->B) y, eq params y -> f c=f y *) } let lazy_init_reference dir id = lazy (init_reference dir id) diff --git a/library/coqlib.mli b/library/coqlib.mli index 8077c47c72..b4bd1b0e06 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -8,10 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Util open Names open Libnames -open Globnames -open Util (** This module collects the global references, constructions and patterns of the standard library used in ocaml files *) @@ -44,14 +43,14 @@ open Util type message = string -val find_reference : message -> string list -> string -> global_reference -val coq_reference : message -> string list -> string -> global_reference +val find_reference : message -> string list -> string -> GlobRef.t +val coq_reference : message -> string list -> string -> GlobRef.t (** For tactics/commands requiring vernacular libraries *) val check_required_library : string list -> unit (** Search in several modules (not prefixed by "Coq") *) -val gen_reference_in_modules : string->string list list-> string -> global_reference +val gen_reference_in_modules : string->string list list-> string -> GlobRef.t val arith_modules : string list list val zarith_base_modules : string list list @@ -78,24 +77,24 @@ val type_of_id : Constant.t (** Natural numbers *) val nat_path : full_path -val glob_nat : global_reference +val glob_nat : GlobRef.t val path_of_O : constructor val path_of_S : constructor -val glob_O : global_reference -val glob_S : global_reference +val glob_O : GlobRef.t +val glob_S : GlobRef.t (** Booleans *) -val glob_bool : global_reference +val glob_bool : GlobRef.t val path_of_true : constructor val path_of_false : constructor -val glob_true : global_reference -val glob_false : global_reference +val glob_true : GlobRef.t +val glob_false : GlobRef.t (** Equality *) -val glob_eq : global_reference -val glob_identity : global_reference -val glob_jmeq : global_reference +val glob_eq : GlobRef.t +val glob_identity : GlobRef.t +val glob_jmeq : GlobRef.t (** {6 ... } *) (** Constructions and patterns related to Coq initial state are unknown @@ -106,18 +105,18 @@ val glob_jmeq : global_reference at runtime. *) type coq_bool_data = { - andb : global_reference; - andb_prop : global_reference; - andb_true_intro : global_reference} + andb : GlobRef.t; + andb_prop : GlobRef.t; + andb_true_intro : GlobRef.t} val build_bool_type : coq_bool_data delayed (** {6 For Equality tactics } *) type coq_sigma_data = { - proj1 : global_reference; - proj2 : global_reference; - elim : global_reference; - intro : global_reference; - typ : global_reference } + proj1 : GlobRef.t; + proj2 : GlobRef.t; + elim : GlobRef.t; + intro : GlobRef.t; + typ : GlobRef.t } val build_sigma_set : coq_sigma_data delayed val build_sigma_type : coq_sigma_data delayed @@ -132,30 +131,30 @@ val build_sigma : coq_sigma_data delayed val build_prod : coq_sigma_data delayed type coq_eq_data = { - eq : global_reference; - ind : global_reference; - refl : global_reference; - sym : global_reference; - trans: global_reference; - congr: global_reference } + eq : GlobRef.t; + ind : GlobRef.t; + refl : GlobRef.t; + sym : GlobRef.t; + trans: GlobRef.t; + congr: GlobRef.t } val build_coq_eq_data : coq_eq_data delayed val build_coq_identity_data : coq_eq_data delayed val build_coq_jmeq_data : coq_eq_data delayed -val build_coq_eq : global_reference delayed (** = [(build_coq_eq_data()).eq] *) -val build_coq_eq_refl : global_reference delayed (** = [(build_coq_eq_data()).refl] *) -val build_coq_eq_sym : global_reference delayed (** = [(build_coq_eq_data()).sym] *) -val build_coq_f_equal2 : global_reference delayed +val build_coq_eq : GlobRef.t delayed (** = [(build_coq_eq_data()).eq] *) +val build_coq_eq_refl : GlobRef.t delayed (** = [(build_coq_eq_data()).refl] *) +val build_coq_eq_sym : GlobRef.t delayed (** = [(build_coq_eq_data()).sym] *) +val build_coq_f_equal2 : GlobRef.t delayed (** Data needed for discriminate and injection *) type coq_inversion_data = { - inv_eq : global_reference; (** : forall params, args -> Prop *) - inv_ind : global_reference; (** : forall params P (H : P params) args, eq params args + inv_eq : GlobRef.t; (** : forall params, args -> Prop *) + inv_ind : GlobRef.t; (** : forall params P (H : P params) args, eq params args -> P args *) - inv_congr: global_reference (** : forall params B (f:t->B) args, eq params args -> + inv_congr: GlobRef.t (** : forall params B (f:t->B) args, eq params args -> f params = f args *) } @@ -165,45 +164,45 @@ val build_coq_inversion_jmeq_data : coq_inversion_data delayed val build_coq_inversion_eq_true_data : coq_inversion_data delayed (** Specif *) -val build_coq_sumbool : global_reference delayed +val build_coq_sumbool : GlobRef.t delayed (** {6 ... } *) (** Connectives The False proposition *) -val build_coq_False : global_reference delayed +val build_coq_False : GlobRef.t delayed (** The True proposition and its unique proof *) -val build_coq_True : global_reference delayed -val build_coq_I : global_reference delayed +val build_coq_True : GlobRef.t delayed +val build_coq_I : GlobRef.t delayed (** Negation *) -val build_coq_not : global_reference delayed +val build_coq_not : GlobRef.t delayed (** Conjunction *) -val build_coq_and : global_reference delayed -val build_coq_conj : global_reference delayed -val build_coq_iff : global_reference delayed +val build_coq_and : GlobRef.t delayed +val build_coq_conj : GlobRef.t delayed +val build_coq_iff : GlobRef.t delayed -val build_coq_iff_left_proj : global_reference delayed -val build_coq_iff_right_proj : global_reference delayed +val build_coq_iff_left_proj : GlobRef.t delayed +val build_coq_iff_right_proj : GlobRef.t delayed (** Disjunction *) -val build_coq_or : global_reference delayed +val build_coq_or : GlobRef.t delayed (** Existential quantifier *) -val build_coq_ex : global_reference delayed - -val coq_eq_ref : global_reference lazy_t -val coq_identity_ref : global_reference lazy_t -val coq_jmeq_ref : global_reference lazy_t -val coq_eq_true_ref : global_reference lazy_t -val coq_existS_ref : global_reference lazy_t -val coq_existT_ref : global_reference lazy_t -val coq_exist_ref : global_reference lazy_t -val coq_not_ref : global_reference lazy_t -val coq_False_ref : global_reference lazy_t -val coq_sumbool_ref : global_reference lazy_t -val coq_sig_ref : global_reference lazy_t - -val coq_or_ref : global_reference lazy_t -val coq_iff_ref : global_reference lazy_t +val build_coq_ex : GlobRef.t delayed + +val coq_eq_ref : GlobRef.t lazy_t +val coq_identity_ref : GlobRef.t lazy_t +val coq_jmeq_ref : GlobRef.t lazy_t +val coq_eq_true_ref : GlobRef.t lazy_t +val coq_existS_ref : GlobRef.t lazy_t +val coq_existT_ref : GlobRef.t lazy_t +val coq_exist_ref : GlobRef.t lazy_t +val coq_not_ref : GlobRef.t lazy_t +val coq_False_ref : GlobRef.t lazy_t +val coq_sumbool_ref : GlobRef.t lazy_t +val coq_sig_ref : GlobRef.t lazy_t + +val coq_or_ref : GlobRef.t lazy_t +val coq_iff_ref : GlobRef.t lazy_t diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml new file mode 100644 index 0000000000..0d32853116 --- /dev/null +++ b/library/decl_kinds.ml @@ -0,0 +1,87 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Informal mathematical status of declarations *) + +type discharge = DoDischarge | NoDischarge + +type locality = Discharge | Local | Global + +type binding_kind = Explicit | Implicit + +type polymorphic = bool + +type private_flag = bool + +type cumulative_inductive_flag = bool + +type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary + +type definition_object_kind = + | Definition + | Coercion + | SubClass + | CanonicalStructure + | Example + | Fixpoint + | CoFixpoint + | Scheme + | StructureComponent + | IdentityCoercion + | Instance + | Method + | Let + +type assumption_object_kind = Definitional | Logical | Conjectural + +(* [assumption_kind] + + | Local | Global + ------------------------------------ + Definitional | Variable | Parameter + Logical | Hypothesis | Axiom + +*) +type assumption_kind = locality * polymorphic * assumption_object_kind + +type definition_kind = locality * polymorphic * definition_object_kind + +(** Kinds used in proofs *) + +type goal_object_kind = + | DefinitionBody of definition_object_kind + | Proof of theorem_kind + +type goal_kind = locality * polymorphic * goal_object_kind + +(** Kinds used in library *) + +type logical_kind = + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind + +(** Recursive power of type declarations *) + +type recursivity_kind = Declarations.recursivity_kind = + | Finite (** = inductive *) + [@ocaml.deprecated "Please use [Declarations.Finite"] + | CoFinite (** = coinductive *) + [@ocaml.deprecated "Please use [Declarations.CoFinite"] + | BiFinite (** = non-recursive, like in "Record" definitions *) + [@ocaml.deprecated "Please use [Declarations.BiFinite"] +[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] diff --git a/library/declaremods.ml b/library/declaremods.ml index 762efc5e30..1d5df49cfd 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -17,11 +17,25 @@ open Entries open Libnames open Libobject open Mod_subst -open Vernacexpr open Misctypes (** {6 Inlining levels} *) +(** Rigid / flexible module signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Which module inline annotations should we honor, + either None or the ones whose level is less or equal + to the given integer *) + +type inline = + | NoInline + | DefaultInline + | InlineAt of int + let default_inline () = Some (Flags.get_inline_level ()) let inl2intopt = function diff --git a/library/declaremods.mli b/library/declaremods.mli index fd8d296147..4aee7feae9 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -9,10 +9,24 @@ (************************************************************************) open Names -open Vernacexpr (** {6 Modules } *) +(** Rigid / flexible module signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Which module inline annotations should we honor, + either None or the ones whose level is less or equal + to the given integer *) + +type inline = + | NoInline + | DefaultInline + | InlineAt of int + type 'modast module_interpretor = Environ.env -> Misctypes.module_kind -> 'modast -> Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t diff --git a/library/global.mli b/library/global.mli index 015f4d5822..906d246eef 100644 --- a/library/global.mli +++ b/library/global.mli @@ -123,26 +123,26 @@ val env_of_context : Environ.named_context_val -> Environ.env val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit val is_joined_environment : unit -> bool -val is_polymorphic : Globnames.global_reference -> bool -val is_template_polymorphic : Globnames.global_reference -> bool -val is_type_in_type : Globnames.global_reference -> bool +val is_polymorphic : GlobRef.t -> bool +val is_template_polymorphic : GlobRef.t -> bool +val is_type_in_type : GlobRef.t -> bool val constr_of_global_in_context : Environ.env -> - Globnames.global_reference -> Constr.types * Univ.AUContext.t + GlobRef.t -> Constr.types * Univ.AUContext.t (** Returns the type of the constant in its local universe context. The type should not be used without pushing it's universe context in the environmnent of usage. For non-universe-polymorphic constants, it does not matter. *) val type_of_global_in_context : Environ.env -> - Globnames.global_reference -> Constr.types * Univ.AUContext.t + GlobRef.t -> Constr.types * Univ.AUContext.t (** Returns the type of the constant in its local universe context. The type should not be used without pushing it's universe context in the environmnent of usage. For non-universe-polymorphic constants, it does not matter. *) (** Returns the universe context of the global reference (whatever its polymorphic status is). *) -val universes_of_global : Globnames.global_reference -> Univ.AUContext.t +val universes_of_global : GlobRef.t -> Univ.AUContext.t (** {6 Retroknowledge } *) diff --git a/library/globnames.ml b/library/globnames.ml index 2fa3adba24..6b78d12baf 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -15,7 +15,7 @@ open Mod_subst open Libnames (*s Global reference is a kernel side type for all references together *) -type global_reference = Names.global_reference = +type global_reference = GlobRef.t = | VarRef of variable (** A reference to the section-context. *) | ConstRef of Constant.t (** A reference to the environment. *) | IndRef of inductive (** A reference to an inductive type. *) @@ -26,14 +26,6 @@ let isConstRef = function ConstRef _ -> true | _ -> false let isIndRef = function IndRef _ -> true | _ -> false let isConstructRef = function ConstructRef _ -> true | _ -> false -let eq_gr gr1 gr2 = - gr1 == gr2 || match gr1,gr2 with - | ConstRef con1, ConstRef con2 -> Constant.equal con1 con2 - | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2 - | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2 - | VarRef v1, VarRef v2 -> Id.equal v1 v2 - | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false - let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef" let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" @@ -245,3 +237,6 @@ let pop_global_reference = function | IndRef (kn,i) -> IndRef (pop_kn kn,i) | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j) | VarRef id -> anomaly (Pp.str "VarRef not poppable.") + +(* Deprecated *) +let eq_gr = GlobRef.equal diff --git a/library/globnames.mli b/library/globnames.mli index f2b88b870b..2fe35ebccd 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -14,71 +14,73 @@ open Constr open Mod_subst (** {6 Global reference is a kernel side type for all references together } *) -type global_reference = Names.global_reference = +type global_reference = GlobRef.t = | VarRef of variable (** A reference to the section-context. *) | ConstRef of Constant.t (** A reference to the environment. *) | IndRef of inductive (** A reference to an inductive type. *) | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) +[@@ocaml.deprecated "Use Names.GlobRef.t"] -val isVarRef : global_reference -> bool -val isConstRef : global_reference -> bool -val isIndRef : global_reference -> bool -val isConstructRef : global_reference -> bool +val isVarRef : GlobRef.t -> bool +val isConstRef : GlobRef.t -> bool +val isIndRef : GlobRef.t -> bool +val isConstructRef : GlobRef.t -> bool -val eq_gr : global_reference -> global_reference -> bool -val canonical_gr : global_reference -> global_reference +val eq_gr : GlobRef.t -> GlobRef.t -> bool +[@@ocaml.deprecated "Use Names.GlobRef.equal"] +val canonical_gr : GlobRef.t -> GlobRef.t -val destVarRef : global_reference -> variable -val destConstRef : global_reference -> Constant.t -val destIndRef : global_reference -> inductive -val destConstructRef : global_reference -> constructor +val destVarRef : GlobRef.t -> variable +val destConstRef : GlobRef.t -> Constant.t +val destIndRef : GlobRef.t -> inductive +val destConstructRef : GlobRef.t -> constructor -val is_global : global_reference -> constr -> bool +val is_global : GlobRef.t -> constr -> bool val subst_constructor : substitution -> constructor -> constructor * constr -val subst_global : substitution -> global_reference -> global_reference * constr -val subst_global_reference : substitution -> global_reference -> global_reference +val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr +val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t (** This constr is not safe to be typechecked, universe polymorphism is not handled here: just use for printing *) -val printable_constr_of_global : global_reference -> constr +val printable_constr_of_global : GlobRef.t -> constr (** Turn a construction denoting a global reference into a global reference; raise [Not_found] if not a global reference *) -val global_of_constr : constr -> global_reference +val global_of_constr : constr -> GlobRef.t (** Obsolete synonyms for constr_of_global and global_of_constr *) -val reference_of_constr : constr -> global_reference +val reference_of_constr : constr -> GlobRef.t [@@ocaml.deprecated "Alias of Globnames.global_of_constr"] module RefOrdered : sig - type t = global_reference + type t = GlobRef.t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end module RefOrdered_env : sig - type t = global_reference + type t = GlobRef.t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end -module Refset : CSig.SetS with type elt = global_reference +module Refset : CSig.SetS with type elt = GlobRef.t module Refmap : Map.ExtS - with type key = global_reference and module Set := Refset + with type key = GlobRef.t and module Set := Refset -module Refset_env : CSig.SetS with type elt = global_reference +module Refset_env : CSig.SetS with type elt = GlobRef.t module Refmap_env : Map.ExtS - with type key = global_reference and module Set := Refset_env + with type key = GlobRef.t and module Set := Refset_env (** {6 Extended global references } *) type syndef_name = KerName.t type extended_global_reference = - | TrueGlobal of global_reference + | TrueGlobal of GlobRef.t | SynDef of syndef_name module ExtRefOrdered : sig @@ -89,7 +91,7 @@ module ExtRefOrdered : sig end type global_reference_or_constr = - | IsGlobal of global_reference + | IsGlobal of GlobRef.t | IsConstr of constr (** {6 Temporary function to brutally form kernel names from section paths } *) @@ -100,7 +102,6 @@ val encode_con : DirPath.t -> Id.t -> Constant.t val decode_con : Constant.t -> DirPath.t * Id.t (** {6 Popping one level of section in global names } *) - val pop_con : Constant.t -> Constant.t val pop_kn : MutInd.t-> MutInd.t -val pop_global_reference : global_reference -> global_reference +val pop_global_reference : GlobRef.t -> GlobRef.t diff --git a/library/keys.ml b/library/keys.ml index 34a6adabe0..89363455d7 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -10,12 +10,13 @@ (** Keys for unification and indexing *) -open Globnames +open Names open Term +open Globnames open Libobject type key = - | KGlob of global_reference + | KGlob of GlobRef.t | KLam | KLet | KProd @@ -126,7 +127,7 @@ let constr_key kind c = | Construct (c,u) -> KGlob (ConstructRef c) | Var id -> KGlob (VarRef id) | App (f, _) -> aux f - | Proj (p, _) -> KGlob (ConstRef (Names.Projection.constant p)) + | Proj (p, _) -> KGlob (ConstRef (Projection.constant p)) | Cast (p, _, _) -> aux p | Lambda _ -> KLam | Prod _ -> KProd diff --git a/library/keys.mli b/library/keys.mli index 1fb9a3de06..198383650a 100644 --- a/library/keys.mli +++ b/library/keys.mli @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Globnames - type key val declare_equiv_keys : key -> key -> unit @@ -21,5 +19,5 @@ val equiv_keys : key -> key -> bool val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option (** Compute the head key of a term. *) -val pr_keys : (global_reference -> Pp.t) -> Pp.t +val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t (** Pretty-print the mapping *) diff --git a/library/lib.ml b/library/lib.ml index 543cb45bc2..128b27e757 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -51,7 +51,7 @@ let subst_objects subst seg = if obj' == obj then node else (id, obj') in - List.smartmap subst_one seg + List.Smart.map subst_one seg (*let load_and_subst_objects i prefix subst seg = List.rev (List.fold_left (fun seg (id,obj as node) -> @@ -183,22 +183,11 @@ let split_lib_gen test = | before -> after,equal,before in let rec findeq after = function - | hd :: before -> - if test hd - then Some (collect after [hd] before) - else (match hd with - | (sp,ClosedModule seg) - | (sp,ClosedSection seg) -> - (match findeq after seg with - | None -> findeq (hd::after) before - | Some (sub_after,sub_equal,sub_before) -> - Some (sub_after, sub_equal, (List.append sub_before before))) - | _ -> findeq (hd::after) before) - | [] -> None + | hd :: before when test hd -> collect after [hd] before + | hd :: before -> findeq (hd::after) before + | [] -> user_err Pp.(str "no such entry") in - match findeq [] !lib_state.lib_stk with - | None -> user_err Pp.(str "no such entry") - | Some r -> r + findeq [] !lib_state.lib_stk let eq_object_name (fp1, kn1) (fp2, kn2) = eq_full_path fp1 fp2 && Names.KerName.equal kn1 kn2 @@ -580,13 +569,11 @@ let close_section () = in let (secdecls,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; - let full_olddir = !lib_state.path_prefix.obj_dir in pop_path_prefix (); add_entry oname (ClosedSection (List.rev (mark::secdecls))); let newdecls = List.map discharge_item secdecls in Summary.unfreeze_summaries fs; - List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; - Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) + List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls (* State and initialization. *) diff --git a/library/lib.mli b/library/lib.mli index 26f1718ccf..1d77212e9d 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) - +open Names (** Lib: record of operations, backtrack, low-level sections *) (** This module provides a general mechanism to keep a trace of all operations @@ -28,7 +28,7 @@ type node = and library_segment = (Libnames.object_name * node) list -type lib_objects = (Names.Id.t * Libobject.obj) list +type lib_objects = (Id.t * Libobject.obj) list (** {6 Object iteration functions. } *) @@ -54,13 +54,13 @@ val segment_of_objects : (** Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) -val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name +val add_leaf : Id.t -> Libobject.obj -> Libnames.object_name val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit val pull_to_head : Libnames.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) -val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name +val add_leaves : Id.t -> Libobject.obj list -> Libnames.object_name (** {6 ... } *) @@ -76,15 +76,15 @@ val contents_after : Libnames.object_name -> library_segment (** {6 Functions relative to current path } *) (** User-side names *) -val cwd : unit -> Names.DirPath.t -val cwd_except_section : unit -> Names.DirPath.t -val current_dirpath : bool -> Names.DirPath.t (* false = except sections *) -val make_path : Names.Id.t -> Libnames.full_path -val make_path_except_section : Names.Id.t -> Libnames.full_path +val cwd : unit -> DirPath.t +val cwd_except_section : unit -> DirPath.t +val current_dirpath : bool -> DirPath.t (* false = except sections *) +val make_path : Id.t -> Libnames.full_path +val make_path_except_section : Id.t -> Libnames.full_path (** Kernel-side names *) -val current_mp : unit -> Names.ModPath.t -val make_kn : Names.Id.t -> Names.KerName.t +val current_mp : unit -> ModPath.t +val make_kn : Id.t -> KerName.t (** Are we inside an opened section *) val sections_are_opened : unit -> bool @@ -97,19 +97,19 @@ val is_modtype : unit -> bool if the latest module started is a module type. *) val is_modtype_strict : unit -> bool val is_module : unit -> bool -val current_mod_id : unit -> Names.module_ident +val current_mod_id : unit -> module_ident (** Returns the opening node of a given name *) -val find_opening_node : Names.Id.t -> node +val find_opening_node : Id.t -> node (** {6 Modules and module types } *) val start_module : - export -> Names.module_ident -> Names.ModPath.t -> + export -> module_ident -> ModPath.t -> Summary.frozen -> Libnames.object_prefix val start_modtype : - Names.module_ident -> Names.ModPath.t -> + module_ident -> ModPath.t -> Summary.frozen -> Libnames.object_prefix val end_module : @@ -124,23 +124,23 @@ val end_modtype : (** {6 Compilation units } *) -val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit -val end_compilation_checks : Names.DirPath.t -> Libnames.object_name +val start_compilation : DirPath.t -> ModPath.t -> unit +val end_compilation_checks : DirPath.t -> Libnames.object_name val end_compilation : Libnames.object_name-> Libnames.object_prefix * library_segment (** The function [library_dp] returns the [DirPath.t] of the current compiling library (or [default_library]) *) -val library_dp : unit -> Names.DirPath.t +val library_dp : unit -> DirPath.t (** Extract the library part of a name even if in a section *) -val dp_of_mp : Names.ModPath.t -> Names.DirPath.t -val split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list -val library_part : Globnames.global_reference -> Names.DirPath.t +val dp_of_mp : ModPath.t -> DirPath.t +val split_modpath : ModPath.t -> DirPath.t * Id.t list +val library_part : GlobRef.t -> DirPath.t (** {6 Sections } *) -val open_section : Names.Id.t -> unit +val open_section : Id.t -> unit val close_section : unit -> unit (** {6 We can get and set the state of the operations (used in [States]). } *) @@ -164,31 +164,31 @@ type abstr_info = private { (** Universe quantification, same length as the substitution *) } -val instance_from_variable_context : variable_context -> Names.Id.t array +val instance_from_variable_context : variable_context -> Id.t array val named_of_variable_context : variable_context -> Context.Named.t -val section_segment_of_constant : Names.Constant.t -> abstr_info -val section_segment_of_mutual_inductive: Names.MutInd.t -> abstr_info -val section_segment_of_reference : Globnames.global_reference -> abstr_info +val section_segment_of_constant : Constant.t -> abstr_info +val section_segment_of_mutual_inductive: MutInd.t -> abstr_info +val section_segment_of_reference : GlobRef.t -> abstr_info -val variable_section_segment_of_reference : Globnames.global_reference -> variable_context +val variable_section_segment_of_reference : GlobRef.t -> variable_context -val section_instance : Globnames.global_reference -> Univ.Instance.t * Names.Id.t array -val is_in_section : Globnames.global_reference -> bool +val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array +val is_in_section : GlobRef.t -> bool -val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit +val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit val add_section_context : Univ.ContextSet.t -> unit val add_section_constant : Decl_kinds.polymorphic -> - Names.Constant.t -> Context.Named.t -> unit + Constant.t -> Context.Named.t -> unit val add_section_kn : Decl_kinds.polymorphic -> - Names.MutInd.t -> Context.Named.t -> unit + MutInd.t -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) -val discharge_kn : Names.MutInd.t -> Names.MutInd.t -val discharge_con : Names.Constant.t -> Names.Constant.t -val discharge_global : Globnames.global_reference -> Globnames.global_reference -val discharge_inductive : Names.inductive -> Names.inductive +val discharge_kn : MutInd.t -> MutInd.t +val discharge_con : Constant.t -> Constant.t +val discharge_global : GlobRef.t -> GlobRef.t +val discharge_inductive : inductive -> inductive val discharge_abstract_universe_context : abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t diff --git a/library/libnames.ml b/library/libnames.ml index d847313221..4ceea480d2 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -174,8 +174,6 @@ type global_dir_reference = | DirOpenModtype of object_prefix | DirOpenSection of object_prefix | DirModule of object_prefix - | DirClosedSection of DirPath.t - (* this won't last long I hope! *) let eq_op op1 op2 = DirPath.equal op1.obj_dir op2.obj_dir && @@ -187,7 +185,6 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2 | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2 | DirModule op1, DirModule op2 -> eq_op op1 op2 -| DirClosedSection dp1, DirClosedSection dp2 -> DirPath.equal dp1 dp2 | _ -> false type reference_r = diff --git a/library/libnames.mli b/library/libnames.mli index 9dad26129e..81e5bc5b13 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -125,8 +125,6 @@ type global_dir_reference = | DirOpenModtype of object_prefix | DirOpenSection of object_prefix | DirModule of object_prefix - | DirClosedSection of DirPath.t - (** this won't last long I hope! *) val eq_global_dir_reference : global_dir_reference -> global_dir_reference -> bool diff --git a/library/library.mllib b/library/library.mllib index e43bfb5a1f..1c03688470 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -4,7 +4,9 @@ Libobject Summary Nametab Global +Decl_kinds Lib +Misctypes Declaremods Loadpath Library diff --git a/library/misctypes.ml b/library/misctypes.ml new file mode 100644 index 0000000000..b5d30559d8 --- /dev/null +++ b/library/misctypes.ml @@ -0,0 +1,130 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(** Basic types used both in [constr_expr], [glob_constr], and [vernacexpr] *) + +(** Located identifiers and objects with syntax. *) + +type lident = Id.t CAst.t +type lname = Name.t CAst.t +type lstring = string CAst.t + +(** Cases pattern variables *) + +type patvar = Id.t + +(** Introduction patterns *) + +type 'constr intro_pattern_expr = + | IntroForthcoming of bool + | IntroNaming of intro_pattern_naming_expr + | IntroAction of 'constr intro_pattern_action_expr +and intro_pattern_naming_expr = + | IntroIdentifier of Id.t + | IntroFresh of Id.t + | IntroAnonymous +and 'constr intro_pattern_action_expr = + | IntroWildcard + | IntroOrAndPattern of 'constr or_and_intro_pattern_expr + | IntroInjection of ('constr intro_pattern_expr) CAst.t list + | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t + | IntroRewrite of bool +and 'constr or_and_intro_pattern_expr = + | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list + | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list + +(** Move destination for hypothesis *) + +type 'id move_location = + | MoveAfter of 'id + | MoveBefore of 'id + | MoveFirst + | MoveLast (** can be seen as "no move" when doing intro *) + +(** A synonym of [Evar.t], also defined in Term *) + +type existential_key = Evar.t + +(** Case style, shared with Term *) + +type case_style = Constr.case_style = + | LetStyle + | IfStyle + | LetPatternStyle + | MatchStyle + | RegularStyle (** infer printing form from number of constructor *) +[@@ocaml.deprecated "Alias for Constr.case_style"] + +(** Casts *) + +type 'a cast_type = + | CastConv of 'a + | CastVM of 'a + | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) + | CastNative of 'a + +(** Bindings *) + +type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t + +type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list + +type 'a bindings = + | ImplicitBindings of 'a list + | ExplicitBindings of 'a explicit_bindings + | NoBindings + +type 'a with_bindings = 'a * 'a bindings + + +(** Some utility types for parsing *) + +type 'a or_var = + | ArgArg of 'a + | ArgVar of lident + +type 'a and_short_name = 'a * lident option + +type 'a or_by_notation_r = + | AN of 'a + | ByNotation of (string * string option) + +type 'a or_by_notation = 'a or_by_notation_r CAst.t + +(* NB: the last string in [ByNotation] is actually a [Notation.delimiters], + but this formulation avoids a useless dependency. *) + + +(** Kinds of modules *) + +type module_kind = Module | ModType | ModAny + +(** Various flags *) + +type direction_flag = bool (* true = Left-to-right false = right-to-right *) +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type letin_flag = bool (* true = use local def false = use Leibniz *) +type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) + +type multi = + | Precisely of int + | UpTo of int + | RepeatStar + | RepeatPlus + +type ('a, 'b) gen_universe_decl = { + univdecl_instance : 'a; (* Declared universes *) + univdecl_extensible_instance : bool; (* Can new universes be added *) + univdecl_constraints : 'b; (* Declared constraints *) + univdecl_extensible_constraints : bool (* Can new constraints be added *) } diff --git a/library/nametab.ml b/library/nametab.ml index 2046bf7580..995f447061 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -432,7 +432,6 @@ let full_name_module qid = let locate_section qid = match locate_dir qid with | DirOpenSection { obj_dir; _ } -> obj_dir - | DirClosedSection dir -> dir | _ -> raise Not_found let locate_all qid = diff --git a/library/nametab.mli b/library/nametab.mli index cd28518ab6..2ec73a9869 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -75,7 +75,7 @@ val error_global_not_found : qualid CAst.t -> 'a type visibility = Until of int | Exactly of int -val push : visibility -> full_path -> global_reference -> unit +val push : visibility -> full_path -> GlobRef.t -> unit val push_modtype : visibility -> full_path -> ModPath.t -> unit val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit val push_syndef : visibility -> full_path -> syndef_name -> unit @@ -91,7 +91,7 @@ val push_universe : visibility -> full_path -> universe_id -> unit (** These functions globalize a (partially) qualified name or fail with [Not_found] *) -val locate : qualid -> global_reference +val locate : qualid -> GlobRef.t val locate_extended : qualid -> extended_global_reference val locate_constant : qualid -> Constant.t val locate_syndef : qualid -> syndef_name @@ -105,20 +105,20 @@ val locate_universe : qualid -> universe_id references, like [locate] and co, but raise a nice error message in case of failure *) -val global : reference -> global_reference +val global : reference -> GlobRef.t val global_inductive : reference -> inductive (** These functions locate all global references with a given suffix; if [qualid] is valid as such, it comes first in the list *) -val locate_all : qualid -> global_reference list +val locate_all : qualid -> GlobRef.t list val locate_extended_all : qualid -> extended_global_reference list val locate_extended_all_dir : qualid -> global_dir_reference list val locate_extended_all_modtype : qualid -> ModPath.t list (** Mapping a full path to a global reference *) -val global_of_path : full_path -> global_reference +val global_of_path : full_path -> GlobRef.t val extended_global_of_path : full_path -> extended_global_reference (** {6 These functions tell if the given absolute name is already taken } *) @@ -144,7 +144,7 @@ val full_name_module : qualid -> DirPath.t definition, and the (full) dirpath associated to a module path *) val path_of_syndef : syndef_name -> full_path -val path_of_global : global_reference -> full_path +val path_of_global : GlobRef.t -> full_path val dirpath_of_module : ModPath.t -> DirPath.t val path_of_modtype : ModPath.t -> full_path @@ -155,12 +155,12 @@ val path_of_universe : universe_id -> full_path (** Returns in particular the dirpath or the basename of the full path associated to global reference *) -val dirpath_of_global : global_reference -> DirPath.t -val basename_of_global : global_reference -> Id.t +val dirpath_of_global : GlobRef.t -> DirPath.t +val basename_of_global : GlobRef.t -> Id.t (** Printing of global references using names as short as possible. @raise Not_found when the reference is not in the global tables. *) -val pr_global_env : Id.Set.t -> global_reference -> Pp.t +val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t (** The [shortest_qualid] functions given an object with [user_name] @@ -168,7 +168,7 @@ val pr_global_env : Id.Set.t -> global_reference -> Pp.t Coq.A.B.x that denotes the same object. @raise Not_found for unknown objects. *) -val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid +val shortest_qualid_of_global : Id.Set.t -> GlobRef.t -> qualid val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : ModPath.t -> qualid val shortest_qualid_of_module : ModPath.t -> qualid @@ -177,7 +177,7 @@ val shortest_qualid_of_universe : universe_id -> qualid (** Deprecated synonyms *) val extended_locate : qualid -> extended_global_reference (*= locate_extended *) -val absolute_reference : full_path -> global_reference (** = global_of_path *) +val absolute_reference : full_path -> GlobRef.t (** = global_of_path *) (** {5 Generic name handling} *) |