Change saw-core tuple representation.

crux-mir-comp/src/Mir/Compositional/Convert.hs

@@ -315,7 +315,7 @@ termToReg sym sc varMap term shp = do
   where
     go :: forall tp'. TypeShape tp' -> SValue sym -> IO (RegValue sym tp')
     go shp sv = case (shp, sv) of
-        (UnitShape _, SAW.VUnit) -> return ()
+        (UnitShape _, SAW.VTuple ts) | V.null ts -> return ()
         (PrimShape _ BaseBoolRepr, SAW.VBool b) -> return b
         (PrimShape _ (BaseBVRepr w), SAW.VWord (W4.DBV e))
           | Just Refl <- testEquality (W4.exprType e) (BaseBVRepr w) -> return e
@@ -326,9 +326,9 @@ termToReg sym sc varMap term shp = do
                 _ -> fail $ "termToReg: type error: need to produce " ++ show (shapeType shp) ++
                     ", but simulator returned a vector containing " ++ show x
             buildBitVector w bits
-        (TupleShape _ _ flds, _) -> do
-            svs <- tupleToListRev (Ctx.sizeInt $ Ctx.size flds) [] sv
-            goTuple flds svs
+        (TupleShape _ _ flds, SAW.VTuple ts) -> do
+            svs <- traverse SAW.force ts
+            goTuple flds (reverse (V.toList svs))
         (ArrayShape (M.TyArray _ n) _ shp, SAW.VVector thunks) -> do
             svs <- mapM SAW.force $ toList thunks
             when (length svs /= n) $ fail $
@@ -350,21 +350,7 @@ termToReg sym sc varMap term shp = do
         _ -> error $ "termToReg: type error: need to produce " ++ show (shapeType shp) ++
             ", but simulator returned " ++ show sv
 
-    -- | Convert an `SValue` tuple (built from nested `VPair`s) into a list of
-    -- the inner `SValue`s, in reverse order.
-    tupleToListRev :: Int -> [SValue sym] -> SValue sym -> IO [SValue sym]
-    tupleToListRev 2 acc (SAW.VPair x y) = do
-        x' <- SAW.force x
-        y' <- SAW.force y
-        return $ y' : x' : acc
-    tupleToListRev n acc (SAW.VPair x xs) | n > 2 = do
-        x' <- SAW.force x
-        xs' <- SAW.force xs
-        tupleToListRev (n - 1) (x' : acc) xs'
-    tupleToListRev n _ _ | n < 2 = error $ "bad tuple size " ++ show n
-    tupleToListRev n _ v = error $ "termToReg: expected tuple of " ++ show n ++
-        " elements, but got " ++ show v
-
+    -- `SValue`s expected in reverse order.
     goTuple :: forall ctx.
         Assignment FieldShape ctx ->
         [SValue sym] ->