expressions-0.5: Expressions and Formulae a la carte

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 Sort sort, containing elements of element sort Fieldsindex :: Sort element :: Sort
Instances
 Source # Instance detailsDefined in Data.Expression.Sort Methods(==) :: Sort -> Sort -> Bool #(/=) :: Sort -> Sort -> Bool # Source # Instance detailsDefined in Data.Expression.Sort MethodsshowsPrec :: Int -> Sort -> ShowS #show :: Sort -> String #showList :: [Sort] -> ShowS # Source # Instance detailsDefined in Data.Expression.Sort Methods(%~) :: Sing a -> Sing b -> Decision (a :~: b) # Source # Instance detailsDefined in Data.Expression.Sort Associated Typestype Demote Sort = (r :: Type) # MethodsfromSing :: Sing a -> Demote Sort # Source # Instance detailsDefined in Data.Expression.Sort Methods Source # Instance detailsDefined in Data.Expression.Sort Methods Source # Instance detailsDefined in Data.Expression.IfThenElse Methodsieq1 :: IEq a => IfThenElseF a j -> IfThenElseF a j -> Bool Source # Source # Instance detailsDefined in Data.Expression.Array Methodsieq1 :: IEq a => ArrayF a j -> ArrayF a j -> Bool Source # Source # Instance detailsDefined in Data.Expression.Arithmetic Methodsieq1 :: IEq a => ArithmeticF a j -> ArithmeticF a j -> Bool Source # Source # Instance detailsDefined in Data.Expression Methodsieq1 :: IEq a => NegationF a j -> NegationF a j -> Bool Source # Source # Instance detailsDefined in Data.Expression Methodsieq1 :: IEq a => DisjunctionF a j -> DisjunctionF a j -> Bool Source # Source # Instance detailsDefined in Data.Expression Methodsieq1 :: IEq a => ConjunctionF a j -> ConjunctionF a j -> Bool Source # Source # Instance detailsDefined in Data.Expression.IfThenElse Methodsifold :: Monoid m => IfThenElseF (Const m) i' -> Const m i' Source # Source # Instance detailsDefined in Data.Expression.Array Methodsifold :: Monoid m => ArrayF (Const m) i' -> Const m i' Source # Source # Instance detailsDefined in Data.Expression.Arithmetic Methodsifold :: Monoid m => ArithmeticF (Const m) i' -> Const m i' Source # Source # Instance detailsDefined in Data.Expression Methodsifold :: Monoid m => NegationF (Const m) i' -> Const m i' Source # Source # Instance detailsDefined in Data.Expression Methodsifold :: Monoid m => DisjunctionF (Const m) i' -> Const m i' Source # Source # Instance detailsDefined in Data.Expression Methodsifold :: Monoid m => ConjunctionF (Const m) i' -> Const m i' Source # Source # Instance detailsDefined in Data.Expression.IfThenElse Methodsimap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). IfThenElseF a i' -> IfThenElseF b i' Source #index :: IfThenElseF a i' -> Sing i' Source # Source # Instance detailsDefined in Data.Expression.Array Methodsimap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ArrayF a i' -> ArrayF b i' Source #index :: ArrayF a i' -> Sing i' Source # Source # Instance detailsDefined in Data.Expression.Arithmetic Methodsimap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ArithmeticF a i' -> ArithmeticF b i' Source #index :: ArithmeticF a i' -> Sing i' Source # Source # Instance detailsDefined in Data.Expression Methodsimap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). NegationF a i' -> NegationF b i' Source #index :: NegationF a i' -> Sing i' Source # Source # Instance detailsDefined in Data.Expression Methodsimap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). DisjunctionF a i' -> DisjunctionF b i' Source #index :: DisjunctionF a i' -> Sing i' Source # Source # Instance detailsDefined in Data.Expression Methodsimap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ConjunctionF a i' -> ConjunctionF b i' Source #index :: ConjunctionF a i' -> Sing i' Source # Source # Instance detailsDefined in Data.Expression.IfThenElse Methodsitraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). IfThenElseF a i' -> f (IfThenElseF b i') Source # Source # Instance detailsDefined in Data.Expression.Array Methodsitraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). ArrayF a i' -> f (ArrayF b i') Source # Source # Instance detailsDefined in Data.Expression.Arithmetic Methodsitraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). ArithmeticF a i' -> f (ArithmeticF b i') Source # Source # Instance detailsDefined in Data.Expression Methodsitraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). NegationF a i' -> f (NegationF b i') Source # Source # Instance detailsDefined in Data.Expression Methodsitraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). DisjunctionF a i' -> f (DisjunctionF b i') Source # Source # Instance detailsDefined in Data.Expression Methodsitraverse :: Applicative f => (forall (i' :: i). a i' -> f (b i')) -> forall (i' :: i). ConjunctionF a i' -> f (ConjunctionF b i') Source # Source # Instance detailsDefined in Data.Expression.IfThenElse Methods Source # Instance detailsDefined in Data.Expression.Array Methodsishow :: ArrayF (Const String) i -> Const String i Source # Source # Instance detailsDefined in Data.Expression.Arithmetic Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods IShow (EqualityF :: (k -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression.Equality Methods IShow (VarF :: (k -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression Methodsishow :: VarF (Const String) i -> Const String i Source # IShow (ExistentialF v :: (Sort -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression Methodsishow :: ExistentialF v (Const String) i -> Const String i Source # IShow (UniversalF v :: (Sort -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression Methodsishow :: UniversalF v (Const String) i -> Const String i Source # IEq1 (EqualityF :: (Sort -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression.Equality Methodsieq1 :: IEq a => EqualityF a j -> EqualityF a j -> Bool Source # IEq1 (ExistentialF v :: (Sort -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression Methodsieq1 :: IEq a => ExistentialF v a j -> ExistentialF v a j -> Bool Source # IEq1 (UniversalF v :: (Sort -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression Methodsieq1 :: IEq a => UniversalF v a j -> UniversalF v a j -> Bool Source # IEq1 (VarF :: (Sort -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression Methodsieq1 :: IEq a => VarF a j -> VarF a j -> Bool Source # IFoldable (EqualityF :: (Sort -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression.Equality Methodsifold :: Monoid m => EqualityF (Const m) i' -> Const m i' Source # IFoldable (ExistentialF v :: (Sort -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression Methodsifold :: Monoid m => ExistentialF v (Const m) i' -> Const m i' Source # IFoldable (UniversalF v :: (Sort -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression Methodsifold :: Monoid m => UniversalF v (Const m) i' -> Const m i' Source # IFoldable (VarF :: (Sort -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression Methodsifold :: Monoid m => VarF (Const m) i' -> Const m i' Source # IFunctor (EqualityF :: (Sort -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression.Equality Methodsimap :: (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 detailsDefined in Data.Expression Methodsimap :: (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 detailsDefined in Data.Expression Methodsimap :: (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 detailsDefined in Data.Expression Methodsimap :: (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 detailsDefined in Data.Expression.Equality Methodsitraverse :: 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 detailsDefined in Data.Expression Methodsitraverse :: 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 detailsDefined in Data.Expression Methodsitraverse :: 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 detailsDefined in Data.Expression Methodsitraverse :: 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 detailsDefined in Data.Expression MethodsisQuantified' :: MaybeQuantified g => ExistentialF v (IFix g) s -> Const Any s MaybeQuantified (UniversalF v :: (Sort -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression MethodsisQuantified' :: MaybeQuantified g => UniversalF v (IFix g) s -> Const Any s MaybeQuantified (VarF :: (Sort -> Type) -> Sort -> Type) Source # Instance detailsDefined in Data.Expression MethodsisQuantified' :: MaybeQuantified g => VarF (IFix g) s -> Const Any s (SingI n1, SingI n2) => SingI (ArraySort n1 n2 :: Sort) Source # Instance detailsDefined in Data.Expression.Sort Methodssing :: Sing (ArraySort n1 n2) # Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression.IfThenElse Methods Source # Instance detailsDefined in Data.Expression.Array Methods Source # Instance detailsDefined in Data.Expression.Arithmetic Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods Source # Instance detailsDefined in Data.Expression Methods (EqualityF :: (Sort -> Type) -> Sort -> Type) :<: f => Parseable (EqualityF :: (k -> Type) -> Sort -> Type) f Source # Instance detailsDefined in Data.Expression.Equality Methods (ExistentialF v :<: f, SingI v) => Parseable (ExistentialF v :: (Sort -> Type) -> Sort -> Type) f Source # Instance detailsDefined in Data.Expression Methods (UniversalF v :<: f, SingI v) => Parseable (UniversalF v :: (Sort -> Type) -> Sort -> Type) f Source # Instance detailsDefined in Data.Expression Methods (VarF :: (Sort -> Type) -> Sort -> Type) :<: f => Parseable (VarF :: k -> Sort -> Type) f Source # Instance detailsDefined in Data.Expression Methods SingI d => SingI (TyCon1 (ArraySort d) :: Sort ~> Sort) Source # Instance detailsDefined in Data.Expression.Sort Methodssing :: Sing (TyCon1 (ArraySort d)) # Source # Instance detailsDefined in Data.Expression.Sort Methods data Sing (a :: Sort) Source # Instance detailsDefined in Data.Expression.Sort data Sing (a :: Sort) whereSBooleanSort :: forall (a :: Sort). Sing BooleanSortSIntegralSort :: forall (a :: Sort). Sing IntegralSortSArraySort :: forall (a :: Sort) (n :: Sort) (n :: Sort). {..} -> Sing (ArraySort n n) type Demote Sort Source # Instance detailsDefined 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 detailsDefined in Data.Singletons.Prelude.Instances data Sing (a :: Bool) whereSFalse :: forall (a :: Bool). Sing FalseSTrue :: forall (a :: Bool). Sing True data Sing (a :: Ordering) Instance detailsDefined in Data.Singletons.Prelude.Instances data Sing (a :: Ordering) whereSLT :: forall (a :: Ordering). Sing LTSEQ :: forall (a :: Ordering). Sing EQSGT :: forall (a :: Ordering). Sing GT data Sing (n :: Nat) Instance detailsDefined in Data.Singletons.TypeLits.Internal data Sing (n :: Nat) whereSNat :: forall (n :: Nat). KnownNat n => Sing n data Sing (n :: Symbol) Instance detailsDefined in Data.Singletons.TypeLits.Internal data Sing (n :: Symbol) whereSSym :: forall (n :: Symbol). KnownSymbol n => Sing n data Sing (a :: ()) Instance detailsDefined in Data.Singletons.Prelude.Instances data Sing (a :: ()) whereSTuple0 :: forall (a :: ()). Sing () data Sing (a :: Void) Instance detailsDefined in Data.Singletons.Prelude.Instances data Sing (a :: Void) data Sing (a :: All) Instance details data Sing (a :: All) whereSAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n) data Sing (a :: Any) Instance details data Sing (a :: Any) whereSAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n) data Sing (a :: Sort) Source # Instance detailsDefined in Data.Expression.Sort data Sing (a :: Sort) whereSBooleanSort :: forall (a :: Sort). Sing BooleanSortSIntegralSort :: forall (a :: Sort). Sing IntegralSortSArraySort :: forall (a :: Sort) (n :: Sort) (n :: Sort). {..} -> Sing (ArraySort n n) data Sing (b :: [a]) Instance detailsDefined in Data.Singletons.Prelude.Instances data Sing (b :: [a]) whereSNil :: 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 detailsDefined in Data.Singletons.Prelude.Instances data Sing (b :: Maybe a) whereSNothing :: 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 data Sing (b :: Min a) whereSMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n) data Sing (b :: Max a) Instance details data Sing (b :: Max a) whereSMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n) data Sing (b :: First a) Instance details data Sing (b :: First a) whereSFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n) data Sing (b :: Last a) Instance details data Sing (b :: Last a) whereSLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n) data Sing (a :: WrappedMonoid m) Instance details data Sing (a :: WrappedMonoid m) whereSWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n) data Sing (b :: Option a) Instance details data Sing (b :: Option a) whereSOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n) data Sing (b :: Identity a) Instance detailsDefined in Data.Singletons.Prelude.Instances data Sing (b :: Identity a) whereSIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n) data Sing (b :: First a) Instance detailsDefined in Data.Singletons.Prelude.Monoid data Sing (b :: First a) whereSFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n) data Sing (b :: Last a) Instance detailsDefined in Data.Singletons.Prelude.Monoid data Sing (b :: Last a) whereSLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n) data Sing (b :: Dual a) Instance details data Sing (b :: Dual a) whereSDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n) data Sing (b :: Sum a) Instance details data Sing (b :: Sum a) whereSSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n) data Sing (b :: Product a) Instance details data Sing (b :: Product a) whereSProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n) data Sing (b :: Down a) Instance detailsDefined in Data.Singletons.Prelude.Ord data Sing (b :: Down a) whereSDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n) data Sing (b :: NonEmpty a) Instance detailsDefined 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 detailsDefined in Data.Singletons.Prelude.Foldable data Sing (b :: Endo a) whereSEndo :: forall a (b :: Endo a) (x :: a ~> a). Sing x -> Sing (Endo x) data Sing (b :: MaxInternal a) Instance detailsDefined in Data.Singletons.Prelude.Foldable data Sing (b :: MaxInternal a) whereSMaxInternal :: forall a (b :: MaxInternal a) (x :: Maybe a). Sing x -> Sing (MaxInternal x) data Sing (b :: MinInternal a) Instance detailsDefined in Data.Singletons.Prelude.Foldable data Sing (b :: MinInternal a) whereSMinInternal :: forall a (b :: MinInternal a) (x :: Maybe a). Sing x -> Sing (MinInternal x) data Sing (c :: Either a b) Instance detailsDefined in Data.Singletons.Prelude.Instances data Sing (c :: Either a b) whereSLeft :: 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 detailsDefined in Data.Singletons.Prelude.Instances data Sing (c :: (a, b)) whereSTuple2 :: forall a b (c :: (a, b)) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing ((,) n1 n2) data Sing (c :: Arg a b) Instance detailsDefined in Data.Singletons.Prelude.Semigroup data Sing (c :: Arg a b) whereSArg :: forall a b (c :: Arg a b) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing (Arg n1 n2) newtype Sing (f :: k1 ~> k2) Instance detailsDefined 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) Instance detailsDefined in Data.Singletons.Prelude.Traversable data Sing (b :: StateL s a) whereSStateL :: forall s a (b :: StateL s a) (x :: s ~> (s, a)). Sing x -> Sing (StateL x) data Sing (b :: StateR s a) Instance detailsDefined in Data.Singletons.Prelude.Traversable data Sing (b :: StateR s a) whereSStateR :: forall s a (b :: StateR s a) (x :: s ~> (s, a)). Sing x -> Sing (StateR x) data Sing (d :: (a, b, c)) Instance detailsDefined in Data.Singletons.Prelude.Instances data Sing (d :: (a, b, c)) whereSTuple3 :: 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 detailsDefined in Data.Singletons.Prelude.Const data Sing (c :: Const a b) whereSConst :: 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 detailsDefined in Data.Singletons.Prelude.Instances data Sing (e :: (a, b, c, d)) whereSTuple4 :: 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 detailsDefined in Data.Singletons.Prelude.Instances data Sing (f :: (a, b, c, d, e)) whereSTuple5 :: 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 detailsDefined in Data.Singletons.Prelude.Instances data Sing (g :: (a, b, c, d, e, f)) whereSTuple6 :: 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 detailsDefined in Data.Singletons.Prelude.Instances data Sing (h :: (a, b, c, d, e, f, g)) whereSTuple7 :: 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
 Source # Instance detailsDefined in Data.Expression.Sort Methods

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 detailsDefined in Data.Expression.Sort Methods (forall (s :: Sort). Show (d s)) => Show (DynamicallySorted d) Source # Instance detailsDefined in Data.Expression.Sort MethodsshowList :: [DynamicallySorted d] -> ShowS #

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

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.