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

Contents

Orphan instances

Description

Synopsis

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

Documentation

data sa -~> sb where infixr 0 Source #

Symbolic general function type.

>>> :set -XTypeOperators -XOverloadedStrings
>>> f' = "f" :: SymInteger -~> SymInteger
>>> f = (f' #)
>>> f 1
(apply f 1)

>>> f' = con ("a" --> "a" + 1) :: SymInteger -~> SymInteger
>>> f'
\(a:ARG :: Integer) -> (+ 1 a:ARG)
>>> f = (f' #)
>>> f 1
2
>>> f 2
3
>>> f 3
4
>>> f "b"
(+ 1 b)

Constructors

SymGeneralFun :: (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.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), 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.SymGeneralFun 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.SymGeneralFun 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.SymGeneralFun Methods rnf :: (sa -~> sb) -> () #
(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => Eq (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun 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, SupportedNonFuncPrim ca, SupportedPrim ct, SupportedPrim (ca --> ct)) => Apply (sa -~> st) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun 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.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) Source #
(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => Hashable (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods hashWithSalt :: Int -> (sa -~> sb) -> Int # hash :: (sa -~> sb) -> Int #
(SupportedNonFuncPrim 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.SymGeneralFun 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.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 #
(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 (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 #
(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 #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim ca, SupportedPrim cb, SupportedPrim (ca --> cb)) => 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

(-->) :: (SupportedPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedSymbol ca -> sb -> ca --> cb infixr 0 Source #

Construction of general symbolic functions.

>>> f = "a" --> "a" + 1 :: Integer --> Integer
>>> f
\(a:ARG :: Integer) -> (+ 1 a:ARG)

This general symbolic function needs to be applied to symbolic values: >>> f # ("a" :: SymInteger) (+ 1 a)

Orphan instances

(SymRep ca, SymRep cb, SupportedPrim (ca --> cb)) => SymRep (ca --> cb) Source #
Instance details Associated Types type SymType (ca --> cb) Source #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim ca, SupportedPrim cb, 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 #