{-# LANGUAGE DeriveDataTypeable     #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE FlexibleInstances      #-}

module Test where

import Generics.Instant
import Generics.Instant.Rewriting

-------------------------------------------------------------------------------
-- Simple Datatype
-------------------------------------------------------------------------------

-- Example datatype
data Exp = Const Int | Plus Exp Exp deriving (Show, Typeable, Eq)

-- Representable instance
instance Representable Exp where
  type Rep Exp = Var Int :+: Rec Exp :*: Rec Exp

  from (Const n)   = L (Var n)
  from (Plus e e') = R (Rec e :*: Rec e')

  to (L (Var n))            = Const n
  to (R (Rec e :*: Rec e')) = Plus e e'

-- Required Rewritable instance
instance Rewritable Exp

-- An example rule
silly :: Rule Exp
silly = synthesise $ \e n ->
           Plus e (Const n)  +->  e    // n == 0

-- Applying the rewriting mechanism
test1 :: String
test1 = show $ rewrite silly (Plus (Const 2) (Const 0))

-------------------------------------------------------------------------------
-- Mutually recursive datatypes
-------------------------------------------------------------------------------

data Decl = None | Seq Decl Decl | Assign String Expr
  deriving (Show, Typeable, Eq)

data Expr = V String | Lam String Expr | App Expr Expr | Let Decl Expr
  deriving (Show, Typeable, Eq)

instance Representable Decl where
  type Rep Decl = U :+: Rec Decl :*: Rec Decl :+: Var String :*: Rec Expr

  from None         = L U
  from (Seq d1 d2)  = R (L (Rec d1 :*: Rec d2))
  from (Assign v e) = R (R (Var v :*: Rec e))

  to (L U)                       = None
  to (R (L (Rec d1 :*: Rec d2))) = Seq d1 d2
  to (R (R (Var v :*: Rec e)))   = Assign v e

instance Representable Expr where
  type Rep Expr =     Var String :+: Var String :*: Rec Expr
                 :+: Rec Expr :*: Rec Expr :+: Rec Decl :*: Rec Expr

  from (V x)     = L (Var x)
  from (Lam v e) = R (L (Var v :*: Rec e))
  from (App f e) = R (R (L (Rec f :*: Rec e)))
  from (Let d e) = R (R (R (Rec d :*: Rec e)))

  to (L (Var x))                   = V x
  to (R (L (Var v :*: Rec e)))     = Lam v e
  to (R (R (L (Rec f :*: Rec e)))) = App f e
  to (R (R (R (Rec d :*: Rec e)))) = Let d e
              
instance Rewritable Decl
instance Rewritable Expr
instance Rewritable [Char]

remLet :: Rule Expr
remLet = synthesise $ \x e -> Let (Assign x e) (V x) +-> e

remX :: Rule Decl
remX = synthesise $ \v e -> Assign v e +-> None // v == "x"

test2 :: String
test2 = show $ rewrite remLet (Let (Assign "x" (V "y")) (V "x"))

test3 :: String
test3 = show $ rewrite remX (Assign "x" (V "y"))


main = print [test1, test2, test3]