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.Internal.Core.Data.Class.Function

Contents

Function operations

Description

Synopsis

class Function f arg ret | f -> arg ret where
- (#) :: f -> arg -> ret
class Apply uf where
- type FunType uf
- apply :: uf -> FunType uf

Function operations

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

Abstraction for function-like types.

Methods

(#) :: f -> arg -> ret 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 arg ret, Mergeable f, Mergeable ret) => Function (Union f) arg (Union ret) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods (#) :: Union f -> arg -> Union ret Source #
(LinkedRep a sa, LinkedRep b sb) => Function (a --> b) sa sb Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods (#) :: (a --> b) -> sa -> sb Source #
Function (sa -~> sb) sa sb Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods (#) :: (sa -~> sb) -> sa -> sb Source #
Function (sa =~> sb) sa sb Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Methods (#) :: (sa =~> sb) -> sa -> sb Source #
Eq a => Function (a =-> b) a b Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods (#) :: (a =-> b) -> a -> b Source #
Function (a -> b) a b Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Function Methods (#) :: (a -> b) -> 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 AlgReal Source #

Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Associated Types

type FunType AlgReal
Instance details Defined in Grisette.Internal.SymPrim.AlgReal type FunType AlgReal = AlgReal

Methods

apply :: AlgReal -> FunType AlgReal Source #

Apply FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Associated Types

type FunType FPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.FP type FunType FPRoundingMode = FPRoundingMode

Methods

apply :: FPRoundingMode -> FunType FPRoundingMode Source #

Apply SymAlgReal Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Associated Types

type FunType SymAlgReal
Instance details Defined in Grisette.Internal.SymPrim.SymAlgReal type FunType SymAlgReal = SymAlgReal

Methods

apply :: SymAlgReal -> FunType SymAlgReal Source #

Apply SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Associated Types

type FunType SymBool
Instance details Defined in Grisette.Internal.SymPrim.SymBool type FunType SymBool = SymBool

Methods

apply :: SymBool -> FunType SymBool Source #

Apply SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type FunType SymFPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.SymFP type FunType SymFPRoundingMode = SymFPRoundingMode

Methods

apply :: SymFPRoundingMode -> FunType SymFPRoundingMode Source #

Apply SymInteger Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Associated Types

type FunType SymInteger
Instance details Defined in Grisette.Internal.SymPrim.SymInteger type FunType SymInteger = SymInteger

Methods

apply :: SymInteger -> FunType SymInteger Source #

Apply Integer Source #

Instance details

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

Associated Types

type FunType Integer
Instance details Defined in Grisette.Internal.Core.Data.Class.Function type FunType Integer = Integer

Methods

apply :: Integer -> FunType Integer Source #

Apply Bool Source #

Instance details

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

Associated Types

type FunType Bool
Instance details Defined in Grisette.Internal.Core.Data.Class.Function type FunType Bool = Bool

Methods

apply :: Bool -> FunType Bool Source #

Apply (IntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.BV

Associated Types

type FunType (IntN n)
Instance details Defined in Grisette.Internal.SymPrim.BV type FunType (IntN n) = IntN n

Methods

apply :: IntN n -> FunType (IntN n) Source #

Apply (WordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.BV

Associated Types

type FunType (WordN n)
Instance details Defined in Grisette.Internal.SymPrim.BV type FunType (WordN n) = WordN n

Methods

apply :: WordN n -> FunType (WordN n) Source #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type FunType (SymIntN n)
Instance details Defined in Grisette.Internal.SymPrim.SymBV type FunType (SymIntN n) = SymIntN n

Methods

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

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type FunType (SymWordN n)
Instance details Defined in Grisette.Internal.SymPrim.SymBV type FunType (SymWordN n) = SymWordN n

Methods

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

Apply (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Associated Types

type FunType (FP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.FP type FunType (FP eb sb) = FP eb sb

Methods

apply :: FP eb sb -> FunType (FP eb sb) Source #

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

Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

Associated Types

type FunType (ca --> ct)
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun type FunType (ca --> ct) = SymType ca -> FunType (SymType ct)