module LambdaCube.SystemF.Evaluator 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
$ Int -> LCValue -> LCTerm -> LCTerm
substituteValue Int
0 LCValue
v 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
$ Int -> LCType -> LCTerm -> LCTerm
substituteType Int
0 LCType
t LCTerm
b
      | Bool
otherwise
      = [Char] -> LCValue
forall a. HasCallStack => [Char] -> a
error [Char]
"Did you really type check this?"