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

{-# 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

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

-- | Concrete bitvector values: width, value
-- Invariant: The value must be within the range 0 .. 2^width-1
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

-- | Apply an integer function to the values of bitvectors.
--   This function assumes both bitvectors are the same width.
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)

-- | Apply an integer function to the values of a bitvector.
--   This function assumes the function will not require masking.
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

-- | Smart constructor for 'BV's that checks for the width limit
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)

-- | A sequence map represents a mapping from nonnegative integer indices
--   to values.  These are used to represent both finite and infinite sequences.
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 ()

-- | Generate a finite sequence map from a list of values
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

-- | Generate an infinite sequence map from a stream of values
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 =
   -- TODO: use an int-trie?
   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)

-- | Create a finite list of length `n` of the values from [0..n-1] in
--   the given the sequence emap.
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] ]

-- | Create an infinite stream of all the values in a sequence map
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..] ]

-- | Reverse the order of a finite sequence map
reverseSeqMap :: Integer     -- ^ Size of the sequence map
              -> 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

-- | Concatenate the first `n` values of the first sequence map onto the
--   beginning of the second sequence map.
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)

-- | Given a number `n` and a sequence map, return two new sequence maps:
--   the first containing the values from `[0..n-1]` and the next containing
--   the values from `n` onward.
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)

-- | Drop the first @n@ elements of the given @SeqMap@.
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)

-- | Given a sequence map, return a new sequence map that is memoized using
--   a finite map memo table.
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

-- | Apply the given evaluation function pointwise to the two given
--   sequence maps.
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))

-- | Apply the given function to each value in the given sequence map
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)

-- | For efficiency reasons, we handle finite sequences of bits as special cases
--   in the evaluator.  In cases where we know it is safe to do so, we prefer to
--   used a "packed word" representation of bit sequences.  This allows us to rely
--   directly on Integer types (in the concrete evaluator) and SBV's Word types (in
--   the symbolic simulator).
--
--   However, if we cannot be sure all the bits of the sequence
--   will eventually be forced, we must instead rely on an explicit sequence of bits
--   representation.
data WordValue b w i
  = WordVal !w                              -- ^ Packed word representation for bit sequences.
  | BitsVal !(Seq.Seq (Eval b))             -- ^ Sequence of thunks representing bits.
  | LargeBitsVal !Integer !(SeqMap b w i )  -- ^ A large bitvector sequence, represented as a
                                            --   @SeqMap@ of bits.
 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)

-- | An arbitrarily-chosen number of elements where we switch from a dense
--   sequence representation of bit-level words to @SeqMap@ representation.
largeBitSize :: Integer
largeBitSize :: Integer
largeBitSize = 1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` 16

-- | Force a word value into packed word form
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)

-- | Force a word value into a sequence of bits
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

-- | Turn a word value into a sequence of bits, forcing each bit.
--   The sequence is returned in big-endian order.
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)

-- | Turn a word value into a sequence of bits, forcing each bit.
--   The sequence is returned in reverse of the usual order, which is little-endian order.
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))

-- | Compute the size of a word value
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

-- | Select an individual bit from a word value
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

-- | Produce a new @WordValue@ from the one given by updating the @i@th bit with the
--   given bit value.
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

-- | Generic value type, parameterized by bit and word types.
--
--   NOTE: we maintain an important invariant regarding sequence types.
--   `VSeq` must never be used for finite sequences of bits.
--   Always use the `VWord` constructor instead!  Infinite sequences of bits
--   are handled by the `VStream` constructor, just as for other types.
data GenValue b w i
  = VRecord ![(Ident, Eval (GenValue b w i))] -- ^ @ { .. } @
  | VTuple ![Eval (GenValue b w i)]           -- ^ @ ( .. ) @
  | VBit !b                                   -- ^ @ Bit    @
  | VInteger !i                               -- ^ @ Integer @ or @ Z n @
  | VSeq !Integer !(SeqMap b w i)             -- ^ @ [n]a   @
                                              --   Invariant: VSeq is never a sequence of bits
  | VWord !Integer !(Eval (WordValue b w i))  -- ^ @ [n]Bit @
  | VStream !(SeqMap b w i)                   -- ^ @ [inf]a @
  | VFun (Eval (GenValue b w i) -> Eval (GenValue b w i)) -- ^ functions
  | VPoly (TValue -> Eval (GenValue b w i))   -- ^ polymorphic values (kind *)
  | VNumPoly (Nat' -> Eval (GenValue b w i))  -- ^ polymorphic values (kind #)
 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)


-- | Force the evaluation of a word value
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)

-- | Force the evaluation of a value
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


-- Pretty Printing -------------------------------------------------------------

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 -- not sure how to rule this out
  | 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"


-- | This type class defines a collection of operations on bits and words that
--   are necessary to define generic evaluator primitives that operate on both concrete
--   and symbolic values uniformly.
class BitWord b w i | b -> w, w -> i, i -> b where
  -- | Pretty-print an individual bit
  ppBit :: b -> Doc

  -- | Pretty-print a word value
  ppWord :: PPOpts -> w -> Doc

  -- | Pretty-print an integer value
  ppInteger :: PPOpts -> i -> Doc

  -- | Attempt to render a word value as an ASCII character.  Return `Nothing`
  --   if the character value is unknown (e.g., for symbolic values).
  wordAsChar :: w -> Maybe Char

  -- | The number of bits in a word value.
  wordLen :: w -> Integer

  -- | Construct a literal bit value from a boolean.
  bitLit :: Bool -> b

  -- | Construct a literal word value given a bit width and a value.
  wordLit :: Integer -- ^ Width
          -> Integer -- ^ Value
          -> w

  -- | Construct a literal integer value from the given integer.
  integerLit :: Integer -- ^ Value
             -> i

  -- | Extract the numbered bit from the word.
  --
  --   NOTE: this assumes that the sequence of bits is big-endian and finite, so the
  --   bit numbered 0 is the most significant bit.
  wordBit :: w -> Integer -> b

  -- | Update the numbered bit in the word.
  --
  --   NOTE: this assumes that the sequence of bits is big-endian and finite, so the
  --   bit numbered 0 is the most significant bit.
  wordUpdate :: w -> Integer -> b -> w

  -- | Construct a word value from a finite sequence of bits.
  --   NOTE: this assumes that the sequence of bits is big-endian and finite, so the
  --   first element of the list will be the most significant bit.
  packWord :: [b] -> w

  -- | Deconstruct a packed word value in to a finite sequence of bits.
  --   NOTE: this produces a list of bits that represent a big-endian word, so
  --   the most significant bit is the first element of the list.
  unpackWord :: w -> [b]

  -- | Concatenate the two given word values.
  --   NOTE: the first argument represents the more-significant bits
  joinWord :: w -> w -> w

  -- | Take the most-significant bits, and return
  --   those bits and the remainder.  The first element
  --   of the pair is the most significant bits.
  --   The two integer sizes must sum to the length of the given word value.
  splitWord :: Integer -- ^ left width
            -> Integer -- ^ right width
            -> w
            -> (w, w)

  -- | Extract a subsequence of bits from a packed word value.
  --   The first integer argument is the number of bits in the
  --   resulting word.  The second integer argument is the
  --   number of less-significant digits to discard.  Stated another
  --   way, the operation `extractWord n i w` is equivalent to
  --   first shifting `w` right by `i` bits, and then truncating to
  --   `n` bits.
  extractWord :: Integer -- ^ Number of bits to take
              -> Integer -- ^ starting bit
              -> w
              -> w

  -- | 2's complement addition of packed words.  The arguments must have
  --   equal bit width, and the result is of the same width. Overflow is silently
  --   discarded.
  wordPlus :: w -> w -> w

  -- | 2's complement subtraction of packed words.  The arguments must have
  --   equal bit width, and the result is of the same width. Overflow is silently
  --   discarded.
  wordMinus :: w -> w -> w

  -- | 2's complement multiplication of packed words.  The arguments must have
  --   equal bit width, and the result is of the same width. The high bits of the
  --   multiplication are silently discarded.
  wordMult :: w -> w -> w

  -- | Construct an integer value from the given packed word.
  wordToInt :: w -> i

  -- | Addition of unbounded integers.
  intPlus :: i -> i -> i

  -- | Subtraction of unbounded integers.
  intMinus :: i -> i -> i

  -- | Multiplication of unbounded integers.
  intMult :: i -> i -> i

  -- | Addition of integers modulo n, for a concrete positive integer n.
  intModPlus :: Integer -> i -> i -> i

  -- | Subtraction of integers modulo n, for a concrete positive integer n.
  intModMinus :: Integer -> i -> i -> i

  -- | Multiplication of integers modulo n, for a concrete positive integer n.
  intModMult :: Integer -> i -> i -> i

  -- | Construct a packed word of the specified width from an integer value.
  wordFromInt :: Integer -> i -> w

-- | This class defines additional operations necessary to define generic evaluation
--   functions.
class BitWord b w i => EvalPrims b w i where
  -- | Eval prim binds primitive declarations to the primitive values that implement them.  Returns 'Nothing' for abstract primitives (i.e., once that are
  -- not implemented by this backend).
  evalPrim :: Decl -> Maybe (GenValue b w i)

  -- | if/then/else operation.  Choose either the 'then' value or the 'else' value depending
  --   on the value of the test bit.
  iteValue :: b                      -- ^ Test bit
           -> Eval (GenValue b w i)  -- ^ 'then' value
           -> Eval (GenValue b w i)  -- ^ 'else' value
           -> Eval (GenValue b w i)


-- Concrete Big-endian Words ------------------------------------------------------------

mask :: Integer  -- ^ Bit-width
     -> Integer  -- ^ Value
     -> Integer  -- ^ Masked result
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

-- Value Constructors ----------------------------------------------------------

-- | Create a packed word of n bits.
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

-- | Functions that assume word inputs
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)

-- | A type lambda that expects a @Type@.
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)

-- | A type lambda that expects a @Type@ of kind #.
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)

-- | Generate a stream.
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)

-- | This is strict!
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

-- | Construct either a finite sequence, or a stream.  In the finite case,
-- record whether or not the elements were bits, to aid pretty-printing.
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


-- | Construct either a finite sequence, or a stream.  In the finite case,
-- record whether or not the elements were bits, to aid pretty-printing.
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


-- Value Destructors -----------------------------------------------------------

-- | Extract a bit value.
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"]

-- | Extract an integer value.
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"]

-- | Extract a finite sequence value.
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"]

-- | Extract 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]

-- | Extract a packed word.
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

-- | If the given list of values are all fully-evaluated thunks
--   containing bits, return a packed word built from the same bits.
--   However, if any value is not a fully-evaluated bit, return `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

-- | Turn a value into an integer represented by w bits.
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

-- | Extract a function from a value.
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"]

-- | Extract a polymorphic function from a value.
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"]

-- | Extract a polymorphic function from a 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"]

-- | Extract a tuple from a 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"]

-- | Extract a record from a value.
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"]

-- | Lookup a field in 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"]

-- Value to Expression conversion ----------------------------------------------

-- | Given an expected type, returns an expression that evaluates to
-- this value, if we can determine it.
--
-- XXX: View patterns would probably clean up this definition a lot.
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
             ]