typed-racket/typed-racket-test/unit-tests/remove-intersect-tests.rkt
Andrew Kent 4bfb101677 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!))
2017-01-05 20:45:17 -05:00

103 lines
3.7 KiB
Racket

#lang racket/base
(require "test-utils.rkt"
(for-syntax racket/base)
(r:infer infer)
(rep type-rep)
(types abbrev numeric-tower subtype subtract overlap)
rackunit)
(provide tests)
(gen-test-main)
(define-syntax (over-tests stx)
(syntax-case stx ()
[(_ [t1 t2 res] ...)
#'(test-suite "Tests for overlap"
(test-check (format "~a ~a" 't1 't2)
(lambda (a b) (eq? (not (not a)) b))
(overlap? t1 t2) res) ...)]))
(define overlap-tests
(over-tests
[-Number -Integer #t]))
(define-syntax (inter-tests stx)
(syntax-case stx ()
[(_ [t1 t2 res] ...)
#'(test-suite "Tests for intersect"
(test-check (format "~a ~a" 't1 't2)
type-equiv?
(intersect t1 t2) res) ...)]))
(define intersect-tests
(inter-tests
[-Number (Un -Number -Symbol) -Number]
[-Number -Number -Number]
[(Un (-val 'foo) (-val 6)) (Un -Number -Symbol) (Un (-val 'foo) (-val 6))]
[-Number (-mu a (Un -Number -Symbol (make-Listof a))) -Number]
[(Un -Number -Boolean) (-mu a (Un -Number -Symbol (make-Listof a))) -Number]
[(-mu x (Un -Number (make-Listof x))) (Un -Symbol -Number -Boolean) -Number]
[(Un -Number -String -Symbol -Boolean) -Number -Number]
[(-lst -Number) (-pair Univ Univ) (-pair -Number (-lst -Number))]
[(-lst -Number) (-poly (a) (-lst a)) (-poly (a) (-lst a))]
;; FIXME
#;
[-Listof -Sexp (-lst (Un B N -String Sym))]
#;
[-Sexp -Listof (-lst -Sexp)]
[(-val "one") -Fixnum (Un)]
[(Un (-val "one") (-val "two")) (Un (-val "one") (-val 1)) (-val "one")]
;; intersection cases
[(-v a) -String (-unsafe-intersect (-v a) -String)]
[-String (-v a) (-unsafe-intersect (-v a) -String)]
[(-> -Number -Number) (-> -String -String) (-unsafe-intersect (-> -Number -Number)
(-> -String -String))]
[(-mu x (Un (Un -Number -String) (-pair -Number x)))
(-mu x (Un (Un -Number -Symbol) (-pair -Number x)))
(-mu x (Un -Number (-pair -Number x)))]
[(make-Listof (-mu x (Un -String (-HT -String x))))
(make-Listof -HashtableTop)
(make-Listof (-HT -String (-mu x (Un -String (-HT -String x)))))]))
(define-syntax (remo-tests stx)
(syntax-case stx ()
[(_ [t1 t2 res] ...)
(syntax/loc stx
(test-suite "Tests for subtract"
(test-check (format "~a ~a" 't1 't2) type-equiv? (subtract t1 t2) res) ...))]))
(define subtract-tests
(remo-tests
[(Un -Number -Symbol) -Number -Symbol]
[-Number -Number (Un)]
[(Un -Zero -Symbol (make-Listof Univ))
-Zero
(Un -Symbol (make-Listof Univ))]
[(-mu x (Un -Zero -Symbol (make-Listof x)))
-Zero
(Un -Symbol (make-Listof (-mu x (Un -Zero -Symbol (make-Listof x)))))]
[(-mu x (Un -Number -Symbol (make-Listof x)))
-Number
(Un -Symbol (make-Listof (-mu x (Un -Number -Symbol (make-Listof x)))))]
[(-mu x (Un -Number -Symbol -Boolean (make-Listof x)))
-Number
(Un -Symbol -Boolean (make-Listof (-mu x (Un -Number -Symbol -Boolean (make-Listof x)))))]
[(Un (-val #f) (-mu x (Un -Number -Symbol (make-Listof (-v x)))))
(Un -Boolean -Number)
(Un -Symbol (make-Listof (-mu x (Un -Number -Symbol (make-Listof x)))))]
[(Un (-val 'foo) (-val 6)) (Un -Number -Symbol) (Un)]
[(-> (Un -Symbol -Number) -Number) (-> -Number -Number) (Un)]
[(Un (-poly (a) (make-Listof a)) (-> -Number -Number))
(-> -Number -Number)
(-poly (a) (make-Listof a))]
[(Un -Symbol -Number) (-poly (a) -Number) -Symbol]
[(-pair -Number (-v a)) (-pair Univ Univ) (Un)]
))
(define tests
(test-suite "Subtract Intersect"
subtract-tests
intersect-tests
overlap-tests))