grisette-0.12.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2024
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellNone
LanguageHaskell2010

Grisette.Internal.SymPrim.SymGeneralFun

Description

 
Synopsis

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 :: 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.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 #

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

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

Eq (sa -~> sb) Source #

This will crash the program.

SymGeneralFun 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 SymGeneralFun instead.

Instance details

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

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

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

KeyEq (sa -~> sb) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

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

KeyHashable (sa -~> sb) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

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

Apply st => Apply (sa -~> st) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Associated Types

type FunType (sa -~> st) 
Instance details

Defined in Grisette.Internal.SymPrim.SymGeneralFun

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

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) 
Instance details

Defined in Grisette.Internal.SymPrim.SymGeneralFun

type ConType (a -~> b) = ConType a --> ConType b
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) 
Instance details

Defined in Grisette.Internal.SymPrim.SymGeneralFun

type SymType (ca --> cb) = SymType ca -~> SymType cb
(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 #