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

Grisette.Unified.Internal.UnifiedFun

Description

Synopsis

type UnifiedFunConstraint mode a b ca cb sa sb = (Eq (GetFun mode a b), EvalSym (GetFun mode a b), ExtractSym (GetFun mode a b), PPrint (GetFun mode a b), Hashable (GetFun mode a b), Lift (GetFun mode a b), Mergeable (GetFun mode a b), NFData (GetFun mode a b), Show (GetFun mode a b), SubstSym (GetFun mode a b), ToCon (GetFun mode a b) (ca =-> cb), ToCon (sa =~> sb) (GetFun mode a b), ToSym (GetFun mode a b) (sa =~> sb), ToSym (ca =-> cb) (GetFun mode a b), Function (GetFun mode a b) a b, Apply (GetFun mode a b), FunType (GetFun mode a b) ~ (a -> b))
class UnifiedFun (mode :: EvalModeTag) where
- type GetFun mode = (fun :: Type -> Type -> Type) | fun -> mode
unifiedFunInstanceName :: String -> [TheoryToUnify] -> String
genUnifiedFunInstance :: String -> [TheoryToUnify] -> DecsQ
type GetFun2 mode a b = GetFun mode a b
type GetFun3 mode a b c = GetFun mode a (GetFun mode b c)
type GetFun4 mode a b c d = GetFun mode a (GetFun mode b (GetFun mode c d))
type GetFun5 mode a b c d e = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d e)))
type GetFun6 mode a b c d e f = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d (GetFun mode e f))))
type GetFun7 mode a b c d e f g = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d (GetFun mode e (GetFun mode f g)))))
type GetFun8 mode a b c d e f g h = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d (GetFun mode e (GetFun mode f (GetFun mode g h))))))

Documentation

type UnifiedFunConstraint mode a b ca cb sa sb = (Eq (GetFun mode a b), EvalSym (GetFun mode a b), ExtractSym (GetFun mode a b), PPrint (GetFun mode a b), Hashable (GetFun mode a b), Lift (GetFun mode a b), Mergeable (GetFun mode a b), NFData (GetFun mode a b), Show (GetFun mode a b), SubstSym (GetFun mode a b), ToCon (GetFun mode a b) (ca =-> cb), ToCon (sa =~> sb) (GetFun mode a b), ToSym (GetFun mode a b) (sa =~> sb), ToSym (ca =-> cb) (GetFun mode a b), Function (GetFun mode a b) a b, Apply (GetFun mode a b), FunType (GetFun mode a b) ~ (a -> b)) Source #

The constraint for a unified function.

Provide unified function types.

Associated Types

type GetFun mode = (fun :: Type -> Type -> Type) | fun -> mode Source #

Get a unified function type. Resolves to =-> in Con mode, and =~> in Sym mode.

Instances details

UnifiedFun 'Con Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedFun Associated Types type GetFun 'Con = (fun :: Type -> Type -> Type) Source #
UnifiedFun 'Sym Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedFun Associated Types type GetFun 'Sym = (fun :: Type -> Type -> Type) Source #

Generate unified function instance names.

Generate unified function instances.

type GetFun2 mode a b = GetFun mode a b Source #

The unified function type with 2 arguments.

type GetFun3 mode a b c = GetFun mode a (GetFun mode b c) Source #

The unified function type with 3 arguments.

type GetFun4 mode a b c d = GetFun mode a (GetFun mode b (GetFun mode c d)) Source #

The unified function type with 4 arguments.

type GetFun5 mode a b c d e = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d e))) Source #

The unified function type with 5 arguments.

type GetFun6 mode a b c d e f = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d (GetFun mode e f)))) Source #

The unified function type with 6 arguments.

type GetFun7 mode a b c d e f g = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d (GetFun mode e (GetFun mode f g))))) Source #

The unified function type with 7 arguments.

type GetFun8 mode a b c d e f g h = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d (GetFun mode e (GetFun mode f (GetFun mode g h)))))) Source #

The unified function type with 8 arguments.