{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures             #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiWayIf                 #-}
{-# LANGUAGE PatternSynonyms            #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeOperators              #-}

-- |
-- Module      : Copilot.Theorem.What4
-- Description : Prove spec properties using What4.
-- Copyright   : (c) Ben Selfridge, 2020
-- Maintainer  : benselfridge@galois.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Spec properties are translated into the language of SMT solvers using
-- @What4@. A backend solver is then used to prove the property is true. The
-- technique is sound, but incomplete. If a property is proved true by this
-- technique, then it can be guaranteed to be true. However, if a property is
-- not proved true, that does not mean it isn't true. Very simple specifications
-- are unprovable by this technique, including:
--
-- @
-- a = True : a
-- @
--
-- The above specification will not be proved true. The reason is that this
-- technique does not perform any sort of induction. When proving the inner @a@
-- expression, the technique merely allocates a fresh constant standing for
-- "@a@, one timestep in the past." Nothing is asserted about the fresh
-- constant.
--
-- An example of a property that is provable by this approach is:
--
-- @
-- a = True : b
-- b = not a
--
-- -- Property: a || b
-- @
--
-- By allocating a fresh constant, @b_-1@, standing for "the value of @b@ one
-- timestep in the past", the equation for @a || b@ at some arbitrary point in
-- the future reduces to @b_-1 || not b_-1@, which is always true.
--
-- In addition to proving that the stream expression is true at some arbitrary
-- point in the future, we also prove it for the first @k@ timesteps, where @k@
-- is the maximum buffer length of all streams in the given spec. This amounts
-- to simply interpreting the spec, although external variables are still
-- represented as constants with unknown values.

module Copilot.Theorem.What4
  ( prove, Solver(..), SatResult(..)
  ) where

import qualified Copilot.Core.Expr       as CE
import qualified Copilot.Core.Operators  as CE
import qualified Copilot.Core.Spec       as CS
import qualified Copilot.Core.Type       as CT
import qualified Copilot.Core.Type.Array as CT

import qualified What4.Config           as WC
import qualified What4.Expr.Builder     as WB
import qualified What4.Expr.GroundEval  as WG
import qualified What4.Interface        as WI
import qualified What4.BaseTypes        as WT
import qualified What4.Solver           as WS
import qualified What4.Solver.DReal     as WS

import qualified Control.Monad.Fail as Fail
import Control.Monad.State
import qualified Data.BitVector.Sized as BV
import Data.Foldable (foldrM)
import Data.List (elemIndex)
import Data.Maybe (fromJust)
import qualified Data.Map as Map
import Data.Parameterized.Classes
import Data.Parameterized.Context hiding (zipWithM)
import Data.Parameterized.NatRepr
import Data.Parameterized.Nonce
import Data.Parameterized.Some
import Data.Parameterized.SymbolRepr
import qualified Data.Parameterized.Vector as V
import Data.Word
import LibBF ( bfToDouble
             , bfFromDouble
             , bfPosZero
             , pattern NearEven )
import GHC.TypeNats (KnownNat)
import qualified Panic as Panic

-- 'prove' function
--
-- To prove properties of a spec, we translate them into What4 using the TransM
-- monad (transformer on top of IO), then negate each property and ask a backend
-- solver to produce a model for the negation.

-- | We assume round-near-even throughout, but this variable can be changed if
-- needed.
fpRM :: WI.RoundingMode
fpRM :: RoundingMode
fpRM = RoundingMode
WI.RNE

-- | No builder state needed.
data BuilderState a = EmptyState

-- | The solvers supported by the what4 backend.
data Solver = CVC4 | DReal | Yices | Z3

-- | The 'prove' function returns results of this form for each property in a
-- spec.
data SatResult = Valid | Invalid | Unknown
  deriving Int -> SatResult -> ShowS
[SatResult] -> ShowS
SatResult -> String
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)]

-- | Attempt to prove all of the properties in a spec via an SMT solver (which
-- must be installed locally on the host). Return an association list mapping
-- the names of each property to the result returned by the solver.
prove :: Solver
      -- ^ Solver to use
      -> CS.Spec
      -- ^ Spec
      -> IO [(CE.Name, SatResult)]
prove :: Solver -> Spec -> IO [(String, SatResult)]
prove Solver
solver Spec
spec = do
  -- Setup symbolic backend
  Some NonceGenerator IO x
ng <- IO (Some (NonceGenerator IO))
newIONonceGenerator
  ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym <- forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
WB.newExprBuilder FloatModeRepr 'FloatIEEE
WB.FloatIEEERepr forall a. BuilderState a
EmptyState NonceGenerator IO x
ng

  -- Solver-specific options
  case Solver
solver of
    Solver
CVC4 -> [ConfigDesc] -> Config -> IO ()
WC.extendConfig [ConfigDesc]
WS.cvc4Options (forall sym. IsExprBuilder sym => sym -> Config
WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym)
    Solver
DReal -> [ConfigDesc] -> Config -> IO ()
WC.extendConfig [ConfigDesc]
WS.drealOptions (forall sym. IsExprBuilder sym => sym -> Config
WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym)
    Solver
Yices -> [ConfigDesc] -> Config -> IO ()
WC.extendConfig [ConfigDesc]
WS.yicesOptions (forall sym. IsExprBuilder sym => sym -> Config
WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym)
    Solver
Z3 -> [ConfigDesc] -> Config -> IO ()
WC.extendConfig [ConfigDesc]
WS.z3Options (forall sym. IsExprBuilder sym => sym -> Config
WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym)

  -- Build up initial translation state
  let streamMap :: Map Int Stream
streamMap = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$
        (\Stream
stream -> (Stream -> Int
CS.streamId Stream
stream, Stream
stream)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec -> [Stream]
CS.specStreams Spec
spec
  ExprSymFn
  x ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
pow <- forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
WI.freshTotalUninterpFn ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym (String -> SolverSymbol
WI.safeSymbol String
"pow") forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  ExprSymFn
  x ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logb <- forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
WI.freshTotalUninterpFn ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym (String -> SolverSymbol
WI.safeSymbol String
"logb") forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  let st :: TransState x
st = forall t.
Map (String, Int) (XExpr t)
-> Map (String, Int) (XExpr t)
-> Map (Int, Int) (XExpr t)
-> Map Int Stream
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> TransState t
TransState forall k a. Map k a
Map.empty forall k a. Map k a
Map.empty forall k a. Map k a
Map.empty Map Int Stream
streamMap ExprSymFn
  x ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
pow ExprSymFn
  x ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logb

  -- Define TransM action for proving properties. Doing this in TransM rather
  -- than IO allows us to reuse the state for each property.
  let proveProperties :: TransM x [(String, SatResult)]
proveProperties = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Spec -> [Property]
CS.specProperties Spec
spec) forall a b. (a -> b) -> a -> b
$ \Property
pr -> do
        let bufLen :: Stream -> Int
bufLen (CS.Stream Int
_ [a]
buf Expr a
_ Type a
_) = forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
buf
            maxBufLen :: Int
maxBufLen = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 forall a. a -> [a] -> [a]
: (Stream -> Int
bufLen forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec -> [Stream]
CS.specStreams Spec
spec))
        [Expr x BaseBoolType]
prefix <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int
0 .. Int
maxBufLen forall a. Num a => a -> a -> a
- Int
1] forall a b. (a -> b) -> a -> b
$ \Int
k -> do
          XBool Expr x BaseBoolType
p <- 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)
          forall (m :: * -> *) a. Monad m => a -> m a
return Expr x BaseBoolType
p
        XBool Expr x BaseBoolType
p <- forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym Int
0 (Property -> Expr Bool
CS.propertyExpr Property
pr)
        Expr x BaseBoolType
p_and_prefix <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym Expr x BaseBoolType
p_and_prefix

        let clauses :: [Expr x BaseBoolType]
clauses = [Expr x BaseBoolType
not_p_and_prefix]
        case Solver
solver of
          Solver
CVC4 -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ \case
            WS.Sat (GroundEvalFn x
_ge, Maybe (ExprRangeBindings x)
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
            WS.Unsat ()
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
            SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
WS.Unknown -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
          Solver
DReal -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ \case
            WS.Sat (WriterConn x (Writer DReal)
_ge, DRealBindings
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
            WS.Unsat ()
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
            SatResult (WriterConn x (Writer DReal), DRealBindings) ()
WS.Unknown -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
          Solver
Yices -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ \case
            WS.Sat GroundEvalFn x
_ge -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
            WS.Unsat ()
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
            SatResult (GroundEvalFn x) ()
WS.Unknown -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
          Solver
Z3 -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ \case
            WS.Sat (GroundEvalFn x
_ge, Maybe (ExprRangeBindings x)
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
            WS.Unsat ()
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
            SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
WS.Unknown -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)

  -- Execute the action and return the results for each property
  ([(String, SatResult)]
res, TransState x
_) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall t a. TransM t a -> StateT (TransState t) IO a
unTransM TransM x [(String, SatResult)]
proveProperties) TransState x
st
  forall (m :: * -> *) a. Monad m => a -> m a
return [(String, SatResult)]
res

-- What4 translation

-- | the state for translating Copilot expressions into What4 expressions. As we
-- translate, we generate fresh symbolic constants for external variables and
-- for stream variables. We need to only generate one constant per variable, so
-- we allocate them in a map. When we need the constant for a particular
-- variable, we check if it is already in the map, and return it if it is; if it
-- isn't, we generate a fresh constant at that point, store it in the map, and
-- return it.
--
-- We also store three immutable fields in this state, rather than wrap them up
-- in another monad transformer layer. These are initialized prior to
-- translation and are never modified. They are the map from stream ids to the
-- core stream definitions, a symbolic uninterpreted function for "pow", and a
-- symbolic uninterpreted function for "logb".
data TransState t = TransState {
  -- | Map of all external variables we encounter during translation. These are
  -- just fresh constants. The offset indicates how many timesteps in the past
  -- this constant represents for that stream.
  forall t. TransState t -> Map (String, Int) (XExpr t)
externVars :: Map.Map (CE.Name, Int) (XExpr t),
  -- | Map of external variables at specific indices (positive), rather than
  -- offset into the past. This is for interpreting streams at specific offsets.
  forall t. TransState t -> Map (String, Int) (XExpr t)
externVarsAt :: Map.Map (CE.Name, Int) (XExpr t),
  -- | Map from (stream id, negative offset) to fresh constant. These are all
  -- constants representing the values of a stream at some point in the past.
  -- The offset (ALWAYS NEGATIVE) indicates how many timesteps in the past
  -- this constant represents for that stream.
  forall t. TransState t -> Map (Int, Int) (XExpr t)
streamConstants :: Map.Map (CE.Id, Int) (XExpr t),
  -- | Map from stream ids to the streams themselves. This value is never
  -- modified, but I didn't want to make this an RWS, so it's represented as a
  -- stateful value.
  forall t. TransState t -> Map Int Stream
streams :: Map.Map CE.Id CS.Stream,
  -- | Binary power operator, represented as an uninterpreted function.
  forall t.
TransState t
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
pow :: WB.ExprSymFn t
         (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
         WT.BaseRealType,
  -- | Binary logarithm operator, represented as an uninterpreted function.
  forall t.
TransState t
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logb :: WB.ExprSymFn t
          (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
          WT.BaseRealType
  }

newtype TransM t a = TransM { forall t a. TransM t a -> StateT (TransState t) IO a
unTransM :: StateT (TransState t) IO a }
  deriving ( 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
<$ :: forall a b. a -> TransM t b -> TransM t a
$c<$ :: forall t a b. a -> TransM t b -> TransM t a
fmap :: forall a b. (a -> b) -> TransM t a -> TransM t b
$cfmap :: forall t a b. (a -> b) -> TransM t a -> TransM t b
Functor
           , 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
<* :: forall a b. TransM t a -> TransM t b -> TransM t a
$c<* :: forall t a b. TransM t a -> TransM t b -> TransM t a
*> :: forall a b. TransM t a -> TransM t b -> TransM t b
$c*> :: forall t a b. TransM t a -> TransM t b -> TransM t b
liftA2 :: forall a b c.
(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
<*> :: forall a b. 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 :: forall a. a -> TransM t a
$cpure :: forall t a. a -> TransM t a
Applicative
           , 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 :: forall a. a -> TransM t a
$creturn :: forall t a. a -> TransM t a
>> :: forall a b. TransM t a -> TransM t b -> TransM t b
$c>> :: forall t a b. TransM t a -> TransM t b -> TransM t b
>>= :: forall a 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
Monad
           , 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 :: forall a. IO a -> TransM t a
$cliftIO :: forall t a. IO a -> TransM t a
MonadIO
           , MonadState (TransState t)
           )

instance Fail.MonadFail (TransM t) where
  fail :: forall a. String -> TransM t a
fail = forall a. HasCallStack => String -> a
error

data CopilotWhat4 = CopilotWhat4

instance Panic.PanicComponent CopilotWhat4 where
  panicComponentName :: CopilotWhat4 -> String
panicComponentName CopilotWhat4
_ = String
"Copilot/What4 translation"
  panicComponentIssues :: CopilotWhat4 -> String
panicComponentIssues CopilotWhat4
_ = String
"https://github.com/Copilot-Language/copilot/issues"

  {-# NOINLINE Panic.panicComponentRevision #-}
  panicComponentRevision :: CopilotWhat4 -> (String, String)
panicComponentRevision = $(Panic.useGitRevision)

-- | Use this function rather than an error monad since it indicates that
-- copilot-core's "reify" function did something incorrectly.
panic :: MonadIO m => m a
panic :: forall (m :: * -> *) a. MonadIO m => m a
panic = forall a b.
(PanicComponent a, HasCallStack) =>
a -> String -> [String] -> b
Panic.panic CopilotWhat4
CopilotWhat4 String
"Copilot.Theorem.What4"
        [ String
"Ill-typed core expression" ]

-- | The What4 representation of a copilot expression. We do not attempt to
-- track the type of the inner expression at the type level, but instead lump
-- everything together into the 'XExpr t' type. The only reason this is a GADT
-- is for the array case; we need to know that the array length is strictly
-- positive.
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
  -- XArray      :: NatRepr n
  --             -> BaseTypeRepr tp
  --             -> Some (WB.Expr t)
  -- XStruct     :: Assignment BaseTypeRepr tps
  --             -> WB.Expr t (BaseStructType tps)
  --             -> XExpr t

deriving instance Show (XExpr t)

data CopilotValue a = CopilotValue { forall a. CopilotValue a -> Type a
cvType :: CT.Type a
                                   , forall a. CopilotValue a -> a
cvVal :: a
                                   }

valFromExpr :: WG.GroundEvalFn t -> XExpr t -> IO (Some CopilotValue)
valFromExpr :: forall t. GroundEvalFn t -> XExpr t -> IO (Some CopilotValue)
valFromExpr GroundEvalFn t
ge XExpr t
xe = case XExpr t
xe of
  XBool Expr t BaseBoolType
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Bool
CT.Bool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t BaseBoolType
e
  XInt8 Expr t (BaseBVType 8)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Int8
CT.Int8 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Natural). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 8)
e
  XInt16 Expr t (BaseBVType 16)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Int16
CT.Int16 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Natural). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 16)
e
  XInt32 Expr t (BaseBVType 32)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Int32
CT.Int32 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Natural). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 32)
e
  XInt64 Expr t (BaseBVType 64)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Int64
CT.Int64 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Natural). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 64)
e
  XWord8 Expr t (BaseBVType 8)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Word8
CT.Word8 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Natural). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 8)
e
  XWord16 Expr t (BaseBVType 16)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Word16
CT.Word16 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Natural). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 16)
e
  XWord32 Expr t (BaseBVType 32)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Word32
CT.Word32 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Natural). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 32)
e
  XWord64 Expr t (BaseBVType 64)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Word64
CT.Word64 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Natural). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseBVType 64)
e
  XFloat Expr t (BaseFloatType Prec32)
e ->
    forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Float
CT.Float forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Real a, Fractional b) => a -> b
realToFrac forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. RoundMode -> BigFloat -> (Double, Status)
bfToDouble RoundMode
NearEven forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseFloatType Prec32)
e
  XDouble Expr t (BaseFloatType Prec64)
e ->
    forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Double
CT.Double forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. RoundMode -> BigFloat -> (Double, Status)
bfToDouble RoundMode
NearEven forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge Expr t (BaseFloatType Prec64)
e
  XExpr t
_ -> forall a. HasCallStack => String -> a
error String
"valFromExpr unhandled case"
  where
    fromBV :: forall a w . Num a => BV.BV w -> a
    fromBV :: forall a (w :: Natural). Num a => BV w -> a
fromBV = forall a. Num a => Integer -> a
fromInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: Natural). BV w -> Integer
BV.asUnsigned

-- | A view of an XExpr as a bitvector expression, a natrepr for its width, its
-- signed/unsigned status, and the constructor used to reconstruct an XExpr from
-- it. This is a useful view for translation, as many of the operations can be
-- grouped together for all words\/ints\/floats.
data SomeBVExpr t where
  SomeBVExpr :: 1 <= w
             => WB.BVExpr t w
             -> NatRepr w
             -> BVSign
             -> (WB.BVExpr t w -> XExpr t)
             -> SomeBVExpr t

-- | The sign of a bitvector -- this indicates whether it is to be interpreted
-- as a signed 'Int' or an unsigned 'Word'.
data BVSign = Signed | Unsigned

-- | If the inner expression can be viewed as a bitvector, we project out a view
-- of it as such.
asBVExpr :: XExpr t -> Maybe (SomeBVExpr t)
asBVExpr :: forall t. XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe = case XExpr t
xe of
  XInt8 Expr t (BaseBVType 8)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) t.
(1 <= n) =>
BVExpr t n
-> NatRepr n -> BVSign -> (BVExpr t n -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 8)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Signed forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8)
  XInt16 Expr t (BaseBVType 16)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) t.
(1 <= n) =>
BVExpr t n
-> NatRepr n -> BVSign -> (BVExpr t n -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 16)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Signed forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16)
  XInt32 Expr t (BaseBVType 32)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) t.
(1 <= n) =>
BVExpr t n
-> NatRepr n -> BVSign -> (BVExpr t n -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 32)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Signed forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32)
  XInt64 Expr t (BaseBVType 64)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) t.
(1 <= n) =>
BVExpr t n
-> NatRepr n -> BVSign -> (BVExpr t n -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 64)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Signed forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64)
  XWord8 Expr t (BaseBVType 8)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) t.
(1 <= n) =>
BVExpr t n
-> NatRepr n -> BVSign -> (BVExpr t n -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 8)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Unsigned forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8)
  XWord16 Expr t (BaseBVType 16)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) t.
(1 <= n) =>
BVExpr t n
-> NatRepr n -> BVSign -> (BVExpr t n -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 16)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Unsigned forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16)
  XWord32 Expr t (BaseBVType 32)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) t.
(1 <= n) =>
BVExpr t n
-> NatRepr n -> BVSign -> (BVExpr t n -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 32)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Unsigned forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32)
  XWord64 Expr t (BaseBVType 64)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) t.
(1 <= n) =>
BVExpr t n
-> NatRepr n -> BVSign -> (BVExpr t n -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 64)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Unsigned forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64)
  XExpr t
_ -> forall a. Maybe a
Nothing

-- | Translate a constant expression by creating a what4 literal and packaging
-- it up into an 'XExpr'.
translateConstExpr :: forall a t st fs .
                      WB.ExprBuilder t st fs
                   -> CT.Type a
                   -> a
                   -> IO (XExpr t)
translateConstExpr :: 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 = case Type a
tp of
  Type a
CT.Bool -> case a
a of
    a
Bool
True  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Expr t BaseBoolType -> XExpr t
XBool (forall sym. IsExprBuilder sym => sym -> Pred sym
WI.truePred ExprBuilder t st fs
sym)
    a
Bool
False -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Expr t BaseBoolType -> XExpr t
XBool (forall sym. IsExprBuilder sym => sym -> Pred sym
WI.falsePred ExprBuilder t st fs
sym)
  Type a
CT.Int8 -> forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Int8 -> BV 8
BV.int8 a
a)
  Type a
CT.Int16 -> forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Int16 -> BV 16
BV.int16 a
a)
  Type a
CT.Int32 -> forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Int32 -> BV 32
BV.int32 a
a)
  Type a
CT.Int64 -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Int64 -> BV 64
BV.int64 a
a)
  Type a
CT.Word8 -> forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Word8 -> BV 8
BV.word8 a
a)
  Type a
CT.Word16 -> forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Word16 -> BV 16
BV.word16 a
a)
  Type a
CT.Word32 -> forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Word32 -> BV 32
BV.word32 a
a)
  Type a
CT.Word64 -> forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Word64 -> BV 64
BV.word64 a
a)
  Type a
CT.Float -> forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (Double -> BigFloat
bfFromDouble (forall a b. (Real a, Fractional b) => a -> b
realToFrac a
a))
  Type a
CT.Double -> forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (Double -> BigFloat
bfFromDouble a
a)
  CT.Array Type t
tp -> do
    [XExpr t]
elts <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a t (st :: * -> *) fs.
ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
translateConstExpr ExprBuilder t st fs
sym Type t
tp) (forall (n :: Natural) a. Array n a -> [a]
CT.arrayelems a
a)
    Just (Some NatRepr x
n) <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Maybe (Some NatRepr)
someNat (forall (t :: * -> *) a. Foldable t => t a -> Int
length [XExpr t]
elts)
    case forall (n :: Natural). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 NatRepr x
n of
      Left x :~: 0
Refl -> forall (m :: * -> *) a. Monad m => a -> m a
return forall t. XExpr t
XEmptyArray
      Right LeqProof 1 x
LeqProof -> do
        let Just Vector x (XExpr t)
v = forall (n :: Natural) a.
(1 <= n) =>
NatRepr n -> [a] -> Maybe (Vector n a)
V.fromList NatRepr x
n [XExpr t]
elts
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) t. (1 <= n) => Vector n (XExpr t) -> XExpr t
XArray Vector x (XExpr t)
v
  CT.Struct a
_ -> do
    [XExpr t]
elts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. Struct a => a -> [Value a]
CT.toValues a
a) forall a b. (a -> b) -> a -> b
$ \(CT.Value Type t
tp (CT.Field t
a)) ->
      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
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [XExpr t] -> XExpr t
XStruct [XExpr t]
elts

arrayLen :: KnownNat n => CT.Type (CT.Array n t) -> NatRepr n
arrayLen :: forall (n :: Natural) t.
KnownNat n =>
Type (Array n t) -> NatRepr n
arrayLen Type (Array n t)
_ = forall (n :: Natural). KnownNat n => NatRepr n
knownNat

-- | Generate a fresh constant for a given copilot type. This will be called
-- whenever we attempt to get the constant for a given external variable or
-- stream variable, but that variable has not been accessed yet and therefore
-- has no constant allocated.
freshCPConstant :: forall t st fs a .
                   WB.ExprBuilder t st fs
                -> String
                -> CT.Type a
                -> IO (XExpr t)
freshCPConstant :: 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 = case Type a
tp of
  Type a
CT.Bool -> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Int8 -> forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Int16 -> forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Int32 -> forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Int64 -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Word8 -> forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Word16 -> forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Word32 -> forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Word64 -> forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Float -> forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Double -> forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  atp :: Type a
atp@(CT.Array Type t
itp) -> do
    NatRepr n
n <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) t.
KnownNat n =>
Type (Array n t) -> NatRepr n
arrayLen Type a
atp
    case forall (n :: Natural). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 NatRepr n
n of
      Left n :~: 0
Refl -> forall (m :: * -> *) a. Monad m => a -> m a
return forall t. XExpr t
XEmptyArray
      Right LeqProof 1 n
LeqProof -> do
        ((n - 1) + 1) :~: n
Refl <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: Natural -> *) (m :: Natural) (g :: Natural -> *)
       (n :: Natural).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel NatRepr n
n (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1)
        Vector ((n - 1) + 1) (XExpr t)
elts :: V.Vector n (XExpr t) <- forall (m :: * -> *) (h :: Natural) a.
Monad m =>
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> m a)
-> m (Vector (h + 1) a)
V.generateM (forall (n :: Natural). (1 <= n) => NatRepr n -> NatRepr (n - 1)
decNat NatRepr n
n) (forall a b. a -> b -> a
const (forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
"" Type t
itp))
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) t. (1 <= n) => Vector n (XExpr t) -> XExpr t
XArray Vector ((n - 1) + 1) (XExpr t)
elts
  CT.Struct a
stp -> do
    [XExpr t]
elts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. Struct a => a -> [Value a]
CT.toValues a
stp) forall a b. (a -> b) -> a -> b
$ \(CT.Value Type t
ftp Field s t
_) -> forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
"" Type t
ftp
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [XExpr t] -> XExpr t
XStruct [XExpr t]
elts

-- | Get the constant for a given stream id and some offset into the past. This
-- should only be called with a strictly negative offset. When this function
-- gets called for the first time for a given (streamId, offset) pair, it
-- generates a fresh constant and stores it in an internal map. Thereafter, this
-- function will just return that constant when called with the same pair.
getStreamConstant :: WB.ExprBuilder t st fs -> CE.Id -> Int -> TransM t (XExpr t)
getStreamConstant :: forall t (st :: * -> *) fs.
ExprBuilder t st fs -> Int -> Int -> TransM t (XExpr t)
getStreamConstant ExprBuilder t st fs
sym Int
streamId Int
offset = do
  Map (Int, Int) (XExpr t)
scs <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall t. TransState t -> Map (Int, Int) (XExpr t)
streamConstants
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Int
streamId, Int
offset) Map (Int, Int) (XExpr t)
scs of
    Just XExpr t
xe -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
    Maybe (XExpr t)
Nothing -> do
      CS.Stream Int
_ [a]
_ Expr a
_ Type a
tp <- forall t. Int -> TransM t Stream
getStreamDef Int
streamId
      let nm :: String
nm = forall a. Show a => a -> String
show Int
streamId forall a. [a] -> [a] -> [a]
++ String
"_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
offset
      XExpr t
xe <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TransState t
st -> TransState t
st { streamConstants :: Map (Int, Int) (XExpr t)
streamConstants = 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 })
      forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe

-- | Get the constant for a given external variable and some offset into the
-- past. This should only be called with a strictly negative offset. When this
-- function gets called for the first time for a given (var, offset) pair, it
-- generates a fresh constant and stores it in an internal map. Thereafter, this
-- function will just return that constant when called with the same pair.
getExternConstant :: WB.ExprBuilder t st fs
                  -> CT.Type a
                  -> CE.Name
                  -> Int
                  -> TransM t (XExpr t)
getExternConstant :: 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
var Int
offset = do
  Map (String, Int) (XExpr t)
es <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall t. TransState t -> Map (String, Int) (XExpr t)
externVars
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (String
var, Int
offset) Map (String, Int) (XExpr t)
es of
    Just XExpr t
xe -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
    Maybe (XExpr t)
Nothing -> do
      XExpr t
xe <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TransState t
st -> TransState t
st { externVars :: Map (String, Int) (XExpr t)
externVars = 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} )
      forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe

-- | Get the constant for a given external variable at some specific timestep.
getExternConstantAt :: WB.ExprBuilder t st fs
                    -> CT.Type a
                    -> CE.Name
                    -> Int
                    -> TransM t (XExpr t)
getExternConstantAt :: 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
var Int
ix = do
  Map (String, Int) (XExpr t)
es <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall t. TransState t -> Map (String, Int) (XExpr t)
externVarsAt
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (String
var, Int
ix) Map (String, Int) (XExpr t)
es of
    Just XExpr t
xe -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
    Maybe (XExpr t)
Nothing -> do
      XExpr t
xe <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TransState t
st -> TransState t
st { externVarsAt :: Map (String, Int) (XExpr t)
externVarsAt = 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} )
      forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe

-- | Retrieve a stream definition given its id.
getStreamDef :: CE.Id -> TransM t CS.Stream
getStreamDef :: forall t. Int -> TransM t Stream
getStreamDef Int
streamId = forall a. HasCallStack => Maybe a -> a
fromJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
streamId forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. TransState t -> Map Int Stream
streams)

-- | Translate an expression into a what4 representation. The int offset keeps
-- track of how many timesteps into the past each variable is referring to.
-- Initially the value should be zero, but when we translate a stream, the
-- offset is recomputed based on the length of that stream's prefix (subtracted)
-- and the drop index (added).
translateExpr :: WB.ExprBuilder t st fs
              -> Int
              -- ^ number of timesteps in the past we are currently looking
              -- (must always be <= 0)
              -> CE.Expr a
              -> TransM t (XExpr t)
translateExpr :: 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 a
e = case Expr a
e of
  CE.Const Type a
tp a
a -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a t (st :: * -> *) fs.
ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
translateConstExpr ExprBuilder t st fs
sym Type a
tp a
a
  CE.Drop Type a
_tp Word32
ix Int
streamId
    -- If we are referencing a past value of this stream, just return an
    -- unconstrained constant.
    | Int
offset forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
ix forall a. Ord a => a -> a -> Bool
< Int
0 ->
        forall t (st :: * -> *) fs.
ExprBuilder t st fs -> Int -> Int -> TransM t (XExpr t)
getStreamConstant ExprBuilder t st fs
sym Int
streamId (Int
offset forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
ix)
    -- If we are referencing a current or future value of this stream, we need
    -- to translate the stream's expression, using an offset computed based on
    -- the current offset (negative or 0), the drop index (positive or 0), and
    -- the length of the stream's buffer (subtracted).
    | Bool
otherwise -> do
      CS.Stream Int
_ [a]
buf Expr a
e Type a
_ <- forall t. Int -> TransM t Stream
getStreamDef Int
streamId
      forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym (Int
offset forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
ix forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
buf) Expr a
e
  CE.Local Type a1
_ Type a
_ String
_ Expr a1
_ Expr a
_ -> forall a. HasCallStack => String -> a
error String
"translateExpr: Local unimplemented"
  CE.Var Type a
_ String
_ -> forall a. HasCallStack => String -> a
error String
"translateExpr: Var unimplemented"
  CE.ExternVar Type a
tp String
nm Maybe [a]
_prefix -> forall t (st :: * -> *) fs a.
ExprBuilder t st fs
-> Type a -> String -> Int -> TransM t (XExpr t)
getExternConstant ExprBuilder t st fs
sym Type a
tp String
nm Int
offset
  CE.Op1 Op1 a1 a
op Expr a1
e -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr a1
e
  CE.Op2 Op2 a1 b a
op Expr a1
e1 Expr b
e2 -> do
    XExpr t
xe1 <- 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 <- forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr b
e2
    ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall t.
TransState t
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
pow
    ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall t.
TransState t
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logb
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall t (st :: * -> *) fs a b c.
ExprBuilder t st fs
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> Op2 a b c
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp2 ExprBuilder t st fs
sym ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn Op2 a1 b a
op XExpr t
xe1 XExpr t
xe2
  CE.Op3 Op3 a1 b c a
op Expr a1
e1 Expr b
e2 Expr c
e3 -> do
    XExpr t
xe1 <- 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 <- 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 <- 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
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall t (st :: * -> *) fs a b c d.
ExprBuilder t st fs
-> Op3 a b c d -> XExpr t -> XExpr t -> XExpr t -> IO (XExpr t)
translateOp3 ExprBuilder t st fs
sym Op3 a1 b c a
op XExpr t
xe1 XExpr t
xe2 XExpr t
xe3
  CE.Label Type a
_ String
_ Expr a
_ -> forall a. HasCallStack => String -> a
error String
"translateExpr: Label unimplemented"

-- | Translate an expression into a what4 representation at a /specific/
-- timestep, rather than "at some indeterminate point in the future."
translateExprAt :: WB.ExprBuilder t st fs
                -> Int
                -- ^ Index of timestep
                -> CE.Expr a
                -- ^ stream expression
                -> TransM t (XExpr t)
translateExprAt :: 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 a
e = do
  case Expr a
e of
    CE.Const Type a
tp a
a -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a t (st :: * -> *) fs.
ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
translateConstExpr ExprBuilder t st fs
sym Type a
tp a
a
    CE.Drop Type a
_tp Word32
ix Int
streamId -> do
      CS.Stream Int
_ [a]
buf Expr a
e Type a
tp <- forall t. Int -> TransM t Stream
getStreamDef Int
streamId
      if Int
k' forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
buf
        then forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 forall a. [a] -> Int -> a
!! Int
k')
        else forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExprAt ExprBuilder t st fs
sym (Int
k' forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
buf) Expr a
e
      where
        k' :: Int
k' = Int
k forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
ix
    CE.Local Type a1
_ Type a
_ String
_ Expr a1
_ Expr a
_ -> forall a. HasCallStack => String -> a
error String
"translateExpr: Local unimplemented"
    CE.Var Type a
_ String
_ -> forall a. HasCallStack => String -> a
error String
"translateExpr: Var unimplemented"
    CE.ExternVar Type a
tp String
nm Maybe [a]
_prefix -> forall t (st :: * -> *) fs a.
ExprBuilder t st fs
-> Type a -> String -> Int -> TransM t (XExpr t)
getExternConstantAt ExprBuilder t st fs
sym Type a
tp String
nm Int
k
    CE.Op1 Op1 a1 a
op Expr a1
e -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExprAt ExprBuilder t st fs
sym Int
k Expr a1
e
    CE.Op2 Op2 a1 b a
op Expr a1
e1 Expr b
e2 -> do
      XExpr t
xe1 <- 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 <- forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExprAt ExprBuilder t st fs
sym Int
k Expr b
e2
      ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall t.
TransState t
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
pow
      ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall t.
TransState t
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logb
      forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall t (st :: * -> *) fs a b c.
ExprBuilder t st fs
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> Op2 a b c
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp2 ExprBuilder t st fs
sym ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn Op2 a1 b a
op XExpr t
xe1 XExpr t
xe2
    CE.Op3 Op3 a1 b c a
op Expr a1
e1 Expr b
e2 Expr c
e3 -> do
      XExpr t
xe1 <- 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 <- 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 <- 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
      forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall t (st :: * -> *) fs a b c d.
ExprBuilder t st fs
-> Op3 a b c d -> XExpr t -> XExpr t -> XExpr t -> IO (XExpr t)
translateOp3 ExprBuilder t st fs
sym Op3 a1 b c a
op XExpr t
xe1 XExpr t
xe2 XExpr t
xe3
    CE.Label Type a
_ String
_ Expr a
_ -> forall a. HasCallStack => String -> a
error String
"translateExpr: Label unimplemented"

type BVOp1 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> IO (WB.BVExpr t w)

type FPOp1 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.Expr t (WT.BaseFloatType fpp))

type RealOp1 t = WB.Expr t WT.BaseRealType -> IO (WB.Expr t WT.BaseRealType)

fieldName :: KnownSymbol s => CT.Field s a -> SymbolRepr s
fieldName :: forall (s :: Symbol) a. KnownSymbol s => Field s a -> SymbolRepr s
fieldName Field s a
_ = forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol

valueName :: CT.Value a -> Some SymbolRepr
valueName :: forall a. Value a -> Some SymbolRepr
valueName (CT.Value Type t
_ Field s t
f) = forall k (f :: k -> *) (x :: k). f x -> Some f
Some (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 :: 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 a b
op XExpr t
xe = case (Op1 a b
op, XExpr t
xe) of
  (Op1 a b
CE.Not, XBool Expr t BaseBoolType
e) -> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder t st fs
sym Expr t BaseBoolType
e
  (Op1 a b
CE.Not, XExpr t
_) -> forall (m :: * -> *) a. MonadIO m => m a
panic
  (CE.Abs Type a
_, XExpr t
xe) -> (forall (w :: Natural). BVOp1 w t)
-> (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t
-> IO (XExpr t)
numOp forall (w :: Natural). BVOp1 w t
bvAbs forall (fpp :: FloatPrecision). FPOp1 fpp t
fpAbs XExpr t
xe
    where
      bvAbs :: BVOp1 w t
      bvAbs :: forall (w :: Natural). BVOp1 w t
bvAbs BVExpr t w
e = do BVExpr t w
zero <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (forall (w :: Natural). NatRepr w -> BV w
BV.zero forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
                   Expr t BaseBoolType
e_neg <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSlt ExprBuilder t st fs
sym BVExpr t w
e BVExpr t w
zero
                   BVExpr t w
neg_e <- forall sym (w :: Natural).
(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
zero BVExpr t w
e
                   forall sym (w :: Natural).
(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
e_neg BVExpr t w
neg_e BVExpr t w
e
      fpAbs :: FPOp1 fpp t
      fpAbs :: forall (fpp :: FloatPrecision). FPOp1 fpp t
fpAbs Expr t (BaseFloatType fpp)
e = do Expr t (BaseFloatType fpp)
zero <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr BigFloat
bfPosZero
                   Expr t BaseBoolType
e_neg <- 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)
e Expr t (BaseFloatType fpp)
zero
                   Expr t (BaseFloatType fpp)
neg_e <- 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)
zero Expr t (BaseFloatType fpp)
e
                   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
e_neg Expr t (BaseFloatType fpp)
neg_e Expr t (BaseFloatType fpp)
e
  (CE.Sign Type a
_, XExpr t
xe) -> (forall (w :: Natural). BVOp1 w t)
-> (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t
-> IO (XExpr t)
numOp forall (w :: Natural). BVOp1 w t
bvSign forall (fpp :: FloatPrecision). FPOp1 fpp t
fpSign XExpr t
xe
    where
      bvSign :: BVOp1 w t
      bvSign :: forall (w :: Natural). BVOp1 w t
bvSign BVExpr t w
e = do BVExpr t w
zero <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (forall (w :: Natural). NatRepr w -> BV w
BV.zero forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
                    BVExpr t w
neg_one <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV forall (n :: Natural). KnownNat n => NatRepr n
knownNat (-Integer
1))
                    BVExpr t w
pos_one <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV forall (n :: Natural). KnownNat n => NatRepr n
knownNat Integer
1)
                    Expr t BaseBoolType
e_zero <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq ExprBuilder t st fs
sym BVExpr t w
e BVExpr t w
zero
                    Expr t BaseBoolType
e_neg <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSlt ExprBuilder t st fs
sym BVExpr t w
e BVExpr t w
zero
                    BVExpr t w
t <- forall sym (w :: Natural).
(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
e_neg BVExpr t w
neg_one BVExpr t w
pos_one
                    forall sym (w :: Natural).
(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
e_zero BVExpr t w
zero BVExpr t w
t
      fpSign :: FPOp1 fpp t
      fpSign :: forall (fpp :: FloatPrecision). FPOp1 fpp t
fpSign Expr t (BaseFloatType fpp)
e = do Expr t (BaseFloatType fpp)
zero <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr BigFloat
bfPosZero
                    Expr t (BaseFloatType fpp)
neg_one <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (Double -> BigFloat
bfFromDouble (-Double
1.0))
                    Expr t (BaseFloatType fpp)
pos_one <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (Double -> BigFloat
bfFromDouble Double
1.0)
                    Expr t BaseBoolType
e_zero <- 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)
e Expr t (BaseFloatType fpp)
zero
                    Expr t BaseBoolType
e_neg <- 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)
e Expr t (BaseFloatType fpp)
zero
                    Expr t (BaseFloatType fpp)
t <- 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
e_neg Expr t (BaseFloatType fpp)
neg_one Expr t (BaseFloatType fpp)
pos_one
                    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
e_zero Expr t (BaseFloatType fpp)
zero Expr t (BaseFloatType fpp)
t
  (CE.Recip Type a
_, XExpr t
xe) -> (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp1 fpp t
recip XExpr t
xe
    where
      recip :: FPOp1 fpp t
      recip :: forall (fpp :: FloatPrecision). FPOp1 fpp t
recip Expr t (BaseFloatType fpp)
e = do Expr t (BaseFloatType fpp)
one <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
WI.floatLit ExprBuilder t st fs
sym forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (Double -> BigFloat
bfFromDouble Double
1.0)
                   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)
one Expr t (BaseFloatType fpp)
e
  (CE.Exp Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realExp ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Sqrt Type a
_, XExpr t
xe) -> (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t -> IO (XExpr t)
fpOp (forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
WI.floatSqrt ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe
  (CE.Log Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realLog ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Sin Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realSin ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Cos Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realCos ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Tan Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realTan ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Asin Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (RealOp1 t
realRecip forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realSin ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Acos Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (RealOp1 t
realRecip forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realCos ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Atan Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (RealOp1 t
realRecip forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realTan ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Sinh Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realSinh ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Cosh Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realCosh ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Tanh Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realTanh ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Asinh Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (RealOp1 t
realRecip forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realSinh ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Acosh Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (RealOp1 t
realRecip forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realCosh ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Atanh Type a
_, XExpr t
xe) -> RealOp1 t -> XExpr t -> IO (XExpr t)
realOp (RealOp1 t
realRecip forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
WI.realTanh ExprBuilder t st fs
sym) XExpr t
xe
  (CE.BwNot Type a
_, XExpr t
xe) -> case XExpr t
xe of
    XBool Expr t BaseBoolType
e -> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder t st fs
sym Expr t BaseBoolType
e
    XExpr t
_ -> (forall (w :: Natural). BVOp1 w t) -> XExpr t -> IO (XExpr t)
bvOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
WI.bvNotBits ExprBuilder t st fs
sym) XExpr t
xe
  (CE.Cast Type a
_ Type b
tp, XExpr t
xe) -> case (XExpr t
xe, Type b
tp) of
    (XBool Expr t BaseBoolType
e, Type b
CT.Bool) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Expr t BaseBoolType -> XExpr t
XBool Expr t BaseBoolType
e
    (XBool Expr t BaseBoolType
e, Type b
CT.Word8) -> forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
    (XBool Expr t BaseBoolType
e, Type b
CT.Word16) -> forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
    (XBool Expr t BaseBoolType
e, Type b
CT.Word32) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
    (XBool Expr t BaseBoolType
e, Type b
CT.Word64) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
    (XBool Expr t BaseBoolType
e, Type b
CT.Int8) -> forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
    (XBool Expr t BaseBoolType
e, Type b
CT.Int16) -> forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
    (XBool Expr t BaseBoolType
e, Type b
CT.Int32) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
    (XBool Expr t BaseBoolType
e, Type b
CT.Int64) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV ExprBuilder t st fs
sym Expr t BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
    (XInt8 Expr t (BaseBVType 8)
e, Type b
CT.Int8) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 Expr t (BaseBVType 8)
e
    (XInt8 Expr t (BaseBVType 8)
e, Type b
CT.Int16) -> forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
e
    (XInt8 Expr t (BaseBVType 8)
e, Type b
CT.Int32) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
e
    (XInt8 Expr t (BaseBVType 8)
e, Type b
CT.Int64) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
e
    (XInt16 Expr t (BaseBVType 16)
e, Type b
CT.Int16) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 Expr t (BaseBVType 16)
e
    (XInt16 Expr t (BaseBVType 16)
e, Type b
CT.Int32) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 16)
e
    (XInt16 Expr t (BaseBVType 16)
e, Type b
CT.Int64) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 16)
e
    (XInt32 Expr t (BaseBVType 32)
e, Type b
CT.Int32) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 Expr t (BaseBVType 32)
e
    (XInt32 Expr t (BaseBVType 32)
e, Type b
CT.Int64) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 32)
e
    (XInt64 Expr t (BaseBVType 64)
e, Type b
CT.Int64) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 Expr t (BaseBVType 64)
e
    (XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Int16) -> forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
e
    (XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Int32) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
e
    (XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Int64) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
e
    (XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Word8) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 Expr t (BaseBVType 8)
e
    (XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Word16) -> forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
e
    (XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Word32) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
e
    (XWord8 Expr t (BaseBVType 8)
e, Type b
CT.Word64) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 8)
e
    (XWord16 Expr t (BaseBVType 16)
e, Type b
CT.Int32) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 16)
e
    (XWord16 Expr t (BaseBVType 16)
e, Type b
CT.Int64) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 16)
e
    (XWord16 Expr t (BaseBVType 16)
e, Type b
CT.Word16) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 Expr t (BaseBVType 16)
e
    (XWord16 Expr t (BaseBVType 16)
e, Type b
CT.Word32) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 16)
e
    (XWord16 Expr t (BaseBVType 16)
e, Type b
CT.Word64) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 16)
e
    (XWord32 Expr t (BaseBVType 32)
e, Type b
CT.Int64) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 32)
e
    (XWord32 Expr t (BaseBVType 32)
e, Type b
CT.Word32) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 Expr t (BaseBVType 32)
e
    (XWord32 Expr t (BaseBVType 32)
e, Type b
CT.Word64) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat Expr t (BaseBVType 32)
e
    (XWord64 Expr t (BaseBVType 64)
e, Type b
CT.Word64) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 Expr t (BaseBVType 64)
e
    (XExpr t, Type b)
_ -> forall (m :: * -> *) a. MonadIO m => m a
panic
  (CE.GetField (CT.Struct a
s) Type b
_ftp a -> Field s b
extractor, XStruct [XExpr t]
xes) -> do
    let fieldNameRepr :: SymbolRepr s
fieldNameRepr = forall (s :: Symbol) a. KnownSymbol s => Field s a -> SymbolRepr s
fieldName (a -> Field s b
extractor forall a. HasCallStack => a
undefined)
    let structFieldNameReprs :: [Some SymbolRepr]
structFieldNameReprs = forall a. Value a -> Some SymbolRepr
valueName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Struct a => a -> [Value a]
CT.toValues a
s
    let mIx :: Maybe Int
mIx = forall a. Eq a => a -> [a] -> Maybe Int
elemIndex (forall k (f :: k -> *) (x :: k). f x -> Some f
Some SymbolRepr s
fieldNameRepr) [Some SymbolRepr]
structFieldNameReprs
    case Maybe Int
mIx of
      Just Int
ix -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [XExpr t]
xes forall a. [a] -> Int -> a
!! Int
ix
      Maybe Int
Nothing -> forall (m :: * -> *) a. MonadIO m => m a
panic
  (Op1 a b, 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 :: Natural). BVOp1 w t)
-> (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t
-> IO (XExpr t)
numOp forall (w :: Natural). BVOp1 w t
bvOp forall (fpp :: FloatPrecision). FPOp1 fpp t
fpOp XExpr t
xe = case XExpr t
xe of
      XInt8 Expr t (BaseBVType 8)
e -> forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
bvOp Expr t (BaseBVType 8)
e
      XInt16 Expr t (BaseBVType 16)
e -> forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
bvOp Expr t (BaseBVType 16)
e
      XInt32 Expr t (BaseBVType 32)
e -> forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
bvOp Expr t (BaseBVType 32)
e
      XInt64 Expr t (BaseBVType 64)
e -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
bvOp Expr t (BaseBVType 64)
e
      XWord8 Expr t (BaseBVType 8)
e -> forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
bvOp Expr t (BaseBVType 8)
e
      XWord16 Expr t (BaseBVType 16)
e -> forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
bvOp Expr t (BaseBVType 16)
e
      XWord32 Expr t (BaseBVType 32)
e -> forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
bvOp Expr t (BaseBVType 32)
e
      XWord64 Expr t (BaseBVType 64)
e -> forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
bvOp Expr t (BaseBVType 64)
e
      XFloat Expr t (BaseFloatType Prec32)
e -> forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision). FPOp1 fpp t
fpOp Expr t (BaseFloatType Prec32)
e
      XDouble Expr t (BaseFloatType Prec64)
e -> forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision). FPOp1 fpp t
fpOp Expr t (BaseFloatType Prec64)
e
      XExpr t
_ -> forall (m :: * -> *) a. MonadIO m => m a
panic

    bvOp :: (forall w . BVOp1 w t) -> XExpr t -> IO (XExpr t)
    bvOp :: (forall (w :: Natural). BVOp1 w t) -> XExpr t -> IO (XExpr t)
bvOp forall (w :: Natural). BVOp1 w t
f XExpr t
xe = case XExpr t
xe of
      XInt8 Expr t (BaseBVType 8)
e -> forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
f Expr t (BaseBVType 8)
e
      XInt16 Expr t (BaseBVType 16)
e -> forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
f Expr t (BaseBVType 16)
e
      XInt32 Expr t (BaseBVType 32)
e -> forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
f Expr t (BaseBVType 32)
e
      XInt64 Expr t (BaseBVType 64)
e -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
f Expr t (BaseBVType 64)
e
      XWord8 Expr t (BaseBVType 8)
e -> forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
f Expr t (BaseBVType 8)
e
      XWord16 Expr t (BaseBVType 16)
e -> forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
f Expr t (BaseBVType 16)
e
      XWord32 Expr t (BaseBVType 32)
e -> forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
f Expr t (BaseBVType 32)
e
      XWord64 Expr t (BaseBVType 64)
e -> forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 w t
f Expr t (BaseBVType 64)
e
      XExpr t
_ -> forall (m :: * -> *) a. MonadIO m => m a
panic

    fpOp :: (forall fpp . FPOp1 fpp t) -> XExpr t -> IO (XExpr t)
    fpOp :: (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp1 fpp t
g XExpr t
xe = case XExpr t
xe of
      XFloat Expr t (BaseFloatType Prec32)
e -> forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision). FPOp1 fpp t
g Expr t (BaseFloatType Prec32)
e
      XDouble Expr t (BaseFloatType Prec64)
e -> forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision). FPOp1 fpp t
g Expr t (BaseFloatType Prec64)
e
      XExpr t
_ -> forall (m :: * -> *) a. MonadIO m => m a
panic

    realOp :: RealOp1 t -> XExpr t -> IO (XExpr t)
    realOp :: RealOp1 t -> XExpr t -> IO (XExpr t)
realOp RealOp1 t
h XExpr t
xe = (forall (fpp :: FloatPrecision). FPOp1 fpp t)
-> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp1 fpp t
hf XExpr t
xe
      where
        hf :: (forall fpp . FPOp1 fpp t)
        hf :: forall (fpp :: FloatPrecision). FPOp1 fpp t
hf Expr t (BaseFloatType fpp)
e = do Expr t BaseRealType
re <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
e
                  Expr t BaseRealType
hre <- RealOp1 t
h Expr t BaseRealType
re
                  forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
WI.realToFloat ExprBuilder t st fs
sym forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
fpRM Expr t BaseRealType
hre

    realRecip :: RealOp1 t
    realRecip :: RealOp1 t
realRecip Expr t BaseRealType
e = do Expr t BaseRealType
one <- forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
WI.realLit ExprBuilder t st fs
sym Rational
1
                     forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
WI.realDiv ExprBuilder t st fs
sym Expr t BaseRealType
one Expr t BaseRealType
e

type BVOp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BVExpr t w)

type FPOp2 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.Expr t (WT.BaseFloatType fpp))

type RealOp2 t = WB.Expr t WT.BaseRealType -> WB.Expr t WT.BaseRealType -> IO (WB.Expr t WT.BaseRealType)

type BoolCmp2 t = WB.BoolExpr t -> WB.BoolExpr t -> IO (WB.BoolExpr t)

type BVCmp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BoolExpr t)

type FPCmp2 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.BoolExpr t)

translateOp2 :: forall t st fs a b c .
                WB.ExprBuilder t st fs
             -> (WB.ExprSymFn t
                 (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
                 WT.BaseRealType)
             -- ^ Pow function
             -> (WB.ExprSymFn t
                 (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
                 WT.BaseRealType)
             -- ^ Logb function
             -> CE.Op2 a b c
             -> XExpr t
             -> XExpr t
             -> IO (XExpr t)
translateOp2 :: forall t (st :: * -> *) fs a b c.
ExprBuilder t st fs
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> Op2 a b c
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp2 ExprBuilder t st fs
sym ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn Op2 a b c
op XExpr t
xe1 XExpr t
xe2 = case (Op2 a b c
op, XExpr t
xe1, XExpr t
xe2) of
  (Op2 a b c
CE.And, XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.andPred ExprBuilder t st fs
sym Expr t BaseBoolType
e1 Expr t BaseBoolType
e2
  (Op2 a b c
CE.Or, XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.orPred ExprBuilder t st fs
sym Expr t BaseBoolType
e1 Expr t BaseBoolType
e2
  (CE.Add Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Natural). BVOp2 w t)
-> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAdd ExprBuilder t st fs
sym) (forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatAdd ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe1 XExpr t
xe2
  (CE.Sub Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Natural). BVOp2 w t)
-> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSub ExprBuilder t st fs
sym) (forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatSub ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe1 XExpr t
xe2
  (CE.Mul Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Natural). BVOp2 w t)
-> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvMul ExprBuilder t st fs
sym) (forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatMul ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe1 XExpr t
xe2
  (CE.Mod Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Natural). BVOp2 w t)
-> (forall (w :: Natural). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSrem ExprBuilder t st fs
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvUrem ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.Div Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Natural). BVOp2 w t)
-> (forall (w :: Natural). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSdiv ExprBuilder t st fs
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvUdiv ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.Fdiv Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t -> XExpr t -> IO (XExpr t)
fpOp (forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatDiv ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe1 XExpr t
xe2
  (CE.Pow Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t -> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp2 fpp t
powFn' XExpr t
xe1 XExpr t
xe2
    where
      powFn' :: FPOp2 fpp t
      powFn' :: forall (fpp :: FloatPrecision). FPOp2 fpp t
powFn' Expr t (BaseFloatType fpp)
e1 Expr t (BaseFloatType fpp)
e2 = do Expr t BaseRealType
re1 <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
e1
                        Expr t BaseRealType
re2 <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
e2
                        let args :: Assignment (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
args = (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty 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 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 <- forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
WI.applySymFn ExprBuilder t st fs
sym ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn Assignment (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
args
                        forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
WI.realToFloat ExprBuilder t st fs
sym forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
fpRM Expr t BaseRealType
rpow
  (CE.Logb Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t -> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp2 fpp t
logbFn' XExpr t
xe1 XExpr t
xe2
    where
      logbFn' :: FPOp2 fpp t
      logbFn' :: forall (fpp :: FloatPrecision). FPOp2 fpp t
logbFn' Expr t (BaseFloatType fpp)
e1 Expr t (BaseFloatType fpp)
e2 = do Expr t BaseRealType
re1 <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
e1
                         Expr t BaseRealType
re2 <- forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
e2
                         let args :: Assignment (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
args = (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty 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 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 <- forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
WI.applySymFn ExprBuilder t st fs
sym ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn Assignment (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
args
                         forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
WI.realToFloat ExprBuilder t st fs
sym forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
fpRM Expr t BaseRealType
rpow
  (CE.Eq Type a
_, XExpr t
xe1, XExpr t
xe2) -> BoolCmp2 t
-> (forall (w :: Natural). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
cmp (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.eqPred ExprBuilder t st fs
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq ExprBuilder t st fs
sym) (forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatEq ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.Ne Type a
_, XExpr t
xe1, XExpr t
xe2) -> BoolCmp2 t
-> (forall (w :: Natural). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
cmp BoolCmp2 t
neqPred forall (w :: Natural). BVCmp2 w t
bvNeq forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpNeq XExpr t
xe1 XExpr t
xe2
    where
      neqPred :: BoolCmp2 t
      neqPred :: BoolCmp2 t
neqPred Expr t BaseBoolType
e1 Expr t BaseBoolType
e2 = do Expr t BaseBoolType
e <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.eqPred ExprBuilder t st fs
sym Expr t BaseBoolType
e1 Expr t BaseBoolType
e2
                         forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder t st fs
sym Expr t BaseBoolType
e
      bvNeq :: forall w . BVCmp2 w t
      bvNeq :: forall (w :: Natural). BVCmp2 w t
bvNeq BVExpr t w
e1 BVExpr t w
e2 = do Expr t BaseBoolType
e <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq ExprBuilder t st fs
sym BVExpr t w
e1 BVExpr t w
e2
                       forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder t st fs
sym Expr t BaseBoolType
e
      fpNeq :: forall fpp . FPCmp2 fpp t
      fpNeq :: forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpNeq Expr t (BaseFloatType fpp)
e1 Expr t (BaseFloatType fpp)
e2 = do Expr t BaseBoolType
e <- 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)
e1 Expr t (BaseFloatType fpp)
e2
                       forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder t st fs
sym Expr t BaseBoolType
e
  (CE.Le Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Natural). BVCmp2 w t)
-> (forall (w :: Natural). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSle ExprBuilder t st fs
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUle ExprBuilder t st fs
sym) (forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatLe ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.Ge Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Natural). BVCmp2 w t)
-> (forall (w :: Natural). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSge ExprBuilder t st fs
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUge ExprBuilder t st fs
sym) (forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatGe ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.Lt Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Natural). BVCmp2 w t)
-> (forall (w :: Natural). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSlt ExprBuilder t st fs
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUlt ExprBuilder t st fs
sym) (forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatLt ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.Gt Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Natural). BVCmp2 w t)
-> (forall (w :: Natural). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSgt ExprBuilder t st fs
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUgt ExprBuilder t st fs
sym) (forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatGt ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.BwAnd Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Natural). BVOp2 w t)
-> (forall (w :: Natural). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAndBits ExprBuilder t st fs
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAndBits ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.BwOr Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Natural). BVOp2 w t)
-> (forall (w :: Natural). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvOrBits ExprBuilder t st fs
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvOrBits ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.BwXor Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Natural). BVOp2 w t)
-> (forall (w :: Natural). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvXorBits ExprBuilder t st fs
sym) (forall sym (w :: Natural).
(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
  -- Note: For both shift operators, we are interpreting the shifter as an
  -- unsigned bitvector regardless of whether it is a word or an int.
  (CE.BwShiftL Type a
_ Type b
_, XExpr t
xe1, XExpr t
xe2) -> do
    Just (SomeBVExpr BVExpr t w
e1 NatRepr w
w1 BVSign
_ BVExpr t w -> XExpr t
ctor1) <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe1
    Just (SomeBVExpr BVExpr t w
e2 NatRepr w
w2 BVSign
_ BVExpr t w -> XExpr t
_    ) <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe2
    BVExpr t w
e2' <- case forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr w
w1 NatRepr w
w2 of
      NatCaseLT LeqProof (w + 1) w
LeqProof -> forall sym (r :: Natural) (w :: Natural).
(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
e2
      NatCases w w
NatCaseEQ -> forall (m :: * -> *) a. Monad m => a -> m a
return BVExpr t w
e2
      NatCaseGT LeqProof (w + 1) w
LeqProof -> forall sym (u :: Natural) (r :: Natural).
(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
e2
    BVExpr t w -> XExpr t
ctor1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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
e1 BVExpr t w
e2'
  (CE.BwShiftR Type a
_ Type b
_, XExpr t
xe1, XExpr t
xe2) -> do
    Just (SomeBVExpr BVExpr t w
e1 NatRepr w
w1 BVSign
sgn1 BVExpr t w -> XExpr t
ctor1) <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe1
    Just (SomeBVExpr BVExpr t w
e2 NatRepr w
w2 BVSign
_    BVExpr t w -> XExpr t
_    ) <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe2
    BVExpr t w
e2' <- case forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr w
w1 NatRepr w
w2 of
      NatCaseLT LeqProof (w + 1) w
LeqProof -> forall sym (r :: Natural) (w :: Natural).
(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
e2
      NatCases w w
NatCaseEQ -> forall (m :: * -> *) a. Monad m => a -> m a
return BVExpr t w
e2
      NatCaseGT LeqProof (w + 1) w
LeqProof -> forall sym (u :: Natural) (r :: Natural).
(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
e2
    BVExpr t w -> XExpr t
ctor1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case BVSign
sgn1 of
      BVSign
Signed -> forall sym (w :: Natural).
(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
e1 BVExpr t w
e2'
      BVSign
Unsigned -> forall sym (w :: Natural).
(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
e1 BVExpr t w
e2'
  -- Note: Currently, copilot does not check if array indices are out of bounds,
  -- even for constant expressions. The method of translation we are using
  -- simply creates a nest of if-then-else expression to check the index
  -- expression against all possible indices. If the index expression is known
  -- by the solver to be out of bounds (for instance, if it is a constant 5 for
  -- an array of 5 elements), then the if-then-else will trivially resolve to
  -- true.
  (CE.Index Type (Array n c)
_, XExpr t
xe1, XExpr t
xe2) -> do
    case (XExpr t
xe1, XExpr t
xe2) of
      (XArray Vector n (XExpr t)
xes, XWord32 Expr t (BaseBVType 32)
ix) -> forall (n :: Natural).
(1 <= n) =>
ExprBuilder t st fs
-> Word32
-> Expr t (BaseBVType 32)
-> Vector n (XExpr t)
-> IO (XExpr t)
buildIndexExpr ExprBuilder t st fs
sym Word32
0 Expr t (BaseBVType 32)
ix Vector n (XExpr t)
xes
      (XExpr t, XExpr t)
_ -> forall (m :: * -> *) a. MonadIO m => m a
panic
  (Op2 a b c, XExpr t, 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 :: Natural). BVOp2 w t)
-> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp forall (w :: Natural). BVOp2 w t
bvOp forall (fpp :: FloatPrecision). FPOp2 fpp t
fpOp XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
      (XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
bvOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
      (XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
bvOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
      (XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2)-> forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
bvOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
      (XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2)-> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
bvOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
      (XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2)-> forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
bvOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
      (XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2)-> forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
bvOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
      (XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2)-> forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
bvOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
      (XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2)-> forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
bvOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
      (XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2)-> forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision). FPOp2 fpp t
fpOp Expr t (BaseFloatType Prec32)
e1 Expr t (BaseFloatType Prec32)
e2
      (XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2)-> forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision). FPOp2 fpp t
fpOp Expr t (BaseFloatType Prec64)
e1 Expr t (BaseFloatType Prec64)
e2
      (XExpr t, 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 :: Natural). BVOp2 w t)
-> (forall (w :: Natural). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp forall (w :: Natural). BVOp2 w t
opS forall (w :: Natural). BVOp2 w t
opU XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
      (XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
opS Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
      (XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
opS Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
      (XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
opS Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
      (XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
opS Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
      (XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2) -> forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
opU Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
      (XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2) -> forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
opU Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
      (XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
opU Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
      (XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 w t
opU Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
      (XExpr t, XExpr t)
_ -> forall (m :: * -> *) a. MonadIO m => m a
panic

    fpOp :: (forall fpp . FPOp2 fpp t)
         -> XExpr t
         -> XExpr t
         -> IO (XExpr t)
    fpOp :: (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t -> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp2 fpp t
op XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
      (XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2) -> forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision). FPOp2 fpp t
op Expr t (BaseFloatType Prec32)
e1 Expr t (BaseFloatType Prec32)
e2
      (XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2) -> forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision). FPOp2 fpp t
op Expr t (BaseFloatType Prec64)
e1 Expr t (BaseFloatType Prec64)
e2
      (XExpr t, 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 :: Natural). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
cmp BoolCmp2 t
boolOp forall (w :: Natural). BVCmp2 w t
bvOp forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
      (XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BoolCmp2 t
boolOp Expr t BaseBoolType
e1 Expr t BaseBoolType
e2
      (XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
      (XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
      (XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
      (XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
      (XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
      (XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
      (XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
      (XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
      (XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp Expr t (BaseFloatType Prec32)
e1 Expr t (BaseFloatType Prec32)
e2
      (XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp Expr t (BaseFloatType Prec64)
e1 Expr t (BaseFloatType Prec64)
e2
      (XExpr t, 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 :: Natural). BVCmp2 w t)
-> (forall (w :: Natural). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp forall (w :: Natural). BVCmp2 w t
bvSOp forall (w :: Natural). BVCmp2 w t
bvUOp forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
      (XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvSOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
      (XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvSOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
      (XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvSOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
      (XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvSOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
      (XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvUOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
      (XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvUOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
      (XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvUOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
      (XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 w t
bvUOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
      (XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp Expr t (BaseFloatType Prec32)
e1 Expr t (BaseFloatType Prec32)
e2
      (XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2)-> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpOp Expr t (BaseFloatType Prec64)
e1 Expr t (BaseFloatType Prec64)
e2
      (XExpr t, XExpr t)
_ -> forall (m :: * -> *) a. MonadIO m => m a
panic

    buildIndexExpr :: 1 <= n
                   => WB.ExprBuilder t st fs
                   -> Word32
                   -- ^ Index
                   -> WB.Expr t (WT.BaseBVType 32)
                   -- ^ Index
                   -> V.Vector n (XExpr t)
                   -- ^ Elements
                   -> IO (XExpr t)
    buildIndexExpr :: forall (n :: Natural).
(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
curIx Expr t (BaseBVType 32)
ix Vector n (XExpr t)
xelts = case forall (n :: Natural) a.
Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))
V.uncons Vector n (XExpr t)
xelts of
      (XExpr t
xe, Left n :~: 1
Refl) -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
      (XExpr t
xe, Right Vector (n - 1) (XExpr t)
xelts') -> do
        LeqProof 1 (n - 1)
LeqProof <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) a. Vector n a -> LeqProof 1 n
V.nonEmpty Vector (n - 1) (XExpr t)
xelts'
        XExpr t
rstExpr <- forall (n :: Natural).
(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
curIxforall a. Num a => a -> a -> a
+Word32
1) Expr t (BaseBVType 32)
ix Vector (n - 1) (XExpr t)
xelts'
        Expr t (BaseBVType 32)
curIxExpr <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit ExprBuilder t st fs
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Word32 -> BV 32
BV.word32 Word32
curIx)
        Expr t BaseBoolType
ixEq <- forall sym (w :: Natural).
(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)
curIxExpr Expr t (BaseBVType 32)
ix
        ExprBuilder t st fs
-> Expr t BaseBoolType -> XExpr t -> XExpr t -> IO (XExpr t)
mkIte ExprBuilder t st fs
sym Expr t BaseBoolType
ixEq XExpr t
xe XExpr t
rstExpr

    mkIte :: WB.ExprBuilder t st fs
          -> WB.Expr t WT.BaseBoolType
          -> XExpr t
          -> XExpr t
          -> IO (XExpr t)
    mkIte :: ExprBuilder t st fs
-> Expr t BaseBoolType -> XExpr t -> XExpr t -> IO (XExpr t)
mkIte ExprBuilder t st fs
sym Expr t BaseBoolType
pred XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
          (XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 Expr t BaseBoolType
e1 Expr t BaseBoolType
e2
          (XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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 Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
          (XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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 Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
          (XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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 Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
          (XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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 Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
          (XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2) -> forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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 Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
          (XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2) -> forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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 Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
          (XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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 Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
          (XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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 Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
          (XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2) -> forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 Expr t (BaseFloatType Prec32)
e1 Expr t (BaseFloatType Prec32)
e2
          (XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2) -> forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 Expr t (BaseFloatType Prec64)
e1 Expr t (BaseFloatType Prec64)
e2
          (XStruct [XExpr t]
xes1, XStruct [XExpr t]
xes2) ->
            forall t. [XExpr t] -> XExpr t
XStruct forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (ExprBuilder t st fs
-> Expr t BaseBoolType -> XExpr t -> XExpr t -> IO (XExpr t)
mkIte ExprBuilder t st fs
sym Expr t BaseBoolType
pred) [XExpr t]
xes1 [XExpr t]
xes2
          (XArray Vector n (XExpr t)
xes1, XArray Vector n (XExpr t)
xes2) ->
            case forall (n :: Natural) a. Vector n a -> NatRepr n
V.length Vector n (XExpr t)
xes1 forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
`testEquality` forall (n :: Natural) a. Vector n a -> NatRepr n
V.length Vector n (XExpr t)
xes2 of
              Just n :~: n
Refl -> forall (n :: Natural) t. (1 <= n) => Vector n (XExpr t) -> XExpr t
XArray forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c (n :: Natural).
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)
xes2
              Maybe (n :~: n)
Nothing -> forall (m :: * -> *) a. MonadIO m => m a
panic
          (XExpr t, 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 :: 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 (CE.Mux Type b
_) (XBool Expr t BaseBoolType
te) XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
  (XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> forall t. Expr t BaseBoolType -> XExpr t
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.itePred ExprBuilder t st fs
sym Expr t BaseBoolType
te Expr t BaseBoolType
e1 Expr t BaseBoolType
e2
  (XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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
te Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
  (XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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
te Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
  (XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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
te Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
  (XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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
te Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
  (XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2) -> forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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
te Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
  (XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2) -> forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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
te Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
  (XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2) -> forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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
te Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
  (XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2) -> forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(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
te Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
  (XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2) -> forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
te Expr t (BaseFloatType Prec32)
e1 Expr t (BaseFloatType Prec32)
e2
  (XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2) -> forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
te Expr t (BaseFloatType Prec64)
e1 Expr t (BaseFloatType Prec64)
e2
  (XExpr t, XExpr t)
_ -> forall (m :: * -> *) a. MonadIO m => m a
panic
translateOp3 ExprBuilder t st fs
_ Op3 a b c d
_ XExpr t
_ XExpr t
_ XExpr t
_ = forall (m :: * -> *) a. MonadIO m => m a
panic