X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=821d2909a65697d365ddfa7369b34dc6ec5b79e3;hb=d072c3ea699cf33189d18d8431fda9750fc2eb93;hp=51c7d07b267b8bb33d1b9432612a728ffe7c032d;hpb=154cbc049da8d8c3dd090a919a40c90eb23cc24e;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 51c7d07b2..821d2909a 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -180,6 +180,15 @@ EXTEND
     ]
   ];
   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
+  ntactic: [
+    [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t)
+    | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> 
+        GrafiteAst.NChange (loc, what, with_what)
+    | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
+        GrafiteAst.NElim (loc, what, where)
+    | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
+    ]
+  ];
   tactic: [
     [ IDENT "absurd"; t = tactic_term ->
         GrafiteAst.Absurd (loc, t)
@@ -227,12 +236,12 @@ EXTEND
         GrafiteAst.Destruct (loc, xts)
     | IDENT "elim"; what = tactic_term; using = using; 
        pattern = OPT pattern_spec;
-       (num, idents) = intros_spec ->
+       ispecs = intros_spec ->
         let pattern = match pattern with
            | None         -> None, [], Some Ast.UserInput
            | Some pattern -> pattern   
         in
-        GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
+        GrafiteAst.Elim (loc, what, using, pattern, ispecs)
     | IDENT "elimType"; what = tactic_term; using = using;
       (num, idents) = intros_spec ->
         GrafiteAst.ElimType (loc, what, using, (num, idents))
@@ -462,6 +471,10 @@ EXTEND
       | IDENT "skip" -> GrafiteAst.Skip loc
       ]
     ];
+  ntheorem_flavour: [
+    [ [ IDENT "ntheorem"     ] -> `Theorem
+    ]
+  ];
   theorem_flavour: [
     [ [ IDENT "definition"  ] -> `Definition
     | [ IDENT "fact"        ] -> `Fact
@@ -666,6 +679,9 @@ EXTEND
         GrafiteAst.Obj (loc, 
           Ast.Theorem 
             (`Variant,name,typ,Some (Ast.Ident (newname, None))))
+    | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
+      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+        GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
@@ -698,6 +714,10 @@ EXTEND
         let composites = match composites with None -> true | Some _ -> false in
         GrafiteAst.Coercion
          (loc, t, composites, arity, saturations)
+    | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
+        GrafiteAst.PreferCoercion (loc, t)
+    | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
+        GrafiteAst.UnificationHint (loc, t, n)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
@@ -727,6 +747,8 @@ EXTEND
     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
         GrafiteAst.Tactic (loc, Some tac, punct)
     | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
+    | tac = ntactic; punct = punctuation_tactical ->
+        GrafiteAst.NTactic (loc, tac, punct)
     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
@@ -743,7 +765,8 @@ EXTEND
     [ ex = executable ->
        fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
     | com = comment ->
-       fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
+       fun ?(never_include=false) ~include_paths status -> 
+               status,LSome (GrafiteAst.Comment (loc, com))
     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
        !out fname;       
        fun ?(never_include=false) ~include_paths status ->