{-# OPTIONS --rewriting #-}
module DSK where

open import Data.Unit
open import Data.Empty
open import Data.Bool
open import Data.Nat
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality

open import Agda.Builtin.Equality.Rewrite

-- 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 : CTy → Set
id-cont-type (τ ▷⟨ • ⟩ τ') = τ ≡ τ'
id-cont-type (τ ▷⟨ τ₁ ⇨⟨ σ₁ ⟩ τ₁' ∷ σ₂ ⟩ τ')
  = (τ ≡ τ₁) × (τ' ≡ τ₁') × (σ₁ ≡ σ₂)

data Delta : Set where
  K : CTy → Delta
  • : (k : CTy) → id-cont-type k → Delta

data Theta : Set where
  G : Theta
  D : Delta → Theta


Delta→CTy : (Δ : Delta) → CTy
Delta→CTy (K k) = k
Delta→CTy (• k id) = k

Delta-Theta : Delta → Theta → Set
Delta-Theta Δ G = ⊤
Delta-Theta (K k) (D Δ) = ⊥
Delta-Theta (• k id) (D Δ) = ⊤


•-Theta : {k : CTy} → {id : id-cont-type k} →
          (Θ : Theta) → Delta-Theta (• k id) Θ
•-Theta G = tt
•-Theta (D x) = tt

_++_ : Delta → Theta → Delta
Δ ++ G = Δ
d ++ (D Δ) = Δ

_+++_ : Theta → Theta → Theta
G +++ Θ = Θ
D Δ +++ G = D Δ
D Δ₁ +++ D Δ₂ = D Δ₂

Θ+++G≡Θ : (Θ : Theta) → Θ +++ G ≡ Θ
Θ+++G≡Θ G = refl
Θ+++G≡Θ (D Δ) = refl

{-# REWRITE Θ+++G≡Θ #-}

Θ+++DΔ≡Θ : (Θ : Theta) (Δ : Delta) → Θ +++ D Δ ≡ D Δ
Θ+++DΔ≡Θ G Δ = refl
Θ+++DΔ≡Θ (D x) Δ = refl

{-# REWRITE Θ+++DΔ≡Θ #-}

++-assoc : (Δ : Delta) → (Θ' Θ : Theta) →
           Δ ++ (Θ' +++ Θ) ≡ (Δ ++ Θ') ++ Θ
++-assoc Δ G Θ = refl
++-assoc Δ (D Δ') G = refl
++-assoc Δ (D Δ') (D Δ'') = refl

{-# REWRITE ++-assoc #-}

D-++-assoc : (Δ : Delta) → (Θ' Θ : Theta) →
             (D (Δ ++ Θ) +++ Θ') ≡ D (Δ ++ (Θ +++ Θ'))
D-++-assoc Δ G Θ = refl
D-++-assoc Δ (D Δ') Θ = refl

{-# REWRITE D-++-assoc #-}

++-assoc-•D : {k : CTy} {id : id-cont-type k} →
              (Δ : Delta) → (Θ' Θ : Theta) →
              ++-assoc (• k id) (D (Δ ++ Θ')) Θ ≡ ++-assoc Δ Θ' Θ
++-assoc-•D Δ G G = refl
++-assoc-•D Δ G (D x) = refl
++-assoc-•D Δ (D Δ') G = refl
++-assoc-•D Δ (D Δ') (D Δ'') = refl

{-# REWRITE ++-assoc-•D #-}

ΔΘ≡ : {Δ : Delta} {Θ : Theta}
       (ΔΘ₁ ΔΘ₂ : Delta-Theta Δ Θ) → ΔΘ₁ ≡ ΔΘ₂
ΔΘ≡ {Θ = G} tt tt = refl
ΔΘ≡ {Δ = • (γ ▷⟨ σid ⟩ γ') id} {D Δ} tt tt = refl

-- terms
mutual
  data value[_]_ (var : Ty → Set) : Ty → Set where
    -- x
    Var    : {τ₁ : Ty} → (x : var τ₁) → value[ var ] τ₁
    -- n
    Num    : (n : ℕ) → value[ var ] Nat
    -- b
    Bol    : (b : Bool) → value[ var ] Bol
    -- λx.λk.λg.M
    Fun    : {τ₁ τ₂ α β : Ty} → {σα σβ : Mc} →
             (e : var τ₂ → term[ var , K (τ₁ ▷⟨ σα ⟩ α) ]⟨ σβ ⟩ β) →
             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) : Delta → Mc → Ty → Set where
    -- G[K[V]]
    Val    : {τ α : Ty} → {Δ : Delta} → {Θ : Theta} → {σ σ' : Mc} →
             Delta-Theta Δ Θ →
             (c : cont[ var , Δ , τ ]⟨ σ ⟩ α) →
             (v : value[ var ] τ) →
             (m : mcont[ var , Θ , σ' ] σ ) →
             term[ var , Δ ++ Θ ]⟨ σ' ⟩ α
    -- G[K[V@W]]
    App    : {τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ : Theta} {σ σα σβ : Mc} →
             Delta-Theta Δ Θ →
             (v : value[ var ] (τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)) →
             (w : value[ var ] τ₂) →
             (c : cont[ var , Δ , τ₁ ]⟨ σα ⟩ α) →
             (m : mcont[ var , Θ , σ ] σβ ) →
             term[ var , Δ ++ Θ ]⟨ σ ⟩ β

  data cont[_,_,_]⟨_⟩_ (var : Ty → Set) : Delta → Ty → Mc → Ty → Set where
    -- k
    KVar  :  {τ α : Ty} → {σα : Mc} →
             cont[ var , K (τ ▷⟨ σα ⟩ α) , τ ]⟨ σα ⟩ α
    -- kid
    KId    : {γ γ' : Ty} → {σid : Mc} →
             (id : id-cont-type (γ ▷⟨ σid ⟩ γ')) →
             cont[ var , • (γ ▷⟨ σid ⟩ γ') id , γ ]⟨ σid ⟩ γ'
    -- let x = [] in M
    KLet   : {τ α : Ty} → {Δ : Delta} → {σα : Mc} →
             (e : var τ → term[ var , Δ ]⟨ σα ⟩ α) →
             cont[ var , Δ , τ ]⟨ σα ⟩ α

  data mcont[_,_,_]_ (var : Ty → Set) : Theta → Mc → Mc → Set where
    -- g
    GVar   : {σ : Mc} →
             mcont[ var , G , σ ] σ 
    -- K::G
    GCons  : {Δ : Delta} → {Θ : Theta} → {τ α : Ty} → {σ σα σβ : Mc} →
             Delta-Theta Δ Θ →
             (c : cont[ var , Δ , τ ]⟨ σα ⟩ α) →
             (m : mcont[ var , Θ , σ ] σβ ) →
             mcont[ var , D (Δ ++ Θ) , σ ] (τ ⇨⟨ σα ⟩ α ∷ σβ)

-- interpreter
mutual
  〚_〛 : Ty → Set
  〚 Nat 〛 = ℕ
  〚 Bol 〛 = Bool
  〚 τ₂ ⇒ τ₁ ⟨ σ₃ ⟩ τ₃ ⟨ σ₄ ⟩ τ₄ 〛 =
    〚 τ₂ 〛 → (〚 τ₁ 〛 → 〚 σ₃ 〛m → 〚 τ₃ 〛) → 〚 σ₄ 〛m → 〚 τ₄ 〛
  
  〚_〛m : Mc → Set
  〚 • 〛m = ⊤
  〚 τ ⇨⟨ σ ⟩ τ' ∷ σ' 〛m =
    (〚 τ 〛 → 〚 σ 〛m → 〚 τ' 〛) × 〚 σ' 〛m

  〚_〛c : CTy → Set
  〚 τ₁ ▷⟨ σ₂ ⟩ τ₂ 〛c = 〚 τ₁ 〛 → 〚 σ₂ 〛m → 〚 τ₂ 〛

〚_,_〛Θ : Theta → Mc → Set
〚 G , σ 〛Θ = 〚 σ 〛m
〚 D Δ , σ 〛Θ = 〚 Delta→CTy Δ 〛c × 〚 σ 〛m

kid : {γ γ' : Ty} → {σid : Mc} →
      (id : id-cont-type (γ ▷⟨ σid ⟩ γ')) →
      (v : 〚 γ 〛) → (m : 〚 σid 〛m) → 〚 γ' 〛
kid {σid = •} refl v tt = v
kid {σid = τ₁ ⇨⟨ σ ⟩ τ₂ ∷ .σ} (refl , refl , refl) v (k , m) = k v m

mutual
  gv : {τ : Ty} → (v : value[ 〚_〛 ] τ) → 〚 τ 〛
  gv (Var x) = x
  gv (Num n) = n
  gv (Bol b) = b
  gv (Fun e) = λ x k m → g (e x) k m
  gv (Shift id) = λ x k m → x (λ x₂ k₂ m₂ → k x₂ (k₂ , m₂)) (kid id) m
  gv Shift0 = λ {x k (k₀ , m₀) → x (λ x₂ k₂ m₂ → k x₂ (k₂ , m₂)) k₀ m₀}

  g : {τ : Ty} → {Δ : Delta} → {σ : Mc} →
      (e : term[ 〚_〛 , Δ ]⟨ σ ⟩ τ) →
      (Δ : 〚 Delta→CTy Δ 〛c) → (m : 〚 σ 〛m) → 〚 τ 〛
  g (Val {Θ = G} tt c v m) Δ' m' =
    (gc c Δ') (gv v) (gm m m')
  g (Val {Δ = • (γ ▷⟨ σid ⟩ γ') id} {Θ = D Δ} tt c v m) Δ' m' =
    (gc c (kid id)) (gv v) (gm m (Δ' , m'))
  g (App {Θ = G} x v w c m) Δ' m' =
    (gv v) (gv w) (gc c Δ') (gm m m')
  g (App {Δ = • (γ ▷⟨ σid ⟩ γ') id} {Θ = D Δ} x v w c m) Δ' m' =
    (gv v) (gv w) (gc c (kid id)) (gm m (Δ' , m'))

  gc : {Δ : Delta} → {τ α : Ty} → {σα : Mc} →
       (c : cont[ 〚_〛 , Δ , τ ]⟨ σα ⟩ α) →
       (k : 〚 Delta→CTy Δ 〛c) → 〚 τ 〛 → 〚 σα 〛m → 〚 α 〛
  gc KVar k = k
  gc (KId id) k = kid id
  gc (KLet e) k = λ x m → g (e x) k m

  gm : {Θ : Theta} → {σ σ' : Mc} →
       (m : mcont[ 〚_〛 , Θ , σ' ] σ ) →
       (m : 〚 Θ , σ' 〛Θ) → 〚 σ 〛m
  gm GVar m = m
  gm (GCons {Θ = G} tt c m) (Δ , σ) = gc c Δ , gm m σ
  gm (GCons {Δ = • (γ ▷⟨ σid ⟩ γ') id} {Θ = D Δ'} tt c m) (Δ , σ) =
    gc c (kid id) , gm m (Δ , σ)

-- 値による代入規則
mutual
  data SubstV {var : Ty → Set} : {τ τ₁ : Ty} →
              (var τ → value[ var ] τ₁) →
              value[ var ] τ →
              value[ var ] τ₁ → Set where
    sVar=   : {τ : Ty} {v : value[ var ] τ} →
              SubstV (λ x → Var x) v v
    sVar≠   : {τ τ₁ : Ty} {v : value[ var ] τ} {x : var τ₁} →
              SubstV (λ _ → Var x) v (Var x)
    sNum    : {τ : Ty} {v : value[ var ] τ} {n : ℕ} →
              SubstV (λ _ → Num n) v (Num n)
    sBol    : {τ : Ty} {v : value[ var ] τ} {b : Bool} →
              SubstV (λ _ → Bol b) v (Bol b)
    sFun    : {τ′ τ₁ τ₂ α β : Ty} → {σα σβ : Mc} →
              {e  : var τ′ →
                    var τ₂ → term[ var , K (τ₁ ▷⟨ σα ⟩ α) ]⟨ σβ ⟩ β} →
              {v  : value[ var ] τ′} →
              {e′ : var τ₂ → term[ var , K (τ₁ ▷⟨ σα ⟩ α) ]⟨ σβ ⟩ β} →
              ((x : var τ₂) → Subst (λ y → (e y) x) v (e′ x)) →
              SubstV (λ y → Fun (λ x → (e y) x)) v (Fun e′)
    sShift  : {τ τ₁ τ₂ α β γ γ' τ' : Ty} {σ₁ σ₂ σβ σid : Mc}
              {v : value[ var ] τ'} →
              (id : id-cont-type (γ ▷⟨ σid ⟩ γ')) →
              SubstV (λ _ → Shift {τ = τ} {τ₁} {τ₂} {α} {β}
                                  {σ₁ = σ₁} {σ₂} {σβ} {σid} id)
                     v (Shift id)
    sShift0 : {τ τ₀ τ₀' τ₁ τ₂ α β τ' : Ty} {σ₀ σ₀' σ₁ σ₂ : Mc} →
              {v : value[ var ] τ'} →
              SubstV (λ _ → Shift0 {τ = τ} {τ₀} {τ₀'} {τ₁} {τ₂} {α} {β}
                                   {σ₀} {σ₀'} {σ₁} {σ₂})
                     v Shift0

  data Subst {var : Ty → Set} : {τ τ₁ : Ty} {Δ : Delta} {σ : Mc} →
             (var τ → term[ var , Δ ]⟨ σ ⟩ τ₁) →
             value[ var ] τ →
             term[ var , Δ ]⟨ σ ⟩ τ₁ → Set where
    sVal   : {τ' τ α : Ty} → {Δ : Delta} → {Θ : Theta} → {σ σ' : Mc} →
             (ΔΘ : Delta-Theta Δ Θ) →
             {c₁ : var τ' → cont[ var , Δ , τ ]⟨ σ ⟩ α} →
             {v₁ : var τ' → value[ var ] τ} →
             {m₁ : var τ' → mcont[ var , Θ , σ' ] σ} →
             {v  : value[ var ] τ'} →
             {c₂ : cont[ var , Δ , τ ]⟨ σ ⟩ α} →
             {v₂ : value[ var ] τ} →
             {m₂ : mcont[ var , Θ , σ' ] σ} →
             SubstC c₁ v c₂ →
             SubstV v₁ v v₂ →
             SubstM m₁ v m₂ →
             Subst (λ y → Val ΔΘ (c₁ y) (v₁ y) (m₁ y)) v (Val ΔΘ c₂ v₂ m₂)
    sApp   : {τ τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ : Theta} {σ σα σβ : Mc} →
             (ΔΘ : Delta-Theta Δ Θ) →
             {v₁ : var τ → value[ var ] (τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)} →
             {w₁ : var τ → value[ var ] τ₂} →
             {c₁ : var τ → cont[ var , Δ , τ₁ ]⟨ σα ⟩ α} →
             {m₁ : var τ → mcont[ var , Θ , σ ] σβ} →
             {v  : value[ var ] τ} →
             {v₂ : value[ var ] (τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)} →
             {w₂ : value[ var ] τ₂} →
             {c₂ : cont[ var , Δ , τ₁ ]⟨ σα ⟩ α} →
             {m₂ : mcont[ var , Θ , σ ] σβ} →
             SubstV v₁ v v₂ →
             SubstV w₁ v w₂ →
             SubstC c₁ v c₂ →
             SubstM m₁ v m₂ →
             Subst (λ y → App ΔΘ (v₁ y) (w₁ y) (c₁ y) (m₁ y)) v
               (App ΔΘ v₂ w₂ c₂ m₂)

  data SubstC {var : Ty → Set} : {Δ : Delta} → {τ' τ α : Ty} → {σ : Mc} →
              (var τ' → cont[ var , Δ , τ ]⟨ σ ⟩ α) →
              value[ var ] τ' →
              cont[ var , Δ , τ ]⟨ σ ⟩ α → Set where
    sKVar≠ : {τ τ' α : Ty} {σ : Mc} →
             {v : value[ var ] τ'} →
             SubstC {τ = τ} {α} {σ} (λ _ → KVar) v KVar
    sKId   : {τ γ γ' : Ty} → {σid : Mc} →
             {v : value[ var ] τ} →
             (id : id-cont-type (γ ▷⟨ σid ⟩ γ')) →
             SubstC (λ _ → KId id) v (KId id)
    sKLet  : {τ' τ α : Ty} → {Δ : Delta} → {σα : Mc} →
             {e₁ : var τ' → var τ → term[ var , Δ ]⟨ σα ⟩ α} →
             {v  : value[ var ] τ'} →
             {e₂ : var τ → term[ var , Δ ]⟨ σα ⟩ α} →
             ((x : var τ) → Subst (λ y → (e₁ y) x) v (e₂ x)) →
             SubstC (λ y → KLet (e₁ y)) v (KLet e₂)

  data SubstM {var : Ty → Set} : {τ : Ty} → {Θ : Theta} → {σ σ' : Mc} →
              (var τ → mcont[ var , Θ , σ' ] σ) →
              value[ var ] τ →
              mcont[ var , Θ , σ' ] σ → Set where
    sGVar≠ : {τ : Ty} {σ : Mc} →
             {v : value[ var ] τ} →
             SubstM {σ = σ} (λ _ → GVar) v GVar
    sGCons : {Δ : Delta} {Θ : Theta} → {τ' τ α : Ty} → {σ σα σβ : Mc} →
             (ΔΘ : Delta-Theta Δ Θ) →
             {c₁ : var τ' → cont[ var , Δ , τ ]⟨ σα ⟩ α} →
             {m₁ : var τ' → mcont[ var , Θ , σ ] σβ} →
             {v  : value[ var ] τ'} →
             {c₂ : cont[ var , Δ , τ ]⟨ σα ⟩ α} →
             {m₂ : mcont[ var , Θ , σ ] σβ} →
             SubstC c₁ v c₂ →
             SubstM m₁ v m₂ →
             SubstM (λ y → GCons ΔΘ (c₁ y) (m₁ y)) v (GCons ΔΘ c₂ m₂)

-- コンテキストの代入規則
mutual
  data CSubst {var : Ty → Set} : {τ α β : Ty} {Δ : Delta} {σα σβ : Mc} →
              term[ var , K (τ ▷⟨ σα ⟩ α) ]⟨ σβ ⟩ β →
              cont[ var , Δ , τ ]⟨ σα ⟩ α →
              term[ var , Δ ]⟨ σβ ⟩ β → Set where
    sVal₁  : {Δ : Delta} → {τ α τ' α' : Ty} → {σ σα σα' : Mc} →
             {c₁ : cont[ var , K (τ' ▷⟨ σα' ⟩ α') , τ ]⟨ σα ⟩ α} →
             {v  : value[ var ] τ} →
             {m  : mcont[ var , G , σ ] σα} →
             {c  : cont[ var , Δ , τ' ]⟨ σα' ⟩ α'} →
             {c₂ : cont[ var , Δ , τ ]⟨ σα ⟩ α} →
             CSubstC c₁ c c₂ →
             CSubst (Val tt c₁ v m) c (Val tt c₂ v m)
    sVal₂  : {Δ : Delta} → {κ : CTy} → {τ α β τ' : Ty} → {σ σα σβ : Mc} →
             {id : id-cont-type κ} →
             {c' : cont[ var , • κ id , τ' ]⟨ σβ ⟩ β} →
             {v  : value[ var ] τ'} →
             {m₁ : mcont[ var , D (K (τ ▷⟨ σα ⟩ α)) , σ ] σβ} →
             {c  : cont[ var , Δ , τ ]⟨ σα ⟩ α} →
             {m₂ : mcont[ var , D Δ , σ ] σβ} →
             CSubstM m₁ c m₂ →
             CSubst (Val tt c' v m₁) c (Val tt c' v m₂)
    sApp₁  : {τ₁ τ₂ α β τ₁' α' : Ty} {Δ : Delta} {σα σβ σ' σα' : Mc} →
             {v  : value[ var ] (τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)} →
             {w  : value[ var ] τ₂} →
             {c₁ : cont[ var , K (τ₁' ▷⟨ σα' ⟩ α') , τ₁ ]⟨ σα ⟩ α} →
             {m  : mcont[ var , G , σ' ] σβ} →
             {c  : cont[ var , Δ , τ₁' ]⟨ σα' ⟩ α'} →
             {c₂ : cont[ var , Δ , τ₁ ]⟨ σα ⟩ α} →
             CSubstC c₁ c c₂ →
             CSubst (App tt v w c₁ m) c (App tt v w c₂ m)
    sApp₂  : {τ₁ τ₂ α β τ₁' α' : Ty} {Δ : Delta} {κ : CTy}
             {σα σβ σ' σα' : Mc} →
             {id : id-cont-type κ} →
             {v  : value[ var ] (τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)} →
             {w  : value[ var ] τ₂} →
             {c' : cont[ var , • κ id , τ₁ ]⟨ σα ⟩ α} →
             {m₁ : mcont[ var , D (K (τ₁' ▷⟨ σα' ⟩ α')) , σ' ] σβ} →
             {c  : cont[ var , Δ , τ₁' ]⟨ σα' ⟩ α'} →
             {m₂ : mcont[ var , D Δ , σ' ] σβ} →
             CSubstM m₁ c m₂ →
             CSubst (App tt v w c' m₁) c (App tt v w c' m₂)

  data CSubstC {var : Ty → Set} : {Δ : Delta} {τ α τ' α' : Ty} {σ σ' : Mc} →
               cont[ var , K (τ ▷⟨ σ ⟩ α) , τ' ]⟨ σ' ⟩ α' →
               cont[ var , Δ , τ ]⟨ σ ⟩ α →
               cont[ var , Δ , τ' ]⟨ σ' ⟩ α' → Set where
    sKVar= : {Δ : Delta} {τ α : Ty} {σα : Mc} →
             {c : cont[ var , Δ , τ ]⟨ σα ⟩ α} →
             CSubstC KVar c c
    sKLet₂ : {Δ : Delta} {τ α β τ' : Ty} {σα σβ : Mc} →
             {e₁ : var τ' → term[ var , K (τ ▷⟨ σα ⟩ α) ]⟨ σβ ⟩ β} →
             {c  : cont[ var , Δ , τ ]⟨ σα ⟩ α} →
             {e₂ : var τ' → term[ var , Δ ]⟨ σβ ⟩ β} →
             ((x : var τ') → CSubst (e₁ x) c (e₂ x)) →
             CSubstC (KLet e₁) c (KLet e₂)

  data CSubstM {var : Ty → Set} : {Δ : Delta} {τ α : Ty} {σ σα σβ : Mc} →
               mcont[ var , D (K (τ ▷⟨ σα ⟩ α)) , σ ] σβ →
               cont[ var , Δ , τ ]⟨ σα ⟩ α →
               mcont[ var , D Δ , σ ] σβ → Set where
    sGCons₁ : {Δ : Delta} {τ α τ' α' : Ty} {σ σβ σα σα' : Mc} →
              {c₁ : cont[ var , K (τ ▷⟨ σα ⟩ α) , τ' ]⟨ σα' ⟩ α'} →
              {m  : mcont[ var , G , σ ] σβ} →
              {c  : cont[ var , Δ , τ ]⟨ σα ⟩ α} →
              {c₂ : cont[ var , Δ , τ' ]⟨ σα' ⟩ α'} →
              CSubstC c₁ c c₂ →
              CSubstM (GCons tt c₁ m) c (GCons tt c₂ m)
    sGCons₂ : {Δ : Delta} {κ : CTy} {τ α τ₁ α₁ : Ty} {σ σβ σα σ₁ : Mc} →
              {id : id-cont-type κ} →
              {c' : cont[ var , • κ id , τ₁ ]⟨ σ₁ ⟩ α₁} →
              {m₁ : mcont[ var , D (K (τ ▷⟨ σα ⟩ α)) , σ ] σβ} →
              {c  : cont[ var , Δ , τ ]⟨ σα ⟩ α} →
              {m₂ : mcont[ var , D Δ , σ ] σβ} →
              CSubstM m₁ c m₂ →
              CSubstM (GCons tt c' m₁) c (GCons tt c' m₂)


-- メタ継続の代入規則
mutual
  data MSubst {var : Ty → Set} :
              {β : Ty} {Δ Δ' : Delta} {Θ : Theta} {σ σβ : Mc} →
              term[ var , Δ ]⟨ σβ ⟩ β →
              mcont[ var , Θ , σ ] σβ →
              Δ' ≡ Δ ++ Θ →
              term[ var , Δ' ]⟨ σ ⟩ β → Set where
    sVal   : {τ β : Ty} {Δ : Delta} {Θ Θ' : Theta} {σ σ' σβ : Mc} →
             (ΔΘ : Delta-Theta Δ (Θ' +++ Θ)) →
             (ΔΘ' : Delta-Theta Δ Θ') →
             {c  : cont[ var , Δ , τ ]⟨ σβ ⟩ β} →
             {v  : value[ var ] τ} →
             {m₁ : mcont[ var , Θ' , σ' ] σβ} →
             {m  : mcont[ var , Θ , σ ] σ'} →
             {m₂ : mcont[ var , Θ' +++ Θ , σ ] σβ} →
             MSubstM m₁ m refl m₂ →
             MSubst (Val ΔΘ' c v m₁) m refl --(++-assoc Δ Θ' Θ)
                    (Val ΔΘ c v m₂)
    sApp   : {τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ Θ' : Theta}
             {σ σ' σα σβ : Mc} →
             (ΔΘ : Delta-Theta Δ (Θ' +++ Θ)) →
             (ΔΘ' : Delta-Theta Δ Θ') →
             (v  : value[ var ] (τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)) →
             (w  : value[ var ] τ₂) →
             (c  : cont[ var , Δ , τ₁ ]⟨ σα ⟩ α) →
             (m₁ : mcont[ var , Θ' , σ' ] σβ) →
             {m  : mcont[ var , Θ , σ ] σ'} →
             {m₂ : mcont[ var , Θ' +++ Θ , σ ] σβ} →
             MSubstM m₁ m refl m₂ →
             MSubst (App ΔΘ' v w c m₁) m refl --(++-assoc Δ Θ' Θ)
                    (App ΔΘ v w c m₂)
 
  data MSubstM {var : Ty → Set} : {Θ Θ' Θ'+Θ : Theta} {σ σ' σβ : Mc} →
               mcont[ var , Θ' , σ' ] σβ →
               mcont[ var , Θ , σ ] σ' →
               Θ'+Θ ≡ Θ' +++ Θ →
               mcont[ var , Θ'+Θ , σ ] σβ → Set where
    mGVar= : {Θ : Theta} {σ σ' : Mc} →
             {m : mcont[ var , Θ , σ ] σ'} →
             MSubstM GVar m refl m
    mGCons : {Δ : Delta} {Θ Θ' : Theta} {τ α : Ty} {σ σ' σβ σα : Mc} →
             (ΔΘ' : Delta-Theta Δ (Θ +++ Θ')) →
             (ΔΘ : Delta-Theta Δ Θ) →
             {c  : cont[ var , Δ , τ ]⟨ σα ⟩ α} →
             {m₁ : mcont[ var , Θ , σ ] σβ} →
             {m  : mcont[ var , Θ' , σ' ] σ} →
             {m₂ : mcont[ var , Θ +++ Θ' , σ' ] σβ} →
             MSubstM m₁ m refl m₂ →
             MSubstM (GCons ΔΘ c m₁) m refl -- (sym (D-++-assoc Δ Θ' Θ))
                     (GCons ΔΘ' c m₂)

--reduction rules
mutual
  data Reduce {var : Ty → Set} :
              {τ₁ : Ty} → {Δ : Delta} → {σ : Mc} →
              term[ var , Δ ]⟨ σ ⟩ τ₁ →
              term[ var , Δ ]⟨ σ ⟩ τ₁ → Set where
    -- (λx.λk.λg.M) V K G -> M[x:=V][k:=K][g:=G]
    RBetaV  : {τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ : Theta} {σ σα σβ : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {e₁ : var τ₂ → term[ var , K (τ₁ ▷⟨ σα ⟩ α) ]⟨ σβ ⟩ β} →
              {v : value[ var ] τ₂} →
              {c : cont[ var , Δ , τ₁ ]⟨ σα ⟩ α} →
              {m : mcont[ var , Θ , σ ] σβ} →
              {e₁' : term[ var , K (τ₁ ▷⟨ σα ⟩ α) ]⟨ σβ ⟩ β} →
              {e₁'' : term[ var , Δ ]⟨ σβ ⟩ β} →
              {e₂ : term[ var , Δ ++ Θ ]⟨ σ ⟩ β} →
              Subst e₁ v e₁' →
              CSubst e₁' c e₁'' →
              MSubst e₁'' m refl e₂ →
              Reduce (App ΔΘ (Fun (λ x → e₁ x)) v c m)
                     e₂
    -- (λx.λg.M) V G -> M[x:=V][g:=G]
    RBetaLet : {τ α : Ty} {Δ : Delta} {Θ : Theta} {σ σα : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {e₁ : var τ → term[ var , Δ ]⟨ σα ⟩ α} →
              {v  : value[ var ] τ} →
              {m  : mcont[ var , Θ , σ ] σα} →
              {e₁' : term[ var , Δ ]⟨ σα ⟩ α} →
              {e₂ : term[ var , Δ ++ Θ ]⟨ σ ⟩ α} →
              Subst e₁ v e₁' →
              MSubst e₁' m refl e₂ →
              Reduce (Val ΔΘ (KLet e₁) v m) e₂
    -- S W J G -> W (λy.λk.λg.J y (k :: g)) Kid G
    RShift  : {τ τ₁ τ₂ τ₄ τ₅ α β γ γ' τ' α' : Ty} {Δ : Delta}
              {σ σ₁ σ₂ σ₅ σid σα' σβ' : Mc} →
              (id₁ : id-cont-type (γ ▷⟨ σid ⟩ γ')) →
              (id₂ : id-cont-type (τ₄ ▷⟨ σ₅ ⟩ τ₅)) →
              {w : value[ var ]
                   ((τ ⇒ τ₁ ⟨ σ₁ ⟩ τ₂ ⟨ σ₂ ⟩ α)
                      ⇒ γ ⟨ σid ⟩ γ' ⟨ τ' ⇨⟨ σα' ⟩ α' ∷ σβ' ⟩ β)} →
              {j : cont[ var , • (τ₄ ▷⟨ σ₅ ⟩ τ₅) id₂ , τ ]⟨ τ₁ ⇨⟨ σ₁ ⟩ τ₂ ∷ σ₂ ⟩ α} →
              {m : mcont[ var , D Δ , σ ] (τ' ⇨⟨ σα' ⟩ α' ∷ σβ')} →
              Reduce (App (•-Theta {τ₄ ▷⟨ σ₅ ⟩ τ₅} {id₂} (D Δ)) (Shift id₁) w j m)
                     (App (•-Theta {γ ▷⟨ σid ⟩ γ'} {id₁} (D Δ))
                          w (Fun (λ y → Val tt j (Var y) (GCons tt KVar GVar)))
                          (KId id₁) m)
    -- S0 W J (K :: G) -> W (λy.λk.λg.J y (k :: g)) K G
    RShift0 : {τ τ₀ τ₀' τ₁ τ₂ α β γ γ' : Ty} {Δ : Delta} {Θ : Theta}
              {σ σ₀ σ₀' σ₁ σ₂ σid : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              (id : id-cont-type (γ ▷⟨ σid ⟩ γ')) →
              {w : value[ var ] ((τ ⇒ τ₁ ⟨ σ₁ ⟩ τ₂ ⟨ σ₂ ⟩ α)
                                 ⇒ τ₀ ⟨ σ₀ ⟩ τ₀' ⟨ σ₀' ⟩ β)} →
              {j : cont[ var , • (γ ▷⟨ σid ⟩ γ') id , τ ]⟨ τ₁ ⇨⟨ σ₁ ⟩ τ₂ ∷ σ₂ ⟩ α} →
              {c : cont[ var , Δ , τ₀ ]⟨ σ₀ ⟩ τ₀'} →
              {m : mcont[ var , Θ , σ ] σ₀'} →
              Reduce (App tt Shift0 w j (GCons ΔΘ c m))
                     (App ΔΘ w (Fun (λ y → Val tt j (Var y)
                                                     (GCons tt KVar GVar)))
                          c m)
    -- KId V (K :: G) -> K V G
    RReset  : {τ α : Ty} → {Δ : Delta} → {Θ : Theta} → {σ σ' : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {v : value[ var ] τ} →
              {c : cont[ var , Δ , τ ]⟨ σ ⟩ α} →
              {m  : mcont[ var , Θ , σ' ] σ} →
              Reduce (Val tt (KId (refl , refl , refl)) v (GCons ΔΘ c m))
                     (Val ΔΘ c v m)

    -- congruence rules
    RVal₁   : {τ α : Ty} → {Δ : Delta} → {Θ : Theta} → {σ σ' : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {c c' : cont[ var , Δ , τ ]⟨ σ ⟩ α} →
              {v : value[ var ] τ} →
              {m : mcont[ var , Θ , σ' ] σ} →
              ReduceC c c' →
              Reduce (Val ΔΘ c v m)
                     (Val ΔΘ c' v m)
    RVal₂   : {τ α : Ty} → {Δ : Delta} → {Θ : Theta} → {σ σ' : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {c : cont[ var , Δ , τ ]⟨ σ ⟩ α} →
              {v v' : value[ var ] τ} →
              {m : mcont[ var , Θ , σ' ] σ} →
              ReduceV v v' →
              Reduce (Val ΔΘ c v m)
                     (Val ΔΘ c v' m)
    RVal₃   : {τ α : Ty} → {Δ : Delta} → {Θ : Theta} → {σ σ' : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {c : cont[ var , Δ , τ ]⟨ σ ⟩ α} →
              {v : value[ var ] τ} →
              {m m' : mcont[ var , Θ , σ' ] σ} →
              ReduceM m m' →
              Reduce (Val ΔΘ c v m)
                     (Val ΔΘ c v m')
    RApp₁   : {τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ : Theta} {σ σα σβ : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {v v' : value[ var ] (τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)} →
              {w : value[ var ] τ₂} →
              {c : cont[ var , Δ , τ₁ ]⟨ σα ⟩ α} →
              {m : mcont[ var , Θ , σ ] σβ} →
              ReduceV v v' →
              Reduce (App ΔΘ v w c m)
                     (App ΔΘ v' w c m)
    RApp₂   : {τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ : Theta} {σ σα σβ : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {v : value[ var ] (τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)} →
              {w w' : value[ var ] τ₂} →
              {c : cont[ var , Δ , τ₁ ]⟨ σα ⟩ α} →
              {m : mcont[ var , Θ , σ ] σβ} →
              ReduceV w w' →
              Reduce (App ΔΘ v w c m)
                     (App ΔΘ v w' c m)
    RApp₃   : {τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ : Theta} {σ σα σβ : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {v : value[ var ] (τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)} →
              {w : value[ var ] τ₂} →
              {c c' : cont[ var , Δ , τ₁ ]⟨ σα ⟩ α} →
              {m : mcont[ var , Θ , σ ] σβ} →
              ReduceC c c' →
              Reduce (App ΔΘ v w c m)
                     (App ΔΘ v w c' m)
    RApp₄   : {τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ : Theta} {σ σα σβ : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {v : value[ var ] (τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)} →
              {w : value[ var ] τ₂} →
              {c : cont[ var , Δ , τ₁ ]⟨ σα ⟩ α} →
              {m m' : mcont[ var , Θ , σ ] σβ} →
              ReduceM m m' →
              Reduce (App ΔΘ v w c m)
                     (App ΔΘ v w c m')

    -- closure rules
    RId     : {τ₁ : Ty} {Δ : Delta} {σ : Mc} →
              {e : term[ var , Δ ]⟨ σ ⟩ τ₁} →
              Reduce e e
    RTrans  : {τ₁ : Ty} {Δ : Delta} {σ : Mc} →
              {e₁ e₂ e₃ : term[ var , Δ ]⟨ σ ⟩ τ₁} →
              Reduce e₁ e₂ →
              Reduce e₂ e₃ →
              Reduce e₁ e₃

  data ReduceV {var : Ty → Set} :
               {τ₁ : Ty} →
               value[ var ] τ₁ →
               value[ var ] τ₁ → Set where
    -- λx.λk.λg.V x k g -> V
    REtaV   : {τ₁ τ₂ α β : Ty} → {σα σβ : Mc} → 
              {v : value[ var ] (τ₂ ⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)} →
              ReduceV (Fun (λ x → App tt v (Var x) KVar GVar)) v

    -- congruence rule
    RFun    : {τ₁ τ₂ α β : Ty} → {σα σβ : Mc} →
              {e e' : var τ₂ → term[ var , K (τ₁ ▷⟨ σα ⟩ α) ]⟨ σβ ⟩ β} →
              ((x : var τ₂) → Reduce (e x) (e' x)) →
              ReduceV (Fun e) (Fun e')
    -- closure rules
    RId     : {τ₁ : Ty} →
              {v : value[ var ] τ₁} →
              ReduceV v v
    RTrans  : {τ₁ : Ty} →
              {v₁ v₂ v₃ : value[ var ] τ₁} →
              ReduceV v₁ v₂ →
              ReduceV v₂ v₃ →
              ReduceV v₁ v₃

  data ReduceC {var : Ty → Set} : {Δ : Delta} → {τ α : Ty} → {σα : Mc} →
               cont[ var , Δ , τ ]⟨ σα ⟩ α →
               cont[ var , Δ , τ ]⟨ σα ⟩ α → Set where
    -- (λx.λg.K x g) -> K
    REtaLet : {τ α : Ty} → {Δ : Delta} → {σα : Mc} →
              {c : cont[ var , Δ , τ ]⟨ σα ⟩ α} →
              ReduceC (KLet (λ x → Val tt c (Var x) GVar)) c

    -- congruence rule
    RKLet   : {τ α : Ty} → {Δ : Delta} → {σα : Mc} →
              {e e' : var τ → term[ var , Δ ]⟨ σα ⟩ α} →
              ((x : var τ) → Reduce (e x) (e' x)) →
              ReduceC (KLet e) (KLet e')

    -- closure rules
    RId     : {Δ : Delta} → {τ α : Ty} → {σα : Mc} →
              {c : cont[ var , Δ , τ ]⟨ σα ⟩ α} →
              ReduceC c c
    RTrans  : {Δ : Delta} → {τ α : Ty} → {σα : Mc} →
              {c₁ c₂ c₃ : cont[ var , Δ , τ ]⟨ σα ⟩ α} →
              ReduceC c₁ c₂ →
              ReduceC c₂ c₃ →
              ReduceC c₁ c₃

  data ReduceM {var : Ty → Set} : {Θ : Theta} → {σ σ' : Mc} →
               mcont[ var , Θ , σ ] σ' →
               mcont[ var , Θ , σ ] σ' → Set where
    -- congruence rule
    RGCons₁ : {Δ : Delta} → {Θ : Theta} → {τ α : Ty} → {σ σ' σα : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {c c' : cont[ var , Δ , τ ]⟨ σα ⟩ α} →
              {m : mcont[ var , Θ , σ ] σ'} →
              ReduceC c c' →
              ReduceM (GCons ΔΘ c m) (GCons ΔΘ c' m)
    RGCons₂ : {Δ : Delta} → {Θ : Theta} → {τ α : Ty} → {σ σ' σα : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {c : cont[ var , Δ , τ ]⟨ σα ⟩ α} →
              {m m' : mcont[ var , Θ , σ ] σ'} →
              ReduceM m m' →
              ReduceM (GCons ΔΘ c m) (GCons ΔΘ c m')


-- equational reasoning
module Reasoning where

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

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

  _⟶⟨_⟩_ : {var : Ty → Set} {τ₁ : Ty} {Δ : Delta} {σ : 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} {Δ : Delta} {σ : 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} {Δ : Delta} {σ : Mc} →
       (e : term[ var , Δ ]⟨ σ ⟩ τ₁) → Reduce e e
  _∎ e = RId

-- 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 e) = sFun (λ x → Subst≠ (e x))
  SubstV≠ (Shift id) = sShift id
  SubstV≠ Shift0 = sShift0

  Subst≠ : {var : Ty → Set} {τ α : Ty} {Δ : Delta} {σ : Mc} →
           (e₁ : term[ var , Δ ]⟨ σ ⟩ α) →
           {v : value[ var ] τ} →
           Subst (λ _ → e₁) v e₁
  Subst≠ (Val ΔΘ c v m) =
    sVal ΔΘ (SubstC≠ c) (SubstV≠ v) (SubstM≠ m)
  Subst≠ (App ΔΘ v w c m) =
    sApp ΔΘ (SubstV≠ v) (SubstV≠ w) (SubstC≠ c) (SubstM≠ m)

  SubstC≠ : {var : Ty → Set} {Δ : Delta} {τ' τ α : Ty} {σα : Mc} →
            (c₁ : cont[ var , Δ , τ ]⟨ σα ⟩ α) →
            {v : value[ var ] τ'} →
            SubstC (λ _ → c₁) v c₁
  SubstC≠ KVar = sKVar≠
  SubstC≠ (KId id) = sKId id
  SubstC≠ (KLet e) = sKLet (λ x → Subst≠ (e x))

  SubstM≠ : {var : Ty → Set} {τ : Ty} {Θ : Theta} {σ σ' : Mc} →
            (m₁ : mcont[ var , Θ , σ ] σ') →
            {v : value[ var ] τ} →
            SubstM (λ _ → m₁) v m₁
  SubstM≠ GVar = sGVar≠
  SubstM≠ (GCons ΔΘ c m) = sGCons ΔΘ (SubstC≠ c) (SubstM≠ m)