{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

module Control.Comonad.Travel.NonEmpty(
  fromNonEmpty, toNonEmpty
) where

import Control.Category ((.))
import Control.Category.Dual (Dual (..))
import Control.Category.NatOrd
import Control.Comonad.Travel
import Data.Foldable (Foldable (..))
import Data.List.NonEmpty (NonEmpty (..))
import Data.List.NonEmpty qualified as NE
import Data.Singletons (TyCon)
import Data.Singletons.Sigma (Sigma (..))
import GHC.TypeNats
import GHC.TypeNats.Extra (SNat (Succ, Zero))
import GHC.TypeNats.Singletons ()
import Prelude hiding (id, (.))
import Data.Some

viewNE :: NonEmpty a -> (forall n. SNat n -> (forall m. (m :<=: n) -> a) -> r) -> r
viewNE :: forall a r.
NonEmpty a
-> (forall (n :: Nat).
    SNat n -> (forall (m :: Nat). (m :<=: n) -> a) -> r)
-> r
viewNE NonEmpty a
as forall (n :: Nat).
SNat n -> (forall (m :: Nat). (m :<=: n) -> a) -> r
body = case NonEmpty a -> (a, Maybe (NonEmpty a))
forall a. NonEmpty a -> (a, Maybe (NonEmpty a))
NE.uncons NonEmpty a
as of
  (a
a, Maybe (NonEmpty a)
Nothing) -> SNat 0 -> (forall (m :: Nat). (m :<=: 0) -> a) -> r
forall (n :: Nat).
SNat n -> (forall (m :: Nat). (m :<=: n) -> a) -> r
body SNat 0
forall (n :: Nat). (n ~ 0) => SNat n
Zero (a -> forall (m :: Nat). (m :<=: 0) -> a
forall a. a -> forall (m :: Nat). (m :<=: 0) -> a
singletonFn a
a)
  (a
a, Just NonEmpty a
as') -> NonEmpty a
-> (forall (n :: Nat).
    SNat n -> (forall (m :: Nat). (m :<=: n) -> a) -> r)
-> r
forall a r.
NonEmpty a
-> (forall (n :: Nat).
    SNat n -> (forall (m :: Nat). (m :<=: n) -> a) -> r)
-> r
viewNE NonEmpty a
as' (\SNat n
n forall (m :: Nat). (m :<=: n) -> a
f -> SNat (n + 1) -> (forall (m :: Nat). (m :<=: (n + 1)) -> a) -> r
forall (n :: Nat).
SNat n -> (forall (m :: Nat). (m :<=: n) -> a) -> r
body (SNat n -> SNat (n + 1)
forall (n :: Nat) (m :: Nat). (n ~ (m + 1)) => SNat m -> SNat n
Succ SNat n
n) (a
-> (forall (m :: Nat). (m :<=: n) -> a)
-> forall (m :: Nat). (m :<=: (1 + n)) -> a
forall a (n :: Nat).
a
-> (forall (m :: Nat). (m :<=: n) -> a)
-> forall (m :: Nat). (m :<=: (1 + n)) -> a
consFn a
a (m :<=: n) -> a
forall (m :: Nat). (m :<=: n) -> a
f))

singletonFn :: a -> (forall m. (m :<=: 0) -> a)
singletonFn :: forall a. a -> forall (m :: Nat). (m :<=: 0) -> a
singletonFn a
a m :<=: 0
ReflLE = a
a
singletonFn a
_ (SuccLE m :<=: n1
mn) = (m :<=: n1) -> a
forall (p :: Nat -> *) (n :: Nat) a. (0 ~ (1 + n)) => p n -> a
zero_neq_succ m :<=: n1
mn

consFn :: a -> (forall m. (m :<=: n) -> a) -> (forall m. (m :<=: 1 + n) -> a)
consFn :: forall a (n :: Nat).
a
-> (forall (m :: Nat). (m :<=: n) -> a)
-> forall (m :: Nat). (m :<=: (1 + n)) -> a
consFn a
a forall (m :: Nat). (m :<=: n) -> a
f m :<=: (1 + n)
mn = case m :<=: (1 + n)
mn of
  m :<=: (1 + n)
ReflLE -> a
a
  SuccLE m :<=: n1
mn' -> (m :<=: n) -> a
forall (m :: Nat). (m :<=: n) -> a
f m :<=: n
m :<=: n1
mn'

indices :: SNat n -> NonEmpty (Some ((:>=:) n))
indices :: forall (n :: Nat). SNat n -> NonEmpty (Some ((:>=:) n))
indices SNat n
Zero = (n :>=: n) -> Some ((:>=:) n)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some ((n :<=: n) -> n :>=: n
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
cat b a -> Dual cat a b
Dual n :<=: n
forall (n :: Nat). n :<=: n
ReflLE) Some ((:>=:) n) -> [Some ((:>=:) n)] -> NonEmpty (Some ((:>=:) n))
forall a. a -> [a] -> NonEmpty a
:| []
indices (Succ SNat m
n) = (n :>=: n) -> Some ((:>=:) n)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some ((n :<=: n) -> n :>=: n
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
cat b a -> Dual cat a b
Dual n :<=: n
forall (n :: Nat). n :<=: n
ReflLE) Some ((:>=:) n) -> [Some ((:>=:) n)] -> NonEmpty (Some ((:>=:) n))
forall a. a -> [a] -> NonEmpty a
:| (Some ((:>=:) m) -> Some ((:>=:) n))
-> [Some ((:>=:) m)] -> [Some ((:>=:) n)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall (t :: Nat). (m :>=: t) -> n :>=: t)
-> Some ((:>=:) m) -> Some ((:>=:) n)
forall {k} (f :: k -> *) (g :: k -> *).
(forall (t :: k). f t -> g t) -> Some f -> Some g
mapSome Dual (:<=:) m t -> Dual (:<=:) n t
Dual (:<=:) m t -> (1 + m) :>=: t
forall (t :: Nat). (m :>=: t) -> n :>=: t
forall (n :: Nat) (m :: Nat). (n :>=: m) -> (1 + n) :>=: m
succGE) (NonEmpty (Some ((:>=:) m)) -> [Some ((:>=:) m)]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (SNat m -> NonEmpty (Some ((:>=:) m))
forall (n :: Nat). SNat n -> NonEmpty (Some ((:>=:) n))
indices SNat m
n))

succGE :: (n :>=: m) -> (1 + n :>=: m)
succGE :: forall (n :: Nat) (m :: Nat). (n :>=: m) -> (1 + n) :>=: m
succGE (Dual m :<=: n
mn) = (m :<=: (1 + n)) -> Dual (:<=:) (1 + n) m
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
cat b a -> Dual cat a b
Dual ((m :<=: n) -> m :<=: (1 + n)
forall (n :: Nat) (n1 :: Nat). (n :<=: n1) -> n :<=: (1 + n1)
SuccLE m :<=: n
mn)

fromNonEmpty :: NonEmpty a -> Travel (:>=:) a
fromNonEmpty :: forall a. NonEmpty a -> Travel (:>=:) a
fromNonEmpty NonEmpty a
as = NonEmpty a
-> (forall {n :: Nat}.
    SNat n -> (forall (m :: Nat). (m :<=: n) -> a) -> Travel (:>=:) a)
-> Travel (:>=:) a
forall a r.
NonEmpty a
-> (forall (n :: Nat).
    SNat n -> (forall (m :: Nat). (m :<=: n) -> a) -> r)
-> r
viewNE NonEmpty a
as ((forall {n :: Nat}.
  SNat n -> (forall (m :: Nat). (m :<=: n) -> a) -> Travel (:>=:) a)
 -> Travel (:>=:) a)
-> (forall {n :: Nat}.
    SNat n -> (forall (m :: Nat). (m :<=: n) -> a) -> Travel (:>=:) a)
-> Travel (:>=:) a
forall a b. (a -> b) -> a -> b
$ \SNat n
n forall (m :: Nat). (m :<=: n) -> a
f -> Sing n -> (Sigma Nat (TyCon ((:>=:) n)) -> a) -> Travel (:>=:) a
forall k (cat :: k -> k -> *) r (a :: k).
Sing a -> (Sigma k (TyCon (cat a)) -> r) -> Travel cat r
MkTravel SNat n
Sing n
n (\(Sing fst
_ :&: Dual fst :<=: n
mn) -> (fst :<=: n) -> a
forall (m :: Nat). (m :<=: n) -> a
f fst :<=: n
mn)

toNonEmpty :: Travel (:>=:) a -> NonEmpty a
toNonEmpty :: forall a. Travel (:>=:) a -> NonEmpty a
toNonEmpty (MkTravel Sing a
n Sigma Nat (TyCon ((:>=:) a)) -> a
f) = (Sigma Nat (TyCon ((:>=:) a)) -> a
f (Sigma Nat (TyCon ((:>=:) a)) -> a)
-> (Some ((:>=:) a) -> Sigma Nat (TyCon ((:>=:) a)))
-> Some ((:>=:) a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. SNat a -> Some ((:>=:) a) -> Sigma Nat (TyCon ((:>=:) a))
forall (n :: Nat).
SNat n -> Some ((:>=:) n) -> Sigma Nat (TyCon ((:>=:) n))
makeKey SNat a
Sing a
n) (Some ((:>=:) a) -> a) -> NonEmpty (Some ((:>=:) a)) -> NonEmpty a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SNat a -> NonEmpty (Some ((:>=:) a))
forall (n :: Nat). SNat n -> NonEmpty (Some ((:>=:) n))
indices SNat a
Sing a
n

makeKey :: SNat n -> Some ((:>=:) n) -> Sigma Nat (TyCon ((:>=:) n))
makeKey :: forall (n :: Nat).
SNat n -> Some ((:>=:) n) -> Sigma Nat (TyCon ((:>=:) n))
makeKey SNat n
sn (Some (Dual a :<=: n
mn)) = SNat n -> (a :<=: n) -> SNat a
forall (n :: Nat) (m :: Nat). SNat n -> (m :<=: n) -> SNat m
getLower SNat n
sn a :<=: n
mn Sing a -> (TyCon ((:>=:) n) @@ a) -> Sigma Nat (TyCon ((:>=:) n))
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: (a :<=: n) -> Dual (:<=:) n a
forall k (cat :: k -> k -> *) (a :: k) (b :: k).
cat b a -> Dual cat a b
Dual a :<=: n
mn

getLower :: SNat n -> (m :<=: n) -> SNat m
getLower :: forall (n :: Nat) (m :: Nat). SNat n -> (m :<=: n) -> SNat m
getLower SNat n
Zero m :<=: n
mn = case m :<=: n
mn of
  m :<=: n
ReflLE -> SNat m
forall (n :: Nat). (n ~ 0) => SNat n
Zero
  SuccLE m :<=: n1
mn' -> (m :<=: n1) -> SNat m
forall (p :: Nat -> *) (n :: Nat) a. (0 ~ (1 + n)) => p n -> a
zero_neq_succ m :<=: n1
mn'
getLower sn :: SNat n
sn@(Succ SNat m
sn') m :<=: n
mn = case m :<=: n
mn of
  m :<=: n
ReflLE -> SNat n
SNat m
sn
  SuccLE m :<=: n1
mn' -> SNat m -> (m :<=: m) -> SNat m
forall (n :: Nat) (m :: Nat). SNat n -> (m :<=: n) -> SNat m
getLower SNat m
sn' m :<=: m
m :<=: n1
mn'

zero_neq_succ :: forall p n a. (0 ~ (1 + n)) => p n -> a
zero_neq_succ :: forall (p :: Nat -> *) (n :: Nat) a. (0 ~ (1 + n)) => p n -> a
zero_neq_succ p n
_ = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible!"