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

The last couple of weeks's work

This commit is contained in:
Tony Garnock-Jones 2020-06-29 14:16:44 +02:00
parent 8d3146cf30
commit e24012af11
4 changed files with 2155 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
Makefile
View File

@ -1,7 +1,17 @@
LITERATE_MD=unquoting.md
all: $(LITERATE_MD) preserves.pdf
preserves.pdf: preserves.md preserves.css
google-chrome --headless --disable-gpu --print-to-pdf=$@ \
http://localhost:4000/preserves/preserves.html
clean:
rm -f $(LITERATE_MD)
%.md: %.rkt
literate-lisp-to-markdown < $< > $@
test-all:
make -C tests
(cd implementations/javascript; npm test)

394
unquoting.md Normal file
View File

@ -0,0 +1,394 @@
---
title: (Un)quotation in layered pub/sub networks
---
<!--
```racket
#lang racket
(require rackunit)
(require racket/contract)
```
-->
Tony Garnock-Jones <tonyg@leastfixedpoint.com>
June 2020.
## Introduction
There's potential for confusion whenever *patterns* are drawn from
the same set that the *values to be matched* come from.
In layered pub/sub networks like
[Syndicate](https://syndicate-lang.org/), publisher-subscriber
relationships are set up using messages carried over the
publish-subscribe medium itself.
Subscribers build messages containing patterns describing other
messages they are interested in.
But in general, these messages travel across multiple layered
pub/sub dataspaces. To avoid confusion, we have to be very clear
about when a piece of data denotes a pattern and when it is just a
piece of data.
In this post, I'll describe the approach I want to take to solve
this problem for Syndicate in the general case.
### What's the problem?
Consider regular expressions. The regex `ab*c` matches `ac`,
`abc`, `abbc`, and so on; but what if we wanted to match the
literal string `ab*c`? We have to escape the star in the pattern,
writing the pattern as `ab\*c`.
#### Quotation
If we want to use a regex engine to search for a literal string
supplied by someone else---perhaps a user, perhaps an API
client---we have to take care to *quote* the literal string, in
order to avoid confusion caused by metacharacters:[^racket-regexp-quote]
| Literal string | Quoted form |
| --- | --- |
| `no metachars` | `no metachars` |
| `ab*c` | `ab\*c` |
| `...` | `\.\.\.` |
| `(hello \$\ [world])` | `\(hello \\\$\\ \[world\]\)` |
[^racket-regexp-quote]: Racket supplies
[`regexp-quote`](https://github.com/racket/racket/blob/5bb837661c12a9752c6a99f952c0e1b267645b33/racket/collects/racket/private/string.rkt#L38-L51)
([docs](https://docs.racket-lang.org/reference/regexp.html?q=reg%20quo#(def._((lib._racket%2Fprivate%2Fbase..rkt)._regexp-quote))))
for this purpose:
```racket
(check-equal? (regexp-quote "ab*c") "ab\\*c")
(check-equal? (regexp-quote "...") "\\.\\.\\.")
(check-equal? (regexp-quote "(hello \\$\\ [world])") "\\(hello \\\\\\$\\\\ \\[world\\]\\)")
```
#### Invariant
The invariant we want to rely on is
> every string, after quotation, becomes a regular expression that matches
> exactly and only the original string.[^racket-regexp-quotation-invariant]
[^racket-regexp-quotation-invariant]:
Expressing this in code is straightforward:
```racket
(define (regexp-quotation-invariant original-string some-other-string)
(equal? (string=? original-string some-other-string)
(regexp-match? (regexp-quote original-string) some-other-string)))
```
We could use Racket's [random data
generation](https://docs.racket-lang.org/data/Enumerations.html?q=data%2Fen#%28mod-path._data%2Fenumerate%29)
tools to perform randomized testing of this invariant.
Of course, this same problem crops up in any pattern language
where embedding of values in patterns makes sense, so let's
generalize accordingly:
> every value, after quotation, becomes a pattern that matches
> exactly and only the original value.
### Quotation of pub/sub patterns.
In [Syndicate](https://syndicate-lang.org/), we want patterns over
assertions (and thus over messages) to be able to match arbitrary
[Preserves](.) atoms, sequences, and records.
However, to date, there have been special exceptions. The special
records `capture/1` and `discard/0`, embedded in patterns, have
been interpreted as defining pattern variables and wildcards,
respectively. There has been no way to construct a pattern that
matches `capture/1` or `discard/0` records themselves.
Previously, I tried adding a `quote/1` record to the set of
special record types. Experimentation [demonstrated](quoting.rkt)
that patterns with `quote/1` were able to escape the limitations
of patterns without `quote/1`. Also, it's [a theorem](quoting.v)
that quoting is "sensible": that unquotation after quotation of a
pattern always equals the original pattern.
In this post, I'll explore an alternative I think might be better:
letting patterns match anything except a *single* special record,
`unquote/1`. Patterns use `unquote/1` to escape into a
*metalanguage* where special operators like capture, discard, and
so on can be discussed.
## Definitions
We'll work with a simplified data language. Instead of full
Preserves, which includes lists, maps, records, a variety of atoms
and so forth, we'll stick to just records and atoms.
`Value`s are the things our `Pattern`s are to match.
`Value`s that are `Lists` denote records: the first `Value` is the
label of the record, and the remaining `Value`s are its fields.
```racket
(define (record? x)
(and (list? x)
(positive? (length x))
(andmap value? x)))
(define (record-label x) (car x))
(define (record-fields x) (cdr x))
(define (record-arity x) (length (record-fields x)))
(define (record-field x n) (list-ref x (+ n 1)))
```
Atoms, then, are the non-`List` `Value`s.
```racket
(define (atom? x)
(or (string? x)
(symbol? x)
(number? x)))
```
`Value`s are the records and the atoms, and nothing else.
```racket
(define (value? x)
(or (atom? x)
(record? x)))
```
We will frequently need to decide whether a `Value` is a record
with a particular label and arity.
```racket
(define (record/class? x label arity)
(and (record? x)
(equal? (record-label x) label)
(= (record-arity x) arity)))
```
A `Pattern` is a `Value` with certain additional constraints on
the `Operation`s that appear within an `unquote/1` record.
```racket
(define (pattern? x)
(and (value? x)
(or (atom? x)
(if (record/class? x 'unquote 1)
(operation? (record-field x 0))
(andmap pattern? x)))))
```
A valid `Operation` is either a `capture/1`, containing another
pattern; a `discard/0`, denoting wildcard; or `quote/1`, which
promotes an *arbitrary* `Value` to a literal-matching `Pattern`.
This last one is what allows us to write patterns that match
`unquote/1` values without tripping over ourselves.
```racket
(define (operation? x)
(cond [(record/class? x 'capture 1) (pattern? (record-field x 0))]
[(record/class? x 'discard 0) #t]
[(record/class? x 'quote 1) (value? (record-field x 0))]
[else #f]))
```
**Examples**.
```racket
(check-true (pattern? 123))
(check-true (pattern? "Hello"))
(check-true (pattern? 'capture))
(check-true (pattern? 'unquote))
(check-true (pattern? '(Present "Tony")))
(check-true (pattern? '(Says "Tony" "Hello, world!")))
(check-true (pattern? '(Says "Tony" (capture (discard)))))
(check-true (pattern? '(Says "Tony" (unquote (capture (discard))))))
```
Since `pattern?` subsumes `value?`, we see that each of these is
both a `Value` and a `Pattern`. However, the following term is a
`Value` but not a `Pattern`, because it does not conform to the
definition of the `unquote`d `Operation`s.
<!--
```racket
(let ()
```
-->
```racket
(define non-pattern '(Says "Tony" (unquote (noise))))
(check-true (value? non-pattern))
(check-false (pattern? non-pattern))
```
<!--
```racket
)
```
-->
We may use `quote` in conjunction with `unquote` to specify a
pattern that will match our `non-pattern` example:
```racket
(check-true (pattern? '(Says "Tony" ((unquote (quote unquote)) (noise)))))
```
We may also abuse the Lisp notation for quotation and
quasiquotation when writing such patterns, which helps make them a
little shorter and perhaps easier to read:
```racket
(check-true (pattern? '(Says "Tony" (,'unquote (noise)))))
```
Finally, this term isn't even a `Value`: it includes an empty list
within it.
```racket
(check-false (value? '(Says "Tony" ())))
```
## Pattern matching
Let's call our matching operator `Match`, with a capital `M` to
distinguish it from Racket's own `match` syntax.
`Match`, given a `pat`tern and a `val`ue, should answer either a
`List` of the captured values in depth-first, left-to-right order,
if the pattern matches the value, or `#f` if the arguments do not
match.
```racket
;; ;; Precondition: (and (pattern? pat) (value? val))
;; (define (Match pat val)
;; ;;; First of all, let's take care of matching atoms.
;; (cond [(atom? pat) (if (equal? pat val) '() #f)]
;; ;;; Next, the special pattern record `unquote/1` and the operators it
;; ;;; contains.
;; [(record/class? pat 'unquote 1)
;; (define op (record-field pat 0))
;; ;;; A `capture/1` should prepend the current `val`ue to a succeeding
;; ;;; submatch, and should propagate a failing submatch.
;; (cond [(record/class? op 'capture 1)
;; (define r (Match (record-field op 0) val))
;; (and r (cons val r))]
;; ;;; A `discard/0` should accept any `val`ue, yielding a success result
;; ;;; containing no captures.
;; [(record/class? op 'discard 0)
;; '()]
;; ;;; Finally, a `quote/1` should match exactly its argument and nothing
;; ;;; else.
;; [(record/class? op 'quote 1)
;; (if (equal? (record-field op 0) val) '() #f)]
```
---------------------------------------------------------------------------
```racket
;; (struct DISCARD ())
;; (struct CAPTURE (p))
;; (define (q p)
;; (match p
;; [(DISCARD) `(discard)]
;; [(CAPTURE p) `(capture ,(q p))]
;; [`(discard) `('discard)]
;; [`(capture ,p) `('capture ,(q p))]
;; [`(quote ,p) `('quote ,(q p))]
;; [`(,pa . ,pd) `(,(q pa) . ,(q pd))]
;; [a a]))
;; (define (uq p)
;; (match p
;; [`(discard) (DISCARD)]
;; [`(capture ,p) (CAPTURE (uq p))]
;; [`(quote ,p) p]
;; [`(,pa . ,pd) `(,(uq pa) . ,(uq pd))]
;; [a a]))
;; ;; Goal: (uq (q p)) === p
;; ;; (define (m p v k)
;; ;; (match* (p v)
;; ;; [(`(discard) _) (k '())]
;; ;; [(`(capture ,p) v) (m p v (lambda (bs) (cons v bs)))]
;; ;; [(`(quote ,p) v) (and (equal? p v) (k '()))]
;; ;; [(`(,pa . ,pd) `(,va . ,vd)) (m pa va (lambda (bs) (m pd vd (lambda (cs) (k (append bs cs))))))]
;; ;; [(p v) (and (equal? p v) (k '()))]))
;; (define (m p v k)
;; (match* (p v)
;; [((DISCARD) _) (k '())]
;; [((CAPTURE p) v) (m p v (lambda (bs) (cons v bs)))]
;; [(`(,pa . ,pd) `(,va . ,vd)) (m pa va (lambda (bs) (m pd vd (lambda (cs) (k (append bs cs))))))]
;; [(p v) (and (equal? p v) (k '()))]))
;; (module+ test
;; (require rackunit)
;; ;; (define (M p v) (m p v values))
;; (define (M p v) (m (uq p) v values))
;; (check-equal? (M `(capture 1) 1) '(1))
;; (check-equal? (M `(discard) 1) '())
;; (check-equal? (M 1 1) '())
;; (check-equal? (M 2 1) #f)
;; (check-equal? (M `(capture 2) 1) #f)
;; (check-equal? (M `(record (capture (discard))) `(record value)) '(value))
;; (check-equal? (M `(record (capture (discard))) `(record 'value)) '('value))
;; (check-equal? (M `(record (capture (discard))) `(record (capture (discard))))
;; '((capture (discard))))
;; (check-equal? (M `(record ('capture (discard))) `(record (capture (discard))))
;; '())
;; (check-equal? (M `(record (capture ('capture (discard)))) `(record (capture (discard))))
;; '((capture (discard))))
;; (check-equal? (M `(record (capture ('capture (discard)))) `(record value))
;; #f)
;; (check-equal? (M `(record (capture ('capture (discard)))) `(record 'value))
;; #f)
;; (check-equal? (M `(record (capture ('capture (discard)))) `(record ('capture (discard))))
;; #f)
;; (check-equal? (M `(record '(capture (discard))) `(record (capture (discard))))
;; '())
;; (check-equal? (M `(record (capture '(capture (discard)))) `(record (capture (discard))))
;; '((capture (discard))))
;; (check-equal? (M `(record (capture '(capture (discard)))) `(record value))
;; #f)
;; (check-equal? (M `(record (capture '(capture (discard)))) `(record 'value))
;; #f)
;; (check-equal? (M `(record (capture '(capture (discard)))) `(record '(capture (discard))))
;; #f)
;; (check-equal? (M `(record ('quote value)) `(record (capture (discard)))) #f)
;; (check-equal? (M `(record (capture ('quote value))) `(record (capture (discard)))) #f)
;; (check-equal? (M `(record (capture ('quote value))) `(record value)) #f)
;; (check-equal? (M `(record (capture ('quote value))) `(record 'value)) '('value))
;; (check-equal? (M `(record (capture ('quote value))) `(record 'notvalue)) #f)
;; (check-equal? (M `(record ('quote value)) `(record 'value)) '())
;; (check-equal? (M `(record (capture ('quote value))) `(record ('quote value))) #f)
;; (check-equal? (M `(record ''value) `(record (capture (discard)))) #f)
;; (check-equal? (M `(record (capture ''value)) `(record (capture (discard)))) #f)
;; (check-equal? (M `(record (capture ''value)) `(record value)) #f)
;; (check-equal? (M `(record (capture ''value)) `(record 'value)) '('value))
;; (check-equal? (M `(record (capture ''value)) `(record 'notvalue)) #f)
;; (check-equal? (M `(record ''value) `(record 'value)) '())
;; (check-equal? (M `(record (capture ''value)) `(record ''value)) #f)
;; (check-equal? (q (CAPTURE 1)) `(capture 1))
;; (check-equal? (q (DISCARD)) `(discard))
;; (check-equal? (q `(capture 1)) `('capture 1))
;; (check-equal? (q `(discard)) `('discard))
;; )
```

358
unquoting.rkt Normal file
View File

@ -0,0 +1,358 @@
;;; ---
;;; title: (Un)quotation in layered pub/sub networks
;;; ---
;;; <!--
#lang racket
(require rackunit)
(require racket/contract)
;;; -->
;;; Tony Garnock-Jones <tonyg@leastfixedpoint.com>
;;; June 2020.
;;; ## Introduction
;;; There's potential for confusion whenever *patterns* are drawn from
;;; the same set that the *values to be matched* come from.
;;; In layered pub/sub networks like
;;; [Syndicate](https://syndicate-lang.org/), publisher-subscriber
;;; relationships are set up using messages carried over the
;;; publish-subscribe medium itself.
;;; Subscribers build messages containing patterns describing other
;;; messages they are interested in.
;;; But in general, these messages travel across multiple layered
;;; pub/sub dataspaces. To avoid confusion, we have to be very clear
;;; about when a piece of data denotes a pattern and when it is just a
;;; piece of data.
;;; In this post, I'll describe the approach I want to take to solve
;;; this problem for Syndicate in the general case.
;;; ### What's the problem?
;;; Consider regular expressions. The regex `ab*c` matches `ac`,
;;; `abc`, `abbc`, and so on; but what if we wanted to match the
;;; literal string `ab*c`? We have to escape the star in the pattern,
;;; writing the pattern as `ab\*c`.
;;; #### Quotation
;;; If we want to use a regex engine to search for a literal string
;;; supplied by someone else---perhaps a user, perhaps an API
;;; client---we have to take care to *quote* the literal string, in
;;; order to avoid confusion caused by metacharacters:[^racket-regexp-quote]
;;; | Literal string | Quoted form |
;;; | --- | --- |
;;; | `no metachars` | `no metachars` |
;;; | `ab*c` | `ab\*c` |
;;; | `...` | `\.\.\.` |
;;; | `(hello \$\ [world])` | `\(hello \\\$\\ \[world\]\)` |
;;; [^racket-regexp-quote]: Racket supplies
;;; [`regexp-quote`](https://github.com/racket/racket/blob/5bb837661c12a9752c6a99f952c0e1b267645b33/racket/collects/racket/private/string.rkt#L38-L51)
;;; ([docs](https://docs.racket-lang.org/reference/regexp.html?q=reg%20quo#(def._((lib._racket%2Fprivate%2Fbase..rkt)._regexp-quote))))
;;; for this purpose:
(check-equal? (regexp-quote "ab*c") "ab\\*c")
(check-equal? (regexp-quote "...") "\\.\\.\\.")
(check-equal? (regexp-quote "(hello \\$\\ [world])") "\\(hello \\\\\\$\\\\ \\[world\\]\\)")
;;; #### Invariant
;;; The invariant we want to rely on is
;;;
;;; > every string, after quotation, becomes a regular expression that matches
;;; > exactly and only the original string.[^racket-regexp-quotation-invariant]
;;; [^racket-regexp-quotation-invariant]:
;;; Expressing this in code is straightforward:
(define (regexp-quotation-invariant original-string some-other-string)
(equal? (string=? original-string some-other-string)
(regexp-match? (regexp-quote original-string) some-other-string)))
;;; We could use Racket's [random data
;;; generation](https://docs.racket-lang.org/data/Enumerations.html?q=data%2Fen#%28mod-path._data%2Fenumerate%29)
;;; tools to perform randomized testing of this invariant.
;;; Of course, this same problem crops up in any pattern language
;;; where embedding of values in patterns makes sense, so let's
;;; generalize accordingly:
;;;
;;; > every value, after quotation, becomes a pattern that matches
;;; > exactly and only the original value.
;;; ### Quotation of pub/sub patterns.
;;; In [Syndicate](https://syndicate-lang.org/), we want patterns over
;;; assertions (and thus over messages) to be able to match arbitrary
;;; [Preserves](.) atoms, sequences, and records.
;;; However, to date, there have been special exceptions. The special
;;; records `capture/1` and `discard/0`, embedded in patterns, have
;;; been interpreted as defining pattern variables and wildcards,
;;; respectively. There has been no way to construct a pattern that
;;; matches `capture/1` or `discard/0` records themselves.
;;; Previously, I tried adding a `quote/1` record to the set of
;;; special record types. Experimentation [demonstrated](quoting.rkt)
;;; that patterns with `quote/1` were able to escape the limitations
;;; of patterns without `quote/1`. Also, it's [a theorem](quoting.v)
;;; that quoting is "sensible": that unquotation after quotation of a
;;; pattern always equals the original pattern.
;;;
;;; In this post, I'll explore an alternative I think might be better:
;;; letting patterns match anything except a *single* special record,
;;; `unquote/1`. Patterns use `unquote/1` to escape into a
;;; *metalanguage* where special operators like capture, discard, and
;;; so on can be discussed.
;;; ## Definitions
;;;
;;; We'll work with a simplified data language. Instead of full
;;; Preserves, which includes lists, maps, records, a variety of atoms
;;; and so forth, we'll stick to just records and atoms.
;;;
;;; `Value`s are the things our `Pattern`s are to match.
;;;
;;; `Value`s that are `Lists` denote records: the first `Value` is the
;;; label of the record, and the remaining `Value`s are its fields.
(define (record? x)
(and (list? x)
(positive? (length x))
(andmap value? x)))
(define (record-label x) (car x))
(define (record-fields x) (cdr x))
(define (record-arity x) (length (record-fields x)))
(define (record-field x n) (list-ref x (+ n 1)))
;;; Atoms, then, are the non-`List` `Value`s.
(define (atom? x)
(or (string? x)
(symbol? x)
(number? x)))
;;; `Value`s are the records and the atoms, and nothing else.
(define (value? x)
(or (atom? x)
(record? x)))
;;; We will frequently need to decide whether a `Value` is a record
;;; with a particular label and arity.
(define (record/class? x label arity)
(and (record? x)
(equal? (record-label x) label)
(= (record-arity x) arity)))
;;; A `Pattern` is a `Value` with certain additional constraints on
;;; the `Operation`s that appear within an `unquote/1` record.
(define (pattern? x)
(and (value? x)
(or (atom? x)
(if (record/class? x 'unquote 1)
(operation? (record-field x 0))
(andmap pattern? x)))))
;;; A valid `Operation` is either a `capture/1`, containing another
;;; pattern; a `discard/0`, denoting wildcard; or `quote/1`, which
;;; promotes an *arbitrary* `Value` to a literal-matching `Pattern`.
;;; This last one is what allows us to write patterns that match
;;; `unquote/1` values without tripping over ourselves.
(define (operation? x)
(cond [(record/class? x 'capture 1) (pattern? (record-field x 0))]
[(record/class? x 'discard 0) #t]
[(record/class? x 'quote 1) (value? (record-field x 0))]
[else #f]))
;;; **Examples**.
(check-true (pattern? 123))
(check-true (pattern? "Hello"))
(check-true (pattern? 'capture))
(check-true (pattern? 'unquote))
(check-true (pattern? '(Present "Tony")))
(check-true (pattern? '(Says "Tony" "Hello, world!")))
(check-true (pattern? '(Says "Tony" (capture (discard)))))
(check-true (pattern? '(Says "Tony" (unquote (capture (discard))))))
;;; Since `pattern?` subsumes `value?`, we see that each of these is
;;; both a `Value` and a `Pattern`. However, the following term is a
;;; `Value` but not a `Pattern`, because it does not conform to the
;;; definition of the `unquote`d `Operation`s.
;;; <!--
(let ()
;;; -->
(define non-pattern '(Says "Tony" (unquote (noise))))
(check-true (value? non-pattern))
(check-false (pattern? non-pattern))
;;; <!--
)
;;; -->
;;; We may use `quote` in conjunction with `unquote` to specify a
;;; pattern that will match our `non-pattern` example:
(check-true (pattern? '(Says "Tony" ((unquote (quote unquote)) (noise)))))
;;; We may also abuse the Lisp notation for quotation and
;;; quasiquotation when writing such patterns, which helps make them a
;;; little shorter and perhaps easier to read:
(check-true (pattern? '(Says "Tony" (,'unquote (noise)))))
;;; Finally, this term isn't even a `Value`: it includes an empty list
;;; within it.
(check-false (value? '(Says "Tony" ())))
;;; ## Pattern matching
;;;
;;; Let's call our matching operator `Match`, with a capital `M` to
;;; distinguish it from Racket's own `match` syntax.
;;;
;;; `Match`, given a `pat`tern and a `val`ue, should answer either a
;;; `List` of the captured values in depth-first, left-to-right order,
;;; if the pattern matches the value, or `#f` if the arguments do not
;;; match.
;; ;; Precondition: (and (pattern? pat) (value? val))
;; (define (Match pat val)
;; ;;; First of all, let's take care of matching atoms.
;; (cond [(atom? pat) (if (equal? pat val) '() #f)]
;; ;;; Next, the special pattern record `unquote/1` and the operators it
;; ;;; contains.
;; [(record/class? pat 'unquote 1)
;; (define op (record-field pat 0))
;; ;;; A `capture/1` should prepend the current `val`ue to a succeeding
;; ;;; submatch, and should propagate a failing submatch.
;; (cond [(record/class? op 'capture 1)
;; (define r (Match (record-field op 0) val))
;; (and r (cons val r))]
;; ;;; A `discard/0` should accept any `val`ue, yielding a success result
;; ;;; containing no captures.
;; [(record/class? op 'discard 0)
;; '()]
;; ;;; Finally, a `quote/1` should match exactly its argument and nothing
;; ;;; else.
;; [(record/class? op 'quote 1)
;; (if (equal? (record-field op 0) val) '() #f)]
;;; ---------------------------------------------------------------------------
;; (struct DISCARD ())
;; (struct CAPTURE (p))
;; (define (q p)
;; (match p
;; [(DISCARD) `(discard)]
;; [(CAPTURE p) `(capture ,(q p))]
;; [`(discard) `('discard)]
;; [`(capture ,p) `('capture ,(q p))]
;; [`(quote ,p) `('quote ,(q p))]
;; [`(,pa . ,pd) `(,(q pa) . ,(q pd))]
;; [a a]))
;; (define (uq p)
;; (match p
;; [`(discard) (DISCARD)]
;; [`(capture ,p) (CAPTURE (uq p))]
;; [`(quote ,p) p]
;; [`(,pa . ,pd) `(,(uq pa) . ,(uq pd))]
;; [a a]))
;; ;; Goal: (uq (q p)) === p
;; ;; (define (m p v k)
;; ;; (match* (p v)
;; ;; [(`(discard) _) (k '())]
;; ;; [(`(capture ,p) v) (m p v (lambda (bs) (cons v bs)))]
;; ;; [(`(quote ,p) v) (and (equal? p v) (k '()))]
;; ;; [(`(,pa . ,pd) `(,va . ,vd)) (m pa va (lambda (bs) (m pd vd (lambda (cs) (k (append bs cs))))))]
;; ;; [(p v) (and (equal? p v) (k '()))]))
;; (define (m p v k)
;; (match* (p v)
;; [((DISCARD) _) (k '())]
;; [((CAPTURE p) v) (m p v (lambda (bs) (cons v bs)))]
;; [(`(,pa . ,pd) `(,va . ,vd)) (m pa va (lambda (bs) (m pd vd (lambda (cs) (k (append bs cs))))))]
;; [(p v) (and (equal? p v) (k '()))]))
;; (module+ test
;; (require rackunit)
;; ;; (define (M p v) (m p v values))
;; (define (M p v) (m (uq p) v values))
;; (check-equal? (M `(capture 1) 1) '(1))
;; (check-equal? (M `(discard) 1) '())
;; (check-equal? (M 1 1) '())
;; (check-equal? (M 2 1) #f)
;; (check-equal? (M `(capture 2) 1) #f)
;; (check-equal? (M `(record (capture (discard))) `(record value)) '(value))
;; (check-equal? (M `(record (capture (discard))) `(record 'value)) '('value))
;; (check-equal? (M `(record (capture (discard))) `(record (capture (discard))))
;; '((capture (discard))))
;; (check-equal? (M `(record ('capture (discard))) `(record (capture (discard))))
;; '())
;; (check-equal? (M `(record (capture ('capture (discard)))) `(record (capture (discard))))
;; '((capture (discard))))
;; (check-equal? (M `(record (capture ('capture (discard)))) `(record value))
;; #f)
;; (check-equal? (M `(record (capture ('capture (discard)))) `(record 'value))
;; #f)
;; (check-equal? (M `(record (capture ('capture (discard)))) `(record ('capture (discard))))
;; #f)
;; (check-equal? (M `(record '(capture (discard))) `(record (capture (discard))))
;; '())
;; (check-equal? (M `(record (capture '(capture (discard)))) `(record (capture (discard))))
;; '((capture (discard))))
;; (check-equal? (M `(record (capture '(capture (discard)))) `(record value))
;; #f)
;; (check-equal? (M `(record (capture '(capture (discard)))) `(record 'value))
;; #f)
;; (check-equal? (M `(record (capture '(capture (discard)))) `(record '(capture (discard))))
;; #f)
;; (check-equal? (M `(record ('quote value)) `(record (capture (discard)))) #f)
;; (check-equal? (M `(record (capture ('quote value))) `(record (capture (discard)))) #f)
;; (check-equal? (M `(record (capture ('quote value))) `(record value)) #f)
;; (check-equal? (M `(record (capture ('quote value))) `(record 'value)) '('value))
;; (check-equal? (M `(record (capture ('quote value))) `(record 'notvalue)) #f)
;; (check-equal? (M `(record ('quote value)) `(record 'value)) '())
;; (check-equal? (M `(record (capture ('quote value))) `(record ('quote value))) #f)
;; (check-equal? (M `(record ''value) `(record (capture (discard)))) #f)
;; (check-equal? (M `(record (capture ''value)) `(record (capture (discard)))) #f)
;; (check-equal? (M `(record (capture ''value)) `(record value)) #f)
;; (check-equal? (M `(record (capture ''value)) `(record 'value)) '('value))
;; (check-equal? (M `(record (capture ''value)) `(record 'notvalue)) #f)
;; (check-equal? (M `(record ''value) `(record 'value)) '())
;; (check-equal? (M `(record (capture ''value)) `(record ''value)) #f)
;; (check-equal? (q (CAPTURE 1)) `(capture 1))
;; (check-equal? (q (DISCARD)) `(discard))
;; (check-equal? (q `(capture 1)) `('capture 1))
;; (check-equal? (q `(discard)) `('discard))
;; )

1393
unquoting.v Normal file
View File

File diff suppressed because it is too large Load Diff