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
]
];
subst: [
- [ subst = OPT [
- SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *)
- PAREN "[";
- substs = LIST1 [
- i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
- ] SEP SYMBOL ";";
- PAREN "]" ->
- substs
- ] -> subst
+ [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *)
+ PAREN "[";
+ substs = LIST1 [
+ i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
+ ] SEP SYMBOL ";";
+ PAREN "]" ->
+ substs
]
];
substituted_name: [ (* a subs.name is an explicit substitution subject *)
- [ s = IDENT; subst = subst -> CicAst.Ident (s, subst)
- | s = URI; subst = subst -> CicAst.Uri (ind_expansion s, subst)
+ [ s = IDENT; subst = OPT subst -> CicAst.Ident (s, subst)
+ | s = URI; subst = OPT subst -> CicAst.Uri (ind_expansion s, subst)
]
];
name: [ (* as substituted_name with no explicit substitution *)
b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
let binder = mk_binder_ast b typ vars body in
return_term loc binder
+ | b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+ let binder = mk_binder_ast b typ vars body in
+ return_term loc binder
+ | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
+ return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
]
| "logic_add" LEFTA [ (* nothing here by default *) ]
| "logic_mult" LEFTA [ (* nothing here by default *) ]
in
CicAst.Appl (aux t1 @ [t2])
]
- | "binder" RIGHTA
- [
- b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
- let binder = mk_binder_ast b typ vars body in
- return_term loc binder
- | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
- return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
- ]
| "simple" NONA
[ sort = sort -> CicAst.Sort sort
| n = substituted_name -> return_term loc n
| i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ())))
| IMPLICIT -> return_term loc CicAst.Implicit
+ | PLACEHOLDER -> return_term loc CicAst.UserInput
| m = META;
substs = [
PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" ->
reduction_kind: [
[ [ IDENT "reduce" ] -> `Reduce
| [ IDENT "simplify" ] -> `Simpl
- | [ IDENT "whd" ] -> `Whd ]
+ | [ IDENT "whd" ] -> `Whd
+ | [ IDENT "normalize" ] -> `Normalize ]
];
tactic: [
[ [ IDENT "absurd" ]; t = tactic_term ->
let idents = match idents with None -> [] | Some idents -> idents in
TacticAst.Intros (loc, num, idents)
| [ IDENT "intro" ] ->
- TacticAst.Intros (loc, None, [])
+ TacticAst.Intros (loc, Some 1, [])
| [ IDENT "left" ] -> TacticAst.Left loc
| [ "let" | "Let" ];
t = tactic_term; "in"; where = IDENT ->
| None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
| Some pat, [] -> fail loc "Missing term [list]"
| Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
+ | kind = reduction_kind; where = IDENT ; IDENT "at" ; pat = term ->
+ TacticAst.ReduceAt (loc, kind, where, pat)
| [ IDENT "reflexivity" ] ->
TacticAst.Reflexivity loc
| [ IDENT "replace" ];
(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))
+
(**/**)