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 Demote Sort = (r :: *)

Methods

fromSing :: Sing Sort a -> Demote Sort

toSing :: Demote Sort -> SomeSing Sort

SingI Sort BooleanSort

Methods

sing :: Sing BooleanSort a

SingI Sort IntegralSort

Methods

sing :: Sing IntegralSort a

IEq1 Sort IfThenElseF

Methods

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

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

IFoldable Sort IfThenElseF

Methods

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

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'

IFunctor Sort IfThenElseF

Methods

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

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

IFunctor Sort ArrayF

Methods

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

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

IFunctor Sort ArithmeticF

Methods

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

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

IFunctor Sort NegationF

Methods

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

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

IFunctor Sort DisjunctionF

Methods

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

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

IFunctor Sort ConjunctionF

Methods

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

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

ITraversable Sort IfThenElseF

Methods

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

ITraversable Sort ArrayF

Methods

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

ITraversable Sort ArithmeticF

Methods

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

ITraversable Sort NegationF

Methods

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

ITraversable Sort DisjunctionF

Methods

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

ITraversable Sort ConjunctionF

Methods

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

IShow Sort Sort IfThenElseF

Methods

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

IShow Sort Sort ArrayF

Methods

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

IShow Sort Sort ArithmeticF

Methods

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

IShow Sort Sort NegationF

Methods

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

IShow Sort Sort DisjunctionF

Methods

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

IShow Sort Sort ConjunctionF

Methods

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

IShow k Sort (EqualityF k)

Methods

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

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

Methods

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

IShow Sort Sort (ExistentialF v)

Methods

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

IShow Sort Sort (UniversalF v)

Methods

ishow :: f (Const (UniversalF v) String) i -> Const k String 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

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'

IFunctor Sort (EqualityF Sort)

Methods

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

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

IFunctor Sort (ExistentialF v)

Methods

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

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

IFunctor Sort (UniversalF v)

Methods

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

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

IFunctor Sort (VarF (Sort -> *))

Methods

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

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

ITraversable Sort (EqualityF Sort)

Methods

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

ITraversable Sort (ExistentialF v)

Methods

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

ITraversable Sort (UniversalF v)

Methods

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

ITraversable Sort (VarF (Sort -> *))

Methods

itraverse :: Applicative f => (forall (i' :: VarF (Sort -> *)). a i' -> f (b i')) -> forall (i' :: VarF (Sort -> *)). 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 n1, SingI Sort n2) => SingI Sort (ArraySort n1 n2)

Methods

sing :: Sing (ArraySort n1 n2) 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 IfThenElseF f => Parseable ((Sort -> *) -> Sort -> *) IfThenElseF f

Methods

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

(:<:) 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 Demote Sort

type Demote 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 z
• STrue :: Sing Bool z

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z
• SEQ :: Sing Ordering z
• SGT :: Sing Ordering z

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 () z

data Sing Sort

data Sing Sort where

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

data Sing [a]

data Sing [a] where

• SNil :: Sing [a] z
• SCons :: Sing [a] z

data Sing (Maybe a)

data Sing (Maybe a) where

• SNothing :: Sing (Maybe a) z
• SJust :: Sing (Maybe a) z

data Sing (NonEmpty a)

data Sing (NonEmpty a) where

• (:%|) :: Sing (NonEmpty a) z

data Sing (Either a b)

data Sing (Either a b) where

• SLeft :: Sing (Either a b) z
• SRight :: Sing (Either a b) z

data Sing (a, b)

data Sing (a, b) where

• STuple2 :: Sing (a, b) z

data Sing ((~>) k1 k2)

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

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

}

data Sing (a, b, c)

data Sing (a, b, c) where

• STuple3 :: Sing (a, b, c) z

data Sing (a, b, c, d)

data Sing (a, b, c, d) where

• STuple4 :: Sing (a, b, c, d) z

data Sing (a, b, c, d, e)

data Sing (a, b, c, d, e) where

• STuple5 :: Sing (a, b, c, d, e) z

data Sing (a, b, c, d, e, f)

data Sing (a, b, c, d, e, f) where

• STuple6 :: Sing (a, b, c, d, e, f) z

data Sing (a, b, c, d, e, f, g)

data Sing (a, b, c, d, e, f, g) where

• STuple7 :: Sing (a, b, c, d, e, f, g) z

data DynamicSort where

Some sort (obtained for example during parsing)

Constructors

DynamicSort :: forall (s :: Sort). Sing s -> DynamicSort

Instances

Eq DynamicSort

Methods

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

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

data DynamicallySorted (f :: (Sort -> *) -> Sort -> *) where

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

Constructors

DynamicallySorted :: forall (s :: Sort) 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 :: Sort). SingI s => DynamicSort -> Maybe (Sing s)

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

toStaticallySorted :: forall f (s :: Sort). 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.