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

data Sort
- = BooleanSort
- | IntegralSort
- | ArraySort {
  - index :: Sort
  - element :: Sort
  }
data family Sing (a :: k) :: Type
withSort :: forall a (s :: Sort). Sing s -> (SingI s => a) -> a
data DynamicSort where
- DynamicSort :: forall (s :: Sort). Sing s -> DynamicSort
data DynamicallySorted (d :: Sort -> *) where
- DynamicallySorted :: forall (s :: Sort) d. Sing s -> d s -> DynamicallySorted d
type DynamicallySortedFix f = DynamicallySorted (IFix f)
parseSort :: Parser DynamicSort
toDynamicallySorted :: forall d (s :: Sort). SingI s => d s -> DynamicallySorted d
toStaticSort :: forall (s :: Sort). SingI s => DynamicSort -> Maybe (Sing s)
toStaticallySorted :: forall d (s :: Sort). SingI s => DynamicallySorted d -> Maybe (d s)

Documentation

data Sort Source #

A universe of recognized sorts

Constructors

BooleanSort	booleans (true, false)
IntegralSort	integers (..., -1, 0, 1, ...)
ArraySort	arrays indexed by `Sort` sort, containing elements of `element` sort
Fields index :: Sort element :: Sort

Instances

Eq Sort Source #
Instance details Defined in Data.Expression.Sort Methods (==) :: Sort -> Sort -> Bool # (/=) :: Sort -> Sort -> Bool #
Show Sort Source #
Instance details Defined in Data.Expression.Sort Methods showsPrec :: Int -> Sort -> ShowS # show :: Sort -> String # showList :: [Sort] -> ShowS #
SDecide Sort => SDecide Sort Source #
Instance details Defined in Data.Expression.Sort Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) #
SingKind Sort Source #
Instance details Defined in Data.Expression.Sort Associated Types type Demote Sort = (r :: Type) # Methods fromSing :: Sing a -> Demote Sort # toSing :: Demote Sort -> SomeSing Sort #
SingI BooleanSort Source #
Instance details Defined in Data.Expression.Sort Methods sing :: Sing BooleanSort #
SingI IntegralSort Source #
Instance details Defined in Data.Expression.Sort Methods sing :: Sing IntegralSort #
IEq1 IfThenElseF Source #
Instance details Defined in Data.Expression.IfThenElse Methods ieq1 :: IEq a => IfThenElseF a j -> IfThenElseF a j -> Bool Source #
IEq1 ArrayF Source #
Instance details Defined in Data.Expression.Array Methods ieq1 :: IEq a => ArrayF a j -> ArrayF a j -> Bool Source #
IEq1 ArithmeticF Source #
Instance details Defined in Data.Expression.Arithmetic Methods ieq1 :: IEq a => ArithmeticF a j -> ArithmeticF a j -> Bool Source #
IEq1 NegationF Source #
Instance details Defined in Data.Expression Methods ieq1 :: IEq a => NegationF a j -> NegationF a j -> Bool Source #
IEq1 DisjunctionF Source #
Instance details Defined in Data.Expression Methods ieq1 :: IEq a => DisjunctionF a j -> DisjunctionF a j -> Bool Source #
IEq1 ConjunctionF Source #
Instance details Defined in Data.Expression Methods ieq1 :: IEq a => ConjunctionF a j -> ConjunctionF a j -> Bool Source #
IFoldable IfThenElseF Source #
Instance details Defined in Data.Expression.IfThenElse Methods ifold :: Monoid m => IfThenElseF (Const m) i' -> Const m i' Source #
IFoldable ArrayF Source #
Instance details Defined in Data.Expression.Array Methods ifold :: Monoid m => ArrayF (Const m) i' -> Const m i' Source #
IFoldable ArithmeticF Source #
Instance details Defined in Data.Expression.Arithmetic Methods ifold :: Monoid m => ArithmeticF (Const m) i' -> Const m i' Source #
IFoldable NegationF Source #
Instance details Defined in Data.Expression Methods ifold :: Monoid m => NegationF (Const m) i' -> Const m i' Source #
IFoldable DisjunctionF Source #
Instance details Defined in Data.Expression Methods ifold :: Monoid m => DisjunctionF (Const m) i' -> Const m i' Source #
IFoldable ConjunctionF Source #
Instance details Defined in Data.Expression Methods ifold :: Monoid m => ConjunctionF (Const m) i' -> Const m i' Source #
IFunctor IfThenElseF Source #
Instance details Defined in Data.Expression.IfThenElse Methods imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). IfThenElseF a i' -> IfThenElseF b i' Source # index :: IfThenElseF a i' -> Sing i' Source #
IFunctor ArrayF Source #
Instance details Defined in Data.Expression.Array Methods imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ArrayF a i' -> ArrayF b i' Source # index :: ArrayF a i' -> Sing 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 #
IFunctor NegationF Source #
Instance details Defined in Data.Expression Methods imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). NegationF a i' -> NegationF b i' Source # index :: NegationF a i' -> Sing i' Source #
IFunctor DisjunctionF Source #
Instance details Defined in Data.Expression Methods imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). DisjunctionF a i' -> DisjunctionF b i' Source # index :: DisjunctionF a i' -> Sing i' Source #
IFunctor ConjunctionF Source #
Instance details Defined in Data.Expression Methods imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ConjunctionF a i' -> ConjunctionF b i' Source # index :: ConjunctionF a i' -> Sing i' Source #
ITraversable IfThenElseF Source #
Instance details Defined in Data.Expression.IfThenElse Methods itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). IfThenElseF a i' -> f (IfThenElseF b i') Source #
ITraversable ArrayF Source #
Instance details Defined in Data.Expression.Array Methods itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). ArrayF a i' -> f (ArrayF b 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 #
ITraversable NegationF Source #
Instance details Defined in Data.Expression Methods itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). NegationF a i' -> f (NegationF b i') Source #
ITraversable DisjunctionF Source #
Instance details Defined in Data.Expression Methods itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). DisjunctionF a i' -> f (DisjunctionF b i') Source #
ITraversable ConjunctionF Source #
Instance details Defined in Data.Expression Methods itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). ConjunctionF a i' -> f (ConjunctionF b i') Source #
IShow IfThenElseF Source #
Instance details Defined in Data.Expression.IfThenElse Methods ishow :: IfThenElseF (Const String) i -> Const String i Source #
IShow ArrayF Source #
Instance details Defined in Data.Expression.Array Methods ishow :: ArrayF (Const String) i -> Const String i Source #
IShow ArithmeticF Source #
Instance details Defined in Data.Expression.Arithmetic Methods ishow :: ArithmeticF (Const String) i -> Const String i Source #
IShow NegationF Source #
Instance details Defined in Data.Expression Methods ishow :: NegationF (Const String) i -> Const String i Source #
IShow DisjunctionF Source #
Instance details Defined in Data.Expression Methods ishow :: DisjunctionF (Const String) i -> Const String i Source #
IShow ConjunctionF Source #
Instance details Defined in Data.Expression Methods ishow :: ConjunctionF (Const String) i -> Const String i Source #
IShow (EqualityF :: (k -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression.Equality Methods ishow :: EqualityF (Const String) i -> Const String i Source #
IShow (VarF :: (k -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods ishow :: VarF (Const String) i -> Const String i Source #
IShow (ExistentialF v :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods ishow :: ExistentialF v (Const String) i -> Const String i Source #
IShow (UniversalF v :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods ishow :: UniversalF v (Const String) i -> Const String i Source #
IEq1 (EqualityF :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression.Equality Methods ieq1 :: IEq a => EqualityF a j -> EqualityF a j -> Bool Source #
IEq1 (ExistentialF v :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods ieq1 :: IEq a => ExistentialF v a j -> ExistentialF v a j -> Bool Source #
IEq1 (UniversalF v :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods ieq1 :: IEq a => UniversalF v a j -> UniversalF v a j -> Bool Source #
IEq1 (VarF :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods ieq1 :: IEq a => VarF a j -> VarF a j -> Bool Source #
IFoldable (EqualityF :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression.Equality Methods ifold :: Monoid m => EqualityF (Const m) i' -> Const m i' Source #
IFoldable (ExistentialF v :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods ifold :: Monoid m => ExistentialF v (Const m) i' -> Const m i' Source #
IFoldable (UniversalF v :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods ifold :: Monoid m => UniversalF v (Const m) i' -> Const m i' Source #
IFoldable (VarF :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods ifold :: Monoid m => VarF (Const m) i' -> Const m i' Source #
IFunctor (EqualityF :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression.Equality Methods imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). EqualityF a i' -> EqualityF b i' Source # index :: EqualityF a i' -> Sing i' Source #
IFunctor (ExistentialF v :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ExistentialF v a i' -> ExistentialF v b i' Source # index :: ExistentialF v a i' -> Sing i' Source #
IFunctor (UniversalF v :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). UniversalF v a i' -> UniversalF v b i' Source # index :: UniversalF v a i' -> Sing i' Source #
IFunctor (VarF :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). VarF a i' -> VarF b i' Source # index :: VarF a i' -> Sing i' Source #
ITraversable (EqualityF :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression.Equality Methods itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). EqualityF a i' -> f (EqualityF b i') Source #
ITraversable (ExistentialF v :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). ExistentialF v a i' -> f (ExistentialF v b i') Source #
ITraversable (UniversalF v :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). UniversalF v a i' -> f (UniversalF v b i') Source #
ITraversable (VarF :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods itraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). VarF a i' -> f (VarF b i') Source #
MaybeQuantified (ExistentialF v :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods isQuantified' :: MaybeQuantified g => ExistentialF v (IFix g) s -> Const Any s freevars' :: ExistentialF v (Const [DynamicallySorted Var]) s -> Const [DynamicallySorted Var] s
MaybeQuantified (UniversalF v :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods isQuantified' :: MaybeQuantified g => UniversalF v (IFix g) s -> Const Any s freevars' :: UniversalF v (Const [DynamicallySorted Var]) s -> Const [DynamicallySorted Var] s
MaybeQuantified (VarF :: (Sort -> Type) -> Sort -> Type) Source #
Instance details Defined in Data.Expression Methods isQuantified' :: MaybeQuantified g => VarF (IFix g) s -> Const Any s freevars' :: VarF (Const [DynamicallySorted Var]) s -> Const [DynamicallySorted Var] s
(SingI n1, SingI n2) => SingI (ArraySort n1 n2 :: Sort) Source #
Instance details Defined in Data.Expression.Sort Methods sing :: Sing (ArraySort n1 n2) #
JoinSemiLattice (ALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
JoinSemiLattice (QFALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort # join :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort #
JoinSemiLattice (Lia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
JoinSemiLattice (QFLia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort # join :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort #
JoinSemiLattice (QFLogic BooleanSort) Source #
Instance details Defined in Data.Expression Methods (\/) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort # join :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort #
MeetSemiLattice (ALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort # meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort #
MeetSemiLattice (QFALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort # meet :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort #
MeetSemiLattice (Lia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort # meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort #
MeetSemiLattice (QFLia BooleanSort) Source #
Instance details Defined in Data.Expression Methods (/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort # meet :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort #
MeetSemiLattice (QFLogic BooleanSort) Source #
Instance details Defined in Data.Expression Methods (/\) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort # meet :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort #
Lattice (ALia BooleanSort) Source #
Instance details Defined in Data.Expression
Lattice (QFALia BooleanSort) Source #
Instance details Defined in Data.Expression
Lattice (Lia BooleanSort) Source #
Instance details Defined in Data.Expression
Lattice (QFLia BooleanSort) Source #
Instance details Defined in Data.Expression
Lattice (QFLogic BooleanSort) Source #
Instance details Defined in Data.Expression
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 #
BoundedJoinSemiLattice (QFLogic BooleanSort) Source #
Instance details Defined in Data.Expression Methods bottom :: QFLogic 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 #
BoundedMeetSemiLattice (QFLogic BooleanSort) Source #
Instance details Defined in Data.Expression Methods top :: QFLogic BooleanSort #
BoundedLattice (ALia BooleanSort) Source #
Instance details Defined in Data.Expression
BoundedLattice (QFALia BooleanSort) Source #
Instance details Defined in Data.Expression
BoundedLattice (Lia BooleanSort) Source #
Instance details Defined in Data.Expression
BoundedLattice (QFLia BooleanSort) Source #
Instance details Defined in Data.Expression
BoundedLattice (QFLogic BooleanSort) Source #
Instance details Defined in Data.Expression
ComplementedLattice (ALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods complement :: ALia BooleanSort -> ALia BooleanSort Source #
ComplementedLattice (QFALia BooleanSort) Source #
Instance details Defined in Data.Expression Methods complement :: QFALia BooleanSort -> QFALia BooleanSort Source #
ComplementedLattice (Lia BooleanSort) Source #
Instance details Defined in Data.Expression Methods complement :: Lia BooleanSort -> Lia BooleanSort Source #
ComplementedLattice (QFLia BooleanSort) Source #
Instance details Defined in Data.Expression Methods complement :: QFLia BooleanSort -> QFLia BooleanSort Source #
ComplementedLattice (QFLogic BooleanSort) Source #
Instance details Defined in Data.Expression Methods complement :: QFLogic BooleanSort -> QFLogic BooleanSort Source #
IfThenElseF :<: f => Parseable IfThenElseF f Source #
Instance details Defined in Data.Expression.IfThenElse Methods parser :: Proxy IfThenElseF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f) Source #
ArrayF :<: f => Parseable ArrayF f Source #
Instance details Defined in Data.Expression.Array Methods parser :: Proxy ArrayF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f) Source #
ArithmeticF :<: f => Parseable ArithmeticF f Source #
Instance details Defined in Data.Expression.Arithmetic Methods parser :: Proxy ArithmeticF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f) Source #
NegationF :<: f => Parseable NegationF f Source #
Instance details Defined in Data.Expression Methods parser :: Proxy NegationF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f) Source #
DisjunctionF :<: f => Parseable DisjunctionF f Source #
Instance details Defined in Data.Expression Methods parser :: Proxy DisjunctionF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f) Source #
ConjunctionF :<: f => Parseable ConjunctionF f Source #
Instance details Defined in Data.Expression Methods parser :: Proxy ConjunctionF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f) Source #
(EqualityF :: (Sort -> Type) -> Sort -> Type) :<: f => Parseable (EqualityF :: (k -> Type) -> Sort -> Type) f Source #
Instance details Defined in Data.Expression.Equality Methods parser :: Proxy EqualityF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f) Source #
(ExistentialF v :<: f, SingI v) => Parseable (ExistentialF v :: (Sort -> Type) -> Sort -> Type) f Source #
Instance details Defined in Data.Expression Methods parser :: Proxy (ExistentialF v) -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f) Source #
(UniversalF v :<: f, SingI v) => Parseable (UniversalF v :: (Sort -> Type) -> Sort -> Type) f Source #
Instance details Defined in Data.Expression Methods parser :: Proxy (UniversalF v) -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f) Source #
(VarF :: (Sort -> Type) -> Sort -> Type) :<: f => Parseable (VarF :: k -> Sort -> Type) f Source #
Instance details Defined in Data.Expression Methods parser :: Proxy VarF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f) Source #
SingI d => SingI (TyCon1 (ArraySort d) :: Sort ~> Sort) Source #
Instance details Defined in Data.Expression.Sort Methods sing :: Sing (TyCon1 (ArraySort d)) #
SingI (TyCon2 ArraySort) Source #
Instance details Defined in Data.Expression.Sort Methods sing :: Sing (TyCon2 ArraySort) #
data Sing (a :: Sort) Source #
Instance details Defined in Data.Expression.Sort data Sing (a :: Sort) where SBooleanSort :: forall (a :: Sort). Sing BooleanSort SIntegralSort :: forall (a :: Sort). Sing IntegralSort SArraySort :: forall (a :: Sort) (n :: Sort) (n :: Sort). {..} -> Sing (ArraySort n n)
type Demote Sort Source #
Instance details Defined in Data.Expression.Sort type Demote Sort = Sort

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

The singleton kind-indexed data family.

Instances

data Sing (a :: Bool)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Bool) where SFalse :: forall (a :: Bool). Sing False STrue :: forall (a :: Bool). Sing True
data Sing (a :: Ordering)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Ordering) where SLT :: forall (a :: Ordering). Sing LT SEQ :: forall (a :: Ordering). Sing EQ SGT :: forall (a :: Ordering). Sing GT
data Sing (n :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Nat) where SNat :: forall (n :: Nat). KnownNat n => Sing n
data Sing (n :: Symbol)
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Symbol) where SSym :: forall (n :: Symbol). KnownSymbol n => Sing n
data Sing (a :: ())
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: ()) where STuple0 :: forall (a :: ()). Sing ()
data Sing (a :: Void)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Void)
data Sing (a :: All)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: All) where SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)
data Sing (a :: Any)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: Any) where SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)
data Sing (a :: Sort) Source #
Instance details Defined in Data.Expression.Sort data Sing (a :: Sort) where SBooleanSort :: forall (a :: Sort). Sing BooleanSort SIntegralSort :: forall (a :: Sort). Sing IntegralSort SArraySort :: forall (a :: Sort) (n :: Sort) (n :: Sort). {..} -> Sing (ArraySort n n)
data Sing (b :: [a])
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: [a]) where SNil :: forall a (b :: [a]). Sing ([] :: [a]) SCons :: forall a (b :: [a]) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 ': n2)
data Sing (b :: Maybe a)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: Maybe a) where SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a) SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)
data Sing (b :: Min a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Min a) where SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)
data Sing (b :: Max a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Max a) where SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)
data Sing (b :: First a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)
data Sing (b :: Last a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)
data Sing (a :: WrappedMonoid m)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)
data Sing (b :: Option a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Option a) where SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)
data Sing (b :: Identity a)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: Identity a) where SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)
data Sing (b :: First a)
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)
data Sing (b :: Last a)
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)
data Sing (b :: Dual a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Dual a) where SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)
data Sing (b :: Sum a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Sum a) where SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)
data Sing (b :: Product a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Product a) where SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)
data Sing (b :: Down a)
Instance details Defined in Data.Singletons.Prelude.Ord data Sing (b :: Down a) where SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)
data Sing (b :: NonEmpty a)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: NonEmpty a) where (:%\|) :: forall a (b :: NonEmpty a) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 :\| n2)
data Sing (b :: Endo a)
Instance details Defined in Data.Singletons.Prelude.Foldable data Sing (b :: Endo a) where SEndo :: forall a (b :: Endo a) (x :: a ~> a). Sing x -> Sing (Endo x)
data Sing (b :: MinInternal a)
Instance details Defined in Data.Singletons.Prelude.Foldable data Sing (b :: MinInternal a) where SMinInternal :: forall a (b :: MinInternal a) (x :: Maybe a). Sing x -> Sing (MinInternal x)
data Sing (b :: MaxInternal a)
Instance details Defined in Data.Singletons.Prelude.Foldable data Sing (b :: MaxInternal a) where SMaxInternal :: forall a (b :: MaxInternal a) (x :: Maybe a). Sing x -> Sing (MaxInternal x)
data Sing (c :: Either a b)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: Either a b) where SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b) SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)
data Sing (c :: (a, b))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: (a, b)) where STuple2 :: forall a b (c :: (a, b)) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing ((,) n1 n2)
data Sing (c :: Arg a b)
Instance details Defined in Data.Singletons.Prelude.Semigroup data Sing (c :: Arg a b) where SArg :: forall a b (c :: Arg a b) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing (Arg n1 n2)
data Sing (f :: k1 ~> k2)
Instance details Defined in Data.Singletons.Internal data Sing (f :: k1 ~> k2) = SLambda { applySing :: forall (t :: k1). Sing t -> Sing (f @@ t) }
data Sing (b :: StateL s a)
Instance details Defined in Data.Singletons.Prelude.Traversable data Sing (b :: StateL s a) where SStateL :: forall s a (b :: StateL s a) (x :: s ~> (s, a)). Sing x -> Sing (StateL x)
data Sing (b :: StateR s a)
Instance details Defined in Data.Singletons.Prelude.Traversable data Sing (b :: StateR s a) where SStateR :: forall s a (b :: StateR s a) (x :: s ~> (s, a)). Sing x -> Sing (StateR x)
data Sing (d :: (a, b, c))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (d :: (a, b, c)) where STuple3 :: forall a b c (d :: (a, b, c)) (n1 :: a) (n2 :: b) (n3 :: c). Sing n1 -> Sing n2 -> Sing n3 -> Sing ((,,) n1 n2 n3)
data Sing (c :: Const a b)
Instance details Defined in Data.Singletons.Prelude.Const data Sing (c :: Const a b) where SConst :: forall k a (b :: k) (c :: Const a b) (a1 :: a). {..} -> Sing (Const a1 :: Const a b)
data Sing (e :: (a, b, c, d))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (e :: (a, b, c, d)) where STuple4 :: forall a b c d (e :: (a, b, c, d)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing ((,,,) n1 n2 n3 n4)
data Sing (f :: (a, b, c, d, e))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (f :: (a, b, c, d, e)) where STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing ((,,,,) n1 n2 n3 n4 n5)
data Sing (g :: (a, b, c, d, e, f))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (g :: (a, b, c, d, e, f)) where STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing ((,,,,,) n1 n2 n3 n4 n5 n6)
data Sing (h :: (a, b, c, d, e, f, g))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (h :: (a, b, c, d, e, f, g)) where STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f) (n7 :: g). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing n7 -> Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

withSort :: forall a (s :: Sort). Sing s -> (SingI s => a) -> a Source #

Turn implicit sort parameter into explicit one

data DynamicSort where Source #

Some sort (obtained for example during parsing)

Constructors

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

Instances

Eq DynamicSort Source #
Instance details Defined in Data.Expression.Sort Methods (==) :: DynamicSort -> DynamicSort -> Bool # (/=) :: DynamicSort -> DynamicSort -> Bool #

data DynamicallySorted (d :: Sort -> *) where Source #

A value of some sort

Constructors

DynamicallySorted :: forall (s :: Sort) d. Sing s -> d s -> DynamicallySorted d

Instances

(forall (s :: Sort). Eq (d s)) => Eq (DynamicallySorted d) Source #
Instance details Defined in Data.Expression.Sort Methods (==) :: DynamicallySorted d -> DynamicallySorted d -> Bool # (/=) :: DynamicallySorted d -> DynamicallySorted d -> Bool #
(forall (s :: Sort). Show (d s)) => Show (DynamicallySorted d) Source #
Instance details Defined in Data.Expression.Sort Methods showsPrec :: Int -> DynamicallySorted d -> ShowS # show :: DynamicallySorted d -> String # showList :: [DynamicallySorted d] -> ShowS #

type DynamicallySortedFix f = DynamicallySorted (IFix f) Source #

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

parseSort :: Parser DynamicSort Source #

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

toDynamicallySorted :: forall d (s :: Sort). SingI s => d s -> DynamicallySorted d Source #

Converts a statically sorted expression to a dynamically sorted one.

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

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

toStaticallySorted :: forall d (s :: Sort). SingI s => DynamicallySorted d -> Maybe (d s) Source #

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