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

import           Data.List               (elemIndex)
import           Data.Text               (Text)
import qualified Data.Text               as Text
import           LambdaCube.SystemFw.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 ExtLCKind
k ExtLCTerm
b) = LCKind -> LCTerm -> LCTerm
LCTLam (ExtLCKind -> LCKind
elaborateKind ExtLCKind
k) (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 ExtLCKind
k ExtLCType
a) = LCKind -> LCType -> LCType
LCUniv (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
a
    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"