generalized is half-implemented (still broken)

[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..5fc3a7fad5148d03c5aee0328d9b3fd98ddbd234 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -180,9 +180,30 @@ EXTEND
     ]
   ];
   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
+  ntactic: [
+    [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t)
+    | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
+        GrafiteAst.NCases (loc, what, where)
+    | 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)
+    | IDENT "ngeneralize"; p=pattern_spec ->
+        GrafiteAst.NGeneralize (loc, p)
+    | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
+        GrafiteAst.NRewrite (loc, dir, what, where)
+    | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
+    | SYMBOL "#"; SYMBOL "_" -> GrafiteAst.NIntro (loc,"_")
+    | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
+    | SYMBOL "*"; n=IDENT ->
+        GrafiteAst.NCase1 (loc,n)
+    ]
+  ];
   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 +246,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 +481,10 @@ EXTEND
       | IDENT "skip" -> GrafiteAst.Skip loc
       ]
     ];
+  ntheorem_flavour: [
+    [ [ IDENT "ntheorem"     ] -> `Theorem
+    ]
+  ];
   theorem_flavour: [
     [ [ IDENT "definition"  ] -> `Definition
     | [ IDENT "fact"        ] -> `Fact
@@ -524,6 +549,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 +689,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 +724,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 +757,10 @@ 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)
+    | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
+        GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
@@ -739,7 +777,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 ->