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

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 Source
Zconcat x z => Zconcat x ((:.) z y) Source

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.

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

Constructors

Proxy

Instances

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)