suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Refactor type inference to eliminate exceptions.

Browse Source 
This provides approximately 6% speedup on
`racket -l math/scribblings/math.scrbl` and about
14% speedup on the `new-metrics` test.

Mostly this involves threading #f through the whole
of the inference process.  There are several new
macros in `typed-racket/infer/fail` which are useful
for comprehensively using Maybe-monad style
programming in Racket.  Of particular note is `%`,
which satisfies (% f e ...) => (and e ... (f e ...))
but with the obvious fixes.

This commit also weakens several contracts which
caused the build of DrRacket and/or `math` to fail
when contracts were enabled.
This commit is contained in:
Sam Tobin-Hochstadt 2014-05-05 21:30:11 -04:00
parent 5bd3a9ff2f
commit f83950fbab
14 changed files with 490 additions and 305 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

71
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/constraints.rkt
View File

@ -4,25 +4,13 @@
(types abbrev union subtype) (types abbrev union subtype)
(utils tc-utils) (utils tc-utils)
unstable/sequence unstable/hash unstable/sequence unstable/hash
"signatures.rkt" "constraint-structs.rkt" "fail.rkt" "signatures.rkt" "constraint-structs.rkt"
racket/match racket/match
racket/list) racket/list)
(import restrict^ dmap^) (import restrict^ dmap^)
(export constraints^) (export constraints^)
;; It's hard to remove this use of exceptions
;; because there's no monadic version of `hash-union` etc
(define-values (fail-sym exn:infer?)
(let ([sym (gensym 'infer-fail)])
(values sym (λ (s) (and (pair? s) (eq? (car s) sym))))))
;; why does this have to be duplicated?
;; inference failure - masked before it gets to the user program
(define-syntaxes (fail!)
(syntax-rules ()
[(_ s t) (raise (list fail-sym s t))]))
;; Widest constraint possible ;; Widest constraint possible
(define (no-constraint v) (define (no-constraint v)
(make-c (Un) v Univ)) (make-c (Un) v Univ))
@ -31,10 +19,12 @@
;; index variables Y. For now, we add the widest constraints for ;; index variables Y. For now, we add the widest constraints for
;; variables in X to the cmap and create an empty dmap. ;; variables in X to the cmap and create an empty dmap.
(define (empty-cset X Y) (define (empty-cset X Y)
(make-cset (list (cons (for/hash ([x (in-list X)]) (values x (no-constraint x))) (make-cset (list (cons (for/hash ([x (in-list X)])
(values x (no-constraint x)))
(make-dmap (make-immutable-hash null)))))) (make-dmap (make-immutable-hash null))))))
;; add the constraints S <: var <: T to every map in cs
(define (insert cs var S T) (define (insert cs var S T)
(match cs (match cs
[(struct cset (maps)) [(struct cset (maps))
@ -42,7 +32,9 @@
(cons (hash-set map var (make-c S var T)) (cons (hash-set map var (make-c S var T))
dmap)))])) dmap)))]))
;; a stupid impl ;; meet: Type Type -> Type
;; intersect the given types. produces a lower bound on both, but
;; perhaps not the GLB
(define (meet S T) (define (meet S T)
(let ([s* (restrict S T)]) (let ([s* (restrict S T)])
(if (and (subtype s* S) (if (and (subtype s* S)
@ -50,41 +42,54 @@
s* s*
(Un)))) (Un))))
;; join: Type Type -> Type
;; union the given types
(define (join T U) (Un T U)) (define (join T U) (Un T U))
;; meet of two variable constraints
;; never fails
;; if var is provided, the resulting constraint uses it, otherwise it
;; uses the variable from `c1` (which must be the same as the one from
;; `c2`)
(define (c-meet c1 c2 [var #f]) (define (c-meet c1 c2 [var #f])
(match* (c1 c2) (match*/early (c1 c2)
[((struct c (S X T)) (struct c (S* X* T*))) [((struct c (S X T)) (struct c (S* X* T*)))
(unless (or var (eq? X X*)) (unless (or var (eq? X X*))
(int-err "Non-matching vars in c-meet: ~a ~a" X X*)) (int-err "Non-matching vars in c-meet: ~a ~a" X X*))
(let ([S (join S S*)] [T (meet T T*)]) (let ([S (join S S*)] [T (meet T T*)])
(unless (subtype S T) (and (subtype S T)
(fail! S T)) (make-c S (or var X) T)))]))
(make-c S (or var X) T))]))
;; compute the meet of two constraint sets
;; returns #f for failure
(define (cset-meet x y) (define (cset-meet x y)
(match* (x y) (match* (x y)
[((struct cset (maps1)) (struct cset (maps2))) [((struct cset (maps1)) (struct cset (maps2)))
(let ([maps (filter values (define maps (for*/list ([(map1 dmap1) (in-pairs (remove-duplicates maps1))]
(for*/list [(map2 dmap2) (in-pairs (remove-duplicates maps2))]
([(map1 dmap1) (in-pairs (remove-duplicates maps1))] [v (in-value (% cons
[(map2 dmap2) (in-pairs (remove-duplicates maps2))]) (hash-union/fail map1 map2 #:combine c-meet)
(with-handlers ([exn:infer? (lambda (_) #f)]) (dmap-meet dmap1 dmap2)))]
(cons #:when v)
(hash-union map1 map2 #:combine c-meet) v))
(dmap-meet dmap1 dmap2)))))]) (cond [(null? maps)
(when (null? maps) #f]
(fail! maps1 maps2)) [else (make-cset maps)])]
(make-cset maps))]
[(_ _) (int-err "Got non-cset: ~a ~a" x y)])) [(_ _) (int-err "Got non-cset: ~a ~a" x y)]))
;; combines a list of csets using cset-meet individually
;; returns #f for failure
(define (cset-meet* args) (define (cset-meet* args)
(for/fold ([c (make-cset (list (cons (make-immutable-hash null) (for/fold ([c (make-cset (list (cons
(make-immutable-hash null)
(make-dmap (make-immutable-hash null)))))]) (make-dmap (make-immutable-hash null)))))])
([a (in-list args)]) ([a (in-list args)]
#:break (not c))
(cset-meet a c))) (cset-meet a c)))
(define (cset-combine l) ;; produces a cset of all of the maps in all of the given csets
;; FIXME: should this call `remove-duplicates`?
(define (cset-join l)
(let ([mapss (map cset-maps l)]) (let ([mapss (map cset-maps l)])
(make-cset (apply append mapss)))) (make-cset (apply append mapss))))

55
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/dmap.rkt
View File

@ -1,6 +1,6 @@
#lang racket/unit #lang racket/unit
(require "../utils/utils.rkt" (require "../utils/utils.rkt" "fail.rkt"
"signatures.rkt" "constraint-structs.rkt" "signatures.rkt" "constraint-structs.rkt"
(utils tc-utils) (utils tc-utils)
(contract-req) (contract-req)
@ -9,38 +9,40 @@
(import constraints^) (import constraints^)
(export dmap^) (export dmap^)
;; dcon-meet : dcon dcon -> dcon
;; dcon-meet : dcon dcon -> dcon or #f
(define/cond-contract (dcon-meet dc1 dc2) (define/cond-contract (dcon-meet dc1 dc2)
(dcon/c dcon/c . -> . dcon/c) (dcon/c dcon/c . -> . (or/c #f dcon/c))
(match* (dc1 dc2) (match*/early (dc1 dc2)
[((struct dcon-exact (fixed1 rest1)) (or (struct dcon (fixed2 rest2)) [((struct dcon-exact (fixed1 rest1)) (or (struct dcon (fixed2 rest2))
(struct dcon-exact (fixed2 rest2)))) (struct dcon-exact (fixed2 rest2))))
(unless (and rest2 (= (length fixed1) (length fixed2))) #:return-unless (and rest2 (= (length fixed1) (length fixed2)))
(fail! fixed1 fixed2)) #f
(make-dcon-exact (% make-dcon-exact
(for/list ([c1 (in-list fixed1)] (for/list/fail ([c1 (in-list fixed1)]
[c2 (in-list fixed2)]) [c2 (in-list fixed2)])
(c-meet c1 c2 (c-X c1))) (c-meet c1 c2 (c-X c1)))
(c-meet rest1 rest2 (c-X rest1)))] (c-meet rest1 rest2 (c-X rest1)))]
;; redo in the other order to call the first case ;; redo in the other order to call the previous case
[((struct dcon (fixed1 rest1)) (struct dcon-exact (fixed2 rest2))) [((struct dcon (fixed1 rest1)) (struct dcon-exact (fixed2 rest2)))
(dcon-meet dc2 dc1)] (dcon-meet dc2 dc1)]
[((struct dcon (fixed1 #f)) (struct dcon (fixed2 #f))) [((struct dcon (fixed1 #f)) (struct dcon (fixed2 #f)))
(unless (= (length fixed1) (length fixed2)) #:return-unless (= (length fixed1) (length fixed2))
(fail! fixed1 fixed2)) #f
(make-dcon (%1 make-dcon
(for/list ([c1 (in-list fixed1)] (for/list/fail ([c1 (in-list fixed1)]
[c2 (in-list fixed2)]) [c2 (in-list fixed2)])
(c-meet c1 c2 (c-X c1))) (c-meet c1 c2 (c-X c1)))
#f)] #f)]
[((struct dcon (fixed1 #f)) (struct dcon (fixed2 rest))) [((struct dcon (fixed1 #f)) (struct dcon (fixed2 rest)))
(unless (>= (length fixed1) (length fixed2)) #:return-unless (>= (length fixed1) (length fixed2))
(fail! fixed1 fixed2)) #f
(make-dcon (%1 make-dcon
(for/list ([c1 (in-list fixed1)] (for/list/fail ([c1 (in-list fixed1)]
[c2 (in-sequence-forever fixed2 rest)]) [c2 (in-sequence-forever fixed2 rest)])
(c-meet c1 c2 (c-X c1))) (c-meet c1 c2 (c-X c1)))
#f)] #f)]
;; redo in the other order to call the previous case
[((struct dcon (fixed1 rest)) (struct dcon (fixed2 #f))) [((struct dcon (fixed1 rest)) (struct dcon (fixed2 #f)))
(dcon-meet dc2 dc1)] (dcon-meet dc2 dc1)]
[((struct dcon (fixed1 rest1)) (struct dcon (fixed2 rest2))) [((struct dcon (fixed1 rest1)) (struct dcon (fixed2 rest2)))
@ -48,24 +50,25 @@
(if (< (length fixed1) (length fixed2)) (if (< (length fixed1) (length fixed2))
(values fixed1 fixed2 rest1 rest2) (values fixed1 fixed2 rest1 rest2)
(values fixed2 fixed1 rest2 rest1))]) (values fixed2 fixed1 rest2 rest1))])
(make-dcon (% make-dcon
(for/list ([c1 (in-list longer)] (for/list/fail ([c1 (in-list longer)]
[c2 (in-sequence-forever shorter srest)]) [c2 (in-sequence-forever shorter srest)])
(c-meet c1 c2 (c-X c1))) (c-meet c1 c2 (c-X c1)))
(c-meet lrest srest (c-X lrest))))] (c-meet lrest srest (c-X lrest))))]
[((struct dcon-dotted (fixed1 c1 bound1)) (struct dcon-dotted (fixed2 c2 bound2))) [((struct dcon-dotted (fixed1 c1 bound1)) (struct dcon-dotted (fixed2 c2 bound2)))
(unless (and (= (length fixed1) (length fixed2)) #:return-unless (and (= (length fixed1) (length fixed2))
(eq? bound1 bound2)) (eq? bound1 bound2))
(fail! bound1 bound2)) #f
(make-dcon-dotted (for/list ([c1 (in-list fixed1)] [c2 (in-list fixed2)]) (% make-dcon-dotted (for/list/fail ([c1 (in-list fixed1)] [c2 (in-list fixed2)])
(c-meet c1 c2 (c-X c1))) (c-meet c1 c2 (c-X c1)))
(c-meet c1 c2 bound1) bound1)] (c-meet c1 c2 bound1) bound1)]
[((struct dcon _) (struct dcon-dotted _)) [((struct dcon _) (struct dcon-dotted _))
(fail! dc1 dc2)] #f]
[((struct dcon-dotted _) (struct dcon _)) [((struct dcon-dotted _) (struct dcon _))
(fail! dc1 dc2)] #f]
[(_ _) (int-err "Got non-dcons: ~a ~a" dc1 dc2)])) [(_ _) (int-err "Got non-dcons: ~a ~a" dc1 dc2)]))
;; dmap dmap -> dmap or #f
(define (dmap-meet dm1 dm2) (define (dmap-meet dm1 dm2)
(make-dmap (% make-dmap
(hash-union (dmap-map dm1) (dmap-map dm2) #:combine dcon-meet))) (hash-union/fail (dmap-map dm1) (dmap-map dm2) #:combine dcon-meet)))

59
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/fail.rkt Normal file
View File

@ -0,0 +1,59 @@
#lang racket/base
(provide (all-defined-out) early-return)
(require (for-syntax racket/base syntax/parse racket/syntax) "../utils/early-return.rkt"
racket/match)
;; like `match*`, but with `early-return` around the rhss
(define-syntax (match*/early stx)
(define-syntax-class rhs
(pattern (#:when e rhs ...)
#:with r
#'(#:when e (early-return rhs ...)))
(pattern (rhs ...)
#:with r
#'((early-return rhs ...))))
(syntax-parse stx
[(_ e [c . r:rhs] ...)
#'(match* e [c . r.r] ...)]))
;; (% f e ...) == (and e ... (f e ...)) but without repeated evaluation
(define-syntax (% stx)
(syntax-parse stx
[(_ f e ...)
(define/with-syntax (a ...) (generate-temporaries #'(e ...)))
#'(let/fail ([a e] ...)
(f a ...))]))
;; (%1 f e0 e ...) == (and e0 (f e0 e ...)) but without repeated evaluation
(define-syntax (%1 stx)
(syntax-parse stx
[(_ f e0 e ...)
(define/with-syntax (a0 a ...) (generate-temporaries #'(e0 e ...)))
#'(let/fail ([a0 e0])
(let ([a e] ...)
(f a0 a ...)))]))
;; like `let`, but if any bindings are #f, the whole expression produces #f
(define-syntax (let/fail stx)
(syntax-parse stx
[(let/fail () e ...) #'(let () e ...)]
[(let/fail ([x rhs ...] . rest) body ...)
#'(let ([x rhs ...])
(and x
(let/fail rest body ...)))]))
;; (for/list/fail e ...) == (and (andmap values (for/list e ...)) (for/list e ...)
;; but without wasted work
(define-syntax-rule (for/list/fail (cl ...) body ...)
(% reverse
(for/fold ([result null]) (cl ... #:break (not result))
(let ([e (let () body ...)])
(and e (cons e result))))))
;; like hash-union, but if combine ever produces #f, the overall result is #f
(define (hash-union/fail #:combine combine one two)
(for/fold ([one one]) ([(k v) (in-hash two)] #:break (not one))
(define d (if (hash-has-key? one k)
(combine (hash-ref one k) v)
v))
(and d (hash-set one k d))))

382
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
View File

@ -17,7 +17,7 @@
(env index-env tvar-env)) (env index-env tvar-env))
make-env -> ->* one-of/c) make-env -> ->* one-of/c)
"constraint-structs.rkt" "constraint-structs.rkt"
"signatures.rkt" "signatures.rkt" "fail.rkt"
racket/match racket/match
mzlib/etc mzlib/etc
(contract-req) (contract-req)
@ -52,15 +52,17 @@
;; Type Type -> Boolean ;; Type Type -> Boolean
;; Check if a given type pair have been seen before ;; Check if a given type pair have been seen before
(define/cond-contract (seen? s t) (define/cond-contract (seen? s t cs)
((or/c AnyValues? Values/c ValuesDots?) (or/c AnyValues? Values/c ValuesDots?) ((or/c AnyValues? Values/c ValuesDots?) (or/c AnyValues? Values/c ValuesDots?)
(listof (cons/c exact-nonnegative-integer?
exact-nonnegative-integer?))
. -> . any/c) . -> . any/c)
(member (seen-before s t) (current-seen))) (member (seen-before s t) cs))
;; (CMap DMap -> Pair<CMap, DMap>) CSet -> CSet ;; (CMap DMap -> Pair<CMap, DMap>) CSet -> CSet
;; Map a function over a constraint set ;; Map a function over a constraint set
(define (map/cset f cset) (define (map/cset f cset)
(make-cset (for/list ([(cmap dmap) (in-pairs (cset-maps cset))]) (% make-cset (for/list/fail ([(cmap dmap) (in-pairs (cset-maps cset))])
(f cmap dmap)))) (f cmap dmap))))
;; Symbol DCon -> DMap ;; Symbol DCon -> DMap
@ -76,7 +78,8 @@
(define (mover cset dbound vars f) (define (mover cset dbound vars f)
(map/cset (map/cset
(lambda (cmap dmap) (lambda (cmap dmap)
(cons (hash-remove* cmap (cons dbound vars)) (% cons
(hash-remove* cmap (cons dbound vars))
(dmap-meet (dmap-meet
(singleton-dmap (singleton-dmap
dbound dbound
@ -168,40 +171,42 @@
all)))) all))))
(define/cond-contract (cgen/filter V X Y s t) (define/cond-contract (cgen/filter V X Y s t)
((listof symbol?) (listof symbol?) (listof symbol?) Filter? Filter? . -> . cset?) ((listof symbol?) (listof symbol?) (listof symbol?) Filter? Filter? . -> . (or/c #f cset?))
(match* (s t) (match* (s t)
[(e e) (empty-cset X Y)] [(e e) (empty-cset X Y)]
[(e (Top:)) (empty-cset X Y)] [(e (Top:)) (empty-cset X Y)]
;; FIXME - is there something to be said about the logical ones? ;; FIXME - is there something to be said about the logical ones?
[((TypeFilter: s p i) (TypeFilter: t p i)) (cset-meet (cgen V X Y s t) (cgen V X Y t s))] [((TypeFilter: s p i) (TypeFilter: t p i))
[((NotTypeFilter: s p i) (NotTypeFilter: t p i)) (cset-meet (cgen V X Y s t) (cgen V X Y t s))] (% cset-meet (cgen V X Y s t) (cgen V X Y t s))]
[(_ _) (fail! s t)])) [((NotTypeFilter: s p i) (NotTypeFilter: t p i))
(% cset-meet (cgen V X Y s t) (cgen V X Y t s))]
[(_ _) #f]))
;; s and t must be *latent* filter sets ;; s and t must be *latent* filter sets
(define/cond-contract (cgen/filter-set V X Y s t) (define/cond-contract (cgen/filter-set V X Y s t)
((listof symbol?) (listof symbol?) (listof symbol?) FilterSet? FilterSet? . -> . cset?) ((listof symbol?) (listof symbol?) (listof symbol?) FilterSet? FilterSet? . -> . (or/c #f cset?))
(match* (s t) (match* (s t)
[(e e) (empty-cset X Y)] [(e e) (empty-cset X Y)]
[((FilterSet: s+ s-) (FilterSet: t+ t-)) [((FilterSet: s+ s-) (FilterSet: t+ t-))
(cset-meet (cgen/filter V X Y s+ t+) (cgen/filter V X Y s- t-))] (% cset-meet (cgen/filter V X Y s+ t+) (cgen/filter V X Y s- t-))]
[(_ _) (fail! s t)])) [(_ _) #f]))
(define/cond-contract (cgen/object V X Y s t) (define/cond-contract (cgen/object V X Y s t)
((listof symbol?) (listof symbol?) (listof symbol?) Object? Object? . -> . cset?) ((listof symbol?) (listof symbol?) (listof symbol?) Object? Object? . -> . (or/c #f cset?))
(match* (s t) (match* (s t)
[(e e) (empty-cset X Y)] [(e e) (empty-cset X Y)]
[(e (Empty:)) (empty-cset X Y)] [(e (Empty:)) (empty-cset X Y)]
;; FIXME - do something here ;; FIXME - do something here
[(_ _) (fail! s t)])) [(_ _) #f]))
(define/cond-contract (cgen/arr V X Y s-arr t-arr) (define/cond-contract (cgen/arr V X Y s-arr t-arr)
((listof symbol?) (listof symbol?) (listof symbol?) arr? arr? . -> . cset?) ((listof symbol?) (listof symbol?) (listof symbol?) arr? arr? . -> . (or/c #f cset?))
(define (cg S T) (cgen V X Y S T)) (define (cg S T) (cgen V X Y S T))
(match* (s-arr t-arr) (match*/early (s-arr t-arr)
;; the simplest case - no rests, drests, keywords ;; the simplest case - no rests, drests, keywords
[((arr: ss s #f #f '()) [((arr: ss s #f #f '())
(arr: ts t #f #f '())) (arr: ts t #f #f '()))
(cset-meet* (list (% cset-meet* (% list
;; contravariant ;; contravariant
(cgen/list V X Y ts ss) (cgen/list V X Y ts ss)
;; covariant ;; covariant
@ -213,96 +218,100 @@
(cond (cond
;; both rest args are present, so make them the same length ;; both rest args are present, so make them the same length
[(and s-rest t-rest) [(and s-rest t-rest)
(cgen/list V X Y (cons t-rest (extend ss ts t-rest)) (cons s-rest (extend ts ss s-rest)))] (cgen/list V X Y
(cons t-rest (extend ss ts t-rest))
(cons s-rest (extend ts ss s-rest)))]
;; no rest arg on the right, so just pad the left and forget the rest arg ;; no rest arg on the right, so just pad the left and forget the rest arg
[(and s-rest (not t-rest) (<= (length ss) (length ts))) [(and s-rest (not t-rest) (<= (length ss) (length ts)))
(cgen/list V X Y ts (extend ts ss s-rest))] (cgen/list V X Y ts (extend ts ss s-rest))]
;; no rest arg on the left, or wrong number = fail ;; no rest arg on the left, or wrong number = fail
[else (fail! s-arr t-arr)])] [else #f])]
[ret-mapping (cg s t)]) [ret-mapping (cg s t)])
(cset-meet* (list arg-mapping ret-mapping)))] (% cset-meet* (% list arg-mapping ret-mapping)))]
;; dotted on the left, nothing on the right ;; dotted on the left, nothing on the right
[((arr: ss s #f (cons dty dbound) '()) [((arr: ss s #f (cons dty dbound) '())
(arr: ts t #f #f '())) (arr: ts t #f #f '()))
(unless (memq dbound Y) #:return-unless (memq dbound Y)
(fail! s-arr t-arr)) #f
(unless (<= (length ss) (length ts)) #:return-unless (<= (length ss) (length ts))
(fail! ss ts)) #f
(let* ([vars (var-store-take dbound dty (- (length ts) (length ss)))] (let* ([vars (var-store-take dbound dty (- (length ts) (length ss)))]
[new-tys (for/list ([var (in-list vars)]) [new-tys (for/list ([var (in-list vars)])
(substitute (make-F var) dbound dty))] (substitute (make-F var) dbound dty))]
[new-s-arr (make-arr (append ss new-tys) s #f #f null)] [new-s-arr (make-arr (append ss new-tys) s #f #f null)]
[new-cset (cgen/arr V (append vars X) Y new-s-arr t-arr)]) [new-cset (cgen/arr V (append vars X) Y new-s-arr t-arr)])
(move-vars-to-dmap new-cset dbound vars))] (% move-vars-to-dmap new-cset dbound vars))]
;; dotted on the right, nothing on the left ;; dotted on the right, nothing on the left
[((arr: ss s #f #f '()) [((arr: ss s #f #f '())
(arr: ts t #f (cons dty dbound) '())) (arr: ts t #f (cons dty dbound) '()))
(unless (memq dbound Y) #:return-unless (memq dbound Y)
(fail! s-arr t-arr)) #f
(unless (<= (length ts) (length ss)) #:return-unless (<= (length ts) (length ss))
(fail! ss ts)) #f
(let* ([vars (var-store-take dbound dty (- (length ss) (length ts)))] (let* ([vars (var-store-take dbound dty (- (length ss) (length ts)))]
[new-tys (for/list ([var (in-list vars)]) [new-tys (for/list ([var (in-list vars)])
(substitute (make-F var) dbound dty))] (substitute (make-F var) dbound dty))]
[new-t-arr (make-arr (append ts new-tys) t #f #f null)] [new-t-arr (make-arr (append ts new-tys) t #f #f null)]
[new-cset (cgen/arr V (append vars X) Y s-arr new-t-arr)]) [new-cset (cgen/arr V (append vars X) Y s-arr new-t-arr)])
(move-vars-to-dmap new-cset dbound vars))] (% move-vars-to-dmap new-cset dbound vars))]
;; this case is just for constrainting other variables, not dbound ;; this case is just for constrainting other variables, not dbound
[((arr: ss s #f (cons s-dty dbound) '()) [((arr: ss s #f (cons s-dty dbound) '())
(arr: ts t #f (cons t-dty dbound) '())) (arr: ts t #f (cons t-dty dbound) '()))
(unless (= (length ss) (length ts)) #:return-unless (= (length ss) (length ts))
(fail! ss ts)) #f
;; If we want to infer the dotted bound, then why is it in both types? ;; If we want to infer the dotted bound, then why is it in both types?
(when (memq dbound Y) #:return-when (memq dbound Y)
(fail! s-arr t-arr)) #f
(let* ([arg-mapping (cgen/list V X Y ts ss)] (let* ([arg-mapping (cgen/list V X Y ts ss)]
[darg-mapping (cgen V X Y t-dty s-dty)] [darg-mapping (cgen V X Y t-dty s-dty)]
[ret-mapping (cg s t)]) [ret-mapping (cg s t)])
(cset-meet* (% cset-meet*
(list arg-mapping darg-mapping ret-mapping)))] (% list arg-mapping darg-mapping ret-mapping)))]
;; bounds are different ;; bounds are different
[((arr: ss s #f (cons s-dty (? (λ (db) (memq db Y)) dbound)) '()) [((arr: ss s #f (cons s-dty (? (λ (db) (memq db Y)) dbound)) '())
(arr: ts t #f (cons t-dty dbound*) '())) (arr: ts t #f (cons t-dty dbound*) '()))
(unless (= (length ss) (length ts)) (fail! ss ts)) #:return-unless (= (length ss) (length ts)) #f
(when (memq dbound* Y) (fail! s-arr t-arr)) #:return-when (memq dbound* Y) #f
(let* ([arg-mapping (cgen/list V X Y ts ss)] (let* ([arg-mapping (cgen/list V X Y ts ss)]
;; just add dbound as something that can be constrained ;; just add dbound as something that can be constrained
[darg-mapping (move-dotted-rest-to-dmap (cgen V (cons dbound X) Y t-dty s-dty) dbound)] [darg-mapping (% move-dotted-rest-to-dmap (cgen V (cons dbound X) Y t-dty s-dty) dbound)]
[ret-mapping (cg s t)]) [ret-mapping (cg s t)])
(cset-meet* (% cset-meet*
(list arg-mapping darg-mapping ret-mapping)))] (% list arg-mapping darg-mapping ret-mapping)))]
[((arr: ss s #f (cons s-dty dbound) '()) [((arr: ss s #f (cons s-dty dbound) '())
(arr: ts t #f (cons t-dty (? (λ (db) (memq db Y)) dbound*)) '())) (arr: ts t #f (cons t-dty (? (λ (db) (memq db Y)) dbound*)) '()))
(unless (= (length ss) (length ts)) (fail! ss ts)) #:return-unless (= (length ss) (length ts)) #f
(let* ([arg-mapping (cgen/list V X Y ts ss)] (let* ([arg-mapping (cgen/list V X Y ts ss)]
;; just add dbound as something that can be constrained ;; just add dbound as something that can be constrained
[darg-mapping (move-dotted-rest-to-dmap (cgen V (cons dbound* X) Y t-dty s-dty) dbound*)] [darg-mapping (% move-dotted-rest-to-dmap
(cgen V (cons dbound* X) Y t-dty s-dty) dbound*)]
[ret-mapping (cg s t)]) [ret-mapping (cg s t)])
(cset-meet* (% cset-meet*
(list arg-mapping darg-mapping ret-mapping)))] (% list arg-mapping darg-mapping ret-mapping)))]
;; * <: ... ;; * <: ...
[((arr: ss s s-rest #f '()) [((arr: ss s s-rest #f '())
(arr: ts t #f (cons t-dty dbound) '())) (arr: ts t #f (cons t-dty dbound) '()))
(unless (memq dbound Y) #:return-unless (memq dbound Y)
(fail! s-arr t-arr)) #f
(if (<= (length ss) (length ts)) (if (<= (length ss) (length ts))
;; the simple case ;; the simple case
(let* ([arg-mapping (cgen/list V X Y ts (extend ts ss s-rest))] (let* ([arg-mapping (cgen/list V X Y ts (extend ts ss s-rest))]
[darg-mapping (move-rest-to-dmap (cgen V (cons dbound X) Y t-dty s-rest) dbound)] [darg-mapping (% move-rest-to-dmap
(cgen V (cons dbound X) Y t-dty s-rest) dbound)]
[ret-mapping (cg s t)]) [ret-mapping (cg s t)])
(cset-meet* (list arg-mapping darg-mapping ret-mapping))) (% cset-meet* (% list arg-mapping darg-mapping ret-mapping)))
;; the hard case ;; the hard case
(let* ([vars (var-store-take dbound t-dty (- (length ss) (length ts)))] (let* ([vars (var-store-take dbound t-dty (- (length ss) (length ts)))]
[new-tys (for/list ([var (in-list vars)]) [new-tys (for/list ([var (in-list vars)])
(substitute (make-F var) dbound t-dty))] (substitute (make-F var) dbound t-dty))]
[new-t-arr (make-arr (append ts new-tys) t #f (cons t-dty dbound) null)] [new-t-arr (make-arr (append ts new-tys) t #f (cons t-dty dbound) null)]
[new-cset (cgen/arr V (append vars X) Y s-arr new-t-arr)]) [new-cset (cgen/arr V (append vars X) Y s-arr new-t-arr)])
(move-vars+rest-to-dmap new-cset dbound vars)))] (% move-vars+rest-to-dmap new-cset dbound vars)))]
;; If dotted <: starred is correct, add it below. Not sure it is. ;; If dotted <: starred is correct, add it below. Not sure it is.
[((arr: ss s #f (cons s-dty dbound) '()) [((arr: ss s #f (cons s-dty dbound) '())
(arr: ts t t-rest #f '())) (arr: ts t t-rest #f '()))
(unless (memq dbound Y) #:return-unless (memq dbound Y)
(fail! s-arr t-arr)) #f
(cond [(< (length ss) (length ts)) (cond [(< (length ss) (length ts))
;; the hard case ;; the hard case
(let* ([vars (var-store-take dbound s-dty (- (length ts) (length ss)))] (let* ([vars (var-store-take dbound s-dty (- (length ts) (length ss)))]
@ -310,21 +319,25 @@
(substitute (make-F var) dbound s-dty))] (substitute (make-F var) dbound s-dty))]
[new-s-arr (make-arr (append ss new-tys) s #f (cons s-dty dbound) null)] [new-s-arr (make-arr (append ss new-tys) s #f (cons s-dty dbound) null)]
[new-cset (cgen/arr V (append vars X) Y new-s-arr t-arr)]) [new-cset (cgen/arr V (append vars X) Y new-s-arr t-arr)])
(move-vars+rest-to-dmap new-cset dbound vars #:exact #t))] (and new-cset vars
(move-vars+rest-to-dmap new-cset dbound vars #:exact #t)))]
[(= (length ss) (length ts)) [(= (length ss) (length ts))
;; the simple case ;; the simple case
(let* ([arg-mapping (cgen/list V X Y (extend ss ts t-rest) ss)] (let* ([arg-mapping (cgen/list V X Y (extend ss ts t-rest) ss)]
[darg-mapping (move-rest-to-dmap (cgen V (cons dbound X) Y t-rest s-dty) dbound #:exact #t)] [rest-mapping (cgen V (cons dbound X) Y t-rest s-dty)]
[darg-mapping (and rest-mapping
(move-rest-to-dmap
rest-mapping dbound #:exact #t))]
[ret-mapping (cg s t)]) [ret-mapping (cg s t)])
(cset-meet* (list arg-mapping darg-mapping ret-mapping)))] (% cset-meet* (% list arg-mapping darg-mapping ret-mapping)))]
[else [else #f])]
(fail! s-arr t-arr)])] [(_ _) #f]))
[(_ _) (fail! s-arr t-arr)]))
(define/cond-contract (cgen/flds V X Y flds-s flds-t) (define/cond-contract (cgen/flds V X Y flds-s flds-t)
((listof symbol?) (listof symbol?) (listof symbol?) (listof fld?) (listof fld?) . -> . cset?) ((listof symbol?) (listof symbol?) (listof symbol?) (listof fld?) (listof fld?)
(cset-meet* . -> . (or/c #f cset?))
(for/list ([s (in-list flds-s)] [t (in-list flds-t)]) (% cset-meet*
(for/list/fail ([s (in-list flds-s)] [t (in-list flds-t)])
(match* (s t) (match* (s t)
;; mutable - invariant ;; mutable - invariant
[((fld: s _ #t) (fld: t _ #t)) (cset-meet (cgen V X Y s t) (cgen V X Y t s))] [((fld: s _ #t) (fld: t _ #t)) (cset-meet (cgen V X Y s t) (cgen V X Y t s))]
@ -341,26 +354,30 @@
;; the index variables from the TOPLAS paper ;; the index variables from the TOPLAS paper
(define/cond-contract (cgen V X Y S T) (define/cond-contract (cgen V X Y S T)
((listof symbol?) (listof symbol?) (listof symbol?) ((listof symbol?) (listof symbol?) (listof symbol?)
(or/c Values/c ValuesDots? AnyValues?) (or/c Values/c ValuesDots? AnyValues?) . -> . cset?) (or/c Values/c ValuesDots? AnyValues?) (or/c Values/c ValuesDots? AnyValues?)
. -> . (or/c #F cset?))
;; useful quick loop ;; useful quick loop
(define/cond-contract (cg S T) (define/cond-contract (cg S T)
(Type/c Type/c . -> . cset?) (Type/c Type/c . -> . (or/c #f cset?))
(cgen V X Y S T)) (cgen V X Y S T))
;; this places no constraints on any variables in X ;; this places no constraints on any variables in X
(define empty (empty-cset X Y)) (define empty (empty-cset X Y))
;; this constrains just x (which is a single var) ;; this constrains just x (which is a single var)
(define (singleton S x T) (define (singleton S x T)
(insert empty x S T)) (insert empty x S T))
;; FIXME -- figure out how to use parameters less here
;; subtyping doesn't need to use it quite as much
(define cs (current-seen))
;; if we've been around this loop before, we're done (for rec types) ;; if we've been around this loop before, we're done (for rec types)
(if (seen? S T) (if (seen? S T cs)
empty empty
(parameterize ([match-equality-test (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b)))] (parameterize (;; remember S and T, and obtain everything we've seen from the context
;; remember S and T, and obtain everything we've seen from the context ;; we can't make this an argument since we may call back and forth with
;; we can't make this an argument since we may call back and forth with subtyping, for example ;; subtyping, for example
[current-seen (remember S T (current-seen))]) [current-seen (remember S T cs)])
(match* (S T) (match*/early (S T)
;; if they're equal, no constraints are necessary (CG-Refl) ;; if they're equal, no constraints are necessary (CG-Refl)
[(a a) empty] [(a b) #:when (type-equal? a b) empty]
;; CG-Top ;; CG-Top
[(_ (Univ:)) empty] [(_ (Univ:)) empty]
[(_ (AnyValues:)) empty] [(_ (AnyValues:)) empty]
@ -370,23 +387,25 @@
;; check each element ;; check each element
[((Result: s f-s o-s) [((Result: s f-s o-s)
(Result: t f-t o-t)) (Result: t f-t o-t))
(cset-meet* (list (cg s t) (% cset-meet* (% list
(cg s t)
(cgen/filter-set V X Y f-s f-t) (cgen/filter-set V X Y f-s f-t)
(cgen/object V X Y o-s o-t)))] (cgen/object V X Y o-s o-t)))]
;; values are covariant ;; values are covariant
[((Values: ss) (Values: ts)) [((Values: ss) (Values: ts))
(unless (= (length ss) (length ts)) #:return-unless (= (length ss) (length ts))
(fail! ss ts)) #f
(cgen/list V X Y ss ts)] (cgen/list V X Y ss ts)]
;; this constrains `dbound' to be |ts| - |ss| ;; this constrains `dbound' to be |ts| - |ss|
[((ValuesDots: ss s-dty dbound) (Values: ts)) [((ValuesDots: ss s-dty dbound) (Values: ts))
(unless (>= (length ts) (length ss)) (fail! ss ts)) #:return-unless (>= (length ts) (length ss)) #f
(unless (memq dbound Y) (fail! S T)) #:return-unless (memq dbound Y) #f
(let* ([vars (var-store-take dbound s-dty (- (length ts) (length ss)))] (let* ([vars (var-store-take dbound s-dty (- (length ts) (length ss)))]
;; new-tys are dummy plain type variables, standing in for the elements of dbound that need to be generated ;; new-tys are dummy plain type variables,
;; standing in for the elements of dbound that need to be generated
[new-tys (for/list ([var (in-list vars)]) [new-tys (for/list ([var (in-list vars)])
;; must be a Result since we are matching these against ;; must be a Result since we are matching these against
;; the contents of the `Values`, which are Results ;; the contents of the `Values`, which are Results
@ -394,12 +413,12 @@
;; generate constraints on the prefixes, and on the dummy types ;; generate constraints on the prefixes, and on the dummy types
[new-cset (cgen/list V (append vars X) Y (append ss new-tys) ts)]) [new-cset (cgen/list V (append vars X) Y (append ss new-tys) ts)])
;; now take all the dummy types, and use them to constrain dbound appropriately ;; now take all the dummy types, and use them to constrain dbound appropriately
(move-vars-to-dmap new-cset dbound vars))] (% move-vars-to-dmap new-cset dbound vars))]
;; like the case above, but constrains `dbound' to be |ss| - |ts| ;; like the case above, but constrains `dbound' to be |ss| - |ts|
[((Values: ss) (ValuesDots: ts t-dty dbound)) [((Values: ss) (ValuesDots: ts t-dty dbound))
(unless (>= (length ss) (length ts)) (fail! ss ts)) #:return-unless (>= (length ss) (length ts)) #f
(unless (memq dbound Y) (fail! S T)) #:return-unless (memq dbound Y) #f
;; see comments for last case, this case swaps `s` and `t` order ;; see comments for last case, this case swaps `s` and `t` order
(let* ([vars (var-store-take dbound t-dty (- (length ss) (length ts)))] (let* ([vars (var-store-take dbound t-dty (- (length ss) (length ts)))]
@ -410,25 +429,27 @@
;; identical bounds - just unify pairwise ;; identical bounds - just unify pairwise
[((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound)) [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound))
(when (memq dbound Y) (fail! ss ts)) #:return-when (memq dbound Y) #f
(cgen/list V X Y (cons s-dty ss) (cons t-dty ts))] (cgen/list V X Y (cons s-dty ss) (cons t-dty ts))]
[((ValuesDots: ss s-dty (? (λ (db) (memq db Y)) s-dbound)) (ValuesDots: ts t-dty t-dbound)) [((ValuesDots: ss s-dty (? (λ (db) (memq db Y)) s-dbound))
(ValuesDots: ts t-dty t-dbound))
;; What should we do if both are in Y? ;; What should we do if both are in Y?
(when (memq t-dbound Y) (fail! S T)) #:return-when (memq t-dbound Y) #f
(cset-meet (% cset-meet
(cgen/list V X Y ss ts) (cgen/list V X Y ss ts)
(move-dotted-rest-to-dmap (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound))] (% move-dotted-rest-to-dmap
[((ValuesDots: ss s-dty s-dbound) (ValuesDots: ts t-dty (? (λ (db) (memq db Y)) t-dbound))) (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound))]
[((ValuesDots: ss s-dty s-dbound)
(ValuesDots: ts t-dty (? (λ (db) (memq db Y)) t-dbound)))
;; s-dbound can't be in Y, due to previous rule ;; s-dbound can't be in Y, due to previous rule
(cset-meet (% cset-meet
(cgen/list V X Y ss ts) (cgen/list V X Y ss ts)
(move-dotted-rest-to-dmap (cgen V (cons t-dbound X) Y s-dty t-dty) t-dbound))] (% move-dotted-rest-to-dmap (cgen V (cons t-dbound X) Y s-dty t-dty) t-dbound))]
;; they're subtypes. easy. ;; they're subtypes. easy.
[(a b) (=> nevermind) [(a b)
(if (subtype a b) #:when (subtype a b)
empty empty]
(nevermind))]
;; refinements are erased to their bound ;; refinements are erased to their bound
[((Refinement: S _) T) [((Refinement: S _) T)
@ -437,18 +458,21 @@
;; variables that are in X and should be constrained ;; variables that are in X and should be constrained
;; all other variables are compatible only with themselves ;; all other variables are compatible only with themselves
[((F: (? (λ (e) (memq e X)) v)) T) [((F: (? (λ (e) (memq e X)) v)) T)
#:return-when
(match T (match T
;; fail when v* is an index variable ;; fail when v* is an index variable
[(F: v*) (when (and (bound-index? v*) (not (bound-tvar? v*))) [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
(fail! S T))] [_ #f])
[_ (void)]) #f
;; constrain v to be below T (but don't mention V) ;; constrain v to be below T (but don't mention V)
(singleton (Un) v (var-demote T V))] (singleton (Un) v (var-demote T V))]
[(S (F: (? (lambda (e) (memq e X)) v))) [(S (F: (? (lambda (e) (memq e X)) v)))
#:return-when
(match S (match S
[(F: v*) (when (and (bound-index? v*) (not (bound-tvar? v*))) [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
(fail! S T))] [_ #f])
[_ (void)]) #f
;; constrain v to be above S (but don't mention V) ;; constrain v to be above S (but don't mention V)
(singleton (var-promote S V) v Univ)] (singleton (var-promote S V) v Univ)]
@ -462,60 +486,62 @@
[((Poly: v1 b1) T) (cgen (append v1 V) X Y b1 T)] [((Poly: v1 b1) T) (cgen (append v1 V) X Y b1 T)]
;; constrain *each* element of es to be below T, and then combine the constraints ;; constrain *each* element of es to be below T, and then combine the constraints
[((Union: es) T) (cset-meet* (cons empty (for/list ([e (in-list es)]) (cg e T))))] [((Union: es) T)
(define cs (for/list/fail ([e (in-list es)]) (cg e T)))
(and cs (cset-meet* (cons empty cs)))]
;; find *an* element of es which can be made to be a supertype of S ;; find *an* element of es which can be made to be a supertype of S
;; FIXME: we're using multiple csets here, but I don't think it makes a difference ;; FIXME: we're using multiple csets here, but I don't think it makes a difference
;; not using multiple csets will break for: ??? ;; not using multiple csets will break for: ???
[(S (Union: es)) [(S (Union: es))
(cset-combine (cset-join
(filter values (for*/list ([e (in-list es)]
(for/list ([e (in-list es)]) [v (in-value (cg S e))]
(with-handlers ([exn:infer? (λ _ #f)]) (cg S e)))))] #:when v)
v))]
;; two structs with the same name ;; two structs with the same name
;; just check pairwise on the fields ;; just check pairwise on the fields
[((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _)) (=> nevermind) [((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _))
(unless (free-identifier=? nm nm*) (nevermind)) #:when (free-identifier=? nm nm*)
(let ([proc-c (let ([proc-c
(cond [(and proc proc*) (cond [(and proc proc*)
(cg proc proc*)] (cg proc proc*)]
[proc* (fail! S T)] [proc* #f]
[else empty])]) [else empty])])
(cset-meet proc-c (cgen/flds V X Y flds flds*)))] (% cset-meet proc-c (cgen/flds V X Y flds flds*)))]
;; two struct names, need to resolve b/c one could be a parent ;; two struct names, need to resolve b/c one could be a parent
[((Name: n _ _ #t) (Name: n* _ _ #t)) [((Name: n _ _ #t) (Name: n* _ _ #t))
(if (free-identifier=? n n*) (if (free-identifier=? n n*)
null empty ;; just succeed now
(let ((rn (resolve-once S)) (rn* (resolve-once T))) (% cg (resolve-once S) (resolve-once T)))]
(if (and rn rn*) (cg rn rn*) (fail! S T))))]
;; pairs are pointwise ;; pairs are pointwise
[((Pair: a b) (Pair: a* b*)) [((Pair: a b) (Pair: a* b*))
(cset-meet (cg a a*) (cg b b*))] (% cset-meet (cg a a*) (cg b b*))]
;; sequences are covariant ;; sequences are covariant
[((Sequence: ts) (Sequence: ts*)) [((Sequence: ts) (Sequence: ts*))
(cgen/list V X Y ts ts*)] (cgen/list V X Y ts ts*)]
[((Listof: t) (Sequence: (list t*))) [((Listof: t) (Sequence: (list t*)))
(cg t t*)] (cg t t*)]
[((Pair: t1 t2) (Sequence: (list t*))) [((Pair: t1 t2) (Sequence: (list t*)))
(cset-meet (cg t1 t*) (cg t2 (-lst t*)))] (% cset-meet (cg t1 t*) (cg t2 (-lst t*)))]
[((MListof: t) (Sequence: (list t*))) [((MListof: t) (Sequence: (list t*)))
(cg t t*)] (cg t t*)]
;; To check that mutable pair is a sequence we check that the cdr is ;; To check that mutable pair is a sequence we check that the cdr is
;; both an mutable list and a sequence ;; both an mutable list and a sequence
[((MPair: t1 t2) (Sequence: (list t*))) [((MPair: t1 t2) (Sequence: (list t*)))
(cset-meet* (list (cg t1 t*) (cg t2 T) (cg t2 (Un (-val null) (make-MPairTop)))))] (% cset-meet* (% list (cg t1 t*) (cg t2 T) (cg t2 (Un (-val null) (make-MPairTop)))))]
[((List: ts) (Sequence: (list t*))) [((List: ts) (Sequence: (list t*)))
(cset-meet* (for/list ([t (in-list ts)]) (% cset-meet* (for/list/fail ([t (in-list ts)])
(cg t t*)))] (cg t t*)))]
[((HeterogeneousVector: ts) (HeterogeneousVector: ts*)) [((HeterogeneousVector: ts) (HeterogeneousVector: ts*))
(cset-meet (cgen/list V X Y ts ts*) (cgen/list V X Y ts* ts))] (% cset-meet (cgen/list V X Y ts ts*) (cgen/list V X Y ts* ts))]
[((HeterogeneousVector: ts) (Vector: s)) [((HeterogeneousVector: ts) (Vector: s))
(define ts* (map (λ _ s) ts)) ;; invariant, everything has to match (define ts* (map (λ _ s) ts)) ;; invariant, everything has to match
(cset-meet (cgen/list V X Y ts ts*) (cgen/list V X Y ts* ts))] (% cset-meet (cgen/list V X Y ts ts*) (cgen/list V X Y ts* ts))]
[((HeterogeneousVector: ts) (Sequence: (list t*))) [((HeterogeneousVector: ts) (Sequence: (list t*)))
(cset-meet* (for/list ([t (in-list ts)]) (% cset-meet* (for/list/fail ([t (in-list ts)])
(cg t t*)))] (cg t t*)))]
[((Vector: t) (Sequence: (list t*))) [((Vector: t) (Sequence: (list t*)))
(cg t t*)] (cg t t*)]
@ -542,9 +568,7 @@
(define type (define type
(for/or ([t (in-list (list -Byte -Index -NonNegFixnum -Nat))]) (for/or ([t (in-list (list -Byte -Index -NonNegFixnum -Nat))])
(and (subtype S t) t))) (and (subtype S t) t)))
(if type (% cg type t*)]
(cg type t*)
(fail! S T))]
[((Vector: t) (Sequence: (list t*))) [((Vector: t) (Sequence: (list t*)))
(cg t t*)] (cg t t*)]
[((Hashtable: k v) (Sequence: (list k* v*))) [((Hashtable: k v) (Sequence: (list k* v*)))
@ -554,7 +578,7 @@
;; ListDots can be below a Listof ;; ListDots can be below a Listof
;; must be above mu unfolding ;; must be above mu unfolding
[((ListDots: s-dty dbound) (Listof: t-elem)) [((ListDots: s-dty dbound) (Listof: t-elem))
(when (memq dbound Y) (fail! S T)) #:return-when (memq dbound Y) #f
(cgen V X Y (substitute Univ dbound s-dty) t-elem)] (cgen V X Y (substitute Univ dbound s-dty) t-elem)]
;; two ListDots with the same bound, just check the element type ;; two ListDots with the same bound, just check the element type
;; This is conservative because we don't try to infer a constraint on dbound. ;; This is conservative because we don't try to infer a constraint on dbound.
@ -562,7 +586,7 @@
(cgen V X Y s-dty t-dty)] (cgen V X Y s-dty t-dty)]
[((ListDots: s-dty (? (λ (db) (memq db Y)) s-dbound)) (ListDots: t-dty t-dbound)) [((ListDots: s-dty (? (λ (db) (memq db Y)) s-dbound)) (ListDots: t-dty t-dbound))
;; What should we do if both are in Y? ;; What should we do if both are in Y?
(when (memq t-dbound Y) (fail! S T)) #:return-when (memq t-dbound Y) #f
(move-dotted-rest-to-dmap (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound)] (move-dotted-rest-to-dmap (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound)]
[((ListDots: s-dty s-dbound) (ListDots: t-dty (? (λ (db) (memq db Y)) t-dbound))) [((ListDots: s-dty s-dbound) (ListDots: t-dty (? (λ (db) (memq db Y)) t-dbound)))
;; s-dbound can't be in Y, due to previous rule ;; s-dbound can't be in Y, due to previous rule
@ -570,20 +594,20 @@
;; this constrains `dbound' to be |ts| - |ss| ;; this constrains `dbound' to be |ts| - |ss|
[((ListDots: s-dty dbound) (List: ts)) [((ListDots: s-dty dbound) (List: ts))
(unless (memq dbound Y) (fail! S T)) #:return-unless (memq dbound Y) #f
(let* ([vars (var-store-take dbound s-dty (length ts))] (let* ([vars (var-store-take dbound s-dty (length ts))]
;; new-tys are dummy plain type variables, standing in for the elements of dbound that need to be generated ;; new-tys are dummy plain type variables,
;; standing in for the elements of dbound that need to be generated
[new-tys (for/list ([var (in-list vars)]) [new-tys (for/list ([var (in-list vars)])
(substitute (make-F var) dbound s-dty))] (substitute (make-F var) dbound s-dty))]
;; generate constraints on the prefixes, and on the dummy types ;; generate constraints on the prefixes, and on the dummy types
[new-cset (cgen/list V (append vars X) Y new-tys ts)]) [new-cset (cgen/list V (append vars X) Y new-tys ts)])
;; now take all the dummy types, and use them to constrain dbound appropriately ;; now take all the dummy types, and use them to constrain dbound appropriately
(move-vars-to-dmap new-cset dbound vars))] (% move-vars-to-dmap new-cset dbound vars))]
;; same as above, constrains `dbound' to be |ss| - |ts| ;; same as above, constrains `dbound' to be |ss| - |ts|
[((List: ss) (ListDots: t-dty dbound)) [((List: ss) (ListDots: t-dty dbound))
(unless (memq dbound Y) (fail! S T)) #:return-unless (memq dbound Y) #f
;; see comments for last case, we flip s and t though ;; see comments for last case, we flip s and t though
(let* ([vars (var-store-take dbound t-dty (length ss))] (let* ([vars (var-store-take dbound t-dty (length ss))]
@ -594,7 +618,8 @@
;; if we have two mu's, we rename them to have the same variable ;; if we have two mu's, we rename them to have the same variable
;; and then compare the bodies ;; and then compare the bodies
;; This relies on (B 0) only unifying with itself, and thus only hitting the first case of this `match' ;; This relies on (B 0) only unifying with itself,
;; and thus only hitting the first case of this `match'
[((Mu-unsafe: s) (Mu-unsafe: t)) [((Mu-unsafe: s) (Mu-unsafe: t))
(cg s t)] (cg s t)]
@ -604,11 +629,9 @@
;; resolve applications ;; resolve applications
[((App: _ _ _) _) [((App: _ _ _) _)
(let ((S* (resolve-once S))) (% cg (resolve-once S) T)]
(if S* (cg S* T) (fail! S T)))]
[(_ (App: _ _ _)) [(_ (App: _ _ _))
(let ((T* (resolve-once T))) (% cg S (resolve-once T))]
(if T* (cg S T*) (fail! S T)))]
;; If the struct names don't match, try the parent of S ;; If the struct names don't match, try the parent of S
;; Needs to be done after App and Mu in case T is actually the current struct ;; Needs to be done after App and Mu in case T is actually the current struct
@ -619,24 +642,24 @@
;; Invariant here because struct types aren't subtypes just because the ;; Invariant here because struct types aren't subtypes just because the
;; structs are (since you can make a constructor from the type). ;; structs are (since you can make a constructor from the type).
[((StructType: s) (StructType: t)) [((StructType: s) (StructType: t))
(cset-meet (cg s t) (cg t s))] (% cset-meet (cg s t) (cg t s))]
;; vectors are invariant - generate constraints *both* ways ;; vectors are invariant - generate constraints *both* ways
[((Vector: e) (Vector: e*)) [((Vector: e) (Vector: e*))
(cset-meet (cg e e*) (cg e* e))] (% cset-meet (cg e e*) (cg e* e))]
;; boxes are invariant - generate constraints *both* ways ;; boxes are invariant - generate constraints *both* ways
[((Box: e) (Box: e*)) [((Box: e) (Box: e*))
(cset-meet (cg e e*) (cg e* e))] (% cset-meet (cg e e*) (cg e* e))]
[((MPair: s t) (MPair: s* t*)) [((MPair: s t) (MPair: s* t*))
(cset-meet* (list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))] (% cset-meet* (% list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))]
[((Channel: e) (Channel: e*)) [((Channel: e) (Channel: e*))
(cset-meet (cg e e*) (cg e* e))] (% cset-meet (cg e e*) (cg e* e))]
[((ThreadCell: e) (ThreadCell: e*)) [((ThreadCell: e) (ThreadCell: e*))
(cset-meet (cg e e*) (cg e* e))] (% cset-meet (cg e e*) (cg e* e))]
[((Continuation-Mark-Keyof: e) (Continuation-Mark-Keyof: e*)) [((Continuation-Mark-Keyof: e) (Continuation-Mark-Keyof: e*))
(cset-meet (cg e e*) (cg e* e))] (% cset-meet (cg e e*) (cg e* e))]
[((Prompt-Tagof: s t) (Prompt-Tagof: s* t*)) [((Prompt-Tagof: s t) (Prompt-Tagof: s* t*))
(cset-meet* (list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))] (% cset-meet* (% list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))]
[((Promise: e) (Promise: e*)) [((Promise: e) (Promise: e*))
(cg e e*)] (cg e e*)]
[((Ephemeron: e) (Ephemeron: e*)) [((Ephemeron: e) (Ephemeron: e*))
@ -671,7 +694,7 @@
;; we assume all HTs are mutable at the moment ;; we assume all HTs are mutable at the moment
[((Hashtable: s1 s2) (Hashtable: t1 t2)) [((Hashtable: s1 s2) (Hashtable: t1 t2))
;; for mutable hash tables, both are invariant ;; for mutable hash tables, both are invariant
(cset-meet* (list (cg t1 s1) (cg s1 t1) (cg t2 s2) (cg s2 t2)))] (% cset-meet* (% list (cg t1 s1) (cg s1 t1) (cg t2 s2) (cg s2 t2)))]
;; syntax is covariant ;; syntax is covariant
[((Syntax: s1) (Syntax: s2)) [((Syntax: s1) (Syntax: s2))
(cg s1 s2)] (cg s1 s2)]
@ -680,26 +703,26 @@
(cg s1 s2)] (cg s1 s2)]
;; parameters are just like one-arg functions ;; parameters are just like one-arg functions
[((Param: in1 out1) (Param: in2 out2)) [((Param: in1 out1) (Param: in2 out2))
(cset-meet (cg in2 in1) (cg out1 out2))] (% cset-meet (cg in2 in1) (cg out1 out2))]
;; every function is trivially below top-arr ;; every function is trivially below top-arr
[((Function: _) [((Function: _)
(Function: (list (top-arr:)))) (Function: (list (top-arr:))))
empty] empty]
[((Function: (list s-arr ...)) [((Function: (list s-arr ...))
(Function: (list t-arr ...))) (Function: (list t-arr ...)))
(cset-meet* (% cset-meet*
(for/list ([t-arr (in-list t-arr)]) (for/list/fail ([t-arr (in-list t-arr)])
;; for each element of t-arr, we need to get at least one element of s-arr that works ;; for each element of t-arr, we need to get at least one element of s-arr that works
(let ([results (filter values (let ([results (for*/list ([s-arr (in-list s-arr)]
(for/list ([s-arr (in-list s-arr)]) [v (in-value (cgen/arr V X Y s-arr t-arr))]
(with-handlers ([exn:infer? (lambda (_) #f)]) #:when v)
(cgen/arr V X Y s-arr t-arr))))]) v)])
;; ensure that something produces a constraint set ;; ensure that something produces a constraint set
(when (null? results) (fail! S T)) (and (not (null? results))
(cset-combine results))))] (cset-join results)))))]
[(_ _) [(_ _)
;; nothing worked, and we fail ;; nothing worked, and we fail
(fail! S T)])))) #f]))))
;; C : cset? - set of constraints found by the inference engine ;; C : cset? - set of constraints found by the inference engine
;; Y : (listof symbol?) - index variables that must have entries ;; Y : (listof symbol?) - index variables that must have entries
@ -813,15 +836,14 @@
(define/cond-contract (cgen/list V X Y S T (define/cond-contract (cgen/list V X Y S T
#:expected-cset [expected-cset (empty-cset '() '())]) #:expected-cset [expected-cset (empty-cset '() '())])
(((listof symbol?) (listof symbol?) (listof symbol?) (listof Values/c) (listof Values/c)) (((listof symbol?) (listof symbol?) (listof symbol?) (listof Values/c) (listof Values/c))
(#:expected-cset cset?) . ->* . cset?) (#:expected-cset cset?) . ->* . (or/c cset? #f))
(unless (= (length S) (length T)) (and (= (length S) (length T))
(fail! S T)) (% cset-meet*
(cset-meet* (for/list/fail ([s (in-list S)] [t (in-list T)])
(for/list ([s (in-list S)] [t (in-list T)])
;; We meet early to prune the csets to a reasonable size. ;; We meet early to prune the csets to a reasonable size.
;; This weakens the inference a bit, but sometimes avoids ;; This weakens the inference a bit, but sometimes avoids
;; constraint explosion. ;; constraint explosion.
(cset-meet (cgen V X Y s t) expected-cset)))) (% cset-meet (cgen V X Y s t) expected-cset)))))
@ -841,13 +863,13 @@
(or/c #f Values/c ValuesDots?)) (or/c #f Values/c ValuesDots?))
((or/c #f Values/c AnyValues? ValuesDots?)) ((or/c #f Values/c AnyValues? ValuesDots?))
. ->* . (or/c boolean? substitution/c)) . ->* . (or/c boolean? substitution/c))
(with-handlers ([exn:infer? (lambda _ #f)])
(let* ([expected-cset (if expected (let* ([expected-cset (if expected
(cgen null X Y R expected) (cgen null X Y R expected)
(empty-cset '() '()))] (empty-cset '() '()))]
[cs (cgen/list null X Y S T #:expected-cset expected-cset)] [cs (and expected-cset
[cs* (cset-meet cs expected-cset)]) (cgen/list null X Y S T #:expected-cset expected-cset))]
(if R (subst-gen cs* Y R) #t)))) [cs* (% cset-meet cs expected-cset)])
(and cs* (if R (subst-gen cs* Y R) #t))))
infer)) ;to export a variable binding and not syntax infer)) ;to export a variable binding and not syntax
;; like infer, but T-var is the vararg type: ;; like infer, but T-var is the vararg type:
@ -859,22 +881,30 @@
;; like infer, but dotted-var is the bound on the ... ;; like infer, but dotted-var is the bound on the ...
;; and T-dotted is the repeated type ;; and T-dotted is the repeated type
(define (infer/dots X dotted-var S T T-dotted R must-vars #:expected [expected #f]) (define (infer/dots X dotted-var S T T-dotted R must-vars #:expected [expected #f])
(with-handlers ([exn:infer? (lambda _ #f)]) (early-return
(let* ([short-S (take S (length T))] (define short-S (take S (length T)))
[rest-S (drop S (length T))] (define rest-S (drop S (length T)))
[expected-cset (if expected (define expected-cset (if expected
(cgen null X (list dotted-var) R expected) (cgen null X (list dotted-var) R expected)
(empty-cset '() '()))] (empty-cset '() '())))
[cs-short (cgen/list null X (list dotted-var) short-S T #:return-unless expected-cset #f
#:expected-cset expected-cset)] (define cs-short (cgen/list null X (list dotted-var) short-S T
[new-vars (var-store-take dotted-var T-dotted (length rest-S))] #:expected-cset expected-cset))
[new-Ts (for/list ([v (in-list new-vars)]) #:return-unless cs-short #f
(define new-vars (var-store-take dotted-var T-dotted (length rest-S)))
(define new-Ts (for/list ([v (in-list new-vars)])
(substitute (make-F v) dotted-var (substitute (make-F v) dotted-var
(substitute-dots (map make-F new-vars) #f dotted-var T-dotted)))] (substitute-dots (map make-F new-vars)
[cs-dotted (cgen/list null (append new-vars X) (list dotted-var) rest-S new-Ts #f dotted-var T-dotted))))
#:expected-cset expected-cset)] (define cs-dotted (cgen/list null (append new-vars X) (list dotted-var) rest-S new-Ts
[cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars)] #:expected-cset expected-cset))
[cs (cset-meet cs-short cs-dotted*)]) #:return-unless cs-dotted #f
(subst-gen (cset-meet cs expected-cset) (list dotted-var) R)))) (define cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars))
#:return-unless cs-dotted* #f
(define cs (cset-meet cs-short cs-dotted*))
#:return-unless cs #f
(define m (cset-meet cs expected-cset))
#:return-unless m #f
(subst-gen m (list dotted-var) R)))
;(trace cgen)

16
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/signatures.rkt
View File

@ -7,26 +7,20 @@
(provide (all-defined-out)) (provide (all-defined-out))
(define-signature dmap^ (define-signature dmap^
([cond-contracted dmap-meet (dmap? dmap? . -> . dmap?)])) ([cond-contracted dmap-meet (dmap? dmap? . -> . (or/c #f dmap?))]))
(define-signature promote-demote^ (define-signature promote-demote^
([cond-contracted var-promote (Type/c (listof symbol?) . -> . Type/c)] ([cond-contracted var-promote (Type/c (listof symbol?) . -> . Type/c)]
[cond-contracted var-demote (Type/c (listof symbol?) . -> . Type/c)])) [cond-contracted var-demote (Type/c (listof symbol?) . -> . Type/c)]))
(define-signature constraints^ (define-signature constraints^
([cond-contracted exn:infer? (any/c . -> . boolean?)] ([cond-contracted cset-meet (cset? cset? . -> . (or/c #f cset?))]
[cond-contracted fail-sym symbol?] [cond-contracted cset-meet* ((listof cset?) . -> . (or/c #f cset?))]
;; inference failure - masked before it gets to the user program
(define-syntaxes (fail!)
(syntax-rules ()
[(_ s t) (raise (list fail-sym s t))]))
[cond-contracted cset-meet (cset? cset? . -> . cset?)]
[cond-contracted cset-meet* ((listof cset?) . -> . cset?)]
no-constraint no-constraint
[cond-contracted empty-cset ((listof symbol?) (listof symbol?) . -> . cset?)] [cond-contracted empty-cset ((listof symbol?) (listof symbol?) . -> . cset?)]
[cond-contracted insert (cset? symbol? Type/c Type/c . -> . cset?)] [cond-contracted insert (cset? symbol? Type/c Type/c . -> . cset?)]
[cond-contracted cset-combine ((listof cset?) . -> . cset?)] [cond-contracted cset-join ((listof cset?) . -> . cset?)]
[cond-contracted c-meet ((c? c?) (symbol?) . ->* . c?)])) [cond-contracted c-meet ((c? c?) (symbol?) . ->* . (or/c #f c?))]))
(define-signature restrict^ (define-signature restrict^
([cond-contracted restrict ((Type/c Type/c) ((or/c 'new 'orig)) . ->* . Type/c)])) ([cond-contracted restrict ((Type/c Type/c) ((or/c 'new 'orig)) . ->* . Type/c)]))

4
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-below.rkt
View File

@ -9,9 +9,9 @@
(only-in (types printer) pretty-format-type)) (only-in (types printer) pretty-format-type))
(provide/cond-contract (provide/cond-contract
[check-below (-->i ([s (-or/c Type/c full-tc-results/c)] [check-below (-->i ([s (-or/c Type/c tc-results/c)]
[t (s) (if (Type/c? s) Type/c tc-results/c)]) [t (s) (if (Type/c? s) Type/c tc-results/c)])
[_ (s) (if (Type/c? s) Type/c full-tc-results/c)])] [_ (s) (if (Type/c? s) Type/c tc-results/c)])]
[cond-check-below (-->i ([s (-or/c Type/c full-tc-results/c)] [cond-check-below (-->i ([s (-or/c Type/c full-tc-results/c)]
[t (s) (-or/c #f (if (Type/c? s) Type/c tc-results/c))]) [t (s) (-or/c #f (if (Type/c? s) Type/c tc-results/c))])
[_ (s) (-or/c #f (if (Type/c? s) Type/c full-tc-results/c))])] [_ (s) (-or/c #f (if (Type/c? s) Type/c full-tc-results/c))])]

2
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/signatures.rkt
View File

@ -7,7 +7,7 @@
(define-signature tc-expr^ (define-signature tc-expr^
([cond-contracted tc-expr (syntax? . -> . full-tc-results/c)] ([cond-contracted tc-expr (syntax? . -> . full-tc-results/c)]
[cond-contracted tc-expr/check (syntax? tc-results/c . -> . full-tc-results/c)] [cond-contracted tc-expr/check (syntax? tc-results/c . -> . tc-results/c)]
[cond-contracted tc-expr/check/t (syntax? tc-results/c . -> . Type/c)] [cond-contracted tc-expr/check/t (syntax? tc-results/c . -> . Type/c)]
[cond-contracted tc-body (syntax? . -> . full-tc-results/c)] [cond-contracted tc-body (syntax? . -> . full-tc-results/c)]
[cond-contracted tc-body/check (syntax? tc-results/c . -> . full-tc-results/c)] [cond-contracted tc-body/check (syntax? tc-results/c . -> . full-tc-results/c)]

2
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
View File

@ -86,7 +86,7 @@
;; tc-expr/check : syntax tc-results -> tc-results ;; tc-expr/check : syntax tc-results -> tc-results
(define/cond-contract (tc-expr/check/internal form expected) (define/cond-contract (tc-expr/check/internal form expected)
(--> syntax? tc-results/c full-tc-results/c) (--> syntax? tc-results/c tc-results/c)
(parameterize ([current-orig-stx form]) (parameterize ([current-orig-stx form])
;(printf "form: ~a\n" (syntax-object->datum form)) ;(printf "form: ~a\n" (syntax-object->datum form))
;; the argument must be syntax ;; the argument must be syntax

2
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
View File

@ -37,7 +37,7 @@
;; TODO: make this function sane. ;; TODO: make this function sane.
(define/cond-contract (do-check expr->type namess expected-results exprs body expected) (define/cond-contract (do-check expr->type namess expected-results exprs body expected)
((syntax? tc-results/c . -> . any/c) ((syntax? tc-results/c . -> . any/c)
(listof (listof identifier?)) (listof tc-results/c) (listof tc-results/c) (listof (listof identifier?)) (listof tc-results/c)
(listof syntax?) syntax? (or/c #f tc-results/c) (listof syntax?) syntax? (or/c #f tc-results/c)
. -> . . -> .
tc-results/c) tc-results/c)

12
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
View File

@ -3,7 +3,7 @@
racket/match racket/function racket/lazy-require racket/list racket/match racket/function racket/lazy-require racket/list
(prefix-in c: (contract-req)) (prefix-in c: (contract-req))
(rep type-rep filter-rep object-rep rep-utils) (rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils) (utils tc-utils early-return)
(types utils resolve base-abbrev match-expanders (types utils resolve base-abbrev match-expanders
numeric-tower substitute current-seen) numeric-tower substitute current-seen)
(for-syntax racket/base syntax/parse unstable/sequence)) (for-syntax racket/base syntax/parse unstable/sequence))
@ -226,16 +226,6 @@
(subtype* s t) (subtype* s t)
(subtype* t s))) (subtype* t s)))
(define-syntax (early-return stx)
(syntax-parse stx
[(_ e:expr ... #:return-when e0:expr e1:expr rest ...)
#'(let ()
e ...
(if e0 e1
(early-return rest ...)))]
[(_ e:expr ...) #'(let () e ...)]))
(define bottom-key (Rep-seq -Bottom)) (define bottom-key (Rep-seq -Bottom))
(define top-key (Rep-seq Univ)) (define top-key (Rep-seq Univ))

24
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/early-return.rkt Normal file
View File

@ -0,0 +1,24 @@
#lang racket/base
(require (for-syntax racket/base syntax/parse))
(provide early-return)
(define-syntax (early-return stx)
(syntax-parse stx
[(_ e:expr ... #:return-when e0:expr e1:expr rest ...)
(syntax/loc stx
(let ()
e ...
(if e0 e1
(early-return rest ...))))]
[(_ e:expr ... #:return-unless e0:expr e1:expr rest ...)
(syntax/loc stx
(let ()
e ...
(if e0
(early-return rest ...)
e1)))]
[(_ e:expr ...) (syntax/loc stx (let () e ...))]))

16
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/values-dots2.rkt Normal file
View File

@ -0,0 +1,16 @@
#lang typed/racket/base
(: map-with-funcs (All (b c d e ) ((b c d e -> b)
(b c d e -> c)
(b c d e -> d)
(b c d e -> e)
->
(b c d e -> (List b c d e)))))
(define (map-with-funcs f1 f2 f3 f4)
(lambda (b0 c0 d0 e0 )
(list (f1 b0 c0 d0 e0 )
(f2 b0 c0 d0 e0 )
(f3 b0 c0 d0 e0 )
(f4 b0 c0 d0 e0 ))))
(map-with-funcs + - * /)

74
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt
View File

@ -7,7 +7,7 @@
(rep type-rep) (rep type-rep)
(r:infer infer) (r:infer infer)
(types numeric-tower utils abbrev)) (types union substitute numeric-tower utils abbrev))
(provide tests) (provide tests)
(gen-test-main) (gen-test-main)
@ -19,7 +19,7 @@
(fv ty*) (fv ty*)
(list (quote elems) ...)))) (list (quote elems) ...))))
(define-syntax (infer-t stx) (begin-for-syntax
(define-splicing-syntax-class vars (define-splicing-syntax-class vars
(pattern (~seq) #:with vars #'empty) (pattern (~seq) #:with vars #'empty)
(pattern (~seq #:vars vars:expr) )) (pattern (~seq #:vars vars:expr) ))
@ -29,14 +29,44 @@
(define-splicing-syntax-class pass (define-splicing-syntax-class pass
(pattern (~seq) #:with pass #'#t) (pattern (~seq) #:with pass #'#t)
(pattern #:pass #:with pass #'#t) (pattern #:pass #:with pass #'#t)
(pattern #:fail #:with pass #'#f)) (pattern #:fail #:with pass #'#f)))
(define-syntax (infer-t stx)
(syntax-parse stx (syntax-parse stx
([_ S:expr T:expr :vars :indices :pass] ([_ S:expr T:expr :vars :indices :pass]
#'(test-case "foobar" (syntax/loc stx
(test-case (format "~a ~a~a" S T (if pass "" " should fail"))
(define result (infer vars indices (list S) (list T) #f)) (define result (infer vars indices (list S) (list T) #f))
(unless (equal? result pass) (unless (equal? result pass)
(fail-check "Could not infer a substitution")))))) (fail-check "Could not infer a substitution")))))))
(define-syntax (infer-l stx)
(syntax-parse stx
([_ S:expr T:expr :vars :indices :pass]
(syntax/loc stx
(test-case (format "~a ~a~a" S T (if pass "" " should fail"))
(define result (infer vars indices S T #f))
(unless (equal? result pass)
(fail-check "Could not infer a substitution")))))))
(define-syntax-rule (i2-t t1 t2 (a b) ...)
(test-equal? (format "~a ~a" t1 t2)
(infer (fv t1) null (list t2) (list t1) (-lst* (make-F a) ...) #f)
(make-immutable-hash (list (cons a (t-subst b)) ...))))
(define-syntax-rule (i2-l t1 t2 fv (a b) ...)
(test-equal? (format "~a ~a" t2 t1)
(infer fv null t2 t1 (-lst* (make-F a) ...) #f)
(make-immutable-hash (list (cons a (t-subst b)) ...))))
(define (f t1 t2) (infer (fv t1) null (list t1) (list t2) #f))
(define-syntax-rule (i2-f t1 t2)
(infer-t t2 t1 #:vars (fv t2) #:fail))
(define N -Number)
(define B -Boolean)
(define fv-tests (define fv-tests
@ -72,12 +102,46 @@
(infer-t (make-ListDots (-v b) 'b) (make-ListDots (-v b) 'b) #:indices '(b)) (infer-t (make-ListDots (-v b) 'b) (make-ListDots (-v b) 'b) #:indices '(b))
(infer-t (make-ListDots (-v b) 'b) (make-ListDots Univ 'b) #:indices '(b)) (infer-t (make-ListDots (-v b) 'b) (make-ListDots Univ 'b) #:indices '(b))
[infer-t (->... null ((-v a) a) (-v b)) (-> -Symbol -String) #:vars '(b) #:indices '(a)]
[infer-t (->... null ((-v a) a) (make-ListDots (-v a) 'a)) (-> -String -Symbol (-lst* -String -Symbol)) #:indices '(a)]
[infer-t (->... (list (-v b)) ((-v a) a) (-v b)) (-> -String -Symbol -String) #:vars '(b) #:indices '(a)]
[infer-l (list (->... null ((-v b) b) (-v a)) (-> (-v a) -Boolean))
(list (-> -String -Symbol) (-> Univ -Boolean) -String)
#:vars '(a)
#:indices '(b)]
[infer-l (list (->... null ((-v a) a) (-v b)) (make-ListDots (-v a) 'a))
(list (-> -Symbol -Symbol -String) (-lst* -Symbol -Symbol))
#:vars '(b)
#:indices '(a)]
;; Currently Broken ;; Currently Broken
;(infer-t (make-ListDots (-v b) 'b) (-lst -Symbol) #:indices '(b)) ;(infer-t (make-ListDots (-v b) 'b) (-lst -Symbol) #:indices '(b))
;(infer-t (-lst -Symbol) (make-ListDots -Symbol 'b) #:indices '(b)) ;(infer-t (-lst -Symbol) (make-ListDots -Symbol 'b) #:indices '(b))
;(infer-t (make-ListDots (-v b) 'b) (make-ListDots -Symbol 'b) #:indices '(b)) ;(infer-t (make-ListDots (-v b) 'b) (make-ListDots -Symbol 'b) #:indices '(b))
;(infer-t (make-ListDots -Symbol 'b) (make-ListDots (-v b) 'b) #:indices '(b)) ;(infer-t (make-ListDots -Symbol 'b) (make-ListDots (-v b) 'b) #:indices '(b))
;(infer-t (make-ListDots -Symbol 'b) (-pair -Symbol (-lst -Symbol)) #:indices '(b)) ;(infer-t (make-ListDots -Symbol 'b) (-pair -Symbol (-lst -Symbol)) #:indices '(b))
[i2-t (-v a) N ('a N)]
[i2-t (-pair (-v a) (-v a)) (-pair N (Un N B)) ('a (Un N B))]
[i2-t (-lst (-v a)) (-pair N (-pair N (-val null))) ('a N)]
[i2-t (-lst (-v a)) (-pair N (-pair B (-val null))) ('a (Un N B))]
[i2-t Univ (Un N B)]
[i2-t ((-v a) . -> . (-v b)) (-> N N) ('b N) ('a (Un))]
[i2-l (list (-v a) (-v a) (-v b))
(list (Un (-val 1) (-val 2)) N N)
'(a b) ('b N) ('a N)]
[i2-l (list (-> (-v a) Univ) (-lst (-v a)))
(list (-> N (Un N B)) (-lst N))
'(a) ('a N)]
[i2-l (list (-> (-v a) (-v b)) (-lst (-v a)))
(list (-> N N) (-lst (Un (-val 1) (-val 2))))
'(a b) ('b N) ('a (Un (-val 1) (-val 2)))]
[i2-l (list (-lst (-v a)))
(list (-lst (Un B N)))
'(a) ('a (Un N B))]
;; error tests
[i2-f (-lst (-v a)) Univ]
)) ))