{-# LANGUAGE ViewPatterns #-}
module LambdaCube.SystemFw_.Substitution
  ( substituteTypeInType
  , substituteValue
  , substituteNormalInNormal
  ) where

import           LambdaCube.SystemFw_.Ast
import           LambdaCube.SystemFw_.Lifter

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 -> LCTerm -> LCTerm
substDefValue (LCValue
v, Int
0)

substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm
substituteNormalInNormal :: LCNormalTerm -> Int -> LCNormalTerm -> LCNormalTerm
substituteNormalInNormal LCNormalTerm
v = (LCNormalTerm, Int) -> Int -> LCNormalTerm -> LCNormalTerm
substDefNormalInNormal (LCNormalTerm
v, Int
0)

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 (LCTTLam LCKind
k LCType
b)              = LCKind -> LCType -> LCType
LCTTLam LCKind
k (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
b
    go (LCType, Int)
dv     Int
p (LCTTApp LCType
f LCType
a)              = (LCType, Int) -> Int -> LCType -> LCType
go (LCType, Int)
dv Int
p LCType
f LCType -> LCType -> LCType
`LCTTApp` (LCType, Int) -> Int -> LCType -> LCType
go (LCType, Int)
dv Int
p LCType
a

substDefValue :: (LCValue, Int) -> Int -> LCTerm -> LCTerm
substDefValue :: (LCValue, Int) -> Int -> LCTerm -> LCTerm
substDefValue = (LCValue, Int) -> Int -> LCTerm -> LCTerm
go
  where
    go :: (LCValue, Int) -> Int -> LCTerm -> LCTerm
go (LCValue, Int)
dv     Int
x (LCVar ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x) -> Bool
True))  = (LCValue, Int) -> LCTerm
shiftValue (LCValue, Int)
dv
    go (LCValue, 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
_ (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
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 -> LCTerm -> LCTerm
go (LCValue
v, 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)
dv     Int
x (LCApp LCTerm
f LCTerm
a)               = (LCValue, Int) -> Int -> LCTerm -> LCTerm
go (LCValue, Int)
dv Int
x LCTerm
f LCTerm -> LCTerm -> LCTerm
`LCApp` (LCValue, Int) -> Int -> LCTerm -> LCTerm
go (LCValue, Int)
dv Int
x LCTerm
a

substDefNormalInNormal :: (LCNormalTerm, Int) -> Int -> LCNormalTerm -> LCNormalTerm
substDefNormalInNormal :: (LCNormalTerm, Int) -> Int -> LCNormalTerm -> LCNormalTerm
substDefNormalInNormal = (LCNormalTerm, Int) -> Int -> LCNormalTerm -> LCNormalTerm
go
  where
    go :: (LCNormalTerm, Int) -> Int -> LCNormalTerm -> LCNormalTerm
go (LCNormalTerm
v, 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 -> LCNormalTerm -> LCNormalTerm
go (LCNormalTerm
v, 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, Int)
dv     Int
x (LCNormNeut LCNeutralTerm
nt) = (LCNormalTerm, Int) -> Int -> LCNeutralTerm -> LCNormalTerm
substDefNormalInNeutral (LCNormalTerm, Int)
dv Int
x LCNeutralTerm
nt

substDefNormalInNeutral :: (LCNormalTerm, Int) -> Int -> LCNeutralTerm -> LCNormalTerm
substDefNormalInNeutral :: (LCNormalTerm, Int) -> Int -> LCNeutralTerm -> LCNormalTerm
substDefNormalInNeutral (LCNormalTerm, 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) -> LCNormalTerm
shiftNormal (LCNormalTerm, 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
        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 -> LCNormalTerm -> LCNormalTerm
substDefNormalInNormal (LCNormalTerm, Int)
dv Int
x LCNormalTerm
a

shift :: (LCTerm, Int) -> LCTerm
shift :: (LCTerm, Int) -> LCTerm
shift (LCTerm
v, Int
s) = Int -> LCTerm -> LCTerm
go Int
0 LCTerm
v
  where
    go :: Int -> LCTerm -> LCTerm
go 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
n (LCLam LCType
t LCTerm
b) = LCType -> LCTerm -> LCTerm
LCLam LCType
t (LCTerm -> LCTerm) -> LCTerm -> LCTerm
forall a b. (a -> b) -> a -> b
$ Int -> LCTerm -> LCTerm
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) LCTerm
b
    go Int
n (LCApp LCTerm
f LCTerm
a) = Int -> LCTerm -> LCTerm
go Int
n LCTerm
f LCTerm -> LCTerm -> LCTerm
`LCApp` Int -> LCTerm -> LCTerm
go Int
n LCTerm
a

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 (LCTTLam LCKind
k LCType
b) = LCKind -> LCType -> LCType
LCTTLam LCKind
k (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
b
    go Int
m (LCTTApp LCType
f LCType
a) = Int -> LCType -> LCType
go Int
m LCType
f LCType -> LCType -> LCType
`LCTTApp` Int -> LCType -> LCType
go Int
m LCType
a

shiftValue :: (LCValue, Int) -> LCTerm
shiftValue :: (LCValue, Int) -> LCTerm
shiftValue (LCValue
v, Int
s) = (LCTerm, Int) -> LCTerm
shift (LCValue -> LCTerm
liftLCValue LCValue
v, Int
s)

shiftNormal :: (LCNormalTerm, Int) -> LCNormalTerm
shiftNormal :: (LCNormalTerm, Int) -> LCNormalTerm
shiftNormal = Int -> (LCNormalTerm, Int) -> LCNormalTerm
shiftNormalMin Int
0

shiftNormalMin :: Int -> (LCNormalTerm, Int) -> LCNormalTerm
shiftNormalMin :: Int -> (LCNormalTerm, Int) -> LCNormalTerm
shiftNormalMin Int
n' (LCNormalTerm
v, Int
s) = Int -> LCNormalTerm -> LCNormalTerm
go Int
n' LCNormalTerm
v
  where
    go :: Int -> LCNormalTerm -> LCNormalTerm
go Int
n (LCNormLam LCType
t LCNormalTerm
b) = LCType -> LCNormalTerm -> LCNormalTerm
LCNormLam LCType
t (LCNormalTerm -> LCNormalTerm) -> LCNormalTerm -> LCNormalTerm
forall a b. (a -> b) -> a -> b
$ Int -> LCNormalTerm -> LCNormalTerm
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) LCNormalTerm
b
    go Int
n (LCNormNeut LCNeutralTerm
nt) = LCNeutralTerm -> LCNormalTerm
LCNormNeut (LCNeutralTerm -> LCNormalTerm) -> LCNeutralTerm -> LCNormalTerm
forall a b. (a -> b) -> a -> b
$ Int -> (LCNeutralTerm, Int) -> LCNeutralTerm
shiftNeutralMin Int
n (LCNeutralTerm
nt, Int
s)

shiftNeutralMin :: Int -> (LCNeutralTerm, Int) -> LCNeutralTerm
shiftNeutralMin :: Int -> (LCNeutralTerm, Int) -> LCNeutralTerm
shiftNeutralMin Int
n (LCNeutralTerm
v, 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 -> (LCNormalTerm, Int) -> LCNormalTerm
shiftNormalMin Int
n (LCNormalTerm
a, Int
s)