{-# OPTIONS -fglasgow-exts #-}

module Rewriting where

import Control.Monad
import qualified Data.Map as M
import Data.Maybe

import Base
import Representations
import Rules


-- --------------------------------------
-- Rewriting a term
-- --------------------------------------
rewrite :: (Crush (PF a), PFView a, Zip (PF a)) => Rule (Pat (PF a)) -> a -> a
rewrite f term = maybe term id (rewriteM f term)

rewriteM :: (Crush (PF a), PFView a, Zip (PF a), Monad m) => Rule (Pat (PF a)) -> a -> m a 
rewriteM f term = 
  do subst <- match (lhsR f) term
     return (inst subst (rhsR f))


-- --------------------------------------
-- Matching a term
-- --------------------------------------
type Subst a = M.Map MVar (a, Pat (PF a))

match :: (Crush (PF a), PFView a, Zip (PF a), Monad m) => Pat (PF a) -> a -> m (Subst a)
match pat term = 
  case viewPat pat of
    MVar x  -> return (M.singleton x (term, toPat term))
    PF r1   ->
      fzip (,) r1 (from term) >>=
      crush matchOne (return M.empty)
  where
    matchOne (term1, term2) msubst = 
      do subst1 <- msubst
         subst2 <- match (apply subst1 term1) term2
         return (M.union subst1 subst2)


-- --------------------------------------
-- Building a term
-- --------------------------------------
-- Apply a substitution assuming that the result contains
-- no meta-variables. 
inst :: PFView a => Subst a -> Pat (PF a) -> a
inst subst = foldPat find to
  where
    find x = 
      maybe (error "inst: unbound meta-variable") 
            fst
            (M.lookup x subst)

-- Apply a substition to a pattern
apply :: PFView a => Subst a -> Pat (PF a) -> Pat (PF a)
apply subst = foldPat find pat
  where
    find x =
      maybe (var x) 
            snd  
            (M.lookup x subst)