    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TupleSections #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# LANGUAGE ViewPatterns #-}
    {-# LANGUAGE MultiWayIf #-}

    -- | A parser for an s-expression representation of what4 expressions
    module What4.Serialize.Parser
      ( deserializeExpr
      , deserializeExprWithConfig
      , deserializeSymFn
      , deserializeSymFnWithConfig
      , deserializeBaseType
      , readBaseTypes
      , Atom(..)
      , S.WellFormedSExpr(..)
      , Config(..)
      , defaultConfig
      , SomeSymFn(..)
      , type SExpr
      , parseSExpr
      , printSExpr
      ) where

    import           Control.Monad ( when )
    import qualified Control.Monad.Except as E
    import           Control.Monad.IO.Class ( liftIO )
    import qualified Control.Monad.Reader as R
    import qualified Data.BitVector.Sized as BV
    import qualified Data.Foldable as F
    import qualified Data.HashMap.Lazy as HM
    import           Data.Kind
    import qualified Data.SCargot.Repr.WellFormed as S

    import           Data.Text ( Text )
    import qualified Data.Text as T
    import qualified Data.Text.Encoding as T
    import           Text.Printf ( printf )

    import qualified Data.Parameterized.NatRepr as PN
    import qualified Data.Parameterized.Ctx as Ctx
    import qualified Data.Parameterized.Context as Ctx
    import           Data.Parameterized.Classes
    import           Data.Parameterized.Some ( Some(..) )
    import qualified Data.Parameterized.TraversableFC as FC
    import           What4.BaseTypes

    import qualified What4.Expr.ArrayUpdateMap as WAU
    import qualified What4.Expr.Builder as W4
    import qualified What4.IndexLit as WIL
    import qualified What4.Interface as W4

    import           What4.Serialize.SETokens ( Atom(..), printSExpr, parseSExpr )
    import qualified What4.Utils.Serialize as U
    import           What4.Serialize.Printer ( SExpr )

    import           Prelude

    data SomeSymFn t = forall dom ret. SomeSymFn (W4.SymFn t dom ret)

    data Config sym =
      Config
      { forall sym. Config sym -> Text -> IO (Maybe (SomeSymFn sym))
    cSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
      -- ^ The mapping of names to defined What4 SymFns.
      , forall sym. Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
    cExprLookup :: Text -> IO (Maybe (Some (W4.SymExpr sym)))
      -- ^ The mapping of names to defined What4 expressions.
      }

    defaultConfig :: (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym)) => sym -> Config sym
    defaultConfig :: forall sym.
    (IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
    sym -> Config sym
    defaultConfig sym
    _sym = Config { cSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
    cSymFnLookup = IO (Maybe (SomeSymFn sym)) -> Text -> IO (Maybe (SomeSymFn sym))
    forall a b. a -> b -> a
    const (Maybe (SomeSymFn sym) -> IO (Maybe (SomeSymFn sym))
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Maybe (SomeSymFn sym)
    forall a. Maybe a
    Nothing)
                                , cExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))
    cExprLookup = IO (Maybe (Some (SymExpr sym)))
    -> Text -> IO (Maybe (Some (SymExpr sym)))
    forall a b. a -> b -> a
    const (Maybe (Some (SymExpr sym)) -> IO (Maybe (Some (SymExpr sym)))
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Maybe (Some (SymExpr sym))
    forall a. Maybe a
    Nothing)
                                }

    -- | The lexical environment for parsing s-expressions and
    -- procesing them into What4 terms.
    data ProcessorEnv sym =
      ProcessorEnv
      { forall sym. ProcessorEnv sym -> sym
    procSym :: sym
      -- ^ The symbolic What4 backend being used.
      , forall sym. ProcessorEnv sym -> Text -> IO (Maybe (SomeSymFn sym))
    procSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
        -- ^ The user-specified mapping of names to defined What4 SymFns.
      , forall sym.
    ProcessorEnv sym -> Text -> IO (Maybe (Some (SymExpr sym)))
    procExprLookup :: Text -> IO (Maybe (Some (W4.SymExpr sym)))
      -- ^ The user-specified mapping of names to defined What4 expressions.
      , forall sym. ProcessorEnv sym -> HashMap Text (Some (SymExpr sym))
    procLetEnv :: HM.HashMap Text (Some (W4.SymExpr sym))
      -- ^ The current lexical environment w.r.t. let-bindings
      -- encountered while parsing. N.B., these bindings are
      -- checked _before_ the \"global\" bindings implied by the
      -- user-specified lookup functions.
      , forall sym. ProcessorEnv sym -> HashMap Text (SomeSymFn sym)
    procLetFnEnv :: HM.HashMap Text (SomeSymFn sym)
      -- ^ The current lexical symfn environment
      -- w.r.t. letfn-bindings encountered while parsing. N.B.,
      -- these bindings are checked /before/ the \"global\"
      -- bindings implied by the user-specified lookup
      -- functions.
      }

    type Processor sym a = E.ExceptT String (R.ReaderT (ProcessorEnv sym) IO) a

    runProcessor :: ProcessorEnv sym -> Processor sym a -> IO (Either String a)
    runProcessor :: forall sym a.
    ProcessorEnv sym -> Processor sym a -> IO (Either String a)
    runProcessor ProcessorEnv sym
    env Processor sym a
    action = ReaderT (ProcessorEnv sym) IO (Either String a)
    -> ProcessorEnv sym -> IO (Either String a)
    forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
    R.runReaderT (Processor sym a -> ReaderT (ProcessorEnv sym) IO (Either String a)
    forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
    E.runExceptT Processor sym a
    action) ProcessorEnv sym
    env

    lookupExpr :: Text -> Processor sym (Maybe (Some (W4.SymExpr sym)))
    lookupExpr :: forall sym. Text -> Processor sym (Maybe (Some (SymExpr sym)))
    lookupExpr Text
    nm = do
      userLookupFn <- (ProcessorEnv sym -> Text -> IO (Maybe (Some (SymExpr sym))))
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Text -> IO (Maybe (Some (SymExpr sym))))
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.asks ProcessorEnv sym -> Text -> IO (Maybe (Some (SymExpr sym)))
    forall sym.
    ProcessorEnv sym -> Text -> IO (Maybe (Some (SymExpr sym)))
    procExprLookup
      letEnv <- R.asks procLetEnv
      case HM.lookup nm letEnv of
        Maybe (Some (SymExpr sym))
    Nothing -> IO (Maybe (Some (SymExpr sym)))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Maybe (Some (SymExpr sym)))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (IO (Maybe (Some (SymExpr sym)))
     -> ExceptT
          String
          (ReaderT (ProcessorEnv sym) IO)
          (Maybe (Some (SymExpr sym))))
    -> IO (Maybe (Some (SymExpr sym)))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Maybe (Some (SymExpr sym)))
    forall a b. (a -> b) -> a -> b
    $ Text -> IO (Maybe (Some (SymExpr sym)))
    userLookupFn Text
    nm
        Maybe (Some (SymExpr sym))
    res -> Maybe (Some (SymExpr sym))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Maybe (Some (SymExpr sym)))
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Maybe (Some (SymExpr sym))
    res

    lookupFn :: Text -> Processor sym (Maybe (SomeSymFn sym))
    lookupFn :: forall sym. Text -> Processor sym (Maybe (SomeSymFn sym))
    lookupFn Text
    nm = do
      userLookupFn <- (ProcessorEnv sym -> Text -> IO (Maybe (SomeSymFn sym)))
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Text -> IO (Maybe (SomeSymFn sym)))
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.asks ProcessorEnv sym -> Text -> IO (Maybe (SomeSymFn sym))
    forall sym. ProcessorEnv sym -> Text -> IO (Maybe (SomeSymFn sym))
    procSymFnLookup
      letEnv <- R.asks procLetFnEnv
      case HM.lookup nm letEnv of
        Maybe (SomeSymFn sym)
    Nothing -> IO (Maybe (SomeSymFn sym))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Maybe (SomeSymFn sym))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (IO (Maybe (SomeSymFn sym))
     -> ExceptT
          String (ReaderT (ProcessorEnv sym) IO) (Maybe (SomeSymFn sym)))
    -> IO (Maybe (SomeSymFn sym))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Maybe (SomeSymFn sym))
    forall a b. (a -> b) -> a -> b
    $ Text -> IO (Maybe (SomeSymFn sym))
    userLookupFn Text
    nm
        Maybe (SomeSymFn sym)
    res -> Maybe (SomeSymFn sym)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Maybe (SomeSymFn sym))
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Maybe (SomeSymFn sym)
    res

    -- | @(deserializeExpr sym)@ is equivalent
    -- to @(deserializeExpr' (defaultConfig sym))@.
    deserializeExpr ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => sym
      -> SExpr
      -> IO (Either String (Some (W4.SymExpr sym)))
    deserializeExpr :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym -> SExpr -> IO (Either String (Some (SymExpr sym)))
    deserializeExpr sym
    sym = sym
    -> Config sym -> SExpr -> IO (Either String (Some (SymExpr sym)))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym
    -> Config sym -> SExpr -> IO (Either String (Some (SymExpr sym)))
    deserializeExprWithConfig sym
    sym Config sym
    cfg
      where cfg :: Config sym
    cfg = sym -> Config sym
    forall sym.
    (IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
    sym -> Config sym
    defaultConfig sym
    sym

    deserializeExprWithConfig ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => sym
      -> Config sym
      -> SExpr
      -> IO (Either String (Some (W4.SymExpr sym)))
    deserializeExprWithConfig :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym
    -> Config sym -> SExpr -> IO (Either String (Some (SymExpr sym)))
    deserializeExprWithConfig sym
    sym Config sym
    cfg SExpr
    sexpr = ProcessorEnv sym
    -> Processor sym (Some (Expr t))
    -> IO (Either String (Some (Expr t)))
    forall sym a.
    ProcessorEnv sym -> Processor sym a -> IO (Either String a)
    runProcessor ProcessorEnv sym
    env (SExpr -> Processor sym (Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> Processor sym (Some (SymExpr sym))
    readExpr SExpr
    sexpr)
      where env :: ProcessorEnv sym
    env = ProcessorEnv { procSym :: sym
    procSym = sym
    sym
                               , procSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
    procSymFnLookup = Config sym -> Text -> IO (Maybe (SomeSymFn sym))
    forall sym. Config sym -> Text -> IO (Maybe (SomeSymFn sym))
    cSymFnLookup Config sym
    cfg
                               , procExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))
    procExprLookup = Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
    forall sym. Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
    cExprLookup Config sym
    cfg
                               , procLetEnv :: HashMap Text (Some (SymExpr sym))
    procLetEnv = HashMap Text (Some (SymExpr sym))
    HashMap Text (Some (Expr t))
    forall k v. HashMap k v
    HM.empty
                               , procLetFnEnv :: HashMap Text (SomeSymFn sym)
    procLetFnEnv = HashMap Text (SomeSymFn sym)
    forall k v. HashMap k v
    HM.empty
                               }

    -- | @(deserializeSymFn sym)@ is equivalent
    -- to @(deserializeSymFn' (defaultConfig sym))@.
    deserializeSymFn ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => sym
      -> SExpr
      -> IO (Either String (SomeSymFn sym))
    deserializeSymFn :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym -> SExpr -> IO (Either String (SomeSymFn sym))
    deserializeSymFn sym
    sym = sym -> Config sym -> SExpr -> IO (Either String (SomeSymFn sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym -> Config sym -> SExpr -> IO (Either String (SomeSymFn sym))
    deserializeSymFnWithConfig sym
    sym Config sym
    cfg
      where cfg :: Config sym
    cfg = sym -> Config sym
    forall sym.
    (IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
    sym -> Config sym
    defaultConfig sym
    sym

    deserializeSymFnWithConfig ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => sym
      -> Config sym
      -> SExpr
      -> IO (Either String (SomeSymFn sym))
    deserializeSymFnWithConfig :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym -> Config sym -> SExpr -> IO (Either String (SomeSymFn sym))
    deserializeSymFnWithConfig sym
    sym Config sym
    cfg SExpr
    sexpr = ProcessorEnv sym
    -> Processor sym (SomeSymFn sym)
    -> IO (Either String (SomeSymFn sym))
    forall sym a.
    ProcessorEnv sym -> Processor sym a -> IO (Either String a)
    runProcessor ProcessorEnv sym
    env (SExpr -> Processor sym (SomeSymFn sym)
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> Processor sym (SomeSymFn sym)
    readSymFn SExpr
    sexpr)
      where env :: ProcessorEnv sym
    env = ProcessorEnv { procSym :: sym
    procSym = sym
    sym
                               , procSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
    procSymFnLookup = Config sym -> Text -> IO (Maybe (SomeSymFn sym))
    forall sym. Config sym -> Text -> IO (Maybe (SomeSymFn sym))
    cSymFnLookup Config sym
    cfg
                               , procExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))
    procExprLookup = Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
    forall sym. Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
    cExprLookup Config sym
    cfg
                               , procLetEnv :: HashMap Text (Some (SymExpr sym))
    procLetEnv = HashMap Text (Some (SymExpr sym))
    HashMap Text (Some (Expr t))
    forall k v. HashMap k v
    HM.empty
                               , procLetFnEnv :: HashMap Text (SomeSymFn sym)
    procLetFnEnv = HashMap Text (SomeSymFn sym)
    forall k v. HashMap k v
    HM.empty
                               }

    deserializeBaseType ::
      SExpr
      -> Either String (Some BaseTypeRepr)
    deserializeBaseType :: SExpr -> Either String (Some BaseTypeRepr)
    deserializeBaseType SExpr
    sexpr = SExpr -> Either String (Some BaseTypeRepr)
    forall (m :: Type -> Type).
    MonadError String m =>
    SExpr -> m (Some BaseTypeRepr)
    readBaseType SExpr
    sexpr

    -- * First pass of parsing turns the raw text into s-expressions.
    --   This pass is handled by the code in What4.Serialize.SETokens

    -- * Second pass of parsing: turning the s-expressions into symbolic expressions
    -- and the overall templated formula

    -- ** Utility functions

    -- | Utility function for contextualizing errors. Prepends the given prefix
    -- whenever an error is thrown.
    prefixError :: (Monoid e, E.MonadError e m) => e -> m a -> m a
    prefixError :: forall e (m :: Type -> Type) a.
    (Monoid e, MonadError e m) =>
    e -> m a -> m a
    prefixError e
    prefix m a
    act = m a -> (e -> m a) -> m a
    forall a. m a -> (e -> m a) -> m a
    forall e (m :: Type -> Type) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    E.catchError m a
    act (e -> m a
    forall a. e -> m a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (e -> m a) -> (e -> e) -> e -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . e -> e -> e
    forall a. Monoid a => a -> a -> a
    mappend e
    prefix)

    -- | Utility function for lifting a 'Maybe' into a 'MonadError'
    fromMaybeError :: (E.MonadError e m) => e -> Maybe a -> m a
    fromMaybeError :: forall e (m :: Type -> Type) a.
    MonadError e m =>
    e -> Maybe a -> m a
    fromMaybeError e
    err = m a -> (a -> m a) -> Maybe a -> m a
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (e -> m a
    forall a. e -> m a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError e
    err) a -> m a
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return

    readBaseType ::
      forall m . (E.MonadError String m)
      => SExpr
      -> m (Some BaseTypeRepr)
    readBaseType :: forall (m :: Type -> Type).
    MonadError String m =>
    SExpr -> m (Some BaseTypeRepr)
    readBaseType SExpr
    sexpr =
      case SExpr
    sexpr of
        S.WFSAtom (AId Text
    atom) ->
          case (Text -> String
    T.unpack Text
    atom) of
            String
    "Bool" -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
    -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr 'BaseBoolType -> Some BaseTypeRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some BaseTypeRepr 'BaseBoolType
    BaseBoolRepr
            String
    "Int" -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
    -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr 'BaseIntegerType -> Some BaseTypeRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some BaseTypeRepr 'BaseIntegerType
    BaseIntegerRepr
            String
    "Real" -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
    -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr 'BaseRealType -> Some BaseTypeRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some BaseTypeRepr 'BaseRealType
    BaseRealRepr
            String
    "String" -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
    -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr ('BaseStringType 'Unicode) -> Some BaseTypeRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (StringInfoRepr 'Unicode -> BaseTypeRepr ('BaseStringType 'Unicode)
    forall (si :: StringInfo).
    StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
    BaseStringRepr StringInfoRepr 'Unicode
    UnicodeRepr)
            String
    "Complex" -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
    -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr 'BaseComplexType -> Some BaseTypeRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some BaseTypeRepr 'BaseComplexType
    BaseComplexRepr
            String
    _ -> m (Some BaseTypeRepr)
    panic
        S.WFSList [(S.WFSAtom (AId Text
    "BV")), (S.WFSAtom (AInt Integer
    w))]
          | Just (Some NatRepr x
    wRepr) <- Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat Integer
    w
          , Just LeqProof 1 x
    LeqProof <- NatRepr 1 -> NatRepr x -> Maybe (LeqProof 1 x)
    forall (m :: Nat) (n :: Nat).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq (forall (n :: Nat). KnownNat n => NatRepr n
    knownNat @1) NatRepr x
    wRepr
            -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
    -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr ('BaseBVType x) -> Some BaseTypeRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (NatRepr x -> BaseTypeRepr ('BaseBVType x)
    forall (w :: Nat).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr x
    wRepr)
          | Bool
    otherwise
            -> m (Some BaseTypeRepr)
    panic
        S.WFSList [(S.WFSAtom (AId Text
    "Float")), (S.WFSAtom (AInt Integer
    e)), (S.WFSAtom (AInt Integer
    s))]
          | Just (Some NatRepr x
    eRepr) <- Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat Integer
    e
          , Just (Some NatRepr x
    sRepr) <- Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat Integer
    s
          , Just LeqProof 2 x
    LeqProof <- NatRepr 2 -> NatRepr x -> Maybe (LeqProof 2 x)
    forall (m :: Nat) (n :: Nat).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq (forall (n :: Nat). KnownNat n => NatRepr n
    knownNat @2) NatRepr x
    eRepr
          , Just LeqProof 2 x
    LeqProof <- NatRepr 2 -> NatRepr x -> Maybe (LeqProof 2 x)
    forall (m :: Nat) (n :: Nat).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq (forall (n :: Nat). KnownNat n => NatRepr n
    knownNat @2) NatRepr x
    sRepr
            -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (BaseTypeRepr ('BaseFloatType ('FloatingPointPrecision x x))
    -> Some BaseTypeRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (FloatPrecisionRepr ('FloatingPointPrecision x x)
    -> BaseTypeRepr ('BaseFloatType ('FloatingPointPrecision x x))
    forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
    BaseFloatRepr (NatRepr x
    -> NatRepr x -> FloatPrecisionRepr ('FloatingPointPrecision x x)
    forall (eb :: Nat) (sb :: Nat).
    (2 <= eb, 2 <= sb) =>
    NatRepr eb
    -> NatRepr sb -> FloatPrecisionRepr ('FloatingPointPrecision eb sb)
    FloatingPointPrecisionRepr NatRepr x
    eRepr NatRepr x
    sRepr)))
          | Bool
    otherwise -> m (Some BaseTypeRepr)
    panic
        S.WFSList [(S.WFSAtom (AId Text
    "Struct")), SExpr
    args] -> do
          Some tps <- SExpr -> m (Some (Assignment BaseTypeRepr))
    forall (m :: Type -> Type).
    MonadError String m =>
    SExpr -> m (Some (Assignment BaseTypeRepr))
    readBaseTypes SExpr
    args
          return $ Some (BaseStructRepr tps)
        S.WFSList [S.WFSAtom (AId Text
    "Array"), SExpr
    ixArgs, SExpr
    tpArg] -> do
          Some ixs <- SExpr -> m (Some (Assignment BaseTypeRepr))
    forall (m :: Type -> Type).
    MonadError String m =>
    SExpr -> m (Some (Assignment BaseTypeRepr))
    readBaseTypes SExpr
    ixArgs
          Some tp <- readBaseType tpArg
          case Ctx.viewAssign ixs of
            AssignView BaseTypeRepr x
    Ctx.AssignEmpty -> String -> m (Some BaseTypeRepr)
    forall a. String -> m a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String -> m (Some BaseTypeRepr))
    -> String -> m (Some BaseTypeRepr)
    forall a b. (a -> b) -> a -> b
    $ String
    "array type has no indices: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    sexpr
            Ctx.AssignExtend Assignment BaseTypeRepr ctx1
    _ BaseTypeRepr tp
    _ -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
    -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr ('BaseArrayType (ctx1 '::> tp) x) -> Some BaseTypeRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Assignment BaseTypeRepr (ctx1 '::> tp)
    -> BaseTypeRepr x -> BaseTypeRepr ('BaseArrayType (ctx1 '::> tp) x)
    forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
    Assignment BaseTypeRepr (idx ::> tp)
    -> BaseTypeRepr xs -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
    BaseArrayRepr Assignment BaseTypeRepr x
    Assignment BaseTypeRepr (ctx1 '::> tp)
    ixs BaseTypeRepr x
    tp)
        SExpr
    _ -> m (Some BaseTypeRepr)
    panic
      where
        panic :: m (Some BaseTypeRepr)
    panic = String -> m (Some BaseTypeRepr)
    forall a. String -> m a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String -> m (Some BaseTypeRepr))
    -> String -> m (Some BaseTypeRepr)
    forall a b. (a -> b) -> a -> b
    $ String
    "unknown base type: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    sexpr

    readBaseTypes ::
      forall m . (E.MonadError String m)
      => SExpr
      -> m (Some (Ctx.Assignment BaseTypeRepr))
    readBaseTypes :: forall (m :: Type -> Type).
    MonadError String m =>
    SExpr -> m (Some (Assignment BaseTypeRepr))
    readBaseTypes sexpr :: SExpr
    sexpr@(S.WFSAtom Atom
    _) = String -> m (Some (Assignment BaseTypeRepr))
    forall a. String -> m a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String -> m (Some (Assignment BaseTypeRepr)))
    -> String -> m (Some (Assignment BaseTypeRepr))
    forall a b. (a -> b) -> a -> b
    $ String
    "expected list of base types: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    sexpr
    readBaseTypes (S.WFSList [SExpr]
    sexprs) = [Some BaseTypeRepr] -> Some (Assignment BaseTypeRepr)
    forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
    Ctx.fromList ([Some BaseTypeRepr] -> Some (Assignment BaseTypeRepr))
    -> m [Some BaseTypeRepr] -> m (Some (Assignment BaseTypeRepr))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (SExpr -> m (Some BaseTypeRepr))
    -> [SExpr] -> m [Some BaseTypeRepr]
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> [a] -> m [b]
    mapM SExpr -> m (Some BaseTypeRepr)
    forall (m :: Type -> Type).
    MonadError String m =>
    SExpr -> m (Some BaseTypeRepr)
    readBaseType [SExpr]
    sexprs

    -- ** Parsing definitions

    -- | Stores a NatRepr along with proof that its type parameter is a bitvector of
    -- that length. Used for easy pattern matching on the LHS of a binding in a
    -- do-expression to extract the proof.
    data BVProof tp where
      BVProof :: forall n. (1 <= n) => NatRepr n -> BVProof (BaseBVType n)

    -- | Given an expression, monadically either returns proof that it is a
    -- bitvector or throws an error.
    getBVProof :: (W4.IsExpr ex, E.MonadError String m) => ex tp -> m (BVProof tp)
    getBVProof :: forall (ex :: BaseType -> Type) (m :: Type -> Type)
           (tp :: BaseType).
    (IsExpr ex, MonadError String m) =>
    ex tp -> m (BVProof tp)
    getBVProof ex tp
    expr =
      case ex tp -> BaseTypeRepr tp
    forall (tp :: BaseType). ex tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W4.exprType ex tp
    expr of
        BaseBVRepr NatRepr w
    n -> BVProof tp -> m (BVProof tp)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (BVProof tp -> m (BVProof tp)) -> BVProof tp -> m (BVProof tp)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w -> BVProof ('BaseBVType w)
    forall (res :: Nat).
    (1 <= res) =>
    NatRepr res -> BVProof (BaseBVType res)
    BVProof NatRepr w
    n
        BaseTypeRepr tp
    t -> String -> m (BVProof tp)
    forall a. String -> m a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String -> m (BVProof tp)) -> String -> m (BVProof tp)
    forall a b. (a -> b) -> a -> b
    $ String -> String -> String
    forall r. PrintfType r => String -> r
    printf String
    "expected BV, found %s" (BaseTypeRepr tp -> String
    forall a. Show a => a -> String
    show BaseTypeRepr tp
    t)

    -- | Operator type descriptions for parsing s-expression of
    -- the form @(operator operands ...)@.
    data Op sym where
        FloatOp1 :: (forall fpp . sym ->
                     W4.SymFloat sym fpp ->
                     IO (W4.SymFloat sym fpp))
                 -> Op sym
        -- | Generic unary operator description.
        Op1 :: Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1)
            -> (sym ->
                W4.SymExpr sym arg1 ->
                IO (W4.SymExpr sym ret))
            -> Op sym
        -- | Generic dyadic operator description.
        Op2 :: Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1 Ctx.::> arg2)
            -> (sym ->
                W4.SymExpr sym arg1 ->
                W4.SymExpr sym arg2 ->
                IO (W4.SymExpr sym ret))
            -> Op sym
        -- | Generic triadic operator description.
        Op3 :: Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1 Ctx.::> arg2 Ctx.::> arg3)
            -> (sym ->
                W4.SymExpr sym arg1 ->
                W4.SymExpr sym arg2 ->
                W4.SymExpr sym arg3 ->
                IO (W4.SymExpr sym ret)
               )
            -> Op sym
        -- | Generic tetradic operator description.
        Op4 :: Ctx.Assignment
               BaseTypeRepr
               (Ctx.EmptyCtx Ctx.::> arg1 Ctx.::> arg2 Ctx.::> arg3 Ctx.::> arg4)
            -> ( sym ->
                 W4.SymExpr sym arg1 ->
                 W4.SymExpr sym arg2 ->
                 W4.SymExpr sym arg3 ->
                 W4.SymExpr sym arg4 ->
                 IO (W4.SymExpr sym ret)
               )
            -> Op sym
        -- | Encapsulating type for a unary operation that takes one bitvector and
        -- returns another (in IO).
        BVOp1 :: (forall w . (1 <= w) =>
                   sym ->
                   W4.SymBV sym w ->
                   IO (W4.SymBV sym w))
              -> Op sym
        -- | Binop with a bitvector return type, e.g., addition or bitwise operations.
        BVOp2 :: (forall w . (1 <= w) =>
                   sym ->
                   W4.SymBV sym w ->
                   W4.SymBV sym w ->
                   IO (W4.SymBV sym w))
              -> Op sym
        -- | Bitvector binop with a boolean return type, i.e., comparison operators.
        BVComp2 :: (forall w . (1 <= w) =>
                        sym ->
                        W4.SymBV sym w ->
                        W4.SymBV sym w ->
                        IO (W4.Pred sym))
                    -> Op sym

    -- | Lookup mapping operators to their Op definitions (if they exist)
    lookupOp :: forall sym . W4.IsSymExprBuilder sym => Text -> Maybe (Op sym)
    lookupOp :: forall sym. IsSymExprBuilder sym => Text -> Maybe (Op sym)
    lookupOp Text
    name = Text -> HashMap Text (Op sym) -> Maybe (Op sym)
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HM.lookup Text
    name HashMap Text (Op sym)
    forall sym. IsSymExprBuilder sym => HashMap Text (Op sym)
    opTable

    opTable :: (W4.IsSymExprBuilder sym) => HM.HashMap Text (Op sym)
    opTable :: forall sym. IsSymExprBuilder sym => HashMap Text (Op sym)
    opTable =
      [(Text, Op sym)] -> HashMap Text (Op sym)
    forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
    HM.fromList [
      -- -- -- Boolean ops -- -- --
        (Text
    "andp", Assignment
      BaseTypeRepr (('EmptyCtx ::> 'BaseBoolType) ::> 'BaseBoolType)
    -> (sym
        -> SymExpr sym 'BaseBoolType
        -> SymExpr sym 'BaseBoolType
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr (('EmptyCtx ::> 'BaseBoolType) ::> 'BaseBoolType)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym 'BaseBoolType
      -> SymExpr sym 'BaseBoolType
      -> IO (SymExpr sym 'BaseBoolType))
     -> Op sym)
    -> (sym
        -> SymExpr sym 'BaseBoolType
        -> SymExpr sym 'BaseBoolType
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym 'BaseBoolType
    -> SymExpr sym 'BaseBoolType
    -> IO (SymExpr sym 'BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.andPred)
      , (Text
    "orp", Assignment
      BaseTypeRepr (('EmptyCtx ::> 'BaseBoolType) ::> 'BaseBoolType)
    -> (sym
        -> SymExpr sym 'BaseBoolType
        -> SymExpr sym 'BaseBoolType
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr (('EmptyCtx ::> 'BaseBoolType) ::> 'BaseBoolType)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym 'BaseBoolType
      -> SymExpr sym 'BaseBoolType
      -> IO (SymExpr sym 'BaseBoolType))
     -> Op sym)
    -> (sym
        -> SymExpr sym 'BaseBoolType
        -> SymExpr sym 'BaseBoolType
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym 'BaseBoolType
    -> SymExpr sym 'BaseBoolType
    -> IO (SymExpr sym 'BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.orPred)
      , (Text
    "xorp", Assignment
      BaseTypeRepr (('EmptyCtx ::> 'BaseBoolType) ::> 'BaseBoolType)
    -> (sym
        -> SymExpr sym 'BaseBoolType
        -> SymExpr sym 'BaseBoolType
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr (('EmptyCtx ::> 'BaseBoolType) ::> 'BaseBoolType)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym 'BaseBoolType
      -> SymExpr sym 'BaseBoolType
      -> IO (SymExpr sym 'BaseBoolType))
     -> Op sym)
    -> (sym
        -> SymExpr sym 'BaseBoolType
        -> SymExpr sym 'BaseBoolType
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym 'BaseBoolType
    -> SymExpr sym 'BaseBoolType
    -> IO (SymExpr sym 'BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    W4.xorPred)
      , (Text
    "notp", Assignment BaseTypeRepr ('EmptyCtx ::> 'BaseBoolType)
    -> (sym
        -> SymExpr sym 'BaseBoolType -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall (res :: BaseType) sym (arg2 :: BaseType).
    Assignment BaseTypeRepr ('EmptyCtx ::> res)
    -> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
    Op1 Assignment BaseTypeRepr ('EmptyCtx ::> 'BaseBoolType)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym 'BaseBoolType -> IO (SymExpr sym 'BaseBoolType))
     -> Op sym)
    -> (sym
        -> SymExpr sym 'BaseBoolType -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ sym -> SymExpr sym 'BaseBoolType -> IO (SymExpr sym 'BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    W4.notPred)
      -- -- -- Float ops -- -- --
      , (Text
    "floatneg", (forall (fpp :: FloatPrecision).
     sym -> SymFloat sym fpp -> IO (SymFloat sym fpp))
    -> Op sym
    forall sym.
    (forall (fpp :: FloatPrecision).
     sym -> SymFloat sym fpp -> IO (SymFloat sym fpp))
    -> Op sym
    FloatOp1 sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    W4.floatNeg)
      , (Text
    "floatabs", (forall (fpp :: FloatPrecision).
     sym -> SymFloat sym fpp -> IO (SymFloat sym fpp))
    -> Op sym
    forall sym.
    (forall (fpp :: FloatPrecision).
     sym -> SymFloat sym fpp -> IO (SymFloat sym fpp))
    -> Op sym
    FloatOp1 sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    W4.floatAbs)
      -- -- -- Integer ops -- -- --
      , (Text
    "intmul", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
    -> (sym
        -> SymExpr sym 'BaseIntegerType
        -> SymExpr sym 'BaseIntegerType
        -> IO (SymExpr sym 'BaseIntegerType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym 'BaseIntegerType
      -> SymExpr sym 'BaseIntegerType
      -> IO (SymExpr sym 'BaseIntegerType))
     -> Op sym)
    -> (sym
        -> SymExpr sym 'BaseIntegerType
        -> SymExpr sym 'BaseIntegerType
        -> IO (SymExpr sym 'BaseIntegerType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intMul)
      , (Text
    "intadd", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
    -> (sym
        -> SymExpr sym 'BaseIntegerType
        -> SymExpr sym 'BaseIntegerType
        -> IO (SymExpr sym 'BaseIntegerType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym 'BaseIntegerType
      -> SymExpr sym 'BaseIntegerType
      -> IO (SymExpr sym 'BaseIntegerType))
     -> Op sym)
    -> (sym
        -> SymExpr sym 'BaseIntegerType
        -> SymExpr sym 'BaseIntegerType
        -> IO (SymExpr sym 'BaseIntegerType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intAdd)
      , (Text
    "intmod", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
    -> (sym
        -> SymExpr sym 'BaseIntegerType
        -> SymExpr sym 'BaseIntegerType
        -> IO (SymExpr sym 'BaseIntegerType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym 'BaseIntegerType
      -> SymExpr sym 'BaseIntegerType
      -> IO (SymExpr sym 'BaseIntegerType))
     -> Op sym)
    -> (sym
        -> SymExpr sym 'BaseIntegerType
        -> SymExpr sym 'BaseIntegerType
        -> IO (SymExpr sym 'BaseIntegerType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intMod)
      , (Text
    "intdiv", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
    -> (sym
        -> SymExpr sym 'BaseIntegerType
        -> SymExpr sym 'BaseIntegerType
        -> IO (SymExpr sym 'BaseIntegerType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym 'BaseIntegerType
      -> SymExpr sym 'BaseIntegerType
      -> IO (SymExpr sym 'BaseIntegerType))
     -> Op sym)
    -> (sym
        -> SymExpr sym 'BaseIntegerType
        -> SymExpr sym 'BaseIntegerType
        -> IO (SymExpr sym 'BaseIntegerType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intDiv)
      , (Text
    "intle", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
    -> (sym
        -> SymExpr sym 'BaseIntegerType
        -> SymExpr sym 'BaseIntegerType
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym 'BaseIntegerType
      -> SymExpr sym 'BaseIntegerType
      -> IO (SymExpr sym 'BaseBoolType))
     -> Op sym)
    -> (sym
        -> SymExpr sym 'BaseIntegerType
        -> SymExpr sym 'BaseIntegerType
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
    W4.intLe)
      , (Text
    "intabs", Assignment BaseTypeRepr ('EmptyCtx ::> 'BaseIntegerType)
    -> (sym
        -> SymExpr sym 'BaseIntegerType
        -> IO (SymExpr sym 'BaseIntegerType))
    -> Op sym
    forall (res :: BaseType) sym (arg2 :: BaseType).
    Assignment BaseTypeRepr ('EmptyCtx ::> res)
    -> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
    Op1 Assignment BaseTypeRepr ('EmptyCtx ::> 'BaseIntegerType)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym 'BaseIntegerType
      -> IO (SymExpr sym 'BaseIntegerType))
     -> Op sym)
    -> (sym
        -> SymExpr sym 'BaseIntegerType
        -> IO (SymExpr sym 'BaseIntegerType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymInteger sym)
    W4.intAbs)
      -- -- -- Bitvector ops -- -- --
      , (Text
    "bvand", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvAndBits)
      , (Text
    "bvor", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvOrBits)
      , (Text
    "bvadd", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvAdd)
      , (Text
    "bvmul", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvMul)
      , (Text
    "bvudiv", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvUdiv)
      , (Text
    "bvurem", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvUrem)
      , (Text
    "bvshl", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvShl)
      , (Text
    "bvlshr", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvLshr)
      , (Text
    "bvnand", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 ((forall (w :: Nat).
      (1 <= w) =>
      sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
     -> Op sym)
    -> (forall (w :: Nat).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymBV sym w
    arg1 SymBV sym w
    arg2 -> sym -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    W4.bvNotBits sym
    sym (SymBV sym w -> IO (SymBV sym w))
    -> IO (SymBV sym w) -> IO (SymBV sym w)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvAndBits sym
    sym SymBV sym w
    arg1 SymBV sym w
    arg2)
      , (Text
    "bvnor", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 ((forall (w :: Nat).
      (1 <= w) =>
      sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
     -> Op sym)
    -> (forall (w :: Nat).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymBV sym w
    arg1 SymBV sym w
    arg2 -> sym -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    W4.bvNotBits sym
    sym (SymBV sym w -> IO (SymBV sym w))
    -> IO (SymBV sym w) -> IO (SymBV sym w)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvOrBits sym
    sym SymBV sym w
    arg1 SymBV sym w
    arg2)
      , (Text
    "bvxor", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvXorBits)
      , (Text
    "bvxnor", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 ((forall (w :: Nat).
      (1 <= w) =>
      sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
     -> Op sym)
    -> (forall (w :: Nat).
        (1 <= w) =>
        sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymBV sym w
    arg1 SymBV sym w
    arg2 -> sym -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    W4.bvNotBits sym
    sym (SymBV sym w -> IO (SymBV sym w))
    -> IO (SymBV sym w) -> IO (SymBV sym w)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvXorBits sym
    sym SymBV sym w
    arg1 SymBV sym w
    arg2)
      , (Text
    "bvsub", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvSub)
      , (Text
    "bvsdiv", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvSdiv)
      , (Text
    "bvsrem", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvSrem)
      , (Text
    "bvsmod", String -> Op sym
    forall a. HasCallStack => String -> a
    error String
    "bvsmod is not implemented")
      , (Text
    "bvashr", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    W4.bvAshr)
      , (Text
    "bvult", (forall (w :: Nat).
     (1 <= w) =>
     sym
     -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> Op sym
    BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W4.bvUlt)
      , (Text
    "bvule", (forall (w :: Nat).
     (1 <= w) =>
     sym
     -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> Op sym
    BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W4.bvUle)
      , (Text
    "bvugt", (forall (w :: Nat).
     (1 <= w) =>
     sym
     -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> Op sym
    BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W4.bvUgt)
      , (Text
    "bvuge", (forall (w :: Nat).
     (1 <= w) =>
     sym
     -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> Op sym
    BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W4.bvUge)
      , (Text
    "bvslt", (forall (w :: Nat).
     (1 <= w) =>
     sym
     -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> Op sym
    BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W4.bvSlt)
      , (Text
    "bvsle", (forall (w :: Nat).
     (1 <= w) =>
     sym
     -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> Op sym
    BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W4.bvSle)
      , (Text
    "bvsgt", (forall (w :: Nat).
     (1 <= w) =>
     sym
     -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> Op sym
    BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W4.bvSgt)
      , (Text
    "bvsge", (forall (w :: Nat).
     (1 <= w) =>
     sym
     -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> Op sym
    BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W4.bvSge)
      , (Text
    "bveq", (forall (w :: Nat).
     (1 <= w) =>
     sym
     -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> Op sym
    BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W4.bvEq)
      , (Text
    "bvne", (forall (w :: Nat).
     (1 <= w) =>
     sym
     -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
    -> Op sym
    BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    W4.bvNe)
      , (Text
    "bvneg", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp1 sym -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    W4.bvNeg)
      , (Text
    "bvnot", (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    forall sym.
    (forall (w :: Nat).
     (1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w))
    -> Op sym
    BVOp1 sym -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    W4.bvNotBits)
      -- -- -- Floating point ops -- -- --
      , (Text
    "fnegd", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall (res :: BaseType) sym (arg2 :: BaseType).
    Assignment BaseTypeRepr ('EmptyCtx ::> res)
    -> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
    Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    W4.floatNeg @_ @Prec64)
      , (Text
    "fnegs", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall (res :: BaseType) sym (arg2 :: BaseType).
    Assignment BaseTypeRepr ('EmptyCtx ::> res)
    -> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
    Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    W4.floatNeg @_ @Prec32)
      , (Text
    "fabsd", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall (res :: BaseType) sym (arg2 :: BaseType).
    Assignment BaseTypeRepr ('EmptyCtx ::> res)
    -> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
    Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    W4.floatAbs @_ @Prec64)
      , (Text
    "fabss", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall (res :: BaseType) sym (arg2 :: BaseType).
    Assignment BaseTypeRepr ('EmptyCtx ::> res)
    -> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
    Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    W4.floatAbs @_ @Prec32)
      , (Text
    "fsqrt", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec64)
    x -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    W4.floatSqrt @_ @Prec64 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec64)
    x)
      , (Text
    "fsqrts", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec32)
    x -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    W4.floatSqrt @_ @Prec32 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec32)
    x)
      , (Text
    "fnand", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall (res :: BaseType) sym (arg2 :: BaseType).
    Assignment BaseTypeRepr ('EmptyCtx ::> res)
    -> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
    Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym 'BaseBoolType))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (Pred sym)
    W4.floatIsNaN @_ @Prec64)
      , (Text
    "fnans", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall (res :: BaseType) sym (arg2 :: BaseType).
    Assignment BaseTypeRepr ('EmptyCtx ::> res)
    -> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
    Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym 'BaseBoolType))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (Pred sym)
    W4.floatIsNaN @_ @Prec32)
      , (Text
    "frsp", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec64)
    x -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision) (fpp' :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> FloatPrecisionRepr fpp
    -> RoundingMode
    -> SymFloat sym fpp'
    -> IO (SymFloat sym fpp)
    W4.floatCast @_ @Prec32 @Prec64 sym
    sym FloatPrecisionRepr Prec32
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr RoundingMode
    rm SymExpr sym (BaseFloatType Prec64)
    x)
      , (Text
    "fp_single_to_double", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall (res :: BaseType) sym (arg2 :: BaseType).
    Assignment BaseTypeRepr ('EmptyCtx ::> res)
    -> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
    Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym ->
        forall sym (fpp :: FloatPrecision) (fpp' :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> FloatPrecisionRepr fpp
    -> RoundingMode
    -> SymFloat sym fpp'
    -> IO (SymFloat sym fpp)
    W4.floatCast @_ @Prec64 @Prec32 sym
    sym FloatPrecisionRepr Prec64
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr RoundingMode
    W4.RNE)
      , (Text
    "fp_binary_to_double",
         Assignment BaseTypeRepr ('EmptyCtx ::> BaseBVType 64)
    -> (sym
        -> SymExpr sym (BaseBVType 64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall (res :: BaseType) sym (arg2 :: BaseType).
    Assignment BaseTypeRepr ('EmptyCtx ::> res)
    -> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
    Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseBVType 64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 64)
      -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym -> forall sym (eb :: Nat) (sb :: Nat).
    (IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
    sym
    -> FloatPrecisionRepr (FloatingPointPrecision eb sb)
    -> SymBV sym (eb + sb)
    -> IO (SymFloat sym (FloatingPointPrecision eb sb))
    W4.floatFromBinary @_ @11 @53 sym
    sym FloatPrecisionRepr Prec64
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr)
      , (Text
    "fp_binary_to_single",
         Assignment BaseTypeRepr ('EmptyCtx ::> BaseBVType 32)
    -> (sym
        -> SymExpr sym (BaseBVType 32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall (res :: BaseType) sym (arg2 :: BaseType).
    Assignment BaseTypeRepr ('EmptyCtx ::> res)
    -> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
    Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseBVType 32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 32)
      -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym -> forall sym (eb :: Nat) (sb :: Nat).
    (IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
    sym
    -> FloatPrecisionRepr (FloatingPointPrecision eb sb)
    -> SymBV sym (eb + sb)
    -> IO (SymFloat sym (FloatingPointPrecision eb sb))
    W4.floatFromBinary @_ @8 @24 sym
    sym FloatPrecisionRepr Prec32
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr)
      , (Text
    "fp_double_to_binary", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseBVType 64)))
    -> Op sym
    forall (res :: BaseType) sym (arg2 :: BaseType).
    Assignment BaseTypeRepr ('EmptyCtx ::> res)
    -> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
    Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseBVType 64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseBVType 64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (eb :: Nat) (sb :: Nat).
    (IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
    sym
    -> SymFloat sym (FloatingPointPrecision eb sb)
    -> IO (SymBV sym (eb + sb))
    W4.floatToBinary @_ @11 @53)
      , (Text
    "fp_single_to_binary", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseBVType 32)))
    -> Op sym
    forall (res :: BaseType) sym (arg2 :: BaseType).
    Assignment BaseTypeRepr ('EmptyCtx ::> res)
    -> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
    Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym (BaseBVType 32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseBVType 32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (eb :: Nat) (sb :: Nat).
    (IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
    sym
    -> SymFloat sym (FloatingPointPrecision eb sb)
    -> IO (SymBV sym (eb + sb))
    W4.floatToBinary @_ @8 @24)
      , (Text
    "fctid", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseBVType 64)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseBVType 64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseBVType 64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec64)
    x -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseBVType 64)))
    -> IO (SymExpr sym (BaseBVType 64))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseBVType 64)))
     -> IO (SymExpr sym (BaseBVType 64)))
    -> (RoundingMode -> IO (SymExpr sym (BaseBVType 64)))
    -> IO (SymExpr sym (BaseBVType 64))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (w :: Nat) (fpp :: FloatPrecision).
    (IsExprBuilder sym, 1 <= w) =>
    sym
    -> NatRepr w
    -> RoundingMode
    -> SymFloat sym fpp
    -> IO (SymBV sym w)
    W4.floatToSBV @_ @64 @Prec64 sym
    sym NatRepr 64
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr RoundingMode
    rm SymExpr sym (BaseFloatType Prec64)
    x)
      , (Text
    "fctidu", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseBVType 64)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseBVType 64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseBVType 64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec64)
    x -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseBVType 64)))
    -> IO (SymExpr sym (BaseBVType 64))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseBVType 64)))
     -> IO (SymExpr sym (BaseBVType 64)))
    -> (RoundingMode -> IO (SymExpr sym (BaseBVType 64)))
    -> IO (SymExpr sym (BaseBVType 64))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (w :: Nat) (fpp :: FloatPrecision).
    (IsExprBuilder sym, 1 <= w) =>
    sym
    -> NatRepr w
    -> RoundingMode
    -> SymFloat sym fpp
    -> IO (SymBV sym w)
    W4.floatToBV @_ @64 @Prec64 sym
    sym NatRepr 64
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr RoundingMode
    rm SymExpr sym (BaseFloatType Prec64)
    x)
      , (Text
    "fctiw", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseBVType 32)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseBVType 32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseBVType 32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec64)
    x -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseBVType 32)))
    -> IO (SymExpr sym (BaseBVType 32))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseBVType 32)))
     -> IO (SymExpr sym (BaseBVType 32)))
    -> (RoundingMode -> IO (SymExpr sym (BaseBVType 32)))
    -> IO (SymExpr sym (BaseBVType 32))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (w :: Nat) (fpp :: FloatPrecision).
    (IsExprBuilder sym, 1 <= w) =>
    sym
    -> NatRepr w
    -> RoundingMode
    -> SymFloat sym fpp
    -> IO (SymBV sym w)
    W4.floatToSBV @_ @32 @Prec64 sym
    sym NatRepr 32
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr RoundingMode
    rm SymExpr sym (BaseFloatType Prec64)
    x)
      , (Text
    "fctiwu", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseBVType 32)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseBVType 32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseBVType 32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec64)
    x -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseBVType 32)))
    -> IO (SymExpr sym (BaseBVType 32))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseBVType 32)))
     -> IO (SymExpr sym (BaseBVType 32)))
    -> (RoundingMode -> IO (SymExpr sym (BaseBVType 32)))
    -> IO (SymExpr sym (BaseBVType 32))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (w :: Nat) (fpp :: FloatPrecision).
    (IsExprBuilder sym, 1 <= w) =>
    sym
    -> NatRepr w
    -> RoundingMode
    -> SymFloat sym fpp
    -> IO (SymBV sym w)
    W4.floatToBV @_ @32 @Prec64 sym
    sym NatRepr 32
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr RoundingMode
    rm SymExpr sym (BaseFloatType Prec64)
    x)
      , (Text
    "fcfid", Assignment
      BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseBVType 64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseBVType 64)
      -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseBVType 64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseBVType 64)
    x -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (w :: Nat) (fpp :: FloatPrecision).
    (IsExprBuilder sym, 1 <= w) =>
    sym
    -> FloatPrecisionRepr fpp
    -> RoundingMode
    -> SymBV sym w
    -> IO (SymFloat sym fpp)
    W4.sbvToFloat @_ @64 @Prec64 sym
    sym FloatPrecisionRepr Prec64
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr RoundingMode
    rm SymExpr sym (BaseBVType 64)
    x)
      , (Text
    "fcfids", Assignment
      BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseBVType 64)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseBVType 64)
      -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseBVType 64)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseBVType 64)
    x -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (w :: Nat) (fpp :: FloatPrecision).
    (IsExprBuilder sym, 1 <= w) =>
    sym
    -> FloatPrecisionRepr fpp
    -> RoundingMode
    -> SymBV sym w
    -> IO (SymFloat sym fpp)
    W4.sbvToFloat @_ @64 @Prec32 sym
    sym FloatPrecisionRepr Prec32
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr RoundingMode
    rm SymExpr sym (BaseBVType 64)
    x)
      , (Text
    "fcfidu", Assignment
      BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseBVType 64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseBVType 64)
      -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseBVType 64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseBVType 64)
    x -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (w :: Nat) (fpp :: FloatPrecision).
    (IsExprBuilder sym, 1 <= w) =>
    sym
    -> FloatPrecisionRepr fpp
    -> RoundingMode
    -> SymBV sym w
    -> IO (SymFloat sym fpp)
    W4.bvToFloat @_ @64 @Prec64 sym
    sym FloatPrecisionRepr Prec64
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr RoundingMode
    rm SymExpr sym (BaseBVType 64)
    x)
      , (Text
    "fcfidus", Assignment
      BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseBVType 64)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseBVType 64)
      -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseBVType 64)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseBVType 64)
    x -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (w :: Nat) (fpp :: FloatPrecision).
    (IsExprBuilder sym, 1 <= w) =>
    sym
    -> FloatPrecisionRepr fpp
    -> RoundingMode
    -> SymBV sym w
    -> IO (SymFloat sym fpp)
    W4.bvToFloat @_ @64 @Prec32 sym
    sym FloatPrecisionRepr Prec32
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr RoundingMode
    rm SymExpr sym (BaseBVType 64)
    x)
      , (Text
    "frti", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec64)
    x -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    W4.floatRound @_ @Prec64 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec64)
    x)
      , (Text
    "frtis", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec32)
    x -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    W4.floatRound @_ @Prec32 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec32)
    x)
      , (Text
    "fadd", Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
       ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
           (arg4 :: BaseType).
    Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
    -> (sym
        -> SymExpr sym res
        -> SymExpr sym arg2
        -> SymExpr sym arg3
        -> IO (SymExpr sym arg4))
    -> Op sym
    Op3 Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
       ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec64)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec64)
    x SymExpr sym (BaseFloatType Prec64)
    y -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    W4.floatAdd @_ @Prec64 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec64)
    x SymExpr sym (BaseFloatType Prec64)
    y)
      , (Text
    "fadds", Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
       ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
           (arg4 :: BaseType).
    Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
    -> (sym
        -> SymExpr sym res
        -> SymExpr sym arg2
        -> SymExpr sym arg3
        -> IO (SymExpr sym arg4))
    -> Op sym
    Op3 Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
       ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec32)
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec32)
    x SymExpr sym (BaseFloatType Prec32)
    y -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    W4.floatAdd @_ @Prec32 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec32)
    x SymExpr sym (BaseFloatType Prec32)
    y)
      , (Text
    "fsub", Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
       ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
           (arg4 :: BaseType).
    Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
    -> (sym
        -> SymExpr sym res
        -> SymExpr sym arg2
        -> SymExpr sym arg3
        -> IO (SymExpr sym arg4))
    -> Op sym
    Op3 Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
       ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec64)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec64)
    x SymExpr sym (BaseFloatType Prec64)
    y -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    W4.floatSub @_ @Prec64 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec64)
    x SymExpr sym (BaseFloatType Prec64)
    y)
      , (Text
    "fsubs", Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
       ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
           (arg4 :: BaseType).
    Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
    -> (sym
        -> SymExpr sym res
        -> SymExpr sym arg2
        -> SymExpr sym arg3
        -> IO (SymExpr sym arg4))
    -> Op sym
    Op3 Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
       ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec32)
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec32)
    x SymExpr sym (BaseFloatType Prec32)
    y -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    W4.floatSub @_ @Prec32 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec32)
    x SymExpr sym (BaseFloatType Prec32)
    y)
      , (Text
    "fmul", Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
       ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
           (arg4 :: BaseType).
    Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
    -> (sym
        -> SymExpr sym res
        -> SymExpr sym arg2
        -> SymExpr sym arg3
        -> IO (SymExpr sym arg4))
    -> Op sym
    Op3 Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
       ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec64)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec64)
    x SymExpr sym (BaseFloatType Prec64)
    y -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    W4.floatMul @_ @Prec64 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec64)
    x SymExpr sym (BaseFloatType Prec64)
    y)
      , (Text
    "fmuls", Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
       ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
           (arg4 :: BaseType).
    Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
    -> (sym
        -> SymExpr sym res
        -> SymExpr sym arg2
        -> SymExpr sym arg3
        -> IO (SymExpr sym arg4))
    -> Op sym
    Op3 Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
       ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec32)
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec32)
    x SymExpr sym (BaseFloatType Prec32)
    y -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    W4.floatMul @_ @Prec32 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec32)
    x SymExpr sym (BaseFloatType Prec32)
    y)
      , (Text
    "fdiv", Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
       ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
           (arg4 :: BaseType).
    Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
    -> (sym
        -> SymExpr sym res
        -> SymExpr sym arg2
        -> SymExpr sym arg3
        -> IO (SymExpr sym arg4))
    -> Op sym
    Op3 Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
       ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec64)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec64)
    x SymExpr sym (BaseFloatType Prec64)
    y -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    W4.floatDiv @_ @Prec64 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec64)
    x SymExpr sym (BaseFloatType Prec64)
    y)
      , (Text
    "fdivs", Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
       ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
           (arg4 :: BaseType).
    Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
    -> (sym
        -> SymExpr sym res
        -> SymExpr sym arg2
        -> SymExpr sym arg3
        -> IO (SymExpr sym arg4))
    -> Op sym
    Op3 Assignment
      BaseTypeRepr
      ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
       ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec32)
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec32)
    x SymExpr sym (BaseFloatType Prec32)
    y -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    W4.floatDiv @_ @Prec32 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec32)
    x SymExpr sym (BaseFloatType Prec32)
    y)
      , (Text
    "fltd", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseFloatType Prec64) ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseFloatType Prec64) ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec64)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym 'BaseBoolType))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
    W4.floatLt @_ @Prec64)
      , (Text
    "flts", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseFloatType Prec32) ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseFloatType Prec32) ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec32)
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym 'BaseBoolType))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
    W4.floatLt @_ @Prec32)
      , (Text
    "feqd", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseFloatType Prec64) ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseFloatType Prec64) ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec64)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym 'BaseBoolType))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
    W4.floatFpEq @_ @Prec64)
      , (Text
    "feqs", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseFloatType Prec32) ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseFloatType Prec32) ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec32)
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym 'BaseBoolType))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
    W4.floatFpEq @_ @Prec32)
      , (Text
    "fled", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseFloatType Prec64) ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseFloatType Prec64) ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec64)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym 'BaseBoolType))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
    W4.floatLe @_ @Prec64)
      , (Text
    "fles", Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseFloatType Prec32) ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
    Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
    -> (sym
        -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
    -> Op sym
    Op2 Assignment
      BaseTypeRepr
      (('EmptyCtx ::> BaseFloatType Prec32) ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseFloatType Prec32)
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym 'BaseBoolType))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym 'BaseBoolType))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
    W4.floatLe @_ @Prec32)
      , (Text
    "ffma", Assignment
      BaseTypeRepr
      (((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
        ::> BaseFloatType Prec64)
       ::> BaseFloatType Prec64)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType)
           (arg4 :: BaseType) sym (ret :: BaseType).
    Assignment
      BaseTypeRepr (((('EmptyCtx ::> res) ::> arg2) ::> arg3) ::> arg4)
    -> (sym
        -> SymExpr sym res
        -> SymExpr sym arg2
        -> SymExpr sym arg3
        -> SymExpr sym arg4
        -> IO (SymExpr sym ret))
    -> Op sym
    Op4 Assignment
      BaseTypeRepr
      (((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
        ::> BaseFloatType Prec64)
       ::> BaseFloatType Prec64)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec64)
      -> SymExpr sym (BaseFloatType Prec64)
      -> SymExpr sym (BaseFloatType Prec64)
      -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> SymExpr sym (BaseFloatType Prec64)
        -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec64)
    x SymExpr sym (BaseFloatType Prec64)
    y SymExpr sym (BaseFloatType Prec64)
    z -> sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
     -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
    -> IO (SymExpr sym (BaseFloatType Prec64))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm ->
        forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    W4.floatFMA @_ @Prec64 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec64)
    x SymExpr sym (BaseFloatType Prec64)
    y SymExpr sym (BaseFloatType Prec64)
    z)
      , (Text
    "ffmas", Assignment
      BaseTypeRepr
      (((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
        ::> BaseFloatType Prec32)
       ::> BaseFloatType Prec32)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType)
           (arg4 :: BaseType) sym (ret :: BaseType).
    Assignment
      BaseTypeRepr (((('EmptyCtx ::> res) ::> arg2) ::> arg3) ::> arg4)
    -> (sym
        -> SymExpr sym res
        -> SymExpr sym arg2
        -> SymExpr sym arg3
        -> SymExpr sym arg4
        -> IO (SymExpr sym ret))
    -> Op sym
    Op4 Assignment
      BaseTypeRepr
      (((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
        ::> BaseFloatType Prec32)
       ::> BaseFloatType Prec32)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr ((sym
      -> SymExpr sym (BaseBVType 2)
      -> SymExpr sym (BaseFloatType Prec32)
      -> SymExpr sym (BaseFloatType Prec32)
      -> SymExpr sym (BaseFloatType Prec32)
      -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> Op sym)
    -> (sym
        -> SymExpr sym (BaseBVType 2)
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> SymExpr sym (BaseFloatType Prec32)
        -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> Op sym
    forall a b. (a -> b) -> a -> b
    $ \sym
    sym SymExpr sym (BaseBVType 2)
    r SymExpr sym (BaseFloatType Prec32)
    x SymExpr sym (BaseFloatType Prec32)
    y SymExpr sym (BaseFloatType Prec32)
    z ->
        sym
    -> SymExpr sym (BaseBVType 2)
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymBV sym 2
    -> (RoundingMode -> IO (SymExpr sym tp))
    -> IO (SymExpr sym tp)
    U.withRounding sym
    sym SymExpr sym (BaseBVType 2)
    r ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
     -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
    -> IO (SymExpr sym (BaseFloatType Prec32))
    forall a b. (a -> b) -> a -> b
    $ \RoundingMode
    rm -> forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    W4.floatFMA @_ @Prec32 sym
    sym RoundingMode
    rm SymExpr sym (BaseFloatType Prec32)
    x SymExpr sym (BaseFloatType Prec32)
    y SymExpr sym (BaseFloatType Prec32)
    z)
      ]

    -- | Verify a list of arguments has a single argument and
    -- return it, else raise an error.
    readOneArg ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => [SExpr]
      -> Processor sym (Some (W4.SymExpr sym))
    readOneArg :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym (Some (SymExpr sym))
    readOneArg [SExpr]
    operands = do
      args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym [Some (SymExpr sym)]
    readExprs [SExpr]
    operands
      case args of
        [Some (Expr t)
    arg] -> Some (Expr t)
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Some (Expr t)
    arg
        [Some (Expr t)]
    _ -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> String
    forall r. PrintfType r => String -> r
    printf String
    "expecting 1 argument, got %d" ([Some (Expr t)] -> Int
    forall a. [a] -> Int
    forall (t :: Type -> Type) a. Foldable t => t a -> Int
    length [Some (Expr t)]
    args)

    -- | Verify a list of arguments has two arguments and return
    -- it, else raise an error.
    readTwoArgs ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => [SExpr]
      -> Processor sym (Some (W4.SymExpr sym), Some (W4.SymExpr sym))
    readTwoArgs :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
    readTwoArgs [SExpr]
    operands = do
      args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym [Some (SymExpr sym)]
    readExprs [SExpr]
    operands
      case args of
        [Some (Expr t)
    arg1, Some (Expr t)
    arg2] -> (Some (Expr t), Some (Expr t))
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Some (Expr t), Some (Expr t))
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Some (Expr t)
    arg1, Some (Expr t)
    arg2)
        [Some (Expr t)]
    _ -> String
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Some (Expr t), Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT
          String
          (ReaderT (ProcessorEnv sym) IO)
          (Some (Expr t), Some (Expr t)))
    -> String
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Some (Expr t), Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> String
    forall r. PrintfType r => String -> r
    printf String
    "expecting 2 arguments, got %d" ([Some (Expr t)] -> Int
    forall a. [a] -> Int
    forall (t :: Type -> Type) a. Foldable t => t a -> Int
    length [Some (Expr t)]
    args)

    -- | Verify a list of arguments has three arguments and
    -- return it, else raise an error.
    readThreeArgs ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => [SExpr]
      -> Processor sym (Some (W4.SymExpr sym), Some (W4.SymExpr sym), Some (W4.SymExpr sym))
    readThreeArgs :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr]
    -> Processor
         sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
    readThreeArgs [SExpr]
    operands = do
      args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym [Some (SymExpr sym)]
    readExprs [SExpr]
    operands
      case args of
        [Some (Expr t)
    arg1, Some (Expr t)
    arg2, Some (Expr t)
    arg3] -> (Some (Expr t), Some (Expr t), Some (Expr t))
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Some (Expr t), Some (Expr t), Some (Expr t))
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Some (Expr t)
    arg1, Some (Expr t)
    arg2, Some (Expr t)
    arg3)
        [Some (Expr t)]
    _ -> String
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Some (Expr t), Some (Expr t), Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT
          String
          (ReaderT (ProcessorEnv sym) IO)
          (Some (Expr t), Some (Expr t), Some (Expr t)))
    -> String
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Some (Expr t), Some (Expr t), Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> String
    forall r. PrintfType r => String -> r
    printf String
    "expecting 3 arguments, got %d" ([Some (Expr t)] -> Int
    forall a. [a] -> Int
    forall (t :: Type -> Type) a. Foldable t => t a -> Int
    length [Some (Expr t)]
    args)

    -- | Reads an "application" form, i.e. @(operator operands ...)@.
    readApp ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => SExpr
      -> [SExpr]
      -> Processor sym (Some (W4.SymExpr sym))
    readApp :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> [SExpr] -> Processor sym (Some (SymExpr sym))
    readApp (S.WFSAtom (AId Text
    "call")) (S.WFSAtom (AId Text
    fnName):[SExpr]
    operands) = do
      sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.asks ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
    forall sym. ProcessorEnv sym -> sym
    procSym
      maybeFn <- lookupFn fnName
      case maybeFn of
        Just (SomeSymFn SymFn sym dom ret
    fn) -> do
          args <- (SExpr
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> [SExpr]
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Some (Expr t)]
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> [a] -> m [b]
    mapM SExpr
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    SExpr
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> Processor sym (Some (SymExpr sym))
    readExpr [SExpr]
    operands
          assn <- exprAssignment (W4.fnArgTypes fn) args
          liftIO (Some <$> W4.applySymFn sym fn assn)
        Maybe (SomeSymFn sym)
    Nothing -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ String
    "The function name `"
                   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++(Text -> String
    T.unpack Text
    fnName)
                   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++String
    "` is not bound to a SymFn in the current Config."
    readApp opRaw :: SExpr
    opRaw@(S.WFSAtom (AId Text
    "call")) [SExpr]
    operands = String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError
      (String
     -> ExceptT
          String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
    -> String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall a b. (a -> b) -> a -> b
    $ String
    "Unrecognized use of `call`: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Text -> String
    T.unpack (Seq String -> SExpr -> Text
    printSExpr Seq String
    forall a. Monoid a => a
    mempty ([SExpr] -> SExpr
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L (SExpr
    opRawSExpr -> [SExpr] -> [SExpr]
    forall a. a -> [a] -> [a]
    :[SExpr]
    operands))))
    readApp opRaw :: SExpr
    opRaw@(S.WFSAtom (AId Text
    operator)) [SExpr]
    operands = do
      sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
    forall a.
    (ProcessorEnv (ExprBuilder t st fs) -> a)
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
    forall sym. ProcessorEnv sym -> sym
    procSym
      prefixError ("in reading expression:\n"
                   ++(T.unpack $ printSExpr mempty $ S.WFSList (opRaw:operands))++"\n") $
      -- Parse an expression of the form @(fnname operands ...)@
        case lookupOp @sym operator of
          Just (FloatOp1 forall (fpp :: FloatPrecision).
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    fn) -> do
            args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym [Some (SymExpr sym)]
    readExprs [SExpr]
    operands
            case args of
              [Some Expr t x
    a1]
                | BaseFloatRepr FloatPrecisionRepr fpp
    _ <- Expr t x -> BaseTypeRepr x
    forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W4.exprType Expr t x
    a1 -> IO (Some (Expr t))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (Expr t ('BaseFloatType fpp) -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Expr t ('BaseFloatType fpp) -> Some (Expr t))
    -> IO (Expr t ('BaseFloatType fpp)) -> IO (Some (Expr t))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    fn sym
    ExprBuilder t st fs
    sym SymFloat sym fpp
    Expr t x
    a1)
              [Some (Expr t)]
    _ -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError String
    "Unable to unpack FloatOp1 arg in Formula.Parser readApp"
          Just (Op1 Assignment BaseTypeRepr ('EmptyCtx ::> arg1)
    arg_types sym -> SymExpr sym arg1 -> IO (SymExpr sym ret)
    fn) -> do
            args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym [Some (SymExpr sym)]
    readExprs [SExpr]
    operands
            exprAssignment arg_types args >>= \case
              Assignment (Expr t) ctx
    Ctx.Empty Ctx.:> Expr t tp
    arg1 ->
                IO (Some (Expr t))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (Expr t ret -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Expr t ret -> Some (Expr t))
    -> IO (Expr t ret) -> IO (Some (Expr t))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymExpr sym arg1 -> IO (SymExpr sym ret)
    fn sym
    ExprBuilder t st fs
    sym SymExpr sym arg1
    Expr t tp
    arg1)
          Just (Op2 Assignment BaseTypeRepr (('EmptyCtx ::> arg1) ::> arg2)
    arg_types sym -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret)
    fn) -> do
            args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym [Some (SymExpr sym)]
    readExprs [SExpr]
    operands
            exprAssignment arg_types args >>= \case
              Assignment (Expr t) ctx
    Ctx.Empty Ctx.:> Expr t tp
    arg1 Ctx.:> Expr t tp
    arg2 ->
                  IO (Some (Expr t))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (Expr t ret -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Expr t ret -> Some (Expr t))
    -> IO (Expr t ret) -> IO (Some (Expr t))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret)
    fn sym
    ExprBuilder t st fs
    sym SymExpr sym arg1
    Expr t tp
    arg1 SymExpr sym arg2
    Expr t tp
    arg2)
          Just (Op3 Assignment BaseTypeRepr ((('EmptyCtx ::> arg1) ::> arg2) ::> arg3)
    arg_types sym
    -> SymExpr sym arg1
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> IO (SymExpr sym ret)
    fn) -> do
            args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym [Some (SymExpr sym)]
    readExprs [SExpr]
    operands
            exprAssignment arg_types args >>= \case
              Assignment (Expr t) ctx
    Ctx.Empty Ctx.:> Expr t tp
    arg1 Ctx.:> Expr t tp
    arg2 Ctx.:> Expr t tp
    arg3 ->
                  IO (Some (Expr t))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (Expr t ret -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Expr t ret -> Some (Expr t))
    -> IO (Expr t ret) -> IO (Some (Expr t))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> SymExpr sym arg1
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> IO (SymExpr sym ret)
    fn sym
    ExprBuilder t st fs
    sym SymExpr sym arg1
    Expr t tp
    arg1 SymExpr sym arg2
    Expr t tp
    arg2 SymExpr sym arg3
    Expr t tp
    arg3)
          Just (Op4 Assignment
      BaseTypeRepr (((('EmptyCtx ::> arg1) ::> arg2) ::> arg3) ::> arg4)
    arg_types sym
    -> SymExpr sym arg1
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> SymExpr sym arg4
    -> IO (SymExpr sym ret)
    fn) -> do
            args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym [Some (SymExpr sym)]
    readExprs [SExpr]
    operands
            exprAssignment arg_types args >>= \case
              Assignment (Expr t) ctx
    Ctx.Empty Ctx.:> Expr t tp
    arg1 Ctx.:> Expr t tp
    arg2 Ctx.:> Expr t tp
    arg3 Ctx.:> Expr t tp
    arg4 ->
                  IO (Some (Expr t))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (Expr t ret -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Expr t ret -> Some (Expr t))
    -> IO (Expr t ret) -> IO (Some (Expr t))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> SymExpr sym arg1
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> SymExpr sym arg4
    -> IO (SymExpr sym ret)
    fn sym
    ExprBuilder t st fs
    sym SymExpr sym arg1
    Expr t tp
    arg1 SymExpr sym arg2
    Expr t tp
    arg2 SymExpr sym arg3
    Expr t tp
    arg3 SymExpr sym arg4
    Expr t tp
    arg4)
          Just (BVOp1 forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    op) -> do
            Some expr <- [SExpr]
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym (Some (SymExpr sym))
    readOneArg [SExpr]
    operands
            BVProof _ <- getBVProof expr
            liftIO $ Some <$> op sym expr
          Just (BVOp2 forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    op) -> do
            (Some arg1, Some arg2)  <- [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
    readTwoArgs [SExpr]
    operands
            BVProof m <- prefixError "in arg 1: " $ getBVProof arg1
            BVProof n <- prefixError "in arg 2: " $ getBVProof arg2
            case testEquality m n of
              Just n :~: n
    Refl -> IO (Some (Expr t))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (Expr t ('BaseBVType n) -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Expr t ('BaseBVType n) -> Some (Expr t))
    -> IO (Expr t ('BaseBVType n)) -> IO (Some (Expr t))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym n -> SymBV sym n -> IO (SymBV sym n)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    op sym
    ExprBuilder t st fs
    sym SymBV sym n
    Expr t x
    arg1 SymBV sym n
    Expr t x
    arg2)
              Maybe (n :~: n)
    Nothing -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ String -> Text -> String -> String -> String
    forall r. PrintfType r => String -> r
    printf String
    "arguments to %s must be the same length, \
                                             \but arg 1 has length %s \
                                             \and arg 2 has length %s"
                                             Text
    operator
                                             (NatRepr n -> String
    forall a. Show a => a -> String
    show NatRepr n
    m)
                                             (NatRepr n -> String
    forall a. Show a => a -> String
    show NatRepr n
    n)
          Just (BVComp2 forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    op) -> do
            (Some arg1, Some arg2)  <- [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
    readTwoArgs [SExpr]
    operands
            BVProof m <- prefixError "in arg 1: " $ getBVProof arg1
            BVProof n <- prefixError "in arg 2: " $ getBVProof arg2
            case testEquality m n of
              Just n :~: n
    Refl -> IO (Some (Expr t))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (Expr t 'BaseBoolType -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Expr t 'BaseBoolType -> Some (Expr t))
    -> IO (Expr t 'BaseBoolType) -> IO (Some (Expr t))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym n -> SymBV sym n -> IO (Pred sym)
    forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    op sym
    ExprBuilder t st fs
    sym SymBV sym n
    Expr t x
    arg1 SymBV sym n
    Expr t x
    arg2)
              Maybe (n :~: n)
    Nothing -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ String -> Text -> String -> String -> String
    forall r. PrintfType r => String -> r
    printf String
    "arguments to %s must be the same length, \
                                             \but arg 1 has length %s \
                                             \and arg 2 has length %s"
                                             Text
    operator
                                             (NatRepr n -> String
    forall a. Show a => a -> String
    show NatRepr n
    m)
                                             (NatRepr n -> String
    forall a. Show a => a -> String
    show NatRepr n
    n)
          Maybe (Op sym)
    Nothing ->
            -- Operators/syntactic-forms with types too
            -- complicated to nicely fit in the Op type
            case Text
    operator of
              Text
    "concat" -> do
                (Some arg1, Some arg2)  <- [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
    readTwoArgs [SExpr]
    operands
                BVProof _ <- prefixError "in arg 1: " $ getBVProof arg1
                BVProof _ <- prefixError "in arg 2: " $ getBVProof arg2
                liftIO (Some <$> W4.bvConcat sym arg1 arg2)
              Text
    "=" -> do
                (Some arg1, Some arg2)  <- [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
    readTwoArgs [SExpr]
    operands
                case testEquality (W4.exprType arg1) (W4.exprType arg2) of
                  Just x :~: x
    Refl -> IO (Some (Expr t))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (Expr t 'BaseBoolType -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Expr t 'BaseBoolType -> Some (Expr t))
    -> IO (Expr t 'BaseBoolType) -> IO (Some (Expr t))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ExprBuilder t st fs
    -> SymExpr (ExprBuilder t st fs) x
    -> SymExpr (ExprBuilder t st fs) x
    -> IO (Pred (ExprBuilder t st fs))
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
    forall (tp :: BaseType).
    ExprBuilder t st fs
    -> SymExpr (ExprBuilder t st fs) tp
    -> SymExpr (ExprBuilder t st fs) tp
    -> IO (Pred (ExprBuilder t st fs))
    W4.isEq ExprBuilder t st fs
    sym SymExpr (ExprBuilder t st fs) x
    Expr t x
    arg1 SymExpr (ExprBuilder t st fs) x
    Expr t x
    arg2)
                  Maybe (x :~: x)
    Nothing -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $
                    String -> String -> String -> String
    forall r. PrintfType r => String -> r
    printf String
    "arguments must have same types, \
                           \but arg 1 has type %s \
                           \and arg 2 has type %s"
                    (BaseTypeRepr x -> String
    forall a. Show a => a -> String
    show (Expr t x -> BaseTypeRepr x
    forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W4.exprType Expr t x
    arg1))
                    (BaseTypeRepr x -> String
    forall a. Show a => a -> String
    show (Expr t x -> BaseTypeRepr x
    forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W4.exprType Expr t x
    arg2))
              Text
    "ite" -> do
                (Some test, Some then_, Some else_)  <- [SExpr]
    -> Processor
         sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr]
    -> Processor
         sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
    readThreeArgs [SExpr]
    operands
                case W4.exprType test of
                  BaseTypeRepr x
    BaseBoolRepr ->
                    case BaseTypeRepr x -> BaseTypeRepr x -> Maybe (x :~: x)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: BaseType) (b :: BaseType).
    BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
    testEquality (Expr t x -> BaseTypeRepr x
    forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W4.exprType Expr t x
    then_) (Expr t x -> BaseTypeRepr x
    forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W4.exprType Expr t x
    else_) of
                      Just x :~: x
    Refl -> IO (Some (Expr t))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (Expr t x -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Expr t x -> Some (Expr t)) -> IO (Expr t x) -> IO (Some (Expr t))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ExprBuilder t st fs
    -> Pred (ExprBuilder t st fs)
    -> SymExpr (ExprBuilder t st fs) x
    -> SymExpr (ExprBuilder t st fs) x
    -> IO (SymExpr (ExprBuilder t st fs) x)
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym
    -> Pred sym
    -> SymExpr sym tp
    -> SymExpr sym tp
    -> IO (SymExpr sym tp)
    forall (tp :: BaseType).
    ExprBuilder t st fs
    -> Pred (ExprBuilder t st fs)
    -> SymExpr (ExprBuilder t st fs) tp
    -> SymExpr (ExprBuilder t st fs) tp
    -> IO (SymExpr (ExprBuilder t st fs) tp)
    W4.baseTypeIte ExprBuilder t st fs
    sym Pred (ExprBuilder t st fs)
    Expr t x
    test SymExpr (ExprBuilder t st fs) x
    Expr t x
    then_ SymExpr (ExprBuilder t st fs) x
    Expr t x
    else_)
                      Maybe (x :~: x)
    Nothing -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $
                        String -> String -> String -> String
    forall r. PrintfType r => String -> r
    printf String
    "then and else branches must have same type, \
                               \but then has type %s \
                               \and else has type %s"
                        (BaseTypeRepr x -> String
    forall a. Show a => a -> String
    show (Expr t x -> BaseTypeRepr x
    forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W4.exprType Expr t x
    then_))
                        (BaseTypeRepr x -> String
    forall a. Show a => a -> String
    show (Expr t x -> BaseTypeRepr x
    forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W4.exprType Expr t x
    else_))
                  BaseTypeRepr x
    tp -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ String -> String -> String
    forall r. PrintfType r => String -> r
    printf String
    "test expression must be a boolean; got %s" (BaseTypeRepr x -> String
    forall a. Show a => a -> String
    show BaseTypeRepr x
    tp)
              Text
    "select" -> do
                (Some arr, Some idx)  <- [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
    readTwoArgs [SExpr]
    operands
                ArraySingleDim _ <- expectArrayWithIndex (W4.exprType idx) (W4.exprType arr)
                let idx' = Assignment (Expr t) 'EmptyCtx
    forall {k} (f :: k -> Type). Assignment f EmptyCtx
    Ctx.empty Assignment (Expr t) 'EmptyCtx
    -> Expr t x -> Assignment (Expr t) (SingleCtx x)
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    Ctx.:> Expr t x
    idx
                liftIO (Some <$> W4.arrayLookup sym arr idx')
              Text
    "store" -> do
                (Some arr, Some idx, Some expr)  <- [SExpr]
    -> Processor
         sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr]
    -> Processor
         sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
    readThreeArgs [SExpr]
    operands
                ArraySingleDim resRepr <- expectArrayWithIndex (W4.exprType idx) (W4.exprType arr)
                case testEquality resRepr (W4.exprType expr) of
                  Just res :~: x
    Refl ->
                    let idx' :: Assignment (Expr t) (SingleCtx x)
    idx' = Assignment (Expr t) 'EmptyCtx
    forall {k} (f :: k -> Type). Assignment f EmptyCtx
    Ctx.empty Assignment (Expr t) 'EmptyCtx
    -> Expr t x -> Assignment (Expr t) (SingleCtx x)
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    Ctx.:> Expr t x
    idx
                    in IO (Some (Expr t))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (Expr t (BaseArrayType (SingleCtx x) x) -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Expr t (BaseArrayType (SingleCtx x) x) -> Some (Expr t))
    -> IO (Expr t (BaseArrayType (SingleCtx x) x))
    -> IO (Some (Expr t))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ExprBuilder t st fs
    -> SymArray (ExprBuilder t st fs) (SingleCtx x) x
    -> Assignment (SymExpr (ExprBuilder t st fs)) (SingleCtx x)
    -> SymExpr (ExprBuilder t st fs) x
    -> IO (SymArray (ExprBuilder t st fs) (SingleCtx x) x)
    forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymArray sym (idx ::> tp) b
    -> Assignment (SymExpr sym) (idx ::> tp)
    -> SymExpr sym b
    -> IO (SymArray sym (idx ::> tp) b)
    forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
    ExprBuilder t st fs
    -> SymArray (ExprBuilder t st fs) (idx ::> tp) b
    -> Assignment (SymExpr (ExprBuilder t st fs)) (idx ::> tp)
    -> SymExpr (ExprBuilder t st fs) b
    -> IO (SymArray (ExprBuilder t st fs) (idx ::> tp) b)
    W4.arrayUpdate ExprBuilder t st fs
    sym SymArray (ExprBuilder t st fs) (SingleCtx x) x
    Expr t x
    arr Assignment (SymExpr (ExprBuilder t st fs)) (SingleCtx x)
    Assignment (Expr t) (SingleCtx x)
    idx' SymExpr (ExprBuilder t st fs) x
    Expr t x
    expr)
                  Maybe (res :~: x)
    Nothing -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ String -> String -> String -> String
    forall r. PrintfType r => String -> r
    printf String
    "Array result type %s does not match %s"
                             (BaseTypeRepr res -> String
    forall a. Show a => a -> String
    show BaseTypeRepr res
    resRepr)
                             (BaseTypeRepr x -> String
    forall a. Show a => a -> String
    show (Expr t x -> BaseTypeRepr x
    forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W4.exprType Expr t x
    expr))
              Text
    "updateArray" -> do
                (Some arr, Some idx, Some expr)  <- [SExpr]
    -> Processor
         sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr]
    -> Processor
         sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
    readThreeArgs [SExpr]
    operands
                ArraySingleDim resRepr <- expectArrayWithIndex (W4.exprType idx) (W4.exprType arr)
                case testEquality resRepr (W4.exprType expr) of
                  Just res :~: x
    Refl ->
                    let idx' :: Assignment (Expr t) (SingleCtx x)
    idx' = Assignment (Expr t) 'EmptyCtx
    forall {k} (f :: k -> Type). Assignment f EmptyCtx
    Ctx.empty Assignment (Expr t) 'EmptyCtx
    -> Expr t x -> Assignment (Expr t) (SingleCtx x)
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    Ctx.:> Expr t x
    idx
                    in IO (Some (Expr t))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (Expr t (BaseArrayType (SingleCtx x) x) -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Expr t (BaseArrayType (SingleCtx x) x) -> Some (Expr t))
    -> IO (Expr t (BaseArrayType (SingleCtx x) x))
    -> IO (Some (Expr t))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ExprBuilder t st fs
    -> SymArray (ExprBuilder t st fs) (SingleCtx x) x
    -> Assignment (SymExpr (ExprBuilder t st fs)) (SingleCtx x)
    -> SymExpr (ExprBuilder t st fs) x
    -> IO (SymArray (ExprBuilder t st fs) (SingleCtx x) x)
    forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
    IsExprBuilder sym =>
    sym
    -> SymArray sym (idx ::> tp) b
    -> Assignment (SymExpr sym) (idx ::> tp)
    -> SymExpr sym b
    -> IO (SymArray sym (idx ::> tp) b)
    forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
    ExprBuilder t st fs
    -> SymArray (ExprBuilder t st fs) (idx ::> tp) b
    -> Assignment (SymExpr (ExprBuilder t st fs)) (idx ::> tp)
    -> SymExpr (ExprBuilder t st fs) b
    -> IO (SymArray (ExprBuilder t st fs) (idx ::> tp) b)
    W4.arrayUpdate ExprBuilder t st fs
    sym SymArray (ExprBuilder t st fs) (SingleCtx x) x
    Expr t x
    arr Assignment (SymExpr (ExprBuilder t st fs)) (SingleCtx x)
    Assignment (Expr t) (SingleCtx x)
    idx' SymExpr (ExprBuilder t st fs) x
    Expr t x
    expr)
                  Maybe (res :~: x)
    Nothing -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ String -> String -> String -> String
    forall r. PrintfType r => String -> r
    printf String
    "Array result type %s does not match %s"
                             (BaseTypeRepr res -> String
    forall a. Show a => a -> String
    show BaseTypeRepr res
    resRepr)
                             (BaseTypeRepr x -> String
    forall a. Show a => a -> String
    show (Expr t x -> BaseTypeRepr x
    forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W4.exprType Expr t x
    expr))

              Text
    "arrayMap" ->
                -- arrayMap(idxs, array)

                -- The list of indexes is a list of pairs where each pair is:
                --
                -- > (indexList, expr)

                -- Each list of indexes is a list of 'IndexLit' (since we have multi-dimensional indexing)
                case [SExpr]
    operands of
                  [SExpr
    updateSExprList, SExpr
    arrSExpr] -> do
                    Some arrExpr <- SExpr
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> Processor sym (Some (SymExpr sym))
    readExpr SExpr
    arrSExpr
                    case W4.exprType arrExpr of
                      BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
    idxReprs BaseTypeRepr xs
    arrTyRepr -> do
                        updateMap <- Assignment BaseTypeRepr (idx ::> tp)
    -> BaseTypeRepr xs
    -> SExpr
    -> Processor sym (ArrayUpdateMap (SymExpr sym) (idx ::> tp) xs)
    forall sym t (st :: Type -> Type) fs (tp :: BaseType)
           (i :: Ctx BaseType) (itp :: BaseType).
    (sym ~ ExprBuilder t st fs) =>
    Assignment BaseTypeRepr (i ::> itp)
    -> BaseTypeRepr tp
    -> SExpr
    -> Processor sym (ArrayUpdateMap (SymExpr sym) (i ::> itp) tp)
    expectArrayUpdateMap Assignment BaseTypeRepr (idx ::> tp)
    idxReprs BaseTypeRepr xs
    arrTyRepr SExpr
    updateSExprList
                        liftIO (Some <$> W4.sbMakeExpr sym (W4.ArrayMap idxReprs arrTyRepr updateMap arrExpr))
                      BaseTypeRepr x
    repr -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [String
    "expected an array type for the value in 'arrayMap', but got", BaseTypeRepr x -> String
    forall a. Show a => a -> String
    show BaseTypeRepr x
    repr]
                  [SExpr]
    _ -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [String
    "expected a list of indices and an array expression, but got", [SExpr] -> String
    forall a. Show a => a -> String
    show [SExpr]
    operands]

              Text
    "field" -> do
                case [SExpr]
    operands of
                  [SExpr
    rawStruct, S.WFSAtom (AInt Integer
    rawIdx)] -> do
                    Some struct  <- SExpr
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> Processor sym (Some (SymExpr sym))
    readExpr SExpr
    rawStruct
                    case W4.exprType struct of
                      (BaseStructRepr Assignment BaseTypeRepr ctx
    fldTpReprs) ->
                        case Int -> Size ctx -> Maybe (Some (Index ctx))
    forall {k} (ctx :: Ctx k).
    Int -> Size ctx -> Maybe (Some (Index ctx))
    Ctx.intIndex (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    rawIdx) (Assignment BaseTypeRepr ctx -> Size ctx
    forall {k} (f :: k -> Type) (ctx :: Ctx k).
    Assignment f ctx -> Size ctx
    Ctx.size Assignment BaseTypeRepr ctx
    fldTpReprs) of
                          Just (Some Index ctx x
    i) -> IO (Some (Expr t))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (Expr t x -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Expr t x -> Some (Expr t)) -> IO (Expr t x) -> IO (Some (Expr t))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ExprBuilder t st fs
    -> SymStruct (ExprBuilder t st fs) ctx
    -> Index ctx x
    -> IO (SymExpr (ExprBuilder t st fs) x)
    forall sym (flds :: Ctx BaseType) (tp :: BaseType).
    IsExprBuilder sym =>
    sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
    forall (flds :: Ctx BaseType) (tp :: BaseType).
    ExprBuilder t st fs
    -> SymStruct (ExprBuilder t st fs) flds
    -> Index flds tp
    -> IO (SymExpr (ExprBuilder t st fs) tp)
    W4.structField ExprBuilder t st fs
    sym SymStruct (ExprBuilder t st fs) ctx
    Expr t x
    struct Index ctx x
    i)
                          Maybe (Some (Index ctx))
    Nothing -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $
                            [String] -> String
    unwords [String
    "invalid struct index, got", Assignment BaseTypeRepr ctx -> String
    forall a. Show a => a -> String
    show Assignment BaseTypeRepr ctx
    fldTpReprs, String
    "and", Integer -> String
    forall a. Show a => a -> String
    show Integer
    rawIdx]
                      BaseTypeRepr x
    srepr -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [String
    "expected a struct, got", BaseTypeRepr x -> String
    forall a. Show a => a -> String
    show BaseTypeRepr x
    srepr]
                  [SExpr]
    _ -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [String
    "expected an arg and an Int, got", [SExpr] -> String
    forall a. Show a => a -> String
    show [SExpr]
    operands]
              Text
    "struct" -> do
                case [SExpr]
    operands of
                  [S.WFSList [SExpr]
    rawFldExprs] -> do
                    Some flds <- [SExpr] -> Processor sym (Some (Assignment (SymExpr sym)))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym (Some (Assignment (SymExpr sym)))
    readExprsAsAssignment [SExpr]
    rawFldExprs
                    liftIO (Some <$> W4.mkStruct sym flds)
                  [SExpr]
    _ -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [String
    "struct expects a single operand, got", [SExpr] -> String
    forall a. Show a => a -> String
    show [SExpr]
    operands]
              Text
    "sbvToInteger" -> do
                (Some arg) <- [SExpr]
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym (Some (SymExpr sym))
    readOneArg [SExpr]
    operands
                BVProof _ <- getBVProof arg
                liftIO $ Some <$> W4.sbvToInteger sym arg
              Text
    "bvToInteger" -> do
                (Some arg) <- [SExpr]
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym (Some (SymExpr sym))
    readOneArg [SExpr]
    operands
                BVProof _ <- getBVProof arg
                liftIO $ Some <$> W4.bvToInteger sym arg
              Text
    "integerToBV" -> do
                case [SExpr]
    operands of
                  [S.WFSAtom (ANat Nat
    width), SExpr
    rawValExpr] -> do
                    Some x <- SExpr
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> Processor sym (Some (SymExpr sym))
    readExpr SExpr
    rawValExpr
                    case (mkNatRepr width, W4.exprType x) of
                      (Some NatRepr x
    w, BaseTypeRepr x
    BaseIntegerRepr)
                        | Just LeqProof 1 x
    LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
    forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
    isPosNat NatRepr x
    w -> do
                        IO (Some (Expr t))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (Expr t (BaseBVType x) -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Expr t (BaseBVType x) -> Some (Expr t))
    -> IO (Expr t (BaseBVType x)) -> IO (Some (Expr t))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ExprBuilder t st fs
    -> SymInteger (ExprBuilder t st fs)
    -> NatRepr x
    -> IO (SymBV (ExprBuilder t st fs) x)
    forall (w :: Nat).
    (1 <= w) =>
    ExprBuilder t st fs
    -> SymInteger (ExprBuilder t st fs)
    -> NatRepr w
    -> IO (SymBV (ExprBuilder t st fs) w)
    forall sym (w :: Nat).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
    W4.integerToBV ExprBuilder t st fs
    sym SymInteger (ExprBuilder t st fs)
    Expr t x
    x NatRepr x
    w)
                      (Some NatRepr, BaseTypeRepr x)
    srepr -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [String
    "expected a non-zero natural and an integer, got", (Some NatRepr, BaseTypeRepr x) -> String
    forall a. Show a => a -> String
    show (Some NatRepr, BaseTypeRepr x)
    srepr]
                  [SExpr]
    _ -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [String
    "integerToBV expects two operands, the first of which is a nat, got", [SExpr] -> String
    forall a. Show a => a -> String
    show [SExpr]
    operands]
              Text
    _ -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ String -> Text -> String
    forall r. PrintfType r => String -> r
    printf String
    "couldn't parse application of %s" (Seq String -> SExpr -> Text
    printSExpr Seq String
    forall a. Monoid a => a
    mempty SExpr
    opRaw)
    -- Parse an expression of the form @((_ extract i j) x)@.
    readApp (S.WFSList [S.WFSAtom (AId Text
    "_"), S.WFSAtom (AId Text
    "extract"), S.WFSAtom (AInt Integer
    iInt), S.WFSAtom (AInt Integer
    jInt)])
      [SExpr]
    args = String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall e (m :: Type -> Type) a.
    (Monoid e, MonadError e m) =>
    e -> m a -> m a
    prefixError String
    "in reading extract expression: " (ExceptT
       String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
     -> ExceptT
          String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall a b. (a -> b) -> a -> b
    $ do
      sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
    forall a.
    (ProcessorEnv (ExprBuilder t st fs) -> a)
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
    forall sym. ProcessorEnv sym -> sym
    procSym
      (Some arg) <- readOneArg args
      -- The SMT-LIB spec represents extracts differently than Crucible does. Per
      -- SMT: "extraction of bits i down to j from a bitvector of size m to yield a
      -- new bitvector of size n, where n = i - j + 1". Per Crucible:
      --
      -- > -- | Select a subsequence from a bitvector.
      -- > bvSelect :: (1 <= n, idx + n <= w)
      -- >          => sym
      -- >          -> NatRepr idx  -- ^ Starting index, from 0 as least significant bit
      -- >          -> NatRepr n    -- ^ Number of bits to take
      -- >          -> SymBV sym w  -- ^ Bitvector to select from
      -- >          -> IO (SymBV sym n)
      --
      -- The "starting index" seems to be from the bottom, so that (in slightly
      -- pseudocode)
      --
      -- > > bvSelect sym 0 8 (0x01020304:[32])
      -- > 0x4:[8]
      -- > > bvSelect sym 24 8 (0x01020304:[32])
      -- > 0x1:[8]
      --
      -- Thus, n = i - j + 1, and idx = j.
      let nInt = Integer
    iInt Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    jInt Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1
          idxInt = Integer
    jInt
      Some nNat <- prefixError "in calculating extract length: " $ intToNatM nInt
      Some idxNat <- prefixError "in extract lower bound: " $ intToNatM idxInt
      LeqProof <- fromMaybeError "extract length must be positive" $ isPosNat nNat
      BVProof lenNat <- getBVProof arg
      LeqProof <- fromMaybeError "invalid extract for given bitvector" $
        testLeq (addNat idxNat nNat) lenNat
      liftIO (Some <$> W4.bvSelect sym idxNat nNat arg)
    -- Parse an expression of the form @((_ zero_extend i) x)@ or @((_ sign_extend i) x)@.
    readApp (S.WFSList [S.WFSAtom (AId Text
    "_"), S.WFSAtom (AId Text
    extend), S.WFSAtom (AInt Integer
    iInt)])
      [SExpr]
    args
      | Text
    extend Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    "zero_extend" Bool -> Bool -> Bool
    ||
        Text
    extend Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    "sign_extend" = String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall e (m :: Type -> Type) a.
    (Monoid e, MonadError e m) =>
    e -> m a -> m a
    prefixError (String -> Text -> String
    forall r. PrintfType r => String -> r
    printf String
    "in reading %s expression: " Text
    extend) (ExceptT
       String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
     -> ExceptT
          String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall a b. (a -> b) -> a -> b
    $ do
          sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
    forall a.
    (ProcessorEnv (ExprBuilder t st fs) -> a)
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
    forall sym. ProcessorEnv sym -> sym
    procSym
          Some arg <- readOneArg args
          Some iNat <- intToNatM iInt
          iPositive <- fromMaybeError "must extend by a positive length" $ isPosNat iNat
          BVProof lenNat <- getBVProof arg
          let newLen = NatRepr n -> NatRepr x -> NatRepr (n + x)
    forall (m :: Nat) (n :: Nat).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    addNat NatRepr n
    lenNat NatRepr x
    iNat
          liftIO $ withLeqProof (leqAdd2 (leqRefl lenNat) iPositive) $
            let op = if Text
    extend Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    "zero_extend" then ExprBuilder t st fs
    -> NatRepr (n + x)
    -> SymBV (ExprBuilder t st fs) n
    -> IO (SymBV (ExprBuilder t st fs) (n + x))
    forall (u :: Nat) (r :: Nat).
    (1 <= u, (u + 1) <= r) =>
    ExprBuilder t st fs
    -> NatRepr r
    -> SymBV (ExprBuilder t st fs) u
    -> IO (SymBV (ExprBuilder t st fs) r)
    forall sym (u :: Nat) (r :: Nat).
    (IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    W4.bvZext else ExprBuilder t st fs
    -> NatRepr (n + x)
    -> SymBV (ExprBuilder t st fs) n
    -> IO (SymBV (ExprBuilder t st fs) (n + x))
    forall (u :: Nat) (r :: Nat).
    (1 <= u, (u + 1) <= r) =>
    ExprBuilder t st fs
    -> NatRepr r
    -> SymBV (ExprBuilder t st fs) u
    -> IO (SymBV (ExprBuilder t st fs) r)
    forall sym (u :: Nat) (r :: Nat).
    (IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    W4.bvSext
            in Some <$> op sym newLen arg
    readApp (S.WFSList [S.WFSAtom (AId Text
    "_"), S.WFSAtom (AId Text
    "bvfill"), S.WFSAtom (AInt Integer
    width)]) [SExpr]
    args =
      String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall e (m :: Type -> Type) a.
    (Monoid e, MonadError e m) =>
    e -> m a -> m a
    prefixError String
    "in reading bvfill expression" (ExceptT
       String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
     -> ExceptT
          String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall a b. (a -> b) -> a -> b
    $ do
        sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
    forall a.
    (ProcessorEnv (ExprBuilder t st fs) -> a)
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
    forall sym. ProcessorEnv sym -> sym
    procSym
        Some arg <- readOneArg args
        case W4.exprType arg of
          BaseTypeRepr x
    BaseBoolRepr -> do
            Some widthRep <- Integer
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some NatRepr)
    forall (m :: Type -> Type).
    MonadError String m =>
    Integer -> m (Some NatRepr)
    intToNatM Integer
    width
            LeqProof <- fromMaybeError "must extend by a positive length" $ isPosNat widthRep
            liftIO (Some <$> W4.bvFill sym widthRep arg)
          BaseTypeRepr x
    tyrep -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
    "Invalid argument type to bvFill: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ BaseTypeRepr x -> String
    forall a. Show a => a -> String
    show BaseTypeRepr x
    tyrep)
    readApp SExpr
    rator [SExpr]
    rands = String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT
          String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
    -> String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall a b. (a -> b) -> a -> b
    $ (String
    "readApp could not parse the following: "
                                          String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Text -> String
    T.unpack (Seq String -> SExpr -> Text
    printSExpr Seq String
    forall a. Monoid a => a
    mempty (SExpr -> Text) -> SExpr -> Text
    forall a b. (a -> b) -> a -> b
    $ [SExpr] -> SExpr
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.WFSList (SExpr
    ratorSExpr -> [SExpr] -> [SExpr]
    forall a. a -> [a] -> [a]
    :[SExpr]
    rands))))

    -- | Try converting an 'Integer' to a 'NatRepr' or throw an error if not
    -- possible.
    intToNatM :: (E.MonadError String m) => Integer -> m (Some NatRepr)
    intToNatM :: forall (m :: Type -> Type).
    MonadError String m =>
    Integer -> m (Some NatRepr)
    intToNatM = String -> Maybe (Some NatRepr) -> m (Some NatRepr)
    forall e (m :: Type -> Type) a.
    MonadError e m =>
    e -> Maybe a -> m a
    fromMaybeError String
    "integer must be non-negative to be a nat" (Maybe (Some NatRepr) -> m (Some NatRepr))
    -> (Integer -> Maybe (Some NatRepr)) -> Integer -> m (Some NatRepr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat

    -- | Parse a list of array updates where each entry in the list is:
    --
    -- > (idxs, elt)
    --
    -- where each @idxs@ is a list (assignment) of indexes (with type @idxReprs@)
    -- and each element is an expr.
    --
    -- NOTE: We assume that there are no duplicates in the list and apply the
    -- updates in an arbitrary order.  This is true for any map serialized by this
    -- library.
    expectArrayUpdateMap
      :: forall sym t st fs tp i itp
       . (sym ~ W4.ExprBuilder t st fs)
      => Ctx.Assignment BaseTypeRepr (i Ctx.::> itp)
      -> BaseTypeRepr tp
      -> SExpr
      -> Processor sym (WAU.ArrayUpdateMap (W4.SymExpr sym) (i Ctx.::> itp) tp)
    expectArrayUpdateMap :: forall sym t (st :: Type -> Type) fs (tp :: BaseType)
           (i :: Ctx BaseType) (itp :: BaseType).
    (sym ~ ExprBuilder t st fs) =>
    Assignment BaseTypeRepr (i ::> itp)
    -> BaseTypeRepr tp
    -> SExpr
    -> Processor sym (ArrayUpdateMap (SymExpr sym) (i ::> itp) tp)
    expectArrayUpdateMap Assignment BaseTypeRepr (i ::> itp)
    idxReprs BaseTypeRepr tp
    arrTyRepr SExpr
    updateSExprList =
      case SExpr
    updateSExprList of
        S.L [SExpr]
    items -> (SExpr
     -> ArrayUpdateMap (Expr t) (i ::> itp) tp
     -> ExceptT
          String
          (ReaderT (ProcessorEnv sym) IO)
          (ArrayUpdateMap (Expr t) (i ::> itp) tp))
    -> ArrayUpdateMap (Expr t) (i ::> itp) tp
    -> [SExpr]
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (ArrayUpdateMap (Expr t) (i ::> itp) tp)
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Foldable t, Monad m) =>
    (a -> b -> m b) -> b -> t a -> m b
    F.foldrM SExpr
    -> ArrayUpdateMap (Expr t) (i ::> itp) tp
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (ArrayUpdateMap (Expr t) (i ::> itp) tp)
    expectArrayUpdateEntry ArrayUpdateMap (Expr t) (i ::> itp) tp
    forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    ArrayUpdateMap e ctx tp
    WAU.empty [SExpr]
    items
        SExpr
    _ -> String
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (ArrayUpdateMap (Expr t) (i ::> itp) tp)
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError String
    "Expected a list of array element updates in ArrayMap"
      where
        expectArrayUpdateEntry :: SExpr
    -> ArrayUpdateMap (Expr t) (i ::> itp) tp
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (ArrayUpdateMap (Expr t) (i ::> itp) tp)
    expectArrayUpdateEntry SExpr
    pair ArrayUpdateMap (Expr t) (i ::> itp) tp
    updateMap =
          case SExpr
    pair of
            S.L [S.L [SExpr]
    idxListExprs, SExpr
    elt] -> do
              idxs <- (forall (tp :: BaseType).
     Index (i ::> itp) tp
     -> BaseTypeRepr tp
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (IndexLit tp))
    -> Assignment BaseTypeRepr (i ::> itp)
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Assignment IndexLit (i ::> itp))
    forall {k} (m :: Type -> Type) (ctx :: Ctx k) (f :: k -> Type)
           (g :: k -> Type).
    Applicative m =>
    (forall (tp :: k). Index ctx tp -> f tp -> m (g tp))
    -> Assignment f ctx -> m (Assignment g ctx)
    Ctx.traverseWithIndex ([SExpr]
    -> Index (i ::> itp) tp
    -> BaseTypeRepr tp
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (IndexLit tp)
    forall (ctx :: Ctx BaseType) (tp :: BaseType) sym.
    [SExpr]
    -> Index ctx tp -> BaseTypeRepr tp -> Processor sym (IndexLit tp)
    parseIndexLit [SExpr]
    idxListExprs) Assignment BaseTypeRepr (i ::> itp)
    idxReprs
              Some x <- readExpr elt
              case testEquality arrTyRepr (W4.exprType x) of
                Just tp :~: x
    Refl -> ArrayUpdateMap (Expr t) (i ::> itp) tp
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (ArrayUpdateMap (Expr t) (i ::> itp) tp)
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (BaseTypeRepr tp
    -> Assignment IndexLit (i ::> itp)
    -> Expr t tp
    -> ArrayUpdateMap (Expr t) (i ::> itp) tp
    -> ArrayUpdateMap (Expr t) (i ::> itp) tp
    forall (e :: BaseType -> Type) (tp :: BaseType)
           (ctx :: Ctx BaseType).
    (HashableF e, HasAbsValue e) =>
    BaseTypeRepr tp
    -> Assignment IndexLit ctx
    -> e tp
    -> ArrayUpdateMap e ctx tp
    -> ArrayUpdateMap e ctx tp
    WAU.insert BaseTypeRepr tp
    arrTyRepr Assignment IndexLit (i ::> itp)
    idxs Expr t tp
    Expr t x
    x ArrayUpdateMap (Expr t) (i ::> itp) tp
    updateMap)
                Maybe (tp :~: x)
    Nothing -> String
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (ArrayUpdateMap (Expr t) (i ::> itp) tp)
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError ([String] -> String
    forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
    concat [ String
    "Invalid element type in ArrayMap update: expected "
                                                , BaseTypeRepr tp -> String
    forall a. Show a => a -> String
    show BaseTypeRepr tp
    arrTyRepr
                                                , String
    " but got "
                                                , BaseTypeRepr x -> String
    forall a. Show a => a -> String
    show (Expr t x -> BaseTypeRepr x
    forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W4.exprType Expr t x
    x)])
            SExpr
    _ -> String
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (ArrayUpdateMap (Expr t) (i ::> itp) tp)
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError String
    "Unexpected ArrayMap update item structure"

    -- | Safe list indexing
    --
    -- This version only traverses the list once (compared to computing the length
    -- and then using unsafe indexing)
    (!?) :: [a] -> Int -> Maybe a
    [a]
    lst !? :: forall a. [a] -> Int -> Maybe a
    !? Int
    idx
      | Int
    idx Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    0 = Maybe a
    forall a. Maybe a
    Nothing
      | Bool
    otherwise = Int -> [a] -> Maybe a
    forall {t} {a}. (Eq t, Num t) => t -> [a] -> Maybe a
    go Int
    idx [a]
    lst
      where
        go :: t -> [a] -> Maybe a
    go t
    0 (a
    x:[a]
    _xs) = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    x
        go t
    i (a
    _:[a]
    xs) = t -> [a] -> Maybe a
    go (t
    i t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    1) [a]
    xs
        go t
    _ [] = Maybe a
    forall a. Maybe a
    Nothing

    -- | Parse a single 'WIL.IndexLit' out of a list of 'SExpr' (at the named index)
    --
    -- This is used to build the assignment of indexes
    parseIndexLit :: [SExpr]
                   -> Ctx.Index ctx tp
                   -> BaseTypeRepr tp
                   -> Processor sym (WIL.IndexLit tp)
    parseIndexLit :: forall (ctx :: Ctx BaseType) (tp :: BaseType) sym.
    [SExpr]
    -> Index ctx tp -> BaseTypeRepr tp -> Processor sym (IndexLit tp)
    parseIndexLit [SExpr]
    exprs Index ctx tp
    idx BaseTypeRepr tp
    repr
      | Just (S.A Atom
    atom) <- [SExpr]
    exprs [SExpr] -> Int -> Maybe SExpr
    forall a. [a] -> Int -> Maybe a
    !? Index ctx tp -> Int
    forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
    Ctx.indexVal Index ctx tp
    idx =
          case (BaseTypeRepr tp
    repr, Atom
    atom) of
            (BaseBVRepr NatRepr w
    w, ABV Int
    w' Integer
    val)
              | NatRepr w -> Integer
    forall (n :: Nat). NatRepr n -> Integer
    PN.intValue NatRepr w
    w Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    w' ->
                IndexLit tp -> Processor sym (IndexLit tp)
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (NatRepr w -> BV w -> IndexLit ('BaseBVType w)
    forall (w :: Nat).
    (1 <= w) =>
    NatRepr w -> BV w -> IndexLit ('BaseBVType w)
    WIL.BVIndexLit NatRepr w
    w (NatRepr w -> Integer -> BV w
    forall (w :: Nat). NatRepr w -> Integer -> BV w
    BV.mkBV NatRepr w
    w Integer
    val))
              | Bool
    otherwise -> String -> Processor sym (IndexLit tp)
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
    "Array update index bitvector size mismatch: expected " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NatRepr w -> String
    forall a. Show a => a -> String
    show NatRepr w
    w String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " but got " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    w')
            (BaseTypeRepr tp
    BaseIntegerRepr, AInt Integer
    i) -> IndexLit tp -> Processor sym (IndexLit tp)
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Integer -> IndexLit 'BaseIntegerType
    WIL.IntIndexLit Integer
    i)
            (BaseTypeRepr tp, Atom)
    _ -> String -> Processor sym (IndexLit tp)
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
    "Unexpected array update index type: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ BaseTypeRepr tp -> String
    forall a. Show a => a -> String
    show BaseTypeRepr tp
    repr)
      | Bool
    otherwise = String -> Processor sym (IndexLit tp)
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
    "Invalid or missing array update index at " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Index ctx tp -> String
    forall a. Show a => a -> String
    show Index ctx tp
    idx)

    data ArrayJudgment :: BaseType -> BaseType -> Type where
      ArraySingleDim :: forall idx res.
                        BaseTypeRepr res
                     -> ArrayJudgment idx (BaseArrayType (Ctx.SingleCtx idx) res)

    expectArrayWithIndex :: (E.MonadError String m) => BaseTypeRepr tp1 -> BaseTypeRepr tp2 -> m (ArrayJudgment tp1 tp2)
    expectArrayWithIndex :: forall (m :: Type -> Type) (tp1 :: BaseType) (tp2 :: BaseType).
    MonadError String m =>
    BaseTypeRepr tp1 -> BaseTypeRepr tp2 -> m (ArrayJudgment tp1 tp2)
    expectArrayWithIndex BaseTypeRepr tp1
    dimRepr (BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
    idxTpReprs BaseTypeRepr xs
    resRepr) =
      case Assignment BaseTypeRepr (idx ::> tp)
    -> AssignView BaseTypeRepr (idx ::> tp)
    forall {k} (f :: k -> Type) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    Ctx.viewAssign Assignment BaseTypeRepr (idx ::> tp)
    idxTpReprs of
        Ctx.AssignExtend Assignment BaseTypeRepr ctx1
    rest BaseTypeRepr tp
    idxTpRepr ->
          case Assignment BaseTypeRepr ctx1 -> AssignView BaseTypeRepr ctx1
    forall {k} (f :: k -> Type) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    Ctx.viewAssign Assignment BaseTypeRepr ctx1
    rest of
            AssignView BaseTypeRepr ctx1
    Ctx.AssignEmpty ->
              case BaseTypeRepr tp -> BaseTypeRepr tp1 -> Maybe (tp :~: tp1)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: BaseType) (b :: BaseType).
    BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
    testEquality BaseTypeRepr tp
    idxTpRepr BaseTypeRepr tp1
    dimRepr of
                Just tp :~: tp1
    Refl -> ArrayJudgment tp1 tp2 -> m (ArrayJudgment tp1 tp2)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (ArrayJudgment tp1 tp2 -> m (ArrayJudgment tp1 tp2))
    -> ArrayJudgment tp1 tp2 -> m (ArrayJudgment tp1 tp2)
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr xs
    -> ArrayJudgment tp1 (BaseArrayType (SingleCtx tp1) xs)
    forall (idx :: BaseType) (res :: BaseType).
    BaseTypeRepr res
    -> ArrayJudgment idx (BaseArrayType (SingleCtx idx) res)
    ArraySingleDim BaseTypeRepr xs
    resRepr
                Maybe (tp :~: tp1)
    Nothing -> String -> m (ArrayJudgment tp1 tp2)
    forall a. String -> m a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String -> m (ArrayJudgment tp1 tp2))
    -> String -> m (ArrayJudgment tp1 tp2)
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [String
    "Array index type", BaseTypeRepr tp -> String
    forall a. Show a => a -> String
    show BaseTypeRepr tp
    idxTpRepr,
                                                   String
    "does not match", BaseTypeRepr tp1 -> String
    forall a. Show a => a -> String
    show BaseTypeRepr tp1
    dimRepr]
            AssignView BaseTypeRepr ctx1
    _ -> String -> m (ArrayJudgment tp1 tp2)
    forall a. String -> m a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError String
    "multidimensional arrays are not supported"
    expectArrayWithIndex BaseTypeRepr tp1
    _ BaseTypeRepr tp2
    repr = String -> m (ArrayJudgment tp1 tp2)
    forall a. String -> m a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String -> m (ArrayJudgment tp1 tp2))
    -> String -> m (ArrayJudgment tp1 tp2)
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [String
    "expected an array, got", BaseTypeRepr tp2 -> String
    forall a. Show a => a -> String
    show BaseTypeRepr tp2
    repr]

    exprAssignment ::
      forall sym ctx ex . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym), ShowF ex, W4.IsExpr ex)
      => Ctx.Assignment BaseTypeRepr ctx
      -> [Some ex]
      -> Processor sym (Ctx.Assignment ex ctx)
    exprAssignment :: forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
    (IsSymExprBuilder sym, ShowF (SymExpr sym), ShowF ex, IsExpr ex) =>
    Assignment BaseTypeRepr ctx
    -> [Some ex] -> Processor sym (Assignment ex ctx)
    exprAssignment Assignment BaseTypeRepr ctx
    tpAssns [Some ex]
    exs = do
      Some exsAsn <- Some (Assignment ex)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (Assignment ex))
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Some (Assignment ex)
     -> ExceptT
          String (ReaderT (ProcessorEnv sym) IO) (Some (Assignment ex)))
    -> Some (Assignment ex)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (Assignment ex))
    forall a b. (a -> b) -> a -> b
    $ [Some ex] -> Some (Assignment ex)
    forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
    Ctx.fromList [Some ex]
    exs
      exsRepr <- return $ FC.fmapFC W4.exprType exsAsn
      case testEquality exsRepr tpAssns of
        Just x :~: ctx
    Refl -> Assignment ex ctx
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Assignment ex ctx)
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Assignment ex ctx
    Assignment ex x
    exsAsn
        Maybe (x :~: ctx)
    Nothing -> String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Assignment ex ctx)
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT
          String (ReaderT (ProcessorEnv sym) IO) (Assignment ex ctx))
    -> String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Assignment ex ctx)
    forall a b. (a -> b) -> a -> b
    $
          String
    "Unexpected expression types for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Assignment ex x -> String
    forall a. Show a => a -> String
    show Assignment ex x
    exsAsn
          String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\nExpected: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Assignment BaseTypeRepr ctx -> String
    forall a. Show a => a -> String
    show Assignment BaseTypeRepr ctx
    tpAssns
          String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\nGot: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Assignment BaseTypeRepr x -> String
    forall a. Show a => a -> String
    show Assignment BaseTypeRepr x
    exsRepr

    -- | Given the s-expressions for the bindings and body of a
    -- let, parse the bindings into the Reader monad's state and
    -- then parse the body with those newly bound variables.
    readLetExpr ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => [SExpr]
      -- ^ Bindings in a let-expression.
      -> SExpr
      -- ^ Body of the let-expression.
      -> Processor sym (Some (W4.SymExpr sym))
    readLetExpr :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
    readLetExpr [] SExpr
    body = SExpr
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> Processor sym (Some (SymExpr sym))
    readExpr SExpr
    body
    readLetExpr ((S.WFSList [S.WFSAtom (AId Text
    x), SExpr
    e]):[SExpr]
    rst) SExpr
    body = do
      v <- SExpr
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> Processor sym (Some (SymExpr sym))
    readExpr SExpr
    e
      R.local (\ProcessorEnv (ExprBuilder t st fs)
    c -> ProcessorEnv (ExprBuilder t st fs)
    c {procLetEnv = (HM.insert x v) $ procLetEnv c}) $
        readLetExpr rst body
    readLetExpr [SExpr]
    bindings SExpr
    _body = String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT
          String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
    -> String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall a b. (a -> b) -> a -> b
    $
      String
    "invalid s-expression for let-bindings: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ([SExpr] -> String
    forall a. Show a => a -> String
    show [SExpr]
    bindings)

    readLetFnExpr ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => [SExpr]
      -- ^ Bindings in a let-expression.
      -> SExpr
      -- ^ Body of the let-expression.
      -> Processor sym (Some (W4.SymExpr sym))
    readLetFnExpr :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
    readLetFnExpr [] SExpr
    body = SExpr
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> Processor sym (Some (SymExpr sym))
    readExpr SExpr
    body
    readLetFnExpr ((S.WFSList [S.WFSAtom (AId Text
    f), SExpr
    e]):[SExpr]
    rst) SExpr
    body = do
      v <- SExpr -> Processor sym (SomeSymFn sym)
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> Processor sym (SomeSymFn sym)
    readSymFn SExpr
    e
      R.local (\ProcessorEnv sym
    c -> ProcessorEnv sym
    c {procLetFnEnv = (HM.insert f v) $ procLetFnEnv c}) $
        readLetExpr rst body
    readLetFnExpr [SExpr]
    bindings SExpr
    _body = String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT
          String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
    -> String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall a b. (a -> b) -> a -> b
    $
      String
    "invalid s-expression for let-bindings: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ([SExpr] -> String
    forall a. Show a => a -> String
    show [SExpr]
    bindings)

    -- | Parse an arbitrary expression.
    readExpr ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => SExpr
      -> Processor sym (Some (W4.SymExpr sym))
    readExpr :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> Processor sym (Some (SymExpr sym))
    readExpr (S.WFSAtom (AInt Integer
    n)) = do
      sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
    forall a.
    (ProcessorEnv (ExprBuilder t st fs) -> a)
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
    forall sym. ProcessorEnv sym -> sym
    procSym
      liftIO $ (Some <$> W4.intLit sym n)
    readExpr (S.WFSAtom (ANat Nat
    _)) =
      String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError String
    "Bare Natural literals are no longer used"
    readExpr (S.WFSAtom (ABool Bool
    b)) = do
      sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
    forall a.
    (ProcessorEnv (ExprBuilder t st fs) -> a)
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
    forall sym. ProcessorEnv sym -> sym
    procSym
      liftIO $ return $ Some $ W4.backendPred sym b
    readExpr (S.WFSAtom (AFloat (Some FloatPrecisionRepr x
    repr) BigFloat
    bf)) = do
      sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
    forall a.
    (ProcessorEnv (ExprBuilder t st fs) -> a)
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
    forall sym. ProcessorEnv sym -> sym
    procSym
      liftIO $ (Some <$> W4.floatLit sym repr bf)
    readExpr (S.WFSAtom (AStr Some StringInfoRepr
    prefix Text
    content)) = do
      sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
    forall a.
    (ProcessorEnv (ExprBuilder t st fs) -> a)
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
    forall sym. ProcessorEnv sym -> sym
    procSym
      case prefix of
        (Some StringInfoRepr x
    W4.UnicodeRepr) -> do
          s <- IO (Expr t ('BaseStringType 'Unicode))
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Expr t ('BaseStringType 'Unicode))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (IO (Expr t ('BaseStringType 'Unicode))
     -> ExceptT
          String
          (ReaderT (ProcessorEnv sym) IO)
          (Expr t ('BaseStringType 'Unicode)))
    -> IO (Expr t ('BaseStringType 'Unicode))
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Expr t ('BaseStringType 'Unicode))
    forall a b. (a -> b) -> a -> b
    $ ExprBuilder t st fs
    -> StringLiteral 'Unicode
    -> IO (SymString (ExprBuilder t st fs) 'Unicode)
    forall sym (si :: StringInfo).
    IsExprBuilder sym =>
    sym -> StringLiteral si -> IO (SymString sym si)
    forall (si :: StringInfo).
    ExprBuilder t st fs
    -> StringLiteral si -> IO (SymString (ExprBuilder t st fs) si)
    W4.stringLit ExprBuilder t st fs
    sym (StringLiteral 'Unicode
     -> IO (SymString (ExprBuilder t st fs) 'Unicode))
    -> StringLiteral 'Unicode
    -> IO (SymString (ExprBuilder t st fs) 'Unicode)
    forall a b. (a -> b) -> a -> b
    $ Text -> StringLiteral 'Unicode
    W4.UnicodeLiteral Text
    content
          return $ Some $ s
        (Some StringInfoRepr x
    W4.Char8Repr) -> do
          s <- IO (Expr t (BaseStringType 'Char8))
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Expr t (BaseStringType 'Char8))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (IO (Expr t (BaseStringType 'Char8))
     -> ExceptT
          String
          (ReaderT (ProcessorEnv sym) IO)
          (Expr t (BaseStringType 'Char8)))
    -> IO (Expr t (BaseStringType 'Char8))
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Expr t (BaseStringType 'Char8))
    forall a b. (a -> b) -> a -> b
    $ ExprBuilder t st fs
    -> StringLiteral 'Char8
    -> IO (SymString (ExprBuilder t st fs) 'Char8)
    forall sym (si :: StringInfo).
    IsExprBuilder sym =>
    sym -> StringLiteral si -> IO (SymString sym si)
    forall (si :: StringInfo).
    ExprBuilder t st fs
    -> StringLiteral si -> IO (SymString (ExprBuilder t st fs) si)
    W4.stringLit ExprBuilder t st fs
    sym (StringLiteral 'Char8
     -> IO (SymString (ExprBuilder t st fs) 'Char8))
    -> StringLiteral 'Char8
    -> IO (SymString (ExprBuilder t st fs) 'Char8)
    forall a b. (a -> b) -> a -> b
    $ ByteString -> StringLiteral 'Char8
    W4.Char8Literal (ByteString -> StringLiteral 'Char8)
    -> ByteString -> StringLiteral 'Char8
    forall a b. (a -> b) -> a -> b
    $ Text -> ByteString
    T.encodeUtf8 Text
    content
          return $ Some $ s
        (Some StringInfoRepr x
    W4.Char16Repr) -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ String
    "Char16 strings are not yet supported"
    readExpr (S.WFSAtom (AReal Rational
    _)) = String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT
          String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
    -> String
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall a b. (a -> b) -> a -> b
    $ String
    "TODO: support readExpr for real literals"
    readExpr (S.WFSAtom (ABV Int
    len Integer
    val)) = do
      -- This is a bitvector literal.
      sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
    forall a.
    (ProcessorEnv (ExprBuilder t st fs) -> a)
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
    forall sym. ProcessorEnv sym -> sym
    procSym
      -- The following two patterns should never fail, given that during parsing we
      -- can only construct BVs with positive length.
      case someNat (toInteger len) of
        Just (Some NatRepr x
    lenRepr) -> do
            pf <- case NatRepr x -> Maybe (LeqProof 1 x)
    forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
    isPosNat NatRepr x
    lenRepr of
                    Just LeqProof 1 x
    pf -> LeqProof 1 x
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (LeqProof 1 x)
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return LeqProof 1 x
    pf
                    Maybe (LeqProof 1 x)
    Nothing -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (LeqProof 1 x)
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError String
    "What4.Serialize.Parser.readExpr isPosNat failure"
            liftIO $ withLeqProof pf (Some <$> W4.bvLit sym lenRepr (BV.mkBV lenRepr val))
        Maybe (Some NatRepr)
    Nothing -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError String
    "SemMC.Formula.Parser.readExpr someNat failure"
      -- Just (Some lenRepr) <- return $ someNat (toInteger len)
      -- let Just pf = isPosNat lenRepr
      -- liftIO $ withLeqProof pf (Some <$> W4.bvLit sym lenRepr val)
    -- Let-bound variable
    readExpr (S.WFSAtom (AId Text
    name)) = do
      maybeBinding <- Text -> Processor sym (Maybe (Some (SymExpr sym)))
    forall sym. Text -> Processor sym (Maybe (Some (SymExpr sym)))
    lookupExpr Text
    name
      -- We first check the local lexical environment (i.e., the
      -- in-scope let-bindings) before consulting the "global"
      -- scope.
      case maybeBinding of
        -- simply return it's bound value
        Just Some (Expr t)
    binding -> Some (Expr t)
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Some (Expr t)
    binding
        Maybe (Some (Expr t))
    Nothing -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a b. (a -> b) -> a -> b
    $ (String
    "Unbound variable encountered during deserialization: "
                                   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Text -> String
    T.unpack Text
    name))
    readExpr (S.WFSList ((S.WFSAtom (AId Text
    "let")):[SExpr]
    rhs)) =
      case [SExpr]
    rhs of
        [S.WFSList [SExpr]
    bindings, SExpr
    body] -> [SExpr]
    -> SExpr
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
    readLetExpr [SExpr]
    bindings SExpr
    body
        [SExpr]
    _ -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError String
    "ill-formed let s-expression"
    readExpr (S.WFSList ((S.WFSAtom (AId Text
    "letfn")):[SExpr]
    rhs)) =
      case [SExpr]
    rhs of
        [S.WFSList [SExpr]
    bindings, SExpr
    body] -> [SExpr]
    -> SExpr
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
    readLetFnExpr [SExpr]
    bindings SExpr
    body
        [SExpr]
    _ -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError String
    "ill-formed letfn s-expression"
    readExpr (S.WFSList []) = String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError String
    "ill-formed empty s-expression"
    readExpr (S.WFSList (SExpr
    operator:[SExpr]
    operands)) = SExpr
    -> [SExpr]
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> [SExpr] -> Processor sym (Some (SymExpr sym))
    readApp SExpr
    operator [SExpr]
    operands

    -- | Parse multiple expressions in a list.
    readExprs ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => [SExpr]
      -> Processor sym [Some (W4.SymExpr sym)]
    readExprs :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym [Some (SymExpr sym)]
    readExprs [SExpr]
    exprs = (SExpr
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
    -> [SExpr]
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Some (Expr t)]
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> [a] -> m [b]
    mapM SExpr -> Processor sym (Some (SymExpr sym))
    SExpr
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> Processor sym (Some (SymExpr sym))
    readExpr [SExpr]
    exprs

    readExprsAsAssignment ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => [SExpr]
      -> Processor sym (Some (Ctx.Assignment (W4.SymExpr sym)))
    readExprsAsAssignment :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym (Some (Assignment (SymExpr sym)))
    readExprsAsAssignment [SExpr]
    exprs = [Some (Expr t)] -> Some (Assignment (Expr t))
    forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
    Ctx.fromList ([Some (Expr t)] -> Some (Assignment (Expr t)))
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Some (Expr t)]
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some (Assignment (Expr t)))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [SExpr] -> Processor sym [Some (SymExpr sym)]
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    [SExpr] -> Processor sym [Some (SymExpr sym)]
    readExprs [SExpr]
    exprs

    readFnType ::
      forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))
      => SExpr
      -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
    readFnType :: forall sym.
    (IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
    SExpr -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
    readFnType (S.WFSList ((S.WFSAtom (AId Text
    "->")):[SExpr]
    typeSExprs)) =
      case [SExpr] -> Maybe ([SExpr], SExpr)
    forall a. [a] -> Maybe ([a], a)
    unsnoc [SExpr]
    typeSExprs of
        Maybe ([SExpr], SExpr)
    Nothing ->
          String -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr))
    -> String -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
    forall a b. (a -> b) -> a -> b
    $ (String
    "invalid type signature for function: "
                          String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Text -> String
    T.unpack (Text -> String) -> Text -> String
    forall a b. (a -> b) -> a -> b
    $ Seq String -> SExpr -> Text
    printSExpr Seq String
    forall a. Monoid a => a
    mempty ([SExpr] -> SExpr
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [SExpr]
    typeSExprs)))
        Just ([SExpr]
    domSExps, SExpr
    retSExp) -> do
          dom <- (SExpr
     -> ExceptT
          String (ReaderT (ProcessorEnv sym) IO) (Some BaseTypeRepr))
    -> [SExpr]
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) [Some BaseTypeRepr]
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> [a] -> m [b]
    mapM SExpr
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (Some BaseTypeRepr)
    forall (m :: Type -> Type).
    MonadError String m =>
    SExpr -> m (Some BaseTypeRepr)
    readBaseType [SExpr]
    domSExps
          ret <- readBaseType retSExp
          return (dom, ret)
    readFnType SExpr
    sexpr =
      String -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr))
    -> String -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
    forall a b. (a -> b) -> a -> b
    $ (String
    "invalid type signature for function: "
                      String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Text -> String
    T.unpack (Text -> String) -> Text -> String
    forall a b. (a -> b) -> a -> b
    $ Seq String -> SExpr -> Text
    printSExpr Seq String
    forall a. Monoid a => a
    mempty SExpr
    sexpr))

    -- | If the list is empty, return 'Nothing'. If the list is non-empty, return
    -- @'Just' (xs, x)@, where @xs@ is equivalent to calling 'init' on the list and
    -- @x@ is equivalent to calling 'last' on the list.
    unsnoc :: [a] -> Maybe ([a], a)
    unsnoc :: forall a. [a] -> Maybe ([a], a)
    unsnoc []     = Maybe ([a], a)
    forall a. Maybe a
    Nothing
    unsnoc (a
    x:[a]
    xs) = case [a] -> Maybe ([a], a)
    forall a. [a] -> Maybe ([a], a)
    unsnoc [a]
    xs of
                      Maybe ([a], a)
    Nothing    -> ([a], a) -> Maybe ([a], a)
    forall a. a -> Maybe a
    Just ([], a
    x)
                      Just ([a]
    a,a
    b) -> ([a], a) -> Maybe ([a], a)
    forall a. a -> Maybe a
    Just (a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    a, a
    b)

    readFnArgs ::
      forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))
      => [SExpr]
      -> Processor sym [Text]
    readFnArgs :: forall sym.
    (IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
    [SExpr] -> Processor sym [Text]
    readFnArgs [] = [Text] -> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Text]
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return []
    readFnArgs ((S.WFSAtom (AId Text
    name)):[SExpr]
    rest) = do
      names <- ([SExpr] -> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Text]
    forall sym.
    (IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
    [SExpr] -> Processor sym [Text]
    readFnArgs [SExpr]
    rest)
      return $ name:names
    readFnArgs (SExpr
    badArg:[SExpr]
    _) =
      String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Text]
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Text])
    -> String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Text]
    forall a b. (a -> b) -> a -> b
    $ (String
    "invalid function argument encountered: "
                      String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Text -> String
    T.unpack (Text -> String) -> Text -> String
    forall a b. (a -> b) -> a -> b
    $ Seq String -> SExpr -> Text
    printSExpr Seq String
    forall a. Monoid a => a
    mempty SExpr
    badArg))

    someVarExpr ::
        forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))
      => sym
      -> Some (W4.BoundVar sym)
      -> Some (W4.SymExpr sym)
    someVarExpr :: forall sym.
    (IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
    sym -> Some (BoundVar sym) -> Some (SymExpr sym)
    someVarExpr sym
    sym (Some BoundVar sym x
    bv) = SymExpr sym x -> Some (SymExpr sym)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (sym -> BoundVar sym x -> SymExpr sym x
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym -> BoundVar sym tp -> SymExpr sym tp
    forall (tp :: BaseType). sym -> BoundVar sym tp -> SymExpr sym tp
    W4.varExpr sym
    sym BoundVar sym x
    bv)

    readSymFn ::
      forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
      => SExpr
      -> Processor sym (SomeSymFn sym)
    readSymFn :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    SExpr -> Processor sym (SomeSymFn sym)
    readSymFn (S.WFSList [ S.WFSAtom (AId Text
    "definedfn")
                         , S.WFSAtom (AStr Some StringInfoRepr
    _ Text
    rawSymFnName)
                         , SExpr
    rawFnType
                         , S.WFSList [SExpr]
    argVarsRaw
                         , SExpr
    bodyRaw
                         ]) = do
      sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
    forall a.
    (ProcessorEnv (ExprBuilder t st fs) -> a)
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
    forall sym. ProcessorEnv sym -> sym
    procSym
      symFnName <- case W4.userSymbol (T.unpack rawSymFnName) of
                     Left SolverSymbolError
    _ -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol)
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol
    forall a b. (a -> b) -> a -> b
    $ (String
    "Bad symbolic function name : "
                                               String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Text -> String
    T.unpack Text
    rawSymFnName))
                     Right SolverSymbol
    solverSym -> SolverSymbol
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SolverSymbol
    solverSym
      argNames <- readFnArgs argVarsRaw
      (argTys, _retTy) <- readFnType rawFnType
      when (not (length argTys == length argNames)) $
        E.throwError $ "Function type expected "
        ++ (show $ length argTys)
        ++ " args but found "
        ++ (show $ length argNames)
      argVars <- mapM (\(Text
    name, (Some BaseTypeRepr x
    ty)) ->
                         case String -> Either SolverSymbolError SolverSymbol
    W4.userSymbol (Text -> String
    T.unpack Text
    name) of
                           Left SolverSymbolError
    _ -> String
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Some (BoundVar (ExprBuilder t st fs)))
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT
          String
          (ReaderT (ProcessorEnv sym) IO)
          (Some (BoundVar (ExprBuilder t st fs))))
    -> String
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Some (BoundVar (ExprBuilder t st fs)))
    forall a b. (a -> b) -> a -> b
    $ String
    "Bad arg name : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Text -> String
    T.unpack Text
    name)
                           Right SolverSymbol
    solverSym -> IO (Some (BoundVar (ExprBuilder t st fs)))
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Some (BoundVar (ExprBuilder t st fs)))
    forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (IO (Some (BoundVar (ExprBuilder t st fs)))
     -> ExceptT
          String
          (ReaderT (ProcessorEnv sym) IO)
          (Some (BoundVar (ExprBuilder t st fs))))
    -> IO (Some (BoundVar (ExprBuilder t st fs)))
    -> ExceptT
         String
         (ReaderT (ProcessorEnv sym) IO)
         (Some (BoundVar (ExprBuilder t st fs)))
    forall a b. (a -> b) -> a -> b
    $ ExprBoundVar t x -> Some (BoundVar (ExprBuilder t st fs))
    ExprBoundVar t x -> Some (ExprBoundVar t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (ExprBoundVar t x -> Some (BoundVar (ExprBuilder t st fs)))
    -> IO (ExprBoundVar t x)
    -> IO (Some (BoundVar (ExprBuilder t st fs)))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> ExprBuilder t st fs
    -> SolverSymbol
    -> BaseTypeRepr x
    -> IO (BoundVar (ExprBuilder t st fs) x)
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
    forall (tp :: BaseType).
    ExprBuilder t st fs
    -> SolverSymbol
    -> BaseTypeRepr tp
    -> IO (BoundVar (ExprBuilder t st fs) tp)
    W4.freshBoundVar ExprBuilder t st fs
    sym SolverSymbol
    solverSym BaseTypeRepr x
    ty)
                 $ zip argNames argTys
      (Some body) <- let newBindings = [(Text, Some (SymExpr (ExprBuilder t st fs)))]
    -> HashMap Text (Some (SymExpr (ExprBuilder t st fs)))
    forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
    HM.fromList
                                       ([(Text, Some (SymExpr (ExprBuilder t st fs)))]
     -> HashMap Text (Some (SymExpr (ExprBuilder t st fs))))
    -> [(Text, Some (SymExpr (ExprBuilder t st fs)))]
    -> HashMap Text (Some (SymExpr (ExprBuilder t st fs)))
    forall a b. (a -> b) -> a -> b
    $ [Text]
    -> [Some (SymExpr (ExprBuilder t st fs))]
    -> [(Text, Some (SymExpr (ExprBuilder t st fs)))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Text]
    argNames
                                       ([Some (SymExpr (ExprBuilder t st fs))]
     -> [(Text, Some (SymExpr (ExprBuilder t st fs)))])
    -> [Some (SymExpr (ExprBuilder t st fs))]
    -> [(Text, Some (SymExpr (ExprBuilder t st fs)))]
    forall a b. (a -> b) -> a -> b
    $ (Some (BoundVar (ExprBuilder t st fs))
     -> Some (SymExpr (ExprBuilder t st fs)))
    -> [Some (BoundVar (ExprBuilder t st fs))]
    -> [Some (SymExpr (ExprBuilder t st fs))]
    forall a b. (a -> b) -> [a] -> [b]
    map (ExprBuilder t st fs
    -> Some (BoundVar (ExprBuilder t st fs))
    -> Some (SymExpr (ExprBuilder t st fs))
    forall sym.
    (IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
    sym -> Some (BoundVar sym) -> Some (SymExpr sym)
    someVarExpr ExprBuilder t st fs
    sym) [Some (BoundVar (ExprBuilder t st fs))]
    argVars
                     in R.local
                        (\ProcessorEnv (ExprBuilder t st fs)
    env -> ProcessorEnv (ExprBuilder t st fs)
    env {procLetEnv = HM.union (procLetEnv env) newBindings})
                        $ readExpr bodyRaw
      Some argVarAssignment <- return $ Ctx.fromList argVars
      symFn <- liftIO $ W4.definedFn sym symFnName argVarAssignment body W4.UnfoldConcrete
      return $ SomeSymFn symFn
    readSymFn badSExp :: SExpr
    badSExp@(S.WFSList ((S.WFSAtom (AId Text
    "definedfn")):[SExpr]
    _)) =
      String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym)
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym)
    forall a b. (a -> b) -> a -> b
    $ (String
    "invalid `definedfn`: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Text -> String
    T.unpack (Text -> String) -> Text -> String
    forall a b. (a -> b) -> a -> b
    $ Seq String -> SExpr -> Text
    printSExpr Seq String
    forall a. Monoid a => a
    mempty SExpr
    badSExp))
    readSymFn (S.WFSList [ S.WFSAtom (AId Text
    "uninterpfn")
                         , S.WFSAtom (AStr Some StringInfoRepr
    _ Text
    rawSymFnName)
                         , SExpr
    rawFnType
                         ]) = do
      sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
    -> ExceptT
         String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
    forall a.
    (ProcessorEnv (ExprBuilder t st fs) -> a)
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
    R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
    forall sym. ProcessorEnv sym -> sym
    procSym
      symFnName <- case W4.userSymbol (T.unpack rawSymFnName) of
                     Left SolverSymbolError
    _ -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol)
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol
    forall a b. (a -> b) -> a -> b
    $ (String
    "Bad symbolic function name : "
                                               String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Text -> String
    T.unpack Text
    rawSymFnName))
                     Right SolverSymbol
    solverSym -> SolverSymbol
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol
    forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SolverSymbol
    solverSym
      (argTys, (Some retTy)) <- readFnType rawFnType
      Some domain <- return $ Ctx.fromList argTys
      symFn <- liftIO $ W4.freshTotalUninterpFn sym symFnName domain retTy
      return $ SomeSymFn symFn
    readSymFn badSExp :: SExpr
    badSExp@(S.WFSList ((S.WFSAtom (AId Text
    "uninterpfn")):[SExpr]
    _)) =
      String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym)
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
     -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym))
    -> String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym)
    forall a b. (a -> b) -> a -> b
    $ (String
    "invalid `uninterpfn`: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Text -> String
    T.unpack (Text -> String) -> Text -> String
    forall a b. (a -> b) -> a -> b
    $ Seq String -> SExpr -> Text
    printSExpr Seq String
    forall a. Monoid a => a
    mempty SExpr
    badSExp))
    readSymFn SExpr
    sexpr = String
    -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym)
    forall a.
    String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    E.throwError (String
    "invalid function definition: "
                                    String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Text -> String
    T.unpack (Text -> String) -> Text -> String
    forall a b. (a -> b) -> a -> b
    $ Seq String -> SExpr -> Text
    printSExpr Seq String
    forall a. Monoid a => a
    mempty SExpr
    sexpr))