X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=1b06b81c97fd64b26b4429956c25e9c573c7bdd5;hb=c92a4b4096c9633c27a6cb392d8027cad4c34144;hp=e480efd34f1cbfbc77656716ee0f4f9ff0b59f66;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index e480efd34..1b06b81c9 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -31,15 +31,17 @@ module Ast = CicNotationPt
 
 type 'a localized_option =
    LSome of 'a
- | LNone of Token.flocation
+ | LNone of GrafiteAst.loc
 
-type statement =
- include_paths:string list ->
- LexiconEngine.status ->
-  LexiconEngine.status *
+type ast_statement =
   (CicNotationPt.term, CicNotationPt.term,
    CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
-    GrafiteAst.statement localized_option
+    GrafiteAst.statement
+
+type statement =
+  include_paths:string list ->
+  LexiconEngine.status ->
+    LexiconEngine.status * ast_statement localized_option
 
 let grammar = CicNotationParser.level2_ast_grammar
 
@@ -140,16 +142,12 @@ EXTEND
         GrafiteAst.ClearBody (loc,id)
     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
         GrafiteAst.Change (loc, what, t)
-    | IDENT "compare"; t = tactic_term ->
-        GrafiteAst.Compare (loc,t)
     | IDENT "constructor"; n = int ->
         GrafiteAst.Constructor (loc, n)
     | IDENT "contradiction" ->
         GrafiteAst.Contradiction loc
     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
         GrafiteAst.Cut (loc, ident, t)
-    | IDENT "decide"; IDENT "equality" ->
-        GrafiteAst.DecideEquality loc
     | IDENT "decompose"; types = OPT ident_list0; what = IDENT;
       (num, idents) = intros_spec ->
         let types = match types with None -> [] | Some types -> types in
@@ -343,7 +341,7 @@ EXTEND
         GrafiteAst.WMatch (loc,t)
     | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
         GrafiteAst.WInstance (loc,t)
-    | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> 
+    | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING -> 
         GrafiteAst.WLocate (loc,id)
     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
         GrafiteAst.WElim (loc, t)
@@ -451,7 +449,10 @@ EXTEND
   ];
   
   include_command: [ [
-      IDENT "include" ; path = QSTRING -> loc,path
+      IDENT "include" ; path = QSTRING -> 
+        loc,path,LexiconAst.WithPreferences
+    | IDENT "include'" ; path = QSTRING -> 
+        loc,path,LexiconAst.WithoutPreferences
    ]];
 
   grafite_command: [ [
@@ -471,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 = 
@@ -530,11 +533,11 @@ EXTEND
        fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
     | com = comment ->
        fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
-    | (iloc,fname) = include_command ; SYMBOL "."  ->
+    | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
        fun ~include_paths status ->
         let path = DependenciesParser.baseuri_of_script ~include_paths fname in
         let status =
-         LexiconEngine.eval_command status (LexiconAst.Include (iloc,path))
+         LexiconEngine.eval_command status (LexiconAst.Include (iloc,path,mode))
         in
          status,
           LSome