Language.SMTLib2.Internals.Interface

Documentation

class Same tps

All elements of this list must be of the same type

Minimal complete definition

sameType, sameToAllEq

Instances

(Same ((:) Type tp tps), (~) Type tp (SameType ((:) Type tp tps))) => Same ((:) Type tp ((:) Type tp tps))

Associated Types

type SameType ((:) Type tp ((:) Type tp tps) :: [Type]) :: Type

Methods

sameType :: List Type Repr ((Type ': tp) ((Type ': tp) tps)) -> Repr (SameType ((Type ': tp) ((Type ': tp) tps)))

sameToAllEq :: List Type e ((Type ': tp) ((Type ': tp) tps)) -> List Type e (AllEq (SameType ((Type ': tp) ((Type ': tp) tps))) (Length Type ((Type ': tp) ((Type ': tp) tps))))

Same ((:) Type tp ([] Type))

Associated Types

type SameType ((:) Type tp ([] Type) :: [Type]) :: Type

Methods

sameType :: List Type Repr ((Type ': tp) [Type]) -> Repr (SameType ((Type ': tp) [Type]))

sameToAllEq :: List Type e ((Type ': tp) [Type]) -> List Type e (AllEq (SameType ((Type ': tp) [Type])) (Length Type ((Type ': tp) [Type])))

class Num (Value tp) => IsSMTNumber tp

Minimal complete definition

smtNumRepr, smtFromInteger

Instances

IsSMTNumber IntType

Methods

smtNumRepr :: NumRepr IntType

smtFromInteger :: Integer -> Value IntType

IsSMTNumber RealType

Methods

smtNumRepr :: NumRepr RealType

smtFromInteger :: Integer -> Value RealType

class HasMonad a where

Minimal complete definition

embedM

Associated Types

type MatchMonad a (m :: * -> *) :: Constraint

type MonadResult a :: *

Methods

embedM :: (Applicative m, MatchMonad a m) => a -> m (MonadResult a)

Instances

HasMonad (m (List Type e tp))

Associated Types

type MatchMonad (m (List Type e tp)) (m :: * -> *) :: Constraint

type MonadResult (m (List Type e tp)) :: *

Methods

embedM :: (Applicative m, MatchMonad (m (List Type e tp)) m) => m (List Type e tp) -> m (MonadResult (m (List Type e tp)))

HasMonad (m (e tp))

Associated Types

type MatchMonad (m (e tp)) (m :: * -> *) :: Constraint

type MonadResult (m (e tp)) :: *

Methods

embedM :: (Applicative m, MatchMonad (m (e tp)) m) => m (e tp) -> m (MonadResult (m (e tp)))

HasMonad (e tp)

Associated Types

type MatchMonad (e tp) (m :: * -> *) :: Constraint

type MonadResult (e tp) :: *

Methods

embedM :: (Applicative m, MatchMonad (e tp) m) => e tp -> m (MonadResult (e tp))

HasMonad (List Type e tp)

Associated Types

type MatchMonad (List Type e tp) (m :: * -> *) :: Constraint

type MonadResult (List Type e tp) :: *

Methods

embedM :: (Applicative m, MatchMonad (List Type e tp) m) => List Type e tp -> m (MonadResult (List Type e tp))

Expressions

pattern Var :: forall rtp v qv fun fv lv e. () => forall tp. (~) Type tp rtp => v tp -> Expression v qv fun fv lv e rtp

Constants

pattern ConstBool :: forall rtp v qv fun fv lv e. () => (~) Type rtp BoolType => Bool -> Expression v qv fun fv lv e rtp

Matches constant boolean expressions (true or false).

pattern ConstInt :: forall rtp v qv fun fv lv e. () => (~) Type rtp IntType => Integer -> Expression v qv fun fv lv e rtp

pattern ConstReal :: forall rtp v qv fun fv lv e. () => (~) Type rtp RealType => Rational -> Expression v qv fun fv lv e rtp

pattern ConstBV :: forall rtp v qv fun fv lv e. () => forall bw. (~) Type rtp (BitVecType bw) => Integer -> BitWidth bw -> Expression v qv fun fv lv e rtp

constant :: Embed m e => Value tp -> m (e tp)

Create a constant, for example an integer:

Example:

do
  x <- declareVar int
  -- x is greater than 5
  assert $ x .>. constant (IntValue 5)
  

asConstant :: Expression v qv fun fv lv e tp -> Maybe (Value tp)

true :: Embed m e => m (e BoolType)

Create the boolean expression "true".

false :: Embed m e => m (e BoolType)

Create the boolean expression "false".

cbool :: Embed m e => Bool -> m (e BoolType)

Create a boolean constant expression.

cint :: Embed m e => Integer -> m (e IntType)

Create an integer constant expression.

creal :: Embed m e => Rational -> m (e RealType)

Create a real constant expression.

Example:

import Data.Ratio

x = creal (5 % 4)
  

cbv

Arguments

:: Embed m e

=> Integer

The value (negative values will be stored in two's-complement).

-> BitWidth bw

The bitwidth of the bitvector value.

-> m (e (BitVecType bw))

Create a constant bitvector expression.

cbvUntyped

Arguments

:: (Embed m e, Monad m)

=> Integer

The value (negative values will be stored in two's-complement).

-> Integer

The bitwidth (must be >= 0).

-> (forall bw. e (BitVecType bw) -> m b)

-> m b

Create an untyped constant bitvector expression.

cdt :: (Embed m e, IsDatatype t, Length par ~ Parameters t) => t par Value -> m (e (DataType t par))

Quantification

exists :: (Embed m e, Monad m) => List Repr tps -> (forall m e. (Embed m e, Monad m) => List e tps -> m (e BoolType)) -> m (e BoolType)

forall :: (Embed m e, Monad m) => List Repr tps -> (forall m e. (Embed m e, Monad m) => List e tps -> m (e BoolType)) -> m (e BoolType)

Functions

pattern Fun :: forall t t1 t2 t3 t4 t5 t6. () => forall arg arg1 res. (~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type arg1 res) => t5 ((,) [Type] Type arg1 res) -> List Type t6 arg -> Expression t4 t3 t5 t2 t1 t6 t

app :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e args) => Function (EmFun m e) '(args, res) -> a -> m (e res)

Create an expression by applying a function to a list of arguments.

fun :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e args) => EmFun m e '(args, res) -> a -> m (e res)

Equality

pattern EqLst :: forall e rtp v qv fun fv lv. GetType e => forall tp. (~) Type rtp BoolType => [e tp] -> Expression v qv fun fv lv e rtp

pattern Eq :: forall e rtp v qv fun fv lv. GetType e => forall tps. ((~) Type rtp BoolType, Same tps) => List Type e tps -> Expression v qv fun fv lv e rtp

pattern (:==:) :: forall e rtp v qv fun fv lv. GetType e => forall tp. (~) Type rtp BoolType => e tp -> e tp -> Expression v qv fun 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) infix 4

Create a boolean expression that encodes that two expressions have the same value.

Example:

is5 :: Backend b => Expr b IntType -> SMT b BoolType
is5 e = e .==. cint 5
  

pattern DistinctLst :: forall e rtp v qv fun fv lv. GetType e => forall tp. (~) Type rtp BoolType => [e tp] -> Expression v qv fun fv lv e rtp

pattern Distinct :: forall e rtp v qv fun fv lv. GetType e => forall tps. ((~) Type rtp BoolType, Same tps) => List Type e tps -> Expression v qv fun fv lv e rtp

pattern (:/=:) :: forall e rtp v qv fun fv lv. GetType e => forall tp. (~) Type rtp BoolType => e tp -> e tp -> Expression v qv fun 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) infix 4

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)) => Function (EmFun m e) '(tps, res) -> arg -> m (e (ArrayType idx res))

Comparison

pattern Ord :: forall rtp e v qv fun fv lv. () => forall tp. ((~) Type rtp BoolType, IsSMTNumber tp) => OrdOp -> e tp -> e tp -> Expression v qv fun fv lv e rtp

pattern (:>=:) :: forall rtp e v qv fun fv lv. () => forall tp. ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun fv lv e rtp

pattern (:>:) :: forall rtp e v qv fun fv lv. () => forall tp. ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun fv lv e rtp

pattern (:<=:) :: forall rtp e v qv fun fv lv. () => forall tp. ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun fv lv e rtp

pattern (:<:) :: forall rtp e v qv fun fv lv. () => forall tp. ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun 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) infix 4

(.>.) :: (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

(.<=.) :: (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

(.<.) :: (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

Arithmetic

pattern ArithLst :: forall tp e v qv fun fv lv. () => IsSMTNumber tp => ArithOp -> [e tp] -> Expression v qv fun fv lv e tp

pattern Arith :: forall tp e v qv fun fv lv. () => forall tps. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => ArithOp -> List Type e tps -> Expression v qv fun 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 :: forall lv fv fun qv v tp e. () => IsSMTNumber tp => [e tp] -> Expression v qv fun fv lv e tp

pattern Plus :: forall tp lv fv fun qv v e. () => forall tps. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun fv lv e tp

pattern (:+:) :: forall tp lv fv fun qv v e. () => forall tps x xs x1 xs1. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~#) [Type] [Type] tps ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => e x -> e x1 -> Expression v qv fun 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) infixl 6

pattern MultLst :: forall lv fv fun qv v tp e. () => IsSMTNumber tp => [e tp] -> Expression v qv fun fv lv e tp

pattern Mult :: forall tp lv fv fun qv v e. () => forall tps. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun fv lv e tp

pattern (:*:) :: forall tp lv fv fun qv v e. () => forall tps x xs x1 xs1. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~#) [Type] [Type] tps ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => e x -> e x1 -> Expression v qv fun 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) infixl 7

pattern MinusLst :: forall lv fv fun qv v tp e. () => IsSMTNumber tp => [e tp] -> Expression v qv fun fv lv e tp

pattern Minus :: forall tp lv fv fun qv v e. () => forall tps. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun fv lv e tp

pattern (:-:) :: forall tp lv fv fun qv v e. () => forall tps x xs x1 xs1. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~#) [Type] [Type] tps ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => e x -> e x1 -> Expression v qv fun fv lv e tp

pattern Neg :: forall tp lv fv fun qv v e. () => forall tps x xs. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~#) [Type] [Type] tps ((:) Type x xs), (~#) [Type] [Type] xs ([] Type)) => e x -> Expression v qv fun 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) infixl 6

neg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp)

pattern Div :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs x1 xs1. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => t6 x -> t6 x1 -> Expression t5 t4 t3 t2 t1 t6 t

pattern Mod :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs x1 xs1. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => t6 x -> t6 x1 -> Expression t5 t4 t3 t2 t1 t6 t

pattern Rem :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs x1 xs1. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => t6 x -> t6 x1 -> Expression t5 t4 t3 t2 t1 t6 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) infixl 7

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

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

pattern (:/:) :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs x1 xs1. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type RealType ((:) Type RealType ([] Type))) RealType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => t6 x -> t6 x1 -> Expression t5 t4 t3 t2 t1 t6 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) infixl 7

pattern Abs :: forall tp e v qv fun fv lv. () => IsSMTNumber tp => e tp -> Expression v qv fun fv lv e tp

abs' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp)

Logic

pattern Not :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type BoolType ([] Type)) BoolType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ([] Type)) => t6 x -> Expression t5 t4 t3 t2 t1 t6 t

not' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => a -> m (e BoolType)

pattern LogicLst :: forall rtp e v qv fun fv lv. () => (~) Type rtp BoolType => LogicOp -> [e BoolType] -> Expression v qv fun fv lv e rtp

pattern Logic :: forall rtp e v qv fun fv lv. () => forall tps. ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => LogicOp -> List Type e tps -> Expression v qv fun fv lv e rtp

logic :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => LogicOp -> [a] -> m (e BoolType)

pattern AndLst :: forall rtp lv fv fun qv v e. () => (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun fv lv e rtp

pattern And :: forall rtp lv fv fun qv v e. () => forall tps. ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun fv lv e rtp

pattern (:&:) :: forall rtp e v qv fun fv lv. () => (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun 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) infixr 3

pattern OrLst :: forall rtp lv fv fun qv v e. () => (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun fv lv e rtp

pattern Or :: forall rtp lv fv fun qv v e. () => forall tps. ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun fv lv e rtp

pattern (:|:) :: forall rtp e v qv fun fv lv. () => (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun 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) infixr 2

pattern XOrLst :: forall rtp lv fv fun qv v e. () => (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun fv lv e rtp

pattern XOr :: forall rtp lv fv fun qv v e. () => forall tps. ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun fv lv e rtp

xor' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)

pattern ImpliesLst :: forall rtp lv fv fun qv v e. () => (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun fv lv e rtp

pattern Implies :: forall rtp lv fv fun qv v e. () => forall tps. ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun fv lv e rtp

pattern (:=>:) :: forall rtp e v qv fun fv lv. () => (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun 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) infixr 2

Conversion

pattern ToReal :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ([] Type)) RealType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ([] Type)) => t6 x -> Expression t5 t4 t3 t2 t1 t6 t

pattern ToInt :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type RealType ([] Type)) IntType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ([] Type)) => t6 x -> Expression t5 t4 t3 t2 t1 t6 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)

If-then-else

pattern ITE :: forall e tp v qv fun fv lv. GetType e => e BoolType -> e tp -> e tp -> Expression v qv fun 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)

Bitvectors

pattern BVComp :: forall e rtp v qv fun fv lv. GetType e => forall bw. (~) Type rtp BoolType => BVCompOp -> e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVULE :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVULT :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVUGE :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVUGT :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVSLE :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVSLT :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVSGE :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVSGT :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun 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 :: forall e rtp v qv fun fv lv. GetType e => forall bw. (~) Type rtp (BitVecType bw) => BVBinOp -> e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVAdd :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVSub :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVMul :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVURem :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVSRem :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVUDiv :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVSDiv :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVSHL :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVLSHR :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVASHR :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVXor :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVAnd :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVOr :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun 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 :: forall e rtp v qv fun fv lv. GetType e => forall bw. (~) Type rtp (BitVecType bw) => BVUnOp -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVNot :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> Expression v qv fun fv lv e rtp

pattern BVNeg :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> Expression v qv fun 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 :: forall e rtp v qv fun fv lv. GetType e => forall n1 n2. (~) Type rtp (BitVecType ((+) n1 n2)) => e (BitVecType n1) -> e (BitVecType n2) -> Expression v qv fun fv lv e rtp

pattern Extract :: forall e rtp v qv fun fv lv. GetType e => forall len start bw. (~) Type rtp (BitVecType len) => BitWidth start -> BitWidth len -> e (BitVecType bw) -> Expression v qv fun 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) => BitWidth start -> BitWidth len -> a -> m (e (BitVecType len))

extractChecked :: forall m e a bw start len. (Embed m e, HasMonad a, MatchMonad a m, KnownNat start, KnownNat len, MonadResult a ~ e (BitVecType bw)) => BitWidth start -> BitWidth len -> a -> m (e (BitVecType len))

extractUntypedStart :: forall m e a bw len. (Embed m e, HasMonad a, MatchMonad a m, KnownNat len, MonadResult a ~ e (BitVecType bw)) => Integer -> BitWidth len -> a -> m (e (BitVecType len))

extractUntyped :: forall m e a bw b. (Embed m e, Monad m, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => Integer -> Integer -> a -> (forall len. e (BitVecType len) -> m b) -> m b

Arrays

pattern Select :: forall e rtp v qv fun fv lv. GetType e => forall val idx. (~) Type rtp val => e (ArrayType idx val) -> List Type e idx -> Expression v qv fun fv lv e rtp

pattern Store :: forall e rtp v qv fun fv lv. GetType e => forall idx val. (~) Type rtp (ArrayType idx val) => e (ArrayType idx val) -> List Type e idx -> e val -> Expression v qv fun fv lv e rtp

pattern ConstArray :: forall e rtp v qv fun fv lv. GetType e => forall idx val. (~) Type rtp (ArrayType idx val) => List Type Repr idx -> e val -> Expression v qv fun 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)

Access an array element. The following law holds:

   select (store arr i e) i .==. e

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)

A specialized version of select when the index is just a single element.

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

Write an element into an array and return the resulting array. The following laws hold (forall i/=j):

   select (store arr i e) i .==. e
   select (store arr i e) j .==. select arr j

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

A specialized version of store when the index is just a single element.

constArray :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => List Repr idx -> a -> m (e (ArrayType idx tp))

Create an array where every element is the same. The following holds:

   select (constArray tp e) i .==. e

Datatypes

pattern Mk :: forall t t1 t2 t3 t4 t5 t6. () => forall arg dt par sig. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type (Instantiated sig par) (DataType ([Type] -> (Type -> *) -> *) dt par)), IsDatatype dt, (~) Nat (Length Type par) (Parameters dt)) => Datatype dt -> List Type Repr par -> Constr dt sig -> List Type t6 arg -> Expression t5 t4 t3 t2 t1 t6 t

mk :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e (Instantiated sig par), IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Constr dt sig -> a -> m (e (DataType dt par))

pattern Is :: forall e rtp v qv fun fv lv. GetType e => forall dt sig par. (~) Type rtp BoolType => Constr dt sig -> e (DataType ([Type] -> (Type -> *) -> *) dt par) -> Expression v qv fun fv lv e rtp

is :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (DataType dt par), IsDatatype dt) => a -> Constr dt sig -> m (e BoolType)

(.#.) :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (DataType dt par), IsDatatype dt) => a -> Field dt tp -> m (e (CType tp par))

Misc

pattern Divisible :: forall rtp e v qv fun fv lv. () => (~) Type rtp BoolType => Integer -> e IntType -> Expression v qv fun fv lv e rtp

divisible :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => Integer -> a -> m (e BoolType)

Lists

(.:.) :: (HasMonad a, MonadResult a ~ e tp, MatchMonad a m, Applicative m) => a -> m (List e tps) -> m (List e (tp ': tps)) infixr 5

Create a typed list by appending an element to the front of another list.

nil :: Applicative m => m (List e '[])

Create an empty list.