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

Add NoFilter and NoObject to represent no information about filter/object.

Browse Source 
Handle these properly in check-below (with test).
Use NoFilter and NoObject to make if typechecking work properly with filters.
Reject mismatched filters/objects (with test).

New version of require/typed that handles opaque and struct requires.
Reorganize docs around this.

svn: r15155

original commit: 7b82069fa0805e3de16c9a49d6c303789fc75419
This commit is contained in:
Sam Tobin-Hochstadt 2009-06-12 19:04:39 +00:00
parent 3e612cbb93
commit ab3e94b6e2
11 changed files with 120 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
View File

@ -718,7 +718,7 @@
(-poly (a) (a . -> . a))]
[tc-e (apply values (list 1 2 3)) #:ret (ret (list -Integer -Integer -Integer))]
[tc-e (ann (if #t 3 "foo") Integer) -Integer]
[tc-e/t (ann (if #t 3 "foo") Integer) -Integer]
[tc-e/t (plambda: (a ...) ([x : Number] . [y : a ... a])
(andmap null? (map list y)))
@ -730,7 +730,7 @@
#;[tc-err (let: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))])
(fact 20))]
#;[tc-err ]
[tc-err (ann (lambda: ([x : Any]) #f) (Any -> Boolean : String))]
)
(test-suite
"check-type tests"

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

@ -576,8 +576,10 @@
(syntax-parse stx
[(values t ...)
#:when (eq? 'values (syntax-e #'values))
(ret (map parse-type (syntax->list #'(t ...))))]
[t (ret (parse-type #'t))]))
(ret (map parse-type (syntax->list #'(t ...)))
(map (lambda (x) (make-NoFilter)) (syntax->list #'(t ...)))
(map (lambda (x) (make-NoObject)) (syntax->list #'(t ...))))]
[t (ret (parse-type #'t) (make-NoFilter) (make-NoObject))]))
(define parse-tc-results/id (parse/id parse-tc-results))

20
collects/typed-scheme/private/prims.ss
View File

@ -63,9 +63,25 @@ This file defines two sorts of primitives. All of them are provided into any mod
(pattern (orig-nm:id internal-nm:id)
#:with spec #'(orig-nm internal-nm)
#:with nm #'internal-nm))
(define-syntax-class simple-clause
#:attributes (nm ty)
(pattern [nm:opt-rename ty]))
(define-syntax-class struct-clause
#:literals (struct)
#:attributes (nm (body 1))
(pattern [struct nm:opt-rename (body ...)]))
(define-syntax-class opaque-clause
#:literals (opaque)
#:attributes (ty pred opt)
(pattern [opaque ty:id pred:id]
#:with opt #'())
(pattern [opaque ty:id pred:id #:name-exists]
#:with opt #'(#:name-exists)))
(syntax-parse stx
[(_ lib [nm:opt-rename ty] ...)
#'(begin (require/typed nm ty lib) ...)]
[(_ lib (~or [sc:simple-clause] [strc:struct-clause] [oc:opaque-clause]) ...)
#'(begin (require/typed sc.nm sc.ty lib) ...
(require-typed-struct strc.nm (strc.body ...) lib) ...
(require/opaque-type oc.ty oc.pred lib . oc.opt) ...)]
[(_ nm:opt-rename ty lib (~or [#:struct-maker parent] #:opt) ...)
(with-syntax ([cnt* (generate-temporary #'nm.nm)]
[sm (if #'parent

4
collects/typed-scheme/rep/filter-rep.ss
View File

@ -48,6 +48,10 @@
()
[result FilterSet?])])
;; represents no info about the filters of this expression
;; should only be used for parsing type annotations and expected types
(df NoFilter () [#:fold-rhs #:base])
(define index/c (or/c natural-number/c keyword?))
(dlf LBot () [#:fold-rhs #:base])

4
collects/typed-scheme/rep/object-rep.ss
View File

@ -15,6 +15,10 @@
[#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))]
[#:fold-rhs (*Path (map pathelem-rec-id p) v)])
;; represents no info about the filters of this expression
;; should only be used for parsing type annotations and expected types
(do NoObject () [#:fold-rhs #:base])
(dlo LEmpty () [#:fold-rhs #:base])
(dlo LPath ([p (listof PathElem?)] [idx index/c])

73
collects/typed-scheme/ts-reference.scrbl
View File

@ -149,6 +149,18 @@ different arity.}
@defform[(pcase-lambda: (a ...) [formals body] ...)]{
A polymorphic function of multiple arities.}
@subsection{Loops}
@defform/subs[(do: : u ([id : t init-expr step-expr-maybe] ...)
(stop?-expr finish-expr ...)
expr ...+)
([step-expr-maybe code:blank
step-expr])]{
Like @scheme[do], but each @scheme[id] having the associated type @scheme[t], and
the final body @scheme[expr] having the type @scheme[u].
}
@subsection{Definitions}
@defform*[[(define: v : t e)
@ -212,48 +224,39 @@ contexts.}
Here, @scheme[_m] is a module spec, @scheme[_pred] is an identifier
naming a predicate, and @scheme[_r] is an optionally-renamed identifier.
@defform*[[
(require/typed r t m)
(require/typed m [r t] ...)
]]{The first form requires @scheme[r] from module @scheme[m], giving
it type @scheme[t]. The second form generalizes this to multiple
identifiers.
@defform/subs[#:literals (struct opaque)
(require/typed m rt-clause ...)
([rt-clause [r t]
[struct name ([f : t] ...)]
[struct (name parent) ([f : t] ...)]
[opaque t pred]])
]{This form requires identifiers from the module @scheme[m], giving
them the specified types.
In both cases, the identifiers are protected with @rtech{contracts} which
enforce the type @scheme[t]. If this contract fails, the module
The first form requires @scheme[r], giving it type @scheme[t].
The second and third forms require the struct with name @scheme[name]
with fields @scheme[f ...], where each field has type @scheme[t]. The
third form allows a @scheme[parent] structure type to be specified.
The parent type must already be a structure type known to Typed
Scheme, either built-in or via @scheme[require/typed]. The
structure predicate has the appropriate Typed Scheme filter type so
that it may be used as a predicate in @scheme[if] expressions in Typed
Scheme.
The fourth case defines a new type @scheme[t]. @scheme[pred], imported from
module @scheme[m], is a predicate for this type. The type is defined
as precisely those values to which @scheme[pred] produces
@scheme[#t]. @scheme[pred] must have type @scheme[(Any -> Boolean)].
In all cases, the identifiers are protected with @rtech{contracts} which
enforce the specified types. If this contract fails, the module
@scheme[m] is blamed.
Some types, notably polymorphic types constructed with @scheme[All],
cannot be converted to contracts and raise a static error when used in
a @scheme[require/typed] form.}
@defform[(require/opaque-type t pred m)]{
This defines a new type @scheme[t]. @scheme[pred], imported from
module @scheme[m], is a predicate for this type. The type is defined
as precisely those values to which @scheme[pred] produces
@scheme[#t]. @scheme[pred] must have type @scheme[(Any -> Boolean)].}
@defform*[[(require-typed-struct name ([f : t] ...) m)
(require-typed-struct (name parent) ([f : t] ...) m)]]{
Requires all the functions associated with the structure @scheme[name] from the module @scheme[m],
with the appropriate types. The structure predicate has the
appropriate Typed Scheme filter type so that it may be used as a
predicate in @scheme[if] expressions in Typed Scheme.
In the second form, @scheme[parent] must already be a structure type
known to Typed Scheme, either via @scheme[define-struct:] or
@scheme[require-typed-struct].
}
@defform/subs[(do: : u ([id : t init-expr step-expr-maybe] ...)
(stop?-expr finish-expr ...)
expr ...+)
([step-expr-maybe code:blank
step-expr])]{
Like @scheme[do], but each @scheme[id] having the associated type @scheme[t], and
the final body @scheme[expr] having the type @scheme[u].
}
@section{Libraries Provided With Typed Scheme}
The @schememodname[typed-scheme] language corresponds to the

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

@ -501,8 +501,7 @@
;; syntax tc-results? -> tc-results?
(define (tc/app/check form expected)
(define t (tc/app/internal form expected))
(check-below t expected)
expected)
(check-below t expected))
(define (object-index os i)
(unless (number? i)
@ -638,4 +637,5 @@
[((arr: _ _ _ drest '()) _)
(int-err "funapp with drest args NYI")]
[((arr: _ _ _ _ kws) _)
(int-err "funapp with keyword args NYI")]))
(int-err "funapp with keyword args NYI")]))

36
collects/typed-scheme/typecheck/tc-expr-unit.ss
View File

@ -2,7 +2,7 @@
(require (rename-in "../utils/utils.ss" [private private-in]))
(require syntax/kerncase
(require syntax/kerncase mzlib/trace
scheme/match (prefix-in - scheme/contract)
"signatures.ss"
(types utils convenience union subtype)
@ -133,18 +133,42 @@
;; (Type Type -> Type))
(define (check-below tr1 expected)
(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: t1) (tc-results: t2))
(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)))
[((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: (list) (list)) (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)]
[(not (and (equal? f1 f2) (equal? o1 o2)))
(tc-error/expr "Expected result with filter ~a and object ~a, got filter ~a and object ~a" f2 o2 f1 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))

19
collects/typed-scheme/typecheck/tc-if.ss
View File

@ -18,6 +18,11 @@
(import tc-expr^)
(export tc-if^)
(define (erase-filter tc)
(match tc
[(tc-results: ts _ _)
(ret ts (for/list ([f ts]) (make-NoFilter)) (for/list ([f ts]) (make-NoObject)))]))
(define (tc/if-twoarm tst thn els [expected #f])
(define (tc expr reachable?)
(unless reachable? (warn-unreachable expr))
@ -25,7 +30,7 @@
;; if reachable? is #f, then we don't want to verify that this branch has the appropriate type
;; in particular, it might be (void)
[(and expected reachable?)
(tc-expr/check expr expected)]
(tc-expr/check expr (erase-filter expected))]
;; this code is reachable, but we have no expected type
[reachable? (tc-expr expr)]
;; otherwise, this code is unreachable
@ -41,11 +46,15 @@
[(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) fs- flag-) (tc els (unbox flag-)))])
;; if we have the same number of values in both cases
(cond [(= (length ts) (length us))
(combine-results
(for/list ([t ts] [u us] [o2 os2] [o3 os3] [f2 fs2] [f3 fs3])
(combine-filter f1 f2 f3 t u o2 o3)))]
(let ([r
(combine-results
(for/list ([t ts] [u us] [o2 os2] [o3 os3] [f2 fs2] [f3 fs3])
(combine-filter f1 f2 f3 t u o2 o3)))])
(if expected
(check-below r expected)
r))]
[else
(tc-error/expr #:return (ret Err)
(tc-error/expr #:return (ret (or expected Err))
"Expected the same number of values from both branches of if expression, but got ~a and ~a"
(length ts) (length us))])))]
[(tc-results: t _ _)

2
collects/typed-scheme/types/printer.ss
View File

@ -45,6 +45,7 @@
(for ([i thn]) (fp "~a " i)) (fp "|")
(for ([i els]) (fp " ~a" i))
(fp")")]
[(NoFilter:) (fp "-")]
[(NotTypeFilter: type path id) (fp "(! ~a @ ~a ~a)" type path (syntax-e id))]
[(TypeFilter: type path id) (fp "(~a @ ~a ~a)" type path (syntax-e id))]
[(Bot:) (fp "Bot")]))
@ -65,6 +66,7 @@
(define (print-object c port write?)
(define (fp . args) (apply fprintf port args))
(match c
[(NoObject:) (fp "-")]
[(Empty:) (fp "")]
[(Path: pes i) (fp "~a" (append pes (list (syntax-e i))))]))

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

@ -240,7 +240,7 @@
[ret
(->d ([t (or/c Type/c (listof Type/c))])
([f (if (list? t)
(listof FilterSet?)
(listof (or/c FilterSet? NoFilter?))
FilterSet?)]
[o (if (list? t)
(listof Object?)