{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.Eval.Value where
import Data.Bits
import Data.IORef
import qualified Data.Sequence as Seq
import qualified Data.Foldable as Fold
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import MonadLib
import qualified Cryptol.Eval.Arch as Arch
import Cryptol.Eval.Monad
import Cryptol.Eval.Type
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
import Cryptol.Utils.Ident (Ident,mkIdent)
import Cryptol.Utils.PP
import Cryptol.Utils.Panic(panic)
import Data.List(genericLength, genericIndex, genericDrop)
import qualified Data.Text as T
import Numeric (showIntAtBase)
import GHC.Generics (Generic)
import Control.DeepSeq
data BV = BV !Integer !Integer deriving ((forall x. BV -> Rep BV x)
-> (forall x. Rep BV x -> BV) -> Generic BV
forall x. Rep BV x -> BV
forall x. BV -> Rep BV x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep BV x -> BV
$cfrom :: forall x. BV -> Rep BV x
Generic, BV -> ()
(BV -> ()) -> NFData BV
forall a. (a -> ()) -> NFData a
rnf :: BV -> ()
$crnf :: BV -> ()
NFData)
instance Show BV where
show :: BV -> String
show = Integer -> String
forall a. Show a => a -> String
show (Integer -> String) -> (BV -> Integer) -> BV -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> Integer
bvVal
binBV :: (Integer -> Integer -> Integer) -> BV -> BV -> BV
binBV :: (Integer -> Integer -> Integer) -> BV -> BV -> BV
binBV f :: Integer -> Integer -> Integer
f (BV w :: Integer
w x :: Integer
x) (BV _ y :: Integer
y) = Integer -> Integer -> BV
mkBv Integer
w (Integer -> Integer -> Integer
f Integer
x Integer
y)
unaryBV :: (Integer -> Integer) -> BV -> BV
unaryBV :: (Integer -> Integer) -> BV -> BV
unaryBV f :: Integer -> Integer
f (BV w :: Integer
w x :: Integer
x) = Integer -> Integer -> BV
mkBv Integer
w (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
f Integer
x
bvVal :: BV -> Integer
bvVal :: BV -> Integer
bvVal (BV _w :: Integer
_w x :: Integer
x) = Integer
x
mkBv :: Integer -> Integer -> BV
mkBv :: Integer -> Integer -> BV
mkBv w :: Integer
w i :: Integer
i = Integer -> Integer -> BV
BV Integer
w (Integer -> Integer -> Integer
mask Integer
w Integer
i)
data SeqMap b w i
= IndexSeqMap !(Integer -> Eval (GenValue b w i))
| UpdateSeqMap !(Map Integer (Eval (GenValue b w i)))
!(Integer -> Eval (GenValue b w i))
lookupSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap (IndexSeqMap f :: Integer -> Eval (GenValue b w i)
f) i :: Integer
i = Integer -> Eval (GenValue b w i)
f Integer
i
lookupSeqMap (UpdateSeqMap m :: Map Integer (Eval (GenValue b w i))
m f :: Integer -> Eval (GenValue b w i)
f) i :: Integer
i =
case Integer
-> Map Integer (Eval (GenValue b w i))
-> Maybe (Eval (GenValue b w i))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Integer
i Map Integer (Eval (GenValue b w i))
m of
Just x :: Eval (GenValue b w i)
x -> Eval (GenValue b w i)
x
Nothing -> Integer -> Eval (GenValue b w i)
f Integer
i
type SeqValMap = SeqMap Bool BV Integer
instance NFData (SeqMap b w i) where
rnf :: SeqMap b w i -> ()
rnf x :: SeqMap b w i
x = SeqMap b w i -> () -> ()
forall a b. a -> b -> b
seq SeqMap b w i
x ()
finiteSeqMap :: [Eval (GenValue b w i)] -> SeqMap b w i
finiteSeqMap :: [Eval (GenValue b w i)] -> SeqMap b w i
finiteSeqMap xs :: [Eval (GenValue b w i)]
xs =
Map Integer (Eval (GenValue b w i))
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i.
Map Integer (Eval (GenValue b w i))
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
UpdateSeqMap
([(Integer, Eval (GenValue b w i))]
-> Map Integer (Eval (GenValue b w i))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([Integer]
-> [Eval (GenValue b w i)] -> [(Integer, Eval (GenValue b w i))]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [Eval (GenValue b w i)]
xs))
Integer -> Eval (GenValue b w i)
forall a. Integer -> Eval a
invalidIndex
infiniteSeqMap :: [Eval (GenValue b w i)] -> Eval (SeqMap b w i)
infiniteSeqMap :: [Eval (GenValue b w i)] -> Eval (SeqMap b w i)
infiniteSeqMap xs :: [Eval (GenValue b w i)]
xs =
SeqMap b w i -> Eval (SeqMap b w i)
forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
memoMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i -> [Eval (GenValue b w i)] -> Integer -> Eval (GenValue b w i)
forall i a. Integral i => [a] -> i -> a
genericIndex [Eval (GenValue b w i)]
xs Integer
i)
enumerateSeqMap :: (Integral n) => n -> SeqMap b w i -> [Eval (GenValue b w i)]
enumerateSeqMap :: n -> SeqMap b w i -> [Eval (GenValue b w i)]
enumerateSeqMap n :: n
n m :: SeqMap b w i
m = [ SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
m Integer
i | Integer
i <- [0 .. (n -> Integer
forall a. Integral a => a -> Integer
toInteger n
n)Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-1] ]
streamSeqMap :: SeqMap b w i -> [Eval (GenValue b w i)]
streamSeqMap :: SeqMap b w i -> [Eval (GenValue b w i)]
streamSeqMap m :: SeqMap b w i
m = [ SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
m Integer
i | Integer
i <- [0..] ]
reverseSeqMap :: Integer
-> SeqMap b w i
-> SeqMap b w i
reverseSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i
reverseSeqMap n :: Integer
n vals :: SeqMap b w i
vals = (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
vals (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i)
updateSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
updateSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
updateSeqMap (UpdateSeqMap m :: Map Integer (Eval (GenValue b w i))
m sm :: Integer -> Eval (GenValue b w i)
sm) i :: Integer
i x :: Eval (GenValue b w i)
x = Map Integer (Eval (GenValue b w i))
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i.
Map Integer (Eval (GenValue b w i))
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
UpdateSeqMap (Integer
-> Eval (GenValue b w i)
-> Map Integer (Eval (GenValue b w i))
-> Map Integer (Eval (GenValue b w i))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
i Eval (GenValue b w i)
x Map Integer (Eval (GenValue b w i))
m) Integer -> Eval (GenValue b w i)
sm
updateSeqMap (IndexSeqMap f :: Integer -> Eval (GenValue b w i)
f) i :: Integer
i x :: Eval (GenValue b w i)
x = Map Integer (Eval (GenValue b w i))
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i.
Map Integer (Eval (GenValue b w i))
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
UpdateSeqMap (Integer
-> Eval (GenValue b w i) -> Map Integer (Eval (GenValue b w i))
forall k a. k -> a -> Map k a
Map.singleton Integer
i Eval (GenValue b w i)
x) Integer -> Eval (GenValue b w i)
f
concatSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i -> SeqMap b w i
concatSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i -> SeqMap b w i
concatSeqMap n :: Integer
n x :: SeqMap b w i
x y :: SeqMap b w i
y =
(Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i ->
if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n
then SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
x Integer
i
else SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
y (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
n)
splitSeqMap :: Integer -> SeqMap b w i -> (SeqMap b w i, SeqMap b w i)
splitSeqMap :: Integer -> SeqMap b w i -> (SeqMap b w i, SeqMap b w i)
splitSeqMap n :: Integer
n xs :: SeqMap b w i
xs = (SeqMap b w i
hd,SeqMap b w i
tl)
where
hd :: SeqMap b w i
hd = SeqMap b w i
xs
tl :: SeqMap b w i
tl = (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
xs (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
n)
dropSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i
dropSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i
dropSeqMap 0 xs :: SeqMap b w i
xs = SeqMap b w i
xs
dropSeqMap n :: Integer
n xs :: SeqMap b w i
xs = (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
xs (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
n)
memoMap :: SeqMap b w i -> Eval (SeqMap b w i)
memoMap :: SeqMap b w i -> Eval (SeqMap b w i)
memoMap x :: SeqMap b w i
x = do
IORef (Map Integer (GenValue b w i))
cache <- IO (IORef (Map Integer (GenValue b w i)))
-> Eval (IORef (Map Integer (GenValue b w i)))
forall a. IO a -> Eval a
io (IO (IORef (Map Integer (GenValue b w i)))
-> Eval (IORef (Map Integer (GenValue b w i))))
-> IO (IORef (Map Integer (GenValue b w i)))
-> Eval (IORef (Map Integer (GenValue b w i)))
forall a b. (a -> b) -> a -> b
$ Map Integer (GenValue b w i)
-> IO (IORef (Map Integer (GenValue b w i)))
forall a. a -> IO (IORef a)
newIORef (Map Integer (GenValue b w i)
-> IO (IORef (Map Integer (GenValue b w i))))
-> Map Integer (GenValue b w i)
-> IO (IORef (Map Integer (GenValue b w i)))
forall a b. (a -> b) -> a -> b
$ Map Integer (GenValue b w i)
forall k a. Map k a
Map.empty
SeqMap b w i -> Eval (SeqMap b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap b w i -> Eval (SeqMap b w i))
-> SeqMap b w i -> Eval (SeqMap b w i)
forall a b. (a -> b) -> a -> b
$ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap (IORef (Map Integer (GenValue b w i))
-> Integer -> Eval (GenValue b w i)
memo IORef (Map Integer (GenValue b w i))
cache)
where
memo :: IORef (Map Integer (GenValue b w i))
-> Integer -> Eval (GenValue b w i)
memo cache :: IORef (Map Integer (GenValue b w i))
cache i :: Integer
i = do
Maybe (GenValue b w i)
mz <- IO (Maybe (GenValue b w i)) -> Eval (Maybe (GenValue b w i))
forall a. IO a -> Eval a
io (Integer -> Map Integer (GenValue b w i) -> Maybe (GenValue b w i)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Integer
i (Map Integer (GenValue b w i) -> Maybe (GenValue b w i))
-> IO (Map Integer (GenValue b w i)) -> IO (Maybe (GenValue b w i))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (Map Integer (GenValue b w i))
-> IO (Map Integer (GenValue b w i))
forall a. IORef a -> IO a
readIORef IORef (Map Integer (GenValue b w i))
cache)
case Maybe (GenValue b w i)
mz of
Just z :: GenValue b w i
z -> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return GenValue b w i
z
Nothing -> IORef (Map Integer (GenValue b w i))
-> Integer -> Eval (GenValue b w i)
doEval IORef (Map Integer (GenValue b w i))
cache Integer
i
doEval :: IORef (Map Integer (GenValue b w i))
-> Integer -> Eval (GenValue b w i)
doEval cache :: IORef (Map Integer (GenValue b w i))
cache i :: Integer
i = do
GenValue b w i
v <- SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
x Integer
i
IO () -> Eval ()
forall a. IO a -> Eval a
io (IO () -> Eval ()) -> IO () -> Eval ()
forall a b. (a -> b) -> a -> b
$ IORef (Map Integer (GenValue b w i))
-> (Map Integer (GenValue b w i) -> Map Integer (GenValue b w i))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Map Integer (GenValue b w i))
cache (Integer
-> GenValue b w i
-> Map Integer (GenValue b w i)
-> Map Integer (GenValue b w i)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
i GenValue b w i
v)
GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return GenValue b w i
v
zipSeqMap :: (GenValue b w i -> GenValue b w i -> Eval (GenValue b w i))
-> SeqMap b w i
-> SeqMap b w i
-> Eval (SeqMap b w i)
zipSeqMap :: (GenValue b w i -> GenValue b w i -> Eval (GenValue b w i))
-> SeqMap b w i -> SeqMap b w i -> Eval (SeqMap b w i)
zipSeqMap f :: GenValue b w i -> GenValue b w i -> Eval (GenValue b w i)
f x :: SeqMap b w i
x y :: SeqMap b w i
y =
SeqMap b w i -> Eval (SeqMap b w i)
forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
memoMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i -> Eval (Eval (GenValue b w i)) -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (GenValue b w i -> GenValue b w i -> Eval (GenValue b w i)
f (GenValue b w i -> GenValue b w i -> Eval (GenValue b w i))
-> Eval (GenValue b w i)
-> Eval (GenValue b w i -> Eval (GenValue b w i))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
x Integer
i Eval (GenValue b w i -> Eval (GenValue b w i))
-> Eval (GenValue b w i) -> Eval (Eval (GenValue b w i))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
y Integer
i))
mapSeqMap :: (GenValue b w i -> Eval (GenValue b w i))
-> SeqMap b w i -> Eval (SeqMap b w i)
mapSeqMap :: (GenValue b w i -> Eval (GenValue b w i))
-> SeqMap b w i -> Eval (SeqMap b w i)
mapSeqMap f :: GenValue b w i -> Eval (GenValue b w i)
f x :: SeqMap b w i
x =
SeqMap b w i -> Eval (SeqMap b w i)
forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
memoMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i -> GenValue b w i -> Eval (GenValue b w i)
f (GenValue b w i -> Eval (GenValue b w i))
-> Eval (GenValue b w i) -> Eval (GenValue b w i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
x Integer
i)
data WordValue b w i
= WordVal !w
| BitsVal !(Seq.Seq (Eval b))
| LargeBitsVal !Integer !(SeqMap b w i )
deriving ((forall x. WordValue b w i -> Rep (WordValue b w i) x)
-> (forall x. Rep (WordValue b w i) x -> WordValue b w i)
-> Generic (WordValue b w i)
forall x. Rep (WordValue b w i) x -> WordValue b w i
forall x. WordValue b w i -> Rep (WordValue b w i) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall b w i x. Rep (WordValue b w i) x -> WordValue b w i
forall b w i x. WordValue b w i -> Rep (WordValue b w i) x
$cto :: forall b w i x. Rep (WordValue b w i) x -> WordValue b w i
$cfrom :: forall b w i x. WordValue b w i -> Rep (WordValue b w i) x
Generic, WordValue b w i -> ()
(WordValue b w i -> ()) -> NFData (WordValue b w i)
forall a. (a -> ()) -> NFData a
forall b w i. (NFData w, NFData b) => WordValue b w i -> ()
rnf :: WordValue b w i -> ()
$crnf :: forall b w i. (NFData w, NFData b) => WordValue b w i -> ()
NFData)
largeBitSize :: Integer
largeBitSize :: Integer
largeBitSize = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` 16
asWordVal :: BitWord b w i => WordValue b w i -> Eval w
asWordVal :: WordValue b w i -> Eval w
asWordVal (WordVal w :: w
w) = w -> Eval w
forall (m :: * -> *) a. Monad m => a -> m a
return w
w
asWordVal (BitsVal bs :: Seq (Eval b)
bs) = [b] -> w
forall b w i. BitWord b w i => [b] -> w
packWord ([b] -> w) -> Eval [b] -> Eval w
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Eval b] -> Eval [b]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Seq (Eval b) -> [Eval b]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Seq (Eval b)
bs)
asWordVal (LargeBitsVal n :: Integer
n xs :: SeqMap b w i
xs) = [b] -> w
forall b w i. BitWord b w i => [b] -> w
packWord ([b] -> w) -> Eval [b] -> Eval w
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Eval (GenValue b w i) -> Eval b)
-> [Eval (GenValue b w i)] -> Eval [b]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (GenValue b w i -> Eval b
forall b w i. GenValue b w i -> Eval b
fromBit (GenValue b w i -> Eval b) -> Eval (GenValue b w i) -> Eval b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (Integer -> SeqMap b w i -> [Eval (GenValue b w i)]
forall n b w i.
Integral n =>
n -> SeqMap b w i -> [Eval (GenValue b w i)]
enumerateSeqMap Integer
n SeqMap b w i
xs)
asBitsMap :: BitWord b w i => WordValue b w i -> SeqMap b w i
asBitsMap :: WordValue b w i -> SeqMap b w i
asBitsMap (WordVal w :: w
w) = (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i -> GenValue b w i -> Eval (GenValue b w i)
forall a. a -> Eval a
ready (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ b -> GenValue b w i
forall b w i. b -> GenValue b w i
VBit (b -> GenValue b w i) -> b -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ w -> Integer -> b
forall b w i. BitWord b w i => w -> Integer -> b
wordBit w
w Integer
i
asBitsMap (BitsVal bs :: Seq (Eval b)
bs) = (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i -> b -> GenValue b w i
forall b w i. b -> GenValue b w i
VBit (b -> GenValue b w i) -> Eval b -> Eval (GenValue b w i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval (Eval b) -> Eval b
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Seq (Eval b) -> Integer -> Eval (Eval b)
forall a. Seq a -> Integer -> Eval a
checkedSeqIndex Seq (Eval b)
bs Integer
i)
asBitsMap (LargeBitsVal _ xs :: SeqMap b w i
xs) = SeqMap b w i
xs
enumerateWordValue :: BitWord b w i => WordValue b w i -> Eval [b]
enumerateWordValue :: WordValue b w i -> Eval [b]
enumerateWordValue (WordVal w :: w
w) = [b] -> Eval [b]
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> Eval [b]) -> [b] -> Eval [b]
forall a b. (a -> b) -> a -> b
$ w -> [b]
forall b w i. BitWord b w i => w -> [b]
unpackWord w
w
enumerateWordValue (BitsVal bs :: Seq (Eval b)
bs) = [Eval b] -> Eval [b]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Seq (Eval b) -> [Eval b]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Seq (Eval b)
bs)
enumerateWordValue (LargeBitsVal n :: Integer
n xs :: SeqMap b w i
xs) = (Eval (GenValue b w i) -> Eval b)
-> [Eval (GenValue b w i)] -> Eval [b]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (GenValue b w i -> Eval b
forall b w i. GenValue b w i -> Eval b
fromBit (GenValue b w i -> Eval b) -> Eval (GenValue b w i) -> Eval b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (Integer -> SeqMap b w i -> [Eval (GenValue b w i)]
forall n b w i.
Integral n =>
n -> SeqMap b w i -> [Eval (GenValue b w i)]
enumerateSeqMap Integer
n SeqMap b w i
xs)
enumerateWordValueRev :: BitWord b w i => WordValue b w i -> Eval [b]
enumerateWordValueRev :: WordValue b w i -> Eval [b]
enumerateWordValueRev (WordVal w :: w
w) = [b] -> Eval [b]
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> Eval [b]) -> [b] -> Eval [b]
forall a b. (a -> b) -> a -> b
$ [b] -> [b]
forall a. [a] -> [a]
reverse ([b] -> [b]) -> [b] -> [b]
forall a b. (a -> b) -> a -> b
$ w -> [b]
forall b w i. BitWord b w i => w -> [b]
unpackWord w
w
enumerateWordValueRev (BitsVal bs :: Seq (Eval b)
bs) = [Eval b] -> Eval [b]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Seq (Eval b) -> [Eval b]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList (Seq (Eval b) -> [Eval b]) -> Seq (Eval b) -> [Eval b]
forall a b. (a -> b) -> a -> b
$ Seq (Eval b) -> Seq (Eval b)
forall a. Seq a -> Seq a
Seq.reverse Seq (Eval b)
bs)
enumerateWordValueRev (LargeBitsVal n :: Integer
n xs :: SeqMap b w i
xs) = (Eval (GenValue b w i) -> Eval b)
-> [Eval (GenValue b w i)] -> Eval [b]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (GenValue b w i -> Eval b
forall b w i. GenValue b w i -> Eval b
fromBit (GenValue b w i -> Eval b) -> Eval (GenValue b w i) -> Eval b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (Integer -> SeqMap b w i -> [Eval (GenValue b w i)]
forall n b w i.
Integral n =>
n -> SeqMap b w i -> [Eval (GenValue b w i)]
enumerateSeqMap Integer
n (Integer -> SeqMap b w i -> SeqMap b w i
forall b w i. Integer -> SeqMap b w i -> SeqMap b w i
reverseSeqMap Integer
n SeqMap b w i
xs))
wordValueSize :: BitWord b w i => WordValue b w i -> Integer
wordValueSize :: WordValue b w i -> Integer
wordValueSize (WordVal w :: w
w) = w -> Integer
forall b w i. BitWord b w i => w -> Integer
wordLen w
w
wordValueSize (BitsVal bs :: Seq (Eval b)
bs) = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Seq (Eval b) -> Int
forall a. Seq a -> Int
Seq.length Seq (Eval b)
bs
wordValueSize (LargeBitsVal n :: Integer
n _) = Integer
n
checkedSeqIndex :: Seq.Seq a -> Integer -> Eval a
checkedSeqIndex :: Seq a -> Integer -> Eval a
checkedSeqIndex xs :: Seq a
xs i :: Integer
i =
case Seq a -> ViewL a
forall a. Seq a -> ViewL a
Seq.viewl (Int -> Seq a -> Seq a
forall a. Int -> Seq a -> Seq a
Seq.drop (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i) Seq a
xs) of
x :: a
x Seq.:< _ -> a -> Eval a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
Seq.EmptyL -> Integer -> Eval a
forall a. Integer -> Eval a
invalidIndex Integer
i
checkedIndex :: [a] -> Integer -> Eval a
checkedIndex :: [a] -> Integer -> Eval a
checkedIndex xs :: [a]
xs i :: Integer
i =
case Integer -> [a] -> [a]
forall i a. Integral i => i -> [a] -> [a]
genericDrop Integer
i [a]
xs of
(x :: a
x:_) -> a -> Eval a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
_ -> Integer -> Eval a
forall a. Integer -> Eval a
invalidIndex Integer
i
indexWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b
indexWordValue :: WordValue b w i -> Integer -> Eval b
indexWordValue (WordVal w :: w
w) idx :: Integer
idx
| Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< w -> Integer
forall b w i. BitWord b w i => w -> Integer
wordLen w
w = b -> Eval b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> Eval b) -> b -> Eval b
forall a b. (a -> b) -> a -> b
$ w -> Integer -> b
forall b w i. BitWord b w i => w -> Integer -> b
wordBit w
w Integer
idx
| Bool
otherwise = Integer -> Eval b
forall a. Integer -> Eval a
invalidIndex Integer
idx
indexWordValue (BitsVal bs :: Seq (Eval b)
bs) idx :: Integer
idx = Eval (Eval b) -> Eval b
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Seq (Eval b) -> Integer -> Eval (Eval b)
forall a. Seq a -> Integer -> Eval a
checkedSeqIndex Seq (Eval b)
bs Integer
idx)
indexWordValue (LargeBitsVal n :: Integer
n xs :: SeqMap b w i
xs) idx :: Integer
idx
| Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n = GenValue b w i -> Eval b
forall b w i. GenValue b w i -> Eval b
fromBit (GenValue b w i -> Eval b) -> Eval (GenValue b w i) -> Eval b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
xs Integer
idx
| Bool
otherwise = Integer -> Eval b
forall a. Integer -> Eval a
invalidIndex Integer
idx
updateWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i)
updateWordValue :: WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i)
updateWordValue (WordVal w :: w
w) idx :: Integer
idx (Ready b :: b
b)
| Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< w -> Integer
forall b w i. BitWord b w i => w -> Integer
wordLen w
w = WordValue b w i -> Eval (WordValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue b w i -> Eval (WordValue b w i))
-> WordValue b w i -> Eval (WordValue b w i)
forall a b. (a -> b) -> a -> b
$ w -> WordValue b w i
forall b w i. w -> WordValue b w i
WordVal (w -> WordValue b w i) -> w -> WordValue b w i
forall a b. (a -> b) -> a -> b
$ w -> Integer -> b -> w
forall b w i. BitWord b w i => w -> Integer -> b -> w
wordUpdate w
w Integer
idx b
b
| Bool
otherwise = Integer -> Eval (WordValue b w i)
forall a. Integer -> Eval a
invalidIndex Integer
idx
updateWordValue (WordVal w :: w
w) idx :: Integer
idx b :: Eval b
b
| Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< w -> Integer
forall b w i. BitWord b w i => w -> Integer
wordLen w
w = WordValue b w i -> Eval (WordValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue b w i -> Eval (WordValue b w i))
-> WordValue b w i -> Eval (WordValue b w i)
forall a b. (a -> b) -> a -> b
$ Seq (Eval b) -> WordValue b w i
forall b w i. Seq (Eval b) -> WordValue b w i
BitsVal (Seq (Eval b) -> WordValue b w i)
-> Seq (Eval b) -> WordValue b w i
forall a b. (a -> b) -> a -> b
$ Int -> Eval b -> Seq (Eval b) -> Seq (Eval b)
forall a. Int -> a -> Seq a -> Seq a
Seq.update (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
idx) Eval b
b (Seq (Eval b) -> Seq (Eval b)) -> Seq (Eval b) -> Seq (Eval b)
forall a b. (a -> b) -> a -> b
$ [Eval b] -> Seq (Eval b)
forall a. [a] -> Seq a
Seq.fromList ([Eval b] -> Seq (Eval b)) -> [Eval b] -> Seq (Eval b)
forall a b. (a -> b) -> a -> b
$ (b -> Eval b) -> [b] -> [Eval b]
forall a b. (a -> b) -> [a] -> [b]
map b -> Eval b
forall a. a -> Eval a
ready ([b] -> [Eval b]) -> [b] -> [Eval b]
forall a b. (a -> b) -> a -> b
$ w -> [b]
forall b w i. BitWord b w i => w -> [b]
unpackWord w
w
| Bool
otherwise = Integer -> Eval (WordValue b w i)
forall a. Integer -> Eval a
invalidIndex Integer
idx
updateWordValue (BitsVal bs :: Seq (Eval b)
bs) idx :: Integer
idx b :: Eval b
b
| Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Seq (Eval b) -> Int
forall a. Seq a -> Int
Seq.length Seq (Eval b)
bs) = WordValue b w i -> Eval (WordValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue b w i -> Eval (WordValue b w i))
-> WordValue b w i -> Eval (WordValue b w i)
forall a b. (a -> b) -> a -> b
$ Seq (Eval b) -> WordValue b w i
forall b w i. Seq (Eval b) -> WordValue b w i
BitsVal (Seq (Eval b) -> WordValue b w i)
-> Seq (Eval b) -> WordValue b w i
forall a b. (a -> b) -> a -> b
$ Int -> Eval b -> Seq (Eval b) -> Seq (Eval b)
forall a. Int -> a -> Seq a -> Seq a
Seq.update (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
idx) Eval b
b Seq (Eval b)
bs
| Bool
otherwise = Integer -> Eval (WordValue b w i)
forall a. Integer -> Eval a
invalidIndex Integer
idx
updateWordValue (LargeBitsVal n :: Integer
n xs :: SeqMap b w i
xs) idx :: Integer
idx b :: Eval b
b
| Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n = WordValue b w i -> Eval (WordValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue b w i -> Eval (WordValue b w i))
-> WordValue b w i -> Eval (WordValue b w i)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap b w i -> WordValue b w i
forall b w i. Integer -> SeqMap b w i -> WordValue b w i
LargeBitsVal Integer
n (SeqMap b w i -> WordValue b w i)
-> SeqMap b w i -> WordValue b w i
forall a b. (a -> b) -> a -> b
$ SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
forall b w i.
SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
updateSeqMap SeqMap b w i
xs Integer
idx (b -> GenValue b w i
forall b w i. b -> GenValue b w i
VBit (b -> GenValue b w i) -> Eval b -> Eval (GenValue b w i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval b
b)
| Bool
otherwise = Integer -> Eval (WordValue b w i)
forall a. Integer -> Eval a
invalidIndex Integer
idx
data GenValue b w i
= VRecord ![(Ident, Eval (GenValue b w i))]
| VTuple ![Eval (GenValue b w i)]
| VBit !b
| VInteger !i
| VSeq !Integer !(SeqMap b w i)
| VWord !Integer !(Eval (WordValue b w i))
| VStream !(SeqMap b w i)
| VFun (Eval (GenValue b w i) -> Eval (GenValue b w i))
| VPoly (TValue -> Eval (GenValue b w i))
| VNumPoly (Nat' -> Eval (GenValue b w i))
deriving ((forall x. GenValue b w i -> Rep (GenValue b w i) x)
-> (forall x. Rep (GenValue b w i) x -> GenValue b w i)
-> Generic (GenValue b w i)
forall x. Rep (GenValue b w i) x -> GenValue b w i
forall x. GenValue b w i -> Rep (GenValue b w i) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall b w i x. Rep (GenValue b w i) x -> GenValue b w i
forall b w i x. GenValue b w i -> Rep (GenValue b w i) x
$cto :: forall b w i x. Rep (GenValue b w i) x -> GenValue b w i
$cfrom :: forall b w i x. GenValue b w i -> Rep (GenValue b w i) x
Generic, GenValue b w i -> ()
(GenValue b w i -> ()) -> NFData (GenValue b w i)
forall a. (a -> ()) -> NFData a
forall b w i.
(NFData b, NFData i, NFData w) =>
GenValue b w i -> ()
rnf :: GenValue b w i -> ()
$crnf :: forall b w i.
(NFData b, NFData i, NFData w) =>
GenValue b w i -> ()
NFData)
forceWordValue :: WordValue b w i -> Eval ()
forceWordValue :: WordValue b w i -> Eval ()
forceWordValue (WordVal _w :: w
_w) = () -> Eval ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
forceWordValue (BitsVal bs :: Seq (Eval b)
bs) = (Eval b -> Eval ()) -> Seq (Eval b) -> Eval ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\b :: Eval b
b -> () -> b -> ()
forall a b. a -> b -> a
const () (b -> ()) -> Eval b -> Eval ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval b
b) Seq (Eval b)
bs
forceWordValue (LargeBitsVal n :: Integer
n xs :: SeqMap b w i
xs) = (Eval (GenValue b w i) -> Eval ())
-> [Eval (GenValue b w i)] -> Eval ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\x :: Eval (GenValue b w i)
x -> () -> GenValue b w i -> ()
forall a b. a -> b -> a
const () (GenValue b w i -> ()) -> Eval (GenValue b w i) -> Eval ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval (GenValue b w i)
x) (Integer -> SeqMap b w i -> [Eval (GenValue b w i)]
forall n b w i.
Integral n =>
n -> SeqMap b w i -> [Eval (GenValue b w i)]
enumerateSeqMap Integer
n SeqMap b w i
xs)
forceValue :: GenValue b w i -> Eval ()
forceValue :: GenValue b w i -> Eval ()
forceValue v :: GenValue b w i
v = case GenValue b w i
v of
VRecord fs :: [(Ident, Eval (GenValue b w i))]
fs -> ((Ident, Eval (GenValue b w i)) -> Eval ())
-> [(Ident, Eval (GenValue b w i))] -> Eval ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\x :: (Ident, Eval (GenValue b w i))
x -> GenValue b w i -> Eval ()
forall b w i. GenValue b w i -> Eval ()
forceValue (GenValue b w i -> Eval ()) -> Eval (GenValue b w i) -> Eval ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Ident, Eval (GenValue b w i)) -> Eval (GenValue b w i)
forall a b. (a, b) -> b
snd (Ident, Eval (GenValue b w i))
x) [(Ident, Eval (GenValue b w i))]
fs
VTuple xs :: [Eval (GenValue b w i)]
xs -> (Eval (GenValue b w i) -> Eval ())
-> [Eval (GenValue b w i)] -> Eval ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (GenValue b w i -> Eval ()
forall b w i. GenValue b w i -> Eval ()
forceValue (GenValue b w i -> Eval ()) -> Eval (GenValue b w i) -> Eval ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) [Eval (GenValue b w i)]
xs
VSeq n :: Integer
n xs :: SeqMap b w i
xs -> (Eval (GenValue b w i) -> Eval ())
-> [Eval (GenValue b w i)] -> Eval ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (GenValue b w i -> Eval ()
forall b w i. GenValue b w i -> Eval ()
forceValue (GenValue b w i -> Eval ()) -> Eval (GenValue b w i) -> Eval ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (Integer -> SeqMap b w i -> [Eval (GenValue b w i)]
forall n b w i.
Integral n =>
n -> SeqMap b w i -> [Eval (GenValue b w i)]
enumerateSeqMap Integer
n SeqMap b w i
xs)
VBit _b :: b
_b -> () -> Eval ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
VInteger _i :: i
_i -> () -> Eval ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
VWord _ wv :: Eval (WordValue b w i)
wv -> WordValue b w i -> Eval ()
forall b w i. WordValue b w i -> Eval ()
forceWordValue (WordValue b w i -> Eval ()) -> Eval (WordValue b w i) -> Eval ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (WordValue b w i)
wv
VStream _ -> () -> Eval ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
VFun _ -> () -> Eval ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
VPoly _ -> () -> Eval ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
VNumPoly _ -> () -> Eval ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
instance (Show b, Show w, Show i) => Show (GenValue b w i) where
show :: GenValue b w i -> String
show v :: GenValue b w i
v = case GenValue b w i
v of
VRecord fs :: [(Ident, Eval (GenValue b w i))]
fs -> "record:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Ident] -> String
forall a. Show a => a -> String
show (((Ident, Eval (GenValue b w i)) -> Ident)
-> [(Ident, Eval (GenValue b w i))] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Eval (GenValue b w i)) -> Ident
forall a b. (a, b) -> a
fst [(Ident, Eval (GenValue b w i))]
fs)
VTuple xs :: [Eval (GenValue b w i)]
xs -> "tuple:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Eval (GenValue b w i)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Eval (GenValue b w i)]
xs)
VBit b :: b
b -> b -> String
forall a. Show a => a -> String
show b
b
VInteger i :: i
i -> i -> String
forall a. Show a => a -> String
show i
i
VSeq n :: Integer
n _ -> "seq:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
VWord n :: Integer
n _ -> "word:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
VStream _ -> "stream"
VFun _ -> "fun"
VPoly _ -> "poly"
VNumPoly _ -> "numpoly"
type Value = GenValue Bool BV Integer
defaultPPOpts :: PPOpts
defaultPPOpts :: PPOpts
defaultPPOpts = PPOpts :: Bool -> Int -> Int -> PPOpts
PPOpts { useAscii :: Bool
useAscii = Bool
False, useBase :: Int
useBase = 10, useInfLength :: Int
useInfLength = 5 }
atFst :: Functor f => (a -> f b) -> (a, c) -> f (b, c)
atFst :: (a -> f b) -> (a, c) -> f (b, c)
atFst f :: a -> f b
f (x :: a
x,y :: c
y) = (b -> (b, c)) -> f b -> f (b, c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,c
y) (f b -> f (b, c)) -> f b -> f (b, c)
forall a b. (a -> b) -> a -> b
$ a -> f b
f a
x
atSnd :: Functor f => (a -> f b) -> (c, a) -> f (c, b)
atSnd :: (a -> f b) -> (c, a) -> f (c, b)
atSnd f :: a -> f b
f (x :: c
x,y :: a
y) = (b -> (c, b)) -> f b -> f (c, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (c
x,) (f b -> f (c, b)) -> f b -> f (c, b)
forall a b. (a -> b) -> a -> b
$ a -> f b
f a
y
ppValue :: forall b w i
. BitWord b w i
=> PPOpts
-> GenValue b w i
-> Eval Doc
ppValue :: PPOpts -> GenValue b w i -> Eval Doc
ppValue opts :: PPOpts
opts = GenValue b w i -> Eval Doc
loop
where
loop :: GenValue b w i -> Eval Doc
loop :: GenValue b w i -> Eval Doc
loop val :: GenValue b w i
val = case GenValue b w i
val of
VRecord fs :: [(Ident, Eval (GenValue b w i))]
fs -> do [(Ident, Doc)]
fs' <- ((Ident, Eval (GenValue b w i)) -> Eval (Ident, Doc))
-> [(Ident, Eval (GenValue b w i))] -> Eval [(Ident, Doc)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Eval (GenValue b w i) -> Eval Doc)
-> (Ident, Eval (GenValue b w i)) -> Eval (Ident, Doc)
forall (f :: * -> *) a b c.
Functor f =>
(a -> f b) -> (c, a) -> f (c, b)
atSnd (Eval (GenValue b w i) -> (GenValue b w i -> Eval Doc) -> Eval Doc
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=GenValue b w i -> Eval Doc
loop)) ([(Ident, Eval (GenValue b w i))] -> Eval [(Ident, Doc)])
-> [(Ident, Eval (GenValue b w i))] -> Eval [(Ident, Doc)]
forall a b. (a -> b) -> a -> b
$ [(Ident, Eval (GenValue b w i))]
fs
Doc -> Eval Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Eval Doc) -> Doc -> Eval Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
braces ([Doc] -> Doc
sep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma (((Ident, Doc) -> Doc) -> [(Ident, Doc)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Doc) -> Doc
forall a. PP a => (a, Doc) -> Doc
ppField [(Ident, Doc)]
fs')))
where
ppField :: (a, Doc) -> Doc
ppField (f :: a
f,r :: Doc
r) = a -> Doc
forall a. PP a => a -> Doc
pp a
f Doc -> Doc -> Doc
<+> Char -> Doc
char '=' Doc -> Doc -> Doc
<+> Doc
r
VTuple vals :: [Eval (GenValue b w i)]
vals -> do [Doc]
vals' <- (Eval (GenValue b w i) -> Eval Doc)
-> [Eval (GenValue b w i)] -> Eval [Doc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Eval (GenValue b w i) -> (GenValue b w i -> Eval Doc) -> Eval Doc
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=GenValue b w i -> Eval Doc
loop) [Eval (GenValue b w i)]
vals
Doc -> Eval Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Eval Doc) -> Doc -> Eval Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens ([Doc] -> Doc
sep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc]
vals'))
VBit b :: b
b -> Doc -> Eval Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Eval Doc) -> Doc -> Eval Doc
forall a b. (a -> b) -> a -> b
$ b -> Doc
forall b w i. BitWord b w i => b -> Doc
ppBit b
b
VInteger i :: i
i -> Doc -> Eval Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Eval Doc) -> Doc -> Eval Doc
forall a b. (a -> b) -> a -> b
$ PPOpts -> i -> Doc
forall b w i. BitWord b w i => PPOpts -> i -> Doc
ppInteger PPOpts
opts i
i
VSeq sz :: Integer
sz vals :: SeqMap b w i
vals -> Integer -> SeqMap b w i -> Eval Doc
ppWordSeq Integer
sz SeqMap b w i
vals
VWord _ wv :: Eval (WordValue b w i)
wv -> WordValue b w i -> Eval Doc
ppWordVal (WordValue b w i -> Eval Doc) -> Eval (WordValue b w i) -> Eval Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (WordValue b w i)
wv
VStream vals :: SeqMap b w i
vals -> do [Doc]
vals' <- (Eval (GenValue b w i) -> Eval Doc)
-> [Eval (GenValue b w i)] -> Eval [Doc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Eval (GenValue b w i) -> (GenValue b w i -> Eval Doc) -> Eval Doc
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=GenValue b w i -> Eval Doc
loop) ([Eval (GenValue b w i)] -> Eval [Doc])
-> [Eval (GenValue b w i)] -> Eval [Doc]
forall a b. (a -> b) -> a -> b
$ Int -> SeqMap b w i -> [Eval (GenValue b w i)]
forall n b w i.
Integral n =>
n -> SeqMap b w i -> [Eval (GenValue b w i)]
enumerateSeqMap (PPOpts -> Int
useInfLength PPOpts
opts) SeqMap b w i
vals
Doc -> Eval Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Eval Doc) -> Doc -> Eval Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep
([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma
( [Doc]
vals' [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Doc
text "..."]
)
VFun _ -> Doc -> Eval Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Eval Doc) -> Doc -> Eval Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "<function>"
VPoly _ -> Doc -> Eval Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Eval Doc) -> Doc -> Eval Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "<polymorphic value>"
VNumPoly _ -> Doc -> Eval Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Eval Doc) -> Doc -> Eval Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "<polymorphic value>"
ppWordVal :: WordValue b w i -> Eval Doc
ppWordVal :: WordValue b w i -> Eval Doc
ppWordVal w :: WordValue b w i
w = PPOpts -> w -> Doc
forall b w i. BitWord b w i => PPOpts -> w -> Doc
ppWord PPOpts
opts (w -> Doc) -> Eval w -> Eval Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WordValue b w i -> Eval w
forall b w i. BitWord b w i => WordValue b w i -> Eval w
asWordVal WordValue b w i
w
ppWordSeq :: Integer -> SeqMap b w i -> Eval Doc
ppWordSeq :: Integer -> SeqMap b w i -> Eval Doc
ppWordSeq sz :: Integer
sz vals :: SeqMap b w i
vals = do
[GenValue b w i]
ws <- [Eval (GenValue b w i)] -> Eval [GenValue b w i]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Integer -> SeqMap b w i -> [Eval (GenValue b w i)]
forall n b w i.
Integral n =>
n -> SeqMap b w i -> [Eval (GenValue b w i)]
enumerateSeqMap Integer
sz SeqMap b w i
vals)
case [GenValue b w i]
ws of
w :: GenValue b w i
w : _
| Just l :: Integer
l <- GenValue b w i -> Maybe Integer
forall b w i. BitWord b w i => GenValue b w i -> Maybe Integer
vWordLen GenValue b w i
w
, PPOpts -> Integer -> Bool
asciiMode PPOpts
opts Integer
l
-> do [w]
vs <- (GenValue b w i -> Eval w) -> [GenValue b w i] -> Eval [w]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (String -> GenValue b w i -> Eval w
forall b w i. BitWord b w i => String -> GenValue b w i -> Eval w
fromVWord "ppWordSeq") [GenValue b w i]
ws
case (w -> Maybe Char) -> [w] -> Maybe String
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse w -> Maybe Char
forall b w i. BitWord b w i => w -> Maybe Char
wordAsChar [w]
vs of
Just str :: String
str -> Doc -> Eval Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Eval Doc) -> Doc -> Eval Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (ShowS
forall a. Show a => a -> String
show String
str)
_ -> Doc -> Eval Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Eval Doc) -> Doc -> Eval Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
brackets ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (w -> Doc) -> [w] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (PPOpts -> w -> Doc
forall b w i. BitWord b w i => PPOpts -> w -> Doc
ppWord PPOpts
opts) [w]
vs))
_ -> do [Doc]
ws' <- (GenValue b w i -> Eval Doc) -> [GenValue b w i] -> Eval [Doc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse GenValue b w i -> Eval Doc
loop [GenValue b w i]
ws
Doc -> Eval Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Eval Doc) -> Doc -> Eval Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
brackets ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc]
ws'))
asciiMode :: PPOpts -> Integer -> Bool
asciiMode :: PPOpts -> Integer -> Bool
asciiMode opts :: PPOpts
opts width :: Integer
width = PPOpts -> Bool
useAscii PPOpts
opts Bool -> Bool -> Bool
&& (Integer
width Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 7 Bool -> Bool -> Bool
|| Integer
width Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 8)
integerToChar :: Integer -> Char
integerToChar :: Integer -> Char
integerToChar = Int -> Char
forall a. Enum a => Int -> a
toEnum (Int -> Char) -> (Integer -> Int) -> Integer -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a. Num a => Integer -> a
fromInteger
ppBV :: PPOpts -> BV -> Doc
ppBV :: PPOpts -> BV -> Doc
ppBV opts :: PPOpts
opts (BV width :: Integer
width i :: Integer
i)
| Int
base Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 36 = Integer -> Doc
integer Integer
i
| PPOpts -> Integer -> Bool
asciiMode PPOpts
opts Integer
width = String -> Doc
text (Char -> String
forall a. Show a => a -> String
show (Int -> Char
forall a. Enum a => Int -> a
toEnum (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i) :: Char))
| Bool
otherwise = Doc
prefix Doc -> Doc -> Doc
<.> String -> Doc
text String
value
where
base :: Int
base = PPOpts -> Int
useBase PPOpts
opts
padding :: Int -> Doc
padding bitsPerDigit :: Int
bitsPerDigit = String -> Doc
text (Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
padLen '0')
where
padLen :: Int
padLen | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 = Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
| Bool
otherwise = Int
d
(d :: Int
d,m :: Int
m) = (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
width Int -> Int -> Int
forall a. Num a => a -> a -> a
- (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
value Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
bitsPerDigit))
Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
`divMod` Int
bitsPerDigit
prefix :: Doc
prefix = case Int
base of
2 -> String -> Doc
text "0b" Doc -> Doc -> Doc
<.> Int -> Doc
padding 1
8 -> String -> Doc
text "0o" Doc -> Doc -> Doc
<.> Int -> Doc
padding 3
10 -> Doc
empty
16 -> String -> Doc
text "0x" Doc -> Doc -> Doc
<.> Int -> Doc
padding 4
_ -> String -> Doc
text "0" Doc -> Doc -> Doc
<.> Char -> Doc
char '<' Doc -> Doc -> Doc
<.> Int -> Doc
int Int
base Doc -> Doc -> Doc
<.> Char -> Doc
char '>'
value :: String
value = Integer -> (Int -> Char) -> Integer -> ShowS
forall a. (Integral a, Show a) => a -> (Int -> Char) -> a -> ShowS
showIntAtBase (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
base) (String
digits String -> Int -> Char
forall a. [a] -> Int -> a
!!) Integer
i ""
digits :: String
digits = "0123456789abcdefghijklmnopqrstuvwxyz"
class BitWord b w i | b -> w, w -> i, i -> b where
ppBit :: b -> Doc
ppWord :: PPOpts -> w -> Doc
ppInteger :: PPOpts -> i -> Doc
wordAsChar :: w -> Maybe Char
wordLen :: w -> Integer
bitLit :: Bool -> b
wordLit :: Integer
-> Integer
-> w
integerLit :: Integer
-> i
wordBit :: w -> Integer -> b
wordUpdate :: w -> Integer -> b -> w
packWord :: [b] -> w
unpackWord :: w -> [b]
joinWord :: w -> w -> w
splitWord :: Integer
-> Integer
-> w
-> (w, w)
:: Integer
-> Integer
-> w
-> w
wordPlus :: w -> w -> w
wordMinus :: w -> w -> w
wordMult :: w -> w -> w
wordToInt :: w -> i
intPlus :: i -> i -> i
intMinus :: i -> i -> i
intMult :: i -> i -> i
intModPlus :: Integer -> i -> i -> i
intModMinus :: Integer -> i -> i -> i
intModMult :: Integer -> i -> i -> i
wordFromInt :: Integer -> i -> w
class BitWord b w i => EvalPrims b w i where
evalPrim :: Decl -> Maybe (GenValue b w i)
iteValue :: b
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
mask :: Integer
-> Integer
-> Integer
mask :: Integer -> Integer -> Integer
mask w :: Integer
w i :: Integer
i | Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
Arch.maxBigIntWidth = Integer -> Integer
forall a. Integer -> a
wordTooWide Integer
w
| Bool
otherwise = Integer
i Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. ((1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
w) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1)
instance BitWord Bool BV Integer where
wordLen :: BV -> Integer
wordLen (BV w :: Integer
w _) = Integer
w
wordAsChar :: BV -> Maybe Char
wordAsChar (BV _ x :: Integer
x) = Char -> Maybe Char
forall a. a -> Maybe a
Just (Char -> Maybe Char) -> Char -> Maybe Char
forall a b. (a -> b) -> a -> b
$ Integer -> Char
integerToChar Integer
x
wordBit :: BV -> Integer -> Bool
wordBit (BV w :: Integer
w x :: Integer
x) idx :: Integer
idx = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
idx))
wordUpdate :: BV -> Integer -> Bool -> BV
wordUpdate (BV w :: Integer
w x :: Integer
x) idx :: Integer
idx True = Integer -> Integer -> BV
BV Integer
w (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
setBit Integer
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
idx)))
wordUpdate (BV w :: Integer
w x :: Integer
x) idx :: Integer
idx False = Integer -> Integer -> BV
BV Integer
w (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
clearBit Integer
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
idx)))
ppBit :: Bool -> Doc
ppBit b :: Bool
b | Bool
b = String -> Doc
text "True"
| Bool
otherwise = String -> Doc
text "False"
ppWord :: PPOpts -> BV -> Doc
ppWord = PPOpts -> BV -> Doc
ppBV
ppInteger :: PPOpts -> Integer -> Doc
ppInteger _opts :: PPOpts
_opts i :: Integer
i = Integer -> Doc
integer Integer
i
bitLit :: Bool -> Bool
bitLit b :: Bool
b = Bool
b
wordLit :: Integer -> Integer -> BV
wordLit = Integer -> Integer -> BV
mkBv
integerLit :: Integer -> Integer
integerLit i :: Integer
i = Integer
i
packWord :: [Bool] -> BV
packWord bits :: [Bool]
bits = Integer -> Integer -> BV
BV (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
w) Integer
a
where
w :: Int
w = case [Bool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
bits of
len :: Int
len | Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
Arch.maxBigIntWidth -> Integer -> Int
forall a. Integer -> a
wordTooWide (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len)
| Bool
otherwise -> Int
len
a :: Integer
a = (Integer -> (Int, Bool) -> Integer)
-> Integer -> [(Int, Bool)] -> Integer
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Integer -> (Int, Bool) -> Integer
forall p. Bits p => p -> (Int, Bool) -> p
setb 0 ([Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1, Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- 2 .. 0] [Bool]
bits)
setb :: p -> (Int, Bool) -> p
setb acc :: p
acc (n :: Int
n,b :: Bool
b) | Bool
b = p -> Int -> p
forall a. Bits a => a -> Int -> a
setBit p
acc Int
n
| Bool
otherwise = p
acc
unpackWord :: BV -> [Bool]
unpackWord (BV w :: Integer
w a :: Integer
a) = [ Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a Int
n | Int
n <- [Int
w' Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1, Int
w' Int -> Int -> Int
forall a. Num a => a -> a -> a
- 2 .. 0] ]
where
w' :: Int
w' = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
w
joinWord :: BV -> BV -> BV
joinWord (BV i :: Integer
i x :: Integer
x) (BV j :: Integer
j y :: Integer
y) =
Integer -> Integer -> BV
BV (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j) (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y)
splitWord :: Integer -> Integer -> BV -> (BV, BV)
splitWord leftW :: Integer
leftW rightW :: Integer
rightW (BV _ x :: Integer
x) =
( Integer -> Integer -> BV
BV Integer
leftW (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
rightW)), Integer -> Integer -> BV
mkBv Integer
rightW Integer
x )
extractWord :: Integer -> Integer -> BV -> BV
extractWord n :: Integer
n i :: Integer
i (BV _ x :: Integer
x) = Integer -> Integer -> BV
mkBv Integer
n (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i))
wordPlus :: BV -> BV -> BV
wordPlus (BV i :: Integer
i x :: Integer
x) (BV j :: Integer
j y :: Integer
y)
| Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = Integer -> Integer -> BV
mkBv Integer
i (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
y)
| Bool
otherwise = String -> [String] -> BV
forall a. HasCallStack => String -> [String] -> a
panic "Attempt to add words of different sizes: wordPlus" []
wordMinus :: BV -> BV -> BV
wordMinus (BV i :: Integer
i x :: Integer
x) (BV j :: Integer
j y :: Integer
y)
| Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = Integer -> Integer -> BV
mkBv Integer
i (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
y)
| Bool
otherwise = String -> [String] -> BV
forall a. HasCallStack => String -> [String] -> a
panic "Attempt to subtract words of different sizes: wordMinus" []
wordMult :: BV -> BV -> BV
wordMult (BV i :: Integer
i x :: Integer
x) (BV j :: Integer
j y :: Integer
y)
| Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = Integer -> Integer -> BV
mkBv Integer
i (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
y)
| Bool
otherwise = String -> [String] -> BV
forall a. HasCallStack => String -> [String] -> a
panic "Attempt to multiply words of different sizes: wordMult" []
intPlus :: Integer -> Integer -> Integer
intPlus x :: Integer
x y :: Integer
y = Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y
intMinus :: Integer -> Integer -> Integer
intMinus x :: Integer
x y :: Integer
y = Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y
intMult :: Integer -> Integer -> Integer
intMult x :: Integer
x y :: Integer
y = Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y
intModPlus :: Integer -> Integer -> Integer -> Integer
intModPlus m :: Integer
m x :: Integer
x y :: Integer
y = (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m
intModMinus :: Integer -> Integer -> Integer -> Integer
intModMinus m :: Integer
m x :: Integer
x y :: Integer
y = (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m
intModMult :: Integer -> Integer -> Integer -> Integer
intModMult m :: Integer
m x :: Integer
x y :: Integer
y = (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m
wordToInt :: BV -> Integer
wordToInt (BV _ x :: Integer
x) = Integer
x
wordFromInt :: Integer -> Integer -> BV
wordFromInt w :: Integer
w x :: Integer
x = Integer -> Integer -> BV
mkBv Integer
w Integer
x
word :: BitWord b w i => Integer -> Integer -> GenValue b w i
word :: Integer -> Integer -> GenValue b w i
word n :: Integer
n i :: Integer
i
| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
Arch.maxBigIntWidth = Integer -> GenValue b w i
forall a. Integer -> a
wordTooWide Integer
n
| Bool
otherwise = Integer -> Eval (WordValue b w i) -> GenValue b w i
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord Integer
n (Eval (WordValue b w i) -> GenValue b w i)
-> Eval (WordValue b w i) -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ WordValue b w i -> Eval (WordValue b w i)
forall a. a -> Eval a
ready (WordValue b w i -> Eval (WordValue b w i))
-> WordValue b w i -> Eval (WordValue b w i)
forall a b. (a -> b) -> a -> b
$ w -> WordValue b w i
forall b w i. w -> WordValue b w i
WordVal (w -> WordValue b w i) -> w -> WordValue b w i
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> w
forall b w i. BitWord b w i => Integer -> Integer -> w
wordLit Integer
n Integer
i
lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
lam = (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
VFun
wlam :: BitWord b w i => (w -> Eval (GenValue b w i)) -> GenValue b w i
wlam :: (w -> Eval (GenValue b w i)) -> GenValue b w i
wlam f :: w -> Eval (GenValue b w i)
f = (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
VFun (\x :: Eval (GenValue b w i)
x -> Eval (GenValue b w i)
x Eval (GenValue b w i) -> (GenValue b w i -> Eval w) -> Eval w
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> GenValue b w i -> Eval w
forall b w i. BitWord b w i => String -> GenValue b w i -> Eval w
fromVWord "wlam" Eval w -> (w -> Eval (GenValue b w i)) -> Eval (GenValue b w i)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= w -> Eval (GenValue b w i)
f)
tlam :: (TValue -> GenValue b w i) -> GenValue b w i
tlam :: (TValue -> GenValue b w i) -> GenValue b w i
tlam f :: TValue -> GenValue b w i
f = (TValue -> Eval (GenValue b w i)) -> GenValue b w i
forall b w i. (TValue -> Eval (GenValue b w i)) -> GenValue b w i
VPoly (GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> (TValue -> GenValue b w i) -> TValue -> Eval (GenValue b w i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TValue -> GenValue b w i
f)
nlam :: (Nat' -> GenValue b w i) -> GenValue b w i
nlam :: (Nat' -> GenValue b w i) -> GenValue b w i
nlam f :: Nat' -> GenValue b w i
f = (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
forall b w i. (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
VNumPoly (GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> (Nat' -> GenValue b w i) -> Nat' -> Eval (GenValue b w i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat' -> GenValue b w i
f)
toStream :: [GenValue b w i] -> Eval (GenValue b w i)
toStream :: [GenValue b w i] -> Eval (GenValue b w i)
toStream vs :: [GenValue b w i]
vs =
SeqMap b w i -> GenValue b w i
forall b w i. SeqMap b w i -> GenValue b w i
VStream (SeqMap b w i -> GenValue b w i)
-> Eval (SeqMap b w i) -> Eval (GenValue b w i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Eval (GenValue b w i)] -> Eval (SeqMap b w i)
forall b w i. [Eval (GenValue b w i)] -> Eval (SeqMap b w i)
infiniteSeqMap ((GenValue b w i -> Eval (GenValue b w i))
-> [GenValue b w i] -> [Eval (GenValue b w i)]
forall a b. (a -> b) -> [a] -> [b]
map GenValue b w i -> Eval (GenValue b w i)
forall a. a -> Eval a
ready [GenValue b w i]
vs)
toFinSeq :: BitWord b w i
=> Integer -> TValue -> [GenValue b w i] -> GenValue b w i
toFinSeq :: Integer -> TValue -> [GenValue b w i] -> GenValue b w i
toFinSeq len :: Integer
len elty :: TValue
elty vs :: [GenValue b w i]
vs
| TValue -> Bool
isTBit TValue
elty = Integer -> Eval (WordValue b w i) -> GenValue b w i
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord Integer
len (Eval (WordValue b w i) -> GenValue b w i)
-> Eval (WordValue b w i) -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ WordValue b w i -> Eval (WordValue b w i)
forall a. a -> Eval a
ready (WordValue b w i -> Eval (WordValue b w i))
-> WordValue b w i -> Eval (WordValue b w i)
forall a b. (a -> b) -> a -> b
$ w -> WordValue b w i
forall b w i. w -> WordValue b w i
WordVal (w -> WordValue b w i) -> w -> WordValue b w i
forall a b. (a -> b) -> a -> b
$ [b] -> w
forall b w i. BitWord b w i => [b] -> w
packWord ([b] -> w) -> [b] -> w
forall a b. (a -> b) -> a -> b
$ (GenValue b w i -> b) -> [GenValue b w i] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map GenValue b w i -> b
forall b w i. GenValue b w i -> b
fromVBit [GenValue b w i]
vs
| Bool
otherwise = Integer -> SeqMap b w i -> GenValue b w i
forall b w i. Integer -> SeqMap b w i -> GenValue b w i
VSeq Integer
len (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ [Eval (GenValue b w i)] -> SeqMap b w i
forall b w i. [Eval (GenValue b w i)] -> SeqMap b w i
finiteSeqMap ((GenValue b w i -> Eval (GenValue b w i))
-> [GenValue b w i] -> [Eval (GenValue b w i)]
forall a b. (a -> b) -> [a] -> [b]
map GenValue b w i -> Eval (GenValue b w i)
forall a. a -> Eval a
ready [GenValue b w i]
vs)
boolToWord :: [Bool] -> Value
boolToWord :: [Bool] -> Value
boolToWord bs :: [Bool]
bs = Integer -> Eval (WordValue Bool BV Integer) -> Value
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord ([Bool] -> Integer
forall i a. Num i => [a] -> i
genericLength [Bool]
bs) (Eval (WordValue Bool BV Integer) -> Value)
-> Eval (WordValue Bool BV Integer) -> Value
forall a b. (a -> b) -> a -> b
$ WordValue Bool BV Integer -> Eval (WordValue Bool BV Integer)
forall a. a -> Eval a
ready (WordValue Bool BV Integer -> Eval (WordValue Bool BV Integer))
-> WordValue Bool BV Integer -> Eval (WordValue Bool BV Integer)
forall a b. (a -> b) -> a -> b
$ BV -> WordValue Bool BV Integer
forall b w i. w -> WordValue b w i
WordVal (BV -> WordValue Bool BV Integer)
-> BV -> WordValue Bool BV Integer
forall a b. (a -> b) -> a -> b
$ [Bool] -> BV
forall b w i. BitWord b w i => [b] -> w
packWord [Bool]
bs
toSeq :: BitWord b w i
=> Nat' -> TValue -> [GenValue b w i] -> Eval (GenValue b w i)
toSeq :: Nat' -> TValue -> [GenValue b w i] -> Eval (GenValue b w i)
toSeq len :: Nat'
len elty :: TValue
elty vals :: [GenValue b w i]
vals = case Nat'
len of
Nat n :: Integer
n -> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ Integer -> TValue -> [GenValue b w i] -> GenValue b w i
forall b w i.
BitWord b w i =>
Integer -> TValue -> [GenValue b w i] -> GenValue b w i
toFinSeq Integer
n TValue
elty [GenValue b w i]
vals
Inf -> [GenValue b w i] -> Eval (GenValue b w i)
forall b w i. [GenValue b w i] -> Eval (GenValue b w i)
toStream [GenValue b w i]
vals
mkSeq :: Nat' -> TValue -> SeqMap b w i -> GenValue b w i
mkSeq :: Nat' -> TValue -> SeqMap b w i -> GenValue b w i
mkSeq len :: Nat'
len elty :: TValue
elty vals :: SeqMap b w i
vals = case Nat'
len of
Nat n :: Integer
n
| TValue -> Bool
isTBit TValue
elty -> Integer -> Eval (WordValue b w i) -> GenValue b w i
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord Integer
n (Eval (WordValue b w i) -> GenValue b w i)
-> Eval (WordValue b w i) -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ WordValue b w i -> Eval (WordValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue b w i -> Eval (WordValue b w i))
-> WordValue b w i -> Eval (WordValue b w i)
forall a b. (a -> b) -> a -> b
$ Seq (Eval b) -> WordValue b w i
forall b w i. Seq (Eval b) -> WordValue b w i
BitsVal (Seq (Eval b) -> WordValue b w i)
-> Seq (Eval b) -> WordValue b w i
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> Eval b) -> Seq (Eval b)
forall a. Int -> (Int -> a) -> Seq a
Seq.fromFunction (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n) ((Int -> Eval b) -> Seq (Eval b))
-> (Int -> Eval b) -> Seq (Eval b)
forall a b. (a -> b) -> a -> b
$ \i :: Int
i ->
GenValue b w i -> b
forall b w i. GenValue b w i -> b
fromVBit (GenValue b w i -> b) -> Eval (GenValue b w i) -> Eval b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
vals (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i)
| Bool
otherwise -> Integer -> SeqMap b w i -> GenValue b w i
forall b w i. Integer -> SeqMap b w i -> GenValue b w i
VSeq Integer
n SeqMap b w i
vals
Inf -> SeqMap b w i -> GenValue b w i
forall b w i. SeqMap b w i -> GenValue b w i
VStream SeqMap b w i
vals
fromVBit :: GenValue b w i -> b
fromVBit :: GenValue b w i -> b
fromVBit val :: GenValue b w i
val = case GenValue b w i
val of
VBit b :: b
b -> b
b
_ -> String -> [String] -> b
forall a. HasCallStack => String -> [String] -> a
evalPanic "fromVBit" ["not a Bit"]
fromVInteger :: GenValue b w i -> i
fromVInteger :: GenValue b w i -> i
fromVInteger val :: GenValue b w i
val = case GenValue b w i
val of
VInteger i :: i
i -> i
i
_ -> String -> [String] -> i
forall a. HasCallStack => String -> [String] -> a
evalPanic "fromVInteger" ["not an Integer"]
fromVSeq :: GenValue b w i -> SeqMap b w i
fromVSeq :: GenValue b w i -> SeqMap b w i
fromVSeq val :: GenValue b w i
val = case GenValue b w i
val of
VSeq _ vs :: SeqMap b w i
vs -> SeqMap b w i
vs
_ -> String -> [String] -> SeqMap b w i
forall a. HasCallStack => String -> [String] -> a
evalPanic "fromVSeq" ["not a sequence"]
fromSeq :: forall b w i. BitWord b w i => String -> GenValue b w i -> Eval (SeqMap b w i)
fromSeq :: String -> GenValue b w i -> Eval (SeqMap b w i)
fromSeq msg :: String
msg val :: GenValue b w i
val = case GenValue b w i
val of
VSeq _ vs :: SeqMap b w i
vs -> SeqMap b w i -> Eval (SeqMap b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return SeqMap b w i
vs
VStream vs :: SeqMap b w i
vs -> SeqMap b w i -> Eval (SeqMap b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return SeqMap b w i
vs
_ -> String -> [String] -> Eval (SeqMap b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "fromSeq" ["not a sequence", String
msg]
fromStr :: Value -> Eval String
fromStr :: Value -> Eval String
fromStr (VSeq n :: Integer
n vals :: SeqMap Bool BV Integer
vals) =
(Eval Value -> Eval Char) -> [Eval Value] -> Eval String
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\x :: Eval Value
x -> Int -> Char
forall a. Enum a => Int -> a
toEnum (Int -> Char) -> (Integer -> Int) -> Integer -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Char) -> Eval Integer -> Eval Char
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Value -> Eval Integer
fromWord "fromStr" (Value -> Eval Integer) -> Eval Value -> Eval Integer
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval Value
x)) (Integer -> SeqMap Bool BV Integer -> [Eval Value]
forall n b w i.
Integral n =>
n -> SeqMap b w i -> [Eval (GenValue b w i)]
enumerateSeqMap Integer
n SeqMap Bool BV Integer
vals)
fromStr _ = String -> [String] -> Eval String
forall a. HasCallStack => String -> [String] -> a
evalPanic "fromStr" ["Not a finite sequence"]
fromBit :: GenValue b w i -> Eval b
fromBit :: GenValue b w i -> Eval b
fromBit (VBit b :: b
b) = b -> Eval b
forall (m :: * -> *) a. Monad m => a -> m a
return b
b
fromBit _ = String -> [String] -> Eval b
forall a. HasCallStack => String -> [String] -> a
evalPanic "fromBit" ["Not a bit value"]
fromWordVal :: String -> GenValue b w i -> Eval (WordValue b w i)
fromWordVal :: String -> GenValue b w i -> Eval (WordValue b w i)
fromWordVal _msg :: String
_msg (VWord _ wval :: Eval (WordValue b w i)
wval) = Eval (WordValue b w i)
wval
fromWordVal msg :: String
msg _ = String -> [String] -> Eval (WordValue b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "fromWordVal" ["not a word value", String
msg]
fromVWord :: BitWord b w i => String -> GenValue b w i -> Eval w
fromVWord :: String -> GenValue b w i -> Eval w
fromVWord _msg :: String
_msg (VWord _ wval :: Eval (WordValue b w i)
wval) = Eval (WordValue b w i)
wval Eval (WordValue b w i) -> (WordValue b w i -> Eval w) -> Eval w
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= WordValue b w i -> Eval w
forall b w i. BitWord b w i => WordValue b w i -> Eval w
asWordVal
fromVWord msg :: String
msg _ = String -> [String] -> Eval w
forall a. HasCallStack => String -> [String] -> a
evalPanic "fromVWord" ["not a word", String
msg]
vWordLen :: BitWord b w i => GenValue b w i -> Maybe Integer
vWordLen :: GenValue b w i -> Maybe Integer
vWordLen val :: GenValue b w i
val = case GenValue b w i
val of
VWord n :: Integer
n _wv :: Eval (WordValue b w i)
_wv -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n
_ -> Maybe Integer
forall a. Maybe a
Nothing
tryFromBits :: BitWord b w i => [Eval (GenValue b w i)] -> Maybe w
tryFromBits :: [Eval (GenValue b w i)] -> Maybe w
tryFromBits = ([b] -> [b]) -> [Eval (GenValue b w i)] -> Maybe w
forall b a i a w i.
BitWord b a i =>
([a] -> [b]) -> [Eval (GenValue a w i)] -> Maybe a
go [b] -> [b]
forall a. a -> a
id
where
go :: ([a] -> [b]) -> [Eval (GenValue a w i)] -> Maybe a
go f :: [a] -> [b]
f [] = a -> Maybe a
forall a. a -> Maybe a
Just ([b] -> a
forall b w i. BitWord b w i => [b] -> w
packWord ([a] -> [b]
f []))
go f :: [a] -> [b]
f (Ready (VBit b :: a
b) : vs :: [Eval (GenValue a w i)]
vs) = ([a] -> [b]) -> [Eval (GenValue a w i)] -> Maybe a
go ([a] -> [b]
f ([a] -> [b]) -> ([a] -> [a]) -> [a] -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
b a -> [a] -> [a]
forall a. a -> [a] -> [a]
:)) [Eval (GenValue a w i)]
vs
go _ (_ : _) = Maybe a
forall a. Maybe a
Nothing
fromWord :: String -> Value -> Eval Integer
fromWord :: String -> Value -> Eval Integer
fromWord msg :: String
msg val :: Value
val = BV -> Integer
bvVal (BV -> Integer) -> Eval BV -> Eval Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Value -> Eval BV
forall b w i. BitWord b w i => String -> GenValue b w i -> Eval w
fromVWord String
msg Value
val
fromVFun :: GenValue b w i -> (Eval (GenValue b w i) -> Eval (GenValue b w i))
fromVFun :: GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)
fromVFun val :: GenValue b w i
val = case GenValue b w i
val of
VFun f :: Eval (GenValue b w i) -> Eval (GenValue b w i)
f -> Eval (GenValue b w i) -> Eval (GenValue b w i)
f
_ -> String
-> [String] -> Eval (GenValue b w i) -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "fromVFun" ["not a function"]
fromVPoly :: GenValue b w i -> (TValue -> Eval (GenValue b w i))
fromVPoly :: GenValue b w i -> TValue -> Eval (GenValue b w i)
fromVPoly val :: GenValue b w i
val = case GenValue b w i
val of
VPoly f :: TValue -> Eval (GenValue b w i)
f -> TValue -> Eval (GenValue b w i)
f
_ -> String -> [String] -> TValue -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "fromVPoly" ["not a polymorphic value"]
fromVNumPoly :: GenValue b w i -> (Nat' -> Eval (GenValue b w i))
fromVNumPoly :: GenValue b w i -> Nat' -> Eval (GenValue b w i)
fromVNumPoly val :: GenValue b w i
val = case GenValue b w i
val of
VNumPoly f :: Nat' -> Eval (GenValue b w i)
f -> Nat' -> Eval (GenValue b w i)
f
_ -> String -> [String] -> Nat' -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "fromVNumPoly" ["not a polymorphic value"]
fromVTuple :: GenValue b w i -> [Eval (GenValue b w i)]
fromVTuple :: GenValue b w i -> [Eval (GenValue b w i)]
fromVTuple val :: GenValue b w i
val = case GenValue b w i
val of
VTuple vs :: [Eval (GenValue b w i)]
vs -> [Eval (GenValue b w i)]
vs
_ -> String -> [String] -> [Eval (GenValue b w i)]
forall a. HasCallStack => String -> [String] -> a
evalPanic "fromVTuple" ["not a tuple"]
fromVRecord :: GenValue b w i -> [(Ident, Eval (GenValue b w i))]
fromVRecord :: GenValue b w i -> [(Ident, Eval (GenValue b w i))]
fromVRecord val :: GenValue b w i
val = case GenValue b w i
val of
VRecord fs :: [(Ident, Eval (GenValue b w i))]
fs -> [(Ident, Eval (GenValue b w i))]
fs
_ -> String -> [String] -> [(Ident, Eval (GenValue b w i))]
forall a. HasCallStack => String -> [String] -> a
evalPanic "fromVRecord" ["not a record"]
lookupRecord :: Ident -> GenValue b w i -> Eval (GenValue b w i)
lookupRecord :: Ident -> GenValue b w i -> Eval (GenValue b w i)
lookupRecord f :: Ident
f rec :: GenValue b w i
rec = case Ident
-> [(Ident, Eval (GenValue b w i))]
-> Maybe (Eval (GenValue b w i))
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
f (GenValue b w i -> [(Ident, Eval (GenValue b w i))]
forall b w i. GenValue b w i -> [(Ident, Eval (GenValue b w i))]
fromVRecord GenValue b w i
rec) of
Just val :: Eval (GenValue b w i)
val -> Eval (GenValue b w i)
val
Nothing -> String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "lookupRecord" ["malformed record"]
toExpr :: PrimMap -> Type -> Value -> Eval (Maybe Expr)
toExpr :: PrimMap -> Type -> Value -> Eval (Maybe Expr)
toExpr prims :: PrimMap
prims t0 :: Type
t0 v0 :: Value
v0 = ChoiceT Eval Expr -> Eval (Maybe Expr)
forall (m :: * -> *) a. Monad m => ChoiceT m a -> m (Maybe a)
findOne (Type -> Value -> ChoiceT Eval Expr
go Type
t0 Value
v0)
where
prim :: String -> Expr
prim n :: String
n = PrimMap -> Ident -> Expr
ePrim PrimMap
prims (Text -> Ident
mkIdent (String -> Text
T.pack String
n))
go :: Type -> Value -> ChoiceT Eval Expr
go :: Type -> Value -> ChoiceT Eval Expr
go ty :: Type
ty val :: Value
val = case (Type -> Type
tNoUser Type
ty, Value
val) of
(TRec tfs :: [(Ident, Type)]
tfs, VRecord vfs :: [(Ident, Eval Value)]
vfs) -> do
let fns :: [Ident]
fns = ((Ident, Eval Value) -> Ident) -> [(Ident, Eval Value)] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Eval Value) -> Ident
forall a b. (a, b) -> a
fst [(Ident, Eval Value)]
vfs
Bool -> ChoiceT Eval ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (((Ident, Type) -> Ident) -> [(Ident, Type)] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Type) -> Ident
forall a b. (a, b) -> a
fst [(Ident, Type)]
tfs [Ident] -> [Ident] -> Bool
forall a. Eq a => a -> a -> Bool
== [Ident]
fns)
[Expr]
fes <- (Type -> Value -> ChoiceT Eval Expr)
-> [Type] -> [Value] -> ChoiceT Eval [Expr]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Type -> Value -> ChoiceT Eval Expr
go (((Ident, Type) -> Type) -> [(Ident, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Type) -> Type
forall a b. (a, b) -> b
snd [(Ident, Type)]
tfs) ([Value] -> ChoiceT Eval [Expr])
-> ChoiceT Eval [Value] -> ChoiceT Eval [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval [Value] -> ChoiceT Eval [Value]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (((Ident, Eval Value) -> Eval Value)
-> [(Ident, Eval Value)] -> Eval [Value]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Ident, Eval Value) -> Eval Value
forall a b. (a, b) -> b
snd [(Ident, Eval Value)]
vfs)
Expr -> ChoiceT Eval Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ChoiceT Eval Expr) -> Expr -> ChoiceT Eval Expr
forall a b. (a -> b) -> a -> b
$ [(Ident, Expr)] -> Expr
ERec ([Ident] -> [Expr] -> [(Ident, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
fns [Expr]
fes)
(TCon (TC (TCTuple tl :: Int
tl)) ts :: [Type]
ts, VTuple tvs :: [Eval Value]
tvs) -> do
Bool -> ChoiceT Eval ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Int
tl Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== ([Eval Value] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Eval Value]
tvs))
[Expr] -> Expr
ETuple ([Expr] -> Expr) -> ChoiceT Eval [Expr] -> ChoiceT Eval Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ((Type -> Value -> ChoiceT Eval Expr)
-> [Type] -> [Value] -> ChoiceT Eval [Expr]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Type -> Value -> ChoiceT Eval Expr
go [Type]
ts ([Value] -> ChoiceT Eval [Expr])
-> ChoiceT Eval [Value] -> ChoiceT Eval [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval [Value] -> ChoiceT Eval [Value]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift ([Eval Value] -> Eval [Value]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Eval Value]
tvs))
(TCon (TC TCBit) [], VBit True ) -> Expr -> ChoiceT Eval Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Expr
prim "True")
(TCon (TC TCBit) [], VBit False) -> Expr -> ChoiceT Eval Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Expr
prim "False")
(TCon (TC TCInteger) [], VInteger i :: Integer
i) ->
Expr -> ChoiceT Eval Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ChoiceT Eval Expr) -> Expr -> ChoiceT Eval Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Type -> Expr
ETApp (Expr -> Type -> Expr
ETApp (String -> Expr
prim "number") (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
i)) Type
ty
(TCon (TC TCIntMod) [_n :: Type
_n], VInteger i :: Integer
i) ->
Expr -> ChoiceT Eval Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ChoiceT Eval Expr) -> Expr -> ChoiceT Eval Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Type -> Expr
ETApp (Expr -> Type -> Expr
ETApp (String -> Expr
prim "number") (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
i)) Type
ty
(TCon (TC TCSeq) [a :: Type
a,b :: Type
b], VSeq 0 _) -> do
Bool -> ChoiceT Eval ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
a Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
tZero)
Expr -> ChoiceT Eval Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ChoiceT Eval Expr) -> Expr -> ChoiceT Eval Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Type -> Expr
EList [] Type
b
(TCon (TC TCSeq) [a :: Type
a,b :: Type
b], VSeq n :: Integer
n svs :: SeqMap Bool BV Integer
svs) -> do
Bool -> ChoiceT Eval ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
a Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
n)
[Expr]
ses <- (Value -> ChoiceT Eval Expr) -> [Value] -> ChoiceT Eval [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> Value -> ChoiceT Eval Expr
go Type
b) ([Value] -> ChoiceT Eval [Expr])
-> ChoiceT Eval [Value] -> ChoiceT Eval [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval [Value] -> ChoiceT Eval [Value]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift ([Eval Value] -> Eval [Value]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Integer -> SeqMap Bool BV Integer -> [Eval Value]
forall n b w i.
Integral n =>
n -> SeqMap b w i -> [Eval (GenValue b w i)]
enumerateSeqMap Integer
n SeqMap Bool BV Integer
svs))
Expr -> ChoiceT Eval Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ChoiceT Eval Expr) -> Expr -> ChoiceT Eval Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Type -> Expr
EList [Expr]
ses Type
b
(TCon (TC TCSeq) [a :: Type
a,(TCon (TC TCBit) [])], VWord _ wval :: Eval (WordValue Bool BV Integer)
wval) -> do
BV w :: Integer
w v :: Integer
v <- Eval BV -> ChoiceT Eval BV
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (WordValue Bool BV Integer -> Eval BV
forall b w i. BitWord b w i => WordValue b w i -> Eval w
asWordVal (WordValue Bool BV Integer -> Eval BV)
-> Eval (WordValue Bool BV Integer) -> Eval BV
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (WordValue Bool BV Integer)
wval)
Bool -> ChoiceT Eval ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
a Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
w)
Expr -> ChoiceT Eval Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ChoiceT Eval Expr) -> Expr -> ChoiceT Eval Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Type -> Expr
ETApp (Expr -> Type -> Expr
ETApp (String -> Expr
prim "number") (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
v)) Type
ty
(_, VStream _) -> String -> ChoiceT Eval Expr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "cannot construct infinite expressions"
(_, VFun _) -> String -> ChoiceT Eval Expr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "cannot convert function values to expressions"
(_, VPoly _) -> String -> ChoiceT Eval Expr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "cannot convert polymorphic values to expressions"
_ -> do Doc
doc <- Eval Doc -> ChoiceT Eval Doc
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (PPOpts -> Value -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
ppValue PPOpts
defaultPPOpts Value
val)
String -> [String] -> ChoiceT Eval Expr
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.Eval.Value.toExpr"
["type mismatch:"
, Type -> String
forall a. PP a => a -> String
pretty Type
ty
, Doc -> String
render Doc
doc
]