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

Handle polymorphic function application.

Browse Source 
Paths work with car/cdr.
Fix #%require/#%provide top-level handling.

svn: r14735
This commit is contained in:
Sam Tobin-Hochstadt 2009-05-06 22:45:12 +00:00
parent 07341c605b
commit 50696a08a3
10 changed files with 136 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/typed-scheme/infer/infer-unit.ss
View File

@ -454,11 +454,11 @@
(let ([cs (cgen/list null X S T)])
(if (not expected)
(subst-gen cs R must-vars)
(cset-meet cs (cgen null X R expected))))))
(subst-gen (cset-meet cs (cgen null X R expected)) R must-vars)))))
;; like infer, but T-var is the vararg type:
(define (infer/vararg X S T T-var R must-vars [expected #f])
(define new-T (extend S T T-var))
(define new-T (if T-var (extend S T T-var) T))
(and ((length S) . >= . (length T))
(infer X S new-T R must-vars expected)))

3
collects/typed-scheme/infer/signatures.ss
View File

@ -33,7 +33,8 @@
[cnt infer/vararg (((listof symbol?)
(listof Type?)
(listof Type?)
Type? Type?
(or/c #f Type?)
Type?
(listof symbol?))
((or/c #f Type?)) . ->* . any)]
[cnt infer/dots (((listof symbol?)

27
collects/typed-scheme/private/base-env.ss
View File

@ -14,7 +14,23 @@
[raise (Univ . -> . (Un))]
[car (-poly (a b) (cl-> [((-pair a b)) a] [((-lst a)) a]))]
[car (-poly (a b)
(cl->*
(->acc (list (-pair a b)) a (list -car))
(->* (list (-lst a)) a)))]
[cdr (-poly (a b)
(cl->*
(->acc (list (-pair a b)) b (list -cdr))
(->* (list (-lst a)) (-lst a))))]
[cadr (-poly (a b c)
(cl-> [((-pair a (-pair b c))) b]
[((-lst a)) a]))]
[caddr (-poly (a) (-> (-lst a) a))]
[cadddr (-poly (a) (-> (-lst a) a))]
[cddr (-poly (a) (-> (-lst a) (-lst a)))]
[cdddr (-poly (a) (-> (-lst a) (-lst a)))]
[first (-poly (a b) (cl-> [((-pair a b)) a] [((-lst a)) a]))]
[second (-poly (a b c)
(cl-> [((-pair a (-pair b c))) b]
@ -26,14 +42,7 @@
[fifth (-poly (a) ((-lst a) . -> . a))]
[sixth (-poly (a) ((-lst a) . -> . a))]
[rest (-poly (a) ((-lst a) . -> . (-lst a)))]
[cadr (-poly (a b c)
(cl-> [((-pair a (-pair b c))) b]
[((-lst a)) a]))]
[caddr (-poly (a) (-> (-lst a) a))]
[cadddr (-poly (a) (-> (-lst a) a))]
[cdr (-poly (a b) (cl-> [((-pair a b)) b] [((-lst a)) (-lst a)]))]
[cddr (-poly (a) (-> (-lst a) (-lst a)))]
[cdddr (-poly (a) (-> (-lst a) (-lst a)))]
[cons (-poly (a b)
(cl-> [(a (-lst a)) (-lst a)]
[(a b) (-pair a b)]))]

21
collects/typed-scheme/test2.ss
View File

@ -19,11 +19,12 @@
(+)
(+ 1 2 3)
(+ 1 2 3.5)
#|
(define-struct: (Z) x ([y : Z]))
(define: my-x : (x Number) (make-x 1))
(number? (x-y my-x))
(if (number? (x-y my-x)) (+ 1 (x-y my-x)) 7)
(define-struct: (Z) X ([y : Z]))
(define: my-x : (X Number) (make-X 1))
#| ; FIXME - doesn't work yet
(number? (X-y my-x))
(if (number? (X-y my-x)) (+ 1 (X-y my-x)) 7)
|#
(define: (f2) : (U) (error 'foo))
@ -32,5 +33,15 @@
(: f3 (U (Number -> Number) (Number -> String)))
(define (f3 x) 7)
(define: x : (List Any Any) (list 1 23 ))
(car x)
(if (number? (car x)) (add1 (car #{x :: (Pair Number Any)})) 7)
(if (number? (car x)) (add1 (car x)) 7)
;; error
;(f 12 "hi")
(map + (list 1 2 3))
(map + (list 1 2 3) (list 1 2 3))
;; error
;(map + (list 1 2 3) (list 1 2 "foo"))

26
collects/typed-scheme/typecheck/tc-app-helper.ss
View File

@ -1,7 +1,7 @@
#lang scheme/base
(require "../utils/utils.ss"
(utils tc-utils))
(require "../utils/utils.ss" scheme/match
(utils tc-utils) (rep type-rep) (types utils union))
(provide (all-defined-out))
@ -39,3 +39,25 @@
(if expected
(format "Expected result: ~a~n" expected)
""))]))
(define (poly-fail t argtypes #:name [name #f] #:expected [expected #f])
(match t
[(or (Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests '()) ...)))
(PolyDots-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests '()) ...))))
(let ([fcn-string (if name
(format "function ~a" (syntax->datum name))
"function")])
(if (and (andmap null? msg-doms)
(null? argtypes))
(tc-error/expr #:return (ret (Un))
(string-append
"Could not infer types for applying polymorphic "
fcn-string
"\n"))
(tc-error/expr #:return (ret (Un))
(string-append
"Polymorphic " fcn-string " could not be applied to arguments:~n"
(domain-mismatches t msg-doms msg-rests msg-drests msg-rngs argtypes #f #f #:expected expected)
(if (not (for/and ([t (apply append (map fv/list msg-doms))]) (memq t msg-vars)))
(string-append "Type Variables: " (stringify msg-vars) "\n")
"")))))]))

48
collects/typed-scheme/typecheck/tc-app.ss
View File

@ -4,10 +4,11 @@
"signatures.ss" "tc-metafunctions.ss"
"tc-app-helper.ss"
stxclass scheme/match mzlib/trace
(for-syntax stxclass)
(for-syntax stxclass scheme/base)
(types utils abbrev union subtype resolve)
(utils tc-utils)
(rep type-rep filter-rep object-rep)
(r:infer infer)
(for-template
(only-in '#%kernel [apply k:apply])
"internal-forms.ss" scheme/base
@ -89,6 +90,19 @@
(define (in-indexes dom)
(in-range (length dom)))
(define-syntax (handle-clauses stx)
(syntax-parse stx
[(_ (lsts ... arrs) f-stx args-stx pred infer t argtys expected)
(with-syntax ([(vars ... a) (generate-temporaries #'(lsts ... arrs))])
(syntax/loc stx
(or (for/or ([vars lsts] ... [a arrs]
#:when (pred vars ... a))
(let ([substitution (infer vars ... a)])
(and substitution
(tc/funapp1 f-stx args-stx (subst-all substitution a) argtys expected #:check #f))))
(poly-fail t argtys #:name (and (identifier? f-stx) f-stx) #:expected expected))))]))
(define (tc/funapp f-stx args-stx ftype0 argtys expected)
(match* (ftype0 argtys)
;; we special-case this (no case-lambda) for improved error messages
@ -109,6 +123,34 @@
#:return (or expected (ret (Un)))
(string-append "No function domains matched in function application:\n"
(domain-mismatches t doms rests drests rngs argtys-t #f #f))))]
;; polymorphic functions without dotted rest
[((tc-result1: (and t
(or (Poly: vars
(Function: (list (and arrs (arr: doms rngs rests (and drests #f) '())) ...)))
(PolyDots: vars
(Function: (list (and arrs (arr: doms rngs rests (and drests #f) '())) ...))))))
(list (tc-result1: argtys-t) ...))
(handle-clauses (doms rngs rests arrs) f-stx args-stx
;; only try inference if the argument lengths are appropriate
(lambda (dom _ rest a) ((if rest <= =) (length dom) (length argtys)))
;; only try to infer the free vars of the rng (which includes the vars in filters/objects)
;; note that we have to use argtys-t here, since argtys is a list of tc-results
(lambda (dom rng rest a) (infer/vararg vars argtys-t dom rest rng (fv rng) (and expected (tc-results->values expected))))
t argtys expected)]
;; polymorphic ... type
[((tc-result1: (and t (PolyDots:
(and vars (list fixed-vars ... dotted-var))
(Function: (list (and arrs (arr: doms rngs (and #f rests) (cons dtys dbounds) '())) ...)))))
(list (tc-result1: argtys-t) ...))
(handle-clauses (doms dtys dbounds rngs arrs) f-stx args-stx
(lambda (dom dty dbound rng arr) (and (<= (length dom) (length argtys))
(eq? dotted-var dbound)))
(lambda (dom dty dbound rng arr)
(infer/dots fixed-vars dotted-var argtys-t dom dty rng (fv rng) #:expected (and expected (tc-results->values expected))))
t argtys expected)]
;; procedural structs
[(tc-result1: (and sty (Struct: _ _ _ (? Type? proc-ty) _ _ _)))
(tc/funapp f-stx (cons (syntax/loc f-stx dummy) args-stx) (ret proc-ty) (cons sty argtys) expected)]
;; parameters are functions too
[((tc-result1: (Param: in out)) (list)) (ret out)]
[((tc-result1: (Param: in out)) (list (tc-result1: t)))
@ -167,5 +209,7 @@
[_ (make-Empty)])]
[_ (make-Empty)]))])
(ret t-r f-r o-r))]
[(_ _)
[((arr: _ _ _ drest '()) _)
(int-err "funapp with drest args NYI")]
[((arr: _ _ _ _ kws) _)
(int-err "funapp with keyword args NYI")]))

6
collects/typed-scheme/typecheck/tc-metafunctions.ss
View File

@ -11,7 +11,7 @@
(for-syntax scheme/base))
(provide combine-filter apply-filter abstract-filter abstract-filters
split-lfilters merge-filter-sets values->tc-results)
split-lfilters merge-filter-sets values->tc-results tc-results->values)
;; this implements the sequence invariant described on the first page relating to Bot
(define (lcombine l1 l2)
@ -173,3 +173,7 @@
[(LEmpty:) #f]
[(LPath: p (== i)) (make-Path p x)]))
(make-Empty))))]))
(define (tc-results->values tc)
(match tc
[(tc-results: ts) (-values ts)]))

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

@ -119,11 +119,11 @@
;; typecheck the body, and produce syntax-time code that registers types
[let ([type (tc-toplevel-form body2)])])
(define-syntax-class invis-kw
#:literals (define-values define-syntaxes require provide begin)
#:literals (define-values define-syntaxes #%require #%provide begin)
(pattern define-values)
(pattern define-syntaxes)
(pattern require)
(pattern provide)
(pattern #%require)
(pattern #%provide)
(pattern begin))
(syntax-parse body2
[(head:invis-kw . _)

15
collects/typed-scheme/types/abbrev.ss
View File

@ -125,6 +125,9 @@
(define -no-lobj (make-LEmpty))
(define -no-obj (make-Empty))
(define -car (make-CarPE))
(define -cdr (make-CdrPE))
;; convenient syntax
(define-syntax -v
@ -177,8 +180,12 @@
(make-Function (list (make-arr* dom rng #:rest rst)))]
[(_ dom rng : filters)
(make-Function (list (make-arr* dom rng #:filters filters)))]
[(_ dom rng : filters : object)
(make-Function (list (make-arr* dom rng #:filters filters #:object object)))]
[(_ dom rst rng : filters)
(make-Function (list (make-arr* dom rng #:rest rst #:filters filters)))]))
(make-Function (list (make-arr* dom rng #:rest rst #:filters filters)))]
[(_ dom rst rng : filters : object)
(make-Function (list (make-arr* dom rng #:rest rst #:filters filters #:object object)))]))
(define-syntax (-> stx)
(syntax-parse stx
@ -201,6 +208,12 @@
[(_ dom (dty dbound) rng : filters)
(make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound) #:filters filters)))]))
(define (->acc dom rng path)
(make-Function (list (make-arr* dom rng
#:filters (-LFS (list (-not-filter (-val #f) path))
(list (-filter (-val #f) path)))
#:object (make-LPath path 0)))))
(define (cl->* . args)
(define (funty-arities f)
(match f

6
collects/typed-scheme/types/utils.ss
View File

@ -187,7 +187,11 @@
[(_ tp fp op) #'(struct tc-results ((list (struct tc-result (tp fp op))) #f))]
[(_ tp) #'(struct tc-results ((list (struct tc-result (tp _ _))) #f))]))
(provide tc-result: tc-results: tc-result1: tc-result? tc-results?)
(define (tc-results-t tc)
(match tc
[(tc-results: t) t]))
(provide tc-result: tc-results: tc-result1: tc-result? tc-results? tc-results-t)
;; convenience function for returning the result of typechecking an expression
(define ret