{-# 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(..)
, 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
clampedIntAdd :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
clampedIntAdd :: forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedIntAdd sym
sym SymBV sym w
x SymBV sym w
y = do
let w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
forall (n :: Natural) (m :: Natural) a.
NatRepr n -> NatRepr m -> ((m <= (n + m)) => a) -> a
withAddPrefixLeq NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat :: NatRepr 1) forall a b. (a -> b) -> a -> b
$ do
let w' :: NatRepr (w + 1)
w' = forall (n :: Natural). NatRepr n -> NatRepr (n + 1)
incNat NatRepr w
w
SymExpr sym (BaseBVType (w + 1))
x' <- forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr (w + 1)
w' SymBV sym w
x
SymExpr sym (BaseBVType (w + 1))
y' <- forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr (w + 1)
w' SymBV sym w
y
SymExpr sym (BaseBVType (w + 1))
r' <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd sym
sym SymExpr sym (BaseBVType (w + 1))
x' SymExpr sym (BaseBVType (w + 1))
y'
SymExpr sym BaseBoolType
too_high <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSgt sym
sym SymExpr sym (BaseBVType (w + 1))
r' forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + 1)
w' (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr (w + 1)
w')
SymBV sym w
max_int <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr w
w)
SymExpr sym BaseBoolType
too_low <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymExpr sym (BaseBVType (w + 1))
r' forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (w + 1)
w' (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr (w + 1)
w')
SymBV sym w
min_int <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr w
w)
SymBV sym w
r <- forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr w
w SymExpr sym (BaseBVType (w + 1))
r'
SymBV sym w
r_low <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
too_low SymBV sym w
min_int SymBV sym w
r
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
too_high SymBV sym w
max_int SymBV sym w
r_low
clampedIntSub :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
clampedIntSub :: forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedIntSub sym
sym SymBV sym w
x SymBV sym w
y = do
let w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
(SymExpr sym BaseBoolType
ov, SymBV sym w
xy) <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
subSignedOF sym
sym SymBV sym w
x SymBV sym w
y
SymExpr sym BaseBoolType
ysign <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
y
SymBV sym w
minint <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
minSignedBV sym
sym NatRepr w
w
SymBV sym w
maxint <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxSignedBV sym
sym NatRepr w
w
SymBV sym w
ov_val <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
ysign SymBV sym w
maxint SymBV sym w
minint
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
ov SymBV sym w
ov_val SymBV sym w
xy
clampedIntMul :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
clampedIntMul :: forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedIntMul sym
sym SymBV sym w
x SymBV sym w
y = do
let w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
(SymBV sym w
hi,SymBV sym w
lo) <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
signedWideMultiplyBV sym
sym SymBV sym w
x SymBV sym w
y
SymBV sym w
zro <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w)
SymBV sym w
ones <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxUnsignedBV sym
sym NatRepr w
w
SymExpr sym BaseBoolType
ok_pos <- forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
lo)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymBV sym w
hi SymBV sym w
zro
SymExpr sym BaseBoolType
ok_neg <- forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
lo
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymBV sym w
hi SymBV sym w
ones
SymExpr sym BaseBoolType
ov <- forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym SymExpr sym BaseBoolType
ok_pos SymExpr sym BaseBoolType
ok_neg
SymBV sym w
minint <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
minSignedBV sym
sym NatRepr w
w
SymBV sym w
maxint <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxSignedBV sym
sym NatRepr w
w
SymExpr sym BaseBoolType
hisign <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
hi
SymBV sym w
ov_val <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
hisign SymBV sym w
minint SymBV sym w
maxint
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
ov SymBV sym w
ov_val SymBV sym w
lo
clampedIntNeg :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> IO (SymBV sym w)
clampedIntNeg :: forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
clampedIntNeg sym
sym SymBV sym w
x = do
let w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
SymBV sym w
minint <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
minSignedBV sym
sym NatRepr w
w
SymExpr sym BaseBoolType
p <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymBV sym w
x SymBV sym w
minint
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
p (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxSignedBV sym
sym NatRepr w
w) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
bvNeg sym
sym SymBV sym w
x)
clampedIntAbs :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> IO (SymBV sym w)
clampedIntAbs :: forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
clampedIntAbs sym
sym SymBV sym w
x = do
SymExpr sym BaseBoolType
isNeg <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym SymBV sym w
x
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
isNeg (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
clampedIntNeg sym
sym SymBV sym w
x) (forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymBV sym w
x)
clampedUIntAdd :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
clampedUIntAdd :: forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedUIntAdd sym
sym SymBV sym w
x SymBV sym w
y = do
let w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
(SymExpr sym BaseBoolType
ov, SymBV sym w
xy) <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
addUnsignedOF sym
sym SymBV sym w
x SymBV sym w
y
SymBV sym w
maxint <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxUnsignedBV sym
sym NatRepr w
w
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
ov SymBV sym w
maxint SymBV sym w
xy
clampedUIntSub :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
clampedUIntSub :: forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedUIntSub sym
sym SymBV sym w
x SymBV sym w
y = do
let w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
SymExpr sym BaseBoolType
no_underflow <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUge sym
sym SymBV sym w
x SymBV sym w
y
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte
sym
sym
SymExpr sym BaseBoolType
no_underflow
(forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvSub sym
sym SymBV sym w
x SymBV sym w
y)
(forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w))
clampedUIntMul :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
clampedUIntMul :: forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedUIntMul sym
sym SymBV sym w
x SymBV sym w
y = do
let w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
x
(SymBV sym w
hi, SymBV sym w
lo) <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
unsignedWideMultiplyBV sym
sym SymBV sym w
x SymBV sym w
y
SymBV sym w
maxint <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> IO (SymBV sym w)
maxUnsignedBV sym
sym NatRepr w
w
SymExpr sym BaseBoolType
ov <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym SymBV sym w
hi
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
ov SymBV sym w
maxint SymBV sym w
lo
data MatlabSolverFn (f :: BaseType -> Type) args ret where
BoolOrFn :: MatlabSolverFn f (EmptyCtx ::> BaseBoolType ::> BaseBoolType) BaseBoolType
IsIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType
IntLeFn :: MatlabSolverFn f (EmptyCtx ::> BaseIntegerType ::> BaseIntegerType) BaseBoolType
BVToIntegerFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
SBVToIntegerFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
IntegerToRealFn :: MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType
RealToIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseIntegerType
PredToIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType
IntSeqFn :: !(f BaseIntegerType)
-> !(f BaseIntegerType)
-> MatlabSolverFn f (EmptyCtx ::> BaseIntegerType ::> BaseIntegerType) BaseIntegerType
RealSeqFn :: !(f BaseRealType)
-> !(f BaseRealType)
-> MatlabSolverFn f (EmptyCtx ::> BaseIntegerType ::> BaseIntegerType) BaseRealType
IndicesInRange :: !(Assignment OnlyIntRepr (idx ::> itp))
-> !(Assignment f (idx ::> itp))
-> MatlabSolverFn f (idx ::> itp) BaseBoolType
IsEqFn :: !(BaseTypeRepr tp)
-> MatlabSolverFn f (EmptyCtx ::> tp ::> tp) BaseBoolType
BVIsNonZeroFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseBoolType
ClampedIntNegFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)
ClampedIntAbsFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)
ClampedIntAddFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f
(EmptyCtx ::> BaseBVType w ::> BaseBVType w)
(BaseBVType w)
ClampedIntSubFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f
(EmptyCtx ::> BaseBVType w ::> BaseBVType w)
(BaseBVType w)
ClampedIntMulFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f
(EmptyCtx ::> BaseBVType w ::> BaseBVType w)
(BaseBVType w)
ClampedUIntAddFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f
(EmptyCtx ::> BaseBVType w ::> BaseBVType w)
(BaseBVType w)
ClampedUIntSubFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f
(EmptyCtx ::> BaseBVType w ::> BaseBVType w)
(BaseBVType w)
ClampedUIntMulFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f
(EmptyCtx ::> BaseBVType w ::> BaseBVType w)
(BaseBVType w)
IntSetWidthFn :: (1 <= m, 1 <= n)
=> !(NatRepr m)
-> !(NatRepr n)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
UIntSetWidthFn :: (1 <= m, 1 <= n)
=> !(NatRepr m)
-> !(NatRepr n)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
UIntToIntFn :: (1 <= m, 1 <= n)
=> !(NatRepr m)
-> !(NatRepr n)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
IntToUIntFn :: (1 <= m, 1 <= n)
=> !(NatRepr m)
-> !(NatRepr n)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
RealIsNonZeroFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType
RealCosFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseRealType
RealSinFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseRealType
RealToSBVFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseRealType) (BaseBVType w)
RealToUBVFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseRealType) (BaseBVType w)
PredToBVFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseBoolType) (BaseBVType w)
CplxIsNonZeroFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseBoolType
CplxIsRealFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseBoolType
RealToComplexFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseComplexType
RealPartOfCplxFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType
ImagPartOfCplxFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType
CplxNegFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
CplxAddFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType ::> BaseComplexType)
BaseComplexType
CplxSubFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType ::> BaseComplexType)
BaseComplexType
CplxMulFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType ::> BaseComplexType)
BaseComplexType
CplxRoundFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
CplxFloorFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
CplxCeilFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
CplxMagFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType
CplxSqrtFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
CplxExpFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType)
BaseComplexType
CplxLogFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType)
BaseComplexType
CplxLogBaseFn :: !Integer
-> MatlabSolverFn f
(EmptyCtx ::> BaseComplexType)
BaseComplexType
CplxSinFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType)
BaseComplexType
CplxCosFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType)
BaseComplexType
CplxTanFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType)
BaseComplexType
$(return [])
traverseMatlabSolverFn :: Applicative m
=> (forall tp . e tp -> m (f tp))
-> MatlabSolverFn e a r
-> m (MatlabSolverFn f a r)
traverseMatlabSolverFn :: forall (m :: Type -> Type) (e :: BaseType -> Type)
(f :: BaseType -> Type) (a :: Ctx BaseType) (r :: BaseType).
Applicative m =>
(forall (tp :: BaseType). e tp -> m (f tp))
-> MatlabSolverFn e a r -> m (MatlabSolverFn f a r)
traverseMatlabSolverFn forall (tp :: BaseType). e tp -> m (f tp)
f MatlabSolverFn e a r
fn_id =
case MatlabSolverFn e a r
fn_id of
MatlabSolverFn e a r
BoolOrFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn
f ((EmptyCtx ::> BaseBoolType) '::> BaseBoolType) BaseBoolType
BoolOrFn
MatlabSolverFn e a r
IsIntegerFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseBoolType
IsIntegerFn
MatlabSolverFn e a r
IntLeFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn
f
((EmptyCtx ::> BaseIntegerType) '::> BaseIntegerType)
BaseBoolType
IntLeFn
BVToIntegerFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
BVToIntegerFn NatRepr w
w
SBVToIntegerFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
SBVToIntegerFn NatRepr w
w
MatlabSolverFn e a r
IntegerToRealFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType
IntegerToRealFn
MatlabSolverFn e a r
RealToIntegerFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseIntegerType
RealToIntegerFn
MatlabSolverFn e a r
PredToIntegerFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType
PredToIntegerFn
IntSeqFn e BaseIntegerType
b e BaseIntegerType
i -> forall (f :: BaseType -> Type).
f BaseIntegerType
-> f BaseIntegerType
-> MatlabSolverFn
f
((EmptyCtx ::> BaseIntegerType) '::> BaseIntegerType)
BaseIntegerType
IntSeqFn forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tp :: BaseType). e tp -> m (f tp)
f e BaseIntegerType
b forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (tp :: BaseType). e tp -> m (f tp)
f e BaseIntegerType
i
RealSeqFn e BaseRealType
b e BaseRealType
i -> forall (f :: BaseType -> Type).
f BaseRealType
-> f BaseRealType
-> MatlabSolverFn
f
((EmptyCtx ::> BaseIntegerType) '::> BaseIntegerType)
BaseRealType
RealSeqFn forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tp :: BaseType). e tp -> m (f tp)
f e BaseRealType
b forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (tp :: BaseType). e tp -> m (f tp)
f e BaseRealType
i
IndicesInRange Assignment OnlyIntRepr (idx '::> itp)
tps Assignment e (idx '::> itp)
a -> forall (w :: Ctx BaseType) (n :: BaseType) (f :: BaseType -> Type).
Assignment OnlyIntRepr (w ::> n)
-> Assignment f (w ::> n)
-> MatlabSolverFn f (w ::> n) BaseBoolType
IndicesInRange Assignment OnlyIntRepr (idx '::> itp)
tps forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC forall (tp :: BaseType). e tp -> m (f tp)
f Assignment e (idx '::> itp)
a
IsEqFn BaseTypeRepr tp
tp -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: BaseType) (f :: BaseType -> Type).
BaseTypeRepr w
-> MatlabSolverFn f ((EmptyCtx ::> w) ::> w) BaseBoolType
IsEqFn BaseTypeRepr tp
tp
BVIsNonZeroFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseBoolType
BVIsNonZeroFn NatRepr w
w
ClampedIntNegFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)
ClampedIntNegFn NatRepr w
w
ClampedIntAbsFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)
ClampedIntAbsFn NatRepr w
w
ClampedIntAddFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn
f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
ClampedIntAddFn NatRepr w
w
ClampedIntSubFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn
f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
ClampedIntSubFn NatRepr w
w
ClampedIntMulFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn
f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
ClampedIntMulFn NatRepr w
w
ClampedUIntAddFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn
f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
ClampedUIntAddFn NatRepr w
w
ClampedUIntSubFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn
f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
ClampedUIntSubFn NatRepr w
w
ClampedUIntMulFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn
f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
ClampedUIntMulFn NatRepr w
w
IntSetWidthFn NatRepr m
i NatRepr n
o -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (n :: Natural) (f :: BaseType -> Type).
(1 <= w, 1 <= n) =>
NatRepr w
-> NatRepr n
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType n)
IntSetWidthFn NatRepr m
i NatRepr n
o
UIntSetWidthFn NatRepr m
i NatRepr n
o -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (n :: Natural) (f :: BaseType -> Type).
(1 <= w, 1 <= n) =>
NatRepr w
-> NatRepr n
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType n)
UIntSetWidthFn NatRepr m
i NatRepr n
o
UIntToIntFn NatRepr m
i NatRepr n
o -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (n :: Natural) (f :: BaseType -> Type).
(1 <= w, 1 <= n) =>
NatRepr w
-> NatRepr n
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType n)
UIntToIntFn NatRepr m
i NatRepr n
o
IntToUIntFn NatRepr m
i NatRepr n
o -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (n :: Natural) (f :: BaseType -> Type).
(1 <= w, 1 <= n) =>
NatRepr w
-> NatRepr n
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType n)
IntToUIntFn NatRepr m
i NatRepr n
o
MatlabSolverFn e a r
RealCosFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseRealType
RealCosFn
MatlabSolverFn e a r
RealSinFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseRealType
RealSinFn
MatlabSolverFn e a r
RealIsNonZeroFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseBoolType
RealIsNonZeroFn
RealToSBVFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn f (EmptyCtx '::> BaseRealType) (BaseBVType w)
RealToSBVFn NatRepr w
w
RealToUBVFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn f (EmptyCtx '::> BaseRealType) (BaseBVType w)
RealToUBVFn NatRepr w
w
PredToBVFn NatRepr w
w -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Natural) (f :: BaseType -> Type).
(1 <= w) =>
NatRepr w
-> MatlabSolverFn f (EmptyCtx ::> BaseBoolType) (BaseBVType w)
PredToBVFn NatRepr w
w
MatlabSolverFn e a r
CplxIsNonZeroFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseBoolType
CplxIsNonZeroFn
MatlabSolverFn e a r
CplxIsRealFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseBoolType
CplxIsRealFn
MatlabSolverFn e a r
RealToComplexFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseRealType) BaseComplexType
RealToComplexFn
MatlabSolverFn e a r
RealPartOfCplxFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseRealType
RealPartOfCplxFn
MatlabSolverFn e a r
ImagPartOfCplxFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseRealType
ImagPartOfCplxFn
MatlabSolverFn e a r
CplxNegFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxNegFn
MatlabSolverFn e a r
CplxAddFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn
f
((EmptyCtx '::> BaseComplexType) '::> BaseComplexType)
BaseComplexType
CplxAddFn
MatlabSolverFn e a r
CplxSubFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn
f
((EmptyCtx '::> BaseComplexType) '::> BaseComplexType)
BaseComplexType
CplxSubFn
MatlabSolverFn e a r
CplxMulFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn
f
((EmptyCtx '::> BaseComplexType) '::> BaseComplexType)
BaseComplexType
CplxMulFn
MatlabSolverFn e a r
CplxRoundFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxRoundFn
MatlabSolverFn e a r
CplxFloorFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxFloorFn
MatlabSolverFn e a r
CplxCeilFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxCeilFn
MatlabSolverFn e a r
CplxMagFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseRealType
CplxMagFn
MatlabSolverFn e a r
CplxSqrtFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxSqrtFn
MatlabSolverFn e a r
CplxExpFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxExpFn
MatlabSolverFn e a r
CplxLogFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxLogFn
CplxLogBaseFn Integer
b -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
Integer
-> MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxLogBaseFn Integer
b
MatlabSolverFn e a r
CplxSinFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxSinFn
MatlabSolverFn e a r
CplxCosFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxCosFn
MatlabSolverFn e a r
CplxTanFn -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: BaseType -> Type).
MatlabSolverFn f (EmptyCtx '::> BaseComplexType) BaseComplexType
CplxTanFn
binCtx :: BaseTypeRepr tp -> Ctx.Assignment BaseTypeRepr (EmptyCtx ::> tp ::> tp)
binCtx :: forall (tp :: BaseType).
BaseTypeRepr tp
-> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
binCtx BaseTypeRepr tp
tp = forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> BaseTypeRepr tp
tp forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> BaseTypeRepr tp
tp
matlabSolverArgTypes :: MatlabSolverFn f args ret -> Assignment BaseTypeRepr args
matlabSolverArgTypes :: forall (f :: BaseType -> Type) (args :: Ctx BaseType)
(ret :: BaseType).
MatlabSolverFn f args ret -> Assignment BaseTypeRepr args
matlabSolverArgTypes MatlabSolverFn f args ret
f =
case MatlabSolverFn f args ret
f of
MatlabSolverFn f args ret
BoolOrFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
IsIntegerFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
IntLeFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
BVToIntegerFn NatRepr w
w -> forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)
SBVToIntegerFn NatRepr w
w -> forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)
MatlabSolverFn f args ret
IntegerToRealFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
RealToIntegerFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
PredToIntegerFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
IntSeqFn{} -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
IndicesInRange Assignment OnlyIntRepr (idx '::> itp)
tps Assignment f (idx '::> itp)
_ -> forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC forall (tp :: BaseType). OnlyIntRepr tp -> BaseTypeRepr tp
toBaseTypeRepr Assignment OnlyIntRepr (idx '::> itp)
tps
RealSeqFn f BaseRealType
_ f BaseRealType
_ -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
IsEqFn BaseTypeRepr tp
tp -> forall (tp :: BaseType).
BaseTypeRepr tp
-> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
binCtx BaseTypeRepr tp
tp
BVIsNonZeroFn NatRepr w
w -> forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)
ClampedIntNegFn NatRepr w
w -> forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)
ClampedIntAbsFn NatRepr w
w -> forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)
ClampedIntAddFn NatRepr w
w -> forall (tp :: BaseType).
BaseTypeRepr tp
-> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
binCtx (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)
ClampedIntSubFn NatRepr w
w -> forall (tp :: BaseType).
BaseTypeRepr tp
-> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
binCtx (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)
ClampedIntMulFn NatRepr w
w -> forall (tp :: BaseType).
BaseTypeRepr tp
-> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
binCtx (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)
ClampedUIntAddFn NatRepr w
w -> forall (tp :: BaseType).
BaseTypeRepr tp
-> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
binCtx (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)
ClampedUIntSubFn NatRepr w
w -> forall (tp :: BaseType).
BaseTypeRepr tp
-> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
binCtx (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)
ClampedUIntMulFn NatRepr w
w -> forall (tp :: BaseType).
BaseTypeRepr tp
-> Assignment BaseTypeRepr ((EmptyCtx ::> tp) ::> tp)
binCtx (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)
IntSetWidthFn NatRepr m
i NatRepr n
_ -> forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr m
i)
UIntSetWidthFn NatRepr m
i NatRepr n
_ -> forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr m
i)
UIntToIntFn NatRepr m
i NatRepr n
_ -> forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr m
i)
IntToUIntFn NatRepr m
i NatRepr n
_ -> forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr m
i)
MatlabSolverFn f args ret
RealCosFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
RealSinFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
RealIsNonZeroFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
RealToSBVFn NatRepr w
_ -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
RealToUBVFn NatRepr w
_ -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
PredToBVFn NatRepr w
_ -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxIsNonZeroFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxIsRealFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
RealToComplexFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
RealPartOfCplxFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
ImagPartOfCplxFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxNegFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxAddFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxSubFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxMulFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxRoundFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxFloorFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxCeilFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxMagFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxSqrtFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxExpFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxLogFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
CplxLogBaseFn Integer
_ -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxSinFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxCosFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxTanFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
matlabSolverReturnType :: MatlabSolverFn f args ret -> BaseTypeRepr ret
matlabSolverReturnType :: forall (f :: BaseType -> Type) (args :: Ctx BaseType)
(ret :: BaseType).
MatlabSolverFn f args ret -> BaseTypeRepr ret
matlabSolverReturnType MatlabSolverFn f args ret
f =
case MatlabSolverFn f args ret
f of
MatlabSolverFn f args ret
BoolOrFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
IsIntegerFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
IntLeFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
BVToIntegerFn{} -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
SBVToIntegerFn{} -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
IntegerToRealFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
RealToIntegerFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
PredToIntegerFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
IntSeqFn{} -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
IndicesInRange{} -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
RealSeqFn f BaseRealType
_ f BaseRealType
_ -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
IsEqFn{} -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
BVIsNonZeroFn NatRepr w
_ -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
ClampedIntNegFn NatRepr w
w -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w
ClampedIntAbsFn NatRepr w
w -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w
ClampedIntAddFn NatRepr w
w -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w
ClampedIntSubFn NatRepr w
w -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w
ClampedIntMulFn NatRepr w
w -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w
ClampedUIntAddFn NatRepr w
w -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w
ClampedUIntSubFn NatRepr w
w -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w
ClampedUIntMulFn NatRepr w
w -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w
IntSetWidthFn NatRepr m
_ NatRepr n
o -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr n
o
UIntSetWidthFn NatRepr m
_ NatRepr n
o -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr n
o
UIntToIntFn NatRepr m
_ NatRepr n
o -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr n
o
IntToUIntFn NatRepr m
_ NatRepr n
o -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr n
o
MatlabSolverFn f args ret
RealCosFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
RealSinFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
RealIsNonZeroFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
RealToSBVFn NatRepr w
w -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w
RealToUBVFn NatRepr w
w -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w
PredToBVFn NatRepr w
w -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w
MatlabSolverFn f args ret
CplxIsNonZeroFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxIsRealFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
RealToComplexFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
RealPartOfCplxFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
ImagPartOfCplxFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxNegFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxAddFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxSubFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxMulFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxRoundFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxFloorFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxCeilFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxMagFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxSqrtFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxExpFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxLogFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
CplxLogBaseFn Integer
_ -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxSinFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxCosFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
MatlabSolverFn f args ret
CplxTanFn -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
ppMatlabSolverFn :: IsExpr f => MatlabSolverFn f a r -> Doc ann
ppMatlabSolverFn :: forall (f :: BaseType -> Type) (a :: Ctx BaseType) (r :: BaseType)
ann.
IsExpr f =>
MatlabSolverFn f a r -> Doc ann
ppMatlabSolverFn MatlabSolverFn f a r
f =
case MatlabSolverFn f a r
f of
MatlabSolverFn f a r
BoolOrFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"bool_or"
MatlabSolverFn f a r
IsIntegerFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"is_integer"
MatlabSolverFn f a r
IntLeFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"int_le"
BVToIntegerFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"bv_to_int" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
SBVToIntegerFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"sbv_to_int" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
MatlabSolverFn f a r
IntegerToRealFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"integer_to_real"
MatlabSolverFn f a r
RealToIntegerFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"real_to_integer"
MatlabSolverFn f a r
PredToIntegerFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"pred_to_integer"
IntSeqFn f BaseIntegerType
b f BaseIntegerType
i -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"nat_seq" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr f BaseIntegerType
b forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr f BaseIntegerType
i
RealSeqFn f BaseRealType
b f BaseRealType
i -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"real_seq" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr f BaseRealType
b forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr f BaseRealType
i
IndicesInRange Assignment OnlyIntRepr (idx '::> itp)
_ Assignment f (idx '::> itp)
bnds ->
forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty String
"indices_in_range" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. [Doc ann] -> Doc ann
sep (forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr Assignment f (idx '::> itp)
bnds))
IsEqFn{} -> forall a ann. Pretty a => a -> Doc ann
pretty String
"is_eq"
BVIsNonZeroFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"bv_is_nonzero" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
ClampedIntNegFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"clamped_int_neg" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
ClampedIntAbsFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"clamped_neg_abs" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
ClampedIntAddFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"clamped_int_add" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
ClampedIntSubFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"clamped_int_sub" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
ClampedIntMulFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"clamped_int_mul" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
ClampedUIntAddFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"clamped_uint_add" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
ClampedUIntSubFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"clamped_uint_sub" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
ClampedUIntMulFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"clamped_uint_mul" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
IntSetWidthFn NatRepr m
i NatRepr n
o -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"int_set_width" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr m
i forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr n
o
UIntSetWidthFn NatRepr m
i NatRepr n
o -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"uint_set_width" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr m
i forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr n
o
UIntToIntFn NatRepr m
i NatRepr n
o -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"uint_to_int" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr m
i forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr n
o
IntToUIntFn NatRepr m
i NatRepr n
o -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"int_to_uint" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr m
i forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr n
o
MatlabSolverFn f a r
RealCosFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"real_cos"
MatlabSolverFn f a r
RealSinFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"real_sin"
MatlabSolverFn f a r
RealIsNonZeroFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"real_is_nonzero"
RealToSBVFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"real_to_sbv" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
RealToUBVFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"real_to_sbv" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
PredToBVFn NatRepr w
w -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"pred_to_bv" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr NatRepr w
w
MatlabSolverFn f a r
CplxIsNonZeroFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_is_nonzero"
MatlabSolverFn f a r
CplxIsRealFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_is_real"
MatlabSolverFn f a r
RealToComplexFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"real_to_complex"
MatlabSolverFn f a r
RealPartOfCplxFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"real_part_of_complex"
MatlabSolverFn f a r
ImagPartOfCplxFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"imag_part_of_complex"
MatlabSolverFn f a r
CplxNegFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_neg"
MatlabSolverFn f a r
CplxAddFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_add"
MatlabSolverFn f a r
CplxSubFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_sub"
MatlabSolverFn f a r
CplxMulFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_mul"
MatlabSolverFn f a r
CplxRoundFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_round"
MatlabSolverFn f a r
CplxFloorFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_floor"
MatlabSolverFn f a r
CplxCeilFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_ceil"
MatlabSolverFn f a r
CplxMagFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_mag"
MatlabSolverFn f a r
CplxSqrtFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_sqrt"
MatlabSolverFn f a r
CplxExpFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_exp"
MatlabSolverFn f a r
CplxLogFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_log"
CplxLogBaseFn Integer
b -> forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_log_base" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Integer
b
MatlabSolverFn f a r
CplxSinFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_sin"
MatlabSolverFn f a r
CplxCosFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_cos"
MatlabSolverFn f a r
CplxTanFn -> forall a ann. Pretty a => a -> Doc ann
pretty String
"cplx_tan"
ppNatRepr :: NatRepr w -> Doc ann
ppNatRepr :: forall (w :: Natural) ann. NatRepr w -> Doc ann
ppNatRepr = forall a ann. Show a => a -> Doc ann
viaShow
testSolverFnEq :: TestEquality f
=> MatlabSolverFn f ax rx
-> MatlabSolverFn f ay ry
-> Maybe ((ax ::> rx) :~: (ay ::> ry))
testSolverFnEq :: forall (f :: BaseType -> Type) (ax :: Ctx BaseType)
(rx :: BaseType) (ay :: Ctx BaseType) (ry :: BaseType).
TestEquality f =>
MatlabSolverFn f ax rx
-> MatlabSolverFn f ay ry -> Maybe ((ax ::> rx) :~: (ay ::> ry))
testSolverFnEq = $(structuralTypeEquality [t|MatlabSolverFn|]
[ ( DataArg 0 `TypeApp` AnyType
, [|testEquality|]
)
, ( ConType [t|NatRepr|] `TypeApp` AnyType
, [|testEquality|]
)
, ( ConType [t|Assignment|] `TypeApp` AnyType `TypeApp` AnyType
, [|testEquality|]
)
, ( ConType [t|BaseTypeRepr|] `TypeApp` AnyType
, [|testEquality|]
)
]
)
instance TestEquality f => Eq (MatlabSolverFn f args tp) where
MatlabSolverFn f args tp
x == :: MatlabSolverFn f args tp -> MatlabSolverFn f args tp -> Bool
== MatlabSolverFn f args tp
y = forall a. Maybe a -> Bool
isJust (forall (f :: BaseType -> Type) (ax :: Ctx BaseType)
(rx :: BaseType) (ay :: Ctx BaseType) (ry :: BaseType).
TestEquality f =>
MatlabSolverFn f ax rx
-> MatlabSolverFn f ay ry -> Maybe ((ax ::> rx) :~: (ay ::> ry))
testSolverFnEq MatlabSolverFn f args tp
x MatlabSolverFn f args tp
y)
instance ( Hashable (f BaseRealType)
, Hashable (f BaseIntegerType)
, HashableF f
, TestEquality f
)
=> Hashable (MatlabSolverFn f args tp) where
hashWithSalt :: Int -> MatlabSolverFn f args tp -> Int
hashWithSalt = $(structuralHashWithSalt [t|MatlabSolverFn|] [])
realIsNonZero :: IsExprBuilder sym => sym -> SymReal sym -> IO (Pred sym)
realIsNonZero :: forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (Pred sym)
realIsNonZero sym
sym = forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realNe sym
sym (forall sym. IsExprBuilder sym => sym -> SymReal sym
realZero sym
sym)
evalMatlabSolverFn :: forall sym args ret
. IsExprBuilder sym
=> MatlabSolverFn (SymExpr sym) args ret
-> sym
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
evalMatlabSolverFn :: forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsExprBuilder sym =>
MatlabSolverFn (SymExpr sym) args ret
-> sym -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
evalMatlabSolverFn MatlabSolverFn (SymExpr sym) args ret
f sym
sym =
case MatlabSolverFn (SymExpr sym) args ret
f of
MatlabSolverFn (SymExpr sym) args ret
BoolOrFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym
MatlabSolverFn (SymExpr sym) args ret
IsIntegerFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (Pred sym)
isInteger sym
sym
MatlabSolverFn (SymExpr sym) args ret
IntLeFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym
BVToIntegerFn{} -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
bvToInteger sym
sym
SBVToIntegerFn{} -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
sbvToInteger sym
sym
MatlabSolverFn (SymExpr sym) args ret
IntegerToRealFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym
MatlabSolverFn (SymExpr sym) args ret
RealToIntegerFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realToInteger sym
sym
MatlabSolverFn (SymExpr sym) args ret
PredToIntegerFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym BaseBoolType
p ->
forall sym v.
IsExprBuilder sym =>
(sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
intIte sym
sym SymExpr sym BaseBoolType
p (forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
1) (forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
0)
IntSeqFn SymExpr sym BaseIntegerType
b SymExpr sym BaseIntegerType
inc -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym BaseIntegerType
idx SymExpr sym BaseIntegerType
_ -> do
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intAdd sym
sym SymExpr sym BaseIntegerType
b forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMul sym
sym SymExpr sym BaseIntegerType
inc SymExpr sym BaseIntegerType
idx
RealSeqFn SymExpr sym BaseRealType
b SymExpr sym BaseRealType
inc -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym BaseIntegerType
_ SymExpr sym BaseIntegerType
idx -> do
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymExpr sym BaseRealType
b forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymExpr sym BaseRealType
inc forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym SymExpr sym BaseIntegerType
idx
IndicesInRange Assignment OnlyIntRepr (idx '::> itp)
tps0 Assignment (SymExpr sym) (idx '::> itp)
bnds0 -> \Assignment (SymExpr sym) args
args ->
forall {k} (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
Ctx.forIndex (forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment OnlyIntRepr (idx '::> itp)
tps0) (forall (ctx :: Ctx BaseType) (tp :: BaseType).
Assignment OnlyIntRepr ctx
-> Assignment (SymExpr sym) ctx
-> Assignment (SymExpr sym) ctx
-> IO (SymExpr sym BaseBoolType)
-> Index ctx tp
-> IO (SymExpr sym BaseBoolType)
g Assignment OnlyIntRepr (idx '::> itp)
tps0 Assignment (SymExpr sym) (idx '::> itp)
bnds0 Assignment (SymExpr sym) args
args) (forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym))
where g :: Assignment OnlyIntRepr ctx
-> Assignment (SymExpr sym) ctx
-> Assignment (SymExpr sym) ctx
-> IO (Pred sym)
-> Index ctx tp
-> IO (Pred sym)
g :: forall (ctx :: Ctx BaseType) (tp :: BaseType).
Assignment OnlyIntRepr ctx
-> Assignment (SymExpr sym) ctx
-> Assignment (SymExpr sym) ctx
-> IO (SymExpr sym BaseBoolType)
-> Index ctx tp
-> IO (SymExpr sym BaseBoolType)
g Assignment OnlyIntRepr ctx
tps Assignment (SymExpr sym) ctx
bnds Assignment (SymExpr sym) ctx
args IO (SymExpr sym BaseBoolType)
m Index ctx tp
i = do
case Assignment OnlyIntRepr ctx
tps forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i of
OnlyIntRepr tp
OnlyIntRepr -> do
let v :: SymExpr sym tp
v = Assignment (SymExpr sym) ctx
args forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index ctx tp
i
let bnd :: SymExpr sym tp
bnd = Assignment (SymExpr sym) ctx
bnds forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index ctx tp
i
SymExpr sym BaseIntegerType
one <- forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
1
SymExpr sym BaseBoolType
p <- forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymExpr sym BaseIntegerType
one SymExpr sym tp
v forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymExpr sym tp
v SymExpr sym tp
bnd
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym SymExpr sym BaseBoolType
p forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (SymExpr sym BaseBoolType)
m
IsEqFn{} -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym tp
x SymExpr sym tp
y -> do
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
isEq sym
sym SymExpr sym tp
x SymExpr sym tp
y
BVIsNonZeroFn NatRepr w
_ -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym
ClampedIntNegFn NatRepr w
_ -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
clampedIntNeg sym
sym
ClampedIntAbsFn NatRepr w
_ -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
clampedIntAbs sym
sym
ClampedIntAddFn NatRepr w
_ -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedIntAdd sym
sym
ClampedIntSubFn NatRepr w
_ -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedIntSub sym
sym
ClampedIntMulFn NatRepr w
_ -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedIntMul sym
sym
ClampedUIntAddFn NatRepr w
_ -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedUIntAdd sym
sym
ClampedUIntSubFn NatRepr w
_ -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedUIntSub sym
sym
ClampedUIntMulFn NatRepr w
_ -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
clampedUIntMul sym
sym
IntSetWidthFn NatRepr m
_ NatRepr n
o -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym (BaseBVType m)
v -> forall sym (m :: Natural) (n :: Natural).
(IsExprBuilder sym, 1 <= m, 1 <= n) =>
sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
intSetWidth sym
sym SymExpr sym (BaseBVType m)
v NatRepr n
o
UIntSetWidthFn NatRepr m
_ NatRepr n
o -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym (BaseBVType m)
v -> forall sym (m :: Natural) (n :: Natural).
(IsExprBuilder sym, 1 <= m, 1 <= n) =>
sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
uintSetWidth sym
sym SymExpr sym (BaseBVType m)
v NatRepr n
o
UIntToIntFn NatRepr m
_ NatRepr n
o -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym (BaseBVType m)
v -> forall sym (m :: Natural) (n :: Natural).
(IsExprBuilder sym, 1 <= m, 1 <= n) =>
sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
uintToInt sym
sym SymExpr sym (BaseBVType m)
v NatRepr n
o
IntToUIntFn NatRepr m
_ NatRepr n
o -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym (BaseBVType m)
v -> forall sym (m :: Natural) (n :: Natural).
(IsExprBuilder sym, 1 <= m, 1 <= n) =>
sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
intToUInt sym
sym SymExpr sym (BaseBVType m)
v NatRepr n
o
MatlabSolverFn (SymExpr sym) args ret
RealIsNonZeroFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (Pred sym)
realIsNonZero sym
sym
MatlabSolverFn (SymExpr sym) args ret
RealCosFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realCos sym
sym
MatlabSolverFn (SymExpr sym) args ret
RealSinFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realSin sym
sym
RealToSBVFn NatRepr w
w -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym BaseRealType
v -> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
realToSBV sym
sym SymExpr sym BaseRealType
v NatRepr w
w
RealToUBVFn NatRepr w
w -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym BaseRealType
v -> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
realToBV sym
sym SymExpr sym BaseRealType
v NatRepr w
w
PredToBVFn NatRepr w
w -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym BaseBoolType
v -> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
predToBV sym
sym SymExpr sym BaseBoolType
v NatRepr w
w
MatlabSolverFn (SymExpr sym) args ret
CplxIsNonZeroFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ \SymExpr sym BaseComplexType
x -> do
(SymExpr sym BaseRealType
real_x :+ SymExpr sym BaseRealType
imag_x) <- forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxGetParts sym
sym SymExpr sym BaseComplexType
x
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (Pred sym)
realIsNonZero sym
sym SymExpr sym BaseRealType
real_x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (Pred sym)
realIsNonZero sym
sym SymExpr sym BaseRealType
imag_x
MatlabSolverFn (SymExpr sym) args ret
CplxIsRealFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (Pred sym)
isReal sym
sym
MatlabSolverFn (SymExpr sym) args ret
RealToComplexFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymCplx sym)
cplxFromReal sym
sym
MatlabSolverFn (SymExpr sym) args ret
RealPartOfCplxFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymReal sym)
getRealPart sym
sym
MatlabSolverFn (SymExpr sym) args ret
ImagPartOfCplxFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymReal sym)
getImagPart sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxNegFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymCplx sym)
cplxNeg sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxAddFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxAdd sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxSubFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxSub sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxMulFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxMul sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxRoundFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymCplx sym)
cplxRound sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxFloorFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymCplx sym)
cplxFloor sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxCeilFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymCplx sym)
cplxCeil sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxMagFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymReal sym)
cplxMag sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxSqrtFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymCplx sym)
cplxSqrt sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxExpFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymCplx sym)
cplxExp sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxLogFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymCplx sym)
cplxLog sym
sym
CplxLogBaseFn Integer
b -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
Rational -> sym -> SymCplx sym -> IO (SymCplx sym)
cplxLogBase (forall a. Real a => a -> Rational
toRational Integer
b) sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxSinFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymCplx sym)
cplxSin sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxCosFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymCplx sym)
cplxCos sym
sym
MatlabSolverFn (SymExpr sym) args ret
CplxTanFn -> forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
Ctx.uncurryAssignment forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymCplx sym)
cplxTan sym
sym
class IsSymExprBuilder sym => MatlabSymbolicArrayBuilder sym where
mkMatlabSolverFn :: sym
-> MatlabSolverFn (SymExpr sym) args ret
-> IO (SymFn sym args ret)