{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE EmptyDataDecls             #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE GADTs                      #-}

module Generics.MultiRec.Transformations.RewriteRules (
  Transformation, Transform, apply, insert, AnyInsert (..)
  ) where

import Generics.MultiRec hiding ( foldM )
import Generics.MultiRec.Rewriting
import Generics.MultiRec.Zipper (Zipper, Loc, leave, enter, update)

import Data.Maybe ( fromJust )
import Control.Monad ( (>=>), foldM )

--------------------------------------------------------------------------------
-- Patch
--------------------------------------------------------------------------------
-- Basically, a class synonym
class (Zipper phi (PF phi), Rewrite phi) => Transform phi
instance Transform phi => Rewrite phi

-- An edit is a list of:
type Transformation phi a = [ AnyInsert phi a ]

-- Existential for insertion
data AnyInsert phi a where 
  AnyInsert ::
    -- Proof
    phi ix
    -- A path to the location to edit
    -> (Loc phi I0 a -> Maybe (Loc phi I0 a)) 
    -- The rewrite rule to apply there
    -> Rule phi ix
    -> AnyInsert phi a

insert :: El phi ix => (Loc phi I0 a -> Maybe (Loc phi I0 a)) -> Rule phi ix
          -> AnyInsert phi a
insert = AnyInsert proof

-- Patching is terribly simple: at the given locations, apply all the rules,
-- then exit the zipper.
apply :: Transform phi => Transformation phi a -> phi a -> a -> Maybe a
apply rs p x = fmap leave $ foldM appRule (enter p x) rs
  where appRule a (AnyInsert p' l r) = l a >>=
                            updateM (\p'' -> case eqS p' p'' of
                                              Nothing   -> const Nothing
                                              Just Refl -> rewriteM r)

updateM :: (forall xi. phi xi -> xi -> Maybe xi)
        -> Loc phi I0 ix -> Maybe (Loc phi I0 ix)
-- updateM f (Loc p (I0 x) s) = f p x >>= \y -> Loc p (I0 y) s
updateM f = Just . update (\p -> maybe (error "updateM") id . f p)