aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-28 00:16:46 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-04-23 16:23:49 +0200
commit7dfac786626f8f6775dadc0df85360759584c976 (patch)
tree9c0355fb0dba4a48e14d0e5b316c66dfd416d685 /library
parent5c34cfa54ec1959758baa3dd283e2e30853380db (diff)
[api] Relocate `intf` modules according to dependency-order.
In a component-based source code organization of Coq `intf` doesn't fit very well, as it sits in bit of "limbo" between different components, and indeed, encourages developers to place types in sometimes random places wrt the hierarchy. For example, lower parts of the system reference `Vernacexpr`, which morally lives in a pretty higher part of the system. We move all the files in `intf` to the lowest place their dependencies can accommodate: - `Misctypes`: is used by Declaremod, thus it has to go in `library` or below. Ideally, this file would disappear. - `Evar_kinds`: it is used by files in `engine`, so that seems its proper placement. - `Decl_kinds`: used in `library`, seems like the right place. [could also be merged. - `Glob_term`: belongs to pretyping, where it is placed. - `Locus`: ditto. - `Pattern`: ditto. - `Genredexpr`: depended by a few modules in `pretyping`, seems like the righ place. - `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and could be fixed, as this module should be declared in `interp` which is the one eliminating it. - `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed as it contains stuff it shouldn't. The right place should be `parsing`. - `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`. - `Notation_term`: First place used is `interp`, seems like the right place. Additionally, for some files it could be worth to merge files of the form `Foo` with `Foo_ops` in the medium term, as to create proper ADT modules as done in the kernel with `Name`, etc...
Diffstat (limited to 'library')
-rw-r--r--library/decl_kinds.ml87
-rw-r--r--library/library.mllib2
-rw-r--r--library/misctypes.ml149
3 files changed, 238 insertions, 0 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
new file mode 100644
index 000000000..0d3285311
--- /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/library.mllib b/library/library.mllib
index e43bfb5a1..1c0368847 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 000000000..72db3b31c
--- /dev/null
+++ b/library/misctypes.ml
@@ -0,0 +1,149 @@
+(************************************************************************)
+(* * 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 *)
+
+(** Sorts *)
+
+type 'a glob_sort_gen =
+ | GProp (** representation of [Prop] literal *)
+ | GSet (** representation of [Set] literal *)
+ | GType of 'a (** representation of [Type] literal *)
+
+type 'a universe_kind =
+ | UAnonymous
+ | UUnknown
+ | UNamed of 'a
+
+type level_info = Libnames.reference universe_kind
+type glob_level = level_info glob_sort_gen
+type glob_constraint = glob_level * Univ.constraint_type * glob_level
+
+type sort_info = (Libnames.reference * int) option list
+type glob_sort = sort_info glob_sort_gen
+
+(** 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 *) }