remove interning for most Reps in TR

Prior to this change (which was Typed Racket PR 469) all internal TR
objects (Reps) were interned and kept around for the entire duration
of type checking.  Because of this, frequent operations that rebuilt
types were particularly costly (e.g. various forms of
substitution). To recoup some of this cost, caching was being used in
a lot of places. This PR sought to remove interning as the default
behavior for Reps and allow for more flexibility in how we approach
time/space performance needs going forward.

The following changes were included in this overhaul:

Interning: All Reps are no longer interned. Right now we only intern
unions and some propositions.

Rep generic operations: we now use racket/generic so we're not
reinventing this wheel.

Singletons: Reps (e.g. TrueProp, Univ, etc) can be declared singleton,
which creates a single instance of the rep that all visible operations
(even within the declaring module) are defined in terms of
(e.g. predicates are defined as (λ (x) (eq? x singleton-instance)),
etc).

Custom constructors: Custom constructors can be specified for Reps,
which allows for simple normalization, interning, or other invariants
to be enfored whenever a Rep is created.

Union: Unions used to try to ensure no obviously overlaping types
would inhabit the same Union (e.g. (U String (Pairof Any Any) (Pairof
Int Int)) would be simplified to (U String (Pairof Any Any))). This,
however, required frequent calls to subtyping every time a Union was
modified and working with Unions thus had a high cost (another thing
that caching was used to reduce). Instead of this, Unions now enforce
a much simpler set of invariants on their members: (1) No duplicates
(by virtue of using a hash-based set), (2) Any and Nothing do not
appear in unions, and (3) Nested unions are flattened. Also, using a
hashset as the internal data structure meant that we could easily
intern unions w.r.t. equal? equality. NOTE: we do reduce unions to not
contain obviously overlapping terms when printing to users and when
generating contracts (so obviously and avoidable inneficient contracts
are not generated – See union.rkt for 'normalize-type').

Subtyping changes: Subtyping has been designed to reduce dispatch time
w/ a switch since we no longer cache _all_ subtyping calls (we only
cache subtyping results for unions since they have some costly
subtyping).

prop-ops changes: AndProps now are careful to sort OrProps by length
before building the resulting proposition. This is done because
OrProp implication only checks if one Or is a subset of another Or.
By ordering Or props by size, we only ever check if an OrProp implies
another if its size is <= the other OrProp. This also makes the
smart constructor '-and' more robust, since the order the props
appear does not affect if some Ors are kept or not.

Testing: More subtype tests have been added (we are still probably
relying too much on typecheck-tests.rkt and not the more granular unit
tests in general).  Also, typecheck-tests.rkt has been changed to
check for type-equivalence (i.e. subtyping in both directions)
instead of equal? equivalence.
This commit is contained in:
Andrew Kent 2016-10-21 18:53:29 -04:00
parent 90a4d73414
commit 8e7f39025a
103 changed files with 3620 additions and 2727 deletions

View File

@ -4,7 +4,7 @@
"../utils/utils.rkt"
(for-template racket/base racket/list racket/unsafe/ops racket/flonum racket/extflonum racket/fixnum)
(utils tc-utils)
(rename-in (types union abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym]))
(rename-in (types abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym]))
(provide indexing)

View File

@ -23,22 +23,29 @@
(only-in racket/private/pre-base new-apply-proc)
(only-in (types abbrev) [-Boolean B] [-Symbol Sym] -Flat)
(only-in (types numeric-tower) [-Number N])
(only-in (rep type-rep values-rep)
make-ClassTop
make-UnitTop
make-Name
(only-in (rep type-rep values-rep object-rep)
-car
-cdr
-force
-field
-syntax-e
-ClassTop
-UnitTop
make-ValuesDots
make-MPairTop
make-BoxTop make-ChannelTop make-VectorTop
make-ThreadCellTop
-MPairTop
-BoxTop
-ChannelTop
-VectorTop
-ThreadCellTop
make-Ephemeron
make-CustodianBox
make-HeterogeneousVector
make-Continuation-Mark-Keyof
make-Continuation-Mark-KeyTop
-Continuation-Mark-KeyTop
make-Prompt-Tagof
make-Prompt-TagTop
make-StructType make-StructTypeTop
-Prompt-TagTop
make-StructType
-StructTypeTop
make-ListDots))
;; Racket Reference
@ -829,18 +836,18 @@
[unsafe-set-mcdr! (-poly (a b)
(cl->* (-> (-mpair a b) b -Void)
(-> (-mlst a) (-mlst a) -Void)))]
[mpair? (make-pred-ty (make-MPairTop))]
[mpair? (make-pred-ty -MPairTop)]
[mlist (-poly (a) (->* (list) a (-mlst a)))]
[mlength (-poly (a) (-> (-mlst a) -Index))]
[mreverse! (-poly (a) (-> (-mlst a) (-mlst a)))]
[mappend (-poly (a) (->* (list) (-mlst a) (-mlst a)))]
;; Section 4.11 (Vectors)
[vector? (make-pred-ty (make-VectorTop))]
[vector? (make-pred-ty -VectorTop)]
[vector->list (-poly (a) (cl->* (-> (-vec a) (-lst a))
(-> (make-VectorTop) (-lst Univ))))]
(-> -VectorTop (-lst Univ))))]
[list->vector (-poly (a) (-> (-lst a) (-vec a)))]
[vector-length ((make-VectorTop) . -> . -Index)]
[vector-length (-VectorTop . -> . -Index)]
[vector (-poly (a) (->* (list) a (-vec a)))]
[vector-immutable (-poly (a) (->* (list) a (-vec a)))]
[vector->immutable-vector (-poly (a) (-> (-vec a) (-vec a)))]
@ -893,26 +900,26 @@
[box-immutable (-poly (a) (a . -> . (-box a)))]
[unbox (-poly (a) (cl->*
((-box a) . -> . a)
((make-BoxTop) . -> . Univ)))]
(-BoxTop . -> . Univ)))]
[set-box! (-poly (a) ((-box a) a . -> . -Void))]
[box-cas! (-poly (a) ((-box a) a a . -> . -Boolean))]
[unsafe-unbox (-poly (a) (cl->*
((-box a) . -> . a)
((make-BoxTop) . -> . Univ)))]
(-BoxTop . -> . Univ)))]
[unsafe-set-box! (-poly (a) ((-box a) a . -> . -Void))]
[unsafe-unbox* (-poly (a) (cl->*
((-box a) . -> . a)
((make-BoxTop) . -> . Univ)))]
(-BoxTop . -> . Univ)))]
[unsafe-set-box*! (-poly (a) ((-box a) a . -> . -Void))]
[unsafe-box*-cas! (-poly (a) ((-box a) a a . -> . -Boolean))]
[box? (make-pred-ty (make-BoxTop))]
[box? (make-pred-ty -BoxTop)]
;; Section 4.13 (Hash Tables)
[hash? (make-pred-ty -HashTop)]
[hash-eq? (-> -HashTop B)]
[hash-eqv? (-> -HashTop B)]
[hash-equal? (-> -HashTop B)]
[hash-weak? (-> -HashTop B)]
[hash? (make-pred-ty -HashtableTop)]
[hash-eq? (-> -HashtableTop B)]
[hash-eqv? (-> -HashtableTop B)]
[hash-equal? (-> -HashtableTop B)]
[hash-weak? (-> -HashtableTop B)]
[hash (-poly (a b) (cl->* (-> (-HT a b))
(a b . -> . (-HT a b))
(a b a b . -> . (-HT a b))
@ -944,11 +951,11 @@
(cl-> [((-HT a b) a) b]
[((-HT a b) a (-val #f)) (-opt b)]
[((-HT a b) a (-> c)) (Un b c)]
[(-HashTop a) Univ]
[(-HashTop a (-val #f)) Univ]
[(-HashTop a (-> c)) Univ]))]
[(-HashtableTop a) Univ]
[(-HashtableTop a (-val #f)) Univ]
[(-HashtableTop a (-> c)) Univ]))]
[hash-ref! (-poly (a b) (-> (-HT a b) a (-> b) b))]
[hash-has-key? (-HashTop Univ . -> . B)]
[hash-has-key? (-HashtableTop Univ . -> . B)]
[hash-update! (-poly (a b)
(cl-> [((-HT a b) a (-> b b)) -Void]
[((-HT a b) a (-> b b) (-> b)) -Void]))]
@ -956,21 +963,21 @@
(cl-> [((-HT a b) a (-> b b)) (-HT a b)]
[((-HT a b) a (-> b b) (-> b)) (-HT a b)]))]
[hash-remove (-poly (a b) (cl-> [((-HT a b) Univ) (-HT a b)]
[(-HashTop Univ) -HashTop]))]
[(-HashtableTop Univ) -HashtableTop]))]
[hash-remove! (-poly (a b) (cl-> [((-HT a b) a) -Void]
[(-HashTop a) -Void]))]
[(-HashtableTop a) -Void]))]
[hash-map (-poly (a b c) (cl-> [((-HT a b) (a b . -> . c)) (-lst c)]
[(-HashTop (Univ Univ . -> . c)) (-lst c)]))]
[(-HashtableTop (Univ Univ . -> . c)) (-lst c)]))]
[hash-for-each (-poly (a b c) (cl-> [((-HT a b) (-> a b c)) -Void]
[(-HashTop (-> Univ Univ c)) -Void]))]
[hash-count (-> -HashTop -Index)]
[hash-empty? (-> -HashTop -Boolean)]
[(-HashtableTop (-> Univ Univ c)) -Void]))]
[hash-count (-> -HashtableTop -Index)]
[hash-empty? (-> -HashtableTop -Boolean)]
[hash-keys (-poly (a b) (cl-> [((-HT a b)) (-lst a)]
[(-HashTop) (-lst Univ)]))]
[(-HashtableTop) (-lst Univ)]))]
[hash-values (-poly (a b) (cl-> [((-HT a b)) (-lst b)]
[(-HashTop) (-lst Univ)]))]
[(-HashtableTop) (-lst Univ)]))]
[hash->list (-poly (a b) (cl-> [((-HT a b)) (-lst (-pair a b))]
[(-HashTop) (-lst (-pair Univ Univ))]))]
[(-HashtableTop) (-lst (-pair Univ Univ))]))]
[hash-copy (-poly (a b) (-> (-HT a b) (-HT a b)))]
[eq-hash-code (-> Univ -Fixnum)]
@ -980,23 +987,23 @@
[hash-iterate-first (-poly (a b)
(cl->*
((-HT a b) . -> . (Un (-val #f) -Integer))
(-> -HashTop (Un (-val #f) -Integer))))]
(-> -HashtableTop (Un (-val #f) -Integer))))]
[hash-iterate-next (-poly (a b)
(cl->*
((-HT a b) -Integer . -> . (Un (-val #f) -Integer))
(-> -HashTop -Integer (Un (-val #f) -Integer))))]
(-> -HashtableTop -Integer (Un (-val #f) -Integer))))]
[hash-iterate-key (-poly (a b)
(cl->* ((-HT a b) -Integer . -> . a)
(-> -HashTop -Integer Univ)))]
(-> -HashtableTop -Integer Univ)))]
[hash-iterate-value (-poly (a b)
(cl->* ((-HT a b) -Integer . -> . b)
(-> -HashTop -Integer Univ)))]
(-> -HashtableTop -Integer Univ)))]
[hash-iterate-pair (-poly (a b)
(cl->* ((-HT a b) -Integer . -> . (-pair a b))
(-> -HashTop -Integer Univ)))]
(-> -HashtableTop -Integer Univ)))]
[hash-iterate-key+value (-poly (a b)
(cl->* ((-HT a b) -Integer . -> . (-values (list a b)))
(-> -HashTop -Integer (-values (list Univ Univ)))))]
(-> -HashtableTop -Integer (-values (list Univ Univ)))))]
[make-custom-hash (->opt (-> Univ Univ Univ) (-> Univ -Nat) [(-> Univ -Nat)] Univ)]
[make-immutable-custom-hash (->opt (-> Univ Univ Univ) (-> Univ -Nat) [(-> Univ -Nat)] Univ)]
@ -1146,7 +1153,7 @@
;; Section 5.2 (Structure Types)
[make-struct-type
(->opt -Symbol
(-opt (make-StructTypeTop))
(-opt -StructTypeTop)
-Nat -Nat
[Univ
(-lst (-pair -Struct-Type-Property Univ))
@ -1155,7 +1162,7 @@
(-lst -Nat)
(-opt top-func)
(-opt -Symbol)]
(-values (list (make-StructTypeTop) top-func top-func top-func top-func)))]
(-values (list -StructTypeTop top-func top-func top-func top-func)))]
[make-struct-field-accessor (->opt top-func -Nat [(-opt -Symbol)] top-func)]
[make-struct-field-mutator (->opt top-func -Nat [(-opt -Symbol)] top-func)]
@ -1173,33 +1180,33 @@
;; Section 5.6 (Structure Utilities)
[struct->vector (Univ . -> . (-vec Univ))]
[struct? (-> Univ -Boolean)]
[struct-type? (make-pred-ty (make-StructTypeTop))]
[struct-type? (make-pred-ty -StructTypeTop)]
;; Section 6.2 (Classes)
[object% (-class)]
;; Section 6.11 (Object, Class, and Interface Utilities)
[object? (make-pred-ty (-object))]
[class? (make-pred-ty (make-ClassTop))]
[class? (make-pred-ty -ClassTop)]
;; TODO: interface?
;; generic?
[object=? (-> (-object) (-object) -Boolean)]
[object->vector (->opt (-object) [Univ] (-vec Univ))]
;; TODO: class->interface
;; object-interface
[is-a? (-> Univ (make-ClassTop) -Boolean)]
[subclass? (-> Univ (make-ClassTop) -Boolean)]
[is-a? (-> Univ -ClassTop -Boolean)]
[subclass? (-> Univ -ClassTop -Boolean)]
;; TODO: implementation?
;; interface-extension?
;; method-in-interface?
;; interface->method-names
[object-method-arity-includes? (-> (-object) -Symbol -Nat -Boolean)]
[field-names (-> (-object) (-lst -Symbol))]
[object-info (-> (-object) (-values (list (Un (make-ClassTop) (-val #f)) -Boolean)))]
[object-info (-> (-object) (-values (list (Un -ClassTop (-val #f)) -Boolean)))]
;; TODO: class-info (is this sound to allow?)
;; Section 7.8 (Unit Utilities)
[unit? (make-pred-ty (make-UnitTop))]
[unit? (make-pred-ty -UnitTop)]
;; Section 9.1
[exn:misc:match? (-> Univ B)]
@ -1309,34 +1316,34 @@
(make-ValuesDots (list (-result b)) c 'c))
(make-ValuesDots (list (-result (Un a b))) c 'c))))]
[call-with-continuation-barrier (-poly (a) (-> (-> a) a))]
[continuation-prompt-available? (-> (make-Prompt-TagTop) B)]
[continuation-prompt-available? (-> -Prompt-TagTop B)]
[continuation?
(asym-pred Univ B (-PS (-is-type 0 top-func) -tt))]
[continuation-prompt-tag? (make-pred-ty (make-Prompt-TagTop))]
[continuation-prompt-tag? (make-pred-ty -Prompt-TagTop)]
[dynamic-wind (-poly (a) (-> (-> ManyUniv) (-> a) (-> ManyUniv) a))]
;; Section 10.5 (Continuation Marks)
;; continuation-marks needs type for continuations as other
;; possible first argument
[continuation-marks
(->opt (Un (-val #f) -Thread) [(make-Prompt-TagTop)] -Cont-Mark-Set)]
[current-continuation-marks (->opt [(make-Prompt-TagTop)] -Cont-Mark-Set)]
(->opt (Un (-val #f) -Thread) [-Prompt-TagTop] -Cont-Mark-Set)]
[current-continuation-marks (->opt [-Prompt-TagTop] -Cont-Mark-Set)]
[continuation-mark-set->list
(-poly (a)
(cl->*
(->opt -Cont-Mark-Set (make-Continuation-Mark-Keyof a)
[(make-Prompt-TagTop)] (-lst a))
(->opt -Cont-Mark-Set Univ [(make-Prompt-TagTop)] (-lst Univ))))]
[-Prompt-TagTop] (-lst a))
(->opt -Cont-Mark-Set Univ [-Prompt-TagTop] (-lst Univ))))]
[continuation-mark-set->list*
(-poly (a b)
(cl->*
(->opt -Cont-Mark-Set
(-lst (make-Continuation-Mark-Keyof a))
[b (make-Prompt-TagTop)]
[b -Prompt-TagTop]
(-lst (-vec (Un a b))))
(->opt -Cont-Mark-Set
(-lst Univ)
[Univ (make-Prompt-TagTop)]
[Univ -Prompt-TagTop]
(-lst (-vec Univ)))))]
[continuation-mark-set-first
(-poly (a b)
@ -1344,12 +1351,12 @@
(-> (-opt -Cont-Mark-Set) (make-Continuation-Mark-Keyof a)
(-opt a))
(->opt (-opt -Cont-Mark-Set) (make-Continuation-Mark-Keyof a)
[b (make-Prompt-TagTop)]
[b -Prompt-TagTop]
(Un a b))
(->opt (-opt -Cont-Mark-Set) Univ [Univ (make-Prompt-TagTop)] Univ)))]
(->opt (-opt -Cont-Mark-Set) Univ [Univ -Prompt-TagTop] Univ)))]
[call-with-immediate-continuation-mark
(-poly (a) (->opt Univ (-> Univ a) [Univ] a))]
[continuation-mark-key? (make-pred-ty (make-Continuation-Mark-KeyTop))]
[continuation-mark-key? (make-pred-ty -Continuation-Mark-KeyTop)]
[continuation-mark-set? (make-pred-ty -Cont-Mark-Set)]
[make-continuation-mark-key
(-poly (a) (->opt [-Symbol] (make-Continuation-Mark-Keyof a)))]
@ -1438,7 +1445,7 @@
;; Section 11.2.2
[make-channel (-poly (a) (-> (-channel a)))]
[channel? (make-pred-ty (make-ChannelTop))]
[channel? (make-pred-ty -ChannelTop)]
[channel-get (-poly (a) ((-channel a) . -> . a))]
[channel-try-get (-poly (a) ((-channel a) . -> . (Un a (-val #f))))]
[channel-put (-poly (a) ((-channel a) a . -> . -Void))]
@ -1468,7 +1475,7 @@
[a a] b)))]
;; Section 11.3.1 (Thread Cells)
[thread-cell? (make-pred-ty (make-ThreadCellTop))]
[thread-cell? (make-pred-ty -ThreadCellTop)]
[make-thread-cell (-poly (a) (->opt a [Univ] (-thread-cell a)))]
[thread-cell-ref (-poly (a) (-> (-thread-cell a) a))]
[thread-cell-set! (-poly (a) (-> (-thread-cell a) a -Void))]
@ -1755,7 +1762,7 @@
;; Section 12.8
[syntax-recertify (-poly (a) (-> (-Syntax a) (-Syntax Univ) -Inspector Univ (-Syntax a)))]
[syntax-debug-info (-poly (a) (->opt (-Syntax a) [(-opt -Integer) Univ] -HashTop))]
[syntax-debug-info (-poly (a) (->opt (-Syntax a) [(-opt -Integer) Univ] -HashtableTop))]
;; Section 12.9
[expand (-> Univ (-Syntax Univ))]
@ -2495,23 +2502,23 @@
[make-sibling-inspector (->opt [-Inspector] -Inspector)]
[current-inspector (-Param -Inspector -Inspector)]
[struct-info (-> Univ (-values (list (-opt (make-StructTypeTop)) B)))]
[struct-info (-> Univ (-values (list (-opt -StructTypeTop) B)))]
[struct-type-info
(-poly (a)
(cl->*
(-> (make-StructType a)
(-values (list Sym -Nat -Nat (-> a -Nat Univ)
(-> a -Nat (Un) -Void) (-lst -Nat)
(-opt (make-StructTypeTop)) B)))
(-> (make-StructTypeTop)
(-opt -StructTypeTop) B)))
(-> -StructTypeTop
(-values (list Sym -Nat -Nat top-func top-func (-lst -Nat)
(-opt (make-StructTypeTop)) B)))))]
[struct-type-make-constructor (-> (make-StructTypeTop) top-func)]
(-opt -StructTypeTop) B)))))]
[struct-type-make-constructor (-> -StructTypeTop top-func)]
[struct-type-make-predicate
(-poly (a)
(cl->*
(-> (make-StructType a) (make-pred-ty a))
(-> (make-StructTypeTop) (-> Univ B))))]
(-> -StructTypeTop (-> Univ B))))]
[object-name (-> Univ Univ)]
;; Section 14.9 (Code Inspectors)
@ -3069,8 +3076,8 @@
(cl->*
(->acc (list (-pair a b)) b (list -cdr))
(->* (list (-lst a)) (-lst a))))]
[unsafe-vector-length ((make-VectorTop) . -> . -Index)]
[unsafe-vector*-length ((make-VectorTop) . -> . -Index)]
[unsafe-vector-length (-VectorTop . -> . -Index)]
[unsafe-vector*-length (-VectorTop . -> . -Index)]
[unsafe-struct-ref top-func]
[unsafe-struct*-ref top-func]
[unsafe-struct-set! top-func]

View File

@ -4,14 +4,15 @@
;; that are expanded into by Racket macros
(require
"../utils/utils.rkt"
(only-in "../rep/type-rep.rkt" make-StructTypeTop)
(only-in "../rep/type-rep.rkt" -StructTypeTop)
racket/promise
string-constants/string-constant
racket/private/kw racket/file racket/port syntax/parse racket/path
(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 union) [make-arr* make-arr])
(rename-in (types abbrev numeric-tower)
[make-arr* make-arr])
(for-syntax racket/base syntax/parse
(only-in racket/syntax syntax-local-eval)))
(provide make-template-identifier)
@ -121,67 +122,67 @@
[(make-template-identifier 'default-in-hash 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a b)]
[(-HashTop) (-seq Univ Univ)]))]
[(-HashtableTop) (-seq Univ Univ)]))]
[(make-template-identifier 'default-in-hash-keys 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a)]
[(-HashTop) (-seq Univ)]))]
[(-HashtableTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-hash-values 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq b)]
[(-HashTop) (-seq Univ)]))]
[(-HashtableTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-hash-pairs 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq (-pair a b))]
[(-HashTop) (-seq (-pair Univ Univ))]))]
[(-HashtableTop) (-seq (-pair Univ Univ))]))]
[(make-template-identifier 'default-in-immutable-hash 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a b)]
[(-HashTop) (-seq Univ Univ)]))]
[(-HashtableTop) (-seq Univ Univ)]))]
[(make-template-identifier 'default-in-immutable-hash-keys 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a)]
[(-HashTop) (-seq Univ)]))]
[(-HashtableTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-immutable-hash-values 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq b)]
[(-HashTop) (-seq Univ)]))]
[(-HashtableTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-immutable-hash-pairs 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq (-pair a b))]
[(-HashTop) (-seq (-pair Univ Univ))]))]
[(-HashtableTop) (-seq (-pair Univ Univ))]))]
[(make-template-identifier 'default-in-mutable-hash 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a b)]
[(-HashTop) (-seq Univ Univ)]))]
[(-HashtableTop) (-seq Univ Univ)]))]
[(make-template-identifier 'default-in-mutable-hash-keys 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a)]
[(-HashTop) (-seq Univ)]))]
[(-HashtableTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-mutable-hash-values 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq b)]
[(-HashTop) (-seq Univ)]))]
[(-HashtableTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-mutable-hash-pairs 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq (-pair a b))]
[(-HashTop) (-seq (-pair Univ Univ))]))]
[(-HashtableTop) (-seq (-pair Univ Univ))]))]
[(make-template-identifier 'default-in-weak-hash 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a b)]
[(-HashTop) (-seq Univ Univ)]))]
[(-HashtableTop) (-seq Univ Univ)]))]
[(make-template-identifier 'default-in-weak-hash-keys 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a)]
[(-HashTop) (-seq Univ)]))]
[(-HashtableTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-weak-hash-values 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq b)]
[(-HashTop) (-seq Univ)]))]
[(-HashtableTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-weak-hash-pairs 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq (-pair a b))]
[(-HashTop) (-seq (-pair Univ Univ))]))]
[(-HashtableTop) (-seq (-pair Univ Univ))]))]
;; in-port
[(make-template-identifier 'in-port 'racket/private/for)
(-poly (a)
@ -246,9 +247,9 @@
[(make-template-identifier 'prop:named-keyword-procedure 'racket/private/kw)
-Struct-Type-Property]
[(make-template-identifier 'struct:keyword-procedure/arity-error 'racket/private/kw)
(make-StructTypeTop)]
-StructTypeTop]
[(make-template-identifier 'struct:keyword-method/arity-error 'racket/private/kw)
(make-StructTypeTop)]
-StructTypeTop]
;; from the expansion of `define-runtime-path`
[(make-template-identifier 'path-of 'racket/runtime-path)
(-> -Path -Path)]

View File

@ -3,7 +3,7 @@
(require
"../utils/utils.rkt"
(rep type-rep)
(types abbrev numeric-tower union)
(types abbrev numeric-tower)
(typecheck tc-structs)
;;For tests
(prefix-in k: '#%kernel))

View File

@ -1,7 +1,8 @@
#lang s-exp "type-env-lang.rkt"
(require "../types/abbrev.rkt" "../types/union.rkt"
"../types/numeric-tower.rkt" "../rep/type-rep.rkt")
(require "../types/abbrev.rkt"
"../types/numeric-tower.rkt"
"../rep/type-rep.rkt")
[Complex -Number]
[Number -Number]
@ -119,14 +120,14 @@
[ChannelTop -ChannelTop]
[Async-ChannelTop -Async-ChannelTop]
[VectorTop -VectorTop]
[HashTableTop -HashTop]
[HashTableTop -HashtableTop]
[MPairTop -MPairTop]
[Thread-CellTop -Thread-CellTop]
[Thread-CellTop -ThreadCellTop]
[Prompt-TagTop -Prompt-TagTop]
[Continuation-Mark-KeyTop -Continuation-Mark-KeyTop]
[Struct-TypeTop (make-StructTypeTop)]
[ClassTop (make-ClassTop)]
[UnitTop (make-UnitTop)]
[Struct-TypeTop -StructTypeTop]
[ClassTop -ClassTop]
[UnitTop -UnitTop]
[Keyword -Keyword]
[Thread -Thread]
[Resolved-Module-Path -Resolved-Module-Path]

View File

@ -5,7 +5,7 @@
(require (for-syntax racket/base syntax/parse)
(utils tc-utils)
(env init-envs)
(types abbrev numeric-tower union prop-ops))
(types abbrev numeric-tower prop-ops))
(define-syntax (-#%module-begin stx)
(define-syntax-class clause
@ -29,4 +29,4 @@
require
(except-out (all-from-out racket/base) #%module-begin)
types rep private utils
(types-out abbrev numeric-tower union prop-ops))
(types-out abbrev numeric-tower prop-ops))

View File

@ -12,7 +12,7 @@
racket/base
syntax/parse
syntax/stx)
(for-syntax (types abbrev numeric-tower union prop-ops)))
(for-syntax (types abbrev numeric-tower prop-ops)))
(provide type-environment
(rename-out [-#%module-begin #%module-begin])
@ -21,7 +21,7 @@
(except-out (all-from-out racket/base) #%module-begin)
(for-syntax (except-out (all-from-out racket/base) #%module-begin))
types rep private utils
(for-syntax (types-out abbrev numeric-tower union prop-ops)))
(for-syntax (types-out abbrev numeric-tower prop-ops)))
;; syntax classes for type clauses in the type-environment macro
(begin-for-syntax

View File

@ -21,8 +21,6 @@
type-env-map
type-env-for-each)
(lazy-require ["../rep/type-rep.rkt" (Type? type-equal?)])
;; free-id-table from id -> type or Box[type]
;; where id is a variable, and type is the type of the variable
;; if the result is a box, then the type has not actually been defined, just registered
@ -37,7 +35,7 @@
(cond [(free-id-table-ref the-mapping id (lambda _ #f))
=> (lambda (e)
(define t (if (box? e) (unbox e) e))
(unless (and (Type? t) (type-equal? t type))
(unless (equal? t type)
(tc-error/delayed #:stx id "Duplicate type annotation of ~a for ~a, previous was ~a" type (syntax-e id) t))
(when (box? e)
(free-id-table-set! the-mapping id t)))]
@ -51,7 +49,7 @@
=>
(λ (t) ;; it's ok to annotate with the same type
(define t* (if (box? t) (unbox t) t))
(unless (and (Type? t*) (type-equal? type t*))
(unless (equal? type t*)
(tc-error/delayed #:stx id "Duplicate type annotation of ~a for ~a, previous was ~a" type (syntax-e id) t*)))]
[else (free-id-table-set! the-mapping id (box type))]))

View File

@ -3,19 +3,18 @@
;; Support for defining the initial TR environment
(require "../utils/utils.rkt"
"../utils/tc-utils.rkt"
(utils tc-utils hset)
"global-env.rkt"
"type-name-env.rkt"
"type-alias-env.rkt"
"mvar-env.rkt"
"signature-env.rkt"
(rename-in racket/private/sort [sort raw-sort])
(rep core-rep type-rep
prop-rep rep-utils
object-rep values-rep
free-variance)
(for-syntax syntax/parse racket/base)
(types abbrev struct-table union utils)
(types abbrev struct-table utils)
data/queue
racket/dict racket/list racket/set racket/promise
racket/match)
@ -59,11 +58,11 @@
;; Compute for a given type how many times each type inside of it
;; is referenced
(define (compute-popularity ty)
(when (Type? ty)
(hash-update! pop-table ty add1 0))
(when (walkable? ty)
(Rep-walk compute-popularity ty)))
(define (compute-popularity x)
(when (Type? x)
(hash-update! pop-table x add1 0))
(when (Rep? x)
(Rep-for-each x compute-popularity)))
(define (popular? ty)
(> (hash-ref pop-table ty 0) 5))
@ -91,22 +90,22 @@
(λ (stx)
(syntax-parse stx
[(_ id)
#'(? Rep? (app (λ (v) (hash-ref predefined-type-table (Rep-seq v) #f))
#'(? Rep? (app (λ (v) (hash-ref predefined-type-table v #f))
(? values id)))])))
;; Helper for type->sexp
(define (recur ty)
(define (numeric? t) (match t [(Base: _ _ _ b) b] [(Value: (? number?)) #t] [_ #f]))
(define (split-union ts)
(define-values (nums others) (partition numeric? ts))
(cond [(or (null? nums) (null? others))
;; nothing interesting to do in this case
`(make-Union (list ,@(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
`(simple-Un ,(type->sexp (apply Un nums))
,(type->sexp (apply Un others)))]))
(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)))])))
(match ty
[(In-Predefined-Table: id) id]
@ -215,12 +214,12 @@
,(object->sexp obj))]
[(AnyValues: prop)
`(make-AnyValues ,(prop->sexp prop))]
[(Union: (list (Value: vs) ...))
[(Union: (app hset->list (list (Value: vs) ...)))
`(one-of/c ,@(for/list ([v (in-list vs)])
`(quote ,v)))]
[(Union: elems) (split-union elems)]
[(Intersection: elems)
`(make-Intersection (list ,@(map type->sexp elems)))]
`(make-Intersection (hset ,@(hset-map elems type->sexp)))]
[(Name: stx 0 #t)
`(-struct-name (quote-syntax ,stx))]
[(Name: stx args struct?)
@ -238,10 +237,9 @@
[(Prefab: key flds)
`(make-Prefab (quote ,key)
(list ,@(map type->sexp flds)))]
[(App: rator rands stx)
[(App: rator rands)
`(make-App ,(type->sexp rator)
(list ,@(map type->sexp rands))
,(and stx `(quote-syntax ,stx)))]
(list ,@(map type->sexp rands)))]
[(Opaque: pred)
`(make-Opaque (quote-syntax ,pred))]
[(Refinement: parent pred)
@ -344,7 +342,7 @@
;; Convert an object to an s-expression to eval
(define (object->sexp obj)
(match obj
[(Empty:) `(make-Empty)]
[(Empty:) `-empty-obj]
[(Path: null (cons 0 arg))
`(-arg-path ,arg)]
[(Path: null (cons depth arg))

View File

@ -1,13 +1,13 @@
#lang racket/base
(require syntax/id-table racket/dict)
(require syntax/id-table)
(provide mvar-env register-mutated-var is-var-mutated?)
(define mvar-env (make-free-id-table))
(define (register-mutated-var id)
(dict-set! mvar-env id #t))
(free-id-table-set! mvar-env id #t))
(define (is-var-mutated? id)
(dict-ref mvar-env id #f))
(free-id-table-ref mvar-env id #f))

View File

@ -8,8 +8,7 @@
lookup-signature
lookup-signature/check
signature-env-map
signature-env-for-each
with-signature-env/extend)
signature-env-for-each)
(require syntax/id-table
racket/match
@ -21,7 +20,7 @@
(rep type-rep))
;; initial signature environment
(define signature-env (make-parameter (make-immutable-free-id-table)))
(define signature-env (make-free-id-table))
;; register-signature! : identifier? Signature? -> Void
;; adds a mapping from the given identifier to the given signature
@ -30,30 +29,19 @@
(when (lookup-signature id)
(tc-error/fields "duplicate signature definition"
"identifier" (syntax-e id)))
(signature-env (free-id-table-set (signature-env) id sig)))
(define-syntax-rule (with-signature-env/extend ids sigs . b)
(let ([ids* ids]
[sigs* sigs])
(define new-env
(for/fold ([env (signature-env)])
([id (in-list ids*)]
[sig (in-list sigs*)])
(free-id-table-set env id sig)))
(parameterize ([signature-env new-env]) . b)))
(free-id-table-set! signature-env id sig))
;; Iterate over the signature environment forcing the types of bindings
;; in each signature
(define (finalize-signatures!)
(sorted-dict-for-each (signature-env) (λ (id sig) (force sig)) id<))
(sorted-dict-for-each signature-env (λ (id sig) (force sig)) id<))
;; lookup-signature : identifier? -> (or/c #f Signature?)
;; look up the signature corresponding to the given identifier
;; in the signature environment
(define (lookup-signature id)
(cond
[(free-id-table-ref (signature-env) id #f) => force]
[(free-id-table-ref signature-env id #f) => force]
[else #f]))
;; lookup-signature/check : identifier? -> Signature?
@ -67,7 +55,7 @@
#:stx id)))
(define (signature-env-map f)
(sorted-dict-map (signature-env) (λ (id sig) (f id (force sig))) id<))
(sorted-dict-map signature-env (λ (id sig) (f id (force sig))) id<))
(define (signature-env-for-each f)
(sorted-dict-for-each (signature-env) (λ (id sig) (f id (force sig))) id<))
(sorted-dict-for-each signature-env (λ (id sig) (f id (force sig))) id<))

View File

@ -3,7 +3,7 @@
;; This module provides helper functions for type aliases
(require "../utils/utils.rkt"
(utils tarjan tc-utils)
(utils tarjan tc-utils hset)
(env type-alias-env type-name-env)
(rep type-rep)
(private parse-type)
@ -57,11 +57,12 @@
;;
(define (check-type-alias-contractive id type)
(define/match (check type)
[((Union: elems)) (andmap check elems)]
[((Union: elems)) (for/and ([elem (in-hset elems)]) (check elem))]
[((Intersection: elems)) (for/and ([elem (in-hset elems)]) (check elem))]
[((Name/simple: name-id))
(and (not (free-identifier=? name-id id))
(check (resolve-once type)))]
[((App: rator rands stx))
[((App: rator rands))
(and (check rator) (check rands))]
[((Mu: _ body)) (check body)]
[((Poly: names body)) (check body)]

View File

@ -20,14 +20,9 @@
(free-id-table-map (env-types e)
(λ (id ty) (format "[~a ∈ ~a]" id ty)))
(env-props e)
(free-id-table-map (env-types e)
(free-id-table-map (env-aliases e)
(λ (id ty) (format "[~a ≡ ~a]" id ty))))))
;; when interning is removed, the -empty-obj
;; shorthand will be visible in this file. until
;; then this will do -amk
(define -empty-obj (make-Empty))
(provide/cond-contract
[env? predicate/c]
[env-set-type (env? identifier? Type? . -> . env?)]

View File

@ -107,7 +107,7 @@
[(or (not tvars) (null? tvars)) #t]
[else
(define free-vars (free-vars-hash (free-vars* type)))
(define variance (map (λ (v) (hash-ref free-vars v Constant)) tvars))
(define variance (map (λ (v) (hash-ref free-vars v variance:const)) tvars))
(define old-variance (lookup-type-variance name))
(register-type-variance! name variance)
@ -117,5 +117,5 @@
;; Initialize variance of the given id to Constant for all type vars
(define (add-constant-variance! name vars)
(unless (or (not vars) (null? vars))
(register-type-variance! name (map (lambda (_) Constant) vars))))
(register-type-variance! name (map (lambda (_) variance:const) vars))))

View File

@ -1,11 +1,11 @@
#lang racket/unit
(require "../utils/utils.rkt"
(types abbrev union subtype)
(types abbrev subtype)
racket/dict
"fail.rkt" "signatures.rkt" "constraint-structs.rkt"
racket/match
racket/list)
"fail.rkt" "signatures.rkt" "constraint-structs.rkt"
racket/match
racket/list)
(import intersect^ dmap^)
(export constraints^)

View File

@ -10,23 +10,21 @@
(require "../utils/utils.rkt"
(except-in
(combine-in
(utils tc-utils)
(utils tc-utils hset)
(rep free-variance type-rep prop-rep object-rep
values-rep rep-utils type-mask)
(types utils abbrev numeric-tower union subtype resolve
(types utils abbrev numeric-tower subtype resolve
substitute generalize prefab)
(env index-env tvar-env))
make-env -> ->* one-of/c)
"constraint-structs.rkt"
"signatures.rkt" "fail.rkt"
"promote-demote.rkt"
racket/match racket/set
mzlib/etc
racket/match
(contract-req)
(for-syntax
racket/base
syntax/parse)
racket/dict
racket/hash racket/list)
(import dmap^ constraints^)
@ -41,8 +39,7 @@
;; Type Type -> Pair<Seq, Seq>
;; construct a pair for the set of seen type pairs
(define (seen-before s t)
(cons (Rep-seq s) (Rep-seq t)))
(define seen-before cons)
;; Context, contains which type variables and indices to infer and which cannot be mentioned in
;; constraints.
@ -88,27 +85,24 @@
;; Add the type pair to the set of seen type pairs
(define/cond-contract (remember s t A)
((or/c AnyValues? Values/c ValuesDots?) (or/c AnyValues? Values/c ValuesDots?)
(listof (cons/c exact-nonnegative-integer?
exact-nonnegative-integer?))
(listof (cons/c Rep? Rep?))
. -> .
(listof (cons/c exact-nonnegative-integer?
exact-nonnegative-integer?)))
(listof (cons/c Rep? Rep?)))
(cons (seen-before s t) A))
;; Type Type -> Boolean
;; Check if a given type pair have been seen before
(define/cond-contract (seen? s t cs)
((or/c AnyValues? Values/c ValuesDots?) (or/c AnyValues? Values/c ValuesDots?)
(listof (cons/c exact-nonnegative-integer?
exact-nonnegative-integer?))
(listof (cons/c Rep? Rep?))
. -> . any/c)
(member (seen-before s t) cs))
;; (CMap DMap -> Pair<CMap, DMap>) CSet -> CSet
;; Map a function over a constraint set
(define (map/cset f cset)
(% make-cset (for/list/fail ([(cmap dmap) (in-dict (cset-maps cset))])
(f cmap dmap))))
(% make-cset (for/list/fail ([cmap/dmap (in-list (cset-maps cset))])
(f (car cmap/dmap) (cdr cmap/dmap)))))
;; Symbol DCon -> DMap
;; Construct a dmap containing only a single mapping
@ -192,7 +186,7 @@
(define (List->end v)
(match v
[(== -Null type-equal?) (null-end)]
[(== -Null) (null-end)]
[(Listof: t) (uniform-end t)]
[(ListDots: t dbound) (dotted-end t dbound)]
[_ #f]))
@ -430,7 +424,7 @@
(define cs (current-seen))
;; if we've been around this loop before, we're done (for rec types)
(cond
[(type-equal? S T) empty] ;; (CG-Refl)
[(equal? S T) empty] ;; (CG-Refl)
[(Univ? T) empty] ;; CG-Top
[(seen? S T cs) empty]
[else
@ -448,11 +442,12 @@
(ValuesDots: (list (Result: _ psets _) ...) _ _))
(AnyValues: q))
(cset-join
(filter identity
(for/list ([pset (in-list psets)])
(match pset
[(PropSet: p+ p-)
(% cset-meet (cgen/prop context p+ q) (cgen/prop context p- q))]))))]
(for*/list ([pset (in-list psets)]
[cs (in-value (% cset-meet
(cgen/prop context (PropSet-thn pset) q)
(cgen/prop context (PropSet-els pset) q)))]
#:when cs)
cs))]
;; check all non Type? first so that calling subtype is safe
@ -532,28 +527,28 @@
;; find *an* element of elems which can be made a subtype of T
[((Intersection: ts) T)
(cset-join
(for*/list ([t (in-list ts)]
(for*/list ([t (in-hset 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-list ts)]) (cg S ts)))
(define cs (for/list/fail ([ts (in-hset 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-list es)]) (cg e T)))
(define cs (for/list/fail ([e (in-hset es)]) (cg e T)))
(and cs (cset-meet* (cons empty cs)))]
;; 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 '()))))
(and (Bottom:) (bind es (hset)))))
(cset-join
(for*/list ([e (in-list es)]
(for*/list ([e (in-hset es)]
[v (in-value (cg S e))]
#:when v)
v))]
@ -608,7 +603,7 @@
;; To check that mutable pair is a sequence we check that the cdr is
;; both an mutable list and a sequence
[((MPair: t1 t2) (Sequence: (list t*)))
(% cset-meet (cg t1 t*) (cg t2 T) (cg t2 (Un -Null (make-MPairTop))))]
(% cset-meet (cg t1 t*) (cg t2 T) (cg t2 (Un -Null -MPairTop)))]
[((List: ts) (Sequence: (list t*)))
(% cset-meet* (for/list/fail ([t (in-list ts)])
(cg t t*)))]
@ -653,9 +648,9 @@
;; resolve applications
[((App: _ _ _) _)
[((App: _ _) _)
(% cg (resolve-once S) T)]
[(_ (App: _ _ _))
[(_ (App: _ _))
(% cg S (resolve-once T))]
;; If the struct names don't match, try the parent of S
@ -755,13 +750,21 @@
;; nothing worked, and we fail
#f]))]))
;; C : cset? - set of constraints found by the inference engine
;; X : (listof symbol?) - type variables that must have entries
;; Y : (listof symbol?) - index variables that must have entries
;; R : Type? - result type into which we will be substituting
(define/cond-contract (subst-gen C X Y R)
(cset? (listof symbol?) (listof symbol?) (or/c Values/c AnyValues? ValuesDots?)
. -> . (or/c #f substitution/c))
;; C : set of constraints found by the inference engine
;; X : type variables that must have entries
;; Y : index variables that must have entries
;; R : result type into which we will be substituting
;; multiple-substitutions? : should we return one substitution (#f), or
;; all the substitutions that were possible? (#t)
;; NOTE: multiple substitutions are rare -- at the time of adding this
;; parameter this feature is only used by the tc-app/list.
;; NOTE: if multiple substitutions is #t, a list is returned,
;; otherwise a single substitution (not in a list) is returned.
(define/cond-contract (substs-gen C X Y R multiple-substitutions?)
(cset? (listof symbol?) (listof symbol?) (or/c Values/c AnyValues? ValuesDots?) boolean?
. -> . (or/c substitution/c
(cons/c substitution/c
(listof substitution/c))))
(define var-hash (free-vars-hash (free-vars* R)))
(define idx-hash (free-vars-hash (free-idxs* R)))
;; c : Constaint
@ -769,15 +772,14 @@
(define (constraint->type v variance)
(match v
[(c S T)
(evcase variance
[Constant S]
[Covariant S]
[Contravariant T]
[Invariant
(let ([gS (generalize S)])
(if (subtype gS T)
gS
S))])]))
(match variance
[(? variance:const?) S]
[(? variance:co?) S]
[(? variance:contra?) T]
[(? variance:inv?) (let ([gS (generalize S)])
(if (subtype gS T)
gS
S))])]))
;; Since we don't add entries to the empty cset for index variables (since there is no
;; widest constraint, due to dcon-exacts), we must add substitutions here if no constraint
@ -787,46 +789,50 @@
(hash-union
(for/hash ([v (in-list Y)]
#:unless (hash-has-key? S v))
(let ([var (hash-ref idx-hash v Constant)])
(let ([var (hash-ref idx-hash v variance:const)])
(values v
(evcase var
[Constant (i-subst null)]
[Covariant (i-subst null)]
[Contravariant (i-subst/starred null Univ)]
;; TODO figure out if there is a better subst here
[Invariant (i-subst null)]))))
(match var
[(? variance:const?) (i-subst null)]
[(? variance:co?) (i-subst null)]
[(? variance:contra?) (i-subst/starred null Univ)]
;; TODO figure out if there is a better subst here
[(? variance:inv) (i-subst null)]))))
S))
(match (car (cset-maps C))
[(cons cmap (dmap dm))
(let* ([subst (hash-union
(for/hash ([(k dc) (in-hash dm)])
(define (c->t c) (constraint->type c (hash-ref idx-hash k Constant)))
(values
k
(match dc
[(dcon fixed #f)
(i-subst (map c->t fixed))]
[(or (dcon fixed rest) (dcon-exact fixed rest))
(i-subst/starred
(map c->t fixed)
(c->t rest))]
[(dcon-dotted fixed dc dbound)
(i-subst/dotted
(map c->t fixed)
(c->t dc)
dbound)])))
(for/hash ([(k v) (in-hash cmap)])
(values k (t-subst (constraint->type v (hash-ref var-hash k Constant))))))]
[subst (for/fold ([subst subst]) ([v (in-list X)])
(let ([entry (hash-ref subst v #f)])
;; Make sure we got a subst entry for a type var
;; (i.e. just a type to substitute)
;; If we don't have one, there are no constraints on this variable
(if (and entry (t-subst? entry))
subst
(hash-set subst v (t-subst Univ)))))])
;; verify that we got all the important variables
(extend-idxs subst))]))
(define (build-subst m)
(match m
[(cons cmap (dmap dm))
(let* ([subst (hash-union
(for/hash ([(k dc) (in-hash dm)])
(define (c->t c) (constraint->type c (hash-ref idx-hash k variance:const)))
(values
k
(match dc
[(dcon fixed #f)
(i-subst (map c->t fixed))]
[(or (dcon fixed rest) (dcon-exact fixed rest))
(i-subst/starred
(map c->t fixed)
(c->t rest))]
[(dcon-dotted fixed dc dbound)
(i-subst/dotted
(map c->t fixed)
(c->t dc)
dbound)])))
(for/hash ([(k v) (in-hash cmap)])
(values k (t-subst (constraint->type v (hash-ref var-hash k variance:const))))))]
[subst (for/fold ([subst subst]) ([v (in-list X)])
(let ([entry (hash-ref subst v #f)])
;; Make sure we got a subst entry for a type var
;; (i.e. just a type to substitute)
;; If we don't have one, there are no constraints on this variable
(if (and entry (t-subst? entry))
subst
(hash-set subst v (t-subst Univ)))))])
;; verify that we got all the important variables
(extend-idxs subst))]))
(if multiple-substitutions?
(map build-subst (cset-maps C))
(build-subst (car (cset-maps C)))))
;; context : the context of what to infer/not infer
;; S : a list of types to be the subtypes of T
@ -858,11 +864,13 @@
;; just return a boolean result
(define infer
(let ()
(define/cond-contract (infer X Y S T R [expected #f])
(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?))
. ->* . (or/c boolean? substitution/c))
((or/c #f Values/c AnyValues? ValuesDots?)
#:multiple? boolean?)
. ->* . (or/c #f substitution/c (cons/c substitution/c
(listof substitution/c))))
(define ctx (context null X Y ))
(define expected-cset
(if expected
@ -871,7 +879,10 @@
(and expected-cset
(let* ([cs (cgen/list ctx S T #:expected-cset expected-cset)]
[cs* (% cset-meet cs expected-cset)])
(and cs* (if R (subst-gen cs* X Y R) #t)))))
(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
;; like infer, but T-var is the vararg type:
@ -905,4 +916,12 @@
#:return-unless cs #f
(define m (cset-meet cs expected-cset))
#:return-unless m #f
(subst-gen m X (list dotted-var) R)))
(substs-gen m X (list dotted-var) R #f)))
;(trace subst-gen)
;(trace cgen)
;(trace cgen/list)
;(trace cgen/arr)
;(trace cgen/seq)

View File

@ -1,8 +1,9 @@
#lang racket/unit
(require "../utils/utils.rkt")
(require (rep type-rep type-mask)
(types abbrev base-abbrev union subtype resolve overlap)
(require "../utils/utils.rkt"
(utils hset)
(rep type-rep type-mask rep-utils)
(types abbrev base-abbrev subtype resolve overlap)
"signatures.rkt"
racket/match
racket/set)
@ -15,9 +16,6 @@
;; a non-additive intersection computation defined below
;; (i.e. only parts of t1 will remain, no parts from t2 are added))
(define (intersect t1 t2)
;; build-type: build a type while propogating bottom
(define (build-type constructor . args)
(if (memf Bottom? args) -Bottom (apply constructor args)))
(cond
;; we dispatch w/ Error first, because it behaves in
;; strange ways (e.g. it is and ⊥ w.r.t subtyping) and
@ -36,11 +34,11 @@
(define (rec t1 t2) (intersect t1 t2 seen))
(match* (t1 t2)
;; quick overlap check
[(_ _) #:when (disjoint-masks? (Type-mask t1) (Type-mask t2)) -Bottom]
[(_ _) #:when (disjoint-masks? (mask t1) (mask t2)) -Bottom]
;; already a subtype
[(t1 t2) #:when (subtype t1 t2) t1]
[(t1 t2) #:when (subtype t2 t1) t2]
[(_ _) #:when (subtype t1 t2) t1]
[(_ _) #:when (subtype t2 t1) t2]
;; polymorphic intersect
@ -53,32 +51,32 @@
;; structural recursion on types
[((Pair: a1 d1) (Pair: a2 d2))
(build-type -pair (rec a1 a2) (rec d1 d2))]
(-pair (rec a1 a2) (rec d1 d2))]
;; FIXME: support structural updating for structs when structs are updated to
;; contain not only *if* they are polymorphic, but *which* fields are too
;;[((Struct: _ _ _ _ _ _)
;; (Struct: _ _ _ _ _ _))]
[((Syntax: t1*) (Syntax: t2*))
(build-type -Syntax (rec t1* t2*))]
(-Syntax (rec t1* t2*))]
[((Promise: t1*) (Promise: t2*))
(build-type -Promise (rec t1* t2*))]
(-Promise (rec t1* t2*))]
[((Union: t1s) t2)
(match t2
;; let's be consistent in slamming together unions
;; (i.e. if we don't do this dual traversal, the order the
;; unions are passed to 'intersect' can produces different
;; albeit equivalent (modulo subtyping, we hope) answers)
[(Union: t2s) (apply Un (for*/list ([t1 (in-list t1s)]
[t2 (in-list t2s)])
(rec t1 t2)))]
[_ (apply Un (map (λ (t1) (rec t1 t2)) t1s))])]
[(t1 (Union: t2s)) (apply Un (map (λ (t2) (rec t1 t2)) t2s))]
;; (albeit equivalent modulo subtyping, we believe) answers)
[(Union: t2s) (make-Union (for*/hset ([t1 (in-hset t1s)]
[t2 (in-hset t2s)])
(rec t1 t2)))]
[_ (Union-map t1s (λ (t1) (rec t1 t2)))])]
[(t1 (Union: t2s)) (Union-map t2s (λ (t2) (rec t1 t2)))]
[((Intersection: t1s) t2)
(apply -unsafe-intersect (map (λ (t1) (rec t1 t2)) t1s))]
(apply -unsafe-intersect (hset-map t1s (λ (t1) (rec t1 t2))))]
[(t1 (Intersection: t2s))
(apply -unsafe-intersect (map (λ (t2) (rec t1 t2)) t2s))]
(apply -unsafe-intersect (hset-map t2s (λ (t2) (rec t1 t2))))]
;; For resolvable types, we record the occurrence and save a back pointer
;; in 'seen'. Then, if this pair of types emerges again, we know that we are
@ -166,10 +164,10 @@
;; unions
[((Union: t1s) t2)
(apply Un (map (λ (t1) (restrict t1 t2 resolved)) t1s))]
(Union-map t1s (λ (t1) (restrict t1 t2 resolved)))]
[(t1 (Union: t2s))
(apply Un (map (λ (t2) (restrict t1 t2 resolved)) t2s))]
(Union-map t2s (λ (t2) (restrict t1 t2 resolved)))]
;; restrictions
[((Intersection: t1s) t2)

View File

@ -53,18 +53,17 @@
(and drest (cons (contra (car drest)) (cdr drest)))
(map contra kws))])]))
(match cur
[(? structural? t)
(define mk (Rep-constructor t))
(apply mk (for/list ([t (in-list (Rep-values t))]
[v (in-list (Type-variances t))])
(cond
[(eq? v Covariant) (co t)]
[(eq? v Invariant)
[(app Rep-variances variances) #:when variances
(define mk (Rep-constructor cur))
(apply mk (for/list ([t (in-list (Rep-values cur))]
[v (in-list variances)])
(match v
[(? variance:co?) (co t)]
[(? variance:inv?)
(if (V-in? V t)
(if change Univ -Bottom)
t)]
[(eq? v Contravariant)
(contra t)])))]
[(? variance:contra?) (contra t)])))]
[(Unit: imports exports init-depends t)
(make-Unit (map co imports)
(map contra imports)
@ -80,4 +79,4 @@
(if change Univ -Bottom)
t))
elems))]
[_ (Rep-fold co cur)]))
[_ (Rep-fmap cur co)]))

View File

@ -36,7 +36,9 @@
;; range
(or/c #f Values/c ValuesDots?))
;; optional expected type
((or/c #f Values/c AnyValues? ValuesDots?))
((or/c #f Values/c AnyValues? ValuesDots?)
;; optional multiple substitutions?
#:multiple? boolean?)
. ->* . any)]
[cond-contracted infer/vararg ((;; variables from the forall
(listof symbol?)

View File

@ -5,7 +5,8 @@
"../utils/utils.rkt"
(for-template racket/base racket/fixnum racket/unsafe/ops)
(for-syntax racket/base syntax/parse racket/syntax)
(types numeric-tower union)
(rep type-rep)
(types numeric-tower)
(optimizer utils logging))
(provide fixnum-expr fixnum-opt-expr)

View File

@ -5,7 +5,7 @@
(for-template racket/base racket/flonum racket/unsafe/ops racket/math)
"../utils/utils.rkt"
(utils tc-utils)
(types numeric-tower union abbrev)
(types numeric-tower abbrev)
(optimizer utils numeric-utils logging fixnum))
(provide float-opt-expr float-arg-expr int-expr float-op)

View File

@ -4,7 +4,7 @@
syntax/parse/experimental/specialize
(for-template racket/base)
"../utils/utils.rkt"
(types numeric-tower union)
(types abbrev numeric-tower)
(optimizer utils logging))
(provide number-opt-expr)

View File

@ -14,9 +14,9 @@
(define-syntax-class/specialize string-expr
(typed-expr (λ (t) (type-equal? t -String))))
(typed-expr (λ (t) (equal? t -String))))
(define-syntax-class/specialize bytes-expr
(typed-expr (λ (t) (type-equal? t -Bytes))))
(typed-expr (λ (t) (equal? t -Bytes))))
(define-syntax-class/specialize list-expr
(typed-expr (λ (t)
(match t

View File

@ -41,7 +41,7 @@
;; similar, but with type equality
(define (isoftype? s t)
(match (type-of s)
[(tc-result1: (== t type-equal?)) #t] [_ #f]))
[(tc-result1: (== t)) #t] [_ #f]))
;; generates a table matching safe to unsafe promitives
(define (mk-unsafe-tbl generic safe-pattern unsafe-pattern)

View File

@ -4,11 +4,11 @@
(require (rename-in "../utils/utils.rkt" [infer infer-in])
(except-in (rep core-rep type-rep object-rep) make-arr)
(rename-in (types abbrev union utils prop-ops resolve
(rename-in (types abbrev utils prop-ops resolve
classes prefab signatures)
[make-arr* make-arr])
(only-in (infer-in infer) intersect)
(utils tc-utils stxclass-util literal-syntax-class)
(utils tc-utils stxclass-util literal-syntax-class hset)
syntax/stx (prefix-in c: (contract-req))
syntax/parse racket/sequence
(env tvar-env type-alias-env mvar-env
@ -236,9 +236,9 @@
(define-syntax-class path-elem
#:description "path element"
(pattern :car^
#:attr pe (make-CarPE))
#:attr pe -car)
(pattern :cdr^
#:attr pe (make-CdrPE)))
#:attr pe -cdr))
(define-syntax-class @
@ -453,9 +453,10 @@
(define productive
(let loop ((ty t*))
(match ty
[(Union: elems) (andmap loop elems)]
[(Union: elems) (for/and ([elem (in-hset elems)]) (loop elem))]
[(Intersection: elems) (for/and ([elem (in-hset elems)]) (loop elem))]
[(F: _) (not (equal? ty tvar))]
[(App: rator rands stx)
[(App: rator rands)
(loop (resolve-app rator rands stx))]
[(Mu: _ body) (loop body)]
[(Poly: names body) (loop body)]
@ -629,7 +630,10 @@
[args (parse-types #'(arg args ...))])
(resolve-app-check-error rator args stx)
(match rator
[(? Name?) (make-App rator args stx)]
[(? Name?)
(define app (make-App rator args))
(register-app-for-checking! app stx)
app]
[(Poly: _ _) (instantiate-poly rator args)]
[(Mu: _ _) (loop (unfold rator) args)]
[(Error:) Err]
@ -904,8 +908,7 @@
(unbox class-box)))
;; Ok to return Error here, since this type will
;; get reparsed in another pass
(make-Error)
])]))
Err])]))
;; get-parent-inits : (U Type #f) -> Inits
;; Extract the init arguments out of a parent class type

View File

@ -4,7 +4,7 @@
(rep type-rep)
(utils tc-utils)
(env global-env mvar-env)
(except-in (types subtype abbrev union utils generalize)
(except-in (types subtype abbrev utils generalize)
-> ->* one-of/c)
(private parse-type syntax-properties)
(contract-req)
@ -29,7 +29,7 @@
let-binding)
(define t1 (parse-type/id stx prop))
(define t2 (lookup-type stx (lambda () #f)))
(when (and t2 (not (type-equal? t1 t2)))
(when (and t2 (not (equal? t1 t2)))
(maybe-finish-register-type stx)
(tc-error/delayed #:stx stx "Duplicate type annotation of ~a for ~a, previous was ~a" t1 (syntax-e stx) t2)))
(if (syntax? prop)

View File

@ -6,11 +6,10 @@
"../utils/utils.rkt"
syntax/parse
(rep type-rep prop-rep object-rep)
(utils tc-utils)
(utils tc-utils hset)
(env type-name-env row-constraint-env)
(rep core-rep rep-utils type-mask values-rep)
(types resolve union utils printer)
(only-in (types abbrev) -Dead-Code)
(types resolve utils printer match-expanders union)
(prefix-in t: (types abbrev numeric-tower subtype))
(private parse-type syntax-properties)
racket/match racket/syntax racket/list
@ -84,7 +83,7 @@
(define (generate-contract-def stx cache sc-cache)
(define prop (get-contract-def-property stx))
(match-define (contract-def type-stx flat? maker? typed-side) prop)
(define *typ (if type-stx (parse-type type-stx) -Dead-Code))
(define *typ (if type-stx (parse-type type-stx) t:-Dead-Code))
(define kind (if (and type-stx flat?) 'flat 'impersonator))
(syntax-parse stx #:literals (define-values)
[(define-values (n) _)
@ -320,7 +319,7 @@
[(_ sc-cache type-expr typed-side-expr match-clause ...)
#'(let ([type type-expr]
[typed-side typed-side-expr])
(define key (cons (Rep-seq type) typed-side))
(define key (cons type typed-side))
(cond [(hash-ref sc-cache key #f)]
[else
(define sc (match type match-clause ...))
@ -359,7 +358,7 @@
;; We special case this rather than just resorting to standard
;; App resolution (see case below) because the resolution process
;; will make type->static-contract infinite loop.
[(App: (Name: name _ #f) _ _)
[(App: (Name: name _ #f) _)
;; Key with (cons name 'app) instead of just name because the
;; application of the Name is not necessarily the same as the
;; Name type alone
@ -388,27 +387,29 @@
(λ () (loop resolved-name 'both rv)))
(lookup-name-sc type typed-side)])]
;; Ordinary type applications or struct type names, just resolve
[(or (App: _ _ _) (Name/struct:)) (t->sc (resolve-once type))]
[(or (App: _ _) (Name/struct:)) (t->sc (resolve-once type))]
[(Univ:) (if (from-typed? typed-side) any-wrap/sc any/sc)]
[(Bottom:) (or/sc)]
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
(listof/sc (t->sc elem-ty))]
[(Listof: elem-ty) (listof/sc (t->sc elem-ty))]
[(Base: sym cnt _ _)
(flat/sc #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt)) sym)]
[(Distinction: _ _ t) ; from define-new-subtype
(t->sc t)]
[(Refinement: par p?)
(and/sc (t->sc par) (flat/sc p?))]
[(Union: elems)
(define-values (numeric non-numeric) (partition (λ (t) (eq? mask:number (Type-mask t))) elems))
(define numeric-sc (numeric-type->static-contract (apply Un numeric)))
(if numeric-sc
(apply or/sc numeric-sc (map t->sc non-numeric))
(apply or/sc (map t->sc elems)))]
[(? Union? t)
(match (normalize-type t)
[(Union: (app hset->list elems))
(define-values (numeric non-numeric) (partition (λ (t) (eq? mask:number (mask t))) elems))
(define numeric-sc (numeric-type->static-contract (apply Un numeric)))
(if numeric-sc
(apply or/sc numeric-sc (map t->sc non-numeric))
(apply or/sc (map t->sc elems)))]
[t (t->sc t)])]
[(Intersection: ts)
(define-values (chaperones/impersonators others)
(for/fold ([cs/is null] [others null])
([elem (in-list ts)])
([elem (in-hset ts)])
(define c (t->sc elem))
(if (equal? flat-sym (get-max-contract-kind c))
(values cs/is (cons c others))
@ -782,7 +783,8 @@
(let loop ([ty b])
(match (resolve ty)
[(Function: _) #t]
[(Union: elems) (andmap loop elems)]
[(Union: elems) (for/and ([elem (in-hset elems)]) (loop elem))]
[(Intersection: elems) (for/or ([elem (in-hset elems)]) (loop elem))]
[(Poly: _ body) (loop body)]
[(PolyDots: _ body) (loop body)]
[_ #f])))
@ -820,7 +822,8 @@
(let loop ([ty b])
(match (resolve ty)
[(Function: _) #t]
[(Union: elems) (andmap loop elems)]
[(Union: elems) (for/and ([elem (in-hset elems)]) (loop elem))]
[(Intersection: elems) (for/or ([elem (in-hset elems)]) (loop elem))]
[(Poly: _ body) (loop body)]
[(PolyDots: _ body) (loop body)]
[_ #f])))
@ -843,8 +846,8 @@
(let/ec escape
(let loop ([rep type])
(match rep
[(App: (Name: _ _ #f) _ _) (escape #t)]
[_ (Rep-walk loop rep)]))
[(App: (Name: _ _ #f) _) (escape #t)]
[_ (Rep-for-each rep loop)]))
#f))
;; True if the arities `arrs` are what we'd expect from a struct predicate
@ -940,52 +943,52 @@
;; numeric special cases
;; since often-used types like Integer are big unions, this would
;; generate large contracts.
[(== t:-PosByte type-equal?) positive-byte/sc]
[(== t:-Byte type-equal?) byte/sc]
[(== t:-PosIndex type-equal?) positive-index/sc]
[(== t:-Index type-equal?) index/sc]
[(== t:-PosFixnum type-equal?) positive-fixnum/sc]
[(== t:-NonNegFixnum type-equal?) nonnegative-fixnum/sc]
[(== t:-PosByte) positive-byte/sc]
[(== t:-Byte) byte/sc]
[(== t:-PosIndex) positive-index/sc]
[(== t:-Index) index/sc]
[(== t:-PosFixnum) positive-fixnum/sc]
[(== t:-NonNegFixnum) nonnegative-fixnum/sc]
;; -NegFixnum is a base type
[(== t:-NonPosFixnum type-equal?) nonpositive-fixnum/sc]
[(== t:-Fixnum type-equal?) fixnum/sc]
[(== t:-PosInt type-equal?) positive-integer/sc]
[(== t:-Nat type-equal?) natural/sc]
[(== t:-NegInt type-equal?) negative-integer/sc]
[(== t:-NonPosInt type-equal?) nonpositive-integer/sc]
[(== t:-Int type-equal?) integer/sc]
[(== t:-PosRat type-equal?) positive-rational/sc]
[(== t:-NonNegRat type-equal?) nonnegative-rational/sc]
[(== t:-NegRat type-equal?) negative-rational/sc]
[(== t:-NonPosRat type-equal?) nonpositive-rational/sc]
[(== t:-Rat type-equal?) rational/sc]
[(== t:-FlonumZero type-equal?) flonum-zero/sc]
[(== t:-NonNegFlonum type-equal?) nonnegative-flonum/sc]
[(== t:-NonPosFlonum type-equal?) nonpositive-flonum/sc]
[(== t:-Flonum type-equal?) flonum/sc]
[(== t:-SingleFlonumZero type-equal?) single-flonum-zero/sc]
[(== t:-InexactRealZero type-equal?) inexact-real-zero/sc]
[(== t:-PosInexactReal type-equal?) positive-inexact-real/sc]
[(== t:-NonNegSingleFlonum type-equal?) nonnegative-single-flonum/sc]
[(== t:-NonNegInexactReal type-equal?) nonnegative-inexact-real/sc]
[(== t:-NegInexactReal type-equal?) negative-inexact-real/sc]
[(== t:-NonPosSingleFlonum type-equal?) nonpositive-single-flonum/sc]
[(== t:-NonPosInexactReal type-equal?) nonpositive-inexact-real/sc]
[(== t:-SingleFlonum type-equal?) single-flonum/sc]
[(== t:-InexactReal type-equal?) inexact-real/sc]
[(== t:-RealZero type-equal?) real-zero/sc]
[(== t:-PosReal type-equal?) positive-real/sc]
[(== t:-NonNegReal type-equal?) nonnegative-real/sc]
[(== t:-NegReal type-equal?) negative-real/sc]
[(== t:-NonPosReal type-equal?) nonpositive-real/sc]
[(== t:-Real type-equal?) real/sc]
[(== t:-ExactNumber type-equal?) exact-number/sc]
[(== t:-InexactComplex type-equal?) inexact-complex/sc]
[(== t:-Number type-equal?) number/sc]
[(== t:-ExtFlonumZero type-equal?) extflonum-zero/sc]
[(== t:-NonNegExtFlonum type-equal?) nonnegative-extflonum/sc]
[(== t:-NonPosExtFlonum type-equal?) nonpositive-extflonum/sc]
[(== t:-ExtFlonum type-equal?) extflonum/sc]
[(== t:-NonPosFixnum) nonpositive-fixnum/sc]
[(== t:-Fixnum) fixnum/sc]
[(== t:-PosInt) positive-integer/sc]
[(== t:-Nat) natural/sc]
[(== t:-NegInt) negative-integer/sc]
[(== t:-NonPosInt) nonpositive-integer/sc]
[(== t:-Int) integer/sc]
[(== t:-PosRat) positive-rational/sc]
[(== t:-NonNegRat) nonnegative-rational/sc]
[(== t:-NegRat) negative-rational/sc]
[(== t:-NonPosRat) nonpositive-rational/sc]
[(== t:-Rat) rational/sc]
[(== t:-FlonumZero) flonum-zero/sc]
[(== t:-NonNegFlonum) nonnegative-flonum/sc]
[(== t:-NonPosFlonum) nonpositive-flonum/sc]
[(== t:-Flonum) flonum/sc]
[(== t:-SingleFlonumZero) single-flonum-zero/sc]
[(== t:-InexactRealZero) inexact-real-zero/sc]
[(== t:-PosInexactReal) positive-inexact-real/sc]
[(== t:-NonNegSingleFlonum) nonnegative-single-flonum/sc]
[(== t:-NonNegInexactReal) nonnegative-inexact-real/sc]
[(== t:-NegInexactReal) negative-inexact-real/sc]
[(== t:-NonPosSingleFlonum) nonpositive-single-flonum/sc]
[(== t:-NonPosInexactReal) nonpositive-inexact-real/sc]
[(== t:-SingleFlonum) single-flonum/sc]
[(== t:-InexactReal) inexact-real/sc]
[(== t:-RealZero) real-zero/sc]
[(== t:-PosReal) positive-real/sc]
[(== t:-NonNegReal) nonnegative-real/sc]
[(== t:-NegReal) negative-real/sc]
[(== t:-NonPosReal) nonpositive-real/sc]
[(== t:-Real) real/sc]
[(== t:-ExactNumber) exact-number/sc]
[(== t:-InexactComplex) inexact-complex/sc]
[(== t:-Number) number/sc]
[(== t:-ExtFlonumZero) extflonum-zero/sc]
[(== t:-NonNegExtFlonum) nonnegative-extflonum/sc]
[(== t:-NonPosExtFlonum) nonpositive-extflonum/sc]
[(== t:-ExtFlonum) extflonum/sc]
[else #f]))

View File

@ -20,7 +20,7 @@
(for-syntax racket/base racket/syntax
syntax/parse))
(provide Type Type-mask Type-subtype-cache Type?
(provide Type Type?
Prop Prop?
Object Object? OptObject?
PathElem PathElem?
@ -29,22 +29,8 @@
def-values
def-prop
def-object
def-pathelem
type-equal?
prop-equal?
object-equal?)
def-pathelem)
(define-syntax type-equal? (make-rename-transformer #'eq?))
(define-syntax prop-equal? (make-rename-transformer #'eq?))
(define-syntax object-equal? (make-rename-transformer #'eq?))
(provide-for-cond-contract name-ref/c)
;; A Name-Ref is any value that represents an object.
;; As an identifier, it represents a free variable in the environment
;; As a pair, it represents a De Bruijn indexed bound variable (cons lvl arg-num)
(define-for-cond-contract name-ref/c
(or/c identifier? (cons/c natural-number/c natural-number/c)))
;;************************************************************
;; Custom Printing Tools
@ -55,32 +41,40 @@
print-prop print-object print-pathelem
print-values print-propset print-result)])
;; Note: We eta expand the printer so it is not evaluated until needed.
(define-syntax (struct/printer stx)
;; comment out the above lazy-require and uncomment the following
;; s-exp for simple debug printing of Rep structs
#;(begin
(define (debug-printer rep port write?)
(display (cons (Rep-name rep) (Rep-values rep)) port))
(define print-type debug-printer)
(define print-prop debug-printer)
(define print-object debug-printer)
(define print-pathelem debug-printer)
(define print-values debug-printer)
(define print-propset debug-printer)
(define print-result debug-printer))
(define-syntax (def-rep-class stx)
(syntax-parse stx
[(_ name:id
(flds:id ...)
printer:id)
#:printer printer:id
#:define-form def:id)
(with-syntax ([mk (generate-temporary 'dont-use-me)])
(syntax/loc
(quasisyntax/loc
stx
(struct name Rep (flds ...)
#:constructor-name mk
#:transparent
#:property prop:custom-print-quotable 'never
#:methods gen:custom-write
[(define (write-proc v port write?) (printer v port write?))])))]))
(define-syntax (build-rep-definer syntax)
(syntax-parse syntax
[(_ class:id def-id:id)
(syntax/loc syntax
(define-syntax (def-id stx)
(syntax-parse stx
[(_ variant:id flds:expr . rst)
(syntax/loc stx
(def-rep variant flds [#:parent class] . rst))])))]))
(begin (struct name ()
#:constructor-name mk
#:transparent
#:property prop:custom-print-quotable 'never
#:methods gen:custom-write
;; Note: We eta expand the printer so it is not evaluated until needed.
[(define (write-proc v port write?) (printer v port write?))])
(define-syntax (def stx)
(syntax-parse stx
[(_ variant:id flds:expr . rst)
(syntax/loc stx
(def-rep variant flds [#:parent name] . rst))])))))]))
;;
;; These structs are the 'meta-variables' of TR's internal grammar,
@ -95,18 +89,9 @@
;;************************************************************
;; Types
;;************************************************************
;;
;;
;; The 'mask' field that is used for quick-checking of certain
;; properties. See type-mask.rkt for details.
;; subtype-cache - for a given type τ, the subtype-cache
;; is a mapping from Type -> boolean, s.t. if
;; τ.subtype-cache[σ] = #t then τ <: σ holds, otherwise
;; if τ.subtype-cache[σ] = #f, then τ <: σ does not hold
;; mask - the type mask for this type
(struct/printer Type (subtype-cache mask) print-type)
(build-rep-definer Type def-type)
(def-rep-class Type #:printer print-type #:define-form def-type)
;;-----------------
;; Universal Type
@ -114,15 +99,17 @@
;; the type of all well-typed terms
;; (called Any in user programs)
(def-type Univ () #:base
[#:type-mask mask:unknown])
(def-type Univ ()
[#:mask mask:unknown]
[#:singleton Univ])
;;-----------------
;; Bottom Type
;;-----------------
(def-type Bottom () #:base
[#:type-mask mask:bottom])
(def-type Bottom ()
[#:mask mask:bottom]
[#:singleton -Bottom])
;;************************************************************
;; Prop
@ -130,13 +117,10 @@
;;
;; These convey learned information about program terms while
;; typechecking.
(def-rep-class Prop #:printer print-prop #:define-form def-prop)
(struct/printer Prop () print-prop)
(build-rep-definer Prop def-prop)
(def-prop TrueProp () #:base)
(def-prop FalseProp () #:base)
(def-prop TrueProp () [#:singleton -tt])
(def-prop FalseProp () [#:singleton -ff])
;;************************************************************
;; Fields and Symbolic Objects
@ -151,19 +135,17 @@
;;--------------
;; e.g. car, cdr, etc
(struct/printer PathElem () print-pathelem)
(build-rep-definer PathElem def-pathelem)
(def-rep-class PathElem #:printer print-pathelem #:define-form def-pathelem)
;;----------
;; Objects
;;----------
(struct/printer Object () print-object)
(build-rep-definer Object def-object)
(def-rep-class Object #:printer print-object #:define-form def-object)
;; empty object
(def-rep Empty () #:base
(def-rep Empty ()
[#:singleton -empty-obj]
[#:extras
#:property prop:custom-print-quotable 'never
#:methods gen:custom-write
@ -181,9 +163,7 @@
;;
;; Racket expressions can produce 0 or more values, 'SomeValues'
;; represents the general class of all these possibilities
(struct/printer SomeValues () print-values)
(build-rep-definer SomeValues def-values)
(def-rep-class SomeValues #:printer print-values #:define-form def-values)
;;************************************************************
@ -198,10 +178,9 @@
(def-rep PropSet ([thn Prop?] [els Prop?])
[#:intern-key (cons (Rep-seq thn) (Rep-seq els))]
[#:frees (f) (combine-frees (list (f thn) (f els)))]
[#:fold (f) (make-PropSet (f thn) (f els))]
[#:walk (f) (begin (f thn) (f els))]
[#:fmap (f) (make-PropSet (f thn) (f els))]
[#:for-each (f) (begin (f thn) (f els))]
[#:extras
#:property prop:custom-print-quotable 'never
#:methods gen:custom-write
@ -223,10 +202,9 @@
(def-rep Result ([t Type?] [ps PropSet?] [o OptObject?])
[#:intern-key (list* (Rep-seq t) (Rep-seq ps) (Rep-seq o))]
[#:frees (f) (combine-frees (list (f t) (f ps) (f o)))]
[#:fold (f) (make-Result (f t) (f ps) (f o))]
[#:walk (f) (begin (f t) (f ps) (f o))]
[#:fmap (f) (make-Result (f t) (f ps) (f o))]
[#:for-each (f) (begin (f t) (f ps) (f o))]
[#:extras
#:property prop:custom-print-quotable 'never
#:methods gen:custom-write

View File

@ -9,7 +9,7 @@
(provide
;; Variances
Covariant Contravariant Invariant Constant Dotted
variance:co variance:contra variance:inv variance:const variance:dotted
variance? variance->binding
;; Construcing frees
@ -23,12 +23,21 @@
;; Examining frees
free-vars-hash
free-vars-names
free-vars-has-key?)
free-vars-has-key?
variance:co?
variance:contra?
variance:inv?
variance:const?
variance:dotted?)
;; this file contains support for calculating the free variables/indexes of types
;; actual computation is done in rep-utils.rkt and type-rep.rkt
(define-values (variance? Covariant Contravariant Invariant Constant Dotted)
(define-values (variance? variance:co
variance:contra
variance:inv
variance:const
variance:dotted)
(let ()
(define-struct Variance () #:transparent)
(define-struct (Covariant Variance) () #:transparent)
@ -39,19 +48,26 @@
(define-struct (Dotted Variance) () #:transparent)
(values Variance? (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant) (make-Dotted))))
(define (variance:co? x) (eq? x variance:co))
(define (variance:contra? x) (eq? x variance:contra))
(define (variance:inv? x) (eq? x variance:inv))
(define (variance:const? x) (eq? x variance:const))
(define (variance:dotted? x) (eq? x variance:dotted))
(define (variance->binding var)
(match var
((== Covariant) #'Covariant)
((== Contravariant) #'Contravariant)
((== Invariant) #'Invariant)
((== Constant) #'Constant)
((== Dotted) #'Dotted)))
[(? variance:co?) #'variance:co]
[(? variance:contra?) #'variance:contra]
[(? variance:inv?) #'variance:inv]
[(? variance:const?) #'variance:const]
[(? variance:dotted?) #'variance:dotted]))
(define (flip-variance v)
(match v
((== Covariant) Contravariant)
((== Contravariant) Covariant)
(else v)))
[(? variance:co?) variance:contra]
[(? variance:contra?) variance:co]
[_ v]))
;;All of these are used internally
;;Only combined-frees is used externally
@ -61,7 +77,7 @@
;; Base constructors
(define (single-free-var name (variance Covariant))
(define (single-free-var name [variance variance:co])
(combined-frees (hasheq name variance) null))
(define empty-free-vars
@ -89,13 +105,13 @@
(define (make-invariant frees)
(combined-frees
(for/hasheq ([name (free-vars-names frees)])
(values name Invariant))
(values name variance:inv))
null))
(define (make-constant frees)
(combined-frees
(for/hasheq ([name (free-vars-names frees)])
(values name Constant))
(values name variance:const))
null))
;; Listof[frees] -> frees
@ -141,11 +157,11 @@
(combine-hashes
(for/list ((var (lookup-type-variance name)) (arg args))
(free-vars-hash
(cond
[(eq? var Covariant) arg]
[(eq? var Contravariant) (flip-variances arg)]
[(eq? var Invariant) (make-invariant arg)]
[(eq? var Constant) (make-constant arg)]))))]))
(match var
[(? variance:co?) arg]
[(? variance:contra?) (flip-variances arg)]
[(? variance:inv?) (make-invariant arg)]
[(? variance:const?) (make-constant arg)]))))]))
;; frees = HT[Idx,Variance] where Idx is either Symbol or Number
@ -154,11 +170,11 @@
(define ((combine-var v) w)
(cond
[(eq? v w) v]
[(eq? v Dotted) w]
[(eq? w Dotted) v]
[(eq? v Constant) w]
[(eq? w Constant) v]
[else Invariant]))
[(variance:dotted? v) w]
[(variance:dotted? w) v]
[(variance:const? v) w]
[(variance:const? w) v]
[else variance:inv]))
(for*/fold ([ht #hasheq()])
([old-free (in-list hashes)]
[(sym var) (in-hash old-free)])

View File

@ -6,37 +6,43 @@
;; See "Logical Types for Untyped Languages" pg.3
(require "../utils/utils.rkt"
racket/match
"rep-utils.rkt"
"core-rep.rkt"
"free-variance.rkt"
(env mvar-env)
(contract-req))
(provide -id-path)
(provide -id-path name-ref=?)
(def-pathelem CarPE () [#:singleton -car])
(def-pathelem CdrPE () [#:singleton -cdr])
(def-pathelem SyntaxPE () [#:singleton -syntax-e])
(def-pathelem ForcePE () [#:singleton -force])
(def-pathelem FieldPE () [#:singleton -field])
(def-pathelem CarPE () #:base)
(def-pathelem CdrPE () #:base)
(def-pathelem SyntaxPE () #:base)
(def-pathelem ForcePE () #:base)
;; t is always a Name (can't put that into the contract b/c of circularity)
(def-pathelem StructPE ([t Type?] [idx natural-number/c])
[#:intern-key (cons (Rep-seq t) idx)]
[#:frees (f) (f t)]
[#:fold (f) (make-StructPE (f t) idx)]
[#:walk (f) (f t)])
(def-pathelem FieldPE () #:base)
[#:fmap (f) (make-StructPE (f t) idx)]
[#:for-each (f) (f t)])
(def-object Path ([elems (listof PathElem?)] [name name-ref/c])
[#:intern-key (cons (hash-name name) (map Rep-seq elems))]
[#:frees (f) (combine-frees (map f elems))]
[#:fold (f) (make-Path (map f elems) name)]
[#:walk (f) (for-each f elems)])
[#:fmap (f) (make-Path (map f elems) name)]
[#:for-each (f) (for-each f elems)]
[#:custom-constructor
(cond
[(identifier? name)
(if (is-var-mutated? name)
-empty-obj
(let ([name (normalize-id name)])
(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))])])
(define (-id-path id)
(cond
[(identifier? id)
(if (is-var-mutated? id)
(make-Empty)
(make-Path null id))]
[else
(make-Path null id)]))
(define path-intern-table (make-weak-hash))
(define (-id-path name) (make-Path null name))

View File

@ -7,29 +7,31 @@
"core-rep.rkt"
"object-rep.rkt"
racket/match
racket/lazy-require)
racket/lazy-require
(only-in racket/unsafe/ops unsafe-fx<=))
(lazy-require
["../types/prop-ops.rkt" (-and -or)])
(provide hash-name
-is-type
-not-type
AndProp?
AndProp:
AndProp-ps
OrProp?
OrProp:
OrProp-ps
(rename-out [make-OrProp* make-OrProp]
[make-AndProp* make-AndProp]))
(provide -is-type
-not-type)
(def-prop TypeProp ([obj Object?] [type (and/c Type? (not/c Univ?) (not/c Bottom?))])
[#:intern-key (cons (Rep-seq obj) (Rep-seq type))]
[#:frees (f) (combine-frees (list (f obj) (f type)))]
[#:fold (f) (-is-type (f obj) (f type))]
[#:walk (f) (begin (f obj) (f type))])
[#:fmap (f) (make-TypeProp (f obj) (f type))]
[#:for-each (f) (begin (f obj) (f type))]
[#:custom-constructor
(cond
[(Empty? obj) -tt]
[(Univ? type) -tt]
[(Bottom? type) -ff]
[else
(intern-double-ref!
tprop-intern-table
obj type #:construct (make-TypeProp obj type))])])
(define tprop-intern-table (make-weak-hash))
;; Abbreviation for props
;; `i` can be an integer or name-ref/c for backwards compatibility
@ -42,18 +44,23 @@
[(exact-integer? i) (make-Path null (cons 0 i))]
[(pair? i) (make-Path null i)]
[else (-id-path i)]))
(cond
[(Empty? o) (make-TrueProp)]
[(Univ? t) (make-TrueProp)]
[(Bottom? t) (make-FalseProp)]
[else (make-TypeProp o t)]))
(make-TypeProp o t))
(def-prop NotTypeProp ([obj Object?] [type (and/c Type? (not/c Univ?) (not/c Bottom?))])
[#:intern-key (cons (Rep-seq obj) (Rep-seq type))]
[#:frees (f) (combine-frees (list (f obj) (f type)))]
[#:fold (f) (-not-type (f obj) (f type))]
[#:walk (f) (begin (f obj) (f type))])
[#:fmap (f) (-not-type (f obj) (f type))]
[#:for-each (f) (begin (f obj) (f type))]
[#:custom-constructor
(cond
[(Empty? obj) -tt]
[(Univ? type) -ff]
[(Bottom? type) -tt]
[else
(intern-double-ref!
ntprop-intern-table
obj type #:construct (make-NotTypeProp obj type))])])
(define ntprop-intern-table (make-weak-hash))
;; Abbreviation for not props
;; `i` can be an integer or name-ref/c for backwards compatibility
@ -66,36 +73,23 @@
[(exact-integer? i) (make-Path null (cons 0 i))]
[(pair? i) (make-Path null i)]
[else (-id-path i)]))
(cond
[(Empty? o) (make-TrueProp)]
[(Bottom? t) (make-TrueProp)]
[(Univ? t) (make-FalseProp)]
[else (make-NotTypeProp o t)]))
(make-NotTypeProp o t))
(def-prop OrProp ([ps (and/c (length>=/c 2)
(listof (or/c TypeProp? NotTypeProp?)))])
#:no-provide
[#:intern-key (for/hash ([p (in-list ps)]) (values p #t))]
(def-prop OrProp ([ps (listof (or/c TypeProp? NotTypeProp?))])
[#:frees (f) (combine-frees (map f ps))]
[#:fold (f) (apply -or (map f ps))]
[#:walk (f) (for-each f ps)])
[#:fmap (f) (apply -or (map f ps))]
[#:for-each (f) (for-each f ps)]
[#:custom-constructor
(let ([ps (sort ps (λ (p q) (unsafe-fx<= (eq-hash-code p)
(eq-hash-code q))))])
(intern-single-ref!
orprop-intern-table
ps
#:construct (make-OrProp ps)))])
(define (make-OrProp* ps)
(match ps
[(list) (make-FalseProp)]
[(list p) p]
[ps (make-OrProp ps)]))
(define orprop-intern-table (make-weak-hash))
(def-prop AndProp ([ps (and/c (length>=/c 2)
(listof (or/c OrProp? TypeProp? NotTypeProp?)))])
#:no-provide
[#:intern-key (for/hash ([p (in-list ps)]) (values p #t))]
(def-prop AndProp ([ps (listof (or/c OrProp? TypeProp? NotTypeProp?))])
[#:frees (f) (combine-frees (map f ps))]
[#:fold (f) (apply -and (map f ps))]
[#:walk (f) (for-each f ps)])
(define (make-AndProp* ps)
(match ps
[(list) (make-TrueProp)]
[(list p) p]
[ps (make-AndProp ps)]))
[#:fmap (f) (apply -and (map f ps))]
[#:for-each (f) (for-each f ps)])

View File

@ -0,0 +1,68 @@
#lang racket/base
(require "rep-utils.rkt"
racket/match
racket/unsafe/ops
(for-syntax racket/base
syntax/parse
racket/list
racket/syntax))
(provide define-switch)
;; a macro for defining a switch function of the form:
;; (define name (λ (a b ...) (switch (Rep-uid a) [switch-clauses ...])))
;;
;; This allows us to dispatch on the first arguments Rep-uid,
;; which can be more efficient than long match statements with a case
;; for large numbers of Reps (e.g. subtype)
(define-syntax (define-switch stx)
(define-syntax-class (switch-clause arg other-args)
(pattern (((~datum case:) rep-name:id pattern:expr) . body)
#:with name #'rep-name
#:with idx (format-id #'rep-name "uid:~a" (syntax->datum #'rep-name))
#:with function
(with-syntax ([arg arg]
[other-args other-args])
(syntax/loc #'body
(λ (arg . other-args)
(match arg
[pattern . body]))))))
(syntax-parse stx
[(_ (name:id arg:id args:id ...)
(~var clause (switch-clause #'arg #'(args ...))) ...
[(~datum else:) . default])
(define name-symbols (map syntax->datum (syntax->list #'(clause.name ...))))
(unless (not (null? name-symbols))
(raise-syntax-error 'define-switch "switch cannot be null" stx))
(define sorted-name-symbols (sort name-symbols symbol<?))
(unless (eq? (first name-symbols) (first sorted-name-symbols))
(raise-syntax-error 'define-switch
(format "expected ~a as the first case"
(first sorted-name-symbols))
stx))
;; we verify that the Rep cases appear in name-sorted order (so
;; they are easier to find when browsing the code) and that there
;; are no duplicate cases
(for ([cur (in-list (rest name-symbols))]
[cur-stx (in-list (rest (syntax->list #'(clause ...))))]
[cur* (in-list (rest sorted-name-symbols))]
[prev* (in-list sorted-name-symbols)]
[prev-stx (in-list (syntax->list #'(clause ...)))])
(when (eq? cur* prev*)
(raise-syntax-error 'define-switch
(format "duplicate switch cases for ~a" prev*)
prev-stx))
(unless (eq? cur cur*)
(raise-syntax-error 'define-switch
(format "switch cases must be sorted! expected ~a but got ~a"
cur* cur)
cur-stx)))
(syntax/loc stx
(define name
(let* ([default-fun (λ (arg args ...) . default)]
[switch-table (make-vector (get-uid-count) default-fun)])
(vector-set! switch-table clause.idx clause.function)
...
(λ (arg args ...) ((unsafe-vector-ref switch-table (Rep-uid arg)) arg args ...)))))]))

View File

@ -1,20 +1,20 @@
#lang racket/base
(require "../utils/utils.rkt"
"../utils/print-struct.rkt"
(utils tc-utils)
racket/match
racket/generic
(contract-req)
"free-variance.rkt"
"type-mask.rkt"
racket/stxparam
syntax/parse/define
syntax/id-table
racket/unsafe/ops
racket/generic
(only-in racket/unsafe/ops unsafe-struct-ref)
(for-syntax
(utils tc-utils)
racket/match
racket/list
racket/sequence
(except-in syntax/parse id identifier keyword)
racket/base
syntax/struct
@ -24,159 +24,225 @@
(provide (all-defined-out)
get-uid-count
(for-syntax var-name))
;; Contract and Hash related helpers
(provide-for-cond-contract length>=/c)
(define-for-cond-contract ((length>=/c len) l)
(and (list? l)
(>= (length l) len)))
;; seq: interning-generated serial number used to compare Reps (type<).
;; free-vars: cached free type variables
;; free-idxs: cached free dot sequence variables
;; stx: originating syntax for error-reporting
(struct Rep (seq free-vars free-idxs) #:transparent
#:methods gen:equal+hash
[(define (equal-proc x y recur)
(unsafe-fx= (Rep-seq x) (Rep-seq y)))
(define (hash-proc x recur) (Rep-seq x))
(define (hash2-proc x recur) (Rep-seq x))])
(define-for-cond-contract name-ref/c
(or/c identifier?
(cons/c exact-integer? exact-integer?)))
(define (Rep<? x y)
(unsafe-fx< (Rep-seq x) (Rep-seq y)))
(define (name-ref=? x y)
(cond
[(identifier? x)
(and (identifier? y) (free-identifier=? x y))]
[else (equal? x y)]))
;; prop:get-values
(define-values (prop:Rep-name Rep-name)
(let-values ([(prop _ accessor) (make-struct-type-property 'named)])
(values prop accessor)))
(define id-table (make-free-id-table))
(define (normalize-id id)
(free-id-table-ref! id-table id id))
(define (hash-id id)
(eq-hash-code (identifier-binding-symbol id)))
(define (hash-name-ref name rec)
(if (identifier? name)
(hash-id name)
(rec name)))
;; prop:get-values
(define-values (prop:values-fun values-fun)
(let-values ([(prop _ accessor) (make-struct-type-property 'values)])
(values prop accessor)))
;; Rep-values
(define (Rep-values x)
((values-fun x) x))
;; prop:get-constructor
(define-values (prop:constructor-fun Rep-constructor)
(let-values ([(prop _ accessor) (make-struct-type-property 'constructor)])
(values prop accessor)))
;; structural type info for simple/straightforward types
;; (i.e. we store the list of field variances)
(define-values (prop:structural structural? Type-variances)
(make-struct-type-property 'structural))
;; top type predicates
(define-values (prop:top-type has-top-type? top-type-pred)
(make-struct-type-property 'top-type))
;; prop:walk-fun
(define-values (prop:walk-fun walkable? walk-fun)
(make-struct-type-property 'walk))
;; Rep-walk
(define (Rep-walk f x)
(define fun (walk-fun x))
(when (procedure? fun)
(fun f x)))
;; prop:fold-fun
(define-values (prop:fold-fun foldable? fold-fun)
(make-struct-type-property 'fold))
;; Rep-fold
(define (Rep-fold f x)
(define fun (fold-fun x))
(if (procedure? fun)
(fun f x)
x))
;; 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.
;; The table is referenced in env/init-env.rkt
;;
;; For example, instead of marshalling a big union for `Integer`, we
;; simply emit `-Integer`, which evaluates to the right type.
(define predefined-type-table (make-hash))
(define-syntax-rule (declare-predefined-type! id)
(hash-set! predefined-type-table id #'id))
(provide predefined-type-table)
(define-syntax-rule (define/decl id e)
(begin (define id e)
(declare-predefined-type! id)))
;; Is this a type that can be a 'back-edge' into the type graph?
;; (i.e. could blindly following this type lead to infinite recursion?)
(define-values (prop:resolvable resolvable?)
(let-values ([(prop predicate _) (make-struct-type-property 'resolvable)])
(values prop predicate)))
;; fetches an interned Rep based on the given _single_ key
;; NOTE: the #:construct expression is only run if there
;; is no interned copy, so we should avoid unnecessary
;; allocation w/ this approach
(define-simple-macro (intern-single-ref! table-exp:expr
key-exp:expr
#:construct val-exp:expr)
(let ([table table-exp])
(define key key-exp)
(define intern-box (hash-ref table key #f))
(cond
[(and intern-box (weak-box-value intern-box #f))]
[else
(define val val-exp)
(hash-set! table key (make-weak-box val))
val])))
;; fetches an interned Rep based on the given _two_ keys
;; see 'intern-single-ref!'
(define-simple-macro (intern-double-ref! table:id
key-exp1:expr
key-exp2:expr
#:construct val-exp:expr)
(intern-single-ref! (hash-ref! table key-exp1 make-weak-hash)
key-exp2
#:construct val-exp))
;; - - - - - - - - - - - -
;; Rep Properties
;; - - - - - - - - - - - -
(define-generics Rep
;; A symbol name for a Rep
;; Rep-name : Rep -> symbol
(Rep-name Rep)
;; The values this rep contains (see Rep-constructor).
;; Rep-values : Rep -> (listof any/c)
(Rep-values Rep)
;; is there a simple, structural description for the variances
;; of this Rep's fields? (currently only used for 'structural' types,
;; see type-rep.rkt
;; Rep-constructor : Rep -> (any ... -> Rep)
(Rep-variances Rep)
;; The intended constructor for this Rep.
;; i.e. (equal? ((Rep-constructor rep) (Rep-values rep)) rep) = #t
;; Rep-constructor : Rep -> (any ... -> Rep)
(Rep-constructor Rep)
;; can this Rep contain free type variables?
;; (i.e. 'F' types from rep/type-rep.rkt)
;; Rep-free-ty-vars-fun : Rep -> free-vars
(Rep-free-vars Rep)
;; can this Rep contain free dotted type variables (idxs)?
;; (e.g. things like ListDots, etc rep/type-rep.rkt
;; which have an arity/structure which depends on instantiation)
;; Rep-free-ty-idxs-fun : Rep -> free-dotted-vars
(Rep-free-idxs Rep)
;; is this Rep mappable?
;; (i.e. can we traverse it w/ applying a function to
;; the fields? a lá map for lists)
;; Rep-fmap : Rep procedure -> Rep
(Rep-fmap Rep f)
;; is this Rep walkable?
;; (i.e. can we traverse it w/ some effectful function
;; a lá for-each for lists)
;; Rep-walk-fun : Rep procedure -> void
(Rep-for-each Rep f))
;; used internally when generating gen:Rep method definitions
;; so that we don't have to mess around w/ 'define/generic'
(define-syntax free-vars* (make-rename-transformer #'Rep-free-vars))
(define-syntax free-idxs* (make-rename-transformer #'Rep-free-idxs))
;; A variant-unique fixnum.
;; Rep-uid : Rep -> fixnum
(define-values (prop:uid Rep-uid)
(let-values ([(prop _ acc) (make-struct-type-property 'uid)])
(values prop acc)))
(define-values (prop:mask raw-mask)
(let-values ([(prop _ acc) (make-struct-type-property 'mask)])
(values prop acc)))
;; Type-mask : Rep -> fixnum
(define-syntax-rule (mask rep)
(let ([mask (raw-mask rep)])
(if (procedure? mask)
(mask rep)
mask)))
;;************************************************************
;; Rep Declaration Syntax Classes
;;************************************************************
(define (make-counter!)
(let ([state 0])
(λ () (begin0 state (set! state (unsafe-fx+ 1 state))))))
(define count! (make-counter!))
(define id-count! (make-counter!))
(define identifier-table (make-free-id-table))
(define (hash-id id)
(free-id-table-ref!
identifier-table
id
(λ () (let ([c (id-count!)])
(free-id-table-set! identifier-table id c)
c))))
(define (hash-name name)
(if (identifier? name)
(hash-id name)
name))
(define-values (next-uid! get-uid-count)
(let ([state 0]
[finalized? #f])
(values (λ () (if finalized?
(int-err "next-uid! called after uid count finalized!")
(begin0 state (set! state (add1 state)))))
(λ () (set! finalized? #t) state))))
(begin-for-syntax
;; defines a "rep transformer"
;; These are functions defined to fold over Reps (e.g. Rep-fmap, Rep-for-each).
;; Because they are defined within the definition of the struct, they bind the same
;; identifiers which declare the Rep's fields to those same fields.
(define (rep-transform self f-id struct-fields body)
(with-syntax ([f-id f-id]
[self self]
[(fld ...) struct-fields]
[body body])
#'(λ (self f-id)
(let ([fld (unsafe-struct-ref self (struct-field-index fld))] ...) . body))))
;; like "rep-transform" but the folding function is fixed (e.g. free-vars)
(define (fixed-rep-transform self f-id fun struct-fields body)
(with-syntax ([transformer (rep-transform self f-id struct-fields body)]
[self self]
[fun fun])
#'(λ (self) (transformer self fun))))
;; #:frees definition parsing
(define-syntax-class freesspec
(define-syntax-class (freesspec struct-fields)
#:attributes (free-vars free-idxs)
(pattern ([#:vars (f1) . vars-body]
[#:idxs (f2) . idxs-body])
#:with free-vars #'(let ([f1 Rep-free-vars]) . vars-body)
#:with free-idxs #'(let ([f2 Rep-free-idxs]) . idxs-body))
(pattern ((f:id) . body)
#:with free-vars #'(let ([f Rep-free-vars]) . body)
#:with free-idxs #'(let ([f Rep-free-idxs]) . body)))
;; #:fold definition parsing
(define-syntax-class (walkspec name match-expdr struct-fields)
(pattern
([#:vars (f1 (~optional (~seq #:self self1:id)
#:defaults ([self1 (generate-temporary 'self)])))
. vars-body]
[#:idxs (f2 (~optional (~seq #:self self2:id)
#:defaults ([self2 (generate-temporary 'self)])))
. idxs-body])
#:with free-vars (fixed-rep-transform #'self1 #'f1 #'free-vars* struct-fields #'vars-body)
#:with free-idxs (fixed-rep-transform #'self2 #'f2 #'free-idxs* struct-fields #'idxs-body))
(pattern
((f:id (~optional (~seq #:self self:id)
#:defaults ([self (generate-temporary 'self)])))
. body)
#:with free-vars (fixed-rep-transform #'self #'f #'free-vars* struct-fields #'body)
#:with free-idxs (fixed-rep-transform #'self #'f #'free-idxs* struct-fields #'body)))
(define-syntax-class (constructor-spec constructor-name raw-constructor-name struct-fields)
#:attributes (def)
(pattern ((f:id) . body)
(pattern body
#:with def
(with-syntax ([name name]
[(flds ...) struct-fields]
[mexpdr match-expdr])
#'(λ (f self)
(match self
[(mexpdr flds ...) . body]
[_ (error 'Rep-walk "bad match in ~a's walk" (quote name))])))))
;; #:map definition parsing
(define-syntax-class (foldspec name match-expdr struct-fields)
(with-syntax ([constructor-name constructor-name]
[raw-constructor-name raw-constructor-name]
[(struct-fields ...) struct-fields])
#'(define (constructor-name struct-fields ...)
(let ([constructor-name raw-constructor-name])
. body)))))
;; definer parser for functions who operate on Reps. Fields are automatically bound
;; to the struct-field id names in the body. An optional self argument can be specified.
(define-syntax-class (generic-transformer struct-fields)
#:attributes (def)
(pattern ((f:id (~optional (~seq #:self self:id)
#:defaults ([self (generate-temporary 'self)])))
. body)
#:with def
(with-syntax ([name name]
[(flds ...) struct-fields]
[mexpdr match-expdr])
#'(λ (f self)
(match self
[(mexpdr flds ...) . body]
[_ (error 'Rep-fold "bad match in ~a's fold" (quote name))])))))
#:with def (rep-transform #'self #'f struct-fields #'body)))
;; variant name parsing
(define-syntax-class var-name
#:attributes (name raw-constructor constructor mexpdr pred)
#:attributes (name constructor raw-constructor match-expander predicate)
(pattern name:id
#:with raw-constructor
;; raw constructor should only be used by macros (hence the gensym)
(format-id #'name "raw-make-~a" (gensym (syntax-e #'name)))
#:with constructor
(format-id #'name "make-~a" (syntax-e #'name))
#:with mexpdr
;; hidden constructor for use inside custom constructor defs
#:with raw-constructor (format-id #'name "raw-make-~a" (syntax-e #'name))
#:with match-expander
(format-id #'name "~a:" (syntax-e #'name))
#:with pred
#:with predicate
(format-id #'name "~a?" (syntax-e #'name))))
;; structure accessor parsing
(define-syntax-class (fld-id struct-name)
@ -208,31 +274,25 @@
;; options
(~or
;; parent struct (if any)
(~optional (~optional [#:parent parent:id])
#:defaults ([parent #'Rep]))
(~optional [#:parent parent:id])
;; base declaration (i.e. no fold/map)
(~optional (~and #:base base?))
;; All Reps are interned
(~optional [#:intern-key provided-intern-key])
;; #:frees spec (how to compute this Rep's free type variables)
(~optional [#:frees . frees-spec:freesspec])
;; #:walk spec (how to traverse this structure for effect)
(~optional [#:walk . (~var walk-spec (walkspec #'var.name
#'var.mexpdr
#'(flds.ids ...)))])
(~optional [#:frees . (~var frees-spec (freesspec #'(flds.ids ...)))])
;; #:for-each spec (how to traverse this structure for effect)
(~optional [#:for-each . (~var for-each-spec (generic-transformer #'(flds.ids ...)))])
;; #:fold spec (how to transform & fold this structure)
(~optional [#:fold . (~var fold-spec (foldspec #'var.name
#'var.mexpdr
#'(flds.ids ...)))])
(~optional [#:type-mask . type-mask-body])
;; is this a Type w/ a Top type? (e.g. Vector --> VectorTop)
(~optional [#:top top-pred:id])
(~optional [#:fmap . (~var fold-spec (generic-transformer #'(flds.ids ...)))])
(~optional [#:mask . rep-mask-body])
(~optional [#:variances ((~literal list) variances ...)])
;; #:no-provide option (i.e. don't provide anything automatically)
(~optional (~and #:needs-resolving needs-resolving?))
;; #:no-provide option (i.e. don't provide anything automatically)
(~optional (~and #:no-provide no-provide?))
;; field variances (e.g. covariant/contravariant/etc) declarations
(~optional (~and [#:variances variances ...] structural))
(~optional (~and #:no-provide no-provide?-kw))
(~optional [#:singleton singleton:id])
(~optional [#:custom-constructor . (~var constr-def
(constructor-spec #'var.constructor
#'var.raw-constructor
#'(flds.ids ...)))])
(~optional (~and #:non-transparent non-transparent-kw))
;; #:extras to specify other struct properties in a per-definition manner
(~optional [#:extras . extras]))
...)
@ -242,141 +302,156 @@
;; - - - - - - - - - - - - - - -
;; build convenient boolean flags
(define is-a-type? (eq? 'Type (syntax-e #'parent)))
(define intern-key (if (attribute provided-intern-key)
#'provided-intern-key
#'#t))
;; intern-key is required (when the number of fields is > 0)
(when (and (not (attribute provided-intern-key))
(> (length (syntax->list #'flds)) 0))
(raise-syntax-error 'def-rep "intern key specification required when the number of fields > 0"
(define is-a-type? (and (attribute parent) (eq? 'Type (syntax-e #'parent))))
;; singletons cannot have fields or #:no-provide
(when (and (attribute singleton)
(or (attribute no-provide?-kw)
(> (length (syntax->list #'flds)) 0)))
(raise-syntax-error 'def-rep "singletons cannot have fields or the #:no-provide option"
#'var))
;; no frees, walk, or fold for #:base Reps
(when (and (attribute base?) (or (attribute frees-spec)
(attribute walk-spec)
(attribute fold-spec)))
(raise-syntax-error 'def-rep "base reps cannot have #:frees, #:walk, or #:fold"
(when (and (attribute base?)
(attribute singleton))
(raise-syntax-error 'def-rep "singletons are base by def, do not provide #:base option"
#'var))
;; if non-base, frees, walk, and fold are required
(when (and (not (attribute base?))
;; no frees, for-each, fold, or abs/inst for #:base Reps
(when (and (or (attribute base?)
(attribute singleton))
(or (attribute frees-spec)
(attribute for-each-spec)
(attribute fold-spec)))
(raise-syntax-error 'def-rep "base reps and singletons cannot have #:frees, #:for-each, or #:fold"
#'var))
;; if non-base, frees, for-each, and fold are required
(when (and (not (or (attribute base?) (attribute singleton)))
(or (not (attribute frees-spec))
(not (attribute walk-spec))
(not (attribute for-each-spec))
(not (attribute fold-spec))))
(raise-syntax-error 'def-rep "non-base reps require #:frees, #:walk, and #:fold"
(raise-syntax-error 'def-rep "non-base reps require #:frees, #:for-each, and #:fold"
#'var))
;; can't be structural and not a type
(when (and (not is-a-type?) (attribute structural))
(raise-syntax-error 'def-rep "only types can be structural" #'structural))
;; - - - - - - - - - - - - - - -
;; Let's build the definitions!
;; - - - - - - - - - - - - - - -
(with-syntax*
([intern-key intern-key]
([uid-id (format-id #'var.name "uid:~a" (syntax->datum #'var.name))]
[(parent ...) (if (attribute parent) #'(parent) #'())]
;; contract for constructor
[constructor-contract #'(-> flds.contracts ... var.pred)]
[constructor-contract #'(-> flds.contracts ... any)]
[constructor-name (if (attribute constr-def)
#'var.raw-constructor
#'var.constructor)]
[constructor-def (if (attribute constr-def)
#'constr-def.def
#'(begin))]
[(maybe-transparent ...) (if (attribute non-transparent-kw)
#'()
#'(#:transparent))]
;; match expander (skips 'meta' fields)
[mexpdr-def
#`(define-match-expander var.mexpdr
#`(define-match-expander var.match-expander
(λ (s)
(syntax-parse s
[(_ . pats)
#,(if is-a-type? ;; skip Type-mask and subtype cache
#'(syntax/loc s (var.name _ _ _ _ _ . pats))
#'(syntax/loc s (var.name _ _ _ . pats)))])))]
[(_ . pats) (syntax/loc s (var.name . pats))])))]
;; Rep generic definitions
;; -----------------------
;; free var/idx defs
[free-vars-def (cond
[(attribute base?) #'empty-free-vars]
[else #'frees-spec.free-vars])]
[free-idxs-def (cond
[(attribute base?) #'empty-free-vars]
[else #'frees-spec.free-idxs])]
;; top type info
[(maybe-top-type-spec ...)
(if (attribute top-pred)
#'(#:property prop:top-type top-pred)
#'())]
;; if it's a structural type, save its field variances
[(maybe-structural ...)
(if (attribute structural)
#'(#:property prop:structural (list variances ...))
#'())]
;; an argument if we accept a type mask
[mask-arg (generate-temporary 'mask)]
;; constructor w/ interning and Type-mask handeling if necessary
[constructor-def
[Rep-name-def
#'(define (Rep-name _) 'var.name)]
[Rep-values-def
#'(define (Rep-values rep)
(match rep
[(var.name flds.ids ...) (list flds.ids ...)]))]
[Rep-variances-def
(cond
;; non-Types don't need masks
[(not is-a-type?)
#'(define var.constructor
(let ([intern-table (make-hash)])
(λ (flds.ids ...)
(let ([key intern-key]
[fail (λ () (let ([fvs free-vars-def]
[fis free-idxs-def])
(var.raw-constructor (count!) fvs fis flds.ids ...)))])
(hash-ref! intern-table key fail)))))]
[(attribute variances)
#'(define (Rep-variances _)
(list variances ...))]
[else
;; Types have to provide Type-masks and subtype caches
#`(define var.constructor
(let ([intern-table (make-hash)])
(λ (flds.ids ...)
(let ([key intern-key]
[fail (λ () (let ([fvs free-vars-def]
[fis free-idxs-def]
[mask-val #,(if (attribute type-mask-body)
#'(let () . type-mask-body)
#'mask:unknown)])
(var.raw-constructor (count!) fvs fis (make-hash) mask-val flds.ids ...)))])
(hash-ref! intern-table key fail)))))])]
;; walk def
[walk-def (cond
[(attribute base?) #'#f]
[else #'walk-spec.def])]
#'(define (Rep-variances _) #f)])]
[Rep-constructor-def
#'(define (Rep-constructor rep) var.constructor)]
;; free var/idx defs
[Rep-free-vars-def
(cond
[(or (attribute base?)
(attribute singleton))
#'(define (Rep-free-vars _) empty-free-vars)]
[else #'(define Rep-free-vars frees-spec.free-vars)])]
[Rep-free-idxs-def
(cond
[(or (attribute base?)
(attribute singleton))
#'(define (Rep-free-idxs _) empty-free-vars)]
[else #'(define Rep-free-idxs frees-spec.free-idxs)])]
;; for-each def
[Rep-for-each-def
(cond
[(or (attribute base?) (attribute singleton))
#'(define (Rep-for-each rep f) (void))]
[else #'(define Rep-for-each for-each-spec.def)])]
;; fold def
[fold-def (cond
[(attribute base?) #'#f]
[else #'fold-spec.def])]
;; is this a type that needs resolving (e.g. Mu)
[(maybe-needs-resolving ...)
(if (attribute needs-resolving?)
#'(#:property prop:resolvable #t)
#'())]
[Rep-fmap-def
(cond
[(or (attribute base?) (attribute singleton))
#'(define (Rep-fmap rep f) rep)]
[else #'(define Rep-fmap fold-spec.def)])]
;; how do we pull out the values required to fold this Rep?
[values-def #'(match-lambda
[(var.mexpdr flds.ids ...) (list flds.ids ...)])]
[rep-mask-body
(cond
[(attribute rep-mask-body) #'(let () . rep-mask-body)]
[else #'mask:unknown])]
;; module provided defintions, if any
[(provides ...)
(cond
[(attribute no-provide?) #'()]
[(attribute no-provide?-kw) #'()]
[else
#'((provide var.mexpdr var.pred flds.accessors ...)
#'((provide var.match-expander var.predicate flds.accessors ...)
(provide/cond-contract (var.constructor constructor-contract)))])]
[(extra-defs ...) (if (attribute extras) #'extras #'())])
[(extra-defs ...) (if (attribute extras) #'extras #'())]
[struct-def #'(struct var.name parent ... (flds.ids ...)
maybe-transparent ...
#:constructor-name constructor-name
#:property prop:uid uid-id
#:property prop:mask rep-mask-body
#:methods gen:Rep
[Rep-name-def
Rep-values-def
Rep-constructor-def
Rep-variances-def
Rep-free-vars-def
Rep-free-idxs-def
Rep-for-each-def
Rep-fmap-def]
extra-defs ...)])
;; - - - - - - - - - - - - - - -
;; macro output
;; - - - - - - - - - - - - - - -
#'(begin
(struct var.name parent (flds.ids ...) #:transparent
#:constructor-name
var.raw-constructor
#:property prop:Rep-name (quote var.name)
#:property prop:constructor-fun
(λ (flds.ids ...) (var.constructor flds.ids ...))
#:property prop:values-fun
values-def
#:property prop:walk-fun
walk-def
#:property prop:fold-fun
fold-def
maybe-top-type-spec ...
maybe-structural ...
maybe-needs-resolving ...
extra-defs ...)
constructor-def
mexpdr-def
provides ...))]))
(cond
[(attribute singleton)
(syntax/loc stx
(begin
(define uid-id (next-uid!))
(define singleton
(let ()
struct-def
(var.constructor)))
(declare-predefined-type! singleton)
(define (var.predicate x) (eq? x singleton))
(define-match-expander var.match-expander
(λ (s)
(syntax-parse s
[(_) (syntax/loc s (? var.predicate))])))
(provide singleton var.predicate var.match-expander
uid-id)))]
[else
(syntax/loc stx
(begin
(define uid-id (next-uid!))
struct-def
constructor-def
mexpdr-def
provides ...
(provide uid-id)))]))]))
;; macro for easily defining sets of types represented by fixnum bitfields
@ -465,9 +540,3 @@
;; provide the bit variables (e.g. bits:Null)
atoms.provide ...
unions.provide ...))]))
(provide
Rep-values
(rename-out [Rep-free-vars free-vars*]
[Rep-free-idxs free-idxs*]))

File diff suppressed because it is too large Load Diff

View File

@ -21,10 +21,9 @@
;;---------
(def-values Values ([results (listof Result?)])
[#:intern-key (map Rep-seq results)]
[#:frees (f) (combine-frees (map f results))]
[#:fold (f) (make-Values (map f results))]
[#:walk (f) (for-each f results)])
[#:fmap (f) (make-Values (map f results))]
[#:for-each (f) (for-each f results)])
;; Anything that can be treated as a _simple_
;; Values by sufficient expansion
@ -42,10 +41,9 @@
;; return type of functions
(def-values AnyValues ([p Prop?])
[#:intern-key (Rep-seq p)]
[#:frees (f) (f p)]
[#:fold (f) (make-AnyValues (f p))]
[#:walk (f) (f p)])
[#:fmap (f) (make-AnyValues (f p))]
[#:for-each (f) (f p)])
;;-------------
;; ValuesDots
@ -55,8 +53,16 @@
(def-values ValuesDots ([results (listof Result?)]
[dty Type?]
[dbound (or/c symbol? natural-number/c)])
[#:intern-key (list* (Rep-seq dty) dbound (map Rep-seq results))]
[#:frees (f) (combine-frees (map f results))]
[#:fold (f) (make-ValuesDots (map f results) (f dty) dbound)]
[#:walk (f) (begin (f dty)
(for-each f results))])
[#:frees
[#:vars (f)
(if (symbol? dbound)
(free-vars-remove (combine-frees (map free-vars* (cons dty results))) dbound)
(combine-frees (map free-vars* (cons dty results))))]
[#:idxs (f)
(if (symbol? dbound)
(combine-frees (cons (single-free-var dbound)
(map free-idxs* (cons dty results))))
(combine-frees (map free-idxs* (cons dty results))))]]
[#:fmap (f) (make-ValuesDots (map f results) (f dty) dbound)]
[#:for-each (f) (begin (f dty)
(for-each f results))])

View File

@ -47,7 +47,7 @@
(parameterize ((current-variable-values values))
(let loop ()
(define change #f)
(for (((v thunk) (equation-set-equations eqs)))
(for ([(v thunk) (in-hash (equation-set-equations eqs))])
(define new-value (thunk))
(define old-value (hash-ref values v))
(unless (equal? new-value old-value)

View File

@ -1,7 +1,7 @@
#lang racket/base
;; Implements a check that to determine if a part of a static contract has two (or more) parametric
;; contracts as direct descendents.
;; Implements a check to determine if a part of a static contract has two
;; (or more) parametric contracts as direct descendents.
(require
"../utils/utils.rkt"
@ -34,11 +34,11 @@
(define seen? #f)
(match sc
;; skip already seen sc
[(? (λ (sc) (hash-ref seen (list sc variance) #f)))
[_ #:when (hash-ref seen (list sc variance) #f)
(set! seen? #t)]
[(or (or/sc: elems ...) (and/sc: elems ...))
(add-equation! eqs (get-var sc)
(lambda () (for/sum ((e (in-list elems)))
(lambda () (for/sum ([e (in-list elems)])
(variable-ref (get-var e)))))]
[(or (parametric-var/sc: id) (sealing-var/sc: id))
(add-equation! eqs (get-var sc) (lambda () 1))]

View File

@ -3,7 +3,7 @@
(require "../utils/utils.rkt"
racket/match (prefix-in - (contract-req))
racket/format
(types utils union subtype prop-ops abbrev)
(types utils subtype prop-ops abbrev)
(utils tc-utils)
(rep type-rep object-rep prop-rep)
(typecheck error-message))
@ -88,8 +88,8 @@
[(p p) #t]
[(p #f) #t]
[((PropSet: p1+ p1-) (PropSet: p2+ p2-))
(and (implies-atomic? p1+ p2+)
(implies-atomic? p1- p2-))]
(and (implies? p1+ p2+)
(implies? p1- p2-))]
[(_ _) #f]))
(define (object-better? o1 o2)
(match* (o1 o2)
@ -98,13 +98,13 @@
[(_ _) #f]))
(define (prop-better? p1 p2)
(or (not p2)
(implies-atomic? p1 p2)))
(implies? p1 p2)))
(match* (tr1 expected)
;; This case has to be first so that bottom (exceptions, etc.) can be allowed in cases
;; where multiple values are expected.
;; We can ignore the props and objects in the actual value because they would never be about a value
[((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _)
[((tc-result1: (? Bottom?)) _)
(fix-results/bottom expected)]
[((tc-any-results: p1) (tc-any-results: p2))
@ -205,3 +205,4 @@
[((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)]))

View File

@ -13,7 +13,7 @@
"signatures.rkt"
(private parse-type syntax-properties)
(env lexical-env tvar-env global-env type-alias-helper mvar-env)
(types utils abbrev union subtype resolve generalize)
(types utils abbrev subtype resolve generalize)
(typecheck check-below internal-forms)
(utils tc-utils mutated-vars)
(rep object-rep type-rep values-rep)
@ -885,7 +885,7 @@
(->acc (list Univ)
(or (and maybe-type (car maybe-type))
Univ)
(list (make-FieldPE))
(list -field)
#:var getter-id)
(-> Univ (or (and maybe-type (car maybe-type)) -Bottom)
-Void))))

View File

@ -5,7 +5,7 @@
racket/match
"signatures.rkt" "tc-metafunctions.rkt"
"tc-funapp.rkt"
(types utils abbrev union resolve subtype match-expanders)
(types utils abbrev resolve subtype match-expanders)
(typecheck check-below)
(private syntax-properties)
(utils tc-utils)

View File

@ -71,7 +71,7 @@
(only-in (base-env base-special-env) make-template-identifier)
(env lexical-env tvar-env global-env
signature-env)
(types utils abbrev union subtype resolve generalize signatures)
(types utils abbrev subtype resolve generalize signatures)
(typecheck check-below internal-forms)
(utils tc-utils)
(rep type-rep values-rep)

View File

@ -5,7 +5,7 @@
"utils.rkt"
syntax/parse syntax/stx racket/match
(typecheck signatures tc-funapp)
(types abbrev prop-ops union utils)
(types abbrev prop-ops utils)
(rep type-rep object-rep)
(for-label racket/base racket/bool))

View File

@ -1,10 +1,11 @@
#lang racket/unit
(require "../../utils/utils.rkt"
(utils hset)
syntax/parse syntax/stx racket/match racket/sequence
"signatures.rkt"
"utils.rkt"
(types utils abbrev numeric-tower union resolve type-table generalize)
(types utils abbrev numeric-tower resolve type-table generalize)
(typecheck signatures check-below)
(rep type-rep type-mask rep-utils)
(for-label racket/unsafe/ops racket/base))
@ -127,8 +128,8 @@
;; we re-run this whole algorithm with that. Otherwise, we treat
;; it like any other expected type.
[(tc-result1: (app resolve (Union: ts))) (=> continue)
(define u-ts (for/list ([t (in-list ts)]
#:when (eq? mask:vector (Type-mask t)))
(define u-ts (for/list ([t (in-hset ts)]
#:when (eq? mask:vector (mask t)))
t))
(match u-ts
[(list t0) (tc/app #'(#%plain-app . form) (ret t0))]

View File

@ -5,8 +5,8 @@
"signatures.rkt"
"utils.rkt"
syntax/parse syntax/stx racket/match racket/sequence
(typecheck signatures tc-funapp)
(types abbrev utils union substitute)
(typecheck signatures tc-funapp error-message)
(types abbrev utils substitute)
(rep type-rep)
(env tvar-env)
(prefix-in i: (infer infer))
@ -35,13 +35,10 @@
(match* ((single-value #'arg0) (stx-map single-value #'(arg ...)))
;; if the argument is a ListDots
[((tc-result1: (ListDots: t0 bound0))
(list (tc-result1: (or (and (ListDots: t bound) (app (λ _ #f) var))
;; a devious hack - just generate #f so the test below succeeds
;; have to explicitly bind `var' since otherwise `var' appears
;; on only one side of the or
(list (tc-result1: (or (and (ListDots: t bound))
;; NOTE: safe to include these, `map' will error if any list is
;; not the same length as all the others
(and (Listof: t var) (app (λ _ #f) bound))))
(and (Listof: t) (bind bound #f ))))
...))
(=> fail)
(unless (for/and ([b (in-list bound)]) (or (not b) (eq? bound0 b))) (fail))
@ -81,21 +78,42 @@
;; TODO fix double typechecking
[_ (tc/app-regular #'form expected)])))
;; special case for `list'
(pattern (list . args)
(let ()
(define vs (stx-map (λ (x) (gensym)) #'args))
(define l-type (-Tuple (map make-F vs)))
(define subst
(match expected
[(tc-result1: t)
;; We want to infer the largest vs that are still under the element types
(i:infer vs null (list l-type) (list t) (-values (list (-> l-type Univ))))]
[_ #f]))
(ret (-Tuple
(for/list ([i (in-syntax #'args)] [v (in-list vs)])
(or (and subst
(tc-expr/check/t? i (ret (subst-all subst (make-F v)))))
(tc-expr/t i)))))))
(pattern
(list . args)
(let ([args-list (syntax->list #'args)])
(match expected
[(tc-result1: t)
(match t
[(List: ts)
(cond
[(= (length ts) (length args-list))
(for ([arg (in-list args-list)]
[t (in-list ts)])
(tc-expr/check arg (ret t)))
(ret t)]
[else
(expected-but-got t (-Tuple (map tc-expr/t args-list)))
(ret t)])]
[_
(define vs (map (λ (_) (gensym)) args-list))
(define l-type (-Tuple (map make-F vs)))
;; We want to infer the largest vs that are still under the element types
(define substs (i:infer vs null (list l-type) (list t) (-values (list (-> l-type Univ)))
#:multiple? #t))
(cond
[substs
(define result
(for*/first ([subst (in-list substs)]
[argtys (in-value (for/list ([arg (in-list args-list)]
[v (in-list vs)])
(tc-expr/check/t? arg (ret (subst-all subst (make-F v))))))]
#:when (andmap values argtys))
(ret (-Tuple argtys))))
(or result
(begin (expected-but-got t (-Tuple (map tc-expr/t args-list)))
expected))]
[else (ret (-Tuple (map tc-expr/t args-list)))])])]
[_ (ret (-Tuple (map tc-expr/t args-list)))])))
;; special case for `list*'
(pattern (list* (~between args:expr 1 +inf.0) ...)
(match-let* ([(list tys ... last) (stx-map tc-expr/t #'(args ...))])

View File

@ -7,7 +7,7 @@
racket/format
racket/list
(typecheck signatures)
(types base-abbrev resolve subtype type-table union utils)
(types base-abbrev resolve subtype type-table utils)
(rep type-rep)
(utils tc-utils)

View File

@ -6,7 +6,7 @@
(contract-req)
(rep type-rep prop-rep object-rep rep-utils)
(utils tc-utils)
(types tc-result resolve subtype update union prop-ops)
(types tc-result resolve subtype update prop-ops)
(env type-env-structs lexical-env mvar-env)
(rename-in (types abbrev)
[-> -->]
@ -32,7 +32,7 @@
(identifier-binding x))
(let* ([t (lookup-type/lexical x Γ #:fail (lambda _ Univ))]
[new-t (update t pt #t lo)])
(if (type-equal? new-t -Bottom)
(if (Bottom? new-t)
(values #f '())
(loop ps negs (env-set-type Γ x new-t))))]
;; process negative info _after_ positive info so we don't miss anything
@ -47,7 +47,7 @@
[(cons (NotTypeProp: (Path: lo x) pt) rst)
(let* ([t (lookup-type/lexical x Γ #:fail (lambda _ Univ))]
[new-t (update t pt #f lo)])
(if (type-equal? new-t -Bottom)
(if (Bottom? new-t)
#f
(loop rst (env-set-type Γ x new-t))))]
[_ Γ]))])

View File

@ -5,7 +5,7 @@
racket/match (prefix-in - (contract-req))
"signatures.rkt"
"check-below.rkt" "../types/kw-types.rkt"
(types utils abbrev union subtype type-table path-type
(types utils abbrev subtype type-table path-type
prop-ops overlap resolve generalize tc-result)
(private-in syntax-properties parse-type)
(rep type-rep prop-rep object-rep)
@ -403,7 +403,7 @@
[(Box: t) (-box (check-below (find-stx-type x t) t))]
[_ (-box (generalize (find-stx-type x)))])]
[(? hash? h)
(match (and expected (resolve (intersect expected -HashTop)))
(match (and expected (resolve (intersect expected -HashtableTop)))
[(Hashtable: kt vt)
(define kts (hash-map h (lambda (x y) (find-stx-type x kt))))
(define vts (hash-map h (lambda (x y) (find-stx-type y vt))))

View File

@ -1,6 +1,7 @@
#lang racket/base
(require (rename-in "../utils/utils.rkt" [infer r:infer])
(utils hset)
racket/match racket/list
(prefix-in c: (contract-req))
(env tvar-env)
@ -160,9 +161,9 @@
[(? 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: (and ts (list (? Function?) ...)))
[(Union: ts) #:when (for/and ([t (in-hset ts)]) (Function? t))
(merge-tc-results
(for/list ([fty ts])
(for/list ([fty (in-hset 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)]

View File

@ -6,7 +6,7 @@
racket/sequence
(contract-req)
(rep type-rep object-rep rep-utils)
(rename-in (types abbrev utils union)
(rename-in (types abbrev utils)
[-> t:->]
[->* t:->*]
[one-of/c t:one-of/c])

View File

@ -3,7 +3,7 @@
(require "../utils/utils.rkt"
racket/match
(typecheck signatures check-below)
(types abbrev numeric-tower resolve subtype union generalize
(types abbrev numeric-tower resolve subtype generalize
prefab)
(rep type-rep)
(only-in (infer infer) intersect)
@ -113,7 +113,7 @@
[_ (make-HeterogeneousVector (for/list ([l (in-vector (syntax-e #'i))])
(generalize (tc-literal l #f))))])]
[(~var i (3d hash?))
(match (and expected (resolve (intersect expected -HashTop)))
(match (and expected (resolve (intersect expected -HashtableTop)))
[(Hashtable: k v)
(let* ([h (syntax-e #'i)]
[ks (hash-map h (lambda (x y) (tc-literal x k)))]

View File

@ -2,7 +2,7 @@
(require "../utils/utils.rkt"
racket/match racket/list
(except-in (types abbrev union utils prop-ops tc-result)
(except-in (types abbrev utils prop-ops tc-result)
-> ->* one-of/c)
(rep type-rep prop-rep object-rep values-rep rep-utils)
(typecheck tc-subst check-below)
@ -96,8 +96,8 @@
(loop derived-ors (cons p derived-atoms) worklist)]
[(AndProp: qs) (loop derived-ors derived-atoms (append qs worklist))]
[(== -tt prop-equal?) (loop derived-ors derived-atoms worklist)]
[(== -ff prop-equal?) (values #f #f)])]
[(TrueProp:) (loop derived-ors derived-atoms worklist)]
[(FalseProp:) (values #f #f)])]
[_ (values derived-ors derived-atoms)])))
@ -148,8 +148,10 @@
(merge-dty dty1 dty2))]
;; otherwise, error
[else
(tc-error/expr "Expected the same number of values, but got ~a and ~a"
(length results1) (length results2))])])
(tc-error/expr "Expected the same number of values, but got ~a"
(if (< (length results1) (length results2))
(format "~a and ~a." (length results1) (length results2))
(format "~a and ~a." (length results2) (length results1))))])])
(for/fold ([res (ret -Bottom)]) ([res2 (in-list results)])
(merge-two-results res res2)))

View File

@ -9,7 +9,7 @@
(typecheck signatures tc-funapp tc-metafunctions)
(types base-abbrev resolve utils type-table)
(rep type-rep)
(utils tc-utils)
(utils tc-utils hset)
(for-template racket/base))
(import tc-expr^)
@ -41,8 +41,8 @@
[_ (int-err "non-symbol methods not supported by Typed Racket: ~a"
rcvr-type)])]
;; union of objects, check pointwise and union the results
[(Union: (list (and objs (Instance: _)) ...))
(merge-tc-results (map do-check objs))]
[(Union: objs) #:when (for/and ([t (in-hset objs)]) (Instance? t))
(merge-tc-results (hset-map objs do-check))]
[_ (tc-error/expr/fields
"send: type mismatch"
"expected" "an object"

View File

@ -163,15 +163,15 @@
(define poly-base
(if (null? tvars)
name-type
(make-App name-type (map make-F tvars) #f)))
(make-App name-type (map make-F tvars))))
;; is this structure covariant in *all* arguments?
(define (covariant-for? fields mutable)
(for*/and ([var (in-list tvars)]
[t (in-list fields)])
(let ([variance (hash-ref (free-vars-hash (free-vars* t)) var Constant)])
(or (eq? variance Constant)
(and (not mutable) (eq? variance Covariant))))))
(let ([variance (hash-ref (free-vars-hash (free-vars* t)) var variance:const)])
(or (variance:const? variance)
(and (not mutable) (variance:co? variance))))))
(define covariant?
(and (covariant-for? self-fields mutable)
(covariant-for? parent-fields parent-mutable)))

View File

@ -201,4 +201,4 @@
[else
(-not-type (make-Path flds nm) (subst not-ty-at-flds))]))]
;; else default fold over subfields
[_ (Rep-fold subst rep)])))
[_ (Rep-fmap rep subst)])))

View File

@ -5,7 +5,7 @@
racket/list racket/dict racket/match racket/sequence
(prefix-in c: (contract-req))
(rep core-rep type-rep values-rep)
(types utils abbrev type-table struct-table)
(types utils abbrev type-table struct-table resolve)
(private parse-type type-annotation syntax-properties type-contract)
(env global-env init-envs type-name-env type-alias-env
lexical-env env-req mvar-env scoped-tvar-env
@ -101,7 +101,7 @@
[mk-ty (match struct-type
[(Poly-names: ns body)
(make-Poly ns
((map fld-t (Struct-flds body)) #f . ->* . (make-App t (map make-F ns) #f)))]
((map fld-t (Struct-flds body)) #f . ->* . (make-App t (map make-F ns))))]
[else
((map fld-t (Struct-flds struct-type)) #f . ->* . t)])])
(register-type #'r.name mk-ty)
@ -400,12 +400,16 @@
[else (int-err "Two conflicting definitions: ~a ~a" def other-def)]))
(dict-update h (binding-name def) merge-def-bindings #f)))
(do-time "computed def-tbl")
;; check that all parsed apps are sensible
(check-registered-apps!)
;; typecheck the expressions and the rhss of defintions
;(displayln "Starting pass2")
(for-each tc-toplevel/pass2 forms)
(do-time "Finished pass2")
;; check that declarations correspond to definitions
;; and that any additional parsed apps are sensible
(check-all-registered-types)
(check-registered-apps!)
;; log messages to check-syntax to show extra types / arrows before failures
(log-message online-check-syntax-logger
'info

View File

@ -135,7 +135,7 @@
;; has no meaningful type to print
['no-type #f]
;; don't print results of type void
[(tc-result1: (== -Void type-equal?)) #f]
[(tc-result1: (== -Void)) #f]
;; don't print results of unknown type
[(tc-any-results: f) #f]
[(tc-result1: t f o)

View File

@ -12,12 +12,18 @@
racket/function
(prefix-in c: (contract-req))
(rename-in (rep type-rep prop-rep object-rep values-rep)
(rename-in (rep rep-utils type-rep prop-rep object-rep values-rep)
[make-Base make-Base*])
(types union numeric-tower prefab)
(types numeric-tower prefab)
;; Using this form so all-from-out works
"base-abbrev.rkt" "match-expanders.rkt"
;; signature env req here is so it is statically required by
;; the code loaded during typechecking, otherwise we get
;; a `reference to a module that is not available` error
;; from references generated by init-envs
(env signature-env)
(for-syntax racket/base syntax/parse)
;; for base type contracts and predicates
@ -44,7 +50,7 @@
(only-in '#%place place? place-channel?))
(provide (except-out (all-defined-out) make-Base)
(all-from-out "base-abbrev.rkt" "match-expanders.rkt"))
(except-out (all-from-out "base-abbrev.rkt" "match-expanders.rkt") make-arr))
;; All the types defined here are not numeric
(define (make-Base name contract predicate)
@ -189,19 +195,6 @@
(define Syntax-Sexp (-Sexpof Any-Syntax))
(define Ident (-Syntax -Symbol))
(define -HT make-Hashtable)
(define/decl -StructTypeTop (make-StructTypeTop))
(define/decl -BoxTop (make-BoxTop))
(define/decl -Weak-BoxTop (make-Weak-BoxTop))
(define/decl -ChannelTop (make-ChannelTop))
(define/decl -Async-ChannelTop (make-Async-ChannelTop))
(define/decl -HashTop (make-HashtableTop))
(define/decl -VectorTop (make-VectorTop))
(define/decl -MPairTop (make-MPairTop))
(define/decl -Thread-CellTop (make-ThreadCellTop))
(define/decl -Prompt-TagTop (make-Prompt-TagTop))
(define/decl -Continuation-Mark-KeyTop (make-Continuation-Mark-KeyTop))
(define/decl -ClassTop (make-ClassTop))
(define/decl -UnitTop (make-UnitTop))
(define/decl -Port (Un -Output-Port -Input-Port))
(define/decl -SomeSystemPath (Un -Path -OtherSystemPath))
(define/decl -Pathlike (Un -String -Path))
@ -252,13 +245,6 @@
(define/decl -Environment-Variables
(make-Base 'Environment-Variables #'environment-variables? environment-variables?))
;; Paths
(define/decl -car (make-CarPE))
(define/decl -cdr (make-CdrPE))
(define/decl -syntax-e (make-SyntaxPE))
(define/decl -force (make-ForcePE))
(define/decl -field (make-FieldPE))
;; Type alias names
(define (-struct-name name)
(make-Name name 0 #t))

View File

@ -6,7 +6,8 @@
;; extends it with more types and type abbreviations.
(require "../utils/utils.rkt"
(rep type-rep prop-rep object-rep values-rep rep-utils)
"../rep/type-rep.rkt"
(rep prop-rep object-rep values-rep rep-utils)
(env mvar-env)
racket/match racket/list (prefix-in c: (contract-req))
(for-syntax racket/base syntax/parse racket/list)
@ -17,40 +18,21 @@
-is-type
-not-type
-id-path
(all-from-out "../rep/type-rep.rkt")
(rename-out [make-Listof -lst]
[make-MListof -mlst]))
;; This table maps types (or really, the sequence number of the type)
;; to identifiers that are those types. This allows us to avoid
;; reconstructing the type when using it from its marshaled
;; representation. The table is referenced in env/init-env.rkt
;;
;; For example, instead of marshalling a big union for `Integer`, we
;; simply emit `-Integer`, which evaluates to the right type.
(define predefined-type-table (make-hasheq))
(define-syntax-rule (declare-predefined-type! id)
(hash-set! predefined-type-table (Rep-seq id) #'id))
(provide predefined-type-table)
(define-syntax-rule (define/decl id e)
(begin (define id e)
(declare-predefined-type! id)))
;; Top and error types
(define/decl Univ (make-Univ))
(define/decl -Bottom (make-Bottom))
(define/decl Err (make-Error))
(define/decl -False (make-Value #f))
(define/decl -True (make-Value #t))
(define/decl -Boolean (make-Union (list -False -True)))
(define/decl -Boolean (Un -False -True))
(define -val make-Value)
(define/decl -Null (-val null))
;; Char type and List type (needed because of how sequences are checked in subtype)
(define/decl -Char (make-Base 'Char #'char? char? #f))
(define/decl -Null (-val null))
(define (make-Listof elem) (-mu list-rec (simple-Un -Null (make-Pair elem list-rec))))
(define (make-MListof elem) (-mu list-rec (simple-Un -Null (make-MPair elem list-rec))))
(define (make-Listof elem) (-mu list-rec (Un -Null (make-Pair elem list-rec))))
(define (make-MListof elem) (-mu list-rec (Un -Null (make-MPair elem list-rec))))
;; Needed for evt checking in subtype.rkt
(define/decl -Symbol (make-Base 'Symbol #'symbol? symbol? #f))
@ -68,21 +50,6 @@
(define (-Tuple* l b)
(foldr -pair b l))
;; Simple union type constructor, does not check for overlaps
;; Normalizes representation by sorting types.
;; Type * -> Type
;; The input types can be union types, but should not have a complicated
;; overlap relationship.
(define simple-Un
(let ([flat (match-lambda
[(Union: es) es]
[t (list t)])])
(case-lambda
[() -Bottom]
[(t) t]
[args
(make-Union (remove-duplicates (append-map flat args) type-equal?))])))
;; Recursive types
(define-syntax -v
(syntax-rules ()
@ -104,11 +71,8 @@
(make-Result t pset o)]))
;; Propositions
(define/decl -tt (make-TrueProp))
(define/decl -ff (make-FalseProp))
(define/decl -tt-propset (make-PropSet -tt -tt))
(define/decl -ff-propset (make-PropSet -ff -ff))
(define/decl -empty-obj (make-Empty))
(define (-arg-path arg [depth 0])
(make-Path null (cons depth arg)))

View File

@ -140,7 +140,7 @@
(append (dict-keys fields) field-cs)
(append (dict-keys methods) method-cs)
(append (dict-keys augments) augment-cs)))]
[_ (Rep-walk infer! cur)]))
[_ (Rep-for-each cur infer!)]))
(map remove-duplicates constraints))
;; infer-row : RowConstraints Type -> Row

View File

@ -31,8 +31,6 @@
(append t1s/t2s A))
(define-syntax-rule (seen? t1 t2 seen-ts)
(let ([seq1 (Rep-seq t1)]
[seq2 (Rep-seq t2)])
(for/or ([p (in-list seen-ts)])
(and (= (Rep-seq (car p)) seq1)
(= (Rep-seq (cdr p)) seq2)))))
(for/or ([p (in-list seen-ts)])
(and (equal? (car p) t1)
(equal? (cdr p) t2))))

View File

@ -2,7 +2,7 @@
(require "../utils/utils.rkt"
(rep type-rep)
"abbrev.rkt" "subtype.rkt" "substitute.rkt" "union.rkt"
"abbrev.rkt" "subtype.rkt" "substitute.rkt"
"numeric-tower.rkt"
racket/match)

View File

@ -89,29 +89,26 @@
(define (prefix-of a b)
(define (rest-equal? a b)
(match* (a b)
[(#f #f) #t]
[(a a) #t]
[(#f _) #f]
[(_ #f) #f]
[(a b) (type-equal? a b)]))
[(_ _) #f]))
(define (drest-equal? a b)
(match* (a b)
[((list t b) (list t* b*)) (and (type-equal? t t*) (equal? b b*))]
[((list t b) (list t b)) #t]
[(#f #f) #t]
[(_ _) #f]))
(define (kw-equal? a b)
(and (equal? (length a) (length b))
(for/and ([k1 (in-list a)] [k2 (in-list b)])
(type-equal? k1 k2))))
(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*)
(type-equal? result result*)
(kw-equal? kws kws*)
(for/and ([p (in-list args)] [p* (in-list args*)])
(type-equal? p p*)))]))
(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

View File

@ -1,26 +1,62 @@
#lang racket/base
(require "../utils/utils.rkt")
(require (rep type-rep values-rep rep-utils)
(require "../utils/utils.rkt"
(utils hset)
(rep type-rep values-rep rep-utils)
racket/match
(types resolve)
(contract-req)
racket/set
syntax/parse/define
(types resolve base-abbrev)
(for-syntax racket/base syntax/parse))
(provide Listof: List: MListof: AnyPoly: AnyPoly-names: Function/arrs:
SimpleListof: SimpleMListof:
PredicateProp:)
(define-match-expander Listof:
(lambda (stx)
(syntax-parse stx
[(_ elem-pat (~optional var-pat #:defaults ([var-pat #'var])))
[(_ elem-pat)
(syntax/loc stx
(or (Mu: var-pat (Union: (list (Value: '()) (Pair: elem-pat (F: var-pat)))))
(Mu: var-pat (Union: (list (Pair: elem-pat (F: var-pat)) (Value: '()))))))])))
(app Listof? (? Type? elem-pat)))])))
(define-match-expander SimpleListof:
(lambda (stx)
(syntax-parse stx
[(_ elem-pat)
(syntax/loc stx
(app (λ (t) (Listof? t #t)) (? Type? elem-pat)))])))
(define-simple-macro (make-Listof-pred listof-pred?:id pair-matcher:id)
(define (listof-pred? t [simple? #f])
(match t
[(Mu-unsafe: (Union: elems))
#:when (and (= 2 (hset-count elems))
(hset-member? elems -Null))
(match (hset-first (hset-remove elems -Null))
[(pair-matcher elem-t (B: 0))
(define elem-t* (instantiate-raw-type t elem-t))
(cond
[simple? (and (equal? elem-t elem-t*) elem-t)]
[else elem-t*])]
[_ #f])]
[(Union: elems)
#:when (and (= 2 (hset-count elems))
(hset-member? elems -Null))
(match (hset-first (hset-remove elems -Null))
[(pair-matcher hd-t tl-t)
(cond
[(listof-pred? tl-t)
=> (λ (lst-t) (and (equal? hd-t lst-t) hd-t))]
[else #f])]
[_ #f])]
[_ #f])))
(make-Listof-pred Listof? Pair:)
(make-Listof-pred MListof? MPair:)
(define-match-expander List:
(lambda (stx)
@ -30,27 +66,33 @@
[(_ elem-pats #:tail tail-pat)
#'(? Type? (app untuple (? values elem-pats) tail-pat))])))
(define-match-expander MListof:
(lambda (stx)
(syntax-parse stx
[(_ elem-pat)
(syntax/loc stx (app MListof? (? Type? elem-pat)))])))
(define-match-expander SimpleMListof:
(lambda (stx)
(syntax-parse stx
[(_ elem-pat)
(syntax/loc stx (app (λ (t) (MListof? t #t)) (? Type? elem-pat)))])))
;; Type? -> (or/c (values/c #f #f) (values/c (listof Type?) Type?)))
;; Returns the prefix of types that are consed on to the last type (a non finite-pair type).
;; The last type may contain pairs if it is a list type.
(define (untuple t)
(let loop ((t t) (seen (set)))
(if (not (set-member? seen (Rep-seq t)))
(let loop ([t t]
[seen (hset)])
(if (not (hset-member? seen t))
(match (resolve t)
[(Pair: a b)
(define-values (elems tail) (loop b (set-add seen (Rep-seq t))))
(define-values (elems tail) (loop b (hset-add seen t)))
(values (cons a elems) tail)]
[_ (values null t)])
(values null t))))
(define-match-expander MListof:
(lambda (stx)
(syntax-parse stx
[(_ elem-pat (~optional var-pat #:defaults ([var-pat #'var])))
;; see note above
#'(or (Mu: var-pat (Union: (list (Value: '()) (MPair: elem-pat (F: var-pat)))))
(Mu: var-pat (Union: (list (MPair: elem-pat (F: var-pat)) (Value: '())))))])))
(define (unpoly t)
(match t
[(Poly: fixed-vars t)

View File

@ -1,8 +1,8 @@
#lang racket/base
(require "../utils/utils.rkt"
(rename-in (types numeric-predicates base-abbrev)
[simple-Un *Un])
(rep rep-utils)
(types numeric-predicates base-abbrev)
(rename-in (rep type-rep) [make-Base make-Base*])
racket/function
racket/extflonum
@ -59,15 +59,15 @@
(define/decl -One (make-Value 1))
;; Infinities (These are part of Flonum/Single-Flonum, but useful abbreviatios.)
(define/decl -PosInfinity (*Un (-val +inf.0) (-val +inf.f)))
(define/decl -NegInfinity (*Un (-val -inf.0) (-val -inf.f)))
(define/decl -PosInfinity (Un (-val +inf.0) (-val +inf.f)))
(define/decl -NegInfinity (Un (-val -inf.0) (-val -inf.f)))
;; Integers
(define/decl -Byte>1 (make-Base 'Byte-Larger-Than-One ; unsigned
#'(and/c byte? (lambda (x) (> x 1)))
(conjoin byte? (lambda (x) (> x 1)))))
(define/decl -PosByte (*Un -One -Byte>1))
(define/decl -Byte (*Un -Zero -PosByte))
(define/decl -PosByte (Un -One -Byte>1))
(define/decl -Byte (Un -Zero -PosByte))
(define/decl -PosIndexNotByte
(make-Base 'Positive-Index-Not-Byte
;; index? will be checked at runtime, can be platform-specific
@ -76,23 +76,23 @@
(lambda (x) (and (portable-index? x)
(positive? x)
(not (byte? x))))))
(define/decl -PosIndex (*Un -One -Byte>1 -PosIndexNotByte))
(define/decl -Index (*Un -Zero -PosIndex))
(define/decl -PosIndex (Un -One -Byte>1 -PosIndexNotByte))
(define/decl -Index (Un -Zero -PosIndex))
(define/decl -PosFixnumNotIndex
(make-Base 'Positive-Fixnum-Not-Index
#'(and/c fixnum? positive? (not/c index?))
(lambda (x) (and (portable-fixnum? x)
(positive? x)
(not (portable-index? x))))))
(define/decl -PosFixnum (*Un -PosFixnumNotIndex -PosIndex))
(define/decl -NonNegFixnum (*Un -PosFixnum -Zero))
(define/decl -PosFixnum (Un -PosFixnumNotIndex -PosIndex))
(define/decl -NonNegFixnum (Un -PosFixnum -Zero))
(define/decl -NegFixnum
(make-Base 'Negative-Fixnum
#'(and/c fixnum? negative?)
(lambda (x) (and (portable-fixnum? x)
(negative? x)))))
(define/decl -NonPosFixnum (*Un -NegFixnum -Zero))
(define/decl -Fixnum (*Un -NegFixnum -Zero -PosFixnum))
(define/decl -NonPosFixnum (Un -NegFixnum -Zero))
(define/decl -Fixnum (Un -NegFixnum -Zero -PosFixnum))
;; This type, and others like it, should *not* be exported, or used for
;; anything but building unions. Especially, no literals should be given
;; these types.
@ -102,8 +102,8 @@
(lambda (x) (and (exact-integer? x)
(positive? x)
(not (portable-fixnum? x))))))
(define/decl -PosInt (*Un -PosIntNotFixnum -PosFixnum))
(define/decl -NonNegInt (*Un -PosInt -Zero))
(define/decl -PosInt (Un -PosIntNotFixnum -PosFixnum))
(define/decl -NonNegInt (Un -PosInt -Zero))
(define/decl -Nat -NonNegInt)
(define/decl -NegIntNotFixnum
(make-Base 'Negative-Integer-Not-Fixnum
@ -111,9 +111,9 @@
(lambda (x) (and (exact-integer? x)
(negative? x)
(not (portable-fixnum? x))))))
(define/decl -NegInt (*Un -NegIntNotFixnum -NegFixnum))
(define/decl -NonPosInt (*Un -NegInt -Zero))
(define/decl -Int (*Un -NegInt -Zero -PosInt))
(define/decl -NegInt (Un -NegIntNotFixnum -NegFixnum))
(define/decl -NonPosInt (Un -NegInt -Zero))
(define/decl -Int (Un -NegInt -Zero -PosInt))
;; Rationals
(define/decl -PosRatNotInt
@ -122,17 +122,17 @@
(lambda (x) (and (exact-rational? x)
(positive? x)
(not (exact-integer? x))))))
(define/decl -PosRat (*Un -PosRatNotInt -PosInt))
(define/decl -NonNegRat (*Un -PosRat -Zero))
(define/decl -PosRat (Un -PosRatNotInt -PosInt))
(define/decl -NonNegRat (Un -PosRat -Zero))
(define/decl -NegRatNotInt
(make-Base 'Negative-Rational-Not-Integer
#'(and/c exact-rational? negative? (not/c integer?))
(lambda (x) (and (exact-rational? x)
(negative? x)
(not (exact-integer? x))))))
(define/decl -NegRat (*Un -NegRatNotInt -NegInt))
(define/decl -NonPosRat (*Un -NegRat -Zero))
(define/decl -Rat (*Un -NegRat -Zero -PosRat))
(define/decl -NegRat (Un -NegRatNotInt -NegInt))
(define/decl -NonPosRat (Un -NegRat -Zero))
(define/decl -Rat (Un -NegRat -Zero -PosRat))
;; Floating-point numbers
;; NaN is included in all floating-point types
@ -148,20 +148,20 @@
(make-Base 'Float-Negative-Zero
#'(lambda (x) (eqv? x -0.0))
(lambda (x) (eqv? x -0.0))))
(define/decl -FlonumZero (*Un -FlonumPosZero -FlonumNegZero -FlonumNan))
(define/decl -FlonumZero (Un -FlonumPosZero -FlonumNegZero -FlonumNan))
(define/decl -PosFlonumNoNan
(make-Base 'Positive-Float-No-NaN
#'(and/c flonum? positive?)
(lambda (x) (and (flonum? x) (positive? x)))))
(define/decl -PosFlonum (*Un -PosFlonumNoNan -FlonumNan))
(define/decl -NonNegFlonum (*Un -PosFlonum -FlonumZero))
(define/decl -PosFlonum (Un -PosFlonumNoNan -FlonumNan))
(define/decl -NonNegFlonum (Un -PosFlonum -FlonumZero))
(define/decl -NegFlonumNoNan
(make-Base 'Negative-Float-No-NaN
#'(and/c flonum? negative?)
(lambda (x) (and (flonum? x) (negative? x)))))
(define/decl -NegFlonum (*Un -NegFlonumNoNan -FlonumNan))
(define/decl -NonPosFlonum (*Un -NegFlonum -FlonumZero))
(define/decl -Flonum (*Un -NegFlonumNoNan -FlonumNegZero -FlonumPosZero -PosFlonumNoNan -FlonumNan)) ; 64-bit floats
(define/decl -NegFlonum (Un -NegFlonumNoNan -FlonumNan))
(define/decl -NonPosFlonum (Un -NegFlonum -FlonumZero))
(define/decl -Flonum (Un -NegFlonumNoNan -FlonumNegZero -FlonumPosZero -PosFlonumNoNan -FlonumNan)) ; 64-bit floats
;; inexact reals can be flonums (64-bit floats) or 32-bit floats
(define/decl -SingleFlonumNan
(make-Base 'Single-Flonum-Nan
@ -176,40 +176,40 @@
(make-Base 'Single-Flonum-Negative-Zero
#'(lambda (x) (eqv? x -0.0f0))
(lambda (x) (eqv? x -0.0f0))))
(define/decl -SingleFlonumZero (*Un -SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumNan))
(define/decl -InexactRealNan (*Un -FlonumNan -SingleFlonumNan))
(define/decl -InexactRealPosZero (*Un -SingleFlonumPosZero -FlonumPosZero))
(define/decl -InexactRealNegZero (*Un -SingleFlonumNegZero -FlonumNegZero))
(define/decl -InexactRealZero (*Un -InexactRealPosZero
(define/decl -SingleFlonumZero (Un -SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumNan))
(define/decl -InexactRealNan (Un -FlonumNan -SingleFlonumNan))
(define/decl -InexactRealPosZero (Un -SingleFlonumPosZero -FlonumPosZero))
(define/decl -InexactRealNegZero (Un -SingleFlonumNegZero -FlonumNegZero))
(define/decl -InexactRealZero (Un -InexactRealPosZero
-InexactRealNegZero
-InexactRealNan))
(define/decl -PosSingleFlonumNoNan
(make-Base 'Positive-Single-Flonum-No-Nan
#'(and/c single-flonum? positive?)
(lambda (x) (and (single-flonum? x) (positive? x)))))
(define/decl -PosSingleFlonum (*Un -PosSingleFlonumNoNan -SingleFlonumNan))
(define/decl -PosInexactReal (*Un -PosSingleFlonum -PosFlonum))
(define/decl -NonNegSingleFlonum (*Un -PosSingleFlonum -SingleFlonumZero))
(define/decl -NonNegInexactReal (*Un -PosInexactReal -InexactRealZero))
(define/decl -PosSingleFlonum (Un -PosSingleFlonumNoNan -SingleFlonumNan))
(define/decl -PosInexactReal (Un -PosSingleFlonum -PosFlonum))
(define/decl -NonNegSingleFlonum (Un -PosSingleFlonum -SingleFlonumZero))
(define/decl -NonNegInexactReal (Un -PosInexactReal -InexactRealZero))
(define/decl -NegSingleFlonumNoNan
(make-Base 'Negative-Single-Flonum-No-Nan
#'(and/c single-flonum? negative?)
(lambda (x) (and (single-flonum? x) (negative? x)))))
(define/decl -NegSingleFlonum (*Un -NegSingleFlonumNoNan -SingleFlonumNan))
(define/decl -NegInexactReal (*Un -NegSingleFlonum -NegFlonum))
(define/decl -NonPosSingleFlonum (*Un -NegSingleFlonum -SingleFlonumZero))
(define/decl -NonPosInexactReal (*Un -NegInexactReal -InexactRealZero))
(define/decl -SingleFlonum (*Un -NegSingleFlonum -SingleFlonumNegZero -SingleFlonumPosZero -PosSingleFlonum -SingleFlonumNan))
(define/decl -InexactReal (*Un -SingleFlonum -Flonum))
(define/decl -NegSingleFlonum (Un -NegSingleFlonumNoNan -SingleFlonumNan))
(define/decl -NegInexactReal (Un -NegSingleFlonum -NegFlonum))
(define/decl -NonPosSingleFlonum (Un -NegSingleFlonum -SingleFlonumZero))
(define/decl -NonPosInexactReal (Un -NegInexactReal -InexactRealZero))
(define/decl -SingleFlonum (Un -NegSingleFlonum -SingleFlonumNegZero -SingleFlonumPosZero -PosSingleFlonum -SingleFlonumNan))
(define/decl -InexactReal (Un -SingleFlonum -Flonum))
;; Reals
(define/decl -RealZero (*Un -Zero -InexactRealZero))
(define/decl -RealZeroNoNan (*Un -Zero -InexactRealPosZero -InexactRealNegZero))
(define/decl -PosReal (*Un -PosRat -PosInexactReal))
(define/decl -NonNegReal (*Un -NonNegRat -NonNegInexactReal))
(define/decl -NegReal (*Un -NegRat -NegInexactReal))
(define/decl -NonPosReal (*Un -NonPosRat -NonPosInexactReal))
(define/decl -Real (*Un -Rat -InexactReal))
(define/decl -RealZero (Un -Zero -InexactRealZero))
(define/decl -RealZeroNoNan (Un -Zero -InexactRealPosZero -InexactRealNegZero))
(define/decl -PosReal (Un -PosRat -PosInexactReal))
(define/decl -NonNegReal (Un -NonNegRat -NonNegInexactReal))
(define/decl -NegReal (Un -NegRat -NegInexactReal))
(define/decl -NonPosReal (Un -NonPosRat -NonPosInexactReal))
(define/decl -Real (Un -Rat -InexactReal))
;; Complexes
;; We could go into _much_ more precision here.
@ -290,11 +290,11 @@
(and (number? x)
(single-flonum? (imag-part x))
(single-flonum? (real-part x))))))
(define/decl -ExactNumber (*Un -ExactImaginary -ExactComplex -Rat))
(define/decl -InexactImaginary (*Un -FloatImaginary -SingleFlonumImaginary))
(define/decl -Imaginary (*Un -ExactImaginary -InexactImaginary))
(define/decl -InexactComplex (*Un -FloatComplex -SingleFlonumComplex))
(define/decl -Complex (*Un -Real -Imaginary -ExactComplex -InexactComplex))
(define/decl -ExactNumber (Un -ExactImaginary -ExactComplex -Rat))
(define/decl -InexactImaginary (Un -FloatImaginary -SingleFlonumImaginary))
(define/decl -Imaginary (Un -ExactImaginary -InexactImaginary))
(define/decl -InexactComplex (Un -FloatComplex -SingleFlonumComplex))
(define/decl -Complex (Un -Real -Imaginary -ExactComplex -InexactComplex))
(define/decl -Number -Complex)
;; 80-bit floating-point numbers
@ -329,9 +329,9 @@
(lambda (x) (and (extflonum? x) (extfl>= x 0.0t0)))
#f))
(define/decl -ExtFlonumZero (*Un -ExtFlonumPosZero -ExtFlonumNegZero -ExtFlonumNan))
(define/decl -PosExtFlonum (*Un -PosExtFlonumNoNan -ExtFlonumNan))
(define/decl -NonNegExtFlonum (*Un -PosExtFlonum -ExtFlonumZero))
(define/decl -NegExtFlonum (*Un -NegExtFlonumNoNan -ExtFlonumNan))
(define/decl -NonPosExtFlonum (*Un -NegExtFlonum -ExtFlonumZero))
(define/decl -ExtFlonum (*Un -NegExtFlonumNoNan -ExtFlonumNegZero -ExtFlonumPosZero -PosExtFlonumNoNan -ExtFlonumNan))
(define/decl -ExtFlonumZero (Un -ExtFlonumPosZero -ExtFlonumNegZero -ExtFlonumNan))
(define/decl -PosExtFlonum (Un -PosExtFlonumNoNan -ExtFlonumNan))
(define/decl -NonNegExtFlonum (Un -PosExtFlonum -ExtFlonumZero))
(define/decl -NegExtFlonum (Un -NegExtFlonumNoNan -ExtFlonumNan))
(define/decl -NonPosExtFlonum (Un -NegExtFlonum -ExtFlonumZero))
(define/decl -ExtFlonum (Un -NegExtFlonumNoNan -ExtFlonumNegZero -ExtFlonumPosZero -PosExtFlonumNoNan -ExtFlonumNan))

View File

@ -1,6 +1,7 @@
#lang racket/base
(require "../utils/utils.rkt"
(utils hset)
(rep type-rep rep-utils type-mask)
(prefix-in c: (contract-req))
(types abbrev subtype resolve utils)
@ -40,8 +41,8 @@
(define/cond-contract (overlap? t1 t2)
(c:-> Type? Type? boolean?)
(cond
[(type-equal? t1 t2) #t]
[(disjoint-masks? (Type-mask t1) (Type-mask t2)) #f]
[(equal? t1 t2) #t]
[(disjoint-masks? (mask t1) (mask t2)) #f]
[(seen? t1 t2) #t]
[else
(with-updated-seen
@ -58,15 +59,24 @@
(? App? s)))
#:no-order
(overlap? t (resolve-once s))]
[((? Mu? t) s) #:no-order (overlap? (unfold t) s)]
[((Refinement: t _) s) #:no-order (overlap? t s)]
[((Union: ts) s)
#:no-order
(ormap (λ (t) (overlap? t s)) ts)]
[((? Mu? t1) t2) #:no-order (overlap? (unfold t1) t2)]
[((Refinement: t1 _) t2) #:no-order (overlap? t1 t2)]
[((Union: ts1) t2)
(match t2
[(Union: ts2)
(or (hset-overlap? ts1 ts2)
(for*/or ([t1 (in-hset ts1)]
[t2 (in-hset ts2)])
(overlap? t1 t2)))]
[_ (or (hset-member? ts1 t2)
(for/or ([t1 (in-hset ts1)])
(overlap? t1 t2)))])]
[(t1 (Union: ts2))
(or (hset-member? ts2 t1)
(for/or ([t2 (in-hset ts2)]) (overlap? t1 t2)))]
[((Intersection: ts) s)
#:no-order
(for/and ([t (in-list ts)])
(overlap? t s))]
(for/and ([t (in-hset ts)]) (overlap? t s))]
[((or (Poly-unsafe: _ t1)
(PolyDots-unsafe: _ t1))
t2)

View File

@ -4,9 +4,9 @@
racket/match racket/set
(contract-req)
(rep object-rep type-rep values-rep)
(utils tc-utils)
(utils tc-utils hset)
(typecheck renamer)
(types subtype resolve union)
(types subtype resolve)
(except-in (types utils abbrev kw-types) -> ->* one-of/c))
(require-for-cond-contract (rep rep-utils))
@ -31,7 +31,7 @@
(match* (t path)
;; empty path
[(t (list)) t]
;; pair ops
[((Pair: t s) (cons (CarPE:) rst))
(path-type rst t (hash))]
@ -53,16 +53,13 @@
(path-type rst ft (hash)))]
[((Intersection: ts) _)
(apply -unsafe-intersect (for*/list ([t (in-list ts)]
(apply -unsafe-intersect (for*/list ([t (in-hset ts)]
[t (in-value (path-type path t resolved))]
#:when t)
t))]
[((Union: ts) _)
(apply Un (for*/list ([t (in-list ts)]
[t (in-value (path-type path t resolved))]
#:when t)
t))]
(Union-map ts (λ (t) (or (path-type path t resolved) -Bottom)))]
;; paths into polymorphic types
;; TODO can this expose unbound type indices... probably. It should be
;; shielded with a check for type indexes/variables/whatever.
@ -70,7 +67,7 @@
[((PolyDots: _ body-t) _) (path-type path body-t resolved)]
[((PolyRow: _ _ body-t) _) (path-type path body-t resolved)]
[((Distinction: _ _ t) _) (path-type path t resolved)]
;; for private fields in classes
[((Function: (list (arr: doms (Values: (list (Result: rng _ _))) _ _ _)))
(cons (FieldPE:) rst))
@ -78,8 +75,9 @@
;; types which need resolving
[((? resolvable?) _) #:when (not (hash-ref resolved t #f))
(path-type path (resolve-once t) (hash-set resolved t #t))]
(path-type path (resolve-once t) (hash-set resolved t #t))]
;; type/path mismatch =(
[(_ _) #f])))

View File

@ -13,11 +13,13 @@
"types/match-expanders.rkt"
"types/kw-types.rkt"
"types/utils.rkt" "types/abbrev.rkt"
"types/union.rkt"
"types/resolve.rkt"
"types/prefab.rkt"
"utils/utils.rkt"
"utils/primitive-comparison.rkt"
"utils/tc-utils.rkt")
"utils/tc-utils.rkt"
"utils/hset.rkt")
(for-syntax racket/base syntax/parse))
;; printer-type: (one-of/c 'custom 'debug)
@ -65,7 +67,7 @@
(define (has-name? t)
(define candidates
(for/list ([(n t*) (in-dict (force (current-type-names)))]
#:when (and print-aliases (Type? t*) (type-equal? t t*)))
#:when (and print-aliases (Type? t*) (equal? t t*)))
n))
(and (pair? candidates)
(sort candidates string>? #:key symbol->string #:cache-keys? #t)))
@ -165,13 +167,13 @@
;; We do set coverage, with the elements of the union being what we want to
;; cover, and all the names types we know about being the sets.
(define (cover-union t ignored-names)
(match-define (Union: elems) t)
(match-define (Union: (app hset->list elems)) t)
(define valid-names
;; We keep only unions, and only those that are subtypes of t.
;; It's no use attempting to cover t with things that go outside of t.
(filter (lambda (p)
(match p
[(cons name (and t* (Union: elts)))
[(cons name (? Union? t*))
(and (not (member name ignored-names))
(subtype t* t))]
[_ #f]))
@ -180,7 +182,7 @@
;; note that racket/set supports lists with equal?, which in
;; the case of Types will be type-equal?
(define candidates
(map (match-lambda [(cons name (Union: elts)) (cons name elts)])
(map (match-lambda [(cons name (Union: (app hset->list elts))) (cons name elts)])
valid-names))
;; some types in the union may not be coverable by the candidates
;; (e.g. type variables, etc.)
@ -487,16 +489,15 @@
[(MPairTop:) 'MPairTop]
[(Prompt-TagTop:) 'Prompt-TagTop]
[(Continuation-Mark-KeyTop:) 'Continuation-Mark-KeyTop]
[(App: rator rands stx)
[(App: rator rands)
(list* (type->sexp rator) (map type->sexp rands))]
;; Special cases for lists. Avoid printing with these cases if the
;; element type refers to the Mu variable (otherwise it prints the
;; type variable with no binding).
[(Listof: elem-ty var)
#:when (not (memq var (fv elem-ty)))
[(SimpleListof: elem-ty)
;; in the 'elem-ty' type
`(Listof ,(t->s elem-ty))]
[(MListof: elem-ty var)
#:when (not (memq var (fv elem-ty)))
[(SimpleMListof: elem-ty)
`(MListof ,(t->s elem-ty))]
;; format as a string to preserve reader abbreviations and primitive
;; values like characters (when `display`ed)
@ -526,10 +527,13 @@
[(CustodianBox: e) `(CustodianBoxof ,(t->s e))]
[(Set: e) `(Setof ,(t->s e))]
[(Evt: r) `(Evtof ,(t->s r))]
[(Union: elems)
(define-values (covered remaining) (cover-union type ignored-names))
(cons 'U (sort (append covered (map t->s remaining)) primitive<=?))]
[(Intersection: elems)
[(? Union? (app normalize-type type))
(match type
[(? Union?)
(define-values (covered remaining) (cover-union type ignored-names))
(cons 'U (sort (append covered (map t->s remaining)) primitive<=?))]
[_ (t->s type)])]
[(Intersection: (app hset->list elems))
(cons ' (sort (map t->s elems) primitive<=?))]
[(Pair: l r) `(Pairof ,(t->s l) ,(t->s r))]
[(ListDots: dty dbound) `(List ,(t->s dty) ... ,dbound)]
@ -563,7 +567,8 @@
(Vector: (F: x))
(Box: (F: x))))))
'Syntax]
[(Mu-name: name body) `(Rec ,name ,(t->s body))]
[(Mu-name: name body)
`(Rec ,name ,(t->s body))]
[(B: idx) `(B ,idx)]
[(Syntax: t) `(Syntaxof ,(t->s t))]
[(Instance: (and (? has-name?) cls)) `(Instance ,(t->s cls))]
@ -577,6 +582,7 @@
(export ,@(map signature->sexp exports))
(init-depend ,@(map signature->sexp init-depends))
,(values->sexp body))]
[(UnitTop:) 'UnitTop]
[(MPair: s t) `(MPairof ,(t->s s) ,(t->s t))]
[(Refinement: parent p?)
`(Refinement ,(t->s parent) ,(syntax-e p?))]

View File

@ -6,19 +6,21 @@
(rep type-rep prop-rep object-rep values-rep rep-utils)
(only-in (infer infer) intersect)
compatibility/mlist
(types union subtype overlap subtract abbrev tc-result))
racket/set
(types subtype overlap subtract abbrev tc-result union))
(provide/cond-contract
[-and (c:->* () #:rest (c:listof Prop?) Prop?)]
[-or (c:->* () #:rest (c:listof Prop?) Prop?)]
[implies-atomic? (c:-> Prop? Prop? boolean?)]
[implies? (c:-> Prop? Prop? boolean?)]
[prop-equiv? (c:-> Prop? Prop? boolean?)]
[negate-prop (c:-> Prop? Prop?)]
[complementary? (c:-> Prop? Prop? boolean?)]
[contradictory? (c:-> Prop? Prop? boolean?)]
[add-unconditional-prop-all-args (c:-> Function? Type? Function?)]
[add-unconditional-prop (c:-> tc-results/c Prop? tc-results/c)]
[erase-props (c:-> tc-results/c tc-results/c)]
[name-ref=? (c:-> name-ref/c name-ref/c boolean?)]
[reduce-propset/type (c:-> PropSet? Type? PropSet?)]
[reduce-tc-results/subsumption (c:-> tc-results/c tc-results/c)])
@ -27,8 +29,8 @@
;; its true proposition is -ff, etc)
(define (reduce-propset/type ps t)
(cond
[(type-equal? -Bottom t) -ff-propset]
[(type-equal? -False t) (-PS -ff (PropSet-els ps))]
[(Bottom? t) -ff-propset]
[(equal? -False t) (-PS -ff (PropSet-els ps))]
[(not (overlap? t -False)) (-PS (PropSet-thn ps) -ff)]
[else ps]))
@ -48,12 +50,12 @@
(define p- (if ps (PropSet-els ps) -tt))
(define o (if obj obj -empty-obj))
(cond
[(or (type-equal? -False t)
[(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)]
[(prop-equal? -ff p-) (tc-result (subtract t -False) (-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]
@ -70,129 +72,117 @@
;; Returns true if the AND of the two props is equivalent to FalseProp
(define (contradictory? p1 p2)
(match* (p1 p2)
[((TypeProp: o1 t1) (TypeProp: o2 t2))
#:when (object-equal? o1 o2)
(not (overlap? t1 t2))]
[((TypeProp: o1 t1) (NotTypeProp: o2 t2))
#:when (object-equal? o1 o2)
(subtype t1 t2)]
(and (eq? o1 o2) (subtype t1 t2))]
[((NotTypeProp: o2 t2) (TypeProp: o1 t1))
#:when (object-equal? o1 o2)
(subtype t1 t2)]
[(_ _) (or (prop-equal? p1 -ff)
(prop-equal? p2 -ff))]))
(and (eq? o1 o2) (subtype t1 t2))]
[((FalseProp:) _) #t]
[(_ (FalseProp:)) #t]
[(_ _) #f]))
;; complementary: Prop? Prop? -> boolean?
;; Returns true if the OR of the two props is equivalent to Top
(define (complementary? p1 p2)
(match* (p1 p2)
[((TypeProp: o1 t1) (NotTypeProp: o2 t2))
#:when (object-equal? o1 o2)
(subtype t2 t1)]
(and (eq? o1 o2) (subtype t2 t1))]
[((NotTypeProp: o2 t2) (TypeProp: o1 t1))
#:when (object-equal? o1 o2)
(subtype t2 t1)]
[(_ _) (or (prop-equal? p1 -tt)
(prop-equal? p2 -tt))]))
(define (name-ref=? a b)
(or (equal? a b)
(and (identifier? a)
(identifier? b)
(free-identifier=? a b))))
(and (eq? o1 o2) (subtype t2 t1))]
[((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 (implies-atomic? p q)
(match* (p q)
;; reflexivity
[(_ _) #:when (or (prop-equal? p q)
(prop-equal? q -tt)
(prop-equal? p -ff)) #t]
[(_ _) #:when (or (eq? p q)
(TrueProp? q)
(FalseProp? p)) #t]
;; ps ⊆ qs ?
[((OrProp: ps) (OrProp: qs))
(and (for/and ([p (in-list ps)])
(member p qs prop-equal?))
(memq p qs))
#t)]
;; p ∈ qs ?
[(p (OrProp: qs)) (and (member p qs prop-equal?) #t)]
[(p (OrProp: qs)) (and (memq p qs) #t)]
;; q ∈ ps ?
[((AndProp: ps) q) (and (member q ps prop-equal?) #t)]
[((AndProp: ps) q) (or (equal? p q) (and (memq q ps) #t))]
;; t1 <: t2 ?
[((TypeProp: o1 t1)
(TypeProp: o2 t2))
#:when (object-equal? o1 o2)
(subtype t1 t2)]
(and (eq? o1 o2) (subtype t1 t2))]
;; t2 <: t1 ?
[((NotTypeProp: o1 t1) (NotTypeProp: o2 t2))
#:when (object-equal? o1 o2)
(subtype t2 t1)]
[((NotTypeProp: o1 t1)
(NotTypeProp: o2 t2))
(and (eq? o1 o2) (subtype t2 t1))]
;; t1 ∩ t2 = ∅ ?
[((TypeProp: o1 t1) (NotTypeProp: o2 t2))
#:when (object-equal? o1 o2)
(not (overlap? t1 t2))]
[((TypeProp: o1 t1)
(NotTypeProp: o2 t2))
(and (eq? o1 o2) (not (overlap? t1 t2)))]
;; otherwise we give up
[(_ _) #f]))
;; intersect-update
;; (mlist (mcons Object Type)) Object Type -> (mlist (mcons Object Type))
(define (implies? p q)
(FalseProp? (-and p (negate-prop q))))
(define (prop-equiv? p q)
(and (implies? p q)
(implies? q p)))
;; helpers for compact
(define (intersect-update! dict t1 p)
(hash-update! dict p (λ (t2) (intersect t1 t2)) Univ))
(define (union-update! dict t1 p)
(hash-update! dict p (λ (t2) (Un t1 t2)) -Bottom))
;; compact : (listof prop) bool -> (listof prop)
;; props : propositions to compress
;; or? : is this an Or (alternative is And)
;;
;; updates mutable association list 'dict' entry for 'o' w/ type t
;; if no entry for 'o' is found, else if some previous type s is present
;; update the type to t ∩ s
(define (intersect-update dict o t)
(cond
[(massq o dict) => (λ (p)
(set-mcdr! p (intersect t (mcdr p)))
dict)]
[else (mcons (mcons o t) dict)]))
;; union-update
;; (mlist (mcons Object Type)) Object Type -> (mlist (mcons Object Type))
;; This combines all the TypeProps at the same path into one TypeProp. If it is an Or the
;; combination is done using Un, otherwise, intersect. The reverse is done for NotTypeProps.
;; If it is an Or this simplifies to -tt if any of the atomic props simplified to -tt, and
;; removes any -ff values. The reverse is done if this is an And.
;;
;; updates mutable association list 'dict' entry for 'o' w/ type t
;; if no entry for 'o' is found, else if some previous type s is present
;; update the type to t s
(define (union-update dict o t)
(cond
[(massq o dict) => (λ (p)
(set-mcdr! p (Un t (mcdr p)))
dict)]
[else (mcons (mcons o t) dict)]))
;; NOTE: this is significantly faster as a macro than a function (even
;; with define-inline)
(define-syntax-rule (compact props or?)
(match props
[(or (list) (list _)) props]
[_
(define tf-map (make-hash))
(define ntf-map (make-hash))
;; compact-or-props : (Listof prop) -> (Listof prop)
;;
;; This combines all the TypeProps at the same path into one TypeProp with Un, and
;; all of the NotTypeProps at the same path into one NotTypeProp with intersect.
;; The Or then simplifies to -tt if any of the atomic props simplified to -tt, and
;; any values of -ff are removed.
(define/cond-contract (compact-or-props props)
((c:listof Prop?) . c:-> . (c:listof Prop?))
(define-values (pos neg others)
(for/fold ([pos '()] [neg '()] [others '()])
([prop (in-list props)])
(match prop
[(TypeProp: o t)
(values (union-update pos o t) neg others)]
[(NotTypeProp: o t)
(values pos (intersect-update neg o t) others)]
[_ (values pos neg (cons prop others))])))
(let ([pos (for*/list ([p (in-mlist pos)]
[p (in-value (-is-type (mcar p) (mcdr p)))]
#:when (not (FalseProp? p)))
p)]
[neg (for*/list ([p (in-mlist neg)]
[p (in-value (-not-type (mcar p) (mcdr p)))]
#:when (not (FalseProp? p)))
p)])
(if (or (member -tt pos prop-equal?)
(member -tt neg prop-equal?))
(list -tt)
(append pos neg others))))
;; consolidate type info and separate out other props
(define others
(for/fold ([others '()])
([prop (in-list props)])
(match prop
[(TypeProp: o t1)
((if or? union-update! intersect-update!) tf-map t1 o)
others]
[(NotTypeProp: o t1)
((if or? intersect-update! union-update!) ntf-map t1 o)
others]
[_ (cons prop others)])))
;; convert consolidated types into props and gather everything
(define raw-results
(append (for/list ([(k v) (in-hash tf-map)])
(-is-type k v))
(for/list([(k v) (in-hash ntf-map)])
(-not-type k v))
others))
;; check for abort condition and remove trivial props
(if or?
(if (member -tt raw-results)
(list -tt)
(filter-not FalseProp? raw-results))
(if (member -ff raw-results)
(list -ff)
(filter-not TrueProp? raw-results)))]))
@ -214,31 +204,44 @@
;; 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))
(match ands
[(cons (AndProp: elems) ands)
(apply -and (for/list ([elem (in-list elems)])
(apply -or elem (append ands others))))]
[_ (make-OrProp others)]))
(let loop ([ps args] [result null])
(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)
(define results (mutable-set))
(for ([p (in-list ps)])
(match p
[(OrProp: ps*) (for ([p* (in-list ps*)])
(set-add! results p*))]
[p (set-add! results p)]))
(set->list results))
(let loop ([ps (flatten-ors/remove-duplicates args)]
[result null])
(match ps
[(cons p ps)
(match p
[(OrProp: ps*) (loop (append ps* ps) result)]
[(? FalseProp?) (loop ps result)]
[_
(let check-loop ([qs ps])
(match qs
[(cons q qs) (cond
[(complementary? p q) -tt]
[(implies-atomic? p q) (loop ps result)]
[else (check-loop qs)])]
[_ #:when (for/or ([q (in-list result)])
(implies-atomic? p q))
(loop ps result)]
[_ (loop ps (cons p result))]))])]
[_ (distribute (compact-or-props result))])))
[(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)]) (complementary? p cur)) -tt]
[(for/or ([p (in-list result)]) (complementary? p cur)) -tt]
;; don't include 'cur' if its covered by another prop
[(for/or ([p (in-list rst)]) (implies-atomic? cur p))
(loop rst result)]
[(for/or ([p (in-list result)]) (implies-atomic? 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?
@ -247,47 +250,52 @@
;; will be a conjunction of only atomic propositions and disjunctions
;; (i.e. a CNF proposition)
(define (-and . args)
(define-values (pos neg others)
(let loop ([args args]
[pos '()]
[neg '()]
[others '()])
(match args
[(cons arg args)
(match arg
[(TypeProp: o t) (loop args (intersect-update pos o t) neg others)]
[(NotTypeProp: o t) (loop args pos (union-update neg o t) others)]
[(AndProp: ps)
(let-values ([(pos neg others) (loop ps pos neg others)])
(loop args pos neg others))]
[_ (loop args pos neg (cons arg others))])]
[_ (values pos neg others)])))
;; Move all the type props up front as they are the stronger props
(let loop ([ps (append (for*/list ([p (in-mlist pos)]
[p (in-value (-is-type (mcar p) (mcdr p)))]
#:when (not (prop-equal? -tt p)))
p)
(for*/list ([p (in-mlist neg)]
[p (in-value (-not-type (mcar p) (mcdr p)))]
#:when (not (prop-equal? -tt p)))
p)
others)]
(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 (mutable-set))
(define nts (mutable-set))
(define ors (make-hash))
(define others (mutable-set))
(let partition! ([ps ps])
(for ([p (in-list ps)])
(match p
[(? TypeProp?) (set-add! ts p)]
[(? NotTypeProp?) (set-add! nts p)]
[(OrProp: ps*) (hash-update! ors (length ps*) (λ (l) (cons p l)) '())]
[(AndProp: ps*) (partition! ps*)]
[_ (set-add! others p)])))
(define ors-smallest-to-largest
(append-map cdr (sort (hash->list ors)
(λ (len/ors1 len/ors2)
(< (car len/ors1) (car len/ors2))))))
(append (set->list ts)
(set->list nts)
(set->list others)
ors-smallest-to-largest))
(let loop ([ps (flatten-ands/remove-duplicates/order args)]
[result null])
(match ps
[(cons p ps)
[(cons cur rst)
(cond
[(let check-loop ([qs ps])
(match qs
[(cons q qs) (cond
[(contradictory? p q) -ff]
[(implies-atomic? q p) (loop ps result)]
[else (check-loop qs)])]
[_ #f]))]
[(for/or ([q (in-list result)])
(implies-atomic? q p))
(loop ps result)]
[else (loop ps (cons p result))])]
[_ (make-AndProp result)])))
;; 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)]) (contradictory? p cur)) -ff]
[(for/or ([p (in-list result)]) (contradictory? 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)]) (implies-atomic? 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.
@ -297,14 +305,14 @@
[(tc-any-results: f) (tc-any-results (-and prop f))]
[(tc-results: ts (list (PropSet: ps+ ps-) ...) os)
(ret ts
(for/list ([f+ (in-list ps+)]
[f- (in-list ps-)])
(-PS (-and prop f+) (-and prop f-)))
(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 ([f+ ps+] [f- ps-])
(-PS (-and prop f+) (-and prop f-)))
(for/list ([p+ (in-list ps+)] [p- (in-list ps-)])
(-PS (-and prop p+) (-and prop p-)))
os
dty
dbound)]))
@ -345,4 +353,4 @@
(ret ts
empties
empties
dty dbound)]))
dty dbound)]))

View File

@ -12,7 +12,9 @@
(provide resolve-name resolve-app resolvable?
resolve-app-check-error
resolver-cache-remove!
current-check-polymorphic-recursion)
current-check-polymorphic-recursion
register-app-for-checking!
check-registered-apps!)
(provide/cond-contract
[resolve-once (Type? . -> . (or/c Type? #f))]
[resolve (Type? . -> . Type?)])
@ -38,6 +40,29 @@
(define already-resolving? (make-parameter #f))
;; list of (cons/c App? syntax?) of parsed Apps
;; during early phase of typechecking,
;; `check-registered-apps!` consumes these to verify
;; they are correct
(define apps-to-check (box '()))
;; registers an App for checking
;; used while parsing types initially,
;; once all definitions are loaded, we can verify
;; Apps are well formed (i.e. take the correct number of args, etc)
(define (register-app-for-checking! app stx)
(set-box! apps-to-check
(cons (cons app stx)
(unbox apps-to-check))))
;; checks apps registered with `register-app-for-checking!`
(define (check-registered-apps!)
(for* ([p (in-list (unbox apps-to-check))]
[(app stx) (in-pair p)])
(match app
[(App: (? Name? rator) rands)
(resolve-app-check-error rator rands stx)]))
(set-box! apps-to-check '()))
(define (resolve-app-check-error rator rands stx)
(parameterize ([current-orig-stx stx])
@ -54,7 +79,7 @@
(define poly-num (length (poly-vars (current-poly-struct))))
(if (= poly-num (length rands))
(when (not (or (ormap Error? rands)
(andmap type-equal? rands
(andmap equal? rands
(poly-vars (current-poly-struct)))))
(tc-error (~a "structure type constructor applied to non-regular arguments"
"\n type: " rator
@ -112,25 +137,27 @@
[var (in-list current-vars)])
(check-argument rand var))]
[_ (void)])]
[(Mu: _ _) (void)]
[(App: _ _ _) (void)]
[(Error:) (void)]
[(? Mu?) (void)]
[(? App?) (void)]
[(? Error?) (void)]
[_ (tc-error/delayed (~a "type cannot be applied"
"\n type: " rator
"\n arguments...: " rands))])))
(define (resolve-app rator rands stx)
(parameterize ([current-orig-stx stx]
(define (resolve-app rator rands [stx #f])
(parameterize ([current-orig-stx (or stx (current-orig-stx))]
[already-resolving? #t])
(resolve-app-check-error rator rands stx)
(match rator
[(? Name?)
(let ([r (resolve-name rator)])
(and r (resolve-app r rands stx)))]
[(Poly: _ _) (instantiate-poly rator rands)]
[(Mu: _ _) (resolve-app (unfold rator) rands stx)]
[(App: r r* s) (resolve-app (resolve-app r r* s) rands stx)]
[(? Poly?) (instantiate-poly rator rands)]
[(? Mu?) (resolve-app (unfold rator) rands stx)]
[(App: r r*) (resolve-app (resolve-app r r* (current-orig-stx))
rands
(current-orig-stx))]
[_ (tc-error (~a "cannot apply a non-polymorphic type"
"\n type: " rator
"\n arguments: " rands))])))
@ -145,7 +172,7 @@
(or r
(let ([r* (match t
[(Mu: _ _) (unfold t)]
[(App: r r* s) (resolve-app r r* s)]
[(App: r r*) (resolve-app r r* #f)]
[(? Name?) (resolve-name t)])])
(when (and r* (not (currently-subtyping?)))
(hash-set! resolver-cache t r*))

View File

@ -78,7 +78,7 @@
(λ (name)
(int-err "substitute used on ... variable ~a in type ~a" name target))]
[else (make-ListDots (sub dty) dbound)])]
[_ (Rep-fold sub target)])))
[_ (Rep-fmap target sub)])))
@ -137,7 +137,7 @@
(and rest (sub rest))
(and drest (cons (sub (car drest)) (cdr drest)))
(map sub kws))])]
[_ (Rep-fold sub target)])))
[_ (Rep-fmap target sub)])))
;; implements curly brace substitution from the formalism, with the addition
;; that a substitution can include fixed args in addition to a different dotted arg
@ -177,7 +177,7 @@
image-bound]
[else (cdr drest)])))
(map sub kws)))]
[_ (Rep-fold sub target)])))
[_ (Rep-fmap target sub)])))
;; substitute many variables
;; subst-all : substitution/c Type -> Type

View File

@ -1,9 +1,10 @@
#lang racket/base
(require "../utils/utils.rkt"
(utils hset)
(rep type-rep rep-utils type-mask)
(types abbrev union subtype resolve utils)
racket/match racket/set)
(types abbrev subtype resolve utils)
racket/match)
(provide subtract)
@ -16,15 +17,15 @@
(define result
(let sub ([t t])
(match t
[_ #:when (disjoint-masks? (Type-mask t) (Type-mask s)) t]
[_ #:when (disjoint-masks? (mask t) (mask s)) t]
[_ #:when (subtype t s) -Bottom]
[(or (App: _ _ _) (? Name?))
[(or (App: _ _) (? Name?))
;; must be different, since they're not subtypes
;; and n must refer to a distinct struct type
t]
[(Union: elems) (apply Un (map sub elems))]
[(Union: elems) (Union-map elems sub)]
[(Intersection: ts)
(apply -unsafe-intersect (set-map ts sub))]
(apply -unsafe-intersect (hset-map ts sub))]
[(? Mu?) (sub (unfold t))]
[(Poly: vs b) (make-Poly vs (sub b))]
[_ t])))

File diff suppressed because it is too large Load Diff

View File

@ -10,7 +10,7 @@
"../utils/utils.rkt"
(contract-req)
(rep type-rep)
(types utils union printer)
(types utils printer)
(typecheck possible-domains tc-metafunctions)
(utils tc-utils)
(for-template racket/base))

View File

@ -1,57 +1,55 @@
#lang racket/base
(require "../utils/utils.rkt"
(utils hset)
(rep type-rep rep-utils)
(prefix-in c: (contract-req))
(types subtype base-abbrev resolve current-seen)
racket/match
racket/list)
(provide normalize-type
Un
union)
(provide/cond-contract
[Un (() #:rest (c:listof Type?) . c:->* . Type?)])
;; t1 t2
;; But excludes duplicate info w.r.t. subtyping
;; can be useful in a few places, but avoid using
;; in hot code when Un (or similar) will suffice.
(define (union t1 t2)
(cond
[(subtype t1 t2) t2]
[(subtype t2 t1) t1]
[else (Un t1 t2)]))
;; a is a Type (not a union type)
;; b is a List[Type] (non overlapping, non Union-types)
;; The output is a non overlapping list of non Union types.
;; The overlapping constraint is lifted if we are in the midst of subtyping. This is because during
;; subtyping calls to subtype are expensive.
(define (merge a b)
(define b* (make-Union b))
(match* (a b)
;; If a union element is a Name application, then it should not
;; be checked for subtyping since that can cause infinite
;; loops if this is called during type instantiation.
[((App: (? Name? rator) rands stx) _)
;; However, we should check if it's a well-formed application
;; so that bad applications are rejected early.
(resolve-app-check-error rator rands stx)
(cons a b)]
[(_ _) #:when (currently-subtyping?) (cons a b)]
[((? (λ _ (subtype a b*))) _) b]
[((? (λ _ (subtype b* a))) _) (list a)]
[(_ _) (cons a (filter-not (λ (b-elem) (subtype b-elem a)) b))]))
;; t is a Type (not a union type)
;; b is a hset[Type] (non overlapping, non Union-types)
;; The output is a non overlapping hset of non Union types.
(define (merge t ts)
(let ([t (normalize-type t)])
(define t* (make-Union ts))
(cond
[(subtype t* t) (hset t)]
[(subtype t t*) ts]
[else (hset-add (hset-filter ts (λ (b-elem) (not (subtype b-elem t))))
t)])))
;; Type -> List[Type]
(define (flat t)
;; list[Type] -> hset[Type]
(define (flatten ts)
(for/fold ([s (hset)])
([t (in-hset ts)])
(match t
[(Union: ts) (hset-union s ts)]
[_ (hset-add s t)])))
;; Recursively reduce unions so that they do not contain
;; reduntant information w.r.t. subtyping. We used to maintain
;; this properly throughout typechecking, but this was costly.
;; Not we only do it as we are generating contracts, since we
;; don't want to do redundant runtime checks, etc.
(define (normalize-type t)
(match t
[(Union: es) es]
[_ (list t)]))
;; Union constructor
;; Normalizes representation by sorting types.
;; Type * -> Type
;; The input types can overlap and be union types
(define Un-cache (make-weak-hash))
(define Un
(case-lambda
[() -Bottom]
[(t) t]
[args
(cond [(hash-ref Un-cache args #f)]
[else
(define ts (foldr merge '()
(remove-duplicates (append-map flat args) type-equal?)))
(define type (make-Union ts))
(hash-set! Un-cache args type)
type])]))
[(Union: ts) (make-Union (for/fold ([ts (hset)])
([t (in-hset (flatten ts))])
(merge t ts)))]
[_ (Rep-fmap t normalize-type)]))

View File

@ -5,8 +5,8 @@
(contract-req)
(infer-in infer)
(rep core-rep type-rep prop-rep object-rep values-rep rep-utils)
(utils tc-utils)
(types resolve subtype subtract union)
(utils tc-utils hset)
(types resolve subtype subtract)
(rename-in (types abbrev)
[-> -->]
[->* -->*]
@ -82,11 +82,11 @@
(list (make-arr* doms (update rng rst))))]
[((Union: ts) _)
(apply Un (map (λ (t) (update t path)) ts))]
(Union-map ts (λ (t) (update t path)))]
[((Intersection: ts) _)
(for/fold ([t Univ])
([elem (in-list ts)])
([elem (in-hset ts)])
(intersect t (update elem path)))]
[(_ _)

View File

@ -0,0 +1,169 @@
#lang racket/base
(require "utils.rkt"
(contract-req)
racket/match
(for-syntax racket/base racket/match))
;; Lightweight variant of sets
(provide hset hseteq hseteqv
hset?
hset-empty?
hset-member?
hset-count
hset-add
hset-remove
hset-first
hsubset?
hset-overlap?
hset=?
hset-subtract
hset-union
hset-intersect
hset-partition
hset-map
hset-filter
hset-for-each
hset->list
list->hset
list->hseteq
for/hset
for/hseteq
for/hseteqv
for*/hset
for*/hseteq
in-hset)
(provide-for-cond-contract hsetof)
(define-for-cond-contract (hsetof c) (hash/c c #t #:immutable #t #:flat? #t))
(define build-hset
(case-lambda
[() #hash()]
[l (for/fold ([s #hash()]) ([e (in-list l)])
(hash-set s e #t))]))
(define hset
(case-lambda
[() #hash()]
[l (for/fold ([s #hash()]) ([e (in-list l)])
(hash-set s e #t))]))
(define hseteq
(case-lambda
[() #hasheq()]
[l (for/fold ([s #hasheq()]) ([e (in-list l)])
(hash-set s e #t))]))
(define (hseteqv)
(case-lambda
[() #hasheqv()]
[l (for/fold ([s #hasheqv()]) ([e (in-list l)])
(hash-set s e #t))]))
(define (hset? s) (hash? s))
(define (hset-empty? s) (zero? (hash-count s)))
(define (hset-member? s e) (hash-ref s e #f))
(define (hset-count s) (hash-count s))
(define (hset-add s e) (hash-set s e #t))
(define (hset-remove s e) (hash-remove s e))
(define (hset-first s) (hash-iterate-key s (hash-iterate-first s)))
(define-syntax in-hset (make-rename-transformer #'in-immutable-hash-keys))
(define (hsubset? s1 s2)
(hash-keys-subset? s1 s2))
(define (hset-overlap? s1 s2)
(if ((hset-count s1) . < . (hset-count s2))
(hset-overlap? s2 s1)
(for/or ([k (in-hset s2)])
(hset-member? s1 k))))
(define (hset=? s1 s2)
(or (eq? s1 s2)
(and (= (hash-count s1) (hash-count s2))
(hash-keys-subset? s1 s2))))
(define (hset-subtract s1 s2)
(for/fold ([s1 s1]) ([k (in-hset s2)])
(hash-remove s1 k)))
(define (hset-union s1 s2)
(if ((hset-count s1) . < . (hset-count s2))
(hset-union s2 s1)
(for/fold ([s1 s1]) ([k (in-hset s2)])
(hash-set s1 k #t))))
(define (hset-intersect s1 s2)
(if ((hset-count s1) . < . (hset-count s2))
(hset-union s2 s1)
(for/fold ([s s2]) ([k (in-hset s2)])
(if (hash-ref s1 k #f)
s
(hash-remove s k)))))
(define (hset-partition s pred empty-y-set empty-n-set)
(for/fold ([y empty-y-set] [n empty-n-set]) ([v (in-hset s)])
(if (pred v)
(values (hset-add y v) n)
(values y (hset-add n v)))))
(define (hset->list s) (hash-keys s))
(define (list->hset l)
(for/hset ([k (in-list l)])
k))
(define (list->hseteq l)
(for/hseteq ([k (in-list l)])
k))
(define (hset-map h f)
(for/fold ([result '()])
([x (in-hset h)])
(cons (f x) result)))
(define (hset-filter h f)
(for/fold ([result h])
([x (in-hset h)])
(if (f x)
result
(hset-remove result x))))
(define (hset-for-each h f)
(for ([x (in-hset h)]) (f x)))
(define-syntax-rule (for/hset bindings body ...)
(for/hash bindings (values
(let ()
body ...)
#t)))
(define-syntax-rule (for/hseteq bindings body ...)
(for/hasheq bindings (values
(let ()
body ...)
#t)))
(define-syntax-rule (for/hseteqv bindings body ...)
(for/hasheqv bindings (values
(let ()
body ...)
#t)))
(define-syntax-rule (for*/hset bindings body ...)
(for*/hash bindings (values
(let ()
body ...)
#t)))
(define-syntax-rule (for*/hseteq bindings body ...)
(for*/hasheq bindings (values
(let ()
body ...)
#t)))

View File

@ -191,8 +191,9 @@ don't depend on any other portion of the system
(define (tc-error/delayed msg #:stx [stx* (current-orig-stx)] . rest)
(let ([stx (locate-stx stx*)])
(unless (syntax? stx)
(int-err "erroneous syntax was not a syntax object: ~a ~a"
stx (syntax->datum stx*)))
(int-err "erroneous syntax was not a syntax object: ~a\n (error message: ~a)"
stx
msg))
(current-type-error? #t)
(if (delay-errors?)
(set! delayed-errors (cons (make-err (apply format msg rest)
@ -272,9 +273,10 @@ don't depend on any other portion of the system
(string-append
"Internal Typechecker Error: "
(apply format msg args)
(format "\nwhile typechecking:\n~a\noriginally:\n~a"
(syntax->datum (current-orig-stx))
(syntax->datum (locate-stx (current-orig-stx)))))
(let ([stx (current-orig-stx)])
(format "\nwhile typechecking:\n~a\noriginally:\n~a"
(and stx (syntax->datum stx))
(and stx (syntax->datum (locate-stx stx))))))
(current-continuation-marks))))
;; are we currently expanding in a typed module (or top-level form)?

View File

@ -22,6 +22,7 @@ at least theoretically.
list-extend
filter-multiple
syntax-length
in-pair
in-sequence-forever
match*/no-order
bind)
@ -272,3 +273,12 @@ at least theoretically.
(syntax-parser
[(_ x:id val:expr)
#'(app (λ (_) val) x)]))
(define-syntax (assert stx)
(syntax-case stx ()
[(_ expr)
#`(unless expr #,(quasisyntax/loc stx (error 'assert "failed!")))]))
(define-syntax-rule (in-pair p)
(in-parallel (in-value (car p)) (in-value (cdr p))))

View File

@ -5,8 +5,7 @@
(require pict
"racket/private/gui-types.rkt"
(for-syntax (only-in typed-racket/rep/type-rep
make-Name
make-Union)
make-Name)
(submod "racket/private/gui-types.rkt" #%type-decl)))
(begin-for-syntax
@ -19,7 +18,7 @@
(-inst (parse-type #'Color%)))
(define -pict (-struct-name #'pict))
(define -pict-path
(make-Union (list (-val #f) -pict (-lst -pict))))
(Un (-val #f) -pict (-lst -pict)))
(define -child (-struct-name #'child))
(define -text-style
(-mu -text-style

View File

@ -3,12 +3,12 @@
;; This module provides a typed version of racket/async-channel
(require racket/async-channel
(for-syntax (only-in (rep type-rep) make-Async-ChannelTop)))
(for-syntax (only-in (rep type-rep) -Async-ChannelTop)))
;; Section 11.2.4 (Buffered Asynchronous Channels)
(type-environment
[make-async-channel (-poly (a) (->opt [(-opt -PosInt)] (-async-channel a)))]
[async-channel? (make-pred-ty (make-Async-ChannelTop))]
[async-channel? (make-pred-ty -Async-ChannelTop)]
[async-channel-get (-poly (a) ((-async-channel a) . -> . a))]
[async-channel-try-get (-poly (a) ((-async-channel a) . -> . (-opt a)))]
[async-channel-put (-poly (a) ((-async-channel a) a . -> . -Void))]

View File

@ -7,7 +7,7 @@
(utils tc-utils)
(env init-envs)
(except-in (rep prop-rep object-rep type-rep) make-arr)
(rename-in (types abbrev union) [make-arr* make-arr])))
(rename-in (types abbrev) [make-arr* make-arr])))
(define-for-syntax unit-env
(make-env

View File

@ -1,5 +1,5 @@
#;
(exn-pred #rx"expected: \\(Listof Nothing\\).*given: \\(Listof Pos\\*\\)")
(exn-pred #rx"expected: \\Null.*given: \\(Listof Pos\\*\\)")
#lang typed/racket
(define-type Pos Integer)
(define-new-subtype Pos* (p Pos))

View File

@ -1,5 +1,5 @@
#;
(exn-pred #rx"expected: \\(Listof Nothing\\).*given: \\(Listof Pos\\*\\)")
(exn-pred #rx"expected: \\Null.*given: \\(Listof Pos\\*\\)")
#lang typed/racket
(define-type Pos Integer)
(define-new-subtype Pos* (p Pos))

View File

@ -1,7 +1,6 @@
#lang racket
(require typed-racket/infer/infer
typed-racket/types/union
typed-racket/types/prop-ops
typed-racket/types/abbrev
typed-racket/rep/type-rep

View File

@ -3,7 +3,7 @@
(require "test-utils.rkt"
rackunit racket/list racket/match racket/format
syntax/srcloc syntax/location
(types abbrev union tc-result)
(types abbrev tc-result)
(utils tc-utils)
(rep prop-rep object-rep type-rep)
(typecheck check-below)

View File

@ -25,7 +25,7 @@
define lambda λ case-lambda)
(prefix-in tr: (only-in (base-env prims) define lambda λ case-lambda))
(for-syntax (rep type-rep prop-rep object-rep)
(rename-in (types abbrev union numeric-tower prop-ops utils)
(rename-in (types abbrev numeric-tower prop-ops utils)
[Un t:Un]
[-> t:->])))
@ -1485,7 +1485,7 @@
(init-rest [rst : (List Symbol)])))
(make-object c% "wrong"))
#:ret (tc-ret (make-Instance (make-Class #f null null null null (-Tuple (list -Symbol)))))
#:msg #rx"expected: \\(List Symbol.*given: \\(List String"]
#:msg #rx"expected: Symbol.*given: String"]
;; PR 14408, test init-field order
[tc-e (let ()
(define c%

View File

@ -6,7 +6,7 @@
(for-template racket/base)
(private type-contract)
(rep type-rep values-rep)
(types abbrev numeric-tower union)
(types abbrev numeric-tower)
(static-contracts combinators optimize)
(submod typed-racket/private/type-contract numeric-contracts)
(submod typed-racket/private/type-contract test-exports)
@ -20,7 +20,7 @@
(define-syntax-rule (t e)
(test-case (format "~a" 'e)
(let ((v e))
(let ([v e])
(with-check-info (('type v))
(type->contract
e
@ -128,262 +128,263 @@
(fun-val ctced-val))))))]))
(define tests
(test-suite "Contract Tests"
(t (-Number . -> . -Number))
(t (-Promise -Number))
(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 (-struct #'struct-name1 #f (list (make-fld -Symbol #'acc #f))))
;; Adapted from PR 13815
(t (-poly (a) (-> a a)))
(t (-poly (a) (-mu X (-> a X))))
(t (-poly (a) (-poly (b) (-> a a))))
(t (-poly (a) (-App (-poly (b) (-> a a)) (list -Number) #'#f)))
(test-suite
"Contract Tests"
(t (-Number . -> . -Number))
(t (-Promise -Number))
(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 (-struct #'struct-name1 #f (list (make-fld -Symbol #'acc #f))))
;; Adapted from PR 13815
(t (-poly (a) (-> a a)))
(t (-poly (a) (-mu X (-> a X))))
(t (-poly (a) (-poly (b) (-> a a))))
(t (-poly (a) (-App (-poly (b) (-> a a)) (list -Number))))
(t (-poly (a) -Flonum))
(t (-poly (a) (-set -Number)))
(t (-poly (a) (-lst a)))
(t (-poly (a) (-vec a)))
(t (-> (-poly (A B) (-> (Un A (-mu X (Un A (-lst X)))) (Un A (-mu X (Un A (-lst X))))))
(-> -Symbol (-mu X (Un -Symbol (-lst X))))))
(t (-poly (a) -Flonum))
(t (-poly (a) (-set -Number)))
(t (-poly (a) (-lst a)))
(t (-poly (a) (-vec a)))
(t (-> (-poly (A B) (-> (Un A (-mu X (Un A (-lst X)))) (Un A (-mu X (Un A (-lst X))))))
(-> -Symbol (-mu X (Un -Symbol (-lst X))))))
(t (-polydots (a) -Symbol))
(t (-polydots (a) (->... (list) (a a) -Symbol)))
(t (-polydots (a) -Symbol))
(t (-polydots (a) (->... (list) (a a) -Symbol)))
(t (-polyrow (a) (list null null null null) -Symbol))
(t (-polyrow (a) (list null null null null)
(-> (-class #:row (-v a)) (-class #:row (-v a)))))
(t (-polyrow (a) (list null null null null) -Symbol))
(t (-polyrow (a) (list null null null null)
(-> (-class #:row (-v a)) (-class #:row (-v a)))))
(t (-mu x (-Syntax x)))
(t (-> (-> Univ -Bottom : -ff-propset) -Bottom : -ff-propset))
(t (-poly (A B) (-> A B (Un A B))))
(t (-mu x (-Syntax x)))
(t (-> (-> Univ -Bottom : -ff-propset) -Bottom : -ff-propset))
(t (-poly (A B) (-> A B (Un A B))))
(t/fail ((-poly (a) (-vec a)) . -> . -Symbol)
"cannot generate contract for non-function polymorphic type")
(t/fail (-> (-poly (a b) (-> (Un a b) (Un a b))) Univ)
"multiple parametric contracts are not supported")
(t/fail
(-> (-poly (A B) (-> (Un B (-mu X (Un A (-lst X)))) (Un B (-mu X (Un A (-lst X))))))
(-> -Symbol (-mu X (Un -Symbol (-lst X)))))
"multiple parametric contracts are not supported")
(t/fail (-> (-polydots (a) (->... (list) (a a) -Symbol)) Univ)
"cannot generate contract for variable arity polymorphic type")
(t/fail ((-poly (a) (-vec a)) . -> . -Symbol)
"cannot generate contract for non-function polymorphic type")
(t/fail (-> (-poly (a b) (-> (Un a b) (Un a b))) Univ)
"multiple parametric contracts are not supported")
(t/fail
(-> (-poly (A B) (-> (Un B (-mu X (Un A (-lst X)))) (Un B (-mu X (Un A (-lst X))))))
(-> -Symbol (-mu X (Un -Symbol (-lst X)))))
"multiple parametric contracts are not supported")
(t/fail (-> (-polydots (a) (->... (list) (a a) -Symbol)) Univ)
"cannot generate contract for variable arity polymorphic type")
;; PR 14894 - FIXME: the polydots case may be possible for typed functions
(t/fail (-polydots (a) (->... (list) (a a) (make-ValuesDots null a 'a)))
"dotted return values")
(t/fail (-> ManyUniv)
"unknown return values")
;; PR 14894 - FIXME: the polydots case may be possible for typed functions
(t/fail (-polydots (a) (->... (list) (a a) (make-ValuesDots null a 'a)))
"dotted return values")
(t/fail (-> ManyUniv)
"unknown return values")
;; 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/fail (cl->* (-> -String ManyUniv) (-> -String Univ ManyUniv))
"unknown return values")
;; 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/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)))))
"case function type with optional keyword arguments")
(t/fail (-> (make-pred-ty -Symbol)-Symbol)
"function type with props or objects")
(t/fail (cl->*
(-> -Boolean -Boolean)
(-> -Symbol -Symbol))
"two cases of arity 1")
(t/fail (-struct #'struct-name2 #f (list (make-fld -Symbol #'acc #f)) (-> -Symbol))
"procedural structs are not supported")
(t/fail (-Syntax (-> -Boolean -Boolean))
"required a flat contract but generated a chaperone contract")
(t/fail (-Syntax (-seq -Boolean))
"required a flat contract but generated an impersonator contract")
(t/fail (-set (-seq -Boolean))
"required a chaperone contract but generated an impersonator contract")
(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)))))
"case function type with optional keyword arguments")
(t/fail (-> (make-pred-ty -Symbol)-Symbol)
"function type with props or objects")
(t/fail (cl->*
(-> -Boolean -Boolean)
(-> -Symbol -Symbol))
"two cases of arity 1")
(t/fail (-struct #'struct-name2 #f (list (make-fld -Symbol #'acc #f)) (-> -Symbol))
"procedural structs are not supported")
(t/fail (-Syntax (-> -Boolean -Boolean))
"required a flat contract but generated a chaperone contract")
(t/fail (-Syntax (-seq -Boolean))
"required a flat contract but generated an impersonator contract")
(t/fail (-set (-seq -Boolean))
"required a chaperone contract but generated an impersonator contract")
(t/fail
(make-Function
(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)))))
"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")
(t/fail
(make-Function
(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)))))
"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")
(t-sc -Number number/sc)
(t-sc -Integer integer/sc)
(t-sc (-lst Univ) (listof/sc any-wrap/sc))
(t-sc (Un (-lst Univ) -Number) (or/sc number/sc (listof/sc any-wrap/sc)))
(t-sc -Number number/sc)
(t-sc -Integer integer/sc)
(t-sc (-lst Univ) (listof/sc any-wrap/sc))
(t-sc (Un (-lst Univ) -Number) (or/sc number/sc (listof/sc any-wrap/sc)))
;; Github pull request #226
(let ([ctc (-> Univ -Boolean)])
;; Ordinary functions should have a contract
(t-int ctc
(lambda (f) (f 6))
(lambda (x) #t)
#:untyped)
(t-int/fail ctc
(lambda (f) (f 6))
(lambda (x) 'bad)
#:untyped
#:msg #rx"promised: boolean\\?.*produced: 'bad.*blaming: untyped")
;; Struct predicates should not have a contract
(t-int ctc
(lambda (foo?)
(when (has-contract? foo?)
(error "Regression failed for PR #266: struct predicate has a contract"))
(foo? foo?))
(let-values ([(_t _c foo? _a _m) (make-struct-type 'foo #f 0 0)])
foo?)
#:untyped)
;; Unless the struct predicate is guarded by an untyped chaperone
(t-int/fail ctc
(lambda (foo?) (foo? string-append))
(let-values ([(_t _c foo? _a _m) (make-struct-type 'foo #f 0 0)])
(chaperone-procedure foo? (lambda (x) (x 0) x)))
#:untyped
#:msg #rx"broke its own contract")
;; Typed chaperones are okay, though
(t-int ctc
(lambda (foo?)
(when (has-contract? foo?)
(error "Regression failed for PR #266: typed chaperone has a contract"))
(foo? foo?))
(let-values ([(_t _c foo? _a _m) (make-struct-type 'foo #f 0 0)])
(chaperone-procedure foo? #f))
#:typed))
;; Github pull request #226
(let ([ctc (-> Univ -Boolean)])
;; Ordinary functions should have a contract
(t-int ctc
(lambda (f) (f 6))
(lambda (x) #t)
#:untyped)
(t-int/fail ctc
(lambda (f) (f 6))
(lambda (x) 'bad)
#:untyped
#:msg #rx"promised: boolean\\?.*produced: 'bad.*blaming: untyped")
;; Struct predicates should not have a contract
(t-int ctc
(lambda (foo?)
(when (has-contract? foo?)
(error "Regression failed for PR #266: struct predicate has a contract"))
(foo? foo?))
(let-values ([(_t _c foo? _a _m) (make-struct-type 'foo #f 0 0)])
foo?)
#:untyped)
;; Unless the struct predicate is guarded by an untyped chaperone
(t-int/fail ctc
(lambda (foo?) (foo? string-append))
(let-values ([(_t _c foo? _a _m) (make-struct-type 'foo #f 0 0)])
(chaperone-procedure foo? (lambda (x) (x 0) x)))
#:untyped
#:msg #rx"broke its own contract")
;; Typed chaperones are okay, though
(t-int ctc
(lambda (foo?)
(when (has-contract? foo?)
(error "Regression failed for PR #266: typed chaperone has a contract"))
(foo? foo?))
(let-values ([(_t _c foo? _a _m) (make-struct-type 'foo #f 0 0)])
(chaperone-procedure foo? #f))
#:typed))
;; classes
(t-sc (-class) (class/sc #f null null))
(t-sc (-class #:init ([x -Number #f] [y -Number #f]))
(class/sc #f
(list (member-spec 'init 'x number/sc)
(member-spec 'init 'y number/sc))
null))
(t-sc (-class #:init ([x -Number #f] [y -Number #t]))
(class/sc #f
(list (member-spec 'init 'x number/sc)
(member-spec 'init 'y number/sc))
null))
(t-sc (-class #:init ([x -Number #f]) #:init-field ([y -Integer #f]))
(class/sc #f
(list (member-spec 'init 'x number/sc)
(member-spec 'init 'y integer/sc)
(member-spec 'field 'y integer/sc))
null))
(t (-class #:method ([m (-poly (x) (-> x x))])))
(t (-class #:method ([m (-polydots (x) (->... (list) (x x) -Void))])))
(t (-class #:method ([m (-polyrow (x) (list null null null null)
(-> (-class #:row (-v x)) -Void))])))
;; classes
(t-sc (-class) (class/sc #f null null))
(t-sc (-class #:init ([x -Number #f] [y -Number #f]))
(class/sc #f
(list (member-spec 'init 'x number/sc)
(member-spec 'init 'y number/sc))
null))
(t-sc (-class #:init ([x -Number #f] [y -Number #t]))
(class/sc #f
(list (member-spec 'init 'x number/sc)
(member-spec 'init 'y number/sc))
null))
(t-sc (-class #:init ([x -Number #f]) #:init-field ([y -Integer #f]))
(class/sc #f
(list (member-spec 'init 'x number/sc)
(member-spec 'init 'y integer/sc)
(member-spec 'field 'y integer/sc))
null))
(t (-class #:method ([m (-poly (x) (-> x x))])))
(t (-class #:method ([m (-polydots (x) (->... (list) (x x) -Void))])))
(t (-class #:method ([m (-polyrow (x) (list null null null null)
(-> (-class #:row (-v x)) -Void))])))
;; units
;; These tests do not have sufficient coverage because more
;; coverage requires a proper set up of the signature environment.
;; Further coverage of unit contract compilations occurs in
;; integration tests.
(t-sc (-unit null null null (-values (list -Integer)))
(unit/sc null null null (list integer/sc)))
(t-sc (-unit null null null (-values (list -Integer -Number)))
(unit/sc null null null (list integer/sc number/sc)))
(t-sc (-unit null null null (-values (list)))
(unit/sc null null null null))
;; units
;; These tests do not have sufficient coverage because more
;; coverage requires a proper set up of the signature environment.
;; Further coverage of unit contract compilations occurs in
;; integration tests.
(t-sc (-unit null null null (-values (list -Integer)))
(unit/sc null null null (list integer/sc)))
(t-sc (-unit null null null (-values (list -Integer -Number)))
(unit/sc null null null (list integer/sc number/sc)))
(t-sc (-unit null null null (-values (list)))
(unit/sc null null null null))
;; typed/untyped interaction tests
(t-int (-poly (a) (-> a a))
(λ (f) (f 1))
(λ (x) 1)
#:typed)
(t-int/fail (-poly (a) (-> a a))
(λ (f) (f 1))
(λ (x) 1)
#:untyped
#:msg #rx"produced: 1.*blaming: untyped")
(t-int (cl->* (->* '() -String -String)
(->* (list -Symbol) -Symbol -Symbol))
(λ (f) (f "a" "b"))
(case-lambda [xs (car xs)]
[(sym . xs) sym]))
(t-int (make-Evt -String)
(λ (x) (channel-get x))
(let ([ch (make-channel)])
(thread (λ () (channel-put ch "ok")))
ch)
#:untyped)
(t-int/fail (make-Evt -String)
(λ (x) (channel-get x))
(let ([ch (make-channel)])
(thread (λ () (channel-put ch 'bad)))
ch)
#:untyped
#:msg #rx"promised: String.*produced: 'bad")
(t-int/fail (make-Evt (-> -String -String))
(λ (x) ((sync x) 'bad))
(let ([ch (make-channel)])
(thread
(λ ()
(channel-put ch (λ (x) (string-append x "x")))))
ch)
#:typed
#:msg #rx"expected: String.*given: 'bad")
(t-int/fail (make-Evt -String)
(λ (x) (channel-put x "bad"))
(make-channel)
#:untyped
#:msg #rx"cannot put on a channel")
;; typed/untyped interaction with class/object contracts
(t-int/fail (-object #:method ([m (-> -String)]))
(λ (o) (send o n))
(new (class object% (super-new)
(define/public (m) "m")
(define/public (n) "n")))
#:typed
#:msg #rx"cannot call uncontracted")
(t-int (-class #:method ([m (-> -String)]))
(λ (s%) (class s% (super-new)
(define/public (n) "ok")))
(class object% (super-new)
(define/public (m) "m"))
#:untyped)
;; typed/untyped interaction tests
(t-int (-poly (a) (-> a a))
(λ (f) (f 1))
(λ (x) 1)
#:typed)
(t-int/fail (-poly (a) (-> a a))
(λ (f) (f 1))
(λ (x) 1)
#:untyped
#:msg #rx"produced: 1.*blaming: untyped")
(t-int (cl->* (->* '() -String -String)
(->* (list -Symbol) -Symbol -Symbol))
(λ (f) (f "a" "b"))
(case-lambda [xs (car xs)]
[(sym . xs) sym]))
(t-int (make-Evt -String)
(λ (x) (channel-get x))
(let ([ch (make-channel)])
(thread (λ () (channel-put ch "ok")))
ch)
#:untyped)
(t-int/fail (make-Evt -String)
(λ (x) (channel-get x))
(let ([ch (make-channel)])
(thread (λ () (channel-put ch 'bad)))
ch)
#:untyped
#:msg #rx"promised: String.*produced: 'bad")
(t-int/fail (make-Evt (-> -String -String))
(λ (x) ((sync x) 'bad))
(let ([ch (make-channel)])
(thread
(λ ()
(channel-put ch (λ (x) (string-append x "x")))))
ch)
#:typed
#:msg #rx"expected: String.*given: 'bad")
(t-int/fail (make-Evt -String)
(λ (x) (channel-put x "bad"))
(make-channel)
#:untyped
#:msg #rx"cannot put on a channel")
;; typed/untyped interaction with class/object contracts
(t-int/fail (-object #:method ([m (-> -String)]))
(λ (o) (send o n))
(new (class object% (super-new)
(define/public (m) "m")
(define/public (n) "n")))
#:typed
#:msg #rx"cannot call uncontracted")
(t-int (-class #:method ([m (-> -String)]))
(λ (s%) (class s% (super-new)
(define/public (n) "ok")))
(class object% (super-new)
(define/public (m) "m"))
#:untyped)
;; Github issue #368
(t-int/fail (-> -Integer -Integer)
values
3
#:untyped
#:msg #rx"promised: a procedure")
(t-int/fail (-> -Integer -Integer)
values
(λ () 3)
#:untyped
#:msg #rx"that accepts 1 non-keyword")
;; Github issue #368
(t-int/fail (-> -Integer -Integer)
values
3
#:untyped
#:msg #rx"promised: a procedure")
(t-int/fail (-> -Integer -Integer)
values
(λ () 3)
#:untyped
#:msg #rx"that accepts 1 non-keyword")
;; Value types with numbers shouldn't be checked with =
(t-int/fail (make-Value 3.0)
values
3
#:untyped
#:msg #rx"promised: 3.0")
(t-int/fail (make-Value 3)
values
3.0
#:untyped
#:msg #rx"promised: 3")
;; Value types with numbers shouldn't be checked with =
(t-int/fail (make-Value 3.0)
values
3
#:untyped
#:msg #rx"promised: 3.0")
(t-int/fail (make-Value 3)
values
3.0
#:untyped
#:msg #rx"promised: 3")
;; intersection types
(t (-unsafe-intersect (-seq -Symbol) (-pair -Symbol (-lst -Symbol))))
(t/fail (-unsafe-intersect (-Number . -> . -Number) (-String . -> . -String))
"more than 1 non-flat contract")
(t/fail (-unsafe-intersect (-box -Symbol) (-box Univ))
"more than 1 non-flat contract")
))
;; intersection types
(t (-unsafe-intersect (-seq -Symbol) (-pair -Symbol (-lst -Symbol))))
(t/fail (-unsafe-intersect (-Number . -> . -Number) (-String . -> . -String))
"more than 1 non-flat contract")
(t/fail (-unsafe-intersect (-box -Symbol) (-box Univ))
"more than 1 non-flat contract")
))

View File

@ -4,7 +4,7 @@
racket/format
rackunit
(rep rep-utils core-rep type-rep)
(types generalize abbrev union)
(types generalize abbrev)
(for-syntax racket/base syntax/parse))
(provide tests)
@ -18,7 +18,7 @@
(define expected exp*)
(with-check-info (['actual actual]
['expected expected])
(unless (type-equal? actual expected)
(unless (equal? actual expected)
(fail-check "Didn't generalize to expected type."))))]))

View File

@ -5,20 +5,14 @@
racket/list
(for-syntax racket/base syntax/parse)
syntax/location syntax/srcloc
(rep type-rep)
(rep rep-utils type-rep free-variance values-rep)
(r:infer infer promote-demote)
(types union substitute numeric-tower utils abbrev))
(types substitute numeric-tower utils abbrev))
(provide tests)
(gen-test-main)
(define-syntax-rule (fv-t ty elems ...)
(let ([ty* ty])
(test-check (format "~a" 'ty)
equal?
(fv ty*)
(list (quote elems) ...))))
(begin-for-syntax
(define-splicing-syntax-class result
@ -35,6 +29,109 @@
(pattern #:pass #:with pass #'#t)
(pattern #:fail #:with pass #'#f)))
(define N -Number)
(define B -Boolean)
(define-syntax-rule (fv-t ty [elems variances] ...)
(let ([ty* ty])
(test-check
(format "~a" 'ty)
equal?
(free-vars-hash (free-vars* ty*))
(make-immutable-hasheq (list (cons (quote elems) variances) ...)))))
(define-syntax-rule (fi-t ty [elems variances] ...)
(let ([ty* ty])
(test-check
(format "~a" 'ty)
equal?
(free-vars-hash (free-idxs* ty*))
(make-immutable-hasheq (list (cons (quote elems) variances) ...)))))
(define fv-tests
(test-suite
"Tests for fv"
[fv-t N]
[fv-t (-v a) [a variance:co]]
[fv-t (-pair (-v a) (-v b)) [a variance:co] [b variance:co]]
[fv-t (-pair (-HT (-v a) (-v b)) (-v c)) [a variance:inv] [b variance:inv] [c variance:co]]
[fv-t (-poly (a) a)]
[fv-t (-poly (a) (-v b)) [b variance:co]]
[fv-t (-poly (a b c d e) a)]
[fv-t (-poly (b) (-v a)) [a variance:co]]
[fv-t (-poly (b c d e) (-v a)) [a variance:co]]
[fv-t (-mu a (-lst a))]
[fv-t (-mu a (-lst (-pair a (-v b)))) [b variance:co]]
[fv-t (-vec (-lst (-v a))) [a variance:inv]]
[fv-t (->* null (-v a) N) [a variance:contra]]
))
(define fi-tests
(test-suite
"Test suite for fi"
[fi-t (make-ValuesDots null (-v a) 'a) [a variance:co]]
[fi-t (->... (list) ((-v a) (-v a)) (make-ValuesDots null (-v a) 'a))
[a variance:co]]))
(define-syntax (pd-t stx)
(syntax-parse stx
([_ S:expr (vars:id ...) D:expr P:expr]
(quasisyntax/loc stx
(test-case (format "~a => ~a < ~a < ~a" '(vars ...) 'D 'S 'P)
(define S-v S)
(define promoted (var-promote S-v '(vars ...)))
(define demoted (var-demote S-v '(vars ...)))
#,(syntax/loc stx
(check-equal? promoted P "Promoted value doesn't match expected."))
#,(syntax/loc stx
(check-equal? demoted D "Demoted value doesn't match expected.")))))))
(define pd-tests
(test-suite
"Tests for var-promote/var-demote"
(pd-t Univ () Univ Univ)
(pd-t (-v a) () (-v a) (-v a))
(pd-t (-v a) (a) -Bottom Univ)
(pd-t (-v a) (b) (-v a) (-v a))
(pd-t (-vec (-v a)) (a) (-vec -Bottom) (-vec Univ))
(pd-t (-vec (-lst (-v a))) (a) (-vec -Bottom) (-vec Univ))
(pd-t (-vec (-v a)) (b) (-vec (-v a)) (-vec (-v a)))
(pd-t (-box (-v a)) (a) (-box -Bottom) (-box Univ))
(pd-t (-box (-lst (-v a))) (a) (-box -Bottom) (-box Univ))
(pd-t (-box (-v a)) (b) (-box (-v a)) (-box (-v a)))
(pd-t (-channel (-v a)) (a) (-channel -Bottom) (-channel Univ))
(pd-t (-channel (-lst (-v a))) (a) (-channel -Bottom) (-channel Univ))
(pd-t (-channel (-v a)) (b) (-channel (-v a)) (-channel (-v a)))
(pd-t (-thread-cell (-v a)) (a) (-thread-cell -Bottom) (-thread-cell Univ))
(pd-t (-thread-cell (-lst (-v a))) (a) (-thread-cell -Bottom) (-thread-cell Univ))
(pd-t (-thread-cell (-v a)) (b) (-thread-cell (-v a)) (-thread-cell (-v a)))
(pd-t (-HT (-v a) (-v a)) (a) (-HT -Bottom -Bottom) (-HT Univ Univ))
(pd-t (-HT (-lst (-v a)) (-lst (-v a))) (a) (-HT -Bottom -Bottom) (-HT Univ Univ))
(pd-t (-HT (-v a) (-v a)) (b) (-HT (-v a) (-v a)) (-HT (-v a) (-v a)))
(pd-t (-Param (-v a) (-v b)) (a b) (-Param Univ -Bottom) (-Param -Bottom Univ))
(pd-t (-Param (-lst (-v a)) (-lst (-v b))) (a b)
(-Param (-lst Univ) (-lst -Bottom))
(-Param (-lst -Bottom) (-lst Univ)))
(pd-t (->* (list (-lst (-v a))) (-lst (-v a)) (-lst (-v a))) (a)
(->* (list (-lst Univ)) (-lst Univ) (-lst -Bottom))
(->* (list (-lst -Bottom)) (-lst -Bottom) (-lst Univ)))
(pd-t (->key #:a (-lst (-v a)) #t #:b (-lst (-v a)) #f -Symbol) (a)
(->key #:a (-lst Univ) #t #:b (-lst Univ) #f -Symbol)
(->key #:a (-lst -Bottom) #t #:b (-lst -Bottom) #f -Symbol))
(pd-t (->... (list) ((-lst (-v a)) b) -Symbol) (a)
(->... (list) ((-lst Univ) b) -Symbol)
(->... (list) ((-lst -Bottom) b) -Symbol))))
(define-syntax (infer-t stx)
(syntax-parse stx
([_ S:expr T:expr . rest]
@ -77,222 +174,149 @@
(define-syntax-rule (i2-f t1 t2)
(infer-t t2 t1 #:vars (fv t2) #:fail))
(define N -Number)
(define B -Boolean)
(define-syntax (pd-t stx)
(syntax-parse stx
([_ S:expr (vars:id ...) D:expr P:expr]
(quasisyntax/loc stx
(test-case (format "~a => ~a < ~a < ~a" '(vars ...) 'D 'S 'P)
(define S-v S)
(define promoted (var-promote S-v '(vars ...)))
(define demoted (var-demote S-v '(vars ...)))
#,(syntax/loc stx
(check-equal? promoted P "Promoted value doesn't match expected."))
#,(syntax/loc stx
(check-equal? demoted D "Demoted value doesn't match expected.")))))))
(define fv-tests
(test-suite "Tests for fv"
(fv-t -Number)
[fv-t (-v a) a]
[fv-t (-poly (a) a)]
[fv-t (-poly (a b c d e) a)]
[fv-t (-poly (b) (-v a)) a]
[fv-t (-poly (b c d e) (-v a)) a]
[fv-t (-mu a (-lst a))]
[fv-t (-mu a (-lst (-pair a (-v b)))) b]
[fv-t (->* null (-v a) -Number) a] ;; check that a is CONTRAVARIANT
))
(define pd-tests
(test-suite "Tests for var-promote/var-demote"
(pd-t Univ () Univ Univ)
(pd-t (-v a) () (-v a) (-v a))
(pd-t (-v a) (a) -Bottom Univ)
(pd-t (-v a) (b) (-v a) (-v a))
(pd-t (-vec (-v a)) (a) (-vec -Bottom) (-vec Univ))
(pd-t (-vec (-lst (-v a))) (a) (-vec -Bottom) (-vec Univ))
(pd-t (-vec (-v a)) (b) (-vec (-v a)) (-vec (-v a)))
(pd-t (-box (-v a)) (a) (-box -Bottom) (-box Univ))
(pd-t (-box (-lst (-v a))) (a) (-box -Bottom) (-box Univ))
(pd-t (-box (-v a)) (b) (-box (-v a)) (-box (-v a)))
(pd-t (-channel (-v a)) (a) (-channel -Bottom) (-channel Univ))
(pd-t (-channel (-lst (-v a))) (a) (-channel -Bottom) (-channel Univ))
(pd-t (-channel (-v a)) (b) (-channel (-v a)) (-channel (-v a)))
(pd-t (-thread-cell (-v a)) (a) (-thread-cell -Bottom) (-thread-cell Univ))
(pd-t (-thread-cell (-lst (-v a))) (a) (-thread-cell -Bottom) (-thread-cell Univ))
(pd-t (-thread-cell (-v a)) (b) (-thread-cell (-v a)) (-thread-cell (-v a)))
(pd-t (-HT (-v a) (-v a)) (a) (-HT -Bottom -Bottom) (-HT Univ Univ))
(pd-t (-HT (-lst (-v a)) (-lst (-v a))) (a) (-HT -Bottom -Bottom) (-HT Univ Univ))
(pd-t (-HT (-v a) (-v a)) (b) (-HT (-v a) (-v a)) (-HT (-v a) (-v a)))
(pd-t (-Param (-v a) (-v b)) (a b) (-Param Univ -Bottom) (-Param -Bottom Univ))
(pd-t (-Param (-lst (-v a)) (-lst (-v b))) (a b)
(-Param (-lst Univ) (-lst -Bottom))
(-Param (-lst -Bottom) (-lst Univ)))
(pd-t (->* (list (-lst (-v a))) (-lst (-v a)) (-lst (-v a))) (a)
(->* (list (-lst Univ)) (-lst Univ) (-lst -Bottom))
(->* (list (-lst -Bottom)) (-lst -Bottom) (-lst Univ)))
(pd-t (->key #:a (-lst (-v a)) #t #:b (-lst (-v a)) #f -Symbol) (a)
(->key #:a (-lst Univ) #t #:b (-lst Univ) #f -Symbol)
(->key #:a (-lst -Bottom) #t #:b (-lst -Bottom) #f -Symbol))
(pd-t (->... (list) ((-lst (-v a)) b) -Symbol) (a)
(->... (list) ((-lst Univ) b) -Symbol)
(->... (list) ((-lst -Bottom) b) -Symbol))
))
(define infer-tests
(test-suite "Tests for infer"
(infer-t Univ Univ)
(infer-t (-v a) Univ)
(infer-t (-v a) (-v a) #:result [(-v a) (-v a)])
(infer-t Univ (-v a) #:fail)
(infer-t Univ (-v a) #:vars '(a))
(infer-t (-v a) Univ #:vars '(a))
(infer-t (-v a) -Bottom #:vars '(a))
(infer-t (-v a) (-v b) #:fail)
(infer-t (-v a) (-v b) #:vars '(a))
(infer-t (-v a) (-v b) #:vars '(b))
(test-suite
"Tests for infer"
(infer-t Univ Univ)
(infer-t (-v a) Univ)
(infer-t (-v a) (-v a) #:result [(-v a) (-v a)])
(infer-t Univ (-v a) #:fail)
(infer-t Univ (-v a) #:vars '(a))
(infer-t (-v a) Univ #:vars '(a))
(infer-t (-v a) -Bottom #:vars '(a))
(infer-t (-v a) (-v b) #:fail)
(infer-t (-v a) (-v b) #:vars '(a))
(infer-t (-v a) (-v b) #:vars '(b))
(infer-t (make-ListDots -Symbol 'b) (-lst -Symbol) #:indices '(b)
#:result [(make-ListDots (-v b) 'b) -Null])
(infer-t (make-ListDots (-v a) 'b) (-lst -Symbol) #:vars '(a) #:indices '(b)
#:result [(-lst* (make-ListDots (-v b) 'b) (-v a))
(-lst* (-lst -Bottom) -Bottom)])
(infer-t (make-ListDots (-v b) 'b) (-lst -Symbol) #:indices '(b)
#:result [(make-ListDots (-v b) 'b) (-lst -Bottom)])
(infer-t (make-ListDots -Symbol 'b) (-lst -Symbol) #:indices '(b)
#:result [(make-ListDots (-v b) 'b) -Null])
(infer-t (make-ListDots (-v a) 'b) (-lst -Symbol) #:vars '(a) #:indices '(b)
#:result [(-lst* (make-ListDots (-v b) 'b) (-v a))
(-lst* (-lst -Bottom) -Bottom)])
(infer-t (make-ListDots (-v b) 'b) (-lst -Symbol) #:indices '(b)
#:result [(make-ListDots (-v b) 'b) (-lst -Bottom)])
(infer-t (-lst -Symbol) (make-ListDots -Symbol 'b) #:indices '(b)
#:result [(make-ListDots (-v b) 'b) (-lst -Bottom)])
(infer-t (-lst -Symbol) (make-ListDots (-v b) 'b) #:indices '(b)
#:result [(make-ListDots (-v b) 'b) (-lst -Symbol)])
(infer-t (make-ListDots (-v b) 'b) (-lst Univ) #:indices '(b))
(infer-t (make-ListDots (-v a) 'a) (-lst Univ))
(infer-t (make-ListDots (-lst (-v a)) 'a) (-lst (-lst Univ)))
(infer-t (make-ListDots (-vec (-v a)) 'a) (-lst (-vec Univ)) #:fail)
(infer-t (-lst -Symbol) (make-ListDots -Symbol 'b) #:indices '(b)
#:result [(make-ListDots (-v b) 'b) (-lst -Bottom)])
(infer-t (-lst -Symbol) (make-ListDots (-v b) 'b) #:indices '(b)
#:result [(make-ListDots (-v b) 'b) (-lst -Symbol)])
(infer-t (make-ListDots (-v b) 'b) (-lst Univ) #:indices '(b))
(infer-t (make-ListDots (-v a) 'a) (-lst Univ))
(infer-t (make-ListDots (-lst (-v a)) 'a) (-lst (-lst Univ)))
(infer-t (make-ListDots (-vec (-v a)) 'a) (-lst (-vec Univ)) #:fail)
(infer-t (make-ListDots (-v a) 'b) (make-ListDots -Symbol 'b) #:vars '(a))
(infer-t (make-ListDots (-v b) 'b) (make-ListDots -Symbol 'b) #:indices '(b))
(infer-t (make-ListDots -Symbol 'b) (make-ListDots (-v b) 'b) #:indices '(b))
(infer-t (make-ListDots -Symbol 'b) (make-ListDots Univ 'b) #:indices '(b))
(infer-t (make-ListDots (-v b) 'b) (make-ListDots (-v b) 'b) #:indices '(b))
(infer-t (make-ListDots (-v b) 'b) (make-ListDots Univ 'b) #:indices '(b))
(infer-t (-pair (-v a) (make-ListDots (-v b) 'b))
(-pair (-v a) (make-ListDots (-v b) 'b))
#:result [(-v a) (-v a)])
(infer-t (make-ListDots (-v a) 'b) (make-ListDots -Symbol 'b) #:vars '(a))
(infer-t (make-ListDots (-v b) 'b) (make-ListDots -Symbol 'b) #:indices '(b))
(infer-t (make-ListDots -Symbol 'b) (make-ListDots (-v b) 'b) #:indices '(b))
(infer-t (make-ListDots -Symbol 'b) (make-ListDots Univ 'b) #:indices '(b))
(infer-t (make-ListDots (-v b) 'b) (make-ListDots (-v b) 'b) #:indices '(b))
(infer-t (make-ListDots (-v b) 'b) (make-ListDots Univ 'b) #:indices '(b))
(infer-t (-pair (-v a) (make-ListDots (-v b) 'b))
(-pair (-v a) (make-ListDots (-v b) 'b))
#:result [(-v a) (-v a)])
[infer-t (->... null ((-v a) a) (-v b)) (-> -Symbol -String) #:vars '(b) #:indices '(a)]
[infer-t (->... null ((-v a) a) (make-ListDots (-v a) 'a)) (-> -String -Symbol (-lst* -String -Symbol)) #:indices '(a)]
[infer-t (->... (list (-v b)) ((-v a) a) (-v b)) (-> -String -Symbol -String) #:vars '(b) #:indices '(a)]
[infer-t (->... (list (-v b)) ((-v a) a) (-v b))
(->... (list -Symbol) (-String a) (-v b))
#:vars '(b) #:indices '(a)
#:result [(-lst* (make-ListDots (-v a) 'a) (-v b))
(-lst* (-lst -String) -Symbol)]]
[infer-t (->* (list -Symbol) -String -Void)
(->... (list) ((-v a) a) -Void)
#:indices '(a)
#:result [(-lst* (make-ListDots (-v a) 'a))
(-lst* (-lst* -Bottom #:tail (-lst -Bottom)))]]
[infer-t (->* (list) -String -Void) (->... (list) (-String a) -Void)]
[infer-t (->... null ((-v a) a) (-v b)) (-> -Symbol -String) #:vars '(b) #:indices '(a)]
[infer-t (->... null ((-v a) a) (make-ListDots (-v a) 'a)) (-> -String -Symbol (-lst* -String -Symbol)) #:indices '(a)]
[infer-t (->... (list (-v b)) ((-v a) a) (-v b)) (-> -String -Symbol -String) #:vars '(b) #:indices '(a)]
[infer-t (->... (list (-v b)) ((-v a) a) (-v b))
(->... (list -Symbol) (-String a) (-v b))
#:vars '(b) #:indices '(a)
#:result [(-lst* (make-ListDots (-v a) 'a) (-v b))
(-lst* (-lst -String) -Symbol)]]
[infer-t (->* (list -Symbol) -String -Void)
(->... (list) ((-v a) a) -Void)
#:indices '(a)
#:result [(-lst* (make-ListDots (-v a) 'a))
(-lst* (-lst* -Bottom #:tail (-lst -Bottom)))]]
[infer-t (->* (list) -String -Void) (->... (list) (-String a) -Void)]
[infer-l (list (->... null ((-v b) b) (-v a)) (-> (-v a) -Boolean))
(list (-> -String -Symbol) (-> -Symbol -Boolean))
#:vars '(a)
#:indices '(b)]
[infer-l (list (->... null ((-v a) a) (-v b)) (make-ListDots (-v a) 'a))
(list (-> -Symbol -Symbol -String) (-lst* -Symbol -Symbol))
#:vars '(b)
#:indices '(a)]
[infer-l (list (->... null ((-v b) b) (-v a)) (-> (-v a) -Boolean))
(list (-> -String -Symbol) (-> -Symbol -Boolean))
#:vars '(a)
#:indices '(b)]
[infer-l (list (->... null ((-v a) a) (-v b)) (make-ListDots (-v a) 'a))
(list (-> -Symbol -Symbol -String) (-lst* -Symbol -Symbol))
#:vars '(b)
#:indices '(a)]
[infer-t (-> (-values (list -String))) (-> (-values-dots (list) -Symbol 'b)) #:indices '(b) #:fail]
[infer-t (make-ListDots -String 'a) (make-ListDots -Symbol 'b) #:indices '(b) #:fail]
[infer-t (make-ListDots -String 'a) (make-ListDots -Symbol 'b) #:indices '(a) #:fail]
[infer-t (-lst* -String) (make-ListDots -Symbol 'b) #:indices '(b) #:fail]
[infer-t (->* (list -Symbol) -Symbol -Void) (->* (list) (-v a) -Void) #:vars '(a) #:fail]
[infer-t (-> (-values (list -String))) (-> (-values-dots (list) -Symbol 'b)) #:indices '(b) #:fail]
[infer-t (make-ListDots -String 'a) (make-ListDots -Symbol 'b) #:indices '(b) #:fail]
[infer-t (make-ListDots -String 'a) (make-ListDots -Symbol 'b) #:indices '(a) #:fail]
[infer-t (-lst* -String) (make-ListDots -Symbol 'b) #:indices '(b) #:fail]
[infer-t (->* (list -Symbol) -Symbol -Void) (->* (list) (-v a) -Void) #:vars '(a) #:fail]
[infer-t (-> (-values (list -Bottom))) (-> (-values (list (-v b) (-v b)))) #:vars '(a)]
[infer-t (-> (-values (list (-v a)))) (-> (-values (list (-v b) (-v b)))) #:vars '(a)]
[infer-t (-> (-values (list -Bottom))) (-> (-values (list (-v b) (-v b)))) #:vars '(a)]
[infer-t (-> (-values (list (-v a)))) (-> (-values (list (-v b) (-v b)))) #:vars '(a)]
[infer-t
(-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-lst (-v b)) 'b))
(-lst* (-> Univ Univ))
#:indices '(b) #:fail]
[infer-t
(-lst* (-> Univ Univ))
(-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-lst (-v b)) 'b))
#:indices '(b) #:fail]
[infer-t
(-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-v b) 'b))
(-pair (-> -Symbol Univ) (-lst -String))
#:indices '(b) #:fail]
[infer-t
(-pair (-> -Symbol Univ) (-lst -String))
(-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-v b) 'b))
#:indices '(b) #:fail]
[infer-t
(-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-lst (-v b)) 'b))
(-lst* (-> Univ Univ))
#:indices '(b) #:fail]
[infer-t
(-lst* (-> Univ Univ))
(-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-lst (-v b)) 'b))
#:indices '(b) #:fail]
[infer-t
(-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-v b) 'b))
(-pair (-> -Symbol Univ) (-lst -String))
#:indices '(b) #:fail]
[infer-t
(-pair (-> -Symbol Univ) (-lst -String))
(-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-v b) 'b))
#:indices '(b) #:fail]
[infer-t
(-lst (-mu A (Un (-v b) (-lst A))))
(-mu C (Un (-v b2) (-lst C)))
#:vars '(b2)
#:result [(-vec (-v b2)) (-vec (-lst (-mu A (Un (-v b) (-lst A)))))]]
[infer-t
(-lst (-mu A (Un (-v b) (-lst A))))
(-mu C (Un (-v b2) (-lst C)))
#:vars '(b2)
#:result [(-vec (-v b2)) (-vec (-lst (-mu A (Un (-v b) (-lst A)))))]]
[infer-t
(-mlst (-val 'b))
(-mlst (-v a))
#:vars '(a)
#:result [(-seq (-v a)) (-seq (-val 'b))]]
[infer-t
(-mlst (-val 'b))
(-mlst (-v a))
#:vars '(a)
#:result [(-seq (-v a)) (-seq (-val 'b))]]
[infer-t
(-lst (-val (-v a)))
(Un (-pair (-v a) Univ) -Null)
#:vars '(a)]
[infer-t
(-lst (-val (-v a)))
(Un (-pair (-v a) Univ) -Null)
#:vars '(a)]
;; Currently Broken
;(infer-t (make-ListDots -Symbol 'b) (-pair -Symbol (-lst -Symbol)) #:indices '(b))
[i2-t (-v a) N ('a N)]
[i2-t (-pair (-v a) (-v a)) (-pair N (Un N B)) ('a (Un N B))]
[i2-t (-lst (-v a)) (-lst* N N) ('a N)]
[i2-t (-lst (-v a)) (-lst* N B) ('a (Un N B))]
[i2-t Univ (Un N B)]
[i2-t ((-v a) . -> . (-v b)) (-> N N) ('b N) ('a (Un))]
[i2-t (-> (-v a) (-v a)) (->* null B B) ('a B)]
;; Currently Broken
;(infer-t (make-ListDots -Symbol 'b) (-pair -Symbol (-lst -Symbol)) #:indices '(b))
[i2-t (-v a) N ('a N)]
[i2-t (-pair (-v a) (-v a)) (-pair N (Un N B)) ('a (Un N B))]
[i2-t (-lst (-v a)) (-lst* N N) ('a N)]
[i2-t (-lst (-v a)) (-lst* N B) ('a (Un N B))]
[i2-t Univ (Un N B)]
[i2-t ((-v a) . -> . (-v b)) (-> N N) ('b N) ('a (Un))]
[i2-t (-> (-v a) (-v a)) (->* null B B) ('a B)]
[i2-l (list (-v a) (-v a) (-v b))
(list (Un (-val 1) (-val 2)) N N)
'(a b) ('b N) ('a N)]
[i2-l (list (-> (-v a) Univ) (-lst (-v a)))
(list (-> N (Un N B)) (-lst N))
'(a) ('a N)]
[i2-l (list (-> (-v a) (-v b)) (-lst (-v a)))
(list (-> N N) (-lst (Un (-val 1) (-val 2))))
'(a b) ('b N) ('a (Un (-val 1) (-val 2)))]
[i2-l (list (-lst (-v a)))
(list (-lst (Un B N)))
'(a) ('a (Un N B))]
;; error tests
[i2-f (-lst (-v a)) Univ]
[i2-f (->* null B B) (-> (-v a) (-v b))]
))
[i2-l (list (-v a) (-v a) (-v b))
(list (Un (-val 1) (-val 2)) N N)
'(a b) ('b N) ('a (Un (-val 2) N))]
[i2-l (list (-> (-v a) Univ) (-lst (-v a)))
(list (-> N (Un N B)) (-lst N))
'(a) ('a N)]
[i2-l (list (-> (-v a) (-v b)) (-lst (-v a)))
(list (-> N N) (-lst (Un (-val 1) (-val 2))))
'(a b) ('b N) ('a (Un (-val 1) (-val 2)))]
[i2-l (list (-lst (-v a)))
(list (-lst (Un B N)))
'(a) ('a (Un N B))]
;; error tests
[i2-f (-lst (-v a)) Univ]
[i2-f (->* null B B) (-> (-v a) (-v b))]
))
(define tests
(test-suite "All inference tests"
pd-tests
fv-tests
infer-tests))
(test-suite
"All inference tests"
fv-tests
fi-tests
pd-tests
infer-tests
))

View File

@ -4,7 +4,7 @@
rackunit
(rep object-rep type-rep)
(env init-envs)
(types abbrev union))
(types abbrev))
(provide tests)
(gen-test-main)
@ -29,16 +29,16 @@
(convert (-mu x (-lst* Univ (-box x))))
'(make-Mu 'x (make-Pair Univ (make-Pair (make-Box (make-F 'x)) -Null))))
(check-equal?
(convert (make-StructTypeTop))
(convert -StructTypeTop)
'-StructTypeTop)
(check-equal?
(convert (make-BoxTop))
(convert -BoxTop)
'-BoxTop)
(check-equal?
(convert (make-ClassTop))
(convert -ClassTop)
'-ClassTop)
(check-equal?
(convert (make-FieldPE))
(convert -field)
'-field)
(check-equal?
(convert (make-StructType (make-Struct #'foo #f null #f #f #'foo?)))

View File

@ -4,7 +4,7 @@
rackunit racket/format
(typecheck tc-metafunctions tc-subst)
(rep prop-rep type-rep object-rep values-rep)
(types abbrev union prop-ops tc-result numeric-tower)
(types abbrev prop-ops tc-result numeric-tower)
(for-syntax racket/base syntax/parse))
(provide tests)

View File

@ -13,7 +13,7 @@
(rep type-rep values-rep)
(submod typed-racket/base-env/base-types initialize)
(rename-in (types union abbrev numeric-tower resolve)
(rename-in (types abbrev numeric-tower resolve)
[Un t:Un] [-> t:->] [->* t:->*]))
(only-in typed-racket/typed-racket do-standard-inits)
(base-env base-types base-types-extra colon)
@ -68,7 +68,7 @@
[delay-errors? #f])
(define expected ty-val)
(define actual (parse-type (quote-syntax ty-stx)))
#`(values #,expected #,actual #,(type-equal? actual expected)))))
#`(values #,expected #,actual #,(equal? actual expected)))))
(unless same?
(with-check-info (['expected expected] ['actual actual])
(fail-check "Unequal types")))))]))
@ -252,7 +252,7 @@
[(Struct-Type arity-at-least) (make-StructType (resolve -Arity-At-Least))]
[FAIL (Struct-Type Integer)]
[FAIL (Struct-Type foo)]
[Struct-TypeTop (make-StructTypeTop)]
[Struct-TypeTop -StructTypeTop]
;; keyword function types
[(#:a String -> String)
@ -396,7 +396,7 @@
(make-Unit null null null (-values (list -Void)))]
[(Unit (import) (export))
(make-Unit null null null (-values (list -Void)))]
[UnitTop (make-UnitTop)]
[UnitTop -UnitTop]
[FAIL (Unit (export) String)]
[FAIL (Unit (import) String)]
[FAIL (Unit (init-depend) String)]

View File

@ -3,7 +3,7 @@
(require "test-utils.rkt"
rackunit racket/format
(rep prop-rep)
(types abbrev union prop-ops)
(types abbrev prop-ops)
(for-syntax racket/base syntax/parse))
(provide tests)

View File

@ -3,7 +3,7 @@
(for-syntax racket/base)
(r:infer infer)
(rep type-rep)
(types abbrev numeric-tower subtype union subtract overlap)
(types abbrev numeric-tower subtype subtract overlap)
rackunit)
(provide tests)
(gen-test-main)
@ -57,7 +57,7 @@
(-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 (make-HashtableTop))
(make-Listof -HashtableTop)
(make-Listof (-HT -String (-mu x (Un -String (-HT -String x)))))]))
(define-syntax (remo-tests stx)

View File

@ -5,9 +5,10 @@
(for-syntax racket/base)
(for-template racket/base)
(rep type-rep prop-rep object-rep)
(for-syntax (rename-in (types utils union numeric-tower abbrev prop-ops)
[Un t:Un]
[-> t:->]))
(for-syntax
(rename-in (types utils numeric-tower abbrev prop-ops)
[Un t:Un]
[-> t:->]))
(utils tc-utils utils)
(utils mutated-vars)
@ -18,7 +19,7 @@
(for-syntax syntax/kerncase syntax/parse racket/syntax
(types abbrev numeric-tower utils)
(utils mutated-vars) (env mvar-env)
(utils tc-utils) (typecheck typechecker))
(utils tc-utils) (typecheck typechecker check-below))
typed-racket/base-env/prims
typed-racket/base-env/base-types
(for-syntax typed-racket/standard-inits))
@ -34,19 +35,23 @@
[(tc-e expr ty) (syntax/loc stx (tc-e expr #:ret (reduce-tc-results/subsumption (ret ty))))]
[(id a #:ret b)
(syntax/loc stx
(test-case (format "~a ~a" (quote-line-number id) 'a)
(let-values
([(res1 expanded)
(phase1-phase0-eval
(test-case
(format "~a ~a" (quote-line-number id) 'a)
(let*-values
([(res1 res2 equiv? expanded)
(phase1-phase0-eval
(let ([ex (local-expand #'a 'expression null)])
(find-mutated-vars ex mvar-env)
#`(values '#,(tc-expr ex) '#,(syntax->datum ex))))]
[(res2) (phase1-phase0-eval #`'#,b)])
(with-check-info (['expanded expanded])
(unless (tc-result-equal/test? res1 res2)
(fail-check (format "Expression didn't have expected type.\n Expected: ~a\n Actual: ~a\n"
(struct->vector res1)
(struct->vector res2))))))))]))
(let ([res1 (tc-expr ex)]
[res2 b])
(let ([equiv? (and (check-below res1 res2)
(check-below res2 res1))])
#`(values '#,res1 '#,res2 '#,equiv? '#,(syntax->datum ex))))))])
(with-check-info (['expanded expanded])
(unless equiv?
(fail-check (format "Expression didn't have expected type.\n Expected: ~a\n Actual: ~a\n"
(struct->vector res1)
(struct->vector res2))))))))]))
(define tests
(test-suite

View File

@ -9,7 +9,7 @@
racket/base
(private type-contract)
(static-contracts instantiate)
(types abbrev numeric-tower union)))
(types abbrev numeric-tower)))
(provide tests)
(gen-test-main)

View File

@ -8,18 +8,26 @@
(gen-test-main)
(define-syntax-rule (s img var tgt result)
(test-eq? (format "~a" '(img tgt)) (substitute img 'var tgt) result))
(test-equal? (format "~a" '(img tgt))
(substitute img 'var tgt)
result))
(define-syntax-rule (s* imgs rest var tgt result)
(test-eq? (format "~a" '(img tgt)) (substitute-dots (list . imgs) rest 'var tgt) result))
(test-equal? (format "~a" '(img tgt))
(substitute-dots (list . imgs) rest 'var tgt)
result))
(define-syntax-rule (s... imgs var tgt result)
(test-eq? (format "~a" '(img tgt)) (substitute-dots (list . imgs) #f 'var tgt) result))
(test-equal? (format "~a" '(img tgt))
(substitute-dots (list . imgs) #f 'var tgt)
result))
(define tests
(test-suite "Tests for substitution"
(s -Number a (-v a) -Number)
(s -Number a (-pair (-v a) -String) (-pair -Number -String))
(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))

View File

@ -1,7 +1,7 @@
#lang racket/base
(require "test-utils.rkt"
(types subtype numeric-tower union utils abbrev)
(types subtype numeric-tower utils abbrev)
(rep type-rep values-rep)
(env init-envs type-env-structs)
rackunit
@ -10,69 +10,252 @@
(provide tests)
(gen-test-main)
(define-for-syntax (single-subtype-test stx)
(syntax-case stx (FAIL)
[(FAIL t s) (syntax/loc stx (test-check (format "FAIL ~a" '(t s)) (lambda (a b) (not (subtype a b))) t s))]
[(t s) (syntax/loc stx (test-check (format "~a" '(t s)) subtype t s))]))
(define-syntax (subtyping-tests stx)
(define (single-test stx)
(syntax-case stx (FAIL)
[(FAIL t s) (syntax/loc stx (test-check (format "FAIL ~a" '(t s)) (lambda (a b) (not (subtype a b))) t s))]
[(t s) (syntax/loc stx (test-check (format "~a" '(t s)) subtype t s))]))
(syntax-case stx ()
[(_ str cl ...)
(with-syntax ([(new-cl ...) (map single-subtype-test (syntax->list #'(cl ...)))])
(syntax/loc stx
(begin (test-suite (format "Tests for subtyping (~a)" str)
new-cl ...))))]))
(define x1 #'x)
(define x2 #'x)
(define A (make-F (gensym 'A)))
(define B (make-F (gensym 'B)))
(define AorB (Un A B))
(define t1a (-mu T (-lst (Un (-v a) T))))
(define t1b (unfold t1a))
(define t2 -Number)
(define-for-syntax (covariant-test stx)
(syntax-case stx ()
[(mk []) (syntax/loc stx
(subtyping-tests
(format "covariant tests for ~a" mk)
[(mk A) (mk A)]
[(mk t1a) (mk t1b)]
[(mk A) (mk AorB)]
[FAIL (mk AorB) (mk A)]
[FAIL (mk Univ) A]
[FAIL A (mk Univ)]))]
[(mk [] [])
(syntax/loc stx
(subtyping-tests
(format "covariant tests for ~a" mk)
[(mk A B) (mk A B)]
[(mk A B) (mk AorB B)]
[(mk A B) (mk A AorB)]
[(mk A B) (mk AorB AorB)]
[(mk t1a t1a) (mk t1b t1b)]
[FAIL (mk AorB B) (mk A B)]
[FAIL (mk A AorB) (mk A B)]
[FAIL (mk AorB AorB) (mk A B)]
[FAIL (mk Univ Univ) A]
[FAIL A (mk Univ Univ)]))]))
(define-syntax (covariant-tests stx)
(syntax-case stx ()
[(_ cl ...)
(with-syntax ([(new-cl ...) (map single-test (syntax->list #'(cl ...)))])
(syntax/loc stx
(begin (test-suite "Tests for subtyping"
new-cl ...))))]))
(with-syntax ([(co-tests ...) (map covariant-test (syntax->list #'(cl ...)))])
(syntax/loc stx
(begin co-tests ...)))]))
(define-for-syntax (invariant-test stx)
(syntax-case stx ()
[(mk () #:top top)
(syntax/loc stx
(subtyping-tests
(format "invariant tests for ~a" mk)
[(mk A) (mk A)]
[(mk t1a) (mk t1b)]
[(mk A) top]
[FAIL top (mk A)]
[FAIL (mk A) (mk AorB)]
[FAIL (mk AorB) (mk A)]
[FAIL (mk Univ) A]
[FAIL A (mk Univ)]))]
[(mk () () #:top top)
(syntax/loc stx
(subtyping-tests
(format "invariant tests for ~a" mk)
[(mk A B) (mk A B)]
[(mk t1a t1a) (mk t1b t1b)]
[(mk A B) top]
[FAIL top (mk A B)]
[FAIL (mk A B) (mk AorB B)]
[FAIL (mk A B) (mk A AorB)]
[FAIL (mk A B) (mk AorB AorB)]
[FAIL (mk AorB B) (mk A B)]
[FAIL (mk A AorB) (mk A B)]
[FAIL (mk AorB AorB) (mk A B)]
[FAIL (mk Univ Univ) A]
[FAIL A (mk Univ Univ)]))]))
(define-syntax (invariant-tests stx)
(syntax-case stx ()
[(_ cl ...)
(with-syntax ([(inv-tests ...) (map invariant-test (syntax->list #'(cl ...)))])
(syntax/loc stx
(begin inv-tests ...)))]))
(define t1 (-mu T (-lst (Un (-v a) T))))
(define t2 (unfold t1))
(define tests
(define simple-tests
(subtyping-tests
;; trivial examples
(Univ Univ)
(-Number Univ)
(-Boolean Univ)
(-Symbol Univ)
(-Void Univ)
[-Number -Number]
"Simple Subtyping Tests"
;; trivial () examples
[Univ Univ]
[-Bottom Univ]
[-Number Univ]
[-Boolean Univ]
[-Symbol Univ]
[-Void Univ]
[FAIL Univ -Symbol]
[FAIL Univ -Number]
;; Reflexivity
[(-val 6) (-val 6)]
[-Symbol -Symbol]
;; Error
[Err -Number]
[-Number Err]
;; B
[(make-B 0) (make-B 0)]
[FAIL (make-B 0) (make-B 1)]
;; F
[(-v a) (-v a)]
[FAIL (-v a) (-v b)]
;; Value
[(-val 'a) (-val 'a)]
[(-val 'a) -Symbol]
[FAIL -Symbol (-val 'a)]
[FAIL (-val 'a) (-val 'b)]
;; Base
[-String -String]
[FAIL -Symbol -String]
;; Opaque
[(make-Opaque x1) (make-Opaque x2)]
[FAIL (make-Opaque #'a) (make-Opaque #'b)]
;; Refinement
[(make-Refinement A x1) (make-Refinement A x2)]
;[(make-Refinement t1a x1) (make-Refinement t1b x1)]
;[(make-Refinement t1a x1) t1b]
[FAIL (make-Refinement t2 x1) t1b]
[FAIL (make-Refinement A #'a) (make-Refinement A #'b)]
[FAIL (make-Refinement A x1) (make-Refinement B x1)]
;; Distinction
[(-Distinction 'a 'b A) A]
[(-Distinction 'a 'b A) AorB]
[FAIL (-Distinction 'a 'b AorB) A]
))
(define structural-tests
(test-suite
"Structural Subtyping tests"
(covariant-tests
[make-Pair () ()]
[make-Promise ()]
[make-Ephemeron ()]
[make-CustodianBox ()]
[make-Set ()]
[make-Evt ()]
[make-Syntax ()]
[make-Future ()])
(invariant-tests
[make-MPair () () #:top -MPairTop]
[make-Vector () #:top -VectorTop]
[make-Box () #:top -BoxTop]
[make-Channel () #:top -ChannelTop]
[make-Async-Channel () #:top -Async-ChannelTop]
[make-ThreadCell () #:top -ThreadCellTop]
[make-Weak-Box () #:top -Weak-BoxTop]
[make-Hashtable () () #:top -HashtableTop]
[make-Prompt-Tagof () () #:top -Prompt-TagTop]
[make-Continuation-Mark-Keyof () #:top -Continuation-Mark-KeyTop])
(subtyping-tests
"Param"
[(make-Param A B) (make-Param A B)]
[(make-Param A B) (make-Param A AorB)]
[(make-Param AorB B) (make-Param A B)]
[FAIL (make-Param A B) (make-Param AorB B)]
[FAIL (make-Param A AorB) (make-Param A B)])
(subtyping-tests
"Evt special cases"
;; evts
[(-evt t1a) (-evt t1b)]
[FAIL (-evt -Byte) (-evt -String)]
[-Semaphore (-evt -Semaphore)]
[FAIL -Semaphore (-evt -Int)]
[-Output-Port (-evt -Output-Port)]
[FAIL -Output-Port (-evt -Int)]
[-Input-Port (-evt -Input-Port)]
[FAIL -Input-Port (-evt -Int)]
[-TCP-Listener (-evt -TCP-Listener)]
[FAIL -TCP-Listener (-evt -Int)]
[-Thread (-evt -Thread)]
[FAIL -Thread (-evt -Int)]
[-Subprocess (-evt -Subprocess)]
[FAIL -Subprocess (-evt -Int)]
[-Will-Executor (-evt -Will-Executor)]
[FAIL -Will-Executor (-evt -Int)]
[(make-CustodianBox -String) (-evt (make-CustodianBox -String))]
[FAIL (make-CustodianBox -String) (-evt -String)]
[(-channel -String) (-evt -String)]
[FAIL (-channel -String) (-evt -Int)]
[-Log-Receiver (-evt (make-HeterogeneousVector
(list -Symbol -String Univ
(Un (-val #f) -Symbol))))]
[FAIL -Log-Receiver (-evt -Int)])
(subtyping-tests
"Sequence special cases"
[(-set -Number) (make-Sequence (list -Number))]
[-FlVector (make-Sequence (list -Flonum))]
[-FlVector (make-Sequence (list -Number))]
[-FxVector (make-Sequence (list -Fixnum))]
[-FxVector (make-Sequence (list -Number))]
[(-val 5) (-seq -Nat)]
[(-val 5) (-seq -Byte)]
[-Index (-seq -Index)]
[-NonNegFixnum (-seq -NonNegFixnum)]
[-Index (-seq -Nat)]
[FAIL (-val -5) (-seq -Nat)]
[FAIL -Fixnum (-seq -Fixnum)]
[FAIL -NonNegFixnum (-seq -Index)]
[FAIL (-val 5.0) (-seq -Nat)]
[(-pair -String (-lst -String)) (-seq -String)]
[FAIL (-pair -String (-lst -Symbol)) (-seq -String)]
[FAIL (-pair -String (-vec -String)) (-seq -String)]
[(-mpair -String -Null) (-seq -String)]
[(-mlst -String) (-seq -String)]
[(-mpair -String (-mlst -String)) (-seq -String)]
[FAIL (-mpair -String (-mlst -Symbol)) (-seq -String)]
[FAIL (-mpair -String (-vec -String)) (-seq -String)]
[(-mpair -String (-mlst (-val "hello"))) (-seq -String)])
(subtyping-tests
"Other Structural Cases"
[(-Param -String -Symbol) (cl->* (-> -Symbol) (-> -String -Void))]
[(-lst* -Number -Number (-val 'foo)) (-lst (Un -Number -Symbol))])))
(define other-tests
(subtyping-tests
"Other Subtyping Tests"
;; recursive types and unions
[(Un (-pair Univ (-lst Univ)) -Null) (-lst Univ)]
[(-lst* -Number -Number (-val 'foo)) (-lst Univ)]
[(-lst* -Number -Number (-val 'foo)) (-lst (Un -Number -Symbol))]
[(-pair (-val 6) (-val 6)) (-pair -Number -Number)]
[(-val 6) (-val 6)]
;; unions
[(Un -Number) -Number]
[(Un -Number -Number) -Number]
[(Un -Number -Symbol) (Un -Symbol -Number)]
[(Un (-val 6) (-val 7)) -Number]
[(Un (-val #f) (Un (-val 6) (-val 7))) (Un -Number (Un -Boolean -Symbol))]
[(Un (-val #f) (Un (-val 6) (-val 7))) (-mu x (Un -Number (Un -Boolean -Symbol)))]
[(Un -Number (-val #f) (-mu x (Un -Number -Symbol (make-Listof x))))
(-mu x (Un -Number -Symbol -Boolean (make-Listof x)))]
;; intersections
[(-unsafe-intersect -Number) -Number]
[(-unsafe-intersect -Number -Symbol) -Number]
[(-unsafe-intersect -Boolean -Number) -Number]
[(-unsafe-intersect -Number -Number) -Number]
[FAIL -Number (-unsafe-intersect -Boolean -Number)]
[(-unsafe-intersect -Boolean -Number) (-unsafe-intersect -Boolean -Number)]
[(-unsafe-intersect -Sexp
(Un -Null (-pair -Sexp (-unsafe-intersect (make-Listof Univ) -Sexp))))
(make-Listof Univ)]
[(-unsafe-intersect (-v A) (-v B))
(Un -String (-unsafe-intersect (-v A) (-v B)))]
;; sexps vs list*s of nums
[(-mu x (Un -Number -Symbol (make-Listof x))) (-mu x (Un -Number -Symbol -Boolean (make-Listof x)))]
[(-mu x (Un -Number (make-Listof x))) (-mu x (Un -Number -Symbol (make-Listof x)))]
[(-mu x (Un -Number (make-Listof x))) (-mu y (Un -Number -Symbol (make-Listof y)))]
;; a hard one
[(-mu x (Un -Number (-lst* x -Symbol x))) -Sexp]
[t1 (unfold t1)]
[(unfold t1) t1]
;; simple function types
((Univ . -> . -Number) (-Number . -> . Univ))
[(Univ Univ Univ . -> . -Number) (Univ Univ -Number . -> . -Number)]
[t1a (unfold t1a)]
[(unfold t1a) t1a]
;; simple list types
[(make-Listof -Number) (make-Listof Univ)]
[(make-Listof -Number) (make-Listof -Number)]
@ -80,24 +263,10 @@
[(-mu x (make-Listof x)) (-mu x* (make-Listof x*))]
[(-pair -Number -Number) (-pair Univ -Number)]
[(-pair -Number -Number) (-pair -Number -Number)]
;; from page 7
;; from page 7 (my favorite page! But seriously, page 7 of... what???)
[(-mu t (-> t t)) (-mu s (-> s s))]
[(-mu s (-> -Number s)) (-mu t (-> -Number (-> -Number t)))]
;; polymorphic types
[(-poly (t) (-> t t)) (-poly (s) (-> s s))]
[FAIL (make-Listof -Number) (-poly (t) (make-Listof t))]
[(-poly (a) (make-Listof (-v a))) (make-Listof -Number)] ;;
[(-poly (a) -Number) -Number]
[(-val 6) -Number]
[(-val 'hello) -Symbol]
[(-set -Number) (make-Sequence (list -Number))]
[-FlVector (make-Sequence (list -Flonum))]
[-FlVector (make-Sequence (list -Number))]
[-FxVector (make-Sequence (list -Fixnum))]
[-FxVector (make-Sequence (list -Number))]
[((Un -Symbol -Number) . -> . -Number) (-> -Number -Number)]
[(-poly (t) (-> -Number t)) (-mu t (-> -Number t))]
;; not subtypes
[FAIL (-val 'hello) -Number]
[FAIL (-val #f) -Symbol]
@ -108,10 +277,78 @@
[FAIL -Symbol (-val 'Sym)]
[FAIL (Un -Symbol -Number) (-poly (a) -Number)]
;; bugs found
[(Un (-val 'foo) (-val 6)) (Un (-val 'foo) (-val 6))]
[(-poly (a) (make-Listof (-v a))) (make-Listof (-mu x (Un (make-Listof x) -Number)))]
[FAIL (make-Listof (-mu x (Un (make-Listof x) -Number))) (-poly (a) (make-Listof a))]
;; HeterogeneousVector
[(make-HeterogeneousVector (list t1a)) (-vec t1b)]
[(make-HeterogeneousVector (list t1a t1a)) (-vec t1b)]
[FAIL (-vec t1b) (make-HeterogeneousVector (list t1a t1a))]
[FAIL (make-HeterogeneousVector (list t2)) (-vec t1b)]
[FAIL (make-HeterogeneousVector (list t1a t2)) (-vec t1b)]
[(make-HeterogeneousVector (list t1a t1b)) (make-HeterogeneousVector (list t1b t1a))]
[(make-HeterogeneousVector (list t1a t1b)) (make-HeterogeneousVector (list t1b t1a))]
[FAIL (make-HeterogeneousVector (list t1a)) (make-HeterogeneousVector (list t1b t1a))]
[FAIL (make-HeterogeneousVector (list t1a t2)) (make-HeterogeneousVector (list t1b t1a))]
[FAIL (make-HeterogeneousVector (list t2 t1a)) (make-HeterogeneousVector (list t1b t1a))]
))
(define set-theoretic-type-tests
(subtyping-tests
"Set-theoretic Subtyping"
;; Unions
[(-val 0.0f0) -SingleFlonum]
[(-val -0.0f0) -SingleFlonum]
[(-val 1.0f0) -SingleFlonum]
[(-val -34.2f0) -NegSingleFlonum]
[(-val 6) -Number]
[(Un (-val 'foo) (-val 6)) (Un (-val 'foo) (-val 6))]
[(Un -Number) -Number]
[(Un -Number -Number) -Number]
[(Un -Number -Symbol) (Un -Symbol -Number)]
[(Un (-val 6) (-val 7)) -Number]
[(Un (-val #f) (Un (-val 6) (-val 7))) (Un -Number (Un -Boolean -Symbol))]
;; intersections
[(-unsafe-intersect -Number) -Number]
[(-unsafe-intersect -Number -Symbol) -Number]
[(-unsafe-intersect -Boolean -Number) -Number]
[(-unsafe-intersect -Number -Number) -Number]
[FAIL -Number (-unsafe-intersect -Boolean -Number)]
[(-unsafe-intersect -Boolean -Number) (-unsafe-intersect -Boolean -Number)]
[(-unsafe-intersect -Sexp
(Un -Null (-pair -Sexp (-unsafe-intersect (make-Listof Univ) -Sexp))))
(make-Listof Univ)]
[(-unsafe-intersect (-v A) (-v B))
(Un -String (-unsafe-intersect (-v A) (-v B)))]
))
(define poly-tests
(subtyping-tests
"Polymorphic Subtyping"
[(-poly (t) (-> t t)) (-poly (s) (-> s s))]
[FAIL (make-Listof -Number) (-poly (t) (make-Listof t))]
[(-poly (a) (make-Listof (-v a))) (make-Listof -Number)] ;;
[(-poly (a) -Number) -Number]
[FAIL (-poly (a) (-poly (b) (-pair a b))) (-poly (a) (-poly (b) (-pair b a)))]
;; The following currently are not subtypes, because they are not replaceable
;; in an instantiation context. It may be sound for them to be subtypes but
;; the implications of that change are unknown.
[FAIL (-poly (x) (-lst x)) (-poly (x y) (-lst x))]
[FAIL (-poly (y z) (-lst y)) (-poly (z y) (-lst y))]
[FAIL (-poly (y) (-poly (z) (-pair y z))) (-poly (y z) (-pair y z))]
[FAIL (-poly (y z) (-pair y z)) (-poly (y) (-poly (z) (-pair y z)))]))
(define function-tests
(subtyping-tests
"Function Subtyping"
;; simple function types
[((Un -Symbol -Number) . -> . -Number) (-> -Number -Number)]
[(-poly (t) (-> -Number t)) (-mu t (-> -Number t))]
((Univ . -> . -Number) (-Number . -> . Univ))
[(Univ Univ Univ . -> . -Number) (Univ Univ -Number . -> . -Number)]
;; case-lambda
[(cl-> [(-Number) -Number] [(-Boolean) -Boolean]) (-Number . -> . -Number)]
;; special case for unused variables
@ -132,8 +369,9 @@
[(-Number) a]))
(cl-> [() (-pair -Number (-v b))]
[(-Number) (-pair -Number (-v b))])]
;[(-values (list -Number)) (-values (list Univ))]
;; polymorphic function types should be subtypes of the function top
[(-poly (a) (a . -> . a)) top-func]
[FAIL (-> Univ) (null Univ . ->* . Univ)]
[(-poly (b) ((Un (make-Base 'foo #'dummy values #f)
(-struct #'bar #f
@ -142,126 +380,15 @@
((Un (make-Base 'foo #'dummy values #f) (-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f))))
. -> . (-lst (-pair -Number (-v a))))]
[(-poly (b) ((-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld b #'values #f))) . -> . (-lst b)))
((-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f))) . -> . (-lst (-pair -Number (-v a))))]
((-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)))
. -> .
(-lst (-pair -Number (-v a))))]
[(-poly (a) (a . -> . (make-Listof a))) ((-v b) . -> . (make-Listof (-v b)))]
[(-poly (a) (a . -> . (make-Listof a))) ((-pair -Number (-v b)) . -> . (make-Listof (-pair -Number (-v b))))]
[FAIL (-poly (a b) (-> a a)) (-poly (a b) (-> a b))]
[FAIL (-poly (a) (-poly (b) (-pair a b))) (-poly (a) (-poly (b) (-pair b a)))]
;; The following currently are not subtypes, because they are not replacable
;; in an instantiation context. It may be sound for them to be subtypes but
;; the implications of that change are unknown.
[FAIL (-poly (x) (-lst x)) (-poly (x y) (-lst x))]
[FAIL (-poly (y z) (-lst y)) (-poly (z y) (-lst y))]
[FAIL (-poly (y) (-poly (z) (-pair y z))) (-poly (y z) (-pair y z))]
[FAIL (-poly (y z) (-pair y z)) (-poly (y) (-poly (z) (-pair y z)))]
;; polymorphic function types should be subtypes of the function top
[(-poly (a) (a . -> . a)) top-func]
(FAIL (-> Univ) (null Univ . ->* . Univ))
[(cl->* (-Number . -> . -String) (-Boolean . -> . -String)) ((Un -Boolean -Number) . -> . -String)]
[(-struct #'a #f null) (-struct #'a #f null)]
[(-struct #'a #f (list (make-fld -String #'values #f))) (-struct #'a #f (list (make-fld -String #'values #f)))]
[(-struct #'a #f (list (make-fld -String #'values #f))) (-struct #'a #f (list (make-fld Univ #'values #f)))]
[(-val 0.0f0) -SingleFlonum]
[(-val -0.0f0) -SingleFlonum]
[(-val 1.0f0) -SingleFlonum]
[(-pair -String (-lst -String)) (-seq -String)]
[FAIL (-pair -String (-lst -Symbol)) (-seq -String)]
[FAIL (-pair -String (-vec -String)) (-seq -String)]
[(-mpair -String -Null) (-seq -String)]
[(-mlst -String) (-seq -String)]
[(-mpair -String (-mlst -String)) (-seq -String)]
[FAIL (-mpair -String (-mlst -Symbol)) (-seq -String)]
[FAIL (-mpair -String (-vec -String)) (-seq -String)]
[(-mpair -String (-mlst (-val "hello"))) (-seq -String)]
[(-Param -Byte -Byte) (-Param (-val 0) -Int)]
[FAIL (-Param -Byte -Byte) (-Param -Int -Int)]
[(-Param -String -Symbol) (cl->* (-> -Symbol) (-> -String -Void))]
[(-vec t1) (-vec t2)]
[(make-HeterogeneousVector (list t1)) (-vec t2)]
[(make-HeterogeneousVector (list t1 t2)) (make-HeterogeneousVector (list t2 t1))]
[(-box t1) (-box t2)]
[(-thread-cell t1) (-thread-cell t2)]
[(-channel t1) (-channel t2)]
[(-mpair t1 t2) (-mpair t2 t1)]
[(-HT t1 t2) (-HT t2 t1)]
[(make-Prompt-Tagof t1 t2) (make-Prompt-Tagof t2 t1)]
[(make-Continuation-Mark-Keyof t1) (make-Continuation-Mark-Keyof t2)]
;; evts
[(-evt t1) (-evt t2)]
[FAIL (-evt -Byte) (-evt -String)]
[-Semaphore (-evt -Semaphore)]
[FAIL -Semaphore (-evt -Int)]
[-Output-Port (-evt -Output-Port)]
[FAIL -Output-Port (-evt -Int)]
[-Input-Port (-evt -Input-Port)]
[FAIL -Input-Port (-evt -Int)]
[-TCP-Listener (-evt -TCP-Listener)]
[FAIL -TCP-Listener (-evt -Int)]
[-Thread (-evt -Thread)]
[FAIL -Thread (-evt -Int)]
[-Subprocess (-evt -Subprocess)]
[FAIL -Subprocess (-evt -Int)]
[-Will-Executor (-evt -Will-Executor)]
[FAIL -Will-Executor (-evt -Int)]
[(make-CustodianBox -String) (-evt (make-CustodianBox -String))]
[FAIL (make-CustodianBox -String) (-evt -String)]
[(-channel -String) (-evt -String)]
[FAIL (-channel -String) (-evt -Int)]
[-Log-Receiver (-evt (make-HeterogeneousVector
(list -Symbol -String Univ
(Un (-val #f) -Symbol))))]
[FAIL -Log-Receiver (-evt -Int)]
[(-val 5) (-seq -Nat)]
[(-val 5) (-seq -Byte)]
[-Index (-seq -Index)]
[-NonNegFixnum (-seq -NonNegFixnum)]
[-Index (-seq -Nat)]
[FAIL (-val -5) (-seq -Nat)]
[FAIL -Fixnum (-seq -Fixnum)]
[FAIL -NonNegFixnum (-seq -Index)]
[FAIL (-val 5.0) (-seq -Nat)]
[(-polydots (a) (->... (list Univ) (a a) (make-ValuesDots null a 'a)))
(-polydots (a) (->... (list -String) (a a) (make-ValuesDots null a 'a)))]
[(-polydots (a) (->... null (Univ a) (make-ValuesDots (list (-result a)) a 'a)))
(-polydots (a) (->... null (-String a) (make-ValuesDots (list (-result a)) a 'a)))]
[(-polydots (a) (->... null (a a) (make-ValuesDots (list (-result -String)) -String 'a)))
(-polydots (a) (->... null (a a) (make-ValuesDots (list (-result Univ)) Univ 'a)))]
[(-polydots (a) (->... null (Univ a) (-values (list Univ))))
(->* null Univ Univ)]
[(-polydots (a) (->... null (a a) (make-ListDots a 'a)))
(-> -String -Symbol (-Tuple (list -String -Symbol)))]
[(-> -String -Symbol (-Tuple (list -String -Symbol)))
(-polydots (a) (-> -String -Symbol (-lst (Un -String -Symbol))))]
[(-polydots (a) (->... null (a a) (make-ListDots a 'a)))
(-poly (a b) (-> a b (-Tuple (list a b))))]
[(-polydots (b a) (-> (->... (list b) (a a) (make-ValuesDots (list (-result b)) a 'a)) Univ))
(-polydots (a) (-> (->... (list) (a a) (make-ValuesDots null a 'a)) Univ))]
[(-polydots (a) (->... (list) (a a) (make-ListDots a 'a)))
(-polydots (b a) (->... (list b) (a a) (-pair b (make-ListDots a 'a))))]
[FAIL
(-polydots (c a b) (->... (list (->... (list a) (b b) c) (-vec a)) ((-vec b) b) (-vec c)))
(->* (list (->* (list) -Symbol -Symbol)) (-vec -Symbol) (-vec -Symbol))]
[(-> Univ -Boolean : (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))
(-> Univ -Boolean : -tt-propset)]
[(-> Univ -Boolean : -ff-propset)
@ -284,9 +411,6 @@
[FAIL (make-ListDots (-box (make-F 'a)) 'a) (-lst (-box Univ))]
[(make-ListDots (-> -Symbol (make-F 'a)) 'a) (-lst (-> -Symbol Univ))]
;[FAIL (make-ValuesDots (list) -Symbol 'a) (make-ValuesDots (list (-result -String)) -String 'a)]
;[(-values (list -Bottom)) (-values (list -String -Symbol))]
[(-> Univ -Bottom) (-> Univ (-values (list -String -Symbol)))]
[(-> Univ -Bottom) (-> Univ (-values-dots null -String 'x))]
@ -326,8 +450,67 @@
[FAIL
(->key -String #:x -Symbol #f #:y -Symbol #f Univ)
(->optkey -String [-Void] #:x -Symbol #t Univ)]
;; Proposition subtyping
[(make-pred-ty (list -Real) -Boolean (Un (-val 0.0) (-val 0)))
(make-pred-ty (list -Int) -Boolean (-val 0))]
;; classes and objects
[(-polydots (a) (->... (list Univ) (a a) (make-ValuesDots null a 'a)))
(-polydots (a) (->... (list -String) (a a) (make-ValuesDots null a 'a)))]
[(-polydots (a) (->... null (Univ a) (make-ValuesDots (list (-result a)) a 'a)))
(-polydots (a) (->... null (-String a) (make-ValuesDots (list (-result a)) a 'a)))]
[(-polydots (a) (->... null (a a) (make-ValuesDots (list (-result -String)) -String 'a)))
(-polydots (a) (->... null (a a) (make-ValuesDots (list (-result Univ)) Univ 'a)))]
[(-polydots (a) (->... null (Univ a) (-values (list Univ))))
(->* null Univ Univ)]
;; ListDots
[(-polydots (a) (->... null (a a) (make-ListDots a 'a)))
(-> -String -Symbol (-Tuple (list -String -Symbol)))]
[(-> -String -Symbol (-Tuple (list -String -Symbol)))
(-polydots (a) (-> -String -Symbol (-lst (Un -String -Symbol))))]
[(-polydots (a) (->... null (a a) (make-ListDots a 'a)))
(-poly (a b) (-> a b (-Tuple (list a b))))]
[(-polydots (b a) (-> (->... (list b) (a a) (make-ValuesDots (list (-result b)) a 'a)) Univ))
(-polydots (a) (-> (->... (list) (a a) (make-ValuesDots null a 'a)) Univ))]
[(-polydots (a) (->... (list) (a a) (make-ListDots a 'a)))
(-polydots (b a) (->... (list b) (a a) (-pair b (make-ListDots a 'a))))]
[FAIL
(-polydots (c a b) (->... (list (->... (list a) (b b) c) (-vec a)) ((-vec b) b) (-vec c)))
(->* (list (->* (list) -Symbol -Symbol)) (-vec -Symbol) (-vec -Symbol))]))
(define struct-tests
(subtyping-tests
"Struct Subtyping"
[(-struct x1 #f null) (-struct x2 #f null)]
[(-struct #'a #f (list (make-fld -String #'values #f))) (-struct #'a #f (list (make-fld -String #'values #f)))]
[(-struct #'a #f (list (make-fld -String #'values #f))) (-struct #'a #f (list (make-fld Univ #'values #f)))]
;; prefab structs
[(-prefab 'foo -String) (-prefab 'foo -String)]
[(-prefab 'foo -String) (-prefab 'foo (-opt -String))]
[(-prefab '(bar foo 1) -String -Symbol) (-prefab 'foo -String)]
[(-prefab '(bar foo 1) -String -Symbol) (-prefab 'foo (-opt -String))]
[FAIL
(-prefab '(foo #(0)) -String) (-prefab '(foo #(0)) (-opt -String))]
[(-prefab '(foo 1 #(0)) -String -Symbol)
(-prefab '(foo #(0)) -String)]
[(-prefab '(bar foo 1 #(0)) -String -Symbol)
(-prefab '(foo #(0)) -String)]
[FAIL
(-prefab '(foo #()) -String) (-prefab '(foo #(0)) (-opt -String))]
;; TODO StructType ?
))
(define oo-tests
(subtyping-tests
"Object Oriented Subtyping"
[(-class #:method ((m (-> -Nat))) #:augment ((m (-> -Nat))))
(-class #:method ((m (-> -Nat))) #:augment ((m (-> -Nat))))]
[(-object #:method ((m (-> -Nat))) #:augment ((m (-> -Nat))))
@ -369,24 +552,43 @@
(-class #:method ((m (-> -Nat))) #:augment ((m (-> -Nat))))]
[FAIL
(-class #:method ((m (-> -Nat))) #:augment ((m (-> -Nat))))
(-class #:method ((m (-> -Nat))))]
(-class #:method ((m (-> -Nat))))]))
;; prefab structs
[(-prefab 'foo -String) (-prefab 'foo -String)]
[(-prefab 'foo -String) (-prefab 'foo (-opt -String))]
[(-prefab '(bar foo 1) -String -Symbol) (-prefab 'foo -String)]
[(-prefab '(bar foo 1) -String -Symbol) (-prefab 'foo (-opt -String))]
[FAIL
(-prefab '(foo #(0)) -String) (-prefab '(foo #(0)) (-opt -String))]
[(-prefab '(foo 1 #(0)) -String -Symbol)
(-prefab '(foo #(0)) -String)]
[(-prefab '(bar foo 1 #(0)) -String -Symbol)
(-prefab '(foo #(0)) -String)]
[FAIL
(-prefab '(foo #()) -String) (-prefab '(foo #(0)) (-opt -String))]
(define-for-syntax (single-subval-test stx)
(syntax-case stx (FAIL)
[(FAIL t s) (syntax/loc stx (test-check (format "FAIL ~a" '(t s)) (lambda (a b) (not (subval a b))) t s))]
[(t s) (syntax/loc stx (test-check (format "~a" '(t s)) subval t s))]))
;; Proposition subtyping
((make-pred-ty (list -Real) -Boolean (Un (-val 0.0) (-val 0)))
(make-pred-ty (list -Int) -Boolean (-val 0)))
(define-syntax (subval-tests stx)
(syntax-case stx ()
[(_ str cl ...)
(with-syntax ([(new-cl ...) (map single-subval-test (syntax->list #'(cl ...)))])
(syntax/loc stx
(begin (test-suite (format "Tests for subval (~a)" str)
new-cl ...))))]))
(define values-tests
(subval-tests
"SomeValues"
[(-values (list -Number))
(-values (list Univ))]
[FAIL (make-ValuesDots (list) -Symbol 'a)
(make-ValuesDots (list (-result -String)) -String 'a)]
[(-values (list -Bottom))
(-values (list -String -Symbol))]
))
(define tests
(test-suite
"All Subtype Tests"
simple-tests
structural-tests
set-theoretic-type-tests
struct-tests
poly-tests
function-tests
oo-tests
values-tests
other-tests))

View File

@ -5,16 +5,23 @@
racket/gui/dynamic
typed-racket/utils/utils
(for-syntax racket/base syntax/parse)
(types utils)
(types utils subtype)
(utils tc-utils)
(typecheck check-below)
(rep type-rep)
rackunit rackunit/text-ui)
(provide private typecheck (rename-out [infer r:infer]) utils env rep types base-env static-contracts
(all-defined-out))
;; FIXME - do something more intelligent
(define (tc-result-equal/test? a b)
(equal? a b))
(define (tc-result-equal/test? res1 res2)
(define (below? res1 res2)
(parameterize ([delay-errors? #f])
(with-handlers ([exn:fail? (λ (_) #f)])
(check-below res1 res2)
#t)))
(and (below? res1 res2)
(below? res2 res1)))
(define-syntax (check-type-equal? stx)
(syntax-case stx ()

View File

@ -2,7 +2,7 @@
(require "test-utils.rkt" (for-syntax racket/base)
(rep type-rep)
(types abbrev numeric-tower union)
(types abbrev numeric-tower)
rackunit)
(provide tests)
@ -15,8 +15,8 @@
(define (single-test stx)
(syntax-case stx (FAIL)
[(FAIL t s) (syntax/loc stx (test-check (format "FAIL ~a" '(t s))
(lambda (a b) (not (type-equal? a b))) t s))]
[(t s) (syntax/loc stx (test-check (format "~a" '(t s)) type-equal? t s))]))
(lambda (a b) (not (equal? a b))) t s))]
[(t s) (syntax/loc stx (test-check (format "~a" '(t s)) equal? t s))]))
(syntax-case stx ()
[(_ cl ...)
#`(test-suite "Tests for type equality"

Some files were not shown because too many files have changed in this diff Show More