Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Trustworthy
Language	Haskell2010

Grisette.Core.Data.Class.Function

Contents

Function operations

Description

Synopsis

class Function f where
- type Arg f
- type Ret f
- (#) :: f -> Arg f -> Ret f
class Apply uf where
- type FunType uf
- apply :: uf -> FunType uf

Function operations

class Function f where Source #

Abstraction for function-like types.

Associated Types

type Arg f Source #

Argument type

type Ret f Source #

Return type

Methods

(#) :: f -> Arg f -> Ret f infixl 9 Source #

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

Instances details

(Function f, Mergeable f, Mergeable a, Ret f ~ a) => Function (UnionM f) Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM Associated Types type Arg (UnionM f) Source # type Ret (UnionM f) Source # Methods (#) :: UnionM f -> Arg (UnionM f) -> Ret (UnionM f) Source #
(LinkedRep a sa, LinkedRep b sb) => Function (a --> b) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term Associated Types type Arg (a --> b) Source # type Ret (a --> b) Source # Methods (#) :: (a --> b) -> Arg (a --> b) -> Ret (a --> b) Source #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Function (sa -~> sb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type Arg (sa -~> sb) Source # type Ret (sa -~> sb) Source # Methods (#) :: (sa -~> sb) -> Arg (sa -~> sb) -> Ret (sa -~> sb) Source #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Function (sa =~> sb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type Arg (sa =~> sb) Source # type Ret (sa =~> sb) Source # Methods (#) :: (sa =~> sb) -> Arg (sa =~> sb) -> Ret (sa =~> sb) Source #
Eq a => Function (a =-> b) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.TabularFun Associated Types type Arg (a =-> b) Source # type Ret (a =-> b) Source # Methods (#) :: (a =-> b) -> Arg (a =-> b) -> Ret (a =-> b) Source #
Function (a -> b) Source #
Instance details Defined in Grisette.Core.Data.Class.Function Associated Types type Arg (a -> b) Source # type Ret (a -> b) Source # Methods (#) :: (a -> b) -> Arg (a -> b) -> Ret (a -> b) Source #

class Apply uf where Source #

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 Source #

Methods

apply :: uf -> FunType uf Source #

Instances

Instances details

Apply SymBool Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type FunType SymBool Source # Methods apply :: SymBool -> FunType SymBool Source #
Apply SymInteger Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type FunType SymInteger Source # Methods apply :: SymInteger -> FunType SymInteger Source #
(KnownNat n, 1 <= n) => Apply (SymIntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type FunType (SymIntN n) Source # Methods apply :: SymIntN n -> FunType (SymIntN n) Source #
(KnownNat n, 1 <= n) => Apply (SymWordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type FunType (SymWordN n) Source # Methods apply :: SymWordN n -> FunType (SymWordN n) Source #
(LinkedRep ca sa, LinkedRep ct st, Apply st) => Apply (sa -~> st) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type FunType (sa -~> st) Source # Methods apply :: (sa -~> st) -> FunType (sa -~> st) Source #
(LinkedRep ca sa, LinkedRep ct st, Apply st) => Apply (sa =~> st) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type FunType (sa =~> st) Source # Methods apply :: (sa =~> st) -> FunType (sa =~> st) Source #
Apply b => Apply (a -> b) Source #
Instance details Defined in Grisette.Core.Data.Class.Function Associated Types type FunType (a -> b) Source # Methods apply :: (a -> b) -> FunType (a -> b) Source #