module LambdaCube.SystemF.Lifter ( liftLCValue , liftLCNormal ) where import LambdaCube.SystemF.Ast liftLCValue :: LCValue -> LCTerm liftLCValue :: LCValue -> LCTerm liftLCValue (LCValLam LCType t LCTerm b) = LCType -> LCTerm -> LCTerm LCLam LCType t LCTerm b liftLCValue (LCValTLam LCTerm b) = LCTerm -> LCTerm LCTLam LCTerm b liftLCNormal :: LCNormalTerm -> LCTerm liftLCNormal :: LCNormalTerm -> LCTerm liftLCNormal (LCNormLam LCType t LCNormalTerm b) = LCType -> LCTerm -> LCTerm LCLam LCType t (LCTerm -> LCTerm) -> LCTerm -> LCTerm forall a b. (a -> b) -> a -> b $ LCNormalTerm -> LCTerm liftLCNormal LCNormalTerm b liftLCNormal (LCNormTLam LCNormalTerm b) = LCTerm -> LCTerm LCTLam (LCTerm -> LCTerm) -> LCTerm -> LCTerm forall a b. (a -> b) -> a -> b $ LCNormalTerm -> LCTerm liftLCNormal LCNormalTerm b liftLCNormal (LCNormNeut LCNeutralTerm nt) = LCNeutralTerm -> LCTerm liftLCNeutral LCNeutralTerm nt liftLCNeutral :: LCNeutralTerm -> LCTerm liftLCNeutral :: LCNeutralTerm -> LCTerm liftLCNeutral (LCNeutVar Int x) = Int -> LCTerm LCVar Int x liftLCNeutral (LCNeutApp LCNeutralTerm f LCNormalTerm a) = LCNeutralTerm -> LCTerm liftLCNeutral LCNeutralTerm f LCTerm -> LCTerm -> LCTerm `LCApp` LCNormalTerm -> LCTerm liftLCNormal LCNormalTerm a liftLCNeutral (LCNeutTApp LCNeutralTerm f LCType t) = LCNeutralTerm -> LCTerm liftLCNeutral LCNeutralTerm f LCTerm -> LCType -> LCTerm `LCTApp` LCType t