summaryrefslogtreecommitdiff
path: root/parsing/g_tactic.ml4
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /parsing/g_tactic.ml4
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'parsing/g_tactic.ml4')
-rw-r--r--parsing/g_tactic.ml4182
1 files changed, 118 insertions, 64 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index ad093507..c845daf2 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_tactic.ml4 12009 2009-03-23 22:55:37Z herbelin $ *)
+(* $Id$ *)
open Pp
open Pcoq
@@ -22,7 +22,7 @@ open Termops
let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta]
-let tactic_kw = [ "->"; "<-" ]
+let tactic_kw = [ "->"; "<-" ; "by" ]
let _ = List.iter (fun s -> Lexer.add_token("",s)) tactic_kw
(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
@@ -147,9 +147,29 @@ let induction_arg_of_constr (c,lbind as clbind) =
with _ -> ElimOnConstr clbind
else ElimOnConstr clbind
+let mkTacCase with_evar = function
+ | [([ElimOnConstr cl],None,(None,None))],None ->
+ TacCase (with_evar,cl)
+ (* Reinterpret numbers as a notation for terms *)
+ | [([(ElimOnAnonHyp n)],None,(None,None))],None ->
+ TacCase (with_evar,
+ (CPrim (dummy_loc, Numeral (Bigint.of_string (string_of_int n))),
+ NoBindings))
+ (* Reinterpret ident as notations for variables in the context *)
+ (* because we don't know if they are quantified or not *)
+ | [([ElimOnIdent id],None,(None,None))],None ->
+ TacCase (with_evar,(CRef (Ident id),NoBindings))
+ | ic ->
+ if List.exists (fun (cl,a,b) ->
+ List.exists (function ElimOnAnonHyp _ -> true | _ -> false) cl)
+ (fst ic)
+ then
+ error "Use of numbers as direct arguments of 'case' is not supported.";
+ TacInductionDestruct (false,with_evar,ic)
+
let rec mkCLambdaN_simple_loc loc bll c =
match bll with
- | ((loc1,_)::_ as idl,bk,t) :: bll ->
+ | ((loc1,_)::_ as idl,bk,t) :: bll ->
CLambdaN (loc,[idl,bk,t],mkCLambdaN_simple_loc (join_loc loc1 loc) bll c)
| ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c
| [] -> c
@@ -166,11 +186,39 @@ let map_int_or_var f = function
| Rawterm.ArgArg x -> Rawterm.ArgArg (f x)
| Rawterm.ArgVar _ as y -> y
+let all_concl_occs_clause = { onhyps=Some[]; concl_occs=all_occurrences_expr }
+
+let has_no_specified_occs cl =
+ (cl.onhyps = None ||
+ List.for_all (fun ((occs,_),_) -> occs = all_occurrences_expr)
+ (Option.get cl.onhyps))
+ && (cl.concl_occs = all_occurrences_expr
+ || cl.concl_occs = no_occurrences_expr)
+
+let merge_occurrences loc cl = function
+ | None ->
+ if has_no_specified_occs cl then (None, cl)
+ else
+ user_err_loc (loc,"",str "Found an \"at\" clause without \"with\" clause.")
+ | Some (occs,p) ->
+ (Some p,
+ if occs = all_occurrences_expr then cl
+ else if cl = all_concl_occs_clause then { onhyps=Some[]; concl_occs=occs }
+ else match cl.onhyps with
+ | Some [(occs',id),l] when
+ occs' = all_occurrences_expr && cl.concl_occs = no_occurrences_expr ->
+ { cl with onhyps=Some[(occs,id),l] }
+ | _ ->
+ if has_no_specified_occs cl then
+ user_err_loc (loc,"",str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.")
+ else
+ user_err_loc (loc,"",str "Cannot use clause \"at\" twice."))
+
(* Auxiliary grammar rules *)
GEXTEND Gram
GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
- bindings red_expr int_or_var open_constr casted_open_constr
+ bindings red_expr int_or_var open_constr casted_open_constr
simple_intropattern;
int_or_var:
@@ -183,7 +231,7 @@ GEXTEND Gram
;
(* An identifier or a quotation meta-variable *)
id_or_meta:
- [ [ id = identref -> AI id
+ [ [ id = identref -> AI id
(* This is used in quotations *)
| id = METAIDENT -> MetaId (loc,id) ] ]
@@ -215,19 +263,14 @@ GEXTEND Gram
| c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr ->
(Some (occs,c1), c2) ] ]
;
- smart_global:
- [ [ c = global -> AN c
- | s = ne_string; sc = OPT ["%"; key = IDENT -> key ] ->
- ByNotation (loc,s,sc) ] ]
- ;
occs_nums:
[ [ nl = LIST1 nat_or_var -> no_occurrences_expr_but nl
| "-"; n = nat_or_var; nl = LIST0 int_or_var ->
(* have used int_or_var instead of nat_or_var for compatibility *)
all_occurrences_expr_but (List.map (map_int_or_var abs) (n::nl)) ] ]
- ;
+ ;
occs:
- [ [ "at"; occs = occs_nums -> occs | -> all_occurrences_expr_but [] ] ]
+ [ [ "at"; occs = occs_nums -> occs | -> all_occurrences_expr ] ]
;
pattern_occ:
[ [ c = constr; nl = occs -> (nl,c) ] ]
@@ -242,13 +285,13 @@ GEXTEND Gram
[ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> loc,IntroOrAndPattern tc
| "()" -> loc,IntroOrAndPattern [[]]
| "("; si = simple_intropattern; ")" -> loc,IntroOrAndPattern [[si]]
- | "("; si = simple_intropattern; ",";
- tc = LIST1 simple_intropattern SEP "," ; ")" ->
+ | "("; si = simple_intropattern; ",";
+ tc = LIST1 simple_intropattern SEP "," ; ")" ->
loc,IntroOrAndPattern [si::tc]
- | "("; si = simple_intropattern; "&";
- tc = LIST1 simple_intropattern SEP "&" ; ")" ->
+ | "("; si = simple_intropattern; "&";
+ tc = LIST1 simple_intropattern SEP "&" ; ")" ->
(* (A & B & C) is translated into (A,(B,C)) *)
- let rec pairify = function
+ let rec pairify = function
| ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l]
| t::q -> IntroOrAndPattern [[t;(loc_of_ne_list q,pairify q)]]
in loc,pairify (si::tc) ] ]
@@ -256,10 +299,12 @@ GEXTEND Gram
naming_intropattern:
[ [ prefix = pattern_ident -> loc, IntroFresh prefix
| "?" -> loc, IntroAnonymous
- | id = ident -> loc, IntroIdentifier id ] ]
+ | id = ident -> loc, IntroIdentifier id
+ | "*" -> loc, IntroForthcoming true
+ | "**" -> loc, IntroForthcoming false ] ]
;
intropattern_modifier:
- [ [ IDENT "_eqn";
+ [ [ IDENT "_eqn";
id = [ ":"; id = naming_intropattern -> id | -> loc, IntroAnonymous ]
-> id ] ]
;
@@ -357,7 +402,7 @@ GEXTEND Gram
clause_dft_concl:
[ [ "in"; cl = in_clause -> cl
| occs=occs -> {onhyps=Some[]; concl_occs=occs}
- | -> {onhyps=Some[]; concl_occs=all_occurrences_expr} ] ]
+ | -> all_concl_occs_clause ] ]
;
clause_dft_all:
[ [ "in"; cl = in_clause -> cl
@@ -378,14 +423,14 @@ GEXTEND Gram
[ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat)
| -> None ] ]
;
- orient:
- [ [ "->" -> true
+ orient:
+ [ [ "->" -> true
| "<-" -> false
| -> true ]]
;
simple_binder:
[ [ na=name -> ([na],Default Explicit,CHole (loc, None))
- | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c)
+ | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c)
] ]
;
fixdecl:
@@ -401,7 +446,7 @@ GEXTEND Gram
(loc,id,bl,None,ty) ] ]
;
bindings_with_parameters:
- [ [ check_for_coloneq; "("; id = ident; bl = LIST0 simple_binder;
+ [ [ check_for_coloneq; "("; id = ident; bl = LIST0 simple_binder;
":="; c = lconstr; ")" -> (id, mkCLambdaN_simple bl c) ] ]
;
hintbases:
@@ -433,17 +478,17 @@ GEXTEND Gram
[ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ]
;
by_tactic:
- [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac
+ [ [ "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac
| -> TacId [] ] ]
;
opt_by_tactic:
- [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> Some tac
+ [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac
| -> None ] ]
;
- rename :
+ rename :
[ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
;
- rewriter :
+ rewriter :
[ [ "!"; c = constr_with_bindings -> (RepeatPlus,c)
| ["?"| LEFTQMARK]; c = constr_with_bindings -> (RepeatStar,c)
| n = natural; "!"; c = constr_with_bindings -> (Precisely n,c)
@@ -452,12 +497,18 @@ GEXTEND Gram
| c = constr_with_bindings -> (Precisely 1, c)
] ]
;
- oriented_rewriter :
+ oriented_rewriter :
[ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ]
- ;
+ ;
induction_clause:
- [ [ lc = LIST1 induction_arg; ipats = with_induction_names;
- el = OPT eliminator; cl = opt_clause -> (lc,el,ipats,cl) ] ]
+ [ [ lc = LIST1 induction_arg; ipats = with_induction_names;
+ el = OPT eliminator -> (lc,el,ipats) ] ]
+ ;
+ one_induction_clause:
+ [ [ ic = induction_clause; cl = opt_clause -> ([ic],cl) ] ]
+ ;
+ induction_clause_list:
+ [ [ ic = LIST1 induction_clause SEP ","; cl = opt_clause -> (ic,cl) ] ]
;
move_location:
[ [ IDENT "after"; id = id_or_meta -> MoveAfter id
@@ -466,9 +517,9 @@ GEXTEND Gram
| "at"; IDENT "top" -> MoveToEnd false ] ]
;
simple_tactic:
- [ [
+ [ [
(* Basic tactics *)
- IDENT "intros"; IDENT "until"; id = quantified_hypothesis ->
+ IDENT "intros"; IDENT "until"; id = quantified_hypothesis ->
TacIntrosUntil id
| IDENT "intros"; pl = intropatterns -> TacIntroPattern pl
| IDENT "intro"; id = ident; hto = move_location ->
@@ -482,7 +533,7 @@ GEXTEND Gram
| IDENT "exact_no_check"; c = constr -> TacExactNoCheck c
| IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c
- | IDENT "apply"; cl = LIST1 constr_with_bindings SEP ",";
+ | IDENT "apply"; cl = LIST1 constr_with_bindings SEP ",";
inhyp = in_hyp_as -> TacApply (true,false,cl,inhyp)
| IDENT "eapply"; cl = LIST1 constr_with_bindings SEP ",";
inhyp = in_hyp_as -> TacApply (true,true,cl,inhyp)
@@ -495,8 +546,8 @@ GEXTEND Gram
| IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator ->
TacElim (true,cl,el)
| IDENT "elimtype"; c = constr -> TacElimType c
- | IDENT "case"; cl = constr_with_bindings -> TacCase (false,cl)
- | IDENT "ecase"; cl = constr_with_bindings -> TacCase (true,cl)
+ | IDENT "case"; icl = induction_clause_list -> mkTacCase false icl
+ | IDENT "ecase"; icl = induction_clause_list -> mkTacCase true icl
| IDENT "casetype"; c = constr -> TacCaseType c
| "fix"; n = natural -> TacFix (None,n)
| "fix"; id = ident; n = natural -> TacFix (Some id,n)
@@ -519,11 +570,11 @@ GEXTEND Gram
TacLetTac (na,c,p,false)
(* Begin compatibility *)
- | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
- c = lconstr; ")" ->
+ | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
+ c = lconstr; ")" ->
TacAssert (None,Some (loc,IntroIdentifier id),c)
- | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
- c = lconstr; ")"; tac=by_tactic ->
+ | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+ c = lconstr; ")"; tac=by_tactic ->
TacAssert (Some tac,Some (loc,IntroIdentifier id),c)
(* End compatibility *)
@@ -538,8 +589,8 @@ GEXTEND Gram
| IDENT "generalize"; c = constr; l = LIST1 constr ->
let gen_everywhere c = ((all_occurrences_expr,c),Names.Anonymous) in
TacGeneralize (List.map gen_everywhere (c::l))
- | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs;
- na = as_name;
+ | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs;
+ na = as_name;
l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] ->
TacGeneralize (((nl,c),na)::l)
| IDENT "generalize"; IDENT "dependent"; c = constr -> TacGeneralizeDep c
@@ -551,18 +602,18 @@ GEXTEND Gram
(* Derived basic tactics *)
| IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
TacSimpleInductionDestruct (true,h)
- | IDENT "induction"; ic = induction_clause ->
- TacInductionDestruct (true,false,[ic])
- | IDENT "einduction"; ic = induction_clause ->
- TacInductionDestruct(true,true,[ic])
+ | IDENT "induction"; ic = one_induction_clause ->
+ TacInductionDestruct (true,false,ic)
+ | IDENT "einduction"; ic = one_induction_clause ->
+ TacInductionDestruct(true,true,ic)
| IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
| IDENT "simple"; IDENT "destruct"; h = quantified_hypothesis ->
TacSimpleInductionDestruct (false,h)
- | IDENT "destruct"; ic = induction_clause ->
- TacInductionDestruct(false,false,[ic])
- | IDENT "edestruct"; ic = induction_clause ->
- TacInductionDestruct(false,true,[ic])
+ | IDENT "destruct"; icl = induction_clause_list ->
+ TacInductionDestruct(false,false,icl)
+ | IDENT "edestruct"; icl = induction_clause_list ->
+ TacInductionDestruct(false,true,icl)
| IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
| IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
| IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr
@@ -600,10 +651,11 @@ GEXTEND Gram
| IDENT "eleft"; bl = with_bindings -> TacLeft (true,bl)
| IDENT "right"; bl = with_bindings -> TacRight (false,bl)
| IDENT "eright"; bl = with_bindings -> TacRight (true,bl)
- | IDENT "split"; bl = with_bindings -> TacSplit (false,false,bl)
- | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,bl)
- | "exists"; bl = opt_bindings -> TacSplit (false,true,bl)
- | IDENT "eexists"; bl = opt_bindings -> TacSplit (true,true,bl)
+ | IDENT "split"; bl = with_bindings -> TacSplit (false,false,[bl])
+ | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,[bl])
+ | "exists"; bll = LIST1 opt_bindings SEP "," -> TacSplit (false,true,bll)
+ | IDENT "eexists"; bll = LIST1 opt_bindings SEP "," ->
+ TacSplit (true,true,bll)
| IDENT "constructor"; n = num_or_meta; l = with_bindings ->
TacConstructor (false,n,l)
| IDENT "econstructor"; n = num_or_meta; l = with_bindings ->
@@ -614,33 +666,34 @@ GEXTEND Gram
(* Equivalence relations *)
| IDENT "reflexivity" -> TacReflexivity
| IDENT "symmetry"; cl = clause_dft_concl -> TacSymmetry cl
- | IDENT "transitivity"; c = constr -> TacTransitivity c
+ | IDENT "transitivity"; c = constr -> TacTransitivity (Some c)
+ | IDENT "etransitivity" -> TacTransitivity None
(* Equality and inversion *)
- | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
+ | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
cl = clause_dft_concl; t=opt_by_tactic -> TacRewrite (false,l,cl,t)
- | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
+ | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
cl = clause_dft_concl; t=opt_by_tactic -> TacRewrite (true,l,cl,t)
| IDENT "dependent"; k =
[ IDENT "simple"; IDENT "inversion" -> SimpleInversion
| IDENT "inversion" -> FullInversion
| IDENT "inversion_clear" -> FullInversionClear ];
- hyp = quantified_hypothesis;
+ hyp = quantified_hypothesis;
ids = with_inversion_names; co = OPT ["with"; c = constr -> c] ->
TacInversion (DepInversion (k,co,ids),hyp)
| IDENT "simple"; IDENT "inversion";
hyp = quantified_hypothesis; ids = with_inversion_names;
cl = in_hyp_list ->
TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)
- | IDENT "inversion";
+ | IDENT "inversion";
hyp = quantified_hypothesis; ids = with_inversion_names;
cl = in_hyp_list ->
TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)
- | IDENT "inversion_clear";
- hyp = quantified_hypothesis; ids = with_inversion_names;
+ | IDENT "inversion_clear";
+ hyp = quantified_hypothesis; ids = with_inversion_names;
cl = in_hyp_list ->
TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)
- | IDENT "inversion"; hyp = quantified_hypothesis;
+ | IDENT "inversion"; hyp = quantified_hypothesis;
"using"; c = constr; cl = in_hyp_list ->
TacInversion (InversionUsing (c,cl), hyp)
@@ -648,7 +701,8 @@ GEXTEND Gram
| r = red_tactic; cl = clause_dft_concl -> TacReduce (r, cl)
(* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
| IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
- TacChange (oc,c,cl)
+ let p,cl = merge_occurrences loc cl oc in
+ TacChange (p,c,cl)
] ]
;
END;;