Language.SMTLib2.Internals.Expression

Documentation

type family AllEq tp n :: [Type]

Equations

AllEq tp Z = `[]`

AllEq tp (S n) = tp : AllEq tp n

allEqToList :: Natural n -> List a (AllEq tp n) -> [a tp]

allEqFromList :: [a tp] -> (forall n. Natural n -> List a (AllEq tp n) -> r) -> r

allEqOf :: Repr tp -> Natural n -> List Repr (AllEq tp n)

mapAllEq :: Monad m => (e1 tp -> m (e2 tp)) -> Natural n -> List e1 (AllEq tp n) -> m (List e2 (AllEq tp n))

data Function fun con field sig where

Constructors

Fun :: fun `(arg, res)` -> Function fun con field `(arg, res)`

Eq :: Repr tp -> Natural n -> Function fun con field `(AllEq tp n, BoolType)`

Distinct :: Repr tp -> Natural n -> Function fun con field `(AllEq tp n, BoolType)`

Map :: List Repr idx -> Function fun con field `(arg, res)` -> Function fun con field `(Lifted arg idx, ArrayType idx res)`

Ord :: NumRepr tp -> OrdOp -> Function fun con field `(`[tp, tp]`, BoolType)`

Arith :: NumRepr tp -> ArithOp -> Natural n -> Function fun con field `(AllEq tp n, tp)`

ArithIntBin :: ArithOpInt -> Function fun con field `(`[IntType, IntType]`, IntType)`

Divide :: Function fun con field `(`[RealType, RealType]`, RealType)`

Abs :: NumRepr tp -> Function fun con field `(`[tp]`, tp)`

Not :: Function fun con field `(`[BoolType]`, BoolType)`

Logic :: LogicOp -> Natural n -> Function fun con field `(AllEq BoolType n, BoolType)`

ToReal :: Function fun con field `(`[IntType]`, RealType)`

ToInt :: Function fun con field `(`[RealType]`, IntType)`

ITE :: Repr a -> Function fun con field `(`[BoolType, a, a]`, a)`

BVComp :: BVCompOp -> Natural a -> Function fun con field `(`[BitVecType a, BitVecType a]`, BoolType)`

BVBin :: BVBinOp -> Natural a -> Function fun con field `(`[BitVecType a, BitVecType a]`, BitVecType a)`

BVUn :: BVUnOp -> Natural a -> Function fun con field `(`[BitVecType a]`, BitVecType a)`

Select :: List Repr idx -> Repr val -> Function fun con field `(ArrayType idx val : idx, val)`

Store :: List Repr idx -> Repr val -> Function fun con field `(ArrayType idx val : (val : idx), ArrayType idx val)`

ConstArray :: List Repr idx -> Repr val -> Function fun con field `(`[val]`, ArrayType idx val)`

Concat :: Natural n1 -> Natural n2 -> Function fun con field `(`[BitVecType n1, BitVecType n2]`, BitVecType (n1 + n2))`

Extract :: (((start + len) <= bw) ~ True) => Natural bw -> Natural start -> Natural len -> Function fun con field `(`[BitVecType bw]`, BitVecType len)`

Constructor :: IsDatatype a => con `(arg, a)` -> Function fun con field `(arg, DataType a)`

Test :: IsDatatype a => con `(arg, a)` -> Function fun con field `(`[DataType a]`, BoolType)`

Field :: IsDatatype a => field `(a, t)` -> Function fun con field `(`[DataType a]`, t)`

Divisible :: Integer -> Function fun con field `(`[IntType]`, BoolType)`

Instances

(GCompare ((,) [Type] Type) fun, GCompare ((,) [Type] *) con, GCompare ((,) * Type) field) => GCompare ((,) [Type] Type) (Function fun con field)

(GEq ((,) [Type] Type) fun, GEq ((,) [Type] *) con, GEq ((,) * Type) field) => GEq ((,) [Type] Type) (Function fun con field)

(GShow ((,) [Type] Type) fun, GShow ((,) [Type] *) con, GShow ((,) * Type) field) => GShow ((,) [Type] Type) (Function fun con field)

(GetFunType fun, GetConType con, GetFieldType field) => GetFunType (Function fun con field)

(GEq ((,) [Type] Type) fun, GEq ((,) [Type] *) con, GEq ((,) * Type) field) => Eq (Function fun con field sig)

(GShow ((,) [Type] Type) fun, GShow ((,) [Type] *) con, GShow ((,) * Type) field) => Show (Function fun con field sig)

data AnyFunction fun con field where

Constructors

AnyFunction :: Function fun con field `(arg, t)` -> AnyFunction fun con field

data OrdOp

Constructors

Ge

Gt

Le

Lt

Instances

Eq OrdOp

Ord OrdOp

Show OrdOp

data ArithOp

Constructors

Plus

Mult

Minus

Instances

Eq ArithOp

Ord ArithOp

Show ArithOp

data ArithOpInt

Constructors

Div

Mod

Rem

Instances

Eq ArithOpInt

Ord ArithOpInt

Show ArithOpInt

data LogicOp

Constructors

And

Or

XOr

Implies

Instances

Eq LogicOp

Ord LogicOp

Show LogicOp

data BVCompOp

Constructors

BVULE

BVULT

BVUGE

BVUGT

BVSLE

BVSLT

BVSGE

BVSGT

Instances

Eq BVCompOp

Ord BVCompOp

Show BVCompOp

data BVBinOp

Constructors

BVAdd

BVSub

BVMul

BVURem

BVSRem

BVUDiv

BVSDiv

BVSHL

BVLSHR

BVASHR

BVXor

BVAnd

BVOr

Instances

Eq BVBinOp

Ord BVBinOp

Show BVBinOp

data BVUnOp

Constructors

BVNot

BVNeg

Instances

Eq BVUnOp

Ord BVUnOp

Show BVUnOp

data LetBinding v e t

Constructors

LetBinding

Fields

letVar :: v t

letExpr :: e t

Instances

(GCompare Type v, GCompare Type e) => GCompare Type (LetBinding v e)

(GEq Type v, GEq Type e) => GEq Type (LetBinding v e)

data Quantifier

Constructors

Forall

Exists

Instances

Eq Quantifier

Ord Quantifier

Show Quantifier

data Expression v qv fun con field fv lv e res where

Constructors

Var :: v res -> Expression v qv fun con field fv lv e res

QVar :: qv res -> Expression v qv fun con field fv lv e res

FVar :: fv res -> Expression v qv fun con field fv lv e res

LVar :: lv res -> Expression v qv fun con field fv lv e res

App :: Function fun con field `(arg, res)` -> List e arg -> Expression v qv fun con field fv lv e res

Const :: Value con a -> Expression v qv fun con field fv lv e a

AsArray :: Function fun con field `(arg, res)` -> Expression v qv fun con field fv lv e (ArrayType arg res)

Quantification :: Quantifier -> List qv arg -> e BoolType -> Expression v qv fun con field fv lv e BoolType

Let :: List (LetBinding lv e) arg -> e res -> Expression v qv fun con field fv lv e res

Instances

(GCompare Type v, GCompare Type qv, GCompare ((,) [Type] Type) fun, GCompare ((,) [Type] *) con, GCompare ((,) * Type) field, GCompare Type fv, GCompare Type lv, GCompare Type e) => GCompare Type (Expression v qv fun con field fv lv e)

(GEq Type v, GEq Type qv, GEq ((,) [Type] Type) fun, GEq ((,) [Type] *) con, GEq ((,) * Type) field, GEq Type fv, GEq Type lv, GEq Type e) => GEq Type (Expression v qv fun con field fv lv e)

(GShow Type v, GShow Type qv, GShow ((,) [Type] Type) fun, GShow ((,) [Type] *) con, GShow ((,) * Type) field, GShow Type fv, GShow Type lv, GShow Type e) => GShow Type (Expression v qv fun con field fv lv e)

(GetType v, GetType qv, GetFunType fun, GetConType con, GetFieldType field, GetType fv, GetType lv, GetType e) => GetType (Expression v qv fun con field fv lv e)

(GEq Type v, GEq Type qv, GEq ((,) [Type] Type) fun, GEq ((,) [Type] *) con, GEq ((,) * Type) field, GEq Type fv, GEq Type lv, GEq Type e) => Eq (Expression v qv fun con field fv lv e t)

(GCompare Type v, GCompare Type qv, GCompare ((,) [Type] Type) fun, GCompare ((,) [Type] *) con, GCompare ((,) * Type) field, GCompare Type fv, GCompare Type lv, GCompare Type e) => Ord (Expression v qv fun con field fv lv e t)

(GShow Type v, GShow Type qv, GShow ((,) [Type] Type) fun, GShow ((,) [Type] *) con, GShow ((,) * Type) field, GShow Type fv, GShow Type lv, GShow Type e) => Show (Expression v qv fun con field fv lv e r)

class SMTOrd t where

Methods

lt :: Function fun con field `(`[t, t]`, BoolType)`

le :: Function fun con field `(`[t, t]`, BoolType)`

gt :: Function fun con field `(`[t, t]`, BoolType)`

ge :: Function fun con field `(`[t, t]`, BoolType)`

Instances

SMTOrd IntType

SMTOrd RealType

class SMTArith t where

Methods

arithFromInteger :: Integer -> ConcreteValue t

arith :: ArithOp -> Natural n -> Function fun con field `(AllEq t n, t)`

plus :: Natural n -> Function fun con field `(AllEq t n, t)`

minus :: Natural n -> Function fun con field `(AllEq t n, t)`

mult :: Natural n -> Function fun con field `(AllEq t n, t)`

abs' :: Function fun con field `(`[t]`, t)`

Instances

SMTArith IntType

SMTArith RealType

functionType :: Monad m => (forall arg t. fun `(arg, t)` -> m (List Repr arg, Repr t)) -> (forall arg dt. IsDatatype dt => con `(arg, dt)` -> m (List Repr arg, Datatype `(DatatypeSig dt, dt)`)) -> (forall dt t. IsDatatype dt => field `(dt, t)` -> m (Datatype `(DatatypeSig dt, dt)`, Repr t)) -> Function fun con field `(arg, res)` -> m (List Repr arg, Repr res)

expressionType :: (Monad m, Functor m) => (forall t. v t -> m (Repr t)) -> (forall t. qv t -> m (Repr t)) -> (forall arg t. fun `(arg, t)` -> m (List Repr arg, Repr t)) -> (forall arg dt. IsDatatype dt => con `(arg, dt)` -> m (List Repr arg, Datatype `(DatatypeSig dt, dt)`)) -> (forall dt t. IsDatatype dt => field `(dt, t)` -> m (Datatype `(DatatypeSig dt, dt)`, Repr t)) -> (forall t. fv t -> m (Repr t)) -> (forall t. lv t -> m (Repr t)) -> (forall t. e t -> m (Repr t)) -> Expression v qv fun con field fv lv e res -> m (Repr res)

mapExpr

Arguments

:: (Functor m, Monad m, Typeable con2)

=> (forall t. v1 t -> m (v2 t))

How to translate variables

-> (forall t. qv1 t -> m (qv2 t))

How to translate quantified variables

-> (forall arg t. fun1 `(arg, t)` -> m (fun2 `(arg, t)`))

How to translate functions

-> (forall arg t. con1 `(arg, t)` -> m (con2 `(arg, t)`))

How to translate constructrs

-> (forall t res. field1 `(t, res)` -> m (field2 `(t, res)`))

How to translate field accessors

-> (forall t. fv1 t -> m (fv2 t))

How to translate function variables

-> (forall t. lv1 t -> m (lv2 t))

How to translate let variables

-> (forall t. e1 t -> m (e2 t))

How to translate sub-expressions

-> Expression v1 qv1 fun1 con1 field1 fv1 lv1 e1 r

The expression to translate

-> m (Expression v2 qv2 fun2 con2 field2 fv2 lv2 e2 r)

mapFunction :: (Functor m, Monad m) => (forall arg t. fun1 `(arg, t)` -> m (fun2 `(arg, t)`)) -> (forall arg t. con1 `(arg, t)` -> m (con2 `(arg, t)`)) -> (forall t res. field1 `(t, res)` -> m (field2 `(t, res)`)) -> Function fun1 con1 field1 `(arg, res)` -> m (Function fun2 con2 field2 `(arg, res)`)

data RenderMode

Constructors

SMTRendering

Instances

Eq RenderMode

Ord RenderMode

Show RenderMode

renderExprDefault :: (GetType qv, GShow v, GShow qv, GShow fun, GShow con, GShow field, GShow fv, GShow lv, GShow e) => RenderMode -> Expression v qv fun con field fv lv e tp -> ShowS

renderExpr :: GetType qv => RenderMode -> (forall tp. v tp -> ShowS) -> (forall tp. qv tp -> ShowS) -> (forall arg res. fun `(arg, res)` -> ShowS) -> (forall arg dt. con `(arg, dt)` -> ShowS) -> (forall dt res. field `(dt, res)` -> ShowS) -> (forall tp. fv tp -> ShowS) -> (forall tp. lv tp -> ShowS) -> (forall tp. e tp -> ShowS) -> Expression v qv fun con field fv lv e tp -> ShowS

renderValue :: RenderMode -> (forall arg dt. con `(arg, dt)` -> ShowS) -> Value con tp -> ShowS

renderFunction :: RenderMode -> (forall arg res. fun `(arg, res)` -> ShowS) -> (forall arg dt. con `(arg, dt)` -> ShowS) -> (forall dt res. field `(dt, res)` -> ShowS) -> Function fun con field `(arg, res)` -> ShowS

renderType :: RenderMode -> Repr tp -> ShowS

data NoVar t

Constructors

NoVar'

Instances

GetType NoVar

GCompare Type NoVar

GEq Type NoVar

GShow Type NoVar

Eq (NoVar t)

Ord (NoVar t)

Show (NoVar t)

data NoFun sig

Constructors

NoFun'

Instances

GetFunType NoFun

Eq (NoFun t)

Ord (NoFun t)

Show (NoFun t)

GCompare ((,) [Type] Type) NoFun

GEq ((,) [Type] Type) NoFun

GShow ((,) [Type] Type) NoFun

data NoCon sig

Constructors

NoCon'

Instances

GetConType NoCon

Eq (NoCon t)

Ord (NoCon t)

Show (NoCon t)

GCompare ((,) [Type] *) NoCon

GEq ((,) [Type] *) NoCon

GShow ((,) [Type] *) NoCon

data NoField sig

Constructors

NoField'

Instances

GetFieldType NoField

Eq (NoField t)

Ord (NoField t)

Show (NoField t)

GCompare ((,) * Type) NoField

GEq ((,) * Type) NoField

GShow ((,) * Type) NoField