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 )
class (Zipper phi (PF phi), Rewrite phi) => Transform phi
instance Transform phi => Rewrite phi
type Transformation phi a = [ AnyInsert phi a ]
data AnyInsert phi a where
AnyInsert ::
phi ix
-> (Loc phi I0 a -> Maybe (Loc phi I0 a))
-> 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
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 = Just . update (\p -> maybe (error "updateM") id . f p)