added Variant theorem flavour

[helm.git] / helm / ocaml / cic / cicParser.ml

diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml
index e4a840ccf5243ad59a90669318429a8b26de6fa2..a289683772312aa3114040a53261b48fe186ce7d 100644 (file)
--- a/helm/ocaml/cic/cicParser.ml
+++ b/helm/ocaml/cic/cicParser.ml
@@ -64,6 +64,7 @@ type stack_entry =
       (string * Cic.annterm) list (* id, name, inductive, arity, constructors *)
   | Meta_subst of Cic.annterm option
   | Obj_class of Cic.object_class
+  | Obj_flavour of Cic.object_flavour
   | Obj_field of string (* field name *)
   | Obj_generated
   | Tag of string * (string * string) list  (* tag name, attributes *)
@@ -99,6 +100,7 @@ let string_of_stack ctxt =
           sprintf "Inductive_type %s (id=%s)" name id
       | Meta_subst _ -> "Meta_subst"
       | Obj_class _ -> "Obj_class"
+      | Obj_flavour _ -> "Obj_flavour"
       | Obj_field name -> "Obj_field " ^ name
       | Obj_generated -> "Obj_generated"
       | Tag (tag, _) -> "Tag " ^ tag)
@@ -615,6 +617,7 @@ let end_element ctxt tag =
   | "attributes" ->
       let rec aux acc = function  (* retrieve object attributes *)
         | Obj_class c :: tl -> aux (`Class c :: acc) tl
+        | Obj_flavour f :: tl -> aux (`Flavour f :: acc) tl
         | Obj_generated :: tl -> aux (`Generated :: acc) tl
         | tl -> acc, tl
       in
@@ -627,6 +630,16 @@ let end_element ctxt tag =
         (match pop_tag_attrs ctxt with
         | ["name", name] -> Obj_field name
         | _ -> attribute_error ())
+  | "flavour" ->
+      push ctxt 
+        (match pop_tag_attrs ctxt with
+        | [ "value", "definition"] -> Obj_flavour `Definition
+        | [ "value", "fact"] -> Obj_flavour `Fact
+        | [ "value", "lemma"] -> Obj_flavour `Lemma
+        | [ "value", "remark"] -> Obj_flavour `Remark
+        | [ "value", "theorem"] -> Obj_flavour `Theorem
+        | [ "value", "variant"] -> Obj_flavour `Variant
+        | _ -> attribute_error ())
   | "class" ->
       let class_modifiers = pop_class_modifiers ctxt in
       push ctxt