- return_tactic loc (TacticAst.Intros (num, idents))
- | [ IDENT "intro" | IDENT "Intro" ] ->
- return_tactic loc (TacticAst.Intros (Some 1, []))
- | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left
- | [ "let" | "Let" ];
- t = tactic_term; "in"; where = IDENT ->
- return_tactic loc (TacticAst.LetIn (t, where))
- | kind = reduction_kind;
- pat = OPT [
- "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] ->
- pat
- ];
- terms = LIST0 term SEP SYMBOL "," ->
- let tac =
- (match (pat, terms) with
- | None, [] -> TacticAst.Reduce (kind, None)
- | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal))
- | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat))
- | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat)))
- in
- return_tactic loc tac
- | [ IDENT "reflexivity" | IDENT "Reflexivity" ] ->
- return_tactic loc TacticAst.Reflexivity
- | [ IDENT "replace" | IDENT "Replace" ];
- t1 = tactic_term; "with"; t2 = tactic_term ->
- return_tactic loc (TacticAst.Replace (t1, t2))
- (* TODO Rewrite *)
- (* TODO Replace_pattern *)
- | [ IDENT "right" | IDENT "Right" ] -> return_tactic loc TacticAst.Right
- | [ IDENT "ring" | IDENT "Ring" ] -> return_tactic loc TacticAst.Ring
- | [ IDENT "split" | IDENT "Split" ] -> return_tactic loc TacticAst.Split
- | [ IDENT "symmetry" | IDENT "Symmetry" ] ->
- return_tactic loc TacticAst.Symmetry
- | [ IDENT "transitivity" | IDENT "Transitivity" ];
- t = tactic_term ->
- return_tactic loc (TacticAst.Transitivity t)
+ TacticAst.Elim (loc, what, using, num, idents)
+ | IDENT "elimType"; what = tactic_term;
+ using = OPT [ "using"; using = tactic_term -> using ];
+ OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 ->
+ let idents = match idents with None -> [] | Some idents -> idents in
+ TacticAst.ElimType (loc, what, using, num, idents)
+ | IDENT "exact"; t = tactic_term ->
+ TacticAst.Exact (loc, t)
+ | IDENT "exists" ->
+ TacticAst.Exists loc
+ | IDENT "fail" -> TacticAst.Fail loc
+ | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
+ let (pt,_,_) = p in
+ if pt <> None then
+ raise
+ (Parse_error
+ (loc,"the pattern cannot specify the term to replace, only its paths in the hypotheses and in the conclusion"))
+ else
+ TacticAst.Fold (loc, kind, t, p)
+ | IDENT "fourier" ->
+ TacticAst.Fourier loc
+ | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 ->
+ let idents = match idents with None -> [] | Some idents -> idents in
+ TacticAst.FwdSimpl (loc, hyp, idents)
+ | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
+ TacticAst.Generalize (loc,p,id)
+ | IDENT "goal"; n = NUM ->
+ TacticAst.Goal (loc, int_of_string n)
+ | IDENT "id" -> TacticAst.IdTac loc
+ | IDENT "injection"; t = tactic_term ->
+ TacticAst.Injection (loc, t)
+ | IDENT "intro"; ident = OPT IDENT ->
+ let idents = match ident with None -> [] | Some id -> [id] in
+ TacticAst.Intros (loc, Some 1, idents)
+ | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 ->
+ let idents = match idents with None -> [] | Some idents -> idents in
+ TacticAst.Intros (loc, num, idents)
+ | IDENT "lapply";
+ depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ];
+ what = tactic_term;
+ to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
+ ident = OPT [ "using" ; ident = IDENT -> ident ] ->
+ let to_what = match to_what with None -> [] | Some to_what -> to_what in
+ TacticAst.LApply (loc, depth, to_what, what, ident)
+ | IDENT "left" -> TacticAst.Left loc
+ | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
+ TacticAst.LetIn (loc, t, where)
+ | kind = reduction_kind; p = pattern_spec ->
+ TacticAst.Reduce (loc, kind, p)
+ | IDENT "reflexivity" ->
+ TacticAst.Reflexivity loc
+ | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
+ TacticAst.Replace (loc, p, t)
+ | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec ->
+ let (pt,_,_) = p in
+ if pt <> None then
+ raise
+ (Parse_error
+ (loc,"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))
+ else
+ TacticAst.Rewrite (loc, d, t, p)
+ | IDENT "right" ->
+ TacticAst.Right loc
+ | IDENT "ring" ->
+ TacticAst.Ring loc
+ | IDENT "split" ->
+ TacticAst.Split loc
+ | IDENT "symmetry" ->
+ TacticAst.Symmetry loc
+ | IDENT "transitivity"; t = tactic_term ->
+ TacticAst.Transitivity (loc, t)