- ; takes a list of constraints and a type environment, and makes it work
-(define (substitute c env)
- (let ((go (lambda (x) (let ((tv (cdr x))
- (n (car x)))
- ;; (display tv)
- ;; (display "\n")
- ;; (display n)
- (cons n (fold-left
- (lambda (a y)
- ;; (display y)
- ;; (display ":")
- ;; (display a)
- (cond ((eq? a (car y)) (cdr y))
- ((eq? a (cdr y)) (car y))
- (else a)))
- tv c))))))
- (map go env)))
+
+ ; TODO: what's the most appropriate substitution?
+ ; should all constraints just be limited to a pair?
+(define (substitute cs t)
+ (define (blah c)
+ (if (null? (cdr c))
+ (car c)
+ (if (not (tvar? (car c)))
+ (car c)
+ (blah (cdr c)))))
+ (fold-left
+ (lambda (t c)
+ (if (member t c)
+ (blah c)
+ t))
+ t cs))
+
+(define (substitute-env cs env)
+ (map (lambda (x) (cons (car x) (substitute cs (cdr x)))) env))
+
+(define (~ a b)
+ (list (list a b)))
+
+(define (consolidate x y)
+ (define (merge a b)
+ (cond ((null? a) b)
+ ((null? b) a)
+ (else (if (member (car b) a)
+ (merge a (cdr b))
+ (cons (car b) (merge a (cdr b)))))))
+ (define (overlap? a b)
+ (if (or (null? a) (null? b))
+ #f
+ (if (fold-left (lambda (acc v)
+ (or acc (eq? v (car a))))
+ #f b)
+ #t
+ (overlap? (cdr a) b))))
+
+ (cond ((null? y) x)
+ ((null? x) y)
+ (else (let* ((a (car y))
+ (merged (fold-left
+ (lambda (acc b)
+ (if acc
+ acc
+ (if (overlap? a b)
+ (cons (merge a b) b)
+ #f)))
+ #f x))
+ (removed (if merged
+ (filter (lambda (b) (not (eq? b (cdr merged)))) x)
+ x)))
+ (if merged
+ (consolidate removed (cons (car merged) (cdr y)))
+ (consolidate (cons a x) (cdr y)))))))