ADP.Fusion.Base.TyLvlIx

Type-level indexing functionality

Documentation

class GetIndexGo ixTy myTy cmp where

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.

Associated Types

type ResolvedIx ixTy myTy cmp :: *

Methods

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

Instances

GetIndexGo Z Z EQ

GetIndexGo (RunningIndex Z) (RunningIndex Z) EQ

GetIndexGo (RunningIndex ix) (RunningIndex Z) (CmpNat (ToNat (RunningIndex ix)) (ToNat (RunningIndex Z))) => GetIndexGo (RunningIndex ((:.) ix i)) (RunningIndex Z) GT

GetIndexGo (RunningIndex ix) (RunningIndex ((:.) my m)) (CmpNat (ToNat (RunningIndex ix)) (ToNat (RunningIndex ((:.) my m)))) => GetIndexGo (RunningIndex ((:.) ix i)) (RunningIndex ((:.) my m)) GT

GetIndexGo (RunningIndex ((:.) ix i)) (RunningIndex ((:.) my m)) EQ

GetIndexGo ix Z (CmpNat (ToNat ix) (ToNat Z)) => GetIndexGo ((:.) ix i) Z GT

GetIndexGo ix ((:.) my m) (CmpNat (ToNat ix) (ToNat ((:.) my m))) => GetIndexGo ((:.) ix i) ((:.) my m) GT

GetIndexGo ((:.) ix i) ((:.) my m) EQ

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

Wrap GetIndexGo and the type-level shenanigans.

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

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

Simplifying wrapper around getIndexGo.

type family ToNat x :: Nat

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

Instances

type ToNat Z = 0

type ToNat (RunningIndex Z) = 0

type ToNat (RunningIndex ((:.) is i)) = (+) (ToNat (RunningIndex is)) 1

type ToNat ((:.) is i) = (+) (ToNat is) 1