From 0a1c1775edd38608c1331f9d5499698256a2e93d Mon Sep 17 00:00:00 2001
From: daniel frumin <dan@groupoid.moe>
Date: Mon, 24 Jun 2024 10:59:24 +0200
Subject: [PATCH] tweaks

---
 theories/effects/delim.v               | 19 ++++++++++++++++++-
 theories/examples/delim_lang/logpred.v |  1 +
 theories/examples/delim_lang/logrel.v  |  1 +
 3 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/theories/effects/delim.v b/theories/effects/delim.v
index 5862e8e..5012d37 100644
--- a/theories/effects/delim.v
+++ b/theories/effects/delim.v
@@ -1,4 +1,21 @@
-(** * Representation of delimited continuations *)
+(** * Representation of delimited continuations
+
+This representation is inspired by the abstract machine semantics for
+the CPS hierarchy, and is designed with manipualtion of
+meta-continuations in mind.
+
+We consider shift/reset, appcont operations, as well as the explicit
+"pop" operation. The "state" for delimited continuations is a
+meta-continuation: a stack of continuations corresponding to different
+delimiters. Every time we do "reset" we push the current continuation
+onto the stack, thus making the contiuation outside "reset" not
+visible to the operations inside it. The "shift" operation behaves
+similarly to call/cc by capturing the current continuation (which was
+already delimited by reset). Finally, when we exit the scope of reset,
+we need to restore the previous continuation which was pushed onto the
+stack. For this, we explicitly use the "pop" operation.
+
+ *)
 From gitrees Require Import prelude gitree.
 From iris.algebra Require Import list.
 
diff --git a/theories/examples/delim_lang/logpred.v b/theories/examples/delim_lang/logpred.v
index f1ae73e..ba9301b 100644
--- a/theories/examples/delim_lang/logpred.v
+++ b/theories/examples/delim_lang/logpred.v
@@ -1,3 +1,4 @@
+(** Logical predicate for safety *)
 From gitrees Require Import gitree lang_generic hom.
 From gitrees.effects Require Import delim.
 From gitrees.examples.delim_lang Require Import lang interp typing hom.
diff --git a/theories/examples/delim_lang/logrel.v b/theories/examples/delim_lang/logrel.v
index 5d29269..324c419 100644
--- a/theories/examples/delim_lang/logrel.v
+++ b/theories/examples/delim_lang/logrel.v
@@ -1,3 +1,4 @@
+(** Logical relation for adequacy wrt the machine semantics *)
 From gitrees Require Import gitree lang_generic hom.
 From gitrees.effects Require Import delim.
 From gitrees.examples.delim_lang Require Import lang interp typing hom.