This commit is contained in:
Tony Garnock-Jones 2023-11-01 13:27:26 +01:00
parent d7b983e140
commit e0736e03c5
1 changed files with 16 additions and 9 deletions

View File

@ -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`.