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

module Rules where

import Base
import Representations
import Rewriting

-------------------------
-- compiling rules
-------------------------

-- we want to easily write down rules that involve metavariables by reusing
-- the power of Haskell's lambda-abstractions; for example:
--
--   \x y z -> x :*: (y :+: z) :~> x :*: y :+: x :*: z
--
-- therefore, we provide some machinery for `compiling' such
-- lambda-abstractions into rules involving the pattern types that can be
-- obtained by extending a type's pattern functor

class View (Target a) => Compile a where
  type Target a :: *
  allLeft       :: a -> Rule (Target a)
  oneRight      :: a -> [Rule (Target a)]
  compile       :: a -> Rule (Pat (PF (Target a)))

-- just rules, no metavariables
instance View a => Compile (Rule a) where
  type Target (Rule a)  = a
  allLeft x             = x
  oneRight _            = []
  compile (lhs :~> rhs) = toPat (from lhs) :~> toPat (from rhs)

-- rules involving metavariables can be expressed by functions that produce
-- rules; rules are then compiled according to the following scheme:
-- okay, but now the scheme is clear: the zero-variable constructor pretty
-- much stands alone, but for n >= 1, the n-variable constructor all follow the
-- following pattern:
--
--   compile f = merge
--     [ diff 0       (f left left ... left) (f right left ... left)
--     , diff 1       (f left left ... left) (f left right ... left)
--         :  :        :   :    :        :    :   :        .      :
--         :  :        :   :    :        :    :   :    .     .    .
--         :  :        :   :    :        :    :   :    :       .
--     , diff (n - 1) (f left left ... left) (f left left ... right)
--     ]
--
-- in particular, note the diagonal pattern of calls to right in the
-- third-position arguments of the diff invocations!

-- the last constraint in the instance head requires undecidable instances:
-- can this be solved??
instance (Compile a, Left b, Right b, Match (PF (Target a))) =>
         Compile (b -> a) where
  type Target (b -> a) = Target a
  allLeft f            = allLeft (f left)
  oneRight f           = allLeft (f right) : oneRight (f left)
  compile f            = mergeRules 
                       $ zipWith (\v r -> diffRules v allL r) [0 ..] oneRs
    where
      diffRules x l r = diff x (from $ lhsR l) (from $ lhsR r) :~>
                        diff x (from $ rhsR l) (from $ rhsR r)
      mergeRules      = foldr1 $ \l r -> merge (lhsR l) (lhsR r) :~>
                                         merge (rhsR l) (rhsR r)
      allL            = allLeft f
      oneRs           = oneRight f