Safe Haskell | None |
---|---|
Language | Haskell2010 |
NOTE highly experimental
- data SplitType
- type family CalcSplitType splitType varTy
- type family ArgTy argTy
- newtype Split uId splitType synVar = Split {
- getSplit :: synVar
- split :: Proxy (uId :: Symbol) -> Proxy (splitType :: SplitType) -> synVar -> Split uId splitType synVar
- collectIx :: forall uId ls i. SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => Proxy uId -> Elm ls i -> SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i)
- type family SameSid uId elm :: Bool
- type family OR a b
- class Zconcat x y where
- class SplitIxCol uId b e where
- type SplitIxTy uId b e :: *
- splitIxCol :: Proxy uId -> Proxy b -> e -> SplitIxTy uId b e
- data Proxy t :: k -> * = Proxy
Documentation
type family CalcSplitType splitType varTy Source
The Arg synVar
means that we probably need to rewrite the internal
type resolution now!
CalcSplitType Fragment varTy = () | |
CalcSplitType Final varTy = varTy |
newtype Split uId splitType synVar Source
Wraps a normal non-terminal and attaches a type-level unique identier
and z-ordering (with the unused Z
at 0
).
TODO attach empty/non-empty stuff (or get from non-splitted synvar?)
TODO re-introduce z-ordering later (once we have a sort fun)
SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => SplitIxCol uId True (Elm ((:!:) ls (Split sId splitType (Backtrack (ITbl mF arr c j x) mF mB r))) i) Source | |
SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => SplitIxCol uId True (Elm ((:!:) ls (Split sId splitType (ITbl m arr c j x))) i) Source | |
Element ls i => Element ((:!:) ls (Split uId splitType (Backtrack (ITbl mF arr c j x) mF mB r))) i Source | |
Element ls i => Element ((:!:) ls (Split uId splitType (ITbl m arr c j x))) i Source | |
Build (Split uId splitType synVar) Source | |
type SplitIxTy uId True (Elm ((:!:) ls (Split sId splitType (Backtrack (ITbl mF arr c j x) mF mB r))) i) = (:.) (SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i)) i Source | |
type SplitIxTy uId True (Elm ((:!:) ls (Split sId splitType (ITbl m arr c j x))) i) = (:.) (SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i)) i Source | |
data Elm ((:!:) ls (Split uId splitType (Backtrack (ITbl mF arr c j x) mF mB r))) = ElmSplitBtITbl !(Proxy Symbol uId) !(CalcSplitType splitType (x, [r])) !(RunningIndex i) !(Elm ls i) Source | |
data Elm ((:!:) ls (Split uId splitType (ITbl m arr c j x))) = ElmSplitITbl !(Proxy Symbol uId) !(CalcSplitType splitType x) !(RunningIndex i) !(Elm ls i) Source | |
type Arg ((:!:) ls (Split uId splitType (Backtrack (ITbl mF arr c j x) mF mB r))) = (:.) (Arg ls) (CalcSplitType splitType (x, [r])) Source | |
type Arg ((:!:) ls (Split uId splitType (ITbl m arr c j x))) = (:.) (Arg ls) (CalcSplitType splitType x) Source | |
type RecElm ((:!:) ls (Split uId splitType (Backtrack (ITbl mF arr c j x) mF mB r))) i = Elm ls i Source | |
type RecElm ((:!:) ls (Split uId splitType (ITbl m arr c j x))) i = Elm ls i Source | |
type Stack (Split uId splitType synVar) = (:!:) S (Split uId splitType synVar) |
split :: Proxy (uId :: Symbol) -> Proxy (splitType :: SplitType) -> synVar -> Split uId splitType synVar Source
TODO Here, we probably want to default to a NonEmpty
condition. Or at
least have different versions of split
.
collectIx :: forall uId ls i. SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => Proxy uId -> Elm ls i -> SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i) Source
collectIx
gobbles up indices that are tagged with the same symbolic
identifier.
type family SameSid uId elm :: Bool Source
Closed type family that gives us a (type) function for type symbol equality.
class SplitIxCol uId b e where Source
Actually collect split indices based on if we managed to find the
right Split
synvar (based on the right symbol).
TODO this is not completely right, or? Since we should consider inside/outside?
TODO splitIxCol
will need the index type i
to combine running index
and index into the actual lookup part.
splitIxCol :: Proxy uId -> Proxy b -> e -> SplitIxTy uId b e Source
(SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i), Zconcat (SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i)) (SplitIxTy uId (SameSid uId (TermSymbol a b)) (TermSymbol a b))) => SplitIxCol uId True (Elm ((:!:) ls (TermSymbol a b)) i) Source | |
SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => SplitIxCol uId True (Elm ((:!:) ls (Split sId splitType (Backtrack (ITbl mF arr c j x) mF mB r))) i) Source | |
SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => SplitIxCol uId True (Elm ((:!:) ls (Split sId splitType (ITbl m arr c j x))) i) Source | |
(SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i), Element ((:!:) ls l) i, (~) * (RecElm ((:!:) ls l) i) (Elm ls i)) => SplitIxCol uId False (Elm ((:!:) ls l) i) Source | |
SplitIxCol uId b (Elm S i) Source |
data Proxy t :: k -> *
A concrete, poly-kinded proxy type
Monad (Proxy *) | |
Functor (Proxy *) | |
Applicative (Proxy *) | |
Foldable (Proxy *) | |
Traversable (Proxy *) | |
Bounded (Proxy k s) | |
Enum (Proxy k s) | |
Eq (Proxy k s) | |
Ord (Proxy k s) | |
Read (Proxy k s) | |
Show (Proxy k s) | |
Ix (Proxy k s) | |
Generic (Proxy * t) | |
Monoid (Proxy k s) | |
type Rep (Proxy k t) = D1 D1Proxy (C1 C1_0Proxy U1) |