diff options
Diffstat (limited to 'parsing/g_ltac.ml4')
| -rw-r--r-- | parsing/g_ltac.ml4 | 255 |
1 files changed, 122 insertions, 133 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 7349a6f8..6ed22c7e 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -6,16 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_ltac.ml4,v 1.28.2.2 2004/07/16 19:30:38 herbelin Exp $ *) +(* $Id: g_ltac.ml4 8129 2006-03-05 09:05:12Z herbelin $ *) open Pp open Util -open Ast open Topconstr open Rawterm open Tacexpr open Vernacexpr -open Ast open Pcoq open Prim open Tactic @@ -37,163 +35,156 @@ let arg_of_expr = function TacArg a -> a | e -> Tacexp (e:raw_tactic_expr) +let tacarg_of_expr = function + | TacArg (Reference r) -> TacCall (dummy_loc,r,[]) + | TacArg a -> a + | e -> Tacexp (e:raw_tactic_expr) + (* Tactics grammar rules *) -if !Options.v7 then GEXTEND Gram - GLOBAL: tactic Vernac_.command tactic_arg; + GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval; -(* - GLOBAL: tactic_atom tactic_atom0 tactic_expr input_fun; -*) + tactic_expr: + [ "5" LEFTA + [ 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) ] + | "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" -> + TacMatchContext (b,false,mrl) + | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; + mrl = match_context_list; "end" -> + TacMatchContext (b,true,mrl) + | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> + TacMatch (b,c,mrl) + | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + TacFirst l + | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + TacSolve l + | IDENT "complete" ; ta = tactic_expr -> TacComplete ta + | IDENT "idtac"; l = LIST0 message_token -> TacId l + | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ]; + l = LIST0 message_token -> TacFail (n,l) + | IDENT "external"; com = STRING; req = STRING; la = LIST1 tactic_arg -> + TacArg (TacExternal (loc,com,req,la)) + | st = simple_tactic -> TacAtom (loc,st) + | a = may_eval_arg -> TacArg(a) + | IDENT "constr"; ":"; c = Constr.constr -> + TacArg(ConstrMayEval(ConstrTerm c)) + | IDENT "ipattern"; ":"; ipat = simple_intropattern -> + TacArg(IntroPattern ipat) + | r = reference; la = LIST1 tactic_arg -> + TacArg(TacCall (loc,r,la)) + | r = reference -> TacArg (Reference r) ] + | "0" + [ "("; a = tactic_expr; ")" -> a + | a = tactic_atom -> TacArg a ] ] + ; + (* Tactic arguments *) + tactic_arg: + [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> tacarg_of_expr a + | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat + | a = may_eval_arg -> a + | r = reference -> Reference r + | a = tactic_atom -> a + | c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ] + ; + may_eval_arg: + [ [ c = constr_eval -> ConstrMayEval c + | IDENT "fresh"; s = OPT STRING -> TacFreshId s ] ] + ; + constr_eval: + [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> + ConstrEval (rtc,c) + | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" -> + ConstrContext (id,c) + | IDENT "type"; IDENT "of"; c = Constr.constr -> + ConstrTypeOf c ] ] + ; + constr_may_eval: (* For extensions *) + [ [ c = constr_eval -> c + | c = Constr.constr -> ConstrTerm c ] ] + ; + tactic_atom: + [ [ id = METAIDENT -> MetaIdArg (loc,id) + | "()" -> TacVoid ] ] + ; + match_key: + [ [ "match" -> false ] ] + ; input_fun: - [ [ l = base_ident -> Some l - | "()" -> None ] ] + [ [ "_" -> None + | l = ident -> Some l ] ] ; let_clause: - [ [ id = identref; "="; te = tactic_letarg -> LETCLAUSE (id, None, te) - | id = base_ident; ":"; c = Constr.constr; ":="; "Proof" -> - LETTOPCLAUSE (id, c) - | id = identref; ":"; c = constrarg; ":="; te = tactic_letarg -> - LETCLAUSE (id, Some (TacArg(ConstrMayEval c)), te) - | id = base_ident; ":"; c = Constr.constr -> - LETTOPCLAUSE (id, c) ] ] + [ [ id = identref; ":="; te = tactic_expr -> + LETCLAUSE (id, None, arg_of_expr te) + | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + LETCLAUSE (id, None, arg_of_expr (TacFun(args,te))) ] ] ; rec_clause: - [ [ name = identref; it = LIST1 input_fun; "->"; body = tactic_expr -> + [ [ name = identref; it = LIST1 input_fun; ":="; body = tactic_expr -> (name,(it,body)) ] ] ; match_pattern: - [ [ id = Constr.constr_pattern; "["; pc = Constr.constr_pattern; "]" -> - let (_,s) = coerce_to_id id in Subterm (Some s, pc) - | "["; pc = Constr.constr_pattern; "]" -> Subterm (None,pc) - | pc = Constr.constr_pattern -> Term pc ] ] + [ [ IDENT "context"; oid = OPT Constr.ident; + "["; pc = Constr.lconstr_pattern; "]" -> + Subterm (oid, pc) + | pc = Constr.lconstr_pattern -> Term pc ] ] ; match_hyps: [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) ] ] ; match_context_rule: - [ [ "["; largs = LIST0 match_hyps SEP ";"; "|-"; mp = match_pattern; "]"; - "->"; te = tactic_expr -> Pat (largs, mp, te) - | IDENT "_"; "->"; te = tactic_expr -> All te ] ] + [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; + "=>"; te = tactic_expr -> Pat (largs, mp, te) + | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; + "]"; "=>"; te = tactic_expr -> Pat (largs, mp, te) + | "_"; "=>"; te = tactic_expr -> All te ] ] ; match_context_list: [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ] ; match_rule: - [ [ "["; mp = match_pattern; "]"; "->"; te = tactic_expr -> Pat ([],mp,te) - | IDENT "_"; "->"; te = tactic_expr -> All te ] ] + [ [ mp = match_pattern; "=>"; te = tactic_expr -> Pat ([],mp,te) + | "_"; "=>"; te = tactic_expr -> All te ] ] ; match_list: [ [ mrl = LIST1 match_rule SEP "|" -> mrl | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ] ; - tactic_expr: - [ [ ta = tactic_expr5 -> ta ] ] - ; - tactic_expr5: - [ [ ta0 = tactic_expr5; ";"; ta1 = tactic_expr4 -> TacThen (ta0, ta1) - | ta = tactic_expr5; ";"; "["; lta = LIST0 tactic_expr SEP "|"; "]" -> - TacThens (ta, lta) - | y = tactic_expr4 -> y ] ] - ; - tactic_expr4: - [ [ ta = tactic_expr3 -> ta ] ] - ; - tactic_expr3: - [ [ IDENT "Try"; ta = tactic_expr3 -> TacTry ta - | IDENT "Do"; n = int_or_var; ta = tactic_expr3 -> TacDo (n,ta) - | IDENT "Repeat"; ta = tactic_expr3 -> TacRepeat ta - | IDENT "Progress"; ta = tactic_expr3 -> TacProgress ta - | IDENT "Info"; tc = tactic_expr3 -> TacInfo tc - | ta = tactic_expr2 -> ta ] ] - ; - tactic_expr2: - [ [ ta0 = tactic_atom; "Orelse"; ta1 = tactic_expr3 -> TacOrelse (ta0,ta1) - | ta = tactic_atom -> ta ] ] - ; - tactic_atom: - [ [ IDENT "Fun"; it = LIST1 input_fun ; "->"; body = tactic_expr -> - TacFun (it,body) - | IDENT "Rec"; rc = rec_clause -> - warning "'Rec f ...' is obsolete; use 'Rec f ... In f' instead"; - TacLetRecIn ([rc],TacArg (Reference (Libnames.Ident (fst rc)))) - | IDENT "Rec"; rc = rec_clause; rcl = LIST0 rec_clause SEP "And"; - [IDENT "In" | "in"]; body = tactic_expr -> TacLetRecIn (rc::rcl,body) - | IDENT "Let"; llc = LIST1 let_clause SEP "And"; IDENT "In"; - u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u) - - | IDENT "Match"; IDENT "Context"; IDENT "With"; mrl = match_context_list - -> TacMatchContext (false,mrl) - | IDENT "Match"; IDENT "Reverse"; IDENT "Context"; IDENT "With"; mrl = match_context_list - -> TacMatchContext (true,mrl) - | IDENT "Match"; c = constrarg; IDENT "With"; mrl = match_list -> - TacMatch (TacArg(ConstrMayEval c),mrl) -(*To do: put Abstract in Refiner*) - | IDENT "Abstract"; tc = tactic_expr -> TacAbstract (tc,None) - | IDENT "Abstract"; tc = tactic_expr; "using"; s = base_ident -> - TacAbstract (tc,Some s) -(*End of To do*) - | IDENT "First" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> - TacFirst l - | IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> - TacSolve l - | IDENT "Idtac" ; s = [ s = STRING -> s | -> ""] -> TacId s - | IDENT "Fail"; n = [ n = int_or_var -> n | -> fail_default_value ]; - s = [ s = STRING -> s | -> ""] -> TacFail (n,s) - | st = simple_tactic -> TacAtom (loc,st) - | "("; a = tactic_expr; ")" -> a - | a = tactic_arg -> TacArg a - ] ] - ; - (* Tactic arguments *) - tactic_arg: - [ [ ta = tactic_arg1 -> ta ] ] - ; - tactic_letarg: - (* Cannot be merged with tactic_arg1, since then "In"/"And" are - parsed as lqualid! *) - [ [ IDENT "Eval"; rtc = red_expr; "in"; c = Constr.constr -> - ConstrMayEval (ConstrEval (rtc,c)) - | IDENT "Inst"; id = identref; "["; c = Constr.constr; "]" -> - ConstrMayEval (ConstrContext (id,c)) - | IDENT "Check"; c = Constr.constr -> - ConstrMayEval (ConstrTypeOf c) - | IDENT "FreshId"; s = OPT STRING -> TacFreshId s - | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat - | r = reference -> Reference r - | ta = tactic_arg0 -> ta ] ] - ; - tactic_arg1: - [ [ IDENT "Eval"; rtc = red_expr; "in"; c = Constr.constr -> - ConstrMayEval (ConstrEval (rtc,c)) - | IDENT "Inst"; id = identref; "["; c = Constr.constr; "]" -> - ConstrMayEval (ConstrContext (id,c)) - | IDENT "Check"; c = Constr.constr -> - ConstrMayEval (ConstrTypeOf c) - | IDENT "FreshId"; s = OPT STRING -> TacFreshId s - | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat - | r = reference; la = LIST1 tactic_arg0 -> TacCall (loc,r,la) - | r = reference -> Reference r - | ta = tactic_arg0 -> ta ] ] - ; - tactic_arg0: - [ [ "("; a = tactic_expr; ")" -> arg_of_expr a - | "()" -> TacVoid - | r = reference -> Reference r - | n = integer -> Integer n - | id = METAIDENT -> MetaIdArg (loc,id) - | "?" -> ConstrMayEval (ConstrTerm (CHole loc)) - | "?"; n = natural -> ConstrMayEval (ConstrTerm (CPatVar (loc,(false,Pattern.patvar_of_int n)))) - | "'"; c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ] + message_token: + [ [ id = identref -> MsgIdent (AI id) + | s = STRING -> MsgString s + | n = integer -> MsgInt n ] ] ; (* Definitions for tactics *) - deftok: - [ [ IDENT "Meta" - | IDENT "Tactic" ] ] - ; tacdef_body: [ [ name = identref; it=LIST1 input_fun; ":="; body = tactic_expr -> (name, TacFun (it, body)) @@ -204,10 +195,8 @@ GEXTEND Gram [ [ tac = tactic_expr -> tac ] ] ; Vernac_.command: - [ [ deftok; "Definition"; b = tacdef_body -> - VernacDeclareTacticDefinition (false, [b]) - | IDENT "Recursive"; deftok; "Definition"; - l = LIST1 tacdef_body SEP "And" -> + [ [ IDENT "Ltac"; + l = LIST1 tacdef_body SEP "with" -> VernacDeclareTacticDefinition (true, l) ] ] ; END |