git @ Cat's Eye Technologies TPiS / rel_1_0_2006_0528
Initial import of TPiS version 1.0 revision 2006.0528. catseye 12 years ago
12 changed file(s) with 1665 addition(s) and 0 deletion(s). Raw diff Collapse all Expand all
+28
-0
LICENSE less more
0 Copyright (c)2006 Chris Pressey. All rights reserved.
1
2 Redistribution and use in source and binary forms, with or without
3 modification, are permitted provided that the following conditions
4 are met:
5
6 1. Redistributions of source code must retain the above copyright
7 notices, this list of conditions and the following disclaimer.
8 2. Redistributions in binary form must reproduce the above copyright
9 notices, this list of conditions, and the following disclaimer in
10 the documentation and/or other materials provided with the
11 distribution.
12 3. Neither the names of the copyright holders nor the names of their
13 contributors may be used to endorse or promote products derived
14 from this software without specific prior written permission.
15
16 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
17 ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES INCLUDING, BUT NOT
18 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
19 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
20 COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
21 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
22 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
23 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
24 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
25 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
26 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
27 POSSIBILITY OF SUCH DAMAGE.
+54
-0
boot.scm less more
0 ;
1 ; boot.scm - bootstrap driver
2 ; Total Procedures in Scheme, May 2006, Chris Pressey
3 ; For license information, see the file LICENSE in this directory.
4 ;
5
6 ;
7 ; Bootstrapping process for asserting that the totality checker
8 ; is itself total.
9 ;
10 (load "std.scm")
11
12 (load "boot1.scm")
13
14 (load "util.scm")
15 (load "env.scm")
16 (load "canon.scm")
17 (load "crit.scm")
18 (load "total.scm")
19
20 (display "Re-loading with real definition of define-total") (newline)
21 (load "boot2.scm")
22
23 (load "util.scm")
24 (load "env.scm")
25 (load "canon.scm")
26 (load "crit.scm")
27 (load "total.scm")
28
29 (load "boot3.scm")
30
31 ;; Define-total.
32
33 (define-total fac
34 (lambda (n)
35 (if (>= n 0)
36 (cond
37 ((zero? n)
38 1)
39 (else
40 (* n (fac (- n 1))))))))
41 ;
42 ; This should be an error.
43 ;
44
45 ;(define-total ever1
46 ; (lambda (x)
47 ; (cond
48 ; ((eq? x 10000)
49 ; x)
50 ; (else
51 ; (ever1 (+ x 1))))))
52
53 (display (fac 5)) (newline)
+38
-0
boot1.scm less more
0 ;
1 ; boot1.scm - first stage bootstrap for define[rec]-total
2 ; Total Procedures in Scheme, May 2006, Chris Pressey
3 ; For license information, see the file LICENSE in this directory.
4 ;
5
6 ;
7 ; These macros are used in the first stage of bootstrapping
8 ; to provide "reasonable" semantics for define-total before
9 ; total procedure checking is actually defined. i.e. it
10 ; allows the procedure to be defined, without actually checking
11 ; it, on the assumption that a future bootstrapping pass will
12 ; do that. ("This is Fake D.I.Y.")
13 ;
14 ; Note that these do not affect known-total-env in any way.
15 ;
16 (define-syntax define-total
17 (syntax-rules ()
18 ((define-total proc-name lambda-expr)
19 (begin
20 (define proc-name lambda-expr)
21 (display "WARNING: assuming ") (display (quote proc-name)) (display " is total for now, ")
22 (display "please re-load file with real define-total later") (newline)))))
23
24 (define-syntax definerec-total
25 (syntax-rules ()
26 ((definerec-total ((name val) ...))
27 (definerec-total "split" (name ...) (val ...) () ()))
28 ((definerec-total "split" (name1 name2 ...) (val1 val2 ...) nacc vacc)
29 (definerec-total "split" (name2 ...) (val2 ...) (name1 . nacc) (val1 . vacc)))
30 ((definerec-total "split" () () nacc vacc)
31 (definerec-total "define" nacc vacc))
32 ((definerec-total "define" (name1 name2 ...) (val1 val2 ...))
33 (begin
34 (define-total name1 val1)
35 (definerec-total "define" (name2 ...) (val2 ...))))
36 ((definerec-total "define" () ())
37 (display ""))))
+47
-0
boot2.scm less more
0 ;
1 ; boot2.scm - second stage bootstrap for define[rec]-total
2 ; Total Procedures in Scheme, May 2006, Chris Pressey
3 ; For license information, see the file LICENSE in this directory.
4 ;
5
6 ;
7 ; These macros are used in the second stage of bootstrapping, to
8 ; replace the existing definitions of assumed total procedures with
9 ; genuinely checked total procedures.
10 ;
11 ; Note that these DO affect known-total-env, by adding to it.
12 ;
13 (define-syntax define-total
14 (syntax-rules ()
15 ((define-total proc-name lambda-expr)
16 (begin
17 (display "Redefining ") (display (quote proc-name)) (display " as total procedure") (newline)
18 (let* ((proc-rep (canonicalize (quote lambda-expr) known-total-env)))
19 (cond
20 ((not (proc-total? (quote proc-name) proc-rep known-total-env))
21 (error "procedure could not be determined to be total")))
22 (set! known-total-env
23 (extend-env known-total-env (quote proc-name) 'total-proc))
24 (set! proc-name lambda-expr))))))
25
26 (define-syntax definerec-total
27 (syntax-rules ()
28 ((definerec-total ((name val) ...))
29 (definerec-total "split" (name ...) (val ...) () ()))
30 ((definerec-total "split" (name1 name2 ...) (val1 val2 ...) nacc vacc)
31 (definerec-total "split" (name2 ...) (val2 ...) (name1 . nacc) (val1 . vacc)))
32 ((definerec-total "split" () () names exprs)
33 (begin
34 (display "Redefining ") (display (quote names)) (display " as total procedures") (newline)
35 (cond
36 ((not (procs-total? (quote names) (quote exprs) known-total-env))
37 (error "procedures could not be determined to be total")))
38 (set! known-total-env
39 (names->env (quote names) 'total-proc known-total-env))
40 (definerec-total "define" names exprs)))
41 ((definerec-total "define" (name1 name2 ...) (val1 val2 ...))
42 (begin
43 (set! name1 val1)
44 (definerec-total "define" (name2 ...) (val2 ...))))
45 ((definerec-total "define" () ())
46 (display ""))))
+53
-0
boot3.scm less more
0 ;
1 ; boot3.scm - third stage bootstrap for define[rec]-total
2 ; Total Procedures in Scheme, May 2006, Chris Pressey
3 ; For license information, see the file LICENSE in this directory.
4 ;
5
6 ;
7 ; Given a new procedure name and a procedure (lambda) S-expression, define
8 ; a new procedure with this name and this lambda, if and only if it can be
9 ; established that the procedure is total.
10 ;
11 ; This has side-effects; an environment of known-total procedures is kept,
12 ; and if the given procedure turns out to be total, it is added to this.
13 ;
14 ; A new environment is set up which initially associates each argument name
15 ; with a nil value, indicating that we know nothing about it yet.
16 ;
17 ; These are the final, "real" definitions of define-total and definerec-total,
18 ; used in the last stage of the bootstrapping process.
19 ;
20 (define-syntax define-total
21 (syntax-rules ()
22 ((define-total proc-name lambda-expr)
23 (begin
24 (define proc-name 'TBA)
25 (let* ((proc-rep (canonicalize (quote lambda-expr) known-total-env)))
26 (cond
27 ((not (proc-total? (quote proc-name) proc-rep known-total-env))
28 (error "procedure could not be determined to be total")))
29 (set! known-total-env
30 (extend-env known-total-env (quote proc-name) 'total-proc))
31 (set! proc-name lambda-expr))))))
32
33 (define-syntax definerec-total
34 (syntax-rules ()
35 ((definerec-total ((name val) ...))
36 (definerec-total "split" (name ...) (val ...) () ()))
37 ((definerec-total "split" (name1 name2 ...) (val1 val2 ...) nacc vacc)
38 (definerec-total "split" (name2 ...) (val2 ...) (name1 . nacc) (val1 . vacc)))
39 ((definerec-total "split" () () names exprs)
40 (begin
41 (cond
42 ((not (procs-total? (quote names) (quote exprs) known-total-env))
43 (error "procedures could not be determined to be total")))
44 (set! known-total-env
45 (names->env (quote names) 'total-proc known-total-env))
46 (definerec-total "define" names exprs)))
47 ((definerec-total "define" (name1 name2 ...) (val1 val2 ...))
48 (begin
49 (define name1 val1)
50 (definerec-total "define" (name2 ...) (val2 ...))))
51 ((definerec-total "define" () ())
52 (display ""))))
+258
-0
canon.scm less more
0 ;
1 ; canon.scm - canonicalization of Scheme procedure S-expressions
2 ; Total Procedures in Scheme, May 2006, Chris Pressey
3 ; For license information, see the file LICENSE in this directory.
4 ;
5
6 (define forbidden-syntax '(
7 set!
8 letrec
9 do
10 delay
11 let-syntax
12 letrec-syntax
13 syntax-rules
14 define
15 define-syntax
16 ))
17
18 ;
19 ; Create the environment that the body of a let* statement would
20 ; be evaluated with.
21 ;
22 (define-total make-let*-env
23 (lambda (names env)
24 (if (acyclic? names)
25 (cond
26 ((null? names)
27 env)
28 (else
29 (let* ((first (car names))
30 (rest (cdr names))
31 (new-env (extend-env env first 'defined)))
32 (make-let*-env rest new-env)))))))
33
34 (definerec-total (
35
36 ;
37 ; Canonicalize the given S-expression representing a Scheme procedre.
38 ; That is, return a new S-exp which is equivalent to the given S-exp,
39 ; but "de-sugared" so that it is simpler and so we can more easily
40 ; work with it during program analysis.
41 ;
42 ; Aborts with an error, as a side-effect, if there is invalid syntax
43 ; in the procedure, that is, syntax which does not appear in the
44 ; subset of Scheme which we can successfully canonicalize.
45 ;
46 (canonicalize
47 (lambda (expr-rep env)
48 (if (acyclic? expr-rep)
49 (cond
50 ((null? expr-rep) ; for totality-checker's benefit
51 expr-rep)
52 ((pair? expr-rep)
53 (cond
54 ;
55 ; If it is defined in the environment, it might be a
56 ; local variable which we are calling, in which case
57 ; we must override the default meaning of the symbol.
58 ; (This code is a copy of the is-call? code below.)
59 ;
60 ((and (symbol? (car expr-rep)) (get-env env (car expr-rep)))
61 (let* ((func-ref-rep (canonicalize (car expr-rep) env))
62 (args-rep (cdr expr-rep))
63 (pair (canonicalize-func-args args-rep env '() '()))
64 (new-bindings (car pair))
65 (new-args (cdr pair))
66 (new-call-rep (cons func-ref-rep new-args)))
67 (cond
68 ((null? expr-rep)
69 expr-rep)
70 ((null? new-bindings)
71 expr-rep)
72 (else
73 (list 'let new-bindings new-call-rep)))))
74 ;
75 ; 'if' with no else-branch is given an explicit undefined else branch.
76 ;
77 ((is-if? expr-rep)
78 (let* ((test-expr (cadr expr-rep)) ; get-test-expr
79 (then-expr (caddr expr-rep))) ; get-then-expr
80 (if (> (length expr-rep) 3)
81 (let* ((else-expr (cadddr expr-rep))) ; get-else-expr
82 (list 'if (canonicalize test-expr env)
83 (canonicalize then-expr env)
84 (canonicalize else-expr env)))
85 (list 'if (canonicalize test-expr env)
86 (canonicalize then-expr env)
87 ''undefined))))
88 ((is-cond? expr-rep)
89 (canonicalize-cond-branches (cdr expr-rep) env)) ; get-cond-branches
90 ;
91 ; XXX TODO: disallow named let
92 ;
93 ((is-let? expr-rep)
94 (let* ((bindings (cadr expr-rep)) ; get-let-bindings
95 (body-rep (cddr expr-rep)) ; get-let-body
96 (names (bindings->names bindings))
97 (new-bindings (canonicalize-bindings bindings env '()))
98 (new-env (extend-env-many env (names->env names 'defined (make-empty-env))))
99 (new-body (canonicalize-begin body-rep new-env)))
100 (list 'let new-bindings new-body)))
101 ((is-let*? expr-rep)
102 (let* ((bindings (cadr expr-rep)) ; get-let-bindings
103 (body (cddr expr-rep)) ; get-let-body
104 (names (bindings->names bindings))
105 (inner-env (make-let*-env names env))
106 (canon-body (canonicalize-begin body inner-env)))
107 (canonicalize-let* bindings canon-body env)))
108 ;
109 ; Canonicalizing a lambda expression doesn't make any significant
110 ; structural changes by itself, but it does modify the environment.
111 ;
112 ((is-lambda? expr-rep)
113 (let* ((args (cadr expr-rep)) ; get-lambda-args
114 (body-rep (cddr expr-rep)) ; get-lambda-body
115 (new-bindings (names->env args 'defined (make-empty-env)))
116 (new-env (extend-env-many env new-bindings))
117 (new-body (canonicalize-begin body-rep new-env)))
118 (list 'lambda args new-body)))
119 ((is-begin? expr-rep)
120 (canonicalize-begin (cdr expr-rep) env)) ; get-begin-list
121 ;
122 ; Evaluation of parameters inside a function call are brought outside the
123 ; function call, i.e. (foo (bar baz)) -> (let ((x (bar baz))) (func x))
124 ; This only brings out nontrivial (non-symbol, int etc) parameters.
125 ;
126 ((is-call? expr-rep)
127 (let* ((func-ref-rep (canonicalize (car expr-rep) env))
128 (args-rep (cdr expr-rep))
129 (pair (canonicalize-func-args args-rep env '() '()))
130 (new-bindings (car pair))
131 (new-args (cdr pair))
132 (new-call-rep (cons func-ref-rep new-args)))
133 (cond
134 ((null? expr-rep)
135 expr-rep)
136 ((null? new-bindings)
137 expr-rep)
138 (else
139 (list 'let new-bindings new-call-rep)))))
140 ((memv (car expr-rep) forbidden-syntax)
141 #f)
142 (else
143 expr-rep)))
144 (else
145 expr-rep)))))
146
147 ;
148 ; 'cond' is transformed into a series of nested 'if's.
149 ;
150 (canonicalize-cond-branches
151 (lambda (branch-reps env)
152 (if (acyclic? branch-reps)
153 (cond
154 ((null? branch-reps)
155 ''undefined)
156 (else
157 (let* ((first-branch (car branch-reps))
158 (rest-of-branches (cdr branch-reps))
159 (first-test (car first-branch))
160 (first-result (cdr first-branch))
161 (canon-result (canonicalize-begin first-result env)))
162 (cond
163 ((eq? first-test 'else)
164 canon-result)
165 (else
166 (list 'if
167 (canonicalize first-test env)
168 canon-result
169 (canonicalize-cond-branches rest-of-branches env))))))))))
170
171 (canonicalize-bindings
172 (lambda (bindings env acc)
173 (if (acyclic? bindings)
174 (cond
175 ((null? bindings)
176 (reverse acc))
177 (else
178 (let* ((binding (car bindings))
179 (rest (cdr bindings))
180 (name (car binding))
181 (value (cadr binding))
182 (new-value (canonicalize value env))
183 (new-binding (list name new-value)))
184 (canonicalize-bindings rest env (cons new-binding acc))))))))
185
186 ;
187 ; 'let*' is transformed into a series of nested 'let's.
188 ; Note that body-rep is given to us pre-canonicalized.
189 ;
190 (canonicalize-let*
191 (lambda (bindings body-rep env)
192 (if (acyclic? bindings)
193 (cond
194 ((null? bindings)
195 body-rep)
196 (else
197 (let* ((binding (car bindings))
198 (rest (cdr bindings))
199 (name (car binding))
200 (value (cadr binding))
201 (canon-val (canonicalize value env))
202 (new-env (extend-env env name '())))
203 (list 'let
204 (list (list name canon-val))
205 (canonicalize-let* rest body-rep env))))))))
206
207 ;
208 ; The list of expressions contained inside a 'begin' expression
209 ; is transformed into a series of nested, two-statement 'begin's.
210 ;
211 (canonicalize-begin
212 (lambda (exprs env)
213 (if (acyclic? exprs)
214 (cond
215 ((null? exprs)
216 ''undefined)
217 ((null? (cdr exprs))
218 (canonicalize (car exprs) env))
219 (else
220 (let* ((first (canonicalize (car exprs) env))
221 (rest (canonicalize-begin (cdr exprs) env)))
222 (list 'begin first rest)))))))
223
224 (canonicalize-func-args
225 (lambda (args env acc-let acc-args)
226 (if (acyclic? args)
227 (cond
228 ((null? args)
229 (cons (reverse acc-let) (reverse acc-args)))
230 ((list? (car args))
231 (let* ((canonicalized-arg (canonicalize (car args) env))
232 (new-name (get-fresh-name env))
233 (new-env (extend-env env new-name '()))
234 (new-acc-let (cons (list new-name canonicalized-arg) acc-let))
235 (new-acc-args (cons new-name acc-args)))
236 (canonicalize-func-args (cdr args) new-env new-acc-let new-acc-args)))
237 (else
238 (canonicalize-func-args (cdr args) env acc-let (cons (car args) acc-args)))))))
239
240 ))
241
242 ;
243 ; Given a list of S-expressions representing Scheme expressions, return
244 ; a corresponding list of canonicalized expressions.
245 ;
246 (define-total canonicalize-all
247 (lambda (expr-reps env acc)
248 (if (acyclic? expr-reps)
249 (cond
250 ((null? expr-reps)
251 (reverse acc))
252 (else
253 (let* ((expr-rep (car expr-reps))
254 (rest (cdr expr-reps))
255 (canon-expr-rep (canonicalize expr-rep env))
256 (new-acc (cons canon-expr-rep acc)))
257 (canonicalize-all rest env new-acc)))))))
+163
-0
crit.scm less more
0 ;
1 ; crit.scm - critical argument locator
2 ; Total Procedures in Scheme, May 2006, Chris Pressey
3 ; For license information, see the file LICENSE in this directory.
4 ;
5
6 ;
7 ; Given an abstract environment and the test expression of an 'if',
8 ; return the environment which should apply to the 'then' expression
9 ; branch of the 'if'. For example, if the test is '(zero? n)', our
10 ; new environment is a copy of the given environment, but with the
11 ; name 'n' now bound to 'crit-nat' because n is available as a critical
12 ; natural number argument inside the 'then' branch of this if expression.
13 ;
14 (define-total make-then-branch-env
15 (lambda (env test-expr-rep)
16 (cond
17 ((is-call? test-expr-rep)
18 (let ((proc-name (car test-expr-rep))
19 (proc-args (cdr test-expr-rep)))
20 (cond
21 ((eq? proc-name 'acyclic?)
22 (extend-env env (car proc-args) 'list))
23 ((and (eq? proc-name '>=) (eq? (cadr proc-args) 0))
24 (extend-env env (car proc-args) 'nat))
25 ((and (eq? proc-name 'zero?) (eq? (get-env env (car proc-args)) 'nat))
26 (extend-env env (car proc-args) 'crit-nat))
27 ((and (eq? proc-name 'null?) (eq? (get-env env (car proc-args)) 'list))
28 (extend-env env (car proc-args) 'crit-list))
29 (else
30 env))))
31 (else
32 env))))
33
34 ;
35 ; 'Update' the env to reflect the information accrued in args,
36 ; after name changes to variables (let).
37 ;
38 ; OTOH, if renaming has taken place, we need to retrieve the
39 ; bindings and re-associate the types with the previous names,
40 ; aka "back propogate" the types.
41 ;
42 ; XXX still TODO?
43 ;
44 (define-total back-propogate-crit
45 (lambda (lower-env upper-env)
46 lower-env))
47
48 (define-total merge-crit-envs
49 (lambda (env1 env2 acc-env)
50 (if (acyclic? env1)
51 (cond
52 ((null? env1)
53 acc-env)
54 (else
55 (let* ((pair (car env1))
56 (rest (cdr env1))
57 (var (car pair))
58 (type1 (cdr pair))
59 (type2 (get-env env2 var)))
60 ;
61 ; Note that this glosses over the possibility that the
62 ; var is 'crit-nat' in one environment and 'crit-list' in
63 ; the other, which, absurd as it is, can happen.
64 ;
65 (cond
66 ((or (eq? type1 'crit-nat) (eq? type2 'crit-nat))
67 (merge-crit-envs rest env2 (extend-env acc-env var 'crit-nat)))
68 ((or (eq? type1 'crit-list) (eq? type2 'crit-list))
69 (merge-crit-envs rest env2 (extend-env acc-env var 'crit-list)))
70 (else
71 (merge-crit-envs rest env2 acc-env)))))))))
72
73 ;
74 ; Given the representation and name of a procedure, find its
75 ; critical arguments. The critical arguments are the arguments
76 ; that take on a predictable final value exactly when the
77 ; procedure returns.
78 ;
79 ; We find critical arguments by first finding critical variables,
80 ; then relating these variables to the arguments they came from.
81 ;
82 ; We find critical variables by creating new environments on
83 ; each branch of a conditional statement, and noticing if a
84 ; variable takes on a final value in any branch that terminates
85 ; (rather than recursing.)
86 ;
87 (define-total find-crit-expr
88 (lambda (expr-rep proc-names env)
89 (if (acyclic? expr-rep)
90 (cond
91 ;
92 ; This branch is used to convince the totality checker that
93 ; the expr-rep data structure really is well-founded, even
94 ; though it will never in practice be taken.
95 ;
96 ((null? expr-rep)
97 env)
98 ((is-let? expr-rep)
99 (let* ((body-rep (caddr expr-rep)) ; get-let-body
100 (in-let-env (find-crit-expr body-rep proc-names env)))
101 (back-propogate-crit in-let-env env)))
102 ;
103 ; A variable is critical if it has a critical type in either environment
104 ; of an if expression.
105 ;
106 ; Note that this is the only place where we extend the
107 ; environment.
108 ;
109 ((is-if? expr-rep)
110 (let* ((test-expr-rep (cadr expr-rep)) ; get-test-expr
111 (then-expr-rep (caddr expr-rep)) ; get-then-expr
112 (else-expr-rep (cadddr expr-rep)) ; get-else-expr
113 (then-env (make-then-branch-env env test-expr-rep))
114 (in-then-env (find-crit-expr then-expr-rep proc-names then-env))
115 (in-else-env (find-crit-expr else-expr-rep proc-names env))
116 (merged-env (merge-crit-envs in-then-env in-else-env '())))
117 merged-env))
118 ;
119 ; When we see a 'begin', we know that only the second expression
120 ; can establish critical variables, since the first cannot return.
121 ;
122 ((is-begin? expr-rep)
123 (let* ((sub-expr (caddr expr-rep))) ; get=begin-second
124 (find-crit-expr sub-expr proc-names env)))
125 ((is-call? expr-rep)
126 (let* ((called-proc-name (car expr-rep)))
127 (cond
128 ((memv called-proc-name proc-names)
129 ;
130 ; The procedure recursively calls itself here.
131 ; Therefore none of the variables in this branch
132 ; can be critical variables, so return an empty
133 ; environment.
134 ;
135 '())
136 ((not (is-identifier? called-proc-name))
137 '())
138 (else
139 ;
140 ; The procedure terminates non-recursively here,
141 ; therefore some of the variables in this branch
142 ; might be critical variables, so return (i.e.
143 ; endorse) the environment we were given.
144 ;
145 env))))
146 (else
147 ;
148 ; The procedure terminates here too; see above comment.
149 ;
150 env)))))
151
152 ;
153 ; Find the critical arguments of a procedure.
154 ;
155 (define-total find-crit
156 (lambda (expr-rep proc-names)
157 (cond
158 ((is-lambda? expr-rep)
159 (let* ((body (caddr expr-rep))) ; get-canonicalized-lambda-body
160 (find-crit-expr body proc-names '())))
161 (else
162 '()))))
+146
-0
env.scm less more
0 ;
1 ; env.scm - environment support for abstract interpretation
2 ; Total Procedures in Scheme, May 2006, Chris Pressey
3 ; For license information, see the file LICENSE in this directory.
4 ;
5
6 ;
7 ; Each environment associates a name with a type.
8 ;
9 ; For canonicalization, we only need to know if a name has been
10 ; defined at all. In this case, the only type is 'defined'.
11 ; For the termination analysis proper, we need a more refined system:
12 ;
13 ; unknown a variable which we know nothing about.
14 ;
15 ; list a variable that we know to be an acyclic list.
16 ; (true branch of an 'acyclic-list?' test.)
17 ;
18 ; reduced-list cdr of an acylic-list.
19 ;
20 ; null null list.
21 ;
22 ; nat a variable which has tested for positive integerness.
23 ;
24 ; reduced-nat a positive-int that has been decremented.
25 ;
26 ; zero a variable that we know must be zero (true branch
27 ; of a 'zero?' test.)
28 ;
29 ; total-proc a procedure that we know always terminates.
30 ;
31
32
33 (define-total make-empty-env
34 (lambda ()
35 '()))
36
37 (define-total extend-env
38 (lambda (env name value)
39 (cons (cons name value) env)))
40
41 (define-total names->env
42 (lambda (names value env)
43 (if (acyclic? names)
44 (cond
45 ((null? names)
46 env)
47 (else
48 (names->env (cdr names) value (extend-env env (car names) value)))))))
49
50 (define-total extend-env-many
51 (lambda (env list-of-bindings)
52 (append list-of-bindings env)))
53
54 (define-total get-env
55 (lambda (env name)
56 (let* ((result (assq name env)))
57 (cond
58 (result
59 (cdr result))
60 (else
61 #f)))))
62
63 (define-total get-fresher-name
64 (lambda (env acc)
65 (if (acyclic? env)
66 (cond
67 ((null? env)
68 acc)
69 ((get-env env acc)
70 (get-fresher-name (cdr env) (string->symbol
71 (string-append (symbol->string acc) (symbol->string (caar env))))))
72 (else
73 acc)))))
74
75 (define-total get-fresh-name
76 (lambda (env)
77 (get-fresher-name env 'z)))
78
79 ; Entries in env2 override those in env1.
80 (define-total merge-envs
81 (lambda (env1 env2)
82 (if (acyclic? env1)
83 (cond
84 ((null? env1)
85 env2)
86 ((get-env env2 (caar env1))
87 (merge-envs (cdr env1) env2))
88 (else
89 (merge-envs (cdr env1) (cons (car env1) env2)))))))
90
91 (define-total display-env-loop
92 (lambda (env)
93 (if (acyclic? env)
94 (cond
95 ((null? env)
96 'ok)
97 (else
98 (let* ((pair (car env))
99 (key (car pair))
100 (val (cdr pair)))
101 (if (not (get-env orig-known-total-env key))
102 (begin (display key) (display " -> ") (display val) (display "; "))
103 'whatever)
104 (display-env-loop (cdr env))))))))
105
106 (define-total display-env
107 (lambda (env)
108 (display "{")
109 (display-env-loop env)
110 (display "}")))
111
112 ;
113 ; There is only one type complex enough to require helper functions -
114 ; the type of the procedure currently being analyzed, called a "this".
115 ; A this tracks the types of all of its arguments.
116 ;
117
118 (define-total is-this?
119 (lambda (type)
120 (and (pair? type) (eq? (car type) 'this))))
121
122 (define-total this-args
123 (lambda (type)
124 (cdr type)))
125
126 (define-total all-unknown?
127 (lambda (types)
128 (if (acyclic? types)
129 (cond
130 ((null? types)
131 #t)
132 (else
133 (cond
134 ((eq? (car types) 'unknown)
135 (all-unknown? (cdr types)))
136 (else
137 #f)))))))
138
139 ;
140 ; A type is "recursable" if it is a this and at least one of the types
141 ; of its arguments is not "unknown".
142 ;
143 (define-total is-recursable?
144 (lambda (type)
145 (and (is-this? type) (not (all-unknown? (this-args type))))))
+102
-0
std.scm less more
0 ;
1 ; std.scm - standard environment of known-total procedures.
2 ; Total Procedures in Scheme, May 2006, Chris Pressey
3 ; For license information, see the file LICENSE in this directory.
4 ;
5
6 ;
7 ; These are mostly Scheme builtins.
8 ;
9 ; We make some assumptions about this list. The basic assumption
10 ; is that all of these builtins are implemented correctly and are
11 ; thus guaranteed to return. Another assumption is that those
12 ; builtins that operate on lists (for example, 'length', 'memv',
13 ; 'list->vector', etc) always return, even when given a cyclic list
14 ; (even though R5RS does not specify this behaviour.) Should this
15 ; assumption fail for some given implementation of some of these
16 ; builtins, those builtins should be removed from this list, and
17 ; if those builtins are used in the totality checker itself
18 ; (notably 'reverse' is used in several places,) "hand-rolled"
19 ; versions that are guaranteed to terminate should be substituted.
20 ;
21 ; Note that this file should NOT be reloaded during bootstrapping.
22 ;
23 ; It might be nice if these were local to define-total, but
24 ; it's more useful for testing purposes if we can access them
25 ; from outside there too.
26 ;
27 (define orig-known-total-env
28 (map (lambda (name) (cons name 'total-proc)) '(
29 eqv? eq? equal?
30 number? complex? real? rational? integer?
31 exact? inexact?
32 = < > <= >=
33 zero? positive? negative? odd? even? max min
34 + * - /
35 abs quotient remainder modulo
36 gcd lcm
37 numerator denominator
38 floor ceiling truncate round
39 rationalize
40 exp log sin cos tan asin acos atan
41 sqrt expt
42 make-rectangular make-polar real-part imag-part magnitude angle
43 exact->inexact inexact->exact
44 number->string string->number
45 not boolean? and or
46 pair? cons car cdr
47 ;set-car! set-cdr! ; no side effects
48 caar cadr cdar cddr
49 caaar caadr cadar caddr cdaar cdadr cddar cdddr
50 caaaar caaadr caadar caaddr cadaar cadadr caddar cadddr
51 cdaaar cdaadr cdadar cdaddr cddaar cddadr cdddar cddddr
52 null? list?
53 list length append reverse ; NOTE: can depend on implementation
54 list-tail list-ref ; NOTE: can depend on implementation
55 memq memv member ; NOTE: can depend on implementation
56 assq assv assoc ; NOTE: can depend on implementation
57 symbol? symbol->string string->symbol
58 char?
59 char=? char<? char>? char<=? char>=?
60 char-ci=? char-ci<? char-ci>? char-ci<=? char-ci>=?
61 char-alphabetic? char-numeric? char-whitespace?
62 char-upper-case? char-lower-case?
63 char->integer integer->char
64 char-upcase char-downcase
65 string? make-string string string-length string-ref
66 ;string-set! ; no side effects
67 string=? string-ci=?
68 string<? string>? string<=? string>=?
69 string-ci<? string-ci>? string-ci<=? string-ci>=?
70 substring string-append
71 string->list list->string
72 string-copy
73 ;string-fill! ; no side effects
74 vector? make-vector vector vector-length vector-ref
75 ;vector-set! ; no side effects
76 vector->list list->vector
77 ;vector-fill! ; no side effects
78 procedure?
79 ;apply ; The following builtins call for
80 ;map for-each ; more complex flow analysis than
81 ;force ; our analyzer does at present.
82 ;call-with-current-continuation values call-with-values dynamic-wind
83 ;eval scheme-report-environment null-environment interaction-environment
84 ;call-with-input-file call-with-output-file
85 input-port? output-port?
86 current-input-port current-output-port
87 ;with-input-from-file with-output-to-file
88 ;open-input-file open-output-file
89 ;close-input-port close-output-port
90 read read-char peek-char
91 eof-object? char-ready?
92 write display newline write-char
93 ;load transcript-on transcript-off
94 acyclic? ; part of the analyzer
95 )))
96
97 ;
98 ; This variable changes over time, as define-total and definerec-total
99 ; 'learn' about new user-defined procedures which are also total.
100 ;
101 (define known-total-env orig-known-total-env)
+284
-0
test.scm less more
0 ;
1 ; test.scm - simple test suite
2 ; Total Procedures in Scheme, May 2006, Chris Pressey
3 ; For license information, see the file LICENSE in this directory.
4 ;
5
6 (load "std.scm")
7 (load "boot1.scm")
8 (load "util.scm")
9 (load "env.scm")
10 (load "canon.scm")
11 (load "crit.scm")
12 (load "total.scm")
13
14 ;
15 ; Definitions (as S-expressions) of procedures that we will test.
16 ;
17
18 (define simple-proc
19 '(lambda (a b)
20 (if (> a b) (* 2 a) (* 3 b)))
21 )
22
23 (define unsafe-fac-proc
24 '(lambda (n)
25 (cond
26 ((zero? n)
27 1)
28 (else
29 (* n (fac (- n 1))))))
30 )
31
32 (define fac-proc
33 '(lambda (n)
34 (if (>= n 0)
35 (cond
36 ((zero? n)
37 1)
38 (else
39 (* n (fac (- n 1)))))
40 0))
41 )
42
43 (define unsafe-anbncn-proc
44 '(lambda (l k)
45 (cond
46 ((null? l)
47 (eq? k 0))
48 ((eq? (car l) 'a)
49 (anbncn (cdr l) (+ k 1)))
50 ((eq? (car l) 'b)
51 (anbncn (cdr l) (+ k 1)))
52 ((eq? (car l) 'c)
53 (anbncn (cdr l) (- k 2)))
54 (else
55 (anbncn (cdr l) k))))
56 )
57
58 (define anbncn-proc
59 '(lambda (l k)
60 (if (acyclic? l)
61 (cond
62 ((null? l)
63 (eq? k 0))
64 ((eq? (car l) 'a)
65 (anbncn (cdr l) (+ k 1)))
66 ((eq? (car l) 'b)
67 (anbncn (cdr l) (+ k 1)))
68 ((eq? (car l) 'c)
69 (anbncn (cdr l) (- k 2)))
70 (else
71 (anbncn (cdr l) k)))))
72 )
73
74 (define ack-proc
75 '(lambda (x y)
76 (if (and (>= x 0) (>= y 0))
77 (cond
78 ((zero? x)
79 (+ y 1))
80 ((zero? y)
81 (ack (- x 1) 1))
82 (else
83 (ack (- x 1) (ack x (- y 1)))))))
84 )
85
86 (define ever1-proc
87 '(lambda (x)
88 (cond
89 ((eq? x 10000)
90 x)
91 (else
92 (ever1 (+ x 1)))))
93 )
94
95 ;
96 ; The tests proper.
97 ;
98
99 ;; Tests for acyclicity.
100
101 (test acyclic-1
102 (acyclic? '(1 2 3 4 5))
103 #t
104 )
105
106 (test acyclic-2
107 (acyclic? '(1 2 (a b c) 3 4 5))
108 #t
109 )
110
111 (test acyclic-3
112 (let* ((tail '(5 . TBA))
113 (lst (append '(1 2 3 4) tail)))
114 (set-cdr! tail lst)
115 (acyclic? lst))
116 #f
117 )
118
119 (test acyclic-4
120 (let* ((tail '(5 . TBA))
121 (inner-lst (append '(1 2 3 4) tail))
122 (outer-lst (list 'a 'b inner-lst 'c 'd)))
123 (set-cdr! tail inner-lst)
124 (acyclic? outer-lst))
125 #f
126 )
127
128 ;; Tests for canonicalization.
129
130 (test canonicalize-simple
131 (canonicalize simple-proc '())
132 '(lambda (a b)
133 (if (> a b)
134 (* 2 a)
135 (* 3 b)))
136 )
137
138 (test canonicalize-fac
139 (canonicalize fac-proc '())
140 '(lambda (n)
141 (if (>= n 0)
142 (if (zero? n)
143 1
144 (let ((z
145 (let ((z (- n 1))) (fac z))
146 ))
147 (* n z)))
148 0))
149 )
150
151 (test canonicalize-ack
152 (canonicalize ack-proc '())
153 '(lambda (x y)
154 (if (let ((z (>= x 0)) (zz (>= y 0))) (and z zz))
155 (if (zero? x)
156 (+ y 1)
157 (if (zero? y)
158 (let ((z (- x 1)))
159 (ack z 1))
160 (let ((z (- x 1))
161 (zz (let ((zz (- y 1))) (ack x zz))))
162 (ack z zz))))
163 'undefined))
164 )
165
166 (test canonicalize-let*
167 (canonicalize
168 '(lambda (x y)
169 (let* ((p (+ x y))
170 (q (* p p)))
171 (display q)))
172 '())
173 '(lambda (x y)
174 (let ((p (+ x y)))
175 (let ((q (* p p)))
176 (display q))))
177 )
178
179 ;; Tests for finding critical arguments.
180
181 (test crit-args-simple
182 (find-crit (canonicalize simple-proc '()) '(simple))
183 '()
184 )
185
186 (test crit-args-fac
187 (find-crit (canonicalize fac-proc '()) '(fac))
188 '((n . crit-nat))
189 )
190
191 (test crit-args-unsafe-fac
192 (find-crit (canonicalize unsafe-fac-proc '()) '(fac))
193 '()
194 )
195
196 (test crit-args-anbncn
197 (find-crit (canonicalize anbncn-proc '()) '(anbncn))
198 '((l . crit-list))
199 )
200
201 (test crit-args-ack
202 (find-crit (canonicalize ack-proc '()) '(ack))
203 '()
204 )
205
206 (test crit-args-ever1
207 (find-crit (canonicalize ever1-proc '()) '(ever1))
208 '()
209 )
210
211 ;; Tests for determining totality.
212
213 (test proc-total-simple
214 (proc-total? 'simple (canonicalize simple-proc '()) known-total-env)
215 #t
216 )
217
218 (test proc-total-fac
219 (proc-total? 'fac (canonicalize fac-proc '()) known-total-env)
220 #t
221 )
222
223 (test proc-total-unsafe-fac
224 (proc-total? 'fac (canonicalize unsafe-fac-proc '()) known-total-env)
225 #f
226 )
227
228 (test proc-total-anbncn
229 (proc-total? 'anbncn (canonicalize anbncn-proc '()) known-total-env)
230 #t
231 )
232
233 (test proc-total-ack
234 (proc-total? 'ack (canonicalize ack-proc '()) known-total-env)
235 #f
236 )
237
238 (test proc-total-ever1
239 (proc-total? 'ever1 (canonicalize ever1-proc '()) known-total-env)
240 #f
241 )
242
243 ;; Tests for determining totality of mutually-recursive procedures.
244
245 (test mutrec-total-even
246 (procs-total? '(even odd) (list
247 (canonicalize '(lambda (x)
248 (if (>= x 0)
249 (cond
250 ((zero? x)
251 1)
252 (else
253 (odd (- x 1)))))) '())
254 (canonicalize '(lambda (x)
255 (if (>= x 0)
256 (cond
257 ((zero? x)
258 0)
259 (else
260 (odd (- x 1)))))) '()))
261 known-total-env)
262 #t
263 )
264
265 (test mutrec-total-bad
266 (procs-total? '(foo bar) (list
267 (canonicalize '(lambda (x y)
268 (if (acyclic? x)
269 (cond
270 ((null? x)
271 (bar '(1 2 3 4 5) y))
272 (else
273 (foo (cdr x) (+ y 1)))))) '())
274 (canonicalize '(lambda (x y)
275 (if (acyclic? x)
276 (cond
277 ((null? x)
278 (foo '(1 2 3 4 5) y))
279 (else
280 (bar (cdr x) (+ y 1)))))) '()))
281 known-total-env)
282 #f
283 )
+363
-0
total.scm less more
0 ;
1 ; total.scm - kernel of totality checker
2 ; Total Procedures in Scheme, May 2006, Chris Pressey
3 ; For license information, see the file LICENSE in this directory.
4 ;
5
6 ;
7 ; Create initial environment from the list of arguments of the lambda
8 ; expression and from the environment of previously gathered critical
9 ; arguments. Each argument which is found in the critical arguments
10 ; gets a type apropos to its critical nature; arguments that are not
11 ; found in the critical argument environment get the type 'unknown'.
12 ;
13 (define-total make-initial-args
14 (lambda (formals crit-args env)
15 (if (acyclic? formals)
16 (cond
17 ((null? formals)
18 env)
19 (else
20 (let* ((formal (car formals))
21 (rest (cdr formals))
22 (type (get-env crit-args formal)))
23 (cond
24 (type
25 (make-initial-args rest crit-args (extend-env env formal type)))
26 (else
27 (make-initial-args rest crit-args (extend-env env formal 'unknown))))))))))
28
29 ;
30 ; Create a new 'this' type.
31 ;
32 (define-total make-this
33 (lambda (formals crit-args acc)
34 (if (acyclic? formals)
35 (cond
36 ((null? formals)
37 (cons 'this (reverse acc)))
38 (else
39 (let* ((formal (car formals))
40 (rest (cdr formals))
41 (this-arg (or (get-env crit-args formal) 'unknown)))
42 (make-this rest crit-args (cons this-arg acc))))))))
43
44 ;
45 ; Create a new environment that is suited for a base for the
46 ; environments of a set of mutually recursive procedures.
47 ; This environment has one 'this' in it for each procedure.
48 ; These procedures can call each other, and so must be informed
49 ; of each others' critical arguments.
50 ;
51 (define-total make-mutual-env
52 (lambda (proc-names expr-reps env)
53 (if (acyclic? proc-names)
54 (cond
55 ((null? proc-names)
56 env)
57 (else
58 (let* ((proc-name (car proc-names))
59 (expr-rep (car expr-reps))
60 (formals (cadr expr-rep)) ; get-lambda-args
61 (crit-args (find-crit expr-rep proc-names))
62 (this (make-this formals crit-args '()))
63 (new-env (extend-env env proc-name this)))
64 (make-mutual-env (cdr proc-names) (cdr expr-reps) new-env)))))))
65
66 ;
67 ; A list of built-in functions that, when applied to an acyclic list
68 ; (list or reduced-list type) always result in a reduced-list.
69 ;
70 (define reducing-procs '(
71 car
72 cdr
73 caar
74 cadr
75 cdar
76 cddr
77 caaar
78 caadr
79 cadar
80 caddr
81 cdaar
82 cdadr
83 cddar
84 cdddr
85 caaaar
86 caaadr
87 caadar
88 caaddr
89 cadaar
90 cadadr
91 caddar
92 cadddr
93 cdaaar
94 cdaadr
95 cdadar
96 cdaddr
97 cddaar
98 cddadr
99 cdddar
100 cddddr
101 ))
102
103 ;
104 ; Determine the type of an expression, with respect to totality analysis.
105 ;
106 ; If the expression is (- foo 1) where foo is a critical natural number,
107 ; the type is a reduced natural number.
108 ;
109 ; If the expression is (cdr foo) where foo is a critical list, the
110 ; type is a reduced list.
111 ;
112 (define-total get-expr-type
113 (lambda (expr-rep env)
114 (cond
115 ((is-call? expr-rep)
116 (let* ((proc-name (car expr-rep))
117 (proc-args (cdr expr-rep))
118 (proc-type (get-env env proc-name)))
119 (cond
120 ((eq? proc-name '-)
121 (cond
122 ((and (eq? (get-env env (car proc-args)) 'crit-nat)
123 (eq? (cadr proc-args) 1))
124 'reduced-nat)
125 (else
126 'unknown)))
127 ((memv proc-name reducing-procs)
128 (cond
129 ((or (eq? (get-env env (car proc-args)) 'crit-list)
130 (eq? (get-env env (car proc-args)) 'reduced-list))
131 'reduced-list)
132 (else
133 'unknown)))
134 (else
135 'unknown))))
136 (else
137 'unknown))))
138
139 ;
140 ; When encountering a self-recursive call, check that each passed
141 ; argument coincides with an identified critical argument.
142 ;
143 (define-total check-recurse-args
144 (lambda (actuals formal-types env)
145 (if (acyclic? actuals)
146 (cond
147 ((null? actuals)
148 #t)
149 (else
150 (let* ((actual (car actuals))
151 (actual-type (get-env env actual))
152 (formal-type (car formal-types)))
153 (cond
154 ((and (eq? formal-type 'crit-nat) (not (eq? actual-type 'reduced-nat)))
155 #f)
156 ((and (eq? formal-type 'crit-list) (not (eq? actual-type 'reduced-list)))
157 #f)
158 (else
159 (check-recurse-args (cdr actuals) (cdr formal-types) env)))))))))
160
161 ;
162 ; Create a new abstract environment from the existing one, in the context
163 ; of the abstract execution of the body of the let.
164 ;
165 (define-total make-let-env
166 (lambda (names vals orig-env new-env)
167 (if (acyclic? names)
168 (cond
169 ((null? names)
170 (merge-envs orig-env new-env))
171 (else
172 (let* ((first-name (car names))
173 (rest-names (cdr names))
174 (first-val (car vals))
175 (rest-vals (cdr vals))
176 (first-type (get-expr-type first-val orig-env))
177 (new-env (extend-env new-env first-name first-type)))
178 (cond
179 (first-type
180 (make-let-env rest-names rest-vals orig-env new-env))
181 (else
182 #f))))))))
183
184 (definerec-total (
185
186 ;
187 ; Determine if all bindings in a let-expression are total.
188 ;
189 (bindings-total?
190 (lambda (bindings env)
191 (if (acyclic? bindings)
192 (cond
193 ((null? bindings)
194 #t)
195 (else
196 (let* ((binding (car bindings))
197 (rest (cdr bindings))
198 (name (car binding))
199 (val (cadr binding)))
200 (cond
201 ((expr-total? val env)
202 (bindings-total? rest env))
203 (else
204 #f))))))))
205
206 ;
207 ; Given a canonicalized representation of an expression and a type
208 ; environment, return #t if we can establish that this expression is total
209 ; (always terminates for any input,) or #f if we cannot establish that.
210 ;
211 (expr-total?
212 (lambda (expr-rep env)
213 (if (acyclic? expr-rep)
214 (cond
215 ;
216 ; Branch never taken but convinces analysis that we're total.
217 ;
218 ((null? expr-rep)
219 #t)
220 ;
221 ; a) If we see a 'let', we abstractly evaluate each of its
222 ; initial values in the current environment; then we
223 ; create a new environment where each name is bound to its
224 ; newly associated (abstract) value, and abstractly evaluate
225 ; the body in the new environment.
226 ;
227 ((is-let? expr-rep)
228 (let* ((bindings (cadr expr-rep))
229 (names (bindings->names bindings))
230 (vals (bindings->values bindings))
231 (body-rep (caddr expr-rep))
232 (new-env (make-let-env names vals env '())))
233 (cond
234 (new-env
235 (and (bindings-total? bindings env)
236 (expr-total? body-rep new-env)))
237 (else
238 (display expr-rep)
239 #f))))
240 ;
241 ; b) If we see an 'if', we abstractly evaluate the test
242 ; and both branches; the procedure is only total if
243 ; all of these are total.
244 ;
245 ((is-if? expr-rep)
246 (let* ((test-expr-rep (cadr expr-rep)) ; get-test-expr
247 (then-expr-rep (caddr expr-rep)) ; get-then-expr
248 (else-expr-rep (cadddr expr-rep)) ; get-else-expr
249 (test-total (expr-total? test-expr-rep env))
250 (then-total (expr-total? then-expr-rep env))
251 (else-total (expr-total? else-expr-rep env)))
252 (and test-total then-total else-total)))
253 ;
254 ; c) A sequence is only total if all of its constituent
255 ; expressions are total.
256 ;
257 ((is-begin? expr-rep)
258 (let* ((first-expr (cadr expr-rep)) ; get-begin-first
259 (second-expr (caddr expr-rep))) ; get-begin-second
260 (and (expr-total? first-expr env)
261 (expr-total? second-expr env))))
262 ;
263 ; d) If we see a call to a procedure, we insist that the
264 ; called procedure must be total as well. There are three
265 ; sub-cases to consider here:
266 ;
267 ((is-call? expr-rep)
268 (let* ((proc-name (car expr-rep))
269 (proc-type (get-env env proc-name))
270 (proc-args (cdr expr-rep)))
271 (cond
272 ;
273 ; d.1) It's a call to a function that we already know is total.
274 ;
275 ((eq? proc-type 'total-proc)
276 #t)
277 ;
278 ; d.2) It's a recursive call - either self-recursive or
279 ; to one of any number of mutually recursive procedures.
280 ; In either case, we must check that the arguments being
281 ; passed to the critical arguments of the procedure are
282 ; those that monotonically decrease.
283 ;
284 ((is-recursable? proc-type)
285 (check-recurse-args proc-args (this-args proc-type) env))
286 ;
287 ; d.3) It's a call to a function that we know nothing about.
288 ; Perhaps it is an external function which was not
289 ; given in the list of known-total functions, or perhaps
290 ; it was passed to this function as a parameter. Either
291 ; way, because of this call, we must assume that our
292 ; function might not be total.
293 ;
294 (else
295 #f))))
296 ;
297 ; e) Otherwise, the expression is an atom, number, lambda, or
298 ; other primitive, and as such, is certainly total.
299 ;
300 (else
301 #t)))))
302
303 ))
304
305 ;
306 ; Given the name of a procedure, a canonicalized, syntax-checked S-expression
307 ; representing that procedure, and a type environment, return #t if we can
308 ; establish that this procedure is total (always terminates for any input,)
309 ; or #f if we cannot establish that.
310 ;
311 ; We create a new environment from the given environment, which we use while
312 ; checking the representation of the procedure. In this new environment,
313 ; each of the arguments of the procedure is associated with its type, and
314 ; the name of the procedure is associated with a 'this' type, which knows
315 ; the types that each of the arguments should be.
316 ;
317 (define-total proc-total?
318 (lambda (proc-name expr-rep env)
319 (cond
320 ((is-lambda? expr-rep)
321 (let* ((crit-args (find-crit expr-rep (list proc-name)))
322 (body-rep (caddr expr-rep)) ; get-canonicalized-lambda-body
323 (formals (cadr expr-rep)) ; get-lambda-args
324 (inner-env (make-initial-args formals crit-args '()))
325 (this (make-this formals crit-args '()))
326 (outer-env (extend-env env proc-name this))
327 (new-env (merge-envs outer-env inner-env)))
328 (expr-total? body-rep new-env)))
329 (else
330 #f))))
331
332 ;
333 ; Given a set of (possibly mutually recursive) procedures, determine if
334 ; they are all total. First form the mutual environment, then call
335 ; each-proc-total? on the list of procedures, with that environment.
336 ;
337 (define procs-total?
338 (lambda (proc-names expr-reps env)
339 (let* ((canon-expr-reps (canonicalize-all expr-reps env '()))
340 (mutual-env (make-mutual-env proc-names canon-expr-reps (make-empty-env))))
341 (each-proc-total? proc-names canon-expr-reps (merge-envs env mutual-env)))))
342
343 ;
344 ; Do the actual work required by procs-total?.
345 ;
346 (define-total each-proc-total?
347 (lambda (proc-names expr-reps env)
348 (if (acyclic? expr-reps)
349 (cond
350 ((null? expr-reps)
351 #t)
352 (else
353 (let* ((proc-name (car proc-names))
354 (expr-rep (car expr-reps))
355 (body-rep (caddr expr-rep)) ; get-canonicalized-lambda-body
356 (formals (cadr expr-rep)) ; get-lambda-args
357 (crit-args (find-crit expr-rep proc-names))
358 (inner-env (make-initial-args formals crit-args '()))
359 (new-env (merge-envs env inner-env)))
360 (and
361 (expr-total? body-rep new-env)
362 (each-proc-total? (cdr proc-names) (cdr expr-reps) env))))))))
+129
-0
util.scm less more
0 ;
1 ; util.scm - miscellaneous utility procedures
2 ; Total Procedures in Scheme, May 2006, Chris Pressey
3 ; For license information, see the file LICENSE in this directory.
4 ;
5
6 ;
7 ; Determine if a Scheme datum is acyclic.
8 ;
9 (define acyclic?
10 (lambda (pair)
11 (acyclic-test pair '())))
12
13 (define acyclic-test
14 (lambda (pair acc)
15 (cond
16 ((not (pair? pair))
17 #t)
18 ((memq pair acc)
19 #f)
20 (else
21 (let ((fst (car pair))
22 (snd (cdr pair))
23 (new-acc (cons pair acc)))
24 (and (acyclic-test fst new-acc) (acyclic-test snd new-acc)))))))
25
26 ;
27 ; XXX explain and/or borrow eopl:error
28 ;
29 (define-total error
30 (lambda (msg)
31 (display msg) (newline)
32 (read '())))
33
34 ;
35 ; Test case for test suite.
36 ;
37 (define-syntax test
38 (syntax-rules ()
39 ((test test-name expr expected)
40 (begin
41 (display "Running test: ") (display (quote test-name)) (display "... ")
42 (let ((result expr))
43 (cond
44 ((equal? result expected)
45 (display "passed.") (newline))
46 (else
47 (display "FAILED!") (newline)
48 (display "Expected: ") (display expected) (newline)
49 (display "Actual: ") (display result) (newline))))))))
50
51 ;
52 ; XXX there may be a problem doing NON-TAIL (self-)recursion, check it out.
53 ;
54 (define-total bindings->names
55 (lambda (bindings)
56 (if (acyclic? bindings)
57 (cond
58 ((null? bindings)
59 '())
60 (else
61 (let* ((binding (car bindings))
62 (rest (cdr bindings))
63 (name (car binding)))
64 (cons name (bindings->names rest))))))))
65
66 (define-total bindings->values
67 (lambda (bindings)
68 (if (acyclic? bindings)
69 (cond
70 ((null? bindings)
71 '())
72 (else
73 (let* ((binding (car bindings))
74 (rest (cdr bindings))
75 (value (cadr binding)))
76 (cons value (bindings->values rest))))))))
77
78 (define-total is-lambda?
79 (lambda (expr-rep)
80 (and
81 (pair? expr-rep)
82 (eq? 'lambda (car expr-rep)))))
83
84 (define-total is-let?
85 (lambda (expr-rep)
86 (and
87 (pair? expr-rep)
88 (eq? 'let (car expr-rep)))))
89
90 (define-total is-let*?
91 (lambda (expr-rep)
92 (and
93 (pair? expr-rep)
94 (eq? 'let* (car expr-rep)))))
95
96 (define-total is-if?
97 (lambda (expr-rep)
98 (and
99 (pair? expr-rep)
100 (eq? 'if (car expr-rep)))))
101
102 (define-total is-cond?
103 (lambda (expr-rep)
104 (and
105 (pair? expr-rep)
106 (eq? 'cond (car expr-rep)))))
107
108 (define-total is-begin?
109 (lambda (expr-rep)
110 (and
111 (pair? expr-rep)
112 (eq? 'begin (car expr-rep)))))
113
114 (define-total is-call?
115 (lambda (expr-rep)
116 (and
117 (pair? expr-rep)
118 (not (eq? (car expr-rep) 'quote))))) ;... and all others
119
120 (define-total is-identifier?
121 (lambda (expr-rep)
122 (symbol? expr-rep)))
123
124 (define-total is-quote?
125 (lambda (expr-rep)
126 (and
127 (pair? expr-rep)
128 (eq? 'quote (car expr-rep)))))