    -- |
    -- Module      :  Cryptol.Symbolic.Value
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE TypeSynonymInstances #-}
    {-# OPTIONS_GHC -fno-warn-orphans #-}
    module Cryptol.Symbolic.Value
      ( SBool, SWord, SInteger
      , literalSWord
      , fromBitsLE
      , forallBV_, existsBV_
      , forallSBool_, existsSBool_
      , forallSInteger_, existsSInteger_
      , Value
      , TValue, isTBit, tvSeq
      , GenValue(..), lam, tlam, toStream, toFinSeq, toSeq
      , fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
      , fromSeq, fromVWord
      , evalPanic
      , iteSValue, mergeValue, mergeWord, mergeBit, mergeBits, mergeSeqMap
      , mergeWord'
      )
      where

    import Data.Bits (bit, complement)
    import Data.List (foldl')
    import qualified Data.Sequence as Seq

    import Data.SBV (symbolicEnv)
    import Data.SBV.Dynamic

    --import Cryptol.Eval.Monad
    import Cryptol.Eval.Type   (TValue(..), isTBit, tvSeq)
    import Cryptol.Eval.Monad  (Eval, ready)
    import Cryptol.Eval.Value  ( GenValue(..), BitWord(..), lam, tlam, toStream,
                               toFinSeq, toSeq, WordValue(..),
                               fromSeq, fromVBit, fromVWord, fromVFun, fromVPoly,
                               fromVTuple, fromVRecord, lookupRecord, SeqMap(..),
                               ppBV, BV(..), integerToChar, lookupSeqMap, memoMap,
                               wordValueSize, asBitsMap)
    import Cryptol.Utils.Panic (panic)
    import Cryptol.Utils.PP

    import Control.Monad.Trans  (liftIO)

    -- SBool and SWord -------------------------------------------------------------

    type SBool = SVal
    type SWord = SVal
    type SInteger = SVal

    fromBitsLE :: [SBool] -> SWord
    fromBitsLE :: [SBool] -> SBool
    fromBitsLE bs :: [SBool]
    bs = (SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl' SBool -> SBool -> SBool
    f (Int -> Integer -> SBool
    literalSWord 0 0) [SBool]
    bs
      where f :: SBool -> SBool -> SBool
    f w :: SBool
    w b :: SBool
    b = SBool -> SBool -> SBool
    svJoin (SBool -> SBool
    svToWord1 SBool
    b) SBool
    w

    literalSWord :: Int -> Integer -> SWord
    literalSWord :: Int -> Integer -> SBool
    literalSWord w :: Int
    w i :: Integer
    i = Kind -> Integer -> SBool
    svInteger (Bool -> Int -> Kind
    KBounded Bool
    False Int
    w) Integer
    i

    forallBV_ :: Int -> Symbolic SWord
    forallBV_ :: Int -> Symbolic SBool
    forallBV_ w :: Int
    w = SymbolicT IO State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv SymbolicT IO State -> (State -> Symbolic SBool) -> Symbolic SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SBool -> Symbolic SBool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SBool -> Symbolic SBool)
    -> (State -> IO SBool) -> State -> Symbolic SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SBool
    svMkSymVar (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    ALL) (Bool -> Int -> Kind
    KBounded Bool
    False Int
    w) Maybe String
    forall a. Maybe a
    Nothing

    existsBV_ :: Int -> Symbolic SWord
    existsBV_ :: Int -> Symbolic SBool
    existsBV_ w :: Int
    w = SymbolicT IO State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv SymbolicT IO State -> (State -> Symbolic SBool) -> Symbolic SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SBool -> Symbolic SBool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SBool -> Symbolic SBool)
    -> (State -> IO SBool) -> State -> Symbolic SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SBool
    svMkSymVar (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    EX) (Bool -> Int -> Kind
    KBounded Bool
    False Int
    w) Maybe String
    forall a. Maybe a
    Nothing

    forallSBool_ :: Symbolic SBool
    forallSBool_ :: Symbolic SBool
    forallSBool_ = SymbolicT IO State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv SymbolicT IO State -> (State -> Symbolic SBool) -> Symbolic SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SBool -> Symbolic SBool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SBool -> Symbolic SBool)
    -> (State -> IO SBool) -> State -> Symbolic SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SBool
    svMkSymVar (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    ALL) Kind
    KBool Maybe String
    forall a. Maybe a
    Nothing

    existsSBool_ :: Symbolic SBool
    existsSBool_ :: Symbolic SBool
    existsSBool_ = SymbolicT IO State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv SymbolicT IO State -> (State -> Symbolic SBool) -> Symbolic SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SBool -> Symbolic SBool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SBool -> Symbolic SBool)
    -> (State -> IO SBool) -> State -> Symbolic SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SBool
    svMkSymVar (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    EX) Kind
    KBool Maybe String
    forall a. Maybe a
    Nothing

    forallSInteger_ :: Symbolic SBool
    forallSInteger_ :: Symbolic SBool
    forallSInteger_ = SymbolicT IO State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv SymbolicT IO State -> (State -> Symbolic SBool) -> Symbolic SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SBool -> Symbolic SBool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SBool -> Symbolic SBool)
    -> (State -> IO SBool) -> State -> Symbolic SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SBool
    svMkSymVar (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    ALL) Kind
    KUnbounded Maybe String
    forall a. Maybe a
    Nothing

    existsSInteger_ :: Symbolic SBool
    existsSInteger_ :: Symbolic SBool
    existsSInteger_ = SymbolicT IO State
    forall (m :: * -> *). MonadSymbolic m => m State
    symbolicEnv SymbolicT IO State -> (State -> Symbolic SBool) -> Symbolic SBool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= IO SBool -> Symbolic SBool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO SBool -> Symbolic SBool)
    -> (State -> IO SBool) -> State -> Symbolic SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Quantifier -> Kind -> Maybe String -> State -> IO SBool
    svMkSymVar (Quantifier -> Maybe Quantifier
    forall a. a -> Maybe a
    Just Quantifier
    EX) Kind
    KUnbounded Maybe String
    forall a. Maybe a
    Nothing

    -- Values ----------------------------------------------------------------------

    type Value = GenValue SBool SWord SInteger

    -- Symbolic Conditionals -------------------------------------------------------

    iteSValue :: SBool -> Value -> Value -> Eval Value
    iteSValue :: SBool -> Value -> Value -> Eval Value
    iteSValue c :: SBool
    c x :: Value
    x y :: Value
    y =
      case SBool -> Maybe Bool
    svAsBool SBool
    c of
        Just True  -> Value -> Eval Value
    forall (m :: * -> *) a. Monad m => a -> m a
    return Value
    x
        Just False -> Value -> Eval Value
    forall (m :: * -> *) a. Monad m => a -> m a
    return Value
    y
        Nothing    -> Bool -> SBool -> Value -> Value -> Eval Value
    mergeValue Bool
    True SBool
    c Value
    x Value
    y

    mergeBit :: Bool
             -> SBool
             -> SBool
             -> SBool
             -> SBool
    mergeBit :: Bool -> SBool -> SBool -> SBool -> SBool
    mergeBit f :: Bool
    f c :: SBool
    c b1 :: SBool
    b1 b2 :: SBool
    b2 = Kind -> Bool -> SBool -> SBool -> SBool -> SBool
    svSymbolicMerge Kind
    KBool Bool
    f SBool
    c SBool
    b1 SBool
    b2

    mergeWord :: Bool
              -> SBool
              -> WordValue SBool SWord SInteger
              -> WordValue SBool SWord SInteger
              -> WordValue SBool SWord SInteger
    mergeWord :: Bool
    -> SBool
    -> WordValue SBool SBool SBool
    -> WordValue SBool SBool SBool
    -> WordValue SBool SBool SBool
    mergeWord f :: Bool
    f c :: SBool
    c (WordVal w1 :: SBool
    w1) (WordVal w2 :: SBool
    w2) =
        SBool -> WordValue SBool SBool SBool
    forall b w i. w -> WordValue b w i
    WordVal (SBool -> WordValue SBool SBool SBool)
    -> SBool -> WordValue SBool SBool SBool
    forall a b. (a -> b) -> a -> b
    $ Kind -> Bool -> SBool -> SBool -> SBool -> SBool
    svSymbolicMerge (SBool -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBool
    w1) Bool
    f SBool
    c SBool
    w1 SBool
    w2
    mergeWord f :: Bool
    f c :: SBool
    c (WordVal w1 :: SBool
    w1) (BitsVal ys :: Seq (Eval SBool)
    ys) =
        Seq (Eval SBool) -> WordValue SBool SBool SBool
    forall b w i. Seq (Eval b) -> WordValue b w i
    BitsVal (Seq (Eval SBool) -> WordValue SBool SBool SBool)
    -> Seq (Eval SBool) -> WordValue SBool SBool SBool
    forall a b. (a -> b) -> a -> b
    $ Bool
    -> SBool
    -> Seq (Eval SBool)
    -> Seq (Eval SBool)
    -> Seq (Eval SBool)
    mergeBits Bool
    f SBool
    c ([Eval SBool] -> Seq (Eval SBool)
    forall a. [a] -> Seq a
    Seq.fromList ([Eval SBool] -> Seq (Eval SBool))
    -> [Eval SBool] -> Seq (Eval SBool)
    forall a b. (a -> b) -> a -> b
    $ (SBool -> Eval SBool) -> [SBool] -> [Eval SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map SBool -> Eval SBool
    forall a. a -> Eval a
    ready ([SBool] -> [Eval SBool]) -> [SBool] -> [Eval SBool]
    forall a b. (a -> b) -> a -> b
    $ SBool -> [SBool]
    forall b w i. BitWord b w i => w -> [b]
    unpackWord SBool
    w1) Seq (Eval SBool)
    ys
    mergeWord f :: Bool
    f c :: SBool
    c (BitsVal xs :: Seq (Eval SBool)
    xs) (WordVal w2 :: SBool
    w2) =
        Seq (Eval SBool) -> WordValue SBool SBool SBool
    forall b w i. Seq (Eval b) -> WordValue b w i
    BitsVal (Seq (Eval SBool) -> WordValue SBool SBool SBool)
    -> Seq (Eval SBool) -> WordValue SBool SBool SBool
    forall a b. (a -> b) -> a -> b
    $ Bool
    -> SBool
    -> Seq (Eval SBool)
    -> Seq (Eval SBool)
    -> Seq (Eval SBool)
    mergeBits Bool
    f SBool
    c Seq (Eval SBool)
    xs ([Eval SBool] -> Seq (Eval SBool)
    forall a. [a] -> Seq a
    Seq.fromList ([Eval SBool] -> Seq (Eval SBool))
    -> [Eval SBool] -> Seq (Eval SBool)
    forall a b. (a -> b) -> a -> b
    $ (SBool -> Eval SBool) -> [SBool] -> [Eval SBool]
    forall a b. (a -> b) -> [a] -> [b]
    map SBool -> Eval SBool
    forall a. a -> Eval a
    ready ([SBool] -> [Eval SBool]) -> [SBool] -> [Eval SBool]
    forall a b. (a -> b) -> a -> b
    $ SBool -> [SBool]
    forall b w i. BitWord b w i => w -> [b]
    unpackWord SBool
    w2)
    mergeWord f :: Bool
    f c :: SBool
    c (BitsVal xs :: Seq (Eval SBool)
    xs) (BitsVal ys :: Seq (Eval SBool)
    ys) =
        Seq (Eval SBool) -> WordValue SBool SBool SBool
    forall b w i. Seq (Eval b) -> WordValue b w i
    BitsVal (Seq (Eval SBool) -> WordValue SBool SBool SBool)
    -> Seq (Eval SBool) -> WordValue SBool SBool SBool
    forall a b. (a -> b) -> a -> b
    $ Bool
    -> SBool
    -> Seq (Eval SBool)
    -> Seq (Eval SBool)
    -> Seq (Eval SBool)
    mergeBits Bool
    f SBool
    c Seq (Eval SBool)
    xs Seq (Eval SBool)
    ys
    mergeWord f :: Bool
    f c :: SBool
    c w1 :: WordValue SBool SBool SBool
    w1 w2 :: WordValue SBool SBool SBool
    w2 =
        Integer -> SeqMap SBool SBool SBool -> WordValue SBool SBool SBool
    forall b w i. Integer -> SeqMap b w i -> WordValue b w i
    LargeBitsVal (WordValue SBool SBool SBool -> Integer
    forall b w i. BitWord b w i => WordValue b w i -> Integer
    wordValueSize WordValue SBool SBool SBool
    w1) (Bool
    -> SBool
    -> SeqMap SBool SBool SBool
    -> SeqMap SBool SBool SBool
    -> SeqMap SBool SBool SBool
    mergeSeqMap Bool
    f SBool
    c (WordValue SBool SBool SBool -> SeqMap SBool SBool SBool
    forall b w i. BitWord b w i => WordValue b w i -> SeqMap b w i
    asBitsMap WordValue SBool SBool SBool
    w1) (WordValue SBool SBool SBool -> SeqMap SBool SBool SBool
    forall b w i. BitWord b w i => WordValue b w i -> SeqMap b w i
    asBitsMap WordValue SBool SBool SBool
    w2))

    mergeWord' :: Bool
               -> SBool
               -> Eval (WordValue SBool SWord SInteger)
               -> Eval (WordValue SBool SWord SInteger)
               -> Eval (WordValue SBool SWord SInteger)
    mergeWord' :: Bool
    -> SBool
    -> Eval (WordValue SBool SBool SBool)
    -> Eval (WordValue SBool SBool SBool)
    -> Eval (WordValue SBool SBool SBool)
    mergeWord' f :: Bool
    f c :: SBool
    c x :: Eval (WordValue SBool SBool SBool)
    x y :: Eval (WordValue SBool SBool SBool)
    y = Bool
    -> SBool
    -> WordValue SBool SBool SBool
    -> WordValue SBool SBool SBool
    -> WordValue SBool SBool SBool
    mergeWord Bool
    f SBool
    c (WordValue SBool SBool SBool
     -> WordValue SBool SBool SBool -> WordValue SBool SBool SBool)
    -> Eval (WordValue SBool SBool SBool)
    -> Eval
         (WordValue SBool SBool SBool -> WordValue SBool SBool SBool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval (WordValue SBool SBool SBool)
    x Eval (WordValue SBool SBool SBool -> WordValue SBool SBool SBool)
    -> Eval (WordValue SBool SBool SBool)
    -> Eval (WordValue SBool SBool SBool)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Eval (WordValue SBool SBool SBool)
    y

    mergeBits :: Bool
              -> SBool
              -> Seq.Seq (Eval SBool)
              -> Seq.Seq (Eval SBool)
              -> Seq.Seq (Eval SBool)
    mergeBits :: Bool
    -> SBool
    -> Seq (Eval SBool)
    -> Seq (Eval SBool)
    -> Seq (Eval SBool)
    mergeBits f :: Bool
    f c :: SBool
    c bs1 :: Seq (Eval SBool)
    bs1 bs2 :: Seq (Eval SBool)
    bs2 = (Eval SBool -> Eval SBool -> Eval SBool)
    -> Seq (Eval SBool) -> Seq (Eval SBool) -> Seq (Eval SBool)
    forall a b c. (a -> b -> c) -> Seq a -> Seq b -> Seq c
    Seq.zipWith Eval SBool -> Eval SBool -> Eval SBool
    forall (f :: * -> *).
    Applicative f =>
    f SBool -> f SBool -> f SBool
    mergeBit' Seq (Eval SBool)
    bs1 Seq (Eval SBool)
    bs2
     where mergeBit' :: f SBool -> f SBool -> f SBool
    mergeBit' b1 :: f SBool
    b1 b2 :: f SBool
    b2 = Bool -> SBool -> SBool -> SBool -> SBool
    mergeBit Bool
    f SBool
    c (SBool -> SBool -> SBool) -> f SBool -> f (SBool -> SBool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f SBool
    b1 f (SBool -> SBool) -> f SBool -> f SBool
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> f SBool
    b2

    mergeInteger :: Bool
                 -> SBool
                 -> SInteger
                 -> SInteger
                 -> SInteger
    mergeInteger :: Bool -> SBool -> SBool -> SBool -> SBool
    mergeInteger f :: Bool
    f c :: SBool
    c x :: SBool
    x y :: SBool
    y = Kind -> Bool -> SBool -> SBool -> SBool -> SBool
    svSymbolicMerge Kind
    KUnbounded Bool
    f SBool
    c SBool
    x SBool
    y

    mergeValue :: Bool -> SBool -> Value -> Value -> Eval Value
    mergeValue :: Bool -> SBool -> Value -> Value -> Eval Value
    mergeValue f :: Bool
    f c :: SBool
    c v1 :: Value
    v1 v2 :: Value
    v2 =
      case (Value
    v1, Value
    v2) of
        (VRecord fs1 :: [(Ident, Eval Value)]
    fs1, VRecord fs2 :: [(Ident, Eval Value)]
    fs2) -> Value -> Eval Value
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> Value -> Eval Value
    forall a b. (a -> b) -> a -> b
    $ [(Ident, Eval Value)] -> Value
    forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    VRecord ([(Ident, Eval Value)] -> Value) -> [(Ident, Eval Value)] -> Value
    forall a b. (a -> b) -> a -> b
    $ ((Ident, Eval Value) -> (Ident, Eval Value) -> (Ident, Eval Value))
    -> [(Ident, Eval Value)]
    -> [(Ident, Eval Value)]
    -> [(Ident, Eval Value)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (Ident, Eval Value) -> (Ident, Eval Value) -> (Ident, Eval Value)
    forall a.
    Eq a =>
    (a, Eval Value) -> (a, Eval Value) -> (a, Eval Value)
    mergeField [(Ident, Eval Value)]
    fs1 [(Ident, Eval Value)]
    fs2
        (VTuple vs1 :: [Eval Value]
    vs1 , VTuple vs2 :: [Eval Value]
    vs2 ) -> Value -> Eval Value
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> Value -> Eval Value
    forall a b. (a -> b) -> a -> b
    $ [Eval Value] -> Value
    forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
    VTuple ([Eval Value] -> Value) -> [Eval Value] -> Value
    forall a b. (a -> b) -> a -> b
    $ (Eval Value -> Eval Value -> Eval Value)
    -> [Eval Value] -> [Eval Value] -> [Eval Value]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (Bool -> SBool -> Eval Value -> Eval Value -> Eval Value
    mergeValue' Bool
    f SBool
    c) [Eval Value]
    vs1 [Eval Value]
    vs2
        (VBit b1 :: SBool
    b1    , VBit b2 :: SBool
    b2    ) -> Value -> Eval Value
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> Value -> Eval Value
    forall a b. (a -> b) -> a -> b
    $ SBool -> Value
    forall b w i. b -> GenValue b w i
    VBit (SBool -> Value) -> SBool -> Value
    forall a b. (a -> b) -> a -> b
    $ Bool -> SBool -> SBool -> SBool -> SBool
    mergeBit Bool
    f SBool
    c SBool
    b1 SBool
    b2
        (VInteger i1 :: SBool
    i1, VInteger i2 :: SBool
    i2) -> Value -> Eval Value
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> Value -> Eval Value
    forall a b. (a -> b) -> a -> b
    $ SBool -> Value
    forall b w i. i -> GenValue b w i
    VInteger (SBool -> Value) -> SBool -> Value
    forall a b. (a -> b) -> a -> b
    $ Bool -> SBool -> SBool -> SBool -> SBool
    mergeInteger Bool
    f SBool
    c SBool
    i1 SBool
    i2
        (VWord n1 :: Integer
    n1 w1 :: Eval (WordValue SBool SBool SBool)
    w1, VWord n2 :: Integer
    n2 w2 :: Eval (WordValue SBool SBool SBool)
    w2 ) | Integer
    n1 Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    n2 -> Value -> Eval Value
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> Value -> Eval Value
    forall a b. (a -> b) -> a -> b
    $ Integer -> Eval (WordValue SBool SBool SBool) -> Value
    forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
    VWord Integer
    n1 (Eval (WordValue SBool SBool SBool) -> Value)
    -> Eval (WordValue SBool SBool SBool) -> Value
    forall a b. (a -> b) -> a -> b
    $ Bool
    -> SBool
    -> Eval (WordValue SBool SBool SBool)
    -> Eval (WordValue SBool SBool SBool)
    -> Eval (WordValue SBool SBool SBool)
    mergeWord' Bool
    f SBool
    c Eval (WordValue SBool SBool SBool)
    w1 Eval (WordValue SBool SBool SBool)
    w2
        (VSeq n1 :: Integer
    n1 vs1 :: SeqMap SBool SBool SBool
    vs1, VSeq n2 :: Integer
    n2 vs2 :: SeqMap SBool SBool SBool
    vs2 ) | Integer
    n1 Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    n2 -> Integer -> SeqMap SBool SBool SBool -> Value
    forall b w i. Integer -> SeqMap b w i -> GenValue b w i
    VSeq Integer
    n1 (SeqMap SBool SBool SBool -> Value)
    -> Eval (SeqMap SBool SBool SBool) -> Eval Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool)
    forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
    memoMap (Bool
    -> SBool
    -> SeqMap SBool SBool SBool
    -> SeqMap SBool SBool SBool
    -> SeqMap SBool SBool SBool
    mergeSeqMap Bool
    f SBool
    c SeqMap SBool SBool SBool
    vs1 SeqMap SBool SBool SBool
    vs2)
        (VStream vs1 :: SeqMap SBool SBool SBool
    vs1, VStream vs2 :: SeqMap SBool SBool SBool
    vs2) -> SeqMap SBool SBool SBool -> Value
    forall b w i. SeqMap b w i -> GenValue b w i
    VStream (SeqMap SBool SBool SBool -> Value)
    -> Eval (SeqMap SBool SBool SBool) -> Eval Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool)
    forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
    memoMap (Bool
    -> SBool
    -> SeqMap SBool SBool SBool
    -> SeqMap SBool SBool SBool
    -> SeqMap SBool SBool SBool
    mergeSeqMap Bool
    f SBool
    c SeqMap SBool SBool SBool
    vs1 SeqMap SBool SBool SBool
    vs2)
        (VFun f1 :: Eval Value -> Eval Value
    f1    , VFun f2 :: Eval Value -> Eval Value
    f2    ) -> Value -> Eval Value
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> Value -> Eval Value
    forall a b. (a -> b) -> a -> b
    $ (Eval Value -> Eval Value) -> Value
    forall b w i.
    (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
    VFun ((Eval Value -> Eval Value) -> Value)
    -> (Eval Value -> Eval Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \x :: Eval Value
    x -> Bool -> SBool -> Eval Value -> Eval Value -> Eval Value
    mergeValue' Bool
    f SBool
    c (Eval Value -> Eval Value
    f1 Eval Value
    x) (Eval Value -> Eval Value
    f2 Eval Value
    x)
        (VPoly f1 :: TValue -> Eval Value
    f1   , VPoly f2 :: TValue -> Eval Value
    f2   ) -> Value -> Eval Value
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> Value -> Eval Value
    forall a b. (a -> b) -> a -> b
    $ (TValue -> Eval Value) -> Value
    forall b w i. (TValue -> Eval (GenValue b w i)) -> GenValue b w i
    VPoly ((TValue -> Eval Value) -> Value)
    -> (TValue -> Eval Value) -> Value
    forall a b. (a -> b) -> a -> b
    $ \x :: TValue
    x -> Bool -> SBool -> Eval Value -> Eval Value -> Eval Value
    mergeValue' Bool
    f SBool
    c (TValue -> Eval Value
    f1 TValue
    x) (TValue -> Eval Value
    f2 TValue
    x)
        (_          , _          ) -> String -> [String] -> Eval Value
    forall a. HasCallStack => String -> [String] -> a
    panic "Cryptol.Symbolic.Value"
                                      [ "mergeValue: incompatible values" ]
      where
        mergeField :: (a, Eval Value) -> (a, Eval Value) -> (a, Eval Value)
    mergeField (n1 :: a
    n1, x1 :: Eval Value
    x1) (n2 :: a
    n2, x2 :: Eval Value
    x2)
          | a
    n1 a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    n2  = (a
    n1, Bool -> SBool -> Eval Value -> Eval Value -> Eval Value
    mergeValue' Bool
    f SBool
    c Eval Value
    x1 Eval Value
    x2)
          | Bool
    otherwise = String -> [String] -> (a, Eval Value)
    forall a. HasCallStack => String -> [String] -> a
    panic "Cryptol.Symbolic.Value"
                        [ "mergeValue.mergeField: incompatible values" ]

    mergeValue' :: Bool -> SBool -> Eval Value -> Eval Value -> Eval Value
    mergeValue' :: Bool -> SBool -> Eval Value -> Eval Value -> Eval Value
    mergeValue' f :: Bool
    f c :: SBool
    c x1 :: Eval Value
    x1 x2 :: Eval Value
    x2 =
      do Value
    v1 <- Eval Value
    x1
         Value
    v2 <- Eval Value
    x2
         Bool -> SBool -> Value -> Value -> Eval Value
    mergeValue Bool
    f SBool
    c Value
    v1 Value
    v2

    mergeSeqMap :: Bool -> SBool -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger
    mergeSeqMap :: Bool
    -> SBool
    -> SeqMap SBool SBool SBool
    -> SeqMap SBool SBool SBool
    -> SeqMap SBool SBool SBool
    mergeSeqMap f :: Bool
    f c :: SBool
    c x :: SeqMap SBool SBool SBool
    x y :: SeqMap SBool SBool SBool
    y =
      (Integer -> Eval Value) -> SeqMap SBool SBool SBool
    forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    IndexSeqMap ((Integer -> Eval Value) -> SeqMap SBool SBool SBool)
    -> (Integer -> Eval Value) -> SeqMap SBool SBool SBool
    forall a b. (a -> b) -> a -> b
    $ \i :: Integer
    i ->
      do Value
    xi <- SeqMap SBool SBool SBool -> Integer -> Eval Value
    forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
    lookupSeqMap SeqMap SBool SBool SBool
    x Integer
    i
         Value
    yi <- SeqMap SBool SBool SBool -> Integer -> Eval Value
    forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
    lookupSeqMap SeqMap SBool SBool SBool
    y Integer
    i
         Bool -> SBool -> Value -> Value -> Eval Value
    mergeValue Bool
    f SBool
    c Value
    xi Value
    yi

    -- Symbolic Big-endian Words -------------------------------------------------------

    instance BitWord SBool SWord SInteger where
      wordLen :: SBool -> Integer
    wordLen v :: SBool
    v = Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (SBool -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SBool
    v)
      wordAsChar :: SBool -> Maybe Char
    wordAsChar v :: SBool
    v = Integer -> Char
    integerToChar (Integer -> Char) -> Maybe Integer -> Maybe Char
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SBool -> Maybe Integer
    svAsInteger SBool
    v

      ppBit :: SBool -> Doc
    ppBit v :: SBool
    v
         | Just b :: Bool
    b <- SBool -> Maybe Bool
    svAsBool SBool
    v = String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $! if Bool
    b then "True" else "False"
         | Bool
    otherwise            = String -> Doc
    text "?"
      ppWord :: PPOpts -> SBool -> Doc
    ppWord opts :: PPOpts
    opts v :: SBool
    v
         | Just x :: Integer
    x <- SBool -> Maybe Integer
    svAsInteger SBool
    v = PPOpts -> BV -> Doc
    ppBV PPOpts
    opts (Integer -> Integer -> BV
    BV (SBool -> Integer
    forall b w i. BitWord b w i => w -> Integer
    wordLen SBool
    v) Integer
    x)
         | Bool
    otherwise               = String -> Doc
    text "[?]"
      ppInteger :: PPOpts -> SBool -> Doc
    ppInteger _opts :: PPOpts
    _opts v :: SBool
    v
         | Just x :: Integer
    x <- SBool -> Maybe Integer
    svAsInteger SBool
    v = Integer -> Doc
    integer Integer
    x
         | Bool
    otherwise               = String -> Doc
    text "[?]"

      bitLit :: Bool -> SBool
    bitLit b :: Bool
    b    = Bool -> SBool
    svBool Bool
    b
      wordLit :: Integer -> Integer -> SBool
    wordLit n :: Integer
    n x :: Integer
    x = Kind -> Integer -> SBool
    svInteger (Bool -> Int -> Kind
    KBounded Bool
    False (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    n)) Integer
    x
      integerLit :: Integer -> SBool
    integerLit x :: Integer
    x = Kind -> Integer -> SBool
    svInteger Kind
    KUnbounded Integer
    x

      wordBit :: SBool -> Integer -> SBool
    wordBit x :: SBool
    x idx :: Integer
    idx = SBool -> Int -> SBool
    svTestBit SBool
    x (SBool -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SBool
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    idx)

      wordUpdate :: SBool -> Integer -> SBool -> SBool
    wordUpdate x :: SBool
    x idx :: Integer
    idx b :: SBool
    b = Kind -> Bool -> SBool -> SBool -> SBool -> SBool
    svSymbolicMerge (SBool -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBool
    x) Bool
    False SBool
    b SBool
    wtrue SBool
    wfalse
        where
         i' :: Int
    i' = SBool -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SBool
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    idx
         wtrue :: SBool
    wtrue  = SBool
    x SBool -> SBool -> SBool
    `svOr`  Kind -> Integer -> SBool
    svInteger (SBool -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBool
    x) (Int -> Integer
    forall a. Bits a => Int -> a
    bit Int
    i' :: Integer)
         wfalse :: SBool
    wfalse = SBool
    x SBool -> SBool -> SBool
    `svAnd` Kind -> Integer -> SBool
    svInteger (SBool -> Kind
    forall a. HasKind a => a -> Kind
    kindOf SBool
    x) (Integer -> Integer
    forall a. Bits a => a -> a
    complement (Int -> Integer
    forall a. Bits a => Int -> a
    bit Int
    i' :: Integer))

      packWord :: [SBool] -> SBool
    packWord bs :: [SBool]
    bs = [SBool] -> SBool
    fromBitsLE ([SBool] -> [SBool]
    forall a. [a] -> [a]
    reverse [SBool]
    bs)
      unpackWord :: SBool -> [SBool]
    unpackWord x :: SBool
    x = [ SBool -> Int -> SBool
    svTestBit SBool
    x Int
    i | Int
    i <- [Int] -> [Int]
    forall a. [a] -> [a]
    reverse [0 .. SBool -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SBool
    x Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1] ]

      joinWord :: SBool -> SBool -> SBool
    joinWord x :: SBool
    x y :: SBool
    y = SBool -> SBool -> SBool
    svJoin SBool
    x SBool
    y

      splitWord :: Integer -> Integer -> SBool -> (SBool, SBool)
    splitWord _leftW :: Integer
    _leftW rightW :: Integer
    rightW w :: SBool
    w =
        ( Int -> Int -> SBool -> SBool
    svExtract (SBool -> Int
    forall a. HasKind a => a -> Int
    intSizeOf SBool
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1) (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    rightW) SBool
    w
        , Int -> Int -> SBool -> SBool
    svExtract (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    rightW Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1) 0 SBool
    w
        )

      extractWord :: Integer -> Integer -> SBool -> SBool
    extractWord len :: Integer
    len start :: Integer
    start w :: SBool
    w =
        Int -> Int -> SBool -> SBool
    svExtract (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    start Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1) (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    start) SBool
    w

      wordPlus :: SBool -> SBool -> SBool
    wordPlus  = SBool -> SBool -> SBool
    svPlus
      wordMinus :: SBool -> SBool -> SBool
    wordMinus = SBool -> SBool -> SBool
    svMinus
      wordMult :: SBool -> SBool -> SBool
    wordMult  = SBool -> SBool -> SBool
    svTimes

      intPlus :: SBool -> SBool -> SBool
    intPlus  = SBool -> SBool -> SBool
    svPlus
      intMinus :: SBool -> SBool -> SBool
    intMinus = SBool -> SBool -> SBool
    svMinus
      intMult :: SBool -> SBool -> SBool
    intMult  = SBool -> SBool -> SBool
    svTimes

      intModPlus :: Integer -> SBool -> SBool -> SBool
    intModPlus  _m :: Integer
    _m = SBool -> SBool -> SBool
    svPlus
      intModMinus :: Integer -> SBool -> SBool -> SBool
    intModMinus _m :: Integer
    _m = SBool -> SBool -> SBool
    svMinus
      intModMult :: Integer -> SBool -> SBool -> SBool
    intModMult  _m :: Integer
    _m = SBool -> SBool -> SBool
    svTimes

      wordToInt :: SBool -> SBool
    wordToInt = SBool -> SBool
    svToInteger
      wordFromInt :: Integer -> SBool -> SBool
    wordFromInt = Integer -> SBool -> SBool
    svFromInteger

    -- TODO: implement this properly in SBV using "bv2int"
    svToInteger :: SWord -> SInteger
    svToInteger :: SBool -> SBool
    svToInteger w :: SBool
    w =
      case SBool -> Maybe Integer
    svAsInteger SBool
    w of
        Nothing -> Kind -> SBool -> SBool
    svFromIntegral Kind
    KUnbounded SBool
    w
        Just x :: Integer
    x  -> Kind -> Integer -> SBool
    svInteger Kind
    KUnbounded Integer
    x

    -- TODO: implement this properly in SBV using "int2bv"
    svFromInteger :: Integer -> SInteger -> SWord
    svFromInteger :: Integer -> SBool -> SBool
    svFromInteger 0 _ = Int -> Integer -> SBool
    literalSWord 0 0
    svFromInteger n :: Integer
    n i :: SBool
    i =
      case SBool -> Maybe Integer
    svAsInteger SBool
    i of
        Nothing -> Kind -> SBool -> SBool
    svFromIntegral (Bool -> Int -> Kind
    KBounded Bool
    False (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    n)) SBool
    i
        Just x :: Integer
    x  -> Int -> Integer -> SBool
    literalSWord (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    n) Integer
    x

    -- Errors ----------------------------------------------------------------------

    evalPanic :: String -> [String] -> a
    evalPanic :: String -> [String] -> a
    evalPanic cxt :: String
    cxt = String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    panic ("[Symbolic]" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cxt)