author | desharna |
Mon, 06 Oct 2014 13:40:31 +0200 | |
changeset 58583 | 1dd83cbba636 |
parent 58461 | 75ee8d49c724 |
child 58634 | 9f10d82e8188 |
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 |
||
9 |
structure BNF_LFP_Rec_Sugar_More : sig end = |
|
10 |
struct |
|
11 |
||
12 |
open BNF_Util |
|
13 |
open BNF_Def |
|
14 |
open BNF_FP_Util |
|
15 |
open BNF_FP_Def_Sugar |
|
16 |
open BNF_FP_N2M_Sugar |
|
17 |
open BNF_LFP_Rec_Sugar |
|
18 |
||
58389 | 19 |
(* FIXME: remove "nat" cases throughout once it is registered as a datatype *) |
20 |
||
57993 | 21 |
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
|
22 |
|
58389 | 23 |
fun is_new_datatype _ @{type_name nat} = true |
24 |
| is_new_datatype ctxt s = |
|
25 |
(case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false); |
|
55571 | 26 |
|
58461 | 27 |
fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, fp_ctr_sugar = {ctr_sugar, ...}, |
28 |
fp_co_induct_sugar = {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) = |
|
58388 | 29 |
{T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar, |
30 |
recx = recx, rec_thms = rec_thms}; |
|
55571 | 31 |
|
58389 | 32 |
fun basic_lfp_sugars_of _ [@{typ nat}] _ _ lthy = |
33 |
([], [0], [nat_basic_lfp_sugar], [], [], TrueI (*dummy*), [], false, lthy) |
|
34 |
| basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 = |
|
35 |
let |
|
36 |
val ((missing_arg_Ts, perm0_kks, |
|
58461 | 37 |
fp_sugars as {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _, |
58389 | 38 |
(lfp_sugar_thms, _)), lthy) = |
39 |
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
|
40 |
|
58389 | 41 |
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
|
42 |
|
58389 | 43 |
val Ts = map #T fp_sugars; |
44 |
val Xs = map #X fp_sugars; |
|
58461 | 45 |
val Cs = map (body_type o fastype_of o #co_rec o #fp_co_induct_sugar) fp_sugars; |
58389 | 46 |
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
|
47 |
|
58389 | 48 |
fun zip_XrecT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_XrecT) Us)] |
49 |
| zip_XrecT U = |
|
50 |
(case AList.lookup (op =) Xs_TCs U of |
|
51 |
SOME (T, C) => [T, C] |
|
52 |
| NONE => [U]); |
|
55574
4a940ebceef8
rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents:
55571
diff
changeset
|
53 |
|
58460 | 54 |
val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) fp_sugars; |
58389 | 55 |
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
|
56 |
|
58389 | 57 |
val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs; |
58 |
val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs; |
|
59 |
in |
|
60 |
(missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars, |
|
61 |
fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, induct_attrs, |
|
62 |
is_some lfp_sugar_thms, lthy) |
|
63 |
end; |
|
55571 | 64 |
|
58387 | 65 |
exception NO_MAP of term; |
55571 | 66 |
|
67 |
fun ill_formed_rec_call ctxt t = |
|
68 |
error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
|
69 |
fun invalid_map ctxt t = |
|
70 |
error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t)); |
|
71 |
fun unexpected_rec_call ctxt t = |
|
72 |
error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
|
73 |
||
74 |
fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' = |
|
75 |
let |
|
76 |
fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else (); |
|
77 |
||
78 |
val typof = curry fastype_of1 bound_Ts; |
|
57303 | 79 |
val build_map_fst = build_map ctxt [] (fst_const o fst); |
55571 | 80 |
|
81 |
val yT = typof y; |
|
82 |
val yU = typof y'; |
|
83 |
||
84 |
fun y_of_y' () = build_map_fst (yU, yT) $ y'; |
|
85 |
val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t); |
|
86 |
||
87 |
fun massage_mutual_fun U T t = |
|
88 |
(case t of |
|
89 |
Const (@{const_name comp}, _) $ t1 $ t2 => |
|
90 |
mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2) |
|
91 |
| _ => |
|
92 |
if has_call t then |
|
93 |
(case try HOLogic.dest_prodT U of |
|
94 |
SOME (U1, U2) => if U1 = T then raw_massage_fun T U2 t else invalid_map ctxt t |
|
95 |
| NONE => invalid_map ctxt t) |
|
96 |
else |
|
97 |
mk_comp bound_Ts (t, build_map_fst (U, T))); |
|
98 |
||
99 |
fun massage_map (Type (_, Us)) (Type (s, Ts)) t = |
|
100 |
(case try (dest_map ctxt s) t of |
|
101 |
SOME (map0, fs) => |
|
102 |
let |
|
103 |
val Type (_, ran_Ts) = range_type (typof t); |
|
104 |
val map' = mk_map (length fs) Us ran_Ts map0; |
|
105 |
val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs; |
|
106 |
in |
|
107 |
Term.list_comb (map', fs') |
|
108 |
end |
|
58387 | 109 |
| NONE => raise NO_MAP t) |
110 |
| massage_map _ _ t = raise NO_MAP t |
|
55571 | 111 |
and massage_map_or_map_arg U T t = |
112 |
if T = U then |
|
113 |
tap check_no_call t |
|
114 |
else |
|
115 |
massage_map U T t |
|
58387 | 116 |
handle NO_MAP _ => massage_mutual_fun U T t; |
55571 | 117 |
|
118 |
fun massage_call (t as t1 $ t2) = |
|
119 |
if has_call t then |
|
120 |
if t2 = y then |
|
121 |
massage_map yU yT (elim_y t1) $ y' |
|
58387 | 122 |
handle NO_MAP t' => invalid_map ctxt t' |
55571 | 123 |
else |
124 |
let val (g, xs) = Term.strip_comb t2 in |
|
125 |
if g = y then |
|
126 |
if exists has_call xs then unexpected_rec_call ctxt t2 |
|
127 |
else Term.list_comb (massage_call (mk_compN (length xs) bound_Ts (t1, y)), xs) |
|
128 |
else |
|
129 |
ill_formed_rec_call ctxt t |
|
130 |
end |
|
131 |
else |
|
132 |
elim_y t |
|
133 |
| massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t; |
|
134 |
in |
|
135 |
massage_call |
|
136 |
end; |
|
137 |
||
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
138 |
fun rewrite_map_arg get_ctr_pos rec_type res_type = |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
139 |
let |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
140 |
val pT = HOLogic.mk_prodT (rec_type, res_type); |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
141 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
142 |
fun subst d (t as Bound d') = t |> d = SOME d' ? curry (op $) (fst_const pT) |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
143 |
| subst d (Abs (v, T, b)) = |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
144 |
Abs (v, if d = SOME ~1 then pT else T, subst (Option.map (Integer.add 1) d) b) |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
145 |
| subst d t = |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
146 |
let |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
147 |
val (u, vs) = strip_comb t; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
148 |
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
|
149 |
in |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
150 |
if ctr_pos >= 0 then |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
151 |
if d = SOME ~1 andalso length vs = ctr_pos then |
56638 | 152 |
Term.list_comb (permute_args ctr_pos (snd_const pT), vs) |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
153 |
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
|
154 |
d = try (fn Bound n => n) (nth vs ctr_pos) then |
56638 | 155 |
Term.list_comb (snd_const pT $ 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
|
156 |
else |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
157 |
raise PRIMREC ("recursive call not directly applied to constructor argument", [t]) |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
158 |
else |
56638 | 159 |
Term.list_comb (u, map (subst (d |> d = SOME ~1 ? K NONE)) vs) |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
160 |
end |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
161 |
in |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
162 |
subst (SOME ~1) |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
163 |
end; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
164 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
165 |
fun rewrite_nested_rec_call ctxt has_call get_ctr_pos = |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
166 |
massage_nested_rec_call ctxt has_call (rewrite_map_arg get_ctr_pos); |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
167 |
|
55571 | 168 |
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
|
169 |
{nested_simps = nested_simps, is_new_datatype = is_new_datatype, |
58389 | 170 |
basic_lfp_sugars_of = basic_lfp_sugars_of, |
171 |
rewrite_nested_rec_call = SOME rewrite_nested_rec_call}); |
|
55571 | 172 |
|
173 |
end; |