grisette-0.1.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 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

ModelRep (ModelValuePair t) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair t) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

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

ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair a, ModelSymPair b) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

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

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

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

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

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 c), KnownNat a, KnownNat b, KnownNat c, BVConcat (bv a) (bv b) (bv c)) => !Id -> !(Term (bv a)) -> !(Term (bv b)) -> Term (bv c) 
BVSelectTerm :: (SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a, KnownNat w, KnownNat ix, BVSelect (bv a) ix w (bv w)) => !Id -> !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv a)) -> Term (bv w) 
BVExtendTerm :: (SupportedPrim (bv a), SupportedPrim (bv b), KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b)) => !Id -> !Bool -> !(TypeRep n) -> !(Term (bv a)) -> Term (bv b) 
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 
DivIntegerTerm :: !Id -> Term Integer -> Term Integer -> Term Integer 
ModIntegerTerm :: !Id -> Term Integer -> Term Integer -> Term Integer 

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 c), KnownNat a, KnownNat b, KnownNat c, BVConcat (bv a) (bv b) (bv c)) => !(Term (bv a)) -> !(Term (bv b)) -> UTerm (bv c) 
UBVSelectTerm :: (SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a, KnownNat ix, KnownNat w, BVSelect (bv a) ix w (bv w)) => !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv a)) -> UTerm (bv w) 
UBVExtendTerm :: (SupportedPrim (bv a), SupportedPrim (bv b), KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b)) => !Bool -> !(TypeRep n) -> !(Term (bv a)) -> UTerm (bv b) 
UTabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a =-> b) -> Term a -> UTerm b 
UGeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> UTerm b 
UDivIntegerTerm :: Term Integer -> Term Integer -> UTerm Integer 
UModIntegerTerm :: Term Integer -> Term Integer -> UTerm Integer 

data FunArg Source #

Constructors

FunArg 

Instances

Instances details
Generic FunArg Source # 
Instance details

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

Associated Types

type Rep FunArg :: Type -> Type #

Methods

from :: FunArg -> Rep FunArg x #

to :: Rep FunArg x -> FunArg #

Show FunArg Source # 
Instance details

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

NFData FunArg Source # 
Instance details

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

Methods

rnf :: FunArg -> () #

Eq FunArg Source # 
Instance details

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

Methods

(==) :: FunArg -> FunArg -> Bool #

(/=) :: FunArg -> FunArg -> Bool #

Ord FunArg Source # 
Instance details

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

Hashable FunArg Source # 
Instance details

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

Methods

hashWithSalt :: Int -> FunArg -> Int #

hash :: FunArg -> Int #

Lift FunArg Source # 
Instance details

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

Methods

lift :: Quote m => FunArg -> m Exp #

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

type Rep FunArg Source # 
Instance details

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

type Rep FunArg = D1 ('MetaData "FunArg" "Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'False) (C1 ('MetaCons "FunArg" 'PrefixI 'False) (U1 :: Type -> Type))

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

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 #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

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) => Function (a -~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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 #

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 #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Ret (a --> b) = Sym b
type Ret (a -~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

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