module LambdaCube.SystemF.Elaborator
  ( elaborate
  , elaborateType
  ) where

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

elaborate :: ExtLCTerm -> LCTerm
elaborate :: ExtLCTerm -> LCTerm
elaborate = [Text] -> [Text] -> ExtLCTerm -> LCTerm
go [] []
  where
    go :: [Text] -> [Text] -> ExtLCTerm -> LCTerm
go [Text]
_  [Text]
vl (ExtLCVar Text
x)
      | Just Int
n <- Text
x Text -> [Text] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
`elemIndex` [Text]
vl
      = Int -> LCTerm
LCVar Int
n
      | Bool
otherwise
      = [Char] -> LCTerm
forall a. HasCallStack => [Char] -> a
error ([Char] -> LCTerm) -> [Char] -> LCTerm
forall a b. (a -> b) -> a -> b
$ [Char]
"Term 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]
tl [Text]
vl (ExtLCLam Text
x ExtLCType
t ExtLCTerm
b) = LCType -> LCTerm -> LCTerm
LCLam ([Text] -> ExtLCType -> LCType
elaborateType [Text]
tl ExtLCType
t) (LCTerm -> LCTerm) -> LCTerm -> LCTerm
forall a b. (a -> b) -> a -> b
$ [Text] -> [Text] -> ExtLCTerm -> LCTerm
go [Text]
tl (Text
x Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
vl) ExtLCTerm
b
    go [Text]
tl [Text]
vl (ExtLCApp ExtLCTerm
f ExtLCTerm
a) = [Text] -> [Text] -> ExtLCTerm -> LCTerm
go [Text]
tl [Text]
vl ExtLCTerm
f LCTerm -> LCTerm -> LCTerm
`LCApp` [Text] -> [Text] -> ExtLCTerm -> LCTerm
go [Text]
tl [Text]
vl ExtLCTerm
a
    go [Text]
tl [Text]
vl (ExtLCTLam Text
p ExtLCTerm
b) = LCTerm -> LCTerm
LCTLam (LCTerm -> LCTerm) -> LCTerm -> LCTerm
forall a b. (a -> b) -> a -> b
$ [Text] -> [Text] -> ExtLCTerm -> LCTerm
go (Text
p Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
tl) [Text]
vl ExtLCTerm
b
    go [Text]
tl [Text]
vl (ExtLCTApp ExtLCTerm
f ExtLCType
t) = [Text] -> [Text] -> ExtLCTerm -> LCTerm
go [Text]
tl [Text]
vl ExtLCTerm
f LCTerm -> LCType -> LCTerm
`LCTApp` [Text] -> ExtLCType -> LCType
elaborateType [Text]
tl ExtLCType
t
    go [Text]
_  [Text]
_  (ExtLCMVar [Char]
_) = [Char] -> LCTerm
forall a. HasCallStack => [Char] -> a
error [Char]
"invalid TemplateHaskell code splicer"

elaborateType :: [Text] -> ExtLCType -> LCType
elaborateType :: [Text] -> ExtLCType -> LCType
elaborateType = [Text] -> ExtLCType -> LCType
go
  where
    go :: [Text] -> ExtLCType -> LCType
go [Text]
_ ExtLCType
ExtLCBase = LCType
LCBase
    go [Text]
l (ExtLCTVar Text
p)
      | Just Int
n <- Text
p Text -> [Text] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
`elemIndex` [Text]
l
      = Int -> LCType
LCTVar Int
n
      | Bool
otherwise
      = [Char] -> LCType
forall a. HasCallStack => [Char] -> a
error ([Char] -> LCType) -> [Char] -> LCType
forall a b. (a -> b) -> a -> b
$ [Char]
"Type variable " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
Text.unpack Text
p [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" is not in scope"
    go [Text]
l (ExtLCArr ExtLCType
a ExtLCType
b) = [Text] -> ExtLCType -> LCType
go [Text]
l ExtLCType
a LCType -> LCType -> LCType
`LCArr` [Text] -> ExtLCType -> LCType
go [Text]
l ExtLCType
b
    go [Text]
l (ExtLCUniv Text
p ExtLCType
a) = LCType -> LCType
LCUniv (LCType -> LCType) -> LCType -> LCType
forall a b. (a -> b) -> a -> b
$ [Text] -> ExtLCType -> LCType
go (Text
p Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
l) ExtLCType
a
    go [Text]
_ (ExtLCMTVar [Char]
_) = [Char] -> LCType
forall a. HasCallStack => [Char] -> a
error [Char]
"invalid TemplateHaskell code splicer"