scsh-0.5/bcomp/recon.scm

384 lines
14 KiB
Scheme
Raw Normal View History

; Copyright (c) 1993, 1994 Richard Kelsey and Jonathan Rees. See file COPYING.
; Rudimentary type reconstruction, hardly worthy of the name.
; Currently, NODE-TYPE is called in two places. One is to determine
; the type of the right-hand side of a DEFINE for a variable that is
; never assigned, so uses of the variable can be checked later. The
; other is when compiling a call, to check types of arguments and
; produce warning messages.
; This is heuristic, to say the least. It's not clear what the right
; interface or formalism is for Scheme; I'm still experimenting.
; Obviously we can't do Hindley-Milner inference. Not only does
; Scheme have subtyping, but it also has dependent types up the wazoo.
; For example, the following is perfectly correct Scheme:
;
; (define (foo x y) (if (even? x) (car y) (vector-ref y 3)))
(define (node-type node env)
;; Ignore env, since we don't ever call CLASSIFY or LOOKUP.
(reconstruct node 'fast any-values-type))
(define (reconstruct-type node env)
(reconstruct node '() any-values-type))
(define (reconstruct node constrained want-type)
(cond ((node? node)
((operator-table-ref reconstructors (node-operator-id node))
node constrained want-type))
((pair? node) any-values-type)
((name? node) value-type)
(else (constant-type node))))
(define reconstructors
(make-operator-table (lambda (node constrained want-type)
(reconstruct-call node constrained want-type))))
(define (define-reconstructor name type proc)
(operator-define! reconstructors name type proc))
(define-reconstructor 'lambda syntax-type
(lambda (node constrained want-type)
(if (eq? constrained 'fast)
any-procedure-type
(let ((form (node-form node))
(var-nodes (node-ref node 'var-nodes))
(want-result (careful-codomain want-type)))
(let ((formals (cadr form)))
(if var-nodes
(let* ((alist (map (lambda (node) (cons node value-type))
var-nodes))
;; We can't do (append alist constrained) because the
;; lambda might not be called...
(cod (reconstruct-body (cddr form)
alist
want-result)))
(procedure-type (if (n-ary? formals)
any-values-type ;lose
(make-some-values-type (map cdr alist)))
cod
#t))
(procedure-type
(if (n-ary? formals)
any-values-type ;lose
(make-some-values-type (map (lambda (f) value-type)
formals)))
(reconstruct-body (cddr form) constrained want-result)
#t)))))))
(define (careful-codomain proc-type)
(if (procedure-type? proc-type)
(procedure-type-codomain proc-type)
any-values-type))
(define (reconstruct-body body constrained want-type)
(if (null? (cdr body))
(reconstruct (car body) constrained want-type)
any-values-type))
(define operator/name (get-operator 'name))
(define-reconstructor 'name 'leaf
(lambda (node constrained want-type)
(if (eq? constrained 'fast)
(reconstruct-name node)
(let ((z (assq node constrained)))
(if z
(let ((type (meet-type (cdr z) want-type)))
(begin (set-cdr! z type)
type))
(reconstruct-name node))))))
(define (reconstruct-name node)
(let ((probe (node-ref node 'binding)))
(if (binding? probe)
(let ((t (binding-type probe)))
(cond ((variable-type? t) (variable-value-type t))
((subtype? t value-type) t)
(else value-type)))
value-type)))
(define (reconstruct-call node constrained want-type)
(let* ((form (node-form node))
(op-type (reconstruct (car form)
constrained
(procedure-type any-arguments-type
want-type
#f)))
(args (cdr form))
(lose (lambda ()
(for-each (lambda (arg)
(examine arg constrained value-type))
args))))
(if (procedure-type? op-type)
(begin (if (restrictive? op-type)
(let loop ((args args)
(dom (procedure-type-domain op-type)))
(if (not (or (null? args)
(empty-rail-type? dom)))
(begin (examine (car args)
constrained
(head-type dom))
(loop (cdr args) (tail-type dom)))))
(lose))
(procedure-type-codomain op-type))
(begin (lose)
any-values-type))))
(define-reconstructor 'literal 'leaf
(lambda (node constrained want-type)
(constant-type (node-form node))))
(define-reconstructor 'quote syntax-type
(lambda (node constrained want-type)
(constant-type (cadr (node-form node)))))
(define-reconstructor 'if syntax-type
(lambda (node constrained want-type)
(let ((form (node-form node)))
(examine (cadr form) constrained value-type)
;; Fork off two different constrain sets
(let ((con-alist (fork-constraints constrained))
(alt-alist (fork-constraints constrained)))
(let ((con-type (reconstruct (caddr form) con-alist want-type))
(alt-type (reconstruct (cadddr form) alt-alist want-type)))
(if (pair? constrained)
(for-each (lambda (c1 c2 c)
(set-cdr! c (join-type (cdr c1) (cdr c2))))
con-alist
alt-alist
constrained))
(join-type con-type alt-type))))))
(define (fork-constraints constrained)
(if (pair? constrained)
(map (lambda (x) (cons (car x) (cdr x)))
constrained)
constrained))
(define-reconstructor 'begin syntax-type
(lambda (node constrained want-type)
;; This is unsound - there might be a throw out of some subform
;; other than the final one.
(do ((forms (cdr (node-form node)) (cdr forms)))
((null? (cdr forms))
(reconstruct (car forms) constrained want-type))
(examine (car forms) constrained any-values-type))))
(define (examine node constrained want-type)
(if (pair? constrained)
(reconstruct node constrained want-type)
want-type))
(define-reconstructor 'set! syntax-type
(lambda (node constrained want-type)
(examine (caddr (node-form node)) constrained value-type)
unspecific-type))
(define-reconstructor 'letrec syntax-type
(lambda (node constrained want-type)
(let ((form (node-form node)))
(if (eq? constrained 'fast)
(reconstruct (last form) 'fast want-type)
(let ((types (map (lambda (spec)
(reconstruct (cadr spec) constrained value-type))
(cadr form))))
(reconstruct (last form)
(let ((nodes (node-ref node 'var-nodes)))
(if nodes
(append (map cons nodes types)
constrained)
constrained))
want-type))))))
(define-reconstructor 'primitive-procedure syntax-type
(lambda (node constrained want-type)
(operator-type (get-operator (cadr (node-form node)))))) ;mumble
(define-reconstructor 'loophole syntax-type
(lambda (node constrained want-type)
(let ((args (cdr (node-form node))))
(examine (cadr args) constrained any-values-type)
(sexp->type (schemify (car args)) #t)))) ;Foo
(define (node->type node)
(if (node? node)
(let ((form (node-form node)))
(if (pair? form)
(map node->type form)
(desyntaxify form)))
(desyntaxify node)))
(define-reconstructor 'define syntax-type
(lambda (node constrained want-type)
':definition))
(define-reconstructor 'define-syntax syntax-type
(lambda (node constrained want-type)
':definition))
(define call-node? (node-predicate 'call))
(define name-node? (node-predicate 'name))
(define begin-node? (node-predicate 'begin))
; --------------------
; Primitive procedures:
(define-reconstructor 'values any-procedure-type
(lambda (node constrained want-type)
(make-some-values-type (map (lambda (node)
(meet-type
(reconstruct node constrained value-type)
value-type))
(cdr (node-form node))))))
(define-reconstructor 'call-with-values
(proc ((proc () any-values-type #f)
any-procedure-type)
any-values-type)
(lambda (node constrained want-type)
(let* ((args (cdr (node-form node)))
(thunk-type (reconstruct (car args)
constrained
(procedure-type empty-rail-type
any-values-type
#f))))
(careful-codomain
(reconstruct (cadr args)
constrained
(procedure-type (careful-codomain thunk-type)
any-values-type
#f))))))
(define (reconstruct-apply node constrained want-type)
(let* ((args (cdr (node-form node)))
(proc-type (reconstruct (car args)
constrained
any-procedure-type)))
(for-each (lambda (arg) (examine arg constrained value-type))
(cdr args))
(careful-codomain proc-type)))
(define-reconstructor 'apply
(proc (any-procedure-type &rest value-type) any-values-type)
reconstruct-apply)
(define-reconstructor 'primitive-catch
(proc ((proc (escape-type) any-values-type #f))
any-values-type)
reconstruct-apply)
; --------------------
; Types of simple primitives.
(define (declare-operator-type ops type)
(if (list? ops)
(for-each (lambda (op) (get-operator op type))
ops)
(get-operator ops type)))
(declare-operator-type 'with-continuation
(proc (escape-type (proc () any-values-type #f))
any-arguments-type))
(declare-operator-type 'eq?
(proc (value-type value-type) boolean-type))
(declare-operator-type '(number? integer? rational? real? complex?
char? eof-object? input-port? output-port?)
(proc (value-type) boolean-type))
(declare-operator-type 'exact?
(proc (number-type) boolean-type))
(declare-operator-type 'exact->inexact (proc (exact-type) inexact-type))
(declare-operator-type 'inexact->exact (proc (inexact-type) exact-type))
(declare-operator-type '(exp log sin cos tan asin acos sqrt)
(proc (number-type) number-type))
(declare-operator-type '(atan)
(proc (number-type number-type) number-type))
(declare-operator-type '(floor)
(proc (real-type) integer-type))
(declare-operator-type '(real-part imag-part angle magnitude)
(proc (complex-type) real-type))
(declare-operator-type '(numerator denominator)
(proc (rational-type) integer-type))
(declare-operator-type '(+ * - /)
(proc (number-type number-type) number-type))
(declare-operator-type '(= <)
(proc (real-type real-type) boolean-type))
(declare-operator-type '(make-polar make-rectangular)
(proc (real-type real-type) complex-type))
(declare-operator-type '(quotient remainder)
(proc (integer-type integer-type) integer-type))
(declare-operator-type '(bitwise-not)
(proc (exact-integer-type) exact-integer-type))
(declare-operator-type '(bitwise-and bitwise-ior bitwise-xor
arithmetic-shift)
(proc (exact-integer-type exact-integer-type)
exact-integer-type))
(declare-operator-type '(char=? char<?)
(proc (char-type char-type) boolean-type))
(declare-operator-type 'char->ascii
(proc (char-type) exact-integer-type))
(declare-operator-type 'ascii->char
(proc (exact-integer-type) char-type))
(declare-operator-type 'string=?
(proc (string-type string-type) boolean-type))
(declare-operator-type 'open-port
;; Can return #f
(proc (string-type exact-integer-type) value-type))
(declare-operator-type 'cons (proc (value-type value-type) pair-type))
(declare-operator-type 'intern (proc (string-type vector-type) symbol-type))
; Can't do I/O until the meta-types interface exports input-port-type and
; output-port-type.
(define (constant-type x)
(cond ((number? x)
(meet-type (if (exact? x) exact-type inexact-type)
(cond ((integer? x) integer-type)
((rational? x) rational-type)
((real? x) real-type)
((complex? x) complex-type)
(else number-type))))
((boolean? x) boolean-type)
((pair? x) pair-type)
((string? x) string-type)
((char? x) char-type)
((null? x) null-type)
((symbol? x) symbol-type)
((vector? x) vector-type)
(else value-type)))