328 random_def))) random_defs') |
328 random_def))) random_defs') |
329 |> snd |
329 |> snd |
330 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
330 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
331 end; |
331 end; |
332 |
332 |
|
333 |
|
334 |
333 fun ensure_random_datatype raw_tycos thy = |
335 fun ensure_random_datatype raw_tycos thy = |
334 let |
336 let |
335 val pp = Syntax.pp_global thy; |
337 val pp = Syntax.pp_global thy; |
336 val algebra = Sign.classes_of thy; |
338 val algebra = Sign.classes_of thy; |
337 val (descr, vs, tycos, (names, auxnames), (raw_Ts, raw_Us)) = |
339 val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) = |
338 DatatypePackage.the_datatype_descr thy raw_tycos; |
340 DatatypePackage.the_datatype_descr thy raw_tycos; |
339 |
341 val aTs = (flat o maps snd o maps snd) (DatatypeAux.interpret_construction descr raw_vs |
340 (*FIXME this is only an approximation*) |
342 { atyp = single, dtyp = K o K }); |
341 val (raw_vs :: _, raw_coss) = (split_list |
343 fun meet_random T = Sorts.meet_sort (Sign.classes_of thy) (Logic.varifyT T, @{sort random}); |
342 o map (DatatypePackage.the_datatype_spec thy)) tycos; |
344 val vtab = (Vartab.empty |
343 val raw_Ts' = maps (maps snd) raw_coss; |
345 |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs |
344 val vs' = (fold o fold_atyps) (fn TFree (v, _) => insert (op =) v) raw_Ts' []; |
346 |> fold meet_random aTs |
345 val vs = map (fn (v, sort) => (v, if member (op =) vs' v |
347 |> SOME) handle CLASS_ERROR => NONE; |
346 then Sorts.inter_sort algebra (sort, @{sort random}) else sort)) raw_vs; |
348 val vconstrain = case vtab of SOME vtab => (fn (v, _) => |
347 val constrain = map_atyps |
349 (v, (the o Vartab.lookup vtab) (v, 0))) |
348 (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)); |
350 | NONE => I; |
349 |
351 val vs = map vconstrain raw_vs; |
350 val (Ts, Us) = (pairself o map) constrain (raw_Ts, raw_Us); |
352 val constrain = map_atyps (fn TFree v => TFree (vconstrain v)); |
351 val sorts = map snd vs; |
353 val has_inst = exists (fn tyco => |
352 val algebra' = algebra |
|
353 |> fold (fn tyco => Sorts.add_arities pp |
|
354 (tyco, map (rpair sorts) @{sort random})) tycos; |
|
355 val can_inst = forall (fn T => Sorts.of_sort algebra' (T, @{sort random})) Ts; |
|
356 val hast_inst = exists (fn tyco => |
|
357 can (Sorts.mg_domain algebra tyco) @{sort random}) tycos; |
354 can (Sorts.mg_domain algebra tyco) @{sort random}) tycos; |
358 in if can_inst andalso not hast_inst then |
355 in if is_some vtab andalso not has_inst then |
359 (mk_random_datatype descr vs tycos (names, auxnames) (raw_Ts, raw_Us) thy |
356 (mk_random_datatype descr vs tycos (names, auxnames) |
|
357 ((pairself o map) constrain raw_TUs) thy |
360 (*FIXME ephemeral handles*) |
358 (*FIXME ephemeral handles*) |
361 handle Datatype_Fun => thy |
359 handle Datatype_Fun => thy |
362 | e as TERM (msg, ts) => (tracing (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); raise e) |
360 | e as TERM (msg, ts) => (tracing (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); raise e) |
363 | e as TYPE (msg, _, _) => (tracing msg; raise e) |
361 | e as TYPE (msg, _, _) => (tracing msg; raise e) |
364 | e as ERROR msg => (tracing msg; raise e)) |
362 | e as ERROR msg => (tracing msg; raise e)) |