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

Add new datastructures for dots work.

Browse Source
This commit is contained in:
Sam Tobin-Hochstadt 2008-06-09 17:07:41 -04:00
parent dc47e25c44
commit a7c63840e4
13 changed files with 152 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/typed-scheme/private/check-subforms-unit.ss
View File

@ -38,7 +38,7 @@
(define body-ty #f)
(define (get-result-ty t)
(match t
[(Function: (list (arr: _ rngs _ _ _) ...)) (apply Un rngs)]
[(Function: (list (arr: _ rngs #f _ _ _) ...)) (apply Un rngs)]
[_ (tc-error "Internal error in get-result-ty: not a function type: ~n~a" t)]))
(let loop ([form form])
(parameterize ([current-orig-stx form])

20
collects/typed-scheme/private/free-variance.ss
View File

@ -1,22 +1,25 @@
#lang scheme/base
(require (for-syntax scheme/base)
"tc-utils.ss"
mzlib/etc)
;; this file contains support for calculating the free variables/indexes of types
;; actual computation is done in rep-utils.ss and type-rep.ss
(define-values (Covariant Contravariant Invariant Constant)
(define-values (Covariant Contravariant Invariant Constant Dotted)
(let ()
(define-struct Variance () #:inspector #f)
(define-struct (Covariant Variance) () #:inspector #f)
(define-struct (Contravariant Variance) () #:inspector #f)
(define-struct (Invariant Variance) () #:inspector #f)
(define-struct (Constant Variance) () #:inspector #f)
(values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant))))
;; not really a variance, but is disjoint with the others
(define-struct (Dotted Variance) () #:inspector #f)
(values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant) (make-Dotted))))
(provide Covariant Contravariant Invariant Constant)
(provide Covariant Contravariant Invariant Constant Dotted)
;; hashtables for keeping track of free variables and indexes
(define index-table (make-weak-hasheq))
@ -39,6 +42,8 @@
(define (combine-var v w)
(cond
[(eq? v w) v]
[(or (eq? v Dotted) (eq? w Dotted))
(int-err "Cannot combine Dotted w/ not Dotted: ~a ~a" v w)]
[(eq? v Constant) w]
[(eq? w Constant) v]
[else Invariant]))
@ -54,6 +59,12 @@
freess)
ht)
;; given a set of free variables, remove bound, add bound ...
(define (fix-bound vs bound)
(define vs* (hash-map* (lambda (k v) v) vs))
(hash-remove! vs* bound)
(hash-set! vs* bound (cons bound Dotted)))
;; frees -> frees
(define (flip-variances vs)
(hash-map*
@ -89,7 +100,8 @@
(when (< k n) (hash-remove! new-ht k))))
new-ht)
(provide combine-frees flip-variances without-below unless-in-table var-table index-table empty-hash-table)
(provide combine-frees flip-variances without-below unless-in-table var-table index-table empty-hash-table
fix-bound)
(define-syntax (unless-in-table stx)
(syntax-case stx ()

6
collects/typed-scheme/private/infer-ops.ss
View File

@ -37,7 +37,7 @@
[#:Param in out
(make-Param (var-demote in V)
(vp out))]
[#:arr dom rng rest thn els
[#:arr dom rng rest #f thn els
(if
(apply V-in? V (append thn els))
(make-top-arr)
@ -61,7 +61,7 @@
[#:Param in out
(make-Param (var-promote in V)
(vd out))]
[#:arr dom rng rest thn els
[#:arr dom rng rest #f thn els
(if (apply V-in? V (append thn els))
(make-arr null (Un) Univ null null)
(make-arr (for/list ([d dom]) (var-promote d V))
@ -238,7 +238,7 @@
(for*/list ([t-arr t-arr] [s-arr s-arr])
(with-handlers ([exn:infer? (lambda (_) #f)])
(match* (t-arr s-arr)
[((arr: ts t t-rest t-thn-eff t-els-eff) (arr: ss s s-rest s-thn-eff s-els-eff))
[((arr: ts t t-rest #f t-thn-eff t-els-eff) (arr: ss s s-rest #f s-thn-eff s-els-eff))
(let ([arg-mapping
(cond [(and t-rest s-rest (= (length ts) (length ss)))
(cgen/list X V (cons s-rest ss) (cons t-rest ts))]

6
collects/typed-scheme/private/infer.ss
View File

@ -320,7 +320,7 @@
(cond [(and (null? t-arr) (null? s-arr)) mapping]
[(or (null? t-arr) (null? s-arr)) (unmatch!)]
[else (match (list (car t-arr) (car s-arr))
[(list (arr: ts t t-rest t-thn-eff t-els-eff) (arr: ss s s-rest s-thn-eff s-els-eff))
[(list (arr: ts t t-rest #f t-thn-eff t-els-eff) (arr: ss s s-rest #f s-thn-eff s-els-eff))
(let ([arg-mapping
(cond [(and t-rest s-rest (= (length ts) (length ss)))
(infer/int/list (cons t-rest ts) (cons s-rest ss) mapping (swap flag))]
@ -360,7 +360,7 @@
[els-mapping (infer/int/list/eff (apply append t-els-eff) (apply append s-els-eff) mapping flag)])
(U (U arg-mapping ret-mapping) (U thn-mapping els-mapping))))]
;; here, we try to handle a case-lambda as the argument to a polymorphic function
[(list (Function: ftys) (and t (Function: (list (arr: ss s s-rest s-thn-eff s-els-eff)))))
[(list (Function: ftys) (and t (Function: (list (arr: ss s s-rest #f s-thn-eff s-els-eff)))))
(=> unmatch)
(when (= 1 (length ftys)) (unmatch)) ;; we should have handled this case already
(or
@ -371,7 +371,7 @@
(infer/int (make-Function (list fty)) t mapping flag)))
ftys)
(fail!))]
[(list (and t (Function: (list (arr: ss s s-rest s-thn-eff s-els-eff)))) (Function: ftys))
[(list (and t (Function: (list (arr: ss s s-rest #f s-thn-eff s-els-eff)))) (Function: ftys))
(=> unmatch)
(when (= 1 (length ftys)) (unmatch)) ;; we should have handled this case already
(or

4
collects/typed-scheme/private/rep-utils.ss
View File

@ -144,7 +144,7 @@
(hash-set! var-table v fvs)
(hash-set! index-table v fis))
v)))])])
#'(begin
#`(begin
(define-struct (nm parent) flds #:inspector #f)
(define-match-expander ex
(lambda (s)
@ -152,7 +152,7 @@
(syntax-case s ()
[(__ . fs) (quasisyntax/loc s (struct nm #, (syntax/loc #'fs (_ . fs))))]))))
(begin-for-syntax
(hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs)))
(hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs #'#,stx)))
intern
provides
frees)))])))

4
collects/typed-scheme/private/subtype.ss
View File

@ -99,10 +99,10 @@
(match (list s t)
;; top for functions is above everything
[(list _ (top-arr:)) A0]
[(list (arr: s1 s2 #f thn-eff els-eff) (arr: t1 t2 #f thn-eff els-eff))
[(list (arr: s1 s2 #f #f thn-eff els-eff) (arr: t1 t2 #f #f thn-eff els-eff))
(let ([A1 (subtypes* A0 t1 s1)])
(subtype* A1 s2 t2))]
[(list (arr: s1 s2 s3 thn-eff els-eff) (arr: t1 t2 t3 thn-eff* els-eff*))
[(list (arr: s1 s2 s3 #f thn-eff els-eff) (arr: t1 t2 t3 #f thn-eff* els-eff*))
(unless
(or (and (null? thn-eff*) (null? els-eff*))
(and (effects-equal? thn-eff thn-eff*)

18
collects/typed-scheme/private/tc-app-unit.ss
View File

@ -132,7 +132,7 @@
(define (printable dom rst)
(list dom rst '..))
(match f-ty
[(tc-result: (Function: (list (arr: doms rngs rests thn-effs els-effs) ..1)))
[(tc-result: (Function: (list (arr: doms rngs rests #f thn-effs els-effs) ..1)))
(let loop ([doms* doms] [rngs* rngs] [rests* rests])
(cond [(null? doms*)
(if (and (not (null? doms)) (null? (cdr doms)))
@ -148,14 +148,14 @@
[(and (subtypes arg-tys (car doms*)) (car rests*) (subtype tail-ty (make-Listof (car rests*))))
(ret (car rngs*))]
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*))]))]
[(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests thn-effs els-effs) ..1))))
[(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests #f thn-effs els-effs) ..1))))
(for-each (lambda (x) (unless (not (Poly? x))
(tc-error "Polymorphic argument ~a to polymorphic function in apply not allowed" x)))
arg-tys0)
(let loop ([doms* doms] [rngs* rngs] [rests* rests])
(cond [(null? doms*)
(match f-ty
[(tc-result: (Poly-names: vars (Function: (list (arr: doms rngs rests thn-effs els-effs) ..1))))
[(tc-result: (Poly-names: vars (Function: (list (arr: doms rngs rests #f thn-effs els-effs) ..1))))
(cond
[(null? doms) (int-err "how could doms be null: ~a ~a" doms f-ty)]
[(= 1 (length doms))
@ -223,7 +223,7 @@
[_ (tc-error/expr #:return (ret (Un))
"Wrong number of arguments to parameter - expected 0 or 1, got ~a"
(length argtypes))])]
[(tc-result: (Function: (list (arr: doms rngs rests latent-thn-effs latent-els-effs) ..1)) thn-eff els-eff)
[(tc-result: (Function: (list (arr: doms rngs rests #f latent-thn-effs latent-els-effs) ..1)) thn-eff els-eff)
(if (= 1 (length doms))
(let-values ([(thn-eff els-eff)
(tc-args argtypes arg-thn-effs arg-els-effs (car doms) (car rests)
@ -245,7 +245,7 @@
argtypes)]
[(subtypes/varargs argtypes (car doms*) (car rests*)) (ret (car rngs))]
[else (loop (cdr doms*) (cdr rngs) (cdr rests*))])))]
[(and rft (tc-result: (Poly: vars (Function: (list (arr: doms rngs #f thn-effs els-effs) ...)))))
[(and rft (tc-result: (Poly: vars (Function: (list (arr: doms rngs #f #f thn-effs els-effs) ...)))))
;(printf "Typechecking poly app~nftype: ~a~n" ftype)
;(printf "ftype again: ~a~n" ftype)
;(printf "resolved ftype: ~a : ~a~n" (equal? rft ftype) rft)
@ -256,7 +256,7 @@
argtypes)
(let loop ([doms* doms] [rngs* rngs])
(cond [(null? doms*)
(match-let ([(tc-result: (Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs #f _ _) ...)))) ftype])
(match-let ([(tc-result: (Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs #f #f _ _) ...)))) ftype])
(if (= 1 (length doms))
(tc-error/expr #:return (ret (Un))
"Polymorphic function could not be applied to arguments:~nExpected: ~a ~nActual: ~a"
@ -290,7 +290,7 @@
)]|#
[else (loop (cdr doms*) (cdr rngs*))]))]
;; polymorphic varargs
[(tc-result: (Poly: vars (Function: (list (arr: dom rng rest thn-eff els-eff)))))
[(tc-result: (Poly: vars (Function: (list (arr: dom rng rest #f thn-eff els-eff)))))
(for-each (lambda (x) (unless (not (Poly? x))
(tc-error "Polymorphic argument ~a to polymorphic function not allowed" x)))
argtypes)
@ -310,7 +310,7 @@
[else (tc-error/expr #:return (ret (Un))
"no polymorphic function domain matched - domain was: ~a rest type was: ~a arguments were ~a"
(stringify dom) rest (stringify argtypes))]))]
[(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests thn-effs els-effs) ...))))
[(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests #f thn-effs els-effs) ...))))
(tc-error/expr #:return (ret (Un)) "polymorphic vararg case-lambda application not yet supported")]
;; Union of function types works if we can apply all of them
[(tc-result: (Union: (list (and fs (Function: _)) ...)) e1 e2)
@ -413,7 +413,7 @@
(match-let* ([(tc-result: prod-t) (tc-expr #'prod)]
[(tc-result: con-t) (tc-expr #'con)])
(match (list prod-t con-t)
[(list (Function: (list (arr: (list) vals #f _ _))) (Function: (list (arr: dom rng #f _ _))))
[(list (Function: (list (arr: (list) vals #f #f _ _))) (Function: (list (arr: dom rng #f #f _ _))))
(=> unmatch)
(match (list vals dom)
[(list (Values: v) (list t ...))

4
collects/typed-scheme/private/tc-lambda-unit.ss
View File

@ -132,10 +132,10 @@
(let loop ([expected expected])
(match expected
[(Mu: _ _) (loop (unfold expected))]
[(Function: (list (arr: args ret rest _ _)))
[(Function: (list (arr: args ret rest #f _ _)))
(tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest)
expected]
[(Function: (list (arr: argss rets rests _ _) ...))
[(Function: (list (arr: argss rets rests #f _ _) ...))
(for ([args argss] [ret rets] [rest rests])
(tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest))
expected]

8
collects/typed-scheme/private/type-contract.ss
View File

@ -80,13 +80,13 @@
(define (f a)
(define-values (dom* rngs* rst)
(match a
[(arr: dom (Values: rngs) #f _ _)
[(arr: dom (Values: rngs) #f #f _ _)
(values (map t->c dom) (map t->c rngs) #f)]
[(arr: dom rng #f _ _)
[(arr: dom rng #f #f _ _)
(values (map t->c dom) (list (t->c rng)) #f)]
[(arr: dom (Values: rngs) rst _ _)
[(arr: dom (Values: rngs) rst #f _ _)
(values (map t->c dom) (map t->c rngs) (t->c rst))]
[(arr: dom rng rst _ _)
[(arr: dom rng rst #f _ _)
(values (map t->c dom) (list (t->c rng)) (t->c rst))]))
(with-syntax
([(dom* ...) dom*]

4
collects/typed-scheme/private/type-effect-convenience.ss
View File

@ -68,8 +68,8 @@
(define make-arr*
(case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))]
[(dom rng rest) (make-arr dom rng rest (list) (list))]
[(dom rng rest eff1 eff2) (make-arr dom rng rest eff1 eff2)]))
[(dom rng rest) (make-arr dom rng rest #f (list) (list))]
[(dom rng rest eff1 eff2) (make-arr dom rng rest #f eff1 eff2)]))
(define (make-promise-ty t)
(make-Struct (string->uninterned-symbol "Promise") #f (list t) #f #f #'promise? values))

8
collects/typed-scheme/private/type-effect-printer.ss
View File

@ -46,11 +46,13 @@
(match a
[(top-arr:)
(fp "Procedure")]
[(arr: dom rng rest thn-eff els-eff)
[(arr: dom rng rest drest thn-eff els-eff)
(fp "(")
(for-each (lambda (t) (fp "~a " t)) dom)
(when rest
(fp "~a .. " rest))
(fp "~a* " rest))
(when drest
(fp "~a ..." drest))
(fp "-> ~a" rng)
(unless (and (null? thn-eff) (null? els-eff))
(fp " : ~a ~a" thn-eff els-eff))
@ -96,7 +98,7 @@
[(list) (fp "(case-lambda)")]
[(list a) (print-arr a)]
[(list a ...) (fp "(case-lambda ") (for-each print-arr a) (fp ")")]))]
[(arr: _ _ _ _ _) (print-arr c)]
[(arr: _ _ _ _ _ _) (print-arr c)]
[(Vector: e) (fp "(Vectorof ~a)" e)]
[(Box: e) (fp "(Box ~a)" e)]
[(Union: elems) (fp "~a" (cons 'U elems))]

121
collects/typed-scheme/private/type-rep.ss
View File

@ -21,7 +21,7 @@
;; n is a Name
(dt F (n) [#:frees (make-immutable-hasheq (list (cons n Covariant))) empty-hash-table] [#:fold-rhs #:base])
;; id is an Identifier
(dt Name (id) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
@ -54,10 +54,19 @@
;; n is how many variables are bound here
;; body is a Scope
(dt Poly (n body) #:no-provide [#:frees (free-vars* body) (without-below n (free-idxs* body))]
(dt Poly (n body) #:no-provide
[#:frees (free-vars* body) (without-below n (free-idxs* body))]
[#:fold-rhs (let ([body* (remove-scopes n body)])
(*Poly n (add-scopes n (type-rec-id body*))))])
;; n is how many variables are bound here
;; there are n-1 'normal' vars and 1 ... var
;; body is a Scope
(dt PolyDots (n body) #:no-provide
[#:frees (free-vars* body) (without-below n (free-idxs* body))]
[#:fold-rhs (let ([body* (remove-scopes n body)])
(*PolyDots n (add-scopes n (type-rec-id body*))))])
;; pred : identifier
;; cert : syntax certifier
(dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base])
@ -83,24 +92,37 @@
;; dom : Listof[Type]
;; rng : Type
;; rest : Type
;; rest : Option[Type]
;; drest : Option[Cons[Type,Name or nat]]
;; rest and drest NOT both true
;; thn-eff : Effect
;; els-eff : Effect
;; arr is NOT a Type
(dt arr (dom rng rest thn-eff els-eff)
[#:frees (combine-frees (append (map flip-variances (map free-vars* dom))
(map free-vars* (append (list rng)
(if rest (list rest) null)
thn-eff
els-eff))))
(combine-frees (append (map flip-variances (map free-idxs* dom))
(map free-idxs* (append (list rng)
(if rest (list rest) null)
thn-eff
els-eff))))]
(dt arr (dom rng rest drest thn-eff els-eff)
[#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null) dom)))
(match drest
[(cons t (? symbol? bnd))
(let ([vs (free-vars* t)])
(flip-variances (fix-bound vs bnd)))]
[(cons t bnd) (flip-variances (free-vars* t))]
[_ null])
(list (free-vars* rng))
(map make-invariant
(map free-vars* (append thn-eff els-eff)))))
(combine-frees (append (map flip-variances (map free-idxs* (append (if rest (list rest) null) dom)))
(match drest
[(cons t (? number? bnd))
(let ([vs (free-idxs* t)])
(flip-variances (fix-bound vs bnd)))]
[(cons t bnd) (flip-variances (free-idxs* t))]
[_ null])
(list (free-idxs* rng))
(map make-invariant
(map free-idxs* (append thn-eff els-eff)))))]
[#:fold-rhs (*arr (map type-rec-id dom)
(type-rec-id rng)
(and rest (type-rec-id rest))
(and drest (cons (type-rec-id (car drest)) (cdr drest)))
(map effect-rec-id thn-eff)
(map effect-rec-id els-eff))])
@ -203,19 +225,22 @@
[(kw #:matcher mtch pats ... expr)
(hash-set! ht (syntax-e #'kw) (list #'mtch
(syntax/loc cl (pats ...))
(lambda (tr er) #'expr)))]
(lambda (tr er) #'expr)
cl))]
[(kw pats ... expr)
(hash-set! ht (syntax-e #'kw) (list (mk-matcher (syntax-e #'kw))
(syntax/loc cl (pats ...))
(lambda (tr er) #'expr)))]))
(lambda (tr er) #'expr)
cl))]))
(define rid #'type-rec-id)
(define erid #'effect-rec-id)
(define (gen-clause k v)
(define match-ex (car v))
(define pats (cadr v))
(define body-f (caddr v))
(define pat (quasisyntax/loc pats (#,match-ex . #,pats)))
(define cl (quasisyntax/loc match-ex (#,pat #,(body-f rid erid))))
(define src (cadddr v))
(define pat (quasisyntax/loc src (#,match-ex . #,pats)))
(define cl (quasisyntax/loc src (#,pat #,(body-f rid erid))))
cl)
(syntax-case stx ()
[(tc rec-id ty [kw pats ... es] ...)
@ -266,6 +291,9 @@
;; necessary to avoid infinite loops
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
[#:PolyDots n body*
(let ([body (remove-scopes n body*)])
(*PolyDots n (*Scope (loop (+ n outer) body))))]
[#:Poly n body*
(let ([body (remove-scopes n body*)])
(*Poly n (*Scope (loop (+ n outer) body))))])))
@ -291,6 +319,9 @@
;; necessary to avoid infinite loops
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
[#:PolyDots n body*
(let ([body (remove-scopes n body*)])
(*PolyDots n (*Scope (loop (+ n outer) body))))]
[#:Poly n body*
(let ([body (remove-scopes n body*)])
(*Poly n (*Scope (loop (+ n outer) body))))])))
@ -337,6 +368,21 @@
(error "Wrong number of names"))
(instantiate-many (map *F names) scope)]))
;; the 'smart' constructor
(define (PolyDots* names body)
(if (null? names) body
(let ([v (*PolyDots (length names) (abstract-many names body))])
(hash-set! name-table v names)
v)))
;; the 'smart' destructor
(define (PolyDots-body* names t)
(match t
[(PolyDots: n scope)
(unless (= (length names) n)
(error "Wrong number of names"))
(instantiate-many (map *F names) scope)]))
(print-struct #t)
(define-match-expander Mu-unsafe:
@ -349,6 +395,11 @@
(syntax-case stx ()
[(_ n bp) #'(? Poly? (app (lambda (t) (list (Poly-n t) (Poly-body t))) (list n bp)))])))
(define-match-expander PolyDots-unsafe:
(lambda (stx)
(syntax-case stx ()
[(_ n bp) #'(? PolyDots? (app (lambda (t) (list (PolyDots-n t) (PolyDots-body t))) (list n bp)))])))
(define-match-expander Mu:*
(lambda (stx)
(syntax-case stx ()
@ -392,6 +443,31 @@
(list syms (Poly-body* syms t))))
(list nps bp)))])))
;; This match expander wraps the smart constructor
;; names are generated with gensym
(define-match-expander PolyDots:*
(lambda (stx)
(syntax-case stx ()
[(_ nps bp)
#'(? PolyDots?
(app (lambda (t)
(let* ([n (PolyDots-n t)]
[syms (build-list n (lambda _ (gensym)))])
(list syms (PolyDots-body* syms t))))
(list nps bp)))])))
;; This match expander uses the names from the hashtable
(define-match-expander PolyDots-names:
(lambda (stx)
(syntax-case stx ()
[(_ nps bp)
#'(? PolyDots?
(app (lambda (t)
(let* ([n (PolyDots-n t)]
[syms (hash-ref name-table t)])
(list syms (PolyDots-body* syms t))))
(list nps bp)))])))
;; unfold : Type -> Type
;; must be applied to a Mu
(define (unfold t)
@ -417,21 +493,26 @@
(provide
unfold
Mu-name: Poly-names:
PolyDots-names:
Type-seq Effect-seq
Mu-unsafe: Poly-unsafe:
Mu? Poly?
PolyDots-unsafe:
Mu? Poly? PolyDots?
arr
Type? Effect?
Poly-n
PolyDots-n
free-vars*
type-equal? type-compare type<?
remove-dups
(rename-out [Mu:* Mu:]
[Poly:* Poly:]
[PolyDots:* PolyDots:]
[Mu* make-Mu]
[Poly* make-Poly]
[Mu-body* Mu-body]
[Poly-body* Poly-body]))
[Poly-body* Poly-body]
[PolyDots-body* PolyDots-body]))
;(trace unfold)

4
collects/typed-scheme/private/unify.ss
View File

@ -42,8 +42,8 @@
(unify/acc (map (lambda (p) (map (lambda (e) (subst v t e)) p)) rest)
(cons (list v t) acc))]
;; arrow types - just add a whole bunch of new constraints
[(list (list (Function: (list (arr: ts t t-rest t-thn-eff t-els-eff) ...))
(Function: (list (arr: ss s s-rest s-thn-eff s-els-eff) ...)))
[(list (list (Function: (list (arr: ts t t-rest #f t-thn-eff t-els-eff) ...))
(Function: (list (arr: ss s s-rest #f s-thn-eff s-els-eff) ...)))
rest ...)
#;(printf "arrow unification~n")
(let ()