];
tactical:
[ "sequence" LEFTA
- [ tacticals = LIST1 NEXT SEP SYMBOL ";" ->
- TacticAst.Seq (loc, tacticals)
+ [ tactical = NEXT -> tactical
+ | tacticals = LIST1 NEXT SEP SYMBOL ";" -> TacticAst.Seq (loc, tacticals)
]
| "then" NONA
[ tac = tactical;
(TacticAst.Then (loc, tac, tacs))
]
| "loops" RIGHTA
- [ [ IDENT "do" ]; count = int; tac = tactical ->
+ [ IDENT "do"; count = int; tac = tactical ->
TacticAst.Do (loc, count, tac)
- | [ IDENT "repeat" ]; tac = tactical ->
+ | IDENT "repeat"; tac = tactical ->
TacticAst.Repeat (loc, tac)
]
| "simple" NONA
let tactical_terminator = "."
let tactic_terminator = tactical_terminator
let command_terminator = tactical_terminator
-let tactical_separator = ";"
let pp_term_ast term = CicAstPp.pp_term term
let pp_term_cic term = CicPp.ppterm term
| Tactic (_, tac) -> pp_tactic tac
| Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac)
| Repeat (_, tac) -> "repeat " ^ pp_tactical tac
- | Seq (_, tacs) -> pp_tacticals tacs
+ | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs
| Then (_, tac, tacs) ->
- sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs)
- | Tries (_, tacs) -> sprintf "tries [%s]" (pp_tacticals tacs)
+ sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals ~sep:" | " tacs)
+ | Tries (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
| Try (_, tac) -> "try " ^ pp_tactical tac
-and pp_tacticals tacs =
- String.concat (tactical_separator ^ " ") (List.map pp_tactical tacs)
+and pp_tacticals ~sep tacs =
+ String.concat sep (List.map pp_tactical tacs)
let pp_tactical tac = pp_tactical tac ^ tactical_terminator
let pp_tactic tac = pp_tactic tac ^ tactic_terminator