module LambdaCube.SystemFw.Normalizer ( normalize ) 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 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 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 -> LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm substituteNormalInNormal LCNormalTerm a' Int 0 LCNormalTerm b LCNormTLam LCKind _ 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 LCKind _ 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