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

{-# 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 (join)
import           Control.Monad.IO.Class (MonadIO(..))
import           Data.Bits (bit, shiftL)
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 ( EvalError(..), Unsupported(..) )
import Cryptol.Backend.SBV

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

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

type Value = GenValue SBV

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

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

  [ -- Literals
    (String
"True"        , SBit SBV -> Value
forall sym. SBit sym -> GenValue sym
VBit (SBV -> Bool -> SBit SBV
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit SBV
sym Bool
True))
  , (String
"False"       , SBit SBV -> Value
forall sym. SBit sym -> GenValue sym
VBit (SBV -> Bool -> SBit SBV
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit SBV
sym Bool
False))
  , (String
"number"      , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
ecNumberV SBV
sym) -- Converts a numeric type into its corresponding value.
                                    -- { val, rep } (Literal val rep) => rep
  , (String
"fraction"     , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
ecFractionV SBV
sym)
  , (String
"ratio"       , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
ratioV SBV
sym)

    -- Zero
  , (String
"zero"        , (TValue -> SEval SBV Value) -> Value
forall sym. (TValue -> SEval sym (GenValue sym)) -> GenValue sym
VPoly (SBV -> TValue -> SEval SBV Value
forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV SBV
sym))

    -- Logic
  , (String
"&&"          , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
andV SBV
sym))
  , (String
"||"          , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
orV SBV
sym))
  , (String
"^"           , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
xorV SBV
sym))
  , (String
"complement"  , Unary SBV -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary  (SBV -> Unary SBV
forall sym. Backend sym => sym -> Unary sym
complementV SBV
sym))

    -- Ring
  , (String
"fromInteger" , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
fromIntegerV SBV
sym)
  , (String
"+"           , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
addV SBV
sym))
  , (String
"-"           , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
subV SBV
sym))
  , (String
"negate"      , Unary SBV -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary (SBV -> Unary SBV
forall sym. Backend sym => sym -> Unary sym
negateV SBV
sym))
  , (String
"*"           , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
mulV SBV
sym))

    -- Integral
  , (String
"toInteger"   , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
toIntegerV SBV
sym)
  , (String
"/"           , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
divV SBV
sym))
  , (String
"%"           , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
modV SBV
sym))
  , (String
"^^"          , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
expV SBV
sym)
  , (String
"infFrom"     , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
infFromV SBV
sym)
  , (String
"infFromThen" , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
infFromThenV SBV
sym)

    -- Field
  , (String
"recip"       , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
recipV SBV
sym)
  , (String
"/."          , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
fieldDivideV SBV
sym)

    -- Round
  , (String
"floor"       , Unary SBV -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary (SBV -> Unary SBV
forall sym. Backend sym => sym -> Unary sym
floorV SBV
sym))
  , (String
"ceiling"     , Unary SBV -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary (SBV -> Unary SBV
forall sym. Backend sym => sym -> Unary sym
ceilingV SBV
sym))
  , (String
"trunc"       , Unary SBV -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary (SBV -> Unary SBV
forall sym. Backend sym => sym -> Unary sym
truncV SBV
sym))
  , (String
"roundAway"   , Unary SBV -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary (SBV -> Unary SBV
forall sym. Backend sym => sym -> Unary sym
roundAwayV SBV
sym))
  , (String
"roundToEven" , Unary SBV -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary (SBV -> Unary SBV
forall sym. Backend sym => sym -> Unary sym
roundToEvenV SBV
sym))

    -- Word operations
  , (String
"/$"          , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
sdivV SBV
sym)
  , (String
"%$"          , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
smodV SBV
sym)
  , (String
"lg2"         , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
lg2V SBV
sym)
  , (String
">>$"         , SBV -> Value
sshrV SBV
sym)

    -- Cmp
  , (String
"<"           , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
lessThanV SBV
sym))
  , (String
">"           , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
greaterThanV SBV
sym))
  , (String
"<="          , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
lessThanEqV SBV
sym))
  , (String
">="          , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
greaterThanEqV SBV
sym))
  , (String
"=="          , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
eqV SBV
sym))
  , (String
"!="          , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
distinctV SBV
sym))

    -- SignedCmp
  , (String
"<$"          , Binary SBV -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (SBV -> Binary SBV
forall sym. Backend sym => sym -> Binary sym
signedLessThanV SBV
sym))

    -- Finite enumerations
  , (String
"fromTo"      , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
fromToV SBV
sym)
  , (String
"fromThenTo"  , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
fromThenToV SBV
sym)

    -- Sequence manipulations
  , (String
"#"          , -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d
     (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ Nat'
front ->
     (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ Nat'
back  ->
     (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ TValue
elty  ->
     (SEval SBV Value -> SEval SBV Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam  ((SEval SBV Value -> SEval SBV Value) -> Value)
-> (SEval SBV Value -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ SEval SBV Value
l     -> Value -> SBVEval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> SBVEval Value) -> Value -> SBVEval Value
forall a b. (a -> b) -> a -> b
$
     (SEval SBV Value -> SEval SBV Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam  ((SEval SBV Value -> SEval SBV Value) -> Value)
-> (SEval SBV Value -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ SEval SBV Value
r     -> SBVEval (SBVEval Value) -> SBVEval Value
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (SBV -> Nat' -> Nat' -> Binary SBV
forall sym.
Backend sym =>
sym
-> Nat'
-> Nat'
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
ccatV SBV
sym Nat'
front Nat'
back TValue
elty (Value -> Value -> SBVEval Value)
-> SBVEval Value -> SBVEval (Value -> SBVEval Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval SBV Value
SBVEval Value
l SBVEval (Value -> SBVEval Value)
-> SBVEval Value -> SBVEval (SBVEval Value)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SEval SBV Value
SBVEval Value
r))

  , (String
"join"       ,
     (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ Nat'
parts ->
     (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ (Nat' -> Integer
finNat' -> Integer
each)  ->
     (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ TValue
a     ->
     (SEval SBV Value -> SEval SBV Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam  ((SEval SBV Value -> SEval SBV Value) -> Value)
-> (SEval SBV Value -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ SEval SBV Value
x     ->
       SBV -> Nat' -> Integer -> Unary SBV
forall sym.
Backend sym =>
sym
-> Nat'
-> Integer
-> TValue
-> GenValue sym
-> SEval sym (GenValue sym)
joinV SBV
sym Nat'
parts Integer
each TValue
a (Value -> SBVEval Value) -> SBVEval Value -> SBVEval Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval SBV Value
SBVEval Value
x)

  , (String
"split"       , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
ecSplitV SBV
sym)

  , (String
"splitAt"    ,
     (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ Nat'
front ->
     (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ Nat'
back  ->
     (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ TValue
a     ->
     (SEval SBV Value -> SEval SBV Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam  ((SEval SBV Value -> SEval SBV Value) -> Value)
-> (SEval SBV Value -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ SEval SBV Value
x     ->
       SBV -> Nat' -> Nat' -> Unary SBV
forall sym.
Backend sym =>
sym
-> Nat'
-> Nat'
-> TValue
-> GenValue sym
-> SEval sym (GenValue sym)
splitAtV SBV
sym Nat'
front Nat'
back TValue
a (Value -> SBVEval Value) -> SBVEval Value -> SBVEval Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval SBV Value
SBVEval Value
x)

  , (String
"reverse"    , (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Nat'
_a ->
                    (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
_b ->
                     (SEval SBV Value -> SEval SBV Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval SBV Value -> SEval SBV Value) -> Value)
-> (SEval SBV Value -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval SBV Value
xs -> SBV -> Value -> SEval SBV Value
forall sym.
Backend sym =>
sym -> GenValue sym -> SEval sym (GenValue sym)
reverseV SBV
sym (Value -> SBVEval Value) -> SBVEval Value -> SBVEval Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval SBV Value
SBVEval Value
xs)

  , (String
"transpose"  , (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Nat'
a ->
                    (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Nat'
b ->
                    (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
c ->
                     (SEval SBV Value -> SEval SBV Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval SBV Value -> SEval SBV Value) -> Value)
-> (SEval SBV Value -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval SBV Value
xs -> SBV -> Nat' -> Nat' -> Unary SBV
forall sym.
Backend sym =>
sym
-> Nat'
-> Nat'
-> TValue
-> GenValue sym
-> SEval sym (GenValue sym)
transposeV SBV
sym Nat'
a Nat'
b TValue
c (Value -> SBVEval Value) -> SBVEval Value -> SBVEval Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval SBV Value
SBVEval Value
xs)

    -- Shifts and rotates
  , (String
"<<"          , SBV
-> String
-> (SBV
    -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Value
forall sym.
Backend sym =>
sym
-> String
-> (sym
    -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> GenValue sym
logicShift SBV
sym String
"<<"
                       SBV -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
shl SVal
SWord SBV
x SVal
SWord SBV
y))
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
lshr SVal
SWord SBV
x SVal
SWord SBV
y))
                       Nat' -> Integer -> Integer -> Maybe Integer
shiftLeftReindex Nat' -> Integer -> Integer -> Maybe Integer
shiftRightReindex)

  , (String
">>"          , SBV
-> String
-> (SBV
    -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Value
forall sym.
Backend sym =>
sym
-> String
-> (sym
    -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> GenValue sym
logicShift SBV
sym String
">>"
                       SBV -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
lshr SVal
SWord SBV
x SVal
SWord SBV
y))
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
shl SVal
SWord SBV
x SVal
SWord SBV
y))
                       Nat' -> Integer -> Integer -> Maybe Integer
shiftRightReindex Nat' -> Integer -> Integer -> Maybe Integer
shiftLeftReindex)

  , (String
"<<<"         , SBV
-> String
-> (SBV
    -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Value
forall sym.
Backend sym =>
sym
-> String
-> (sym
    -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> GenValue sym
logicShift SBV
sym String
"<<<"
                       SBV -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
rotateShrink
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
SBV.svRotateLeft SVal
SWord SBV
x SVal
SWord SBV
y))
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
SBV.svRotateRight SVal
SWord SBV
x SVal
SWord SBV
y))
                       Nat' -> Integer -> Integer -> Maybe Integer
rotateLeftReindex Nat' -> Integer -> Integer -> Maybe Integer
rotateRightReindex)

  , (String
">>>"         , SBV
-> String
-> (SBV
    -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (SWord SBV -> SWord SBV -> SEval SBV (SWord SBV))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Value
forall sym.
Backend sym =>
sym
-> String
-> (sym
    -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> GenValue sym
logicShift SBV
sym String
">>>"
                       SBV -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
rotateShrink
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
SBV.svRotateRight SVal
SWord SBV
x SVal
SWord SBV
y))
                       (\SWord SBV
x SWord SBV
y -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SVal -> SVal
SBV.svRotateLeft SVal
SWord SBV
x SVal
SWord SBV
y))
                       Nat' -> Integer -> Integer -> Maybe Integer
rotateRightReindex Nat' -> Integer -> Integer -> Maybe Integer
rotateLeftReindex)

    -- Indexing and updates
  , (String
"@"           , SBV
-> (Nat'
    -> TValue
    -> SeqMap SBV
    -> TValue
    -> SInteger SBV
    -> SEval SBV Value)
-> (Nat'
    -> TValue -> SeqMap SBV -> TValue -> [SBit SBV] -> SEval SBV Value)
-> (Nat'
    -> TValue -> SeqMap SBV -> TValue -> SWord SBV -> SEval SBV Value)
-> Value
forall sym.
Backend sym =>
sym
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> SInteger sym
    -> SEval sym (GenValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> [SBit sym]
    -> SEval sym (GenValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> SWord sym
    -> SEval sym (GenValue sym))
-> GenValue sym
indexPrim SBV
sym (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> SVal
-> SEval SBV Value
indexFront SBV
sym) (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> [SBit SBV]
-> SEval SBV Value
indexFront_bits SBV
sym) (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> SVal
-> SEval SBV Value
indexFront SBV
sym))
  , (String
"!"           , SBV
-> (Nat'
    -> TValue
    -> SeqMap SBV
    -> TValue
    -> SInteger SBV
    -> SEval SBV Value)
-> (Nat'
    -> TValue -> SeqMap SBV -> TValue -> [SBit SBV] -> SEval SBV Value)
-> (Nat'
    -> TValue -> SeqMap SBV -> TValue -> SWord SBV -> SEval SBV Value)
-> Value
forall sym.
Backend sym =>
sym
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> SInteger sym
    -> SEval sym (GenValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> [SBit sym]
    -> SEval sym (GenValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> SWord sym
    -> SEval sym (GenValue sym))
-> GenValue sym
indexPrim SBV
sym (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> SWord SBV
-> SEval SBV Value
indexBack SBV
sym) (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> [SBit SBV]
-> SEval SBV Value
indexBack_bits SBV
sym) (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> SWord SBV
-> SEval SBV Value
indexBack SBV
sym))

  , (String
"update"      , SBV
-> (Nat'
    -> TValue
    -> WordValue SBV
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV Value
    -> SEval SBV (WordValue SBV))
-> (Nat'
    -> TValue
    -> SeqMap SBV
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV Value
    -> SEval SBV (SeqMap SBV))
-> Value
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
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (SeqMap sym))
-> GenValue sym
updatePrim SBV
sym (SBV
-> Nat'
-> TValue
-> WordValue SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV Value
-> SEval SBV (WordValue SBV)
updateFrontSym_word SBV
sym) (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV Value
-> SEval SBV (SeqMap SBV)
updateFrontSym SBV
sym))
  , (String
"updateEnd"   , SBV
-> (Nat'
    -> TValue
    -> WordValue SBV
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV Value
    -> SEval SBV (WordValue SBV))
-> (Nat'
    -> TValue
    -> SeqMap SBV
    -> Either (SInteger SBV) (WordValue SBV)
    -> SEval SBV Value
    -> SEval SBV (SeqMap SBV))
-> Value
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
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (SeqMap sym))
-> GenValue sym
updatePrim SBV
sym (SBV
-> Nat'
-> TValue
-> WordValue SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV Value
-> SEval SBV (WordValue SBV)
updateBackSym_word SBV
sym) (SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV Value
-> SEval SBV (SeqMap SBV)
updateBackSym SBV
sym))

    -- Misc

  , (String
"fromZ"       , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
fromZV SBV
sym)

  , (String
"foldl"       , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
foldlV SBV
sym)
  , (String
"foldl'"      , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
foldl'V SBV
sym)

  , (String
"deepseq"     ,
      (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
_a ->
      (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
_b ->
       (SEval SBV Value -> SEval SBV Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval SBV Value -> SEval SBV Value) -> Value)
-> (SEval SBV Value -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval SBV Value
x -> Value -> SBVEval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> SBVEval Value) -> Value -> SBVEval Value
forall a b. (a -> b) -> a -> b
$
       (SEval SBV Value -> SEval SBV Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval SBV Value -> SEval SBV Value) -> Value)
-> (SEval SBV Value -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval SBV Value
y ->
         do ()
_ <- Value -> SBVEval ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
forceValue (Value -> SBVEval ()) -> SBVEval Value -> SBVEval ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval SBV Value
SBVEval Value
x
            SEval SBV Value
SBVEval Value
y)

  , (String
"parmap"      , SBV -> Value
forall sym. Backend sym => sym -> GenValue sym
parmapV SBV
sym)

    -- {at,len} (fin len) => [len][8] -> at
  , (String
"error"       ,
      (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
a ->
      (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Nat'
_ ->
      (SEval SBV Value -> SEval SBV Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun ((SEval SBV Value -> SEval SBV Value) -> Value)
-> (SEval SBV Value -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval SBV Value
s -> SBV -> TValue -> String -> SEval SBV Value
forall sym.
Backend sym =>
sym -> TValue -> String -> SEval sym (GenValue sym)
errorV SBV
sym TValue
a (String -> SBVEval Value) -> SBVEval String -> SBVEval Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (SBV -> Value -> SEval SBV String
forall sym. Backend sym => sym -> GenValue sym -> SEval sym String
valueToString SBV
sym (Value -> SBVEval String) -> SBVEval Value -> SBVEval String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval SBV Value
SBVEval Value
s))

  , (String
"random"      ,
      (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
a ->
      SBV -> (SWord SBV -> SEval SBV Value) -> Value
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam SBV
sym ((SWord SBV -> SEval SBV Value) -> Value)
-> (SWord SBV -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SWord SBV
x ->
         case SBV -> SInteger SBV -> Maybe Integer
forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit SBV
sym SWord SBV
SInteger SBV
x of
           Just Integer
i  -> SBV -> TValue -> Integer -> SEval SBV Value
forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
randomV SBV
sym TValue
a Integer
i
           Maybe Integer
Nothing -> SBV -> String -> SEval SBV Value
forall sym a. Backend sym => sym -> String -> SEval sym a
cryUserError SBV
sym String
"cannot evaluate 'random' with symbolic inputs")

     -- The trace function simply forces its first two
     -- values before returing the third in the symbolic
     -- evaluator.
  , (String
"trace",
      (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Nat'
_n ->
      (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
_a ->
      (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
_b ->
       (SEval SBV Value -> SEval SBV Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval SBV Value -> SEval SBV Value) -> Value)
-> (SEval SBV Value -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval SBV Value
s -> Value -> SBVEval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> SBVEval Value) -> Value -> SBVEval Value
forall a b. (a -> b) -> a -> b
$
       (SEval SBV Value -> SEval SBV Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval SBV Value -> SEval SBV Value) -> Value)
-> (SEval SBV Value -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval SBV Value
x -> Value -> SBVEval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> SBVEval Value) -> Value -> SBVEval Value
forall a b. (a -> b) -> a -> b
$
       (SEval SBV Value -> SEval SBV Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval SBV Value -> SEval SBV Value) -> Value)
-> (SEval SBV Value -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval SBV Value
y -> do
         Value
_ <- SEval SBV Value
SBVEval Value
s
         Value
_ <- SEval SBV Value
SBVEval Value
x
         SEval SBV Value
SBVEval Value
y)
  ]


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

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

  | Bool
otherwise
  = SEval SBV Value
SBVEval Value
folded

 where
    k :: Kind
k = SVal -> Kind
forall a. HasKind a => a -> Kind
SBV.kindOf SVal
idx
    def :: SEval SBV Value
def = SBV -> TValue -> SEval SBV Value
forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV SBV
sym TValue
a
    f :: Integer -> SBVEval Value -> SEval SBV Value
f Integer
n SBVEval Value
y = SBV
-> SBit SBV
-> SEval SBV Value
-> SEval SBV Value
-> SEval SBV Value
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 -> Integer -> SEval SBV Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap SBV
xs Integer
n) SEval SBV Value
SBVEval Value
y
    folded :: SBVEval Value
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 -> SBVEval Value -> SBVEval Value)
-> SBVEval Value -> [Integer] -> SBVEval Value
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Integer -> SBVEval Value -> SEval SBV Value
Integer -> SBVEval Value -> SBVEval Value
f SEval SBV Value
SBVEval Value
def [Integer
0 .. Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1]
            Nat'
_ -> (Integer -> SBVEval Value -> SBVEval Value)
-> SBVEval Value -> [Integer] -> SBVEval Value
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Integer -> SBVEval Value -> SEval SBV Value
Integer -> SBVEval Value -> SBVEval Value
f SEval SBV Value
SBVEval Value
def [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 -> SBVEval Value -> SBVEval Value)
-> SBVEval Value -> [Integer] -> SBVEval Value
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Integer -> SBVEval Value -> SEval SBV Value
Integer -> SBVEval Value -> SBVEval Value
f SEval SBV Value
SBVEval Value
def [Integer
0 .. Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1]
            Nat'
Inf -> IO Value -> SBVEval Value
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Unsupported -> IO Value
forall a e. Exception e => e -> a
X.throw (String -> Unsupported
UnsupportedSymbolicOp String
"unbounded integer indexing"))

indexBack ::
  SBV ->
  Nat' ->
  TValue ->
  SeqMap SBV ->
  TValue ->
  SWord SBV ->
  SEval SBV Value
indexBack :: SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> SWord SBV
-> SEval SBV Value
indexBack SBV
sym (Nat Integer
n) TValue
a SeqMap SBV
xs TValue
ix SWord SBV
idx = SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> SVal
-> SEval SBV Value
indexFront SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
a (Integer -> SeqMap SBV -> SeqMap SBV
forall sym. Integer -> SeqMap sym -> SeqMap sym
reverseSeqMap Integer
n SeqMap SBV
xs) TValue
ix SVal
SWord SBV
idx
indexBack SBV
_ Nat'
Inf TValue
_ SeqMap SBV
_ TValue
_ SWord SBV
_ = String -> [String] -> SBVEval Value
forall a. String -> [String] -> a
evalPanic String
"Expected finite sequence" [String
"indexBack"]

indexFront_bits ::
  SBV ->
  Nat' ->
  TValue ->
  SeqMap SBV ->
  TValue ->
  [SBit SBV] ->
  SEval SBV Value
indexFront_bits :: SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> [SBit SBV]
-> SEval SBV Value
indexFront_bits SBV
sym Nat'
mblen TValue
_a SeqMap SBV
xs TValue
_ix [SBit SBV]
bits0 = Integer -> Int -> [SBit SBV] -> SEval SBV Value
go Integer
0 ([SVal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SVal]
[SBit SBV]
bits0) [SBit SBV]
bits0
 where
  go :: Integer -> Int -> [SBit SBV] -> SEval SBV Value
  go :: Integer -> Int -> [SBit SBV] -> SEval SBV Value
go Integer
i Int
_k []
    -- For indices out of range, fail
    | Nat Integer
n <- Nat'
mblen
    , Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n
    = SBV -> EvalError -> SEval SBV Value
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError SBV
sym (Maybe Integer -> EvalError
InvalidIndex (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i))

    | Bool
otherwise
    = SeqMap SBV -> Integer -> SEval SBV Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap SBV
xs Integer
i

  go Integer
i Int
k (SBit SBV
b:[SBit SBV]
bs)
    -- Fail early when all possible indices we could compute from here
    -- are out of bounds
    | Nat Integer
n <- Nat'
mblen
    , (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
k) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n
    = SBV -> EvalError -> SEval SBV Value
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError SBV
sym (Maybe Integer -> EvalError
InvalidIndex Maybe Integer
forall a. Maybe a
Nothing)

    | Bool
otherwise
    = SBV
-> SBit SBV
-> SEval SBV Value
-> SEval SBV Value
-> SEval SBV Value
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue SBV
sym SBit SBV
b
         (Integer -> Int -> [SBit SBV] -> SEval SBV Value
go ((Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [SBit SBV]
bs)
         (Integer -> Int -> [SBit SBV] -> SEval SBV Value
go  (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
1)      (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [SBit SBV]
bs)


indexBack_bits ::
  SBV ->
  Nat' ->
  TValue ->
  SeqMap SBV ->
  TValue ->
  [SBit SBV] ->
  SEval SBV Value
indexBack_bits :: SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> [SBit SBV]
-> SEval SBV Value
indexBack_bits SBV
sym (Nat Integer
n) TValue
a SeqMap SBV
xs TValue
ix [SBit SBV]
idx = SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> TValue
-> [SBit SBV]
-> SEval SBV Value
indexFront_bits SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
a (Integer -> SeqMap SBV -> SeqMap SBV
forall sym. Integer -> SeqMap sym -> SeqMap sym
reverseSeqMap Integer
n SeqMap SBV
xs) TValue
ix [SBit SBV]
idx
indexBack_bits SBV
_ Nat'
Inf TValue
_ SeqMap SBV
_ TValue
_ [SBit SBV]
_ = String -> [String] -> SBVEval Value
forall a. String -> [String] -> a
evalPanic String
"Expected finite sequence" [String
"indexBack_bits"]


-- | Compare a symbolic word value with a concrete integer.
wordValueEqualsInteger :: SBV -> WordValue SBV -> Integer -> SEval SBV (SBit SBV)
wordValueEqualsInteger :: SBV -> WordValue SBV -> Integer -> SEval SBV (SBit SBV)
wordValueEqualsInteger SBV
sym WordValue SBV
wv Integer
i
  | SBV -> WordValue SBV -> Integer
forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize SBV
sym WordValue SBV
wv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer -> Integer
widthInteger Integer
i = SVal -> SBVEval SVal
forall (m :: * -> *) a. Monad m => a -> m a
return SVal
SBV.svFalse
  | Bool
otherwise =
    case WordValue SBV
wv of
      WordVal SWord SBV
w -> SVal -> SBVEval SVal
forall (m :: * -> *) a. Monad m => a -> m a
return (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal
SBV.svEqual SVal
SWord SBV
w (Int -> Integer -> SWord SBV
literalSWord (SVal -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SVal
SWord SBV
w) Integer
i)
      WordValue SBV
_ -> Integer -> [SBit SBV] -> SBit SBV
bitsAre Integer
i ([SVal] -> SVal) -> SBVEval [SVal] -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV -> WordValue SBV -> SEval SBV [SBit SBV]
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValueRev SBV
sym WordValue SBV
wv -- little-endian
  where
    bitsAre :: Integer -> [SBit SBV] -> SBit SBV
    bitsAre :: Integer -> [SBit SBV] -> SBit SBV
bitsAre Integer
n [] = Bool -> SVal
SBV.svBool (Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)
    bitsAre Integer
n (SBit SBV
b : [SBit SBV]
bs) = SVal -> SVal -> SVal
SBV.svAnd (Bool -> SBit SBV -> SBit SBV
bitIs (Integer -> Bool
forall a. Integral a => a -> Bool
odd Integer
n) SBit SBV
b) (Integer -> [SBit SBV] -> SBit SBV
bitsAre (Integer
n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2) [SBit SBV]
bs)

    bitIs :: Bool -> SBit SBV -> SBit SBV
    bitIs :: Bool -> SBit SBV -> SBit SBV
bitIs Bool
b SBit SBV
x = if Bool
b then SBit SBV
x else SVal -> SVal
SBV.svNot SVal
SBit SBV
x


updateFrontSym ::
  SBV ->
  Nat' ->
  TValue ->
  SeqMap SBV ->
  Either (SInteger SBV) (WordValue SBV) ->
  SEval SBV (GenValue SBV) ->
  SEval SBV (SeqMap SBV)
updateFrontSym :: SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV Value
-> SEval SBV (SeqMap SBV)
updateFrontSym SBV
sym Nat'
_len TValue
_eltTy SeqMap SBV
vs (Left SInteger SBV
idx) SEval SBV Value
val =
  case SVal -> Maybe Integer
SBV.svAsInteger SVal
SInteger SBV
idx of
    Just Integer
i -> SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ SeqMap SBV -> Integer -> SEval SBV Value -> SeqMap SBV
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap SeqMap SBV
vs Integer
i SEval SBV Value
val
    Maybe Integer
Nothing -> SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval SBV Value) -> SeqMap SBV
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval SBV Value) -> SeqMap SBV)
-> (Integer -> SEval SBV Value) -> SeqMap 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 Value
-> SEval SBV Value
-> SEval SBV Value
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 Value
val (SeqMap SBV -> Integer -> SEval SBV Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap SBV
vs Integer
i)

updateFrontSym SBV
sym Nat'
_len TValue
_eltTy SeqMap SBV
vs (Right WordValue SBV
wv) SEval SBV Value
val =
  case WordValue SBV
wv of
    WordVal SWord SBV
w | Just Integer
j <- SVal -> Maybe Integer
SBV.svAsInteger SVal
SWord SBV
w ->
      SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ SeqMap SBV -> Integer -> SEval SBV Value -> SeqMap SBV
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap SeqMap SBV
vs Integer
j SEval SBV Value
val
    WordValue SBV
_ ->
      SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval SBV Value) -> SeqMap SBV
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval SBV Value) -> SeqMap SBV)
-> (Integer -> SEval SBV Value) -> SeqMap SBV
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
      do SVal
b <- SBV -> WordValue SBV -> Integer -> SEval SBV (SBit SBV)
wordValueEqualsInteger SBV
sym WordValue SBV
wv Integer
i
         SBV
-> SBit SBV
-> SEval SBV Value
-> SEval SBV Value
-> SEval SBV Value
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 Value
val (SeqMap SBV -> Integer -> SEval SBV Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap 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 Value
-> SEval SBV (WordValue SBV)
updateFrontSym_word SBV
_ Nat'
Inf TValue
_ WordValue SBV
_ Either (SInteger SBV) (WordValue SBV)
_ SEval SBV Value
_ = String -> [String] -> SBVEval (WordValue SBV)
forall a. String -> [String] -> a
evalPanic String
"Expected finite sequence" [String
"updateFrontSym_bits"]

updateFrontSym_word SBV
sym (Nat Integer
_) TValue
eltTy (LargeBitsVal Integer
n SeqMap SBV
bv) Either (SInteger SBV) (WordValue SBV)
idx SEval SBV Value
val =
  Integer -> SeqMap SBV -> WordValue SBV
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
n (SeqMap SBV -> WordValue SBV)
-> SBVEval (SeqMap SBV) -> SBVEval (WordValue SBV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV Value
-> SEval SBV (SeqMap SBV)
updateFrontSym SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
eltTy SeqMap SBV
bv Either (SInteger SBV) (WordValue SBV)
idx SEval SBV Value
val

updateFrontSym_word SBV
sym (Nat Integer
n) TValue
eltTy (WordVal SWord SBV
bv) (Left SInteger SBV
idx) SEval SBV Value
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
-> Nat'
-> TValue
-> WordValue SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV Value
-> SEval SBV (WordValue SBV)
updateFrontSym_word SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
eltTy (SWord SBV -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal SWord SBV
bv) (WordValue SBV -> Either SVal (WordValue SBV)
forall a b. b -> Either a b
Right (SWord SBV -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal SVal
SWord SBV
idx')) SEval SBV Value
val

updateFrontSym_word SBV
sym (Nat Integer
n) TValue
eltTy WordValue SBV
bv (Right WordValue SBV
wv) SEval SBV Value
val =
  case WordValue SBV
wv of
    WordVal SWord SBV
idx
      | Just Integer
j <- SVal -> Maybe Integer
SBV.svAsInteger SVal
SWord SBV
idx ->
          SBV
-> WordValue SBV
-> Integer
-> SEval SBV (SBit SBV)
-> SEval SBV (WordValue SBV)
forall sym.
Backend sym =>
sym
-> WordValue sym
-> Integer
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordValue SBV
sym WordValue SBV
bv Integer
j (Value -> SVal
forall sym. GenValue sym -> SBit sym
fromVBit (Value -> SVal) -> SBVEval Value -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval SBV Value
SBVEval Value
val)

      | WordVal SWord SBV
bw <- WordValue SBV
bv ->
        SVal -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal (SVal -> WordValue SBV) -> SBVEval SVal -> SBVEval (WordValue SBV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          do SVal
b <- Value -> SVal
forall sym. GenValue sym -> SBit sym
fromVBit (Value -> SVal) -> SBVEval Value -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval SBV Value
SBVEval Value
val
             let sz :: Int
sz   = SVal -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SVal
SWord SBV
bw
             let z :: SWord SBV
z    = Int -> Integer -> SWord SBV
literalSWord Int
sz Integer
0
             let znot :: SVal
znot = SVal -> SVal
SBV.svNot SVal
SWord SBV
z
             let q :: SVal
q    = Kind -> Bool -> SVal -> SVal -> SVal -> SVal
SBV.svSymbolicMerge (SVal -> Kind
forall a. HasKind a => a -> Kind
SBV.kindOf SVal
SWord SBV
bw) Bool
True SVal
b SVal
znot SVal
SWord SBV
z
             let msk :: SVal
msk  = SVal -> SVal -> SVal
SBV.svShiftRight (Int -> Integer -> SWord SBV
literalSWord Int
sz (Int -> Integer
forall a. Bits a => Int -> a
bit (Int
szInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))) SVal
SWord SBV
idx
             let bw' :: SVal
bw'  = SVal -> SVal -> SVal
SBV.svAnd SVal
SWord SBV
bw (SVal -> SVal
SBV.svNot SVal
msk)
             SVal -> SBVEval SVal
forall (m :: * -> *) a. Monad m => a -> m a
return (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
SBV.svXOr SVal
bw' (SVal -> SVal -> SVal
SBV.svAnd SVal
q SVal
msk)

    WordValue SBV
_ -> Integer -> SeqMap SBV -> WordValue SBV
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
n (SeqMap SBV -> WordValue SBV)
-> SBVEval (SeqMap SBV) -> SBVEval (WordValue SBV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV Value
-> SEval SBV (SeqMap SBV)
updateFrontSym SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
eltTy (SBV -> WordValue SBV -> SeqMap SBV
forall sym. Backend sym => sym -> WordValue sym -> SeqMap sym
asBitsMap SBV
sym WordValue SBV
bv) (WordValue SBV -> Either SVal (WordValue SBV)
forall a b. b -> Either a b
Right WordValue SBV
wv) SEval SBV Value
val


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

updateBackSym SBV
sym (Nat Integer
n) TValue
_eltTy SeqMap SBV
vs (Left SInteger SBV
idx) SEval SBV Value
val =
  case SVal -> Maybe Integer
SBV.svAsInteger SVal
SInteger SBV
idx of
    Just Integer
i -> SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ SeqMap SBV -> Integer -> SEval SBV Value -> SeqMap SBV
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap SeqMap 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 Value
val
    Maybe Integer
Nothing -> SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval SBV Value) -> SeqMap SBV
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval SBV Value) -> SeqMap SBV)
-> (Integer -> SEval SBV Value) -> SeqMap 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 Value
-> SEval SBV Value
-> SEval SBV Value
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 Value
val (SeqMap SBV -> Integer -> SEval SBV Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap SBV
vs Integer
i)

updateBackSym SBV
sym (Nat Integer
n) TValue
_eltTy SeqMap SBV
vs (Right WordValue SBV
wv) SEval SBV Value
val =
  case WordValue SBV
wv of
    WordVal SWord SBV
w | Just Integer
j <- SVal -> Maybe Integer
SBV.svAsInteger SVal
SWord SBV
w ->
      SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ SeqMap SBV -> Integer -> SEval SBV Value -> SeqMap SBV
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap SeqMap 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 Value
val
    WordValue SBV
_ ->
      SeqMap SBV -> SBVEval (SeqMap SBV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBV -> SBVEval (SeqMap SBV))
-> SeqMap SBV -> SBVEval (SeqMap SBV)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval SBV Value) -> SeqMap SBV
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval SBV Value) -> SeqMap SBV)
-> (Integer -> SEval SBV Value) -> SeqMap SBV
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
      do SVal
b <- SBV -> WordValue SBV -> Integer -> SEval SBV (SBit SBV)
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 Value
-> SEval SBV Value
-> SEval SBV Value
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 Value
val (SeqMap SBV -> Integer -> SEval SBV Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap 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 Value
-> SEval SBV (WordValue SBV)
updateBackSym_word SBV
_ Nat'
Inf TValue
_ WordValue SBV
_ Either (SInteger SBV) (WordValue SBV)
_ SEval SBV Value
_ = String -> [String] -> SBVEval (WordValue SBV)
forall a. String -> [String] -> a
evalPanic String
"Expected finite sequence" [String
"updateBackSym_bits"]

updateBackSym_word SBV
sym (Nat Integer
_) TValue
eltTy (LargeBitsVal Integer
n SeqMap SBV
bv) Either (SInteger SBV) (WordValue SBV)
idx SEval SBV Value
val =
  Integer -> SeqMap SBV -> WordValue SBV
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
n (SeqMap SBV -> WordValue SBV)
-> SBVEval (SeqMap SBV) -> SBVEval (WordValue SBV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV Value
-> SEval SBV (SeqMap SBV)
updateBackSym SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
eltTy SeqMap SBV
bv Either (SInteger SBV) (WordValue SBV)
idx SEval SBV Value
val

updateBackSym_word SBV
sym (Nat Integer
n) TValue
eltTy (WordVal SWord SBV
bv) (Left SInteger SBV
idx) SEval SBV Value
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
-> Nat'
-> TValue
-> WordValue SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV Value
-> SEval SBV (WordValue SBV)
updateBackSym_word SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
eltTy (SWord SBV -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal SWord SBV
bv) (WordValue SBV -> Either SVal (WordValue SBV)
forall a b. b -> Either a b
Right (SWord SBV -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal SVal
SWord SBV
idx')) SEval SBV Value
val

updateBackSym_word SBV
sym (Nat Integer
n) TValue
eltTy WordValue SBV
bv (Right WordValue SBV
wv) SEval SBV Value
val = do
  case WordValue SBV
wv of
    WordVal SWord SBV
idx
      | Just Integer
j <- SVal -> Maybe Integer
SBV.svAsInteger SVal
SWord SBV
idx ->
          SBV
-> WordValue SBV
-> Integer
-> SEval SBV (SBit SBV)
-> SEval SBV (WordValue SBV)
forall sym.
Backend sym =>
sym
-> WordValue sym
-> Integer
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordValue SBV
sym WordValue SBV
bv (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) (Value -> SVal
forall sym. GenValue sym -> SBit sym
fromVBit (Value -> SVal) -> SBVEval Value -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval SBV Value
SBVEval Value
val)

      | WordVal SWord SBV
bw <- WordValue SBV
bv ->
        SVal -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal (SVal -> WordValue SBV) -> SBVEval SVal -> SBVEval (WordValue SBV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          do SVal
b <- Value -> SVal
forall sym. GenValue sym -> SBit sym
fromVBit (Value -> SVal) -> SBVEval Value -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval SBV Value
SBVEval Value
val
             let sz :: Int
sz   = SVal -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SVal
SWord SBV
bw
             let z :: SWord SBV
z    = Int -> Integer -> SWord SBV
literalSWord Int
sz Integer
0
             let znot :: SVal
znot = SVal -> SVal
SBV.svNot SVal
SWord SBV
z
             let q :: SVal
q    = Kind -> Bool -> SVal -> SVal -> SVal -> SVal
SBV.svSymbolicMerge (SVal -> Kind
forall a. HasKind a => a -> Kind
SBV.kindOf SVal
SWord SBV
bw) Bool
True SVal
b SVal
znot SVal
SWord SBV
z
             let msk :: SVal
msk  = SVal -> SVal -> SVal
SBV.svShiftLeft (Int -> Integer -> SWord SBV
literalSWord Int
sz Integer
1) SVal
SWord SBV
idx
             let bw' :: SVal
bw'  = SVal -> SVal -> SVal
SBV.svAnd SVal
SWord SBV
bw (SVal -> SVal
SBV.svNot SVal
msk)
             SVal -> SBVEval SVal
forall (m :: * -> *) a. Monad m => a -> m a
return (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
SBV.svXOr SVal
bw' (SVal -> SVal -> SVal
SBV.svAnd SVal
q SVal
msk)

    WordValue SBV
_ -> Integer -> SeqMap SBV -> WordValue SBV
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
n (SeqMap SBV -> WordValue SBV)
-> SBVEval (SeqMap SBV) -> SBVEval (WordValue SBV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV
-> Nat'
-> TValue
-> SeqMap SBV
-> Either (SInteger SBV) (WordValue SBV)
-> SEval SBV Value
-> SEval SBV (SeqMap SBV)
updateBackSym SBV
sym (Integer -> Nat'
Nat Integer
n) TValue
eltTy (SBV -> WordValue SBV -> SeqMap SBV
forall sym. Backend sym => sym -> WordValue sym -> SeqMap sym
asBitsMap SBV
sym WordValue SBV
bv) (WordValue SBV -> Either SVal (WordValue SBV)
forall a b. b -> Either a b
Right WordValue SBV
wv) SEval SBV Value
val


asWordList :: [WordValue SBV] -> Maybe [SWord SBV]
asWordList :: [WordValue SBV] -> Maybe [SWord SBV]
asWordList = ([SWord SBV] -> [SWord SBV])
-> [WordValue SBV] -> Maybe [SWord SBV]
go [SWord SBV] -> [SWord SBV]
forall a. a -> a
id
 where go :: ([SWord SBV] -> [SWord SBV]) -> [WordValue SBV] -> Maybe [SWord SBV]
       go :: ([SWord SBV] -> [SWord SBV])
-> [WordValue SBV] -> Maybe [SWord SBV]
go [SWord SBV] -> [SWord SBV]
f [] = [SVal] -> Maybe [SVal]
forall a. a -> Maybe a
Just ([SWord SBV] -> [SWord SBV]
f [])
       go [SWord SBV] -> [SWord SBV]
f (WordVal SWord SBV
x :[WordValue SBV]
vs) = ([SWord SBV] -> [SWord SBV])
-> [WordValue SBV] -> Maybe [SWord SBV]
go ([SVal] -> [SVal]
[SWord SBV] -> [SWord SBV]
f ([SVal] -> [SVal]) -> ([SVal] -> [SVal]) -> [SVal] -> [SVal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SVal
SWord SBV
xSVal -> [SVal] -> [SVal]
forall a. a -> [a] -> [a]
:)) [WordValue SBV]
vs
       go [SWord SBV] -> [SWord SBV]
_f (LargeBitsVal Integer
_ SeqMap SBV
_ : [WordValue SBV]
_) = Maybe [SWord SBV]
forall a. Maybe a
Nothing

sshrV :: SBV -> Value
sshrV :: SBV -> Value
sshrV SBV
sym =
  (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Nat'
n ->
  (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
ix ->
  SBV -> (SWord SBV -> SEval SBV Value) -> Value
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam SBV
sym ((SWord SBV -> SEval SBV Value) -> Value)
-> (SWord SBV -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SWord SBV
x -> Value -> SBVEval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> SBVEval Value) -> Value -> SBVEval Value
forall a b. (a -> b) -> a -> b
$
  (SEval SBV Value -> SEval SBV Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval SBV Value -> SEval SBV Value) -> Value)
-> (SEval SBV Value -> SEval SBV Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval SBV Value
y ->
   SEval SBV Value
SBVEval Value
y SBVEval Value
-> (Value -> SBVEval (Either SVal (WordValue SBV)))
-> SBVEval (Either SVal (WordValue SBV))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SBV
-> String
-> TValue
-> Value
-> SEval SBV (Either (SInteger SBV) (WordValue SBV))
forall sym.
Backend sym =>
sym
-> String
-> TValue
-> GenValue sym
-> SEval sym (Either (SInteger sym) (WordValue sym))
asIndex SBV
sym String
">>$" TValue
ix SBVEval (Either SVal (WordValue SBV))
-> (Either SVal (WordValue SBV) -> SBVEval Value) -> SBVEval Value
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
     Left SVal
idx ->
       do let w :: Integer
w = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (SVal -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SVal
SWord SBV
x)
          let pneg :: SVal
pneg = SVal -> SVal -> SVal
svLessThan SVal
idx (Kind -> Integer -> SVal
svInteger Kind
KUnbounded Integer
0)
          SVal
zneg <- SVal -> SVal -> SVal
shl SVal
SWord SBV
x  (SVal -> SVal) -> (SVal -> SVal) -> SVal -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SInteger SBV -> SWord SBV
svFromInteger Integer
w (SVal -> SVal) -> SBVEval SVal -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink SBV
sym Nat'
n TValue
ix (SVal -> SVal
SBV.svUNeg SVal
idx)
          SVal
zpos <- SVal -> SVal -> SVal
ashr SVal
SWord SBV
x (SVal -> SVal) -> (SVal -> SVal) -> SVal -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SInteger SBV -> SWord SBV
svFromInteger Integer
w (SVal -> SVal) -> SBVEval SVal -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV -> Nat' -> TValue -> SInteger SBV -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink SBV
sym Nat'
n TValue
ix SVal
SInteger SBV
idx
          let z :: SVal
z = Kind -> Bool -> SVal -> SVal -> SVal -> SVal
svSymbolicMerge (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
SWord SBV
x) Bool
True SVal
pneg SVal
zneg SVal
zpos
          Value -> SBVEval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> SBVEval Value)
-> (SVal -> Value) -> SVal -> SBVEval Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SEval SBV (WordValue SBV) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
w (SBVEval (WordValue SBV) -> Value)
-> (SVal -> SBVEval (WordValue SBV)) -> SVal -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue SBV -> SBVEval (WordValue SBV)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue SBV -> SBVEval (WordValue SBV))
-> (SVal -> WordValue SBV) -> SVal -> SBVEval (WordValue SBV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal (SVal -> SBVEval Value) -> SVal -> SBVEval Value
forall a b. (a -> b) -> a -> b
$ SVal
z

     Right WordValue SBV
wv ->
       do SVal
z <- SVal -> SVal -> SVal
ashr SVal
SWord SBV
x (SVal -> SVal) -> SBVEval SVal -> SBVEval SVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV -> WordValue SBV -> SEval SBV (SWord SBV)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal SBV
sym WordValue SBV
wv
          Value -> SBVEval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> SBVEval Value)
-> (SVal -> Value) -> SVal -> SBVEval Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SEval SBV (WordValue SBV) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (SVal -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SVal
SWord SBV
x)) (SBVEval (WordValue SBV) -> Value)
-> (SVal -> SBVEval (WordValue SBV)) -> SVal -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue SBV -> SBVEval (WordValue SBV)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue SBV -> SBVEval (WordValue SBV))
-> (SVal -> WordValue SBV) -> SVal -> SBVEval (WordValue SBV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> WordValue SBV
forall sym. SWord sym -> WordValue sym
WordVal (SVal -> SBVEval Value) -> SVal -> SBVEval Value
forall a b. (a -> b) -> a -> b
$ SVal
z