module LambdaCube.SystemF.TypeChecker where

import           Data.List                       (uncons)
import           LambdaCube.SystemF.Ast
import           LambdaCube.SystemF.Substitution

infer :: LCTerm -> LCType
infer :: LCTerm -> LCType
infer = [LCType] -> LCTerm -> LCType
go []
  where
    go :: [LCType] -> LCTerm -> LCType
go [LCType]
tl (LCVar Int
n) = LCType
-> ((LCType, [LCType]) -> LCType)
-> Maybe (LCType, [LCType])
-> LCType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Char] -> LCType
forall a. HasCallStack => [Char] -> a
error [Char]
"Out-of-scope variable") (LCType, [LCType]) -> LCType
forall a b. (a, b) -> a
fst (Maybe (LCType, [LCType]) -> LCType)
-> ([LCType] -> Maybe (LCType, [LCType])) -> [LCType] -> LCType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LCType] -> Maybe (LCType, [LCType])
forall a. [a] -> Maybe (a, [a])
uncons ([LCType] -> LCType) -> [LCType] -> LCType
forall a b. (a -> b) -> a -> b
$ Int -> [LCType] -> [LCType]
forall a. Int -> [a] -> [a]
drop Int
n [LCType]
tl
    go [LCType]
tl (LCLam LCType
t LCTerm
b) = LCType
t LCType -> LCType -> LCType
`LCArr` [LCType] -> LCTerm -> LCType
go (LCType
t LCType -> [LCType] -> [LCType]
forall a. a -> [a] -> [a]
: [LCType]
tl) LCTerm
b
    go [LCType]
tl (LCApp LCTerm
f LCTerm
a)
      | LCArr LCType
at LCType
rt <- [LCType] -> LCTerm -> LCType
go [LCType]
tl LCTerm
f
      , LCType
at LCType -> LCType -> Bool
forall a. Eq a => a -> a -> Bool
== [LCType] -> LCTerm -> LCType
go [LCType]
tl LCTerm
a
      = LCType
rt
      | Bool
otherwise
      = [Char] -> LCType
forall a. HasCallStack => [Char] -> a
error [Char]
"Function argument type mismatch"
    go [LCType]
tl (LCTLam LCTerm
b) = LCType -> LCType
LCUniv (LCType -> LCType) -> LCType -> LCType
forall a b. (a -> b) -> a -> b
$ [LCType] -> LCTerm -> LCType
go [LCType]
tl LCTerm
b
    go [LCType]
tl (LCTApp LCTerm
f LCType
t)
      | LCUniv LCType
rt <- [LCType] -> LCTerm -> LCType
go [LCType]
tl LCTerm
f
      = Int -> LCType -> LCType -> LCType
substituteTypeInType Int
0 LCType
t LCType
rt
      | Bool
otherwise
      = [Char] -> LCType
forall a. HasCallStack => [Char] -> a
error [Char]
"Function argument type mismatch"