{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}

module Expr where

import Generics.Annotations.ShowFam

import Generics.MultiRec.Base
import Generics.MultiRec.TH

import Control.Monad.Either

import FoldEAlgK

data Expr
  = EAdd     Expr  Expr
  | EMul     Expr  Expr
  | ETup     Expr  Expr
  | EIntLit  Int
  | ETyped   Expr  Type
  deriving (Eq, Show)

data Type
  = TyInt
  | TyTup  Type Type
  deriving (Eq, Show)

data AST :: * -> * where
  Expr  :: AST Expr
  Type  :: AST Type

instance ShowFam AST where
  showFam Expr  = show
  showFam Type     = show

$(deriveConstructors [''Expr, ''Type])
$(deriveFamily ''AST [''Expr, ''Type] "PFAST")
type instance PF AST = PFAST

inferType :: ErrorAlgebra (PF AST) String Type
inferType = ( equal "+" & equal "*" & tup & const (Right TyInt) & equal "::" )
          & ( Right TyInt & tup )
  where
    equal op ty1 ty2
      | ty1 == ty2 = Right ty1
      | otherwise  = Left ("lhs and rhs of " ++ op ++ " must have equal types")
    tup ty1 ty2 = Right (TyTup ty1 ty2)