diff options
Diffstat (limited to 'parsing/g_ltac.ml4')
| -rw-r--r-- | parsing/g_ltac.ml4 | 42 |
1 files changed, 26 insertions, 16 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index c01c23b6..27ff8140 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_ltac.ml4 9037 2006-07-11 12:43:50Z herbelin $ *) +(* $Id: g_ltac.ml4 9333 2006-11-02 13:59:14Z barras $ *) open Pp open Util @@ -43,38 +43,34 @@ let tacarg_of_expr = function (* Tactics grammar rules *) GEXTEND Gram - GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval; + GLOBAL: tactic Vernac_.command tactic_expr binder_tactic tactic_arg + constr_may_eval; tactic_expr: - [ "5" LEFTA - [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1) + [ "5" RIGHTA + [ te = binder_tactic -> te ] + | "4" LEFTA + [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1) + | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1) | ta = tactic_expr; ";"; "["; lta = LIST0 OPT tactic_expr SEP "|"; "]" -> let lta = List.map (function None -> TacId [] | Some t -> t) lta in TacThens (ta, lta) ] - | "4" - [ ] | "3" RIGHTA [ IDENT "try"; ta = tactic_expr -> TacTry ta | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta | IDENT "progress"; ta = tactic_expr -> TacProgress ta - | IDENT "info"; tc = tactic_expr -> TacInfo tc (*To do: put Abstract in Refiner*) | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None) | IDENT "abstract"; tc = NEXT; "using"; s = ident -> TacAbstract (tc,Some s) ] (*End of To do*) | "2" RIGHTA - [ ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] + [ ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) + | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] | "1" RIGHTA - [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr -> - TacFun (it,body) - | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in"; - body = tactic_expr -> TacLetRecIn (rcl,body) - | "let"; llc = LIST1 let_clause SEP "with"; "in"; - u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u) - | b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> + [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> TacMatchContext (b,false,mrl) | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; mrl = match_context_list; "end" -> @@ -104,6 +100,17 @@ GEXTEND Gram [ "("; a = tactic_expr; ")" -> a | a = tactic_atom -> TacArg a ] ] ; + (* binder_tactic: level 5 of tactic_expr *) + binder_tactic: + [ RIGHTA + [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> + TacFun (it,body) + | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in"; + body = tactic_expr LEVEL "5" -> TacLetRecIn (rcl,body) + | "let"; llc = LIST1 let_clause SEP "with"; "in"; + u = tactic_expr LEVEL "5" -> TacLetIn (make_letin_clause loc llc,u) + | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ] + ; (* Tactic arguments *) tactic_arg: [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> tacarg_of_expr a @@ -115,7 +122,10 @@ GEXTEND Gram ; may_eval_arg: [ [ c = constr_eval -> ConstrMayEval c - | IDENT "fresh"; s = OPT STRING -> TacFreshId s ] ] + | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l ] ] + ; + fresh_id: + [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (loc,id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> |