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

Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Description

 
Synopsis

Documentation

class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where Source #

Indicates that a type is supported and can be represented as a symbolic term.

Minimal complete definition

defaultValue

Associated Types

type PrimConstraint t :: Constraint Source #

type PrimConstraint t = ()

Methods

withPrim :: proxy t -> (PrimConstraint t => a) -> a Source #

default withPrim :: PrimConstraint t => proxy t -> (PrimConstraint t => a) -> a Source #

termCache :: Cache (Term t) Source #

pformatCon :: t -> String Source #

default pformatCon :: Show t => t -> String Source #

pformatSym :: TypedSymbol t -> String Source #

defaultValue :: t Source #

defaultValueDynamic :: proxy t -> ModelValue Source #

Instances

Instances details
SupportedPrim Integer Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint Integer Source #

SupportedPrim Bool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint Bool Source #

(KnownNat w, 1 <= w) => SupportedPrim (IntN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (IntN w) Source #

(KnownNat w, 1 <= w) => SupportedPrim (WordN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (WordN w) Source #

(SupportedPrim a, SupportedPrim b) => SupportedPrim (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (a --> b) Source #

Methods

withPrim :: proxy (a --> b) -> (PrimConstraint (a --> b) => a0) -> a0 Source #

termCache :: Cache (Term (a --> b)) Source #

pformatCon :: (a --> b) -> String Source #

pformatSym :: TypedSymbol (a --> b) -> String Source #

defaultValue :: a --> b Source #

defaultValueDynamic :: proxy (a --> b) -> ModelValue Source #

(SupportedPrim a, SupportedPrim b) => SupportedPrim (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

Associated Types

type PrimConstraint (a =-> b) Source #

Methods

withPrim :: proxy (a =-> b) -> (PrimConstraint (a =-> b) => a0) -> a0 Source #

termCache :: Cache (Term (a =-> b)) Source #

pformatCon :: (a =-> b) -> String Source #

pformatSym :: TypedSymbol (a =-> b) -> String Source #

defaultValue :: a =-> b Source #

defaultValueDynamic :: proxy (a =-> b) -> ModelValue Source #

class SupportedPrim con => SymRep con Source #

Type family to resolve the symbolic type associated with a concrete type.

Associated Types

type SymType con Source #

Instances

Instances details
SymRep Integer Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType Integer Source #

SymRep Bool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType Bool Source #

(KnownNat n, 1 <= n) => SymRep (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType (IntN n) Source #

(KnownNat n, 1 <= n) => SymRep (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType (WordN n) Source #

(SymRep ca, SymRep cb) => SymRep (ca --> cb) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType (ca --> cb) Source #

(SymRep a, SymRep b) => SymRep (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType (a =-> b) Source #

class ConRep sym Source #

Type family to resolve the concrete type associated with a symbolic type.

Associated Types

type ConType sym Source #

Instances

Instances details
ConRep SymBool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type ConType SymBool Source #

ConRep SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type ConType SymInteger Source #

(KnownNat n, 1 <= n) => ConRep (SymIntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type ConType (SymIntN n) Source #

(KnownNat n, 1 <= n) => ConRep (SymWordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type ConType (SymWordN n) Source #

(ConRep a, ConRep b) => ConRep (a -~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type ConType (a -~> b) Source #

(ConRep a, ConRep b) => ConRep (a =~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type ConType (a =~> b) Source #

class (ConRep sym, SymRep con, sym ~ SymType con, con ~ ConType sym) => LinkedRep con sym | con -> sym, sym -> con where Source #

One-to-one mapping between symbolic types and concrete types.

Methods

underlyingTerm :: sym -> Term con Source #

wrapTerm :: Term con -> sym Source #

Instances

Instances details
LinkedRep Integer SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

LinkedRep Bool SymBool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

(KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

(LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca --> cb) (sa -~> sb) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

(LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca =-> cb) (sa =~> sb) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

class (SupportedPrim arg, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => UnaryOp tag arg t | tag arg -> t where Source #

Methods

partialEvalUnary :: (Typeable tag, Typeable t) => tag -> Term arg -> Term t Source #

pformatUnary :: tag -> Term arg -> String Source #

class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => BinaryOp tag arg1 arg2 t | tag arg1 arg2 -> t where Source #

Methods

partialEvalBinary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term t Source #

pformatBinary :: tag -> Term arg1 -> Term arg2 -> String Source #

class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim arg3, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => TernaryOp tag arg1 arg2 arg3 t | tag arg1 arg2 arg3 -> t where Source #

Methods

partialEvalTernary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t Source #

pformatTernary :: tag -> Term arg1 -> Term arg2 -> Term arg3 -> String Source #

data TypedSymbol t where Source #

A typed symbol is a symbol that is associated with a type. Note that the same symbol bodies with different types are considered different symbols and can coexist in a term.

Simple symbols can be created with the OverloadedStrings extension:

>>> :set -XOverloadedStrings
>>> "a" :: TypedSymbol Bool
a :: Bool

Constructors

SimpleSymbol :: SupportedPrim t => String -> TypedSymbol t 
IndexedSymbol :: SupportedPrim t => String -> Int -> TypedSymbol t 
WithInfo :: forall t a. (SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => TypedSymbol t -> a -> TypedSymbol t 

Instances

Instances details
SymbolSetOps SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelOps Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Lift (TypedSymbol t :: Type) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

lift :: Quote m => TypedSymbol t -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => TypedSymbol t -> Code m (TypedSymbol t) #

SupportedPrim t => IsString (TypedSymbol t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Show (TypedSymbol t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

NFData (TypedSymbol t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

rnf :: TypedSymbol t -> () #

Eq (TypedSymbol t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Ord (TypedSymbol t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Hashable (TypedSymbol t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

hashWithSalt :: Int -> TypedSymbol t -> Int #

hash :: TypedSymbol t -> Int #

SymbolSetRep (TypedSymbol t) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

data Term t where Source #

Constructors

ConTerm :: SupportedPrim t => !Id -> !t -> Term t 
SymTerm :: SupportedPrim t => !Id -> !(TypedSymbol t) -> Term t 
UnaryTerm :: UnaryOp tag arg t => !Id -> !tag -> !(Term arg) -> Term t 
BinaryTerm :: BinaryOp tag arg1 arg2 t => !Id -> !tag -> !(Term arg1) -> !(Term arg2) -> Term t 
TernaryTerm :: TernaryOp tag arg1 arg2 arg3 t => !Id -> !tag -> !(Term arg1) -> !(Term arg2) -> !(Term arg3) -> Term t 
NotTerm :: !Id -> !(Term Bool) -> Term Bool 
OrTerm :: !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool 
AndTerm :: !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool 
EqvTerm :: SupportedPrim t => !Id -> !(Term t) -> !(Term t) -> Term Bool 
ITETerm :: SupportedPrim t => !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t 
AddNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> !(Term t) -> Term t 
UMinusNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> Term t 
TimesNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> !(Term t) -> Term t 
AbsNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> Term t 
SignumNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> Term t 
LTNumTerm :: (SupportedPrim t, Num t, Ord t) => !Id -> !(Term t) -> !(Term t) -> Term Bool 
LENumTerm :: (SupportedPrim t, Num t, Ord t) => !Id -> !(Term t) -> !(Term t) -> Term Bool 
AndBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !(Term t) -> Term t 
OrBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !(Term t) -> Term t 
XorBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !(Term t) -> Term t 
ComplementBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> Term t 
ShiftBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !Int -> Term t 
RotateBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !Int -> Term t 
BVConcatTerm :: (SupportedPrim (bv a), SupportedPrim (bv b), SupportedPrim (bv (a + b)), KnownNat a, KnownNat b, 1 <= a, 1 <= b, SizedBV bv) => !Id -> !(Term (bv a)) -> !(Term (bv b)) -> Term (bv (a + b)) 
BVSelectTerm :: (SupportedPrim (bv n), SupportedPrim (bv w), KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n, SizedBV bv) => !Id -> !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv n)) -> Term (bv w) 
BVExtendTerm :: (SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l, KnownNat r, 1 <= l, l <= r, SizedBV bv) => !Id -> !Bool -> !(TypeRep r) -> !(Term (bv l)) -> Term (bv r) 
TabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => !Id -> Term (a =-> b) -> Term a -> Term b 
GeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => !Id -> Term (a --> b) -> Term a -> Term b 
DivIntegralTerm :: (SupportedPrim t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
ModIntegralTerm :: (SupportedPrim t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
QuotIntegralTerm :: (SupportedPrim t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
RemIntegralTerm :: (SupportedPrim t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
DivBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
ModBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
QuotBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
RemBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 

Instances

Instances details
Lift (Term t :: Type) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

lift :: Quote m => Term t -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => Term t -> Code m (Term t) #

Show (Term ty) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

showsPrec :: Int -> Term ty -> ShowS #

show :: Term ty -> String #

showList :: [Term ty] -> ShowS #

NFData (Term a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

rnf :: Term a -> () #

SupportedPrim t => Eq (Term t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

(==) :: Term t -> Term t -> Bool #

(/=) :: Term t -> Term t -> Bool #

SupportedPrim t => Eq (Description (Term t)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

(==) :: Description (Term t) -> Description (Term t) -> Bool #

(/=) :: Description (Term t) -> Description (Term t) -> Bool #

SupportedPrim t => Hashable (Term t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

hashWithSalt :: Int -> Term t -> Int #

hash :: Term t -> Int #

SupportedPrim t => Hashable (Description (Term t)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

hashWithSalt :: Int -> Description (Term t) -> Int #

hash :: Description (Term t) -> Int #

SupportedPrim t => Interned (Term t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

data Description (Term t) #

type Uninterned (Term t) #

Methods

describe :: Uninterned (Term t) -> Description (Term t) #

identify :: Id -> Uninterned (Term t) -> Term t #

seedIdentity :: p (Term t) -> Id #

cacheWidth :: p (Term t) -> Int #

modifyAdvice :: IO (Term t) -> IO (Term t) #

cache :: Cache (Term t) #

data Description (Term t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

data Description (Term t) where
type Uninterned (Term t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

type Uninterned (Term t) = UTerm t

data UTerm t where Source #

Constructors

UConTerm :: SupportedPrim t => !t -> UTerm t 
USymTerm :: SupportedPrim t => !(TypedSymbol t) -> UTerm t 
UUnaryTerm :: UnaryOp tag arg t => !tag -> !(Term arg) -> UTerm t 
UBinaryTerm :: BinaryOp tag arg1 arg2 t => !tag -> !(Term arg1) -> !(Term arg2) -> UTerm t 
UTernaryTerm :: TernaryOp tag arg1 arg2 arg3 t => !tag -> !(Term arg1) -> !(Term arg2) -> !(Term arg3) -> UTerm t 
UNotTerm :: !(Term Bool) -> UTerm Bool 
UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool 
UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool 
UEqvTerm :: SupportedPrim t => !(Term t) -> !(Term t) -> UTerm Bool 
UITETerm :: SupportedPrim t => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t 
UAddNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t 
UUMinusNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t 
UTimesNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t 
UAbsNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t 
USignumNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t 
ULTNumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool 
ULENumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool 
UAndBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t 
UOrBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t 
UXorBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t 
UComplementBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> UTerm t 
UShiftBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !Int -> UTerm t 
URotateBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !Int -> UTerm t 
UBVConcatTerm :: (SupportedPrim (bv a), SupportedPrim (bv b), SupportedPrim (bv (a + b)), KnownNat a, KnownNat b, 1 <= a, 1 <= b, SizedBV bv) => !(Term (bv a)) -> !(Term (bv b)) -> UTerm (bv (a + b)) 
UBVSelectTerm :: (SupportedPrim (bv n), SupportedPrim (bv w), KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n, SizedBV bv) => !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv n)) -> UTerm (bv w) 
UBVExtendTerm :: (SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l, KnownNat r, 1 <= l, l <= r, SizedBV bv) => !Bool -> !(TypeRep r) -> !(Term (bv l)) -> UTerm (bv r) 
UTabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a =-> b) -> Term a -> UTerm b 
UGeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> UTerm b 
UDivIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t 
UModIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t 
UQuotIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t 
URemIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t 
UDivBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t 
UModBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t 
UQuotBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t 
URemBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t 

data a --> b where infixr 0 Source #

General symbolic function type. Use the # operator to apply the function. Note that this function should be applied to symbolic values only. It is by itself already a symbolic value, but can be considered partially concrete as the function body is specified. Use -~> for uninterpreted general symbolic functions.

The result would be partially evaluated.

>>> :set -XOverloadedStrings
>>> :set -XTypeOperators
>>> let f = ("x" :: TypedSymbol Integer) --> ("x" + 1 + "y" :: SymInteger) :: Integer --> Integer
>>> f # 1    -- 1 has the type SymInteger
(+ 2 y)
>>> f # "a"  -- "a" has the type SymInteger
(+ 1 (+ a y))

Constructors

GeneralFun :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b 

Instances

Instances details
Lift (a --> b :: Type) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

lift :: Quote m => (a --> b) -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => (a --> b) -> Code m (a --> b) #

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (ca --> cb)) (sa -~> sb) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

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

Show (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

showsPrec :: Int -> (a --> b) -> ShowS #

show :: (a --> b) -> String #

showList :: [a --> b] -> ShowS #

NFData (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

rnf :: (a --> b) -> () #

Eq (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

(==) :: (a --> b) -> (a --> b) -> Bool #

(/=) :: (a --> b) -> (a --> b) -> Bool #

(LinkedRep a sa, LinkedRep b sb) => Function (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type Arg (a --> b) Source #

type Ret (a --> b) Source #

Methods

(#) :: (a --> b) -> Arg (a --> b) -> Ret (a --> b) Source #

(SupportedPrim a, SupportedPrim b) => SupportedPrim (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (a --> b) Source #

Methods

withPrim :: proxy (a --> b) -> (PrimConstraint (a --> b) => a0) -> a0 Source #

termCache :: Cache (Term (a --> b)) Source #

pformatCon :: (a --> b) -> String Source #

pformatSym :: TypedSymbol (a --> b) -> String Source #

defaultValue :: a --> b Source #

defaultValueDynamic :: proxy (a --> b) -> ModelValue Source #

(SymRep ca, SymRep cb) => SymRep (ca --> cb) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType (ca --> cb) Source #

Hashable (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

hashWithSalt :: Int -> (a --> b) -> Int #

hash :: (a --> b) -> Int #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

con :: (ca --> cb) -> sa -~> sb Source #

conView :: (sa -~> sb) -> Maybe (ca --> cb) Source #

ssym :: String -> sa -~> sb Source #

isym :: String -> Int -> sa -~> sb Source #

sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> sa -~> sb Source #

iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> sa -~> sb Source #

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa -~> sb) (ca --> cb) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca --> cb) (sa -~> sb) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

(LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca --> cb) (sa -~> sb) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

type Arg (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

type Arg (a --> b) = SymType a
type Ret (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

type Ret (a --> b) = SymType b
type PrimConstraint (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

type SymType (ca --> cb) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type SymType (ca --> cb) = SymType ca -~> SymType cb