Grisette.Internal.SymPrim.SymGeneralFun

Documentation

data sa -~> sb where infixr 0

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

(SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => GenSym () (sa -~> sb)

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

Methods

fresh :: MonadFresh m => () -> m (Union (sa -~> sb))

(SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => GenSymSimple () (sa -~> sb)

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

Methods

simpleFresh :: MonadFresh m => () -> m (sa -~> sb)

Lift (sa -~> sb :: Type)

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)

Defined in Grisette.Internal.Core.Control.Monad.Union

Methods

toSym :: Union (ca --> cb) -> sa -~> sb

(SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => IsString (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

fromString :: String -> sa -~> sb

Show (sa -~> sb)

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)

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)

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)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

put :: Putter (sa -~> sb)

get :: Get (sa -~> sb)

NFData (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

rnf :: (sa -~> sb) -> ()

Eq (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

(==) :: (sa -~> sb) -> (sa -~> sb) -> Bool

(/=) :: (sa -~> sb) -> (sa -~> sb) -> Bool

EvalSym (sa -~> sb)

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

Methods

evalSym :: Bool -> Model -> (sa -~> sb) -> sa -~> sb

ExtractSym (sa -~> sb)

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

Methods

extractSym :: (sa -~> sb) -> AnySymbolSet

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => (sa -~> sb) -> Maybe (SymbolSet knd)

Apply st => Apply (sa -~> st)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Associated Types

type FunType (sa -~> st)

Methods

apply :: (sa -~> st) -> FunType (sa -~> st)

ITEOp (sa -~> sb)

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

Methods

symIte :: SymBool -> (sa -~> sb) -> (sa -~> sb) -> sa -~> sb

Mergeable (sa -~> sb)

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

Methods

rootStrategy :: MergingStrategy (sa -~> sb)

PPrint (sa -~> sb)

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

Methods

pformat :: (sa -~> sb) -> Doc ann

pformatPrec :: Int -> (sa -~> sb) -> Doc ann

pformatList :: [sa -~> sb] -> Doc ann

SimpleMergeable (sa -~> sb)

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

Methods

mrgIte :: SymBool -> (sa -~> sb) -> (sa -~> sb) -> sa -~> sb

SubstSym (sa -~> sb)

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

Methods

substSym :: forall cb sb0 (knd :: SymbolKind). (LinkedRep cb sb0, IsSymbolKind knd) => TypedSymbol knd cb -> sb0 -> (sa -~> sb) -> sa -~> sb

AllSyms (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

allSymsS :: (sa -~> sb) -> [SomeSym] -> [SomeSym]

allSyms :: (sa -~> sb) -> [SomeSym]

(ConRep a, ConRep b) => ConRep (a -~> b)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Associated Types

type ConType (a -~> b)

Hashable (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

hashWithSalt :: Int -> (sa -~> sb) -> Int

hash :: (sa -~> sb) -> Int

Function (sa -~> sb) sa sb

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

(#) :: (sa -~> sb) -> sa -> sb

GenSym (sa -~> sb) (sa -~> sb)

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

Methods

fresh :: MonadFresh m => (sa -~> sb) -> m (Union (sa -~> sb))

GenSymSimple (sa -~> sb) (sa -~> sb)

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

Methods

simpleFresh :: MonadFresh m => (sa -~> sb) -> m (sa -~> sb)

(SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb)) => Solvable (ca --> cb) (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

con :: (ca --> cb) -> sa -~> sb

conView :: (sa -~> sb) -> Maybe (ca --> cb)

sym :: Symbol -> sa -~> sb

ssym :: Identifier -> sa -~> sb

isym :: Identifier -> Int -> sa -~> sb

ToCon (a -~> b) (a -~> b)

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

Methods

toCon :: (a -~> b) -> Maybe (a -~> b)

(LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa -~> sb) (ca --> cb)

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

Methods

toCon :: (sa -~> sb) -> Maybe (ca --> cb)

(SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca --> cb) (sa -~> sb)

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

Methods

toSym :: (ca --> cb) -> sa -~> sb

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (sa -~> sb) (sa -~> sb)

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

Methods

toSym :: (sa -~> sb) -> sa -~> sb

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

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

underlyingTerm :: (sa -~> sb) -> Term (ca --> cb)

wrapTerm :: Term (ca --> cb) -> sa -~> sb

type FunType (sa -~> st)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

type FunType (sa -~> st) = sa -> FunType st

type ConType (a -~> b)

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

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)

Associated Types

type SymType (ca --> cb)

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

Methods

underlyingTerm :: (sa -~> sb) -> Term (ca --> cb)

wrapTerm :: Term (ca --> cb) -> sa -~> sb