diff options
Diffstat (limited to 'library/decl_kinds.ml')
-rw-r--r-- | library/decl_kinds.ml | 70 |
1 files changed, 48 insertions, 22 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index a030284c..af54df2f 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -6,7 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_kinds.ml,v 1.6.2.1 2004/07/16 19:30:33 herbelin Exp $ *) +(* $Id: decl_kinds.ml 7944 2006-01-29 16:01:32Z herbelin $ *) + +open Util (* Informal mathematical status of declarations *) @@ -14,23 +16,32 @@ type locality_flag = (*bool (* local = true; global = false *)*) | Local | Global -(* Kinds used at parsing time *) +type boxed_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 type strength = locality_flag (* For compatibility *) -type type_as_formula_kind = Definitional | Logical | Conjectural +type assumption_object_kind = Definitional | Logical | Conjectural (* [assumption_kind] @@ -40,36 +51,51 @@ type type_as_formula_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality_flag * type_as_formula_kind +type assumption_kind = locality_flag * assumption_object_kind -type definition_kind = locality_flag * definition_object_kind +type definition_kind = locality_flag * boxed_flag * definition_object_kind (* Kinds used in proofs *) -type global_goal_kind = - | DefinitionBody +type goal_object_kind = + | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = - | IsGlobal of global_goal_kind - | IsLocal +type goal_kind = locality_flag * goal_object_kind (* Kinds used in library *) -type local_theorem_kind = LocalStatement - -type 'a mathematical_kind = - | IsAssumption of type_as_formula_kind - | IsDefinition - | IsConjecture - | IsProof of 'a - -type global_kind = theorem_kind mathematical_kind -type local_kind = local_theorem_kind mathematical_kind +type logical_kind = + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind (* Utils *) -let theorem_kind_of_goal_kind = function - | DefinitionBody -> IsDefinition +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 (l,boxed,d) = + match (l,d) with + | Local, Coercion -> "Coercion Local" + | Global, Coercion -> "Coercion" + | Local, Definition -> "Let" + | Global, Definition -> if boxed then "Boxed Definition" else "Definition" + | Local, SubClass -> "Local SubClass" + | Global, SubClass -> "SubClass" + | Global, CanonicalStructure -> "Canonical Structure" + | Global, Example -> "Example" + | Local, (CanonicalStructure|Example) -> + anomaly "Unsupported local definition kind" + | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion) + -> anomaly "Internal definition kind" |