ADP.Fusion.SynVar.Split.Type

NOTE highly experimental

Documentation

data SplitType

Constructors

Fragment

Final

type family CalcSplitType splitType varTy where ...

The Arg synVar means that we probably need to rewrite the internal type resolution now!

Equations

CalcSplitType Fragment varTy = ()

CalcSplitType Final varTy = varTy

type family ArgTy argTy where ...

Should never fail?

Equations

ArgTy (z :. x) = x

newtype Split uId splitType synVar

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)

Constructors

Split

Fields

• getSplit :: synVar

Instances

SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => SplitIxCol uId True (Elm ((:!:) ls (Split sId splitType (TwITblBt arr c j x mF mB r))) i)

Associated Types

type SplitIxTy (uId :: Symbol) (True :: Bool) (Elm ((:!:) ls (Split sId splitType (TwITblBt arr c j x mF mB r))) i) :: *

Methods

splitIxCol :: Proxy Symbol uId -> Proxy Bool True -> Elm (ls :!: Split sId splitType (TwITblBt arr c j x mF mB r)) i -> SplitIxTy uId True (Elm (ls :!: Split sId splitType (TwITblBt arr c j x mF mB r)) i)

SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => SplitIxCol uId True (Elm ((:!:) ls (Split sId splitType (TwITbl m arr c j x))) i)

Associated Types

type SplitIxTy (uId :: Symbol) (True :: Bool) (Elm ((:!:) ls (Split sId splitType (TwITbl m arr c j x))) i) :: *

Methods

splitIxCol :: Proxy Symbol uId -> Proxy Bool True -> Elm (ls :!: Split sId splitType (TwITbl m arr c j x)) i -> SplitIxTy uId True (Elm (ls :!: Split sId splitType (TwITbl m arr c j x)) i)

Element ls i => Element ((:!:) ls (Split uId splitType (TwITblBt arr c j x mF mB r))) i

Associated Types

data Elm ((:!:) ls (Split uId splitType (TwITblBt arr c j x mF mB r))) i :: *

type RecElm ((:!:) ls (Split uId splitType (TwITblBt arr c j x mF mB r))) i :: *

type Arg ((:!:) ls (Split uId splitType (TwITblBt arr c j x mF mB r))) :: *

Methods

getArg :: Elm (ls :!: Split uId splitType (TwITblBt arr c j x mF mB r)) i -> Arg (ls :!: Split uId splitType (TwITblBt arr c j x mF mB r))

getIdx :: Elm (ls :!: Split uId splitType (TwITblBt arr c j x mF mB r)) i -> RunningIndex i

getElm :: Elm (ls :!: Split uId splitType (TwITblBt arr c j x mF mB r)) i -> RecElm (ls :!: Split uId splitType (TwITblBt arr c j x mF mB r)) i

Element ls i => Element ((:!:) ls (Split uId splitType (TwITbl m arr c j x))) i

Associated Types

data Elm ((:!:) ls (Split uId splitType (TwITbl m arr c j x))) i :: *

type RecElm ((:!:) ls (Split uId splitType (TwITbl m arr c j x))) i :: *

type Arg ((:!:) ls (Split uId splitType (TwITbl m arr c j x))) :: *

Methods

getArg :: Elm (ls :!: Split uId splitType (TwITbl m arr c j x)) i -> Arg (ls :!: Split uId splitType (TwITbl m arr c j x))

getIdx :: Elm (ls :!: Split uId splitType (TwITbl m arr c j x)) i -> RunningIndex i

getElm :: Elm (ls :!: Split uId splitType (TwITbl m arr c j x)) i -> RecElm (ls :!: Split uId splitType (TwITbl m arr c j x)) i

Build (Split uId splitType synVar)

Associated Types

type Stack (Split uId splitType synVar) :: *

Methods

build :: Split uId splitType synVar -> Stack (Split uId splitType synVar)

type SplitIxTy uId True (Elm ((:!:) ls (Split sId splitType (TwITblBt arr c j x mF mB r))) i)

type SplitIxTy uId True (Elm ((:!:) ls (Split sId splitType (TwITblBt arr c j x mF mB r))) i) = (:.) (SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i)) i

type SplitIxTy uId True (Elm ((:!:) ls (Split sId splitType (TwITbl m arr c j x))) i)

type SplitIxTy uId True (Elm ((:!:) ls (Split sId splitType (TwITbl m arr c j x))) i) = (:.) (SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i)) i

data Elm ((:!:) ls (Split uId splitType (TwITblBt arr c j x mF mB r)))

data Elm ((:!:) ls (Split uId splitType (TwITblBt arr c j x mF mB r))) = ElmSplitBtITbl !(Proxy Symbol uId) !(CalcSplitType splitType (x, [r])) !(RunningIndex i) !(Elm ls i) !i

data Elm ((:!:) ls (Split uId splitType (TwITbl m arr c j x)))

data Elm ((:!:) ls (Split uId splitType (TwITbl m arr c j x))) = ElmSplitITbl !(Proxy Symbol uId) !(CalcSplitType splitType x) !(RunningIndex i) !(Elm ls i) !i

type Arg ((:!:) ls (Split uId splitType (TwITblBt arr c j x mF mB r)))

type Arg ((:!:) ls (Split uId splitType (TwITblBt arr c j x mF mB r))) = (:.) (Arg ls) (CalcSplitType splitType (x, [r]))

type Arg ((:!:) ls (Split uId splitType (TwITbl m arr c j x)))

type Arg ((:!:) ls (Split uId splitType (TwITbl m arr c j x))) = (:.) (Arg ls) (CalcSplitType splitType x)

type RecElm ((:!:) ls (Split uId splitType (TwITblBt arr c j x mF mB r))) i

type RecElm ((:!:) ls (Split uId splitType (TwITblBt arr c j x mF mB r))) i = Elm ls i

type RecElm ((:!:) ls (Split uId splitType (TwITbl m arr c j x))) i

type RecElm ((:!:) ls (Split uId splitType (TwITbl m arr c j x))) i = Elm ls i

type Stack (Split uId splitType synVar)

type Stack (Split uId splitType synVar) = (:!:) S (Split uId splitType synVar)

split :: Proxy (uId :: Symbol) -> Proxy (splitType :: SplitType) -> synVar -> Split uId splitType synVar

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)

collectIx gobbles up indices that are tagged with the same symbolic identifier.

type family SameSid uId elm :: Bool where ...

Closed type family that gives us a (type) function for type symbol equality.

Equations

SameSid uId (Elm (ls :!: Split sId splitType synVar) i) = uId == sId

SameSid uId (Elm (ls :!: TermSymbol a b) i) = SameSid uId (TermSymbol a b)

SameSid uId M = False

SameSid uId (TermSymbol a (Split sId splitType synVar)) = OR (uId == sId) (SameSid uId a)

SameSid uId (Elm (ls :!: l) i) = False

type family OR a b where ...

Type-level (||)

Equations

OR False False = False

OR a b = True

class Zconcat x y where

x ++ y but for inductive tuples.

TODO move to PrimitiveArray

Minimal complete definition

zconcat

Associated Types

type Zpp x y :: *

Methods

zconcat :: x -> y -> Zpp x y

Instances

Zconcat x Z

Associated Types

type Zpp x Z :: *

Methods

zconcat :: x -> Z -> Zpp x Z

Zconcat x z => Zconcat x ((:.) z y)

Associated Types

type Zpp x ((:.) z y) :: *

Methods

zconcat :: x -> (z :. y) -> Zpp x (z :. y)

class SplitIxCol uId b e where

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.

Minimal complete definition

splitIxCol

Associated Types

type SplitIxTy uId b e :: *

Methods

splitIxCol :: Proxy uId -> Proxy b -> e -> SplitIxTy uId b e

Instances

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

Associated Types

type SplitIxTy (uId :: Symbol) (True :: Bool) (Elm ((:!:) ls (TermSymbol a b)) i) :: *

Methods

splitIxCol :: Proxy Symbol uId -> Proxy Bool True -> Elm (ls :!: TermSymbol a b) i -> SplitIxTy uId True (Elm (ls :!: TermSymbol a b) i)

SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => SplitIxCol uId True (Elm ((:!:) ls (Split sId splitType (TwITblBt arr c j x mF mB r))) i)

Associated Types

type SplitIxTy (uId :: Symbol) (True :: Bool) (Elm ((:!:) ls (Split sId splitType (TwITblBt arr c j x mF mB r))) i) :: *

Methods

splitIxCol :: Proxy Symbol uId -> Proxy Bool True -> Elm (ls :!: Split sId splitType (TwITblBt arr c j x mF mB r)) i -> SplitIxTy uId True (Elm (ls :!: Split sId splitType (TwITblBt arr c j x mF mB r)) i)

SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => SplitIxCol uId True (Elm ((:!:) ls (Split sId splitType (TwITbl m arr c j x))) i)

Associated Types

type SplitIxTy (uId :: Symbol) (True :: Bool) (Elm ((:!:) ls (Split sId splitType (TwITbl m arr c j x))) i) :: *

Methods

splitIxCol :: Proxy Symbol uId -> Proxy Bool True -> Elm (ls :!: Split sId splitType (TwITbl m arr c j x)) i -> SplitIxTy uId True (Elm (ls :!: Split sId splitType (TwITbl m arr c j x)) i)

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

Associated Types

type SplitIxTy (uId :: Symbol) (False :: Bool) (Elm ((:!:) ls l) i) :: *

Methods

splitIxCol :: Proxy Symbol uId -> Proxy Bool False -> Elm (ls :!: l) i -> SplitIxTy uId False (Elm (ls :!: l) i)

SplitIxCol uId b (Elm S i)

Associated Types

type SplitIxTy (uId :: Symbol) (b :: Bool) (Elm S i) :: *

Methods

splitIxCol :: Proxy Symbol uId -> Proxy Bool b -> Elm S i -> SplitIxTy uId b (Elm S i)

data Proxy k t :: forall k. k -> *

A concrete, poly-kinded proxy type

Constructors

Proxy

Instances

Monad (Proxy *)

Methods

(>>=) :: Proxy * a -> (a -> Proxy * b) -> Proxy * b

(>>) :: Proxy * a -> Proxy * b -> Proxy * b

return :: a -> Proxy * a

fail :: String -> Proxy * a

Functor (Proxy *)

Methods

fmap :: (a -> b) -> Proxy * a -> Proxy * b

(<$) :: a -> Proxy * b -> Proxy * a

Applicative (Proxy *)

Methods

pure :: a -> Proxy * a

(<*>) :: Proxy * (a -> b) -> Proxy * a -> Proxy * b

(*>) :: Proxy * a -> Proxy * b -> Proxy * b

(<*) :: Proxy * a -> Proxy * b -> Proxy * a

Foldable (Proxy *)

Methods

fold :: Monoid m => Proxy * m -> m

foldMap :: Monoid m => (a -> m) -> Proxy * a -> m

foldr :: (a -> b -> b) -> b -> Proxy * a -> b

foldr' :: (a -> b -> b) -> b -> Proxy * a -> b

foldl :: (b -> a -> b) -> b -> Proxy * a -> b

foldl' :: (b -> a -> b) -> b -> Proxy * a -> b

foldr1 :: (a -> a -> a) -> Proxy * a -> a

foldl1 :: (a -> a -> a) -> Proxy * a -> a

toList :: Proxy * a -> [a]

null :: Proxy * a -> Bool

length :: Proxy * a -> Int

elem :: Eq a => a -> Proxy * a -> Bool

maximum :: Ord a => Proxy * a -> a

minimum :: Ord a => Proxy * a -> a

sum :: Num a => Proxy * a -> a

product :: Num a => Proxy * a -> a

Traversable (Proxy *)

Methods

traverse :: Applicative f => (a -> f b) -> Proxy * a -> f (Proxy * b)

sequenceA :: Applicative f => Proxy * (f a) -> f (Proxy * a)

mapM :: Monad m => (a -> m b) -> Proxy * a -> m (Proxy * b)

sequence :: Monad m => Proxy * (m a) -> m (Proxy * a)

Generic1 (Proxy *)

Associated Types

type Rep1 (Proxy * :: * -> *) :: * -> *

Methods

from1 :: Proxy * a -> Rep1 (Proxy *) a

to1 :: Rep1 (Proxy *) a -> Proxy * a

Alternative (Proxy *)

Methods

empty :: Proxy * a

(<|>) :: Proxy * a -> Proxy * a -> Proxy * a

some :: Proxy * a -> Proxy * [a]

many :: Proxy * a -> Proxy * [a]

MonadPlus (Proxy *)

Methods

mzero :: Proxy * a

mplus :: Proxy * a -> Proxy * a -> Proxy * a

Eq1 (Proxy *)

Since: 4.9.0.0

Methods

liftEq :: (a -> b -> Bool) -> Proxy * a -> Proxy * b -> Bool

Ord1 (Proxy *)

Since: 4.9.0.0

Methods

liftCompare :: (a -> b -> Ordering) -> Proxy * a -> Proxy * b -> Ordering

Read1 (Proxy *)

Since: 4.9.0.0

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Proxy * a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Proxy * a]

Show1 (Proxy *)

Since: 4.9.0.0

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Proxy * a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Proxy * a] -> ShowS

Hashable1 (Proxy *)

Methods

liftHashWithSalt :: (Int -> a -> Int) -> Int -> Proxy * a -> Int

Bounded (Proxy k s)

Methods

minBound :: Proxy k s

maxBound :: Proxy k s

Enum (Proxy k s)

Methods

succ :: Proxy k s -> Proxy k s

pred :: Proxy k s -> Proxy k s

toEnum :: Int -> Proxy k s

fromEnum :: Proxy k s -> Int

enumFrom :: Proxy k s -> [Proxy k s]

enumFromThen :: Proxy k s -> Proxy k s -> [Proxy k s]

enumFromTo :: Proxy k s -> Proxy k s -> [Proxy k s]

enumFromThenTo :: Proxy k s -> Proxy k s -> Proxy k s -> [Proxy k s]

Eq (Proxy k s)

Methods

(==) :: Proxy k s -> Proxy k s -> Bool

(/=) :: Proxy k s -> Proxy k s -> Bool

Data t => Data (Proxy * t)

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Proxy * t -> c (Proxy * t)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Proxy * t)

toConstr :: Proxy * t -> Constr

dataTypeOf :: Proxy * t -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Proxy * t))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Proxy * t))

gmapT :: (forall b. Data b => b -> b) -> Proxy * t -> Proxy * t

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Proxy * t -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Proxy * t -> r

gmapQ :: (forall d. Data d => d -> u) -> Proxy * t -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Proxy * t -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Proxy * t -> m (Proxy * t)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Proxy * t -> m (Proxy * t)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Proxy * t -> m (Proxy * t)

Ord (Proxy k s)

Methods

compare :: Proxy k s -> Proxy k s -> Ordering

(<) :: Proxy k s -> Proxy k s -> Bool

(<=) :: Proxy k s -> Proxy k s -> Bool

(>) :: Proxy k s -> Proxy k s -> Bool

(>=) :: Proxy k s -> Proxy k s -> Bool

max :: Proxy k s -> Proxy k s -> Proxy k s

min :: Proxy k s -> Proxy k s -> Proxy k s

Read (Proxy k s)

Methods

readsPrec :: Int -> ReadS (Proxy k s)

readList :: ReadS [Proxy k s]

readPrec :: ReadPrec (Proxy k s)

readListPrec :: ReadPrec [Proxy k s]

Show (Proxy k s)

Methods

showsPrec :: Int -> Proxy k s -> ShowS

show :: Proxy k s -> String

showList :: [Proxy k s] -> ShowS

Ix (Proxy k s)

Methods

range :: (Proxy k s, Proxy k s) -> [Proxy k s]

index :: (Proxy k s, Proxy k s) -> Proxy k s -> Int

unsafeIndex :: (Proxy k s, Proxy k s) -> Proxy k s -> Int

inRange :: (Proxy k s, Proxy k s) -> Proxy k s -> Bool

rangeSize :: (Proxy k s, Proxy k s) -> Int

unsafeRangeSize :: (Proxy k s, Proxy k s) -> Int

Generic (Proxy k t)

Associated Types

type Rep (Proxy k t) :: * -> *

Methods

from :: Proxy k t -> Rep (Proxy k t) x

to :: Rep (Proxy k t) x -> Proxy k t

Semigroup (Proxy k s)

Methods

(<>) :: Proxy k s -> Proxy k s -> Proxy k s

sconcat :: NonEmpty (Proxy k s) -> Proxy k s

stimes :: Integral b => b -> Proxy k s -> Proxy k s

Monoid (Proxy k s)

Methods

mempty :: Proxy k s

mappend :: Proxy k s -> Proxy k s -> Proxy k s

mconcat :: [Proxy k s] -> Proxy k s

Hashable (Proxy * a)

Methods

hashWithSalt :: Int -> Proxy * a -> Int

hash :: Proxy * a -> Int

type Rep1 (Proxy *)

type Rep1 (Proxy *) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) U1)

type Rep (Proxy k t)

type Rep (Proxy k t) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) U1)