[continued from previous message]

(pair? (cdr x))
(args? (cadr x) #f)
(pair? (cddr x)))
(transform-define x))
((and (pair? x) ; (define name expr)
(eq? 'define (car x))
(pair? (cdr x))
(symbol? (cadr x))
(pair? (cddr x))
(null? (cdddr x)))
(make-define-con x))
((and (pair? x) ; define-syntax
(eq? 'define-syntax (car x))
(pair? (cdr x))
(symbol? (cadr x))
(pair? (cddr x)))
(make-syntax-con x))
((list? x) ; (fun arg ...)
(make-application-con x))
((or (boolean? x) ; atom
(char? x)
(integer? x)
(null? x)
(pair? x)
(real? x)
(string? x)
(vector? x))
(list (con (var x) (type-of x))))
(else
(error "make-constraints" x))))

(define (constraints x s0)
(let ((xa (alpha-conv x)))
(append (intrinsic-constraints)
s0
(make-constraints xa)
(list (con (var xa) (var x))))))

;; ----- constraint solver (unifier) ------

(define (lookup x s)
(if (var? x)
(let ((b (assoc x s)))
(if b
(if (eq? (cadr b) x)
x
(lookup (cadr b) s))
x))
x))

(define (extend l r s)
(cons (list l r) s))

(define (fail msg x y)
(list #F msg x y))

(define (mismatch x y)
(fail "type mismatch" x y))

(define (not-unifiable x y)
(fail "unification failed" x y))

(define (failed? x)
(and (pair? x)
(not (car x))))

(define (fix-arity a b)
(define (multiply x n)
(let loop ((r '())
(n n))
(if (positive? n)
(loop (cons x r) (- n 1))
r)))
(let* ((k (+ 2 (- (length b) (length a)))))
(let loop ((a a)
(r '()))
(if (eq? '... (cadr a))
(append (reverse r) (multiply (car a) k) (cddr a))
(loop (cdr a) (cons (car a) r))))))

(define type-var
(let ((c 0))
(lambda (new)
(if new (set! c (+ 1 c)))
(var (string->symbol (string-append "_." (number->string c)))))))

(define (instantiate fun)
(let ((var-map '()))
(define (inst fun)
(map (lambda (x)
(cond ((arrow? x)
(inst x))
((and (pair? x)
(eq? 'quote (car x))
(pair? (cdr x)))
(cond ((eq? '? (cadr x))
(type-var #t))
((assq (cadr x) var-map) => cdr)
(else
(let ((t (type-var #t)))
(set! var-map (cons (cons (cadr x) t) var-map))
t))))
((same? x)
(type-var #F))
(else
x)))
fun))
(inst fun)))

(define (flatten-unions x)
(cond ((null? x) x)
((and (pair? x)
(eq? 'U (car x)))
(let ((u (cons 'U (make-set
(remq 'T (remq 'U (flatten (cdr x))))))))
(if (null? (cddr u))
(apply type (u-members u))
u)))
((pair? x)
(cons (flatten-unions (car x))
(flatten-unions (cdr x))))
(else
x)))

(define (union-member? x a)
(and (memq (type-name x) (flatten-unions a)) #t))

(define (common-members? a b)
(not (null? (intersection (flatten-unions a) (flatten-unions b)))))

(define (unify lcon subst)
(if (null? lcon)
subst
(let ((lv (con-lhs (car lcon)))
(rv (con-rhs (car lcon))))
(let* ((l (lookup lv subst))
(r (lookup rv subst))
(l (if (union? l)
(map (lambda (x) (lookup x subst)) l)
l))
(r (if (union? r)
(map (lambda (x) (lookup x subst)) r)
r)))
(cond ((var? l)
(unify (cdr lcon) (extend l r subst)))
((var? r)
(unify (cdr lcon) (extend r l subst)))
((polymorphic? l)
(let try ((p (poly-sigs l)))
(if (null? p)
(mismatch lv rv)
(let ((nsubst (unify (list (con (car p) r)) subst)))
(if (failed? nsubst)
(try (cdr p))
nsubst)))))
((polymorphic? r)
(let try ((p (poly-sigs r)))
(if (null? p)
(mismatch lv rv)
(let ((nsubst (unify (list (con l (car p))) subst)))
(if (failed? nsubst)
(try (cdr p))
nsubst)))))
((and (arrow? l)
(arrow? r))
(let* ((l (if (memq '... l) (fix-arity l r) l))
(r (if (memq '... r) (fix-arity r l) r)))
(let ((l (instantiate l))
(r (instantiate r)))
(if (not (= (length l) (length r)))
(mismatch lv rv)
(unify (append (map con (cdr l) (cdr r))
(cdr lcon))
subst)))))
((and (union? l)
(union? r))
(if (common-members? (u-members l) (u-members r))
(unify (cdr lcon) subst)
(mismatch lv rv)))
((union? l)
(if (union-member? r l)
(unify (cdr lcon) subst)
(mismatch lv rv)))
((union? r)
(if (union-member? l r)
(unify (cdr lcon) subst)
(mismatch lv rv)))
((and (type? l)
(type? r))
(if (eq? (type-name l) (type-name r))
(unify (cdr lcon) subst)
(mismatch lv rv)))
(else
(not-unifiable `(,lv ,(rename-vars l))
`(,rv ,(rename-vars r)))))))))

;; ----- query interface ------

(define (resolve x s)
(call-with-current-continuation
(lambda (exit)
(define (res x)
(cond ((var? x)
(let ((b (lookup x s)))
(cond ((and (not (equal? x b))
(contains? x b))
(exit (fail "circular" x b)))
((and (var? b)
(eq? (cadr b) (cadr x)))
(var (cadr x)))
(else
(res b)))))
((pair? x)
(cons (res (car x)) (res (cdr x))))
(else
x)))
(instantiate (flatten-unions (res x))))))

(define (rename-vars x)
(define tvar
(let ((c (char->integer #\a)))
(lambda ()
(let ((n c))
(set! c (+ 1 c))
(list 'quote (string->symbol
(string (integer->char n))))))))
(define dict '())
(define (rename x)
(cond ((var? x)
(cond ((assoc x dict)
=> cdr)
(else
(let ((t (tvar)))
(set! dict (cons (cons x t) dict))
t))))
((type? x)
(type-name x))
((pair? x)
(cons (rename (car x))
(rename (cdr x))))
(else
x)))
(rename x))

(define (infer x s0)
(unify (constraints x s0) '()))

(define (query x s)
(resolve (lookup (var x) s) s))

(define (query/r x s)
(let ((res (query x s)))
(if (failed? res)
res
(rename-vars res))))

(define (type-signature x s0)
(let ((subst (infer x s0)))
(if (failed? subst)
subst
(query/r x subst))))

(define (sig x)
(type-signature x '()))

(define (definition-name x)
(and (pair? x)
(eq? 'define (car x))
(pair? (cdr x))
(or (and (symbol? (cadr x))
(cadr x))
(and (pair? (cadr x))
(caadr x)))))

(define (new-con x t)
(let ((v (definition-name x)))
(if v
(list (con (var v) t))
t)))

(define (type-check-program)
(let loop ((x (read))
(s '()))
(if (not (eof-object? x))
(let ((t (type-signature x s))
(n (definition-name x)))
(if n
(begin (display n)
(display " :: ")
(display t)
(newline)))
(loop (read)
(new-con x t))))))

; (display (sig '(define (length x)
; (if (null? x)
; 0
; (+ 1 (length (cdr x)))))) )
; (newline)
----->>> snip <<<-------------------------------------------------------------

--
Nils M Holm < n m h @ t 3 x . o r g > www.t3x.org

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)