module LambdaCube.SystemFw_.Evaluator where

import           LambdaCube.SystemFw_.Ast
import           LambdaCube.SystemFw_.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 (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?"