GLOBAL: term statement;
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
- ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
+ new_name: [
+ [ id = IDENT -> Some id
+ | SYMBOL "_" -> None ]
+ ];
+ ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
tactic_term_list1: [
[ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
];
GrafiteAst.ApplyS (loc, t, params)
| IDENT "assumption" ->
GrafiteAst.Assumption loc
- | IDENT "auto"; params = auto_params ->
- GrafiteAst.Auto (loc,params)
+ | IDENT "autobatch"; params = auto_params ->
+ GrafiteAst.AutoBatch (loc,params)
| IDENT "cases"; what = tactic_term;
- (num, idents) = intros_spec ->
- GrafiteAst.Cases (loc, what, idents)
+ specs = intros_spec ->
+ GrafiteAst.Cases (loc, what, specs)
| IDENT "clear"; ids = LIST1 IDENT ->
GrafiteAst.Clear (loc, ids)
| IDENT "clearbody"; id = IDENT ->
GrafiteAst.ClearBody (loc,id)
| IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Change (loc, what, t)
+ | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
+ OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
+ let times = match times with None -> 1 | Some i -> i in
+ GrafiteAst.Compose (loc, t1, t2, times, specs)
| IDENT "constructor"; n = int ->
GrafiteAst.Constructor (loc, n)
| IDENT "contradiction" ->
GrafiteAst.Contradiction loc
| IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
GrafiteAst.Cut (loc, ident, t)
- | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
+ | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
let idents = match idents with None -> [] | Some idents -> idents in
GrafiteAst.Decompose (loc, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
| None -> None, [], Some Ast.UserInput
| Some pattern -> pattern
in
- GrafiteAst.Elim (loc, what, using, pattern, num, idents)
+ GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
| IDENT "elimType"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
- GrafiteAst.ElimType (loc, what, using, num, idents)
+ GrafiteAst.ElimType (loc, what, using, (num, idents))
| IDENT "exact"; t = tactic_term ->
GrafiteAst.Exact (loc, t)
| IDENT "exists" ->
GrafiteAst.Fold (loc, kind, t, p)
| IDENT "fourier" ->
GrafiteAst.Fourier loc
- | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
+ | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
let idents = match idents with None -> [] | Some idents -> idents in
GrafiteAst.FwdSimpl (loc, hyp, idents)
| IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
GrafiteAst.Generalize (loc,p,id)
| IDENT "id" -> GrafiteAst.IdTac loc
| IDENT "intro"; ident = OPT IDENT ->
- let idents = match ident with None -> [] | Some id -> [id] in
- GrafiteAst.Intros (loc, Some 1, idents)
- | IDENT "intros"; (num, idents) = intros_spec ->
- GrafiteAst.Intros (loc, num, idents)
+ let idents = match ident with None -> [] | Some id -> [Some id] in
+ GrafiteAst.Intros (loc, (Some 1, idents))
+ | IDENT "intros"; specs = intros_spec ->
+ GrafiteAst.Intros (loc, specs)
| IDENT "inversion"; t = tactic_term ->
GrafiteAst.Inversion (loc, t)
| IDENT "lapply";
let prefix = match prefix with None -> "" | Some prefix -> prefix in
GrafiteAst.Inline (loc,style,suri,prefix)
| [ IDENT "hint" ] -> GrafiteAst.Hint loc
+ | IDENT "auto"; params = auto_params ->
+ GrafiteAst.AutoInteractive (loc,params)
| [ IDENT "whelp"; "match" ] ; t = term ->
GrafiteAst.WMatch (loc,t)
| [ IDENT "whelp"; IDENT "instance" ] ; t = term ->