ADPfusion-0.5.2.0: Efficient, high-level dynamic programming.

Safe HaskellNone
LanguageHaskell2010

ADP.Fusion.SynVar.Split.Type

Description

NOTE highly experimental

Synopsis

Documentation

data SplitType Source #

Constructors

Fragment 
Final 

type family CalcSplitType splitType varTy where ... 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 where ... 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

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

Associated Types

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

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

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

Associated Types

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

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

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

Associated Types

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

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

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

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

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

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 Source #

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

Associated Types

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

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

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

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

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

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 Source #

Build (Split uId splitType synVar) Source # 

Associated Types

type Stack (Split uId splitType synVar) :: * Source #

Methods

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

type SplitIxTy uId True (Elm ((:!:) ls (Split sId splitType (TwITblBt arr c j x mF mB r))) i) Source # 
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) Source # 
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))) Source # 
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))) Source # 
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))) Source # 
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))) Source # 
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 Source # 
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 Source # 
type RecElm ((:!:) ls (Split uId splitType (TwITbl m arr c j x))) i = Elm ls i
type Stack (Split uId splitType synVar) 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 where ... 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 where ... 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

Minimal complete definition

zconcat

Associated Types

type Zpp x y :: * Source #

Methods

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

Instances

Zconcat x Z Source # 

Associated Types

type Zpp x Z :: * Source #

Methods

zconcat :: x -> Z -> Zpp x Z Source #

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

Associated Types

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

Methods

zconcat :: x -> (z :. y) -> Zpp 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.

Minimal complete definition

splitIxCol

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 # 

Associated Types

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

Methods

splitIxCol :: Proxy Symbol uId -> Proxy Bool True -> Elm (ls :!: TermSymbol a b) i -> SplitIxTy 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 (TwITblBt arr c j x mF mB r))) i) Source # 

Associated Types

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

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

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

Associated Types

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

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

Associated Types

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

Methods

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

SplitIxCol uId b (Elm S i) Source # 

Associated Types

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

Methods

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

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 #

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

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)