{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Data.SOP.Index (
    -- * Indexing SOP types
    Index (..)
  , dictIndexAll
  , indices
  , injectNS
  , injectNS'
  , projectNP
    -- * Zipping with indices
  , hcimap
  , hcizipWith
  , hcizipWith3
  , hcizipWith4
  , himap
  , hizipWith
  , hizipWith3
  , hizipWith4
    -- * Indices with Word
  , npWithIndices
  , nsFromIndex
  , nsToIndex
  , toWord8
  ) where

import           Data.Coerce
import           Data.Kind (Type)
import           Data.Proxy
import           Data.SOP.BasicFunctors
import           Data.SOP.Constraint
import           Data.SOP.Dict (Dict (..))
import           Data.SOP.Sing
import           Data.SOP.Strict
import           Data.Word

type Index :: [k] -> k -> Type
data Index xs x where
  IZ ::               Index (x ': xs) x
  IS :: Index xs x -> Index (y ': xs) x

indices :: forall xs. SListI xs => NP (Index xs) xs
indices :: forall {k} (xs :: [k]). SListI xs => NP (Index xs) xs
indices = case forall (xs :: [k]). SListI xs => SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList @xs of
    SList xs
SNil  -> NP (Index xs) xs
NP (Index xs) '[]
forall {k} (f :: k -> *). NP f '[]
Nil
    SList xs
SCons -> Index xs x
Index (x : xs) x
forall {k} (x :: k) (xs :: [k]). Index (x : xs) x
IZ Index xs x -> NP (Index xs) xs -> NP (Index xs) (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* (forall (a :: k). Index xs a -> Index xs a)
-> NP (Index xs) xs -> NP (Index xs) xs
forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap Index xs a -> Index xs a
Index xs a -> Index (x : xs) a
forall (a :: k). Index xs a -> Index xs a
forall {k} (xs :: [k]) (x :: k) (y :: k).
Index xs x -> Index (y : xs) x
IS NP (Index xs) xs
forall {k} (xs :: [k]). SListI xs => NP (Index xs) xs
indices

dictIndexAll :: All c xs => Proxy c -> Index xs x -> Dict c x
dictIndexAll :: forall {k} (c :: k -> Constraint) (xs :: [k]) (x :: k).
All c xs =>
Proxy c -> Index xs x -> Dict c x
dictIndexAll Proxy c
p = \case
    Index xs x
IZ      -> Dict c x
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    IS Index xs x
idx' -> Proxy c -> Index xs x -> Dict c x
forall {k} (c :: k -> Constraint) (xs :: [k]) (x :: k).
All c xs =>
Proxy c -> Index xs x -> Dict c x
dictIndexAll Proxy c
p Index xs x
idx'

injectNS :: forall f x xs. Index xs x -> f x -> NS f xs
injectNS :: forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
Index xs x -> f x -> NS f xs
injectNS Index xs x
idx f x
x = case Index xs x
idx of
    Index xs x
IZ      -> f x -> NS f (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NS f (x : xs1)
Z f x
x
    IS Index xs x
idx' -> NS f xs -> NS f (y : xs)
forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k).
NS f xs1 -> NS f (x : xs1)
S (Index xs x -> f x -> NS f xs
forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
Index xs x -> f x -> NS f xs
injectNS Index xs x
idx' f x
x)

injectNS' ::
     forall f a b x xs. (Coercible a (f x), Coercible b (NS f xs))
  => Proxy f -> Index xs x -> a -> b
injectNS' :: forall {k} (f :: k -> *) a b (x :: k) (xs :: [k]).
(Coercible a (f x), Coercible b (NS f xs)) =>
Proxy f -> Index xs x -> a -> b
injectNS' Proxy f
_ Index xs x
idx = NS f xs -> b
forall a b. Coercible a b => a -> b
coerce (NS f xs -> b) -> (a -> NS f xs) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
Index xs x -> f x -> NS f xs
forall (f :: k -> *) (x :: k) (xs :: [k]).
Index xs x -> f x -> NS f xs
injectNS @f Index xs x
idx (f x -> NS f xs) -> (a -> f x) -> a -> NS f xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f x
forall a b. Coercible a b => a -> b
coerce

projectNP :: Index xs x -> NP f xs -> f x
projectNP :: forall {k} (xs :: [k]) (x :: k) (f :: k -> *).
Index xs x -> NP f xs -> f x
projectNP Index xs x
IZ       (f x
x :* NP f xs1
_ ) = f x
f x
x
projectNP (IS Index xs x
idx) (f x
_ :* NP f xs1
xs) = Index xs x -> NP f xs -> f x
forall {k} (xs :: [k]) (x :: k) (f :: k -> *).
Index xs x -> NP f xs -> f x
projectNP Index xs x
idx NP f xs
NP f xs1
xs

{-------------------------------------------------------------------------------
  Zipping with indices
-------------------------------------------------------------------------------}

hcimap ::
     (HAp h, All c xs, Prod h ~ NP)
  => proxy c
  -> (forall a. c a => Index xs a -> f1 a -> f2 a)
  -> h f1 xs
  -> h f2 xs
hcimap :: forall {k} (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *)
       (f2 :: k -> *).
(HAp h, All c xs, Prod h ~ NP) =>
proxy c
-> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a)
-> h f1 xs
-> h f2 xs
hcimap proxy c
p forall (a :: k). c a => Index xs a -> f1 a -> f2 a
f h f1 xs
xs1 =
    proxy c
-> (forall (a :: k). c a => (-.->) (Index xs) (f1 -.-> f2) a)
-> NP (Index xs -.-> (f1 -.-> f2)) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
forall (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
AllN NP c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
hcpure proxy c
p ((Index xs a -> f1 a -> f2 a) -> (-.->) (Index xs) (f1 -.-> f2) a
forall {k} (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *).
(f a -> f' a -> f'' a) -> (-.->) f (f' -.-> f'') a
fn_2 Index xs a -> f1 a -> f2 a
forall (a :: k). c a => Index xs a -> f1 a -> f2 a
f)
      Prod NP (Index xs -.-> (f1 -.-> f2)) xs
-> NP (Index xs) xs -> NP (f1 -.-> f2) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
`hap` NP (Index xs) xs
forall {k} (xs :: [k]). SListI xs => NP (Index xs) xs
indices
      Prod h (f1 -.-> f2) xs -> h f1 xs -> h f2 xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f1 xs
xs1

himap ::
     (HAp h, SListI xs, Prod h ~ NP)
  => (forall a. Index xs a -> f1 a -> f2 a)
  -> h f1 xs
  -> h f2 xs
himap :: forall {k} (h :: (k -> *) -> [k] -> *) (xs :: [k]) (f1 :: k -> *)
       (f2 :: k -> *).
(HAp h, SListI xs, Prod h ~ NP) =>
(forall (a :: k). Index xs a -> f1 a -> f2 a) -> h f1 xs -> h f2 xs
himap = Proxy Top
-> (forall (a :: k). Top a => Index xs a -> f1 a -> f2 a)
-> h f1 xs
-> h f2 xs
forall {k} (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *)
       (f2 :: k -> *).
(HAp h, All c xs, Prod h ~ NP) =>
proxy c
-> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a)
-> h f1 xs
-> h f2 xs
hcimap (forall {k} (t :: k). Proxy t
forall (t :: k -> Constraint). Proxy t
Proxy @Top)

hcizipWith ::
     (HAp h, All c xs, Prod h ~ NP)
  => proxy c
  -> (forall a. c a => Index xs a -> f1 a -> f2 a -> f3 a)
  -> NP f1 xs
  -> h  f2 xs
  -> h  f3 xs
hcizipWith :: forall {k} (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *)
       (f2 :: k -> *) (f3 :: k -> *).
(HAp h, All c xs, Prod h ~ NP) =>
proxy c
-> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a)
-> NP f1 xs
-> h f2 xs
-> h f3 xs
hcizipWith proxy c
p forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a
f NP f1 xs
xs1 h f2 xs
xs2 =
    proxy c
-> (forall (a :: k).
    c a =>
    (-.->) (Index xs) (f1 -.-> (f2 -.-> f3)) a)
-> NP (Index xs -.-> (f1 -.-> (f2 -.-> f3))) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
forall (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
AllN NP c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
hcpure proxy c
p ((Index xs a -> f1 a -> f2 a -> f3 a)
-> (-.->) (Index xs) (f1 -.-> (f2 -.-> f3)) a
forall {k} (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *)
       (f''' :: k -> *).
(f a -> f' a -> f'' a -> f''' a)
-> (-.->) f (f' -.-> (f'' -.-> f''')) a
fn_3 Index xs a -> f1 a -> f2 a -> f3 a
forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a
f)
      Prod NP (Index xs -.-> (f1 -.-> (f2 -.-> f3))) xs
-> NP (Index xs) xs -> NP (f1 -.-> (f2 -.-> f3)) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
`hap` NP (Index xs) xs
forall {k} (xs :: [k]). SListI xs => NP (Index xs) xs
indices
      Prod NP (f1 -.-> (f2 -.-> f3)) xs -> NP f1 xs -> NP (f2 -.-> f3) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
`hap` NP f1 xs
xs1
      Prod h (f2 -.-> f3) xs -> h f2 xs -> h f3 xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f2 xs
xs2

hizipWith ::
     (HAp h, SListI xs, Prod h ~ NP)
  => (forall a. Index xs a -> f1 a -> f2 a -> f3 a)
  -> NP f1 xs
  -> h  f2 xs
  -> h  f3 xs
hizipWith :: forall {k} (h :: (k -> *) -> [k] -> *) (xs :: [k]) (f1 :: k -> *)
       (f2 :: k -> *) (f3 :: k -> *).
(HAp h, SListI xs, Prod h ~ NP) =>
(forall (a :: k). Index xs a -> f1 a -> f2 a -> f3 a)
-> NP f1 xs -> h f2 xs -> h f3 xs
hizipWith = Proxy Top
-> (forall (a :: k). Top a => Index xs a -> f1 a -> f2 a -> f3 a)
-> NP f1 xs
-> h f2 xs
-> h f3 xs
forall {k} (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *)
       (f2 :: k -> *) (f3 :: k -> *).
(HAp h, All c xs, Prod h ~ NP) =>
proxy c
-> (forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a)
-> NP f1 xs
-> h f2 xs
-> h f3 xs
hcizipWith (forall {k} (t :: k). Proxy t
forall (t :: k -> Constraint). Proxy t
Proxy @Top)

hcizipWith3 ::
     (HAp h, All c xs, Prod h ~ NP)
  => proxy c
  -> (forall a. c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
  -> NP f1 xs
  -> NP f2 xs
  -> h  f3 xs
  -> h  f4 xs
hcizipWith3 :: forall {k} (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *)
       (f2 :: k -> *) (f3 :: k -> *) (f4 :: k -> *).
(HAp h, All c xs, Prod h ~ NP) =>
proxy c
-> (forall (a :: k).
    c a =>
    Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
-> NP f1 xs
-> NP f2 xs
-> h f3 xs
-> h f4 xs
hcizipWith3 proxy c
p forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a
f NP f1 xs
xs1 NP f2 xs
xs2 h f3 xs
xs3 =
    proxy c
-> (forall (a :: k).
    c a =>
    (-.->) (Index xs) (f1 -.-> (f2 -.-> (f3 -.-> f4))) a)
-> NP (Index xs -.-> (f1 -.-> (f2 -.-> (f3 -.-> f4)))) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
forall (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
AllN NP c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
hcpure proxy c
p ((Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
-> (-.->) (Index xs) (f1 -.-> (f2 -.-> (f3 -.-> f4))) a
forall {k} (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *)
       (f''' :: k -> *) (f'''' :: k -> *).
(f a -> f' a -> f'' a -> f''' a -> f'''' a)
-> (-.->) f (f' -.-> (f'' -.-> (f''' -.-> f''''))) a
fn_4 Index xs a -> f1 a -> f2 a -> f3 a -> f4 a
forall (a :: k). c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a
f)
      Prod NP (Index xs -.-> (f1 -.-> (f2 -.-> (f3 -.-> f4)))) xs
-> NP (Index xs) xs -> NP (f1 -.-> (f2 -.-> (f3 -.-> f4))) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
`hap` NP (Index xs) xs
forall {k} (xs :: [k]). SListI xs => NP (Index xs) xs
indices
      Prod NP (f1 -.-> (f2 -.-> (f3 -.-> f4))) xs
-> NP f1 xs -> NP (f2 -.-> (f3 -.-> f4)) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
`hap` NP f1 xs
xs1
      Prod NP (f2 -.-> (f3 -.-> f4)) xs -> NP f2 xs -> NP (f3 -.-> f4) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
`hap` NP f2 xs
xs2
      Prod h (f3 -.-> f4) xs -> h f3 xs -> h f4 xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f3 xs
xs3

hizipWith3 ::
     (HAp h, SListI xs, Prod h ~ NP)
  => (forall a. Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
  -> NP f1 xs
  -> NP f2 xs
  -> h  f3 xs
  -> h  f4 xs
hizipWith3 :: forall {k} (h :: (k -> *) -> [k] -> *) (xs :: [k]) (f1 :: k -> *)
       (f2 :: k -> *) (f3 :: k -> *) (f4 :: k -> *).
(HAp h, SListI xs, Prod h ~ NP) =>
(forall (a :: k). Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
-> NP f1 xs -> NP f2 xs -> h f3 xs -> h f4 xs
hizipWith3 = Proxy Top
-> (forall (a :: k).
    Top a =>
    Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
-> NP f1 xs
-> NP f2 xs
-> h f3 xs
-> h f4 xs
forall {k} (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *)
       (f2 :: k -> *) (f3 :: k -> *) (f4 :: k -> *).
(HAp h, All c xs, Prod h ~ NP) =>
proxy c
-> (forall (a :: k).
    c a =>
    Index xs a -> f1 a -> f2 a -> f3 a -> f4 a)
-> NP f1 xs
-> NP f2 xs
-> h f3 xs
-> h f4 xs
hcizipWith3 (forall {k} (t :: k). Proxy t
forall (t :: k -> Constraint). Proxy t
Proxy @Top)

hcizipWith4 ::
     (HAp h, All c xs, Prod h ~ NP)
  => proxy c
  -> (forall a. c a => Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
  -> NP f1 xs
  -> NP f2 xs
  -> NP f3 xs
  -> h  f4 xs
  -> h  f5 xs
hcizipWith4 :: forall {k} (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *)
       (f2 :: k -> *) (f3 :: k -> *) (f4 :: k -> *) (f5 :: k -> *).
(HAp h, All c xs, Prod h ~ NP) =>
proxy c
-> (forall (a :: k).
    c a =>
    Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
-> NP f1 xs
-> NP f2 xs
-> NP f3 xs
-> h f4 xs
-> h f5 xs
hcizipWith4 proxy c
p forall (a :: k).
c a =>
Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a
f NP f1 xs
xs1 NP f2 xs
xs2 NP f3 xs
xs3 h f4 xs
xs4 =
    proxy c
-> (forall (a :: k).
    c a =>
    (-.->) (Index xs) (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a)
-> NP (Index xs -.-> (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5))))) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
forall (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
AllN NP c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
hcpure proxy c
p ((Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
-> (-.->) (Index xs) (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a
forall {k} (f0 :: k -> *) (a :: k) (f1 :: k -> *) (f2 :: k -> *)
       (f3 :: k -> *) (f4 :: k -> *) (f5 :: k -> *).
(f0 a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
-> (-.->) f0 (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) a
fn_5 Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a
forall (a :: k).
c a =>
Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a
f)
      Prod
  NP (Index xs -.-> (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5))))) xs
-> NP (Index xs) xs
-> NP (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
`hap` NP (Index xs) xs
forall {k} (xs :: [k]). SListI xs => NP (Index xs) xs
indices
      Prod NP (f1 -.-> (f2 -.-> (f3 -.-> (f4 -.-> f5)))) xs
-> NP f1 xs -> NP (f2 -.-> (f3 -.-> (f4 -.-> f5))) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
`hap` NP f1 xs
xs1
      Prod NP (f2 -.-> (f3 -.-> (f4 -.-> f5))) xs
-> NP f2 xs -> NP (f3 -.-> (f4 -.-> f5)) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
`hap` NP f2 xs
xs2
      Prod NP (f3 -.-> (f4 -.-> f5)) xs -> NP f3 xs -> NP (f4 -.-> f5) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
`hap` NP f3 xs
xs3
      Prod h (f4 -.-> f5) xs -> h f4 xs -> h f5 xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f4 xs
xs4

hizipWith4 ::
     (HAp h, SListI xs, Prod h ~ NP)
  => (forall a. Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
  -> NP f1 xs
  -> NP f2 xs
  -> NP f3 xs
  -> h  f4 xs
  -> h  f5 xs
hizipWith4 :: forall {k} (h :: (k -> *) -> [k] -> *) (xs :: [k]) (f1 :: k -> *)
       (f2 :: k -> *) (f3 :: k -> *) (f4 :: k -> *) (f5 :: k -> *).
(HAp h, SListI xs, Prod h ~ NP) =>
(forall (a :: k).
 Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
-> NP f1 xs -> NP f2 xs -> NP f3 xs -> h f4 xs -> h f5 xs
hizipWith4 = Proxy Top
-> (forall (a :: k).
    Top a =>
    Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
-> NP f1 xs
-> NP f2 xs
-> NP f3 xs
-> h f4 xs
-> h f5 xs
forall {k} (h :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f1 :: k -> *)
       (f2 :: k -> *) (f3 :: k -> *) (f4 :: k -> *) (f5 :: k -> *).
(HAp h, All c xs, Prod h ~ NP) =>
proxy c
-> (forall (a :: k).
    c a =>
    Index xs a -> f1 a -> f2 a -> f3 a -> f4 a -> f5 a)
-> NP f1 xs
-> NP f2 xs
-> NP f3 xs
-> h f4 xs
-> h f5 xs
hcizipWith4 (forall {k} (t :: k). Proxy t
forall (t :: k -> Constraint). Proxy t
Proxy @Top)

{-------------------------------------------------------------------------------
 Indices with Word
-------------------------------------------------------------------------------}

-- | We only allow up to 23 (so counting from 0, 24 elements in @xs@), because
-- CBOR stores a 'Word8' in the range 0-23 as a single byte equal to the value
-- of the 'Word8'.
npWithIndices :: SListI xs => NP (K Word8) xs
npWithIndices :: forall {k} (xs :: [k]). SListI xs => NP (K Word8) xs
npWithIndices = Word8 -> SList xs -> NP (K Word8) xs
forall {k} (xs' :: [k]). Word8 -> SList xs' -> NP (K Word8) xs'
go Word8
0 SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: Word8 -> SList xs' -> NP (K Word8) xs'
    go :: forall {k} (xs' :: [k]). Word8 -> SList xs' -> NP (K Word8) xs'
go !Word8
_ SList xs'
SNil  = NP (K Word8) xs'
NP (K Word8) '[]
forall {k} (f :: k -> *). NP f '[]
Nil
    go Word8
24 SList xs'
SCons = [Char] -> NP (K Word8) xs'
forall a. HasCallStack => [Char] -> a
error [Char]
"npWithIndices out of range"
    go !Word8
i SList xs'
SCons = Word8 -> K Word8 x
forall k a (b :: k). a -> K a b
K Word8
i K Word8 x -> NP (K Word8) xs -> NP (K Word8) (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* Word8 -> SList xs -> NP (K Word8) xs
forall {k} (xs' :: [k]). Word8 -> SList xs' -> NP (K Word8) xs'
go (Word8
i Word8 -> Word8 -> Word8
forall a. Num a => a -> a -> a
+ Word8
1) SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList

nsToIndex :: SListI xs => NS f xs -> Word8
nsToIndex :: forall {k} (xs :: [k]) (f :: k -> *). SListI xs => NS f xs -> Word8
nsToIndex = NS (K Word8) xs -> Word8
NS (K Word8) xs -> CollapseTo NS Word8
forall (xs :: [k]) a.
SListIN NS xs =>
NS (K a) xs -> CollapseTo NS a
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse (NS (K Word8) xs -> Word8)
-> (NS f xs -> NS (K Word8) xs) -> NS f xs -> Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). K Word8 a -> f a -> K Word8 a)
-> Prod NS (K Word8) xs -> NS f xs -> NS (K Word8) xs
forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith K Word8 a -> f a -> K Word8 a
forall (a :: k). K Word8 a -> f a -> K Word8 a
forall a b. a -> b -> a
const Prod NS (K Word8) xs
NP (K Word8) xs
forall {k} (xs :: [k]). SListI xs => NP (K Word8) xs
npWithIndices

-- | We only allow up to 23, see 'npWithIndices'.
nsFromIndex :: SListI xs => Word8 -> Maybe (NS (K ()) xs)
nsFromIndex :: forall {k} (xs :: [k]). SListI xs => Word8 -> Maybe (NS (K ()) xs)
nsFromIndex Word8
n = Word8 -> SList xs -> Maybe (NS (K ()) xs)
forall {k} (xs' :: [k]).
Word8 -> SList xs' -> Maybe (NS (K ()) xs')
go Word8
0 SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: Word8 -> SList xs' -> Maybe (NS (K ()) xs')
    go :: forall {k} (xs' :: [k]).
Word8 -> SList xs' -> Maybe (NS (K ()) xs')
go !Word8
i SList xs'
SCons
      | Word8
i Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
24   = [Char] -> Maybe (NS (K ()) xs')
forall a. HasCallStack => [Char] -> a
error [Char]
"nsFromIndex out of range"
      | Word8
i Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
n    = NS (K ()) xs' -> Maybe (NS (K ()) xs')
forall a. a -> Maybe a
Just (NS (K ()) xs' -> Maybe (NS (K ()) xs'))
-> NS (K ()) xs' -> Maybe (NS (K ()) xs')
forall a b. (a -> b) -> a -> b
$ K () x -> NS (K ()) (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NS f (x : xs1)
Z (K () x -> NS (K ()) (x : xs)) -> K () x -> NS (K ()) (x : xs)
forall a b. (a -> b) -> a -> b
$ () -> K () x
forall k a (b :: k). a -> K a b
K ()
      | Bool
otherwise = NS (K ()) xs -> NS (K ()) xs'
NS (K ()) xs -> NS (K ()) (x : xs)
forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k).
NS f xs1 -> NS f (x : xs1)
S (NS (K ()) xs -> NS (K ()) xs')
-> Maybe (NS (K ()) xs) -> Maybe (NS (K ()) xs')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Word8 -> SList xs -> Maybe (NS (K ()) xs)
forall {k} (xs' :: [k]).
Word8 -> SList xs' -> Maybe (NS (K ()) xs')
go (Word8
i Word8 -> Word8 -> Word8
forall a. Num a => a -> a -> a
+ Word8
1) SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList
    go !Word8
_ SList xs'
SNil    = Maybe (NS (K ()) xs')
forall a. Maybe a
Nothing

toWord8 :: Index xs x -> Word8
toWord8 :: forall {k} (xs :: [k]) (x :: k). Index xs x -> Word8
toWord8 = Word8 -> Index xs x -> Word8
forall {k} (ys :: [k]) (y :: k). Word8 -> Index ys y -> Word8
go Word8
0
  where
    go :: Word8 -> Index ys y -> Word8
    go :: forall {k} (ys :: [k]) (y :: k). Word8 -> Index ys y -> Word8
go !Word8
n = \case
      Index ys y
IZ      -> Word8
n
      IS Index xs y
idx' -> Word8 -> Index xs y -> Word8
forall {k} (ys :: [k]) (y :: k). Word8 -> Index ys y -> Word8
go (Word8
n Word8 -> Word8 -> Word8
forall a. Num a => a -> a -> a
+ Word8
1) Index xs y
idx'