aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-01-28 23:06:58 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-01-28 23:06:58 +0000
commitadadd8db0e9eb1e5161057a7064426b84a3d2605 (patch)
tree47513322d7127fc5f67001751376b8831d0b8c0e /library
parentafb7c5ccdf3d261aaf071ff77a4260f3b4b5d399 (diff)
- Ajout syntaxe concrète Property/Corollary, synonymes de Lemma
- Ajout syntaxe concrète Example, synonyme de Definition - Réorganisation de la structure interne des types de déclarations (decl_kinds) - Notamment, ajout de noms pour les déclarations interne (Scheme, Fixpoint...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7940 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
-rw-r--r--library/decl_kinds.ml67
1 files changed, 46 insertions, 21 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 597431840..c6879575d 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -8,29 +8,39 @@
(* $Id$ *)
+open Util
+
(* Informal mathematical status of declarations *)
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
+ | Corollary
type definition_object_kind =
- | Definition of bool
+ | 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,35 +50,50 @@ 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
- | 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"
+ | Corollary -> "Corollary"
+ | Property -> "Property"
+
+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"