{-# LANGUAGE FlexibleContexts #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Generics.Regular.Rewriting.Machinery
-- Copyright   :  (c) 2008 Universiteit Utrecht
-- License     :  BSD3
--
-- Maintainer  :  generics@haskell.org
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Summary: Core machinery for rewriting terms.
-----------------------------------------------------------------------------

module Generics.Regular.Rewriting.Machinery (

  -- * Type class synonym summarizing generic functions.
  Rewrite,

  -- * Applying a rule specification to a term.
  applyRuleM,
  applyRule,

  -- * Rewriting a term.
  rewriteM,
  rewrite,

)  where

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

import Generics.Regular.Base
import Generics.Regular.Functions
import qualified Generics.Regular.Functions.Show as G
import Generics.Regular.Rewriting.Rules


-----------------------------------------------------------------------------
-- Type class synonym summarizing generic functions.
-----------------------------------------------------------------------------
-- | The @Rewrite@ is a type class synonym, hiding some of the implementation
-- details.
--
-- To be able to use the rewriting functions, the user is required to provide
-- an instance of this type class.
class (Regular a, Crush (PF a), GMap (PF a), G.Show (PF a)
      , Zip (PF a), LR (PF a), Functor (PF a)) => Rewrite a


-----------------------------------------------------------------------------
-- Applying a rule to a term.
-----------------------------------------------------------------------------

{-# INLINE applyRuleM #-}
-- | Applies a rule specification to a term, obtaining a monadic value.
applyRuleM :: (Builder r, Rewrite (Target r), Monad m) => r -> Target r -> m (Target r)
applyRuleM = rewriteM . rule

{-# INLINE applyRule #-}
-- | Applies a rule specification to a term, obtaining the original term 
-- when rewriting fails.
applyRule :: (Builder r, Rewrite (Target r)) => r -> Target r -> Target r
applyRule = rewrite . rule


-----------------------------------------------------------------------------
-- Rewriting a term.
-----------------------------------------------------------------------------

{-# INLINE rewriteM #-}
-- | Rewrites a term, obtaining a monadic value.
rewriteM :: (Rewrite a, Monad m) => Rule a -> a -> m a 
rewriteM f term = 
  do subst <- match (lhsR f) term
     return (inst subst (rhsR f))

{-# INLINE rewrite #-}
-- | Rewrites a term, obtaining the original term when rewriting fails.
rewrite :: Rewrite a => Rule a -> a -> a
rewrite f term = maybe term id (rewriteM f term)


-----------------------------------------------------------------------------
-- Matching a term.
-----------------------------------------------------------------------------

-- | A substitution maps a metavariable to a pair of the original term
-- and the converted term. Both are stored to improve efficiency, since
-- the right-hand side of a term may caontain multiple occurrences of the
-- same metavariable.
type Subst a = M.Map Metavar (a, SchemeOf a)

-- | Matches a term to the left-hand side of a rule.
match :: (Rewrite a, Monad m) => SchemeOf a -> a -> m (Subst a)
match scheme term = 
  case schemeView scheme of
    Metavar x -> return (M.singleton x (term, toScheme term))
    PF r      ->
      fzip (,) r (from term) >>=
      crushr 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.
-----------------------------------------------------------------------------

-- | Applies a substitution to a term.
apply :: (Regular a, Functor (PF a)) => Subst a -> SchemeOf a -> SchemeOf a
apply subst = foldScheme findMetavar pf
  where
    findMetavar x = maybe (metavar x) snd (M.lookup x subst)

-- | Instantiates all the metavariables in a term, assuming that there are no
-- unbound metavariables in the term.
inst :: (Regular a, Functor (PF a)) => Subst a -> SchemeOf a -> a
inst subst = foldScheme findMetavar to
  where
    findMetavar x = 
      maybe undefined fst (M.lookup x subst)