471 make_plain_fun maybe_opt T1 T2 |
471 make_plain_fun maybe_opt T1 T2 |
472 #> unarize_unbox_etc_term |
472 #> unarize_unbox_etc_term |
473 #> format_fun (uniterize_unarize_unbox_etc_type T') |
473 #> format_fun (uniterize_unarize_unbox_etc_type T') |
474 (uniterize_unarize_unbox_etc_type T1) |
474 (uniterize_unarize_unbox_etc_type T1) |
475 (uniterize_unarize_unbox_etc_type T2)) |
475 (uniterize_unarize_unbox_etc_type T2)) |
476 fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ = |
476 |
|
477 |
|
478 fun term_for_fun_or_set seen T T' j = |
477 let |
479 let |
478 val k1 = card_of_type card_assigns T1 |
480 val k1 = card_of_type card_assigns (pseudo_domain_type T) |
479 val k2 = card_of_type card_assigns T2 |
481 val k2 = card_of_type card_assigns (pseudo_range_type T) |
480 in |
482 in |
481 term_for_rep true seen T T' (Vect (k1, Atom (k2, 0))) |
483 term_for_rep true seen T T' (Vect (k1, Atom (k2, 0))) |
482 [nth_combination (replicate k1 (k2, 0)) j] |
484 [nth_combination (replicate k1 (k2, 0)) j] |
483 handle General.Subscript => |
485 handle General.Subscript => |
484 raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom", |
486 raise ARG ("Nitpick_Model.reconstruct_term.\ |
|
487 \term_for_fun_or_set", |
485 signed_string_of_int j ^ " for " ^ |
488 signed_string_of_int j ^ " for " ^ |
486 string_for_rep (Vect (k1, Atom (k2, 0)))) |
489 string_for_rep (Vect (k1, Atom (k2, 0)))) |
487 end |
490 end |
|
491 and term_for_atom seen (T as Type (@{type_name fun}, _)) T' j _ = |
|
492 term_for_fun_or_set seen T T' j |
|
493 | term_for_atom seen (T as Type (@{type_name set}, _)) T' j _ = |
|
494 term_for_fun_or_set seen T T' j |
488 | term_for_atom seen (Type (@{type_name prod}, [T1, T2])) _ j k = |
495 | term_for_atom seen (Type (@{type_name prod}, [T1, T2])) _ j k = |
489 let |
496 let |
490 val k1 = card_of_type card_assigns T1 |
497 val k1 = card_of_type card_assigns T1 |
491 val k2 = k div k1 |
498 val k2 = k div k1 |
492 in |
499 in |
493 list_comb (HOLogic.pair_const T1 T2, |
500 list_comb (HOLogic.pair_const T1 T2, |
494 map3 (fn T => term_for_atom seen T T) [T1, T2] |
501 map3 (fn T => term_for_atom seen T T) [T1, T2] |
495 [j div k2, j mod k2] [k1, k2]) (* ### k2 or k1? FIXME *) |
502 (* ### k2 or k1? FIXME *) |
|
503 [j div k2, j mod k2] [k1, k2]) |
496 end |
504 end |
497 | term_for_atom seen @{typ prop} _ j k = |
505 | term_for_atom seen @{typ prop} _ j k = |
498 HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k) |
506 HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k) |
499 | term_for_atom _ @{typ bool} _ j _ = |
507 | term_for_atom _ @{typ bool} _ j _ = |
500 if j = 0 then @{const False} else @{const True} |
508 if j = 0 then @{const False} else @{const True} |