From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- parsing/g_ltac.ml4 | 131 ++++++++++++++++++++++++++++++++--------------------- 1 file changed, 79 insertions(+), 52 deletions(-) (limited to 'parsing/g_ltac.ml4') diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 34615ad1..b4d96e5c 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -1,21 +1,23 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* a | e -> Tacexp (e:raw_tactic_expr) +let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () +let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n +let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat + (* Tactics grammar rules *) GEXTEND Gram - GLOBAL: tactic Vernac_.command tactic_expr binder_tactic tactic_arg + GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg constr_may_eval; tactic_then_last: @@ -44,29 +50,44 @@ GEXTEND Gram | -> ([TacId []], None) ] ] ; + tactic_then_locality: (* [true] for the local variant [TacThens] and [false] + for [TacExtend] *) + [ [ "[" ; l = OPT">" -> if Option.is_empty l then true else false ] ] + ; tactic_expr: [ "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, [||]) - | ta0 = tactic_expr; ";"; "["; (first,tail) = tactic_then_gen; "]" -> - match tail with - | Some (t,last) -> TacThen (ta0, Array.of_list first, t, last) - | None -> TacThens (ta0,first) ] + [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1) + | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0,ta1) + | ta0 = tactic_expr; ";"; l = tactic_then_locality; (first,tail) = tactic_then_gen; "]" -> + match l , tail with + | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last)) + | true , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last) + | false , None -> TacThen (ta0,TacDispatch first) + | true , None -> TacThens (ta0,first) ] | "3" RIGHTA [ IDENT "try"; ta = tactic_expr -> TacTry ta | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta) + | IDENT "time"; s = OPT string; ta = tactic_expr -> TacTime (s,ta) | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta | IDENT "progress"; ta = tactic_expr -> TacProgress ta + | IDENT "once"; ta = tactic_expr -> TacOnce ta + | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta + | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta (*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 = binder_tactic -> TacOrelse (ta0,ta1) + [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1) + | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1) + | IDENT "tryif" ; ta = tactic_expr ; + "then" ; tat = tactic_expr ; + "else" ; tae = tactic_expr -> TacIfThenCatch(ta,tat,tae) + | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] | "1" RIGHTA [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> @@ -81,23 +102,25 @@ GEXTEND Gram | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> TacSolve l | 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 (loc,TacExternal (loc,com,req,la)) - | st = simple_tactic -> TacAtom (loc,st) - | a = may_eval_arg -> TacArg(loc,a) - | IDENT "constr"; ":"; id = METAIDENT -> - TacArg(loc,MetaIdArg (loc,false,id)) + | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ]; + l = LIST0 message_token -> TacFail (g,n,l) + | st = simple_tactic -> st | IDENT "constr"; ":"; c = Constr.constr -> - TacArg(loc,ConstrMayEval(ConstrTerm c)) - | IDENT "ipattern"; ":"; ipat = simple_intropattern -> - TacArg(loc,IntroPattern ipat) + TacArg(!@loc,ConstrMayEval(ConstrTerm c)) + | a = tactic_top_or_arg -> TacArg(!@loc,a) | r = reference; la = LIST0 tactic_arg -> - TacArg(loc,TacCall (loc,r,la)) ] + TacArg(!@loc,TacCall (!@loc,r,la)) ] | "0" [ "("; a = tactic_expr; ")" -> a - | a = tactic_atom -> TacArg (loc,a) ] ] + | "["; ">"; (tf,tail) = tactic_then_gen; "]" -> + begin match tail with + | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) + | None -> TacDispatch tf + end + | a = tactic_atom -> TacArg (!@loc,a) ] ] + ; + failkw: + [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ] ; (* binder_tactic: level 5 of tactic_expr *) binder_tactic: @@ -112,21 +135,26 @@ GEXTEND Gram (* Tactic arguments *) tactic_arg: [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a - | IDENT "ltac"; ":"; n = natural -> Integer n - | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat - | a = may_eval_arg -> a + | IDENT "ltac"; ":"; n = natural -> TacGeneric (genarg_of_int n) + | a = tactic_top_or_arg -> a | r = reference -> Reference r | c = Constr.constr -> ConstrMayEval (ConstrTerm c) (* Unambigous entries: tolerated w/o "ltac:" modifier *) - | id = METAIDENT -> MetaIdArg (loc,true,id) - | "()" -> TacVoid ] ] + | id = METAIDENT -> MetaIdArg (!@loc,true,id) + | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; - may_eval_arg: - [ [ c = constr_eval -> ConstrMayEval c - | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l ] ] + (* Can be used as argument and at toplevel in tactic expressions. *) + tactic_top_or_arg: + [ [ IDENT "uconstr"; ":" ; c = uconstr -> UConstr c + | IDENT "ipattern"; ":"; ipat = simple_intropattern -> + TacGeneric (genarg_of_ipattern ipat) + | c = constr_eval -> ConstrMayEval c + | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l + | IDENT "type_term"; c=uconstr -> TacPretype c + | IDENT "numgoals" -> TacNumgoals ] ] ; fresh_id: - [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (loc,id) ] ] + [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (!@loc,id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -141,13 +169,15 @@ GEXTEND Gram | c = Constr.constr -> ConstrTerm c ] ] ; tactic_atom: - [ [ id = METAIDENT -> MetaIdArg (loc,true,id) - | n = integer -> Integer n - | r = reference -> TacCall (loc,r,[]) - | "()" -> TacVoid ] ] + [ [ id = METAIDENT -> MetaIdArg (!@loc,true,id) + | n = integer -> TacGeneric (genarg_of_int n) + | r = reference -> TacCall (!@loc,r,[]) + | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; match_key: - [ [ "match" -> false | "lazymatch" -> true ] ] + [ [ "match" -> Once + | "lazymatch" -> Select + | "multimatch" -> General ] ] ; input_fun: [ [ "_" -> None @@ -162,9 +192,11 @@ GEXTEND Gram match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> - Subterm (false,oid, pc) + let mode = not (!Flags.tactic_context_compat) in + Subterm (mode, oid, pc) | IDENT "appcontext"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> + msg_warning (strbrk "appcontext is deprecated"); Subterm (true,oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; @@ -175,10 +207,10 @@ GEXTEND Gram let t, ty = match mpv with | Term t -> (match t with - | CCast (loc, t, CastConv (_, ty)) -> Term t, Some (Term ty) + | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty) | _ -> mpv, None) | _ -> mpv, None - in Def (na, t, Option.default (Term (CHole (dummy_loc, None))) ty) + in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, IntroAnonymous, None))) ty) ] ] ; match_context_rule: @@ -201,7 +233,7 @@ GEXTEND Gram | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ] ; message_token: - [ [ id = identref -> MsgIdent (AI id) + [ [ id = identref -> MsgIdent id | s = STRING -> MsgString s | n = integer -> MsgInt n ] ] ; @@ -221,9 +253,4 @@ GEXTEND Gram tactic: [ [ tac = tactic_expr -> tac ] ] ; - Vernac_.command: - [ [ IDENT "Ltac"; - l = LIST1 tacdef_body SEP "with" -> - VernacDeclareTacticDefinition (use_module_locality (), true, l) ] ] - ; END -- cgit v1.2.3