Copyright	(C) 2017-18 Jakub Daniel
License	BSD-style (see the file LICENSE)
Maintainer	Jakub Daniel <jakub.daniel@protonmail.com>
Stability	experimental
Safe Haskell	None
Language	Haskell2010

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 index :: Sort element :: Sort

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 :: * # Methods fromSing :: Sing Sort a -> DemoteRep Sort # toSing :: DemoteRep Sort -> SomeSing 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 #
Methods ishow :: f (Const k String) i -> Const DisjunctionF String i Source #
IShow Sort Sort ConjunctionF Source #
Methods ishow :: f (Const k String) i -> Const ConjunctionF String i 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 #
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) Source #
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 -> *)) 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) #
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) Source #
Methods complement :: ALia BooleanSort -> ALia BooleanSort Source #
ComplementedLattice (QFALia BooleanSort) Source #
Methods complement :: QFALia BooleanSort -> QFALia BooleanSort Source #
ComplementedLattice (Lia BooleanSort) Source #
Methods complement :: Lia BooleanSort -> Lia BooleanSort Source #
ComplementedLattice (QFLia BooleanSort) Source #
Methods complement :: QFLia BooleanSort -> QFLia BooleanSort Source #
ComplementedLattice (QFLogic BooleanSort) Source #
Methods complement :: QFLogic BooleanSort -> QFLogic BooleanSort Source #
(:<:) Sort ArrayF f => Parseable ((Sort -> ) -> Sort -> ) ArrayF f Source #
Methods parser :: Proxy ArrayF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #
(:<:) Sort ArithmeticF f => Parseable ((Sort -> ) -> Sort -> ) ArithmeticF f Source #
Methods parser :: Proxy ArithmeticF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #
(:<:) Sort NegationF f => Parseable ((Sort -> ) -> Sort -> ) NegationF f Source #
Methods parser :: Proxy NegationF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #
(:<:) Sort DisjunctionF f => Parseable ((Sort -> ) -> Sort -> ) DisjunctionF f Source #
Methods parser :: Proxy DisjunctionF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #
(:<:) Sort ConjunctionF f => Parseable ((Sort -> ) -> Sort -> ) ConjunctionF f Source #
Methods parser :: Proxy ConjunctionF f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #
(:<:) Sort (EqualityF Sort) f => Parseable ((k -> ) -> Sort -> ) (EqualityF k) f Source #
Methods parser :: Proxy (EqualityF k) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #
((:<:) Sort (ExistentialF v) f, SingI Sort v) => Parseable ((Sort -> ) -> Sort -> ) (ExistentialF v) f Source #
Methods parser :: Proxy (ExistentialF v) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #
((:<:) Sort (UniversalF v) f, SingI Sort v) => Parseable ((Sort -> ) -> Sort -> ) (UniversalF v) f Source #
Methods parser :: Proxy (UniversalF v) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #
(:<:) Sort (VarF (Sort -> )) f => Parseable (k -> Sort -> ) (VarF k) f Source #
Methods parser :: Proxy (VarF k) f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g) Source #
data Sing Sort Source #
data Sing Sort where SBooleanSort :: Sing Sort z SIntegralSort :: Sing Sort z SArraySort :: Sing Sort z
type DemoteRep Sort Source #
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 Source #

Some sort (obtained for example during parsing)

Constructors

DynamicSort :: forall s. Sing s -> DynamicSort

Instances

Eq DynamicSort Source #
Methods (==) :: DynamicSort -> DynamicSort -> Bool # (/=) :: DynamicSort -> DynamicSort -> Bool #

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

Instances

IEq1 Sort f => Eq (DynamicallySorted f) Source #
Methods (==) :: DynamicallySorted f -> DynamicallySorted f -> Bool # (/=) :: DynamicallySorted f -> DynamicallySorted f -> Bool #
(IFunctor Sort f, IShow Sort Sort f) => Show (DynamicallySorted f) Source #
Methods showsPrec :: Int -> DynamicallySorted f -> ShowS # show :: DynamicallySorted f -> String # showList :: [DynamicallySorted f] -> ShowS #

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.