lambda-cube-0.1.0.0: src/LambdaCube/STLC/Elaborator.hs

module LambdaCube.STLC.Elaborator where

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

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