From 5eea0b88ead2e67a505085b7d39465efd5906279 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Wed, 8 Dec 2021 12:35:31 -0600
Subject: [PATCH] Kont

---
 Makefile                     |  9 +++++----
 src/Project/Cesk.agda        | 26 +++++++++++++-------------
 src/Project/Definitions.agda |  8 ++++----
 src/Project/Do.agda          | 18 +++++++++++++++---
 src/Project/notes.txt        | 22 ++++++++++++++++++++--
 5 files changed, 57 insertions(+), 26 deletions(-)

diff --git a/Makefile b/Makefile
index 104a5e1..dbf612a 100644
--- a/Makefile
+++ b/Makefile
@@ -1,16 +1,17 @@
 SOURCE_MODULES := $(shell find src/Project -name "*.agda" -exec basename {} \;)
 GENERATED_TEX := $(patsubst %.agda, gentex/Project/%.tex, $(SOURCE_MODULES))
 
+main.pdf: main.tex agda.sty
+	tectonic --keep-logs main.tex
+
 gentex/Project/%.tex: src/Project/%.agda
 	agda --latex-dir=gentex --latex $<
 
 agda.sty: $(GENERATED_TEX)
+	rm -f agda.sty
 	cp gentex/agda.sty agda.sty
 
-main.pdf: main.tex agda.sty
-	tectonic --keep-logs main.tex
-
 watch:
-	watchexec -e tex -- make main.pdf
+	watchexec -e agda,tex -- make main.pdf
 
 .PHONY: watch
diff --git a/src/Project/Cesk.agda b/src/Project/Cesk.agda
index a7b79b2..d0d9e16 100644
--- a/src/Project/Cesk.agda
+++ b/src/Project/Cesk.agda
@@ -3,9 +3,9 @@
 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; `ℕ; _,_; _k⇒_; _⇒_; _∋_; _·_; _∘_; _[_∶_]; ∅)
+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.Util using (_$_)
-open import Project.Do using (StepResult; part; done; do-kont; do-apply)
+open import Project.Do using (StepResult; part; done; do-kont; do-apply-kont; do-apply-halt)
 
 open Aexp
 open Value
@@ -25,16 +25,16 @@ 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 K) =
+step (mkState Tc Γ (C₁ · C₂) E halt) =
   let C₁′ = astep C₁ E in
   let C₂′ = astep C₂ E in
-  do-apply C₁′ C₂′ K
-step (mkState Tc Γ (atomic x) E K) with K
-... | halt = done $ astep x E
-... | kont l = part $ do-kont l $ astep x E
-step (mkState Tc Γ (call/cc C) E K) =
-  part $ mkState (({!   !} ⇒ {!   !}) k⇒ {!   !}) Γ {!  !} {!   !} {!   !}
-
--- 3 + (call/cc k . k 2 + k 4)
--- (k . k 2 + k 4) (\x . 3 + x)
--- ((\x . 3 + x) 2 + (\x . 3 + x) 4)
\ No newline at end of file
+  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 .((_ ⇒ _) ⇒ _) Γ (call/cc C) E K) =
+  let C′ = C · {!   !} in
+  {!   !}
diff --git a/src/Project/Definitions.agda b/src/Project/Definitions.agda
index 9a1cca4..6d02800 100644
--- a/src/Project/Definitions.agda
+++ b/src/Project/Definitions.agda
@@ -12,7 +12,7 @@ infixr 7 _⇒_
 
 data Type : Set where
   _⇒_ : Type → Type → Type
-  _k⇒_ : Type → Type → Type
+  -- _k⇒_ : Type → Type → Type
   `ℕ : Type
 
 data Context : Set where
@@ -55,10 +55,10 @@ data Exp Γ where
 
   -- Functions
   _·_ : ∀ {A B} → Aexp Γ (A ⇒ B) → Aexp Γ A → Exp Γ B
-  _∘_ : ∀ {A B} → Aexp Γ (A k⇒ B) → Exp Γ B
+  -- _∘_ : ∀ {A B} → Aexp Γ (A k⇒ B) → Exp Γ B
 
   -- Call/cc
-  call/cc : ∀ {Tω A B} → Exp Γ (A ⇒ B) → Exp Γ Tω
+  call/cc : ∀ {Ki Ko R} → Aexp (Γ , Ki) ((Ki ⇒ Ko) ⇒ R) → Exp Γ ((Ki ⇒ Ko) ⇒ R)
 
 data Kont (Tω : Type) : Type → Set
 
@@ -71,7 +71,7 @@ data Value where
   clo : ∀ {Γ} {A B : Type} → Exp (Γ , A) B → Env Γ → Value (A ⇒ B)
 
   -- Call/CC
-  kont : ∀ {Tω Ti Tc} → Kont Tω Tc → Value (Ti k⇒ Tc)
+  kont : ∀ {Tω Ki Ko} → Kont Tω (Ki ⇒ Ko) → Value ((Ki ⇒ Ko) ⇒ Tω)
 
 record Letk (Tv Tω : Type) : Set
 
diff --git a/src/Project/Do.agda b/src/Project/Do.agda
index f0d0ee0..157ce38 100644
--- a/src/Project/Do.agda
+++ b/src/Project/Do.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module Project.Do where
 
 open import Project.Definitions using (Letk; Kont; Exp; Value; State; Type; kont; halt; letk; clo; zero; suc; mkState; `_; `ℕ; _·_; _⇒_; _,_; _[_∶_])
@@ -14,8 +16,18 @@ do-kont {Tv} {Tω} (letk {Tc} Γ C E k) v =
   let E′ = E [ Tv ∶ v ] in
   mkState Tc Γ′ C E′ k
 
-do-apply : ∀ {A B Tω} → Value (A ⇒ B) → Value A → Kont Tω B → StepResult Tω
-do-apply (clo {Γ} {A} {B} body e) v k =
+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 =
   let Γ′ = Γ , A in
   let E′ = e [ A ∶ v ] in
-  part $ mkState B Γ′ body E′ k
\ No newline at end of file
+  part $ mkState B Γ′ body E′ (kont k)
+do-apply-kont (kont x) b k = part $ do-kont 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) b = done b
+do-apply-halt (kont (kont x)) b = part $ do-kont x b
\ No newline at end of file
diff --git a/src/Project/notes.txt b/src/Project/notes.txt
index 59df81d..cf31184 100644
--- a/src/Project/notes.txt
+++ b/src/Project/notes.txt
@@ -11,7 +11,25 @@ State {
 State {
   Tc = ?
   Ctx = nil
-  C = x * 2
+  C = 
   E  = [x = call/cc k . suc k]
   K = halt
-}
\ No newline at end of file
+}
+
+State {
+  Tc = ?
+  Ctx = 
+}
+
+---
+
+k : String -> N
+left part : (String -> N) -> Bool
+entire thing : (kont String -> N) -> Bool
+
+
+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)
\ No newline at end of file