{-# OPTIONS_GHC -fglasgow-exts #-}

import Indices
import Base
import Rewriting

data Expr = Let Decl Expr | EVar String
  deriving Show
data Decl = String := Expr | Dummy -- otherwise left/right don't fail with zip
  deriving Show

data ED :: * -> * where
  Expr   :: ED Expr
  Decl   :: ED Decl
  String :: ED String

edixeq :: Monad m => ED a -> ED b -> m (TEq a b)
edixeq Expr Expr = return TEq
edixeq Decl Decl = return TEq
edixeq String String = return TEq
edixeq _     _     = fail "Failed to match witnesses of ED datatypes"

type instance PF ED = Sum (Tag Expr (Prod (Id Decl) (Id Expr))) (
                      Sum (Tag Expr (Id String)) (
                      Sum (Tag Decl (Prod (Id String) (Id Expr))) (
                      Sum (Tag Decl Unit)
                          (Tag String (K String))
                          )))


instance Repr ED where
  ixeq = edixeq


instance Ix ED Expr where
  from (Let decl expr)  =  (Inl (Tag (Prod (Id (I decl)) (Id (I expr)))))
  from (EVar var)       =  (Inr (Inl (Tag (Id (I var)))))

  to ( (Inl (Tag (Prod (Id decl') (Id expr'))))) = Let (unI decl') (unI expr')
  to ( (Inr (Inl (Tag (Id var'))))) = EVar (unI var')

  ix = Expr

instance Ix ED Decl where
  from (var := expr) =  (Inr (Inr (Inl (Tag (Prod (Id (I var)) (Id (I expr)))))))
  from Dummy           =  (Inr (Inr (Inr (Inl (Tag Unit)))))

  to ((Inr (Inr (Inl (Tag (Prod (Id var') (Id expr'))))))) = (unI var') := (unI expr')
  to ((Inr (Inr (Inr ((Inl (Tag Unit)))))))                              = Dummy

  ix = Decl

instance Ix ED String where
  from s     = (Inr (Inr (Inr (Inr (Tag (K s))))))

  to ((Inr (Inr (Inr (Inr (Tag (K s))))))) = s

  ix = String

{-

instance RewriteDT ED
instance Rewrite ED Expr
instance Rewrite ED Decl
instance Rewrite ED String

-- Now we have to check that the instances satisfy the required properties
props = do
        leftRightProp pED (undefined::String)
        leftRightProp pED (undefined::Expr)
        leftRightProp pED (undefined::Decl)
-}

instance Rewrite ED -- this is the ugly part about class synonyms

xvar v = HIn (Inl (K v))
xlet a b = (HIn (Inr (Inl (Tag (Prod (Id a) (Id b))))))

rule0 :: Rule (Scheme ED Expr)
rule0 = xvar 0 :~> xvar 0

-- Let decl expr :~> Let decl (Let decl expr)
rule1 :: Rule (Scheme ED Expr)

rule1 = xlet (xvar 0) (xvar 1) :~> xlet (xvar 0) (xlet (xvar 0) (xvar 1))

expr0 = Let ("x" := (EVar "y")) (EVar "x")

test0 = rewrite rule0 expr0

test1 = rewrite rule1 expr0

-- inlining
test2 = rewrite2 Expr (\var expr -> Let (var := expr) (EVar var) :~> expr) expr0
  -- evaluates to |EVar "y"|
  --
  --