{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Generics.Regular.Rewriting.Rules
-- Copyright   :  (c) 2008 Universiteit Utrecht
-- License     :  BSD3
--
-- Maintainer  :  generics@haskell.org
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Summary: Functions for transforming a rule specification to a rule.
--
-----------------------------------------------------------------------------

module Generics.Regular.Rewriting.Rules (

  -- * Rule specification.
  RuleSpec (..),
  lhsR,
  rhsR,
  
  -- * Representation of a rule.
  Rule,
  SchemeOf,
  Metavar,
  metavar,
  pf, 
  toScheme,
  SchemeView (..),
  schemeView,
  foldScheme,

  -- * Builder for transforming a rule specification to a rule.
  Builder (..),
  ruleM, 
  rule

) where

import Data.List

import Generics.Regular.Base
import Generics.Regular.Functions


-----------------------------------------------------------------------------
-- Rule specification.
-----------------------------------------------------------------------------

-- | Specifies a rule as a value of a datatype.
infix 5 :~>
data RuleSpec a = a :~> a

-- | Returns the left-hand side of a rule.
lhsR :: RuleSpec a -> a
lhsR (x :~> _) = x

-- | Returns the right-hand side of a rule.
rhsR :: RuleSpec a -> a
rhsR (_ :~> y) = y


-----------------------------------------------------------------------------
-- Representation of a rule.
-----------------------------------------------------------------------------

-- | Extends a pattern functor with a case for a metavariable.
type Ext f    = K Metavar :+: f
type Metavar  = Int

-- | Recursively extends a type with a case for a metavariable.
type Scheme f = Fix (Ext f)

-- | Extends the pattern functor of a value.
type SchemeOf a = Scheme (PF a)

-- | Allows metavariables on either side of a rule.
type Rule a = RuleSpec (SchemeOf a)

-- | Constructs a metavariable.
metavar :: Metavar -> Scheme f
metavar = In . L . K

-- | Constructs a pattern functor value.
pf :: f (Scheme f) -> Scheme f
pf = In . R

-- | A view on schemes to easily distinguish metavariables from
-- pattern functor values.
data SchemeView f = Metavar Metavar | PF (f (Scheme f))

-- | Returns the value corresponding to the @SchemeView@.
schemeView :: Scheme f -> SchemeView f
schemeView (In (L (K x))) = Metavar x
schemeView (In (R r))     = PF r

-- | Recursively converts a value to a @SchemeOf@ value.
toScheme :: (Regular a, Functor (PF a)) => a -> SchemeOf a
toScheme = pf . fmap toScheme . from

-- | Folds a @Scheme@ value given a function to apply to metavariables and a
-- function to apply to a pattern functor value.
foldScheme :: Functor f => (Metavar -> a) -> (f a -> a) -> Scheme f -> a
foldScheme f g scheme =
  case schemeView scheme of
    Metavar x -> f x
    PF r      -> g (fmap (foldScheme f g) r)


-----------------------------------------------------------------------------
-- Builder for transforming a rule specification to a rule.
-----------------------------------------------------------------------------

-- | The type class @Builder@ captures the functions, that are defined by
-- induction on the type argument, that construct appropriate @left@ and 
-- @right@ values. These values are used to transform a rule specification
-- to a rule.
class Regular (Target a) => Builder a where
  type Target a :: *
  base          :: a -> RuleSpec (Target a)
  diag          :: a -> [RuleSpec (Target a)]

instance Regular a => Builder (RuleSpec a) where
  type Target (RuleSpec a) = a
  base x                   = x
  diag x                   = [x]

instance (b ~ Target a, Builder a, Regular b, LR (PF b)) => Builder (b -> a) where
  type Target (b -> a) = Target a
  base f               = base (f left)
  
  -- Since mergeSchemes prefers metavariables in the first argument, it
  -- suffices to provide undefined to f in the recursive call to diag:
  --
  -- f left left to f right left, and
  -- f left left to f undefined right
  -- 
  -- The first hole of the first instance of f is filled with a metavariable, 
  -- after which mergeSchemes does not care any more about the first hole
  -- of the second instance of f.
  diag f               = base (f right) : diag (f left)

-- | Transforms a rule specification to a rule and throws a runtime error if
-- an unbound metavariable occurs in the right-hand side of the rule.
rule :: ( Builder r, Crush (PF (Target r))
        , Functor (PF (Target r)), Zip (PF (Target r)))
     => r -> Rule (Target r)
rule = maybe (error "rule: unbound metavariable") id . ruleM

-- | Transforms a rule specification to a rule and returns @Nothing@ if
-- an unbound metavariable occurs in the right-hand side of the rule.
ruleM :: (  Builder r, Crush (PF (Target r))
          , Zip (PF (Target r)), Functor (PF (Target r)))
      => r -> Maybe (Rule (Target r))
ruleM f = checkMetavars $ foldr1 mergeRules rules
  where
    checkMetavars r 
      | allElem rMetavars lMetavars = Just r
      | otherwise                   = Nothing
      where 
        allElem xs ys = all (`elem` ys) xs
        lMetavars = collectMetavars (lhsR r) [] 
        rMetavars = collectMetavars (rhsR r) []
        collectMetavars = foldScheme (:) (crushr (.) id)
    mergeRules x y = 
      mergeSchemes (lhsR x) (lhsR y) :~>
      mergeSchemes (rhsR x) (rhsR y)
    rules          = zipWith (ins (base f)) (diag f) [0..]   
    ins x y v      = 
      insertMetavar v (lhsR x) (lhsR y) :~>
      insertMetavar v (rhsR x) (rhsR y)

-- | Merges two schemes by preferring the metavariables that occur in either
-- of the two arguments.
mergeSchemes :: Zip f => Scheme f -> Scheme f -> Scheme f
mergeSchemes p@(In x) q@(In y) =
  case (schemeView p, schemeView q) of
    (Metavar _, _)  ->  p
    (_, Metavar _)  ->  q 
    _               ->  In (fzip' mergeSchemes x y)

-- | Inserts a metavariable in the right place by zipping two instances of
-- the function that are applied to different values. These values ensure
-- that the zipping process fails exactly at the point where a metavariable
-- is required to be inserted.
insertMetavar :: (Regular a, Zip (PF a)) => Metavar -> a -> a -> SchemeOf a
insertMetavar v x y =
  case fzip (insertMetavar v) (from x) (from y) of
    Just str -> pf str
    Nothing  -> metavar v