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 Sort sort, containing elements of element sort

Fields

• index :: Sort
• element :: Sort

Instances

Eq Sort

Defined in Data.Expression.Sort

Methods

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

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

Show Sort

Defined in Data.Expression.Sort

Methods

showsPrec :: Int -> Sort -> ShowS

show :: Sort -> String

showList :: [Sort] -> ShowS

SDecide Sort => SDecide Sort

Defined in Data.Expression.Sort

Methods

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

SingKind Sort

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

Defined in Data.Expression.Sort

Methods

sing :: Sing BooleanSort

SingI IntegralSort

Defined in Data.Expression.Sort

Methods

sing :: Sing IntegralSort

IEq1 IfThenElseF

Defined in Data.Expression.IfThenElse

Methods

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

IEq1 ArrayF

Defined in Data.Expression.Array

Methods

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

IEq1 ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

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

IEq1 NegationF

Defined in Data.Expression

Methods

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

IEq1 DisjunctionF

Defined in Data.Expression

Methods

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

IEq1 ConjunctionF

Defined in Data.Expression

Methods

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

IFoldable IfThenElseF

Defined in Data.Expression.IfThenElse

Methods

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

IFoldable ArrayF

Defined in Data.Expression.Array

Methods

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

IFoldable ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

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

IFoldable NegationF

Defined in Data.Expression

Methods

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

IFoldable DisjunctionF

Defined in Data.Expression

Methods

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

IFoldable ConjunctionF

Defined in Data.Expression

Methods

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

IFunctor IfThenElseF

Defined in Data.Expression.IfThenElse

Methods

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

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

IFunctor ArrayF

Defined in Data.Expression.Array

Methods

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

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

IFunctor ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

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

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

IFunctor NegationF

Defined in Data.Expression

Methods

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

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

IFunctor DisjunctionF

Defined in Data.Expression

Methods

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

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

IFunctor ConjunctionF

Defined in Data.Expression

Methods

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

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

ITraversable IfThenElseF

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')

ITraversable ArrayF

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')

ITraversable ArithmeticF

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')

ITraversable NegationF

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')

ITraversable DisjunctionF

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')

ITraversable ConjunctionF

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')

IShow IfThenElseF

Defined in Data.Expression.IfThenElse

Methods

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

IShow ArrayF

Defined in Data.Expression.Array

Methods

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

IShow ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

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

IShow NegationF

Defined in Data.Expression

Methods

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

IShow DisjunctionF

Defined in Data.Expression

Methods

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

IShow ConjunctionF

Defined in Data.Expression

Methods

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

IShow (EqualityF :: (k -> Type) -> Sort -> Type)

Defined in Data.Expression.Equality

Methods

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

IShow (VarF :: (k -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

ishow :: VarF (Const String) i -> Const String i

IShow (ExistentialF v :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

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

IShow (UniversalF v :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

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

IEq1 (EqualityF :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression.Equality

Methods

ieq1 :: IEq a => EqualityF a j -> EqualityF a j -> Bool

IEq1 (ExistentialF v :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

ieq1 :: IEq a => ExistentialF v a j -> ExistentialF v a j -> Bool

IEq1 (UniversalF v :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

ieq1 :: IEq a => UniversalF v a j -> UniversalF v a j -> Bool

IEq1 (VarF :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

ieq1 :: IEq a => VarF a j -> VarF a j -> Bool

IFoldable (EqualityF :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression.Equality

Methods

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

IFoldable (ExistentialF v :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

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

IFoldable (UniversalF v :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

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

IFoldable (VarF :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

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

IFunctor (EqualityF :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression.Equality

Methods

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

index :: EqualityF a i' -> Sing i'

IFunctor (ExistentialF v :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

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

index :: ExistentialF v a i' -> Sing i'

IFunctor (UniversalF v :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

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

index :: UniversalF v a i' -> Sing i'

IFunctor (VarF :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

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

index :: VarF a i' -> Sing i'

ITraversable (EqualityF :: (Sort -> Type) -> Sort -> Type)

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')

ITraversable (ExistentialF v :: (Sort -> Type) -> Sort -> Type)

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')

ITraversable (UniversalF v :: (Sort -> Type) -> Sort -> Type)

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')

ITraversable (VarF :: (Sort -> Type) -> Sort -> Type)

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')

MaybeQuantified (ExistentialF v :: (Sort -> Type) -> Sort -> Type)

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)

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)

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)

Defined in Data.Expression.Sort

Methods

sing :: Sing (ArraySort n1 n2)

Heyting (ALia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

neg :: ALia BooleanSort -> ALia BooleanSort

(<=>) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

Heyting (QFALia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

neg :: QFALia BooleanSort -> QFALia BooleanSort

(<=>) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

Heyting (Lia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

neg :: Lia BooleanSort -> Lia BooleanSort

(<=>) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

Heyting (QFLia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

neg :: QFLia BooleanSort -> QFLia BooleanSort

(<=>) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

Heyting (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(==>) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

neg :: QFLogic BooleanSort -> QFLogic BooleanSort

(<=>) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

Lattice (ALia BooleanSort)

Defined in Data.Expression

Methods

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

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

Lattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

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

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

Lattice (Lia BooleanSort)

Defined in Data.Expression

Methods

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

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

Lattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

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

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

Lattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

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

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

BoundedJoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: ALia BooleanSort

BoundedJoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFALia BooleanSort

BoundedJoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

bottom :: Lia BooleanSort

BoundedJoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLia BooleanSort

BoundedJoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLogic BooleanSort

BoundedMeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

top :: ALia BooleanSort

BoundedMeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

top :: QFALia BooleanSort

BoundedMeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

top :: Lia BooleanSort

BoundedMeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

top :: QFLia BooleanSort

BoundedMeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

top :: QFLogic BooleanSort

IfThenElseF :<: f => Parseable IfThenElseF f

Defined in Data.Expression.IfThenElse

Methods

parser :: Proxy IfThenElseF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f)

ArrayF :<: f => Parseable ArrayF f

Defined in Data.Expression.Array

Methods

parser :: Proxy ArrayF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f)

ArithmeticF :<: f => Parseable ArithmeticF f

Defined in Data.Expression.Arithmetic

Methods

parser :: Proxy ArithmeticF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f)

NegationF :<: f => Parseable NegationF f

Defined in Data.Expression

Methods

parser :: Proxy NegationF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f)

DisjunctionF :<: f => Parseable DisjunctionF f

Defined in Data.Expression

Methods

parser :: Proxy DisjunctionF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f)

ConjunctionF :<: f => Parseable ConjunctionF f

Defined in Data.Expression

Methods

parser :: Proxy ConjunctionF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f)

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

Defined in Data.Expression.Equality

Methods

parser :: Proxy EqualityF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f)

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

Defined in Data.Expression

Methods

parser :: Proxy (ExistentialF v) -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f)

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

Defined in Data.Expression

Methods

parser :: Proxy (UniversalF v) -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f)

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

Defined in Data.Expression

Methods

parser :: Proxy VarF -> Parser (DynamicallySortedFix f) -> Parser (DynamicallySortedFix f)

SingI d => SingI (TyCon1 (ArraySort d) :: Sort ~> Sort)

Defined in Data.Expression.Sort

Methods

sing :: Sing (TyCon1 (ArraySort d))

SingI (TyCon2 ArraySort)

Defined in Data.Expression.Sort

Methods

sing :: Sing (TyCon2 ArraySort)

data Sing (a :: Sort)

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

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)

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)

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)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: forall (n :: Nat). KnownNat n => Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: forall (n :: Symbol). KnownSymbol n => Sing n

data Sing (a :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where

• STuple0 :: forall (a :: ()). Sing ()

data Sing (a :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)

data Sing (a :: All)

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)

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)

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])

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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 :: MaxInternal a)

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 (b :: MinInternal a)

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 (c :: Either a b)

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

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)

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)

newtype Sing (f :: k1 ~> k2)

Defined in Data.Singletons.Internal

newtype Sing (f :: k1 ~> k2) = SLambda {

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

}

data Sing (b :: StateL s a)

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)

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

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)

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

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

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

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

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

Turn implicit sort parameter into explicit one

data DynamicSort where

Some sort (obtained for example during parsing)

Constructors

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

Instances

Eq DynamicSort

Defined in Data.Expression.Sort

Methods

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

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

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

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)

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)

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)

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

parseSort :: Parser DynamicSort

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

Converts a statically sorted expression to a dynamically sorted one.

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

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

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

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