| SYMBOL "<" -> `RightToLeft ]
];
int: [ [ num = NUMBER -> int_of_string num ] ];
+ intros_names: [
+ [ idents = OPT ident_list0 ->
+ match idents with None -> [] | Some idents -> idents
+ ]
+ ];
intros_spec: [
[ OPT [ IDENT "names" ];
num = OPT [ num = int -> num ];
- idents = OPT ident_list0 ->
- let idents = match idents with None -> [] | Some idents -> idents in
+ 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 ->
GrafiteAst.Reflexivity loc
| IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Replace (loc, p, t)
- | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec ->
+ | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
+ xnames = OPT [ "as"; n = ident_list0 -> n ] ->
let (pt,_,_) = p in
if pt <> None then
raise
(CicNotationParser.Parse_error
"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
else
- GrafiteAst.Rewrite (loc, d, t, p)
+ let n = match xnames with None -> [] | Some names -> names in
+ GrafiteAst.Rewrite (loc, d, t, p, n)
| IDENT "right" ->
GrafiteAst.Right loc
| IDENT "ring" ->
| 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 ->
[ [ IDENT "check" ]; t = term ->
GrafiteAst.Check (loc, t)
| [ IDENT "inline"];
- style = OPT [ IDENT "procedural" ];
+ style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
suri = QSTRING; prefix = OPT QSTRING ->
let style = match style with
- | None -> GrafiteAst.Declarative
- | Some _ -> GrafiteAst.Procedural
+ | None -> GrafiteAst.Declarative
+ | Some depth -> GrafiteAst.Procedural depth
in
let prefix = match prefix with None -> "" | Some prefix -> prefix in
GrafiteAst.Inline (loc,style,suri,prefix)
GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
| "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
defs = CicNotationParser.let_defs ->
+ (* In case of mutual definitions here we produce just
+ the syntax tree for the first one. The others will be
+ generated from the completely specified term just before
+ insertion in the environment. We use the flavour
+ `MutualDefinition to rememer this. *)
let name,ty =
match defs with
| (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
| _ -> assert false
in
let body = Ast.Ident (name,None) in
- GrafiteAst.Obj (loc, Ast.Theorem(`Definition, name, ty,
- Some (Ast.LetRec (ind_kind, defs, body))))
+ let flavour =
+ if List.length defs = 1 then
+ `Definition
+ else
+ `MutualDefinition
+ in
+ GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
+ Some (Ast.LetRec (ind_kind, defs, body))))
| IDENT "inductive"; spec = inductive_spec ->
let (params, ind_types) = spec in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))