Delete do-old

src/Project/Do-old.agda

@@ -1,64 +0,0 @@
--- {-# OPTIONS --allow-unsolved-metas #-}
-
-module Project.Do where
-
-open import Project.Definitions using (Letk; Kont; Env; Exp; Value; State; Type; kont; halt; letk; clo; zero; suc; mkState; `_; `ℕ; _·_; _⇒_; _,_; _[_∶_])
-open import Project.Util using (_$_)
-
-data StepResult (A : Type) : Set where
-  part : State A → StepResult A
-  done : Value A → StepResult A
-
--- Apply the continuation to the value, resulting in a state.
-do-kont : ∀ {Tv Tω} (L : Letk Tv Tω) → Value Tv → State Tω
-do-kont {Tv} {Tω} (letk {Tc} Γ C E k) v =
-  let Γ′ = Γ , Tv in
-  let E′ = E [ Tv ∶ v ] in
-  mkState Tc Γ′ C E′ k
-
-apply-kont : ∀ {Tv Tω} → Letk Tv Tω → Value Tv → StepResult Tω
-apply-kont {Tv} (letk {Tc} Γ C E K) v =
-  part $ mkState Tc (Γ , Tv) C (E [ Tv ∶ v ]) K
-
-chain-kont : ∀ {A B C} → Letk A B → Letk B C → Letk A C
-chain-kont (letk Γ C E halt) b = letk Γ C E $ kont b
-chain-kont (letk Γ C E (kont k)) b = letk Γ C E $ kont $ chain-kont k b
-
-apply-proc-clo-kont : ∀ {Γ A B Tω} → Exp (Γ , A) B → Env Γ → Value A → Letk B Tω → StepResult Tω
-apply-proc-clo-kont {Γ} {A} {B} body e arg k =
-  let Γ′ = Γ , A in
-  let E′ = e [ A ∶ arg ] in
-  part $ mkState B Γ′ body E′ (kont k)
-
-apply-proc-clo-halt : ∀ {Γ A Tω} → Exp (Γ , A) Tω → Env Γ → Value A → StepResult Tω
-apply-proc-clo-halt {Γ} {A} {B} body e arg =
-  let Γ′ = Γ , A in
-  let E′ = e [ A ∶ arg ] in
-  part $ mkState B Γ′ body E′ halt
-
--- apply-proc-with-kont : ∀ {A B Tω} → Value (A ⇒ B) → Value A → Letk B Tω → StepResult Tω
--- apply-proc-with-kont (clo {Γ} {A} {B} body e) v k =
---   let Γ′ = Γ , A in
---   let E′ = e [ A ∶ v ] in
---   part $ mkState B Γ′ body E′ (kont k)
--- apply-proc-with-kont halt b k = part $ do-kont k b
--- apply-proc-with-kont {A} {B} {Tω} (kont (kont x)) a k = 
---   let k′ = chain-kont x k in
---   part $ do-kont k′ a
--- do-apply-kont (kont halt) b (letk Γ C E K) = {! done b  !}
--- do-apply-kont (kont (kont x)) b (letk Γ C E K) = {!   !}
-
--- do-apply-with-kont : ∀ {A B Tω} → Value (A ⇒ B) → Value A → Letk B Tω → StepResult Tω
--- do-apply-with-kont (clo body e) v k = apply-proc-clo-kont body e v k
--- do-apply-with-kont halt v k = done {!   !}
--- do-apply-with-kont (letk x) v k = apply-kont {!   !} {!   !}
--- 
--- -- This needs to be a separate function in order to unify B with Tω
--- do-apply-with-halt : ∀ {A Tω} → Value (A ⇒ Tω) → Value A → StepResult Tω
--- do-apply-with-halt {A} {Tω} (clo {Γ} body e) v = apply-proc-clo-halt body e v
---   let Γ′ = Γ , A in
---   let E′ = e [ A ∶ v ] in
---   part $ mkState Tω Γ′ body E′ halt
--- apply-proc-halt (halt halt) a = done (halt halt)
--- apply-proc-halt (halt (kont x)) a = part $ {! !}
--- apply-proc-halt (letk x) a = part $ do-kont x a -- part $ do-kont k a