{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes       #-}
{-# LANGUAGE TypeOperators    #-}
{-# LANGUAGE PatternSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE TypeFamilies #-}

module Fold where

import Base
import HMap

type Alg l r = forall ix. Ix l ix => l ix -> Str l r ix -> r ix

fold :: (Ix l ix, HMap (PF l)) => l ix ->
        Alg l r -> ix -> r ix
fold _ alg = alg ix . hmap (\ l (I x) -> fold ix alg x) . from

-- Creating an algebra

infixr &
infixr :->

type AlgPart a (l :: * -> *) r ix = a l r ix -> r ix
type (f :-> g) (l :: * -> *) (r :: * -> *) ix = f l r ix -> g l r ix

(&) :: (AlgPart a :-> AlgPart b :-> AlgPart (a :+: b)) l r ix
(f & g) (L x) = f x
(f & g) (R x) = g x 

fn :: (a l r ix -> b l r ix -> c) -> (a :*: b) l r ix -> c
fn f (x :*: y) = f x y

tag :: AlgPart a l r ix -> AlgPart (a ::: ix) l r ix'
tag f (Tag x) = f x

type family Simplify x :: *
type instance Simplify (Id x l r ix) = r x
type instance Simplify (K x l r ix)  = x

class Get x where
  get :: x -> Simplify x

instance Get (Id x l r ix) where
  get (Id x) = x

instance Get (K x l r ix) where
  get (K x) = x

embed :: Get (a l r ix) => (Simplify (a l r ix) -> r ix) -> AlgPart a l r ix
embed f x = f (get x)