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

Better support for #:when clauses in the for: macros.

Browse Source 
original commit: 3518428635a7adb9f591d4cb9b8905e8add439ee
This commit is contained in:
Vincent St-Amour 2010-05-27 11:25:33 -04:00
commit 7ef168c27d
29 changed files with 334 additions and 201 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
collects/tests/typed-scheme/fail/require-typed-missing.rkt Normal file
View File

@ -0,0 +1,16 @@
#;
(exn-pred "at least one")
#lang typed/racket
(require/typed (make-main (([Listof Node] [Listof Edge] -> Graph)
(State Number Number MouseEvent -> State)
(State KeyEvent -> State)
(State -> Scene)
(Any -> Boolean)
(State -> Boolean)
(Stop -> Graph)
(Any -> Edge)
(Edge -> Graph)
->
(Boolean -> Graph))))

2
collects/tests/typed-scheme/succeed/fixnum.rkt
View File

@ -10,7 +10,7 @@
;; really badly wrong.
(: check (All (a) ((a a -> Boolean) a a -> Boolean)))
;; Simple check function as RacUnit doesn't work in Typed Scheme (yet)
;; Simple check function as RackUnit doesn't work in Typed Scheme (yet)
(define (check f a b)
(if (f a b)
#t

2
collects/tests/typed-scheme/succeed/flonum.rkt
View File

@ -5,7 +5,7 @@
scheme/unsafe/ops)
(: check (All (a) ((a a -> Boolean) a a -> Boolean)))
;; Simple check function as RacUnit doesn't work in Typed Scheme (yet)
;; Simple check function as RackUnit doesn't work in Typed Scheme (yet)
(define (check f a b)
(if (f a b)
#t

2
collects/tests/typed-scheme/succeed/flvector.rkt
View File

@ -11,7 +11,7 @@
;; really badly wrong.
(: check (All (a) ((a a -> Boolean) a a -> Boolean)))
;; Simple check function as RacUnit doesn't work in Typed Scheme (yet)
;; Simple check function as RackUnit doesn't work in Typed Scheme (yet)
(define (check f a b)
(if (f a b)
#t

25
collects/tests/typed-scheme/succeed/or-sym.rkt Normal file
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))))

15
collects/tests/typed-scheme/succeed/pr10470.rkt Normal file
View File

@ -0,0 +1,15 @@
(module pr10470 typed-scheme
(define-type-alias (Memo alpha) (U (Option alpha) (-> (Option alpha))))
(define-struct: table ([val : (Memo Number)]) #:mutable)
(: f (table -> (Option Number)))
(define (f tab)
(let ([proc-or-num (table-val tab)])
(cond
[(procedure? proc-or-num)
(let ([result (proc-or-num)])
(set-table-val! tab result)
result)]
[else proc-or-num]))))

2
collects/tests/typed-scheme/unit-tests/parse-type-tests.rkt
View File

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

10
collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt
View File

@ -611,7 +611,7 @@
(do: : Number ((x : (Listof Number) x (cdr x))
(sum : Number 0 (+ sum (car x))))
((null? x) sum)))
N]
#:ret (ret N (-FS -top -top) (make-NoObject))]
[tc-e/t (if #f 1 'foo) (-val 'foo)]
@ -794,6 +794,14 @@
[tc-e (floor 1/2) -Integer]
[tc-e (ceiling 1/2) -Integer]
[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
"check-type tests"

20
collects/typed-scheme/private/base-env-numeric.rkt
View File

@ -19,6 +19,8 @@
(define-for-syntax binop
(lambda (t [r t])
(t t . -> . r)))
(define-for-syntax rounder
(cl->* (-> -ExactRational -Integer) (-> -Flonum -Flonum) (-> -Real -Real)))
(define-for-syntax (unop t) (-> t t))
@ -112,18 +114,10 @@
(-Real . -> . -ExactRational)
(N . -> . N))]
[floor (cl->*
(-> -ExactRational -Integer)
(-> -Flonum -Flonum)
(-> -Real -Real))]
[ceiling (cl->*
(-> -ExactRational -Integer)
(-> -Flonum -Flonum)
(-> -Real -Real))]
[truncate (cl->*
(-> -ExactRational -Integer)
(-> -Flonum -Flonum)
(-> -Real -Real))]
[floor rounder]
[ceiling rounder]
[truncate rounder]
[round rounder]
[make-rectangular (-Real -Real . -> . N)]
[make-polar (-Real -Real . -> . N)]
[real-part (N . -> . -Real)]
@ -150,8 +144,6 @@
[gcd (null -Integer . ->* . -Integer)]
[lcm (null -Integer . ->* . -Integer)]
[round (-Real . -> . -Real)]
;; scheme/math
[sgn (-Real . -> . -Real)]

18
collects/typed-scheme/private/base-env.rkt
View File

@ -422,13 +422,19 @@
[match:error ((list) Univ . ->* . (Un))]
[arithmetic-shift (-Integer -Integer . -> . -Integer)]
[bitwise-and (null -Integer . ->* . -Integer)]
[bitwise-ior (null -Integer . ->* . -Integer)]
[bitwise-not (null -Integer . ->* . -Integer)]
[bitwise-xor (null -Integer . ->* . -Integer)]
[arithmetic-shift (cl->* (-Nat -Nat . -> . -Nat)
(-Integer -Integer . -> . -Integer))]
[bitwise-and (cl->* (null -Nat . ->* . -Nat)
(null -Integer . ->* . -Integer))]
[bitwise-ior (cl->* (null -Nat . ->* . -Nat)
(null -Integer . ->* . -Integer))]
[bitwise-not (cl->* (null -Nat . ->* . -Nat)
(null -Integer . ->* . -Integer))]
[bitwise-xor (cl->* (null -Nat . ->* . -Nat)
(null -Integer . ->* . -Integer))]
[abs (-Real . -> . -Real)]
[abs (cl->* (-Integer . -> . -Nat)
(-Real . -> . -Real))]
[file-exists? (-Pathlike . -> . B)]
[string->symbol (-String . -> . Sym)]

44
collects/typed-scheme/private/for-clauses.rkt Normal file
View File

@ -0,0 +1,44 @@
#lang racket/base
(require syntax/parse
"annotate-classes.rkt"
(for-template racket/base))
(provide convert-for-clauses)
;; we need handle #:when clauses manually because we need to annotate
;; the type of each nested for
(define (convert-for-clauses name clauses body ty)
(let loop ((clauses clauses))
(define-splicing-syntax-class for-clause
;; single-valued seq-expr
(pattern (var:annotated-name seq-expr:expr)
#:with expand #'(var.ann-name seq-expr))
;; multi-valued seq-expr
(pattern ((v:annotated-name ...) seq-expr:expr)
#:with expand #'((v.ann-name ...) seq-expr)))
(syntax-parse clauses
[(head:for-clause next:for-clause ... #:when rest ...)
(syntax-property
(quasisyntax/loc clauses
(#,name
(head.expand next.expand ...)
#,(loop #'(#:when rest ...))))
'type-ascription
ty)]
[(head:for-clause ...) ; we reached the end
(syntax-property
(quasisyntax/loc clauses
(#,name
(head.expand ...)
#,@body))
'type-ascription
ty)]
[(#:when guard) ; we end on a #:when clause
(quasisyntax/loc clauses
(when guard
#,@body))]
[(#:when guard rest ...)
(quasisyntax/loc clauses
(when guard
#,(loop #'(rest ...))))])))

32
collects/typed-scheme/private/optimize.rkt
View File

@ -1,6 +1,6 @@
#lang scheme/base
(require syntax/parse (for-template scheme/base scheme/unsafe/ops)
(require syntax/parse (for-template scheme/base scheme/flonum scheme/unsafe/ops)
"../utils/utils.rkt" unstable/match scheme/match unstable/syntax
(rep type-rep)
(types abbrev type-table utils))
@ -13,14 +13,20 @@
#:with opt #'e.opt))
(define-syntax-class float-binary-op
#:literals (+ - * / = <= < > >= min max)
#:literals (+ - * / = <= < > >= min max
fl+ fl- fl* fl/ fl= fl<= fl< fl> fl>= flmin flmax)
(pattern (~and i:id (~or + - * / = <= < > >= min max))
#:with unsafe (format-id #'here "unsafe-fl~a" #'i)))
#:with unsafe (format-id #'here "unsafe-fl~a" #'i))
(pattern (~and i:id (~or fl+ fl- fl* fl/ fl= fl<= fl< fl> fl>= flmin flmax))
#:with unsafe (format-id #'here "unsafe-~a" #'i)))
(define-syntax-class float-unary-op
#:literals (abs sin cos tan asin acos atan log exp)
(pattern (~and i:id (~or abs sin cos tan asin acos atan log exp))
#:with unsafe (format-id #'here "unsafe-fl~a" #'i)))
#:literals (abs sin cos tan asin acos atan log exp sqrt round floor ceiling truncate
flabs flsin flcos fltan flasin flacos flatan fllog flexp flsqrt flround flfloor flceiling fltruncate)
(pattern (~and i:id (~or abs sin cos tan asin acos atan log exp sqrt round floor ceiling truncate))
#:with unsafe (format-id #'here "unsafe-fl~a" #'i))
(pattern (~and i:id (~or flabs flsin flcos fltan flasin flacos flatan fllog flexp flsqrt flround flfloor flceiling fltruncate))
#:with unsafe (format-id #'here "unsafe-~a" #'i)))
(define-syntax-class pair-opt-expr
(pattern e:opt-expr
@ -60,11 +66,11 @@
(begin (log-optimization "unary float" #'op)
#'(op.unsafe f.opt)))
;; unlike their safe counterparts, unsafe binary operators can only take 2 arguments
(pattern (#%plain-app op:float-binary-op f fs ...)
(pattern (#%plain-app op:float-binary-op f1 f2 fs ...)
#:with opt
(begin (log-optimization "binary float" #'op)
(for/fold ([o #'f.opt])
([e (syntax->list #'(fs.opt ...))])
(for/fold ([o #'f1.opt])
([e (syntax->list #'(f2.opt fs.opt ...))])
#`(op.unsafe #,o #,e))))
(pattern (#%plain-app op:pair-unary-op p)
#:with opt
@ -99,10 +105,10 @@
#:exists 'append)
(current-output-port))))
(begin0
(parameterize ([current-output-port port])
(syntax-parse stx #:literal-sets (kernel-literals)
[e:opt-expr
(syntax/loc stx e.opt)]))
(parameterize ([current-output-port port])
(syntax-parse stx #:literal-sets (kernel-literals)
[e:opt-expr
(syntax/loc stx e.opt)]))
(if (and *log-optimizations?*
*log-optimizatons-to-log-file?*)
(close-output-port port)

2
collects/typed-scheme/private/parse-type.rkt
View File

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

45
collects/typed-scheme/private/prims.rkt
View File

@ -39,7 +39,8 @@ This file defines two sorts of primitives. All of them are provided into any mod
(private internal)
(except-in (utils utils tc-utils))
(env type-name-env)
"type-contract.rkt"))
"type-contract.rkt"
"for-clauses.rkt"))
(require (utils require-contract)
"colon.rkt"
@ -47,7 +48,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
(except-in mzlib/contract ->)
(only-in mzlib/contract [-> c->])
mzlib/struct
"base-types.rkt"
"base-types-new.rkt"
"base-types-extra.rkt")
(define-for-syntax (ignore stx) (syntax-property stx 'typechecker:ignore #t))
@ -79,7 +80,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
#:fail-unless (eq? 'opaque (syntax-e #'opaque)) #f
#:with opt #'(#:name-exists)))
(syntax-parse stx
[(_ lib (~or sc:simple-clause strc:struct-clause oc:opaque-clause) ...)
[(_ lib:expr (~or sc:simple-clause strc:struct-clause oc:opaque-clause) ...)
(unless (< 0 (length (syntax->list #'(sc ... strc ... oc ...))))
(raise-syntax-error #f "at least one specification is required" stx))
#'(begin
(require/opaque-type oc.ty oc.pred lib . oc.opt) ...
(require/typed sc.nm sc.ty lib) ...
@ -366,15 +369,39 @@ This file defines two sorts of primitives. All of them are provided into any mod
(define-syntax (do: stx)
(syntax-parse stx #:literals (:)
[(_ : ty
((var:annotated-name init (~optional step:expr #:defaults ([step #'var]))) ...)
(stop?:expr (~optional (~seq finish0:expr finish:expr ...) #:defaults ([finish0 #'(void)] [(finish 1) '()])))
((var:annotated-name rest ...) ...)
(stop?:expr ret ...)
c:expr ...)
(syntax/loc
stx
(let: doloop : ty ([var.name : var.ty init] ...)
(if stop?
(begin finish0 finish ...)
(begin c ... (doloop step ...)))))]))
(ann (do ((var.ann-name rest ...) ...)
(stop? ret ...)
c ...)
ty))]))
(define-for-syntax (define-for-variant name)
(lambda (stx)
(syntax-parse stx #:literals (:)
[(_ : ty
clauses
c:expr ...)
(convert-for-clauses name #'clauses #'(c ...) #'ty)])))
(define-syntax (define-for-variants stx)
(syntax-parse stx
[(_ (name untyped-name) ...)
(quasisyntax/loc
stx
(begin (define-syntax name (define-for-variant #'untyped-name)) ...))]))
(define-for-variants
(for: for)
(for/list: for/list)
(for/hash: for/hash)
(for/hasheq: for/hasheq)
(for/hasheqv: for/hasheqv)
(for/and: for/and)
(for/or: for/or)
(for/first: for/first)
(for/last: for/last))
(define-syntax (provide: stx)
(syntax-parse stx

1
collects/typed-scheme/private/with-types.rkt
View File

@ -8,7 +8,6 @@
"base-env-indexing-old.rkt"
"extra-procs.rkt"
"prims.rkt"
"base-types.rkt"
racket/contract/regions racket/contract/base
(for-syntax
"base-types-extra.rkt"

20
collects/typed-scheme/rep/rep-utils.rkt
View File

@ -1,7 +1,7 @@
#lang scheme/base
(require "../utils/utils.rkt")
(require mzlib/struct
(require mzlib/struct mzlib/pconvert
scheme/match
syntax/boundmap
"free-variance.rkt"
@ -265,4 +265,20 @@
(apply maker (list-update flds idx new-val)))
(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)

4
collects/typed-scheme/typecheck/signatures.rkt
View File

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

3
collects/typed-scheme/typecheck/tc-app-helper.rkt
View File

@ -1,13 +1,14 @@
#lang scheme/base
(require "../utils/utils.rkt" scheme/match unstable/list
(utils tc-utils) (rep type-rep) (types utils union))
(utils tc-utils) (rep type-rep) (types utils union abbrev))
(provide (all-defined-out))
(define (make-printable t)
(match t
[(tc-result1: t) t]
[(tc-results: ts) (-values ts)]
[_ t]))
(define (stringify-domain dom rst drst [rng #f])

143
collects/typed-scheme/typecheck/tc-expr-unit.rkt
View File

@ -181,88 +181,69 @@
(match* (o1 o2)
[(o o) #t]
[(o (or (NoObject:) (Empty:))) #t]
[(_ _) #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)
;; 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:)))
(ret ts2)]
[((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _)
expected]
[((tc-results: ts fs os) (tc-results: ts2 (NoFilter:) (NoObject:)))
(unless (= (length ts) (length ts2))
(tc-error/expr "Expected ~a values, but got ~a" (length ts2) (length ts)))
(unless (for/and ([t ts] [s ts2]) (subtype t s))
(tc-error/expr "Expected ~a, but got ~a" (stringify ts2) (stringify ts)))
(if (= (length ts) (length ts2))
(ret ts2 fs os)
(ret ts2))]
[((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:)))
(cond
[(not (subtype t1 t2))
(tc-error/expr "Expected ~a, but got ~a" t2 t1)])
expected]
[((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2))
(cond
[(not (subtype t1 t2))
(tc-error/expr "Expected ~a, but got ~a" t2 t1)]
[(and (not (filter-better? f1 f2))
(object-better? o1 o2))
(tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)]
[(and (filter-better? f1 f2)
(not (object-better? o1 o2)))
(tc-error/expr "Expected result with object ~a, got object ~a" o2 o1)]
[(and (not (filter-better? f1 f2))
(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))]
[else
expected])]
[((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
(unless (andmap subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
expected]
[((tc-results: t1 fs os) (tc-results: t2 fs os))
(unless (= (length t1) (length t2))
(tc-error/expr "Expected ~a values, but got ~a" (length t2) (length t1)))
(unless (for/and ([t t1] [s t2]) (subtype t s))
(tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
expected]
[((tc-result1: t1 f o) (? Type? t2))
(unless (subtype t1 t2)
[(_ _) #f]))
(match* (tr1 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:)))
(ret ts2)]
[((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _)
expected]
[((tc-results: ts fs os) (tc-results: ts2 (NoFilter:) (NoObject:)))
(unless (= (length ts) (length ts2))
(tc-error/expr "Expected ~a values, but got ~a" (length ts2) (length ts)))
(unless (for/and ([t ts] [s ts2]) (subtype t s))
(tc-error/expr "Expected ~a, but got ~a" (stringify ts2) (stringify ts)))
(if (= (length ts) (length ts2))
(ret ts2 fs os)
(ret ts2))]
[((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:)))
(cond
[(not (subtype t1 t2))
(tc-error/expr "Expected ~a, but got ~a" t2 t1)])
expected]
[((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2))
(cond
[(not (subtype t1 t2))
(tc-error/expr "Expected ~a, but got ~a" t2 t1)]
[(and (not (filter-better? f1 f2))
(object-better? o1 o2))
(tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)]
[(and (filter-better? f1 f2)
(not (object-better? o1 o2)))
(tc-error/expr "Expected result with object ~a, got object ~a" o2 o1)]
[(and (not (filter-better? f1 f2))
(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))])
expected]
[((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
(unless (andmap subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
expected]
[((tc-results: t1 fs os) (tc-results: t2 fs os))
(unless (= (length t1) (length t2))
(tc-error/expr "Expected ~a values, but got ~a" (length t2) (length t1)))
(unless (for/and ([t t1] [s t2]) (subtype t s))
(tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
expected]
[((tc-result1: t1 f o) (? Type? t2))
(unless (subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
(ret t2 f o)]
[((? Type? t1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:)))
(unless (subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
t1]
[((? Type? t1) (tc-result1: t2 f o))
(if (subtype t1 t2)
(tc-error/expr "Expected result with filter ~a and ~a, got ~a" f (print-object o) t1)
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
(ret t2 f o)]
[((? Type? t1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:)))
(unless (subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
t1]
[((? Type? t1) (tc-result1: t2 f o))
(if (subtype t1 t2)
(tc-error/expr "Expected result with filter ~a and ~a, got ~a" f (print-object o) t1)
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
t1]
[((? Type? t1) (? Type? t2))
(unless (subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
expected]
[(a b) (int-err "unexpected input for check-below: ~a ~a" a b)])))
t1]
[((? Type? t1) (? Type? t2))
(unless (subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
expected]
[(a b) (int-err "unexpected input for check-below: ~a ~a" a b)]))
(define (tc-expr/check/type form expected)
#;(syntax? Type/c . -> . tc-results?)

7
collects/typed-scheme/typecheck/tc-if.rkt
View File

@ -50,10 +50,12 @@
(env-props env-els))]
[(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-)))])
;(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 "els-props: ~a~n" (env-props env-els))
;(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)
;; if we have the same number of values in both cases
(cond [(= (length ts) (length us))
@ -66,6 +68,7 @@
[(_ (NoFilter:))
(-FS -top -top)]
[((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))
(-or (apply -and fs+ f2- new-thn-props) (apply -and fs- f3- new-els-props)))])]
[type (Un t2 t3)]

22
collects/typed-scheme/typecheck/tc-lambda-unit.rkt
View File

@ -41,7 +41,8 @@
(abstract-results body arg-names)
#:kws (map make-Keyword kw kw-ty req?)
#: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)
(format "Expected function with ~a argument~a~a, but got function with ~a argument~a~a"
@ -74,11 +75,11 @@
(define (check-body)
(with-lexical-env/extend
arg-list arg-types
(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))
;; make up a fake name if none exists, this is an error case anyway
(and drest (cons (or rest (generate-temporary)) drest))
(tc-exprs/check (syntax->list body) ret-ty))))
(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))
;; make up a fake name if none exists, this is an error case anyway
(and drest (cons (or rest (generate-temporary)) drest))
(tc-exprs/check (syntax->list body) ret-ty))))
(when (or (not (= arg-len tys-len))
(and (or rest-ty drest) (not rest)))
(tc-error/delayed (expected-str tys-len rest-ty drest arg-len rest)))
@ -152,7 +153,7 @@
(parameterize ([dotted-env (extend-env (list #'rest)
(list (cons rest-type bound))
(dotted-env))])
(make lam-result
(make-lam-result
(map list arg-list arg-types)
null
#f
@ -163,7 +164,7 @@
(with-lexical-env/extend
(cons #'rest arg-list)
(cons (make-Listof rest-type) arg-types)
(make lam-result
(make-lam-result
(map list arg-list arg-types)
null
(list #'rest rest-type)
@ -245,7 +246,7 @@
(tc/plambda form formals bodies expected)]
[(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: 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
[(tc-result1: (and t (Poly-names: ns expected*)))
(let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)])
@ -299,7 +300,8 @@
(unless (check-below (tc/plambda form formals bodies #f) t)
(tc-error/expr #:return expected
"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
;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> tc-result

25
collects/typed-scheme/typecheck/tc-let-unit.rkt
View File

@ -21,6 +21,11 @@
(import tc-expr^)
(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])
(((syntax? syntax? tc-results? . c:-> . any/c)
(listof (listof identifier?)) (listof tc-results?)
@ -66,17 +71,17 @@
(for/fold ([s i])
([nm (in-list (apply append abstract namess))])
(proc s nm (make-Empty) #t))))])
(define (run res)
(match res
[(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) dt db)]))
(if expected
(begin
(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)
(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) dt db)])))))
(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)
(tc/letrec-values/internal namess exprs body form expected))

18
collects/typed-scheme/typecheck/tc-toplevel.rkt
View File

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

6
collects/typed-scheme/typecheck/typechecker.rkt
View File

@ -6,12 +6,12 @@
(only-in scheme/unit
provide-signature-elements
define-values/invoke-unit/infer link)
"signatures.rkt" "tc-toplevel.rkt"
"signatures.rkt"
"tc-if.rkt" "tc-lambda-unit.rkt" "tc-app.rkt"
"tc-let-unit.rkt" "tc-dots-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
(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@))

4
collects/typed-scheme/typed-scheme.rkt
View File

@ -2,13 +2,13 @@
(require (rename-in "utils/utils.rkt" [infer r:infer]))
(require (private base-types with-types)
(require (private with-types)
(for-syntax
(except-in syntax/parse id)
scheme/base
(private type-contract optimize)
(types utils convenience)
(typecheck typechecker provide-handling)
(typecheck typechecker provide-handling tc-toplevel)
(env type-environments type-name-env type-alias-env)
(r:infer infer)
(utils tc-utils)

28
collects/typed-scheme/types/printer.rkt
View File

@ -1,9 +1,8 @@
#lang scheme/base
(require "../utils/utils.rkt")
(require (rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils)
scheme/match)
(require unstable/sequence racket/require racket/match
(path-up "rep/type-rep.rkt" "rep/filter-rep.rkt" "rep/object-rep.rkt"
"rep/rep-utils.rkt" "utils/utils.rkt" "utils/tc-utils.rkt"))
;; do we attempt to find instantiations of polymorphic types to print?
;; FIXME - currently broken
@ -18,16 +17,10 @@
;; does t have a type name associated with it currently?
;; has-name : Type -> Maybe[Symbol]
(define (has-name? t)
(define ns ((current-type-names)))
(let/ec return
(unless print-aliases
(return #f))
(for-each
(lambda (pair)
(cond [(eq? t (cdr pair))
(return (car pair))]))
ns)
#f))
(and print-aliases
(for/first ([(n t*) (in-pairs (in-list ((current-type-names))))]
#:when (and (Type? t*) (type-equal? t t*)))
n)))
(define (print-filter c port write?)
(define (fp . args) (apply fprintf port args))
@ -61,7 +54,7 @@
(define (fp . args) (apply fprintf port args))
(match c
[(NoObject:) (fp "-")]
[(Empty:) (fp "")]
[(Empty:) (fp "-")]
[(Path: pes i) (fp "~a" (append pes (list i)))]
[else (fp "(Unknown Object: ~a)" (struct->vector c))]))
@ -126,9 +119,8 @@
[(Univ:) (fp "Any")]
;; special case number until something better happens
;;[(Base: 'Number _) (fp "Number")]
[(? has-name?)
#;(printf "has a name\n")
(fp "~a" (has-name? c))]
[(app has-name? (? values name))
(fp "~a" name)]
[(StructTop: st) (fp "~a" st)]
[(BoxTop:) (fp "Box")]
[(VectorTop:) (fp "Vector")]

15
collects/typed-scheme/utils/utils.rkt
View File

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

2
collects/typed/racket/base.rkt
View File

@ -2,7 +2,7 @@
(providing (libs (except racket/base #%module-begin #%top-interaction with-handlers lambda #%app)
(providing (libs (except racket/base #%module-begin #%top-interaction with-handlers lambda #%app define-struct)
(except typed-scheme/private/prims)
(except typed-scheme/private/base-types-new)
(except typed-scheme/private/base-types-extra))

2
collects/typed/scheme/base.rkt
View File

@ -2,7 +2,7 @@
(providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers lambda #%app)
(providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers lambda #%app define-struct)
(except typed-scheme/private/prims)
(except typed-scheme/private/base-types-new)
(except typed-scheme/private/base-types-extra))