{-# 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)