{-|
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 = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
  forall (n :: Natural) (m :: Natural) a.
NatRepr n -> NatRepr m -> ((m <= (n + m)) => a) -> a
withAddPrefixLeq NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat :: NatRepr 1) forall a b. (a -> b) -> a -> b
$ do
  -- Compute result with 1 additional bit to catch clamping
  let w' :: NatRepr (w + 1)
w' = forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
incNat NatRepr w
w
  SymExpr sym (BaseBVType (w + 1))
x'  <- 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'  <- 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'  <- 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 <- 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' forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + 1)
w' (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr (w + 1)
w')
  SymBV sym w
max_int <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
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 <- 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' forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + 1)
w' (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr (w + 1)
w')
  SymBV sym w
min_int <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr w
w)

  -- Clamp integer range.
  SymBV sym w
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 <- 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
  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 = 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) <- 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  <- 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 <- 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 <- 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 <- 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
  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 = 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) <- 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    <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w)
  SymBV sym w
ones   <- 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 <- forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
lo)
                              forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> 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 <- forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
lo
                              forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> 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     <- forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 <- 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 <- 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 <- 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 <- 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
  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 = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
  SymBV sym w
minint <- 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 <- 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
  forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM 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 (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxSignedBV sym
sym NatRepr w
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  <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
x
  forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM 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 (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
clampedIntNeg sym
sym SymBV sym w
x) (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 = 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) <- 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   <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxUnsignedBV sym
sym NatRepr w
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 = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
  SymExpr sym BaseBoolType
no_underflow <- 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

  forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM 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
       (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
       (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
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 = 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) <- 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   <- 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       <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym SymBV sym w
hi
  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             -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn
  f ((EmptyCtx ::> BaseBoolType) '::> BaseBoolType) BaseBoolType
BoolOrFn
    MatlabSolverFn e a r
IsIntegerFn          -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseBoolType
IsIntegerFn
    MatlabSolverFn e a r
IntLeFn              -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn
  f
  ((EmptyCtx ::> BaseIntegerType) '::> BaseIntegerType)
  BaseBoolType
IntLeFn
    BVToIntegerFn NatRepr w
w      -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
BVToIntegerFn NatRepr w
w
    SBVToIntegerFn NatRepr w
w     -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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      -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType
IntegerToRealFn
    MatlabSolverFn e a r
RealToIntegerFn      -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseIntegerType
RealToIntegerFn
    MatlabSolverFn e a r
PredToIntegerFn      -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType
PredToIntegerFn
    IntSeqFn  e BaseIntegerType
b e BaseIntegerType
i        -> forall (f :: BaseType -> Type).
f BaseIntegerType
-> f BaseIntegerType
-> MatlabSolverFn
     f
     ((EmptyCtx ::> BaseIntegerType) '::> BaseIntegerType)
     BaseIntegerType
IntSeqFn forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tp :: BaseType). e tp -> m (f tp)
f e BaseIntegerType
b forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (tp :: BaseType). e tp -> m (f tp)
f e BaseIntegerType
i
    RealSeqFn e BaseRealType
b e BaseRealType
i        -> forall (f :: BaseType -> Type).
f BaseRealType
-> f BaseRealType
-> MatlabSolverFn
     f
     ((EmptyCtx ::> BaseIntegerType) '::> BaseIntegerType)
     BaseRealType
RealSeqFn forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tp :: BaseType). e tp -> m (f tp)
f e BaseRealType
b forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (tp :: BaseType). e tp -> m (f tp)
f e BaseRealType
i
    IndicesInRange Assignment OnlyIntRepr (idx '::> itp)
tps Assignment e (idx '::> itp)
a -> 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 forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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)
traverseFC forall (tp :: BaseType). e tp -> m (f tp)
f Assignment e (idx '::> itp)
a
    IsEqFn BaseTypeRepr tp
tp            -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: BaseType) (f :: BaseType -> Type).
BaseTypeRepr w
-> MatlabSolverFn f ((EmptyCtx ::> w) ::> w) BaseBoolType
IsEqFn BaseTypeRepr tp
tp

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

    ClampedIntNegFn NatRepr w
w    -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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    -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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    -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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    -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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    -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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   -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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   -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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   -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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    -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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   -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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      -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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      -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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            -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseRealType
RealCosFn
    MatlabSolverFn e a r
RealSinFn            -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseRealType
RealSinFn
    MatlabSolverFn e a r
RealIsNonZeroFn      -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseBoolType
RealIsNonZeroFn

    RealToSBVFn NatRepr w
w        -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn f (EmptyCtx '::> BaseRealType) (BaseBVType w)
RealToSBVFn NatRepr w
w
    RealToUBVFn NatRepr w
w        -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn f (EmptyCtx '::> BaseRealType) (BaseBVType w)
RealToUBVFn NatRepr w
w
    PredToBVFn  NatRepr w
w        -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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      -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseBoolType
CplxIsNonZeroFn
    MatlabSolverFn e a r
CplxIsRealFn         -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseBoolType
CplxIsRealFn
    MatlabSolverFn e a r
RealToComplexFn      -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseComplexType
RealToComplexFn
    MatlabSolverFn e a r
RealPartOfCplxFn     -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseRealType
RealPartOfCplxFn
    MatlabSolverFn e a r
ImagPartOfCplxFn     -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseRealType
ImagPartOfCplxFn
    MatlabSolverFn e a r
CplxNegFn            -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxNegFn
    MatlabSolverFn e a r
CplxAddFn            -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn
  f
  ((EmptyCtx '::> BaseComplexType) '::> BaseComplexType)
  BaseComplexType
CplxAddFn
    MatlabSolverFn e a r
CplxSubFn            -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn
  f
  ((EmptyCtx '::> BaseComplexType) '::> BaseComplexType)
  BaseComplexType
CplxSubFn
    MatlabSolverFn e a r
CplxMulFn            -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn
  f
  ((EmptyCtx '::> BaseComplexType) '::> BaseComplexType)
  BaseComplexType
CplxMulFn
    MatlabSolverFn e a r
CplxRoundFn          -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxRoundFn
    MatlabSolverFn e a r
CplxFloorFn          -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxFloorFn
    MatlabSolverFn e a r
CplxCeilFn           -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxCeilFn
    MatlabSolverFn e a r
CplxMagFn            -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseRealType
CplxMagFn
    MatlabSolverFn e a r
CplxSqrtFn           -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxSqrtFn
    MatlabSolverFn e a r
CplxExpFn            -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxExpFn
    MatlabSolverFn e a r
CplxLogFn            -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxLogFn
    CplxLogBaseFn Integer
b      -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
Integer
-> MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxLogBaseFn Integer
b
    MatlabSolverFn e a r
CplxSinFn            -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxSinFn
    MatlabSolverFn e a r
CplxCosFn            -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxCosFn
    MatlabSolverFn e a r
CplxTanFn            -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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 = forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty 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 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             -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
IsIntegerFn          -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
IntLeFn              -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVToIntegerFn NatRepr w
w      -> forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)
    SBVToIntegerFn NatRepr w
w     -> forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)
    MatlabSolverFn f args ret
IntegerToRealFn      -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
RealToIntegerFn      -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
PredToIntegerFn      -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntSeqFn{}           -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IndicesInRange Assignment OnlyIntRepr (idx '::> itp)
tps Assignment f (idx '::> itp)
_ -> 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
fmapFC forall (tp :: BaseType). OnlyIntRepr tp -> BaseTypeRepr tp
toBaseTypeRepr Assignment OnlyIntRepr (idx '::> itp)
tps
    RealSeqFn f BaseRealType
_ f BaseRealType
_        -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IsEqFn BaseTypeRepr tp
tp            -> forall (tp :: BaseType).
BaseTypeRepr tp
-> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
binCtx BaseTypeRepr tp
tp

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

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

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

    MatlabSolverFn f args ret
CplxIsNonZeroFn      -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxIsRealFn         -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
RealToComplexFn      -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
RealPartOfCplxFn     -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
ImagPartOfCplxFn     -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxNegFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxAddFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxSubFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxMulFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxRoundFn          -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxFloorFn          -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxCeilFn           -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxMagFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxSqrtFn           -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxExpFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxLogFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    CplxLogBaseFn Integer
_      -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxSinFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxCosFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxTanFn            -> 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             -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
IsIntegerFn          -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
IntLeFn              -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVToIntegerFn{}      -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    SBVToIntegerFn{}     -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
IntegerToRealFn      -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
RealToIntegerFn      -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
PredToIntegerFn      -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntSeqFn{}           -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IndicesInRange{}     -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealSeqFn f BaseRealType
_ f BaseRealType
_        -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IsEqFn{}             -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

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

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

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

    MatlabSolverFn f args ret
CplxIsNonZeroFn      -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxIsRealFn         -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
RealToComplexFn      -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
RealPartOfCplxFn     -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
ImagPartOfCplxFn     -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxNegFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxAddFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxSubFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxMulFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxRoundFn          -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxFloorFn          -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxCeilFn           -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxMagFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxSqrtFn           -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxExpFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxLogFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    CplxLogBaseFn Integer
_      -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxSinFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxCosFn            -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    MatlabSolverFn f args ret
CplxTanFn            -> 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             -> forall a ann. Pretty a => a -> Doc ann
pretty String
"bool_or"
    MatlabSolverFn f a r
IsIntegerFn          -> forall a ann. Pretty a => a -> Doc ann
pretty String
"is_integer"
    MatlabSolverFn f a r
IntLeFn              -> forall a ann. Pretty a => a -> Doc ann
pretty String
"int_le"
    BVToIntegerFn NatRepr w
w      -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"bv_to_int" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
    SBVToIntegerFn NatRepr w
w     -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"sbv_to_int" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
    MatlabSolverFn f a r
IntegerToRealFn      -> forall a ann. Pretty a => a -> Doc ann
pretty String
"integer_to_real"
    MatlabSolverFn f a r
RealToIntegerFn      -> forall a ann. Pretty a => a -> Doc ann
pretty String
"real_to_integer"
    MatlabSolverFn f a r
PredToIntegerFn      -> forall a ann. Pretty a => a -> Doc ann
pretty String
"pred_to_integer"
    IntSeqFn  f BaseIntegerType
b f BaseIntegerType
i        -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"nat_seq"  forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr f BaseIntegerType
b forall ann. Doc ann -> Doc ann -> 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        -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"real_seq" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr f BaseRealType
b forall ann. Doc ann -> Doc ann -> 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 ->
      forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty String
"indices_in_range" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. [Doc ann] -> Doc ann
sep (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]
toListFC forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr Assignment f (idx '::> itp)
bnds))
    IsEqFn{}             -> forall a ann. Pretty a => a -> Doc ann
pretty String
"is_eq"

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

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

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

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

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

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

    MatlabSolverFn f a r
CplxRoundFn          -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_round"
    MatlabSolverFn f a r
CplxFloorFn          -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_floor"
    MatlabSolverFn f a r
CplxCeilFn           -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_ceil"
    MatlabSolverFn f a r
CplxMagFn            -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_mag"
    MatlabSolverFn f a r
CplxSqrtFn           -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_sqrt"
    MatlabSolverFn f a r
CplxExpFn            -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_exp"
    MatlabSolverFn f a r
CplxLogFn            -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_log"
    CplxLogBaseFn Integer
b      -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_log_base" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Integer
b
    MatlabSolverFn f a r
CplxSinFn            -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_sin"
    MatlabSolverFn f a r
CplxCosFn            -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_cos"
    MatlabSolverFn f a r
CplxTanFn            -> 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 = 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 = forall a. Maybe a -> Bool
isJust (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 = forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realNe sym
sym (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         -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym

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

    BVIsNonZeroFn NatRepr w
_    -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym
    ClampedIntNegFn NatRepr w
_  -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
clampedIntNeg sym
sym
    ClampedIntAbsFn NatRepr w
_  -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
clampedIntAbs sym
sym
    ClampedIntAddFn NatRepr w
_  -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ 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
_  -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ 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
_  -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ 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
_ -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ 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
_ -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ 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
_ -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ 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 -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym (BaseBVType m)
v -> 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 -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym (BaseBVType m)
v -> 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    -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym (BaseBVType m)
v -> 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    -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym (BaseBVType m)
v -> 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    -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (Pred sym)
realIsNonZero sym
sym
    MatlabSolverFn (SymExpr sym) args ret
RealCosFn          -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realCos sym
sym
    MatlabSolverFn (SymExpr sym) args ret
RealSinFn          -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSin sym
sym

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

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

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

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