type ast_statement =
(CicNotationPt.term, CicNotationPt.term,
- CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
+ CicNotationPt.term GrafiteAst.reduction,
+ CicNotationPt.term CicNotationPt.obj, string)
GrafiteAst.statement
type statement =
| SYMBOL "<" -> `RightToLeft ]
];
int: [ [ num = NUMBER -> int_of_string num ] ];
+ intros_names: [
+ [ idents = OPT ident_list0 ->
+ match idents with None -> [] | Some idents -> idents
+ ]
+ ];
intros_spec: [
- [ num = OPT [ num = int -> num ]; idents = OPT ident_list0 ->
- let idents = match idents with None -> [] | Some idents -> idents in
+ [ OPT [ IDENT "names" ];
+ num = OPT [ num = int -> num ];
+ idents = intros_names ->
num, idents
]
];
GrafiteAst.Assumption loc
| IDENT "auto"; params = auto_params ->
GrafiteAst.Auto (loc,params)
+ | IDENT "cases"; what = tactic_term;
+ (num, idents) = intros_spec ->
+ GrafiteAst.Cases (loc, what, idents)
| IDENT "clear"; ids = LIST1 IDENT ->
GrafiteAst.Clear (loc, ids)
| IDENT "clearbody"; id = IDENT ->
| LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
| IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
GrafiteAst.We_need_to_prove (loc, t, id, t1)
+ | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
+ GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
| IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
| IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
macro: [
[ [ IDENT "check" ]; t = term ->
GrafiteAst.Check (loc, t)
- | [ IDENT "inline"]; suri = QSTRING; prefix = OPT QSTRING ->
- let prefix = match prefix with None -> "" | Some prefix -> prefix in
- GrafiteAst.Inline (loc,suri,prefix)
+ | [ IDENT "inline"];
+ style = OPT [ IDENT "procedural" ];
+ suri = QSTRING; prefix = OPT QSTRING ->
+ let style = match style with
+ | None -> GrafiteAst.Declarative
+ | Some _ -> GrafiteAst.Procedural
+ in
+ let prefix = match prefix with None -> "" | Some prefix -> prefix in
+ GrafiteAst.Inline (loc,style,suri,prefix)
| [ IDENT "hint" ] -> GrafiteAst.Hint loc
| [ IDENT "whelp"; "match" ] ; t = term ->
GrafiteAst.WMatch (loc,t)