- tactical0 : [ [ t = tactical; SYMBOL "." -> t ] ];
- tactical: [
- [ IDENT "fail" -> return_tactical loc TacticAst.Fail
- | IDENT "do"; count = int; tac = tactical ->
- return_tactical loc (TacticAst.Do (count, tac))
- | IDENT "id" -> return_tactical loc TacticAst.IdTac
- | IDENT "repeat"; tac = tactical ->
- return_tactical loc (TacticAst.Repeat tac)
- | tactics = LIST0 tactical SEP SYMBOL ";" ->
- return_tactical loc (TacticAst.Seq tactics)
- | tac = tactical;
- PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
- return_tactical loc (TacticAst.Then (tac, tacs))
- | IDENT "tries";
- PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
- return_tactical loc (TacticAst.Tries tacs)
- | IDENT "try"; tac = tactical -> return_tactical loc (TacticAst.Try tac)
- | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
- | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
+ tactical0: [ [ t = tactical; SYMBOL "." -> t ] ];
+ tactical:
+ [ "command" NONA
+ [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
+ | "sequence" LEFTA
+ [ tactics = LIST1 NEXT SEP SYMBOL ";" ->
+ return_tactical loc (TacticAst.Seq tactics)
+ ]
+ | "then" NONA
+ [ tac = tactical;
+ PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
+ return_tactical loc (TacticAst.Then (tac, tacs))
+ ]
+ | "loops" RIGHTA
+ [ [ IDENT "do" | IDENT "Do" ]; count = int; tac = tactical ->
+ return_tactical loc (TacticAst.Do (count, tac))
+ | [ IDENT "repeat" | IDENT "Repeat" ]; tac = tactical ->
+ return_tactical loc (TacticAst.Repeat tac)
+ ]
+ | "simple" NONA
+ [ [ IDENT "tries" | IDENT "Tries" ];
+ PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
+ return_tactical loc (TacticAst.Tries tacs)
+ | [ IDENT "try" | IDENT "Try" ]; tac = NEXT ->
+ return_tactical loc (TacticAst.Try tac)
+ | [ IDENT "fail" | IDENT "Fail" ] -> return_tactical loc TacticAst.Fail
+ | [ IDENT "id" | IDENT "Id" ] -> return_tactical loc TacticAst.IdTac
+ | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
+ | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
+ ]
+ ];
+ theorem_flavour: [ (* all flavours but Goal *)
+ [ [ IDENT "definition" | IDENT "Definition" ] -> `Definition
+ | [ IDENT "fact" | IDENT "Fact" ] -> `Fact
+ | [ IDENT "lemma" | IDENT "Lemma" ] -> `Lemma
+ | [ IDENT "remark" | IDENT "Remark" ] -> `Remark
+ | [ IDENT "theorem" | IDENT "Theorem" ] -> `Theorem
+ ]
+ ];
+ command: [
+ [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort
+ | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
+ | [ IDENT "quit" | IDENT "Quit" ] -> return_command loc TacticAst.Quit
+ | [ IDENT "qed" | IDENT "Qed" ] ->
+ return_command loc (TacticAst.Qed None)
+ | [ IDENT "save" | IDENT "Save" ]; name = IDENT ->
+ return_command loc (TacticAst.Qed (Some name))
+ | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ return_command loc (TacticAst.Theorem (flavour, name, typ, body))
+ | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ return_command loc (TacticAst.Theorem (`Goal, None, typ, body))