IT WORKS

src/Project/Cesk.agda

@@ -13,14 +13,14 @@ open Aexp
 open Value
 open State
 
-astep : ∀ {Γ A} → Aexp Γ A → Env Γ → Value A
+astep : ∀ {Tω Γ A} → Aexp Tω Γ A → Env Tω Γ → Value Tω A
 astep (value v) _ = v
 astep zero _  = zero
 astep (suc c) e = suc $ astep c e
 astep (` id) e = lookup e id
 astep (ƛ body) e = clo body e
 
-inject : {A : Type} → Exp ∅ A → State A
+inject : {A : Type} → Exp A ∅ A → State A
 inject {A} C = mkState A ∅ C ∅ halt
 
 step : ∀ {Tω : Type} → State Tω → StepResult Tω
@@ -36,15 +36,15 @@ step (mkState Tc Γ (x₁ ∘ x₂) E K) with astep x₁ E
 -- abort (x₁ ∘ x₂) : A
 -- apply-kont (letk (abort `zero)) 2
 -- get back to doing (3 + )
-... | cont {Tω} {A} k =
+... | cont k =
   let val = astep x₂ E in
-  let K′ = kont $ letk Γ (abort (` zero)) E k in
-  apply-kont {! K′  !} val
+  let K′ = kont $ letk Γ (atomic $ ` 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 =
   let Γ′ = Γc , K[ A ⇒ ⊥ ] in
-  let E′ = env [ K[ A ⇒ ⊥ ] ∶ cont {Tω = Tω} K ] in
-  part $ mkState Tc Γ′ body E′ K
+  let E′ = env [ K[ A ⇒ ⊥ ] ∶ cont K ] in
+  part $ mkState Tω Γ′ body E′ halt
 step (mkState Tc Γ (abort V⊥) E K) with astep V⊥ E
 ... | ()
 step (mkState Tc Γ (`let {A} C₁ C₂) E K) =
@@ -61,11 +61,11 @@ eval′ (suc n) s with step s
 ... | part x = eval′ n x
 ... | done x = complete $ done x
 
-eval : ∀ {A} → ℕ → Exp ∅ A → EvalResult
+eval : ∀ {A} → ℕ → Exp A ∅ 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
+expRes+ : expRes ≡ (complete $ done $ (suc (suc (suc zero))))
+expRes+ = refl

src/Project/Definitions.agda

@@ -21,80 +21,83 @@ data Context : Set where
   ∅ : Context
   _,_ : Context → Type → Context
 
-data Value : Type → Set
+data Value (Tω : Type) : Type → Set
 
-data Env : Context → Set where
-  ∅ : Env ∅
-  _[_∶_] : ∀ {Γ} → Env Γ → (A : Type) → Value A → Env (Γ , A)
+data Env (Tω : Type) : Context → Set where
+  ∅ : Env Tω ∅
+  _[_∶_] : ∀ {Γ} → Env Tω Γ → (A : Type) → Value Tω A → Env Tω (Γ , A)
 
 data _∋_ : Context → Type → Set where
   zero : ∀ {Γ A} → Γ , A ∋ A
   suc : ∀ {Γ A B} → Γ ∋ A → Γ , B ∋ A
 
-lookup : ∀ {Γ A} → Env Γ → Γ ∋ A → Value A
+lookup : ∀ {Tω Γ A} → Env Tω Γ → Γ ∋ A → Value Tω A
 lookup ∅ ()
 lookup (env [ A ∶ x ]) zero = x
 lookup (env [ A ∶ x ]) (suc id) = lookup env id
 
-data Aexp Context : Type → Set
-data Exp Context : Type → Set
+data Aexp (Tω : Type) Context : Type → Set
+data Exp (Tω : Type) Context : Type → Set
 
-data Aexp Γ where
-  value : ∀ {A} → Value A → Aexp Γ A
+data Aexp Tω Γ where
+  value : ∀ {A} → Value Tω A → Aexp Tω Γ A
 
   -- Natural numbers
-  zero : Aexp Γ `ℕ
-  suc : Aexp Γ `ℕ → Aexp Γ `ℕ
+  zero : Aexp Tω Γ `ℕ
+  suc : Aexp Tω Γ `ℕ → Aexp Tω Γ `ℕ
 
   -- Functions
-  `_ : ∀ {A} → Γ ∋ A → Aexp Γ A
-  ƛ : ∀ {B} {A : Type} → Exp (Γ , A) B → Aexp Γ (A ⇒ B)
+  `_ : ∀ {A} → Γ ∋ A → Aexp Tω Γ A
+  ƛ : ∀ {B} {A : Type} → Exp Tω (Γ , A) B → Aexp Tω Γ (A ⇒ B)
 
-data Exp Γ where
-  abort : ∀ {A} → Aexp Γ ⊥ → Exp Γ A
+data Exp Tω Γ where
+  abort : ∀ {A} → Aexp Tω Γ ⊥ → Exp Tω Γ A
 
   -- Atomic expressions
-  atomic : ∀ {A} → Aexp Γ A → Exp Γ A
+  atomic : ∀ {A} → Aexp Tω Γ A → Exp Tω Γ A
 
   -- Natural numbers
-  case : ∀ {A} → Aexp Γ `ℕ → Exp Γ A → Aexp Γ (`ℕ ⇒ A) → Exp Γ A
+  case : ∀ {A} → Aexp Tω Γ `ℕ → Exp Tω Γ A → Aexp Tω Γ (`ℕ ⇒ A) → Exp Tω Γ A
 
   -- Functions
-  _·_ : ∀ {A B} → Aexp Γ (A ⇒ B) → Aexp Γ A → Exp Γ B
-  _∘_ : ∀ {A B} → Aexp Γ K[ A ⇒ B ] → Aexp Γ A → Exp Γ B
+  _·_ : ∀ {A B} → Aexp Tω Γ (A ⇒ B) → Aexp Tω Γ A → Exp Tω Γ B
+  _∘_ : ∀ {A} → Aexp Tω Γ K[ A ⇒ ⊥ ] → Aexp Tω Γ A → Exp Tω Γ ⊥
 
   -- Call/cc
-  call/cc : ∀ {A Tω} → Aexp Γ (K[ A ⇒ ⊥ ] ⇒ Tω) → Exp Γ Tω
+  call/cc : ∀ {A} → Aexp Tω Γ (K[ A ⇒ ⊥ ] ⇒ Tω) → Exp Tω Γ A
 
   -- Let
-  `let : ∀ {A B : Type} → Exp Γ A → Exp (Γ , A) B → Exp Γ B
+  `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 (s = call/cc ƛk . let (k' = abort k) (k' · 2)) (suc s)
+-- exp = let (call/cc ƛ . let (`0 · 2) (abort `0)) ((\. suc `0) · `0)
 -- exp = 3
-exp : Exp ∅ `ℕ
-exp =
-  `let
-    (call/cc (ƛ (` zero ∘ suc (suc zero))))
-    (`let
-      (abort (` zero))
-      ((ƛ (atomic (suc (` suc zero)))) · ` zero))
+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
 
-data Value where
+data Value Tω where
   -- Natural numbers
-  zero : Value `ℕ
-  suc : Value `ℕ → Value `ℕ
+  zero : Value Tω `ℕ
+  suc : Value Tω `ℕ → Value Tω `ℕ
 
   -- Functions
-  clo : ∀ {Γ} {A B : Type} → Exp (Γ , A) B → Env Γ → Value (A ⇒ B)
+  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 : ∀ {Tω A B} → Kont Tω A → Value K[ B ⇒ ⊥ ]
+  cont : ∀ {A} → Kont Tω A → Value Tω K[ A ⇒ ⊥ ]
 
 record Letk Tω Tv where
   inductive
@@ -102,8 +105,8 @@ record Letk Tω Tv where
   field
     {Tc} : Type
     Γ : Context
-    C : Exp (Γ , Tv) Tc
-    E : Env Γ
+    C : Exp Tω (Γ , Tv) Tc
+    E : Env Tω Γ
     K : Kont Tω Tc
 
 data Kont Tω where
@@ -117,6 +120,6 @@ record State (Tω : Type) : Set where
   field
     Tc : Type
     Γ : Context
-    C : Exp Γ Tc
-    E : Env Γ
+    C : Exp Tω Γ Tc
+    E : Env Tω Γ
     K : Kont Tω Tc

src/Project/Do.agda

@@ -7,14 +7,14 @@ open import Project.Util
 
 data StepResult (A : Type) : Set where
   part : State A → StepResult A
-  done : Value A → StepResult A
+  done : Value A A → StepResult A
 
-apply-kont : ∀ {Tv Tω} → Kont Tω Tv → Value Tv → StepResult Tω
+apply-kont : ∀ {Tv Tω} → Kont Tω Tv → Value Tω Tv → StepResult Tω
 apply-kont {Tv} (kont (letk {Tc} Γ C E K)) v =
   part $ mkState Tc (Γ , Tv) C (E [ Tv ∶ v ]) K
 apply-kont halt v = done v
 
-apply-proc-clo : ∀ {Γ A B Tω} → Exp (Γ , A) B → Env Γ → Value A → Kont Tω B → StepResult Tω
+apply-proc-clo : ∀ {Γ A B Tω} → Exp Tω (Γ , A) B → Env Tω Γ → Value Tω A → Kont Tω B → StepResult Tω
 apply-proc-clo {Γ} {A} {B} body env arg k =
   let Γ′ = Γ , A in
   let E′ = env [ A ∶ arg ] in