-
Notifications
You must be signed in to change notification settings - Fork 6
/
matche.tex
210 lines (181 loc) · 7.15 KB
/
matche.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
\chapter{{\bf \matchesymbol} and {\bf \lambdaesymbol}}\label{matche}
In this appendix we describe \scheme|matche| and \scheme|lambdae|,
pattern-matching macros for writing concise miniKanren programs.
These macros were designed by Will Byrd and implemented by Ramana
Kumar with the help of Dan Friedman.
To illustrate the use of \scheme|matche| and \scheme|lambdae|
we will rewrite the explicit definition of \scheme|appendo|, which uses
the core miniKanren operators \scheme|==|, \scheme|conde|, and \scheme|exist|.
\schemedisplayspace
\begin{schemedisplay}
(define appendo
(lambda (l s out)
(conde
((== '() l) (== s out))
((exist (a d res)
(== `(,a . ,d) l)
(== `(,a . ,res) out)
(appendo d s res))))))
\end{schemedisplay}
We can shorten the \scheme|appendo| definition using \scheme|matche|.
\scheme|matche| resembles \scheme|pmatch| (Appendix~\ref{pmatch})
syntactically, but uses unification rather than uni-directional
pattern matching. \scheme|matche| expands into a \scheme|conde|;
each \scheme|matche| clause becomes a \scheme|conde|
clause\footnote{The \scheme|matcha| and \scheme|matchu| forms are
identical to \scheme|matche|, except they expand into uses of
\scheme|conda| and \scheme|condu|, respectively.}. As with
\scheme|pmatch| the first expression in each clause is an implicitly
quasiquoted pattern. Unquoted identifiers in a pattern are introduced
as unassociated logic variables whose scope is limited to the pattern
and goals in that clause.
Here is \scheme|appendo| defined with \scheme|matche|.
\schemedisplayspace
\begin{schemedisplay}
(define appendo
(lambda (l s out)
(match-e `(,l ,s ,out)
(`(() ,s ,s))
(`((,a . ,d) ,s (,a . ,res)) (appendo d s res)))))
\end{schemedisplay}
\noindent The pattern in the first clause attempts to unify the first
argument of \scheme|appendo| with the empty list, while also unifying
\scheme|appendo|'s second and third arguments. The same unquoted
identifier can appear more than once in a \scheme|matche| pattern;
this is not allowed in \scheme|pmatch|.
We can make \scheme|appendo| even shorter by using \scheme|lambdae|.
\scheme|lambdae| just expands into a \scheme|lambda| wrapped around a
\scheme|matche|---the \scheme|matche| matches against the
\scheme|lambda|'s argument list\footnote{The \scheme|lambdaa| and \scheme|lambdau| forms are
identical to \scheme|lambdae|, except they expand into uses of
\scheme|matcha| and \scheme|matchu|, respectively.}.
\schemedisplayspace
\begin{schemedisplay}
(define appendo
(lambda-e (l s out)
(`(() ,s ,s))
(`((,a . ,d) ,s (,a . ,res)) (appendo d s res))))
\end{schemedisplay}
The double-underscore symbol \scheme|__| represents a pattern wildcard
that matches any value without binding it to a variable. For example,
the pattern in \scheme|pairo|
\schemedisplayspace
\begin{schemedisplay}
(define pairo
(lambda-e (x)
(`((__ . __)))))
\end{schemedisplay}
\noindent matches any pair, regardless of the values of its car and
cdr.
\scheme|lambdae| and \scheme|matche| also support nominal logic (see
Chapter~\ref{akchapter}). Just as unquoted identifiers in a pattern
are introduced as unassociated logic variables, using unquote splicing
in a pattern introduces a fresh nom whose scope is limited to the
pattern and goals in that clause. For example, the goal constructor
\schemedisplayspace
\begin{schemedisplay}
(define foo
(lambda (t)
(fresh (a b)
(exist (x y)
(conde
((== (tie a (tie b `(,x ,b))) t))
((== (tie a (tie b `(,y ,b))) t))
((== (tie a (tie b `(,b ,y))) t))
((== (tie a (tie b `(,b ,y))) t)))))))
\end{schemedisplay}
\noindent can be re-written as
\schemedisplayspace
\begin{schemedisplay}
(define foo
(lambda-e (t)
(`(tie-tag ,@a (tie-tag ,@b (,x ,@b))))
(`(tie-tag ,@a (tie-tag ,@b (,y ,@b))))
(`(tie-tag ,@a (tie-tag ,@b (,@b ,y))))
(`(tie-tag ,@a (tie-tag ,@b (,@b ,y))))))
\end{schemedisplay}
\noindent where \scheme|'tie-tag| is the tag returned by the
\scheme|tie| constructor\footnote{Unfortunately, this explicit pattern
matching breaks the abstraction of the \scheme|tie| constructor.}.
Here is the definition of \scheme|lambdae|,
and its impure variants \scheme|lambdaa| and \scheme|lambdau|.
\schemedisplayspace
\begin{schemedisplay}
(define-syntax lambdae
(syntax-rules ()
((_ (x ...) c c* ...)
(lambda (x ...) (matche (quasiquote (unquote x) ...) (c c* ...) ())))))
(define-syntax lambdaa
(syntax-rules ()
((_ (x ...) c c* ...)
(lambda (x ...) (matcha (quasiquote (unquote x) ...) (c c* ...) ())))))
(define-syntax lambdau
(syntax-rules ()
((_ (x ...) c c* ...)
(lambda (x ...) (matchu (quasiquote (unquote x) ...) (c c* ...) ())))))
\end{schemedisplay}
Here is the definition of \scheme|matche|, and its impure variants \scheme|matcha| and \scheme|matchu|.
\schemedisplayspace
\begin{schemedisplay}
(define-syntax exist*
(syntax-rules ()
((_ (x ...) g0 g ...)
(lambdag@ (a)
(inc
(let* ((x (var 'x)) ...)
(bind* (g0 a) g ...)))))))
(define-syntax fresh*
(syntax-rules ()
((_ (x ...) g0 g ...)
(lambdag@ (a)
(inc
(let* ((x (nom 'x)) ...)
(bind* (g0 a) g ...)))))))
(define-syntax matche
(syntax-rules ()
((_ (f x ...) g* . cs)
(let ((v (f x ...))) (matche v g* . cs)))
((_ v g* . cs) (mpat conde v (g* . cs) ()))))
(define-syntax matcha
(syntax-rules ()
((_ (f x ...) g* . cs)
(let ((v (f x ...))) (matcha v g* . cs)))
((_ v g* . cs) (mpat conda v (g* . cs) ()))))
\end{schemedisplay}
\newpage
\begin{schemedisplay}
(define-syntax matchu
(syntax-rules ()
((_ (f x ...) g* . cs)
(let ((v (f x ...))) (matchu v g* . cs)))
((_ v g* . cs) (mpat condu v (g* . cs) ()))))
(define-syntax mpat
(syntax-rules (__ quote unquote unquote-splicing expand cons)
((_ co v () (l ...)) (co l ...))
((_ co v (pat) xs as ((g ...) . cs) (l ...))
(mpat co v cs (l ... ((fresh* as (exist* xs (== `pat v) g ...))))))
((_ co v ((__ g0 g ...) . cs) (l ...))
(mpat co v cs (l ... ((exist () g0 g ...)))))
((_ co v (((unquote y) g0 g ...) . cs) (l ...))
(mpat co v cs (l ... ((exist (y) (== y v) g0 g ...)))))
((_ co v (((unquote-splicing b) g0 g ...) . cs) (l ...))
(mpat co v cs (l ... ((fresh (b) g0 g ...)))))
((_ co v ((pat g ...) . cs) ls)
(mpat co v (pat expand) () () ((g ...) . cs) ls))
((_ co v (__ expand . k) (x ...) as cs ls)
(mpat co v ((unquote y) . k) (y x ...) as cs ls))
((_ co v ((unquote y) expand . k) (x ...) as cs ls)
(mpat co v ((unquote y) . k) (y x ...) as cs ls))
((_ co v ((unquote-splicing b) expand . k) xs (a ...) cs ls)
(mpat co v ((unquote b) . k) xs (b a ...) cs ls))
((_ co v ((quote c) expand . k) xs as cs ls)
(mpat co v (c . k) xs as cs ls))
((_ co v ((a . d) expand . k) xs as cs ls)
(mpat co v (d expand a expand cons . k) xs as cs ls))
((_ co v (d a expand cons . k) xs as cs ls)
(mpat co v (a expand d cons . k) xs as cs ls))
((_ co v (a d cons . k) xs as cs ls)
(mpat co v ((a . d) . k) xs as cs ls))
((_ co v (c expand . k) xs as cs ls)
(mpat co v (c . k) xs as cs ls))))
\end{schemedisplay}