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

Contents

Orphan instances

Description

Synopsis

data sa =~> sb where
- SymTabularFun :: forall ca sa cb sb. (LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb), SupportedNonFuncPrim ca) => Term (ca =-> cb) -> sa =~> sb

Documentation

data sa =~> sb where infixr 0 Source #

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 :: forall ca sa cb sb. (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.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) Source #

Instance details

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

Methods

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

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

Instance details

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) Source #

Instance details

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) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

put :: Putter (sa =~> sb) #

get :: Get (sa =~> sb) #

NFData (sa =~> sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

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

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

Instance details

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

fromString :: String -> sa =~> sb #

Show (sa =~> sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

showsPrec :: Int -> (sa =~> sb) -> ShowS #

show :: (sa =~> sb) -> String #

showList :: [sa =~> sb] -> ShowS #

Eq (sa =~> sb) Source #

This will crash the program.

SymTabularFun cannot be compared concretely.

If you want to use the type as keys in hash maps based on term equality, say memo table, you should use AsKey SymTabularFun instead.

Instance details

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

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

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

KeyEq (sa =~> sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

keyEq :: (sa =~> sb) -> (sa =~> sb) -> Bool Source #

KeyHashable (sa =~> sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

keyHashWithSalt :: Int -> (sa =~> sb) -> Int Source #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymTabularFun

Associated Types

type FunType (sa =~> st)
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun type FunType (sa =~> st) = sa -> FunType st

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

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

Associated Types

type ConType (a =~> b)
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun type ConType (a =~> b) = ConType a =-> ConType b

Function (sa =~> sb) sa sb Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymTabularFun

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 #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymTabularFun

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), 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 #

(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 #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymTabularFun

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

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

type ConType (a =~> b) Source #

Instance details

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) Source #

Instance details

Associated Types

type SymType (a =-> b)
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun type SymType (a =-> b) = SymType a =~> SymType b

(LinkedRep ca sa, LinkedRep cb sb, 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 #