module LambdaCube.SystemFw_.Normalizer where

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

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