- 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:
+ [ "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
+(* | [ IDENT "goal" | IDENT "Goal" ] -> `Goal *)
+ ]
+ ];
+ theorem_cmd: [
+ [ flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ];
+ SYMBOL "." ->
+ (loc, flavour, name, typ, body)
+ | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ];
+ SYMBOL "." ->
+ (loc, `Goal, None, typ, body)
+ ]
+ ];
+ proof_cmd: [ [ [ IDENT "proof" | IDENT "Proof" ]; SYMBOL "." -> loc ] ];
+ qed_cmd: [
+ [ [ IDENT "qed" | IDENT "Qed" ]; SYMBOL "." -> (loc, None)
+ | [ IDENT "save" | IDENT "Save" ]; name = IDENT; SYMBOL "." ->
+ (loc, Some name)