{-# 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   #-}
-- |Provides bare-bones /zipper/ functionality
-- to 'SRep' and 'Holes'.
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

-- |A value of type 'SZip ty w f' corresponds to a value of type
-- 'SRep w f' with one of its leaves of type @w ty@ absent.
-- This is essentially a zipper for 'SRep'.
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)

-- |We can transform a 'SZip' into a 'SRep' given
-- we are provided with a value to /plug/ into the identified position.
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)

-- |Maps over a 'SZip'
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)

-- |Given a @z :: SZip ty h f@ and a @r :: Rep w f@, if @z@ and @r@
-- are made with the same constuctor we return a representation
-- that contains both @h@s and @w@s in its leaves, except in one leaf
-- of type @ty@. This is analogous to 'zipSRep'.
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

-- |Overlaps two zippers together; only succeeds if both zippers
-- have the same constructor AND hole.
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

-- |Analogous to 'repLeavesList'
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]

-- |The 'Zipper' datatype packages a 'SZip' in a more standard
-- presentation. A value of type @Zipper c f g t@ represents
-- a value of type @SRep f t@, where exactly one recursive leaf (of type @t@)
-- carries a value of type @g t@, moreover, we also carry a proof that
-- the constraint @c@ holds.
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

-- |Auxiliar type synonym for annotated fixpoints.
type Zipper' kappa fam ann phi t
  = Zipper (CompoundCnstr kappa fam t)
           (HolesAnn kappa fam ann phi)
           (HolesAnn kappa fam ann phi) t

-- |Given a function that checks wheter an arbitrary position
-- is recursive and a value of @t@, returns all possible zippers ove
-- @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 _ = []
      
-- |Retrieves the constructor name for a representation.
-- /WARNING; UNSAFE/ this function only works if @f@ is the representation of
-- a type constructed with "GHC.Generics" builtin mechanisms.
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"