author | blanchet |
Fri, 27 Jun 2014 10:11:44 +0200 | |
changeset 57399 | cfc19f0a6261 |
parent 57397 | 5004aca20821 |
child 57993 | c52255a71114 |
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 |
||
56638 | 6 |
More new-style 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 |
||
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
19 |
val nested_simps = @{thms id_def split comp_def fst_conv snd_conv}; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
20 |
|
55571 | 21 |
fun is_new_datatype ctxt s = |
22 |
(case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false); |
|
23 |
||
55863 | 24 |
fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_defs, ctr_sugar, co_rec = recx, |
25 |
co_rec_thms = rec_thms, ...} : fp_sugar) = |
|
55574
4a940ebceef8
rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents:
55571
diff
changeset
|
26 |
{T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_defs = ctr_defs, |
55863 | 27 |
ctr_sugar = ctr_sugar, recx = recx, rec_thms = rec_thms}; |
55571 | 28 |
|
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55575
diff
changeset
|
29 |
fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 = |
55571 | 30 |
let |
31 |
val ((missing_arg_Ts, perm0_kks, |
|
57397 | 32 |
fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _, |
56857
aa2de99be748
note correct induction schemes in 'primrec' (for N2M)
blanchet
parents:
56638
diff
changeset
|
33 |
(lfp_sugar_thms, _)), lthy) = |
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55575
diff
changeset
|
34 |
nested_to_mutual_fps 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
|
35 |
|
4a940ebceef8
rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents:
55571
diff
changeset
|
36 |
val Ts = map #T fp_sugars; |
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55575
diff
changeset
|
37 |
val Xs = map #X fp_sugars; |
55863 | 38 |
val Cs = map (body_type o fastype_of o #co_rec) fp_sugars; |
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55575
diff
changeset
|
39 |
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
|
40 |
|
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55575
diff
changeset
|
41 |
fun zip_recT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_recT) Us)] |
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55575
diff
changeset
|
42 |
| zip_recT U = |
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55575
diff
changeset
|
43 |
(case AList.lookup (op =) Xs_TCs U of |
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55575
diff
changeset
|
44 |
SOME (T, C) => [T, C] |
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55575
diff
changeset
|
45 |
| NONE => [U]); |
55574
4a940ebceef8
rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents:
55571
diff
changeset
|
46 |
|
55772
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55575
diff
changeset
|
47 |
val ctrXs_Tsss = map #ctrXs_Tss fp_sugars; |
367ec44763fd
correct most general type for mutual recursion when several identical types are involved
blanchet
parents:
55575
diff
changeset
|
48 |
val fun_arg_Tssss = map (map (map zip_recT)) ctrXs_Tsss; |
55574
4a940ebceef8
rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents:
55571
diff
changeset
|
49 |
|
57399 | 50 |
val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs; |
57397 | 51 |
val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs; |
55571 | 52 |
in |
55574
4a940ebceef8
rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents:
55571
diff
changeset
|
53 |
(missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars, |
57399 | 54 |
fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, is_some lfp_sugar_thms, lthy) |
55571 | 55 |
end; |
56 |
||
57 |
exception NOT_A_MAP of term; |
|
58 |
||
59 |
fun ill_formed_rec_call ctxt t = |
|
60 |
error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
|
61 |
fun invalid_map ctxt t = |
|
62 |
error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t)); |
|
63 |
fun unexpected_rec_call ctxt t = |
|
64 |
error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
|
65 |
||
66 |
fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' = |
|
67 |
let |
|
68 |
fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else (); |
|
69 |
||
70 |
val typof = curry fastype_of1 bound_Ts; |
|
57303 | 71 |
val build_map_fst = build_map ctxt [] (fst_const o fst); |
55571 | 72 |
|
73 |
val yT = typof y; |
|
74 |
val yU = typof y'; |
|
75 |
||
76 |
fun y_of_y' () = build_map_fst (yU, yT) $ y'; |
|
77 |
val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t); |
|
78 |
||
79 |
fun massage_mutual_fun U T t = |
|
80 |
(case t of |
|
81 |
Const (@{const_name comp}, _) $ t1 $ t2 => |
|
82 |
mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2) |
|
83 |
| _ => |
|
84 |
if has_call t then |
|
85 |
(case try HOLogic.dest_prodT U of |
|
86 |
SOME (U1, U2) => if U1 = T then raw_massage_fun T U2 t else invalid_map ctxt t |
|
87 |
| NONE => invalid_map ctxt t) |
|
88 |
else |
|
89 |
mk_comp bound_Ts (t, build_map_fst (U, T))); |
|
90 |
||
91 |
fun massage_map (Type (_, Us)) (Type (s, Ts)) t = |
|
92 |
(case try (dest_map ctxt s) t of |
|
93 |
SOME (map0, fs) => |
|
94 |
let |
|
95 |
val Type (_, ran_Ts) = range_type (typof t); |
|
96 |
val map' = mk_map (length fs) Us ran_Ts map0; |
|
97 |
val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs; |
|
98 |
in |
|
99 |
Term.list_comb (map', fs') |
|
100 |
end |
|
101 |
| NONE => raise NOT_A_MAP t) |
|
102 |
| massage_map _ _ t = raise NOT_A_MAP t |
|
103 |
and massage_map_or_map_arg U T t = |
|
104 |
if T = U then |
|
105 |
tap check_no_call t |
|
106 |
else |
|
107 |
massage_map U T t |
|
108 |
handle NOT_A_MAP _ => massage_mutual_fun U T t; |
|
109 |
||
110 |
fun massage_call (t as t1 $ t2) = |
|
111 |
if has_call t then |
|
112 |
if t2 = y then |
|
113 |
massage_map yU yT (elim_y t1) $ y' |
|
114 |
handle NOT_A_MAP t' => invalid_map ctxt t' |
|
115 |
else |
|
116 |
let val (g, xs) = Term.strip_comb t2 in |
|
117 |
if g = y then |
|
118 |
if exists has_call xs then unexpected_rec_call ctxt t2 |
|
119 |
else Term.list_comb (massage_call (mk_compN (length xs) bound_Ts (t1, y)), xs) |
|
120 |
else |
|
121 |
ill_formed_rec_call ctxt t |
|
122 |
end |
|
123 |
else |
|
124 |
elim_y t |
|
125 |
| massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t; |
|
126 |
in |
|
127 |
massage_call |
|
128 |
end; |
|
129 |
||
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
130 |
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
|
131 |
let |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
132 |
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
|
133 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
134 |
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
|
135 |
| subst d (Abs (v, T, b)) = |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
136 |
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
|
137 |
| subst d t = |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
138 |
let |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
139 |
val (u, vs) = strip_comb t; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
140 |
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
|
141 |
in |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
142 |
if ctr_pos >= 0 then |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
143 |
if d = SOME ~1 andalso length vs = ctr_pos then |
56638 | 144 |
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
|
145 |
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
|
146 |
d = try (fn Bound n => n) (nth vs ctr_pos) then |
56638 | 147 |
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
|
148 |
else |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
149 |
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
|
150 |
else |
56638 | 151 |
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
|
152 |
end |
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 |
subst (SOME ~1) |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
155 |
end; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
156 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
157 |
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
|
158 |
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
|
159 |
|
55571 | 160 |
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
|
161 |
{nested_simps = nested_simps, is_new_datatype = is_new_datatype, |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55574
diff
changeset
|
162 |
get_basic_lfp_sugars = get_basic_lfp_sugars, rewrite_nested_rec_call = rewrite_nested_rec_call}); |
55571 | 163 |
|
164 |
end; |