expressions-0.1.1: Expressions and Formulas 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.Sort

Description

 

Synopsis

Documentation

data Sort Source #

A universe of recognized sorts

Constructors

BooleanSort

booleans (true, false)

IntegralSort

integers (..., -1, 0, 1, ...)

ArraySort

arrays indexed by index sort, containing elements of element sort

Fields

Instances

Eq Sort Source # 

Methods

(==) :: Sort -> Sort -> Bool #

(/=) :: Sort -> Sort -> Bool #

Show Sort Source # 

Methods

showsPrec :: Int -> Sort -> ShowS #

show :: Sort -> String #

showList :: [Sort] -> ShowS #

SDecide Sort Source # 

Methods

(%~) :: Sing Sort a -> Sing Sort b -> Decision ((Sort :~: a) b) #

SingKind Sort Source # 

Associated Types

type DemoteRep Sort :: * #

SingI Sort BooleanSort Source # 

Methods

sing :: Sing BooleanSort a #

SingI Sort IntegralSort Source # 

Methods

sing :: Sing IntegralSort a #

IFoldable Sort ArrayF Source # 

Methods

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

IFoldable Sort ArithmeticF Source # 

Methods

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

IFoldable Sort NegationF Source # 

Methods

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

IFoldable Sort DisjunctionF Source # 

Methods

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

IFoldable Sort ConjunctionF Source # 

Methods

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

IEq1 Sort ArrayF Source # 

Methods

ieq1 :: IEq ArrayF a => f a j -> f a j -> Bool Source #

IEq1 Sort ArithmeticF Source # 

Methods

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

IEq1 Sort NegationF Source # 

Methods

ieq1 :: IEq NegationF a => f a j -> f a j -> Bool Source #

IEq1 Sort DisjunctionF Source # 

Methods

ieq1 :: IEq DisjunctionF a => f a j -> f a j -> Bool Source #

IEq1 Sort ConjunctionF Source # 

Methods

ieq1 :: IEq ConjunctionF a => f a j -> f a j -> Bool Source #

IFunctor Sort ArrayF Source # 

Methods

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

index :: f a i' -> Sing ArrayF i' Source #

IFunctor Sort ArithmeticF Source # 

Methods

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

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

IFunctor Sort NegationF Source # 

Methods

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

index :: f a i' -> Sing NegationF i' Source #

IFunctor Sort DisjunctionF Source # 

Methods

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

index :: f a i' -> Sing DisjunctionF i' Source #

IFunctor Sort ConjunctionF Source # 

Methods

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

index :: f a i' -> Sing ConjunctionF i' Source #

ITraversable Sort ArrayF Source # 

Methods

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

ITraversable Sort ArithmeticF Source # 

Methods

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

ITraversable Sort NegationF Source # 

Methods

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

ITraversable Sort DisjunctionF Source # 

Methods

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

ITraversable Sort ConjunctionF Source # 

Methods

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

IShow Sort Sort ArrayF Source # 

Methods

ishow :: f (Const k String) i -> Const ArrayF String i Source #

IShow Sort Sort ArithmeticF Source # 

Methods

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

IShow Sort Sort NegationF Source # 

Methods

ishow :: f (Const k String) i -> Const NegationF String i Source #

IShow Sort Sort DisjunctionF Source # 
IShow Sort Sort ConjunctionF Source # 
IShow Sort k (EqualityF k) Source # 

Methods

ishow :: f (Const k String) i -> Const (EqualityF k) String i Source #

IShow Sort k (VarF (k -> *)) Source # 

Methods

ishow :: f (Const k String) i -> Const (VarF (k -> *)) String i Source #

IShow Sort Sort (ExistentialF v) Source # 

Methods

ishow :: f (Const k String) i -> Const (ExistentialF v) String i Source #

IShow Sort Sort (UniversalF v) Source # 

Methods

ishow :: f (Const k String) i -> Const (UniversalF v) String i Source #

IFoldable Sort (EqualityF Sort) Source # 

Methods

ifold :: Monoid m => f (Const (EqualityF Sort) m) i' -> Const (EqualityF Sort) m i' Source #

IFoldable Sort (ExistentialF v) Source # 

Methods

ifold :: Monoid m => f (Const (ExistentialF v) m) i' -> Const (ExistentialF v) m i' Source #

IFoldable Sort (UniversalF v) Source # 

Methods

ifold :: Monoid m => f (Const (UniversalF v) m) i' -> Const (UniversalF v) m i' Source #

IFoldable Sort (VarF (Sort -> *)) Source # 

Methods

ifold :: Monoid m => f (Const (VarF (Sort -> *)) m) i' -> Const (VarF (Sort -> *)) m i' Source #

IEq1 Sort (EqualityF Sort) Source # 

Methods

ieq1 :: IEq (EqualityF Sort) a => f a j -> f a j -> Bool Source #

IEq1 Sort (ExistentialF v) Source # 

Methods

ieq1 :: IEq (ExistentialF v) a => f a j -> f a j -> Bool Source #

IEq1 Sort (UniversalF v) Source # 

Methods

ieq1 :: IEq (UniversalF v) a => f a j -> f a j -> Bool Source #

IEq1 Sort (VarF (Sort -> *)) Source # 

Methods

ieq1 :: IEq (VarF (Sort -> *)) a => f a j -> f a j -> Bool Source #

IFunctor Sort (EqualityF Sort) Source # 

Methods

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

index :: f a i' -> Sing (EqualityF Sort) i' Source #

IFunctor Sort (ExistentialF v) Source # 

Methods

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

index :: f a i' -> Sing (ExistentialF v) i' Source #

IFunctor Sort (UniversalF v) Source # 

Methods

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

index :: f a i' -> Sing (UniversalF v) i' Source #

IFunctor Sort (VarF (Sort -> *)) Source # 

Methods

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

index :: f a i' -> Sing (VarF (Sort -> *)) i' Source #

ITraversable Sort (EqualityF Sort) Source # 

Methods

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

ITraversable Sort (ExistentialF v) Source # 

Methods

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

ITraversable Sort (UniversalF v) Source # 

Methods

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

ITraversable Sort (VarF (Sort -> *)) Source # 

Methods

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

MaybeQuantified Sort (ExistentialF v) Source # 
MaybeQuantified Sort (UniversalF v) Source # 
MaybeQuantified Sort (VarF (Sort -> *)) Source # 

Methods

isQuantified' :: MaybeQuantified (VarF (Sort -> *)) g => f (IFix (VarF (Sort -> *)) g) s -> Const (VarF (Sort -> *)) Any s

freevars' :: f (Const (VarF (Sort -> *)) [DynamicallySorted (VarF (Sort -> *))]) s -> Const (VarF (Sort -> *)) [DynamicallySorted (VarF (Sort -> *))] s

(SingI Sort n0, SingI Sort n1) => SingI Sort (ArraySort n0 n1) Source # 

Methods

sing :: Sing (ArraySort n0 n1) a #

JoinSemiLattice (ALia BooleanSort) # 
JoinSemiLattice (QFALia BooleanSort) # 
JoinSemiLattice (Lia BooleanSort) # 
JoinSemiLattice (QFLia BooleanSort) # 
JoinSemiLattice (QFLogic BooleanSort) # 
MeetSemiLattice (ALia BooleanSort) # 
MeetSemiLattice (QFALia BooleanSort) # 
MeetSemiLattice (Lia BooleanSort) # 
MeetSemiLattice (QFLia BooleanSort) # 
MeetSemiLattice (QFLogic BooleanSort) # 
Lattice (ALia BooleanSort) # 
Lattice (QFALia BooleanSort) # 
Lattice (Lia BooleanSort) # 
Lattice (QFLia BooleanSort) # 
Lattice (QFLogic BooleanSort) # 
BoundedJoinSemiLattice (ALia BooleanSort) # 
BoundedJoinSemiLattice (QFALia BooleanSort) # 
BoundedJoinSemiLattice (Lia BooleanSort) # 
BoundedJoinSemiLattice (QFLia BooleanSort) # 
BoundedJoinSemiLattice (QFLogic BooleanSort) # 
BoundedMeetSemiLattice (ALia BooleanSort) # 

Methods

top :: ALia BooleanSort #

BoundedMeetSemiLattice (QFALia BooleanSort) # 
BoundedMeetSemiLattice (Lia BooleanSort) # 

Methods

top :: Lia BooleanSort #

BoundedMeetSemiLattice (QFLia BooleanSort) # 
BoundedMeetSemiLattice (QFLogic BooleanSort) # 
BoundedLattice (ALia BooleanSort) # 
BoundedLattice (QFALia BooleanSort) # 
BoundedLattice (Lia BooleanSort) # 
BoundedLattice (QFLia BooleanSort) # 
BoundedLattice (QFLogic BooleanSort) # 
ComplementedLattice (ALia BooleanSort) Source # 
ComplementedLattice (QFALia BooleanSort) Source # 
ComplementedLattice (Lia BooleanSort) Source # 
ComplementedLattice (QFLia BooleanSort) Source # 
ComplementedLattice (QFLogic BooleanSort) Source # 
(:<:) Sort ArrayF f => Parseable ((Sort -> *) -> Sort -> *) ArrayF f Source # 
(:<:) Sort ArithmeticF f => Parseable ((Sort -> *) -> Sort -> *) ArithmeticF f Source # 
(:<:) Sort NegationF f => Parseable ((Sort -> *) -> Sort -> *) NegationF f Source # 
(:<:) Sort DisjunctionF f => Parseable ((Sort -> *) -> Sort -> *) DisjunctionF f Source # 
(:<:) Sort ConjunctionF f => Parseable ((Sort -> *) -> Sort -> *) ConjunctionF f Source # 
(:<:) Sort (EqualityF Sort) f => Parseable ((k -> *) -> Sort -> *) (EqualityF k) f Source # 
((:<:) Sort (ExistentialF v) f, SingI Sort v) => Parseable ((Sort -> *) -> Sort -> *) (ExistentialF v) f Source # 
((:<:) Sort (UniversalF v) f, SingI Sort v) => Parseable ((Sort -> *) -> Sort -> *) (UniversalF v) f Source # 
(:<:) Sort (VarF (Sort -> *)) f => Parseable (k -> Sort -> *) (VarF k) f Source # 
data Sing Sort Source # 
type DemoteRep Sort Source # 

data family Sing k (a :: k) :: * #

The singleton kind-indexed data family.

Instances

data Sing Bool 
data Sing Bool where
data Sing Ordering 
data Sing Nat 
data Sing Nat where
data Sing Symbol 
data Sing Symbol where
data Sing () 
data Sing () where
data Sing Sort # 
data Sing [a0] 
data Sing [a0] where
data Sing (Maybe a0) 
data Sing (Maybe a0) where
data Sing (NonEmpty a0) 
data Sing (NonEmpty a0) where
data Sing (Either a0 b0) 
data Sing (Either a0 b0) where
data Sing (a0, b0) 
data Sing (a0, b0) where
data Sing ((~>) k1 k2) 
data Sing ((~>) k1 k2) = SLambda {}
data Sing (a0, b0, c0) 
data Sing (a0, b0, c0) where
data Sing (a0, b0, c0, d0) 
data Sing (a0, b0, c0, d0) where
data Sing (a0, b0, c0, d0, e0) 
data Sing (a0, b0, c0, d0, e0) where
data Sing (a0, b0, c0, d0, e0, f0) 
data Sing (a0, b0, c0, d0, e0, f0) where
data Sing (a0, b0, c0, d0, e0, f0, g0) 
data Sing (a0, b0, c0, d0, e0, f0, g0) where

data DynamicSort where Source #

Some sort (obtained for example during parsing)

Constructors

DynamicSort :: forall s. Sing s -> DynamicSort 

data DynamicallySorted f where Source #

An expression of some sort (obtained for example during parsing)

Constructors

DynamicallySorted :: forall s f. Sing s -> IFix f s -> DynamicallySorted f 

parseSort :: Parser DynamicSort Source #

Parser that accepts sort definitions such as bool, int, array int int, array int (array ...).

toStaticSort :: forall s. SingI s => DynamicSort -> Maybe (Sing s) Source #

Tries to convert some sort (DynamicSort) to a requested sort.

toStaticallySorted :: forall f s. SingI s => DynamicallySorted f -> Maybe (IFix f s) Source #

Tries to convert an expression (DynamicallySorted) of some sort to an expression of requested sort. Performs no conversions.