--- 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))