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

Merge pull request #2 from andmkent/master

Browse Source 
let-aliasing + removing let imps
This commit is contained in:
Andrew Kent 2014-12-22 12:59:32 -05:00
commit ca88457092
13 changed files with 414 additions and 114 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
typed-racket-doc/typed-racket/scribblings/guide/occurrence.scrbl
View File

@ -157,3 +157,39 @@ interactions, which may include mutations. It is possible to work
around this by moving the variable inside of a module or into a local
binding form like @racket[let].
@section{@racket[let]-aliasing}
Typed Racket is able to reason about some cases when variables introduced
by let-expressions alias other values (e.g. when they alias non-mutated identifiers,
@racket[car]/@racket[cdr]/@racket[struct] accesses into immutable values, etc...).
This allows programs which explicitly rely on occurrence typing and aliasing to
typecheck:
@racketblock+eval[#:eval the-eval
(: f (Any -> Number))
(define (f x)
(let ([y x])
(cond
[(number? y) x]
[(and (pair? y)
(number? (car y)))
(car x)]
[else 42])))
]
It also allows the typechecker to check programs which use macros
that heavily rely on let-bindings internally (such as @racket[match]):
@racketblock+eval[#:eval the-eval
(: g (Any -> Number))
(define (g x)
(match x
[(? number?) x]
[`(_ . (_ . ,(? number?))) (cddr x)]
[`(_ . (_ . ,(? pair? p)))
(if (number? (caddr x))
(car p)
41)]
[_ 42]))
]

76
typed-racket-lib/typed-racket/env/lexical-env.rkt vendored
View File

@ -7,19 +7,26 @@
;; but split here for performance
(require "../utils/utils.rkt"
racket/keyword-transform racket/list
racket/keyword-transform racket/list racket/match racket/set
(for-syntax syntax/parse racket/base)
(contract-req)
(env type-env-structs global-env mvar-env)
(rep object-rep type-rep rep-utils)
(utils tc-utils)
(only-in (rep type-rep) Type/c)
(typecheck renamer)
(types subtype resolve union)
(except-in (types utils abbrev kw-types) -> ->* one-of/c))
(provide lexical-env with-lexical-env with-lexical-env/extend
(provide lexical-env
with-lexical-env
with-lexical-env/extend-types
with-lexical-env/extend-types+aliases
update-type/lexical)
(provide/cond-contract
[lookup-type/lexical ((identifier?) (env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))])
[lookup-type/lexical ((identifier?) (env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))]
[lookup-alias/lexical ((identifier?) (env?) . ->* . (or/c Path? Empty?))]
[path-type ((listof PathElem?) Type/c . -> . Type/c)])
;; the current lexical environment
(define lexical-env (make-parameter empty-prop-env))
@ -29,9 +36,12 @@
(parameterize ([lexical-env e]) . b))
;; run code in an extended env
(define-syntax-rule (with-lexical-env/extend is ts . b)
(define-syntax-rule (with-lexical-env/extend-types is ts . b)
(with-lexical-env (extend/values (lexical-env) is ts) . b))
;; run code in an extended env + an alias extension
(define-syntax-rule (with-lexical-env/extend-types+aliases is ts os . b)
(with-lexical-env (extend+alias/values (lexical-env) is ts os) . b))
;; find the type of identifier i, looking first in the lexical env, then in the top-level env
;; identifier -> Type
@ -54,8 +64,8 @@
=> (λ (prop)
(define orig (car (flatten prop)))
(define pre-t
(lookup-type/lexical orig env
#:fail (lambda (i) (lookup-fail i) #f)))
(lookup-type/lexical
orig env #:fail (lambda (i) (lookup-fail i) #f)))
(define t (if pre-t
(kw-convert pre-t #f)
Err))
@ -63,6 +73,10 @@
t)]
[else ((or fail lookup-fail) i)]))))))
;; looks up the representative object for an id (i.e. itself or an alias if one exists)
(define (lookup-alias/lexical i [env (lexical-env)])
(lookup-alias env i -id-path))
;; refine the type of i in the lexical env
;; (identifier type -> type) identifier -> environment
@ -86,3 +100,53 @@
[new-v (f i v)]
[new-env (extend env i new-v)])
new-env)))]))
;; returns the result of following a path into a type
;; (Listof PathElem) Type -> Type
;; Ex. '(CarPE) (Pair α β) -> α
;; resolved is the set of resolved types so far at a particular
;; path - it ensures we are making progress, that we do not
;; continue unfolding types infinitely while not progressing.
;; It is intentionally reset each time we decrease the
;; paths size on a recursive call, and maintained/extended
;; when the path does not decrease on a recursive call.
(define (path-type path t [resolved (set)])
(match* (t path)
;; empty path
[(t (list)) t]
;; pair ops
[((Pair: t s) (list rst ... (CarPE:)))
(path-type rst t)]
[((Pair: t s) (list rst ... (CdrPE:)))
(path-type rst s)]
;; syntax ops
[((Syntax: t) (list rst ... (SyntaxPE:)))
(path-type rst t)]
;; promise op
[((Promise: t) (list rst ... (ForcePE:)))
(path-type rst t)]
;; struct ops
[((Struct: nm par flds proc poly pred)
(list rst ... (StructPE: (? (λ (s) (subtype t s)) s) idx)))
(match-let ([(fld: ft _ _) (list-ref flds idx)])
(path-type rst ft))]
[((Union: ts) _)
(apply Un (map (λ (t) (path-type path t resolved)) ts))]
;; paths into polymorphic types
[((Poly: _ body-t) _) (path-type path body-t resolved)]
[((PolyDots: _ body-t) _) (path-type path body-t resolved)]
[((PolyRow: _ _ body-t) _) (path-type path body-t resolved)]
;; types which need resolving
[((? needs-resolving?) _) #:when (not (set-member? resolved t))
(path-type path (resolve-once t) (set-add resolved t))]
;; type/path mismatch =(
[(_ _)
(int-err "\n\tBad path/type lookup!\n\tPath:~a\n\tType: ~a\n" path t)]))

64
typed-racket-lib/typed-racket/env/type-env-structs.rkt vendored
View File

@ -3,13 +3,16 @@
(require racket/match
syntax/id-table
(except-in "../utils/utils.rkt" env)
(contract-req))
(contract-req)
(rep object-rep))
(require-for-cond-contract (rep type-rep filter-rep))
;; types is a free-id-table of identifiers to types
;; props is a list of known propositions
(define-struct/cond-contract env ([types immutable-free-id-table?] [props (listof Filter/c)])
(define-struct/cond-contract env ([types immutable-free-id-table?]
[props (listof Filter/c)]
[aliases immutable-free-id-table?])
#:transparent
#:property prop:custom-write
(lambda (e prt mode)
@ -22,33 +25,62 @@
[lookup (env? identifier? (identifier? . -> . any) . -> . any)]
[env-props (env? . -> . (listof Filter/c))]
[replace-props (env? (listof Filter/c) . -> . env?)]
[empty-prop-env env?])
[empty-prop-env env?]
[extend+alias/values (env? (listof identifier?) (listof Type/c) (listof Object?) . -> . env?)]
[lookup-alias (env? identifier? (identifier? . -> . (or/c #f Object?)) . -> . (or/c #f Object?))])
(define empty-prop-env
(env
(make-immutable-free-id-table)
null))
null
(make-immutable-free-id-table)))
(define (replace-props e props)
(match e
[(env tys _)
(env tys props)]))
(match-let ([(env tys _ als) e])
(env tys props als)))
(define (lookup e key fail)
(match e
[(env tys _) (free-id-table-ref tys key (λ () (fail key)))]))
(match-let ([(env tys _ _) e])
(free-id-table-ref tys key (λ () (fail key)))))
;; extend that works on single arguments
(define (extend e k v)
(extend/values e (list k) (list v)))
;; takes two lists of identifiers and types to be added
;; extends an environment with types (no aliases)
(define (extend/values e ks vs)
(match e
[(env tys p)
(env
(for/fold ([tys tys]) ([k (in-list ks)] [v (in-list vs)])
(free-id-table-set tys k v))
p)]))
(match-let* ([(env tys ps als) e]
[tys* (for/fold ([tys tys]) ([k (in-list ks)] [v (in-list vs)])
(free-id-table-set tys k v))])
(env tys* ps als)))
;; extends an environment with types and aliases
(define (extend+alias/values e ids ts os)
(match-let*-values
([((env tys ps als)) e]
[(tys* als*) (for/fold ([tys tys]
[als als])
([id (in-list ids)]
[t (in-list ts)]
[o (in-list os)])
(match o
;; no alias, so just record the type as usual
[(Empty:)
(values (free-id-table-set tys id t) als)]
;; id is aliased to an identifier
[(Path: '() id*)
;; record the alias relation *and* type of that alias id
(values (free-id-table-set tys id* t)
(free-id-table-set als id o))]
;; id is aliased to an object with a non-empty path
[(Path: p x)
;; just record the alias
(values tys (free-id-table-set als id o))]))])
(env tys* ps als*)))
(define (lookup-alias e key fail)
(match-let ([(env _ _ als) e])
(free-id-table-ref als key (λ () (fail key)))))

83
typed-racket-lib/typed-racket/infer/restrict.rkt
View File

@ -2,36 +2,67 @@
(require "../utils/utils.rkt")
(require (rep type-rep)
(types union subtype remove-intersect resolve)
(types abbrev base-abbrev union subtype remove-intersect resolve)
"signatures.rkt"
racket/match)
racket/match
racket/set)
(import infer^)
(export restrict^)
;; we don't use union map directly, since that might produce too many elements
(define (union-map f l)
(match l
[(Union: es)
(let ([l (map f es)])
(apply Un l))]))
;; NEW IMPL
;; restrict t1 to be a subtype of t2
;; if `f' is 'new, use t2 when giving up, otherwise use t1
(define (restrict* t1 t2 [f 'new])
(cond
[(subtype t1 t2) t1] ;; already a subtype
[(match t2
[(Poly: vars t)
(and (infer vars null (list t1) (list t) #f) t1)]
[_ #f])]
[(Union? t1) (union-map (lambda (e) (restrict* e t2 f)) t1)]
[(Union? t2) (union-map (lambda (e) (restrict* t1 e f)) t2)]
[(needs-resolving? t1) (restrict* (resolve-once t1) t2 f)]
[(needs-resolving? t2) (restrict* t1 (resolve-once t2) f)]
[(subtype t2 t1) t2] ;; we don't actually want this - want something that's a part of t1
[(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty
[else (if (eq? f 'new) t2 t1)])) ;; t2 and t1 have a complex relationship, so we punt
(define restrict restrict*)
;; if `pref' is 'new, use t2 when giving up, otherwise use t1
(define (restrict t1 t2 [pref 'new])
;; build-type: build a type while propogating bottom
(define (build-type constructor . args)
(if (memf Bottom? args) -Bottom (apply constructor args)))
;; resolved is a set tracking previously seen restrict cases
;; (i.e. pairs of t1 t2) to prevent infinite unfolding.
;; subtyping performs a similar check for the same
;; reason
(define (restrict* t1 t2 pref resolved)
(match* (t1 t2)
;; already a subtype
[(_ _) #:when (subtype t1 t2)
t1]
;; polymorphic restrict
[(_ (Poly: vars t)) #:when (infer vars null (list t1) (list t) #f)
t1]
;; structural recursion on types
[((Pair: a1 d1) (Pair: a2 d2))
(build-type -pair
(restrict* a1 a2 pref resolved)
(restrict* d1 d2 pref resolved))]
;; FIXME: support structural updating for structs when structs are updated to
;; contain not only *if* they are polymorphic, but *which* fields are too
;;[((Struct: _ _ _ _ _ _)
;; (Struct: _ _ _ _ _ _))]
[((Syntax: t1*) (Syntax: t2*))
(build-type -Syntax (restrict* t1* t2* pref resolved))]
[((Promise: t1*) (Promise: t2*))
(build-type -Promise (restrict* t1* t2* pref resolved))]
;; unions
[((Union: t1s) _) (apply Un (map (λ (t1*) (restrict* t1* t2 pref resolved)) t1s))]
[(_ (Union: t2s)) (apply Un (map (λ (t2*) (restrict* t1 t2* pref resolved)) t2s))]
;; resolve resolvable types if we haven't already done so
[((? needs-resolving?) _) #:when (not (set-member? resolved (cons t1 t2)))
(restrict* (resolve-once t1) t2 pref (set-add resolved (cons t1 t2)))]
[(_ (? needs-resolving?)) #:when (not (set-member? resolved (cons t1 t2)))
(restrict* t1 (resolve-once t2) pref (set-add resolved (cons t1 t2)))]
;; we don't actually want this - want something that's a part of t1
[(_ _) #:when (subtype t2 t1)
t2]
;; there's no overlap, so the restriction is empty
[(_ _) #:when (not (overlap t1 t2))
(Un)]
;; t2 and t1 have a complex relationship, so we punt
[(_ _) (if (eq? pref 'new) t2 t1)]))
(restrict* t1 t2 pref (set)))

12
typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt
View File

@ -450,32 +450,32 @@
local-private-table private-method-types
self-type))
(do-timestamp "built local tables")
(with-lexical-env/extend lexical-names/top-level lexical-types/top-level
(with-lexical-env/extend-types lexical-names/top-level lexical-types/top-level
(check-super-new super-new super-inits super-init-rest))
(do-timestamp "checked super-new")
(with-lexical-env/extend lexical-names/top-level lexical-types/top-level
(with-lexical-env/extend-types lexical-names/top-level lexical-types/top-level
(for ([stx other-top-level-exprs])
(tc-expr stx)))
(do-timestamp "checked other top-level exprs")
(with-lexical-env/extend lexical-names/top-level lexical-types/top-level
(with-lexical-env/extend-types lexical-names/top-level lexical-types/top-level
(check-field-set!s (hash-ref parse-info 'initializer-body)
local-field-table
inits))
(do-timestamp "checked field initializers")
(define checked-method-types
(with-lexical-env/extend lexical-names lexical-types
(with-lexical-env/extend-types lexical-names lexical-types
(check-methods (append (hash-ref parse-info 'pubment-names)
(hash-ref parse-info 'overridable-names))
internal-external-mapping method-stxs
methods self-type)))
(do-timestamp "checked methods")
(define checked-augment-types
(with-lexical-env/extend lexical-names lexical-types
(with-lexical-env/extend-types lexical-names lexical-types
(check-methods (hash-ref parse-info 'augment-names)
internal-external-mapping method-stxs
augments self-type)))
(do-timestamp "checked augments")
(with-lexical-env/extend lexical-names lexical-types
(with-lexical-env/extend-types lexical-names lexical-types
(check-private-methods method-stxs (hash-ref parse-info 'private-names)
private-method-types self-type))
(do-timestamp "checked privates")

38
typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
View File

@ -16,48 +16,54 @@
[one-of/c -one-of/c])
(typecheck tc-metafunctions))
(provide
with-lexical-env/extend-props)
(provide with-lexical-env/extend-props)
(define/cond-contract (update t ft pos? lo)
(Type/c Type/c boolean? (listof PathElem?) . -> . Type/c)
;; build-type: build a type while propogating bottom
(define (build-type constructor . args)
(if (memf Bottom? args) -Bottom (apply constructor args)))
(match* ((resolve t) lo)
;; pair ops
[((Pair: t s) (list rst ... (CarPE:)))
(-pair (update t ft pos? rst) s)]
(build-type -pair (update t ft pos? rst) s)]
[((Pair: t s) (list rst ... (CdrPE:)))
(-pair t (update s ft pos? rst))]
(build-type -pair t (update s ft pos? rst))]
;; syntax ops
[((Syntax: t) (list rst ... (SyntaxPE:)))
(-Syntax (update t ft pos? rst))]
(build-type -Syntax (update t ft pos? rst))]
;; promise op
[((Promise: t) (list rst ... (ForcePE:)))
(-Promise (update t ft pos? rst))]
(build-type -Promise (update t ft pos? rst))]
;; struct ops
[((Struct: nm par flds proc poly pred)
(list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)))
(make-Struct nm par
(list-update flds idx (match-lambda
[(fld: e acc-id #f)
(make-fld (update e ft pos? rst) acc-id #f)]
[_ (int-err "update on mutable struct field")]))
proc poly pred)]
;; note: this updates fields regardless of whether or not they are
;; a polymorphic field. Because subtyping is nominal and accessor
;; functions do not reflect this, this behavior is unobservable
;; except when an a variable aliases the field in a let binding
(build-type make-Struct nm par
(list-update flds idx (match-lambda
[(fld: e acc-id #f)
(make-fld (update e ft pos? rst) acc-id #f)]
[_ (int-err "update on mutable struct field")]))
proc poly pred)]
;; otherwise
[(t (list))
[(t '())
(if pos?
(restrict t ft)
(remove t ft))]
[((Union: ts) lo)
(apply Un (map (lambda (t) (update t ft pos? lo)) ts))]
(apply Un (map (λ (t) (update t ft pos? lo)) ts))]
[(t* lo)
;; This likely comes up with (-lst t) and we need to improve the system to make sure this case
;; dosen't happen
#;
(int-err "update along ill-typed path: ~a ~a ~a" t t* lo)
;;(int-err "update along ill-typed path: ~a ~a ~a" t t* lo)
t]))
;; Returns #f if anything becomes (U)

14
typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
View File

@ -7,7 +7,7 @@
"check-below.rkt" "../types/kw-types.rkt"
(types utils abbrev union subtype type-table filter-ops remove-intersect resolve generalize)
(private-in syntax-properties)
(rep type-rep filter-rep)
(rep type-rep filter-rep object-rep)
(only-in (infer infer) restrict)
(utils tc-utils)
(env lexical-env)
@ -41,8 +41,16 @@
(--> identifier? full-tc-results/c)
(define rename-id (contract-rename-id-property id))
(define id* (or rename-id id))
(define ty (lookup-type/lexical id*))
(define obj (-id-path id*))
;; see if id* is an alias for an object
;; if not (-id-path id*) is returned
(define obj (lookup-alias/lexical id*))
(define-values (alias-path alias-id)
(match obj
[(Path: p x) (values p x)]
[(Empty:) (values (list) id*)]))
;; calculate the type, resolving aliasing and paths if necessary
(define ty (path-type alias-path (lookup-type/lexical alias-id)))
(ret ty
(if (overlap ty (-val #f))
(-FS (-not-filter (-val #f) obj) (-filter (-val #f) obj))

7
typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
View File

@ -81,7 +81,7 @@
(make-arr*
arg-types
(abstract-results
(with-lexical-env/extend
(with-lexical-env/extend-types
(append rest-names arg-names)
(append rest-types arg-types)
(tc-body/check body expected))
@ -507,8 +507,9 @@
(define (tc/rec-lambda/check formals* body name args return)
(define formals (syntax->list formals*))
(define ft (t:->* args (tc-results->values return)))
(with-lexical-env/extend
(cons name formals) (cons ft args)
(with-lexical-env/extend-types
(cons name formals)
(cons ft args)
(values
(replace-names (map (λ (f) (list f -empty-obj)) (cons name formals)) (ret ft))
(replace-names (map (λ (f) (list f -empty-obj)) (cons name formals)) (tc-body/check body return)))))

34
typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
View File

@ -6,7 +6,7 @@
(private type-annotation parse-type syntax-properties)
(env lexical-env type-alias-helper mvar-env
global-env scoped-tvar-env)
(rep filter-rep)
(rep filter-rep object-rep)
syntax/free-vars
(typecheck signatures tc-metafunctions tc-subst internal-forms tc-envops)
(utils tarjan)
@ -43,33 +43,43 @@
. -> .
tc-results/c)
(with-cond-contract t/p ([expected-types (listof (listof Type/c))]
[objs (listof (listof Object?))]
[props (listof (listof Filter?))])
(define-values (expected-types props)
(for/lists (e p)
(define-values (expected-types objs props)
(for/lists (e o p)
([e-r (in-list expected-results)]
[names (in-list namess)])
(match e-r
[(list (tc-result: e-ts (FilterSet: fs+ fs-) os) ...)
(values e-ts
os
(apply append
(for/list ([n (in-list names)]
[t (in-list e-ts)]
[f+ (in-list fs+)]
[f- (in-list fs-)])
[f- (in-list fs-)]
[o (in-list os)])
(cond
[(not (overlap t (-val #f)))
(list f+)]
[(is-var-mutated? n)
(list)]
[else
(list (-imp (-not-filter (-val #f) n) f+)
(-imp (-filter (-val #f) n) f-))]))))]
;; n is being bound to an expression w/ object o
;; we don't need any new info, aliasing and the
;; lexical environment will have the needed info
[(Path? o) (list)]
;; n is being bound to an expression w/o an object
;; so remember n in our propositions
[else (list (-or (-and (-not-filter (-val #f) n) f+)
(-and (-filter (-val #f) n) f-)))]))))]
[(list (tc-result: e-ts (NoFilter:) _) ...)
(values e-ts null)]))))
;; extend the lexical environment for checking the body
(with-lexical-env/extend
;; with types and potential aliases
(with-lexical-env/extend-types+aliases
(append* namess)
(append* expected-types)
(append* objs)
(replace-names
(get-names+objects namess expected-results)
(with-lexical-env/extend-props
@ -223,9 +233,11 @@
(get-type/infer names expr
(lambda (e) (tc-expr/maybe-expected/t e names))
tc-expr/check))
(with-lexical-env/extend names ts
(replace-names (map list names os)
(loop (cdr clauses))))])))
(with-lexical-env/extend-types
names
ts
(replace-names (map list names os)
(loop (cdr clauses))))])))
;; this is so match can provide us with a syntax property to
;; say that this binding is only called in tail position

5
typed-racket-lib/typed-racket/types/printer.rkt
View File

@ -130,8 +130,9 @@
[(CarPE:) 'car]
[(CdrPE:) 'cdr]
[(ForcePE:) 'force]
[(StructPE: t i) `(,(pathelem->sexp t) ,i)]
[else `(Unknown Path Element: ,(struct->vector pathelem))]))
[(StructPE: t i) `(,(type->sexp t)-,i)]
[(SyntaxPE:) 'syntax]
[else `(Invalid Path-Element: ,(struct->vector pathelem))]))
;; object->sexp : Object -> S-expression
;; Print an Object (see object-rep.rkt) to the given port

41
typed-racket-test/succeed/aliasing-tests.rkt Normal file
View File

@ -0,0 +1,41 @@
#lang typed/racket
;; This checks that restrict can successfully update
;; by unfolding recursive definitions and structurally updating
;; down car/cdr paths
(define: (number-of-macro-definitions [expr : Sexp]) : Number
(match expr
[`(define-syntaxes (,s . ,z ). ,_ ) ;`(define-syntaxes (,s ...) ,_ ...)
(if (and (list? expr) (list? z))
(length (cons s z));;s -> cadr expr
(error "corrupted file"))]
[_ 0]))
(define: (num-of-define-syntax [exprs : (Listof Sexp)]) : Number
(foldl (lambda: ([t : Sexp] [r : Number]) (+ (number-of-macro-definitions t) r)) 0 exprs))
(struct snafu ([x : Number]))
#;(define (foo [f : snafu]) : Integer ;; doesn't (i.e. shouldn't) typecheck
(if (exact-integer? (snafu-x f))
(snafu-x f)
42))
#;(define (goo [f : snafu]) : Integer ;; doesn't (i.e. shouldn't) typecheck
(let ([n (snafu-x f)])
(if (exact-integer? n)
(snafu-x f)
42)))
(define (bar [f : snafu]) : Integer
(let ([n (snafu-x f)])
(if (exact-integer? n)
n
42)))
(define (baz [f : snafu]) : Integer
(let ([n (snafu-x f)])
(if (exact-integer? (snafu-x f))
n
42)))

44
typed-racket-test/succeed/slow-check.rkt
View File

@ -19,29 +19,27 @@
(match x
[(list _ (list (list (? number? x) y (? number? xs) ys))) 1]
[_ 2])]))
; typechecking this will be fast after implications are removed
;
; (: filters-more (-> Boolean Boolean Boolean Boolean Boolean
; Boolean Boolean Boolean Boolean Natural))
; (define (filters-more inc1? inc2? inc3? a-min?
; a-max? b-min? b-max? c-min? c-max?)
; (let-values ([(a-min? a-max?) (if inc1?
; (values a-min? a-max?)
; (values a-max? a-min?))]
; [(b-min? b-max?) (if inc2?
; (values b-min? b-max?)
; (values b-max? b-min?))]
; [(c-min? c-max?) (if inc3?
; (values c-min? c-max?)
; (values c-max? c-min?))])
; (cond [a-min? 0]
; [b-min? 1]
; [a-max? 2]
; [b-max? 3]
; [c-min? 4]
; [c-max? 5]
; [else 6])))
(: filters-more (-> Boolean Boolean Boolean Boolean Boolean
Boolean Boolean Boolean Boolean Natural))
(define (filters-more inc1? inc2? inc3? a-min?
a-max? b-min? b-max? c-min? c-max?)
(let-values ([(a-min? a-max?) (if inc1?
(values a-min? a-max?)
(values a-max? a-min?))]
[(b-min? b-max?) (if inc2?
(values b-min? b-max?)
(values b-max? b-min?))]
[(c-min? c-max?) (if inc3?
(values c-min? c-max?)
(values c-max? c-min?))])
(cond [a-min? 0]
[b-min? 1]
[a-max? 2]
[b-max? 3]
[c-min? 4]
[c-max? 5]
[else 6])))
(: bar : Any → Any)
(define (bar s)

74
typed-racket-test/unit-tests/typecheck-tests.rkt
View File

@ -273,6 +273,7 @@
racket/future
racket/list
racket/math
racket/match
racket/path
racket/place
racket/port
@ -320,7 +321,6 @@
(-filter (-val #f) var))
(make-Path null var))))
(define tests
(test-suite
"Typechecker tests"
@ -3354,7 +3354,77 @@
[tc-e ((letrec ((loop (lambda: ([x : (Listof Integer)]) (cond ((null? (cdr x)) #t) (else #f))))) loop)
(list 1 2))
-Boolean]
)
;; bottom propogation from cons
[tc-e (let ()
(: f ((U (Listof Number) (Listof String)) -> (Listof Number)))
(define f (λ (l) (cond
[(empty? l) '()]
[(number? (car l)) l]
[else (map string-length l)])))
(void))
-Void]
;; aliasing unit tests
[tc-e (let ()
(: foo (-> Any Number))
(define foo
(λ (x)
(let ([y x])
(if (number? y)
x
42))))
(void))
-Void]
[tc-e (let ()
(: foo (-> Any Number))
(define foo
(λ (x)
(match x
[(? number?) x]
[`(_ . (_ . ,(? number?))) (cddr x)]
[`(_ . (_ . ,(? pair? p)))
(if (number? (caddr x))
(car p)
41)]
[_ 42])))
(void))
-Void]
;; tests looking up path-types into unions
[tc-e (let ()
(: foo ((U (Pairof Number Number) (Pairof Number String)) -> Number))
(define foo (λ (p)
(let ([x (car p)])
x)))
(void))
-Void]
;; tests looking up path-types into polymorphic functions
[tc-e (let ()
(: poly-foo (All (α β) (U (Pairof Number α) (Pairof Number β)) -> Number))
(define poly-foo (λ (p) (let ([x (car p)])
x)))
(void))
-Void]
[tc-e (let ()
(: poly-foo (All (α β) ((U (Pairof Number α) (Pairof Number β)) -> (U α β))))
(define poly-foo (λ (p)
(let ([x (cdr p)])
x)))
(void))
-Void]
[tc-e (let ()
(: poly-foo-dots (All (α ... β) (U (Pairof Number α) (Pairof Number β)) -> Number))
(define poly-foo-dots (λ (p)
(let ([x (car p)])
(car p))))
(void))
-Void]
)
(test-suite
"tc-literal tests"