module LambdaCube.SystemF.TypeChecker ( infer ) 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 x) = 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 x [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 -> LCType) -> [LCType] -> [LCType] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap ((LCType, Int) -> LCType shiftType ((LCType, Int) -> LCType) -> (LCType -> (LCType, Int)) -> LCType -> LCType forall b c a. (b -> c) -> (a -> b) -> a -> c . (, Int 1)) [LCType] tl) LCTerm b go [LCType] tl (LCTApp LCTerm f LCType t) | LCUniv LCType rt <- [LCType] -> LCTerm -> LCType go [LCType] tl LCTerm f = LCType -> Int -> LCType -> LCType substituteTypeInType LCType t Int 0 LCType rt | Bool otherwise = [Char] -> LCType forall a. HasCallStack => [Char] -> a error [Char] "Function argument type mismatch"