{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Generics.Simplistic.Zipper where
import Data.Proxy
import Data.Type.Equality
import GHC.Generics
import Data.Functor.Sum
import Control.Arrow (first)
import Generics.Simplistic
import Generics.Simplistic.Deep
import Generics.Simplistic.Util
data SZip ty w f where
Z_KH :: SZip ty w (K1 i ty)
Z_L1 :: SZip ty w f -> SZip ty w (f :+: g)
Z_R1 :: SZip ty w g -> SZip ty w (f :+: g)
Z_PairL :: SZip ty w f -> SRep w g -> SZip ty w (f :*: g)
Z_PairR :: SRep w f -> SZip ty w g -> SZip ty w (f :*: g)
Z_M1 :: SMeta i t -> SZip ty w f -> SZip ty w (M1 i t f)
deriving instance (forall a. Show (w a)) => Show (SZip h w f)
deriving instance (forall a. Eq (w a)) => Eq (SZip h w f)
plug :: SZip ty phi f -> phi ty -> SRep phi f
plug :: SZip ty phi f -> phi ty -> SRep phi f
plug Z_KH k :: phi ty
k = phi ty -> SRep phi (K1 i ty)
forall k (w :: * -> *) a i. w a -> SRep w (K1 i a)
S_K1 phi ty
k
plug (Z_L1 x :: SZip ty phi f
x) k :: phi ty
k = SRep phi f -> SRep phi f
forall k (w :: * -> *) (f :: k -> *) (g :: k -> *).
SRep w f -> SRep w (f :+: g)
S_L1 (SRep phi f -> SRep phi f) -> SRep phi f -> SRep phi f
forall a b. (a -> b) -> a -> b
$ SZip ty phi f -> phi ty -> SRep phi f
forall k ty (phi :: * -> *) (f :: k -> *).
SZip ty phi f -> phi ty -> SRep phi f
plug SZip ty phi f
x phi ty
k
plug (Z_R1 x :: SZip ty phi g
x) k :: phi ty
k = SRep phi g -> SRep phi f
forall k (w :: * -> *) (g :: k -> *) (f :: k -> *).
SRep w g -> SRep w (f :+: g)
S_R1 (SRep phi g -> SRep phi f) -> SRep phi g -> SRep phi f
forall a b. (a -> b) -> a -> b
$ SZip ty phi g -> phi ty -> SRep phi g
forall k ty (phi :: * -> *) (f :: k -> *).
SZip ty phi f -> phi ty -> SRep phi f
plug SZip ty phi g
x phi ty
k
plug (Z_M1 c :: SMeta i t
c x :: SZip ty phi f
x) k :: phi ty
k = SMeta i t -> SRep phi f -> SRep phi (M1 i t f)
forall k i (t :: Meta) (w :: * -> *) (f :: k -> *).
SMeta i t -> SRep w f -> SRep w (M1 i t f)
S_M1 SMeta i t
c (SRep phi f -> SRep phi f) -> SRep phi f -> SRep phi f
forall a b. (a -> b) -> a -> b
$ SZip ty phi f -> phi ty -> SRep phi f
forall k ty (phi :: * -> *) (f :: k -> *).
SZip ty phi f -> phi ty -> SRep phi f
plug SZip ty phi f
x phi ty
k
plug (Z_PairL x :: SZip ty phi f
x y :: SRep phi g
y) k :: phi ty
k = (SZip ty phi f -> phi ty -> SRep phi f
forall k ty (phi :: * -> *) (f :: k -> *).
SZip ty phi f -> phi ty -> SRep phi f
plug SZip ty phi f
x phi ty
k) SRep phi f -> SRep phi g -> SRep phi (f :*: g)
forall k (w :: * -> *) (f :: k -> *) (g :: k -> *).
SRep w f -> SRep w g -> SRep w (f :*: g)
:**: SRep phi g
y
plug (Z_PairR x :: SRep phi f
x y :: SZip ty phi g
y) k :: phi ty
k = SRep phi f
x SRep phi f -> SRep phi g -> SRep phi (f :*: g)
forall k (w :: * -> *) (f :: k -> *) (g :: k -> *).
SRep w f -> SRep w g -> SRep w (f :*: g)
:**: (SZip ty phi g -> phi ty -> SRep phi g
forall k ty (phi :: * -> *) (f :: k -> *).
SZip ty phi f -> phi ty -> SRep phi f
plug SZip ty phi g
y phi ty
k)
zipperMap :: (forall x . h x -> g x)
-> SZip ty h f -> SZip ty g f
zipperMap :: (forall x. h x -> g x) -> SZip ty h f -> SZip ty g f
zipperMap f :: forall x. h x -> g x
f (Z_L1 x :: SZip ty h f
x) = SZip ty g f -> SZip ty g (f :+: g)
forall k ty (w :: * -> *) (f :: k -> *) (g :: k -> *).
SZip ty w f -> SZip ty w (f :+: g)
Z_L1 ((forall x. h x -> g x) -> SZip ty h f -> SZip ty g f
forall k (h :: * -> *) (g :: * -> *) ty (f :: k -> *).
(forall x. h x -> g x) -> SZip ty h f -> SZip ty g f
zipperMap forall x. h x -> g x
f SZip ty h f
x)
zipperMap f :: forall x. h x -> g x
f (Z_R1 x :: SZip ty h g
x) = SZip ty g g -> SZip ty g (f :+: g)
forall k ty (w :: * -> *) (g :: k -> *) (f :: k -> *).
SZip ty w g -> SZip ty w (f :+: g)
Z_R1 ((forall x. h x -> g x) -> SZip ty h g -> SZip ty g g
forall k (h :: * -> *) (g :: * -> *) ty (f :: k -> *).
(forall x. h x -> g x) -> SZip ty h f -> SZip ty g f
zipperMap forall x. h x -> g x
f SZip ty h g
x)
zipperMap f :: forall x. h x -> g x
f (Z_M1 c :: SMeta i t
c x :: SZip ty h f
x) = SMeta i t -> SZip ty g f -> SZip ty g (M1 i t f)
forall k g (t :: Meta) ty (w :: * -> *) (f :: k -> *).
SMeta g t -> SZip ty w f -> SZip ty w (M1 g t f)
Z_M1 SMeta i t
c ((forall x. h x -> g x) -> SZip ty h f -> SZip ty g f
forall k (h :: * -> *) (g :: * -> *) ty (f :: k -> *).
(forall x. h x -> g x) -> SZip ty h f -> SZip ty g f
zipperMap forall x. h x -> g x
f SZip ty h f
x)
zipperMap f :: forall x. h x -> g x
f (Z_PairL x :: SZip ty h f
x y :: SRep h g
y) = SZip ty g f -> SRep g g -> SZip ty g (f :*: g)
forall k ty (w :: * -> *) (f :: k -> *) (g :: k -> *).
SZip ty w f -> SRep w g -> SZip ty w (f :*: g)
Z_PairL ((forall x. h x -> g x) -> SZip ty h f -> SZip ty g f
forall k (h :: * -> *) (g :: * -> *) ty (f :: k -> *).
(forall x. h x -> g x) -> SZip ty h f -> SZip ty g f
zipperMap forall x. h x -> g x
f SZip ty h f
x) ((forall x. h x -> g x) -> SRep h g -> SRep g g
forall k (f :: * -> *) (g :: * -> *) (rep :: k -> *).
(forall y. f y -> g y) -> SRep f rep -> SRep g rep
repMap forall x. h x -> g x
f SRep h g
y)
zipperMap f :: forall x. h x -> g x
f (Z_PairR x :: SRep h f
x y :: SZip ty h g
y) = SRep g f -> SZip ty g g -> SZip ty g (f :*: g)
forall k (w :: * -> *) (f :: k -> *) ty (g :: k -> *).
SRep w f -> SZip ty w g -> SZip ty w (f :*: g)
Z_PairR ((forall x. h x -> g x) -> SRep h f -> SRep g f
forall k (f :: * -> *) (g :: * -> *) (rep :: k -> *).
(forall y. f y -> g y) -> SRep f rep -> SRep g rep
repMap forall x. h x -> g x
f SRep h f
x) ((forall x. h x -> g x) -> SZip ty h g -> SZip ty g g
forall k (h :: * -> *) (g :: * -> *) ty (f :: k -> *).
(forall x. h x -> g x) -> SZip ty h f -> SZip ty g f
zipperMap forall x. h x -> g x
f SZip ty h g
y)
zipperMap _ Z_KH = SZip ty g f
forall k ty (w :: * -> *) i. SZip ty w (K1 i ty)
Z_KH
inr1 :: (x :*: y) t -> (Sum z x :*: y) t
inr1 :: (:*:) x y t -> (:*:) (Sum z x) y t
inr1 (x :: x t
x :*: y :: y t
y) = (x t -> Sum z x t
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR x t
x Sum z x t -> y t -> (:*:) (Sum z x) y t
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: y t
y)
zipperRepZip :: SZip ty h f -> SRep w f -> Maybe (SRep ((Sum ((:~:) ty) h) :*: w) f)
zipperRepZip :: SZip ty h f -> SRep w f -> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
zipperRepZip Z_KH (S_K1 y :: w a
y) = SRep (Sum ((:~:) a) h :*: w) (K1 i a)
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
forall (m :: * -> *) a. Monad m => a -> m a
return (SRep (Sum ((:~:) a) h :*: w) (K1 i a)
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) f))
-> SRep (Sum ((:~:) a) h :*: w) (K1 i a)
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
forall a b. (a -> b) -> a -> b
$ (:*:) (Sum ((:~:) a) h) w a
-> SRep (Sum ((:~:) a) h :*: w) (K1 i a)
forall k (w :: * -> *) a i. w a -> SRep w (K1 i a)
S_K1 ((a :~: a) -> Sum ((:~:) a) h a
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL a :~: a
forall k (a :: k). a :~: a
Refl Sum ((:~:) a) h a -> w a -> (:*:) (Sum ((:~:) a) h) w a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: w a
y)
zipperRepZip (Z_L1 x :: SZip ty h f
x) (S_L1 y :: SRep w f
y) = SRep (Sum ((:~:) ty) h :*: w) f
-> SRep (Sum ((:~:) ty) h :*: w) (f :+: g)
forall k (w :: * -> *) (f :: k -> *) (g :: k -> *).
SRep w f -> SRep w (f :+: g)
S_L1 (SRep (Sum ((:~:) ty) h :*: w) f
-> SRep (Sum ((:~:) ty) h :*: w) (f :+: g))
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) (f :+: g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SZip ty h f -> SRep w f -> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
forall k ty (h :: * -> *) (f :: k -> *) (w :: * -> *).
SZip ty h f -> SRep w f -> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
zipperRepZip SZip ty h f
x SRep w f
SRep w f
y
zipperRepZip (Z_R1 x :: SZip ty h g
x) (S_R1 y :: SRep w g
y) = SRep (Sum ((:~:) ty) h :*: w) g
-> SRep (Sum ((:~:) ty) h :*: w) (f :+: g)
forall k (w :: * -> *) (g :: k -> *) (f :: k -> *).
SRep w g -> SRep w (f :+: g)
S_R1 (SRep (Sum ((:~:) ty) h :*: w) g
-> SRep (Sum ((:~:) ty) h :*: w) (f :+: g))
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) g)
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) (f :+: g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SZip ty h g -> SRep w g -> Maybe (SRep (Sum ((:~:) ty) h :*: w) g)
forall k ty (h :: * -> *) (f :: k -> *) (w :: * -> *).
SZip ty h f -> SRep w f -> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
zipperRepZip SZip ty h g
x SRep w g
SRep w g
y
zipperRepZip (Z_M1 c :: SMeta i t
c x :: SZip ty h f
x) (S_M1 _ y :: SRep w f
y) = SMeta i t
-> SRep (Sum ((:~:) ty) h :*: w) f
-> SRep (Sum ((:~:) ty) h :*: w) (M1 i t f)
forall k i (t :: Meta) (w :: * -> *) (f :: k -> *).
SMeta i t -> SRep w f -> SRep w (M1 i t f)
S_M1 SMeta i t
c (SRep (Sum ((:~:) ty) h :*: w) f
-> SRep (Sum ((:~:) ty) h :*: w) (M1 i t f))
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) (M1 i t f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SZip ty h f -> SRep w f -> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
forall k ty (h :: * -> *) (f :: k -> *) (w :: * -> *).
SZip ty h f -> SRep w f -> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
zipperRepZip SZip ty h f
x SRep w f
SRep w f
y
zipperRepZip (Z_PairL x :: SZip ty h f
x y :: SRep h g
y) (y1 :: SRep w f
y1 :**: y2 :: SRep w g
y2)
= SRep (Sum ((:~:) ty) h :*: w) f
-> SRep (Sum ((:~:) ty) h :*: w) g
-> SRep (Sum ((:~:) ty) h :*: w) (f :*: g)
forall k (w :: * -> *) (f :: k -> *) (g :: k -> *).
SRep w f -> SRep w g -> SRep w (f :*: g)
(:**:) (SRep (Sum ((:~:) ty) h :*: w) f
-> SRep (Sum ((:~:) ty) h :*: w) g
-> SRep (Sum ((:~:) ty) h :*: w) (f :*: g))
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
-> Maybe
(SRep (Sum ((:~:) ty) h :*: w) g
-> SRep (Sum ((:~:) ty) h :*: w) (f :*: g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SZip ty h f -> SRep w f -> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
forall k ty (h :: * -> *) (f :: k -> *) (w :: * -> *).
SZip ty h f -> SRep w f -> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
zipperRepZip SZip ty h f
x SRep w f
SRep w f
y1 Maybe
(SRep (Sum ((:~:) ty) h :*: w) g
-> SRep (Sum ((:~:) ty) h :*: w) (f :*: g))
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) g)
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) (f :*: g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((forall y. (:*:) h w y -> (:*:) (Sum ((:~:) ty) h) w y)
-> SRep (h :*: w) g -> SRep (Sum ((:~:) ty) h :*: w) g
forall k (f :: * -> *) (g :: * -> *) (rep :: k -> *).
(forall y. f y -> g y) -> SRep f rep -> SRep g rep
repMap forall y. (:*:) h w y -> (:*:) (Sum ((:~:) ty) h) w y
forall k (x :: k -> *) (y :: k -> *) (t :: k) (z :: k -> *).
(:*:) x y t -> (:*:) (Sum z x) y t
inr1 (SRep (h :*: w) g -> SRep (Sum ((:~:) ty) h :*: w) g)
-> Maybe (SRep (h :*: w) g)
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) g)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRep h g -> SRep w g -> Maybe (SRep (h :*: w) g)
forall k (w :: * -> *) (f :: k -> *) (z :: * -> *).
SRep w f -> SRep z f -> Maybe (SRep (w :*: z) f)
zipSRep SRep h g
y SRep w g
SRep w g
y2)
zipperRepZip (Z_PairR x :: SRep h f
x y :: SZip ty h g
y) (y1 :: SRep w f
y1 :**: y2 :: SRep w g
y2)
= SRep (Sum ((:~:) ty) h :*: w) f
-> SRep (Sum ((:~:) ty) h :*: w) g
-> SRep (Sum ((:~:) ty) h :*: w) (f :*: g)
forall k (w :: * -> *) (f :: k -> *) (g :: k -> *).
SRep w f -> SRep w g -> SRep w (f :*: g)
(:**:) (SRep (Sum ((:~:) ty) h :*: w) f
-> SRep (Sum ((:~:) ty) h :*: w) g
-> SRep (Sum ((:~:) ty) h :*: w) (f :*: g))
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
-> Maybe
(SRep (Sum ((:~:) ty) h :*: w) g
-> SRep (Sum ((:~:) ty) h :*: w) (f :*: g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((forall y. (:*:) h w y -> (:*:) (Sum ((:~:) ty) h) w y)
-> SRep (h :*: w) f -> SRep (Sum ((:~:) ty) h :*: w) f
forall k (f :: * -> *) (g :: * -> *) (rep :: k -> *).
(forall y. f y -> g y) -> SRep f rep -> SRep g rep
repMap forall y. (:*:) h w y -> (:*:) (Sum ((:~:) ty) h) w y
forall k (x :: k -> *) (y :: k -> *) (t :: k) (z :: k -> *).
(:*:) x y t -> (:*:) (Sum z x) y t
inr1 (SRep (h :*: w) f -> SRep (Sum ((:~:) ty) h :*: w) f)
-> Maybe (SRep (h :*: w) f)
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRep h f -> SRep w f -> Maybe (SRep (h :*: w) f)
forall k (w :: * -> *) (f :: k -> *) (z :: * -> *).
SRep w f -> SRep z f -> Maybe (SRep (w :*: z) f)
zipSRep SRep h f
x SRep w f
SRep w f
y1) Maybe
(SRep (Sum ((:~:) ty) h :*: w) g
-> SRep (Sum ((:~:) ty) h :*: w) (f :*: g))
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) g)
-> Maybe (SRep (Sum ((:~:) ty) h :*: w) (f :*: g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SZip ty h g -> SRep w g -> Maybe (SRep (Sum ((:~:) ty) h :*: w) g)
forall k ty (h :: * -> *) (f :: k -> *) (w :: * -> *).
SZip ty h f -> SRep w f -> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
zipperRepZip SZip ty h g
y SRep w g
SRep w g
y2
zipperRepZip _ _ = Maybe (SRep (Sum ((:~:) ty) h :*: w) f)
forall a. Maybe a
Nothing
zipSZip :: SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f)
zipSZip :: SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f)
zipSZip Z_KH Z_KH = SZip ty (h :*: w) (K1 i ty) -> Maybe (SZip ty (h :*: w) (K1 i ty))
forall a. a -> Maybe a
Just SZip ty (h :*: w) (K1 i ty)
forall k ty (w :: * -> *) i. SZip ty w (K1 i ty)
Z_KH
zipSZip (Z_L1 x :: SZip ty h f
x) (Z_L1 y :: SZip ty w f
y) = SZip ty (h :*: w) f -> SZip ty (h :*: w) (f :+: g)
forall k ty (w :: * -> *) (f :: k -> *) (g :: k -> *).
SZip ty w f -> SZip ty w (f :+: g)
Z_L1 (SZip ty (h :*: w) f -> SZip ty (h :*: w) (f :+: g))
-> Maybe (SZip ty (h :*: w) f)
-> Maybe (SZip ty (h :*: w) (f :+: g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f)
forall k ty (h :: * -> *) (f :: k -> *) (w :: * -> *).
SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f)
zipSZip SZip ty h f
x SZip ty w f
SZip ty w f
y
zipSZip (Z_R1 x :: SZip ty h g
x) (Z_R1 y :: SZip ty w g
y) = SZip ty (h :*: w) g -> SZip ty (h :*: w) (f :+: g)
forall k ty (w :: * -> *) (g :: k -> *) (f :: k -> *).
SZip ty w g -> SZip ty w (f :+: g)
Z_R1 (SZip ty (h :*: w) g -> SZip ty (h :*: w) (f :+: g))
-> Maybe (SZip ty (h :*: w) g)
-> Maybe (SZip ty (h :*: w) (f :+: g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SZip ty h g -> SZip ty w g -> Maybe (SZip ty (h :*: w) g)
forall k ty (h :: * -> *) (f :: k -> *) (w :: * -> *).
SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f)
zipSZip SZip ty h g
x SZip ty w g
SZip ty w g
y
zipSZip (Z_M1 c :: SMeta i t
c x :: SZip ty h f
x) (Z_M1 _ y :: SZip ty w f
y) = SMeta i t -> SZip ty (h :*: w) f -> SZip ty (h :*: w) (M1 i t f)
forall k g (t :: Meta) ty (w :: * -> *) (f :: k -> *).
SMeta g t -> SZip ty w f -> SZip ty w (M1 g t f)
Z_M1 SMeta i t
c (SZip ty (h :*: w) f -> SZip ty (h :*: w) (M1 i t f))
-> Maybe (SZip ty (h :*: w) f)
-> Maybe (SZip ty (h :*: w) (M1 i t f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f)
forall k ty (h :: * -> *) (f :: k -> *) (w :: * -> *).
SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f)
zipSZip SZip ty h f
x SZip ty w f
SZip ty w f
y
zipSZip (Z_PairL x :: SZip ty h f
x y :: SRep h g
y) (Z_PairL w :: SZip ty w f
w z :: SRep w g
z)
= SZip ty (h :*: w) f
-> SRep (h :*: w) g -> SZip ty (h :*: w) (f :*: g)
forall k ty (w :: * -> *) (f :: k -> *) (g :: k -> *).
SZip ty w f -> SRep w g -> SZip ty w (f :*: g)
Z_PairL (SZip ty (h :*: w) f
-> SRep (h :*: w) g -> SZip ty (h :*: w) (f :*: g))
-> Maybe (SZip ty (h :*: w) f)
-> Maybe (SRep (h :*: w) g -> SZip ty (h :*: w) (f :*: g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f)
forall k ty (h :: * -> *) (f :: k -> *) (w :: * -> *).
SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f)
zipSZip SZip ty h f
x SZip ty w f
SZip ty w f
w Maybe (SRep (h :*: w) g -> SZip ty (h :*: w) (f :*: g))
-> Maybe (SRep (h :*: w) g) -> Maybe (SZip ty (h :*: w) (f :*: g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SRep h g -> SRep w g -> Maybe (SRep (h :*: w) g)
forall k (w :: * -> *) (f :: k -> *) (z :: * -> *).
SRep w f -> SRep z f -> Maybe (SRep (w :*: z) f)
zipSRep SRep h g
y SRep w g
SRep w g
z
zipSZip (Z_PairR x :: SRep h f
x y :: SZip ty h g
y) (Z_PairR w :: SRep w f
w z :: SZip ty w g
z)
= SRep (h :*: w) f
-> SZip ty (h :*: w) g -> SZip ty (h :*: w) (f :*: g)
forall k (w :: * -> *) (f :: k -> *) ty (g :: k -> *).
SRep w f -> SZip ty w g -> SZip ty w (f :*: g)
Z_PairR (SRep (h :*: w) f
-> SZip ty (h :*: w) g -> SZip ty (h :*: w) (f :*: g))
-> Maybe (SRep (h :*: w) f)
-> Maybe (SZip ty (h :*: w) g -> SZip ty (h :*: w) (f :*: g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRep h f -> SRep w f -> Maybe (SRep (h :*: w) f)
forall k (w :: * -> *) (f :: k -> *) (z :: * -> *).
SRep w f -> SRep z f -> Maybe (SRep (w :*: z) f)
zipSRep SRep h f
x SRep w f
SRep w f
w Maybe (SZip ty (h :*: w) g -> SZip ty (h :*: w) (f :*: g))
-> Maybe (SZip ty (h :*: w) g)
-> Maybe (SZip ty (h :*: w) (f :*: g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SZip ty h g -> SZip ty w g -> Maybe (SZip ty (h :*: w) g)
forall k ty (h :: * -> *) (f :: k -> *) (w :: * -> *).
SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f)
zipSZip SZip ty h g
y SZip ty w g
SZip ty w g
z
zipSZip _ _ = Maybe (SZip ty (h :*: w) f)
forall a. Maybe a
Nothing
zipLeavesList :: SZip ty w f -> [Maybe (Exists w)]
zipLeavesList :: SZip ty w f -> [Maybe (Exists w)]
zipLeavesList (Z_L1 x :: SZip ty w f
x) = SZip ty w f -> [Maybe (Exists w)]
forall k ty (w :: * -> *) (f :: k -> *).
SZip ty w f -> [Maybe (Exists w)]
zipLeavesList SZip ty w f
x
zipLeavesList (Z_R1 x :: SZip ty w g
x) = SZip ty w g -> [Maybe (Exists w)]
forall k ty (w :: * -> *) (f :: k -> *).
SZip ty w f -> [Maybe (Exists w)]
zipLeavesList SZip ty w g
x
zipLeavesList (Z_M1 _ x :: SZip ty w f
x) = SZip ty w f -> [Maybe (Exists w)]
forall k ty (w :: * -> *) (f :: k -> *).
SZip ty w f -> [Maybe (Exists w)]
zipLeavesList SZip ty w f
x
zipLeavesList (Z_PairL l :: SZip ty w f
l x :: SRep w g
x) = SZip ty w f -> [Maybe (Exists w)]
forall k ty (w :: * -> *) (f :: k -> *).
SZip ty w f -> [Maybe (Exists w)]
zipLeavesList SZip ty w f
l [Maybe (Exists w)] -> [Maybe (Exists w)] -> [Maybe (Exists w)]
forall a. [a] -> [a] -> [a]
++ (Exists w -> Maybe (Exists w)) -> [Exists w] -> [Maybe (Exists w)]
forall a b. (a -> b) -> [a] -> [b]
map Exists w -> Maybe (Exists w)
forall a. a -> Maybe a
Just (SRep w g -> [Exists w]
forall k (w :: * -> *) (rep :: k -> *). SRep w rep -> [Exists w]
repLeavesList SRep w g
x)
zipLeavesList (Z_PairR x :: SRep w f
x l :: SZip ty w g
l) = (Exists w -> Maybe (Exists w)) -> [Exists w] -> [Maybe (Exists w)]
forall a b. (a -> b) -> [a] -> [b]
map Exists w -> Maybe (Exists w)
forall a. a -> Maybe a
Just (SRep w f -> [Exists w]
forall k (w :: * -> *) (rep :: k -> *). SRep w rep -> [Exists w]
repLeavesList SRep w f
x) [Maybe (Exists w)] -> [Maybe (Exists w)] -> [Maybe (Exists w)]
forall a. [a] -> [a] -> [a]
++ SZip ty w g -> [Maybe (Exists w)]
forall k ty (w :: * -> *) (f :: k -> *).
SZip ty w f -> [Maybe (Exists w)]
zipLeavesList SZip ty w g
l
zipLeavesList (SZip ty w f
Z_KH ) = [Maybe (Exists w)
forall a. Maybe a
Nothing]
data Zipper c f g t where
Zipper :: c
=> { Zipper c f g t -> SZip t f (Rep t)
zipper :: SZip t f (Rep t)
, Zipper c f g t -> g t
sel :: g t
}
-> Zipper c f g t
type Zipper' kappa fam ann phi t
= Zipper (CompoundCnstr kappa fam t)
(HolesAnn kappa fam ann phi)
(HolesAnn kappa fam ann phi) t
zippers :: forall kappa fam ann phi t
. (forall a . (Elem t fam) => phi a -> Maybe (a :~: t))
-> HolesAnn kappa fam ann phi t
-> [Zipper' kappa fam ann phi t]
zippers :: (forall a. Elem t fam => phi a -> Maybe (a :~: t))
-> HolesAnn kappa fam ann phi t -> [Zipper' kappa fam ann phi t]
zippers _ (Prim' _ _) = []
zippers _ (Hole' _ _) = []
zippers aux :: forall a. Elem t fam => phi a -> Maybe (a :~: t)
aux (Roll' _ r :: SRep (HolesAnn kappa fam ann phi) (Rep t)
r) = ((SZip t (HolesAnn kappa fam ann phi) (Rep t),
HolesAnn kappa fam ann phi t)
-> Zipper
(('True ~ 'True, HasElem t fam), 'False ~ 'False, Generic t)
(HolesAnn kappa fam ann phi)
(HolesAnn kappa fam ann phi)
t)
-> [(SZip t (HolesAnn kappa fam ann phi) (Rep t),
HolesAnn kappa fam ann phi t)]
-> [Zipper
(('True ~ 'True, HasElem t fam), 'False ~ 'False, Generic t)
(HolesAnn kappa fam ann phi)
(HolesAnn kappa fam ann phi)
t]
forall a b. (a -> b) -> [a] -> [b]
map ((SZip t (HolesAnn kappa fam ann phi) (Rep t)
-> HolesAnn kappa fam ann phi t
-> Zipper
(('True ~ 'True, HasElem t fam), 'False ~ 'False, Generic t)
(HolesAnn kappa fam ann phi)
(HolesAnn kappa fam ann phi)
t)
-> (SZip t (HolesAnn kappa fam ann phi) (Rep t),
HolesAnn kappa fam ann phi t)
-> Zipper
(('True ~ 'True, HasElem t fam), 'False ~ 'False, Generic t)
(HolesAnn kappa fam ann phi)
(HolesAnn kappa fam ann phi)
t
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SZip t (HolesAnn kappa fam ann phi) (Rep t)
-> HolesAnn kappa fam ann phi t
-> Zipper
(('True ~ 'True, HasElem t fam), 'False ~ 'False, Generic t)
(HolesAnn kappa fam ann phi)
(HolesAnn kappa fam ann phi)
t
forall (c :: Constraint) t (f :: * -> *) (g :: * -> *).
c =>
SZip t f (Rep t) -> g t -> Zipper c f g t
Zipper) (SRep (HolesAnn kappa fam ann phi) (Rep t)
-> [(SZip t (HolesAnn kappa fam ann phi) (Rep t),
HolesAnn kappa fam ann phi t)]
forall k (f :: k -> *).
SRep (HolesAnn kappa fam ann phi) f
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
go SRep (HolesAnn kappa fam ann phi) (Rep t)
r)
where
pf :: Proxy fam
pf :: Proxy fam
pf = Proxy fam
forall k (t :: k). Proxy t
Proxy
pa :: HolesAnn kappa fam ann phi a -> Proxy a
pa :: HolesAnn kappa fam ann phi a -> Proxy a
pa _ = Proxy a
forall k (t :: k). Proxy t
Proxy
go :: SRep (HolesAnn kappa fam ann phi) f
-> [(SZip t (HolesAnn kappa fam ann phi) f
, HolesAnn kappa fam ann phi t)]
go :: SRep (HolesAnn kappa fam ann phi) f
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
go S_U1 = []
go (S_L1 x :: SRep (HolesAnn kappa fam ann phi) f
x) = (SZip t (HolesAnn kappa fam ann phi) f
-> SZip t (HolesAnn kappa fam ann phi) (f :+: g))
-> (SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)
-> (SZip t (HolesAnn kappa fam ann phi) (f :+: g),
HolesAnn kappa fam ann phi t)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first SZip t (HolesAnn kappa fam ann phi) f
-> SZip t (HolesAnn kappa fam ann phi) (f :+: g)
forall k ty (w :: * -> *) (f :: k -> *) (g :: k -> *).
SZip ty w f -> SZip ty w (f :+: g)
Z_L1 ((SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)
-> (SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t))
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRep (HolesAnn kappa fam ann phi) f
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
forall k (f :: k -> *).
SRep (HolesAnn kappa fam ann phi) f
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
go SRep (HolesAnn kappa fam ann phi) f
x
go (S_R1 x :: SRep (HolesAnn kappa fam ann phi) g
x) = (SZip t (HolesAnn kappa fam ann phi) g
-> SZip t (HolesAnn kappa fam ann phi) (f :+: g))
-> (SZip t (HolesAnn kappa fam ann phi) g,
HolesAnn kappa fam ann phi t)
-> (SZip t (HolesAnn kappa fam ann phi) (f :+: g),
HolesAnn kappa fam ann phi t)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first SZip t (HolesAnn kappa fam ann phi) g
-> SZip t (HolesAnn kappa fam ann phi) (f :+: g)
forall k ty (w :: * -> *) (g :: k -> *) (f :: k -> *).
SZip ty w g -> SZip ty w (f :+: g)
Z_R1 ((SZip t (HolesAnn kappa fam ann phi) g,
HolesAnn kappa fam ann phi t)
-> (SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t))
-> [(SZip t (HolesAnn kappa fam ann phi) g,
HolesAnn kappa fam ann phi t)]
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRep (HolesAnn kappa fam ann phi) g
-> [(SZip t (HolesAnn kappa fam ann phi) g,
HolesAnn kappa fam ann phi t)]
forall k (f :: k -> *).
SRep (HolesAnn kappa fam ann phi) f
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
go SRep (HolesAnn kappa fam ann phi) g
x
go (S_M1 c :: SMeta i t
c x :: SRep (HolesAnn kappa fam ann phi) f
x) = (SZip t (HolesAnn kappa fam ann phi) f
-> SZip t (HolesAnn kappa fam ann phi) (M1 i t f))
-> (SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)
-> (SZip t (HolesAnn kappa fam ann phi) (M1 i t f),
HolesAnn kappa fam ann phi t)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (SMeta i t
-> SZip t (HolesAnn kappa fam ann phi) f
-> SZip t (HolesAnn kappa fam ann phi) (M1 i t f)
forall k g (t :: Meta) ty (w :: * -> *) (f :: k -> *).
SMeta g t -> SZip ty w f -> SZip ty w (M1 g t f)
Z_M1 SMeta i t
c) ((SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)
-> (SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t))
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRep (HolesAnn kappa fam ann phi) f
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
forall k (f :: k -> *).
SRep (HolesAnn kappa fam ann phi) f
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
go SRep (HolesAnn kappa fam ann phi) f
x
go (x :: SRep (HolesAnn kappa fam ann phi) f
x :**: y :: SRep (HolesAnn kappa fam ann phi) g
y) = ((SZip t (HolesAnn kappa fam ann phi) f
-> SZip t (HolesAnn kappa fam ann phi) (f :*: g))
-> (SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)
-> (SZip t (HolesAnn kappa fam ann phi) (f :*: g),
HolesAnn kappa fam ann phi t)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((SZip t (HolesAnn kappa fam ann phi) f
-> SRep (HolesAnn kappa fam ann phi) g
-> SZip t (HolesAnn kappa fam ann phi) (f :*: g))
-> SRep (HolesAnn kappa fam ann phi) g
-> SZip t (HolesAnn kappa fam ann phi) f
-> SZip t (HolesAnn kappa fam ann phi) (f :*: g)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SZip t (HolesAnn kappa fam ann phi) f
-> SRep (HolesAnn kappa fam ann phi) g
-> SZip t (HolesAnn kappa fam ann phi) (f :*: g)
forall k ty (w :: * -> *) (f :: k -> *) (g :: k -> *).
SZip ty w f -> SRep w g -> SZip ty w (f :*: g)
Z_PairL SRep (HolesAnn kappa fam ann phi) g
y) ((SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)
-> (SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t))
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRep (HolesAnn kappa fam ann phi) f
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
forall k (f :: k -> *).
SRep (HolesAnn kappa fam ann phi) f
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
go SRep (HolesAnn kappa fam ann phi) f
x)
[(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
forall a. [a] -> [a] -> [a]
++ ((SZip t (HolesAnn kappa fam ann phi) g
-> SZip t (HolesAnn kappa fam ann phi) (f :*: g))
-> (SZip t (HolesAnn kappa fam ann phi) g,
HolesAnn kappa fam ann phi t)
-> (SZip t (HolesAnn kappa fam ann phi) (f :*: g),
HolesAnn kappa fam ann phi t)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (SRep (HolesAnn kappa fam ann phi) f
-> SZip t (HolesAnn kappa fam ann phi) g
-> SZip t (HolesAnn kappa fam ann phi) (f :*: g)
forall k (w :: * -> *) (f :: k -> *) ty (g :: k -> *).
SRep w f -> SZip ty w g -> SZip ty w (f :*: g)
Z_PairR SRep (HolesAnn kappa fam ann phi) f
x) ((SZip t (HolesAnn kappa fam ann phi) g,
HolesAnn kappa fam ann phi t)
-> (SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t))
-> [(SZip t (HolesAnn kappa fam ann phi) g,
HolesAnn kappa fam ann phi t)]
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRep (HolesAnn kappa fam ann phi) g
-> [(SZip t (HolesAnn kappa fam ann phi) g,
HolesAnn kappa fam ann phi t)]
forall k (f :: k -> *).
SRep (HolesAnn kappa fam ann phi) f
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
go SRep (HolesAnn kappa fam ann phi) g
y)
go (S_K1 x :: HolesAnn kappa fam ann phi a
x@(Roll' _ _)) =
case Proxy fam -> Proxy t -> Proxy a -> Maybe (t :~: a)
forall k (fam :: [k]) (x :: k) (y :: k).
(Elem x fam, Elem y fam) =>
Proxy fam -> Proxy x -> Proxy y -> Maybe (x :~: y)
sameTy Proxy fam
pf (Proxy t
forall k (t :: k). Proxy t
Proxy :: Proxy t) (HolesAnn kappa fam ann phi a -> Proxy a
forall a. HolesAnn kappa fam ann phi a -> Proxy a
pa HolesAnn kappa fam ann phi a
x) of
Just Refl -> (SZip t (HolesAnn kappa fam ann phi) (K1 i t),
HolesAnn kappa fam ann phi a)
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((SZip t (HolesAnn kappa fam ann phi) (K1 i t),
HolesAnn kappa fam ann phi a)
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)])
-> (SZip t (HolesAnn kappa fam ann phi) (K1 i t),
HolesAnn kappa fam ann phi a)
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
forall a b. (a -> b) -> a -> b
$ (SZip t (HolesAnn kappa fam ann phi) (K1 i t)
forall k ty (w :: * -> *) i. SZip ty w (K1 i ty)
Z_KH , HolesAnn kappa fam ann phi a
x)
Nothing -> []
go (S_K1 x :: HolesAnn kappa fam ann phi a
x@(Hole' _ xh :: phi a
xh)) =
case phi a -> Maybe (a :~: t)
forall a. Elem t fam => phi a -> Maybe (a :~: t)
aux phi a
xh of
Just Refl -> (SZip t (HolesAnn kappa fam ann phi) (K1 i t),
HolesAnn kappa fam ann phi a)
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((SZip t (HolesAnn kappa fam ann phi) (K1 i t),
HolesAnn kappa fam ann phi a)
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)])
-> (SZip t (HolesAnn kappa fam ann phi) (K1 i t),
HolesAnn kappa fam ann phi a)
-> [(SZip t (HolesAnn kappa fam ann phi) f,
HolesAnn kappa fam ann phi t)]
forall a b. (a -> b) -> a -> b
$ (SZip t (HolesAnn kappa fam ann phi) (K1 i t)
forall k ty (w :: * -> *) i. SZip ty w (K1 i ty)
Z_KH , HolesAnn kappa fam ann phi a
x)
Nothing -> []
go _ = []
zipConstructorName :: SZip h w f -> String
zipConstructorName :: SZip h w f -> String
zipConstructorName (Z_M1 x :: SMeta i t
x@SMeta i t
SM_C _)
= SMeta C t -> String
forall k (c :: k). SMeta C c -> String
getConstructorName SMeta i t
SMeta C t
x
zipConstructorName (Z_M1 _ x :: SZip h w f
x)
= SZip h w f -> String
forall k h (w :: * -> *) (f :: k -> *). SZip h w f -> String
zipConstructorName SZip h w f
x
zipConstructorName (Z_L1 x :: SZip h w f
x)
= SZip h w f -> String
forall k h (w :: * -> *) (f :: k -> *). SZip h w f -> String
zipConstructorName SZip h w f
x
zipConstructorName (Z_R1 x :: SZip h w g
x)
= SZip h w g -> String
forall k h (w :: * -> *) (f :: k -> *). SZip h w f -> String
zipConstructorName SZip h w g
x
zipConstructorName _
= ShowS
forall a. HasCallStack => String -> a
error "Please; use GHC's deriving mechanism. This keeps M1's at the top of the Rep"