Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Constraints for some typed instructions we share accross a few places and related type-level helpers.
Synopsis
- type ConstraintDUPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerOrSameLength inp n, (n > 'Z) ~ 'True, inp ~ (LazyTake (Decrement n) inp ++ (a ': Drop n inp)), out ~ (a ': inp))
- type ConstraintDUPN n inp out a = ConstraintDUPN' T n inp out a
- type ConstraintDIPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (s :: [kind]) (s' :: [kind]) = (RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ inp, (LazyTake n inp ++ s') ~ out, s ~ Drop n inp, s' ~ Drop n out)
- type ConstraintDIPN n inp out s s' = ConstraintDIPN' T n inp out s s'
- type ConstraintDIG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerThan inp n, out ~ (a ': (LazyTake n inp ++ Drop ('S n) inp)), inp ~ (LazyTake n (Drop ('S 'Z) out) ++ (a ': Drop ('S n) out)))
- type ConstraintDIG n inp out a = ConstraintDIG' T n inp out a
- type ConstraintDUG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = ConstraintDIG' kind n out inp a
- type ConstraintDUG n inp out a = ConstraintDUG' T n inp out a
- type ConstraintPairN (n :: Peano) (inp :: [T]) = (RequireLongerOrSameLength inp n, FailUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n \8805 2"))
- type ConstraintUnpairN (n :: Peano) (pair :: T) = (FailUnless (n >= ToPeano 2) ('Text "'UNPAIR n' expects n \8805 2"), FailUnless (CombedPairLeafCountIsAtLeast n pair) (If (IsPair pair) ((((('Text "'UNPAIR " :<>: 'ShowType (FromPeano n)) :<>: 'Text "' expects a right-combed pair with at least ") :<>: 'ShowType (FromPeano n)) :<>: 'Text " elements at the top of the stack,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairLeafCount pair))) :<>: 'Text " elements.")) ('Text "Expected a pair at the top of the stack, but found: " :<>: 'ShowType pair)))
- type ConstraintGetN (ix :: Peano) (pair :: T) = FailUnless (CombedPairNodeIndexIsValid ix pair) (If (IsPair pair) ((((('Text "'GET " :<>: 'ShowType (FromPeano ix)) :<>: 'Text "' expects a right-combed pair with at least ") :<>: 'ShowType (FromPeano ix + 1)) :<>: 'Text " nodes at the top of the stack,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairNodeCount pair))) :<>: 'Text " nodes.")) ('Text "Expected a pair at the top of the stack, but found: " :<>: 'ShowType pair))
- type ConstraintUpdateN (ix :: Peano) (pair :: T) = FailUnless (CombedPairNodeIndexIsValid ix pair) (If (IsPair pair) ((((('Text "'UPDATE " :<>: 'ShowType (FromPeano ix)) :<>: 'Text "' expects the 2nd element of the stack to be a right-combed pair with at least ") :<>: 'ShowType (FromPeano ix + 1)) :<>: 'Text " nodes,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairNodeCount pair))) :<>: 'Text " nodes.")) ('Text "Expected the 2nd element of the stack to be a pair, but found: " :<>: 'ShowType pair))
- type PairN (n :: Peano) (s :: [T]) = RightComb (LazyTake n s) ': Drop n s
- type family UnpairN (n :: Peano) (s :: T) :: [T] where ...
- type family UpdateN (ix :: Peano) (val :: T) (pair :: T) :: T where ...
- type family GetN (ix :: Peano) (pair :: T) :: T where ...
- type family RightComb (s :: [T]) :: T where ...
Documentation
type ConstraintDUPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerOrSameLength inp n, (n > 'Z) ~ 'True, inp ~ (LazyTake (Decrement n) inp ++ (a ': Drop n inp)), out ~ (a ': inp)) Source #
Constraint that is used in DUPN, we want to share it with typechecking code and eDSL code.
type ConstraintDUPN n inp out a = ConstraintDUPN' T n inp out a Source #
type ConstraintDIPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (s :: [kind]) (s' :: [kind]) = (RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ inp, (LazyTake n inp ++ s') ~ out, s ~ Drop n inp, s' ~ Drop n out) Source #
Constraint that is used in DIPN, we want to share it with typechecking code and eDSL code.
type ConstraintDIPN n inp out s s' = ConstraintDIPN' T n inp out s s' Source #
type ConstraintDIG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (RequireLongerThan inp n, out ~ (a ': (LazyTake n inp ++ Drop ('S n) inp)), inp ~ (LazyTake n (Drop ('S 'Z) out) ++ (a ': Drop ('S n) out))) Source #
Constraint that is used in DIG, we want to share it with typechecking code and eDSL code.
type ConstraintDIG n inp out a = ConstraintDIG' T n inp out a Source #
type ConstraintDUG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = ConstraintDIG' kind n out inp a Source #
Constraint that is used in DUG, we want to share it with typechecking code and eDSL code.
type ConstraintDUG n inp out a = ConstraintDUG' T n inp out a Source #
type ConstraintPairN (n :: Peano) (inp :: [T]) = (RequireLongerOrSameLength inp n, FailUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n \8805 2")) Source #
type ConstraintUnpairN (n :: Peano) (pair :: T) = (FailUnless (n >= ToPeano 2) ('Text "'UNPAIR n' expects n \8805 2"), FailUnless (CombedPairLeafCountIsAtLeast n pair) (If (IsPair pair) ((((('Text "'UNPAIR " :<>: 'ShowType (FromPeano n)) :<>: 'Text "' expects a right-combed pair with at least ") :<>: 'ShowType (FromPeano n)) :<>: 'Text " elements at the top of the stack,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairLeafCount pair))) :<>: 'Text " elements.")) ('Text "Expected a pair at the top of the stack, but found: " :<>: 'ShowType pair))) Source #
type ConstraintGetN (ix :: Peano) (pair :: T) = FailUnless (CombedPairNodeIndexIsValid ix pair) (If (IsPair pair) ((((('Text "'GET " :<>: 'ShowType (FromPeano ix)) :<>: 'Text "' expects a right-combed pair with at least ") :<>: 'ShowType (FromPeano ix + 1)) :<>: 'Text " nodes at the top of the stack,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairNodeCount pair))) :<>: 'Text " nodes.")) ('Text "Expected a pair at the top of the stack, but found: " :<>: 'ShowType pair)) Source #
type ConstraintUpdateN (ix :: Peano) (pair :: T) = FailUnless (CombedPairNodeIndexIsValid ix pair) (If (IsPair pair) ((((('Text "'UPDATE " :<>: 'ShowType (FromPeano ix)) :<>: 'Text "' expects the 2nd element of the stack to be a right-combed pair with at least ") :<>: 'ShowType (FromPeano ix + 1)) :<>: 'Text " nodes,") :$$: (('Text "but the pair only contains " :<>: 'ShowType (FromPeano (CombedPairNodeCount pair))) :<>: 'Text " nodes.")) ('Text "Expected the 2nd element of the stack to be a pair, but found: " :<>: 'ShowType pair)) Source #
Helpers
type family UnpairN (n :: Peano) (s :: T) :: [T] where ... Source #
Splits a right-combed pair into n
elements.
UnpairN (ToPeano 3) ('TPair 'TInt ('TPair 'TString 'TUnit)) ~ '[ 'TInt, 'TString, 'TUnit]
UnpairN (ToPeano 3) ('TPair 'TInt ('TPair 'TString ('TPair 'TUnit 'TInt))) ~ '[ 'TInt, 'TString, 'TPair 'TUnit 'TInt]
type family UpdateN (ix :: Peano) (val :: T) (pair :: T) :: T where ... Source #
Update the node at index ix
of a right-combed pair.