Safe Haskell	None
Language	Haskell2010

ADP.Fusion.SynVar.Split.Type

Description

NOTE highly experimental

Synopsis

Documentation

data SplitType Source

Constructors

Fragment
Final

type family CalcSplitType splitType varTy Source

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 Source

Should never fail?

Equations

ArgTy (z :. x) = x

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)

Constructors

Split
Fields getSplit :: synVar

Instances

SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => SplitIxCol uId True (Elm ((:!:) ls (Split sId splitType (Backtrack (ITbl mF arr j x) mF mB r))) i)
SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => SplitIxCol uId True (Elm ((:!:) ls (Split sId splitType (ITbl m arr j x))) i)
(Monad mB, Element ls Subword, MkStream mB ls Subword, SplitIxCol uId (SameSid uId (Elm ls Subword)) (Elm ls Subword), (~) * ((:.) (SplitIxTy uId (SameSid uId (Elm ls Subword)) (Elm ls Subword)) Subword) mix, PrimArrayOps arr ((:.) (SplitIxTy uId (SameSid uId (Elm ls Subword)) (Elm ls Subword)) Subword) x) => MkStream mB ((:!:) ls (Split uId Final (Backtrack (ITbl mF arr mix x) mF mB r))) Subword
(Monad mB, Element ls Subword, MkStream mB ls Subword) => MkStream mB ((:!:) ls (Split uId Fragment (Backtrack (ITbl mF arr j x) mF mB r))) Subword
(Monad m, Element ls Subword, MkStream m ls Subword, SplitIxCol uId (SameSid uId (Elm ls Subword)) (Elm ls Subword), (~) * ((:.) (SplitIxTy uId (SameSid uId (Elm ls Subword)) (Elm ls Subword)) Subword) mix, PrimArrayOps arr ((:.) (SplitIxTy uId (SameSid uId (Elm ls Subword)) (Elm ls Subword)) Subword) x) => MkStream m ((:!:) ls (Split uId Final (ITbl m arr mix x))) Subword
(Monad m, Element ls Subword, MkStream m ls Subword) => MkStream m ((:!:) ls (Split uId Fragment (ITbl m arr j x))) Subword
Element ls i => Element ((:!:) ls (Split uId splitType (Backtrack (ITbl mF arr j x) mF mB r))) i
Element ls i => Element ((:!:) ls (Split uId splitType (ITbl m arr j x))) i
Build (Split uId splitType synVar)
type SplitIxTy uId True (Elm ((:!:) ls (Split sId splitType (Backtrack (ITbl mF arr 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 (ITbl m arr j x))) i) = (:.) (SplitIxTy uId (SameSid uId (Elm ls i)) (Elm ls i)) i
data Elm ((:!:) ls (Split uId splitType (Backtrack (ITbl mF arr j x) mF mB r))) = ElmSplitBtITbl !(Proxy Symbol uId) !(CalcSplitType splitType (x, [r])) !i !i !(Elm ls i)
data Elm ((:!:) ls (Split uId splitType (ITbl m arr j x))) = ElmSplitITbl !(Proxy Symbol uId) !(CalcSplitType splitType x) !i !i !(Elm ls i)
type Arg ((:!:) ls (Split uId splitType (Backtrack (ITbl mF arr j x) mF mB r))) = (:.) (Arg ls) (CalcSplitType splitType (x, [r]))
type Arg ((:!:) ls (Split uId splitType (ITbl m arr j x))) = (:.) (Arg ls) (CalcSplitType splitType x)
type RecElm ((:!:) ls (Split uId splitType (Backtrack (ITbl mF arr j x) mF mB r))) i = Elm ls i
type RecElm ((:!:) ls (Split uId splitType (ITbl m arr j x))) i = Elm ls i
type Stack (Split uId splitType synVar) = (:!:) S (Split uId splitType synVar)

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

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.

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 Source

Type-level (||)

Equations

OR False False = False
OR a b = True

class Zconcat x y where Source

x ++ y but for inductive tuples.

TODO move to PrimitiveArray

Associated Types

type Zpp x y :: * Source

Methods

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

Instances

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

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

Associated Types

type SplitIxTy uId b e :: * Source

Methods

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

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)
SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => SplitIxCol uId True (Elm ((:!:) ls (Split sId splitType (Backtrack (ITbl mF arr j x) mF mB r))) i)
SplitIxCol uId (SameSid uId (Elm ls i)) (Elm ls i) => SplitIxCol uId True (Elm ((:!:) ls (Split sId splitType (ITbl m arr 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)
SplitIxCol uId b (Elm S i)

data Proxy t :: k -> *

A concrete, poly-kinded proxy type

Constructors

Proxy

Instances

Monad (Proxy *)
Functor (Proxy *)
Applicative (Proxy *)
Bounded (Proxy k s)
Enum (Proxy k s)
Eq (Proxy k s)
Data t => Data (Proxy * t)
Ord (Proxy k s)
Read (Proxy k s)
Show (Proxy k s)
Ix (Proxy k s)
Generic (Proxy * t)
Monoid (Proxy * s)
Typeable (k -> *) (Proxy k)
type Rep (Proxy k t) = D1 D1Proxy (C1 C1_0Proxy U1)