From: Enrico Tassi Date: Fri, 8 Jul 2005 14:08:57 +0000 (+0000) Subject: added Variant theorem flavour X-Git-Tag: pre_notation~68 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=18b2b2742fe8ebb3d11b32b9bb727f510df6927a;p=helm.git added Variant theorem flavour --- 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> ; 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> (* ≝ *); 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 (** * 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"