{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Copilot.Theorem.What4
( prove, Solver(..), SatResult(..)
) where
import qualified Copilot.Core.Expr as CE
import qualified Copilot.Core.Operators as CE
import qualified Copilot.Core.Spec as CS
import qualified Copilot.Core.Type as CT
import qualified Copilot.Core.Type.Array as CT
import qualified What4.Config as WC
import qualified What4.Expr.Builder as WB
import qualified What4.Expr.GroundEval as WG
import qualified What4.Interface as WI
import qualified What4.BaseTypes as WT
import qualified What4.Solver as WS
import qualified What4.Solver.DReal as WS
import qualified Control.Monad.Fail as Fail
import Control.Monad.State
import qualified Data.BitVector.Sized as BV
import Data.Foldable (foldrM)
import Data.List (elemIndex)
import Data.Maybe (fromJust)
import qualified Data.Map as Map
import Data.Parameterized.Classes
import Data.Parameterized.Context hiding (zipWithM)
import Data.Parameterized.NatRepr
import Data.Parameterized.Nonce
import Data.Parameterized.Some
import Data.Parameterized.SymbolRepr
import qualified Data.Parameterized.Vector as V
import Data.Word
import LibBF ( bfToDouble
, bfFromDouble
, bfPosZero
, pattern NearEven )
import GHC.TypeNats (KnownNat)
import qualified Panic as Panic
fpRM :: WI.RoundingMode
fpRM :: RoundingMode
fpRM = RoundingMode
WI.RNE
data BuilderState a = EmptyState
data Solver = CVC4 | DReal | Yices | Z3
data SatResult = Valid | Invalid | Unknown
deriving Int -> SatResult -> ShowS
[SatResult] -> ShowS
SatResult -> String
(Int -> SatResult -> ShowS)
-> (SatResult -> String)
-> ([SatResult] -> ShowS)
-> Show SatResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SatResult] -> ShowS
$cshowList :: [SatResult] -> ShowS
show :: SatResult -> String
$cshow :: SatResult -> String
showsPrec :: Int -> SatResult -> ShowS
$cshowsPrec :: Int -> SatResult -> ShowS
Show
type CounterExample = [(String, Some CopilotValue)]
prove :: Solver
-> CS.Spec
-> IO [(CE.Name, SatResult)]
prove :: Solver -> Spec -> IO [(String, SatResult)]
prove Solver
solver Spec
spec = do
Some NonceGenerator IO x
ng <- IO (Some (NonceGenerator IO))
newIONonceGenerator
ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym <- FloatModeRepr 'FloatIEEE
-> BuilderState x
-> NonceGenerator IO x
-> IO (ExprBuilder x BuilderState (Flags 'FloatIEEE))
forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
WB.newExprBuilder FloatModeRepr 'FloatIEEE
WB.FloatIEEERepr BuilderState x
forall a. BuilderState a
EmptyState NonceGenerator IO x
ng
case Solver
solver of
Solver
CVC4 -> [ConfigDesc] -> Config -> IO ()
WC.extendConfig [ConfigDesc]
WS.cvc4Options (ExprBuilder x BuilderState (Flags 'FloatIEEE) -> Config
forall sym. IsExprBuilder sym => sym -> Config
WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym)
Solver
DReal -> [ConfigDesc] -> Config -> IO ()
WC.extendConfig [ConfigDesc]
WS.drealOptions (ExprBuilder x BuilderState (Flags 'FloatIEEE) -> Config
forall sym. IsExprBuilder sym => sym -> Config
WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym)
Solver
Yices -> [ConfigDesc] -> Config -> IO ()
WC.extendConfig [ConfigDesc]
WS.yicesOptions (ExprBuilder x BuilderState (Flags 'FloatIEEE) -> Config
forall sym. IsExprBuilder sym => sym -> Config
WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym)
Solver
Z3 -> [ConfigDesc] -> Config -> IO ()
WC.extendConfig [ConfigDesc]
WS.z3Options (ExprBuilder x BuilderState (Flags 'FloatIEEE) -> Config
forall sym. IsExprBuilder sym => sym -> Config
WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym)
let streamMap :: Map Int Stream
streamMap = [(Int, Stream)] -> Map Int Stream
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Stream)] -> Map Int Stream)
-> [(Int, Stream)] -> Map Int Stream
forall a b. (a -> b) -> a -> b
$
(\Stream
stream -> (Stream -> Int
CS.streamId Stream
stream, Stream
stream)) (Stream -> (Int, Stream)) -> [Stream] -> [(Int, Stream)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec -> [Stream]
CS.specStreams Spec
spec
ExprSymFn
x ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
pow <- ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> SolverSymbol
-> Assignment
BaseTypeRepr ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
-> BaseTypeRepr BaseRealType
-> IO
(SymFn
(ExprBuilder x BuilderState (Flags 'FloatIEEE))
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType)
forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
WI.freshTotalUninterpFn ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym (String -> SolverSymbol
WI.safeSymbol String
"pow") Assignment
BaseTypeRepr ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr BaseTypeRepr BaseRealType
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
ExprSymFn
x ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logb <- ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> SolverSymbol
-> Assignment
BaseTypeRepr ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
-> BaseTypeRepr BaseRealType
-> IO
(SymFn
(ExprBuilder x BuilderState (Flags 'FloatIEEE))
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType)
forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
WI.freshTotalUninterpFn ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym (String -> SolverSymbol
WI.safeSymbol String
"logb") Assignment
BaseTypeRepr ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr BaseTypeRepr BaseRealType
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
let st :: TransState x
st = Map (String, Int) (XExpr x)
-> Map (String, Int) (XExpr x)
-> Map (Int, Int) (XExpr x)
-> Map Int Stream
-> ExprSymFn
x ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
x ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> TransState x
forall t.
Map (String, Int) (XExpr t)
-> Map (String, Int) (XExpr t)
-> Map (Int, Int) (XExpr t)
-> Map Int Stream
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> TransState t
TransState Map (String, Int) (XExpr x)
forall k a. Map k a
Map.empty Map (String, Int) (XExpr x)
forall k a. Map k a
Map.empty Map (Int, Int) (XExpr x)
forall k a. Map k a
Map.empty Map Int Stream
streamMap ExprSymFn
x ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
pow ExprSymFn
x ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logb
let proveProperties :: TransM x [(String, SatResult)]
proveProperties = [Property]
-> (Property -> TransM x (String, SatResult))
-> TransM x [(String, SatResult)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Spec -> [Property]
CS.specProperties Spec
spec) ((Property -> TransM x (String, SatResult))
-> TransM x [(String, SatResult)])
-> (Property -> TransM x (String, SatResult))
-> TransM x [(String, SatResult)]
forall a b. (a -> b) -> a -> b
$ \Property
pr -> do
let bufLen :: Stream -> Int
bufLen (CS.Stream Int
_ [a]
buf Expr a
_ Type a
_) = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
buf
maxBufLen :: Int
maxBufLen = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (Stream -> Int
bufLen (Stream -> Int) -> [Stream] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec -> [Stream]
CS.specStreams Spec
spec))
[Expr x BaseBoolType]
prefix <- [Int]
-> (Int -> TransM x (Expr x BaseBoolType))
-> TransM x [Expr x BaseBoolType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int
0 .. Int
maxBufLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] ((Int -> TransM x (Expr x BaseBoolType))
-> TransM x [Expr x BaseBoolType])
-> (Int -> TransM x (Expr x BaseBoolType))
-> TransM x [Expr x BaseBoolType]
forall a b. (a -> b) -> a -> b
$ \Int
k -> do
XBool Expr x BaseBoolType
p <- ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> Int -> Expr Bool -> TransM x (XExpr x)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExprAt ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym Int
k (Property -> Expr Bool
CS.propertyExpr Property
pr)
Expr x BaseBoolType -> TransM x (Expr x BaseBoolType)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr x BaseBoolType
p
XBool Expr x BaseBoolType
p <- ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> Int -> Expr Bool -> TransM x (XExpr x)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym Int
0 (Property -> Expr Bool
CS.propertyExpr Property
pr)
Expr x BaseBoolType
p_and_prefix <- IO (Expr x BaseBoolType) -> TransM x (Expr x BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Expr x BaseBoolType) -> TransM x (Expr x BaseBoolType))
-> IO (Expr x BaseBoolType) -> TransM x (Expr x BaseBoolType)
forall a b. (a -> b) -> a -> b
$ (Expr x BaseBoolType
-> Expr x BaseBoolType -> IO (Expr x BaseBoolType))
-> Expr x BaseBoolType
-> [Expr x BaseBoolType]
-> IO (Expr x BaseBoolType)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> Pred (ExprBuilder x BuilderState (Flags 'FloatIEEE))
-> Pred (ExprBuilder x BuilderState (Flags 'FloatIEEE))
-> IO (Pred (ExprBuilder x BuilderState (Flags 'FloatIEEE)))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.andPred ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym) Expr x BaseBoolType
p [Expr x BaseBoolType]
prefix
Expr x BaseBoolType
not_p_and_prefix <- IO (Expr x BaseBoolType) -> TransM x (Expr x BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Expr x BaseBoolType) -> TransM x (Expr x BaseBoolType))
-> IO (Expr x BaseBoolType) -> TransM x (Expr x BaseBoolType)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> Pred (ExprBuilder x BuilderState (Flags 'FloatIEEE))
-> IO (Pred (ExprBuilder x BuilderState (Flags 'FloatIEEE)))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym Expr x BaseBoolType
Pred (ExprBuilder x BuilderState (Flags 'FloatIEEE))
p_and_prefix
let clauses :: [Expr x BaseBoolType]
clauses = [Expr x BaseBoolType
not_p_and_prefix]
case Solver
solver of
Solver
CVC4 -> IO (String, SatResult) -> TransM x (String, SatResult)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, SatResult) -> TransM x (String, SatResult))
-> IO (String, SatResult) -> TransM x (String, SatResult)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> LogData
-> [Expr x BaseBoolType]
-> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
-> IO (String, SatResult))
-> IO (String, SatResult)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
-> IO a)
-> IO a
WS.runCVC4InOverride ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym LogData
WS.defaultLogData [Expr x BaseBoolType]
clauses ((SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
-> IO (String, SatResult))
-> IO (String, SatResult))
-> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
-> IO (String, SatResult))
-> IO (String, SatResult)
forall a b. (a -> b) -> a -> b
$ \case
WS.Sat (GroundEvalFn x
_ge, Maybe (ExprRangeBindings x)
_) -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
WS.Unsat ()
_ -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
Solver
DReal -> IO (String, SatResult) -> TransM x (String, SatResult)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, SatResult) -> TransM x (String, SatResult))
-> IO (String, SatResult) -> TransM x (String, SatResult)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> LogData
-> [Expr x BaseBoolType]
-> (SatResult (WriterConn x (Writer DReal), DRealBindings) ()
-> IO (String, SatResult))
-> IO (String, SatResult)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (WriterConn t (Writer DReal), DRealBindings) ()
-> IO a)
-> IO a
WS.runDRealInOverride ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym LogData
WS.defaultLogData [Expr x BaseBoolType]
clauses ((SatResult (WriterConn x (Writer DReal), DRealBindings) ()
-> IO (String, SatResult))
-> IO (String, SatResult))
-> (SatResult (WriterConn x (Writer DReal), DRealBindings) ()
-> IO (String, SatResult))
-> IO (String, SatResult)
forall a b. (a -> b) -> a -> b
$ \case
WS.Sat (WriterConn x (Writer DReal)
_ge, DRealBindings
_) -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
WS.Unsat ()
_ -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
SatResult (WriterConn x (Writer DReal), DRealBindings) ()
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
Solver
Yices -> IO (String, SatResult) -> TransM x (String, SatResult)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, SatResult) -> TransM x (String, SatResult))
-> IO (String, SatResult) -> TransM x (String, SatResult)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> LogData
-> [Expr x BaseBoolType]
-> (SatResult (GroundEvalFn x) () -> IO (String, SatResult))
-> IO (String, SatResult)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t) () -> IO a)
-> IO a
WS.runYicesInOverride ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym LogData
WS.defaultLogData [Expr x BaseBoolType]
clauses ((SatResult (GroundEvalFn x) () -> IO (String, SatResult))
-> IO (String, SatResult))
-> (SatResult (GroundEvalFn x) () -> IO (String, SatResult))
-> IO (String, SatResult)
forall a b. (a -> b) -> a -> b
$ \case
WS.Sat GroundEvalFn x
_ge -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
WS.Unsat ()
_ -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
SatResult (GroundEvalFn x) ()
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
Solver
Z3 -> IO (String, SatResult) -> TransM x (String, SatResult)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, SatResult) -> TransM x (String, SatResult))
-> IO (String, SatResult) -> TransM x (String, SatResult)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> LogData
-> [Expr x BaseBoolType]
-> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
-> IO (String, SatResult))
-> IO (String, SatResult)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
-> IO a)
-> IO a
WS.runZ3InOverride ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym LogData
WS.defaultLogData [Expr x BaseBoolType]
clauses ((SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
-> IO (String, SatResult))
-> IO (String, SatResult))
-> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
-> IO (String, SatResult))
-> IO (String, SatResult)
forall a b. (a -> b) -> a -> b
$ \case
WS.Sat (GroundEvalFn x
_ge, Maybe (ExprRangeBindings x)
_) -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
WS.Unsat ()
_ -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
([(String, SatResult)]
res, TransState x
_) <- StateT (TransState x) IO [(String, SatResult)]
-> TransState x -> IO ([(String, SatResult)], TransState x)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (TransM x [(String, SatResult)]
-> StateT (TransState x) IO [(String, SatResult)]
forall t a. TransM t a -> StateT (TransState t) IO a
unTransM TransM x [(String, SatResult)]
proveProperties) TransState x
st
[(String, SatResult)] -> IO [(String, SatResult)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(String, SatResult)]
res
data TransState t = TransState {
TransState t -> Map (String, Int) (XExpr t)
externVars :: Map.Map (CE.Name, Int) (XExpr t),
TransState t -> Map (String, Int) (XExpr t)
externVarsAt :: Map.Map (CE.Name, Int) (XExpr t),
TransState t -> Map (Int, Int) (XExpr t)
streamConstants :: Map.Map (CE.Id, Int) (XExpr t),
TransState t -> Map Int Stream
streams :: Map.Map CE.Id CS.Stream,
TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
pow :: WB.ExprSymFn t
(EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
WT.BaseRealType,
TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logb :: WB.ExprSymFn t
(EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
WT.BaseRealType
}
newtype TransM t a = TransM { TransM t a -> StateT (TransState t) IO a
unTransM :: StateT (TransState t) IO a }
deriving ( a -> TransM t b -> TransM t a
(a -> b) -> TransM t a -> TransM t b
(forall a b. (a -> b) -> TransM t a -> TransM t b)
-> (forall a b. a -> TransM t b -> TransM t a)
-> Functor (TransM t)
forall a b. a -> TransM t b -> TransM t a
forall a b. (a -> b) -> TransM t a -> TransM t b
forall t a b. a -> TransM t b -> TransM t a
forall t a b. (a -> b) -> TransM t a -> TransM t b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> TransM t b -> TransM t a
$c<$ :: forall t a b. a -> TransM t b -> TransM t a
fmap :: (a -> b) -> TransM t a -> TransM t b
$cfmap :: forall t a b. (a -> b) -> TransM t a -> TransM t b
Functor
, Functor (TransM t)
a -> TransM t a
Functor (TransM t)
-> (forall a. a -> TransM t a)
-> (forall a b. TransM t (a -> b) -> TransM t a -> TransM t b)
-> (forall a b c.
(a -> b -> c) -> TransM t a -> TransM t b -> TransM t c)
-> (forall a b. TransM t a -> TransM t b -> TransM t b)
-> (forall a b. TransM t a -> TransM t b -> TransM t a)
-> Applicative (TransM t)
TransM t a -> TransM t b -> TransM t b
TransM t a -> TransM t b -> TransM t a
TransM t (a -> b) -> TransM t a -> TransM t b
(a -> b -> c) -> TransM t a -> TransM t b -> TransM t c
forall t. Functor (TransM t)
forall a. a -> TransM t a
forall t a. a -> TransM t a
forall a b. TransM t a -> TransM t b -> TransM t a
forall a b. TransM t a -> TransM t b -> TransM t b
forall a b. TransM t (a -> b) -> TransM t a -> TransM t b
forall t a b. TransM t a -> TransM t b -> TransM t a
forall t a b. TransM t a -> TransM t b -> TransM t b
forall t a b. TransM t (a -> b) -> TransM t a -> TransM t b
forall a b c.
(a -> b -> c) -> TransM t a -> TransM t b -> TransM t c
forall t a b c.
(a -> b -> c) -> TransM t a -> TransM t b -> TransM t c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: TransM t a -> TransM t b -> TransM t a
$c<* :: forall t a b. TransM t a -> TransM t b -> TransM t a
*> :: TransM t a -> TransM t b -> TransM t b
$c*> :: forall t a b. TransM t a -> TransM t b -> TransM t b
liftA2 :: (a -> b -> c) -> TransM t a -> TransM t b -> TransM t c
$cliftA2 :: forall t a b c.
(a -> b -> c) -> TransM t a -> TransM t b -> TransM t c
<*> :: TransM t (a -> b) -> TransM t a -> TransM t b
$c<*> :: forall t a b. TransM t (a -> b) -> TransM t a -> TransM t b
pure :: a -> TransM t a
$cpure :: forall t a. a -> TransM t a
$cp1Applicative :: forall t. Functor (TransM t)
Applicative
, Applicative (TransM t)
a -> TransM t a
Applicative (TransM t)
-> (forall a b. TransM t a -> (a -> TransM t b) -> TransM t b)
-> (forall a b. TransM t a -> TransM t b -> TransM t b)
-> (forall a. a -> TransM t a)
-> Monad (TransM t)
TransM t a -> (a -> TransM t b) -> TransM t b
TransM t a -> TransM t b -> TransM t b
forall t. Applicative (TransM t)
forall a. a -> TransM t a
forall t a. a -> TransM t a
forall a b. TransM t a -> TransM t b -> TransM t b
forall a b. TransM t a -> (a -> TransM t b) -> TransM t b
forall t a b. TransM t a -> TransM t b -> TransM t b
forall t a b. TransM t a -> (a -> TransM t b) -> TransM t b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> TransM t a
$creturn :: forall t a. a -> TransM t a
>> :: TransM t a -> TransM t b -> TransM t b
$c>> :: forall t a b. TransM t a -> TransM t b -> TransM t b
>>= :: TransM t a -> (a -> TransM t b) -> TransM t b
$c>>= :: forall t a b. TransM t a -> (a -> TransM t b) -> TransM t b
$cp1Monad :: forall t. Applicative (TransM t)
Monad
, Monad (TransM t)
Monad (TransM t)
-> (forall a. IO a -> TransM t a) -> MonadIO (TransM t)
IO a -> TransM t a
forall t. Monad (TransM t)
forall a. IO a -> TransM t a
forall t a. IO a -> TransM t a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> TransM t a
$cliftIO :: forall t a. IO a -> TransM t a
$cp1MonadIO :: forall t. Monad (TransM t)
MonadIO
, MonadState (TransState t)
)
instance Fail.MonadFail (TransM t) where
fail :: String -> TransM t a
fail = String -> TransM t a
forall a. HasCallStack => String -> a
error
data CopilotWhat4 = CopilotWhat4
instance Panic.PanicComponent CopilotWhat4 where
panicComponentName :: CopilotWhat4 -> String
panicComponentName CopilotWhat4
_ = String
"Copilot/What4 translation"
panicComponentIssues :: CopilotWhat4 -> String
panicComponentIssues CopilotWhat4
_ = String
"https://github.com/Copilot-Language/copilot/issues"
{-# NOINLINE Panic.panicComponentRevision #-}
panicComponentRevision :: CopilotWhat4 -> (String, String)
panicComponentRevision = $(CopilotWhat4 -> (String, String)
Panic.useGitRevision)
panic :: MonadIO m => m a
panic :: m a
panic = CopilotWhat4 -> String -> [String] -> m a
forall a b.
(PanicComponent a, HasCallStack) =>
a -> String -> [String] -> b
Panic.panic CopilotWhat4
CopilotWhat4 String
"Copilot.Theorem.What4"
[ String
"Ill-typed core expression" ]
data XExpr t where
XBool :: WB.Expr t WT.BaseBoolType -> XExpr t
XInt8 :: WB.Expr t (WT.BaseBVType 8) -> XExpr t
XInt16 :: WB.Expr t (WT.BaseBVType 16) -> XExpr t
XInt32 :: WB.Expr t (WT.BaseBVType 32) -> XExpr t
XInt64 :: WB.Expr t (WT.BaseBVType 64) -> XExpr t
XWord8 :: WB.Expr t (WT.BaseBVType 8) -> XExpr t
XWord16 :: WB.Expr t (WT.BaseBVType 16) -> XExpr t
XWord32 :: WB.Expr t (WT.BaseBVType 32) -> XExpr t
XWord64 :: WB.Expr t (WT.BaseBVType 64) -> XExpr t
XFloat :: WB.Expr t (WT.BaseFloatType WT.Prec32) -> XExpr t
XDouble :: WB.Expr t (WT.BaseFloatType WT.Prec64) -> XExpr t
XEmptyArray :: XExpr t
XArray :: 1 <= n => V.Vector n (XExpr t) -> XExpr t
XStruct :: [XExpr t] -> XExpr t
deriving instance Show (XExpr t)
data CopilotValue a = CopilotValue { CopilotValue a -> Type a
cvType :: CT.Type a
, CopilotValue a -> a
cvVal :: a
}
valFromExpr :: WG.GroundEvalFn t -> XExpr t -> IO (Some CopilotValue)
valFromExpr :: GroundEvalFn t -> XExpr t -> IO (Some CopilotValue)
valFromExpr GroundEvalFn t
ge XExpr t
xe = case XExpr t
xe of
XBool Expr t BaseBoolType
e -> CopilotValue Bool -> Some CopilotValue
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (CopilotValue Bool -> Some CopilotValue)
-> (Bool -> CopilotValue Bool) -> Bool -> Some CopilotValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type Bool -> Bool -> CopilotValue Bool
forall a. Type a -> a -> CopilotValue a
CopilotValue Type Bool
CT.Bool (Bool -> Some CopilotValue) -> IO Bool -> IO (Some CopilotValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> Expr t BaseBoolType -> IO (GroundValue BaseBoolType)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t BaseBoolType
e
XInt8 Expr t (BaseBVType 8)
e -> CopilotValue Int8 -> Some CopilotValue
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (CopilotValue Int8 -> Some CopilotValue)
-> (BV 8 -> CopilotValue Int8) -> BV 8 -> Some CopilotValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type Int8 -> Int8 -> CopilotValue Int8
forall a. Type a -> a -> CopilotValue a
CopilotValue Type Int8
CT.Int8 (Int8 -> CopilotValue Int8)
-> (BV 8 -> Int8) -> BV 8 -> CopilotValue Int8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV 8 -> Int8
forall a (w :: Nat). Num a => BV w -> a
fromBV (BV 8 -> Some CopilotValue) -> IO (BV 8) -> IO (Some CopilotValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> Expr t (BaseBVType 8) -> IO (GroundValue (BaseBVType 8))
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 8)
e
XInt16 Expr t (BaseBVType 16)
e -> CopilotValue Int16 -> Some CopilotValue
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (CopilotValue Int16 -> Some CopilotValue)
-> (BV 16 -> CopilotValue Int16) -> BV 16 -> Some CopilotValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type Int16 -> Int16 -> CopilotValue Int16
forall a. Type a -> a -> CopilotValue a
CopilotValue Type Int16
CT.Int16 (Int16 -> CopilotValue Int16)
-> (BV 16 -> Int16) -> BV 16 -> CopilotValue Int16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV 16 -> Int16
forall a (w :: Nat). Num a => BV w -> a
fromBV (BV 16 -> Some CopilotValue)
-> IO (BV 16) -> IO (Some CopilotValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> Expr t (BaseBVType 16) -> IO (GroundValue (BaseBVType 16))
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 16)
e
XInt32 Expr t (BaseBVType 32)
e -> CopilotValue Int32 -> Some CopilotValue
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (CopilotValue Int32 -> Some CopilotValue)
-> (BV 32 -> CopilotValue Int32) -> BV 32 -> Some CopilotValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type Int32 -> Int32 -> CopilotValue Int32
forall a. Type a -> a -> CopilotValue a
CopilotValue Type Int32
CT.Int32 (Int32 -> CopilotValue Int32)
-> (BV 32 -> Int32) -> BV 32 -> CopilotValue Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV 32 -> Int32
forall a (w :: Nat). Num a => BV w -> a
fromBV (BV 32 -> Some CopilotValue)
-> IO (BV 32) -> IO (Some CopilotValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> Expr t (BaseBVType 32) -> IO (GroundValue (BaseBVType 32))
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 32)
e
XInt64 Expr t (BaseBVType 64)
e -> CopilotValue Int64 -> Some CopilotValue
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (CopilotValue Int64 -> Some CopilotValue)
-> (BV 64 -> CopilotValue Int64) -> BV 64 -> Some CopilotValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type Int64 -> Int64 -> CopilotValue Int64
forall a. Type a -> a -> CopilotValue a
CopilotValue Type Int64
CT.Int64 (Int64 -> CopilotValue Int64)
-> (BV 64 -> Int64) -> BV 64 -> CopilotValue Int64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV 64 -> Int64
forall a (w :: Nat). Num a => BV w -> a
fromBV (BV 64 -> Some CopilotValue)
-> IO (BV 64) -> IO (Some CopilotValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> Expr t (BaseBVType 64) -> IO (GroundValue (BaseBVType 64))
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 64)
e
XWord8 Expr t (BaseBVType 8)
e -> CopilotValue Word8 -> Some CopilotValue
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (CopilotValue Word8 -> Some CopilotValue)
-> (BV 8 -> CopilotValue Word8) -> BV 8 -> Some CopilotValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type Word8 -> Word8 -> CopilotValue Word8
forall a. Type a -> a -> CopilotValue a
CopilotValue Type Word8
CT.Word8 (Word8 -> CopilotValue Word8)
-> (BV 8 -> Word8) -> BV 8 -> CopilotValue Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV 8 -> Word8
forall a (w :: Nat). Num a => BV w -> a
fromBV (BV 8 -> Some CopilotValue) -> IO (BV 8) -> IO (Some CopilotValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> Expr t (BaseBVType 8) -> IO (GroundValue (BaseBVType 8))
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 8)
e
XWord16 Expr t (BaseBVType 16)
e -> CopilotValue Word16 -> Some CopilotValue
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (CopilotValue Word16 -> Some CopilotValue)
-> (BV 16 -> CopilotValue Word16) -> BV 16 -> Some CopilotValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type Word16 -> Word16 -> CopilotValue Word16
forall a. Type a -> a -> CopilotValue a
CopilotValue Type Word16
CT.Word16 (Word16 -> CopilotValue Word16)
-> (BV 16 -> Word16) -> BV 16 -> CopilotValue Word16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV 16 -> Word16
forall a (w :: Nat). Num a => BV w -> a
fromBV (BV 16 -> Some CopilotValue)
-> IO (BV 16) -> IO (Some CopilotValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> Expr t (BaseBVType 16) -> IO (GroundValue (BaseBVType 16))
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 16)
e
XWord32 Expr t (BaseBVType 32)
e -> CopilotValue Word32 -> Some CopilotValue
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (CopilotValue Word32 -> Some CopilotValue)
-> (BV 32 -> CopilotValue Word32) -> BV 32 -> Some CopilotValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type Word32 -> Word32 -> CopilotValue Word32
forall a. Type a -> a -> CopilotValue a
CopilotValue Type Word32
CT.Word32 (Word32 -> CopilotValue Word32)
-> (BV 32 -> Word32) -> BV 32 -> CopilotValue Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV 32 -> Word32
forall a (w :: Nat). Num a => BV w -> a
fromBV (BV 32 -> Some CopilotValue)
-> IO (BV 32) -> IO (Some CopilotValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> Expr t (BaseBVType 32) -> IO (GroundValue (BaseBVType 32))
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 32)
e
XWord64 Expr t (BaseBVType 64)
e -> CopilotValue Word64 -> Some CopilotValue
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (CopilotValue Word64 -> Some CopilotValue)
-> (BV 64 -> CopilotValue Word64) -> BV 64 -> Some CopilotValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type Word64 -> Word64 -> CopilotValue Word64
forall a. Type a -> a -> CopilotValue a
CopilotValue Type Word64
CT.Word64 (Word64 -> CopilotValue Word64)
-> (BV 64 -> Word64) -> BV 64 -> CopilotValue Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV 64 -> Word64
forall a (w :: Nat). Num a => BV w -> a
fromBV (BV 64 -> Some CopilotValue)
-> IO (BV 64) -> IO (Some CopilotValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> Expr t (BaseBVType 64) -> IO (GroundValue (BaseBVType 64))
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 64)
e
XFloat Expr t (BaseFloatType Prec32)
e ->
CopilotValue Float -> Some CopilotValue
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (CopilotValue Float -> Some CopilotValue)
-> (BigFloat -> CopilotValue Float)
-> BigFloat
-> Some CopilotValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type Float -> Float -> CopilotValue Float
forall a. Type a -> a -> CopilotValue a
CopilotValue Type Float
CT.Float (Float -> CopilotValue Float)
-> (BigFloat -> Float) -> BigFloat -> CopilotValue Float
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Float
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Double -> Float) -> (BigFloat -> Double) -> BigFloat -> Float
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Double, Status) -> Double
forall a b. (a, b) -> a
fst ((Double, Status) -> Double)
-> (BigFloat -> (Double, Status)) -> BigFloat -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RoundMode -> BigFloat -> (Double, Status)
bfToDouble RoundMode
NearEven (BigFloat -> Some CopilotValue)
-> IO BigFloat -> IO (Some CopilotValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> Expr t (BaseFloatType Prec32)
-> IO (GroundValue (BaseFloatType Prec32))
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseFloatType Prec32)
e
XDouble Expr t (BaseFloatType Prec64)
e ->
CopilotValue Double -> Some CopilotValue
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (CopilotValue Double -> Some CopilotValue)
-> (BigFloat -> CopilotValue Double)
-> BigFloat
-> Some CopilotValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type Double -> Double -> CopilotValue Double
forall a. Type a -> a -> CopilotValue a
CopilotValue Type Double
CT.Double (Double -> CopilotValue Double)
-> (BigFloat -> Double) -> BigFloat -> CopilotValue Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Double, Status) -> Double
forall a b. (a, b) -> a
fst ((Double, Status) -> Double)
-> (BigFloat -> (Double, Status)) -> BigFloat -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RoundMode -> BigFloat -> (Double, Status)
bfToDouble RoundMode
NearEven (BigFloat -> Some CopilotValue)
-> IO BigFloat -> IO (Some CopilotValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn t
-> Expr t (BaseFloatType Prec64)
-> IO (GroundValue (BaseFloatType Prec64))
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseFloatType Prec64)
e
XExpr t
_ -> String -> IO (Some CopilotValue)
forall a. HasCallStack => String -> a
error String
"valFromExpr unhandled case"
where fromBV :: forall a w . Num a => BV.BV w -> a
fromBV :: BV w -> a
fromBV = Integer -> a
forall a. Num a => Integer -> a
fromInteger (Integer -> a) -> (BV w -> Integer) -> BV w -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned
data SomeBVExpr t where
SomeBVExpr :: 1 <= w
=> WB.BVExpr t w
-> NatRepr w
-> BVSign
-> (WB.BVExpr t w -> XExpr t)
-> SomeBVExpr t
data BVSign = Signed | Unsigned
asBVExpr :: XExpr t -> Maybe (SomeBVExpr t)
asBVExpr :: XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe = case XExpr t
xe of
XInt8 Expr t (BaseBVType 8)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 8)
-> NatRepr 8
-> BVSign
-> (Expr t (BaseBVType 8) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 8)
e NatRepr 8
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Signed Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8)
XInt16 Expr t (BaseBVType 16)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 16)
-> NatRepr 16
-> BVSign
-> (Expr t (BaseBVType 16) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 16)
e NatRepr 16
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Signed Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16)
XInt32 Expr t (BaseBVType 32)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 32)
-> NatRepr 32
-> BVSign
-> (Expr t (BaseBVType 32) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 32)
e NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Signed Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32)
XInt64 Expr t (BaseBVType 64)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 64)
-> NatRepr 64
-> BVSign
-> (Expr t (BaseBVType 64) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 64)
e NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Signed Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64)
XWord8 Expr t (BaseBVType 8)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 8)
-> NatRepr 8
-> BVSign
-> (Expr t (BaseBVType 8) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 8)
e NatRepr 8
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Unsigned Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8)
XWord16 Expr t (BaseBVType 16)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 16)
-> NatRepr 16
-> BVSign
-> (Expr t (BaseBVType 16) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 16)
e NatRepr 16
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Unsigned Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16)
XWord32 Expr t (BaseBVType 32)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 32)
-> NatRepr 32
-> BVSign
-> (Expr t (BaseBVType 32) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 32)
e NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Unsigned Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32)
XWord64 Expr t (BaseBVType 64)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 64)
-> NatRepr 64
-> BVSign
-> (Expr t (BaseBVType 64) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 64)
e NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Unsigned Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64)
XExpr t
_ -> Maybe (SomeBVExpr t)
forall a. Maybe a
Nothing
translateConstExpr :: forall a t st fs .
WB.ExprBuilder t st fs
-> CT.Type a
-> a
-> IO (XExpr t)
translateConstExpr :: ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
translateConstExpr ExprBuilder t st fs
sym Type a
tp a
a = case Type a
tp of
Type a
CT.Bool -> case a
a of
a
True -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (ExprBuilder t st fs -> Pred (ExprBuilder t st fs)
forall sym. IsExprBuilder sym => sym -> Pred sym
WI.truePred ExprBuilder t st fs
sym)
a
False -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (ExprBuilder t st fs -> Pred (ExprBuilder t st fs)
forall sym. IsExprBuilder sym => sym -> Pred sym
WI.falsePred ExprBuilder t st fs
sym)
Type a
CT.Int8 -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 8 -> BV 8 -> IO (SymBV (ExprBuilder t st fs) 8)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym NatRepr 8
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (Int8 -> BV 8
BV.int8 a
Int8
a)
Type a
CT.Int16 -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 16 -> BV 16 -> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym NatRepr 16
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (Int16 -> BV 16
BV.int16 a
Int16
a)
Type a
CT.Int32 -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 32 -> BV 32 -> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (Int32 -> BV 32
BV.int32 a
Int32
a)
Type a
CT.Int64 -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 64 -> BV 64 -> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (Int64 -> BV 64
BV.int64 a
Int64
a)
Type a
CT.Word8 -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 8 -> BV 8 -> IO (SymBV (ExprBuilder t st fs) 8)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym NatRepr 8
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (Word8 -> BV 8
BV.word8 a
Word8
a)
Type a
CT.Word16 -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 16 -> BV 16 -> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym NatRepr 16
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (Word16 -> BV 16
BV.word16 a
Word16
a)
Type a
CT.Word32 -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 32 -> BV 32 -> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (Word32 -> BV 32
BV.word32 a
Word32
a)
Type a
CT.Word64 -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 64 -> BV 64 -> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (Word64 -> BV 64
BV.word64 a
Word64
a)
Type a
CT.Float -> Expr t (BaseFloatType Prec32) -> XExpr t
forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat (Expr t (BaseFloatType Prec32) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> FloatPrecisionRepr Prec32
-> BigFloat
-> IO (SymFloat (ExprBuilder t st fs) Prec32)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym FloatPrecisionRepr Prec32
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (Double -> BigFloat
bfFromDouble (a -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac a
a))
Type a
CT.Double -> Expr t (BaseFloatType Prec64) -> XExpr t
forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble (Expr t (BaseFloatType Prec64) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> FloatPrecisionRepr Prec64
-> BigFloat
-> IO (SymFloat (ExprBuilder t st fs) Prec64)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym FloatPrecisionRepr Prec64
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (Double -> BigFloat
bfFromDouble a
Double
a)
CT.Array Type t
tp -> do
[XExpr t]
elts <- (t -> IO (XExpr t)) -> [t] -> IO [XExpr t]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (ExprBuilder t st fs -> Type t -> t -> IO (XExpr t)
forall a t (st :: * -> *) fs.
ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
translateConstExpr ExprBuilder t st fs
sym Type t
tp) (Array n t -> [t]
forall (n :: Nat) a. Array n a -> [a]
CT.arrayelems a
Array n t
a)
Just (Some NatRepr x
n) <- Maybe (Some NatRepr) -> IO (Maybe (Some NatRepr))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Some NatRepr) -> IO (Maybe (Some NatRepr)))
-> Maybe (Some NatRepr) -> IO (Maybe (Some NatRepr))
forall a b. (a -> b) -> a -> b
$ Int -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat ([XExpr t] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [XExpr t]
elts)
case NatRepr x -> Either (x :~: 0) (LeqProof 1 x)
forall (n :: Nat). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 NatRepr x
n of
Left x :~: 0
Refl -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
forall t. XExpr t
XEmptyArray
Right LeqProof 1 x
LeqProof -> do
let Just Vector x (XExpr t)
v = NatRepr x -> [XExpr t] -> Maybe (Vector x (XExpr t))
forall (n :: Nat) a.
(1 <= n) =>
NatRepr n -> [a] -> Maybe (Vector n a)
V.fromList NatRepr x
n [XExpr t]
elts
XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Vector x (XExpr t) -> XExpr t
forall (n :: Nat) t. (1 <= n) => Vector n (XExpr t) -> XExpr t
XArray Vector x (XExpr t)
v
CT.Struct a
_ -> do
[XExpr t]
elts <- [Value a] -> (Value a -> IO (XExpr t)) -> IO [XExpr t]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (a -> [Value a]
forall a. Struct a => a -> [Value a]
CT.toValues a
a) ((Value a -> IO (XExpr t)) -> IO [XExpr t])
-> (Value a -> IO (XExpr t)) -> IO [XExpr t]
forall a b. (a -> b) -> a -> b
$ \(CT.Value Type t
tp (CT.Field t
a)) ->
ExprBuilder t st fs -> Type t -> t -> IO (XExpr t)
forall a t (st :: * -> *) fs.
ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
translateConstExpr ExprBuilder t st fs
sym Type t
tp t
a
XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ [XExpr t] -> XExpr t
forall t. [XExpr t] -> XExpr t
XStruct [XExpr t]
elts
arrayLen :: KnownNat n => CT.Type (CT.Array n t) -> NatRepr n
arrayLen :: Type (Array n t) -> NatRepr n
arrayLen Type (Array n t)
_ = NatRepr n
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
freshCPConstant :: forall t st fs a .
WB.ExprBuilder t st fs
-> String
-> CT.Type a
-> IO (XExpr t)
freshCPConstant :: ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
nm Type a
tp = case Type a
tp of
Type a
CT.Bool -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr BaseBoolType
-> IO (SymExpr (ExprBuilder t st fs) BaseBoolType)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr BaseBoolType
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
Type a
CT.Int8 -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 8)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 8))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 8)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
Type a
CT.Int16 -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 16)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 16))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 16)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
Type a
CT.Int32 -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 32)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 32))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 32)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
Type a
CT.Int64 -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 64)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 64))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 64)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
Type a
CT.Word8 -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 8)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 8))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 8)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
Type a
CT.Word16 -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 16)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 16))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 16)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
Type a
CT.Word32 -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 32)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 32))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 32)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
Type a
CT.Word64 -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 64)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 64))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 64)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
Type a
CT.Float -> Expr t (BaseFloatType Prec32) -> XExpr t
forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat (Expr t (BaseFloatType Prec32) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseFloatType Prec32)
-> IO (SymExpr (ExprBuilder t st fs) (BaseFloatType Prec32))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseFloatType Prec32)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
Type a
CT.Double -> Expr t (BaseFloatType Prec64) -> XExpr t
forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble (Expr t (BaseFloatType Prec64) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseFloatType Prec64)
-> IO (SymExpr (ExprBuilder t st fs) (BaseFloatType Prec64))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseFloatType Prec64)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
atp :: Type a
atp@(CT.Array Type t
itp) -> do
NatRepr n
n <- NatRepr n -> IO (NatRepr n)
forall (m :: * -> *) a. Monad m => a -> m a
return (NatRepr n -> IO (NatRepr n)) -> NatRepr n -> IO (NatRepr n)
forall a b. (a -> b) -> a -> b
$ Type (Array n t) -> NatRepr n
forall (n :: Nat) t. KnownNat n => Type (Array n t) -> NatRepr n
arrayLen Type a
Type (Array n t)
atp
case NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
forall (n :: Nat). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 NatRepr n
n of
Left n :~: 0
Refl -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
forall t. XExpr t
XEmptyArray
Right LeqProof 1 n
LeqProof -> do
((n - 1) + 1) :~: n
Refl <- (((n - 1) + 1) :~: n) -> IO (((n - 1) + 1) :~: n)
forall (m :: * -> *) a. Monad m => a -> m a
return ((((n - 1) + 1) :~: n) -> IO (((n - 1) + 1) :~: n))
-> (((n - 1) + 1) :~: n) -> IO (((n - 1) + 1) :~: n)
forall a b. (a -> b) -> a -> b
$ NatRepr n -> NatRepr 1 -> ((n - 1) + 1) :~: n
forall (f :: Nat -> *) (m :: Nat) (g :: Nat -> *) (n :: Nat).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel NatRepr n
n (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1)
Vector n (XExpr t)
elts :: V.Vector n (XExpr t) <- NatRepr (n - 1)
-> (forall (n :: Nat). (n <= (n - 1)) => NatRepr n -> IO (XExpr t))
-> IO (Vector ((n - 1) + 1) (XExpr t))
forall (m :: * -> *) (h :: Nat) a.
Monad m =>
NatRepr h
-> (forall (n :: Nat). (n <= h) => NatRepr n -> m a)
-> m (Vector (h + 1) a)
V.generateM (NatRepr n -> NatRepr (n - 1)
forall (n :: Nat). (1 <= n) => NatRepr n -> NatRepr (n - 1)
decNat NatRepr n
n) (IO (XExpr t) -> NatRepr n -> IO (XExpr t)
forall a b. a -> b -> a
const (ExprBuilder t st fs -> String -> Type t -> IO (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
"" Type t
itp))
XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Vector n (XExpr t) -> XExpr t
forall (n :: Nat) t. (1 <= n) => Vector n (XExpr t) -> XExpr t
XArray Vector n (XExpr t)
elts
CT.Struct a
stp -> do
[XExpr t]
elts <- [Value a] -> (Value a -> IO (XExpr t)) -> IO [XExpr t]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (a -> [Value a]
forall a. Struct a => a -> [Value a]
CT.toValues a
stp) ((Value a -> IO (XExpr t)) -> IO [XExpr t])
-> (Value a -> IO (XExpr t)) -> IO [XExpr t]
forall a b. (a -> b) -> a -> b
$ \(CT.Value Type t
ftp Field s t
_) -> ExprBuilder t st fs -> String -> Type t -> IO (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
"" Type t
ftp
XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ [XExpr t] -> XExpr t
forall t. [XExpr t] -> XExpr t
XStruct [XExpr t]
elts
getStreamConstant :: WB.ExprBuilder t st fs -> CE.Id -> Int -> TransM t (XExpr t)
getStreamConstant :: ExprBuilder t st fs -> Int -> Int -> TransM t (XExpr t)
getStreamConstant ExprBuilder t st fs
sym Int
streamId Int
offset = do
Map (Int, Int) (XExpr t)
scs <- (TransState t -> Map (Int, Int) (XExpr t))
-> TransM t (Map (Int, Int) (XExpr t))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t -> Map (Int, Int) (XExpr t)
forall t. TransState t -> Map (Int, Int) (XExpr t)
streamConstants
case (Int, Int) -> Map (Int, Int) (XExpr t) -> Maybe (XExpr t)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Int
streamId, Int
offset) Map (Int, Int) (XExpr t)
scs of
Just XExpr t
xe -> XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
Maybe (XExpr t)
Nothing -> do
CS.Stream Int
_ [a]
_ Expr a
_ Type a
tp <- Int -> TransM t Stream
forall t. Int -> TransM t Stream
getStreamDef Int
streamId
let nm :: String
nm = Int -> String
forall a. Show a => a -> String
show Int
streamId String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
offset
XExpr t
xe <- IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
nm Type a
tp
(TransState t -> TransState t) -> TransM t ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TransState t
st -> TransState t
st { streamConstants :: Map (Int, Int) (XExpr t)
streamConstants = (Int, Int)
-> XExpr t -> Map (Int, Int) (XExpr t) -> Map (Int, Int) (XExpr t)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Int
streamId, Int
offset) XExpr t
xe Map (Int, Int) (XExpr t)
scs })
XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
getExternConstant :: WB.ExprBuilder t st fs
-> CT.Type a
-> CE.Name
-> Int
-> TransM t (XExpr t)
getExternConstant :: ExprBuilder t st fs
-> Type a -> String -> Int -> TransM t (XExpr t)
getExternConstant ExprBuilder t st fs
sym Type a
tp String
var Int
offset = do
Map (String, Int) (XExpr t)
es <- (TransState t -> Map (String, Int) (XExpr t))
-> TransM t (Map (String, Int) (XExpr t))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t -> Map (String, Int) (XExpr t)
forall t. TransState t -> Map (String, Int) (XExpr t)
externVars
case (String, Int) -> Map (String, Int) (XExpr t) -> Maybe (XExpr t)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (String
var, Int
offset) Map (String, Int) (XExpr t)
es of
Just XExpr t
xe -> XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
Maybe (XExpr t)
Nothing -> do
XExpr t
xe <- IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
var Type a
tp
(TransState t -> TransState t) -> TransM t ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TransState t
st -> TransState t
st { externVars :: Map (String, Int) (XExpr t)
externVars = (String, Int)
-> XExpr t
-> Map (String, Int) (XExpr t)
-> Map (String, Int) (XExpr t)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (String
var, Int
offset) XExpr t
xe Map (String, Int) (XExpr t)
es} )
XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
getExternConstantAt :: WB.ExprBuilder t st fs
-> CT.Type a
-> CE.Name
-> Int
-> TransM t (XExpr t)
getExternConstantAt :: ExprBuilder t st fs
-> Type a -> String -> Int -> TransM t (XExpr t)
getExternConstantAt ExprBuilder t st fs
sym Type a
tp String
var Int
ix = do
Map (String, Int) (XExpr t)
es <- (TransState t -> Map (String, Int) (XExpr t))
-> TransM t (Map (String, Int) (XExpr t))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t -> Map (String, Int) (XExpr t)
forall t. TransState t -> Map (String, Int) (XExpr t)
externVarsAt
case (String, Int) -> Map (String, Int) (XExpr t) -> Maybe (XExpr t)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (String
var, Int
ix) Map (String, Int) (XExpr t)
es of
Just XExpr t
xe -> XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
Maybe (XExpr t)
Nothing -> do
XExpr t
xe <- IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
var Type a
tp
(TransState t -> TransState t) -> TransM t ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TransState t
st -> TransState t
st { externVarsAt :: Map (String, Int) (XExpr t)
externVarsAt = (String, Int)
-> XExpr t
-> Map (String, Int) (XExpr t)
-> Map (String, Int) (XExpr t)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (String
var, Int
ix) XExpr t
xe Map (String, Int) (XExpr t)
es} )
XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
getStreamDef :: CE.Id -> TransM t CS.Stream
getStreamDef :: Int -> TransM t Stream
getStreamDef Int
streamId = Maybe Stream -> Stream
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Stream -> Stream)
-> TransM t (Maybe Stream) -> TransM t Stream
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TransState t -> Maybe Stream) -> TransM t (Maybe Stream)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Int -> Map Int Stream -> Maybe Stream
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
streamId (Map Int Stream -> Maybe Stream)
-> (TransState t -> Map Int Stream) -> TransState t -> Maybe Stream
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TransState t -> Map Int Stream
forall t. TransState t -> Map Int Stream
streams)
translateExpr :: WB.ExprBuilder t st fs
-> Int
-> CE.Expr a
-> TransM t (XExpr t)
translateExpr :: ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr a
e = case Expr a
e of
CE.Const Type a
tp a
a -> IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
forall a t (st :: * -> *) fs.
ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
translateConstExpr ExprBuilder t st fs
sym Type a
tp a
a
CE.Drop Type a
_tp Word32
ix Int
streamId
| Int
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
ix Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 ->
ExprBuilder t st fs -> Int -> Int -> TransM t (XExpr t)
forall t (st :: * -> *) fs.
ExprBuilder t st fs -> Int -> Int -> TransM t (XExpr t)
getStreamConstant ExprBuilder t st fs
sym Int
streamId (Int
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
ix)
| Bool
otherwise -> do
CS.Stream Int
_ [a]
buf Expr a
e Type a
_ <- Int -> TransM t Stream
forall t. Int -> TransM t Stream
getStreamDef Int
streamId
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym (Int
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
- [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
buf) Expr a
e
CE.Local Type a1
_ Type a
_ String
_ Expr a1
_ Expr a
_ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error String
"translateExpr: Local unimplemented"
CE.Var Type a
_ String
_ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error String
"translateExpr: Var unimplemented"
CE.ExternVar Type a
tp String
nm Maybe [a]
_prefix -> ExprBuilder t st fs
-> Type a -> String -> Int -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs
-> Type a -> String -> Int -> TransM t (XExpr t)
getExternConstant ExprBuilder t st fs
sym Type a
tp String
nm Int
offset
CE.Op1 Op1 a1 a
op Expr a1
e -> IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> (XExpr t -> IO (XExpr t)) -> XExpr t -> TransM t (XExpr t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprBuilder t st fs -> Op1 a1 a -> XExpr t -> IO (XExpr t)
forall t (st :: * -> *) fs a b.
ExprBuilder t st fs -> Op1 a b -> XExpr t -> IO (XExpr t)
translateOp1 ExprBuilder t st fs
sym Op1 a1 a
op (XExpr t -> TransM t (XExpr t))
-> TransM t (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder t st fs -> Int -> Expr a1 -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr a1
e
CE.Op2 Op2 a1 b a
op Expr a1
e1 Expr b
e2 -> do
XExpr t
xe1 <- ExprBuilder t st fs -> Int -> Expr a1 -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr a1
e1
XExpr t
xe2 <- ExprBuilder t st fs -> Int -> Expr b -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr b
e2
ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn <- (TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType)
-> TransM
t
(ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
forall t.
TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
pow
ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn <- (TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType)
-> TransM
t
(ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
forall t.
TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logb
IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> Op2 a1 b a
-> XExpr t
-> XExpr t
-> IO (XExpr t)
forall t (st :: * -> *) fs a b c.
ExprBuilder t st fs
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> Op2 a b c
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp2 ExprBuilder t st fs
sym ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn Op2 a1 b a
op XExpr t
xe1 XExpr t
xe2
CE.Op3 Op3 a1 b c a
op Expr a1
e1 Expr b
e2 Expr c
e3 -> do
XExpr t
xe1 <- ExprBuilder t st fs -> Int -> Expr a1 -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr a1
e1
XExpr t
xe2 <- ExprBuilder t st fs -> Int -> Expr b -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr b
e2
XExpr t
xe3 <- ExprBuilder t st fs -> Int -> Expr c -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr c
e3
IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs
-> Op3 a1 b c a -> XExpr t -> XExpr t -> XExpr t -> IO (XExpr t)
forall t (st :: * -> *) fs a b c d.
ExprBuilder t st fs
-> Op3 a b c d -> XExpr t -> XExpr t -> XExpr t -> IO (XExpr t)
translateOp3 ExprBuilder t st fs
sym Op3 a1 b c a
op XExpr t
xe1 XExpr t
xe2 XExpr t
xe3
CE.Label Type a
_ String
_ Expr a
_ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error String
"translateExpr: Label unimplemented"
translateExprAt :: WB.ExprBuilder t st fs
-> Int
-> CE.Expr a
-> TransM t (XExpr t)
translateExprAt :: ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExprAt ExprBuilder t st fs
sym Int
k Expr a
e = do
case Expr a
e of
CE.Const Type a
tp a
a -> IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
forall a t (st :: * -> *) fs.
ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
translateConstExpr ExprBuilder t st fs
sym Type a
tp a
a
CE.Drop Type a
_tp Word32
ix Int
streamId -> do
CS.Stream Int
_ [a]
buf Expr a
e Type a
tp <- Int -> TransM t Stream
forall t. Int -> TransM t Stream
getStreamDef Int
streamId
if Int
k' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
buf
then IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
forall a t (st :: * -> *) fs.
ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
translateConstExpr ExprBuilder t st fs
sym Type a
tp ([a]
buf [a] -> Int -> a
forall a. [a] -> Int -> a
!! Int
k')
else ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExprAt ExprBuilder t st fs
sym (Int
k' Int -> Int -> Int
forall a. Num a => a -> a -> a
- [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
buf) Expr a
e
where k' :: Int
k' = Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
ix
CE.Local Type a1
_ Type a
_ String
_ Expr a1
_ Expr a
_ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error String
"translateExpr: Local unimplemented"
CE.Var Type a
_ String
_ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error String
"translateExpr: Var unimplemented"
CE.ExternVar Type a
tp String
nm Maybe [a]
_prefix -> ExprBuilder t st fs
-> Type a -> String -> Int -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs
-> Type a -> String -> Int -> TransM t (XExpr t)
getExternConstantAt ExprBuilder t st fs
sym Type a
tp String
nm Int
k
CE.Op1 Op1 a1 a
op Expr a1
e -> IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> (XExpr t -> IO (XExpr t)) -> XExpr t -> TransM t (XExpr t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprBuilder t st fs -> Op1 a1 a -> XExpr t -> IO (XExpr t)
forall t (st :: * -> *) fs a b.
ExprBuilder t st fs -> Op1 a b -> XExpr t -> IO (XExpr t)
translateOp1 ExprBuilder t st fs
sym Op1 a1 a
op (XExpr t -> TransM t (XExpr t))
-> TransM t (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder t st fs -> Int -> Expr a1 -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExprAt ExprBuilder t st fs
sym Int
k Expr a1
e
CE.Op2 Op2 a1 b a
op Expr a1
e1 Expr b
e2 -> do
XExpr t
xe1 <- ExprBuilder t st fs -> Int -> Expr a1 -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExprAt ExprBuilder t st fs
sym Int
k Expr a1
e1
XExpr t
xe2 <- ExprBuilder t st fs -> Int -> Expr b -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExprAt ExprBuilder t st fs
sym Int
k Expr b
e2
ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn <- (TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType)
-> TransM
t
(ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
forall t.
TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
pow
ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn <- (TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType)
-> TransM
t
(ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
forall t.
TransState t
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logb
IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> Op2 a1 b a
-> XExpr t
-> XExpr t
-> IO (XExpr t)
forall t (st :: * -> *) fs a b c.
ExprBuilder t st fs
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> Op2 a b c
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp2 ExprBuilder t st fs
sym ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn Op2 a1 b a
op XExpr t
xe1 XExpr t
xe2
CE.Op3 Op3 a1 b c a
op Expr a1
e1 Expr b
e2 Expr c
e3 -> do
XExpr t
xe1 <- ExprBuilder t st fs -> Int -> Expr a1 -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExprAt ExprBuilder t st fs
sym Int
k Expr a1
e1
XExpr t
xe2 <- ExprBuilder t st fs -> Int -> Expr b -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExprAt ExprBuilder t st fs
sym Int
k Expr b
e2
XExpr t
xe3 <- ExprBuilder t st fs -> Int -> Expr c -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExprAt ExprBuilder t st fs
sym Int
k Expr c
e3
IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs
-> Op3 a1 b c a -> XExpr t -> XExpr t -> XExpr t -> IO (XExpr t)
forall t (st :: * -> *) fs a b c d.
ExprBuilder t st fs
-> Op3 a b c d -> XExpr t -> XExpr t -> XExpr t -> IO (XExpr t)
translateOp3 ExprBuilder t st fs
sym Op3 a1 b c a
op XExpr t
xe1 XExpr t
xe2 XExpr t
xe3
CE.Label Type a
_ String
_ Expr a
_ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error String
"translateExpr: Label unimplemented"
type BVOp1 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> IO (WB.BVExpr t w)
type FPOp1 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.Expr t (WT.BaseFloatType fpp))
type RealOp1 t = WB.Expr t WT.BaseRealType -> IO (WB.Expr t WT.BaseRealType)
fieldName :: KnownSymbol s => CT.Field s a -> SymbolRepr s
fieldName :: Field s a -> SymbolRepr s
fieldName Field s a
_ = SymbolRepr s
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol
valueName :: CT.Value a -> Some SymbolRepr
valueName :: Value a -> Some SymbolRepr
valueName (CT.Value Type t
_ Field s t
f) = SymbolRepr s -> Some SymbolRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (Field s t -> SymbolRepr s
forall (s :: Symbol) a. KnownSymbol s => Field s a -> SymbolRepr s
fieldName Field s t
f)
translateOp1 :: forall t st fs a b .
WB.ExprBuilder t st fs
-> CE.Op1 a b
-> XExpr t
-> IO (XExpr t)
translateOp1 :: ExprBuilder t st fs -> Op1 a b -> XExpr t -> IO (XExpr t)
translateOp1 ExprBuilder t st fs
sym Op1 a b
op XExpr t
xe = case (Op1 a b
op, XExpr t
xe) of
(Op1 a b
CE.Not, XBool Expr t BaseBoolType
e) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e
(Op1 a b
CE.Not, XExpr t
_) -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
(CE.Abs Type a
_, XExpr t
xe) -> (forall (w :: Nat). BVOp1 w t)
-> (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t
-> IO (XExpr t)
numOp forall (w :: Nat). BVOp1 w t
bvAbs forall (fpp :: FloatPrecision). FPOp1 fpp t
fpAbs XExpr t
xe
where bvAbs :: BVOp1 w t
bvAbs :: BVExpr t w -> IO (BVExpr t w)
bvAbs BVExpr t w
e = do BVExpr t w
zero <- ExprBuilder t st fs
-> NatRepr w -> BV w -> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
Expr t BaseBoolType
e_neg <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSlt ExprBuilder t st fs
sym BVExpr t w
SymBV (ExprBuilder t st fs) w
e BVExpr t w
SymBV (ExprBuilder t st fs) w
zero
BVExpr t w
neg_e <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSub ExprBuilder t st fs
sym BVExpr t w
SymBV (ExprBuilder t st fs) w
zero BVExpr t w
SymBV (ExprBuilder t st fs) w
e
ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e_neg BVExpr t w
SymBV (ExprBuilder t st fs) w
neg_e BVExpr t w
SymBV (ExprBuilder t st fs) w
e
fpAbs :: FPOp1 fpp t
fpAbs :: Expr t (BaseFloatType fpp) -> IO (Expr t (BaseFloatType fpp))
fpAbs Expr t (BaseFloatType fpp)
e = do Expr t (BaseFloatType fpp)
zero <- ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> BigFloat
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym FloatPrecisionRepr fpp
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr BigFloat
bfPosZero
Expr t BaseBoolType
e_neg <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatLt ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
zero
Expr t (BaseFloatType fpp)
neg_e <- ExprBuilder t st fs
-> RoundingMode
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatSub ExprBuilder t st fs
sym RoundingMode
fpRM Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
zero Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e
ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e_neg Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
neg_e Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e
(CE.Sign Type a
_, XExpr t
xe) -> (forall (w :: Nat). BVOp1 w t)
-> (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t
-> IO (XExpr t)
numOp forall (w :: Nat). BVOp1 w t
bvSign forall (fpp :: FloatPrecision). FPOp1 fpp t
fpSign XExpr t
xe
where bvSign :: BVOp1 w t
bvSign :: BVExpr t w -> IO (BVExpr t w)
bvSign BVExpr t w
e = do BVExpr t w
zero <- ExprBuilder t st fs
-> NatRepr w -> BV w -> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym NatRepr w
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
BVExpr t w
neg_one <- ExprBuilder t st fs
-> NatRepr w -> BV w -> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (-Integer
1))
BVExpr t w
pos_one <- ExprBuilder t st fs
-> NatRepr w -> BV w -> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Integer
1)
Expr t BaseBoolType
e_zero <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq ExprBuilder t st fs
sym BVExpr t w
SymBV (ExprBuilder t st fs) w
e BVExpr t w
SymBV (ExprBuilder t st fs) w
zero
Expr t BaseBoolType
e_neg <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSlt ExprBuilder t st fs
sym BVExpr t w
SymBV (ExprBuilder t st fs) w
e BVExpr t w
SymBV (ExprBuilder t st fs) w
zero
BVExpr t w
t <- ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e_neg BVExpr t w
SymBV (ExprBuilder t st fs) w
neg_one BVExpr t w
SymBV (ExprBuilder t st fs) w
pos_one
ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e_zero BVExpr t w
SymBV (ExprBuilder t st fs) w
zero BVExpr t w
SymBV (ExprBuilder t st fs) w
t
fpSign :: FPOp1 fpp t
fpSign :: Expr t (BaseFloatType fpp) -> IO (Expr t (BaseFloatType fpp))
fpSign Expr t (BaseFloatType fpp)
e = do Expr t (BaseFloatType fpp)
zero <- ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> BigFloat
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym FloatPrecisionRepr fpp
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr BigFloat
bfPosZero
Expr t (BaseFloatType fpp)
neg_one <- ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> BigFloat
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym FloatPrecisionRepr fpp
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (Double -> BigFloat
bfFromDouble (-Double
1.0))
Expr t (BaseFloatType fpp)
pos_one <- ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> BigFloat
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym FloatPrecisionRepr fpp
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (Double -> BigFloat
bfFromDouble Double
1.0)
Expr t BaseBoolType
e_zero <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatEq ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
zero
Expr t BaseBoolType
e_neg <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatLt ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
zero
Expr t (BaseFloatType fpp)
t <- ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e_neg Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
neg_one Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
pos_one
ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e_zero Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
zero Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
t
(CE.Recip Type a
_, XExpr t
xe) -> (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp1 fpp t
recip XExpr t
xe
where recip :: FPOp1 fpp t
recip :: Expr t (BaseFloatType fpp) -> IO (Expr t (BaseFloatType fpp))
recip Expr t (BaseFloatType fpp)
e = do Expr t (BaseFloatType fpp)
one <- ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> BigFloat
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym FloatPrecisionRepr fpp
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (Double -> BigFloat
bfFromDouble Double
1.0)
ExprBuilder t st fs
-> RoundingMode
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatDiv ExprBuilder t st fs
sym RoundingMode
fpRM Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
one Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e
(CE.Exp Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realExp ExprBuilder t st fs
sym) XExpr t
xe
(CE.Sqrt Type a
_, XExpr t
xe) -> (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t -> IO (XExpr t)
fpOp (ExprBuilder t st fs
-> RoundingMode
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
WI.floatSqrt ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe
(CE.Log Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realLog ExprBuilder t st fs
sym) XExpr t
xe
(CE.Sin Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realSin ExprBuilder t st fs
sym) XExpr t
xe
(CE.Cos Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realCos ExprBuilder t st fs
sym) XExpr t
xe
(CE.Tan Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realTan ExprBuilder t st fs
sym) XExpr t
xe
(CE.Asin Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (RealOp1 t
realRecip RealOp1 t -> RealOp1 t -> RealOp1 t
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realSin ExprBuilder t st fs
sym) XExpr t
xe
(CE.Acos Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (RealOp1 t
realRecip RealOp1 t -> RealOp1 t -> RealOp1 t
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realCos ExprBuilder t st fs
sym) XExpr t
xe
(CE.Atan Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (RealOp1 t
realRecip RealOp1 t -> RealOp1 t -> RealOp1 t
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realTan ExprBuilder t st fs
sym) XExpr t
xe
(CE.Sinh Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realSinh ExprBuilder t st fs
sym) XExpr t
xe
(CE.Cosh Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realCosh ExprBuilder t st fs
sym) XExpr t
xe
(CE.Tanh Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realTanh ExprBuilder t st fs
sym) XExpr t
xe
(CE.Asinh Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (RealOp1 t
realRecip RealOp1 t -> RealOp1 t -> RealOp1 t
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realSinh ExprBuilder t st fs
sym) XExpr t
xe
(CE.Acosh Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (RealOp1 t
realRecip RealOp1 t -> RealOp1 t -> RealOp1 t
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realCosh ExprBuilder t st fs
sym) XExpr t
xe
(CE.Atanh Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (RealOp1 t
realRecip RealOp1 t -> RealOp1 t -> RealOp1 t
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realTanh ExprBuilder t st fs
sym) XExpr t
xe
(CE.BwNot Type a
_, XExpr t
xe) -> case XExpr t
xe of
XBool Expr t BaseBoolType
e -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e
XExpr t
_ -> (forall (w :: Nat). BVOp1 w t) -> XExpr t -> IO (XExpr t)
bvOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
WI.bvNotBits ExprBuilder t st fs
sym) XExpr t
xe
(CE.Cast Type a
_ Type b
tp, XExpr t
xe) -> case (XExpr t
xe, Type b
tp) of
(XBool Expr t BaseBoolType
e, Type b
CT.Bool) -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool Expr t BaseBoolType
e
(XBool Expr t BaseBoolType
e, Type b
CT.Word8) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> NatRepr 8
-> IO (SymBV (ExprBuilder t st fs) 8)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e NatRepr 8
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
(XBool Expr t BaseBoolType
e, Type b
CT.Word16) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> NatRepr 16
-> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e NatRepr 16
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
(XBool Expr t BaseBoolType
e, Type b
CT.Word32) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> NatRepr 32
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
(XBool Expr t BaseBoolType
e, Type b
CT.Word64) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> NatRepr 64
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
(XBool Expr t BaseBoolType
e, Type b
CT.Int8) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> NatRepr 8
-> IO (SymBV (ExprBuilder t st fs) 8)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e NatRepr 8
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
(XBool Expr t BaseBoolType
e, Type b
CT.Int16) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> NatRepr 16
-> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e NatRepr 16
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
(XBool Expr t BaseBoolType
e, Type b
CT.Int32) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> NatRepr 32
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
(XBool Expr t BaseBoolType
e, Type b
CT.Int64) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> NatRepr 64
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
(XInt8 Expr t (BaseBVType 8)
e, Type b
CT.Int8) -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 Expr t (BaseBVType 8)
e
(XInt8 Expr t (BaseBVType 8)
e, Type b
CT.Int16) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 16
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext ExprBuilder t st fs
sym NatRepr 16
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e
(XInt8 Expr t (BaseBVType 8)
e, Type b
CT.Int32) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 32
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext ExprBuilder t st fs
sym NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e
(XInt8 Expr t (BaseBVType 8)
e, Type b
CT.Int64) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 64
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext ExprBuilder t st fs
sym NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e
(XInt16 Expr t (BaseBVType 16)
e, Type b
CT.Int16) -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 Expr t (BaseBVType 16)
e
(XInt16 Expr t (BaseBVType 16)
e, Type b
CT.Int32) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 32
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext ExprBuilder t st fs
sym NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e
(XInt16 Expr t (BaseBVType 16)
e, Type b
CT.Int64) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 64
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext ExprBuilder t st fs
sym NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e
(XInt32 Expr t (BaseBVType 32)
e, Type b
CT.Int32) -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 Expr t (BaseBVType 32)
e
(XInt32 Expr t (BaseBVType 32)
e, Type b
CT.Int64) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 64
-> SymBV (ExprBuilder t st fs) 32
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext ExprBuilder t st fs
sym NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e
(XInt64 Expr t (BaseBVType 64)
e, Type b
CT.Int64) -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 Expr t (BaseBVType 64)
e
(XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Int16) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 16
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr 16
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e
(XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Int32) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 32
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e
(XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Int64) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 64
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e
(XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Word8) -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 Expr t (BaseBVType 8)
e
(XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Word16) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 16
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr 16
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e
(XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Word32) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 32
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e
(XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Word64) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 64
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e
(XWord16 Expr t (BaseBVType 16)
e, Type b
CT.Int32) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 32
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e
(XWord16 Expr t (BaseBVType 16)
e, Type b
CT.Int64) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 64
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e
(XWord16 Expr t (BaseBVType 16)
e, Type b
CT.Word16) -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 Expr t (BaseBVType 16)
e
(XWord16 Expr t (BaseBVType 16)
e, Type b
CT.Word32) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 32
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e
(XWord16 Expr t (BaseBVType 16)
e, Type b
CT.Word64) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 64
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e
(XWord32 Expr t (BaseBVType 32)
e, Type b
CT.Int64) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 64
-> SymBV (ExprBuilder t st fs) 32
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e
(XWord32 Expr t (BaseBVType 32)
e, Type b
CT.Word32) -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 Expr t (BaseBVType 32)
e
(XWord32 Expr t (BaseBVType 32)
e, Type b
CT.Word64) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr 64
-> SymBV (ExprBuilder t st fs) 32
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e
(XWord64 Expr t (BaseBVType 64)
e, Type b
CT.Word64) -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 Expr t (BaseBVType 64)
e
(XExpr t, Type b)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
(CE.GetField (CT.Struct a
s) Type b
_ftp a -> Field s b
extractor, XStruct [XExpr t]
xes) -> do
let fieldNameRepr :: SymbolRepr s
fieldNameRepr = Field s b -> SymbolRepr s
forall (s :: Symbol) a. KnownSymbol s => Field s a -> SymbolRepr s
fieldName (a -> Field s b
extractor a
forall a. HasCallStack => a
undefined)
let structFieldNameReprs :: [Some SymbolRepr]
structFieldNameReprs = Value a -> Some SymbolRepr
forall a. Value a -> Some SymbolRepr
valueName (Value a -> Some SymbolRepr) -> [Value a] -> [Some SymbolRepr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> [Value a]
forall a. Struct a => a -> [Value a]
CT.toValues a
s
let mIx :: Maybe Int
mIx = Some SymbolRepr -> [Some SymbolRepr] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex (SymbolRepr s -> Some SymbolRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some SymbolRepr s
fieldNameRepr) [Some SymbolRepr]
structFieldNameReprs
case Maybe Int
mIx of
Just Int
ix -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ [XExpr t]
xes [XExpr t] -> Int -> XExpr t
forall a. [a] -> Int -> a
!! Int
ix
Maybe Int
Nothing -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
(Op1 a b, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
where numOp :: (forall w . BVOp1 w t)
-> (forall fpp . FPOp1 fpp t)
-> XExpr t
-> IO (XExpr t)
numOp :: (forall (w :: Nat). BVOp1 w t)
-> (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t
-> IO (XExpr t)
numOp forall (w :: Nat). BVOp1 w t
bvOp forall (fpp :: FloatPrecision). FPOp1 fpp t
fpOp XExpr t
xe = case XExpr t
xe of
XInt8 Expr t (BaseBVType 8)
e -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8) -> IO (Expr t (BaseBVType 8))
forall (w :: Nat). BVOp1 w t
bvOp Expr t (BaseBVType 8)
e
XInt16 Expr t (BaseBVType 16)
e -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16) -> IO (Expr t (BaseBVType 16))
forall (w :: Nat). BVOp1 w t
bvOp Expr t (BaseBVType 16)
e
XInt32 Expr t (BaseBVType 32)
e -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32) -> IO (Expr t (BaseBVType 32))
forall (w :: Nat). BVOp1 w t
bvOp Expr t (BaseBVType 32)
e
XInt64 Expr t (BaseBVType 64)
e -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64) -> IO (Expr t (BaseBVType 64))
forall (w :: Nat). BVOp1 w t
bvOp Expr t (BaseBVType 64)
e
XWord8 Expr t (BaseBVType 8)
e -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8) -> IO (Expr t (BaseBVType 8))
forall (w :: Nat). BVOp1 w t
bvOp Expr t (BaseBVType 8)
e
XWord16 Expr t (BaseBVType 16)
e -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16) -> IO (Expr t (BaseBVType 16))
forall (w :: Nat). BVOp1 w t
bvOp Expr t (BaseBVType 16)
e
XWord32 Expr t (BaseBVType 32)
e -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32) -> IO (Expr t (BaseBVType 32))
forall (w :: Nat). BVOp1 w t
bvOp Expr t (BaseBVType 32)
e
XWord64 Expr t (BaseBVType 64)
e -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64) -> IO (Expr t (BaseBVType 64))
forall (w :: Nat). BVOp1 w t
bvOp Expr t (BaseBVType 64)
e
XFloat Expr t (BaseFloatType Prec32)
e -> Expr t (BaseFloatType Prec32) -> XExpr t
forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat (Expr t (BaseFloatType Prec32) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec32) -> IO (Expr t (BaseFloatType Prec32))
forall (fpp :: FloatPrecision). FPOp1 fpp t
fpOp Expr t (BaseFloatType Prec32)
e
XDouble Expr t (BaseFloatType Prec64)
e -> Expr t (BaseFloatType Prec64) -> XExpr t
forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble (Expr t (BaseFloatType Prec64) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec64) -> IO (Expr t (BaseFloatType Prec64))
forall (fpp :: FloatPrecision). FPOp1 fpp t
fpOp Expr t (BaseFloatType Prec64)
e
XExpr t
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
bvOp :: (forall w . BVOp1 w t) -> XExpr t -> IO (XExpr t)
bvOp :: (forall (w :: Nat). BVOp1 w t) -> XExpr t -> IO (XExpr t)
bvOp forall (w :: Nat). BVOp1 w t
f XExpr t
xe = case XExpr t
xe of
XInt8 Expr t (BaseBVType 8)
e -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8) -> IO (Expr t (BaseBVType 8))
forall (w :: Nat). BVOp1 w t
f Expr t (BaseBVType 8)
e
XInt16 Expr t (BaseBVType 16)
e -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16) -> IO (Expr t (BaseBVType 16))
forall (w :: Nat). BVOp1 w t
f Expr t (BaseBVType 16)
e
XInt32 Expr t (BaseBVType 32)
e -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32) -> IO (Expr t (BaseBVType 32))
forall (w :: Nat). BVOp1 w t
f Expr t (BaseBVType 32)
e
XInt64 Expr t (BaseBVType 64)
e -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64) -> IO (Expr t (BaseBVType 64))
forall (w :: Nat). BVOp1 w t
f Expr t (BaseBVType 64)
e
XWord8 Expr t (BaseBVType 8)
e -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8) -> IO (Expr t (BaseBVType 8))
forall (w :: Nat). BVOp1 w t
f Expr t (BaseBVType 8)
e
XWord16 Expr t (BaseBVType 16)
e -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16) -> IO (Expr t (BaseBVType 16))
forall (w :: Nat). BVOp1 w t
f Expr t (BaseBVType 16)
e
XWord32 Expr t (BaseBVType 32)
e -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32) -> IO (Expr t (BaseBVType 32))
forall (w :: Nat). BVOp1 w t
f Expr t (BaseBVType 32)
e
XWord64 Expr t (BaseBVType 64)
e -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64) -> IO (Expr t (BaseBVType 64))
forall (w :: Nat). BVOp1 w t
f Expr t (BaseBVType 64)
e
XExpr t
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
fpOp :: (forall fpp . FPOp1 fpp t) -> XExpr t -> IO (XExpr t)
fpOp :: (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp1 fpp t
g XExpr t
xe = case XExpr t
xe of
XFloat Expr t (BaseFloatType Prec32)
e -> Expr t (BaseFloatType Prec32) -> XExpr t
forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat (Expr t (BaseFloatType Prec32) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec32) -> IO (Expr t (BaseFloatType Prec32))
forall (fpp :: FloatPrecision). FPOp1 fpp t
g Expr t (BaseFloatType Prec32)
e
XDouble Expr t (BaseFloatType Prec64)
e -> Expr t (BaseFloatType Prec64) -> XExpr t
forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble (Expr t (BaseFloatType Prec64) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec64) -> IO (Expr t (BaseFloatType Prec64))
forall (fpp :: FloatPrecision). FPOp1 fpp t
g Expr t (BaseFloatType Prec64)
e
XExpr t
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
realOp :: RealOp1 t -> XExpr t -> IO (XExpr t)
realOp :: RealOp1 t -> XExpr t -> IO (XExpr t)
realOp RealOp1 t
h XExpr t
xe = (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp1 fpp t
hf XExpr t
xe
where hf :: (forall fpp . FPOp1 fpp t)
hf :: Expr t (BaseFloatType fpp) -> IO (Expr t (BaseFloatType fpp))
hf Expr t (BaseFloatType fpp)
e = do Expr t BaseRealType
re <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymReal (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e
Expr t BaseRealType
hre <- RealOp1 t
h Expr t BaseRealType
re
ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal (ExprBuilder t st fs)
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
WI.realToFloat ExprBuilder t st fs
sym FloatPrecisionRepr fpp
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
fpRM Expr t BaseRealType
SymReal (ExprBuilder t st fs)
hre
realRecip :: RealOp1 t
realRecip :: RealOp1 t
realRecip Expr t BaseRealType
e = do Expr t BaseRealType
one <- ExprBuilder t st fs
-> Rational -> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
WI.realLit ExprBuilder t st fs
sym Rational
1
ExprBuilder t st fs
-> SymReal (ExprBuilder t st fs)
-> SymReal (ExprBuilder t st fs)
-> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
WI.realDiv ExprBuilder t st fs
sym Expr t BaseRealType
SymReal (ExprBuilder t st fs)
one Expr t BaseRealType
SymReal (ExprBuilder t st fs)
e
type BVOp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BVExpr t w)
type FPOp2 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.Expr t (WT.BaseFloatType fpp))
type RealOp2 t = WB.Expr t WT.BaseRealType -> WB.Expr t WT.BaseRealType -> IO (WB.Expr t WT.BaseRealType)
type BoolCmp2 t = WB.BoolExpr t -> WB.BoolExpr t -> IO (WB.BoolExpr t)
type BVCmp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BoolExpr t)
type FPCmp2 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.BoolExpr t)
translateOp2 :: forall t st fs a b c .
WB.ExprBuilder t st fs
-> (WB.ExprSymFn t
(EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
WT.BaseRealType)
-> (WB.ExprSymFn t
(EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
WT.BaseRealType)
-> CE.Op2 a b c
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp2 :: ExprBuilder t st fs
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> Op2 a b c
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp2 ExprBuilder t st fs
sym ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn Op2 a b c
op XExpr t
xe1 XExpr t
xe2 = case (Op2 a b c
op, XExpr t
xe1, XExpr t
xe2) of
(Op2 a b c
CE.And, XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.andPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e1 Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e2
(Op2 a b c
CE.Or, XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.orPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e1 Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e2
(CE.Add Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAdd ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> RoundingMode
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatAdd ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe1 XExpr t
xe2
(CE.Sub Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSub ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> RoundingMode
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatSub ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe1 XExpr t
xe2
(CE.Mul Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvMul ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> RoundingMode
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatMul ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe1 XExpr t
xe2
(CE.Mod Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (w :: Nat). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSrem ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvUrem ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
(CE.Div Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (w :: Nat). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSdiv ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvUdiv ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
(CE.Fdiv Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t -> XExpr t -> IO (XExpr t)
fpOp (ExprBuilder t st fs
-> RoundingMode
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatDiv ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe1 XExpr t
xe2
(CE.Pow Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t -> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp2 fpp t
powFn' XExpr t
xe1 XExpr t
xe2
where powFn' :: FPOp2 fpp t
powFn' :: Expr t (BaseFloatType fpp)
-> Expr t (BaseFloatType fpp) -> IO (Expr t (BaseFloatType fpp))
powFn' Expr t (BaseFloatType fpp)
e1 Expr t (BaseFloatType fpp)
e2 = do Expr t BaseRealType
re1 <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymReal (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e1
Expr t BaseRealType
re2 <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymReal (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e2
let args :: Assignment (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
args = (Assignment (Expr t) EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment (Expr t) EmptyCtx
-> Expr t BaseRealType
-> Assignment (Expr t) (EmptyCtx ::> BaseRealType)
forall k (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Expr t BaseRealType
re1 Assignment (Expr t) (EmptyCtx ::> BaseRealType)
-> Expr t BaseRealType
-> Assignment
(Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
forall k (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Expr t BaseRealType
re2)
Expr t BaseRealType
rpow <- ExprBuilder t st fs
-> SymFn
(ExprBuilder t st fs)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
-> Assignment
(SymExpr (ExprBuilder t st fs))
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
-> IO (SymReal (ExprBuilder t st fs))
forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
WI.applySymFn ExprBuilder t st fs
sym ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
SymFn
(ExprBuilder t st fs)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
powFn Assignment (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
Assignment
(SymExpr (ExprBuilder t st fs))
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
args
ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal (ExprBuilder t st fs)
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
WI.realToFloat ExprBuilder t st fs
sym FloatPrecisionRepr fpp
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
fpRM Expr t BaseRealType
SymReal (ExprBuilder t st fs)
rpow
(CE.Logb Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t -> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp2 fpp t
logbFn' XExpr t
xe1 XExpr t
xe2
where logbFn' :: FPOp2 fpp t
logbFn' :: Expr t (BaseFloatType fpp)
-> Expr t (BaseFloatType fpp) -> IO (Expr t (BaseFloatType fpp))
logbFn' Expr t (BaseFloatType fpp)
e1 Expr t (BaseFloatType fpp)
e2 = do Expr t BaseRealType
re1 <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymReal (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e1
Expr t BaseRealType
re2 <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymReal (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e2
let args :: Assignment (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
args = (Assignment (Expr t) EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment (Expr t) EmptyCtx
-> Expr t BaseRealType
-> Assignment (Expr t) (EmptyCtx ::> BaseRealType)
forall k (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Expr t BaseRealType
re1 Assignment (Expr t) (EmptyCtx ::> BaseRealType)
-> Expr t BaseRealType
-> Assignment
(Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
forall k (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Expr t BaseRealType
re2)
Expr t BaseRealType
rpow <- ExprBuilder t st fs
-> SymFn
(ExprBuilder t st fs)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
-> Assignment
(SymExpr (ExprBuilder t st fs))
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
-> IO (SymReal (ExprBuilder t st fs))
forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
WI.applySymFn ExprBuilder t st fs
sym ExprSymFn
t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
SymFn
(ExprBuilder t st fs)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
logbFn Assignment (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
Assignment
(SymExpr (ExprBuilder t st fs))
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
args
ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal (ExprBuilder t st fs)
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
WI.realToFloat ExprBuilder t st fs
sym FloatPrecisionRepr fpp
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
fpRM Expr t BaseRealType
SymReal (ExprBuilder t st fs)
rpow
(CE.Eq Type a
_, XExpr t
xe1, XExpr t
xe2) -> BoolCmp2 t
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
cmp (ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.eqPred ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatEq ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
(CE.Ne Type a
_, XExpr t
xe1, XExpr t
xe2) -> BoolCmp2 t
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
cmp BoolCmp2 t
neqPred forall (w :: Nat). BVCmp2 w t
bvNeq forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpNeq XExpr t
xe1 XExpr t
xe2
where neqPred :: BoolCmp2 t
neqPred :: BoolCmp2 t
neqPred Expr t BaseBoolType
e1 Expr t BaseBoolType
e2 = do Expr t BaseBoolType
e <- ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.eqPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e1 Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e2
ExprBuilder t st fs
-> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e
bvNeq :: forall w . BVCmp2 w t
bvNeq :: BVExpr t w -> BVExpr t w -> IO (Expr t BaseBoolType)
bvNeq BVExpr t w
e1 BVExpr t w
e2 = do Expr t BaseBoolType
e <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq ExprBuilder t st fs
sym BVExpr t w
SymBV (ExprBuilder t st fs) w
e1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2
ExprBuilder t st fs
-> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e
fpNeq :: forall fpp . FPCmp2 fpp t
fpNeq :: Expr t (BaseFloatType fpp)
-> Expr t (BaseFloatType fpp) -> IO (Expr t BaseBoolType)
fpNeq Expr t (BaseFloatType fpp)
e1 Expr t (BaseFloatType fpp)
e2 = do Expr t BaseBoolType
e <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatEq ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e1 Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e2
ExprBuilder t st fs
-> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e
(CE.Le Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVCmp2 w t)
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSle ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUle ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatLe ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
(CE.Ge Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVCmp2 w t)
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSge ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUge ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatGe ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
(CE.Lt Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVCmp2 w t)
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSlt ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUlt ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatLt ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
(CE.Gt Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVCmp2 w t)
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSgt ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUgt ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatGt ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
(CE.BwAnd Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (w :: Nat). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAndBits ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAndBits ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
(CE.BwOr Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (w :: Nat). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvOrBits ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvOrBits ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
(CE.BwXor Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (w :: Nat). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvXorBits ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvXorBits ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
(CE.BwShiftL Type a
_ Type b
_, XExpr t
xe1, XExpr t
xe2) -> do
Just (SomeBVExpr BVExpr t w
e1 NatRepr w
w1 BVSign
_ BVExpr t w -> XExpr t
ctor1) <- Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t)))
-> Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall a b. (a -> b) -> a -> b
$ XExpr t -> Maybe (SomeBVExpr t)
forall t. XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe1
Just (SomeBVExpr BVExpr t w
e2 NatRepr w
w2 BVSign
_ BVExpr t w -> XExpr t
_ ) <- Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t)))
-> Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall a b. (a -> b) -> a -> b
$ XExpr t -> Maybe (SomeBVExpr t)
forall t. XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe2
BVExpr t w
e2' <- case NatRepr w -> NatRepr w -> NatCases w w
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr w
w1 NatRepr w
w2 of
NatCaseLT LeqProof (w + 1) w
LeqProof -> ExprBuilder t st fs
-> NatRepr w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc ExprBuilder t st fs
sym NatRepr w
w1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2
NatCases w w
NatCaseEQ -> BVExpr t w -> IO (BVExpr t w)
forall (m :: * -> *) a. Monad m => a -> m a
return BVExpr t w
e2
NatCaseGT LeqProof (w + 1) w
LeqProof -> ExprBuilder t st fs
-> NatRepr w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr w
w1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2
BVExpr t w -> XExpr t
ctor1 (BVExpr t w -> XExpr t) -> IO (BVExpr t w) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvShl ExprBuilder t st fs
sym BVExpr t w
SymBV (ExprBuilder t st fs) w
e1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2'
(CE.BwShiftR Type a
_ Type b
_, XExpr t
xe1, XExpr t
xe2) -> do
Just (SomeBVExpr BVExpr t w
e1 NatRepr w
w1 BVSign
sgn1 BVExpr t w -> XExpr t
ctor1) <- Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t)))
-> Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall a b. (a -> b) -> a -> b
$ XExpr t -> Maybe (SomeBVExpr t)
forall t. XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe1
Just (SomeBVExpr BVExpr t w
e2 NatRepr w
w2 BVSign
_ BVExpr t w -> XExpr t
_ ) <- Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t)))
-> Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall a b. (a -> b) -> a -> b
$ XExpr t -> Maybe (SomeBVExpr t)
forall t. XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe2
BVExpr t w
e2' <- case NatRepr w -> NatRepr w -> NatCases w w
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr w
w1 NatRepr w
w2 of
NatCaseLT LeqProof (w + 1) w
LeqProof -> ExprBuilder t st fs
-> NatRepr w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc ExprBuilder t st fs
sym NatRepr w
w1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2
NatCases w w
NatCaseEQ -> BVExpr t w -> IO (BVExpr t w)
forall (m :: * -> *) a. Monad m => a -> m a
return BVExpr t w
e2
NatCaseGT LeqProof (w + 1) w
LeqProof -> ExprBuilder t st fs
-> NatRepr w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr w
w1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2
BVExpr t w -> XExpr t
ctor1 (BVExpr t w -> XExpr t) -> IO (BVExpr t w) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case BVSign
sgn1 of
BVSign
Signed -> ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAshr ExprBuilder t st fs
sym BVExpr t w
SymBV (ExprBuilder t st fs) w
e1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2'
BVSign
Unsigned -> ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvLshr ExprBuilder t st fs
sym BVExpr t w
SymBV (ExprBuilder t st fs) w
e1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2'
(CE.Index Type (Array n c)
_, XExpr t
xe1, XExpr t
xe2) -> do
case (XExpr t
xe1, XExpr t
xe2) of
(XArray Vector n (XExpr t)
xes, XWord32 Expr t (BaseBVType 32)
ix) -> ExprBuilder t st fs
-> Word32
-> Expr t (BaseBVType 32)
-> Vector n (XExpr t)
-> IO (XExpr t)
forall (n :: Nat).
(1 <= n) =>
ExprBuilder t st fs
-> Word32
-> Expr t (BaseBVType 32)
-> Vector n (XExpr t)
-> IO (XExpr t)
buildIndexExpr ExprBuilder t st fs
sym Word32
0 Expr t (BaseBVType 32)
ix Vector n (XExpr t)
xes
(XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
(Op2 a b c, XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
where numOp :: (forall w . BVOp2 w t)
-> (forall fpp . FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp :: (forall (w :: Nat). BVOp2 w t)
-> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp forall (w :: Nat). BVOp2 w t
bvOp forall (fpp :: FloatPrecision). FPOp2 fpp t
fpOp XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8)
-> Expr t (BaseBVType 8) -> IO (Expr t (BaseBVType 8))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
(XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16)
-> Expr t (BaseBVType 16) -> IO (Expr t (BaseBVType 16))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
(XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2)-> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32)
-> Expr t (BaseBVType 32) -> IO (Expr t (BaseBVType 32))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
(XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2)-> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64)
-> Expr t (BaseBVType 64) -> IO (Expr t (BaseBVType 64))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
(XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2)-> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8)
-> Expr t (BaseBVType 8) -> IO (Expr t (BaseBVType 8))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
(XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2)-> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16)
-> Expr t (BaseBVType 16) -> IO (Expr t (BaseBVType 16))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
(XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2)-> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32)
-> Expr t (BaseBVType 32) -> IO (Expr t (BaseBVType 32))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
(XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2)-> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64)
-> Expr t (BaseBVType 64) -> IO (Expr t (BaseBVType 64))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
(XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2)-> Expr t (BaseFloatType Prec32) -> XExpr t
forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat (Expr t (BaseFloatType Prec32) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec32)
-> Expr t (BaseFloatType Prec32)
-> IO (Expr t (BaseFloatType Prec32))
forall (fpp :: FloatPrecision). FPOp2 fpp t
fpOp Expr t (BaseFloatType Prec32)
e1 Expr t (BaseFloatType Prec32)
e2
(XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2)-> Expr t (BaseFloatType Prec64) -> XExpr t
forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble (Expr t (BaseFloatType Prec64) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec64)
-> Expr t (BaseFloatType Prec64)
-> IO (Expr t (BaseFloatType Prec64))
forall (fpp :: FloatPrecision). FPOp2 fpp t
fpOp Expr t (BaseFloatType Prec64)
e1 Expr t (BaseFloatType Prec64)
e2
(XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
bvOp :: (forall w . BVOp2 w t)
-> (forall w . BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp :: (forall (w :: Nat). BVOp2 w t)
-> (forall (w :: Nat). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp forall (w :: Nat). BVOp2 w t
opS forall (w :: Nat). BVOp2 w t
opU XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8)
-> Expr t (BaseBVType 8) -> IO (Expr t (BaseBVType 8))
forall (w :: Nat). BVOp2 w t
opS Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
(XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16)
-> Expr t (BaseBVType 16) -> IO (Expr t (BaseBVType 16))
forall (w :: Nat). BVOp2 w t
opS Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
(XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32)
-> Expr t (BaseBVType 32) -> IO (Expr t (BaseBVType 32))
forall (w :: Nat). BVOp2 w t
opS Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
(XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64)
-> Expr t (BaseBVType 64) -> IO (Expr t (BaseBVType 64))
forall (w :: Nat). BVOp2 w t
opS Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
(XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8)
-> Expr t (BaseBVType 8) -> IO (Expr t (BaseBVType 8))
forall (w :: Nat). BVOp2 w t
opU Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
(XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16)
-> Expr t (BaseBVType 16) -> IO (Expr t (BaseBVType 16))
forall (w :: Nat). BVOp2 w t
opU Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
(XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32)
-> Expr t (BaseBVType 32) -> IO (Expr t (BaseBVType 32))
forall (w :: Nat). BVOp2 w t
opU Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
(XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64)
-> Expr t (BaseBVType 64) -> IO (Expr t (BaseBVType 64))
forall (w :: Nat). BVOp2 w t
opU Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
(XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
fpOp :: (forall fpp . FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
fpOp :: (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t -> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp2 fpp t
op XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2) -> Expr t (BaseFloatType Prec32) -> XExpr t
forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat (Expr t (BaseFloatType Prec32) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec32)
-> Expr t (BaseFloatType Prec32)
-> IO (Expr t (BaseFloatType Prec32))
forall (fpp :: FloatPrecision). FPOp2 fpp t
op Expr t (BaseFloatType Prec32)
e1 Expr t (BaseFloatType Prec32)
e2
(XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2) -> Expr t (BaseFloatType Prec64) -> XExpr t
forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble (Expr t (BaseFloatType Prec64) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec64)
-> Expr t (BaseFloatType Prec64)
-> IO (Expr t (BaseFloatType Prec64))
forall (fpp :: FloatPrecision). FPOp2 fpp t
op Expr t (BaseFloatType Prec64)
e1 Expr t (BaseFloatType Prec64)
e2
(XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
cmp :: BoolCmp2 t
-> (forall w . BVCmp2 w t)
-> (forall fpp . FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
cmp :: BoolCmp2 t
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
cmp BoolCmp2 t
boolOp forall (w :: Nat). BVCmp2 w t
bvOp forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BoolCmp2 t
boolOp Expr t BaseBoolType
e1 Expr t BaseBoolType
e2
(XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8)
-> Expr t (BaseBVType 8) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
(XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16)
-> Expr t (BaseBVType 16) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
(XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32)
-> Expr t (BaseBVType 32) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
(XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64)
-> Expr t (BaseBVType 64) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
(XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8)
-> Expr t (BaseBVType 8) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
(XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16)
-> Expr t (BaseBVType 16) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
(XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32)
-> Expr t (BaseBVType 32) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
(XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64)
-> Expr t (BaseBVType 64) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
(XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec32)
-> Expr t (BaseFloatType Prec32) -> IO (Expr t BaseBoolType)
forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp Expr t (BaseFloatType Prec32)
e1 Expr t (BaseFloatType Prec32)
e2
(XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec64)
-> Expr t (BaseFloatType Prec64) -> IO (Expr t BaseBoolType)
forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp Expr t (BaseFloatType Prec64)
e1 Expr t (BaseFloatType Prec64)
e2
(XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
numCmp :: (forall w . BVCmp2 w t)
-> (forall w . BVCmp2 w t)
-> (forall fpp . FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp :: (forall (w :: Nat). BVCmp2 w t)
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp forall (w :: Nat). BVCmp2 w t
bvSOp forall (w :: Nat). BVCmp2 w t
bvUOp forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8)
-> Expr t (BaseBVType 8) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvSOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
(XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16)
-> Expr t (BaseBVType 16) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvSOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
(XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32)
-> Expr t (BaseBVType 32) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvSOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
(XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64)
-> Expr t (BaseBVType 64) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvSOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
(XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8)
-> Expr t (BaseBVType 8) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvUOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
(XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16)
-> Expr t (BaseBVType 16) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvUOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
(XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32)
-> Expr t (BaseBVType 32) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvUOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
(XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64)
-> Expr t (BaseBVType 64) -> IO (Expr t BaseBoolType)
forall (w :: Nat). BVCmp2 w t
bvUOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
(XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec32)
-> Expr t (BaseFloatType Prec32) -> IO (Expr t BaseBoolType)
forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp Expr t (BaseFloatType Prec32)
e1 Expr t (BaseFloatType Prec32)
e2
(XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2)-> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec64)
-> Expr t (BaseFloatType Prec64) -> IO (Expr t BaseBoolType)
forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp Expr t (BaseFloatType Prec64)
e1 Expr t (BaseFloatType Prec64)
e2
(XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
buildIndexExpr :: 1 <= n
=> WB.ExprBuilder t st fs
-> Word32
-> WB.Expr t (WT.BaseBVType 32)
-> V.Vector n (XExpr t)
-> IO (XExpr t)
buildIndexExpr :: ExprBuilder t st fs
-> Word32
-> Expr t (BaseBVType 32)
-> Vector n (XExpr t)
-> IO (XExpr t)
buildIndexExpr ExprBuilder t st fs
sym Word32
curIx Expr t (BaseBVType 32)
ix Vector n (XExpr t)
xelts = case Vector n (XExpr t)
-> (XExpr t, Either (n :~: 1) (Vector (n - 1) (XExpr t)))
forall (n :: Nat) a.
Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))
V.uncons Vector n (XExpr t)
xelts of
(XExpr t
xe, Left n :~: 1
Refl) -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
(XExpr t
xe, Right Vector (n - 1) (XExpr t)
xelts') -> do
LeqProof 1 (n - 1)
LeqProof <- LeqProof 1 (n - 1) -> IO (LeqProof 1 (n - 1))
forall (m :: * -> *) a. Monad m => a -> m a
return (LeqProof 1 (n - 1) -> IO (LeqProof 1 (n - 1)))
-> LeqProof 1 (n - 1) -> IO (LeqProof 1 (n - 1))
forall a b. (a -> b) -> a -> b
$ Vector (n - 1) (XExpr t) -> LeqProof 1 (n - 1)
forall (n :: Nat) a. Vector n a -> LeqProof 1 n
V.nonEmpty Vector (n - 1) (XExpr t)
xelts'
XExpr t
rstExpr <- ExprBuilder t st fs
-> Word32
-> Expr t (BaseBVType 32)
-> Vector (n - 1) (XExpr t)
-> IO (XExpr t)
forall (n :: Nat).
(1 <= n) =>
ExprBuilder t st fs
-> Word32
-> Expr t (BaseBVType 32)
-> Vector n (XExpr t)
-> IO (XExpr t)
buildIndexExpr ExprBuilder t st fs
sym (Word32
curIxWord32 -> Word32 -> Word32
forall a. Num a => a -> a -> a
+Word32
1) Expr t (BaseBVType 32)
ix Vector (n - 1) (XExpr t)
xelts'
Expr t (BaseBVType 32)
curIxExpr <- ExprBuilder t st fs
-> NatRepr 32 -> BV 32 -> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (Word32 -> BV 32
BV.word32 Word32
curIx)
Expr t BaseBoolType
ixEq <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) 32
-> SymBV (ExprBuilder t st fs) 32
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq ExprBuilder t st fs
sym Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
curIxExpr Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
ix
ExprBuilder t st fs
-> Expr t BaseBoolType -> XExpr t -> XExpr t -> IO (XExpr t)
mkIte ExprBuilder t st fs
sym Expr t BaseBoolType
ixEq XExpr t
xe XExpr t
rstExpr
mkIte :: WB.ExprBuilder t st fs
-> WB.Expr t WT.BaseBoolType
-> XExpr t
-> XExpr t
-> IO (XExpr t)
mkIte :: ExprBuilder t st fs
-> Expr t BaseBoolType -> XExpr t -> XExpr t -> IO (XExpr t)
mkIte ExprBuilder t st fs
sym Expr t BaseBoolType
pred XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.itePred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e1 Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e2
(XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 8
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 8)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e1 Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e2
(XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 16
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e1 Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e2
(XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 32
-> SymBV (ExprBuilder t st fs) 32
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e1 Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e2
(XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 64
-> SymBV (ExprBuilder t st fs) 64
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e1 Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e2
(XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 8
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 8)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e1 Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e2
(XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 16
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e1 Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e2
(XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 32
-> SymBV (ExprBuilder t st fs) 32
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e1 Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e2
(XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 64
-> SymBV (ExprBuilder t st fs) 64
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e1 Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e2
(XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2) -> Expr t (BaseFloatType Prec32) -> XExpr t
forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat (Expr t (BaseFloatType Prec32) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymFloat (ExprBuilder t st fs) Prec32
-> SymFloat (ExprBuilder t st fs) Prec32
-> IO (SymFloat (ExprBuilder t st fs) Prec32)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseFloatType Prec32)
SymFloat (ExprBuilder t st fs) Prec32
e1 Expr t (BaseFloatType Prec32)
SymFloat (ExprBuilder t st fs) Prec32
e2
(XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2) -> Expr t (BaseFloatType Prec64) -> XExpr t
forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble (Expr t (BaseFloatType Prec64) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymFloat (ExprBuilder t st fs) Prec64
-> SymFloat (ExprBuilder t st fs) Prec64
-> IO (SymFloat (ExprBuilder t st fs) Prec64)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseFloatType Prec64)
SymFloat (ExprBuilder t st fs) Prec64
e1 Expr t (BaseFloatType Prec64)
SymFloat (ExprBuilder t st fs) Prec64
e2
(XStruct [XExpr t]
xes1, XStruct [XExpr t]
xes2) ->
[XExpr t] -> XExpr t
forall t. [XExpr t] -> XExpr t
XStruct ([XExpr t] -> XExpr t) -> IO [XExpr t] -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (XExpr t -> XExpr t -> IO (XExpr t))
-> [XExpr t] -> [XExpr t] -> IO [XExpr t]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (ExprBuilder t st fs
-> Expr t BaseBoolType -> XExpr t -> XExpr t -> IO (XExpr t)
mkIte ExprBuilder t st fs
sym Expr t BaseBoolType
pred) [XExpr t]
xes1 [XExpr t]
xes2
(XArray Vector n (XExpr t)
xes1, XArray Vector n (XExpr t)
xes2) ->
case Vector n (XExpr t) -> NatRepr n
forall (n :: Nat) a. Vector n a -> NatRepr n
V.length Vector n (XExpr t)
xes1 NatRepr n -> NatRepr n -> Maybe (n :~: n)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
`testEquality` Vector n (XExpr t) -> NatRepr n
forall (n :: Nat) a. Vector n a -> NatRepr n
V.length Vector n (XExpr t)
xes2 of
Just n :~: n
Refl -> Vector n (XExpr t) -> XExpr t
forall (n :: Nat) t. (1 <= n) => Vector n (XExpr t) -> XExpr t
XArray (Vector n (XExpr t) -> XExpr t)
-> IO (Vector n (XExpr t)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (XExpr t -> XExpr t -> IO (XExpr t))
-> Vector n (XExpr t)
-> Vector n (XExpr t)
-> IO (Vector n (XExpr t))
forall (m :: * -> *) a b c (n :: Nat).
Monad m =>
(a -> b -> m c) -> Vector n a -> Vector n b -> m (Vector n c)
V.zipWithM (ExprBuilder t st fs
-> Expr t BaseBoolType -> XExpr t -> XExpr t -> IO (XExpr t)
mkIte ExprBuilder t st fs
sym Expr t BaseBoolType
pred) Vector n (XExpr t)
xes1 Vector n (XExpr t)
Vector n (XExpr t)
xes2
Maybe (n :~: n)
Nothing -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
(XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
translateOp3 :: forall t st fs a b c d .
WB.ExprBuilder t st fs
-> CE.Op3 a b c d
-> XExpr t
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp3 :: ExprBuilder t st fs
-> Op3 a b c d -> XExpr t -> XExpr t -> XExpr t -> IO (XExpr t)
translateOp3 ExprBuilder t st fs
sym (CE.Mux Type b
_) (XBool Expr t BaseBoolType
te) XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.itePred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e1 Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e2
(XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 8
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 8)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e1 Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e2
(XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 16
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e1 Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e2
(XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 32
-> SymBV (ExprBuilder t st fs) 32
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e1 Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e2
(XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 64
-> SymBV (ExprBuilder t st fs) 64
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e1 Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e2
(XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 8
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 8)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e1 Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e2
(XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 16
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e1 Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e2
(XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 32
-> SymBV (ExprBuilder t st fs) 32
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e1 Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e2
(XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 64
-> SymBV (ExprBuilder t st fs) 64
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e1 Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e2
(XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2) -> Expr t (BaseFloatType Prec32) -> XExpr t
forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat (Expr t (BaseFloatType Prec32) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymFloat (ExprBuilder t st fs) Prec32
-> SymFloat (ExprBuilder t st fs) Prec32
-> IO (SymFloat (ExprBuilder t st fs) Prec32)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseFloatType Prec32)
SymFloat (ExprBuilder t st fs) Prec32
e1 Expr t (BaseFloatType Prec32)
SymFloat (ExprBuilder t st fs) Prec32
e2
(XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2) -> Expr t (BaseFloatType Prec64) -> XExpr t
forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble (Expr t (BaseFloatType Prec64) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymFloat (ExprBuilder t st fs) Prec64
-> SymFloat (ExprBuilder t st fs) Prec64
-> IO (SymFloat (ExprBuilder t st fs) Prec64)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseFloatType Prec64)
SymFloat (ExprBuilder t st fs) Prec64
e1 Expr t (BaseFloatType Prec64)
SymFloat (ExprBuilder t st fs) Prec64
e2
(XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
translateOp3 ExprBuilder t st fs
_ Op3 a b c d
_ XExpr t
_ XExpr t
_ XExpr t
_ = IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic