--- 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
--- 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
--- 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))
--- 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
--- 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])
--- 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
--- 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)) =>
--- 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)
--- 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
--- 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;