author | blanchet |
Fri, 10 Apr 2015 14:03:18 +0200 | |
changeset 60001 | 0e1b220ec4c9 |
parent 60000 | b0816837ef4b |
child 60002 | 50cf9e0ae818 |
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) -> |
|
12 |
typ list -> term -> term -> term -> term |
|
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 = |
|
31 |
(case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false); |
|
55571 | 32 |
|
58461 | 33 |
fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, fp_ctr_sugar = {ctr_sugar, ...}, |
34 |
fp_co_induct_sugar = {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) = |
|
58388 | 35 |
{T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar, |
36 |
recx = recx, rec_thms = rec_thms}; |
|
55571 | 37 |
|
58389 | 38 |
fun basic_lfp_sugars_of _ [@{typ nat}] _ _ lthy = |
39 |
([], [0], [nat_basic_lfp_sugar], [], [], TrueI (*dummy*), [], false, lthy) |
|
40 |
| basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 = |
|
41 |
let |
|
42 |
val ((missing_arg_Ts, perm0_kks, |
|
58461 | 43 |
fp_sugars as {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _, |
58389 | 44 |
(lfp_sugar_thms, _)), lthy) = |
45 |
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
|
46 |
|
58389 | 47 |
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
|
48 |
|
58389 | 49 |
val Ts = map #T fp_sugars; |
50 |
val Xs = map #X fp_sugars; |
|
58461 | 51 |
val Cs = map (body_type o fastype_of o #co_rec o #fp_co_induct_sugar) fp_sugars; |
58389 | 52 |
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
|
53 |
|
58389 | 54 |
fun zip_XrecT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_XrecT) Us)] |
55 |
| zip_XrecT U = |
|
56 |
(case AList.lookup (op =) Xs_TCs U of |
|
57 |
SOME (T, C) => [T, C] |
|
58 |
| NONE => [U]); |
|
55574
4a940ebceef8
rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents:
55571
diff
changeset
|
59 |
|
58460 | 60 |
val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) fp_sugars; |
58389 | 61 |
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
|
62 |
|
58389 | 63 |
val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs; |
64 |
val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs; |
|
65 |
in |
|
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58461
diff
changeset
|
66 |
(missing_arg_Ts, perm0_kks, @{map 3} basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars, |
58389 | 67 |
fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, induct_attrs, |
68 |
is_some lfp_sugar_thms, lthy) |
|
69 |
end; |
|
55571 | 70 |
|
58387 | 71 |
exception NO_MAP of term; |
55571 | 72 |
|
73 |
fun ill_formed_rec_call ctxt t = |
|
74 |
error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
|
75 |
fun invalid_map ctxt t = |
|
76 |
error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t)); |
|
60001 | 77 |
fun unexpected_rec_call ctxt eqns t = |
78 |
error_at ctxt eqns ("Unexpected recursive call in " ^ quote (Syntax.string_of_term ctxt t)); |
|
55571 | 79 |
|
60001 | 80 |
fun massage_nested_rec_call ctxt has_call massage_fun bound_Ts y y' t0 = |
55571 | 81 |
let |
60001 | 82 |
fun check_no_call t = if has_call t then unexpected_rec_call ctxt [t0] t else (); |
55571 | 83 |
|
84 |
val typof = curry fastype_of1 bound_Ts; |
|
57303 | 85 |
val build_map_fst = build_map ctxt [] (fst_const o fst); |
55571 | 86 |
|
87 |
val yT = typof y; |
|
88 |
val yU = typof y'; |
|
89 |
||
90 |
fun y_of_y' () = build_map_fst (yU, yT) $ y'; |
|
91 |
val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t); |
|
92 |
||
93 |
fun massage_mutual_fun U T t = |
|
94 |
(case t of |
|
95 |
Const (@{const_name comp}, _) $ t1 $ t2 => |
|
96 |
mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2) |
|
97 |
| _ => |
|
60001 | 98 |
if has_call t then massage_fun U T t else mk_comp bound_Ts (t, build_map_fst (U, T))); |
55571 | 99 |
|
100 |
fun massage_map (Type (_, Us)) (Type (s, Ts)) t = |
|
101 |
(case try (dest_map ctxt s) t of |
|
102 |
SOME (map0, fs) => |
|
103 |
let |
|
104 |
val Type (_, ran_Ts) = range_type (typof t); |
|
105 |
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
|
106 |
val fs' = map_flattened_map_args ctxt s (@{map 3} massage_map_or_map_arg Us Ts) fs; |
55571 | 107 |
in |
108 |
Term.list_comb (map', fs') |
|
109 |
end |
|
58387 | 110 |
| NONE => raise NO_MAP t) |
111 |
| massage_map _ _ t = raise NO_MAP t |
|
55571 | 112 |
and massage_map_or_map_arg U T t = |
113 |
if T = U then |
|
114 |
tap check_no_call t |
|
115 |
else |
|
116 |
massage_map U T t |
|
58387 | 117 |
handle NO_MAP _ => massage_mutual_fun U T t; |
55571 | 118 |
|
60001 | 119 |
fun massage_outer_call (t as t1 $ t2) = |
55571 | 120 |
if has_call t then |
121 |
if t2 = y then |
|
122 |
massage_map yU yT (elim_y t1) $ y' |
|
58387 | 123 |
handle NO_MAP t' => invalid_map ctxt t' |
55571 | 124 |
else |
125 |
let val (g, xs) = Term.strip_comb t2 in |
|
126 |
if g = y then |
|
60001 | 127 |
if exists has_call xs then unexpected_rec_call ctxt [t0] t2 |
128 |
else Term.list_comb (massage_outer_call (mk_compN (length xs) bound_Ts (t1, y)), xs) |
|
55571 | 129 |
else |
130 |
ill_formed_rec_call ctxt t |
|
131 |
end |
|
132 |
else |
|
133 |
elim_y t |
|
60001 | 134 |
| massage_outer_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t; |
55571 | 135 |
in |
60001 | 136 |
massage_outer_call t0 |
55571 | 137 |
end; |
138 |
||
60001 | 139 |
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
|
140 |
let |
60001 | 141 |
val _ = |
142 |
(case try HOLogic.dest_prodT U of |
|
143 |
SOME (U1, _) => U1 = T orelse invalid_map ctxt t |
|
144 |
| NONE => invalid_map ctxt t); |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
145 |
|
60001 | 146 |
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
|
147 |
| subst d (Abs (v, T, b)) = |
60001 | 148 |
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
|
149 |
| subst d t = |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
150 |
let |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
151 |
val (u, vs) = strip_comb t; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
152 |
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
|
153 |
in |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
154 |
if ctr_pos >= 0 then |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
155 |
if d = SOME ~1 andalso length vs = ctr_pos then |
60001 | 156 |
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
|
157 |
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
|
158 |
d = try (fn Bound n => n) (nth vs ctr_pos) then |
60001 | 159 |
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
|
160 |
else |
59595 | 161 |
error ("Recursive call not directly applied to constructor argument in " ^ |
162 |
quote (Syntax.string_of_term ctxt t)) |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
163 |
else |
60001 | 164 |
Term.list_comb (u, map (subst (if d = SOME ~1 then NONE else d)) vs) |
165 |
end; |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
166 |
in |
60001 | 167 |
subst (SOME ~1) t |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
168 |
end; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
169 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
170 |
fun rewrite_nested_rec_call ctxt has_call get_ctr_pos = |
60001 | 171 |
massage_nested_rec_call ctxt has_call (rewrite_map_fun ctxt get_ctr_pos); |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
172 |
|
55571 | 173 |
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
|
174 |
{nested_simps = nested_simps, is_new_datatype = is_new_datatype, |
58389 | 175 |
basic_lfp_sugars_of = basic_lfp_sugars_of, |
176 |
rewrite_nested_rec_call = SOME rewrite_nested_rec_call}); |
|
55571 | 177 |
|
178 |
end; |