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

module Data.SOP.Index (
    -- * Indexing SOP types
    Index (.., IS, IZ)
  , 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.Proxy
import           Data.SOP.BasicFunctors
import           Data.SOP.Constraint
import           Data.SOP.Dict (Dict (..))
import           Data.SOP.Sing
import           Data.SOP.Strict
import           Data.Type.Equality ((:~:) (..))
import           Data.Word

newtype Index xs x = Index { forall {k} (xs :: [k]) (x :: k). Index xs x -> NS ((:~:) x) xs
getIndex :: NS ((:~:) x) xs }

pattern IZ ::
     ()
  => xs ~ (x ': xs1)
  => Index xs x
pattern $mIZ :: forall {r} {k} {xs :: [k]} {x :: k}.
Index xs x
-> (forall {xs1 :: [k]}. (xs ~ (x : xs1)) => r)
-> ((# #) -> r)
-> r
$bIZ :: forall {k} (xs :: [k]) (x :: k) (xs1 :: [k]).
(xs ~ (x : xs1)) =>
Index xs x
IZ = Index (Z Refl)

pattern IS ::
     ()
  => xs ~ (x' ': xs')
  => Index xs' x
  -> Index xs x
pattern $mIS :: forall {r} {k} {xs :: [k]} {x :: k}.
Index xs x
-> (forall {x' :: k} {xs' :: [k]}.
    (xs ~ (x' : xs')) =>
    Index xs' x -> r)
-> ((# #) -> r)
-> r
$bIS :: forall {k} (xs :: [k]) (x :: k) (x' :: k) (xs' :: [k]).
(xs ~ (x' : xs')) =>
Index xs' x -> Index xs x
IS z <- Index (S (Index -> z)) where
  IS (Index NS ((:~:) x) xs'
z) = NS ((:~:) x) xs -> Index xs x
forall {k} (xs :: [k]) (x :: k). NS ((:~:) x) xs -> Index xs x
Index (NS ((:~:) x) xs' -> NS ((:~:) x) (x' : xs')
forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k).
NS f xs1 -> NS f (x : xs1)
S NS ((:~:) x) xs'
z)

{-# COMPLETE IZ, IS #-}

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
forall {k} (xs :: [k]) (x :: k) (xs1 :: [k]).
(xs ~ (x : xs1)) =>
Index 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
forall (a :: k). Index xs a -> Index xs a
forall {k} (xs :: [k]) (x :: k) (x' :: k) (xs' :: [k]).
(xs ~ (x' : xs')) =>
Index xs' x -> Index xs x
IS NP (Index xs) xs
forall {k} (xs :: [k]). SListI xs => NP (Index xs) xs
indices

dictIndexAll :: forall c xs x. 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 (Index NS ((:~:) x) xs
idx) = NS (K (Dict c x)) xs -> CollapseTo NS (Dict c x)
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 (Dict c x)) xs -> CollapseTo NS (Dict c x))
-> NS (K (Dict c x)) xs -> CollapseTo NS (Dict c x)
forall a b. (a -> b) -> a -> b
$ Proxy c
-> (forall (a :: k). c a => (x :~: a) -> K (Dict c x) a)
-> NS ((:~:) x) xs
-> NS (K (Dict c x)) xs
forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap Proxy c
p (\x :~: a
Refl -> Dict c x -> K (Dict c x) a
forall k a (b :: k). a -> K a b
K Dict c x
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict) NS ((:~:) x) xs
idx

injectNS :: forall f x xs. All Top xs => Index xs x -> f x -> NS f xs
injectNS :: forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
All Top xs =>
Index xs x -> f x -> NS f xs
injectNS (Index NS ((:~:) x) xs
idx) f x
x = (forall (a :: k). (x :~: a) -> f a) -> NS ((:~:) x) xs -> NS f 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 (\x :~: a
Refl -> f x
f a
x) NS ((:~:) x) xs
idx

injectNS' ::
     forall f a b x xs. All Top 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]).
(All Top xs, 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]).
All Top xs =>
Index xs x -> f x -> NS f xs
forall (f :: k -> *) (x :: k) (xs :: [k]).
All Top xs =>
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 :: All Top xs => Index xs x -> NP f xs -> f x
projectNP :: forall {k} (xs :: [k]) (x :: k) (f :: k -> *).
All Top xs =>
Index xs x -> NP f xs -> f x
projectNP (Index NS ((:~:) x) xs
idx) NP f xs
np =
  NS (K (f x)) xs -> CollapseTo NS (f x)
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 (f x)) xs -> CollapseTo NS (f x))
-> NS (K (f x)) xs -> CollapseTo NS (f x)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). f a -> (x :~: a) -> K (f x) a)
-> Prod NS f xs -> NS ((:~:) x) xs -> NS (K (f x)) 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
hliftA2 (\f a
f x :~: a
Refl -> f x -> K (f x) a
forall k a (b :: k). a -> K a b
K f x
f a
f) Prod NS f xs
NP f xs
np NS ((:~:) x) xs
idx

{-------------------------------------------------------------------------------
  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 -> NS ((:~:) x) xs -> Word8
forall {k} (y :: k) (ys :: [k]). Word8 -> NS ((:~:) y) ys -> Word8
go Word8
0 (NS ((:~:) x) xs -> Word8)
-> (Index xs x -> NS ((:~:) x) xs) -> Index xs x -> Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index xs x -> NS ((:~:) x) xs
forall {k} (xs :: [k]) (x :: k). Index xs x -> NS ((:~:) x) xs
getIndex
  where
    go :: Word8 -> NS ((:~:) y) ys -> Word8
    go :: forall {k} (y :: k) (ys :: [k]). Word8 -> NS ((:~:) y) ys -> Word8
go !Word8
n = \case
      Z y :~: x
Refl -> Word8
n
      S NS ((:~:) y) xs1
idx  -> Word8 -> NS ((:~:) y) xs1 -> Word8
forall {k} (y :: k) (ys :: [k]). Word8 -> NS ((:~:) y) ys -> Word8
go (Word8
n Word8 -> Word8 -> Word8
forall a. Num a => a -> a -> a
+ Word8
1) NS ((:~:) y) xs1
idx