b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
let binder = mk_binder_ast b typ vars body in
return_term loc binder
+ | b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+ let binder = mk_binder_ast b typ vars body in
+ return_term loc binder
| t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
]
in
CicAst.Appl (aux t1 @ [t2])
]
- | "binder" RIGHTA
- [
- b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
- let binder = mk_binder_ast b typ vars body in
- return_term loc binder
- ]
| "simple" NONA
[ sort = sort -> CicAst.Sort sort
| n = substituted_name -> return_term loc n
TacticAst.Apply (loc, t)
| [ IDENT "assumption" ] ->
TacticAst.Assumption loc
- | [ IDENT "auto" ] -> TacticAst.Auto loc
+ | [ IDENT "auto" ] ; num = OPT [ i = NUM -> int_of_string i ] ->
+ TacticAst.Auto (loc,num)
| [ IDENT "change" ];
t1 = tactic_term; "with"; t2 = tactic_term;
where = tactic_where ->
(match (pat, terms) with
| None, [] -> TacticAst.Reduce (loc, kind, None)
| None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
- | Some pat, [] -> TacticAst.Reduce (loc, kind, Some ([], pat))
+ | Some pat, [] -> fail loc "Missing term [list]"
| Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
| [ IDENT "reflexivity" ] ->
TacticAst.Reflexivity loc
| [ IDENT "replace" ];
t1 = tactic_term; "with"; t2 = tactic_term ->
TacticAst.Replace (loc, t1, t2)
- (* TODO Rewrite *)
+ | [ IDENT "rewrite" ; IDENT "left" ] ; t = term ->
+ TacticAst.Rewrite (loc,`Left, t, None)
+ | [ IDENT "rewrite" ; IDENT "right" ] ; t = term ->
+ TacticAst.Rewrite (loc,`Right, t, None)
(* TODO Replace_pattern *)
| [ IDENT "right" ] -> TacticAst.Right loc
| [ IDENT "ring" ] -> TacticAst.Ring loc
| [ IDENT "check" ]; t = term ->
TacticAst.Check (loc, t)
| [ IDENT "hint" ] -> TacticAst.Hint loc
+ | [ IDENT "whelp"; "match" ] ; t = term ->
+ TacticAst.WMatch (loc,t)
+ | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
+ TacticAst.WInstance (loc,t)
+ | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT ->
+ TacticAst.WLocate (loc,id)
+ | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
+ TacticAst.WElim (loc, t)
+ | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
+ TacticAst.WHint (loc,t)
| [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
]];
TacticAst.Alias (loc, spec)
]];
- statement: [
+ executable: [
[ cmd = command; SYMBOL "." -> TacticAst.Command (loc, cmd)
| tac = tactical; SYMBOL "." -> TacticAst.Tactical (loc, tac)
| mac = macro; SYMBOL "." -> TacticAst.Macro (loc, mac)
]
];
+
+ comment: [
+ [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
+ TacticAst.Code (loc, ex)
+ | str = NOTE ->
+ TacticAst.Note (loc, str)
+ ]
+ ];
+
+ statement: [
+ [ ex = executable -> TacticAst.Executable (loc,ex)
+ | com = comment -> TacticAst.Comment (loc, com)
+ ]
+ ];
END
let exc_located_wrapper f =