module LambdaCube.SystemF.Evaluator ( evaluate ) where import LambdaCube.SystemF.Ast import LambdaCube.SystemF.Substitution evaluate :: LCTerm -> LCValue evaluate :: LCTerm -> LCValue evaluate = LCTerm -> LCValue go where go :: LCTerm -> LCValue go (LCVar Int _) = [Char] -> LCValue forall a. HasCallStack => [Char] -> a error [Char] "Did you really type check this?" go (LCLam LCType t LCTerm b) = LCType -> LCTerm -> LCValue LCValLam LCType t LCTerm b go (LCApp LCTerm f LCTerm a) | LCValLam LCType _ LCTerm b <- LCTerm -> LCValue go LCTerm f , LCValue v <- LCTerm -> LCValue go LCTerm a = LCTerm -> LCValue go (LCTerm -> LCValue) -> LCTerm -> LCValue forall a b. (a -> b) -> a -> b $ LCValue -> Int -> LCTerm -> LCTerm substituteValue LCValue v Int 0 LCTerm b | Bool otherwise = [Char] -> LCValue forall a. HasCallStack => [Char] -> a error [Char] "Did you really type check this?" go (LCTLam LCTerm b) = LCTerm -> LCValue LCValTLam LCTerm b go (LCTApp LCTerm f LCType t) | LCValTLam LCTerm b <- LCTerm -> LCValue go LCTerm f = LCTerm -> LCValue go (LCTerm -> LCValue) -> LCTerm -> LCValue forall a b. (a -> b) -> a -> b $ LCType -> Int -> LCTerm -> LCTerm substituteType LCType t Int 0 LCTerm b | Bool otherwise = [Char] -> LCValue forall a. HasCallStack => [Char] -> a error [Char] "Did you really type check this?"