GrafiteAst.ApplyS (loc, t, params)
| IDENT "assumption" ->
GrafiteAst.Assumption loc
- | IDENT "auto"; params =
- LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
- string_of_int v | v = IDENT -> v ] -> i,v ] ->
+ | IDENT "auto"; params = auto_params ->
GrafiteAst.Auto (loc,params)
| IDENT "clear"; ids = LIST1 IDENT ->
GrafiteAst.Clear (loc, ids)
| IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
GrafiteAst.Case(loc,id,params)
- | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation ->
- GrafiteAst.RewritingStep(loc, Some termine, t1, t2, cont)
- | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation ->
+ | start=[IDENT "conclude" -> None | IDENT "obtain" ; name = IDENT -> Some name] ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ; cont=rewriting_step_continuation ->
+ GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
+ | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
+ cont=rewriting_step_continuation ->
GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
]
+];
+ auto_params: [
+ [ params =
+ LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
+ string_of_int v | v = IDENT -> v ] -> i,v ] ->
+ params
+ ]
+];
+ auto_params': [
+ [ LPAREN; params = auto_params; RPAREN -> params
+ | -> []
+ ]
];
by_continuation: [
[ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)
]
];
rewriting_step_continuation : [
- [ IDENT "done" -> None
- | IDENT "we" ; IDENT "proved" ; id=IDENT -> Some (Cic.Name id)
- | -> Some Cic.Anonymous
+ [ IDENT "done" -> true
+ | -> false
]
];
atomic_tactical:
macro: [
[ [ IDENT "check" ]; t = term ->
GrafiteAst.Check (loc, t)
- | [ IDENT "inline"]; suri = QSTRING ->
- GrafiteAst.Inline (loc,suri)
+ | [ IDENT "inline"]; suri = QSTRING; prefix = OPT QSTRING ->
+ let prefix = match prefix with None -> "" | Some prefix -> prefix in
+ GrafiteAst.Inline (loc,suri,prefix)
| [ IDENT "hint" ] -> GrafiteAst.Hint loc
| [ IDENT "whelp"; "match" ] ; t = term ->
GrafiteAst.WMatch (loc,t)