{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE Rank2Types            #-}
{-# LANGUAGE FlexibleInstances     #-}

module FoldEAlgK where

import Except

import Generics.MultiRec.Base
import Generics.MultiRec.HFunctor
import Generics.MultiRec.HFix

-- * The type family of convenient algebras.

-- | The type family we use to describe the convenient algebras.
type family ErrorAlgebra
  (f :: (* -> *) -> * -> *) 
  (e :: *)         -- error type
  (r :: *)         -- index
  :: *

-- | For a constant, we take the constant value to a result.
type instance ErrorAlgebra (K a) e r = a -> Either e r

-- | For a unit, no arguments are available.
type instance ErrorAlgebra U e r = Either e r

-- | For an identity, we turn the recursive result into a final result.
--   Note that the index can change.
type instance ErrorAlgebra (I xi) e r = r -> Either e r

-- | For a sum, the algebra is a pair of two algebras.
type instance ErrorAlgebra (f :+: g) e r = (ErrorAlgebra f e r, ErrorAlgebra g e r)

-- | For a product where the left hand side is a constant, we
--   take the value as an additional argument.
type instance ErrorAlgebra (K a :*: g) e r = a -> ErrorAlgebra g e r

-- | For a product where the left hand side is an identity, we
--   take the recursive result as an additional argument.
type instance ErrorAlgebra (I xi :*: g) e r = r -> ErrorAlgebra g e r

-- | Tags are ignored.
type instance ErrorAlgebra (f :>: xi) e r = ErrorAlgebra f e r

-- | Constructors are ignored.
type instance ErrorAlgebra (C c f) e ix = ErrorAlgebra f e ix

-- * The class to turn convenient algebras into standard algebras.

-- | The class fold explains how to convert a convenient algebra
--   'Alg' back into a function from functor to result, as required
--   by the standard fold function.
class Fold f where
  alg :: ErrorAlgebra f e r -> f (K0 r) ix -> Either e r

instance Fold (K a) where
  alg f (K x) = f x

instance Fold U where
  alg f U     = f

instance Fold (I xi) where
  alg f (I (K0 x)) = f x

instance (Fold f, Fold g) => Fold (f :+: g) where
  alg (f, g) (L x) = alg f x
  alg (f, g) (R x) = alg g x

instance Fold g => Fold (K a :*: g) where
  alg f (K x :*: y) = alg (f x) y

instance Fold g => Fold (I xi :*: g) where
  alg f (I (K0 x) :*: y) = alg (f x) y

instance Fold f => Fold (f :>: xi) where
  alg f (Tag x) = alg f x

instance Fold f => Fold (C c f) where
  alg f (C x) = alg f x

foldE :: (HFunctor phi f, Fold f) => ErrorAlgebra f e r ->
  phi ix -> HFix (K x :*: f) ix -> Except [(e, x)] r
foldE a proof (HIn (K k :*: f)) =
    case hmapA (\proof' -> fmap K0 . foldE a proof') proof f of
      Failed xs -> Failed xs
      OK expr' -> case alg a expr' of
        Left x'  -> Failed [(x', k)]
        Right v  -> OK v

-- | For constructing algebras that are made of nested pairs rather
--   than n-ary tuples, it is helpful to use this pairing combinator.
(&) :: a -> b -> (a, b)
(&) = (,)

infixr 5 &