author | blanchet |
Fri, 30 Dec 2016 15:40:35 +0100 | |
changeset 64705 | 7596b0736ab9 |
parent 64627 | 8d7cb22482e3 |
child 66290 | 88714f2e40e8 |
permissions | -rw-r--r-- |
55571 | 1 |
(* Title: HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML |
2 |
Author: Lorenz Panny, TU Muenchen |
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
|
4 |
Copyright 2013 |
|
5 |
||
58315 | 6 |
More recursor sugar. |
55571 | 7 |
*) |
8 |
||
60000 | 9 |
signature BNF_LFP_REC_SUGAR_MORE = |
10 |
sig |
|
11 |
val massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) -> |
|
60002 | 12 |
(typ * typ -> term) -> typ list -> term -> term -> term -> term |
60000 | 13 |
end; |
14 |
||
15 |
structure BNF_LFP_Rec_Sugar_More : BNF_LFP_REC_SUGAR_MORE = |
|
55571 | 16 |
struct |
17 |
||
18 |
open BNF_Util |
|
19 |
open BNF_Def |
|
20 |
open BNF_FP_Util |
|
21 |
open BNF_FP_Def_Sugar |
|
22 |
open BNF_FP_N2M_Sugar |
|
23 |
open BNF_LFP_Rec_Sugar |
|
24 |
||
58389 | 25 |
(* FIXME: remove "nat" cases throughout once it is registered as a datatype *) |
26 |
||
57993 | 27 |
val nested_simps = @{thms o_def[abs_def] id_def split fst_conv snd_conv}; |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
28 |
|
58389 | 29 |
fun is_new_datatype _ @{type_name nat} = true |
30 |
| is_new_datatype ctxt s = |
|
63859
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
62326
diff
changeset
|
31 |
(case fp_sugar_of ctxt s of |
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
62326
diff
changeset
|
32 |
SOME {fp = Least_FP, fp_co_induct_sugar = SOME _, ...} => true |
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
62326
diff
changeset
|
33 |
| _ => false); |
55571 | 34 |
|
58461 | 35 |
fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, fp_ctr_sugar = {ctr_sugar, ...}, |
63859
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
62326
diff
changeset
|
36 |
fp_co_induct_sugar = SOME {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) = |
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
62326
diff
changeset
|
37 |
{T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar, |
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
62326
diff
changeset
|
38 |
recx = recx, rec_thms = rec_thms}; |
55571 | 39 |
|
58389 | 40 |
fun basic_lfp_sugars_of _ [@{typ nat}] _ _ lthy = |
62326
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
41 |
([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, lthy) |
58389 | 42 |
| basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 = |
43 |
let |
|
44 |
val ((missing_arg_Ts, perm0_kks, |
|
61760 | 45 |
fp_sugars as {fp_nesting_bnfs, |
63859
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
62326
diff
changeset
|
46 |
fp_co_induct_sugar = SOME {common_co_inducts = [common_induct], ...}, ...} :: _, |
58389 | 47 |
(lfp_sugar_thms, _)), lthy) = |
48 |
nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0; |
|
55574
4a940ebceef8
rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents:
55571
diff
changeset
|
49 |
|
58389 | 50 |
val induct_attrs = (case lfp_sugar_thms of SOME ((_, _, attrs), _) => attrs | NONE => []); |
58283
71d74e641538
preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents:
58131
diff
changeset
|
51 |
|
58389 | 52 |
val Ts = map #T fp_sugars; |
53 |
val Xs = map #X fp_sugars; |
|
63859
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
62326
diff
changeset
|
54 |
val Cs = map (body_type o fastype_of o #co_rec o the o #fp_co_induct_sugar) fp_sugars; |
58389 | 55 |
val Xs_TCs = Xs ~~ (Ts ~~ Cs); |
55574
4a940ebceef8
rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents:
55571
diff
changeset
|
56 |
|
58389 | 57 |
fun zip_XrecT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_XrecT) Us)] |
58 |
| zip_XrecT U = |
|
59 |
(case AList.lookup (op =) Xs_TCs U of |
|
60 |
SOME (T, C) => [T, C] |
|
61 |
| NONE => [U]); |
|
55574
4a940ebceef8
rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents:
55571
diff
changeset
|
62 |
|
58460 | 63 |
val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) fp_sugars; |
58389 | 64 |
val fun_arg_Tssss = map (map (map zip_XrecT)) ctrXs_Tsss; |
55574
4a940ebceef8
rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents:
55571
diff
changeset
|
65 |
|
58389 | 66 |
val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs; |
67 |
val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs; |
|
62326
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
68 |
val fp_nesting_pred_maps = map pred_map_of_bnf fp_nesting_bnfs; |
58389 | 69 |
in |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58461
diff
changeset
|
70 |
(missing_arg_Ts, perm0_kks, @{map 3} basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars, |
62326
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
71 |
fp_nesting_map_ident0s, fp_nesting_map_comps, fp_nesting_pred_maps, common_induct, |
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
72 |
induct_attrs, is_some lfp_sugar_thms, lthy) |
58389 | 73 |
end; |
55571 | 74 |
|
58387 | 75 |
exception NO_MAP of term; |
55571 | 76 |
|
60002 | 77 |
fun massage_nested_rec_call ctxt has_call massage_fun massage_nonfun bound_Ts y y' t0 = |
55571 | 78 |
let |
64705
7596b0736ab9
more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents:
64627
diff
changeset
|
79 |
fun check_no_call t = if has_call t then unexpected_rec_call_in ctxt [t0] t else (); |
55571 | 80 |
|
81 |
val typof = curry fastype_of1 bound_Ts; |
|
64627
8d7cb22482e3
generalized ML function (towards nonuniform datatypes)
blanchet
parents:
63859
diff
changeset
|
82 |
val massage_no_call = build_map ctxt [] [] massage_nonfun; |
55571 | 83 |
|
84 |
val yT = typof y; |
|
85 |
val yU = typof y'; |
|
86 |
||
60002 | 87 |
fun y_of_y' () = massage_no_call (yU, yT) $ y'; |
55571 | 88 |
val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t); |
89 |
||
90 |
fun massage_mutual_fun U T t = |
|
91 |
(case t of |
|
92 |
Const (@{const_name comp}, _) $ t1 $ t2 => |
|
93 |
mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2) |
|
94 |
| _ => |
|
60002 | 95 |
if has_call t then massage_fun U T t else mk_comp bound_Ts (t, massage_no_call (U, T))); |
55571 | 96 |
|
97 |
fun massage_map (Type (_, Us)) (Type (s, Ts)) t = |
|
98 |
(case try (dest_map ctxt s) t of |
|
99 |
SOME (map0, fs) => |
|
100 |
let |
|
101 |
val Type (_, ran_Ts) = range_type (typof t); |
|
102 |
val map' = mk_map (length fs) Us ran_Ts map0; |
|
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58461
diff
changeset
|
103 |
val fs' = map_flattened_map_args ctxt s (@{map 3} massage_map_or_map_arg Us Ts) fs; |
55571 | 104 |
in |
105 |
Term.list_comb (map', fs') |
|
106 |
end |
|
62326
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
107 |
| NONE => |
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
108 |
(case try (dest_pred ctxt s) t of |
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
109 |
SOME (pred0, fs) => |
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
110 |
let |
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
111 |
val pred' = mk_pred Us pred0; |
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
112 |
val fs' = map_flattened_map_args ctxt s (@{map 3} massage_map_or_map_arg Us Ts) fs; |
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
113 |
in |
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
114 |
Term.list_comb (pred', fs') |
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
115 |
end |
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
61760
diff
changeset
|
116 |
| NONE => raise NO_MAP t)) |
58387 | 117 |
| massage_map _ _ t = raise NO_MAP t |
55571 | 118 |
and massage_map_or_map_arg U T t = |
119 |
if T = U then |
|
120 |
tap check_no_call t |
|
121 |
else |
|
122 |
massage_map U T t |
|
58387 | 123 |
handle NO_MAP _ => massage_mutual_fun U T t; |
55571 | 124 |
|
60001 | 125 |
fun massage_outer_call (t as t1 $ t2) = |
55571 | 126 |
if has_call t then |
127 |
if t2 = y then |
|
128 |
massage_map yU yT (elim_y t1) $ y' |
|
64705
7596b0736ab9
more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents:
64627
diff
changeset
|
129 |
handle NO_MAP t' => invalid_map ctxt [t0] t' |
55571 | 130 |
else |
131 |
let val (g, xs) = Term.strip_comb t2 in |
|
132 |
if g = y then |
|
64705
7596b0736ab9
more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents:
64627
diff
changeset
|
133 |
if exists has_call xs then unexpected_rec_call_in ctxt [t0] t2 |
60001 | 134 |
else Term.list_comb (massage_outer_call (mk_compN (length xs) bound_Ts (t1, y)), xs) |
55571 | 135 |
else |
136 |
ill_formed_rec_call ctxt t |
|
137 |
end |
|
138 |
else |
|
139 |
elim_y t |
|
60001 | 140 |
| massage_outer_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t; |
55571 | 141 |
in |
60001 | 142 |
massage_outer_call t0 |
55571 | 143 |
end; |
144 |
||
60001 | 145 |
fun rewrite_map_fun ctxt get_ctr_pos U T t = |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
146 |
let |
60001 | 147 |
val _ = |
148 |
(case try HOLogic.dest_prodT U of |
|
64705
7596b0736ab9
more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents:
64627
diff
changeset
|
149 |
SOME (U1, _) => U1 = T orelse invalid_map ctxt [] t |
7596b0736ab9
more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents:
64627
diff
changeset
|
150 |
| NONE => invalid_map ctxt [] t); |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
151 |
|
60001 | 152 |
fun subst d (t as Bound d') = t |> d = SOME d' ? curry (op $) (fst_const U) |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
153 |
| subst d (Abs (v, T, b)) = |
60001 | 154 |
Abs (v, if d = SOME ~1 then U else T, subst (Option.map (Integer.add 1) d) b) |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
155 |
| subst d t = |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
156 |
let |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
157 |
val (u, vs) = strip_comb t; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
158 |
val ctr_pos = try (get_ctr_pos o fst o dest_Free) u |> the_default ~1; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
159 |
in |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
160 |
if ctr_pos >= 0 then |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
161 |
if d = SOME ~1 andalso length vs = ctr_pos then |
60001 | 162 |
Term.list_comb (permute_args ctr_pos (snd_const U), vs) |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
163 |
else if length vs > ctr_pos andalso is_some d andalso |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
164 |
d = try (fn Bound n => n) (nth vs ctr_pos) then |
60001 | 165 |
Term.list_comb (snd_const U $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs)) |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
166 |
else |
64705
7596b0736ab9
more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents:
64627
diff
changeset
|
167 |
rec_call_not_apply_to_ctr_arg ctxt [] t |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
168 |
else |
60001 | 169 |
Term.list_comb (u, map (subst (if d = SOME ~1 then NONE else d)) vs) |
170 |
end; |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
171 |
in |
60001 | 172 |
subst (SOME ~1) t |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
173 |
end; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
174 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
175 |
fun rewrite_nested_rec_call ctxt has_call get_ctr_pos = |
60002 | 176 |
massage_nested_rec_call ctxt has_call (rewrite_map_fun ctxt get_ctr_pos) (fst_const o fst); |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
177 |
|
55571 | 178 |
val _ = Theory.setup (register_lfp_rec_extension |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
179 |
{nested_simps = nested_simps, is_new_datatype = is_new_datatype, |
58389 | 180 |
basic_lfp_sugars_of = basic_lfp_sugars_of, |
181 |
rewrite_nested_rec_call = SOME rewrite_nested_rec_call}); |
|
55571 | 182 |
|
183 |
end; |