-- |
-- 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 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)
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 (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 (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 -> SBVEval (GenValue SBV)
folded'

  | Bool
otherwise = SEval SBV (GenValue SBV)
SBVEval (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' :: SBVEval (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
raiseError SBV
sym (Maybe Integer -> EvalError
InvalidIndex Maybe Integer
forall a. Maybe a
Nothing)
        Just SBVEval (GenValue SBV)
m  -> 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 (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 (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 (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 (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))
forall sym (f :: * -> *) sym a.
(Backend sym, Applicative f, SEval sym ~ SEval sym) =>
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 (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) -> SBVEval (SeqMap SBV (GenValue SBV))
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
i SEval SBV (GenValue SBV)
val
    Maybe Integer
Nothing -> SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV))
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 -> 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 (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 (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 (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
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
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) -> SBVEval (SeqMap SBV (GenValue SBV))
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
i) SEval SBV (GenValue SBV)
val
    Maybe Integer
Nothing -> SeqMap SBV (GenValue SBV) -> SBVEval (SeqMap SBV (GenValue SBV))
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 -> 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 (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 (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 (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
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
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)