{-# OPTIONS --rewriting #-}
module CPS 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

-- target type
mutual
  data Ty : Set where
    Nat : Ty
    Bol : Ty
    _⇒[_]⇒_⇒_ : Ty → CTy → Mc → Ty → Ty

  data CTy : Set where
    _⇒_⇒_ : Ty → Mc → Ty → CTy

  data Mc : Set where
    [] : Mc
    _∷_ : CTy → Mc → Mc

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 Δ) = ⊤

Delta-Theta-K : Delta → Theta → Delta → Delta → Theta → Set
Delta-Theta-K (K x) G Δ Δ₂ Θ₂ = Δ ≡ Δ₂ × Θ₂ ≡ G
Delta-Theta-K (K x) (D x₁) Δ Δ₂ Θ₂ = ⊥
Delta-Theta-K (• k x) G Δ Δ₂ Θ₂ = ⊥
Delta-Theta-K (• k x) (D (K x₁)) Δ Δ₂ Θ₂ = Δ₂ ≡ (• k x) × Θ₂ ≡ D Δ
Delta-Theta-K (• k x) (D (• k₁ x₁)) Δ Δ₂ Θ₂ = ⊥

•-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


-- CPS 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
    -- K V G
    Val    : {τ α : Ty} → {Δ : Delta} → {Θ : Theta} → {σ σ' : Mc} →
             Delta-Theta Δ Θ →
             (k : cont[ var , Δ ] (τ ⇒ σ ⇒ α)) →
             (v : value[ var ] τ) →
             (g : mcont[ var , Θ , σ' ] σ) →
             term[ var , Δ ++ Θ , σ' ]⇒ α
    -- V W K G
    App    : {τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ : Theta} {σ σα σβ : Mc} →
             Delta-Theta Δ Θ →
             (v : value[ var ] (τ₂ ⇒[ τ₁ ⇒ σα ⇒ α ]⇒ σβ ⇒ β)) →
             (w : value[ var ] τ₂) →
             (k : cont[ var , Δ ] (τ₁ ⇒ σα ⇒ α)) →
             (g : mcont[ var , Θ , σ ] σβ) →
             term[ var , Δ ++ Θ , σ ]⇒ β

  data cont[_,_]_ (var : Ty → Set) : Delta → CTy → Set where
    -- k
    KVar   : {k : CTy} →
             cont[ var , K k ] k
    -- kid
    KId    : {γ γ' : Ty} → {σid : Mc} →
             (id : id-cont-type (γ ⇒ σid ⇒ γ')) →
             cont[ var , • (γ ⇒ σid ⇒ γ') id ] (γ ⇒ σid ⇒ γ')
    -- λx.λg.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} → {Δ' : CTy} → {σ σ' : Mc} →
             Delta-Theta Δ Θ →
             (k : cont[ var , Δ ] Δ') →
             (g : mcont[ var , Θ , σ ] σ') →
             mcont[ var , D (Δ ++ Θ) , σ ] (Δ' ∷ σ')

-- example
-- λx.λk.k x
val1 : {var : Ty → Set} → {τ₁ α : Ty} → {σ : Mc} →
       value[ var ] (τ₁ ⇒[ τ₁ ⇒ σ ⇒ α ]⇒ σ ⇒ α)
val1 = Fun (λ x → Val tt KVar (Var x) GVar)

-- interpreter
mutual
  〚_〛 : Ty → Set
  〚 Nat 〛 = ℕ
  〚 Bol 〛 = Bool
  〚 τ₂ ⇒[ τ₁ ⇒ σ₃ ⇒ τ₃ ]⇒ σ₄ ⇒ τ₄ 〛 =
    〚 τ₂ 〛 → (〚 τ₁ 〛 → 〚 σ₃ 〛m → 〚 τ₃ 〛) → 〚 σ₄ 〛m → 〚 τ₄ 〛
  
  〚_〛m : Mc → Set
  〚 [] 〛m = ⊤
  〚 Δ ∷ σ 〛m = 〚 Δ 〛c × 〚 σ 〛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 k v m) Δ' m' =
    (gc k Δ') (gv v) (gm m m')
  g (Val {Δ = • (γ ⇒ σid ⇒ γ') id} {Θ = D Δ} tt k v m) Δ' m' =
    (gc k (kid id)) (gv v) (gm m (Δ' , m'))
  g (App {Θ = G} x v w k m) Δ' m' =
    (gv v) (gv w) (gc k Δ') (gm m m')
  g (App {Δ = • (γ ⇒ σid ⇒ γ') id} {Θ = D Δ} x v w k m) Δ' m' =
    (gv v) (gv w) (gc k (kid id)) (gm m (Δ' , m'))

  gc : {Δ : Delta} → {k' : CTy} →
       (c : cont[ 〚_〛 , Δ ] k') →
       (k : 〚 Delta→CTy Δ 〛c) → 〚 k' 〛c
  gc KVar k = k
  gc (KId id) k = kid id
  gc (KLet e) k = λ x m → g (e x) k m

  gm : {Θ : Theta} → {σ σ' : Mc} →
       (g : mcont[ 〚_〛 , Θ , σ' ] σ) →
       (m : 〚 Θ , σ' 〛Θ) → 〚 σ 〛m
  gm GVar m = m
  gm (GCons {Θ = G} tt k m) (Δ , σ) = gc k Δ , gm m σ
  gm (GCons {Δ = • (γ ⇒ σid ⇒ γ') id} {Θ = D Δ'} tt k m) (Δ , σ) =
    gc k (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 Δ Θ) →
             {k₁ : var τ' → cont[ var , Δ ] (τ ⇒ σ ⇒ α)} →
             {v₁ : var τ' → value[ var ] τ} →
             {m₁ : var τ' → mcont[ var , Θ , σ' ] σ} →
             {v  : value[ var ] τ'} →
             {k₂ : cont[ var , Δ ] (τ ⇒ σ ⇒ α)} →
             {v₂ : value[ var ] τ} →
             {m₂ : mcont[ var , Θ , σ' ] σ} →
             SubstC k₁ v k₂ →
             SubstV v₁ v v₂ →
             SubstM m₁ v m₂ →
             Subst (λ y → Val ΔΘ (k₁ y) (v₁ y) (m₁ y)) v (Val ΔΘ k₂ v₂ m₂)
    sApp   : {τ τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ : Theta} {σ σα σβ : Mc} →
             (ΔΘ : Delta-Theta Δ Θ) →
             {v₁ : var τ → value[ var ] (τ₂ ⇒[ τ₁ ⇒ σα ⇒ α ]⇒ σβ ⇒ β)} →
             {w₁ : var τ → value[ var ] τ₂} →
             {k₁ : var τ → cont[ var , Δ ] (τ₁ ⇒ σα ⇒ α)} →
             {m₁ : var τ → mcont[ var , Θ , σ ] σβ} →
             {v  : value[ var ] τ} →
             {v₂ : value[ var ] (τ₂ ⇒[ τ₁ ⇒ σα ⇒ α ]⇒ σβ ⇒ β)} →
             {w₂ : value[ var ] τ₂} →
             {k₂ : cont[ var , Δ ] (τ₁ ⇒ σα ⇒ α)} →
             {m₂ : mcont[ var , Θ , σ ] σβ} →
             SubstV v₁ v v₂ →
             SubstV w₁ v w₂ →
             SubstC k₁ v k₂ →
             SubstM m₁ v m₂ →
             Subst (λ y → App ΔΘ (v₁ y) (w₁ y) (k₁ y) (m₁ y)) v
                   (App ΔΘ v₂ w₂ k₂ m₂)

  data SubstC {var : Ty → Set} : {τ : Ty} → {Δ : Delta} → {k : CTy} →
              (var τ → cont[ var , Δ ] k) →
              value[ var ] τ →
              cont[ var , Δ ] k → Set where
    sKVar≠ : {τ : Ty} {k : CTy} →
             {v : value[ var ] τ} →
             SubstC {k = k} (λ _ → 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 : {τ : Ty} {Δ : Delta} {Θ : Theta} {Δ' : CTy} {σ σ' : Mc} →
             (ΔΘ : Delta-Theta Δ Θ) →
             {k₁ : var τ → cont[ var , Δ ] Δ'} →
             {m₁ : var τ → mcont[ var , Θ , σ ] σ'} →
             {v  : value[ var ] τ} →
             {k₂ : cont[ var , Δ ] Δ'} →
             {m₂ : mcont[ var , Θ , σ ] σ'} →
             SubstC k₁ v k₂ →
             SubstM m₁ v m₂ →
             SubstM (λ y → GCons ΔΘ (k₁ y) (m₁ y)) v (GCons ΔΘ k₂ m₂)

-- 継続の代入規則
mutual
  data CSubst {var : Ty → Set} : {β : Ty} {Δ : Delta} {κ : CTy} {σβ : Mc} →
              term[ var , K κ , σβ ]⇒ β →
              cont[ var , Δ ] κ →
              term[ var , Δ , σβ ]⇒ β → Set where
    sVal₁  : {τ β : Ty} → {Δ : Delta} → {κ : CTy} → {σ σ' : Mc} →
             {k₁ : cont[ var , K κ ] (τ ⇒ σ ⇒ β)} →
             {v  : value[ var ] τ} →
             {m  : mcont[ var , G , σ' ] σ} →
             {c  : cont[ var , Δ ] κ} →
             {k₂ : cont[ var , Δ ] (τ ⇒ σ ⇒ β)} →
             CSubstC k₁ c k₂ →
             CSubst (Val tt k₁ v m) c (Val tt k₂ v m)
    sVal₂  : {τ β : Ty} → {Δ : Delta} → {κ κ' : CTy} → {σ σ' : Mc} →
             {id : id-cont-type κ'} →
             {k  : 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 k v m₁) c (Val tt k v m₂)
    sApp₁  : {τ₁ τ₂ α β : Ty} {Δ : Delta} {κ : CTy} {σα σβ σ' : Mc} →
             {v  : value[ var ] (τ₂ ⇒[ τ₁ ⇒ σα ⇒ α ]⇒ σβ ⇒ β)} →
             {w  : value[ var ] τ₂} →
             {k₁ : cont[ var , K κ ] (τ₁ ⇒ σα ⇒ α)} →
             {m  : mcont[ var , G , σ' ] σβ} →
             {c  : cont[ var , Δ ] κ} →
             {k₂ : cont[ var , Δ ] (τ₁ ⇒ σα ⇒ α)} →
             CSubstC k₁ c k₂ →
             CSubst (App tt v w k₁ m) c (App tt v w k₂ m)
    sApp₂  : {τ₁ τ₂ α β : Ty} {Δ : Delta} {κ κ' : CTy}
             {σα σβ σ' : Mc} →
             {id : id-cont-type κ'} →
             {v  : value[ var ] (τ₂ ⇒[ τ₁ ⇒ σα ⇒ α ]⇒ σβ ⇒ β)} →
             {w  : value[ var ] τ₂} →
             {k  : cont[ var , • κ' id ] (τ₁ ⇒ σα ⇒ α)} →
             {m₁ : mcont[ var , D (K κ) , σ' ] σβ} →
             {c  : cont[ var , Δ ] κ} →
             {m₂ : mcont[ var , D Δ , σ' ] σβ} →
             CSubstM m₁ c m₂ →
             CSubst (App tt v w k m₁) c (App tt v w k m₂)

  data CSubstC {var : Ty → Set} : {Δ : Delta} {κ κ' : CTy} →
               cont[ var , K κ ] κ' →
               cont[ var , Δ ] κ →
               cont[ var , Δ ] κ' → Set where
    sKVar= : {Δ : Delta} {κ : CTy} →
             {c : cont[ var , Δ ] κ} →
             CSubstC KVar c c
    sKLet₂  : {τ α : Ty} → {Δ : Delta} → {κ : CTy} → {σα : 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} {κ : CTy} {σ σβ : Mc} →
               mcont[ var , D (K κ) , σ ] σβ →
               cont[ var , Δ ] κ →
               mcont[ var , D Δ , σ ] σβ → Set where
    sGCons₁ : {Δ : Delta} → {κ κ' : CTy} → {σ σ' : Mc} →
              {k₁ : cont[ var , K κ ] κ'} →
              {m  : mcont[ var , G , σ' ] σ} →
              {c  : cont[ var , Δ ] κ} →
              {k₂ : cont[ var , Δ ] κ'} →
              CSubstC k₁ c k₂ →
              CSubstM (GCons tt k₁ m) c (GCons tt k₂ m)
    sGCons₂ : {Δ : Delta} → {κ κ' κ'' : CTy} → {σ σ' : Mc} →
              {id : id-cont-type κ'} →
              {k  : cont[ var , • κ' id ] κ''} →
              {m₁ : mcont[ var , D (K κ) , σ' ] σ} →
              {c  : cont[ var , Δ ] κ} →
              {m₂ : mcont[ var , D Δ , σ' ] σ} →
              CSubstM m₁ c m₂ →
              CSubstM (GCons tt k m₁) c (GCons tt k m₂)
              
  data CSubstCM {var : Ty → Set} : {Δ Δ₁ Δ₂ : Delta} {Θ₁ Θ₂ : Theta} →
                {κ κ' : CTy} {σ σβ : Mc} →
                (ΔΘK : Delta-Theta-K Δ₁ Θ₁ Δ Δ₂ Θ₂) →
                cont[ var , Δ₁ ] κ' →
                mcont[ var , Θ₁ , σ ] σβ →
                cont[ var , Δ ] κ →
                cont[ var , Δ₂ ] κ' → 
                mcont[ var , Θ₂ , σ ] σβ → Set where
     sKG :  {Δ : Delta} → {κ κ' : CTy} → {σ σ' : Mc} →
            {k₁ : cont[ var , K κ ] κ'} →
            {m  : mcont[ var , G , σ' ] σ} →
            {c  : cont[ var , Δ ] κ} →
            {k₂ : cont[ var , Δ ] κ'} →
            CSubstC k₁ c k₂ →
            CSubstCM (refl , refl) k₁ m c k₂ m
     s•DK : {Δ : Delta} → {κ κ' κ'' : CTy} → {σ σ' : Mc} →
            {id : id-cont-type κ'} →
            {k  : cont[ var , • κ' id ] κ''} →
            {m₁ : mcont[ var , D (K κ) , σ' ] σ} →
            {c  : cont[ var , Δ ] κ} →
            {m₂ : mcont[ var , D Δ , σ' ] σ} →
            CSubstM m₁ c m₂ →
            CSubstCM (refl , refl) k m₁ c k 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 Δ Θ') →
             {k  : cont[ var , Δ ] (τ ⇒ σβ ⇒ β)} →
             {v  : value[ var ] τ} →
             {m₁ : mcont[ var , Θ' , σ' ] σβ} →
             {g  : mcont[ var , Θ , σ ] σ'} →
             {m₂ : mcont[ var , Θ' +++ Θ , σ ] σβ} →
             MSubstM m₁ g refl m₂ →
             MSubst (Val ΔΘ' k v m₁) g refl --(++-assoc Δ Θ' Θ)
                    (Val ΔΘ k v m₂)
    sApp   : {τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ Θ' : Theta}
             {σ σ' σα σβ : Mc} →
             (ΔΘ : Delta-Theta Δ (Θ' +++ Θ)) →
             (ΔΘ' : Delta-Theta Δ Θ') →
             (v  : value[ var ] (τ₂ ⇒[ τ₁ ⇒ σα ⇒ α ]⇒ σβ ⇒ β)) →
             (w  : value[ var ] τ₂) →
             (k  : cont[ var , Δ ] (τ₁ ⇒ σα ⇒ α)) →
             (m₁ : mcont[ var , Θ' , σ' ] σβ) →
             {g  : mcont[ var , Θ , σ ] σ'} →
             {m₂ : mcont[ var , Θ' +++ Θ , σ ] σβ} →
             MSubstM m₁ g refl m₂ →
             MSubst (App ΔΘ' v w k m₁) g refl --(++-assoc Δ Θ' Θ)
                    (App ΔΘ v w k m₂)

  data MSubstM {var : Ty → Set} : {Θ Θ' Θ'+Θ : Theta} {σ σ' σβ : Mc} →
               mcont[ var , Θ' , σ' ] σβ →
               mcont[ var , Θ , σ ] σ' →
               Θ'+Θ ≡ Θ' +++ Θ →
               mcont[ var , Θ'+Θ , σ ] σβ → Set where
    mGVar= : {Θ : Theta} {σ σ' : Mc} →
             {g : mcont[ var , Θ , σ ] σ'} →
             MSubstM GVar g refl g
    mGCons : {Δ : Delta} {Θ Θ' : Theta} {κ : CTy} {σ σ' σβ : Mc} →
             (ΔΘ' : Delta-Theta Δ (Θ +++ Θ')) →
             (ΔΘ : Delta-Theta Δ Θ) →
             {k  : cont[ var , Δ ] κ} →
             {m₁ : mcont[ var , Θ , σ ] σβ} →
             {g  : mcont[ var , Θ' , σ' ] σ} →
             {m₂ : mcont[ var , Θ +++ Θ' , σ' ] σβ} →
             MSubstM m₁ g refl m₂ →
             MSubstM (GCons ΔΘ k m₁) g refl -- (sym (D-++-assoc Δ Θ' Θ))
                     (GCons ΔΘ' k 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 ] τ₂} →
              {k : cont[ var , Δ ] (τ₁ ⇒ σα ⇒ α)} →
              {m : mcont[ var , Θ , σ ] σβ} →
              {e₁′ : term[ var , K (τ₁ ⇒ σα ⇒ α) , σβ ]⇒ β} →
              {e₁′′ : term[ var , Δ , σβ ]⇒ β} →
              {e₂ : term[ var , Δ ++ Θ , σ ]⇒ β} →
              Subst e₁ v e₁′ →
              CSubst e₁′ k e₁′′ →
              MSubst e₁′′ m refl e₂ →
              Reduce (App ΔΘ (Fun (λ x → e₁ x)) v k 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 ]
                   (τ ⇒ (τ₁ ⇒ σ₁ ⇒ τ₂) ∷ σ₂ ⇒ α)} →
              {k : cont[ var , Δ ] (τ₀ ⇒ σ₀ ⇒ τ₀')} →
              {m : mcont[ var , Θ , σ ] σ₀'} →
              Reduce (App tt Shift0 w j (GCons ΔΘ k m))
                     (App ΔΘ w (Fun (λ y → Val tt j (Var y)
                                                     (GCons tt KVar GVar)))
                          k m)
    -- KId V (K :: G) -> K V G
    RReset  : {τ α : Ty} → {Δ : Delta} → {Θ : Theta} → {σ σ' : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {v : value[ var ] τ} →
              {k : cont[ var , Δ ] (τ ⇒ σ ⇒ α)} →
              {m  : mcont[ var , Θ , σ' ] σ} →
              Reduce (Val tt (KId (refl , refl , refl)) v (GCons ΔΘ k m))
                     (Val ΔΘ k v m)

    -- congruence rules
    RVal₁   : {τ α : Ty} → {Δ : Delta} → {Θ : Theta} → {σ σ' : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {k k' : cont[ var , Δ ] (τ ⇒ σ ⇒ α)} →
              {v : value[ var ] τ} →
              {m : mcont[ var , Θ , σ' ] σ} →
              ReduceC k k' →
              Reduce (Val ΔΘ k v m)
                     (Val ΔΘ k' v m)
    RVal₂   : {τ α : Ty} → {Δ : Delta} → {Θ : Theta} → {σ σ' : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {k : cont[ var , Δ ] (τ ⇒ σ ⇒ α)} →
              {v v' : value[ var ] τ} →
              {m : mcont[ var , Θ , σ' ] σ} →
              ReduceV v v' →
              Reduce (Val ΔΘ k v m)
                     (Val ΔΘ k v' m)
    RVal₃   : {τ α : Ty} → {Δ : Delta} → {Θ : Theta} → {σ σ' : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {k : cont[ var , Δ ] (τ ⇒ σ ⇒ α)} →
              {v : value[ var ] τ} →
              {m m' : mcont[ var , Θ , σ' ] σ} →
              ReduceM m m' →
              Reduce (Val ΔΘ k v m)
                     (Val ΔΘ k v m')
    RApp₁   : {τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ : Theta} {σ σα σβ : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {v v' : value[ var ] (τ₂ ⇒[ τ₁ ⇒ σα ⇒ α ]⇒ σβ ⇒ β)} →
              {w : value[ var ] τ₂} →
              {k : cont[ var , Δ ] (τ₁ ⇒ σα ⇒ α)} →
              {m : mcont[ var , Θ , σ ] σβ} →
              ReduceV v v' →
              Reduce
                     (App ΔΘ v w k m)
                     (App ΔΘ v' w k m)
    RApp₂   : {τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ : Theta} {σ σα σβ : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {v : value[ var ] (τ₂ ⇒[ τ₁ ⇒ σα ⇒ α ]⇒ σβ ⇒ β)} →
              {w w' : value[ var ] τ₂} →
              {k : cont[ var , Δ ] (τ₁ ⇒ σα ⇒ α)} →
              {m : mcont[ var , Θ , σ ] σβ} →
              ReduceV w w' →
              Reduce (App ΔΘ v w k m)
                     (App ΔΘ v w' k m)
    RApp₃   : {τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ : Theta} {σ σα σβ : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {v : value[ var ] (τ₂ ⇒[ τ₁ ⇒ σα ⇒ α ]⇒ σβ ⇒ β)} →
              {w : value[ var ] τ₂} →
              {k k' : cont[ var , Δ ] (τ₁ ⇒ σα ⇒ α)} →
              {m : mcont[ var , Θ , σ ] σβ} →
              ReduceC k k' →
              Reduce
                     (App ΔΘ v w k m)
                     (App ΔΘ v w k' m)
    RApp₄   : {τ₁ τ₂ α β : Ty} {Δ : Delta} {Θ : Theta} {σ σα σβ : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {v : value[ var ] (τ₂ ⇒[ τ₁ ⇒ σα ⇒ α ]⇒ σβ ⇒ β)} →
              {w : value[ var ] τ₂} →
              {k : cont[ var , Δ ] (τ₁ ⇒ σα ⇒ α)} →
              {m m' : mcont[ var , Θ , σ ] σβ} →
              ReduceM m m' →
              Reduce (App ΔΘ v w k m)
                     (App ΔΘ v w k 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} → {κ : CTy} →
               cont[ var , Δ ] κ →
               cont[ var , Δ ] κ → Set where
    -- (λx.λg.K x g) -> K
    REtaLet : {τ α : Ty} → {Δ : Delta} → {σα : Mc} →
              {k : cont[ var , Δ ] (τ ⇒ σα ⇒ α)} →
              ReduceC (KLet (λ x → Val tt k (Var x) GVar)) k

    -- 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} → {κ : CTy} →
              {k : cont[ var , Δ ] κ} →
              ReduceC k k
    RTrans  : {Δ : Delta} → {κ : CTy} →
              {k₁ k₂ k₃ : cont[ var , Δ ] κ} →
              ReduceC k₁ k₂ →
              ReduceC k₂ k₃ →
              ReduceC k₁ k₃

  data ReduceM {var : Ty → Set} : {Θ : Theta} → {σ σ' : Mc} →
               mcont[ var , Θ , σ ] σ' →
               mcont[ var , Θ , σ ] σ' → Set where
    -- congruence rule
    RGCons₁ : {Δ : Delta} → {Θ : Theta} → {Δ' : CTy} → {σ σ' : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {k k' : cont[ var , Δ ] Δ'} →
              {m : mcont[ var , Θ , σ ] σ'} →
              ReduceC k k' →
              ReduceM (GCons ΔΘ k m) (GCons ΔΘ k' m)
    RGCons₂ : {Δ : Delta} → {Θ : Theta} → {Δ' : CTy} → {σ σ' : Mc} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {k : cont[ var , Δ ] Δ'} →
              {m m' : mcont[ var , Θ , σ ] σ'} →
              ReduceM m m' →
              ReduceM (GCons ΔΘ k m) (GCons ΔΘ k m')
              
  data ReduceCM {var : Ty → Set} : {Δ : Delta} → {Θ : Theta} → 
                {κ : CTy} → {σ σ' : Mc} →
                cont[ var , Δ ] κ →
                mcont[ var , Θ , σ ] σ' →
                cont[ var , Δ ] κ →
                mcont[ var , Θ , σ ] σ' → Set where
     RedC : {Δ : Delta} → {Θ : Theta} → {Δ' : CTy} → {σ σ' : Mc} →
            {k k' : cont[ var , Δ ] Δ'} →
            {m : mcont[ var , Θ , σ ] σ'} →
            ReduceC k k' →
            ReduceCM k m k' m
     RedM : {Δ : Delta} → {Θ : Theta} → {Δ' : CTy} → {σ σ' : Mc} →
            {k : cont[ var , Δ ] Δ'} →
            {m m' : mcont[ var , Θ , σ ] σ'} →
            ReduceM m m' →
            ReduceCM k m k 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 ΔΘ k v m) =
    sVal ΔΘ (SubstC≠ k) (SubstV≠ v) (SubstM≠ m)
  Subst≠ (App ΔΘ v w k m) =
    sApp ΔΘ (SubstV≠ v) (SubstV≠ w) (SubstC≠ k) (SubstM≠ m)

  SubstC≠ : {var : Ty → Set} {τ : Ty} {Δ : Delta} {κ : CTy} →
            (k₁ : cont[ var , Δ ] κ) →
            {v : value[ var ] τ} →
            SubstC (λ _ → k₁) v k₁
  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 ΔΘ k m) = sGCons ΔΘ (SubstC≠ k) (SubstM≠ m)