{-# 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

data Delta : Set where
  K : Delta
  • : Delta

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

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

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

•-Theta : (Θ : Theta) → Delta-Theta • Θ
•-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 : (Δ : Delta) → (Θ' Θ : Theta) →
              ++-assoc • (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
ΔΘ≡ {Δ = •} {D Δ} tt tt = refl

-- CPS terms
mutual
  data value[_] (var : Set) : Set where
    -- x
    Var    : (x : var) → value[ var ]
    -- n
    Num    : (n : ℕ) → value[ var ]
    -- b
    Bol    : (b : Bool) → value[ var ]
    -- λx.λk.λg.M
    Fun    : (e : var → term[ var , K ]) → value[ var ]
    -- S
    Shift  : value[ var ]
    -- S0
    Shift0 : value[ var ]

  data term[_,_] (var : Set) : Delta → Set where
    -- K V G
    Val    : {Δ : Delta} → {Θ : Theta} →
             Delta-Theta Δ Θ →
             (k : cont[ var , Δ ]) →
             (v : value[ var ]) →
             (g : mcont[ var , Θ ]) →
             term[ var , Δ ++ Θ ]
    -- V W K G
    App    : {Δ : Delta} {Θ : Theta} →
             Delta-Theta Δ Θ →
             (v : value[ var ]) →
             (w : value[ var ]) →
             (k : cont[ var , Δ ]) →
             (g : mcont[ var , Θ ]) →
             term[ var , Δ ++ Θ ]

  data cont[_,_] (var : Set) : Delta → Set where
    -- k
    KVar   : cont[ var , K ]
    -- kid
    KId    : cont[ var , • ]
    -- λx.λg.M
    KLet   : {Δ : Delta} →
             (e : var → term[ var , Δ ]) →
             cont[ var , Δ ]

  data mcont[_,_] (var : Set) : Theta → Set where
    -- g
    GVar   : mcont[ var , G ]
    -- K::G
    GCons  : {Δ : Delta} → {Θ : Theta} →
             Delta-Theta Δ Θ →
             (k : cont[ var , Δ ]) →
             (g : mcont[ var , Θ ]) →
             mcont[ var , D (Δ ++ Θ) ]

-- example
-- λx.λk.k x
val1 : {var : Set} → value[ var ]
val1 = Fun (λ x → Val tt KVar (Var x) GVar)

-- 値による代入規則
mutual
  data SubstV {var : Set} :
              (var → value[ var ]) → value[ var ] → value[ var ] → Set where
    sVar=   : {v : value[ var ]} →
              SubstV (λ x → Var x) v v
    sVar≠   : {v : value[ var ]} {x : var} →
              SubstV (λ _ → Var x) v (Var x)
    sNum    : {v : value[ var ]} {n : ℕ} →
              SubstV (λ _ → Num n) v (Num n)
    sBol    : {v : value[ var ]} {b : Bool} →
              SubstV (λ _ → Bol b) v (Bol b)
    sFun    : {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  : {v : value[ var ]} →
              SubstV (λ _ → Shift) v Shift
    sShift0 : {v : value[ var ]} →
              SubstV (λ _ → Shift0) v Shift0

  data Subst {var : Set} : {Δ : Delta} →
             (var → term[ var , Δ ]) →
             value[ var ] →
             term[ var , Δ ] → Set where
    sVal   : {Δ : Delta} → {Θ : Theta} →
             (ΔΘ : 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   : {Δ : Delta} {Θ : Theta} →
             (ΔΘ : 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 : Set} : {Δ : Delta} →
              (var → cont[ var , Δ ]) →
              value[ var ] →
              cont[ var , Δ ] → Set where
    sKVar≠ : {v : value[ var ]} →
             SubstC (λ _ → KVar) v KVar
    sKId   : {v : value[ var ]} →
             SubstC (λ _ → KId) v KId
    sKLet  : {Δ : Delta} →
             {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 : Set} : {Θ : Theta} →
              (var → mcont[ var , Θ ]) →
              value[ var ] →
              mcont[ var , Θ ] → Set where
    sGVar≠ : {v : value[ var ]} →
             SubstM (λ _ → GVar) v GVar
    sGCons : {Δ : Delta} {Θ : Theta} →
             (ΔΘ : 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 : Set} : {Δ : Delta} →
              term[ var , K ] →
              cont[ var , Δ ] →
              term[ var , Δ ] → Set where
    sVal₁  : {Δ : Delta} →
             {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₂  : {Δ : Delta} →
             {k  : cont[ var , • ]} →
             {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₁  : {Δ : Delta} →
             {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₂  : {Δ : Delta}
             {v  : value[ var ]} →
             {w  : value[ var ]} →
             {k  : cont[ var , • ]} →
             {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 : Set} : {Δ : Delta} →
               cont[ var , K ] →
               cont[ var , Δ ] →
               cont[ var , Δ ] → Set where
    sKVar= : {Δ : Delta} →
             {c : cont[ var , Δ ]} →
             CSubstC KVar c c
    sKLet₂  : {Δ : Delta} →
             {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 : Set} : {Δ : Delta} →
               mcont[ var , D K ] →
               cont[ var , Δ ] →
               mcont[ var , D Δ ] → Set where
    sGCons₁ : {Δ : Delta} →
              {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} →
              {k  : cont[ var , • ]} →
              {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 : Set} : {Δ Δ₁ Δ₂ : Delta} {Θ₁ Θ₂ : Theta} →
                (ΔΘK : Delta-Theta-K Δ₁ Θ₁ Δ Δ₂ Θ₂) →
                cont[ var , Δ₁ ] →
                mcont[ var , Θ₁ ] →
                cont[ var , Δ ] →
                cont[ var , Δ₂ ] → 
                mcont[ var , Θ₂ ] → Set where
     sKG :  {Δ : Delta} →
            {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} →
            {k  : cont[ var , • ]} →
            {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 : Set} :
              {Δ Δ' : Delta} {Θ : Theta} →
              term[ var , Δ ] →
              mcont[ var , Θ ] →
              Δ' ≡ Δ ++ Θ →
              term[ var , Δ' ] → Set where
    sVal   : {Δ : Delta} {Θ Θ' : Theta} →
             (ΔΘ : 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   : {Δ : Delta} {Θ Θ' : Theta}
             (ΔΘ : 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 : Set} : {Θ Θ' Θ'+Θ : Theta} →
               mcont[ var , Θ' ] →
               mcont[ var , Θ ] →
               Θ'+Θ ≡ Θ' +++ Θ →
               mcont[ var , Θ'+Θ ] → Set where
    mGVar= : {Θ : Theta} →
             {g : mcont[ var , Θ ]} →
             MSubstM GVar g refl g
    mGCons : {Δ : Delta} {Θ Θ' : Theta} →
             (ΔΘ' : 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 : Set} : {Δ : Delta} →
              term[ var , Δ ] →
              term[ var , Δ ] → Set where
    -- (λx.λk.λg.M) V K G -> M[x:=V][k:=K][g:=G]
    RBetaV  : {Δ : Delta} {Θ : Theta} →
              (ΔΘ : 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 : {Δ : Delta} {Θ : Theta} →
              (ΔΘ : 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  : {Δ : Delta}
              {w : value[ var ]} →
              {j : cont[ var , • ]} →
              {m : mcont[ var , D Δ ]} →
              Reduce (App (•-Theta (D Δ)) Shift w j m)
                     (App (•-Theta (D Δ))
                          w (Fun (λ y → Val tt j (Var y) (GCons tt KVar GVar)))
                          KId m)
    -- S0 W J (K :: G) -> W (λy.λk.λg.J y (k :: g)) K G
    RShift0 : {Δ : Delta} {Θ : Theta}
              (ΔΘ : Delta-Theta Δ Θ) →
              {w : value[ var ]} →
              {j : cont[ var , • ]} →
              {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  : {Δ : Delta} → {Θ : Theta} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {v : value[ var ]} →
              {k : cont[ var , Δ ]} →
              {m  : mcont[ var , Θ ]} →
              Reduce (Val tt KId v (GCons ΔΘ k m))
                     (Val ΔΘ k v m)

    -- congruence rules
    RVal₁   : {Δ : Delta} → {Θ : Theta} →
              (ΔΘ : 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₂   : {Δ : Delta} → {Θ : Theta} →
              (ΔΘ : 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₃   : {Δ : Delta} → {Θ : Theta} →
              (ΔΘ : 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₁   : {Δ : Delta} {Θ : Theta} →
              (ΔΘ : 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₂   : {Δ : Delta} {Θ : Theta} →
              (ΔΘ : 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₃   : {Δ : Delta} {Θ : Theta} →
              (ΔΘ : 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₄   : {Δ : Delta} {Θ : Theta} →
              (ΔΘ : 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     : {Δ : Delta} →
              {e : term[ var , Δ ]} →
              Reduce e e
    RTrans  : {Δ : Delta} →
              {e₁ e₂ e₃ : term[ var , Δ ]} →
              Reduce e₁ e₂ →
              Reduce e₂ e₃ →
              Reduce e₁ e₃

  data ReduceV {var : Set} : value[ var ] → value[ var ] → Set where
    -- λx.λk.λg.V x k g -> V
    REtaV   : {v : value[ var ]} →
              ReduceV (Fun (λ x → App tt v (Var x) KVar GVar)) v

    -- congruence rule
    RFun    : {e e' : var → term[ var , K ]} →
              ((x : var) → Reduce (e x) (e' x)) →
              ReduceV (Fun e) (Fun e')
    -- closure rules
    RId     : {v : value[ var ]} →
              ReduceV v v
    RTrans  : {v₁ v₂ v₃ : value[ var ]} →
              ReduceV v₁ v₂ →
              ReduceV v₂ v₃ →
              ReduceV v₁ v₃

  data ReduceC {var : Set} : {Δ : Delta} →
               cont[ var , Δ ] →
               cont[ var , Δ ] → Set where
    -- (λx.λg.K x g) -> K
    REtaLet : {Δ : Delta} →
              {k : cont[ var , Δ ]} →
              ReduceC (KLet (λ x → Val tt k (Var x) GVar)) k

    -- congruence rule
    RKLet   : {Δ : Delta} →
              {e e' : var → term[ var , Δ ]} →
              ((x : var) → Reduce (e x) (e' x)) →
              ReduceC (KLet e) (KLet e')

    -- closure rules
    RId     : {Δ : Delta} →
              {k : cont[ var , Δ ]} →
              ReduceC k k
    RTrans  : {Δ : Delta} →
              {k₁ k₂ k₃ : cont[ var , Δ ]} →
              ReduceC k₁ k₂ →
              ReduceC k₂ k₃ →
              ReduceC k₁ k₃

  data ReduceM {var : Set} : {Θ : Theta} →
               mcont[ var , Θ ] →
               mcont[ var , Θ ] → Set where
    -- congruence rule
    RGCons₁ : {Δ : Delta} → {Θ : Theta} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {k k' : cont[ var , Δ ]} →
              {m : mcont[ var , Θ ]} →
              ReduceC k k' →
              ReduceM (GCons ΔΘ k m) (GCons ΔΘ k' m)
    RGCons₂ : {Δ : Delta} → {Θ : Theta} →
              (ΔΘ : Delta-Theta Δ Θ) →
              {k : cont[ var , Δ ]} →
              {m m' : mcont[ var , Θ ]} →
              ReduceM m m' →
              ReduceM (GCons ΔΘ k m) (GCons ΔΘ k m')
              
  data ReduceCM {var : Set} : {Δ : Delta} → {Θ : Theta} → 
                cont[ var , Δ ] →
                mcont[ var , Θ ] →
                cont[ var , Δ ] →
                mcont[ var , Θ ] → Set where
     RedC : {Δ : Delta} → {Θ : Theta} →
            {k k' : cont[ var , Δ ]} →
            {m : mcont[ var , Θ ]} →
            ReduceC k k' →
            ReduceCM k m k' m
     RedM : {Δ : Delta} → {Θ : Theta} →
            {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 : Set} {Δ : Delta} →
           {e₁ e₂ : term[ var , Δ ]} →
           Reduce e₁ e₂ → Reduce e₁ e₂
  begin_ red = red

  _⟶⟨_⟩_ : {var : Set} {Δ : Delta} →
            (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 : Set} {Δ : Delta} →
           (e₁ {e₂ e₃} : term[ var , Δ ]) →
           e₁ ≡ e₂ → Reduce e₂ e₃ →
           Reduce e₁ e₃
  _≡⟨_⟩_ e₁ {e₂} {e₃} refl e₂-red-e₃ = e₂-red-e₃

  _∎ : {var : Set} {Δ : Delta} →
       (e : term[ var , Δ ]) → Reduce e e
  _∎ e = RId

-- lemma
mutual
  SubstV≠ : {var : Set} →
            (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 = sShift
  SubstV≠ Shift0 = sShift0

  Subst≠ : {var : Set} {Δ : Delta} →
           (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 : Set} {Δ : Delta} →
            (k₁ : cont[ var , Δ ]) →
            {v : value[ var ]} →
            SubstC (λ _ → k₁) v k₁
  SubstC≠ KVar = sKVar≠
  SubstC≠ KId = sKId
  SubstC≠ (KLet e) = sKLet (λ x → Subst≠ (e x))

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