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