From ccfbd1f2de779ffe627b2f2108d9b49539a79e6f Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 2 Dec 2014 14:07:23 -0800
Subject: [PATCH] Fix symbolic simulator implementations of (!!) and (@@)

Now these operations correctly set the is-bit flag on
the VSeq constructor when the result type is a list of bits.

Fixes #148.
---
 src/Cryptol/Symbolic/Prims.hs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs
index 3747f212..30c9f150 100644
--- a/src/Cryptol/Symbolic/Prims.hs
+++ b/src/Cryptol/Symbolic/Prims.hs
@@ -206,7 +206,7 @@ evalECon econ =
       VFun $ \xs ->
       VFun $ \ys ->
         let err = zeroV a -- default for out-of-bounds accesses
-        in mapV (selectV (\i -> nthV err xs i)) ys
+        in mapV (isTBit a) (selectV (\i -> nthV err xs i)) ys
 
     ECAtBack      -> -- {n,a,i} (fin n, fin i) => [n]a -> [i] -> a
       tlam $ \(finTValue -> n) ->
@@ -225,7 +225,7 @@ evalECon econ =
       VFun $ \xs ->
       VFun $ \ys ->
         let err = zeroV a -- default for out-of-bounds accesses
-        in mapV (selectV (\i -> nthV err xs (n - 1 - i))) ys
+        in mapV (isTBit a) (selectV (\i -> nthV err xs (n - 1 - i))) ys
 
     ECFromThen   -> fromThenV
     ECFromTo     -> fromToV
@@ -315,10 +315,10 @@ nthV err v n =
                                     VBit (SBV.sbvTestBit x i)
     _                       -> err
 
-mapV :: (Value -> Value) -> Value -> Value
-mapV f v =
+mapV :: Bool -> (Value -> Value) -> Value -> Value
+mapV isBit f v =
   case v of
-    VSeq b xs  -> VSeq b (map f xs)
+    VSeq _ xs  -> VSeq isBit (map f xs)
     VStream xs -> VStream (map f xs)
     _          -> panic "Cryptol.Symbolic.Prims.mapV" [ "non-mappable value" ]