module LambdaCube.SystemFw_.Normalizer where

import           LambdaCube.SystemFw_.Ast
import           LambdaCube.SystemFw_.TypeChecker (reduceType)

substituteNormal :: Int -> LCNormalTerm -> LCNormalTerm -> LCNormalTerm
substituteNormal n v = go n
  where
    go m (LCNormLam t b) = LCNormLam t $ go (m + 1) b
    go m (LCNormNeut nt) = substituteNeutral m v nt

substituteNeutral :: Int -> LCNormalTerm -> LCNeutralTerm -> LCNormalTerm
substituteNeutral n v = go n
  where
    go m e@(LCNeutVar l) = if m == l then v else LCNormNeut e
    go m (LCNeutApp f a) =
      case go m f of
        LCNormLam _ b -> substituteNormal 0 a' b
        LCNormNeut nt -> LCNormNeut $ nt `LCNeutApp` a'
      where
        a' = substituteNormal m v a

normalize :: LCTerm -> LCNormalTerm
normalize = go
  where
    go (LCVar n) = LCNormNeut $ LCNeutVar n
    go (LCLam t b) = LCNormLam (reduceType t) $ go b
    go (LCApp f a) =
      case go f of
        LCNormLam _ b   -> substituteNormal 0 a' b
        LCNormNeut neut -> LCNormNeut $ neut `LCNeutApp` a'
      where
        a' = go a