Clean up the code

src/Project/Cesk.agda

@@ -1,5 +1,3 @@
--- {-# OPTIONS --allow-incomplete-matches --allow-unsolved-metas #-}
-
 module Project.Cesk where
 
 open import Relation.Binary.PropositionalEquality
@@ -31,11 +29,6 @@ step (mkState Tc Γ (case C isZ isS) E K) with astep C E
 step (mkState Tc Γ (x₁ · x₂) E K) with astep x₁ E
 ... | clo body env = apply-proc-clo body env (astep x₂ E) K
 step (mkState Tc Γ (x₁ ∘ x₂) E K) with astep x₁ E
--- x₁ = k , x₂ = 2
--- x₁ ∘ x₂ : ⊥
--- abort (x₁ ∘ x₂) : A
--- apply-kont (letk (abort `zero)) 2
--- get back to doing (3 + )
 ... | cont k =
   let val = astep x₂ E in
   let K′ = kont $ letk Γ (atomic $ ` zero) E k in
@@ -64,8 +57,10 @@ eval′ (suc n) s with step s
 eval : ∀ {A} → ℕ → Exp A ∅ A → EvalResult
 eval n e = eval′ n (inject e)
 
-expRes : EvalResult
-expRes = eval 100 exp
+exp : Exp `ℕ ∅ `ℕ
+exp = 
+  `let (call/cc (ƛ (`let (` zero ∘ suc (suc zero)) (abort (` zero)))))
+  ((ƛ $ atomic $ suc $ ` zero) · ` zero)
 
-expRes+ : expRes ≡ (complete $ done $ (suc (suc (suc zero))))
+expRes+ : eval 7 exp ≡ (complete $ done $ (suc (suc (suc zero))))
 expRes+ = refl

src/Project/Definitions.agda

@@ -69,21 +69,6 @@ data Exp Tω Γ where
   -- Let
   `let : ∀ {A B : Type} → Exp Tω Γ A → Exp Tω (Γ , A) B → Exp Tω Γ B
 
-
--- exp = let (call/cc ƛ . let (abort `0) (`0 · 2)) ((\ . suc `0) · `0)
--- exp = let (call/cc ƛ . let (`0 · 2) (abort `0)) ((\. suc `0) · `0)
--- exp = 3
-exp : Exp `ℕ ∅ `ℕ
-exp = 
-  `let (call/cc (ƛ (`let (` zero ∘ suc (suc zero)) (abort (` zero)))))
-  ((ƛ $ atomic $ suc $ ` zero) · ` zero)
-
---   `let
---     (call/cc (ƛ (` zero ∘ suc (suc zero))))
---     (`let
---       (abort (` zero))
---       ((ƛ (atomic (suc (` suc zero)))) · ` zero))
-
 data Kont (Tω : Type) : Type → Set
 record Letk (Tv Tω : Type) : Set
 
@@ -96,7 +81,6 @@ data Value Tω where
   clo : ∀ {Γ} {A B : Type} → Exp Tω (Γ , A) B → Env Tω Γ → Value Tω (A ⇒ B)
 
   -- Call/CC
-  -- cont : ∀ {Tω A} → Kont Tω A → Value (A ⇒ ⊥)
   cont : ∀ {A} → Kont Tω A → Value Tω K[ A ⇒ ⊥ ]
 
 record Letk Tω Tv where
@@ -113,8 +97,6 @@ data Kont Tω where
   halt : Kont Tω Tω
   kont : ∀ {Tc} → Letk Tω Tc → Kont Tω Tc
 
--- A is the type of C
--- B is the eventual type
 record State (Tω : Type) : Set where
   constructor mkState
   field

src/Project/Do.agda

@@ -1,5 +1,3 @@
--- {-# OPTIONS --allow-unsolved-metas #-}
-
 module Project.Do where
 
 open import Project.Definitions
@@ -18,11 +16,4 @@ apply-proc-clo : ∀ {Γ A B Tω} → Exp Tω (Γ , A) B → Env Tω Γ → Valu
 apply-proc-clo {Γ} {A} {B} body env arg k =
   let Γ′ = Γ , A in
   let E′ = env [ A ∶ arg ] in
-  part $ mkState B Γ′ body E′ k
-
--- apply-proc : ∀ {A B Tω} → Value (A ⇒ B) → Value A → Kont Tω B → StepResult Tω
--- apply-proc {A} {B} (clo {Γ} x E) arg K =
---   let Γ′ = Γ , A in
---   let E′ = E [ A ∶ arg ] in
---   part $ mkState B Γ′ x E′ K
--- apply-proc (cont k) arg K = apply-kont {!   !} {!   !}
+  part $ mkState B Γ′ body E′ k