{-# LANGUAGE FlexibleContexts   #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies       #-}
{-# LANGUAGE PatternSignatures  #-}
{-# LANGUAGE ScopedTypeVariables#-}

module Zipper where

import Control.Monad

import Representations

data Zipper a = Zipper a [D (PF a) a]

class Diff (f :: * -> *) where
  type D f :: * -- original data
           -> *

instance Diff Id where
  type D Id = Unit

instance Diff (K a) where
  type D (K a) = Zero

instance Diff Unit where
  type D Unit = Zero

refute :: Zero a -> b
refute x = x `seq` error "Why don't you refute this oh Haskell!"

instance (Diff f,Diff g) => Diff (Sum f g) where
  type D (Sum f g) = Sum (D f) (D g)

instance (Diff f,Diff g) => Diff (Prod f g) where
  type D (Prod f g) = Sum (Prod (D f) g)
                             -- recurse into fist component
                             -- leave second unchanged         
                          (Prod f (D g))
                             -- now go into second

instance (Diff f) => Diff (Con f) where
  type D (Con f) = D f

toZipper :: a -> Zipper a
toZipper x = Zipper x []

fromZipper :: Zipper a -> a
fromZipper (Zipper x []) = x

down :: (PFView a,ZipFuns (PF a)) => Zipper a -> Maybe (Zipper a)
down (Zipper x ctxs)
  = case nextf (Left (from x)) of
      Left (ctx,x') -> Just (Zipper x' (ctx:ctxs))
      Right _ -> Nothing

up :: (PFView a,ZipFuns (PF a)) => Zipper a -> Maybe (Zipper a)
up (Zipper x []) = Nothing
up (Zipper x (ctx:ctxs)) = Just (Zipper (to (upf x ctx)) ctxs)


getZipper :: Zipper a -> a
getZipper (Zipper x _) = x

next :: forall a . (PFView a,ZipFuns (PF a)) => Zipper a -> Maybe (Zipper a)
next (Zipper x []) = Nothing
next (Zipper x (ctx:ctxs))
  = case nextf (Right (x,ctx)) of
      Left (ctx',x') -> Just (Zipper x' (ctx':ctxs))
      Right (x'::PF a a) -> Nothing
        -- without the pattern signature above,
        -- GHC does not want to unify the f from
        -- nextf's signature with PF a

class ZipFuns f where
  nextf  :: Either (f a) (a,D f a) -> Either (D f a,a) (f a)
  upf    :: a -> D f a -> f a
  


instance ZipFuns Id where
  nextf (Left (Id a)) = Left (Unit,a)
  nextf (Right (a,Unit)) = Right (Id a)

  upf a Unit = Id a

instance ZipFuns (K a) where
  nextf (Left (K x)) = Right (K x)
  nextf (Right (a,ctx)) = refute ctx

instance ZipFuns Unit where
  nextf (Left Unit) = Right Unit
  nextf (Right (x,ctx))  = refute ctx

instance ZipFuns f => ZipFuns (Con f) where
  nextf (Left (Con cname x))
    = case nextf (Left x) of
        Left x -> Left x
        Right y -> Right (Con cname y)
  nextf (Right (a,ctx))
    = case nextf (Right (a,ctx)) of
        Left res -> Left res
        Right x' -> Right (Con "invented con" x')
          -- the con name thing above is ugly
          -- it could be remeddied by "type-level"
          -- constructor tags.

instance (ZipFuns f,ZipFuns g) => ZipFuns (Sum f g) where
  nextf (Left (Inl x))
    = case nextf (Left x) of
        Left (ctx',a') -> Left (Inl ctx',a')

  nextf (Left (Inr y))
    = case nextf (Left y) of
        Left (ctx',a') -> Left (Inr ctx',a')

  nextf (Right (a,Inl ctx))
    = case nextf (Right (a,ctx)) of
        Left (ctx',a') -> Left (Inl ctx',a')
        Right x'       -> Right (Inl x')
  nextf (Right (a,Inr ctx))
    = case nextf (Right (a,ctx)) of
        Left (ctx',a') -> Left (Inr ctx',a')
        Right y'       -> Right (Inr y')

instance (ZipFuns f,ZipFuns g) => ZipFuns (Prod f g) where
  nextf (Left (Prod x y))
    = case nextf (Left x) of
        Left (ctx',a') -> Left (Inl (Prod ctx' y),a')
        Right _ ->
          case nextf (Left y) of
            Left (ctx',a') -> Left (Inr (Prod x ctx'),a')
            Right _ -> Right (Prod x y)

  nextf (Right (a,Inl (Prod ctx y)))
    = case nextf (Right (a,ctx)) of
        Left (ctx',a') -> Left (Inl (Prod ctx' y),a')
        Right x' ->
          case nextf (Left y) of
            Left (ctx',a') -> Left (Inr (Prod x' ctx'),a')
            Right _ -> Right (Prod x' y)