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

Contents

Orphan instances

Description

Synopsis

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

Documentation

data sa =~> sb where infixr 0 Source #

Symbolic tabular function type.

>>> :set -XTypeOperators -XOverloadedStrings
>>> 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) => Term (ca =-> cb) -> sa =~> sb

Instances

Instances details

(SupportedPrim (ca =-> cb), 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 (UnionM (sa =~> sb)) Source #
(SupportedPrim (ca =-> cb), 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), LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (ca =-> cb)) (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods toSym :: UnionM (ca =-> cb) -> sa =~> sb Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => IsString (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Methods fromString :: String -> sa =~> sb #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb 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 #
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) => Eq (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Methods (==) :: (sa =~> sb) -> (sa =~> sb) -> Bool # (/=) :: (sa =~> sb) -> (sa =~> sb) -> Bool #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => EvaluateSym (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.EvaluateSym Methods evaluateSym :: Bool -> Model -> (sa =~> sb) -> sa =~> sb Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ExtractSymbolics (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: (sa =~> sb) -> SymbolSet Source #
(LinkedRep ca sa, LinkedRep ct st, Apply st, SupportedPrim ca, SupportedPrim ct, SupportedPrim (ca =-> ct)) => Apply (sa =~> st) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Associated Types type FunType (sa =~> st) Source # Methods apply :: (sa =~> st) -> FunType (sa =~> st) Source #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => GPretty (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GPretty Methods gpretty :: (sa =~> sb) -> Doc ann Source # gprettyPrec :: Int -> (sa =~> sb) -> Doc ann Source # gprettyList :: [sa =~> sb] -> Doc ann Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> (sa =~> sb) -> (sa =~> sb) -> sa =~> sb Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => Mergeable (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (sa =~> sb) Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => SimpleMergeable (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> (sa =~> sb) -> (sa =~> sb) -> sa =~> sb Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => SubstituteSym (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb0 => TypedSymbol cb -> sb0 -> (sa =~> sb) -> sa =~> sb Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => 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) Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => Hashable (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Methods hashWithSalt :: Int -> (sa =~> sb) -> Int # hash :: (sa =~> sb) -> Int #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => Function (sa =~> sb) sa sb Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Methods (#) :: (sa =~> sb) -> sa -> sb Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => GenSym (sa =~> sb) (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => (sa =~> sb) -> m (UnionM (sa =~> sb)) Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => 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 #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => 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 #
(SupportedPrim a, SupportedPrim b) => ToCon (a =~> b) (a =~> b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: (a =~> b) -> Maybe (a =~> b) Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa =~> sb) (ca =-> cb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: (sa =~> sb) -> Maybe (ca =-> cb) Source #
(SupportedPrim a, SupportedPrim b) => ToSym (a =~> b) (a =~> b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: (a =~> b) -> a =~> b Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca =-> cb) (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: (ca =-> cb) -> sa =~> sb Source #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => 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) Source #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => LinkedRep (ca =-> cb) (sa =~> sb) Source #
Instance details Methods underlyingTerm :: (sa =~> sb) -> Term (ca =-> cb) Source # wrapTerm :: Term (ca =-> cb) -> sa =~> sb Source #