diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/decl_kinds.ml | 126 | ||||
| -rw-r--r-- | library/decl_kinds.mli | 91 | ||||
| -rw-r--r-- | library/kindops.ml | 41 | ||||
| -rw-r--r-- | library/kindops.mli | 16 | ||||
| -rw-r--r-- | library/library.mllib | 2 |
5 files changed, 58 insertions, 218 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml deleted file mode 100644 index e8734cbaa..000000000 --- a/library/decl_kinds.ml +++ /dev/null @@ -1,126 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Errors -open Util -open Libnames - -(* Informal mathematical status of declarations *) - -type locality = - | Local - | Global - -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 - -type assumption_object_kind = Definitional | Logical | Conjectural - -(* [assumption_kind] - - | Local | Global - ------------------------------------ - Definitional | Variable | Parameter - Logical | Hypothesis | Axiom - -*) -type assumption_kind = locality * assumption_object_kind - -type definition_kind = locality * definition_object_kind - -(* Kinds used in proofs *) - -type goal_object_kind = - | DefinitionBody of definition_object_kind - | Proof of theorem_kind - -type goal_kind = locality * goal_object_kind - -(* Kinds used in library *) - -type logical_kind = - | IsAssumption of assumption_object_kind - | IsDefinition of definition_object_kind - | IsProof of theorem_kind - -(* Utils *) - -let logical_kind_of_goal_kind = function - | DefinitionBody d -> IsDefinition d - | Proof s -> IsProof s - -let string_of_theorem_kind = function - | Theorem -> "Theorem" - | Lemma -> "Lemma" - | Fact -> "Fact" - | Remark -> "Remark" - | Property -> "Property" - | Proposition -> "Proposition" - | 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) -> - anomaly "Unsupported local definition kind" - | Local, Instance -> "Instance" - | Global, Instance -> "Global Instance" - | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) - -> anomaly "Internal definition kind" - -(* Strength *) - -let strength_of_global = function - | VarRef _ -> Local - | IndRef _ | ConstructRef _ | ConstRef _ -> Global - -let string_of_strength = function - | Local -> "Local" - | Global -> "Global" - - -(* Recursive power *) - -(* spiwack: this definition might be of use in the kernel, for now I do not - push them deeper than needed, though. *) -type recursivity_kind = - | Finite (* = inductive *) - | CoFinite (* = coinductive *) - | BiFinite (* = non-recursive, like in "Record" definitions *) - -(* helper, converts to "finiteness flag" booleans *) -let recursivity_flag_of_kind = function - | Finite | BiFinite -> true - | CoFinite -> false diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli deleted file mode 100644 index 5b81d54ee..000000000 --- a/library/decl_kinds.mli +++ /dev/null @@ -1,91 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Errors -open Util -open Libnames - -(** Informal mathematical status of declarations *) - -type locality = - | Local - | Global - -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 - -type assumption_object_kind = Definitional | Logical | Conjectural - -(** [assumption_kind] - - | Local | Global - ------------------------------------ - Definitional | Variable | Parameter - Logical | Hypothesis | Axiom - -*) -type assumption_kind = locality * assumption_object_kind - -type definition_kind = locality * definition_object_kind - -(** Kinds used in proofs *) - -type goal_object_kind = - | DefinitionBody of definition_object_kind - | Proof of theorem_kind - -type goal_kind = locality * goal_object_kind - -(** Kinds used in library *) - -type logical_kind = - | IsAssumption of assumption_object_kind - | IsDefinition of definition_object_kind - | IsProof of theorem_kind - -(** Utils *) - -val logical_kind_of_goal_kind : goal_object_kind -> logical_kind -val string_of_theorem_kind : theorem_kind -> string -val string_of_definition_kind : - locality * definition_object_kind -> string - -(** About locality *) - -val strength_of_global : global_reference -> locality -val string_of_strength : locality -> string - -(** About recursive power of type declarations *) - -type recursivity_kind = - | Finite (** = inductive *) - | CoFinite (** = coinductive *) - | BiFinite (** = non-recursive, like in "Record" definitions *) - -(** helper, converts to "finiteness flag" booleans *) -val recursivity_flag_of_kind : recursivity_kind -> bool diff --git a/library/kindops.ml b/library/kindops.ml new file mode 100644 index 000000000..012e599e2 --- /dev/null +++ b/library/kindops.ml @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Decl_kinds + +(** Operations about types defined in [Decl_kinds] *) + +let logical_kind_of_goal_kind = function + | DefinitionBody d -> IsDefinition d + | Proof s -> IsProof s + +let string_of_theorem_kind = function + | Theorem -> "Theorem" + | Lemma -> "Lemma" + | Fact -> "Fact" + | Remark -> "Remark" + | Property -> "Property" + | Proposition -> "Proposition" + | 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 "Unsupported local definition kind" + | Local, Instance -> "Instance" + | Global, Instance -> "Global Instance" + | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) + -> Errors.anomaly "Internal definition kind" diff --git a/library/kindops.mli b/library/kindops.mli new file mode 100644 index 000000000..c7f2a2e7f --- /dev/null +++ b/library/kindops.mli @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Decl_kinds + +(** Operations about types defined in [Decl_kinds] *) + +val logical_kind_of_goal_kind : goal_object_kind -> logical_kind +val string_of_theorem_kind : theorem_kind -> string +val string_of_definition_kind : + locality * definition_object_kind -> string diff --git a/library/library.mllib b/library/library.mllib index e8b5a7a4c..edd5bfc07 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -8,7 +8,7 @@ Lib Declaremods Library States -Decl_kinds +Kindops Dischargedhypsmap Goptions Decls |