{-# 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
(
GenValue(..)
, forceValue
, Backend(..)
, asciiMode
, EvalOpts(..)
, word
, lam
, flam
, tlam
, nlam
, ilam
, mkSeq
, fromVBit
, fromVInteger
, fromVRational
, fromVFloat
, fromVSeq
, fromSeq
, fromWordVal
, asIndex
, fromVWord
, vWordLen
, tryFromBits
, fromVFun
, fromVPoly
, fromVNumPoly
, fromVTuple
, fromVRecord
, lookupRecord
, defaultPPOpts
, ppValue
, 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)
data EvalOpts = EvalOpts
{ EvalOpts -> Logger
evalLogger :: Logger
, EvalOpts -> PPOpts
evalPPOpts :: PPOpts
}
data GenValue sym
= VRecord !(RecordMap Ident (SEval sym (GenValue sym)))
| VTuple ![SEval sym (GenValue sym)]
| VBit !(SBit sym)
| VInteger !(SInteger sym)
| VRational !(SRational sym)
| VFloat !(SFloat sym)
| VSeq !Integer !(SeqMap sym (GenValue sym))
| VWord !Integer !(WordValue sym)
| VStream !(SeqMap sym (GenValue sym))
| VFun CallStack (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
| VPoly CallStack (TValue -> SEval sym (GenValue sym))
| VNumPoly CallStack (Nat' -> SEval sym (GenValue sym))
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
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"
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
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
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
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)
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
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
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`" ])
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
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]
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]
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]
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]
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]
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
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
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]
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]
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]
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]
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]
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]
{-# 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)