-- |
-- 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 FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}

module Cryptol.Eval.Value
  ( -- * GenericValue
    GenValue(..)
  , forceWordValue
  , forceValue
  , Backend(..)
  , asciiMode
    -- ** Value introduction operations
  , word
  , lam
  , wlam
  , flam
  , tlam
  , nlam
  , ilam
  , toStream
  , toFinSeq
  , toSeq
  , mkSeq
    -- ** Value eliminators
  , fromVBit
  , fromVInteger
  , fromVRational
  , fromVFloat
  , fromVSeq
  , fromSeq
  , fromWordVal
  , asIndex
  , fromVWord
  , vWordLen
  , tryFromBits
  , fromVFun
  , fromVPoly
  , fromVNumPoly
  , fromVTuple
  , fromVRecord
  , lookupRecord
    -- ** Pretty printing
  , defaultPPOpts
  , ppValue

    -- * Sequence Maps
  , SeqMap (..)
  , lookupSeqMap
  , finiteSeqMap
  , infiniteSeqMap
  , enumerateSeqMap
  , streamSeqMap
  , reverseSeqMap
  , updateSeqMap
  , dropSeqMap
  , concatSeqMap
  , splitSeqMap
  , memoMap
  , zipSeqMap
  , mapSeqMap
  , largeBitSize
    -- * WordValue
  , WordValue(..)
  , asWordVal
  , asBitsMap
  , enumerateWordValue
  , enumerateWordValueRev
  , wordValueSize
  , indexWordValue
  , updateWordValue
  ) where

import Control.Monad.IO.Class
import Data.Bits
import Data.IORef
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import MonadLib

import Cryptol.Backend
import qualified Cryptol.Backend.Arch as Arch
import Cryptol.Backend.Monad ( PPOpts(..), evalPanic, wordTooWide, defaultPPOpts, asciiMode )
import Cryptol.Eval.Type

import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
import Cryptol.Utils.Ident (Ident)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.PP
import Cryptol.Utils.RecordMap

import Data.List(genericIndex)

import GHC.Generics (Generic)

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

-- | A sequence map represents a mapping from nonnegative integer indices
--   to values.  These are used to represent both finite and infinite sequences.
data SeqMap sym
  = IndexSeqMap  !(Integer -> SEval sym (GenValue sym))
  | UpdateSeqMap !(Map Integer (SEval sym (GenValue sym)))
                 !(Integer -> SEval sym (GenValue sym))

lookupSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap (IndexSeqMap Integer -> SEval sym (GenValue sym)
f) Integer
i = Integer -> SEval sym (GenValue sym)
f Integer
i
lookupSeqMap (UpdateSeqMap Map Integer (SEval sym (GenValue sym))
m Integer -> SEval sym (GenValue sym)
f) Integer
i =
  case Integer
-> Map Integer (SEval sym (GenValue sym))
-> Maybe (SEval sym (GenValue sym))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Integer
i Map Integer (SEval sym (GenValue sym))
m of
    Just SEval sym (GenValue sym)
x  -> SEval sym (GenValue sym)
x
    Maybe (SEval sym (GenValue sym))
Nothing -> Integer -> SEval sym (GenValue sym)
f Integer
i

-- | 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 = Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
48

-- | Generate a finite sequence map from a list of values
finiteSeqMap :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap :: sym -> [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap sym
sym [SEval sym (GenValue sym)]
xs =
   Map Integer (SEval sym (GenValue sym))
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym.
Map Integer (SEval sym (GenValue sym))
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
UpdateSeqMap
      ([(Integer, SEval sym (GenValue sym))]
-> Map Integer (SEval sym (GenValue sym))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([Integer]
-> [SEval sym (GenValue sym)]
-> [(Integer, SEval sym (GenValue sym))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0..] [SEval sym (GenValue sym)]
xs))
      (sym -> Integer -> SEval sym (GenValue sym)
forall sym a. Backend sym => sym -> Integer -> SEval sym a
invalidIndex sym
sym)

-- | Generate an infinite sequence map from a stream of values
infiniteSeqMap :: Backend sym => [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)
infiniteSeqMap :: [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)
infiniteSeqMap [SEval sym (GenValue sym)]
xs =
   -- TODO: use an int-trie?
   SeqMap sym -> SEval sym (SeqMap sym)
forall (m :: * -> *) sym.
(MonadIO m, Backend sym) =>
SeqMap sym -> m (SeqMap sym)
memoMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i -> [SEval sym (GenValue sym)] -> Integer -> SEval sym (GenValue sym)
forall i a. Integral i => [a] -> i -> a
genericIndex [SEval sym (GenValue sym)]
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 sym -> [SEval sym (GenValue sym)]
enumerateSeqMap :: n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap n
n SeqMap sym
m = [ SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
m Integer
i | Integer
i <- [Integer
0 .. (n -> Integer
forall a. Integral a => a -> Integer
toInteger n
n)Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1] ]

-- | Create an infinite stream of all the values in a sequence map
streamSeqMap :: SeqMap sym -> [SEval sym (GenValue sym)]
streamSeqMap :: SeqMap sym -> [SEval sym (GenValue sym)]
streamSeqMap SeqMap sym
m = [ SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
m Integer
i | Integer
i <- [Integer
0..] ]

-- | Reverse the order of a finite sequence map
reverseSeqMap :: Integer     -- ^ Size of the sequence map
              -> SeqMap sym
              -> SeqMap sym
reverseSeqMap :: Integer -> SeqMap sym -> SeqMap sym
reverseSeqMap Integer
n SeqMap sym
vals = (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i -> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
vals (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i)

updateSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap (UpdateSeqMap Map Integer (SEval sym (GenValue sym))
m Integer -> SEval sym (GenValue sym)
sm) Integer
i SEval sym (GenValue sym)
x = Map Integer (SEval sym (GenValue sym))
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym.
Map Integer (SEval sym (GenValue sym))
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
UpdateSeqMap (Integer
-> SEval sym (GenValue sym)
-> Map Integer (SEval sym (GenValue sym))
-> Map Integer (SEval sym (GenValue sym))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
i SEval sym (GenValue sym)
x Map Integer (SEval sym (GenValue sym))
m) Integer -> SEval sym (GenValue sym)
sm
updateSeqMap (IndexSeqMap Integer -> SEval sym (GenValue sym)
f) Integer
i SEval sym (GenValue sym)
x = Map Integer (SEval sym (GenValue sym))
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym.
Map Integer (SEval sym (GenValue sym))
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
UpdateSeqMap (Integer
-> SEval sym (GenValue sym)
-> Map Integer (SEval sym (GenValue sym))
forall k a. k -> a -> Map k a
Map.singleton Integer
i SEval sym (GenValue sym)
x) Integer -> SEval sym (GenValue sym)
f

-- | Concatenate the first @n@ values of the first sequence map onto the
--   beginning of the second sequence map.
concatSeqMap :: Integer -> SeqMap sym -> SeqMap sym -> SeqMap sym
concatSeqMap :: Integer -> SeqMap sym -> SeqMap sym -> SeqMap sym
concatSeqMap Integer
n SeqMap sym
x SeqMap sym
y =
    (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
       if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n
         then SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
x Integer
i
         else SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
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 sym -> (SeqMap sym, SeqMap sym)
splitSeqMap :: Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
splitSeqMap Integer
n SeqMap sym
xs = (SeqMap sym
hd,SeqMap sym
tl)
  where
  hd :: SeqMap sym
hd = SeqMap sym
xs
  tl :: SeqMap sym
tl = (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i -> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
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 sym -> SeqMap sym
dropSeqMap :: Integer -> SeqMap sym -> SeqMap sym
dropSeqMap Integer
0 SeqMap sym
xs = SeqMap sym
xs
dropSeqMap Integer
n SeqMap sym
xs = (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i -> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
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 :: (MonadIO m, Backend sym) => SeqMap sym -> m (SeqMap sym)
memoMap :: SeqMap sym -> m (SeqMap sym)
memoMap SeqMap sym
x = do
  IORef (Map Integer (GenValue sym))
cache <- IO (IORef (Map Integer (GenValue sym)))
-> m (IORef (Map Integer (GenValue sym)))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef (Map Integer (GenValue sym)))
 -> m (IORef (Map Integer (GenValue sym))))
-> IO (IORef (Map Integer (GenValue sym)))
-> m (IORef (Map Integer (GenValue sym)))
forall a b. (a -> b) -> a -> b
$ Map Integer (GenValue sym)
-> IO (IORef (Map Integer (GenValue sym)))
forall a. a -> IO (IORef a)
newIORef (Map Integer (GenValue sym)
 -> IO (IORef (Map Integer (GenValue sym))))
-> Map Integer (GenValue sym)
-> IO (IORef (Map Integer (GenValue sym)))
forall a b. (a -> b) -> a -> b
$ Map Integer (GenValue sym)
forall k a. Map k a
Map.empty
  SeqMap sym -> m (SeqMap sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap sym -> m (SeqMap sym)) -> SeqMap sym -> m (SeqMap sym)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap (IORef (Map Integer (GenValue sym))
-> Integer -> SEval sym (GenValue sym)
memo IORef (Map Integer (GenValue sym))
cache)

  where
  memo :: IORef (Map Integer (GenValue sym))
-> Integer -> SEval sym (GenValue sym)
memo IORef (Map Integer (GenValue sym))
cache Integer
i = do
    Maybe (GenValue sym)
mz <- IO (Maybe (GenValue sym)) -> SEval sym (Maybe (GenValue sym))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Integer -> Map Integer (GenValue sym) -> Maybe (GenValue sym)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Integer
i (Map Integer (GenValue sym) -> Maybe (GenValue sym))
-> IO (Map Integer (GenValue sym)) -> IO (Maybe (GenValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (Map Integer (GenValue sym))
-> IO (Map Integer (GenValue sym))
forall a. IORef a -> IO a
readIORef IORef (Map Integer (GenValue sym))
cache)
    case Maybe (GenValue sym)
mz of
      Just GenValue sym
z  -> GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return GenValue sym
z
      Maybe (GenValue sym)
Nothing -> IORef (Map Integer (GenValue sym))
-> Integer -> SEval sym (GenValue sym)
doEval IORef (Map Integer (GenValue sym))
cache Integer
i

  doEval :: IORef (Map Integer (GenValue sym))
-> Integer -> SEval sym (GenValue sym)
doEval IORef (Map Integer (GenValue sym))
cache Integer
i = do
    GenValue sym
v <- SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
x Integer
i
    IO () -> SEval sym ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> SEval sym ()) -> IO () -> SEval sym ()
forall a b. (a -> b) -> a -> b
$ IORef (Map Integer (GenValue sym))
-> (Map Integer (GenValue sym) -> (Map Integer (GenValue sym), ()))
-> IO ()
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef (Map Integer (GenValue sym))
cache (\Map Integer (GenValue sym)
m -> (Integer
-> GenValue sym
-> Map Integer (GenValue sym)
-> Map Integer (GenValue sym)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
i GenValue sym
v Map Integer (GenValue sym)
m, ()))
    GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return GenValue sym
v

-- | Apply the given evaluation function pointwise to the two given
--   sequence maps.
zipSeqMap ::
  Backend sym =>
  (GenValue sym -> GenValue sym -> SEval sym (GenValue sym)) ->
  SeqMap sym ->
  SeqMap sym ->
  SEval sym (SeqMap sym)
zipSeqMap :: (GenValue sym -> GenValue sym -> SEval sym (GenValue sym))
-> SeqMap sym -> SeqMap sym -> SEval sym (SeqMap sym)
zipSeqMap GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
f SeqMap sym
x SeqMap sym
y =
  SeqMap sym -> SEval sym (SeqMap sym)
forall (m :: * -> *) sym.
(MonadIO m, Backend sym) =>
SeqMap sym -> m (SeqMap sym)
memoMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i -> SEval sym (SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
f (GenValue sym -> GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym -> SEval sym (GenValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
x Integer
i SEval sym (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
y Integer
i))

-- | Apply the given function to each value in the given sequence map
mapSeqMap ::
  Backend sym =>
  (GenValue sym -> SEval sym (GenValue sym)) ->
  SeqMap sym -> SEval sym (SeqMap sym)
mapSeqMap :: (GenValue sym -> SEval sym (GenValue sym))
-> SeqMap sym -> SEval sym (SeqMap sym)
mapSeqMap GenValue sym -> SEval sym (GenValue sym)
f SeqMap sym
x =
  SeqMap sym -> SEval sym (SeqMap sym)
forall (m :: * -> *) sym.
(MonadIO m, Backend sym) =>
SeqMap sym -> m (SeqMap sym)
memoMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i -> GenValue sym -> SEval sym (GenValue sym)
f (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
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 sym
  = WordVal !(SWord sym)                      -- ^ Packed word representation for bit sequences.
  | LargeBitsVal !Integer !(SeqMap sym)       -- ^ A large bitvector sequence, represented as a
                                            --   'SeqMap' of bits.
 deriving ((forall x. WordValue sym -> Rep (WordValue sym) x)
-> (forall x. Rep (WordValue sym) x -> WordValue sym)
-> Generic (WordValue sym)
forall x. Rep (WordValue sym) x -> WordValue sym
forall x. WordValue sym -> Rep (WordValue sym) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall sym x. Rep (WordValue sym) x -> WordValue sym
forall sym x. WordValue sym -> Rep (WordValue sym) x
$cto :: forall sym x. Rep (WordValue sym) x -> WordValue sym
$cfrom :: forall sym x. WordValue sym -> Rep (WordValue sym) x
Generic)

-- | Force a word value into packed word form
asWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal :: sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
_   (WordVal SWord sym
w)         = SWord sym -> SEval sym (SWord sym)
forall (m :: * -> *) a. Monad m => a -> m a
return SWord sym
w
asWordVal sym
sym (LargeBitsVal Integer
n SeqMap sym
xs) = sym -> [SBit sym] -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> [SBit sym] -> SEval sym (SWord sym)
packWord sym
sym ([SBit sym] -> SEval sym (SWord sym))
-> SEval sym [SBit sym] -> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (SEval sym (GenValue sym) -> SEval sym (SBit sym))
-> [SEval sym (GenValue sym)] -> SEval sym [SBit sym]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (GenValue sym -> SBit sym
forall sym. GenValue sym -> SBit sym
fromVBit (GenValue sym -> SBit sym)
-> SEval sym (GenValue sym) -> SEval sym (SBit sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Integer -> SeqMap sym -> [SEval sym (GenValue sym)]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
n SeqMap sym
xs)

-- | Force a word value into a sequence of bits
asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym
asBitsMap :: sym -> WordValue sym -> SeqMap sym
asBitsMap sym
sym (WordVal SWord sym
w)  = (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i -> SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (sym -> SWord sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SWord sym -> Integer -> SEval sym (SBit sym)
wordBit sym
sym SWord sym
w Integer
i)
asBitsMap sym
_   (LargeBitsVal Integer
_ SeqMap sym
xs) = SeqMap sym
xs

-- | Turn a word value into a sequence of bits, forcing each bit.
--   The sequence is returned in big-endian order.
enumerateWordValue :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValue :: sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValue sym
sym (WordVal SWord sym
w) = sym -> SWord sym -> SEval sym [SBit sym]
forall sym. Backend sym => sym -> SWord sym -> SEval sym [SBit sym]
unpackWord sym
sym SWord sym
w
enumerateWordValue sym
_ (LargeBitsVal Integer
n SeqMap sym
xs) = (SEval sym (GenValue sym) -> SEval sym (SBit sym))
-> [SEval sym (GenValue sym)] -> SEval sym [SBit sym]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (GenValue sym -> SBit sym
forall sym. GenValue sym -> SBit sym
fromVBit (GenValue sym -> SBit sym)
-> SEval sym (GenValue sym) -> SEval sym (SBit sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Integer -> SeqMap sym -> [SEval sym (GenValue sym)]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
n SeqMap sym
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 :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValueRev :: sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValueRev sym
sym (WordVal SWord sym
w)  = [SBit sym] -> [SBit sym]
forall a. [a] -> [a]
reverse ([SBit sym] -> [SBit sym])
-> SEval sym [SBit sym] -> SEval sym [SBit sym]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SWord sym -> SEval sym [SBit sym]
forall sym. Backend sym => sym -> SWord sym -> SEval sym [SBit sym]
unpackWord sym
sym SWord sym
w
enumerateWordValueRev sym
_   (LargeBitsVal Integer
n SeqMap sym
xs) = (SEval sym (GenValue sym) -> SEval sym (SBit sym))
-> [SEval sym (GenValue sym)] -> SEval sym [SBit sym]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (GenValue sym -> SBit sym
forall sym. GenValue sym -> SBit sym
fromVBit (GenValue sym -> SBit sym)
-> SEval sym (GenValue sym) -> SEval sym (SBit sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Integer -> SeqMap sym -> [SEval sym (GenValue sym)]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
n (Integer -> SeqMap sym -> SeqMap sym
forall sym. Integer -> SeqMap sym -> SeqMap sym
reverseSeqMap Integer
n SeqMap sym
xs))

-- | Compute the size of a word value
wordValueSize :: Backend sym => sym -> WordValue sym -> Integer
wordValueSize :: sym -> WordValue sym -> Integer
wordValueSize sym
sym (WordVal SWord sym
w)  = sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w
wordValueSize sym
_ (LargeBitsVal Integer
n SeqMap sym
_) = Integer
n

-- | Select an individual bit from a word value
indexWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue :: sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym (WordVal SWord sym
w) Integer
idx
   | Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
idx Bool -> Bool -> Bool
&& Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w = sym -> SWord sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SWord sym -> Integer -> SEval sym (SBit sym)
wordBit sym
sym SWord sym
w Integer
idx
   | Bool
otherwise = sym -> Integer -> SEval sym (SBit sym)
forall sym a. Backend sym => sym -> Integer -> SEval sym a
invalidIndex sym
sym Integer
idx
indexWordValue sym
sym (LargeBitsVal Integer
n SeqMap sym
xs) Integer
idx
   | Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
idx Bool -> Bool -> Bool
&& Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n = GenValue sym -> SBit sym
forall sym. GenValue sym -> SBit sym
fromVBit (GenValue sym -> SBit sym)
-> SEval sym (GenValue sym) -> SEval sym (SBit sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
xs Integer
idx
   | Bool
otherwise = sym -> Integer -> SEval sym (SBit sym)
forall sym a. Backend sym => sym -> Integer -> SEval sym a
invalidIndex sym
sym Integer
idx

-- | Produce a new 'WordValue' from the one given by updating the @i@th bit with the
--   given bit value.
updateWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym) -> SEval sym (WordValue sym)
updateWordValue :: sym
-> WordValue sym
-> Integer
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordValue sym
sym (WordVal SWord sym
w) Integer
idx SEval sym (SBit sym)
b
   | Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
|| Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w = sym -> Integer -> SEval sym (WordValue sym)
forall sym a. Backend sym => sym -> Integer -> SEval sym a
invalidIndex sym
sym Integer
idx
   | sym -> SEval sym (SBit sym) -> Bool
forall sym a. Backend sym => sym -> SEval sym a -> Bool
isReady sym
sym SEval sym (SBit sym)
b = SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (sym -> SWord sym -> Integer -> SBit sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> Integer -> SBit sym -> SEval sym (SWord sym)
wordUpdate sym
sym SWord sym
w Integer
idx (SBit sym -> SEval sym (SWord sym))
-> SEval sym (SBit sym) -> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (SBit sym)
b)

updateWordValue sym
sym WordValue sym
wv Integer
idx SEval sym (SBit sym)
b
   | Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
idx Bool -> Bool -> Bool
&& Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< sym -> WordValue sym -> Integer
forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
wv =
        WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue sym -> SEval sym (WordValue sym))
-> WordValue sym -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> WordValue sym
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal (sym -> WordValue sym -> Integer
forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
wv) (SeqMap sym -> WordValue sym) -> SeqMap sym -> WordValue sym
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap (sym -> WordValue sym -> SeqMap sym
forall sym. Backend sym => sym -> WordValue sym -> SeqMap sym
asBitsMap sym
sym WordValue sym
wv) Integer
idx (SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SBit sym)
b)
   | Bool
otherwise = sym -> Integer -> SEval sym (WordValue sym)
forall sym a. Backend sym => sym -> Integer -> SEval sym a
invalidIndex sym
sym 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 sym
  = VRecord !(RecordMap Ident (SEval sym (GenValue sym))) -- ^ @ { .. } @
  | VTuple ![SEval sym (GenValue sym)]              -- ^ @ ( .. ) @
  | VBit !(SBit sym)                           -- ^ @ Bit    @
  | VInteger !(SInteger sym)                   -- ^ @ Integer @ or @ Z n @
  | VRational !(SRational sym)                 -- ^ @ Rational @
  | VFloat !(SFloat sym)
  | VSeq !Integer !(SeqMap sym)                -- ^ @ [n]a   @
                                               --   Invariant: VSeq is never a sequence of bits
  | VWord !Integer !(SEval sym (WordValue sym))  -- ^ @ [n]Bit @
  | VStream !(SeqMap sym)                   -- ^ @ [inf]a @
  | VFun (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -- ^ functions
  | VPoly (TValue -> SEval sym (GenValue sym))   -- ^ polymorphic values (kind *)
  | VNumPoly (Nat' -> SEval sym (GenValue sym))  -- ^ polymorphic values (kind #)
 deriving (forall x. GenValue sym -> Rep (GenValue sym) x)
-> (forall x. Rep (GenValue sym) x -> GenValue sym)
-> Generic (GenValue sym)
forall x. Rep (GenValue sym) x -> GenValue sym
forall x. GenValue sym -> Rep (GenValue sym) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall sym x. Rep (GenValue sym) x -> GenValue sym
forall sym x. GenValue sym -> Rep (GenValue sym) x
$cto :: forall sym x. Rep (GenValue sym) x -> GenValue sym
$cfrom :: forall sym x. GenValue sym -> Rep (GenValue sym) x
Generic


-- | Force the evaluation of a word value
forceWordValue :: Backend sym => WordValue sym -> SEval sym ()
forceWordValue :: WordValue sym -> SEval sym ()
forceWordValue (WordVal SWord sym
w)  = SWord sym -> SEval sym () -> SEval sym ()
seq SWord sym
w (() -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
forceWordValue (LargeBitsVal Integer
n SeqMap sym
xs) = (SEval sym (GenValue sym) -> SEval sym ())
-> [SEval sym (GenValue sym)] -> SEval sym ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\SEval sym (GenValue sym)
x -> () -> GenValue sym -> ()
forall a b. a -> b -> a
const () (GenValue sym -> ()) -> SEval sym (GenValue sym) -> SEval sym ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
x) (Integer -> SeqMap sym -> [SEval sym (GenValue sym)]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
n SeqMap sym
xs)

-- | Force the evaluation of a value
forceValue :: Backend sym => GenValue sym -> SEval sym ()
forceValue :: GenValue sym -> SEval sym ()
forceValue GenValue sym
v = case GenValue sym
v of
  VRecord RecordMap Ident (SEval sym (GenValue sym))
fs  -> (SEval sym (GenValue sym) -> SEval sym ())
-> RecordMap Ident (SEval sym (GenValue sym)) -> SEval sym ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (GenValue sym -> SEval sym ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
forceValue (GenValue sym -> SEval sym ())
-> SEval sym (GenValue sym) -> SEval sym ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) RecordMap Ident (SEval sym (GenValue sym))
fs
  VTuple [SEval sym (GenValue sym)]
xs   -> (SEval sym (GenValue sym) -> SEval sym ())
-> [SEval sym (GenValue sym)] -> SEval sym ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (GenValue sym -> SEval sym ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
forceValue (GenValue sym -> SEval sym ())
-> SEval sym (GenValue sym) -> SEval sym ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) [SEval sym (GenValue sym)]
xs
  VSeq Integer
n SeqMap sym
xs   -> (SEval sym (GenValue sym) -> SEval sym ())
-> [SEval sym (GenValue sym)] -> SEval sym ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (GenValue sym -> SEval sym ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
forceValue (GenValue sym -> SEval sym ())
-> SEval sym (GenValue sym) -> SEval sym ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (Integer -> SeqMap sym -> [SEval sym (GenValue sym)]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
n SeqMap sym
xs)
  VBit SBit sym
b      -> SBit sym -> SEval sym () -> SEval sym ()
seq SBit sym
b (() -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VInteger SInteger sym
i  -> SInteger sym -> SEval sym () -> SEval sym ()
seq SInteger sym
i (() -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VRational SRational sym
q -> SRational sym -> SEval sym () -> SEval sym ()
seq SRational sym
q (() -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VFloat SFloat sym
f    -> SFloat sym -> SEval sym () -> SEval sym ()
seq SFloat sym
f (() -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VWord Integer
_ SEval sym (WordValue sym)
wv  -> WordValue sym -> SEval sym ()
forall sym. Backend sym => WordValue sym -> SEval sym ()
forceWordValue (WordValue sym -> SEval sym ())
-> SEval sym (WordValue sym) -> SEval sym ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
wv
  VStream SeqMap sym
_   -> () -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VFun SEval sym (GenValue sym) -> SEval sym (GenValue sym)
_      -> () -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VPoly TValue -> SEval sym (GenValue sym)
_     -> () -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VNumPoly Nat' -> SEval sym (GenValue sym)
_  -> () -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()



instance Backend sym => Show (GenValue sym) where
  show :: GenValue sym -> String
show GenValue sym
v = case GenValue sym
v of
    VRecord RecordMap Ident (SEval sym (GenValue sym))
fs -> String
"record:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Ident] -> String
forall a. Show a => a -> String
show (RecordMap Ident (SEval sym (GenValue sym)) -> [Ident]
forall a b. RecordMap a b -> [a]
displayOrder RecordMap Ident (SEval sym (GenValue sym))
fs)
    VTuple [SEval sym (GenValue sym)]
xs  -> String
"tuple:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([SEval sym (GenValue sym)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SEval sym (GenValue sym)]
xs)
    VBit SBit sym
_     -> String
"bit"
    VInteger SInteger sym
_ -> String
"integer"
    VRational SRational sym
_ -> String
"rational"
    VFloat SFloat sym
_   -> String
"float"
    VSeq Integer
n SeqMap sym
_   -> String
"seq:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
    VWord Integer
n SEval sym (WordValue sym)
_  -> String
"word:"  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
    VStream SeqMap sym
_  -> String
"stream"
    VFun SEval sym (GenValue sym) -> SEval sym (GenValue sym)
_     -> String
"fun"
    VPoly TValue -> SEval sym (GenValue sym)
_    -> String
"poly"
    VNumPoly Nat' -> SEval sym (GenValue sym)
_ -> String
"numpoly"


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

ppValue :: forall sym.
  Backend sym =>
  sym ->
  PPOpts ->
  GenValue sym ->
  SEval sym Doc
ppValue :: sym -> PPOpts -> GenValue sym -> SEval sym Doc
ppValue sym
x PPOpts
opts = GenValue sym -> SEval sym Doc
loop
  where
  loop :: GenValue sym -> SEval sym Doc
  loop :: GenValue sym -> SEval sym Doc
loop GenValue sym
val = case GenValue sym
val of
    VRecord RecordMap Ident (SEval sym (GenValue sym))
fs         -> do RecordMap Ident Doc
fs' <- (SEval sym (GenValue sym) -> SEval sym Doc)
-> RecordMap Ident (SEval sym (GenValue sym))
-> SEval sym (RecordMap Ident Doc)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym Doc) -> SEval sym Doc
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GenValue sym -> SEval sym Doc
loop) RecordMap Ident (SEval sym (GenValue sym))
fs
                             Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym 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 (RecordMap Ident Doc -> [(Ident, Doc)]
forall a b. (Show a, Ord a) => RecordMap a b -> [(a, b)]
displayFields RecordMap Ident Doc
fs'))))
      where
      ppField :: (a, Doc) -> Doc
ppField (a
f,Doc
r) = a -> Doc
forall a. PP a => a -> Doc
pp a
f Doc -> Doc -> Doc
<+> Char -> Doc
char Char
'=' Doc -> Doc -> Doc
<+> Doc
r
    VTuple [SEval sym (GenValue sym)]
vals        -> do [Doc]
vals' <- (SEval sym (GenValue sym) -> SEval sym Doc)
-> [SEval sym (GenValue sym)] -> SEval sym [Doc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym Doc) -> SEval sym Doc
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=GenValue sym -> SEval sym Doc
loop) [SEval sym (GenValue sym)]
vals
                             Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens ([Doc] -> Doc
sep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc]
vals'))
    VBit SBit sym
b             -> Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ sym -> SBit sym -> Doc
forall sym. Backend sym => sym -> SBit sym -> Doc
ppBit sym
x SBit sym
b
    VInteger SInteger sym
i         -> Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ sym -> PPOpts -> SInteger sym -> Doc
forall sym. Backend sym => sym -> PPOpts -> SInteger sym -> Doc
ppInteger sym
x PPOpts
opts SInteger sym
i
    VRational SRational sym
q        -> Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ sym -> PPOpts -> SRational sym -> Doc
forall sym. Backend sym => sym -> PPOpts -> SRational sym -> Doc
ppRational sym
x PPOpts
opts SRational sym
q
    VFloat SFloat sym
i           -> Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ sym -> PPOpts -> SFloat sym -> Doc
forall sym. Backend sym => sym -> PPOpts -> SFloat sym -> Doc
ppFloat sym
x PPOpts
opts SFloat sym
i
    VSeq Integer
sz SeqMap sym
vals       -> Integer -> SeqMap sym -> SEval sym Doc
ppWordSeq Integer
sz SeqMap sym
vals
    VWord Integer
_ SEval sym (WordValue sym)
wv         -> WordValue sym -> SEval sym Doc
ppWordVal (WordValue sym -> SEval sym Doc)
-> SEval sym (WordValue sym) -> SEval sym Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
wv
    VStream SeqMap sym
vals       -> do [Doc]
vals' <- (SEval sym (GenValue sym) -> SEval sym Doc)
-> [SEval sym (GenValue sym)] -> SEval sym [Doc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym Doc) -> SEval sym Doc
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=GenValue sym -> SEval sym Doc
loop) ([SEval sym (GenValue sym)] -> SEval sym [Doc])
-> [SEval sym (GenValue sym)] -> SEval sym [Doc]
forall a b. (a -> b) -> a -> b
$ Int -> SeqMap sym -> [SEval sym (GenValue sym)]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap (PPOpts -> Int
useInfLength PPOpts
opts) SeqMap sym
vals
                             Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym 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 String
"..."]
                                   )
    VFun SEval sym (GenValue sym) -> SEval sym (GenValue sym)
_             -> Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"<function>"
    VPoly TValue -> SEval sym (GenValue sym)
_            -> Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"<polymorphic value>"
    VNumPoly Nat' -> SEval sym (GenValue sym)
_         -> Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"<polymorphic value>"

  ppWordVal :: WordValue sym -> SEval sym Doc
  ppWordVal :: WordValue sym -> SEval sym Doc
ppWordVal WordValue sym
w = sym -> PPOpts -> SWord sym -> Doc
forall sym. Backend sym => sym -> PPOpts -> SWord sym -> Doc
ppWord sym
x PPOpts
opts (SWord sym -> Doc) -> SEval sym (SWord sym) -> SEval sym Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> WordValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
x WordValue sym
w

  ppWordSeq :: Integer -> SeqMap sym -> SEval sym Doc
  ppWordSeq :: Integer -> SeqMap sym -> SEval sym Doc
ppWordSeq Integer
sz SeqMap sym
vals = do
    [GenValue sym]
ws <- [SEval sym (GenValue sym)] -> SEval sym [GenValue sym]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Integer -> SeqMap sym -> [SEval sym (GenValue sym)]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
sz SeqMap sym
vals)
    case [GenValue sym]
ws of
      GenValue sym
w : [GenValue sym]
_
        | Just Integer
l <- GenValue sym -> Maybe Integer
forall sym. Backend sym => GenValue sym -> Maybe Integer
vWordLen GenValue sym
w
        , PPOpts -> Integer -> Bool
asciiMode PPOpts
opts Integer
l
        -> do [SWord sym]
vs <- (GenValue sym -> SEval sym (SWord sym))
-> [GenValue sym] -> SEval sym [SWord sym]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (sym -> String -> GenValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
x String
"ppWordSeq") [GenValue sym]
ws
              case (SWord sym -> Maybe Char) -> [SWord sym] -> Maybe String
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (sym -> SWord sym -> Maybe Char
forall sym. Backend sym => sym -> SWord sym -> Maybe Char
wordAsChar sym
x) [SWord sym]
vs of
                Just String
str -> Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (ShowS
forall a. Show a => a -> String
show String
str)
                Maybe String
_ -> Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym 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
$ (SWord sym -> Doc) -> [SWord sym] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (sym -> PPOpts -> SWord sym -> Doc
forall sym. Backend sym => sym -> PPOpts -> SWord sym -> Doc
ppWord sym
x PPOpts
opts) [SWord sym]
vs))
      [GenValue sym]
_ -> do [Doc]
ws' <- (GenValue sym -> SEval sym Doc)
-> [GenValue sym] -> SEval sym [Doc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse GenValue sym -> SEval sym Doc
loop [GenValue sym]
ws
              Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
brackets ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc]
ws'))


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

-- | Create a packed word of n bits.
word :: Backend sym => sym -> Integer -> Integer -> GenValue sym
word :: sym -> Integer -> Integer -> GenValue sym
word sym
sym Integer
n Integer
i
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
Arch.maxBigIntWidth = Integer -> GenValue sym
forall a. Integer -> a
wordTooWide Integer
n
  | Bool
otherwise                = Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
n (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> Integer -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
n Integer
i)


lam :: (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -> GenValue sym
lam :: (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam  = (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun

-- | Functions that assume word inputs
wlam :: Backend sym => sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam :: sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam sym
sym SWord sym -> SEval sym (GenValue sym)
f = (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun (\SEval sym (GenValue sym)
arg -> SEval sym (GenValue sym)
arg SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym (SWord sym)) -> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= sym -> String -> GenValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"wlam" SEval sym (SWord sym)
-> (SWord sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SWord sym -> SEval sym (GenValue sym)
f)

-- | Functions that assume floating point inputs
flam :: Backend sym =>
        (SFloat sym -> SEval sym (GenValue sym)) -> GenValue sym
flam :: (SFloat sym -> SEval sym (GenValue sym)) -> GenValue sym
flam SFloat sym -> SEval sym (GenValue sym)
f = (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun (\SEval sym (GenValue sym)
arg -> SEval sym (GenValue sym)
arg SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SFloat sym -> SEval sym (GenValue sym)
f (SFloat sym -> SEval sym (GenValue sym))
-> (GenValue sym -> SFloat sym)
-> GenValue sym
-> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenValue sym -> SFloat sym
forall sym. GenValue sym -> SFloat sym
fromVFloat)



-- | A type lambda that expects a 'Type'.
tlam :: Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam :: (TValue -> GenValue sym) -> GenValue sym
tlam TValue -> GenValue sym
f = (TValue -> SEval sym (GenValue sym)) -> GenValue sym
forall sym. (TValue -> SEval sym (GenValue sym)) -> GenValue sym
VPoly (GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> (TValue -> GenValue sym) -> TValue -> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TValue -> GenValue sym
f)

-- | A type lambda that expects a 'Type' of kind #.
nlam :: Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam :: (Nat' -> GenValue sym) -> GenValue sym
nlam Nat' -> GenValue sym
f = (Nat' -> SEval sym (GenValue sym)) -> GenValue sym
forall sym. (Nat' -> SEval sym (GenValue sym)) -> GenValue sym
VNumPoly (GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> (Nat' -> GenValue sym) -> Nat' -> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat' -> GenValue sym
f)

-- | A type lambda that expects a finite numeric type.
ilam :: Backend sym => (Integer -> GenValue sym) -> GenValue sym
ilam :: (Integer -> GenValue sym) -> GenValue sym
ilam Integer -> GenValue sym
f = (Nat' -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam (\Nat'
n -> case Nat'
n of
                       Nat Integer
i -> Integer -> GenValue sym
f Integer
i
                       Nat'
Inf   -> String -> [String] -> GenValue sym
forall a. HasCallStack => String -> [String] -> a
panic String
"ilam" [ String
"Unexpected `inf`" ])

-- | Generate a stream.
toStream :: Backend sym => [GenValue sym] -> SEval sym (GenValue sym)
toStream :: [GenValue sym] -> SEval sym (GenValue sym)
toStream [GenValue sym]
vs =
   SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym)
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
[SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)
infiniteSeqMap ((GenValue sym -> SEval sym (GenValue sym))
-> [GenValue sym] -> [SEval sym (GenValue sym)]
forall a b. (a -> b) -> [a] -> [b]
map GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure [GenValue sym]
vs)

toFinSeq ::
  Backend sym =>
  sym -> Integer -> TValue -> [GenValue sym] -> GenValue sym
toFinSeq :: sym -> Integer -> TValue -> [GenValue sym] -> GenValue sym
toFinSeq sym
sym Integer
len TValue
elty [GenValue sym]
vs
   | TValue -> Bool
isTBit TValue
elty = Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
len (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> [SBit sym] -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> [SBit sym] -> SEval sym (SWord sym)
packWord sym
sym ((GenValue sym -> SBit sym) -> [GenValue sym] -> [SBit sym]
forall a b. (a -> b) -> [a] -> [b]
map GenValue sym -> SBit sym
forall sym. GenValue sym -> SBit sym
fromVBit [GenValue sym]
vs))
   | Bool
otherwise   = Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
len (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ sym -> [SEval sym (GenValue sym)] -> SeqMap sym
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap sym
sym ((GenValue sym -> SEval sym (GenValue sym))
-> [GenValue sym] -> [SEval sym (GenValue sym)]
forall a b. (a -> b) -> [a] -> [b]
map GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure [GenValue sym]
vs)

-- | 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 ::
  Backend sym =>
  sym -> Nat' -> TValue -> [GenValue sym] -> SEval sym (GenValue sym)
toSeq :: sym -> Nat' -> TValue -> [GenValue sym] -> SEval sym (GenValue sym)
toSeq sym
sym Nat'
len TValue
elty [GenValue sym]
vals = case Nat'
len of
  Nat Integer
n -> GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ sym -> Integer -> TValue -> [GenValue sym] -> GenValue sym
forall sym.
Backend sym =>
sym -> Integer -> TValue -> [GenValue sym] -> GenValue sym
toFinSeq sym
sym Integer
n TValue
elty [GenValue sym]
vals
  Nat'
Inf   -> [GenValue sym] -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
[GenValue sym] -> SEval sym (GenValue sym)
toStream [GenValue sym]
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 :: Backend sym => Nat' -> TValue -> SeqMap sym -> GenValue sym
mkSeq :: Nat' -> TValue -> SeqMap sym -> GenValue sym
mkSeq Nat'
len TValue
elty SeqMap sym
vals = case Nat'
len of
  Nat Integer
n
    | TValue -> Bool
isTBit TValue
elty -> Integer -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
n (SEval sym (WordValue sym) -> GenValue sym)
-> SEval sym (WordValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue sym -> SEval sym (WordValue sym))
-> WordValue sym -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> WordValue sym
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
n SeqMap sym
vals
    | Bool
otherwise   -> Integer -> SeqMap sym -> GenValue sym
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
n SeqMap sym
vals
  Nat'
Inf             -> SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream SeqMap sym
vals


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

-- | Extract a bit value.
fromVBit :: GenValue sym -> SBit sym
fromVBit :: GenValue sym -> SBit sym
fromVBit GenValue sym
val = case GenValue sym
val of
  VBit SBit sym
b -> SBit sym
b
  GenValue sym
_      -> String -> [String] -> SBit sym
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVBit" [String
"not a Bit"]

-- | Extract an integer value.
fromVInteger :: GenValue sym -> SInteger sym
fromVInteger :: GenValue sym -> SInteger sym
fromVInteger GenValue sym
val = case GenValue sym
val of
  VInteger SInteger sym
i -> SInteger sym
i
  GenValue sym
_      -> String -> [String] -> SInteger sym
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVInteger" [String
"not an Integer"]

-- | Extract a rational value.
fromVRational :: GenValue sym -> SRational sym
fromVRational :: GenValue sym -> SRational sym
fromVRational GenValue sym
val = case GenValue sym
val of
  VRational SRational sym
q -> SRational sym
q
  GenValue sym
_      -> String -> [String] -> SRational sym
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVRational" [String
"not a Rational"]

-- | Extract a finite sequence value.
fromVSeq :: GenValue sym -> SeqMap sym
fromVSeq :: GenValue sym -> SeqMap sym
fromVSeq GenValue sym
val = case GenValue sym
val of
  VSeq Integer
_ SeqMap sym
vs -> SeqMap sym
vs
  GenValue sym
_         -> String -> [String] -> SeqMap sym
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVSeq" [String
"not a sequence"]

-- | Extract a sequence.
fromSeq :: Backend sym => String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq :: String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
msg GenValue sym
val = case GenValue sym
val of
  VSeq Integer
_ SeqMap sym
vs   -> SeqMap sym -> SEval sym (SeqMap sym)
forall (m :: * -> *) a. Monad m => a -> m a
return SeqMap sym
vs
  VStream SeqMap sym
vs  -> SeqMap sym -> SEval sym (SeqMap sym)
forall (m :: * -> *) a. Monad m => a -> m a
return SeqMap sym
vs
  GenValue sym
_           -> String -> [String] -> SEval sym (SeqMap sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromSeq" [String
"not a sequence", String
msg]

fromWordVal :: Backend sym => String -> GenValue sym -> SEval sym (WordValue sym)
fromWordVal :: String -> GenValue sym -> SEval sym (WordValue sym)
fromWordVal String
_msg (VWord Integer
_ SEval sym (WordValue sym)
wval) = SEval sym (WordValue sym)
wval
fromWordVal String
msg GenValue sym
_ = String -> [String] -> SEval sym (WordValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromWordVal" [String
"not a word value", String
msg]

asIndex :: Backend sym =>
  sym -> String -> TValue -> GenValue sym -> SEval sym (Either (SInteger sym) (WordValue sym))
asIndex :: sym
-> String
-> TValue
-> GenValue sym
-> SEval sym (Either (SInteger sym) (WordValue sym))
asIndex sym
_sym String
_msg TValue
TVInteger (VInteger SInteger sym
i) = Either (SInteger sym) (WordValue sym)
-> SEval sym (Either (SInteger sym) (WordValue sym))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SInteger sym -> Either (SInteger sym) (WordValue sym)
forall a b. a -> Either a b
Left SInteger sym
i)
asIndex sym
_sym String
_msg TValue
_ (VWord Integer
_ SEval sym (WordValue sym)
wval) = WordValue sym -> Either (SInteger sym) (WordValue sym)
forall a b. b -> Either a b
Right (WordValue sym -> Either (SInteger sym) (WordValue sym))
-> SEval sym (WordValue sym)
-> SEval sym (Either (SInteger sym) (WordValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (WordValue sym)
wval
asIndex sym
_sym  String
msg TValue
_ GenValue sym
_ = String
-> [String] -> SEval sym (Either (SInteger sym) (WordValue sym))
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"asIndex" [String
"not an index value", String
msg]

-- | Extract a packed word.
fromVWord :: Backend sym => sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord :: sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
_msg (VWord Integer
_ SEval sym (WordValue sym)
wval) = SEval sym (WordValue sym)
wval SEval sym (WordValue sym)
-> (WordValue sym -> SEval sym (SWord sym))
-> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= sym -> WordValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym
fromVWord sym
_ String
msg GenValue sym
_ = String -> [String] -> SEval sym (SWord sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVWord" [String
"not a word", String
msg]

vWordLen :: Backend sym => GenValue sym -> Maybe Integer
vWordLen :: GenValue sym -> Maybe Integer
vWordLen GenValue sym
val = case GenValue sym
val of
  VWord Integer
n SEval sym (WordValue sym)
_wv              -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n
  GenValue sym
_                        -> 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 :: Backend sym => sym -> [SEval sym (GenValue sym)] -> Maybe (SEval sym (SWord sym))
tryFromBits :: sym -> [SEval sym (GenValue sym)] -> Maybe (SEval sym (SWord sym))
tryFromBits sym
sym = ([SEval sym (SBit sym)] -> [SEval sym (SBit sym)])
-> [SEval sym (GenValue sym)] -> Maybe (SEval sym (SWord sym))
go [SEval sym (SBit sym)] -> [SEval sym (SBit sym)]
forall a. a -> a
id
  where
  go :: ([SEval sym (SBit sym)] -> [SEval sym (SBit sym)])
-> [SEval sym (GenValue sym)] -> Maybe (SEval sym (SWord sym))
go [SEval sym (SBit sym)] -> [SEval sym (SBit sym)]
f [] = SEval sym (SWord sym) -> Maybe (SEval sym (SWord sym))
forall a. a -> Maybe a
Just (sym -> [SBit sym] -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> [SBit sym] -> SEval sym (SWord sym)
packWord sym
sym ([SBit sym] -> SEval sym (SWord sym))
-> SEval sym [SBit sym] -> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [SEval sym (SBit sym)] -> SEval sym [SBit sym]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([SEval sym (SBit sym)] -> [SEval sym (SBit sym)]
f []))
  go [SEval sym (SBit sym)] -> [SEval sym (SBit sym)]
f (SEval sym (GenValue sym)
v : [SEval sym (GenValue sym)]
vs) | sym -> SEval sym (GenValue sym) -> Bool
forall sym a. Backend sym => sym -> SEval sym a -> Bool
isReady sym
sym SEval sym (GenValue sym)
v = ([SEval sym (SBit sym)] -> [SEval sym (SBit sym)])
-> [SEval sym (GenValue sym)] -> Maybe (SEval sym (SWord sym))
go ([SEval sym (SBit sym)] -> [SEval sym (SBit sym)]
f ([SEval sym (SBit sym)] -> [SEval sym (SBit sym)])
-> ([SEval sym (SBit sym)] -> [SEval sym (SBit sym)])
-> [SEval sym (SBit sym)]
-> [SEval sym (SBit sym)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((GenValue sym -> SBit sym
forall sym. GenValue sym -> SBit sym
fromVBit (GenValue sym -> SBit sym)
-> SEval sym (GenValue sym) -> SEval sym (SBit sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
v)SEval sym (SBit sym)
-> [SEval sym (SBit sym)] -> [SEval sym (SBit sym)]
forall a. a -> [a] -> [a]
:)) [SEval sym (GenValue sym)]
vs
  go [SEval sym (SBit sym)] -> [SEval sym (SBit sym)]
_ (SEval sym (GenValue sym)
_ : [SEval sym (GenValue sym)]
_) = Maybe (SEval sym (SWord sym))
forall a. Maybe a
Nothing

-- | Extract a function from a value.
fromVFun :: GenValue sym -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
fromVFun :: GenValue sym
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
fromVFun GenValue sym
val = case GenValue sym
val of
  VFun SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f
  GenValue sym
_      -> String
-> [String] -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVFun" [String
"not a function"]

-- | Extract a polymorphic function from a value.
fromVPoly :: GenValue sym -> (TValue -> SEval sym (GenValue sym))
fromVPoly :: GenValue sym -> TValue -> SEval sym (GenValue sym)
fromVPoly GenValue sym
val = case GenValue sym
val of
  VPoly TValue -> SEval sym (GenValue sym)
f -> TValue -> SEval sym (GenValue sym)
f
  GenValue sym
_       -> String -> [String] -> TValue -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVPoly" [String
"not a polymorphic value"]

-- | Extract a polymorphic function from a value.
fromVNumPoly :: GenValue sym -> (Nat' -> SEval sym (GenValue sym))
fromVNumPoly :: GenValue sym -> Nat' -> SEval sym (GenValue sym)
fromVNumPoly GenValue sym
val = case GenValue sym
val of
  VNumPoly Nat' -> SEval sym (GenValue sym)
f -> Nat' -> SEval sym (GenValue sym)
f
  GenValue sym
_          -> String -> [String] -> Nat' -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVNumPoly" [String
"not a polymorphic value"]

-- | Extract a tuple from a value.
fromVTuple :: GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple :: GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
val = case GenValue sym
val of
  VTuple [SEval sym (GenValue sym)]
vs -> [SEval sym (GenValue sym)]
vs
  GenValue sym
_         -> String -> [String] -> [SEval sym (GenValue sym)]
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVTuple" [String
"not a tuple"]

-- | Extract a record from a value.
fromVRecord :: GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
fromVRecord :: GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
fromVRecord GenValue sym
val = case GenValue sym
val of
  VRecord RecordMap Ident (SEval sym (GenValue sym))
fs -> RecordMap Ident (SEval sym (GenValue sym))
fs
  GenValue sym
_          -> String -> [String] -> RecordMap Ident (SEval sym (GenValue sym))
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVRecord" [String
"not a record"]

fromVFloat :: GenValue sym -> SFloat sym
fromVFloat :: GenValue sym -> SFloat sym
fromVFloat GenValue sym
val =
  case GenValue sym
val of
    VFloat SFloat sym
x -> SFloat sym
x
    GenValue sym
_        -> String -> [String] -> SFloat sym
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVFloat" [String
"not a Float"]

-- | Lookup a field in a record.
lookupRecord :: Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord :: Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
f GenValue sym
val =
  case Ident
-> RecordMap Ident (SEval sym (GenValue sym))
-> Maybe (SEval sym (GenValue sym))
forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
f (GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
forall sym.
GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
fromVRecord GenValue sym
val) of
    Just SEval sym (GenValue sym)
x  -> SEval sym (GenValue sym)
x
    Maybe (SEval sym (GenValue sym))
Nothing -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"lookupRecord" [String
"malformed record"]