module A201802.LR0 where

open import A201801.Prelude
open import A201801.Category
open import A201801.Fin
open import A201801.FinLemmas
open import A201801.Vec


--------------------------------------------------------------------------------


infixr 8 _βŠƒ_
data Type : Set
  where
    𝔹   : Type
    _∨_ : Type β†’ Type β†’ Type
    𝟘   : Type
    πŸ™   : Type
    _∧_ : Type β†’ Type β†’ Type
    _βŠƒ_ : Type β†’ Type β†’ Type


Types : Nat β†’ Set
Types g = Vec Type g


--------------------------------------------------------------------------------


data Term (g : Nat) : Set
  where
    VAR   : Fin g β†’ Term g
    LAM   : Term (suc g) β†’ Term g
    APP   : Term g β†’ Term g β†’ Term g
    PAIR  : Term g β†’ Term g β†’ Term g
    FST   : Term g β†’ Term g
    SND   : Term g β†’ Term g
    UNIT  : Term g
    ABORT : Term g β†’ Term g
    LEFT  : Term g β†’ Term g
    RIGHT : Term g β†’ Term g
    CASE  : Term g β†’ Term (suc g) β†’ Term (suc g) β†’ Term g
    TRUE  : Term g
    FALSE : Term g
    IF    : Term g β†’ Term g β†’ Term g β†’ Term g


Terms : Nat β†’ Nat β†’ Set
Terms g n = Vec (Term g) n


--------------------------------------------------------------------------------


REN : βˆ€ {g gβ€²} β†’ gβ€² β‰₯ g β†’ Term g
               β†’ Term gβ€²
REN e (VAR I)      = VAR (RENβˆ‹ e I)
REN e (LAM M)      = LAM (REN (keep e) M)
REN e (APP M N)    = APP (REN e M) (REN e N)
REN e (PAIR M N)   = PAIR (REN e M) (REN e N)
REN e (FST M)      = FST (REN e M)
REN e (SND M)      = SND (REN e M)
REN e UNIT         = UNIT
REN e (ABORT M)    = ABORT (REN e M)
REN e (LEFT M)     = LEFT (REN e M)
REN e (RIGHT M)    = RIGHT (REN e M)
REN e (CASE M N O) = CASE (REN e M) (REN (keep e) N) (REN (keep e) O)
REN e TRUE         = TRUE
REN e FALSE        = FALSE
REN e (IF M N O)   = IF (REN e M) (REN e N) (REN e O)


RENS : βˆ€ {g gβ€² n} β†’ gβ€² β‰₯ g β†’ Terms g n
                  β†’ Terms gβ€² n
RENS e Ο„ = MAPS (REN e) Ο„


WK : βˆ€ {g} β†’ Term g
           β†’ Term (suc g)
WK M = REN (drop id) M


WKS : βˆ€ {g n} β†’ Terms g n
              β†’ Terms (suc g) n
WKS Ο„ = RENS (drop id) Ο„


VZ : βˆ€ {g} β†’ Term (suc g)
VZ = VAR zero


LIFTS : βˆ€ {g n} β†’ Terms g n
                β†’ Terms (suc g) (suc n)
LIFTS Ο„ = WKS Ο„ , VZ


VARS : βˆ€ {g gβ€²} β†’ gβ€² β‰₯ g
                β†’ Terms gβ€² g
VARS done     = βˆ™
VARS (drop e) = WKS (VARS e)
VARS (keep e) = LIFTS (VARS e)


IDS : βˆ€ {g} β†’ Terms g g
IDS = VARS id


SUB : βˆ€ {g n} β†’ Terms g n β†’ Term n
              β†’ Term g
SUB Ο„ (VAR I)      = GET Ο„ I
SUB Ο„ (LAM M)      = LAM (SUB (LIFTS Ο„) M)
SUB Ο„ (APP M N)    = APP (SUB Ο„ M) (SUB Ο„ N)
SUB Ο„ (PAIR M N)   = PAIR (SUB Ο„ M) (SUB Ο„ N)
SUB Ο„ (FST M)      = FST (SUB Ο„ M)
SUB Ο„ (SND M)      = SND (SUB Ο„ M)
SUB Ο„ UNIT         = UNIT
SUB Ο„ (ABORT M)    = ABORT (SUB Ο„ M)
SUB Ο„ (LEFT M)     = LEFT (SUB Ο„ M)
SUB Ο„ (RIGHT M)    = RIGHT (SUB Ο„ M)
SUB Ο„ (CASE M N O) = CASE (SUB Ο„ M) (SUB (LIFTS Ο„) N) (SUB (LIFTS Ο„) O)
SUB Ο„ TRUE         = TRUE
SUB Ο„ FALSE        = FALSE
SUB Ο„ (IF M N O)   = IF (SUB Ο„ M) (SUB Ο„ N) (SUB Ο„ O)


SUBS : βˆ€ {g n m} β†’ Terms g n β†’ Terms n m
                 β†’ Terms g m
SUBS Ο„ Ο… = MAPS (SUB Ο„) Ο…


CUT : βˆ€ {g} β†’ Term g β†’ Term (suc g)
            β†’ Term g
CUT M N = SUB (IDS , M) N


--------------------------------------------------------------------------------