|
22 | 22 | "signatures.rkt" "fail.rkt" |
23 | 23 | "promote-demote.rkt" |
24 | 24 | racket/match |
25 | | - (only-in racket/function curry curryr) |
| 25 | + (only-in racket/function curry curryr thunk) |
26 | 26 | ;racket/trace |
27 | 27 | (contract-req) |
28 | 28 | (for-syntax |
|
66 | 66 | [(context V X Y) |
67 | 67 | (context (append bounds V) (append vars X) (append indices Y))])) |
68 | 68 |
|
| 69 | + |
69 | 70 | (define (inferable-index? ctx bound) |
70 | 71 | (match ctx |
71 | 72 | [(context _ _ Y) |
|
493 | 494 | ;; this constrains just x (which is a single var) |
494 | 495 | (define (singleton S x T) |
495 | 496 | (insert empty x S T)) |
| 497 | + |
| 498 | + (define (constrain tvar-a tvar-b #:above above) |
| 499 | + (match-define (F: var maybe-type-bound) tvar-a) |
| 500 | + (define-values (default sub sing) (if above |
| 501 | + (values Univ |
| 502 | + (thunk (subtype tvar-b maybe-type-bound obj)) |
| 503 | + (curry singleton (var-promote tvar-b (context-bounds context)) var)) |
| 504 | + (values -Bottom |
| 505 | + (thunk (subtype maybe-type-bound tvar-b obj)) |
| 506 | + (curryr singleton var (var-demote tvar-b (context-bounds context)))))) |
| 507 | + (cond |
| 508 | + [(not maybe-type-bound) (sing default)] |
| 509 | + [(sub) (sing maybe-type-bound)] |
| 510 | + [else #f])) |
| 511 | + |
496 | 512 | ;; FIXME -- figure out how to use parameters less here |
497 | 513 | ;; subtyping doesn't need to use it quite as much |
498 | 514 | (define cs (current-seen)) |
|
569 | 585 |
|
570 | 586 | ;; variables that are in X and should be constrained |
571 | 587 | ;; all other variables are compatible only with themselves |
572 | | - [((F: (? (inferable-var? context) v) maybe-type-bound) T) |
| 588 | + [((and (F: (? (inferable-var? context))) S) T) |
573 | 589 | #:return-when |
574 | 590 | (match T |
575 | 591 | ;; fail when v* is an index variable |
576 | 592 | [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))] |
577 | 593 | [_ #f]) |
578 | 594 | #f |
579 | | - ;; constrain v to be below T (but don't mention bounds) |
580 | | - (let ([sing (curryr singleton v (var-demote T (context-bounds context)))]) |
581 | | - (cond |
582 | | - [(and maybe-type-bound (subtype maybe-type-bound T obj)) |
583 | | - (sing maybe-type-bound)] |
584 | | - [(not maybe-type-bound) (sing -Bottom)] |
585 | | - [else #f]))] |
586 | | - |
587 | | - [(S (F: (? (inferable-var? context) v) maybe-type-bound)) |
| 595 | + ;; constrain S to be below T (but don't mention bounds) |
| 596 | + (constrain S T #:above #f)] |
| 597 | + |
| 598 | + [(S (and (F: (? (inferable-var? context))) T)) |
588 | 599 | #:return-when |
589 | 600 | (match S |
590 | 601 | [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))] |
591 | 602 | [_ #f]) |
592 | 603 | #f |
593 | | - ;; constrain v to be above S (but don't mention bounds) |
594 | | - (let ([sing (curry singleton (var-promote S (context-bounds context)) v)]) |
595 | | - (cond |
596 | | - [(and maybe-type-bound (subtype S maybe-type-bound obj)) |
597 | | - (sing maybe-type-bound)] |
598 | | - [(not maybe-type-bound) (sing Univ)] |
599 | | - [else #f]))] |
| 604 | + ;; constrain T to be above S (but don't mention bounds) |
| 605 | + (constrain T S #:above #t)] |
600 | 606 |
|
601 | 607 | ;; recursive names should get resolved as they're seen |
602 | 608 | [(s (? Name? t)) |
|
0 commit comments