1) mk_meta now returns also the index of the created meta

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 976bea700353fc2c002df3e7796ef734b4195ee8..e6b3d8991493298421701895bdaf3332c20dd3fc 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -180,9 +180,17 @@ 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)
+    ]
+  ];
   tactic: [
     [ IDENT "absurd"; t = tactic_term ->
         GrafiteAst.Absurd (loc, t)
+    | IDENT "apply"; IDENT "rule"; t = tactic_term ->
+        GrafiteAst.ApplyRule (loc, t)
     | IDENT "apply"; t = tactic_term ->
         GrafiteAst.Apply (loc, t)
     | IDENT "applyP"; t = tactic_term ->
@@ -225,12 +233,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))
@@ -460,6 +468,10 @@ EXTEND
       | IDENT "skip" -> GrafiteAst.Skip loc
       ]
     ];
+  ntheorem_flavour: [
+    [ [ IDENT "ntheorem"     ] -> `Theorem
+    ]
+  ];
   theorem_flavour: [
     [ [ IDENT "definition"  ] -> `Definition
     | [ IDENT "fact"        ] -> `Fact
@@ -524,6 +536,8 @@ EXTEND
   macro: [
     [ [ IDENT "check"   ]; t = term ->
         GrafiteAst.Check (loc, t)
+    | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
+        GrafiteAst.Eval (loc, kind, t)
     | [ IDENT "inline"]; 
         style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
         suri = QSTRING; prefix = OPT QSTRING;
@@ -662,6 +676,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))
@@ -694,6 +711,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 ->
@@ -723,6 +744,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)
@@ -739,7 +762,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 ->