    {-|
    Module      : What4.Expr.MATLAB
    Description : Low-level support for MATLAB-style arithmetic operations
    Copyright   : (c) Galois, Inc, 2016-2020
    License     : BSD3
    Maintainer  : Joe Hendrix <jhendrix@galois.com>

    This module provides an interface that a symbolic backend should
    implement to support MATLAB intrinsics.
    -}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE TypeOperators #-}
    module What4.Expr.MATLAB
      ( MatlabSolverFn(..)
      , matlabSolverArgTypes
      , matlabSolverReturnType
      , ppMatlabSolverFn
      , evalMatlabSolverFn
      , testSolverFnEq
      , traverseMatlabSolverFn
      , MatlabSymbolicArrayBuilder(..)

        -- * Utilities for definition
      , clampedIntAdd
      , clampedIntSub
      , clampedIntMul
      , clampedIntNeg
      , clampedIntAbs
      , clampedUIntAdd
      , clampedUIntSub
      , clampedUIntMul
      ) where

    import           Control.Monad (join)
    import qualified Data.BitVector.Sized as BV
    import           Data.Kind (Type)
    import           Data.Hashable
    import           Data.Parameterized.Classes
    import           Data.Parameterized.Context as Ctx
    import           Data.Parameterized.TH.GADT
    import           Data.Parameterized.TraversableFC
    import           Prettyprinter

    import           What4.BaseTypes
    import           What4.Interface
    import           What4.Utils.Complex
    import           What4.Utils.OnlyIntRepr

    ------------------------------------------------------------------------
    -- MatlabSolverFn

    clampedIntAdd :: (IsExprBuilder sym, 1 <= w)
                  => sym
                  -> SymBV sym w
                  -> SymBV sym w
                  -> IO (SymBV sym w)
    clampedIntAdd :: forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    clampedIntAdd sym
    sym SymBV sym w
    x SymBV sym w
    y = do
      let w :: NatRepr w
    w = SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    bvWidth SymBV sym w
    x
      NatRepr w
    -> NatRepr 1
    -> (Assert (1 <=? (w + 1)) (LeErrMsg 1 (w + 1)) =>
        IO (SymBV sym w))
    -> IO (SymBV sym w)
    forall (n :: Natural) (m :: Natural) a.
    NatRepr n -> NatRepr m -> ((m <= (n + m)) => a) -> a
    withAddPrefixLeq NatRepr w
    w (NatRepr 1
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat :: NatRepr 1) ((Assert (1 <=? (w + 1)) (LeErrMsg 1 (w + 1)) => IO (SymBV sym w))
     -> IO (SymBV sym w))
    -> (Assert (1 <=? (w + 1)) (LeErrMsg 1 (w + 1)) =>
        IO (SymBV sym w))
    -> IO (SymBV sym w)
    forall a b. (a -> b) -> a -> b
    $ do
      -- Compute result with 1 additional bit to catch clamping
      let w' :: NatRepr (w + 1)
    w' = NatRepr w -> NatRepr (w + 1)
    forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
    incNat NatRepr w
    w
      SymExpr sym (BaseBVType (w + 1))
    x'  <- sym
    -> NatRepr (w + 1)
    -> SymBV sym w
    -> IO (SymExpr sym (BaseBVType (w + 1)))
    forall (u :: Natural) (r :: Natural).
    (1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    forall sym (u :: Natural) (r :: Natural).
    (IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    bvSext sym
    sym NatRepr (w + 1)
    w' SymBV sym w
    x
      SymExpr sym (BaseBVType (w + 1))
    y'  <- sym
    -> NatRepr (w + 1)
    -> SymBV sym w
    -> IO (SymExpr sym (BaseBVType (w + 1)))
    forall (u :: Natural) (r :: Natural).
    (1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    forall sym (u :: Natural) (r :: Natural).
    (IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
    sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
    bvSext sym
    sym NatRepr (w + 1)
    w' SymBV sym w
    y
      -- Compute result.
      SymExpr sym (BaseBVType (w + 1))
    r'  <- sym
    -> SymExpr sym (BaseBVType (w + 1))
    -> SymExpr sym (BaseBVType (w + 1))
    -> IO (SymExpr sym (BaseBVType (w + 1)))
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvAdd sym
    sym SymExpr sym (BaseBVType (w + 1))
    x' SymExpr sym (BaseBVType (w + 1))
    y'

      -- Check is result is greater than or equal to max value.
      SymExpr sym BaseBoolType
    too_high <- sym
    -> SymExpr sym (BaseBVType (w + 1))
    -> SymExpr sym (BaseBVType (w + 1))
    -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    bvSgt sym
    sym SymExpr sym (BaseBVType (w + 1))
    r' (SymExpr sym (BaseBVType (w + 1)) -> IO (SymExpr sym BaseBoolType))
    -> IO (SymExpr sym (BaseBVType (w + 1)))
    -> IO (SymExpr sym BaseBoolType)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym
    -> NatRepr (w + 1)
    -> BV (w + 1)
    -> IO (SymExpr sym (BaseBVType (w + 1)))
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    bvLit sym
    sym NatRepr (w + 1)
    w' (NatRepr (w + 1) -> BV (w + 1)
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
    BV.maxSigned NatRepr (w + 1)
    w')
      SymBV sym w
    max_int <- sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    bvLit sym
    sym NatRepr w
    w (NatRepr w -> BV w
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
    BV.maxSigned NatRepr w
    w)

      -- Check is result is less than min value.
      SymExpr sym BaseBoolType
    too_low <- sym
    -> SymExpr sym (BaseBVType (w + 1))
    -> SymExpr sym (BaseBVType (w + 1))
    -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    bvSlt sym
    sym SymExpr sym (BaseBVType (w + 1))
    r' (SymExpr sym (BaseBVType (w + 1)) -> IO (SymExpr sym BaseBoolType))
    -> IO (SymExpr sym (BaseBVType (w + 1)))
    -> IO (SymExpr sym BaseBoolType)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym
    -> NatRepr (w + 1)
    -> BV (w + 1)
    -> IO (SymExpr sym (BaseBVType (w + 1)))
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    bvLit sym
    sym NatRepr (w + 1)
    w' (NatRepr (w + 1) -> BV (w + 1)
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
    BV.minSigned NatRepr (w + 1)
    w')
      SymBV sym w
    min_int <- sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    bvLit sym
    sym NatRepr w
    w (NatRepr w -> BV w
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
    BV.minSigned NatRepr w
    w)

      -- Clamp integer range.
      SymBV sym w
    r <- sym
    -> NatRepr w
    -> SymExpr sym (BaseBVType (w + 1))
    -> IO (SymBV sym w)
    forall (r :: Natural) (w :: Natural).
    (1 <= r, (r + 1) <= w) =>
    sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
    forall sym (r :: Natural) (w :: Natural).
    (IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
    sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
    bvTrunc sym
    sym NatRepr w
    w SymExpr sym (BaseBVType (w + 1))
    r'
      SymBV sym w
    r_low <- sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvIte sym
    sym SymExpr sym BaseBoolType
    too_low SymBV sym w
    min_int SymBV sym w
    r
      sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvIte sym
    sym SymExpr sym BaseBoolType
    too_high SymBV sym w
    max_int SymBV sym w
    r_low

    clampedIntSub :: (IsExprBuilder sym, 1 <= w)
                  => sym
                  -> SymBV sym w
                  -> SymBV sym w
                  -> IO (SymBV sym w)
    clampedIntSub :: forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    clampedIntSub sym
    sym SymBV sym w
    x SymBV sym w
    y = do
      let w :: NatRepr w
    w = SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    bvWidth SymBV sym w
    x
      (SymExpr sym BaseBoolType
    ov, SymBV sym w
    xy) <- sym
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymExpr sym BaseBoolType, SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymExpr sym BaseBoolType, SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
    subSignedOF sym
    sym SymBV sym w
    x SymBV sym w
    y
      SymExpr sym BaseBoolType
    ysign  <- sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (Pred sym)
    bvIsNeg sym
    sym SymBV sym w
    y
      SymBV sym w
    minint <- sym -> NatRepr w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    minSignedBV sym
    sym NatRepr w
    w
      SymBV sym w
    maxint <- sym -> NatRepr w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    maxSignedBV sym
    sym NatRepr w
    w
      SymBV sym w
    ov_val <- sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvIte sym
    sym SymExpr sym BaseBoolType
    ysign SymBV sym w
    maxint SymBV sym w
    minint
      sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvIte sym
    sym SymExpr sym BaseBoolType
    ov SymBV sym w
    ov_val SymBV sym w
    xy

    clampedIntMul :: (IsExprBuilder sym, 1 <= w)
                  => sym
                  -> SymBV sym w
                  -> SymBV sym w
                  -> IO (SymBV sym w)
    clampedIntMul :: forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    clampedIntMul sym
    sym SymBV sym w
    x SymBV sym w
    y = do
      let w :: NatRepr w
    w = SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    bvWidth SymBV sym w
    x
      (SymBV sym w
    hi,SymBV sym w
    lo) <- sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
    signedWideMultiplyBV sym
    sym SymBV sym w
    x SymBV sym w
    y
      SymBV sym w
    zro    <- sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    bvLit sym
    sym NatRepr w
    w (NatRepr w -> BV w
    forall (w :: Natural). NatRepr w -> BV w
    BV.zero NatRepr w
    w)
      SymBV sym w
    ones   <- sym -> NatRepr w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    maxUnsignedBV sym
    sym NatRepr w
    w
      SymExpr sym BaseBoolType
    ok_pos <- IO (IO (SymExpr sym BaseBoolType)) -> IO (SymExpr sym BaseBoolType)
    forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
    join (IO (IO (SymExpr sym BaseBoolType))
     -> IO (SymExpr sym BaseBoolType))
    -> IO (IO (SymExpr sym BaseBoolType))
    -> IO (SymExpr sym BaseBoolType)
    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)
    andPred sym
    sym (SymExpr sym BaseBoolType
     -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
    -> IO (SymExpr sym BaseBoolType)
    -> IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    notPred sym
    sym (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
    -> IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (Pred sym)
    bvIsNeg sym
    sym SymBV sym w
    lo)
                                  IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
    -> IO (SymExpr sym BaseBoolType)
    -> IO (IO (SymExpr sym BaseBoolType))
    forall a b. IO (a -> b) -> IO a -> IO b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    bvEq sym
    sym SymBV sym w
    hi SymBV sym w
    zro
      SymExpr sym BaseBoolType
    ok_neg <- IO (IO (SymExpr sym BaseBoolType)) -> IO (SymExpr sym BaseBoolType)
    forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
    join (IO (IO (SymExpr sym BaseBoolType))
     -> IO (SymExpr sym BaseBoolType))
    -> IO (IO (SymExpr sym BaseBoolType))
    -> IO (SymExpr sym BaseBoolType)
    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)
    andPred sym
    sym (SymExpr sym BaseBoolType
     -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
    -> IO (SymExpr sym BaseBoolType)
    -> IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (Pred sym)
    bvIsNeg sym
    sym SymBV sym w
    lo
                                  IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
    -> IO (SymExpr sym BaseBoolType)
    -> IO (IO (SymExpr sym BaseBoolType))
    forall a b. IO (a -> b) -> IO a -> IO b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    bvEq sym
    sym SymBV sym w
    hi SymBV sym w
    ones
      SymExpr sym BaseBoolType
    ov     <- sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    notPred sym
    sym (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
    -> IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym
    -> SymExpr sym BaseBoolType
    -> SymExpr sym BaseBoolType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    orPred sym
    sym SymExpr sym BaseBoolType
    ok_pos SymExpr sym BaseBoolType
    ok_neg

      SymBV sym w
    minint <- sym -> NatRepr w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    minSignedBV sym
    sym NatRepr w
    w
      SymBV sym w
    maxint <- sym -> NatRepr w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    maxSignedBV sym
    sym NatRepr w
    w
      SymExpr sym BaseBoolType
    hisign <- sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (Pred sym)
    bvIsNeg sym
    sym SymBV sym w
    hi
      SymBV sym w
    ov_val <- sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvIte sym
    sym SymExpr sym BaseBoolType
    hisign SymBV sym w
    minint SymBV sym w
    maxint
      sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvIte sym
    sym SymExpr sym BaseBoolType
    ov SymBV sym w
    ov_val SymBV sym w
    lo

    -- | Compute the clamped negation of a signed bitvector.
    --
    --   The only difference between this operation and the usual
    --   2's complement negation function is the handling of MIN_INT.
    --   The usual 2's complement negation sends MIN_INT to MIN_INT;
    --   however, the clamped version instead sends MIN_INT to MAX_INT.
    clampedIntNeg :: (IsExprBuilder sym, 1 <= w)
                  => sym
                  -> SymBV sym w
                  -> IO (SymBV sym w)
    clampedIntNeg :: forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    clampedIntNeg sym
    sym SymBV sym w
    x = do
      let w :: NatRepr w
    w = SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    bvWidth SymBV sym w
    x
      SymBV sym w
    minint <- sym -> NatRepr w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    minSignedBV sym
    sym NatRepr w
    w

      -- return maxint when x == minint, and neg(x) otherwise
      SymExpr sym BaseBoolType
    p <- sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    bvEq sym
    sym SymBV sym w
    x SymBV sym w
    minint
      (sym
     -> SymExpr sym BaseBoolType
     -> SymBV sym w
     -> SymBV sym w
     -> IO (SymBV sym w))
    -> sym
    -> SymExpr sym BaseBoolType
    -> IO (SymBV sym w)
    -> IO (SymBV sym w)
    -> IO (SymBV sym w)
    forall sym v.
    IsExprBuilder sym =>
    (sym -> Pred sym -> v -> v -> IO v)
    -> sym -> Pred sym -> IO v -> IO v -> IO v
    iteM sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvIte sym
    sym SymExpr sym BaseBoolType
    p (sym -> NatRepr w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    maxSignedBV sym
    sym NatRepr w
    w) (sym -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    bvNeg sym
    sym SymBV sym w
    x)

    -- | Compute the clamped absolute value of a signed bitvector.
    --
    --   The only difference between this operation and the usual 2's
    --   complement operation is the handling of MIN_INT.  The usual 2's
    --   complement absolute value function sends MIN_INT to MIN_INT;
    --   however, the clamped version instead sends MIN_INT to MAX_INT.
    clampedIntAbs :: (IsExprBuilder sym, 1 <= w)
                  => sym
                  -> SymBV sym w
                  -> IO (SymBV sym w)
    clampedIntAbs :: forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    clampedIntAbs sym
    sym SymBV sym w
    x = do
      SymExpr sym BaseBoolType
    isNeg  <- sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (Pred sym)
    bvIsNeg sym
    sym SymBV sym w
    x
      (sym
     -> SymExpr sym BaseBoolType
     -> SymBV sym w
     -> SymBV sym w
     -> IO (SymBV sym w))
    -> sym
    -> SymExpr sym BaseBoolType
    -> IO (SymBV sym w)
    -> IO (SymBV sym w)
    -> IO (SymBV sym w)
    forall sym v.
    IsExprBuilder sym =>
    (sym -> Pred sym -> v -> v -> IO v)
    -> sym -> Pred sym -> IO v -> IO v -> IO v
    iteM sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvIte sym
    sym SymExpr sym BaseBoolType
    isNeg (sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    clampedIntNeg sym
    sym SymBV sym w
    x) (SymBV sym w -> IO (SymBV sym w)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure SymBV sym w
    x)

    clampedUIntAdd :: (IsExprBuilder sym, 1 <= w)
                   => sym
                   -> SymBV sym w
                   -> SymBV sym w
                   -> IO (SymBV sym w)
    clampedUIntAdd :: forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    clampedUIntAdd sym
    sym SymBV sym w
    x SymBV sym w
    y = do
      let w :: NatRepr w
    w = SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    bvWidth SymBV sym w
    x
      (SymExpr sym BaseBoolType
    ov, SymBV sym w
    xy) <- sym
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymExpr sym BaseBoolType, SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymExpr sym BaseBoolType, SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
    addUnsignedOF sym
    sym SymBV sym w
    x SymBV sym w
    y
      SymBV sym w
    maxint   <- sym -> NatRepr w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    maxUnsignedBV sym
    sym NatRepr w
    w
      sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvIte sym
    sym SymExpr sym BaseBoolType
    ov SymBV sym w
    maxint SymBV sym w
    xy

    clampedUIntSub :: (IsExprBuilder sym, 1 <= w)
                   => sym
                   -> SymBV sym w
                   -> SymBV sym w
                   -> IO (SymBV sym w)
    clampedUIntSub :: forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    clampedUIntSub sym
    sym SymBV sym w
    x SymBV sym w
    y = do
      let w :: NatRepr w
    w = SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    bvWidth SymBV sym w
    x
      SymExpr sym BaseBoolType
    no_underflow <- sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
    bvUge sym
    sym SymBV sym w
    x SymBV sym w
    y

      (sym
     -> SymExpr sym BaseBoolType
     -> SymBV sym w
     -> SymBV sym w
     -> IO (SymBV sym w))
    -> sym
    -> SymExpr sym BaseBoolType
    -> IO (SymBV sym w)
    -> IO (SymBV sym w)
    -> IO (SymBV sym w)
    forall sym v.
    IsExprBuilder sym =>
    (sym -> Pred sym -> v -> v -> IO v)
    -> sym -> Pred sym -> IO v -> IO v -> IO v
    iteM sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvIte
           sym
    sym
           SymExpr sym BaseBoolType
    no_underflow
           (sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvSub sym
    sym SymBV sym w
    x SymBV sym w
    y) -- Perform subtraction if y >= x
           (sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> BV w -> IO (SymBV sym w)
    bvLit sym
    sym NatRepr w
    w (NatRepr w -> BV w
    forall (w :: Natural). NatRepr w -> BV w
    BV.zero NatRepr w
    w)) -- Otherwise return min int

    clampedUIntMul :: (IsExprBuilder sym, 1 <= w)
                   => sym
                   -> SymBV sym w
                   -> SymBV sym w
                   -> IO (SymBV sym w)
    clampedUIntMul :: forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    clampedUIntMul sym
    sym SymBV sym w
    x SymBV sym w
    y = do
      let w :: NatRepr w
    w = SymBV sym w -> NatRepr w
    forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    bvWidth SymBV sym w
    x
      (SymBV sym w
    hi, SymBV sym w
    lo) <- sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
    unsignedWideMultiplyBV sym
    sym SymBV sym w
    x SymBV sym w
    y
      SymBV sym w
    maxint   <- sym -> NatRepr w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> NatRepr w -> IO (SymBV sym w)
    maxUnsignedBV sym
    sym NatRepr w
    w
      SymExpr sym BaseBoolType
    ov       <- sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (Pred sym)
    bvIsNonzero sym
    sym SymBV sym w
    hi
      sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym
    -> SymExpr sym BaseBoolType
    -> SymBV sym w
    -> SymBV sym w
    -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    bvIte sym
    sym SymExpr sym BaseBoolType
    ov SymBV sym w
    maxint SymBV sym w
    lo

    ------------------------------------------------------------------------
    -- MatlabSolverFn

    -- | Builtin functions that can be used to generate symbolic functions.
    --
    -- These functions are expected to be total, but the value returned may not be
    -- specified.  e.g. 'IntegerToNatFn' must return some natural number for every
    -- integer, but for negative integers, the particular number is unspecified.
    data MatlabSolverFn (f :: BaseType -> Type) args ret where

      -- Or two Boolean variables
      BoolOrFn :: MatlabSolverFn f (EmptyCtx ::> BaseBoolType ::> BaseBoolType) BaseBoolType

      -- Returns true if the real value is an integer.
      IsIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType

      -- Return true if first value is less than or equal to second.
      IntLeFn :: MatlabSolverFn f (EmptyCtx ::> BaseIntegerType ::> BaseIntegerType) BaseBoolType

      -- A function for mapping a unsigned bitvector to an integer.
      BVToIntegerFn :: (1 <= w)
                => !(NatRepr w)
                ->  MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
      -- A function for mapping a signed bitvector to a integer.
      SBVToIntegerFn :: (1 <= w)
                     => !(NatRepr w)
                     -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType

      -- A function for mapping an integer to equivalent real.
      IntegerToRealFn :: MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType

      -- A function for mapping a real to equivalent integer.
      --
      -- Function may return any value if input is not an integer.
      RealToIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseIntegerType

      -- A function that maps Booleans logical value to an integer
      -- (either 0 for false, or 1 for true)
      PredToIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType

      -- 'IntSeqFn base c' denotes the function '\i _ -> base + c*i
      IntSeqFn :: !(f BaseIntegerType)
               -> !(f BaseIntegerType)
               -> MatlabSolverFn f (EmptyCtx ::> BaseIntegerType ::> BaseIntegerType) BaseIntegerType

      -- 'RealSeqFn base c' denotes the function '\_ i -> base + c*i
      RealSeqFn :: !(f BaseRealType)
                -> !(f BaseRealType)
                -> MatlabSolverFn f (EmptyCtx ::> BaseIntegerType ::> BaseIntegerType) BaseRealType

      -- 'IndicesInRange tps upper_bounds' returns a predicate that is true if all the arguments
      -- (which must be natural numbers) are between 1 and the given upper bounds (inclusive).
      IndicesInRange :: !(Assignment OnlyIntRepr (idx ::> itp))
                     -> !(Assignment f (idx ::> itp))
                        -- Upper bounds on indices
                     -> MatlabSolverFn f (idx ::> itp) BaseBoolType

      IsEqFn :: !(BaseTypeRepr tp)
             -> MatlabSolverFn f (EmptyCtx ::> tp ::> tp) BaseBoolType

      ------------------------------------------------------------------------
      -- Bitvector functions

      -- Returns true if the bitvector is non-zero.
      BVIsNonZeroFn :: (1 <= w)
                    => !(NatRepr w)
                    -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseBoolType

      -- Negate a signed bitvector
      ClampedIntNegFn :: (1 <= w)
               => !(NatRepr w)
               -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)

      -- Get absolute value of a signed bitvector
      ClampedIntAbsFn :: (1 <= w)
             => !(NatRepr w)
             -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)

      -- Add two values without wrapping but rather rounding to
      -- 0/max value when the result is out of range.
      ClampedIntAddFn :: (1 <= w)
               => !(NatRepr w)
               -> MatlabSolverFn f
                     (EmptyCtx ::> BaseBVType w ::> BaseBVType w)
                     (BaseBVType w)

      -- Subtract one value from another without wrapping but rather rounding to
      -- 0/max value when the result is out of range.
      ClampedIntSubFn :: (1 <= w)
               => !(NatRepr w)
               -> MatlabSolverFn f
                     (EmptyCtx ::> BaseBVType w ::> BaseBVType w)
                     (BaseBVType w)

      -- Multiple two values without wrapping but rather rounding to
      -- 0/max value when the result is out of range.
      ClampedIntMulFn :: (1 <= w)
               => !(NatRepr w)
               -> MatlabSolverFn f
                     (EmptyCtx ::> BaseBVType w ::> BaseBVType w)
                     (BaseBVType w)

      -- Add two values without wrapping but rather rounding to
      -- 0/max value when the result is out of range.
      ClampedUIntAddFn :: (1 <= w)
               => !(NatRepr w)
               -> MatlabSolverFn f
                     (EmptyCtx ::> BaseBVType w ::> BaseBVType w)
                     (BaseBVType w)

      -- Subtract one value from another without wrapping but rather rounding to
      -- 0/max value when the result is out of range.
      ClampedUIntSubFn :: (1 <= w)
               => !(NatRepr w)
               -> MatlabSolverFn f
                     (EmptyCtx ::> BaseBVType w ::> BaseBVType w)
                     (BaseBVType w)

      -- Multiple two values without wrapping but rather rounding to
      -- 0/max value when the result is out of range.
      ClampedUIntMulFn :: (1 <= w)
               => !(NatRepr w)
               -> MatlabSolverFn f
                     (EmptyCtx ::> BaseBVType w ::> BaseBVType w)
                     (BaseBVType w)

      -- Convert a signed integer to the nearest signed integer with the
      -- given width.  This clamps the value to min-int or max int when truncated
      -- the width.
      IntSetWidthFn :: (1 <= m, 1 <= n)
                    => !(NatRepr m)
                    -> !(NatRepr n)
                    -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)

      -- Convert a unsigned integer to the nearest unsigned integer with the
      -- given width.  This clamps the value to min-int or max int when truncated
      -- the width.
      UIntSetWidthFn :: (1 <= m, 1 <= n)
                     => !(NatRepr m)
                     -> !(NatRepr n)
                     -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)

      -- Convert a unsigned integer to the nearest signed integer with the
      -- given width.  This clamps the value to min-int or max int when truncated
      -- the width.
      UIntToIntFn :: (1 <= m, 1 <= n)
                    => !(NatRepr m)
                    -> !(NatRepr n)
                    -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)

      -- Convert a signed integer to the nearest unsigned integer with the
      -- given width.  This clamps the value to min-int or max int when truncated
      -- the width.
      IntToUIntFn :: (1 <= m, 1 <= n)
                  => !(NatRepr m)
                  -> !(NatRepr n)
                  -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)

      ------------------------------------------------------------------------
      -- Real functions

      -- Returns true if the complex number is non-zero.
      RealIsNonZeroFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType

      RealCosFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseRealType
      RealSinFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseRealType

      ------------------------------------------------------------------------
      -- Conversion functions

      RealToSBVFn :: (1 <= w)
                  => !(NatRepr w)
                  -> MatlabSolverFn f (EmptyCtx ::> BaseRealType) (BaseBVType w)

      RealToUBVFn :: (1 <= w)
                  => !(NatRepr w)
                  -> MatlabSolverFn f (EmptyCtx ::> BaseRealType) (BaseBVType w)

      -- Return 1 if the predicate is true; 0 otherwise.
      PredToBVFn :: (1 <= w)
                 => !(NatRepr w)
                 -> MatlabSolverFn f (EmptyCtx ::> BaseBoolType) (BaseBVType w)

      ------------------------------------------------------------------------
      -- Complex functions

      -- Returns true if the complex number is non-zero.
      CplxIsNonZeroFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseBoolType

      -- Returns true if the imaginary part of complex number is zero.
      CplxIsRealFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseBoolType

      -- A function for mapping a real to equivalent complex with imaginary number equals 0.
      RealToComplexFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseComplexType
      -- Returns the real component out of a complex number.
      RealPartOfCplxFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType
      -- Returns the imag component out of a complex number.
      ImagPartOfCplxFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType

      -- Return the complex number formed by negating both components.
      CplxNegFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType

      -- Add two complex values.
      CplxAddFn :: MatlabSolverFn f
                     (EmptyCtx ::> BaseComplexType ::> BaseComplexType)
                     BaseComplexType

      -- Subtract one complex value from another.
      CplxSubFn :: MatlabSolverFn f
                     (EmptyCtx ::> BaseComplexType ::> BaseComplexType)
                     BaseComplexType

      -- Multiply two complex values.
      CplxMulFn :: MatlabSolverFn f
                     (EmptyCtx ::> BaseComplexType ::> BaseComplexType)
                     BaseComplexType

      -- Return the complex number formed by rounding both components.
      --
      -- Rounding is away from zero.
      CplxRoundFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
      -- Return the complex number formed by taking floor of both components.
      CplxFloorFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
      -- Return the complex number formed by taking ceiling of both components.
      CplxCeilFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType

      -- Return magningture of complex number.
      CplxMagFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType

      -- Return the principal square root of a complex number.
      CplxSqrtFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType

      -- Returns complex exponential of input
      CplxExpFn :: MatlabSolverFn f
                     (EmptyCtx ::> BaseComplexType)
                     BaseComplexType
      -- Returns complex natural logarithm of input
      CplxLogFn :: MatlabSolverFn f
                     (EmptyCtx ::> BaseComplexType)
                     BaseComplexType
      -- Returns complex natural logarithm of input
      CplxLogBaseFn :: !Integer
                    -> MatlabSolverFn f
                         (EmptyCtx ::> BaseComplexType)
                         BaseComplexType
      -- Returns complex sine of input
      CplxSinFn :: MatlabSolverFn f
                     (EmptyCtx ::> BaseComplexType)
                     BaseComplexType
      -- Returns complex cosine of input
      CplxCosFn :: MatlabSolverFn f
                     (EmptyCtx ::> BaseComplexType)
                     BaseComplexType
      -- Returns tangent of input.
      --
      CplxTanFn :: MatlabSolverFn f
                     (EmptyCtx ::> BaseComplexType)
                     BaseComplexType

    -- Dummy declaration splice to bring App into template haskell scope.
    $(return [])

    traverseMatlabSolverFn :: Applicative m
                           => (forall tp . e tp -> m (f tp))
                           -> MatlabSolverFn e a r
                           -> m (MatlabSolverFn f a r)
    traverseMatlabSolverFn :: forall (m :: Type -> Type) (e :: BaseType -> Type)
           (f :: BaseType -> Type) (a :: Ctx BaseType) (r :: BaseType).
    Applicative m =>
    (forall (tp :: BaseType). e tp -> m (f tp))
    -> MatlabSolverFn e a r -> m (MatlabSolverFn f a r)
    traverseMatlabSolverFn forall (tp :: BaseType). e tp -> m (f tp)
    f MatlabSolverFn e a r
    fn_id =
      case MatlabSolverFn e a r
    fn_id of
        MatlabSolverFn e a r
    BoolOrFn             -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn
      f ((EmptyCtx ::> BaseBoolType) '::> BaseBoolType) BaseBoolType
    forall (f :: BaseType -> Type).
    MatlabSolverFn
      f ((EmptyCtx ::> BaseBoolType) '::> BaseBoolType) BaseBoolType
    BoolOrFn
        MatlabSolverFn e a r
    IsIntegerFn          -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseBoolType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseBoolType
    IsIntegerFn
        MatlabSolverFn e a r
    IntLeFn              -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn
      f
      ((EmptyCtx ::> BaseIntegerType) '::> BaseIntegerType)
      BaseBoolType
    forall (f :: BaseType -> Type).
    MatlabSolverFn
      f
      ((EmptyCtx ::> BaseIntegerType) '::> BaseIntegerType)
      BaseBoolType
    IntLeFn
        BVToIntegerFn NatRepr w
    w      -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn f (EmptyCtx '::> BaseBVType w) BaseIntegerType
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
    BVToIntegerFn NatRepr w
    w
        SBVToIntegerFn NatRepr w
    w     -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn f (EmptyCtx '::> BaseBVType w) BaseIntegerType
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
    SBVToIntegerFn NatRepr w
    w
        MatlabSolverFn e a r
    IntegerToRealFn      -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType
    IntegerToRealFn
        MatlabSolverFn e a r
    RealToIntegerFn      -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseIntegerType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseIntegerType
    RealToIntegerFn
        MatlabSolverFn e a r
    PredToIntegerFn      -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType
    PredToIntegerFn
        IntSeqFn  e BaseIntegerType
    b e BaseIntegerType
    i        -> f BaseIntegerType -> f BaseIntegerType -> MatlabSolverFn f a r
    f BaseIntegerType
    -> f BaseIntegerType
    -> MatlabSolverFn
         f
         ((EmptyCtx ::> BaseIntegerType) '::> BaseIntegerType)
         BaseIntegerType
    forall (f :: BaseType -> Type).
    f BaseIntegerType
    -> f BaseIntegerType
    -> MatlabSolverFn
         f
         ((EmptyCtx ::> BaseIntegerType) '::> BaseIntegerType)
         BaseIntegerType
    IntSeqFn (f BaseIntegerType -> f BaseIntegerType -> MatlabSolverFn f a r)
    -> m (f BaseIntegerType)
    -> m (f BaseIntegerType -> MatlabSolverFn f a r)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> e BaseIntegerType -> m (f BaseIntegerType)
    forall (tp :: BaseType). e tp -> m (f tp)
    f e BaseIntegerType
    b m (f BaseIntegerType -> MatlabSolverFn f a r)
    -> m (f BaseIntegerType) -> m (MatlabSolverFn f a r)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> e BaseIntegerType -> m (f BaseIntegerType)
    forall (tp :: BaseType). e tp -> m (f tp)
    f e BaseIntegerType
    i
        RealSeqFn e BaseRealType
    b e BaseRealType
    i        -> f BaseRealType -> f BaseRealType -> MatlabSolverFn f a r
    f BaseRealType
    -> f BaseRealType
    -> MatlabSolverFn
         f
         ((EmptyCtx ::> BaseIntegerType) '::> BaseIntegerType)
         BaseRealType
    forall (f :: BaseType -> Type).
    f BaseRealType
    -> f BaseRealType
    -> MatlabSolverFn
         f
         ((EmptyCtx ::> BaseIntegerType) '::> BaseIntegerType)
         BaseRealType
    RealSeqFn (f BaseRealType -> f BaseRealType -> MatlabSolverFn f a r)
    -> m (f BaseRealType) -> m (f BaseRealType -> MatlabSolverFn f a r)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> e BaseRealType -> m (f BaseRealType)
    forall (tp :: BaseType). e tp -> m (f tp)
    f e BaseRealType
    b m (f BaseRealType -> MatlabSolverFn f a r)
    -> m (f BaseRealType) -> m (MatlabSolverFn f a r)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> e BaseRealType -> m (f BaseRealType)
    forall (tp :: BaseType). e tp -> m (f tp)
    f e BaseRealType
    i
        IndicesInRange Assignment OnlyIntRepr (idx '::> itp)
    tps Assignment e (idx '::> itp)
    a -> Assignment OnlyIntRepr (idx '::> itp)
    -> Assignment f (idx '::> itp)
    -> MatlabSolverFn f (idx '::> itp) BaseBoolType
    forall (w :: Ctx BaseType) (n :: BaseType) (f :: BaseType -> Type).
    Assignment OnlyIntRepr (w ::> n)
    -> Assignment f (w ::> n)
    -> MatlabSolverFn f (w ::> n) BaseBoolType
    IndicesInRange Assignment OnlyIntRepr (idx '::> itp)
    tps (Assignment f (idx '::> itp) -> MatlabSolverFn f a r)
    -> m (Assignment f (idx '::> itp)) -> m (MatlabSolverFn f a r)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (forall (tp :: BaseType). e tp -> m (f tp))
    -> forall (x :: Ctx BaseType). Assignment e x -> m (Assignment f x)
    forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
           (g :: k -> Type) (m :: Type -> Type).
    (TraversableFC t, Applicative m) =>
    (forall (x :: k). f x -> m (g x))
    -> forall (x :: l). t f x -> m (t g x)
    forall (f :: BaseType -> Type) (g :: BaseType -> Type)
           (m :: Type -> Type).
    Applicative m =>
    (forall (x :: BaseType). f x -> m (g x))
    -> forall (x :: Ctx BaseType). Assignment f x -> m (Assignment g x)
    traverseFC e x -> m (f x)
    forall (tp :: BaseType). e tp -> m (f tp)
    f Assignment e (idx '::> itp)
    a
        IsEqFn BaseTypeRepr tp
    tp            -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ BaseTypeRepr tp
    -> MatlabSolverFn f ((EmptyCtx ::> tp) '::> tp) BaseBoolType
    forall (w :: BaseType) (f :: BaseType -> Type).
    BaseTypeRepr w
    -> MatlabSolverFn f ((EmptyCtx ::> w) ::> w) BaseBoolType
    IsEqFn BaseTypeRepr tp
    tp

        BVIsNonZeroFn NatRepr w
    w      -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn f (EmptyCtx '::> BaseBVType w) BaseBoolType
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseBoolType
    BVIsNonZeroFn NatRepr w
    w

        ClampedIntNegFn NatRepr w
    w    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn f (EmptyCtx '::> BaseBVType w) (BaseBVType w)
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)
    ClampedIntNegFn NatRepr w
    w
        ClampedIntAbsFn NatRepr w
    w    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn f (EmptyCtx '::> BaseBVType w) (BaseBVType w)
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)
    ClampedIntAbsFn NatRepr w
    w
        ClampedIntAddFn NatRepr w
    w    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn
         f ((EmptyCtx ::> BaseBVType w) '::> BaseBVType w) (BaseBVType w)
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn
         f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
    ClampedIntAddFn NatRepr w
    w
        ClampedIntSubFn NatRepr w
    w    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn
         f ((EmptyCtx ::> BaseBVType w) '::> BaseBVType w) (BaseBVType w)
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn
         f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
    ClampedIntSubFn NatRepr w
    w
        ClampedIntMulFn NatRepr w
    w    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn
         f ((EmptyCtx ::> BaseBVType w) '::> BaseBVType w) (BaseBVType w)
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn
         f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
    ClampedIntMulFn NatRepr w
    w

        ClampedUIntAddFn NatRepr w
    w   -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn
         f ((EmptyCtx ::> BaseBVType w) '::> BaseBVType w) (BaseBVType w)
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn
         f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
    ClampedUIntAddFn NatRepr w
    w
        ClampedUIntSubFn NatRepr w
    w   -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn
         f ((EmptyCtx ::> BaseBVType w) '::> BaseBVType w) (BaseBVType w)
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn
         f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
    ClampedUIntSubFn NatRepr w
    w
        ClampedUIntMulFn NatRepr w
    w   -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn
         f ((EmptyCtx ::> BaseBVType w) '::> BaseBVType w) (BaseBVType w)
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn
         f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
    ClampedUIntMulFn NatRepr w
    w

        IntSetWidthFn NatRepr m
    i NatRepr n
    o    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr m
    -> NatRepr n
    -> MatlabSolverFn f (EmptyCtx '::> BaseBVType m) ('BaseBVType n)
    forall (w :: Natural) (n :: Natural) (f :: BaseType -> Type).
    (1 <= w, 1 <= n) =>
    NatRepr w
    -> NatRepr n
    -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType n)
    IntSetWidthFn NatRepr m
    i NatRepr n
    o
        UIntSetWidthFn NatRepr m
    i NatRepr n
    o   -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr m
    -> NatRepr n
    -> MatlabSolverFn f (EmptyCtx '::> BaseBVType m) ('BaseBVType n)
    forall (w :: Natural) (n :: Natural) (f :: BaseType -> Type).
    (1 <= w, 1 <= n) =>
    NatRepr w
    -> NatRepr n
    -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType n)
    UIntSetWidthFn NatRepr m
    i NatRepr n
    o
        UIntToIntFn NatRepr m
    i NatRepr n
    o      -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr m
    -> NatRepr n
    -> MatlabSolverFn f (EmptyCtx '::> BaseBVType m) ('BaseBVType n)
    forall (w :: Natural) (n :: Natural) (f :: BaseType -> Type).
    (1 <= w, 1 <= n) =>
    NatRepr w
    -> NatRepr n
    -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType n)
    UIntToIntFn NatRepr m
    i NatRepr n
    o
        IntToUIntFn NatRepr m
    i NatRepr n
    o      -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr m
    -> NatRepr n
    -> MatlabSolverFn f (EmptyCtx '::> BaseBVType m) ('BaseBVType n)
    forall (w :: Natural) (n :: Natural) (f :: BaseType -> Type).
    (1 <= w, 1 <= n) =>
    NatRepr w
    -> NatRepr n
    -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType n)
    IntToUIntFn NatRepr m
    i NatRepr n
    o

        MatlabSolverFn e a r
    RealCosFn            -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseRealType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseRealType
    RealCosFn
        MatlabSolverFn e a r
    RealSinFn            -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseRealType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseRealType
    RealSinFn
        MatlabSolverFn e a r
    RealIsNonZeroFn      -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseBoolType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseBoolType
    RealIsNonZeroFn

        RealToSBVFn NatRepr w
    w        -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn f (EmptyCtx '::> BaseRealType) ('BaseBVType w)
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn f (EmptyCtx '::> BaseRealType) (BaseBVType w)
    RealToSBVFn NatRepr w
    w
        RealToUBVFn NatRepr w
    w        -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn f (EmptyCtx '::> BaseRealType) ('BaseBVType w)
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn f (EmptyCtx '::> BaseRealType) (BaseBVType w)
    RealToUBVFn NatRepr w
    w
        PredToBVFn  NatRepr w
    w        -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ NatRepr w
    -> MatlabSolverFn f (EmptyCtx ::> BaseBoolType) ('BaseBVType w)
    forall (w :: Natural) (f :: BaseType -> Type).
    (1 <= w) =>
    NatRepr w
    -> MatlabSolverFn f (EmptyCtx ::> BaseBoolType) (BaseBVType w)
    PredToBVFn  NatRepr w
    w

        MatlabSolverFn e a r
    CplxIsNonZeroFn      -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseBoolType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseBoolType
    CplxIsNonZeroFn
        MatlabSolverFn e a r
    CplxIsRealFn         -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseBoolType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseBoolType
    CplxIsRealFn
        MatlabSolverFn e a r
    RealToComplexFn      -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseComplexType
    RealToComplexFn
        MatlabSolverFn e a r
    RealPartOfCplxFn     -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseRealType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseRealType
    RealPartOfCplxFn
        MatlabSolverFn e a r
    ImagPartOfCplxFn     -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseRealType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseRealType
    ImagPartOfCplxFn
        MatlabSolverFn e a r
    CplxNegFn            -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    CplxNegFn
        MatlabSolverFn e a r
    CplxAddFn            -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn
      f
      ((EmptyCtx '::> BaseComplexType) '::> BaseComplexType)
      BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn
      f
      ((EmptyCtx '::> BaseComplexType) '::> BaseComplexType)
      BaseComplexType
    CplxAddFn
        MatlabSolverFn e a r
    CplxSubFn            -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn
      f
      ((EmptyCtx '::> BaseComplexType) '::> BaseComplexType)
      BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn
      f
      ((EmptyCtx '::> BaseComplexType) '::> BaseComplexType)
      BaseComplexType
    CplxSubFn
        MatlabSolverFn e a r
    CplxMulFn            -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn
      f
      ((EmptyCtx '::> BaseComplexType) '::> BaseComplexType)
      BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn
      f
      ((EmptyCtx '::> BaseComplexType) '::> BaseComplexType)
      BaseComplexType
    CplxMulFn
        MatlabSolverFn e a r
    CplxRoundFn          -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    CplxRoundFn
        MatlabSolverFn e a r
    CplxFloorFn          -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    CplxFloorFn
        MatlabSolverFn e a r
    CplxCeilFn           -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    CplxCeilFn
        MatlabSolverFn e a r
    CplxMagFn            -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseRealType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseRealType
    CplxMagFn
        MatlabSolverFn e a r
    CplxSqrtFn           -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    CplxSqrtFn
        MatlabSolverFn e a r
    CplxExpFn            -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    CplxExpFn
        MatlabSolverFn e a r
    CplxLogFn            -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    CplxLogFn
        CplxLogBaseFn Integer
    b      -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ Integer
    -> MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    forall (f :: BaseType -> Type).
    Integer
    -> MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    CplxLogBaseFn Integer
    b
        MatlabSolverFn e a r
    CplxSinFn            -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    CplxSinFn
        MatlabSolverFn e a r
    CplxCosFn            -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    CplxCosFn
        MatlabSolverFn e a r
    CplxTanFn            -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a. a -> m a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (MatlabSolverFn f a r -> m (MatlabSolverFn f a r))
    -> MatlabSolverFn f a r -> m (MatlabSolverFn f a r)
    forall a b. (a -> b) -> a -> b
    $ MatlabSolverFn f a r
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    forall (f :: BaseType -> Type).
    MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
    CplxTanFn

    -- | Utilities to make a pair with the same value.
    binCtx :: BaseTypeRepr tp -> Ctx.Assignment BaseTypeRepr (EmptyCtx ::> tp ::> tp)
    binCtx :: forall (tp :: BaseType).
    BaseTypeRepr tp
    -> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
    binCtx BaseTypeRepr tp
    tp = Assignment BaseTypeRepr EmptyCtx
    forall {k} (f :: k -> Type). Assignment f EmptyCtx
    Ctx.empty Assignment BaseTypeRepr EmptyCtx
    -> BaseTypeRepr tp -> Assignment BaseTypeRepr (EmptyCtx ::> tp)
    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.:> BaseTypeRepr tp
    tp Assignment BaseTypeRepr (EmptyCtx ::> tp)
    -> BaseTypeRepr tp
    -> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
    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.:> BaseTypeRepr tp
    tp

    -- | Get arg tpyes of solver fn.
    matlabSolverArgTypes :: MatlabSolverFn f args ret -> Assignment BaseTypeRepr args
    matlabSolverArgTypes :: forall (f :: BaseType -> Type) (args :: Ctx BaseType)
           (ret :: BaseType).
    MatlabSolverFn f args ret -> Assignment BaseTypeRepr args
    matlabSolverArgTypes MatlabSolverFn f args ret
    f =
      case MatlabSolverFn f args ret
    f of
        MatlabSolverFn f args ret
    BoolOrFn             -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    IsIntegerFn          -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    IntLeFn              -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        BVToIntegerFn NatRepr w
    w      -> BaseTypeRepr (BaseBVType w)
    -> Assignment BaseTypeRepr (EmptyCtx '::> BaseBVType w)
    forall {k} (f :: k -> Type) (tp :: k).
    f tp -> Assignment f (EmptyCtx ::> tp)
    Ctx.singleton (NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w)
        SBVToIntegerFn NatRepr w
    w     -> BaseTypeRepr (BaseBVType w)
    -> Assignment BaseTypeRepr (EmptyCtx '::> BaseBVType w)
    forall {k} (f :: k -> Type) (tp :: k).
    f tp -> Assignment f (EmptyCtx ::> tp)
    Ctx.singleton (NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w)
        MatlabSolverFn f args ret
    IntegerToRealFn      -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    RealToIntegerFn      -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    PredToIntegerFn      -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        IntSeqFn{}           -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        IndicesInRange Assignment OnlyIntRepr (idx '::> itp)
    tps Assignment f (idx '::> itp)
    _ -> (forall (x :: BaseType). OnlyIntRepr x -> BaseTypeRepr x)
    -> forall (x :: Ctx BaseType).
       Assignment OnlyIntRepr x -> Assignment BaseTypeRepr x
    forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
           (g :: k -> Type).
    FunctorFC t =>
    (forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
    forall (f :: BaseType -> Type) (g :: BaseType -> Type).
    (forall (x :: BaseType). f x -> g x)
    -> forall (x :: Ctx BaseType). Assignment f x -> Assignment g x
    fmapFC OnlyIntRepr x -> BaseTypeRepr x
    forall (x :: BaseType). OnlyIntRepr x -> BaseTypeRepr x
    toBaseTypeRepr Assignment OnlyIntRepr args
    Assignment OnlyIntRepr (idx '::> itp)
    tps
        RealSeqFn f BaseRealType
    _ f BaseRealType
    _        -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        IsEqFn BaseTypeRepr tp
    tp            -> BaseTypeRepr tp
    -> Assignment BaseTypeRepr ((EmptyCtx ::> tp) '::> tp)
    forall (tp :: BaseType).
    BaseTypeRepr tp
    -> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
    binCtx BaseTypeRepr tp
    tp

        BVIsNonZeroFn NatRepr w
    w      -> BaseTypeRepr (BaseBVType w)
    -> Assignment BaseTypeRepr (EmptyCtx '::> BaseBVType w)
    forall {k} (f :: k -> Type) (tp :: k).
    f tp -> Assignment f (EmptyCtx ::> tp)
    Ctx.singleton (NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w)
        ClampedIntNegFn NatRepr w
    w    -> BaseTypeRepr (BaseBVType w)
    -> Assignment BaseTypeRepr (EmptyCtx '::> BaseBVType w)
    forall {k} (f :: k -> Type) (tp :: k).
    f tp -> Assignment f (EmptyCtx ::> tp)
    Ctx.singleton (NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w)
        ClampedIntAbsFn NatRepr w
    w    -> BaseTypeRepr (BaseBVType w)
    -> Assignment BaseTypeRepr (EmptyCtx '::> BaseBVType w)
    forall {k} (f :: k -> Type) (tp :: k).
    f tp -> Assignment f (EmptyCtx ::> tp)
    Ctx.singleton (NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w)
        ClampedIntAddFn NatRepr w
    w    -> BaseTypeRepr (BaseBVType w)
    -> Assignment
         BaseTypeRepr ((EmptyCtx ::> BaseBVType w) '::> BaseBVType w)
    forall (tp :: BaseType).
    BaseTypeRepr tp
    -> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
    binCtx (NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w)
        ClampedIntSubFn NatRepr w
    w    -> BaseTypeRepr (BaseBVType w)
    -> Assignment
         BaseTypeRepr ((EmptyCtx ::> BaseBVType w) '::> BaseBVType w)
    forall (tp :: BaseType).
    BaseTypeRepr tp
    -> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
    binCtx (NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w)
        ClampedIntMulFn NatRepr w
    w    -> BaseTypeRepr (BaseBVType w)
    -> Assignment
         BaseTypeRepr ((EmptyCtx ::> BaseBVType w) '::> BaseBVType w)
    forall (tp :: BaseType).
    BaseTypeRepr tp
    -> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
    binCtx (NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w)
        ClampedUIntAddFn NatRepr w
    w   -> BaseTypeRepr (BaseBVType w)
    -> Assignment
         BaseTypeRepr ((EmptyCtx ::> BaseBVType w) '::> BaseBVType w)
    forall (tp :: BaseType).
    BaseTypeRepr tp
    -> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
    binCtx (NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w)
        ClampedUIntSubFn NatRepr w
    w   -> BaseTypeRepr (BaseBVType w)
    -> Assignment
         BaseTypeRepr ((EmptyCtx ::> BaseBVType w) '::> BaseBVType w)
    forall (tp :: BaseType).
    BaseTypeRepr tp
    -> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
    binCtx (NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w)
        ClampedUIntMulFn NatRepr w
    w   -> BaseTypeRepr (BaseBVType w)
    -> Assignment
         BaseTypeRepr ((EmptyCtx ::> BaseBVType w) '::> BaseBVType w)
    forall (tp :: BaseType).
    BaseTypeRepr tp
    -> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
    binCtx (NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w)
        IntSetWidthFn  NatRepr m
    i NatRepr n
    _   -> BaseTypeRepr (BaseBVType m)
    -> Assignment BaseTypeRepr (EmptyCtx '::> BaseBVType m)
    forall {k} (f :: k -> Type) (tp :: k).
    f tp -> Assignment f (EmptyCtx ::> tp)
    Ctx.singleton (NatRepr m -> BaseTypeRepr (BaseBVType m)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr m
    i)
        UIntSetWidthFn NatRepr m
    i NatRepr n
    _   -> BaseTypeRepr (BaseBVType m)
    -> Assignment BaseTypeRepr (EmptyCtx '::> BaseBVType m)
    forall {k} (f :: k -> Type) (tp :: k).
    f tp -> Assignment f (EmptyCtx ::> tp)
    Ctx.singleton (NatRepr m -> BaseTypeRepr (BaseBVType m)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr m
    i)
        UIntToIntFn NatRepr m
    i NatRepr n
    _      -> BaseTypeRepr (BaseBVType m)
    -> Assignment BaseTypeRepr (EmptyCtx '::> BaseBVType m)
    forall {k} (f :: k -> Type) (tp :: k).
    f tp -> Assignment f (EmptyCtx ::> tp)
    Ctx.singleton (NatRepr m -> BaseTypeRepr (BaseBVType m)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr m
    i)
        IntToUIntFn NatRepr m
    i NatRepr n
    _      -> BaseTypeRepr (BaseBVType m)
    -> Assignment BaseTypeRepr (EmptyCtx '::> BaseBVType m)
    forall {k} (f :: k -> Type) (tp :: k).
    f tp -> Assignment f (EmptyCtx ::> tp)
    Ctx.singleton (NatRepr m -> BaseTypeRepr (BaseBVType m)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr m
    i)

        MatlabSolverFn f args ret
    RealCosFn            -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    RealSinFn            -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    RealIsNonZeroFn      -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr

        RealToSBVFn NatRepr w
    _        -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        RealToUBVFn NatRepr w
    _        -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        PredToBVFn  NatRepr w
    _        -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr

        MatlabSolverFn f args ret
    CplxIsNonZeroFn      -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxIsRealFn         -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    RealToComplexFn      -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    RealPartOfCplxFn     -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    ImagPartOfCplxFn     -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxNegFn            -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxAddFn            -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxSubFn            -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxMulFn            -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxRoundFn          -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxFloorFn          -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxCeilFn           -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxMagFn            -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxSqrtFn           -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxExpFn            -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxLogFn            -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        CplxLogBaseFn Integer
    _      -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxSinFn            -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxCosFn            -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxTanFn            -> Assignment BaseTypeRepr args
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr

    -- | Get return type of solver fn.
    matlabSolverReturnType :: MatlabSolverFn f args ret -> BaseTypeRepr ret
    matlabSolverReturnType :: forall (f :: BaseType -> Type) (args :: Ctx BaseType)
           (ret :: BaseType).
    MatlabSolverFn f args ret -> BaseTypeRepr ret
    matlabSolverReturnType MatlabSolverFn f args ret
    f =
      case MatlabSolverFn f args ret
    f of
        MatlabSolverFn f args ret
    BoolOrFn             -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    IsIntegerFn          -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    IntLeFn              -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        BVToIntegerFn{}      -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        SBVToIntegerFn{}     -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    IntegerToRealFn      -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    RealToIntegerFn      -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    PredToIntegerFn      -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        IntSeqFn{}           -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        IndicesInRange{}     -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        RealSeqFn f BaseRealType
    _ f BaseRealType
    _        -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        IsEqFn{}             -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr

        BVIsNonZeroFn NatRepr w
    _      -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        ClampedIntNegFn NatRepr w
    w    -> NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w
        ClampedIntAbsFn NatRepr w
    w    -> NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w
        ClampedIntAddFn NatRepr w
    w    -> NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w
        ClampedIntSubFn NatRepr w
    w    -> NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w
        ClampedIntMulFn NatRepr w
    w    -> NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w
        ClampedUIntAddFn NatRepr w
    w   -> NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w
        ClampedUIntSubFn NatRepr w
    w   -> NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w
        ClampedUIntMulFn NatRepr w
    w   -> NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w
        IntSetWidthFn  NatRepr m
    _ NatRepr n
    o   -> NatRepr n -> BaseTypeRepr ('BaseBVType n)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr n
    o
        UIntSetWidthFn NatRepr m
    _ NatRepr n
    o   -> NatRepr n -> BaseTypeRepr ('BaseBVType n)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr n
    o
        UIntToIntFn NatRepr m
    _ NatRepr n
    o      -> NatRepr n -> BaseTypeRepr ('BaseBVType n)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr n
    o
        IntToUIntFn NatRepr m
    _ NatRepr n
    o      -> NatRepr n -> BaseTypeRepr ('BaseBVType n)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr n
    o

        MatlabSolverFn f args ret
    RealCosFn            -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    RealSinFn            -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    RealIsNonZeroFn      -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr

        RealToSBVFn NatRepr w
    w        -> NatRepr w -> BaseTypeRepr ('BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w
        RealToUBVFn NatRepr w
    w        -> NatRepr w -> BaseTypeRepr ('BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w
        PredToBVFn  NatRepr w
    w        -> NatRepr w -> BaseTypeRepr ('BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr w
    w

        MatlabSolverFn f args ret
    CplxIsNonZeroFn      -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxIsRealFn         -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    RealToComplexFn      -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    RealPartOfCplxFn     -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    ImagPartOfCplxFn     -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxNegFn            -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxAddFn            -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxSubFn            -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxMulFn            -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxRoundFn          -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxFloorFn          -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxCeilFn           -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxMagFn            -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxSqrtFn           -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxExpFn            -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxLogFn            -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        CplxLogBaseFn Integer
    _      -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxSinFn            -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxCosFn            -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
        MatlabSolverFn f args ret
    CplxTanFn            -> BaseTypeRepr ret
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr

    ppMatlabSolverFn :: IsExpr f => MatlabSolverFn f a r -> Doc ann
    ppMatlabSolverFn :: forall (f :: BaseType -> Type) (a :: Ctx BaseType) (r :: BaseType)
           ann.
    IsExpr f =>
    MatlabSolverFn f a r -> Doc ann
    ppMatlabSolverFn MatlabSolverFn f a r
    f =
      case MatlabSolverFn f a r
    f of
        MatlabSolverFn f a r
    BoolOrFn             -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "bool_or"
        MatlabSolverFn f a r
    IsIntegerFn          -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "is_integer"
        MatlabSolverFn f a r
    IntLeFn              -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "int_le"
        BVToIntegerFn NatRepr w
    w      -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "bv_to_int" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w
        SBVToIntegerFn NatRepr w
    w     -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "sbv_to_int" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w
        MatlabSolverFn f a r
    IntegerToRealFn      -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "integer_to_real"
        MatlabSolverFn f a r
    RealToIntegerFn      -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "real_to_integer"
        MatlabSolverFn f a r
    PredToIntegerFn      -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "pred_to_integer"
        IntSeqFn  f BaseIntegerType
    b f BaseIntegerType
    i        -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "nat_seq"  Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> f BaseIntegerType -> Doc ann
    forall (tp :: BaseType) ann. f tp -> Doc ann
    forall (e :: BaseType -> Type) (tp :: BaseType) ann.
    IsExpr e =>
    e tp -> Doc ann
    printSymExpr f BaseIntegerType
    b Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> f BaseIntegerType -> Doc ann
    forall (tp :: BaseType) ann. f tp -> Doc ann
    forall (e :: BaseType -> Type) (tp :: BaseType) ann.
    IsExpr e =>
    e tp -> Doc ann
    printSymExpr f BaseIntegerType
    i
        RealSeqFn f BaseRealType
    b f BaseRealType
    i        -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "real_seq" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> f BaseRealType -> Doc ann
    forall (tp :: BaseType) ann. f tp -> Doc ann
    forall (e :: BaseType -> Type) (tp :: BaseType) ann.
    IsExpr e =>
    e tp -> Doc ann
    printSymExpr f BaseRealType
    b Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> f BaseRealType -> Doc ann
    forall (tp :: BaseType) ann. f tp -> Doc ann
    forall (e :: BaseType -> Type) (tp :: BaseType) ann.
    IsExpr e =>
    e tp -> Doc ann
    printSymExpr f BaseRealType
    i
        IndicesInRange Assignment OnlyIntRepr (idx '::> itp)
    _ Assignment f (idx '::> itp)
    bnds ->
          Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "indices_in_range" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> [Doc ann] -> Doc ann
    forall ann. [Doc ann] -> Doc ann
    sep ((forall (x :: BaseType). f x -> Doc ann)
    -> forall (x :: Ctx BaseType). Assignment f x -> [Doc ann]
    forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
    FoldableFC t =>
    (forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
    forall (f :: BaseType -> Type) a.
    (forall (x :: BaseType). f x -> a)
    -> forall (x :: Ctx BaseType). Assignment f x -> [a]
    toListFC f x -> Doc ann
    forall (x :: BaseType). f x -> Doc ann
    forall (tp :: BaseType) ann. f tp -> Doc ann
    forall (e :: BaseType -> Type) (tp :: BaseType) ann.
    IsExpr e =>
    e tp -> Doc ann
    printSymExpr Assignment f (idx '::> itp)
    bnds))
        IsEqFn{}             -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "is_eq"

        BVIsNonZeroFn NatRepr w
    w      -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "bv_is_nonzero" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w
        ClampedIntNegFn NatRepr w
    w    -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "clamped_int_neg" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w
        ClampedIntAbsFn NatRepr w
    w    -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "clamped_neg_abs" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w
        ClampedIntAddFn NatRepr w
    w    -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "clamped_int_add" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w
        ClampedIntSubFn NatRepr w
    w    -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "clamped_int_sub" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w
        ClampedIntMulFn NatRepr w
    w    -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "clamped_int_mul" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w
        ClampedUIntAddFn NatRepr w
    w   -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "clamped_uint_add" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w
        ClampedUIntSubFn NatRepr w
    w   -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "clamped_uint_sub" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w
        ClampedUIntMulFn NatRepr w
    w   -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "clamped_uint_mul" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w

        IntSetWidthFn NatRepr m
    i NatRepr n
    o    -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "int_set_width"  Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr m -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr m
    i Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr n -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr n
    o
        UIntSetWidthFn NatRepr m
    i NatRepr n
    o   -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "uint_set_width" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr m -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr m
    i Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr n -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr n
    o
        UIntToIntFn NatRepr m
    i NatRepr n
    o      -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "uint_to_int"  Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr m -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr m
    i Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr n -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr n
    o
        IntToUIntFn NatRepr m
    i NatRepr n
    o      -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "int_to_uint"  Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr m -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr m
    i Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr n -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr n
    o

        MatlabSolverFn f a r
    RealCosFn            -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "real_cos"
        MatlabSolverFn f a r
    RealSinFn            -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "real_sin"
        MatlabSolverFn f a r
    RealIsNonZeroFn      -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "real_is_nonzero"

        RealToSBVFn NatRepr w
    w        -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "real_to_sbv" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w
        RealToUBVFn NatRepr w
    w        -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "real_to_sbv" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w
        PredToBVFn  NatRepr w
    w        -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "pred_to_bv"  Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> NatRepr w -> Doc ann
    forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr NatRepr w
    w

        MatlabSolverFn f a r
    CplxIsNonZeroFn      -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_is_nonzero"
        MatlabSolverFn f a r
    CplxIsRealFn         -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_is_real"
        MatlabSolverFn f a r
    RealToComplexFn      -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "real_to_complex"
        MatlabSolverFn f a r
    RealPartOfCplxFn     -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "real_part_of_complex"
        MatlabSolverFn f a r
    ImagPartOfCplxFn     -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "imag_part_of_complex"

        MatlabSolverFn f a r
    CplxNegFn            -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_neg"
        MatlabSolverFn f a r
    CplxAddFn            -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_add"
        MatlabSolverFn f a r
    CplxSubFn            -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_sub"
        MatlabSolverFn f a r
    CplxMulFn            -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_mul"

        MatlabSolverFn f a r
    CplxRoundFn          -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_round"
        MatlabSolverFn f a r
    CplxFloorFn          -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_floor"
        MatlabSolverFn f a r
    CplxCeilFn           -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_ceil"
        MatlabSolverFn f a r
    CplxMagFn            -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_mag"
        MatlabSolverFn f a r
    CplxSqrtFn           -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_sqrt"
        MatlabSolverFn f a r
    CplxExpFn            -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_exp"
        MatlabSolverFn f a r
    CplxLogFn            -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_log"
        CplxLogBaseFn Integer
    b      -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_log_base" Doc ann -> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Integer -> Doc ann
    forall ann. Integer -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty Integer
    b
        MatlabSolverFn f a r
    CplxSinFn            -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_sin"
        MatlabSolverFn f a r
    CplxCosFn            -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_cos"
        MatlabSolverFn f a r
    CplxTanFn            -> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty String
    "cplx_tan"

    ppNatRepr :: NatRepr w -> Doc ann
    ppNatRepr :: forall (w :: Natural) ann. NatRepr w -> Doc ann
    ppNatRepr = NatRepr w -> Doc ann
    forall a ann. Show a => a -> Doc ann
    viaShow

    -- | Test 'MatlabSolverFn' values for equality.
    testSolverFnEq :: TestEquality f
                   => MatlabSolverFn f ax rx
                   -> MatlabSolverFn f ay ry
                   -> Maybe ((ax ::> rx) :~: (ay ::> ry))
    testSolverFnEq :: forall (f :: BaseType -> Type) (ax :: Ctx BaseType)
           (rx :: BaseType) (ay :: Ctx BaseType) (ry :: BaseType).
    TestEquality f =>
    MatlabSolverFn f ax rx
    -> MatlabSolverFn f ay ry -> Maybe ((ax ::> rx) :~: (ay ::> ry))
    testSolverFnEq = $(structuralTypeEquality [t|MatlabSolverFn|]
                       [ ( DataArg 0 `TypeApp` AnyType
                         , [|testEquality|]
                         )
                       , ( ConType [t|NatRepr|] `TypeApp` AnyType
                         , [|testEquality|]
                         )
                       , ( ConType [t|Assignment|] `TypeApp` AnyType `TypeApp` AnyType
                         , [|testEquality|]
                         )
                       , ( ConType [t|BaseTypeRepr|] `TypeApp` AnyType
                         , [|testEquality|]
                         )
                       ]
                      )

    instance TestEquality f => Eq (MatlabSolverFn f args tp) where
      MatlabSolverFn f args tp
    x == :: MatlabSolverFn f args tp -> MatlabSolverFn f args tp -> Bool
    == MatlabSolverFn f args tp
    y = Maybe ((args ::> tp) :~: (args ::> tp)) -> Bool
    forall a. Maybe a -> Bool
    isJust (MatlabSolverFn f args tp
    -> MatlabSolverFn f args tp
    -> Maybe ((args ::> tp) :~: (args ::> tp))
    forall (f :: BaseType -> Type) (ax :: Ctx BaseType)
           (rx :: BaseType) (ay :: Ctx BaseType) (ry :: BaseType).
    TestEquality f =>
    MatlabSolverFn f ax rx
    -> MatlabSolverFn f ay ry -> Maybe ((ax ::> rx) :~: (ay ::> ry))
    testSolverFnEq MatlabSolverFn f args tp
    x MatlabSolverFn f args tp
    y)

    instance ( Hashable (f BaseRealType)
             , Hashable (f BaseIntegerType)
             , HashableF f
             , TestEquality f
             )
             => Hashable (MatlabSolverFn f args tp) where
      hashWithSalt :: Int -> MatlabSolverFn f args tp -> Int
    hashWithSalt = $(structuralHashWithSalt [t|MatlabSolverFn|] [])

    realIsNonZero :: IsExprBuilder sym => sym -> SymReal sym -> IO (Pred sym)
    realIsNonZero :: forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (Pred sym)
    realIsNonZero sym
    sym = sym
    -> SymExpr sym BaseRealType
    -> SymExpr sym BaseRealType
    -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
    realNe sym
    sym (sym -> SymExpr sym BaseRealType
    forall sym. IsExprBuilder sym => sym -> SymReal sym
    realZero sym
    sym)

    evalMatlabSolverFn :: forall sym args ret
                       .  IsExprBuilder sym
                       => MatlabSolverFn (SymExpr sym) args ret
                       -> sym
                       -> Assignment (SymExpr sym) args
                       -> IO (SymExpr sym ret)
    evalMatlabSolverFn :: forall sym (args :: Ctx BaseType) (ret :: BaseType).
    IsExprBuilder sym =>
    MatlabSolverFn (SymExpr sym) args ret
    -> sym -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    evalMatlabSolverFn MatlabSolverFn (SymExpr sym) args ret
    f sym
    sym =
      case MatlabSolverFn (SymExpr sym) args ret
    f of
        MatlabSolverFn (SymExpr sym) args ret
    BoolOrFn         -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    orPred sym
    sym

        MatlabSolverFn (SymExpr sym) args ret
    IsIntegerFn      -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymReal sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (Pred sym)
    isInteger sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    IntLeFn          -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
    intLe sym
    sym
        BVToIntegerFn{}  -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymBV sym w -> IO (SymInteger sym)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymInteger sym)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymInteger sym)
    bvToInteger sym
    sym
        SBVToIntegerFn{} -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymBV sym w -> IO (SymInteger sym)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (SymInteger sym)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymInteger sym)
    sbvToInteger sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    IntegerToRealFn  -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymInteger sym -> IO (SymReal sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymReal sym)
    integerToReal sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    RealToIntegerFn  -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymReal sym -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (SymInteger sym)
    realToInteger sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    PredToIntegerFn  -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ \Pred sym
    p ->
          (sym
     -> Pred sym
     -> SymInteger sym
     -> SymInteger sym
     -> IO (SymInteger sym))
    -> sym
    -> Pred sym
    -> IO (SymInteger sym)
    -> IO (SymInteger sym)
    -> IO (SymInteger sym)
    forall sym v.
    IsExprBuilder sym =>
    (sym -> Pred sym -> v -> v -> IO v)
    -> sym -> Pred sym -> IO v -> IO v -> IO v
    iteM sym
    -> Pred sym
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym
    -> Pred sym
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SymInteger sym)
    intIte sym
    sym Pred sym
    p (sym -> Integer -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    intLit sym
    sym Integer
    1) (sym -> Integer -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    intLit sym
    sym Integer
    0)
        IntSeqFn SymInteger sym
    b SymInteger sym
    inc   -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ \SymInteger sym
    idx SymInteger sym
    _ -> do
          sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    intAdd sym
    sym SymInteger sym
    b (SymInteger sym -> IO (SymInteger sym))
    -> IO (SymInteger sym) -> IO (SymInteger sym)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
    intMul sym
    sym SymInteger sym
    inc SymInteger sym
    idx
        RealSeqFn SymReal sym
    b SymReal sym
    inc -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ \SymInteger sym
    _ SymInteger sym
    idx -> do
          sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
    realAdd sym
    sym SymReal sym
    b (SymReal sym -> IO (SymReal sym))
    -> IO (SymReal sym) -> IO (SymReal sym)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
    realMul sym
    sym SymReal sym
    inc (SymReal sym -> IO (SymReal sym))
    -> IO (SymReal sym) -> IO (SymReal sym)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SymInteger sym -> IO (SymReal sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymReal sym)
    integerToReal sym
    sym SymInteger sym
    idx
        IndicesInRange Assignment OnlyIntRepr (idx '::> itp)
    tps0 Assignment (SymExpr sym) (idx '::> itp)
    bnds0 -> \Assignment (SymExpr sym) args
    args ->
            Size (idx '::> itp)
    -> (forall (tp :: BaseType).
        IO (Pred sym) -> Index (idx '::> itp) tp -> IO (Pred sym))
    -> IO (Pred sym)
    -> IO (Pred sym)
    forall {k} (ctx :: Ctx k) r.
    Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
    Ctx.forIndex (Assignment OnlyIntRepr (idx '::> itp) -> Size (idx '::> itp)
    forall {k} (f :: k -> Type) (ctx :: Ctx k).
    Assignment f ctx -> Size ctx
    Ctx.size Assignment OnlyIntRepr (idx '::> itp)
    tps0) (Assignment OnlyIntRepr (idx '::> itp)
    -> Assignment (SymExpr sym) (idx '::> itp)
    -> Assignment (SymExpr sym) (idx '::> itp)
    -> IO (Pred sym)
    -> Index (idx '::> itp) tp
    -> IO (Pred sym)
    forall (ctx :: Ctx BaseType) (tp :: BaseType).
    Assignment OnlyIntRepr ctx
    -> Assignment (SymExpr sym) ctx
    -> Assignment (SymExpr sym) ctx
    -> IO (Pred sym)
    -> Index ctx tp
    -> IO (Pred sym)
    g Assignment OnlyIntRepr (idx '::> itp)
    tps0 Assignment (SymExpr sym) (idx '::> itp)
    bnds0 Assignment (SymExpr sym) args
    Assignment (SymExpr sym) (idx '::> itp)
    args) (Pred sym -> IO (Pred sym)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (sym -> Pred sym
    forall sym. IsExprBuilder sym => sym -> Pred sym
    truePred sym
    sym))
          where g :: Assignment OnlyIntRepr ctx
                  -> Assignment (SymExpr sym) ctx
                  -> Assignment (SymExpr sym) ctx
                  -> IO (Pred sym)
                  -> Index ctx tp
                  -> IO (Pred sym)
                g :: forall (ctx :: Ctx BaseType) (tp :: BaseType).
    Assignment OnlyIntRepr ctx
    -> Assignment (SymExpr sym) ctx
    -> Assignment (SymExpr sym) ctx
    -> IO (Pred sym)
    -> Index ctx tp
    -> IO (Pred sym)
    g Assignment OnlyIntRepr ctx
    tps Assignment (SymExpr sym) ctx
    bnds Assignment (SymExpr sym) ctx
    args IO (Pred sym)
    m Index ctx tp
    i = do
                  case Assignment OnlyIntRepr ctx
    tps Assignment OnlyIntRepr ctx -> Index ctx tp -> OnlyIntRepr tp
    forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    Ctx.! Index ctx tp
    i of
                    OnlyIntRepr tp
    OnlyIntRepr -> do
                      let v :: SymExpr sym tp
    v = Assignment (SymExpr sym) ctx
    args Assignment (SymExpr sym) ctx -> Index ctx tp -> SymExpr sym tp
    forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    ! Index ctx tp
    i
                      let bnd :: SymExpr sym tp
    bnd = Assignment (SymExpr sym) ctx
    bnds Assignment (SymExpr sym) ctx -> Index ctx tp -> SymExpr sym tp
    forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
    Assignment f ctx -> Index ctx tp -> f tp
    ! Index ctx tp
    i
                      SymInteger sym
    one <- sym -> Integer -> IO (SymInteger sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> IO (SymInteger sym)
    intLit sym
    sym Integer
    1
                      Pred sym
    p <- IO (IO (Pred sym)) -> IO (Pred sym)
    forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
    join (IO (IO (Pred sym)) -> IO (Pred sym))
    -> IO (IO (Pred sym)) -> IO (Pred sym)
    forall a b. (a -> b) -> a -> b
    $ sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    andPred sym
    sym (Pred sym -> Pred sym -> IO (Pred sym))
    -> IO (Pred sym) -> IO (Pred sym -> IO (Pred sym))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
    intLe sym
    sym SymInteger sym
    one SymExpr sym tp
    SymInteger sym
    v IO (Pred sym -> IO (Pred sym))
    -> IO (Pred sym) -> IO (IO (Pred sym))
    forall a b. IO (a -> b) -> IO a -> IO b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
    intLe sym
    sym SymExpr sym tp
    SymInteger sym
    v SymExpr sym tp
    SymInteger sym
    bnd
                      sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    andPred sym
    sym Pred sym
    p (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IO (Pred sym)
    m
        IsEqFn{} -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ \SymExpr sym tp
    x SymExpr sym tp
    y -> do
          sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
    forall sym (tp :: BaseType).
    IsExprBuilder sym =>
    sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
    forall (tp :: BaseType).
    sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
    isEq sym
    sym SymExpr sym tp
    x SymExpr sym tp
    y

        BVIsNonZeroFn NatRepr w
    _    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymBV sym w -> IO (Pred sym)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> IO (Pred sym)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (Pred sym)
    bvIsNonzero sym
    sym
        ClampedIntNegFn NatRepr w
    _  -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    clampedIntNeg sym
    sym
        ClampedIntAbsFn NatRepr w
    _  -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> IO (SymBV sym w)
    clampedIntAbs sym
    sym
        ClampedIntAddFn NatRepr w
    _  -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    clampedIntAdd sym
    sym
        ClampedIntSubFn NatRepr w
    _  -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    clampedIntSub sym
    sym
        ClampedIntMulFn NatRepr w
    _  -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    clampedIntMul sym
    sym
        ClampedUIntAddFn NatRepr w
    _ -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    clampedUIntAdd sym
    sym
        ClampedUIntSubFn NatRepr w
    _ -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    clampedUIntSub sym
    sym
        ClampedUIntMulFn NatRepr w
    _ -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
    clampedUIntMul sym
    sym

        IntSetWidthFn  NatRepr m
    _ NatRepr n
    o -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ \SymExpr sym (BaseBVType m)
    v -> sym -> SymExpr sym (BaseBVType m) -> NatRepr n -> IO (SymBV sym n)
    forall (m :: Natural) (n :: Natural).
    (1 <= m, 1 <= n) =>
    sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
    forall sym (m :: Natural) (n :: Natural).
    (IsExprBuilder sym, 1 <= m, 1 <= n) =>
    sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
    intSetWidth  sym
    sym SymExpr sym (BaseBVType m)
    v NatRepr n
    o
        UIntSetWidthFn NatRepr m
    _ NatRepr n
    o -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ \SymExpr sym (BaseBVType m)
    v -> sym -> SymExpr sym (BaseBVType m) -> NatRepr n -> IO (SymBV sym n)
    forall (m :: Natural) (n :: Natural).
    (1 <= m, 1 <= n) =>
    sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
    forall sym (m :: Natural) (n :: Natural).
    (IsExprBuilder sym, 1 <= m, 1 <= n) =>
    sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
    uintSetWidth sym
    sym SymExpr sym (BaseBVType m)
    v NatRepr n
    o
        UIntToIntFn NatRepr m
    _ NatRepr n
    o    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ \SymExpr sym (BaseBVType m)
    v -> sym -> SymExpr sym (BaseBVType m) -> NatRepr n -> IO (SymBV sym n)
    forall (m :: Natural) (n :: Natural).
    (1 <= m, 1 <= n) =>
    sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
    forall sym (m :: Natural) (n :: Natural).
    (IsExprBuilder sym, 1 <= m, 1 <= n) =>
    sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
    uintToInt sym
    sym SymExpr sym (BaseBVType m)
    v NatRepr n
    o
        IntToUIntFn NatRepr m
    _ NatRepr n
    o    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ \SymExpr sym (BaseBVType m)
    v -> sym -> SymExpr sym (BaseBVType m) -> NatRepr n -> IO (SymBV sym n)
    forall (m :: Natural) (n :: Natural).
    (1 <= m, 1 <= n) =>
    sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
    forall sym (m :: Natural) (n :: Natural).
    (IsExprBuilder sym, 1 <= m, 1 <= n) =>
    sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
    intToUInt sym
    sym SymExpr sym (BaseBVType m)
    v NatRepr n
    o

        MatlabSolverFn (SymExpr sym) args ret
    RealIsNonZeroFn    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymReal sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (Pred sym)
    realIsNonZero sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    RealCosFn          -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymReal sym -> IO (SymReal sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (SymReal sym)
    realCos sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    RealSinFn          -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymReal sym -> IO (SymReal sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (SymReal sym)
    realSin sym
    sym

        RealToSBVFn NatRepr w
    w      -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ \SymReal sym
    v -> sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
    realToSBV sym
    sym SymReal sym
    v NatRepr w
    w
        RealToUBVFn NatRepr w
    w      -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ \SymReal sym
    v -> sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
    realToBV  sym
    sym SymReal sym
    v NatRepr w
    w
        PredToBVFn  NatRepr w
    w      -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ \Pred sym
    v -> sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
    forall (w :: Natural).
    (1 <= w) =>
    sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
    forall sym (w :: Natural).
    (IsExprBuilder sym, 1 <= w) =>
    sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
    predToBV  sym
    sym Pred sym
    v NatRepr w
    w

        MatlabSolverFn (SymExpr sym) args ret
    CplxIsNonZeroFn  -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ \SymExpr sym BaseComplexType
    x -> do
          (SymReal sym
    real_x :+ SymReal sym
    imag_x) <- sym -> SymExpr sym BaseComplexType -> IO (Complex (SymReal sym))
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (Complex (SymReal sym))
    cplxGetParts sym
    sym SymExpr sym BaseComplexType
    x
          IO (IO (Pred sym)) -> IO (Pred sym)
    forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
    join (IO (IO (Pred sym)) -> IO (Pred sym))
    -> IO (IO (Pred sym)) -> IO (Pred sym)
    forall a b. (a -> b) -> a -> b
    $ sym -> Pred sym -> Pred sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
    orPred sym
    sym (Pred sym -> Pred sym -> IO (Pred sym))
    -> IO (Pred sym) -> IO (Pred sym -> IO (Pred sym))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymReal sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (Pred sym)
    realIsNonZero sym
    sym SymReal sym
    real_x IO (Pred sym -> IO (Pred sym))
    -> IO (Pred sym) -> IO (IO (Pred sym))
    forall a b. IO (a -> b) -> IO a -> IO b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> sym -> SymReal sym -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (Pred sym)
    realIsNonZero sym
    sym SymReal sym
    imag_x
        MatlabSolverFn (SymExpr sym) args ret
    CplxIsRealFn     -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymExpr sym BaseComplexType -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (Pred sym)
    isReal sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    RealToComplexFn  -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymReal sym -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> IO (SymCplx sym)
    cplxFromReal sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    RealPartOfCplxFn -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymExpr sym BaseComplexType -> IO (SymReal sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (SymReal sym)
    getRealPart sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    ImagPartOfCplxFn -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymExpr sym BaseComplexType -> IO (SymReal sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (SymReal sym)
    getImagPart sym
    sym

        MatlabSolverFn (SymExpr sym) args ret
    CplxNegFn        -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseComplexType -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (SymCplx sym)
    cplxNeg sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    CplxAddFn        -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseComplexType
    -> SymExpr sym BaseComplexType
    -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
    cplxAdd sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    CplxSubFn        -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseComplexType
    -> SymExpr sym BaseComplexType
    -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
    cplxSub sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    CplxMulFn        -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseComplexType
    -> SymExpr sym BaseComplexType
    -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
    cplxMul sym
    sym

        MatlabSolverFn (SymExpr sym) args ret
    CplxRoundFn      -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseComplexType -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (SymCplx sym)
    cplxRound sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    CplxFloorFn      -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseComplexType -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (SymCplx sym)
    cplxFloor sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    CplxCeilFn       -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseComplexType -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (SymCplx sym)
    cplxCeil  sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    CplxMagFn        -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym -> SymExpr sym BaseComplexType -> IO (SymReal sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (SymReal sym)
    cplxMag   sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    CplxSqrtFn       -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseComplexType -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (SymCplx sym)
    cplxSqrt  sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    CplxExpFn        -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseComplexType -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (SymCplx sym)
    cplxExp   sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    CplxLogFn        -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseComplexType -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (SymCplx sym)
    cplxLog   sym
    sym
        CplxLogBaseFn Integer
    b  -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ Rational
    -> sym
    -> SymExpr sym BaseComplexType
    -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    Rational -> sym -> SymCplx sym -> IO (SymCplx sym)
    cplxLogBase (Integer -> Rational
    forall a. Real a => a -> Rational
    toRational Integer
    b) sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    CplxSinFn        -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseComplexType -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (SymCplx sym)
    cplxSin  sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    CplxCosFn        -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseComplexType -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (SymCplx sym)
    cplxCos  sym
    sym
        MatlabSolverFn (SymExpr sym) args ret
    CplxTanFn        -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
    forall k (ctx :: Ctx k) (f :: k -> Type) x.
    CurryAssignmentClass ctx =>
    CurryAssignment ctx f x -> Assignment f ctx -> x
    forall (f :: BaseType -> Type) x.
    CurryAssignment args f x -> Assignment f args -> x
    Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
     -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret))
    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
    -> Assignment (SymExpr sym) args
    -> IO (SymExpr sym ret)
    forall a b. (a -> b) -> a -> b
    $ sym
    -> SymExpr sym BaseComplexType -> IO (SymExpr sym BaseComplexType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymCplx sym -> IO (SymCplx sym)
    cplxTan  sym
    sym

    -- | This class is provides functions needed to implement the symbolic
    -- array intrinsic functions
    class IsSymExprBuilder sym => MatlabSymbolicArrayBuilder sym where

      -- | Create a Matlab solver function from its prototype.
      mkMatlabSolverFn :: sym
                       -> MatlabSolverFn (SymExpr sym) args ret
                       -> IO (SymFn sym args ret)