Data.Expression.Arithmetic

Documentation

data ArithmeticF a s 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

IFoldable Sort ArithmeticF

Methods

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

IEq1 Sort ArithmeticF

Methods

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

IFunctor Sort ArithmeticF

Methods

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

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

ITraversable Sort ArithmeticF

Methods

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

IShow Sort Sort ArithmeticF

Methods

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

JoinSemiLattice (ALia BooleanSort)

Methods

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

join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

JoinSemiLattice (QFALia BooleanSort)

Methods

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

join :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

JoinSemiLattice (Lia BooleanSort)

Methods

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

join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

JoinSemiLattice (QFLia BooleanSort)

Methods

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

join :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

MeetSemiLattice (ALia BooleanSort)

Methods

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

meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

MeetSemiLattice (QFALia BooleanSort)

Methods

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

meet :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

MeetSemiLattice (Lia BooleanSort)

Methods

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

meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

MeetSemiLattice (QFLia BooleanSort)

Methods

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

meet :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

Lattice (ALia BooleanSort)

Lattice (QFALia BooleanSort)

Lattice (Lia BooleanSort)

Lattice (QFLia BooleanSort)

BoundedJoinSemiLattice (ALia BooleanSort)

Methods

bottom :: ALia BooleanSort

BoundedJoinSemiLattice (QFALia BooleanSort)

Methods

bottom :: QFALia BooleanSort

BoundedJoinSemiLattice (Lia BooleanSort)

Methods

bottom :: Lia BooleanSort

BoundedJoinSemiLattice (QFLia BooleanSort)

Methods

bottom :: QFLia BooleanSort

BoundedMeetSemiLattice (ALia BooleanSort)

Methods

top :: ALia BooleanSort

BoundedMeetSemiLattice (QFALia BooleanSort)

Methods

top :: QFALia BooleanSort

BoundedMeetSemiLattice (Lia BooleanSort)

Methods

top :: Lia BooleanSort

BoundedMeetSemiLattice (QFLia BooleanSort)

Methods

top :: QFLia BooleanSort

BoundedLattice (ALia BooleanSort)

BoundedLattice (QFALia BooleanSort)

BoundedLattice (Lia BooleanSort)

BoundedLattice (QFLia BooleanSort)

ComplementedLattice (ALia BooleanSort)

Methods

complement :: ALia BooleanSort -> ALia BooleanSort

ComplementedLattice (QFALia BooleanSort)

Methods

complement :: QFALia BooleanSort -> QFALia BooleanSort

ComplementedLattice (Lia BooleanSort)

Methods

complement :: Lia BooleanSort -> Lia BooleanSort

ComplementedLattice (QFLia BooleanSort)

Methods

complement :: QFLia BooleanSort -> QFLia BooleanSort

(:<:) Sort ArithmeticF f => Parseable ((Sort -> *) -> Sort -> *) ArithmeticF f

Methods

parser :: Proxy ArithmeticF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

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

A smart constructor for integer constants

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