module LambdaCube.SystemFw.Normalizer where

import           LambdaCube.SystemFw.Ast
import           LambdaCube.SystemFw.Substitution

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
t (LCNormalTerm -> LCNormalTerm) -> LCNormalTerm -> LCNormalTerm
forall a b. (a -> b) -> a -> b
$ LCTerm -> LCNormalTerm
go LCTerm
b
    go (LCTLam LCKind
k LCTerm
b) = LCKind -> LCNormalTerm -> LCNormalTerm
LCNormTLam LCKind
k (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
        LCNormTLam LCKind
_ LCNormalTerm
_  -> [Char] -> LCNormalTerm
forall a. HasCallStack => [Char] -> a
error [Char]
"Did you really type check this?"
        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
    go (LCTApp LCTerm
f LCType
t) =
      case LCTerm -> LCNormalTerm
go LCTerm
f of
        LCNormLam LCType
_ LCNormalTerm
_   -> [Char] -> LCNormalTerm
forall a. HasCallStack => [Char] -> a
error [Char]
"Did you really type check this?"
        LCNormTLam LCKind
_ LCNormalTerm
b  -> Int -> LCType -> LCNormalTerm -> LCNormalTerm
substituteTypeInNormal Int
0 LCType
t LCNormalTerm
b
        LCNormNeut LCNeutralTerm
neut -> LCNeutralTerm -> LCNormalTerm
LCNormNeut (LCNeutralTerm -> LCNormalTerm) -> LCNeutralTerm -> LCNormalTerm
forall a b. (a -> b) -> a -> b
$ LCNeutralTerm
neut LCNeutralTerm -> LCType -> LCNeutralTerm
`LCNeutTApp` LCType
t