Permalink
Browse files

use bits for base unions, make unions deterministic

This PR primarily changes how we represent Base types and unions of
Base types. Basically, Base types now contain a bits field, which
contains an exact-nonnegative-integer? with exactly one bit set to
1. This allows us to represent unions of Base types by simply OR-ing
together the various base bits. We store these unions in a new type
called a BaseUnion (which contains a field for numeric Base type bits
and a field for non-numeric Base type bits). We can perform set
operations on BaseUnion types rather quickly (using simple bitwise
arithmetic operations).

To make Union and BaseUnion work together nicely, the Union type now
has a field for non-Base types, and a field which contains any and all
Base types placed directly in the Union ( either as a Base if there is
only one, or as a BaseUnion if there are more than one).

Other changes present in this PR:

Base types are now "closed" -- i.e. Base types are only declared in
base-types.rkt and numeric-base-types.rkt with a special macro that
assigns them their respective bits. The constructor make-Base is no
longer provided for miscellaneous usages.

Some singleton Value types were moved to Base so all of our common
unions of basic types can fit into the new BaseUnion type (namely
Null, Void, One, Zero, and the booleans).

A new Val-able match expander lets us match on singleton types that
used to all be Value types, but, as described above, now some are Base
types.

Unions contain deterministically ordered, duplicate free lists (in
addition to sets for equality and constant time membership checks), so
iterating over Unions can be done deterministically (yay!) -- this
gets rid of some otherwise problematic behavior in areas like type
inference, where the order Unions are iterated over can actually
affect the results (i.e. if two valid type inferences are possible,
nondeterministic ordering means we can sometimes get one and sometimes
get another, which makes for particularly difficult to debug issues
and in general has no immediate solution (both substitutions are
valid, after all!))
  • Loading branch information...
pnwamk committed Dec 29, 2016
1 parent e72f250 commit 4bfb1016778567a22dfedcf3dc7aaa43bf40dd15
Showing with 1,729 additions and 1,476 deletions.
  1. +15 −20 typed-racket-lib/typed-racket/env/init-envs.rkt
  2. +4 −8 typed-racket-lib/typed-racket/env/type-alias-helper.rkt
  3. +9 −6 typed-racket-lib/typed-racket/infer/constraint-structs.rkt
  4. +47 −43 typed-racket-lib/typed-racket/infer/infer-unit.rkt
  5. +59 −83 typed-racket-lib/typed-racket/infer/intersect.rkt
  6. +4 −3 typed-racket-lib/typed-racket/optimizer/utils.rkt
  7. +4 −4 typed-racket-lib/typed-racket/private/parse-type.rkt
  8. +304 −298 typed-racket-lib/typed-racket/private/type-contract.rkt
  9. +109 −0 typed-racket-lib/typed-racket/rep/base-type-rep.rkt
  10. +220 −0 typed-racket-lib/typed-racket/rep/base-types.rkt
  11. +63 −0 typed-racket-lib/typed-racket/rep/base-union.rkt
  12. +1 −0 typed-racket-lib/typed-racket/rep/core-rep.rkt
  13. +247 −0 typed-racket-lib/typed-racket/rep/numeric-base-types.rkt
  14. +0 −88 typed-racket-lib/typed-racket/rep/rep-utils.rkt
  15. +5 −11 typed-racket-lib/typed-racket/rep/type-mask.rkt
  16. +209 −108 typed-racket-lib/typed-racket/rep/type-rep.rkt
  17. +8 −8 typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt
  18. +5 −5 typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
  19. +1 −1 typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt
  20. +2 −3 typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
  21. +3 −3 typed-racket-lib/typed-racket/typecheck/tc-send.rkt
  22. +10 −90 typed-racket-lib/typed-racket/types/abbrev.rkt
  23. +6 −11 typed-racket-lib/typed-racket/types/base-abbrev.rkt
  24. +6 −6 typed-racket-lib/typed-racket/types/generalize.rkt
  25. +41 −27 typed-racket-lib/typed-racket/types/match-expanders.rkt
  26. +23 −256 typed-racket-lib/typed-racket/types/numeric-tower.rkt
  27. +39 −23 typed-racket-lib/typed-racket/types/overlap.rkt
  28. +7 −4 typed-racket-lib/typed-racket/types/path-type.rkt
  29. +38 −29 typed-racket-lib/typed-racket/types/printer.rkt
  30. +15 −4 typed-racket-lib/typed-racket/types/subtract.rkt
  31. +185 −134 typed-racket-lib/typed-racket/types/subtype.rkt
  32. +5 −16 typed-racket-lib/typed-racket/types/union.rkt
  33. +7 −4 typed-racket-lib/typed-racket/types/update.rkt
  34. +0 −169 typed-racket-lib/typed-racket/utils/hset.rkt
  35. +1 −1 typed-racket-test/unit-tests/infer-tests.rkt
  36. +8 −2 typed-racket-test/unit-tests/remove-intersect-tests.rkt
  37. +8 −3 typed-racket-test/unit-tests/subtype-tests.rkt
  38. +11 −5 typed-racket-test/unit-tests/type-equal-tests.rkt
@@ -3,7 +3,7 @@
;; Support for defining the initial TR environment
(require "../utils/utils.rkt"
- (utils tc-utils hset)
+ (utils tc-utils)
"global-env.rkt"
"type-name-env.rkt"
"type-alias-env.rkt"
@@ -95,22 +95,13 @@
;; Helper for type->sexp
(define (recur ty)
- (define (numeric? t) (match t [(Base: _ _ _ b) b] [(Value: (? number?)) #t] [_ #f]))
- (define (split-union ts)
- (let ([ts (hset->list ts)])
- (define-values (nums others) (partition numeric? ts))
- (cond [(or (null? nums) (null? others))
- ;; nothing interesting to do in this case
- `(Un ,@(map type->sexp ts))]
- [else
- ;; we do a little more work to hopefully save a bunch in serialization space
- ;; if we get a hit in the predefined-type-table
- `(Un ,(type->sexp (apply Un nums)) ,(type->sexp (apply Un others)))])))
-
+ (define (numeric? t) (match t
+ [(Base-bits: num? _) num?]
+ [(Value: (? number?)) #t]
+ [_ #f]))
(match ty
[(In-Predefined-Table: id) id]
- [(Base: n cnt pred _)
- (int-err "Base type ~a not in predefined-type-table" n)]
+ [(? Base?) (int-err "Base type ~a not in predefined-type-table" ty)]
[(B: nat) `(make-B ,nat)]
[(F: sym) `(make-F (quote ,sym))]
[(Pair: ty (Listof: ty))
@@ -214,12 +205,16 @@
,(object->sexp obj))]
[(AnyValues: prop)
`(make-AnyValues ,(prop->sexp prop))]
- [(Union: (app hset->list (list (Value: vs) ...)))
- `(one-of/c ,@(for/list ([v (in-list vs)])
- `(quote ,v)))]
- [(Union: elems) (split-union elems)]
+ [(Union: (? Bottom?) ts)
+ #:when (andmap Value? ts)
+ `(one-of/c ,@(for/list ([t (in-list ts)])
+ `(quote ,(Value-val t))))]
+
+ [(BaseUnion: bbits nbits) `(make-BaseUnion ,bbits ,nbits)]
+ [(Union: base elems) `(Un . ,(append (if (Bottom? base) '() (list (type->sexp base)))
+ (map type->sexp elems)))]
[(Intersection: elems)
- `(make-Intersection (hset ,@(hset-map elems type->sexp)))]
+ `(make-Intersection (list ,@(map type->sexp elems)))]
[(Name: stx 0 #t)
`(-struct-name (quote-syntax ,stx))]
[(Name: stx args struct?)
@@ -3,7 +3,7 @@
;; This module provides helper functions for type aliases
(require "../utils/utils.rkt"
- (utils tarjan tc-utils hset)
+ (utils tarjan tc-utils)
(env type-alias-env type-name-env)
(rep type-rep)
(private parse-type)
@@ -57,8 +57,8 @@
;;
(define (check-type-alias-contractive id type)
(define/match (check type)
- [((Union: elems)) (for/and ([elem (in-hset elems)]) (check elem))]
- [((Intersection: elems)) (for/and ([elem (in-hset elems)]) (check elem))]
+ [((Union: _ ts)) (andmap check ts)]
+ [((Intersection: elems)) (andmap check elems)]
[((Name/simple: name-id))
(and (not (free-identifier=? name-id id))
(check (resolve-once type)))]
@@ -90,11 +90,7 @@
;; Identifier -> Type
;; Construct a fresh placeholder type
(define (make-placeholder-type id)
- (make-Base ;; the uninterned symbol here ensures that no two type
- ;; aliases get the same placeholder type
- (string->uninterned-symbol (symbol->string (syntax-e id)))
- #'(int-err "Encountered unresolved alias placeholder")
- (lambda _ #f) #f))
+ (make-Opaque id))
;; register-all-type-aliases : Listof<Id> Dict<Id, TypeAliasInfo> -> Void
;;
@@ -37,11 +37,14 @@
;; don't want to rule them out too early
(define-struct/cond-contract cset ([maps (listof (cons/c (hash/c symbol? c? #:immutable #t) dmap?))]) #:transparent)
+(define no-cset (make-cset '()))
+
(provide-for-cond-contract dcon/c)
(provide
- (struct-out cset)
- (struct-out dmap)
- (struct-out dcon)
- (struct-out dcon-dotted)
- (struct-out dcon-exact)
- (struct-out c))
+ no-cset
+ (struct-out cset)
+ (struct-out dmap)
+ (struct-out dcon)
+ (struct-out dcon-dotted)
+ (struct-out dcon-exact)
+ (struct-out c))
@@ -10,7 +10,7 @@
(require "../utils/utils.rkt"
(except-in
(combine-in
- (utils tc-utils hset)
+ (utils tc-utils)
(rep free-variance type-rep prop-rep object-rep
values-rep rep-utils type-mask)
(types utils abbrev numeric-tower subtype resolve
@@ -397,7 +397,6 @@
(define (cgen/inv context s t)
(% cset-meet (cgen context s t) (cgen context t s)))
-
;; context : the context of what to infer/not infer
;; S : a type to be the subtype of T
;; T : a type
@@ -527,28 +526,32 @@
;; find *an* element of elems which can be made a subtype of T
[((Intersection: ts) T)
(cset-join
- (for*/list ([t (in-hset ts)]
+ (for*/list ([t (in-list ts)]
[v (in-value (cg t T))]
#:when v)
v))]
;; constrain S to be below *each* element of elems, and then combine the constraints
[(S (Intersection: ts))
- (define cs (for/list/fail ([ts (in-hset ts)]) (cg S ts)))
+ (define cs (for/list/fail ([ts (in-list ts)]) (cg S ts)))
(and cs (cset-meet* (cons empty cs)))]
;; constrain *each* element of es to be below T, and then combine the constraints
- [((Union: es) T)
- (define cs (for/list/fail ([e (in-hset es)]) (cg e T)))
+ [((BaseUnion-bases: es) T)
+ (define cs (for/list/fail ([e (in-list es)]) (cg e T)))
+ (and cs (cset-meet* (cons empty cs)))]
+ [((Union-all: es) T)
+ (define cs (for/list/fail ([e (in-list es)]) (cg e T)))
(and cs (cset-meet* (cons empty cs)))]
+ [(_ (Bottom:)) no-cset]
+
;; find *an* element of es which can be made to be a supertype of S
;; FIXME: we're using multiple csets here, but I don't think it makes a difference
;; not using multiple csets will break for: ???
- [(S (or (Union: es)
- (and (Bottom:) (bind es (hset)))))
+ [(S (Union-all: es))
(cset-join
- (for*/list ([e (in-hset es)]
+ (for*/list ([e (in-list es)]
[v (in-value (cg S e))]
#:when v)
v))]
@@ -617,11 +620,11 @@
(cg t t*)))]
[((Vector: t) (Sequence: (list t*)))
(cg t t*)]
- [((Base: 'String _ _ _) (Sequence: (list t*)))
+ [((? Base:String?) (Sequence: (list t*)))
(cg -Char t*)]
- [((Base: 'Bytes _ _ _) (Sequence: (list t*)))
+ [((? Base:Bytes?) (Sequence: (list t*)))
(cg -Nat t*)]
- [((Base: 'Input-Port _ _ _) (Sequence: (list t*)))
+ [((? Base:Input-Port?) (Sequence: (list t*)))
(cg -Nat t*)]
[((Value: (? exact-nonnegative-integer? n)) (Sequence: (list t*)))
(define possibilities
@@ -636,7 +639,8 @@
[(list pred? type)
(and (pred? n) type)])))
(cg type t*)]
- [((Base: _ _ _ #t) (Sequence: (list t*)))
+ ;; numeric? == #true
+ [((Base-bits: #t _) (Sequence: (list t*)))
(define type
(for/or ([t (in-list (list -Byte -Index -NonNegFixnum -Nat))])
(and (subtype S t) t)))
@@ -694,28 +698,28 @@
(cg a a*)]
[((Evt: a) (Evt: a*))
(cg a a*)]
- [((Base: 'Semaphore _ _ _) (Evt: t))
+ [((? Base:Semaphore?) (Evt: t))
(cg S t)]
- [((Base: 'Output-Port _ _ _) (Evt: t))
+ [((? Base:Output-Port?) (Evt: t))
(cg S t)]
- [((Base: 'Input-Port _ _ _) (Evt: t))
+ [((? Base:Input-Port?) (Evt: t))
(cg S t)]
- [((Base: 'TCP-Listener _ _ _) (Evt: t))
+ [((? Base:TCP-Listener?) (Evt: t))
(cg S t)]
- [((Base: 'Thread _ _ _) (Evt: t))
+ [((? Base:Thread?) (Evt: t))
(cg S t)]
- [((Base: 'Subprocess _ _ _) (Evt: t))
+ [((? Base:Subprocess?) (Evt: t))
(cg S t)]
- [((Base: 'Will-Executor _ _ _) (Evt: t))
+ [((? Base:Will-Executor?) (Evt: t))
(cg S t)]
- [((Base: 'LogReceiver _ _ _) (Evt: t ))
+ [((? Base:Log-Receiver?) (Evt: t ))
(cg (make-HeterogeneousVector
(list -Symbol -String Univ
(Un (-val #f) -Symbol)))
t)]
- [((Base: 'Place _ _ _) (Evt: t))
+ [((? Base:Place?) (Evt: t))
(cg Univ t)]
- [((Base: 'Base-Place-Channel _ _ _) (Evt: t))
+ [((? Base:Base-Place-Channel?) (Evt: t))
(cg Univ t)]
[((CustodianBox: t) (Evt: t*)) (cg S t*)]
[((Channel: t) (Evt: t*)) (cg t t*)]
@@ -864,26 +868,26 @@
;; just return a boolean result
(define infer
(let ()
- (define/cond-contract (infer X Y S T R [expected #f] #:multiple? [multiple-substitutions? #f])
- (((listof symbol?) (listof symbol?) (listof Type?) (listof Type?)
- (or/c #f Values/c ValuesDots?))
- ((or/c #f Values/c AnyValues? ValuesDots?)
- #:multiple? boolean?)
- . ->* . (or/c boolean?
- substitution/c
- (cons/c substitution/c
- (listof substitution/c))))
- (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)]
- [cs* (% cset-meet cs expected-cset)])
- (and cs* (cond
- [R (substs-gen cs* X Y R multiple-substitutions?)]
- [else #t])))))
+ (define/cond-contract (infer X Y S T R [expected #f] #:multiple? [multiple-substitutions? #f])
+ (((listof symbol?) (listof symbol?) (listof Type?) (listof Type?)
+ (or/c #f Values/c ValuesDots?))
+ ((or/c #f Values/c AnyValues? ValuesDots?)
+ #:multiple? boolean?)
+ . ->* . (or/c boolean?
+ substitution/c
+ (cons/c substitution/c
+ (listof substitution/c))))
+ (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)]
+ [cs* (% cset-meet cs expected-cset)])
+ (and cs* (cond
+ [R (substs-gen cs* X Y R multiple-substitutions?)]
+ [else #t])))))
;(trace infer)
infer)) ;to export a variable binding and not syntax
Oops, something went wrong.

0 comments on commit 4bfb101

Please sign in to comment.