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

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

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

  -- Clamp integer range.
  SymBV sym w
r <- sym
-> NatRepr w
-> SymExpr sym (BaseBVType (w + 1))
-> IO (SymBV sym w)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w SymExpr sym (BaseBVType (w + 1))
r'
  SymBV sym w
r_low <- sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
too_low SymBV sym w
min_int SymBV sym w
r
  sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(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 :: sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedIntSub sym
sym SymBV sym w
x SymBV sym w
y = do
  let w :: NatRepr w
w = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
  (SymExpr sym BaseBoolType
ov, SymBV sym w
xy) <- sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymExpr sym BaseBoolType, SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
subSignedOF sym
sym SymBV sym w
x SymBV sym w
y
  SymExpr sym BaseBoolType
ysign  <- sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
y
  SymBV sym w
minint <- sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
minSignedBV sym
sym NatRepr w
w
  SymBV sym w
maxint <- sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxSignedBV sym
sym NatRepr w
w
  SymBV sym w
ov_val <- sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
ysign SymBV sym w
maxint SymBV sym w
minint
  sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(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 :: sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedIntMul sym
sym SymBV sym w
x SymBV sym w
y = do
  let w :: NatRepr w
w = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
  (SymBV sym w
hi,SymBV sym w
lo) <- sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
signedWideMultiplyBV sym
sym SymBV sym w
x SymBV sym w
y
  SymBV sym w
zro    <- sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w)
  SymBV sym w
ones   <- sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxUnsignedBV sym
sym NatRepr w
w
  SymExpr sym BaseBoolType
ok_pos <- IO (IO (SymExpr sym BaseBoolType)) -> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (IO (IO (SymExpr sym BaseBoolType))
 -> IO (SymExpr sym BaseBoolType))
-> IO (IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym (SymExpr sym BaseBoolType
 -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
lo)
                              IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> IO (IO (SymExpr sym BaseBoolType))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymBV sym w
hi SymBV sym w
zro
  SymExpr sym BaseBoolType
ok_neg <- IO (IO (SymExpr sym BaseBoolType)) -> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (IO (IO (SymExpr sym BaseBoolType))
 -> IO (SymExpr sym BaseBoolType))
-> IO (IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym (SymExpr sym BaseBoolType
 -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
lo
                              IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> IO (IO (SymExpr sym BaseBoolType))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymBV sym w
hi SymBV sym w
ones
  SymExpr sym BaseBoolType
ov     <- sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym SymExpr sym BaseBoolType
ok_pos SymExpr sym BaseBoolType
ok_neg

  SymBV sym w
minint <- sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
minSignedBV sym
sym NatRepr w
w
  SymBV sym w
maxint <- sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxSignedBV sym
sym NatRepr w
w
  SymExpr sym BaseBoolType
hisign <- sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
hi
  SymBV sym w
ov_val <- sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
hisign SymBV sym w
minint SymBV sym w
maxint
  sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(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 :: sym -> SymBV sym w -> IO (SymBV sym w)
clampedIntNeg sym
sym SymBV sym w
x = do
  let w :: NatRepr w
w = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
  SymBV sym w
minint <- sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
minSignedBV sym
sym NatRepr w
w

  -- return maxint when x == minint, and neg(x) otherwise
  SymExpr sym BaseBoolType
p <- sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymBV sym w
x SymBV sym w
minint
  (sym
 -> SymExpr sym BaseBoolType
 -> SymBV sym w
 -> SymBV sym w
 -> IO (SymBV sym w))
-> sym
-> SymExpr sym BaseBoolType
-> IO (SymBV sym w)
-> IO (SymBV sym w)
-> IO (SymBV sym w)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
p (sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxSignedBV sym
sym NatRepr w
w) (sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(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 :: sym -> SymBV sym w -> IO (SymBV sym w)
clampedIntAbs sym
sym SymBV sym w
x = do
  SymExpr sym BaseBoolType
isNeg  <- sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
x
  (sym
 -> SymExpr sym BaseBoolType
 -> SymBV sym w
 -> SymBV sym w
 -> IO (SymBV sym w))
-> sym
-> SymExpr sym BaseBoolType
-> IO (SymBV sym w)
-> IO (SymBV sym w)
-> IO (SymBV sym w)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
isNeg (sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
clampedIntNeg sym
sym SymBV sym w
x) (SymBV sym w -> IO (SymBV sym w)
forall (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 :: sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedUIntAdd sym
sym SymBV sym w
x SymBV sym w
y = do
  let w :: NatRepr w
w = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
  (SymExpr sym BaseBoolType
ov, SymBV sym w
xy) <- sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymExpr sym BaseBoolType, SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
addUnsignedOF sym
sym SymBV sym w
x SymBV sym w
y
  SymBV sym w
maxint   <- sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxUnsignedBV sym
sym NatRepr w
w
  sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(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 :: sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedUIntSub sym
sym SymBV sym w
x SymBV sym w
y = do
  let w :: NatRepr w
w = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
  SymExpr sym BaseBoolType
no_underflow <- sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUge sym
sym SymBV sym w
x SymBV sym w
y

  (sym
 -> SymExpr sym BaseBoolType
 -> SymBV sym w
 -> SymBV sym w
 -> IO (SymBV sym w))
-> sym
-> SymExpr sym BaseBoolType
-> IO (SymBV sym w)
-> IO (SymBV sym w)
-> IO (SymBV sym w)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte
       sym
sym
       SymExpr sym BaseBoolType
no_underflow
       (sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvSub sym
sym SymBV sym w
x SymBV sym w
y) -- Perform subtraction if y >= x
       (sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (NatRepr w -> BV w
forall (w :: Nat). 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 :: sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedUIntMul sym
sym SymBV sym w
x SymBV sym w
y = do
  let w :: NatRepr w
w = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
  (SymBV sym w
hi, SymBV sym w
lo) <- sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
unsignedWideMultiplyBV sym
sym SymBV sym w
x SymBV sym w
y
  SymBV sym w
maxint   <- sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxUnsignedBV sym
sym NatRepr w
w
  SymExpr sym BaseBoolType
ov       <- sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym SymBV sym w
hi
  sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(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 (tp :: BaseType). e tp -> m (f tp))
-> MatlabSolverFn e a r -> m (MatlabSolverFn f a r)
traverseMatlabSolverFn forall (tp :: BaseType). e tp -> m (f tp)
f MatlabSolverFn e a r
fn_id =
  case MatlabSolverFn e a r
fn_id of
    MatlabSolverFn e a r
BoolOrFn             -> MatlabSolverFn
  f ((EmptyCtx ::> BaseBoolType) ::> BaseBoolType) BaseBoolType
-> m (MatlabSolverFn
        f ((EmptyCtx ::> BaseBoolType) ::> BaseBoolType) BaseBoolType)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MatlabSolverFn
   f ((EmptyCtx ::> BaseBoolType) ::> BaseBoolType) BaseBoolType
 -> m (MatlabSolverFn
         f ((EmptyCtx ::> BaseBoolType) ::> BaseBoolType) BaseBoolType))
-> MatlabSolverFn
     f ((EmptyCtx ::> BaseBoolType) ::> BaseBoolType) BaseBoolType
-> m (MatlabSolverFn
        f ((EmptyCtx ::> BaseBoolType) ::> BaseBoolType) BaseBoolType)
forall a b. (a -> b) -> a -> b
$ MatlabSolverFn
  f ((EmptyCtx ::> BaseBoolType) ::> BaseBoolType) BaseBoolType
forall (f :: BaseType -> Type).
MatlabSolverFn
  f ((EmptyCtx ::> BaseBoolType) ::> BaseBoolType) BaseBoolType
BoolOrFn
    MatlabSolverFn e a r
IsIntegerFn          -> MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType
-> m (MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType
 -> m (MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType))
-> MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType
-> m (MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType)
forall a b. (a -> b) -> a -> b
$ MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType
forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType
IsIntegerFn
    MatlabSolverFn e a r
IntLeFn              -> MatlabSolverFn
  f ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType) BaseBoolType
-> m (MatlabSolverFn
        f
        ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
        BaseBoolType)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MatlabSolverFn
   f ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType) BaseBoolType
 -> m (MatlabSolverFn
         f
         ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
         BaseBoolType))
-> MatlabSolverFn
     f ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType) BaseBoolType
-> m (MatlabSolverFn
        f
        ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
        BaseBoolType)
forall a b. (a -> b) -> a -> b
$ MatlabSolverFn
  f ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType) BaseBoolType
forall (f :: BaseType -> Type).
MatlabSolverFn
  f ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType) BaseBoolType
IntLeFn
    BVToIntegerFn NatRepr w
w      -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
-> m (MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
 -> m (MatlabSolverFn
         f (EmptyCtx ::> BaseBVType w) BaseIntegerType))
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
-> m (MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ NatRepr w
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
forall (w :: Nat) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
BVToIntegerFn NatRepr w
w
    SBVToIntegerFn NatRepr w
w     -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
-> m (MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
 -> m (MatlabSolverFn
         f (EmptyCtx ::> BaseBVType w) BaseIntegerType))
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
-> m (MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ NatRepr w
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
forall (w :: Nat) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
SBVToIntegerFn NatRepr w
w
    MatlabSolverFn e a r
IntegerToRealFn      -> MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType
-> m (MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType
 -> m (MatlabSolverFn
         f (EmptyCtx ::> BaseIntegerType) BaseRealType))
-> MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType
-> m (MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType)
forall a b. (a -> b) -> a -> b
$ MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType
forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType
IntegerToRealFn
    MatlabSolverFn e a r
RealToIntegerFn      -> MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseIntegerType
-> m (MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseIntegerType)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseIntegerType
 -> m (MatlabSolverFn
         f (EmptyCtx ::> BaseRealType) BaseIntegerType))
-> MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseIntegerType
-> m (MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseIntegerType
forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseIntegerType
RealToIntegerFn
    MatlabSolverFn e a r
PredToIntegerFn      -> MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType
-> m (MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType
 -> m (MatlabSolverFn
         f (EmptyCtx ::> BaseBoolType) BaseIntegerType))
-> MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType
-> m (MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType
forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType
PredToIntegerFn
    IntSeqFn  e BaseIntegerType
b e BaseIntegerType
i        -> f BaseIntegerType
-> f BaseIntegerType
-> MatlabSolverFn
     f
     ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
     BaseIntegerType
forall (f :: BaseType -> Type).
f BaseIntegerType
-> f BaseIntegerType
-> MatlabSolverFn
     f
     ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
     BaseIntegerType
IntSeqFn (f BaseIntegerType
 -> f BaseIntegerType
 -> MatlabSolverFn
      f
      ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
      BaseIntegerType)
-> m (f BaseIntegerType)
-> m (f BaseIntegerType
      -> MatlabSolverFn
           f
           ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
           BaseIntegerType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e BaseIntegerType -> m (f BaseIntegerType)
forall (tp :: BaseType). e tp -> m (f tp)
f e BaseIntegerType
b m (f BaseIntegerType
   -> MatlabSolverFn
        f
        ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
        BaseIntegerType)
-> m (f BaseIntegerType)
-> m (MatlabSolverFn
        f
        ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
        BaseIntegerType)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> e BaseIntegerType -> m (f BaseIntegerType)
forall (tp :: BaseType). e tp -> m (f tp)
f e BaseIntegerType
i
    RealSeqFn e BaseRealType
b e BaseRealType
i        -> f BaseRealType
-> f BaseRealType
-> MatlabSolverFn
     f ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType) BaseRealType
forall (f :: BaseType -> Type).
f BaseRealType
-> f BaseRealType
-> MatlabSolverFn
     f ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType) BaseRealType
RealSeqFn (f BaseRealType
 -> f BaseRealType
 -> MatlabSolverFn
      f
      ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
      BaseRealType)
-> m (f BaseRealType)
-> m (f BaseRealType
      -> MatlabSolverFn
           f
           ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
           BaseRealType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e BaseRealType -> m (f BaseRealType)
forall (tp :: BaseType). e tp -> m (f tp)
f e BaseRealType
b m (f BaseRealType
   -> MatlabSolverFn
        f
        ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
        BaseRealType)
-> m (f BaseRealType)
-> m (MatlabSolverFn
        f
        ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
        BaseRealType)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> e BaseRealType -> m (f BaseRealType)
forall (tp :: BaseType). e tp -> m (f tp)
f e BaseRealType
i
    IndicesInRange Assignment OnlyIntRepr (idx ::> itp)
tps Assignment e (idx ::> itp)
a -> Assignment OnlyIntRepr (idx ::> itp)
-> Assignment f (idx ::> itp)
-> MatlabSolverFn f (idx ::> itp) BaseBoolType
forall (idx :: Ctx BaseType) (itp :: BaseType)
       (f :: BaseType -> Type).
Assignment OnlyIntRepr (idx ::> itp)
-> Assignment f (idx ::> itp)
-> MatlabSolverFn f (idx ::> itp) BaseBoolType
IndicesInRange Assignment OnlyIntRepr (idx ::> itp)
tps (Assignment f (idx ::> itp)
 -> MatlabSolverFn f (idx ::> itp) BaseBoolType)
-> m (Assignment f (idx ::> itp))
-> m (MatlabSolverFn f (idx ::> itp) BaseBoolType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (tp :: BaseType). e tp -> m (f tp))
-> Assignment e (idx ::> itp) -> m (Assignment f (idx ::> itp))
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            -> MatlabSolverFn f ((EmptyCtx ::> tp) ::> tp) BaseBoolType
-> m (MatlabSolverFn f ((EmptyCtx ::> tp) ::> tp) BaseBoolType)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MatlabSolverFn f ((EmptyCtx ::> tp) ::> tp) BaseBoolType
 -> m (MatlabSolverFn f ((EmptyCtx ::> tp) ::> tp) BaseBoolType))
-> MatlabSolverFn f ((EmptyCtx ::> tp) ::> tp) BaseBoolType
-> m (MatlabSolverFn f ((EmptyCtx ::> tp) ::> tp) BaseBoolType)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr tp
-> MatlabSolverFn f ((EmptyCtx ::> tp) ::> tp) BaseBoolType
forall (tp :: BaseType) (f :: BaseType -> Type).
BaseTypeRepr tp
-> MatlabSolverFn f ((EmptyCtx ::> tp) ::> tp) BaseBoolType
IsEqFn BaseTypeRepr tp
tp

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

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

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

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

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

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


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

-- | Utilities to make a pair with the same value.
binCtx :: BaseTypeRepr tp -> Ctx.Assignment BaseTypeRepr (EmptyCtx ::> tp ::> tp)
binCtx :: BaseTypeRepr tp
-> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
binCtx BaseTypeRepr tp
tp = Assignment BaseTypeRepr EmptyCtx
forall k (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty Assignment BaseTypeRepr EmptyCtx
-> BaseTypeRepr tp -> Assignment BaseTypeRepr (EmptyCtx ::> tp)
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> BaseTypeRepr tp
tp Assignment BaseTypeRepr (EmptyCtx ::> tp)
-> BaseTypeRepr tp
-> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> BaseTypeRepr tp
tp

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Test 'MatlabSolverFn' values for equality.
testSolverFnEq :: TestEquality f
               => MatlabSolverFn f ax rx
               -> MatlabSolverFn f ay ry
               -> Maybe ((ax ::> rx) :~: (ay ::> ry))
testSolverFnEq :: 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 ( Hashable (f BaseRealType)
         , Hashable (f BaseIntegerType)
         , HashableF 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 :: sym -> SymReal sym -> IO (Pred sym)
realIsNonZero sym
sym = sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realNe sym
sym (sym -> SymReal 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 :: MatlabSolverFn (SymExpr sym) args ret
-> sym -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
evalMatlabSolverFn MatlabSolverFn (SymExpr sym) args ret
f sym
sym =
  case MatlabSolverFn (SymExpr sym) args ret
f of
    MatlabSolverFn (SymExpr sym) args ret
BoolOrFn         -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
 -> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym

    MatlabSolverFn (SymExpr sym) args ret
IsIntegerFn      -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
 -> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym -> SymReal sym -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (Pred sym)
isInteger sym
sym
    MatlabSolverFn (SymExpr sym) args ret
IntLeFn          -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
 -> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym
    BVToIntegerFn{}  -> CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
-> Assignment (SymExpr sym) args -> IO (SymInteger sym)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
 -> Assignment (SymExpr sym) args -> IO (SymInteger sym))
-> CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
-> Assignment (SymExpr sym) args
-> IO (SymInteger sym)
forall a b. (a -> b) -> a -> b
$ sym -> SymBV sym w -> IO (SymInteger sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
bvToInteger sym
sym
    SBVToIntegerFn{} -> CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
-> Assignment (SymExpr sym) args -> IO (SymInteger sym)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
 -> Assignment (SymExpr sym) args -> IO (SymInteger sym))
-> CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
-> Assignment (SymExpr sym) args
-> IO (SymInteger sym)
forall a b. (a -> b) -> a -> b
$ sym -> SymBV sym w -> IO (SymInteger sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
sbvToInteger sym
sym
    MatlabSolverFn (SymExpr sym) args ret
IntegerToRealFn  -> CurryAssignment args (SymExpr sym) (IO (SymReal sym))
-> Assignment (SymExpr sym) args -> IO (SymReal sym)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymReal sym))
 -> Assignment (SymExpr sym) args -> IO (SymReal sym))
-> CurryAssignment args (SymExpr sym) (IO (SymReal sym))
-> Assignment (SymExpr sym) args
-> IO (SymReal sym)
forall a b. (a -> b) -> a -> b
$ sym -> SymInteger sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym
    MatlabSolverFn (SymExpr sym) args ret
RealToIntegerFn  -> CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
-> Assignment (SymExpr sym) args -> IO (SymInteger sym)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
 -> Assignment (SymExpr sym) args -> IO (SymInteger sym))
-> CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
-> Assignment (SymExpr sym) args
-> IO (SymInteger sym)
forall a b. (a -> b) -> a -> b
$ sym -> SymReal sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realToInteger sym
sym
    MatlabSolverFn (SymExpr sym) args ret
PredToIntegerFn  -> CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
-> Assignment (SymExpr sym) args -> IO (SymInteger sym)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
 -> Assignment (SymExpr sym) args -> IO (SymInteger sym))
-> CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
-> Assignment (SymExpr sym) args
-> IO (SymInteger sym)
forall a b. (a -> b) -> a -> b
$ \SymExpr sym BaseBoolType
p ->
      (sym
 -> SymExpr sym BaseBoolType
 -> SymInteger sym
 -> SymInteger sym
 -> IO (SymInteger sym))
-> sym
-> SymExpr sym BaseBoolType
-> IO (SymInteger sym)
-> IO (SymInteger sym)
-> IO (SymInteger sym)
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM sym
-> SymExpr sym BaseBoolType
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
intIte sym
sym SymExpr sym BaseBoolType
p (sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
1) (sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
0)
    IntSeqFn SymInteger sym
b SymInteger sym
inc   -> CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
-> Assignment (SymExpr sym) args -> IO (SymInteger sym)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
 -> Assignment (SymExpr sym) args -> IO (SymInteger sym))
-> CurryAssignment args (SymExpr sym) (IO (SymInteger sym))
-> Assignment (SymExpr sym) args
-> IO (SymInteger sym)
forall a b. (a -> b) -> a -> b
$ \SymInteger sym
idx SymInteger sym
_ -> do
      sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intAdd sym
sym SymInteger sym
b (SymInteger sym -> IO (SymInteger sym))
-> IO (SymInteger sym) -> IO (SymInteger sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMul sym
sym SymInteger sym
inc SymInteger sym
idx
    RealSeqFn SymReal sym
b SymReal sym
inc -> CurryAssignment args (SymExpr sym) (IO (SymReal sym))
-> Assignment (SymExpr sym) args -> IO (SymReal sym)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymReal sym))
 -> Assignment (SymExpr sym) args -> IO (SymReal sym))
-> CurryAssignment args (SymExpr sym) (IO (SymReal sym))
-> Assignment (SymExpr sym) args
-> IO (SymReal sym)
forall a b. (a -> b) -> a -> b
$ \SymInteger sym
_ SymInteger sym
idx -> do
      sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymReal sym
b (SymReal sym -> IO (SymReal sym))
-> IO (SymReal sym) -> IO (SymReal sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
inc (SymReal sym -> IO (SymReal sym))
-> IO (SymReal sym) -> IO (SymReal sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymInteger sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym SymInteger sym
idx
    IndicesInRange Assignment OnlyIntRepr (idx ::> itp)
tps0 Assignment (SymExpr sym) (idx ::> itp)
bnds0 -> \Assignment (SymExpr sym) args
args ->
        Size (idx ::> itp)
-> (forall (tp :: BaseType).
    IO (SymExpr sym BaseBoolType)
    -> Index (idx ::> itp) tp -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> IO (SymExpr sym BaseBoolType)
forall k (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
Ctx.forIndex (Assignment OnlyIntRepr (idx ::> itp) -> Size (idx ::> itp)
forall k (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment OnlyIntRepr (idx ::> itp)
tps0) (Assignment OnlyIntRepr (idx ::> itp)
-> Assignment (SymExpr sym) (idx ::> itp)
-> Assignment (SymExpr sym) (idx ::> itp)
-> IO (SymExpr sym BaseBoolType)
-> Index (idx ::> itp) tp
-> IO (SymExpr sym BaseBoolType)
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
Assignment (SymExpr sym) (idx ::> itp)
args) (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (sym -> SymExpr sym BaseBoolType
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 :: 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 Assignment OnlyIntRepr ctx -> Index ctx tp -> OnlyIntRepr tp
forall k (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i of
                OnlyIntRepr tp
OnlyIntRepr -> do
                  let v :: SymExpr sym tp
v = Assignment (SymExpr sym) ctx
args Assignment (SymExpr sym) ctx -> Index ctx tp -> SymExpr sym tp
forall k (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index ctx tp
i
                  let bnd :: SymExpr sym tp
bnd = Assignment (SymExpr sym) ctx
bnds Assignment (SymExpr sym) ctx -> Index ctx tp -> SymExpr sym tp
forall k (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index ctx tp
i
                  SymInteger sym
one <- sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
1
                  SymExpr sym BaseBoolType
p <- IO (IO (SymExpr sym BaseBoolType)) -> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (IO (IO (SymExpr sym BaseBoolType))
 -> IO (SymExpr sym BaseBoolType))
-> IO (IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym (SymExpr sym BaseBoolType
 -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymInteger sym
one SymExpr sym tp
SymInteger sym
v IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> IO (IO (SymExpr sym BaseBoolType))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymExpr sym tp
SymInteger sym
v SymExpr sym tp
SymInteger sym
bnd
                  sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym SymExpr sym BaseBoolType
p (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (SymExpr sym BaseBoolType)
m
    IsEqFn{} -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
 -> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ \SymExpr sym tp
x SymExpr sym tp
y -> do
      sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym BaseBoolType)
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
_    -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
 -> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym
    ClampedIntNegFn NatRepr w
_  -> CurryAssignment
  args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym (BaseBVType w))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment
   args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
 -> Assignment (SymExpr sym) args
 -> IO (SymExpr sym (BaseBVType w)))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym (BaseBVType w) -> IO (SymExpr sym (BaseBVType w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
clampedIntNeg sym
sym
    ClampedIntAbsFn NatRepr w
_  -> CurryAssignment
  args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym (BaseBVType w))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment
   args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
 -> Assignment (SymExpr sym) args
 -> IO (SymExpr sym (BaseBVType w)))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym (BaseBVType w) -> IO (SymExpr sym (BaseBVType w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
clampedIntAbs sym
sym
    ClampedIntAddFn NatRepr w
_  -> CurryAssignment
  args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym (BaseBVType w))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment
   args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
 -> Assignment (SymExpr sym) args
 -> IO (SymExpr sym (BaseBVType w)))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedIntAdd sym
sym
    ClampedIntSubFn NatRepr w
_  -> CurryAssignment
  args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym (BaseBVType w))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment
   args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
 -> Assignment (SymExpr sym) args
 -> IO (SymExpr sym (BaseBVType w)))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedIntSub sym
sym
    ClampedIntMulFn NatRepr w
_  -> CurryAssignment
  args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym (BaseBVType w))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment
   args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
 -> Assignment (SymExpr sym) args
 -> IO (SymExpr sym (BaseBVType w)))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedIntMul sym
sym
    ClampedUIntAddFn NatRepr w
_ -> CurryAssignment
  args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym (BaseBVType w))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment
   args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
 -> Assignment (SymExpr sym) args
 -> IO (SymExpr sym (BaseBVType w)))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedUIntAdd sym
sym
    ClampedUIntSubFn NatRepr w
_ -> CurryAssignment
  args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym (BaseBVType w))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment
   args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
 -> Assignment (SymExpr sym) args
 -> IO (SymExpr sym (BaseBVType w)))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedUIntSub sym
sym
    ClampedUIntMulFn NatRepr w
_ -> CurryAssignment
  args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym (BaseBVType w))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment
   args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
 -> Assignment (SymExpr sym) args
 -> IO (SymExpr sym (BaseBVType w)))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedUIntMul sym
sym

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

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

    RealToSBVFn NatRepr w
w      -> CurryAssignment
  args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym (BaseBVType w))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment
   args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
 -> Assignment (SymExpr sym) args
 -> IO (SymExpr sym (BaseBVType w)))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ \SymReal sym
v -> sym -> SymReal sym -> NatRepr w -> IO (SymExpr sym (BaseBVType w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
realToSBV sym
sym SymReal sym
v NatRepr w
w
    RealToUBVFn NatRepr w
w      -> CurryAssignment
  args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym (BaseBVType w))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment
   args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
 -> Assignment (SymExpr sym) args
 -> IO (SymExpr sym (BaseBVType w)))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ \SymReal sym
v -> sym -> SymReal sym -> NatRepr w -> IO (SymExpr sym (BaseBVType w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
realToBV  sym
sym SymReal sym
v NatRepr w
w
    PredToBVFn  NatRepr w
w      -> CurryAssignment
  args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym (BaseBVType w))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment
   args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
 -> Assignment (SymExpr sym) args
 -> IO (SymExpr sym (BaseBVType w)))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym (BaseBVType w)))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym (BaseBVType w))
forall a b. (a -> b) -> a -> b
$ \SymExpr sym BaseBoolType
v -> sym
-> SymExpr sym BaseBoolType
-> NatRepr w
-> IO (SymExpr sym (BaseBVType w))
forall sym (w :: Nat).
(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  -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
 -> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ \SymExpr sym BaseComplexType
x -> do
      (SymReal sym
real_x :+ SymReal sym
imag_x) <- sym -> SymExpr sym BaseComplexType -> IO (Complex (SymReal sym))
forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymExpr sym BaseComplexType
x
      IO (IO (SymExpr sym BaseBoolType)) -> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (IO (IO (SymExpr sym BaseBoolType))
 -> IO (SymExpr sym BaseBoolType))
-> IO (IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym (SymExpr sym BaseBoolType
 -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymReal sym -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (Pred sym)
realIsNonZero sym
sym SymReal sym
real_x IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> IO (IO (SymExpr sym BaseBoolType))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym -> SymReal sym -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (Pred sym)
realIsNonZero sym
sym SymReal sym
imag_x
    MatlabSolverFn (SymExpr sym) args ret
CplxIsRealFn     -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
 -> Assignment (SymExpr sym) args -> IO (SymExpr sym BaseBoolType))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym BaseBoolType))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym -> SymExpr sym BaseComplexType -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Pred sym)
isReal sym
sym
    MatlabSolverFn (SymExpr sym) args ret
RealToComplexFn  -> CurryAssignment
  args (SymExpr sym) (IO (SymExpr sym BaseComplexType))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym BaseComplexType)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment
   args (SymExpr sym) (IO (SymExpr sym BaseComplexType))
 -> Assignment (SymExpr sym) args
 -> IO (SymExpr sym BaseComplexType))
-> CurryAssignment
     args (SymExpr sym) (IO (SymExpr sym BaseComplexType))
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym BaseComplexType)
forall a b. (a -> b) -> a -> b
$ sym -> SymReal sym -> IO (SymExpr sym BaseComplexType)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymCplx sym)
cplxFromReal sym
sym
    MatlabSolverFn (SymExpr sym) args ret
RealPartOfCplxFn -> CurryAssignment args (SymExpr sym) (IO (SymReal sym))
-> Assignment (SymExpr sym) args -> IO (SymReal sym)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymReal sym))
 -> Assignment (SymExpr sym) args -> IO (SymReal sym))
-> CurryAssignment args (SymExpr sym) (IO (SymReal sym))
-> Assignment (SymExpr sym) args
-> IO (SymReal sym)
forall a b. (a -> b) -> a -> b
$ sym -> SymExpr sym BaseComplexType -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymReal sym)
getRealPart sym
sym
    MatlabSolverFn (SymExpr sym) args ret
ImagPartOfCplxFn -> CurryAssignment args (SymExpr sym) (IO (SymReal sym))
-> Assignment (SymExpr sym) args -> IO (SymReal sym)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment (CurryAssignment args (SymExpr sym) (IO (SymReal sym))
 -> Assignment (SymExpr sym) args -> IO (SymReal sym))
-> CurryAssignment args (SymExpr sym) (IO (SymReal sym))
-> Assignment (SymExpr sym) args
-> IO (SymReal sym)
forall a b. (a -> b) -> a -> b
$ sym -> SymExpr sym BaseComplexType -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymReal sym)
getImagPart sym
sym

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

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

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

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