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

add more refinement support for inference and literals (#528)

Browse Source 
This PR adds more support for refinement reasoning, in particular
type inference is now aware of argument objects which allows for
more programs w/ refinements to typecheck. Additionally, working
with vector types and literals that are refined or need to have
properties about their length proven now works.
This commit is contained in:
Andrew Kent 2017-04-22 18:45:22 -04:00 committed by GitHub
parent ebb0770edf
commit 80d1654dee
21 changed files with 832 additions and 508 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
typed-racket-lib/typed-racket/infer/dmap.rkt
View File

@ -39,7 +39,7 @@
#f
(%1 make-dcon
(for/list/fail ([c1 (in-list fixed1)]
[c2 (in-sequence-forever fixed2 rest)])
[c2 (in-list/rest fixed2 rest)])
(c-meet c1 c2))
#f)]
;; redo in the other order to call the previous case
@ -52,7 +52,7 @@
(values fixed2 fixed1 rest2 rest1))])
(% make-dcon
(for/list/fail ([c1 (in-list longer)]
[c2 (in-sequence-forever shorter srest)])
[c2 (in-list/rest shorter srest)])
(c-meet c1 c2))
(c-meet lrest srest)))]
[((struct dcon-dotted (fixed1 c1 bound1)) (struct dcon-dotted (fixed2 c2 bound2)))

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

@ -404,13 +404,16 @@
;; produces a cset which determines a substitution that makes S a subtype of T
;; implements the V |-_X S <: T => C judgment from Pierce+Turner, extended with
;; the index variables from the TOPLAS paper
(define/cond-contract (cgen context S T)
(context? (or/c Values/c ValuesDots? AnyValues?) (or/c Values/c ValuesDots? AnyValues?)
. -> . (or/c #F cset?))
(define/cond-contract (cgen context S T [obj #f])
(->* (context? (or/c Values/c ValuesDots? AnyValues?)
(or/c Values/c ValuesDots? AnyValues?))
((or/c #f OptObject?))
(or/c #F cset?))
;; useful quick loop
(define/cond-contract (cg S T)
(Type? Type? . -> . (or/c #f cset?))
(cgen context S T))
(define/cond-contract (cg S T [obj #f])
(->* (Type? Type?) ((or/c #f OptObject?))
(or/c #f cset?))
(cgen context S T obj))
(define/cond-contract (cg/inv S T)
(Type? Type? . -> . (or/c #f cset?))
(cgen/inv context S T))
@ -454,7 +457,8 @@
;; check each element
[((Result: s pset-s o-s)
(Result: t pset-t o-t))
(% cset-meet (cg s t)
(% cset-meet
(cg s t o-s)
(cgen/prop-set context pset-s pset-t)
(cgen/object context o-s o-t))]
@ -465,8 +469,8 @@
;; Check for a substition that S is below (ret -Bottom).
(define bottom-case
(match S
[(Values: (list (Result: s f-s o-s)))
(cgen context s -Bottom)]
[(Values: (list (Result: s _ o-s)))
(cgen context s -Bottom o-s)]
[else #f]))
(define regular-case
(cgen/seq context s-seq t-seq))
@ -477,7 +481,7 @@
;; they're subtypes. easy.
[(a b) #:when (cond
[(Type? a) (subtype a b)]
[(Type? a) (subtype a b obj)]
[(Result? a) (subresult a b)]
[else (subval a b)])
empty]
@ -488,7 +492,7 @@
;; refinements are erased to their bound
[((Refinement: S _) T)
(cg S T)]
(cg S T obj)]
;; variables that are in X and should be constrained
;; all other variables are compatible only with themselves
@ -513,29 +517,31 @@
;; recursive names should get resolved as they're seen
[(s (? Name? t))
(cg s (resolve-once t))]
(let ([t (resolve-once t)])
(and t (cg s t obj)))]
[((? Name? s) t)
(cg (resolve-once s) t)]
(let ([s (resolve-once s)])
(and s (cg s t obj)))]
;; constrain b1 to be below T, but don't mention the new vars
[((Poly: v1 b1) T) (cgen (context-add context #:bounds v1) b1 T)]
;; Mu's just get unfolded
[((? Mu? s) t) (cg (unfold s) t)]
[(s (? Mu? t)) (cg s (unfold t))]
[((? Mu? s) t) (cg (unfold s) t obj)]
[(s (? Mu? t)) (cg s (unfold t) obj)]
;; find *an* element of elems which can be made a subtype of T
[((Intersection: ts raw-prop) T)
(cset-join
(for*/list ([t (in-list ts)]
[v (in-value (cg t T))]
[v (in-value (cg t T obj))]
#:when v)
v))]
;; constrain S to be below *each* element of elems, and then combine the constraints
[(S (Intersection: ts raw-prop))
(define cs (for/list/fail ([ts (in-list ts)]) (cg S ts)))
(let ([obj (-id-path (genid))])
(define cs (for/list/fail ([ts (in-list ts)]) (cg S ts obj)))
(let ([obj (if (Object? obj) obj (-id-path (genid)))])
(and cs
(implies-in-env? (lexical-env)
(-is-type obj S)
@ -544,10 +550,10 @@
;; constrain *each* element of es to be below T, and then combine the constraints
[((BaseUnion-bases: es) T)
(define cs (for/list/fail ([e (in-list es)]) (cg e T)))
(define cs (for/list/fail ([e (in-list es)]) (cg e T obj)))
(and cs (cset-meet* (cons empty cs)))]
[((Union-all: es) T)
(define cs (for/list/fail ([e (in-list es)]) (cg e T)))
(define cs (for/list/fail ([e (in-list es)]) (cg e T obj)))
(and cs (cset-meet* (cons empty cs)))]
[(_ (Bottom:)) no-cset]
@ -558,16 +564,16 @@
[(S (Union-all: es))
(cset-join
(for*/list ([e (in-list es)]
[v (in-value (cg S e))]
[v (in-value (cg S e obj))]
#:when v)
v))]
;; from define-new-subtype
[((Distinction: nm1 id1 S) (app resolve (Distinction: nm2 id2 T)))
#:when (and (equal? nm1 nm2) (equal? id1 id2))
(cg S T)]
(cg S T obj)]
[((Distinction: _ _ S) T)
(cg S T)]
(cg S T obj)]
;; two structs with the same name
;; just check pairwise on the fields
@ -596,17 +602,23 @@
[((Name: n _ #t) (Name: n* _ #t))
(if (free-identifier=? n n*)
empty ;; just succeed now
(% cg (resolve-once S) (resolve-once T)))]
(let ([S (resolve-once S)]
[T (resolve-once T)])
(and S T (cg S T obj))))]
;; pairs are pointwise
[((Pair: a b) (Pair: a* b*))
(% cset-meet (cg a a*) (cg b b*))]
(% cset-meet
(cg a a* (-car-of obj))
(cg b b* (-cdr-of obj)))]
;; sequences are covariant
[((Sequence: ts) (Sequence: ts*))
(cgen/list context ts ts*)]
[((Listof: t) (Sequence: (list t*)))
(cg t t*)]
[((Pair: t1 t2) (Sequence: (list t*)))
(% cset-meet (cg t1 t*) (cg t2 (-lst t*)))]
(% cset-meet
(cg t1 t* (-car-of obj))
(cg t2 (-lst t*) (-cdr-of obj)))]
[((MListof: t) (Sequence: (list t*)))
(cg t t*)]
;; To check that mutable pair is a sequence we check that the cdr is
@ -659,9 +671,11 @@
;; resolve applications
[((App: _ _) _)
(% cg (resolve-once S) T)]
(let ([S (resolve-once S)])
(and S (cg S T obj)))]
[(_ (App: _ _))
(% cg S (resolve-once T))]
(let ([T (resolve-once T)])
(and T (cg S T obj)))]
;; If the struct names don't match, try the parent of S
;; Needs to be done after App and Mu in case T is actually the current struct
@ -850,16 +864,21 @@
;; expected-cset : a cset representing the expected type, to meet early and
;; keep the number of constraints in check. (empty by default)
;; produces a cset which determines a substitution that makes the Ss subtypes of the Ts
(define/cond-contract (cgen/list context S T
(define/cond-contract (cgen/list context S T [objs '()]
#:expected-cset [expected-cset (empty-cset '() '())])
((context? (listof Values/c) (listof Values/c)) (#:expected-cset cset?) . ->* . (or/c cset? #f))
(->* (context? (listof Values/c) (listof Values/c))
((listof (or/c #f OptObject?))
#:expected-cset cset?)
(or/c cset? #f))
(and (= (length S) (length T))
(% cset-meet*
(for/list/fail ([s (in-list S)] [t (in-list T)])
(for/list/fail ([s (in-list S)]
[t (in-list T)]
[obj (in-list/rest objs #f)])
;; We meet early to prune the csets to a reasonable size.
;; This weakens the inference a bit, but sometimes avoids
;; constraint explosion.
(% cset-meet (cgen context s t) expected-cset)))))
(% cset-meet (cgen context s t obj) expected-cset)))))
@ -874,22 +893,26 @@
;; just return a boolean result
(define infer
(let ()
(define/cond-contract (infer X Y S T R [expected #f] #:multiple? [multiple-substitutions? #f])
(define/cond-contract (infer X Y S T R [expected #f]
#:multiple? [multiple-substitutions? #f]
#:objs [objs '()])
(((listof symbol?) (listof symbol?) (listof Type?) (listof Type?)
(or/c #f Values/c ValuesDots?))
((or/c #f Values/c AnyValues? ValuesDots?)
#:multiple? boolean?)
#:multiple? boolean?
#:objs (listof OptObject?))
. ->* . (or/c boolean?
substitution/c
(cons/c substitution/c
(listof substitution/c))))
(define ctx (context null X Y ))
(define ctx (context null X Y))
(define expected-cset
(if expected
(cgen ctx R expected)
(empty-cset '() '())))
(and expected-cset
(let* ([cs (cgen/list ctx S T #:expected-cset expected-cset)]
(let* ([cs (cgen/list ctx S T objs
#:expected-cset expected-cset)]
[cs* (% cset-meet cs expected-cset)])
(and cs* (cond
[R (substs-gen cs* X Y R multiple-substitutions?)]
@ -898,17 +921,20 @@
infer)) ;to export a variable binding and not syntax
;; like infer, but T-var is the vararg type:
(define (infer/vararg X Y S T T-var R [expected #f])
(define (infer/vararg X Y S T T-var R [expected #f]
#:objs [objs '()])
(define new-T (if T-var (list-extend S T T-var) T))
(and ((length S) . >= . (length T))
(infer X Y S new-T R expected)))
(infer X Y S new-T R expected #:objs objs)))
;; like infer, but dotted-var is the bound on the ...
;; and T-dotted is the repeated type
(define (infer/dots X dotted-var S T T-dotted R must-vars #:expected [expected #f])
(define (infer/dots X dotted-var S T T-dotted R must-vars
#:expected [expected #f]
#:objs [objs (map (λ (_) #f) S)])
(early-return
(define short-S (take S (length T)))
(define rest-S (drop S (length T)))
(define-values (short-S rest-S) (split-at S (length T)))
(define-values (short-objs rest-objs) (split-at objs (length T)))
;; Generate a new type corresponding to T-dotted for every extra arg.
(define-values (new-vars new-Ts)
(generate-dbound-prefix dotted-var T-dotted (length rest-S) #f))
@ -922,8 +948,12 @@
#:return-unless expected-cset #f
(define cs (% move-vars-to-dmap
(% cset-meet
(cgen/list ctx short-S (map subst T) #:expected-cset expected-cset)
(cgen/list ctx rest-S new-Ts #:expected-cset expected-cset))
(cgen/list ctx short-S (map subst T)
short-objs
#:expected-cset expected-cset)
(cgen/list ctx rest-S new-Ts
rest-objs
#:expected-cset expected-cset))
dotted-var new-vars))
#:return-unless cs #f
(define m (cset-meet cs expected-cset))

6
typed-racket-lib/typed-racket/infer/intersect.rkt
View File

@ -11,7 +11,7 @@
(export intersect^)
(define ((intersect-types additive?) t1 t2 #:obj [obj -empty-obj])
(define ((intersect-types additive?) t1 t2 [obj -empty-obj])
(cond
;; we dispatch w/ Error first, because it behaves in
;; strange ways (e.g. it is ⊤ and ⊥ w.r.t subtyping) and
@ -32,8 +32,8 @@
[(_ _) #:when (not (overlap? t1 t2)) -Bottom]
;; already a subtype
[(_ _) #:when (subtype t1 t2 #:obj obj) t1]
[(_ _) #:when (subtype t2 t1 #:obj obj) t2]
[(_ _) #:when (subtype t1 t2 obj) t1]
[(_ _) #:when (subtype t2 t1 obj) t2]
;; polymorphic intersect

15
typed-racket-lib/typed-racket/infer/signatures.rkt
View File

@ -21,8 +21,8 @@
[cond-contracted c-meet ((c? c?) (symbol?) . ->* . (or/c #f c?))]))
(define-signature intersect^
([cond-contracted intersect ((Type? Type?) (#:obj OptObject?) . ->* . Type?)]
[cond-contracted restrict ((Type? Type?) (#:obj OptObject?) . ->* . Type?)]))
([cond-contracted intersect ((Type? Type?) (OptObject?) . ->* . Type?)]
[cond-contracted restrict ((Type? Type?) (OptObject?) . ->* . Type?)]))
(define-signature infer^
([cond-contracted infer ((;; variables from the forall
@ -38,7 +38,8 @@
;; optional expected type
((or/c #f Values/c AnyValues? ValuesDots?)
;; optional multiple substitutions?
#:multiple? boolean?)
#:multiple? boolean?
#:objs (listof OptObject?))
. ->* . any)]
[cond-contracted infer/vararg ((;; variables from the forall
(listof symbol?)
@ -53,7 +54,9 @@
;; range
(or/c #f Values/c ValuesDots?))
;; [optional] expected type
((or/c #f Values/c AnyValues? ValuesDots?)) . ->* . any)]
((or/c #f Values/c AnyValues? ValuesDots?)
#:objs (listof OptObject?))
. ->* . any)]
[cond-contracted infer/dots (((listof symbol?)
symbol?
(listof Values/c)
@ -61,4 +64,6 @@
Values/c
(or/c Values/c ValuesDots?)
(listof symbol?))
(#:expected (or/c #f Values/c AnyValues? ValuesDots?)) . ->* . any)]))
(#:expected (or/c #f Values/c AnyValues? ValuesDots?)
#:objs (listof OptObject?))
. ->* . any)]))

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

@ -31,6 +31,7 @@
genobj
make-obj-seq
obj-seq-next
scale-obj
(rename-out [make-LExp* make-LExp]
[make-LExp raw-make-LExp])
(all-from-out "fme-utils.rkt"))
@ -283,18 +284,20 @@
(cond
[(or (Empty? o1) (Empty? o2)) -empty-obj]
[(and (LExp? o1) (constant-LExp? o1))
=> (scale-obj o2)]
=> (λ (n) (scale-obj n o2))]
[(and (LExp? o2) (constant-LExp? o2))
=> (scale-obj o1)]
=> (λ (n) (scale-obj n o1))]
[else -empty-obj]))
(define ((scale-obj o) c)
(match o
[(? Path?) (-lexp (list c o))]
(define/cond-contract (scale-obj n obj)
(-> exact-integer? OptObject? OptObject?)
(match obj
[(? Path?) (-lexp (list n obj))]
[(LExp: const terms)
;; scaling doesn't modify which objects are in the LExp! =)
;; just constants & coefficients
(make-LExp* (* c const) (terms-scale terms c))]))
(make-LExp* (* n const) (terms-scale terms n))]
[(Empty:) -empty-obj]))

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

@ -1558,11 +1558,21 @@
(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)]))

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

@ -86,10 +86,10 @@
(type-mismatch p2 p1 "mismatch in proposition"))
(tc-any-results (fix-props p2 p1))]
[((or (tc-results: _ (list (PropSet: fs+ fs-) ...) _)
(tc-results: _ (list (PropSet: fs+ fs-) ...) _ _ _))
[((or (tc-results: _ (list (PropSet: ps+ ps-) ...) _)
(tc-results: _ (list (PropSet: ps+ ps-) ...) _ _ _))
(tc-any-results: p2))
(define merged-prop (apply -and (map -or fs+ fs-)))
(define merged-prop (apply -and (map -or ps+ ps-)))
(unless (prop-better? merged-prop p2)
(type-mismatch p2 merged-prop "mismatch in proposition"))
(tc-any-results (fix-props p2 merged-prop))]
@ -97,7 +97,7 @@
[((tc-result1: t1 p1 o1) (tc-result1: t2 p2 o2))
(cond
[(not (subtype t1 t2))
[(not (subtype t1 t2 o1))
(expected-but-got t2 t1)]
[(and (not (prop-set-better? p1 p2))
(object-better? o1 o2))
@ -124,48 +124,53 @@
[((tc-results: t1 p1 o1 dty1 dbound)
(tc-results: t2 (list (or #f (PropSet: (TrueProp:) (TrueProp:))) ...)
(list (or #f (Empty:)) ...) dty2 dbound))
(list (or #f (Empty:)) ...) dty2 dbound))
(cond
[(= (length t1) (length t2))
(unless (andmap subtype t1 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)])
(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)
(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)])
(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:)) ...)))
(list (or #f (Empty:)) ...)))
(unless (= (length t1) (length t2))
(value-mismatch expected tr1))
(unless (for/and ([t (in-list t1)] [s (in-list t2)]) (subtype t s))
(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)]) (subtype t s))
(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)) (=> continue)
(if (= (length t1) (length t2))
(continue)
(value-mismatch expected tr1))
[((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?))

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

@ -38,7 +38,7 @@
"expected at least" (length dom)
"given" (length t-a)
#:delayed? #t)])
(for ([dom-t (if rest (in-sequence-forever dom rest) (in-list dom))]
(for ([dom-t (if rest (in-list/rest dom rest) (in-list dom))]
[a (in-syntax args-stx)]
[arg-t (in-list t-a)])
(parameterize ([current-orig-stx a]) (check-below arg-t dom-t))))
@ -48,8 +48,8 @@
(let-values
([(o-a t-a) (for/lists (os ts)
([_ (in-range dom-count)]
[oa (in-sequence-forever (in-list o-a) -empty-obj)]
[ta (in-sequence-forever (in-list t-a) Univ)])
[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

8
typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
View File

@ -88,7 +88,7 @@
;; vector-ref on het vectors
(pattern (~and form ((~or vector-ref unsafe-vector-ref unsafe-vector*-ref) vec:expr index:expr))
(match (single-value #'vec)
[(tc-result1: (and vec-t (app resolve (HeterogeneousVector: es))))
[(tc-result1: (and vec-t (app resolve (Is-a: (HeterogeneousVector: es)))))
(tc/hetero-ref #'index es vec-t "vector")]
[v-ty (tc/app-regular #'form expected)]))
;; unsafe struct-set!
@ -100,17 +100,17 @@
;; vector-set! on het vectors
(pattern (~and form ((~or vector-set! unsafe-vector-set! unsafe-vector*-set!) v:expr index:expr val:expr))
(match (single-value #'v)
[(tc-result1: (and vec-t (app resolve (HeterogeneousVector: es))))
[(tc-result1: (and vec-t (app resolve (Is-a: (HeterogeneousVector: es)))))
(tc/hetero-set! #'index es #'val vec-t "vector")]
[v-ty (tc/app-regular #'form expected)]))
(pattern (~and form ((~or vector-immutable vector) args:expr ...))
(match expected
[(tc-result1: (app resolve (Vector: t)))
[(tc-result1: (app resolve (Is-a: (Vector: t))))
(ret (make-HeterogeneousVector
(for/list ([e (in-syntax #'(args ...))])
(tc-expr/check e (ret t))
t)))]
[(tc-result1: (app resolve (HeterogeneousVector: ts)))
[(tc-result1: (app resolve (Is-a: (HeterogeneousVector: ts))))
(cond
[(= (length ts) (syntax-length #'(args ...)))
(ret

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

@ -86,16 +86,21 @@
(map single-value args*)]
[(Function:
(app matching-arities
(list (arr: doms ranges rests drests _) ..1)))
(define matching-domains
(in-values-sequence
(apply in-parallel
(for/list ((dom (in-list doms)) (rest (in-list rests)))
(in-sequences (in-list dom) (in-cycle (in-value rest)))))))
(for/list ([a (in-list args*)] [types matching-domains])
(match-define (cons t ts) types)
(if (for/and ((t2 (in-list ts))) (equal? t t2))
(tc-expr/check a (ret t))
(single-value a)))]
(list (arr: doms _ rests _ _) ..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
(for/list ([arg-stx (in-list args*)]
[arg-idx (in-naturals)])
(define dom-ty (list-ref/default (car doms)
arg-idx
(car rests)))
(cond
[(for/and ([dom (in-list doms)]
[rest (in-list rests)])
(equal? dom-ty
(list-ref/default dom arg-idx rest)))
(tc-expr/check arg-stx (ret dom-ty))]
[else (single-value arg-stx)]))]
[_ (map single-value args*)]))
(tc/funapp #'f #'args f-ty arg-tys expected))]))

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

@ -51,7 +51,7 @@
(loop ps negs (append new-props new) (env-set-id-type Γ x new-t))]))]
[(TypeProp: obj pt)
(let ([t (lookup-obj-type/lexical obj Γ #:fail (λ (_) Univ))])
(define new-t (intersect t pt #:obj obj))
(define new-t (intersect t pt obj))
(cond
[(Bottom? new-t) #f]
[(equal? t new-t) (loop ps negs new Γ)]

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

@ -21,12 +21,14 @@
racket/extflonum
;; Needed for current implementation of typechecking letrec-syntax+values
(for-template (only-in racket/base list letrec-values
+ * < <= = >= >)
+ - * < <= = >= > add1 sub1 modulo
min max vector-length random)
;; see tc-app-contracts.rkt
racket/contract/private/provide)
(for-label (only-in '#%paramz [parameterization-key pz:pk])
(only-in racket/private/class-internal find-method/who)))
(only-in racket/private/class-internal find-method/who))
(for-syntax racket/base racket/syntax))
(import tc-if^ tc-lambda^ tc-app^ tc-let^ tc-send^ check-subforms^ tc-literal^
check-class^ check-unit^ tc-expression^)
@ -398,7 +400,7 @@
[(HeterogeneousVector: ts)
(make-HeterogeneousVector
(for/list ([x (in-list xs)]
[t (in-sequence-forever (in-list ts) #f)])
[t (in-list/rest ts #f)])
(cond-check-below (find-stx-type x t) t)))]
[_ (make-HeterogeneousVector (for/list ([x (in-list xs)])
(generalize (find-stx-type x #f))))])]
@ -426,20 +428,32 @@
;; adds linear info for the following operations:
;; + * < <= = >= >
;; when the arguments are integers w/ objects
;; a lot of the content in this function should eventually
;; just be moved to the actual types of the respective
;; racket identifiers, but in an effort to move progress forward
;; and not break programs currently typechecking, this more
;; explicit, hard-coded helper will do (i.e. some of these functions
;; currently have extremely large types in TR -- modifying their
;; type is not always trivial)
(define (add-applicable-linear-info form result)
;; class to recognize expressions that typecheck at a subtype of -Int
;; and whose object is non-empty
(define-syntax-class int/obj
(define-syntax-class (t/obj type)
#:attributes (obj)
(pattern e:expr
#:do [(define o
(match (type-of #'e)
[(tc-result1: t _ (? Object? o))
#:when (subtype t -Int)
#:when (subtype t type)
o]
[_ #f]))]
#:fail-unless o "not an integer with a non-empty object"
#:fail-unless o (format "not a ~a expr with a non-empty object" type)
#:attr obj o))
(define-syntax (obj stx)
(syntax-case stx ()
[(_ e)
(with-syntax ([e* (format-id #'e "~a.obj" (syntax->datum #'e))])
(syntax/loc #'e (attribute e*)))]))
;; class to recognize int comparisons and associate their
;; internal TR prop constructors
(define-syntax-class int-comparison
@ -474,32 +488,90 @@
;; inspect the function appplication to see if it is a linear
;; integer compatible form we want to enrich with info when
;; #:with-linear-integer-arithmetic is specified by the user
(syntax-parse form
[(#%plain-app (~literal *) e1:int/obj e2:int/obj)
(match result
[(tc-result1: t ps _)
(define o1*o2 (-obj* (attribute e1.obj) (attribute e2.obj)))
(match result
[(tc-result1: ret-t ps _)
(syntax-parse form
;; *
[(#%plain-app (~literal *) (~var e1 (t/obj -Int)) (~var es (t/obj -Int)) ...)
(define product-obj (apply -obj* (obj e1) (obj es)))
(cond
[(Object? o1*o2)
(ret (-refine/fresh x t (-eq (-lexp x) o1*o2))
[(Object? product-obj)
(ret (-refine/fresh x ret-t (-eq (-lexp x) product-obj))
ps
o1*o2)]
product-obj)]
[else result])]
[_ result])]
[(#%plain-app (~literal +) e:int/obj es:int/obj ...)
(match result
[(tc-result1: t ps _)
(define l (apply -lexp (attribute e.obj) (attribute es.obj)))
(ret (-refine/fresh x t (-eq (-lexp x) l))
;; +
[(#%plain-app (~literal +) (~var e (t/obj -Int)) (~var es (t/obj -Int)) ...)
(define l (apply -lexp (obj e) (obj es)))
(ret (-refine/fresh x ret-t (-eq (-lexp x) l))
ps
l)])]
[(#%plain-app comp:int-comparison
e1:int/obj
e2:int/obj
es:int/obj ...)
(define p (apply -and (comparison-props (attribute comp.constructor)
(attribute e1.obj)
(attribute e2.obj)
(attribute es.obj))))
(add-p/not-p result p)]
l)]
;; -
[(#%plain-app (~literal -) (~var e (t/obj -Int)) (~var es (t/obj -Int)) ...)
(define l (apply -lexp
(obj e)
(for/list ([o (in-list (obj es))])
(scale-obj -1 o))))
(ret (-refine/fresh x ret-t (-eq (-lexp x) l))
ps
l)]
;; add1
[(#%plain-app (~literal add1) (~var e (t/obj -Int)))
(define l (-lexp 1 (obj e)))
(ret (-refine/fresh x ret-t (-eq (-lexp x) l))
ps
l)]
;; sub1
[(#%plain-app (~literal sub1) (~var e (t/obj -Int)))
(define l (-lexp -1 (obj e)))
(ret (-refine/fresh x ret-t (-eq (-lexp x) l))
ps
l)]
;; modulo
[(#%plain-app (~literal modulo) (~var e1 (t/obj -Int)) (~var e2 (t/obj -Nat)))
(ret (-refine/fresh x ret-t (-lt (-lexp x) (obj e2)))
ps
-empty-obj)]
;; max
[(#%plain-app (~literal max) (~var e1 (t/obj -Int)) (~var es (t/obj -Int)) ...)
(ret (-refine/fresh x ret-t
(apply -and (let ([l (-lexp x)])
(for/list ([o (in-list (cons (obj e1) (obj es)))])
(-geq l o)))))
ps
-empty-obj)]
;; min
[(#%plain-app (~literal min) (~var e1 (t/obj -Int)) (~var es (t/obj -Int)) ...)
(ret (-refine/fresh x ret-t
(apply -and (let ([l (-lexp x)])
(for/list ([o (in-list (cons (obj e1) (obj es)))])
(-leq l o)))))
ps
-empty-obj)]
;; random
[(#%plain-app (~literal random) (~var e1 (t/obj -Int)))
(ret (-refine/fresh x ret-t (-lt (-lexp x) (obj e1)))
ps
-empty-obj)]
[(#%plain-app (~literal random) (~var e1 (t/obj -Int)) (~var e2 (t/obj -Int)))
(ret (-refine/fresh x ret-t (-and (-leq (obj e1) (-lexp x))
(-lt (-lexp x) (obj e2))))
ps
-empty-obj)]
;; vector-length
[(#%plain-app (~literal vector-length) (~var e1 (t/obj -VectorTop)))
(define l (-vec-len-of (obj e1)))
(ret (-refine/fresh x ret-t (-eq (-lexp x) l))
ps
l)]
[(#%plain-app comp:int-comparison
(~var e1 (t/obj -Int))
(~var e2 (t/obj -Int))
(~var es (t/obj -Int)) ...)
(define p (apply -and (comparison-props (attribute comp.constructor)
(obj e1)
(obj e2)
(obj es))))
(add-p/not-p result p)]
[_ result])]
[_ result]))

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

@ -111,13 +111,20 @@
[drest
(infer/dots
fixed-vars dotted-var argtys dom (car drest) rng (fv rng)
#:expected (and expected (tc-results->values expected)))]
#: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)))]
(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)))])))
[else (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)]
@ -141,7 +148,8 @@
(let ([rng (subst-dom-objs argtys argobjs rng)])
(extend-tvars vars
(infer/vararg vars null argtys dom rest rng
(and expected (tc-results->values expected)))))
(and expected (tc-results->values expected))
#:objs argobjs)))
#:function-type f-type
#:args-results args-res
#:expected expected)]

37
typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
View File

@ -31,7 +31,7 @@
(pattern (~and i (~or :number :str :bytes :char))
#:fail-unless expected #f
#:fail-unless (let ([n (syntax-e #'i)])
(subtype (-val n) expected #:obj (if (exact-integer? n) (-lexp n) -empty-obj))) #f))
(subtype (-val n) expected (if (exact-integer? n) (-lexp n) -empty-obj))) #f))
(syntax-parse v-stx
[i:exp expected]
[i:boolean (-val (syntax-e #'i))]
@ -113,21 +113,26 @@
[t
(-pair (tc-literal #'i) (tc-literal #'r))])]
[(~var i (3d vector?))
(match (and expected (resolve (intersect expected -VectorTop)))
[(Vector: t)
(make-Vector
(check-below
(apply Un
(for/list ([l (in-vector (syntax-e #'i))])
(tc-literal l t)))
(define vec-val (syntax-e #'i))
(define vec-ty
(match (and expected (resolve (intersect expected -VectorTop)))
[(Is-a: (Vector: t))
(make-Vector
(check-below
(apply Un (for/list ([l (in-vector vec-val)])
(tc-literal l t)))
t))]
[(HeterogeneousVector: ts)
(make-HeterogeneousVector
(for/list ([l (in-vector (syntax-e #'i))]
[t (in-sequence-forever (in-list ts) #f)])
(cond-check-below (tc-literal l t) t)))]
[_ (make-HeterogeneousVector (for/list ([l (in-vector (syntax-e #'i))])
(generalize (tc-literal l #f))))])]
[(Is-a: (HeterogeneousVector: ts))
(make-HeterogeneousVector
(for/list ([l (in-vector (syntax-e #'i))]
[t (in-list/rest ts #f)])
(cond-check-below (tc-literal l t) t)))]
[_ (make-HeterogeneousVector (for/list ([l (in-vector (syntax-e #'i))])
(generalize (tc-literal l #f))))]))
(if (with-linear-integer-arithmetic?)
(-refine/fresh v vec-ty (-eq (-lexp (vector-length vec-val))
(-vec-len-of (-id-path v))))
vec-ty)]
[(~var i (3d hash?))
(match (and expected (resolve (intersect expected -HashtableTop)))
[(Hashtable: k v)
@ -149,7 +154,7 @@
(define (tc-prefab struct-inst expected)
(define expected-ts
(match (and expected (resolve expected))
[(Prefab: _ ts) (in-sequence-forever (in-list ts) #f)]
[(Prefab: _ ts) (in-list/rest ts #f)]
[_ (in-cycle (in-value #f))]))
(define key (prefab-struct-key struct-inst))
(define struct-vec (struct->vector struct-inst))

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

@ -38,11 +38,11 @@
;; 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 (map (λ (_) Univ) os)])
(define (values->tc-results v os [ts '()])
(define targets
(for/list ([o (in-list os)]
[arg (in-naturals)]
[t (in-list ts)])
[t (in-list/rest ts Univ)])
(list (cons 0 arg) o t)))
(define res
(match v
@ -177,7 +177,7 @@
(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 obj))
(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]
@ -197,8 +197,8 @@
(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 obj))
(define new-neg-obj-ty (restrict neg-obj-ty inner-obj-ty-at-flds #:obj obj))
(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]

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

@ -11,9 +11,27 @@
(provide Listof: List: MListof: AnyPoly: AnyPoly-names: Function/arrs:
SimpleListof: SimpleMListof:
PredicateProp:
Val-able:)
Val-able:
Is-a:)
;; matches types that are exactly the pattern,
;; or that are an intersection type of some kind where
;; exactly 1 of the types in the intersection is of the type
(define-match-expander Is-a:
(lambda (stx)
(syntax-parse stx
[(_ pat)
(syntax/loc stx
(or pat
(Intersection: (or (list pat)
(app (λ (ts) (filter (match-lambda
[pat #t]
[_ #f])
ts))
(list pat)))
_)))])))
;; some types used to be represented by a Value rep,
;; but are now represented by a Base rep. This function
;; helps us recover the singleton values for those types.
@ -27,15 +45,14 @@
[(== -One) (box-immutable 1)]
[_ #f]))
;; matches types that correspond to singleton values
(define-match-expander Val-able:
(lambda (stx)
(syntax-parse stx
[(_ pat)
(syntax/loc stx
(or (Value: pat)
(app Base->val? (box pat))
(Intersection: (list (or (Value: pat)
(app Base->val? (box pat)))) _)))])))
(Is-a: (or (Value: pat)
(app Base->val? (box pat)))))])))
(define-match-expander Listof:
(lambda (stx)

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

@ -67,16 +67,15 @@
;; atomic-contradiction?: Prop? Prop? -> boolean?
;; Returns true if the AND of the two props is equivalent to FalseProp
(define (atomic-contradiction? p1 p2)
(match* (p1 p2)
[((TypeProp: o1 t1) (NotTypeProp: o2 t2))
(and (eq? o1 o2) (subtype t1 t2 #:obj o1))]
[((NotTypeProp: o2 t2) (TypeProp: o1 t1))
(and (eq? o1 o2) (subtype t1 t2 #:obj o1))]
[((? LeqProp?) (? LeqProp?)) (contradictory-Leqs? p1 p2)]
[((FalseProp:) _) #t]
[(_ (FalseProp:)) #t]
[(_ _) #f]))
(define/match (atomic-contradiction? p1 p2)
[((TypeProp: o1 t1) (NotTypeProp: o2 t2))
(and (eq? o1 o2) (subtype t1 t2 o1))]
[((NotTypeProp: o2 t2) (TypeProp: o1 t1))
(and (eq? o1 o2) (subtype t1 t2 o1))]
[((? LeqProp?) (? LeqProp?)) (contradictory-Leqs? p1 p2)]
[((FalseProp:) _) #t]
[(_ (FalseProp:)) #t]
[(_ _) #f])
;; do pes1 and pes2 share a common suffix and,
@ -129,75 +128,72 @@
;; like atomic-contradiction? but it tries a little
;; harder, reasoning about how paths overlap
(define (contradiction? p1 p2)
(match* (p1 p2)
[((FalseProp:) _) #t]
[(_ (FalseProp:)) #t]
[((TypeProp: o t1) (NotTypeProp: o t2)) (subtype t1 t2 #:obj o)]
[((NotTypeProp: o t2) (TypeProp: o t1)) (subtype t1 t2 #:obj o)]
[((? LeqProp?) (? LeqProp?)) (contradictory-Leqs? p1 p2)]
[((TypeProp: (Path: pes1 x1) t1)
(TypeProp: (Path: pes2 x2) t2))
#:when (name-ref=? x1 x2)
(updates/pos-to-bot? pes1 t1 pes2 t2)]
[((TypeProp: (Path: pes1 x1) t1)
(NotTypeProp: (Path: pes2 x2) t2))
#:when (name-ref=? x1 x2)
(updates/neg-to-bot? pes1 t1 pes2 t2)]
[((NotTypeProp: (Path: pes2 x2) t2)
(TypeProp: (Path: pes1 x1) t1))
#:when (name-ref=? x1 x2)
(updates/neg-to-bot? pes1 t1 pes2 t2)]
[(_ _) #f]))
(define/match (contradiction? p1 p2)
[((FalseProp:) _) #t]
[(_ (FalseProp:)) #t]
[((TypeProp: o t1) (NotTypeProp: o t2)) (subtype t1 t2 o)]
[((NotTypeProp: o t2) (TypeProp: o t1)) (subtype t1 t2 o)]
[((? LeqProp?) (? LeqProp?)) (contradictory-Leqs? p1 p2)]
[((TypeProp: (Path: pes1 x1) t1)
(TypeProp: (Path: pes2 x2) t2))
#:when (name-ref=? x1 x2)
(updates/pos-to-bot? pes1 t1 pes2 t2)]
[((TypeProp: (Path: pes1 x1) t1)
(NotTypeProp: (Path: pes2 x2) t2))
#:when (name-ref=? x1 x2)
(updates/neg-to-bot? pes1 t1 pes2 t2)]
[((NotTypeProp: (Path: pes2 x2) t2)
(TypeProp: (Path: pes1 x1) t1))
#:when (name-ref=? x1 x2)
(updates/neg-to-bot? pes1 t1 pes2 t2)]
[(_ _) #f])
;; atomic-complement?: Prop? Prop? -> boolean?
;; Returns true if the OR of the two props is equivalent to Top
(define (atomic-complement? p1 p2)
(match* (p1 p2)
[((TypeProp: o1 t1) (NotTypeProp: o2 t2))
(and (eq? o1 o2) (subtype t2 t1 #:obj o1))]
[((NotTypeProp: o2 t2) (TypeProp: o1 t1))
(and (eq? o1 o2) (subtype t2 t1 #:obj o1))]
[((? LeqProp?) (? LeqProp?)) (complementary-Leqs? p1 p2)]
[((TrueProp:) _) #t]
[(_ (TrueProp:)) #t]
[(_ _) #f]))
(define/match (atomic-complement? p1 p2)
[((TypeProp: o1 t1) (NotTypeProp: o2 t2))
(and (eq? o1 o2) (subtype t2 t1 o1))]
[((NotTypeProp: o2 t2) (TypeProp: o1 t1))
(and (eq? o1 o2) (subtype t2 t1 o1))]
[((? LeqProp?) (? LeqProp?)) (complementary-Leqs? p1 p2)]
[((TrueProp:) _) #t]
[(_ (TrueProp:)) #t]
[(_ _) #f])
;; does p imply q? (but only directly/simply)
;; NOTE: because Ors and Atomic props are
;; interned, we use eq? and memq
(define (atomic-implies? p q)
(match* (p q)
;; reflexivity
[(_ _) #:when (or (eq? p q)
(TrueProp? q)
(FalseProp? p)) #t]
;; ps ⊆ qs ?
[((OrProp: ps) (OrProp: qs))
(and (for/and ([p (in-list ps)])
(memq p qs))
#t)]
;; p ∈ qs ?
[(p (OrProp: qs)) (and (memq p qs) #t)]
;; q ∈ ps ?
[((AndProp: ps) q) (or (equal? p q) (and (memq q ps) #t))]
;; t1 <: t2 ?
[((TypeProp: o1 t1)
(TypeProp: o2 t2))
(and (eq? o1 o2) (subtype t1 t2 #:obj o1))]
;; t2 <: t1 ?
[((NotTypeProp: o1 t1)
(NotTypeProp: o2 t2))
(and (eq? o1 o2) (subtype t2 t1 #:obj o1))]
;; t1 ∩ t2 = ∅ ?
[((TypeProp: o1 t1)
(NotTypeProp: o2 t2))
(and (eq? o1 o2) (not (overlap? t1 t2)))]
[((? LeqProp? p) (? LeqProp? q))
(Leq-implies-Leq? p q)]
;; otherwise we give up
[(_ _) #f]))
(define/match (atomic-implies? p q)
;; reflexivity
[(_ _) #:when (or (eq? p q)
(TrueProp? q)
(FalseProp? p)) #t]
;; ps ⊆ qs ?
[((OrProp: ps) (OrProp: qs))
(and (for/and ([p (in-list ps)])
(memq p qs))
#t)]
;; p ∈ qs ?
[(p (OrProp: qs)) (and (memq p qs) #t)]
;; q ∈ ps ?
[((AndProp: ps) q) (or (equal? p q) (and (memq q ps) #t))]
;; t1 <: t2 ?
[((TypeProp: o1 t1)
(TypeProp: o2 t2))
(and (eq? o1 o2) (subtype t1 t2 o1))]
;; t2 <: t1 ?
[((NotTypeProp: o1 t1)
(NotTypeProp: o2 t2))
(and (eq? o1 o2) (subtype t2 t1 o1))]
;; t1 ∩ t2 = ∅ ?
[((TypeProp: o1 t1)
(NotTypeProp: o2 t2))
(and (eq? o1 o2) (not (overlap? t1 t2)))]
[((? LeqProp? p) (? LeqProp? q))
(Leq-implies-Leq? p q)]
;; otherwise we give up
[(_ _) #f])
(define (implies? p q)
(FalseProp? (-and p (negate-prop q))))
@ -227,8 +223,8 @@
(match props
[(or (list) (list _)) props]
[_
(define tf-map (make-hash))
(define ntf-map (make-hash))
(define tf-map (make-hasheq))
(define ntf-map (make-hasheq))
;; consolidate type info and separate out other props
(define-values (leqs others)
@ -246,9 +242,9 @@
[_ (values leqs (cons prop others))])))
;; convert consolidated types into props and gather everything
(define raw-results
(append (for/list ([(k v) (in-hash tf-map)])
(append (for/list ([(k v) (in-mutable-hash tf-map)])
(-is-type k v))
(for/list([(k v) (in-hash ntf-map)])
(for/list([(k v) (in-mutable-hash ntf-map)])
(-not-type k v))
leqs
others))
@ -269,16 +265,15 @@
;; negate-prop: Prop? -> Prop?
;; Logically inverts a prop.
(define (negate-prop p)
(match p
[(? FalseProp?) -tt]
[(? TrueProp?) -ff]
[(TypeProp: o t) (-not-type o t)]
[(NotTypeProp: o t) (-is-type o t)]
[(AndProp: ps) (apply -or (map negate-prop ps))]
[(OrProp: ps) (apply -and (map negate-prop ps))]
[(LeqProp: lhs rhs)
(-leq (-lexp-add1 rhs) lhs)]))
(define/match (negate-prop p)
[((? FalseProp?)) -tt]
[((? TrueProp?)) -ff]
[((TypeProp: o t)) (-not-type o t)]
[((NotTypeProp: o t)) (-is-type o t)]
[((AndProp: ps)) (apply -or (map negate-prop ps))]
[((OrProp: ps)) (apply -and (map negate-prop ps))]
[((LeqProp: lhs rhs))
(-leq (-lexp-add1 rhs) lhs)])
;; -or
;; (listof Prop?) -> Prop?
@ -286,46 +281,55 @@
;; Smart 'normalizing' constructor for disjunctions. The result
;; will be a disjunction of only atomic propositions (i.e. a clause
;; in a CNF formula)
(define (-or . args)
(define mk
(match-lambda [(list) -ff]
[(list p) p]
[ps (make-OrProp ps)]))
(define (distribute args)
(define-values (ands others) (partition AndProp? args))
(if (null? ands)
(mk others)
(match-let ([(AndProp: elems) (car ands)])
(apply -and (for/list ([a (in-list elems)])
(apply -or a (append (cdr ands) others)))))))
(define (flatten-ors/remove-duplicates ps)
(let loop ([ps ps]
[result '()])
(match ps
[(cons p rst)
(match p
[(OrProp: ps*) (loop rst (append ps* result))]
[_ (loop rst (cons p result))])]
[_ (remove-duplicates result)])))
(let loop ([ps (flatten-ors/remove-duplicates args)]
[result null])
(match ps
[(cons cur rst)
(cond
;; trivial cases
[(TrueProp? cur) -tt]
[(FalseProp? cur) (loop rst result)]
;; is there a complementary case e.g. (ϕ ∨ ¬ϕ)? if so abort
[(for/or ([p (in-list rst)]) (atomic-complement? p cur)) -tt]
[(for/or ([p (in-list result)]) (atomic-complement? p cur)) -tt]
;; don't include 'cur' if its covered by another prop
[(for/or ([p (in-list rst)]) (atomic-implies? cur p))
(loop rst result)]
[(for/or ([p (in-list result)]) (atomic-implies? cur p))
(loop rst result)]
;; otherwise keep 'cur' in this disjunction
[else (loop rst (cons cur result))])]
[_ (distribute (compact result #t))])))
(define/match (-or . args)
;; specialize for trivial <=2 arg cases
[((list)) -ff]
[((list p)) p]
[((list p p)) p]
[((list (TrueProp:) p)) -tt]
[((list p (TrueProp:))) -tt]
[((list (FalseProp:) p)) p]
[((list p (FalseProp:))) p]
[(args)
(define mk
(match-lambda [(list) -ff]
[(list p) p]
[ps (make-OrProp ps)]))
(define (distribute args)
(define-values (ands others) (partition AndProp? args))
(if (null? ands)
(mk others)
(match-let ([(AndProp: elems) (car ands)])
(apply -and (for/list ([a (in-list elems)])
(apply -or a (append (cdr ands) others)))))))
(define (flatten-ors/remove-duplicates ps)
(let loop ([ps ps]
[result '()])
(match ps
[(cons p rst)
(match p
[(OrProp: ps*) (loop rst (append ps* result))]
[_ (loop rst (cons p result))])]
[_ (remove-duplicates result)])))
(let loop ([ps (flatten-ors/remove-duplicates args)]
[result null])
(match ps
[(cons cur rst)
(cond
;; trivial cases
[(TrueProp? cur) -tt]
[(FalseProp? cur) (loop rst result)]
;; is there a complementary case e.g. (ϕ ∨ ¬ϕ)? if so abort
[(for/or ([p (in-list rst)]) (atomic-complement? p cur)) -tt]
[(for/or ([p (in-list result)]) (atomic-complement? p cur)) -tt]
;; don't include 'cur' if its covered by another prop
[(for/or ([p (in-list rst)]) (atomic-implies? cur p))
(loop rst result)]
[(for/or ([p (in-list result)]) (atomic-implies? cur p))
(loop rst result)]
;; otherwise keep 'cur' in this disjunction
[else (loop rst (cons cur result))])]
[_ (distribute (compact result #t))]))])
;; -and
;; (listof Prop?) -> Prop?
@ -333,105 +337,111 @@
;; Smart 'normalizing' constructor for conjunctions. The result
;; will be a conjunction of only atomic propositions and disjunctions
;; (i.e. a CNF proposition)
(define (-and . args)
(define mk
(match-lambda [(list) -tt]
[(list p) p]
[ps (make-AndProp ps)]))
;; we remove duplicates and organize the props so that the
;; strongest ones come first (note: this includes considering
;; smaller ors before larger ors)
(define (flatten-ands/remove-duplicates/order ps)
(define ts '())
(define nts '())
(define ors (make-hash))
(define others '())
(let partition! ([ps ps])
(for ([p (in-list ps)])
(match p
[(? TypeProp?) (set! ts (cons p ts))]
[(? NotTypeProp?) (set! nts (cons p nts))]
[(OrProp: ps*) (hash-update! ors (length ps*) (λ (l) (cons p l)) '())]
[(AndProp: ps*) (partition! ps*)]
[_ (set! others (cons p others))])))
(define ors-smallest-to-largest
(append-map cdr (sort (hash->list ors)
(λ (len/ors1 len/ors2)
(< (car len/ors1) (car len/ors2))))))
(remove-duplicates (append ts nts others ors-smallest-to-largest) eq?))
(let loop ([ps (flatten-ands/remove-duplicates/order args)]
[result null])
(match ps
[(cons cur rst)
(cond
;; trivial cases
[(FalseProp? cur) -ff]
[(TrueProp? cur) (loop rst result)]
;; is there a contradition e.g. (ϕ ∧ ¬ϕ), if so abort
[(for/or ([p (in-list rst)]) (atomic-contradiction? p cur)) -ff]
[(for/or ([p (in-list result)]) (atomic-contradiction? p cur)) -ff]
;; don't include 'cur' if its implied by another prop
;; already in our result (this is why we order the props!)
[(for/or ([p (in-list result)]) (atomic-implies? p cur))
(loop rst result)]
;; otherwise keep 'cur' in this conjunction
[else (loop rst (cons cur result))])]
[_ (mk (compact result #f))])))
(define/match (-and . args)
;; specialize for trivial <=2 arg cases
[((list)) -tt]
[((list p)) p]
[((list p p)) p]
[((list (TrueProp:) p)) p]
[((list p (TrueProp:))) p]
[((list (FalseProp:) p)) -ff]
[((list p (FalseProp:))) -ff]
[(args)
(define mk
(match-lambda [(list) -tt]
[(list p) p]
[ps (make-AndProp ps)]))
;; we remove duplicates and organize the props so that the
;; strongest ones come first (note: this includes considering
;; smaller ors before larger ors)
(define (flatten-ands/remove-duplicates/order ps)
(define ts '())
(define nts '())
(define ors (make-hash))
(define others '())
(let partition! ([ps ps])
(for ([p (in-list ps)])
(match p
[(? TypeProp?) (set! ts (cons p ts))]
[(? NotTypeProp?) (set! nts (cons p nts))]
[(OrProp: ps*) (hash-update! ors (length ps*) (λ (l) (cons p l)) '())]
[(AndProp: ps*) (partition! ps*)]
[_ (set! others (cons p others))])))
(define ors-smallest-to-largest
(append-map cdr (sort (hash->list ors)
(λ (len/ors1 len/ors2)
(< (car len/ors1) (car len/ors2))))))
(remove-duplicates (append ts nts others ors-smallest-to-largest) eq?))
(let loop ([ps (flatten-ands/remove-duplicates/order args)]
[result null])
(match ps
[(cons cur rst)
(cond
;; trivial cases
[(FalseProp? cur) -ff]
[(TrueProp? cur) (loop rst result)]
;; is there a contradition e.g. (ϕ ∧ ¬ϕ), if so abort
[(for/or ([p (in-list rst)]) (atomic-contradiction? p cur)) -ff]
[(for/or ([p (in-list result)]) (atomic-contradiction? p cur)) -ff]
;; don't include 'cur' if its implied by another prop
;; already in our result (this is why we order the props!)
[(for/or ([p (in-list result)]) (atomic-implies? p cur))
(loop rst result)]
;; otherwise keep 'cur' in this conjunction
[else (loop rst (cons cur result))])]
[_ (mk (compact result #f))]))])
;; add-unconditional-prop: tc-results? Prop? -> tc-results?
;; 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 (add-unconditional-prop results prop)
(match results
[(tc-any-results: p) (tc-any-results (-and prop p))]
[(tc-results: ts (list (PropSet: ps+ ps-) ...) os)
(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)
(ret ts
(for/list ([p+ (in-list ps+)] [p- (in-list ps-)])
(-PS (-and prop p+) (-and prop p-)))
os
dty
dbound)]))
(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)])
;; 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 (add-unconditional-prop-all-args arr type)
(match arr
[(Function: (list (arr: dom rng rest drest kws)))
(match rng
[(Values: (list (Result: tp (PropSet: -true-prop -false-prop) 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))))])]))
(define/match (add-unconditional-prop-all-args arr type)
[((Function: (list (arr: dom rng rest drest kws))) type)
(match rng
[(Values: (list (Result: tp (PropSet: -true-prop -false-prop) 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))))])])
;; tc-results/c -> tc-results/c
(define (erase-props tc)
(match 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)]))
(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)])

6
typed-racket-lib/typed-racket/types/subtract.rkt
View File

@ -12,14 +12,14 @@
;; Type Type -> Type
;; conservatively calculates set subtraction
;; between the types (i.e. t - s)
(define (subtract t s #:obj [obj -empty-obj])
(define (subtract t s [obj -empty-obj])
(define s-mask (mask s))
(define result
(let recurse ([t t] [obj obj])
(define (sub t [obj -empty-obj]) (recurse t obj))
(match t
[_ #:when (disjoint-masks? (mask t) s-mask) t]
[_ #:when (subtype t s #:obj obj) -Bottom]
[_ #:when (subtype t s obj) -Bottom]
[(or (App: _ _) (? Name?))
;; must be different, since they're not subtypes
;; and n must refer to a distinct struct type
@ -43,5 +43,5 @@
[(Poly: vs b) (make-Poly vs (sub b) obj)]
[_ t])))
(cond
[(subtype t result #:obj obj) t]
[(subtype t result obj) t]
[else result]))

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

@ -26,7 +26,7 @@
(provide NameStruct:)
(provide/cond-contract
[subtype (->* (Type? Type?) (#:obj OptObject?) boolean?)]
[subtype (->* (Type? Type?) ((or/c #f OptObject?)) boolean?)]
[subresult (-> Result? Result? boolean?)]
[subval (-> SomeValues? SomeValues? boolean?)]
[type-equiv? (-> Type? Type? boolean?)]
@ -49,15 +49,8 @@
;; is t1 a subtype of t2?
;; type type -> boolean
(define (subtype t1 t2 #:obj [obj #f])
(and
(cond
[obj (subtype* (seen) t1 t2 obj)]
[else
(define-values (o os) (obj-seq-next (temp-objs)))
(parameterize ([temp-objs os])
(subtype* (seen) t1 t2 o))])
#t))
(define (subtype t1 t2 [obj #f])
(and (subtype* (seen) t1 t2 obj) #t))
;; is v1 a subval of v2?
@ -380,6 +373,11 @@
(subtype* t1 t2)
(subtype* t2 t1)))
(define-syntax-rule (with-fresh-obj obj . body)
(let-values ([(obj os) (obj-seq-next (temp-objs))])
(parameterize ([temp-objs os])
. body)))
;; the algorithm for recursive types transcribed directly from TAPL, pg 305
;; List[(cons Number Number)] type type -> List[(cons Number Number)] or #f
;; is s a subtype of t, taking into account previously seen pairs A
@ -388,73 +386,63 @@
;; types as they are encountered:
;; needs-resolved? types (Mus, Names, Apps),
;; Instances, and Structs (Prefabs?)
(define subtype*
(case-lambda
[(A t1 t2)
(define-values (o os) (obj-seq-next (temp-objs)))
(parameterize ([temp-objs os])
(subtype* A t1 t2 o))]
[(A t1 t2 obj)
(cond
[(Univ? t2) A]
[(Bottom? t1) A]
;; error is top and bot
[(or (Error? t1) (Error? t2)) A]
[(disjoint-masks? (mask t1) (mask t2)) #f]
[(equal? t1 t2) A]
[(seen? t1 t2 A) A]
[else
;; first we check on a few t2 cases
;; that need to come early during checking
(match t2
[(Intersection: t2s raw-prop)
(let ([A (for/fold ([A A])
([t2 (in-list t2s)]
#:break (not A))
(subtype* A t1 t2 obj))])
(and A
(or (TrueProp? raw-prop)
(let* ([obj (if (Empty? obj) (-id-path (genid)) obj)]
[prop (instantiate-rep/obj raw-prop obj t1)])
(implies-in-env? (lexical-env)
(-is-type obj t1)
prop)))
A))]
[(? resolvable?)
(let ([A (remember t1 t2 A)])
(with-updated-seen A
(let ([t2 (resolve-once t2)])
;; check needed for if a name that hasn't been resolved yet
(and (Type? t2) (subtype* A t1 t2 obj)))))]
[_
;; otherwise we case on t1
(subtype-cases
A t1 t2 obj
;; if we're still not certain after the switch,
;; check the cases that need to come at the end
(λ (A t1 t2 obj)
(match* (t1 t2)
[(t1 (Union/set: base2 ts2 elems2))
(cond
[(hash-has-key? elems2 t1) A]
[(subtype* A t1 base2 obj)]
[else (for/or ([elem2 (in-list ts2)])
(subtype* A t1 elem2 obj))])]
[(_ (Instance: (? resolvable? t2*)))
(let ([A (remember t1 t2 A)])
(with-updated-seen A
(let ([t2* (resolve-once t2*)])
(and (Type? t2*)
(subtype* A t1 (make-Instance t2*) obj)))))]
[(_ (Poly: vs2 b2))
#:when (null? (fv b2))
(subtype* A t1 b2 obj)]
[(_ (PolyDots: vs2 b2))
#:when (and (null? (fv b2))
(null? (fi b2)))
(subtype* A t1 b2 obj)]
[(_ _) #f])))])])]))
(define (subtype* A t1 t2 [obj #f])
(cond
[(Univ? t2) A]
[(Bottom? t1) A]
;; error is top and bot
[(or (Error? t1) (Error? t2)) A]
[(disjoint-masks? (mask t1) (mask t2)) #f]
[(equal? t1 t2) A]
[(seen? t1 t2 A) A]
[else
;; first we check on a few t2 cases
;; that need to come early during checking
(match t2
[(Intersection: t2s raw-prop)
(let ([A (for/fold ([A A])
([t2 (in-list t2s)]
#:break (not A))
(subtype* A t1 t2 obj))])
(and A
(or (TrueProp? raw-prop)
(let* ([obj (if (Object? obj) obj (-id-path (genid)))]
[prop (instantiate-rep/obj raw-prop obj t1)])
(implies-in-env? (lexical-env)
(-is-type obj t1)
prop)))
A))]
[(? resolvable?)
(let ([A (remember t1 t2 A)])
(with-updated-seen A
(let ([t2 (resolve-once t2)])
;; check needed for if a name that hasn't been resolved yet
(and (Type? t2) (subtype* A t1 t2 obj)))))]
[_ ;; otherwise we case on t1
(subtype-cases A t1 t2 obj)])]))
(define (continue<: A t1 t2 obj)
(match* (t1 t2)
[(t1 (Union/set: base2 ts2 elems2))
(cond
[(hash-has-key? elems2 t1) A]
[(subtype* A t1 base2 obj)]
[else (for/or ([elem2 (in-list ts2)])
(subtype* A t1 elem2 obj))])]
[(_ (Instance: (? resolvable? t2*)))
(let ([A (remember t1 t2 A)])
(with-updated-seen A
(let ([t2* (resolve-once t2*)])
(and (Type? t2*)
(subtype* A t1 (make-Instance t2*) obj)))))]
[(_ (Poly: vs2 b2))
#:when (null? (fv b2))
(subtype* A t1 b2 obj)]
[(_ (PolyDots: vs2 b2))
#:when (and (null? (fv b2))
(null? (fi b2)))
(subtype* A t1 b2 obj)]
[(_ _) #f]))
;; these data structures are allocated once and
;; used below in 'subtype-switch'
@ -489,7 +477,7 @@
(cons portable-fixnum? -NonNegFixnum)
(cons values -Nat)))
(define-rep-switch (subtype-cases A (#:switch t1) t2 obj continue)
(define-rep-switch (subtype-cases A (#:switch t1) t2 obj)
;; NOTE: keep these in alphabetical order
;; or ease of finding cases
[(case: App _)
@ -503,7 +491,7 @@
[(? Async-ChannelTop?) A]
[(Async-Channel: elem2) (type≡? A elem1 elem2)]
[(Evt: evt-t) (subtype* A elem1 evt-t)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Base (Base-bits: num? bits))
(match t2
[(BaseUnion: bbits nbits)
@ -535,7 +523,7 @@
[(Base:Log-Receiver? t1)
(subtype* A log-vect-type evt-t)]
[else #f])]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: BaseUnion (BaseUnion: bbits1 nbits1))
(match t2
[(? Base?) #f]
@ -555,13 +543,13 @@
(match t2
[(? BoxTop?) A]
[(Box: elem2) (type≡? A elem1 elem2)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Channel (Channel: elem1))
(match t2
[(? ChannelTop?) A]
[(Channel: elem2) (type≡? A elem1 elem2)]
[(Evt: evt-t) (subtype* A elem1 evt-t)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Class (Class: row inits fields methods augments init-rest))
(match t2
[(? ClassTop?) A]
@ -601,13 +589,13 @@
(sub init-rest init-rest*))
(and (not init-rest) (not init-rest*)
A)))]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Continuation-Mark-Keyof (Continuation-Mark-Keyof: val1))
(match t2
[(? Continuation-Mark-KeyTop?) A]
[(Continuation-Mark-Keyof: val2)
(type≡? A val1 val2)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: CustodianBox (CustodianBox: elem1))
(match t2
[(CustodianBox: elem2) (subtype* A elem1 elem2)]
@ -615,7 +603,7 @@
;; Note that it's the whole box type that's being
;; compared against evt-t here
(subtype* A t1 evt-t)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Distinction (Distinction: nm1 id1 t1*))
(match t2
[(app resolve (Distinction: nm2 id2 t2*))
@ -623,20 +611,20 @@
(subtype* A t1* t2*)]
[_ (cond
[(subtype* A t1* t2 obj)]
[else (continue A t1 t2 obj)])])]
[else (continue<: A t1 t2 obj)])])]
[(case: Ephemeron (Ephemeron: elem1))
(match t2
[(Ephemeron: elem2) (subtype* A elem1 elem2)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Evt (Evt: result1))
(match t2
[(Evt: result2) (subtype* A result1 result2)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: F (F: var1))
(match t2
;; tvars are equal if they are the same variable
[(F: var2) (eq? var1 var2)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Function (Function: arrs1))
(match t2
;; special-case for case-lambda/union with only one argument
@ -656,11 +644,11 @@
[(supertype-of-one/arr A (car arrs2) arrs1)
=> (λ (A) (loop-arities A (cdr arrs2)))]
[else #f])))]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Future (Future: elem1))
(match t2
[(Future: elem2) (subtype* A elem1 elem2)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Hashtable (Hashtable: key1 val1))
(match t2
[(? HashtableTop?) A]
@ -671,7 +659,7 @@
(subtype-seq A
(subtype* key1 key2)
(subtype* val1 val2))]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: HeterogeneousVector (HeterogeneousVector: elems1))
(match t2
[(VectorTop:) A]
@ -693,7 +681,7 @@
([elem1 (in-list elems1)]
#:break (not A))
(subtype* A elem1 seq-t))]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Instance (Instance: inst-t1))
(cond
[(resolvable? inst-t1)
@ -723,7 +711,7 @@
(and ;; Note that init & augment clauses don't matter for objects
(subtype-clause? method-map method-map*)
(subtype-clause? field-map field-map*))]
[(_ _) (continue A t1 t2 obj)])])]
[(_ _) (continue<: A t1 t2 obj)])])]
[(case: Intersection (Intersection: t1s _))
(match t1
[(Refine: t1* raw-prop)
@ -736,17 +724,16 @@
[else (with-lexical-env env
(subtype* A t1* t2 obj))])]
[else
(define id (genid))
(define obj (-id-path id))
(define prop (instantiate-rep/obj raw-prop obj t1*))
;; 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))])]
(with-fresh-obj obj
(define prop (instantiate-rep/obj raw-prop obj t1*))
;; 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)))])]
[_
(cond
[(for/or ([t1 (in-list t1s)])
(subtype* A t1 t2 obj))]
[else (continue A t1 t2 obj)])])]
[else (continue<: A t1 t2 obj)])])]
[(case: ListDots (ListDots: dty1 dbound1))
(match t2
;; recur structurally on dotted lists, assuming same bounds
@ -760,7 +747,7 @@
;; variance issues.
[(Listof: elem2)
(subtype* A (-poly (dbound1) dty1) elem2)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: MPair (MPair: t11 t12))
(match t2
[(? MPairTop?) A]
@ -775,7 +762,7 @@
(subtype* t11 seq-t)
(subtype* t12 null-or-mpair-top)
(subtype* t12 (make-Sequence (list seq-t))))]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Mu _)
(let ([A (remember t1 t2 A)])
(with-updated-seen A
@ -805,21 +792,21 @@
(subtype-seq A
(subtype* t11 seq-t)
(subtype* t12 (-lst seq-t)))]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Param (Param: in1 out1))
(match t2
[(Param: in2 out2) (subtype-seq A
(subtype* in2 in1)
(subtype* out1 out2))]
[_ (subtype* A (cl->* (t-> out1) (t-> in1 -Void)) t2)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Poly (Poly: names b1))
(match t2
[(? Poly?) #:when (= (length names) (Poly-n t2))
(subtype* A b1 (Poly-body names t2))]
;; use local inference to see if we can use the polytype here
[_ #:when (infer names null (list b1) (list t2) Univ) A]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: PolyDots (PolyDots: (list ns ... n-dotted) b1))
(match t2
[(PolyDots: (list ms ... m-dotted) b2)
@ -847,7 +834,7 @@
(subtype* A (subst-all subst b1) b2)]
[_ #:when (infer ns (list n-dotted) (list b1) (list t2) Univ)
A]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Prefab (Prefab: k1 ss))
(match t2
[(Prefab: k2 ts)
@ -866,11 +853,11 @@
(subtype* t s)
(subtype* s t))
(subtype* A s t))))))))]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Promise (Promise: elem1))
(match t2
[(Promise: elem2) (subtype* A elem1 elem2)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Prompt-Tagof (Prompt-Tagof: body1 handler1))
(match t2
[(? Prompt-TagTop?) A]
@ -878,7 +865,7 @@
(subtype-seq A
(type≡? body1 body2)
(type≡? handler1 handler2))]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Refinement (Refinement: t1-parent id1))
(match t2
[(Refinement: t2-parent id2)
@ -886,17 +873,17 @@
(subtype* A t1-parent t2-parent)]
[_ (cond
[(subtype* A t1-parent t2)]
[else (continue A t1 t2 obj)])])]
[else (continue<: A t1 t2 obj)])])]
;; sequences are covariant
[(case: Sequence (Sequence: ts1))
(match t2
[(Sequence: ts2) (subtypes* A ts1 ts2)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Set (Set: elem1))
(match t2
[(Set: elem2) (subtype* A elem1 elem2)]
[(Sequence: (list seq-t)) (subtype* A elem1 seq-t)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Struct (Struct: nm1 parent1 flds1 proc1 _ _))
(match t2
;; Avoid resolving things that refer to different structs.
@ -934,21 +921,21 @@
(let ([A (remember t1 t2 A)])
(with-updated-seen A
(subtype* A parent1 t2))))]
[else (continue A t1 t2 obj)])]
[_ (continue A t1 t2 obj)])]
[else (continue<: A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: StructType (StructType: t1*))
(match t2
[(StructTypeTop:) A]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Syntax (Syntax: elem1))
(match t2
[(Syntax: elem2) (subtype* A elem1 elem2)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: ThreadCell (ThreadCell: elem1))
(match t2
[(? ThreadCellTop?) A]
[(ThreadCell: elem2) (type≡? A elem1 elem2)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Union (Union/set: base1 ts1 elems1))
(let ([A (subtype* A base1 t2 obj)])
(and A
@ -977,7 +964,7 @@
(check-sub-signatures? exports1 exports2)
(check-sub-signatures? init-depends2 init-depends1)
(subval* A t1* t2*))]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Value (Value: val1))
(match t2
[(Base-predicate: pred) (and (pred val1) A)]
@ -1006,16 +993,16 @@
(-is-type obj t1)
(instantiate-rep/obj p* obj t1)))))
A]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Vector (Vector: elem1))
(match t2
[(? VectorTop?) A]
[(Vector: elem2) (type≡? A elem1 elem2)]
[(Sequence: (list seq-t)) (subtype* A elem1 seq-t)]
[_ (continue A t1 t2 obj)])]
[_ (continue<: A t1 t2 obj)])]
[(case: Weak-Box (Weak-Box: elem1))
(match t2
[(? Weak-BoxTop?) A]
[(Weak-Box: elem2) (type≡? A elem1 elem2)]
[_ (continue A t1 t2 obj)])]
[else: (continue A t1 t2 obj)])
[_ (continue<: A t1 t2 obj)])]
[else: (continue<: A t1 t2 obj)])

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

@ -27,7 +27,8 @@ at least theoretically.
filter-multiple
syntax-length
in-pair
in-sequence-forever
in-list/rest
list-ref/default
match*/no-order
bind
genid
@ -257,17 +258,6 @@ at least theoretically.
(let ((list (syntax->list stx)))
(and list (length list))))
(define (in-sequence-forever seq val)
(make-do-sequence
(λ ()
(let-values ([(more? gen) (sequence-generate seq)])
(values (λ (e) (if (more?) (gen) val))
(λ (_) #t)
#t
(λ (_) #t)
(λ _ #t)
(λ _ #t))))))
(define-syntax (match*/no-order stx)
(define (parse-clauses clauses)
(syntax-parse clauses
@ -344,3 +334,75 @@ at least theoretically.
(syntax-source-module id)))))
(require 'local-ids)
;; in-list/rest
;; (in-list/rest l v)
;;
;; iterates through the elements of the
;; list 'l' until they are exhausted, at which
;; point 'v' is used for each subsequent iteration
(define (in-list/rest-proc l rest)
(in-sequences l (in-cycle (in-value rest))))
(define-sequence-syntax in-list/rest
(λ () #'in-list/rest-proc)
(λ (stx)
(syntax-case stx ()
[[(val) (_ list-exp rest-exp)]
#'[(val)
(:do-in
;; ([(outer-id ...) outer-expr] ...)
([(list) list-exp]
[(rest) rest-exp])
;; outer-check
#t
;; ([loop-id loop-expr] ...)
([pos list])
;; pos-guard
#t
;; ([(inner-id ...) inner-expr] ...)
([(val pos) (if (pair? pos)
(values (car pos) (cdr pos))
(values rest '()))])
;; pre-guard
#t
;; post-guard
#t
;; (loop-arg ...)
(pos))]]
[[xs (_ dd-exp)]
(list? (syntax->datum #'xs))
(raise-syntax-error 'in-list/rest
(format "expected an identifier, given ~a"
(syntax->list #'xs))
#'xs)]
[blah (raise-syntax-error 'in-list/rest "invalid usage" #'blah)])))
;; quick in-list/rest sanity checks
(module+ test
(unless (equal? (for/list ([_ (in-range 0)]
[val (in-list/rest (list 1 2) #f)])
val)
(list))
(error 'in-list/rest "broken!"))
(unless (equal? (for/list ([_ (in-range 2)]
[val (in-list/rest (list 1 2) #f)])
val)
(list 1 2))
(error 'in-list/rest "broken!"))
(unless (equal? (for/list ([_ (in-range 4)]
[val (in-list/rest (list 1 2) #f)])
val)
(list 1 2 #f #f))
(error 'in-list/rest "broken!")))
(define (list-ref/default xs idx default)
(match xs
['() default]
[(cons x xs)
(if (eqv? 0 idx)
x
(list-ref/default xs (sub1 idx) default))]))

105
typed-racket-test/succeed/with-integer-linear-arith2.rkt Normal file
View File

@ -0,0 +1,105 @@
#lang typed/racket
#:with-linear-integer-arithmetic
(define-type (V8 A) (Refine [v : (Vectorof A)] (= 8 (vector-length v))))
(define-type Nat<8 (Refine [i : Natural] (< i 8)))
(: v8ref (-> (V8 Any) Nat<8 Any))
(define (v8ref v i)
(vector-ref v i))
(: poly-v8ref (All (A) (-> (V8 A) Nat<8 A)))
(define (poly-v8ref v i)
(vector-ref v i))
(ann (vector 0 1 2 3 4 5 6 7) (V8 Any))
(ann (vector 0 1 2 3 4 5 6 7) (V8 Byte))
(ann '#(0 1 2 3 4 5 6 7) (V8 Any))
(ann '#(0 1 2 3 4 5 6 7) (V8 Byte))
;;(v8ref (vector 0 1 2 3 4 5 6) 4) ;; should fail
(v8ref (vector 0 1 2 3 4 5 6 7) 4)
(poly-v8ref (vector 0 1 2 3 4 5 6 7) 4)
;(v8ref (vector 0 1 2 3 4 5 6 7) 9) ;; should fail
;(v8ref (vector 0 1 2 3 4 5 6 7 8) 4) ;; should fail
;(poly-v8ref (vector 0 1 2 3 4 5 6 7) 9) ;; should fail
(define v0 : (V8 Any) (vector 0 1 2 3 4 5 6 7))
(define v1 : (Vectorof Any) (vector 0 1 2 3 4 5 6 7))
(if (= 8 (vector-length v0))
(v8ref v0 3)
(ann "hello" Number))
;; TODO
;; this doesn't work right now because aliasing
;; vector-length makes the type un-updatable (i.e. silly
;; implementation bug that needs a minor refactoring of
;; our object representations)
;; (define (byte->byte [b : Byte]) b)
;;(let ([len (vector-length v0)])
;; (when (byte? len)
;; (byte->byte len)))
(when (and (<= 8 (vector-length v1))
(<= (vector-length v1) 8))
(v8ref v1 3))
(define zero 0)
(define one 1)
(define two 2)
(define three 3)
;; cute syntax that forces an integer equality/inequality/etc
;; else typechecking will fail -- also the type check
;; error highlights the test case
(define-syntax (assert= stx)
(syntax-case stx ()
[(_ expr1 expr2)
#`(unless (= expr1 expr2)
#,(quasisyntax/loc stx
(add1 #,(syntax/loc stx "undead = code"))))]))
(define-syntax (assert< stx)
(syntax-case stx ()
[(_ expr1 expr2)
#`(unless (< expr1 expr2)
#,(quasisyntax/loc stx
(add1 #,(syntax/loc stx "undead < code"))))]))
(define-syntax (assert<= stx)
(syntax-case stx ()
[(_ expr1 expr2)
#`(unless (<= expr1 expr2)
#,(quasisyntax/loc stx
(add1 #,(syntax/loc stx "undead <= code"))))]))
(assert= (- three zero) three)
(assert= (- 3 zero) three)
(assert= (- three 0) three)
(assert= (- three zero) 3)
(assert= (- three two) one)
(assert= (+ one two) three)
(assert= (+ one two) three)
(assert= (- (+ one two) one) two)
(assert= (* 2 2 (+ one two)) 12)
(assert= (add1 one) two)
(assert= (sub1 one) 0)
;; would be nice if this worked... I think it doesn't currently
;; because the (min...) expression has a specific type, but
;; no object, and so we learn (<= empty-obj two) =(
;; solutions:
;; 1 - existential results a la the paper
;; 2 - check for contradictions before erasing
;; the empty object? (this is sort of what
;; we do anyway right now but we dont' do it
;; enough to see this contradiction? maybe this is
;; a subtyping limitation...)
;(assert<= (min one two three) two)