module LambdaCube.STLC.Elaborator where

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

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 String
_) = String -> LCType
forall a. HasCallStack => String -> a
error String
"invalid TemplateHaskell code splicer"

elaborate :: ExtLCTerm -> LCTerm
elaborate :: ExtLCTerm -> LCTerm
elaborate = [Text] -> ExtLCTerm -> LCTerm
go []
  where
    go :: [Text] -> ExtLCTerm -> LCTerm
go [Text]
l (ExtLCVar Text
v)
      | Just Int
idx <- Text
v Text -> [Text] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
`elemIndex` [Text]
l
      = Int -> LCTerm
LCVar Int
idx
      | Bool
otherwise
      = String -> LCTerm
forall a. HasCallStack => String -> a
error (String -> LCTerm) -> String -> LCTerm
forall a b. (a -> b) -> a -> b
$ String
"Variable " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Text -> String
Text.unpack Text
v String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" is not in scope"
    go [Text]
l (ExtLCLam Text
v 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
v 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 String
_) = String -> LCTerm
forall a. HasCallStack => String -> a
error String
"invalid TemplateHaskell code splicer"