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

  , EvalOpts(..)
    -- ** Value introduction operations
  , word
  , lam
  , 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 Data.Ratio
import qualified Data.Map.Strict as Map
import MonadLib
import Numeric (showIntAtBase)

import Cryptol.Backend
import qualified Cryptol.Backend.Arch as Arch
import Cryptol.Backend.Monad
  ( evalPanic, wordTooWide, CallStack, combineCallStacks )
import Cryptol.Backend.FloatHelpers (fpPP)
import Cryptol.Eval.Type

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

import Data.List(genericIndex)

import GHC.Generics (Generic)

-- | Some options for evalutaion
data EvalOpts = EvalOpts
  { EvalOpts -> Logger
evalLogger :: Logger    -- ^ Where to print stuff (e.g., for @trace@)
  , EvalOpts -> PPOpts
evalPPOpts :: PPOpts    -- ^ How to pretty print things.
  }

-- 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 :: [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap :: [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap [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))
      (\Integer
i -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"finiteSeqMap" [String
"Out of bounds access of finite seq map", String
"length: " String -> String -> String
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), Integer -> String
forall a. Show a => a -> String
show Integer
i])

-- | Generate an infinite sequence map from a stream of values
infiniteSeqMap :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)
infiniteSeqMap :: sym -> [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)
infiniteSeqMap sym
sym [SEval sym (GenValue sym)]
xs =
   -- TODO: use an int-trie?
   sym -> SeqMap sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
sym -> SeqMap sym -> SEval sym (SeqMap sym)
memoMap sym
sym ((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 :: Backend sym => sym -> SeqMap sym -> SEval sym (SeqMap sym)
memoMap :: sym -> SeqMap sym -> SEval sym (SeqMap sym)
memoMap sym
sym SeqMap sym
x = do
  CallStack
stk <- sym -> SEval sym CallStack
forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym
  IORef (Map Integer (GenValue sym))
cache <- IO (IORef (Map Integer (GenValue sym)))
-> SEval sym (IORef (Map Integer (GenValue sym)))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef (Map Integer (GenValue sym)))
 -> SEval sym (IORef (Map Integer (GenValue sym))))
-> IO (IORef (Map Integer (GenValue sym)))
-> SEval sym (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 -> SEval sym (SeqMap sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap sym -> SEval sym (SeqMap sym))
-> SeqMap sym -> SEval sym (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))
-> CallStack -> Integer -> SEval sym (GenValue sym)
memo IORef (Map Integer (GenValue sym))
cache CallStack
stk)

  where
  memo :: IORef (Map Integer (GenValue sym))
-> CallStack -> Integer -> SEval sym (GenValue sym)
memo IORef (Map Integer (GenValue sym))
cache CallStack
stk 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 -> sym
-> CallStack
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym a.
Backend sym =>
sym -> CallStack -> SEval sym a -> SEval sym a
sWithCallStack sym
sym CallStack
stk (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 =>
  sym ->
  (GenValue sym -> GenValue sym -> SEval sym (GenValue sym)) ->
  SeqMap sym ->
  SeqMap sym ->
  SEval sym (SeqMap sym)
zipSeqMap :: sym
-> (GenValue sym -> GenValue sym -> SEval sym (GenValue sym))
-> SeqMap sym
-> SeqMap sym
-> SEval sym (SeqMap sym)
zipSeqMap sym
sym GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
f SeqMap sym
x SeqMap sym
y =
  sym -> SeqMap sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
sym -> SeqMap sym -> SEval sym (SeqMap sym)
memoMap sym
sym ((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 =>
  sym ->
  (GenValue sym -> SEval sym (GenValue sym)) ->
  SeqMap sym -> SEval sym (SeqMap sym)
mapSeqMap :: sym
-> (GenValue sym -> SEval sym (GenValue sym))
-> SeqMap sym
-> SEval sym (SeqMap sym)
mapSeqMap sym
sym GenValue sym -> SEval sym (GenValue sym)
f SeqMap sym
x =
  sym -> SeqMap sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
sym -> SeqMap sym -> SEval sym (SeqMap sym)
memoMap sym
sym ((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  CallStack (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -- ^ functions
  | VPoly CallStack (TValue -> SEval sym (GenValue sym))   -- ^ polymorphic values (kind *)
  | VNumPoly CallStack (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 ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VPoly{}     -> () -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VNumPoly{}  -> () -> 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 -> String -> String
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 -> String -> String
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 -> String -> String
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 -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
    VStream SeqMap sym
_  -> String
"stream"
    VFun{}     -> String
"fun"
    VPoly{}    -> String
"poly"
    VNumPoly{} -> 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             -> sym -> SBit sym -> SEval sym Doc
forall sym. Backend sym => sym -> SBit sym -> SEval sym Doc
ppSBit sym
x SBit sym
b
    VInteger SInteger sym
i         -> sym -> SInteger sym -> SEval sym Doc
forall sym. Backend sym => sym -> SInteger sym -> SEval sym Doc
ppSInteger sym
x SInteger sym
i
    VRational SRational sym
q        -> sym -> SRational sym -> SEval sym Doc
forall sym. Backend sym => sym -> SRational sym -> SEval sym Doc
ppSRational sym
x SRational sym
q
    VFloat SFloat sym
i           -> sym -> PPOpts -> SFloat sym -> SEval sym Doc
forall sym.
Backend sym =>
sym -> PPOpts -> SFloat sym -> SEval sym Doc
ppSFloat 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{}             -> 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{}            -> 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{}         -> 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 -> SEval sym Doc
forall sym.
Backend sym =>
sym -> PPOpts -> SWord sym -> SEval sym Doc
ppSWord sym
x PPOpts
opts (SWord sym -> SEval sym Doc)
-> SEval sym (SWord sym) -> SEval sym Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m 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 (String -> String
forall a. Show a => a -> String
show String
str)
                Maybe String
_ -> do [Doc]
vs' <- (SWord sym -> SEval sym Doc) -> [SWord sym] -> SEval sym [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (sym -> PPOpts -> SWord sym -> SEval sym Doc
forall sym.
Backend sym =>
sym -> PPOpts -> SWord sym -> SEval sym Doc
ppSWord sym
x PPOpts
opts) [SWord sym]
vs
                        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]
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'))

ppSBit :: Backend sym => sym -> SBit sym -> SEval sym Doc
ppSBit :: sym -> SBit sym -> SEval sym Doc
ppSBit sym
sym SBit sym
b =
  case sym -> SBit sym -> Maybe Bool
forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b of
    Just Bool
True  -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"True")
    Just Bool
False -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"False")
    Maybe Bool
Nothing    -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"?")

ppSInteger :: Backend sym => sym -> SInteger sym -> SEval sym Doc
ppSInteger :: sym -> SInteger sym -> SEval sym Doc
ppSInteger sym
sym SInteger sym
x =
  case sym -> SInteger sym -> Maybe Integer
forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
x of
    Just Integer
i  -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Doc
integer Integer
i)
    Maybe Integer
Nothing -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"[?]")

ppSFloat :: Backend sym => sym -> PPOpts -> SFloat sym -> SEval sym Doc
ppSFloat :: sym -> PPOpts -> SFloat sym -> SEval sym Doc
ppSFloat sym
sym PPOpts
opts SFloat sym
x =
  case sym -> SFloat sym -> Maybe BF
forall sym. Backend sym => sym -> SFloat sym -> Maybe BF
fpAsLit sym
sym SFloat sym
x of
    Just BF
fp -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PPOpts -> BF -> Doc
fpPP PPOpts
opts BF
fp)
    Maybe BF
Nothing -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"[?]")

ppSRational :: Backend sym => sym -> SRational sym -> SEval sym Doc
ppSRational :: sym -> SRational sym -> SEval sym Doc
ppSRational sym
sym (SRational SInteger sym
n SInteger sym
d)
  | Just Integer
ni <- sym -> SInteger sym -> Maybe Integer
forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
n
  , Just Integer
di <- sym -> SInteger sym -> Maybe Integer
forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
d
  = let q :: Ratio Integer
q = Integer
ni Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
di in
      Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"(ratio" Doc -> Doc -> Doc
<+> Integer -> Doc
integer (Ratio Integer -> Integer
forall a. Ratio a -> a
numerator Ratio Integer
q) Doc -> Doc -> Doc
<+> (Integer -> Doc
integer (Ratio Integer -> Integer
forall a. Ratio a -> a
denominator Ratio Integer
q) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
")"))

  | Bool
otherwise
  = do Doc
n' <- sym -> SInteger sym -> SEval sym Doc
forall sym. Backend sym => sym -> SInteger sym -> SEval sym Doc
ppSInteger sym
sym SInteger sym
n
       Doc
d' <- sym -> SInteger sym -> SEval sym Doc
forall sym. Backend sym => sym -> SInteger sym -> SEval sym Doc
ppSInteger sym
sym SInteger sym
d
       Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"(ratio" Doc -> Doc -> Doc
<+> Doc
n' Doc -> Doc -> Doc
<+> (Doc
d' Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
")"))

ppSWord :: Backend sym => sym -> PPOpts -> SWord sym -> SEval sym Doc
ppSWord :: sym -> PPOpts -> SWord sym -> SEval sym Doc
ppSWord sym
sym PPOpts
opts SWord sym
bv
  | PPOpts -> Integer -> Bool
asciiMode PPOpts
opts Integer
width =
      case sym -> SWord sym -> Maybe (Integer, Integer)
forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
bv of
        Just (Integer
_,Integer
i) -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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)))
        Maybe (Integer, Integer)
Nothing    -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"?")

  | Bool
otherwise =
      case sym -> SWord sym -> Maybe (Integer, Integer)
forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
bv of
        Just (Integer
_,Integer
i) ->
          let val :: String
val = Integer -> String
value Integer
i in
          Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Doc
prefix (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
val) Doc -> Doc -> Doc
<.> String -> Doc
text String
val)
        Maybe (Integer, Integer)
Nothing
          | Int
base Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2  -> Integer -> String -> SEval sym Doc
sliceDigits Integer
1 String
"0b"
          | Int
base Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
8  -> Integer -> String -> SEval sym Doc
sliceDigits Integer
3 String
"0o"
          | Int
base Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
16 -> Integer -> String -> SEval sym Doc
sliceDigits Integer
4 String
"0x"
          | Bool
otherwise  -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"[?]")

  where
  width :: Integer
width = sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
bv

  base :: Int
base = if PPOpts -> Int
useBase PPOpts
opts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
36 then Int
10 else PPOpts -> Int
useBase PPOpts
opts

  padding :: Int -> Int -> Doc
padding Int
bitsPerDigit Int
len = String -> Doc
text (Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
padLen Char
'0')
    where
    padLen :: Int
padLen | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0     = Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
           | Bool
otherwise = Int
d

    (Int
d,Int
m) = (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
width Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Int
len 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 :: Int -> Doc
prefix Int
len = case Int
base of
    Int
2  -> String -> Doc
text String
"0b" Doc -> Doc -> Doc
<.> Int -> Int -> Doc
padding Int
1 Int
len
    Int
8  -> String -> Doc
text String
"0o" Doc -> Doc -> Doc
<.> Int -> Int -> Doc
padding Int
3 Int
len
    Int
10 -> Doc
empty
    Int
16 -> String -> Doc
text String
"0x" Doc -> Doc -> Doc
<.> Int -> Int -> Doc
padding Int
4 Int
len
    Int
_  -> String -> Doc
text String
"0"  Doc -> Doc -> Doc
<.> Char -> Doc
char Char
'<' Doc -> Doc -> Doc
<.> Int -> Doc
int Int
base Doc -> Doc -> Doc
<.> Char -> Doc
char Char
'>'

  value :: Integer -> String
value Integer
i = Integer -> (Int -> Char) -> Integer -> String -> String
forall a.
(Integral a, Show a) =>
a -> (Int -> Char) -> a -> String -> String
showIntAtBase (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
base) (String
digits String -> Int -> Char
forall a. [a] -> Int -> a
!!) Integer
i String
""
  digits :: String
digits  = String
"0123456789abcdefghijklmnopqrstuvwxyz"

  toDigit :: SWord sym -> Char
toDigit SWord sym
w =
    case sym -> SWord sym -> Maybe (Integer, Integer)
forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
w of
      Just (Integer
_,Integer
i) | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
36 -> String
digits String -> Int -> Char
forall a. [a] -> Int -> a
!! Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i
      Maybe (Integer, Integer)
_ -> Char
'?'

  sliceDigits :: Integer -> String -> SEval sym Doc
sliceDigits Integer
bits String
pfx =
    do [SWord sym]
ws <- Integer -> [SWord sym] -> SWord sym -> SEval sym [SWord sym]
goDigits Integer
bits [] SWord sym
bv
       let ds :: String
ds = (SWord sym -> Char) -> [SWord sym] -> String
forall a b. (a -> b) -> [a] -> [b]
map SWord sym -> Char
toDigit [SWord sym]
ws
       Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
pfx Doc -> Doc -> Doc
<.> String -> Doc
text String
ds)

  goDigits :: Integer -> [SWord sym] -> SWord sym -> SEval sym [SWord sym]
goDigits Integer
bits [SWord sym]
ds SWord sym
w
    | sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
bits =
        do (SWord sym
hi,SWord sym
lo) <- sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
splitWord sym
sym (sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
bits) Integer
bits SWord sym
w
           Integer -> [SWord sym] -> SWord sym -> SEval sym [SWord sym]
goDigits Integer
bits (SWord sym
loSWord sym -> [SWord sym] -> [SWord sym]
forall a. a -> [a] -> [a]
:[SWord sym]
ds) SWord sym
hi

    | sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = [SWord sym] -> SEval sym [SWord sym]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord sym
wSWord sym -> [SWord sym] -> [SWord sym]
forall a. a -> [a] -> [a]
:[SWord sym]
ds)

    | Bool
otherwise          = [SWord sym] -> SEval sym [SWord sym]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [SWord sym]
ds

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


-- | Construct a function value
lam :: Backend sym => sym -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
lam :: sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
lam sym
sym SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f = CallStack
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
CallStack
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun (CallStack
 -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> SEval sym CallStack
-> SEval
     sym
     ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
      -> GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SEval sym CallStack
forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym SEval
  sym
  ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
   -> GenValue sym)
-> SEval sym (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
forall (f :: * -> *) a. Applicative f => a -> f a
pure SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f

-- | Functions that assume floating point inputs
flam :: Backend sym => sym ->
        (SFloat sym -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
flam :: sym
-> (SFloat sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
flam sym
sym SFloat sym -> SEval sym (GenValue sym)
f = CallStack
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
CallStack
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun (CallStack
 -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> SEval sym CallStack
-> SEval
     sym
     ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
      -> GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SEval sym CallStack
forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym SEval
  sym
  ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
   -> GenValue sym)
-> SEval sym (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (\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 => sym -> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
tlam :: sym
-> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
tlam sym
sym TValue -> SEval sym (GenValue sym)
f = CallStack -> (TValue -> SEval sym (GenValue sym)) -> GenValue sym
forall sym.
CallStack -> (TValue -> SEval sym (GenValue sym)) -> GenValue sym
VPoly (CallStack -> (TValue -> SEval sym (GenValue sym)) -> GenValue sym)
-> SEval sym CallStack
-> SEval sym ((TValue -> SEval sym (GenValue sym)) -> GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SEval sym CallStack
forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym SEval sym ((TValue -> SEval sym (GenValue sym)) -> GenValue sym)
-> SEval sym (TValue -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TValue -> SEval sym (GenValue sym))
-> SEval sym (TValue -> SEval sym (GenValue sym))
forall (f :: * -> *) a. Applicative f => a -> f a
pure TValue -> SEval sym (GenValue sym)
f

-- | A type lambda that expects a 'Type' of kind #.
nlam :: Backend sym => sym -> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
nlam :: sym
-> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
nlam sym
sym Nat' -> SEval sym (GenValue sym)
f = CallStack -> (Nat' -> SEval sym (GenValue sym)) -> GenValue sym
forall sym.
CallStack -> (Nat' -> SEval sym (GenValue sym)) -> GenValue sym
VNumPoly (CallStack -> (Nat' -> SEval sym (GenValue sym)) -> GenValue sym)
-> SEval sym CallStack
-> SEval sym ((Nat' -> SEval sym (GenValue sym)) -> GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SEval sym CallStack
forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym SEval sym ((Nat' -> SEval sym (GenValue sym)) -> GenValue sym)
-> SEval sym (Nat' -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Nat' -> SEval sym (GenValue sym))
-> SEval sym (Nat' -> SEval sym (GenValue sym))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nat' -> SEval sym (GenValue sym)
f

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

-- | Generate a stream.
toStream :: Backend sym => sym -> [GenValue sym] -> SEval sym (GenValue sym)
toStream :: sym -> [GenValue sym] -> SEval sym (GenValue sym)
toStream sym
sym [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
<$> sym -> [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)
infiniteSeqMap 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)

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
$ [SEval sym (GenValue sym)] -> SeqMap sym
forall sym. [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap ((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   -> sym -> [GenValue sym] -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> [GenValue sym] -> SEval sym (GenValue sym)
toStream sym
sym [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 :: Backend sym => sym -> GenValue sym -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
fromVFun :: sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym GenValue sym
val = case GenValue sym
val of
  VFun CallStack
fnstk SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f ->
    \SEval sym (GenValue sym)
x -> sym
-> (CallStack -> CallStack)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym a.
Backend sym =>
sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
sModifyCallStack sym
sym (\CallStack
stk -> CallStack -> CallStack -> CallStack
combineCallStacks CallStack
stk CallStack
fnstk) (SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f SEval sym (GenValue sym)
x)
  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 :: Backend sym => sym -> GenValue sym -> (TValue -> SEval sym (GenValue sym))
fromVPoly :: sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
fromVPoly sym
sym GenValue sym
val = case GenValue sym
val of
  VPoly CallStack
fnstk TValue -> SEval sym (GenValue sym)
f ->
    \TValue
x -> sym
-> (CallStack -> CallStack)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym a.
Backend sym =>
sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
sModifyCallStack sym
sym (\CallStack
stk -> CallStack -> CallStack -> CallStack
combineCallStacks CallStack
stk CallStack
fnstk) (TValue -> SEval sym (GenValue sym)
f TValue
x)
  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 :: Backend sym => sym -> GenValue sym -> (Nat' -> SEval sym (GenValue sym))
fromVNumPoly :: sym -> GenValue sym -> Nat' -> SEval sym (GenValue sym)
fromVNumPoly sym
sym GenValue sym
val = case GenValue sym
val of
  VNumPoly CallStack
fnstk Nat' -> SEval sym (GenValue sym)
f ->
    \Nat'
x -> sym
-> (CallStack -> CallStack)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym a.
Backend sym =>
sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
sModifyCallStack sym
sym (\CallStack
stk -> CallStack -> CallStack -> CallStack
combineCallStacks CallStack
stk CallStack
fnstk) (Nat' -> SEval sym (GenValue sym)
f Nat'
x)
  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"]