Merge branch 'master' of git.racket-lang.org:plt

This commit is contained in:
Matthew Flatt 2010-05-24 18:55:31 -06:00
commit a9250ec4f0
18 changed files with 182 additions and 136 deletions

View File

@ -1178,7 +1178,7 @@ path/s is either such a string or a list of them.
"collects/redex/examples/letrec.rkt" drdr:command-line (mzc *) "collects/redex/examples/letrec.rkt" drdr:command-line (mzc *)
"collects/redex/examples/omega.rkt" drdr:command-line (mzc *) "collects/redex/examples/omega.rkt" drdr:command-line (mzc *)
"collects/redex/examples/r6rs/r6rs-tests.rkt" drdr:command-line (mzc *) "collects/redex/examples/r6rs/r6rs-tests.rkt" drdr:command-line (mzc *)
"collects/redex/examples/r6rs/show-examples.rkt" drdr:command-line (gracket-text *) "collects/redex/examples/r6rs/show-examples.rkt" drdr:command-line (mzc *)
"collects/redex/examples/racket-machine/reduction-test.rkt" drdr:command-line (mzc *) "collects/redex/examples/racket-machine/reduction-test.rkt" drdr:command-line (mzc *)
"collects/redex/examples/racket-machine/verification-test.rkt" drdr:command-line (mzc *) "collects/redex/examples/racket-machine/verification-test.rkt" drdr:command-line (mzc *)
"collects/redex/examples/semaphores.rkt" drdr:command-line (mzc *) "collects/redex/examples/semaphores.rkt" drdr:command-line (mzc *)

View File

@ -184,7 +184,7 @@
'variant-field #'field))) 'variant-field #'field)))
... ...
(define set-variant-field! (define set-variant-field!
(lambda-memocontract (v) (lambda-memocontract (v nv)
(contract (f:variant? field/c . -> . void) (contract (f:variant? field/c . -> . void)
set-variant*-field! set-variant*-field!
'set-variant-field! 'use 'set-variant-field! 'use

View File

@ -0,0 +1,11 @@
#lang plai
(require (prefix-in eli: tests/eli-tester))
(define-type A (a (x number?)))
(define an-a (a 10))
(eli:test
(a-x an-a) => 10
(set-a-x! an-a 20)
(a-x an-a) => 20)

View File

@ -0,0 +1,25 @@
#lang typed/scheme
#;#;
(: g (Any -> Boolean : (U 'r 's)))
(define (g x)
(let ([q x])
(let ([op2 (eq? 'r x)])
(if op2 op2 (eq? 's x)))))
(define: f? : (Any -> Boolean : (U 'q 'r 's))
(lambda (x)
(let ([op1 (eq? 'q x)])
(if op1 op1
(let ([op2 (eq? 'r x)])
(if op2
;; !#f_op2
op2
(eq? 's x)))))))
(define: f2? : (Any -> Boolean : (U 'q 'r 's))
(lambda (x)
(or (eq? 'q x)
(eq? 'r x)
(eq? 's x))))

View File

@ -106,6 +106,8 @@
(-polydots (a) ((list) [a a] . ->... . N))] (-polydots (a) ((list) [a a] . ->... . N))]
[(Any -> Boolean : Number) (make-pred-ty -Number)] [(Any -> Boolean : Number) (make-pred-ty -Number)]
[(Integer -> (All (X) (X -> X)))
(t:-> -Integer (-poly (x) (t:-> x x)))]
)) ))

View File

@ -794,6 +794,14 @@
[tc-e (floor 1/2) -Integer] [tc-e (floor 1/2) -Integer]
[tc-e (ceiling 1/2) -Integer] [tc-e (ceiling 1/2) -Integer]
[tc-e (truncate 0.5) -Flonum] [tc-e (truncate 0.5) -Flonum]
[tc-e/t (ann (lambda (x) (lambda (x) x))
(Integer -> (All (X) (X -> X))))
(t:-> -Integer (-poly (x) (t:-> x x)))]
[tc-e/t (lambda: ([x : Any])
(or (eq? 'q x)
(eq? 'r x)
(eq? 's x)))
(make-pred-ty (t:Un (-val 'q) (-val 'r) (-val 's)))]
) )
(test-suite (test-suite
"check-type tests" "check-type tests"

View File

@ -365,8 +365,6 @@
[((~and kw values) tys ...) [((~and kw values) tys ...)
(add-type-name-reference #'kw) (add-type-name-reference #'kw)
(-values (map parse-type (syntax->list #'(tys ...))))] (-values (map parse-type (syntax->list #'(tys ...))))]
[(t:All . rest)
(parse-all-type stx parse-values-type)]
[t [t
(-values (list (parse-type #'t)))]))) (-values (list (parse-type #'t)))])))

View File

@ -1,7 +1,7 @@
#lang scheme/base #lang scheme/base
(require "../utils/utils.rkt") (require "../utils/utils.rkt")
(require mzlib/struct (require mzlib/struct mzlib/pconvert
scheme/match scheme/match
syntax/boundmap syntax/boundmap
"free-variance.rkt" "free-variance.rkt"
@ -266,3 +266,19 @@
(define (replace-syntax rep stx) (define (replace-syntax rep stx)
(replace-field rep stx 3)) (replace-field rep stx 3))
(define (converter v basic sub)
(define (gen-constructor sym)
(string->symbol (string-append "make-" (substring (symbol->string sym) 7))))
(match v
[(? (lambda (e) (or (Filter? e)
(Object? e)
(PathElem? e)))
(app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx vals)))
`(,(gen-constructor tag) ,@(map sub vals))]
[(? Type?
(app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx key vals)))
`(,(gen-constructor tag) ,@(map sub vals))]
[_ (basic v)]))
(current-print-convert-hook converter)

View File

@ -6,10 +6,6 @@
(types utils)) (types utils))
(provide (all-defined-out)) (provide (all-defined-out))
(define-signature typechecker^
([cnt type-check (syntax? . -> . syntax?)]
[cnt tc-toplevel-form (syntax? . -> . any)]))
(define-signature tc-expr^ (define-signature tc-expr^
([cnt tc-expr (syntax? . -> . tc-results?)] ([cnt tc-expr (syntax? . -> . tc-results?)]
[cnt tc-literal (->* (syntax?) ((or/c #f Type/c)) Type/c)] [cnt tc-literal (->* (syntax?) ((or/c #f Type/c)) Type/c)]

View File

@ -182,24 +182,6 @@
[(o o) #t] [(o o) #t]
[(o (or (NoObject:) (Empty:))) #t] [(o (or (NoObject:) (Empty:))) #t]
[(_ _) #f])) [(_ _) #f]))
(define (maybe-abstract r)
(define l (hash-ref to-be-abstr expected #f))
(define (sub-one proc i)
(for/fold ([s i])
([nm (in-list l)])
(proc s nm (make-Empty) #t)))
(define (subber proc lst)
(for/list ([i (in-list lst)])
(sub-one proc i)))
(if l
(match r
[(tc-results: ts fs os)
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
[(tc-results: ts fs os dt db)
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) (sub-one subst-type dt) db)]
[t (sub-one subst-type t)])
r))
(let ([tr1 (maybe-abstract tr1)])
(match* (tr1 expected) (match* (tr1 expected)
;; these two have to be first so that errors can be allowed in cases where multiple values are expected ;; these two have to be first so that errors can be allowed in cases where multiple values are expected
[((tc-result1: (? (lambda (t) (type-equal? t (Un))))) (tc-results: ts2 (NoFilter:) (NoObject:))) [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) (tc-results: ts2 (NoFilter:) (NoObject:)))
@ -232,9 +214,8 @@
(tc-error/expr "Expected result with object ~a, got object ~a" o2 o1)] (tc-error/expr "Expected result with object ~a, got object ~a" o2 o1)]
[(and (not (filter-better? f1 f2)) [(and (not (filter-better? f1 f2))
(not (object-better? o1 o2))) (not (object-better? o1 o2)))
(tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))] (tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))])
[else expected]
expected])]
[((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound)) [((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
(unless (andmap subtype t1 t2) (unless (andmap subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1))) (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
@ -262,7 +243,7 @@
(unless (subtype t1 t2) (unless (subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" t2 t1)) (tc-error/expr "Expected ~a, but got ~a" t2 t1))
expected] expected]
[(a b) (int-err "unexpected input for check-below: ~a ~a" a b)]))) [(a b) (int-err "unexpected input for check-below: ~a ~a" a b)]))
(define (tc-expr/check/type form expected) (define (tc-expr/check/type form expected)
#;(syntax? Type/c . -> . tc-results?) #;(syntax? Type/c . -> . tc-results?)

View File

@ -50,10 +50,12 @@
(env-props env-els))] (env-props env-els))]
[(tc-results: ts fs2 os2) (with-lexical-env env-thn (tc thn (unbox flag+)))] [(tc-results: ts fs2 os2) (with-lexical-env env-thn (tc thn (unbox flag+)))]
[(tc-results: us fs3 os3) (with-lexical-env env-els (tc els (unbox flag-)))]) [(tc-results: us fs3 os3) (with-lexical-env env-els (tc els (unbox flag-)))])
;(printf "old els-props: ~a\n" (env-props (lexical-env))) ;(printf "old props: ~a\n" (env-props (lexical-env)))
;(printf "fs+: ~a~n" fs+)
;(printf "fs-: ~a~n" fs-) ;(printf "fs-: ~a~n" fs-)
;(printf "els-props: ~a~n" (env-props env-els))
;(printf "thn-props: ~a~n" (env-props env-thn)) ;(printf "thn-props: ~a~n" (env-props env-thn))
;(printf "els-props: ~a~n" (env-props env-els))
;(printf "new-thn-props: ~a~n" new-thn-props)
;(printf "new-els-props: ~a~n" new-els-props) ;(printf "new-els-props: ~a~n" new-els-props)
;; if we have the same number of values in both cases ;; if we have the same number of values in both cases
(cond [(= (length ts) (length us)) (cond [(= (length ts) (length us))
@ -66,6 +68,7 @@
[(_ (NoFilter:)) [(_ (NoFilter:))
(-FS -top -top)] (-FS -top -top)]
[((FilterSet: f2+ f2-) (FilterSet: f3+ f3-)) [((FilterSet: f2+ f2-) (FilterSet: f3+ f3-))
;(printf "f2- ~a f+ ~a\n" f2- fs+)
(-FS (-or (apply -and fs+ f2+ new-thn-props) (apply -and fs- f3+ new-els-props)) (-FS (-or (apply -and fs+ f2+ new-thn-props) (apply -and fs- f3+ new-els-props))
(-or (apply -and fs+ f2- new-thn-props) (apply -and fs- f3- new-els-props)))])] (-or (apply -and fs+ f2- new-thn-props) (apply -and fs- f3- new-els-props)))])]
[type (Un t2 t3)] [type (Un t2 t3)]

View File

@ -41,7 +41,8 @@
(abstract-results body arg-names) (abstract-results body arg-names)
#:kws (map make-Keyword kw kw-ty req?) #:kws (map make-Keyword kw kw-ty req?)
#:rest (if rest (second rest) #f) #:rest (if rest (second rest) #f)
#:drest (if drest (cdr drest) #f)))])) #:drest (if drest (cdr drest) #f)))]
[_ (int-err "not a lam-result")]))
(define (expected-str tys-len rest-ty drest arg-len rest) (define (expected-str tys-len rest-ty drest arg-len rest)
(format "Expected function with ~a argument~a~a, but got function with ~a argument~a~a" (format "Expected function with ~a argument~a~a, but got function with ~a argument~a~a"
@ -74,7 +75,7 @@
(define (check-body) (define (check-body)
(with-lexical-env/extend (with-lexical-env/extend
arg-list arg-types arg-list arg-types
(lam-result (for/list ([al arg-list] [at arg-types] [a-ty arg-tys]) (list al at)) null (make-lam-result (for/list ([al arg-list] [at arg-types] [a-ty arg-tys]) (list al at)) null
(and rest-ty (list (or rest (generate-temporary)) rest-ty)) (and rest-ty (list (or rest (generate-temporary)) rest-ty))
;; make up a fake name if none exists, this is an error case anyway ;; make up a fake name if none exists, this is an error case anyway
(and drest (cons (or rest (generate-temporary)) drest)) (and drest (cons (or rest (generate-temporary)) drest))
@ -152,7 +153,7 @@
(parameterize ([dotted-env (extend-env (list #'rest) (parameterize ([dotted-env (extend-env (list #'rest)
(list (cons rest-type bound)) (list (cons rest-type bound))
(dotted-env))]) (dotted-env))])
(make lam-result (make-lam-result
(map list arg-list arg-types) (map list arg-list arg-types)
null null
#f #f
@ -163,7 +164,7 @@
(with-lexical-env/extend (with-lexical-env/extend
(cons #'rest arg-list) (cons #'rest arg-list)
(cons (make-Listof rest-type) arg-types) (cons (make-Listof rest-type) arg-types)
(make lam-result (make-lam-result
(map list arg-list arg-types) (map list arg-list arg-types)
null null
(list #'rest rest-type) (list #'rest rest-type)
@ -245,7 +246,7 @@
(tc/plambda form formals bodies expected)] (tc/plambda form formals bodies expected)]
[(tc-result1: (Error:)) (tc/mono-lambda/type formals bodies #f)] [(tc-result1: (Error:)) (tc/mono-lambda/type formals bodies #f)]
[(tc-result1: (and v (Values: _))) (maybe-loop form formals bodies (values->tc-results v #f))] [(tc-result1: (and v (Values: _))) (maybe-loop form formals bodies (values->tc-results v #f))]
[(tc-result1: t) (int-err "expected not an appropriate tc-result: ~a ~a" expected t)])) [_ (int-err "expected not an appropriate tc-result: ~a" expected)]))
(match expected (match expected
[(tc-result1: (and t (Poly-names: ns expected*))) [(tc-result1: (and t (Poly-names: ns expected*)))
(let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)]) (let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)])
@ -299,7 +300,8 @@
(unless (check-below (tc/plambda form formals bodies #f) t) (unless (check-below (tc/plambda form formals bodies #f) t)
(tc-error/expr #:return expected (tc-error/expr #:return expected
"Expected a value of type ~a, but got a polymorphic function." t)) "Expected a value of type ~a, but got a polymorphic function." t))
t])) t]
[_ (int-err "not a good expected value: ~a" expected)]))
;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic ;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic
;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> tc-result ;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> tc-result

View File

@ -21,6 +21,11 @@
(import tc-expr^) (import tc-expr^)
(export tc-let^) (export tc-let^)
(define (erase-filter tc)
(match tc
[(tc-results: ts _ _)
(ret ts (for/list ([f ts]) (make-NoFilter)) (for/list ([f ts]) (make-NoObject)))]))
(d/c (do-check expr->type namess results form exprs body clauses expected #:abstract [abstract null]) (d/c (do-check expr->type namess results form exprs body clauses expected #:abstract [abstract null])
(((syntax? syntax? tc-results? . c:-> . any/c) (((syntax? syntax? tc-results? . c:-> . any/c)
(listof (listof identifier?)) (listof tc-results?) (listof (listof identifier?)) (listof tc-results?)
@ -66,17 +71,17 @@
(for/fold ([s i]) (for/fold ([s i])
([nm (in-list (apply append abstract namess))]) ([nm (in-list (apply append abstract namess))])
(proc s nm (make-Empty) #t))))]) (proc s nm (make-Empty) #t))))])
(if expected (define (run res)
(begin (match res
(hash-update! to-be-abstr expected
(lambda (old-l) (apply append old-l abstract namess))
null)
(tc-exprs/check (syntax->list body) expected))
(match (tc-exprs (syntax->list body))
[(tc-results: ts fs os) [(tc-results: ts fs os)
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))] (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
[(tc-results: ts fs os dt db) [(tc-results: ts fs os dt db)
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) dt db)]))))) (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) dt db)]))
(if expected
(check-below
(run (tc-exprs/check (syntax->list body) (erase-filter expected)))
expected)
(run (tc-exprs (syntax->list body)))))))
(define (tc/letrec-values/check namess exprs body form expected) (define (tc/letrec-values/check namess exprs body form expected)
(tc/letrec-values/internal namess exprs body form expected)) (tc/letrec-values/internal namess exprs body form expected))

View File

@ -1,13 +1,13 @@
#lang scheme/unit #lang racket/base
(require (rename-in "../utils/utils.rkt" [infer r:infer])
(require (rename-in "../utils/utils.rkt" [infer r:infer])) syntax/kerncase
(require syntax/kerncase
unstable/list unstable/syntax syntax/parse unstable/debug unstable/list unstable/syntax syntax/parse unstable/debug
mzlib/etc mzlib/etc
scheme/match scheme/match
"signatures.rkt" "signatures.rkt"
"tc-structs.rkt" "tc-structs.rkt"
"typechecker.rkt"
;; to appease syntax-parse ;; to appease syntax-parse
"internal-forms.rkt" "internal-forms.rkt"
(rep type-rep) (rep type-rep)
@ -18,14 +18,16 @@
(utils tc-utils) (utils tc-utils)
"provide-handling.rkt" "provide-handling.rkt"
"def-binding.rkt" "def-binding.rkt"
(prefix-in c: racket/contract)
(for-template (for-template
"internal-forms.rkt" "internal-forms.rkt"
unstable/location unstable/location
mzlib/contract mzlib/contract
scheme/base)) scheme/base))
(import tc-expr^ check-subforms^) (c:provide/contract
(export typechecker^) [type-check (syntax? . c:-> . syntax?)]
[tc-toplevel-form (syntax? . c:-> . c:any/c)])
(define unann-defs (make-free-id-table)) (define unann-defs (make-free-id-table))

View File

@ -6,12 +6,12 @@
(only-in scheme/unit (only-in scheme/unit
provide-signature-elements provide-signature-elements
define-values/invoke-unit/infer link) define-values/invoke-unit/infer link)
"signatures.rkt" "tc-toplevel.rkt" "signatures.rkt"
"tc-if.rkt" "tc-lambda-unit.rkt" "tc-app.rkt" "tc-if.rkt" "tc-lambda-unit.rkt" "tc-app.rkt"
"tc-let-unit.rkt" "tc-dots-unit.rkt" "tc-let-unit.rkt" "tc-dots-unit.rkt"
"tc-expr-unit.rkt" "check-subforms-unit.rkt") "tc-expr-unit.rkt" "check-subforms-unit.rkt")
(provide-signature-elements typechecker^ tc-expr^) (provide-signature-elements tc-expr^ check-subforms^)
(define-values/invoke-unit/infer (define-values/invoke-unit/infer
(link tc-toplevel@ tc-if@ tc-lambda@ tc-dots@ tc-app@ tc-let@ tc-expr@ check-subforms@)) (link tc-if@ tc-lambda@ tc-dots@ tc-app@ tc-let@ tc-expr@ check-subforms@))

View File

@ -8,7 +8,7 @@
scheme/base scheme/base
(private type-contract optimize) (private type-contract optimize)
(types utils convenience) (types utils convenience)
(typecheck typechecker provide-handling) (typecheck typechecker provide-handling tc-toplevel)
(env type-environments type-name-env type-alias-env) (env type-environments type-name-env type-alias-env)
(r:infer infer) (r:infer infer)
(utils tc-utils) (utils tc-utils)
@ -43,7 +43,7 @@
([(lambda (e) (and catch-errors? (exn:fail? e) (not (exn:fail:syntax? e)))) ([(lambda (e) (and catch-errors? (exn:fail? e) (not (exn:fail:syntax? e))))
(lambda (e) (tc-error "Internal error: ~a" e))])] (lambda (e) (tc-error "Internal error: ~a" e))])]
[parameterize (;; enable fancy printing? [parameterize (;; enable fancy printing?
[custom-printer #t] [custom-printer #f]
;; a cheat to avoid units ;; a cheat to avoid units
[infer-param infer] [infer-param infer]
;; do we report multiple errors ;; do we report multiple errors

View File

@ -61,7 +61,7 @@
(define (fp . args) (apply fprintf port args)) (define (fp . args) (apply fprintf port args))
(match c (match c
[(NoObject:) (fp "-")] [(NoObject:) (fp "-")]
[(Empty:) (fp "")] [(Empty:) (fp "-")]
[(Path: pes i) (fp "~a" (append pes (list i)))] [(Path: pes i) (fp "~a" (append pes (list i)))]
[else (fp "(Unknown Object: ~a)" (struct->vector c))])) [else (fp "(Unknown Object: ~a)" (struct->vector c))]))

View File

@ -139,15 +139,12 @@ at least theoretically.
print-type* print-filter* print-latentfilter* print-object* print-latentobject* print-type* print-filter* print-latentfilter* print-object* print-latentobject*
print-pathelem*) print-pathelem*)
(define pseudo-printer (define (pseudo-printer s port mode)
(lambda (s port mode)
(parameterize ([current-output-port port] (parameterize ([current-output-port port]
[show-sharing #f] [show-sharing #f]
[booleans-as-true/false #f] [booleans-as-true/false #f]
[constructor-style-printing #t]) [constructor-style-printing #t])
(newline) (pretty-print (print-convert s))))
(pretty-print (print-convert s))
(newline))))
(define custom-printer (make-parameter #t)) (define custom-printer (make-parameter #t))