From 18b2b2742fe8ebb3d11b32b9bb727f510df6927a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 8 Jul 2005 14:08:57 +0000
Subject: [PATCH] added Variant theorem flavour
---
helm/ocaml/cic/cic.ml | 10 ++++++++++
helm/ocaml/cic/cicParser.ml | 13 +++++++++++++
helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 5 +++++
helm/ocaml/cic_disambiguation/disambiguate.ml | 10 ++++++----
helm/ocaml/cic_transformations/cic2Xml.ml | 9 +++++++++
helm/ocaml/cic_transformations/tacticAst.ml | 8 +-------
helm/ocaml/cic_transformations/tacticAstPp.ml | 3 ++-
7 files changed, 46 insertions(+), 12 deletions(-)
diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index ba51157ff..1c2bf8df0 100644
--- 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 e4a840ccf..a28968377 100644
--- 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 9a4340f9f..451d77292 100644
--- 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 62382c897..dd915a282 100644
--- 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 056240ef1..3ca6a3a50 100644
--- 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 31e209353..e4f454ed6 100644
--- 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 bd26fb387..794e09e70 100644
--- 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"
--
2.39.2