    {-# Language FlexibleContexts #-}
    {-# Language TypeFamilies #-}
    module Cryptol.Backend
      ( Backend(..)
      , sDelay
      , invalidIndex
      , cryUserError
      , cryNoPrimError
      , FPArith2
      , IndexDirection(..)

      , enumerateIntBits
      , enumerateIntBits'

        -- * Rationals
      , SRational(..)
      , intToRational
      , ratio
      , rationalAdd
      , rationalSub
      , rationalNegate
      , rationalMul
      , rationalRecip
      , rationalDivide
      , rationalFloor
      , rationalCeiling
      , rationalTrunc
      , rationalRoundAway
      , rationalRoundToEven
      , rationalEq
      , rationalLessThan
      , rationalGreaterThan
      , iteRational
      ) where

    import qualified Control.Exception as X
    import Control.Monad.IO.Class
    import Data.Kind (Type)

    import Cryptol.Backend.FloatHelpers (BF)
    import Cryptol.Backend.Monad
      ( EvalError(..), Unsupported(..), CallStack, pushCallFrame )
    import Cryptol.ModuleSystem.Name(Name)
    import Cryptol.Parser.Position
    import Cryptol.TypeCheck.Solver.InfNat(Nat'(..),widthInteger)

    data IndexDirection
      = IndexForward
      | IndexBackward

    invalidIndex :: Backend sym => sym -> Integer -> SEval sym a
    invalidIndex :: forall sym a. Backend sym => sym -> Integer -> SEval sym a
    invalidIndex sym
    sym Integer
    i = sym -> EvalError -> SEval sym a
    forall a. sym -> EvalError -> SEval sym a
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    raiseError sym
    sym (Maybe Integer -> EvalError
    InvalidIndex (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    i))

    cryUserError :: Backend sym => sym -> String -> SEval sym a
    cryUserError :: forall sym a. Backend sym => sym -> String -> SEval sym a
    cryUserError sym
    sym String
    msg = sym -> EvalError -> SEval sym a
    forall a. sym -> EvalError -> SEval sym a
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    raiseError sym
    sym (String -> EvalError
    UserError String
    msg)

    cryNoPrimError :: Backend sym => sym -> Name -> SEval sym a
    cryNoPrimError :: forall sym a. Backend sym => sym -> Name -> SEval sym a
    cryNoPrimError sym
    sym Name
    nm = sym -> EvalError -> SEval sym a
    forall a. sym -> EvalError -> SEval sym a
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    raiseError sym
    sym (Name -> EvalError
    NoPrim Name
    nm)

    {-# INLINE sDelay #-}
    -- | Delay the given evaluation computation, returning a thunk
    --   which will run the computation when forced.  Raise a loop
    --   error if the resulting thunk is forced during its own evaluation.
    sDelay :: Backend sym => sym -> SEval sym a -> SEval sym (SEval sym a)
    sDelay :: forall sym a.
    Backend sym =>
    sym -> SEval sym a -> SEval sym (SEval sym a)
    sDelay sym
    sym SEval sym a
    m = sym
    -> SEval sym a
    -> Maybe (SEval sym a)
    -> String
    -> SEval sym (SEval sym a)
    forall a.
    sym
    -> SEval sym a
    -> Maybe (SEval sym a)
    -> String
    -> SEval sym (SEval sym a)
    forall sym a.
    Backend sym =>
    sym
    -> SEval sym a
    -> Maybe (SEval sym a)
    -> String
    -> SEval sym (SEval sym a)
    sDelayFill sym
    sym SEval sym a
    m Maybe (SEval sym a)
    forall a. Maybe a
    Nothing String
    ""

    -- | Representation of rational numbers.
    --     Invariant: denominator is not 0
    data SRational sym =
      SRational
      { forall sym. SRational sym -> SInteger sym
    sNum :: SInteger sym
      , forall sym. SRational sym -> SInteger sym
    sDenom :: SInteger sym
      }

    intToRational :: Backend sym => sym -> SInteger sym -> SEval sym (SRational sym)
    intToRational :: forall sym.
    Backend sym =>
    sym -> SInteger sym -> SEval sym (SRational sym)
    intToRational sym
    sym SInteger sym
    x = SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational SInteger sym
    x (SInteger sym -> SRational sym)
    -> SEval sym (SInteger sym) -> SEval sym (SRational sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    1)

    ratio :: Backend sym => sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
    ratio :: forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
    ratio sym
    sym SInteger sym
    n SInteger sym
    d =
      do SBit sym
    pz  <- sym -> SBit sym -> SEval sym (SBit sym)
    forall sym. Backend sym => sym -> SBit sym -> SEval sym (SBit sym)
    bitComplement sym
    sym (SBit sym -> SEval sym (SBit sym))
    -> SEval sym (SBit sym) -> SEval sym (SBit sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    intEq sym
    sym SInteger sym
    d (SInteger sym -> SEval sym (SBit sym))
    -> SEval sym (SInteger sym) -> SEval sym (SBit sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    0
         sym -> SBit sym -> EvalError -> SEval sym ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition sym
    sym SBit sym
    pz EvalError
    DivideByZero
         SRational sym -> SEval sym (SRational sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational SInteger sym
    n SInteger sym
    d)

    rationalRecip :: Backend sym => sym -> SRational sym -> SEval sym (SRational sym)
    rationalRecip :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SRational sym)
    rationalRecip sym
    sym (SRational SInteger sym
    a SInteger sym
    b) = sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
    ratio sym
    sym SInteger sym
    b SInteger sym
    a

    rationalDivide :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    rationalDivide :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    rationalDivide sym
    sym SRational sym
    x SRational sym
    y = sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    rationalMul sym
    sym SRational sym
    x (SRational sym -> SEval sym (SRational sym))
    -> SEval sym (SRational sym) -> SEval sym (SRational sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SRational sym -> SEval sym (SRational sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SRational sym)
    rationalRecip sym
    sym SRational sym
    y

    rationalFloor :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)
     -- NB, relies on integer division being round-to-negative-inf division
    rationalFloor :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SInteger sym)
    rationalFloor sym
    sym (SRational SInteger sym
    n SInteger sym
    d) = sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intDiv sym
    sym SInteger sym
    n SInteger sym
    d

    rationalCeiling :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)
    rationalCeiling :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SInteger sym)
    rationalCeiling sym
    sym SRational sym
    r = sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SEval sym (SInteger sym)
    intNegate sym
    sym (SInteger sym -> SEval sym (SInteger sym))
    -> SEval sym (SInteger sym) -> SEval sym (SInteger sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SRational sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SInteger sym)
    rationalFloor sym
    sym (SRational sym -> SEval sym (SInteger sym))
    -> SEval sym (SRational sym) -> SEval sym (SInteger sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SRational sym -> SEval sym (SRational sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SRational sym)
    rationalNegate sym
    sym SRational sym
    r

    rationalTrunc :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)
    rationalTrunc :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SInteger sym)
    rationalTrunc sym
    sym SRational sym
    r =
      do SBit sym
    p <- sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    rationalLessThan sym
    sym SRational sym
    r (SRational sym -> SEval sym (SBit sym))
    -> SEval sym (SRational sym) -> SEval sym (SBit sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SInteger sym -> SEval sym (SRational sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SEval sym (SRational sym)
    intToRational sym
    sym (SInteger sym -> SEval sym (SRational sym))
    -> SEval sym (SInteger sym) -> SEval sym (SRational sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    0
         SInteger sym
    cr <- sym -> SRational sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SInteger sym)
    rationalCeiling sym
    sym SRational sym
    r
         SInteger sym
    fr <- sym -> SRational sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SInteger sym)
    rationalFloor sym
    sym SRational sym
    r
         sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    iteInteger sym
    sym SBit sym
    p SInteger sym
    cr SInteger sym
    fr

    rationalRoundAway :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)
    rationalRoundAway :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SInteger sym)
    rationalRoundAway sym
    sym SRational sym
    r =
      do SBit sym
    p <- sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    rationalLessThan sym
    sym SRational sym
    r (SRational sym -> SEval sym (SBit sym))
    -> SEval sym (SRational sym) -> SEval sym (SBit sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SInteger sym -> SEval sym (SRational sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SEval sym (SRational sym)
    intToRational sym
    sym (SInteger sym -> SEval sym (SRational sym))
    -> SEval sym (SInteger sym) -> SEval sym (SRational sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    0
         SRational sym
    half <- SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational (SInteger sym -> SInteger sym -> SRational sym)
    -> SEval sym (SInteger sym)
    -> SEval sym (SInteger sym -> SRational sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    1 SEval sym (SInteger sym -> SRational sym)
    -> SEval sym (SInteger sym) -> SEval sym (SRational sym)
    forall a b. SEval sym (a -> b) -> SEval sym a -> SEval sym b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    2
         SInteger sym
    cr <- sym -> SRational sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SInteger sym)
    rationalCeiling sym
    sym (SRational sym -> SEval sym (SInteger sym))
    -> SEval sym (SRational sym) -> SEval sym (SInteger sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    rationalSub sym
    sym SRational sym
    r SRational sym
    half
         SInteger sym
    fr <- sym -> SRational sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SInteger sym)
    rationalFloor sym
    sym (SRational sym -> SEval sym (SInteger sym))
    -> SEval sym (SRational sym) -> SEval sym (SInteger sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    rationalAdd sym
    sym SRational sym
    r SRational sym
    half
         sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    iteInteger sym
    sym SBit sym
    p SInteger sym
    cr SInteger sym
    fr

    rationalRoundToEven :: Backend sym => sym -> SRational sym -> SEval sym (SInteger sym)
    rationalRoundToEven :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SInteger sym)
    rationalRoundToEven sym
    sym SRational sym
    r =
      do SInteger sym
    lo <- sym -> SRational sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SInteger sym)
    rationalFloor sym
    sym SRational sym
    r
         SInteger sym
    hi <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intPlus sym
    sym SInteger sym
    lo (SInteger sym -> SEval sym (SInteger sym))
    -> SEval sym (SInteger sym) -> SEval sym (SInteger sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    1
         -- NB: `diff` will be nonnegative because `lo <= r`
         SRational sym
    diff <- sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    rationalSub sym
    sym SRational sym
    r (SRational sym -> SEval sym (SRational sym))
    -> SEval sym (SRational sym) -> SEval sym (SRational sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SInteger sym -> SEval sym (SRational sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SEval sym (SRational sym)
    intToRational sym
    sym SInteger sym
    lo
         SRational sym
    half <- SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational (SInteger sym -> SInteger sym -> SRational sym)
    -> SEval sym (SInteger sym)
    -> SEval sym (SInteger sym -> SRational sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    1 SEval sym (SInteger sym -> SRational sym)
    -> SEval sym (SInteger sym) -> SEval sym (SRational sym)
    forall a b. SEval sym (a -> b) -> SEval sym a -> SEval sym b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    2

         SEval sym (SBit sym)
    -> SEval sym (SInteger sym)
    -> SEval sym (SInteger sym)
    -> SEval sym (SInteger sym)
    ite (sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    rationalLessThan sym
    sym SRational sym
    diff SRational sym
    half) (SInteger sym -> SEval sym (SInteger sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SInteger sym
    lo) (SEval sym (SInteger sym) -> SEval sym (SInteger sym))
    -> SEval sym (SInteger sym) -> SEval sym (SInteger sym)
    forall a b. (a -> b) -> a -> b
    $
           SEval sym (SBit sym)
    -> SEval sym (SInteger sym)
    -> SEval sym (SInteger sym)
    -> SEval sym (SInteger sym)
    ite (sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    rationalGreaterThan sym
    sym SRational sym
    diff SRational sym
    half) (SInteger sym -> SEval sym (SInteger sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SInteger sym
    hi) (SEval sym (SInteger sym) -> SEval sym (SInteger sym))
    -> SEval sym (SInteger sym) -> SEval sym (SInteger sym)
    forall a b. (a -> b) -> a -> b
    $
             SEval sym (SBit sym)
    -> SEval sym (SInteger sym)
    -> SEval sym (SInteger sym)
    -> SEval sym (SInteger sym)
    ite (SInteger sym -> SEval sym (SBit sym)
    isEven SInteger sym
    lo) (SInteger sym -> SEval sym (SInteger sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SInteger sym
    lo) (SInteger sym -> SEval sym (SInteger sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SInteger sym
    hi)

     where
     isEven :: SInteger sym -> SEval sym (SBit sym)
    isEven SInteger sym
    x =
       do SInteger sym
    parity <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMod sym
    sym SInteger sym
    x (SInteger sym -> SEval sym (SInteger sym))
    -> SEval sym (SInteger sym) -> SEval sym (SInteger sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    2
          sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    intEq sym
    sym SInteger sym
    parity (SInteger sym -> SEval sym (SBit sym))
    -> SEval sym (SInteger sym) -> SEval sym (SBit sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    0

     ite :: SEval sym (SBit sym)
    -> SEval sym (SInteger sym)
    -> SEval sym (SInteger sym)
    -> SEval sym (SInteger sym)
    ite SEval sym (SBit sym)
    x SEval sym (SInteger sym)
    t SEval sym (SInteger sym)
    e =
       do SBit sym
    x' <- SEval sym (SBit sym)
    x
          case sym -> SBit sym -> Maybe Bool
    forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
    bitAsLit sym
    sym SBit sym
    x' of
            Just Bool
    True -> SEval sym (SInteger sym)
    t
            Just Bool
    False -> SEval sym (SInteger sym)
    e
            Maybe Bool
    Nothing ->
              do SInteger sym
    t' <- SEval sym (SInteger sym)
    t
                 SInteger sym
    e' <- SEval sym (SInteger sym)
    e
                 sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    iteInteger sym
    sym SBit sym
    x' SInteger sym
    t' SInteger sym
    e'

    rationalAdd :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    rationalAdd :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    rationalAdd sym
    sym (SRational SInteger sym
    a SInteger sym
    b) (SRational SInteger sym
    c SInteger sym
    d) =
      do SInteger sym
    ad <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMult sym
    sym SInteger sym
    a SInteger sym
    d
         SInteger sym
    bc <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMult sym
    sym SInteger sym
    b SInteger sym
    c
         SInteger sym
    bd <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMult sym
    sym SInteger sym
    b SInteger sym
    d
         SInteger sym
    ad_bc <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intPlus sym
    sym SInteger sym
    ad SInteger sym
    bc
         SRational sym -> SEval sym (SRational sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational SInteger sym
    ad_bc SInteger sym
    bd)

    rationalSub :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    rationalSub :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    rationalSub sym
    sym (SRational SInteger sym
    a SInteger sym
    b) (SRational SInteger sym
    c SInteger sym
    d) =
      do SInteger sym
    ad <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMult sym
    sym SInteger sym
    a SInteger sym
    d
         SInteger sym
    bc <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMult sym
    sym SInteger sym
    b SInteger sym
    c
         SInteger sym
    bd <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMult sym
    sym SInteger sym
    b SInteger sym
    d
         SInteger sym
    ad_bc <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMinus sym
    sym SInteger sym
    ad SInteger sym
    bc
         SRational sym -> SEval sym (SRational sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational SInteger sym
    ad_bc SInteger sym
    bd)

    rationalNegate :: Backend sym => sym -> SRational sym -> SEval sym (SRational sym)
    rationalNegate :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SRational sym)
    rationalNegate sym
    sym (SRational SInteger sym
    a SInteger sym
    b) =
      do SInteger sym
    aneg <- sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SEval sym (SInteger sym)
    intNegate sym
    sym SInteger sym
    a
         SRational sym -> SEval sym (SRational sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational SInteger sym
    aneg SInteger sym
    b)

    rationalMul :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    rationalMul :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    rationalMul sym
    sym (SRational SInteger sym
    a SInteger sym
    b) (SRational SInteger sym
    c SInteger sym
    d) =
      do SInteger sym
    ac <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMult sym
    sym SInteger sym
    a SInteger sym
    c
         SInteger sym
    bd <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMult sym
    sym SInteger sym
    b SInteger sym
    d
         SRational sym -> SEval sym (SRational sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational SInteger sym
    ac SInteger sym
    bd)

    rationalEq :: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    rationalEq :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    rationalEq sym
    sym (SRational SInteger sym
    a SInteger sym
    b) (SRational SInteger sym
    c SInteger sym
    d) =
      do SInteger sym
    ad <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMult sym
    sym SInteger sym
    a SInteger sym
    d
         SInteger sym
    bc <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMult sym
    sym SInteger sym
    b SInteger sym
    c
         sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    intEq sym
    sym SInteger sym
    ad SInteger sym
    bc

    normalizeSign :: Backend sym => sym -> SRational sym -> SEval sym (SRational sym)
    normalizeSign :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SRational sym)
    normalizeSign sym
    sym (SRational SInteger sym
    a SInteger sym
    b) =
      do SBit sym
    p <- sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    intLessThan sym
    sym SInteger sym
    b (SInteger sym -> SEval sym (SBit sym))
    -> SEval sym (SInteger sym) -> SEval sym (SBit sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    0
         case sym -> SBit sym -> Maybe Bool
    forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
    bitAsLit sym
    sym SBit sym
    p of
           Just Bool
    False -> SRational sym -> SEval sym (SRational sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational SInteger sym
    a SInteger sym
    b)
           Just Bool
    True  ->
             do SInteger sym
    aneg <- sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SEval sym (SInteger sym)
    intNegate sym
    sym SInteger sym
    a
                SInteger sym
    bneg <- sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SEval sym (SInteger sym)
    intNegate sym
    sym SInteger sym
    b
                SRational sym -> SEval sym (SRational sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational SInteger sym
    aneg SInteger sym
    bneg)
           Maybe Bool
    Nothing ->
             do SInteger sym
    aneg <- sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SEval sym (SInteger sym)
    intNegate sym
    sym SInteger sym
    a
                SInteger sym
    bneg <- sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SEval sym (SInteger sym)
    intNegate sym
    sym SInteger sym
    b
                SInteger sym
    a' <- sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    iteInteger sym
    sym SBit sym
    p SInteger sym
    aneg SInteger sym
    a
                SInteger sym
    b' <- sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    iteInteger sym
    sym SBit sym
    p SInteger sym
    bneg SInteger sym
    b
                SRational sym -> SEval sym (SRational sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational SInteger sym
    a' SInteger sym
    b')

    rationalLessThan:: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    rationalLessThan :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    rationalLessThan sym
    sym SRational sym
    x SRational sym
    y =
      do SRational SInteger sym
    a SInteger sym
    b <- sym -> SRational sym -> SEval sym (SRational sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SRational sym)
    normalizeSign sym
    sym SRational sym
    x
         SRational SInteger sym
    c SInteger sym
    d <- sym -> SRational sym -> SEval sym (SRational sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SEval sym (SRational sym)
    normalizeSign sym
    sym SRational sym
    y
         SInteger sym
    ad <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMult sym
    sym SInteger sym
    a SInteger sym
    d
         SInteger sym
    bc <- sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
    intMult sym
    sym SInteger sym
    b SInteger sym
    c
         sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    intLessThan sym
    sym SInteger sym
    ad SInteger sym
    bc

    rationalGreaterThan:: Backend sym => sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    rationalGreaterThan :: forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    rationalGreaterThan sym
    sym = (SRational sym -> SRational sym -> SEval sym (SBit sym))
    -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    rationalLessThan sym
    sym)

    iteRational :: Backend sym => sym -> SBit sym -> SRational sym -> SRational sym -> SEval sym (SRational sym)
    iteRational :: forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SRational sym
    -> SRational sym
    -> SEval sym (SRational sym)
    iteRational sym
    sym SBit sym
    p (SRational SInteger sym
    a SInteger sym
    b) (SRational SInteger sym
    c SInteger sym
    d) =
      SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational (SInteger sym -> SInteger sym -> SRational sym)
    -> SEval sym (SInteger sym)
    -> SEval sym (SInteger sym -> SRational sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    iteInteger sym
    sym SBit sym
    p SInteger sym
    a SInteger sym
    c SEval sym (SInteger sym -> SRational sym)
    -> SEval sym (SInteger sym) -> SEval sym (SRational sym)
    forall a b. SEval sym (a -> b) -> SEval sym a -> SEval sym b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SInteger sym
    -> SInteger sym
    -> SEval sym (SInteger sym)
    iteInteger sym
    sym SBit sym
    p SInteger sym
    b SInteger sym
    d

    -- | Compute the list of bits in an integer in big-endian order.
    --   The integer argument is a concrete upper bound for
    --   the symbolic integer.
    enumerateIntBits' :: Backend sym =>
      sym ->
      Integer ->
      SInteger sym ->
      SEval sym (Integer, [SBit sym])
    enumerateIntBits' :: forall sym.
    Backend sym =>
    sym -> Integer -> SInteger sym -> SEval sym (Integer, [SBit sym])
    enumerateIntBits' sym
    sym Integer
    n SInteger sym
    idx =
      do let width :: Integer
    width = Integer -> Integer
    widthInteger Integer
    n
         SWord sym
    w <- sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
    wordFromInt sym
    sym Integer
    width SInteger sym
    idx
         [SBit sym]
    bs <- sym -> SWord sym -> SEval sym [SBit sym]
    forall sym. Backend sym => sym -> SWord sym -> SEval sym [SBit sym]
    unpackWord sym
    sym SWord sym
    w
         (Integer, [SBit sym]) -> SEval sym (Integer, [SBit sym])
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer
    width, [SBit sym]
    bs)

    -- | Compute the list of bits in an integer in big-endian order.
    --   Fails if neither the sequence length nor the type value
    --   provide an upper bound for the integer.
    enumerateIntBits :: Backend sym =>
      sym ->
      Nat' ->
      SInteger sym ->
      SEval sym (Integer, [SBit sym])
    enumerateIntBits :: forall sym.
    Backend sym =>
    sym -> Nat' -> SInteger sym -> SEval sym (Integer, [SBit sym])
    enumerateIntBits sym
    sym (Nat Integer
    n) SInteger sym
    idx = sym -> Integer -> SInteger sym -> SEval sym (Integer, [SBit sym])
    forall sym.
    Backend sym =>
    sym -> Integer -> SInteger sym -> SEval sym (Integer, [SBit sym])
    enumerateIntBits' sym
    sym Integer
    n SInteger sym
    idx
    enumerateIntBits sym
    _sym Nat'
    Inf SInteger sym
    _ = IO (Integer, [SBit sym]) -> SEval sym (Integer, [SBit sym])
    forall a. IO a -> SEval sym a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (Unsupported -> IO (Integer, [SBit sym])
    forall a e. Exception e => e -> a
    X.throw (String -> Unsupported
    UnsupportedSymbolicOp String
    "unbounded integer shifting"))

    -- | This type class defines a collection of operations on bits, words and integers that
    --   are necessary to define generic evaluator primitives that operate on both concrete
    --   and symbolic values uniformly.
    class MonadIO (SEval sym) => Backend sym where
      type SBit sym :: Type
      type SWord sym :: Type
      type SInteger sym :: Type
      type SFloat sym :: Type
      type SEval sym :: Type -> Type

      -- ==== Evaluation monad operations ====

      -- | Check if an operation is "ready", which means its
      --   evaluation will be trivial.
      isReady :: sym -> SEval sym a -> SEval sym (Maybe a)

      -- | Produce a thunk value which can be filled with its associated computation
      --   after the fact.  A preallocated thunk is returned, along with an operation to
      --   fill the thunk with the associated computation.
      --   This is used to implement recursive declaration groups.
      sDeclareHole :: sym -> String -> SEval sym (SEval sym a, SEval sym a -> SEval sym ())

      -- | Delay the given evaluation computation, returning a thunk
      --   which will run the computation when forced.  Run the 'retry'
      --   computation instead if the resulting thunk is forced during
      --   its own evaluation.
      sDelayFill :: sym -> SEval sym a -> Maybe (SEval sym a) -> String -> SEval sym (SEval sym a)

      -- | Begin evaluating the given computation eagerly in a separate thread
      --   and return a thunk which will await the completion of the given computation
      --   when forced.
      sSpark :: sym -> SEval sym a -> SEval sym (SEval sym a)

      -- | Push a call frame on to the current call stack while evaluating the given action
      sPushFrame :: sym -> Name -> Range -> SEval sym a -> SEval sym a
      sPushFrame sym
    sym Name
    nm Range
    rng SEval sym a
    m = sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
    forall a.
    sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
    forall sym a.
    Backend sym =>
    sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
    sModifyCallStack sym
    sym (Name -> Range -> CallStack -> CallStack
    pushCallFrame Name
    nm Range
    rng) SEval sym a
    m

      -- | Use the given call stack while evaluating the given action
      sWithCallStack :: sym -> CallStack -> SEval sym a -> SEval sym a
      sWithCallStack sym
    sym CallStack
    stk SEval sym a
    m = sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
    forall a.
    sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
    forall sym a.
    Backend sym =>
    sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
    sModifyCallStack sym
    sym (\CallStack
    _ -> CallStack
    stk) SEval sym a
    m

      -- | Apply the given function to the current call stack while evaluating the given action
      sModifyCallStack :: sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a

      -- | Retrieve the current evaluation call stack
      sGetCallStack :: sym -> SEval sym CallStack

      -- | Merge the two given computations according to the predicate.
      mergeEval ::
         sym ->
         (SBit sym -> a -> a -> SEval sym a) {- ^ A merge operation on values -} ->
         SBit sym {- ^ The condition -} ->
         SEval sym a {- ^ The "then" computation -} ->
         SEval sym a {- ^ The "else" computation -} ->
         SEval sym a

      -- | Assert that a condition must hold, and indicate what sort of
      --   error is indicated if the condition fails.
      assertSideCondition :: sym -> SBit sym -> EvalError -> SEval sym ()

      -- | Indiciate that an error condition exists
      raiseError :: sym -> EvalError -> SEval sym a

      -- ==== Identifying literal values ====

      -- | Determine if this symbolic bit is a boolean literal
      bitAsLit :: sym -> SBit sym -> Maybe Bool

      -- | The number of bits in a word value.
      wordLen :: sym -> SWord sym -> Integer

      -- | Determine if this symbolic word is a literal.
      --   If so, return the bit width and value.
      wordAsLit :: sym -> SWord sym -> Maybe (Integer, Integer)

      -- | Attempt to render a word value as an ASCII character.  Return 'Nothing'
      --   if the character value is unknown (e.g., for symbolic values).
      wordAsChar :: sym -> SWord sym -> Maybe Char

      -- | Determine if this symbolic integer is a literal
      integerAsLit :: sym -> SInteger sym -> Maybe Integer

      -- | Determine if this symbolic floating-point value is a literal
      fpAsLit :: sym -> SFloat sym -> Maybe BF

      -- ==== Creating literal values ====

      -- | Construct a literal bit value from a boolean.
      bitLit :: sym -> Bool -> SBit sym

      -- | Construct a literal word value given a bit width and a value.
      wordLit ::
        sym ->
        Integer {- ^ Width -} ->
        Integer {- ^ Value -} ->
        SEval sym (SWord sym)

      -- | Construct a literal integer value from the given integer.
      integerLit ::
        sym ->
        Integer {- ^ Value -} ->
        SEval sym (SInteger sym)

      -- | Construct a floating point value from the given rational.
      fpLit ::
        sym ->
        Integer  {- ^ exponent bits -} ->
        Integer  {- ^ precision bits -} ->
        Rational {- ^ The rational -} ->
        SEval sym (SFloat sym)

      -- | Construct a floating point value from the given bit-precise
      --   floating-point representation.
      fpExactLit :: sym -> BF -> SEval sym (SFloat sym)

      -- ==== If/then/else operations ====
      iteBit :: sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
      iteWord :: sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
      iteInteger :: sym -> SBit sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
      iteFloat :: sym -> SBit sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)

      -- ==== Bit operations ====
      bitEq  :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
      bitOr  :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
      bitAnd :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
      bitXor :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
      bitComplement :: sym -> SBit sym -> SEval sym (SBit sym)

      -- ==== Word operations ====

      -- | Extract the numbered bit from the word.
      --
      --   NOTE: this assumes that the sequence of bits is big-endian and finite, so the
      --   bit numbered 0 is the most significant bit.
      wordBit ::
        sym ->
        SWord sym ->
        Integer {- ^ Bit position to extract -} ->
        SEval sym (SBit sym)

      -- | Update the numbered bit in the word.
      --
      --   NOTE: this assumes that the sequence of bits is big-endian and finite, so the
      --   bit numbered 0 is the most significant bit.
      wordUpdate ::
        sym ->
        SWord sym ->
        Integer {- ^ Bit position to update -} ->
        SBit sym ->
        SEval sym (SWord sym)

      -- | Construct a word value from a finite sequence of bits.
      --   NOTE: this assumes that the sequence of bits is big-endian and finite, so the
      --   first element of the list will be the most significant bit.
      packWord ::
        sym ->
        [SBit sym] ->
        SEval sym (SWord sym)

      -- | Deconstruct a packed word value in to a finite sequence of bits.
      --   NOTE: this produces a list of bits that represent a big-endian word, so
      --   the most significant bit is the first element of the list.
      unpackWord ::
        sym ->
        SWord sym ->
        SEval sym [SBit sym]

      -- | Construct a packed word of the specified width from an integer value.
      wordFromInt ::
        sym ->
        Integer {- ^ bit-width -} ->
        SInteger sym ->
        SEval sym (SWord sym)

      -- | Concatenate the two given word values.
      --   NOTE: the first argument represents the more-significant bits
      joinWord ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | Take the most-significant bits, and return
      --   those bits and the remainder.  The first element
      --   of the pair is the most significant bits.
      --   The two integer sizes must sum to the length of the given word value.
      splitWord ::
        sym ->
        Integer {- ^ left width -} ->
        Integer {- ^ right width -} ->
        SWord sym ->
        SEval sym (SWord sym, SWord sym)

      -- | Extract a subsequence of bits from a packed word value.
      --   The first integer argument is the number of bits in the
      --   resulting word.  The second integer argument is the
      --   number of less-significant digits to discard.  Stated another
      --   way, the operation @extractWord n i w@ is equivalent to
      --   first shifting @w@ right by @i@ bits, and then truncating to
      --   @n@ bits.
      extractWord ::
        sym ->
        Integer {- ^ Number of bits to take -} ->
        Integer {- ^ starting bit -} ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | Bitwise OR
      wordOr ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | Bitwise AND
      wordAnd ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | Bitwise XOR
      wordXor ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | Bitwise complement
      wordComplement ::
        sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | 2's complement addition of packed words.  The arguments must have
      --   equal bit width, and the result is of the same width. Overflow is silently
      --   discarded.
      wordPlus ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | 2's complement subtraction of packed words.  The arguments must have
      --   equal bit width, and the result is of the same width. Overflow is silently
      --   discarded.
      wordMinus ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | 2's complement multiplication of packed words.  The arguments must have
      --   equal bit width, and the result is of the same width. The high bits of the
      --   multiplication are silently discarded.
      wordMult ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | 2's complement unsigned division of packed words.  The arguments must have
      --   equal bit width, and the result is of the same width.  It is illegal to
      --   call with a second argument concretely equal to 0.
      wordDiv ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | 2's complement unsigned modulus of packed words.  The arguments must have
      --   equal bit width, and the result is of the same width.  It is illegal to
      --   call with a second argument concretely equal to 0.
      wordMod ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | 2's complement signed division of packed words.  The arguments must have
      --   equal bit width, and the result is of the same width.  It is illegal to
      --   call with a second argument concretely equal to 0.
      wordSignedDiv ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | 2's complement signed modulus of packed words.  The arguments must have
      --   equal bit width, and the result is of the same width.  It is illegal to
      --   call with a second argument concretely equal to 0.
      wordSignedMod ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | Shift a bitvector left by the specified amount.
      --   The shift amount is considered as an unsigned value.
      --   Shifting by more than the word length results in 0.
      wordShiftLeft ::
        sym ->
        SWord sym {- ^ value to shift -} ->
        SWord sym {- ^ amount to shift by -} ->
        SEval sym (SWord sym)

      -- | Shift a bitvector right by the specified amount.
      --   This is a logical shift, which shifts in 0 values
      --   on the left. The shift amount is considered as an
      --   unsigned value. Shifting by more than the word length
      --   results in 0.
      wordShiftRight ::
        sym ->
        SWord sym {- ^ value to shift -} ->
        SWord sym {- ^ amount to shift by -} ->
        SEval sym (SWord sym)

      -- | Shift a bitvector right by the specified amount.  This is an
      --   arithmetic shift, which shifts in copies of the high bit on the
      --   left. The shift amount is considered as an unsigned
      --   value. Shifting by more than the word length results in filling
      --   the bitvector with the high bit.
      wordSignedShiftRight ::
        sym ->
        SWord sym {- ^ value to shift -} ->
        SWord sym {- ^ amount to shift by -} ->
        SEval sym (SWord sym)

      wordRotateLeft ::
        sym ->
        SWord sym {- ^ value to rotate -} ->
        SWord sym {- ^ amount to rotate by -} ->
        SEval sym (SWord sym)

      wordRotateRight ::
        sym ->
        SWord sym {- ^ value to rotate -} ->
        SWord sym {- ^ amount to rotate by -} ->
        SEval sym (SWord sym)

      -- | 2's complement negation of bitvectors
      wordNegate ::
        sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | Compute rounded-up log-2 of the input
      wordLg2 ::
        sym ->
        SWord sym ->
        SEval sym (SWord sym)

      -- | Test if two words are equal.  Arguments must have the same width.
      wordEq ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SBit sym)

      -- | Signed less-than comparison on words.  Arguments must have the same width.
      wordSignedLessThan ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SBit sym)

      -- | Unsigned less-than comparison on words.  Arguments must have the same width.
      wordLessThan ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SBit sym)

      -- | Unsigned greater-than comparison on words.  Arguments must have the same width.
      wordGreaterThan ::
        sym ->
        SWord sym ->
        SWord sym ->
        SEval sym (SBit sym)

      -- | Construct an integer value from the given packed word.
      wordToInt ::
        sym ->
        SWord sym ->
        SEval sym (SInteger sym)

      -- | Construct a signed integer value from the given packed word.
      wordToSignedInt ::
        sym ->
        SWord sym ->
        SEval sym (SInteger sym)

      -- ==== Integer operations ====

      -- | Addition of unbounded integers.
      intPlus ::
        sym ->
        SInteger sym ->
        SInteger sym ->
        SEval sym (SInteger sym)

      -- | Negation of unbounded integers
      intNegate ::
        sym ->
        SInteger sym ->
        SEval sym (SInteger sym)

      -- | Subtraction of unbounded integers.
      intMinus ::
        sym ->
        SInteger sym ->
        SInteger sym ->
        SEval sym (SInteger sym)

      -- | Multiplication of unbounded integers.
      intMult ::
        sym ->
        SInteger sym ->
        SInteger sym ->
        SEval sym (SInteger sym)

      -- | Integer division, rounding down. It is illegal to
      --   call with a second argument concretely equal to 0.
      --   Same semantics as Haskell's @div@ operation.
      intDiv ::
        sym ->
        SInteger sym ->
        SInteger sym ->
        SEval sym (SInteger sym)

      -- | Integer modulus, with division rounding down. It is illegal to
      --   call with a second argument concretely equal to 0.
      --   Same semantics as Haskell's @mod@ operation.
      intMod ::
        sym ->
        SInteger sym ->
        SInteger sym ->
        SEval sym (SInteger sym)

      -- | Equality comparison on integers
      intEq ::
        sym ->
        SInteger sym ->
        SInteger sym ->
        SEval sym (SBit sym)

      -- | Less-than comparison on integers
      intLessThan ::
        sym ->
        SInteger sym ->
        SInteger sym ->
        SEval sym (SBit sym)

      -- | Greater-than comparison on integers
      intGreaterThan ::
        sym ->
        SInteger sym ->
        SInteger sym ->
        SEval sym (SBit sym)

      -- ==== Operations on Z_n ====

      -- | Turn an integer into a value in Z_n
      intToZn ::
        sym ->
        Integer {- ^ modulus -} ->
        SInteger sym ->
        SEval sym (SInteger sym)

      -- | Transform a Z_n value into an integer, ensuring the value is properly
      --   reduced modulo n
      znToInt ::
        sym ->
        Integer {- ^ modulus -} ->
        SInteger sym ->
        SEval sym (SInteger sym)

      -- | Addition of integers modulo n, for a concrete positive integer n.
      znPlus ::
        sym ->
        Integer {- ^ modulus -} ->
        SInteger sym ->
        SInteger sym ->
        SEval sym (SInteger sym)

      -- | Additive inverse of integers modulo n
      znNegate ::
        sym ->
        Integer {- ^ modulus -} ->
        SInteger sym ->
        SEval sym (SInteger sym)

      -- | Subtraction of integers modulo n, for a concrete positive integer n.
      znMinus ::
        sym ->
        Integer {- ^ modulus -} ->
        SInteger sym ->
        SInteger sym ->
        SEval sym (SInteger sym)

      -- | Multiplication of integers modulo n, for a concrete positive integer n.
      znMult ::
        sym ->
        Integer {- ^ modulus -} ->
        SInteger sym ->
        SInteger sym ->
        SEval sym (SInteger sym)

      -- | Equality test of integers modulo n
      znEq ::
        sym ->
        Integer {- ^ modulus -} ->
        SInteger sym ->
        SInteger sym ->
        SEval sym (SBit sym)

      -- | Multiplicative inverse in (Z n).
      --   PRECONDITION: the modulus is a prime
      znRecip ::
        sym ->
        Integer {- ^ modulus -} ->
        SInteger sym ->
        SEval sym (SInteger sym)

      -- == Float Operations ==
      fpEq          :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
      fpLessThan    :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
      fpGreaterThan :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)

      fpLogicalEq   :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)

      fpNaN    :: sym -> Integer {- ^ exponent bits -} -> Integer {- ^ precision bits -} -> SEval sym (SFloat sym)
      fpPosInf :: sym -> Integer {- ^ exponent bits -} -> Integer {- ^ precision bits -} -> SEval sym (SFloat sym)

      fpPlus, fpMinus, fpMult, fpDiv :: FPArith2 sym
      fpNeg, fpAbs :: sym -> SFloat sym -> SEval sym (SFloat sym)
      fpSqrt :: sym -> SWord sym -> SFloat sym -> SEval sym (SFloat sym)

      fpFMA :: sym -> SWord sym -> SFloat sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)

      fpIsZero, fpIsNeg, fpIsNaN, fpIsInf, fpIsNorm, fpIsSubnorm :: sym -> SFloat sym -> SEval sym (SBit sym)

      fpToBits :: sym -> SFloat sym -> SEval sym (SWord sym)
      fpFromBits ::
        sym ->
        Integer {- ^ exponent bits -} ->
        Integer {- ^ precision bits -} ->
        SWord sym ->
        SEval sym (SFloat sym)

      fpToInteger ::
        sym ->
        String {- ^ Name of the function for error reporting -} ->
        SWord sym {- ^ Rounding mode -} ->
        SFloat sym ->
        SEval sym (SInteger sym)

      fpFromInteger ::
        sym ->
        Integer         {- ^ exp width -} ->
        Integer         {- ^ prec width -} ->
        SWord sym       {- ^ rounding mode -} ->
        SInteger sym    {- ^ the integer to use -} ->
        SEval sym (SFloat sym)

      fpToRational ::
        sym ->
        SFloat sym ->
        SEval sym (SRational sym)

      fpFromRational ::
        sym ->
        Integer         {- ^ exp width -} ->
        Integer         {- ^ prec width -} ->
        SWord sym       {- ^ rounding mode -} ->
        SRational sym ->
        SEval sym (SFloat sym)

    type FPArith2 sym =
      sym ->
      SWord sym ->
      SFloat sym ->
      SFloat sym ->
      SEval sym (SFloat sym)