From fde77d79f335e6d94954602c26d27070e21ba107 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 23 Oct 2014 13:59:47 -0700 Subject: [PATCH] Make symbolic if-then-else operator lazier on infinite stream values This addresses issue #128. --- src/Cryptol/Symbolic/Value.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Cryptol/Symbolic/Value.hs b/src/Cryptol/Symbolic/Value.hs index 7521d571..e13a7a42 100644 --- a/src/Cryptol/Symbolic/Value.hs +++ b/src/Cryptol/Symbolic/Value.hs @@ -44,7 +44,7 @@ instance Mergeable Value where (VBit b1 , VBit b2 ) -> VBit $ symbolicMerge f c b1 b2 (VWord w1 , VWord w2 ) -> VWord $ symbolicMerge f c w1 w2 (VSeq b1 vs1, VSeq _ vs2 ) -> VSeq b1 $ symbolicMerge f c vs1 vs2 - (VStream vs1, VStream vs2) -> VStream $ symbolicMerge f c vs1 vs2 + (VStream vs1, VStream vs2) -> VStream $ mergeStream vs1 vs2 (VFun f1 , VFun f2 ) -> VFun $ symbolicMerge f c f1 f2 (VPoly f1 , VPoly f2 ) -> VPoly $ symbolicMerge f c f1 f2 (VWord w1 , _ ) -> VWord $ symbolicMerge f c w1 (fromWord v2) @@ -56,6 +56,8 @@ instance Mergeable Value where | n1 == n2 = (n1, symbolicMerge f c x1 x2) | otherwise = panic "Cryptol.Symbolic.Value" [ "symbolicMerge.mergeField: incompatible values" ] + mergeStream xs ys = + symbolicMerge f c (head xs) (head ys) : mergeStream (tail xs) (tail ys) -- Big-endian Words ------------------------------------------------------------