author | noschinl |
Thu, 16 Apr 2015 15:55:55 +0200 | |
changeset 60088 | 0a064330a885 |
parent 60079 | ef4fe30e9ef1 |
child 60102 | 820e8e704ba6 |
child 60108 | d7fe3e0aca85 |
permissions | -rw-r--r-- |
59975 | 1 |
(* Title: HOL/Library/rewrite.ML |
2 |
Author: Christoph Traut, Lars Noschinski, TU Muenchen |
|
59739 | 3 |
|
59975 | 4 |
This is a rewrite method that supports subterm-selection based on patterns. |
59739 | 5 |
|
59975 | 6 |
The patterns accepted by rewrite are of the following form: |
7 |
<atom> ::= <term> | "concl" | "asm" | "for" "(" <names> ")" |
|
8 |
<pattern> ::= (in <atom> | at <atom>) [<pattern>] |
|
9 |
<args> ::= [<pattern>] ("to" <term>) <thms> |
|
59739 | 10 |
|
59975 | 11 |
This syntax was clearly inspired by Gonthier's and Tassi's language of |
12 |
patterns but has diverged significantly during its development. |
|
59739 | 13 |
|
59975 | 14 |
We also allow introduction of identifiers for bound variables, |
15 |
which can then be used to match arbitrary subterms inside abstractions. |
|
59739 | 16 |
*) |
17 |
||
59975 | 18 |
signature REWRITE = |
19 |
sig |
|
60079 | 20 |
datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list |
21 |
||
22 |
val mk_hole: int -> typ -> term |
|
23 |
||
24 |
val rewrite: Proof.context |
|
25 |
-> (term * (string * typ) list, string * typ option) pattern list * term option |
|
26 |
-> thm list |
|
27 |
-> cterm |
|
28 |
-> thm Seq.seq |
|
29 |
||
30 |
val rewrite_tac: Proof.context |
|
31 |
-> (term * (string * typ) list, string * typ option) pattern list * term option |
|
32 |
-> thm list |
|
33 |
-> int |
|
34 |
-> tactic |
|
59739 | 35 |
end |
36 |
||
59975 | 37 |
structure Rewrite : REWRITE = |
59739 | 38 |
struct |
39 |
||
40 |
datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list |
|
41 |
||
42 |
fun map_term_pattern f (Term x) = f x |
|
43 |
| map_term_pattern _ (For ss) = (For ss) |
|
44 |
| map_term_pattern _ At = At |
|
45 |
| map_term_pattern _ In = In |
|
46 |
| map_term_pattern _ Concl = Concl |
|
47 |
| map_term_pattern _ Asm = Asm |
|
48 |
||
49 |
||
50 |
exception NO_TO_MATCH |
|
51 |
||
52 |
fun SEQ_CONCAT (tacq : tactic Seq.seq) : tactic = fn st => Seq.maps (fn tac => tac st) tacq |
|
53 |
||
54 |
(* We rewrite subterms using rewrite conversions. These are conversions |
|
55 |
that also take a context and a list of identifiers for bound variables |
|
56 |
as parameters. *) |
|
57 |
type rewrite_conv = Proof.context -> (string * term) list -> conv |
|
58 |
||
59 |
(* To apply such a rewrite conversion to a subterm of our goal, we use |
|
60 |
subterm positions, which are just functions that map a rewrite conversion, |
|
61 |
working on the top level, to a new rewrite conversion, working on |
|
62 |
a specific subterm. |
|
63 |
||
64 |
During substitution, we are traversing the goal to find subterms that |
|
65 |
we can rewrite. For each of these subterms, a subterm position is |
|
66 |
created and later used in creating a conversion that we use to try and |
|
67 |
rewrite this subterm. *) |
|
68 |
type subterm_position = rewrite_conv -> rewrite_conv |
|
69 |
||
70 |
(* A focusterm represents a subterm. It is a tuple (t, p), consisting |
|
71 |
of the subterm t itself and its subterm position p. *) |
|
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
72 |
type focusterm = (Type.tyenv * Proof.context) * term * subterm_position |
59739 | 73 |
|
74 |
val dummyN = Name.internal "__dummy" |
|
75 |
val holeN = Name.internal "_hole" |
|
76 |
||
77 |
fun prep_meta_eq ctxt = |
|
78 |
Simplifier.mksimps ctxt #> map Drule.zero_var_indexes |
|
79 |
||
80 |
||
81 |
(* rewrite conversions *) |
|
82 |
||
83 |
fun abs_rewr_cconv ident : subterm_position = |
|
84 |
let |
|
85 |
fun add_ident NONE _ l = l |
|
86 |
| add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l |
|
59975 | 87 |
fun inner rewr ctxt idents = |
88 |
CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt |
|
59739 | 89 |
in inner end |
59975 | 90 |
|
59739 | 91 |
val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr |
92 |
val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr |
|
60050 | 93 |
val imp_rewr_cconv : subterm_position = fn rewr => CConv.concl_cconv 1 oo rewr |
60054
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
94 |
val with_prems_rewr_cconv : subterm_position = fn rewr => CConv.with_prems_cconv ~1 oo rewr |
59739 | 95 |
|
96 |
||
97 |
(* focus terms *) |
|
98 |
||
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
99 |
fun ft_abs ctxt (s,T) ((tyenv, u_ctxt), u, pos) = |
59739 | 100 |
case try (fastype_of #> dest_funT) u of |
101 |
NONE => raise TERM ("ft_abs: no function type", [u]) |
|
102 |
| SOME (U, _) => |
|
59975 | 103 |
let |
104 |
val tyenv' = |
|
105 |
if T = dummyT then tyenv |
|
106 |
else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv |
|
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
107 |
val (s', u_ctxt') = |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
108 |
case s of |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
109 |
NONE => yield_singleton Variable.variant_fixes (Name.internal dummyN) u_ctxt |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
110 |
| SOME s => (s, u_ctxt) |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
111 |
val x = Free (s', Envir.norm_type tyenv' T) |
59975 | 112 |
val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand} |
113 |
fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds |
|
114 |
val (u', pos') = |
|
115 |
case u of |
|
116 |
Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s) |
|
117 |
| _ => (u $ x, pos o eta_expand o abs_rewr_cconv s) |
|
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
118 |
in ((tyenv', u_ctxt'), u', pos') end |
59975 | 119 |
handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u]) |
59739 | 120 |
|
121 |
fun ft_fun _ (tyenv, l $ _, pos) = (tyenv, l, pos o fun_rewr_cconv) |
|
122 |
| ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft |
|
123 |
| ft_fun _ (_, t, _) = raise TERM ("ft_fun", [t]) |
|
124 |
||
60050 | 125 |
local |
126 |
||
127 |
fun ft_arg_gen cconv _ (tyenv, _ $ r, pos) = (tyenv, r, pos o cconv) |
|
128 |
| ft_arg_gen cconv ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg_gen cconv ctxt o ft_abs ctxt (NONE, T)) ft |
|
129 |
| ft_arg_gen _ _ (_, t, _) = raise TERM ("ft_arg", [t]) |
|
130 |
||
131 |
in |
|
132 |
||
133 |
val ft_arg = ft_arg_gen arg_rewr_cconv |
|
134 |
val ft_imp = ft_arg_gen imp_rewr_cconv |
|
135 |
||
136 |
end |
|
59739 | 137 |
|
138 |
(* Move to B in !!x_1 ... x_n. B. Do not eta-expand *) |
|
139 |
fun ft_params ctxt (ft as (_, t, _) : focusterm) = |
|
140 |
case t of |
|
141 |
Const (@{const_name "Pure.all"}, _) $ Abs (_,T,_) => |
|
142 |
(ft_params ctxt o ft_abs ctxt (NONE, T) o ft_arg ctxt) ft |
|
143 |
| Const (@{const_name "Pure.all"}, _) => |
|
144 |
(ft_params ctxt o ft_arg ctxt) ft |
|
145 |
| _ => ft |
|
146 |
||
147 |
fun ft_all ctxt ident (ft as (_, Const (@{const_name "Pure.all"}, T) $ _, _) : focusterm) = |
|
148 |
let |
|
149 |
val def_U = T |> dest_funT |> fst |> dest_funT |> fst |
|
150 |
val ident' = apsnd (the_default (def_U)) ident |
|
151 |
in (ft_abs ctxt ident' o ft_arg ctxt) ft end |
|
152 |
| ft_all _ _ (_, t, _) = raise TERM ("ft_all", [t]) |
|
153 |
||
154 |
fun ft_for ctxt idents (ft as (_, t, _) : focusterm) = |
|
155 |
let |
|
156 |
fun f rev_idents (Const (@{const_name "Pure.all"}, _) $ t) = |
|
157 |
let |
|
158 |
val (rev_idents', desc) = f rev_idents (case t of Abs (_,_,u) => u | _ => t) |
|
159 |
in |
|
160 |
case rev_idents' of |
|
161 |
[] => ([], desc o ft_all ctxt (NONE, NONE)) |
|
162 |
| (x :: xs) => (xs , desc o ft_all ctxt x) |
|
163 |
end |
|
164 |
| f rev_idents _ = (rev_idents, I) |
|
59975 | 165 |
in |
166 |
case f (rev idents) t of |
|
59739 | 167 |
([], ft') => SOME (ft' ft) |
168 |
| _ => NONE |
|
169 |
end |
|
170 |
||
171 |
fun ft_concl ctxt (ft as (_, t, _) : focusterm) = |
|
172 |
case t of |
|
60050 | 173 |
(Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_imp ctxt) ft |
59739 | 174 |
| _ => ft |
175 |
||
60054
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
176 |
fun ft_assm _ (tyenv, (Const (@{const_name "Pure.imp"}, _) $ l) $ _, pos) = |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
177 |
(tyenv, l, pos o with_prems_rewr_cconv) |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
178 |
| ft_assm _ (_, t, _) = raise TERM ("ft_assm", [t]) |
59739 | 179 |
|
180 |
fun ft_judgment ctxt (ft as (_, t, _) : focusterm) = |
|
59970 | 181 |
if Object_Logic.is_judgment ctxt t |
59739 | 182 |
then ft_arg ctxt ft |
183 |
else ft |
|
184 |
||
60055 | 185 |
(* Find all subterms that might be a valid point to apply a rule. *) |
186 |
fun valid_match_points ctxt (ft : focusterm) = |
|
59739 | 187 |
let |
60055 | 188 |
fun descend (_, _ $ _, _) = [ft_fun ctxt, ft_arg ctxt] |
189 |
| descend (_, Abs (_, T, _), _) = [ft_abs ctxt (NONE, T)] |
|
190 |
| descend _ = [] |
|
191 |
fun subseq ft = |
|
192 |
descend ft |> Seq.of_list |> Seq.maps (fn f => ft |> f |> valid_match_points ctxt) |
|
59739 | 193 |
fun is_valid (l $ _) = is_valid l |
194 |
| is_valid (Abs (_, _, a)) = is_valid a |
|
195 |
| is_valid (Var _) = false |
|
196 |
| is_valid (Bound _) = false |
|
197 |
| is_valid _ = true |
|
198 |
in |
|
60055 | 199 |
Seq.make (fn () => SOME (ft, subseq ft)) |
200 |
|> Seq.filter (#2 #> is_valid) |
|
59739 | 201 |
end |
202 |
||
60079 | 203 |
fun mk_hole i T = Var ((holeN, i), T) |
204 |
||
59739 | 205 |
fun is_hole (Var ((name, _), _)) = (name = holeN) |
206 |
| is_hole _ = false |
|
207 |
||
208 |
fun is_hole_const (Const (@{const_name rewrite_HOLE}, _)) = true |
|
209 |
| is_hole_const _ = false |
|
210 |
||
211 |
val hole_syntax = |
|
212 |
let |
|
213 |
(* Modified variant of Term.replace_hole *) |
|
214 |
fun replace_hole Ts (Const (@{const_name rewrite_HOLE}, T)) i = |
|
60079 | 215 |
(list_comb (mk_hole i (Ts ---> T), map_range Bound (length Ts)), i + 1) |
59739 | 216 |
| replace_hole Ts (Abs (x, T, t)) i = |
217 |
let val (t', i') = replace_hole (T :: Ts) t i |
|
218 |
in (Abs (x, T, t'), i') end |
|
219 |
| replace_hole Ts (t $ u) i = |
|
220 |
let |
|
221 |
val (t', i') = replace_hole Ts t i |
|
222 |
val (u', i'') = replace_hole Ts u i' |
|
223 |
in (t' $ u', i'') end |
|
224 |
| replace_hole _ a i = (a, i) |
|
225 |
fun prep_holes ts = #1 (fold_map (replace_hole []) ts 1) |
|
226 |
in |
|
227 |
Context.proof_map (Syntax_Phases.term_check 101 "hole_expansion" (K prep_holes)) |
|
228 |
#> Proof_Context.set_mode Proof_Context.mode_pattern |
|
229 |
end |
|
230 |
||
231 |
(* Find a subterm of the focusterm matching the pattern. *) |
|
232 |
fun find_matches ctxt pattern_list = |
|
233 |
let |
|
234 |
fun move_term ctxt (t, off) (ft : focusterm) = |
|
235 |
let |
|
236 |
val thy = Proof_Context.theory_of ctxt |
|
237 |
||
238 |
val eta_expands = |
|
239 |
let val (_, ts) = strip_comb t |
|
240 |
in map fastype_of (snd (take_suffix is_Var ts)) end |
|
241 |
||
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
242 |
fun do_match ((tyenv, u_ctxt), u, pos) = |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
243 |
case try (Pattern.match thy (apply2 Logic.mk_term (t,u))) (tyenv, Vartab.empty) of |
59739 | 244 |
NONE => NONE |
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
245 |
| SOME (tyenv', _) => SOME (off ((tyenv', u_ctxt), u, pos)) |
59739 | 246 |
|
247 |
fun match_argT T u = |
|
248 |
let val (U, _) = dest_funT (fastype_of u) |
|
249 |
in try (Sign.typ_match thy (T,U)) end |
|
250 |
handle TYPE _ => K NONE |
|
251 |
||
252 |
fun desc [] ft = do_match ft |
|
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
253 |
| desc (T :: Ts) (ft as ((tyenv, u_ctxt) , u, pos)) = |
59739 | 254 |
case do_match ft of |
255 |
NONE => |
|
256 |
(case match_argT T u tyenv of |
|
257 |
NONE => NONE |
|
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
258 |
| SOME tyenv' => desc Ts (ft_abs ctxt (NONE, T) ((tyenv', u_ctxt), u, pos))) |
59739 | 259 |
| SOME ft => SOME ft |
260 |
in desc eta_expands ft end |
|
261 |
||
60052
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset
|
262 |
fun move_assms ctxt (ft: focusterm) = |
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset
|
263 |
let |
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset
|
264 |
fun f () = case try (ft_assm ctxt) ft of |
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset
|
265 |
NONE => NONE |
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset
|
266 |
| SOME ft' => SOME (ft', move_assms ctxt (ft_imp ctxt ft)) |
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset
|
267 |
in Seq.make f end |
59739 | 268 |
|
269 |
fun apply_pat At = Seq.map (ft_judgment ctxt) |
|
270 |
| apply_pat In = Seq.maps (valid_match_points ctxt) |
|
60052
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset
|
271 |
| apply_pat Asm = Seq.maps (move_assms ctxt o ft_params ctxt) |
59739 | 272 |
| apply_pat Concl = Seq.map (ft_concl ctxt o ft_params ctxt) |
273 |
| apply_pat (For idents) = Seq.map_filter ((ft_for ctxt (map (apfst SOME) idents))) |
|
274 |
| apply_pat (Term x) = Seq.map_filter ( (move_term ctxt x)) |
|
275 |
||
276 |
fun apply_pats ft = ft |
|
277 |
|> Seq.single |
|
278 |
|> fold apply_pat pattern_list |
|
279 |
in |
|
280 |
apply_pats |
|
281 |
end |
|
282 |
||
283 |
fun instantiate_normalize_env ctxt env thm = |
|
284 |
let |
|
285 |
fun certs f = map (apply2 (f ctxt)) |
|
286 |
val prop = Thm.prop_of thm |
|
287 |
val norm_type = Envir.norm_type o Envir.type_env |
|
288 |
val insts = Term.add_vars prop [] |
|
289 |
|> map (fn x as (s,T) => (Var (s, norm_type env T), Envir.norm_term env (Var x))) |
|
290 |
|> certs Thm.cterm_of |
|
291 |
val tyinsts = Term.add_tvars prop [] |
|
292 |
|> map (fn x => (TVar x, norm_type env (TVar x))) |
|
293 |
|> certs Thm.ctyp_of |
|
294 |
in Drule.instantiate_normalize (tyinsts, insts) thm end |
|
295 |
||
296 |
fun unify_with_rhs context to env thm = |
|
297 |
let |
|
298 |
val (_, rhs) = thm |> Thm.concl_of |> Logic.dest_equals |
|
299 |
val env' = Pattern.unify context (Logic.mk_term to, Logic.mk_term rhs) env |
|
300 |
handle Pattern.Unif => raise NO_TO_MATCH |
|
301 |
in env' end |
|
302 |
||
303 |
fun inst_thm_to _ (NONE, _) thm = thm |
|
304 |
| inst_thm_to (ctxt : Proof.context) (SOME to, env) thm = |
|
305 |
instantiate_normalize_env ctxt (unify_with_rhs (Context.Proof ctxt) to env thm) thm |
|
306 |
||
307 |
fun inst_thm ctxt idents (to, tyenv) thm = |
|
308 |
let |
|
309 |
(* Replace any identifiers with their corresponding bound variables. *) |
|
310 |
val maxidx = Term.maxidx_typs (map (snd o snd) (Vartab.dest tyenv)) 0 |
|
311 |
val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv = tyenv} |
|
312 |
val replace_idents = |
|
313 |
let |
|
314 |
fun subst ((n1, s)::ss) (t as Free (n2, _)) = if n1 = n2 then s else subst ss t |
|
315 |
| subst _ t = t |
|
316 |
in Term.map_aterms (subst idents) end |
|
317 |
||
60051 | 318 |
val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (the_list to) |
59739 | 319 |
val thm' = Thm.incr_indexes (maxidx + 1) thm |
320 |
in SOME (inst_thm_to ctxt (Option.map replace_idents to, env) thm') end |
|
321 |
handle NO_TO_MATCH => NONE |
|
322 |
||
60079 | 323 |
local |
324 |
||
325 |
fun rewrite_raw ctxt (pattern, to) thms ct = |
|
59739 | 326 |
let |
60079 | 327 |
fun interpret_term_patterns ctxt = |
328 |
let |
|
329 |
||
330 |
fun descend_hole fixes (Abs (_, _, t)) = |
|
331 |
(case descend_hole fixes t of |
|
332 |
NONE => NONE |
|
333 |
| SOME (fix :: fixes', pos) => SOME (fixes', pos o ft_abs ctxt (apfst SOME fix)) |
|
334 |
| SOME ([], _) => raise Match (* XXX -- check phases modified binding *)) |
|
335 |
| descend_hole fixes (t as l $ r) = |
|
336 |
let val (f, _) = strip_comb t |
|
337 |
in |
|
338 |
if is_hole f |
|
339 |
then SOME (fixes, I) |
|
340 |
else |
|
341 |
(case descend_hole fixes l of |
|
342 |
SOME (fixes', pos) => SOME (fixes', pos o ft_fun ctxt) |
|
343 |
| NONE => |
|
344 |
(case descend_hole fixes r of |
|
345 |
SOME (fixes', pos) => SOME (fixes', pos o ft_arg ctxt) |
|
346 |
| NONE => NONE)) |
|
347 |
end |
|
348 |
| descend_hole fixes t = |
|
349 |
if is_hole t then SOME (fixes, I) else NONE |
|
350 |
||
351 |
fun f (t, fixes) = Term (t, (descend_hole (rev fixes) #> the_default ([], I) #> snd) t) |
|
352 |
||
353 |
in map (map_term_pattern f) end |
|
354 |
||
355 |
val pattern' = interpret_term_patterns ctxt pattern |
|
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
356 |
val matches = find_matches ctxt pattern' ((Vartab.empty, ctxt), Thm.term_of ct, I) |
60079 | 357 |
|
358 |
val thms' = maps (prep_meta_eq ctxt) thms |
|
59739 | 359 |
|
360 |
fun rewrite_conv insty ctxt bounds = |
|
60079 | 361 |
CConv.rewrs_cconv (map_filter (inst_thm ctxt bounds insty) thms') |
59739 | 362 |
|
363 |
fun distinct_prems th = |
|
364 |
case Seq.pull (distinct_subgoals_tac th) of |
|
365 |
NONE => th |
|
366 |
| SOME (th', _) => th' |
|
367 |
||
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
368 |
fun conv (((tyenv, _), _, position) : focusterm) = |
60079 | 369 |
distinct_prems o position (rewrite_conv (to, tyenv)) ctxt [] |
370 |
||
371 |
in Seq.map (fn ft => conv ft) matches end |
|
372 |
||
373 |
in |
|
374 |
||
375 |
fun rewrite ctxt pat thms ct = |
|
376 |
rewrite_raw ctxt pat thms ct |> Seq.map_filter (fn cv => try cv ct) |
|
59739 | 377 |
|
60079 | 378 |
fun rewrite_export_tac ctxt (pat, pat_ctxt) thms = |
59739 | 379 |
let |
60079 | 380 |
val export = case pat_ctxt of |
381 |
NONE => I |
|
382 |
| SOME inner => singleton (Proof_Context.export inner ctxt) |
|
383 |
val tac = CSUBGOAL (fn (ct, i) => |
|
384 |
rewrite_raw ctxt pat thms ct |
|
385 |
|> Seq.map (fn cv => CCONVERSION (export o cv) i) |
|
386 |
|> SEQ_CONCAT) |
|
59739 | 387 |
in tac end |
388 |
||
60079 | 389 |
fun rewrite_tac ctxt pat = rewrite_export_tac ctxt (pat, NONE) |
390 |
||
391 |
end |
|
392 |
||
59975 | 393 |
val _ = |
394 |
Theory.setup |
|
59739 | 395 |
let |
396 |
fun mk_fix s = (Binding.name s, NONE, NoSyn) |
|
397 |
||
398 |
val raw_pattern : (string, binding * string option * mixfix) pattern list parser = |
|
399 |
let |
|
400 |
val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In) |
|
401 |
val atom = (Args.$$$ "asm" >> K Asm) || |
|
402 |
(Args.$$$ "concl" >> K Concl) || |
|
403 |
(Args.$$$ "for" |-- Args.parens (Scan.optional Parse.fixes []) >> For) || |
|
404 |
(Parse.term >> Term) |
|
405 |
val sep_atom = sep -- atom >> (fn (s,a) => [s,a]) |
|
406 |
||
407 |
fun append_default [] = [Concl, In] |
|
408 |
| append_default (ps as Term _ :: _) = Concl :: In :: ps |
|
409 |
| append_default ps = ps |
|
410 |
||
411 |
in Scan.repeat sep_atom >> (flat #> rev #> append_default) end |
|
412 |
||
59975 | 413 |
fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) => |
59739 | 414 |
let |
415 |
val (r, toks') = scan toks |
|
59975 | 416 |
val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context |
417 |
in (r', (context', toks' : Token.T list)) end |
|
59739 | 418 |
|
419 |
fun read_fixes fixes ctxt = |
|
420 |
let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx) |
|
421 |
in Proof_Context.add_fixes (map read_typ fixes) ctxt end |
|
422 |
||
423 |
fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) = |
|
424 |
let |
|
425 |
fun add_constrs ctxt n (Abs (x, T, t)) = |
|
426 |
let |
|
427 |
val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt |
|
428 |
in |
|
429 |
(case add_constrs ctxt' (n+1) t of |
|
430 |
NONE => NONE |
|
431 |
| SOME ((ctxt'', n', xs), t') => |
|
432 |
let |
|
433 |
val U = Type_Infer.mk_param n [] |
|
434 |
val u = Type.constraint (U --> dummyT) (Abs (x, T, t')) |
|
435 |
in SOME ((ctxt'', n', (x', U) :: xs), u) end) |
|
436 |
end |
|
437 |
| add_constrs ctxt n (l $ r) = |
|
438 |
(case add_constrs ctxt n l of |
|
439 |
SOME (c, l') => SOME (c, l' $ r) |
|
440 |
| NONE => |
|
441 |
(case add_constrs ctxt n r of |
|
442 |
SOME (c, r') => SOME (c, l $ r') |
|
443 |
| NONE => NONE)) |
|
444 |
| add_constrs ctxt n t = |
|
445 |
if is_hole_const t then SOME ((ctxt, n, []), t) else NONE |
|
446 |
||
447 |
fun prep (Term s) (n, ctxt) = |
|
448 |
let |
|
449 |
val t = Syntax.parse_term ctxt s |
|
450 |
val ((ctxt', n', bs), t') = |
|
451 |
the_default ((ctxt, n, []), t) (add_constrs ctxt (n+1) t) |
|
452 |
in (Term (t', bs), (n', ctxt')) end |
|
453 |
| prep (For ss) (n, ctxt) = |
|
454 |
let val (ns, ctxt') = read_fixes ss ctxt |
|
455 |
in (For ns, (n, ctxt')) end |
|
456 |
| prep At (n,ctxt) = (At, (n, ctxt)) |
|
457 |
| prep In (n,ctxt) = (In, (n, ctxt)) |
|
458 |
| prep Concl (n,ctxt) = (Concl, (n, ctxt)) |
|
459 |
| prep Asm (n,ctxt) = (Asm, (n, ctxt)) |
|
460 |
||
461 |
val (xs, (_, ctxt')) = fold_map prep ps (0, ctxt) |
|
462 |
||
463 |
in (xs, ctxt') end |
|
464 |
||
465 |
fun prep_args ctxt (((raw_pats, raw_to), raw_ths)) = |
|
466 |
let |
|
467 |
||
468 |
fun check_terms ctxt ps to = |
|
469 |
let |
|
470 |
fun safe_chop (0: int) xs = ([], xs) |
|
471 |
| safe_chop n (x :: xs) = chop (n - 1) xs |>> cons x |
|
472 |
| safe_chop _ _ = raise Match |
|
473 |
||
474 |
fun reinsert_pat _ (Term (_, cs)) (t :: ts) = |
|
475 |
let val (cs', ts') = safe_chop (length cs) ts |
|
476 |
in (Term (t, map dest_Free cs'), ts') end |
|
477 |
| reinsert_pat _ (Term _) [] = raise Match |
|
478 |
| reinsert_pat ctxt (For ss) ts = |
|
479 |
let val fixes = map (fn s => (s, Variable.default_type ctxt s)) ss |
|
480 |
in (For fixes, ts) end |
|
481 |
| reinsert_pat _ At ts = (At, ts) |
|
482 |
| reinsert_pat _ In ts = (In, ts) |
|
483 |
| reinsert_pat _ Concl ts = (Concl, ts) |
|
484 |
| reinsert_pat _ Asm ts = (Asm, ts) |
|
485 |
||
486 |
fun free_constr (s,T) = Type.constraint T (Free (s, dummyT)) |
|
487 |
fun mk_free_constrs (Term (t, cs)) = t :: map free_constr cs |
|
488 |
| mk_free_constrs _ = [] |
|
489 |
||
60051 | 490 |
val ts = maps mk_free_constrs ps @ the_list to |
59739 | 491 |
|> Syntax.check_terms (hole_syntax ctxt) |
492 |
val ctxt' = fold Variable.declare_term ts ctxt |
|
493 |
val (ps', (to', ts')) = fold_map (reinsert_pat ctxt') ps ts |
|
494 |
||> (fn xs => case to of NONE => (NONE, xs) | SOME _ => (SOME (hd xs), tl xs)) |
|
495 |
val _ = case ts' of (_ :: _) => raise Match | [] => () |
|
496 |
in ((ps', to'), ctxt') end |
|
497 |
||
498 |
val (pats, ctxt') = prep_pats ctxt raw_pats |
|
499 |
||
500 |
val ths = Attrib.eval_thms ctxt' raw_ths |
|
501 |
val to = Option.map (Syntax.parse_term ctxt') raw_to |
|
502 |
||
503 |
val ((pats', to'), ctxt'') = check_terms ctxt' pats to |
|
504 |
||
60079 | 505 |
in ((pats', ths, (to', ctxt)), ctxt'') end |
59739 | 506 |
|
507 |
val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term) |
|
508 |
||
509 |
val subst_parser = |
|
510 |
let val scan = raw_pattern -- to_parser -- Parse.xthms1 |
|
59975 | 511 |
in context_lift scan prep_args end |
59739 | 512 |
in |
513 |
Method.setup @{binding rewrite} (subst_parser >> |
|
60079 | 514 |
(fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => |
515 |
SIMPLE_METHOD' (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms))) |
|
59739 | 516 |
"single-step rewriting, allowing subterm selection via patterns." |
517 |
end |
|
518 |
end |