let return_tactical loc tactical = TacticAst.LocatedTactical (loc, tactical)
let return_command loc cmd = cmd
-let fail (x, y) msg =
+let fail floc msg =
+ let (x, y) = CicAst.loc_of_floc floc in
failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
let name_of_string = function
try
int_of_string num
with Failure _ ->
- let (x, y) = loc in
+ let (x, y) = CicAst.loc_of_floc loc in
raise (Parse_error (sprintf
"integer literal expected at characters %d-%d" x y))
]
substituted_name: [ (* a subs.name is an explicit substitution subject *)
[ s = [ IDENT | SYMBOL ];
subst = OPT [
- SYMBOL "\subst"; (* to avoid catching frequent "a [1]" cases *)
+ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *)
PAREN "[";
substs = LIST1 [
i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
];
tactical0: [ [ t = tactical; SYMBOL "." -> t ] ];
tactical:
- [ "sequence" LEFTA
+ [ "command" NONA
+ [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
+ | "sequence" LEFTA
[ tactics = LIST1 NEXT SEP SYMBOL ";" ->
return_tactical loc (TacticAst.Seq tactics)
]
| [ 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)
- | cmd = command -> return_tactical loc (TacticAst.Command cmd)
]
];
theorem_flavour: [ (* all flavours but Goal *)
]
];
command: [
- [ [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
+ [ [ 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)
let exc_located_wrapper f =
try
Lazy.force f
- with Stdpp.Exc_located ((x, y), exn) ->
+ with Stdpp.Exc_located (floc, exn) ->
+ let (x, y) = CicAst.loc_of_floc floc in
raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
(Printexc.to_string exn)))
else
try
Grammar.Entry.parse aliases (Stream.of_string s)
- with Stdpp.Exc_located ((x, y), exn) ->
+ with Stdpp.Exc_located (floc, exn) ->
+ let (x, y) = CicAst.loc_of_floc floc in
raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
(Printexc.to_string exn)))
end