Data.Expression.Arithmetic

Documentation

data ArithmeticF a (s :: Sort) where

A functor representing linear integer arithmetic: constants (cnst), addition (add or .+.), multiplication (mul or .*.), divisibility predicate (.\.) and ordering (.<., .>., .<=., .>=.).

Constructors

Const :: Int -> ArithmeticF a IntegralSort

Add :: [a IntegralSort] -> ArithmeticF a IntegralSort

Mul :: [a IntegralSort] -> ArithmeticF a IntegralSort

Divides :: Int -> a IntegralSort -> ArithmeticF a BooleanSort

LessThan :: a IntegralSort -> a IntegralSort -> ArithmeticF a BooleanSort

Instances

IEq1 ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

ieq1 :: IEq a => ArithmeticF a j -> ArithmeticF a j -> Bool

IFoldable ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

ifold :: Monoid m => ArithmeticF (Const m) i' -> Const m i'

IFunctor ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ArithmeticF a i' -> ArithmeticF b i'

index :: ArithmeticF a i' -> Sing i'

ITraversable ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). ArithmeticF a i' -> f (ArithmeticF b i')

IShow ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

ishow :: ArithmeticF (Const String) i -> Const String i

Heyting (ALia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

neg :: ALia BooleanSort -> ALia BooleanSort

(<=>) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

Heyting (QFALia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

neg :: QFALia BooleanSort -> QFALia BooleanSort

(<=>) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

Heyting (Lia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

neg :: Lia BooleanSort -> Lia BooleanSort

(<=>) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

Heyting (QFLia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

neg :: QFLia BooleanSort -> QFLia BooleanSort

(<=>) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

Lattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

(/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

Lattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

(/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

Lattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

(/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

Lattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

(/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

BoundedJoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: ALia BooleanSort

BoundedJoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFALia BooleanSort

BoundedJoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

bottom :: Lia BooleanSort

BoundedJoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLia BooleanSort

BoundedMeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

top :: ALia BooleanSort

BoundedMeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

top :: QFALia BooleanSort

BoundedMeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

top :: Lia BooleanSort

BoundedMeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

top :: QFLia BooleanSort

ArithmeticF :<: f => Parseable ArithmeticF f

Defined in Data.Expression.Arithmetic

Methods

parser :: Proxy ArithmeticF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f)

cnst :: ArithmeticF :<: f => Int -> IFix f IntegralSort

A smart constructor for integer constants

cnsts :: forall f (s :: Sort). (ArithmeticF :<: f, IFoldable f, IFunctor f, IEq1 f) => IFix f s -> [IFix f IntegralSort]

Collects a list of all constants occurring in an expression.

add :: ArithmeticF :<: f => [IFix f IntegralSort] -> IFix f IntegralSort

A smart constructor for a variadic addition

mul :: ArithmeticF :<: f => [IFix f IntegralSort] -> IFix f IntegralSort

A smart constructor for a variadic multiplication

(.+.) :: forall f. ArithmeticF :<: f => IFix f IntegralSort -> IFix f IntegralSort -> IFix f IntegralSort infixl 8

A smart constructor for binary addition

(.*.) :: forall f. ArithmeticF :<: f => IFix f IntegralSort -> IFix f IntegralSort -> IFix f IntegralSort infixl 9

A smart constructor for a binary multiplication

(.\.) :: ArithmeticF :<: f => Int -> IFix f IntegralSort -> IFix f BooleanSort infix 7

A smart constructor for a divisibility predicate

(.<.) :: forall f. ArithmeticF :<: f => IFix f IntegralSort -> IFix f IntegralSort -> IFix f BooleanSort infix 7

A smart constructor for <

(.>.) :: forall f. ArithmeticF :<: f => IFix f IntegralSort -> IFix f IntegralSort -> IFix f BooleanSort infix 7

A smart constructor for >

(.<=.) :: forall f. ArithmeticF :<: f => IFix f IntegralSort -> IFix f IntegralSort -> IFix f BooleanSort infix 7

A smart constructor for <=

(.>=.) :: forall f. ArithmeticF :<: f => IFix f IntegralSort -> IFix f IntegralSort -> IFix f BooleanSort infix 7

A smart constructor for >=