Data.Integer.Presburger.HOAS

Documentation

data Formula

Constructors

Formula :/\: Formula

Formula :\/: Formula

Formula :=>: Formula

Formula :<=>: Formula

Not Formula

Exists (Term -> Formula)

Forall (Term -> Formula)

TRUE

FALSE

Term :<: Term

Term :>: Term

Term :<=: Term

Term :>=: Term

Term :=: Term

Term :/=: Term

Integer :| Term

Instances

PP Formula

Quant Formula

check :: Formula -> Bool

translate :: Formula -> Form (Prop PosP)

class Quant t

Instances

Quant Formula

Quant t => Quant (Term -> t)

exists, forall :: Quant t => t -> Formula

data Term

Terms of Presburger arithmetic. Term are created by using the Num class. WARNING: Presburger arithmetic only supports multiplication by a constant, trying to create invalid terms will result in a run-time error. A more type-safe alternative is to use the '(.*)' operator.

Instances

Eq Term

Num Term

Show Term

PP Term

Quant t => Quant (Term -> t)

(.*) :: Integer -> Term -> Term

is_constant :: Term -> Maybe Integer

Check if a term is a constant (i.e., contains no variables). If so, then we return the constant, otherwise we return Nothing.

class PP a where

Methods

pp :: a -> Doc

Instances

PP Env

PP Term

PP Conn

PP Formula

SignPP p => PP (NormProp p)

SignPP p => PP (Prop p)

PP p => PP (Form p)