This post defines and tests the match/non-overlapping Scheme macro which is
a simple pattern matcher with guards in the style of Dijkstra’s Guarded Commands (Dijkstra 1975). It ensures that the patterns and optional guards of different clauses do not overlap.3 This non-overlapping property ensures that the ordering of the clauses does not matter, and is required for writing correct relational programs (Byrd 2009).
Inspired by the good old paper:
Dijkstra, Edsger W., 1975. Guarded commands, nondeterminacy and formal derivation of programs. In Commun. ACM, Association for Computing Machinery, New York, NY, USA, vol. 18, pp. 453–457.Abstract: So-called “guarded commands” are introduced as a building block for alternative and repetitive constructs that allow nondeterministic program components for which at least the activity evoked, but possibly even the final state, is not necessarily uniquely determined by the initial state. For the formal derivation of programs expressed in terms of these constructs, a calculus will be be shown.
It is a generalization of
Oleg Kiselyov’s pmatch, a
simple pattern-matcher for linear patterns:
from it we adapt the test test/meta-circular-interpreter about a meta-circular interpreter.
This matcher is described and used in the paper about miniKanren.
Our implementation contains:
- some refactorings of the upstream code,
- matching of vectors and records,
- guards are introduced after the
⇒keyword, - injection and negated injection of expressions in patterns (see those in action in a more complex interpreter)
- sexp-based error reporting in case of either no matches or overlapping patterns.
An example
For the sake of clarity, consider the following definition:
(define (w x y)
(match/non-overlapping (cons x y)
((,a . ,b) (and (number? a) (number? b)) ⇒ (* a b))
((,a . ,b) (+ a b))
((,a ,b ,c) (and (number? a) (number? b) (number? c)) ⇒ (+ a b c))))
so that evaluating the expression (list (w 3 4) (apply w '(1 (3 4)))) yields
Error: match/non-overlapping
((reason "overlapping match")
(expr (cons x y))
(value (3 . 4))
(ambiguities
(((,a unquote b) (and (number? a) (number? b)) ⇒ (* a b))
((,a unquote b) #t ⇒ (+ a b)))))
as expected.
Implementation
Tests
test/base-non-overlapping: pass
(define (test/base-non-overlapping _)
(⊦= 'empty (match/non-overlapping '() (() 'empty)))
(⊦= 'empty (match/non-overlapping #() (#() 'empty)))
(⊦= '() (match/non-overlapping '() (,r r)))
(⊦= #() (match/non-overlapping #() (,r r)))
(⊦= 'p (match/non-overlapping '(p) ((,r) r)))
(⊦= #t (match/non-overlapping #(p) (#(p) #t)))
(⊦= 'p (match/non-overlapping #(p) (#(,r) r)))
(⊦= 3 (match/non-overlapping #(3 2) (#(,r 2) r)))
(⊦= '(3 2) (match/non-overlapping #(3 2) (#(,r ,s) (list r s))))
(⊦= '(3 2 ())
(match/non-overlapping
(vector->list #(3 2))
((,r ,s unquote t) (list r s t))))
(⊦⧳ ((exn)) (match/non-overlapping #(3 2) ((,r 2 ,t) r)))
(⊦= 3 (match/non-overlapping #(3 2) (#(,r ,e) r)))
(⊦= 3
(match/non-overlapping
(make-record-instance 'hello 3 2)
(#(hello ,r ,e) r))))
((eta 0.009) (memory #(8401664 2268096 1048576)) (stdout "") (stderr ""))
test/h-non-overlapping: pass
(define (test/h-non-overlapping _)
(define (h x y)
(match/non-overlapping
(cons x y)
(((,a unquote b) ⊣ (and (number? a) (number? b))) (* a b))
(((,a ,b ,c) ⊣ (and (number? a) (number? b) (number? c))) (+ a b c))))
(⊦= '(12 8) (list (h 3 4) (apply h '(1 (3 4))))))
((eta 0.001) (memory #(8401664 2269264 1048576)) (stdout "") (stderr ""))
test/h-overlapping: pass
(define (test/h-overlapping _)
(define (w x y)
(match/non-overlapping
(cons x y)
(((,a unquote b) ⊣ (and (number? a) (number? b))) (* a b))
((,a unquote b) (+ a b))
(((,a ,b ,c) ⊣ (and (number? a) (number? b) (number? c))) (+ a b c))))
(⊦⧳ ((exn)) (list (w 3 4) (apply w '(1 (3 4))))))
((eta 0.003) (memory #(8401664 2274336 1048576)) (stdout "") (stderr ""))
test/meta-circular-interpreter: pass
(define (test/meta-circular-interpreter _)
(define (lookup x env)
(cond ((assq x env) => cdr) (else (error "Can't find " x))))
(define (int code env)
(match/non-overlapping
code
(',x x)
(((let (,x ,e) ,body) ⊣ (symbol? x))
(let ((xv (int e env))) (int body (cons (cons x xv) env))))
((τ ,body) (τ (int body env)))
(((λ ,argl ,body) ⊣ (symbol? argl))
(λ arglv (int body (cons (cons argl arglv) env))))
(((λ (,x) ,body) ⊣ (symbol? x))
(λ (xv) (int body (cons (cons x xv) env))))
(((,op unquote args)
⊣
(not (or (eq? op 'quote) (eq? op 'let) (eq? op 'τ) (eq? op 'λ))))
(let ((opv (int op env)) (argvs (map (λ (c) (int c env)) args)))
(apply opv argvs)))
((,x ⊣ (symbol? x)) (lookup x env))
((,x ⊣ (or (number? x) (string? x))) x)))
(define env0 (interaction-environment/symbols '(+ - display identity)))
(define-syntax-rule (dint body) (int 'body env0))
(⊦ equal? 1 (dint 1))
(⊦ equal? 'x (dint 'x))
(⊦ void? (dint (display 'x)))
(⊦ equal? 'x (dint (identity 'x)))
(⊦⧳ ((exn)) (dint (display x)))
(⊦ equal? 6 (dint (let (x (+ 1 2 3)) x)))
(⊦ equal? 1 (let1 (t (dint (τ 1))) (t)))
(⊦ equal? 1 ((dint (λ (x) x)) 1))
(⊦ equal? '(1 2 3) ((dint (λ x x)) 1 2 3))
(⊦ equal? 5 (((dint (λ (x) (λ (y) (+ x y)))) 2) 3)))
((eta 0.001) (memory #(8401664 2272512 1048576)) (stdout "x") (stderr ""))
test/λ-match-first: pass
(define (test/λ-match-first _)
(define h
(λ-match/first
(((,a ,b) ⊣ (and (number? a) (number? b))) (* a b))
(((,a (,b ,c)) ⊣ (and (number? a) (number? b) (number? c)))
(+ a b c))))
(⊦= '(12 8) (list (h 3 4) (apply h '(1 (3 4))))))
((eta 0.0) (memory #(8401664 2272768 1048576)) (stdout "") (stderr ""))
test/λ-match-first/unquote-unquote-pattern: pass
(define (test/λ-match-first/unquote-unquote-pattern _)
(⊦= 2 (match/first '(1 (1)) ((,x (,,x)) (add1 x)))))
((eta 0.0) (memory #(8401664 2274216 1048576)) (stdout "") (stderr ""))