Elaborator.hs

module LambdaCube.SystemFw_.Elaborator where

import           Data.List                (elemIndex)
import qualified Data.Text                as Text
import           LambdaCube.SystemFw_.Ast

elaborate :: ExtLCTerm -> Either String LCTerm
elaborate = go []
  where
    go l (ExtLCVar x)
      | Just n <- x `elemIndex` l
      = Right $ LCVar n
      | otherwise
      = Left $ "Term variable " <> Text.unpack x <> " is not in scope"
    go l (ExtLCLam x t b) = LCLam <$> typeElaborate t <*> go (x : l) b
    go l (ExtLCApp f a) = LCApp <$> go l f <*> go l a

typeElaborate :: ExtLCType -> Either String LCType
typeElaborate = go []
  where
    go _ ExtLCBase = Right LCBase
    go l (ExtLCTVar x)
      | Just n <- x `elemIndex` l
      = Right $ LCTVar n
      | otherwise
      = Left  $ "Type variable " <> Text.unpack x <> " is not in scope"
    go l (ExtLCArr a b) = LCArr <$> go l a <*> go l b
    go l (ExtLCTTLam x k b) = LCTTLam k <$> go (x : l) b
    go l (ExtLCTTApp f a) = LCTTApp <$> go l f <*> go l a