# HG changeset patch # User blanchet # Date 1280911175 -7200 # Node ID b02e204b613a929f4d9ecf483c2f37ab8b9bc0ad # Parent a493dc2179a30ab457ef5d7df2a7edf5a9de977f get rid of all "optimizations" regarding "unit" and other cardinality-1 types diff -r a493dc2179a3 -r b02e204b613a src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Tue Aug 03 21:37:12 2010 +0200 +++ b/src/HOL/Tools/Nitpick/minipick.ML Wed Aug 04 10:39:35 2010 +0200 @@ -37,7 +37,7 @@ fun check_type ctxt (Type (@{type_name fun}, Ts)) = List.app (check_type ctxt) Ts - | check_type ctxt (Type (@{type_name Product_Type.prod}, Ts)) = + | check_type ctxt (Type (@{type_name prod}, Ts)) = List.app (check_type ctxt) Ts | check_type _ @{typ bool} = () | check_type _ (TFree (_, @{sort "{}"})) = () @@ -51,7 +51,7 @@ atom_schema_of SRep card T1 | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) = atom_schema_of SRep card T1 @ atom_schema_of RRep card T2 - | atom_schema_of _ card (Type (@{type_name Product_Type.prod}, Ts)) = + | atom_schema_of _ card (Type (@{type_name prod}, Ts)) = maps (atom_schema_of SRep card) Ts | atom_schema_of _ card T = [card T] val arity_of = length ooo atom_schema_of @@ -290,7 +290,7 @@ val thy = ProofContext.theory_of ctxt fun card (Type (@{type_name fun}, [T1, T2])) = reasonable_power (card T2) (card T1) - | card (Type (@{type_name Product_Type.prod}, [T1, T2])) = card T1 * card T2 + | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2 | card @{typ bool} = 2 | card T = Int.max (1, raw_card T) val neg_t = @{const Not} $ Object_Logic.atomize_term thy t diff -r a493dc2179a3 -r b02e204b613a src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Aug 03 21:37:12 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Aug 04 10:39:35 2010 +0200 @@ -400,7 +400,6 @@ (@{const_name "op -->"}, 2), (@{const_name If}, 3), (@{const_name Let}, 2), - (@{const_name Unity}, 0), (@{const_name Pair}, 2), (@{const_name fst}, 1), (@{const_name snd}, 1), @@ -456,7 +455,7 @@ | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) = unarize_unbox_etc_type (Type (@{type_name fun}, Ts)) | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) = - Type (@{type_name Product_Type.prod}, map unarize_unbox_etc_type Ts) + Type (@{type_name prod}, map unarize_unbox_etc_type Ts) | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) = @@ -512,7 +511,7 @@ | is_fun_type _ = false fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true | is_set_type _ = false -fun is_pair_type (Type (@{type_name Product_Type.prod}, _)) = true +fun is_pair_type (Type (@{type_name prod}, _)) = true | is_pair_type _ = false fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s | is_lfp_iterator_type _ = false @@ -549,7 +548,7 @@ | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) val nth_range_type = snd oo strip_n_binders -fun num_factors_in_type (Type (@{type_name Product_Type.prod}, [T1, T2])) = +fun num_factors_in_type (Type (@{type_name prod}, [T1, T2])) = fold (Integer.add o num_factors_in_type) [T1, T2] 0 | num_factors_in_type _ = 1 fun num_binder_types (Type (@{type_name fun}, [_, T2])) = @@ -560,7 +559,7 @@ (if is_pair_type (body_type T) then binder_types else curried_binder_types) T fun mk_flat_tuple _ [t] = t - | mk_flat_tuple (Type (@{type_name Product_Type.prod}, [T1, T2])) (t :: ts) = + | mk_flat_tuple (Type (@{type_name prod}, [T1, T2])) (t :: ts) = HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts) | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts) fun dest_n_tuple 1 t = [t] @@ -598,8 +597,8 @@ (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype", e.g., by adding a field to "Datatype_Aux.info". *) fun is_basic_datatype thy stds s = - member (op =) [@{type_name Product_Type.prod}, @{type_name bool}, @{type_name unit}, - @{type_name int}, "Code_Numeral.code_numeral"] s orelse + member (op =) [@{type_name prod}, @{type_name bool}, @{type_name int}, + "Code_Numeral.code_numeral"] s orelse (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T) fun instantiate_type thy T1 T1' T2 = @@ -795,7 +794,7 @@ Type (@{type_name fun}, _) => (boxy = InPair orelse boxy = InFunLHS) andalso not (is_boolean_type (body_type T)) - | Type (@{type_name Product_Type.prod}, Ts) => + | Type (@{type_name prod}, Ts) => boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse ((boxy = InExpr orelse boxy = InFunLHS) andalso exists (is_boxing_worth_it hol_ctxt InPair) @@ -815,12 +814,12 @@ else box_type hol_ctxt (in_fun_lhs_for boxy) T1 --> box_type hol_ctxt (in_fun_rhs_for boxy) T2 - | Type (z as (@{type_name Product_Type.prod}, Ts)) => + | Type (z as (@{type_name prod}, Ts)) => if boxy <> InConstr andalso boxy <> InSel andalso should_box_type hol_ctxt boxy z then Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts) else - Type (@{type_name Product_Type.prod}, + Type (@{type_name prod}, map (box_type hol_ctxt (if boxy = InConstr orelse boxy = InSel then boxy else InPair)) Ts) @@ -982,7 +981,7 @@ Const (nth_sel_for_constr x n) else let - fun aux m (Type (@{type_name Product_Type.prod}, [T1, T2])) = + fun aux m (Type (@{type_name prod}, [T1, T2])) = let val (m, t1) = aux m T1 val (m, t2) = aux m T2 @@ -1072,7 +1071,7 @@ | (Type (new_s, new_Ts as [new_T1, new_T2]), Type (old_s, old_Ts as [old_T1, old_T2])) => if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse - old_s = @{type_name pair_box} orelse old_s = @{type_name Product_Type.prod} then + old_s = @{type_name pair_box} orelse old_s = @{type_name prod} then case constr_expand hol_ctxt old_T t of Const (old_s, _) $ t1 => if new_s = @{type_name fun} then @@ -1084,7 +1083,7 @@ (Type (@{type_name fun}, old_Ts)) t1] | Const _ $ t1 $ t2 => construct_value ctxt stds - (if new_s = @{type_name Product_Type.prod} then @{const_name Pair} + (if new_s = @{type_name prod} then @{const_name Pair} else @{const_name PairBox}, new_Ts ---> new_T) (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2] [t1, t2]) @@ -1095,12 +1094,11 @@ fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) = reasonable_power (card_of_type assigns T2) (card_of_type assigns T1) - | card_of_type assigns (Type (@{type_name Product_Type.prod}, [T1, T2])) = + | card_of_type assigns (Type (@{type_name prod}, [T1, T2])) = card_of_type assigns T1 * card_of_type assigns T2 | card_of_type _ (Type (@{type_name itself}, _)) = 1 | card_of_type _ @{typ prop} = 2 | card_of_type _ @{typ bool} = 2 - | card_of_type _ @{typ unit} = 1 | card_of_type assigns T = case AList.lookup (op =) assigns T of SOME k => k @@ -1116,7 +1114,7 @@ else Int.min (max, reasonable_power k2 k1) end | bounded_card_of_type max default_card assigns - (Type (@{type_name Product_Type.prod}, [T1, T2])) = + (Type (@{type_name prod}, [T1, T2])) = let val k1 = bounded_card_of_type max default_card assigns T1 val k2 = bounded_card_of_type max default_card assigns T2 @@ -1146,7 +1144,7 @@ else if k1 >= max orelse k2 >= max then max else Int.min (max, reasonable_power k2 k1) end - | Type (@{type_name Product_Type.prod}, [T1, T2]) => + | Type (@{type_name prod}, [T1, T2]) => let val k1 = aux avoid T1 val k2 = aux avoid T2 @@ -1158,7 +1156,6 @@ | Type (@{type_name itself}, _) => 1 | @{typ prop} => 2 | @{typ bool} => 2 - | @{typ unit} => 1 | Type _ => (case datatype_constrs hol_ctxt T of [] => if is_integer_type T orelse is_bit_type T then 0 @@ -1198,9 +1195,10 @@ fun special_bounds ts = fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst) +(* FIXME: detect "rep_datatype"? *) fun is_funky_typedef_name thy s = - member (op =) [@{type_name unit}, @{type_name Product_Type.prod}, @{type_name Sum_Type.sum}, - @{type_name int}] s orelse + member (op =) [@{type_name unit}, @{type_name prod}, + @{type_name Sum_Type.sum}, @{type_name int}] s orelse is_frac_type thy (Type (s, [])) fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s | is_funky_typedef _ _ = false @@ -2088,7 +2086,7 @@ val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts val set_T = tuple_T --> bool_T val curried_T = tuple_T --> set_T - val uncurried_T = Type (@{type_name Product_Type.prod}, [tuple_T, tuple_T]) --> bool_T + val uncurried_T = Type (@{type_name prod}, [tuple_T, tuple_T]) --> bool_T val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T) val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs) @@ -2215,11 +2213,10 @@ fun aux T accum = case T of Type (@{type_name fun}, Ts) => fold aux Ts accum - | Type (@{type_name Product_Type.prod}, Ts) => fold aux Ts accum + | Type (@{type_name prod}, Ts) => fold aux Ts accum | Type (@{type_name itself}, [T1]) => aux T1 accum | Type (_, Ts) => - if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) - T then + if member (op =) (@{typ prop} :: @{typ bool} :: accum) T then accum else T :: accum diff -r a493dc2179a3 -r b02e204b613a src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Aug 03 21:37:12 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Aug 04 10:39:35 2010 +0200 @@ -492,24 +492,19 @@ case old_R of Atom _ => lone_rep_fallback kk (Struct Rs) old_R r | Struct Rs' => - let - val Rs = filter (not_equal Unit) Rs - val Rs' = filter (not_equal Unit) Rs' - in - if Rs' = Rs then - r - else if map card_of_rep Rs' = map card_of_rep Rs then - let - val old_arities = map arity_of_rep Rs' - val old_offsets = offset_list old_arities - val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities - in - fold1 (#kk_product kk) - (map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs) - end - else - lone_rep_fallback kk (Struct Rs) old_R r - end + if Rs' = Rs then + r + else if map card_of_rep Rs' = map card_of_rep Rs then + let + val old_arities = map arity_of_rep Rs' + val old_offsets = offset_list old_arities + val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities + in + fold1 (#kk_product kk) + (map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs) + end + else + lone_rep_fallback kk (Struct Rs) old_R r | _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R]) and vect_from_rel_expr kk k R old_R r = case old_R of @@ -525,7 +520,6 @@ (all_singletons_for_rep R1)) else raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) - | Func (Unit, R2) => rel_expr_from_rel_expr kk R R2 r | Func (R1, R2) => fold1 (#kk_product kk) (map (fn arg_r => @@ -541,20 +535,6 @@ func_from_no_opt_rel_expr kk R1 R2 (Vect (dom_card, R2')) (vect_from_rel_expr kk dom_card R2' (Atom x) r) end - | func_from_no_opt_rel_expr kk Unit R2 old_R r = - (case old_R of - Vect (_, R') => rel_expr_from_rel_expr kk R2 R' r - | Func (Unit, R2') => rel_expr_from_rel_expr kk R2 R2' r - | Func (Atom (1, _), Formula Neut) => - (case unopt_rep R2 of - Atom (2, j0) => atom_from_formula kk j0 (#kk_some kk r) - | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", - [old_R, Func (Unit, R2)])) - | Func (R1', R2') => - rel_expr_from_rel_expr kk R2 R2' (#kk_project_seq kk r (arity_of_rep R1') - (arity_of_rep R2')) - | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", - [old_R, Func (Unit, R2)])) | func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r = (case old_R of Vect (k, Atom (2, j0)) => @@ -578,9 +558,6 @@ in #kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r) end - | Func (Unit, (Atom (2, j0))) => - #kk_rel_if kk (#kk_rel_eq kk r (KK.Atom (j0 + 1))) - (full_rel_for_rep R1) (empty_rel_for_rep R1) | Func (R1', Atom (2, j0)) => func_from_no_opt_rel_expr kk R1 (Formula Neut) (Func (R1', Formula Neut)) (#kk_join kk r (KK.Atom (j0 + 1))) @@ -615,11 +592,6 @@ end | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", [old_R, Func (R1, R2)])) - | Func (Unit, R2') => - let val j0 = some_j0 in - func_from_no_opt_rel_expr kk R1 R2 (Func (Atom (1, j0), R2')) - (#kk_product kk (KK.Atom j0) r) - end | Func (R1', R2') => if R1 = R1' andalso R2 = R2' then r @@ -1099,9 +1071,7 @@ val R2 = rep_of u2 val (dom_R, ran_R) = case min_rep R1 R2 of - Func (Unit, R') => - (Atom (1, offset_of_type ofs dom_T), R') - | Func Rp => Rp + Func Rp => Rp | R => (Atom (card_of_domain_from_rep 2 R, offset_of_type ofs dom_T), if is_opt_rep R then Opt bool_atom_R else Formula Neut) @@ -1126,8 +1096,7 @@ end | Op2 (DefEq, _, _, u1, u2) => (case min_rep (rep_of u1) (rep_of u2) of - Unit => KK.True - | Formula polar => + Formula polar => kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) | min_R => let @@ -1145,8 +1114,7 @@ end) | Op2 (Eq, _, _, u1, u2) => (case min_rep (rep_of u1) (rep_of u2) of - Unit => KK.True - | Formula polar => + Formula polar => kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) | min_R => if is_opt_rep min_R then @@ -1426,11 +1394,10 @@ rel_expr_from_rel_expr kk R R' (kk_closure (to_rep R' u1)) end | Op1 (SingletonSet, _, Func (R1, Opt _), Cst (Unrep, _, _)) => - (if R1 = Unit then I else kk_product (full_rel_for_rep R1)) false_atom + kk_product (full_rel_for_rep R1) false_atom | Op1 (SingletonSet, _, R, u1) => (case R of Func (R1, Formula Neut) => to_rep R1 u1 - | Func (Unit, Opt R) => to_guard [u1] R true_atom | Func (R1, Opt _) => single_rel_rel_let kk (fn r => kk_rel_if (kk_no r) (empty_rel_for_rep R) @@ -1676,10 +1643,8 @@ Struct Rs => to_product Rs us | Vect (k, R) => to_product (replicate k R) us | Atom (1, j0) => - (case filter (not_equal Unit o rep_of) us of - [] => KK.Atom j0 - | us' => kk_rel_if (kk_some (fold1 kk_product (map to_r us'))) - (KK.Atom j0) KK.None) + kk_rel_if (kk_some (fold1 kk_product (map to_r us))) + (KK.Atom j0) KK.None | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u])) | Construct ([u'], _, _, []) => to_r u' | Construct (discr_u :: sel_us, _, _, arg_us) => @@ -1715,21 +1680,10 @@ and to_atom (x as (k, j0)) u = case rep_of u of Formula _ => atom_from_formula kk j0 (to_f u) - | Unit => if k = 1 then KK.Atom j0 - else raise NUT ("Nitpick_Kodkod.to_atom", [u]) | R => atom_from_rel_expr kk x R (to_r u) - and to_struct Rs u = - case rep_of u of - Unit => full_rel_for_rep (Struct Rs) - | R' => struct_from_rel_expr kk Rs R' (to_r u) - and to_vect k R u = - case rep_of u of - Unit => full_rel_for_rep (Vect (k, R)) - | R' => vect_from_rel_expr kk k R R' (to_r u) - and to_func R1 R2 u = - case rep_of u of - Unit => full_rel_for_rep (Func (R1, R2)) - | R' => rel_expr_to_func kk R1 R2 R' (to_r u) + and to_struct Rs u = struct_from_rel_expr kk Rs (rep_of u) (to_r u) + and to_vect k R u = vect_from_rel_expr kk k R (rep_of u) (to_r u) + and to_func R1 R2 u = rel_expr_to_func kk R1 R2 (rep_of u) (to_r u) and to_opt R u = let val old_R = rep_of u in if is_opt_rep old_R then @@ -1764,10 +1718,7 @@ and to_project new_R old_R r j0 = rel_expr_from_rel_expr kk new_R old_R (kk_project_seq r j0 (arity_of_rep old_R)) - and to_product Rs us = - case map (uncurry to_opt) (filter (not_equal Unit o fst) (Rs ~~ us)) of - [] => raise REP ("Nitpick_Kodkod.to_product", Rs) - | rs => fold1 kk_product rs + and to_product Rs us = fold1 kk_product (map (uncurry to_opt) (Rs ~~ us)) and to_nth_pair_sel n res_T res_R u = case u of Tuple (_, _, us) => to_rep res_R (nth us n) @@ -1789,12 +1740,7 @@ end val nth_R = nth Rs n val j0 = if n = 0 then 0 else arity_of_rep (hd Rs) - in - case arity_of_rep nth_R of - 0 => to_guard [u] res_R - (to_rep res_R (Cst (Unity, res_T, Unit))) - | _ => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0 - end + in to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0 end and to_set_bool_op connective set_oper u1 u2 = let val min_R = min_rep (rep_of u1) (rep_of u2) @@ -1804,8 +1750,6 @@ case min_R of Vect (k, Atom _) => kk_vect_set_bool_op connective k r1 r2 | Func (_, Formula Neut) => set_oper r1 r2 - | Func (Unit, Atom (2, j0)) => - connective (formula_from_atom j0 r1) (formula_from_atom j0 r2) | Func (_, Atom _) => set_oper (kk_join r1 true_atom) (kk_join r2 true_atom) | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R]) @@ -1843,12 +1787,7 @@ raise REP ("Nitpick_Kodkod.to_apply", [R]) | to_apply res_R func_u arg_u = case unopt_rep (rep_of func_u) of - Unit => - let val j0 = offset_of_type ofs (type_of func_u) in - to_guard [arg_u] res_R - (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (KK.Atom j0)) - end - | Atom (1, j0) => + Atom (1, j0) => to_guard [arg_u] res_R (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (to_r func_u)) | Atom (k, _) => @@ -1867,9 +1806,6 @@ | Func (R, Formula Neut) => to_guard [arg_u] res_R (rel_expr_from_formula kk res_R (kk_subset (to_opt R arg_u) (to_r func_u))) - | Func (Unit, R2) => - to_guard [arg_u] res_R - (rel_expr_from_rel_expr kk res_R R2 (to_r func_u)) | Func (R1, R2) => rel_expr_from_rel_expr kk res_R R2 (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u)) diff -r a493dc2179a3 -r b02e204b613a src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Aug 03 21:37:12 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Aug 04 10:39:35 2010 +0200 @@ -170,7 +170,7 @@ Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])])) $ t1 $ t2) = let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in - Const (@{const_name Pair}, Ts ---> Type (@{type_name Product_Type.prod}, Ts)) + Const (@{const_name Pair}, Ts ---> Type (@{type_name prod}, Ts)) $ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2 end | unarize_unbox_etc_term (Const (s, T)) = @@ -185,27 +185,27 @@ | unarize_unbox_etc_term (Abs (s, T, t')) = Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t') -fun factor_out_types (T1 as Type (@{type_name Product_Type.prod}, [T11, T12])) - (T2 as Type (@{type_name Product_Type.prod}, [T21, T22])) = +fun factor_out_types (T1 as Type (@{type_name prod}, [T11, T12])) + (T2 as Type (@{type_name prod}, [T21, T22])) = let val (n1, n2) = pairself num_factors_in_type (T11, T21) in if n1 = n2 then let val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22 in - ((Type (@{type_name Product_Type.prod}, [T11, T11']), opt_T12'), - (Type (@{type_name Product_Type.prod}, [T21, T21']), opt_T22')) + ((Type (@{type_name prod}, [T11, T11']), opt_T12'), + (Type (@{type_name prod}, [T21, T21']), opt_T22')) end else if n1 < n2 then case factor_out_types T1 T21 of (p1, (T21', NONE)) => (p1, (T21', SOME T22)) | (p1, (T21', SOME T22')) => - (p1, (T21', SOME (Type (@{type_name Product_Type.prod}, [T22', T22])))) + (p1, (T21', SOME (Type (@{type_name prod}, [T22', T22])))) else swap (factor_out_types T2 T1) end - | factor_out_types (Type (@{type_name Product_Type.prod}, [T11, T12])) T2 = + | factor_out_types (Type (@{type_name prod}, [T11, T12])) T2 = ((T11, SOME T12), (T2, NONE)) - | factor_out_types T1 (Type (@{type_name Product_Type.prod}, [T21, T22])) = + | factor_out_types T1 (Type (@{type_name prod}, [T21, T22])) = ((T1, NONE), (T21, SOME T22)) | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE)) @@ -239,7 +239,7 @@ val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2) val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end -fun pair_up (Type (@{type_name Product_Type.prod}, [T1', T2'])) +fun pair_up (Type (@{type_name prod}, [T1', T2'])) (t1 as Const (@{const_name Pair}, Type (@{type_name fun}, [_, Type (@{type_name fun}, [_, T1])])) @@ -287,8 +287,8 @@ and do_term (Type (@{type_name fun}, [T1', T2'])) (Type (@{type_name fun}, [T1, T2])) t = do_fun T1' T2' T1 T2 t - | do_term (T' as Type (@{type_name Product_Type.prod}, Ts' as [T1', T2'])) - (Type (@{type_name Product_Type.prod}, [T1, T2])) + | do_term (T' as Type (@{type_name prod}, Ts' as [T1', T2'])) + (Type (@{type_name prod}, [T1, T2])) (Const (@{const_name Pair}, _) $ t1 $ t2) = Const (@{const_name Pair}, Ts' ---> T') $ do_term T1' T1 t1 $ do_term T2' T2 t2 @@ -303,7 +303,7 @@ | truth_const_sort_key @{const False} = "2" | truth_const_sort_key _ = "1" -fun mk_tuple (Type (@{type_name Product_Type.prod}, [T1, T2])) ts = +fun mk_tuple (Type (@{type_name prod}, [T1, T2])) ts = HOLogic.mk_prod (mk_tuple T1 ts, mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1)))) | mk_tuple _ (t :: _) = t @@ -463,7 +463,7 @@ signed_string_of_int j ^ " for " ^ string_for_rep (Vect (k1, Atom (k2, 0)))) end - | term_for_atom seen (Type (@{type_name Product_Type.prod}, [T1, T2])) _ j k = + | term_for_atom seen (Type (@{type_name prod}, [T1, T2])) _ j k = let val k1 = card_of_type card_assigns T1 val k2 = k div k1 @@ -476,7 +476,6 @@ HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k) | term_for_atom _ @{typ bool} _ j _ = if j = 0 then @{const False} else @{const True} - | term_for_atom _ @{typ unit} _ _ _ = @{const Unity} | term_for_atom seen T _ j k = if T = nat_T andalso is_standard_datatype thy stds nat_T then HOLogic.mk_number nat_T j @@ -588,11 +587,10 @@ (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k)) (map (term_for_rep true seen T2 T2 R o single) (batch_list (arity_of_rep R) js)) - and term_for_rep _ seen T T' Unit [[]] = term_for_atom seen T T' 0 1 - | term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] = + and term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] = if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R]) - | term_for_rep _ seen (Type (@{type_name Product_Type.prod}, [T1, T2])) _ + | term_for_rep _ seen (Type (@{type_name prod}, [T1, T2])) _ (Struct [R1, R2]) [js] = let val arity1 = arity_of_rep R1 diff -r a493dc2179a3 -r b02e204b613a src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Aug 03 21:37:12 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Wed Aug 04 10:39:35 2010 +0200 @@ -254,7 +254,7 @@ else case T of Type (@{type_name fun}, [T1, T2]) => MFun (fresh_mfun_for_fun_type mdata false T1 T2) - | Type (@{type_name Product_Type.prod}, [T1, T2]) => MPair (pairself do_type (T1, T2)) + | Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2)) | Type (z as (s, _)) => if could_exist_alpha_sub_mtype ctxt alpha_T T then case AList.lookup (op =) (!datatype_mcache) z of @@ -1043,8 +1043,8 @@ | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) => Type (if should_finitize T a then @{type_name fin_fun} else @{type_name fun}, map2 type_from_mtype Ts [M1, M2]) - | (MPair (M1, M2), Type (@{type_name Product_Type.prod}, Ts)) => - Type (@{type_name Product_Type.prod}, map2 type_from_mtype Ts [M1, M2]) + | (MPair (M1, M2), Type (@{type_name prod}, Ts)) => + Type (@{type_name prod}, map2 type_from_mtype Ts [M1, M2]) | (MType _, _) => T | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype", [M], [T]) diff -r a493dc2179a3 -r b02e204b613a src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Aug 03 21:37:12 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Aug 04 10:39:35 2010 +0200 @@ -14,7 +14,6 @@ type rep = Nitpick_Rep.rep datatype cst = - Unity | False | True | Iden | @@ -132,7 +131,6 @@ structure KK = Kodkod datatype cst = - Unity | False | True | Iden | @@ -202,8 +200,7 @@ exception NUT of string * nut list -fun string_for_cst Unity = "Unity" - | string_for_cst False = "False" +fun string_for_cst False = "False" | string_for_cst True = "True" | string_for_cst Iden = "Iden" | string_for_cst (Num j) = "Num " ^ signed_string_of_int j @@ -429,7 +426,7 @@ let val res_T = snd (HOLogic.dest_prodT T) in (res_T, Const (@{const_name snd}, T --> res_T) $ t) end -fun factorize (z as (Type (@{type_name Product_Type.prod}, _), _)) = +fun factorize (z as (Type (@{type_name prod}, _), _)) = maps factorize [mk_fst z, mk_snd z] | factorize z = [z] @@ -534,7 +531,6 @@ sub t1, sub_abs s T' t2) | (t0 as Const (@{const_name Let}, _), [t1, t2]) => sub (t0 $ t1 $ eta_expand Ts t2 1) - | (@{const Unity}, []) => Cst (Unity, @{typ unit}, Any) | (Const (@{const_name Pair}, T), [t1, t2]) => Tuple (nth_range_type 2 T, Any, map sub [t1, t2]) | (Const (@{const_name fst}, T), [t1]) => @@ -754,8 +750,6 @@ | Construct (_, _, _, us) => forall is_constructive us | _ => false -fun optimize_unit u = - if rep_of u = Unit then Cst (Unity, type_of u, Unit) else u fun unknown_boolean T R = Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown, T, R) @@ -768,7 +762,6 @@ else raise SAME ()) handle SAME () => Op1 (oper, T, R, u1)) - |> optimize_unit fun s_op2 oper T R u1 u2 = ((case oper of All => if is_subnut_of u1 u2 then Op2 (All, T, R, u1, u2) else u2 @@ -810,7 +803,6 @@ raise SAME () | _ => raise SAME ()) handle SAME () => Op2 (oper, T, R, u1, u2)) - |> optimize_unit fun s_op3 oper T R u1 u2 u3 = ((case oper of Let => @@ -820,13 +812,11 @@ raise SAME () | _ => raise SAME ()) handle SAME () => Op3 (oper, T, R, u1, u2, u3)) - |> optimize_unit fun s_tuple T R us = - (if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us)) - |> optimize_unit + if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us) fun untuple f (Tuple (_, _, us)) = maps (untuple f) us - | untuple f u = if rep_of u = Unit then [] else [f u] + | untuple f u = [f u] fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...}) unsound table def = @@ -855,17 +845,14 @@ Cst (if is_twos_complement_representable bits j then Num j else Unrep, T, best_opt_set_rep_for_type scope T) else - (case spec_of_type scope T of - (1, j0) => if j = 0 then Cst (Unity, T, Unit) - else Cst (Unrep, T, Opt (Atom (1, j0))) - | (k, j0) => - let - val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1 - else j < k) - in - if ok then Cst (Num j, T, Atom (k, j0)) - else Cst (Unrep, T, Opt (Atom (k, j0))) - end) + let + val (k, j0) = spec_of_type scope T + val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1 + else j < k) + in + if ok then Cst (Num j, T, Atom (k, j0)) + else Cst (Unrep, T, Opt (Atom (k, j0))) + end | Cst (Suc, T as Type (@{type_name fun}, [T1, _]), _) => let val R = Atom (spec_of_type scope T1) in Cst (Suc, T, Func (R, Opt R)) @@ -1035,8 +1022,7 @@ in s_op2 Apply T ran_R u1 u2 end | Op2 (Lambda, T, _, u1, u2) => (case best_set_rep_for_type scope T of - Unit => Cst (Unity, T, Unit) - | R as Func (R1, _) => + R as Func (R1, _) => let val table' = NameTable.update (u1, R1) table val u1' = aux table' false Neut u1 @@ -1149,8 +1135,8 @@ let val Rs = map (best_one_rep_for_type scope o type_of) us val us = map sub us - val R = if forall (curry (op =) Unit) Rs then Unit else Struct Rs - val R' = (exists (is_opt_rep o rep_of) us ? opt_rep ofs T) R + val R' = Struct Rs + |> exists (is_opt_rep o rep_of) us ? opt_rep ofs T in s_tuple T R' us end | Construct (us', T, _, us) => let @@ -1170,7 +1156,6 @@ s_op1 Cast (type_of u) (Formula polar) u end end - |> optimize_unit in aux table def Pos end fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys) @@ -1203,7 +1188,7 @@ val w = constr (j, type_of v, rep_of v) in (w :: ws, pool, NameTable.update (v, w) table) end -fun shape_tuple (T as Type (@{type_name Product_Type.prod}, [T1, T2])) (R as Struct [R1, R2]) +fun shape_tuple (T as Type (@{type_name prod}, [T1, T2])) (R as Struct [R1, R2]) us = let val arity1 = arity_of_rep R1 in Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)), @@ -1213,7 +1198,6 @@ Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us)) | shape_tuple T _ [u] = if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u]) - | shape_tuple T Unit [] = Cst (Unity, T, Unit) | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us) fun rename_n_ary_var rename_free v (ws, pool, table) = @@ -1259,7 +1243,6 @@ fun rename_free_vars vs pool table = let - val vs = filter (not_equal Unit o rep_of) vs val (vs, pool, table) = fold (rename_n_ary_var true) vs ([], pool, table) in (rev vs, pool, table) end @@ -1280,7 +1263,7 @@ Op2 (oper, T, R, rename_vars_in_nut pool table u1, rename_vars_in_nut pool table u2) | Op3 (Let, T, R, u1, u2, u3) => - if rep_of u2 = Unit orelse inline_nut u2 then + if inline_nut u2 then let val u2 = rename_vars_in_nut pool table u2 val table = NameTable.update (u1, u2) table diff -r a493dc2179a3 -r b02e204b613a src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Aug 03 21:37:12 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Aug 04 10:39:35 2010 +0200 @@ -132,8 +132,8 @@ let fun box_relational_operator_type (Type (@{type_name fun}, Ts)) = Type (@{type_name fun}, map box_relational_operator_type Ts) - | box_relational_operator_type (Type (@{type_name Product_Type.prod}, Ts)) = - Type (@{type_name Product_Type.prod}, map (box_type hol_ctxt InPair) Ts) + | box_relational_operator_type (Type (@{type_name prod}, Ts)) = + Type (@{type_name prod}, map (box_type hol_ctxt InPair) Ts) | box_relational_operator_type T = T fun add_boxed_types_for_var (z as (_, T)) (T', t') = case t' of @@ -1000,10 +1000,9 @@ and add_axioms_for_type depth T = case T of Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts - | Type (@{type_name Product_Type.prod}, Ts) => fold (add_axioms_for_type depth) Ts + | Type (@{type_name prod}, Ts) => fold (add_axioms_for_type depth) Ts | @{typ prop} => I | @{typ bool} => I - | @{typ unit} => I | TFree (_, S) => add_axioms_for_sort depth T S | TVar (_, S) => add_axioms_for_sort depth T S | Type (z as (_, Ts)) => diff -r a493dc2179a3 -r b02e204b613a src/HOL/Tools/Nitpick/nitpick_rep.ML --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Aug 03 21:37:12 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Wed Aug 04 10:39:35 2010 +0200 @@ -13,7 +13,6 @@ datatype rep = Any | Formula of polarity | - Unit | Atom of int * int | Struct of rep list | Vect of int * rep | @@ -68,7 +67,6 @@ datatype rep = Any | Formula of polarity | - Unit | Atom of int * int | Struct of rep list | Vect of int * rep | @@ -88,7 +86,6 @@ end and string_for_rep Any = "X" | string_for_rep (Formula polar) = "F" ^ string_for_polarity polar - | string_for_rep Unit = "U" | string_for_rep (Atom (k, j0)) = "A" ^ string_of_int k ^ (if j0 = 0 then "" else "@" ^ string_of_int j0) | string_for_rep (Struct rs) = "[" ^ commas (map string_for_rep rs) ^ "]" @@ -108,7 +105,6 @@ fun card_of_rep Any = raise REP ("Nitpick_Rep.card_of_rep", [Any]) | card_of_rep (Formula _) = 2 - | card_of_rep Unit = 1 | card_of_rep (Atom (k, _)) = k | card_of_rep (Struct rs) = Integer.prod (map card_of_rep rs) | card_of_rep (Vect (k, R)) = reasonable_power (card_of_rep R) k @@ -117,7 +113,6 @@ | card_of_rep (Opt R) = card_of_rep R fun arity_of_rep Any = raise REP ("Nitpick_Rep.arity_of_rep", [Any]) | arity_of_rep (Formula _) = 0 - | arity_of_rep Unit = 0 | arity_of_rep (Atom _) = 1 | arity_of_rep (Struct Rs) = Integer.sum (map arity_of_rep Rs) | arity_of_rep (Vect (k, R)) = k * arity_of_rep R @@ -126,7 +121,6 @@ fun min_univ_card_of_rep Any = raise REP ("Nitpick_Rep.min_univ_card_of_rep", [Any]) | min_univ_card_of_rep (Formula _) = 0 - | min_univ_card_of_rep Unit = 0 | min_univ_card_of_rep (Atom (k, j0)) = k + j0 + 1 | min_univ_card_of_rep (Struct Rs) = fold Integer.max (map min_univ_card_of_rep Rs) 0 @@ -135,8 +129,7 @@ Int.max (min_univ_card_of_rep R1, min_univ_card_of_rep R2) | min_univ_card_of_rep (Opt R) = min_univ_card_of_rep R -fun is_one_rep Unit = true - | is_one_rep (Atom _) = true +fun is_one_rep (Atom _) = true | is_one_rep (Struct _) = true | is_one_rep (Vect _) = true | is_one_rep _ = false @@ -145,8 +138,7 @@ fun dest_Func (Func z) = z | dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R]) -fun lazy_range_rep _ _ _ Unit = Unit - | lazy_range_rep _ _ _ (Vect (_, R)) = R +fun lazy_range_rep _ _ _ (Vect (_, R)) = R | lazy_range_rep _ _ _ (Func (_, R2)) = R2 | lazy_range_rep ofs T ran_card (Opt R) = Opt (lazy_range_rep ofs T ran_card R) @@ -201,8 +193,6 @@ Formula (min_polarity polar1 polar2) | min_rep (Formula polar) _ = Formula polar | min_rep _ (Formula polar) = Formula polar - | min_rep Unit _ = Unit - | min_rep _ Unit = Unit | min_rep (Atom x) _ = Atom x | min_rep _ (Atom x) = Atom x | min_rep (Struct Rs1) (Struct Rs2) = Struct (min_reps Rs1 Rs2) @@ -231,8 +221,7 @@ fun card_of_domain_from_rep ran_card R = case R of - Unit => 1 - | Atom (k, _) => exact_log ran_card k + Atom (k, _) => exact_log ran_card k | Vect (k, _) => k | Func (R1, _) => card_of_rep R1 | Opt R => card_of_domain_from_rep ran_card R @@ -246,24 +235,12 @@ fun best_one_rep_for_type (scope as {card_assigns, ...} : scope) (Type (@{type_name fun}, [T1, T2])) = - (case best_one_rep_for_type scope T2 of - Unit => Unit - | R2 => Vect (card_of_type card_assigns T1, R2)) - | best_one_rep_for_type scope (Type (@{type_name Product_Type.prod}, [T1, T2])) = - (case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of - (Unit, Unit) => Unit - | (R1, R2) => Struct [R1, R2]) + Vect (card_of_type card_assigns T1, (best_one_rep_for_type scope T2)) + | best_one_rep_for_type scope (Type (@{type_name prod}, Ts)) = + Struct (map (best_one_rep_for_type scope) Ts) | best_one_rep_for_type {card_assigns, datatypes, ofs, ...} T = - (case card_of_type card_assigns T of - 1 => if is_some (datatype_spec datatypes T) orelse - is_iterator_type T then - Atom (1, offset_of_type ofs T) - else - Unit - | k => Atom (k, offset_of_type ofs T)) + Atom (card_of_type card_assigns T, offset_of_type ofs T) -(* Datatypes are never represented by Unit, because it would confuse - "nfa_transitions_for_ctor". *) fun best_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) = Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2) | best_opt_set_rep_for_type (scope as {ofs, ...}) T = @@ -272,10 +249,7 @@ (Type (@{type_name fun}, [T1, T2])) = (case (best_one_rep_for_type scope T1, best_non_opt_set_rep_for_type scope T2) of - (_, Unit) => Unit - | (Unit, Atom (2, _)) => - Func (Atom (1, offset_of_type ofs T1), Formula Neut) - | (R1, Atom (2, _)) => Func (R1, Formula Neut) + (R1, Atom (2, _)) => Func (R1, Formula Neut) | z => Func z) | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T fun best_set_rep_for_type (scope as {datatypes, ...}) T = @@ -290,7 +264,6 @@ fun atom_schema_of_rep Any = raise REP ("Nitpick_Rep.atom_schema_of_rep", [Any]) | atom_schema_of_rep (Formula _) = [] - | atom_schema_of_rep Unit = [] | atom_schema_of_rep (Atom x) = [x] | atom_schema_of_rep (Struct Rs) = atom_schema_of_reps Rs | atom_schema_of_rep (Vect (k, R)) = replicate_list k (atom_schema_of_rep R) @@ -300,9 +273,8 @@ and atom_schema_of_reps Rs = maps atom_schema_of_rep Rs fun type_schema_of_rep _ (Formula _) = [] - | type_schema_of_rep _ Unit = [] | type_schema_of_rep T (Atom _) = [T] - | type_schema_of_rep (Type (@{type_name Product_Type.prod}, [T1, T2])) (Struct [R1, R2]) = + | type_schema_of_rep (Type (@{type_name prod}, [T1, T2])) (Struct [R1, R2]) = type_schema_of_reps [T1, T2] [R1, R2] | type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) = replicate_list k (type_schema_of_rep T2 R) diff -r a493dc2179a3 -r b02e204b613a src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Aug 03 21:37:12 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Aug 04 10:39:35 2010 +0200 @@ -114,7 +114,7 @@ is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2 | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) = is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2 - | is_complete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) = + | is_complete_type dtypes facto (Type (@{type_name prod}, Ts)) = forall (is_complete_type dtypes facto) Ts | is_complete_type dtypes facto T = not (is_integer_like_type T) andalso not (is_bit_type T) andalso @@ -124,7 +124,7 @@ is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2 | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) = is_concrete_type dtypes facto T2 - | is_concrete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) = + | is_concrete_type dtypes facto (Type (@{type_name prod}, Ts)) = forall (is_concrete_type dtypes facto) Ts | is_concrete_type dtypes facto T = fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto diff -r a493dc2179a3 -r b02e204b613a src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Aug 03 21:37:12 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Wed Aug 04 10:39:35 2010 +0200 @@ -23,10 +23,8 @@ fun cast_to_rep R u = Op1 (Cast, type_of u, R, u) -val unit_T = @{typ unit} val dummy_T = @{typ 'a} -val unity = Cst (Unity, unit_T, Unit) val atom1_v1 = FreeName ("atom1_v1", dummy_T, Atom (1, 0)) val atom2_v1 = FreeName ("atom2_v1", dummy_T, Atom (2, 0)) val atom6_v1 = FreeName ("atom6_v1", dummy_T, Atom (6, 0)) @@ -36,19 +34,14 @@ val atom81_v1 = FreeName ("atom81_v1", dummy_T, Atom (81, 0)) val struct_atom1_atom1_v1 = FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Atom (1, 0)]) -val struct_atom1_unit_v1 = - FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Unit]) -val struct_unit_atom1_v1 = - FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Unit, Atom (1, 0)]) (* - Formula Unit Atom Struct Vect Func - Formula X N/A X X N/A N/A - Unit N/A N/A N/A N/A N/A N/A - Atom X N/A X X X X - Struct N/A N/A X X N/A N/A - Vect N/A N/A X N/A X X - Func N/A N/A X N/A X X + Formula Atom Struct Vect Func + Formula X X X N/A N/A + Atom X X X X X + Struct N/A X X N/A N/A + Vect N/A X N/A X X + Func N/A X N/A X X *) val tests = @@ -77,22 +70,6 @@ Struct [Atom (2, 0), Atom (3, 0)]]) atom24_v1), atom24_v1)), - ("rep_conversion_struct_struct_4", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Struct [Atom (24, 0), Unit]) - (cast_to_rep (Struct [Atom (24, 0), Atom (1, 0)]) atom24_v1), - atom24_v1)), - ("rep_conversion_struct_struct_5", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Struct [Atom (24, 0), Atom (1, 0)]) - (cast_to_rep (Struct [Atom (24, 0), Unit]) atom24_v1), - atom24_v1)), - ("rep_conversion_struct_struct_6", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Struct [Atom (1, 0), Atom (1, 0)]) - (cast_to_rep (Struct [Atom (1, 0), Unit]) - (cast_to_rep (Struct [Unit, Atom (1, 0)]) atom1_v1)), - atom1_v1)), ("rep_conversion_vect_vect_1", Op2 (Eq, bool_T, Formula Neut, cast_to_rep (Atom (16, 0)) @@ -133,50 +110,10 @@ Struct [Atom (2, 0), Atom (3, 0)])) atom36_v1)), atom36_v1)), - ("rep_conversion_func_func_3", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Atom (36, 0)) - (cast_to_rep (Func (Unit, Struct [Atom (6, 0), Atom (6, 0)])) - (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) atom36_v1)), - atom36_v1)), - ("rep_conversion_func_func_4", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Atom (36, 0)) - (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) - (cast_to_rep (Func (Unit, Struct [Atom (6, 0), Atom (6, 0)])) - atom36_v1)), - atom36_v1)), - ("rep_conversion_func_func_5", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Atom (36, 0)) - (cast_to_rep (Func (Unit, Vect (2, Atom (6, 0)))) - (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) atom36_v1)), - atom36_v1)), - ("rep_conversion_func_func_6", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Atom (36, 0)) - (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) - (cast_to_rep (Func (Unit, Vect (2, Atom (6, 0)))) - atom36_v1)), - atom36_v1)), - ("rep_conversion_func_func_7", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Atom (2, 0)) - (cast_to_rep (Func (Unit, Atom (2, 0))) - (cast_to_rep (Func (Atom (1, 0), Formula Neut)) atom2_v1)), - atom2_v1)), - ("rep_conversion_func_func_8", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Atom (2, 0)) - (cast_to_rep (Func (Atom (1, 0), Formula Neut)) - (cast_to_rep (Func (Unit, Atom (2, 0))) atom2_v1)), - atom2_v1)), ("rep_conversion_atom_formula_atom", Op2 (Eq, bool_T, Formula Neut, cast_to_rep (Atom (2, 0)) (cast_to_rep (Formula Neut) atom2_v1), atom2_v1)), - ("rep_conversion_unit_atom", - Op2 (Eq, bool_T, Formula Neut, cast_to_rep (Atom (1, 0)) unity, unity)), ("rep_conversion_atom_struct_atom1", Op2 (Eq, bool_T, Formula Neut, cast_to_rep (Atom (6, 0)) @@ -188,17 +125,6 @@ (cast_to_rep (Struct [Struct [Atom (3, 0), Atom (4, 0)], Atom (2, 0)]) atom24_v1), atom24_v1)), - ("rep_conversion_atom_struct_atom_3", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Atom (6, 0)) - (cast_to_rep (Struct [Atom (6, 0), Unit]) atom6_v1), - atom6_v1)), - ("rep_conversion_atom_struct_atom_4", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Atom (6, 0)) - (cast_to_rep (Struct [Struct [Atom (3, 0), Unit], Atom (2, 0)]) - atom6_v1), - atom6_v1)), ("rep_conversion_atom_vect_func_atom_1", Op2 (Eq, bool_T, Formula Neut, cast_to_rep (Atom (16, 0)) @@ -217,18 +143,6 @@ (cast_to_rep (Vect (4, Atom (2, 0))) (cast_to_rep (Func (Atom (4, 0), Formula Neut)) atom16_v1)), atom16_v1)), - ("rep_conversion_atom_vect_func_atom_4", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Atom (16, 0)) - (cast_to_rep (Vect (1, Atom (16, 0))) - (cast_to_rep (Func (Unit, Atom (16, 0))) atom16_v1)), - atom16_v1)), - ("rep_conversion_atom_vect_func_atom_5", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Atom (16, 0)) - (cast_to_rep (Vect (1, Atom (16, 0))) - (cast_to_rep (Func (Unit, Atom (16, 0))) atom16_v1)), - atom16_v1)), ("rep_conversion_atom_func_vect_atom_1", Op2 (Eq, bool_T, Formula Neut, cast_to_rep (Atom (16, 0)) @@ -247,12 +161,6 @@ (cast_to_rep (Func (Atom (4, 0), Formula Neut)) (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)), atom16_v1)), - ("rep_conversion_atom_func_vect_atom_4", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Atom (16, 0)) - (cast_to_rep (Func (Unit, Atom (16, 0))) - (cast_to_rep (Vect (1, Atom (16, 0))) atom16_v1)), - atom16_v1)), ("rep_conversion_atom_func_vect_atom_5", Op2 (Eq, bool_T, Formula Neut, cast_to_rep (Atom (16, 0)) @@ -274,23 +182,7 @@ ("rep_conversion_struct_atom1_1", Op2 (Eq, bool_T, Formula Neut, cast_to_rep (Struct [Atom (1, 0), Atom (1, 0)]) atom1_v1, - struct_atom1_atom1_v1)), - ("rep_conversion_struct_atom1_2", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Struct [Atom (1, 0), Unit]) atom1_v1, - struct_atom1_unit_v1)), - ("rep_conversion_struct_atom1_3", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Struct [Unit, Atom (1, 0)]) atom1_v1, - struct_unit_atom1_v1)) -(* - ("rep_conversion_struct_formula_struct_1", - Op2 (Eq, bool_T, Formula Neut, - cast_to_rep (Struct [Atom (2, 0), Unit]) - (cast_to_rep (Formula Neut) struct_atom_2_unit_v1), - struct_atom_2_unit_v1)) -*) - ] + struct_atom1_atom1_v1))] fun problem_for_nut ctxt (name, u) = let @@ -319,13 +211,14 @@ fun run_all_tests () = let - val {overlord, ...} = Nitpick_Isar.default_params thy [] + val {overlord, ...} = Nitpick_Isar.default_params @{theory} [] val max_threads = 1 val max_solutions = 1 in case Kodkod.solve_any_problem overlord NONE max_threads max_solutions (map (problem_for_nut @{context}) tests) of - Kodkod.Normal ([], _, _) => () - | _ => error "Tests failed." + Kodkod.Normal ([], _, _) => () + | _ => error "Tests failed." + end end;