From bd92c1cbb3a999e1ac2c97d8c6e93bbc8529b627 Mon Sep 17 00:00:00 2001
From: Matthew Dempsky <matthew@dempsky.org>
Date: Thu, 24 Sep 2020 11:43:41 -0700
Subject: [PATCH] Fix typos in operational semantics for "Loop" command

In section 13.3, the type of Loop is defined as:

    Loop : forall a, a -> (a -> cmd (outcome a)) -> cmd a

However, the operational semantics provided in sections 14.1 and 18.1
invoke the loop body function using "Again(i)" (type "outcome a").
They should instead use simply "i" (type "a").

Changing to "f(i)" also matches the StepLoop formalizations in
SeparationLogic.v and ConcurrentSeparationLogic.v, which invoke simply
"body init" (rather than "body (Again init)").
---
 frap_book.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/frap_book.tex b/frap_book.tex
index 08fbda7..7f9e04d 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -3703,7 +3703,7 @@ $$\infer{\smallstep{(h, x \leftarrow c_1; c_2(x))}{(h', x \leftarrow c'_1; c_2(x
 }
 \quad \infer{\smallstep{(h, x \leftarrow \mt{Return} \; v; c(x))}{(h, c(v))}}{}$$
 
-$$\infer{\smallstep{(h, \mt{Loop} \; i \; f)}{(h, x \leftarrow f(\mt{Again}(i)); \mt{match} \; x \; \mt{with} \; \mt{Done}(a) \Rightarrow \mt{Return} \; a \mid \mt{Again}(a) \Rightarrow \mt{Loop} \; a \; f)}}{}$$
+$$\infer{\smallstep{(h, \mt{Loop} \; i \; f)}{(h, x \leftarrow f(i); \mt{match} \; x \; \mt{with} \; \mt{Done}(a) \Rightarrow \mt{Return} \; a \mid \mt{Again}(a) \Rightarrow \mt{Loop} \; a \; f)}}{}$$
 
 $$\infer{\smallstep{(h, \mt{Read} \; a)}{(h, \mt{Return} \; v)}}{
   \msel{h}{a} = v
@@ -4753,7 +4753,7 @@ $$\infer{\smallstep{(h, l, x \leftarrow c_1; c_2(x))}{(h', l', x \leftarrow c'_1
 }
 \quad \infer{\smallstep{(h, l, x \leftarrow \mt{Return} \; v; c_2(x))}{(h, k, c_2(v))}}{}$$
 
-$$\infer{\smallstep{(h, l, \mt{Loop} \; i \; f)}{(h, l, x \leftarrow f(\mt{Again}(i)); \mt{match} \; x \; \mt{with} \; \mt{Done}(a) \Rightarrow \mt{Return} \; a \mid \mt{Again}(a) \Rightarrow \mt{Loop} \; a \; f)}}{}$$
+$$\infer{\smallstep{(h, l, \mt{Loop} \; i \; f)}{(h, l, x \leftarrow f(i); \mt{match} \; x \; \mt{with} \; \mt{Done}(a) \Rightarrow \mt{Return} \; a \mid \mt{Again}(a) \Rightarrow \mt{Loop} \; a \; f)}}{}$$
 
 $$\infer{\smallstep{(h, l, \mt{Read} \; a)}{(h, l, \mt{Return} \; v)}}{
   \msel{h}{a} = v