src/HOL/Tools/Nitpick/nitpick_kodkod.ML

   | _ => lone_rep_fallback kk (Atom x) old_R r
 and struct_from_rel_expr kk Rs old_R r =
   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
     Atom _ => lone_rep_fallback kk (Vect (k, R)) old_R r
   | Vect (k', R') =>

             (map (fn arg_r =>
                      rel_expr_from_formula kk R (#kk_subset kk arg_r r))
                  (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 =>
                    rel_expr_from_rel_expr kk R R2
                                          (kk_n_fold_join kk true R1 R2 arg_r r))

       val R2' = case R2 of Atom _ => R2 | _ => Atom (card_of_rep R2, some_j0)
     in
       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)) =>
        let
          val args_rs = all_singletons_for_rep R1

                     |> rel_expr_from_rel_expr kk R1' R1
            val kk_xeq = (if is_one_rep R1' then #kk_subset else #kk_rel_eq) kk
          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)))
      | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
                        [old_R, Func (R1, Formula Neut)]))

                                  (#kk_subset kk r2 r3)
              end
            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
       else
         let

              val dom_T = domain_type (type_of u1)
              val R1 = rep_of u1
              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)
              val set_R = Func (dom_R, ran_R)
            in

                  val widen2 = (polar = Neg andalso is_opt_rep R2)
                in kk_subset (set_to_r widen1 u1) (set_to_r widen2 u2) end
            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
                 fun args (Op2 (Apply, _, _, u1, u2)) = u2 :: args u1
                   | args (Tuple (_, _, us)) = us

                 else
                   kk_subset (to_rep min_R u1) (to_rep min_R u2)
               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
                 if polar = Neut then
                   (* continuation of hackish optimization *)

         else
           let val R' = rep_to_binary_rel_rep ofs (type_of u1) (rep_of u1) in
             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)
                             (rel_expr_to_func kk R1 bool_atom_R
                                               (Func (R1, Formula Neut)) r))

       | Tuple (_, R, us) =>
         (case unopt_rep R of
            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) =>
         let
           val set_rs =

         KK.AssignRelReg ((arity_of_rep R, j), to_r u)
       | to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1])
     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
           rel_expr_from_rel_expr kk (Opt R) old_R (to_r u)
         else

         else kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r
       end
     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)
       | _ => let
                val R = rep_of u

                      [Atom (a_card, offset_of_type ofs a_T),
                       Atom (b_card, offset_of_type ofs b_T)]
                    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)
         val r1 = to_rep min_R u1
         val r2 = to_rep min_R u2
       in
         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])
       end
     and to_bit_word_unary_op T R oper =

       end
     and to_apply (R as Formula _) func_u arg_u =
         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, _) =>
           let
             val dom_card = card_of_rep (rep_of arg_u)

                    (rel_expr_from_rel_expr kk res_R R' (to_r func_u))
         | Vect (k, R') => to_apply_vect k R' res_R (to_r func_u) arg_u
         | 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))
           |> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R
         | _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u])