-- |
-- 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 ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}

module Cryptol.Eval.Value
  ( -- * GenericValue
    GenValue(..)
  , forceValue
  , Backend(..)
  , asciiMode

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

import Data.Ratio
import Numeric (showIntAtBase)

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

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 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)]              -- ^ @ ( .. ) @
  | VBit !(SBit sym)                           -- ^ @ Bit    @
  | VInteger !(SInteger sym)                   -- ^ @ Integer @ or @ Z n @
  | VRational !(SRational sym)                 -- ^ @ Rational @
  | VFloat !(SFloat sym)
  | VSeq !Integer !(SeqMap sym (GenValue sym)) -- ^ @ [n]a   @
                                               --   Invariant: VSeq is never a sequence of bits
  | VWord !Integer !(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 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 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  -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall sym. Backend sym => GenValue sym -> SEval sym ()
forceValue 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   -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall sym. Backend sym => GenValue sym -> SEval sym ()
forceValue forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) [SEval sym (GenValue sym)]
xs
  VSeq Integer
n SeqMap sym (GenValue sym)
xs   -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall sym. Backend sym => GenValue sym -> SEval sym ()
forceValue forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (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      -> seq :: forall a b. a -> b -> b
seq SBit sym
b (forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VInteger SInteger sym
i  -> seq :: forall a b. a -> b -> b
seq SInteger sym
i (forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VRational SRational sym
q -> seq :: forall a b. a -> b -> b
seq SRational sym
q (forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VFloat SFloat sym
f    -> seq :: forall a b. a -> b -> b
seq SFloat sym
f (forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VWord Integer
_ WordValue sym
wv  -> forall sym. Backend sym => WordValue sym -> SEval sym ()
forceWordValue WordValue sym
wv
  VStream SeqMap sym (GenValue sym)
_   -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VFun{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VPoly{}     -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VNumPoly{}  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()



instance 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:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a b. RecordMap a b -> [a]
displayOrder RecordMap Ident (SEval sym (GenValue sym))
fs)
    VTuple [SEval sym (GenValue sym)]
xs  -> String
"tuple:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (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 (GenValue sym)
_   -> String
"seq:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n
    VWord Integer
n WordValue sym
_  -> String
"word:"  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n
    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 = 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' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (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
                             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
ppRecord (forall a b. (a -> b) -> [a] -> [b]
map 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) = 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' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=GenValue sym -> SEval sym Doc
loop) [SEval sym (GenValue sym)]
vals
                             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
ppTuple [Doc]
vals'
    VBit SBit sym
b             -> forall sym. Backend sym => sym -> SBit sym -> SEval sym Doc
ppSBit sym
x SBit sym
b
    VInteger SInteger sym
i         -> forall sym. Backend sym => sym -> SInteger sym -> SEval sym Doc
ppSInteger sym
x SInteger sym
i
    VRational SRational sym
q        -> forall sym. Backend sym => sym -> SRational sym -> SEval sym Doc
ppSRational sym
x SRational sym
q
    VFloat SFloat sym
i           -> 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 Integer
_ WordValue sym
wv         -> WordValue sym -> SEval sym Doc
ppWordVal WordValue sym
wv
    VStream SeqMap sym (GenValue sym)
vals       -> do [Doc]
vals' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=GenValue sym -> SEval sym Doc
loop) forall a b. (a -> b) -> a -> b
$ 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
                             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
ppList ( [Doc]
vals' forall a. [a] -> [a] -> [a]
++ [String -> Doc
text String
"..."] )
    VFun{}             -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"<function>"
    VPoly{}            -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"<polymorphic value>"
    VNumPoly{}         -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 -> forall a b. (Show a, Ord a) => RecordMap a b -> [(a, b)]
displayFields
    FieldOrder
CanonicalOrder -> forall a b. RecordMap a b -> [(a, b)]
canonicalFields

  ppWordVal :: WordValue sym -> SEval sym Doc
  ppWordVal :: WordValue sym -> SEval sym Doc
ppWordVal WordValue sym
w = forall sym.
Backend sym =>
sym -> PPOpts -> SWord sym -> SEval sym Doc
ppSWord sym
x PPOpts
opts forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (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 <- forall sym. Backend sym => GenValue sym -> Maybe Integer
vWordLen GenValue sym
w
        , PPOpts -> Integer -> Bool
asciiMode PPOpts
opts Integer
l
        -> do [SWord sym]
vs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
x String
"ppWordSeq") [GenValue sym]
ws
              case forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym. Backend sym => sym -> SWord sym -> Maybe Char
wordAsChar sym
x) [SWord sym]
vs of
                Just String
str -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> Doc
text (forall a. Show a => a -> String
show String
str)
                Maybe String
_ -> do [Doc]
vs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym.
Backend sym =>
sym -> PPOpts -> SWord sym -> SEval sym Doc
ppSWord sym
x PPOpts
opts) [SWord sym]
vs
                        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
ppList [Doc]
vs'
      [GenValue sym]
_ -> do [Doc]
ws' <- 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
              forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b of
    Just Bool
True  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"True")
    Just Bool
False -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"False")
    Maybe Bool
Nothing    -> 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 forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
x of
    Just Integer
i  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Doc
integer Integer
i)
    Maybe Integer
Nothing -> 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 forall sym. Backend sym => sym -> SFloat sym -> Maybe BF
fpAsLit sym
sym SFloat sym
x of
    Just BF
fp -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (PPOpts -> BF -> Doc
fpPP PPOpts
opts BF
fp)
    Maybe BF
Nothing -> 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 <- forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
n
  , Just Integer
di <- forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
d
  = let q :: Ratio Integer
q = Integer
ni forall a. Integral a => a -> a -> Ratio a
% Integer
di in
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"(ratio" Doc -> Doc -> Doc
<+> Integer -> Doc
integer (forall a. Ratio a -> a
numerator Ratio Integer
q) Doc -> Doc -> Doc
<+> (Integer -> Doc
integer (forall a. Ratio a -> a
denominator Ratio Integer
q) forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
")"))

  | Bool
otherwise
  = do Doc
n' <- forall sym. Backend sym => sym -> SInteger sym -> SEval sym Doc
ppSInteger sym
sym SInteger sym
n
       Doc
d' <- forall sym. Backend sym => sym -> SInteger sym -> SEval sym Doc
ppSInteger sym
sym SInteger sym
d
       forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"(ratio" Doc -> Doc -> Doc
<+> Doc
n' Doc -> Doc -> Doc
<+> (Doc
d' 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 forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
bv of
        Just (Integer
_,Integer
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text (forall a. Show a => a -> String
show (forall a. Enum a => Int -> a
toEnum (forall a. Num a => Integer -> a
fromInteger Integer
i) :: Char)))
        Maybe (Integer, Integer)
Nothing    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"?")

  | Bool
otherwise =
      case 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
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Doc
prefix (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 forall a. Eq a => a -> a -> Bool
== Int
2  -> Integer -> String -> SEval sym Doc
sliceDigits Integer
1 String
"0b"
          | Int
base forall a. Eq a => a -> a -> Bool
== Int
8  -> Integer -> String -> SEval sym Doc
sliceDigits Integer
3 String
"0o"
          | Int
base forall a. Eq a => a -> a -> Bool
== Int
16 -> Integer -> String -> SEval sym Doc
sliceDigits Integer
4 String
"0x"
          | Bool
otherwise  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"[?]")

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

  base :: Int
base = if PPOpts -> Int
useBase PPOpts
opts 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 (forall a. Int -> a -> [a]
replicate Int
padLen Char
'0')
    where
    padLen :: Int
padLen | Int
m forall a. Ord a => a -> a -> Bool
> Int
0     = Int
d forall a. Num a => a -> a -> a
+ Int
1
           | Bool
otherwise = Int
d

    (Int
d,Int
m) = (forall a. Num a => Integer -> a
fromInteger Integer
width forall a. Num a => a -> a -> a
- (Int
len forall a. Num a => a -> a -> a
* Int
bitsPerDigit))
                   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 -> 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 = forall a. (Integral a, Show a) => a -> (Int -> Char) -> a -> ShowS
showIntAtBase (forall a. Integral a => a -> Integer
toInteger Int
base) (String
digits forall a. [a] -> Int -> a
!!) Integer
i String
""
  digits :: String
digits  = String
"0123456789abcdefghijklmnopqrstuvwxyz"

  toDigit :: SWord sym -> Char
toDigit SWord sym
w =
    case forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
w of
      Just (Integer
_,Integer
i) | Integer
i forall a. Ord a => a -> a -> Bool
<= Integer
36 -> String
digits forall a. [a] -> Int -> a
!! 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 = forall a b. (a -> b) -> [a] -> [b]
map SWord sym -> Char
toDigit [SWord sym]
ws
       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
    | forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w forall a. Ord a => a -> a -> Bool
> Integer
bits =
        do (SWord sym
hi,SWord sym
lo) <- forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
splitWord sym
sym (forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w 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
loforall a. a -> [a] -> [a]
:[SWord sym]
ds) SWord sym
hi

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

    | Bool
otherwise          = 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 forall a. Ord a => a -> a -> Bool
>= Integer
Arch.maxBigIntWidth = forall a. Integer -> a
wordTooWide Integer
n
  | Bool
otherwise                = forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. SWord sym -> WordValue sym
wordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall sym.
CallStack
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 = forall sym.
CallStack
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure (\SEval sym (GenValue sym)
arg -> SEval sym (GenValue sym)
arg forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SFloat sym -> SEval sym (GenValue sym)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall sym.
Backend sym =>
sym
-> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
tlam sym
sym TValue -> SEval sym (GenValue sym)
f = forall sym.
CallStack -> (TValue -> SEval sym (GenValue sym)) -> GenValue sym
VPoly forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 = forall sym.
CallStack -> (Nat' -> SEval sym (GenValue sym)) -> GenValue sym
VNumPoly forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 =
   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   -> forall a. HasCallStack => String -> [String] -> a
panic String
"ilam" [ String
"Unexpected `inf`" ])

-- | 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 -> forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n (forall sym. GenValue sym -> SBit sym
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqMap sym (GenValue sym)
vals)
    | Bool
otherwise   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
n SeqMap sym (GenValue sym)
vals
  Nat'
Inf             -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream SeqMap sym (GenValue sym)
vals


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

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

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

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

-- | Extract a finite sequence value.
fromVSeq :: GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq :: forall 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
_         -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVSeq" [String
"not a sequence", 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   -> forall (m :: * -> *) a. Monad m => a -> m a
return SeqMap sym (GenValue sym)
vs
  VStream SeqMap sym (GenValue sym)
vs  -> forall (m :: * -> *) a. Monad m => a -> m a
return SeqMap sym (GenValue sym)
vs
  GenValue sym
_           -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromSeq" [String
"not a sequence", String
msg, 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 Integer
_ WordValue sym
wval) = WordValue sym
wval
fromWordVal String
msg GenValue sym
val = forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromWordVal" [String
"not a word value", String
msg, 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) = forall a b. a -> Either a b
Left SInteger sym
i
asIndex sym
_sym String
_msg TValue
_ (VWord Integer
_ WordValue sym
wval) = forall a b. b -> Either a b
Right WordValue sym
wval
asIndex sym
_sym  String
msg TValue
_ GenValue sym
val = forall a. HasCallStack => String -> [String] -> a
evalPanic String
"asIndex" [String
"not an index value", String
msg, 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 Integer
_ WordValue sym
wval) = forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym WordValue sym
wval
fromVWord sym
_ String
msg GenValue sym
val = forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVWord" [String
"not a word", String
msg, 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 Integer
n WordValue sym
_wv              -> forall a. a -> Maybe a
Just Integer
n
  GenValue sym
_                        -> 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 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 [] = forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (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) =
    forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (GenValue sym)
v 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((forall sym. GenValue sym -> SBit sym
fromVBit GenValue sym
v')forall a. a -> [a] -> [a]
:)) [SEval sym (GenValue sym)]
vs
      Maybe (GenValue sym)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 -> 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
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVFun" [String
"not a function", 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 -> 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
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVPoly" [String
"not a polymorphic value", 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 -> 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
_  -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVNumPoly" [String
"not a polymorphic value", forall a. Show a => a -> String
show GenValue sym
val]

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

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

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

-- | Lookup a field in a record.
lookupRecord :: Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord :: forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
f GenValue sym
val =
  case forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
f (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 -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"lookupRecord" [String
"malformed record", forall a. Show a => a -> String
show GenValue sym
val]


-- Merge and if/then/else

{-# 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  <- forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b = SEval sym (GenValue sym)
x
  | Just Bool
False <- forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b = SEval sym (GenValue sym)
y
  | Bool
otherwise = 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

{-# 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 = 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 (forall sym.
Backend sym =>
sym
-> SBit sym
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
mergeValue sym
sym)

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 = 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 -> 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 -> forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Eval.Value" [ String
"mergeValue: incompatible record values", forall a. Show a => a -> String
show Either Ident Ident
f ]
           Right RecordMap Ident (SEval sym (GenValue sym))
r -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord RecordMap Ident (SEval sym (GenValue sym))
r)
    (VTuple [SEval sym (GenValue sym)]
vs1  , VTuple [SEval sym (GenValue sym)]
vs2  ) | forall (t :: * -> *) a. Foldable t => t a -> Int
length [SEval sym (GenValue sym)]
vs1 forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [SEval sym (GenValue sym)]
vs2  ->
                                  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (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     ) -> forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 ) -> forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) -> forall sym. SRational sym -> GenValue sym
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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)    -> forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 Integer
n1 WordValue sym
w1 , VWord Integer
n2 WordValue sym
w2 ) | Integer
n1 forall a. Eq a => a -> a -> Bool
== Integer
n2 -> forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
n1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
    (VSeq Integer
n1 SeqMap sym (GenValue sym)
vs1 , VSeq Integer
n2 SeqMap sym (GenValue sym)
vs2 ) | Integer
n1 forall a. Eq a => a -> a -> Bool
== Integer
n2 -> forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
n1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym (Integer -> Nat'
Nat Integer
n1) (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 ) -> forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym Nat'
Inf (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{}   ) -> forall sym.
Backend sym =>
sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
lam sym
sym forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
x -> 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 (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) (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{}  ) -> forall sym.
Backend sym =>
sym
-> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
tlam sym
sym forall a b. (a -> b) -> a -> b
$ \TValue
x -> 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 (forall sym.
Backend sym =>
sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
fromVPoly sym
sym GenValue sym
f1 TValue
x) (forall sym.
Backend sym =>
sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
fromVPoly sym
sym GenValue sym
f2 TValue
x)
    (GenValue sym
_           , GenValue sym
_           ) -> forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Eval.Value"
                                  [ String
"mergeValue: incompatible values", forall a. Show a => a -> String
show GenValue sym
v1, 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 =
  forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
    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 (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
x Integer
i) (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
y Integer
i)