{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE KindSignatures        #-}

module Generics.MultiRec.Rewriting.HZip where

import Generics.MultiRec.Base
import Generics.MultiRec.ZipWith


-- | Combine two structures monadically only
combine :: (Monad m, HZipWith rel rel' f) =>
           (forall b c ix'. rel b ix' -> rel' c ix' 
                         -> r1 ix' -> r2 ix' -> m ()) ->
           f r1 ix -> f r2 ix -> m ()
combine f x y = hzipWithM wrapf x y >> return ()
  where
    wrapf r1 r2 x' y' = f r1 r2 x' y' >> return (K0 ())

-- | Monadic generic equality (just for the sake of the monad!)
eq' :: (Monad m, Fam phi es, Fam phi es', HZipWith (FamRel phi es) (FamRel phi es') (PF phi))
    => phi es b ix -> phi es' c ix -> b -> c -> m ()
eq' p1 p2 x y = undefined --zipWithM undefined p1 p2 undefined x y --combine eq' (from p1 x) (from p2 y)

{-
zipcaseM :: (Monad m) => 
         (forall b' c' ix'. rel  b' ix' -> rel'  c' ix' -> f ix' -> f' ix' -> m (f'' ix')) -> 
         (forall b' c' ix'. rel2 b' ix' -> rel2' c' ix' -> g ix' -> g' ix' -> m (g'' ix')) -> 
         RelCase rel rel2 b ix -> RelCase rel' rel2' c ix -> Case f g ix -> Case f' g' ix -> m (Case f'' g'' ix)
zipcaseM f _ (RL p) (RL p') (CL x) (CL x') = liftM CL (f p p' x x')
zipcaseM _ g (RR p) (RR p') (CR y) (CR y') = liftM CR (g p p' y y')
zipcaseM _ _ _      _       _      _       = mzero
-}