| Copyright | (c) Sirui Lu 2021-2023 |
|---|---|
| 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.IR.SymPrim.Data.Prim.InternedTerm.Term
Description
Synopsis
- class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where
- type PrimConstraint t :: Constraint
- withPrim :: proxy t -> (PrimConstraint t => a) -> a
- termCache :: Cache (Term t)
- pformatCon :: t -> String
- pformatSym :: TypedSymbol t -> String
- defaultValue :: t
- defaultValueDynamic :: proxy t -> ModelValue
- 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
- partialEvalUnary :: (Typeable tag, Typeable t) => tag -> Term arg -> Term t
- pformatUnary :: tag -> Term arg -> String
- 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
- partialEvalBinary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term t
- pformatBinary :: tag -> Term arg1 -> Term arg2 -> String
- 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
- data TypedSymbol t where
- 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
- data SomeTypedSymbol where
- SomeTypedSymbol :: forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol
- showUntyped :: TypedSymbol t -> String
- withSymbolSupported :: TypedSymbol t -> (SupportedPrim t => a) -> a
- someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol
- data Term t where
- 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
- data UTerm t where
- 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 = FunArg
- data a --> b where
- GeneralFun :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b
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
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
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 #
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 #
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 #
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 Boola :: 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
data SomeTypedSymbol where Source #
Constructors
| SomeTypedSymbol :: forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol |
Instances
showUntyped :: TypedSymbol t -> String Source #
withSymbolSupported :: TypedSymbol t -> (SupportedPrim t => a) -> a Source #
someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol Source #
Constructors
Instances
Constructors
Constructors
| FunArg |
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 |