GrafiteAst.FwdSimpl (loc, hyp, idents)
| IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
GrafiteAst.Generalize (loc,p,id)
- | IDENT "goal"; n = int ->
- GrafiteAst.Goal (loc, n)
| IDENT "id" -> GrafiteAst.IdTac loc
| IDENT "intro"; ident = OPT IDENT ->
let idents = match ident with None -> [] | Some id -> [id] in
(GrafiteAst.Then (loc, tac, tacs))
]
| "loops" RIGHTA
- [ IDENT "do"; count = int; tac = SELF; IDENT "end" ->
+ [ IDENT "do"; count = int; tac = SELF ->
GrafiteAst.Do (loc, count, tac)
- | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac)
+ | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
]
| "simple" NONA
[ IDENT "first";
GrafiteAst.Solve (loc, tacs)
| IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
| LPAREN; tac = SELF; RPAREN -> tac
- | tac = tactic -> GrafiteAst.Tactic (loc, tac)
+ | tac = tactic -> tac
]
];
punctuation_tactical:
| SYMBOL "." -> GrafiteAst.Dot loc
]
];
- tactical:
+ non_punctuation_tactical:
[ "simple" NONA
[ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
| IDENT "unfocus" -> GrafiteAst.Unfocus loc
| IDENT "skip" -> GrafiteAst.Skip loc
- | tac = atomic_tactical LEVEL "loops" -> tac
]
];
theorem_flavour: [
]];
executable: [
[ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
- | tac = tactical; punct = punctuation_tactical ->
- GrafiteAst.Tactical (loc, tac, Some punct)
- | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None)
+ | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
+ GrafiteAst.Tactic (loc, Some tac, punct)
+ | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
+ | tac = non_punctuation_tactical; punct = punctuation_tactical ->
+ GrafiteAst.NonPunctuationTactical (loc, tac, punct)
| mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
]
];