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

module Rules where

import Base
import Representations


-- --------------------------------------
-- Rule types
-- --------------------------------------
infix 5 :~>
data Rule a = a :~> a

type Rule1 a = a -> Rule  a
type Rule2 a = a -> Rule1 a
type Rule3 a = a -> Rule2 a

lhsR :: Rule a -> a
lhsR (lhs :~> rhs) = lhs

rhsR :: Rule a -> a
rhsR (lhs :~> rhs) = rhs

type Rule' a = Rule (Pat (PF a))


-- --------------------------------------
-- Type for patterns (lhs, rhs of a rule)
-- --------------------------------------
type Pat f = Fix (Sum (K MVar) f)
type MVar  = Int

var :: MVar -> Pat f
var = In . Inl . K

pat :: f (Pat f) -> Pat f
pat = In . Inr

toPat :: (Functor (PF a), PFView a) => a -> Pat (PF a)
toPat = pat . fmap toPat . from

data ViewPat f = MVar MVar | PF (f (Pat f))

viewPat :: Pat f -> ViewPat f
viewPat (In (Inl (K x))) = MVar x
viewPat (In (Inr r))     = PF r

foldPat :: Functor f => (MVar -> a) -> (f a -> a) -> Pat f -> a
foldPat f g pat =
  case viewPat pat of
    MVar x -> f x
    PF r   -> g (fmap (foldPat f g) r)


-- --------------------------------------
-- Making a rule
-- --------------------------------------
class PFView (Target a) => Builder a where
  type Target a :: *
  base          :: a -> Rule (Target a)
  diag          :: a -> [Rule (Target a)]

instance PFView a => Builder (Rule a) where
  type Target (Rule a)  = a
  base x                = x
  diag x                = [x]

instance (Builder a, LR (PF b), PFView b) => Builder (b -> a) where
  type Target (b -> a) = Target a
  base f               = base (f left)
  diag f               = base (f right) : diag (f left)

rule :: (Builder a, Zip (PF (Target a))) => a -> Rule (Pat (PF (Target a)))
rule f = 
  mergeRules $ zipWith (flip diffRules (base f)) [0..] (diag f)
  where
    mergeRules = 
      foldr1 $ \l r -> merge (lhsR l) (lhsR r) :~>
                       merge (rhsR l) (rhsR r)
    diffRules x l r = 
      diff x (lhsR l) (lhsR r) :~>
      diff x (rhsR l) (rhsR r)


-- --------------------------------------
-- Extend a value with a meta-variable 
-- case. Two structures are traversed 
-- in parallel, whenever the structures 
-- mismatch, insert a meta-variable.
-- Otherwise, lift the matching parts.
-- --------------------------------------
diff :: (PFView a, Zip (PF a)) => MVar -> a -> a -> Pat (PF a)
diff name x y =
  case fzip (diff name) (from x) (from y) of
    Just str -> pat str
    Nothing  -> var name


-- --------------------------------------
-- Merge two patterns by accepting a
-- meta-variable case in one of the 
-- patterns, and otherwise zip the 
-- remaining parts.
-- --------------------------------------
merge :: Zip f => Pat f -> Pat f -> Pat f
merge p@(In x) q@(In y) =
  case (viewPat p, viewPat q) of
    (MVar i, _)  ->  p
    (_, MVar j)  ->  q 
    _            ->  In (fzip' merge x y)