blanchet@54440
|
1 |
(* Title: HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
|
blanchet@54440
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
blanchet@54440
|
3 |
Copyright 2013
|
blanchet@54440
|
4 |
|
blanchet@54440
|
5 |
Suggared flattening of nested to mutual (co)recursion.
|
blanchet@54440
|
6 |
*)
|
blanchet@54440
|
7 |
|
blanchet@54440
|
8 |
signature BNF_FP_N2M_SUGAR =
|
blanchet@54440
|
9 |
sig
|
blanchet@55695
|
10 |
val unfold_let: term -> term
|
blanchet@55695
|
11 |
val dest_map: Proof.context -> string -> term -> term * term list
|
blanchet@55695
|
12 |
|
blanchet@55738
|
13 |
val mutualize_fp_sugars: BNF_FP_Util.fp_kind -> binding list -> typ list -> (term -> int list) ->
|
blanchet@55738
|
14 |
term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory ->
|
blanchet@54883
|
15 |
(BNF_FP_Def_Sugar.fp_sugar list
|
blanchet@54883
|
16 |
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
|
blanchet@54883
|
17 |
* local_theory
|
blanchet@55719
|
18 |
val indexify_callsss: BNF_FP_Def_Sugar.fp_sugar -> (term * term list list) list ->
|
blanchet@55719
|
19 |
term list list list
|
blanchet@55146
|
20 |
val nested_to_mutual_fps: BNF_FP_Util.fp_kind -> binding list -> typ list -> (term -> int list) ->
|
blanchet@55146
|
21 |
(term * term list list) list list -> local_theory ->
|
blanchet@54883
|
22 |
(typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
|
blanchet@54883
|
23 |
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
|
blanchet@54883
|
24 |
* local_theory
|
blanchet@54440
|
25 |
end;
|
blanchet@54440
|
26 |
|
blanchet@54440
|
27 |
structure BNF_FP_N2M_Sugar : BNF_FP_N2M_SUGAR =
|
blanchet@54440
|
28 |
struct
|
blanchet@54440
|
29 |
|
blanchet@55143
|
30 |
open Ctr_Sugar
|
blanchet@54440
|
31 |
open BNF_Util
|
blanchet@54440
|
32 |
open BNF_Def
|
blanchet@54440
|
33 |
open BNF_FP_Util
|
blanchet@54440
|
34 |
open BNF_FP_Def_Sugar
|
blanchet@54440
|
35 |
open BNF_FP_N2M
|
blanchet@54440
|
36 |
|
blanchet@54440
|
37 |
val n2mN = "n2m_"
|
blanchet@54440
|
38 |
|
blanchet@55708
|
39 |
type n2m_sugar = fp_sugar list * (lfp_sugar_thms option * gfp_sugar_thms option);
|
blanchet@55708
|
40 |
|
blanchet@55708
|
41 |
structure Data = Generic_Data
|
blanchet@55708
|
42 |
(
|
blanchet@55708
|
43 |
type T = n2m_sugar Typtab.table;
|
blanchet@55708
|
44 |
val empty = Typtab.empty;
|
blanchet@55708
|
45 |
val extend = I;
|
blanchet@55708
|
46 |
val merge = Typtab.merge (eq_fst (eq_list eq_fp_sugar));
|
blanchet@55708
|
47 |
);
|
blanchet@55708
|
48 |
|
blanchet@55708
|
49 |
fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) =
|
blanchet@55708
|
50 |
(map (morph_fp_sugar phi) fp_sugars,
|
blanchet@55708
|
51 |
(Option.map (morph_lfp_sugar_thms phi) lfp_sugar_thms_opt,
|
blanchet@55708
|
52 |
Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt));
|
blanchet@55708
|
53 |
|
blanchet@55708
|
54 |
val transfer_n2m_sugar =
|
blanchet@55708
|
55 |
morph_n2m_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
|
blanchet@55708
|
56 |
|
blanchet@55708
|
57 |
fun n2m_sugar_of ctxt =
|
blanchet@55708
|
58 |
Typtab.lookup (Data.get (Context.Proof ctxt))
|
blanchet@55708
|
59 |
#> Option.map (transfer_n2m_sugar ctxt);
|
blanchet@55708
|
60 |
|
blanchet@55708
|
61 |
fun register_n2m_sugar key n2m_sugar =
|
blanchet@55708
|
62 |
Local_Theory.declaration {syntax = false, pervasive = false}
|
blanchet@55708
|
63 |
(fn phi => Data.map (Typtab.default (key, morph_n2m_sugar phi n2m_sugar)));
|
blanchet@55708
|
64 |
|
blanchet@55695
|
65 |
fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1))
|
blanchet@55695
|
66 |
| unfold_let (Const (@{const_name prod_case}, _) $ t) =
|
blanchet@55695
|
67 |
(case unfold_let t of
|
blanchet@55695
|
68 |
t' as Abs (s1, T1, Abs (s2, T2, _)) =>
|
blanchet@55695
|
69 |
let
|
blanchet@55695
|
70 |
val x = (s1 ^ s2, Term.maxidx_of_term t + 1);
|
blanchet@55695
|
71 |
val v = Var (x, HOLogic.mk_prodT (T1, T2));
|
blanchet@55695
|
72 |
in
|
blanchet@55695
|
73 |
lambda v (unfold_let (betapplys (t', [HOLogic.mk_fst v, HOLogic.mk_snd v])))
|
blanchet@55695
|
74 |
end
|
blanchet@55695
|
75 |
| _ => t)
|
blanchet@55695
|
76 |
| unfold_let (t $ u) = betapply (unfold_let t, unfold_let u)
|
blanchet@55695
|
77 |
| unfold_let (Abs (s, T, t)) = Abs (s, T, unfold_let t)
|
blanchet@55695
|
78 |
| unfold_let t = t;
|
blanchet@55695
|
79 |
|
blanchet@55695
|
80 |
fun mk_map_pattern ctxt s =
|
blanchet@55695
|
81 |
let
|
blanchet@55695
|
82 |
val bnf = the (bnf_of ctxt s);
|
blanchet@55695
|
83 |
val mapx = map_of_bnf bnf;
|
blanchet@55695
|
84 |
val live = live_of_bnf bnf;
|
blanchet@55695
|
85 |
val (f_Ts, _) = strip_typeN live (fastype_of mapx);
|
blanchet@55717
|
86 |
val fs = map_index (fn (i, T) => Var (("?f", i), T)) f_Ts;
|
blanchet@55695
|
87 |
in
|
blanchet@55695
|
88 |
(mapx, betapplys (mapx, fs))
|
blanchet@55695
|
89 |
end;
|
blanchet@55695
|
90 |
|
blanchet@55695
|
91 |
fun dest_map ctxt s call =
|
blanchet@55695
|
92 |
let
|
blanchet@55695
|
93 |
val (map0, pat) = mk_map_pattern ctxt s;
|
blanchet@55695
|
94 |
val (_, tenv) = fo_match ctxt call pat;
|
blanchet@55695
|
95 |
in
|
blanchet@55695
|
96 |
(map0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv [])
|
blanchet@55695
|
97 |
end;
|
blanchet@55695
|
98 |
|
blanchet@55728
|
99 |
fun dest_abs_or_applied_map _ _ (Abs (_, _, t)) = (Term.dummy, [t])
|
blanchet@55728
|
100 |
| dest_abs_or_applied_map ctxt s (t1 $ _) = dest_map ctxt s t1;
|
blanchet@55691
|
101 |
|
blanchet@55697
|
102 |
fun map_partition f xs =
|
blanchet@55697
|
103 |
fold_rev (fn x => fn (ys, (good, bad)) =>
|
blanchet@55697
|
104 |
case f x of SOME y => (y :: ys, (x :: good, bad)) | NONE => (ys, (good, x :: bad)))
|
blanchet@55697
|
105 |
xs ([], ([], []));
|
blanchet@55697
|
106 |
|
blanchet@55708
|
107 |
fun key_of_fp_eqs fp fpTs fp_eqs =
|
blanchet@55719
|
108 |
Type (fp_case fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs);
|
blanchet@55708
|
109 |
|
blanchet@54440
|
110 |
(* TODO: test with sort constraints on As *)
|
blanchet@55738
|
111 |
fun mutualize_fp_sugars fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
|
blanchet@55738
|
112 |
let
|
blanchet@55738
|
113 |
val thy = Proof_Context.theory_of no_defs_lthy0;
|
blanchet@54440
|
114 |
|
blanchet@55738
|
115 |
val qsotm = quote o Syntax.string_of_term no_defs_lthy0;
|
blanchet@54440
|
116 |
|
blanchet@55738
|
117 |
fun incompatible_calls t1 t2 =
|
blanchet@55738
|
118 |
error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ qsotm t1 ^ " vs. " ^ qsotm t2);
|
blanchet@55697
|
119 |
|
blanchet@55738
|
120 |
val b_names = map Binding.name_of bs;
|
blanchet@55738
|
121 |
val fp_b_names = map base_name_of_typ fpTs;
|
blanchet@54440
|
122 |
|
blanchet@55738
|
123 |
val nn = length fpTs;
|
blanchet@54440
|
124 |
|
blanchet@55738
|
125 |
fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) =
|
blanchet@55738
|
126 |
let
|
blanchet@55738
|
127 |
val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
|
blanchet@55738
|
128 |
val phi = Morphism.term_morphism (Term.subst_TVars rho);
|
blanchet@55738
|
129 |
in
|
blanchet@55738
|
130 |
morph_ctr_sugar phi (nth ctr_sugars index)
|
blanchet@55738
|
131 |
end;
|
blanchet@54440
|
132 |
|
blanchet@55738
|
133 |
val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
|
blanchet@55738
|
134 |
val mapss = map (of_fp_sugar #mapss) fp_sugars0;
|
blanchet@55738
|
135 |
val ctr_sugars0 = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
|
blanchet@54440
|
136 |
|
blanchet@55738
|
137 |
val ctrss = map #ctrs ctr_sugars0;
|
blanchet@55738
|
138 |
val ctr_Tss = map (map fastype_of) ctrss;
|
blanchet@54440
|
139 |
|
blanchet@55738
|
140 |
val As' = fold (fold Term.add_tfreesT) ctr_Tss [];
|
blanchet@55738
|
141 |
val As = map TFree As';
|
blanchet@54440
|
142 |
|
blanchet@55738
|
143 |
val ((Cs, Xs), no_defs_lthy) =
|
blanchet@55738
|
144 |
no_defs_lthy0
|
blanchet@55738
|
145 |
|> fold Variable.declare_typ As
|
blanchet@55738
|
146 |
|> mk_TFrees nn
|
blanchet@55738
|
147 |
||>> variant_tfrees fp_b_names;
|
blanchet@54440
|
148 |
|
blanchet@55738
|
149 |
fun check_call_dead live_call call =
|
blanchet@55738
|
150 |
if null (get_indices call) then () else incompatible_calls live_call call;
|
blanchet@55697
|
151 |
|
blanchet@55738
|
152 |
fun freeze_fpTs_simple (T as Type (s, Ts)) =
|
blanchet@55738
|
153 |
(case find_index (curry (op =) T) fpTs of
|
blanchet@55738
|
154 |
~1 => Type (s, map freeze_fpTs_simple Ts)
|
blanchet@55738
|
155 |
| kk => nth Xs kk)
|
blanchet@55738
|
156 |
| freeze_fpTs_simple T = T;
|
blanchet@55705
|
157 |
|
blanchet@55738
|
158 |
fun freeze_fpTs_map (callss, (live_call :: _, dead_calls)) s Ts =
|
blanchet@55738
|
159 |
(List.app (check_call_dead live_call) dead_calls;
|
blanchet@55738
|
160 |
Type (s, map2 freeze_fpTs (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
|
blanchet@55738
|
161 |
(transpose callss)) Ts))
|
blanchet@55738
|
162 |
and freeze_fpTs calls (T as Type (s, Ts)) =
|
blanchet@55738
|
163 |
(case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
|
blanchet@55738
|
164 |
([], _) =>
|
blanchet@55738
|
165 |
(case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of
|
blanchet@55738
|
166 |
([], _) => freeze_fpTs_simple T
|
blanchet@55707
|
167 |
| callsp => freeze_fpTs_map callsp s Ts)
|
blanchet@55738
|
168 |
| callsp => freeze_fpTs_map callsp s Ts)
|
blanchet@55738
|
169 |
| freeze_fpTs _ T = T;
|
blanchet@54440
|
170 |
|
blanchet@55738
|
171 |
val ctr_Tsss = map (map binder_types) ctr_Tss;
|
blanchet@55738
|
172 |
val ctrXs_Tsss = map2 (map2 (map2 freeze_fpTs)) callssss ctr_Tsss;
|
blanchet@55738
|
173 |
val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
|
blanchet@55738
|
174 |
val Ts = map (body_type o hd) ctr_Tss;
|
blanchet@54440
|
175 |
|
blanchet@55738
|
176 |
val ns = map length ctr_Tsss;
|
blanchet@55738
|
177 |
val kss = map (fn n => 1 upto n) ns;
|
blanchet@55738
|
178 |
val mss = map (map length) ctr_Tsss;
|
blanchet@54440
|
179 |
|
blanchet@55738
|
180 |
val fp_eqs = map dest_TFree Xs ~~ ctrXs_sum_prod_Ts;
|
blanchet@55738
|
181 |
val key = key_of_fp_eqs fp fpTs fp_eqs;
|
blanchet@55738
|
182 |
in
|
blanchet@55738
|
183 |
(case n2m_sugar_of no_defs_lthy key of
|
blanchet@55738
|
184 |
SOME n2m_sugar => (n2m_sugar, no_defs_lthy)
|
blanchet@55738
|
185 |
| NONE =>
|
blanchet@55738
|
186 |
let
|
blanchet@55738
|
187 |
val base_fp_names = Name.variant_list [] fp_b_names;
|
blanchet@55738
|
188 |
val fp_bs = map2 (fn b_name => fn base_fp_name =>
|
blanchet@55738
|
189 |
Binding.qualify true b_name (Binding.name (n2mN ^ base_fp_name)))
|
blanchet@55738
|
190 |
b_names base_fp_names;
|
blanchet@54440
|
191 |
|
blanchet@55738
|
192 |
val (pre_bnfs, (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_injects,
|
blanchet@55738
|
193 |
dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
|
blanchet@55738
|
194 |
fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' fp_eqs no_defs_lthy;
|
blanchet@54440
|
195 |
|
blanchet@55738
|
196 |
val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
|
blanchet@55738
|
197 |
val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
|
blanchet@54440
|
198 |
|
blanchet@55738
|
199 |
val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
|
blanchet@55738
|
200 |
mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy;
|
blanchet@54440
|
201 |
|
blanchet@55738
|
202 |
fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
|
blanchet@54440
|
203 |
|
blanchet@55738
|
204 |
val ((co_iterss, co_iter_defss), lthy) =
|
blanchet@55738
|
205 |
fold_map2 (fn b =>
|
blanchet@55738
|
206 |
(if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types)
|
blanchet@55738
|
207 |
else define_coiters [unfoldN, corecN] (the coiters_args_types))
|
blanchet@55738
|
208 |
(mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
|
blanchet@55738
|
209 |
|>> split_list;
|
blanchet@54440
|
210 |
|
blanchet@55738
|
211 |
val rho = tvar_subst thy Ts fpTs;
|
blanchet@55738
|
212 |
val ctr_sugar_phi = Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho))
|
blanchet@55738
|
213 |
(Morphism.term_morphism (Term.subst_TVars rho));
|
blanchet@55738
|
214 |
val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi;
|
blanchet@54440
|
215 |
|
blanchet@55738
|
216 |
val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
|
blanchet@54440
|
217 |
|
blanchet@55738
|
218 |
val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
|
blanchet@55738
|
219 |
sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
|
blanchet@55738
|
220 |
if fp = Least_FP then
|
blanchet@55738
|
221 |
derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
|
blanchet@55738
|
222 |
xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
|
blanchet@55738
|
223 |
co_iterss co_iter_defss lthy
|
blanchet@55738
|
224 |
|> `(fn ((_, induct, _), (fold_thmss, rec_thmss, _)) =>
|
blanchet@55738
|
225 |
([induct], fold_thmss, rec_thmss, [], [], [], []))
|
blanchet@55738
|
226 |
||> (fn info => (SOME info, NONE))
|
blanchet@55738
|
227 |
else
|
blanchet@55738
|
228 |
derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
|
blanchet@55738
|
229 |
dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
|
blanchet@55738
|
230 |
ns ctr_defss ctr_sugars co_iterss co_iter_defss
|
blanchet@55738
|
231 |
(Proof_Context.export lthy no_defs_lthy) lthy
|
blanchet@55738
|
232 |
|> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
|
blanchet@55738
|
233 |
(disc_unfold_thmss, disc_corec_thmss, _), _,
|
blanchet@55738
|
234 |
(sel_unfold_thmsss, sel_corec_thmsss, _)) =>
|
blanchet@55738
|
235 |
(map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
|
blanchet@55738
|
236 |
disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
|
blanchet@55738
|
237 |
||> (fn info => (NONE, SOME info));
|
blanchet@54440
|
238 |
|
blanchet@55738
|
239 |
val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
|
blanchet@54440
|
240 |
|
blanchet@55738
|
241 |
fun mk_target_fp_sugar (kk, T) =
|
blanchet@55738
|
242 |
{T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
|
blanchet@55738
|
243 |
nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
|
blanchet@55738
|
244 |
ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
|
blanchet@55738
|
245 |
co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
|
blanchet@55738
|
246 |
disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
|
blanchet@55738
|
247 |
sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
|
blanchet@55738
|
248 |
|> morph_fp_sugar phi;
|
blanchet@54440
|
249 |
|
blanchet@55738
|
250 |
val n2m_sugar = (map_index mk_target_fp_sugar fpTs, fp_sugar_thms);
|
blanchet@55738
|
251 |
in
|
blanchet@55738
|
252 |
(n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar)
|
blanchet@55738
|
253 |
end)
|
blanchet@55738
|
254 |
end;
|
blanchet@54440
|
255 |
|
blanchet@54440
|
256 |
fun indexify_callsss fp_sugar callsss =
|
blanchet@54440
|
257 |
let
|
blanchet@54440
|
258 |
val {ctrs, ...} = of_fp_sugar #ctr_sugars fp_sugar;
|
blanchet@55735
|
259 |
fun indexify_ctr ctr =
|
blanchet@54440
|
260 |
(case AList.lookup Term.aconv_untyped callsss ctr of
|
blanchet@54440
|
261 |
NONE => replicate (num_binder_types (fastype_of ctr)) []
|
blanchet@55695
|
262 |
| SOME callss => map (map (Envir.beta_eta_contract o unfold_let)) callss);
|
blanchet@54440
|
263 |
in
|
blanchet@55735
|
264 |
map indexify_ctr ctrs
|
blanchet@54440
|
265 |
end;
|
blanchet@54440
|
266 |
|
blanchet@55735
|
267 |
fun retypargs tyargs (Type (s, _)) = Type (s, tyargs);
|
blanchet@55735
|
268 |
|
blanchet@55735
|
269 |
fun fold_subtype_pairs f (T as Type (s, Ts), U as Type (s', Us)) =
|
blanchet@55735
|
270 |
f (T, U) #> (if s = s' then fold (fold_subtype_pairs f) (Ts ~~ Us) else I)
|
blanchet@55735
|
271 |
| fold_subtype_pairs f TU = f TU;
|
blanchet@55735
|
272 |
|
blanchet@55146
|
273 |
fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
|
blanchet@54440
|
274 |
let
|
blanchet@54440
|
275 |
val qsoty = quote o Syntax.string_of_typ lthy;
|
blanchet@54440
|
276 |
val qsotys = space_implode " or " o map qsoty;
|
blanchet@54440
|
277 |
|
blanchet@55705
|
278 |
fun duplicate_datatype T = error (qsoty T ^ " is not mutually recursive with itself");
|
blanchet@54440
|
279 |
fun not_co_datatype0 T = error (qsoty T ^ " is not a " ^ co_prefix fp ^ "datatype");
|
blanchet@54440
|
280 |
fun not_co_datatype (T as Type (s, _)) =
|
blanchet@54440
|
281 |
if fp = Least_FP andalso
|
blanchet@54440
|
282 |
is_some (Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then
|
blanchet@54440
|
283 |
error (qsoty T ^ " is not a new-style datatype (cf. \"datatype_new\")")
|
blanchet@54440
|
284 |
else
|
blanchet@54440
|
285 |
not_co_datatype0 T
|
blanchet@54440
|
286 |
| not_co_datatype T = not_co_datatype0 T;
|
blanchet@54440
|
287 |
|
blanchet@55705
|
288 |
val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T);
|
blanchet@55705
|
289 |
|
blanchet@55738
|
290 |
val perm_actual_Ts =
|
blanchet@55718
|
291 |
sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts;
|
blanchet@54440
|
292 |
|
blanchet@55735
|
293 |
fun the_ctrs_of (Type (s, Ts)) = map (mk_ctr Ts) (#ctrs (the (ctr_sugar_of lthy s)));
|
blanchet@55735
|
294 |
|
blanchet@55734
|
295 |
fun the_fp_sugar_of (T as Type (T_name, _)) =
|
blanchet@55734
|
296 |
(case fp_sugar_of lthy T_name of
|
blanchet@55734
|
297 |
SOME (fp_sugar as {fp = fp', ...}) => if fp = fp' then fp_sugar else not_co_datatype T
|
blanchet@55734
|
298 |
| NONE => not_co_datatype T);
|
blanchet@55734
|
299 |
|
blanchet@55735
|
300 |
fun gen_rhss_in gen_Ts rho subTs =
|
blanchet@55735
|
301 |
let
|
blanchet@55735
|
302 |
fun maybe_insert (T, Type (_, gen_tyargs)) =
|
blanchet@55735
|
303 |
if member (op =) subTs T then insert (op =) gen_tyargs else I
|
blanchet@55735
|
304 |
| maybe_insert _ = I;
|
blanchet@55735
|
305 |
|
blanchet@55735
|
306 |
val ctrs = maps the_ctrs_of gen_Ts;
|
blanchet@55735
|
307 |
val gen_ctr_Ts = maps (binder_types o fastype_of) ctrs;
|
blanchet@55735
|
308 |
val ctr_Ts = map (Term.typ_subst_atomic rho) gen_ctr_Ts;
|
blanchet@55735
|
309 |
in
|
blanchet@55735
|
310 |
fold (fold_subtype_pairs maybe_insert) (ctr_Ts ~~ gen_ctr_Ts) []
|
blanchet@55735
|
311 |
end;
|
blanchet@55735
|
312 |
|
blanchet@55738
|
313 |
fun gather_types _ _ num_groups seen gen_seen [] = (num_groups, seen, gen_seen)
|
blanchet@55738
|
314 |
| gather_types lthy rho num_groups seen gen_seen ((T as Type (_, tyargs)) :: Ts) =
|
blanchet@55734
|
315 |
let
|
blanchet@55735
|
316 |
val {fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T;
|
blanchet@55735
|
317 |
val mutual_Ts = map (retypargs tyargs) mutual_Ts0;
|
blanchet@55735
|
318 |
|
blanchet@55735
|
319 |
fun fresh_tyargs () =
|
blanchet@55735
|
320 |
let
|
blanchet@55735
|
321 |
(* The name "'z" is unlikely to clash with the context, yielding more cache hits. *)
|
blanchet@55735
|
322 |
val (gen_tyargs, lthy') =
|
blanchet@55735
|
323 |
variant_tfrees (replicate (length tyargs) "z") lthy
|
blanchet@55735
|
324 |
|>> map Logic.varifyT_global;
|
blanchet@55735
|
325 |
val rho' = (gen_tyargs ~~ tyargs) @ rho;
|
blanchet@55735
|
326 |
in
|
blanchet@55735
|
327 |
(rho', gen_tyargs, gen_seen, lthy')
|
blanchet@55735
|
328 |
end;
|
blanchet@55735
|
329 |
|
blanchet@55735
|
330 |
val (rho', gen_tyargs, gen_seen', lthy') =
|
blanchet@55735
|
331 |
if exists (exists_subtype_in seen) mutual_Ts then
|
blanchet@55735
|
332 |
(case gen_rhss_in gen_seen rho mutual_Ts of
|
blanchet@55735
|
333 |
[] => fresh_tyargs ()
|
blanchet@55735
|
334 |
| gen_tyargss as gen_tyargs :: gen_tyargss_tl =>
|
blanchet@55735
|
335 |
let
|
blanchet@55735
|
336 |
val unify_pairs = split_list (maps (curry (op ~~) gen_tyargs) gen_tyargss_tl);
|
blanchet@55735
|
337 |
val mgu = Type.raw_unifys unify_pairs Vartab.empty;
|
blanchet@55735
|
338 |
val gen_tyargs' = map (Envir.subst_type mgu) gen_tyargs;
|
blanchet@55735
|
339 |
val gen_seen' = map (Envir.subst_type mgu) gen_seen;
|
blanchet@55735
|
340 |
in
|
blanchet@55735
|
341 |
(rho, gen_tyargs', gen_seen', lthy)
|
blanchet@55735
|
342 |
end)
|
blanchet@55735
|
343 |
else
|
blanchet@55735
|
344 |
fresh_tyargs ();
|
blanchet@55735
|
345 |
|
blanchet@55735
|
346 |
val gen_mutual_Ts = map (retypargs gen_tyargs) mutual_Ts0;
|
blanchet@55735
|
347 |
val Ts' = filter_out (member (op =) mutual_Ts) Ts;
|
blanchet@55734
|
348 |
in
|
blanchet@55738
|
349 |
gather_types lthy' rho' (num_groups + 1) (seen @ mutual_Ts) (gen_seen' @ gen_mutual_Ts)
|
blanchet@55738
|
350 |
Ts'
|
blanchet@55734
|
351 |
end
|
blanchet@55738
|
352 |
| gather_types _ _ _ _ _ (T :: _) = not_co_datatype T;
|
blanchet@54440
|
353 |
|
blanchet@55738
|
354 |
val (num_groups, perm_Ts, perm_gen_Ts) = gather_types lthy [] 0 [] [] perm_actual_Ts;
|
blanchet@55735
|
355 |
val perm_frozen_gen_Ts = map Logic.unvarifyT_global perm_gen_Ts;
|
blanchet@55735
|
356 |
|
blanchet@54440
|
357 |
val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
|
blanchet@54440
|
358 |
val Ts = actual_Ts @ missing_Ts;
|
blanchet@54440
|
359 |
|
blanchet@54440
|
360 |
val nn = length Ts;
|
blanchet@54440
|
361 |
val kks = 0 upto nn - 1;
|
blanchet@54440
|
362 |
|
blanchet@55719
|
363 |
val callssss0 = pad_list [] nn actual_callssss0;
|
blanchet@55719
|
364 |
|
blanchet@54440
|
365 |
val common_name = mk_common_name (map Binding.name_of actual_bs);
|
blanchet@54440
|
366 |
val bs = pad_list (Binding.name common_name) nn actual_bs;
|
blanchet@54440
|
367 |
|
blanchet@54440
|
368 |
fun permute xs = permute_like (op =) Ts perm_Ts xs;
|
blanchet@54440
|
369 |
fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs;
|
blanchet@54440
|
370 |
|
blanchet@54440
|
371 |
val perm_bs = permute bs;
|
blanchet@54440
|
372 |
val perm_kks = permute kks;
|
blanchet@55719
|
373 |
val perm_callssss0 = permute callssss0;
|
blanchet@54440
|
374 |
val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
|
blanchet@54440
|
375 |
|
blanchet@55719
|
376 |
val perm_callssss = map2 indexify_callsss perm_fp_sugars0 perm_callssss0;
|
blanchet@54440
|
377 |
|
blanchet@54440
|
378 |
val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
|
blanchet@54440
|
379 |
|
blanchet@54883
|
380 |
val ((perm_fp_sugars, fp_sugar_thms), lthy) =
|
blanchet@55738
|
381 |
if num_groups > 1 then
|
blanchet@55738
|
382 |
mutualize_fp_sugars fp perm_bs perm_frozen_gen_Ts get_perm_indices perm_callssss
|
blanchet@55738
|
383 |
perm_fp_sugars0 lthy
|
blanchet@55738
|
384 |
else
|
blanchet@55738
|
385 |
((perm_fp_sugars0, (NONE, NONE)), lthy);
|
blanchet@54440
|
386 |
|
blanchet@54440
|
387 |
val fp_sugars = unpermute perm_fp_sugars;
|
blanchet@54440
|
388 |
in
|
blanchet@54883
|
389 |
((missing_Ts, perm_kks, fp_sugars, fp_sugar_thms), lthy)
|
blanchet@54440
|
390 |
end;
|
blanchet@54440
|
391 |
|
blanchet@54440
|
392 |
end;
|