{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# 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 GHC.Float (castWord32ToFloat, castWord64ToDouble)
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
solver spec :: Spec
spec = do
Some ng :: 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
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)
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)
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)
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 -> (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
(Expr 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 "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
(Expr 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 "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
(Expr x)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
-> ExprSymFn
x
(Expr 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
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
-> ExprSymFn
t
(Expr 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
(Expr x)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
pow ExprSymFn
x
(Expr 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
$ \pr :: Property
pr -> do
let bufLen :: Stream -> Int
bufLen (CS.Stream _ buf :: [a]
buf _ _) = [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 (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 [0 .. Int
maxBufLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- 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
$ \k :: Int
k -> do
XBool p :: 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 p :: 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 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
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 (_ge :: 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)
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
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 (_ge :: WriterConn x (Writer DReal)
_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)
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
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 _ge :: 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)
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
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 (_ge :: 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)
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
(res :: [(String, SatResult)]
res, _) <- 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
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
pow :: WB.ExprSymFn t (WB.Expr t)
(EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
WT.BaseRealType,
TransState t
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
logb :: WB.ExprSymFn t (WB.Expr 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 _ = "Copilot/What4 translation"
panicComponentIssues :: CopilotWhat4 -> String
panicComponentIssues _ = "https://github.com/Copilot-Language/copilot-theorem/issues"
{-# NOINLINE Panic.panicComponentRevision #-}
panicComponentRevision :: CopilotWhat4 -> (String, String)
panicComponentRevision = $(Bool
String -> ShowS
forall a. [a] -> [a] -> [a]
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 "Copilot.Theorem.What4"
[ "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 ge :: GroundEvalFn t
ge xe :: XExpr t
xe = case XExpr t
xe of
XBool e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: Expr t (BaseFloatType Prec32)
e ->
CopilotValue Float -> Some CopilotValue
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (CopilotValue Float -> Some CopilotValue)
-> (BV 32 -> CopilotValue Float) -> BV 32 -> 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)
-> (BV 32 -> Float) -> BV 32 -> CopilotValue Float
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> Float
castWord32ToFloat (Word32 -> Float) -> (BV 32 -> Word32) -> BV 32 -> Float
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 (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 e :: Expr t (BaseFloatType Prec64)
e ->
CopilotValue Double -> Some CopilotValue
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (CopilotValue Double -> Some CopilotValue)
-> (BV 64 -> CopilotValue Double) -> BV 64 -> 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)
-> (BV 64 -> Double) -> BV 64 -> CopilotValue Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Double
castWord64ToDouble (Word64 -> Double) -> (BV 64 -> Word64) -> BV 64 -> Double
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 (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
_ -> String -> IO (Some CopilotValue)
forall a. HasCallStack => String -> a
error "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 xe :: XExpr t
xe = case XExpr t
xe of
XInt8 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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)
_ -> 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 sym :: ExprBuilder t st fs
sym tp :: Type a
tp a :: a
a = case Type a
tp of
CT.Bool -> case a
a of
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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
-> Rational
-> IO (SymFloat (ExprBuilder t st fs) Prec32)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> Rational -> 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 (a -> Rational
forall a. Real a => a -> Rational
toRational a
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
-> Rational
-> IO (SymFloat (ExprBuilder t st fs) Prec64)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> Rational -> 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 (a -> Rational
forall a. Real a => a -> Rational
toRational a
a)
CT.Array tp :: 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 n :: 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 Refl -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
forall t. XExpr t
XEmptyArray
Right LeqProof -> do
let Just v :: 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 _ -> 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 tp :: Type t
tp (CT.Field a :: 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 _ = 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 sym :: ExprBuilder t st fs
sym nm :: String
nm tp :: Type a
tp = case Type a
tp of
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
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
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
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
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
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
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
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
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
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
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 itp :: 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 Refl -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
forall t. XExpr t
XEmptyArray
Right 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 "" 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 stp :: 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 ftp :: Type t
ftp _) -> 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 "" 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 sym :: ExprBuilder t st fs
sym streamId :: Int
streamId offset :: 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 xe :: XExpr t
xe -> XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
Nothing -> do
CS.Stream _ _ _ tp :: 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 -> 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 (\st :: 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 sym :: ExprBuilder t st fs
sym tp :: Type a
tp var :: String
var offset :: 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 xe :: XExpr t
xe -> XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
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 (\st :: 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 sym :: ExprBuilder t st fs
sym tp :: Type a
tp var :: String
var ix :: 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 xe :: XExpr t
xe -> XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
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 (\st :: 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 streamId :: 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 sym :: ExprBuilder t st fs
sym offset :: Int
offset e :: Expr a
e = case Expr a
e of
CE.Const tp :: Type a
tp a :: 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 _tp :: Type a
_tp ix :: Word32
ix streamId :: 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
< 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 _ buf :: [a]
buf e :: Expr a
e _ <- 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 _ _ _ _ _ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error "translateExpr: Local unimplemented"
CE.Var _ _ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error "translateExpr: Var unimplemented"
CE.ExternVar tp :: Type a
tp nm :: String
nm _prefix :: 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 op :: Op1 a1 a
op e :: 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 op :: Op2 a1 b a
op e1 :: Expr a1
e1 e2 :: 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
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
powFn <- (TransState t
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType)
-> TransM
t
(ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
forall t.
TransState t
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
pow
ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
logbFn <- (TransState t
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType)
-> TransM
t
(ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
forall t.
TransState t
-> ExprSymFn
t
(Expr 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
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
-> ExprSymFn
t
(Expr 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
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
-> Op2 a b c
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp2 ExprBuilder t st fs
sym ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
powFn ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
logbFn Op2 a1 b a
op XExpr t
xe1 XExpr t
xe2
CE.Op3 op :: Op3 a1 b c a
op e1 :: Expr a1
e1 e2 :: Expr b
e2 e3 :: 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 _ _ _ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error "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 sym :: ExprBuilder t st fs
sym k :: Int
k e :: Expr a
e = do
case Expr a
e of
CE.Const tp :: Type a
tp a :: 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 _tp :: Type a
_tp ix :: Word32
ix streamId :: Int
streamId -> do
CS.Stream _ buf :: [a]
buf e :: Expr a
e tp :: 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 _ _ _ _ _ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error "translateExpr: Local unimplemented"
CE.Var _ _ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error "translateExpr: Var unimplemented"
CE.ExternVar tp :: Type a
tp nm :: String
nm _prefix :: 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 op :: Op1 a1 a
op e :: 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 op :: Op2 a1 b a
op e1 :: Expr a1
e1 e2 :: 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
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
powFn <- (TransState t
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType)
-> TransM
t
(ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
forall t.
TransState t
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
pow
ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
logbFn <- (TransState t
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType)
-> TransM
t
(ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
forall t.
TransState t
-> ExprSymFn
t
(Expr 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
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
-> ExprSymFn
t
(Expr 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
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
-> Op2 a b c
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp2 ExprBuilder t st fs
sym ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
powFn ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
logbFn Op2 a1 b a
op XExpr t
xe1 XExpr t
xe2
CE.Op3 op :: Op3 a1 b c a
op e1 :: Expr a1
e1 e2 :: Expr b
e2 e3 :: 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 _ _ _ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error "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 _ = SymbolRepr s
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol
valueName :: CT.Value a -> Some SymbolRepr
valueName :: Value a -> Some SymbolRepr
valueName (CT.Value _ f :: 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 sym :: ExprBuilder t st fs
sym op :: Op1 a b
op xe :: XExpr t
xe = case (Op1 a b
op, XExpr t
xe) of
(CE.Not, XBool e :: 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
(CE.Not, _) -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
(CE.Abs _, xe :: 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 e :: 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 e :: Expr t (BaseFloatType fpp)
e = do Expr t (BaseFloatType fpp)
zero <- ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> Rational
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> Rational -> 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 0
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 _, xe :: 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 e :: 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 (-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 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 e :: Expr t (BaseFloatType fpp)
e = do Expr t (BaseFloatType fpp)
zero <- ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> Rational
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> Rational -> 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 0
Expr t (BaseFloatType fpp)
neg_one <- ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> Rational
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> Rational -> 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 (-1)
Expr t (BaseFloatType fpp)
pos_one <- ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> Rational
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> Rational -> 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 1
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 _, xe :: 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 e :: Expr t (BaseFloatType fpp)
e = do Expr t (BaseFloatType fpp)
one <- ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> Rational
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> Rational -> 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 1
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 _, xe :: 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 _, xe :: 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 _, xe :: 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 _, xe :: 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 _, xe :: 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 _, xe :: 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 _, xe :: 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 _, xe :: 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 _, xe :: 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 _, xe :: 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 _, xe :: 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 _, xe :: 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 _, xe :: 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 _, xe :: 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 _, xe :: 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 _, xe :: XExpr t
xe) -> case XExpr t
xe of
XBool e :: 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
_ -> (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 _ tp :: Type b
tp, xe :: XExpr t
xe) -> case (XExpr t
xe, Type b
tp) of
(XBool e :: Expr t BaseBoolType
e, 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 e :: Expr t BaseBoolType
e, 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 e :: Expr t BaseBoolType
e, 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 e :: Expr t BaseBoolType
e, 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 e :: Expr t BaseBoolType
e, 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 e :: Expr t BaseBoolType
e, 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 e :: Expr t BaseBoolType
e, 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 e :: Expr t BaseBoolType
e, 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 e :: Expr t BaseBoolType
e, 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 e :: Expr t (BaseBVType 8)
e, 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 e :: Expr t (BaseBVType 8)
e, 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 e :: Expr t (BaseBVType 8)
e, 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 e :: Expr t (BaseBVType 8)
e, 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 e :: Expr t (BaseBVType 16)
e, 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 e :: Expr t (BaseBVType 16)
e, 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 e :: Expr t (BaseBVType 16)
e, 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 e :: Expr t (BaseBVType 32)
e, 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 e :: Expr t (BaseBVType 32)
e, 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 e :: Expr t (BaseBVType 64)
e, 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 e :: Expr t (BaseBVType 8)
e, 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 e :: Expr t (BaseBVType 8)
e, 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 e :: Expr t (BaseBVType 8)
e, 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 e :: Expr t (BaseBVType 8)
e, 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 e :: Expr t (BaseBVType 8)
e, 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 e :: Expr t (BaseBVType 8)
e, 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 e :: Expr t (BaseBVType 8)
e, 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 e :: Expr t (BaseBVType 16)
e, 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 e :: Expr t (BaseBVType 16)
e, 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 e :: Expr t (BaseBVType 16)
e, 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 e :: Expr t (BaseBVType 16)
e, 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 e :: Expr t (BaseBVType 16)
e, 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 e :: Expr t (BaseBVType 32)
e, 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 e :: Expr t (BaseBVType 32)
e, 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 e :: Expr t (BaseBVType 32)
e, 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 e :: Expr t (BaseBVType 64)
e, 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
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
(CE.GetField (CT.Struct s :: a
s) _ftp :: Type b
_ftp extractor :: a -> Field s b
extractor, XStruct xes :: [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 ix :: 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
Nothing -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
_ -> 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 bvOp :: forall (w :: Nat). BVOp1 w t
bvOp fpOp :: forall (fpp :: FloatPrecision). FPOp1 fpp t
fpOp xe :: XExpr t
xe = case XExpr t
xe of
XInt8 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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
_ -> 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 f :: forall (w :: Nat). BVOp1 w t
f xe :: XExpr t
xe = case XExpr t
xe of
XInt8 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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 e :: 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
_ -> 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 g :: forall (fpp :: FloatPrecision). FPOp1 fpp t
g xe :: XExpr t
xe = case XExpr t
xe of
XFloat e :: 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 e :: 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
_ -> 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 h :: RealOp1 t
h xe :: 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 e :: 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 e :: 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 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 (WB.Expr t)
(EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
WT.BaseRealType)
-> (WB.ExprSymFn t (WB.Expr 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
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
-> ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
-> Op2 a b c
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp2 sym :: ExprBuilder t st fs
sym powFn :: ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
powFn logbFn :: ExprSymFn
t
(Expr t)
((EmptyCtx ::> BaseRealType) ::> BaseRealType)
BaseRealType
logbFn op :: Op2 a b c
op xe1 :: XExpr t
xe1 xe2 :: XExpr t
xe2 = case (Op2 a b c
op, XExpr t
xe1, XExpr t
xe2) of
(CE.And, XBool e1 :: Expr t BaseBoolType
e1, XBool e2 :: 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
(CE.Or, XBool e1 :: Expr t BaseBoolType
e1, XBool e2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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' e1 :: Expr t (BaseFloatType fpp)
e1 e2 :: 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
(Expr 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 _, xe1 :: XExpr t
xe1, xe2 :: 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' e1 :: Expr t (BaseFloatType fpp)
e1 e2 :: 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
(Expr 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 e1 :: Expr t BaseBoolType
e1 e2 :: 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 e1 :: BVExpr t w
e1 e2 :: 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 e1 :: Expr t (BaseFloatType fpp)
e1 e2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _, xe1 :: XExpr t
xe1, xe2 :: 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 _ _, xe1 :: XExpr t
xe1, xe2 :: XExpr t
xe2) -> do
Just (SomeBVExpr e1 :: BVExpr t w
e1 w1 :: NatRepr w
w1 _ ctor1 :: 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 e2 :: BVExpr t w
e2 w2 :: NatRepr w
w2 _ _ ) <- 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 -> 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
NatCaseEQ -> BVExpr t w -> IO (BVExpr t w)
forall (m :: * -> *) a. Monad m => a -> m a
return BVExpr t w
e2
NatCaseGT 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 _ _, xe1 :: XExpr t
xe1, xe2 :: XExpr t
xe2) -> do
Just (SomeBVExpr e1 :: BVExpr t w
e1 w1 :: NatRepr w
w1 sgn1 :: BVSign
sgn1 ctor1 :: 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 e2 :: BVExpr t w
e2 w2 :: NatRepr w
w2 _ _ ) <- 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 -> 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
NatCaseEQ -> BVExpr t w -> IO (BVExpr t w)
forall (m :: * -> *) a. Monad m => a -> m a
return BVExpr t w
e2
NatCaseGT 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
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'
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 _, xe1 :: XExpr t
xe1, xe2 :: XExpr t
xe2) -> do
case (XExpr t
xe1, XExpr t
xe2) of
(XArray xes :: Vector n (XExpr t)
xes, XWord32 ix :: 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 0 Expr t (BaseBVType 32)
ix Vector n (XExpr t)
xes
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
_ -> 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 bvOp :: forall (w :: Nat). BVOp2 w t
bvOp fpOp :: forall (fpp :: FloatPrecision). FPOp2 fpp t
fpOp xe1 :: XExpr t
xe1 xe2 :: XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XInt8 e1 :: Expr t (BaseBVType 8)
e1, XInt8 e2 :: 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 e1 :: Expr t (BaseBVType 16)
e1, XInt16 e2 :: 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 e1 :: Expr t (BaseBVType 32)
e1, XInt32 e2 :: 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 e1 :: Expr t (BaseBVType 64)
e1, XInt64 e2 :: 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 e1 :: Expr t (BaseBVType 8)
e1, XWord8 e2 :: 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 e1 :: Expr t (BaseBVType 16)
e1, XWord16 e2 :: 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 e1 :: Expr t (BaseBVType 32)
e1, XWord32 e2 :: 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 e1 :: Expr t (BaseBVType 64)
e1, XWord64 e2 :: 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 e1 :: Expr t (BaseFloatType Prec32)
e1, XFloat e2 :: 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 e1 :: Expr t (BaseFloatType Prec64)
e1, XDouble e2 :: 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
_ -> 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 opS :: forall (w :: Nat). BVOp2 w t
opS opU :: forall (w :: Nat). BVOp2 w t
opU xe1 :: XExpr t
xe1 xe2 :: XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XInt8 e1 :: Expr t (BaseBVType 8)
e1, XInt8 e2 :: 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 e1 :: Expr t (BaseBVType 16)
e1, XInt16 e2 :: 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 e1 :: Expr t (BaseBVType 32)
e1, XInt32 e2 :: 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 e1 :: Expr t (BaseBVType 64)
e1, XInt64 e2 :: 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 e1 :: Expr t (BaseBVType 8)
e1, XWord8 e2 :: 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 e1 :: Expr t (BaseBVType 16)
e1, XWord16 e2 :: 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 e1 :: Expr t (BaseBVType 32)
e1, XWord32 e2 :: 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 e1 :: Expr t (BaseBVType 64)
e1, XWord64 e2 :: 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
_ -> 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 op :: forall (fpp :: FloatPrecision). FPOp2 fpp t
op xe1 :: XExpr t
xe1 xe2 :: XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XFloat e1 :: Expr t (BaseFloatType Prec32)
e1, XFloat e2 :: 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 e1 :: Expr t (BaseFloatType Prec64)
e1, XDouble e2 :: 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
_ -> 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 boolOp :: BoolCmp2 t
boolOp bvOp :: forall (w :: Nat). BVCmp2 w t
bvOp fpOp :: forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp xe1 :: XExpr t
xe1 xe2 :: XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XBool e1 :: Expr t BaseBoolType
e1, XBool e2 :: 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 e1 :: Expr t (BaseBVType 8)
e1, XInt8 e2 :: 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 e1 :: Expr t (BaseBVType 16)
e1, XInt16 e2 :: 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 e1 :: Expr t (BaseBVType 32)
e1, XInt32 e2 :: 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 e1 :: Expr t (BaseBVType 64)
e1, XInt64 e2 :: 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 e1 :: Expr t (BaseBVType 8)
e1, XWord8 e2 :: 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 e1 :: Expr t (BaseBVType 16)
e1, XWord16 e2 :: 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 e1 :: Expr t (BaseBVType 32)
e1, XWord32 e2 :: 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 e1 :: Expr t (BaseBVType 64)
e1, XWord64 e2 :: 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 e1 :: Expr t (BaseFloatType Prec32)
e1, XFloat e2 :: 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 e1 :: Expr t (BaseFloatType Prec64)
e1, XDouble e2 :: 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
_ -> 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 bvSOp :: forall (w :: Nat). BVCmp2 w t
bvSOp bvUOp :: forall (w :: Nat). BVCmp2 w t
bvUOp fpOp :: forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp xe1 :: XExpr t
xe1 xe2 :: XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XInt8 e1 :: Expr t (BaseBVType 8)
e1, XInt8 e2 :: 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 e1 :: Expr t (BaseBVType 16)
e1, XInt16 e2 :: 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 e1 :: Expr t (BaseBVType 32)
e1, XInt32 e2 :: 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 e1 :: Expr t (BaseBVType 64)
e1, XInt64 e2 :: 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 e1 :: Expr t (BaseBVType 8)
e1, XWord8 e2 :: 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 e1 :: Expr t (BaseBVType 16)
e1, XWord16 e2 :: 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 e1 :: Expr t (BaseBVType 32)
e1, XWord32 e2 :: 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 e1 :: Expr t (BaseBVType 64)
e1, XWord64 e2 :: 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 e1 :: Expr t (BaseFloatType Prec32)
e1, XFloat e2 :: 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 e1 :: Expr t (BaseFloatType Prec64)
e1, XDouble e2 :: 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
_ -> 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 sym :: ExprBuilder t st fs
sym curIx :: Word32
curIx ix :: Expr t (BaseBVType 32)
ix xelts :: 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
(xe :: XExpr t
xe, Left Refl) -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
(xe :: XExpr t
xe, Right xelts' :: 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
+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 sym :: ExprBuilder t st fs
sym pred :: Expr t BaseBoolType
pred xe1 :: XExpr t
xe1 xe2 :: XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XBool e1 :: Expr t BaseBoolType
e1, XBool e2 :: 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 e1 :: Expr t (BaseBVType 8)
e1, XInt8 e2 :: 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 e1 :: Expr t (BaseBVType 16)
e1, XInt16 e2 :: 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 e1 :: Expr t (BaseBVType 32)
e1, XInt32 e2 :: 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 e1 :: Expr t (BaseBVType 64)
e1, XInt64 e2 :: 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 e1 :: Expr t (BaseBVType 8)
e1, XWord8 e2 :: 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 e1 :: Expr t (BaseBVType 16)
e1, XWord16 e2 :: 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 e1 :: Expr t (BaseBVType 32)
e1, XWord32 e2 :: 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 e1 :: Expr t (BaseBVType 64)
e1, XWord64 e2 :: 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 e1 :: Expr t (BaseFloatType Prec32)
e1, XFloat e2 :: 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 e1 :: Expr t (BaseFloatType Prec64)
e1, XDouble e2 :: 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 xes1 :: [XExpr t]
xes1, XStruct xes2 :: [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 xes1 :: Vector n (XExpr t)
xes1, XArray xes2 :: 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 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
Nothing -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
_ -> 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 sym :: ExprBuilder t st fs
sym (CE.Mux _) (XBool te :: Expr t BaseBoolType
te) xe1 :: XExpr t
xe1 xe2 :: XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
(XBool e1 :: Expr t BaseBoolType
e1, XBool e2 :: 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 e1 :: Expr t (BaseBVType 8)
e1, XInt8 e2 :: 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 e1 :: Expr t (BaseBVType 16)
e1, XInt16 e2 :: 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 e1 :: Expr t (BaseBVType 32)
e1, XInt32 e2 :: 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 e1 :: Expr t (BaseBVType 64)
e1, XInt64 e2 :: 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 e1 :: Expr t (BaseBVType 8)
e1, XWord8 e2 :: 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 e1 :: Expr t (BaseBVType 16)
e1, XWord16 e2 :: 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 e1 :: Expr t (BaseBVType 32)
e1, XWord32 e2 :: 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 e1 :: Expr t (BaseBVType 64)
e1, XWord64 e2 :: 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 e1 :: Expr t (BaseFloatType Prec32)
e1, XFloat e2 :: 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 e1 :: Expr t (BaseFloatType Prec64)
e1, XDouble e2 :: 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
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
translateOp3 _ _ _ _ _ = IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic