{-# 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]