{-# LANGUAGE ViewPatterns #-} module LambdaCube.SystemF.Substitution ( substituteType , substituteTypeInType , substituteValue , substituteNormalInNormal , substituteTypeInNormal , shiftType ) where import LambdaCube.SystemF.Ast import LambdaCube.SystemF.Lifter substituteType :: LCType -> Int -> LCTerm -> LCTerm substituteType :: LCType -> Int -> LCTerm -> LCTerm substituteType LCType v = (LCType, Int) -> Int -> LCTerm -> LCTerm substDefType (LCType v, Int 0) substituteTypeInType :: LCType -> Int -> LCType -> LCType substituteTypeInType :: LCType -> Int -> LCType -> LCType substituteTypeInType LCType v = (LCType, Int) -> Int -> LCType -> LCType substDefTypeInType (LCType v, Int 0) substituteValue :: LCValue -> Int -> LCTerm -> LCTerm substituteValue :: LCValue -> Int -> LCTerm -> LCTerm substituteValue LCValue v = (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm substDefValue (LCValue v, Int 0, Int 0) substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm substituteNormalInNormal LCNormalTerm v = (LCNormalTerm, Int, Int) -> Int -> LCNormalTerm -> LCNormalTerm substDefNormalInNormal (LCNormalTerm v, Int 0, Int 0) substituteTypeInNormal :: LCType -> Int -> LCNormalTerm -> LCNormalTerm substituteTypeInNormal :: LCType -> Int -> LCNormalTerm -> LCNormalTerm substituteTypeInNormal LCType v = (LCType, Int) -> Int -> LCNormalTerm -> LCNormalTerm substDefTypeInNormal (LCType v, Int 0) substDefType :: (LCType, Int) -> Int -> LCTerm -> LCTerm substDefType :: (LCType, Int) -> Int -> LCTerm -> LCTerm substDefType = (LCType, Int) -> Int -> LCTerm -> LCTerm go where go :: (LCType, Int) -> Int -> LCTerm -> LCTerm go (LCType, Int) _ Int _ e :: LCTerm e@(LCVar Int _) = LCTerm e go (LCType, Int) dv Int p (LCLam LCType t LCTerm b) = LCType -> LCTerm -> LCTerm LCLam ((LCType, Int) -> Int -> LCType -> LCType substDefTypeInType (LCType, Int) dv Int p LCType t) (LCTerm -> LCTerm) -> LCTerm -> LCTerm forall a b. (a -> b) -> a -> b $ (LCType, Int) -> Int -> LCTerm -> LCTerm go (LCType, Int) dv Int p LCTerm b go (LCType, Int) dv Int p (LCApp LCTerm f LCTerm a) = (LCType, Int) -> Int -> LCTerm -> LCTerm go (LCType, Int) dv Int p LCTerm f LCTerm -> LCTerm -> LCTerm `LCApp` (LCType, Int) -> Int -> LCTerm -> LCTerm go (LCType, Int) dv Int p LCTerm a go (LCType v, Int r) Int p (LCTLam LCTerm b) = LCTerm -> LCTerm LCTLam (LCTerm -> LCTerm) -> LCTerm -> LCTerm forall a b. (a -> b) -> a -> b $ (LCType, Int) -> Int -> LCTerm -> LCTerm go (LCType v, Int r Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) (Int p Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) LCTerm b go (LCType, Int) dv Int p (LCTApp LCTerm f LCType t) = (LCType, Int) -> Int -> LCTerm -> LCTerm go (LCType, Int) dv Int p LCTerm f LCTerm -> LCType -> LCTerm `LCTApp` (LCType, Int) -> Int -> LCType -> LCType substDefTypeInType (LCType, Int) dv Int p LCType t substDefTypeInType :: (LCType, Int) -> Int -> LCType -> LCType substDefTypeInType :: (LCType, Int) -> Int -> LCType -> LCType substDefTypeInType = (LCType, Int) -> Int -> LCType -> LCType go where go :: (LCType, Int) -> Int -> LCType -> LCType go (LCType, Int) _ Int _ LCType LCBase = LCType LCBase go (LCType, Int) dv Int p (LCTVar ((Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == Int p) -> Bool True)) = (LCType, Int) -> LCType shiftType (LCType, Int) dv go (LCType, Int) _ Int p e :: LCType e@(LCTVar ((Int -> Int -> Bool forall a. Ord a => a -> a -> Bool < Int p) -> Bool True)) = LCType e go (LCType, Int) _ Int _ (LCTVar Int q) = Int -> LCType LCTVar (Int -> LCType) -> Int -> LCType forall a b. (a -> b) -> a -> b $ Int q Int -> Int -> Int forall a. Num a => a -> a -> a - Int 1 go (LCType, Int) dv Int p (LCArr LCType a LCType b) = (LCType, Int) -> Int -> LCType -> LCType go (LCType, Int) dv Int p LCType a LCType -> LCType -> LCType `LCArr` (LCType, Int) -> Int -> LCType -> LCType go (LCType, Int) dv Int p LCType b go (LCType v, Int r) Int p (LCUniv LCType a) = LCType -> LCType LCUniv (LCType -> LCType) -> LCType -> LCType forall a b. (a -> b) -> a -> b $ (LCType, Int) -> Int -> LCType -> LCType go (LCType v, Int r Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) (Int p Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) LCType a substDefValue :: (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm substDefValue :: (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm substDefValue = (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm go where go :: (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm go (LCValue, Int, Int) dv Int x (LCVar ((Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == Int x) -> Bool True)) = (LCValue, Int, Int) -> LCTerm shiftValue (LCValue, Int, Int) dv go (LCValue, Int, Int) _ Int x e :: LCTerm e@(LCVar ((Int -> Int -> Bool forall a. Ord a => a -> a -> Bool < Int x) -> Bool True)) = LCTerm e go (LCValue, Int, Int) _ Int _ (LCVar Int y) = Int -> LCTerm LCVar (Int -> LCTerm) -> Int -> LCTerm forall a b. (a -> b) -> a -> b $ Int y Int -> Int -> Int forall a. Num a => a -> a -> a - Int 1 go (LCValue v, Int r, Int s) Int x (LCLam LCType t LCTerm b) = LCType -> LCTerm -> LCTerm LCLam LCType t (LCTerm -> LCTerm) -> LCTerm -> LCTerm forall a b. (a -> b) -> a -> b $ (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm go (LCValue v, Int r, Int s Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) (Int x Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) LCTerm b go (LCValue, Int, Int) dv Int x (LCApp LCTerm f LCTerm a) = (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm go (LCValue, Int, Int) dv Int x LCTerm f LCTerm -> LCTerm -> LCTerm `LCApp` (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm go (LCValue, Int, Int) dv Int x LCTerm a go (LCValue v, Int r, Int s) Int x (LCTLam LCTerm b) = LCTerm -> LCTerm LCTLam (LCTerm -> LCTerm) -> LCTerm -> LCTerm forall a b. (a -> b) -> a -> b $ (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm go (LCValue v, Int r Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1, Int s) Int x LCTerm b go (LCValue, Int, Int) dv Int x (LCTApp LCTerm f LCType t) = (LCValue, Int, Int) -> Int -> LCTerm -> LCTerm go (LCValue, Int, Int) dv Int x LCTerm f LCTerm -> LCType -> LCTerm `LCTApp` LCType t substDefNormalInNormal :: (LCNormalTerm, Int, Int) -> Int -> LCNormalTerm -> LCNormalTerm substDefNormalInNormal :: (LCNormalTerm, Int, Int) -> Int -> LCNormalTerm -> LCNormalTerm substDefNormalInNormal = (LCNormalTerm, Int, Int) -> Int -> LCNormalTerm -> LCNormalTerm go where go :: (LCNormalTerm, Int, Int) -> Int -> LCNormalTerm -> LCNormalTerm go (LCNormalTerm v, Int r, Int s) Int x (LCNormLam LCType t LCNormalTerm b) = LCType -> LCNormalTerm -> LCNormalTerm LCNormLam LCType t (LCNormalTerm -> LCNormalTerm) -> LCNormalTerm -> LCNormalTerm forall a b. (a -> b) -> a -> b $ (LCNormalTerm, Int, Int) -> Int -> LCNormalTerm -> LCNormalTerm go (LCNormalTerm v, Int r, Int s Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) (Int x Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) LCNormalTerm b go (LCNormalTerm v, Int r, Int s) Int x (LCNormTLam LCNormalTerm b) = LCNormalTerm -> LCNormalTerm LCNormTLam (LCNormalTerm -> LCNormalTerm) -> LCNormalTerm -> LCNormalTerm forall a b. (a -> b) -> a -> b $ (LCNormalTerm, Int, Int) -> Int -> LCNormalTerm -> LCNormalTerm go (LCNormalTerm v, Int r Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1, Int s) Int x LCNormalTerm b go (LCNormalTerm, Int, Int) dv Int x (LCNormNeut LCNeutralTerm nt) = (LCNormalTerm, Int, Int) -> Int -> LCNeutralTerm -> LCNormalTerm substDefNormalInNeutral (LCNormalTerm, Int, Int) dv Int x LCNeutralTerm nt substDefNormalInNeutral :: (LCNormalTerm, Int, Int) -> Int -> LCNeutralTerm -> LCNormalTerm substDefNormalInNeutral :: (LCNormalTerm, Int, Int) -> Int -> LCNeutralTerm -> LCNormalTerm substDefNormalInNeutral (LCNormalTerm, Int, Int) dv Int x = LCNeutralTerm -> LCNormalTerm go where go :: LCNeutralTerm -> LCNormalTerm go (LCNeutVar ((Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == Int x) -> Bool True)) = (LCNormalTerm, Int, Int) -> LCNormalTerm shiftNormal (LCNormalTerm, Int, Int) dv go e :: LCNeutralTerm e@(LCNeutVar ((Int -> Int -> Bool forall a. Ord a => a -> a -> Bool < Int x) -> Bool True)) = LCNeutralTerm -> LCNormalTerm LCNormNeut LCNeutralTerm e go (LCNeutVar Int y) = LCNeutralTerm -> LCNormalTerm LCNormNeut (LCNeutralTerm -> LCNormalTerm) -> (Int -> LCNeutralTerm) -> Int -> LCNormalTerm forall b c a. (b -> c) -> (a -> b) -> a -> c . Int -> LCNeutralTerm LCNeutVar (Int -> LCNormalTerm) -> Int -> LCNormalTerm forall a b. (a -> b) -> a -> b $ Int y Int -> Int -> Int forall a. Num a => a -> a -> a - Int 1 go (LCNeutApp LCNeutralTerm f LCNormalTerm a) = case LCNeutralTerm -> LCNormalTerm go LCNeutralTerm 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' = (LCNormalTerm, Int, Int) -> Int -> LCNormalTerm -> LCNormalTerm substDefNormalInNormal (LCNormalTerm, Int, Int) dv Int x LCNormalTerm a go (LCNeutTApp LCNeutralTerm f LCType t) = case LCNeutralTerm -> LCNormalTerm go LCNeutralTerm 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 substDefTypeInNormal :: (LCType, Int) -> Int -> LCNormalTerm -> LCNormalTerm substDefTypeInNormal :: (LCType, Int) -> Int -> LCNormalTerm -> LCNormalTerm substDefTypeInNormal = (LCType, Int) -> Int -> LCNormalTerm -> LCNormalTerm go where go :: (LCType, Int) -> Int -> LCNormalTerm -> LCNormalTerm go (LCType, Int) dv Int p (LCNormLam LCType t LCNormalTerm b) = LCType -> LCNormalTerm -> LCNormalTerm LCNormLam ((LCType, Int) -> Int -> LCType -> LCType substDefTypeInType (LCType, Int) dv Int p LCType t) (LCNormalTerm -> LCNormalTerm) -> LCNormalTerm -> LCNormalTerm forall a b. (a -> b) -> a -> b $ (LCType, Int) -> Int -> LCNormalTerm -> LCNormalTerm go (LCType, Int) dv Int p LCNormalTerm b go (LCType v, Int r) Int p (LCNormTLam LCNormalTerm b) = LCNormalTerm -> LCNormalTerm LCNormTLam (LCNormalTerm -> LCNormalTerm) -> LCNormalTerm -> LCNormalTerm forall a b. (a -> b) -> a -> b $ (LCType, Int) -> Int -> LCNormalTerm -> LCNormalTerm go (LCType v, Int r Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) (Int p Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) LCNormalTerm b go (LCType, Int) dv Int p (LCNormNeut LCNeutralTerm nt) = (LCType, Int) -> Int -> LCNeutralTerm -> LCNormalTerm substDefTypeInNeutral (LCType, Int) dv Int p LCNeutralTerm nt substDefTypeInNeutral :: (LCType, Int) -> Int -> LCNeutralTerm -> LCNormalTerm substDefTypeInNeutral :: (LCType, Int) -> Int -> LCNeutralTerm -> LCNormalTerm substDefTypeInNeutral (LCType, Int) dv Int p = LCNeutralTerm -> LCNormalTerm go where go :: LCNeutralTerm -> LCNormalTerm go e :: LCNeutralTerm e@(LCNeutVar Int _) = LCNeutralTerm -> LCNormalTerm LCNormNeut LCNeutralTerm e go (LCNeutApp LCNeutralTerm f LCNormalTerm a) = case LCNeutralTerm -> LCNormalTerm go LCNeutralTerm 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' = (LCType, Int) -> Int -> LCNormalTerm -> LCNormalTerm substDefTypeInNormal (LCType, Int) dv Int p LCNormalTerm a go (LCNeutTApp LCNeutralTerm f LCType t) = case LCNeutralTerm -> LCNormalTerm go LCNeutralTerm 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' where t' :: LCType t' = (LCType, Int) -> Int -> LCType -> LCType substDefTypeInType (LCType, Int) dv Int p LCType t shift :: (LCTerm, Int, Int) -> LCTerm shift :: (LCTerm, Int, Int) -> LCTerm shift = Int -> Int -> (LCTerm, Int, Int) -> LCTerm shiftMin Int 0 Int 0 shiftMin :: Int -> Int -> (LCTerm, Int, Int) -> LCTerm shiftMin :: Int -> Int -> (LCTerm, Int, Int) -> LCTerm shiftMin Int m' Int n' (LCTerm v, Int r, Int s) = Int -> Int -> LCTerm -> LCTerm go Int m' Int n' LCTerm v where go :: Int -> Int -> LCTerm -> LCTerm go Int _ Int n (LCVar Int x) = Int -> LCTerm LCVar (Int -> LCTerm) -> Int -> LCTerm forall a b. (a -> b) -> a -> b $ if Int x Int -> Int -> Bool forall a. Ord a => a -> a -> Bool < Int n then Int x else Int x Int -> Int -> Int forall a. Num a => a -> a -> a + Int s go Int m Int n (LCLam LCType t LCTerm b) = LCType -> LCTerm -> LCTerm LCLam (Int -> (LCType, Int) -> LCType shiftTypeMin Int m (LCType t, Int r)) (LCTerm -> LCTerm) -> LCTerm -> LCTerm forall a b. (a -> b) -> a -> b $ Int -> Int -> LCTerm -> LCTerm go Int m (Int n Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) LCTerm b go Int m Int n (LCApp LCTerm f LCTerm a) = Int -> Int -> LCTerm -> LCTerm go Int m Int n LCTerm f LCTerm -> LCTerm -> LCTerm `LCApp` Int -> Int -> LCTerm -> LCTerm go Int m Int n LCTerm a go Int m Int n (LCTLam LCTerm b) = LCTerm -> LCTerm LCTLam (LCTerm -> LCTerm) -> LCTerm -> LCTerm forall a b. (a -> b) -> a -> b $ Int -> Int -> LCTerm -> LCTerm go (Int m Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) Int n LCTerm b go Int m Int n (LCTApp LCTerm f LCType t) = Int -> Int -> LCTerm -> LCTerm go Int m Int n LCTerm f LCTerm -> LCType -> LCTerm `LCTApp` Int -> (LCType, Int) -> LCType shiftTypeMin Int m (LCType t, Int r) shiftType :: (LCType, Int) -> LCType shiftType :: (LCType, Int) -> LCType shiftType = Int -> (LCType, Int) -> LCType shiftTypeMin Int 0 shiftTypeMin :: Int -> (LCType, Int) -> LCType shiftTypeMin :: Int -> (LCType, Int) -> LCType shiftTypeMin Int m' (LCType v, Int r) = Int -> LCType -> LCType go Int m' LCType v where go :: Int -> LCType -> LCType go Int _ LCType LCBase = LCType LCBase go Int m (LCTVar Int p) = Int -> LCType LCTVar (Int -> LCType) -> Int -> LCType forall a b. (a -> b) -> a -> b $ if Int p Int -> Int -> Bool forall a. Ord a => a -> a -> Bool < Int m then Int p else Int p Int -> Int -> Int forall a. Num a => a -> a -> a + Int r go Int m (LCArr LCType a LCType b) = Int -> LCType -> LCType go Int m LCType a LCType -> LCType -> LCType `LCArr` Int -> LCType -> LCType go Int m LCType b go Int m (LCUniv LCType a) = LCType -> LCType LCUniv (LCType -> LCType) -> LCType -> LCType forall a b. (a -> b) -> a -> b $ Int -> LCType -> LCType go (Int m Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) LCType a shiftValue :: (LCValue, Int, Int) -> LCTerm shiftValue :: (LCValue, Int, Int) -> LCTerm shiftValue (LCValue v, Int r, Int s) = (LCTerm, Int, Int) -> LCTerm shift (LCValue -> LCTerm liftLCValue LCValue v, Int r, Int s) shiftNormal :: (LCNormalTerm, Int, Int) -> LCNormalTerm shiftNormal :: (LCNormalTerm, Int, Int) -> LCNormalTerm shiftNormal = Int -> Int -> (LCNormalTerm, Int, Int) -> LCNormalTerm shiftNormalMin Int 0 Int 0 shiftNormalMin :: Int -> Int -> (LCNormalTerm, Int, Int) -> LCNormalTerm shiftNormalMin :: Int -> Int -> (LCNormalTerm, Int, Int) -> LCNormalTerm shiftNormalMin Int m' Int n' (LCNormalTerm v, Int r, Int s) = Int -> Int -> LCNormalTerm -> LCNormalTerm go Int m' Int n' LCNormalTerm v where go :: Int -> Int -> LCNormalTerm -> LCNormalTerm go Int m Int n (LCNormLam LCType t LCNormalTerm b) = LCType -> LCNormalTerm -> LCNormalTerm LCNormLam (Int -> (LCType, Int) -> LCType shiftTypeMin Int m (LCType t, Int r)) (LCNormalTerm -> LCNormalTerm) -> LCNormalTerm -> LCNormalTerm forall a b. (a -> b) -> a -> b $ Int -> Int -> LCNormalTerm -> LCNormalTerm go Int m (Int n Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) LCNormalTerm b go Int m Int n (LCNormTLam LCNormalTerm b) = LCNormalTerm -> LCNormalTerm LCNormTLam (LCNormalTerm -> LCNormalTerm) -> LCNormalTerm -> LCNormalTerm forall a b. (a -> b) -> a -> b $ Int -> Int -> LCNormalTerm -> LCNormalTerm go (Int m Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) Int n LCNormalTerm b go Int m Int n (LCNormNeut LCNeutralTerm nt) = LCNeutralTerm -> LCNormalTerm LCNormNeut (LCNeutralTerm -> LCNormalTerm) -> LCNeutralTerm -> LCNormalTerm forall a b. (a -> b) -> a -> b $ Int -> Int -> (LCNeutralTerm, Int, Int) -> LCNeutralTerm shiftNeutralMin Int m Int n (LCNeutralTerm nt, Int r, Int s) shiftNeutralMin :: Int -> Int -> (LCNeutralTerm, Int, Int) -> LCNeutralTerm shiftNeutralMin :: Int -> Int -> (LCNeutralTerm, Int, Int) -> LCNeutralTerm shiftNeutralMin Int m Int n (LCNeutralTerm v, Int r, Int s) = LCNeutralTerm -> LCNeutralTerm go LCNeutralTerm v where go :: LCNeutralTerm -> LCNeutralTerm go (LCNeutVar Int x) = Int -> LCNeutralTerm LCNeutVar (Int -> LCNeutralTerm) -> Int -> LCNeutralTerm forall a b. (a -> b) -> a -> b $ if Int x Int -> Int -> Bool forall a. Ord a => a -> a -> Bool < Int n then Int x else Int x Int -> Int -> Int forall a. Num a => a -> a -> a + Int s go (LCNeutApp LCNeutralTerm f LCNormalTerm a) = LCNeutralTerm -> LCNeutralTerm go LCNeutralTerm f LCNeutralTerm -> LCNormalTerm -> LCNeutralTerm `LCNeutApp` Int -> Int -> (LCNormalTerm, Int, Int) -> LCNormalTerm shiftNormalMin Int m Int n (LCNormalTerm a, Int r, Int s) go (LCNeutTApp LCNeutralTerm f LCType t) = LCNeutralTerm -> LCNeutralTerm go LCNeutralTerm f LCNeutralTerm -> LCType -> LCNeutralTerm `LCNeutTApp` Int -> (LCType, Int) -> LCType shiftTypeMin Int m (LCType t, Int r)