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

module AST where

import Base
import ShowFam

-------------------------------------------------------------------------------
-- a system of mutually recursive types for representing abstract syntax
-------------------------------------------------------------------------------

infix 1 :=

type Var  = String
data Decl = Var := Exp deriving Show
data Exp  = Var Var | Abs Var Exp | App Exp Exp | Let Decl Exp deriving Show

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

data AST :: * -> * where
  Decl :: AST Decl
  Exp  :: AST Exp

type instance PF AST = K Var   :*: Id Exp  ::: Decl  :+:    -- (:=)
                       K Var               ::: Exp   :+:    -- Var
                       K Var   :*: Id Exp  ::: Exp   :+:    -- Abs
                       Id Exp  :*: Id Exp  ::: Exp   :+:    -- App
                       Id Decl :*: Id Exp  ::: Exp          -- Let

instance Ix AST Decl where
  ix                              = Decl
  from (x := e)                   = L (Tag (K x :*: Id (I e)))
  to (L (Tag (K x :*: Id (I e)))) = x := e
 
instance Ix AST Exp where
  ix                                      = Exp

  from (Var x    )                        = R(L     (Tag (K x            )))
  from (Abs x  e )                        = R(R(L   (Tag (K x       :*: Id (I e )))))
  from (App e1 e2)                        = R(R(R(L (Tag (Id (I e1) :*: Id (I e2))))))
  from (Let d  e )                        = R(R(R(R (Tag (Id (I d)  :*: Id (I e ))))))

  to (R(L     (Tag (K x                      )))) = Var x
  to (R(R(L   (Tag (K x       :*: Id (I e)  ))))) = Abs x  e
  to (R(R(R(L (Tag (Id (I e1) :*: Id (I e2))))))) = App e1 e2 
  to (R(R(R(R (Tag (Id (I d)  :*: Id (I e) )))))) = Let d  e

-------------------------------------------------------------------------------
-- pretty printing
-------------------------------------------------------------------------------

instance ShowFam AST where
  showFam Decl = show
  showFam Exp  = show