module linear.Scope where

open import Data.Nat
open import Data.Fin hiding (_+_)
open import Function

data Mergey : (k l : )  Set where
  finish : {k : }  Mergey k k
  copy   : {k l : }  Mergey k l  Mergey (suc k) (suc l)
  insert : {k l : }  Mergey k l  Mergey k (suc l)

Weakening : (T :   Set)  Set
Weakening T = {k l : } (m : Mergey k l)  T k  T l

Extending : (T :     Set)  Set
Extending T = {k l : } (o : )  T k l  T (o + k) (o + l)

copys : Extending Mergey
copys zero    m = m
copys (suc o) m = copy (copys o m)

inserts : {k l : } (o : )  Mergey k l  Mergey k (o + l)
inserts zero    m = m
inserts (suc o) m = insert (inserts o m)

weakFin : Weakening Fin
weakFin finish     k       = k
weakFin (copy m)   zero    = zero
weakFin (copy m)   (suc k) = suc (weakFin m k)
weakFin (insert m) k       = suc (weakFin m k)

data Env (T :   Set) : (k l : )  Set where
  []  : {l : }  Env T 0 l
  v∷_ : {k l : }  Env T k l  Env T (suc k) (suc l)
  _∷_ : {k l : } (t : T l) (ρ : Env T k l)  Env T (suc k) l

Substituting : (E T :   Set)  Set
Substituting E T = {k l : } (ρ : Env E k l)  T k  T l

record Freshey (T :   Set) : Set where
  field
    fresh : {k : }  T (suc k)
    weak  : Weakening T

substFin : {k l : } {T :   Set} (F : Freshey T) (ρ : Env T k l)  Fin k  T l
substFin F (v∷ ρ)  zero    = Freshey.fresh F
substFin F (t  ρ) zero    = t
substFin F (v∷ ρ)  (suc v) = Freshey.weak F (insert finish) $ substFin F ρ v
substFin F (t  ρ) (suc v) = substFin F ρ v

withFreshVars : {T :   Set}  Extending (Env T)
withFreshVars zero    ρ = ρ
withFreshVars (suc o) ρ = v∷ withFreshVars o ρ