Grisette.Internal.Core.Data.Class.Function

Function operations

class Function f arg ret | f -> arg ret where

Abstraction for function-like types.

Methods

(#) :: f -> arg -> ret infixl 9

Function application operator.

The operator is not right associated (like ($)). It is left associated, and you can provide many arguments with this operator once at a time.

>>> (+1) # 2
3

>>> (+) # 2 # 3
5

Instances

(Function f arg ret, Mergeable f, Mergeable ret) => Function (UnionM f) arg (UnionM ret)

Defined in Grisette.Internal.Core.Control.Monad.UnionM

Methods

(#) :: UnionM f -> arg -> UnionM ret

(LinkedRep a sa, LinkedRep b sb) => Function (a --> b) sa sb

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

(#) :: (a --> b) -> sa -> sb

(SupportedNonFuncPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb)) => Function (sa -~> sb) sa sb

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

(#) :: (sa -~> sb) -> sa -> sb

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => Function (sa =~> sb) sa sb

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

(#) :: (sa =~> sb) -> sa -> sb

Eq a => Function (a =-> b) a b

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

(#) :: (a =-> b) -> a -> b

Function (a -> b) a b

Defined in Grisette.Internal.Core.Data.Class.Function

Methods

(#) :: (a -> b) -> a -> b

class Apply uf where

Applying an uninterpreted function.

>>> let f = "f" :: SymInteger =~> SymInteger =~> SymInteger
>>> apply f "a" "b"
(apply (apply f a) b)

Note that for implementation reasons, you can also use apply function on a non-function symbolic value. In this case, the function is treated as an id function.

Associated Types

type FunType uf

Methods

apply :: uf -> FunType uf

Instances

Apply SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Associated Types

type FunType SymBool

Methods

apply :: SymBool -> FunType SymBool

Apply SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Associated Types

type FunType SymInteger

Methods

apply :: SymInteger -> FunType SymInteger

(KnownNat n, 1 <= n) => Apply (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type FunType (SymIntN n)

Methods

apply :: SymIntN n -> FunType (SymIntN n)

(KnownNat n, 1 <= n) => Apply (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type FunType (SymWordN n)

Methods

apply :: SymWordN n -> FunType (SymWordN n)

(LinkedRep ca sa, LinkedRep ct st, Apply st, SupportedNonFuncPrim ca, SupportedPrim ct, SupportedPrim (ca --> ct)) => Apply (sa -~> st)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Associated Types

type FunType (sa -~> st)

Methods

apply :: (sa -~> st) -> FunType (sa -~> st)

(LinkedRep ca sa, LinkedRep ct st, Apply st, SupportedPrim ca, SupportedPrim ct, SupportedPrim (ca =-> ct)) => Apply (sa =~> st)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Associated Types

type FunType (sa =~> st)

Methods

apply :: (sa =~> st) -> FunType (sa =~> st)

Apply b => Apply (a -> b)

Defined in Grisette.Internal.Core.Data.Class.Function

Associated Types

type FunType (a -> b)

Methods

apply :: (a -> b) -> FunType (a -> b)