Nested tuples no longer put an extra unit type at the end.

This makes the tuple type representation match other systems like lean
more closely.

prelude/Prelude.sawcore

@@ -69,8 +69,8 @@ fst a b tup = tup.(1);
 snd : (a b : sort 0) -> a * b -> b;
 snd a b tup = tup.(2);
 
-uncurry (a b c : sort 0) (f : a -> b -> c) : (#(a, b) -> c)
-  = (\ (x : #(a, b)) -> f x.1 x.2);
+uncurry (a b c : sort 0) (f : a -> b -> c) : a * b -> c
+  = (\ (x : a * b) -> f x.(1) x.(2));
 
 
 --------------------------------------------------------------------------------
@@ -859,13 +859,13 @@ expNat b e =
   Nat_cases Nat 1 (\ (e':Nat) -> \ (exp_b_e:Nat) -> mulNat b exp_b_e) e;
 
 -- | Natural division and modulus
-primitive divModNat : Nat -> Nat -> #(Nat, Nat);
+primitive divModNat : Nat -> Nat -> Nat * Nat;
 
 divNat : Nat -> Nat -> Nat;
-divNat x y = (divModNat x y).1;
+divNat x y = (divModNat x y).(1);
 
 modNat : Nat -> Nat -> Nat;
-modNat x y = (divModNat x y).2;
+modNat x y = (divModNat x y).(2);
 
 -- There are implicit constructors from integer literals.
 
@@ -923,7 +923,7 @@ single = replicate 1;
 axiom at_single : (a : sort 0) -> (x : a) -> (i : Nat) -> Eq a (at 1 a (single a x) i) x;
 
 -- Zip together two lists (truncating the longer of the two).
-primitive zip : (a b : sort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) #(a, b);
+primitive zip : (a b : sort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) (a * b);
 
 primitive foldr : (a b : sort 0) -> (n : Nat) -> (a -> b -> b) -> b -> Vec n a -> b;
 
@@ -1089,7 +1089,7 @@ bvCarry n x y = bvult n (bvAdd n x y) x;
 bvSCarry : (n : Nat) -> bitvector (Succ n) -> bitvector (Succ n) -> Bool;
 bvSCarry n x y = and (boolEq (msb n x) (msb n y)) (xor (msb n x) (msb n (bvAdd (Succ n) x y)));
 
-bvAddWithCarry : (n : Nat) -> bitvector n -> bitvector n -> #(Bool, bitvector n);
+bvAddWithCarry : (n : Nat) -> bitvector n -> bitvector n -> Bool * bitvector n;
 bvAddWithCarry n x y = (bvCarry n x y, bvAdd n x y);
 
 axiom bvAddZeroL : (n : Nat) -> (x : bitvector n) -> Eq (bitvector n) (bvAdd n (bvNat n 0) x) x;

src/Verifier/SAW/SharedTerm.hs

@@ -1068,10 +1068,12 @@ scPairType sc x y = scFlatTermF sc (PairType x y)
 
 scTuple :: SharedContext -> [Term] -> IO Term
 scTuple sc [] = scUnitValue sc
+scTuple _ [t] = return t
 scTuple sc (t : ts) = scPairValue sc t =<< scTuple sc ts
 
 scTupleType :: SharedContext -> [Term] -> IO Term
 scTupleType sc [] = scUnitType sc
+scTupleType _ [t] = return t
 scTupleType sc (t : ts) = scPairType sc t =<< scTupleType sc ts
 
 scPairLeft :: SharedContext -> Term -> IO Term
@@ -1084,11 +1086,16 @@ scPairSelector :: SharedContext -> Term -> Bool -> IO Term
 scPairSelector sc t False = scPairLeft sc t
 scPairSelector sc t True = scPairRight sc t
 
-scTupleSelector :: SharedContext -> Term -> Int -> IO Term
-scTupleSelector sc t i
+scTupleSelector ::
+  SharedContext -> Term ->
+  Int {- ^ 1-based index -} ->
+  Int {- ^ tuple size -} ->
+  IO Term
+scTupleSelector sc t i n
+  | n == 1    = return t
   | i == 1    = scPairLeft sc t
   | i > 1     = do t' <- scPairRight sc t
-                   scTupleSelector sc t' (i - 1)
+                   scTupleSelector sc t' (i - 1) (n - 1)
   | otherwise = fail "scTupleSelector: non-positive index"
 
 scFun :: SharedContext -> Term -> Term -> IO Term

src/Verifier/SAW/Simulator/Value.hs

@@ -171,11 +171,14 @@ instance Show Nil where
 
 vTuple :: VMonad l => [Thunk l] -> Value l
 vTuple [] = VUnit
-vTuple (x:xs) = VPair x (ready (vTuple xs))
+vTuple [_] = error "vTuple: unsupported 1-tuple"
+vTuple [x, y] = VPair x y
+vTuple (x : xs) = VPair x (ready (vTuple xs))
 
 vTupleType :: VMonad l => [Value l] -> Value l
 vTupleType [] = VUnitType
-vTupleType (t:ts) = VPairType t (vTupleType ts)
+vTupleType [t] = t
+vTupleType (t : ts) = VPairType t (vTupleType ts)
 
 valPairLeft :: (VMonad l, Show (Extra l)) => Value l -> MValue l
 valPairLeft (VPair t1 _) = force t1
@@ -229,7 +232,7 @@ asFiniteTypeValue v =
       t2 <- asFiniteTypeValue v2
       case t2 of
         FTTuple ts -> return (FTTuple (t1 : ts))
-        _ -> Nothing
+        _ -> return (FTTuple [t1, t2])
     VRecordType elem_tps ->
       FTRec <$> Map.fromList <$>
       mapM (\(fld,tp) -> (fld,) <$> asFiniteTypeValue tp) elem_tps

src/Verifier/SAW/UntypedAST.hs

@@ -217,17 +217,21 @@ asApp = go []
   where go l (App t u)   = go (u:l) t
         go l t = (t,l)
 
--- | Build a tuple value @(x1, .., xn)@. TODO: unary tuples?
+-- | Build a tuple value @(x1, .., xn)@.
 mkTupleValue :: Pos -> [Term] -> Term
 mkTupleValue p [] = UnitValue p
+mkTupleValue _ [x] = x
 mkTupleValue p (x:xs) = PairValue (pos x) x (mkTupleValue p xs)
 
--- | Build a tuple type @#(x1, .., xn)@. TODO: unary tuples?
+-- | Build a tuple type @#(x1, .., xn)@.
 mkTupleType :: Pos -> [Term] -> Term
 mkTupleType p [] = UnitType p
+mkTupleType _ [x] = x
 mkTupleType p (x:xs) = PairType (pos x) x (mkTupleType p xs)
 
--- | Build a projection @t.i@ of a tuple
+-- | Build a projection @t.i@ of a tuple. NOTE: This function does not
+-- work to access the last component in a tuple, since it always
+-- generates a @PairLeft@.
 mkTupleSelector :: Term -> Integer -> Term
 mkTupleSelector t i
   | i == 1    = PairLeft t