Before adding T\omega to value

src/Project/Cesk.agda

@@ -1,7 +1,9 @@
-{-# OPTIONS --allow-incomplete-matches --allow-unsolved-metas #-}
+-- {-# OPTIONS --allow-incomplete-matches --allow-unsolved-metas #-}
 
 module Project.Cesk where
 
+open import Relation.Binary.PropositionalEquality
+open import Data.Nat
 open import Data.Product renaming (_,_ to ⦅_,_⦆)
 open import Project.Definitions
 open import Project.Util using (_$_)
@@ -28,57 +30,42 @@ step (mkState Tc Γ (case C isZ isS) E K) with astep C E
 ... | suc n = part $ mkState Tc Γ (isS · value n) E K
 step (mkState Tc Γ (x₁ · x₂) E K) with astep x₁ E
 ... | clo body env = apply-proc-clo body env (astep x₂ E) K
-... | cont halt = {!   !}
-... | cont (kont x) = {!   !}
--- ... | cont k = apply-kont {! k  !} (astep x₂ E)
--- ... | clo body env = apply-proc-clo body env (astep x₂ E) K
-step (mkState Tc Γ (call/cc {A} aexp) E K) with astep aexp E
+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 {Tω} {A} k =
+  let val = astep x₂ E in
+  let K′ = kont $ letk Γ (abort (` zero)) E k in
+  apply-kont {! K′  !} val
+step {Tω} (mkState Tc Γ (call/cc {A} aexp) E K) with astep aexp E
 ... | clo {Γc} body env =
-  part $ mkState Tc (Γc , A ⇒ ⊥) body (env [ A ⇒ ⊥ ∶ cont K ]) K
-... | cont k = apply-kont K {!   !}
--- part $ mkState ((A ⇒ ⊥) ⇒ Tc) Γ aexp E K′
---  let Γ′ = Γ , A ⇒ ⊥ in
---  let E′ = E [ A ⇒ ⊥ ∶ cont {!   !} ] in
---  part $ mkState (((A ⇒ ⊥) ⇒ Tc)) Γ′ aexp E′ {!   !}
+  let Γ′ = Γc , K[ A ⇒ ⊥ ] in
+  let E′ = env [ K[ A ⇒ ⊥ ] ∶ cont {Tω = Tω} K ] in
+  part $ mkState Tc Γ′ body E′ K
 step (mkState Tc Γ (abort V⊥) E K) with astep V⊥ E
 ... | ()
 step (mkState Tc Γ (`let {A} C₁ C₂) E K) =
   let K′ = letk Γ C₂ E K in
   part $ mkState A Γ C₁ E (kont K′)
---... | clo {Γc} {A} {B} body env =
---  let T = Κ[ Tc ⇒ ⊥ ] in
---  let v = cont K in
---  part $ mkState Tc (Γc , T) {! body  !} (env [ T ∶ v ]) K
 
---   let proc = astep x E in
---   let val = cont K in
---   part $ apply-proc proc val K
+data EvalResult : Set where
+  complete : ∀ {A} → StepResult A → EvalResult
+  exhausted : ∀ {A} → State A → EvalResult
 
--- step (mkState Tc Γ (case c cz cs) E K) with ⦅ astep c E , astep cs E ⦆
--- ... | ⦅ zero , _ ⦆ = part $ mkState Tc Γ cz E K
--- ... | ⦅ suc n , clo {Γc} cc cloE ⦆ =
---         part $ mkState Tc (Γc , `ℕ) cc (cloE [ `ℕ ∶ n ]) K
--- step (mkState Tc Γ (C₁ · C₂) E halt) =
---   let C₁′ = astep C₁ E in
---   let C₂′ = astep C₂ E in
---   apply-proc-halt C₁′ C₂′
--- step {Tω} (mkState Tc Γ (C₁ · C₂) E (kont k)) =
---   let C₁′ = astep C₁ E in
---   let C₂′ = astep C₂ E in
---   apply-helper C₁′ C₂′
---     where
---       apply-helper : ∀ {T : Type} → Value (T ⇒ Tc) → Value T → StepResult Tω
---       apply-helper (clo c e) v = apply-proc-clo-kont c e v k
---       apply-helper (kont x) v = apply-kont k {! v  !}
---   -- apply-proc-with-kont C₁′ C₂′ k
--- step (mkState Tc Γ (atomic x) E halt) = done $ astep x E
--- step (mkState Tc Γ (atomic x) E (kont k)) = part $ do-kont k $ astep x E
--- 
--- -- step (mkState Tc Γ (call/cc C) E halt) =
--- --   let proc = astep C E in
--- --   let value = kont halt in
--- --   apply-proc-halt {!   !} value
--- -- step (mkState Tc Γ (call/cc C) E (kont k)) =
--- --   let proc = astep C E in
--- --   let value = kont (kont k) in
--- --   apply-proc-halt {!   !} value k
+eval′ : ∀ {A} → ℕ → State A → EvalResult
+eval′ 0 s = exhausted s
+eval′ (suc n) s with step s
+... | part x = eval′ n x
+... | done x = complete $ done x
+
+eval : ∀ {A} → ℕ → Exp ∅ A → EvalResult
+eval n e = eval′ n (inject e)
+
+expRes : EvalResult
+expRes = eval 100 exp
+
+-- expRes+ : expRes ≡ (complete $ done $ (suc (suc (suc zero))))
+-- expRes+ = refl

src/Project/Definitions.agda

@@ -7,6 +7,7 @@ open import Project.Util using (_$_)
 
 infix 4 _∋_
 infix 4 _·_
+infix 4 _∘_
 infixl 6 _,_
 infixr 7 _⇒_
 
@@ -14,6 +15,7 @@ data Type : Set where
   ⊥ : Type
   `ℕ : Type
   _⇒_ : Type → Type → Type
+  K[_⇒_] : Type → Type → Type
 
 data Context : Set where
   ∅ : Context
@@ -59,9 +61,10 @@ data Exp Γ where
 
   -- Functions
   _·_ : ∀ {A B} → Aexp Γ (A ⇒ B) → Aexp Γ A → Exp Γ B
+  _∘_ : ∀ {A B} → Aexp Γ K[ A ⇒ B ] → Aexp Γ A → Exp Γ B
 
   -- Call/cc
-  call/cc : ∀ {A Tω} → Aexp (Γ) ((A ⇒ ⊥) ⇒ Tω) → Exp Γ Tω
+  call/cc : ∀ {A Tω} → Aexp Γ (K[ A ⇒ ⊥ ] ⇒ Tω) → Exp Γ Tω
 
   -- Let
   `let : ∀ {A B : Type} → Exp Γ A → Exp (Γ , A) B → Exp Γ B
@@ -72,10 +75,11 @@ data Exp Γ where
 -- exp = 3
 exp : Exp ∅ `ℕ
 exp =
-  `let (call/cc (
-    -- `let (` zero · suc (suc zero)) (abort (` zero))
-    ƛ (` zero · suc (suc zero))
-  )) (`let (abort (` zero)) ((ƛ (atomic (suc (` 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
@@ -90,7 +94,7 @@ data Value where
 
   -- Call/CC
   -- cont : ∀ {Tω A} → Kont Tω A → Value (A ⇒ ⊥)
-  cont : ∀ {Tω A B} → Kont Tω A → Value (B ⇒ ⊥)
+  cont : ∀ {Tω A B} → Kont Tω A → Value K[ B ⇒ ⊥ ]
 
 record Letk Tω Tv where
   inductive