guile-prescheme/ps-compiler/prescheme/inference.scm

;;; Ported from Scheme 48 1.9.  See file COPYING for notices and license.
;;;
;;; Port Author: Andrew Whatson
;;;
;;; Original Authors: Richard Kelsey, Mike Sperber
;;;
;;;   scheme48-1.9.2/ps-compiler/prescheme/inference.scm
;;;
;;; 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-module (ps-compiler prescheme inference)
  #:use-module (prescheme scheme48)
  #:use-module (prescheme bcomp node)
  #:use-module (prescheme bcomp schemify)
  #:use-module (ps-compiler prescheme type)
  #:use-module (ps-compiler prescheme type-var)
  #:use-module (ps-compiler util syntax)
  #:use-module (ps-compiler util util)
  #:export (unify!
            *currently-checking*))

(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))
          ((and (eq? p1 type/unit)
                (eq? p2 type/unit))
           #f)
          ((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)))