summaryrefslogtreecommitdiff
path: root/parsing/g_ltac.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_ltac.ml4')
-rw-r--r--parsing/g_ltac.ml4131
1 files changed, 79 insertions, 52 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
-open Util
-open Topconstr
-open Glob_term
+open Compat
+open Constrexpr
open Tacexpr
-open Vernacexpr
+open Misctypes
+open Genarg
+open Genredexpr
+open Tok (* necessary for camlp4 *)
+
open Pcoq
-open Prim
-open Tactic
-open Tok
+open Pcoq.Prim
+open Pcoq.Tactic
let fail_default_value = ArgArg 0
@@ -23,10 +25,14 @@ let arg_of_expr = function
TacArg (loc,a) -> 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-11 23:49:45 +0000