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
|
;;; Continuation-passing style (CPS) intermediate language (IL)
;; Copyright (C) 2013 Free Software Foundation, Inc.
;;;; This library is free software; you can redistribute it and/or
;;;; modify it under the terms of the GNU Lesser General Public
;;;; License as published by the Free Software Foundation; either
;;;; version 3 of the License, or (at your option) any later version.
;;;;
;;;; This library is distributed in the hope that it will be useful,
;;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
;;;; Lesser General Public License for more details.
;;;;
;;;; You should have received a copy of the GNU Lesser General Public
;;;; License along with this library; if not, write to the Free Software
;;;; Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
;;; Commentary:
;;;
;;;
;;; Code:
(define-module (language cps verify)
#:use-module (ice-9 match)
#:use-module (srfi srfi-26)
#:use-module (language cps)
#:export (verify-cps))
(define (verify-cps fun)
(define seen-gensyms (make-hash-table))
(define (add sym env)
(if (hashq-ref seen-gensyms sym)
(error "duplicate gensym" sym)
(begin
(hashq-set! seen-gensyms sym #t)
(cons sym env))))
(define (add-env new env)
(if (null? new)
env
(add-env (cdr new) (add (car new) env))))
(define (check-var sym env)
(cond
((not (hashq-ref seen-gensyms sym))
(error "unbound lexical" sym))
((not (memq sym env))
(error "displaced lexical" sym))))
(define (check-src src)
(if (and src (not (and (list? src) (and-map pair? src)
(and-map symbol? (map car src)))))
(error "bad src")))
(define (visit-cont-body cont k-env v-env)
(match cont
(($ $kif kt kf)
(check-var kt k-env)
(check-var kf k-env))
(($ $ktrunc ($ $arity ((? symbol?) ...) () (or #f (? symbol?)) () #f) k)
(check-var k k-env))
(($ $kargs ((? symbol? name) ...) ((? symbol? sym) ...) body)
(unless (= (length name) (length sym))
(error "name and sym lengths don't match" name sym))
(visit-term body k-env (add-env sym v-env)))
(_
;; $kclause, $kentry, and $ktail are only ever seen in $fun.
(error "unexpected cont body" cont))))
(define (visit-clause clause k-env v-env)
(match clause
(($ $cont kclause src*
($ $kclause
($ $arity
((? symbol? req) ...)
((? symbol? opt) ...)
(and rest (or #f (? symbol?)))
(((? keyword? kw) (? symbol? kwname) (? symbol? kwsym)) ...)
(or #f #t))
($ $cont kbody src (and body ($ $kargs names syms _)))))
(check-src src*)
(check-src src)
(for-each (lambda (sym)
(unless (memq sym syms)
(error "bad keyword sym" sym)))
kwsym)
;; FIXME: It is technically possible for kw syms to alias other
;; syms.
(unless (equal? (append req opt (if rest (list rest) '()) kwname)
names)
(error "clause body names do not match arity names" exp))
(let ((k-env (add-env (list kclause kbody) k-env)))
(visit-cont-body body k-env v-env)))
(_
(error "unexpected clause" clause))))
(define (visit-fun fun k-env v-env)
(match fun
(($ $fun meta ((? symbol? free) ...)
($ $cont kbody src
($ $kentry (? symbol? self) ($ $cont ktail _ ($ $ktail)) clauses)))
(when (and meta (not (and (list? meta) (and-map pair? meta))))
(error "meta should be alist" meta))
(for-each (cut check-var <> v-env) free)
(check-src src)
;; Reset the continuation environment, because Guile's
;; continuations are local.
(let ((v-env (add-env (list self) v-env))
(k-env (add-env (list ktail) '())))
(for-each (cut visit-clause <> k-env v-env) clauses)))
(_
(error "unexpected $fun" fun))))
(define (visit-expression exp k-env v-env)
(match exp
(($ $var sym)
(check-var sym v-env))
(($ $void)
#t)
(($ $const val)
#t)
(($ $prim (? symbol? name))
#t)
(($ $fun)
(visit-fun fun k-env v-env))
(($ $call (? symbol? proc) ((? symbol? arg) ...))
(check-var proc v-env)
(for-each (cut check-var <> v-env) arg))
(($ $primcall (? symbol? name) ((? symbol? arg) ...))
(for-each (cut check-var <> v-env) arg))
(($ $values ((? symbol? arg) ...))
(for-each (cut check-var <> v-env) arg))
(($ $prompt escape? tag handler)
(unless (boolean? escape?) (error "escape? should be boolean" escape?))
(check-var tag v-env)
(check-var handler k-env))
(_
(error "unexpected expression" exp))))
(define (visit-term term k-env v-env)
(match term
(($ $letk (($ $cont (? symbol? k) src cont) ...) body)
(let ((k-env (add-env k k-env)))
(for-each check-src src)
(for-each (cut visit-cont-body <> k-env v-env) cont)
(visit-term body k-env v-env)))
(($ $letrec ((? symbol? name) ...) ((? symbol? sym) ...) (fun ...) body)
(unless (= (length name) (length sym) (length fun))
(error "letrec syms, names, and funs not same length" term))
(let ((v-env (add-env sym v-env)))
(for-each (cut visit-fun <> k-env v-env) fun)
(visit-term body k-env v-env)))
(($ $continue k exp)
(check-var k k-env)
(visit-expression exp k-env v-env))
(_
(error "unexpected term" term))))
(visit-fun fun '() '())
fun)
|