Grisette.Internal.SymPrim.SymTabularFun

Documentation

data sa =~> sb where infixr 0

Symbolic tabular function type.

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

>>> f' = con (TabularFun [(1, 2), (2, 3)] 4) :: SymInteger =~> SymInteger
>>> f = (f' #)
>>> f 1
2
>>> f 2
3
>>> f 3
4
>>> f "b"
(ite (= b 1) 2 (ite (= b 2) 3 4))

Constructors

SymTabularFun :: (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.SymTabularFun

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.Internal.Impl.Core.Control.Monad.Union

Methods

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

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

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

fromString :: String -> sa =~> sb

Show (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

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.SymTabularFun

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.SymTabularFun

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.SymTabularFun

Methods

put :: Putter (sa =~> sb)

get :: Get (sa =~> sb)

NFData (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

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

Eq (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.SymTabularFun

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

EvalSym (sa =~> sb)

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

Methods

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

ExtractSym (sa =~> sb)

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

Methods

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

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

Mergeable (sa =~> sb)

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

Methods

rootStrategy :: MergingStrategy (sa =~> sb)

PPrint (sa =~> sb)

Defined in Grisette.Internal.Internal.Impl.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.Internal.Impl.Core.Data.Class.SimpleMergeable

Methods

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

SubstSym (sa =~> sb)

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

AllSyms (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.SymTabularFun

Associated Types

type ConType (a =~> b)

Hashable (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

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

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

Function (sa =~> sb) sa sb

Defined in Grisette.Internal.SymPrim.SymTabularFun

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)

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

Defined in Grisette.Internal.SymPrim.SymTabularFun

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

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

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

type FunType (sa =~> st)

Defined in Grisette.Internal.SymPrim.SymTabularFun

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

type ConType (a =~> b)

Defined in Grisette.Internal.SymPrim.SymTabularFun

type ConType (a =~> b) = ConType a =-> ConType b

Orphan instances

(SymRep a, SymRep b, SupportedPrim (a =-> b)) => SymRep (a =-> b)

Associated Types

type SymType (a =-> b)

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

Methods

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

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