i hate call/cc

2021-12-09 02:05:20 -06:00 · 2021-12-09 02:05:20 -06:00 · 953bb21dc8
parent 69ecaeb7b8
commit 953bb21dc8
5 changed files with 161 additions and 67 deletions
--- a/src/Project/Cesk.agda
+++ b/src/Project/Cesk.agda
@ -3,15 +3,16 @@
 module Project.Cesk where

 open import Data.Product renaming (_,_ to ⦅_,_⦆)
-open import Project.Definitions using (Aexp; Exp; Env; State; Letk; Kont; Value; Type; atomic; kont; letk; lookup; call/cc; case; mkState; halt; `ℕ; _,_; _⇒_; _∋_; _·_; _[_∶_]; ∅)
+open import Project.Definitions
 open import Project.Util using (_$_)
-open import Project.Do using (StepResult; part; done; do-kont; do-apply-kont; do-apply-halt)
+open import Project.Do

 open Aexp
 open Value
 open State

 astep : ∀ {Γ A} → Aexp Γ A → Env Γ → Value A
+astep (value v) _ = v
 astep zero _  = zero
 astep (suc c) e = suc $ astep c e
 astep (` id) e = lookup e id
@ -21,26 +22,51 @@ inject : {A : Type} → Exp ∅ A → State A
 inject {A} C = mkState A ∅ C ∅ halt

 step : ∀ {Tω : Type} → State Tω → StepResult Tω
-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
-  do-apply-halt C₁′ C₂′
-step (mkState Tc Γ (C₁ · C₂) E (kont k)) =
-  let C₁′ = astep C₁ E in
-  let C₂′ = astep C₂ E in
-  do-apply-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 Γ (atomic x) E K) = apply-kont K $ astep x E
+step (mkState Tc Γ (case C isZ isS) E K) with astep C E
+... | zero = part $ mkState Tc Γ isZ E K
+... | 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 = done $ {!  !}
+... | cont (kont k) = {! apply-kont (kont k) ? !}
+-- ... | clo body env = apply-proc-clo body env (astep x₂ E) K
+step (mkState Tc Γ (call/cc x) E K) with astep x E
+... | proc = {!   !}
+--... | 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

-step (mkState Tc Γ (call/cc C) E halt) =
-  let proc = astep C E in
-  let value = kont halt in
-  do-apply-halt {!   !} value
-step (mkState Tc Γ (call/cc C) E (kont k)) =
-  let proc = astep C E in
-  let value = kont (kont k) in
-  do-apply-kont {!   !} value k
+--   let proc = astep x E in
+--   let val = cont K in
+--   part $ apply-proc proc val K
+
+-- 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
--- a/src/Project/Definitions.agda
+++ b/src/Project/Definitions.agda
@ -11,8 +11,8 @@ infixl 6 _,_
 infixr 7 _⇒_

 data Type : Set where
+  ⊥ : Type
  _⇒_ : Type → Type → Type
-  _k⇒_ : Type → Type → Type
  `ℕ : Type

 data Context : Set where
@ -38,6 +38,8 @@ data Aexp Context : Type → Set
 data Exp Context : Type → Set

 data Aexp Γ where
+  value : ∀ {A} → Value A → Aexp Γ A
+
  -- Natural numbers
  zero : Aexp Γ `ℕ
  suc : Aexp Γ `ℕ → Aexp Γ `ℕ
@ -55,12 +57,12 @@ data Exp Γ where

  -- Functions
  _·_ : ∀ {A B} → Aexp Γ (A ⇒ B) → Aexp Γ A → Exp Γ B
-  -- _∘_ : ∀ {A B} → Aexp Γ (A k⇒ B) → Exp Γ B

  -- Call/cc
-  call/cc : ∀ {A B Tω} → Aexp Γ (A ⇒ Tω) → Exp Γ (A ⇒ B)
+  call/cc : ∀ {A B Tω} → Aexp Γ ((A ⇒ ⊥) ⇒ B) → Exp Γ Tω

 data Kont (Tω : Type) : Type → Set
+record Letk (Tv Tω : Type) : Set

 data Value where
  -- Natural numbers
@ -71,12 +73,9 @@ data Value where
  clo : ∀ {Γ} {A B : Type} → Exp (Γ , A) B → Env Γ → Value (A ⇒ B)

  -- Call/CC
-  -- kont : ∀ {Tω Ki Ko} → Kont Tω (Ki ⇒ Ko) → Value ((Ki ⇒ Ko) k⇒ Tω)
-  kont : ∀ {A Tω} → Kont Tω A → Value (A ⇒ Tω)
+  cont : ∀ {Tω A} → Kont Tω A → Value (A ⇒ ⊥)

-record Letk (Tv Tω : Type) : Set
-
-record Letk Tv Tω where
+record Letk Tω Tv where
  inductive
  constructor letk
  field
@ -88,7 +87,7 @@ record Letk Tv Tω where

 data Kont Tω where
  halt : Kont Tω Tω
-  kont : ∀ {Tc} → Letk Tc Tω → Kont Tω Tc
+  kont : ∀ {Tc} → Letk Tω Tc → Kont Tω Tc

 -- A is the type of C
 -- B is the eventual type
--- a/src/Project/Do-old.agda
+++ b/src/Project/Do-old.agda
@ -0,0 +1,64 @@
+-- {-# 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
--- a/src/Project/Do.agda
+++ b/src/Project/Do.agda
@ -2,45 +2,27 @@

 module Project.Do where

-open import Project.Definitions using (Letk; Kont; Exp; Value; State; Type; kont; halt; letk; clo; zero; suc; mkState; `_; `ℕ; _·_; _⇒_; _,_; _[_∶_])
-open import Project.Util using (_$_)
+open import Project.Definitions
+open import Project.Util

 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
-
-applykont : ∀ {Tv Tω} → Letk Tv Tω → Value Tv → StepResult Tω
-applykont {Tv} (letk {Tc} Γ C E K) v =
+apply-kont : ∀ {Tv Tω} → Kont Tω Tv → Value 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

-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
-
-do-apply-kont : ∀ {A B Tω} → Value (A ⇒ B) → Value A → Letk B Tω → StepResult Tω
-do-apply-kont (clo {Γ} {A} {B} body e) v k =
+apply-proc-clo : ∀ {Γ A B Tω} → Exp (Γ , A) B → Env Γ → Value A → Kont Tω B → StepResult Tω
+apply-proc-clo {Γ} {A} {B} body env arg k =
  let Γ′ = Γ , A in
-  let E′ = e [ A ∶ v ] in
-  part $ mkState B Γ′ body E′ (kont k)
-do-apply-kont (kont halt) a k = part $ do-kont k a
-do-apply-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) = {!   !}
+  let E′ = env [ A ∶ arg ] in
+  part $ mkState B Γ′ body E′ k

-- This needs to be a separate function in order to unify B with Tω
-do-apply-halt : ∀ {A Tω} → Value (A ⇒ Tω) → Value A → StepResult Tω
-do-apply-halt {A} {Tω} (clo {Γ} body e) v =
-  let Γ′ = Γ , A in
-  let E′ = e [ A ∶ v ] in
-  part $ mkState Tω Γ′ body E′ halt
-do-apply-halt (kont halt) a = done a
-do-apply-halt (kont (kont k)) a = part $ do-kont k a
+-- 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 {!   !} {!   !}
--- a/src/Project/notes.txt
+++ b/src/Project/notes.txt
@ -32,4 +32,27 @@ call/cc : ((String -> N) -> Bool)

 len (call/cc k . if k "hello" is even then true else false)
 (k . if k "hello" is even then true else false) (\x . len x)
-((\x . 3 + x) 2 + (\x . 3 + x) 4)
+((\x . 3 + x) 2 + (\x . 3 + x) 4)
+
+---
+
+3 + (call/cc \k . abort (k 2))
+
+abort : _|_ -> A
+k : Nat -> _|_
+k n = (yield 3 + n); exit
+k 2 : _|_
+abort (k 2) : A
+\k . abort (k 2) : (Nat -> _|_) -> A
+(call/cc \k . abort (k 2)) : Nat
+
+---
+
+cont (\n . 3 + n)
+
+--
+
+apply-kont (Kont String Nat) Nat
+
+--
+