produce the correct type

original commit: 62af50867a825aab3572a442276921b205180a3a
This commit is contained in:
Sam Tobin-Hochstadt 2010-05-05 17:50:20 -04:00
commit 80e644c20d
22 changed files with 385 additions and 36 deletions

View File

@ -10,7 +10,7 @@
"unit-tests/test-utils.ss")
(define (scheme-file? s)
(regexp-match ".*[.](ss|scm)" (path->string s)))
(regexp-match ".*[.](rkt|ss|scm)" (path->string s)))
(define-namespace-anchor a)
@ -86,8 +86,8 @@
(test-suite "Typed Scheme Tests"
unit-tests int-tests))
(define (go) (test/gui tests))
(define (go/text) (run-tests tests 'verbose))
(define (go [unit? #f]) (test/gui (if unit? unit-tests tests)))
(define (go/text [unit? #f]) (run-tests (if unit? unit-tests tests) 'verbose))
(provide go go/text)

View File

@ -1,6 +1,7 @@
#lang scheme/base
#lang racket/base
(require racket/vector)
(require "main.ss")
(current-namespace (make-base-namespace))
(unless (= 0 (go/text))
(unless (= 0 (go/text (vector-member "unit" (current-command-line-arguments))))
(error "Typed Scheme Tests did not pass."))

View File

@ -0,0 +1,10 @@
#lang typed/scheme
(define-struct: x ([y : Any]) #:mutable)
(define: the-x : Any (make-x 1))
(if (x? the-x)
(x-y the-x)
0)

View File

@ -0,0 +1,18 @@
#lang typed/scheme/base
(require typed/racunit)
(: my-+ : Integer Integer -> Integer)
(define (my-+ a b)
(if (zero? a)
b
(my-+ (sub1 a) (add1 b))))
(: my-* : Integer Integer -> Integer)
(define (my-* a b)
(if (= 1 a)
b
(my-* (sub1 a) (my-+ b b))))
(test-begin
(check-equal? (my-+ 1 1) 2 "Simple addition")
(check-equal? (my-* 2 2) 4 "Simple multiplication"))

View File

@ -3,16 +3,20 @@
(require
"test-utils.ss"
"typecheck-tests.ss" ;;fail
"subtype-tests.ss" ;; pass
"type-equal-tests.ss" ;; pass
"remove-intersect-tests.ss" ;; pass
"parse-type-tests.ss" ;; pass
"type-annotation-test.ss" ;; pass
"module-tests.ss" ;; pass
"subst-tests.ss" ;; pass
"infer-tests.ss" ;; pass
"type-annotation-test.ss" ;; pass
"module-tests.ss" ;; pass
"contract-tests.ss"
(r:infer infer infer-dummy) racunit)
(r:infer infer infer-dummy)
racunit racunit/text-ui)
(provide unit-tests)
@ -22,7 +26,7 @@
(make-test-suite
"Unit Tests"
(for/list ([f (list
typecheck-tests
typecheck-tests
subtype-tests
type-equal-tests
restrict-tests

View File

@ -47,8 +47,9 @@
(syntax-case stx ()
[(_ nm a b)
(syntax/loc stx (test-check nm type-equal? a b))]))
(define-binary-check (check-tc-result-equal?* tc-result-equal/test? a b))
(define-syntax (check-tc-result-equal? stx)
(syntax-case stx ()
[(_ nm a b)
(syntax/loc stx (test-check nm tc-result-equal/test? a b))]))
(syntax/loc stx (test-case nm (check-tc-result-equal?* a b)))]))

View File

@ -6,7 +6,8 @@
(require (private base-env prims type-annotation
base-types-extra
base-env-numeric
base-env-indexing)
base-env-indexing
parse-type)
(typecheck typechecker)
(rep type-rep filter-rep object-rep)
(rename-in (types utils union convenience abbrev)
@ -17,7 +18,7 @@
(utils tc-utils utils)
unstable/mutated-vars
(env type-name-env type-environments init-envs)
racunit
racunit racunit/text-ui
syntax/parse
(for-syntax (utils tc-utils)
(typecheck typechecker)
@ -801,14 +802,17 @@
(define: foo : (Integer * -> Integer) +)
(foo 1 2 3 4 5))
-Integer]
[tc-e (let ()
(define: x : Any 7)
(if (box? x) (unbox x) 1))
Univ]
)
(test-suite
"check-type tests"
(test-exn "Fails correctly" exn:fail:syntax? (lambda () (parameterize ([orig-module-stx #'here])
(check-type #'here N B))))
(test-not-exn "Doesn't fail on subtypes" (lambda () (check-type #'here N Univ)))
(test-not-exn "Doesn't fail on equal types" (lambda () (check-type #'here N N)))
)
(test-not-exn "Doesn't fail on equal types" (lambda () (check-type #'here N N))))
(test-suite
"tc-literal tests"
(tc-l 5 -ExactPositiveInteger)
@ -822,7 +826,8 @@
(tc-l #f (-val #f))
(tc-l #"foo" -Bytes)
[tc-l () (-val null)]
)
[tc-l (3 . 4) (-pair -Pos -Pos)]
[tc-l #hash((1 . 2) (3 . 4)) (make-Hashtable -Pos -Pos)])
))

View File

@ -137,7 +137,7 @@
[tan (N . -> . N)]
[acos (N . -> . N)]
[asin (N . -> . N)]
[atan (N . -> . N)]
[atan (cl->* (N . -> . N) (-Real -Real . -> . N))]
[gcd (null -Integer . ->* . -Integer)]
[lcm (null -Integer . ->* . -Integer)]

View File

@ -116,7 +116,9 @@
[newline (->opt [-Output-Port] -Void)]
[not (-> Univ B)]
[box (-poly (a) (a . -> . (-box a)))]
[unbox (-poly (a) ((-box a) . -> . a))]
[unbox (-poly (a) (cl->*
((-box a) . -> . a)
((make-BoxTop) . -> . Univ)))]
[set-box! (-poly (a) ((-box a) a . -> . -Void))]
[box? (make-pred-ty (make-BoxTop))]
[cons? (make-pred-ty (-pair Univ Univ))]
@ -365,6 +367,11 @@
[vector-immutable (-poly (a) (->* (list) a (-vec a)))]
[vector->immutable-vector (-poly (a) (-> (-vec a) (-vec a)))]
[vector-fill! (-poly (a) (-> (-vec a) a -Void))]
[vector-argmax (-poly (a) (-> (-> a -Real) (-vec a) a))]
[vector-argmin (-poly (a) (-> (-> a -Real) (-vec a) a))]
[vector-memq (-poly (a) (-> a (-vec a) (-opt -Nat)))]
[vector-memv (-poly (a) (-> a (-vec a) (-opt -Nat)))]
[vector-member (-poly (a) (a (-vec a) . -> . (-opt -Nat)))]
;; [vector->values no good type here]

View File

@ -6,11 +6,12 @@
(utils tc-utils stxclass-util)
syntax/stx (prefix-in c: scheme/contract)
syntax/parse
(env type-environments type-name-env type-alias-env lexical-env)
(prefix-in t: (combine-in "base-types-extra.rkt" "base-types.rkt")) (only-in "colon.rkt" :)
(env type-environments type-name-env type-alias-env lexical-env)
scheme/match
(for-template scheme/base "base-types-extra.rkt" "colon.rkt")
(for-template (prefix-in t: "base-types-extra.rkt")))
(for-template scheme/base "colon.ss")
;; needed at this phase for tests
(combine-in (prefix-in t: "base-types-extra.ss") "colon.ss")
(for-template (prefix-in t: "base-types-extra.ss")))
(define-struct poly (name vars) #:prefab)
@ -86,8 +87,7 @@
(define-splicing-syntax-class latent-filter
#:description "latent filter"
(pattern (~seq t:expr @:id pe:path-elem ...)
#:fail-unless (eq? (syntax-e #'@) '@) "expected @"
(pattern (~seq t:expr (~describe "@" (~datum @)) pe:path-elem ...)
#:attr type (parse-type #'t)
#:attr path (attribute pe.pe))
(pattern t:expr
@ -98,8 +98,8 @@
(parameterize ([current-orig-stx stx])
(syntax-parse
stx
#:literals (t:Class t:Refinement t:Instance t:Tuple t:List cons t:pred t:-> : case-lambda
t:Vectorof t:mu t:Rec t:U t:All t:Opaque t:Parameter quote)
#:literals (t:Class t:Refinement t:Instance t:List cons t:pred t:-> : case-lambda
t:Rec t:U t:All t:Opaque t:Parameter quote)
[t
#:declare t (3d Type?)
(attribute t.datum)]
@ -152,7 +152,7 @@
[_ (tc-error/stx
ty
"Component of case-lambda type was not a function clause")]))))]
[((~and kw t:Vectorof) t)
#;[((~and kw t:Vectorof) t)
(add-type-name-reference #'kw)
(make-Vector (parse-type #'t))]
[((~and kw t:Rec) x:id t)
@ -289,11 +289,11 @@
(tc-error "Opaque: bad syntax")]
[(t:U . rest)
(tc-error "Union: bad syntax")]
[(t:Vectorof . rest)
#;[(t:Vectorof . rest)
(tc-error "Vectorof: bad syntax")]
[((~and (~datum mu) t:mu) . rest)
[((~and (~datum mu) t:Rec) . rest)
(tc-error "mu: bad syntax")]
[(t:mu . rest)
[(t:Rec . rest)
(tc-error "Rec: bad syntax")]
[(t ... t:-> . rest)
(tc-error "->: bad syntax")]

View File

@ -199,7 +199,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
(syntax/loc stx
(define: nm : arrty
(lambda: formals body ...))))]
[(define: nm:id ~! (~describe "type annotation" (~seq : ty)) body)
[(define: nm:id ~! (~describe ":" :) (~describe "type" ty) body)
(identifier? #'nm)
(with-syntax ([new-nm (syntax-property #'nm 'type-label #'ty)])
(syntax/loc stx (define new-nm body)))]

View File

@ -21,6 +21,7 @@
@subsubsub*section{Base Types}
@deftogether[(
@defidform[Number]
@defidform[Complex]
@defidform[Real]
@defidform[Integer]
@defidform[Natural]

View File

@ -19,9 +19,10 @@
(except-in (env type-environments) extend)
(rep type-rep filter-rep object-rep)
(r:infer infer)
'#%paramz
(for-template
(only-in '#%kernel [apply k:apply])
"internal-forms.rkt" scheme/base scheme/bool
"internal-forms.rkt" scheme/base scheme/bool '#%paramz
(only-in racket/private/class-internal make-object do-make-object)))
(import tc-expr^ tc-lambda^ tc-dots^ tc-let^)
@ -414,7 +415,21 @@
(syntax-parse form
#:literals (#%plain-app #%plain-lambda letrec-values quote
values apply k:apply not list list* call-with-values do-make-object make-object cons
andmap ormap reverse)
andmap ormap reverse extend-parameterization)
[(#%plain-app extend-parameterization pmz args ...)
(let loop ([args (syntax->list #'(args ...))])
(if (null? args) (ret Univ)
(let* ([p (car args)]
[pt (single-value p)]
[v (cadr args)]
[vt (single-value v)])
(match pt
[(tc-result1: (Param: a b))
(check-below vt a)
(loop (cddr args))]
[(tc-result1: t)
(tc-error/expr #:ret (or expected (ret Univ)) "expected Parameter, but got ~a" t)
(loop (cddr args))]))))]
;; call-with-values
[(#%plain-app call-with-values prod con)
(match (tc/funapp #'prod #'() (single-value #'prod) null #f)

View File

@ -68,6 +68,12 @@
[_ (make-Vector (apply Un
(for/list ([l (syntax-e #'i)])
(tc-literal l #f))))])]
[(~var i (3d hash?))
(let* ([h (syntax-e #'i)]
[ks (hash-map h (lambda (x y) (tc-literal x)))]
[vs (hash-map h (lambda (x y) (tc-literal y)))])
(make-Hashtable (apply Un ks) (apply Un vs)))]
[(a . b) (-pair (tc-literal #'a) (tc-literal #'b))]
[_ Univ]))

View File

@ -111,6 +111,7 @@
#:maker (or maker* maker)
#:predicate (or pred* pred)
#:struct-info si
#:poly? poly?
#:constructor-return cret))))
;; generate names, and register the approriate types give field types and structure type
@ -123,6 +124,7 @@
#:pred-wrapper [pred-wrapper values]
#:maker [maker* #f]
#:predicate [pred* #f]
#:poly? [poly? #f]
#:constructor-return [cret #f])
;; create the approriate names that define-struct will bind
(define-values (struct-type-id maker pred getters setters) (struct-names nm flds setters?))
@ -137,7 +139,7 @@
(cons (or maker* maker)
(wrapper (->* external-fld-types (if cret cret name))))
(cons (or pred* pred)
(make-pred-ty (if setters?
(make-pred-ty (if (and setters? poly?)
(make-StructTop sty)
(pred-wrapper name)))))
(for/list ([g (in-list getters)] [t (in-list external-fld-types/no-parent)] [i (in-naturals)])

View File

@ -5,14 +5,16 @@
(define-struct any-wrap (val)
#:property prop:custom-write
(lambda (v p write?)
(fprintf p "#<Typed Value>")))
(fprintf p "#<Typed Value: ~a>" (any-wrap-val v))))
(define (traverse wrap?)
(define (t v)
(match v
[(? (lambda (e) (and (any-wrap? e) (not wrap?)))) (any-wrap-val v)]
[(? (lambda (e)
(or (number? e) (string? e) (char? e) (symbol? e) (keyword? e) (bytes? e) (void? e)))) v]
(or (number? e) (string? e) (char? e) (symbol? e)
(keyword? e) (bytes? e) (boolean? e) (void? e))))
v]
[(cons x y) (cons (t x) (t y))]
[(and (? immutable?) (? vector?)) (vector-map t v)]
[(and (? immutable?) (box v)) (box (t v))]

View File

@ -46,7 +46,7 @@ don't depend on any other portion of the system
[stx (locate-stx e)])
(when (and (warn-unreachable?)
(log-level? l 'warning)
(syntax-original? (syntax-local-introduce e))
(and (syntax-transforming?) (syntax-original? (syntax-local-introduce e)))
#;(and (orig-module-stx) (eq? (debug syntax-source-module e) (debug syntax-source-module (orig-module-stx))))
#;(syntax-source-module stx))
(log-message l 'warning (format "Typed Scheme has detected unreachable code: ~e" (syntax->datum (locate-stx e)))

View File

@ -0,0 +1,60 @@
#lang racket/base
(require (for-syntax syntax/parse racket/base syntax/id-table racket/dict
unstable/debug))
(define-for-syntax (rewrite stx tbl from)
(define (rw stx)
(syntax-recertify
(syntax-parse stx #:literal-sets (kernel-literals)
[i:identifier
(dict-ref tbl #'i #'i)]
;; no expressions here
[((~or (~literal #%top) (~literal quote) (~literal quote-syntax)) . _) stx]
[(#%plain-lambda formals expr ...)
(quasisyntax/loc stx (#%plain-lambda formals #,@(map rw (syntax->list #'(expr ...)))))]
[(case-lambda [formals expr ...] ...)
(with-syntax ([((expr* ...) ...) (for*/list ([exprs (in-list (syntax->list #'((expr ...) ...)))]
[e (in-list (syntax->list exprs))])
(rw e))])
(quasisyntax/loc stx (case-lambda [formals expr* ...] ...)))]
[(let-values ([(id ...) rhs] ...) expr ...)
(with-syntax ([(rhs* ...) (map rw (syntax->list #'(rhs ...)))]
[(expr* ...) (map rw (syntax->list #'(expr ...)))])
(quasisyntax/loc stx (let-values ([(id ...) rhs*] ...) expr* ...)))]
[(letrec-values ([(id ...) rhs] ...) expr ...)
(with-syntax ([(rhs* ...) (map rw (syntax->list #'(rhs ...)))]
[(expr* ...) (map rw (syntax->list #'(expr ...)))])
(quasisyntax/loc stx (letrec-values ([(id ...) rhs*] ...) expr* ...)))]
[(letrec-syntaxes+values ([(sid ...) srhs] ...) ([(id ...) rhs] ...) expr ...)
(with-syntax ([(srhs* ...) (map rw (syntax->list #'(srhs ...)))]
[(rhs* ...) (map rw (syntax->list #'(rhs ...)))]
[(expr* ...) (map rw (syntax->list #'(expr ...)))])
(quasisyntax/loc stx (letrec-syntaxes+values ([(sid ...) srhs*] ...) ([(id ...) rhs*] ...) expr* ...)))]
[((~and kw
(~or if begin begin0 set! #%plain-app #%expression
#%variable-reference with-continuation-mark))
expr ...)
(quasisyntax/loc stx (#,#'kw #,@(map rw (syntax->list #'(expr ...)))))])
stx
(current-code-inspector)
#f))
(rw stx))
(define-syntax (define-rewriter stx)
(syntax-case stx ()
[(_ orig-name new-name [from to] ...)
#'(begin
(define-for-syntax from-list (list #'from ...))
(define-for-syntax tbl (make-immutable-free-id-table (map cons from-list (list #'to ...))))
(define-syntax (new-name stx)
(syntax-case stx ()
[(_ . args)
(let ([result (local-expand (syntax/loc stx (orig-name . args)) (syntax-local-context) null)])
(rewrite result tbl from-list))])))]))
(provide define-rewriter)
#;(define-syntax-rule (m x) (+ x 7))
#;(define-rewriter m n [+ -])
#;(n 77)

View File

@ -0,0 +1,10 @@
#lang typed/scheme
(require typed/racunit
typed/private/utils)
(require/typed/provide
racunit/gui
[test/gui
(Test * -> Any)]
[make-gui-runner
(-> (Test * -> Any))])

View File

@ -0,0 +1,170 @@
#lang typed/scheme
(require typed/private/utils
typed/private/rewriter
"type-env-ext.rkt")
(define-type check-ish-ty
(case-lambda
(Any Any -> (U #t Void))
(Any Any String -> (U #t Void))))
(define-type (Predicate A) (A -> Boolean))
(define-type (Thunk A) (-> A))
; 3.2
(require/typed/provide
racunit
[check (All (A B C)
(case-lambda
((A B -> C) A B -> C)
((A B -> C) A B String -> C)))]
[check-eq? check-ish-ty]
[check-not-eq? check-ish-ty]
[check-eqv? check-ish-ty]
[check-not-eqv? check-ish-ty]
[check-equal? check-ish-ty]
[check-not-equal? check-ish-ty]
[check-pred
(All (A B)
(case-lambda
((A -> B) A -> #t)
((A -> B) A String -> #t)))]
[check-=
(case-lambda
(Number Number Number -> #t)
(Number Number Number String -> #t))]
[check-true
(case-lambda
(Boolean -> #t)
(Boolean String -> #t))]
[check-false
(case-lambda
(Boolean -> #t)
(Boolean String -> #t))]
[check-not-false
(case-lambda
(Any -> #t)
(Any String -> #t))]
[check-exn
(case-lambda
((Predicate Any) (Thunk Any) -> #t)
((Predicate Any) (Thunk Any) String -> #t))]
[check-not-exn
(case-lambda
((Thunk Any) -> #t)
((Thunk Any) String -> #t))]
[fail
(case-lambda
(-> #t)
(String -> #t))]
[check-regexp-match
(Regexp String -> #t)])
; 3.2.1
(require-typed-struct check-info
([name : Symbol] [value : Any])
racunit)
(define-type CheckInfo check-info)
(provide (struct-out check-info) CheckInfo)
(require/typed/provide
racunit
[make-check-name (String -> CheckInfo)]
[make-check-params ((Listof Any) -> CheckInfo)]
[make-check-location ((List Any (Option Number) (Option Number) (Option Number) (Option Number)) -> CheckInfo)]
[make-check-expression (Any -> CheckInfo)]
[make-check-message (String -> CheckInfo)]
[make-check-actual (Any -> CheckInfo)]
[make-check-expected (Any -> CheckInfo)]
[with-check-info* (All (A) ((Listof CheckInfo) (Thunk A) -> A))])
(require (only-in racunit with-check-info))
(provide with-check-info)
; 3.2.2
(require (only-in racunit define-simple-check define-binary-check define-check fail-check))
(provide define-simple-check define-binary-check define-check fail-check)
; 3.2.3
(require/typed/provide
racunit
[current-check-handler
(Parameter (Any -> Any))]
[current-check-around
(Parameter ((Thunk Any) -> Any))])
; 3.3
(require (prefix-in t: (except-in racunit struct:check-info struct:exn:test struct:exn:test:check struct:test-result struct:test-failure
struct:test-error struct:test-success)))
(define-rewriter t:test-begin test-begin
[t:current-test-case-around current-test-case-around]
[t:check-around check-around]
[t:current-check-handler current-check-handler]
[t:current-check-around current-check-around])
(define-rewriter t:test-case test-case
[t:current-test-case-around current-test-case-around]
[t:check-around check-around]
[t:current-check-handler current-check-handler]
[t:current-check-around current-check-around])
(provide test-begin test-case)
(require/opaque-type TestCase test-case? racunit)
(provide TestCase test-case?)
(require (only-in racunit test-suite))
(provide test-suite)
(require/opaque-type TestSuite test-suite? racunit)
(provide TestSuite test-suite?)
(define-type Test (U TestCase TestSuite))
(provide Test)
(require/typed/provide
racunit
[make-test-suite
(case-lambda
(String (Listof Test) -> TestSuite)
; XXX #:before #:after
)])
(require (only-in racunit define-test-suite define/provide-test-suite))
(provide define-test-suite define/provide-test-suite)
(require/typed/provide
racunit
[current-test-name (Parameter (Option String))]
[current-test-case-around (Parameter ((Thunk Any) -> Any))]
[test-suite-test-case-around ((Thunk Any) -> Any)]
[test-suite-check-around ((Thunk Any) -> Any)])
; 3.4
(require (only-in racunit before after around delay-test))
(provide before after around delay-test)
; 3.5
; XXX require/expose seems WRONG for typed/scheme
; 3.7
(require-typed-struct (exn:test exn) () racunit)
(require-typed-struct (exn:test:check exn:test) ([stack : (Listof CheckInfo)]) racunit)
(require-typed-struct test-result ([test-case-name : (Option String)]) racunit)
(require-typed-struct (test-failure test-result) ([result : Any]) racunit)
(require-typed-struct (test-error test-result) ([result : Any]) racunit)
(require-typed-struct (test-success test-result) ([result : Any]) racunit)
(provide (struct-out exn:test) (struct-out exn:test:check)
(struct-out test-result)
(struct-out test-failure) (struct-out test-error) (struct-out test-success))
(define-type (Tree A)
(Rec The-Tree
(Listof (U A The-Tree))))
(require/typed/provide
racunit
[run-test-case
((Option String) (Thunk Any) -> test-result)]
[run-test
(Test -> (Tree test-result))]
; XXX Requires keywords and weird stuff
#;[fold-test-results
XXX]
; XXX Requires knowing more about test cases and structs
#;[foldts
XXX])

View File

@ -0,0 +1,14 @@
#lang typed/scheme
(require typed/racunit
typed/private/utils)
(define-type Verbosity
(U 'quiet 'normal 'verbose))
(require/typed/provide
racunit/text-ui
[run-tests
(case-lambda
(Test -> Natural)
(Test Verbosity -> Natural))])
(provide Verbosity)

View File

@ -0,0 +1,23 @@
#lang scheme/base
(require typed-scheme/utils/utils
(prefix-in ru: (combine-in racunit racunit/private/test-case racunit/private/check))
(for-syntax
scheme/base syntax/parse
(utils tc-utils)
(env init-envs)
(except-in (rep filter-rep object-rep type-rep) make-arr)
(types convenience union)
(only-in (types convenience) [make-arr* make-arr])))
(define-for-syntax unit-env
(make-env
[ru:check-around
(-poly (a) (-> (-> a) a))]
;; current-test-case-around
[(syntax-parse (local-expand #'(ru:test-begin 0) 'expression null)
#:context #'ru:test-begin
[(_ _ . _) #'ctca])
(-poly (a) (-> (-> a) a))]))
(begin-for-syntax (initialize-type-env unit-env))