module LambdaCube.SystemFw_.Elaborator
  ( elaborate
  , elaborateType
  , elaborateKind
  ) where

import           Data.List                (elemIndex)
import qualified Data.Text                as Text
import           LambdaCube.SystemFw_.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
n <- Text
x Text -> [Text] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
`elemIndex` [Text]
l
      = 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]
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 = [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 (ExtLCTTLam Text
p ExtLCKind
k ExtLCType
b) = LCKind -> LCType -> LCType
LCTTLam (ExtLCKind -> LCKind
elaborateKind ExtLCKind
k) (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
b
    go [Text]
l (ExtLCTTApp ExtLCType
f ExtLCType
a) = [Text] -> ExtLCType -> LCType
go [Text]
l ExtLCType
f LCType -> LCType -> LCType
`LCTTApp` [Text] -> ExtLCType -> LCType
go [Text]
l ExtLCType
a
    go [Text]
_ (ExtLCMTVar [Char]
_) = [Char] -> LCType
forall a. HasCallStack => [Char] -> a
error [Char]
"invalid TemplateHaskell code splicer"

elaborateKind :: ExtLCKind -> LCKind
elaborateKind :: ExtLCKind -> LCKind
elaborateKind = ExtLCKind -> LCKind
go
  where
    go :: ExtLCKind -> LCKind
go ExtLCKind
ExtLCStar = LCKind
LCStar
    go (ExtLCKArr ExtLCKind
a ExtLCKind
b) = ExtLCKind -> LCKind
go ExtLCKind
a LCKind -> LCKind -> LCKind
`LCKArr` ExtLCKind -> LCKind
go ExtLCKind
b
    go (ExtLCMKVar [Char]
_) = [Char] -> LCKind
forall a. HasCallStack => [Char] -> a
error [Char]
"invalid TemplateHaskell code splicer"