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

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

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

Defined in Data.Expression.Equality

Methods

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

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

Defined in Data.Expression

Methods

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

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

Defined in Data.Expression

Methods

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

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

Defined in Data.Expression

Methods

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

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

Defined in Data.Expression.Equality

Methods

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

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

Defined in Data.Expression

Methods

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

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

Defined in Data.Expression

Methods

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

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

Defined in Data.Expression

Methods

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

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

Defined in Data.Expression.Equality

Methods

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

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

Defined in Data.Expression

Methods

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

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

Defined in Data.Expression

Methods

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

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

Defined in Data.Expression

Methods

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

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

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

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

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

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

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

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

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

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

Defined in Data.Expression

Methods

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

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

MaybeQuantified (UniversalF v :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

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

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

MaybeQuantified (VarF :: (Sort -> *) -> Sort -> *)

Defined in Data.Expression

Methods

isQuantified' :: MaybeQuantified g => VarF (IFix g) s -> Const Any s

freevars' :: VarF (Const [DynamicallySorted VarF]) s -> Const [DynamicallySorted VarF] s

(SingI n1, SingI n2) => SingI (ArraySort n1 n2 :: Sort)

Defined in Data.Expression.Sort

Methods

sing :: Sing (ArraySort n1 n2)

JoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

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

join :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

JoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

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

join :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

JoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

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

join :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

JoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

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

join :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

JoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

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

join :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

MeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

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

meet :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

MeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

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

meet :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

MeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

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

meet :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

MeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

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

meet :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

MeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

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

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

Lattice (ALia BooleanSort)

Defined in Data.Expression

Lattice (QFALia BooleanSort)

Defined in Data.Expression

Lattice (Lia BooleanSort)

Defined in Data.Expression

Lattice (QFLia BooleanSort)

Defined in Data.Expression

Lattice (QFLogic BooleanSort)

Defined in Data.Expression

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

BoundedLattice (ALia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFALia BooleanSort)

Defined in Data.Expression

BoundedLattice (Lia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFLia BooleanSort)

Defined in Data.Expression

BoundedLattice (QFLogic BooleanSort)

Defined in Data.Expression

ComplementedLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

complement :: ALia BooleanSort -> ALia BooleanSort

ComplementedLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFALia BooleanSort -> QFALia BooleanSort

ComplementedLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

complement :: Lia BooleanSort -> Lia BooleanSort

ComplementedLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLia BooleanSort -> QFLia BooleanSort

ComplementedLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

complement :: QFLogic BooleanSort -> QFLogic BooleanSort

IfThenElseF :<: f => Parseable IfThenElseF f

Defined in Data.Expression.IfThenElse

Methods

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

ArrayF :<: f => Parseable ArrayF f

Defined in Data.Expression.Array

Methods

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

ArithmeticF :<: f => Parseable ArithmeticF f

Defined in Data.Expression.Arithmetic

Methods

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

NegationF :<: f => Parseable NegationF f

Defined in Data.Expression

Methods

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

DisjunctionF :<: f => Parseable DisjunctionF f

Defined in Data.Expression

Methods

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

ConjunctionF :<: f => Parseable ConjunctionF f

Defined in Data.Expression

Methods

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

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

Defined in Data.Expression.Equality

Methods

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

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

Defined in Data.Expression

Methods

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

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

Defined in Data.Expression

Methods

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

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

Defined in Data.Expression

Methods

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

data Sing (z :: Sort)

Defined in Data.Expression.Sort

data Sing (z :: Sort) where

• SBooleanSort :: Sing BooleanSort
• SIntegralSort :: Sing IntegralSort
• SArraySort :: Sing (ArraySort n n)

type Demote Sort

Defined in Data.Expression.Sort

type Demote Sort = Sort

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

The singleton kind-indexed data family.

Instances

data Sing (z :: Bool)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Bool) where

• SFalse :: Sing False
• STrue :: Sing True

data Sing (z :: Ordering)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Ordering) where

• SLT :: Sing LT
• SEQ :: Sing EQ
• SGT :: Sing GT

data Sing (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: Sing n

data Sing (z :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: ()) where

• STuple0 :: Sing ()

data Sing (z :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Void)

data Sing (z :: Sort)

Defined in Data.Expression.Sort

data Sing (z :: Sort) where

• SBooleanSort :: Sing BooleanSort
• SIntegralSort :: Sing IntegralSort
• SArraySort :: Sing (ArraySort n n)

data Sing (z :: [a])

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: [a]) where

• SNil :: Sing ([] :: [a])
• SCons :: Sing (n1 ': n2)

data Sing (z :: Maybe a)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Maybe a) where

• SNothing :: Sing (Nothing :: Maybe a)
• SJust :: Sing (Just n)

data Sing (z :: NonEmpty a)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: NonEmpty a) where

• (:%|) :: Sing (n1 :| n2)

data Sing (z :: Either a b)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Either a b) where

• SLeft :: Sing (Left n :: Either a b)
• SRight :: Sing (Right n :: Either a b)

data Sing (z :: (a, b))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b)) where

• STuple2 :: Sing ((,) n1 n2)

data Sing (f :: k1 ~> k2)

Defined in Data.Singletons.Internal

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

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

}

data Sing (z :: (a, b, c))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c)) where

• STuple3 :: Sing ((,,) n1 n2 n3)

data Sing (z :: (a, b, c, d))

Defined in Data.Singletons.Prelude.Instances

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

• STuple4 :: Sing ((,,,) n1 n2 n3 n4)

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

Defined in Data.Singletons.Prelude.Instances

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

• STuple5 :: Sing ((,,,,) n1 n2 n3 n4 n5)

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

Defined in Data.Singletons.Prelude.Instances

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

• STuple6 :: Sing ((,,,,,) n1 n2 n3 n4 n5 n6)

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

Defined in Data.Singletons.Prelude.Instances

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

• STuple7 :: Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

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 (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 f => Eq (DynamicallySorted f)

Defined in Data.Expression.Sort

Methods

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

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

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

Defined in Data.Expression.Sort

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

toDynamicallySorted :: forall f (s :: Sort). SingI s => IFix f s -> DynamicallySorted f

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