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

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}

module Cryptol.Eval.Value
  ( -- * GenericValue
    GenValue 
      (VRecord, VTuple
      , VEnum, VBit
      , VInteger, VRational
      , VFloat, VWord
      , VStream, VFun
      , VPoly, VNumPoly
      , VSeq) -- pattern synonym
  , ConValue
  , forceValue
  , Backend(..)
  , asciiMode

  , EvalOpts(..)
    -- ** Value introduction operations
  , word
  , lam
  , flam
  , tlam
  , nlam
  , ilam
  , FinSeq
  , toFinSeq
  , unsafeToFinSeq
  , finSeq
  , mkSeq
  , wordSeq
    -- ** Value eliminators
  , fromVBit
  , fromVInteger
  , fromVRational
  , fromVFloat
  , fromVSeq
  , fromSeq
  , fromWordVal
  , asIndex
  , fromVWord
  , vWordLen
  , tryFromBits
  , fromVFun
  , fromVPoly
  , fromVNumPoly
  , fromVTuple
  , fromVRecord
  , lookupRecord
  , fromVEnum
    -- ** Pretty printing
  , defaultPPOpts
  , ppValue
  , ppValuePrec
    -- * Merge and if/then/else
  , iteValue
  , caseValue, CaseCont(..)
  , mergeValue
  ) where

import Data.Ratio
import Numeric (showIntAtBase)
import Data.Map(Map)
import qualified Data.Map as Map
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IMap
import qualified Data.Vector as Vector

import Cryptol.Backend
import Cryptol.Backend.SeqMap
import qualified Cryptol.Backend.Arch as Arch
import Cryptol.Backend.Monad
  ( evalPanic, wordTooWide, CallStack, combineCallStacks,EvalError(..))
import Cryptol.Backend.FloatHelpers (fpPP)
import Cryptol.Backend.WordValue

import Cryptol.Eval.Type

import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))

import Cryptol.Utils.Ident (Ident,unpackIdent)
import Cryptol.Utils.Logger(Logger)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.PP
import Cryptol.Utils.RecordMap

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

-- | 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)]              -- ^ @ ( .. ) @
  | VEnum !(SInteger sym) !(IntMap (ConValue sym))
    -- ^ As an example, consider the enum value @Just ()@. The 'SInteger' is the
    -- tag (e.g., 'Just' would have the tag @0@), and the 'IntMap' contains the
    -- fields (e.g., @{ 0 -> ("Just",()) }@. The 'IntMap' is only really needed
    -- to represent symbolic values.
  | VBit !(SBit sym)                           -- ^ @ Bit    @
  | VInteger !(SInteger sym)                   -- ^ @ Integer @ or @ Z n @
  | VRational !(SRational sym)                 -- ^ @ Rational @
  | VFloat !(SFloat sym)
  | VSeqCtor !Integer !(SeqMap sym (GenValue sym)) -- ^ @ [n]a   @
                                                   --   Invariant: VSeqCtor is never a sequence of bits
                                                   --   This constructor is intentionally not exported
                                                   --   to preserve the invariant. Use smart constructors
                                                   --   such as 'mkSeq' or 'finSeq' instead.
  | VWord !(WordValue sym)                     -- ^ @ [n]Bit @
  | VStream !(SeqMap sym (GenValue 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
$cfrom :: forall sym x. GenValue sym -> Rep (GenValue sym) x
from :: forall x. GenValue sym -> Rep (GenValue sym) x
$cto :: forall sym x. Rep (GenValue sym) x -> GenValue sym
to :: forall x. Rep (GenValue sym) x -> GenValue sym
Generic

-- | A view-only pattern for deconstructing finite sequences. Use
--   'mkSeq' or 'finSeq' for construction.
pattern VSeq :: Integer -> SeqMap sym (GenValue sym) -> GenValue sym
pattern $mVSeq :: forall {r} {sym}.
GenValue sym
-> (Integer -> SeqMap sym (GenValue sym) -> r) -> ((# #) -> r) -> r
VSeq len vals <- VSeqCtor len vals

-- This is all GenValue constructors except for VSeqCtor, which
-- is instead swapped for the view-only VSeq pattern
{-# COMPLETE VRecord, VTuple, VEnum, VBit, VInteger,
             VRational, VFloat, VWord, VStream,
             VFun, VPoly, VNumPoly, VSeq #-}

type ConValue sym = ConInfo (SEval sym (GenValue sym))

-- | Force the evaluation of a value
forceValue :: Backend sym => GenValue sym -> SEval sym ()
forceValue :: forall sym. Backend sym => 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
  VEnum SInteger sym
i IntMap (ConValue sym)
xs  -> SInteger sym -> SEval sym () -> SEval sym ()
forall a b. a -> b -> b
seq SInteger sym
i ((ConValue sym -> SEval sym ())
-> IntMap (ConValue sym) -> SEval sym ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ConValue sym -> SEval sym ()
forall sym. Backend sym => ConValue sym -> SEval sym ()
forceConValue IntMap (ConValue sym)
xs)
  VSeq Integer
n SeqMap 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
=<<) (Integer -> SeqMap sym (GenValue sym) -> [SEval sym (GenValue sym)]
forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n SeqMap sym (GenValue sym)
xs)
  VBit SBit sym
b      -> SBit sym -> SEval sym () -> SEval sym ()
forall a b. a -> b -> b
seq SBit sym
b (() -> SEval sym ()
forall a. a -> SEval sym a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VInteger SInteger sym
i  -> SInteger sym -> SEval sym () -> SEval sym ()
forall a b. a -> b -> b
seq SInteger sym
i (() -> SEval sym ()
forall a. a -> SEval sym a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VRational SRational sym
q -> SRational sym -> SEval sym () -> SEval sym ()
forall a b. a -> b -> b
seq SRational sym
q (() -> SEval sym ()
forall a. a -> SEval sym a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VFloat SFloat sym
f    -> SFloat sym -> SEval sym () -> SEval sym ()
forall a b. a -> b -> b
seq SFloat sym
f (() -> SEval sym ()
forall a. a -> SEval sym a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VWord WordValue sym
wv    -> WordValue sym -> SEval sym ()
forall sym. Backend sym => WordValue sym -> SEval sym ()
forceWordValue WordValue sym
wv
  VStream SeqMap sym (GenValue sym)
_   -> () -> SEval sym ()
forall a. a -> SEval sym a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VFun{}      -> () -> SEval sym ()
forall a. a -> SEval sym a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VPoly{}     -> () -> SEval sym ()
forall a. a -> SEval sym a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VNumPoly{}  -> () -> SEval sym ()
forall a. a -> SEval sym a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

forceConValue :: Backend sym => ConValue sym -> SEval sym ()
forceConValue :: forall sym. Backend sym => ConValue sym -> SEval sym ()
forceConValue (ConInfo Ident
i Vector (SEval sym (GenValue sym))
vs) = Ident
i Ident -> SEval sym () -> SEval sym ()
forall a b. a -> b -> b
`seq` (SEval sym (GenValue sym) -> SEval sym ())
-> Vector (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
=<<) Vector (SEval sym (GenValue sym))
vs

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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SEval sym (GenValue sym)]
xs)
    VEnum SInteger sym
_ IntMap (ConValue sym)
_  -> String
"enum"
    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 (GenValue sym)
_   -> String
"seq:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
    VWord WordValue sym
wv    -> String
"word:"  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (WordValue sym -> Integer
forall sym. Backend sym => WordValue sym -> Integer
wordValWidth WordValue sym
wv)
    VStream SeqMap sym (GenValue 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 :: forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
ppValue sym
x PPOpts
opts = sym -> PPOpts -> Int -> GenValue sym -> SEval sym Doc
forall sym.
Backend sym =>
sym -> PPOpts -> Int -> GenValue sym -> SEval sym Doc
ppValuePrec sym
x PPOpts
opts Int
0

ppValuePrec :: forall sym.
  Backend sym =>
  sym ->
  PPOpts ->
  Int ->
  GenValue sym ->
  SEval sym Doc
ppValuePrec :: forall sym.
Backend sym =>
sym -> PPOpts -> Int -> GenValue sym -> SEval sym Doc
ppValuePrec sym
x PPOpts
opts = Int -> GenValue sym -> SEval sym Doc
loop
  where
  loop :: Int -> GenValue sym -> SEval sym Doc
  loop :: Int -> GenValue sym -> SEval sym Doc
loop Int
prec 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
traverse (SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym Doc) -> SEval sym Doc
forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> GenValue sym -> SEval sym Doc
loop Int
0) RecordMap Ident (SEval sym (GenValue sym))
fs
                             Doc -> SEval sym Doc
forall a. a -> SEval sym a
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
ppRecord (((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)]
fields 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym Doc) -> SEval sym Doc
forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=Int -> GenValue sym -> SEval sym Doc
loop Int
0) [SEval sym (GenValue sym)]
vals
                             Doc -> SEval sym Doc
forall a. a -> SEval sym a
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
ppTuple [Doc]
vals'
    VEnum SInteger sym
c IntMap (ConValue sym)
vs         -> Int -> SInteger sym -> IntMap (ConValue sym) -> SEval sym Doc
ppEnumVal Int
prec SInteger sym
c IntMap (ConValue sym)
vs
    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 (GenValue sym)
vals       -> Integer -> SeqMap sym (GenValue sym) -> SEval sym Doc
ppWordSeq Integer
sz SeqMap sym (GenValue sym)
vals
    VWord WordValue sym
wv           -> WordValue sym -> SEval sym Doc
ppWordVal WordValue sym
wv
    VStream SeqMap 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym Doc) -> SEval sym Doc
forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=Int -> GenValue sym -> SEval sym Doc
loop Int
0) ([SEval sym (GenValue sym)] -> SEval sym [Doc])
-> [SEval sym (GenValue sym)] -> SEval sym [Doc]
forall a b. (a -> b) -> a -> b
$ Int -> SeqMap sym (GenValue sym) -> [SEval sym (GenValue sym)]
forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap (PPOpts -> Int
useInfLength PPOpts
opts) SeqMap sym (GenValue sym)
vals
                             Doc -> SEval sym Doc
forall a. a -> SEval sym a
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
ppList ( [Doc]
vals' [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Doc
text String
"..."] )
    VFun{}             -> Doc -> SEval sym Doc
forall a. a -> SEval sym a
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 a. a -> SEval sym a
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 a. a -> SEval sym a
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>"

  fields :: RecordMap Ident Doc -> [(Ident, Doc)]
  fields :: RecordMap Ident Doc -> [(Ident, Doc)]
fields = case PPOpts -> FieldOrder
useFieldOrder PPOpts
opts of
    FieldOrder
DisplayOrder -> RecordMap Ident Doc -> [(Ident, Doc)]
forall a b. (Show a, Ord a) => RecordMap a b -> [(a, b)]
displayFields
    FieldOrder
CanonicalOrder -> RecordMap Ident Doc -> [(Ident, Doc)]
forall a b. RecordMap a b -> [(a, b)]
canonicalFields

  ppEnumVal :: Int -> SInteger sym -> IntMap (ConValue sym) -> SEval sym Doc
ppEnumVal Int
prec SInteger sym
i IntMap (ConValue sym)
mp =
    case sym -> SInteger sym -> Maybe Integer
forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
x SInteger sym
i of
      Just Integer
c ->
        case Int -> IntMap (ConValue sym) -> Maybe (ConValue sym)
forall a. Int -> IntMap a -> Maybe a
IMap.lookup (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
c) IntMap (ConValue sym)
mp of
          Just ConValue sym
con
            | ConValue sym -> Bool
forall a. ConInfo a -> Bool
isNullaryCon ConValue sym
con -> Doc -> SEval sym Doc
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ident -> Doc
forall a. PP a => a -> Doc
pp (ConValue sym -> Ident
forall a. ConInfo a -> Ident
conIdent ConValue sym
con))
            | Bool
otherwise ->
              do Vector Doc
vds <- (SEval sym (GenValue sym) -> SEval sym Doc)
-> Vector (SEval sym (GenValue sym)) -> SEval sym (Vector Doc)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse (SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym Doc) -> SEval sym Doc
forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> GenValue sym -> SEval sym Doc
loop Int
1) (ConValue sym -> Vector (SEval sym (GenValue sym))
forall a. ConInfo a -> Vector a
conFields ConValue sym
con)
                 let d :: Doc
d = Ident -> Doc
forall a. PP a => a -> Doc
pp (ConValue sym -> Ident
forall a. ConInfo a -> Ident
conIdent ConValue sym
con) Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (Vector Doc -> [Doc]
forall a. Vector a -> [a]
Vector.toList Vector Doc
vds)
                 Doc -> SEval sym Doc
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (if Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Doc -> Doc
parens Doc
d else Doc
d)
          Maybe (ConValue sym)
Nothing -> String -> [String] -> SEval sym Doc
forall a. HasCallStack => String -> [String] -> a
panic String
"ppEnumVal" [String
"Malformed enum value", Integer -> String
forall a. Show a => a -> String
show Integer
c]
      Maybe Integer
Nothing -> Doc -> SEval sym Doc
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"[?]")

  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 (GenValue sym) -> SEval sym Doc
  ppWordSeq :: Integer -> SeqMap sym (GenValue sym) -> SEval sym Doc
ppWordSeq Integer
sz SeqMap sym (GenValue 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)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence (Integer -> SeqMap sym (GenValue sym) -> [SEval sym (GenValue sym)]
forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
sz SeqMap sym (GenValue 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [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 a. a -> SEval sym a
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
_ -> 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> SEval sym a
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
ppList [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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Int -> GenValue sym -> SEval sym Doc
loop Int
0) [GenValue sym]
ws
              Doc -> SEval sym Doc
forall a. a -> SEval sym a
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
ppList [Doc]
ws'

ppSBit :: Backend sym => sym -> SBit sym -> SEval sym Doc
ppSBit :: forall sym. Backend sym => 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 a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"True")
    Just Bool
False -> Doc -> SEval sym Doc
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"False")
    Maybe Bool
Nothing    -> Doc -> SEval sym Doc
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"?")

ppSInteger :: Backend sym => sym -> SInteger sym -> SEval sym Doc
ppSInteger :: forall sym. Backend sym => 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 a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Doc
integer Integer
i)
    Maybe Integer
Nothing -> Doc -> SEval sym Doc
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"[?]")

ppSFloat :: Backend sym => sym -> PPOpts -> SFloat sym -> SEval sym Doc
ppSFloat :: forall sym.
Backend sym =>
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 a. a -> SEval sym a
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 a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"[?]")

ppSRational :: Backend sym => sym -> SRational sym -> SEval sym Doc
ppSRational :: forall sym. Backend sym => 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 a. a -> SEval sym a
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 a. a -> SEval sym a
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 :: forall sym.
Backend sym =>
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 a. a -> SEval sym a
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 a. a -> SEval sym a
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 a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Doc
prefix (String -> Int
forall a. [a] -> 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 a. a -> SEval sym a
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
forall a. Monoid a => a
mempty
    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 -> ShowS
forall a. Integral a => a -> (Int -> Char) -> a -> ShowS
showIntAtBase (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
base) (String
digits String -> Int -> Char
forall a. HasCallStack => [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. HasCallStack => [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 a. a -> SEval sym a
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 a. a -> SEval sym a
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 a. a -> SEval sym a
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 -> SEval sym (GenValue sym)
word :: forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (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 -> SEval sym (GenValue sym)
forall a. Integer -> a
wordTooWide Integer
n
  | Bool
otherwise                = WordValue sym -> GenValue sym
forall sym. WordValue sym -> GenValue sym
VWord (WordValue sym -> GenValue sym)
-> (SWord sym -> WordValue sym) -> SWord sym -> GenValue sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
wordVal (SWord sym -> GenValue sym)
-> SEval sym (SWord sym) -> SEval sym (GenValue 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 :: forall sym.
Backend sym =>
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 a b. SEval sym (a -> b) -> SEval sym a -> SEval sym b
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 a. a -> SEval sym a
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 :: forall sym.
Backend sym =>
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 a b. SEval sym (a -> b) -> SEval sym a -> SEval sym b
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 a. a -> SEval sym a
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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
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. Backend 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 :: forall sym.
Backend sym =>
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 a b. SEval sym (a -> b) -> SEval sym a -> SEval sym b
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 a. a -> SEval sym a
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 :: forall sym.
Backend sym =>
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 a b. SEval sym (a -> b) -> SEval sym a -> SEval sym b
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 a. a -> SEval sym a
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 :: forall sym.
Backend sym =>
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`" ])

-- | A finite sequence of non-VBit values. Used in 'finSeq' to
--   safely construct a 'VSeq'.
newtype FinSeq sym = FinSeq [SEval sym (GenValue sym)]

-- | Safely wrap a 'GenValue' list as a 'FinSeq'. Returns 'Nothing'
--   if any values are a 'VBit'.
toFinSeq :: Backend sym => [GenValue sym] -> Maybe (FinSeq sym)
toFinSeq :: forall sym. Backend sym => [GenValue sym] -> Maybe (FinSeq sym)
toFinSeq [GenValue sym]
xs = [SEval sym (GenValue sym)] -> FinSeq sym
forall sym. [SEval sym (GenValue sym)] -> FinSeq sym
FinSeq ([SEval sym (GenValue sym)] -> FinSeq sym)
-> Maybe [SEval sym (GenValue sym)] -> Maybe (FinSeq sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GenValue sym -> Maybe (SEval sym (GenValue sym)))
-> [GenValue sym] -> Maybe [SEval sym (GenValue sym)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM GenValue sym -> Maybe (SEval sym (GenValue sym))
forall {f :: * -> *} {sym}.
Applicative f =>
GenValue sym -> Maybe (f (GenValue sym))
go [GenValue sym]
xs
  where
    go :: GenValue sym -> Maybe (f (GenValue sym))
go GenValue sym
x = case GenValue sym
x of
      VBit SBit sym
_ -> Maybe (f (GenValue sym))
forall a. Maybe a
Nothing
      GenValue sym
_ -> f (GenValue sym) -> Maybe (f (GenValue sym))
forall a. a -> Maybe a
Just (GenValue sym -> f (GenValue sym)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure GenValue sym
x)

-- | Wrap a 'GenValue' thunk list as a 'FinSeq'. Any 'VBit' elements
--   will raise an runtime error when evaluated.
unsafeToFinSeq :: Backend sym => [SEval sym (GenValue sym)] -> FinSeq sym
unsafeToFinSeq :: forall sym. Backend sym => [SEval sym (GenValue sym)] -> FinSeq sym
unsafeToFinSeq [SEval sym (GenValue sym)]
xs = [SEval sym (GenValue sym)] -> FinSeq sym
forall sym. [SEval sym (GenValue sym)] -> FinSeq sym
FinSeq ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> [SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)]
forall a b. (a -> b) -> [a] -> [b]
map SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall {sym} {m :: * -> *}.
(Backend sym, Monad m) =>
m (GenValue sym) -> m (GenValue sym)
go [SEval sym (GenValue sym)]
xs)
  where
    go :: m (GenValue sym) -> m (GenValue sym)
go m (GenValue sym)
f = m (GenValue sym)
f m (GenValue sym)
-> (GenValue sym -> m (GenValue sym)) -> m (GenValue sym)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \GenValue sym
x -> case GenValue sym
x of
      VBit SBit sym
_ -> String -> [String] -> m (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"unsafeToFinSeq" [ String
"Unexpected `VBit`", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
x ]
      GenValue sym
_ -> GenValue sym -> m (GenValue sym)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure GenValue sym
x

-- | Construct a finite sequence from a 'FinSeq'. In contrast to
--   'mkSeq' this is a pure function. See 'toFinSeq' or 'unsafeToFinSeq'
--   for creating a 'FinSeq' from a list of values.
finSeq :: Backend sym => sym -> Integer -> FinSeq sym -> GenValue sym
finSeq :: forall sym.
Backend sym =>
sym -> Integer -> FinSeq sym -> GenValue sym
finSeq sym
sym Integer
len (FinSeq [SEval sym (GenValue sym)]
vs) = Integer -> SeqMap sym (GenValue sym) -> GenValue sym
forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeqCtor Integer
len (sym -> [SEval sym (GenValue sym)] -> SeqMap sym (GenValue sym)
forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
finiteSeqMap sym
sym [SEval sym (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.
mkSeq :: Backend sym => sym -> Nat' -> TValue -> SeqMap sym (GenValue sym) -> SEval sym (GenValue sym)
mkSeq :: forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym Nat'
len TValue
elty SeqMap sym (GenValue sym)
vals = case Nat'
len of
  Nat Integer
n
    | TValue -> Bool
isTBit TValue
elty -> WordValue sym -> GenValue sym
forall sym. WordValue sym -> GenValue sym
VWord (WordValue sym -> GenValue sym)
-> SEval sym (WordValue sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n (GenValue sym -> SBit sym
forall sym. Backend sym => GenValue sym -> SBit sym
fromVBit (GenValue sym -> SBit sym)
-> SeqMap sym (GenValue sym) -> SeqMap sym (SBit sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqMap sym (GenValue sym)
vals)
    | Bool
otherwise   -> GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym (GenValue sym) -> GenValue sym
forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeqCtor Integer
n SeqMap sym (GenValue sym)
vals
  Nat'
Inf             -> GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym (GenValue sym) -> GenValue sym
forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream SeqMap sym (GenValue sym)
vals

-- | Construct a finite sequence of word values.
wordSeq :: 
  Backend sym => 
  sym ->
  -- | The length of the sequence.
  Integer ->
  -- | The word size of the element type.
  Integer ->
  SeqMap sym (GenValue sym) -> 
  SEval sym (GenValue sym)
wordSeq :: forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
wordSeq sym
sym Integer
n Integer
w SeqMap sym (GenValue sym)
vals = sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym (Integer -> Nat'
Nat Integer
n) (Integer -> TValue -> TValue
TVSeq Integer
w TValue
TVBit) SeqMap sym (GenValue sym)
vals

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

-- | Extract a bit value.
fromVBit :: Backend sym => GenValue sym -> SBit sym
fromVBit :: forall sym. Backend sym => 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", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract an integer value.
fromVInteger :: Backend sym => GenValue sym -> SInteger sym
fromVInteger :: forall sym. Backend sym => 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", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract a rational value.
fromVRational :: Backend sym => GenValue sym -> SRational sym
fromVRational :: forall sym. Backend sym => 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", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

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

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

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

asIndex :: Backend sym =>
  sym -> String -> TValue -> GenValue sym -> Either (SInteger sym) (WordValue sym)
asIndex :: forall sym.
Backend sym =>
sym
-> String
-> TValue
-> GenValue sym
-> Either (SInteger sym) (WordValue sym)
asIndex sym
_sym String
_msg TValue
TVInteger (VInteger SInteger sym
i) = 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 WordValue sym
wval) = WordValue sym -> Either (SInteger sym) (WordValue sym)
forall a b. b -> Either a b
Right WordValue sym
wval
asIndex sym
_sym  String
msg TValue
_ GenValue sym
val = String -> [String] -> Either (SInteger sym) (WordValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"asIndex" [String
"not an index value", String
msg, GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

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

vWordLen :: Backend sym => GenValue sym -> Maybe Integer
vWordLen :: forall sym. Backend sym => GenValue sym -> Maybe Integer
vWordLen GenValue sym
val = case GenValue sym
val of
  VWord WordValue sym
wv              -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (WordValue sym -> Integer
forall sym. Backend sym => WordValue sym -> Integer
wordValWidth WordValue sym
wv)
  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)] -> SEval sym (Maybe (SWord sym))
tryFromBits :: forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
tryFromBits sym
sym = ([SBit sym] -> [SBit sym])
-> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
go [SBit sym] -> [SBit sym]
forall a. a -> a
id
  where
  go :: ([SBit sym] -> [SBit sym])
-> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
go [SBit sym] -> [SBit sym]
f [] = SWord sym -> Maybe (SWord sym)
forall a. a -> Maybe a
Just (SWord sym -> Maybe (SWord sym))
-> SEval sym (SWord sym) -> SEval sym (Maybe (SWord 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 ([SBit sym] -> [SBit sym]
f []))
  go [SBit sym] -> [SBit sym]
f (SEval sym (GenValue sym)
v : [SEval sym (GenValue sym)]
vs) =
    sym -> SEval sym (GenValue sym) -> SEval sym (Maybe (GenValue sym))
forall a. sym -> SEval sym a -> SEval sym (Maybe a)
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (GenValue sym)
v SEval sym (Maybe (GenValue sym))
-> (Maybe (GenValue sym) -> SEval sym (Maybe (SWord sym)))
-> SEval sym (Maybe (SWord sym))
forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just GenValue sym
v' -> ([SBit sym] -> [SBit sym])
-> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
go ([SBit sym] -> [SBit sym]
f ([SBit sym] -> [SBit sym])
-> ([SBit sym] -> [SBit sym]) -> [SBit sym] -> [SBit sym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((GenValue sym -> SBit sym
forall sym. Backend sym => GenValue sym -> SBit sym
fromVBit GenValue sym
v')SBit sym -> [SBit sym] -> [SBit sym]
forall a. a -> [a] -> [a]
:)) [SEval sym (GenValue sym)]
vs
      Maybe (GenValue sym)
Nothing -> Maybe (SWord sym) -> SEval sym (Maybe (SWord sym))
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (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 :: forall sym.
Backend sym =>
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 a.
sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
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", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract a polymorphic function from a value.
fromVPoly :: Backend sym => sym -> GenValue sym -> (TValue -> SEval sym (GenValue sym))
fromVPoly :: forall sym.
Backend sym =>
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 a.
sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
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", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract a polymorphic function from a value.
fromVNumPoly :: Backend sym => sym -> GenValue sym -> (Nat' -> SEval sym (GenValue sym))
fromVNumPoly :: forall sym.
Backend sym =>
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 a.
sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
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", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract a tuple from a value.
fromVTuple :: Backend sym => GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple :: forall sym.
Backend sym =>
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", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract a record from a value.
fromVRecord :: Backend sym => GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
fromVRecord :: forall sym.
Backend sym =>
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", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

fromVEnum :: Backend sym => GenValue sym -> (SInteger sym, IntMap (ConValue sym))
fromVEnum :: forall sym.
Backend sym =>
GenValue sym -> (SInteger sym, IntMap (ConValue sym))
fromVEnum GenValue sym
val =
  case GenValue sym
val of
    VEnum SInteger sym
c IntMap (ConValue sym)
xs -> (SInteger sym
c,IntMap (ConValue sym)
xs)
    GenValue sym
_          -> String -> [String] -> (SInteger sym, IntMap (ConValue sym))
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVEnum" [String
"not an enum", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

fromVFloat :: Backend sym => GenValue sym -> SFloat sym
fromVFloat :: forall sym. Backend sym => 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", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Lookup a field in a record.
lookupRecord :: Backend sym => Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord :: forall sym.
Backend sym =>
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.
Backend 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", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]


-- Merge and if/then/else and case

{-# INLINE iteValue #-}
iteValue :: Backend sym =>
  sym ->
  SBit sym ->
  SEval sym (GenValue sym) ->
  SEval sym (GenValue sym) ->
  SEval sym (GenValue sym)
iteValue :: forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue sym
sym SBit sym
b SEval sym (GenValue sym)
x SEval sym (GenValue sym)
y
  | Just Bool
True  <- sym -> SBit sym -> Maybe Bool
forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b = SEval sym (GenValue sym)
x
  | Just Bool
False <- sym -> SBit sym -> Maybe Bool
forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b = SEval sym (GenValue sym)
y
  | Bool
otherwise = sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
mergeValue' sym
sym SBit sym
b SEval sym (GenValue sym)
x SEval sym (GenValue sym)
y

data CaseCont sym = CaseCont
  { forall sym.
CaseCont sym
-> Map
     Ident ([SEval sym (GenValue sym)] -> SEval sym (GenValue sym))
caseCon  :: Map Ident ([SEval sym (GenValue sym)] -> SEval sym (GenValue sym))
  , forall sym. CaseCont sym -> Maybe (SEval sym (GenValue sym))
caseDflt :: Maybe (SEval sym (GenValue sym))
  }

caseValue :: Backend sym =>
  sym ->
  SInteger sym ->
  IntMap (ConValue sym) ->
  CaseCont sym ->
  SEval sym (GenValue sym)
caseValue :: forall sym.
Backend sym =>
sym
-> SInteger sym
-> IntMap (ConValue sym)
-> CaseCont sym
-> SEval sym (GenValue sym)
caseValue sym
sym SInteger sym
tag IntMap (ConValue sym)
alts CaseCont sym
k
  | Just Integer
c <- sym -> SInteger sym -> Maybe Integer
forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
tag =
    case Int -> IntMap (ConValue sym) -> Maybe (ConValue sym)
forall a. Int -> IntMap a -> Maybe a
IMap.lookup (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
c) IntMap (ConValue sym)
alts of
      Just ConValue sym
conV -> ConValue sym -> SEval sym (GenValue sym)
doCase ConValue sym
conV
      Maybe (ConValue sym)
Nothing -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"caseValue" [String
"Missing constructor for tag", Integer -> String
forall a. Show a => a -> String
show Integer
c]
  | Bool
otherwise = ((Int, ConValue sym)
 -> SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
-> [(Int, ConValue sym)]
-> SEval sym (GenValue sym)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Int, ConValue sym)
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
doSymCase (Maybe String -> SEval sym (GenValue sym)
doDefault Maybe String
forall a. Maybe a
Nothing) (IntMap (ConValue sym) -> [(Int, ConValue sym)]
forall a. IntMap a -> [(Int, a)]
IMap.toList IntMap (ConValue sym)
alts)
  where
  doSymCase :: (Int, ConValue sym)
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
doSymCase (Int
n,ConValue sym
con) SEval sym (GenValue sym)
otherOpts =
    do SInteger sym
expect <- sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)
       SBit sym
yes    <- sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq sym
sym SInteger sym
tag SInteger sym
expect
       sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue sym
sym SBit sym
yes (ConValue sym -> SEval sym (GenValue sym)
doCase ConValue sym
con) SEval sym (GenValue sym)
otherOpts

  doDefault :: Maybe String -> SEval sym (GenValue sym)
doDefault Maybe String
mb =
    case CaseCont sym -> Maybe (SEval sym (GenValue sym))
forall sym. CaseCont sym -> Maybe (SEval sym (GenValue sym))
caseDflt CaseCont sym
k of
      Just SEval sym (GenValue sym)
yes -> SEval sym (GenValue sym)
yes
      Maybe (SEval sym (GenValue sym))
Nothing  -> sym -> EvalError -> SEval sym (GenValue sym)
forall a. sym -> EvalError -> SEval sym a
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError sym
sym (Maybe String -> EvalError
NoMatchingConstructor Maybe String
mb)

  doCase :: ConValue sym -> SEval sym (GenValue sym)
doCase (ConInfo Ident
con Vector (SEval sym (GenValue sym))
fs) =
    case Ident
-> Map
     Ident ([SEval sym (GenValue sym)] -> SEval sym (GenValue sym))
-> Maybe ([SEval sym (GenValue sym)] -> SEval sym (GenValue sym))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
con (CaseCont sym
-> Map
     Ident ([SEval sym (GenValue sym)] -> SEval sym (GenValue sym))
forall sym.
CaseCont sym
-> Map
     Ident ([SEval sym (GenValue sym)] -> SEval sym (GenValue sym))
caseCon CaseCont sym
k) of
      Just [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)
yes -> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)
yes (Vector (SEval sym (GenValue sym)) -> [SEval sym (GenValue sym)]
forall a. Vector a -> [a]
Vector.toList Vector (SEval sym (GenValue sym))
fs)
      Maybe ([SEval sym (GenValue sym)] -> SEval sym (GenValue sym))
Nothing  -> Maybe String -> SEval sym (GenValue sym)
doDefault (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$! Ident -> String
unpackIdent Ident
con)

{-# INLINE mergeValue' #-}
mergeValue' :: Backend sym =>
  sym ->
  SBit sym ->
  SEval sym (GenValue sym) ->
  SEval sym (GenValue sym) ->
  SEval sym (GenValue sym)
mergeValue' :: forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
mergeValue' sym
sym = sym
-> (SBit sym
    -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym))
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall a.
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> SBit sym
-> SEval sym a
-> SEval sym a
-> SEval sym a
forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> SBit sym
-> SEval sym a
-> SEval sym a
-> SEval sym a
mergeEval sym
sym (sym
-> SBit sym
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
mergeValue sym
sym)

mergeConValue ::
  Backend sym => sym -> SBit sym -> ConValue sym -> ConValue sym -> ConValue sym
mergeConValue :: forall sym.
Backend sym =>
sym -> SBit sym -> ConValue sym -> ConValue sym -> ConValue sym
mergeConValue sym
sym SBit sym
c = (SEval sym (GenValue sym)
 -> SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> ConInfo (SEval sym (GenValue sym))
-> ConInfo (SEval sym (GenValue sym))
-> ConInfo (SEval sym (GenValue sym))
forall a b c. (a -> b -> c) -> ConInfo a -> ConInfo b -> ConInfo c
zipConInfo (sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
mergeValue' sym
sym SBit sym
c)

mergeValue :: Backend sym =>
  sym ->
  SBit sym ->
  GenValue sym ->
  GenValue sym ->
  SEval sym (GenValue sym)
mergeValue :: forall sym.
Backend sym =>
sym
-> SBit sym
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
mergeValue sym
sym SBit sym
c GenValue sym
v1 GenValue sym
v2 =
  case (GenValue sym
v1, GenValue sym
v2) of
    (VRecord RecordMap Ident (SEval sym (GenValue sym))
fs1 , VRecord RecordMap Ident (SEval sym (GenValue sym))
fs2 ) ->
      do let res :: Either
  (Either Ident Ident) (RecordMap Ident (SEval sym (GenValue sym)))
res = (Ident
 -> SEval sym (GenValue sym)
 -> SEval sym (GenValue sym)
 -> SEval sym (GenValue sym))
-> RecordMap Ident (SEval sym (GenValue sym))
-> RecordMap Ident (SEval sym (GenValue sym))
-> Either
     (Either Ident Ident) (RecordMap Ident (SEval sym (GenValue sym)))
forall a b c d.
Ord a =>
(a -> b -> c -> d)
-> RecordMap a b
-> RecordMap a c
-> Either (Either a a) (RecordMap a d)
zipRecords (\Ident
_lbl -> sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
mergeValue' sym
sym SBit sym
c) RecordMap Ident (SEval sym (GenValue sym))
fs1 RecordMap Ident (SEval sym (GenValue sym))
fs2
         case Either
  (Either Ident Ident) (RecordMap Ident (SEval sym (GenValue sym)))
res of
           Left Either Ident Ident
f -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Eval.Value" [ String
"mergeValue: incompatible record values", Either Ident Ident -> String
forall a. Show a => a -> String
show Either Ident Ident
f ]
           Right RecordMap Ident (SEval sym (GenValue sym))
r -> GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord RecordMap Ident (SEval sym (GenValue sym))
r)

    (VEnum SInteger sym
c1 IntMap (ConValue sym)
fs1, VEnum SInteger sym
c2 IntMap (ConValue sym)
fs2) ->
      SInteger sym -> IntMap (ConValue sym) -> GenValue sym
forall sym. SInteger sym -> IntMap (ConValue sym) -> GenValue sym
VEnum (SInteger sym -> IntMap (ConValue sym) -> GenValue sym)
-> SEval sym (SInteger sym)
-> SEval sym (IntMap (ConValue sym) -> GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
iteInteger sym
sym SBit sym
c SInteger sym
c1 SInteger sym
c2
            SEval sym (IntMap (ConValue sym) -> GenValue sym)
-> SEval sym (IntMap (ConValue sym)) -> SEval sym (GenValue sym)
forall a b. SEval sym (a -> b) -> SEval sym a -> SEval sym b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IntMap (ConValue sym) -> SEval sym (IntMap (ConValue sym))
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((ConValue sym -> ConValue sym -> ConValue sym)
-> IntMap (ConValue sym)
-> IntMap (ConValue sym)
-> IntMap (ConValue sym)
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IMap.unionWith (sym -> SBit sym -> ConValue sym -> ConValue sym -> ConValue sym
forall sym.
Backend sym =>
sym -> SBit sym -> ConValue sym -> ConValue sym -> ConValue sym
mergeConValue sym
sym SBit sym
c) IntMap (ConValue sym)
fs1 IntMap (ConValue sym)
fs2)

    (VTuple [SEval sym (GenValue sym)]
vs1  , VTuple [SEval sym (GenValue sym)]
vs2  ) | [SEval sym (GenValue sym)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SEval sym (GenValue sym)]
vs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [SEval sym (GenValue sym)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SEval sym (GenValue sym)]
vs2  ->
                                  GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ [SEval sym (GenValue sym)] -> GenValue sym
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple ([SEval sym (GenValue sym)] -> GenValue sym)
-> [SEval sym (GenValue sym)] -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (SEval sym (GenValue sym)
 -> SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
mergeValue' sym
sym SBit sym
c) [SEval sym (GenValue sym)]
vs1 [SEval sym (GenValue sym)]
vs2
    (VBit SBit sym
b1     , VBit SBit sym
b2     ) -> 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 -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
iteBit sym
sym SBit sym
c SBit sym
b1 SBit sym
b2
    (VInteger SInteger sym
i1 , VInteger SInteger sym
i2 ) -> SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
iteInteger sym
sym SBit sym
c SInteger sym
i1 SInteger sym
i2
    (VRational SRational sym
q1, VRational SRational sym
q2) -> SRational sym -> GenValue sym
forall sym. SRational sym -> GenValue sym
VRational (SRational sym -> GenValue sym)
-> SEval sym (SRational sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SBit sym
-> SRational sym
-> SRational sym
-> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SRational sym
-> SRational sym
-> SEval sym (SRational sym)
iteRational sym
sym SBit sym
c SRational sym
q1 SRational sym
q2
    (VFloat SFloat sym
f1   , VFloat SFloat sym
f2)    -> SFloat sym -> GenValue sym
forall sym. SFloat sym -> GenValue sym
VFloat (SFloat sym -> GenValue sym)
-> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SBit sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym
-> SBit sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
iteFloat sym
sym SBit sym
c SFloat sym
f1 SFloat sym
f2
    (VWord WordValue sym
w1    , VWord WordValue sym
w2 ) | WordValue sym -> Integer
forall sym. Backend sym => WordValue sym -> Integer
wordValWidth WordValue sym
w1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== WordValue sym -> Integer
forall sym. Backend sym => WordValue sym -> Integer
wordValWidth WordValue sym
w2 -> WordValue sym -> GenValue sym
forall sym. WordValue sym -> GenValue sym
VWord (WordValue sym -> GenValue sym)
-> SEval sym (WordValue sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SBit sym
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
mergeWord sym
sym SBit sym
c WordValue sym
w1 WordValue sym
w2
    (VSeqCtor Integer
n1 SeqMap sym (GenValue sym)
vs1 , VSeqCtor Integer
n2 SeqMap sym (GenValue sym)
vs2 ) | Integer
n1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n2 -> Integer -> SeqMap sym (GenValue sym) -> GenValue sym
forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeqCtor Integer
n1 (SeqMap sym (GenValue sym) -> GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Nat'
-> SeqMap sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym (Integer -> Nat'
Nat Integer
n1) (sym
-> SBit sym
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
mergeSeqMapVal sym
sym SBit sym
c SeqMap sym (GenValue sym)
vs1 SeqMap sym (GenValue sym)
vs2)
    (VStream SeqMap sym (GenValue sym)
vs1 , VStream SeqMap sym (GenValue sym)
vs2 ) -> SeqMap sym (GenValue sym) -> GenValue sym
forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream (SeqMap sym (GenValue sym) -> GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Nat'
-> SeqMap sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym Nat'
Inf (sym
-> SBit sym
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
mergeSeqMapVal sym
sym SBit sym
c SeqMap sym (GenValue sym)
vs1 SeqMap sym (GenValue sym)
vs2)
    (f1 :: GenValue sym
f1@VFun{}   , f2 :: GenValue sym
f2@VFun{}   ) -> sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
lam sym
sym ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> SEval sym (GenValue sym))
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
x -> sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
mergeValue' sym
sym SBit sym
c (sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym GenValue sym
f1 SEval sym (GenValue sym)
x) (sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym GenValue sym
f2 SEval sym (GenValue sym)
x)
    (f1 :: GenValue sym
f1@VPoly{}  , f2 :: GenValue sym
f2@VPoly{}  ) -> sym
-> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
tlam sym
sym ((TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym))
-> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ \TValue
x -> sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
mergeValue' sym
sym SBit sym
c (sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
fromVPoly sym
sym GenValue sym
f1 TValue
x) (sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
fromVPoly sym
sym GenValue sym
f2 TValue
x)
    (GenValue sym
_           , GenValue sym
_           ) -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Eval.Value"
                                  [ String
"mergeValue: incompatible values", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
v1, GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
v2 ]

{-# INLINE mergeSeqMapVal #-}
mergeSeqMapVal :: Backend sym =>
  sym ->
  SBit sym ->
  SeqMap sym (GenValue sym)->
  SeqMap sym (GenValue sym)->
  SeqMap sym (GenValue sym)
mergeSeqMapVal :: forall sym.
Backend sym =>
sym
-> SBit sym
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
mergeSeqMapVal sym
sym SBit sym
c SeqMap sym (GenValue sym)
x SeqMap sym (GenValue sym)
y =
  (Integer -> SEval sym (GenValue sym)) -> SeqMap sym (GenValue sym)
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap ((Integer -> SEval sym (GenValue sym))
 -> SeqMap sym (GenValue sym))
-> (Integer -> SEval sym (GenValue sym))
-> SeqMap sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
    sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue sym
sym SBit sym
c (SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
x Integer
i) (SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
y Integer
i)