-- Type system for shift0/reset0

module DS where

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Bool using (Bool; true; false)
open import Data.String using (String)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥)
open import Data.Product using (_×_; _,_)
open import Relation.Binary.PropositionalEquality

-- Types
mutual

  -- Term types
  data Ty : Set where
    Nat   : Ty
    Bol   : Ty
    _⇒_⟨_⟩_⟨_⟩_ : Ty → Ty → Mc → Ty → Mc → Ty → Ty

  -- Metacontinuation types
  data Mc : Set where
    •        : Mc
    _⇨⟨_⟩_∷_ : Ty → Mc → Ty → Mc → Mc

-- Cont types
data CTy : Set where
  _▷⟨_⟩_ : Ty → Mc → Ty → CTy

-- Identity continuation check
id-cont-type : Ty → Mc → Ty → Set
id-cont-type τ • τ' = τ ≡ τ'
id-cont-type τ (τ₁ ⇨⟨ σ₁ ⟩ τ₁' ∷ σ₂) τ'
  = (τ ≡ τ₁) × (τ' ≡ τ₁') × (σ₁ ≡ σ₂)

-- Terms
mutual
  data value[_]_ (var : Ty → Set) : Ty → Set where
    -- x
    Var    : {τ₁ : Ty} → (x : var τ₁) → value[ var ] τ₁
    -- n
    Num    : (n : ℕ) → value[ var ] Nat
    -- n
    Bol    : (b : Bool) → value[ var ] Bol
    -- λx.M
    Fun    : {τ₁ τ₂ α β : Ty} {σα σβ : Mc} →
             (f : var τ₂ → term[ var , τ₁ ▷⟨ σα ⟩ α ]⟨ σβ ⟩ β) →
             value[ var ] (τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)
    -- S
    Shift  : {τ τ₁ τ₂ α β γ γ' : Ty} {σ₁ σ₂ σid σβ : Mc} →
             (id : id-cont-type γ σid γ') →
             value[ var ] (((τ ⇒ τ₁ ⟨ σ₁ ⟩ τ₂ ⟨ σ₂ ⟩ α)
                            ⇒ γ ⟨ σid ⟩ γ' ⟨ σβ ⟩ β)
                           ⇒ τ ⟨ τ₁ ⇨⟨ σ₁ ⟩ τ₂ ∷ σ₂ ⟩ α ⟨ σβ ⟩ β)
    -- S0
    Shift0 : {τ τ₀ τ₀' τ₁ τ₂ α β : Ty} {σ₀ σ₀' σ₁ σ₂ : Mc} →
            value[ var ] (((τ ⇒ τ₁ ⟨ σ₁ ⟩ τ₂ ⟨ σ₂ ⟩ α)
                           ⇒ τ₀ ⟨ σ₀ ⟩ τ₀' ⟨ σ₀' ⟩ β)
                          ⇒ τ ⟨ τ₁ ⇨⟨ σ₁ ⟩ τ₂ ∷ σ₂ ⟩ α
                               ⟨ τ₀  ⇨⟨ σ₀ ⟩ τ₀' ∷ σ₀' ⟩ β)

  data term[_,_]⟨_⟩_ (var : Ty → Set) : CTy → Mc → Ty → Set where
    Val    : {τ₁ α : Ty} {σα : Mc} →
             (v : value[ var ] τ₁) →
             term[ var , τ₁ ▷⟨ σα ⟩ α ]⟨ σα ⟩ α
    NonVal : {β : Ty} {Δ : CTy} {σβ : Mc} →
             (p : nonvalue[ var , Δ ]⟨ σβ ⟩ β) →
             term[ var , Δ ]⟨ σβ ⟩ β

  data nonvalue[_,_]⟨_⟩_ (var : Ty → Set) : CTy → Mc → Ty → Set where
    -- M N
    App   : {τ₁ τ₂ α β γ δ : Ty} {σα σβ σγ σδ : Mc} →
            (e₁ : term[ var ,
                  (τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β) ▷⟨ σγ ⟩ γ ]⟨ σδ ⟩ δ) →
            (e₂ : term[ var , τ₂ ▷⟨ σβ ⟩ β ]⟨ σγ ⟩ γ) →
            nonvalue[ var , τ₁ ▷⟨ σα ⟩ α ]⟨ σδ ⟩ δ
    -- <M>
    Reset : {τ α β γ γ' : Ty} {σα σβ σid : Mc} →
            (id : id-cont-type γ σid γ') →
            (e : term[ var , γ ▷⟨ σid ⟩ γ' ]⟨ τ ⇨⟨ σα ⟩ α ∷ σβ ⟩ β) →
            nonvalue[ var , τ ▷⟨ σα ⟩ α ]⟨ σβ ⟩ β
    -- let x = M in N
    Let   : {τ₂ β γ : Ty} {τ₁▷⟨σα⟩α : CTy} {σβ σγ : Mc} →
            (e₁ : term[ var , τ₂ ▷⟨ σβ ⟩ β ]⟨ σγ ⟩ γ) →            -- M
            (e₂ : var τ₂ → term[ var , τ₁▷⟨σα⟩α ]⟨ σβ ⟩ β) →  -- λx. N
            nonvalue[ var , τ₁▷⟨σα⟩α ]⟨ σγ ⟩ γ

-- examples
-- λx.x
val1 : {var : Ty → Set} → {τ₁ τ₂ : Ty} → {σ₂ : Mc} →
       value[ var ] (τ₁ ⇒ τ₁ ⟨ σ₂ ⟩ τ₂ ⟨ σ₂ ⟩ τ₂)
val1 = Fun (λ x → Val (Var x))

-- λx.S(λk.k x)
val2 : {var : Ty → Set} → {τ₁ τ₂ γ γ' : Ty} → {σid σ₂ : Mc} →
       (id : id-cont-type γ σid γ') →
       value[ var ] (τ₁ ⇒ τ₁ ⟨ γ ⇨⟨ σid ⟩ γ' ∷ σ₂ ⟩ τ₂ ⟨ σ₂ ⟩ τ₂)
val2 id = Fun (λ x → NonVal (App (Val (Shift id))
           (Val (Fun (λ k → NonVal (App (Val (Var k)) (Val (Var x))))))))

-- λx.S(λk.x)
val3 : {var : Ty → Set} → {τ₁ τ₂ τ₃ τ₄ τ₅ τ₆ : Ty} → {σ₁ σ₂ σ₃ : Mc} →
       (id : id-cont-type τ₁ σ₃ τ₆) →
       value[ var ] (τ₁ ⇒ τ₂ ⟨ τ₃ ⇨⟨ σ₁ ⟩ τ₄ ∷ σ₂ ⟩ τ₅ ⟨ σ₃ ⟩ τ₆)
val3 id = Fun (λ x → NonVal (App (Val (Shift id))
                                  (Val (Fun (λ k → Val (Var x))))))

-- λx.S0(λk.x)
val3' : {var : Ty → Set} → {τ₁ τ₂ τ₃ τ₄ τ₅ τ₆ : Ty} → {σ₁ σ₂ σ₃ : Mc} →
        value[ var ]
          (τ₁ ⇒ τ₂ ⟨ τ₃ ⇨⟨ σ₁ ⟩ τ₄ ∷ σ₂ ⟩ τ₅ ⟨ τ₁ ⇨⟨ σ₃ ⟩ τ₆ ∷ σ₃ ⟩ τ₆)
val3' = Fun (λ x → NonVal (App (Val Shift0)
                                (Val (Fun (λ k → Val (Var x))))))

-- Interpretation of types
mutual
  〚_〛τ : Ty → Set
  〚 Nat 〛τ = ℕ
  〚 Bol 〛τ = Bool
  〚 τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β 〛τ =
    〚 τ₂ 〛τ → (〚 τ₁ 〛τ → 〚 σα 〛σ → 〚 α 〛τ) → 〚 σβ 〛σ → 〚 β 〛τ

  〚_〛σ : Mc → Set
  〚 • 〛σ = ⊤
  〚 τ ⇨⟨ σ ⟩ τ' ∷ σ' 〛σ =
    (〚 τ 〛τ → 〚 σ 〛σ → 〚 τ' 〛τ) × 〚 σ' 〛σ

-- Initial continuation
idk : {τ τ' : Ty} → {σ : Mc} → id-cont-type τ σ τ' →
      〚 τ 〛τ → 〚 σ 〛σ → 〚 τ' 〛τ
idk {σ = •} refl v tt = v
idk {σ = τ ⇨⟨ σ ⟩ τ' ∷ .σ} (refl , refl , refl) v (k₀ , m₀) = k₀ v m₀

-- Interpreter
mutual
  gv : {τ α : Ty} {σα : Mc} →
       (v : value[ 〚_〛τ ] τ) →
       (k : 〚 τ 〛τ → 〚 σα 〛σ → 〚 α 〛τ) (m : 〚 σα 〛σ) → 〚 α 〛τ
  gv (Var x) k m = k x m
  gv (Num n) k m = k n m
  gv (Bol b) k m = k b m
  gv (Fun f) k m = k (λ x t₁ m₁ → g (f x) t₁ m₁) m
  gv (Shift id) k m =
    k (λ x k₁ m₁ → x (λ v k₂ m₂ → k₁ v (k₂ , m₂)) (idk id) m₁) m
  gv Shift0 k m =
    k (λ { x k₁ (k₀ , m₀) → x (λ v k₂ m₂ → k₁ v (k₂ , m₂)) k₀ m₀ }) m

  g : {τ α β : Ty} {σα σβ : Mc} →
      (e : term[ 〚_〛τ , τ ▷⟨ σα ⟩ α ]⟨ σβ ⟩ β) →
      (k : 〚 τ 〛τ → 〚 σα 〛σ → 〚 α 〛τ) → (m : 〚 σβ 〛σ) → 〚 β 〛τ
  g (Val v) k m = gv v k m
  g (NonVal p) k m = gp p k m

  gp : {τ α β : Ty} {σα σβ : Mc} →
       (p : nonvalue[ 〚_〛τ , τ ▷⟨ σα ⟩ α ]⟨ σβ ⟩ β) →
       (k : 〚 τ 〛τ → 〚 σα 〛σ → 〚 α 〛τ) → (m : 〚 σβ 〛σ) → 〚 β 〛τ
  gp (App e₁ e₂) k m = g e₁ (λ v₁ m₁ → g e₂ (λ v₂ m₂ → v₁ v₂ k m₂) m₁) m
  gp (Reset id e) k m = g e (idk id) (k , m)
  gp (Let e₁ e₂) k m = g e₁ (λ v₁ m₁ → g (e₂ v₁) k m₁) m

-- Evaluation context (inside-out)
data pcontext[_,_,_]⟨_⟩_ (var : Ty → Set): CTy → Ty → Mc → Ty → Set where
  -- []
  Hole : {τ α : Ty} {σ : Mc} →
         pcontext[ var , τ ▷⟨ σ ⟩ α , τ ]⟨ σ ⟩ α
  -- K[[]@M]
  App₁ : {τ₁ τ₂ τ₃ τ₄ τ₅ : Ty} {Δ : CTy} {σ₃ σ₄ σ₅ : Mc} →
         (k : pcontext[ var , Δ , τ₁ ]⟨ σ₃ ⟩ τ₃) →
         (e : term[ var , τ₂ ▷⟨ σ₄ ⟩ τ₄ ]⟨ σ₅ ⟩ τ₅) →
         pcontext[ var , Δ , τ₂ ⇒ τ₁ ⟨ σ₃ ⟩ τ₃ ⟨ σ₄ ⟩ τ₄ ]⟨ σ₅ ⟩ τ₅
  -- K[V@[]]
  App₂  : {τ₁ τ₂ τ₃ τ₄ : Ty} {Δ : CTy} {σ₃ σ₄ : Mc} →
          (v : value[ var ] (τ₂ ⇒ τ₁ ⟨ σ₃ ⟩ τ₃ ⟨ σ₄ ⟩ τ₄)) →
          (k : pcontext[ var , Δ , τ₁ ]⟨ σ₃ ⟩ τ₃) →
          pcontext[ var , Δ , τ₂ ]⟨ σ₄ ⟩ τ₄
  -- K[Let x = [] in M]
  Let   : {τ₁ τ₂ τ₃ τ₄ : Ty} {Δ : CTy} {σ₃ σ₄ : Mc} →
          (k : pcontext[ var , Δ , τ₁ ]⟨ σ₃ ⟩ τ₃) →                -- K
          (f : var τ₂ → term[ var , τ₁ ▷⟨ σ₃ ⟩ τ₃ ]⟨ σ₄ ⟩ τ₄) →   -- λx. M
          pcontext[ var , Δ , τ₂ ]⟨ σ₄ ⟩ τ₄

-- Plug
plug : {var : Ty → Set} → {τ₁ τ₂ τ₃ : Ty} {τ₄▷⟨σ⟩τ₅ : CTy} {σ₁ σ₂ : Mc} →
       (k : pcontext[ var , τ₄▷⟨σ⟩τ₅ , τ₁ ]⟨ σ₁ ⟩ τ₂) →
       (e : term[ var , τ₁ ▷⟨ σ₁ ⟩ τ₂ ]⟨ σ₂ ⟩ τ₃) →
       term[ var , τ₄▷⟨σ⟩τ₅ ]⟨ σ₂ ⟩ τ₃
plug Hole e = e
plug (App₁ k e₂) e = plug k (NonVal (App e e₂))
plug (App₂ v₁ k) e = plug k (NonVal (App (Val v₁) e))
plug (Let k e₂) e = plug k (NonVal (Let e e₂))

-- Substitution relation M[x:=V]
mutual
  data SubstV {var : Ty → Set} : {τ₁ τ₂ : Ty} →
              (var τ₁ → value[ var ] τ₂) →
              value[ var ] τ₁ →
              value[ var ] τ₂ → Set where
    -- (λx.x)[v] → v
    sVar=  : {τ₁ : Ty} {v : value[ var ] τ₁} →
             SubstV (λ x → Var x) v v
    -- (λ_.x)[v] → x
    sVar≠  : {τ₁ τ₂ : Ty} {v : value[ var ] τ₂} {x : var τ₁} →
             SubstV (λ _ → Var x) v (Var x)
    -- (λ_.n)[v] → n
    sNum   : {τ₁ : Ty} {v : value[ var ] τ₁} {n : ℕ} →
             SubstV (λ _ → Num n) v (Num n)
    -- (λ_.b)[v] → b
    sBol   : {τ₁ : Ty} {v : value[ var ] τ₁} {b : Bool} →
             SubstV (λ _ → Bol b) v (Bol b)
    -- (λy.λx.ey)[v] → λx.e′
    sFun   : {τ τ₁ τ₂ τ₃ τ₄ : Ty} {σ₃ σ₄ : Mc} →
             {e₁ : var τ₁ → var τ → term[ var , τ₂ ▷⟨ σ₃ ⟩ τ₃ ]⟨ σ₄ ⟩ τ₄} →
             {v : value[ var ] τ₁} →
             {e₁′ : var τ → term[ var , τ₂ ▷⟨ σ₃ ⟩ τ₃ ]⟨ σ₄ ⟩ τ₄} →
             ((x : var τ) → Subst (λ y → (e₁ y) x) v (e₁′ x)) →
             SubstV (λ y → Fun (e₁ y)) v (Fun e₁′)
    -- (λ_.S)[v] → S
    sShift : {τ τ' τ₁ τ₂ α β γ γ' : Ty} {σ₁ σ₂ σid σβ : Mc}
             {v : value[ var ] τ'} →
             (id : id-cont-type γ σid γ') →
             SubstV (λ _ → Shift {τ = τ} {τ₁} {τ₂} {α} {β} {γ} {γ'}
                                  {σ₁} {σ₂} {σid} {σβ} id)
                    v (Shift id)
    -- (λ_.S0)[v] → S0
    sShift0 : {τ τ' τ₀ τ₀' τ₁ τ₂ α β : Ty} {σ₀ σ₀' σ₁ σ₂ : Mc} →
              {v : value[ var ] τ'} →
              SubstV (λ _ → Shift0 {τ = τ} {τ₀} {τ₀'} {τ₁} {τ₂} {α} {β}
                                   {σ₀} {σ₀'} {σ₁} {σ₂})
                     v Shift0

  data Subst {var : Ty → Set} : {τ₁ τ₂ : Ty} {Δ : CTy} {σ₂ : Mc} →
             (var τ₁ → term[ var , Δ ]⟨ σ₂ ⟩ τ₂) →
             value[ var ] τ₁ →
             term[ var , Δ ]⟨ σ₂ ⟩ τ₂ → Set where
    sVal   : {τ τ₁ τ₂ : Ty} {σ₂ : Mc} →
             {v₁ : var τ → value[ var ] τ₁} →
             {v : value[ var ] τ} →
             {v₁′ : value[ var ] τ₁} →
             SubstV v₁ v v₁′ →
             Subst {τ₂ = τ₂} {σ₂ = σ₂} (λ y → Val (v₁ y)) v (Val v₁′)
    sNonVal : {τ τ₄ : Ty} {τ₁▷⟨σ₃⟩τ₃ : CTy} {σ₄ : Mc} →
             {e : var τ → nonvalue[ var , τ₁▷⟨σ₃⟩τ₃ ]⟨ σ₄ ⟩ τ₄} →
             {v : value[ var ] τ} →
             {e′ : nonvalue[ var , τ₁▷⟨σ₃⟩τ₃ ]⟨ σ₄ ⟩ τ₄} →
             SubstNV e v e′ →
             Subst (λ y → NonVal (e y)) v (NonVal e′)

  data SubstNV {var : Ty → Set} : {τ₁ τ₄ : Ty} {τ₂▷⟨σ₃⟩τ₃ : CTy} {σ₄ : Mc} →
             (var τ₁ → nonvalue[ var , τ₂▷⟨σ₃⟩τ₃ ]⟨ σ₄ ⟩ τ₄) →
             value[ var ] τ₁ →
             nonvalue[ var , τ₂▷⟨σ₃⟩τ₃ ]⟨ σ₄ ⟩ τ₄ → Set where
    sApp   : {τ τ₁ τ₂ τ₃ τ₄ τ₅ τ₆ : Ty} {σ₃ σ₄ σ₅ σ₆ : Mc} →
             {e₁ : var τ → term[ var ,
                   (τ₂ ⇒ τ₁ ⟨ σ₃ ⟩ τ₃ ⟨ σ₄ ⟩ τ₄) ▷⟨ σ₅ ⟩ τ₅ ]⟨ σ₆ ⟩ τ₆}
             {e₂ : var τ → term[ var , τ₂ ▷⟨ σ₄ ⟩ τ₄ ]⟨ σ₅ ⟩ τ₅}
             {v : value[ var ] τ}
             {e₁′ : term[ var ,
                   (τ₂ ⇒ τ₁ ⟨ σ₃ ⟩ τ₃ ⟨ σ₄ ⟩ τ₄) ▷⟨ σ₅ ⟩ τ₅ ]⟨ σ₆ ⟩ τ₆}
             {e₂′ : term[ var , τ₂ ▷⟨ σ₄ ⟩ τ₄ ]⟨ σ₅ ⟩ τ₅} →
             Subst e₁ v e₁′ → Subst e₂ v e₂′ →
             SubstNV (λ y → App (e₁ y) (e₂ y)) v (App e₁′ e₂′)
    sReset : {τ τ' α β γ γ' : Ty} {σα σβ σid : Mc} →
             {id : id-cont-type γ σid γ'} →
             {e₁ : var τ →
                   term[ var , γ ▷⟨ σid ⟩ γ' ]⟨ τ' ⇨⟨ σα ⟩ α ∷ σβ ⟩ β} →
             {v : value[ var ] τ} →
             {e₁′ : term[ var , γ ▷⟨ σid ⟩ γ' ]⟨ τ' ⇨⟨ σα ⟩ α ∷ σβ ⟩ β} →
             Subst e₁ v e₁′ →
             SubstNV (λ y → Reset id (e₁ y))
                     v
                     (Reset id e₁′)
    sLet   : {τ τ₁ β γ : Ty} {τ₂▷⟨σα⟩α : CTy} {σβ σγ : Mc} →
             {e₁ : var τ → term[ var , τ₁ ▷⟨ σβ ⟩ β ]⟨ σγ ⟩ γ} →
             {e₂ : var τ → (var τ₁ → term[ var , τ₂▷⟨σα⟩α ]⟨ σβ ⟩ β)} →
             {v : value[ var ] τ} →
             {e₁′ : term[ var , τ₁ ▷⟨ σβ ⟩ β ]⟨ σγ ⟩ γ} →
             {e₂′ : var τ₁ → term[ var , τ₂▷⟨σα⟩α ]⟨ σβ ⟩ β} →
             ((x : var τ₁) → Subst (λ y → (e₂ y) x) v (e₂′ x)) →
             Subst e₁ v e₁′ →
             SubstNV (λ y → Let (e₁ y) (e₂ y)) v (Let e₁′ e₂′)

--lemma
mutual
  SubstV≠ : {var : Ty → Set} {τ₁ τ : Ty} →
            (v₁ : value[ var ] τ₁) →
            {v : value[ var ] τ} →
            SubstV (λ _ → v₁) v v₁
  SubstV≠ (Var x) = sVar≠
  SubstV≠ (Num n) = sNum
  SubstV≠ (Bol b) = sBol
  SubstV≠ (Fun f) = sFun (λ x → Subst≠ (f x))
  SubstV≠ (Shift id) = sShift id
  SubstV≠ Shift0 = sShift0

  Subst≠ : {var : Ty → Set} {τ β : Ty} {τ▷⟨σα⟩α : CTy} {σβ : Mc}  →
           (e : term[ var , τ▷⟨σα⟩α ]⟨ σβ ⟩ β) →
           {v : value[ var ] τ} →
           Subst (λ _ → e) v e
  Subst≠ (Val v) = sVal (SubstV≠ v)
  Subst≠ (NonVal p) = sNonVal (SubstNV≠ p)

  SubstNV≠ : {var : Ty → Set} {τ β : Ty} {τ▷⟨σα⟩α : CTy} {σβ : Mc}  →
             (e : nonvalue[ var , τ▷⟨σα⟩α ]⟨ σβ ⟩ β) →
             {v : value[ var ] τ} →
             SubstNV (λ _ → e) v e
  SubstNV≠ (App (Val v) (Val w)) = sApp (sVal (SubstV≠ v)) (sVal (SubstV≠ w))
  SubstNV≠ (App (Val v) (NonVal q)) = sApp (sVal (SubstV≠ v)) (sNonVal (SubstNV≠ q))
  SubstNV≠ (App (NonVal p) (Val w)) = sApp (sNonVal (SubstNV≠ p)) (sVal (SubstV≠ w))
  SubstNV≠ (App (NonVal p) (NonVal q)) = sApp (sNonVal (SubstNV≠ p)) (sNonVal (SubstNV≠ q))
  SubstNV≠ (Reset id e) = sReset (Subst≠ e)
  SubstNV≠ (Let e₁ e₂) = sLet (λ x → Subst≠ (e₂ x)) (Subst≠ e₁)

-- reduction rules
data Reduce {var : Ty → Set} : {β : Ty} {τ▷⟨σ⟩α : CTy} {σβ : Mc} →
            term[ var , τ▷⟨σ⟩α ]⟨ σβ ⟩ β →
            term[ var , τ▷⟨σ⟩α ]⟨ σβ ⟩ β → Set where
  -- (λx.M)V -> M[x:=V]
  RBetaV : {τ τ₁ τ₂ τ₃ : Ty} {σ₂ σ₃ : Mc} →
           (e₁ : var τ → term[ var , τ₁ ▷⟨ σ₂ ⟩ τ₂ ]⟨ σ₃ ⟩ τ₃) →
           (v₂ : value[ var ] τ) →
           (e₁′ : term[ var , τ₁ ▷⟨ σ₂ ⟩ τ₂ ]⟨ σ₃ ⟩ τ₃) →
           (sub : Subst e₁ v₂ e₁′) →
           Reduce (NonVal (App (Val (Fun e₁)) (Val v₂)))
                  e₁′
  -- λx.V@x -> V
  REtaV  : {τ₁ τ₂ τ₃ τ₄ β : Ty} {σ₃ σ₄ σβ : Mc} →
           (v : value[ var ] (τ₂ ⇒ τ₁ ⟨ σ₃ ⟩ τ₃ ⟨ σ₄ ⟩ τ₄)) →
           Reduce {β = β} {σβ = σβ}
                  (Val (Fun (λ x → NonVal (App (Val v) (Val (Var x))))))
                  (Val v)
  -- let x = V in M -> M[x:=V]
  RBetaLet : {τ₁ τ₄ : Ty} {τ₂▷⟨σ₃⟩τ₃ : CTy} {σ₄ : Mc} →
           (v₁ : value[ var ] τ₁) →
           (e₂ : var τ₁ → term[ var , τ₂▷⟨σ₃⟩τ₃ ]⟨ σ₄ ⟩ τ₄) →
           (e₂′ : term[ var , τ₂▷⟨σ₃⟩τ₃ ]⟨ σ₄ ⟩ τ₄) →
           (sub : Subst e₂ v₁ e₂′) →
           Reduce (NonVal (Let (Val v₁) e₂))
                  e₂′
  -- let x = M in x -> M
  REtaLet : {τ₁ τ₂ τ₃ : Ty} {σ₂ σ₃ : Mc} →
           (e₁ : term[ var , τ₁ ▷⟨ σ₂ ⟩ τ₂ ]⟨ σ₃ ⟩ τ₃) →
           Reduce (NonVal (Let e₁ (λ x → Val (Var x))))
                  e₁

  -- let y = (let x = L in M) in N -> let x = L in let y = M in N
  RAssoc : {τ₁ τ₂ τ₃ τ₄ τ₅ : Ty} {τ₇▷⟨σ₈⟩τ₈ : CTy} {σ₂ σ₃ σ₅ : Mc} →
           (e₁ : term[ var , τ₁ ▷⟨ σ₂ ⟩ τ₂ ]⟨ σ₃ ⟩ τ₃) →
           (e₂ : var τ₁ → term[ var , τ₄ ▷⟨ σ₅ ⟩ τ₅ ]⟨ σ₂ ⟩ τ₂) →
           (e₃ : var τ₄ → term[ var , τ₇▷⟨σ₈⟩τ₈ ]⟨ σ₅ ⟩ τ₅) →
           Reduce (NonVal (Let (NonVal (Let e₁ (λ x → e₂ x))) (λ y → e₃ y)))
                  (NonVal (Let e₁ (λ x → NonVal (Let (e₂ x) (λ y → e₃ y)))))
  -- P@N -> let x = P in x@N
  RLet1  : {τ₁ τ₂ τ₃ τ₄ τ₅ τ₆ : Ty} {σ₃ σ₄ σ₅ σ₆ : Mc} →
           (e₁ : nonvalue[ var ,
                 (τ₂ ⇒ τ₁ ⟨ σ₃ ⟩ τ₃ ⟨ σ₄ ⟩ τ₄) ▷⟨ σ₅ ⟩ τ₅ ]⟨ σ₆ ⟩ τ₆) →
           (e₂ : term[ var , τ₂ ▷⟨ σ₄ ⟩ τ₄ ]⟨ σ₅ ⟩ τ₅) →
           Reduce (NonVal (App (NonVal e₁) e₂))
                  (NonVal (Let (NonVal e₁) (λ x →
                            NonVal (App (Val (Var x)) e₂))))
  -- V@Q -> let y = Q in V@y
  RLet2  : {τ₁ τ₂ τ₃ τ₄ τ₅ : Ty} {σ₃ σ₄ σ₅ : Mc} →
           {v₁ : value[ var ] (τ₂ ⇒ τ₁ ⟨ σ₃ ⟩ τ₃ ⟨ σ₄ ⟩ τ₄)} →
           (e₂ : nonvalue[ var , τ₂ ▷⟨ σ₄ ⟩ τ₄ ]⟨ σ₅ ⟩ τ₅) →
           Reduce (NonVal (App (Val v₁) (NonVal e₂)))
                  (NonVal (Let (NonVal e₂) (λ y →
                            NonVal (App (Val v₁) (Val (Var y))))))
  -- <J[S@V]> -> <V@(λy.<J[y]>)>
  RShift : {τ τ₁ τ₂ τ₄ τ₅ α β γ γ' τ' α' : Ty}
           {σ₁ σ₂ σ₅ σid σα' σβ' : Mc} →
           (id₁ : id-cont-type γ σid γ') →
           (id₂ : id-cont-type τ₄ σ₅ τ₅) →
           (v : value[ var ]
                ((τ ⇒ τ₁ ⟨ σ₁ ⟩ τ₂ ⟨ σ₂ ⟩ α) ⇒
                 γ ⟨ σid ⟩ γ' ⟨ τ' ⇨⟨ σα' ⟩ α' ∷ σβ' ⟩ β)) →
           (j : pcontext[ var ,
                  τ₄ ▷⟨ σ₅ ⟩ τ₅ , τ ]⟨ τ₁ ⇨⟨ σ₁ ⟩ τ₂ ∷ σ₂ ⟩ α) →
           Reduce (NonVal (Reset id₂ (plug j (NonVal (App (Val (Shift id₁))
                                                          (Val v))))))
                  (NonVal (Reset id₁ (NonVal (App (Val v)
                    (Val (Fun (λ y →
                      NonVal (Reset id₂ (plug j (Val (Var y)))))))))))
  -- <J[S0@V]> -> V@(λy.<J[y]>)
  RShift0 : {τ τ₁ τ₂ τ₄ τ₅ α β τ₀ τ₀' : Ty} {σ₁ σ₂ σ₅ σ₀ σ₀' : Mc} →
           (id : id-cont-type τ₄ σ₅ τ₅) →
           (v : value[ var ]
                ((τ ⇒ τ₁ ⟨ σ₁ ⟩ τ₂ ⟨ σ₂ ⟩ α) ⇒ τ₀ ⟨ σ₀ ⟩ τ₀' ⟨ σ₀' ⟩ β)
               ) →
           (j : pcontext[ var ,
                  τ₄ ▷⟨ σ₅ ⟩ τ₅ , τ ]⟨ τ₁ ⇨⟨ σ₁ ⟩ τ₂ ∷ σ₂ ⟩ α) →
           Reduce (NonVal (Reset id (plug j (NonVal (App (Val Shift0)
                                                         (Val v))))))
                  (NonVal (App (Val v)
                    (Val (Fun (λ y →
                      NonVal (Reset id (plug j (Val (Var y)))))))))
  -- <V> -> V
  RReset : {τ₁ β : Ty} {σβ : Mc} →
           (v₁ : value[ var ] τ₁) →
           Reduce {β = β} {σβ = σβ}
                  (NonVal (Reset (refl , refl , refl) (Val v₁)))
                  (Val v₁)

  -- congruence rules
  RFun   : {τ₁ τ₂ τ₃ τ₄ β : Ty} {σ₃ σ₄ σβ : Mc} →
           {e e′ : var τ₂ → term[ var , τ₁ ▷⟨ σ₃ ⟩ τ₃ ]⟨ σ₄ ⟩ τ₄} →
           ((x : var τ₂) → Reduce (e x) (e′ x)) →
           Reduce {β = β} {σβ = σβ} (Val (Fun e)) (Val (Fun e′))
  RApp₁  : {τ₁ τ₂ τ₃ τ₄ τ₅ τ₆ : Ty} {σ₃ σ₄ σ₅ σ₆ : Mc} →
           {e₁ e₁′ : term[ var ,
              (τ₂ ⇒ τ₁ ⟨ σ₃ ⟩ τ₃ ⟨ σ₄ ⟩ τ₄) ▷⟨ σ₅ ⟩ τ₅ ]⟨ σ₆ ⟩ τ₆} →
           {e₂ : term[ var , τ₂ ▷⟨ σ₄ ⟩ τ₄ ]⟨ σ₅ ⟩ τ₅} →
           Reduce e₁ e₁′ →
           Reduce (NonVal (App e₁ e₂)) (NonVal (App e₁′ e₂))
  RApp₂  : {τ₁ τ₂ τ₃ τ₄ τ₅ : Ty} {σ₃ σ₄ σ₅ : Mc} →
           {v₁ : value[ var ] (τ₂ ⇒ τ₁ ⟨ σ₃ ⟩ τ₃ ⟨ σ₄ ⟩ τ₄)} →
           {e₂ e₂′ : term[ var , τ₂ ▷⟨ σ₄ ⟩ τ₄ ]⟨ σ₅ ⟩ τ₅} →
           Reduce e₂ e₂′ →
           Reduce (NonVal (App (Val v₁) e₂)) (NonVal (App (Val v₁) e₂′))
  RLet₁  : {τ₁ β γ : Ty} {τ₂▷⟨σα⟩α : CTy} {σβ σγ : Mc} →
           {e₁ e₁′ : term[ var , τ₁ ▷⟨ σβ ⟩ β ]⟨ σγ ⟩ γ} →
           {e₂ : (var τ₁ → term[ var , τ₂▷⟨σα⟩α ]⟨ σβ ⟩ β)} →
           Reduce e₁ e₁′ →
           Reduce (NonVal (Let e₁ e₂)) (NonVal (Let e₁′ e₂))
  RLet₂  : {τ₁ β γ : Ty} {τ₂▷⟨σα⟩α : CTy} {σβ σγ : Mc} →
           {e₁ : term[ var , τ₁ ▷⟨ σβ ⟩ β ]⟨ σγ ⟩ γ} →
           {e₂ e₂′ : (var τ₁ → term[ var , τ₂▷⟨σα⟩α ]⟨ σβ ⟩ β)} →
           ((x : var τ₁) → Reduce (e₂ x) (e₂′ x)) →
           Reduce (NonVal (Let e₁ e₂)) (NonVal (Let e₁ e₂′))
  RReset₁ : {τ α β γ γ' : Ty} {σα σβ σid : Mc} →
           (id : id-cont-type γ σid γ') →
           {e e′ : term[ var , γ ▷⟨ σid ⟩ γ' ]⟨ τ ⇨⟨ σα ⟩ α ∷ σβ ⟩ β} →
           Reduce e e′ →
           Reduce {β = β}
                  (NonVal (Reset id e))
                  (NonVal (Reset id e′))
  -- closure rules
  RId    : {β : Ty} {τ▷⟨σ⟩α : CTy } {σβ : Mc} →
           {e : term[ var , τ▷⟨σ⟩α ]⟨ σβ ⟩ β} →
           Reduce e e
  RTrans : {β : Ty} {τ▷⟨σ⟩α : CTy } {σβ : Mc} →
           {e₁ e₂ e₃ : term[ var , τ▷⟨σ⟩α ]⟨ σβ ⟩ β} →
           Reduce e₁ e₂ →
           Reduce e₂ e₃ →
           Reduce e₁ e₃

-- equational reasoning
module Reasoning where

  infix   _∎
  infixr  _⟶⟨_⟩_ _≡⟨_⟩_
  infix   begin_

  begin_ : {var : Ty → Set} {τ₃ : Ty} {τ₁▷⟨σ₂⟩τ₂ : CTy} {σ₃ : Mc} →
           {e₁ e₂ : term[ var , τ₁▷⟨σ₂⟩τ₂ ]⟨ σ₃ ⟩ τ₃} →
           Reduce e₁ e₂ → Reduce e₁ e₂
  begin_ red = red

  _⟶⟨_⟩_ : {var : Ty → Set} {τ₃ : Ty} {τ₁▷⟨σ₂⟩τ₂ : CTy} {σ₃ : Mc} →
            (e₁ {e₂ e₃} : term[ var , τ₁▷⟨σ₂⟩τ₂ ]⟨ σ₃ ⟩ τ₃) →
            Reduce e₁ e₂ → Reduce e₂ e₃ → Reduce e₁ e₃
  _⟶⟨_⟩_ e₁ {e₂} {e₃} e₁-red-e₂ e₂-red-e₃ = RTrans e₁-red-e₂ e₂-red-e₃

  _≡⟨_⟩_ : {var : Ty → Set} {τ₃ : Ty} {τ₁▷⟨σ₂⟩τ₂ : CTy} {σ₃ : Mc} →
           (e₁ {e₂ e₃} : term[ var , τ₁▷⟨σ₂⟩τ₂ ]⟨ σ₃ ⟩ τ₃) →
           e₁ ≡ e₂ → Reduce e₂ e₃ →
           Reduce e₁ e₃
  _≡⟨_⟩_ e₁ {e₂} {e₃} refl e₂-red-e₃ = e₂-red-e₃

  _∎ : {var : Ty → Set} {τ₃ : Ty} {τ₁▷⟨σ₂⟩τ₂ : CTy} {σ₃ : Mc} →
       (e : term[ var , τ₁▷⟨σ₂⟩τ₂ ]⟨ σ₃ ⟩ τ₃) → Reduce e e
  _∎ e = RId

-- lemma

-- v does not reduce to nonval e
reduceVal : {var : Ty → Set} {τ α : Ty} {σα : Mc} →
            {v : value[ var ] τ } →
            {e : nonvalue[ var , τ ▷⟨ σα ⟩ α ]⟨ σα ⟩ α} →
            Reduce (Val v) (NonVal e) → ⊥
reduceVal (RTrans {e₂ = Val v} red₁ red₂) = reduceVal red₂
reduceVal (RTrans {e₂ = NonVal p} red₁ red₂) =  reduceVal red₁


-- Example

-- term1: (λx.1)@2 = 1
term1 : Reduce {var = 〚_〛τ} {β = Nat} {σβ = •}
          (NonVal (App (Val (Fun (λ x → Val (Num )))) (Val (Num ))))
          (Val (Num ))
term1 = begin
  NonVal (App (Val (Fun (λ x → Val (Num )))) (Val (Num )))
  ⟶⟨ RBetaV (λ x → Val (Num )) (Num ) (Val (Num )) (sVal sNum) ⟩
  Val (Num )
  ∎
  where open Reasoning

-- term2: <(λx.x)@(S0@(λk.k@1))> = 1
term2 : Reduce {var = 〚_〛τ} {β = Nat} {σβ = •}
          (NonVal (Reset (refl , refl , refl)
                   (NonVal (App (Val (Fun (λ x → Val (Var x))))
                                (NonVal (App (Val Shift0)
                                             (Val (Fun (λ k → NonVal (App (Val (Var k))
                                                                          (Val (Num ))))))))))))
          (Val (Num ))
term2 = begin
  NonVal (Reset (refl , refl , refl)
           (NonVal (App (Val (Fun (λ x → Val (Var x))))
                        (NonVal (App (Val Shift0)
                                     (Val (Fun (λ k → NonVal (App (Val (Var k))
                                                                  (Val (Num )))))))))))
  ⟶⟨ RShift0 (refl , refl , refl)
             (Fun (λ k → NonVal (App (Val (Var k)) (Val (Num )))))
             (App₂ (Fun (λ x → Val (Var x))) Hole) ⟩
  NonVal (App (Val (Fun (λ k → NonVal (App (Val (Var k)) (Val (Num ))))))
               (Val (Fun (λ y →
                 NonVal (Reset (refl , refl , refl)
                   (NonVal (App (Val (Fun (λ x → Val (Var x))))
                                (Val (Var y)))))))))
  ⟶⟨ RBetaV (λ k → NonVal (App (Val (Var k)) (Val (Num ))))
             (Fun (λ y →
               NonVal (Reset (refl , refl , refl)
                 (NonVal (App (Val (Fun (λ x → Val (Var x)))) (Val (Var y)))))))
             (NonVal (App (Val (Fun (λ y →
               NonVal (Reset (refl , refl , refl)
                 (NonVal (App (Val (Fun (λ x → Val (Var x))))
                              (Val (Var y))))))))
                  (Val (Num ))))
             (sNonVal (sApp (sVal sVar=) (sVal sNum))) ⟩
  NonVal (App (Val (Fun (λ y →
                 NonVal (Reset (refl , refl , refl)
                   (NonVal (App (Val (Fun (λ x → Val (Var x))))
                                (Val (Var y))))))))
               (Val (Num )))
  ⟶⟨ RBetaV (λ y → NonVal (Reset (refl , refl , refl)
                           (NonVal (App (Val (Fun (λ x → Val (Var x)))) (Val (Var y))))))
             (Num )
             (NonVal (Reset (refl , refl , refl)
               (NonVal (App (Val (Fun (λ x → Val (Var x)))) (Val (Num ))))))
             (sNonVal (sReset (sNonVal (sApp (sVal (sFun (λ x → sVal sVar≠)))
                                             (sVal sVar=))))) ⟩
  NonVal (Reset (refl , refl , refl)
           (NonVal (App (Val (Fun (λ x → Val (Var x)))) (Val (Num )))))
  ⟶⟨ RReset₁ (refl , refl , refl)
             (RBetaV (λ x → Val (Var x)) (Num )
                     (Val (Num )) (sVal sVar=)) ⟩
  NonVal (Reset (refl , refl , refl) (Val (Num )))
  ⟶⟨ RReset (Num ) ⟩
  Val (Num )
  ∎
  where open Reasoning