{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module Cryptol.Eval.Generic where
import qualified Control.Exception as X
import Control.Monad(join)
import Control.Monad.IO.Class (MonadIO(..))
import System.Random.TF.Gen (seedTFGen)
import Data.Bits ((.&.), shiftR)
import Data.Maybe (fromMaybe)
import qualified Data.Map.Strict as Map
import Data.Map(Map)
import Data.Ratio ((%))
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul,nAdd)
import Cryptol.Backend
import Cryptol.Backend.Concrete (Concrete(..))
import Cryptol.Backend.Monad( Eval, evalPanic, EvalError(..), Unsupported(..) )
import Cryptol.Backend.SeqMap
import Cryptol.Backend.WordValue
import Cryptol.Testing.Random( randomValue )
import Cryptol.Eval.Prims
import Cryptol.Eval.Type
import Cryptol.Eval.Value
import Cryptol.Utils.Ident (PrimIdent, prelPrim, floatPrim)
import Cryptol.Utils.Logger(logPrint)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.PP
import Cryptol.Utils.RecordMap
{-# SPECIALIZE mkLit :: Concrete -> TValue -> Integer -> Eval (GenValue Concrete)
#-}
mkLit :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym)
mkLit :: forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
mkLit sym
sym TValue
ty Integer
i =
case TValue
ty of
TValue
TVBit -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. SBit sym -> GenValue sym
VBit (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym (Integer
i forall a. Ord a => a -> a -> Bool
> Integer
0))
TValue
TVInteger -> forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
i
TVIntMod Integer
m
| Integer
m forall a. Eq a => a -> a -> Bool
== Integer
0 -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"mkLit" [String
"0 modulus not allowed"]
| Bool
otherwise -> forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym (Integer
i forall a. Integral a => a -> a -> a
`mod` Integer
m)
TVFloat Integer
e Integer
p -> forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
fpLit sym
sym Integer
e Integer
p (forall a. Num a => Integer -> a
fromInteger Integer
i)
TVSeq Integer
w TValue
TVBit -> forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (GenValue sym)
word sym
sym Integer
w Integer
i
TValue
TVRational -> forall sym. SRational sym -> GenValue sym
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SRational sym)
intToRational sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
i)
TValue
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"Cryptol.Eval.Prim.evalConst"
[ String
"Invalid type for number" ]
{-# SPECIALIZE ecNumberV :: Concrete -> Prim Concrete
#-}
ecNumberV :: Backend sym => sym -> Prim sym
ecNumberV :: forall sym. Backend sym => sym -> Prim sym
ecNumberV sym
sym =
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
valT ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
case Nat'
valT of
Nat Integer
v -> forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
mkLit sym
sym TValue
ty Integer
v
Nat'
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"Cryptol.Eval.Prim.evalConst"
[String
"Unexpected Inf in constant."
, forall a. Show a => a -> String
show Nat'
valT
, forall a. Show a => a -> String
show TValue
ty
]
{-# SPECIALIZE intV :: Concrete -> Integer -> TValue -> Eval (GenValue Concrete)
#-}
intV :: Backend sym => sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
intV :: forall sym.
Backend sym =>
sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
intV sym
sym SInteger sym
i =
forall sym.
Backend sym =>
sym
-> (Integer -> SEval sym (SWord sym))
-> SEval sym (SInteger sym)
-> (Integer -> SEval sym (SInteger sym))
-> SEval sym (SRational sym)
-> (Integer -> Integer -> SEval sym (SFloat sym))
-> TValue
-> SEval sym (GenValue sym)
ringNullary sym
sym
(\Integer
w -> forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
wordFromInt sym
sym Integer
w SInteger sym
i)
(forall (f :: * -> *) a. Applicative f => a -> f a
pure SInteger sym
i)
(\Integer
m -> forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
intToZn sym
sym Integer
m SInteger sym
i)
(forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SRational sym)
intToRational sym
sym SInteger sym
i)
(\Integer
e Integer
p -> forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndMode sym
sym forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SWord sym
-> SInteger sym
-> SEval sym (SFloat sym)
fpFromInteger sym
sym Integer
e Integer
p SWord sym
r SInteger sym
i)
{-# SPECIALIZE ratioV :: Concrete -> Prim Concrete #-}
ratioV :: Backend sym => sym -> Prim sym
ratioV :: forall sym. Backend sym => sym -> Prim sym
ratioV sym
sym =
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
x ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
y ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do SInteger sym
x' <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
x
SInteger sym
y' <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
y
forall sym. SRational sym -> GenValue sym
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
ratio sym
sym SInteger sym
x' SInteger sym
y'
{-# SPECIALIZE ecFractionV :: Concrete -> Prim Concrete
#-}
ecFractionV :: Backend sym => sym -> Prim sym
ecFractionV :: forall sym. Backend sym => sym -> Prim sym
ecFractionV sym
sym =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
d ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_r ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
case TValue
ty of
TVFloat Integer
e Integer
p -> forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
fpLit sym
sym Integer
e Integer
p (Integer
n forall a. Integral a => a -> a -> Ratio a
% Integer
d)
TValue
TVRational ->
do SInteger sym
x <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
n
SInteger sym
y <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
d
forall sym. SRational sym -> GenValue sym
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
ratio sym
sym SInteger sym
x SInteger sym
y
TValue
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ecFractionV"
[ String
"Unexpected `FLiteral` type: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TValue
ty ]
{-# SPECIALIZE fromZV :: Concrete -> Prim Concrete #-}
fromZV :: Backend sym => sym -> Prim sym
fromZV :: forall sym. Backend sym => sym -> Prim sym
fromZV sym
sym =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
v ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
(forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
znToInt sym
sym Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. GenValue sym -> SInteger sym
fromVInteger forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
v))
type Binary sym = TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
{-# SPECIALIZE binary :: Binary Concrete -> Prim Concrete
#-}
binary :: Backend sym => Binary sym -> Prim sym
binary :: forall sym. Backend sym => Binary sym -> Prim sym
binary Binary sym
f = forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
a ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
b ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim forall a b. (a -> b) -> a -> b
$
do GenValue sym
x <- SEval sym (GenValue sym)
a
GenValue sym
y <- SEval sym (GenValue sym)
b
Binary sym
f TValue
ty GenValue sym
x GenValue sym
y
type Unary sym = TValue -> GenValue sym -> SEval sym (GenValue sym)
{-# SPECIALIZE unary :: Unary Concrete -> Prim Concrete
#-}
unary :: Backend sym => Unary sym -> Prim sym
unary :: forall sym. Backend sym => Unary sym -> Prim sym
unary Unary sym
f = forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
a ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (Unary sym
f TValue
ty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
a)
type BinWord sym = Integer -> SWord sym -> SWord sym -> SEval sym (SWord sym)
{-# SPECIALIZE ringBinary :: Concrete -> BinWord Concrete ->
(SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
(Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
(SRational Concrete -> SRational Concrete -> SEval Concrete (SRational Concrete)) ->
(SFloat Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)) ->
Binary Concrete
#-}
ringBinary :: forall sym.
Backend sym =>
sym ->
BinWord sym ->
(SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
(Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
(SRational sym -> SRational sym -> SEval sym (SRational sym)) ->
(SFloat sym -> SFloat sym -> SEval sym (SFloat sym)) ->
Binary sym
ringBinary :: forall sym.
Backend sym =>
sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (Integer
-> SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym))
-> Binary sym
ringBinary sym
sym BinWord sym
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz SRational sym -> SRational sym -> SEval sym (SRational sym)
opq SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp = TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
loop
where
loop' :: TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' :: TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' TValue
ty SEval sym (GenValue sym)
l SEval sym (GenValue sym)
r = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SEval sym (GenValue sym)
r)
loop :: TValue
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
loop :: TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
ty GenValue sym
l GenValue sym
r = case TValue
ty of
TValue
TVBit ->
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringBinary" [String
"Bit not in class Ring"]
TValue
TVInteger ->
forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi (forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
l) (forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
r)
TVIntMod Integer
n ->
forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz Integer
n (forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
l) (forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
r)
TVFloat {} ->
forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp (forall sym. GenValue sym -> SFloat sym
fromVFloat GenValue sym
l) (forall sym. GenValue sym -> SFloat sym
fromVFloat GenValue sym
r)
TValue
TVRational ->
forall sym. SRational sym -> GenValue sym
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRational sym -> SRational sym -> SEval sym (SRational sym)
opq (forall sym. GenValue sym -> SRational sym
fromVRational GenValue sym
l) (forall sym. GenValue sym -> SRational sym
fromVRational GenValue sym
r)
TVArray{} ->
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"arithBinary" [String
"Array not in class Ring"]
TVSeq Integer
w TValue
a
| TValue -> Bool
isTBit TValue
a -> do
SWord sym
lw <- forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"ringLeft" GenValue sym
l
SWord sym
rw <- forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"ringRight" GenValue sym
r
CallStack
stk <- forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w 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 a.
Backend sym =>
sym -> CallStack -> SEval sym a -> SEval sym a
sWithCallStack sym
sym CallStack
stk (BinWord sym
opw Integer
w SWord sym
lw SWord sym
rw))
| Bool
otherwise -> forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (forall sym a.
Backend sym =>
sym
-> (a -> a -> SEval sym a)
-> Nat'
-> SeqMap sym a
-> SeqMap sym a
-> SEval sym (SeqMap sym a)
zipSeqMap sym
sym (TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
a) (Integer -> Nat'
Nat Integer
w) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"ringBinary left" GenValue sym
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
(forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"ringBinary right" GenValue sym
r)))
TVStream TValue
a ->
forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (forall sym a.
Backend sym =>
sym
-> (a -> a -> SEval sym a)
-> Nat'
-> SeqMap sym a
-> SeqMap sym a
-> SEval sym (SeqMap sym a)
zipSeqMap sym
sym (TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
a) Nat'
Inf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"ringBinary left" GenValue sym
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
(forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"ringBinary right" GenValue sym
r)))
TVFun TValue
_ TValue
ety ->
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 -> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' TValue
ety (forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym GenValue sym
l 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
r SEval sym (GenValue sym)
x)
TVTuple [TValue]
tys ->
do [SEval sym (GenValue sym)]
ls <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym) (forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
l)
[SEval sym (GenValue sym)]
rs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym) (forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
r)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple (forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' [TValue]
tys [SEval sym (GenValue sym)]
ls [SEval sym (GenValue sym)]
rs)
TVRec RecordMap Ident TValue
fs ->
do forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
forall (t :: * -> *) a b c.
Applicative t =>
(a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
traverseRecordMap
(\Ident
f TValue
fty -> forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' TValue
fty (forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
f GenValue sym
l) (forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
f GenValue sym
r)))
RecordMap Ident TValue
fs
TVAbstract {} ->
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringBinary" [String
"Abstract type not in `Ring`"]
TVNewtype {} ->
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringBinary" [String
"Newtype not in `Ring`"]
type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym)
{-# SPECIALIZE ringUnary ::
Concrete ->
UnaryWord Concrete ->
(SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
(Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
(SRational Concrete -> SEval Concrete (SRational Concrete)) ->
(SFloat Concrete -> SEval Concrete (SFloat Concrete)) ->
Unary Concrete
#-}
ringUnary :: forall sym.
Backend sym =>
sym ->
UnaryWord sym ->
(SInteger sym -> SEval sym (SInteger sym)) ->
(Integer -> SInteger sym -> SEval sym (SInteger sym)) ->
(SRational sym -> SEval sym (SRational sym)) ->
(SFloat sym -> SEval sym (SFloat sym)) ->
Unary sym
ringUnary :: forall sym.
Backend sym =>
sym
-> UnaryWord sym
-> (SInteger sym -> SEval sym (SInteger sym))
-> (Integer -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SEval sym (SFloat sym))
-> Unary sym
ringUnary sym
sym UnaryWord sym
opw SInteger sym -> SEval sym (SInteger sym)
opi Integer -> SInteger sym -> SEval sym (SInteger sym)
opz SRational sym -> SEval sym (SRational sym)
opq SFloat sym -> SEval sym (SFloat sym)
opfp = TValue -> GenValue sym -> SEval sym (GenValue sym)
loop
where
loop' :: TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' :: TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' TValue
ty SEval sym (GenValue sym)
v = TValue -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
ty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
v
loop :: TValue -> GenValue sym -> SEval sym (GenValue sym)
loop :: TValue -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
ty GenValue sym
v = case TValue
ty of
TValue
TVBit ->
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringUnary" [String
"Bit not in class Ring"]
TValue
TVInteger ->
forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SInteger sym -> SEval sym (SInteger sym)
opi (forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
v)
TVIntMod Integer
n ->
forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> SInteger sym -> SEval sym (SInteger sym)
opz Integer
n (forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
v)
TVFloat {} ->
forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SFloat sym -> SEval sym (SFloat sym)
opfp (forall sym. GenValue sym -> SFloat sym
fromVFloat GenValue sym
v)
TValue
TVRational ->
forall sym. SRational sym -> GenValue sym
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRational sym -> SEval sym (SRational sym)
opq (forall sym. GenValue sym -> SRational sym
fromVRational GenValue sym
v)
TVArray{} ->
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"arithUnary" [String
"Array not in class Ring"]
TVSeq Integer
w TValue
a
| TValue -> Bool
isTBit TValue
a -> do
SWord sym
wx <- forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"ringUnary" GenValue sym
v
CallStack
stk <- forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w 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 a.
Backend sym =>
sym -> CallStack -> SEval sym a -> SEval sym a
sWithCallStack sym
sym CallStack
stk (UnaryWord sym
opw Integer
w SWord sym
wx)
| Bool
otherwise -> forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym a.
Backend sym =>
sym
-> (a -> SEval sym a)
-> Nat'
-> SeqMap sym a
-> SEval sym (SeqMap sym a)
mapSeqMap sym
sym (TValue -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
a) (Integer -> Nat'
Nat Integer
w) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"ringUnary" GenValue sym
v)
TVStream TValue
a ->
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
-> (a -> SEval sym a)
-> Nat'
-> SeqMap sym a
-> SEval sym (SeqMap sym a)
mapSeqMap sym
sym (TValue -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
a) Nat'
Inf forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"ringUnary" GenValue sym
v)
TVFun TValue
_ TValue
ety ->
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)
y -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' TValue
ety (forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym GenValue sym
v SEval sym (GenValue sym)
y)
TVTuple [TValue]
tys ->
do [SEval sym (GenValue sym)]
as <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym) (forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
v)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' [TValue]
tys [SEval sym (GenValue sym)]
as)
TVRec RecordMap Ident TValue
fs ->
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
forall (t :: * -> *) a b c.
Applicative t =>
(a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
traverseRecordMap
(\Ident
f TValue
fty -> forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' TValue
fty (forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
f GenValue sym
v)))
RecordMap Ident TValue
fs
TVAbstract {} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringUnary" [String
"Abstract type not in `Ring`"]
TVNewtype {} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringUnary" [String
"Newtype not in `Ring`"]
{-# SPECIALIZE ringNullary ::
Concrete ->
(Integer -> SEval Concrete (SWord Concrete)) ->
SEval Concrete (SInteger Concrete) ->
(Integer -> SEval Concrete (SInteger Concrete)) ->
SEval Concrete (SRational Concrete) ->
(Integer -> Integer -> SEval Concrete (SFloat Concrete)) ->
TValue ->
SEval Concrete (GenValue Concrete)
#-}
ringNullary :: forall sym.
Backend sym =>
sym ->
(Integer -> SEval sym (SWord sym)) ->
SEval sym (SInteger sym) ->
(Integer -> SEval sym (SInteger sym)) ->
SEval sym (SRational sym) ->
(Integer -> Integer -> SEval sym (SFloat sym)) ->
TValue ->
SEval sym (GenValue sym)
ringNullary :: forall sym.
Backend sym =>
sym
-> (Integer -> SEval sym (SWord sym))
-> SEval sym (SInteger sym)
-> (Integer -> SEval sym (SInteger sym))
-> SEval sym (SRational sym)
-> (Integer -> Integer -> SEval sym (SFloat sym))
-> TValue
-> SEval sym (GenValue sym)
ringNullary sym
sym Integer -> SEval sym (SWord sym)
opw SEval sym (SInteger sym)
opi Integer -> SEval sym (SInteger sym)
opz SEval sym (SRational sym)
opq Integer -> Integer -> SEval sym (SFloat sym)
opfp = TValue -> SEval sym (GenValue sym)
loop
where
loop :: TValue -> SEval sym (GenValue sym)
loop :: TValue -> SEval sym (GenValue sym)
loop TValue
ty =
case TValue
ty of
TValue
TVBit -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringNullary" [String
"Bit not in class Ring"]
TValue
TVInteger -> forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SInteger sym)
opi
TVIntMod Integer
n -> forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> SEval sym (SInteger sym)
opz Integer
n
TVFloat Integer
e Integer
p -> forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Integer -> SEval sym (SFloat sym)
opfp Integer
e Integer
p
TValue
TVRational -> forall sym. SRational sym -> GenValue sym
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SRational sym)
opq
TVArray{} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"arithNullary" [String
"Array not in class Ring"]
TVSeq Integer
w TValue
a
| TValue -> Bool
isTBit TValue
a ->
do CallStack
stk <- forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w 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 a.
Backend sym =>
sym -> CallStack -> SEval sym a -> SEval sym a
sWithCallStack sym
sym CallStack
stk (Integer -> SEval sym (SWord sym)
opw Integer
w)
| Bool
otherwise ->
do SEval sym (GenValue sym)
v <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (TValue -> SEval sym (GenValue sym)
loop TValue
a)
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
w forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
_i -> SEval sym (GenValue sym)
v
TVStream TValue
a ->
do SEval sym (GenValue sym)
v <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (TValue -> SEval sym (GenValue sym)
loop TValue
a)
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 forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
_i -> SEval sym (GenValue sym)
v
TVFun TValue
_ TValue
b ->
do SEval sym (GenValue sym)
v <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (TValue -> SEval sym (GenValue sym)
loop TValue
b)
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
const SEval sym (GenValue sym)
v)
TVTuple [TValue]
tys ->
do [SEval sym (GenValue sym)]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. TValue -> SEval sym (GenValue sym)
loop) [TValue]
tys
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 [SEval sym (GenValue sym)]
xs
TVRec RecordMap Ident TValue
fs ->
do RecordMap Ident (SEval sym (GenValue sym))
xs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. TValue -> SEval sym (GenValue sym)
loop) RecordMap Ident TValue
fs
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord RecordMap Ident (SEval sym (GenValue sym))
xs
TVAbstract {} ->
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringNullary" [String
"Abstract type not in `Ring`"]
TVNewtype {} ->
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"ringNullary" [String
"Newtype not in `Ring`"]
{-# SPECIALIZE integralBinary :: Concrete -> BinWord Concrete ->
(SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
Binary Concrete
#-}
integralBinary :: forall sym.
Backend sym =>
sym ->
BinWord sym ->
(SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
Binary sym
integralBinary :: forall sym.
Backend sym =>
sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> Binary sym
integralBinary sym
sym BinWord sym
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi TValue
ty GenValue sym
l GenValue sym
r = case TValue
ty of
TValue
TVInteger ->
forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi (forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
l) (forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
r)
TVSeq Integer
w TValue
a
| TValue -> Bool
isTBit TValue
a ->
do SWord sym
wl <- forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"integralBinary left" GenValue sym
l
SWord sym
wr <- forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"integralBinary right" GenValue sym
r
CallStack
stk <- forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w 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 a.
Backend sym =>
sym -> CallStack -> SEval sym a -> SEval sym a
sWithCallStack sym
sym CallStack
stk (BinWord sym
opw Integer
w SWord sym
wl SWord sym
wr)
TValue
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"integralBinary" [forall a. Show a => a -> String
show TValue
ty forall a. [a] -> [a] -> [a]
++ String
" not int class `Integral`"]
{-# SPECIALIZE fromIntegerV :: Concrete -> Prim Concrete
#-}
fromIntegerV :: Backend sym => sym -> Prim sym
fromIntegerV :: forall sym. Backend sym => sym -> Prim sym
fromIntegerV sym
sym =
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
a ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
v ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do SInteger sym
i <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
v
forall sym.
Backend sym =>
sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
intV sym
sym SInteger sym
i TValue
a
{-# INLINE addV #-}
addV :: Backend sym => sym -> Binary sym
addV :: forall sym. Backend sym => sym -> Binary sym
addV sym
sym = forall sym.
Backend sym =>
sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (Integer
-> SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym))
-> Binary sym
ringBinary sym
sym forall {p}. p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz SRational sym -> SRational sym -> SEval sym (SRational sym)
opq SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp
where
opw :: p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw p
_w SWord sym
x SWord sym
y = forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordPlus sym
sym SWord sym
x SWord sym
y
opi :: SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi SInteger sym
x SInteger sym
y = forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intPlus sym
sym SInteger sym
x SInteger sym
y
opz :: Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz Integer
m SInteger sym
x SInteger sym
y = forall sym.
Backend sym =>
sym
-> Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
znPlus sym
sym Integer
m SInteger sym
x SInteger sym
y
opq :: SRational sym -> SRational sym -> SEval sym (SRational sym)
opq SRational sym
x SRational sym
y = forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalAdd sym
sym SRational sym
x SRational sym
y
opfp :: SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp SFloat sym
x SFloat sym
y = forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndMode sym
sym forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> forall sym. Backend sym => FPArith2 sym
fpPlus sym
sym SWord sym
r SFloat sym
x SFloat sym
y
{-# INLINE subV #-}
subV :: Backend sym => sym -> Binary sym
subV :: forall sym. Backend sym => sym -> Binary sym
subV sym
sym = forall sym.
Backend sym =>
sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (Integer
-> SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym))
-> Binary sym
ringBinary sym
sym forall {p}. p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz SRational sym -> SRational sym -> SEval sym (SRational sym)
opq SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp
where
opw :: p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw p
_w SWord sym
x SWord sym
y = forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordMinus sym
sym SWord sym
x SWord sym
y
opi :: SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi SInteger sym
x SInteger sym
y = forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMinus sym
sym SInteger sym
x SInteger sym
y
opz :: Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz Integer
m SInteger sym
x SInteger sym
y = forall sym.
Backend sym =>
sym
-> Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
znMinus sym
sym Integer
m SInteger sym
x SInteger sym
y
opq :: SRational sym -> SRational sym -> SEval sym (SRational sym)
opq SRational sym
x SRational sym
y = forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalSub sym
sym SRational sym
x SRational sym
y
opfp :: SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp SFloat sym
x SFloat sym
y = forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndMode sym
sym forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> forall sym. Backend sym => FPArith2 sym
fpMinus sym
sym SWord sym
r SFloat sym
x SFloat sym
y
{-# INLINE negateV #-}
negateV :: Backend sym => sym -> Unary sym
negateV :: forall sym. Backend sym => sym -> Unary sym
negateV sym
sym = forall sym.
Backend sym =>
sym
-> UnaryWord sym
-> (SInteger sym -> SEval sym (SInteger sym))
-> (Integer -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SEval sym (SFloat sym))
-> Unary sym
ringUnary sym
sym forall {p}. p -> SWord sym -> SEval sym (SWord sym)
opw SInteger sym -> SEval sym (SInteger sym)
opi Integer -> SInteger sym -> SEval sym (SInteger sym)
opz SRational sym -> SEval sym (SRational sym)
opq SFloat sym -> SEval sym (SFloat sym)
opfp
where
opw :: p -> SWord sym -> SEval sym (SWord sym)
opw p
_w SWord sym
x = forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SWord sym)
wordNegate sym
sym SWord sym
x
opi :: SInteger sym -> SEval sym (SInteger sym)
opi SInteger sym
x = forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SInteger sym)
intNegate sym
sym SInteger sym
x
opz :: Integer -> SInteger sym -> SEval sym (SInteger sym)
opz Integer
m SInteger sym
x = forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
znNegate sym
sym Integer
m SInteger sym
x
opq :: SRational sym -> SEval sym (SRational sym)
opq SRational sym
x = forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SRational sym)
rationalNegate sym
sym SRational sym
x
opfp :: SFloat sym -> SEval sym (SFloat sym)
opfp SFloat sym
x = forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SFloat sym)
fpNeg sym
sym SFloat sym
x
{-# INLINE mulV #-}
mulV :: Backend sym => sym -> Binary sym
mulV :: forall sym. Backend sym => sym -> Binary sym
mulV sym
sym = forall sym.
Backend sym =>
sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (Integer
-> SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> (SRational sym -> SRational sym -> SEval sym (SRational sym))
-> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym))
-> Binary sym
ringBinary sym
sym forall {p}. p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz SRational sym -> SRational sym -> SEval sym (SRational sym)
opq SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp
where
opw :: p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw p
_w SWord sym
x SWord sym
y = forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordMult sym
sym SWord sym
x SWord sym
y
opi :: SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi SInteger sym
x SInteger sym
y = forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMult sym
sym SInteger sym
x SInteger sym
y
opz :: Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opz Integer
m SInteger sym
x SInteger sym
y = forall sym.
Backend sym =>
sym
-> Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
znMult sym
sym Integer
m SInteger sym
x SInteger sym
y
opq :: SRational sym -> SRational sym -> SEval sym (SRational sym)
opq SRational sym
x SRational sym
y = forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalMul sym
sym SRational sym
x SRational sym
y
opfp :: SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
opfp SFloat sym
x SFloat sym
y = forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndMode sym
sym forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> forall sym. Backend sym => FPArith2 sym
fpMult sym
sym SWord sym
r SFloat sym
x SFloat sym
y
{-# INLINE divV #-}
divV :: Backend sym => sym -> Binary sym
divV :: forall sym. Backend sym => sym -> Binary sym
divV sym
sym = forall sym.
Backend sym =>
sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> Binary sym
integralBinary sym
sym forall {p}. p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi
where
opw :: p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw p
_w SWord sym
x SWord sym
y = forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordDiv sym
sym SWord sym
x SWord sym
y
opi :: SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi SInteger sym
x SInteger sym
y = forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intDiv sym
sym SInteger sym
x SInteger sym
y
{-# SPECIALIZE expV :: Concrete -> Prim Concrete #-}
expV :: Backend sym => sym -> Prim sym
expV :: forall sym. Backend sym => sym -> Prim sym
expV sym
sym =
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
aty ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ety ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
am ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
em ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do GenValue sym
a <- SEval sym (GenValue sym)
am
GenValue sym
e <- SEval sym (GenValue sym)
em
case TValue
ety of
TValue
TVInteger ->
let ei :: SInteger sym
ei = forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
e in
case forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
ei of
Just Integer
n
| Integer
n forall a. Eq a => a -> a -> Bool
== Integer
0 ->
do SInteger sym
onei <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
1
forall sym.
Backend sym =>
sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
intV sym
sym SInteger sym
onei TValue
aty
| Integer
n forall a. Ord a => a -> a -> Bool
> Integer
0 ->
do (Integer
_,[SBit sym]
ebits) <- forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (Integer, [SBit sym])
enumerateIntBits' sym
sym Integer
n SInteger sym
ei
forall sym.
Backend sym =>
sym
-> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
computeExponent sym
sym TValue
aty GenValue sym
a [SBit sym]
ebits
| Bool
otherwise -> forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError sym
sym EvalError
NegativeExponent
Maybe Integer
Nothing -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a e. Exception e => e -> a
X.throw (String -> Unsupported
UnsupportedSymbolicOp String
"integer exponentiation"))
TVSeq Integer
_w TValue
el | TValue -> Bool
isTBit TValue
el ->
do [SBit sym]
ebits <- forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValue sym
sym (forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"(^^)" GenValue sym
e)
forall sym.
Backend sym =>
sym
-> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
computeExponent sym
sym TValue
aty GenValue sym
a [SBit sym]
ebits
TValue
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"expV" [forall a. Show a => a -> String
show TValue
ety forall a. [a] -> [a] -> [a]
++ String
" not int class `Integral`"]
{-# SPECIALIZE computeExponent ::
Concrete -> TValue -> GenValue Concrete -> [SBit Concrete] -> SEval Concrete (GenValue Concrete)
#-}
computeExponent :: Backend sym =>
sym -> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
computeExponent :: forall sym.
Backend sym =>
sym
-> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
computeExponent sym
sym TValue
aty GenValue sym
a [SBit sym]
bs0 =
do SInteger sym
onei <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
1
GenValue sym
one <- forall sym.
Backend sym =>
sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
intV sym
sym SInteger sym
onei TValue
aty
GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
loop GenValue sym
one ([SBit sym] -> [SBit sym]
dropLeadingZeros [SBit sym]
bs0)
where
dropLeadingZeros :: [SBit sym] -> [SBit sym]
dropLeadingZeros [] = []
dropLeadingZeros (SBit sym
b:[SBit sym]
bs)
| Just Bool
False <- forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b = [SBit sym] -> [SBit sym]
dropLeadingZeros [SBit sym]
bs
| Bool
otherwise = (SBit sym
bforall a. a -> [a] -> [a]
:[SBit sym]
bs)
loop :: GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
loop GenValue sym
acc [] = forall (m :: * -> *) a. Monad m => a -> m a
return GenValue sym
acc
loop GenValue sym
acc (SBit sym
b:[SBit sym]
bs) =
do GenValue sym
sq <- forall sym. Backend sym => sym -> Binary sym
mulV sym
sym TValue
aty GenValue sym
acc GenValue sym
acc
GenValue sym
acc' <- 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
(forall sym. Backend sym => sym -> Binary sym
mulV sym
sym TValue
aty GenValue sym
a GenValue sym
sq)
(forall (f :: * -> *) a. Applicative f => a -> f a
pure GenValue sym
sq)
GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
loop GenValue sym
acc' [SBit sym]
bs
{-# INLINE modV #-}
modV :: Backend sym => sym -> Binary sym
modV :: forall sym. Backend sym => sym -> Binary sym
modV sym
sym = forall sym.
Backend sym =>
sym
-> BinWord sym
-> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym))
-> Binary sym
integralBinary sym
sym forall {p}. p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi
where
opw :: p -> SWord sym -> SWord sym -> SEval sym (SWord sym)
opw p
_w SWord sym
x SWord sym
y = forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordMod sym
sym SWord sym
x SWord sym
y
opi :: SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
opi SInteger sym
x SInteger sym
y = forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMod sym
sym SInteger sym
x SInteger sym
y
{-# SPECIALIZE toIntegerV :: Concrete -> Prim Concrete #-}
toIntegerV :: Backend sym => sym -> Prim sym
toIntegerV :: forall sym. Backend sym => sym -> Prim sym
toIntegerV sym
sym =
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
a ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
v ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
case TValue
a of
TVSeq Integer
_w TValue
el | TValue -> Bool
isTBit TValue
el ->
forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SInteger sym)
wordToInt sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"toInteger" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
v))
TValue
TVInteger -> SEval sym (GenValue sym)
v
TValue
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"toInteger" [forall a. Show a => a -> String
show TValue
a forall a. [a] -> [a] -> [a]
++ String
" not in class `Integral`"]
{-# SPECIALIZE recipV :: Concrete -> Prim Concrete #-}
recipV :: Backend sym => sym -> Prim sym
recipV :: forall sym. Backend sym => sym -> Prim sym
recipV sym
sym =
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
a ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
case TValue
a of
TValue
TVRational -> forall sym. SRational sym -> GenValue sym
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SRational sym)
rationalRecip sym
sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. GenValue sym -> SRational sym
fromVRational forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
x)
TVFloat Integer
e Integer
p ->
do SFloat sym
one <- forall sym.
Backend sym =>
sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
fpLit sym
sym Integer
e Integer
p Rational
1
SWord sym
r <- forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndMode sym
sym
SFloat sym
xv <- forall sym. GenValue sym -> SFloat sym
fromVFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
x
forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. Backend sym => FPArith2 sym
fpDiv sym
sym SWord sym
r SFloat sym
one SFloat sym
xv
TVIntMod Integer
m -> forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
znRecip sym
sym Integer
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. GenValue sym -> SInteger sym
fromVInteger forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
x)
TValue
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"recip" [forall a. Show a => a -> String
show TValue
a forall a. [a] -> [a] -> [a]
++ String
"is not a Field"]
{-# SPECIALIZE fieldDivideV :: Concrete -> Prim Concrete #-}
fieldDivideV :: Backend sym => sym -> Prim sym
fieldDivideV :: forall sym. Backend sym => sym -> Prim sym
fieldDivideV sym
sym =
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
a ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
x ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
y ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
case TValue
a of
TValue
TVRational ->
do SRational sym
x' <- forall sym. GenValue sym -> SRational sym
fromVRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
x
SRational sym
y' <- forall sym. GenValue sym -> SRational sym
fromVRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
y
forall sym. SRational sym -> GenValue sym
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
rationalDivide sym
sym SRational sym
x' SRational sym
y'
TVFloat Integer
_e Integer
_p ->
do SFloat sym
xv <- forall sym. GenValue sym -> SFloat sym
fromVFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
x
SFloat sym
yv <- forall sym. GenValue sym -> SFloat sym
fromVFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
y
SWord sym
r <- forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndMode sym
sym
forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. Backend sym => FPArith2 sym
fpDiv sym
sym SWord sym
r SFloat sym
xv SFloat sym
yv
TVIntMod Integer
m ->
do SInteger sym
x' <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
x
SInteger sym
y' <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
y
SInteger sym
yinv <- forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
znRecip sym
sym Integer
m SInteger sym
y'
forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
znMult sym
sym Integer
m SInteger sym
x' SInteger sym
yinv
TValue
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"recip" [forall a. Show a => a -> String
show TValue
a forall a. [a] -> [a] -> [a]
++ String
"is not a Field"]
{-# SPECIALIZE roundOp ::
Concrete ->
String ->
(SRational Concrete -> SEval Concrete (SInteger Concrete)) ->
(SFloat Concrete -> SEval Concrete (SInteger Concrete)) ->
Unary Concrete #-}
roundOp ::
Backend sym =>
sym ->
String ->
(SRational sym -> SEval sym (SInteger sym)) ->
(SFloat sym -> SEval sym (SInteger sym)) ->
Unary sym
roundOp :: forall sym.
Backend sym =>
sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
roundOp sym
_sym String
nm SRational sym -> SEval sym (SInteger sym)
qop SFloat sym -> SEval sym (SInteger sym)
opfp TValue
ty GenValue sym
v =
case TValue
ty of
TValue
TVRational -> forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SRational sym -> SEval sym (SInteger sym)
qop (forall sym. GenValue sym -> SRational sym
fromVRational GenValue sym
v))
TVFloat Integer
_ Integer
_ -> forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SFloat sym -> SEval sym (SInteger sym)
opfp (forall sym. GenValue sym -> SFloat sym
fromVFloat GenValue sym
v)
TValue
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
nm [forall a. Show a => a -> String
show TValue
ty forall a. [a] -> [a] -> [a]
++ String
" is not a Field"]
{-# INLINE floorV #-}
floorV :: Backend sym => sym -> Unary sym
floorV :: forall sym. Backend sym => sym -> Unary sym
floorV sym
sym = forall sym.
Backend sym =>
sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
roundOp sym
sym String
"floor" SRational sym -> SEval sym (SInteger sym)
opq SFloat sym -> SEval sym (SInteger sym)
opfp
where
opq :: SRational sym -> SEval sym (SInteger sym)
opq = forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalFloor sym
sym
opfp :: SFloat sym -> SEval sym (SInteger sym)
opfp = \SFloat sym
x -> forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRTN sym
sym forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> forall sym.
Backend sym =>
sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpToInteger sym
sym String
"floor" SWord sym
r SFloat sym
x
{-# INLINE ceilingV #-}
ceilingV :: Backend sym => sym -> Unary sym
ceilingV :: forall sym. Backend sym => sym -> Unary sym
ceilingV sym
sym = forall sym.
Backend sym =>
sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
roundOp sym
sym String
"ceiling" SRational sym -> SEval sym (SInteger sym)
opq SFloat sym -> SEval sym (SInteger sym)
opfp
where
opq :: SRational sym -> SEval sym (SInteger sym)
opq = forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalCeiling sym
sym
opfp :: SFloat sym -> SEval sym (SInteger sym)
opfp = \SFloat sym
x -> forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRTP sym
sym forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> forall sym.
Backend sym =>
sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpToInteger sym
sym String
"ceiling" SWord sym
r SFloat sym
x
{-# INLINE truncV #-}
truncV :: Backend sym => sym -> Unary sym
truncV :: forall sym. Backend sym => sym -> Unary sym
truncV sym
sym = forall sym.
Backend sym =>
sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
roundOp sym
sym String
"trunc" SRational sym -> SEval sym (SInteger sym)
opq SFloat sym -> SEval sym (SInteger sym)
opfp
where
opq :: SRational sym -> SEval sym (SInteger sym)
opq = forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalTrunc sym
sym
opfp :: SFloat sym -> SEval sym (SInteger sym)
opfp = \SFloat sym
x -> forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRTZ sym
sym forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> forall sym.
Backend sym =>
sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpToInteger sym
sym String
"trunc" SWord sym
r SFloat sym
x
{-# INLINE roundAwayV #-}
roundAwayV :: Backend sym => sym -> Unary sym
roundAwayV :: forall sym. Backend sym => sym -> Unary sym
roundAwayV sym
sym = forall sym.
Backend sym =>
sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
roundOp sym
sym String
"roundAway" SRational sym -> SEval sym (SInteger sym)
opq SFloat sym -> SEval sym (SInteger sym)
opfp
where
opq :: SRational sym -> SEval sym (SInteger sym)
opq = forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalRoundAway sym
sym
opfp :: SFloat sym -> SEval sym (SInteger sym)
opfp = \SFloat sym
x -> forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRNA sym
sym forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> forall sym.
Backend sym =>
sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpToInteger sym
sym String
"roundAway" SWord sym
r SFloat sym
x
{-# INLINE roundToEvenV #-}
roundToEvenV :: Backend sym => sym -> Unary sym
roundToEvenV :: forall sym. Backend sym => sym -> Unary sym
roundToEvenV sym
sym = forall sym.
Backend sym =>
sym
-> String
-> (SRational sym -> SEval sym (SInteger sym))
-> (SFloat sym -> SEval sym (SInteger sym))
-> Unary sym
roundOp sym
sym String
"roundToEven" SRational sym -> SEval sym (SInteger sym)
opq SFloat sym -> SEval sym (SInteger sym)
opfp
where
opq :: SRational sym -> SEval sym (SInteger sym)
opq = forall sym.
Backend sym =>
sym -> SRational sym -> SEval sym (SInteger sym)
rationalRoundToEven sym
sym
opfp :: SFloat sym -> SEval sym (SInteger sym)
opfp = \SFloat sym
x -> forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRNE sym
sym forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SWord sym
r -> forall sym.
Backend sym =>
sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpToInteger sym
sym String
"roundToEven" SWord sym
r SFloat sym
x
{-# INLINE andV #-}
andV :: Backend sym => sym -> Binary sym
andV :: forall sym. Backend sym => sym -> Binary sym
andV sym
sym = forall sym.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> Binary sym
logicBinary sym
sym (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitAnd sym
sym) (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordAnd sym
sym)
{-# INLINE orV #-}
orV :: Backend sym => sym -> Binary sym
orV :: forall sym. Backend sym => sym -> Binary sym
orV sym
sym = forall sym.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> Binary sym
logicBinary sym
sym (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitOr sym
sym) (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordOr sym
sym)
{-# INLINE xorV #-}
xorV :: Backend sym => sym -> Binary sym
xorV :: forall sym. Backend sym => sym -> Binary sym
xorV sym
sym = forall sym.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> Binary sym
logicBinary sym
sym (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitXor sym
sym) (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordXor sym
sym)
{-# INLINE complementV #-}
complementV :: Backend sym => sym -> Unary sym
complementV :: forall sym. Backend sym => sym -> Unary sym
complementV sym
sym = forall sym.
Backend sym =>
sym
-> (SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SEval sym (SWord sym))
-> Unary sym
logicUnary sym
sym (forall sym. Backend sym => sym -> SBit sym -> SEval sym (SBit sym)
bitComplement sym
sym) (forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SWord sym)
wordComplement sym
sym)
{-# INLINE lg2V #-}
lg2V :: Backend sym => sym -> Prim sym
lg2V :: forall sym. Backend sym => sym -> Prim sym
lg2V sym
sym =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
w ->
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord sym
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w 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 -> SWord sym -> SEval sym (SWord sym)
wordLg2 sym
sym SWord sym
x)
{-# SPECIALIZE sdivV :: Concrete -> Prim Concrete #-}
sdivV :: Backend sym => sym -> Prim sym
sdivV :: forall sym. Backend sym => sym -> Prim sym
sdivV sym
sym =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
w ->
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord sym
x ->
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord sym
y ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w 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 -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordSignedDiv sym
sym SWord sym
x SWord sym
y)
{-# SPECIALIZE smodV :: Concrete -> Prim Concrete #-}
smodV :: Backend sym => sym -> Prim sym
smodV :: forall sym. Backend sym => sym -> Prim sym
smodV sym
sym =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
w ->
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord sym
x ->
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord sym
y ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w 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 -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordSignedMod sym
sym SWord sym
x SWord sym
y)
{-# SPECIALIZE toSignedIntegerV :: Concrete -> Prim Concrete #-}
toSignedIntegerV :: Backend sym => sym -> Prim sym
toSignedIntegerV :: forall sym. Backend sym => sym -> Prim sym
toSignedIntegerV sym
sym =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_w ->
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord sym
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SInteger sym)
wordToSignedInt sym
sym SWord sym
x)
{-# SPECIALIZE cmpValue ::
Concrete ->
(SBit Concrete -> SBit Concrete -> SEval Concrete a -> SEval Concrete a) ->
(SWord Concrete -> SWord Concrete -> SEval Concrete a -> SEval Concrete a) ->
(SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->
(Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->
(SRational Concrete -> SRational Concrete -> SEval Concrete a -> SEval Concrete a) ->
(SFloat Concrete -> SFloat Concrete -> SEval Concrete a -> SEval Concrete a) ->
(TValue -> GenValue Concrete -> GenValue Concrete -> SEval Concrete a -> SEval Concrete a)
#-}
cmpValue ::
Backend sym =>
sym ->
(SBit sym -> SBit sym -> SEval sym a -> SEval sym a) ->
(SWord sym -> SWord sym -> SEval sym a -> SEval sym a) ->
(SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->
(Integer -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->
(SRational sym -> SRational sym -> SEval sym a -> SEval sym a) ->
(SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a) ->
(TValue -> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a)
cmpValue :: forall sym a.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym a -> SEval sym a)
-> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a)
-> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (Integer
-> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a)
-> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a)
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym a
-> SEval sym a
cmpValue sym
sym SBit sym -> SBit sym -> SEval sym a -> SEval sym a
fb SWord sym -> SWord sym -> SEval sym a -> SEval sym a
fw SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a
fi Integer
-> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a
fz SRational sym -> SRational sym -> SEval sym a -> SEval sym a
fq SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a
ff = TValue
-> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a
cmp
where
cmp :: TValue
-> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a
cmp TValue
ty GenValue sym
v1 GenValue sym
v2 SEval sym a
k =
case TValue
ty of
TValue
TVBit -> SBit sym -> SBit sym -> SEval sym a -> SEval sym a
fb (forall sym. GenValue sym -> SBit sym
fromVBit GenValue sym
v1) (forall sym. GenValue sym -> SBit sym
fromVBit GenValue sym
v2) SEval sym a
k
TValue
TVInteger -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a
fi (forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
v1) (forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
v2) SEval sym a
k
TVFloat Integer
_ Integer
_ -> SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a
ff (forall sym. GenValue sym -> SFloat sym
fromVFloat GenValue sym
v1) (forall sym. GenValue sym -> SFloat sym
fromVFloat GenValue sym
v2) SEval sym a
k
TVIntMod Integer
n -> Integer
-> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a
fz Integer
n (forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
v1) (forall sym. GenValue sym -> SInteger sym
fromVInteger GenValue sym
v2) SEval sym a
k
TValue
TVRational -> SRational sym -> SRational sym -> SEval sym a -> SEval sym a
fq (forall sym. GenValue sym -> SRational sym
fromVRational GenValue sym
v1) (forall sym. GenValue sym -> SRational sym
fromVRational GenValue sym
v2) SEval sym a
k
TVArray{} -> forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Prims.Value.cmpValue"
[ String
"Arrays are not comparable" ]
TVSeq Integer
n TValue
t
| TValue -> Bool
isTBit TValue
t -> do SWord sym
w1 <- forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"cmpValue" GenValue sym
v1
SWord sym
w2 <- forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
"cmpValue" GenValue sym
v2
SWord sym -> SWord sym -> SEval sym a -> SEval sym a
fw SWord sym
w1 SWord sym
w2 SEval sym a
k
| Bool
otherwise -> [TValue]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
-> SEval sym a
-> SEval sym a
cmpValues (forall a. a -> [a]
repeat TValue
t)
(forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n (forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq GenValue sym
v1))
(forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n (forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq GenValue sym
v2))
SEval sym a
k
TVStream TValue
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Prims.Value.cmpValue"
[ String
"Infinite streams are not comparable" ]
TVFun TValue
_ TValue
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Prims.Value.cmpValue"
[ String
"Functions are not comparable" ]
TVTuple [TValue]
tys -> [TValue]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
-> SEval sym a
-> SEval sym a
cmpValues [TValue]
tys (forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
v1) (forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
v2) SEval sym a
k
TVRec RecordMap Ident TValue
fields -> [TValue]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
-> SEval sym a
-> SEval sym a
cmpValues
(forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident TValue
fields)
(forall a b. RecordMap a b -> [b]
recordElements (forall sym.
GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
fromVRecord GenValue sym
v1))
(forall a b. RecordMap a b -> [b]
recordElements (forall sym.
GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
fromVRecord GenValue sym
v2))
SEval sym a
k
TVAbstract {} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"cmpValue"
[ String
"Abstract type not in `Cmp`" ]
TVNewtype {} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"cmpValue"
[ String
"Newtype not in `Cmp`" ]
cmpValues :: [TValue]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
-> SEval sym a
-> SEval sym a
cmpValues (TValue
t : [TValue]
ts) (SEval sym (GenValue sym)
x1 : [SEval sym (GenValue sym)]
xs1) (SEval sym (GenValue sym)
x2 : [SEval sym (GenValue sym)]
xs2) SEval sym a
k =
do GenValue sym
x1' <- SEval sym (GenValue sym)
x1
GenValue sym
x2' <- SEval sym (GenValue sym)
x2
TValue
-> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a
cmp TValue
t GenValue sym
x1' GenValue sym
x2' ([TValue]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
-> SEval sym a
-> SEval sym a
cmpValues [TValue]
ts [SEval sym (GenValue sym)]
xs1 [SEval sym (GenValue sym)]
xs2 SEval sym a
k)
cmpValues [TValue]
_ [SEval sym (GenValue sym)]
_ [SEval sym (GenValue sym)]
_ SEval sym a
k = SEval sym a
k
{-# INLINE bitLessThan #-}
bitLessThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitLessThan :: forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitLessThan sym
sym SBit sym
x SBit sym
y =
do SBit sym
xnot <- forall sym. Backend sym => sym -> SBit sym -> SEval sym (SBit sym)
bitComplement sym
sym SBit sym
x
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitAnd sym
sym SBit sym
xnot SBit sym
y
{-# INLINE bitGreaterThan #-}
bitGreaterThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitGreaterThan :: forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitGreaterThan sym
sym SBit sym
x SBit sym
y = forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitLessThan sym
sym SBit sym
y SBit sym
x
{-# INLINE valEq #-}
valEq :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
valEq :: forall sym.
Backend sym =>
sym
-> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
valEq sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = forall sym a.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym a -> SEval sym a)
-> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a)
-> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (Integer
-> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a)
-> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a)
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym a
-> SEval sym a
cmpValue sym
sym SBit sym
-> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fb SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SInteger sym
-> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fi Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
fz SRational sym
-> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fq SFloat sym
-> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
ff TValue
ty GenValue sym
v1 GenValue sym
v2 (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
True)
where
fb :: SBit sym
-> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fb SBit sym
x SBit sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitEq sym
sym SBit sym
x SBit sym
y) SEval sym (SBit sym)
k
fw :: SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SWord sym
x SWord sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordEq sym
sym SWord sym
x SWord sym
y) SEval sym (SBit sym)
k
fi :: SInteger sym
-> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fi SInteger sym
x SInteger sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym (forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq sym
sym SInteger sym
x SInteger sym
y) SEval sym (SBit sym)
k
fz :: Integer
-> SInteger sym
-> SInteger sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
fz Integer
m SInteger sym
x SInteger sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym (forall sym.
Backend sym =>
sym
-> Integer -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
znEq sym
sym Integer
m SInteger sym
x SInteger sym
y) SEval sym (SBit sym)
k
fq :: SRational sym
-> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fq SRational sym
x SRational sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym (forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalEq sym
sym SRational sym
x SRational sym
y) SEval sym (SBit sym)
k
ff :: SFloat sym
-> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
ff SFloat sym
x SFloat sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym (forall sym.
Backend sym =>
sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpEq sym
sym SFloat sym
x SFloat sym
y) SEval sym (SBit sym)
k
{-# INLINE valLt #-}
valLt :: Backend sym =>
sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
valLt :: forall sym.
Backend sym =>
sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
valLt sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 SBit sym
final = forall sym a.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym a -> SEval sym a)
-> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a)
-> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (Integer
-> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a)
-> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a)
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym a
-> SEval sym a
cmpValue sym
sym SBit sym
-> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fb SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SInteger sym
-> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fi forall {p} {p} {p} {p} {a}. p -> p -> p -> p -> a
fz SRational sym
-> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fq SFloat sym
-> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
ff TValue
ty GenValue sym
v1 GenValue sym
v2 (forall (f :: * -> *) a. Applicative f => a -> f a
pure SBit sym
final)
where
fb :: SBit sym
-> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fb SBit sym
x SBit sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitLessThan sym
sym SBit sym
x SBit sym
y) (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitEq sym
sym SBit sym
x SBit sym
y) SEval sym (SBit sym)
k
fw :: SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SWord sym
x SWord sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordLessThan sym
sym SWord sym
x SWord sym
y) (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordEq sym
sym SWord sym
x SWord sym
y) SEval sym (SBit sym)
k
fi :: SInteger sym
-> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fi SInteger sym
x SInteger sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intLessThan sym
sym SInteger sym
x SInteger sym
y) (forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq sym
sym SInteger sym
x SInteger sym
y) SEval sym (SBit sym)
k
fz :: p -> p -> p -> p -> a
fz p
_ p
_ p
_ p
_ = forall a. HasCallStack => String -> [String] -> a
panic String
"valLt" [String
"Z_n is not in `Cmp`"]
fq :: SRational sym
-> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fq SRational sym
x SRational sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalLessThan sym
sym SRational sym
x SRational sym
y) (forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalEq sym
sym SRational sym
x SRational sym
y) SEval sym (SBit sym)
k
ff :: SFloat sym
-> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
ff SFloat sym
x SFloat sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (forall sym.
Backend sym =>
sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpLessThan sym
sym SFloat sym
x SFloat sym
y) (forall sym.
Backend sym =>
sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpEq sym
sym SFloat sym
x SFloat sym
y) SEval sym (SBit sym)
k
{-# INLINE valGt #-}
valGt :: Backend sym =>
sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
valGt :: forall sym.
Backend sym =>
sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
valGt sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 SBit sym
final = forall sym a.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym a -> SEval sym a)
-> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a)
-> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (Integer
-> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a)
-> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a)
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym a
-> SEval sym a
cmpValue sym
sym SBit sym
-> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fb SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SInteger sym
-> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fi forall {p} {p} {p} {p} {a}. p -> p -> p -> p -> a
fz SRational sym
-> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fq SFloat sym
-> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
ff TValue
ty GenValue sym
v1 GenValue sym
v2 (forall (f :: * -> *) a. Applicative f => a -> f a
pure SBit sym
final)
where
fb :: SBit sym
-> SBit sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fb SBit sym
x SBit sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitGreaterThan sym
sym SBit sym
x SBit sym
y) (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitEq sym
sym SBit sym
x SBit sym
y) SEval sym (SBit sym)
k
fw :: SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SWord sym
x SWord sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordGreaterThan sym
sym SWord sym
x SWord sym
y) (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordEq sym
sym SWord sym
x SWord sym
y) SEval sym (SBit sym)
k
fi :: SInteger sym
-> SInteger sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fi SInteger sym
x SInteger sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intGreaterThan sym
sym SInteger sym
x SInteger sym
y) (forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq sym
sym SInteger sym
x SInteger sym
y) SEval sym (SBit sym)
k
fz :: p -> p -> p -> p -> a
fz p
_ p
_ p
_ p
_ = forall a. HasCallStack => String -> [String] -> a
panic String
"valGt" [String
"Z_n is not in `Cmp`"]
fq :: SRational sym
-> SRational sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fq SRational sym
x SRational sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalGreaterThan sym
sym SRational sym
x SRational sym
y) (forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalEq sym
sym SRational sym
x SRational sym
y) SEval sym (SBit sym)
k
ff :: SFloat sym
-> SFloat sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
ff SFloat sym
x SFloat sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (forall sym.
Backend sym =>
sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpGreaterThan sym
sym SFloat sym
x SFloat sym
y) (forall sym.
Backend sym =>
sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpEq sym
sym SFloat sym
x SFloat sym
y) SEval sym (SBit sym)
k
{-# INLINE eqCombine #-}
eqCombine :: Backend sym =>
sym ->
SEval sym (SBit sym) ->
SEval sym (SBit sym) ->
SEval sym (SBit sym)
eqCombine :: forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
eqCombine sym
sym SEval sym (SBit sym)
eq SEval sym (SBit sym)
k = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitAnd sym
sym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SBit sym)
eq forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SEval sym (SBit sym)
k)
{-# INLINE lexCombine #-}
lexCombine :: Backend sym =>
sym ->
SEval sym (SBit sym) ->
SEval sym (SBit sym) ->
SEval sym (SBit sym) ->
SEval sym (SBit sym)
lexCombine :: forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym SEval sym (SBit sym)
cmp SEval sym (SBit sym)
eq SEval sym (SBit sym)
k =
do SBit sym
c <- SEval sym (SBit sym)
cmp
SBit sym
e <- SEval sym (SBit sym)
eq
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitOr sym
sym SBit sym
c forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitAnd sym
sym SBit sym
e forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (SBit sym)
k
{-# INLINE eqV #-}
eqV :: Backend sym => sym -> Binary sym
eqV :: forall sym. Backend sym => sym -> Binary sym
eqV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
valEq sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2
{-# INLINE distinctV #-}
distinctV :: Backend sym => sym -> Binary sym
distinctV :: forall sym. Backend sym => sym -> Binary sym
distinctV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = 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 -> SEval sym (SBit sym)
bitComplement sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym
-> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
valEq sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2)
{-# INLINE lessThanV #-}
lessThanV :: Backend sym => sym -> Binary sym
lessThanV :: forall sym. Backend sym => sym -> Binary sym
lessThanV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
valLt sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
False)
{-# INLINE lessThanEqV #-}
lessThanEqV :: Backend sym => sym -> Binary sym
lessThanEqV :: forall sym. Backend sym => sym -> Binary sym
lessThanEqV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
valLt sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
True)
{-# INLINE greaterThanV #-}
greaterThanV :: Backend sym => sym -> Binary sym
greaterThanV :: forall sym. Backend sym => sym -> Binary sym
greaterThanV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
valGt sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
False)
{-# INLINE greaterThanEqV #-}
greaterThanEqV :: Backend sym => sym -> Binary sym
greaterThanEqV :: forall sym. Backend sym => sym -> Binary sym
greaterThanEqV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> TValue
-> GenValue sym
-> GenValue sym
-> SBit sym
-> SEval sym (SBit sym)
valGt sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
True)
{-# INLINE signedLessThanV #-}
signedLessThanV :: Backend sym => sym -> Binary sym
signedLessThanV :: forall sym. Backend sym => sym -> Binary sym
signedLessThanV sym
sym TValue
ty GenValue sym
v1 GenValue sym
v2 = forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym a -> SEval sym a)
-> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a)
-> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (Integer
-> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a)
-> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a)
-> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a)
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym a
-> SEval sym a
cmpValue sym
sym forall {p} {p} {p} {a}. p -> p -> p -> a
fb SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw forall {p} {p} {p} {a}. p -> p -> p -> a
fi forall {a} {p} {p} {p} {a}. Show a => a -> p -> p -> p -> a
fz forall {p} {p} {p} {a}. p -> p -> p -> a
fq forall {p} {p} {p} {a}. p -> p -> p -> a
ff TValue
ty GenValue sym
v1 GenValue sym
v2 (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
False)
where
fb :: p -> p -> p -> a
fb p
_ p
_ p
_ = forall a. HasCallStack => String -> [String] -> a
panic String
"signedLessThan" [String
"Attempted to perform signed comparison on bit type"]
fw :: SWord sym
-> SWord sym -> SEval sym (SBit sym) -> SEval sym (SBit sym)
fw SWord sym
x SWord sym
y SEval sym (SBit sym)
k = forall sym.
Backend sym =>
sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
lexCombine sym
sym (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordSignedLessThan sym
sym SWord sym
x SWord sym
y) (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordEq sym
sym SWord sym
x SWord sym
y) SEval sym (SBit sym)
k
fi :: p -> p -> p -> a
fi p
_ p
_ p
_ = forall a. HasCallStack => String -> [String] -> a
panic String
"signedLessThan" [String
"Attempted to perform signed comparison on Integer type"]
fz :: a -> p -> p -> p -> a
fz a
m p
_ p
_ p
_ = forall a. HasCallStack => String -> [String] -> a
panic String
"signedLessThan" [String
"Attempted to perform signed comparison on Z_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
m forall a. [a] -> [a] -> [a]
++ String
" type"]
fq :: p -> p -> p -> a
fq p
_ p
_ p
_ = forall a. HasCallStack => String -> [String] -> a
panic String
"signedLessThan" [String
"Attempted to perform signed comparison on Rational type"]
ff :: p -> p -> p -> a
ff p
_ p
_ p
_ = forall a. HasCallStack => String -> [String] -> a
panic String
"signedLessThan" [String
"Attempted to perform signed comparison on Float"]
{-# SPECIALIZE zeroV ::
Concrete ->
TValue ->
SEval Concrete (GenValue Concrete)
#-}
zeroV :: forall sym.
Backend sym =>
sym ->
TValue ->
SEval sym (GenValue sym)
zeroV :: forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
ty = case TValue
ty of
TValue
TVBit ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. SBit sym -> GenValue sym
VBit (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
False))
TValue
TVInteger ->
forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
0
TVIntMod Integer
_ ->
forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
0
TValue
TVRational ->
forall sym. SRational sym -> GenValue sym
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SRational sym)
intToRational sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
0)
TVArray{} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"zeroV" [String
"Array not in class Zero"]
TVFloat Integer
e Integer
p ->
forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
fpLit sym
sym Integer
e Integer
p Rational
0
TVSeq Integer
w TValue
ety
| TValue -> Bool
isTBit TValue
ety -> forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (GenValue sym)
word sym
sym Integer
w Integer
0
| Bool
otherwise ->
do SEval sym (GenValue sym)
z <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
ety)
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
w (forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
_i -> SEval sym (GenValue sym)
z)
TVStream TValue
ety ->
do SEval sym (GenValue sym)
z <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
ety)
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 (forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
_i -> SEval sym (GenValue sym)
z)
TVFun TValue
_ TValue
bty ->
do SEval sym (GenValue sym)
z <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
bty)
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
const SEval sym (GenValue sym)
z)
TVTuple [TValue]
tys ->
do [SEval sym (GenValue sym)]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym) [TValue]
tys
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 [SEval sym (GenValue sym)]
xs
TVRec RecordMap Ident TValue
fields ->
do RecordMap Ident (SEval sym (GenValue sym))
xs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym) RecordMap Ident TValue
fields
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord RecordMap Ident (SEval sym (GenValue sym))
xs
TVAbstract {} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"zeroV" [ String
"Abstract type not in `Zero`" ]
TVNewtype {} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"zeroV" [ String
"Newtype not in `Zero`" ]
{-# SPECIALIZE joinSeq ::
Concrete ->
Nat' ->
Integer ->
TValue ->
SEval Concrete (SeqMap Concrete (GenValue Concrete)) ->
SEval Concrete (GenValue Concrete)
#-}
joinSeq ::
Backend sym =>
sym ->
Nat' ->
Integer ->
TValue ->
SEval sym (SeqMap sym (GenValue sym)) ->
SEval sym (GenValue sym)
joinSeq :: forall sym.
Backend sym =>
sym
-> Nat'
-> Integer
-> TValue
-> SEval sym (SeqMap sym (GenValue sym))
-> SEval sym (GenValue sym)
joinSeq sym
sym Nat'
_parts Integer
0 TValue
a SEval sym (SeqMap sym (GenValue sym))
_val
= forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym (Integer -> TValue -> TValue
TVSeq Integer
0 TValue
a)
joinSeq sym
sym (Nat Integer
parts) Integer
each TValue
TVBit SEval sym (SeqMap sym (GenValue sym))
val
= do WordValue sym
w <- forall sym.
Backend sym =>
sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym (Integer
partsforall a. Num a => a -> a -> a
*Integer
each)
(forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SeqMap sym (WordValue sym)
-> SEval sym (WordValue sym)
joinWords sym
sym Integer
parts Integer
each forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"joinV") forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (SeqMap sym (GenValue sym))
val)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. Integer -> WordValue sym -> GenValue sym
VWord (Integer
partsforall a. Num a => a -> a -> a
*Integer
each) WordValue sym
w)
joinSeq sym
sym Nat'
Inf Integer
each TValue
TVBit SEval sym (SeqMap sym (GenValue sym))
val
= forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
do let (Integer
q,Integer
r) = forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
each
SeqMap sym (GenValue sym)
xs <- SEval sym (SeqMap sym (GenValue sym))
val
WordValue sym
ys <- forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"join seq" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
xs Integer
q
forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym WordValue sym
ys Integer
r
joinSeq sym
_sym Nat'
parts Integer
each TValue
_a SEval sym (SeqMap sym (GenValue sym))
val
= forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
vSeq forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> do
let (Integer
q,Integer
r) = forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
each
SeqMap sym (GenValue sym)
xs <- SEval sym (SeqMap sym (GenValue sym))
val
SeqMap sym (GenValue sym)
ys <- forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"join seq" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
xs Integer
q
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
ys Integer
r
where
len :: Nat'
len = Nat'
parts Nat' -> Nat' -> Nat'
`nMul` (Integer -> Nat'
Nat Integer
each)
vSeq :: SeqMap sym (GenValue sym) -> GenValue sym
vSeq = case Nat'
len of
Nat'
Inf -> forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream
Nat Integer
n -> forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
n
{-# INLINE joinV #-}
joinV ::
Backend sym =>
sym ->
Nat' ->
Integer ->
TValue ->
SEval sym (GenValue sym) ->
SEval sym (GenValue sym)
joinV :: forall sym.
Backend sym =>
sym
-> Nat'
-> Integer
-> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
joinV sym
sym Nat'
parts Integer
each TValue
a SEval sym (GenValue sym)
val =
do SEval sym (SeqMap sym (GenValue sym))
xs <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"joinV" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val)
forall sym.
Backend sym =>
sym
-> Nat'
-> Integer
-> TValue
-> SEval sym (SeqMap sym (GenValue sym))
-> SEval sym (GenValue sym)
joinSeq sym
sym Nat'
parts Integer
each TValue
a SEval sym (SeqMap sym (GenValue sym))
xs
{-# INLINE takeV #-}
takeV ::
Backend sym =>
sym ->
Nat' ->
Nat' ->
TValue ->
SEval sym (GenValue sym) ->
SEval sym (GenValue sym)
takeV :: forall sym.
Backend sym =>
sym
-> Nat'
-> Nat'
-> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
takeV sym
sym Nat'
front Nat'
back TValue
a SEval sym (GenValue sym)
val =
case Nat'
front of
Nat'
Inf -> SEval sym (GenValue sym)
val
Nat Integer
front' ->
case Nat'
back of
Nat Integer
back' | TValue -> Bool
isTBit TValue
a ->
do WordValue sym
w <- forall sym.
Backend sym =>
sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym Integer
front' (forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
takeWordVal sym
sym Integer
front' Integer
back' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"takeV" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
val))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
front' WordValue sym
w)
Nat'
Inf | TValue -> Bool
isTBit TValue
a ->
do WordValue sym
w <- forall sym.
Backend sym =>
sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym Integer
front' (forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
front' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall sym. GenValue sym -> SBit sym
fromVBit forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"takeV" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
front' WordValue sym
w)
Nat'
_ ->
do SeqMap sym (GenValue sym)
xs <- forall sym a.
Backend sym =>
sym -> SEval sym (SeqMap sym a) -> SEval sym (SeqMap sym a)
delaySeqMap sym
sym (forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"takeV" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
front' SeqMap sym (GenValue sym)
xs)
{-# INLINE dropV #-}
dropV ::
Backend sym =>
sym ->
Integer ->
Nat' ->
TValue ->
SEval sym (GenValue sym) ->
SEval sym (GenValue sym)
dropV :: forall sym.
Backend sym =>
sym
-> Integer
-> Nat'
-> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
dropV sym
sym Integer
front Nat'
back TValue
a SEval sym (GenValue sym)
val =
case Nat'
back of
Nat Integer
back' | TValue -> Bool
isTBit TValue
a ->
do WordValue sym
w <- forall sym.
Backend sym =>
sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym Integer
back' (forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
dropWordVal sym
sym Integer
front Integer
back' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"dropV" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
val))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
back' WordValue sym
w)
Nat'
_ ->
do SeqMap sym (GenValue sym)
xs <- forall sym a.
Backend sym =>
sym -> SEval sym (SeqMap sym a) -> SEval sym (SeqMap sym a)
delaySeqMap sym
sym (forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a
dropSeqMap Integer
front forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"dropV" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val))
forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym Nat'
back TValue
a SeqMap sym (GenValue sym)
xs
{-# INLINE splitV #-}
splitV :: Backend sym =>
sym ->
Nat' ->
Integer ->
TValue ->
SEval sym (GenValue sym) ->
SEval sym (GenValue sym)
splitV :: forall sym.
Backend sym =>
sym
-> Nat'
-> Integer
-> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
splitV sym
sym Nat'
parts Integer
each TValue
a SEval sym (GenValue sym)
val =
case (Nat'
parts, Integer
each) of
(Nat Integer
p, Integer
e) | TValue -> Bool
isTBit TValue
a -> do
SEval sym (WordValue sym)
val' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"splitV" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
val)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
p forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
e forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
extractWordVal sym
sym Integer
e ((Integer
pforall a. Num a => a -> a -> a
-Integer
iforall a. Num a => a -> a -> a
-Integer
1)forall a. Num a => a -> a -> a
*Integer
e) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
val')
(Nat'
Inf, Integer
e) | TValue -> Bool
isTBit TValue
a -> do
SEval sym (SeqMap sym (GenValue sym))
val' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"splitV" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
e 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
e (forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
j ->
let idx :: Integer
idx = Integer
iforall a. Num a => a -> a -> a
*Integer
e forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> Integer
toInteger Integer
j
in Integer
idx seq :: forall a b. a -> b -> b
`seq` do
SeqMap sym (GenValue sym)
xs <- SEval sym (SeqMap sym (GenValue sym))
val'
forall sym. GenValue sym -> SBit sym
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
xs Integer
idx)
(Nat Integer
p, Integer
e) -> do
SEval sym (SeqMap sym (GenValue sym))
val' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"splitV" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
p forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
e forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
j -> do
SeqMap sym (GenValue sym)
xs <- SEval sym (SeqMap sym (GenValue sym))
val'
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
xs (Integer
e forall a. Num a => a -> a -> a
* Integer
i forall a. Num a => a -> a -> a
+ Integer
j)
(Nat'
Inf , Integer
e) -> do
SEval sym (SeqMap sym (GenValue sym))
val' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"splitV" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
e forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
j -> do
SeqMap sym (GenValue sym)
xs <- SEval sym (SeqMap sym (GenValue sym))
val'
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
xs (Integer
e forall a. Num a => a -> a -> a
* Integer
i forall a. Num a => a -> a -> a
+ Integer
j)
{-# INLINE reverseV #-}
reverseV :: forall sym.
Backend sym =>
sym ->
Integer ->
TValue ->
SEval sym (GenValue sym) ->
SEval sym (GenValue sym)
reverseV :: forall sym.
Backend sym =>
sym
-> Integer
-> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
reverseV sym
sym Integer
n TValue
TVBit SEval sym (GenValue sym)
val =
do WordValue sym
w <- forall sym.
Backend sym =>
sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym Integer
n (forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (WordValue sym)
reverseWordVal sym
sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"reverseV" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
n WordValue sym
w)
reverseV sym
sym Integer
n TValue
_a SEval sym (GenValue sym)
val =
do SeqMap sym (GenValue sym)
xs <- forall sym a.
Backend sym =>
sym -> SEval sym (SeqMap sym a) -> SEval sym (SeqMap sym a)
delaySeqMap sym
sym (forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a
reverseSeqMap Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"reverseV" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
n SeqMap sym (GenValue sym)
xs)
{-# INLINE transposeV #-}
transposeV ::
Backend sym =>
sym ->
Nat' ->
Nat' ->
TValue ->
GenValue sym ->
SEval sym (GenValue sym)
transposeV :: forall sym.
Backend sym =>
sym
-> Nat'
-> Nat'
-> TValue
-> GenValue sym
-> SEval sym (GenValue sym)
transposeV sym
sym Nat'
a Nat'
b TValue
c GenValue sym
xs
| TValue -> Bool
isTBit TValue
c, Nat Integer
na <- Nat'
a =
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
bseq forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
bi ->
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
na 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
na (forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
ai ->
do SeqMap sym (GenValue sym)
xs' <- forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"transposeV" GenValue sym
xs
GenValue sym
ys <- forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
xs' Integer
ai
case GenValue sym
ys of
VStream SeqMap sym (GenValue sym)
ys' -> forall sym. GenValue sym -> SBit sym
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
ys' Integer
bi
VWord Integer
_ WordValue sym
wv -> forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym WordValue sym
wv Integer
bi
GenValue sym
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"transpose" [String
"expected sequence of bits"])
| TValue -> Bool
isTBit TValue
c, Nat'
Inf <- Nat'
a =
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
bseq forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
bi ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
ai ->
do SeqMap sym (GenValue sym)
xs' <- forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"transposeV" GenValue sym
xs
GenValue sym
ys <- forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
xs' Integer
ai
case GenValue sym
ys of
VStream SeqMap sym (GenValue sym)
ys' -> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
ys' Integer
bi
VWord Integer
_ WordValue sym
wv -> forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym WordValue sym
wv Integer
bi
GenValue sym
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"transpose" [String
"expected sequence of bits"]
| Bool
otherwise =
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
bseq forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
bi ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
aseq forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
ai -> do
SeqMap sym (GenValue sym)
xs' <- forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"transposeV 1" GenValue sym
xs
SeqMap sym (GenValue sym)
ys <- forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"transposeV 2" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
xs' Integer
ai
GenValue sym
z <- forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
ys Integer
bi
forall (m :: * -> *) a. Monad m => a -> m a
return GenValue sym
z
where
bseq :: SeqMap sym (GenValue sym) -> GenValue sym
bseq =
case Nat'
b of
Nat Integer
nb -> forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
nb
Nat'
Inf -> forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream
aseq :: SeqMap sym (GenValue sym) -> GenValue sym
aseq =
case Nat'
a of
Nat Integer
na -> forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
na
Nat'
Inf -> forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream
{-# INLINE ccatV #-}
ccatV ::
Backend sym =>
sym ->
Integer ->
Nat' ->
TValue ->
SEval sym (GenValue sym) ->
SEval sym (GenValue sym) ->
SEval sym (GenValue sym)
ccatV :: forall sym.
Backend sym =>
sym
-> Integer
-> Nat'
-> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
ccatV sym
sym Integer
front (Nat Integer
back) TValue
TVBit SEval sym (GenValue sym)
l SEval sym (GenValue sym)
r =
do Maybe (GenValue sym)
ml <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (GenValue sym)
l
Maybe (GenValue sym)
mr <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (GenValue sym)
r
case (Maybe (GenValue sym)
ml, Maybe (GenValue sym)
mr) of
(Just GenValue sym
l', Just GenValue sym
r') ->
forall sym. Integer -> WordValue sym -> GenValue sym
VWord (Integer
frontforall a. Num a => a -> a -> a
+Integer
back) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
forall sym.
Backend sym =>
sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
joinWordVal sym
sym (forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"ccatV left" GenValue sym
l') (forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"ccatV right" GenValue sym
r')
(Maybe (GenValue sym), Maybe (GenValue sym))
_ ->
forall sym. Integer -> WordValue sym -> GenValue sym
VWord (Integer
frontforall a. Num a => a -> a -> a
+Integer
back) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym (Integer
frontforall a. Num a => a -> a -> a
+Integer
back)
(do WordValue sym
l' <- forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"ccatV left" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
l
WordValue sym
r' <- forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"ccatV right" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
r
forall sym.
Backend sym =>
sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
joinWordVal sym
sym WordValue sym
l' WordValue sym
r')
ccatV sym
sym Integer
front Nat'
Inf TValue
TVBit SEval sym (GenValue sym)
l SEval sym (GenValue sym)
r =
do SEval sym (SeqMap sym (SBit sym))
l'' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
sym -> WordValue sym -> SeqMap sym (SBit sym)
asBitsMap sym
sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"ccatV left" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
l)
SEval sym (SeqMap sym (GenValue sym))
r'' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"ccatV right" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
r)
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 forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
if Integer
i forall a. Ord a => a -> a -> Bool
< Integer
front then do
SeqMap sym (SBit sym)
ls <- SEval sym (SeqMap sym (SBit sym))
l''
forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (SBit sym)
ls Integer
i
else do
SeqMap sym (GenValue sym)
rs <- SEval sym (SeqMap sym (GenValue sym))
r''
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
rs (Integer
iforall a. Num a => a -> a -> a
-Integer
front)
ccatV sym
sym Integer
front Nat'
back TValue
elty SEval sym (GenValue sym)
l SEval sym (GenValue sym)
r =
do SEval sym (SeqMap sym (GenValue sym))
l'' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"ccatV left" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
l)
SEval sym (SeqMap sym (GenValue sym))
r'' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"ccatV right" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
r)
forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym (TFun -> [Nat'] -> Nat'
evalTF TFun
TCAdd [Integer -> Nat'
Nat Integer
front,Nat'
back]) TValue
elty forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
if Integer
i forall a. Ord a => a -> a -> Bool
< Integer
front then do
SeqMap sym (GenValue sym)
ls <- SEval sym (SeqMap sym (GenValue sym))
l''
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
ls Integer
i
else do
SeqMap sym (GenValue sym)
rs <- SEval sym (SeqMap sym (GenValue sym))
r''
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
rs (Integer
iforall a. Num a => a -> a -> a
-Integer
front)
{-# SPECIALIZE logicBinary ::
Concrete ->
(SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)) ->
(SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)) ->
Binary Concrete
#-}
logicBinary :: forall sym.
Backend sym =>
sym ->
(SBit sym -> SBit sym -> SEval sym (SBit sym)) ->
(SWord sym -> SWord sym -> SEval sym (SWord sym)) ->
Binary sym
logicBinary :: forall sym.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> Binary sym
logicBinary sym
sym SBit sym -> SBit sym -> SEval sym (SBit sym)
opb SWord sym -> SWord sym -> SEval sym (SWord sym)
opw = TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
loop
where
loop' :: TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' :: TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' TValue
ty SEval sym (GenValue sym)
l SEval sym (GenValue sym)
r = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SEval sym (GenValue sym)
r)
loop :: TValue
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
loop :: TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
ty GenValue sym
l GenValue sym
r = case TValue
ty of
TValue
TVBit -> forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SBit sym -> SBit sym -> SEval sym (SBit sym)
opb (forall sym. GenValue sym -> SBit sym
fromVBit GenValue sym
l) (forall sym. GenValue sym -> SBit sym
fromVBit GenValue sym
r))
TValue
TVInteger -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicBinary" [String
"Integer not in class Logic"]
TVIntMod Integer
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicBinary" [String
"Z not in class Logic"]
TValue
TVRational -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicBinary" [String
"Rational not in class Logic"]
TVArray{} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicBinary" [String
"Array not in class Logic"]
TVFloat {} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicBinary" [String
"Float not in class Logic"]
TVSeq Integer
w TValue
aty
| TValue -> Bool
isTBit TValue
aty
-> forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym Integer
w
(forall sym.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
wordValLogicOp sym
sym SBit sym -> SBit sym -> SEval sym (SBit sym)
opb SWord sym -> SWord sym -> SEval sym (SWord sym)
opw
(forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"logicBinary l" GenValue sym
l)
(forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"logicBinary r" GenValue sym
r))
| Bool
otherwise -> forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (forall sym a.
Backend sym =>
sym
-> (a -> a -> SEval sym a)
-> Nat'
-> SeqMap sym a
-> SeqMap sym a
-> SEval sym (SeqMap sym a)
zipSeqMap sym
sym (TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
aty) (Integer -> Nat'
Nat Integer
w) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"logicBinary left" GenValue sym
l)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"logicBinary right" GenValue sym
r)))
TVStream TValue
aty ->
forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (forall sym a.
Backend sym =>
sym
-> (a -> a -> SEval sym a)
-> Nat'
-> SeqMap sym a
-> SeqMap sym a
-> SEval sym (SeqMap sym a)
zipSeqMap sym
sym (TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
aty) Nat'
Inf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"logicBinary left" GenValue sym
l) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
(forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"logicBinary right" GenValue sym
r)))
TVTuple [TValue]
etys -> do
[SEval sym (GenValue sym)]
ls <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym) (forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
l)
[SEval sym (GenValue sym)]
rs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym) (forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
r)
forall (m :: * -> *) a. Monad m => a -> m a
return 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 d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' [TValue]
etys [SEval sym (GenValue sym)]
ls [SEval sym (GenValue sym)]
rs
TVFun TValue
_ TValue
bty ->
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)
a -> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' TValue
bty (forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym GenValue sym
l SEval sym (GenValue sym)
a) (forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym GenValue sym
r SEval sym (GenValue sym)
a)
TVRec RecordMap Ident TValue
fields ->
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
forall (t :: * -> *) a b c.
Applicative t =>
(a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
traverseRecordMap
(\Ident
f TValue
fty -> forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
loop' TValue
fty (forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
f GenValue sym
l) (forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
f GenValue sym
r)))
RecordMap Ident TValue
fields
TVAbstract {} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicBinary"
[ String
"Abstract type not in `Logic`" ]
TVNewtype {} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicBinary"
[ String
"Newtype not in `Logic`" ]
{-# SPECIALIZE logicUnary ::
Concrete ->
(SBit Concrete -> SEval Concrete (SBit Concrete)) ->
(SWord Concrete -> SEval Concrete (SWord Concrete)) ->
Unary Concrete
#-}
logicUnary :: forall sym.
Backend sym =>
sym ->
(SBit sym -> SEval sym (SBit sym)) ->
(SWord sym -> SEval sym (SWord sym)) ->
Unary sym
logicUnary :: forall sym.
Backend sym =>
sym
-> (SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SEval sym (SWord sym))
-> Unary sym
logicUnary sym
sym SBit sym -> SEval sym (SBit sym)
opb SWord sym -> SEval sym (SWord sym)
opw = TValue -> GenValue sym -> SEval sym (GenValue sym)
loop
where
loop' :: TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' :: TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' TValue
ty SEval sym (GenValue sym)
val = TValue -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
ty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val
loop :: TValue -> GenValue sym -> SEval sym (GenValue sym)
loop :: TValue -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
ty GenValue sym
val = case TValue
ty of
TValue
TVBit -> forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SBit sym -> SEval sym (SBit sym)
opb (forall sym. GenValue sym -> SBit sym
fromVBit GenValue sym
val))
TValue
TVInteger -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicUnary" [String
"Integer not in class Logic"]
TVIntMod Integer
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicUnary" [String
"Z not in class Logic"]
TVFloat {} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicUnary" [String
"Float not in class Logic"]
TValue
TVRational -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicBinary" [String
"Rational not in class Logic"]
TVArray{} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicUnary" [String
"Array not in class Logic"]
TVSeq Integer
w TValue
ety
| TValue -> Bool
isTBit TValue
ety
-> forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym Integer
w (forall sym.
Backend sym =>
sym
-> (SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SEval sym (SWord sym))
-> WordValue sym
-> SEval sym (WordValue sym)
wordValUnaryOp sym
sym SBit sym -> SEval sym (SBit sym)
opb SWord sym -> SEval sym (SWord sym)
opw (forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"logicUnary" GenValue sym
val))
| Bool
otherwise
-> forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym a.
Backend sym =>
sym
-> (a -> SEval sym a)
-> Nat'
-> SeqMap sym a
-> SEval sym (SeqMap sym a)
mapSeqMap sym
sym (TValue -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
ety) (Integer -> Nat'
Nat Integer
w) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"logicUnary" GenValue sym
val)
TVStream TValue
ety ->
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
-> (a -> SEval sym a)
-> Nat'
-> SeqMap sym a
-> SEval sym (SeqMap sym a)
mapSeqMap sym
sym (TValue -> GenValue sym -> SEval sym (GenValue sym)
loop TValue
ety) Nat'
Inf forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"logicUnary" GenValue sym
val)
TVTuple [TValue]
etys ->
do [SEval sym (GenValue sym)]
as <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym) (forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
val)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' [TValue]
etys [SEval sym (GenValue sym)]
as)
TVFun TValue
_ TValue
bty ->
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)
a -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' TValue
bty (forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym GenValue sym
val SEval sym (GenValue sym)
a)
TVRec RecordMap Ident TValue
fields ->
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
forall (t :: * -> *) a b c.
Applicative t =>
(a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
traverseRecordMap
(\Ident
f TValue
fty -> forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' TValue
fty (forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
f GenValue sym
val)))
RecordMap Ident TValue
fields
TVAbstract {} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicUnary" [ String
"Abstract type not in `Logic`" ]
TVNewtype {} -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicUnary" [ String
"Newtype not in `Logic`" ]
{-# INLINE assertIndexInBounds #-}
assertIndexInBounds ::
Backend sym =>
sym ->
Nat' ->
Either (SInteger sym) (WordValue sym) ->
SEval sym ()
assertIndexInBounds :: forall sym.
Backend sym =>
sym
-> Nat' -> Either (SInteger sym) (WordValue sym) -> SEval sym ()
assertIndexInBounds sym
sym Nat'
Inf (Left SInteger sym
idx) =
do SBit sym
ppos <- forall sym. Backend sym => sym -> SBit sym -> SEval sym (SBit sym)
bitComplement sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intLessThan sym
sym SInteger sym
idx forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
0
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition sym
sym SBit sym
ppos (Maybe Integer -> EvalError
InvalidIndex (forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
idx))
assertIndexInBounds sym
sym (Nat Integer
n) (Left SInteger sym
idx) =
do SInteger sym
n' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
n
SBit sym
ppos <- forall sym. Backend sym => sym -> SBit sym -> SEval sym (SBit sym)
bitComplement sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intLessThan sym
sym SInteger sym
idx forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
0
SBit sym
pn <- forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intLessThan sym
sym SInteger sym
idx SInteger sym
n'
SBit sym
p <- forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitAnd sym
sym SBit sym
ppos SBit sym
pn
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition sym
sym SBit sym
p (Maybe Integer -> EvalError
InvalidIndex (forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
idx))
assertIndexInBounds sym
_sym Nat'
Inf (Right WordValue sym
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertIndexInBounds sym
sym (Nat Integer
n) (Right WordValue sym
idx) =
forall sym.
Backend sym =>
sym -> Integer -> WordValue sym -> SEval sym ()
assertWordValueInBounds sym
sym Integer
n WordValue sym
idx
{-# INLINE indexPrim #-}
indexPrim ::
Backend sym =>
sym ->
IndexDirection ->
(Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> SInteger sym -> SEval sym (GenValue sym)) ->
(Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> Integer -> [IndexSegment sym] -> SEval sym (GenValue sym)) ->
Prim sym
indexPrim :: forall sym.
Backend sym =>
sym
-> IndexDirection
-> (Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> TValue
-> SInteger sym
-> SEval sym (GenValue sym))
-> (Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> TValue
-> Integer
-> [IndexSegment sym]
-> SEval sym (GenValue sym))
-> Prim sym
indexPrim sym
sym IndexDirection
dir Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> TValue
-> SInteger sym
-> SEval sym (GenValue sym)
int_op Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> TValue
-> Integer
-> [IndexSegment sym]
-> SEval sym (GenValue sym)
word_op =
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
len ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
eltTy ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ix ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
xs ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
idx ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do SeqMap sym (GenValue sym)
vs <- SEval sym (GenValue sym)
xs forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
VWord Integer
_ WordValue sym
w -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap (\Integer
i -> forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym WordValue sym
w Integer
i)
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
"Expected sequence value" [String
"indexPrim"]
let vs' :: SeqMap sym (GenValue sym)
vs' = case (Nat'
len, IndexDirection
dir) of
(Nat'
_ , IndexDirection
IndexForward) -> SeqMap sym (GenValue sym)
vs
(Nat Integer
n, IndexDirection
IndexBackward) -> forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a
reverseSeqMap Integer
n SeqMap sym (GenValue sym)
vs
(Nat'
Inf , IndexDirection
IndexBackward) -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"Expected finite sequence" [String
"!"]
Either (SInteger sym) (WordValue sym)
idx' <- forall sym.
Backend sym =>
sym
-> String
-> TValue
-> GenValue sym
-> Either (SInteger sym) (WordValue sym)
asIndex sym
sym String
"index" TValue
ix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
idx
forall sym.
Backend sym =>
sym
-> Nat' -> Either (SInteger sym) (WordValue sym) -> SEval sym ()
assertIndexInBounds sym
sym Nat'
len Either (SInteger sym) (WordValue sym)
idx'
case Either (SInteger sym) (WordValue sym)
idx' of
Left SInteger sym
i -> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> TValue
-> SInteger sym
-> SEval sym (GenValue sym)
int_op Nat'
len TValue
eltTy SeqMap sym (GenValue sym)
vs' TValue
ix SInteger sym
i
Right WordValue sym
w -> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> TValue
-> Integer
-> [IndexSegment sym]
-> SEval sym (GenValue sym)
word_op Nat'
len TValue
eltTy SeqMap sym (GenValue sym)
vs' TValue
ix (forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
w) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [IndexSegment sym]
enumerateIndexSegments sym
sym WordValue sym
w
{-# INLINE updatePrim #-}
updatePrim ::
Backend sym =>
sym ->
(Nat' -> TValue -> WordValue sym -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (WordValue sym)) ->
(Nat' -> TValue -> SeqMap sym (GenValue sym) -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (SeqMap sym (GenValue sym))) ->
Prim sym
updatePrim :: forall sym.
Backend sym =>
sym
-> (Nat'
-> TValue
-> WordValue sym
-> Either (SInteger sym) (WordValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (WordValue sym))
-> (Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> Either (SInteger sym) (WordValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym)))
-> Prim sym
updatePrim sym
sym Nat'
-> TValue
-> WordValue sym
-> Either (SInteger sym) (WordValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (WordValue sym)
updateWord Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> Either (SInteger sym) (WordValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
updateSeq =
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
len ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
eltTy ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ix ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
xs ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
idx ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
val ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do Either (SInteger sym) (WordValue sym)
idx' <- forall sym.
Backend sym =>
sym
-> String
-> TValue
-> GenValue sym
-> Either (SInteger sym) (WordValue sym)
asIndex sym
sym String
"update" TValue
ix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
idx
forall sym.
Backend sym =>
sym
-> Nat' -> Either (SInteger sym) (WordValue sym) -> SEval sym ()
assertIndexInBounds sym
sym Nat'
len Either (SInteger sym) (WordValue sym)
idx'
case (Nat'
len, TValue
eltTy) of
(Nat Integer
n, TValue
TVBit) -> 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
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym Integer
n
(do WordValue sym
w <- forall sym. Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal String
"updatePrim" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
xs; Nat'
-> TValue
-> WordValue sym
-> Either (SInteger sym) (WordValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (WordValue sym)
updateWord Nat'
len TValue
eltTy WordValue sym
w Either (SInteger sym) (WordValue sym)
idx' SEval sym (GenValue sym)
val)
(Nat Integer
n, TValue
_ ) -> forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a.
Backend sym =>
sym -> SEval sym (SeqMap sym a) -> SEval sym (SeqMap sym a)
delaySeqMap sym
sym
(do SeqMap sym (GenValue sym)
vs <- forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"updatePrim" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
xs; Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> Either (SInteger sym) (WordValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
updateSeq Nat'
len TValue
eltTy SeqMap sym (GenValue sym)
vs Either (SInteger sym) (WordValue sym)
idx' SEval sym (GenValue sym)
val)
(Nat'
Inf , TValue
_ ) -> 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 -> SEval sym (SeqMap sym a) -> SEval sym (SeqMap sym a)
delaySeqMap sym
sym
(do SeqMap sym (GenValue sym)
vs <- forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
"updatePrim" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
xs; Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> Either (SInteger sym) (WordValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
updateSeq Nat'
len TValue
eltTy SeqMap sym (GenValue sym)
vs Either (SInteger sym) (WordValue sym)
idx' SEval sym (GenValue sym)
val)
{-# INLINE fromToV #-}
fromToV :: Backend sym => sym -> Prim sym
fromToV :: forall sym. Backend sym => sym -> Prim sym
fromToV sym
sym =
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
first ->
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
lst ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
let !f :: Integer -> SEval sym (GenValue sym)
f = forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
mkLit sym
sym TValue
ty in
case (Nat'
first, Nat'
lst) of
(Nat Integer
first', Nat Integer
lst') ->
let len :: Integer
len = Integer
1 forall a. Num a => a -> a -> a
+ (Integer
lst' forall a. Num a => a -> a -> a
- Integer
first')
in forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym (Integer -> Nat'
Nat Integer
len) TValue
ty forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> Integer -> SEval sym (GenValue sym)
f (Integer
first' forall a. Num a => a -> a -> a
+ Integer
i)
(Nat', Nat')
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromToV" [String
"invalid arguments"]
{-# INLINE fromThenToV #-}
fromThenToV :: Backend sym => sym -> Prim sym
fromThenToV :: forall sym. Backend sym => sym -> Prim sym
fromThenToV sym
sym =
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
first ->
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
next ->
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
lst ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
len ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
let !f :: Integer -> SEval sym (GenValue sym)
f = forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
mkLit sym
sym TValue
ty in
case (Nat'
first, Nat'
next, Nat'
lst, Nat'
len) of
(Nat Integer
first', Nat Integer
next', Nat Integer
_lst', Nat Integer
len') ->
let diff :: Integer
diff = Integer
next' forall a. Num a => a -> a -> a
- Integer
first'
in forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym (Integer -> Nat'
Nat Integer
len') TValue
ty forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> Integer -> SEval sym (GenValue sym)
f (Integer
first' forall a. Num a => a -> a -> a
+ Integer
iforall a. Num a => a -> a -> a
*Integer
diff)
(Nat', Nat', Nat', Nat')
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromThenToV" [String
"invalid arguments"]
{-# INLINE fromToLessThanV #-}
fromToLessThanV :: Backend sym => sym -> Prim sym
fromToLessThanV :: forall sym. Backend sym => sym -> Prim sym
fromToLessThanV sym
sym =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
first ->
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
bound ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
let !f :: Integer -> SEval sym (GenValue sym)
f = forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
mkLit sym
sym TValue
ty
ss :: SeqMap sym (GenValue sym)
ss = forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> Integer -> SEval sym (GenValue sym)
f (Integer
first forall a. Num a => a -> a -> a
+ Integer
i)
in case Nat'
bound of
Nat'
Inf -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream SeqMap sym (GenValue sym)
ss
Nat Integer
bound' -> forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym (Integer -> Nat'
Nat (Integer
bound' forall a. Num a => a -> a -> a
- Integer
first)) TValue
ty SeqMap sym (GenValue sym)
ss
{-# INLINE fromToByV #-}
fromToByV :: Backend sym => sym -> Prim sym
fromToByV :: forall sym. Backend sym => sym -> Prim sym
fromToByV sym
sym =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
first ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
lst ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
stride ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
let !f :: Integer -> SEval sym (GenValue sym)
f = forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
mkLit sym
sym TValue
ty
ss :: SeqMap sym (GenValue sym)
ss = forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> Integer -> SEval sym (GenValue sym)
f (Integer
first forall a. Num a => a -> a -> a
+ Integer
iforall a. Num a => a -> a -> a
*Integer
stride)
in forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym (Integer -> Nat'
Nat (Integer
1 forall a. Num a => a -> a -> a
+ ((Integer
lst forall a. Num a => a -> a -> a
- Integer
first) forall a. Integral a => a -> a -> a
`div` Integer
stride))) TValue
ty SeqMap sym (GenValue sym)
ss
{-# INLINE fromToByLessThanV #-}
fromToByLessThanV :: Backend sym => sym -> Prim sym
fromToByLessThanV :: forall sym. Backend sym => sym -> Prim sym
fromToByLessThanV sym
sym =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
first ->
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
bound ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
stride ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
let !f :: Integer -> SEval sym (GenValue sym)
f = forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
mkLit sym
sym TValue
ty
ss :: SeqMap sym (GenValue sym)
ss = forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> Integer -> SEval sym (GenValue sym)
f (Integer
first forall a. Num a => a -> a -> a
+ Integer
iforall a. Num a => a -> a -> a
*Integer
stride)
in case Nat'
bound of
Nat'
Inf -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream SeqMap sym (GenValue sym)
ss
Nat Integer
bound' -> forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym (Integer -> Nat'
Nat ((Integer
bound' forall a. Num a => a -> a -> a
- Integer
first forall a. Num a => a -> a -> a
+ Integer
stride forall a. Num a => a -> a -> a
- Integer
1) forall a. Integral a => a -> a -> a
`div` Integer
stride)) TValue
ty SeqMap sym (GenValue sym)
ss
{-# INLINE fromToDownByV #-}
fromToDownByV :: Backend sym => sym -> Prim sym
fromToDownByV :: forall sym. Backend sym => sym -> Prim sym
fromToDownByV sym
sym =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
first ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
lst ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
stride ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
let !f :: Integer -> SEval sym (GenValue sym)
f = forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
mkLit sym
sym TValue
ty
ss :: SeqMap sym (GenValue sym)
ss = forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> Integer -> SEval sym (GenValue sym)
f (Integer
first forall a. Num a => a -> a -> a
- Integer
iforall a. Num a => a -> a -> a
*Integer
stride)
in forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym (Integer -> Nat'
Nat (Integer
1 forall a. Num a => a -> a -> a
+ ((Integer
first forall a. Num a => a -> a -> a
- Integer
lst) forall a. Integral a => a -> a -> a
`div` Integer
stride))) TValue
ty SeqMap sym (GenValue sym)
ss
{-# INLINE fromToDownByGreaterThanV #-}
fromToDownByGreaterThanV :: Backend sym => sym -> Prim sym
fromToDownByGreaterThanV :: forall sym. Backend sym => sym -> Prim sym
fromToDownByGreaterThanV sym
sym =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
first ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
bound ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
stride ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
let !f :: Integer -> SEval sym (GenValue sym)
f = forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
mkLit sym
sym TValue
ty
ss :: SeqMap sym (GenValue sym)
ss = forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> Integer -> SEval sym (GenValue sym)
f (Integer
first forall a. Num a => a -> a -> a
- Integer
iforall a. Num a => a -> a -> a
*Integer
stride)
in forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym (Integer -> Nat'
Nat ((Integer
first forall a. Num a => a -> a -> a
- Integer
bound forall a. Num a => a -> a -> a
+ Integer
stride forall a. Num a => a -> a -> a
- Integer
1) forall a. Integral a => a -> a -> a
`div` Integer
stride)) TValue
ty SeqMap sym (GenValue sym)
ss
{-# INLINE infFromV #-}
infFromV :: Backend sym => sym -> Prim sym
infFromV :: forall sym. Backend sym => sym -> Prim sym
infFromV sym
sym =
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do SEval sym (GenValue sym)
mx <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym SEval sym (GenValue sym)
x
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
do GenValue sym
x' <- SEval sym (GenValue sym)
mx
SInteger sym
i' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
i
forall sym. Backend sym => sym -> Binary sym
addV sym
sym TValue
ty GenValue sym
x' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
intV sym
sym SInteger sym
i' TValue
ty
{-# INLINE infFromThenV #-}
infFromThenV :: Backend sym => sym -> Prim sym
infFromThenV :: forall sym. Backend sym => sym -> Prim sym
infFromThenV sym
sym =
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
first ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
next ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do SEval sym (GenValue sym, GenValue sym)
mxd <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym
(do GenValue sym
x <- SEval sym (GenValue sym)
first
GenValue sym
y <- SEval sym (GenValue sym)
next
GenValue sym
d <- forall sym. Backend sym => sym -> Binary sym
subV sym
sym TValue
ty GenValue sym
y GenValue sym
x
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym
x,GenValue sym
d))
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> do
(GenValue sym
x,GenValue sym
d) <- SEval sym (GenValue sym, GenValue sym)
mxd
SInteger sym
i' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
i
forall sym. Backend sym => sym -> Binary sym
addV sym
sym TValue
ty GenValue sym
x forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. Backend sym => sym -> Binary sym
mulV sym
sym TValue
ty GenValue sym
d forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
intV sym
sym SInteger sym
i' TValue
ty
{-# INLINE shiftLeftReindex #-}
shiftLeftReindex :: Nat' -> Integer -> Integer -> Maybe Integer
shiftLeftReindex :: Nat' -> Integer -> Integer -> Maybe Integer
shiftLeftReindex Nat'
sz Integer
i Integer
shft =
case Nat'
sz of
Nat Integer
n | Integer
iforall a. Num a => a -> a -> a
+Integer
shft forall a. Ord a => a -> a -> Bool
>= Integer
n -> forall a. Maybe a
Nothing
Nat'
_ -> forall a. a -> Maybe a
Just (Integer
iforall a. Num a => a -> a -> a
+Integer
shft)
{-# INLINE shiftRightReindex #-}
shiftRightReindex :: Nat' -> Integer -> Integer -> Maybe Integer
shiftRightReindex :: Nat' -> Integer -> Integer -> Maybe Integer
shiftRightReindex Nat'
_sz Integer
i Integer
shft =
if Integer
iforall a. Num a => a -> a -> a
-Integer
shft forall a. Ord a => a -> a -> Bool
< Integer
0 then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just (Integer
iforall a. Num a => a -> a -> a
-Integer
shft)
{-# INLINE rotateLeftReindex #-}
rotateLeftReindex :: Nat' -> Integer -> Integer -> Maybe Integer
rotateLeftReindex :: Nat' -> Integer -> Integer -> Maybe Integer
rotateLeftReindex Nat'
sz Integer
i Integer
shft =
case Nat'
sz of
Nat'
Inf -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"cannot rotate infinite sequence" []
Nat Integer
n -> forall a. a -> Maybe a
Just ((Integer
iforall a. Num a => a -> a -> a
+Integer
shft) forall a. Integral a => a -> a -> a
`mod` Integer
n)
{-# INLINE rotateRightReindex #-}
rotateRightReindex :: Nat' -> Integer -> Integer -> Maybe Integer
rotateRightReindex :: Nat' -> Integer -> Integer -> Maybe Integer
rotateRightReindex Nat'
sz Integer
i Integer
shft =
case Nat'
sz of
Nat'
Inf -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"cannot rotate infinite sequence" []
Nat Integer
n -> forall a. a -> Maybe a
Just ((Integer
iforall a. Num a => a -> a -> a
+Integer
nforall a. Num a => a -> a -> a
-Integer
shft) forall a. Integral a => a -> a -> a
`mod` Integer
n)
{-# INLINE logicShift #-}
logicShift :: Backend sym =>
sym ->
String ->
(sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
->
(SWord sym -> SWord sym -> SEval sym (SWord sym))
->
(SWord sym -> SWord sym -> SEval sym (SWord sym))
->
(Nat' -> Integer -> Integer -> Maybe Integer)
->
(Nat' -> Integer -> Integer -> Maybe Integer)
->
Prim sym
logicShift :: forall sym.
Backend sym =>
sym
-> String
-> (sym
-> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Prim sym
logicShift sym
sym String
nm sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shrinkRange SWord sym -> SWord sym -> SEval sym (SWord sym)
wopPos SWord sym -> SWord sym -> SEval sym (SWord sym)
wopNeg Nat' -> Integer -> Integer -> Maybe Integer
reindexPos Nat' -> Integer -> Integer -> Maybe Integer
reindexNeg =
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
m ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ix ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
a ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
xs ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
y ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do GenValue sym
xs' <- SEval sym (GenValue sym)
xs
Either (SInteger sym) (WordValue sym)
y' <- forall sym.
Backend sym =>
sym
-> String
-> TValue
-> GenValue sym
-> Either (SInteger sym) (WordValue sym)
asIndex sym
sym String
"shift" TValue
ix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
y
case Either (SInteger sym) (WordValue sym)
y' of
Left SInteger sym
int_idx ->
do SBit sym
pneg <- forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intLessThan sym
sym SInteger sym
int_idx forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
0
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue sym
sym SBit sym
pneg
(forall sym.
Backend sym =>
sym
-> String
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Nat'
-> TValue
-> GenValue sym
-> SInteger sym
-> SEval sym (GenValue sym)
intShifter sym
sym String
nm SWord sym -> SWord sym -> SEval sym (SWord sym)
wopNeg Nat' -> Integer -> Integer -> Maybe Integer
reindexNeg Nat'
m TValue
a GenValue sym
xs' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shrinkRange sym
sym Nat'
m TValue
ix forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SInteger sym)
intNegate sym
sym SInteger sym
int_idx)
(forall sym.
Backend sym =>
sym
-> String
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Nat'
-> TValue
-> GenValue sym
-> SInteger sym
-> SEval sym (GenValue sym)
intShifter sym
sym String
nm SWord sym -> SWord sym -> SEval sym (SWord sym)
wopPos Nat' -> Integer -> Integer -> Maybe Integer
reindexPos Nat'
m TValue
a GenValue sym
xs' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shrinkRange sym
sym Nat'
m TValue
ix SInteger sym
int_idx)
Right WordValue sym
idx ->
forall sym.
Backend sym =>
sym
-> String
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Nat'
-> TValue
-> GenValue sym
-> WordValue sym
-> SEval sym (GenValue sym)
wordShifter sym
sym String
nm SWord sym -> SWord sym -> SEval sym (SWord sym)
wopPos Nat' -> Integer -> Integer -> Maybe Integer
reindexPos Nat'
m TValue
a GenValue sym
xs' WordValue sym
idx
{-# INLINE intShifter #-}
intShifter :: Backend sym =>
sym ->
String ->
(SWord sym -> SWord sym -> SEval sym (SWord sym)) ->
(Nat' -> Integer -> Integer -> Maybe Integer) ->
Nat' ->
TValue ->
GenValue sym ->
SInteger sym ->
SEval sym (GenValue sym)
intShifter :: forall sym.
Backend sym =>
sym
-> String
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Nat'
-> TValue
-> GenValue sym
-> SInteger sym
-> SEval sym (GenValue sym)
intShifter sym
sym String
nm SWord sym -> SWord sym -> SEval sym (SWord sym)
wop Nat' -> Integer -> Integer -> Maybe Integer
reindex Nat'
m TValue
a GenValue sym
xs SInteger sym
idx =
case GenValue sym
xs of
VWord Integer
w WordValue sym
x -> forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Integer -> Integer -> Maybe Integer)
-> WordValue sym
-> SInteger sym
-> SEval sym (WordValue sym)
shiftWordByInteger sym
sym SWord sym -> SWord sym -> SEval sym (SWord sym)
wop (Nat' -> Integer -> Integer -> Maybe Integer
reindex Nat'
m) WordValue sym
x SInteger sym
idx
VSeq Integer
w SeqMap sym (GenValue sym)
vs -> forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> (Integer -> Integer -> Maybe Integer)
-> SEval sym a
-> Nat'
-> SeqMap sym a
-> SInteger sym
-> SEval sym (SeqMap sym a)
shiftSeqByInteger sym
sym (forall sym.
Backend sym =>
sym
-> SBit sym
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
mergeValue sym
sym) (Nat' -> Integer -> Integer -> Maybe Integer
reindex Nat'
m) (forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
a) Nat'
m SeqMap sym (GenValue sym)
vs SInteger sym
idx
VStream SeqMap sym (GenValue sym)
vs -> 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
-> (SBit sym -> a -> a -> SEval sym a)
-> (Integer -> Integer -> Maybe Integer)
-> SEval sym a
-> Nat'
-> SeqMap sym a
-> SInteger sym
-> SEval sym (SeqMap sym a)
shiftSeqByInteger sym
sym (forall sym.
Backend sym =>
sym
-> SBit sym
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
mergeValue sym
sym) (Nat' -> Integer -> Integer -> Maybe Integer
reindex Nat'
m) (forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
a) Nat'
m SeqMap sym (GenValue sym)
vs SInteger sym
idx
GenValue sym
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"expected sequence value in shift operation" [String
nm]
{-# INLINE wordShifter #-}
wordShifter :: Backend sym =>
sym ->
String ->
(SWord sym -> SWord sym -> SEval sym (SWord sym)) ->
(Nat' -> Integer -> Integer -> Maybe Integer) ->
Nat' ->
TValue ->
GenValue sym ->
WordValue sym ->
SEval sym (GenValue sym)
wordShifter :: forall sym.
Backend sym =>
sym
-> String
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Nat'
-> TValue
-> GenValue sym
-> WordValue sym
-> SEval sym (GenValue sym)
wordShifter sym
sym String
nm SWord sym -> SWord sym -> SEval sym (SWord sym)
wop Nat' -> Integer -> Integer -> Maybe Integer
reindex Nat'
m TValue
a GenValue sym
xs WordValue sym
idx =
case GenValue sym
xs of
VWord Integer
w WordValue sym
x -> forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Integer -> Integer -> Maybe Integer)
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
shiftWordByWord sym
sym SWord sym -> SWord sym -> SEval sym (SWord sym)
wop (Nat' -> Integer -> Integer -> Maybe Integer
reindex Nat'
m) WordValue sym
x WordValue sym
idx
VSeq Integer
w SeqMap sym (GenValue sym)
vs -> forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> (Integer -> Integer -> Maybe Integer)
-> SEval sym a
-> Nat'
-> SeqMap sym a
-> WordValue sym
-> SEval sym (SeqMap sym a)
shiftSeqByWord sym
sym (forall sym.
Backend sym =>
sym
-> SBit sym
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
mergeValue sym
sym) (Nat' -> Integer -> Integer -> Maybe Integer
reindex Nat'
m) (forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
a) (Integer -> Nat'
Nat Integer
w) SeqMap sym (GenValue sym)
vs WordValue sym
idx
VStream SeqMap sym (GenValue sym)
vs -> 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
-> (SBit sym -> a -> a -> SEval sym a)
-> (Integer -> Integer -> Maybe Integer)
-> SEval sym a
-> Nat'
-> SeqMap sym a
-> WordValue sym
-> SEval sym (SeqMap sym a)
shiftSeqByWord sym
sym (forall sym.
Backend sym =>
sym
-> SBit sym
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
mergeValue sym
sym) (Nat' -> Integer -> Integer -> Maybe Integer
reindex Nat'
m) (forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
a) Nat'
Inf SeqMap sym (GenValue sym)
vs WordValue sym
idx
GenValue sym
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"expected sequence value in shift operation" [String
nm]
{-# INLINE shiftShrink #-}
shiftShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink :: forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink sym
_sym Nat'
Inf TValue
_ SInteger sym
x = forall (m :: * -> *) a. Monad m => a -> m a
return SInteger sym
x
shiftShrink sym
sym (Nat Integer
w) TValue
_ SInteger sym
x =
do SInteger sym
w' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
w
SBit sym
p <- forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intLessThan sym
sym SInteger sym
w' SInteger sym
x
forall sym.
Backend sym =>
sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
iteInteger sym
sym SBit sym
p SInteger sym
w' SInteger sym
x
{-# INLINE rotateShrink #-}
rotateShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
rotateShrink :: forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
rotateShrink sym
_sym Nat'
Inf TValue
_ SInteger sym
_ = forall a. HasCallStack => String -> [String] -> a
panic String
"rotateShrink" [String
"expected finite sequence in rotate"]
rotateShrink sym
sym (Nat Integer
0) TValue
_ SInteger sym
_ = forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
0
rotateShrink sym
sym (Nat Integer
w) TValue
_ SInteger sym
x =
do SInteger sym
w' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
w
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
intMod sym
sym SInteger sym
x SInteger sym
w'
{-# INLINE sshrV #-}
sshrV :: Backend sym => sym -> Prim sym
sshrV :: forall sym. Backend sym => sym -> Prim sym
sshrV sym
sym =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ix ->
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord sym
x ->
forall sym. (GenValue sym -> Prim sym) -> Prim sym
PStrict \GenValue sym
y ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim forall a b. (a -> b) -> a -> b
$
case forall sym.
Backend sym =>
sym
-> String
-> TValue
-> GenValue sym
-> Either (SInteger sym) (WordValue sym)
asIndex sym
sym String
">>$" TValue
ix GenValue sym
y of
Left SInteger sym
i ->
do SBit sym
pneg <- forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intLessThan sym
sym SInteger sym
i forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
0
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
-> SBit sym
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
mergeWord' sym
sym
SBit sym
pneg
(do SInteger sym
i' <- forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink sym
sym (Integer -> Nat'
Nat Integer
n) TValue
ix forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> SInteger sym -> SEval sym (SInteger sym)
intNegate sym
sym SInteger sym
i
SWord sym
amt <- forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
wordFromInt sym
sym Integer
n SInteger sym
i'
forall sym. SWord sym -> WordValue sym
wordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordShiftLeft sym
sym SWord sym
x SWord sym
amt)
(do SInteger sym
i' <- forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink sym
sym (Integer -> Nat'
Nat Integer
n) TValue
ix SInteger sym
i
SWord sym
amt <- forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
wordFromInt sym
sym Integer
n SInteger sym
i'
forall sym. SWord sym -> WordValue sym
wordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordSignedShiftRight sym
sym SWord sym
x SWord sym
amt)
Right WordValue sym
wv ->
do SWord sym
amt <- forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym WordValue sym
wv
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 -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordSignedShiftRight sym
sym SWord sym
x SWord sym
amt
{-# SPECIALIZE errorV ::
Concrete ->
TValue ->
String ->
SEval Concrete (GenValue Concrete)
#-}
errorV :: forall sym.
Backend sym =>
sym ->
TValue ->
String ->
SEval sym (GenValue sym)
errorV :: forall sym.
Backend sym =>
sym -> TValue -> String -> SEval sym (GenValue sym)
errorV sym
sym TValue
_ty String
msg =
do CallStack
stk <- forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym
forall sym a.
Backend sym =>
sym -> CallStack -> SEval sym a -> SEval sym a
sWithCallStack sym
sym CallStack
stk (forall sym a. Backend sym => sym -> String -> SEval sym a
cryUserError sym
sym String
msg)
{-# INLINE valueToChar #-}
valueToChar :: Backend sym => sym -> GenValue sym -> SEval sym Char
valueToChar :: forall sym. Backend sym => sym -> GenValue sym -> SEval sym Char
valueToChar sym
sym (VWord Integer
8 WordValue sym
wval) =
do SWord sym
w <- forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym WordValue sym
wval
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall a. a -> Maybe a -> a
fromMaybe Char
'?' (forall sym. Backend sym => sym -> SWord sym -> Maybe Char
wordAsChar sym
sym SWord sym
w)
valueToChar sym
_ GenValue sym
_ = forall a. HasCallStack => String -> [String] -> a
evalPanic String
"valueToChar" [String
"Not an 8-bit bitvector"]
{-# INLINE valueToString #-}
valueToString :: Backend sym => sym -> GenValue sym -> SEval sym String
valueToString :: forall sym. Backend sym => sym -> GenValue sym -> SEval sym String
valueToString sym
sym (VSeq Integer
n SeqMap sym (GenValue sym)
vals) = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym. Backend sym => sym -> GenValue sym -> SEval sym Char
valueToChar sym
sym 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)
vals)
valueToString sym
_ GenValue sym
_ = forall a. HasCallStack => String -> [String] -> a
evalPanic String
"valueToString" [String
"Not a finite sequence"]
foldlV :: Backend sym => sym -> Prim sym
foldlV :: forall sym. Backend sym => sym -> Prim sym
foldlV sym
sym =
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
_n ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
_a ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
_b ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
f ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
z ->
forall sym. (GenValue sym -> Prim sym) -> Prim sym
PStrict \GenValue sym
v ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
case GenValue sym
v of
VSeq Integer
n SeqMap sym (GenValue sym)
m -> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> [SEval sym (GenValue sym)]
-> SEval sym (GenValue sym)
go0 SEval sym (GenValue sym)
f SEval sym (GenValue sym)
z (forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n SeqMap sym (GenValue sym)
m)
VWord Integer
_n WordValue sym
wv -> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> [SEval sym (GenValue sym)]
-> SEval sym (GenValue sym)
go0 SEval sym (GenValue sym)
f SEval sym (GenValue sym)
z forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. SBit sym -> GenValue sym
VBit) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValue sym
sym WordValue sym
wv)
GenValue sym
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Eval.Generic.foldlV" [String
"Expected finite sequence"]
where
go0 :: SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> [SEval sym (GenValue sym)]
-> SEval sym (GenValue sym)
go0 SEval sym (GenValue sym)
_f SEval sym (GenValue sym)
a [] = SEval sym (GenValue sym)
a
go0 SEval sym (GenValue sym)
f SEval sym (GenValue sym)
a [SEval sym (GenValue sym)]
bs =
do SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' <- forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
f
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
-> [SEval sym (GenValue sym)]
-> SEval sym (GenValue sym)
go1 SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' SEval sym (GenValue sym)
a [SEval sym (GenValue sym)]
bs
go1 :: (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
-> [SEval sym (GenValue sym)]
-> SEval sym (GenValue sym)
go1 SEval sym (GenValue sym) -> SEval sym (GenValue sym)
_f SEval sym (GenValue sym)
a [] = SEval sym (GenValue sym)
a
go1 SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f SEval sym (GenValue sym)
a (SEval sym (GenValue sym)
b:[SEval sym (GenValue sym)]
bs) =
do SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' <- forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f SEval sym (GenValue sym)
a)
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
-> [SEval sym (GenValue sym)]
-> SEval sym (GenValue sym)
go1 SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f (SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' SEval sym (GenValue sym)
b) [SEval sym (GenValue sym)]
bs
foldl'V :: Backend sym => sym -> Prim sym
foldl'V :: forall sym. Backend sym => sym -> Prim sym
foldl'V sym
sym =
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
_n ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
_a ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
_b ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
f ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
z ->
forall sym. (GenValue sym -> Prim sym) -> Prim sym
PStrict \GenValue sym
v ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
case GenValue sym
v of
VSeq Integer
n SeqMap sym (GenValue sym)
m -> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> [SEval sym (GenValue sym)]
-> SEval sym (GenValue sym)
go0 SEval sym (GenValue sym)
f SEval sym (GenValue sym)
z (forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n SeqMap sym (GenValue sym)
m)
VWord Integer
_n WordValue sym
wv -> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> [SEval sym (GenValue sym)]
-> SEval sym (GenValue sym)
go0 SEval sym (GenValue sym)
f SEval sym (GenValue sym)
z forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. SBit sym -> GenValue sym
VBit) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValue sym
sym WordValue sym
wv)
GenValue sym
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Eval.Generic.foldlV" [String
"Expected finite sequence"]
where
go0 :: SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> [SEval sym (GenValue sym)]
-> SEval sym (GenValue sym)
go0 SEval sym (GenValue sym)
_f SEval sym (GenValue sym)
a [] = SEval sym (GenValue sym)
a
go0 SEval sym (GenValue sym)
f SEval sym (GenValue sym)
a [SEval sym (GenValue sym)]
bs =
do SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' <- forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
f
SEval sym (GenValue sym)
a' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym SEval sym (GenValue sym)
a
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)
a'
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
-> [SEval sym (GenValue sym)]
-> SEval sym (GenValue sym)
go1 SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' SEval sym (GenValue sym)
a' [SEval sym (GenValue sym)]
bs
go1 :: (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
-> [SEval sym (GenValue sym)]
-> SEval sym (GenValue sym)
go1 SEval sym (GenValue sym) -> SEval sym (GenValue sym)
_f SEval sym (GenValue sym)
a [] = SEval sym (GenValue sym)
a
go1 SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f SEval sym (GenValue sym)
a (SEval sym (GenValue sym)
b:[SEval sym (GenValue sym)]
bs) =
do SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' <- forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f SEval sym (GenValue sym)
a)
SEval sym (GenValue sym)
a' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' SEval sym (GenValue sym)
b)
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)
a'
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
-> [SEval sym (GenValue sym)]
-> SEval sym (GenValue sym)
go1 SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f SEval sym (GenValue sym)
a' [SEval sym (GenValue sym)]
bs
scanlV :: forall sym. Backend sym => sym -> Prim sym
scanlV :: forall sym. Backend sym => sym -> Prim sym
scanlV sym
sym =
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
n ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
a ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
_b ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
f ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
z ->
forall sym. (GenValue sym -> Prim sym) -> Prim sym
PStrict \GenValue sym
v ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do SeqMap sym (GenValue sym)
sm <- case GenValue sym
v of
VSeq Integer
_ SeqMap sym (GenValue sym)
m -> Nat'
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
scan Nat'
n SEval sym (GenValue sym)
f SEval sym (GenValue sym)
z SeqMap sym (GenValue sym)
m
VWord Integer
_ WordValue sym
wv -> Nat'
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
scan Nat'
n SEval sym (GenValue sym)
f SEval sym (GenValue sym)
z (forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> WordValue sym -> SeqMap sym (SBit sym)
asBitsMap sym
sym WordValue sym
wv)
VStream SeqMap sym (GenValue sym)
m -> Nat'
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
scan Nat'
n SEval sym (GenValue sym)
f SEval sym (GenValue sym)
z SeqMap sym (GenValue sym)
m
GenValue sym
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Eval.Generic.scanlV" [String
"Expected sequence"]
forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym (Nat' -> Nat' -> Nat'
nAdd (Integer -> Nat'
Nat Integer
1) Nat'
n) TValue
a SeqMap sym (GenValue sym)
sm
where
scan :: Nat' ->
SEval sym (GenValue sym) ->
SEval sym (GenValue sym) ->
(SeqMap sym (GenValue sym)) ->
SEval sym (SeqMap sym (GenValue sym))
scan :: Nat'
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
scan Nat'
n SEval sym (GenValue sym)
f SEval sym (GenValue sym)
z SeqMap sym (GenValue sym)
m =
do (SEval sym (SeqMap sym (GenValue sym))
result, SEval sym (SeqMap sym (GenValue sym)) -> SEval sym ()
fill) <- forall sym a.
Backend sym =>
sym
-> String -> SEval sym (SEval sym a, SEval sym a -> SEval sym ())
sDeclareHole sym
sym String
"scanl"
SEval sym (SeqMap sym (GenValue sym)) -> SEval sym ()
fill forall a b. (a -> b) -> a -> b
$ forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym (Nat' -> Nat' -> Nat'
nAdd (Integer -> Nat'
Nat Integer
1) Nat'
n) forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
if Integer
i forall a. Eq a => a -> a -> Bool
== Integer
0 then SEval sym (GenValue sym)
z
else
do SeqMap sym (GenValue sym)
r <- SEval sym (SeqMap sym (GenValue sym))
result
SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' <- forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
f
SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f'' <- forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
r (Integer
iforall a. Num a => a -> a -> a
-Integer
1))
SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f'' (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
m (Integer
iforall a. Num a => a -> a -> a
-Integer
1))
SEval sym (SeqMap sym (GenValue sym))
result
{-# SPECIALIZE randomV ::
Concrete -> TValue -> Integer -> SEval Concrete (GenValue Concrete)
#-}
randomV :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym)
randomV :: forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
randomV sym
sym TValue
ty Integer
seed =
case forall sym g.
(Backend sym, RandomGen g) =>
sym -> TValue -> Maybe (Gen g sym)
randomValue sym
sym TValue
ty of
Maybe (Gen TFGen sym)
Nothing -> forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
ty
Just Gen TFGen sym
gen ->
let mask64 :: Integer
mask64 = Integer
0xFFFFFFFFFFFFFFFF
unpack :: Integer -> [a]
unpack Integer
s = forall a. Num a => Integer -> a
fromInteger (Integer
s forall a. Bits a => a -> a -> a
.&. Integer
mask64) forall a. a -> [a] -> [a]
: Integer -> [a]
unpack (Integer
s forall a. Bits a => a -> Int -> a
`shiftR` Int
64)
(Word64
a, Word64
b, Word64
c, Word64
d) = case forall a. Int -> [a] -> [a]
take Int
4 (forall {a}. Num a => Integer -> [a]
unpack Integer
seed) of
[Word64
a', Word64
b', Word64
c', Word64
d'] -> (Word64
a', Word64
b', Word64
c', Word64
d')
[Word64]
_ -> forall a. HasCallStack => String -> a
error String
"randomV: impossible (infinite seed is finite)"
in forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Gen TFGen sym
gen Integer
100 forall a b. (a -> b) -> a -> b
$ (Word64, Word64, Word64, Word64) -> TFGen
seedTFGen (Word64
a, Word64
b, Word64
c, Word64
d)
parmapV :: Backend sym => sym -> Prim sym
parmapV :: forall sym. Backend sym => sym -> Prim sym
parmapV sym
sym =
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
_a ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
_b ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_n ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
f ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
xs ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' <- forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
f
GenValue sym
xs' <- SEval sym (GenValue sym)
xs
case GenValue sym
xs' of
VWord Integer
n WordValue sym
w ->
do let m :: SeqMap sym (SBit sym)
m = forall sym.
Backend sym =>
sym -> WordValue sym -> SeqMap sym (SBit sym)
asBitsMap sym
sym WordValue sym
w
SeqMap sym (GenValue sym)
m' <- forall sym a.
Backend sym =>
sym
-> (SEval sym a -> SEval sym (GenValue sym))
-> Integer
-> SeqMap sym a
-> SEval sym (SeqMap sym (GenValue sym))
sparkParMap sym
sym (\SEval sym (SBit sym)
x -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' (forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SBit sym)
x)) Integer
n SeqMap sym (SBit sym)
m
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)
m'))
VSeq Integer
n SeqMap sym (GenValue sym)
m ->
forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a.
Backend sym =>
sym
-> (SEval sym a -> SEval sym (GenValue sym))
-> Integer
-> SeqMap sym a
-> SEval sym (SeqMap sym (GenValue sym))
sparkParMap sym
sym SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' Integer
n SeqMap sym (GenValue sym)
m
GenValue sym
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"parmapV" [String
"expected sequence!"]
sparkParMap ::
Backend sym =>
sym ->
(SEval sym a -> SEval sym (GenValue sym)) ->
Integer ->
SeqMap sym a ->
SEval sym (SeqMap sym (GenValue sym))
sparkParMap :: forall sym a.
Backend sym =>
sym
-> (SEval sym a -> SEval sym (GenValue sym))
-> Integer
-> SeqMap sym a
-> SEval sym (SeqMap sym (GenValue sym))
sparkParMap sym
sym SEval sym a -> SEval sym (GenValue sym)
f Integer
n SeqMap sym a
m =
forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
finiteSeqMap sym
sym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sSpark sym
sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEval sym a -> SEval sym (GenValue sym)
g) (forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n SeqMap sym a
m)
where
g :: SEval sym a -> SEval sym (GenValue sym)
g SEval sym a
x =
do SEval sym (GenValue sym)
z <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (SEval sym a -> SEval sym (GenValue sym)
f SEval sym a
x)
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)
z
SEval sym (GenValue sym)
z
fpConst ::
Backend sym =>
(Integer -> Integer -> SEval sym (SFloat sym)) ->
Prim sym
fpConst :: forall sym.
Backend sym =>
(Integer -> Integer -> SEval sym (SFloat sym)) -> Prim sym
fpConst Integer -> Integer -> SEval sym (SFloat sym)
mk =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
e ->
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \ ~(Nat Integer
p) ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Integer -> SEval sym (SFloat sym)
mk Integer
e Integer
p)
fpBinArithV :: Backend sym => sym -> FPArith2 sym -> Prim sym
fpBinArithV :: forall sym. Backend sym => sym -> FPArith2 sym -> Prim sym
fpBinArithV sym
sym FPArith2 sym
fun =
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_e ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_p ->
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord sym
r ->
forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
x ->
forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
y ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FPArith2 sym
fun sym
sym SWord sym
r SFloat sym
x SFloat sym
y)
fpRndMode, fpRndRNE, fpRndRNA, fpRndRTP, fpRndRTN, fpRndRTZ ::
Backend sym => sym -> SEval sym (SWord sym)
fpRndMode :: forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndMode = forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRNE
fpRndRNE :: forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRNE sym
sym = forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
3 Integer
0
fpRndRNA :: forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRNA sym
sym = forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
3 Integer
1
fpRndRTP :: forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRTP sym
sym = forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
3 Integer
2
fpRndRTN :: forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRTN sym
sym = forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
3 Integer
3
fpRndRTZ :: forall sym. Backend sym => sym -> SEval sym (SWord sym)
fpRndRTZ sym
sym = forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
3 Integer
4
{-# SPECIALIZE genericFloatTable :: Concrete -> Map PrimIdent (Prim Concrete) #-}
genericFloatTable :: Backend sym => sym -> Map PrimIdent (Prim sym)
genericFloatTable :: forall sym. Backend sym => sym -> Map PrimIdent (Prim sym)
genericFloatTable sym
sym =
let ~> :: a -> b -> (a, b)
(~>) = (,) in
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Text
n, Prim sym
v) -> (Text -> PrimIdent
floatPrim Text
n, Prim sym
v))
[ Text
"fpNaN" forall a b. a -> b -> (a, b)
~> forall sym.
Backend sym =>
(Integer -> Integer -> SEval sym (SFloat sym)) -> Prim sym
fpConst (forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SFloat sym)
fpNaN sym
sym)
, Text
"fpPosInf" forall a b. a -> b -> (a, b)
~> forall sym.
Backend sym =>
(Integer -> Integer -> SEval sym (SFloat sym)) -> Prim sym
fpConst (forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SFloat sym)
fpPosInf sym
sym)
, Text
"fpFromBits" forall a b. a -> b -> (a, b)
~> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
e -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p -> forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord sym
w ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> Integer -> SWord sym -> SEval sym (SFloat sym)
fpFromBits sym
sym Integer
e Integer
p SWord sym
w)
, Text
"fpToBits" forall a b. a -> b -> (a, b)
~> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
e -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p -> forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
x -> forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
(forall sym. Integer -> WordValue sym -> GenValue sym
VWord (Integer
eforall a. Num a => a -> a -> a
+Integer
p) 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 -> SFloat sym -> SEval sym (SWord sym)
fpToBits sym
sym SFloat sym
x)
, Text
"=.=" forall a b. a -> b -> (a, b)
~> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
x -> forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
y ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpLogicalEq sym
sym SFloat sym
x SFloat sym
y)
, Text
"fpIsNaN" forall a b. a -> b -> (a, b)
~> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SBit sym)
fpIsNaN sym
sym SFloat sym
x)
, Text
"fpIsInf" forall a b. a -> b -> (a, b)
~> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SBit sym)
fpIsInf sym
sym SFloat sym
x)
, Text
"fpIsZero" forall a b. a -> b -> (a, b)
~> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SBit sym)
fpIsZero sym
sym SFloat sym
x)
, Text
"fpIsNeg" forall a b. a -> b -> (a, b)
~> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SBit sym)
fpIsNeg sym
sym SFloat sym
x)
, Text
"fpIsNormal" forall a b. a -> b -> (a, b)
~> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SBit sym)
fpIsNorm sym
sym SFloat sym
x)
, Text
"fpIsSubnormal" forall a b. a -> b -> (a, b)
~> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SBit sym -> GenValue sym
VBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SBit sym)
fpIsSubnorm sym
sym SFloat sym
x)
, Text
"fpAdd" forall a b. a -> b -> (a, b)
~> forall sym. Backend sym => sym -> FPArith2 sym -> Prim sym
fpBinArithV sym
sym forall sym. Backend sym => FPArith2 sym
fpPlus
, Text
"fpSub" forall a b. a -> b -> (a, b)
~> forall sym. Backend sym => sym -> FPArith2 sym -> Prim sym
fpBinArithV sym
sym forall sym. Backend sym => FPArith2 sym
fpMinus
, Text
"fpMul" forall a b. a -> b -> (a, b)
~> forall sym. Backend sym => sym -> FPArith2 sym -> Prim sym
fpBinArithV sym
sym forall sym. Backend sym => FPArith2 sym
fpMult
, Text
"fpDiv" forall a b. a -> b -> (a, b)
~> forall sym. Backend sym => sym -> FPArith2 sym -> Prim sym
fpBinArithV sym
sym forall sym. Backend sym => FPArith2 sym
fpDiv
, Text
"fpFMA" forall a b. a -> b -> (a, b)
~> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord sym
r ->
forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
x -> forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
y -> forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
z ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> SWord sym
-> SFloat sym
-> SFloat sym
-> SFloat sym
-> SEval sym (SFloat sym)
fpFMA sym
sym SWord sym
r SFloat sym
x SFloat sym
y SFloat sym
z)
, Text
"fpAbs" forall a b. a -> b -> (a, b)
~> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ ->
forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SFloat sym)
fpAbs sym
sym SFloat sym
x)
, Text
"fpSqrt" forall a b. a -> b -> (a, b)
~> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ ->
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord sym
r -> forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SWord sym -> SFloat sym -> SEval sym (SFloat sym)
fpSqrt sym
sym SWord sym
r SFloat sym
x)
, Text
"fpToRational" forall a b. a -> b -> (a, b)
~>
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_e -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_p -> forall sym. (SFloat sym -> Prim sym) -> Prim sym
PFloatFun \SFloat sym
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym. SRational sym -> GenValue sym
VRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SFloat sym -> SEval sym (SRational sym)
fpToRational sym
sym SFloat sym
x)
, Text
"fpFromRational" forall a b. a -> b -> (a, b)
~>
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
e -> forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p -> forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord sym
r -> forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do SRational sym
rat <- forall sym. GenValue sym -> SRational sym
fromVRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
x
forall sym. SFloat sym -> GenValue sym
VFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SWord sym
-> SRational sym
-> SEval sym (SFloat sym)
fpFromRational sym
sym Integer
e Integer
p SWord sym
r SRational sym
rat
]
{-# SPECIALIZE genericPrimTable :: Concrete -> IO EvalOpts -> Map PrimIdent (Prim Concrete) #-}
genericPrimTable :: Backend sym => sym -> IO EvalOpts -> Map PrimIdent (Prim sym)
genericPrimTable :: forall sym.
Backend sym =>
sym -> IO EvalOpts -> Map PrimIdent (Prim sym)
genericPrimTable sym
sym IO EvalOpts
getEOpts =
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Text
n, Prim sym
v) -> (Text -> PrimIdent
prelPrim Text
n, Prim sym
v))
[
(Text
"True" , forall sym. GenValue sym -> Prim sym
PVal forall a b. (a -> b) -> a -> b
$ forall sym. SBit sym -> GenValue sym
VBit (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
True))
, (Text
"False" , forall sym. GenValue sym -> Prim sym
PVal forall a b. (a -> b) -> a -> b
$ forall sym. SBit sym -> GenValue sym
VBit (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
False))
, (Text
"number" , {-# SCC "Prelude::number" #-}
forall sym. Backend sym => sym -> Prim sym
ecNumberV sym
sym)
, (Text
"ratio" , {-# SCC "Prelude::ratio" #-}
forall sym. Backend sym => sym -> Prim sym
ratioV sym
sym)
, (Text
"fraction" , forall sym. Backend sym => sym -> Prim sym
ecFractionV sym
sym)
, (Text
"zero" , {-# SCC "Prelude::zero" #-}
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
ty ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV sym
sym TValue
ty))
, (Text
"&&" , {-# SCC "Prelude::(&&)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
andV sym
sym))
, (Text
"||" , {-# SCC "Prelude::(||)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
orV sym
sym))
, (Text
"^" , {-# SCC "Prelude::(^)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
xorV sym
sym))
, (Text
"complement" , {-# SCC "Prelude::complement" #-}
forall sym. Backend sym => Unary sym -> Prim sym
unary (forall sym. Backend sym => sym -> Unary sym
complementV sym
sym))
, (Text
"fromInteger", {-# SCC "Prelude::fromInteger" #-}
forall sym. Backend sym => sym -> Prim sym
fromIntegerV sym
sym)
, (Text
"+" , {-# SCC "Prelude::(+)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
addV sym
sym))
, (Text
"-" , {-# SCC "Prelude::(-)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
subV sym
sym))
, (Text
"*" , {-# SCC "Prelude::(*)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
mulV sym
sym))
, (Text
"negate" , {-# SCC "Prelude::negate" #-}
forall sym. Backend sym => Unary sym -> Prim sym
unary (forall sym. Backend sym => sym -> Unary sym
negateV sym
sym))
, (Text
"toInteger" , {-# SCC "Prelude::toInteger" #-}
forall sym. Backend sym => sym -> Prim sym
toIntegerV sym
sym)
, (Text
"/" , {-# SCC "Prelude::(/)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
divV sym
sym))
, (Text
"%" , {-# SCC "Prelude::(%)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
modV sym
sym))
, (Text
"^^" , {-# SCC "Prelude::(^^)" #-}
forall sym. Backend sym => sym -> Prim sym
expV sym
sym)
, (Text
"infFrom" , {-# SCC "Prelude::infFrom" #-}
forall sym. Backend sym => sym -> Prim sym
infFromV sym
sym)
, (Text
"infFromThen", {-# SCC "Prelude::infFromThen" #-}
forall sym. Backend sym => sym -> Prim sym
infFromThenV sym
sym)
, (Text
"recip" , {-# SCC "Prelude::recip" #-}
forall sym. Backend sym => sym -> Prim sym
recipV sym
sym)
, (Text
"/." , {-# SCC "Prelude::(/.)" #-}
forall sym. Backend sym => sym -> Prim sym
fieldDivideV sym
sym)
, (Text
"floor" , {-# SCC "Prelude::floor" #-}
forall sym. Backend sym => Unary sym -> Prim sym
unary (forall sym. Backend sym => sym -> Unary sym
floorV sym
sym))
, (Text
"ceiling" , {-# SCC "Prelude::ceiling" #-}
forall sym. Backend sym => Unary sym -> Prim sym
unary (forall sym. Backend sym => sym -> Unary sym
ceilingV sym
sym))
, (Text
"trunc" , {-# SCC "Prelude::trunc" #-}
forall sym. Backend sym => Unary sym -> Prim sym
unary (forall sym. Backend sym => sym -> Unary sym
truncV sym
sym))
, (Text
"roundAway" , {-# SCC "Prelude::roundAway" #-}
forall sym. Backend sym => Unary sym -> Prim sym
unary (forall sym. Backend sym => sym -> Unary sym
roundAwayV sym
sym))
, (Text
"roundToEven", {-# SCC "Prelude::roundToEven" #-}
forall sym. Backend sym => Unary sym -> Prim sym
unary (forall sym. Backend sym => sym -> Unary sym
roundToEvenV sym
sym))
, (Text
"toSignedInteger"
, {-# SCC "Prelude::toSignedInteger" #-}
forall sym. Backend sym => sym -> Prim sym
toSignedIntegerV sym
sym)
, (Text
"/$" , {-# SCC "Prelude::(/$)" #-}
forall sym. Backend sym => sym -> Prim sym
sdivV sym
sym)
, (Text
"%$" , {-# SCC "Prelude::(%$)" #-}
forall sym. Backend sym => sym -> Prim sym
smodV sym
sym)
, (Text
"lg2" , {-# SCC "Prelude::lg2" #-}
forall sym. Backend sym => sym -> Prim sym
lg2V sym
sym)
, (Text
"<" , {-# SCC "Prelude::(<)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
lessThanV sym
sym))
, (Text
">" , {-# SCC "Prelude::(>)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
greaterThanV sym
sym))
, (Text
"<=" , {-# SCC "Prelude::(<=)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
lessThanEqV sym
sym))
, (Text
">=" , {-# SCC "Prelude::(>=)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
greaterThanEqV sym
sym))
, (Text
"==" , {-# SCC "Prelude::(==)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
eqV sym
sym))
, (Text
"!=" , {-# SCC "Prelude::(!=)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
distinctV sym
sym))
, (Text
"<$" , {-# SCC "Prelude::(<$)" #-}
forall sym. Backend sym => Binary sym -> Prim sym
binary (forall sym. Backend sym => sym -> Binary sym
signedLessThanV sym
sym))
, (Text
"fromTo" , {-# SCC "Prelude::fromTo" #-}
forall sym. Backend sym => sym -> Prim sym
fromToV sym
sym)
, (Text
"fromThenTo" , {-# SCC "Prelude::fromThenTo" #-}
forall sym. Backend sym => sym -> Prim sym
fromThenToV sym
sym)
, (Text
"fromToLessThan"
, {-# SCC "Prelude::fromToLessThan" #-}
forall sym. Backend sym => sym -> Prim sym
fromToLessThanV sym
sym)
, (Text
"fromToBy" , {-# SCC "Prelude::fromToBy" #-}
forall sym. Backend sym => sym -> Prim sym
fromToByV sym
sym)
, (Text
"fromToByLessThan",
{-# SCC "Prelude::fromToByLessThan" #-}
forall sym. Backend sym => sym -> Prim sym
fromToByLessThanV sym
sym)
, (Text
"fromToDownBy", {-# SCC "Prelude::fromToDownBy" #-}
forall sym. Backend sym => sym -> Prim sym
fromToDownByV sym
sym)
, (Text
"fromToDownByGreaterThan"
, {-# SCC "Prelude::fromToDownByGreaterThan" #-}
forall sym. Backend sym => sym -> Prim sym
fromToDownByGreaterThanV sym
sym)
, (Text
"#" , {-# SCC "Prelude::(#)" #-}
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
front ->
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
back ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
elty ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
l ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
r ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim forall a b. (a -> b) -> a -> b
$ forall sym.
Backend sym =>
sym
-> Integer
-> Nat'
-> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
ccatV sym
sym Integer
front Nat'
back TValue
elty SEval sym (GenValue sym)
l SEval sym (GenValue sym)
r)
, (Text
"join" , {-# SCC "Prelude::join" #-}
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
parts ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
each ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
a ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim forall a b. (a -> b) -> a -> b
$ forall sym.
Backend sym =>
sym
-> Nat'
-> Integer
-> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
joinV sym
sym Nat'
parts Integer
each TValue
a SEval sym (GenValue sym)
x)
, (Text
"split" , {-# SCC "Prelude::split" #-}
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
parts ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
each ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
a ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
val ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim forall a b. (a -> b) -> a -> b
$ forall sym.
Backend sym =>
sym
-> Nat'
-> Integer
-> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
splitV sym
sym Nat'
parts Integer
each TValue
a SEval sym (GenValue sym)
val)
, (Text
"take" , {-# SCC "Preldue::take" #-}
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
front ->
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
back ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
a ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
xs ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim forall a b. (a -> b) -> a -> b
$ forall sym.
Backend sym =>
sym
-> Nat'
-> Nat'
-> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
takeV sym
sym Nat'
front Nat'
back TValue
a SEval sym (GenValue sym)
xs)
, (Text
"drop" , {-# SCC "Preldue::drop" #-}
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
front ->
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
back ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
a ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
xs ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim forall a b. (a -> b) -> a -> b
$ forall sym.
Backend sym =>
sym
-> Integer
-> Nat'
-> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
dropV sym
sym Integer
front Nat'
back TValue
a SEval sym (GenValue sym)
xs)
, (Text
"reverse" , {-# SCC "Prelude::reverse" #-}
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
a ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
b ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
xs ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim forall a b. (a -> b) -> a -> b
$ forall sym.
Backend sym =>
sym
-> Integer
-> TValue
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
reverseV sym
sym Integer
a TValue
b SEval sym (GenValue sym)
xs)
, (Text
"transpose" , {-# SCC "Prelude::transpose" #-}
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
a ->
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
b ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
c ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
xs ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim forall a b. (a -> b) -> a -> b
$ forall sym.
Backend sym =>
sym
-> Nat'
-> Nat'
-> TValue
-> GenValue sym
-> SEval sym (GenValue sym)
transposeV sym
sym Nat'
a Nat'
b TValue
c forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
xs)
, (Text
"<<" , {-# SCC "Prelude::(<<)" #-}
forall sym.
Backend sym =>
sym
-> String
-> (sym
-> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Prim sym
logicShift sym
sym String
"<<" forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink
(forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordShiftLeft sym
sym) (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordShiftRight sym
sym)
Nat' -> Integer -> Integer -> Maybe Integer
shiftLeftReindex Nat' -> Integer -> Integer -> Maybe Integer
shiftRightReindex)
, (Text
">>" , {-# SCC "Prelude::(>>)" #-}
forall sym.
Backend sym =>
sym
-> String
-> (sym
-> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Prim sym
logicShift sym
sym String
">>" forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
shiftShrink
(forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordShiftRight sym
sym) (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordShiftLeft sym
sym)
Nat' -> Integer -> Integer -> Maybe Integer
shiftRightReindex Nat' -> Integer -> Integer -> Maybe Integer
shiftLeftReindex)
, (Text
"<<<" , {-# SCC "Prelude::(<<<)" #-}
forall sym.
Backend sym =>
sym
-> String
-> (sym
-> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Prim sym
logicShift sym
sym String
"<<<" forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
rotateShrink
(forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordRotateLeft sym
sym) (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordRotateRight sym
sym)
Nat' -> Integer -> Integer -> Maybe Integer
rotateLeftReindex Nat' -> Integer -> Integer -> Maybe Integer
rotateRightReindex)
, (Text
">>>" , {-# SCC "Prelude::(>>>)" #-}
forall sym.
Backend sym =>
sym
-> String
-> (sym
-> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Prim sym
logicShift sym
sym String
">>>" forall sym.
Backend sym =>
sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
rotateShrink
(forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordRotateRight sym
sym) (forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordRotateLeft sym
sym)
Nat' -> Integer -> Integer -> Maybe Integer
rotateRightReindex Nat' -> Integer -> Integer -> Maybe Integer
rotateLeftReindex)
, (Text
">>$" , {-# SCC "Prelude::(>>$)" #-}
forall sym. Backend sym => sym -> Prim sym
sshrV sym
sym)
, (Text
"error" , {-# SCC "Prelude::error" #-}
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
a ->
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_ ->
forall sym. (GenValue sym -> Prim sym) -> Prim sym
PStrict \GenValue sym
s ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (forall sym.
Backend sym =>
sym -> TValue -> String -> SEval sym (GenValue sym)
errorV sym
sym TValue
a forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. Backend sym => sym -> GenValue sym -> SEval sym String
valueToString sym
sym GenValue sym
s))
, (Text
"trace" , {-# SCC "Prelude::trace" #-}
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
_n ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
_a ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
_b ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
s ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
x ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
y ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do String
msg <- forall sym. Backend sym => sym -> GenValue sym -> SEval sym String
valueToString sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
s
EvalOpts { PPOpts
evalPPOpts :: EvalOpts -> PPOpts
evalPPOpts :: PPOpts
evalPPOpts, Logger
evalLogger :: EvalOpts -> Logger
evalLogger :: Logger
evalLogger } <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO EvalOpts
getEOpts
Doc
doc <- forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
ppValue sym
sym PPOpts
evalPPOpts forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
x
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. Show a => Logger -> a -> IO ()
logPrint Logger
evalLogger
forall a b. (a -> b) -> a -> b
$ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
msg then Doc
doc else String -> Doc
text String
msg Doc -> Doc -> Doc
<+> Doc
doc
SEval sym (GenValue sym)
y)
, (Text
"random" , {-# SCC "Prelude::random" #-}
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
a ->
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \SWord sym
x ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
case forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
x of
Just (Integer
_,Integer
i) -> forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
randomV sym
sym TValue
a Integer
i
Maybe (Integer, Integer)
Nothing -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a e. Exception e => e -> a
X.throw (String -> Unsupported
UnsupportedSymbolicOp String
"random")))
, (Text
"foldl" , {-# SCC "Prelude::foldl" #-}
forall sym. Backend sym => sym -> Prim sym
foldlV sym
sym)
, (Text
"foldl'" , {-# SCC "Prelude::foldl'" #-}
forall sym. Backend sym => sym -> Prim sym
foldl'V sym
sym)
, (Text
"scanl" , {-# SCC "Prelude::scanl" #-}
forall sym. Backend sym => sym -> Prim sym
scanlV sym
sym)
, (Text
"deepseq" , {-# SCC "Prelude::deepseq" #-}
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
_a ->
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly \TValue
_b ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
x ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval sym (GenValue sym)
y ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim do ()
_ <- 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)
x
SEval sym (GenValue sym)
y)
, (Text
"parmap" , {-# SCC "Prelude::parmap" #-}
forall sym. Backend sym => sym -> Prim sym
parmapV sym
sym)
, (Text
"fromZ" , {-# SCC "Prelude::fromZ" #-}
forall sym. Backend sym => sym -> Prim sym
fromZV sym
sym)
]