Commits

catseye  committed 675d3fa

Initial import of TPiS version 1.0 revision 2006.0528.

  • Participants
  • Tags rel_1_0_2006_0528

Comments (0)

Files changed (12)

+Copyright (c)2006 Chris Pressey.  All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notices, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notices, this list of conditions, and the following disclaimer in
+   the documentation and/or other materials provided with the
+   distribution.
+3. Neither the names of the copyright holders nor the names of their
+   contributors may be used to endorse or promote products derived
+   from this software without specific prior written permission. 
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
+FOR A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE
+COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
+;
+; boot.scm - bootstrap driver
+; Total Procedures in Scheme, May 2006, Chris Pressey
+; For license information, see the file LICENSE in this directory.
+;
+
+;
+; Bootstrapping process for asserting that the totality checker
+; is itself total.
+;
+(load "std.scm")
+
+(load "boot1.scm")
+
+(load "util.scm")
+(load "env.scm")
+(load "canon.scm")
+(load "crit.scm")
+(load "total.scm")
+
+(display "Re-loading with real definition of define-total") (newline)
+(load "boot2.scm")
+
+(load "util.scm")
+(load "env.scm")
+(load "canon.scm")
+(load "crit.scm")
+(load "total.scm")
+
+(load "boot3.scm")
+
+;; Define-total.
+
+(define-total fac
+  (lambda (n)
+    (if (>= n 0)
+      (cond
+        ((zero? n)
+          1)
+        (else
+          (* n (fac (- n 1))))))))
+;
+; This should be an error.
+;
+
+;(define-total ever1
+;  (lambda (x)
+;     (cond
+;       ((eq? x 10000)
+;         x)
+;       (else
+;         (ever1 (+ x 1))))))
+
+(display (fac 5)) (newline)
+;
+; boot1.scm - first stage bootstrap for define[rec]-total
+; Total Procedures in Scheme, May 2006, Chris Pressey
+; For license information, see the file LICENSE in this directory.
+;
+
+;
+; These macros are used in the first stage of bootstrapping
+; to provide "reasonable" semantics for define-total before
+; total procedure checking is actually defined.  i.e. it
+; allows the procedure to be defined, without actually checking
+; it, on the assumption that a future bootstrapping pass will
+; do that.  ("This is Fake D.I.Y.")
+;
+; Note that these do not affect known-total-env in any way.
+;
+(define-syntax define-total
+  (syntax-rules ()
+    ((define-total proc-name lambda-expr)
+      (begin
+        (define proc-name lambda-expr)
+        (display "WARNING: assuming ") (display (quote proc-name)) (display " is total for now, ")
+        (display "please re-load file with real define-total later") (newline)))))
+
+(define-syntax definerec-total
+  (syntax-rules ()
+    ((definerec-total ((name val) ...))
+      (definerec-total "split" (name ...) (val ...) () ()))
+    ((definerec-total "split" (name1 name2 ...) (val1 val2 ...) nacc vacc)
+      (definerec-total "split" (name2 ...) (val2 ...) (name1 . nacc) (val1 . vacc)))
+    ((definerec-total "split" () () nacc vacc)
+      (definerec-total "define" nacc vacc))
+    ((definerec-total "define" (name1 name2 ...) (val1 val2 ...))
+      (begin
+        (define-total name1 val1)
+        (definerec-total "define" (name2 ...) (val2 ...))))
+    ((definerec-total "define" () ())
+      (display ""))))
+;
+; boot2.scm - second stage bootstrap for define[rec]-total
+; Total Procedures in Scheme, May 2006, Chris Pressey
+; For license information, see the file LICENSE in this directory.
+;
+
+;
+; These macros are used in the second stage of bootstrapping, to
+; replace the existing definitions of assumed total procedures with
+; genuinely checked total procedures.
+;
+; Note that these DO affect known-total-env, by adding to it.
+;
+(define-syntax define-total
+  (syntax-rules ()
+    ((define-total proc-name lambda-expr)
+      (begin
+        (display "Redefining ") (display (quote proc-name)) (display " as total procedure") (newline)
+        (let* ((proc-rep (canonicalize (quote lambda-expr) known-total-env)))
+          (cond
+            ((not (proc-total? (quote proc-name) proc-rep known-total-env))
+              (error "procedure could not be determined to be total")))
+        (set! known-total-env
+          (extend-env known-total-env (quote proc-name) 'total-proc))
+        (set! proc-name lambda-expr))))))
+
+(define-syntax definerec-total
+  (syntax-rules ()
+    ((definerec-total ((name val) ...))
+      (definerec-total "split" (name ...) (val ...) () ()))
+    ((definerec-total "split" (name1 name2 ...) (val1 val2 ...) nacc vacc)
+      (definerec-total "split" (name2 ...) (val2 ...) (name1 . nacc) (val1 . vacc)))
+    ((definerec-total "split" () () names exprs)
+      (begin
+        (display "Redefining ") (display (quote names)) (display " as total procedures") (newline)
+        (cond
+          ((not (procs-total? (quote names) (quote exprs) known-total-env))
+            (error "procedures could not be determined to be total")))
+        (set! known-total-env
+          (names->env (quote names) 'total-proc known-total-env))
+        (definerec-total "define" names exprs)))
+    ((definerec-total "define" (name1 name2 ...) (val1 val2 ...))
+      (begin
+        (set! name1 val1)
+        (definerec-total "define" (name2 ...) (val2 ...))))
+    ((definerec-total "define" () ())
+      (display ""))))
+;
+; boot3.scm - third stage bootstrap for define[rec]-total
+; Total Procedures in Scheme, May 2006, Chris Pressey
+; For license information, see the file LICENSE in this directory.
+;
+
+;
+; Given a new procedure name and a procedure (lambda) S-expression, define
+; a new procedure with this name and this lambda, if and only if it can be
+; established that the procedure is total.
+;
+; This has side-effects; an environment of known-total procedures is kept,
+; and if the given procedure turns out to be total, it is added to this.
+;
+; A new environment is set up which initially associates each argument name
+; with a nil value, indicating that we know nothing about it yet.
+;
+; These are the final, "real" definitions of define-total and definerec-total,
+; used in the last stage of the bootstrapping process.
+;
+(define-syntax define-total
+  (syntax-rules ()
+    ((define-total proc-name lambda-expr)
+      (begin
+        (define proc-name 'TBA)
+        (let* ((proc-rep (canonicalize (quote lambda-expr) known-total-env)))
+          (cond
+            ((not (proc-total? (quote proc-name) proc-rep known-total-env))
+              (error "procedure could not be determined to be total")))
+        (set! known-total-env
+          (extend-env known-total-env (quote proc-name) 'total-proc))
+        (set! proc-name lambda-expr))))))
+
+(define-syntax definerec-total
+  (syntax-rules ()
+    ((definerec-total ((name val) ...))
+      (definerec-total "split" (name ...) (val ...) () ()))
+    ((definerec-total "split" (name1 name2 ...) (val1 val2 ...) nacc vacc)
+      (definerec-total "split" (name2 ...) (val2 ...) (name1 . nacc) (val1 . vacc)))
+    ((definerec-total "split" () () names exprs)
+      (begin
+        (cond
+          ((not (procs-total? (quote names) (quote exprs) known-total-env))
+            (error "procedures could not be determined to be total")))
+        (set! known-total-env
+          (names->env (quote names) 'total-proc known-total-env))
+        (definerec-total "define" names exprs)))
+    ((definerec-total "define" (name1 name2 ...) (val1 val2 ...))
+      (begin
+        (define name1 val1)
+        (definerec-total "define" (name2 ...) (val2 ...))))
+    ((definerec-total "define" () ())
+      (display ""))))
+;
+; canon.scm - canonicalization of Scheme procedure S-expressions
+; Total Procedures in Scheme, May 2006, Chris Pressey
+; For license information, see the file LICENSE in this directory.
+;
+
+(define forbidden-syntax '(
+    set!
+    letrec
+    do
+    delay
+    let-syntax
+    letrec-syntax
+    syntax-rules
+    define
+    define-syntax
+  ))
+
+;
+; Create the environment that the body of a let* statement would
+; be evaluated with.
+;
+(define-total make-let*-env
+  (lambda (names env)
+    (if (acyclic? names)
+      (cond
+        ((null? names)
+          env)
+        (else
+          (let* ((first   (car names))
+                 (rest    (cdr names))
+                 (new-env (extend-env env first 'defined)))
+            (make-let*-env rest new-env)))))))
+  
+(definerec-total (
+
+;
+; Canonicalize the given S-expression representing a Scheme procedre.
+; That is, return a new S-exp which is equivalent to the given S-exp,
+; but "de-sugared" so that it is simpler and so we can more easily
+; work with it during program analysis.
+;
+; Aborts with an error, as a side-effect, if there is invalid syntax
+; in the procedure, that is, syntax which does not appear in the
+; subset of Scheme which we can successfully canonicalize.
+;
+(canonicalize
+  (lambda (expr-rep env)
+    (if (acyclic? expr-rep)
+      (cond
+        ((null? expr-rep)  ; for totality-checker's benefit
+          expr-rep)
+        ((pair? expr-rep)
+          (cond
+	    ;
+	    ; If it is defined in the environment, it might be a
+	    ; local variable which we are calling, in which case
+	    ; we must override the default meaning of the symbol.
+	    ; (This code is a copy of the is-call? code below.)
+	    ;
+	    ((and (symbol? (car expr-rep)) (get-env env (car expr-rep)))
+              (let* ((func-ref-rep (canonicalize (car expr-rep) env))
+                     (args-rep     (cdr expr-rep))
+                     (pair         (canonicalize-func-args args-rep env '() '()))
+                     (new-bindings (car pair))
+                     (new-args     (cdr pair))
+                     (new-call-rep (cons func-ref-rep new-args)))
+                (cond
+                  ((null? expr-rep)
+                    expr-rep)
+                  ((null? new-bindings)
+                    expr-rep)
+                  (else
+                    (list 'let new-bindings new-call-rep)))))	      
+            ;
+            ; 'if' with no else-branch is given an explicit undefined else branch.
+            ;
+            ((is-if? expr-rep)
+              (let* ((test-expr (cadr expr-rep))     ; get-test-expr
+                     (then-expr (caddr expr-rep)))   ; get-then-expr
+                (if (> (length expr-rep) 3)
+                    (let* ((else-expr (cadddr expr-rep))) ; get-else-expr
+                      (list 'if (canonicalize test-expr env)
+                                (canonicalize then-expr env)
+                                (canonicalize else-expr env)))
+                    (list 'if (canonicalize test-expr env)
+                              (canonicalize then-expr env)
+                              ''undefined))))
+            ((is-cond? expr-rep)
+              (canonicalize-cond-branches (cdr expr-rep) env)) ; get-cond-branches
+	    ;
+	    ; XXX TODO: disallow named let
+	    ;
+            ((is-let? expr-rep)
+              (let* ((bindings     (cadr expr-rep))  ; get-let-bindings
+                     (body-rep     (cddr expr-rep))  ; get-let-body
+		     (names        (bindings->names bindings))
+                     (new-bindings (canonicalize-bindings bindings env '()))
+                     (new-env      (extend-env-many env (names->env names 'defined (make-empty-env))))
+                     (new-body     (canonicalize-begin body-rep new-env)))
+                (list 'let new-bindings new-body)))
+            ((is-let*? expr-rep)
+              (let* ((bindings   (cadr expr-rep))   ; get-let-bindings
+                     (body       (cddr expr-rep))  ; get-let-body
+                     (names      (bindings->names bindings))
+                     (inner-env  (make-let*-env names env))
+                     (canon-body (canonicalize-begin body inner-env)))
+                (canonicalize-let* bindings canon-body env)))
+            ;
+            ; Canonicalizing a lambda expression doesn't make any significant
+            ; structural changes by itself, but it does modify the environment.
+            ;
+            ((is-lambda? expr-rep)
+              (let* ((args         (cadr expr-rep))           ; get-lambda-args
+                     (body-rep     (cddr expr-rep))           ; get-lambda-body
+                     (new-bindings (names->env args 'defined (make-empty-env)))
+                     (new-env      (extend-env-many env new-bindings))
+                     (new-body     (canonicalize-begin body-rep new-env)))
+                (list 'lambda args new-body)))
+            ((is-begin? expr-rep)
+              (canonicalize-begin (cdr expr-rep) env)) ; get-begin-list
+            ;
+            ; Evaluation of parameters inside a function call are brought outside the
+            ; function call, i.e. (foo (bar baz)) -> (let ((x (bar baz))) (func x))
+            ; This only brings out nontrivial (non-symbol, int etc) parameters.
+            ;
+            ((is-call? expr-rep)
+              (let* ((func-ref-rep (canonicalize (car expr-rep) env))
+                     (args-rep     (cdr expr-rep))
+                     (pair         (canonicalize-func-args args-rep env '() '()))
+                     (new-bindings (car pair))
+                     (new-args     (cdr pair))
+                     (new-call-rep (cons func-ref-rep new-args)))
+                (cond
+                  ((null? expr-rep)
+                    expr-rep)
+                  ((null? new-bindings)
+                    expr-rep)
+                  (else
+                    (list 'let new-bindings new-call-rep)))))
+            ((memv (car expr-rep) forbidden-syntax)
+              #f)
+            (else
+              expr-rep)))
+        (else
+          expr-rep)))))
+
+;
+; 'cond' is transformed into a series of nested 'if's.
+;
+(canonicalize-cond-branches
+  (lambda (branch-reps env)
+    (if (acyclic? branch-reps)
+      (cond
+        ((null? branch-reps)
+          ''undefined)
+        (else
+          (let* ((first-branch     (car branch-reps))
+                 (rest-of-branches (cdr branch-reps))
+                 (first-test       (car first-branch))
+                 (first-result     (cdr first-branch))
+                 (canon-result     (canonicalize-begin first-result env)))
+            (cond
+              ((eq? first-test 'else)
+                canon-result)
+              (else
+                (list 'if
+                      (canonicalize first-test env)
+                      canon-result
+                      (canonicalize-cond-branches rest-of-branches env))))))))))
+
+(canonicalize-bindings
+  (lambda (bindings env acc)
+    (if (acyclic? bindings)
+      (cond
+        ((null? bindings)
+          (reverse acc))
+        (else
+          (let* ((binding     (car bindings))
+                 (rest        (cdr bindings))
+                 (name        (car binding))
+                 (value       (cadr binding))
+                 (new-value   (canonicalize value env))
+                 (new-binding (list name new-value)))
+            (canonicalize-bindings rest env (cons new-binding acc))))))))
+
+;
+; 'let*' is transformed into a series of nested 'let's.
+; Note that body-rep is given to us pre-canonicalized.
+;
+(canonicalize-let*
+  (lambda (bindings body-rep env)
+    (if (acyclic? bindings)
+      (cond
+        ((null? bindings)
+          body-rep)
+        (else
+          (let* ((binding   (car bindings))
+                 (rest      (cdr bindings))
+                 (name      (car binding))
+                 (value     (cadr binding))
+                 (canon-val (canonicalize value env))
+                 (new-env   (extend-env env name '())))
+            (list 'let
+                  (list (list name canon-val))
+                  (canonicalize-let* rest body-rep env))))))))
+
+;
+; The list of expressions contained inside a 'begin' expression
+; is transformed into a series of nested, two-statement 'begin's.
+;
+(canonicalize-begin
+  (lambda (exprs env)
+    (if (acyclic? exprs)
+      (cond
+        ((null? exprs)
+          ''undefined)
+        ((null? (cdr exprs))
+          (canonicalize (car exprs) env))
+        (else
+          (let* ((first (canonicalize (car exprs) env))
+                 (rest  (canonicalize-begin (cdr exprs) env)))
+            (list 'begin first rest)))))))
+
+(canonicalize-func-args
+  (lambda (args env acc-let acc-args)
+    (if (acyclic? args)
+      (cond
+        ((null? args)
+          (cons (reverse acc-let) (reverse acc-args)))
+        ((list? (car args))
+          (let* ((canonicalized-arg (canonicalize (car args) env))
+                 (new-name          (get-fresh-name env))
+                 (new-env           (extend-env env new-name '()))
+                 (new-acc-let       (cons (list new-name canonicalized-arg) acc-let))
+                 (new-acc-args      (cons new-name acc-args)))
+            (canonicalize-func-args (cdr args) new-env new-acc-let new-acc-args)))
+        (else
+          (canonicalize-func-args (cdr args) env acc-let (cons (car args) acc-args)))))))
+
+))
+
+;
+; Given a list of S-expressions representing Scheme expressions, return
+; a corresponding list of canonicalized expressions.
+;
+(define-total canonicalize-all
+  (lambda (expr-reps env acc)
+    (if (acyclic? expr-reps)
+      (cond
+        ((null? expr-reps)
+          (reverse acc))
+        (else
+          (let* ((expr-rep       (car expr-reps))
+                 (rest           (cdr expr-reps))
+                 (canon-expr-rep (canonicalize expr-rep env))
+                 (new-acc        (cons canon-expr-rep acc)))
+            (canonicalize-all rest env new-acc)))))))
+;
+; crit.scm - critical argument locator
+; Total Procedures in Scheme, May 2006, Chris Pressey
+; For license information, see the file LICENSE in this directory.
+;
+
+;
+; Given an abstract environment and the test expression of an 'if',
+; return the environment which should apply to the 'then' expression
+; branch of the 'if'.  For example, if the test is '(zero? n)', our
+; new environment is a copy of the given environment, but with the
+; name 'n' now bound to 'crit-nat' because n is available as a critical
+; natural number argument inside the 'then' branch of this if expression.
+;
+(define-total make-then-branch-env
+  (lambda (env test-expr-rep)
+    (cond
+      ((is-call? test-expr-rep)
+        (let ((proc-name (car test-expr-rep))
+              (proc-args (cdr test-expr-rep)))
+          (cond
+            ((eq? proc-name 'acyclic?)
+              (extend-env env (car proc-args) 'list))
+            ((and (eq? proc-name '>=) (eq? (cadr proc-args) 0))
+              (extend-env env (car proc-args) 'nat))
+            ((and (eq? proc-name 'zero?) (eq? (get-env env (car proc-args)) 'nat))
+              (extend-env env (car proc-args) 'crit-nat))
+            ((and (eq? proc-name 'null?) (eq? (get-env env (car proc-args)) 'list))
+              (extend-env env (car proc-args) 'crit-list))
+            (else
+                env))))
+        (else
+          env))))
+
+;
+; 'Update' the env to reflect the information accrued in args,
+; after name changes to variables (let).
+;
+; OTOH, if renaming has taken place, we need to retrieve the
+; bindings and re-associate the types with the previous names,
+; aka "back propogate" the types.
+;
+; XXX still TODO?
+;
+(define-total back-propogate-crit
+  (lambda (lower-env upper-env)
+    lower-env))
+
+(define-total merge-crit-envs
+  (lambda (env1 env2 acc-env)
+    (if (acyclic? env1)
+      (cond
+        ((null? env1)
+          acc-env)
+        (else
+          (let* ((pair  (car env1))
+                 (rest  (cdr env1))
+                 (var   (car pair))
+                 (type1 (cdr pair))
+                 (type2 (get-env env2 var)))
+            ;
+            ; Note that this glosses over the possibility that the
+            ; var is 'crit-nat' in one environment and 'crit-list' in
+            ; the other, which, absurd as it is, can happen.
+            ;
+            (cond
+              ((or (eq? type1 'crit-nat) (eq? type2 'crit-nat))
+                (merge-crit-envs rest env2 (extend-env acc-env var 'crit-nat)))
+              ((or (eq? type1 'crit-list) (eq? type2 'crit-list))
+                (merge-crit-envs rest env2 (extend-env acc-env var 'crit-list)))
+              (else
+                (merge-crit-envs rest env2 acc-env)))))))))
+
+;
+; Given the representation and name of a procedure, find its
+; critical arguments.  The critical arguments are the arguments
+; that take on a predictable final value exactly when the
+; procedure returns.
+;
+; We find critical arguments by first finding critical variables,
+; then relating these variables to the arguments they came from.
+;
+; We find critical variables by creating new environments on
+; each branch of a conditional statement, and noticing if a
+; variable takes on a final value in any branch that terminates
+; (rather than recursing.)
+;
+(define-total find-crit-expr
+  (lambda (expr-rep proc-names env)
+    (if (acyclic? expr-rep)
+      (cond
+        ;
+        ; This branch is used to convince the totality checker that
+        ; the expr-rep data structure really is well-founded, even
+        ; though it will never in practice be taken.
+        ;
+        ((null? expr-rep)
+          env)
+        ((is-let? expr-rep)
+          (let* ((body-rep   (caddr expr-rep))           ; get-let-body
+                 (in-let-env (find-crit-expr body-rep proc-names env)))
+            (back-propogate-crit in-let-env env)))
+        ;
+        ; A variable is critical if it has a critical type in either environment
+        ; of an if expression.
+        ;
+        ; Note that this is the only place where we extend the
+        ; environment.
+        ;
+        ((is-if? expr-rep)
+          (let* ((test-expr-rep (cadr expr-rep))   ; get-test-expr
+                 (then-expr-rep (caddr expr-rep))  ; get-then-expr
+                 (else-expr-rep (cadddr expr-rep)) ; get-else-expr
+                 (then-env      (make-then-branch-env env test-expr-rep))
+                 (in-then-env   (find-crit-expr then-expr-rep proc-names then-env))
+                 (in-else-env   (find-crit-expr else-expr-rep proc-names env))
+                 (merged-env    (merge-crit-envs in-then-env in-else-env '())))
+            merged-env))
+        ;
+        ; When we see a 'begin', we know that only the second expression
+        ; can establish critical variables, since the first cannot return.
+        ;
+        ((is-begin? expr-rep)
+          (let* ((sub-expr (caddr expr-rep)))  ; get=begin-second
+            (find-crit-expr sub-expr proc-names env)))
+        ((is-call? expr-rep)
+          (let* ((called-proc-name (car expr-rep)))
+            (cond
+              ((memv called-proc-name proc-names)
+                ;
+                ; The procedure recursively calls itself here.
+                ; Therefore none of the variables in this branch
+                ; can be critical variables, so return an empty
+                ; environment.
+                ;
+                '())
+              ((not (is-identifier? called-proc-name))
+                '())
+              (else
+                ;
+                ; The procedure terminates non-recursively here,
+                ; therefore some of the variables in this branch
+                ; might be critical variables, so return (i.e.
+                ; endorse) the environment we were given.
+                ;
+                env))))
+        (else
+          ;
+          ; The procedure terminates here too; see above comment.
+          ;
+          env)))))
+
+;
+; Find the critical arguments of a procedure.
+;
+(define-total find-crit
+  (lambda (expr-rep proc-names)
+    (cond
+      ((is-lambda? expr-rep)
+        (let* ((body (caddr expr-rep))) ; get-canonicalized-lambda-body
+          (find-crit-expr body proc-names '())))
+      (else
+        '()))))
+;
+; env.scm - environment support for abstract interpretation
+; Total Procedures in Scheme, May 2006, Chris Pressey
+; For license information, see the file LICENSE in this directory.
+;
+
+;
+; Each environment associates a name with a type.
+;
+; For canonicalization, we only need to know if a name has been
+; defined at all.  In this case, the only type is 'defined'.
+; For the termination analysis proper, we need a more refined system:
+;
+; unknown         a variable which we know nothing about.
+;
+; list            a variable that we know to be an acyclic list.
+;                 (true branch of an 'acyclic-list?' test.)
+;
+; reduced-list    cdr of an acylic-list.
+;
+; null            null list.
+;
+; nat             a variable which has tested for positive integerness.
+;
+; reduced-nat     a positive-int that has been decremented.
+;
+; zero            a variable that we know must be zero (true branch
+;                 of a 'zero?' test.)
+;
+; total-proc      a procedure that we know always terminates.
+;
+
+
+(define-total make-empty-env
+  (lambda ()
+    '()))
+
+(define-total extend-env
+  (lambda (env name value)
+    (cons (cons name value) env)))
+
+(define-total names->env
+  (lambda (names value env)
+    (if (acyclic? names)
+        (cond
+          ((null? names)
+            env)
+          (else
+            (names->env (cdr names) value (extend-env env (car names) value)))))))
+  
+(define-total extend-env-many
+  (lambda (env list-of-bindings)
+    (append list-of-bindings env)))
+
+(define-total get-env
+  (lambda (env name)
+    (let* ((result (assq name env)))
+      (cond
+        (result
+          (cdr result))
+        (else
+          #f)))))
+
+(define-total get-fresher-name
+  (lambda (env acc)
+    (if (acyclic? env)
+      (cond
+        ((null? env)
+          acc)
+        ((get-env env acc)
+          (get-fresher-name (cdr env) (string->symbol
+              (string-append (symbol->string acc) (symbol->string (caar env))))))
+        (else
+          acc)))))
+
+(define-total get-fresh-name
+  (lambda (env)
+    (get-fresher-name env 'z)))
+    
+; Entries in env2 override those in env1.
+(define-total merge-envs
+  (lambda (env1 env2)
+    (if (acyclic? env1)
+        (cond
+          ((null? env1)
+            env2)
+          ((get-env env2 (caar env1))
+            (merge-envs (cdr env1) env2))
+          (else
+            (merge-envs (cdr env1) (cons (car env1) env2)))))))
+
+(define-total display-env-loop
+  (lambda (env)
+    (if (acyclic? env)
+      (cond
+        ((null? env)
+         'ok)
+        (else
+          (let* ((pair (car env))
+                 (key  (car pair))
+                 (val  (cdr pair)))
+            (if (not (get-env orig-known-total-env key))
+              (begin (display key) (display " -> ") (display val) (display "; "))
+              'whatever)
+            (display-env-loop (cdr env))))))))
+
+(define-total display-env
+  (lambda (env)
+    (display "{")
+    (display-env-loop env)
+    (display "}")))
+
+;
+; There is only one type complex enough to require helper functions -
+; the type of the procedure currently being analyzed, called a "this".
+; A this tracks the types of all of its arguments.
+;
+
+(define-total is-this?
+  (lambda (type)
+    (and (pair? type) (eq? (car type) 'this))))
+
+(define-total this-args
+  (lambda (type)
+    (cdr type)))
+
+(define-total all-unknown?
+  (lambda (types)
+    (if (acyclic? types)
+        (cond
+          ((null? types)
+            #t)
+          (else
+            (cond
+              ((eq? (car types) 'unknown)
+                (all-unknown? (cdr types)))
+              (else
+                #f)))))))
+
+;
+; A type is "recursable" if it is a this and at least one of the types
+; of its arguments is not "unknown".
+;
+(define-total is-recursable?
+  (lambda (type)
+    (and (is-this? type) (not (all-unknown? (this-args type))))))
+;
+; std.scm - standard environment of known-total procedures.
+; Total Procedures in Scheme, May 2006, Chris Pressey
+; For license information, see the file LICENSE in this directory.
+;
+
+;
+; These are mostly Scheme builtins.
+;
+; We make some assumptions about this list.  The basic assumption
+; is that all of these builtins are implemented correctly and are
+; thus guaranteed to return.  Another assumption is that those
+; builtins that operate on lists (for example, 'length', 'memv',
+; 'list->vector', etc) always return, even when given a cyclic list
+; (even though R5RS does not specify this behaviour.)  Should this
+; assumption fail for some given implementation of some of these
+; builtins, those builtins should be removed from this list, and
+; if those builtins are used in the totality checker itself
+; (notably 'reverse' is used in several places,) "hand-rolled"
+; versions that are guaranteed to terminate should be substituted.
+;
+; Note that this file should NOT be reloaded during bootstrapping.
+;
+; It might be nice if these were local to define-total, but
+; it's more useful for testing purposes if we can access them
+; from outside there too.
+;
+(define orig-known-total-env
+  (map (lambda (name) (cons name 'total-proc)) '(
+    eqv? eq? equal?
+    number? complex? real? rational? integer?
+    exact? inexact?
+    = < > <= >=
+    zero? positive? negative? odd? even? max min
+    + * - /
+    abs quotient remainder modulo
+    gcd lcm
+    numerator denominator
+    floor ceiling truncate round
+    rationalize
+    exp log sin cos tan asin acos atan
+    sqrt expt
+    make-rectangular make-polar real-part imag-part magnitude angle
+    exact->inexact inexact->exact
+    number->string string->number
+    not boolean? and or
+    pair? cons car cdr
+    ;set-car! set-cdr!            ; no side effects
+    caar cadr cdar cddr
+    caaar caadr cadar caddr cdaar cdadr cddar cdddr
+    caaaar caaadr caadar caaddr cadaar cadadr caddar cadddr
+    cdaaar cdaadr cdadar cdaddr cddaar cddadr cdddar cddddr
+    null? list?
+    list length append reverse    ; NOTE: can depend on implementation
+    list-tail list-ref            ; NOTE: can depend on implementation
+    memq memv member              ; NOTE: can depend on implementation
+    assq assv assoc               ; NOTE: can depend on implementation
+    symbol? symbol->string string->symbol
+    char?
+    char=? char<? char>? char<=? char>=? 
+    char-ci=? char-ci<? char-ci>? char-ci<=? char-ci>=? 
+    char-alphabetic? char-numeric? char-whitespace?
+    char-upper-case? char-lower-case?
+    char->integer integer->char
+    char-upcase char-downcase
+    string? make-string string string-length string-ref
+    ;string-set!                  ; no side effects
+    string=? string-ci=?
+    string<? string>? string<=? string>=? 
+    string-ci<? string-ci>? string-ci<=? string-ci>=?
+    substring string-append
+    string->list list->string
+    string-copy
+    ;string-fill!                 ; no side effects
+    vector? make-vector vector vector-length vector-ref
+    ;vector-set!                  ; no side effects
+    vector->list list->vector
+    ;vector-fill!                 ; no side effects
+    procedure?
+    ;apply                        ; The following builtins call for
+    ;map for-each                 ; more complex flow analysis than
+    ;force                        ; our analyzer does at present.
+    ;call-with-current-continuation values call-with-values dynamic-wind
+    ;eval scheme-report-environment null-environment interaction-environment
+    ;call-with-input-file call-with-output-file
+    input-port? output-port?
+    current-input-port current-output-port
+    ;with-input-from-file with-output-to-file
+    ;open-input-file open-output-file
+    ;close-input-port close-output-port
+    read read-char peek-char
+    eof-object? char-ready?
+    write display newline write-char
+    ;load transcript-on transcript-off
+    acyclic?                      ; part of the analyzer
+  )))
+
+;
+; This variable changes over time, as define-total and definerec-total
+; 'learn' about new user-defined procedures which are also total.
+;
+(define known-total-env orig-known-total-env)
+;
+; test.scm - simple test suite
+; Total Procedures in Scheme, May 2006, Chris Pressey
+; For license information, see the file LICENSE in this directory.
+;
+
+(load "std.scm")
+(load "boot1.scm")
+(load "util.scm")
+(load "env.scm")
+(load "canon.scm")
+(load "crit.scm")
+(load "total.scm")
+
+;
+; Definitions (as S-expressions) of procedures that we will test.
+;
+
+(define simple-proc
+  '(lambda (a b)
+     (if (> a b) (* 2 a) (* 3 b)))
+)
+
+(define unsafe-fac-proc
+  '(lambda (n)
+     (cond
+       ((zero? n)
+         1)
+       (else
+         (* n (fac (- n 1))))))
+)
+
+(define fac-proc
+  '(lambda (n)
+     (if (>= n 0)
+       (cond
+         ((zero? n)
+           1)
+         (else
+           (* n (fac (- n 1)))))
+       0))
+)
+
+(define unsafe-anbncn-proc
+  '(lambda (l k)
+     (cond
+       ((null? l)
+         (eq? k 0))
+       ((eq? (car l) 'a)
+         (anbncn (cdr l) (+ k 1)))
+       ((eq? (car l) 'b)
+         (anbncn (cdr l) (+ k 1)))
+       ((eq? (car l) 'c)
+         (anbncn (cdr l) (- k 2)))
+       (else
+         (anbncn (cdr l) k))))
+)
+
+(define anbncn-proc
+  '(lambda (l k)
+     (if (acyclic? l)
+       (cond
+         ((null? l)
+           (eq? k 0))
+         ((eq? (car l) 'a)
+           (anbncn (cdr l) (+ k 1)))
+         ((eq? (car l) 'b)
+           (anbncn (cdr l) (+ k 1)))
+         ((eq? (car l) 'c)
+           (anbncn (cdr l) (- k 2)))
+         (else
+           (anbncn (cdr l) k)))))
+)
+
+(define ack-proc
+  '(lambda (x y)
+     (if (and (>= x 0) (>= y 0))
+         (cond
+           ((zero? x)
+             (+ y 1))
+           ((zero? y)
+             (ack (- x 1) 1))
+           (else
+             (ack (- x 1) (ack x (- y 1)))))))
+)
+
+(define ever1-proc
+  '(lambda (x)
+     (cond
+       ((eq? x 10000)
+         x)
+       (else
+         (ever1 (+ x 1)))))
+)
+
+;
+; The tests proper.
+;
+
+;; Tests for acyclicity.
+
+(test acyclic-1
+  (acyclic? '(1 2 3 4 5))
+  #t
+)
+
+(test acyclic-2
+  (acyclic? '(1 2 (a b c) 3 4 5))
+  #t
+)
+
+(test acyclic-3
+  (let* ((tail '(5 . TBA))
+         (lst  (append '(1 2 3 4) tail)))
+    (set-cdr! tail lst)
+    (acyclic? lst))
+  #f
+)
+
+(test acyclic-4
+  (let* ((tail      '(5 . TBA))
+         (inner-lst  (append '(1 2 3 4) tail))
+         (outer-lst  (list 'a 'b inner-lst 'c 'd)))
+    (set-cdr! tail inner-lst)
+    (acyclic? outer-lst))
+  #f
+)
+
+;; Tests for canonicalization.
+
+(test canonicalize-simple
+  (canonicalize simple-proc '())
+  '(lambda (a b)
+     (if (> a b)
+       (* 2 a)
+       (* 3 b)))
+)
+
+(test canonicalize-fac
+  (canonicalize fac-proc '())
+  '(lambda (n)
+     (if (>= n 0)
+       (if (zero? n)
+         1
+         (let ((z
+                (let ((z (- n 1))) (fac z))
+              ))
+           (* n z)))
+       0))
+)
+
+(test canonicalize-ack
+  (canonicalize ack-proc '())
+  '(lambda (x y)
+     (if (let ((z (>= x 0)) (zz (>= y 0))) (and z zz))
+         (if (zero? x)
+             (+ y 1)
+             (if (zero? y)
+                 (let ((z (- x 1)))
+                   (ack z 1))
+                 (let ((z (- x 1))
+                       (zz (let ((zz (- y 1))) (ack x zz))))
+                   (ack z zz))))
+         'undefined))
+)
+
+(test canonicalize-let*
+  (canonicalize
+   '(lambda (x y)
+      (let* ((p (+ x y))
+             (q (* p p)))
+        (display q)))
+   '())
+  '(lambda (x y)
+      (let ((p (+ x y)))
+        (let ((q (* p p)))
+          (display q))))
+)
+
+;; Tests for finding critical arguments.
+
+(test crit-args-simple
+  (find-crit (canonicalize simple-proc '()) '(simple))
+  '()
+)
+
+(test crit-args-fac
+  (find-crit (canonicalize fac-proc '()) '(fac))
+  '((n . crit-nat))
+)
+
+(test crit-args-unsafe-fac
+  (find-crit (canonicalize unsafe-fac-proc '()) '(fac))
+  '()
+)
+
+(test crit-args-anbncn
+  (find-crit (canonicalize anbncn-proc '()) '(anbncn))
+  '((l . crit-list))
+)
+
+(test crit-args-ack
+  (find-crit (canonicalize ack-proc '()) '(ack))
+  '()
+)
+
+(test crit-args-ever1
+  (find-crit (canonicalize ever1-proc '()) '(ever1))
+  '()
+)
+
+;; Tests for determining totality.
+
+(test proc-total-simple
+  (proc-total? 'simple (canonicalize simple-proc '()) known-total-env)
+  #t
+)
+
+(test proc-total-fac
+  (proc-total? 'fac (canonicalize fac-proc '()) known-total-env)
+  #t
+)
+
+(test proc-total-unsafe-fac
+  (proc-total? 'fac (canonicalize unsafe-fac-proc '()) known-total-env)
+  #f
+)
+
+(test proc-total-anbncn
+  (proc-total? 'anbncn (canonicalize anbncn-proc '()) known-total-env)
+  #t
+)
+
+(test proc-total-ack
+  (proc-total? 'ack (canonicalize ack-proc '()) known-total-env)
+  #f
+)
+
+(test proc-total-ever1
+  (proc-total? 'ever1 (canonicalize ever1-proc '()) known-total-env)
+  #f
+)
+
+;; Tests for determining totality of mutually-recursive procedures.
+
+(test mutrec-total-even
+  (procs-total? '(even odd) (list
+    (canonicalize '(lambda (x)
+      (if (>= x 0)
+        (cond
+          ((zero? x)
+            1)
+          (else
+            (odd (- x 1)))))) '())
+    (canonicalize '(lambda (x)
+      (if (>= x 0)
+        (cond
+          ((zero? x)
+            0)
+          (else
+            (odd (- x 1)))))) '()))
+    known-total-env)
+  #t
+)
+
+(test mutrec-total-bad
+  (procs-total? '(foo bar) (list
+    (canonicalize '(lambda (x y)
+      (if (acyclic? x)
+        (cond
+          ((null? x)
+            (bar '(1 2 3 4 5) y))
+          (else
+            (foo (cdr x) (+ y 1)))))) '())
+    (canonicalize '(lambda (x y)
+      (if (acyclic? x)
+        (cond
+          ((null? x)
+            (foo '(1 2 3 4 5) y))
+          (else
+            (bar (cdr x) (+ y 1)))))) '()))
+    known-total-env)
+  #f
+)
+;
+; total.scm - kernel of totality checker
+; Total Procedures in Scheme, May 2006, Chris Pressey
+; For license information, see the file LICENSE in this directory.
+;
+
+;
+; Create initial environment from the list of arguments of the lambda
+; expression and from the environment of previously gathered critical
+; arguments.  Each argument which is found in the critical arguments
+; gets a type apropos to its critical nature; arguments that are not
+; found in the critical argument environment get the type 'unknown'.
+;
+(define-total make-initial-args
+  (lambda (formals crit-args env)
+    (if (acyclic? formals)
+      (cond
+        ((null? formals)
+          env)
+        (else
+          (let* ((formal (car formals))
+                 (rest   (cdr formals))
+                 (type   (get-env crit-args formal)))
+            (cond
+              (type
+                (make-initial-args rest crit-args (extend-env env formal type)))
+              (else
+                (make-initial-args rest crit-args (extend-env env formal 'unknown))))))))))
+
+;
+; Create a new 'this' type.
+;
+(define-total make-this
+  (lambda (formals crit-args acc)
+    (if (acyclic? formals)
+      (cond
+        ((null? formals)
+          (cons 'this (reverse acc)))
+        (else
+          (let* ((formal   (car formals))
+                 (rest     (cdr formals))
+                 (this-arg (or (get-env crit-args formal) 'unknown)))
+            (make-this rest crit-args (cons this-arg acc))))))))
+
+;
+; Create a new environment that is suited for a base for the
+; environments of a set of mutually recursive procedures.
+; This environment has one 'this' in it for each procedure.
+; These procedures can call each other, and so must be informed
+; of each others' critical arguments.
+;
+(define-total make-mutual-env
+  (lambda (proc-names expr-reps env)
+    (if (acyclic? proc-names)
+      (cond
+        ((null? proc-names)
+          env)
+        (else
+          (let* ((proc-name (car proc-names))
+                 (expr-rep  (car expr-reps))
+                 (formals   (cadr expr-rep)) ; get-lambda-args
+                 (crit-args (find-crit expr-rep proc-names))
+                 (this      (make-this formals crit-args '()))
+                 (new-env   (extend-env env proc-name this)))
+            (make-mutual-env (cdr proc-names) (cdr expr-reps) new-env)))))))
+
+;
+; A list of built-in functions that, when applied to an acyclic list
+; (list or reduced-list type) always result in a reduced-list.
+;
+(define reducing-procs '(
+       car
+       cdr
+      caar
+      cadr
+      cdar
+      cddr
+     caaar
+     caadr
+     cadar
+     caddr
+     cdaar
+     cdadr
+     cddar
+     cdddr
+    caaaar
+    caaadr
+    caadar
+    caaddr
+    cadaar
+    cadadr
+    caddar
+    cadddr
+    cdaaar
+    cdaadr
+    cdadar
+    cdaddr
+    cddaar
+    cddadr
+    cdddar
+    cddddr
+  ))
+
+;
+; Determine the type of an expression, with respect to totality analysis.
+;
+; If the expression is (- foo 1) where foo is a critical natural number,
+; the type is a reduced natural number.
+;
+; If the expression is (cdr foo) where foo is a critical list, the
+; type is a reduced list.
+;
+(define-total get-expr-type
+  (lambda (expr-rep env)
+    (cond
+      ((is-call? expr-rep)
+        (let* ((proc-name (car expr-rep))
+               (proc-args (cdr expr-rep))
+               (proc-type (get-env env proc-name)))
+          (cond
+            ((eq? proc-name '-)
+              (cond
+                ((and (eq? (get-env env (car proc-args)) 'crit-nat)
+                      (eq? (cadr proc-args) 1))
+                  'reduced-nat)
+                (else
+                  'unknown)))
+            ((memv proc-name reducing-procs)
+              (cond
+                ((or (eq? (get-env env (car proc-args)) 'crit-list)
+                     (eq? (get-env env (car proc-args)) 'reduced-list))
+                  'reduced-list)
+                (else
+                  'unknown)))
+            (else
+              'unknown))))
+      (else
+        'unknown))))
+
+;
+; When encountering a self-recursive call, check that each passed
+; argument coincides with an identified critical argument.
+;
+(define-total check-recurse-args
+  (lambda (actuals formal-types env)
+    (if (acyclic? actuals)
+      (cond
+        ((null? actuals)
+          #t)
+        (else
+          (let* ((actual      (car actuals))
+                 (actual-type (get-env env actual))
+                 (formal-type (car formal-types)))
+            (cond
+              ((and (eq? formal-type 'crit-nat) (not (eq? actual-type 'reduced-nat)))
+                #f)
+              ((and (eq? formal-type 'crit-list) (not (eq? actual-type 'reduced-list)))
+                #f)
+              (else
+                (check-recurse-args (cdr actuals) (cdr formal-types) env)))))))))
+
+;
+; Create a new abstract environment from the existing one, in the context
+; of the abstract execution of the body of the let.
+;
+(define-total make-let-env
+  (lambda (names vals orig-env new-env)
+    (if (acyclic? names)
+      (cond
+        ((null? names)
+          (merge-envs orig-env new-env))
+        (else
+          (let* ((first-name (car names))
+                 (rest-names (cdr names))
+                 (first-val  (car vals))
+                 (rest-vals  (cdr vals))
+                 (first-type (get-expr-type first-val orig-env))
+                 (new-env    (extend-env new-env first-name first-type)))
+            (cond
+              (first-type
+                (make-let-env rest-names rest-vals orig-env new-env))
+              (else
+                #f))))))))
+
+(definerec-total (
+
+;
+; Determine if all bindings in a let-expression are total.
+;
+(bindings-total?
+  (lambda (bindings env)
+    (if (acyclic? bindings)
+      (cond
+        ((null? bindings)
+          #t)
+        (else
+          (let* ((binding    (car bindings))
+                 (rest       (cdr bindings))
+                 (name       (car binding))
+                 (val        (cadr binding)))
+            (cond
+              ((expr-total? val env)
+                (bindings-total? rest env))
+              (else
+                #f))))))))
+
+;
+; Given a canonicalized representation of an expression and a type
+; environment, return #t if we can establish that this expression is total
+; (always terminates for any input,) or #f if we cannot establish that.
+;
+(expr-total?
+  (lambda (expr-rep env)
+    (if (acyclic? expr-rep)
+      (cond
+        ;
+        ; Branch never taken but convinces analysis that we're total.
+        ;
+        ((null? expr-rep)
+          #t)
+        ;
+        ; a) If we see a 'let', we abstractly evaluate each of its
+        ;    initial values in the current environment; then we
+        ;    create a new environment where each name is bound to its
+        ;    newly associated (abstract) value, and abstractly evaluate
+        ;    the body in the new environment.
+        ;
+        ((is-let? expr-rep)
+          (let* ((bindings  (cadr expr-rep))
+                 (names     (bindings->names bindings))
+                 (vals      (bindings->values bindings))
+                 (body-rep  (caddr expr-rep))
+                 (new-env   (make-let-env names vals env '())))
+            (cond
+              (new-env
+                (and (bindings-total? bindings env)
+                     (expr-total? body-rep new-env)))
+              (else
+                (display expr-rep)
+                #f))))
+        ;
+        ; b) If we see an 'if', we abstractly evaluate the test
+	;    and both branches; the procedure is only total if
+	;    all of these are total.
+        ;
+        ((is-if? expr-rep)
+          (let* ((test-expr-rep (cadr expr-rep))  ; get-test-expr
+                 (then-expr-rep (caddr expr-rep)) ; get-then-expr
+                 (else-expr-rep (cadddr expr-rep)) ; get-else-expr
+		 (test-total    (expr-total? test-expr-rep env))
+                 (then-total    (expr-total? then-expr-rep env))
+                 (else-total    (expr-total? else-expr-rep env)))
+            (and test-total then-total else-total)))
+        ;
+        ; c) A sequence is only total if all of its constituent
+        ;    expressions are total.
+        ;
+        ((is-begin? expr-rep)
+          (let* ((first-expr (cadr expr-rep))     ; get-begin-first
+                 (second-expr (caddr expr-rep)))  ; get-begin-second
+          (and (expr-total? first-expr env)
+               (expr-total? second-expr env))))
+        ;
+        ; d) If we see a call to a procedure, we insist that the
+        ;    called procedure must be total as well.  There are three
+        ;    sub-cases to consider here:
+        ;
+        ((is-call? expr-rep)
+          (let* ((proc-name (car expr-rep))
+                 (proc-type (get-env env proc-name))
+                 (proc-args (cdr expr-rep)))
+            (cond
+              ;
+              ; d.1) It's a call to a function that we already know is total.
+              ;
+              ((eq? proc-type 'total-proc)
+                #t)
+              ;
+              ; d.2) It's a recursive call - either self-recursive or
+              ;      to one of any number of mutually recursive procedures.
+              ;      In either case, we must check that the arguments being
+              ;      passed to the critical arguments of the procedure are
+              ;      those that monotonically decrease.
+              ;
+              ((is-recursable? proc-type)
+                (check-recurse-args proc-args (this-args proc-type) env))
+              ;
+              ; d.3) It's a call to a function that we know nothing about.
+              ;      Perhaps it is an external function which was not
+              ;      given in the list of known-total functions, or perhaps
+              ;      it was passed to this function as a parameter.  Either
+              ;      way, because of this call, we must assume that our
+              ;      function might not be total.
+              ;
+              (else
+                #f))))
+        ;
+        ; e) Otherwise, the expression is an atom, number, lambda, or
+        ;    other primitive, and as such, is certainly total.
+        ;
+        (else
+          #t)))))
+
+))
+
+;
+; Given the name of a procedure, a canonicalized, syntax-checked S-expression
+; representing that procedure, and a type environment, return #t if we can
+; establish that this procedure is total (always terminates for any input,)
+; or #f if we cannot establish that.
+;
+; We create a new environment from the given environment, which we use while
+; checking the representation of the procedure.  In this new environment,
+; each of the arguments of the procedure is associated with its type, and
+; the name of the procedure is associated with a 'this' type, which knows
+; the types that each of the arguments should be.
+;
+(define-total proc-total?
+  (lambda (proc-name expr-rep env)
+    (cond
+      ((is-lambda? expr-rep)
+        (let* ((crit-args (find-crit expr-rep (list proc-name)))
+               (body-rep  (caddr expr-rep)) ; get-canonicalized-lambda-body
+               (formals   (cadr expr-rep))  ; get-lambda-args
+               (inner-env (make-initial-args formals crit-args '()))
+               (this      (make-this formals crit-args '()))
+               (outer-env (extend-env env proc-name this))
+               (new-env   (merge-envs outer-env inner-env)))
+          (expr-total? body-rep new-env)))
+      (else
+        #f))))
+
+;
+; Given a set of (possibly mutually recursive) procedures, determine if
+; they are all total.  First form the mutual environment, then call
+; each-proc-total? on the list of procedures, with that environment.
+;
+(define procs-total?
+  (lambda (proc-names expr-reps env)
+    (let* ((canon-expr-reps (canonicalize-all expr-reps env '()))
+           (mutual-env      (make-mutual-env proc-names canon-expr-reps (make-empty-env))))
+      (each-proc-total? proc-names canon-expr-reps (merge-envs env mutual-env)))))
+
+;
+; Do the actual work required by procs-total?.
+;
+(define-total each-proc-total?
+  (lambda (proc-names expr-reps env)
+    (if (acyclic? expr-reps)
+      (cond
+        ((null? expr-reps)
+          #t)
+        (else
+          (let* ((proc-name (car proc-names))
+                 (expr-rep  (car expr-reps))
+                 (body-rep  (caddr expr-rep)) ; get-canonicalized-lambda-body
+                 (formals   (cadr expr-rep))  ; get-lambda-args
+                 (crit-args (find-crit expr-rep proc-names))
+                 (inner-env (make-initial-args formals crit-args '()))
+                 (new-env   (merge-envs env inner-env)))
+            (and
+              (expr-total? body-rep new-env)
+              (each-proc-total? (cdr proc-names) (cdr expr-reps) env))))))))
+;
+; util.scm - miscellaneous utility procedures
+; Total Procedures in Scheme, May 2006, Chris Pressey
+; For license information, see the file LICENSE in this directory.
+;
+
+;
+; Determine if a Scheme datum is acyclic.
+;
+(define acyclic?
+  (lambda (pair)
+    (acyclic-test pair '())))
+
+(define acyclic-test
+  (lambda (pair acc)
+    (cond
+      ((not (pair? pair))
+        #t)
+      ((memq pair acc)
+        #f)
+      (else
+        (let ((fst     (car pair))
+              (snd     (cdr pair))
+              (new-acc (cons pair acc)))
+          (and (acyclic-test fst new-acc) (acyclic-test snd new-acc)))))))
+
+;
+; XXX explain and/or borrow eopl:error
+;
+(define-total error
+  (lambda (msg)
+    (display msg) (newline)
+    (read '())))
+
+;
+; Test case for test suite.
+;
+(define-syntax test
+  (syntax-rules ()
+    ((test test-name expr expected)
+      (begin
+        (display "Running test: ") (display (quote test-name)) (display "... ")
+        (let ((result expr))
+          (cond
+            ((equal? result expected)
+              (display "passed.") (newline))
+            (else
+              (display "FAILED!") (newline)
+              (display "Expected: ") (display expected) (newline)
+              (display "Actual:   ") (display result) (newline))))))))
+
+;
+; XXX there may be a problem doing NON-TAIL (self-)recursion, check it out.
+;
+(define-total bindings->names
+  (lambda (bindings)
+    (if (acyclic? bindings)
+       (cond
+         ((null? bindings)
+           '())
+         (else
+           (let* ((binding (car bindings))
+                  (rest    (cdr bindings))
+                  (name    (car binding)))
+             (cons name (bindings->names rest))))))))
+
+(define-total bindings->values
+  (lambda (bindings)
+    (if (acyclic? bindings)
+       (cond
+         ((null? bindings)
+           '())
+         (else
+           (let* ((binding (car bindings))
+                  (rest    (cdr bindings))
+                  (value   (cadr binding)))
+             (cons value (bindings->values rest))))))))
+
+(define-total is-lambda?
+  (lambda (expr-rep)
+    (and
+      (pair? expr-rep)
+      (eq? 'lambda (car expr-rep)))))
+
+(define-total is-let?
+  (lambda (expr-rep)
+    (and
+      (pair? expr-rep)
+      (eq? 'let (car expr-rep)))))
+
+(define-total is-let*?
+  (lambda (expr-rep)
+    (and
+      (pair? expr-rep)
+      (eq? 'let* (car expr-rep)))))
+
+(define-total is-if?
+  (lambda (expr-rep)
+    (and
+      (pair? expr-rep)
+      (eq? 'if (car expr-rep)))))
+
+(define-total is-cond?
+  (lambda (expr-rep)
+    (and
+      (pair? expr-rep)
+      (eq? 'cond (car expr-rep)))))
+
+(define-total is-begin?
+  (lambda (expr-rep)
+    (and
+      (pair? expr-rep)
+      (eq? 'begin (car expr-rep)))))
+
+(define-total is-call?
+  (lambda (expr-rep)
+    (and
+      (pair? expr-rep)
+      (not (eq? (car expr-rep) 'quote)))))  ;... and all others
+
+(define-total is-identifier?
+  (lambda (expr-rep)
+    (symbol? expr-rep)))
+
+(define-total is-quote?
+  (lambda (expr-rep)
+    (and
+      (pair? expr-rep)
+      (eq? 'quote (car expr-rep)))))