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.Internal.SymPrim.SymGeneralFun

Contents

Orphan instances

Description

Synopsis

data sa -~> sb where
- SymGeneralFun :: (LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb), SupportedNonFuncPrim ca) => Term (ca --> cb) -> sa -~> sb
(-->) :: (SupportedNonFuncPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedConstantSymbol ca -> sb -> ca --> cb

Documentation

data sa -~> sb where infixr 0 Source #

Symbolic general function type.

>>> f' = "f" :: SymInteger -~> SymInteger
>>> f = (f' #)
>>> f 1
(apply f 1)

>>> f' = con ("a" --> "a" + 1) :: SymInteger -~> SymInteger
>>> f'
\(arg@0 :: Integer) -> (+ 1 arg@0)
>>> f = (f' #)
>>> f 1
2
>>> f 2
3
>>> f 3
4
>>> f "b"
(+ 1 b)

Constructors

SymGeneralFun :: (LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb), SupportedNonFuncPrim ca) => Term (ca --> cb) -> sa -~> sb

Instances

Instances details

(SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => GenSym () (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => () -> m (Union (sa -~> sb)) Source #
(SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => GenSymSimple () (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => () -> m (sa -~> sb) Source #
Lift (sa -~> sb :: Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods lift :: Quote m => (sa -~> sb) -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => (sa -~> sb) -> Code m (sa -~> sb) #
(SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => ToSym (Union (ca --> cb)) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods toSym :: Union (ca --> cb) -> sa -~> sb Source #
(SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => IsString (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods fromString :: String -> sa -~> sb #
Show (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods showsPrec :: Int -> (sa -~> sb) -> ShowS # show :: (sa -~> sb) -> String # showList :: [sa -~> sb] -> ShowS #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb), SupportedNonFuncPrim ca) => Binary (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods put :: (sa -~> sb) -> Put # get :: Get (sa -~> sb) # putList :: [sa -~> sb] -> Put #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb), SupportedNonFuncPrim ca) => Serial (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods serialize :: MonadPut m => (sa -~> sb) -> m () # deserialize :: MonadGet m => m (sa -~> sb) #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb), SupportedNonFuncPrim ca) => Serialize (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods put :: Putter (sa -~> sb) # get :: Get (sa -~> sb) #
NFData (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods rnf :: (sa -~> sb) -> () #
Eq (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods (==) :: (sa -~> sb) -> (sa -~> sb) -> Bool # (/=) :: (sa -~> sb) -> (sa -~> sb) -> Bool #
Apply st => Apply (sa -~> st) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Associated Types type FunType (sa -~> st) Source # Methods apply :: (sa -~> st) -> FunType (sa -~> st) Source #
ITEOp (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> (sa -~> sb) -> (sa -~> sb) -> sa -~> sb Source #
EvalSym (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (sa -~> sb) -> sa -~> sb Source #
ExtractSym (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym Methods extractSym :: (sa -~> sb) -> AnySymbolSet Source # extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => (sa -~> sb) -> Maybe (SymbolSet knd) Source #
Mergeable (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (sa -~> sb) Source # sortIndices :: (sa -~> sb) -> [DynamicSortedIdx] Source #
PPrint (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint Methods pformat :: (sa -~> sb) -> Doc ann Source # pformatPrec :: Int -> (sa -~> sb) -> Doc ann Source # pformatList :: [sa -~> sb] -> Doc ann Source #
SimpleMergeable (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (sa -~> sb) -> (sa -~> sb) -> sa -~> sb Source #
SubstSym (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb0 (knd :: SymbolKind). (LinkedRep cb sb0, IsSymbolKind knd) => TypedSymbol knd cb -> sb0 -> (sa -~> sb) -> sa -~> sb Source #
AllSyms (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods allSymsS :: (sa -~> sb) -> [SomeSym] -> [SomeSym] Source # allSyms :: (sa -~> sb) -> [SomeSym] Source #
(ConRep a, ConRep b) => ConRep (a -~> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Associated Types type ConType (a -~> b) Source #
Hashable (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods hashWithSalt :: Int -> (sa -~> sb) -> Int # hash :: (sa -~> sb) -> Int #
Function (sa -~> sb) sa sb Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods (#) :: (sa -~> sb) -> sa -> sb Source #
GenSym (sa -~> sb) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => (sa -~> sb) -> m (Union (sa -~> sb)) Source #
GenSymSimple (sa -~> sb) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => (sa -~> sb) -> m (sa -~> sb) Source #
(SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb)) => Solvable (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods con :: (ca --> cb) -> sa -~> sb Source # conView :: (sa -~> sb) -> Maybe (ca --> cb) Source # sym :: Symbol -> sa -~> sb Source # ssym :: Identifier -> sa -~> sb Source # isym :: Identifier -> Int -> sa -~> sb Source #
ToCon (a -~> b) (a -~> b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: (a -~> b) -> Maybe (a -~> b) Source #
(LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa -~> sb) (ca --> cb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: (sa -~> sb) -> Maybe (ca --> cb) Source #
(SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (ca --> cb) -> sa -~> sb Source #
(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (sa -~> sb) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (sa -~> sb) -> sa -~> sb Source #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim cb, SupportedPrim (ca --> cb), SupportedNonFuncPrim ca) => LinkedRep (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods underlyingTerm :: (sa -~> sb) -> Term (ca --> cb) Source # wrapTerm :: Term (ca --> cb) -> sa -~> sb Source #
type FunType (sa -~> st) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun type FunType (sa -~> st) = sa -> FunType st
type ConType (a -~> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun type ConType (a -~> b) = ConType a --> ConType b

(-->) :: (SupportedNonFuncPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedConstantSymbol ca -> sb -> ca --> cb infixr 0 Source #

Construction of general symbolic functions.

>>> f = "a" --> "a" + 1 :: Integer --> Integer
>>> f
\(arg@0 :: Integer) -> (+ 1 arg@0)

This general symbolic function needs to be applied to symbolic values:

>>> f # ("a" :: SymInteger)
(+ 1 a)
>>> f # (2 :: SymInteger)
3

Orphan instances

(SymRep ca, SymRep cb, SupportedPrim (ca --> cb)) => SymRep (ca --> cb) Source #
Instance details Associated Types type SymType (ca --> cb) Source #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim cb, SupportedPrim (ca --> cb), SupportedNonFuncPrim ca) => LinkedRep (ca --> cb) (sa -~> sb) Source #
Instance details Methods underlyingTerm :: (sa -~> sb) -> Term (ca --> cb) Source # wrapTerm :: Term (ca --> cb) -> sa -~> sb Source #