Safe Haskell	None
Language	Haskell2010

ADP.Fusion.Core.TyLvlIx

Description

Type-level indexing functionality

Synopsis

Documentation

class GetIndexGo ixTy myTy cmp where Source #

Given some complete index list ixTy and some lower-dimensional version myTy, walk down along ixTy until we have is:.i ~ ms:.m and return m.

Minimal complete definition

getIndexGo

Associated Types

type ResolvedIx ixTy myTy cmp :: * Source #

Methods

getIndexGo :: ixTy -> Proxy myTy -> Proxy cmp -> ResolvedIx ixTy myTy cmp Source #

Instances

GetIndexGo Z Z EQ Source #
Associated Types type ResolvedIx Z Z (EQ :: Ordering) :: * Source # Methods getIndexGo :: Z -> Proxy * Z -> Proxy Ordering EQ -> ResolvedIx Z Z EQ Source #
GetIndexGo (RunningIndex Z) (RunningIndex Z) EQ Source #
Associated Types type ResolvedIx (RunningIndex Z) (RunningIndex Z) (EQ :: Ordering) :: * Source # Methods getIndexGo :: RunningIndex Z -> Proxy * (RunningIndex Z) -> Proxy Ordering EQ -> ResolvedIx (RunningIndex Z) (RunningIndex Z) EQ Source #
GetIndexGo (RunningIndex ix) (RunningIndex Z) (CmpNat (ToNat (RunningIndex ix)) (ToNat (RunningIndex Z))) => GetIndexGo (RunningIndex ((:.) ix i)) (RunningIndex Z) GT Source #
Associated Types type ResolvedIx (RunningIndex ((:.) ix i)) (RunningIndex Z) (GT :: Ordering) :: * Source # Methods getIndexGo :: RunningIndex (ix :. i) -> Proxy * (RunningIndex Z) -> Proxy Ordering GT -> ResolvedIx (RunningIndex (ix :. i)) (RunningIndex Z) GT Source #
GetIndexGo (RunningIndex ix) (RunningIndex ((:.) my m)) (CmpNat (ToNat (RunningIndex ix)) (ToNat (RunningIndex ((:.) my m)))) => GetIndexGo (RunningIndex ((:.) ix i)) (RunningIndex ((:.) my m)) GT Source #
Associated Types type ResolvedIx (RunningIndex ((:.) ix i)) (RunningIndex ((:.) my m)) (GT :: Ordering) :: * Source # Methods getIndexGo :: RunningIndex (ix :. i) -> Proxy * (RunningIndex (my :. m)) -> Proxy Ordering GT -> ResolvedIx (RunningIndex (ix :. i)) (RunningIndex (my :. m)) GT Source #
GetIndexGo (RunningIndex ((:.) ix i)) (RunningIndex ((:.) my m)) EQ Source #
Associated Types type ResolvedIx (RunningIndex ((:.) ix i)) (RunningIndex ((:.) my m)) (EQ :: Ordering) :: * Source # Methods getIndexGo :: RunningIndex (ix :. i) -> Proxy * (RunningIndex (my :. m)) -> Proxy Ordering EQ -> ResolvedIx (RunningIndex (ix :. i)) (RunningIndex (my :. m)) EQ Source #
GetIndexGo ix Z (CmpNat (ToNat ix) (ToNat Z)) => GetIndexGo ((:.) ix i) Z GT Source #
Associated Types type ResolvedIx ((:.) ix i) Z (GT :: Ordering) :: * Source # Methods getIndexGo :: (ix :. i) -> Proxy * Z -> Proxy Ordering GT -> ResolvedIx (ix :. i) Z GT Source #
GetIndexGo ix ((:.) my m) (CmpNat (ToNat ix) (ToNat ((:.) my m))) => GetIndexGo ((:.) ix i) ((:.) my m) GT Source #
Associated Types type ResolvedIx ((:.) ix i) ((:.) my m) (GT :: Ordering) :: * Source # Methods getIndexGo :: (ix :. i) -> Proxy * (my :. m) -> Proxy Ordering GT -> ResolvedIx (ix :. i) (my :. m) GT Source #
GetIndexGo ((:.) ix i) ((:.) my m) EQ Source #
Associated Types type ResolvedIx ((:.) ix i) ((:.) my m) (EQ :: Ordering) :: * Source # Methods getIndexGo :: (ix :. i) -> Proxy * (my :. m) -> Proxy Ordering EQ -> ResolvedIx (ix :. i) (my :. m) EQ Source #

type GetIndex l r = GetIndexGo l r (CmpNat (ToNat l) (ToNat r)) Source #

Wrap GetIndexGo and the type-level shenanigans.

type GetIx l r = ResolvedIx l r (CmpNat (ToNat l) (ToNat r)) Source #

getIndex :: forall ixTy myTy. GetIndex ixTy myTy => ixTy -> Proxy myTy -> GetIx ixTy myTy Source #

Simplifying wrapper around getIndexGo.

type family ToNat x :: Nat Source #

Given some index structure x, return the dimensional number in Nats.

Instances

type ToNat Z Source #
type ToNat Z = 0
type ToNat (RunningIndex Z) Source #
type ToNat (RunningIndex Z) = 0
type ToNat (RunningIndex ((:.) is i)) Source #
type ToNat (RunningIndex ((:.) is i)) = (+) (ToNat (RunningIndex is)) 1
type ToNat ((:.) is i) Source #
type ToNat ((:.) is i) = (+) (ToNat is) 1