{-# 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
(Int -> SatResult -> ShowS)
-> (SatResult -> String)
-> ([SatResult] -> ShowS)
-> Show SatResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SatResult] -> ShowS
$cshowList :: [SatResult] -> ShowS
show :: SatResult -> String
$cshow :: SatResult -> String
showsPrec :: Int -> SatResult -> ShowS
$cshowsPrec :: Int -> SatResult -> ShowS
Show

type CounterExample = [(String, Some CopilotValue)]

-- | 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 <- FloatModeRepr 'FloatIEEE
-> BuilderState x
-> NonceGenerator IO x
-> IO (ExprBuilder x BuilderState (Flags 'FloatIEEE))
forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
WB.newExprBuilder FloatModeRepr 'FloatIEEE
WB.FloatIEEERepr BuilderState x
forall a. BuilderState a
EmptyState NonceGenerator IO x
ng

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

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

  -- 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 = [Property]
-> (Property -> TransM x (String, SatResult))
-> TransM x [(String, SatResult)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Spec -> [Property]
CS.specProperties Spec
spec) ((Property -> TransM x (String, SatResult))
 -> TransM x [(String, SatResult)])
-> (Property -> TransM x (String, SatResult))
-> TransM x [(String, SatResult)]
forall a b. (a -> b) -> a -> b
$ \Property
pr -> do
        let bufLen :: Stream -> Int
bufLen (CS.Stream Int
_ [a]
buf Expr a
_ Type a
_) = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
buf
            maxBufLen :: Int
maxBufLen = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (Stream -> Int
bufLen (Stream -> Int) -> [Stream] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec -> [Stream]
CS.specStreams Spec
spec))
        [Expr x BaseBoolType]
prefix <- [Int]
-> (Int -> TransM x (Expr x BaseBoolType))
-> TransM x [Expr x BaseBoolType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int
0 .. Int
maxBufLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] ((Int -> TransM x (Expr x BaseBoolType))
 -> TransM x [Expr x BaseBoolType])
-> (Int -> TransM x (Expr x BaseBoolType))
-> TransM x [Expr x BaseBoolType]
forall a b. (a -> b) -> a -> b
$ \Int
k -> do
          XBool Expr x BaseBoolType
p <- ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> Int -> Expr Bool -> TransM x (XExpr x)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExprAt ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym Int
k (Property -> Expr Bool
CS.propertyExpr Property
pr)
          Expr x BaseBoolType -> TransM x (Expr x BaseBoolType)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr x BaseBoolType
p
        XBool Expr x BaseBoolType
p <- ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> Int -> Expr Bool -> TransM x (XExpr x)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym Int
0 (Property -> Expr Bool
CS.propertyExpr Property
pr)
        Expr x BaseBoolType
p_and_prefix <- IO (Expr x BaseBoolType) -> TransM x (Expr x BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Expr x BaseBoolType) -> TransM x (Expr x BaseBoolType))
-> IO (Expr x BaseBoolType) -> TransM x (Expr x BaseBoolType)
forall a b. (a -> b) -> a -> b
$ (Expr x BaseBoolType
 -> Expr x BaseBoolType -> IO (Expr x BaseBoolType))
-> Expr x BaseBoolType
-> [Expr x BaseBoolType]
-> IO (Expr x BaseBoolType)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> Pred (ExprBuilder x BuilderState (Flags 'FloatIEEE))
-> Pred (ExprBuilder x BuilderState (Flags 'FloatIEEE))
-> IO (Pred (ExprBuilder x BuilderState (Flags 'FloatIEEE)))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.andPred ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym) Expr x BaseBoolType
p [Expr x BaseBoolType]
prefix
        Expr x BaseBoolType
not_p_and_prefix <- IO (Expr x BaseBoolType) -> TransM x (Expr x BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Expr x BaseBoolType) -> TransM x (Expr x BaseBoolType))
-> IO (Expr x BaseBoolType) -> TransM x (Expr x BaseBoolType)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> Pred (ExprBuilder x BuilderState (Flags 'FloatIEEE))
-> IO (Pred (ExprBuilder x BuilderState (Flags 'FloatIEEE)))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym Expr x BaseBoolType
Pred (ExprBuilder x BuilderState (Flags 'FloatIEEE))
p_and_prefix

        let clauses :: [Expr x BaseBoolType]
clauses = [Expr x BaseBoolType
not_p_and_prefix]
        case Solver
solver of
          Solver
CVC4 -> IO (String, SatResult) -> TransM x (String, SatResult)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, SatResult) -> TransM x (String, SatResult))
-> IO (String, SatResult) -> TransM x (String, SatResult)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> LogData
-> [Expr x BaseBoolType]
-> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
    -> IO (String, SatResult))
-> IO (String, SatResult)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
WS.runCVC4InOverride ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym LogData
WS.defaultLogData [Expr x BaseBoolType]
clauses ((SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
  -> IO (String, SatResult))
 -> IO (String, SatResult))
-> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
    -> IO (String, SatResult))
-> IO (String, SatResult)
forall a b. (a -> b) -> a -> b
$ \case
            WS.Sat (GroundEvalFn x
_ge, Maybe (ExprRangeBindings x)
_) -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
            WS.Unsat ()
_ -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
            SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
          Solver
DReal -> IO (String, SatResult) -> TransM x (String, SatResult)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, SatResult) -> TransM x (String, SatResult))
-> IO (String, SatResult) -> TransM x (String, SatResult)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> LogData
-> [Expr x BaseBoolType]
-> (SatResult (WriterConn x (Writer DReal), DRealBindings) ()
    -> IO (String, SatResult))
-> IO (String, SatResult)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    -> IO a)
-> IO a
WS.runDRealInOverride ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym LogData
WS.defaultLogData [Expr x BaseBoolType]
clauses ((SatResult (WriterConn x (Writer DReal), DRealBindings) ()
  -> IO (String, SatResult))
 -> IO (String, SatResult))
-> (SatResult (WriterConn x (Writer DReal), DRealBindings) ()
    -> IO (String, SatResult))
-> IO (String, SatResult)
forall a b. (a -> b) -> a -> b
$ \case
            WS.Sat (WriterConn x (Writer DReal)
_ge, DRealBindings
_) -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
            WS.Unsat ()
_ -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
            SatResult (WriterConn x (Writer DReal), DRealBindings) ()
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
          Solver
Yices -> IO (String, SatResult) -> TransM x (String, SatResult)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, SatResult) -> TransM x (String, SatResult))
-> IO (String, SatResult) -> TransM x (String, SatResult)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> LogData
-> [Expr x BaseBoolType]
-> (SatResult (GroundEvalFn x) () -> IO (String, SatResult))
-> IO (String, SatResult)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t) () -> IO a)
-> IO a
WS.runYicesInOverride ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym LogData
WS.defaultLogData [Expr x BaseBoolType]
clauses ((SatResult (GroundEvalFn x) () -> IO (String, SatResult))
 -> IO (String, SatResult))
-> (SatResult (GroundEvalFn x) () -> IO (String, SatResult))
-> IO (String, SatResult)
forall a b. (a -> b) -> a -> b
$ \case
            WS.Sat GroundEvalFn x
_ge -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
            WS.Unsat ()
_ -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
            SatResult (GroundEvalFn x) ()
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
          Solver
Z3 -> IO (String, SatResult) -> TransM x (String, SatResult)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, SatResult) -> TransM x (String, SatResult))
-> IO (String, SatResult) -> TransM x (String, SatResult)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> LogData
-> [Expr x BaseBoolType]
-> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
    -> IO (String, SatResult))
-> IO (String, SatResult)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
WS.runZ3InOverride ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym LogData
WS.defaultLogData [Expr x BaseBoolType]
clauses ((SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
  -> IO (String, SatResult))
 -> IO (String, SatResult))
-> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
    -> IO (String, SatResult))
-> IO (String, SatResult)
forall a b. (a -> b) -> a -> b
$ \case
            WS.Sat (GroundEvalFn x
_ge, Maybe (ExprRangeBindings x)
_) -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
            WS.Unsat ()
_ -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
            SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)

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

--------------------------------------------------------------------------------
-- 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.
  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.
  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.
  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.
  TransState t -> Map Int Stream
streams :: Map.Map CE.Id CS.Stream,
  -- | Binary power operator, represented as an uninterpreted function.
  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.
  TransState t
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logb :: WB.ExprSymFn t
          (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
          WT.BaseRealType
  }

newtype TransM t a = TransM { TransM t a -> StateT (TransState t) IO a
unTransM :: StateT (TransState t) IO a }
  deriving ( a -> TransM t b -> TransM t a
(a -> b) -> TransM t a -> TransM t b
(forall a b. (a -> b) -> TransM t a -> TransM t b)
-> (forall a b. a -> TransM t b -> TransM t a)
-> Functor (TransM t)
forall a b. a -> TransM t b -> TransM t a
forall a b. (a -> b) -> TransM t a -> TransM t b
forall t a b. a -> TransM t b -> TransM t a
forall t a b. (a -> b) -> TransM t a -> TransM t b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> TransM t b -> TransM t a
$c<$ :: forall t a b. a -> TransM t b -> TransM t a
fmap :: (a -> b) -> TransM t a -> TransM t b
$cfmap :: forall t a b. (a -> b) -> TransM t a -> TransM t b
Functor
           , Functor (TransM t)
a -> TransM t a
Functor (TransM t)
-> (forall a. a -> TransM t a)
-> (forall a b. TransM t (a -> b) -> TransM t a -> TransM t b)
-> (forall a b c.
    (a -> b -> c) -> TransM t a -> TransM t b -> TransM t c)
-> (forall a b. TransM t a -> TransM t b -> TransM t b)
-> (forall a b. TransM t a -> TransM t b -> TransM t a)
-> Applicative (TransM t)
TransM t a -> TransM t b -> TransM t b
TransM t a -> TransM t b -> TransM t a
TransM t (a -> b) -> TransM t a -> TransM t b
(a -> b -> c) -> TransM t a -> TransM t b -> TransM t c
forall t. Functor (TransM t)
forall a. a -> TransM t a
forall t a. a -> TransM t a
forall a b. TransM t a -> TransM t b -> TransM t a
forall a b. TransM t a -> TransM t b -> TransM t b
forall a b. TransM t (a -> b) -> TransM t a -> TransM t b
forall t a b. TransM t a -> TransM t b -> TransM t a
forall t a b. TransM t a -> TransM t b -> TransM t b
forall t a b. TransM t (a -> b) -> TransM t a -> TransM t b
forall a b c.
(a -> b -> c) -> TransM t a -> TransM t b -> TransM t c
forall t a b c.
(a -> b -> c) -> TransM t a -> TransM t b -> TransM t c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: TransM t a -> TransM t b -> TransM t a
$c<* :: forall t a b. TransM t a -> TransM t b -> TransM t a
*> :: TransM t a -> TransM t b -> TransM t b
$c*> :: forall t a b. TransM t a -> TransM t b -> TransM t b
liftA2 :: (a -> b -> c) -> TransM t a -> TransM t b -> TransM t c
$cliftA2 :: forall t a b c.
(a -> b -> c) -> TransM t a -> TransM t b -> TransM t c
<*> :: TransM t (a -> b) -> TransM t a -> TransM t b
$c<*> :: forall t a b. TransM t (a -> b) -> TransM t a -> TransM t b
pure :: a -> TransM t a
$cpure :: forall t a. a -> TransM t a
$cp1Applicative :: forall t. Functor (TransM t)
Applicative
           , Applicative (TransM t)
a -> TransM t a
Applicative (TransM t)
-> (forall a b. TransM t a -> (a -> TransM t b) -> TransM t b)
-> (forall a b. TransM t a -> TransM t b -> TransM t b)
-> (forall a. a -> TransM t a)
-> Monad (TransM t)
TransM t a -> (a -> TransM t b) -> TransM t b
TransM t a -> TransM t b -> TransM t b
forall t. Applicative (TransM t)
forall a. a -> TransM t a
forall t a. a -> TransM t a
forall a b. TransM t a -> TransM t b -> TransM t b
forall a b. TransM t a -> (a -> TransM t b) -> TransM t b
forall t a b. TransM t a -> TransM t b -> TransM t b
forall t a b. TransM t a -> (a -> TransM t b) -> TransM t b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> TransM t a
$creturn :: forall t a. a -> TransM t a
>> :: TransM t a -> TransM t b -> TransM t b
$c>> :: forall t a b. TransM t a -> TransM t b -> TransM t b
>>= :: TransM t a -> (a -> TransM t b) -> TransM t b
$c>>= :: forall t a b. TransM t a -> (a -> TransM t b) -> TransM t b
$cp1Monad :: forall t. Applicative (TransM t)
Monad
           , Monad (TransM t)
Monad (TransM t)
-> (forall a. IO a -> TransM t a) -> MonadIO (TransM t)
IO a -> TransM t a
forall t. Monad (TransM t)
forall a. IO a -> TransM t a
forall t a. IO a -> TransM t a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> TransM t a
$cliftIO :: forall t a. IO a -> TransM t a
$cp1MonadIO :: forall t. Monad (TransM t)
MonadIO
           , MonadState (TransState t)
           )

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

data CopilotWhat4 = CopilotWhat4

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

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

-- | 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 :: m a
panic = CopilotWhat4 -> String -> [String] -> m a
forall a b.
(PanicComponent a, HasCallStack) =>
a -> String -> [String] -> b
Panic.panic CopilotWhat4
CopilotWhat4 String
"Copilot.Theorem.What4"
        [ String
"Ill-typed core expression" ]

-- | 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 { CopilotValue a -> Type a
cvType :: CT.Type a
                                   , CopilotValue a -> a
cvVal :: a
                                   }

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

-- | 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 :: XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe = case XExpr t
xe of
  XInt8 Expr t (BaseBVType 8)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 8)
-> NatRepr 8
-> BVSign
-> (Expr t (BaseBVType 8) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 8)
e NatRepr 8
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Signed Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8)
  XInt16 Expr t (BaseBVType 16)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 16)
-> NatRepr 16
-> BVSign
-> (Expr t (BaseBVType 16) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 16)
e NatRepr 16
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Signed Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16)
  XInt32 Expr t (BaseBVType 32)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 32)
-> NatRepr 32
-> BVSign
-> (Expr t (BaseBVType 32) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 32)
e NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Signed Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32)
  XInt64 Expr t (BaseBVType 64)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 64)
-> NatRepr 64
-> BVSign
-> (Expr t (BaseBVType 64) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 64)
e NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Signed Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64)
  XWord8 Expr t (BaseBVType 8)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 8)
-> NatRepr 8
-> BVSign
-> (Expr t (BaseBVType 8) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 8)
e NatRepr 8
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Unsigned Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8)
  XWord16 Expr t (BaseBVType 16)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 16)
-> NatRepr 16
-> BVSign
-> (Expr t (BaseBVType 16) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 16)
e NatRepr 16
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Unsigned Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16)
  XWord32 Expr t (BaseBVType 32)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 32)
-> NatRepr 32
-> BVSign
-> (Expr t (BaseBVType 32) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 32)
e NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Unsigned Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32)
  XWord64 Expr t (BaseBVType 64)
e -> SomeBVExpr t -> Maybe (SomeBVExpr t)
forall a. a -> Maybe a
Just (Expr t (BaseBVType 64)
-> NatRepr 64
-> BVSign
-> (Expr t (BaseBVType 64) -> XExpr t)
-> SomeBVExpr t
forall (w :: Nat) t.
(1 <= w) =>
BVExpr t w
-> NatRepr w -> BVSign -> (BVExpr t w -> XExpr t) -> SomeBVExpr t
SomeBVExpr Expr t (BaseBVType 64)
e NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BVSign
Unsigned Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64)
  XExpr t
_ -> Maybe (SomeBVExpr t)
forall a. Maybe a
Nothing

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

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

-- | 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 :: ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
nm Type a
tp = case Type a
tp of
  Type a
CT.Bool -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr BaseBoolType
-> IO (SymExpr (ExprBuilder t st fs) BaseBoolType)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr BaseBoolType
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Int8 -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 8)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 8))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 8)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Int16 -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 16)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 16))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 16)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Int32 -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 32)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 32))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 32)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Int64 -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 64)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 64))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 64)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Word8 -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 8)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 8))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 8)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Word16 -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 16)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 16))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 16)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Word32 -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 32)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 32))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 32)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Word64 -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseBVType 64)
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType 64))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseBVType 64)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Float -> Expr t (BaseFloatType Prec32) -> XExpr t
forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat (Expr t (BaseFloatType Prec32) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseFloatType Prec32)
-> IO (SymExpr (ExprBuilder t st fs) (BaseFloatType Prec32))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseFloatType Prec32)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Double -> Expr t (BaseFloatType Prec64) -> XExpr t
forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble (Expr t (BaseFloatType Prec64) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr (BaseFloatType Prec64)
-> IO (SymExpr (ExprBuilder t st fs) (BaseFloatType Prec64))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant ExprBuilder t st fs
sym (String -> SolverSymbol
WI.safeSymbol String
nm) BaseTypeRepr (BaseFloatType Prec64)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  atp :: Type a
atp@(CT.Array Type t
itp) -> do
    NatRepr n
n <- NatRepr n -> IO (NatRepr n)
forall (m :: * -> *) a. Monad m => a -> m a
return (NatRepr n -> IO (NatRepr n)) -> NatRepr n -> IO (NatRepr n)
forall a b. (a -> b) -> a -> b
$ Type (Array n t) -> NatRepr n
forall (n :: Nat) t. KnownNat n => Type (Array n t) -> NatRepr n
arrayLen Type a
Type (Array n t)
atp
    case NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
forall (n :: Nat). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 NatRepr n
n of
      Left n :~: 0
Refl -> XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
forall t. XExpr t
XEmptyArray
      Right LeqProof 1 n
LeqProof -> do
        ((n - 1) + 1) :~: n
Refl <- (((n - 1) + 1) :~: n) -> IO (((n - 1) + 1) :~: n)
forall (m :: * -> *) a. Monad m => a -> m a
return ((((n - 1) + 1) :~: n) -> IO (((n - 1) + 1) :~: n))
-> (((n - 1) + 1) :~: n) -> IO (((n - 1) + 1) :~: n)
forall a b. (a -> b) -> a -> b
$ NatRepr n -> NatRepr 1 -> ((n - 1) + 1) :~: n
forall (f :: Nat -> *) (m :: Nat) (g :: Nat -> *) (n :: Nat).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel NatRepr n
n (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1)
        Vector n (XExpr t)
elts :: V.Vector n (XExpr t) <- NatRepr (n - 1)
-> (forall (n :: Nat). (n <= (n - 1)) => NatRepr n -> IO (XExpr t))
-> IO (Vector ((n - 1) + 1) (XExpr t))
forall (m :: * -> *) (h :: Nat) a.
Monad m =>
NatRepr h
-> (forall (n :: Nat). (n <= h) => NatRepr n -> m a)
-> m (Vector (h + 1) a)
V.generateM (NatRepr n -> NatRepr (n - 1)
forall (n :: Nat). (1 <= n) => NatRepr n -> NatRepr (n - 1)
decNat NatRepr n
n) (IO (XExpr t) -> NatRepr n -> IO (XExpr t)
forall a b. a -> b -> a
const (ExprBuilder t st fs -> String -> Type t -> IO (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
"" Type t
itp))
        XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ Vector n (XExpr t) -> XExpr t
forall (n :: Nat) t. (1 <= n) => Vector n (XExpr t) -> XExpr t
XArray Vector n (XExpr t)
elts
  CT.Struct a
stp -> do
    [XExpr t]
elts <- [Value a] -> (Value a -> IO (XExpr t)) -> IO [XExpr t]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (a -> [Value a]
forall a. Struct a => a -> [Value a]
CT.toValues a
stp) ((Value a -> IO (XExpr t)) -> IO [XExpr t])
-> (Value a -> IO (XExpr t)) -> IO [XExpr t]
forall a b. (a -> b) -> a -> b
$ \(CT.Value Type t
ftp Field s t
_) -> ExprBuilder t st fs -> String -> Type t -> IO (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
"" Type t
ftp
    XExpr t -> IO (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return (XExpr t -> IO (XExpr t)) -> XExpr t -> IO (XExpr t)
forall a b. (a -> b) -> a -> b
$ [XExpr t] -> XExpr t
forall t. [XExpr t] -> XExpr t
XStruct [XExpr t]
elts

-- | 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 :: ExprBuilder t st fs -> Int -> Int -> TransM t (XExpr t)
getStreamConstant ExprBuilder t st fs
sym Int
streamId Int
offset = do
  Map (Int, Int) (XExpr t)
scs <- (TransState t -> Map (Int, Int) (XExpr t))
-> TransM t (Map (Int, Int) (XExpr t))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t -> Map (Int, Int) (XExpr t)
forall t. TransState t -> Map (Int, Int) (XExpr t)
streamConstants
  case (Int, Int) -> Map (Int, Int) (XExpr t) -> Maybe (XExpr t)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Int
streamId, Int
offset) Map (Int, Int) (XExpr t)
scs of
    Just XExpr t
xe -> XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
    Maybe (XExpr t)
Nothing -> do
      CS.Stream Int
_ [a]
_ Expr a
_ Type a
tp <- Int -> TransM t Stream
forall t. Int -> TransM t Stream
getStreamDef Int
streamId
      let nm :: String
nm = Int -> String
forall a. Show a => a -> String
show Int
streamId String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
offset
      XExpr t
xe <- IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
nm Type a
tp
      (TransState t -> TransState t) -> TransM t ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TransState t
st -> TransState t
st { streamConstants :: Map (Int, Int) (XExpr t)
streamConstants = (Int, Int)
-> XExpr t -> Map (Int, Int) (XExpr t) -> Map (Int, Int) (XExpr t)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Int
streamId, Int
offset) XExpr t
xe Map (Int, Int) (XExpr t)
scs })
      XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe

-- | 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 :: ExprBuilder t st fs
-> Type a -> String -> Int -> TransM t (XExpr t)
getExternConstant ExprBuilder t st fs
sym Type a
tp String
var Int
offset = do
  Map (String, Int) (XExpr t)
es <- (TransState t -> Map (String, Int) (XExpr t))
-> TransM t (Map (String, Int) (XExpr t))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t -> Map (String, Int) (XExpr t)
forall t. TransState t -> Map (String, Int) (XExpr t)
externVars
  case (String, Int) -> Map (String, Int) (XExpr t) -> Maybe (XExpr t)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (String
var, Int
offset) Map (String, Int) (XExpr t)
es of
    Just XExpr t
xe -> XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
    Maybe (XExpr t)
Nothing -> do
      XExpr t
xe <- IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
var Type a
tp
      (TransState t -> TransState t) -> TransM t ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TransState t
st -> TransState t
st { externVars :: Map (String, Int) (XExpr t)
externVars = (String, Int)
-> XExpr t
-> Map (String, Int) (XExpr t)
-> Map (String, Int) (XExpr t)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (String
var, Int
offset) XExpr t
xe Map (String, Int) (XExpr t)
es} )
      XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe

-- | 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 :: ExprBuilder t st fs
-> Type a -> String -> Int -> TransM t (XExpr t)
getExternConstantAt ExprBuilder t st fs
sym Type a
tp String
var Int
ix = do
  Map (String, Int) (XExpr t)
es <- (TransState t -> Map (String, Int) (XExpr t))
-> TransM t (Map (String, Int) (XExpr t))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t -> Map (String, Int) (XExpr t)
forall t. TransState t -> Map (String, Int) (XExpr t)
externVarsAt
  case (String, Int) -> Map (String, Int) (XExpr t) -> Maybe (XExpr t)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (String
var, Int
ix) Map (String, Int) (XExpr t)
es of
    Just XExpr t
xe -> XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe
    Maybe (XExpr t)
Nothing -> do
      XExpr t
xe <- IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> String -> Type a -> IO (XExpr t)
freshCPConstant ExprBuilder t st fs
sym String
var Type a
tp
      (TransState t -> TransState t) -> TransM t ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TransState t
st -> TransState t
st { externVarsAt :: Map (String, Int) (XExpr t)
externVarsAt = (String, Int)
-> XExpr t
-> Map (String, Int) (XExpr t)
-> Map (String, Int) (XExpr t)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (String
var, Int
ix) XExpr t
xe Map (String, Int) (XExpr t)
es} )
      XExpr t -> TransM t (XExpr t)
forall (m :: * -> *) a. Monad m => a -> m a
return XExpr t
xe

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

-- | 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 :: ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr a
e = case Expr a
e of
  CE.Const Type a
tp a
a -> IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
forall a t (st :: * -> *) fs.
ExprBuilder t st fs -> Type a -> a -> IO (XExpr t)
translateConstExpr ExprBuilder t st fs
sym Type a
tp a
a
  CE.Drop Type a
_tp Word32
ix Int
streamId
    -- If we are referencing a past value of this stream, just return an
    -- unconstrained constant.
    | Int
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
ix Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 ->
        ExprBuilder t st fs -> Int -> Int -> TransM t (XExpr t)
forall t (st :: * -> *) fs.
ExprBuilder t st fs -> Int -> Int -> TransM t (XExpr t)
getStreamConstant ExprBuilder t st fs
sym Int
streamId (Int
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
ix)
    -- 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
_ <- Int -> TransM t Stream
forall t. Int -> TransM t Stream
getStreamDef Int
streamId
      ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym (Int
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
- [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
buf) Expr a
e
  CE.Local Type a1
_ Type a
_ String
_ Expr a1
_ Expr a
_ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error String
"translateExpr: Local unimplemented"
  CE.Var Type a
_ String
_ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error String
"translateExpr: Var unimplemented"
  CE.ExternVar Type a
tp String
nm Maybe [a]
_prefix -> ExprBuilder t st fs
-> Type a -> String -> Int -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs
-> Type a -> String -> Int -> TransM t (XExpr t)
getExternConstant ExprBuilder t st fs
sym Type a
tp String
nm Int
offset
  CE.Op1 Op1 a1 a
op Expr a1
e -> IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> (XExpr t -> IO (XExpr t)) -> XExpr t -> TransM t (XExpr t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprBuilder t st fs -> Op1 a1 a -> XExpr t -> IO (XExpr t)
forall t (st :: * -> *) fs a b.
ExprBuilder t st fs -> Op1 a b -> XExpr t -> IO (XExpr t)
translateOp1 ExprBuilder t st fs
sym Op1 a1 a
op (XExpr t -> TransM t (XExpr t))
-> TransM t (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder t st fs -> Int -> Expr a1 -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr a1
e
  CE.Op2 Op2 a1 b a
op Expr a1
e1 Expr b
e2 -> do
    XExpr t
xe1 <- ExprBuilder t st fs -> Int -> Expr a1 -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr a1
e1
    XExpr t
xe2 <- ExprBuilder t st fs -> Int -> Expr b -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr b
e2
    ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn <- (TransState t
 -> ExprSymFn
      t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType)
-> TransM
     t
     (ExprSymFn
        t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
forall t.
TransState t
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
pow
    ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn <- (TransState t
 -> ExprSymFn
      t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType)
-> TransM
     t
     (ExprSymFn
        t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState t
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
forall t.
TransState t
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logb
    IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> Op2 a1 b a
-> XExpr t
-> XExpr t
-> IO (XExpr t)
forall t (st :: * -> *) fs a b c.
ExprBuilder t st fs
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> Op2 a b c
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp2 ExprBuilder t st fs
sym ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn Op2 a1 b a
op XExpr t
xe1 XExpr t
xe2
  CE.Op3 Op3 a1 b c a
op Expr a1
e1 Expr b
e2 Expr c
e3 -> do
    XExpr t
xe1 <- ExprBuilder t st fs -> Int -> Expr a1 -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr a1
e1
    XExpr t
xe2 <- ExprBuilder t st fs -> Int -> Expr b -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr b
e2
    XExpr t
xe3 <- ExprBuilder t st fs -> Int -> Expr c -> TransM t (XExpr t)
forall t (st :: * -> *) fs a.
ExprBuilder t st fs -> Int -> Expr a -> TransM t (XExpr t)
translateExpr ExprBuilder t st fs
sym Int
offset Expr c
e3
    IO (XExpr t) -> TransM t (XExpr t)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (XExpr t) -> TransM t (XExpr t))
-> IO (XExpr t) -> TransM t (XExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs
-> Op3 a1 b c a -> XExpr t -> XExpr t -> XExpr t -> IO (XExpr t)
forall t (st :: * -> *) fs a b c d.
ExprBuilder t st fs
-> Op3 a b c d -> XExpr t -> XExpr t -> XExpr t -> IO (XExpr t)
translateOp3 ExprBuilder t st fs
sym Op3 a1 b c a
op XExpr t
xe1 XExpr t
xe2 XExpr t
xe3
  CE.Label Type a
_ String
_ Expr a
_ -> String -> TransM t (XExpr t)
forall a. HasCallStack => String -> a
error String
"translateExpr: Label unimplemented"

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

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

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

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

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

valueName :: CT.Value a -> Some SymbolRepr
valueName :: Value a -> Some SymbolRepr
valueName (CT.Value Type t
_ Field s t
f) = SymbolRepr s -> Some SymbolRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (Field s t -> SymbolRepr s
forall (s :: Symbol) a. KnownSymbol s => Field s a -> SymbolRepr s
fieldName Field s t
f)

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

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

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

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

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

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

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

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

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

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

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

translateOp2 :: forall t st fs a b c .
                WB.ExprBuilder t st fs
             -> (WB.ExprSymFn t
                 (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
                 WT.BaseRealType)
             -- ^ 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 :: ExprBuilder t st fs
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> ExprSymFn
     t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
-> Op2 a b c
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp2 ExprBuilder t st fs
sym ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
powFn ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
logbFn Op2 a b c
op XExpr t
xe1 XExpr t
xe2 = case (Op2 a b c
op, XExpr t
xe1, XExpr t
xe2) of
  (Op2 a b c
CE.And, XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.andPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e1 Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e2
  (Op2 a b c
CE.Or, XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.orPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e1 Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e2
  (CE.Add Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAdd ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> RoundingMode
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatAdd ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe1 XExpr t
xe2
  (CE.Sub Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSub ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> RoundingMode
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatSub ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe1 XExpr t
xe2
  (CE.Mul Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvMul ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> RoundingMode
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatMul ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe1 XExpr t
xe2
  (CE.Mod Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (w :: Nat). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSrem ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvUrem ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.Div Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (w :: Nat). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSdiv ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvUdiv ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.Fdiv Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t -> XExpr t -> IO (XExpr t)
fpOp (ExprBuilder t st fs
-> RoundingMode
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatDiv ExprBuilder t st fs
sym RoundingMode
fpRM) XExpr t
xe1 XExpr t
xe2
  (CE.Pow Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t -> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp2 fpp t
powFn' XExpr t
xe1 XExpr t
xe2
    where powFn' :: FPOp2 fpp t
          powFn' :: Expr t (BaseFloatType fpp)
-> Expr t (BaseFloatType fpp) -> IO (Expr t (BaseFloatType fpp))
powFn' Expr t (BaseFloatType fpp)
e1 Expr t (BaseFloatType fpp)
e2 = do Expr t BaseRealType
re1 <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymReal (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e1
                            Expr t BaseRealType
re2 <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymReal (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e2
                            let args :: Assignment (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
args = (Assignment (Expr t) EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment (Expr t) EmptyCtx
-> Expr t BaseRealType
-> Assignment (Expr t) (EmptyCtx ::> BaseRealType)
forall k (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Expr t BaseRealType
re1 Assignment (Expr t) (EmptyCtx ::> BaseRealType)
-> Expr t BaseRealType
-> Assignment
     (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
forall k (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Expr t BaseRealType
re2)
                            Expr t BaseRealType
rpow <- ExprBuilder t st fs
-> SymFn
     (ExprBuilder t st fs)
     ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
     BaseRealType
-> Assignment
     (SymExpr (ExprBuilder t st fs))
     ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
-> IO (SymReal (ExprBuilder t st fs))
forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
WI.applySymFn ExprBuilder t st fs
sym ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
SymFn
  (ExprBuilder t st fs)
  ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
  BaseRealType
powFn Assignment (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
Assignment
  (SymExpr (ExprBuilder t st fs))
  ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
args
                            ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal (ExprBuilder t st fs)
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
WI.realToFloat ExprBuilder t st fs
sym FloatPrecisionRepr fpp
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
fpRM Expr t BaseRealType
SymReal (ExprBuilder t st fs)
rpow
  (CE.Logb Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t -> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp2 fpp t
logbFn' XExpr t
xe1 XExpr t
xe2
    where logbFn' :: FPOp2 fpp t
          logbFn' :: Expr t (BaseFloatType fpp)
-> Expr t (BaseFloatType fpp) -> IO (Expr t (BaseFloatType fpp))
logbFn' Expr t (BaseFloatType fpp)
e1 Expr t (BaseFloatType fpp)
e2 = do Expr t BaseRealType
re1 <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymReal (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e1
                             Expr t BaseRealType
re2 <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (SymReal (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymReal sym)
WI.floatToReal ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e2
                             let args :: Assignment (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
args = (Assignment (Expr t) EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment (Expr t) EmptyCtx
-> Expr t BaseRealType
-> Assignment (Expr t) (EmptyCtx ::> BaseRealType)
forall k (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Expr t BaseRealType
re1 Assignment (Expr t) (EmptyCtx ::> BaseRealType)
-> Expr t BaseRealType
-> Assignment
     (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
forall k (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Expr t BaseRealType
re2)
                             Expr t BaseRealType
rpow <- ExprBuilder t st fs
-> SymFn
     (ExprBuilder t st fs)
     ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
     BaseRealType
-> Assignment
     (SymExpr (ExprBuilder t st fs))
     ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
-> IO (SymReal (ExprBuilder t st fs))
forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
WI.applySymFn ExprBuilder t st fs
sym ExprSymFn
  t ((EmptyCtx ::> BaseRealType) ::> BaseRealType) BaseRealType
SymFn
  (ExprBuilder t st fs)
  ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
  BaseRealType
logbFn Assignment (Expr t) ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
Assignment
  (SymExpr (ExprBuilder t st fs))
  ((EmptyCtx ::> BaseRealType) ::> BaseRealType)
args
                             ExprBuilder t st fs
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal (ExprBuilder t st fs)
-> IO (SymFloat (ExprBuilder t st fs) fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
WI.realToFloat ExprBuilder t st fs
sym FloatPrecisionRepr fpp
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
fpRM Expr t BaseRealType
SymReal (ExprBuilder t st fs)
rpow
  (CE.Eq Type a
_, XExpr t
xe1, XExpr t
xe2) -> BoolCmp2 t
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
cmp (ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.eqPred ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatEq ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.Ne Type a
_, XExpr t
xe1, XExpr t
xe2) -> BoolCmp2 t
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
cmp BoolCmp2 t
neqPred forall (w :: Nat). BVCmp2 w t
bvNeq forall (fpp :: FloatPrecision). FPCmp2 fpp t
fpNeq XExpr t
xe1 XExpr t
xe2
    where neqPred :: BoolCmp2 t
          neqPred :: BoolCmp2 t
neqPred Expr t BaseBoolType
e1 Expr t BaseBoolType
e2 = do Expr t BaseBoolType
e <- ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.eqPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e1 Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e2
                             ExprBuilder t st fs
-> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e
          bvNeq :: forall w . BVCmp2 w t
          bvNeq :: BVExpr t w -> BVExpr t w -> IO (Expr t BaseBoolType)
bvNeq BVExpr t w
e1 BVExpr t w
e2 = do Expr t BaseBoolType
e <- ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq ExprBuilder t st fs
sym BVExpr t w
SymBV (ExprBuilder t st fs) w
e1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2
                           ExprBuilder t st fs
-> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e
          fpNeq :: forall fpp . FPCmp2 fpp t
          fpNeq :: Expr t (BaseFloatType fpp)
-> Expr t (BaseFloatType fpp) -> IO (Expr t BaseBoolType)
fpNeq Expr t (BaseFloatType fpp)
e1 Expr t (BaseFloatType fpp)
e2 = do Expr t BaseBoolType
e <- ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatEq ExprBuilder t st fs
sym Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e1 Expr t (BaseFloatType fpp)
SymFloat (ExprBuilder t st fs) fpp
e2
                           ExprBuilder t st fs
-> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e
  (CE.Le Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVCmp2 w t)
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSle ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUle ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatLe ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.Ge Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVCmp2 w t)
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSge ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUge ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatGe ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.Lt Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVCmp2 w t)
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSlt ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUlt ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatLt ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.Gt Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVCmp2 w t)
-> (forall (w :: Nat). BVCmp2 w t)
-> (forall (fpp :: FloatPrecision). FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSgt ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (Pred (ExprBuilder t st fs))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUgt ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymFloat (ExprBuilder t st fs) fpp
-> SymFloat (ExprBuilder t st fs) fpp
-> IO (Pred (ExprBuilder t st fs))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
WI.floatGt ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.BwAnd Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (w :: Nat). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAndBits ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAndBits ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.BwOr Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (w :: Nat). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvOrBits ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvOrBits ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  (CE.BwXor Type a
_, XExpr t
xe1, XExpr t
xe2) -> (forall (w :: Nat). BVOp2 w t)
-> (forall (w :: Nat). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvXorBits ExprBuilder t st fs
sym) (ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvXorBits ExprBuilder t st fs
sym) XExpr t
xe1 XExpr t
xe2
  -- 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) <- Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t)))
-> Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall a b. (a -> b) -> a -> b
$ XExpr t -> Maybe (SomeBVExpr t)
forall t. XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe1
    Just (SomeBVExpr BVExpr t w
e2 NatRepr w
w2 BVSign
_ BVExpr t w -> XExpr t
_    ) <- Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t)))
-> Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall a b. (a -> b) -> a -> b
$ XExpr t -> Maybe (SomeBVExpr t)
forall t. XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe2
    BVExpr t w
e2' <- case NatRepr w -> NatRepr w -> NatCases w w
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr w
w1 NatRepr w
w2 of
      NatCaseLT LeqProof (w + 1) w
LeqProof -> ExprBuilder t st fs
-> NatRepr w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc ExprBuilder t st fs
sym NatRepr w
w1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2
      NatCases w w
NatCaseEQ -> BVExpr t w -> IO (BVExpr t w)
forall (m :: * -> *) a. Monad m => a -> m a
return BVExpr t w
e2
      NatCaseGT LeqProof (w + 1) w
LeqProof -> ExprBuilder t st fs
-> NatRepr w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr w
w1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2
    BVExpr t w -> XExpr t
ctor1 (BVExpr t w -> XExpr t) -> IO (BVExpr t w) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvShl ExprBuilder t st fs
sym BVExpr t w
SymBV (ExprBuilder t st fs) w
e1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2'
  (CE.BwShiftR Type a
_ Type b
_, XExpr t
xe1, XExpr t
xe2) -> do
    Just (SomeBVExpr BVExpr t w
e1 NatRepr w
w1 BVSign
sgn1 BVExpr t w -> XExpr t
ctor1) <- Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t)))
-> Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall a b. (a -> b) -> a -> b
$ XExpr t -> Maybe (SomeBVExpr t)
forall t. XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe1
    Just (SomeBVExpr BVExpr t w
e2 NatRepr w
w2 BVSign
_    BVExpr t w -> XExpr t
_    ) <- Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t)))
-> Maybe (SomeBVExpr t) -> IO (Maybe (SomeBVExpr t))
forall a b. (a -> b) -> a -> b
$ XExpr t -> Maybe (SomeBVExpr t)
forall t. XExpr t -> Maybe (SomeBVExpr t)
asBVExpr XExpr t
xe2
    BVExpr t w
e2' <- case NatRepr w -> NatRepr w -> NatCases w w
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr w
w1 NatRepr w
w2 of
      NatCaseLT LeqProof (w + 1) w
LeqProof -> ExprBuilder t st fs
-> NatRepr w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc ExprBuilder t st fs
sym NatRepr w
w1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2
      NatCases w w
NatCaseEQ -> BVExpr t w -> IO (BVExpr t w)
forall (m :: * -> *) a. Monad m => a -> m a
return BVExpr t w
e2
      NatCaseGT LeqProof (w + 1) w
LeqProof -> ExprBuilder t st fs
-> NatRepr w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext ExprBuilder t st fs
sym NatRepr w
w1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2
    BVExpr t w -> XExpr t
ctor1 (BVExpr t w -> XExpr t) -> IO (BVExpr t w) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case BVSign
sgn1 of
      BVSign
Signed -> ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAshr ExprBuilder t st fs
sym BVExpr t w
SymBV (ExprBuilder t st fs) w
e1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2'
      BVSign
Unsigned -> ExprBuilder t st fs
-> SymBV (ExprBuilder t st fs) w
-> SymBV (ExprBuilder t st fs) w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvLshr ExprBuilder t st fs
sym BVExpr t w
SymBV (ExprBuilder t st fs) w
e1 BVExpr t w
SymBV (ExprBuilder t st fs) w
e2'
  -- 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) -> ExprBuilder t st fs
-> Word32
-> Expr t (BaseBVType 32)
-> Vector n (XExpr t)
-> IO (XExpr t)
forall (n :: Nat).
(1 <= n) =>
ExprBuilder t st fs
-> Word32
-> Expr t (BaseBVType 32)
-> Vector n (XExpr t)
-> IO (XExpr t)
buildIndexExpr ExprBuilder t st fs
sym Word32
0 Expr t (BaseBVType 32)
ix Vector n (XExpr t)
xes
      (XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
  (Op2 a b c, XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
  where numOp :: (forall w . BVOp2 w t)
              -> (forall fpp . FPOp2 fpp t)
              -> XExpr t
              -> XExpr t
              -> IO (XExpr t)
        numOp :: (forall (w :: Nat). BVOp2 w t)
-> (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp forall (w :: Nat). BVOp2 w t
bvOp forall (fpp :: FloatPrecision). FPOp2 fpp t
fpOp XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
          (XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8)
-> Expr t (BaseBVType 8) -> IO (Expr t (BaseBVType 8))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
          (XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16)
-> Expr t (BaseBVType 16) -> IO (Expr t (BaseBVType 16))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
          (XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2)-> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32)
-> Expr t (BaseBVType 32) -> IO (Expr t (BaseBVType 32))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
          (XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2)-> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64)
-> Expr t (BaseBVType 64) -> IO (Expr t (BaseBVType 64))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
          (XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2)-> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8)
-> Expr t (BaseBVType 8) -> IO (Expr t (BaseBVType 8))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
          (XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2)-> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16)
-> Expr t (BaseBVType 16) -> IO (Expr t (BaseBVType 16))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
          (XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2)-> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32)
-> Expr t (BaseBVType 32) -> IO (Expr t (BaseBVType 32))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
          (XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2)-> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64)
-> Expr t (BaseBVType 64) -> IO (Expr t (BaseBVType 64))
forall (w :: Nat). BVOp2 w t
bvOp Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
          (XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2)-> Expr t (BaseFloatType Prec32) -> XExpr t
forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat (Expr t (BaseFloatType Prec32) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec32)
-> Expr t (BaseFloatType Prec32)
-> IO (Expr t (BaseFloatType Prec32))
forall (fpp :: FloatPrecision). FPOp2 fpp t
fpOp Expr t (BaseFloatType Prec32)
e1 Expr t (BaseFloatType Prec32)
e2
          (XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2)-> Expr t (BaseFloatType Prec64) -> XExpr t
forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble (Expr t (BaseFloatType Prec64) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec64)
-> Expr t (BaseFloatType Prec64)
-> IO (Expr t (BaseFloatType Prec64))
forall (fpp :: FloatPrecision). FPOp2 fpp t
fpOp Expr t (BaseFloatType Prec64)
e1 Expr t (BaseFloatType Prec64)
e2
          (XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic

        bvOp :: (forall w . BVOp2 w t)
             -> (forall w . BVOp2 w t)
             -> XExpr t
             -> XExpr t
             -> IO (XExpr t)
        bvOp :: (forall (w :: Nat). BVOp2 w t)
-> (forall (w :: Nat). BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp forall (w :: Nat). BVOp2 w t
opS forall (w :: Nat). BVOp2 w t
opU XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
          (XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8)
-> Expr t (BaseBVType 8) -> IO (Expr t (BaseBVType 8))
forall (w :: Nat). BVOp2 w t
opS Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
          (XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16)
-> Expr t (BaseBVType 16) -> IO (Expr t (BaseBVType 16))
forall (w :: Nat). BVOp2 w t
opS Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
          (XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32)
-> Expr t (BaseBVType 32) -> IO (Expr t (BaseBVType 32))
forall (w :: Nat). BVOp2 w t
opS Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
          (XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64)
-> Expr t (BaseBVType 64) -> IO (Expr t (BaseBVType 64))
forall (w :: Nat). BVOp2 w t
opS Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
          (XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 8)
-> Expr t (BaseBVType 8) -> IO (Expr t (BaseBVType 8))
forall (w :: Nat). BVOp2 w t
opU Expr t (BaseBVType 8)
e1 Expr t (BaseBVType 8)
e2
          (XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 16)
-> Expr t (BaseBVType 16) -> IO (Expr t (BaseBVType 16))
forall (w :: Nat). BVOp2 w t
opU Expr t (BaseBVType 16)
e1 Expr t (BaseBVType 16)
e2
          (XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 32)
-> Expr t (BaseBVType 32) -> IO (Expr t (BaseBVType 32))
forall (w :: Nat). BVOp2 w t
opU Expr t (BaseBVType 32)
e1 Expr t (BaseBVType 32)
e2
          (XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseBVType 64)
-> Expr t (BaseBVType 64) -> IO (Expr t (BaseBVType 64))
forall (w :: Nat). BVOp2 w t
opU Expr t (BaseBVType 64)
e1 Expr t (BaseBVType 64)
e2
          (XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic

        fpOp :: (forall fpp . FPOp2 fpp t)
             -> XExpr t
             -> XExpr t
             -> IO (XExpr t)
        fpOp :: (forall (fpp :: FloatPrecision). FPOp2 fpp t)
-> XExpr t -> XExpr t -> IO (XExpr t)
fpOp forall (fpp :: FloatPrecision). FPOp2 fpp t
op XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
          (XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2) -> Expr t (BaseFloatType Prec32) -> XExpr t
forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat (Expr t (BaseFloatType Prec32) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec32)
-> Expr t (BaseFloatType Prec32)
-> IO (Expr t (BaseFloatType Prec32))
forall (fpp :: FloatPrecision). FPOp2 fpp t
op Expr t (BaseFloatType Prec32)
e1 Expr t (BaseFloatType Prec32)
e2
          (XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2) -> Expr t (BaseFloatType Prec64) -> XExpr t
forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble (Expr t (BaseFloatType Prec64) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (BaseFloatType Prec64)
-> Expr t (BaseFloatType Prec64)
-> IO (Expr t (BaseFloatType Prec64))
forall (fpp :: FloatPrecision). FPOp2 fpp t
op Expr t (BaseFloatType Prec64)
e1 Expr t (BaseFloatType Prec64)
e2
          (XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic

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

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

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

        mkIte :: WB.ExprBuilder t st fs
              -> WB.Expr t WT.BaseBoolType
              -> XExpr t
              -> XExpr t
              -> IO (XExpr t)
        mkIte :: ExprBuilder t st fs
-> Expr t BaseBoolType -> XExpr t -> XExpr t -> IO (XExpr t)
mkIte ExprBuilder t st fs
sym Expr t BaseBoolType
pred XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
              (XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.itePred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e1 Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e2
              (XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 8
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 8)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e1 Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e2
              (XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 16
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e1 Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e2
              (XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 32
-> SymBV (ExprBuilder t st fs) 32
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e1 Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e2
              (XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 64
-> SymBV (ExprBuilder t st fs) 64
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e1 Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e2
              (XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 8
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 8)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e1 Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e2
              (XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 16
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e1 Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e2
              (XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 32
-> SymBV (ExprBuilder t st fs) 32
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e1 Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e2
              (XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 64
-> SymBV (ExprBuilder t st fs) 64
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e1 Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e2
              (XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2) -> Expr t (BaseFloatType Prec32) -> XExpr t
forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat (Expr t (BaseFloatType Prec32) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymFloat (ExprBuilder t st fs) Prec32
-> SymFloat (ExprBuilder t st fs) Prec32
-> IO (SymFloat (ExprBuilder t st fs) Prec32)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseFloatType Prec32)
SymFloat (ExprBuilder t st fs) Prec32
e1 Expr t (BaseFloatType Prec32)
SymFloat (ExprBuilder t st fs) Prec32
e2
              (XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2) -> Expr t (BaseFloatType Prec64) -> XExpr t
forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble (Expr t (BaseFloatType Prec64) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymFloat (ExprBuilder t st fs) Prec64
-> SymFloat (ExprBuilder t st fs) Prec64
-> IO (SymFloat (ExprBuilder t st fs) Prec64)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
pred Expr t (BaseFloatType Prec64)
SymFloat (ExprBuilder t st fs) Prec64
e1 Expr t (BaseFloatType Prec64)
SymFloat (ExprBuilder t st fs) Prec64
e2
              (XStruct [XExpr t]
xes1, XStruct [XExpr t]
xes2) ->
                [XExpr t] -> XExpr t
forall t. [XExpr t] -> XExpr t
XStruct ([XExpr t] -> XExpr t) -> IO [XExpr t] -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (XExpr t -> XExpr t -> IO (XExpr t))
-> [XExpr t] -> [XExpr t] -> IO [XExpr t]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (ExprBuilder t st fs
-> Expr t BaseBoolType -> XExpr t -> XExpr t -> IO (XExpr t)
mkIte ExprBuilder t st fs
sym Expr t BaseBoolType
pred) [XExpr t]
xes1 [XExpr t]
xes2
              (XArray Vector n (XExpr t)
xes1, XArray Vector n (XExpr t)
xes2) ->
                case Vector n (XExpr t) -> NatRepr n
forall (n :: Nat) a. Vector n a -> NatRepr n
V.length Vector n (XExpr t)
xes1 NatRepr n -> NatRepr n -> Maybe (n :~: n)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
`testEquality` Vector n (XExpr t) -> NatRepr n
forall (n :: Nat) a. Vector n a -> NatRepr n
V.length Vector n (XExpr t)
xes2 of
                  Just n :~: n
Refl -> Vector n (XExpr t) -> XExpr t
forall (n :: Nat) t. (1 <= n) => Vector n (XExpr t) -> XExpr t
XArray (Vector n (XExpr t) -> XExpr t)
-> IO (Vector n (XExpr t)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (XExpr t -> XExpr t -> IO (XExpr t))
-> Vector n (XExpr t)
-> Vector n (XExpr t)
-> IO (Vector n (XExpr t))
forall (m :: * -> *) a b c (n :: Nat).
Monad m =>
(a -> b -> m c) -> Vector n a -> Vector n b -> m (Vector n c)
V.zipWithM (ExprBuilder t st fs
-> Expr t BaseBoolType -> XExpr t -> XExpr t -> IO (XExpr t)
mkIte ExprBuilder t st fs
sym Expr t BaseBoolType
pred) Vector n (XExpr t)
xes1 Vector n (XExpr t)
Vector n (XExpr t)
xes2
                  Maybe (n :~: n)
Nothing -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
              (XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic


translateOp3 :: forall t st fs a b c d .
                WB.ExprBuilder t st fs
             -> CE.Op3 a b c d
             -> XExpr t
             -> XExpr t
             -> XExpr t
             -> IO (XExpr t)
translateOp3 :: ExprBuilder t st fs
-> Op3 a b c d -> XExpr t -> XExpr t -> XExpr t -> IO (XExpr t)
translateOp3 ExprBuilder t st fs
sym (CE.Mux Type b
_) (XBool Expr t BaseBoolType
te) XExpr t
xe1 XExpr t
xe2 = case (XExpr t
xe1, XExpr t
xe2) of
  (XBool Expr t BaseBoolType
e1, XBool Expr t BaseBoolType
e2) -> Expr t BaseBoolType -> XExpr t
forall t. Expr t BaseBoolType -> XExpr t
XBool (Expr t BaseBoolType -> XExpr t)
-> IO (Expr t BaseBoolType) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.itePred ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e1 Expr t BaseBoolType
Pred (ExprBuilder t st fs)
e2
  (XInt8 Expr t (BaseBVType 8)
e1, XInt8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XInt8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 8
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 8)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e1 Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e2
  (XInt16 Expr t (BaseBVType 16)
e1, XInt16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XInt16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 16
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e1 Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e2
  (XInt32 Expr t (BaseBVType 32)
e1, XInt32 Expr t (BaseBVType 32)
e2) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XInt32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 32
-> SymBV (ExprBuilder t st fs) 32
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e1 Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e2
  (XInt64 Expr t (BaseBVType 64)
e1, XInt64 Expr t (BaseBVType 64)
e2) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XInt64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 64
-> SymBV (ExprBuilder t st fs) 64
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e1 Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e2
  (XWord8 Expr t (BaseBVType 8)
e1, XWord8 Expr t (BaseBVType 8)
e2) -> Expr t (BaseBVType 8) -> XExpr t
forall t. Expr t (BaseBVType 8) -> XExpr t
XWord8 (Expr t (BaseBVType 8) -> XExpr t)
-> IO (Expr t (BaseBVType 8)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 8
-> SymBV (ExprBuilder t st fs) 8
-> IO (SymBV (ExprBuilder t st fs) 8)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e1 Expr t (BaseBVType 8)
SymBV (ExprBuilder t st fs) 8
e2
  (XWord16 Expr t (BaseBVType 16)
e1, XWord16 Expr t (BaseBVType 16)
e2) -> Expr t (BaseBVType 16) -> XExpr t
forall t. Expr t (BaseBVType 16) -> XExpr t
XWord16 (Expr t (BaseBVType 16) -> XExpr t)
-> IO (Expr t (BaseBVType 16)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 16
-> SymBV (ExprBuilder t st fs) 16
-> IO (SymBV (ExprBuilder t st fs) 16)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e1 Expr t (BaseBVType 16)
SymBV (ExprBuilder t st fs) 16
e2
  (XWord32 Expr t (BaseBVType 32)
e1, XWord32 Expr t (BaseBVType 32)
e2) -> Expr t (BaseBVType 32) -> XExpr t
forall t. Expr t (BaseBVType 32) -> XExpr t
XWord32 (Expr t (BaseBVType 32) -> XExpr t)
-> IO (Expr t (BaseBVType 32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 32
-> SymBV (ExprBuilder t st fs) 32
-> IO (SymBV (ExprBuilder t st fs) 32)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e1 Expr t (BaseBVType 32)
SymBV (ExprBuilder t st fs) 32
e2
  (XWord64 Expr t (BaseBVType 64)
e1, XWord64 Expr t (BaseBVType 64)
e2) -> Expr t (BaseBVType 64) -> XExpr t
forall t. Expr t (BaseBVType 64) -> XExpr t
XWord64 (Expr t (BaseBVType 64) -> XExpr t)
-> IO (Expr t (BaseBVType 64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymBV (ExprBuilder t st fs) 64
-> SymBV (ExprBuilder t st fs) 64
-> IO (SymBV (ExprBuilder t st fs) 64)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e1 Expr t (BaseBVType 64)
SymBV (ExprBuilder t st fs) 64
e2
  (XFloat Expr t (BaseFloatType Prec32)
e1, XFloat Expr t (BaseFloatType Prec32)
e2) -> Expr t (BaseFloatType Prec32) -> XExpr t
forall t. Expr t (BaseFloatType Prec32) -> XExpr t
XFloat (Expr t (BaseFloatType Prec32) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec32)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymFloat (ExprBuilder t st fs) Prec32
-> SymFloat (ExprBuilder t st fs) Prec32
-> IO (SymFloat (ExprBuilder t st fs) Prec32)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseFloatType Prec32)
SymFloat (ExprBuilder t st fs) Prec32
e1 Expr t (BaseFloatType Prec32)
SymFloat (ExprBuilder t st fs) Prec32
e2
  (XDouble Expr t (BaseFloatType Prec64)
e1, XDouble Expr t (BaseFloatType Prec64)
e2) -> Expr t (BaseFloatType Prec64) -> XExpr t
forall t. Expr t (BaseFloatType Prec64) -> XExpr t
XDouble (Expr t (BaseFloatType Prec64) -> XExpr t)
-> IO (Expr t (BaseFloatType Prec64)) -> IO (XExpr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymFloat (ExprBuilder t st fs) Prec64
-> SymFloat (ExprBuilder t st fs) Prec64
-> IO (SymFloat (ExprBuilder t st fs) Prec64)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
WI.floatIte ExprBuilder t st fs
sym Expr t BaseBoolType
Pred (ExprBuilder t st fs)
te Expr t (BaseFloatType Prec64)
SymFloat (ExprBuilder t st fs) Prec64
e1 Expr t (BaseFloatType Prec64)
SymFloat (ExprBuilder t st fs) Prec64
e2
  (XExpr t, XExpr t)
_ -> IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic
translateOp3 ExprBuilder t st fs
_ Op3 a b c d
_ XExpr t
_ XExpr t
_ XExpr t
_ = IO (XExpr t)
forall (m :: * -> *) a. MonadIO m => m a
panic