let macro = Grammar.Entry.create grammar "macro"
let script = Grammar.Entry.create grammar "script"
let statement = Grammar.Entry.create grammar "statement"
+let statements = Grammar.Entry.create grammar "statements"
let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
vars body
EXTEND
- GLOBAL: term term0 statement;
+ GLOBAL: term term0 statement statements;
int: [
[ num = NUM ->
try
(params, ind_types)
] ];
- macro: [[
- [ IDENT "abort" ] -> TacticAst.Abort loc
- | [ IDENT "quit" ] -> TacticAst.Quit loc
+ macro: [
+ [ [ IDENT "quit" ] -> TacticAst.Quit loc
+(* | [ IDENT "abort" ] -> TacticAst.Abort loc *)
| [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
- | [ IDENT "undo" ]; steps = OPT NUM ->
+(* | [ IDENT "undo" ]; steps = OPT NUM ->
TacticAst.Undo (loc, int_opt steps)
| [ IDENT "redo" ]; steps = OPT NUM ->
- TacticAst.Redo (loc, int_opt steps)
+ TacticAst.Redo (loc, int_opt steps) *)
| [ IDENT "check" ]; t = term ->
TacticAst.Check (loc, t)
| [ IDENT "hint" ] -> TacticAst.Hint loc
| [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
TacticAst.WHint (loc,t)
| [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
- ]];
+ ]
+ ];
alias_spec: [
[ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
| com = comment -> TacticAst.Comment (loc, com)
]
];
+ statements: [
+ [ l = LIST0 [ statement ] -> l
+ ]
+ ];
END
let exc_located_wrapper f =
exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream))
let parse_statement stream =
exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
+let parse_statements stream =
+ exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream))
+
(**/**)