expressions-0.5: Expressions and Formulae a la carte

Copyright(C) 2017-18 Jakub Daniel
LicenseBSD-style (see the file LICENSE)
MaintainerJakub Daniel <jakub.daniel@protonmail.com>
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.Expression.Arithmetic

Description

 
Synopsis

Documentation

data ArithmeticF a (s :: Sort) where Source #

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 Source # 
Instance details

Defined in Data.Expression.Arithmetic

Methods

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

IFoldable ArithmeticF Source # 
Instance details

Defined in Data.Expression.Arithmetic

Methods

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

IFunctor ArithmeticF Source # 
Instance details

Defined in Data.Expression.Arithmetic

Methods

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

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

ITraversable ArithmeticF Source # 
Instance details

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

IShow ArithmeticF Source # 
Instance details

Defined in Data.Expression.Arithmetic

Methods

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

Heyting (ALia BooleanSort) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.Expression

Methods

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

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

Lattice (QFALia BooleanSort) Source # 
Instance details

Defined in Data.Expression

Methods

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

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

Lattice (Lia BooleanSort) Source # 
Instance details

Defined in Data.Expression

Methods

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

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

Lattice (QFLia BooleanSort) Source # 
Instance details

Defined in Data.Expression

Methods

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

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

BoundedJoinSemiLattice (ALia BooleanSort) Source # 
Instance details

Defined in Data.Expression

Methods

bottom :: ALia BooleanSort #

BoundedJoinSemiLattice (QFALia BooleanSort) Source # 
Instance details

Defined in Data.Expression

Methods

bottom :: QFALia BooleanSort #

BoundedJoinSemiLattice (Lia BooleanSort) Source # 
Instance details

Defined in Data.Expression

Methods

bottom :: Lia BooleanSort #

BoundedJoinSemiLattice (QFLia BooleanSort) Source # 
Instance details

Defined in Data.Expression

Methods

bottom :: QFLia BooleanSort #

BoundedMeetSemiLattice (ALia BooleanSort) Source # 
Instance details

Defined in Data.Expression

Methods

top :: ALia BooleanSort #

BoundedMeetSemiLattice (QFALia BooleanSort) Source # 
Instance details

Defined in Data.Expression

Methods

top :: QFALia BooleanSort #

BoundedMeetSemiLattice (Lia BooleanSort) Source # 
Instance details

Defined in Data.Expression

Methods

top :: Lia BooleanSort #

BoundedMeetSemiLattice (QFLia BooleanSort) Source # 
Instance details

Defined in Data.Expression

Methods

top :: QFLia BooleanSort #

ArithmeticF :<: f => Parseable ArithmeticF f Source # 
Instance details

Defined in Data.Expression.Arithmetic

Methods

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

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

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] Source #

Collects a list of all constants occurring in an expression.

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

A smart constructor for a variadic addition

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

A smart constructor for a variadic multiplication

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

A smart constructor for binary addition

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

A smart constructor for a binary multiplication

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

A smart constructor for a divisibility predicate

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

A smart constructor for <

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

A smart constructor for >

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

A smart constructor for <=

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

A smart constructor for >=