Data.Expression.Sort

Documentation

data Sort

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

• index :: Sort
• element :: Sort

Instances

Eq Sort

Methods

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

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

Show Sort

Methods

showsPrec :: Int -> Sort -> ShowS

show :: Sort -> String

showList :: [Sort] -> ShowS

SDecide Sort

Methods

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

SingKind Sort

Associated Types

type DemoteRep Sort :: *

Methods

fromSing :: Sing Sort a -> DemoteRep Sort

toSing :: DemoteRep Sort -> SomeSing Sort

SingI Sort BooleanSort

Methods

sing :: Sing BooleanSort a

SingI Sort IntegralSort

Methods

sing :: Sing IntegralSort a

IFoldable Sort ArrayF

Methods

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

IFoldable Sort ArithmeticF

Methods

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

IFoldable Sort NegationF

Methods

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

IFoldable Sort DisjunctionF

Methods

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

IFoldable Sort ConjunctionF

Methods

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

IEq1 Sort ArrayF

Methods

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

IEq1 Sort ArithmeticF

Methods

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

IEq1 Sort NegationF

Methods

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

IEq1 Sort DisjunctionF

Methods

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

IEq1 Sort ConjunctionF

Methods

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

IFunctor Sort ArrayF

Methods

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

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

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'

IFunctor Sort NegationF

Methods

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

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

IFunctor Sort DisjunctionF

Methods

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

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

IFunctor Sort ConjunctionF

Methods

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

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

ITraversable Sort ArrayF

Methods

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

ITraversable Sort ArithmeticF

Methods

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

ITraversable Sort NegationF

Methods

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

ITraversable Sort DisjunctionF

Methods

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

ITraversable Sort ConjunctionF

Methods

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

IShow Sort Sort ArrayF

Methods

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

IShow Sort Sort ArithmeticF

Methods

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

IShow Sort Sort NegationF

Methods

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

IShow Sort Sort DisjunctionF

Methods

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

IShow Sort Sort ConjunctionF

Methods

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

IShow Sort k (EqualityF k)

Methods

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

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

Methods

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

IShow Sort Sort (ExistentialF v)

Methods

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

IShow Sort Sort (UniversalF v)

Methods

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

IFoldable Sort (EqualityF Sort)

Methods

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

IFoldable Sort (ExistentialF v)

Methods

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

IFoldable Sort (UniversalF v)

Methods

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

IFoldable Sort (VarF (Sort -> *))

Methods

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

IEq1 Sort (EqualityF Sort)

Methods

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

IEq1 Sort (ExistentialF v)

Methods

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

IEq1 Sort (UniversalF v)

Methods

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

IEq1 Sort (VarF (Sort -> *))

Methods

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

IFunctor Sort (EqualityF Sort)

Methods

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

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

IFunctor Sort (ExistentialF v)

Methods

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

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

IFunctor Sort (UniversalF v)

Methods

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

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

IFunctor Sort (VarF (Sort -> *))

Methods

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

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

ITraversable Sort (EqualityF Sort)

Methods

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

ITraversable Sort (ExistentialF v)

Methods

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

ITraversable Sort (UniversalF v)

Methods

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

ITraversable Sort (VarF (Sort -> *))

Methods

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

MaybeQuantified Sort (ExistentialF v)

Methods

isQuantified' :: MaybeQuantified (ExistentialF v) g => f (IFix (ExistentialF v) g) s -> Const (ExistentialF v) Any s

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

MaybeQuantified Sort (UniversalF v)

Methods

isQuantified' :: MaybeQuantified (UniversalF v) g => f (IFix (UniversalF v) g) s -> Const (UniversalF v) Any s

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

MaybeQuantified Sort (VarF (Sort -> *))

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)

Methods

sing :: Sing (ArraySort n0 n1) a

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

JoinSemiLattice (QFLogic BooleanSort)

Methods

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

join :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic 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

MeetSemiLattice (QFLogic BooleanSort)

Methods

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

meet :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

Lattice (ALia BooleanSort)

Lattice (QFALia BooleanSort)

Lattice (Lia BooleanSort)

Lattice (QFLia BooleanSort)

Lattice (QFLogic 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

BoundedJoinSemiLattice (QFLogic BooleanSort)

Methods

bottom :: QFLogic 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

BoundedMeetSemiLattice (QFLogic BooleanSort)

Methods

top :: QFLogic BooleanSort

BoundedLattice (ALia BooleanSort)

BoundedLattice (QFALia BooleanSort)

BoundedLattice (Lia BooleanSort)

BoundedLattice (QFLia BooleanSort)

BoundedLattice (QFLogic 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

ComplementedLattice (QFLogic BooleanSort)

Methods

complement :: QFLogic BooleanSort -> QFLogic BooleanSort

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

(:<:) Sort (EqualityF Sort) f => Parseable ((k -> *) -> Sort -> *) (EqualityF k) f

Methods

parser :: Proxy (EqualityF k) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

((:<:) Sort (ExistentialF v) f, SingI Sort v) => Parseable ((Sort -> *) -> Sort -> *) (ExistentialF v) f

Methods

parser :: Proxy (ExistentialF v) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

((:<:) Sort (UniversalF v) f, SingI Sort v) => Parseable ((Sort -> *) -> Sort -> *) (UniversalF v) f

Methods

parser :: Proxy (UniversalF v) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

(:<:) Sort (VarF (Sort -> *)) f => Parseable (k -> Sort -> *) (VarF k) f

Methods

parser :: Proxy (VarF k) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

data Sing Sort

data Sing Sort where

• SBooleanSort :: Sing Sort z
• SIntegralSort :: Sing Sort z
• SArraySort :: Sing Sort z

type DemoteRep Sort

type DemoteRep Sort = Sort

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

The singleton kind-indexed data family.

Instances

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z0
• STrue :: Sing Bool z0

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z0
• SEQ :: Sing Ordering z0
• SGT :: Sing Ordering z0

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

data Sing ()

data Sing () where

• STuple0 :: Sing () z0

data Sing Sort

data Sing Sort where

• SBooleanSort :: Sing Sort z
• SIntegralSort :: Sing Sort z
• SArraySort :: Sing Sort z

data Sing [a0]

data Sing [a0] where

• SNil :: Sing [a0] z0
• SCons :: Sing [a0] z0

data Sing (Maybe a0)

data Sing (Maybe a0) where

• SNothing :: Sing (Maybe a0) z0
• SJust :: Sing (Maybe a0) z0

data Sing (NonEmpty a0)

data Sing (NonEmpty a0) where

• (:%|) :: Sing (NonEmpty a0) z0

data Sing (Either a0 b0)

data Sing (Either a0 b0) where

• SLeft :: Sing (Either a0 b0) z0
• SRight :: Sing (Either a0 b0) z0

data Sing (a0, b0)

data Sing (a0, b0) where

• STuple2 :: Sing (a0, b0) z0

data Sing ((~>) k1 k2)

data Sing ((~>) k1 k2) = SLambda {

• applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t)

}

data Sing (a0, b0, c0)

data Sing (a0, b0, c0) where

• STuple3 :: Sing (a0, b0, c0) z0

data Sing (a0, b0, c0, d0)

data Sing (a0, b0, c0, d0) where

• STuple4 :: Sing (a0, b0, c0, d0) z0

data Sing (a0, b0, c0, d0, e0)

data Sing (a0, b0, c0, d0, e0) where

• STuple5 :: Sing (a0, b0, c0, d0, e0) z0

data Sing (a0, b0, c0, d0, e0, f0)

data Sing (a0, b0, c0, d0, e0, f0) where

• STuple6 :: Sing (a0, b0, c0, d0, e0, f0) z0

data Sing (a0, b0, c0, d0, e0, f0, g0)

data Sing (a0, b0, c0, d0, e0, f0, g0) where

• STuple7 :: Sing (a0, b0, c0, d0, e0, f0, g0) z0

data DynamicSort where

Some sort (obtained for example during parsing)

Constructors

DynamicSort :: forall s. Sing s -> DynamicSort

Instances

Eq DynamicSort

Methods

(==) :: DynamicSort -> DynamicSort -> Bool

(/=) :: DynamicSort -> DynamicSort -> Bool

data DynamicallySorted f where

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

Constructors

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

Instances

IEq1 Sort f => Eq (DynamicallySorted f)

Methods

(==) :: DynamicallySorted f -> DynamicallySorted f -> Bool

(/=) :: DynamicallySorted f -> DynamicallySorted f -> Bool

(IFunctor Sort f, IShow Sort Sort f) => Show (DynamicallySorted f)

Methods

showsPrec :: Int -> DynamicallySorted f -> ShowS

show :: DynamicallySorted f -> String

showList :: [DynamicallySorted f] -> ShowS

parseSort :: Parser DynamicSort

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

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

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

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

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