module LambdaCube.SystemFw_.Evaluator where

import           LambdaCube.SystemFw_.Ast

liftLCValue :: LCValue -> LCTerm
liftLCValue (LCValLam t b) = LCLam t b

substitute :: Int -> LCValue -> LCTerm -> LCTerm
substitute n v = go n
  where
    go m e@(LCVar l) = if m == l then liftLCValue v else e
    go m (LCLam t b) = LCLam t (substitute (m + 1) v b)
    go m (LCApp f a) = LCApp (go m f) (go m a)

evaluate :: LCTerm -> LCValue
evaluate = go
  where
    go (LCVar _) = error "Did you really type check this?"
    go (LCLam t b) = LCValLam t b
    go (LCApp f a)
      | LCValLam _ b <- go f
      , v <- go a
      = go (substitute 0 v b)
      | otherwise
      = error "Did you really type check this?"