1(* Title: HOL/Tools/BNF/bnf_fp_n2m_sugar.ML 2 Author: Jasmin Blanchette, TU Muenchen 3 Copyright 2013 4 5Suggared flattening of nested to mutual (co)recursion. 6*) 7 8signature BNF_FP_N2M_SUGAR = 9sig 10 val unfold_lets_splits: term -> term 11 val unfold_splits_lets: term -> term 12 val dest_map: Proof.context -> string -> term -> term * term list 13 val dest_pred: Proof.context -> string -> term -> term * term list 14 15 val mutualize_fp_sugars: (string -> bool) -> BNF_Util.fp_kind -> int list -> binding list -> 16 typ list -> term list -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> 17 local_theory -> 18 (BNF_FP_Def_Sugar.fp_sugar list 19 * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option)) 20 * local_theory 21 val nested_to_mutual_fps: (string -> bool) -> BNF_Util.fp_kind -> binding list -> typ list -> 22 term list -> (term * term list list) list list -> local_theory -> 23 (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list 24 * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option)) 25 * local_theory 26end; 27 28structure BNF_FP_N2M_Sugar : BNF_FP_N2M_SUGAR = 29struct 30 31open Ctr_Sugar 32open BNF_Util 33open BNF_Def 34open BNF_Comp 35open BNF_FP_Util 36open BNF_FP_Def_Sugar 37open BNF_FP_N2M 38 39val n2mN = "n2m_"; 40 41type n2m_sugar = fp_sugar list * (lfp_sugar_thms option * gfp_sugar_thms option); 42 43structure Data = Generic_Data 44( 45 type T = n2m_sugar Typtab.table; 46 val empty = Typtab.empty; 47 val extend = I; 48 fun merge data : T = Typtab.merge (K true) data; 49); 50 51fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) = 52 (map (morph_fp_sugar phi) fp_sugars, 53 (Option.map (morph_lfp_sugar_thms phi) lfp_sugar_thms_opt, 54 Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt)); 55 56val transfer_n2m_sugar = morph_n2m_sugar o Morphism.transfer_morphism; 57 58fun n2m_sugar_of ctxt = 59 Typtab.lookup (Data.get (Context.Proof ctxt)) 60 #> Option.map (transfer_n2m_sugar (Proof_Context.theory_of ctxt)); 61 62fun register_n2m_sugar key n2m_sugar = 63 Local_Theory.declaration {syntax = false, pervasive = false} 64 (fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar))); 65 66fun unfold_lets_splits (Const (\<^const_name>\<open>Let\<close>, _) $ t $ u) = 67 unfold_lets_splits (betapply (unfold_splits_lets u, t)) 68 | unfold_lets_splits (t $ u) = betapply (unfold_lets_splits t, unfold_lets_splits u) 69 | unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t) 70 | unfold_lets_splits t = t 71and unfold_splits_lets ((t as Const (\<^const_name>\<open>case_prod\<close>, _)) $ u) = 72 (case unfold_splits_lets u of 73 u' as Abs (s1, T1, Abs (s2, T2, _)) => 74 let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in 75 lambda v (incr_boundvars 1 (betapplys (u', [HOLogic.mk_fst v, HOLogic.mk_snd v]))) 76 end 77 | _ => t $ unfold_lets_splits u) 78 | unfold_splits_lets (t as Const (\<^const_name>\<open>Let\<close>, _) $ _ $ _) = unfold_lets_splits t 79 | unfold_splits_lets (t $ u) = betapply (unfold_splits_lets t, unfold_lets_splits u) 80 | unfold_splits_lets (Abs (s, T, t)) = Abs (s, T, unfold_splits_lets t) 81 | unfold_splits_lets t = unfold_lets_splits t; 82 83fun dest_either_map_or_pred map_or_pred_of_bnf ctxt T_name call = 84 let 85 val bnf = the (bnf_of ctxt T_name); 86 val const0 = map_or_pred_of_bnf bnf; 87 val live = live_of_bnf bnf; 88 val (f_Ts, _) = strip_typeN live (fastype_of const0); 89 val fs = map_index (fn (i, T) => Var (("f", i), T)) f_Ts; 90 val pat = betapplys (const0, fs); 91 val (_, tenv) = fo_match ctxt call pat; 92 in 93 (const0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv []) 94 end; 95 96val dest_map = dest_either_map_or_pred map_of_bnf; 97val dest_pred = dest_either_map_or_pred pred_of_bnf; 98 99fun dest_map_or_pred ctxt T_name call = 100 (case try (dest_map ctxt T_name) call of 101 SOME res => res 102 | NONE => dest_pred ctxt T_name call); 103 104fun dest_abs_or_applied_map_or_pred _ _ (Abs (_, _, t)) = (Term.dummy, [t]) 105 | dest_abs_or_applied_map_or_pred ctxt s (t1 $ _) = dest_map_or_pred ctxt s t1; 106 107fun map_partition f xs = 108 fold_rev (fn x => fn (ys, (good, bad)) => 109 case f x of SOME y => (y :: ys, (x :: good, bad)) | NONE => (ys, (good, x :: bad))) 110 xs ([], ([], [])); 111 112fun key_of_fp_eqs fp As fpTs Xs ctrXs_repTs = 113 Type (case_fp fp "l" "g", fpTs @ Xs @ ctrXs_repTs) 114 |> Term.map_atyps (fn T as TFree (_, S) => 115 (case find_index (curry (op =) T) As of 116 ~1 => T 117 | j => TFree ("'" ^ string_of_int j, S))); 118 119fun get_indices callers t = 120 callers 121 |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE) 122 |> map_filter I; 123 124fun mutualize_fp_sugars plugins fp mutual_cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy = 125 let 126 val thy = Proof_Context.theory_of no_defs_lthy; 127 128 val qsotm = quote o Syntax.string_of_term no_defs_lthy; 129 130 fun incompatible_calls ts = 131 error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ commas (map qsotm ts)); 132 fun mutual_self_call caller t = 133 error ("Unsupported mutual self-call " ^ qsotm t ^ " from " ^ qsotm caller); 134 fun nested_self_call t = 135 error ("Unsupported nested self-call " ^ qsotm t); 136 137 val b_names = map Binding.name_of bs; 138 val fp_b_names = map base_name_of_typ fpTs; 139 140 val nn = length fpTs; 141 val kks = 0 upto nn - 1; 142 143 fun target_ctr_sugar_of_fp_sugar fpT ({T, fp_ctr_sugar = {ctr_sugar, ...}, ...} : fp_sugar) = 144 let 145 val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) []; 146 val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho); 147 in 148 morph_ctr_sugar phi ctr_sugar 149 end; 150 151 val ctor_iff_dtors = map (#ctor_iff_dtor o #fp_ctr_sugar) fp_sugars0; 152 val ctr_defss = map (#ctr_defs o #fp_ctr_sugar) fp_sugars0; 153 val mapss = map (#map_thms o #fp_bnf_sugar) fp_sugars0; 154 val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0; 155 156 val ctrss = map #ctrs ctr_sugars; 157 val ctr_Tss = map (map fastype_of) ctrss; 158 159 val As' = fold (fold Term.add_tfreesT) ctr_Tss []; 160 val As = map TFree As'; 161 162 val ((Cs, Xs), _) = 163 no_defs_lthy 164 |> fold Variable.declare_typ As 165 |> mk_TFrees nn 166 ||>> variant_tfrees fp_b_names; 167 168 fun check_call_dead live_call call = 169 if null (get_indices callers call) then () else incompatible_calls [live_call, call]; 170 171 fun freeze_fpTs_type_based_default (T as Type (s, Ts)) = 172 (case filter (curry (op =) T o snd) (map_index I fpTs) of 173 [(kk, _)] => nth Xs kk 174 | _ => Type (s, map freeze_fpTs_type_based_default Ts)) 175 | freeze_fpTs_type_based_default T = T; 176 177 fun freeze_fpTs_mutual_call kk fpT calls T = 178 (case fold (union (op =)) (map (get_indices callers) calls) [] of 179 [] => if T = fpT then nth Xs kk else freeze_fpTs_type_based_default T 180 | [kk'] => 181 if T = fpT andalso kk' <> kk then 182 mutual_self_call (nth callers kk) 183 (the (find_first (not o null o get_indices callers) calls)) 184 else if T = nth fpTs kk' then 185 nth Xs kk' 186 else 187 freeze_fpTs_type_based_default T 188 | _ => incompatible_calls calls); 189 190 fun freeze_fpTs_map kk (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls)) 191 (Type (s, Ts)) = 192 if Ts' = Ts then 193 nested_self_call live_call 194 else 195 (List.app (check_call_dead live_call) dead_calls; 196 Type (s, map2 (freeze_fpTs_call kk fpT) 197 (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] (transpose callss)) Ts)) 198 and freeze_fpTs_call kk fpT calls (T as Type (s, _)) = 199 (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of 200 ([], _) => 201 (case map_partition (try (snd o dest_abs_or_applied_map_or_pred no_defs_lthy s)) calls of 202 ([], _) => freeze_fpTs_mutual_call kk fpT calls T 203 | callsp => freeze_fpTs_map kk fpT callsp T) 204 | callsp => freeze_fpTs_map kk fpT callsp T) 205 | freeze_fpTs_call _ _ _ T = T; 206 207 val ctr_Tsss = map (map binder_types) ctr_Tss; 208 val ctrXs_Tsss = @{map 4} (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss; 209 val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss; 210 211 val ns = map length ctr_Tsss; 212 val kss = map (fn n => 1 upto n) ns; 213 val mss = map (map length) ctr_Tsss; 214 215 val key = key_of_fp_eqs fp As fpTs Xs ctrXs_repTs; 216 in 217 (case n2m_sugar_of no_defs_lthy key of 218 SOME n2m_sugar => (n2m_sugar, no_defs_lthy) 219 | NONE => 220 let 221 val base_fp_names = Name.variant_list [] fp_b_names; 222 val fp_bs = map2 (fn b_name => fn base_fp_name => 223 Binding.qualify true b_name (Binding.name (n2mN ^ base_fp_name))) 224 b_names base_fp_names; 225 226 val Type (s, Us) :: _ = fpTs; 227 val killed_As' = 228 (case bnf_of no_defs_lthy s of 229 NONE => As' 230 | SOME bnf => 231 let 232 val Type (_, Ts) = T_of_bnf bnf; 233 val deads = deads_of_bnf bnf; 234 val dead_Us = 235 map_filter (fn (T, U) => if member (op =) deads T then SOME U else NONE) (Ts ~~ Us); 236 in fold Term.add_tfreesT dead_Us [] end); 237 238 val fp_absT_infos = map #absT_info fp_sugars0; 239 val indexed_fp_ress = map (apsnd #fp_res o `(#fp_res_index)) fp_sugars0; 240 241 val (((pre_bnfs, absT_infos), _), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct, 242 dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) = 243 fixpoint_bnf false I (construct_mutualized_fp fp mutual_cliques fpTs indexed_fp_ress) 244 fp_bs As' killed_As' (map dest_TFree Xs) ctrXs_repTs empty_comp_cache no_defs_lthy; 245 246 val time = time lthy; 247 val timer = time (Timer.startRealTimer ()); 248 249 val fp_abs_inverses = map #abs_inverse fp_absT_infos; 250 val fp_type_definitions = map #type_definition fp_absT_infos; 251 252 val abss = map #abs absT_infos; 253 val reps = map #rep absT_infos; 254 val absTs = map #absT absT_infos; 255 val repTs = map #repT absT_infos; 256 val abs_inverses = map #abs_inverse absT_infos; 257 258 val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs; 259 val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As; 260 261 val (xtor_co_recs, recs_args_types, corecs_args_types) = 262 mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0; 263 264 fun mk_binding b pre = Binding.prefix_name (pre ^ "_") b; 265 266 val ((co_recs, co_rec_defs), lthy) = 267 @{fold_map 2} (fn b => 268 if fp = Least_FP then define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps 269 else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss) 270 fp_bs xtor_co_recs lthy 271 |>> split_list; 272 273 val timer = time (timer ("High-level " ^ co_prefix fp ^ "recursors")); 274 275 val ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss, co_rec_sel_thmsss), 276 fp_sugar_thms) = 277 if fp = Least_FP then 278 derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct 279 xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss 280 fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs 281 lthy 282 |> `(fn ((inducts, induct, _), (rec_thmss, _)) => 283 ([induct], [inducts], rec_thmss, replicate nn [], replicate nn [])) 284 ||> (fn info => (SOME info, NONE)) 285 else 286 derive_coinduct_corecs_thms_for_types lthy pre_bnfs (the corecs_args_types) 287 xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs 288 ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses 289 (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs 290 |> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _, 291 (corec_sel_thmsss, _)) => 292 (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss, 293 corec_disc_thmss, corec_sel_thmsss)) 294 ||> (fn info => (NONE, SOME info)); 295 296 val timer = time (timer ("High-level " ^ co_prefix fp ^ "induction principles")); 297 298 val names_lthy = lthy |> fold Variable.declare_typ (As @ Cs @ Xs); 299 val phi = Proof_Context.export_morphism names_lthy lthy; 300 301 fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctor_iff_dtor ctr_defs ctr_sugar 302 co_rec co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss 303 ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, sel_transfers, ...}, 304 fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels, 305 rel_intros, rel_cases, pred_injects, set_thms, set_selssss, set_introssss, 306 set_cases, ...}, 307 fp_co_induct_sugar = SOME {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, 308 co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts, 309 set_inducts, ...}, 310 ...} : fp_sugar) = 311 {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, 312 pre_bnf = pre_bnf, fp_bnf = nth (#bnfs fp_res) kk, absT_info = absT_info, 313 fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs, 314 fp_ctr_sugar = 315 {ctrXs_Tss = ctrXs_Tss, 316 ctor_iff_dtor = ctor_iff_dtor, 317 ctr_defs = ctr_defs, 318 ctr_sugar = ctr_sugar, 319 ctr_transfers = ctr_transfers, 320 case_transfers = case_transfers, 321 disc_transfers = disc_transfers, 322 sel_transfers = sel_transfers}, 323 fp_bnf_sugar = 324 {map_thms = map_thms, 325 map_disc_iffs = map_disc_iffs, 326 map_selss = map_selss, 327 rel_injects = rel_injects, 328 rel_distincts = rel_distincts, 329 rel_sels = rel_sels, 330 rel_intros = rel_intros, 331 rel_cases = rel_cases, 332 pred_injects = pred_injects, 333 set_thms = set_thms, 334 set_selssss = set_selssss, 335 set_introssss = set_introssss, 336 set_cases = set_cases}, 337 fp_co_induct_sugar = SOME 338 {co_rec = co_rec, 339 common_co_inducts = common_co_inducts, 340 co_inducts = co_inducts, 341 co_rec_def = co_rec_def, 342 co_rec_thms = co_rec_thms, 343 co_rec_discs = co_rec_disc_thms, 344 co_rec_disc_iffs = co_rec_disc_iffs, 345 co_rec_selss = co_rec_sel_thmss, 346 co_rec_codes = co_rec_codes, 347 co_rec_transfers = co_rec_transfers, 348 co_rec_o_maps = co_rec_o_maps, 349 common_rel_co_inducts = common_rel_co_inducts, 350 rel_co_inducts = rel_co_inducts, 351 common_set_inducts = common_set_inducts, 352 set_inducts = set_inducts}} 353 |> morph_fp_sugar phi; 354 355 val target_fp_sugars = 356 @{map 17} mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctor_iff_dtors 357 ctr_defss ctr_sugars co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss 358 co_rec_disc_thmss co_rec_sel_thmsss fp_sugars0; 359 360 val n2m_sugar = (target_fp_sugars, fp_sugar_thms); 361 in 362 (n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar) 363 end) 364 end; 365 366fun indexify_callsss ctrs callsss = 367 let 368 fun indexify_ctr ctr = 369 (case AList.lookup Term.aconv_untyped callsss ctr of 370 NONE => replicate (num_binder_types (fastype_of ctr)) [] 371 | SOME callss => map (map (Envir.beta_eta_contract o unfold_lets_splits)) callss); 372 in 373 map indexify_ctr ctrs 374 end; 375 376fun retypargs tyargs (Type (s, _)) = Type (s, tyargs); 377 378fun fold_subtype_pairs f (T as Type (s, Ts), U as Type (s', Us)) = 379 f (T, U) #> (if s = s' then fold (fold_subtype_pairs f) (Ts ~~ Us) else I) 380 | fold_subtype_pairs f TU = f TU; 381 382val impossible_caller = Bound ~1; 383 384fun nested_to_mutual_fps plugins fp actual_bs actual_Ts actual_callers actual_callssss0 lthy = 385 let 386 val qsoty = quote o Syntax.string_of_typ lthy; 387 val qsotys = space_implode " or " o map qsoty; 388 389 fun not_co_datatype0 T = error (qsoty T ^ " is not a " ^ co_prefix fp ^ "datatype"); 390 fun not_co_datatype (T as Type (s, _)) = 391 if fp = Least_FP andalso 392 is_some (Old_Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then 393 error (qsoty T ^ " is an old-style datatype") 394 else 395 not_co_datatype0 T 396 | not_co_datatype T = not_co_datatype0 T; 397 fun not_mutually_nested_rec Ts1 Ts2 = 398 error (qsotys Ts1 ^ " is neither mutually " ^ co_prefix fp ^ "recursive with " ^ qsotys Ts2 ^ 399 " nor nested " ^ co_prefix fp ^ "recursive through " ^ 400 (if Ts1 = Ts2 andalso length Ts1 = 1 then "itself" else qsotys Ts2)); 401 402 val sorted_actual_Ts = 403 sort (prod_ord int_ord Term_Ord.typ_ord o apply2 (`Term.size_of_typ)) actual_Ts; 404 405 fun the_ctrs_of (Type (s, Ts)) = map (mk_ctr Ts) (#ctrs (the (ctr_sugar_of lthy s))); 406 407 fun gen_rhss_in gen_Ts rho (subTs as Type (_, sub_tyargs) :: _) = 408 let 409 fun maybe_insert (T, Type (_, gen_tyargs)) = 410 member (op =) subTs T ? insert (op =) gen_tyargs 411 | maybe_insert _ = I; 412 413 val gen_ctrs = maps the_ctrs_of gen_Ts; 414 val gen_ctr_Ts = maps (binder_types o fastype_of) gen_ctrs; 415 val ctr_Ts = map (Term.typ_subst_atomic rho) gen_ctr_Ts; 416 in 417 (case fold (fold_subtype_pairs maybe_insert) (ctr_Ts ~~ gen_ctr_Ts) [] of 418 [] => [map (typ_subst_nonatomic (map swap rho)) sub_tyargs] 419 | gen_tyargss => gen_tyargss) 420 end; 421 422 fun the_fp_sugar_of (T as Type (T_name, _)) = 423 (case fp_sugar_of lthy T_name of 424 SOME (fp_sugar as {fp = fp', fp_co_induct_sugar = SOME _, ...}) => 425 if fp = fp' then fp_sugar else not_co_datatype T 426 | _ => not_co_datatype T); 427 428 fun gather_types _ _ rev_seens gen_seen [] = (rev rev_seens, gen_seen) 429 | gather_types lthy rho rev_seens gen_seen ((T as Type (_, tyargs)) :: Ts) = 430 let 431 val {T = Type (_, tyargs0), fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T; 432 val mutual_Ts = map (retypargs tyargs) mutual_Ts0; 433 434 val rev_seen = flat rev_seens; 435 val _ = null rev_seens orelse exists (exists_strict_subtype_in rev_seen) mutual_Ts orelse 436 not_mutually_nested_rec mutual_Ts rev_seen; 437 438 fun fresh_tyargs () = 439 let 440 val (unsorted_gen_tyargs, lthy') = 441 variant_tfrees (replicate (length tyargs) "z") lthy 442 |>> map Logic.varifyT_global; 443 val gen_tyargs = 444 map2 (resort_tfree_or_tvar o snd o dest_TFree_or_TVar) tyargs0 unsorted_gen_tyargs; 445 val rho' = (gen_tyargs ~~ tyargs) @ rho; 446 in 447 (rho', gen_tyargs, gen_seen, lthy') 448 end; 449 450 val (rho', gen_tyargs, gen_seen', lthy') = 451 if exists (exists_subtype_in (flat rev_seens)) mutual_Ts then 452 (case gen_rhss_in gen_seen rho mutual_Ts of 453 [] => fresh_tyargs () 454 | gen_tyargs :: gen_tyargss_tl => 455 let 456 val unify_pairs = split_list (maps (curry (op ~~) gen_tyargs) gen_tyargss_tl); 457 val mgu = Type.raw_unifys unify_pairs Vartab.empty; 458 val gen_tyargs' = map (Envir.norm_type mgu) gen_tyargs; 459 val gen_seen' = map (Envir.norm_type mgu) gen_seen; 460 in 461 (rho, gen_tyargs', gen_seen', lthy) 462 end) 463 else 464 fresh_tyargs (); 465 466 val gen_mutual_Ts = map (retypargs gen_tyargs) mutual_Ts0; 467 val other_mutual_Ts = remove1 (op =) T mutual_Ts; 468 val Ts' = fold (remove1 (op =)) other_mutual_Ts Ts; 469 in 470 gather_types lthy' rho' (mutual_Ts :: rev_seens) (gen_seen' @ gen_mutual_Ts) Ts' 471 end 472 | gather_types _ _ _ _ (T :: _) = not_co_datatype T; 473 474 val (perm_Tss, perm_gen_Ts) = gather_types lthy [] [] [] sorted_actual_Ts; 475 val (perm_mutual_cliques, perm_Ts) = 476 split_list (flat (map_index (fn (i, perm_Ts) => map (pair i) perm_Ts) perm_Tss)); 477 478 val perm_frozen_gen_Ts = map Logic.unvarifyT_global perm_gen_Ts; 479 480 val missing_Ts = fold (remove1 (op =)) actual_Ts perm_Ts; 481 val Ts = actual_Ts @ missing_Ts; 482 483 val nn = length Ts; 484 val kks = 0 upto nn - 1; 485 486 val callssss0 = pad_list [] nn actual_callssss0; 487 488 val common_name = mk_common_name (map Binding.name_of actual_bs); 489 val bs = pad_list (Binding.name common_name) nn actual_bs; 490 val callers = pad_list impossible_caller nn actual_callers; 491 492 fun permute xs = permute_like (op =) Ts perm_Ts xs; 493 fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs; 494 495 (* The assignment of callers to mutual cliques is incorrect in general. This code would need to 496 inspect the actual calls to discover the correct cliques in the presence of type duplicates. 497 However, the naive scheme implemented here supports "prim(co)rec" specifications following 498 reasonable ordering of the duplicates (e.g., keeping the cliques together). *) 499 val perm_bs = permute bs; 500 val perm_callers = permute callers; 501 val perm_kks = permute kks; 502 val perm_callssss0 = permute callssss0; 503 val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts; 504 505 val perm_callssss = 506 map2 (indexify_callsss o #ctrs o #ctr_sugar o #fp_ctr_sugar) perm_fp_sugars0 perm_callssss0; 507 508 val ((perm_fp_sugars, fp_sugar_thms), lthy) = 509 if length perm_Tss = 1 then 510 ((perm_fp_sugars0, (NONE, NONE)), lthy) 511 else 512 mutualize_fp_sugars plugins fp perm_mutual_cliques perm_bs perm_frozen_gen_Ts perm_callers 513 perm_callssss perm_fp_sugars0 lthy; 514 515 val fp_sugars = unpermute perm_fp_sugars; 516 in 517 ((missing_Ts, perm_kks, fp_sugars, fp_sugar_thms), lthy) 518 end; 519 520end; 521