From ba48c24f4edb0701a0aa346466f2a4211f719ab2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 25 May 2006 10:24:34 +0000 Subject: [PATCH] Axioms are not allowed with the syntax: "axiom name: type.". --- components/acic_content/cicNotationPp.ml | 1 + components/acic_content/cicNotationPt.ml | 3 ++- components/cic/cic.ml | 1 + components/cic/cicParser.ml | 1 + components/cic_acic/cic2Xml.ml | 1 + components/cic_disambiguation/disambiguate.ml | 9 ++++++--- components/grafite_parser/grafiteParser.ml | 2 ++ components/library/librarySync.ml | 2 +- matita/matita.lang | 1 + 9 files changed, 16 insertions(+), 5 deletions(-) diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml index 590de7c54..fb38674df 100644 --- a/components/acic_content/cicNotationPp.ml +++ b/components/acic_content/cicNotationPp.ml @@ -258,6 +258,7 @@ let pp_flavour = function | `Remark -> "remark" | `Theorem -> "theorem" | `Variant -> "variant" + | `Axiom -> "axiom" let pp_fields fields = (if fields <> [] then "\n" else "") ^ diff --git a/components/acic_content/cicNotationPt.ml b/components/acic_content/cicNotationPt.ml index a66aa5feb..609fb9d2f 100644 --- a/components/acic_content/cicNotationPt.ml +++ b/components/acic_content/cicNotationPt.ml @@ -171,7 +171,8 @@ type obj = * - name is absent when an unnamed theorem is being proved, tipically in * interactive usage * - body is present when its given along with the command, otherwise it - * will be given in proof editing mode using the tactical language + * will be given in proof editing mode using the tactical language, + * unless the flavour is an Axiom *) | Record of (string * term) list * string * term * (string * term * bool) list (** left parameters, name, type, fields *) diff --git a/components/cic/cic.ml b/components/cic/cic.ml index 1becd4442..20a6cb457 100644 --- a/components/cic/cic.ml +++ b/components/cic/cic.ml @@ -62,6 +62,7 @@ type object_flavour = | `Remark | `Theorem | `Variant + | `Axiom ] type object_class = diff --git a/components/cic/cicParser.ml b/components/cic/cicParser.ml index f9d6d880e..1e9a3a33c 100644 --- a/components/cic/cicParser.ml +++ b/components/cic/cicParser.ml @@ -672,6 +672,7 @@ let end_element ctxt tag = | [ "value", "remark"] -> Obj_flavour `Remark | [ "value", "theorem"] -> Obj_flavour `Theorem | [ "value", "variant"] -> Obj_flavour `Variant + | [ "value", "axiom"] -> Obj_flavour `Axiom | _ -> attribute_error ()) | "class" -> let class_modifiers = pop_class_modifiers ctxt in diff --git a/components/cic_acic/cic2Xml.ml b/components/cic_acic/cic2Xml.ml index 7e97dea6f..95f92346b 100644 --- a/components/cic_acic/cic2Xml.ml +++ b/components/cic_acic/cic2Xml.ml @@ -293,6 +293,7 @@ let xml_of_attrs attributes = | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"] | `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"] | `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"] + | `Axiom -> Xml.xml_empty "flavour" [None, "value", "axiom"] in let xml_attr_of = function | `Generated -> Xml.xml_empty "generated" [] diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index d3af05256..85f05aa1c 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/components/cic_disambiguation/disambiguate.ml @@ -506,10 +506,13 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = | CicNotationPt.Theorem (flavour, name, ty, bo) -> let attrs = [`Flavour flavour] in let ty' = interpretate_term [] env None false ty in - (match bo with - None -> + (match bo,flavour with + None,`Axiom -> + Cic.Constant (name,None,ty',[],attrs) + | Some bo,`Axiom -> assert false + | None,_ -> Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs) - | Some bo -> + | Some bo,_ -> let bo' = Some (interpretate_term [] env None false bo) in Cic.Constant (name,bo',ty',[],attrs)) diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index e83152226..1b06b81c9 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -472,6 +472,8 @@ EXTEND body = term -> GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, Ast.Implicit, Some body)) + | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> + GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = CicNotationParser.let_defs -> let name,ty = diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index 2dcd6a8b9..a09baafe1 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -84,7 +84,7 @@ let save_object_to_disk uri obj ugraph univlist = (univgraphuri,xmlunivgraphpath) :: (* now the optional body, both write and register *) (match bodyxml,bodyuri with - None,None -> [] + None,_ -> [] | Some bodyxml,Some bodyuri-> ensure_path_exists xmlbodypath; Xml.pp ~gzip:true bodyxml (Some xmlbodypath); diff --git a/matita/matita.lang b/matita/matita.lang index 52459589e..1e2f0e57c 100644 --- a/matita/matita.lang +++ b/matita/matita.lang @@ -21,6 +21,7 @@ fact remark variant + axiom -- 2.39.2