syndicate-lang
/
preserves
mirror of https://gitlab.com/preserves/preserves.git
1
0
Fork 1
Code Releases Activity

Correct encoding functions for trailers

This commit is contained in:
Tony Garnock-Jones 2023-11-01 15:42:25 +01:00
parent 85b3e513f9
commit d0619cb164
1 changed files with 5 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
preserves-expressions.md
View File

@ -100,7 +100,7 @@ We write ⌜*p*⌝ for the encoding into Preserves of a P-expression *p*.
| ⌜`,`⌝ | = | `<p |,|>` |
| ⌜`;`⌝ | = | `<p |;|>` |
| ⌜`:` ...⌝ | = | `<p |:` ...`|>` |
| ⌜*t*⌝ | = | ⌜*a*⌝ ... `<a>` | where *a* ... are the annotations in *t* and *t* ∈ **Trailer** |
| ⌜*t*⌝ | = | `@`⌜*a*⌝ ... `<a>` | where `@`*a* ... are the annotations in *t* and *t* ∈ **Trailer** |
The record `<a>` acts as an anchor for the annotations in a `Trailer`.
@ -108,8 +108,10 @@ We overload the ⌜·⌝ notation for encoding whole `Document`s into
sequences of Preserves values.
{:.pseudocode.equations}
| ⌜·⌝ : **P-expression Document** | ⟶ | **Preserves Sequence** |
| ⌜*p* ...⌝ | = | `[`⌜*p*⌝ ...`]` |
| ⌜·⌝ : **P-expression Document** | ⟶ | **Preserves Sequence** |
| ⌜*p* ...⌝ | = | `[`⌜*p*⌝ ...`]` |
| ⌜*p* ... `@`*a* ...⌝ | = | `[`⌜*p*⌝ ... `@`⌜*a*⌝ ... `<a>]` |
| | | where `@`*a* ... are trailing annotations |
## <a id="reading-preserves"></a>Interpreting P-expressions as Preserves