95 lines
2.7 KiB
Scheme
95 lines
2.7 KiB
Scheme
|
; Copyright (c) 1994 by Richard Kelsey. See file COPYING.
|
||
|
|
|
||
|
|
|
||
|
|
; Type Inference
|
||
|
|
;
|
||
|
|
; The entry points to the inferencer are:
|
||
|
|
;
|
||
|
|
; (unify! type1 type2 context)
|
||
|
|
; Unify TYPE1 and TYPE2. CONTEXT is used to provide user feedback when type
|
||
|
|
; errors are detected.
|
||
|
|
;
|
||
|
|
; (make-uvar prefix depth . maybe-id)
|
||
|
|
; Makes a new type variable. PREFIX is a symbol, DEPTH is the current type
|
||
|
|
; depth (used for polymorphism), and MAYBE-ID is an optional unique
|
||
|
|
; integer.
|
||
|
|
;
|
||
|
|
; (schemify-type type depth)
|
||
|
|
; Make TYPE polymorphic in any variables bound at DEPTH.
|
||
|
|
;
|
||
|
|
; (instantiate-type-scheme scheme depth)
|
||
|
|
; Return an instantiation of SCHEME at DEPTH.
|
||
|
|
;
|
||
|
|
; (reset-inference!)
|
||
|
|
; Clear various global variables (to be replaced with fluids at some point)
|
||
|
|
|
||
|
|
|
||
|
|
(define (unify! type1 type2 context)
|
||
|
|
(cond ((really-unify! type1 type2)
|
||
|
|
=> (lambda (error-thunk)
|
||
|
|
(unify-lost error-thunk type1 type2 context)))))
|
||
|
|
|
||
|
|
(define *currently-checking* #f)
|
||
|
|
(define *current-top-exp* #f)
|
||
|
|
|
||
|
|
(define (unify-lost error-thunk type1 type2 context)
|
||
|
|
(cond ((eq? context 'simplifying)
|
||
|
|
(bug "unification error while instantiating an integrable procedure"))
|
||
|
|
((eq? context 'make-monomorphic)
|
||
|
|
#f)
|
||
|
|
(else
|
||
|
|
(user-type-error-message error-thunk type1 type2 context))))
|
||
|
|
|
||
|
|
(define (user-type-error-message error-thunk type1 type2 context)
|
||
|
|
(format #t "Type error in ~S~% " (schemify context))
|
||
|
|
(error-thunk)
|
||
|
|
(if *currently-checking*
|
||
|
|
(begin
|
||
|
|
(format #t "~% while reconstructing the type of~% ")
|
||
|
|
(*currently-checking* (current-output-port))))
|
||
|
|
(error "type problem"))
|
||
|
|
|
||
|
|
(define (really-unify! p1 p2)
|
||
|
|
(let ((p1 (maybe-follow-uvar p1)) ; get the current value of P1
|
||
|
|
(p2 (maybe-follow-uvar p2))) ; get the current value of P2
|
||
|
|
(cond ((or (eq? p1 p2)
|
||
|
|
(eq? p1 type/null)
|
||
|
|
(eq? p2 type/null))
|
||
|
|
#f)
|
||
|
|
((uvar? p1)
|
||
|
|
(bind-uvar! p1 p2))
|
||
|
|
((uvar? p2)
|
||
|
|
(bind-uvar! p2 p1))
|
||
|
|
((other-type? p1)
|
||
|
|
(if (and (other-type? p2)
|
||
|
|
(eq? (other-type-kind p1) (other-type-kind p2))
|
||
|
|
(= (length (other-type-subtypes p1))
|
||
|
|
(length (other-type-subtypes p2))))
|
||
|
|
(unify-lists! (other-type-subtypes p1)
|
||
|
|
(other-type-subtypes p2))
|
||
|
|
(mismatch-failure p1 p2)))
|
||
|
|
(else
|
||
|
|
(mismatch-failure p1 p2)))))
|
||
|
|
|
||
|
|
(define (mismatch-failure t1 t2)
|
||
|
|
(lambda ()
|
||
|
|
(format #t "type mismatch~% ")
|
||
|
|
(display-type t1 (current-output-port))
|
||
|
|
(format #t "~% ")
|
||
|
|
(display-type t2 (current-output-port))))
|
||
|
|
|
||
|
|
(define (unify-lists! l1 l2)
|
||
|
|
(let loop ((l1 l1) (l2 l2))
|
||
|
|
(if (null? l1)
|
||
|
|
#f
|
||
|
|
(or (really-unify! (car l1) (car l2))
|
||
|
|
(loop (cdr l1) (cdr l2))))))
|
||
|
|
|
||
|
|
(define (type-conflict message . stuff)
|
||
|
|
(apply breakpoint message stuff))
|
||
|
|
|
||
|
|
; For debugging
|
||
|
|
(define (uvar-name uvar)
|
||
|
|
(concatenate-symbol (uvar-prefix uvar) "." (uvar-id uvar)))
|
||
|
|
|