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