module LambdaCube.STLC.Elaborator ( elaborate , elaborateType ) where import Data.List (elemIndex) import qualified Data.Text as Text import LambdaCube.STLC.Ast elaborate :: ExtLCTerm -> LCTerm elaborate :: ExtLCTerm -> LCTerm elaborate = [Text] -> ExtLCTerm -> LCTerm go [] where go :: [Text] -> ExtLCTerm -> LCTerm go [Text] l (ExtLCVar Text x) | Just Int idx <- Text x Text -> [Text] -> Maybe Int forall a. Eq a => a -> [a] -> Maybe Int `elemIndex` [Text] l = Int -> LCTerm LCVar Int idx | Bool otherwise = [Char] -> LCTerm forall a. HasCallStack => [Char] -> a error ([Char] -> LCTerm) -> [Char] -> LCTerm forall a b. (a -> b) -> a -> b $ [Char] "Variable " [Char] -> [Char] -> [Char] forall a. Semigroup a => a -> a -> a <> Text -> [Char] Text.unpack Text x [Char] -> [Char] -> [Char] forall a. Semigroup a => a -> a -> a <> [Char] " is not in scope" go [Text] l (ExtLCLam Text x ExtLCType t ExtLCTerm b) = LCType -> LCTerm -> LCTerm LCLam (ExtLCType -> LCType elaborateType ExtLCType t) (LCTerm -> LCTerm) -> LCTerm -> LCTerm forall a b. (a -> b) -> a -> b $ [Text] -> ExtLCTerm -> LCTerm go (Text x Text -> [Text] -> [Text] forall a. a -> [a] -> [a] : [Text] l) ExtLCTerm b go [Text] l (ExtLCApp ExtLCTerm f ExtLCTerm a) = [Text] -> ExtLCTerm -> LCTerm go [Text] l ExtLCTerm f LCTerm -> LCTerm -> LCTerm `LCApp` [Text] -> ExtLCTerm -> LCTerm go [Text] l ExtLCTerm a go [Text] _ (ExtLCMVar [Char] _) = [Char] -> LCTerm forall a. HasCallStack => [Char] -> a error [Char] "invalid TemplateHaskell code splicer" elaborateType :: ExtLCType -> LCType elaborateType :: ExtLCType -> LCType elaborateType = ExtLCType -> LCType go where go :: ExtLCType -> LCType go ExtLCType ExtLCBase = LCType LCBase go (ExtLCArr ExtLCType a ExtLCType b) = ExtLCType -> LCType go ExtLCType a LCType -> LCType -> LCType `LCArr` ExtLCType -> LCType go ExtLCType b go (ExtLCMTVar [Char] _) = [Char] -> LCType forall a. HasCallStack => [Char] -> a error [Char] "invalid TemplateHaskell code splicer"