module LambdaCube.SystemF.Normalizer where

import           LambdaCube.SystemF.Ast
import           LambdaCube.SystemF.Substitution

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