| 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 | None |
| Language | Haskell2010 |
Grisette.Internal.Unified.UnifiedFun
Description
Synopsis
- type UnifiedFunConstraint (mode :: EvalModeTag) a b ca cb sa sb = (Show (GetFun mode a b), Binary (GetFun mode a b), Serial (GetFun mode a b), Serialize (GetFun mode a b), NFData (GetFun mode a b), Eq (GetFun mode a b), EvalSym (GetFun mode a b), ExtractSym (GetFun mode a b), Mergeable (GetFun mode a b), PPrint (GetFun mode a b), SubstSym (GetFun mode a b), Hashable (GetFun mode a b), Lift (GetFun mode a b), Typeable (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 :: EvalModeTag) = (fun :: Type -> Type -> Type) | fun -> mode
- unifiedFunInstanceName :: String -> [TheoryToUnify] -> String
- genUnifiedFunInstance :: String -> [TheoryToUnify] -> DecsQ
- type GetFun2 (mode :: EvalModeTag) a b = GetFun mode a b
- type GetFun3 (mode :: EvalModeTag) a b c = GetFun mode a (GetFun mode b c)
- type GetFun4 (mode :: EvalModeTag) a b c d = GetFun mode a (GetFun mode b (GetFun mode c d))
- type GetFun5 (mode :: EvalModeTag) a b c d e = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d e)))
- type GetFun6 (mode :: EvalModeTag) 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 :: EvalModeTag) 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 :: EvalModeTag) 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 :: EvalModeTag) a b ca cb sa sb = (Show (GetFun mode a b), Binary (GetFun mode a b), Serial (GetFun mode a b), Serialize (GetFun mode a b), NFData (GetFun mode a b), Eq (GetFun mode a b), EvalSym (GetFun mode a b), ExtractSym (GetFun mode a b), Mergeable (GetFun mode a b), PPrint (GetFun mode a b), SubstSym (GetFun mode a b), Hashable (GetFun mode a b), Lift (GetFun mode a b), Typeable (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.
class UnifiedFun (mode :: EvalModeTag) Source #
Provide unified function types.
Associated Types
type GetFun (mode :: EvalModeTag) = (fun :: Type -> Type -> Type) | fun -> mode Source #
Instances
| UnifiedFun 'C Source # | |
Defined in Grisette.Internal.Unified.UnifiedFun | |
| UnifiedFun 'S Source # | |
Defined in Grisette.Internal.Unified.UnifiedFun | |
unifiedFunInstanceName :: String -> [TheoryToUnify] -> String Source #
Generate unified function instance names.
genUnifiedFunInstance :: String -> [TheoryToUnify] -> DecsQ Source #
Generate unified function instances.
type GetFun2 (mode :: EvalModeTag) a b = GetFun mode a b Source #
The unified function type with 2 arguments.
type GetFun3 (mode :: EvalModeTag) a b c = GetFun mode a (GetFun mode b c) Source #
The unified function type with 3 arguments.
type GetFun4 (mode :: EvalModeTag) 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 :: EvalModeTag) 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 :: EvalModeTag) 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.