From e0736e03c531d2cd38686e950677641269b54896 Mon Sep 17 00:00:00 2001
From: Tony Garnock-Jones <tonyg@leastfixedpoint.com>
Date: Wed, 1 Nov 2023 13:27:26 +0100
Subject: [PATCH] Nuance

---
 preserves-expressions.md | 25 ++++++++++++++++---------
 1 file changed, 16 insertions(+), 9 deletions(-)

diff --git a/preserves-expressions.md b/preserves-expressions.md
index ffefe97..836c869 100644
--- a/preserves-expressions.md
+++ b/preserves-expressions.md
@@ -86,7 +86,7 @@ in these positions, but P-expressions allow them.
 
 ## <a id="encoding-pexprs"></a>Encoding P-expressions as Preserves
 
-We write ⌜*p*⌝ for the encoding into Preserves of P-expression *p*.
+We write ⌜*p*⌝ for the encoding into Preserves of a P-expression *p*.
 
 {:.pseudocode.equations}
 | ⌜·⌝ : **Expr**   | ⟶ | **Value** |
@@ -116,13 +116,10 @@ sequences of Preserves values.
 
 The [previous section](#encoding-pexprs) discussed ways of representing
 P-expressions using Preserves. Here, we discuss *interpreting*
-P-expressions *as* Preserves, so that (1) a Preserves datum (2) written
-using Preserves text syntax and then (3) read as a P-expression can be
-(4) interpreted from that P-expression to yield the original datum.
-
-A reader for P-expressions can be adapted to yield a reader for
-Preserves terms by processing (subterms of) each P-expression that the
-reader produces.
+P-expressions *as* Preserves so that (1) a Preserves datum (2) written
+using Preserves text syntax[^careful-use-of-commas] and then (3) read as
+a P-expression can be (4) interpreted from that P-expression to yield
+the original datum.
 
  1. Every `(`..`)` or `;` that appears is an error.
  2. Every `:`, `::`, `:::`, ... is an error, except in context of `Block`s as described below.
@@ -136,6 +133,12 @@ reader produces.
     `Block` with duplicate keys (under interpretation) is an error.
  7. Every `Set` containing any duplicate expressions (under interpretation) is an error.
 
+[^careful-use-of-commas]: Every Preserves datum can be read via a
+    P-expression reader and then interpreted successfully as Preserves
+    *if commas are omitted entirely in the text*. If commas are present,
+    however, they must not appear in certain positions, namely: either
+    before or after *p* in `@`*p* *q*; or before *p* in `#!`*p*.
+
 [^discard-trailers-instead-of-error]: **Implementation note.** When
     implementing parsing of P-expressions into Preserves, consider
     offering an optional mode where trailing annotations `Trailer` are
@@ -278,7 +281,7 @@ P-expression `Expr`s.
    [Ometa](https://en.wikipedia.org/wiki/OMeta), etc.) can be used to
    extract further syntactic structure.
 
-## Appendix: Equations for interpreting P-expressions as Preserves
+## <a id="reading-preserves-equationally"></a>Appendix: Equations for interpreting P-expressions as Preserves
 
 The partial function **uncomma**(*p*) removes all occurrences of `,`
 from a P-expression *p*.
@@ -294,6 +297,10 @@ from a P-expression *p*.
 | **uncomma**(`@`*p* *q*)     | = | `@`**uncomma**(*p*) **uncomma**(*q*) |                                       |
 | **uncomma**(*p*)            | = | *p*                                  | if *p* ∈ **Atom** ∪ **Punct** - {`,`} |
 
+{:.pseudocode.equations}
+| **uncomma** : **Document** | ⇀ | **Document**         |
+| **uncomma**(*p* ...)       | = | **uncomma**(*p*) ... |
+
 We write ⌞**uncomma**(*p*)⌟ for the partial function mapping a
 P-expression *p* ∈ `Expr` to a corresponding Preserves `Value`.