Safe Haskell | None |
---|---|
Language | Haskell98 |
- class Same tps
- class IsSMTNumber tp
- class HasMonad a where
- type MatchMonad a m :: Constraint
- type MonadResult a :: *
- embedM :: (Monad m, MatchMonad a m) => a -> m (MonadResult a)
- pattern Var :: (~) Type tp rtp => v tp -> Expression v qv fun con field fv lv e rtp
- class SMTType t
- pattern ConstBool :: (~) Type rtp BoolType => Bool -> Expression v qv fun con field fv lv e rtp
- pattern ConstInt :: (~) Type rtp IntType => Integer -> Expression v qv fun con field fv lv e rtp
- pattern ConstReal :: (~) Type rtp RealType => Rational -> Expression v qv fun con field fv lv e rtp
- pattern ConstBV :: (~) Type rtp (BitVecType bw) => Integer -> Natural bw -> Expression v qv fun con field fv lv e rtp
- constant :: (Embed m e, SMTType tp) => tp -> m (e (SMTReprType tp))
- asConstant :: SMTType tp => Expression v qv fun con field fv lv e (SMTReprType tp) -> Maybe tp
- true :: Embed m e => m (e BoolType)
- false :: Embed m e => m (e BoolType)
- cbool :: Embed m e => Bool -> m (e BoolType)
- cint :: Embed m e => Integer -> m (e IntType)
- creal :: Embed m e => Rational -> m (e RealType)
- cbv :: Embed m e => Integer -> Natural bw -> m (e (BitVecType bw))
- pattern Fun :: (~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type arg res) => t ((,) [Type] Type arg res) -> List Type t arg -> Expression t t t t t t t t t
- fun :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e args) => EmFun m e `(args, res)` -> a -> m (e res)
- pattern EqLst :: (~) Type rtp BoolType => GetType e => [e tp] -> Expression v qv fun con field fv lv e rtp
- pattern Eq :: ((~) Type rtp BoolType, Same tps) => GetType e => List Type e tps -> Expression v qv fun con field fv lv e rtp
- pattern (:==:) :: (~) Type rtp BoolType => GetType e => e tp -> e tp -> Expression v qv fun con field fv lv e rtp
- eq :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType)
- (.==.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
- pattern DistinctLst :: (~) Type rtp BoolType => GetType e => [e tp] -> Expression v qv fun con field fv lv e rtp
- pattern Distinct :: ((~) Type rtp BoolType, Same tps) => GetType e => List Type e tps -> Expression v qv fun con field fv lv e rtp
- pattern (:/=:) :: (~) Type rtp BoolType => GetType e => e tp -> e tp -> Expression v qv fun con field fv lv e rtp
- distinct :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType)
- (./=.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
- map' :: (Embed m e, HasMonad arg, MatchMonad arg m, MonadResult arg ~ List e (Lifted tps idx), Unlift tps idx, GetType e, GetFunType (EmFun m e), GetFieldType (EmField m e), GetConType (EmConstr m e)) => Function (EmFun m e) (EmConstr m e) (EmField m e) `(tps, res)` -> arg -> m (e (ArrayType idx res))
- pattern Ord :: ((~) Type rtp BoolType, IsSMTNumber tp) => OrdOp -> e tp -> e tp -> Expression v qv fun con field fv lv e rtp
- pattern (:>=:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp
- pattern (:>:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp
- pattern (:<=:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp
- pattern (:<:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp
- ord :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => OrdOp -> a -> b -> m (e BoolType)
- (.>=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
- (.>.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
- (.<=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
- (.<.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
- pattern ArithLst :: IsSMTNumber tp => ArithOp -> [e tp] -> Expression v qv fun con field fv lv e tp
- pattern Arith :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => ArithOp -> List Type e tps -> Expression v qv fun con field fv lv e tp
- arith :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => ArithOp -> [a] -> m (e tp)
- pattern PlusLst :: IsSMTNumber tp => [e tp] -> Expression v qv fun con field fv lv e tp
- pattern Plus :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun con field fv lv e tp
- pattern (:+:) :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> e x -> Expression v qv fun con field fv lv e tp
- plus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)
- (.+.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp)
- pattern MultLst :: IsSMTNumber tp => [e tp] -> Expression v qv fun con field fv lv e tp
- pattern Mult :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun con field fv lv e tp
- pattern (:*:) :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> e x -> Expression v qv fun con field fv lv e tp
- mult :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)
- (.*.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp)
- pattern MinusLst :: IsSMTNumber tp => [e tp] -> Expression v qv fun con field fv lv e tp
- pattern Minus :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun con field fv lv e tp
- pattern (:-:) :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> e x -> Expression v qv fun con field fv lv e tp
- pattern Neg :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> Expression v qv fun con field fv lv e tp
- minus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)
- (.-.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp)
- neg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp)
- pattern Div :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t
- pattern Mod :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t
- pattern Rem :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t
- div' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType)
- mod' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType)
- rem' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType)
- pattern (:/:) :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type RealType ((:) Type RealType ([] Type))) RealType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t
- (./.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e RealType, MonadResult b ~ e RealType) => a -> b -> m (e RealType)
- pattern Abs :: IsSMTNumber tp => e tp -> Expression v qv fun con field fv lv e tp
- abs' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp)
- pattern Not :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type BoolType ([] Type)) BoolType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> Expression t t t t t t t t t
- not' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => a -> m (e BoolType)
- pattern LogicLst :: (~) Type rtp BoolType => LogicOp -> [e BoolType] -> Expression v qv fun con field fv lv e rtp
- pattern Logic :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => LogicOp -> List Type e tps -> Expression v qv fun con field fv lv e rtp
- logic :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => LogicOp -> [a] -> m (e BoolType)
- pattern AndLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp
- pattern And :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp
- pattern (:&:) :: (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun con field fv lv e rtp
- and' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)
- (.&.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType)
- pattern OrLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp
- pattern Or :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp
- pattern (:|:) :: (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun con field fv lv e rtp
- or' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)
- (.|.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType)
- pattern XOrLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp
- pattern XOr :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp
- xor' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)
- pattern ImpliesLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp
- pattern Implies :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp
- pattern (:=>:) :: (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun con field fv lv e rtp
- implies :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)
- (.=>.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType)
- pattern ToReal :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ([] Type)) RealType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> Expression t t t t t t t t t
- pattern ToInt :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type RealType ([] Type)) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> Expression t t t t t t t t t
- toReal :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => a -> m (e RealType)
- toInt :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e RealType) => a -> m (e IntType)
- pattern ITE :: () => GetType e => e BoolType -> e tp -> e tp -> Expression v qv fun con field fv lv e tp
- ite :: (Embed m e, HasMonad a, HasMonad b, HasMonad c, MatchMonad a m, MatchMonad b m, MatchMonad c m, MonadResult a ~ e BoolType, MonadResult b ~ e tp, MonadResult c ~ e tp) => a -> b -> c -> m (e tp)
- pattern BVComp :: (~) Type rtp BoolType => GetType e => BVCompOp -> e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVULE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVULT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVUGE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVUGT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVSLE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVSLT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVSGE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVSGT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- bvcomp :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVCompOp -> a -> b -> m (e BoolType)
- bvule :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
- bvult :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
- bvuge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
- bvugt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
- bvsle :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
- bvslt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
- bvsge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
- bvsgt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
- pattern BVBin :: (~) Type rtp (BitVecType bw) => GetType e => BVBinOp -> e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVAdd :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVSub :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVMul :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVURem :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVSRem :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVUDiv :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVSDiv :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVSHL :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVLSHR :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVASHR :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVXor :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVAnd :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVOr :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- bvbin :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVBinOp -> a -> b -> m (e (BitVecType bw))
- bvadd :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
- bvsub :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
- bvmul :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
- bvurem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
- bvsrem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
- bvudiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
- bvsdiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
- bvshl :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
- bvlshr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
- bvashr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
- bvxor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
- bvand :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
- bvor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
- pattern BVUn :: (~) Type rtp (BitVecType bw) => GetType e => BVUnOp -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVNot :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- pattern BVNeg :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- bvun :: forall m e a bw. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => BVUnOp -> a -> m (e (BitVecType bw))
- bvnot :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw))
- bvneg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw))
- pattern Concat :: (~) Type rtp (BitVecType ((+) n1 n2)) => GetType e => e (BitVecType n1) -> e (BitVecType n2) -> Expression v qv fun con field fv lv e rtp
- pattern Extract :: ((~) Type rtp (BitVecType len), (~) Bool ((<=) ((+) start len) bw) True) => GetType e => Natural start -> Natural len -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp
- concat' :: forall m e a b n1 n2. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType n1), MonadResult b ~ e (BitVecType n2)) => a -> b -> m (e (BitVecType (n1 + n2)))
- extract' :: forall m e a bw start len. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw), ((start + len) <= bw) ~ True) => Natural start -> Natural len -> a -> m (e (BitVecType len))
- pattern Select :: (~) Type rtp val => GetType e => e (ArrayType idx val) -> List Type e idx -> Expression v qv fun con field fv lv e rtp
- pattern Store :: (~) Type rtp (ArrayType idx val) => GetType e => e (ArrayType idx val) -> List Type e idx -> e val -> Expression v qv fun con field fv lv e rtp
- pattern ConstArray :: (~) Type rtp (ArrayType idx val) => GetType e => List Type Repr idx -> e val -> Expression v qv fun con field fv lv e rtp
- select :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx) => arr -> i -> m (e el)
- select1 :: (Embed m e, HasMonad arr, HasMonad idx, MatchMonad arr m, MatchMonad idx m, MonadResult arr ~ e (ArrayType `[idx']` el), MonadResult idx ~ e idx') => arr -> idx -> m (e el)
- store :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx, HasMonad nel, MatchMonad nel m, MonadResult nel ~ e el) => arr -> i -> nel -> m (e (ArrayType idx el))
- store1 :: (Embed m e, HasMonad arr, HasMonad idx, HasMonad el, MatchMonad arr m, MatchMonad idx m, MatchMonad el m, MonadResult arr ~ e (ArrayType `[idx']` el'), MonadResult idx ~ e idx', MonadResult el ~ e el') => arr -> idx -> el -> m (e (ArrayType `[idx']` el'))
- constArray :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => List Repr idx -> a -> m (e (ArrayType idx tp))
- pattern Divisible :: (~) Type rtp BoolType => Integer -> e IntType -> Expression v qv fun con field fv lv e rtp
- divisible :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => Integer -> a -> m (e BoolType)
- (.:.) :: (HasMonad a, MonadResult a ~ e tp, MatchMonad a m, Monad m) => a -> m (List e tps) -> m (List e (tp : tps))
- nil :: Monad m => m (List e `[]`)
Documentation
All elements of this list must be of the same type
sameType, sameToAllEq
class IsSMTNumber tp Source
smtNumRepr, smtFromInteger
type MatchMonad a m :: Constraint Source
type MonadResult a :: * Source
embedM :: (Monad m, MatchMonad a m) => a -> m (MonadResult a) Source
Expressions
pattern Var :: (~) Type tp rtp => v tp -> Expression v qv fun con field fv lv e rtp Source
Constants
toSMTConst, fromSMTConst
pattern ConstBool :: (~) Type rtp BoolType => Bool -> Expression v qv fun con field fv lv e rtp Source
pattern ConstInt :: (~) Type rtp IntType => Integer -> Expression v qv fun con field fv lv e rtp Source
pattern ConstReal :: (~) Type rtp RealType => Rational -> Expression v qv fun con field fv lv e rtp Source
pattern ConstBV :: (~) Type rtp (BitVecType bw) => Integer -> Natural bw -> Expression v qv fun con field fv lv e rtp Source
asConstant :: SMTType tp => Expression v qv fun con field fv lv e (SMTReprType tp) -> Maybe tp Source
Functions
pattern Fun :: (~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type arg res) => t ((,) [Type] Type arg res) -> List Type t arg -> Expression t t t t t t t t t Source
fun :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e args) => EmFun m e `(args, res)` -> a -> m (e res) Source
Equality
pattern EqLst :: (~) Type rtp BoolType => GetType e => [e tp] -> Expression v qv fun con field fv lv e rtp Source
pattern Eq :: ((~) Type rtp BoolType, Same tps) => GetType e => List Type e tps -> Expression v qv fun con field fv lv e rtp Source
pattern (:==:) :: (~) Type rtp BoolType => GetType e => e tp -> e tp -> Expression v qv fun con field fv lv e rtp Source
eq :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType) Source
(.==.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4 Source
pattern DistinctLst :: (~) Type rtp BoolType => GetType e => [e tp] -> Expression v qv fun con field fv lv e rtp Source
pattern Distinct :: ((~) Type rtp BoolType, Same tps) => GetType e => List Type e tps -> Expression v qv fun con field fv lv e rtp Source
pattern (:/=:) :: (~) Type rtp BoolType => GetType e => e tp -> e tp -> Expression v qv fun con field fv lv e rtp Source
distinct :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType) Source
(./=.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4 Source
Map
map' :: (Embed m e, HasMonad arg, MatchMonad arg m, MonadResult arg ~ List e (Lifted tps idx), Unlift tps idx, GetType e, GetFunType (EmFun m e), GetFieldType (EmField m e), GetConType (EmConstr m e)) => Function (EmFun m e) (EmConstr m e) (EmField m e) `(tps, res)` -> arg -> m (e (ArrayType idx res)) Source
Comparison
pattern Ord :: ((~) Type rtp BoolType, IsSMTNumber tp) => OrdOp -> e tp -> e tp -> Expression v qv fun con field fv lv e rtp Source
pattern (:>=:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp Source
pattern (:>:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp Source
pattern (:<=:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp Source
pattern (:<:) :: ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun con field fv lv e rtp Source
ord :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => OrdOp -> a -> b -> m (e BoolType) Source
(.>=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4 Source
(.>.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4 Source
(.<=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4 Source
(.<.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4 Source
Arithmetic
pattern ArithLst :: IsSMTNumber tp => ArithOp -> [e tp] -> Expression v qv fun con field fv lv e tp Source
pattern Arith :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => ArithOp -> List Type e tps -> Expression v qv fun con field fv lv e tp Source
arith :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => ArithOp -> [a] -> m (e tp) Source
pattern PlusLst :: IsSMTNumber tp => [e tp] -> Expression v qv fun con field fv lv e tp Source
pattern Plus :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun con field fv lv e tp Source
pattern (:+:) :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> e x -> Expression v qv fun con field fv lv e tp Source
plus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp) Source
(.+.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp) infixl 6 Source
pattern MultLst :: IsSMTNumber tp => [e tp] -> Expression v qv fun con field fv lv e tp Source
pattern Mult :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun con field fv lv e tp Source
pattern (:*:) :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> e x -> Expression v qv fun con field fv lv e tp Source
mult :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp) Source
(.*.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp) infixl 7 Source
pattern MinusLst :: IsSMTNumber tp => [e tp] -> Expression v qv fun con field fv lv e tp Source
pattern Minus :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun con field fv lv e tp Source
pattern (:-:) :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> e x -> Expression v qv fun con field fv lv e tp Source
pattern Neg :: (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~) [Type] tps ((:) Type x xs), (~) [Type] xs ([] Type)) => e x -> Expression v qv fun con field fv lv e tp Source
minus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp) Source
(.-.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp) infixl 6 Source
neg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp) Source
pattern Div :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t Source
pattern Mod :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t Source
pattern Rem :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t Source
div' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType) infixl 7 Source
mod' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType) infixl 7 Source
rem' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType) infixl 7 Source
pattern (:/:) :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type RealType ((:) Type RealType ([] Type))) RealType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> t x -> Expression t t t t t t t t t Source
(./.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e RealType, MonadResult b ~ e RealType) => a -> b -> m (e RealType) infixl 7 Source
pattern Abs :: IsSMTNumber tp => e tp -> Expression v qv fun con field fv lv e tp Source
abs' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp) Source
Logic
pattern Not :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type BoolType ([] Type)) BoolType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> Expression t t t t t t t t t Source
not' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => a -> m (e BoolType) Source
pattern LogicLst :: (~) Type rtp BoolType => LogicOp -> [e BoolType] -> Expression v qv fun con field fv lv e rtp Source
pattern Logic :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => LogicOp -> List Type e tps -> Expression v qv fun con field fv lv e rtp Source
logic :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => LogicOp -> [a] -> m (e BoolType) Source
pattern AndLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp Source
pattern And :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp Source
pattern (:&:) :: (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun con field fv lv e rtp Source
and' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType) Source
(.&.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType) infixr 3 Source
pattern OrLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp Source
pattern Or :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp Source
pattern (:|:) :: (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun con field fv lv e rtp Source
or' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType) Source
(.|.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType) infixr 2 Source
pattern XOrLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp Source
pattern XOr :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp Source
xor' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType) Source
pattern ImpliesLst :: (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun con field fv lv e rtp Source
pattern Implies :: ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun con field fv lv e rtp Source
pattern (:=>:) :: (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun con field fv lv e rtp Source
implies :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType) Source
(.=>.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType) infixr 2 Source
Conversion
pattern ToReal :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ([] Type)) RealType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> Expression t t t t t t t t t Source
pattern ToInt :: ((~) ((,) [Type] Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type RealType ([] Type)) IntType), (~) [Type] arg ((:) Type x xs), (~) [Type] xs ([] Type)) => t x -> Expression t t t t t t t t t Source
toReal :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => a -> m (e RealType) Source
toInt :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e RealType) => a -> m (e IntType) Source
If-then-else
pattern ITE :: () => GetType e => e BoolType -> e tp -> e tp -> Expression v qv fun con field fv lv e tp Source
ite :: (Embed m e, HasMonad a, HasMonad b, HasMonad c, MatchMonad a m, MatchMonad b m, MatchMonad c m, MonadResult a ~ e BoolType, MonadResult b ~ e tp, MonadResult c ~ e tp) => a -> b -> c -> m (e tp) Source
Bitvectors
pattern BVComp :: (~) Type rtp BoolType => GetType e => BVCompOp -> e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVULE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVULT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVUGE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVUGT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVSLE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVSLT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVSGE :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVSGT :: (~) Type rtp BoolType => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
bvcomp :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVCompOp -> a -> b -> m (e BoolType) Source
bvule :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source
bvult :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source
bvuge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source
bvugt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source
bvsle :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source
bvslt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source
bvsge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source
bvsgt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source
pattern BVBin :: (~) Type rtp (BitVecType bw) => GetType e => BVBinOp -> e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVAdd :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVSub :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVMul :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVURem :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVSRem :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVUDiv :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVSDiv :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVSHL :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVLSHR :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVASHR :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVXor :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVAnd :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVOr :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
bvbin :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVBinOp -> a -> b -> m (e (BitVecType bw)) Source
bvadd :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source
bvsub :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source
bvmul :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source
bvurem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source
bvsrem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source
bvudiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source
bvsdiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source
bvshl :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source
bvlshr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source
bvashr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source
bvxor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source
bvand :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source
bvor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source
pattern BVUn :: (~) Type rtp (BitVecType bw) => GetType e => BVUnOp -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVNot :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
pattern BVNeg :: (~) Type rtp (BitVecType bw) => GetType e => e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
bvun :: forall m e a bw. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => BVUnOp -> a -> m (e (BitVecType bw)) Source
bvnot :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw)) Source
bvneg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw)) Source
pattern Concat :: (~) Type rtp (BitVecType ((+) n1 n2)) => GetType e => e (BitVecType n1) -> e (BitVecType n2) -> Expression v qv fun con field fv lv e rtp Source
pattern Extract :: ((~) Type rtp (BitVecType len), (~) Bool ((<=) ((+) start len) bw) True) => GetType e => Natural start -> Natural len -> e (BitVecType bw) -> Expression v qv fun con field fv lv e rtp Source
concat' :: forall m e a b n1 n2. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType n1), MonadResult b ~ e (BitVecType n2)) => a -> b -> m (e (BitVecType (n1 + n2))) Source
extract' :: forall m e a bw start len. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw), ((start + len) <= bw) ~ True) => Natural start -> Natural len -> a -> m (e (BitVecType len)) Source
Arrays
pattern Select :: (~) Type rtp val => GetType e => e (ArrayType idx val) -> List Type e idx -> Expression v qv fun con field fv lv e rtp Source
pattern Store :: (~) Type rtp (ArrayType idx val) => GetType e => e (ArrayType idx val) -> List Type e idx -> e val -> Expression v qv fun con field fv lv e rtp Source
pattern ConstArray :: (~) Type rtp (ArrayType idx val) => GetType e => List Type Repr idx -> e val -> Expression v qv fun con field fv lv e rtp Source
select :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx) => arr -> i -> m (e el) Source
select1 :: (Embed m e, HasMonad arr, HasMonad idx, MatchMonad arr m, MatchMonad idx m, MonadResult arr ~ e (ArrayType `[idx']` el), MonadResult idx ~ e idx') => arr -> idx -> m (e el) Source
store :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx, HasMonad nel, MatchMonad nel m, MonadResult nel ~ e el) => arr -> i -> nel -> m (e (ArrayType idx el)) Source
store1 :: (Embed m e, HasMonad arr, HasMonad idx, HasMonad el, MatchMonad arr m, MatchMonad idx m, MatchMonad el m, MonadResult arr ~ e (ArrayType `[idx']` el'), MonadResult idx ~ e idx', MonadResult el ~ e el') => arr -> idx -> el -> m (e (ArrayType `[idx']` el')) Source
constArray :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => List Repr idx -> a -> m (e (ArrayType idx tp)) Source
Misc
pattern Divisible :: (~) Type rtp BoolType => Integer -> e IntType -> Expression v qv fun con field fv lv e rtp Source
divisible :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => Integer -> a -> m (e BoolType) Source
Lists
(.:.) :: (HasMonad a, MonadResult a ~ e tp, MatchMonad a m, Monad m) => a -> m (List e tps) -> m (List e (tp : tps)) infixr 5 Source