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

    {-# LANGUAGE BlockArguments #-}
    {-# LANGUAGE DeriveFunctor #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE MultiWayIf #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeSynonymInstances #-}
    {-# LANGUAGE ViewPatterns #-}
    module Cryptol.Eval.SBV
      ( primTable
      ) where

    import qualified Control.Exception as X
    import           Control.Monad.IO.Class (MonadIO(..))
    import qualified Data.Map as Map
    import qualified Data.Text as T

    import Data.SBV.Dynamic as SBV

    import Cryptol.Backend
    import Cryptol.Backend.Monad (Unsupported(..), EvalError(..) )
    import Cryptol.Backend.SBV
    import Cryptol.Backend.SeqMap
    import Cryptol.Backend.WordValue

    import Cryptol.Eval.Type (TValue(..))
    import Cryptol.Eval.Generic
    import Cryptol.Eval.Prims
    import Cryptol.Eval.Value
    import Cryptol.TypeCheck.Solver.InfNat (Nat'(..))
    import Cryptol.Utils.Ident

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

    type Value = GenValue SBV

    -- Primitives ------------------------------------------------------------------

    -- See also Cryptol.Eval.Concrete.primTable
    primTable :: SBV -> IO EvalOpts -> Map.Map PrimIdent (Prim SBV)
    primTable :: SBV -> IO EvalOpts -> Map PrimIdent (Prim SBV)
    primTable SBV
    sym IO EvalOpts
    getEOpts =
      Map PrimIdent (Prim SBV)
    -> Map PrimIdent (Prim SBV) -> Map PrimIdent (Prim SBV)
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (SBV -> IO EvalOpts -> Map PrimIdent (Prim SBV)
    forall sym.
    Backend sym =>
    sym -> IO EvalOpts -> Map PrimIdent (Prim sym)
    genericPrimTable SBV
    sym IO EvalOpts
    getEOpts) (Map PrimIdent (Prim SBV) -> Map PrimIdent (Prim SBV))
    -> Map PrimIdent (Prim SBV) -> Map PrimIdent (Prim SBV)
    forall a b. (a -> b) -> a -> b
    $
      [(PrimIdent, Prim SBV)] -> Map PrimIdent (Prim SBV)
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(PrimIdent, Prim SBV)] -> Map PrimIdent (Prim SBV))
    -> [(PrimIdent, Prim SBV)] -> Map PrimIdent (Prim SBV)
    forall a b. (a -> b) -> a -> b
    $ ((String, Prim SBV) -> (PrimIdent, Prim SBV))
    -> [(String, Prim SBV)] -> [(PrimIdent, Prim SBV)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(String
    n, Prim SBV
    v) -> (Text -> PrimIdent
    prelPrim (String -> Text
    T.pack String
    n), Prim SBV
    v))

      [ -- Indexing and updates
        (String
    "@"           , SBV
    -> IndexDirection
    -> (Nat'
        -> TValue
        -> SeqMap SBV (GenValue SBV)
        -> TValue
        -> SInteger SBV
        -> SEval SBV (GenValue SBV))
    -> (Nat'
        -> TValue
        -> SeqMap SBV (GenValue SBV)
        -> TValue
        -> Integer
        -> [IndexSegment SBV]
        -> SEval SBV (GenValue SBV))
    -> Prim SBV
    forall sym.
    Backend sym =>
    sym
    -> IndexDirection
    -> (Nat'
        -> TValue
        -> SeqMap sym (GenValue sym)
        -> TValue
        -> SInteger sym
        -> SEval sym (GenValue sym))
    -> (Nat'
        -> TValue
        -> SeqMap sym (GenValue sym)
        -> TValue
        -> Integer
        -> [IndexSegment sym]
        -> SEval sym (GenValue sym))
    -> Prim sym
    indexPrim SBV
    sym IndexDirection
    IndexForward  (SBV
    -> Nat'
    -> TValue
    -> SeqMap SBV (GenValue SBV)
    -> TValue
    -> SVal
    -> SEval SBV (GenValue SBV)
    indexFront SBV
    sym) (SBV
    -> Nat'
    -> TValue
    -> SeqMap SBV (GenValue SBV)
    -> TValue
    -> Integer
    -> [IndexSegment SBV]
    -> SEval SBV (GenValue SBV)
    indexFront_segs SBV
    sym))
      , (String
    "!"           , SBV
    -> IndexDirection
    -> (Nat'
        -> TValue
        -> SeqMap SBV (GenValue SBV)
        -> TValue
        -> SInteger SBV
        -> SEval SBV (GenValue SBV))
    -> (Nat'
        -> TValue
        -> SeqMap SBV (GenValue SBV)
        -> TValue
        -> Integer
        -> [IndexSegment SBV]
        -> SEval SBV (GenValue SBV))
    -> Prim SBV
    forall sym.
    Backend sym =>
    sym
    -> IndexDirection
    -> (Nat'
        -> TValue
        -> SeqMap sym (GenValue sym)
        -> TValue
        -> SInteger sym
        -> SEval sym (GenValue sym))
    -> (Nat'
        -> TValue
        -> SeqMap sym (GenValue sym)
        -> TValue
        -> Integer
        -> [IndexSegment sym]
        -> SEval sym (GenValue sym))
    -> Prim sym
    indexPrim SBV
    sym IndexDirection
    IndexBackward (SBV
    -> Nat'
    -> TValue
    -> SeqMap SBV (GenValue SBV)
    -> TValue
    -> SVal
    -> SEval SBV (GenValue SBV)
    indexFront SBV
    sym) (SBV
    -> Nat'
    -> TValue
    -> SeqMap SBV (GenValue SBV)
    -> TValue
    -> Integer
    -> [IndexSegment SBV]
    -> SEval SBV (GenValue SBV)
    indexFront_segs SBV
    sym))

      , (String
    "update"      , SBV
    -> (Nat'
        -> TValue
        -> WordValue SBV
        -> Either (SInteger SBV) (WordValue SBV)
        -> SEval SBV (GenValue SBV)
        -> SEval SBV (WordValue SBV))
    -> (Nat'
        -> TValue
        -> SeqMap SBV (GenValue SBV)
        -> Either (SInteger SBV) (WordValue SBV)
        -> SEval SBV (GenValue SBV)
        -> SEval SBV (SeqMap SBV (GenValue SBV)))
    -> Prim SBV
    forall sym.
    Backend sym =>
    sym
    -> (Nat'
        -> TValue
        -> WordValue sym
        -> Either (SInteger sym) (WordValue sym)
        -> SEval sym (GenValue sym)
        -> SEval sym (WordValue sym))
    -> (Nat'
        -> TValue
        -> SeqMap sym (GenValue sym)
        -> Either (SInteger sym) (WordValue sym)
        -> SEval sym (GenValue sym)
        -> SEval sym (SeqMap sym (GenValue sym)))
    -> Prim sym
    updatePrim SBV
    sym (SBV
    -> Nat'
    -> TValue
    -> WordValue SBV
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (WordValue SBV)
    updateFrontSym_word SBV
    sym) (SBV
    -> Nat'
    -> TValue
    -> SeqMap SBV (GenValue SBV)
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (SeqMap SBV (GenValue SBV))
    updateFrontSym SBV
    sym))
      , (String
    "updateEnd"   , SBV
    -> (Nat'
        -> TValue
        -> WordValue SBV
        -> Either (SInteger SBV) (WordValue SBV)
        -> SEval SBV (GenValue SBV)
        -> SEval SBV (WordValue SBV))
    -> (Nat'
        -> TValue
        -> SeqMap SBV (GenValue SBV)
        -> Either (SInteger SBV) (WordValue SBV)
        -> SEval SBV (GenValue SBV)
        -> SEval SBV (SeqMap SBV (GenValue SBV)))
    -> Prim SBV
    forall sym.
    Backend sym =>
    sym
    -> (Nat'
        -> TValue
        -> WordValue sym
        -> Either (SInteger sym) (WordValue sym)
        -> SEval sym (GenValue sym)
        -> SEval sym (WordValue sym))
    -> (Nat'
        -> TValue
        -> SeqMap sym (GenValue sym)
        -> Either (SInteger sym) (WordValue sym)
        -> SEval sym (GenValue sym)
        -> SEval sym (SeqMap sym (GenValue sym)))
    -> Prim sym
    updatePrim SBV
    sym (SBV
    -> Nat'
    -> TValue
    -> WordValue SBV
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (WordValue SBV)
    updateBackSym_word SBV
    sym) (SBV
    -> Nat'
    -> TValue
    -> SeqMap SBV (GenValue SBV)
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (SeqMap SBV (GenValue SBV))
    updateBackSym SBV
    sym))

      ]

    indexFront ::
      SBV ->
      Nat' ->
      TValue ->
      SeqMap SBV (GenValue SBV) ->
      TValue ->
      SVal ->
      SEval SBV Value
    indexFront :: SBV
    -> Nat'
    -> TValue
    -> SeqMap SBV (GenValue SBV)
    -> TValue
    -> SVal
    -> SEval SBV (GenValue SBV)
    indexFront SBV
    sym Nat'
    mblen TValue
    a SeqMap SBV (GenValue SBV)
    xs TValue
    _ix SVal
    idx
      | Just Integer
    i <- SVal -> Maybe Integer
    SBV.svAsInteger SVal
    idx
      = SeqMap SBV (GenValue SBV) -> Integer -> SEval SBV (GenValue SBV)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap SBV (GenValue SBV)
    xs Integer
    i

      | Nat Integer
    n <- Nat'
    mblen
      , TVSeq Integer
    wlen TValue
    TVBit <- TValue
    a
      = do [WordValue SBV]
    wvs <- (SBVEval (GenValue SBV) -> SBVEval (WordValue SBV))
    -> [SBVEval (GenValue SBV)] -> SBVEval [WordValue SBV]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse (String -> GenValue SBV -> WordValue SBV
    forall sym. Backend sym => String -> GenValue sym -> WordValue sym
    fromWordVal String
    "indexFront" (GenValue SBV -> WordValue SBV)
    -> SBVEval (GenValue SBV) -> SBVEval (WordValue SBV)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>) (Integer -> SeqMap SBV (GenValue SBV) -> [SEval SBV (GenValue SBV)]
    forall sym n a.
    (Backend sym, Integral n) =>
    n -> SeqMap sym a -> [SEval sym a]
    enumerateSeqMap Integer
    n SeqMap SBV (GenValue SBV)
    xs)
           SBV -> [WordValue SBV] -> SEval SBV (Maybe [SWord SBV])
    forall sym.
    Backend sym =>
    sym -> [WordValue sym] -> SEval sym (Maybe [SWord sym])
    asWordList SBV
    sym [WordValue SBV]
    wvs SBVEval (Maybe [SVal])
    -> (Maybe [SVal] -> SBVEval (GenValue SBV))
    -> SBVEval (GenValue SBV)
    forall a b. SBVEval a -> (a -> SBVEval b) -> SBVEval b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
             Just [SVal]
    ws ->
               do SVal
    z <- SBV -> Integer -> Integer -> SEval SBV (SWord SBV)
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> SEval sym (SWord sym)
    wordLit SBV
    sym Integer
    wlen Integer
    0
                  GenValue SBV -> SBVEval (GenValue SBV)
    forall a. a -> SBVEval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue SBV -> SBVEval (GenValue SBV))
    -> GenValue SBV -> SBVEval (GenValue SBV)
    forall a b. (a -> b) -> a -> b
    $ Integer -> WordValue SBV -> GenValue SBV
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    wlen (WordValue SBV -> GenValue SBV) -> WordValue SBV -> GenValue SBV
    forall a b. (a -> b) -> a -> b
    $ SWord SBV -> WordValue SBV
    forall sym. SWord sym -> WordValue sym
    wordVal (SWord SBV -> WordValue SBV) -> SWord SBV -> WordValue SBV
    forall a b. (a -> b) -> a -> b
    $ [SVal] -> SVal -> SVal -> SVal
    SBV.svSelect [SVal]
    ws SVal
    z SVal
    idx
             Maybe [SVal]
    Nothing -> SEval SBV (GenValue SBV)
    SBVEval (GenValue SBV)
    folded'

      | Bool
    otherwise = SEval SBV (GenValue SBV)
    folded'

     where
        k :: Kind
    k = SVal -> Kind
    forall a. HasKind a => a -> Kind
    SBV.kindOf SVal
    idx

        f :: Integer
    -> Maybe (SBVEval (GenValue SBV)) -> Maybe (SBVEval (GenValue SBV))
    f Integer
    n (Just SBVEval (GenValue SBV)
    y) = SBVEval (GenValue SBV) -> Maybe (SBVEval (GenValue SBV))
    forall a. a -> Maybe a
    Just (SBVEval (GenValue SBV) -> Maybe (SBVEval (GenValue SBV)))
    -> SBVEval (GenValue SBV) -> Maybe (SBVEval (GenValue SBV))
    forall a b. (a -> b) -> a -> b
    $ SBV
    -> SBit SBV
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (GenValue SBV)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    iteValue SBV
    sym (SVal -> SVal -> SVal
    SBV.svEqual SVal
    idx (Kind -> Integer -> SVal
    SBV.svInteger Kind
    k Integer
    n)) (SeqMap SBV (GenValue SBV) -> Integer -> SEval SBV (GenValue SBV)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap SBV (GenValue SBV)
    xs Integer
    n) SEval SBV (GenValue SBV)
    SBVEval (GenValue SBV)
    y
        f Integer
    n Maybe (SBVEval (GenValue SBV))
    Nothing  = SBVEval (GenValue SBV) -> Maybe (SBVEval (GenValue SBV))
    forall a. a -> Maybe a
    Just (SBVEval (GenValue SBV) -> Maybe (SBVEval (GenValue SBV)))
    -> SBVEval (GenValue SBV) -> Maybe (SBVEval (GenValue SBV))
    forall a b. (a -> b) -> a -> b
    $ SeqMap SBV (GenValue SBV) -> Integer -> SEval SBV (GenValue SBV)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap SBV (GenValue SBV)
    xs Integer
    n

        folded' :: SEval SBV (GenValue SBV)
    folded' =
          case Maybe (SBVEval (GenValue SBV))
    folded of
            Maybe (SBVEval (GenValue SBV))
    Nothing -> SBV -> EvalError -> SEval SBV (GenValue SBV)
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    forall a. SBV -> EvalError -> SEval SBV a
    raiseError SBV
    sym (Maybe Integer -> EvalError
    InvalidIndex Maybe Integer
    forall a. Maybe a
    Nothing)
            Just SBVEval (GenValue SBV)
    m  -> SEval SBV (GenValue SBV)
    SBVEval (GenValue SBV)
    m

        folded :: Maybe (SBVEval (GenValue SBV))
    folded =
          case Kind
    k of
            KBounded Bool
    _ Int
    w ->
              case Nat'
    mblen of
                Nat Integer
    n | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Int
    w -> (Integer
     -> Maybe (SBVEval (GenValue SBV))
     -> Maybe (SBVEval (GenValue SBV)))
    -> Maybe (SBVEval (GenValue SBV))
    -> [Integer]
    -> Maybe (SBVEval (GenValue SBV))
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Integer
    -> Maybe (SBVEval (GenValue SBV)) -> Maybe (SBVEval (GenValue SBV))
    f Maybe (SBVEval (GenValue SBV))
    forall a. Maybe a
    Nothing [Integer
    0 .. Integer
    nInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1]
                Nat'
    _ -> (Integer
     -> Maybe (SBVEval (GenValue SBV))
     -> Maybe (SBVEval (GenValue SBV)))
    -> Maybe (SBVEval (GenValue SBV))
    -> [Integer]
    -> Maybe (SBVEval (GenValue SBV))
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Integer
    -> Maybe (SBVEval (GenValue SBV)) -> Maybe (SBVEval (GenValue SBV))
    f Maybe (SBVEval (GenValue SBV))
    forall a. Maybe a
    Nothing [Integer
    0 .. Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Int
    w Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1]
            Kind
    _ ->
              case Nat'
    mblen of
                Nat Integer
    n -> (Integer
     -> Maybe (SBVEval (GenValue SBV))
     -> Maybe (SBVEval (GenValue SBV)))
    -> Maybe (SBVEval (GenValue SBV))
    -> [Integer]
    -> Maybe (SBVEval (GenValue SBV))
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Integer
    -> Maybe (SBVEval (GenValue SBV)) -> Maybe (SBVEval (GenValue SBV))
    f Maybe (SBVEval (GenValue SBV))
    forall a. Maybe a
    Nothing [Integer
    0 .. Integer
    nInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1]
                Nat'
    Inf -> SBVEval (GenValue SBV) -> Maybe (SBVEval (GenValue SBV))
    forall a. a -> Maybe a
    Just (IO (GenValue SBV) -> SBVEval (GenValue SBV)
    forall a. IO a -> SBVEval a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Unsupported -> IO (GenValue SBV)
    forall a e. Exception e => e -> a
    X.throw (String -> Unsupported
    UnsupportedSymbolicOp String
    "unbounded integer indexing")))

    indexFront_segs ::
      SBV ->
      Nat' ->
      TValue ->
      SeqMap SBV (GenValue SBV) ->
      TValue ->
      Integer ->
      [IndexSegment SBV] ->
      SEval SBV Value
    indexFront_segs :: SBV
    -> Nat'
    -> TValue
    -> SeqMap SBV (GenValue SBV)
    -> TValue
    -> Integer
    -> [IndexSegment SBV]
    -> SEval SBV (GenValue SBV)
    indexFront_segs SBV
    sym Nat'
    mblen TValue
    a SeqMap SBV (GenValue SBV)
    xs TValue
    ix Integer
    _idx_bits [WordIndexSegment SWord SBV
    w] =
      SBV
    -> Nat'
    -> TValue
    -> SeqMap SBV (GenValue SBV)
    -> TValue
    -> SVal
    -> SEval SBV (GenValue SBV)
    indexFront SBV
    sym Nat'
    mblen TValue
    a SeqMap SBV (GenValue SBV)
    xs TValue
    ix SVal
    SWord SBV
    w

    indexFront_segs SBV
    sym Nat'
    mblen TValue
    _a SeqMap SBV (GenValue SBV)
    xs TValue
    _ix Integer
    idx_bits [IndexSegment SBV]
    segs =
      do SeqMap SBV (GenValue SBV)
    xs' <- SBV
    -> (SBit SBV
        -> GenValue SBV -> GenValue SBV -> SEval SBV (GenValue SBV))
    -> (SeqMap SBV (GenValue SBV)
        -> Integer -> SEval SBV (SeqMap SBV (GenValue SBV)))
    -> Nat'
    -> SeqMap SBV (GenValue SBV)
    -> Integer
    -> [IndexSegment SBV]
    -> SEval SBV (SeqMap SBV (GenValue SBV))
    forall sym a.
    Backend sym =>
    sym
    -> (SBit sym -> a -> a -> SEval sym a)
    -> (SeqMap sym a -> Integer -> SEval sym (SeqMap sym a))
    -> Nat'
    -> SeqMap sym a
    -> Integer
    -> [IndexSegment sym]
    -> SEval sym (SeqMap sym a)
    barrelShifter SBV
    sym (SBV
    -> SBit SBV
    -> GenValue SBV
    -> GenValue SBV
    -> SEval SBV (GenValue SBV)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> GenValue sym
    -> GenValue sym
    -> SEval sym (GenValue sym)
    mergeValue SBV
    sym) SeqMap SBV (GenValue SBV)
    -> Integer -> SEval SBV (SeqMap SBV (GenValue SBV))
    SeqMap SBV (GenValue SBV)
    -> Integer -> SBVEval (SeqMap SBV (GenValue SBV))
    forall {sym} {sym} {f :: * -> *} {a}.
    (SEval sym ~ SEval sym, Backend sym, MonadIO (SEval sym),
     Applicative f) =>
    SeqMap sym a -> Integer -> f (SeqMap sym a)
    shiftOp Nat'
    mblen SeqMap SBV (GenValue SBV)
    xs Integer
    idx_bits [IndexSegment SBV]
    segs
         SeqMap SBV (GenValue SBV) -> Integer -> SEval SBV (GenValue SBV)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap SBV (GenValue SBV)
    xs' Integer
    0
      where
        shiftOp :: SeqMap sym a -> Integer -> f (SeqMap sym a)
    shiftOp SeqMap sym a
    vs Integer
    amt = SeqMap sym a -> f (SeqMap sym a)
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((Integer -> SEval sym a) -> SeqMap sym a
    forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
    indexSeqMap (\Integer
    i -> SeqMap sym a -> Integer -> SEval sym a
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap sym a
    vs (Integer -> SEval sym a) -> Integer -> SEval sym a
    forall a b. (a -> b) -> a -> b
    $! Integer
    amtInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    i))

    updateFrontSym ::
      SBV ->
      Nat' ->
      TValue ->
      SeqMap SBV (GenValue SBV) ->
      Either (SInteger SBV) (WordValue SBV) ->
      SEval SBV (GenValue SBV) ->
      SEval SBV (SeqMap SBV (GenValue SBV))
    updateFrontSym :: SBV
    -> Nat'
    -> TValue
    -> SeqMap SBV (GenValue SBV)
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (SeqMap SBV (GenValue SBV))
    updateFrontSym SBV
    sym Nat'
    _len TValue
    _eltTy SeqMap SBV (GenValue SBV)
    vs (Left SInteger SBV
    idx) SEval SBV (GenValue SBV)
    val =
      case SVal -> Maybe Integer
    SBV.svAsInteger SVal
    SInteger SBV
    idx of
        Just Integer
    i -> SeqMap SBV (GenValue SBV) -> SEval SBV (SeqMap SBV (GenValue SBV))
    forall a. a -> SEval SBV a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SeqMap SBV (GenValue SBV)
     -> SEval SBV (SeqMap SBV (GenValue SBV)))
    -> SeqMap SBV (GenValue SBV)
    -> SEval SBV (SeqMap SBV (GenValue SBV))
    forall a b. (a -> b) -> a -> b
    $ SeqMap SBV (GenValue SBV)
    -> Integer -> SEval SBV (GenValue SBV) -> SeqMap SBV (GenValue SBV)
    forall sym a.
    SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
    updateSeqMap SeqMap SBV (GenValue SBV)
    vs Integer
    i SEval SBV (GenValue SBV)
    val
        Maybe Integer
    Nothing -> SeqMap SBV (GenValue SBV) -> SEval SBV (SeqMap SBV (GenValue SBV))
    forall a. a -> SEval SBV a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SeqMap SBV (GenValue SBV)
     -> SEval SBV (SeqMap SBV (GenValue SBV)))
    -> SeqMap SBV (GenValue SBV)
    -> SEval SBV (SeqMap SBV (GenValue SBV))
    forall a b. (a -> b) -> a -> b
    $ (Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV (GenValue SBV)
    forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
    indexSeqMap ((Integer -> SEval SBV (GenValue SBV))
     -> SeqMap SBV (GenValue SBV))
    -> (Integer -> SEval SBV (GenValue SBV))
    -> SeqMap SBV (GenValue SBV)
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
          do SVal
    b <- SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    intEq SBV
    sym SInteger SBV
    idx (SVal -> SBVEval SVal) -> SBVEval SVal -> SBVEval SVal
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SBV -> Integer -> SEval SBV (SInteger SBV)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit SBV
    sym Integer
    i
             SBV
    -> SBit SBV
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (GenValue SBV)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    iteValue SBV
    sym SVal
    SBit SBV
    b SEval SBV (GenValue SBV)
    val (SeqMap SBV (GenValue SBV) -> Integer -> SEval SBV (GenValue SBV)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap SBV (GenValue SBV)
    vs Integer
    i)

    updateFrontSym SBV
    sym Nat'
    _len TValue
    _eltTy SeqMap SBV (GenValue SBV)
    vs (Right WordValue SBV
    wv) SEval SBV (GenValue SBV)
    val =
      SBV -> WordValue SBV -> SEval SBV (Maybe Integer)
    forall sym.
    Backend sym =>
    sym -> WordValue sym -> SEval sym (Maybe Integer)
    wordValAsLit SBV
    sym WordValue SBV
    wv SBVEval (Maybe Integer)
    -> (Maybe Integer -> SBVEval (SeqMap SBV (GenValue SBV)))
    -> SBVEval (SeqMap SBV (GenValue SBV))
    forall a b. SBVEval a -> (a -> SBVEval b) -> SBVEval b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
       Just Integer
    j -> SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV))
    forall a. a -> SBVEval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV)))
    -> SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV))
    forall a b. (a -> b) -> a -> b
    $ SeqMap SBV (GenValue SBV)
    -> Integer -> SEval SBV (GenValue SBV) -> SeqMap SBV (GenValue SBV)
    forall sym a.
    SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
    updateSeqMap SeqMap SBV (GenValue SBV)
    vs Integer
    j SEval SBV (GenValue SBV)
    val
       Maybe Integer
    Nothing ->
          SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV))
    forall a. a -> SBVEval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV)))
    -> SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV))
    forall a b. (a -> b) -> a -> b
    $ (Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV (GenValue SBV)
    forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
    indexSeqMap ((Integer -> SEval SBV (GenValue SBV))
     -> SeqMap SBV (GenValue SBV))
    -> (Integer -> SEval SBV (GenValue SBV))
    -> SeqMap SBV (GenValue SBV)
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
          do SVal
    b <- SBV -> WordValue SBV -> Integer -> SEval SBV (SBit SBV)
    forall sym.
    Backend sym =>
    sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
    wordValueEqualsInteger SBV
    sym WordValue SBV
    wv Integer
    i
             SBV
    -> SBit SBV
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (GenValue SBV)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    iteValue SBV
    sym SVal
    SBit SBV
    b SEval SBV (GenValue SBV)
    val (SeqMap SBV (GenValue SBV) -> Integer -> SEval SBV (GenValue SBV)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap SBV (GenValue SBV)
    vs Integer
    i)

    updateFrontSym_word ::
      SBV ->
      Nat' ->
      TValue ->
      WordValue SBV ->
      Either (SInteger SBV) (WordValue SBV) ->
      SEval SBV (GenValue SBV) ->
      SEval SBV (WordValue SBV)
    updateFrontSym_word :: SBV
    -> Nat'
    -> TValue
    -> WordValue SBV
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (WordValue SBV)
    updateFrontSym_word SBV
    _ Nat'
    Inf TValue
    _ WordValue SBV
    _ Either (SInteger SBV) (WordValue SBV)
    _ SEval SBV (GenValue SBV)
    _ = String -> [String] -> SBVEval (WordValue SBV)
    forall a. String -> [String] -> a
    evalPanic String
    "Expected finite sequence" [String
    "updateFrontSym_bits"]

    updateFrontSym_word SBV
    sym (Nat Integer
    n) TValue
    _eltTy WordValue SBV
    w (Left SInteger SBV
    idx) SEval SBV (GenValue SBV)
    val =
      do SVal
    idx' <- SBV -> Integer -> SInteger SBV -> SEval SBV (SWord SBV)
    forall sym.
    Backend sym =>
    sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
    wordFromInt SBV
    sym Integer
    n SInteger SBV
    idx
         SBV
    -> IndexDirection
    -> WordValue SBV
    -> WordValue SBV
    -> SEval SBV (SBit SBV)
    -> SEval SBV (WordValue SBV)
    forall sym.
    Backend sym =>
    sym
    -> IndexDirection
    -> WordValue sym
    -> WordValue sym
    -> SEval sym (SBit sym)
    -> SEval sym (WordValue sym)
    updateWordByWord SBV
    sym IndexDirection
    IndexForward WordValue SBV
    w (SWord SBV -> WordValue SBV
    forall sym. SWord sym -> WordValue sym
    wordVal SVal
    SWord SBV
    idx') (GenValue SBV -> SVal
    GenValue SBV -> SBit SBV
    forall sym. GenValue sym -> SBit sym
    fromVBit (GenValue SBV -> SVal) -> SBVEval (GenValue SBV) -> SBVEval SVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SEval SBV (GenValue SBV)
    SBVEval (GenValue SBV)
    val)
    updateFrontSym_word SBV
    sym (Nat Integer
    _n) TValue
    _eltTy WordValue SBV
    w (Right WordValue SBV
    idx) SEval SBV (GenValue SBV)
    val =
      SBV
    -> IndexDirection
    -> WordValue SBV
    -> WordValue SBV
    -> SEval SBV (SBit SBV)
    -> SEval SBV (WordValue SBV)
    forall sym.
    Backend sym =>
    sym
    -> IndexDirection
    -> WordValue sym
    -> WordValue sym
    -> SEval sym (SBit sym)
    -> SEval sym (WordValue sym)
    updateWordByWord SBV
    sym IndexDirection
    IndexForward WordValue SBV
    w WordValue SBV
    idx (GenValue SBV -> SVal
    GenValue SBV -> SBit SBV
    forall sym. GenValue sym -> SBit sym
    fromVBit (GenValue SBV -> SVal) -> SBVEval (GenValue SBV) -> SBVEval SVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SEval SBV (GenValue SBV)
    SBVEval (GenValue SBV)
    val)

    updateBackSym ::
      SBV ->
      Nat' ->
      TValue ->
      SeqMap SBV (GenValue SBV) ->
      Either (SInteger SBV) (WordValue SBV) ->
      SEval SBV (GenValue SBV) ->
      SEval SBV (SeqMap SBV (GenValue SBV))
    updateBackSym :: SBV
    -> Nat'
    -> TValue
    -> SeqMap SBV (GenValue SBV)
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (SeqMap SBV (GenValue SBV))
    updateBackSym SBV
    _ Nat'
    Inf TValue
    _ SeqMap SBV (GenValue SBV)
    _ Either (SInteger SBV) (WordValue SBV)
    _ SEval SBV (GenValue SBV)
    _ = String -> [String] -> SBVEval (SeqMap SBV (GenValue SBV))
    forall a. String -> [String] -> a
    evalPanic String
    "Expected finite sequence" [String
    "updateBackSym"]

    updateBackSym SBV
    sym (Nat Integer
    n) TValue
    _eltTy SeqMap SBV (GenValue SBV)
    vs (Left SInteger SBV
    idx) SEval SBV (GenValue SBV)
    val =
      case SVal -> Maybe Integer
    SBV.svAsInteger SVal
    SInteger SBV
    idx of
        Just Integer
    i -> SeqMap SBV (GenValue SBV) -> SEval SBV (SeqMap SBV (GenValue SBV))
    forall a. a -> SEval SBV a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SeqMap SBV (GenValue SBV)
     -> SEval SBV (SeqMap SBV (GenValue SBV)))
    -> SeqMap SBV (GenValue SBV)
    -> SEval SBV (SeqMap SBV (GenValue SBV))
    forall a b. (a -> b) -> a -> b
    $ SeqMap SBV (GenValue SBV)
    -> Integer -> SEval SBV (GenValue SBV) -> SeqMap SBV (GenValue SBV)
    forall sym a.
    SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
    updateSeqMap SeqMap SBV (GenValue SBV)
    vs (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    i) SEval SBV (GenValue SBV)
    val
        Maybe Integer
    Nothing -> SeqMap SBV (GenValue SBV) -> SEval SBV (SeqMap SBV (GenValue SBV))
    forall a. a -> SEval SBV a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SeqMap SBV (GenValue SBV)
     -> SEval SBV (SeqMap SBV (GenValue SBV)))
    -> SeqMap SBV (GenValue SBV)
    -> SEval SBV (SeqMap SBV (GenValue SBV))
    forall a b. (a -> b) -> a -> b
    $ (Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV (GenValue SBV)
    forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
    indexSeqMap ((Integer -> SEval SBV (GenValue SBV))
     -> SeqMap SBV (GenValue SBV))
    -> (Integer -> SEval SBV (GenValue SBV))
    -> SeqMap SBV (GenValue SBV)
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
          do SVal
    b <- SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    intEq SBV
    sym SInteger SBV
    idx (SVal -> SBVEval SVal) -> SBVEval SVal -> SBVEval SVal
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SBV -> Integer -> SEval SBV (SInteger SBV)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit SBV
    sym (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    i)
             SBV
    -> SBit SBV
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (GenValue SBV)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    iteValue SBV
    sym SVal
    SBit SBV
    b SEval SBV (GenValue SBV)
    val (SeqMap SBV (GenValue SBV) -> Integer -> SEval SBV (GenValue SBV)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap SBV (GenValue SBV)
    vs Integer
    i)

    updateBackSym SBV
    sym (Nat Integer
    n) TValue
    _eltTy SeqMap SBV (GenValue SBV)
    vs (Right WordValue SBV
    wv) SEval SBV (GenValue SBV)
    val =
      SBV -> WordValue SBV -> SEval SBV (Maybe Integer)
    forall sym.
    Backend sym =>
    sym -> WordValue sym -> SEval sym (Maybe Integer)
    wordValAsLit SBV
    sym WordValue SBV
    wv SBVEval (Maybe Integer)
    -> (Maybe Integer -> SBVEval (SeqMap SBV (GenValue SBV)))
    -> SBVEval (SeqMap SBV (GenValue SBV))
    forall a b. SBVEval a -> (a -> SBVEval b) -> SBVEval b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just Integer
    j -> SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV))
    forall a. a -> SBVEval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV)))
    -> SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV))
    forall a b. (a -> b) -> a -> b
    $ SeqMap SBV (GenValue SBV)
    -> Integer -> SEval SBV (GenValue SBV) -> SeqMap SBV (GenValue SBV)
    forall sym a.
    SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
    updateSeqMap SeqMap SBV (GenValue SBV)
    vs (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    j) SEval SBV (GenValue SBV)
    val
        Maybe Integer
    Nothing ->
          SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV))
    forall a. a -> SBVEval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV)))
    -> SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV))
    forall a b. (a -> b) -> a -> b
    $ (Integer -> SEval SBV (GenValue SBV)) -> SeqMap SBV (GenValue SBV)
    forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
    indexSeqMap ((Integer -> SEval SBV (GenValue SBV))
     -> SeqMap SBV (GenValue SBV))
    -> (Integer -> SEval SBV (GenValue SBV))
    -> SeqMap SBV (GenValue SBV)
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i ->
          do SVal
    b <- SBV -> WordValue SBV -> Integer -> SEval SBV (SBit SBV)
    forall sym.
    Backend sym =>
    sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
    wordValueEqualsInteger SBV
    sym WordValue SBV
    wv (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    i)
             SBV
    -> SBit SBV
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (GenValue SBV)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    iteValue SBV
    sym SVal
    SBit SBV
    b SEval SBV (GenValue SBV)
    val (SeqMap SBV (GenValue SBV) -> Integer -> SEval SBV (GenValue SBV)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap SBV (GenValue SBV)
    vs Integer
    i)

    updateBackSym_word ::
      SBV ->
      Nat' ->
      TValue ->
      WordValue SBV ->
      Either (SInteger SBV) (WordValue SBV) ->
      SEval SBV (GenValue SBV) ->
      SEval SBV (WordValue SBV)
    updateBackSym_word :: SBV
    -> Nat'
    -> TValue
    -> WordValue SBV
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV (GenValue SBV)
    -> SEval SBV (WordValue SBV)
    updateBackSym_word SBV
    _ Nat'
    Inf TValue
    _ WordValue SBV
    _ Either (SInteger SBV) (WordValue SBV)
    _ SEval SBV (GenValue SBV)
    _ = String -> [String] -> SBVEval (WordValue SBV)
    forall a. String -> [String] -> a
    evalPanic String
    "Expected finite sequence" [String
    "updateBackSym_bits"]

    updateBackSym_word SBV
    sym (Nat Integer
    n) TValue
    _eltTy WordValue SBV
    w (Left SInteger SBV
    idx) SEval SBV (GenValue SBV)
    val =
      do SVal
    idx' <- SBV -> Integer -> SInteger SBV -> SEval SBV (SWord SBV)
    forall sym.
    Backend sym =>
    sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
    wordFromInt SBV
    sym Integer
    n SInteger SBV
    idx
         SBV
    -> IndexDirection
    -> WordValue SBV
    -> WordValue SBV
    -> SEval SBV (SBit SBV)
    -> SEval SBV (WordValue SBV)
    forall sym.
    Backend sym =>
    sym
    -> IndexDirection
    -> WordValue sym
    -> WordValue sym
    -> SEval sym (SBit sym)
    -> SEval sym (WordValue sym)
    updateWordByWord SBV
    sym IndexDirection
    IndexBackward WordValue SBV
    w (SWord SBV -> WordValue SBV
    forall sym. SWord sym -> WordValue sym
    wordVal SVal
    SWord SBV
    idx') (GenValue SBV -> SVal
    GenValue SBV -> SBit SBV
    forall sym. GenValue sym -> SBit sym
    fromVBit (GenValue SBV -> SVal) -> SBVEval (GenValue SBV) -> SBVEval SVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SEval SBV (GenValue SBV)
    SBVEval (GenValue SBV)
    val)
    updateBackSym_word SBV
    sym (Nat Integer
    _n) TValue
    _eltTy WordValue SBV
    w (Right WordValue SBV
    idx) SEval SBV (GenValue SBV)
    val =
      SBV
    -> IndexDirection
    -> WordValue SBV
    -> WordValue SBV
    -> SEval SBV (SBit SBV)
    -> SEval SBV (WordValue SBV)
    forall sym.
    Backend sym =>
    sym
    -> IndexDirection
    -> WordValue sym
    -> WordValue sym
    -> SEval sym (SBit sym)
    -> SEval sym (WordValue sym)
    updateWordByWord SBV
    sym IndexDirection
    IndexBackward WordValue SBV
    w WordValue SBV
    idx (GenValue SBV -> SVal
    GenValue SBV -> SBit SBV
    forall sym. GenValue sym -> SBit sym
    fromVBit (GenValue SBV -> SVal) -> SBVEval (GenValue SBV) -> SBVEval SVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SEval SBV (GenValue SBV)
    SBVEval (GenValue SBV)
    val)