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

-- Terms
mutual
  data value[_] (var : Set) : Set where
    -- x
    Var    : (x : var) → value[ var ]
    -- n
    Num    : (n : ℕ) → value[ var ]
    -- n
    Bol    : (b : Bool) → value[ var ]
    -- λx.M
    Fun    : (f : var → term[ var ]) → value[ var ]
    -- S
    Shift  : value[ var ]
    -- S0
    Shift0 : value[ var ]

  data term[_] (var : Set) : Set where
    Val    : (v : value[ var ]) → term[ var ]
    NonVal : (p : nonvalue[ var ]) → term[ var ]

  data nonvalue[_] (var : Set) : Set where
    -- M N
    App   : (e₁ : term[ var ]) → (e₂ : term[ var ]) → nonvalue[ var ]
    -- <M>
    Reset : (e : term[ var ]) → nonvalue[ var ]
    -- let x = M in N
    Let   : (e₁ : term[ var ]) →        -- M
            (e₂ : var → term[ var ]) →  -- λx. N
            nonvalue[ var ]

-- examples
-- λx.x
val1 : {var : Set} → value[ var ]
val1 = Fun (λ x → Val (Var x))

-- λx.S(λk.k x)
val2 : {var : Set} → value[ var ]
val2 = Fun (λ x → NonVal (App (Val Shift)
           (Val (Fun (λ k → NonVal (App (Val (Var k)) (Val (Var x))))))))

-- λx.S(λk.x)
val3 : {var : Set} → value[ var ]
val3 = Fun (λ x → NonVal (App (Val Shift)
                                  (Val (Fun (λ k → Val (Var x))))))

-- λx.S0(λk.x)
val3' : {var : Set} → value[ var ]
val3' = Fun (λ x → NonVal (App (Val Shift0)
                                (Val (Fun (λ k → Val (Var x))))))

-- Interpreter cannot be implemented,
-- because untype terms may not terminate

-- Evaluation context (inside-out)
data pcontext[_] (var : Set): Set where
  -- []
  Hole : pcontext[ var ]
  -- K[[]@M]
  App₁ : (k : pcontext[ var ]) → (e : term[ var ]) → pcontext[ var ]
  -- K[V@[]]
  App₂  : (v : value[ var ]) → (k : pcontext[ var ]) → pcontext[ var ]
  -- K[Let x = [] in M]
  Let   : (k : pcontext[ var ]) →                -- K
          (f : var → term[ var ]) →   -- λx. M
          pcontext[ var ]
                                           
data context[_] (var : Set) : Set where
  -- []
  GHole : context[ var ]
  -- G[K[<[]>]]
  GReset : (c : pcontext[ var ]) → (m : context[ var ]) → context[ var ]

-- Plug
plug : {var : Set} → (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₂))

plugM : {var : Set} → (m : context[ var ]) → (e : term[ var ]) → term[ var ]
plugM GHole e = e
plugM (GReset c m) e = plugM m (plug c (NonVal (Reset e)))
  
-- Substitution relation M[x:=V]
mutual
  data SubstV {var : Set} :
              (var → value[ var ]) → value[ var ] → value[ var ] → Set where
    -- (λx.x)[v] → v
    sVar=  : {v : value[ var ]} →
             SubstV (λ x → Var x) v v
    -- (λ_.x)[v] → x
    sVar≠  : {v : value[ var ]} {x : var} →
             SubstV (λ _ → Var x) v (Var x)
    -- (λ_.n)[v] → n
    sNum   : {v : value[ var ]} {n : ℕ} →
             SubstV (λ _ → Num n) v (Num n)
    -- (λ_.b)[v] → b
    sBol   : {v : value[ var ]} {b : Bool} →
             SubstV (λ _ → Bol b) v (Bol b)
    -- (λy.λx.ey)[v] → λx.e′
    sFun   : {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 : {v : value[ var ]} →
             SubstV (λ _ → Shift) v Shift
    -- (λ_.S0)[v] → S0
    sShift0 : {v : value[ var ]} →
              SubstV (λ _ → Shift0) v Shift0

  data Subst {var : Set} :
             (var → term[ var ]) → value[ var ] → term[ var ] → Set where
    sVal   : {v₁ : var → value[ var ]} →
             {v : value[ var ]} →
             {v₁′ : value[ var ]} →
             SubstV v₁ v v₁′ →
             Subst (λ y → Val (v₁ y)) v (Val v₁′)
    sNonVal : {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 : Set} :
             (var → nonvalue[ var ]) → value[ var ] →
             nonvalue[ var ] → Set where
    sApp   : {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 : {e₁ : var → term[ var ]} →
             {v : value[ var ]} →
             {e₁′ : term[ var ]} →
             Subst e₁ v e₁′ →
             SubstNV (λ y → Reset (e₁ y)) v (Reset e₁′)
    sLet   : {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₂′)

data SubstC {var : Set} :
            (var → pcontext[ var ]) →
            value[ var ] →
            pcontext[ var ] → Set where
    sHole : {v : value[ var ]} →
            SubstC (λ x → Hole) v Hole
    sApp₁ : {k₁ : var → pcontext[ var ]} →
            {e₁ : var → term[ var ]} →
            {v  : value[ var ]} →
            {k₂ : pcontext[ var ]} →
            {e₂ : term[ var ]} →
            Subst e₁ v e₂ →
            SubstC k₁ v k₂ →
            SubstC (λ x → (App₁ (k₁ x) (e₁ x))) v (App₁ k₂ e₂)
    sApp₂ : {v₁ : var → value[ var ]} →
            {k₁ : var → pcontext[ var ]} →
            {v  : value[ var ]} →
            {v₂ : value[ var ]} →
            {k₂ : pcontext[ var ]} →
            SubstV v₁ v v₂ →
            SubstC k₁ v k₂ →
            SubstC (λ x → (App₂ (v₁ x) (k₁ x))) v (App₂ v₂ k₂)
    sLet  : {k₁ : var → pcontext[ var ]} →             
            {f₁ : var → (var → term[ var ])} →
            {v  : value[ var ]} →
            {k₂ : pcontext[ var ]} →             
            {f₂ : var → term[ var ]} →
            SubstC k₁ v k₂ →
            ((x : var) → Subst (λ y → f₁ y x) v (f₂ x)) →
            SubstC (λ x → (Let (k₁ x) (f₁ x) )) v (Let k₂ f₂)

data SubstM {var : Set} :
            (var → context[ var ]) → value[ var ] → context[ var ] → Set where
  sGHole  : {v : value[ var ]} →
            SubstM (λ x → GHole) v GHole
  sGReset : {c₁ : var → pcontext[ var ]} →
            {m₁ : var → context[ var ]} →
            {v  : value[ var ]} →
            {c₂ : pcontext[ var ]} → 
            {m₂ : context[ var ]} →
            SubstC c₁ v c₂ →
            SubstM m₁ v m₂ →
            SubstM (λ x → (GReset (c₁ x) (m₁ x))) v (GReset c₂ m₂)

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

  Subst≠ : {var : Set} →
           (e : term[ var ]) →
           {v : value[ var ]} →
           Subst (λ _ → e) v e
  Subst≠ (Val v) = sVal (SubstV≠ v)
  Subst≠ (NonVal p) = sNonVal (SubstNV≠ p)

  SubstNV≠ : {var : Set} →
             (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 e) = sReset (Subst≠ e)
  SubstNV≠ (Let e₁ e₂) = sLet (λ x → Subst≠ (e₂ x)) (Subst≠ e₁)

-- reduction rules
data Reduce {var : Set} : term[ var ] → term[ var ] → Set where
  -- (λx.M)V -> M[x:=V]
  RBetaV : (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  : (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 :
           (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 :
           (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 : (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  : (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  : {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 : (v : value[ var ]) →
           (j : pcontext[ var ]) →
           Reduce (NonVal (Reset (plug j (NonVal (App (Val Shift)
                                                          (Val v))))))
                  (NonVal (Reset (NonVal (App (Val v)
                    (Val (Fun (λ y →
                      NonVal (Reset (plug j (Val (Var y)))))))))))
  -- <J[S0@V]> -> V@(λy.<J[y]>)
  RShift0 : (v : value[ var ]) →
           (j : pcontext[ var ]) →
           Reduce (NonVal (Reset (plug j (NonVal (App (Val Shift0)
                                                         (Val v))))))
                  (NonVal (App (Val v)
                    (Val (Fun (λ y →
                      NonVal (Reset (plug j (Val (Var y)))))))))
  -- <V> -> V
  RReset : (v₁ : value[ var ]) →
           Reduce (NonVal (Reset (Val v₁)))
                  (Val v₁)

  -- congruence rules
  RFun   : {e e′ : var → term[ var ]} →
           ((x : var) → Reduce (e x) (e′ x)) →
           Reduce (Val (Fun e)) (Val (Fun e′))
  RApp₁  : {e₁ e₁′ : term[ var ]} →
           {e₂ : term[ var ]} →
           Reduce e₁ e₁′ →
           Reduce (NonVal (App e₁ e₂)) (NonVal (App e₁′ e₂))
  RApp₂  : {v₁ : value[ var ]} →
           {e₂ e₂′ : term[ var ]} →
           Reduce e₂ e₂′ →
           Reduce (NonVal (App (Val v₁) e₂)) (NonVal (App (Val v₁) e₂′))
  RLet₁  : {e₁ e₁′ : term[ var ]} →
           {e₂ : (var → term[ var ])} →
           Reduce e₁ e₁′ →
           Reduce (NonVal (Let e₁ e₂)) (NonVal (Let e₁′ e₂))
  RLet₂  : {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₁ : {e e′ : term[ var ]} →
           Reduce e e′ →
           Reduce (NonVal (Reset e))
                  (NonVal (Reset e′))
  -- closure rules
  RId    : {e : term[ var ]} →
           Reduce e e
  RTrans : {e₁ e₂ e₃ : term[ var ]} →
           Reduce e₁ e₂ →
           Reduce e₂ e₃ →
           Reduce e₁ e₃

-- equational reasoning
module Reasoning where

  infix  3 _∎
  infixr 2 _⟶⟨_⟩_ _≡⟨_⟩_
  infix  1 begin_

  begin_ : {var : Set} → {e₁ e₂ : term[ var ]} →
           Reduce e₁ e₂ → Reduce e₁ e₂
  begin_ red = red

  _⟶⟨_⟩_ : {var : Set} → (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} →
           (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} →
       (e : term[ var ]) → Reduce e e
  _∎ e = RId

-- lemma

-- v does not reduce to nonval e
reduceVal : {var : Set} → {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₁

-- e -> e' => K[e] -> K[e']
reducePlug : {var : Set} (k : pcontext[ var ]) → {e e' : term[ var ]} →
             Reduce e e' → Reduce (plug k e) (plug k e')
reducePlug Hole red = red
reducePlug (App₁ k e) red = reducePlug k (RApp₁ red)
reducePlug (App₂ v k) red = reducePlug k (RApp₂ red)
reducePlug (Let k f) red = reducePlug k (RLet₁ red)

-- (K[e])[v] = K[v][e[v]]
substPlug : {var : Set}
            {k : var → pcontext[ var ]} →
            {k′ : pcontext[ var ]} →
            {v : value[ var ]} →
            {e : var → term[ var ]} →
            {e′ : term[ var ]} →
            SubstC k v k′ →
            Subst (λ x → e x) v e′ →
            Subst (λ x → plug (k x) (e x)) v (plug k′ e′)
substPlug sHole sub = sub
substPlug (sApp₁ sub₁ sub-c) sub = substPlug sub-c (sNonVal (sApp sub sub₁))
substPlug (sApp₂ sub-v sub-c) sub = substPlug sub-c (sNonVal (sApp (sVal sub-v) sub))
substPlug (sLet sub-c sub₁) sub = substPlug sub-c (sNonVal (sLet (λ x → sub₁ x) sub))

-- e -> e' => G[e] -> G[e']
reducePlugM : {var : Set}
              (m : context[ var ]) →
              {e e' : term[ var ]} →
              Reduce e e' →
              Reduce (plugM m e) (plugM m e')
reducePlugM GHole red = red
reducePlugM (GReset c m) red = reducePlugM m (reducePlug c (RReset₁ red))

-- (G[e])[v] = G[v][e[v]]
substPlugM : {var : Set}
             {m₁ : var → context[ var ]} →
             {e₁ : var → term[ var ]} →
             {v  : value[ var ]} →
             {m₂ : context[ var ]} →
             {e₂ : term[ var ]} →
             SubstM m₁ v m₂ →
             Subst (λ x → e₁ x) v e₂ →
             Subst (λ x → plugM (m₁ x) (e₁ x)) v (plugM m₂ e₂)
substPlugM sGHole sub = sub
substPlugM (sGReset sub-c sub-m) sub =
  substPlugM sub-m (substPlug sub-c (sNonVal (sReset sub)))

-- Example

-- term1: (λx.1)@2 = 1
term1 : Reduce {var = ℕ}
          (NonVal (App (Val (Fun (λ x → Val (Num 1)))) (Val (Num 2))))
          (Val (Num 1))
term1 = begin
  NonVal (App (Val (Fun (λ x → Val (Num 1)))) (Val (Num 2)))
  ⟶⟨ RBetaV (λ x → Val (Num 1)) (Num 2) (Val (Num 1)) (sVal sNum) ⟩
  Val (Num 1)
  ∎
  where open Reasoning

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