]
];
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)
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))
| IDENT "skip" -> GrafiteAst.Skip loc
]
];
+ ntheorem_flavour: [
+ [ [ IDENT "ntheorem" ] -> `Theorem
+ ]
+ ];
theorem_flavour: [
[ [ IDENT "definition" ] -> `Definition
| [ IDENT "fact" ] -> `Fact
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))
(loc, t, composites, arity, saturations)
| IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
GrafiteAst.PreferCoercion (loc, t)
- | IDENT "unification"; IDENT "hint"; t = tactic_term ->
- GrafiteAst.UnificationHint (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 ->
| 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)