- 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

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"