module LambdaCube.SystemFw_.Normalizer
  ( normalize
  ) 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
x) = LCNeutralTerm -> LCNormalTerm
LCNormNeut (LCNeutralTerm -> LCNormalTerm) -> LCNeutralTerm -> LCNormalTerm
forall a b. (a -> b) -> a -> b
$ Int -> LCNeutralTerm
LCNeutVar Int
x
    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 -> LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm
substituteNormalInNormal LCNormalTerm
a' Int
0 LCNormalTerm
b
        LCNormNeut LCNeutralTerm
nt -> LCNeutralTerm -> LCNormalTerm
LCNormNeut (LCNeutralTerm -> LCNormalTerm) -> LCNeutralTerm -> LCNormalTerm
forall a b. (a -> b) -> a -> b
$ LCNeutralTerm
nt LCNeutralTerm -> LCNormalTerm -> LCNeutralTerm
`LCNeutApp` LCNormalTerm
a'
      where
        a' :: LCNormalTerm
a' = LCTerm -> LCNormalTerm
go LCTerm
a