added Variant theorem flavour

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index ba51157ff9f4aa24464733c0820f0b518e4d7119..1c2bf8df0e46d968d703708a33d482ca1e84469d 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -53,6 +53,15 @@ type name =
  | Name of string
  | Anonymous
 
+type object_flavour =
+  [ `Definition
+  | `Fact
+  | `Lemma
+  | `Remark
+  | `Theorem
+  | `Variant
+  ]
+
 type object_class =
   [ `Coercion
   | `Elim of sort   (** elimination principle; if sort is Type, the universe is
@@ -64,6 +73,7 @@ type object_class =
 
 type attribute =
   [ `Class of object_class
+  | `Flavour of object_flavour 
   | `Generated
   ]
 

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

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 9a4340f9fb4b692a9c797e63de88875f57c5ff6f..451d772925d8b5a50b63bdb1772af4e96c002357 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -615,6 +615,11 @@ EXTEND
         TacticAst.Set (loc, n, v)
     |  [ IDENT "drop" ] -> TacticAst.Drop loc
     | [ IDENT "qed"   ] -> TacticAst.Qed loc
+    | IDENT "variant" ; name = IDENT; SYMBOL ":"; 
+      typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
+        TacticAst.Obj (loc, 
+          TacticAst.Theorem 
+            (`Variant,name,typ,Some (CicAst.Ident (newname, None))))
     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body))

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 62382c8975d328fae6b22ed6574851918008e584..dd915a2829c0831961b860dbc76e02b7805cce8d 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -412,14 +412,16 @@ let interpretate_obj ~context ~env ~uri ~is_path obj =
      let field_names = List.map fst fields in
       Cic.InductiveDefinition
        (tyl,[],List.length params,[`Class (`Record field_names)])
-  | TacticAst.Theorem (_,name,ty,bo) ->
+  | TacticAst.Theorem (flavour, name, ty, bo) ->
+     let attrs = [`Flavour flavour] in
      let ty' = interpretate_term [] env None false ty in
-     match bo with
+     (match bo with
         None ->
-         Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],[])
+         Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
       | Some bo ->
          let bo' = Some (interpretate_term [] env None false bo) in
-          Cic.Constant (name,bo',ty',[],[])
+          Cic.Constant (name,bo',ty',[],attrs))
+          
 
   (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
 let rev_uniq =

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index 056240ef13899e24b08a8adf1b9aac306f94eb64..3ca6a3a5040990370f722c0e8c30755b1a1eba3d 100644 (file)
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -276,9 +276,18 @@ let xml_of_attrs attributes =
            ) field_names [<>])
     | `Projection -> Xml.xml_empty "class" [None,"value","projection"]
   in
+  let flavour_of = function
+    | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"]
+    | `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"]
+    | `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"]
+    | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
+    | `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"]
+    | `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"]
+  in
   let xml_attr_of = function
     | `Generated -> Xml.xml_empty "generated" []
     | `Class c -> class_of c
+    | `Flavour f -> flavour_of f
   in
   let xml_attrs =
    List.fold_right 

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 31e2093530f33d6a1c22dd601204c3cafa2b27e3..e4f454ed61fd4cd3a0e80486470c01669b114544 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -71,13 +71,7 @@ type ('term, 'ident) tactic =
   | Symmetry of loc
   | Transitivity of loc * 'term
 
-type thm_flavour =
-  [ `Definition
-  | `Fact
-  | `Lemma
-  | `Remark
-  | `Theorem
-  ]
+type thm_flavour = Cic.object_flavour
 
   (** <name, inductive/coinductive, type, constructor list>
   * true means inductive, false coinductive *)

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index bd26fb387492dcc6947b23945d7769a2bd64a03b..794e09e708cbf517b418be743b9899e44c3bab62 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -141,12 +141,14 @@ let pp_flavour = function
   | `Lemma -> "Lemma"
   | `Remark -> "Remark"
   | `Theorem -> "Theorem"
+  | `Variant -> "Variant"
 
 let pp_search_kind = function
   | `Locate -> "locate"
   | `Hint -> "hint"
   | `Match -> "match"
   | `Elim -> "elim"
+  | `Instance -> "instance"
 
 let pp_macro pp_term = function 
   (* Whelp *)
@@ -227,7 +229,6 @@ let pp_obj = function
     "record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^
     pp_fields fields ^ "}"
 
-
 let pp_command = function
   | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"