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

simplify arrows a little, less list allocation (#566)

Browse Source
This commit is contained in:
Andrew Kent 2017-07-01 16:56:22 +01:00 committed by GitHub
parent c97c90d2ee
commit fa828df919
58 changed files with 1758 additions and 1658 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
typed-racket-lib/typed-racket/base-env/base-special-env.rkt
View File

@ -11,8 +11,7 @@
(for-template (only-in racket/private/kw kw-expander-proc kw-expander-impl)
racket/base racket/file racket/port racket/path racket/list)
(env init-envs)
(rename-in (types abbrev numeric-tower)
[make-arr* make-arr])
(types abbrev numeric-tower)
(for-syntax racket/base syntax/parse
(only-in racket/syntax syntax-local-eval)))
(provide make-template-identifier)

11
typed-racket-lib/typed-racket/base-env/top-interaction.rkt
View File

@ -95,7 +95,8 @@
#,(pretty-format-rep
(match type
[(tc-result1: t f o) t]
[(tc-results: t) (-values t)]
[(tc-results: (list (tc-result: ts) ...) _)
(-values ts)]
[(tc-any-results: f) (-AnyValues f)]))))
"must be applied to exactly one argument")
@ -110,20 +111,20 @@
#`(display
#,(pretty-format-rep
(match type
[(tc-result1: (and t (Function: _)) f o) t]))))
[(tc-result1: (and t (? Fun?)) f o) t]))))
"must be applied to at least one argument" )
;; given a function and a desired return type, fill in the blanks
(define-repl-op :query-type/result-impl (_ op desired-type) #'op
(λ (type)
(match type
[(tc-result1: (and t (Function: _)) f o)
[(tc-result1: (and t (? Fun?)) f o)
(let ([cleaned (cleanup-type t (parse-type #'desired-type) #f)])
#`(display
#,(match cleaned
[(Function: '())
[(Fun: '())
"Desired return type not in the given function's range.\n"]
[(Function: arrs)
[(Fun: _)
(pretty-format-rep cleaned)])))]
[_ (error (format "~a: not a function" (syntax->datum #'op)))]))
"must be applied to exactly two arguments"))

83
typed-racket-lib/typed-racket/env/init-envs.rkt vendored
View File

@ -160,32 +160,42 @@
`(make-Immutable-HashTable ,(type->sexp key) ,(type->sexp val))]
[(Weak-HashTable: key val)
`(make-Weak-HashTable ,(type->sexp key) ,(type->sexp val))]
[(Function: (list (arr: dom (Values: (list (Result: t
(PropSet: (TrueProp:)
(TrueProp:))
(Empty:))))
#f #f '())))
[(Fun: (list (Arrow: dom #f '()
(Values:
(list
(Result: t
(PropSet: (TrueProp:)
(TrueProp:))
(Empty:)))))))
`(simple-> (list ,@(map type->sexp dom)) ,(type->sexp t))]
[(Function: (list (arr: dom (Values: (list (Result: t (PropSet: (TypeProp: pth ft)
(NotTypeProp: pth ft))
(Empty:))))
#f #f '())))
[(Fun: (list (Arrow: dom #f'()
(Values:
(list
(Result: t
(PropSet:
(TypeProp: pth ft)
(NotTypeProp: pth ft))
(Empty:)))))))
`(make-pred-ty (list ,@(map type->sexp dom))
,(type->sexp t)
,(type->sexp ft)
,(object->sexp pth))]
[(Function: (list (arr: dom (Values: (list (Result: t (PropSet: (NotTypeProp: (Path: pth (cons 0 0))
(== -False))
(TypeProp: (Path: pth (cons 0 0))
(== -False)))
(Path: pth (cons 0 0)))))
#f #f '())))
[(Fun: (list (Arrow: dom #f '()
(Values:
(list
(Result: t
(PropSet:
(NotTypeProp: (Path: pth (cons 0 0))
(== -False))
(TypeProp: (Path: pth (cons 0 0))
(== -False)))
(Path: pth (cons 0 0))))))))
`(->acc (list ,@(map type->sexp dom))
,(type->sexp t)
(list ,@(map path-elem->sexp pth)))]
[(Function: (? has-optional-args? arrs))
(match-define (arr: fdoms rng rest _ *kws) (first arrs))
(match-define (arr: ldoms _ _ _ _) (last arrs))
[(Fun: (? has-optional-args? arrs))
(match-define (Arrow: fdoms rest *kws rng) (first arrs))
(match-define (Arrow: ldoms _ _ _) (last arrs))
(define opts (drop ldoms (length fdoms)))
(define kws (map type->sexp *kws))
`(opt-fn (list ,@(map type->sexp fdoms))
@ -193,8 +203,7 @@
,(type->sexp rng)
,@(if rest `(#:rest ,rest) '())
,@(if (null? kws) '() `(#:kws (list ,@kws))))]
[(Function: arrs)
`(make-Function (list ,@(map type->sexp arrs)))]
[(Fun: arrs) `(make-Fun (list ,@(map type->sexp arrs)))]
[(Keyword: kw ty required?)
`(make-Keyword (quote ,kw) ,(type->sexp ty) ,required?)]
[(Values: rs)
@ -293,22 +302,24 @@
(list ,@(map type->sexp exports))
(list ,@(map type->sexp init-depends))
,(type->sexp result))]
[(arr: dom (Values: (list (Result: t (PropSet: (TrueProp:)
(TrueProp:))
(Empty:))))
#f #f '())
`(make-arr* (list ,@(map type->sexp dom))
,(type->sexp t))]
[(arr: dom rng #f #f '())
`(make-arr* (list ,@(map type->sexp dom))
,(type->sexp rng))]
[(arr: dom rng rest drest kws)
`(make-arr (list ,@(map type->sexp dom))
,(type->sexp rng)
,(and rest (type->sexp rest))
,(and drest `(cons ,(type->sexp (car drest))
(quote ,(cdr drest))))
(list ,@(map type->sexp kws)))]
[(Arrow: dom #f '()
(Values: (list (Result: t (PropSet: (TrueProp:)
(TrueProp:))
(Empty:)))))
`(-Arrow (list ,@(map type->sexp dom))
,(type->sexp t))]
[(Arrow: dom #f '() rng)
`(-Arrow (list ,@(map type->sexp dom))
,(type->sexp rng))]
[(Arrow: dom rest kws rng)
`(make-Arrow
(list ,@(map type->sexp dom))
,(and rest (type->sexp rest))
(list ,@(map type->sexp kws))
,(type->sexp rng))]
[(RestDots: ty db)
`(make-RestDots ,(type->sexp ty)
(quote ,db))]
[(Distinction: nm id ty)
`(make-Distinction (quote ,nm)
(quote ,id)

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

@ -39,6 +39,7 @@
(define (add-props-to-current-lexical! ps)
(lexical-env (env-replace-props (lexical-env) (append ps (env-props (lexical-env))))))
;; run code in an extended env
(define-syntax (with-extended-lexical-env stx)
(syntax-parse stx
@ -48,15 +49,19 @@
#:defaults ([objs #'#f]))]
. body)
(syntax/loc stx
(let ([idents ids]
(let ([cur-env (lexical-env)]
[idents ids]
[types tys])
(let ([ps (apply append
(for*/list ([(id ty) (in-parallel (in-list idents) (in-list types))]
[props (in-value (extract-props (-id-path id) ty))]
#:unless (null? props))
props))])
(with-lexical-env (env-replace-props (env-extend/bindings (lexical-env) ids tys objs)
(append ps (env-props (lexical-env))))
(let ([ps (apply
append
(for*/list ([(id ty) (in-parallel (in-list idents) (in-list types))]
[props (in-value (extract-props (-id-path id) ty))]
#:unless (null? props))
props))])
(with-lexical-env
(env-replace-props
(env-extend/bindings cur-env ids tys objs)
(append ps (env-props cur-env)))
. body))))]))
;; find the type of identifier i, looking first in the lexical env, then in the top-level env

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

@ -2,6 +2,7 @@
(require racket/match
syntax/id-table
racket/sequence
(except-in "../utils/utils.rkt" env)
(contract-req)
;; dict ops only used for convenient printing
@ -68,10 +69,22 @@
;; simplifications like env+ in tc-envops.rkt)
(define-syntax (with-naively-extended-lexical-env stx)
(syntax-parse stx
[(_ [#:props ps:expr]
[(_ [(~optional (~seq #:identifiers ids-expr:expr
#:types ts-expr:expr)
#:defaults ([ids-expr #'(list)]
[ts-expr #'(list)]))
(~optional (~seq #:props ps:expr)
#:defaults ([ps #'(list)]))]
. body)
(syntax/loc stx
(with-lexical-env (env-replace-props (lexical-env) (append ps (env-props (lexical-env)))) . body))]))
(let ([cur-env (lexical-env)]
[ids ids-expr]
[ts ts-expr])
(with-lexical-env
(env-replace-props
(env-extend/bindings cur-env ids ts #f)
(append ps (env-props cur-env)))
. body)))]))
(define (env-replace-props e props)

30
typed-racket-lib/typed-racket/infer/infer-unit.rkt
View File

@ -367,18 +367,20 @@
(extend-tvars (list dbound)
(cgen/seq (context-add context #:bounds (list dbound)) (seq ss (uniform-end s-dty)) t-seq))])]))
(define/cond-contract (cgen/arr context s-arr t-arr)
(context? arr? arr? . -> . (or/c #f cset?))
(define/cond-contract (cgen/arrow context s-arr t-arr)
(context? Arrow? Arrow? . -> . (or/c #f cset?))
(match* (s-arr t-arr)
[((arr: ss s s-rest s-drest s-kws) (arr: ts t t-rest t-drest t-kws))
(define (rest->end rest drest)
(cond
[rest (uniform-end rest)]
[drest (dotted-end (car drest) (cdr drest))]
[else (null-end)]))
[((Arrow: ss s-rest s-kws s)
(Arrow: ts t-rest t-kws t))
(define (rest->end rest)
(match rest
[(? Type?) (uniform-end rest)]
[(RestDots: ty dbound)
(dotted-end ty dbound)]
[_ (null-end)]))
(define s-seq (seq ss (rest->end s-rest s-drest)))
(define t-seq (seq ts (rest->end t-rest t-drest)))
(define s-seq (seq ss (rest->end s-rest)))
(define t-seq (seq ts (rest->end t-rest)))
(and (null? s-kws)
(null? t-kws)
(% cset-meet
@ -545,7 +547,7 @@
(and cs
(implies-in-env? (lexical-env)
(-is-type obj S)
(instantiate-rep/obj raw-prop obj S))
(instantiate-obj raw-prop obj))
(cset-meet* (cons empty cs))))]
;; constrain *each* element of es to be below T, and then combine the constraints
@ -768,14 +770,14 @@
;; parameters are just like one-arg functions
[((Param: in1 out1) (Param: in2 out2))
(% cset-meet (cg in2 in1) (cg out1 out2))]
[((Function: (list s-arr ...))
(Function: (list t-arr ...)))
[((Fun: s-arr)
(Fun: t-arr))
(% cset-meet*
(for/list/fail
([t-arr (in-list t-arr)])
;; for each element of t-arr, we need to get at least one element of s-arr that works
(let ([results (for*/list ([s-arr (in-list s-arr)]
[v (in-value (cgen/arr context s-arr t-arr))]
[v (in-value (cgen/arrow context s-arr t-arr))]
#:when v)
v)])
;; ensure that something produces a constraint set

28
typed-racket-lib/typed-racket/infer/promote-demote.rkt
View File

@ -36,22 +36,23 @@
;; Returns the changed arr or #f if there is no arr above it
(define (arr-change arr)
(match arr
[(arr: dom rng rest drest kws)
[(Arrow: dom rest kws rng)
(cond
[(apply V-in? V (get-propsets rng))
#f]
[(and drest (memq (cdr drest) V))
(make-arr (map contra dom)
(co rng)
(contra (car drest))
#f
(map contra kws))]
[(and (RestDots? rest)
(memq (RestDots-nm rest) V))
(make-Arrow
(map contra dom)
(contra (RestDots-ty rest))
(map contra kws)
(co rng))]
[else
(make-arr (map contra dom)
(co rng)
(and rest (contra rest))
(and drest (cons (contra (car drest)) (cdr drest)))
(map contra kws))])]))
(make-Arrow
(map contra dom)
(and rest (contra rest))
(map contra kws)
(co rng))])]))
(match cur
[(app Rep-variances variances) #:when variances
(define mk (Rep-constructor cur))
@ -72,8 +73,7 @@
[(F: name) (if (memq name V)
(if change Univ -Bottom)
cur)]
[(Function: arrs)
(make-Function (filter-map arr-change arrs))]
[(Fun: arrs) (make-Fun (filter-map arr-change arrs))]
[(HeterogeneousVector: elems)
(make-HeterogeneousVector (map (λ (t) (if (V-in? V t)
(if change Univ -Bottom)

9
typed-racket-lib/typed-racket/logic/proves.rkt
View File

@ -7,14 +7,9 @@
("../typecheck/tc-subst.rkt" (instantiate-rep/obj)))
(provide (rename-out [implies-in-env?-for-stupid-infer-unit
implies-in-env?]
[instantiate-rep/obj-for-stupid-infer-unit
instantiate-rep/obj]))
implies-in-env?]))
;; the units for infer currently make it impossible to do
;; lazy requires
(define (implies-in-env?-for-stupid-infer-unit env p q)
(implies-in-env? env p q))
(define (instantiate-rep/obj-for-stupid-infer-unit rep obj type)
(instantiate-rep/obj rep obj type))
(implies-in-env? env p q))

8
typed-racket-lib/typed-racket/optimizer/unboxed-let.rkt
View File

@ -128,10 +128,10 @@
(pattern ((fun-name:constant-var) (~and fun (#%plain-lambda params body ...)))
#:do [(define doms
(match (type-of #'fun)
[(tc-result1: (Function: (list (arr: doms rngs
(and rests #f)
(and drests #f)
(and kws '())))))
[(tc-result1: (Fun: (list (Arrow: doms
#f ;; rest arg
'() ;; kw args
_))))
doms]
[_ #f]))]
#:when doms

42
typed-racket-lib/typed-racket/private/parse-type.rkt
View File

@ -3,11 +3,10 @@
;; This module provides functions for parsing types written by the user
(require (rename-in "../utils/utils.rkt" [infer infer-in])
(except-in (rep core-rep type-rep object-rep rep-utils) make-arr)
(rename-in (types abbrev utils prop-ops resolve
classes prefab signatures
subtype path-type numeric-tower)
[make-arr* make-arr])
(rep core-rep type-rep object-rep rep-utils)
(types abbrev utils prop-ops resolve
classes prefab signatures
subtype path-type numeric-tower)
(only-in (infer-in infer) intersect)
(utils tc-utils stxclass-util literal-syntax-class)
syntax/stx (prefix-in c: (contract-req))
@ -518,7 +517,7 @@
(parse-object-type stx)]
[(:Refinement^ p?:id)
(match (lookup-id-type/lexical #'p?)
[(and t (Function: (list (arr: (list dom) _ #f #f '()))))
[(and t (Fun: (list (Arrow: (list dom) #f '() _))))
(make-Refinement dom #'p?)]
[t (parse-error "expected a predicate for argument to Refinement"
"given" t)])]
@ -613,11 +612,11 @@
[(:pred^ t)
(make-pred-ty (parse-type #'t))]
[(:case->^ tys ...)
(make-Function
(make-Fun
(for/list ([ty (in-syntax #'(tys ...))])
(let ([t (parse-type ty)])
(match t
[(Function: (list arr)) arr]
[(Fun: (list arr)) arr]
[_ (parse-error
#:stx ty
"expected a function type for component of case-> type"
@ -688,10 +687,8 @@
(with-arity (length doms)
(let ([doms (for/list ([d (in-list doms)])
(parse-type d))])
(make-Function
(list (make-arr
doms
(parse-type (syntax/loc stx (rest-dom ...))))))))]
(make-Fun
(list (-Arrow doms (parse-type (syntax/loc stx (rest-dom ...))))))))]
[(~or (:->^ dom rng :colon^ latent:simple-latent-prop)
(dom :->^ rng :colon^ latent:simple-latent-prop))
;; use parse-type instead of parse-values-type because we need to add the props from the pred-ty
@ -701,8 +698,8 @@
[(~or (:->^ dom:non-keyword-ty ... kws:keyword-tys ... rest:non-keyword-ty ddd:star rng)
(dom:non-keyword-ty ... kws:keyword-tys ... rest:non-keyword-ty ddd:star :->^ rng))
(with-arity (length (syntax->list #'(dom ...)))
(make-Function
(list (make-arr
(make-Fun
(list (-Arrow
(parse-types #'(dom ...))
(parse-values-type #'rng)
#:rest (parse-type #'rest)
@ -716,7 +713,7 @@
#:stx #'bound
"used a type variable not bound with ... as a bound on a ..."
"variable" bnd))
(make-Function
(make-Fun
(list
(make-arr-dots (parse-types #'(dom ...))
(parse-values-type #'rng)
@ -727,7 +724,7 @@
(dom:non-keyword-ty ... rest:non-keyword-ty _:ddd :->^ rng))
(with-arity (length (syntax->list #'(dom ...)))
(let ([var (infer-index stx)])
(make-Function
(make-Fun
(list
(make-arr-dots (parse-types #'(dom ...))
(parse-values-type #'rng)
@ -744,11 +741,10 @@
(with-arity (length doms)
(let ([doms (for/list ([d (in-list doms)])
(parse-type d))])
(make-Function
(list (make-arr
doms
(parse-values-type #'rng)
#:kws (map force (attribute kws.Keyword)))))))]
(make-Fun
(list (-Arrow doms
(parse-values-type #'rng)
#:kws (map force (attribute kws.Keyword)))))))]
;; This case needs to be at the end because it uses cut points to give good error messages.
[(~or (:->^ ~! dom:non-keyword-ty ... rng:expr
:colon^ (~var latent (full-latent (syntax->list #'(dom ...)))))
@ -1112,7 +1108,7 @@
;; module since it's duplicated elsewhere
(define (function-type? type)
(match (resolve type)
[(? Function?) #t]
[(? Fun?) #t]
[(Poly: _ body) (function-type? body)]
[(PolyDots: _ body) (function-type? body)]
[(PolyRow: _ _ body) (function-type? body)]
@ -1143,7 +1139,7 @@
(ret (parse-types #'(t ...))
empties
empties)]
[:AnyValues^ (tc-any-results #f)]
[:AnyValues^ (-tc-any-results #f)]
[t (ret (parse-type #'t) #f #f)]))
(define parse-type/id (parse/id parse-type))

65
typed-racket-lib/typed-racket/private/type-annotation.rkt
View File

@ -73,36 +73,49 @@
;; tc-expr : a function like `tc-expr' from tc-expr-unit
;; tc-expr/check : a function like `tc-expr/check' from tc-expr-unit
(define/cond-contract (get-type/infer stxs expr tc-expr tc-expr/check)
((listof identifier?) syntax? (syntax? . -> . tc-results/c) (syntax? tc-results/c . -> . tc-results/c)
. -> . (listof tc-result?))
((listof identifier?)
syntax?
(syntax? . -> . tc-results/c)
(syntax? tc-results/c . -> . tc-results/c)
. -> .
(listof tc-result?))
(match stxs
[(list stx ...)
(let ([anns (for/list ([s (in-list stxs)]) (type-annotation s #:infer #t))])
(let ([anns (for/list ([s (in-list stxs)])
(type-annotation s #:infer #t))])
(if (for/and ([a (in-list anns)]) a)
(match (tc-expr/check expr (ret anns))
[(tc-results: tys fs os)
(map tc-result tys fs os)])
(let ([res (tc-expr expr)])
(match res
[(tc-any-results: _)
(tc-error/expr
#:return (map (lambda _ (tc-result (Un))) stxs)
"Expression should produce ~a values, but produces an unknown number of values"
(length stxs))]
[(tc-results: (list (== -Bottom)) _ _)
(for/list ([_ (in-range (length stxs))])
(tc-result -Bottom))]
[(tc-results: tys fs os)
(if (not (= (length stxs) (length tys)))
(tc-error/expr #:return (map (lambda _ (tc-result (Un))) stxs)
"Expression should produce ~a values, but produces ~a values of types ~a"
(length stxs) (length tys) (stringify tys))
(for/list ([stx (in-list stxs)] [ty (in-list tys)]
[a (in-list anns)] [f (in-list fs)] [o (in-list os)])
(cond [a (check-type stx ty a) (tc-result a f o)]
;; mutated variables get generalized, so that we don't infer too small a type
[(is-var-mutated? stx) (tc-result (generalize ty) f o)]
[else (tc-result ty f o)])))]))))]))
[(tc-results: tcrs _) tcrs])
(match (tc-expr expr)
[(tc-any-results: _)
(tc-error/expr
#:return (map (λ _ (-tc-result -Bottom)) stxs)
"Expression should produce ~a values, but produces an unknown number of values"
(length stxs))]
[(tc-result1: (== -Bottom))
(for/list ([_ (in-range (length stxs))])
(-tc-result -Bottom))]
[(tc-results: tcrs _)
(cond
[(not (= (length stxs) (length tcrs)))
(tc-error/expr #:return (map (λ _ (-tc-result -Bottom)) stxs)
"Expression should produce ~a values, but produces ~a values of types ~a"
(length stxs)
(length tcrs)
(stringify (map tc-result-t tcrs)))]
[else
(for/list ([stx (in-list stxs)]
[tcr (in-list tcrs)]
[a (in-list anns)])
(match tcr
[(tc-result: ty ps o)
(cond [a (check-type stx ty a)
(-tc-result a ps o)]
;; mutated variables get generalized, so that we don't
;; infer too small a type
[(is-var-mutated? stx)
(-tc-result (generalize ty) ps o)]
[else (-tc-result ty ps o)])]))])])))]))
;; check that e-type is compatible with ty in context of stx
;; otherwise, error

92
typed-racket-lib/typed-racket/private/type-contract.rkt
View File

@ -504,7 +504,7 @@
chaperones
(if prop (list prop) '())
impersonators))])]
[(and t (Function: arrs))
[(and t (Fun: arrs))
#:when (any->bool? arrs)
;; Avoid putting (-> any T) contracts on struct predicates (where Boolean <: T)
;; Optimization: if the value is typed, we can assume it's not wrapped
@ -515,7 +515,7 @@
unsafe-spp/sc
safe-spp/sc)])
(or/sc optimized/sc (t->sc/fun t)))]
[(and t (Function: _)) (t->sc/fun t)]
[(and t (? Fun?)) (t->sc/fun t)]
[(Set: t) (set/sc (t->sc t))]
[(Sequence: ts) (apply sequence/sc (map t->sc ts))]
[(Vector: t) (vectorof/sc (t->sc/both t))]
@ -531,7 +531,7 @@
[(Continuation-Mark-Keyof: t)
(continuation-mark-key/sc (t->sc t))]
;; TODO: this is not quite right for case->
[(Prompt-Tagof: s (Function: (list (arr: (list ts ...) _ _ _ _))))
[(Prompt-Tagof: s (Fun: (list (Arrow: ts _ _ _))))
(prompt-tag/sc (map t->sc ts) (t->sc s))]
;; TODO
[(F: v)
@ -740,33 +740,34 @@
;; handle-range : Arr (-> Static-Contact) -> Static-Contract
;; Match the range of an arr and determine if a contract can be generated
;; and call the given thunk or raise an error
(define (handle-range arr convert-arr)
(match arr
(define (handle-range arrow convert-arrow)
(match arrow
;; functions with no props or objects
[(arr: dom (Values: (list (Result: rngs
(PropSet: (TrueProp:)
(TrueProp:))
(Empty:)) ...))
rst drst kws)
(convert-arr)]
[(Arrow: _ _ _
(Values: (list (Result: _
(PropSet: (TrueProp:)
(TrueProp:))
(Empty:)) ...)))
(convert-arrow)]
;; Functions that don't return
[(arr: dom (Values: (list (Result: (== -Bottom) _ _) ...)) rst drst kws)
(convert-arr)]
[(Arrow: _ _ _
(Values: (list (Result: (== -Bottom) _ _) ...)))
(convert-arrow)]
;; functions with props or objects
[(arr: dom (Values: (list (Result: rngs _ _) ...)) rst drst kws)
[(Arrow: _ _ _ (Values: (list (Result: rngs _ _) ...)))
(if (from-untyped? typed-side)
(fail #:reason (~a "cannot generate contract for function type"
" with props or objects."))
(convert-arr))]
[(arr: dom (? ValuesDots?) rst drst kws)
(convert-arrow))]
[(Arrow: _ _ _ (? ValuesDots?))
(fail #:reason (~a "cannot generate contract for function type"
" with dotted return values"))]
[(arr: dom (? AnyValues?) rst drst kws)
[(Arrow: _ _ _ (? AnyValues?))
(fail #:reason (~a "cannot generate contract for function type"
" with unknown return values"))]))
(match f
[(Function: arrs)
[(Fun: arrows)
;; Try to generate a single `->*' contract if possible.
;; This allows contracts to be generated for functions with both optional and keyword args.
;; (and don't otherwise require full `case->')
@ -781,15 +782,15 @@
;; since this code would generate contracts that accept any number of arguments between
;; 2 and 6, which is wrong.
;; TODO sufficient condition, but may not be necessary
[(has-optional-args? arrs)
(define first-arr (first arrs))
(define last-arr (last arrs))
(define (convert-arr)
(match-define (arr: first-dom (Values: (list (Result: rngs _ _) ...))
rst _ kws)
first-arr)
[(has-optional-args? arrows)
(define first-arrow (first arrows))
(define last-arrow (last arrows))
(define (convert-arrow)
(match-define (Arrow: first-dom rst kws
(Values: (list (Result: rngs _ _) ...)))
first-arrow)
;; all but dom is the same for all arrs
(match-define (arr: last-dom _ _ _ _) last-arr)
(define last-dom (Arrow-dom last-arrow))
(define mand-args (map t->sc/neg first-dom))
(define opt-args (map t->sc/neg (drop last-dom (length first-dom))))
(define-values (mand-kws opt-kws)
@ -799,12 +800,12 @@
(define range (map t->sc rngs))
(define rest (and rst (listof/sc (t->sc/neg rst))))
(function/sc (from-typed? typed-side) (process-dom mand-args) opt-args mand-kws opt-kws rest range))
(handle-range first-arr convert-arr)]
(handle-range first-arrow convert-arrow)]
[else
(define ((f case->) a)
(define (convert-arr arr)
(match arr
[(arr: dom (Values: (list (Result: rngs _ _) ...)) rst drst kws)
[(Arrow: dom rst kws (Values: (list (Result: rngs _ _) ...)))
(let-values ([(mand-kws opt-kws) (partition-kws kws)])
;; Garr, I hate case->!
(when (and (not (empty? kws)) case->)
@ -820,23 +821,24 @@
null
(map conv mand-kws)
(map conv opt-kws)
(or
(and rst (listof/sc (t->sc/neg rst)))
(and drst (listof/sc (t->sc/neg (car drst)
#:recursive-values
(hash-set recursive-values (cdr drst) (same any/sc))))))
(match rst
[(? Type?) (listof/sc (t->sc/neg rst))]
[(RestDots: dty dbound)
(listof/sc
(t->sc/neg dty
#:recursive-values
(hash-set recursive-values dbound (same any/sc))))]
[_ #f])
(map t->sc rngs))))]))
(handle-range a (λ () (convert-arr a))))
(define arities
(for/list ([t arrs])
(match t
[(arr: dom _ _ _ _) (length dom)])))
(for/list ([t (in-list arrows)]) (length (Arrow-dom t))))
(define maybe-dup (check-duplicates arities))
(when maybe-dup
(fail #:reason (~a "function type has two cases of arity " maybe-dup)))
(if (= (length arrs) 1)
((f #f) (first arrs))
(case->/sc (map (f #t) arrs)))])]))
(if (= (length arrows) 1)
((f #f) (first arrows))
(case->/sc (map (f #t) arrows)))])]))
;; Generate a contract for a object/class method clause
;; Precondition: type is a valid method type
@ -851,7 +853,7 @@
(t->sc/polydots type fail typed-side recursive-values rec)]
[(? PolyRow?)
(t->sc/polyrow type fail typed-side recursive-values rec)]
[(? Function?)
[(? Fun?)
(t->sc/function type fail typed-side recursive-values loop #t)]
[_ (fail #:reason "invalid method type")]))
@ -868,7 +870,7 @@
(define function-type?
(let loop ([ty b])
(match (resolve ty)
[(Function: _) #t]
[(? Fun?) #t]
[(Union: _ elems) (andmap loop elems)]
[(Intersection: elems _) (ormap loop elems)]
[(Poly: _ body) (loop body)]
@ -907,7 +909,7 @@
(define function-type?
(let loop ([ty b])
(match (resolve ty)
[(Function: _) #t]
[(? Fun?) #t]
[(Union: _ elems) (andmap loop elems)]
[(Intersection: elems _) (ormap loop elems)]
[(Poly: _ body) (loop body)]
@ -939,9 +941,9 @@
;; True if the arities `arrs` are what we'd expect from a struct predicate
(define (any->bool? arrs)
(match arrs
[(list (arr: (list (Univ:))
(Values: (list (Result: t _ _)))
#f #f '()))
[(list (Arrow: (list (Univ:))
#f '()
(Values: (list (Result: t _ _)))))
(t:subtype -Boolean t)]
[_ #f]))

63
typed-racket-lib/typed-racket/rep/object-rep.rkt
View File

@ -29,6 +29,8 @@
LExp-terms
LExp:
genobj
make-id-seq
id-seq-next
make-obj-seq
obj-seq-next
scale-obj
@ -66,9 +68,10 @@
[#:frees (f) (combine-frees (map f elems))]
[#:fmap (f) (make-Path (map f elems) name)]
[#:for-each (f) (for-each f elems)]
[#:custom-constructor
(cond
[(identifier? name)
[#:custom-constructor/contract
(-> (listof PathElem?) (or/c name-ref/c OptObject?) OptObject?)
(match name
[(? identifier?)
;; we don't want objects for visibly mutated or top level variables
(if (or (is-var-mutated? name)
(and (not (identifier-binding name))
@ -78,20 +81,58 @@
(intern-double-ref!
Path-intern-table
name elems #:construct (make-Path elems name))))]
[else (intern-double-ref!
Path-intern-table
name elems #:construct (make-Path elems name))])])
[(? pair?)
(intern-double-ref!
Path-intern-table
name elems #:construct (make-Path elems name))]
[(Path: elems* name*)
(let ([elems* (append elems elems*)])
(intern-double-ref!
Path-intern-table
name* elems* #:construct (make-Path elems* name*)))]
[(? LExp? l) (if (null? elems) l -empty-obj)]
[(Empty:) -empty-obj])])
(define Path-intern-table (make-weak-hash))
(define (-id-path name) (make-Path null name))
;; creates an "id sequence" -- use 'id-seq-next'
;; to iterate through the sequence.
;; For an example use case, see subtype.rkt,
;; which uses a seq to reuse fresh ids for subtype
;; checking for dependent arrows
(define (make-id-seq)
(for/fold ([seq (cons (genid) (box #f))])
([_ (in-range 9)])
(cons (genid) seq)))
;; id-seq-next
;;
;; returns 2 values
;; val 1 - the next id
;; val 2 - the rest of the sequence
(define (id-seq-next s)
(match s
[(cons val vals)
(values val vals)]
[(box (cons val vals))
(values val vals)]
[(box #f)
(define more (make-id-seq))
(if (box-cas! s #f more)
(id-seq-next more)
(id-seq-next s))]))
;; generates a fresh id object
;; NOTE: use this wisely -- calling this function
;; all the time will consume memory leading to GC
;; time that may add up during typechecking
(define (genobj) (-id-path (genid)))
;; creates an "object sequence" -- use 'obj-seq-next'
;; to iterate through the sequence.
;; For an example use case, see subtype.rkt,
@ -161,11 +202,11 @@
;; make-LExp* (provided as make-LExp)
;;
; IF the lexp (exp) contains only 1 variable,
;; IF the lexp (exp) contains only 1 variable,
;; and that variables its coefficient is 1,
; and the constant is 0
; THEN that lone variable is returned
; ELSE it returns the LExp
;; and the constant is 0
;; THEN that lone variable is returned
;; ELSE it returns the LExp
;; NOTE 1: We do this so there is a 'canonical form'
;; for linear expressions which are actually just
;; the underlying object, e.g. insteaf of
@ -326,4 +367,4 @@
(define (add-path-to-lexp p l)
(match l
[(LExp: const terms)
(make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))]))
(make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))]))

3
typed-racket-lib/typed-racket/rep/rep-utils.rkt
View File

@ -91,7 +91,6 @@
(hash-id name)
(rec name)))
;; This table maps a type to an identifier bound to the type.
;; This allows us to avoid reconstructing the type when using
;; it from its marshaled representation.
@ -379,7 +378,7 @@
(or (not (attribute frees-spec))
(not (attribute for-each-spec))
(not (attribute fold-spec))))
(raise-syntax-error 'def-rep "non-base reps require #:frees, #:for-each, and #:fold"
(raise-syntax-error 'def-rep "non-base reps require #:frees, #:for-each, and #:fmap"
#'var))
;; - - - - - - - - - - - - - - -

596
typed-racket-lib/typed-racket/rep/type-rep.rkt
View File

@ -54,17 +54,18 @@
Union-all-flat:
Union/set:
Intersection?
subst-names
inc-lvl
abstract-names
-refine
Refine:
Refine-obj:
Refine-name:
save-term-var-names!
extract-props
(rename-out [instantiate instantiate-raw-type]
[Union:* Union:]
instantiate-type
abstract-type
instantiate-obj
abstract-obj
substitute-names
(rename-out [Union:* Union:]
[Intersection:* Intersection:]
[make-Intersection* make-Intersection]
[Class:* Class:]
@ -114,6 +115,11 @@
;; as it is both Top and Bottom.
(def-type Error () [#:singleton Err])
;;************************************************************
;; Type Variables/Applications
;;************************************************************
;; de Bruijn indexes - should never appear outside of this file
;; bound type variables
;; i is an nat
@ -394,9 +400,9 @@
(def-structural Continuation-Mark-Keyof ([value #:invariant])
[#:mask mask:continuation-mark-key])
;; * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
;;************************************************************
;; List/Vector Types (that are not simple structural types)
;; * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
;;************************************************************
;; dotted list -- after expansion, becomes normal Pair-based list type
(def-type ListDots ([dty Type?] [dbound (or/c symbol? natural-number/c)])
@ -422,9 +428,10 @@
[#:mask mask:vector])
;; * * * * * * *
;; Type Binders
;; * * * * * * *
;;************************************************************
;; Type Binders (Polys, Mus, etc)
;;************************************************************
(def-type Mu ([body Type?])
@ -479,73 +486,83 @@
;; kw : keyword?
;; ty : Type
;; required? : Boolean
;;************************************************************
;; Functions, Arrows
;;************************************************************
;; keyword arguments
(def-rep Keyword ([kw keyword?] [ty Type?] [required? boolean?])
[#:frees (f) (f ty)]
[#:fmap (f) (make-Keyword kw (f ty) required?)]
[#:for-each (f) (f ty)])
(define/provide (Keyword<? kw1 kw2)
(keyword<? (Keyword-kw kw1)
(Keyword-kw kw2)))
(define (keyword-sorted/c kws)
(or (empty? kws)
;; contract for a sorted keyword list
(define-for-cond-contract (keyword-sorted/c kws)
(or (null? kws)
(= (length kws) 1)
(apply keyword<? (map Keyword-kw kws))))
(equal? kws (sort kws Keyword<?))))
(def-rep arr ([dom (listof Type?)]
[rng SomeValues?]
[rest (or/c #f Type?)]
[drest (or/c #f (cons/c Type? (or/c natural-number/c symbol?)))]
[kws (and/c (listof Keyword?) keyword-sorted/c)])
(def-rep RestDots ([ty Type?]
[nm (or/c natural-number/c symbol?)])
[#:frees
[#:vars (f)
(combine-frees
(append (map (compose flip-variances f)
(append (if rest (list rest) null)
(map Keyword-ty kws)
dom))
(match drest
[(cons t (? symbol? bnd))
(list (free-vars-remove (flip-variances (f t)) bnd))]
[(cons t _)
(list (flip-variances (f t)))]
[_ null])
(list (f rng))))]
(cond
[(symbol? nm) (free-vars-remove (f ty) nm)]
[else (f ty)])]
[#:idxs (f)
(combine-frees
(append (map (compose flip-variances f)
(append (if rest (list rest) null)
(map Keyword-ty kws)
dom))
(match drest
[(cons t (? symbol? bnd))
(list (single-free-var bnd variance:contra)
(flip-variances (f t)))]
[(cons t _)
(list (flip-variances (f t)))]
[_ null])
(list (f rng))))]]
[#:fmap (f) (make-arr (map f dom)
(f rng)
(and rest (f rest))
(and drest (cons (f (car drest)) (cdr drest)))
(map f kws))]
(cond
[(symbol? nm) (combine-frees (list (f ty) (single-free-var nm)))]
[else (f ty)])]]
[#:fmap (f) (make-RestDots (f ty) nm)]
[#:for-each (f) (f ty)])
(def-rep Arrow ([dom (listof Type?)]
[rst (or/c #f Type? RestDots?)]
[kws (and/c (listof Keyword?) keyword-sorted/c)]
[rng SomeValues?])
[#:frees (f)
(combine-frees
(list* (f rng)
(if rst
(flip-variances (f rst))
empty-free-vars)
(append
(for/list ([kw (in-list kws)])
(flip-variances (f kw)))
(for/list ([d (in-list dom)])
(flip-variances (f d))))))]
[#:fmap (f) (make-Arrow (map f dom)
(and rst (f rst))
(map f kws)
(f rng))]
[#:for-each (f)
(for-each f dom)
(f rng)
(when drest (f (car drest)))
(when rest (f rest))
(for-each f kws)])
(when rst (f rst))
(for-each f kws)
(f rng)])
;; arities : Listof[arr]
(def-type Function ([arities (listof arr?)])
;; a standard function
;; + all functions are case-> under the hood (i.e. see 'arrows')
;; + each Arrow in 'arrows' may have a dependent range
(def-type Fun ([arrows (listof Arrow?)])
[#:mask mask:procedure]
[#:frees (f) (combine-frees (map f arities))]
[#:fmap (f) (make-Function (map f arities))]
[#:for-each (f) (for-each f arities)])
[#:frees (f) (combine-frees (map f arrows))]
[#:fmap (f) (make-Fun (map f arrows))]
[#:for-each (f) (for-each f arrows)])
;;************************************************************
;; Structs
;;************************************************************
(def-rep fld ([t Type?] [acc identifier?] [mutable? boolean?])
@ -560,7 +577,7 @@
(def-type Struct ([name identifier?]
[parent (or/c #f Struct?)]
[flds (listof fld?)]
[proc (or/c #f Function?)]
[proc (or/c #f Fun?)]
[poly? boolean?]
[pred-id identifier?])
[#:frees (f) (combine-frees (map f (append (if proc (list proc) null)
@ -611,6 +628,9 @@
[#:mask (mask-union mask:struct mask:procedure)])
;;************************************************************
;; Singleton Values (see also Base)
;;************************************************************
;; v : Racket Value
@ -634,6 +654,12 @@
[1 -One]
[_ (make-Value val)])])
;;************************************************************
;; Unions
;;************************************************************
;; mask - cached type mask
;; base - any Base types, or Bottom if none are present
;; ts - the list of types in the union (contains no duplicates,
@ -785,6 +811,10 @@
(define (Un . args)
(Union-fmap (λ (x) x) -Bottom args))
;;************************************************************
;; Intersection/Refinement
;;************************************************************
;; Intersection
;; ts - the list of types (gives deterministic behavior)
@ -877,7 +907,7 @@
[((Intersection: ts prop* tset) _)
(-refine (make-Intersection ts -tt tset) (-and prop prop*))]
[(_ _) (make-Intersection (list t) prop (hash t #t))])]
[(nm t prop) (-refine t (abstract-names prop (list nm)))]))
[(nm t prop) (-refine t (abstract-obj prop nm))]))
(define-match-expander Intersection:*
(λ (stx) (syntax-case stx ()
@ -926,6 +956,43 @@
(app Intersection-w/o-prop t)
(app (λ (i) (Intersection-prop* obj i)) prop)))])))
(define (Intersection-prop* obj t)
(define p (Intersection-prop t))
(and p (instantiate-obj p obj)))
;; given the fact that 'obj' is of type 'type',
;; look inside of type trying to learn
;; more info about obj
(define (extract-props obj type)
(cond
[(Empty? obj) '()]
[else
(define props '())
(let extract! ([rep type]
[obj obj])
(match rep
[(== -Zero)
#:when (with-linear-integer-arithmetic?)
(set! props (cons (-eq obj (-lexp 0)) props))]
[(== -One)
#:when (with-linear-integer-arithmetic?)
(set! props (cons (-eq obj (-lexp 1)) props))]
[(Pair: t1 t2) (extract! t1 (-car-of obj))
(extract! t2 (-cdr-of obj))]
[(Refine-obj: obj t prop)
(set! props (cons prop props))
(extract! t obj)]
[(HeterogeneousVector: ts)
#:when (with-linear-integer-arithmetic?)
(set! props (cons (-eq (-vec-len-of obj) (-lexp (length ts)))
props))]
[(Intersection: ts _ _) (for ([t (in-list ts)])
(extract! t obj))]
[_ (void)]))
props]))
;; refinement based on some predicate function 'pred'
(def-type Refinement ([parent Type?] [pred identifier?])
[#:frees (f) (f parent)]
@ -934,6 +1001,13 @@
[#:mask (λ (t) (mask (Refinement-parent t)))]
[#:custom-constructor (make-Refinement parent (normalize-id pred))])
;;************************************************************
;; Object Oriented
;;************************************************************
;; A Row used in type instantiation
;; For now, this should not appear in user code. It's used
;; internally to perform row instantiations and to represent
@ -1008,6 +1082,11 @@
[#:for-each (f) (f cls)]
[#:mask mask:instance])
;;************************************************************
;; Units
;;************************************************************
;; interp:
;; name is the id of the signature
;; extends is the extended signature or #f
@ -1084,19 +1163,13 @@
;;************************************************************
;; Locally Nameles Type Variable Abstraction/Instantiation
;; Type Variable tools (i.e. Abstraction/Instantiation)
;; Note: see the 'Locally Nameless' binder
;; representation strategy for general
;; details on the approach we're using
;;************************************************************
;; abstract
;;
;; abstracts type variable 'name'
;; to De Bruijn index 0 in 'initial'
(define/cond-contract (abstract name initial)
(-> symbol? Rep? Rep?)
(abstract-many (list name) initial))
;; abstract-many
;; abstract-many/type
;;
;; abstracts the type variable names from 'names-to-abstract'
;; to de bruijn indices in 'initial'.
@ -1105,97 +1178,93 @@
;; names-to-abstract[1] gets mapped to n-2
;; ...
;; names-to-abstract[n-1] gets mapped to 0
(define/cond-contract (abstract-many names-to-abstract initial)
(-> (listof symbol?) Rep? Rep?)
(define n-1 (sub1 (length names-to-abstract)))
(define (abstract-name name lvl default dotted?)
(match (index-of names-to-abstract name eq?)
[#f default]
;; adjust index properly before using (see comments above
;; and note we are under 'lvl' additional binders)
[idx (let ([idx (+ lvl (- n-1 idx))])
(cond [dotted? idx]
[else (make-B idx)]))]))
(let rec/lvl ([cur initial] [lvl 0])
(define (rec rep) (rec/lvl rep lvl))
(match cur
;; Free type variables
[(F: name) (abstract-name name lvl cur #f)]
;; forms w/ (potential) dotted type variables
[(arr: dom rng rest drest kws)
(make-arr (map rec dom)
(rec rng)
(and rest (rec rest))
(match drest
[(cons d-ty d)
(cons (rec d-ty) (abstract-name d lvl d #t))]
[_ #f])
(map rec kws))]
[(ValuesDots: rs dty d)
(make-ValuesDots (map rec rs)
(rec dty)
(abstract-name d lvl d #t))]
[(ListDots: dty d)
(make-ListDots (rec dty)
(abstract-name d lvl d #t))]
;; forms which introduce bindings (increment lvls appropriately)
[(Mu: body) (make-Mu (rec/lvl body (add1 lvl)))]
[(PolyRow: constraints body)
(make-PolyRow constraints (rec/lvl body (add1 lvl)))]
[(PolyDots: n body)
(make-PolyDots n (rec/lvl body (+ n lvl)))]
[(Poly: n body)
(make-Poly n (rec/lvl body (+ n lvl)))]
[_ (Rep-fmap cur rec)])))
(define/cond-contract (abstract-type initial names-to-abstract)
(-> Rep? (or/c symbol? (listof symbol?)) Rep?)
(cond
[(null? names-to-abstract) initial]
[(not (pair? names-to-abstract))
(abstract-type initial (list names-to-abstract))]
[else
(define n-1 (sub1 (length names-to-abstract)))
(define (abstract-name name lvl default dotted?)
(cond
[(symbol? name)
(match (index-of names-to-abstract name eq?)
[#f default]
;; adjust index properly before using (see comments above
;; and note we are under 'lvl' additional binders)
[idx (let ([idx (+ lvl (- n-1 idx))])
(cond [dotted? idx]
[else (make-B idx)]))])]
[else default]))
(type-var-transform initial abstract-name)]))
;; instantiate
;; instantiate-type
;;
;; instantiates De Bruijn index 0 with
;; 'type' in 'initial'
(define/cond-contract (instantiate type initial)
(-> Type? Rep? Rep?)
(instantiate-many (list type) initial))
;; instantiate-many
;;
;; instantiates De Bruijn indices 0 through
;; (sub1 (length images)) with the types from images.
;; instantiates type De Bruijn indices 0 (i.e. (B 0))
;; through (sub1 (length images)) with images.
;; (i.e. De Bruin i = (B i))
;; Specifically, if n = (length images), then
;; index 0 gets mapped to images[n-1]
;; index 1 gets mapped to images[n-2]
;; ...
;; index n-1 gets mapped to images[0]
(define/cond-contract (instantiate-many images initial)
(-> (listof Type?) Rep? Rep?)
(define n-1 (sub1 (length images)))
(define (instantiate-idx idx lvl default dotted?)
;; adjust for being under 'lvl' binders and for
;; index 0 gets mapped to images[n-1], etc
(let ([idx (- n-1 (- idx lvl))])
(match (list-ref/default images idx #f)
[#f default]
[image (cond [dotted? (F-n image)]
[else image])])))
(define/cond-contract (instantiate-type initial images)
(-> Rep? (or/c Type? (listof Type?)) Rep?)
(cond
[(null? images) initial]
[(not (pair? images)) (instantiate-type initial (list images))]
[else
(define n-1 (sub1 (length images)))
(define (instantiate-idx idx lvl default dotted?)
(cond
[(exact-nonnegative-integer? idx)
;; adjust for being under 'depth' binders and for
;; index 0 gets mapped to images[n-1], etc
(let ([idx (- n-1 (- idx lvl))])
(match (list-ref/default images idx #f)
[#f default]
[image (cond [dotted? (F-n image)]
[else image])]))]
[else default]))
(type-var-transform initial instantiate-idx)]))
;; type-var-transform
;;
;; Helper function for instantiate[-many]/type
;; and abstract[-many]/type.
;;
;; transform : [target : (or nat sym)]
;; [lvl : nat]
;; [default : (or Type nat sym)]
;; [dotted? : boolean]
;; ->
;; (or Type nat sym)
;; where 'target' is the thing potentially being replaced
;; 'depth' is how many binders we're under
;; 'default' is what it uses if we're not replacing 'target'
;; 'dotted?' is a flag denoting if this is a dotted var/idx
(define (type-var-transform initial transform)
(let rec/lvl ([cur initial] [lvl 0])
(define (rec rep) (rec/lvl rep lvl))
(match cur
;; Bound De Bruijn indices
[(B: idx) (instantiate-idx idx lvl cur #f)]
;; forms w/ (potential) dotted type indices
[(arr: dom rng rest (cons d-ty (? exact-integer? d)) kws)
(make-arr (map rec dom)
(rec rng)
(and rest (rec rest))
(cons (rec d-ty) (instantiate-idx d lvl d #t))
(map rec kws))]
[(ValuesDots: rs dty (? exact-integer? d))
;; De Bruijn indices
[(B: idx) (transform idx lvl cur #f)]
;; Type variables
[(F: var) (transform var lvl cur #f)]
;; forms w/ dotted type vars/indices
[(RestDots: ty d)
(make-RestDots (rec ty) (transform d lvl d #t))]
[(ValuesDots: rs dty d)
(make-ValuesDots (map rec rs)
(rec dty)
(instantiate-idx d lvl d #t))]
[(ListDots: dty (? exact-integer? d))
(transform d lvl d #t))]
[(ListDots: dty d)
(make-ListDots (rec dty)
(instantiate-idx d lvl d #t))]
(transform d lvl d #t))]
;; forms which introduce bindings (increment lvls appropriately)
[(Mu: body) (make-Mu (rec/lvl body (add1 lvl)))]
[(PolyRow: constraints body)
@ -1207,6 +1276,106 @@
[_ (Rep-fmap cur rec)])))
;;***************************************************************
;; Dependent Function/Refinement tools
;; Note: see the 'Locally Nameless' binder
;; representation strategy for general
;; details on the approach we're using
;;***************************************************************
;; instantiates term De Bruijn indices
;; '(0 . 0) ... '(0 . (sub1 (length os)))
;; in 'initial with objects from 'os'
(define/cond-contract (instantiate-obj initial os)
(-> Rep? (or/c identifier?
OptObject?
(listof (or/c identifier? OptObject?)))
Rep?)
(cond
[(null? os) initial]
[(not (pair? os)) (instantiate-obj initial (list os))]
[else
(define (instantiate-idx name cur-lvl)
(match name
[(cons lvl idx)
#:when (eqv? lvl cur-lvl)
(list-ref os idx)]
[_ name]))
(term-var-transform initial instantiate-idx)]))
;; abstracts the n identifiers from 'ids-to-abstract'
;; in 'initial', replacing them with term De Bruijn indices
;; '(0 . 0) ... '(0 . n-1) (or their appropriate
;; successors under additional binders)
(define/cond-contract (abstract-obj initial ids-to-abstract)
(-> Rep? (or/c identifier? (listof identifier?)) Rep?)
(cond
[(null? ids-to-abstract) initial]
[(not (pair? ids-to-abstract))
(abstract-obj initial (list ids-to-abstract))]
[else
(define (abstract-id id lvl)
(cond
[(identifier? id)
(match (index-of ids-to-abstract id free-identifier=?)
[#f id]
;; adjust index properly before using (see comments above
;; and note we are under 'lvl' additional binders)
[idx (cons lvl idx)])]
[else id]))
(term-var-transform initial abstract-id)]))
;; term-binder-transform
;;
;; Helper function for abstract[-many]/obj
;; and instantiate[-many]/obj.
;;
;; transform : [target : (or nat sym)]
;; [depth : nat]
;; ->
;; (or nat sym)
;; where 'target' is the thing potentially being replaced
;; 'depth' is how many binders we're under
(define (term-var-transform initial transform)
(let rec/lvl ([rep initial] [lvl 0])
(define (rec rep) (rec/lvl rep lvl))
(define (rec/inc rep) (rec/lvl rep (add1 lvl)))
(match rep
;; Functions
;; increment the level of the substituted object
[(Arrow: dom rst kws rng)
(make-Arrow (map rec dom)
(and rst (rec/inc rst))
(map rec kws)
(rec/inc rng))]
;; Refinement types e.g. {x ∈ τ | ψ(x)}
;; increment the level of the substituted object
[(Intersection: ts p _) (-refine
(apply -unsafe-intersect (map rec ts))
(rec/inc p))]
[(Path: flds nm)
(make-Path (map rec flds)
(transform nm lvl))]
[_ (Rep-fmap rep rec)])))
;; simple substitution mapping identifiers to
;; identifiers (or objects)
;; pre: (= (length names) (length names-or-objs))
(define (substitute-names rep names names-or-objs)
(let subst ([rep rep])
(match rep
[(Path: flds (? identifier? name))
(make-Path (map subst flds)
(match (index-of names name free-identifier=?)
[#f name]
[idx (list-ref names-or-objs idx)]))]
[_ (Rep-fmap rep subst)])))
;;************************************************************
;; Smart Constructors/Destructors for Type Binders
;;
@ -1220,7 +1389,7 @@
;; the 'smart' constructor
(define (Mu* name body)
(let ([v (make-Mu (abstract name body))])
(let ([v (make-Mu (abstract-type body name))])
(hash-set! type-var-name-table v name)
v))
@ -1228,13 +1397,13 @@
(define (Mu-body* name t)
(match t
[(Mu: body)
(instantiate (make-F name) body)]))
(instantiate-type body (make-F name))]))
;; unfold : Mu -> Type
(define/cond-contract (unfold t)
(Mu? . -> . Type?)
(match t
[(Mu-unsafe: body) (instantiate t body)]
[(Mu-unsafe: body) (instantiate-type body t)]
[t (error 'unfold "not a mu! ~a" t)]))
@ -1250,7 +1419,7 @@
;;
(define (Poly* names body #:original-names [orig names])
(if (null? names) body
(let ([v (make-Poly (length names) (abstract-many names body))])
(let ([v (make-Poly (length names) (abstract-type body names))])
(hash-set! type-var-name-table v orig)
v)))
@ -1260,12 +1429,12 @@
[(Poly: n body)
(unless (= (length names) n)
(int-err "Wrong number of names: expected ~a got ~a" n (length names)))
(instantiate-many (map make-F names) body)]))
(instantiate-type body (map make-F names))]))
;; PolyDots 'smart' constructor
(define (PolyDots* names body)
(if (null? names) body
(let ([v (make-PolyDots (length names) (abstract-many names body))])
(let ([v (make-PolyDots (length names) (abstract-type body names))])
(hash-set! type-var-name-table v names)
v)))
@ -1275,7 +1444,7 @@
[(PolyDots: n body)
(unless (= (length names) n)
(int-err "Wrong number of names: expected ~a got ~a" n (length names)))
(instantiate-many (map make-F names) body)]))
(instantiate-type body (map make-F names))]))
;; PolyRow 'smart' constructor
@ -1285,7 +1454,7 @@
;; a time. This may change in the future.
;;
(define (PolyRow* names constraints body #:original-names [orig names])
(let ([v (make-PolyRow constraints (abstract-many names body))])
(let ([v (make-PolyRow constraints (abstract-type body names))])
(hash-set! type-var-name-table v orig)
v))
@ -1293,7 +1462,7 @@
(define (PolyRow-body* names t)
(match t
[(PolyRow: constraints body)
(instantiate-many (map make-F names) body)]))
(instantiate-type body (map make-F names))]))
;;***************************************************************
@ -1549,110 +1718,3 @@
(syntax-parse stx
[(_) #'(Name: _ _ #t)]
[(_ name-pat) #'(Name: name-pat _ #t)])))
;;***************************************************************
;; Intersection/Refinement related tools
;;***************************************************************
;; inc-lvl
;; (cons nat nat) -> (cons nat nat)
;; DeBruijn indexes are represented as a pair of naturals.
;; This function increments the 'lvl' field of such an index.
(define (inc-lvl x)
(match x
[(cons lvl arg) (cons (add1 lvl) arg)]
[_ x]))
;; inc-lvls
;; This function increments the 'lvl' field in all of the targets
;; and objects of substitution (see 'inc-lvl' above)
;; (side note: there is a similar but _different_ version
;; of this function in tc-subst.rkt)
(define (inc-lvls targets)
(for/list ([tgt (in-list targets)])
(match tgt
[(cons nm1 (Path: flds nm2))
(cons (inc-lvl nm1) (make-Path flds (inc-lvl nm2)))]
[(cons nm1 rst)
(cons (inc-lvl nm1) rst)])))
;; name substitution -- like subst-rep in
;; tc-subst but much simpler
(define/cond-contract (subst-names rep targets)
(-> Rep? (listof (cons/c name-ref/c OptObject?)) Rep?)
(define (rec/inc-lvl rep)
(subst-names rep (inc-lvls targets)))
(let rec ([rep rep])
(match rep
;; Functions
;; increment the level of the substituted object
[(arr: dom rng rest drest kws)
(make-arr (map rec dom)
(rec/inc-lvl rng)
(and rest (rec rest))
(and drest (cons (rec (car drest)) (cdr drest)))
(map rec kws))]
;; Refinement types e.g. {x ∈ τ | ψ(x)}
;; increment the level of the substituted object
[(Intersection: ts p _) (-refine
(for/fold ([res Univ])
([t (in-list ts)])
(intersect res (rec t)))
(rec/inc-lvl p))]
[(Path: flds nm)
(let ([flds (map rec flds)])
(cond
[(assoc nm targets name-ref=?)
=> (match-lambda
[(cons _ (Path: flds* nm*)) (make-Path (append flds flds*) nm*)]
[(cons _ (Empty:)) -empty-obj]
[(cons _ (? LExp? l)) #:when (null? flds) l]
[_ -empty-obj])]
[else (make-Path flds nm)]))]
[_ (Rep-fmap rep rec)])))
(define (abstract-names rep ids)
(define sub (for/list ([id (in-list ids)]
[idx (in-range (length ids))])
(cons id (-id-path (cons 0 idx)))))
(subst-names rep sub))
(define (Intersection-prop* obj t)
(define p (Intersection-prop t))
(and p (subst-names p (list (cons (cons 0 0) obj)))))
;; given the fact that 'obj' is of type 'type',
;; look inside of type trying to learn
;; more info about obj
(define (extract-props obj type)
(cond
[(Empty? obj) '()]
[else
(define props '())
(let extract! ([rep type]
[obj obj])
(match rep
[(== -Zero)
#:when (with-linear-integer-arithmetic?)
(set! props (cons (-eq obj (-lexp 0)) props))]
[(== -One)
#:when (with-linear-integer-arithmetic?)
(set! props (cons (-eq obj (-lexp 1)) props))]
[(Pair: t1 t2) (extract! t1 (-car-of obj))
(extract! t2 (-cdr-of obj))]
[(Refine-obj: obj t prop)
(set! props (cons prop props))
(extract! t obj)]
[(HeterogeneousVector: ts)
#:when (with-linear-integer-arithmetic?)
(set! props (cons (-eq (-vec-len-of obj) (-lexp (length ts)))
props))]
[(Intersection: ts _ _) (for ([t (in-list ts)])
(extract! t obj))]
[_ (void)]))
props]))

107
typed-racket-lib/typed-racket/typecheck/check-below.rkt
View File

@ -36,10 +36,11 @@
(define (value-string ty)
(match ty
[(tc-result1: _) "1 value"]
[(tc-results: ts) (~a (length ts) " values")]
[(tc-results: tcrs #f) (~a (length tcrs) " values")]
;; TODO simplify this case
[(tc-results: ts _ _ dty _) (~a (length ts) " " (if (= (length ts) 1) "value" "values")
" and `" dty " ...'")]
[(tc-results: tcrs (RestDots: dty _))
(~a (length tcrs) " " (if (= (length tcrs) 1) "value" "values")
" and `" dty " ...'")]
[(tc-any-results: _) "unknown number"]))
(type-mismatch
(value-string expected) (value-string actual)
@ -73,6 +74,13 @@
(define (prop-better? p1 p2)
(or (not p2)
(implies? p1 p2)))
(define (RestDots-better? rdots1 rdots2)
(match* (rdots1 rdots2)
[(rd rd) #t]
[((RestDots: dty1 dbound)
(RestDots: dty2 dbound))
(subtype dty1 dty2)]
[(_ _) #f]))
(match* (tr1 expected)
;; This case has to be first so that bottom (exceptions, etc.) can be allowed in cases
@ -84,15 +92,18 @@
[((tc-any-results: p1) (tc-any-results: p2))
(unless (prop-better? p1 p2)
(type-mismatch p2 p1 "mismatch in proposition"))
(tc-any-results (fix-props p2 p1))]
(-tc-any-results (fix-props p2 p1))]
[((or (tc-results: _ (list (PropSet: ps+ ps-) ...) _)
(tc-results: _ (list (PropSet: ps+ ps-) ...) _ _ _))
[((tc-results: tcrs _)
(tc-any-results: p2))
(define merged-prop (apply -and (map -or ps+ ps-)))
(define merged-prop
(apply -and
(map (match-lambda
[(tc-result: _ (PropSet: p+ p-) _) (-or p+ p-)])
tcrs)))
(unless (prop-better? merged-prop p2)
(type-mismatch p2 merged-prop "mismatch in proposition"))
(tc-any-results (fix-props p2 merged-prop))]
(-tc-any-results (fix-props p2 merged-prop))]
[((tc-result1: t1 p1 o1) (tc-result1: t2 p2 o2))
@ -113,66 +124,47 @@
(ret t2 (fix-props p2 p1) (fix-object o2 o1))]
;; case where expected is like (Values a ... a) but got something else
[((tc-results: t1 p1 o1) (tc-results: t2 p2 o2 dty dbound))
[((tc-results: _ #f) (tc-results: _ (? RestDots?)))
(value-mismatch expected tr1)
(fix-results expected)]
;; case where you have (Values a ... a) but expected something else
[((tc-results: t1 p1 o1 dty dbound) (tc-results: t2 p2 o2))
[((tc-results: _ (? RestDots?)) (tc-results: _ #f))
(value-mismatch expected tr1)
(fix-results expected)]
[((tc-results: t1 p1 o1 dty1 dbound)
(tc-results: t2 (list (or #f (PropSet: (TrueProp:) (TrueProp:))) ...)
(list (or #f (Empty:)) ...) dty2 dbound))
;; case where both have no '...', or both have '...'
;; NOTE: we ignore the propsets and objects... not sure
;; why---maybe there's an assumption that users
;; can't specify props/objects for multiple values?
;; seems like we should add some checks to this doesn't
;; turn into an error in the future that we can't fix w/o
;; breaking programs that relied on it being broken.
[((tc-results: tcrs1 db1)
(tc-results: tcrs2 db2))
(cond
[(= (length t1) (length t2))
(unless (andmap subtype t1 t2 o1)
(expected-but-got (stringify t2) (stringify t1)))
(unless (subtype dty1 dty2)
(type-mismatch dty2 dty1 "mismatch in ... argument"))]
[(= (length tcrs1) (length tcrs2))
(unless (andmap (match-lambda**
[((tc-result: t1 ps1 o1)
(tc-result: t2 ps2 o2))
(and (subtype t1 t2 o1)
(prop-set-better? ps1 ps2)
(object-better? o1 o2))])
tcrs1
tcrs2)
(expected-but-got (stringify (map tc-result-t tcrs1))
(stringify (map tc-result-t tcrs2))))
(match* (db1 db2)
[((RestDots: dty1 dbound1)
(RestDots: dty2 dbound2))
#:when (not (and (eq? dbound1 dbound2)
(subtype dty1 dty2)))
(type-mismatch dty2 dty1 "mismatch in ... argument")]
[(_ _) (void)])]
[else
(value-mismatch expected tr1)])
(fix-results expected)]
[((tc-results: t1 p1 o1 dty1 dbound) (tc-results: t2 p2 o2 dty2 dbound))
(cond
[(= (length t1) (length t2))
(unless (andmap subtype t1 t2 o1)
(expected-but-got (stringify t2) (stringify t1)))
(unless (subtype dty1 dty2)
(type-mismatch dty2 dty1 "mismatch in ... argument"))]
[else
(value-mismatch expected tr1)])
(fix-results expected)]
[((tc-results: t1 p1 o1)
(tc-results: t2 (list (or #f (PropSet: (TrueProp:) (TrueProp:))) ...)
(list (or #f (Empty:)) ...)))
(unless (= (length t1) (length t2))
(value-mismatch expected tr1))
(unless (for/and ([t (in-list t1)]
[s (in-list t2)]
[o (in-list o1)])
(subtype t s o))
(expected-but-got (stringify t2) (stringify t1)))
(fix-results expected)]
[((tc-results: t1 fs os) (tc-results: t2 fs os))
(unless (= (length t1) (length t2))
(value-mismatch expected tr1))
(unless (for/and ([t (in-list t1)]
[s (in-list t2)]
[o (in-list os)])
(subtype t s o))
(expected-but-got (stringify t2) (stringify t1)))
(fix-results expected)]
[((tc-results: t1 p1 o1) (tc-results: t2 p2 o2))
#:when (not (= (length t1) (length t2)))
(value-mismatch expected tr1)
(fix-results expected)]
[((tc-any-results: _) (? tc-results?))
(value-mismatch expected tr1)
(fix-results expected)]
@ -181,7 +173,6 @@
(unless (subtype t1 t2)
(expected-but-got t2 t1))
expected]
[((tc-results: ts fs os dty dbound) (tc-results: ts* fs* os* dty* dbound*))
(int-err "dotted types with different bounds/propositions/objects in check-below nyi: ~a ~a" tr1 expected)]
[(a b) (int-err "unexpected input for check-below: ~a ~a" a b)]))

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

@ -1116,9 +1116,7 @@
;; so that it has the right environment. An earlier approach did
;; check this only in the synthesis stage, but caused some regressions.
(define temp-names (syntax->list #'(names ...)))
(define init-types
(match (tc-expr #'val-expr)
[(tc-results: xs ) xs]))
(define init-types (tc-results-ts (tc-expr #'val-expr)))
(unless (= (length temp-names) (length init-types))
(tc-error/expr "wrong number of values: expected ~a but got ~a"
(length temp-names) (length init-types)))
@ -1136,8 +1134,7 @@
(define (setter->type id)
(define f-type (lookup-id-type/lexical id))
(match f-type
[(Function: (list (arr: (list _ type) _ _ _ _)))
type]
[(Fun: (list (Arrow: (list _ t) _ _ _))) t]
[#f (int-err "setter->type ~a" (syntax-e id))]))
;; check-init-arg : Id Type Syntax -> Void
@ -1152,8 +1149,7 @@
(define type
(tc-expr/check/t init-val (ret (->* null init-type))))
(match type
[(Function: (list (arr: _ (Values: (list (Result: result _ _)))
_ _ _)))
[(Fun: (list (Arrow: _ _ _ (Values: (list (Result: result _ _))))))
(check-below result init-type)]
[_ (int-err "unexpected init value ~a"
(syntax->datum init-val))])]
@ -1204,7 +1200,7 @@
(define init-types
;; this gets re-checked later, so don't throw any errors yet
(match (tc-expr/check? #'initial-values #f)
[(tc-results: xs ) xs]
[(? tc-results? tcrs) (tc-results-ts tcrs)]
;; We have to return something here so use the most conservative type
[#f (make-list (length field-names) Univ)]))
(for ([name (in-list field-names)]
@ -1586,12 +1582,13 @@
;; Fix up a method's arity from a regular function type
(define (function->method type self-type)
(match type
[(Function: (list arrs ...))
(define fixed-arrs
(for/list ([arr arrs])
(match-define (arr: doms rng rest drest kws) arr)
(make-arr (cons self-type doms) rng rest drest kws)))
(make-Function fixed-arrs)]
[(Fun: arrows)
(define fixed-arrows
(map (match-lambda
[(Arrow: dom rst kws rng)
(make-Arrow (cons self-type dom) rst kws rng)])
arrows))
(make-Fun fixed-arrows)]
[(Poly-names: ns body)
(make-Poly ns (function->method body self-type))]
[(PolyDots-names: ns body)
@ -1604,12 +1601,13 @@
;; Turn a "real" method type back into a function type
(define (method->function type)
(match type
[(Function: (list arrs ...))
(define fixed-arrs
(for/list ([arr arrs])
(match-define (arr: doms rng rest drest kws) arr)
(make-arr (cdr doms) rng rest drest kws)))
(make-Function fixed-arrs)]
[(Fun: arrows)
(define fixed-arrows
(map (match-lambda
[(Arrow: (cons _ dom) rst kws rng)
(make-Arrow dom rst kws rng)])
arrows))
(make-Fun fixed-arrows)]
[(Poly-names: ns body)
(make-Poly ns (method->function body))]
[(PolyDots-names: ns body)

20
typed-racket-lib/typed-racket/typecheck/check-subforms-unit.rkt
View File

@ -44,14 +44,24 @@
;; The result of applying the function to a single argument of the type of its first argument.
;; Is used when checking forms like with-handlers, for example.
(define (get-range-result stx t prop-type)
(let loop ((t t))
(let loop ([t t])
(match t
[(Function: (list _ ... (arr: (list arg1) _ _ #f (list (Keyword: _ _ #f) ...)) _ ...))
[(Fun: (list _ ...
(Arrow: (list arg1)
(not (? RestDots?))
(list (Keyword: _ _ #f) ...)
_ )
_ ...))
#:when (subtype prop-type arg1)
(tc/funapp #'here #'(here) t (list (ret arg1)) #f)]
[(Function: (list _ ... (arr: '() _ (? values rest) #f (list (Keyword: _ _ #f) ...)) _ ...))
#:when (subtype prop-type rest)
(tc/funapp #'here #'(here) t (list (ret rest)) #f)]
[(Fun: (list _ ...
(Arrow: (list)
(? Type? rst)
(list (Keyword: _ _ #f) ...)
_ )
_ ...))
#:when (subtype prop-type rst)
(tc/funapp #'here #'(here) t (list (ret rst)) #f)]
[(? resolvable? t)
(loop (resolve t))]
[(or (Poly: ns _) (PolyDots: (list ns ... _) _))

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

@ -735,7 +735,10 @@
check-exports-thunk))
(define invoke-type
(match res
[(tc-results: tps) (-values tps)]))
[(tc-results: tcrs _)
(make-Values
(for/list ([tcr (in-list tcrs)])
(-result (tc-result-t tcr))))]))
(-unit import-signatures
export-signatures
init-depend-signatures

49
typed-racket-lib/typed-racket/typecheck/possible-domains.rkt
View File

@ -40,7 +40,7 @@
;; of domains that would *satisfy* the expected type, e.g. for the :query-type
;; forms.
;; TODO separating pruning and collapsing into separate functions may be nicer
(define (possible-domains doms rests drests rngs expected [permissive? #t])
(define (possible-domains doms rests rngs expected [permissive? #t])
;; is fun-ty subsumed by a function type in others?
(define (is-subsumed-in? fun-ty others)
@ -60,7 +60,7 @@
(eq? expected-ty #t) ; expected is tc-anyresults, anything is fine
(and expected-ty ; not some unknown expected tc-result
(match fun-ty
[(Function: (list (arr: _ rng _ _ _)))
[(Fun: (list (Arrow: _ _ _ rng)))
(let ([rng (match rng
[(Values: (list (Result: t _ _)))
t]
@ -69,19 +69,20 @@
[_ #f])])
(and rng (subtype rng expected-ty)))]))))
(define orig (map list doms rngs rests drests))
(define orig (map list doms rngs rests))
(define cases
(map (compose make-Function list make-arr)
(map (compose make-Fun list make-Arrow)
doms
rests
(make-list (length doms) null)
(map (match-lambda ; strip props
[(AnyValues: f) (-AnyValues -tt)]
[(Values: (list (Result: t _ _) ...))
(-values t)]
[(ValuesDots: (list (Result: t _ _) ...) _ _)
(-values t)])
rngs)
rests drests (make-list (length doms) null)))
[(AnyValues: f) (-AnyValues -tt)]
[(Values: (list (Result: t _ _) ...))
(-values t)]
[(ValuesDots: (list (Result: t _ _) ...) _ _)
(-values t)])
rngs)))
;; iterate in lock step over the function types we analyze and the parts
;; that we will need to print the error message, to make sure we throw
@ -112,10 +113,11 @@
;; function types with a return type of any then test for subtyping
(define fun-tys-ret-any
(map (match-lambda
[(Function: (list (arr: dom _ rest drest _)))
(make-Function (list (make-arr dom
(-values (list Univ))
rest drest null)))])
[(Fun: (list (Arrow: dom rest _ _)))
(make-Fun (list (make-Arrow dom
rest
null
(-values (list Univ)))))])
candidates))
;; Heuristic: often, the last case in the definition (first at this
@ -142,17 +144,17 @@
(call-with-values
(λ ()
(for/lists (_1 _2 _3 _4) ([xs (in-list (reverse parts-res))])
(values (car xs) (cadr xs) (caddr xs) (cadddr xs))))
(for/lists (_1 _2 _3) ([xs (in-list (reverse parts-res))])
(values (car xs) (cadr xs) (caddr xs))))
list)]))
;; Wrapper over possible-domains that works on types.
(define (cleanup-type t [expected #f] [permissive? #t])
(match t
;; function type, prune if possible.
[(Function/arrs: doms rngs rests drests kws)
(match-let ([(list pdoms rngs rests drests)
(possible-domains doms rests drests rngs
[(Fun: (list (Arrow: doms rests _ rngs) ...))
(match-let ([(list pdoms rngs rests)
(possible-domains doms rests rngs
(and expected (ret expected))
permissive?)])
(if (= (length pdoms) (length doms))
@ -161,7 +163,10 @@
;; the original, which may confuse `:print-type''s pruning detection)
t
;; pruning helped, return pruned type
(make-Function (map make-arr
pdoms rngs rests drests (make-list (length pdoms) null)))))]
(make-Fun (map make-Arrow
pdoms
rests
(make-list (length pdoms) null)
rngs))))]
;; not a function type. keep as is.
[_ t]))

132
typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
View File

@ -14,16 +14,17 @@
(provide/cond-contract
[tc/funapp1
((syntax? stx-list? arr? (listof tc-results/c) (or/c #f tc-results/c))
((syntax? stx-list? Arrow? (listof tc-results/c) (or/c #f tc-results/c))
(#:check boolean?)
. ->* . full-tc-results/c)])
(define (tc/funapp1 f-stx args-stx ftype0 argtys expected #:check [check? #t])
;; update tooltip-table with inferred function type
(add-typeof-expr f-stx (ret (make-Function (list ftype0))))
(add-typeof-expr f-stx (ret (make-Fun (list ftype0))))
(match* (ftype0 argtys)
;; we check that all kw args are optional
[((arr: dom rng rest #f (and kws (list (Keyword: _ _ #f) ...)))
(list (tc-result1: t-a phi-a o-a) ...))
[((Arrow: dom rest (and kws (list (Keyword: _ _ #f) ...)) rng)
(list (tc-result1: t-a _ o-a) ...))
#:when (not (RestDots? rest))
(when check?
(cond [(and (not rest) (not (= (length dom) (length t-a))))
@ -42,65 +43,62 @@
[a (in-syntax args-stx)]
[arg-t (in-list t-a)])
(parameterize ([current-orig-stx a]) (check-below arg-t dom-t))))
(let* ([dom-count (length dom)])
;; Currently do nothing with rest args and keyword args as there are no support for them in
;; objects yet.
(let ([dom-count (length dom)])
;; Currently do nothing with rest args and keyword args
;; as there are no support for them in objects yet.
(let-values
([(o-a t-a) (for/lists (os ts)
([_ (in-range dom-count)]
[oa (in-list/rest o-a -empty-obj)]
[ta (in-list/rest t-a Univ)])
(values oa ta))])
(values->tc-results rng o-a t-a)))]
([(o-a t-a) (if (= dom-count (length t-a))
(values o-a t-a)
(for/lists (os ts)
([_ (in-range dom-count)]
[oa (in-list/rest o-a -empty-obj)]
[ta (in-list/rest t-a Univ)])
(values oa ta)))])
(values->tc-results rng o-a t-a)))]
;; this case should only match if the function type has mandatory keywords
;; but no keywords were provided in the application
[((arr: _ _ _ _
;; at least one mandatory keyword
(app (λ (kws)
(for/or ([keyword (in-list kws)])
(match keyword
[(Keyword: kw _ #t) kw]
[_ #f])))
(? values req-kw))) _)
[((Arrow: _ _ kws _) _)
#:when (ormap Keyword-required? kws)
(when check?
(tc-error/fields "could not apply function"
#:more "a required keyword was not supplied"
"missing keyword" req-kw))]
[((arr: _ _ _ drest '()) _)
"missing keyword"
(car (filter Keyword-required? kws))))]
[((Arrow: _ (? RestDots? drest) '() _) _)
(int-err "funapp with drest args ~a ~a NYI" drest argtys)]
[((arr: _ _ _ _ kws) _)
[((Arrow: _ _ kws _) _)
(int-err "funapp with keyword args ~a NYI" kws)]))
(define (make-printable t)
(match t
[(tc-result1: t) (cleanup-type t)]
[(or (tc-results: ts)
(tc-results: ts _ _ _ _))
(-values (map cleanup-type ts))]
[(tc-any-results: f) (-AnyValues -tt)]
[(tc-results: tcrs _)
(-values (for/list ([tcr (in-list tcrs)])
(cleanup-type (tc-result-t tcr))))]
[(tc-any-results: _) (-AnyValues -tt)]
[_ t]))
(define (stringify-domain dom rst drst [rng #f])
(define (stringify-domain dom rst [rng #f])
(let ([doms-string (if (null? dom) "" (string-append (stringify (map make-printable dom)) " "))]
[rng-string (if rng (format " -> ~a" rng) "")])
(cond [drst
(format "~a~a ... ~a~a" doms-string (car drst) (cdr drst) rng-string)]
[rst
(format "~a~a *~a" doms-string rst rng-string)]
[else (string-append (stringify (map make-printable dom)) rng-string)])))
(match rst
[(RestDots: dty dbound)
(format "~a~a ... ~a~a" doms-string dty dbound rng-string)]
[rst
(format "~a~a *~a" doms-string rst rng-string)]
[else (string-append (stringify (map make-printable dom)) rng-string)])))
;; Generates error messages when operand types don't match operator domains.
(provide/cond-contract
[domain-mismatches
((syntax? syntax? Type? (listof (listof Type?)) (listof (or/c #f Type?))
(listof (or/c #f (cons/c Type? (or/c natural-number/c symbol?))))
((syntax? syntax? Type? (listof (listof Type?)) (listof (or/c #f Type? RestDots?))
(listof SomeValues?) (listof tc-results?) (or/c #f Type?) any/c)
(#:expected (or/c #f tc-results/c)
#:return tc-results?
#:msg-thunk (-> string? string?))
. ->* . tc-results/c)])
(define (domain-mismatches f-stx args-stx ty doms rests drests rngs arg-tys tail-ty tail-bound
(define (domain-mismatches f-stx args-stx ty doms rests rngs arg-tys tail-ty tail-bound
#:expected [expected #f] #:return [return (ret -Bottom)]
#:msg-thunk [msg-thunk (lambda (dom) dom)])
(define arguments-str
@ -114,7 +112,10 @@
#:more (format "~a has type Procedure which cannot be applied"
(name->function-str (and (identifier? f-stx) f-stx)))
#:return return)]
[(and (= 1 (length doms)) (not (car rests)) (not (car drests)) (not tail-ty) (not tail-bound))
[(and (= 1 (length doms))
(not (car rests))
(not tail-ty)
(not tail-bound))
(tc-error/expr
#:return return
(msg-thunk
@ -140,7 +141,7 @@
(msg-thunk
(string-append
"Domain: "
(stringify-domain (car doms) (car rests) (car drests))
(stringify-domain (car doms) (car rests))
"\nArguments: "
arguments-str
"\n"
@ -153,13 +154,13 @@
(define nl+spc (if expected "\n " "\n "))
;; we restrict the domains shown in the error messages to those that
;; are useful
(match-let ([(list pdoms prngs prests pdrests) (possible-domains doms rests drests rngs expected)])
(match-let ([(list pdoms prngs prests) (possible-domains doms rests rngs expected)])
;; if we somehow eliminate all the cases (bogus expected type) fall back to showing the
;; extra cases
(let-values ([(pdoms rngs rests drests)
(let-values ([(pdoms rngs rests)
(if (null? pdoms)
(values doms rngs rests drests)
(values pdoms prngs prests pdrests))])
(values doms rngs rests)
(values pdoms prngs prests))])
;; only use `tc/funapp1` if `tail-ty` was *not* provided
;; since it either won't error correctly or produces a poor error
(cond [(and (not tail-ty)
@ -174,8 +175,10 @@
;; if we narrowed down the possible cases to a single one, have
;; tc/funapp1 generate a better error message
(tc/funapp1 f-stx args-stx
(make-arr (car pdoms) (car rngs)
(car rests) (car drests) null)
(make-Arrow (car pdoms)
(car rests)
null
(car rngs))
arg-tys expected)
return]
[else
@ -184,8 +187,8 @@
(string-append
label
(stringify (if expected
(map stringify-domain pdoms rests drests rngs)
(map stringify-domain pdoms rests drests))
(map stringify-domain pdoms rests rngs)
(map stringify-domain pdoms rests))
nl+spc)
"\nArguments: "
arguments-str
@ -207,13 +210,25 @@
(match t
[(or (Poly-names:
msg-vars
(Function/arrs: msg-doms msg-rngs msg-rests msg-drests (list (Keyword: _ _ #f) ...)))
(Fun: (list (Arrow: msg-doms
msg-rests
(list (Keyword: _ _ #f) ...)
msg-rngs)
...)))
(PolyDots-names:
msg-vars
(Function/arrs: msg-doms msg-rngs msg-rests msg-drests (list (Keyword: _ _ #f) ...)))
(Fun: (list (Arrow: msg-doms
msg-rests
(list (Keyword: _ _ #f) ...)
msg-rngs)
...)))
(PolyRow-names:
msg-vars _
(Function/arrs: msg-doms msg-rngs msg-rests msg-drests (list (Keyword: _ _ #f) ...))))
(Fun: (list (Arrow: msg-doms
msg-rests
(list (Keyword: _ _ #f) ...)
msg-rngs)
...))))
(let ([fcn-string (name->function-str name)])
(if (and (andmap null? msg-doms)
(null? argtypes))
@ -221,7 +236,7 @@
"Could not infer types for applying polymorphic "
fcn-string
"\n"))
(domain-mismatches f-stx args-stx t msg-doms msg-rests msg-drests
(domain-mismatches f-stx args-stx t msg-doms msg-rests
msg-rngs argtypes #f #f #:expected expected
#:msg-thunk (lambda (dom)
(string-append
@ -231,9 +246,16 @@
(list->seteq msg-vars)))
(string-append "Type Variables: " (stringify msg-vars) "\n")
""))))))]
[(or (Poly-names: msg-vars (Function/arrs: msg-doms msg-rngs msg-rests msg-drests kws))
(PolyDots-names: msg-vars (Function/arrs: msg-doms msg-rngs msg-rests msg-drests kws))
(PolyRow-names: msg-vars _ (Function/arrs: msg-doms msg-rngs msg-rests msg-drests kws)))
[(or (Poly-names:
msg-vars
(Fun: (list (Arrow: msg-doms msg-rests kws msg-rngs) ...)))
(PolyDots-names:
msg-vars
(Fun: (list (Arrow: msg-doms msg-rests kws msg-rngs) ...)))
(PolyRow-names:
msg-vars
_
(Fun: (list (Arrow: msg-doms msg-rests kws msg-rngs) ...))))
(let ([fcn-string (if name
(format "function with keywords ~a" (syntax->datum name))
"function with keywords")])
@ -243,7 +265,7 @@
"Could not infer types for applying polymorphic "
fcn-string
"\n"))
(domain-mismatches f-stx args-stx t msg-doms msg-rests msg-drests
(domain-mismatches f-stx args-stx t msg-doms msg-rests
msg-rngs argtypes #f #f #:expected expected
#:msg-thunk (lambda (dom)
(string-append

35
typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt
View File

@ -42,7 +42,7 @@
(match (tc-expr #'fn)
[(tc-result1:
(Poly: vars
(Function: (list (and ar (arr: dom rng (and rest #f) (and drest #f) kw-formals))))))
(Fun: (list (and ar (Arrow: dom #f kw-formals rng))))))
(=> fail)
(unless (set-empty? (fv/list kw-formals))
(fail))
@ -53,17 +53,17 @@
(unless subst (fail))
(tc-keywords #'form (list (subst-all subst ar))
(type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected))])]
[(tc-result1: (Function: arities))
(tc-keywords #'(#%plain-app . form) arities (type->list (tc-expr/t #'kws))
[(tc-result1: (Fun: arrows))
(tc-keywords #'(#%plain-app . form) arrows (type->list (tc-expr/t #'kws))
#'kw-arg-list #'pos-args expected)]
[(tc-result1: (Poly: _ (Function: _)))
[(tc-result1: (Poly: _ (Fun: _)))
(tc-error/expr "Inference for polymorphic keyword functions not supported")]
[(tc-result1: t)
(tc-error/expr "Cannot apply expression of type ~a, since it is not a function type" t)])))
(define (tc-keywords/internal arity kws kw-args error?)
(match arity
[(arr: dom rng rest #f ktys)
[(Arrow: dom (not (? RestDots?)) ktys rng)
;; assumes that everything is in sorted order
(let loop ([actual-kws kws]
[actuals (stx-map tc-expr/t kw-args)]
@ -101,24 +101,25 @@
[else ;; otherwise, ignore this formal param, and continue
(loop actual-kws actuals form-rest)])]))]))
(define (tc-keywords form arities kws kw-args pos-args expected)
(match arities
[(list (and a (arr: dom rng rest #f ktys)))
(define (tc-keywords form arrows kws kw-args pos-args expected)
(match arrows
[(list (and a (Arrow: dom (and rst (not (? RestDots?))) ktys rng)))
(tc-keywords/internal a kws kw-args #t)
(tc/funapp (car (syntax-e form)) kw-args
(->* dom rest rng)
(->* dom rst rng)
(stx-map tc-expr pos-args) expected)]
[(list (and a (arr: doms rngs rests (and drests #f) ktyss)) ...)
(let ([new-arities
(for/list ([a (in-list arities)]
;; find all the arities where the keywords match
[(list (and a (Arrow: doms (and rsts (not (? RestDots?))) _ rngs)) ...)
(let ([new-arrows
(for/list ([a (in-list arrows)]
;; find all the arrows where the keywords match
#:when (tc-keywords/internal a kws kw-args #f))
(match a
[(arr: dom rng rest #f ktys) (make-arr* dom rng #:rest rest)]))])
(if (null? new-arities)
[(Arrow: dom (and rst (not (? RestDots?))) ktys rng)
(make-Arrow dom rst '() rng)]))])
(if (null? new-arrows)
(domain-mismatches
(car (syntax-e form)) (cdr (syntax-e form))
(make-Function arities) doms rests drests rngs
(make-Fun arrows) doms rsts rngs
(stx-map tc-expr pos-args)
#f #f #:expected expected
#:msg-thunk
@ -126,7 +127,7 @@
(string-append "No function domains matched in function application:\n"
dom)))
(tc/funapp (car (syntax-e form)) kw-args
(make-Function new-arities)
(make-Fun new-arrows)
(stx-map tc-expr pos-args) expected)))]))
(define (type->list t)

2
typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt
View File

@ -56,7 +56,7 @@
(tc/funapp #'f #'(arg0 arg ...) f-type (cons (ret t0) (map ret t))
expected-elem-type))
[(tc-result1: t) (ret (make-ListDots t bound0))]
[(tc-results: ts)
[(tc-results: (list (tc-result: ts)) _)
(tc-error/expr "Expected one value, but got ~a" (-values ts))])]
;; otherwise, if it's not a ListDots, defer to the regular function typechecking
;; TODO fix double typechecking

47
typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-main.rkt
View File

@ -47,25 +47,30 @@
;; TODO: handle drest, and props/objects
(define (arr-matches? arr args)
(define (arrow-matches? arr args)
(match arr
[(arr: domain
(Values: (list (Result: v
(PropSet: (TrueProp:) (TrueProp:))
(Empty:)) ...))
rest #f (list (Keyword: _ _ #f) ...))
[(Arrow: domain
(and rst (not (? RestDots?)))
(list (Keyword: _ _ #f) ...)
(Values: (list (Result: v
(PropSet: (TrueProp:) (TrueProp:))
(Empty:))
...)))
(cond
[(< (length domain) (length args)) rest]
[(< (length domain) (length args)) rst]
[(= (length domain) (length args)) #t]
[else #f])]
[_ #f]))
(define (has-props? arr)
(match arr
[(arr: _ (Values: (list (Result: v
[(Arrow: _
_
(list (Keyword: _ _ #f) ...)
(Values: (list (Result: v
(PropSet: (TrueProp:) (TrueProp:))
(Empty:)) ...))
_ _ (list (Keyword: _ _ #f) ...)) #f]
(Empty:)) ...)))
#f]
[else #t]))
@ -75,31 +80,31 @@
(let* ([f-ty (tc-expr/t #'f)]
[args* (syntax->list #'args)])
(define (matching-arities arrs)
(for/list ([arr (in-list arrs)] #:when (arr-matches? arr args*)) arr))
(for/list ([arr (in-list arrs)] #:when (arrow-matches? arr args*)) arr))
(define (has-drest/props? arrs)
(for/or ([arr (in-list arrs)])
(or (has-props? arr) (arr-drest arr))))
(or (has-props? arr)
(RestDots? (Arrow-rst arr)))))
(define arg-tys
(match f-ty
[(Function: (? has-drest/props?))
[(Fun: (? has-drest/props?))
(map single-value args*)]
[(Function:
(app matching-arities
(list (arr: doms _ rests _ _) ..1)))
[(Fun: (app matching-arities
(list (Arrow: doms rsts _ _) ..1)))
;; if for a particular argument, all of the domain types
;; agree for each arr type in the case->, then we use
;; that type to check against
;; agree for each arrow type in the case->, then we use
;; that type to check the argument expression against
(for/list ([arg-stx (in-list args*)]
[arg-idx (in-naturals)])
(define dom-ty (list-ref/default (car doms)
arg-idx
(car rests)))
(car rsts)))
(cond
[(for/and ([dom (in-list doms)]
[rest (in-list rests)])
[rst (in-list rsts)])
(equal? dom-ty
(list-ref/default dom arg-idx rest)))
(list-ref/default dom arg-idx rst)))
(tc-expr/check arg-stx (ret dom-ty))]
[else (single-value arg-stx)]))]
[_ (map single-value args*)]))

39
typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt
View File

@ -20,9 +20,12 @@
;; call-with-values
(pattern (call-with-values prod con)
(match (tc/funapp #'prod #'() (tc-expr/t #'prod) null #f)
[(tc-results: ts fs os)
(tc/funapp #'con #'(prod) (tc-expr/t #'con) (map ret ts fs os) expected)]
[(tc-results: ts fs os drest dbound)
[(tc-results: tcrs #f)
(tc/funapp #'con #'(prod) (tc-expr/t #'con)
(for/list ([tcr (in-list tcrs)])
(-tc-results (list tcr) #f))
expected)]
[(tc-results: _ (? RestDots?))
(tc-error/expr "`call-with-values` with ... is not supported")]
[(tc-any-results: _)
(tc/app-regular this-syntax expected)]))
@ -33,26 +36,16 @@
[(or #f (tc-any-results: _)) (single-value #'arg)]
[(tc-result1: tp)
(single-value #'arg expected)]
[(tc-results: ts)
(single-value #'arg)] ;Type check the argument, to find other errors
;; match polydots case and error
[(tc-results: ts _ _ dty dbound)
(single-value #'arg)]))
;; Type check the argument, to find other errors
[_ (single-value #'arg)]))
;; handle `values' specially
(pattern (values . args)
(match expected
[(tc-results: ets efs eos)
(match-let ([(list (tc-result1: ts fs os) ...)
(for/list
([arg (in-syntax #'args)]
[et (in-sequences (in-list ets) (in-cycle (in-value #f)))]
[ef (in-sequences (in-list efs) (in-cycle (in-value #f)))]
[eo (in-sequences (in-list eos) (in-cycle (in-value #f)))])
(if et
(single-value arg (ret et ef eo))
(single-value arg)))])
(ret ts fs os))]
[_ (match-let ([(list (tc-result1: ts fs os) ...)
(for/list ([arg (in-syntax #'args)])
(single-value arg))])
(ret ts fs os))])))
[(or (tc-results: tcrs #f)
(bind tcrs '()))
(-tc-results
(for/list ([arg (in-syntax #'args)]
[tcr (in-list/rest tcrs #f)])
(match (single-value arg (and tcr (-tc-results (list tcr) #f)))
[(tc-results: (list res) #f) res]))
#f)])))

54
typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
View File

@ -45,8 +45,9 @@
(define (failure)
(match f-ty
[(tc-result1:
(and t (AnyPoly-names: _ _ (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1)))))
(domain-mismatches f args t doms rests drests rngs arg-tres full-tail-ty #f
(and t (AnyPoly-names: _ _
(Fun: (list (Arrow: doms rests (list (Keyword: _ _ #f) ...) rngs) ..1)))))
(domain-mismatches f args t doms rests rngs arg-tres full-tail-ty #f
#:msg-thunk (lambda (dom)
(string-append
"Bad arguments to function in `apply':\n"
@ -54,31 +55,36 @@
(match f-ty
;; apply of a simple function or polymorphic function
[(tc-result1: (AnyPoly: vars dotted-vars (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1))))
[(tc-result1:
(AnyPoly: vars dotted-vars (Fun: (list arrows ..1))))
#:when (not (for*/or ([a (in-list arrows)]
[kws (in-value (Arrow-kws a))])
(ormap Keyword-required? kws)))
(or
(for/or ([domain (in-list doms)]
[range (in-list rngs)]
[rest (in-list rests)]
[drest (in-list drests)])
;; Takes a possible substitution and comuptes the substituted range type if it is not #f
(define (finish substitution)
(and substitution (do-ret (subst-all substitution range))))
(for/or ([arrow (in-list arrows)])
(match arrow
[(Arrow: domain rst _ rng)
;; Takes a possible substitution and comuptes
;; the substituted range type if it is not #f
(define (finish substitution)
(and substitution (do-ret (subst-all substitution rng))))
(finish
(infer vars dotted-vars
(list (-Tuple* arg-tys full-tail-ty))
(list (-Tuple* domain
(cond
;; the actual work, when we have a * function
[rest (make-Listof rest)]
;; ... function
[drest (make-ListDots (car drest) (cdr drest))]
;; the function has no rest argument,
;; but provides all the necessary fixed arguments
[else -Null])))
range)))
(finish
(infer vars dotted-vars
(list (-Tuple* arg-tys full-tail-ty))
(list (-Tuple* domain
(match rst
;; the actual work, when we have a * function
[(? Type?) (make-Listof rst)]
;; ... function
[(RestDots: dty dbound)
(make-ListDots dty dbound)]
;; the function has no rest argument,
;; but provides all the necessary fixed arguments
[_ -Null])))
rng))]))
(failure))]
[(tc-result1: (AnyPoly: _ _ (Function: '())))
[(tc-result1: (AnyPoly: _ _ (Fun: '())))
(tc-error/expr "Function has no cases")]
[(tc-result1: f-ty)
(tc-error/expr "Type of argument to apply is not a function type: \n~a" f-ty)]))

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

@ -216,7 +216,7 @@
[(begin0 e . es)
(begin0
(tc-expr/check #'e expected)
(tc-body/check #'es (tc-any-results -tt)))]
(tc-body/check #'es (-tc-any-results -tt)))]
;; if
[(if tst thn els) (tc/if-twoarm #'tst #'thn #'els expected)]
;; lambda
@ -247,14 +247,12 @@
[(~and (let-values ([(f) fun]) . body) kw:kw-lambda^)
#:when expected
(match expected
[(tc-result1: (and f (or (Function: _)
(Poly: _ (Function: _)))))
[(tc-result1: (and f (or (? Fun?) (Poly-unsafe: _ (? Fun?)))))
(define actual-kws (attribute kw.value))
(check-kw-arity actual-kws f)
(tc-expr/check/type #'fun (kw-convert f actual-kws #:split #t))
(ret f -true-propset)]
[(or (tc-results: _) (tc-any-results: _))
(tc-expr/check form #f)])]
[_ (tc-expr/check form #f)])]
;; opt function def
[(~and (let-values ([(f) fun]) . body) opt:opt-lambda^)
#:when expected
@ -349,7 +347,7 @@
;; Body must be a non empty sequence of expressions to typecheck.
;; The final one will be checked against expected.
(define (tc-body/check body expected)
(define any-res (tc-any-results #f))
(define any-res (-tc-any-results #f))
(define exps (syntax->list body))
(let loop ([exps exps])
(match exps
@ -359,10 +357,11 @@
(define props
(match results
[(tc-any-results: p) (list p)]
[(tc-results: _ (list (PropSet: p+ p-) ...) _)
(map -or p+ p-)]
[(tc-results: _ (list (PropSet: p+ p-) ...) _ _ _)
(map -or p+ p-)]))
[(tc-results: tcrs _)
(map (match-lambda
[(tc-result: _ (PropSet: p+ p-) _)
(-or p+ p-)])
tcrs)]))
(with-lexical-env+props
props
#:expected any-res

16
typed-racket-lib/typed-racket/typecheck/tc-expression.rkt
View File

@ -54,15 +54,15 @@
(if row? do-row-inst do-normal-inst))
(define (error-case number)
(tc-error/expr
"Cannot instantiate expression that produces ~a values"
number))
"Cannot instantiate expression that produces ~a values"
number))
(match tc-res
[(tc-results: tys fs os)
(match tys
[(list ty)
(ret (list (inst-type ty inst)) fs os)]
[_ (error-case (if (null? tys) 0 "multiple"))])]
[_ (error-case "multiple")]))
[(tc-results: (list (tc-result: t ps o)) #f)
(ret (inst-type t inst) ps o)]
[_ (error-case (if (and (tc-results? tc-res)
(null? (tc-results-ts tc-res)))
0
"multiple"))]))
;; do-normal-inst : Type Syntax -> Type

126
typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
View File

@ -48,11 +48,13 @@
#:expected expected)))]))
(define (subst-dom-objs argtys argobjs rng)
(subst-rep rng (for/list ([o (in-list argobjs)]
[t (in-list argtys)]
[idx (in-naturals)]
#:when (not (Empty? o)))
(list (cons 0 idx) o t))))
(instantiate-obj+simplify
rng
(for/list ([o (in-list argobjs)]
[t (in-list argtys)]
[idx (in-naturals)]
#:when (not (Empty? o)))
(list* idx o t))))
(define (tc/funapp f-stx args-stx f-type args-res expected)
(match-define (list (tc-result1: argtys (PropSet: argps+ argps-) argobjs) ...) args-res)
@ -60,25 +62,29 @@
(match f-type
;; we special-case this (no case-lambda) for improved error messages
;; tc/funapp1 currently cannot handle drest arities
[(Function: (list (and a (arr: _ _ _ #f _))))
(tc/funapp1 f-stx args-stx a args-res expected)]
[(Function: arrs)
;; check there are no drests
#:when (not (ormap arr-drest arrs))
[(Fun: (list arrow))
#:when (not (RestDots? (Arrow-rst arrow)))
(tc/funapp1 f-stx args-stx arrow args-res expected)]
[(Fun: arrows)
;; check there are no RestDots
#:when (not (for/or ([a (in-list arrows)])
(RestDots? (Arrow-rst a))))
(cond
;; find the first function where the argument types match
[(for/or ([a (in-list arrs)])
(match a [(arr: dom _ rest _ _) (and (subtypes/varargs argtys dom rest) a)]))
[(ormap (match-lambda
[(and a (Arrow: dom rst _ _))
(and (subtypes/varargs argtys dom rst) a)])
arrows)
=> (λ (a)
;; then typecheck here -- we call the separate function so that we get
;; the appropriate props/objects
(tc/funapp1 f-stx args-stx a args-res expected #:check #f))]
[else
;; if nothing matched, error
(match arrs
[(list (arr: doms rngs rests drests _) ...)
(match arrows
[(list (Arrow: doms rsts _ rngs) ...)
(domain-mismatches
f-stx args-stx f-type doms rests drests rngs args-res #f #f
f-stx args-stx f-type doms rsts rngs args-res #f #f
#:expected expected
#:msg-thunk (lambda (dom)
(string-append
@ -86,68 +92,71 @@
dom)))])])]
;; any kind of dotted polymorphic function without mandatory keyword args
[(PolyDots: (list fixed-vars ... dotted-var)
(Function: arrs))
(Fun: arrows))
;; check there are no mandatory kw args
#:when (not (for*/or ([a (in-list arrs)]
[kws (in-value (arr-kws a))])
#:when (not (for*/or ([a (in-list arrows)]
[kws (in-value (Arrow-kws a))])
(ormap Keyword-required? kws)))
(for/first-valid-inference
#:in-arrs [a (in-list arrs)]
#:arr-match (arr: dom rng rest drest _)
#:in-arrs [a (in-list arrows)]
#:arr-match (Arrow: dom rst _ rng)
#:function-syntax f-stx
#:args-syntax args-stx
#:infer-when
;; only try inference if the argument lengths are appropriate
(cond [rest (<= (length dom) (length argtys))]
[drest (and (<= (length dom) (length argtys))
(eq? dotted-var (cdr drest)))]
[else (= (length dom) (length argtys))])
(match rst
[(? Type?) (<= (length dom) (length argtys))]
[(RestDots: _ dbound) (and (<= (length dom) (length argtys))
(eq? dotted-var dbound))]
[_ (= (length dom) (length argtys))])
;; Only try to infer the free vars of the rng (which includes the vars
;; in props/objects).
#:maybe-inferred-substitution
(let ([rng (subst-dom-objs argtys argobjs rng)])
(extend-tvars fixed-vars
(cond
[drest
(infer/dots
fixed-vars dotted-var argtys dom (car drest) rng (fv rng)
#:expected (and expected (tc-results->values expected))
#:objs argobjs)]
[rest
(infer/vararg fixed-vars (list dotted-var) argtys dom rest rng
(and expected (tc-results->values expected))
#:objs argobjs)]
;; no rest or drest
[else (infer fixed-vars
(list dotted-var)
argtys
dom
rng
(and expected (tc-results->values expected))
#:objs argobjs)])))
(extend-tvars
fixed-vars
(match rst
[(? Type?)
(infer/vararg
fixed-vars (list dotted-var) argtys dom rst rng
(and expected (tc-results->values expected))
#:objs argobjs)]
[(RestDots: dty _)
(infer/dots
fixed-vars dotted-var argtys dom dty rng (fv rng)
#:expected (and expected (tc-results->values expected))
#:objs argobjs)]
[_ (infer fixed-vars
(list dotted-var)
argtys
dom
rng
(and expected (tc-results->values expected))
#:objs argobjs)])))
#:function-type f-type
#:args-results args-res
#:expected expected)]
;; regular polymorphic functions without dotted rest,
;; we do not choose any instantiations with mandatory keyword arguments
[(Poly: vars (Function: arrs))
;; check there are no drests
#:when (not (ormap arr-drest arrs))
[(Poly: vars (Fun: arrows))
;; check there are no RestDots
#:when (not (for/or ([a (in-list arrows)])
(RestDots? (Arrow-rst a))))
(for/first-valid-inference
#:in-arrs [a (in-list arrs)]
#:arr-match (arr: dom rng rest _ kws)
#:in-arrs [a (in-list arrows)]
#:arr-match (Arrow: dom rst kws rng)
#:function-syntax f-stx
#:args-syntax args-stx
;; only try inference if the argument lengths are appropriate
;; and there's no mandatory kw
#:infer-when
(and (not (ormap Keyword-required? kws)) ((if rest <= =) (length dom) (length argtys)))
(and (not (ormap Keyword-required? kws)) ((if rst <= =) (length dom) (length argtys)))
;; Only try to infer the free vars of the rng (which includes the vars
;; in props/objects).
#:maybe-inferred-substitution
(let ([rng (subst-dom-objs argtys argobjs rng)])
(extend-tvars vars
(infer/vararg vars null argtys dom rest rng
(infer/vararg vars null argtys dom rst rng
(and expected (tc-results->values expected))
#:objs argobjs)))
#:function-type f-type
@ -156,7 +165,11 @@
;; Row polymorphism. For now we do really dumb inference that only works
;; in very restricted cases, but is probably enough for most cases in
;; the Racket codebase. Eventually this should be extended.
[(PolyRow: vars constraints (and f-ty (Function/arrs: doms _ _ #f _)))
[(PolyRow: vars constraints (and f-ty (Fun: arrows)))
;; check there are no RestDots
#:when (not (for/or ([a (in-list arrows)])
(RestDots? (Arrow-rst a))))
(define (fail)
(poly-fail f-stx args-stx f-type args-res
#:name (and (identifier? f-stx) f-stx)
@ -166,9 +179,10 @@
;; only infer if there is only one argument type that has the relevant
;; row type variable in its free variables in all cases
(define row-var-idxs
(for/list ([dom (in-list doms)])
(for*/list ([a (in-list arrows)]
[dom (in-value (Arrow-dom a))])
(define num-occurs
(for/list ([dom-type dom]
(for/list ([dom-type (in-list dom)]
[idx (in-naturals)]
#:when (member row-var (fv dom-type)))
idx))
@ -189,7 +203,7 @@
args-res expected)]
[else (fail)])]
;; procedural structs
[(Struct: _ _ _ (? Function? proc-ty) _ _)
[(Struct: _ _ _ (? Fun? proc-ty) _ _)
(tc/funapp f-stx #`(#,(syntax/loc f-stx dummy) . #,args-stx) proc-ty
(cons (ret f-type) args-res) expected)]
;; parameters are functions too
@ -212,14 +226,14 @@
[(? resolvable?)
(tc/funapp f-stx args-stx (resolve-once f-type) args-res expected)]
;; a union of functions can be applied if we can apply all of the elements
[(Union: (? Bottom?) ts) #:when (andmap Function? ts)
[(Union: (? Bottom?) ts) #:when (andmap Fun? ts)
(merge-tc-results
(for/list ([fty (in-list ts)])
(tc/funapp f-stx args-stx fty args-res expected)))]
;; bottom or error type is a perfectly good fcn type
[(or (Bottom:) (Error:)) (ret f-type)]
;; otherwise fail
[(Poly: ns (Function: arrs))
[(Poly: ns (? Fun?))
(tc-error/expr
(string-append "Cannot infer type instantiation for type ~a. Please add "
"more type annotations")

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

@ -41,17 +41,16 @@
#:attr mapping (make-immutable-free-id-table)
#:attr flag-mapping (make-immutable-free-id-table)))
(define (expected-str tys-len rest-ty drest arg-len rest)
(define (expected-str tys-len rst arg-len rest-id)
(format "Expected function with ~a argument~a~a, but got function with ~a argument~a~a"
tys-len
(if (= tys-len 1) "" "s")
(if (or rest-ty
drest)
(if rst
" and a rest arg"
"")
arg-len
(if (= arg-len 1) "" "s")
(if rest " and a rest arg" "")))
(if rest-id " and a rest arg" "")))
;; tc-lambda-body: Typechecks the body with the given args and names and returns the resulting arr?.
;; arg-names: The identifiers of the positional args
@ -63,47 +62,46 @@
(define/cond-contract
(tc-lambda-body arg-names arg-types #:rest [raw-rest #f] #:expected [expected #f] body)
(->* ((listof identifier?) (listof Type?) syntax?)
(#:rest (or/c #f (list/c identifier? (or/c Type? (cons/c Type? symbol?))))
(#:rest (or/c #f (list/c identifier? (or/c Type? RestDots?)))
#:expected (or/c #f tc-results/c))
arr?)
(define-values (rest-id rest)
Arrow?)
(define-values (rest-id rst)
(if raw-rest
(values (first raw-rest) (second raw-rest))
(values #f #f)))
(define rest-types
(cond
[(not rest) (list)]
[(cons? rest) (list (make-ListDots (car rest) (cdr rest)))]
[else (list (-lst rest))]))
(match rst
[(? Type?) (list (-lst rst))]
[(RestDots: dty dbound)
(list (make-ListDots dty dbound))]
[#f (list)]))
(define rest-names
(if rest-id (list rest-id) null))
(make-arr*
(-Arrow
arg-types
(abstract-results
(with-extended-lexical-env
[#:identifiers (append rest-names arg-names)
#:types (append rest-types arg-types)]
[#:identifiers (append rest-names arg-names)
#:types (append rest-types arg-types)]
(tc-body/check body expected))
arg-names #:rest-id rest-id)
#:rest (and (Type? rest) rest)
#:drest (and (cons? rest) rest)))
#:rest rst))
;; check-clause: Checks that a lambda clause has arguments and body matching the expected type
;; arg-list: The identifiers of the positional args in the lambda form
;; rest-id: The identifier of the rest arg, or #f for no rest arg
;; body: The body of the lambda to typecheck.
;; arg-tys: The expected positional argument types.
;; rest-ty: The expected base type of the rest arg (not poly dotted case)
;; drest: The expected base type of the rest arg and its bound (poly dotted case)
;; rst: #f, expected rest arg Type, or expected RestDots
;; ret-ty: The expected type of the body of the lambda.
(define/cond-contract (check-clause arg-list rest-id body arg-tys rest-ty drest ret-ty)
(define/cond-contract (check-clause arg-list rest-id body arg-tys rst ret-ty)
((listof identifier?)
(or/c #f identifier?) syntax? (listof Type?) (or/c #f Type?)
(or/c #f (cons/c Type? symbol?)) tc-results/c
(or/c #f identifier?) syntax? (listof Type?) (or/c #f Type? RestDots?)
tc-results/c
. -> .
arr?)
Arrow?)
(let* ([arg-len (length arg-list)]
[tys-len (length arg-tys)]
[arg-types
@ -112,9 +110,12 @@
(cond
[(= arg-len tys-len) arg-tys]
[(< arg-len tys-len) (take arg-tys arg-len)]
[(> arg-len tys-len) (append arg-tys
(map (lambda _ (or rest-ty (Un)))
(drop arg-list tys-len)))]))])
[(> arg-len tys-len)
(append arg-tys
(map (if (Type? rst)
(λ _ rst)
(λ _ -Bottom))
(drop arg-list tys-len)))]))])
;; Check that the number of formal arguments is valid for the expected type.
;; Thus it must be able to accept the number of arguments that the expected
@ -123,19 +124,20 @@
;; This allows a form like (lambda args body) to have the type (-> Symbol
;; Number) with out a rest arg.
(when (or (and (< arg-len tys-len) (not rest-id))
(and (> arg-len tys-len) (not (or rest-ty drest))))
(tc-error/delayed (expected-str tys-len rest-ty drest arg-len rest-id)))
(and (> arg-len tys-len) (not rst)))
(tc-error/delayed (expected-str tys-len rst arg-len rest-id)))
(define rest-type
(cond
[(not rest-id) #f]
[drest drest]
[(RestDots? rst) rst]
[(dotted? rest-id)
=> (λ (b) (cons (extend-tvars (list b) (get-type rest-id #:default Univ)) b))]
=> (λ (b) (make-RestDots (extend-tvars (list b) (get-type rest-id #:default Univ))
b))]
[else
(define base-rest-type
(cond
[(type-annotation rest-id) (get-type rest-id #:default Univ)]
[rest-ty rest-ty]
[(Type? rst) rst]
[else Univ]))
(define extra-types
(if (<= arg-len tys-len)
@ -152,8 +154,8 @@
;; drest-ty and drest-bound are both false or not false
;; tc/lambda-clause/check: formals syntax listof[Type?] tc-result
;; option[Type?] option[(cons Type? symbol)] -> arr?
(define (tc/lambda-clause/check formals body arg-tys ret-ty rest-ty drest)
(check-clause (formals-positional formals) (formals-rest formals) body arg-tys rest-ty drest ret-ty))
(define (tc/lambda-clause/check formals body arg-tys ret-ty rst)
(check-clause (formals-positional formals) (formals-rest formals) body arg-tys rst ret-ty))
;; typecheck a single opt-lambda clause with argument list and body
;; tc/opt-lambda-clause: listof[identifier] syntax -> listof[arr?]
@ -188,12 +190,12 @@
(tc-lambda-body arg-list arg-types body)))
;; restrict-to-arity : arr? nat -> (or/c #f arr?)
;; either produces a new arity which is a subtype of arr with arity n,
;; either produces a new arrow which is a subtype of arr with arity n,
;; or #f is that is not possible
(define (restrict-to-arity arr n)
(match arr
;; currently does not handle rest arguments
[(arr: args ret #f #f '())
[(Arrow: args #f '() _)
#:when (= n (length args))
arr]
[_ #f]))
@ -228,12 +230,13 @@
;; Lambda with poly dotted rest argument
[(and rest-id (dotted? rest-id))
=>
(lambda (bound)
(λ (bound)
(unless (bound-index? bound)
(if (bound-tvar? bound)
(tc-error "Bound on ... type (~a) is not an appropriate type variable" bound)
(tc-error/stx rest-id "Bound on ... type (~a) was not in scope" bound)))
(cons (extend-tvars (list bound) (get-type rest-id #:default Univ)) bound))]
(make-RestDots (extend-tvars (list bound) (get-type rest-id #:default Univ))
bound))]
;; Lambda with regular rest argument
[rest-id
(get-type rest-id #:default Univ)]
@ -246,7 +249,7 @@
;; but we can't return anything but a (listof arr?) here
;; FIXME: misses optimization opportunities in this code
(match (tc-expr eta-expanded?)
[(tc-result1: (Function: arrs))
[(tc-result1: (Fun: arrs))
(define possibles (for*/list ([arr (in-list arrs)]
[restricted (in-value (restrict-to-arity arr (length arg-list)))]
#:when restricted)
@ -330,7 +333,10 @@
[(tc-result1: t)
(define resolved (resolve t))
(match resolved
[(Function/arrs: _ _ _ _ '()) resolved]
[(Fun: arrows)
#:when (for/and ([arr (in-list arrows)])
(null? (Arrow-kws arr)))
resolved]
[_ #f])]
[_ #f]))
@ -342,13 +348,18 @@
(define (find-matching-arrs formal-arity arities-seen)
(match-define (list formal-positionals formal-rest) formal-arity)
(match expected-type
[(Function/arrs: argss rets rests drests '() #:arrs fs)
(for/list ([a (in-list argss)] [f (in-list fs)] [r (in-list rests)] [dr (in-list drests)]
#:unless (arities-seen-seen-before? arities-seen (list (length a) (or r dr)))
#:when (if formal-rest
(or r (>= (length a) formal-positionals))
((if (or r dr) <= =) (length a) formal-positionals)))
f)]
[(Fun: arrows)
#:when (for/and ([arr (in-list arrows)])
(null? (Arrow-kws arr)))
(for*/list ([a (in-list arrows)]
[dom (in-value (Arrow-dom a))]
[rst (in-value (Arrow-rst a))]
#:unless (arities-seen-seen-before? arities-seen (list (length dom) rst))
#:when (cond
[formal-rest
(or (Type? rst) (>= (length dom) formal-positionals))]
[else ((if rst <= =) (length dom) formal-positionals)]))
a)]
[_ #f]))
@ -377,24 +388,26 @@
(andmap (λ (f-b-arr) (empty? (third f-b-arr))) used-formals+bodies+arrs)
;; If the empty function is expected, then don't error out
(match expected-type
[(Function: (list)) #f]
[(Fun: (list)) #f]
[_ #t]))
;; TODO improve error message.
(tc-error/expr #:return (list (make-arr* null (Un) #:rest Univ))
(tc-error/expr #:return (list (-Arrow null -Bottom #:rest Univ))
"Expected a function of type ~a, but got a function with the wrong arity"
expected-type)
(apply append
(for/list ([fb* (in-list used-formals+bodies+arrs)])
(match-define (list f* b* t*) fb*)
(match t*
[#f (tc/lambda-clause f* b*)]
[(list (arr: argss rets rests drests '()) ...)
(for/list ([args (in-list argss)] [ret (in-list rets)] [rest (in-list rests)] [drest (in-list drests)])
(tc/lambda-clause/check
f* b* args (values->tc-results ret (formals->objects f*)) rest drest))])))))
(cond
[(not t*) (tc/lambda-clause f* b*)]
[else
(for/list ([arrow (in-list t*)])
(match arrow
[(Arrow: dom rst '() rng)
(tc/lambda-clause/check
f* b* dom (values->tc-results rng (formals->objects f*)) rst)]))])))))
(define (tc/mono-lambda/type formals bodies expected)
(make-Function
(make-Fun
(tc/mono-lambda
(for/list ([f (in-syntax formals)] [b (in-syntax bodies)])
(list (make-formals f) b))
@ -547,10 +560,9 @@
(define formals (syntax->list formals*))
(define ft (t:->* args (tc-results->values return)))
(define names (cons name formals))
(define objs (map (λ (_) -empty-obj) names))
(with-extended-lexical-env
[#:identifiers (cons name formals)
#:types (cons ft args)]
(values
(replace-names names objs (ret ft))
(replace-names names objs (tc-body/check body return)))))
(erase-identifiers (ret ft) names)
(erase-identifiers (tc-body/check body return) names))))

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

@ -118,8 +118,7 @@
[#:identifiers idents
#:types types
#:aliased-objects aliased-objs]
(erase-names
ids-to-erase
(erase-identifiers
(with-lexical-env+props
props
#:expected expected
@ -130,7 +129,8 @@
;; before checking the body
(pre-body-thunk)
;; typecheck the body
(tc-body/check body expected)))))
(tc-body/check body expected))
ids-to-erase)))
(define (tc-expr/maybe-expected/t e names)
(syntax-parse names
@ -208,7 +208,7 @@
ordered-clauses
(λ ()
;; types the user gave.
(define given-rhs-types (map (λ (l) (map tc-result (map get-type l))) remaining-names))
(define given-rhs-types (map (λ (l) (map -tc-result (map get-type l))) remaining-names))
(check-let-body
remaining-names
given-rhs-types
@ -300,9 +300,9 @@
(with-extended-lexical-env
[#:identifiers names
#:types ts]
(replace-names names
os
(loop (cdr clauses))))])))
(substitute-names (loop (cdr clauses))
names
os))])))
;; this is so match can provide us with a syntax property to
;; say that this binding is only called in tail position
@ -317,6 +317,7 @@
(tc-expr/check e expected)]
[_ (tc-expr e)]))
(define (tc/let-values namess exprs body [expected #f])
(let* (;; a list of each name clause
[namess (stx-map syntax->list namess)]

80
typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
View File

@ -2,7 +2,7 @@
(require "../utils/utils.rkt"
racket/match racket/list
(except-in (types abbrev utils prop-ops tc-result)
(except-in (types abbrev utils prop-ops)
-> ->* one-of/c)
(rep type-rep prop-rep object-rep values-rep rep-utils)
(typecheck tc-subst)
@ -18,24 +18,28 @@
(define/cond-contract (abstract-results results arg-names #:rest-id [rest-id #f])
((tc-results/c (listof identifier?)) (#:rest-id (or/c #f identifier?))
. ->* . SomeValues?)
(define positional-arg-objects
(for/list ([n (in-range (length arg-names))])
(make-Path null (cons 0 n))))
(define-values (names objects)
(if rest-id
(values (cons rest-id arg-names)
(cons -empty-obj positional-arg-objects))
(values arg-names positional-arg-objects)))
(tc-results->values (replace-names names objects results)))
(define abstracted (abstract-obj results arg-names))
(tc-results->values
(if rest-id
(erase-identifiers abstracted (list rest-id))
abstracted)))
(define (tc-results->values tc)
(match (fix-results tc)
[(tc-any-results: f)
(-AnyValues f)]
[(tc-results: ts fs os)
(make-Values (map -result ts fs os))]
[(tc-results: ts fs os dty dbound)
(make-ValuesDots (map -result ts fs os) dty dbound)]))
[(tc-results: tcrs #f)
(make-Values
(map (match-lambda
[(tc-result: t ps o) (-result t ps o)])
tcrs))]
[(tc-results: tcrs (RestDots: dty dbound))
(make-ValuesDots
(map (match-lambda
[(tc-result: t ps o) (-result t ps o)])
tcrs)
dty
dbound)]))
(define (flatten-props ps)
(let loop ([ps ps])
@ -59,16 +63,16 @@
[(cons p rst)
(match p
[(TrueProp:) (partition! rst)]
[(TypeProp: obj (Refine: t p))
[(TypeProp: obj (Refine: t raw-p))
(partition! (list (-is-type obj t)
(instantiate-rep/obj p obj t)))
(instantiate-obj raw-p obj)))
(partition! rst)]
[(? TypeProp? p)
(set! atoms (cons p atoms))
(partition! rst)]
[(NotTypeProp: obj (Refine: t p))
[(NotTypeProp: obj (Refine: t raw-p))
(partition! (list (-or (-not-type obj t)
(negate-prop (instantiate-rep/obj p obj t)))))
(negate-prop (instantiate-obj raw-p obj)))))
(when atoms (partition! rst))]
[(? NotTypeProp? p)
(set! atoms (cons p atoms))
@ -128,48 +132,48 @@
(define (unconditional-prop res)
(match res
[(tc-any-results: pset) pset]
[(tc-results (list (tc-result: _ (PropSet: p+ p-) _) ...) _)
(apply -and (map -or p+ p-))]))
[(tc-any-results: p) p]
[(tc-results: tcrs _)
(apply
-and
(map (match-lambda
[(tc-result: _ (PropSet: p+ p-) _)
(-or p+ p-)])
tcrs))]))
(define (merge-tc-results results)
(define/match (merge-tc-result r1 r2)
[((tc-result: t1 (PropSet: p1+ p1-) o1)
(tc-result: t2 (PropSet: p2+ p2-) o2))
(tc-result
(Un t1 t2)
(-PS (-or p1+ p2+) (-or p1- p2-))
(if (equal? o1 o2) o1 -empty-obj))])
(-tc-result
(Un t1 t2)
(-PS (-or p1+ p2+) (-or p1- p2-))
(if (equal? o1 o2) o1 -empty-obj))])
(define/match (same-dty? r1 r2)
[(#f #f) #t]
[((cons t1 dbound) (cons t2 dbound)) #t]
[((RestDots: t1 dbound) (RestDots: t2 dbound)) #t]
[(_ _) #f])
(define/match (merge-dty r1 r2)
[(#f #f) #f]
[((cons t1 dbound) (cons t2 dbound))
(cons (Un t1 t2) dbound)])
(define/match (number-of-values res)
[((tc-results rs #f))
(length rs)]
[((tc-results rs (cons _ dbound)))
(format "~a and ... ~a" (length rs) dbound)])
[((RestDots: t1 dbound) (RestDots: t2 dbound))
(make-RestDots (Un t1 t2) dbound)])
(define/match (merge-two-results res1 res2)
[((tc-result1: (== -Bottom)) res2) res2]
[(res1 (tc-result1: (== -Bottom))) res1]
[((tc-any-results: f1) res2)
(tc-any-results (-or f1 (unconditional-prop res2)))]
(-tc-any-results (-or f1 (unconditional-prop res2)))]
[(res1 (tc-any-results: f2))
(tc-any-results (-or (unconditional-prop res1) f2))]
[((tc-results results1 dty1) (tc-results results2 dty2))
(-tc-any-results (-or (unconditional-prop res1) f2))]
[((tc-results: results1 dty1)
(tc-results: results2 dty2))
;; if we have the same number of values in both cases
(cond
[(and (= (length results1) (length results2))
(same-dty? dty1 dty2))
(tc-results (map merge-tc-result results1 results2)
(-tc-results (map merge-tc-result results1 results2)
(merge-dty dty1 dty2))]
;; otherwise, error
[else

266
typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
View File

@ -5,211 +5,115 @@
(require "../utils/utils.rkt"
(utils tc-utils)
racket/match racket/list
racket/match
(contract-req)
(except-in (types abbrev utils prop-ops path-type subtract overlap)
(env lexical-env)
(except-in (types abbrev utils prop-ops subtype
path-type subtract overlap)
-> ->* one-of/c)
(only-in (infer infer) intersect restrict)
(types subtype)
(rep core-rep type-rep object-rep
prop-rep rep-utils values-rep))
(provide instantiate-obj+simplify)
(provide/cond-contract
[restrict-values (-> SomeValues? (listof Type?) SomeValues?)]
[values->tc-results (->* (SomeValues? (listof OptObject?))
((listof Type?))
full-tc-results/c)]
[replace-names (-> (listof identifier?)
(listof OptObject?)
tc-results/c
tc-results/c)]
[erase-names (-> (listof identifier?)
tc-results/c
tc-results/c)])
(provide subst-rep
instantiate-rep/obj)
(define (instantiate-rep/obj rep obj [t Univ])
(subst-rep rep (list (list (cons 0 0) obj t))))
[erase-identifiers (-> tc-results/c
(listof identifier?)
tc-results/c)])
;; Substitutes the given objects into the values and turns it into a
;; tc-result. This matches up to the substitutions in the T-App rule
;; from the ICFP paper.
(define (values->tc-results v os [ts '()])
(define targets
(for/list ([o (in-list os)]
[arg (in-naturals)]
[t (in-list/rest ts Univ)])
(list (cons 0 arg) o t)))
(define res
(match v
[(AnyValues: p)
(tc-any-results p)]
[(Results: t ps o)
(ret t ps o)]
[(Results: t ps o dty dbound)
(ret t ps o dty dbound)]
[_ (int-err "invalid res in values->tc-results: ~a" res)]))
;; NOTE! 'os' should contain no unbound relative addresses (i.e. "free"
;; De Bruijn indices) as those indices will NOT be updated if they
;; are substituted under binders.
(define (values->tc-results v objs [types '()])
(define res->tc-res
(match-lambda
[(Result: t ps o) (-tc-result t ps o)]))
(subst-tc-results res targets))
;; Restrict the objects in v refering to the current functions
;; arguments to be of the types ts. Uses an identity substitution (yuck)
;; since substitution does this same restriction.
(define (restrict-values v ts)
(define targets
(for/list ([t (in-list ts)]
[arg (in-naturals)])
(define nm (cons 0 arg))
(list nm (-id-path nm) t)))
(subst-rep v targets))
;; For each name replaces all uses of it in res with the
;; corresponding object. This is used so that names do not escape the
;; scope of their definitions
(define (replace-names names objects res)
(define targets
(for/list ([nm (in-list names)]
[o (in-list objects)])
(list nm o Univ)))
(subst-tc-results res targets))
(define (erase-names names res)
(define targets
(for/list ([nm (in-list names)])
(list nm -empty-obj Univ)))
(subst-tc-results res targets))
(define (subst-tc-results res targets)
(define (sr t ps o)
(subst-tc-result t ps o targets))
(define (sub x) (subst-rep x targets))
(define mapping (for/list ([o (in-list objs)]
[t (in-list/rest types Univ)]
[idx (in-naturals)])
(list* idx o t)))
(match res
[(tc-any-results: p) (tc-any-results (sub p))]
[(tc-results: ts ps os)
(tc-results (map sr ts ps os) #f)]
[(tc-results: ts ps os dt db)
(tc-results (map sr ts ps os) (cons (sub dt) db))]
[_ (int-err "invalid res in subst-tc-results: ~a" res)]))
(match (instantiate-obj+simplify v mapping)
[(AnyValues: p)
(-tc-any-results p)]
[(Values: rs)
(-tc-results (map res->tc-res rs) #f)]
[(ValuesDots: rs dty dbound)
(-tc-results (map res->tc-res rs) (make-RestDots dty dbound))]))
;; Substitution of objects into a tc-result This is a combination of
;; the other substitutions, plus a restriction of the returned type to
;; the arguments type if the returned object corresponds to an
;; argument.
(define (subst-tc-result r-t r-ps r-o targets)
(define type*
(match r-o
[(Path: flds nm)
(cond
[(assoc nm targets name-ref=?) =>
(match-lambda
[(list _ _ t)
(or (path-type flds t) Univ)])]
[else Univ])]
[_ Univ]))
(define (erase-identifiers res names)
(substitute-names res names (for/list ([_ (in-list names)])
-empty-obj)))
(tc-result
(intersect (subst-rep r-t targets)
type*)
(subst-rep r-ps targets)
(subst-rep r-o targets)))
;; inc-lvls
;; This function increments the 'lvl' field in all of the targets
;; and objects of substitution (see 'inc-lvl' above)
(define (inc-lvls targets)
(for/list ([tgt (in-list targets)])
(match tgt
[(list nm1 (Path: flds nm2) ty)
(list (inc-lvl nm1) (make-Path flds (inc-lvl nm2)) ty)]
[(cons nm1 rst)
(cons (inc-lvl nm1) rst)])))
;; Simple substitution of objects into a Rep
;; This is basically 'rep[x ↦ o]'.
;; If that was the only substitution we were doing,
;; and the type of 'x' was 'τ', then 'targets'
;; would equal (list (list x o τ)) (i.e. it's the list of
;; identifiers being substituted out, the optional object replacing
;; them, and their type).
(define/cond-contract (subst-rep rep targets)
(-> any/c (listof (list/c name-ref/c OptObject? Type?))
any/c)
(define (subst/inc rep)
(subst-rep rep (inc-lvls targets)))
;; substitution loop
(let subst ([rep rep])
(define (instantiate-obj+simplify rep mapping)
;; lookup: if idx has a mapping,
;; then returns (cons/c OptObject? Type?),
;; else returns #f
(define (lookup idx) (match (assv idx mapping)
[(cons _ entry) entry]
[_ #f]))
(let subst/lvl ([rep rep] [lvl 0])
(define (subst rep) (subst/lvl rep lvl))
(match rep
;; Functions
;; increment the level of the substituted object
[(arr: dom rng rest drest kws)
(make-arr (map subst dom)
(subst/inc rng)
(and rest (subst rest))
(and drest (cons (subst (car drest)) (cdr drest)))
(map subst kws))]
[(Arrow: dom rst kws rng)
(make-Arrow (map subst dom)
(and rst (subst rst))
(map subst kws)
(subst/lvl rng (add1 lvl)))]
[(Intersection: ts raw-prop)
(-refine (make-Intersection (map subst ts))
(subst/inc raw-prop))]
[(Path: flds nm)
(let ([flds (map subst flds)])
(cond
[(assoc nm targets name-ref=?)
=>
(λ (l) (match (second l)
[(Empty:) -empty-obj]
[(Path: flds* nm*)
(make-Path (append flds flds*) nm*)]
[(? LExp? l) #:when (null? flds) l]
[_ -empty-obj]))]
[else (make-Path flds nm)]))]
(subst/lvl raw-prop (add1 lvl)))]
[(Path: flds (cons (== lvl) (app lookup (list o _))))
(make-Path (map subst flds) o)]
;; restrict with the type for results and props
[(TypeProp: (and obj (Path: flds nm)) obj-ty)
(let ([flds (map subst flds)])
(cond
[(assoc nm targets name-ref=?) =>
(match-lambda
[(list _ inner-obj inner-obj-ty)
(define inner-obj-ty-at-flds (or (path-type flds inner-obj-ty) Univ))
(define new-obj-ty (intersect obj-ty inner-obj-ty-at-flds obj))
(match inner-obj
[_ #:when (Bottom? new-obj-ty) -ff]
[_ #:when (subtype inner-obj-ty-at-flds obj-ty) -tt]
[(Empty:) -tt]
[(Path: flds* nm*)
(define resulting-obj (make-Path (append flds flds*) nm*))
(-is-type resulting-obj new-obj-ty)]
[(? LExp? l) (if (null? flds)
(-is-type l new-obj-ty)
-ff)])])]
[else (-is-type (make-Path flds nm) (subst obj-ty))]))]
[(NotTypeProp: (and obj (Path: flds nm)) neg-obj-ty)
(let ([flds (map subst flds)])
(cond
[(assoc nm targets name-ref=?)
=>
(match-lambda
[(list _ inner-obj inner-obj-ty)
(define inner-obj-ty-at-flds (or (path-type flds inner-obj-ty) Univ))
(define new-obj-ty (subtract inner-obj-ty-at-flds neg-obj-ty obj))
(define new-neg-obj-ty (restrict neg-obj-ty inner-obj-ty-at-flds obj))
(match inner-obj
[_ #:when (Bottom? new-obj-ty) -ff]
[_ #:when (Bottom? new-neg-obj-ty) -tt]
[(Empty:) -tt]
[(Path: flds* nm*)
(define resulting-obj (make-Path (append flds flds*) nm*))
(-not-type resulting-obj new-neg-obj-ty)]
[(? LExp? l) (if (null? flds)
(-not-type l new-neg-obj-ty)
-ff)])])]
[else
(-not-type (make-Path flds nm) (subst neg-obj-ty))]))]
[(TypeProp: (Path: flds (cons (== lvl) (app lookup (? pair? entry))))
prop-ty)
(define o (make-Path (map subst flds) (car entry)))
(define o-ty (or (path-type flds (cdr entry)) Univ))
(define new-prop-ty (intersect prop-ty o-ty o))
(cond
[(Bottom? new-prop-ty) -ff]
[(subtype o-ty prop-ty) -tt]
[(Empty? o) -tt]
[else (-is-type o new-prop-ty)])]
[(NotTypeProp: (Path: flds (cons (== lvl) (app lookup (? pair? entry))))
prop-ty)
(define o (make-Path (map subst flds) (car entry)))
(define o-ty (or (path-type flds (cdr entry)) Univ))
(define new-o-ty (subtract o-ty prop-ty o))
(define new-prop-ty (restrict prop-ty o-ty o))
(cond
[(or (Bottom? new-o-ty)
(Univ? new-prop-ty))
-ff]
[(Empty? o) -tt]
[else (-not-type o new-prop-ty)])]
[(tc-result: orig-t
orig-ps
(Path: flds (cons (== lvl) (app lookup (? pair? entry)))))
(define o (make-Path (map subst flds) (car entry)))
(define t (intersect orig-t (or (path-type flds (cdr entry)) Univ)))
(define ps (subst orig-ps))
(-tc-result t ps o)]
[(Result: orig-t
orig-ps
(Path: flds (cons (== lvl) (app lookup (? pair? entry)))))
(define o (make-Path (map subst flds) (car entry)))
(define t (intersect orig-t (or (path-type flds (cdr entry)) Univ)))
(define ps (subst orig-ps))
(make-Result t ps o)]
;; else default fold over subfields
[_ (Rep-fmap rep subst)])))

11
typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
View File

@ -90,7 +90,8 @@
;; FIXME - this sucks and should die
[t:type-refinement
(match (lookup-id-type/lexical #'t.predicate)
[(and t (Function: (list (arr: (list dom) (Values: (list (Result: rng _ _))) #f #f '()))))
[(and t (Fun: (list (Arrow: (list dom) #f '()
(Values: (list (Result: rng _ _)))))))
(let ([new-t (make-pred-ty (list dom)
rng
(make-Refinement dom #'t.predicate))])
@ -236,7 +237,7 @@
;; typecheck the expressions of a module-top-level form
;; no side-effects
;; syntax? -> (or/c 'no-type tc-results/c)
(define (tc-toplevel/pass2 form [expected (tc-any-results -tt)])
(define (tc-toplevel/pass2 form [expected (-tc-any-results -tt)])
(do-time (format "pass2 ~a line ~a"
(if #t
@ -358,15 +359,15 @@
;; Register signatures in the signature environment
;; but defer type parsing to allow mutually recursive refernces
;; between signatures and type aliases
(for ([sig-form signature-defs])
(for ([sig-form (in-list signature-defs)])
(parse-and-register-signature! sig-form))
(define-values (type-alias-names type-alias-map)
(get-type-alias-info type-aliases))
;; Add the struct names to the type table, but not with a type
(let ((names (map name-of-struct struct-defs))
(type-vars (map type-vars-of-struct struct-defs)))
(let ([names (map name-of-struct struct-defs)]
[type-vars (map type-vars-of-struct struct-defs)])
(for ([name (in-list names)]
[tvars (in-list type-vars)])
(register-resolved-type-alias

2
typed-racket-lib/typed-racket/typecheck/toplevel-trampoline.rkt
View File

@ -153,7 +153,7 @@
[did-I-suggest-:print-type-already? " ..."]
[else (set! did-I-suggest-:print-type-already? #t)
:print-type-message]))]
[(tc-results: t)
[(tc-results: (list (tc-result: t) ...) #f)
(define tcs (map cleanup-type t))
(define tgs (map generalize tcs))
(define tgs-val (make-Values (map -result tgs)))

13
typed-racket-lib/typed-racket/types/abbrev.rkt
View File

@ -22,7 +22,7 @@
(for-syntax racket/base syntax/parse))
(provide (all-defined-out)
(except-out (all-from-out "base-abbrev.rkt" "match-expanders.rkt") make-arr))
(all-from-out "base-abbrev.rkt" "match-expanders.rkt"))
;; Convenient constructors
(define -App make-App)
@ -151,10 +151,10 @@
(make-Struct name parent flds proc poly pred))
;; Function type constructors
(define/decl top-func (make-Function (list)))
(define/decl top-func (make-Fun (list)))
(define (asym-pred dom rng prop)
(make-Function (list (make-arr* (list dom) rng #:props prop))))
(make-Fun (list (-Arrow (list dom) rng #:props prop))))
(define/cond-contract make-pred-ty
(c:case-> (c:-> Type? Type?)
@ -173,8 +173,9 @@
(define (opt-fn args opt-args result #:rest [rest #f] #:kws [kws null])
(apply cl->* (for/list ([i (in-range (add1 (length opt-args)))])
(make-Function (list (make-arr* (append args (take opt-args i)) result
#:rest rest #:kws kws))))))
(make-Fun (list (-Arrow (append args (take opt-args i))
result
#:rest rest #:kws kws))))))
(define-syntax-rule (->opt args ... [opt ...] res)
(opt-fn (list args ...) (list opt ...) res))
@ -247,4 +248,4 @@
[(_ x:id t p)
(syntax/loc stx
(let ([x (genid (syntax->datum #'x))])
(-refine t (abstract-names p (list x)))))]))
(-refine t (abstract-obj p (list x)))))]))

95
typed-racket-lib/typed-racket/types/base-abbrev.rkt
View File

@ -102,20 +102,23 @@
-Weak-HashTableTop))
;; Function types
(define/cond-contract (make-arr* dom rng
#:rest [rest #f] #:drest [drest #f] #:kws [kws null]
#:props [props -tt-propset] #:object [obj -empty-obj])
(define/cond-contract (-Arrow dom rng
#:rest [rst #f]
#:kws [kws null]
#:props [props -tt-propset]
#:object [obj -empty-obj])
(c:->* ((c:listof Type?) (c:or/c SomeValues? Type?))
(#:rest (c:or/c #f Type?)
#:drest (c:or/c #f (c:cons/c Type? symbol?))
(#:rest (c:or/c #f Type? RestDots?)
#:kws (c:listof Keyword?)
#:props PropSet?
#:object OptObject?)
arr?)
(make-arr dom (if (Type? rng)
(make-Values (list (-result rng props obj)))
rng)
rest drest (sort #:key Keyword-kw kws keyword<?)))
Arrow?)
(make-Arrow dom
rst
(sort kws Keyword<?)
(if (Type? rng)
(make-Values (list (-result rng props obj)))
rng)))
(define-syntax (->* stx)
(define-syntax-class c
@ -123,22 +126,22 @@
(syntax-parse stx
[(_ dom rng)
(syntax/loc stx
(make-Function (list (make-arr* dom rng))))]
(make-Fun (list (-Arrow dom rng))))]
[(_ dom rst rng)
(syntax/loc stx
(make-Function (list (make-arr* dom rng #:rest rst))))]
(make-Fun (list (-Arrow dom rng #:rest rst))))]
[(_ dom rng :c props)
(syntax/loc stx
(make-Function (list (make-arr* dom rng #:props props))))]
(make-Fun (list (-Arrow dom rng #:props props))))]
[(_ dom rng _:c props _:c object)
(syntax/loc stx
(make-Function (list (make-arr* dom rng #:props props #:object object))))]
(make-Fun (list (-Arrow dom rng #:props props #:object object))))]
[(_ dom rst rng _:c props)
(syntax/loc stx
(make-Function (list (make-arr* dom rng #:rest rst #:props props))))]
(make-Fun (list (-Arrow dom rng #:rest rst #:props props))))]
[(_ dom rst rng _:c props : object)
(syntax/loc stx
(make-Function (list (make-arr* dom rng #:rest rst #:props props #:object object))))]))
(make-Fun (list (-Arrow dom rng #:rest rst #:props props #:object object))))]))
(define-syntax (-> stx)
(define-syntax-class c
@ -159,30 +162,34 @@
[(_ dom rng) (syntax/loc stx (->* dom rng))]
[(_ dom (dty dbound) rng)
(syntax/loc stx
(make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound)))))]
(make-Fun
(list (-Arrow dom rng #:rest (make-RestDots dty 'dbound)))))]
[(_ dom rng (~datum :) props)
(syntax/loc stx
(->* dom rng (~datum :) props))]
[(_ dom (dty dbound) rng (~datum :) props)
(syntax/loc stx
(make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound) #:props props))))]))
(make-Fun
(list (-Arrow dom rng
#:rest (make-RestDots dty 'dbound)
#:props props))))]))
(define (simple-> doms rng)
(->* doms rng))
(define (->acc dom rng path #:var [var (cons 0 0)])
(define obj (-acc-path path (-id-path var)))
(make-Function
(list (make-arr* dom rng
#:props (-PS (-not-type obj (-val #f))
(-is-type obj (-val #f)))
#:object obj))))
(make-Fun
(list (-Arrow dom rng
#:props (-PS (-not-type obj (-val #f))
(-is-type obj (-val #f)))
#:object obj))))
(define (cl->* . args)
(define (funty-arities f)
(match f
[(Function: as) as]))
(make-Function (apply append (map funty-arities args))))
[(Fun: as) as]))
(make-Fun (apply append (map funty-arities args))))
(define-syntax (cl-> stx)
(syntax-parse stx
@ -194,13 +201,12 @@
(syntax-parse stx
[(_ ty:expr ... (~seq k:keyword kty:expr opt:boolean) ... rng)
(syntax/loc stx
(make-Function
(make-Fun
(list
(make-arr* (list ty ...)
rng
#:kws (sort #:key (match-lambda [(Keyword: kw _ _) kw])
(list (make-Keyword 'k kty opt) ...)
keyword<?)))))]))
(-Arrow (list ty ...)
rng
#:kws (sort (list (make-Keyword 'k kty opt) ...)
Keyword<?)))))]))
(define-syntax (->optkey stx)
(syntax-parse stx
@ -209,16 +215,15 @@
(with-syntax ([((extra ...) ...)
(for/list ([i (in-range (add1 (length l)))])
(take l i))]
[(rsts ...) (for/list ([i (in-range (add1 (length l)))]) #'rst)])
[(rst ...) (for/list ([i (in-range (add1 (length l)))]) #'rst)])
(syntax/loc stx
(make-Function
(make-Fun
(list
(make-arr* (list ty ... extra ...)
rng
#:rest rsts
#:kws (sort #:key (match-lambda [(Keyword: kw _ _) kw])
(list (make-Keyword 'k kty opt) ...)
keyword<?))
(-Arrow (list ty ... extra ...)
rng
#:rest rst
#:kws (sort (list (make-Keyword 'k kty opt) ...)
Keyword<?))
...)))))]
[(_ ty:expr ... [oty:expr ...] (~seq k:keyword kty:expr opt:boolean) ... rng)
(let ([l (syntax->list #'(oty ...))])
@ -226,18 +231,16 @@
(for/list ([i (in-range (add1 (length l)))])
(take l i))])
(syntax/loc stx
(make-Function
(make-Fun
(list
(make-arr* (list ty ... extra ...)
(-Arrow (list ty ... extra ...)
rng
#:rest #f
#:kws (sort #:key (match-lambda [(Keyword: kw _ _) kw])
(list (make-Keyword 'k kty opt) ...)
keyword<?))
#:kws (sort (list (make-Keyword 'k kty opt) ...)
Keyword<?))
...)))))]))
(define (make-arr-dots dom rng dty dbound)
(make-arr* dom rng #:drest (cons dty dbound)))
(-Arrow dom rng #:rest (make-RestDots dty dbound)))
;; Convenient syntax for polymorphic types
(define-syntax -poly

169
typed-racket-lib/typed-racket/types/kw-types.rkt
View File

@ -1,24 +1,20 @@
#lang racket/base
(require "abbrev.rkt"
"../rep/core-rep.rkt"
"../rep/type-rep.rkt"
"../rep/values-rep.rkt"
"../utils/tc-utils.rkt"
"../base-env/annotate-classes.rkt"
"tc-result.rkt"
(require "../utils/utils.rkt"
(utils tc-utils)
(types abbrev tc-result)
(rep core-rep type-rep values-rep)
(base-env annotate-classes)
racket/list racket/set racket/match
racket/format racket/string
racket/dict
syntax/parse)
;; convert : [Listof Keyword] [Listof Type] [Listof Type] [Option Type]
;; [Option Type] [Option (Pair Type symbol)] boolean -> Type
(define (convert kw-ts plain-ts opt-ts rng rest drest split?)
(when drest
(int-err "drest passed to kw-convert"))
(define (convert kw-ts plain-ts opt-ts rng rst split?)
(when (RestDots? rst) (int-err "RestDots passed to kw-convert"))
;; the kw function protocol passes rest args as an explicit list
(define rest-type (if rest (list (-lst rest)) empty))
(define rst-type (if rst (list (-lst rst)) empty))
;; the kw protocol puts the arguments in keyword-sorted order in the
;; function header, so we need to sort the types to match
@ -26,7 +22,7 @@
(sort kw-ts (λ (kw1 kw2) (keyword<? (Keyword-kw kw1)
(Keyword-kw kw2)))))
(make-Function
(make-Fun
(cond
[(not split?)
(define ts
@ -39,8 +35,8 @@
plain-ts
(for/list ([t (in-list opt-ts)]) (-opt t))
(for/list ([t (in-list opt-ts)]) -Boolean)
rest-type)))
(list (make-arr* ts rng #:rest rest #:drest drest))]
rst-type)))
(list (-Arrow ts rng #:rest rst))]
[else
;; The keyword argument types including boolean flags for
;; optional keyword arguments
@ -59,9 +55,8 @@
;; Add boolean arguments for the optional type flaggs.
(define opt-flags (make-list (length opt-ts) -Boolean))
(list (make-arr* (append kw-args plain-ts opt-ts opt-flags rest-type)
rng
#:drest drest))])))
(list (-Arrow (append kw-args plain-ts opt-ts opt-flags rst-type)
rng))])))
;; This is used to fix the props of keyword types.
;; TODO: This should also explore deeper into the actual types and remove props in there as well.
@ -70,54 +65,43 @@
(define (erase-props/Values values)
(match values
[(AnyValues: _) ManyUniv]
[(Results: ts fs os)
(-values ts)]
[(Results: ts fs os dty dbound)
(-values-dots ts dty dbound)]))
[(Values: rs)
(make-Values
(map (match-lambda
[(Result: t _ _) (-result t)])
rs))]
[(ValuesDots: rs dty dbound)
(make-ValuesDots (make-Values
(map (match-lambda
[(Result: t _ _) (-result t)])
rs))
dty
dbound)]))
(define (prefix-of a b)
(define (rest-equal? a b)
(match* (a b)
[(a a) #t]
[(#f _) #f]
[(_ #f) #f]
[(_ _) #f]))
(define (drest-equal? a b)
(match* (a b)
[((list t b) (list t b)) #t]
[(#f #f) #t]
[(_ _) #f]))
(match* (a b)
[((arr: args result rest drest kws)
(arr: args* result* rest* drest* kws*))
(and (< (length args) (length args*))
(rest-equal? rest rest*)
(drest-equal? drest drest*)
(equal? result result*)
(equal? kws kws*)
(for/and ([p (in-list args)]
[p* (in-list args*)])
(equal? p p*)))]))
(define (arity-length a)
(match a
[(arr: args _ _ _ _) (length args)]))
[((Arrow: args1 rst kws rng)
(Arrow: args2 rst kws rng))
(and (< (length args1) (length args2))
(for/and ([t1 (in-list args1)]
[t2 (in-list args2)])
(equal? t1 t2)))]
[(_ _) #f]))
(define (arg-diff a1 a2)
(match a2
[(arr: args _ _ _ _) (drop args (arity-length a1))]))
(drop (Arrow-dom a2)
(length (Arrow-dom a1))))
(define (find-prefixes l)
(define l* (sort l (λ (arr1 arr2) (< (arity-length arr1)
(arity-length arr2)))))
(define l* (sort l (λ (a1 a2) (< (length (Arrow-dom a1))
(length (Arrow-dom a2))))))
(for/fold ([d '()]) ([e (in-list l*)])
(define prefix (for/or ([p (in-dict-keys d)])
(define prefix (for/or ([(p _) (in-assoc d)])
(and (prefix-of p e) p)))
(if prefix
(dict-set d prefix (arg-diff prefix e))
(dict-set d e null))))
(assoc-set d prefix (arg-diff prefix e))
(assoc-set d e null))))
;; handle-extra-or-missing-kws : (Listof Keyword) LambdaKeywords
;; -> (Listof Keyword)
@ -147,13 +131,13 @@
;; use for/list and remove duplicates afterwards instead of
;; set and set->list to retain determinism
(remove-duplicates
(for/list ([(k v) (in-dict table)])
(for/list ([(k v) (in-assoc table)])
(match k
[(arr: mand rng rest drest kws)
[(Arrow: mand rst kws rng)
(define kws* (if actual-kws
(handle-extra-or-missing-kws kws actual-kws)
kws))
(convert kws* mand v rng rest drest split?)]))))
(convert kws* mand v rng rst split?)]))))
(apply cl->* fns))
;; kw-convert : Type (Option LambdaKeywords) [Boolean] -> Type
@ -161,7 +145,7 @@
;; function protocol
(define (kw-convert ft actual-kws #:split [split? #f])
(match ft
[(Function: arrs)
[(Fun: arrs)
(inner-kw-convert arrs actual-kws split?)]
[(Poly-names: names f)
(make-Poly names (kw-convert f actual-kws #:split split?))]
@ -199,9 +183,9 @@
(define non-kw-argc (+ raw-non-kw-argc opt-non-kw-argc))
(define mand-non-kw-argc (- non-kw-argc (* 2 opt-non-kw-argc)))
(match ft
[(Function: arrs)
[(Fun: arrs)
(cond [(= (length arrs) 1) ; no optional args (either kw or not)
(match-define (arr: doms rng _ _ _) (car arrs))
(match-define (Arrow: doms _ _ rng) (car arrs))
(define kw-length
(- (length doms) (+ non-kw-argc (if rest? 1 0))))
(define-values (kw-args other-args) (split-at doms kw-length))
@ -211,17 +195,17 @@
(make-Keyword kw kw-type #t)))
(define rest-type
(and rest? (last other-args)))
(make-Function
(list (make-arr* (take other-args non-kw-argc)
(erase-props/Values rng)
#:kws actual-kws
#:rest rest-type)))]
(make-Fun
(list (-Arrow (take other-args non-kw-argc)
(erase-props/Values rng)
#:kws actual-kws
#:rest rest-type)))]
[(and (even? (length arrs)) ; had optional args
(>= (length arrs) 2))
;; assumption: only one arr is needed, since the types for
;; the actual domain are the same (the difference is in the
;; second type for the optional keyword protocol)
(match-define (arr: doms rng _ _ _) (car arrs))
(match-define (Arrow: doms _ _ rng) (car arrs))
(define kw-length
(- (length doms) (+ non-kw-argc (if rest? 1 0))))
(define kw-args (take doms kw-length))
@ -232,12 +216,12 @@
(define rest-type
(and rest? (last opt-and-rest-args)))
(define opt-types (take opt-and-rest-args opt-non-kw-argc))
(make-Function
(make-Fun
(for/list ([to-take (in-range (add1 (length opt-types)))])
(make-arr* (append mand-args (take opt-types to-take))
(erase-props/Values rng)
#:kws actual-kws
#:rest rest-type)))]
(-Arrow (append mand-args (take opt-types to-take))
(erase-props/Values rng)
#:kws actual-kws
#:rest rest-type)))]
[else (int-err "unsupported arrs in keyword function type")])]
[_ (int-err "unsupported keyword function type")]))
@ -250,9 +234,9 @@
(match-define (lambda-kws actual-mands actual-opts) kw-prop)
(define arrs
(match f-type
[(AnyPoly-names: _ _ (Function: arrs)) arrs]))
(for/and ([arr (in-list arrs)])
(match-define (arr: _ _ _ _ kws) arr)
[(AnyPoly-names: _ _ (Fun: arrs)) arrs]))
(for*/and ([arr (in-list arrs)]
[kws (in-value (Arrow-kws arr))])
(define-values (mand-kw-types opt-kw-types) (partition-kws kws))
(define mand-kws (map Keyword-kw mand-kw-types))
(define opt-kws (map Keyword-kw opt-kw-types))
@ -304,7 +288,7 @@
(define ((opt-convert-arr required-pos optional-pos) arr)
(match arr
[(arr: args result #f #f '())
[(Arrow: args #f '() result)
(define num-args (length args))
(and (>= num-args required-pos)
(<= num-args (+ required-pos optional-pos))
@ -313,24 +297,21 @@
[missing-opt-args (- (+ required-pos optional-pos) num-args)]
[present-flags (map (λ (t) (-val #t)) opt-args)]
[missing-args (make-list missing-opt-args (-val #f))])
(make-arr (append required-args
opt-args
missing-args
present-flags
missing-args)
result
#f
#f
'())))]
[(arr: args result _ _ _) #f]))
(-Arrow (append required-args
opt-args
missing-args
present-flags
missing-args)
result)))]
[_ #f]))
(define (opt-convert ft required-pos optional-pos)
(let loop ([ft ft])
(match ft
[(Function: arrs)
[(Fun: arrs)
(let ([arrs (map (opt-convert-arr required-pos optional-pos) arrs)])
(and (andmap values arrs)
(make-Function arrs)))]
(make-Fun arrs)))]
[(Poly-names: names f)
(match (loop f)
[#f #f]
@ -367,19 +348,19 @@
(define argc (+ raw-argc opt-argc))
(define mand-argc (- argc (* 2 opt-argc)))
(match ft
[(Function: arrs)
[(Fun: arrs)
(cond [(and (even? (length arrs)) (>= (length arrs) 2))
(match-define (arr: doms rng _ _ _) (car arrs))
(match-define (Arrow: doms _ _ rng) (car arrs))
(define-values (mand-args opt-and-rest-args)
(split-at doms mand-argc))
(define rest-type
(and rest? (last opt-and-rest-args)))
(define opt-types (take opt-and-rest-args opt-argc))
(make-Function
(make-Fun
(for/list ([to-take (in-range (add1 (length opt-types)))])
(make-arr* (append mand-args (take opt-types to-take))
rng
#:rest rest-type)))]
(-Arrow (append mand-args (take opt-types to-take))
rng
#:rest rest-type)))]
[else (int-err "unsupported arrs in keyword function type")])]
[_ (int-err "unsupported keyword function type")]))

14
typed-racket-lib/typed-racket/types/match-expanders.rkt
View File

@ -8,7 +8,7 @@
(types resolve base-abbrev)
(for-syntax racket/base syntax/parse))
(provide Listof: List: MListof: AnyPoly: AnyPoly-names: Function/arrs:
(provide Listof: List: MListof: AnyPoly: AnyPoly-names:
SimpleListof: SimpleMListof:
PredicateProp:
Val-able:
@ -75,7 +75,7 @@
[(Mu-unsafe:
(Union: (== -Null)
(list (pair-matcher elem-t (B: 0)))))
(define elem-t* (instantiate-raw-type t elem-t))
(define elem-t* (instantiate-type elem-t t))
(cond
[simple? (and (equal? elem-t elem-t*) elem-t)]
[else elem-t*])]
@ -161,11 +161,6 @@
[(_ vars dotted-vars body)
#'(app unpoly-names vars dotted-vars body)])))
(define-match-expander Function/arrs:
(lambda (stx)
(syntax-parse stx
[(_ doms rngs rests drests kws (~optional (~seq #:arrs arrs) #:defaults ([arrs #'_])))
#'(Function: (and arrs (list (arr: doms rngs rests drests kws) (... ...))))])))
;; A match expander for matching the prop on a predicate. This assumes a standard
;; predicate type of the shape (-> Any Any : SomeType)
@ -173,4 +168,7 @@
(λ (stx)
(syntax-parse stx
[(_ ps)
#'(Function: (list (arr: (list _) (Values: (list (Result: _ ps _))) _ _ _)))])))
#'(Fun: (list (Arrow: (list _)
_
_
(Values: (list (Result: _ ps _))))))])))

2
typed-racket-lib/typed-racket/types/overlap.rkt
View File

@ -125,7 +125,7 @@
(Val-able: (? simple-datum? v2)))
(equal? v1 v2)]
[((Val-able: (? simple-datum?))
(or (? Struct?) (? StructTop?) (? Function?)))
(or (? Struct?) (? StructTop?) (? Fun?)))
#:no-order
#f]
[((Val-able: (not (? hash?)))

2
typed-racket-lib/typed-racket/types/path-type.rkt
View File

@ -77,7 +77,7 @@
[((Distinction: _ _ t) _) (path-type path t resolved)]
;; for private fields in classes
[((Function: (list (arr: doms (Values: (list (Result: rng _ _))) _ _ _)))
[((Fun: (list (Arrow: doms _ _ (Values: (list (Result: rng _ _))))))
(cons (FieldPE:) rst))
(path-type rst rng (hash))]

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

@ -267,7 +267,7 @@
;; Convert an arr (see type-rep.rkt) to its printable form
(define (arr->sexp arr)
(match arr
[(arr: dom rng rest drest kws)
[(Arrow: dom rest kws rng)
(append
(list '->)
(map type->sexp dom)
@ -281,8 +281,11 @@
(if req?
(format "~a ~a" k (type->sexp t))
(format "[~a ~a]" k (type->sexp t)))]))
(if rest `(,(type->sexp rest) *) null)
(if drest `(,(type->sexp (car drest)) ... ,(cdr drest)) null)
(match rest
[(? Type?) `(,(type->sexp rest) *)]
[(RestDots: dty dbound)
`(,(type->sexp dty) ... ,dbound)]
[_ null])
(match rng
[(AnyValues: (? TrueProp?)) '(AnyValues)]
[(AnyValues: p) `(AnyValues : ,(prop->sexp p))]
@ -334,8 +337,8 @@
;; see type-contract.rkt, which does something similar and this code
;; was stolen from/inspired by/etc.
(match* ((first arrs) (last arrs))
[((arr: first-dom rng rst _ kws)
(arr: last-dom _ _ _ _))
[((Arrow: first-dom rst kws rng)
(Arrow: last-dom _ _ _))
(define-values (mand-kws opt-kws) (partition-kws kws))
(define opt-doms (drop last-dom (length first-dom)))
`(->*
@ -383,8 +386,8 @@
;; Convert a case-> type to an s-expression
(define (case-lambda->sexp type)
(match type
[(Function: arities)
(match arities
[(Fun: arrows)
(match arrows
[(list) '(case->)]
[(list a) (arr->sexp a)]
[(and arrs (list a b ...))
@ -549,11 +552,11 @@
`#(,(string->symbol (format "struct:~a" (syntax-e nm)))
,(map t->s t)
,@(if proc (list (t->s proc)) null))]
[(Function: arities)
[(? Fun?)
(parameterize ([current-print-type-fuel
(sub1 (current-print-type-fuel))])
(case-lambda->sexp type))]
[(arr: _ _ _ _ _) `(arr ,(arr->sexp type))]
[(? Arrow?) `(Arrow ,(arr->sexp type))]
[(Vector: e) `(Vectorof ,(t->s e))]
[(HeterogeneousVector: e) `(Vector ,@(map t->s e))]
[(Box: e) `(Boxof ,(t->s e))]

99
typed-racket-lib/typed-racket/types/prop-ops.rkt
View File

@ -18,7 +18,7 @@
[atomic-complement? (c:-> Prop? Prop? boolean?)]
[atomic-contradiction? (c:-> Prop? Prop? boolean?)]
[contradiction? (c:-> Prop? Prop? boolean?)]
[add-unconditional-prop-all-args (c:-> Function? Type? Function?)]
[add-unconditional-prop-all-args (c:-> Fun? Type? Fun?)]
[add-unconditional-prop (c:-> tc-results/c Prop? tc-results/c)]
[erase-props (c:-> tc-results/c tc-results/c)]
[reduce-propset/type (c:-> PropSet? Type? PropSet?)]
@ -42,27 +42,27 @@
;; return type in the proposition (i.e. if it
;; can't be False, then the else prop should be -ff)
(define (reduce-tc-results/subsumption res)
(define (update-ps t ps obj)
(cond
[(Bottom? t) (tc-result t -ff-propset -empty-obj)]
[else
(define p+ (if ps (PropSet-thn ps) -tt))
(define p- (if ps (PropSet-els ps) -tt))
(define o (if obj obj -empty-obj))
(define (update-ps tcr)
(match tcr
[(tc-result: t ps obj)
(cond
[(or (equal? -False t)
(FalseProp? p+))
(tc-result (intersect t -False) (-PS -ff p-) o)]
[(not (overlap? t -False))
(tc-result t (-PS p+ -ff) o)]
[(FalseProp? p-) (tc-result (subtract t -False) (-PS p+ -ff) o)]
[else (tc-result t (-PS p+ p-) o)])]))
[(Bottom? t) (-tc-result t -ff-propset -empty-obj)]
[else
(define p+ (if ps (PropSet-thn ps) -tt))
(define p- (if ps (PropSet-els ps) -tt))
(define o (if obj obj -empty-obj))
(cond
[(or (equal? -False t)
(FalseProp? p+))
(-tc-result (intersect t -False) (-PS -ff p-) o)]
[(not (overlap? t -False))
(-tc-result t (-PS p+ -ff) o)]
[(FalseProp? p-) (-tc-result (subtract t -False) (-PS p+ -ff) o)]
[else (-tc-result t (-PS p+ p-) o)])])]))
(match res
[(tc-any-results: _) res]
[(tc-results: ts pss os)
(tc-results (map update-ps ts pss os) #f)]
[(tc-results: ts pss os dt db)
(tc-results (map update-ps ts pss os) (cons dt db))]))
[(tc-results: tcrs db)
(-tc-results (map update-ps tcrs) db)]))
;; atomic-contradiction?: Prop? Prop? -> boolean?
@ -395,53 +395,40 @@
;; Ands the given proposition to the props in the tc-results.
;; Useful to express properties of the form: if this expressions returns at all, we learn this
(define/match (add-unconditional-prop results prop)
[((tc-any-results: p) prop) (tc-any-results (-and prop p))]
[((tc-results: ts (list (PropSet: ps+ ps-) ...) os) prop)
(ret ts
(for/list ([p+ (in-list ps+)]
[p- (in-list ps-)])
(-PS (-and prop p+) (-and prop p-)))
os)]
[((tc-results: ts (list (PropSet: ps+ ps-) ...) os dty dbound) prop)
(ret ts
(for/list ([p+ (in-list ps+)] [p- (in-list ps-)])
(-PS (-and prop p+) (-and prop p-)))
os
dty
dbound)])
[((tc-any-results: p) prop) (-tc-any-results (-and prop p))]
[((tc-results: tcrs db) prop)
(-tc-results
(map (match-lambda
[(tc-result: t (PropSet: p+ p-) o)
(-tc-result t (-PS (-and prop p+) (-and prop p-)) o)])
tcrs)
db)])
;; ands the given type prop to both sides of the given arr for each argument
;; useful to express properties of the form: if this function returns at all,
;; we learn this about its arguments (like fx primitives, or car/cdr, etc.)
(define/match (add-unconditional-prop-all-args arr type)
[((Function: (list (arr: dom rng rest drest kws))) type)
[((Fun: (list (Arrow: dom rest kws rng))) type)
(match rng
[(Values: (list (Result: tp (PropSet: -true-prop -false-prop) op)))
[(Values: (list (Result: tp (PropSet: p+ p-) op)))
(let ([new-props (apply -and (build-list (length dom)
(lambda (i)
(-is-type i type))))])
(make-Function
(list (make-arr
dom
(make-Values
(list (-result tp
(-PS (-and -true-prop new-props)
(-and -false-prop new-props))
op)))
rest drest kws))))])])
(make-Fun
(list (make-Arrow dom rest kws
(make-Values
(list (-result tp
(-PS (-and p+ new-props)
(-and p- new-props))
op)))))))])])
;; tc-results/c -> tc-results/c
(define/match (erase-props tc)
[((tc-any-results: _)) (tc-any-results #f)]
[((tc-results: ts _ _))
(define empties (make-list (length ts) #f))
(ret ts
empties
empties)]
[((tc-results: ts _ _ dty dbound))
(define empties (make-list (length ts) #f))
(ret ts
empties
empties
dty dbound)])
[((tc-any-results: _)) (-tc-any-results #f)]
[((tc-results: tcrs dbound))
(-tc-results
(map (match-lambda
[(tc-result: t) (-tc-result t #f #f)])
tcrs)
dbound)])

115
typed-racket-lib/typed-racket/types/substitute.rkt
View File

@ -44,40 +44,14 @@
(let sub ([target target])
(match target
[(F: name) (hash-ref subst name target)]
[(arr: dom rng rest drest kws)
(cond
[(and (pair? drest)
(ormap (λ (name) (and (equal? name (cdr drest))
(not (bound-tvar? name))
name))
names))
=>
(λ (name)
(int-err "substitute used on ... variable ~a in type ~a" name target))]
[else
(make-arr (map sub dom)
(sub rng)
(and rest (sub rest))
(and drest (cons (sub (car drest)) (cdr drest)))
(map sub kws))])]
[(ValuesDots: types dty dbound)
(cond
[(for/or ([name (in-list names)])
(and (equal? dbound name)
(not (bound-tvar? name))))
=>
(λ (name)
(int-err "substitute used on ... variable ~a in type ~a" name target))]
[else (make-ValuesDots (map sub types) (sub dty) dbound)])]
[(ListDots: dty dbound)
(cond
[(for/or ([name (in-list names)])
(and (equal? dbound name)
(not (bound-tvar? name))))
=>
(λ (name)
(int-err "substitute used on ... variable ~a in type ~a" name target))]
[else (make-ListDots (sub dty) dbound)])]
[(or (RestDots: _ dbound)
(ListDots: _ dbound)
(ValuesDots: _ _ dbound))
#:when (and (memq dbound names)
(not (bound-tvar? dbound)))
(int-err "substitute used on ... variable ~a in type ~a"
dbound
target)]
[_ (Rep-fmap target sub)])))
@ -117,26 +91,18 @@
(for/list ([img (in-list images)])
(-result (substitute img name expanded))))))])]
[else (make-ValuesDots (map sub types) (sub dty) dbound)])]
[(arr: dom rng rest drest kws)
(cond
[(and (pair? drest)
(eq? name (cdr drest)))
(make-arr (append
(map sub dom)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sub (car drest))])
(map (λ (img) (substitute img name expanded))
images)))
(sub rng)
rimage
#f
(map sub kws))]
[else
(make-arr (map sub dom)
(sub rng)
(and rest (sub rest))
(and drest (cons (sub (car drest)) (cdr drest)))
(map sub kws))])]
[(Arrow: dom (RestDots: dty dbound) kws rng)
#:when (eq? name dbound)
(make-Arrow
(append
(map sub dom)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sub dty)])
(map (λ (img) (substitute img name expanded))
images)))
rimage
(map sub kws)
(sub rng))]
[_ (Rep-fmap target sub)])))
;; implements curly brace substitution from the formalism, with the addition
@ -145,38 +111,27 @@
(define (substitute-dotted pre-image image image-bound name target)
(let sub ([target target])
(match target
[(F: name*) #:when (eq? name* name) image]
[(ValuesDots: types dty dbound)
(let ([extra-types (cond
[(eq? name dbound) pre-image]
[else null])])
(make-ValuesDots (append (map sub types) (map -result extra-types))
(sub dty)
(cond
[(eq? name dbound) image-bound]
[else dbound])))]
#:when (eq? name dbound)
(make-ValuesDots (append (map sub types)
(map -result pre-image))
(sub dty)
image-bound)]
[(ListDots: dty dbound)
(-Tuple*
(if (eq? name dbound) pre-image null)
(make-ListDots (sub dty)
(if (eq? name dbound) image-bound dbound)))]
[(F: name*)
(cond [(eq? name* name) image]
[else target])]
[(arr: dom rng rest drest kws)
(let ([extra-types (cond
[(and drest (eq? name (cdr drest)))
pre-image]
[else null])])
(make-arr (append (map sub dom) extra-types)
(sub rng)
(and rest (sub rest))
(and drest
(cons (substitute image (cdr drest) (sub (car drest)))
(cond
[(eq? name (cdr drest))
image-bound]
[else (cdr drest)])))
(map sub kws)))]
[(Arrow: dom (RestDots: dty dbound) kws rng)
#:when (eq? name dbound)
(make-Arrow
(append (map sub dom) pre-image)
(make-RestDots
(substitute image dbound (sub dty))
image-bound)
(map sub kws)
(sub rng))]
[_ (Rep-fmap target sub)])))
;; substitute many variables

197
typed-racket-lib/typed-racket/types/subtype.rkt
View File

@ -8,7 +8,9 @@
free-variance rep-switch)
(utils tc-utils)
(only-in (env type-env-structs)
with-lexical-env with-naively-extended-lexical-env lexical-env)
with-lexical-env
with-naively-extended-lexical-env
lexical-env)
(types utils resolve match-expanders current-seen
numeric-tower substitute prefab signatures)
(for-syntax racket/base syntax/parse racket/sequence)
@ -19,7 +21,7 @@
(lazy-require
("../infer/infer.rkt" (infer))
("../typecheck/tc-subst.rkt" (restrict-values instantiate-rep/obj))
("../typecheck/tc-subst.rkt" (instantiate-obj+simplify))
("../typecheck/tc-envops.rkt" (env+ implies-in-env?)))
@ -35,19 +37,22 @@
[unrelated-structs (-> Struct? Struct? boolean?)])
;;************************************************************
;; Public Interface to Subtyping
;;************************************************************
;; When subtype is called w/ no object, we
;; us a temporary object to name the arguments.
;; This parameter gives us plenty of fresh, temporary names
;; to use and this way we don't have to be constantly allocating
;; fresh identifiers.
(define temp-ids
(make-parameter (make-id-seq)))
(define temp-objs
(make-parameter (make-obj-seq)))
;;************************************************************
;; Public Interface to Subtyping
;;************************************************************
;; is t1 a subtype of t2?
;; if obj, then we're assuming obj is the subject
;; type type -> boolean
(define (subtype t1 t2 [obj #f])
(and (subtype* (seen) t1 t2 obj) #t))
@ -100,11 +105,6 @@
(λ (A*) (subvals* A* (cdr vs1) (cdr vs2)))]
[else #f]))
;; check if s is a supertype of any element of ts
(define (supertype-of-one/arr A s ts)
(for/or ([t (in-list ts)])
(arr-subtype*/no-fail A t s)))
(define-syntax (let*/and stx)
(syntax-parse stx
[(_ () . e) (syntax/loc stx (let () . e))]
@ -175,68 +175,50 @@
[(_ _) #f]))))
;; combine-arrs
;;
;; Checks if this function is defined by an uneccessary case->
;; matching the following pattern:
;; τ0 -> σ ∧ τ1 -> σ ∧ τn -> σ ...
;; and if so, returns the combined function type:
;; (∪ τ0 τ1 ... τn)-> σ
;; amk: would it be better to simplify function types ahead of time
;; for cases like this where there is a preferable normal form?
(define/cond-contract (combine-arrs arrs)
(-> (listof arr?) (or/c #f arr?))
(match arrs
[(list (and a1 (arr: dom1 rng1 #f #f '())) (arr: dom rng #f #f '()) ...)
(cond
[(null? dom) (make-arr dom1 rng1 #f #f '())]
[(not (apply = 1 (length dom1) (map length dom))) #f]
[(not (for/and ([rng2 (in-list rng)]) (equal? rng1 rng2)))
#f]
[else (make-arr (apply map Un (cons dom1 dom)) rng1 #f #f '())])]
[_ #f]))
;; used when checking if (Arrow ... rst1 ...)
;; is a subtype of (Arrow2 ... rst2 ...)
(define (rest-arg-subtype* A rst1 rst2)
(match* (rst1 rst2)
[(_ #f) A]
[(t t) A]
[((? Type? t1) (? Type? t2)) (subtype* A t2 t1)]
[((RestDots: t1 dbound)
(RestDots: t2 dbound))
(subtype* A t2 t1)]
[(_ _) #f]))
(define-syntax-rule (with-fresh-ids len ids . body)
(let-values ([(ids seq) (for/fold ([ids '()]
[seq (temp-ids)])
([_ (in-range len)])
(define-values (id rst) (id-seq-next seq))
(values (cons id ids) rst))])
(parameterize ([temp-ids seq])
. body)))
;; simple co/contra-variance for ->
(define/cond-contract (arr-subtype*/no-fail A arr1 arr2)
(-> list? arr? arr? any/c)
(define (arrow-subtype* A arr1 arr2)
(match* (arr1 arr2)
;; the really simple case
[((arr: dom1 rng1 #f #f '())
(arr: dom2 rng2 #f #f '()))
(subtype-seq A
(subtypes* dom2 dom1)
(subval* (restrict-values rng1 dom2) rng2))]
[((arr: dom1 rng1 #f #f kws1)
(arr: dom2 rng2 #f #f kws2))
(subtype-seq A
(subtypes* dom2 dom1)
(kw-subtypes* kws1 kws2)
(subval* (restrict-values rng1 dom2) rng2))]
[((arr: dom1 rng1 rest1 #f kws1)
(arr: dom2 rng2 #f #f kws2))
(subtype-seq A
(subtypes*/varargs dom2 dom1 rest1)
(kw-subtypes* kws1 kws2)
(subval* (restrict-values rng1 dom2) rng2))]
[((arr: dom1 rng1 #f #f kws1)
(arr: dom2 rng2 rest2 #f kws2))
#f]
[((arr: dom1 rng1 rest1 #f kws1)
(arr: dom2 rng2 rest2 #f kws2))
(subtype-seq A
(subtypes*/varargs dom2 dom1 rest1)
(subtype* rest2 rest1)
(kw-subtypes* kws1 kws2)
(subval* (restrict-values rng1 dom2) rng2))]
;; handle ... varargs when the bounds are the same
[((arr: dom1 rng1 #f (cons drest1 dbound) kws1)
(arr: dom2 rng2 #f (cons drest2 dbound) kws2))
(subtype-seq A
(subtype* drest2 drest1)
(subtypes* dom2 dom1)
(kw-subtypes* kws1 kws2)
(subval* (restrict-values rng1 dom2) rng2))]
[(_ _) #f]))
[((Arrow: dom1 rst1 kws1 rng1)
(Arrow: dom2 rst2 kws2 rng2))
(define A* (subtype-seq A
(rest-arg-subtype* rst1 rst2)
(subtypes*/varargs dom2 dom1 rst1)
(kw-subtypes* kws1 kws2)))
(cond
[(not A*) #f]
[else
(define arity (max (length dom1) (length dom2)))
(with-fresh-ids arity ids
(define mapping
(for/list ([idx (in-range arity)]
[id (in-list ids)]
[t (in-list/rest dom2 (or rst2 Univ))])
(list* idx id t)))
(subval* A*
(instantiate-obj+simplify rng1 mapping)
(instantiate-obj rng2 ids)))])]))
;;************************************************************
@ -269,10 +251,13 @@
[(and (null? dom) (null? argtys)) A]
[(null? argtys) #f]
[(and (null? dom) rst)
(cond [(subtype* A (car argtys) rst) => (λ (A) (loop-varargs dom (cdr argtys) A))]
[else #f])]
(cond
[(subtype* A (car argtys) rst)
=> (λ (A) (loop-varargs dom (cdr argtys) A))]
[else #f])]
[(null? dom) #f]
[(subtype* A (car argtys) (car dom)) => (λ (A) (loop-varargs (cdr dom) (cdr argtys) A))]
[(subtype* A (car argtys) (car dom))
=> (λ (A) (loop-varargs (cdr dom) (cdr argtys) A))]
[else #f])))
@ -374,8 +359,8 @@
(subtype* t2 t1)))
(define-syntax-rule (with-fresh-obj obj . body)
(let-values ([(obj os) (obj-seq-next (temp-objs))])
(parameterize ([temp-objs os])
(let-values ([(obj seq) (obj-seq-next (temp-objs))])
(parameterize ([temp-objs seq])
. body)))
;; the algorithm for recursive types transcribed directly from TAPL, pg 305
@ -407,7 +392,7 @@
(and A
(or (TrueProp? raw-prop)
(let* ([obj (if (Object? obj) obj (-id-path (genid)))]
[prop (instantiate-rep/obj raw-prop obj t1)])
[prop (instantiate-obj raw-prop obj)])
(implies-in-env? (lexical-env)
(-is-type obj t1)
prop)))
@ -444,6 +429,26 @@
(subtype* A t1 b2 obj)]
[(_ _) #f]))
;; is this a sequence of arrows of the form
;; τ0 -> σ ∧ τ1 -> σ ∧ τn -> σ ...
;; if so, return
;; (∪ τ0 τ1 ... τn) -> σ
;; else return #f
(define/cond-contract (collapsable-arrows? arrows)
(-> (listof Arrow?) (or/c Arrow? #f))
(match arrows
[(cons (Arrow: (list dom1) #f '() rng) remaining)
(match remaining
[(list (Arrow: (list dom2) #f '() (== rng))
(Arrow: (list doms) #f '() (== rng)) ...)
(-Arrow (list (apply Un dom1 dom2 doms)) rng)]
[_ #f])]
[_ #f]))
;; these data structures are allocated once and
;; used below in 'subtype-switch'
(define seq->elem-table
@ -625,26 +630,20 @@
;; tvars are equal if they are the same variable
[(F: var2) (eq? var1 var2)]
[_ (continue<: A t1 t2 obj)])]
[(case: Function (Function: arrs1))
(match t2
;; special-case for case-lambda/union with only one argument
[(Function: (list arr2))
(cond [(null? arrs1) #f]
[else
(define comb (combine-arrs arrs1))
(or (and comb (arr-subtype*/no-fail A comb arr2))
(supertype-of-one/arr A arr2 arrs1))])]
;; case-lambda
[(Function: arrs2)
(if (null? arrs1) #f
(let loop-arities ([A A]
[arrs2 arrs2])
(cond
[(null? arrs2) A]
[(supertype-of-one/arr A (car arrs2) arrs1)
=> (λ (A) (loop-arities A (cdr arrs2)))]
[else #f])))]
[_ (continue<: A t1 t2 obj)])]
[(case: Fun (Fun: arrows1))
(match* (t2 arrows1)
[((Fun: (list arrow2)) (app collapsable-arrows? (? Arrow? arrow1)))
;; special case when lhs can be collapsed into simpler arrow
(arrow-subtype* A arrow1 arrow2)]
[((Fun: arrows2) _)
(cond
[(null? arrows1) #f]
[else (for/fold ([A A])
([a2 (in-list arrows2)]
#:break (not A))
(for/or ([a1 (in-list arrows1)])
(arrow-subtype* A a1 a2)))])]
[(_ _) (continue<: A t1 t2 obj)])]
[(case: Future (Future: elem1))
(match t2
[(Future: elem2) (subtype* A elem1 elem2)]
@ -720,7 +719,7 @@
[(Refine: t1* raw-prop)
(cond
[(Object? obj)
(define prop (instantiate-rep/obj raw-prop obj t1*))
(define prop (instantiate-obj raw-prop obj))
(define env (env+ (lexical-env) (list prop)))
(cond
[(not env) A]
@ -728,7 +727,7 @@
(subtype* A t1* t2 obj))])]
[else
(with-fresh-obj obj
(define prop (instantiate-rep/obj raw-prop obj t1*))
(define prop (instantiate-obj raw-prop obj))
;; since this is a fresh object, we will do a simpler environment extension
(with-naively-extended-lexical-env [#:props (list prop)]
(subtype* A t1* t2 obj)))])]
@ -1008,7 +1007,7 @@
(and (subtype* A t1 t2*)
(implies-in-env? (lexical-env)
(-is-type obj t1)
(instantiate-rep/obj p* obj t1)))))
(instantiate-obj p* obj)))))
A]
[_ (continue<: A t1 t2 obj)])]
[(case: Vector (Vector: elem1))

148
typed-racket-lib/typed-racket/types/tc-result.rkt
View File

@ -1,7 +1,8 @@
#lang racket/base
(require "../utils/utils.rkt"
(rep core-rep type-rep prop-rep values-rep)
(rep rep-utils core-rep type-rep prop-rep
values-rep free-variance)
(utils tc-utils)
(types base-abbrev)
racket/match
@ -9,13 +10,41 @@
;; this structure represents the result of typechecking an expression
;; fields are #f only when the direct result of parsing or annotations
(define-struct/cond-contract tc-result
([t Type?] [pset (c:or/c PropSet? #f)] [o (c:or/c OptObject? #f)])
#:transparent)
(define-struct/cond-contract tc-results
([ts (c:listof tc-result?)] [drest (c:or/c (c:cons/c Type? symbol?) #f)])
#:transparent)
(define-struct/cond-contract tc-any-results ([f (c:or/c Prop? #f)]) #:transparent)
(def-rep tc-result ([t Type?]
[pset (c:or/c PropSet? #f)]
[o (c:or/c OptObject? #f)])
#:no-provide
[#:frees (f)
(combine-frees (list (f t)
(if pset (f pset) empty-free-vars)
(if o (f o) empty-free-vars)))]
[#:fmap (f)
(make-tc-result (f t)
(and pset (f pset))
(and o (f o)))]
[#:for-each (f)
(f t)
(when pset (f pset))
(when o (f o))])
(def-rep tc-results ([tcrs (c:listof tc-result?)]
[drst (c:or/c #f RestDots?)])
#:no-provide
[#:frees (f)
(combine-frees (cons (if drst (f drst) empty-free-vars)
(map f tcrs)))]
[#:fmap (f)
(make-tc-results (map f tcrs)
(and drst (f drst)))]
[#:for-each (f)
(for-each f tcrs)
(when drst (f drst))])
(def-rep tc-any-results ([p (c:or/c Prop? #f)])
#:no-provide
[#:frees (f) (if p (f p) empty-free-vars)]
[#:fmap (f) (make-tc-any-results (and p (f p)))]
[#:for-each (f) (when p (f p))])
(define (tc-results/c v)
(or (tc-results? v)
@ -23,81 +52,48 @@
(define (tc-results1/c v)
(and (tc-results? v)
(= (length (tc-results-ts v)) 1)))
(= (length (tc-results-tcrs v)) 1)))
;; Contract to check that values are tc-results/c and do not contain #f propset or obj
;; Used to contract the return values of typechecking functions.
(define (full-tc-results/c r)
(match r
[(tc-any-results: p) (and p #t)]
[(tc-results: _ ps os)
(and (andmap (λ (x) x) ps)
[(tc-results: (list (tc-result: _ pss os) ...) _)
(and (andmap (λ (x) x) pss)
(andmap (λ (x) x) os)
#t)]
[(tc-results: _ ps os _ _)
(and (andmap (λ (x) x) ps)
(andmap (λ (x) x) os)
#t)]
[else #f]))
[_ #f]))
(define-match-expander tc-result:
(define-match-expander tc-result:*
(syntax-rules ()
[(_ tp fp op) (tc-result tp fp op)]
[(_ tp) (tc-result tp _ _)]))
;; expand-tc-results: (Listof tc-result) -> (Values (Listof Type) (Listof PropSet) (Listof Object))
(define (expand-tc-results results)
(values (map tc-result-t results) (map tc-result-pset results) (map tc-result-o results)))
(define-match-expander tc-results:
(syntax-rules ()
[(_ tp)
(tc-results (app expand-tc-results tp _ _) #f)]
[(_ tp fp op)
(tc-results (app expand-tc-results tp fp op) #f)]
[(_ tp fp op dty dbound)
(tc-results (app expand-tc-results tp fp op) (cons dty dbound))]))
(define-match-expander tc-any-results:
(syntax-rules ()
[(_ f)
(tc-any-results f)]))
(define-match-expander tc-result1:
(syntax-rules ()
[(_ tp) (tc-results: (list tp))]
[(_ tp fp op) (tc-results: (list tp) (list fp) (list op))]))
[(_ t) (tc-results: (list (tc-result: t _ _)) #f)]
[(_ t ps o) (tc-results: (list (tc-result: t ps o)) #f)]))
(define (tc-results-ts* tc)
(match tc
[(tc-results: t) t]))
[(tc-results: (list (tc-result: ts _ _) ...) _) ts]))
(define-match-expander Result1:
(syntax-rules ()
[(_ tp) (Results: (list tp))]
[(_ tp fp op) (Results: (list tp) (list fp) (list op))]))
;; expand-Results: (Listof Rresult) -> (Values (Listof Type) (Listof PropSet) (Listof Object))
(define (expand-Results results)
(values (map Result-t results) (map Result-ps results) (map Result-o results)))
(define-match-expander Results:
(syntax-rules ()
[(_ tp) (Values: (app expand-Results tp _ _))]
[(_ tp fp op) (Values: (app expand-Results tp fp op))]
[(_ tp fp op dty dbound) (ValuesDots: (app expand-Results tp fp op) dty dbound)]))
;; make-tc-result*: Type? PropSet/c Object? -> tc-result?
;; Smart constructor for a tc-result.
(define (-tc-result type [prop -tt-propset] [object -empty-obj])
(cond
[(or (equal? type -Bottom) (equal? prop -ff-propset))
(tc-result -Bottom -ff-propset object)]
(make-tc-result -Bottom -ff-propset object)]
[else
(tc-result type prop object)]))
(make-tc-result type prop object)]))
;; convenience function for returning the result of typechecking an expression
@ -130,7 +126,7 @@
(if (and (list? t) (list? pset) (list? o))
(map -tc-result t pset o)
(list (-tc-result t pset o)))
(cons dty dbound))]))
(make-RestDots dty dbound))]))
;; fix-props:
@ -150,19 +146,28 @@
;; Turns #f Prop or Obj into the Empty/Trivial
(define (fix-results r)
(match r
[(tc-any-results: f) (tc-any-results (fix-props f -tt))]
[(tc-results: ts ps os)
(ret ts (map fix-props ps) (map fix-object os))]
[(tc-results: ts ps os dty dbound)
(ret ts (map fix-props ps) (map fix-object os) dty dbound)]))
[(tc-any-results: p) (make-tc-any-results (fix-props p -tt))]
[(tc-results: ts drst)
(make-tc-results
(map (match-lambda
[(tc-result: t ps o)
(make-tc-result t (fix-props ps) (fix-object o))])
ts)
drst)]))
(define (fix-results/bottom r)
(match r
[(tc-any-results: f) (tc-any-results (fix-props f -ff))]
[(tc-results: ts ps os)
(ret ts (for/list ([p ps]) (fix-props p -ff-propset)) (map fix-object os))]
[(tc-results: ts ps os dty dbound)
(ret ts (for/list ([p ps]) (fix-props p -ff-propset)) (map fix-object os) dty dbound)]))
[(tc-any-results: p) (make-tc-any-results (fix-props p -ff))]
[(tc-results: (list (tc-result: ts ps os) ...) #f)
(ret ts
(for/list ([p (in-list ps)]) (fix-props p -ff-propset))
(map fix-object os))]
[(tc-results: (list (tc-result: ts ps os) ...) (RestDots: dty dbound))
(ret ts
(for/list ([p (in-list ps)]) (fix-props p -ff-propset))
(map fix-object os)
dty
dbound)]))
(provide/cond-contract
[ret
@ -179,15 +184,20 @@
(define tc-result-equal? equal?)
(provide tc-result: tc-results: tc-any-results: tc-result1: Result1: Results:
tc-results)
(provide tc-any-results: tc-result1: Result1: tc-results:
(rename-out [tc-result:* tc-result:]))
(provide/cond-contract
[rename -tc-result tc-result
(c:case->
(Type? . c:-> . tc-result?)
(Type? PropSet? OptObject? . c:-> . tc-result?))]
[tc-any-results ((c:or/c Prop? #f) . c:-> . tc-any-results?)]
[-tc-result
(c:case->
(Type? . c:-> . tc-result?)
(Type? PropSet? OptObject? . c:-> . tc-result?))]
[tc-result-t (tc-result? . c:-> . Type?)]
[rename make-tc-results -tc-results
(c:-> (c:listof tc-result?)
(c:or/c #f RestDots?)
tc-results?)]
[rename make-tc-any-results -tc-any-results
(c:-> (c:or/c #f Prop?) tc-any-results?)]
[rename tc-results-ts* tc-results-ts (tc-results? . c:-> . (c:listof Type?))]
[tc-result-equal? (tc-result? tc-result? . c:-> . boolean?)]
[tc-result? (c:any/c . c:-> . boolean?)]

4
typed-racket-lib/typed-racket/types/type-table.rkt
View File

@ -105,8 +105,8 @@
;; of the + function)
(printer-thunk type-names
(pretty-format-rep (cleanup-type type))))]
[(or (tc-results: types)
(tc-results: types _ _ _ _)) ; FIXME, account for dty/dbound
[(tc-results: (list (tc-result: types _ _)...) _)
;; FIXME, account for dty/dbound
(printer-thunk type-names
(apply string-append
(for/list ([(type index) (in-indexed (in-list types))])

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

@ -66,10 +66,9 @@
;; is an object type that doesn't mention private fields. Thus we use the
;; FieldPE path element as a marker to refine the result of the accessor
;; function.
[((Function: (list (arr: doms (Values: (list (Result: rng _ _))) _ _ _)))
[((Fun: (list (Arrow: doms _ _ (Values: (list (Result: rng _ _))))))
(FieldPE:))
(make-Function
(list (make-arr* doms (update rng rst))))]
(make-Fun (list (-Arrow doms (update rng rst))))]
[((Union: _ ts) _)
;; Note: if there is a path element, then all Base types are

55
typed-racket-lib/typed-racket/types/utils.rkt
View File

@ -74,33 +74,32 @@
;; has-optional-args? : (Listof arr) -> Boolean
;; Check if the given arrs meet the necessary conditions to be printed
;; with a ->* constructor or for generating a ->* contract
(define (has-optional-args? arrs)
(and (> (length arrs) 1)
;; No polydots
(for/and ([arr (in-list arrs)])
(match arr [(arr: _ _ _ drest _) (not drest)]))
;; Keyword args, range and rest specs all the same.
(let* ([xs (map (match-lambda [(arr: _ rng rest-spec _ kws)
(list rng rest-spec kws)])
arrs)]
[first-x (first xs)])
(for/and ([x (in-list (rest xs))])
(equal? x first-x)))
;; Positionals are monotonically increasing by at most one.
(let-values ([(_ ok?)
(for/fold ([positionals (arr-dom (first arrs))]
[ok-so-far? #t])
([arr (in-list (rest arrs))])
(match arr
[(arr: dom _ _ _ _)
(define ldom (length dom))
(define lpositionals (length positionals))
(values dom
(and ok-so-far?
(or (= ldom lpositionals)
(= ldom (add1 lpositionals)))
(equal? positionals (take dom lpositionals))))]))])
ok?)))
(define (has-optional-args? arrows)
(and (> (length arrows) 1)
;; No polydots
(not (ormap (λ (a) (RestDots? (Arrow-rst a))) arrows))
;; Keyword args, range and rest specs all the same.
(match-let ([(cons (Arrow: _ rst1 kws1 rng1) as) arrows])
(for/and ([a (in-list as)])
(match a
[(Arrow: _ rst2 kws2 rng2)
(and (equal? rst1 rst2)
(equal? kws1 kws2)
(equal? rng1 rng2))])))
;; Positionals are monotonically increasing by at most one.
(let-values ([(_ ok?)
(for/fold ([positionals (Arrow-dom (first arrows))]
[ok? #t])
([arr (in-list (rest arrows))]
#:break (not ok?))
(define dom (Arrow-dom arr))
(define ldom (length dom))
(define lpositionals (length positionals))
(values dom
(and (or (= ldom lpositionals)
(= ldom (add1 lpositionals)))
(equal? positionals (take dom lpositionals)))))])
ok?)))
(provide/cond-contract
[instantiate-poly ((or/c Poly? PolyDots? PolyRow?) (listof Rep?)
@ -111,6 +110,6 @@
[fi (Rep? . -> . (listof symbol?))]
[fv/list ((listof Rep?) . -> . (set/c symbol?))]
[current-poly-struct (parameter/c (or/c #f poly?))]
[has-optional-args? (-> (listof arr?) any)]
[has-optional-args? (-> (listof Arrow?) any)]
)

78
typed-racket-lib/typed-racket/utils/utils.rkt
View File

@ -35,7 +35,11 @@ at least theoretically.
gen-pretty-id
local-tr-identifier?
mark-id-as-normalized
normalized-id?)
normalized-id?
assoc-ref
assoc-set
assoc-remove
in-assoc)
(define optimize? (make-parameter #t))
(define with-linear-integer-arithmetic? (make-parameter #f))
@ -354,18 +358,18 @@ at least theoretically.
#'[(val)
(:do-in
;; ([(outer-id ...) outer-expr] ...)
([(list) list-exp]
[(rest) rest-exp])
([(l) list-exp]
[(r) rest-exp])
;; outer-check
#t
;; ([loop-id loop-expr] ...)
([pos list])
([pos l])
;; pos-guard
#t
;; ([(inner-id ...) inner-expr] ...)
([(val pos) (if (pair? pos)
(values (car pos) (cdr pos))
(values rest '()))])
(values r '()))])
;; pre-guard
#t
;; post-guard
@ -405,4 +409,66 @@ at least theoretically.
(if (eqv? 0 idx)
(car xs)
(list-ref/default (cdr xs) (sub1 idx) default))]
[else default]))
[else default]))
(define assoc-ref
(let ([no-arg (gensym)])
(λ (d key [default no-arg])
(cond
[(assoc key d) => cdr]
[(eq? default no-arg)
(raise-mismatch-error 'assoc-ref
(format "no value for key: ~e in: " key)
d)]
[(procedure? default) (default)]
[else default]))))
(define (assoc-set d key val)
(let loop ([xd d])
(cond
[(null? xd) (list (cons key val))]
[else
(let ([a (car xd)])
(if (equal? (car a) key)
(cons (cons key val) (cdr xd))
(cons a (loop (cdr xd)))))])))
(define (assoc-remove d key)
(let loop ([xd d])
(cond
[(null? xd) null]
[else
(let ([a (car xd)])
(if (equal? (car a) key)
(cdr xd)
(cons a (loop (cdr xd)))))])))
(define (in-assoc-proc l)
(in-parallel (map car l) (map cdr l)))
(define-sequence-syntax in-assoc
(λ () #'in-list/rest-proc)
(λ (stx)
(syntax-case stx ()
[[(key val) (_ assoc-exp)]
#'[(val)
(:do-in
;; ([(outer-id ...) outer-expr] ...)
([(l) assoc-exp])
;; outer-check
#t
;; ([loop-id loop-expr] ...)
([pos l])
;; pos-guard
#t
;; ([(inner-id ...) inner-expr] ...)
([(key val pos) (if (pair? pos)
(values (caar pos) (cdar pos) (cdr pos))
(values #f #f #f))])
;; pre-guard
pos
;; post-guard
#t
;; (loop-arg ...)
(pos))]]
[blah (raise-syntax-error 'in-assoc "invalid usage" #'blah)])))

4
typed-racket-more/typed/rackunit/type-env-ext.rkt
View File

@ -6,8 +6,8 @@
racket/base syntax/parse
(utils tc-utils)
(env init-envs)
(except-in (rep prop-rep object-rep type-rep) make-arr)
(rename-in (types abbrev) [make-arr* make-arr])))
(rep prop-rep object-rep type-rep)
(types abbrev)))
(define-for-syntax unit-env
(make-env

7
typed-racket-test/fail/pr13448.rkt
View File

@ -1,7 +0,0 @@
#lang typed/racket
(: foo
(case->
(Number -> Number)
(Number String -> Number)
(Number String String * -> Number)))
(define (foo x (s1 "") . s) x)

43
typed-racket-test/unit-tests/check-below-tests.rkt
View File

@ -27,14 +27,11 @@
(define (check-result result)
(match result
[(tc-results: ts fs os)
(for-each check-prop fs)
(for-each check-object os) ]
[(tc-results: ts fs os dty bound)
(for-each check-prop fs)
[(tc-results: (list (tc-result: _ ps os) ...) _)
(for-each check-prop ps)
(for-each check-object os)]
[(tc-any-results: f)
(check-prop f)]
[(tc-any-results: p)
(check-prop p)]
[(? Type?)
(void)]))
@ -121,23 +118,23 @@
(ret (list -Symbol) (list -tt-propset) (list -empty-obj))
(ret (list Univ) (list -true-propset) (list (make-Path empty #'x))))
(test-below (ret -Bottom) (tc-any-results #f) #:result (tc-any-results -ff))
(test-below (ret Univ) (tc-any-results -tt) #:result (tc-any-results -tt))
(test-below (tc-any-results -ff) (tc-any-results #f) #:result (tc-any-results -ff))
(test-below (ret -Bottom) (-tc-any-results #f) #:result (-tc-any-results -ff))
(test-below (ret Univ) (-tc-any-results -tt) #:result (-tc-any-results -tt))
(test-below (-tc-any-results -ff) (-tc-any-results #f) #:result (-tc-any-results -ff))
(test-below
(ret (list -Symbol -String) (list -true-propset -ff-propset))
(tc-any-results #f)
#:result (tc-any-results -ff))
(test-below (ret -Symbol -ff-propset) (tc-any-results #f) #:result (tc-any-results -ff))
(-tc-any-results #f)
#:result (-tc-any-results -ff))
(test-below (ret -Symbol -ff-propset) (-tc-any-results #f) #:result (-tc-any-results -ff))
(test-below (ret -Symbol -true-propset -empty-obj) (tc-any-results #f)
#:result (tc-any-results -tt))
(test-below (ret (list -Symbol -String)) (tc-any-results #f)
#:result (tc-any-results -tt))
(test-below (ret -Symbol -true-propset -empty-obj) (-tc-any-results #f)
#:result (-tc-any-results -tt))
(test-below (ret (list -Symbol -String)) (-tc-any-results #f)
#:result (-tc-any-results -tt))
(test-below
(ret (list -Symbol -String) (list -true-propset -false-propset) (list -empty-obj -empty-obj))
(tc-any-results #f)
#:result (tc-any-results -tt))
(-tc-any-results #f)
#:result (-tc-any-results -tt))
(test-below #:fail
@ -146,7 +143,7 @@
#:result (ret (list -Symbol -Symbol) (list -tt-propset -tt-propset) (list -empty-obj -empty-obj)))
(test-below #:fail
(tc-any-results -tt)
(-tc-any-results -tt)
(ret -Symbol))
@ -164,7 +161,7 @@
#:result (ret -Symbol -tt-propset -empty-obj Univ 'B))
(test-below #:fail
(tc-any-results -tt)
(-tc-any-results -tt)
(ret -Symbol #f -empty-obj Univ 'B)
#:result (ret (list -Symbol) (list -tt-propset) (list -empty-obj) Univ 'B))
@ -173,8 +170,8 @@
(ret (list -Symbol -Symbol) (list -tt-propset -tt-propset) (list -empty-obj -empty-obj) Univ 'B))
(test-below (ret -Symbol -true-propset -empty-obj Univ 'B)
(tc-any-results #f)
#:result (tc-any-results -tt))
(-tc-any-results #f)
#:result (-tc-any-results -tt))
(test-below
(ret -Symbol)

32
typed-racket-test/unit-tests/contract-tests.rkt
View File

@ -136,9 +136,9 @@
(t (-set Univ))
(t (make-pred-ty -Symbol))
(t (->key -Symbol #:key -Boolean #t Univ))
(t (make-Function
(list (make-arr* (list Univ) -Boolean #:kws (list (make-Keyword '#:key Univ #t))
#:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol))))))
(t (make-Fun
(list (-Arrow (list Univ) -Boolean #:kws (list (make-Keyword '#:key Univ #t))
#:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol))))))
(t (-struct #'struct-name1 #f (list (make-fld -Symbol #'acc #f))))
;; Adapted from PR 13815
(t (-poly (a) (-> a a)))
@ -184,20 +184,20 @@
;; Github Issue #50
(t (cl->* (-> -String -Bottom) (-> -String -Symbol -Bottom)))
(t (make-Function
(list (make-arr* (list -String) -Boolean
#:kws (list (make-Keyword '#:key Univ #t))
#:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))
(make-arr* (list -String Univ) -Boolean
#:kws (list (make-Keyword '#:key Univ #t))
#:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol))))))
(t (make-Fun
(list (-Arrow (list -String) -Boolean
#:kws (list (make-Keyword '#:key Univ #t))
#:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))
(-Arrow (list -String Univ) -Boolean
#:kws (list (make-Keyword '#:key Univ #t))
#:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol))))))
(t/fail (cl->* (-> -String ManyUniv) (-> -String Univ ManyUniv))
"unknown return values")
(t/fail
(make-Function
(list (make-arr* (list) -Boolean #:kws (list (make-Keyword '#:key Univ #f)))
(make-arr* (list Univ) -Boolean #:kws (list (make-Keyword '#:key2 Univ #f)))))
(make-Fun
(list (-Arrow (list) -Boolean #:kws (list (make-Keyword '#:key Univ #f)))
(-Arrow (list Univ) -Boolean #:kws (list (make-Keyword '#:key2 Univ #f)))))
"case function type with optional keyword arguments")
(t/fail (-> (make-pred-ty -Symbol)-Symbol)
"function type with props or objects")
@ -215,10 +215,10 @@
"required a chaperone contract but generated an impersonator contract")
(t/fail
(make-Function
(make-Fun
(list
(make-arr* (list) -Boolean #:kws (list (make-Keyword '#:key Univ #t)))
(make-arr* (list Univ Univ) -Boolean #:kws (list (make-Keyword '#:key2 Univ #t)))))
(-Arrow (list) -Boolean #:kws (list (make-Keyword '#:key Univ #t)))
(-Arrow (list Univ Univ) -Boolean #:kws (list (make-Keyword '#:key2 Univ #t)))))
"case function type with optional keyword arguments")
(t/fail (-vec (-struct #'struct-name3 #f (list (make-fld (-seq -Symbol) #'acc #f)) #f #t))
"required a chaperone contract but generated an impersonator contract")

2
typed-racket-test/unit-tests/keyword-expansion-test.rkt
View File

@ -16,7 +16,7 @@
(define (extract-arrs t)
(match t
[(Function: arrs) (apply set arrs)]
[(Fun: arrs) (apply set arrs)]
[t t]))
(define-syntax-rule (t-opt ((req-arg ...) (opt-arg ...)) expected)

29
typed-racket-test/unit-tests/metafunction-tests.rkt
View File

@ -163,7 +163,7 @@
(check-equal?
(values->tc-results (make-AnyValues (-is-type '(0 . 0) -String))
(list (make-Path null #'x)) (list Univ))
(tc-any-results (-is-type #'x -String)))
(-tc-any-results (-is-type #'x -String)))
(check-equal?
@ -193,29 +193,30 @@
(make-TypeProp (make-Path (list -car) #'x) -NonPosInt))))
)
(test-suite "replace-names"
(test-suite "term substitution"
(check-equal?
(replace-names (list #'x) (list (make-Path null '(0 . 0)))
(ret Univ -tt-propset (make-Path null #'x)))
(abstract-obj (ret Univ -tt-propset (make-Path null #'x))
(list #'x))
(ret Univ -tt-propset (make-Path null '(0 . 0))))
(check-equal?
(replace-names (list #'x) (list (make-Path null '(0 . 0)))
(ret (-> Univ Univ : -tt-propset : (make-Path null #'x))))
(abstract-obj (ret (-> Univ Univ : -tt-propset : (make-Path null #'x)))
(list #'x))
(ret (-> Univ Univ : -tt-propset : (make-Path null '(1 . 0)))))
(check-equal?
(replace-names (list #'x) (list (make-Path null '(0 . 0)))
(ret (-refine/fresh y -Int (-leq (-lexp y) (-lexp #'x)))
-tt-propset
(make-Path null #'x)))
(abstract-obj (ret (-refine/fresh y -Int (-leq (-lexp y) (-lexp #'x)))
-tt-propset
(make-Path null #'x))
(list #'x))
(ret (-refine/fresh y -Int (-leq (-lexp y) (-lexp (make-Path null '(1 . 0)))))
-tt-propset
(make-Path null '(0 . 0))))
(check-equal?
(replace-names (list #'x) (list -empty-obj)
(ret (-refine/fresh y -Int (-leq (-lexp y) (-lexp #'x)))
-tt-propset
(make-Path null #'x)))
(erase-identifiers
(ret (-refine/fresh y -Int (-leq (-lexp y) (-lexp #'x)))
-tt-propset
(make-Path null #'x))
(list #'x))
(ret -Int
-tt-propset
-empty-obj))

10
typed-racket-test/unit-tests/subst-tests.rkt
View File

@ -30,8 +30,8 @@
(s -Number a (-pair -String (-v a)) (-pair -String -Number))
(s* (-Symbol -String) #f a (make-ListDots (-v a) 'a) (-lst* -Symbol -String))
(s* (-Symbol -String) Univ a (make-ListDots (-v a) 'a) (-lst* -Symbol -String #:tail (-lst Univ)))
(s... (-Number -Boolean) a (make-Function (list (make-arr-dots null -Number (-v a) 'a))) (-Number -Boolean . -> . -Number))
(s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v a) 'a))) (-String -Number -Boolean . -> . -Number))
(s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v b) 'a))) (-String (-v b) (-v b) . -> . -Number))
(s... (-Number -Boolean) a (make-Function (list (make-arr-dots (list -String) -Number (-v b) 'b)))
(make-Function (list (make-arr-dots (list -String) -Number (-v b) 'b))))))
(s... (-Number -Boolean) a (make-Fun (list (make-arr-dots null -Number (-v a) 'a))) (-Number -Boolean . -> . -Number))
(s... (-Number -Boolean) a (make-Fun (list (make-arr-dots (list -String) -Number (-v a) 'a))) (-String -Number -Boolean . -> . -Number))
(s... (-Number -Boolean) a (make-Fun (list (make-arr-dots (list -String) -Number (-v b) 'a))) (-String (-v b) (-v b) . -> . -Number))
(s... (-Number -Boolean) a (make-Fun (list (make-arr-dots (list -String) -Number (-v b) 'b)))
(make-Fun (list (make-arr-dots (list -String) -Number (-v b) 'b))))))

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

@ -552,7 +552,7 @@
[tc-e/t #(2 3 #t) (make-HeterogeneousVector (list -Integer -Integer -Boolean))]
[tc-e (vector 2 "3" #t) (make-HeterogeneousVector (list -Integer -String -Boolean))]
[tc-e (vector) (make-HeterogeneousVector (list))]
[tc-e (vector) #:ret (tc-any-results -tt) #:expected (tc-any-results #f)]
[tc-e (vector) #:ret (-tc-any-results -tt) #:expected (-tc-any-results #f)]
[tc-err (vector)
#:ret (tc-ret -Integer)
#:expected (tc-ret -Integer)]
@ -1163,11 +1163,11 @@
(-lst* -One -String -Char)]
;; instantiating non-dotted terms
[tc-e/t (inst (plambda: (a) ([x : a]) x) Integer)
(make-Function
(list (make-arr* (list -Integer) -Integer
#:props (-PS (-not-type (cons 0 0) (-val #f))
(-is-type (cons 0 0) (-val #f)))
#:object (make-Path null (cons 0 0)))))]
(make-Fun
(list (-Arrow (list -Integer) -Integer
#:props (-PS (-not-type (cons 0 0) (-val #f))
(-is-type (cons 0 0) (-val #f)))
#:object (make-Path null (cons 0 0)))))]
[tc-e/t (inst (plambda: (a) [x : a *] (apply list x)) Integer)
((list) -Integer . ->* . (-lst -Integer) : -true-propset)]