Grisette.Core.Data.Class.Function

Function operations

class Function f where

Abstraction for function-like types.

Associated Types

type Arg f

Argument type

type Ret f

Return type

Methods

(#) :: f -> Arg f -> Ret f 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, Mergeable f, Mergeable a, Ret f ~ a) => Function (UnionM f)

Defined in Grisette.Core.Control.Monad.UnionM

Associated Types

type Arg (UnionM f)

type Ret (UnionM f)

Methods

(#) :: UnionM f -> Arg (UnionM f) -> Ret (UnionM f)

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

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type Arg (a --> b)

type Ret (a --> b)

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type Arg (sa -~> sb)

type Ret (sa -~> sb)

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type Arg (sa =~> sb)

type Ret (sa =~> sb)

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.TabularFun

Associated Types

type Arg (a =-> b)

type Ret (a =-> b)

Methods

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

Function (a -> b)

Defined in Grisette.Core.Data.Class.Function

Associated Types

type Arg (a -> b)

type Ret (a -> b)

Methods

(#) :: (a -> b) -> Arg (a -> b) -> Ret (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.IR.SymPrim.Data.SymPrim

Associated Types

type FunType SymBool

Methods

apply :: SymBool -> FunType SymBool

Apply SymInteger

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type FunType SymInteger

Methods

apply :: SymInteger -> FunType SymInteger

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type FunType (SymIntN n)

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type FunType (SymWordN n)

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type FunType (sa -~> st)

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type FunType (sa =~> st)

Methods

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

Apply b => Apply (a -> b)

Defined in Grisette.Core.Data.Class.Function

Associated Types

type FunType (a -> b)

Methods

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