{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeSynonymInstances  #-}

module AST2 where

import Base

-------------------------------------------------------------------------------
-- the AST type from the paper
-------------------------------------------------------------------------------

infix 1 :=

data Expr   =  Const  Int
            |  Add    Expr  Expr
            |  Mul    Expr  Expr
            |  EVar   Var
            |  Let    Decl  Expr
  deriving Show

data Decl   =  Var := Expr
            |  Seq       Decl  Decl
  deriving Show

type Var   =  String

-------------------------------------------------------------------------------
-- grouping the mutual recursive types in a family
-------------------------------------------------------------------------------

data AST :: * -> * where
  Expr  ::  AST Expr
  Decl  ::  AST Decl
  Var   ::  AST Var

type instance PF AST  =    
                   K Int                    :::  Expr  -- |Const|
              :+:  (Id Expr :*: Id Expr)    :::  Expr  -- |Add|
              :+:  (Id Expr :*: Id Expr)    :::  Expr  -- |Mul|
              :+:  Id Var                   :::  Expr  -- |EVar|
              :+:  (Id Decl :*: Id Expr)    :::  Expr  -- |Let|
              :+:  (Id Var :*: Id Expr)     :::  Decl  -- |:=|
              :+:  (Id Decl :*: Id Decl)    :::  Decl  -- |Seq|
              :+:  K String                 :::  Var   -- |V|

instance Ix AST Expr where

  from (Const i)   =  L                     (Tag (K i))
  from (Add e f)   =  R (L                  (Tag (Id (I e) :*: Id (I f))))
  from (Mul e f)   =  R (R (L               (Tag (Id (I e) :*: Id (I f)))))
  from (EVar x)    =  R (R (R (L            (Tag (Id (I x))))))
  from (Let d e)   =  R (R (R (R (L         (Tag (Id (I d) :*: Id (I e)))))))

  to (L                     (Tag (K i)))                        =  Const i
  to (R (L                  (Tag (Id (I e) :*: Id (I f)))))     =  Add e f
  to (R (R (L               (Tag (Id (I e) :*: Id (I f))))))    =  Mul e f
  to (R (R (R (L            (Tag (Id (I x)))))))                =  EVar x
  to (R (R (R (R (L         (Tag (Id (I d) :*: Id (I e))))))))  =  Let d e
  
  ix  =  Expr

instance Ix AST Decl where

  from (x := e)    =  R (R (R (R (R (L      (Tag (Id (I x) :*: Id (I e))))))))
  from (Seq c d)   =  R (R (R (R (R (R (L   (Tag (Id (I c) :*: Id (I d)))))))))

  to (R (R (R (R (R (L      (Tag (Id (I x) :*: Id (I e))))))))) =  x := e
  to (R (R (R (R (R (R (L   (Tag (Id (I c) :*: Id (I d))))))))))=  Seq c d

  ix  =  Decl

instance Ix AST Var where

  from x           =  R (R (R (R (R (R (R(Tag (K x))))))))

  to (R (R (R (R (R (R (R(Tag (K x)))))))))           =  x

  ix  =  Var