From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 25 May 2006 10:24:34 +0000 (+0000)
Subject: Axioms are not allowed with the syntax: "axiom name: type.".
X-Git-Tag: 0.4.95@7852~1435
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ba48c24f4edb0701a0aa346466f2a4211f719ab2;p=helm.git

Axioms are not allowed with the syntax: "axiom name: type.".
---

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 @@
     <keyword>fact</keyword>
     <keyword>remark</keyword>
     <keyword>variant</keyword>
+    <keyword>axiom</keyword>
   </keyword-list>
     
   <keyword-list _name = "Commands" style = "Keyword" case-sensitive="TRUE">