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

Merge in changes from 660.

Browse Source 
svn: r9567
This commit is contained in:
Sam Tobin-Hochstadt 2008-05-01 17:35:50 +00:00
parent 7d6bf0371e
commit 5af7d626be
12 changed files with 134 additions and 71 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -52,7 +52,7 @@
[make-lst/elements -pair])
(make-env
[string->sexpr (-> -String (-mu x (Un Sym -String N B (-lst x))))]
[raise (Univ . -> . (Un))]
(car (make-Poly (list 'a 'b) (cl-> [((-pair (-v a) (-v b))) (-v a)]
[((make-lst (-v a))) (-v a)])))
@ -95,8 +95,12 @@
(number? (make-pred-ty N))
(integer? (make-pred-ty -Integer))
(boolean? (make-pred-ty B))
(add1 (-> N N))
(sub1 (-> N N))
(add1 (cl->*
#;(-> -Integer -Integer)
(-> N N)))
(sub1 (cl->*
#;(-> -Integer -Integer)
(-> N N)))
(eq? (-> Univ Univ B))
(eqv? (-> Univ Univ B))
(equal? (-> Univ Univ B))
@ -179,10 +183,10 @@
(<= (->* (list N N) N B))
[> (->* (list N) N B)]
(zero? (N . -> . B))
(* (->* '() N N))
(/ (->* (list N) N N))
(+ (->* '() N N))
(- (->* (list N) N N))
(* (cl->* (->* '() -Integer -Integer) (->* '() N N)))
(/ (cl->* (->* (list N) N N)))
(+ (cl->* (->* '() -Integer -Integer) (->* '() N N)))
(- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N)))
(max (->* (list N) N N))
(min (->* (list N) N N))
[values (make-Poly '(a) (-> (-v a) (-v a)))]
@ -463,8 +467,8 @@
[make-directory (-> -Path -Void)]
[hash-table-for-each (-poly (a b c)
(-> (-HT a b) (-> a b c) -Void))]
[hash-for-each (-poly (a b c)
(-> (-HT a b) (-> a b c) -Void))]
[delete-file (-> -Pathlike -Void)]
[make-namespace (cl->* (-> -Namespace)

2
collects/typed-scheme/private/base-types.ss
View File

@ -95,7 +95,7 @@
[HashTable (-poly (a b) (-HT a b))]
[Promise (-poly (a) (-Promise a))]
[Pair (-poly (a b) (-pair a b))]
[Box (-poly (a) (make-Box a))]
[Boxof (-poly (a) (make-Box a))]
[Syntax Any-Syntax]
[Identifier Ident]
)

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

@ -139,6 +139,11 @@
(unless (= (length l1) (length l2))
(unmatch))
(cgen-union V X l1 l2)]
#;
[((Poly-unsafe: n b) (Poly-unsafe: n* b*))
(unless (= n n*)
(fail! S T))
(cgen V X b b*)]
[((Union: es) S) (cset-meet* X (for/list ([e es]) (cgen V X e S)))]

5
collects/typed-scheme/private/parse-type.ss
View File

@ -114,7 +114,10 @@
[tvar (make-F var)])
(add-type-name-reference #'mu)
(parameterize ([current-tvars (extend-env (list var) (list tvar) (current-tvars))])
(make-Mu var (parse-type #'t))))]
(let ([t (parse-type #'t)])
(if (memq var (fv t))
(make-Mu var t)
t))))]
[(U ts ...)
(eq? (syntax-e #'U) 'U)
(begin

21
collects/typed-scheme/private/syntax-traversal.ss
View File

@ -41,15 +41,18 @@
(define (look-for-in-orig orig expanded lookfor)
(define src (syntax-source orig))
;; we just might get a lookfor that is already in the original
(if (syntax-original? lookfor)
lookfor
(let ([enclosing (enclosing-syntaxes-with-source expanded lookfor src)]
[syntax-locs (make-hash)])
;; find all syntax locations in original code
(let loop ([stx orig])
(when (syntax? stx) (hash-set! syntax-locs (syntax-loc stx) stx))
(let ([stx (if (syntax? stx) (syntax-e stx) stx)])
(when (pair? stx) (loop (car stx)) (loop (cdr stx)))))
(let ([enclosing (enclosing-syntaxes-with-source expanded lookfor src)]
[syntax-locs (make-hash)])
;; find all syntax locations in original code
(let loop ([stx orig])
(when (syntax? stx) (hash-set! syntax-locs (syntax-loc stx) stx))
(let ([stx (if (syntax? stx) (syntax-e stx) stx)])
(when (pair? stx) (loop (car stx)) (loop (cdr stx)))))
(or
;; we just might get a lookfor that is already in the original
(and (eq? src (syntax-source lookfor))
(hash-ref syntax-locs (syntax-loc lookfor) #f))
;; look for some enclosing expression
(and enclosing
(ormap (lambda (enc) (hash-ref syntax-locs (syntax-loc enc) #f))

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

@ -248,7 +248,7 @@
"Polymorphic function could not be applied to arguments:~nExpected: ~a ~nActual: ~a"
(car msg-doms) argtypes)
(tc-error/expr #:return (ret (Un))
"no polymorphic function domain matched - possible domains were: ~n~a~narguments: were ~n~a"
"no polymorphic function domain matched - possible domains were: ~n~a~narguments were: ~n~a"
(stringify (map stringify msg-doms) "\n") (stringify argtypes))))]
[(and (= (length (car doms*))
(length argtypes))
@ -322,20 +322,25 @@
(kernel-syntax-case* b #f (reverse)
[[(v) (#%plain-app reverse n)]
(free-identifier=? name #'n)
(type-annotation #'v)]
(begin ;(printf "found annotation: ~a ~a~n~a~n" (syntax-e name) (syntax-e #'v) (type-annotation #'v))
(type-annotation #'v))]
[_ #f]))
(kernel-syntax-case*
stx #f (reverse)
[(let-values (binding ...) body)
(cond [(ormap match? (syntax->list #'(binding ...)))]
[else (find #'body)])]
[(#%plain-app e ...) (ormap find (syntax->list #'(e ...)))]
[(if e1 e2 e3) (ormap find (syntax->list #'(e1 e2 e3)))]
[(letrec-values ([(v ...) e] ...) b)
(ormap find (syntax->list #'(e ... b)))]
[(#%plain-lambda (v ...) e)
(find #'e)]
[_ #f]))
stx #f (reverse letrec-syntaxes+values)
[(let-values (binding ...) body)
(cond [(ormap match? (syntax->list #'(binding ...)))]
[else (find #'body)])]
[(#%plain-app e ...) (ormap find (syntax->list #'(e ...)))]
[(if e1 e2 e3) (ormap find (syntax->list #'(e1 e2 e3)))]
[(letrec-values ([(v ...) e] ...) b)
(ormap find (syntax->list #'(e ... b)))]
[(letrec-syntaxes+values _ ([(v ...) e] ...) b)
(ormap find (syntax->list #'(e ... b)))]
[(begin . es)
(ormap find (syntax->list #'es))]
[(#%plain-lambda (v ...) e)
(find #'e)]
[_ #f]))
(define (matches? stx)
(let loop ([stx stx] [ress null] [acc*s null])
@ -449,7 +454,7 @@
;(printf "got here 1~n")
(not (andmap type-annotation (syntax->list #'(val acc ...))))
(free-identifier=? #'val #'val*)
(andmap (lambda (a) (find-annotation #'(if (#%plain-app null? val*) thn els) a))
(ormap (lambda (a) (find-annotation #'(if (#%plain-app null? val*) thn els) a))
(syntax->list #'(acc ...)))
;(printf "got here 2~n")
#;
@ -462,11 +467,12 @@
[_ #f]))
(let* ([ts1 (tc-expr/t #'actual)]
[ts1 (generalize ts1)]
[ann-ts (map (lambda (a) (find-annotation #'(if (#%plain-app null? val*) thn els) a))
(syntax->list #'(acc ...)))]
[ts (cons ts1 ann-ts)])
;(printf "doing match case actuals:~a ann-ts: ~a~n"
; (syntax->datum #'(actuals ...)) ann-ts)
[ann-ts (map (lambda (a ac) (or (find-annotation #'(if (#%plain-app null? val*) thn els) a)
(generalize (tc-expr/t ac))))
(syntax->list #'(acc ...))
(syntax->list #'(actuals ...)))]
[ts (cons ts1 ann-ts)])
;(printf "doing match case actuals:~a ann-ts: ~a~n" (syntax->datum #'(actuals ...)) ann-ts)
;; check that the actual arguments are ok here
(map tc-expr/check (syntax->list #'(actuals ...)) ann-ts)
;(printf "done here ts = ~a~n" ts)
@ -487,7 +493,7 @@
;(printf "special case 1~n")
(not (andmap type-annotation (syntax->list #'(args ...))))
(free-identifier=? #'lp #'lp*))
(let ([ts (map tc-expr/t (syntax->list #'actuals))])
(let ([ts (map (compose generalize tc-expr/t) (syntax->list #'actuals))])
;(printf "special case~n")
(tc/rec-lambda/check form #'(args ...) #'body #'lp ts expected)
(ret expected))]

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

@ -77,9 +77,13 @@
[else (make-arr arg-types t)])]
[t (int-err "bad match - not a tc-result: ~a" t)]))))]
[(args* ... . rest)
(let ([t (tc/lambda-clause args body)])
(check-below (make-Function (list t)) (make-Function (list (make-arr arg-tys ret-ty rest-ty))))
t)]))
(begin
(unless rest-ty
(tc-error "Expected function with ~a arguments and no rest argument,~nbut got function with ~a arguments and a rest argument"
(length arg-tys) (length (syntax->list #'(args* ...)))))
(with-lexical-env/extend
(list #'rest) (list (-lst rest-ty))
(tc/lambda-clause/check #'(args* ...) body arg-tys ret-ty #f)))]))
;; syntax-list[id] block -> arr
(define (tc/lambda-clause args body)
@ -129,7 +133,8 @@
(match expected
[(Mu: _ _) (loop (unfold expected))]
[(Function: (list (arr: args ret rest _ _)))
(tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest)]
(tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest)
expected]
[t (let ([t (tc/mono-lambda formals bodies #f)])
(check-below t expected))]))
(let loop ([formals (syntax->list formals)]
@ -168,16 +173,15 @@
(define (tc/plambda form formals bodies expected)
(match expected
[(Poly-names: ns (and expected* (Function: _)))
(with-syntax ()
(let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)])
(or (and p (map syntax-e (syntax->list p)))
ns))]
[literal-tvars tvars]
[new-tvars (map make-F literal-tvars)]
[ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))])
(tc/mono-lambda formals bodies expected*))])
;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty)
(ret (make-Poly literal-tvars ty))))]
(let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)])
(or (and p (map syntax-e (syntax->list p)))
ns))]
[literal-tvars tvars]
[new-tvars (map make-F literal-tvars)]
[ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))])
(tc/mono-lambda formals bodies expected*))])
;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty)
(ret (make-Poly literal-tvars ty)))]
[_ (tc-error/expr #:return expected "Expected a value of type ~a, but got a polymorphic function." expected)]))

42
collects/typed-scheme/private/tc-let-unit.ss
View File

@ -8,8 +8,10 @@
"type-env.ss"
"parse-type.ss"
"utils.ss"
"type-utils.ss"
syntax/free-vars
mzlib/trace
scheme/match
syntax/kerncase
(for-template
scheme/base
@ -30,7 +32,7 @@
namess
;; the types
types
(for-each (lambda (stx e t) (check-type stx (expr->type e) t))
(for-each expr->type
clauses
exprs
(map list->values-ty types))
@ -65,10 +67,24 @@
(define (tc/letrec-values namess exprs body form)
(tc/letrec-values/internal namess exprs body form #f))
(define (tc-expr/maybe-expected/t e name)
(define expecteds
(map (lambda (stx) (lookup-type stx (lambda () #f))) name))
(define mk (if (and (pair? expecteds) (null? (cdr expecteds)))
car
-values))
(define tcr
(if
(andmap values expecteds)
(tc-expr/check e (mk expecteds))
(tc-expr e)))
(match tcr
[(tc-result: t) t]))
(define (tc/letrec-values/internal namess exprs body form expected)
(let* ([names (map syntax->list (syntax->list namess))]
[flat-names (apply append names)]
[exprs (syntax->list exprs)]
[exprs (syntax->list exprs)]
;; the clauses for error reporting
[clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])
(for-each (lambda (names body)
@ -88,14 +104,28 @@
;; if none of the names bound in the letrec are free vars of this rhs
[(not (ormap (lambda (n) (s:member n flat-names bound-identifier=?)) (free-vars (car exprs))))
;; then check this expression separately
(let ([t (tc-expr/t (car exprs))])
(let ([t (tc-expr/maybe-expected/t (car exprs) (car names))])
(with-lexical-env/extend
(list (car names))
(list (get-type/infer (car names) t))
(loop (cdr names) (cdr exprs) (apply append (cdr names)) (cdr clauses))))]
[else
;(for-each (lambda (vs) (for-each (lambda (v) (printf/log "Letrec Var: ~a~n" (syntax-e v))) vs)) names)
(do-check tc-expr/t names (map (lambda (l) (map get-type l)) names) form exprs body clauses expected)]))))
(do-check (lambda (stx e t)
(match (tc-expr/check e t)
[(tc-result: t) t]))
names (map (lambda (l) (map get-type l)) names) form exprs body clauses expected)]))))
;; this is so match can provide us with a syntax property to
;; say that this binding is only called in tail position
(define ((tc-expr-t/maybe-expected expected) e)
(kernel-syntax-case e #f
[(#%plain-lambda () _)
(and expected (syntax-property e 'typechecker:called-in-tail-position))
(begin
(tc-expr/check e (-> expected))
(-> expected))]
[_ (tc-expr/t e)]))
(define (tc/let-values/internal namess exprs body form expected)
(let* (;; a list of each name clause
@ -103,12 +133,12 @@
;; all the trailing expressions - the ones actually bound to the names
[exprs (syntax->list exprs)]
;; the types of the exprs
[inferred-types (map tc-expr/t exprs)]
[inferred-types (map (tc-expr-t/maybe-expected expected) exprs)]
;; the annotated types of the name (possibly using the inferred types)
[types (map get-type/infer names inferred-types)]
;; the clauses for error reporting
[clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])
(do-check (lambda (x) x) names types form inferred-types body clauses expected)))
(do-check check-type names types form inferred-types body clauses expected)))
(define (tc/let-values/check namess exprs body form expected)
(tc/let-values/internal namess exprs body form expected))

16
collects/typed-scheme/private/tc-structs.ss
View File

@ -92,7 +92,8 @@
#:type-wrapper [type-wrapper values]
#:mutable [setters? #f]
#:proc-ty [proc-ty #f]
#:maker [maker #f])
#:maker [maker #f]
#:constructor-return [cret #f])
(let* ([name (syntax-e nm)]
[fld-types (append parent-field-types types)]
[sty (make-Struct name parent fld-types proc-ty)]
@ -101,7 +102,8 @@
(register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters?
#:wrapper wrapper
#:type-wrapper type-wrapper
#:maker maker)))
#:maker maker
#:constructor-return cret)))
;; generate names, and register the approriate types give field types and structure type
;; optionally wrap things
@ -109,7 +111,8 @@
(define (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters?
#:wrapper [wrapper (lambda (x) x)]
#:type-wrapper [type-wrapper values]
#:maker [maker* #f])
#:maker [maker* #f]
#:constructor-return [cret #f])
;; create the approriate names that define-struct will bind
(define-values (maker pred getters setters) (struct-names nm flds setters?))
;; the type name that is used in all the types
@ -117,7 +120,7 @@
;; register the type name
(register-type-name nm (wrapper sty))
;; register the various function types
(register-type (or maker* maker) (wrapper (->* external-fld-types name)))
(register-type (or maker* maker) (wrapper (->* external-fld-types (if cret cret name))))
(register-types getters
(map (lambda (t) (wrapper (->* (list name) t))) external-fld-types/no-parent))
(when setters?
@ -158,7 +161,7 @@
;; typecheck a non-polymophic struct and register the approriate types
;; tc/struct : (U identifier (list identifier identifier)) Listof[identifier] Listof[syntax] -> void
(define (tc/struct nm/par flds tys [proc-ty #f] #:maker [maker #f])
(define (tc/struct nm/par flds tys [proc-ty #f] #:maker [maker #f] #:constructor-return [cret #f])
;; get the parent info and create some types and type variables
(define-values (nm parent-name parent name name-tvar) (parse-parent nm/par))
;; parse the field types, and determine if the type is recursive
@ -172,7 +175,8 @@
(mk/register-sty nm flds parent-name (get-parent-flds parent) types
;; procedure
#:proc-ty proc-ty-parsed
#:maker maker))
#:maker maker
#:constructor-return (and cret (parse-type cret))))
;; register a struct type
;; convenience function for built-in structs

8
collects/typed-scheme/private/tc-toplevel.ss
View File

@ -39,7 +39,7 @@
(parameterize ([current-orig-stx form])
(kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal define-type-internal
define-typed-struct/exec-internal :-internal assert-predicate-internal
require/typed-internal values :)
require/typed-internal values)
;; forms that are handled in other ways
[stx
(or (syntax-property form 'typechecker:ignore)
@ -57,8 +57,9 @@
;; define-typed-struct
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...))) (#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)))]
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...) #:maker m)) (#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #:maker #'m)]
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...) #:maker m #:constructor-return t))
(#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #:maker #'m #:constructor-return #'t)]
;; define-typed-struct w/ polymorphism
[(define-values () (begin (quote-syntax (define-typed-struct-internal (vars ...) nm ([fld : ty] ...))) (#%plain-app values)))
(tc/poly-struct (syntax->list #'(vars ...)) #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)))]
@ -75,6 +76,7 @@
[(define-values () (begin (quote-syntax (:-internal id ty)) (#%plain-app values)))
(identifier? #'id)
(register-type/undefined #'id (parse-type #'ty))]
;; values definitions
[(define-values (var ...) expr)

5
collects/typed-scheme/private/type-annotation.ss
View File

@ -2,7 +2,8 @@
(require "type-rep.ss" "parse-type.ss" "tc-utils.ss" "subtype.ss" "utils.ss" "union.ss" "resolve-type.ss"
"type-env.ss")
(require (lib "plt-match.ss"))
(require (lib "plt-match.ss")
mzlib/trace)
(provide type-annotation
get-type
get-type/infer
@ -67,7 +68,7 @@
[(type-annotation stx) => (lambda (x)
(log/ann stx x)
x)]
[(not (syntax-original? stx))
[(not (syntax-original? stx))
(tc-error "untyped var: ~a" (syntax-e stx))]
[else
(tc-error "no type information on variable ~a" (syntax-e stx))])))

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

@ -217,6 +217,7 @@
(let/ec exit
(let loop ([t* t])
(match t*
[(Value: '()) (-lst Univ)]
[(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*]
[(Pair: t1 t2)
(let ([t-new (loop t2)])