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

filter -> prop

Browse Source 
This pull request is largely a renaming effort to clean up the TR codebase. There are two primary things I wanted to change:

1. Replace all occurrences of "filter" with "prop" or "proposition"
   - The word "filter" is a meaningless opaque term at this point in the Typed Racket implementation. If anything, it just adds confusion to why things are the way the are. We should use "proposition" instead, since that's what they actually are.

2. Avoid using "Top" and "Bottom" in both the type and proposition realm.
   - Currently the top type is called Univ and the bottom type is called bottom, while the top proposition is called Top and the bottom proposition is called Bot. This is just unnecessarily confusing, doesn't really line up w/ the user-space names, and doesn't line up with the names we use in TR formalisms. Worse, all of the top types of primitive types---e.g. the type of all structs, StructTop--- use Top, so it is really easy to get confused about what name to use for these sorts of things.

With these issues in mind, I made the following changes to names:

Top -> TrueProp
Bot -> FalseProp
TypeFilter -> TypeProp
NotTypeFilter -> NotTypeProp
AndFilter -> AndProp
OrFilter -> OrProp
-filter t o -> -is-type o t
-not-filter t o -> -not-type o t
FilterSet -> PropSet
NoFilter -> #f
NoObject -> #f
-FS -> -PS
-top -> -tt
-bot -> -ff
implied-atomic? q p -> implies-atomic? p q
filter-rec-id -> prop-rec-id
-no-filter -> -no-propset
-top-filter -> -tt-propset
-bot-filter -> -ff-propset
-true-filter -> -true-propset
-false-filter -> -false-propset
PredicateFilter: -> PredicateProp:
add-unconditional-filter-all-args add-unconditional-prop-all-args
This commit is contained in:
Andrew Kent 2016-04-21 23:26:22 -04:00
parent e855755349
commit f9c5a534d0
70 changed files with 1888 additions and 1948 deletions

26
typed-racket-doc/typed-racket/scribblings/guide/occurrence.scrbl
View File

@ -51,7 +51,7 @@ have based on a predicate check in a conditional expression, it can
narrow the type of the variable within the appropriate branch of the
conditional.
@section[#:tag "filters-and-predicates"]{Filters and Predicates}
@section[#:tag "propositions-and-predicates"]{Propositions and Predicates}
In the previous section, we demonstrated that a Typed Racket programmer
can take advantage of occurrence typing to type-check functions
@ -59,7 +59,7 @@ with union types and conditionals. This may raise the question: how
does Typed Racket know how to narrow the type based on the predicate?
The answer is that predicate types in Typed Racket are annotated
with @deftech{filters} that tell the typechecker what additional
with logical @deftech{propositions} that tell the typechecker what additional
information is gained when a predicate check succeeds or fails.
For example, consider the REPL's type printout for @racket[string?]:
@ -69,16 +69,20 @@ For example, consider the REPL's type printout for @racket[string?]:
The type @racket[(-> Any Boolean : String)] has three parts. The first
two are the same as any other function type and indicate that the
predicate takes any value and returns a boolean. The third part, after
the @racket[_:], is a @tech{filter} that tells the typechecker two
things:
the @racket[_:], represents the logical @tech{propositions}
the typechecker learns from the result of applying the function:
@itemlist[#:style 'ordered
@item{If the predicate check succeeds, the argument variable has type @racket[String]}
@item{If the predicate check fails, the argument variable @emph{does not} have type @racket[String]}
]
Predicates for all built-in types are annotated with similar filters
that allow the type system to reason about predicate checks.
@item{If the predicate check succeeds (i.e. produces a
non-@racket[#f] value), the argument variable has type
@racket[String]}
@item{If the predicate check fails (i.e. produces @racket[#f]), the
argument variable @emph{does not} have type @racket[String]} ]
Predicates for all built-in types are annotated with similar propositions
that allow the type system to reason logically about predicate checks.
@section{Other conditionals and assertions}
@ -124,8 +128,8 @@ using an @emph{assertion}. For example,
(define d (assert (- b a) positive?))
]
Using the filter on @racket[positive?], Typed Racket can assign the
type @racket[Positive-Integer] to the whole @racket[assert]
Using the logical propositions on @racket[positive?], Typed Racket can
assign the type @racket[Positive-Integer] to the whole @racket[assert]
expression. This type-checks, but note that the assertion may raise
an exception at run-time if the predicate returns @racket[#f].

10
typed-racket-doc/typed-racket/scribblings/internals.txt
View File

@ -1,17 +1,17 @@
Data Structures used in Typechecking.
The main data structure used in typechecking is a tc-results/c.
This currently has two variants
(struct/c tc-results ((listof (struct/c tc-result (Type/c FilterSet? Object?)))
(struct/c tc-results ((listof (struct/c tc-result (Type/c PropSet? Object?)))
(or/c #f (cons/c Type/c symbol?))))
(struct/c tc-any-results (or/c Filter/c NoFilter?))
(struct/c tc-any-results (or/c Prop? #f))
The first represents a fixed number of values with optional dotted return values.
The second represents an unknown number of values.
A value has three main parts: a Type, a FilterSet, and an Object. For dotted values we do no store a
FilterSet or an Object because they would almost never be useful. They are thus implicitly -top-filter
A value has three main parts: a Type, a PropSet, and an Object. For dotted values we do no store a
PropSet or an Object because they would almost never be useful. They are thus implicitly -tt-propset
and -empty-obj. In the tc-any-results case since we don't know the number of values, we do not store
the Type or the Object, but we do store a filter. This is useful in cases like
the Type or the Object, but we do store a proposition. This is useful in cases like
(let ((x (read)))
(unless (number? x) (error 'bad-input))
(do-stuff x))

56
typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
View File

@ -568,29 +568,33 @@ functions and continuation mark functions.
@section{Other Type Constructors}
@defform*/subs[#:id -> #:literals (|@| * ... ! and or implies car cdr)
[(-> dom ... rng optional-filter)
[(-> dom ... rng opt-proposition)
(-> dom ... rest * rng)
(-> dom ... rest ooo bound rng)
(dom ... -> rng optional-filter)
(dom ... -> rng opt-proposition)
(dom ... rest * -> rng)
(dom ... rest ooo bound -> rng)]
([ooo #,(racket ...)]
[dom type
mandatory-kw
optional-kw]
opt-kw]
[mandatory-kw (code:line keyword type)]
[optional-kw [keyword type]]
[optional-filter (code:line)
[opt-kw [keyword type]]
[opt-proposition (code:line)
(code:line : type)
(code:line : pos-filter neg-filter object)]
[pos-filter (code:line)
(code:line #:+ proposition ...)]
[neg-filter (code:line)
(code:line #:- proposition ...)]
(code:line : pos-proposition
neg-proposition
object)]
[pos-proposition (code:line)
(code:line #:+ proposition ...)]
[neg-proposition (code:line)
(code:line #:- proposition ...)]
[object (code:line)
(code:line #:object index)]
[proposition type
[proposition Top
Bot
type
(! type)
(type |@| path-elem ... index)
(! type |@| path-elem ... index)
@ -629,20 +633,24 @@ functions and continuation mark functions.
(is-zero? 2 #:equality =)
(is-zero? 2 #:equality eq? #:zero 2.0)]
When @racket[optional-filter] is provided, it specifies the @emph{filter} for the
function type (for an introduction to filters, see @tr-guide-secref["filters-and-predicates"]).
For almost all use cases, only the simplest form of filters, with a single type after a
When @racket[opt-proposition] is provided, it specifies the
@emph{proposition} for the function type (for an introduction to
propositions in Typed Racket, see
@tr-guide-secref["propositions-and-predicates"]). For almost all use
cases, only the simplest form of propositions, with a single type after a
@racket[:], are necessary:
@ex[string?]
The filter specifies that when @racket[(string? x)] evaluates to a true value for
a conditional branch, the variable @racket[x] in that branch can be assumed to have
type @racket[String]. Likewise, if the expression evaluates to @racket[#f] in a branch,
the variable @emph{does not} have type @racket[String].
The proposition specifies that when @racket[(string? x)] evaluates to a
true value for a conditional branch, the variable @racket[x] in that
branch can be assumed to have type @racket[String]. Likewise, if the
expression evaluates to @racket[#f] in a branch, the variable
@emph{does not} have type @racket[String].
In some cases, asymmetric type information is useful in filters. For example, the
@racket[filter] function's first argument is specified with only a positive filter:
In some cases, asymmetric type information is useful in the
propositions. For example, the @racket[filter] function's first
argument is specified with only a positive proposition:
@ex[filter]
@ -653,7 +661,7 @@ functions and continuation mark functions.
Conversely, @racket[#:-] specifies that a function provides information for the
false branch of a conditional.
The other filter proposition cases are rarely needed, but the grammar documents them
The other proposition cases are rarely needed, but the grammar documents them
for completeness. They correspond to logical operations on the propositions.
The type of functions can also be specified with an @emph{infix} @racket[->]
@ -710,9 +718,9 @@ functions and continuation mark functions.
@deftogether[(
@defidform[Top]
@defidform[Bot])]{ These are filters that can be used with @racket[->].
@racket[Top] is the filter with no information.
@racket[Bot] is the filter which means the result cannot happen.
@defidform[Bot])]{ These are propositions that can be used with @racket[->].
@racket[Top] is the propositions with no information.
@racket[Bot] is the propositions which means the result cannot happen.
}

702
typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt
View File

@ -41,11 +41,11 @@
;; for fixnum-specific operations. if they return at all, we know
;; their args were fixnums. otherwise, an error would have been thrown
;; for the moment, this is only useful if the result is used as a test
;; once we have a set of filters that are true/false based on reaching
;; once we have a set of props that are true/false based on reaching
;; a certain point, this will be more useful
(define (fx-from-cases . cases)
(apply from-cases (map (lambda (x)
(add-unconditional-filter-all-args
(add-unconditional-prop-all-args
x -Fixnum))
(flatten cases))))
@ -70,14 +70,14 @@
(-> t1 t2 B))
;; simple case useful with equality predicates.
;; if the equality is true, we know that general arg is in fact of specific type.
(define (commutative-equality/filter general specific)
(list (-> general specific B : (-FS (-filter specific 0) -top))
(-> specific general B : (-FS (-filter specific 1) -top))))
(define (commutative-equality/prop general specific)
(list (-> general specific B : (-PS (-is-type 0 specific) -tt))
(-> specific general B : (-PS (-is-type 1 specific) -tt))))
;; if in addition if the equality is false, we know that general arg is not of the specific type.
(define (commutative-equality/strict-filter general specific)
(list (-> general specific B : (-FS (-filter specific 0) (-not-filter specific 0)))
(-> specific general B : (-FS (-filter specific 1) (-not-filter specific 1)))))
(define (commutative-equality/strict-prop general specific)
(list (-> general specific B : (-PS (-is-type 0 specific) (-not-type 0 specific)))
(-> specific general B : (-PS (-is-type 1 specific) (-not-type 1 specific)))))
(define round-type ; also used for truncate
@ -118,8 +118,8 @@
(define fx+-type
(lambda ()
(fx-from-cases
(-> -Zero -Int -Fixnum : -true-filter : (-arg-path 1))
(-> -Int -Zero -Fixnum : -true-filter : (-arg-path 0))
(-> -Zero -Int -Fixnum : -true-propset : (-arg-path 1))
(-> -Int -Zero -Fixnum : -true-propset : (-arg-path 0))
(commutative-binop -PosByte -Byte -PosIndex)
(binop -Byte -Index)
;; in other cases, either we stay within fixnum range, or we error
@ -132,7 +132,7 @@
(define fx--type
(lambda ()
(fx-from-cases
(-> -Int -Zero -Fixnum : -true-filter : (-arg-path 0))
(-> -Int -Zero -Fixnum : -true-propset : (-arg-path 0))
(-One -One . -> . -Zero)
(-PosByte -One . -> . -Byte)
(-PosIndex -One . -> . -Index)
@ -147,8 +147,8 @@
(define fx*-type
(lambda ()
(fx-from-cases
(-> -One -Int -Fixnum : -true-filter : (-arg-path 1))
(-> -Int -One -Fixnum : -true-filter : (-arg-path 0))
(-> -One -Int -Fixnum : -true-propset : (-arg-path 1))
(-> -Int -One -Fixnum : -true-propset : (-arg-path 0))
(commutative-binop -Int -Zero)
(-PosByte -PosByte . -> . -PosIndex)
(-Byte -Byte . -> . -Index)
@ -163,7 +163,7 @@
(lambda ()
(fx-from-cases
(-Zero -Int . -> . -Zero)
(-> -Int -One -Fixnum : -true-filter : (-arg-path 0))
(-> -Int -One -Fixnum : -true-propset : (-arg-path 0))
(-Byte -Nat . -> . -Byte)
(-Index -Nat . -> . -Index)
(-Nat -Nat . -> . -NonNegFixnum)
@ -193,133 +193,133 @@
(define fxabs-type
(lambda ()
(fx-from-cases
(-> -Nat -NonNegFixnum : -true-filter : (-arg-path 0))
(-> -Nat -NonNegFixnum : -true-propset : (-arg-path 0))
((Un -PosInt -NegInt) . -> . -PosFixnum)
(-Int . -> . -NonNegFixnum))))
(define fx=-type
(lambda ()
(fx-from-cases
;; we could rule out cases like (= Pos Neg), but we currently don't
(commutative-equality/strict-filter -Int -Zero)
(map (lambda (t) (commutative-equality/filter -Int t))
(commutative-equality/strict-prop -Int -Zero)
(map (lambda (t) (commutative-equality/prop -Int t))
(list -One -PosByte -Byte -PosIndex -Index -PosFixnum -NonNegFixnum -NegFixnum -NonPosFixnum))
(comp -Int))))
(define fx<-type
(lambda ()
(fx-from-cases
(-> -Int -One B : (-FS (-filter -NonPosFixnum 0) (-filter -PosFixnum 0)))
(-> -Int -Zero B : (-FS (-filter -NegFixnum 0) (-filter -NonNegFixnum 0)))
(-> -Zero -Int B : (-FS (-filter -PosFixnum 1) (-filter -NonPosFixnum 1)))
(-> -Int -One B : (-PS (-is-type 0 -NonPosFixnum) (-is-type 0 -PosFixnum)))
(-> -Int -Zero B : (-PS (-is-type 0 -NegFixnum) (-is-type 0 -NonNegFixnum)))
(-> -Zero -Int B : (-PS (-is-type 1 -PosFixnum) (-is-type 1 -NonPosFixnum)))
(-> -Byte -PosByte B : (-FS -top (-filter -PosByte 0)))
(-> -Byte -Byte B : (-FS (-filter -PosByte 1) -top))
(-> -Pos -Byte B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top))
(-> -Byte -Pos B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1))))
(-> -Byte -Nat B : (-FS -top (-filter -Byte 1)))
(-> -Index -PosIndex B : (-FS -top (-filter -PosIndex 0)))
(-> -Index -Index B : (-FS (-filter -PosIndex 1) -top))
(-> -Pos -Index B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top))
(-> -Index -Pos B : (-FS -top (-and (-filter -PosIndex 0) (-filter -PosIndex 1))))
(-> -Nat -Byte B : (-FS (-and (-filter -Byte 0) (-filter -PosByte 1)) -top))
(-> -Nat -Index B : (-FS (-and (-filter -Index 0) (-filter -PosIndex 1)) -top))
(-> -Index -Nat B : (-FS -top (-filter -Index 1)))
(-> -Byte -PosByte B : (-PS -tt (-is-type 0 -PosByte)))
(-> -Byte -Byte B : (-PS (-is-type 1 -PosByte) -tt))
(-> -Pos -Byte B : (-PS (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte)) -tt))
(-> -Byte -Pos B : (-PS -tt (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte))))
(-> -Byte -Nat B : (-PS -tt (-is-type 1 -Byte)))
(-> -Index -PosIndex B : (-PS -tt (-is-type 0 -PosIndex)))
(-> -Index -Index B : (-PS (-is-type 1 -PosIndex) -tt))
(-> -Pos -Index B : (-PS (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex)) -tt))
(-> -Index -Pos B : (-PS -tt (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex))))
(-> -Nat -Byte B : (-PS (-and (-is-type 0 -Byte) (-is-type 1 -PosByte)) -tt))
(-> -Nat -Index B : (-PS (-and (-is-type 0 -Index) (-is-type 1 -PosIndex)) -tt))
(-> -Index -Nat B : (-PS -tt (-is-type 1 -Index)))
;; general integer cases
(-> -Int -PosInt B : (-FS -top (-filter -PosFixnum 0)))
(-> -Int -Nat B : (-FS -top (-filter -NonNegFixnum 0)))
(-> -Nat -Int B : (-FS (-filter -PosFixnum 1) -top))
(-> -Int -NonPosInt B : (-FS (-filter -NegFixnum 0) -top))
(-> -NegInt -Int B : (-FS -top (-filter -NegFixnum 1)))
(-> -NonPosInt -Int B : (-FS -top (-filter -NonPosFixnum 1)))
(-> -Int -PosInt B : (-PS -tt (-is-type 0 -PosFixnum)))
(-> -Int -Nat B : (-PS -tt (-is-type 0 -NonNegFixnum)))
(-> -Nat -Int B : (-PS (-is-type 1 -PosFixnum) -tt))
(-> -Int -NonPosInt B : (-PS (-is-type 0 -NegFixnum) -tt))
(-> -NegInt -Int B : (-PS -tt (-is-type 1 -NegFixnum)))
(-> -NonPosInt -Int B : (-PS -tt (-is-type 1 -NonPosFixnum)))
(comp -Int))))
(define fx>-type
(lambda ()
(fx-from-cases
(-> -One -Int B : (-FS (-filter -NonPosFixnum 1) (-filter -PosFixnum 1)))
(-> -Zero -Int B : (-FS (-filter -NegFixnum 1) (-filter -NonNegFixnum 1)))
(-> -Int -Zero B : (-FS (-filter -PosFixnum 0) (-filter -NonPosFixnum 0)))
(-> -One -Int B : (-PS (-is-type 1 -NonPosFixnum) (-is-type 1 -PosFixnum)))
(-> -Zero -Int B : (-PS (-is-type 1 -NegFixnum) (-is-type 1 -NonNegFixnum)))
(-> -Int -Zero B : (-PS (-is-type 0 -PosFixnum) (-is-type 0 -NonPosFixnum)))
(-> -PosByte -Byte B : (-FS -top (-filter -PosByte 1)))
(-> -Byte -Byte B : (-FS (-filter -PosByte 0) -top))
(-> -Byte -Pos B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top))
(-> -Pos -Byte B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1))))
(-> -Byte -Nat B : (-FS (-and (-filter -PosByte 0) (-filter -Byte 1)) -top))
(-> -PosIndex -Index B : (-FS -top (-filter -PosIndex 1)))
(-> -Index -Index B : (-FS (-filter -PosIndex 0) -top))
(-> -Index -Pos B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top))
(-> -Pos -Index B : (-FS -top (-and (-filter -PosIndex 0) (-filter -PosIndex 1))))
(-> -Index -Nat B : (-FS (-and (-filter -PosIndex 0) (-filter -Index 1)) -top))
(-> -Nat -Byte B : (-FS -top (-filter -Byte 0)))
(-> -Nat -Index B : (-FS -top (-filter -Index 0)))
(-> -PosByte -Byte B : (-PS -tt (-is-type 1 -PosByte)))
(-> -Byte -Byte B : (-PS (-is-type 0 -PosByte) -tt))
(-> -Byte -Pos B : (-PS (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte)) -tt))
(-> -Pos -Byte B : (-PS -tt (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte))))
(-> -Byte -Nat B : (-PS (-and (-is-type 0 -PosByte) (-is-type 1 -Byte)) -tt))
(-> -PosIndex -Index B : (-PS -tt (-is-type 1 -PosIndex)))
(-> -Index -Index B : (-PS (-is-type 0 -PosIndex) -tt))
(-> -Index -Pos B : (-PS (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex)) -tt))
(-> -Pos -Index B : (-PS -tt (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex))))
(-> -Index -Nat B : (-PS (-and (-is-type 0 -PosIndex) (-is-type 1 -Index)) -tt))
(-> -Nat -Byte B : (-PS -tt (-is-type 0 -Byte)))
(-> -Nat -Index B : (-PS -tt (-is-type 0 -Index)))
;; general integer cases
(-> -PosInt -Int B : (-FS -top (-filter -PosFixnum 1)))
(-> -Nat -Int B : (-FS -top (-filter -NonNegFixnum 1)))
(-> -Int -Nat B : (-FS (-filter -PosFixnum 0) -top))
(-> -NonPosInt -Int B : (-FS (-filter -NegFixnum 1) -top))
(-> -Int -NegInt B : (-FS -top (-filter -NegFixnum 0)))
(-> -Int -NonPosInt B : (-FS -top (-filter -NonPosFixnum 0)))
(-> -PosInt -Int B : (-PS -tt (-is-type 1 -PosFixnum)))
(-> -Nat -Int B : (-PS -tt (-is-type 1 -NonNegFixnum)))
(-> -Int -Nat B : (-PS (-is-type 0 -PosFixnum) -tt))
(-> -NonPosInt -Int B : (-PS (-is-type 1 -NegFixnum) -tt))
(-> -Int -NegInt B : (-PS -tt (-is-type 0 -NegFixnum)))
(-> -Int -NonPosInt B : (-PS -tt (-is-type 0 -NonPosFixnum)))
(comp -Int))))
(define fx<=-type
(lambda ()
(fx-from-cases
(-> -Int -One B : (-FS (-filter (Un -NonPosFixnum -One) 0) (-filter -PosFixnum 0)))
(-> -One -Int B : (-FS (-filter -PosFixnum 1) (-filter -NonPosFixnum 1)))
(-> -Int -Zero B : (-FS (-filter -NonPosFixnum 0) (-filter -PosFixnum 0)))
(-> -Zero -Int B : (-FS (-filter -NonNegFixnum 1) (-filter -NegFixnum 1)))
(-> -Int -One B : (-PS (-is-type 0 (Un -NonPosFixnum -One)) (-is-type 0 -PosFixnum)))
(-> -One -Int B : (-PS (-is-type 1 -PosFixnum) (-is-type 1 -NonPosFixnum)))
(-> -Int -Zero B : (-PS (-is-type 0 -NonPosFixnum) (-is-type 0 -PosFixnum)))
(-> -Zero -Int B : (-PS (-is-type 1 -NonNegFixnum) (-is-type 1 -NegFixnum)))
(-> -PosByte -Byte B : (-FS (-filter -PosByte 1) -top))
(-> -Byte -Byte B : (-FS -top (-filter -PosByte 0)))
(-> -Pos -Byte B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top))
(-> -Byte -Pos B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1))))
(-> -Byte -Nat B : (-FS -top (-and (-filter -PosByte 0) (-filter -Byte 1))))
(-> -PosIndex -Index B : (-FS (-filter -PosIndex 1) -top))
(-> -Index -Index B : (-FS -top (-filter -PosIndex 0)))
(-> -Pos -Index B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top))
(-> -Index -Pos B : (-FS -top (-and (-filter -PosIndex 0) (-filter -PosIndex 1))))
(-> -Nat -Byte B : (-FS (-filter -Byte 0) -top))
(-> -Nat -Index B : (-FS (-filter -Index 0) -top))
(-> -Index -Nat B : (-FS -top (-and (-filter -PosIndex 0) (-filter -Index 1))))
(-> -PosByte -Byte B : (-PS (-is-type 1 -PosByte) -tt))
(-> -Byte -Byte B : (-PS -tt (-is-type 0 -PosByte)))
(-> -Pos -Byte B : (-PS (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte)) -tt))
(-> -Byte -Pos B : (-PS -tt (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte))))
(-> -Byte -Nat B : (-PS -tt (-and (-is-type 0 -PosByte) (-is-type 1 -Byte))))
(-> -PosIndex -Index B : (-PS (-is-type 1 -PosIndex) -tt))
(-> -Index -Index B : (-PS -tt (-is-type 0 -PosIndex)))
(-> -Pos -Index B : (-PS (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex)) -tt))
(-> -Index -Pos B : (-PS -tt (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex))))
(-> -Nat -Byte B : (-PS (-is-type 0 -Byte) -tt))
(-> -Nat -Index B : (-PS (-is-type 0 -Index) -tt))
(-> -Index -Nat B : (-PS -tt (-and (-is-type 0 -PosIndex) (-is-type 1 -Index))))
;; general integer cases
(-> -PosInt -Int B : (-FS (-filter -PosFixnum 1) -top))
(-> -Int -Nat B : (-FS -top (-filter -PosFixnum 0)))
(-> -Nat -Int B : (-FS (-filter -NonNegFixnum 1) -top))
(-> -Int -NegInt B : (-FS (-filter -NegFixnum 0) -top))
(-> -Int -NonPosInt B : (-FS (-filter -NonPosFixnum 0) -top))
(-> -NonPosInt -Int B : (-FS -top (-filter -NegFixnum 1)))
(-> -PosInt -Int B : (-PS (-is-type 1 -PosFixnum) -tt))
(-> -Int -Nat B : (-PS -tt (-is-type 0 -PosFixnum)))
(-> -Nat -Int B : (-PS (-is-type 1 -NonNegFixnum) -tt))
(-> -Int -NegInt B : (-PS (-is-type 0 -NegFixnum) -tt))
(-> -Int -NonPosInt B : (-PS (-is-type 0 -NonPosFixnum) -tt))
(-> -NonPosInt -Int B : (-PS -tt (-is-type 1 -NegFixnum)))
(comp -Int))))
(define fx>=-type
(lambda ()
(fx-from-cases
(-> -One -Int B : (-FS (-filter (Un -One -NonPosInt) 1) (-filter -PosFixnum 1)))
(-> -Int -One B : (-FS (-filter -PosFixnum 0) (-filter -NonPosFixnum 0)))
(-> -Zero -Int B : (-FS (-filter -NonPosFixnum 1) (-filter -PosFixnum 1)))
(-> -Int -Zero B : (-FS (-filter -NonNegFixnum 0) (-filter -NegFixnum 0)))
(-> -One -Int B : (-PS (-is-type 1 (Un -One -NonPosInt)) (-is-type 1 -PosFixnum)))
(-> -Int -One B : (-PS (-is-type 0 -PosFixnum) (-is-type 0 -NonPosFixnum)))
(-> -Zero -Int B : (-PS (-is-type 1 -NonPosFixnum) (-is-type 1 -PosFixnum)))
(-> -Int -Zero B : (-PS (-is-type 0 -NonNegFixnum) (-is-type 0 -NegFixnum)))
(-> -Byte -PosByte B : (-FS (-filter -PosByte 0) -top))
(-> -Byte -Byte B : (-FS -top (-filter -PosByte 1)))
(-> -Byte -Pos B : (-FS (-and (-filter -PosByte 1) (-filter -PosByte 0)) -top))
(-> -Pos -Byte B : (-FS -top (-and (-filter -PosByte 1) (-filter -PosByte 0))))
(-> -Byte -Nat B : (-FS (-filter -Byte 1) -top))
(-> -Zero -Index B : (-FS (-filter -Zero 1) (-filter -PosIndex 1)))
(-> -Index -PosIndex B : (-FS (-filter -PosIndex 0) -top))
(-> -Index -Index B : (-FS -top (-filter -PosIndex 1)))
(-> -Index -Pos B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top))
(-> -Pos -Index B : (-FS -top (-and (-filter -PosIndex 0) (-filter -PosIndex 1))))
(-> -Index -Nat B : (-FS (-filter -Index 1) -top))
(-> -Nat -Byte B : (-FS -top (-and (-filter -Byte 0) (-filter -PosByte 1))))
(-> -Nat -Index B : (-FS -top (-and (-filter -Index 0) (-filter -PosIndex 1))))
(-> -Byte -PosByte B : (-PS (-is-type 0 -PosByte) -tt))
(-> -Byte -Byte B : (-PS -tt (-is-type 1 -PosByte)))
(-> -Byte -Pos B : (-PS (-and (-is-type 1 -PosByte) (-is-type 0 -PosByte)) -tt))
(-> -Pos -Byte B : (-PS -tt (-and (-is-type 1 -PosByte) (-is-type 0 -PosByte))))
(-> -Byte -Nat B : (-PS (-is-type 1 -Byte) -tt))
(-> -Zero -Index B : (-PS (-is-type 1 -Zero) (-is-type 1 -PosIndex)))
(-> -Index -PosIndex B : (-PS (-is-type 0 -PosIndex) -tt))
(-> -Index -Index B : (-PS -tt (-is-type 1 -PosIndex)))
(-> -Index -Pos B : (-PS (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex)) -tt))
(-> -Pos -Index B : (-PS -tt (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex))))
(-> -Index -Nat B : (-PS (-is-type 1 -Index) -tt))
(-> -Nat -Byte B : (-PS -tt (-and (-is-type 0 -Byte) (-is-type 1 -PosByte))))
(-> -Nat -Index B : (-PS -tt (-and (-is-type 0 -Index) (-is-type 1 -PosIndex))))
;; general integer cases
(-> -Int -PosInt B : (-FS (-filter -PosFixnum 0) -top))
(-> -Nat -Int B : (-FS -top (-filter -PosFixnum 1)))
(-> -Int -Nat B : (-FS (-filter -NonNegFixnum 0) -top))
(-> -NegInt -Int B : (-FS (-filter -NegFixnum 1) -top))
(-> -NonPosInt -Int B : (-FS (-filter -NonPosFixnum 1) -top))
(-> -Int -NonPosInt B : (-FS -top (-filter -NegFixnum 0)))
(-> -Int -PosInt B : (-PS (-is-type 0 -PosFixnum) -tt))
(-> -Nat -Int B : (-PS -tt (-is-type 1 -PosFixnum)))
(-> -Int -Nat B : (-PS (-is-type 0 -NonNegFixnum) -tt))
(-> -NegInt -Int B : (-PS (-is-type 1 -NegFixnum) -tt))
(-> -NonPosInt -Int B : (-PS (-is-type 1 -NonPosFixnum) -tt))
(-> -Int -NonPosInt B : (-PS -tt (-is-type 0 -NegFixnum)))
(comp -Int))))
(define fxmin-type
(lambda ()
(fx-from-cases
(-> -Nat -NonPosInt -NonPosFixnum : -true-filter : (-arg-path 1))
(-> -NonPosInt -Nat -NonPosFixnum : -true-filter : (-arg-path 0))
(-> -Nat -NonPosInt -NonPosFixnum : -true-propset : (-arg-path 1))
(-> -NonPosInt -Nat -NonPosFixnum : -true-propset : (-arg-path 0))
(-> -Zero -Int -NonPosFixnum)
(-> -Int -Zero -NonPosFixnum)
@ -335,8 +335,8 @@
(define fxmax-type
(lambda ()
(fx-from-cases
(-> -NonPosInt -Nat -NonNegFixnum : -true-filter : (-arg-path 1))
(-> -Nat -NonPosInt -NonNegFixnum : -true-filter : (-arg-path 0))
(-> -NonPosInt -Nat -NonNegFixnum : -true-propset : (-arg-path 1))
(-> -Nat -NonPosInt -NonNegFixnum : -true-propset : (-arg-path 0))
(-> -Zero -Int -NonNegFixnum)
(-> -Int -Zero -NonNegFixnum)
@ -360,8 +360,8 @@
(define fxior-type
(lambda ()
(fx-from-cases
(-> -Zero -Int -Fixnum : -true-filter : (-arg-path 1))
(-> -Int -Zero -Fixnum : -true-filter : (-arg-path 0))
(-> -Zero -Int -Fixnum : -true-propset : (-arg-path 1))
(-> -Int -Zero -Fixnum : -true-propset : (-arg-path 0))
(commutative-binop -PosByte -Byte -PosByte)
(binop -Byte)
@ -374,8 +374,8 @@
(define fxxor-type
(lambda ()
(fx-from-cases
(-> -Zero -Int -Fixnum : -true-filter : (-arg-path 1))
(-> -Int -Zero -Fixnum : -true-filter : (-arg-path 0))
(-> -Zero -Int -Fixnum : -true-propset : (-arg-path 1))
(-> -Int -Zero -Fixnum : -true-propset : (-arg-path 0))
(binop -One -Zero)
(binop -Byte)
@ -394,7 +394,7 @@
(define fxlshift-type
(lambda ()
(fx-from-cases
(-> -Int -Zero -Fixnum : -true-filter : (-arg-path 0))
(-> -Int -Zero -Fixnum : -true-propset : (-arg-path 0))
(-> -PosInt -Int -PosFixnum) ; negative 2nd arg errors, so we can't reach 0
(-> -Nat -Int -NonNegFixnum)
(-> -NegInt -Int -NegFixnum)
@ -403,7 +403,7 @@
(define fxrshift-type
(lambda ()
(fx-from-cases
(-> -Int -Zero -Fixnum : -true-filter : (-arg-path 0))
(-> -Int -Zero -Fixnum : -true-propset : (-arg-path 0))
(-> -Nat -Int -NonNegFixnum) ; can reach 0
(-> -NegInt -Int -NegFixnum) ; can't reach 0
(-> -NonPosInt -Int -NonPosFixnum)
@ -495,8 +495,8 @@
(binop -Fl))))
(define fl=-type
(fl-type-lambda
(from-cases (commutative-equality/strict-filter -Fl (Un -FlPosZero -FlNegZero))
(map (lambda (t) (commutative-equality/filter -Fl t))
(from-cases (commutative-equality/strict-prop -Fl (Un -FlPosZero -FlNegZero))
(map (lambda (t) (commutative-equality/prop -Fl t))
(list -FlZero -PosFl -NonNegFl
-NegFl -NonPosFl))
(comp -Fl))))
@ -504,30 +504,30 @@
(fl-type-lambda
(from-cases
;; false case, we know nothing, lhs may be NaN. same for all comparison that can involve floats
(-> -NonNegFl -Fl B : (-FS (-filter -PosFl 1) -top))
(-> -Fl -NonPosFl B : (-FS (-filter -NegFl 0) -top))
(-> -NonNegFl -Fl B : (-PS (-is-type 1 -PosFl) -tt))
(-> -Fl -NonPosFl B : (-PS (-is-type 0 -NegFl) -tt))
(comp -Fl))))
(define fl>-type
(fl-type-lambda
(from-cases
(-> -NonPosFl -Fl B : (-FS (-filter -NegFl 1) -top))
(-> -Fl -NonNegFl B : (-FS (-filter -PosFl 0) -top))
(-> -NonPosFl -Fl B : (-PS (-is-type 1 -NegFl) -tt))
(-> -Fl -NonNegFl B : (-PS (-is-type 0 -PosFl) -tt))
(comp -Fl))))
(define fl<=-type
(fl-type-lambda
(from-cases
(-> -PosFl -Fl B : (-FS (-filter -PosFl 1) -top))
(-> -NonNegFl -Fl B : (-FS (-filter -NonNegFl 1) -top))
(-> -Fl -NegFl B : (-FS (-filter -NegFl 0) -top))
(-> -Fl -NonPosFl B : (-FS (-filter -NonPosFl 0) -top))
(-> -PosFl -Fl B : (-PS (-is-type 1 -PosFl) -tt))
(-> -NonNegFl -Fl B : (-PS (-is-type 1 -NonNegFl) -tt))
(-> -Fl -NegFl B : (-PS (-is-type 0 -NegFl) -tt))
(-> -Fl -NonPosFl B : (-PS (-is-type 0 -NonPosFl) -tt))
(comp -Fl))))
(define fl>=-type
(fl-type-lambda
(from-cases
(-> -Fl -PosFl B : (-FS (-filter -PosFl 0) -top))
(-> -Fl -NonNegFl B : (-FS (-filter -NonNegFl 0) -top))
(-> -NegFl -Fl B : (-FS (-filter -NegFl 1) -top))
(-> -NonPosFl -Fl B : (-FS (-filter -NonPosFl 1) -top))
(-> -Fl -PosFl B : (-PS (-is-type 0 -PosFl) -tt))
(-> -Fl -NonNegFl B : (-PS (-is-type 0 -NonNegFl) -tt))
(-> -NegFl -Fl B : (-PS (-is-type 1 -NegFl) -tt))
(-> -NonPosFl -Fl B : (-PS (-is-type 1 -NonPosFl) -tt))
(comp -Fl))))
(define flmin-type
(fl-type-lambda
@ -595,44 +595,44 @@
(define flrandom-type (lambda () (-Pseudo-Random-Generator . -> . -Flonum)))
;; There's a repetitive pattern in the types of each comparison operator.
;; As explained below, this is because filters don't do intersections.
;; As explained below, this is because props don't do intersections.
(define (<-type-pattern base pos non-neg neg non-pos [zero -RealZero])
(list (-> base zero B : (-FS (-filter neg 0) (-filter non-neg 0)))
(-> zero base B : (-FS (-filter pos 1) (-filter non-pos 1)))
(-> base -PosReal B : (-FS -top (-filter pos 0)))
(-> base -NonNegReal B : (-FS -top (-filter non-neg 0)))
(-> -NonNegReal base B : (-FS (-filter pos 1) -top))
(-> base -NonPosReal B : (-FS (-filter neg 0) -top))
(-> -NegReal base B : (-FS -top (-filter neg 1)))
(-> -NonPosReal base B : (-FS -top (-filter non-pos 1)))))
(list (-> base zero B : (-PS (-is-type 0 neg) (-is-type 0 non-neg)))
(-> zero base B : (-PS (-is-type 1 pos) (-is-type 1 non-pos)))
(-> base -PosReal B : (-PS -tt (-is-type 0 pos)))
(-> base -NonNegReal B : (-PS -tt (-is-type 0 non-neg)))
(-> -NonNegReal base B : (-PS (-is-type 1 pos) -tt))
(-> base -NonPosReal B : (-PS (-is-type 0 neg) -tt))
(-> -NegReal base B : (-PS -tt (-is-type 1 neg)))
(-> -NonPosReal base B : (-PS -tt (-is-type 1 non-pos)))))
(define (>-type-pattern base pos non-neg neg non-pos [zero -RealZero])
(list (-> base zero B : (-FS (-filter pos 0) (-filter non-pos 0)))
(-> zero base B : (-FS (-filter neg 1) (-filter non-neg 1)))
(-> base -NonNegReal B : (-FS (-filter pos 0) -top))
(-> -PosReal base B : (-FS -top (-filter pos 1)))
(-> -NonNegReal base B : (-FS -top (-filter non-neg 1)))
(-> -NonPosReal base B : (-FS (-filter neg 1) -top))
(-> base -NegReal B : (-FS -top (-filter neg 0)))
(-> base -NonPosReal B : (-FS -top (-filter non-pos 0)))))
;; this is > with flipped filters
(list (-> base zero B : (-PS (-is-type 0 pos) (-is-type 0 non-pos)))
(-> zero base B : (-PS (-is-type 1 neg) (-is-type 1 non-neg)))
(-> base -NonNegReal B : (-PS (-is-type 0 pos) -tt))
(-> -PosReal base B : (-PS -tt (-is-type 1 pos)))
(-> -NonNegReal base B : (-PS -tt (-is-type 1 non-neg)))
(-> -NonPosReal base B : (-PS (-is-type 1 neg) -tt))
(-> base -NegReal B : (-PS -tt (-is-type 0 neg)))
(-> base -NonPosReal B : (-PS -tt (-is-type 0 non-pos)))))
;; this is > with flipped props
(define (<=-type-pattern base pos non-neg neg non-pos [zero -RealZero])
(list (-> base zero B : (-FS (-filter non-pos 0) (-filter pos 0)))
(-> zero base B : (-FS (-filter non-neg 1) (-filter neg 1)))
(-> base -NonNegReal B : (-FS -top (-filter pos 0)))
(-> -PosReal base B : (-FS (-filter pos 1) -top))
(-> -NonNegReal base B : (-FS (-filter non-neg 1) -top))
(-> -NonPosReal base B : (-FS -top (-filter neg 1)))
(-> base -NegReal B : (-FS (-filter neg 0) -top))
(-> base -NonPosReal B : (-FS (-filter non-pos 0) -top))))
(list (-> base zero B : (-PS (-is-type 0 non-pos) (-is-type 0 pos)))
(-> zero base B : (-PS (-is-type 1 non-neg) (-is-type 1 neg)))
(-> base -NonNegReal B : (-PS -tt (-is-type 0 pos)))
(-> -PosReal base B : (-PS (-is-type 1 pos) -tt))
(-> -NonNegReal base B : (-PS (-is-type 1 non-neg) -tt))
(-> -NonPosReal base B : (-PS -tt (-is-type 1 neg)))
(-> base -NegReal B : (-PS (-is-type 0 neg) -tt))
(-> base -NonPosReal B : (-PS (-is-type 0 non-pos) -tt))))
(define (>=-type-pattern base pos non-neg neg non-pos [zero -RealZero])
(list (-> base zero B : (-FS (-filter non-neg 0) (-filter neg 0)))
(-> zero base B : (-FS (-filter non-pos 1) (-filter pos 1)))
(-> base -PosReal B : (-FS (-filter pos 0) -top))
(-> base -NonNegReal B : (-FS (-filter non-neg 0) -top))
(-> -NonNegReal base B : (-FS -top (-filter pos 1)))
(-> base -NonPosReal B : (-FS -top (-filter neg 0)))
(-> -NegReal base B : (-FS (-filter neg 1) -top))
(-> -NonPosReal base B : (-FS (-filter non-pos 1) -top))))
(list (-> base zero B : (-PS (-is-type 0 non-neg) (-is-type 0 neg)))
(-> zero base B : (-PS (-is-type 1 non-pos) (-is-type 1 pos)))
(-> base -PosReal B : (-PS (-is-type 0 pos) -tt))
(-> base -NonNegReal B : (-PS (-is-type 0 non-neg) -tt))
(-> -NonNegReal base B : (-PS -tt (-is-type 1 pos)))
(-> base -NonPosReal B : (-PS -tt (-is-type 0 neg)))
(-> -NegReal base B : (-PS (-is-type 1 neg) -tt))
(-> -NonPosReal base B : (-PS (-is-type 1 non-pos) -tt))))
(define (negation-pattern pos neg non-neg non-pos)
(list (-> pos neg)
@ -654,7 +654,7 @@
(define abs-cases ; used both for abs and magnitude
(list
;; abs is not the identity on negative zeros.
((Un -Zero -PosReal) . -> . (Un -Zero -PosReal) : -true-filter : (-arg-path 0))
((Un -Zero -PosReal) . -> . (Un -Zero -PosReal) : -true-propset : (-arg-path 0))
;; but we know that we at least get *some* zero, and that it preserves exactness
(map unop (list -FlonumZero -SingleFlonumZero -RealZero))
;; abs may not be closed on fixnums. (abs min-fixnum) is not a fixnum
@ -713,12 +713,12 @@
;; There are 25 values that answer true to zero?. They are either reals, or inexact complexes.
;; Note -RealZero contains NaN and zero? returns #f on it
[zero?
(-> N B : (-FS (-filter (Un -RealZeroNoNan -InexactComplex -InexactImaginary) 0)
(-not-filter -RealZeroNoNan 0)))]
(-> N B : (-PS (-is-type 0 (Un -RealZeroNoNan -InexactComplex -InexactImaginary))
(-not-type 0 -RealZeroNoNan)))]
[number? (make-pred-ty N)]
[integer? (asym-pred Univ B (-FS (-filter (Un -Int -Flonum -SingleFlonum) 0) ; inexact-integers exist...
(-not-filter -Int 0)))]
[integer? (asym-pred Univ B (-PS (-is-type 0 (Un -Int -Flonum -SingleFlonum)) ; inexact-integers exist...
(-not-type 0 -Int)))]
[exact-integer? (make-pred-ty -Int)]
[real? (make-pred-ty -Real)]
[flonum? (make-pred-ty -Flonum)]
@ -727,78 +727,78 @@
[inexact-real? (make-pred-ty -InexactReal)]
[complex? (make-pred-ty N)]
;; `rational?' includes all Reals, except infinities and NaN.
[rational? (asym-pred Univ B (-FS (-filter -Real 0) (-not-filter -Rat 0)))]
[rational? (asym-pred Univ B (-PS (-is-type 0 -Real) (-not-type 0 -Rat)))]
[exact? (make-pred-ty -ExactNumber)]
[inexact? (make-pred-ty (Un -InexactReal -InexactImaginary -InexactComplex))]
[fixnum? (make-pred-ty -Fixnum)]
[index? (make-pred-ty -Index)]
[positive? (-> -Real B : (-FS (-filter -PosReal 0) (-filter -NonPosReal 0)))]
[negative? (-> -Real B : (-FS (-filter -NegReal 0) (-filter -NonNegReal 0)))]
[positive? (-> -Real B : (-PS (-is-type 0 -PosReal) (-is-type 0 -NonPosReal)))]
[negative? (-> -Real B : (-PS (-is-type 0 -NegReal) (-is-type 0 -NonNegReal)))]
[exact-positive-integer? (make-pred-ty -Pos)]
[exact-nonnegative-integer? (make-pred-ty -Nat)]
[odd? (-> -Int B : (-FS (-not-filter -Zero 0) (-not-filter -One 0)))]
[even? (-> -Int B : (-FS (-not-filter -One 0) (-not-filter -Zero 0)))]
[odd? (-> -Int B : (-PS (-not-type 0 -Zero) (-not-type 0 -One)))]
[even? (-> -Int B : (-PS (-not-type 0 -One) (-not-type 0 -Zero)))]
[=
(from-cases
(-> -Real -RealZero B : (-FS (-filter -RealZeroNoNan 0) (-not-filter -RealZeroNoNan 0)))
(-> -RealZero -Real B : (-FS (-filter -RealZeroNoNan 1) (-not-filter -RealZeroNoNan 1)))
(map (lambda (t) (commutative-equality/filter -ExactNumber t))
(-> -Real -RealZero B : (-PS (-is-type 0 -RealZeroNoNan) (-not-type 0 -RealZeroNoNan)))
(-> -RealZero -Real B : (-PS (-is-type 1 -RealZeroNoNan) (-not-type 1 -RealZeroNoNan)))
(map (lambda (t) (commutative-equality/prop -ExactNumber t))
(list -One -PosByte -Byte -PosIndex -Index
-PosFixnum -NonNegFixnum -NegFixnum -NonPosFixnum -Fixnum
-PosInt -Nat -NegInt -NonPosInt -Int
-PosRat -NonNegRat -NegRat -NonPosRat -Rat
-ExactNumber))
;; For all real types: the filters give sign information, and the exactness information is preserved
;; For all real types: the props give sign information, and the exactness information is preserved
;; from the original types.
(map (lambda (t) (commutative-equality/filter -Real t))
(map (lambda (t) (commutative-equality/prop -Real t))
(list -RealZero -PosReal -NonNegReal -NegReal -NonPosReal -Real))
(->* (list N N) N B))]
[< (from-cases
(-> -Int -One B : (-FS (-filter -NonPosInt 0) (-filter -PosInt 0)))
(-> -Real -Zero B : (-FS (-filter -NegReal 0) (-filter -NonNegReal 0)))
(-> -Zero -Real B : (-FS (-filter -PosReal 1) (-filter -NonPosReal 1)))
(-> -Real -RealZero B : (-FS (-filter -NegReal 0) -top)) ;; False says nothing because of NaN
(-> -RealZero -Real B : (-FS (-filter -PosReal 1) -top)) ;; False says nothing because of NaN
(-> -Byte -PosByte B : (-FS -top (-filter -PosByte 0)))
(-> -Byte -Byte B : (-FS (-filter -PosByte 1) -top))
(-> -PosInt -Byte B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top))
(-> -PosReal -Byte B : (-FS (-filter -PosByte 1) -top)) ; -PosReal is ok here, no filter for #f
(-> -Byte -PosInt B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1))))
(-> -Byte -PosRat B : (-FS -top (-filter -PosByte 0))) ; can't be -PosReal, which includes NaN
(-> -Nat -Byte B : (-FS (-and (-filter -Byte 0) (-filter -PosByte 1)) -top))
(-> -NonNegReal -Byte B : (-FS (-filter -PosByte 1) -top))
(-> -Byte -Nat B : (-FS -top (-filter -Byte 1)))
(-> -Index -PosIndex B : (-FS -top (-filter -PosIndex 0)))
(-> -Index -Index B : (-FS (-filter -PosIndex 1) -top))
(-> -PosInt -Index B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top))
(-> -PosReal -Index B : (-FS (-filter -PosIndex 1) -top))
(-> -Index -PosInt B : (-FS -top (-and (-filter -PosIndex 0) (-filter -PosIndex 1))))
(-> -Index -PosRat B : (-FS -top (-filter -PosIndex 0))) ; can't be -PosReal, which includes NaN
(-> -Nat -Index B : (-FS (-and (-filter -Index 0) (-filter -PosIndex 1)) -top))
(-> -NonNegReal -Index B : (-FS (-filter -PosIndex 1) -top))
(-> -Index -Nat B : (-FS -top (-filter -Index 1)))
(-> -Fixnum -PosInt B : (-FS -top (-and (-filter -PosFixnum 0) (-filter -PosFixnum 1))))
(-> -Fixnum -PosRat B : (-FS -top (-filter -PosFixnum 0)))
(-> -Fixnum -Nat B : (-FS -top (-and (-filter -NonNegFixnum 0) (-filter -NonNegFixnum 1))))
(-> -Fixnum -NonNegRat B : (-FS -top (-filter -NonNegFixnum 0)))
(-> -Nat -Fixnum B : (-FS (-and (-filter -PosFixnum 1) (-filter -NonNegFixnum 0)) -top))
(-> -NonNegReal -Fixnum B : (-FS (-filter -PosFixnum 1) -top))
(-> -Fixnum -NonPosInt B : (-FS (-and (-filter -NegFixnum 0) (-filter -NonPosFixnum 1)) -top))
(-> -Fixnum -NonPosReal B : (-FS (-filter -NegFixnum 0) -top))
(-> -NegInt -Fixnum B : (-FS -top (-and (-filter -NegFixnum 0) (-filter -NegFixnum 1))))
(-> -NegRat -Fixnum B : (-FS -top (-filter -NegFixnum 1)))
(-> -NonPosInt -Fixnum B : (-FS -top (-and (-filter -NonPosFixnum 0) (-filter -NonPosFixnum 1))))
(-> -NonPosRat -Fixnum B : (-FS -top (-filter -NonPosFixnum 1)))
(-> -Real -PosInfinity B : (-FS (-not-filter (Un -InexactRealNan -PosInfinity) 0)
(-filter (Un -InexactRealNan -PosInfinity) 0)))
(-> -NegInfinity -Real B : (-FS (-not-filter (Un -InexactRealNan -NegInfinity) 1)
(-filter (Un -InexactRealNan -NegInfinity) 1)))
(-> -PosInfinity -Real B : -false-filter)
(-> -Real -NegInfinity B : -false-filter)
;; If applying filters resulted in the interesection of the filter and the
(-> -Int -One B : (-PS (-is-type 0 -NonPosInt) (-is-type 0 -PosInt)))
(-> -Real -Zero B : (-PS (-is-type 0 -NegReal) (-is-type 0 -NonNegReal)))
(-> -Zero -Real B : (-PS (-is-type 1 -PosReal) (-is-type 1 -NonPosReal)))
(-> -Real -RealZero B : (-PS (-is-type 0 -NegReal) -tt)) ;; False says nothing because of NaN
(-> -RealZero -Real B : (-PS (-is-type 1 -PosReal) -tt)) ;; False says nothing because of NaN
(-> -Byte -PosByte B : (-PS -tt (-is-type 0 -PosByte)))
(-> -Byte -Byte B : (-PS (-is-type 1 -PosByte) -tt))
(-> -PosInt -Byte B : (-PS (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte)) -tt))
(-> -PosReal -Byte B : (-PS (-is-type 1 -PosByte) -tt)) ; -PosReal is ok here, no prop for #f
(-> -Byte -PosInt B : (-PS -tt (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte))))
(-> -Byte -PosRat B : (-PS -tt (-is-type 0 -PosByte))) ; can't be -PosReal, which includes NaN
(-> -Nat -Byte B : (-PS (-and (-is-type 0 -Byte) (-is-type 1 -PosByte)) -tt))
(-> -NonNegReal -Byte B : (-PS (-is-type 1 -PosByte) -tt))
(-> -Byte -Nat B : (-PS -tt (-is-type 1 -Byte)))
(-> -Index -PosIndex B : (-PS -tt (-is-type 0 -PosIndex)))
(-> -Index -Index B : (-PS (-is-type 1 -PosIndex) -tt))
(-> -PosInt -Index B : (-PS (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex)) -tt))
(-> -PosReal -Index B : (-PS (-is-type 1 -PosIndex) -tt))
(-> -Index -PosInt B : (-PS -tt (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex))))
(-> -Index -PosRat B : (-PS -tt (-is-type 0 -PosIndex))) ; can't be -PosReal, which includes NaN
(-> -Nat -Index B : (-PS (-and (-is-type 0 -Index) (-is-type 1 -PosIndex)) -tt))
(-> -NonNegReal -Index B : (-PS (-is-type 1 -PosIndex) -tt))
(-> -Index -Nat B : (-PS -tt (-is-type 1 -Index)))
(-> -Fixnum -PosInt B : (-PS -tt (-and (-is-type 0 -PosFixnum) (-is-type 1 -PosFixnum))))
(-> -Fixnum -PosRat B : (-PS -tt (-is-type 0 -PosFixnum)))
(-> -Fixnum -Nat B : (-PS -tt (-and (-is-type 0 -NonNegFixnum) (-is-type 1 -NonNegFixnum))))
(-> -Fixnum -NonNegRat B : (-PS -tt (-is-type 0 -NonNegFixnum)))
(-> -Nat -Fixnum B : (-PS (-and (-is-type 1 -PosFixnum) (-is-type 0 -NonNegFixnum)) -tt))
(-> -NonNegReal -Fixnum B : (-PS (-is-type 1 -PosFixnum) -tt))
(-> -Fixnum -NonPosInt B : (-PS (-and (-is-type 0 -NegFixnum) (-is-type 1 -NonPosFixnum)) -tt))
(-> -Fixnum -NonPosReal B : (-PS (-is-type 0 -NegFixnum) -tt))
(-> -NegInt -Fixnum B : (-PS -tt (-and (-is-type 0 -NegFixnum) (-is-type 1 -NegFixnum))))
(-> -NegRat -Fixnum B : (-PS -tt (-is-type 1 -NegFixnum)))
(-> -NonPosInt -Fixnum B : (-PS -tt (-and (-is-type 0 -NonPosFixnum) (-is-type 1 -NonPosFixnum))))
(-> -NonPosRat -Fixnum B : (-PS -tt (-is-type 1 -NonPosFixnum)))
(-> -Real -PosInfinity B : (-PS (-not-type 0 (Un -InexactRealNan -PosInfinity))
(-is-type 0 (Un -InexactRealNan -PosInfinity))))
(-> -NegInfinity -Real B : (-PS (-not-type 1 (Un -InexactRealNan -NegInfinity))
(-is-type 1 (Un -InexactRealNan -NegInfinity))))
(-> -PosInfinity -Real B : -false-propset)
(-> -Real -NegInfinity B : -false-propset)
;; If applying props resulted in the interesection of the prop and the
;; original type, we'd only need the cases for Fixnums and those for Reals.
;; Cases for Integers and co would fall out naturally from the Real cases,
;; since we'd keep track of the representation knowledge we'd already have,
@ -812,47 +812,47 @@
(<-type-pattern -Real -PosReal -NonNegReal -NegReal -NonPosReal)
(->* (list R R) R B))]
[> (from-cases
(-> -One -Int B : (-FS (-filter -NonPosInt 1) (-filter -PosInt 1)))
(-> -Real -Zero B : (-FS (-filter -PosReal 0) (-filter -NonPosReal 0)))
(-> -Zero -Real B : (-FS (-filter -NegReal 1) (-filter -NonNegReal 1)))
(-> -Real -RealZero B : (-FS (-filter -PosReal 0) -top)) ;; False says nothing because of NaN
(-> -RealZero -Real B : (-FS (-filter -NegReal 1) -top)) ;; False says nothing because of NaN
(-> -PosByte -Byte B : (-FS -top (-filter -PosByte 1)))
(-> -Byte -Byte B : (-FS (-filter -PosByte 0) -top))
(-> -Byte -PosInt B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top))
(-> -Byte -PosReal B : (-FS (-filter -PosByte 0) -top))
(-> -PosInt -Byte B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1))))
(-> -PosRat -Byte B : (-FS -top (-filter -PosByte 1)))
(-> -Byte -Nat B : (-FS (-and (-filter -PosByte 0) (-filter -Byte 1)) -top))
(-> -Byte -NonNegReal B : (-FS (-filter -PosByte 0) -top))
(-> -Nat -Byte B : (-FS -top (-filter -Byte 0)))
(-> -PosIndex -Index B : (-FS -top (-filter -PosIndex 1)))
(-> -Index -Index B : (-FS (-filter -PosIndex 0) -top))
(-> -Index -PosInt B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top))
(-> -Index -PosReal B : (-FS (-filter -PosIndex 0) -top))
(-> -PosInt -Index B : (-FS -top (-and (-filter -PosIndex 0) (-filter -PosIndex 1))))
(-> -PosRat -Index B : (-FS -top (-filter -PosIndex 1)))
(-> -Index -Nat B : (-FS (-and (-filter -PosIndex 0) (-filter -Index 1)) -top))
(-> -Index -NonNegReal B : (-FS (-filter -PosIndex 0) -top))
(-> -Nat -Index B : (-FS -top (-filter -Index 0)))
(-> -PosInt -Fixnum B : (-FS -top (-and (-filter -PosFixnum 0) (-filter -PosFixnum 1))))
(-> -PosRat -Fixnum B : (-FS -top (-filter -PosFixnum 1)))
(-> -Nat -Fixnum B : (-FS -top (-and (-filter -NonNegFixnum 0) (-filter -NonNegFixnum 1))))
(-> -NonNegRat -Fixnum B : (-FS -top (-filter -NonNegFixnum 1)))
(-> -Fixnum -Nat B : (-FS (-and (-filter -PosFixnum 0) (-filter -NonNegFixnum 1)) -top))
(-> -Fixnum -NonNegReal B : (-FS (-filter -PosFixnum 0) -top))
(-> -NonPosInt -Fixnum B : (-FS (-and (-filter -NonPosFixnum 0) (-filter -NegFixnum 1)) -top))
(-> -NonPosReal -Fixnum B : (-FS (-filter -NegFixnum 1) -top))
(-> -Fixnum -NegInt B : (-FS -top (-and (-filter -NegFixnum 0) (-filter -NegFixnum 1))))
(-> -Fixnum -NegRat B : (-FS -top (-filter -NegFixnum 0)))
(-> -Fixnum -NonPosInt B : (-FS -top (-and (-filter -NonPosFixnum 0) (-filter -NonPosFixnum 1))))
(-> -Fixnum -NonPosRat B : (-FS -top (-filter -NonPosFixnum 0)))
(-> -PosInfinity -Real B : (-FS (-not-filter (Un -InexactRealNan -PosInfinity) 1)
(-filter (Un -InexactRealNan -PosInfinity) 1)))
(-> -Real -NegInfinity B : (-FS (-not-filter (Un -InexactRealNan -NegInfinity) 0)
(-filter (Un -InexactRealNan -NegInfinity) 0)))
(-> -Real -PosInfinity B : -false-filter)
(-> -NegInfinity -Real B : -false-filter)
(-> -One -Int B : (-PS (-is-type 1 -NonPosInt) (-is-type 1 -PosInt)))
(-> -Real -Zero B : (-PS (-is-type 0 -PosReal) (-is-type 0 -NonPosReal)))
(-> -Zero -Real B : (-PS (-is-type 1 -NegReal) (-is-type 1 -NonNegReal)))
(-> -Real -RealZero B : (-PS (-is-type 0 -PosReal) -tt)) ;; False says nothing because of NaN
(-> -RealZero -Real B : (-PS (-is-type 1 -NegReal) -tt)) ;; False says nothing because of NaN
(-> -PosByte -Byte B : (-PS -tt (-is-type 1 -PosByte)))
(-> -Byte -Byte B : (-PS (-is-type 0 -PosByte) -tt))
(-> -Byte -PosInt B : (-PS (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte)) -tt))
(-> -Byte -PosReal B : (-PS (-is-type 0 -PosByte) -tt))
(-> -PosInt -Byte B : (-PS -tt (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte))))
(-> -PosRat -Byte B : (-PS -tt (-is-type 1 -PosByte)))
(-> -Byte -Nat B : (-PS (-and (-is-type 0 -PosByte) (-is-type 1 -Byte)) -tt))
(-> -Byte -NonNegReal B : (-PS (-is-type 0 -PosByte) -tt))
(-> -Nat -Byte B : (-PS -tt (-is-type 0 -Byte)))
(-> -PosIndex -Index B : (-PS -tt (-is-type 1 -PosIndex)))
(-> -Index -Index B : (-PS (-is-type 0 -PosIndex) -tt))
(-> -Index -PosInt B : (-PS (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex)) -tt))
(-> -Index -PosReal B : (-PS (-is-type 0 -PosIndex) -tt))
(-> -PosInt -Index B : (-PS -tt (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex))))
(-> -PosRat -Index B : (-PS -tt (-is-type 1 -PosIndex)))
(-> -Index -Nat B : (-PS (-and (-is-type 0 -PosIndex) (-is-type 1 -Index)) -tt))
(-> -Index -NonNegReal B : (-PS (-is-type 0 -PosIndex) -tt))
(-> -Nat -Index B : (-PS -tt (-is-type 0 -Index)))
(-> -PosInt -Fixnum B : (-PS -tt (-and (-is-type 0 -PosFixnum) (-is-type 1 -PosFixnum))))
(-> -PosRat -Fixnum B : (-PS -tt (-is-type 1 -PosFixnum)))
(-> -Nat -Fixnum B : (-PS -tt (-and (-is-type 0 -NonNegFixnum) (-is-type 1 -NonNegFixnum))))
(-> -NonNegRat -Fixnum B : (-PS -tt (-is-type 1 -NonNegFixnum)))
(-> -Fixnum -Nat B : (-PS (-and (-is-type 0 -PosFixnum) (-is-type 1 -NonNegFixnum)) -tt))
(-> -Fixnum -NonNegReal B : (-PS (-is-type 0 -PosFixnum) -tt))
(-> -NonPosInt -Fixnum B : (-PS (-and (-is-type 0 -NonPosFixnum) (-is-type 1 -NegFixnum)) -tt))
(-> -NonPosReal -Fixnum B : (-PS (-is-type 1 -NegFixnum) -tt))
(-> -Fixnum -NegInt B : (-PS -tt (-and (-is-type 0 -NegFixnum) (-is-type 1 -NegFixnum))))
(-> -Fixnum -NegRat B : (-PS -tt (-is-type 0 -NegFixnum)))
(-> -Fixnum -NonPosInt B : (-PS -tt (-and (-is-type 0 -NonPosFixnum) (-is-type 1 -NonPosFixnum))))
(-> -Fixnum -NonPosRat B : (-PS -tt (-is-type 0 -NonPosFixnum)))
(-> -PosInfinity -Real B : (-PS (-not-type 1 (Un -InexactRealNan -PosInfinity))
(-is-type 1 (Un -InexactRealNan -PosInfinity))))
(-> -Real -NegInfinity B : (-PS (-not-type 0 (Un -InexactRealNan -NegInfinity))
(-is-type 0 (Un -InexactRealNan -NegInfinity))))
(-> -Real -PosInfinity B : -false-propset)
(-> -NegInfinity -Real B : -false-propset)
(>-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt -Zero)
(>-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat -Zero)
(>-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum)
@ -861,46 +861,46 @@
(>-type-pattern -Real -PosReal -NonNegReal -NegReal -NonPosReal)
(->* (list R R) R B))]
[<= (from-cases
(-> -Int -One B : (-FS (-filter (Un -NonPosInt -One) 0) (-filter -PosInt 0)))
(-> -One -Int B : (-FS (-filter -PosInt 1) (-filter -NonPosInt 1)))
(-> -Real -Zero B : (-FS (-filter -NonPosReal 0) (-filter -PosReal 0)))
(-> -Zero -Real B : (-FS (-filter -NonNegReal 1) (-filter -NegReal 1)))
(-> -Real -RealZero B : (-FS (-filter -NonPosReal 0) -top)) ;; False says nothing because of NaN
(-> -RealZero -Real B : (-FS (-filter -NonNegReal 0) -top)) ;; False says nothing because of NaN
(-> -PosByte -Byte B : (-FS (-filter -PosByte 1) -top))
(-> -Byte -Byte B : (-FS -top (-filter -PosByte 0)))
(-> -PosInt -Byte B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top))
(-> -PosReal -Byte B : (-FS (-filter -PosByte 1) -top))
(-> -Byte -PosInt B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1))))
(-> -Byte -PosRat B : (-FS -top (-filter -PosByte 0)))
(-> -Nat -Byte B : (-FS (-filter -Byte 0) -top))
(-> -Byte -Nat B : (-FS -top (-and (-filter -PosByte 0) (-filter -Byte 1))))
(-> -Byte -NonNegRat B : (-FS -top (-filter -PosByte 0)))
(-> -PosIndex -Index B : (-FS (-filter -PosIndex 1) -top))
(-> -Index -Index B : (-FS -top (-filter -PosIndex 0)))
(-> -Pos -Index B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top))
(-> -PosReal -Index B : (-FS (-filter -PosIndex 1) -top))
(-> -Index -Pos B : (-FS -top (-and (-filter -PosIndex 0) (-filter -PosIndex 1))))
(-> -Index -PosRat B : (-FS -top (-filter -PosIndex 0)))
(-> -Nat -Index B : (-FS (-filter -Index 0) -top))
(-> -Index -Nat B : (-FS -top (-and (-filter -PosIndex 0) (-filter -Index 1))))
(-> -Index -NonNegRat B : (-FS -top (-filter -PosIndex 0)))
(-> -PosInt -Fixnum B : (-FS (-and (-filter -PosFixnum 0) (-filter -PosFixnum 1)) -top))
(-> -PosReal -Fixnum B : (-FS (-filter -PosFixnum 1) -top))
(-> -Nat -Fixnum B : (-FS (-and (-filter -NonNegFixnum 0) (-filter -NonNegFixnum 1)) -top))
(-> -NonNegReal -Fixnum B : (-FS (-filter -NonNegFixnum 1) -top))
(-> -Fixnum -Nat B : (-FS -top (-and (-filter -PosFixnum 0) (-filter -NonNegFixnum 1))))
(-> -Fixnum -NonNegRat B : (-FS -top (-filter -PosFixnum 0)))
(-> -NonPosInt -Fixnum B : (-FS -top (-and (-filter -NonPosFixnum 0) (-filter -NegFixnum 1))))
(-> -NonPosRat -Fixnum B : (-FS -top (-filter -NegFixnum 1)))
(-> -Fixnum -NegInt B : (-FS (-and (-filter -NegFixnum 0) (-filter -NegFixnum 1)) -top))
(-> -Fixnum -NegReal B : (-FS (-filter -NegFixnum 0) -top))
(-> -Fixnum -NonPosInt B : (-FS (-and (-filter -NonPosFixnum 0) (-filter -NonPosFixnum 1)) -top))
(-> -Fixnum -NonPosReal B : (-FS (-filter -NonPosFixnum 0) -top))
(-> -Real -PosInfinity B : (-FS (-not-filter -InexactRealNan 0) (-filter -InexactRealNan 0)))
(-> -NegInfinity -Real B : (-FS (-not-filter -InexactRealNan 1) (-filter -InexactRealNan 1)))
(-> -PosInfinity -Real B : (-FS (-filter -PosInfinity 1) (-not-filter -PosInfinity 1)))
(-> -Real -NegInfinity B : (-FS (-filter -NegInfinity 0) (-not-filter -NegInfinity 0)))
(-> -Int -One B : (-PS (-is-type 0 (Un -NonPosInt -One)) (-is-type 0 -PosInt)))
(-> -One -Int B : (-PS (-is-type 1 -PosInt) (-is-type 1 -NonPosInt)))
(-> -Real -Zero B : (-PS (-is-type 0 -NonPosReal) (-is-type 0 -PosReal)))
(-> -Zero -Real B : (-PS (-is-type 1 -NonNegReal) (-is-type 1 -NegReal)))
(-> -Real -RealZero B : (-PS (-is-type 0 -NonPosReal) -tt)) ;; False says nothing because of NaN
(-> -RealZero -Real B : (-PS (-is-type 0 -NonNegReal) -tt)) ;; False says nothing because of NaN
(-> -PosByte -Byte B : (-PS (-is-type 1 -PosByte) -tt))
(-> -Byte -Byte B : (-PS -tt (-is-type 0 -PosByte)))
(-> -PosInt -Byte B : (-PS (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte)) -tt))
(-> -PosReal -Byte B : (-PS (-is-type 1 -PosByte) -tt))
(-> -Byte -PosInt B : (-PS -tt (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte))))
(-> -Byte -PosRat B : (-PS -tt (-is-type 0 -PosByte)))
(-> -Nat -Byte B : (-PS (-is-type 0 -Byte) -tt))
(-> -Byte -Nat B : (-PS -tt (-and (-is-type 0 -PosByte) (-is-type 1 -Byte))))
(-> -Byte -NonNegRat B : (-PS -tt (-is-type 0 -PosByte)))
(-> -PosIndex -Index B : (-PS (-is-type 1 -PosIndex) -tt))
(-> -Index -Index B : (-PS -tt (-is-type 0 -PosIndex)))
(-> -Pos -Index B : (-PS (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex)) -tt))
(-> -PosReal -Index B : (-PS (-is-type 1 -PosIndex) -tt))
(-> -Index -Pos B : (-PS -tt (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex))))
(-> -Index -PosRat B : (-PS -tt (-is-type 0 -PosIndex)))
(-> -Nat -Index B : (-PS (-is-type 0 -Index) -tt))
(-> -Index -Nat B : (-PS -tt (-and (-is-type 0 -PosIndex) (-is-type 1 -Index))))
(-> -Index -NonNegRat B : (-PS -tt (-is-type 0 -PosIndex)))
(-> -PosInt -Fixnum B : (-PS (-and (-is-type 0 -PosFixnum) (-is-type 1 -PosFixnum)) -tt))
(-> -PosReal -Fixnum B : (-PS (-is-type 1 -PosFixnum) -tt))
(-> -Nat -Fixnum B : (-PS (-and (-is-type 0 -NonNegFixnum) (-is-type 1 -NonNegFixnum)) -tt))
(-> -NonNegReal -Fixnum B : (-PS (-is-type 1 -NonNegFixnum) -tt))
(-> -Fixnum -Nat B : (-PS -tt (-and (-is-type 0 -PosFixnum) (-is-type 1 -NonNegFixnum))))
(-> -Fixnum -NonNegRat B : (-PS -tt (-is-type 0 -PosFixnum)))
(-> -NonPosInt -Fixnum B : (-PS -tt (-and (-is-type 0 -NonPosFixnum) (-is-type 1 -NegFixnum))))
(-> -NonPosRat -Fixnum B : (-PS -tt (-is-type 1 -NegFixnum)))
(-> -Fixnum -NegInt B : (-PS (-and (-is-type 0 -NegFixnum) (-is-type 1 -NegFixnum)) -tt))
(-> -Fixnum -NegReal B : (-PS (-is-type 0 -NegFixnum) -tt))
(-> -Fixnum -NonPosInt B : (-PS (-and (-is-type 0 -NonPosFixnum) (-is-type 1 -NonPosFixnum)) -tt))
(-> -Fixnum -NonPosReal B : (-PS (-is-type 0 -NonPosFixnum) -tt))
(-> -Real -PosInfinity B : (-PS (-not-type 0 -InexactRealNan) (-is-type 0 -InexactRealNan)))
(-> -NegInfinity -Real B : (-PS (-not-type 1 -InexactRealNan) (-is-type 1 -InexactRealNan)))
(-> -PosInfinity -Real B : (-PS (-is-type 1 -PosInfinity) (-not-type 1 -PosInfinity)))
(-> -Real -NegInfinity B : (-PS (-is-type 0 -NegInfinity) (-not-type 0 -NegInfinity)))
(<=-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt -Zero)
(<=-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat -Zero)
(<=-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum)
@ -909,46 +909,46 @@
(<=-type-pattern -Real -PosReal -NonNegReal -NegReal -NonPosReal)
(->* (list R R) R B))]
[>= (from-cases
(-> -One -Int B : (-FS (-filter (Un -One -NonPosInt) 1) (-filter -PosInt 1)))
(-> -Int -One B : (-FS (-filter -PosInt 0) (-filter -NonPosInt 0)))
(-> -Real -Zero B : (-FS (-filter -NonNegReal 0) (-filter -NegReal 0)))
(-> -Zero -Real B : (-FS (-filter -NonPosReal 1) (-filter -PosReal 1)))
(-> -Real -RealZero B : (-FS (-filter -NonNegReal 0) -top)) ;; False says nothing because of NaN
(-> -RealZero -Real B : (-FS (-filter -NonPosReal 0) -top)) ;; False says nothing because of NaN
(-> -Byte -PosByte B : (-FS (-filter -PosByte 0) -top))
(-> -Byte -Byte B : (-FS -top (-filter -PosByte 1)))
(-> -Byte -PosInt B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top))
(-> -Byte -PosReal B : (-FS (-filter -PosByte 0) -top))
(-> -PosInt -Byte B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1))))
(-> -PosRat -Byte B : (-FS -top (-filter -PosByte 1)))
(-> -Byte -Nat B : (-FS (-filter -Byte 1) -top))
(-> -Nat -Byte B : (-FS -top (-and (-filter -Byte 0) (-filter -PosByte 1))))
(-> -NonNegRat -Byte B : (-FS -top (-filter -PosByte 1)))
(-> -Index -PosIndex B : (-FS (-filter -PosIndex 0) -top))
(-> -Index -Index B : (-FS -top (-filter -PosIndex 1)))
(-> -Index -Pos B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top))
(-> -Index -PosReal B : (-FS (-filter -PosIndex 0) -top))
(-> -Pos -Index B : (-FS -top (-and (-filter -PosIndex 0) (-filter -PosIndex 1))))
(-> -PosRat -Index B : (-FS -top (-filter -PosIndex 1)))
(-> -Index -Nat B : (-FS (-filter -Index 1) -top))
(-> -Nat -Index B : (-FS -top (-and (-filter -Index 0) (-filter -PosIndex 1))))
(-> -NonNegRat -Index B : (-FS -top (-filter -PosIndex 1)))
(-> -Fixnum -PosInt B : (-FS (-and (-filter -PosFixnum 0) (-filter -PosFixnum 1)) -top))
(-> -Fixnum -PosReal B : (-FS (-filter -PosFixnum 0) -top))
(-> -Fixnum -Nat B : (-FS (-and (-filter -NonNegFixnum 0) (-filter -NonNegFixnum 1)) -top))
(-> -Fixnum -NonNegReal B : (-FS (-filter -NonNegFixnum 0) -top))
(-> -Nat -Fixnum B : (-FS -top (-and (-filter -NonNegFixnum 0) (-filter -PosFixnum 1))))
(-> -NonNegRat -Fixnum B : (-FS -top (-filter -PosFixnum 1)))
(-> -Fixnum -NonPosInt B : (-FS -top (-and (-filter -NegFixnum 0) (-filter -NonPosFixnum 1))))
(-> -Fixnum -NonPosRat B : (-FS -top (-filter -NegFixnum 0)))
(-> -NegInt -Fixnum B : (-FS (-and (-filter -NegFixnum 0) (-filter -NegFixnum 1)) -top))
(-> -NegReal -Fixnum B : (-FS (-filter -NegFixnum 1) -top))
(-> -NonPosInt -Fixnum B : (-FS (-and (-filter -NonPosFixnum 0) (-filter -NonPosFixnum 1)) -top))
(-> -NonPosReal -Fixnum B : (-FS (-filter -NonPosFixnum 1) -top))
(-> -PosInfinity -Real B : (-FS (-not-filter -InexactRealNan 1) (-filter -InexactRealNan 1)))
(-> -Real -NegInfinity B : (-FS (-not-filter -InexactRealNan 0) (-filter -InexactRealNan 0)))
(-> -Real -PosInfinity B : (-FS (-filter -PosInfinity 0) (-not-filter -PosInfinity 0)))
(-> -NegInfinity -Real B : (-FS (-filter -NegInfinity 1) (-not-filter -NegInfinity 1)))
(-> -One -Int B : (-PS (-is-type 1 (Un -One -NonPosInt)) (-is-type 1 -PosInt)))
(-> -Int -One B : (-PS (-is-type 0 -PosInt) (-is-type 0 -NonPosInt)))
(-> -Real -Zero B : (-PS (-is-type 0 -NonNegReal) (-is-type 0 -NegReal)))
(-> -Zero -Real B : (-PS (-is-type 1 -NonPosReal) (-is-type 1 -PosReal)))
(-> -Real -RealZero B : (-PS (-is-type 0 -NonNegReal) -tt)) ;; False says nothing because of NaN
(-> -RealZero -Real B : (-PS (-is-type 0 -NonPosReal) -tt)) ;; False says nothing because of NaN
(-> -Byte -PosByte B : (-PS (-is-type 0 -PosByte) -tt))
(-> -Byte -Byte B : (-PS -tt (-is-type 1 -PosByte)))
(-> -Byte -PosInt B : (-PS (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte)) -tt))
(-> -Byte -PosReal B : (-PS (-is-type 0 -PosByte) -tt))
(-> -PosInt -Byte B : (-PS -tt (-and (-is-type 0 -PosByte) (-is-type 1 -PosByte))))
(-> -PosRat -Byte B : (-PS -tt (-is-type 1 -PosByte)))
(-> -Byte -Nat B : (-PS (-is-type 1 -Byte) -tt))
(-> -Nat -Byte B : (-PS -tt (-and (-is-type 0 -Byte) (-is-type 1 -PosByte))))
(-> -NonNegRat -Byte B : (-PS -tt (-is-type 1 -PosByte)))
(-> -Index -PosIndex B : (-PS (-is-type 0 -PosIndex) -tt))
(-> -Index -Index B : (-PS -tt (-is-type 1 -PosIndex)))
(-> -Index -Pos B : (-PS (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex)) -tt))
(-> -Index -PosReal B : (-PS (-is-type 0 -PosIndex) -tt))
(-> -Pos -Index B : (-PS -tt (-and (-is-type 0 -PosIndex) (-is-type 1 -PosIndex))))
(-> -PosRat -Index B : (-PS -tt (-is-type 1 -PosIndex)))
(-> -Index -Nat B : (-PS (-is-type 1 -Index) -tt))
(-> -Nat -Index B : (-PS -tt (-and (-is-type 0 -Index) (-is-type 1 -PosIndex))))
(-> -NonNegRat -Index B : (-PS -tt (-is-type 1 -PosIndex)))
(-> -Fixnum -PosInt B : (-PS (-and (-is-type 0 -PosFixnum) (-is-type 1 -PosFixnum)) -tt))
(-> -Fixnum -PosReal B : (-PS (-is-type 0 -PosFixnum) -tt))
(-> -Fixnum -Nat B : (-PS (-and (-is-type 0 -NonNegFixnum) (-is-type 1 -NonNegFixnum)) -tt))
(-> -Fixnum -NonNegReal B : (-PS (-is-type 0 -NonNegFixnum) -tt))
(-> -Nat -Fixnum B : (-PS -tt (-and (-is-type 0 -NonNegFixnum) (-is-type 1 -PosFixnum))))
(-> -NonNegRat -Fixnum B : (-PS -tt (-is-type 1 -PosFixnum)))
(-> -Fixnum -NonPosInt B : (-PS -tt (-and (-is-type 0 -NegFixnum) (-is-type 1 -NonPosFixnum))))
(-> -Fixnum -NonPosRat B : (-PS -tt (-is-type 0 -NegFixnum)))
(-> -NegInt -Fixnum B : (-PS (-and (-is-type 0 -NegFixnum) (-is-type 1 -NegFixnum)) -tt))
(-> -NegReal -Fixnum B : (-PS (-is-type 1 -NegFixnum) -tt))
(-> -NonPosInt -Fixnum B : (-PS (-and (-is-type 0 -NonPosFixnum) (-is-type 1 -NonPosFixnum)) -tt))
(-> -NonPosReal -Fixnum B : (-PS (-is-type 1 -NonPosFixnum) -tt))
(-> -PosInfinity -Real B : (-PS (-not-type 1 -InexactRealNan) (-is-type 1 -InexactRealNan)))
(-> -Real -NegInfinity B : (-PS (-not-type 0 -InexactRealNan) (-is-type 0 -InexactRealNan)))
(-> -Real -PosInfinity B : (-PS (-is-type 0 -PosInfinity) (-not-type 0 -PosInfinity)))
(-> -NegInfinity -Real B : (-PS (-is-type 1 -NegInfinity) (-not-type 1 -NegInfinity)))
(>=-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt -Zero)
(>=-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat -Zero)
(>=-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum)
@ -959,10 +959,10 @@
[* (from-cases
(-> -One)
(-> N N : -true-filter : (-arg-path 0))
(-> N N : -true-propset : (-arg-path 0))
(commutative-case -Zero N -Zero)
(-> N -One N : -true-filter : (-arg-path 0))
(-> -One N N : -true-filter : (-arg-path 1))
(-> N -One N : -true-propset : (-arg-path 0))
(-> -One N N : -true-propset : (-arg-path 1))
(-> -PosByte -PosByte -PosIndex)
(-> -Byte -Byte -Index)
(-> -PosByte -PosByte -PosByte -PosFixnum)
@ -1022,10 +1022,10 @@
(varop N))]
[+ (from-cases
(-> -Zero)
(-> N N : -true-filter : (-arg-path 0))
(-> N N : -true-propset : (-arg-path 0))
(binop -Zero)
(-> N -Zero N : -true-filter : (-arg-path 0))
(-> -Zero N N : -true-filter : (-arg-path 1))
(-> N -Zero N : -true-propset : (-arg-path 0))
(-> -Zero N N : -true-propset : (-arg-path 1))
(-> -PosByte -PosByte -PosIndex)
(-> -Byte -Byte -Index)
(-> -PosByte -PosByte -PosByte -PosIndex)
@ -1091,7 +1091,7 @@
(negation-pattern -PosInexactReal -NegInexactReal -NonNegInexactReal -NonPosInexactReal)
(negation-pattern -PosReal -NegReal -NonNegReal -NonPosReal)
(-> N -Zero N : -true-filter : (-arg-path 0))
(-> N -Zero N : -true-propset : (-arg-path 0))
(-> -One -One -Zero)
(-> -PosByte -One -Byte)
(-> -PosIndex -One -Index)
@ -1128,7 +1128,7 @@
[/ (from-cases ; very similar to multiplication, without closure properties for integers
(commutative-case -Zero N -Zero)
(unop -One)
(-> N -One N : -true-filter : (-arg-path 0))
(-> N -One N : -true-propset : (-arg-path 0))
(varop-1+ -PosRat)
(varop-1+ -NonNegRat)
(-> -NegRat -NegRat)
@ -1654,7 +1654,7 @@
(N . -> . N))]
[integer-sqrt
(from-cases
(-> (Un -RealZero -One) (Un -RealZero -One) : -true-filter : (-arg-path 0))
(-> (Un -RealZero -One) (Un -RealZero -One) : -true-propset : (-arg-path 0))
(unop -Byte)
(-NonNegFixnum . -> . -Index)
(-NonNegRat . -> . -Nat)
@ -1664,8 +1664,8 @@
(-Real . -> . N))] ; defined on inexact integers too, but not complex
[integer-sqrt/remainder
(from-cases
(-RealZero . -> . (make-Values (list (-result -RealZero -true-filter (-arg-path 0))
(-result -RealZero -true-filter (-arg-path 0)))))
(-RealZero . -> . (make-Values (list (-result -RealZero -true-propset (-arg-path 0))
(-result -RealZero -true-propset (-arg-path 0)))))
(-One . -> . (-values (list -One -Zero)))
(-Byte . -> . (-values (list -Byte -Byte)))
(-Index . -> . (-values (list -Index -Index)))

52
typed-racket-lib/typed-racket/base-env/base-env.rkt
View File

@ -672,7 +672,7 @@
[((a b c . -> . c) c (-lst a) (-lst b)) c]
[((a b c d . -> . d) d (-lst a) (-lst b) (-lst c)) d]))]
[filter (-poly (a b) (cl->*
((asym-pred a Univ (-FS (-filter b 0) -top))
((asym-pred a Univ (-PS (-is-type 0 b) -tt))
(-lst a)
. -> .
(-lst b))
@ -712,7 +712,7 @@
-Index))]
[partition
(-poly (a b) (cl->*
(-> (asym-pred b Univ (-FS (-filter a 0) -top)) (-lst b) (-values (list (-lst a) (-lst b))))
(-> (asym-pred b Univ (-PS (-is-type 0 a) -tt)) (-lst b) (-values (list (-lst a) (-lst b))))
(-> (-> a Univ) (-lst a) (-values (list (-lst a) (-lst a))))))]
[last (-poly (a) ((-lst a) . -> . a))]
@ -730,7 +730,7 @@
(-poly (a b)
(cl->*
(-> (-lst a)
(asym-pred a Univ (-FS (-filter b 0) -top))
(asym-pred a Univ (-PS (-is-type 0 b) -tt))
(-lst b))
(-> (-lst a) (-> a Univ) (-lst a))))]
[dropf (-poly (a) (-> (-lst a) (-> a Univ) (-lst a)))]
@ -738,14 +738,14 @@
(-poly (a b)
(cl->*
(-> (-lst a)
(asym-pred a Univ (-FS (-filter b 0) -top))
(asym-pred a Univ (-PS (-is-type 0 b) -tt))
(-values (list (-lst b) (-lst a))))
(-> (-lst a) (-> a Univ) (-values (list (-lst a) (-lst a))))))]
[takef-right
(-poly (a b)
(cl->*
(-> (-lst a)
(asym-pred a Univ (-FS (-filter b 0) -top))
(asym-pred a Univ (-PS (-is-type 0 b) -tt))
(-lst b))
(-> (-lst a) (-> a Univ) (-lst a))))]
[dropf-right (-poly (a) (-> (-lst a) (-> a Univ) (-lst a)))]
@ -753,7 +753,7 @@
(-poly (a b)
(cl->*
(-> (-lst a)
(asym-pred a Univ (-FS (-filter b 0) -top))
(asym-pred a Univ (-PS (-is-type 0 b) -tt))
(-values (list (-lst a) (-lst b))))
(-> (-lst a) (-> a Univ) (-values (list (-lst a) (-lst a))))))]
@ -842,7 +842,7 @@
. ->... .
-Index))]
[vector-filter (-poly (a b) (cl->*
((asym-pred a Univ (-FS (-filter b 0) -top))
((asym-pred a Univ (-PS (-is-type 0 b) -tt))
(-vec a)
. -> .
(-vec b))
@ -1030,7 +1030,7 @@
[sequence-fold (-poly (a b) ((b a . -> . b) b (-seq a) . -> . b))]
[sequence-count (-poly (a) ((a . -> . Univ) (-seq a) . -> . -Nat))]
[sequence-filter (-poly (a b) (cl->*
((asym-pred a Univ (-FS (-filter b 0) -top))
((asym-pred a Univ (-PS (-is-type 0 b) -tt))
(-seq a)
. -> .
(-seq b))
@ -1060,7 +1060,7 @@
[proper-subset? (-poly (e) (-> (-set e) (-set e) B))]
[set-map (-poly (e b) (-> (-set e) (-> e b) (-lst b)))]
[set-for-each (-poly (e b) (-> (-set e) (-> e b) -Void))]
[generic-set? (asym-pred Univ B (-FS -top (-not-filter (-set Univ) 0)))]
[generic-set? (asym-pred Univ B (-PS -tt (-not-type 0 (-set Univ))))]
[set? (make-pred-ty (-set Univ))]
[set-equal? (-poly (e) (-> (-set e) B))]
[set-eqv? (-poly (e) (-> (-set e) B))]
@ -1099,14 +1099,14 @@
[identity (-poly (a) (->acc (list a) a null))]
[const (-poly (a) (-> a (->* '() Univ a)))]
[negate (-polydots (a b c d)
(cl->* (-> (-> c Univ : (-FS (-filter a 0) (-not-filter b 0)))
(-> c -Boolean : (-FS (-not-filter b 0) (-filter a 0))))
(-> (-> c Univ : (-FS (-filter a 0) (-filter b 0)))
(-> c -Boolean : (-FS (-filter b 0) (-filter a 0))))
(-> (-> c Univ : (-FS (-not-filter a 0) (-filter b 0)))
(-> c -Boolean : (-FS (-filter b 0) (-not-filter a 0))))
(-> (-> c Univ : (-FS (-not-filter a 0) (-not-filter b 0)))
(-> c -Boolean : (-FS (-not-filter b 0) (-not-filter a 0))))
(cl->* (-> (-> c Univ : (-PS (-is-type 0 a) (-not-type 0 b)))
(-> c -Boolean : (-PS (-not-type 0 b) (-is-type 0 a))))
(-> (-> c Univ : (-PS (-is-type 0 a) (-is-type 0 b)))
(-> c -Boolean : (-PS (-is-type 0 b) (-is-type 0 a))))
(-> (-> c Univ : (-PS (-not-type 0 a) (-is-type 0 b)))
(-> c -Boolean : (-PS (-is-type 0 b) (-not-type 0 a))))
(-> (-> c Univ : (-PS (-not-type 0 a) (-not-type 0 b)))
(-> c -Boolean : (-PS (-not-type 0 b) (-not-type 0 a))))
(-> ((list) [d d] . ->... . Univ)
((list) [d d] . ->... . -Boolean))))]
[conjoin (-polydots (a) (->* '() (->... '() (a a) Univ) (->... '() (a a) Univ)))]
@ -1292,7 +1292,7 @@
[call-with-continuation-barrier (-poly (a) (-> (-> a) a))]
[continuation-prompt-available? (-> (make-Prompt-TagTop) B)]
[continuation?
(asym-pred Univ B (-FS (-filter top-func 0) -top))]
(asym-pred Univ B (-PS (-is-type 0 top-func) -tt))]
[continuation-prompt-tag? (make-pred-ty (make-Prompt-TagTop))]
[dynamic-wind (-poly (a) (-> (-> ManyUniv) (-> a) (-> ManyUniv) a))]
@ -1413,7 +1413,7 @@
[never-evt (-evt (Un))]
[system-idle-evt (-> (-evt -Void))]
[alarm-evt (-> -Real (-mu x (-evt x)))]
[handle-evt? (asym-pred Univ B (-FS (-filter (-evt Univ) 0) -top))]
[handle-evt? (asym-pred Univ B (-PS (-is-type 0 (-evt Univ)) -tt))]
[current-evt-pseudo-random-generator
(-Param -Pseudo-Random-Generator -Pseudo-Random-Generator)]
@ -1424,7 +1424,7 @@
[channel-try-get (-poly (a) ((-channel a) . -> . (Un a (-val #f))))]
[channel-put (-poly (a) ((-channel a) a . -> . -Void))]
[channel-put-evt (-poly (a) (-> (-channel a) a (-mu x (-evt x))))]
[channel-put-evt? (asym-pred Univ B (-FS (-filter (-mu x (-evt x)) 0) -top))]
[channel-put-evt? (asym-pred Univ B (-PS (-is-type 0 (-mu x (-evt x))) -tt))]
;; Section 11.2.3 (Semaphores)
[semaphore? (make-pred-ty -Semaphore)]
@ -1434,7 +1434,7 @@
[semaphore-try-wait? (-> -Semaphore B)]
[semaphore-wait/enable-break (-> -Semaphore -Void)]
[semaphore-peek-evt (-> -Semaphore (-mu x (-evt x)))]
[semaphore-peek-evt? (asym-pred Univ B (-FS (-filter (-mu x (-evt x)) 0) -top))]
[semaphore-peek-evt? (asym-pred Univ B (-PS (-is-type 0 (-mu x (-evt x))) -tt))]
[call-with-semaphore
(-polydots (b a)
(cl->* (->... (list -Semaphore (->... '() [a a] b))
@ -2303,7 +2303,7 @@
[resolved-module-path? (make-pred-ty -Resolved-Module-Path)]
[make-resolved-module-path (-> (Un -Symbol -Path) -Resolved-Module-Path)]
[resolved-module-path-name (-> -Resolved-Module-Path (Un -Path -Symbol))]
[module-path? (asym-pred Univ B (-FS (-filter -Module-Path 0) -top))]
[module-path? (asym-pred Univ B (-PS (-is-type 0 -Module-Path) -tt))]
[current-module-name-resolver (-Param (cl->* (-Resolved-Module-Path Univ . -> . Univ)
((Un -Module-Path -Path)
@ -2487,8 +2487,8 @@
;; Section 15.1 (Path Manipulation)
[path? (make-pred-ty -Path)]
[path-string? (asym-pred Univ B
(-FS (-filter (Un -Path -String) 0)
(-not-filter -Path 0)))]
(-PS (-is-type 0 (Un -Path -String))
(-not-type 0 -Path)))]
[path-for-some-system? (make-pred-ty -SomeSystemPath)]
[string->path (-> -String -Path)]
@ -2681,7 +2681,7 @@
(-Port [(-val #f)] . ->opt . (-values (list -String -String)))
(-Port (-val #t) . -> . (-values (list -String -Index -String -Index))))]
[tcp-port? (asym-pred Univ B (-FS (-filter (Un -Input-Port -Output-Port) 0) -top))]
[tcp-port? (asym-pred Univ B (-PS (-is-type 0 (Un -Input-Port -Output-Port)) -tt))]
;; Section 15.3.2 (racket/udp)
[udp-open-socket (->opt [(-opt -String) (-opt -String)] -UDP-Socket)]
@ -3040,7 +3040,7 @@
[assert (-poly (a b) (cl->*
(Univ (make-pred-ty (list a) Univ b) . -> . b)
(-> (Un a (-val #f)) a)))]
[defined? (->* (list Univ) -Boolean : (-FS (-not-filter -Undefined 0) (-filter -Undefined 0)))]
[defined? (->* (list Univ) -Boolean : (-PS (-not-type 0 -Undefined) (-is-type 0 -Undefined)))]
;; Syntax Manual
;; Section 2.1 (syntax/stx)

2
typed-racket-lib/typed-racket/base-env/class-prims.rkt
View File

@ -282,7 +282,7 @@
[_ #f]))
;; clauses->names : (-> Clause Boolean) Listof<Clause> -> Listof<Id>
;; filter clauses by some property and spit out the names in those clauses
;; prop clauses by some property and spit out the names in those clauses
(define (clauses->names prop clauses [keep-pair? #f])
(apply append
(for/list ([clause (in-list clauses)]

4
typed-racket-lib/typed-racket/base-env/env-lang.rkt
View File

@ -5,7 +5,7 @@
(require (for-syntax racket/base syntax/parse)
(utils tc-utils)
(env init-envs)
(types abbrev numeric-tower union filter-ops))
(types abbrev numeric-tower union 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 filter-ops))
(types-out abbrev numeric-tower union prop-ops))

4
typed-racket-lib/typed-racket/base-env/extra-env-lang.rkt
View File

@ -11,7 +11,7 @@
(for-syntax racket/base
syntax/parse
syntax/stx)
(for-syntax (types abbrev numeric-tower union filter-ops)))
(for-syntax (types abbrev numeric-tower union prop-ops)))
(provide type-environment
(rename-out [-#%module-begin #%module-begin])
@ -20,7 +20,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 filter-ops)))
(for-syntax (types-out abbrev numeric-tower union prop-ops)))
;; syntax classes for type clauses in the type-environment macro
(begin-for-syntax

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

@ -10,7 +10,7 @@
"mvar-env.rkt"
"signature-env.rkt"
(rename-in racket/private/sort [sort raw-sort])
(rep type-rep object-rep filter-rep rep-utils free-variance)
(rep type-rep object-rep prop-rep rep-utils free-variance)
(for-syntax syntax/parse racket/base)
(types abbrev union)
racket/dict racket/list racket/promise
@ -64,21 +64,25 @@
[(? Rep? (app (lambda (v) (hash-ref predefined-type-table (Rep-seq v) #f)) (? values id))) id]
[(Listof: elem-ty)
`(-lst ,(sub elem-ty))]
[(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (Top:) (Top:)) (Empty:)))) #f #f '())))
[(Function: (list (arr: dom (Values: (list (Result: t
(PropSet: (TrueProp:)
(TrueProp:))
(Empty:))))
#f #f '())))
`(simple-> (list ,@(map sub dom)) ,(sub t))]
[(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (TypeFilter: ft pth)
(NotTypeFilter: ft pth))
[(Function: (list (arr: dom (Values: (list (Result: t (PropSet: (TypeProp: pth ft)
(NotTypeProp: pth ft))
(Empty:))))
#f #f '())))
`(make-pred-ty (list ,@(map sub dom)) ,(sub t) ,(sub ft) ,(sub pth))]
[(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (NotTypeFilter: (== -False)
(Path: pth (list 0 0)))
(TypeFilter: (== -False)
(Path: pth (list 0 0))))
[(Function: (list (arr: dom (Values: (list (Result: t (PropSet: (NotTypeProp: (Path: pth (list 0 0))
(== -False))
(TypeProp: (Path: pth (list 0 0))
(== -False)))
(Path: pth (list 0 0)))))
#f #f '())))
`(->acc (list ,@(map sub dom)) ,(sub t) ,(sub pth))]
[(Result: t (FilterSet: (Top:) (Top:)) (Empty:)) `(-result ,(sub t))]
[(Result: t (PropSet: (TrueProp:) (TrueProp:)) (Empty:)) `(-result ,(sub t))]
[(Union: elems) (split-union elems)]
[(Base: n cnt pred _) (int-err "Base type ~a not in predefined-type-table" n)]
[(Name: stx args struct?)
@ -133,10 +137,10 @@
(list ,@(serialize-mapping mapping)))]
[(arr: dom rng rest drest kws)
`(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws))]
[(TypeFilter: t p)
`(make-TypeFilter ,(sub t) ,(sub p))]
[(NotTypeFilter: t p)
`(make-NotTypeFilter ,(sub t) ,(sub p))]
[(TypeProp: o t)
`(make-TypeProp ,(sub o) ,(sub t))]
[(NotTypeProp: o t)
`(make-NotTypeProp ,(sub o) ,(sub t))]
[(Path: p i)
`(make-Path ,(sub p) ,(if (identifier? i)
`(quote-syntax ,i)

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

@ -6,12 +6,12 @@
(contract-req)
(rep object-rep))
(require-for-cond-contract (rep type-rep filter-rep))
(require-for-cond-contract (rep type-rep prop-rep))
;; types is a free-id-table of identifiers to types
;; props is a list of known propositions
(define-struct/cond-contract env ([types immutable-free-id-table?]
[props (listof Filter/c)]
[props (listof Prop?)]
[aliases immutable-free-id-table?])
#:transparent
#:property prop:custom-write
@ -23,8 +23,8 @@
[extend (env? identifier? Type/c . -> . env?)]
[extend/values (env? (listof identifier?) (listof Type/c) . -> . env?)]
[lookup (env? identifier? (identifier? . -> . any) . -> . any)]
[env-props (env? . -> . (listof Filter/c))]
[replace-props (env? (listof Filter/c) . -> . env?)]
[env-props (env? . -> . (listof Prop?))]
[replace-props (env? (listof Prop?) . -> . env?)]
[empty-prop-env env?]
[extend+alias/values (env? (listof identifier?) (listof Type/c) (listof Object?) . -> . env?)]
[lookup-alias (env? identifier? (identifier? . -> . (or/c #f Object?)) . -> . (or/c #f Object?))])

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

@ -11,7 +11,7 @@
(except-in
(combine-in
(utils tc-utils)
(rep free-variance type-rep filter-rep object-rep rep-utils)
(rep free-variance type-rep prop-rep object-rep rep-utils)
(types utils abbrev numeric-tower union subtype resolve
substitute generalize prefab)
(env index-env tvar-env))
@ -224,23 +224,23 @@
(substitute (make-F var) v ty*))))
(define/cond-contract (cgen/filter context s t)
(context? Filter? Filter? . -> . (or/c #f cset?))
(define/cond-contract (cgen/prop context s t)
(context? Prop? Prop? . -> . (or/c #f cset?))
(match* (s t)
[(e e) (empty-cset/context context)]
[(e (Top:)) (empty-cset/context context)]
[(e (TrueProp:)) (empty-cset/context context)]
;; FIXME - is there something to be said about the logical ones?
[((TypeFilter: s p) (TypeFilter: t p)) (cgen/inv context s t)]
[((NotTypeFilter: s p) (NotTypeFilter: t p)) (cgen/inv context s t)]
[((TypeProp: o s) (TypeProp: o t)) (cgen/inv context s t)]
[((NotTypeProp: o s) (NotTypeProp: o t)) (cgen/inv context s t)]
[(_ _) #f]))
;; s and t must be *latent* filter sets
(define/cond-contract (cgen/filter-set context s t)
(context? FilterSet? FilterSet? . -> . (or/c #f cset?))
;; s and t must be *latent* prop sets
(define/cond-contract (cgen/prop-set context s t)
(context? PropSet? PropSet? . -> . (or/c #f cset?))
(match* (s t)
[(e e) (empty-cset/context context)]
[((FilterSet: s+ s-) (FilterSet: t+ t-))
(% cset-meet (cgen/filter context s+ t+) (cgen/filter context s- t-))]
[((PropSet: p+ p-) (PropSet: q+ q-))
(% cset-meet (cgen/prop context p+ q+) (cgen/prop context p- q-))]
[(_ _) #f]))
(define/cond-contract (cgen/object context s t)
@ -439,26 +439,26 @@
;; CG-Top
[(_ (Univ:)) empty]
;; AnyValues
[((AnyValues: s-f) (AnyValues: t-f))
(cgen/filter context s-f t-f)]
[((AnyValues: p) (AnyValues: q))
(cgen/prop context p q)]
[((or (Values: (list (Result: _ fs _) ...))
(ValuesDots: (list (Result: _ fs _) ...) _ _))
(AnyValues: t-f))
[((or (Values: (list (Result: _ psets _) ...))
(ValuesDots: (list (Result: _ psets _) ...) _ _))
(AnyValues: q))
(cset-join
(filter identity
(for/list ([f (in-list fs)])
(match f
[(FilterSet: f+ f-)
(% cset-meet (cgen/filter context f+ t-f) (cgen/filter context f- t-f))]))))]
(for/list ([pset (in-list psets)])
(match pset
[(PropSet: p+ p-)
(% cset-meet (cgen/prop context p+ q) (cgen/prop context p- q))]))))]
;; check all non Type/c first so that calling subtype is safe
;; check each element
[((Result: s f-s o-s)
(Result: t f-t o-t))
[((Result: s pset-s o-s)
(Result: t pset-t o-t))
(% cset-meet (cg s t)
(cgen/filter-set context f-s f-t)
(cgen/prop-set context pset-s pset-t)
(cgen/object context o-s o-t))]
;; Values just delegate to cgen/seq, except special handling for -Bottom.

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

@ -15,13 +15,13 @@
(for/or ([e (in-list (append* (map fv ts)))])
(memq e V)))
;; get-filters : SomeValues -> FilterSet
;; extract filters out of the range of a function type
(define (get-filters rng)
;; get-propset : SomeValues -> PropSet
;; extract prop sets out of the range of a function type
(define (get-propsets rng)
(match rng
[(AnyValues: f) (list (-FS f f))]
[(Values: (list (Result: _ lf _) ...)) lf]
[(ValuesDots: (list (Result: _ lf _) ...) _ _) lf]))
[(AnyValues: p) (list (-PS p p))]
[(Values: (list (Result: _ propsets _) ...)) propsets]
[(ValuesDots: (list (Result: _ propsets _) ...) _ _) propsets]))
(begin-encourage-inline
@ -43,7 +43,7 @@
(match arr
[(arr: dom rng rest drest kws)
(cond
[(apply V-in? V (get-filters rng))
[(apply V-in? V (get-propsets rng))
#f]
[(and drest (memq (cdr drest) V))
(make-arr (map contra dom)
@ -63,7 +63,7 @@
[(Function: arrs)
(make-Function (filter-map arr-change arrs))]
[(? structural?) (structural-map T structural-recur)]
[(? Filter?) ((sub-f co) T)]
[(? Prop?) ((sub-f co) T)]
[(? Object?) ((sub-o co) T)]
[(? Type?) ((sub-t co) T)]))
(define (var-promote T V)

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

@ -4,7 +4,7 @@
(require "../utils/utils.rkt"
(except-in (rep type-rep object-rep) make-arr)
(rename-in (types abbrev union utils filter-ops resolve
(rename-in (types abbrev union utils prop-ops resolve
classes prefab signatures)
[make-arr* make-arr])
(utils tc-utils stxclass-util literal-syntax-class)
@ -227,7 +227,7 @@
#:attributes (type)
(pattern (~optional (~seq #:rest type:non-keyword-ty))))
;; syntax classes for filters, objects, and related things
;; syntax classes for props, objects, and related things
(define-syntax-class path-elem
#:description "path element"
(pattern :car^
@ -244,8 +244,8 @@
#:description "!"
(pattern (~datum !)))
(define-splicing-syntax-class simple-latent-filter
#:description "latent filter"
(define-splicing-syntax-class simple-latent-prop
#:description "latent prop"
(pattern (~seq t:expr :@ pe:path-elem ...)
#:attr type (parse-type #'t)
#:attr path (attribute pe.pe))
@ -254,54 +254,54 @@
#:attr path '()))
(define-syntax-class (prop doms)
#:description "filter proposition"
#:description "proposition"
#:attributes (prop)
(pattern :Top^ #:attr prop -top)
(pattern :Bot^ #:attr prop -bot)
(pattern :Top^ #:attr prop -tt)
(pattern :Bot^ #:attr prop -ff)
;; Here is wrong check
(pattern (t:expr :@ ~! pe:path-elem ... (~var o (filter-object doms)))
#:attr prop (-filter (parse-type #'t) (-acc-path (attribute pe.pe) (attribute o.obj))))
(pattern (t:expr :@ ~! pe:path-elem ... (~var o (prop-object doms)))
#:attr prop (-is-type (-acc-path (attribute pe.pe) (attribute o.obj)) (parse-type #'t)))
;; Here is wrong check
(pattern (:! t:expr :@ ~! pe:path-elem ... (~var o (filter-object doms)))
#:attr prop (-not-filter (parse-type #'t) (-acc-path (attribute pe.pe) (attribute o.obj))))
(pattern (:! t:expr :@ ~! pe:path-elem ... (~var o (prop-object doms)))
#:attr prop (-not-type (-acc-path (attribute pe.pe) (attribute o.obj)) (parse-type #'t)))
(pattern (:! t:expr)
#:attr prop (-not-filter (parse-type #'t) 0))
#:attr prop (-not-type 0 (parse-type #'t)))
(pattern ((~datum and) (~var p (prop doms)) ...)
#:attr prop (apply -and (attribute p.prop)))
(pattern ((~datum or) (~var p (prop doms)) ...)
#:attr prop (apply -or (attribute p.prop)))
(pattern ((~literal implies) (~var p1 (prop doms)) (~var p2 (prop doms)))
#:attr prop (-imp (attribute p1.prop) (attribute p2.prop)))
#:attr prop (-or (negate-prop (attribute p1.prop)) (attribute p2.prop)))
(pattern t:expr
#:attr prop (-filter (parse-type #'t) 0)))
#:attr prop (-is-type 0 (parse-type #'t))))
(define-splicing-syntax-class (filter-object doms)
#:description "filter object"
(define-splicing-syntax-class (prop-object doms)
#:description "prop object"
#:attributes (obj)
(pattern i:id
#:fail-unless (identifier-binding #'i)
"Filters for predicates may not reference identifiers that are unbound"
"Propositions for predicates may not reference identifiers that are unbound"
#:fail-when (is-var-mutated? #'i)
"Filters for predicates may not reference identifiers that are mutated"
"Propositions for predicates may not reference identifiers that are mutated"
#:attr obj (-id-path #'i))
(pattern idx:nat
#:do [(define arg (syntax-e #'idx))]
#:fail-unless (< arg (length doms))
(format "Filter proposition's object index ~a is larger than argument length ~a"
(format "Proposition's object index ~a is larger than argument length ~a"
arg (length doms))
#:attr obj (-arg-path arg 0))
(pattern (~seq depth-idx:nat idx:nat)
#:do [(define arg (syntax-e #'idx))
(define depth (syntax-e #'depth-idx))]
#:fail-unless (<= depth (length (current-arities)))
(format "Index ~a used in a filter, but the use is only within ~a enclosing functions"
(format "Index ~a used in a proposition, but the use is only within ~a enclosing functions"
depth (length (current-arities)))
#:do [(define actual-arg
(if (zero? depth)
(length doms)
(list-ref (current-arities) (sub1 depth))))]
#:fail-unless (< arg actual-arg)
(format "Filter proposition's object index ~a is larger than argument length ~a"
(format "Proposition's object index ~a is larger than argument length ~a"
depth actual-arg)
#:attr obj (-arg-path arg (syntax-e #'depth-idx))))
@ -498,9 +498,9 @@
(list (make-arr
doms
(parse-type (syntax/loc stx (rest-dom ...))))))))]
[(~or (:->^ dom rng :colon^ latent:simple-latent-filter)
(dom :->^ rng :colon^ latent:simple-latent-filter))
;; use parse-type instead of parse-values-type because we need to add the filters from the pred-ty
[(~or (:->^ dom rng :colon^ latent:simple-latent-prop)
(dom :->^ rng :colon^ latent:simple-latent-prop))
;; use parse-type instead of parse-values-type because we need to add the props from the pred-ty
(with-arity 1
(make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (attribute latent.type)
(-acc-path (attribute latent.path) (-arg-path 0))))]
@ -560,11 +560,11 @@
:colon^ (~var latent (full-latent (syntax->list #'(dom ...)))))
(dom:non-keyword-ty ... :->^ rng:expr
~! :colon^ (~var latent (full-latent (syntax->list #'(dom ...))))))
;; use parse-type instead of parse-values-type because we need to add the filters from the pred-ty
;; use parse-type instead of parse-values-type because we need to add the props from the pred-ty
(with-arity (length (syntax->list #'(dom ...)))
(->* (parse-types #'(dom ...))
(parse-type #'rng)
: (-FS (attribute latent.positive) (attribute latent.negative))
: (-PS (attribute latent.positive) (attribute latent.negative))
: (attribute latent.object)))]
[(:->*^ (~var mand (->*-args #t))
(~optional (~var opt (->*-args #f))
@ -924,11 +924,12 @@
(define (parse-tc-results stx)
(syntax-parse stx
[((~or :Values^ :values^) t ...)
(define empties (stx-map (λ (x) #f) #'(t ...)))
(ret (parse-types #'(t ...))
(stx-map (lambda (x) -no-filter) #'(t ...))
(stx-map (lambda (x) -no-obj) #'(t ...)))]
[:AnyValues^ (tc-any-results -no-filter)]
[t (ret (parse-type #'t) -no-filter -no-obj)]))
empties
empties)]
[:AnyValues^ (tc-any-results #f)]
[t (ret (parse-type #'t) #f #f)]))
(define parse-type/id (parse/id parse-type))

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

@ -5,7 +5,7 @@
(require
"../utils/utils.rkt"
syntax/parse
(rep type-rep filter-rep object-rep)
(rep type-rep prop-rep object-rep)
(utils tc-utils)
(env type-name-env row-constraint-env)
(rep rep-utils)
@ -613,17 +613,21 @@
;; and call the given thunk or raise an error
(define (handle-range arr convert-arr)
(match arr
;; functions with no filters or objects
[(arr: dom (Values: (list (Result: rngs (FilterSet: (Top:) (Top:)) (Empty:)) ...)) rst drst kws)
;; functions with no props or objects
[(arr: dom (Values: (list (Result: rngs
(PropSet: (TrueProp:)
(TrueProp:))
(Empty:)) ...))
rst drst kws)
(convert-arr)]
;; Functions that don't return
[(arr: dom (Values: (list (Result: (== -Bottom) _ _) ...)) rst drst kws)
(convert-arr)]
;; functions with filters or objects
;; functions with props or objects
[(arr: dom (Values: (list (Result: rngs _ _) ...)) rst drst kws)
(if (from-untyped? typed-side)
(fail #:reason (~a "cannot generate contract for function type"
" with filters or objects."))
" with props or objects."))
(convert-arr))]
[(arr: dom (? ValuesDots?) rst drst kws)
(fail #:reason (~a "cannot generate contract for function type"
@ -797,7 +801,7 @@
(let/ec escape
(let loop ([type type])
(type-case
(#:Type loop #:Filter (sub-f loop) #:Object (sub-o loop))
(#:Type loop #:Prop (sub-f loop) #:Object (sub-o loop))
type
[#:App arg _ _
(match arg

70
typed-racket-lib/typed-racket/rep/filter-rep.rkt
View File

@ -1,70 +1,4 @@
#lang racket/base
(require "../utils/utils.rkt" "rep-utils.rkt" "free-variance.rkt")
(provide hash-name filter-equal?)
(begin-for-cond-contract
(require racket/contract/base racket/lazy-require)
(lazy-require ["type-rep.rkt" (Type/c Univ? Bottom?)]
["object-rep.rkt" (Path?)]))
(provide-for-cond-contract Filter/c FilterSet/c name-ref/c)
(define-for-cond-contract (Filter/c-predicate? e)
(and (Filter? e) (not (NoFilter? e)) (not (FilterSet? e))))
(define-for-cond-contract Filter/c
(flat-named-contract 'Filter Filter/c-predicate?))
(define-for-cond-contract FilterSet/c
(flat-named-contract
'FilterSet
(λ (e) (or (FilterSet? e) (NoFilter? e)))))
;; A Name-Ref is any value that represents an object.
;; As an identifier, it represents a free variable in the environment
;; As a list, it represents a De Bruijn indexed bound variable
(define-for-cond-contract name-ref/c
(or/c identifier? (list/c integer? integer?)))
(define (hash-name v) (if (identifier? v) (hash-id v) (list v)))
(define-for-cond-contract ((length>=/c len) l)
(and (list? l)
(>= (length l) len)))
(def-filter Bot () [#:fold-rhs #:base])
(def-filter Top () [#:fold-rhs #:base])
(def-filter TypeFilter ([t (and/c Type/c (not/c Univ?) (not/c Bottom?))] [p Path?])
[#:intern (list (Rep-seq t) (Rep-seq p))]
[#:frees (λ (f) (combine-frees (map f (list t p))))]
[#:fold-rhs (*TypeFilter (type-rec-id t) (object-rec-id p))])
(def-filter NotTypeFilter ([t (and/c Type/c (not/c Univ?) (not/c Bottom?))] [p Path?])
[#:intern (list (Rep-seq t) (Rep-seq p))]
[#:frees (λ (f) (combine-frees (map f (list t p))))]
[#:fold-rhs (*NotTypeFilter (type-rec-id t) (object-rec-id p))])
;; implication
(def-filter ImpFilter ([a Filter/c] [c Filter/c]))
(def-filter OrFilter ([fs (and/c (length>=/c 2)
(listof (or/c TypeFilter? NotTypeFilter? ImpFilter?)))])
[#:intern (map Rep-seq fs)]
[#:fold-rhs (*OrFilter (map filter-rec-id fs))]
[#:frees (λ (f) (combine-frees (map f fs)))])
(def-filter AndFilter ([fs (and/c (length>=/c 2)
(listof (or/c OrFilter? TypeFilter? NotTypeFilter? ImpFilter?)))])
[#:intern (map Rep-seq fs)]
[#:fold-rhs (*AndFilter (map filter-rec-id fs))]
[#:frees (λ (f) (combine-frees (map f fs)))])
(def-filter FilterSet ([thn Filter/c] [els Filter/c])
[#:fold-rhs (*FilterSet (filter-rec-id thn) (filter-rec-id els))])
;; represents no info about the filters of this expression
;; should only be used for parsing type annotations and expected types
(def-filter NoFilter () [#:fold-rhs #:base])
(define (filter-equal? a b) (= (Rep-seq a) (Rep-seq b)))
(require "prop-rep.rkt")
(provide (all-from-out "prop-rep.rkt"))

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

@ -5,7 +5,7 @@
;;
;; See "Logical Types for Untyped Languages" pg.3
(require "rep-utils.rkt" "free-variance.rkt" "filter-rep.rkt" "../utils/utils.rkt" (contract-req))
(require "rep-utils.rkt" "free-variance.rkt" "prop-rep.rkt" "../utils/utils.rkt" (contract-req))
(provide object-equal?)
(def-pathelem CarPE () [#:fold-rhs #:base])
@ -25,16 +25,4 @@
[#:frees (λ (f) (combine-frees (map f p)))]
[#:fold-rhs (*Path (map pathelem-rec-id p) v)])
;; represents no info about the object of this expression
;; should only be used for parsing type annotations and expected types
(def-object NoObject () [#:fold-rhs #:base])
(define (object-equal? o1 o2) (= (Rep-seq o1) (Rep-seq o2)))
#|
(dlo LEmpty () [#:fold-rhs #:base])
(dlo LPath ([p (listof PathElem?)] [idx index/c])
[#:frees (λ (f) (combine-frees (map f p)))]
[#:fold-rhs (*LPath (map pathelem-rec-id p) idx)])
|#

56
typed-racket-lib/typed-racket/rep/prop-rep.rkt Normal file
View File

@ -0,0 +1,56 @@
#lang racket/base
(require "../utils/utils.rkt" "rep-utils.rkt" "free-variance.rkt")
(provide hash-name prop-equal?)
(begin-for-cond-contract
(require racket/contract/base racket/lazy-require)
(lazy-require ["type-rep.rkt" (Type/c Univ? Bottom?)]
["object-rep.rkt" (Path?)]))
(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 list, it represents a De Bruijn indexed bound variable
(define-for-cond-contract name-ref/c
(or/c identifier? (list/c integer? integer?)))
(define (hash-name v) (if (identifier? v) (hash-id v) (list v)))
(define-for-cond-contract ((length>=/c len) l)
(and (list? l)
(>= (length l) len)))
;; the trivially "true" proposition
(def-prop TrueProp () [#:fold-rhs #:base])
;; the absurd, "false" proposition
(def-prop FalseProp () [#:fold-rhs #:base])
(def-prop TypeProp ([p Path?] [t (and/c Type/c (not/c Univ?) (not/c Bottom?))])
[#:intern (list (Rep-seq t) (Rep-seq p))]
[#:frees (λ (f) (combine-frees (map f (list t p))))]
[#:fold-rhs (*TypeProp (object-rec-id p) (type-rec-id t))])
(def-prop NotTypeProp ([p Path?] [t (and/c Type/c (not/c Univ?) (not/c Bottom?))])
[#:intern (list (Rep-seq t) (Rep-seq p))]
[#:frees (λ (f) (combine-frees (map f (list t p))))]
[#:fold-rhs (*NotTypeProp (object-rec-id p) (type-rec-id t))])
(def-prop OrProp ([fs (and/c (length>=/c 2)
(listof (or/c TypeProp? NotTypeProp?)))])
[#:intern (map Rep-seq fs)]
[#:fold-rhs (*OrProp (map prop-rec-id fs))]
[#:frees (λ (f) (combine-frees (map f fs)))])
(def-prop AndProp ([fs (and/c (length>=/c 2)
(listof (or/c OrProp? TypeProp? NotTypeProp?)))])
[#:intern (map Rep-seq fs)]
[#:fold-rhs (*AndProp (map prop-rec-id fs))]
[#:frees (λ (f) (combine-frees (map f fs)))])
(def-prop PropSet ([thn Prop?] [els Prop?])
[#:fold-rhs (*PropSet (prop-rec-id thn) (prop-rec-id els))])
(define (prop-equal? a b) (= (Rep-seq a) (Rep-seq b)))

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

@ -20,7 +20,7 @@
(lazy-require
["../types/printer.rkt" (print-type print-filter print-object print-pathelem)])
["../types/printer.rkt" (print-type print-prop print-object print-pathelem)])
(provide == defintern hash-id (for-syntax fold-target))
@ -135,7 +135,7 @@
#:defaults
([frees.f1 (combiner #'Rep-free-vars #'flds.fields)]
[frees.f2 (combiner #'Rep-free-idxs #'flds.fields)]))
;; This tricky beast is for defining the type/filter/etc.'s
;; This tricky beast is for defining the type/prop/etc.'s
;; part of the fold. The make-prim-type's given
;; rec-ids are bound in this expression's context.
(~optional [#:fold-rhs (~var fold-rhs (fold-pat #'name.fold))]
@ -204,7 +204,7 @@
provides))])))
;; rec-ids are identifiers that are of the folded type, so we recur on them.
;; kws is e.g. '(#:Type #:Filter #:Object #:PathElem)
;; kws is e.g. '(#:Type #:Prop #:Object #:PathElem)
(define-for-syntax (mk-fold hashtable rec-ids kws)
(lambda (stx)
(define new-hashtable (make-hasheq))
@ -217,7 +217,7 @@
(syntax/loc this-syntax (pats ...))
(lambda () #'e)
this-syntax))
;; Match on a type (or filter etc) case with keyword k
;; Match on a type (or prop etc) case with keyword k
;; pats are the unignored patterns (say for rator rand)
;; and e is the expression that will run as fold-rhs.
(pattern
@ -351,18 +351,18 @@
;; [unsyntax (*1)]
(mk-fold ht
rec-ids
;; '(#:Type #:Filter #:Object #:PathElem)
;; '(#:Type #:Prop #:Object #:PathElem)
'(i.kw ...)))
(list i.hashtable ...))))))]))
(make-prim-type [Type def-type #:Type type-case print-type type-name-ht type-rec-id #:key]
[Filter def-filter #:Filter filter-case print-filter filter-name-ht filter-rec-id]
[Prop def-prop #:Prop prop-case print-prop prop-name-ht prop-rec-id]
[Object def-object #:Object object-case print-object object-name-ht object-rec-id]
[PathElem def-pathelem #:PathElem pathelem-case print-pathelem pathelem-name-ht pathelem-rec-id])
(define (Rep-values rep)
(match rep
[(? (lambda (e) (or (Filter? e)
[(? (lambda (e) (or (Prop? e)
(Object? e)
(PathElem? e)))
(app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx vals)))
@ -386,7 +386,7 @@
(provide/cond-contract
[rename rep-equal? type-equal? (Type? Type? . -> . boolean?)]
[rename rep<? type<? (Type? Type? . -> . boolean?)]
[rename rep<? filter<? (Filter? Filter? . -> . boolean?)]
[rename rep<? prop<? (Prop? Prop? . -> . boolean?)]
[struct Rep ([seq exact-nonnegative-integer?]
[free-vars (hash/c symbol? variance?)]
[free-idxs (hash/c symbol? variance?)]

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

@ -7,7 +7,7 @@
;; TODO use contract-req
(require (utils tc-utils)
"rep-utils.rkt" "object-rep.rkt" "filter-rep.rkt" "free-variance.rkt"
"rep-utils.rkt" "object-rep.rkt" "prop-rep.rkt" "free-variance.rkt"
racket/match racket/list
racket/contract
racket/lazy-require
@ -22,7 +22,7 @@
Mu-unsafe: Poly-unsafe:
PolyDots-unsafe:
Mu? Poly? PolyDots? PolyRow?
Filter? Object?
Prop? Object?
Type/c Type/c?
Values/c SomeValues/c
Bottom?
@ -274,9 +274,9 @@
[#:frees (λ (f) (f ty))]
[#:fold-rhs (*Keyword kw (type-rec-id ty) required?)])
(def-type Result ([t Type/c] [f FilterSet?] [o Object?])
(def-type Result ([t Type/c] [f PropSet?] [o Object?])
[#:frees (λ (frees) (combine-frees (map frees (list t f o))))]
[#:fold-rhs (*Result (type-rec-id t) (filter-rec-id f) (object-rec-id o))])
[#:fold-rhs (*Result (type-rec-id t) (prop-rec-id f) (object-rec-id o))])
(def-type Values ([rs (listof Result?)])
[#:intern (map Rep-seq rs)]
@ -284,7 +284,7 @@
[#:fold-rhs (*Values (map type-rec-id rs))])
(def-type AnyValues ([f Filter/c])
(def-type AnyValues ([f Prop?])
[#:fold-rhs #:base])
(def-type ValuesDots ([rs (listof Result?)] [dty Type/c] [dbound (or/c symbol? natural-number/c)])
@ -617,10 +617,10 @@
(define ((sub-f st) e)
(filter-case (#:Type st
#:Filter (sub-f st)
#:PathElem (sub-pe st))
e))
(prop-case (#:Type st
#:Prop (sub-f st)
#:PathElem (sub-pe st))
e))
(define ((sub-o st) e)
@ -636,7 +636,7 @@
(define ((sub-t st) e)
(type-case (#:Type st
#:Filter (sub-f st))
#:Prop (sub-f st))
e))
@ -657,7 +657,7 @@
(f (+ (cdr pr) outer)))]
[else default]))
(type-case
(#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb))
(#:Type sb #:Prop (sub-f sb) #:Object (sub-o sb))
ty
[#:F name* (transform name* *B ty)]
;; necessary to avoid infinite loops
@ -711,7 +711,7 @@
(define (sb t) (loop outer t))
(define sf (sub-f sb))
(type-case
(#:Type sb #:Filter sf #:Object (sub-o sb))
(#:Type sb #:Prop sf #:Object (sub-o sb))
ty
[#:B idx (transform idx values ty)]
;; necessary to avoid infinite loops

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

@ -3,9 +3,9 @@
(require "../utils/utils.rkt"
racket/match (prefix-in - (contract-req))
racket/format
(types utils union subtype filter-ops abbrev)
(types utils union subtype prop-ops abbrev)
(utils tc-utils)
(rep type-rep object-rep filter-rep)
(rep type-rep object-rep prop-rep)
(typecheck error-message))
(provide/cond-contract
@ -21,7 +21,7 @@
(define (print-object o)
(match o
[(or (NoObject:) (Empty:)) "no object"]
[(or #f (Empty:)) "no object"]
[_ (format "object ~a" o)]))
;; If expected is #f, then just return tr1
@ -45,37 +45,36 @@
(value-string expected) (value-string actual)
"mismatch in number of values"))
;; fix-filter: FilterSet [FilterSet] -> FilterSet
;; Turns NoFilter into the actual filter; leaves other filters alone.
(define (fix-filter f [f2 -top-filter])
(match f
[(NoFilter:) f2]
[else f]))
;; fix-props:
;; PropSet [PropSet] -> PropSet
;; or
;; Prop [Prop] -> Prop
;; Turns #f prop/propset into the actual prop; leaves other props alone.
(define (fix-props p1 [p2 -tt-propset])
(or p1 p2))
;; fix-object: Object [Object] -> Object
;; Turns NoObject into the actual object; leaves other objects alone.
(define (fix-object o [o2 -empty-obj])
(match o
[(NoObject:) o2]
[else o]))
;; Turns #f into the actual object; leaves other objects alone.
(define (fix-object o1 [o2 -empty-obj])
(or o1 o2))
;; fix-results: tc-results -> tc-results
;; Turns NoObject/NoFilter into the Empty/TopFilter
;; Turns #f Prop or Obj into the Empty/Trivial
(define (fix-results r)
(match r
[(tc-any-results: f) (tc-any-results (fix-filter f -top))]
[(tc-results: ts fs os)
(ret ts (map fix-filter fs) (map fix-object os))]
[(tc-results: ts fs os dty dbound)
(ret ts (map fix-filter fs) (map fix-object os) dty dbound)]))
[(tc-any-results: f) (tc-any-results (fix-props f -tt))]
[(tc-results: ts ps os)
(ret ts (map fix-props ps) (map fix-object os))]
[(tc-results: ts ps os dty dbound)
(ret ts (map fix-props ps) (map fix-object os) dty dbound)]))
(define (fix-results/bottom r)
(match r
[(tc-any-results: f) (tc-any-results (fix-filter f -bot))]
[(tc-results: ts fs os)
(ret ts (for/list ([f fs]) (fix-filter f -bot-filter)) (map fix-object os))]
[(tc-results: ts fs os dty dbound)
(ret ts (for/list ([f fs]) (fix-filter f -bot-filter)) (map fix-object os) dty dbound)]))
[(tc-any-results: f) (tc-any-results (fix-props f -ff))]
[(tc-results: ts ps os)
(ret ts (for/list ([p ps]) (fix-props p -ff-propset)) (map fix-object os))]
[(tc-results: ts ps os dty dbound)
(ret ts (for/list ([p ps]) (fix-props p -ff-propset)) (map fix-object os) dty dbound)]))
@ -84,74 +83,74 @@
;; (Type Results -> Type)
;; (Type Type -> Type))
(define (check-below tr1 expected)
(define (filter-set-better? f1 f2)
(match* (f1 f2)
[(f f) #t]
[(f (NoFilter:)) #t]
[((FilterSet: f1+ f1-) (FilterSet: f2+ f2-))
(and (implied-atomic? f2+ f1+)
(implied-atomic? f2- f1-))]
(define (prop-set-better? p1 p2)
(match* (p1 p2)
[(p p) #t]
[(p #f) #t]
[((PropSet: p1+ p1-) (PropSet: p2+ p2-))
(and (implies-atomic? p1+ p2+)
(implies-atomic? p1- p2-))]
[(_ _) #f]))
(define (object-better? o1 o2)
(match* (o1 o2)
[(o o) #t]
[(o (or (NoObject:) (Empty:))) #t]
[(o (or #f (Empty:))) #t]
[(_ _) #f]))
(define (filter-better? f1 f2)
(or (NoFilter? f2)
(implied-atomic? f2 f1)))
(define (prop-better? p1 p2)
(or (not p2)
(implies-atomic? 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 filters and objects in the actual value because they would never be about a value
;; 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))))) _)
(fix-results/bottom expected)]
[((tc-any-results: f1) (tc-any-results: f2))
(unless (filter-better? f1 f2)
(type-mismatch f2 f1 "mismatch in filter"))
(tc-any-results (fix-filter f2 f1))]
[((tc-any-results: p1) (tc-any-results: p2))
(unless (prop-better? p1 p2)
(type-mismatch p2 p1 "mismatch in proposition"))
(tc-any-results (fix-props p2 p1))]
[((or (tc-results: _ (list (FilterSet: fs+ fs-) ...) _)
(tc-results: _ (list (FilterSet: fs+ fs-) ...) _ _ _))
(tc-any-results: f2))
(define merged-filter (apply -and (map -or fs+ fs-)))
(unless (filter-better? merged-filter f2)
(type-mismatch f2 merged-filter "mismatch in filter"))
(tc-any-results (fix-filter f2 merged-filter))]
[((or (tc-results: _ (list (PropSet: fs+ fs-) ...) _)
(tc-results: _ (list (PropSet: fs+ fs-) ...) _ _ _))
(tc-any-results: p2))
(define merged-prop (apply -and (map -or fs+ fs-)))
(unless (prop-better? merged-prop p2)
(type-mismatch p2 merged-prop "mismatch in proposition"))
(tc-any-results (fix-props p2 merged-prop))]
[((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2))
[((tc-result1: t1 p1 o1) (tc-result1: t2 p2 o2))
(cond
[(not (subtype t1 t2))
(expected-but-got t2 t1)]
[(and (not (filter-set-better? f1 f2))
[(and (not (prop-set-better? p1 p2))
(object-better? o1 o2))
(type-mismatch f2 f1 "mismatch in filter")]
[(and (filter-set-better? f1 f2)
(type-mismatch p2 p1 "mismatch in proposition")]
[(and (prop-set-better? p1 p2)
(not (object-better? o1 o2)))
(type-mismatch (print-object o2) (print-object o1) "mismatch in object")]
[(and (not (filter-set-better? f1 f2))
[(and (not (prop-set-better? p1 p2))
(not (object-better? o1 o2)))
(type-mismatch (format "`~a' and `~a'" f2 (print-object o2))
(format "`~a' and `~a'" f1 (print-object o1))
"mismatch in filter and object")])
(ret t2 (fix-filter f2 f1) (fix-object o2 o1))]
(type-mismatch (format "`~a' and `~a'" p2 (print-object o2))
(format "`~a' and `~a'" p1 (print-object o1))
"mismatch in proposition and object")])
(ret t2 (fix-props p2 p1) (fix-object o2 o1))]
;; case where expected is like (Values a ... a) but got something else
[((tc-results: t1 f1 o1) (tc-results: t2 f2 o2 dty dbound))
[((tc-results: t1 p1 o1) (tc-results: t2 p2 o2 dty dbound))
(value-mismatch expected tr1)
(fix-results expected)]
;; case where you have (Values a ... a) but expected something else
[((tc-results: t1 f1 o1 dty dbound) (tc-results: t2 f2 o2))
[((tc-results: t1 p1 o1 dty dbound) (tc-results: t2 p2 o2))
(value-mismatch expected tr1)
(fix-results expected)]
[((tc-results: t1 f1 o1 dty1 dbound)
(tc-results: t2 (list (or (NoFilter:) (FilterSet: (Top:) (Top:))) ...)
(list (or (NoObject:) (Empty:)) ...) dty2 dbound))
[((tc-results: t1 p1 o1 dty1 dbound)
(tc-results: t2 (list (or #f (PropSet: (TrueProp:) (TrueProp:))) ...)
(list (or #f (Empty:)) ...) dty2 dbound))
(cond
[(= (length t1) (length t2))
(unless (andmap subtype t1 t2)
@ -162,7 +161,7 @@
(value-mismatch expected tr1)])
(fix-results expected)]
[((tc-results: t1 f1 o1 dty1 dbound) (tc-results: t2 f2 o2 dty2 dbound))
[((tc-results: t1 p1 o1 dty1 dbound) (tc-results: t2 p2 o2 dty2 dbound))
(cond
[(= (length t1) (length t2))
(unless (andmap subtype t1 t2)
@ -173,9 +172,9 @@
(value-mismatch expected tr1)])
(fix-results expected)]
[((tc-results: t1 f1 o1)
(tc-results: t2 (list (or (NoFilter:) (FilterSet: (Top:) (Top:))) ...)
(list (or (NoObject:) (Empty:)) ...)))
[((tc-results: t1 p1 o1)
(tc-results: t2 (list (or #f (PropSet: (TrueProp:) (TrueProp:))) ...)
(list (or #f (Empty:)) ...)))
(unless (= (length t1) (length t2))
(value-mismatch expected tr1))
(unless (for/and ([t (in-list t1)] [s (in-list t2)]) (subtype t s))
@ -189,7 +188,7 @@
(expected-but-got (stringify t2) (stringify t1)))
(fix-results expected)]
[((tc-results: t1 f1 o1) (tc-results: t2 f2 o2)) (=> continue)
[((tc-results: t1 p1 o1) (tc-results: t2 p2 o2)) (=> continue)
(if (= (length t1) (length t2))
(continue)
(value-mismatch expected tr1))
@ -204,5 +203,5 @@
(expected-but-got t2 t1))
expected]
[((tc-results: ts fs os dty dbound) (tc-results: ts* fs* os* dty* dbound*))
(int-err "dotted types with different bounds/filters/objects in check-below nyi: ~a ~a" tr1 expected)]
(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)]))

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

@ -461,7 +461,7 @@
(define-values (alias-names alias-map) (get-type-alias-info type-aliases))
(register-all-type-aliases alias-names alias-map)
;; Filter top level expressions into several groups, each processed
;; Prop top level expressions into several groups, each processed
;; into appropriate data structures
;;
;; Augment annotations go in their own table, because they're
@ -983,7 +983,7 @@
(do-timestamp (format "finished method ~a" external-name))
(cons (list external-name pre-method-type) checked)]
;; Only try to type-check if these names are in the
;; filter when it's provided. This allows us to, say, only
;; prop when it's provided. This allows us to, say, only
;; type-check pubments/augments.
[(set-member? names-to-check external-name)
(do-timestamp (format "started checking method ~a" external-name))

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

@ -11,7 +11,7 @@
(utils tc-utils)
(for-syntax racket/base syntax/parse)
(for-template racket/base)
(rep type-rep filter-rep object-rep))
(rep type-rep prop-rep object-rep))
(import tc-if^ tc-lambda^ tc-app^ tc-let^ tc-expr^)
(export check-subforms^)
@ -42,14 +42,14 @@
;; syntax tc-result1 type -> tc-results
;; The result of applying the function to a single argument of the type of its first argument
(define (get-range-result stx t filter-type)
(define (get-range-result stx t prop-type)
(let loop ((t t))
(match t
[(Function: (list _ ... (arr: (list arg1) _ _ #f (list (Keyword: _ _ #f) ...)) _ ...))
#:when (subtype filter-type arg1)
#:when (subtype prop-type arg1)
(tc/funapp #'here #'(here) t (list (ret arg1)) #f)]
[(Function: (list _ ... (arr: '() _ (? values rest) #f (list (Keyword: _ _ #f) ...)) _ ...))
#:when (subtype filter-type rest)
#:when (subtype prop-type rest)
(tc/funapp #'here #'(here) t (list (ret rest)) #f)]
[(? needs-resolving? t)
(loop (resolve t))]
@ -58,17 +58,17 @@
;; This clause should raise an error via the check-below test
[_
(cond [;; a redundant test, but it ensures an error message below
(not (subtype t (-> filter-type Univ)))
(not (subtype t (-> prop-type Univ)))
(parameterize ([current-orig-stx stx])
(check-below t (-> filter-type Univ)))]
[else (int-err "get-range-result: should not happen. type ~a filter ~a"
t filter-type)])
(check-below t (-> prop-type Univ)))]
[else (int-err "get-range-result: should not happen. type ~a prop ~a"
t prop-type)])
(ret (Un))])))
;; Syntax Type -> (Option Type)
;; Extract the type for the filter in a predicate type, or #f if
;; Extract the type for the prop in a predicate type, or #f if
;; the type is an invalid predicate type.
(define (get-filter-type stx pred-type)
(define (get-prop-type stx pred-type)
(cond [;; make sure the predicate has an appropriate type
(subtype pred-type (-> Univ Univ))
(define fun-type
@ -78,10 +78,10 @@
(match fun-type
;; FIXME: Almost all predicates fall into this case, but it may
;; be worth being more precise here for some rare code.
[(PredicateFilter: fs)
(match fs
[(FilterSet: (TypeFilter: ft (Path: '() '(0 0))) _) ft]
[(Bot:) (Un)]
[(PredicateProp: ps)
(match ps
[(PropSet: (TypeProp: (Path: '() '(0 0)) ft) _) ft]
[(FalseProp:) (Un)]
[_ Univ])]
[_ Univ])]
[else
@ -98,12 +98,12 @@
(hash-ref predicate-map key))
(match-define (list handler-stx handler-type)
(hash-ref handler-map key))
(define filter-type
(get-filter-type predicate-stx predicate-type))
(define prop-type
(get-prop-type predicate-stx predicate-type))
;; if the predicate doesn't check, then don't bother
;; with the RHS and return no result
(if filter-type
(get-range-result handler-stx handler-type filter-type)
(if prop-type
(get-range-result handler-stx handler-type prop-type)
(ret (Un)))))
(find-syntax form

4
typed-racket-lib/typed-racket/typecheck/error-message.rkt
View File

@ -18,8 +18,8 @@
(-or/c Type/c string?)
-any)]
[type-mismatch
(-->* ((-or/c Type/c Filter? string?)
(-or/c Type/c Filter? string?))
(-->* ((-or/c Type/c Prop? string?)
(-or/c Type/c Prop? string?))
((-or/c string? #f))
-any)])

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

@ -4,7 +4,7 @@
(contract-req)
racket/list
racket/match
(rep type-rep filter-rep)
(rep type-rep prop-rep)
(except-in (types abbrev subtype tc-result)
-> ->* one-of/c))
@ -18,7 +18,7 @@
;; are relevant to this specific error
;; this is done in several ways:
;; - if a case-lambda case is subsumed by another, we don't need to show it
;; (subsumed cases may be useful for their filter information, but this is
;; (subsumed cases may be useful for their prop information, but this is
;; unrelated to error reporting)
;; - if we have an expected type, we don't need to show the domains for which
;; the result type is not a subtype of the expected type
@ -53,7 +53,7 @@
(and expected
(match expected
[(tc-result1: t) t]
[(tc-any-results: (or (Top:) (NoFilter:))) #t] ; anything is a subtype of expected
[(tc-any-results: (or #f (TrueProp:))) #t] ; anything is a subtype of expected
[_ #f]))) ; don't know what it is, don't do any pruning
(define (returns-subtype-of-expected? fun-ty)
(or (not expected) ; no expected type, anything is fine
@ -74,8 +74,8 @@
(define cases
(map (compose make-Function list make-arr)
doms
(map (match-lambda ; strip filters
[(AnyValues: f) (-AnyValues -top)]
(map (match-lambda ; strip props
[(AnyValues: f) (-AnyValues -tt)]
[(Values: (list (Result: t _ _) ...))
(-values t)]
[(ValuesDots: (list (Result: t _ _) ...) _ _)

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

@ -6,7 +6,7 @@
(contract-req)
(typecheck check-below tc-subst tc-metafunctions possible-domains)
(utils tc-utils)
(rep type-rep filter-rep)
(rep type-rep prop-rep)
(except-in (types utils abbrev subtype type-table)
-> ->* one-of/c))
(require-for-cond-contract
@ -78,7 +78,7 @@
[(or (tc-results: ts)
(tc-results: ts _ _ _ _))
(-values (map cleanup-type ts))]
[(tc-any-results: f) (-AnyValues -top)]
[(tc-any-results: f) (-AnyValues -tt)]
[_ t]))
(define (stringify-domain dom rst drst [rng #f])

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

@ -5,7 +5,7 @@
"utils.rkt"
syntax/parse syntax/stx racket/match
(typecheck signatures tc-funapp)
(types abbrev filter-ops union utils)
(types abbrev prop-ops union utils)
(rep type-rep object-rep)
(for-label racket/base racket/bool))
@ -55,14 +55,14 @@
(match* ((single-value v1) (single-value v2))
[((tc-result1: (Value: (? ok? val1)) _ o1)
(tc-result1: (Value: (? ok? val2)) _ o2))
(ret -Boolean (-FS (-and (-filter (-val val2) o1)
(-filter (-val val1) o2))
(-and (-not-filter (-val val2) o1)
(-not-filter (-val val1) o2))))]
(ret -Boolean (-PS (-and (-is-type o1 (-val val2))
(-is-type o2 (-val val1)))
(-and (-not-type o1 (-val val2))
(-not-type o2 (-val val1)))))]
[((tc-result1: t _ o) (tc-result1: (Value: (? ok? val))))
(ret -Boolean (-FS (-filter (-val val) o) (-not-filter (-val val) o)))]
(ret -Boolean (-PS (-is-type o (-val val)) (-not-type o (-val val))))]
[((tc-result1: (Value: (? ok? val))) (tc-result1: t _ o))
(ret -Boolean (-FS (-filter (-val val) o) (-not-filter (-val val) o)))]
(ret -Boolean (-PS (-is-type o (-val val)) (-not-type o (-val val))))]
[((tc-result1: t _ o)
(or (and (? (lambda _ (id=? #'member comparator)))
(tc-result1: (List: (list (and ts (Value: _)) ...))))
@ -72,8 +72,8 @@
(tc-result1: (List: (list (and ts (Value: (? eq?-able))) ...))))))
(let ([ty (apply Un ts)])
(ret (Un (-val #f) t)
(-FS (-filter ty o)
(-not-filter ty o))))]
(-PS (-is-type o ty)
(-not-type o ty))))]
[(_ _) (ret -Boolean)]))

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

@ -117,7 +117,7 @@
(for/list ([e (in-syntax #'(args ...))]
[t (in-list ts)])
(tc-expr/check/t e (ret t))))
-true-filter)]
-true-propset)]
[else
(tc-error/expr
"expected vector with ~a elements, but got ~a"

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

@ -7,7 +7,7 @@
syntax/parse/experimental/reflect
"../signatures.rkt" "../tc-funapp.rkt"
(types utils)
(rep type-rep filter-rep object-rep))
(rep type-rep prop-rep object-rep))
(import tc-expr^ tc-app-keywords^
tc-app-hetero^ tc-app-list^ tc-app-apply^ tc-app-values^
@ -46,11 +46,13 @@
;; TODO: handle drest, and filters/objects
;; TODO: handle drest, and props/objects
(define (arr-matches? arr args)
(match arr
[(arr: domain
(Values: (list (Result: v (FilterSet: (Top:) (Top:)) (Empty:)) ...))
(Values: (list (Result: v
(PropSet: (TrueProp:) (TrueProp:))
(Empty:)) ...))
rest #f (list (Keyword: _ _ #f) ...))
(cond
[(< (length domain) (length args)) rest]
@ -58,9 +60,11 @@
[else #f])]
[_ #f]))
(define (has-filter? arr)
(define (has-props? arr)
(match arr
[(arr: _ (Values: (list (Result: v (FilterSet: (Top:) (Top:)) (Empty:)) ...))
[(arr: _ (Values: (list (Result: v
(PropSet: (TrueProp:) (TrueProp:))
(Empty:)) ...))
_ _ (list (Keyword: _ _ #f) ...)) #f]
[else #t]))
@ -72,13 +76,13 @@
[args* (syntax->list #'args)])
(define (matching-arities arrs)
(for/list ([arr (in-list arrs)] #:when (arr-matches? arr args*)) arr))
(define (has-drest/filter? arrs)
(define (has-drest/props? arrs)
(for/or ([arr (in-list arrs)])
(or (has-filter? arr) (arr-drest arr))))
(or (has-props? arr) (arr-drest arr))))
(define arg-tys
(match f-ty
[(Function: (? has-drest/filter?))
[(Function: (? has-drest/props?))
(map single-value args*)]
[(Function:
(app matching-arities

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

@ -9,7 +9,7 @@
(typecheck signatures tc-funapp)
(types abbrev type-table utils)
(private type-annotation)
(rep type-rep filter-rep)
(rep type-rep prop-rep)
(utils tc-utils)
(for-label racket/base racket/bool '#%paramz))
@ -50,11 +50,11 @@
Univ))
(list (ret Univ) (single-value #'arg))
expected)]))
;; special-case for not - flip the filters
;; special-case for not - flip the props
(pattern ((~or false? not) arg)
(match (single-value #'arg)
[(tc-result1: t (FilterSet: f+ f-) _)
(ret -Boolean (make-FilterSet f- f+))]))
[(tc-result1: t (PropSet: p+ p-) _)
(ret -Boolean (make-PropSet p- p+))]))
;; special case for (current-contract-region)'s default expansion
;; just let it through without any typechecking, since module-name-fixup
;; is a private function from syntax/location, so this must have been

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

@ -16,7 +16,7 @@
[(Values: (list (Result: ts _ _) ...)) (ret ts)]
[(ValuesDots: (list (Result: ts _ _) ...) dty dbound)
(ret ts
(for/list ([t (in-list ts)]) -top-filter)
(for/list ([t (in-list ts)]) -tt-propset)
(for/list ([t (in-list ts)]) -empty-obj)
dty dbound)]
[_ (int-err "do-ret fails: ~a" t)]))

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

@ -5,9 +5,9 @@
(for-syntax racket/base syntax/parse)
(contract-req)
(infer-in infer)
(rep type-rep filter-rep object-rep rep-utils)
(rep type-rep prop-rep object-rep rep-utils)
(utils tc-utils)
(types tc-result resolve subtype remove-intersect union filter-ops)
(types tc-result resolve subtype remove-intersect union prop-ops)
(env type-env-structs lexical-env)
(rename-in (types abbrev)
[-> -->]
@ -18,7 +18,7 @@
(provide with-lexical-env/extend-props)
(define/cond-contract (update t ft pos? lo)
(define/cond-contract (update t new-t pos? lo)
(Type/c Type/c boolean? (listof PathElem?) . -> . Type/c)
;; build-type: build a type while propogating bottom
(define (build-type constructor . args)
@ -26,17 +26,17 @@
(match* ((resolve t) lo)
;; pair ops
[((Pair: t s) (list rst ... (CarPE:)))
(build-type -pair (update t ft pos? rst) s)]
(build-type -pair (update t new-t pos? rst) s)]
[((Pair: t s) (list rst ... (CdrPE:)))
(build-type -pair t (update s ft pos? rst))]
(build-type -pair t (update s new-t pos? rst))]
;; syntax ops
[((Syntax: t) (list rst ... (SyntaxPE:)))
(build-type -Syntax (update t ft pos? rst))]
(build-type -Syntax (update t new-t pos? rst))]
;; promise op
[((Promise: t) (list rst ... (ForcePE:)))
(build-type -Promise (update t ft pos? rst))]
(build-type -Promise (update t new-t pos? rst))]
;; struct ops
[((Struct: nm par flds proc poly pred)
@ -48,7 +48,7 @@
(let*-values ([(lhs rhs) (split-at flds idx)]
[(ty* acc-id) (match rhs
[(cons (fld: ty acc-id #f) _)
(values (update ty ft pos? rst) acc-id)]
(values (update ty new-t pos? rst) acc-id)]
[_ (int-err "update on mutable struct field")])])
(cond
[(Bottom? ty*) ty*]
@ -66,15 +66,15 @@
[((Function: (list (arr: doms (Values: (list (Result: rng _ _))) _ _ _)))
(list rst ... (FieldPE:)))
(make-Function
(list (make-arr* doms (update rng ft pos? rst))))]
(list (make-arr* doms (update rng new-t pos? rst))))]
;; otherwise
[(t '())
(if pos?
(restrict t ft)
(remove t ft))]
(restrict t new-t)
(remove t new-t))]
[((Union: ts) lo)
(apply Un (map (λ (t) (update t ft pos? lo)) ts))]
(apply Un (map (λ (t) (update t new-t pos? lo)) ts))]
[(t* lo)
;; This likely comes up with (-lst t) and we need to improve the system to make sure this case
;; dosen't happen
@ -82,17 +82,17 @@
t]))
;; Returns #f if anything becomes (U)
(define (env+ env fs)
(define (env+ env ps)
(let/ec exit*
(define (exit) (exit* #f empty))
(define-values (props atoms) (combine-props fs (env-props env) exit))
(define-values (props atoms) (combine-props ps (env-props env) exit))
(values
(for/fold ([Γ (replace-props env props)]) ([f (in-list atoms)])
(match f
[(or (TypeFilter: ft (Path: lo x)) (NotTypeFilter: ft (Path: lo x)))
(for/fold ([Γ (replace-props env props)]) ([p (in-list atoms)])
(match p
[(or (TypeProp: (Path: lo x) pt) (NotTypeProp: (Path: lo x) pt))
(update-type/lexical
(lambda (x t)
(define new-t (update t ft (TypeFilter? f) lo))
(define new-t (update t pt (TypeProp? p) lo))
(when (type-equal? new-t -Bottom)
(exit))
new-t)
@ -102,7 +102,7 @@
;; run code in an extended env and with replaced props. Requires the body to return a tc-results.
;; TODO make this only add the new prop instead of the entire environment once tc-id is fixed to
;; include the interesting props in its filter.
;; include the interesting props in its prop.
;; WARNING: this may bail out when code is unreachable
(define-syntax (with-lexical-env/extend-props stx)
(define-splicing-syntax-class unreachable?

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

@ -6,9 +6,9 @@
"signatures.rkt"
"check-below.rkt" "../types/kw-types.rkt"
(types utils abbrev union subtype type-table path-type
filter-ops remove-intersect resolve generalize)
prop-ops remove-intersect resolve generalize)
(private-in syntax-properties)
(rep type-rep filter-rep object-rep)
(rep type-rep prop-rep object-rep)
(only-in (infer infer) restrict)
(utils tc-utils)
(env lexical-env)
@ -55,8 +55,8 @@
(ret ty
(if (overlap ty (-val #f))
(-FS (-not-filter (-val #f) obj) (-filter (-val #f) obj))
-true-filter)
(-PS (-not-type obj (-val #f)) (-is-type obj (-val #f)))
-true-propset)
obj))
;; typecheck an expression, but throw away the effect
@ -140,21 +140,21 @@
[t:typecheck-failure
(explicit-fail #'t.stx #'t.message #'t.var)]
;; data
[(quote #f) (ret (-val #f) -false-filter)]
[(quote #t) (ret (-val #t) -true-filter)]
[(quote #f) (ret (-val #f) -false-propset)]
[(quote #t) (ret (-val #t) -true-propset)]
[(quote val)
(match expected
[(tc-result1: t)
(ret (tc-literal #'val t) -true-filter)]
(ret (tc-literal #'val t) -true-propset)]
[_
(ret (tc-literal #'val) -true-filter)])]
(ret (tc-literal #'val) -true-propset)])]
;; syntax
[(quote-syntax datum . _)
(define expected-type
(match expected
[(tc-result1: t) t]
[_ #f]))
(ret (find-stx-type #'datum expected-type) -true-filter)]
(ret (find-stx-type #'datum expected-type) -true-propset)]
;; mutation!
[(set! id val)
(match-let* ([(tc-result1: id-t) (single-value #'id)]
@ -200,7 +200,7 @@
[(begin0 e . es)
(begin0
(tc-expr/check #'e expected)
(tc-body/check #'es (tc-any-results -top)))]
(tc-body/check #'es (tc-any-results -tt)))]
;; if
[(if tst thn els) (tc/if-twoarm #'tst #'thn #'els expected)]
;; lambda
@ -236,7 +236,7 @@
(define actual-kws (attribute kw.value))
(check-kw-arity actual-kws f)
(tc-expr/check/type #'fun (kw-convert f actual-kws #:split #t))
(ret f -true-filter)]
(ret f -true-propset)]
[(or (tc-results: _) (tc-any-results: _))
(tc-expr/check form #f)])]
;; opt function def
@ -344,14 +344,14 @@
[else
;; Typecheck the first form.
(define e (first es))
(define results (tc-expr/check e (tc-any-results -no-filter)))
(define results (tc-expr/check e (tc-any-results #f)))
(define props
(match results
[(tc-any-results: f) (list f)]
[(tc-results: _ (list (FilterSet: f+ f-) ...) _)
(map -or f+ f-)]
[(tc-results: _ (list (FilterSet: f+ f-) ...) _ _ _)
(map -or f+ f-)]))
[(tc-results: _ (list (PropSet: p+ p-) ...) _)
(map -or p+ p-)]
[(tc-results: _ (list (PropSet: p+ p-) ...) _ _ _)
(map -or p+ p-)]))
(with-lexical-env/extend-props
props
;; If `e` bails out, mark the rest as ignored.

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

@ -48,7 +48,7 @@
#:when (subtypes/varargs argtys dom rest))
;; then typecheck here
;; we call the separate function so that we get the appropriate
;; filters/objects
;; props/objects
(tc/funapp1 f-stx args-stx a args-res expected #:check #f))
;; if nothing matched, error
(domain-mismatches
@ -70,7 +70,7 @@
(eq? dotted-var (cdr drest)))]
[else (= (length dom) (length argtys))]))
;; Only try to infer the free vars of the rng (which includes the vars
;; in filters/objects).
;; in props/objects).
(λ (dom rng rest drest a)
(extend-tvars fixed-vars
(cond
@ -95,7 +95,7 @@
(λ (dom _ rest kw? a)
(and (andmap not kw?) ((if rest <= =) (length dom) (length argtys))))
;; Only try to infer the free vars of the rng (which includes the vars
;; in filters/objects).
;; in props/objects).
(λ (dom rng rest kw? a)
(extend-tvars vars
(infer/vararg vars null argtys dom rest rng
@ -145,9 +145,9 @@
[(list) (ret out)]
[(list t)
(if (subtype t in)
(ret -Void -true-filter)
(ret -Void -true-propset)
(tc-error/expr
#:return (ret -Void -true-filter)
#:return (ret -Void -true-propset)
"Wrong argument to parameter - expected ~a and got ~a"
in t))]
[_ (tc-error/expr

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

@ -1,7 +1,7 @@
#lang racket/unit
(require "../utils/utils.rkt"
(rep filter-rep)
(types utils filter-ops)
(rep prop-rep)
(types utils prop-ops)
(utils tc-utils)
(typecheck signatures tc-envops tc-metafunctions)
(types type-table)
@ -13,8 +13,8 @@
(define (tc/if-twoarm tst thn els [expected #f])
(match (single-value tst)
[(tc-result1: _ (FilterSet: fs+ fs-) _)
(define expected* (and expected (erase-filter expected)))
[(tc-result1: _ (PropSet: fs+ fs-) _)
(define expected* (and expected (erase-props expected)))
(define results-t
(with-lexical-env/extend-props (list fs+)
#:unreachable (warn-unreachable thn)

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

@ -531,8 +531,8 @@
(match expected
[(tc-result1: (app resolve t)) (or (Poly? t) (PolyDots? t) (PolyRow? t))]
[_ #f]))
(ret (tc/plambda form (get-poly-tvarss form) formals bodies expected) -true-filter)
(ret (tc/mono-lambda/type formals bodies expected) -true-filter)))
(ret (tc/plambda form (get-poly-tvarss form) formals bodies expected) -true-propset)
(ret (tc/mono-lambda/type formals bodies expected) -true-propset)))
;; formals : the formal arguments to the loop
;; body : a block containing the body of the loop

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

@ -1,14 +1,14 @@
#lang racket/unit
(require "../utils/utils.rkt"
(except-in (types utils abbrev filter-ops remove-intersect type-table)
(except-in (types utils abbrev prop-ops remove-intersect type-table)
-> ->* one-of/c)
(only-in (types abbrev) (-> t:->) [->* t:->*])
(private type-annotation parse-type syntax-properties)
(env lexical-env type-alias-helper mvar-env
global-env scoped-tvar-env
signature-env signature-helper)
(rep filter-rep object-rep type-rep)
(rep prop-rep object-rep type-rep)
syntax/free-vars
(typecheck signatures tc-metafunctions tc-subst internal-forms tc-envops)
(utils tarjan)
@ -49,13 +49,13 @@
tc-results/c)
(with-cond-contract t/p ([expected-types (listof (listof Type/c))]
[objs (listof (listof Object?))]
[props (listof (listof Filter?))])
[props (listof (listof Prop?))])
(define-values (expected-types objs props)
(for/lists (e o p)
([e-r (in-list expected-results)]
[names (in-list namess)])
(match e-r
[(list (tc-result: e-ts (FilterSet: fs+ fs-) os) ...)
[(list (tc-result: e-ts (PropSet: fs+ fs-) os) ...)
(values e-ts
(map (λ (o n t) (if (or (is-var-mutated? n) (F? t)) -empty-obj o)) os names e-ts)
(apply append
@ -75,10 +75,10 @@
[(and (Path? o) (not (F? t))) (list)]
;; n is being bound to an expression w/o an object (or whose
;; type is a type variable) so create props about n
[else (list (-or (-and (-not-filter (-val #f) n) f+)
(-and (-filter (-val #f) n) f-)))]))))]
[else (list (-or (-and (-not-type n (-val #f)) f+)
(-and (-is-type n (-val #f)) f-)))]))))]
;; amk: does this case ever occur?
[(list (tc-result: e-ts (NoFilter:) _) ...)
[(list (tc-result: e-ts #f _) ...)
(values e-ts (make-list (length e-ts) -empty-obj) null)]))))
;; extend the lexical environment for checking the body
;; with types and potential aliases
@ -102,7 +102,7 @@
;; in the context of the letrec body
(check-thunk)
;; typecheck the body
(tc-body/check body (and expected (erase-filter expected)))))))
(tc-body/check body (and expected (erase-props expected)))))))
(define (tc-expr/maybe-expected/t e names)
(syntax-parse names
@ -182,7 +182,7 @@
;; after everything, check the body expressions
[(null? remaining-names)
(check-thunk)
(tc-body/check body (and expected (erase-filter expected)))]
(tc-body/check body (and expected (erase-props expected)))]
[else
(define flat-names (apply append remaining-names))
(do-check tc-expr/check

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

@ -2,9 +2,9 @@
(require "../utils/utils.rkt"
racket/match racket/list
(except-in (types abbrev union utils filter-ops tc-result)
(except-in (types abbrev union utils prop-ops tc-result)
-> ->* one-of/c)
(rep type-rep filter-rep object-rep rep-utils)
(rep type-rep prop-rep object-rep rep-utils)
(typecheck tc-subst check-below)
(contract-req))
@ -36,20 +36,20 @@
(make-ValuesDots (map -result ts fs os) dty dbound)]))
(define/cond-contract (resolve atoms prop)
((listof Filter/c)
Filter/c
((listof Prop?)
Prop?
. -> .
Filter/c)
Prop?)
(for/fold ([prop prop])
([a (in-list atoms)])
(match prop
[(AndFilter: ps)
[(AndProp: ps)
(let loop ([ps ps] [result null])
(if (null? ps)
(apply -and result)
(let ([p (car ps)])
(cond [(contradictory? a p) -bot]
[(implied-atomic? p a) (loop (cdr ps) result)]
(cond [(contradictory? a p) -ff]
[(implies-atomic? a p) (loop (cdr ps) result)]
[else (loop (cdr ps) (cons p result))]))))]
[_ prop])))
@ -57,14 +57,14 @@
(let loop ([ps ps])
(match ps
[(list) null]
[(cons (AndFilter: ps*) ps) (loop (append ps* ps))]
[(cons (AndProp: ps*) ps) (loop (append ps* ps))]
[(cons p ps) (cons p (loop ps))])))
(define/cond-contract (combine-props new-props old-props exit)
((listof Filter/c) (listof Filter/c) (-> none/c)
((listof Prop?) (listof Prop?) (-> none/c)
. -> .
(values (listof (or/c ImpFilter? OrFilter?)) (listof (or/c TypeFilter? NotTypeFilter?))))
(define (atomic-prop? p) (or (TypeFilter? p) (NotTypeFilter? p)))
(values (listof OrProp?) (listof (or/c TypeProp? NotTypeProp?))))
(define (atomic-prop? p) (or (TypeProp? p) (NotTypeProp? p)))
(define-values (new-atoms new-formulas) (partition atomic-prop? (flatten-props new-props)))
(let loop ([derived-formulas null]
[derived-atoms new-atoms]
@ -74,12 +74,7 @@
(let* ([p (car worklist)]
[p (resolve derived-atoms p)])
(match p
[(ImpFilter: a c)
(if (for/or ([p (in-list (append derived-formulas derived-atoms))])
(implied-atomic? a p))
(loop derived-formulas derived-atoms (cons c (cdr worklist)))
(loop (cons p derived-formulas) derived-atoms (cdr worklist)))]
[(OrFilter: ps)
[(OrProp: ps)
(let ([new-or
(let or-loop ([ps ps] [result null])
(cond
@ -88,32 +83,32 @@
(contradictory? (car ps) other-p))
(or-loop (cdr ps) result)]
[(for/or ([other-p (in-list derived-atoms)])
(implied-atomic? (car ps) other-p))
-top]
(implies-atomic? other-p (car ps)))
-tt]
[else (or-loop (cdr ps) (cons (car ps) result))]))])
(if (OrFilter? new-or)
(if (OrProp? new-or)
(loop (cons new-or derived-formulas) derived-atoms (cdr worklist))
(loop derived-formulas derived-atoms (cons new-or (cdr worklist)))))]
[(or (? TypeFilter?) (? NotTypeFilter?)) (loop derived-formulas (cons p derived-atoms) (cdr worklist))]
[(or (? TypeProp?) (? NotTypeProp?)) (loop derived-formulas (cons p derived-atoms) (cdr worklist))]
[(AndFilter: ps) (loop derived-formulas derived-atoms (append ps (cdr worklist)))]
[(Top:) (loop derived-formulas derived-atoms (cdr worklist))]
[(Bot:) (exit)])))))
[(AndProp: ps) (loop derived-formulas derived-atoms (append ps (cdr worklist)))]
[(TrueProp:) (loop derived-formulas derived-atoms (cdr worklist))]
[(FalseProp:) (exit)])))))
(define (unconditional-prop res)
(match res
[(tc-any-results: f) f]
[(tc-results (list (tc-result: _ (FilterSet: f+ f-) _) ...) _)
(apply -and (map -or f+ f-))]))
[(tc-any-results: pset) pset]
[(tc-results (list (tc-result: _ (PropSet: p+ p-) _) ...) _)
(apply -and (map -or p+ p-))]))
(define (merge-tc-results results)
(define/match (merge-tc-result r1 r2)
[((tc-result: t1 (FilterSet: f1+ f1-) o1)
(tc-result: t2 (FilterSet: f2+ f2-) o2))
[((tc-result: t1 (PropSet: p1+ p1-) o1)
(tc-result: t2 (PropSet: p2+ p2-) o2))
(tc-result
(Un t1 t2)
(-FS (-or f1+ f2+) (-or f1- f2-))
(-PS (-or p1+ p2+) (-or p1- p2-))
(if (equal? o1 o2) o1 -empty-obj))])
(define/match (same-dty? r1 r2)

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

@ -6,10 +6,10 @@
(require "../utils/utils.rkt"
racket/match racket/list
(contract-req)
(except-in (types abbrev utils filter-ops path-type)
(except-in (types abbrev utils prop-ops path-type)
-> ->* one-of/c)
(only-in (infer infer) restrict)
(rep type-rep object-rep filter-rep rep-utils))
(rep type-rep object-rep prop-rep rep-utils))
(provide add-scope)
@ -49,12 +49,12 @@
;; This is a combination of all of thes substitions from the paper over the different parts of the
;; results.
;; t is the type of the object that we are substituting in. This allows for restriction/simplification
;; of some filters if they conflict with the argument type.
;; of some props if they conflict with the argument type.
(define/cond-contract (subst-tc-results res k o polarity t)
(-> full-tc-results/c name-ref/c Object? boolean? Type? full-tc-results/c)
(define (st ty) (subst-type ty k o polarity t))
(define (sr ty fs ob) (subst-tc-result ty fs ob k o polarity t))
(define (sf f) (subst-filter f k o polarity t))
(define (sf f) (subst-prop f k o polarity t))
(match res
[(tc-any-results: f) (tc-any-results (sf f))]
[(tc-results: ts fs os)
@ -78,34 +78,34 @@
(subst-type r-t k o polarity t)
(restrict argument-side
(subst-type r-t k o polarity t)))
(subst-filter-set r-fs k o polarity t)
(subst-prop-set r-fs k o polarity t)
(subst-object r-o k o polarity)))
;; Substitution of objects into a filter set
;; Substitution of objects into a prop set
;; This is essentially ψ+|ψ- [o/x] from the paper
(define/cond-contract (subst-filter-set fs k o polarity t)
(-> (or/c FilterSet? NoFilter?) name-ref/c Object? boolean? Type/c FilterSet?)
(define extra-filter (-filter t k))
(define (add-extra-filter f)
(define f* (-and f extra-filter))
(define/cond-contract (subst-prop-set pset k o polarity t)
(-> (or/c #f PropSet?) name-ref/c Object? boolean? Type/c PropSet?)
(define extra-prop (-is-type k t))
(define (add-extra-prop p)
(define p* (-and p extra-prop))
(cond
[(filter-equal? f* extra-filter) -top]
[(Bot? f*) -bot]
[else f]))
(match fs
[(FilterSet: f+ f-)
(-FS (subst-filter (add-extra-filter f+) k o polarity t)
(subst-filter (add-extra-filter f-) k o polarity t))]
[_ -top-filter]))
[(prop-equal? p* extra-prop) -tt]
[(FalseProp? p*) -ff]
[else p]))
(match pset
[(PropSet: p+ p-)
(-PS (subst-prop (add-extra-prop p+) k o polarity t)
(subst-prop (add-extra-prop p-) k o polarity t))]
[_ -tt-propset]))
;; Substitution of objects into a type
;; This is essentially t [o/x] from the paper
(define/cond-contract (subst-type t k o polarity ty)
(-> Type? name-ref/c Object? boolean? Type/c Type?)
(define (st t) (subst-type t k o polarity ty))
(define/cond-contract (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs k o polarity ty))
(define/cond-contract (sf fs) (PropSet? . -> . PropSet?) (subst-prop-set fs k o polarity ty))
(type-case (#:Type st
#:Filter sf
#:Prop sf
#:Object (lambda (f) (subst-object f k o polarity)))
t
[#:arr dom rng rest drest kws
@ -135,80 +135,48 @@
(define/cond-contract (subst-object t k o polarity)
(-> Object? name-ref/c Object? boolean? Object?)
(match t
[(NoObject:) t]
[#f t]
[(Empty:) t]
[(Path: p i)
(if (name-ref=? i k)
(match o
[(Empty:) -empty-obj]
;; the result is not from an annotation, so it isn't a NoObject
[(NoObject:) -empty-obj]
[#f -empty-obj]
[(Path: p* i*) (make-Path (append p p*) i*)])
t)]))
;; Substitution of objects into a filter in a filter set
;; This is ψ+ [o/x] and ψ- [o/x] with the addition that filters are restricted to
;; Substitution of objects into a prop in a prop set
;; This is ψ+ [o/x] and ψ- [o/x] with the addition that props are restricted to
;; only those values which are a subtype of the actual argument type (ty).
(define/cond-contract (subst-filter f k o polarity ty)
(-> Filter/c name-ref/c Object? boolean? Type/c Filter/c)
(define (ap f) (subst-filter f k o polarity ty))
(define (tf-matcher t p i maker)
(define/cond-contract (subst-prop p k o polarity ty)
(-> Prop? name-ref/c Object? boolean? Type/c Prop?)
(define (ap q) (subst-prop q k o polarity ty))
(define (tprop-matcher pes i t maker)
(cond
[(name-ref=? i k)
(match o
[(Empty:)
(if polarity -top -bot)]
(if polarity -tt -ff)]
[_
;; `ty` alone doesn't account for the path, so
;; first traverse it with the path to match `t`
(define ty/path (path-type p ty))
(define ty/path (path-type pes ty))
(maker
;; don't restrict if the path doesn't match the type
(if (equal? ty/path Err)
(subst-type t k o polarity ty)
(restrict ty/path
(subst-type t k o polarity ty)))
(-acc-path p o))])]
[(index-free-in? k t) (if polarity -top -bot)]
[else f]))
(-acc-path pes o)
;; don't restrict if the path doesn't match the type
(if (equal? ty/path Err)
(subst-type t k o polarity ty)
(restrict ty/path
(subst-type t k o polarity ty))))])]
[else p]))
(match f
[(ImpFilter: ant consq)
(-imp (subst-filter ant k o (not polarity) ty) (ap consq))]
[(AndFilter: fs) (apply -and (map ap fs))]
[(OrFilter: fs) (apply -or (map ap fs))]
[(Bot:) -bot]
[(Top:) -top]
[(TypeFilter: t (Path: p i))
(tf-matcher t p i -filter)]
[(NotTypeFilter: t (Path: p i))
(tf-matcher t p i -not-filter)]))
;; Determine if the object k occurs free in the given type
(define (index-free-in? k type)
(let/ec
return
(define (for-object o)
(object-case (#:Type for-type)
o
[#:Path p i
(if (name-ref=? i k)
(return #t)
o)]))
(define (for-type t)
(type-case (#:Type for-type
#:Object for-object)
t
[#:arr dom rng rest drest kws
(let* ([st* (if (pair? k)
(lambda (t) (index-free-in? (add-scope k) t))
for-type)])
(for-each for-type dom)
(st* rng)
(and rest (for-type rest))
(and drest (for-type (car drest)))
(for-each for-type kws)
;; dummy return value
(make-arr* null Univ))]))
(for-type type)
#f))
(match p
[(AndProp: ps) (apply -and (map ap ps))]
[(OrProp: ps) (apply -or (map ap ps))]
[(FalseProp:) -ff]
[(TrueProp:) -tt]
[(TypeProp: (Path: pes i) t)
(tprop-matcher pes i t -is-type)]
[(NotTypeProp: (Path: pes i) t)
(tprop-matcher pes i t -not-type)]))

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

@ -213,7 +213,7 @@
;; typecheck the expressions of a module-top-level form
;; no side-effects
;; syntax? -> (or/c 'no-type tc-results/c)
(define (tc-toplevel/pass2 form [expected (tc-any-results -top)])
(define (tc-toplevel/pass2 form [expected (tc-any-results -tt)])
(do-time (format "pass2 ~a line ~a"
(if #t

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

@ -12,7 +12,7 @@
racket/function
(prefix-in c: (contract-req))
(rename-in (rep type-rep filter-rep object-rep)
(rename-in (rep type-rep prop-rep object-rep)
[make-Base make-Base*])
(types union numeric-tower prefab)
;; Using this form so all-from-out works
@ -262,23 +262,23 @@
;; Function type constructors
(define/decl top-func (make-Function (list)))
(define (asym-pred dom rng filter)
(make-Function (list (make-arr* (list dom) rng #:filters filter))))
(define (asym-pred dom rng prop)
(make-Function (list (make-arr* (list dom) rng #:props prop))))
(define/cond-contract make-pred-ty
(c:case-> (c:-> Type/c Type/c)
(c:-> (c:listof Type/c) Type/c Type/c Type/c)
(c:-> (c:listof Type/c) Type/c Type/c Object? Type/c))
(case-lambda
[(in out t p)
(->* in out : (-FS (-filter t p) (-not-filter t p)))]
[(in out t o)
(->* in out : (-PS (-is-type o t) (-not-type o t)))]
[(in out t)
(make-pred-ty in out t (make-Path null (list 0 0)))]
[(t)
(make-pred-ty (list Univ) -Boolean t (make-Path null (list 0 0)))]))
(define/decl -true-filter (-FS -top -bot))
(define/decl -false-filter (-FS -bot -top))
(define/decl -true-propset (-PS -tt -ff))
(define/decl -false-propset (-PS -ff -tt))
(define (opt-fn args opt-args result #:rest [rest #f] #:kws [kws null])
(apply cl->* (for/list ([i (in-range (add1 (length opt-args)))])

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

@ -6,7 +6,7 @@
;; extends it with more types and type abbreviations.
(require "../utils/utils.rkt"
(rep type-rep filter-rep object-rep rep-utils)
(rep type-rep prop-rep object-rep rep-utils)
(env mvar-env)
racket/match racket/list (prefix-in c: (contract-req))
(for-syntax racket/base syntax/parse racket/list)
@ -102,21 +102,19 @@
(make-Mu 'var ty))]))
;; Results
(define/cond-contract (-result t [f -top-filter] [o -empty-obj])
(c:->* (Type/c) (FilterSet? Object?) Result?)
(define/cond-contract (-result t [pset -tt-propset] [o -empty-obj])
(c:->* (Type/c) (PropSet? Object?) Result?)
(cond
[(or (equal? t -Bottom) (equal? f -bot-filter))
(make-Result -Bottom -bot-filter o)]
[(or (equal? t -Bottom) (equal? pset -ff-propset))
(make-Result -Bottom -ff-propset o)]
[else
(make-Result t f o)]))
(make-Result t pset o)]))
;; Filters
(define/decl -top (make-Top))
(define/decl -bot (make-Bot))
(define/decl -no-filter (make-NoFilter))
(define/decl -top-filter (make-FilterSet -top -top))
(define/decl -bot-filter (make-FilterSet -bot -bot))
(define/decl -no-obj (make-NoObject))
;; 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 (-id-path id)
(cond
@ -133,15 +131,15 @@
[(Empty:) -empty-obj]
[(Path: p o) (make-Path (append path-elems p) o)]))
(define/cond-contract (-FS + -)
(c:-> Filter/c Filter/c FilterSet?)
(make-FilterSet + -))
(define/cond-contract (-PS + -)
(c:-> Prop? Prop? PropSet?)
(make-PropSet + -))
;; Abbreviation for filters
;; Abbreviation for props
;; `i` can be an integer or name-ref/c for backwards compatibility
;; FIXME: Make all callers pass in an object and remove backwards compatibility
(define/cond-contract (-filter t i)
(c:-> Type/c (c:or/c integer? name-ref/c Object?) Filter/c)
(define/cond-contract (-is-type i t)
(c:-> (c:or/c integer? name-ref/c Object?) Type/c Prop?)
(define o
(cond
[(Object? i) i]
@ -149,17 +147,17 @@
[(list? i) (make-Path null i)]
[else (-id-path i)]))
(cond
[(Empty? o) -top]
[(equal? Univ t) -top]
[(equal? -Bottom t) -bot]
[else (make-TypeFilter t o)]))
[(Empty? o) -tt]
[(equal? Univ t) -tt]
[(equal? -Bottom t) -ff]
[else (make-TypeProp o t)]))
;; Abbreviation for not filters
;; Abbreviation for not props
;; `i` can be an integer or name-ref/c for backwards compatibility
;; FIXME: Make all callers pass in an object and remove backwards compatibility
(define/cond-contract (-not-filter t i)
(c:-> Type/c (c:or/c integer? name-ref/c Object?) Filter/c)
(define/cond-contract (-not-type i t)
(c:-> (c:or/c integer? name-ref/c Object?) Type/c Prop?)
(define o
(cond
[(Object? i) i]
@ -167,30 +165,30 @@
[(list? i) (make-Path null i)]
[else (-id-path i)]))
(cond
[(Empty? o) -top]
[(equal? -Bottom t) -top]
[(equal? Univ t) -bot]
[else (make-NotTypeFilter t o)]))
[(Empty? o) -tt]
[(equal? -Bottom t) -tt]
[(equal? Univ t) -ff]
[else (make-NotTypeProp o t)]))
;; A Type that corresponds to the any contract for the
;; return type of functions
(define (-AnyValues f) (make-AnyValues f))
(define/decl ManyUniv (make-AnyValues -top))
(define/decl ManyUniv (make-AnyValues -tt))
;; Function types
(define/cond-contract (make-arr* dom rng
#:rest [rest #f] #:drest [drest #f] #:kws [kws null]
#:filters [filters -top-filter] #:object [obj -empty-obj])
#:props [props -tt-propset] #:object [obj -empty-obj])
(c:->* ((c:listof Type/c) (c:or/c SomeValues/c Type/c))
(#:rest (c:or/c #f Type/c)
#:drest (c:or/c #f (c:cons/c Type/c symbol?))
#:kws (c:listof Keyword?)
#:filters FilterSet?
#:props PropSet?
#:object Object?)
arr?)
(make-arr dom (if (Type/c? rng)
(make-Values (list (-result rng filters obj)))
(make-Values (list (-result rng props obj)))
rng)
rest drest (sort #:key Keyword-kw kws keyword<?)))
@ -202,23 +200,23 @@
#'(make-Function (list (make-arr* dom rng)))]
[(_ dom rst rng)
#'(make-Function (list (make-arr* dom rng #:rest rst)))]
[(_ dom rng :c filters)
#'(make-Function (list (make-arr* dom rng #:filters filters)))]
[(_ dom rng _:c filters _:c object)
#'(make-Function (list (make-arr* dom rng #:filters filters #:object object)))]
[(_ dom rst rng _:c filters)
#'(make-Function (list (make-arr* dom rng #:rest rst #:filters filters)))]
[(_ dom rst rng _:c filters : object)
#'(make-Function (list (make-arr* dom rng #:rest rst #:filters filters #:object object)))]))
[(_ dom rng :c props)
#'(make-Function (list (make-arr* dom rng #:props props)))]
[(_ dom rng _:c props _:c object)
#'(make-Function (list (make-arr* dom rng #:props props #:object object)))]
[(_ dom rst rng _:c props)
#'(make-Function (list (make-arr* dom rng #:rest rst #:props props)))]
[(_ dom rst rng _:c props : object)
#'(make-Function (list (make-arr* dom rng #:rest rst #:props props #:object object)))]))
(define-syntax (-> stx)
(define-syntax-class c
(pattern x:id #:fail-unless (eq? ': (syntax-e #'x)) #f))
(syntax-parse stx
[(_ dom ... rng _:c filters _:c objects)
#'(->* (list dom ...) rng : filters : objects)]
[(_ dom ... rng :c filters)
#'(->* (list dom ...) rng : filters)]
[(_ dom ... rng _:c props _:c objects)
#'(->* (list dom ...) rng : props : objects)]
[(_ dom ... rng :c props)
#'(->* (list dom ...) rng : props)]
[(_ dom ... rng)
#'(->* (list dom ...) rng)]))
@ -228,10 +226,10 @@
(->* dom rng)]
[(_ dom (dty dbound) rng)
(make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound))))]
[(_ dom rng : filters)
(->* dom rng : filters)]
[(_ dom (dty dbound) rng : filters)
(make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound) #:filters filters)))]))
[(_ dom rng : props)
(->* dom rng : props)]
[(_ dom (dty dbound) rng : props)
(make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound) #:props props)))]))
(define (simple-> doms rng)
(->* doms rng))
@ -240,8 +238,8 @@
(define obj (-acc-path path (-id-path var)))
(make-Function
(list (make-arr* dom rng
#:filters (-FS (-not-filter (-val #f) obj)
(-filter (-val #f) obj))
#:props (-PS (-not-type obj (-val #f))
(-is-type obj (-val #f)))
#:object obj))))
(define (cl->* . args)

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

@ -133,7 +133,7 @@
;; class type with row variable is found.
(define (inf type)
(type-case
(#:Type inf #:Filter (sub-f inf) #:Object (sub-o inf))
(#:Type inf #:Prop (sub-f inf) #:Object (sub-o inf))
type
[#:Class row inits fields methods augments init-rest
(cond

259
typed-racket-lib/typed-racket/types/filter-ops.rkt
View File

@ -1,259 +0,0 @@
#lang racket/base
(require "../utils/utils.rkt"
racket/list racket/match
(prefix-in c: (contract-req))
(rep type-rep filter-rep object-rep rep-utils)
(only-in (infer infer) restrict)
(types union subtype remove-intersect abbrev tc-result))
(provide/cond-contract
[-and (c:->* () #:rest (c:listof Filter/c) Filter/c)]
[-or (c:->* () #:rest (c:listof Filter/c) Filter/c)]
[-imp (c:-> Filter/c Filter/c Filter/c)]
[implied-atomic? (c:-> Filter/c Filter/c boolean?)]
[complementary? (c:-> Filter/c Filter/c boolean?)]
[contradictory? (c:-> Filter/c Filter/c boolean?)]
[add-unconditional-filter-all-args (c:-> Function? Type/c Function?)]
[add-unconditional-prop (c:-> tc-results/c Filter/c tc-results/c)]
[erase-filter (c:-> tc-results/c tc-results/c)]
[name-ref=? (c:-> name-ref/c name-ref/c boolean?)])
(define (atomic-filter? p)
(or (TypeFilter? p) (NotTypeFilter? p)
(Top? p) (Bot? p)))
;; contradictory: Filter/c Filter/c -> boolean?
;; Returns true if the AND of the two filters is equivalent to Bot
(define (contradictory? f1 f2)
(match* (f1 f2)
[((TypeFilter: t1 p) (NotTypeFilter: t2 p))
(subtype t1 t2)]
[((NotTypeFilter: t2 p) (TypeFilter: t1 p))
(subtype t1 t2)]
[((Bot:) _) #t]
[(_ (Bot:)) #t]
[(_ _) #f]))
;; complementary: Filter/c Filter/c -> boolean?
;; Returns true if the OR of the two filters is equivalent to Top
(define (complementary? f1 f2)
(match* (f1 f2)
[((TypeFilter: t1 p) (NotTypeFilter: t2 p))
(subtype t2 t1)]
[((NotTypeFilter: t2 p) (TypeFilter: t1 p))
(subtype t2 t1)]
[((Top:) (Top:)) #t]
[(_ _) #f]))
(define (name-ref=? a b)
(or (equal? a b)
(and (identifier? a)
(identifier? b)
(free-identifier=? a b))))
;; is f1 implied by f2?
(define (implied-atomic? f1 f2)
(match* (f1 f2)
[(f f) #t]
[((Top:) _) #t]
[(_ (Bot:)) #t]
[((OrFilter: ps) (OrFilter: qs))
(for/and ([q (in-list qs)])
(for/or ([p (in-list ps)])
(filter-equal? p q)))]
[((OrFilter: fs) f2)
(for/or ([f (in-list fs)])
(filter-equal? f f2))]
[(f1 (AndFilter: fs))
(for/or ([f (in-list fs)])
(filter-equal? f f1))]
[((TypeFilter: t1 p) (TypeFilter: t2 p))
(subtype t2 t1)]
[((NotTypeFilter: t2 p) (NotTypeFilter: t1 p))
(subtype t2 t1)]
[((NotTypeFilter: t1 p) (TypeFilter: t2 p))
(not (overlap t1 t2))]
[(_ _) #f]))
(define (hash-name-ref i)
(if (identifier? i) (hash-id i) i))
;; compact : (Listof prop) bool -> (Listof prop)
;; props : propositions to compress
;; or? : is this an OrFilter (alternative is AndFilter)
;;
;; This combines all the TypeFilters at the same path into one TypeFilter. If it is an OrFilter the
;; combination is done using Un, otherwise, restrict. The reverse is done for NotTypeFilters. If it is
;; an OrFilter this simplifies to -top if any of the atomic filters simplified to -top, and removes
;; any -bot values. The reverse is done if this is an AndFilter.
;;
(define/cond-contract (compact props or?)
((c:listof Filter/c) boolean? . c:-> . (c:listof Filter/c))
(define tf-map (make-hash))
(define ntf-map (make-hash))
(define (restrict-update dict t1 p)
(hash-update! dict p (λ (t2) (restrict t1 t2)) Univ))
(define (union-update dict t1 p)
(hash-update! dict p (λ (t2) (Un t1 t2)) -Bottom))
(define-values (atomics others) (partition atomic-filter? props))
(for ([prop (in-list atomics)])
(match prop
[(TypeFilter: t1 p)
((if or? union-update restrict-update) tf-map t1 p) ]
[(NotTypeFilter: t1 p)
((if or? restrict-update union-update) ntf-map t1 p) ]))
(define raw-results
(append others
(for/list ([(k v) (in-hash tf-map)]) (-filter v k))
(for/list ([(k v) (in-hash ntf-map)]) (-not-filter v k))))
(if or?
(if (member -top raw-results)
(list -top)
(filter-not Bot? raw-results))
(if (member -bot raw-results)
(list -bot)
(filter-not Top? raw-results))))
;; invert-filter: Filter/c -> Filter/c
;; Logically inverts a filter.
(define (invert-filter p)
(match p
[(Bot:) -top]
[(Top:) -bot]
[(TypeFilter: t p) (-not-filter t p)]
[(NotTypeFilter: t p) (-filter t p)]
[(AndFilter: fs) (apply -or (map invert-filter fs))]
[(OrFilter: fs) (apply -and (map invert-filter fs))]
[(ImpFilter: f1 f2) (-and f1 (invert-filter f2))]))
;; -imp: Filter/c Filter/c -> Filter/c
;; Smart constructor for make-ImpFilter
(define (-imp p1 p2)
(match* (p1 p2)
[(t t) -top]
[((Bot:) _) -top]
[(_ (Top:)) -top]
[((Top:) _) p2]
[(_ (Bot:)) (invert-filter p1)]
[(_ _) (make-ImpFilter p1 p2)]))
(define (-or . args)
(define mk
(case-lambda [() -bot]
[(f) f]
[fs (make-OrFilter (sort fs filter<?))]))
(define (distribute args)
(define-values (ands others) (partition AndFilter? args))
(if (null? ands)
(apply mk others)
(match-let ([(AndFilter: elems) (car ands)])
(apply -and (for/list ([a (in-list elems)])
(apply -or a (append (cdr ands) others)))))))
(let loop ([fs args] [result null])
(if (null? fs)
(distribute (compact result #t))
(match (car fs)
[(and t (Top:)) t]
[(OrFilter: fs*) (loop (append fs* (cdr fs)) result)]
[(Bot:) (loop (cdr fs) result)]
[t
(cond [(for/or ([f (in-list (append (cdr fs) result))])
(complementary? f t))
-top]
[(let ([t-seq (Rep-seq t)])
(for/or ([f (in-list result)])
(or (= (Rep-seq f) t-seq) (implied-atomic? f t))))
(loop (cdr fs) result)]
[else
(loop (cdr fs) (cons t result))])]))))
(define (-and . args)
(define mk
(case-lambda [() -top]
[(f) f]
[fs (make-AndFilter (sort fs filter<?))]))
(define (flatten-ands fs)
(let loop ([fs fs] [results null])
(match fs
[(list) results]
[(cons (AndFilter: fs*) fs) (loop fs (append fs* results))]
[(cons f fs) (loop fs (cons f results))])))
;; Move all the type filters up front as they are the stronger props
(define-values (filters other-args)
(partition (λ (f) (or (TypeFilter? f) (NotTypeFilter? f)))
(flatten-ands (remove-duplicates args eq? #:key Rep-seq))))
(define-values (type-filters not-type-filters)
(partition TypeFilter? filters))
(let loop ([fs (append type-filters not-type-filters other-args)] [result null])
(if (null? fs)
(apply mk (compact result #f))
(match (car fs)
[(and t (Bot:)) t]
[(Top:) (loop (cdr fs) result)]
[t (cond [(for/or ([f (in-list (append (cdr fs) result))])
(contradictory? f t))
-bot]
[(let ([t-seq (Rep-seq t)])
(for/or ([f (in-list result)])
(or (= (Rep-seq f) t-seq)
(implied-atomic? t f))))
(loop (cdr fs) result)]
[else
(loop (cdr fs) (cons t result))])]))))
;; add-unconditional-prop: tc-results? Filter/c? -> tc-results?
;; Ands the given proposition to the filters in the tc-results.
;; Useful to express properties of the form: if this expressions returns at all, we learn this
(define (add-unconditional-prop results prop)
(match results
[(tc-any-results: f) (tc-any-results (-and prop f))]
[(tc-results: ts (list (FilterSet: fs+ fs-) ...) os)
(ret ts
(for/list ([f+ fs+] [f- fs-])
(-FS (-and prop f+) (-and prop f-)))
os)]
[(tc-results: ts (list (FilterSet: fs+ fs-) ...) os dty dbound)
(ret ts
(for/list ([f+ fs+] [f- fs-])
(-FS (-and prop f+) (-and prop f-)))
os)]))
;; ands the given type filter to both sides of the given arr for each argument
;; useful to express properties of the form: if this function returns at all,
;; we learn this about its arguments (like fx primitives, or car/cdr, etc.)
(define (add-unconditional-filter-all-args arr type)
(match arr
[(Function: (list (arr: dom rng rest drest kws)))
(match rng
[(Values: (list (Result: tp (FilterSet: -true-filter -false-filter) op)))
(let ([new-filters (apply -and (build-list (length dom)
(lambda (i)
(-filter type i))))])
(make-Function
(list (make-arr
dom
(make-Values
(list (-result tp
(-FS (-and -true-filter new-filters)
(-and -false-filter new-filters))
op)))
rest drest kws))))])]))
;; tc-results/c -> tc-results/c
(define (erase-filter tc)
(match tc
[(tc-any-results: _) (tc-any-results -no-filter)]
[(tc-results: ts _ _)
(ret ts
(for/list ([f (in-list ts)]) -no-filter)
(for/list ([f (in-list ts)]) -no-obj))]
[(tc-results: ts _ _ dty dbound)
(ret ts
(for/list ([f (in-list ts)]) -no-filter)
(for/list ([f (in-list ts)]) -no-obj)
dty dbound)]))

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

@ -70,11 +70,11 @@
(list (make-arr* ts rng #:rest rest #:drest drest)))))
;; This is used to fix the filters of keyword types.
;; TODO: This should also explore deeper into the actual types and remove filters in there as well.
;; TODO: This should not remove the filters but instead make them refer to the actual arguments after
;; This is used to fix the props of keyword types.
;; TODO: This should also explore deeper into the actual types and remove props in there as well.
;; TODO: This should not remove the props but instead make them refer to the actual arguments after
;; keyword conversion.
(define (erase-filter/Values values)
(define (erase-props/Values values)
(match values
[(AnyValues: _) ManyUniv]
[(Results: ts fs os)
@ -219,7 +219,7 @@
(and rest? (last other-args)))
(make-Function
(list (make-arr* (take other-args non-kw-argc)
(erase-filter/Values rng)
(erase-props/Values rng)
#:kws actual-kws
#:rest rest-type)))]
[(and (even? (length arrs)) ; had optional args
@ -241,7 +241,7 @@
(make-Function
(for/list ([to-take (in-range (add1 (length opt-types)))])
(make-arr* (append mand-args (take opt-types to-take))
(erase-filter/Values rng)
(erase-props/Values rng)
#:kws actual-kws
#:rest rest-type)))]
[else (int-err "unsupported arrs in keyword function type")])]

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

@ -11,7 +11,7 @@
(for-syntax racket/base syntax/parse))
(provide Listof: List: MListof: AnyPoly: AnyPoly-names: Function/arrs:
PredicateFilter:)
PredicateProp:)
(define-match-expander Listof:
@ -95,10 +95,10 @@
[(_ doms rngs rests drests kws (~optional (~seq #:arrs arrs) #:defaults ([arrs #'_])))
#'(Function: (and arrs (list (arr: doms rngs rests drests kws) (... ...))))])))
;; A match expander for matching the filter on a predicate. This assumes a standard
;; A match expander for matching the prop on a predicate. This assumes a standard
;; predicate type of the shape (-> Any Any : SomeType)
(define-match-expander PredicateFilter:
(define-match-expander PredicateProp:
(λ (stx)
(syntax-parse stx
[(_ fs)
#'(Function: (list (arr: (list _) (Values: (list (Result: _ fs _))) _ _ _)))])))
[(_ ps)
#'(Function: (list (arr: (list _) (Values: (list (Result: _ ps _))) _ _ _)))])))

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

@ -1,13 +1,13 @@
#lang racket/base
;; This module provides functions for printing types and related
;; data structures such as filters and objects
;; data structures such as propositions and objects
(require racket/require racket/match racket/dict racket/string racket/promise
racket/pretty
racket/list
racket/set
(path-up "rep/type-rep.rkt" "rep/filter-rep.rkt" "rep/object-rep.rkt"
(path-up "rep/type-rep.rkt" "rep/prop-rep.rkt" "rep/object-rep.rkt"
"rep/rep-utils.rkt" "types/subtype.rkt"
"types/match-expanders.rkt"
"types/kw-types.rkt"
@ -24,15 +24,15 @@
(define-syntax (provide-printer stx)
(if (eq? printer-type 'debug)
#'(provide (rename-out [debug-printer print-type]
[debug-printer print-filter]
[debug-printer print-prop]
[debug-printer print-object]
[debug-printer print-pathelem]
[debug-pretty-format-type pretty-format-type]))
#'(provide print-type print-filter print-object print-pathelem
#'(provide print-type print-prop print-object print-pathelem
pretty-format-type)))
(provide-printer)
(provide print-complex-filters? type-output-sexpr-tweaker
(provide print-complex-props? type-output-sexpr-tweaker
current-print-type-fuel current-print-unexpanded)
@ -43,7 +43,7 @@
(define print-aliases #t)
(define type-output-sexpr-tweaker (make-parameter values))
(define print-complex-filters? (make-parameter #f))
(define print-complex-props? (make-parameter #f))
;; this parameter controls how far down the type to expand type names
;; interp. 0 -> don't expand
@ -69,15 +69,15 @@
;; print-type also takes an optional (Listof Symbol)
;;
;; These four functions call the helpers below to print an
;; s-expression representation of the given type/pathelem/filter/object.
;; s-expression representation of the given type/pathelem/prop/object.
(define (print-type type port write? [ignored-names '()])
(display (type->sexp type ignored-names) port))
(define (print-pathelem pe port write?)
(display (pathelem->sexp pe) port))
(define (print-filter filter port write?)
(display (filter->sexp filter) port))
(define (print-prop prop port write?)
(display (prop->sexp prop) port))
(define (print-object obj port write?)
(display (object->sexp obj) port))
@ -98,9 +98,9 @@
out))
(string-trim #:left? #f (substring (get-output-string out) indent)))
;; filter->sexp : Filter -> S-expression
;; Print a Filter (see filter-rep.rkt) to the given port
(define (filter->sexp filt)
;; prop->sexp : Prop -> S-expression
;; Print a Prop (see prop-rep.rkt) to the given port
(define (prop->sexp filt)
(define (name-ref->sexp name-ref)
(if (syntax? name-ref)
(syntax-e name-ref)
@ -110,19 +110,16 @@
'()
(list (map pathelem->sexp path))))
(match filt
[(FilterSet: thn els) `(,(filter->sexp thn) \| ,(filter->sexp els))]
[(NoFilter:) '-]
[(NotTypeFilter: type (Path: path nm))
[(PropSet: thn els) `(,(prop->sexp thn) \| ,(prop->sexp els))]
[(NotTypeProp: (Path: path nm) type)
`(! ,(type->sexp type) @ ,@(path->sexps path) ,(name-ref->sexp nm))]
[(TypeFilter: type (Path: path nm))
[(TypeProp: (Path: path nm) type)
`(,(type->sexp type) @ ,@(path->sexps path) ,(name-ref->sexp nm))]
[(Bot:) 'Bot]
[(Top:) 'Top]
[(ImpFilter: a c)
`(ImpFilter ,(filter->sexp a) ,(filter->sexp c))]
[(AndFilter: a) `(AndFilter ,@(map filter->sexp a))]
[(OrFilter: a) `(OrFilter ,@(map filter->sexp a))]
[else `(Unknown Filter: ,(struct->vector filt))]))
[(TrueProp:) 'Top]
[(FalseProp:) 'Bot]
[(AndProp: a) `(AndProp ,@(map prop->sexp a))]
[(OrProp: a) `(OrProp ,@(map prop->sexp a))]
[else `(Unknown Prop: ,(struct->vector filt))]))
;; pathelem->sexp : PathElem -> S-expression
;; Print a PathElem (see object-rep.rkt) to the given port
@ -139,7 +136,6 @@
;; Print an Object (see object-rep.rkt) to the given port
(define (object->sexp object)
(match object
[(NoObject:) '-]
[(Empty:) '-]
[(Path: pes i) (append (map pathelem->sexp pes) (list i))]
[else `(Unknown Object: ,(struct->vector object))]))
@ -222,37 +218,37 @@
(if rest `(,(type->sexp rest) *) null)
(if drest `(,(type->sexp (car drest)) ... ,(cdr drest)) null)
(match rng
[(AnyValues: (Top:)) '(AnyValues)]
[(AnyValues: f) `(AnyValues : ,(filter->sexp f))]
[(Values: (list (Result: t (FilterSet: (Top:) (Top:)) (Empty:))))
[(AnyValues: (TrueProp:)) '(AnyValues)]
[(AnyValues: f) `(AnyValues : ,(prop->sexp f))]
[(Values: (list (Result: t (PropSet: (TrueProp:) (TrueProp:)) (Empty:))))
(list (type->sexp t))]
[(Values: (list (Result: t
(FilterSet: (TypeFilter: ft (Path: pth (list 0 0)))
(NotTypeFilter: ft (Path: pth (list 0 0))))
(PropSet: (TypeProp: (Path: pth (list 0 0)) ft)
(NotTypeProp: (Path: pth (list 0 0)) ft))
(Empty:))))
;; Only print a simple filter for single argument functions,
;; since parse-type only accepts simple latent filters on single
;; Only print a simple prop for single argument functions,
;; since parse-type only accepts simple latent props on single
;; argument functions.
#:when (= 1 (length dom))
(if (null? pth)
`(,(type->sexp t) : ,(type->sexp ft))
`(,(type->sexp t) : ,(type->sexp ft) @
,@(map pathelem->sexp pth)))]
;; Print asymmetric filters with only a positive filter as a
;; Print asymmetric props with only a positive prop as a
;; special case (even when complex printing is off) because it's
;; useful to users who use functions like `filter`.
;; useful to users who use functions like `prop`.
[(Values: (list (Result: t
(FilterSet: (TypeFilter: ft (Path: '() (list 0 0))) (Top:))
(PropSet: (TypeProp: (Path: '() (list 0 0)) ft) (TrueProp:))
(Empty:))))
#:when (= 1 (length dom))
`(,(type->sexp t) : #:+ ,(type->sexp ft))]
[(Values: (list (Result: t fs (Empty:))))
(if (print-complex-filters?)
`(,(type->sexp t) : ,(filter->sexp fs))
(if (print-complex-props?)
`(,(type->sexp t) : ,(prop->sexp fs))
(list (type->sexp t)))]
[(Values: (list (Result: t lf lo)))
(if (print-complex-filters?)
`(,(type->sexp t) : ,(filter->sexp lf) ,(object->sexp lo))
(if (print-complex-props?)
`(,(type->sexp t) : ,(prop->sexp lf) ,(object->sexp lo))
(list (type->sexp t)))]
[_ (list (type->sexp rng))]))]
[else `(Unknown Function Type: ,(struct->vector arr))]))
@ -468,8 +464,8 @@
[(ListDots: dty dbound) `(List ,(t->s dty) ... ,dbound)]
[(F: nm) nm]
;; FIXME (Values are not types and shouldn't need to be considered here
[(AnyValues: (Top:)) 'AnyValues]
[(AnyValues: f) `(AnyValues : ,(filter->sexp f))]
[(AnyValues: (TrueProp:)) 'AnyValues]
[(AnyValues: f) `(AnyValues : ,(prop->sexp f))]
[(Values: (list v)) v]
[(Values: (list v ...)) (cons 'values (map t->s v))]
[(ValuesDots: v dty dbound)
@ -518,9 +514,11 @@
,(t->s body))]
[(Signature: name extends mapping)
(syntax->datum name)]
[(Result: t (or (NoFilter:) (FilterSet: (Top:) (Top:))) (or (NoObject:) (Empty:))) (type->sexp t)]
[(Result: t fs (Empty:)) `(,(type->sexp t) : ,(filter->sexp fs))]
[(Result: t fs lo) `(,(type->sexp t) : ,(filter->sexp fs) : ,(object->sexp lo))]
[(Result: t
(or #f (PropSet: (TrueProp:) (TrueProp:)))
(or #f (Empty:))) (type->sexp t)]
[(Result: t fs (Empty:)) `(,(type->sexp t) : ,(prop->sexp fs))]
[(Result: t fs lo) `(,(type->sexp t) : ,(prop->sexp fs) : ,(object->sexp lo))]
[(MPair: s t) `(MPairof ,(t->s s) ,(t->s t))]
[(Refinement: parent p?)
`(Refinement ,(t->s parent) ,(syntax-e p?))]

257
typed-racket-lib/typed-racket/types/prop-ops.rkt Normal file
View File

@ -0,0 +1,257 @@
#lang racket/base
(require "../utils/utils.rkt"
racket/list racket/match
(prefix-in c: (contract-req))
(rep type-rep prop-rep object-rep rep-utils)
(only-in (infer infer) restrict)
(types union subtype remove-intersect abbrev tc-result))
(provide/cond-contract
[-and (c:->* () #:rest (c:listof Prop?) Prop?)]
[-or (c:->* () #:rest (c:listof Prop?) Prop?)]
[implies-atomic? (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/c 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?)])
(define (atomic-prop? p)
(or (TypeProp? p) (NotTypeProp? p)
(TrueProp? p) (FalseProp? p)))
;; contradictory: Prop? Prop? -> boolean?
;; Returns true if the AND of the two props is equivalent to FalseProp
(define (contradictory? f1 f2)
(match* (f1 f2)
[((TypeProp: o t1) (NotTypeProp: o t2))
(subtype t1 t2)]
[((NotTypeProp: o t2) (TypeProp: o t1))
(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? f1 f2)
(match* (f1 f2)
[((TypeProp: o t1) (NotTypeProp: o t2))
(subtype t2 t1)]
[((NotTypeProp: o t2) (TypeProp: o t1))
(subtype t2 t1)]
[((TrueProp:) (TrueProp:)) #t]
[(_ _) #f]))
(define (name-ref=? a b)
(or (equal? a b)
(and (identifier? a)
(identifier? b)
(free-identifier=? a b))))
;; does p imply q? (but only directly/simply)
(define (implies-atomic? p q)
(match* (p q)
;; reflexivity
[(p p) #t]
;; trivial prop is always satisfied
[(_ (TrueProp:)) #t]
;; ex falso quodlibet
[((FalseProp:) _) #t]
;; ps ⊆ qs ?
[((OrProp: ps) (OrProp: qs))
(and (for/and ([p (in-list ps)])
(member p qs prop-equal?))
#t)]
;; p ∈ qs ?
[(p (OrProp: qs))
(and (member p qs prop-equal?) #t)]
;; q ∈ ps ?
[((AndProp: ps) q)
(and (member q ps prop-equal?) #t)]
;; t1 <: t2 ?
[((TypeProp: o t1) (TypeProp: o t2))
(subtype t1 t2)]
;; t2 <: t1 ?
[((NotTypeProp: o t1) (NotTypeProp: o t2))
(subtype t2 t1)]
;; t1 ∩ t2 = ∅ ?
[((TypeProp: o t1) (NotTypeProp: o t2))
(not (overlap t1 t2))]
;; otherwise we give up
[(_ _) #f]))
(define (hash-name-ref i)
(if (identifier? i) (hash-id i) i))
;; compact : (Listof prop) bool -> (Listof prop)
;; props : propositions to compress
;; or? : is this an Or (alternative is And)
;;
;; This combines all the TypeProps at the same path into one TypeProp. If it is an Or the
;; combination is done using Un, otherwise, restrict. 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.
;;
(define/cond-contract (compact props or?)
((c:listof Prop?) boolean? . c:-> . (c:listof Prop?))
(define tf-map (make-hash))
(define ntf-map (make-hash))
(define (restrict-update dict t1 p)
(hash-update! dict p (λ (t2) (restrict t1 t2)) Univ))
(define (union-update dict t1 p)
(hash-update! dict p (λ (t2) (Un t1 t2)) -Bottom))
(define-values (atomics others) (partition atomic-prop? props))
(for ([prop (in-list atomics)])
(match prop
[(TypeProp: o t1)
((if or? union-update restrict-update) tf-map t1 o) ]
[(NotTypeProp: o t1)
((if or? restrict-update union-update) ntf-map t1 o) ]))
(define raw-results
(append others
(for/list ([(k v) (in-hash tf-map)]) (-is-type k v))
(for/list ([(k v) (in-hash ntf-map)]) (-not-type k v))))
(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))))
;; negate-prop: Prop? -> Prop?
;; Logically inverts a prop.
(define (negate-prop p)
(match p
[(FalseProp:) -tt]
[(TrueProp:) -ff]
[(TypeProp: o t) (-not-type o t)]
[(NotTypeProp: o t) (-is-type o t)]
[(AndProp: ps) (apply -or (map negate-prop ps))]
[(OrProp: ps) (apply -and (map negate-prop ps))]))
(define (-or . args)
(define mk
(case-lambda [() -ff]
[(f) f]
[ps (make-OrProp (sort ps prop<?))]))
(define (distribute args)
(define-values (ands others) (partition AndProp? args))
(if (null? ands)
(apply mk others)
(match-let ([(AndProp: elems) (car ands)])
(apply -and (for/list ([a (in-list elems)])
(apply -or a (append (cdr ands) others)))))))
(let loop ([ps args] [result null])
(if (null? ps)
(distribute (compact result #t))
(match (car ps)
[(and t (TrueProp:)) t]
[(OrProp: ps*) (loop (append ps* (cdr ps)) result)]
[(FalseProp:) (loop (cdr ps) result)]
[t
(cond [(for/or ([f (in-list (append (cdr ps) result))])
(complementary? f t))
-tt]
[(let ([t-seq (Rep-seq t)])
(for/or ([f (in-list result)])
(or (= (Rep-seq f) t-seq) (implies-atomic? t f))))
(loop (cdr ps) result)]
[else
(loop (cdr ps) (cons t result))])]))))
(define (-and . args)
(define mk
(case-lambda [() -tt]
[(f) f]
[ps (make-AndProp (sort ps prop<?))]))
(define (flatten-ands ps)
(let loop ([ps ps] [results null])
(match ps
[(list) results]
[(cons (AndProp: ps*) ps) (loop ps (append ps* results))]
[(cons f ps) (loop ps (cons f results))])))
;; Move all the type props up front as they are the stronger props
(define-values (props other-args)
(partition (λ (p) (or (TypeProp? p) (NotTypeProp? p)))
(flatten-ands (remove-duplicates args eq? #:key Rep-seq))))
(define-values (type-props not-type-props)
(partition TypeProp? props))
(let loop ([ps (append type-props not-type-props other-args)] [result null])
(if (null? ps)
(apply mk (compact result #f))
(match (car ps)
[(and t (FalseProp:)) t]
[(TrueProp:) (loop (cdr ps) result)]
[t (cond [(for/or ([f (in-list (append (cdr ps) result))])
(contradictory? f t))
-ff]
[(let ([t-seq (Rep-seq t)])
(for/or ([f (in-list result)])
(or (= (Rep-seq f) t-seq)
(implies-atomic? f t))))
(loop (cdr ps) result)]
[else
(loop (cdr ps) (cons t result))])]))))
;; add-unconditional-prop: tc-results? Prop? -> tc-results?
;; Ands the given proposition to the props in the tc-results.
;; Useful to express properties of the form: if this expressions returns at all, we learn this
(define (add-unconditional-prop results prop)
(match results
[(tc-any-results: f) (tc-any-results (-and prop f))]
[(tc-results: ts (list (PropSet: ps+ ps-) ...) os)
(ret ts
(for/list ([f+ ps+] [f- ps-])
(-PS (-and prop f+) (-and prop f-)))
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-)))
os)]))
;; ands the given type prop to both sides of the given arr for each argument
;; useful to express properties of the form: if this function returns at all,
;; we learn this about its arguments (like fx primitives, or car/cdr, etc.)
(define (add-unconditional-prop-all-args arr type)
(match arr
[(Function: (list (arr: dom rng rest drest kws)))
(match rng
[(Values: (list (Result: tp (PropSet: -true-prop -false-prop) op)))
(let ([new-props (apply -and (build-list (length dom)
(lambda (i)
(-is-type i type))))])
(make-Function
(list (make-arr
dom
(make-Values
(list (-result tp
(-PS (-and -true-prop new-props)
(-and -false-prop new-props))
op)))
rest drest kws))))])]))
;; tc-results/c -> tc-results/c
(define (erase-props tc)
(match tc
[(tc-any-results: _) (tc-any-results #f)]
[(tc-results: ts _ _)
(define empties (make-list (length ts) #f))
(ret ts
empties
empties)]
[(tc-results: ts _ _ dty dbound)
(define empties (make-list (length ts) #f))
(ret ts
empties
empties
dty dbound)]))

2
typed-racket-lib/typed-racket/types/struct-table.rkt
View File

@ -4,7 +4,7 @@
mzlib/pconvert racket/syntax
"../utils/utils.rkt"
(prefix-in c: (contract-req))
(rep type-rep filter-rep object-rep)
(rep type-rep prop-rep object-rep)
(utils tc-utils)
(env init-envs env-utils))

3
typed-racket-lib/typed-racket/types/structural.rkt
View File

@ -1,3 +1,4 @@
#lang racket/base
;; Module for providing recursive operations over types when the operation doesn't care about the
@ -103,7 +104,7 @@
#'(lambda (t)
(or (type.pred? t) ...))]))
;; Returns true if the type/filter/object supports structural operations.
;; Returns true if the type/prop/object supports structural operations.
(define structural? (gen-structural?))

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

@ -44,7 +44,7 @@
(define names (hash-keys subst))
(define fvs (free-vars* target))
(if (ormap (lambda (name) (free-vars-has-key? fvs name)) names)
(type-case (#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb))
(type-case (#:Type sb #:Prop (sub-f sb) #:Object (sub-o sb))
target
[#:Union tys (apply Un (map sb tys))]
[#:F name (hash-ref subst name target)]
@ -92,7 +92,7 @@
(define (sb t) (substitute-dots images rimage name t))
(if (or (set-member? (free-vars-names (free-idxs* target)) name)
(set-member? (free-vars-names (free-vars* target)) name))
(type-case (#:Type sb #:Filter (sub-f sb)) target
(type-case (#:Type sb #:Prop (sub-f sb)) target
[#:ListDots dty dbound
(if (eq? name dbound)
;; We need to recur first, just to expand out any dotted usages of this.
@ -140,7 +140,7 @@
;; We do a quick check on the free variables to see if we can short circuit the substitution
(if (or (set-member? (free-vars-names (free-idxs* target)) name)
(set-member? (free-vars-names (free-vars* target)) name))
(type-case (#:Type sb #:Filter (sub-f sb))
(type-case (#:Type sb #:Prop (sub-f sb))
target
[#:ValuesDots types dty dbound
(let ([extra-types (if (eq? name dbound) pre-image null)])

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

@ -2,7 +2,7 @@
(require (except-in "../utils/utils.rkt" infer)
racket/match racket/function racket/lazy-require racket/list
(prefix-in c: (contract-req))
(rep type-rep filter-rep object-rep rep-utils)
(rep type-rep prop-rep object-rep rep-utils)
(utils tc-utils early-return)
(types utils resolve base-abbrev match-expanders
numeric-tower substitute current-seen prefab signatures)
@ -137,15 +137,15 @@
(subtype* (restrict-values s-rng t-dom) t-rng))]
[(_ _) #f]))
;; check subtyping of filters, so that predicates subtype correctly
(define (filter-subtype* A0 s t)
;; check subtyping of props, so that predicates subtype correctly
(define (prop-subtype* A0 s t)
(match* (s t)
[(f f) A0]
[((Bot:) t) A0]
[(s (Top:)) A0]
[((TypeFilter: t1 p) (TypeFilter: t2 p))
[((FalseProp:) t) A0]
[(s (TrueProp:)) A0]
[((TypeProp: o t1) (TypeProp: o t2))
(subtype* A0 t1 t2)]
[((NotTypeFilter: t1 p) (NotTypeFilter: t2 p))
[((NotTypeProp: o t1) (NotTypeProp: o t2))
(subtype* A0 t2 t1)]
[(_ _) #f]))
@ -596,26 +596,26 @@
(subtypes* s-rs t-rs)
(subtype* s-dty t-dty))]
[((AnyValues: s-f) (AnyValues: t-f))
(filter-subtype* A0 s-f t-f)]
(prop-subtype* A0 s-f t-f)]
[((or (Values: (list (Result: _ fs _) ...))
(ValuesDots: (list (Result: _ fs _) ...) _ _))
(AnyValues: t-f))
(for/or ([f (in-list fs)])
(match f
[(FilterSet: f+ f-)
[(PropSet: f+ f-)
(subtype-seq A0
(filter-subtype* f+ t-f)
(filter-subtype* f- t-f))]))]
[((Result: t (FilterSet: ft ff) o) (Result: t* (FilterSet: ft* ff*) o))
(prop-subtype* f+ t-f)
(prop-subtype* f- t-f))]))]
[((Result: t (PropSet: ft ff) o) (Result: t* (PropSet: ft* ff*) o))
(subtype-seq A0
(subtype* t t*)
(filter-subtype* ft ft*)
(filter-subtype* ff ff*))]
[((Result: t (FilterSet: ft ff) o) (Result: t* (FilterSet: ft* ff*) (Empty:)))
(prop-subtype* ft ft*)
(prop-subtype* ff ff*))]
[((Result: t (PropSet: ft ff) o) (Result: t* (PropSet: ft* ff*) (Empty:)))
(subtype-seq A0
(subtype* t t*)
(filter-subtype* ft ft*)
(filter-subtype* ff ff*))]
(prop-subtype* ft ft*)
(prop-subtype* ff ff*))]
;; subtyping on other stuff
[((Syntax: t) (Syntax: t*))
(subtype* A0 t t*)]

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

@ -1,20 +1,21 @@
#lang racket/base
(require "../utils/utils.rkt"
(rep type-rep filter-rep)
(rep type-rep prop-rep)
(utils tc-utils)
(types base-abbrev)
racket/match
(prefix-in c: (contract-req)))
;; this structure represents the result of typechecking an expression
;; fields are #f only when the direct result of parsing or annotations
(define-struct/cond-contract tc-result
([t Type/c] [f FilterSet/c] [o Object?])
([t Type/c] [pset (c:or/c PropSet? #f)] [o (c:or/c Object? #f)])
#:transparent)
(define-struct/cond-contract tc-results
([ts (c:listof tc-result?)] [drest (c:or/c (c:cons/c Type/c symbol?) #f)])
#:transparent)
(define-struct/cond-contract tc-any-results ([f (c:or/c Filter/c NoFilter?)]) #:transparent)
(define-struct/cond-contract tc-any-results ([f (c:or/c Prop? #f)]) #:transparent)
(define (tc-results/c v)
(or (tc-results? v)
@ -24,19 +25,17 @@
(and (tc-results? v)
(= (length (tc-results-ts v)) 1)))
;; Contract to check that values are tc-results/c and do not contain -no-filter or -no-obj.
;; Contract to check that values are tc-results/c and do not contain #f propset or obj
;; Used to contract the return values of typechecking functions.
(define (full-tc-results/c r)
(match r
[(tc-any-results: f) (not (equal? -no-filter f))]
[(tc-results: _ fs os)
(and
(not (member -no-filter fs))
(not (member -no-obj os)))]
[(tc-results: _ fs os _ _)
(and
(not (member -no-filter fs))
(not (member -no-obj os)))]
[(tc-any-results: p) (and p #t)]
[(tc-results: _ ps os)
(and (andmap (λ (x) x) ps)
(andmap (λ (x) x) os))]
[(tc-results: _ ps os _ _)
(and (andmap (λ (x) x) ps)
(andmap (λ (x) x) os))]
[else #f]))
@ -45,9 +44,9 @@
[(_ tp fp op) (tc-result tp fp op)]
[(_ tp) (tc-result tp _ _)]))
;; expand-tc-results: (Listof tc-result) -> (Values (Listof Type) (Listof FilterSet) (Listof Object))
;; expand-tc-results: (Listof tc-result) -> (Values (Listof Type) (Listof PropSet) (Listof Object))
(define (expand-tc-results results)
(values (map tc-result-t results) (map tc-result-f results) (map tc-result-o results)))
(values (map tc-result-t results) (map tc-result-pset results) (map tc-result-o results)))
(define-match-expander tc-results:
(syntax-rules ()
@ -78,7 +77,7 @@
[(_ tp) (Results: (list tp))]
[(_ tp fp op) (Results: (list tp) (list fp) (list op))]))
;; expand-Results: (Listof Rresult) -> (Values (Listof Type) (Listof FilterSet) (Listof Object))
;; expand-Results: (Listof Rresult) -> (Values (Listof Type) (Listof PropSet) (Listof Object))
(define (expand-Results results)
(values (map Result-t results) (map Result-f results) (map Result-o results)))
@ -89,14 +88,14 @@
[(_ tp fp op) (Values: (app expand-Results tp fp op))]
[(_ tp fp op dty dbound) (ValuesDots: (app expand-Results tp fp op) dty dbound)]))
;; make-tc-result*: Type/c FilterSet/c Object? -> tc-result?
;; make-tc-result*: Type/c PropSet/c Object? -> tc-result?
;; Smart constructor for a tc-result.
(define (-tc-result type [filter -top-filter] [object -empty-obj])
(define (-tc-result type [prop -tt-propset] [object -empty-obj])
(cond
[(or (equal? type -Bottom) (equal? filter -bot-filter))
(tc-result -Bottom -bot-filter object)]
[(or (equal? type -Bottom) (equal? prop -ff-propset))
(tc-result -Bottom -ff-propset object)]
[else
(tc-result type filter object)]))
(tc-result type prop object)]))
;; convenience function for returning the result of typechecking an expression
@ -104,31 +103,31 @@
(case-lambda [(t)
(make-tc-results
(cond [(Type/c? t)
(list (-tc-result t -top-filter -empty-obj))]
(list (-tc-result t -tt-propset -empty-obj))]
[else
(for/list ([i (in-list t)])
(-tc-result i -top-filter -empty-obj))])
(-tc-result i -tt-propset -empty-obj))])
#f)]
[(t f)
[(t pset)
(make-tc-results
(if (Type/c? t)
(list (-tc-result t f -empty-obj))
(for/list ([i (in-list t)] [f (in-list f)])
(-tc-result i f -empty-obj)))
(list (-tc-result t pset -empty-obj))
(for/list ([i (in-list t)] [pset (in-list pset)])
(-tc-result i pset -empty-obj)))
#f)]
[(t f o)
[(t pset o)
(make-tc-results
(if (and (list? t) (list? f) (list? o))
(map -tc-result t f o)
(list (-tc-result t f o)))
(if (and (list? t) (list? pset) (list? o))
(map -tc-result t pset o)
(list (-tc-result t pset o)))
#f)]
[(t f o dty)
[(t pset o dty)
(int-err "ret used with dty without dbound")]
[(t f o dty dbound)
[(t pset o dty dbound)
(make-tc-results
(if (and (list? t) (list? f) (list? o))
(map -tc-result t f o)
(list (-tc-result t f o)))
(if (and (list? t) (list? pset) (list? o))
(map -tc-result t pset o)
(list (-tc-result t pset o)))
(cons dty dbound))]))
;(trace ret)
@ -137,11 +136,11 @@
[ret
(c:->i ([t (c:or/c Type/c (c:listof Type/c))])
([f (t) (if (list? t)
(c:listof FilterSet/c)
FilterSet/c)]
(c:listof (c:or/c #f PropSet?))
(c:or/c #f PropSet?))]
[o (t) (if (list? t)
(c:listof Object?)
Object?)]
(c:listof (c:or/c #f Object?))
(c:or/c #f Object?))]
[dty Type/c]
[dbound symbol?])
[res tc-results/c])])
@ -154,8 +153,8 @@
[rename -tc-result tc-result
(c:case->
(Type/c . c:-> . tc-result?)
(Type/c FilterSet/c Object? . c:-> . tc-result?))]
[tc-any-results ((c:or/c Filter/c NoFilter?) . c:-> . tc-any-results?)]
(Type/c PropSet? Object? . c:-> . tc-result?))]
[tc-any-results ((c:or/c Prop? #f) . c:-> . tc-any-results?)]
[tc-result-t (tc-result? . c:-> . Type/c)]
[rename tc-results-ts* tc-results-ts (tc-results? . c:-> . (c:listof Type/c))]
[tc-result-equal? (tc-result? tc-result? . c:-> . boolean?)]

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

@ -78,8 +78,9 @@
[((tc-result1: old-t) (tc-result1: t-t))
(ret (Un old-t t-t))]
[((tc-results: old-ts) (tc-results: t-ts))
;; filters don't matter at this point, since only
;; props don't matter at this point, since only
;; the optimizer reads this table
;; -- "I think [the above] comment is no longer true" -samth
(unless (= (length old-ts) (length t-ts))
(int-err
"type table: number of values don't agree ~a ~a"

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

@ -20,7 +20,7 @@
(match t
[(Mu: name b)
(define (sb target)
(type-case (#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb))
(type-case (#:Type sb #:Prop (sub-f sb) #:Object (sub-o sb))
target
[#:F name* (if (eq? name name*) t target)]))
(sb b)]))

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

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

2
typed-racket-test/fail/user-filter-with-bad-index-object.rkt
View File

@ -1,5 +1,5 @@
#;
(exn-pred #rx"Filter proposition's object index 3 is larger than argument length 1")
(exn-pred #rx"Proposition's object index 3 is larger than argument length 1")
#lang typed/racket
;; This test ensures that a filter object like '3' is

16
typed-racket-test/performance/infer-timing.rkt
View File

@ -2,7 +2,7 @@
(require typed-racket/infer/infer
typed-racket/types/union
typed-racket/types/filter-ops
typed-racket/types/prop-ops
typed-racket/types/abbrev
typed-racket/rep/type-rep
typed-racket/types/numeric-tower
@ -62,11 +62,11 @@
;; for fixnum-specific operations. if they return at all, we know
;; their args were fixnums. otherwise, an error would have been thrown
;; for the moment, this is only useful if the result is used as a test
;; once we have a set of filters that are true/false based on reaching
;; once we have a set of props that are true/false based on reaching
;; a certain point, this will be more useful
(define (fx-from-cases . cases)
(apply from-cases (map (lambda (x)
(add-unconditional-filter-all-args
(add-unconditional-prop-all-args
x -Fixnum))
(flatten cases))))
@ -91,13 +91,13 @@
(-> t1 t2 B))
;; simple case useful with equality predicates.
;; if the equality is true, we know that general arg is in fact of specific type.
(define (commutative-equality/filter general specific)
(list (-> general specific B : (-FS (-filter specific 0) -top))
(-> specific general B : (-FS (-filter specific 1) -top))))
(define (commutative-equality/prop general specific)
(list (-> general specific B : (-PS (-is-type 0 specific) -tt))
(-> specific general B : (-PS (-is-type 1 specific) -tt))))
(define (exclude-zero non-neg pos [zero -Zero])
(list (-> zero non-neg B : (-FS (-filter zero 1) (-filter pos 1)))
(-> non-neg zero B : (-FS (-filter zero 0) (-filter pos 0)))))
(list (-> zero non-neg B : (-PS (-is-type 1 zero) (-is-type 1 pos)))
(-> non-neg zero B : (-PS (-is-type 0 zero) (-is-type 0 pos)))))
(define round-type ; also used for truncate

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

@ -38,7 +38,7 @@
"class-util-tests.rkt"
"check-below-tests.rkt"
"init-env-tests.rkt"
"filter-tests.rkt"
"prop-tests.rkt"
"metafunction-tests.rkt"
"generalize-tests.rkt"
"prims-tests.rkt"

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

@ -5,34 +5,34 @@
syntax/srcloc syntax/location
(types abbrev union tc-result)
(utils tc-utils)
(rep filter-rep object-rep type-rep)
(rep prop-rep object-rep type-rep)
(typecheck check-below)
(for-syntax racket/base syntax/parse))
(provide tests)
(gen-test-main)
;; Ensure that we never return a filter of NoFilter or an object of NoObject.
(define (check-filter f)
;; Ensure that we never return a prop or object of #f.
(define (check-prop f)
(match f
[(NoFilter:) (fail-check "Result has no filter (instead of a top filter).")]
[#f (fail-check "Result has no prop (instead of a top prop).")]
[_ (void)]))
(define (check-object o)
(match o
[(NoObject:) (fail-check "Result has no object (instead of an empty object).")]
[#f (fail-check "Result has no object (instead of an empty object).")]
[_ (void)]))
(define (check-result result)
(match result
[(tc-results: ts fs os)
(for-each check-filter fs)
(for-each check-prop fs)
(for-each check-object os) ]
[(tc-results: ts fs os dty bound)
(for-each check-filter fs)
(for-each check-prop fs)
(for-each check-object os)]
[(tc-any-results: f)
(check-filter f)]
(check-prop f)]
[(? Type/c?)
(void)]))
@ -78,143 +78,143 @@
(test-below
(ret -Bottom)
(ret (list Univ Univ) (list -true-filter -no-filter) (list -no-obj -empty-obj))
#:result (ret (list Univ Univ) (list -true-filter -bot-filter) (list -empty-obj -empty-obj)))
(ret (list Univ Univ) (list -true-propset #f) (list #f -empty-obj))
#:result (ret (list Univ Univ) (list -true-propset -ff-propset) (list -empty-obj -empty-obj)))
(test-below
(ret -Bottom)
(ret (list Univ) (list -no-filter) (list -no-obj) Univ 'B)
#:result (ret (list Univ) (list -bot-filter) (list -empty-obj) Univ 'B))
(ret (list Univ) (list #f) (list #f) Univ 'B)
#:result (ret (list Univ) (list -ff-propset) (list -empty-obj) Univ 'B))
;; Bottom is not below everything if the number of values doesn't match up.
(test-below #:fail
(ret (list -Bottom -Bottom))
(ret (list Univ) (list -true-filter) (list -no-obj))
#:result (ret (list Univ) (list -true-filter) (list -empty-obj)))
(ret (list Univ) (list -true-propset) (list #f))
#:result (ret (list Univ) (list -true-propset) (list -empty-obj)))
(test-below #:fail
(ret (list))
(ret (list Univ) (list -true-filter) (list -no-obj))
#:result (ret (list Univ) (list -true-filter) (list -empty-obj)))
(ret (list Univ) (list -true-propset) (list #f))
#:result (ret (list Univ) (list -true-propset) (list -empty-obj)))
(test-below
(ret (list -Symbol) (list -top-filter) (list -empty-obj))
(ret (list Univ) (list -no-filter) (list -no-obj))
#:result (ret (list Univ) (list -top-filter) (list -empty-obj)))
(ret (list -Symbol) (list -tt-propset) (list -empty-obj))
(ret (list Univ) (list #f) (list #f))
#:result (ret (list Univ) (list -tt-propset) (list -empty-obj)))
(test-below
(ret (list -Symbol) (list -true-filter) (list -empty-obj))
(ret (list Univ) (list -top-filter) (list -empty-obj)))
(ret (list -Symbol) (list -true-propset) (list -empty-obj))
(ret (list Univ) (list -tt-propset) (list -empty-obj)))
(test-below #:fail
(ret (list -Symbol) (list -top-filter) (list -empty-obj))
(ret (list Univ) (list -true-filter) (list -no-obj))
#:result (ret (list Univ) (list -true-filter) (list -empty-obj)))
(ret (list -Symbol) (list -tt-propset) (list -empty-obj))
(ret (list Univ) (list -true-propset) (list #f))
#:result (ret (list Univ) (list -true-propset) (list -empty-obj)))
(test-below #:fail #rx"no object"
(ret (list -Symbol) (list -top-filter) (list -empty-obj))
(ret (list Univ) (list -top-filter) (list (make-Path empty #'x))))
(ret (list -Symbol) (list -tt-propset) (list -empty-obj))
(ret (list Univ) (list -tt-propset) (list (make-Path empty #'x))))
(test-below #:fail #rx"no object"
(ret (list -Symbol) (list -top-filter) (list -empty-obj))
(ret (list Univ) (list -true-filter) (list (make-Path empty #'x))))
(ret (list -Symbol) (list -tt-propset) (list -empty-obj))
(ret (list Univ) (list -true-propset) (list (make-Path empty #'x))))
(test-below (ret -Bottom) (tc-any-results -no-filter) #:result (tc-any-results -bot))
(test-below (ret Univ) (tc-any-results -top) #:result (tc-any-results -top))
(test-below (tc-any-results -bot) (tc-any-results -no-filter) #:result (tc-any-results -bot))
(test-below (ret -Bottom) (tc-any-results #f) #:result (tc-any-results -ff))
(test-below (ret Univ) (tc-any-results -tt) #:result (tc-any-results -tt))
(test-below (tc-any-results -ff) (tc-any-results #f) #:result (tc-any-results -ff))
(test-below
(ret (list -Symbol -String) (list -true-filter -bot-filter))
(tc-any-results -no-filter)
#:result (tc-any-results -bot))
(test-below (ret -Symbol -bot-filter) (tc-any-results -no-filter) #:result (tc-any-results -bot))
(ret (list -Symbol -String) (list -true-propset -ff-propset))
(tc-any-results #f)
#:result (tc-any-results -ff))
(test-below (ret -Symbol -ff-propset) (tc-any-results #f) #:result (tc-any-results -ff))
(test-below (ret -Symbol -true-filter -empty-obj) (tc-any-results -no-filter)
#:result (tc-any-results -top))
(test-below (ret (list -Symbol -String)) (tc-any-results -no-filter)
#:result (tc-any-results -top))
(test-below (ret -Symbol -true-propset -empty-obj) (tc-any-results #f)
#:result (tc-any-results -tt))
(test-below (ret (list -Symbol -String)) (tc-any-results #f)
#:result (tc-any-results -tt))
(test-below
(ret (list -Symbol -String) (list -true-filter -false-filter) (list -empty-obj -empty-obj))
(tc-any-results -no-filter)
#:result (tc-any-results -top))
(ret (list -Symbol -String) (list -true-propset -false-propset) (list -empty-obj -empty-obj))
(tc-any-results #f)
#:result (tc-any-results -tt))
(test-below #:fail
(ret -Symbol)
(ret (list -Symbol -Symbol) (list -top-filter -no-filter) (list -no-obj -empty-obj))
#:result (ret (list -Symbol -Symbol) (list -top-filter -top-filter) (list -empty-obj -empty-obj)))
(ret (list -Symbol -Symbol) (list -tt-propset #f) (list #f -empty-obj))
#:result (ret (list -Symbol -Symbol) (list -tt-propset -tt-propset) (list -empty-obj -empty-obj)))
(test-below #:fail
(tc-any-results -top)
(tc-any-results -tt)
(ret -Symbol))
(test-below #:fail
(ret -Symbol -true-filter -empty-obj)
(ret -Symbol -true-filter -empty-obj Univ 'B))
(ret -Symbol -true-propset -empty-obj)
(ret -Symbol -true-propset -empty-obj Univ 'B))
(test-below #:fail
(ret -Symbol -true-filter -empty-obj Univ 'B)
(ret -Symbol -true-filter -empty-obj))
(ret -Symbol -true-propset -empty-obj Univ 'B)
(ret -Symbol -true-propset -empty-obj))
(test-below #:fail
(ret -Symbol)
(ret -Symbol -no-filter -empty-obj Univ 'B)
#:result (ret -Symbol -top-filter -empty-obj Univ 'B))
(ret -Symbol #f -empty-obj Univ 'B)
#:result (ret -Symbol -tt-propset -empty-obj Univ 'B))
(test-below #:fail
(tc-any-results -top)
(ret -Symbol -no-filter -empty-obj Univ 'B)
#:result (ret (list -Symbol) (list -top-filter) (list -empty-obj) Univ 'B))
(tc-any-results -tt)
(ret -Symbol #f -empty-obj Univ 'B)
#:result (ret (list -Symbol) (list -tt-propset) (list -empty-obj) Univ 'B))
(test-below #:fail
(ret -Symbol -top-filter -empty-obj Univ 'B)
(ret (list -Symbol -Symbol) (list -top-filter -top-filter) (list -empty-obj -empty-obj) Univ 'B))
(ret -Symbol -tt-propset -empty-obj Univ 'B)
(ret (list -Symbol -Symbol) (list -tt-propset -tt-propset) (list -empty-obj -empty-obj) Univ 'B))
(test-below (ret -Symbol -true-filter -empty-obj Univ 'B)
(tc-any-results -no-filter)
#:result (tc-any-results -top))
(test-below (ret -Symbol -true-propset -empty-obj Univ 'B)
(tc-any-results #f)
#:result (tc-any-results -tt))
(test-below
(ret -Symbol)
(ret -Symbol -no-filter -empty-obj)
#:result (ret -Symbol -top-filter -empty-obj))
(ret -Symbol #f -empty-obj)
#:result (ret -Symbol -tt-propset -empty-obj))
(test-below
(ret -Symbol -true-filter)
(ret -Symbol -no-filter -empty-obj)
#:result (ret -Symbol -true-filter -empty-obj))
(ret -Symbol -true-propset)
(ret -Symbol #f -empty-obj)
#:result (ret -Symbol -true-propset -empty-obj))
(test-below #:fail
(ret -Symbol -true-filter)
(ret (list Univ -Symbol) (list -no-filter -top-filter))
#:result (ret (list Univ -Symbol) (list -top-filter -top-filter)))
(ret -Symbol -true-propset)
(ret (list Univ -Symbol) (list #f -tt-propset))
#:result (ret (list Univ -Symbol) (list -tt-propset -tt-propset)))
(test-below
(ret (list Univ) (list -true-filter) (list -empty-obj))
(ret Univ -no-filter)
#:result (ret (list Univ) (list -true-filter) (list -empty-obj)))
(ret (list Univ) (list -true-propset) (list -empty-obj))
(ret Univ #f)
#:result (ret (list Univ) (list -true-propset) (list -empty-obj)))
;; Enable these once check-below is fixed
;; Currently does not fail
#;
(test-below #:fail
(ret (list Univ) (list -top-filter) (list -empty-obj) Univ 'B)
(ret (list Univ) (list -false-filter) (list -no-obj) Univ 'B)
#:result (ret (list Univ) (list -false-filter) (list -empty-obj) Univ 'B))
(ret (list Univ) (list -tt-propset) (list -empty-obj) Univ 'B)
(ret (list Univ) (list -false-propset) (list #f) Univ 'B)
#:result (ret (list Univ) (list -false-propset) (list -empty-obj) Univ 'B))
;; Currently does not fail
#;
(test-below #:fail
(ret (list Univ) (list -top-filter) (list -empty-obj))
(ret (list Univ) (list -false-filter) (list -no-obj) Univ 'B)
#:result (ret (list Univ) (list -false-filter) (list -empty-obj) Univ 'B))
(ret (list Univ) (list -tt-propset) (list -empty-obj))
(ret (list Univ) (list -false-propset) (list #f) Univ 'B)
#:result (ret (list Univ) (list -false-propset) (list -empty-obj) Univ 'B))
;; Currently does not fail
#;
(test-below #:fail
(ret (list Univ Univ) (list -top-filter -top-filter) (list -empty-obj -empty-obj))
(ret (list Univ Univ) (list -false-filter -false-filter) (list -no-obj -no-obj))
#:result (ret (list Univ Univ) (list -false-filter -false-filter) (list -empty-obj -empty-obj)))
(ret (list Univ Univ) (list -tt-propset -tt-propset) (list -empty-obj -empty-obj))
(ret (list Univ Univ) (list -false-propset -false-propset) (list #f #f))
#:result (ret (list Univ Univ) (list -false-propset -false-propset) (list -empty-obj -empty-obj)))
))

24
typed-racket-test/unit-tests/class-tests.rkt
View File

@ -23,8 +23,8 @@
base-types base-types-extra)
define lambda λ case-lambda)
(prefix-in tr: (only-in (base-env prims) define lambda λ case-lambda))
(for-syntax (rep type-rep filter-rep object-rep)
(rename-in (types abbrev union numeric-tower filter-ops utils)
(for-syntax (rep type-rep prop-rep object-rep)
(rename-in (types abbrev union numeric-tower prop-ops utils)
[Un t:Un]
[-> t:->])))
@ -107,8 +107,8 @@
-Void]
;; Send to non object
[tc-err (send 4 m 3)
#:ret (ret (-val 5) -bot-filter)
#:expected (ret (-val 5) -no-filter -no-obj)]
#:ret (ret (-val 5) -ff-propset)
#:expected (ret (-val 5) #f #f)]
;; Fails, sending to multiple/unknown values
[tc-err (send (values 'a 'b) m 'c)
#:msg #rx"expected single value"]
@ -857,7 +857,7 @@
(public [m m])
(define m (lambda () "a"))))
(send (new c%) m))
#:ret (ret -String -true-filter)]
#:ret (ret -String -true-propset)]
;; fails, internal name not accessible
[tc-err (let ()
(define c% (class object% (super-new)
@ -951,7 +951,7 @@
[tc-err (class object% (super-new)
(define/public (m) (n))
(define/public (n x) 0))
#:ret (ret (-class #:method ([m (t:-> -Bottom)] [n (t:-> Univ -Zero : -true-filter)])))
#:ret (ret (-class #:method ([m (t:-> -Bottom)] [n (t:-> Univ -Zero : -true-propset)])))
#:msg #rx"since it is not a function type"]
;; test type-checking for classes without any
;; internal type annotations on methods
@ -959,7 +959,7 @@
(define c% (class object% (super-new)
(define/public (m) "a")))
(send (new c%) m))
#:ret (ret -String -true-filter)]
#:ret (ret -String -true-propset)]
;; test inheritance without expected
[tc-e (let ()
(define c% (class (class object% (super-new)
@ -1006,7 +1006,7 @@
(-class
#:row (make-Row null `([x ,-Integer]) null null #f)
#:field ([x -Integer])))
-true-filter)]
-true-propset)]
;; fails, mixin argument is missing required field
[tc-err (let ()
(: f (All (A #:row (field x))
@ -1077,7 +1077,7 @@
(-class
#:row (make-Row null `([x ,-Integer]) null null #f)
#:field ([x -Integer])))
-true-filter)]
-true-propset)]
;; test bad manipulation of rows for inheritance
[tc-e (let ()
(: c% (Class (init [x String] [y String])))
@ -1394,7 +1394,7 @@
(define/pubment (foo x) 0)
(define/public (g x) (foo 3)))
#:ret (ret (-class #:method ([g (t:-> Univ -Bottom)]
[foo (t:-> Univ -Zero : -true-filter)])
[foo (t:-> Univ -Zero : -true-propset)])
#:augment ([foo top-func])))
#:msg #rx"Cannot apply expression of type Any"]
;; the next several tests are for positional init arguments
@ -1529,13 +1529,13 @@
(define/public (m a-foo) (get-field x a-foo))))
(void))
-Void]
;; test that filters are correctly handled for polymorphic classes
;; test that propositions are correctly handled for polymorphic classes
[tc-e (let ()
(class object%
(super-new)
(init x)))
#:ret (ret (-poly (A) (-class #:init ([x A #f]))))
#:expected (ret (-poly (A) (-class #:init ([x A #f]))) -no-filter -no-obj)]
#:expected (ret (-poly (A) (-class #:init ([x A #f]))) #f #f)]
;; test uses of a macro in the body of the class
[tc-e
(let ()

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

@ -135,7 +135,7 @@
(t (->key -Symbol #:key -Boolean #t Univ))
(t (make-Function
(list (make-arr* (list Univ) -Boolean #:kws (list (make-Keyword '#:key Univ #t))
#:filters (-FS (-filter -Symbol 0) (-not-filter -Symbol 0))))))
#:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol))))))
(t (-struct #'struct-name #f (list (make-fld -Symbol #'acc #f))))
;; Adapted from PR 13815
(t (-poly (a) (-> a a)))
@ -158,7 +158,7 @@
(-> (-class #:row (-v a)) (-class #:row (-v a)))))
(t (-mu x (-Syntax x)))
(t (-> (-> Univ -Bottom : -bot-filter) -Bottom : -bot-filter))
(t (-> (-> Univ -Bottom : -ff-propset) -Bottom : -ff-propset))
(t (-poly (A B) (-> A B (Un A B))))
@ -184,10 +184,10 @@
(t (make-Function
(list (make-arr* (list -String) -Boolean
#:kws (list (make-Keyword '#:key Univ #t))
#:filters (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))
#:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))
(make-arr* (list -String Univ) -Boolean
#:kws (list (make-Keyword '#:key Univ #t))
#:filters (-FS (-filter -Symbol 0) (-not-filter -Symbol 0))))))
#:props (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol))))))
(t/fail (cl->* (-> -String ManyUniv) (-> -String Univ ManyUniv))
"unknown return values")
@ -197,7 +197,7 @@
(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 filters or objects")
"function type with props or objects")
(t/fail (cl->*
(-> -Boolean -Boolean)
(-> -Symbol -Symbol))

148
typed-racket-test/unit-tests/filter-tests.rkt
View File

@ -1,148 +0,0 @@
#lang racket/base
(require "test-utils.rkt"
rackunit racket/format
(rep filter-rep)
(types abbrev union filter-ops)
(for-syntax racket/base syntax/parse))
(provide tests)
(gen-test-main)
(define (not-implied-atomic? x y) (not (implied-atomic? x y)))
(define-syntax (test-opposite stx)
(define-syntax-class complementary
(pattern #:complementary #:with check #'check-true)
(pattern #:not-complementary #:with check #'check-false))
(define-syntax-class contradictory
(pattern #:contradictory #:with check #'check-true)
(pattern #:not-contradictory #:with check #'check-false))
(syntax-parse stx
[(_ comp:complementary contr:contradictory f1* f2*)
(syntax/loc stx
(test-case (~a '(opposite f1* f2*))
(define f1 f1*)
(define f2 f2*)
(comp.check (complementary? f1 f2) "Complementary")
(contr.check (contradictory? f1 f2) "Contradictory")))]))
(define tests
(test-suite "Filters"
(test-suite "Opposite"
(test-opposite #:not-complementary #:contradictory
(-filter -Symbol 0)
(-not-filter (Un -Symbol -String) 0))
(test-opposite #:complementary #:not-contradictory
(-filter (Un -Symbol -String) 0)
(-not-filter -Symbol 0))
(test-opposite #:complementary #:contradictory
(-not-filter -Symbol 0)
(-filter -Symbol 0))
(test-opposite #:not-complementary #:not-contradictory
(-filter -Symbol 1)
(-not-filter -Symbol 0))
(test-opposite #:not-complementary #:not-contradictory
(-not-filter -Symbol 0)
(-filter -String 0))
(test-opposite #:not-complementary #:not-contradictory
(-not-filter -Symbol 0)
(-filter -String 0))
(test-opposite #:not-complementary #:contradictory
-bot
-bot)
(test-opposite #:not-complementary #:contradictory
-bot
-top)
(test-opposite #:complementary #:not-contradictory
-top
-top)
)
(test-suite "Implied Atomic"
(check implied-atomic?
-top -top)
(check implied-atomic?
-bot -bot)
(check implied-atomic?
-top -bot)
(check not-implied-atomic?
-bot -top)
(check implied-atomic?
-top (-filter -Symbol 0))
(check implied-atomic?
(-filter -Symbol 0) -bot)
(check implied-atomic?
(-filter (Un -String -Symbol) 0)
(-filter -Symbol 0))
(check not-implied-atomic?
(-filter -Symbol 0)
(-filter (Un -String -Symbol) 0))
(check implied-atomic?
(-not-filter -Symbol 0)
(-not-filter (Un -String -Symbol) 0))
(check not-implied-atomic?
(-not-filter (Un -String -Symbol) 0)
(-not-filter -Symbol 0))
(check not-implied-atomic?
(-filter -Symbol 1)
(-filter -Symbol 0))
(check implied-atomic?
(-filter -Symbol #'x)
(-filter -Symbol #'x))
(check implied-atomic?
(-or (-filter -Symbol 1) (-filter -Symbol #'x))
(-filter -Symbol #'x))
(check implied-atomic?
(-filter -Symbol #'x)
(-and (-filter -Symbol 1) (-filter -Symbol #'x)))
(check implied-atomic?
(-not-filter (-val #f) #'x)
(-filter -Symbol #'x))
)
(test-suite "Implication"
(check-equal? (-imp -bot (-filter -Symbol #'x)) -top)
(check-equal? (-imp -top (-filter -Symbol #'x)) (-filter -Symbol #'x))
(check-equal? (-imp (-filter -Symbol #'x) -top) -top)
(check-equal? (-imp (-filter -Symbol #'x) -bot) (-not-filter -Symbol #'x))
(check-equal? (-imp (-not-filter -Symbol #'x) -bot) (-filter -Symbol #'x))
(check-equal? (-imp (-imp (-not-filter -Symbol #'x) (-not-filter -Symbol #'y)) -bot)
(-and (-not-filter -Symbol #'x) (-filter -Symbol #'y)))
(check-equal?
(-imp (-not-filter -Symbol #'x)
(-not-filter -Symbol #'y))
(make-ImpFilter (-not-filter -Symbol #'x)
(-not-filter -Symbol #'y))))
(test-suite "Simplification"
(check-equal?
(-and (-filter -Symbol #'x) (-not-filter (-val #f) #'x))
(-filter -Symbol #'x))
(check-equal?
(-and (-not-filter (-val #f) #'x) (-filter -Symbol #'x))
(-filter -Symbol #'x))
(check-equal?
(-and (-filter (-val #f) #'y)
(-or (-filter (-val #f) #'y)
(-filter (-val #f) #'x)))
(-filter (-val #f) #'y))
(check-equal?
(-and (-not-filter (-val #f) #'y)
(-or (-not-filter (-val #f) #'y)
(-not-filter (-val #f) #'x)))
(-not-filter (-val #f) #'y)))
))

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

@ -3,8 +3,8 @@
(require "test-utils.rkt"
rackunit racket/format
(typecheck tc-metafunctions tc-subst)
(rep filter-rep type-rep object-rep)
(types abbrev union filter-ops tc-result numeric-tower)
(rep prop-rep type-rep object-rep)
(types abbrev union prop-ops tc-result numeric-tower)
(for-syntax racket/base syntax/parse))
(provide tests)
@ -29,17 +29,17 @@
(test-suite "combine-props"
(test-combine-props
(list (-or (-not-filter -String #'x) (-not-filter -String #'y)))
(list (-filter (Un -String -Symbol) #'x) (-filter (Un -String -Symbol) #'y))
(list (-or (-not-filter -String #'y) (-not-filter -String #'x))
(-filter (Un -String -Symbol) #'y) (-filter (Un -String -Symbol) #'x))
(list (-or (-not-type #'x -String) (-not-type #'y -String)))
(list (-is-type #'x (Un -String -Symbol)) (-is-type #'y (Un -String -Symbol)))
(list (-or (-not-type #'y -String) (-not-type #'x -String))
(-is-type #'y (Un -String -Symbol)) (-is-type #'x (Un -String -Symbol)))
#t)
(test-combine-props
(list (-or (-filter -String #'x) (-filter -String #'y)))
(list (-filter (Un -String -Symbol) #'x) (-filter (Un -String -Symbol) #'y))
(list (-or (-filter -String #'y) (-filter -String #'x))
(-filter (Un -String -Symbol) #'y) (-filter (Un -String -Symbol) #'x))
(list (-or (-is-type #'x -String) (-is-type #'y -String)))
(list (-is-type #'x (Un -String -Symbol)) (-is-type #'y (Un -String -Symbol)))
(list (-or (-is-type #'y -String) (-is-type #'x -String))
(-is-type #'y (Un -String -Symbol)) (-is-type #'x (Un -String -Symbol)))
#t)
)
@ -51,20 +51,20 @@
(merge-tc-results (list (ret Univ)))
(ret Univ))
(check-equal?
(merge-tc-results (list (ret Univ -top-filter (make-Path null #'x))))
(ret Univ -top-filter (make-Path null #'x)))
(merge-tc-results (list (ret Univ -tt-propset (make-Path null #'x))))
(ret Univ -tt-propset (make-Path null #'x)))
(check-equal?
(merge-tc-results (list (ret -Bottom) (ret -Symbol -top-filter (make-Path null #'x))))
(ret -Symbol -top-filter (make-Path null #'x)))
(merge-tc-results (list (ret -Bottom) (ret -Symbol -tt-propset (make-Path null #'x))))
(ret -Symbol -tt-propset (make-Path null #'x)))
(check-equal?
(merge-tc-results (list (ret -String) (ret -Symbol)))
(ret (Un -Symbol -String)))
(check-equal?
(merge-tc-results (list (ret -String -true-filter) (ret -Symbol -true-filter)))
(ret (Un -Symbol -String) -true-filter))
(merge-tc-results (list (ret -String -true-propset) (ret -Symbol -true-propset)))
(ret (Un -Symbol -String) -true-propset))
(check-equal?
(merge-tc-results (list (ret (-val #f) -false-filter) (ret -Symbol -true-filter)))
(ret (Un -Symbol (-val #f)) -top-filter))
(merge-tc-results (list (ret (-val #f) -false-propset) (ret -Symbol -true-propset)))
(ret (Un -Symbol (-val #f)) -tt-propset))
(check-equal?
(merge-tc-results (list (ret (list (-val 0) (-val 1))) (ret (list (-val 1) (-val 2)))))
(ret (list (Un (-val 0) (-val 1)) (Un (-val 1) (-val 2)))))
@ -85,97 +85,90 @@
(ret (list -Symbol -String)))
(check-equal?
(values->tc-results (make-Values (list (-result -Symbol (-FS -top -bot)))) (list -empty-obj) (list Univ))
(ret -Symbol (-FS -top -bot)))
(values->tc-results (make-Values (list (-result -Symbol (-PS -tt -ff)))) (list -empty-obj) (list Univ))
(ret -Symbol (-PS -tt -ff)))
(check-equal?
(values->tc-results (make-Values (list (-result -Symbol (-FS -top -bot) (make-Path null '(0 0)))))
(values->tc-results (make-Values (list (-result -Symbol (-PS -tt -ff) (make-Path null '(0 0)))))
(list -empty-obj) (list Univ))
(ret -Symbol (-FS -top -bot)))
(ret -Symbol (-PS -tt -ff)))
(check-equal?
(values->tc-results (make-Values (list (-result (-opt -Symbol) (-FS (-filter -String '(0 0)) -top))))
(values->tc-results (make-Values (list (-result (-opt -Symbol) (-PS (-is-type '(0 0) -String) -tt))))
(list -empty-obj) (list Univ))
(ret (-opt -Symbol) -top-filter))
(ret (-opt -Symbol) -tt-propset))
(check-equal?
(values->tc-results (make-Values (list (-result (-opt -Symbol) (-FS (-not-filter -String '(0 0)) -top))))
(values->tc-results (make-Values (list (-result (-opt -Symbol) (-PS (-not-type '(0 0) -String) -tt))))
(list -empty-obj) (list Univ))
(ret (-opt -Symbol) -top-filter))
(ret (-opt -Symbol) -tt-propset))
(check-equal?
(values->tc-results (make-Values (list (-result (-opt -Symbol) (-FS (-imp (-not-filter (-val #f) '(0 0))
(-not-filter -String #'x))
-top))))
(list -empty-obj) (list Univ))
(ret (-opt -Symbol) -top-filter))
(check-equal?
(values->tc-results (make-Values (list (-result (-opt -Symbol) (-FS (-not-filter -String '(0 0)) -top)
(values->tc-results (make-Values (list (-result (-opt -Symbol) (-PS (-not-type '(0 0) -String) -tt)
(make-Path null '(0 0)))))
(list (make-Path null #'x)) (list Univ))
(ret (-opt -Symbol) (-FS (-not-filter -String #'x) -top) (make-Path null #'x)))
(ret (-opt -Symbol) (-PS (-not-type #'x -String) -tt) (make-Path null #'x)))
;; Check additional filters
;; Check additional props
(check-equal?
(values->tc-results (make-Values (list (-result (-opt -String) (-FS -top (-not-filter -String '(0 0)))
(values->tc-results (make-Values (list (-result (-opt -String) (-PS -tt (-not-type '(0 0) -String))
(make-Path null '(0 0)))))
(list (make-Path null #'x)) (list -String))
(ret -String -true-filter (make-Path null #'x)))
(ret -String -true-propset (make-Path null #'x)))
;; Substitute into ranges correctly
(check-equal?
(values->tc-results (make-Values (list (-result (-opt (-> Univ -Boolean : (-FS (-filter -Symbol '(0 0)) -top))))))
(values->tc-results (make-Values (list (-result (-opt (-> Univ -Boolean : (-PS (-is-type '(0 0) -Symbol) -tt))))))
(list (make-Path null #'x)) (list Univ))
(ret (-opt (-> Univ -Boolean : (-FS (-filter -Symbol '(0 0)) -top)))))
(ret (-opt (-> Univ -Boolean : (-PS (-is-type '(0 0) -Symbol) -tt)))))
(check-equal?
(values->tc-results (make-Values (list (-result (-opt (-> Univ -Boolean : (-FS (-filter -Symbol '(1 0)) -top))))))
(values->tc-results (make-Values (list (-result (-opt (-> Univ -Boolean : (-PS (-is-type '(1 0) -Symbol) -tt))))))
(list (make-Path null #'x)) (list Univ))
(ret (-opt (-> Univ -Boolean : (-FS (-filter -Symbol #'x) -top)))))
(ret (-opt (-> Univ -Boolean : (-PS (-is-type #'x -Symbol) -tt)))))
;; Substitute into filter of any values
;; Substitute into prop of any values
(check-equal?
(values->tc-results (make-AnyValues (-filter -String '(0 0)))
(values->tc-results (make-AnyValues (-is-type '(0 0) -String))
(list (make-Path null #'x)) (list Univ))
(tc-any-results (-filter -String #'x)))
(tc-any-results (-is-type #'x -String)))
(check-equal?
(values->tc-results (-values-dots null (-> Univ -Boolean : (-FS (-filter -String '(1 0)) -top)) 'b)
(values->tc-results (-values-dots null (-> Univ -Boolean : (-PS (-is-type '(1 0) -String) -tt)) 'b)
(list (make-Path null #'x)) (list Univ))
(ret null null null (-> Univ -Boolean : (-FS (-filter -String #'x) -top)) 'b))
(ret null null null (-> Univ -Boolean : (-PS (-is-type #'x -String) -tt)) 'b))
;; Filter is restricted by type of object
;; Prop is restricted by type of object
(check-equal?
(values->tc-results (make-Values (list (-result -Boolean (-FS (-filter -PosReal '(0 0)) (-filter -NonPosReal '(0 0))))))
(values->tc-results (make-Values (list (-result -Boolean (-PS (-is-type '(0 0) -PosReal) (-is-type '(0 0) -NonPosReal)))))
(list (make-Path null #'x)) (list -Integer))
(ret -Boolean (-FS (-filter -PosInt #'x) (-filter -NonPosInt #'x))))
(ret -Boolean (-PS (-is-type #'x -PosInt) (-is-type #'x -NonPosInt))))
;; Filter restriction accounts for paths
;; Prop restriction accounts for paths
(check-equal?
(values->tc-results
(make-Values
(list (-result -Boolean
(-FS (make-TypeFilter -PosReal
(make-Path (list -car) '(0 0)))
(make-TypeFilter -NonPosReal
(make-Path (list -car) '(0 0)))))))
(-PS (make-TypeProp (make-Path (list -car) '(0 0))
-PosReal)
(make-TypeProp (make-Path (list -car) '(0 0))
-NonPosReal)))))
(list (make-Path null #'x))
(list (-lst -Integer)))
(ret -Boolean
(-FS (make-TypeFilter -PosInt (make-Path (list -car) #'x))
(make-TypeFilter -NonPosInt (make-Path (list -car) #'x)))))
(-PS (make-TypeProp (make-Path (list -car) #'x) -PosInt)
(make-TypeProp (make-Path (list -car) #'x) -NonPosInt))))
)
(test-suite "replace-names"
(check-equal?
(replace-names (list (list #'x (make-Path null (list 0 0))))
(ret Univ -top-filter (make-Path null #'x)))
(ret Univ -top-filter (make-Path null (list 0 0))))
(ret Univ -tt-propset (make-Path null #'x)))
(ret Univ -tt-propset (make-Path null (list 0 0))))
(check-equal?
(replace-names (list (list #'x (make-Path null (list 0 0))))
(ret (-> Univ Univ : -top-filter : (make-Path null #'x))))
(ret (-> Univ Univ : -top-filter : (make-Path null (list 1 0)))))
(ret (-> Univ Univ : -tt-propset : (make-Path null #'x))))
(ret (-> Univ Univ : -tt-propset : (make-Path null (list 1 0)))))
)
))

24
typed-racket-test/unit-tests/parse-type-tests.rkt
View File

@ -163,26 +163,26 @@
[(-> Any Boolean : #:+ (Number @ 0) #:- (! Number @ 0))
(make-pred-ty -Number)]
[(Any -> Boolean : #:+ (! Number @ 0) #:- (Number @ 0))
(t:->* (list Univ) -Boolean : (-FS (-not-filter -Number 0) (-filter -Number 0)))]
(t:->* (list Univ) -Boolean : (-PS (-not-type 0 -Number) (-is-type 0 -Number)))]
[(-> Any Boolean : #:+ (! Number @ 0) #:- (Number @ 0))
(t:->* (list Univ) -Boolean : (-FS (-not-filter -Number 0) (-filter -Number 0)))]
(t:->* (list Univ) -Boolean : (-PS (-not-type 0 -Number) (-is-type 0 -Number)))]
[(-> Any (-> Any Boolean : #:+ (Number @ 1 0) #:- (! Number @ 1 0)))
(t:-> Univ
(t:->* (list Univ) -Boolean : (-FS (-filter -Number '(1 0)) (-not-filter -Number '(1 0)))))]
(t:->* (list Univ) -Boolean : (-PS (-is-type '(1 0) -Number) (-not-type '(1 0) -Number))))]
[(-> Any Any (-> Any Boolean : #:+ (Number @ 1 1) #:- (! Number @ 1 1)))
(t:-> Univ Univ
(t:->* (list Univ) -Boolean : (-FS (-filter -Number '(1 1)) (-not-filter -Number '(1 1)))))]
(t:->* (list Univ) -Boolean : (-PS (-is-type '(1 1) -Number) (-not-type '(1 1) -Number))))]
[(-> Any #:foo Any (-> Any Boolean : #:+ (Number @ 1 0) #:- (! Number @ 1 0)))
(->key Univ #:foo Univ #t
(t:->* (list Univ) -Boolean : (-FS (-filter -Number '(1 0)) (-not-filter -Number '(1 0)))))]
(t:->* (list Univ) -Boolean : (-PS (-is-type '(1 0) -Number) (-not-type '(1 0) -Number))))]
[(All (a b) (-> (-> a Any : #:+ b) (Listof a) (Listof b)))
(-poly (a b) (t:-> (asym-pred a Univ (-FS (-filter b 0) -top)) (-lst a) (-lst b)))]
(-poly (a b) (t:-> (asym-pred a Univ (-PS (-is-type 0 b) -tt)) (-lst a) (-lst b)))]
[(All (a b) (-> (-> a Any : #:+ (! b)) (Listof a) (Listof b)))
(-poly (a b) (t:-> (asym-pred a Univ (-FS (-not-filter b 0) -top)) (-lst a) (-lst b)))]
(-poly (a b) (t:-> (asym-pred a Univ (-PS (-not-type 0 b) -tt)) (-lst a) (-lst b)))]
[(All (a b) (-> (-> a Any : #:- b) (Listof a) (Listof b)))
(-poly (a b) (t:-> (asym-pred a Univ (-FS -top (-filter b 0))) (-lst a) (-lst b)))]
(-poly (a b) (t:-> (asym-pred a Univ (-PS -tt (-is-type 0 b))) (-lst a) (-lst b)))]
[(All (a b) (-> (-> a Any : #:- (! b)) (Listof a) (Listof b)))
(-poly (a b) (t:-> (asym-pred a Univ (-FS -top (-not-filter b 0))) (-lst a) (-lst b)))]
(-poly (a b) (t:-> (asym-pred a Univ (-PS -tt (-not-type 0 b))) (-lst a) (-lst b)))]
[(Number -> Number -> Number)
(t:-> -Number (t:-> -Number -Number))]
[(-> Number (-> Number Number))
@ -201,11 +201,11 @@
[(Any -> Boolean : #:+ (Symbol @ not-mutated-var))
(t:-> Univ -Boolean : (-FS (-filter -Symbol (-id-path #'not-mutated-var)) -top))]
(t:-> Univ -Boolean : (-PS (-is-type (-id-path #'not-mutated-var) -Symbol) -tt))]
[FAIL (Any -> Boolean : #:+ (Symbol @ mutated-var))
#:msg "may not reference identifiers that are mutated"]
[(Any -> Boolean : #:+ (! Symbol @ not-mutated-var))
(t:-> Univ -Boolean : (-FS (-not-filter -Symbol (-id-path #'not-mutated-var)) -top))]
(t:-> Univ -Boolean : (-PS (-not-type (-id-path #'not-mutated-var) -Symbol) -tt))]
[FAIL (Any -> Boolean : #:+ (! Symbol @ mutated-var))
#:msg "may not reference identifiers that are mutated"]
[FAIL (Any -> Boolean : #:+ (String @ unbound))
@ -239,7 +239,7 @@
[(->* (#:bar Integer Integer) (#:foo Integer String) Void)
(->optkey -Integer [-String] #:bar -Integer #t #:foo -Integer #f -Void)]
[(->* (Any (-> Any Boolean : #:+ (String @ 1 0))) Void)
(t:-> Univ (t:->* (list Univ) -Boolean : (-FS (-filter -String '(1 0)) -top))
(t:-> Univ (t:->* (list Univ) -Boolean : (-PS (-is-type '(1 0) -String) -tt))
-Void)]
[FAIL (->* (Any (-> Any Boolean : #:+ (String @ 2 0))) Void)
#:msg "Index 2 used in"]

134
typed-racket-test/unit-tests/prop-tests.rkt Normal file
View File

@ -0,0 +1,134 @@
#lang racket/base
(require "test-utils.rkt"
rackunit racket/format
(rep prop-rep)
(types abbrev union prop-ops)
(for-syntax racket/base syntax/parse))
(provide tests)
(gen-test-main)
(define (not-implies-atomic? y x) (not (implies-atomic? y x)))
(define-syntax (test-opposite stx)
(define-syntax-class complementary
(pattern #:complementary #:with check #'check-true)
(pattern #:not-complementary #:with check #'check-false))
(define-syntax-class contradictory
(pattern #:contradictory #:with check #'check-true)
(pattern #:not-contradictory #:with check #'check-false))
(syntax-parse stx
[(_ comp:complementary contr:contradictory p1* p2*)
(syntax/loc stx
(test-case (~a '(opposite p1* p2*))
(define p1 p1*)
(define p2 p2*)
(comp.check (complementary? p1 p2) "Complementary")
(contr.check (contradictory? p1 p2) "Contradictory")))]))
(define tests
(test-suite "Props"
(test-suite "Opposite"
(test-opposite #:not-complementary #:contradictory
(-is-type 0 -Symbol)
(-not-type 0 (Un -Symbol -String)))
(test-opposite #:complementary #:not-contradictory
(-is-type 0 (Un -Symbol -String))
(-not-type 0 -Symbol))
(test-opposite #:complementary #:contradictory
(-not-type 0 -Symbol)
(-is-type 0 -Symbol))
(test-opposite #:not-complementary #:not-contradictory
(-is-type 1 -Symbol)
(-not-type 0 -Symbol))
(test-opposite #:not-complementary #:not-contradictory
(-not-type 0 -Symbol)
(-is-type 0 -String))
(test-opposite #:not-complementary #:not-contradictory
(-not-type 0 -Symbol)
(-is-type 0 -String))
(test-opposite #:not-complementary #:contradictory
-ff
-ff)
(test-opposite #:not-complementary #:contradictory
-ff
-tt)
(test-opposite #:complementary #:not-contradictory
-tt
-tt)
)
(test-suite "Implies Atomic"
(check implies-atomic?
-tt -tt)
(check implies-atomic?
-ff -ff)
(check implies-atomic?
-ff -tt)
(check not-implies-atomic?
-tt -ff)
(check implies-atomic?
(-is-type 0 -Symbol) -tt)
(check implies-atomic?
-ff (-is-type 0 -Symbol))
(check implies-atomic?
(-is-type 0 -Symbol)
(-is-type 0 (Un -String -Symbol)))
(check not-implies-atomic?
(-is-type 0 (Un -String -Symbol))
(-is-type 0 -Symbol))
(check implies-atomic?
(-not-type 0 (Un -String -Symbol))
(-not-type 0 -Symbol))
(check not-implies-atomic?
(-not-type 0 -Symbol)
(-not-type 0 (Un -String -Symbol)))
(check not-implies-atomic?
(-is-type 0 -Symbol)
(-is-type 1 -Symbol))
(check implies-atomic?
(-is-type #'x -Symbol)
(-is-type #'x -Symbol))
(check implies-atomic?
(-is-type #'x -Symbol)
(-or (-is-type 1 -Symbol) (-is-type #'x -Symbol)))
(check implies-atomic?
(-and (-is-type 1 -Symbol) (-is-type #'x -Symbol))
(-is-type #'x -Symbol))
(check implies-atomic?
(-is-type #'x -Symbol)
(-not-type #'x (-val #f)))
)
(test-suite "Simplification"
(check-equal?
(-and (-is-type #'x -Symbol) (-not-type #'x (-val #f)))
(-is-type #'x -Symbol))
(check-equal?
(-and (-not-type #'x (-val #f)) (-is-type #'x -Symbol))
(-is-type #'x -Symbol))
(check-equal?
(-and (-is-type #'y (-val #f))
(-or (-is-type #'y (-val #f))
(-is-type #'x (-val #f))))
(-is-type #'y (-val #f)))
(check-equal?
(-and (-not-type #'y (-val #f))
(-or (-not-type #'y (-val #f))
(-not-type #'x (-val #f))))
(-not-type #'y (-val #f))))
))

8
typed-racket-test/unit-tests/special-env-typecheck-tests.rkt
View File

@ -4,8 +4,8 @@
"evaluator.rkt"
(for-syntax racket/base)
(for-template racket/base)
(rep type-rep filter-rep object-rep)
(for-syntax (rename-in (types utils union numeric-tower abbrev filter-ops)
(rep type-rep prop-rep object-rep)
(for-syntax (rename-in (types utils union numeric-tower abbrev prop-ops)
[Un t:Un]
[-> t:->]))
(utils tc-utils utils)
@ -27,7 +27,7 @@
(begin-for-syntax (do-standard-inits))
(define-syntax-rule (tc-e/t e t) (tc-e e #:ret (ret t -true-filter)))
(define-syntax-rule (tc-e/t e t) (tc-e e #:ret (ret t -true-propset)))
(define-syntax (tc-e stx)
(syntax-parse stx
@ -120,7 +120,7 @@
;; exception handling
[tc-e (with-handlers ([void (λ (x) (values 0 0))]) (values "" ""))
#:ret (ret (list (t:Un -Zero -String) (t:Un -Zero -String))
(list -true-filter -true-filter))]
(list -true-propset -true-propset))]
(tc-e (make-temporary-file) -Path)
(tc-e (make-temporary-file "ee~a") -Path)

34
typed-racket-test/unit-tests/subtype-tests.rkt
View File

@ -248,24 +248,24 @@
(-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 : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))
(-> Univ -Boolean : -top-filter)]
[(-> Univ -Boolean : -bot-filter)
(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))]
[(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))
(-> (Un -Symbol -String) -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))]
[(-> Univ -Boolean : (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))
(-> Univ -Boolean : -tt-propset)]
[(-> Univ -Boolean : -ff-propset)
(-> Univ -Boolean : (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))]
[(-> Univ -Boolean : (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))
(-> (Un -Symbol -String) -Boolean : (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))]
[FAIL
(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))
(-> Univ -Boolean : (-FS (-filter -String 0) (-not-filter -String 0)))]
(-> Univ -Boolean : (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))
(-> Univ -Boolean : (-PS (-is-type 0 -String) (-not-type 0 -String)))]
;; subtyping for types inside filters
[(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))
(-> Univ -Boolean : (-FS (-filter (-opt -Symbol) 0) (-not-filter -Symbol 0)))]
[(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter (-opt -Symbol) 0)))
(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))]
;; subtyping for types inside propositions
[(-> Univ -Boolean : (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))
(-> Univ -Boolean : (-PS (-is-type 0 (-opt -Symbol)) (-not-type 0 -Symbol)))]
[(-> Univ -Boolean : (-PS (-is-type 0 -Symbol) (-not-type 0 (-opt -Symbol))))
(-> Univ -Boolean : (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))]
[FAIL
(-> Univ -Boolean : (-FS (-filter (-opt -Symbol) 0) (-not-filter (-opt -Symbol) 0)))
(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))]
(-> Univ -Boolean : (-PS (-is-type 0 (-opt -Symbol)) (-not-type 0 (-opt -Symbol))))
(-> Univ -Boolean : (-PS (-is-type 0 -Symbol) (-not-type 0 -Symbol)))]
[FAIL (make-ListDots (-box (make-F 'a)) 'a) (-lst (-box Univ))]
[(make-ListDots (-> -Symbol (make-F 'a)) 'a) (-lst (-> -Symbol Univ))]
@ -276,7 +276,7 @@
[(-> Univ -Bottom) (-> Univ (-values (list -String -Symbol)))]
[(-> Univ -Bottom) (-> Univ (-values-dots null -String 'x))]
[FAIL (make-pred-ty -String) (-> Univ (-AnyValues (-filter -String 0)))]
[FAIL (make-pred-ty -String) (-> Univ (-AnyValues (-is-type 0 -String)))]
;; keyword function types
[(->key #:x -Symbol #f Univ) (->key Univ)]
@ -371,7 +371,7 @@
[FAIL
(-prefab '(foo #()) -String) (-prefab '(foo #(0)) (-opt -String))]
;; Filter subtyping
;; Proposition subtyping
((make-pred-ty (list -Real) -Boolean (Un (-val 0.0) (-val 0)))
(make-pred-ty (list -Int) -Boolean (-val 0)))

36
typed-racket-test/unit-tests/type-printer-tests.rkt
View File

@ -1,6 +1,6 @@
#lang racket/base
;; Tests for type, filter, object, etc. printers for Typed Racket
;; Tests for type, prop, object, etc. printers for Typed Racket
(require "test-utils.rkt"
rackunit
@ -74,29 +74,29 @@
(check-prints-as? (-mu x (-lst x)) "(Rec x (Listof x))")
(check-prints-as? (-seq -String -Symbol) "(Sequenceof String Symbol)")
(check-prints-as? (-poly (a) (-> a -Void)) "(All (a) (-> a Void))")
(check-prints-as? (-> -Input-Port (make-Values (list (-result -String -true-filter)
(-result -String -true-filter))))
(check-prints-as? (-> -Input-Port (make-Values (list (-result -String -true-propset)
(-result -String -true-propset))))
"(-> Input-Port (values (String : (Top | Bot)) (String : (Top | Bot))))")
(check-prints-as? (make-pred-ty -String)
"(-> Any Boolean : String)")
(check-prints-as? (asym-pred Univ -Boolean (-FS (-filter -String 0) -top))
(check-prints-as? (asym-pred Univ -Boolean (-PS (-is-type 0 -String) -tt))
"(-> Any Boolean : #:+ String)")
(check-prints-as? (-> Univ Univ -Boolean : (-FS (-filter -String 0) -top))
(check-prints-as? (-> Univ Univ -Boolean : (-PS (-is-type 0 -String) -tt))
"(-> Any Any Boolean)")
(check-prints-as? (-> Univ Univ -Boolean : (-FS (-filter -String 1) -top))
(check-prints-as? (-> Univ Univ -Boolean : (-PS (-is-type 1 -String) -tt))
"(-> Any Any Boolean)")
;; PR 14510 (next three tests)
(check-prints-as? (-> Univ (-> Univ -Boolean : (-FS (-filter -String '(1 0))
(-not-filter -String '(1 0)))))
(check-prints-as? (-> Univ (-> Univ -Boolean : (-PS (-is-type '(1 0) -String)
(-not-type '(1 0) -String))))
"(-> Any (-> Any Boolean))")
(check-prints-as? (-> Univ Univ -Boolean : (-FS (-filter -String '(0 1))
(-not-filter -String '(0 1))))
(check-prints-as? (-> Univ Univ -Boolean : (-PS (-is-type '(0 1) -String)
(-not-type '(0 1) -String)))
"(-> Any Any Boolean)")
(check-prints-as? (-> Univ Univ -Boolean : (-FS (-filter -String '(0 0))
(-not-filter -String '(0 0))))
(check-prints-as? (-> Univ Univ -Boolean : (-PS (-is-type '(0 0) -String)
(-not-type '(0 0) -String)))
"(-> Any Any Boolean)")
(check-prints-as? (-> Univ (make-Values (list (-result -String -top-filter -empty-obj)
(-result -String -top-filter -empty-obj))))
(check-prints-as? (-> Univ (make-Values (list (-result -String -tt-propset -empty-obj)
(-result -String -tt-propset -empty-obj))))
"(-> Any (values String String))")
;; this case tests that the Number union is printed with its name
;; rather than its expansion (a former bug)
@ -114,11 +114,11 @@
" 'append 'update 'replace 'truncate"
" 'truncate/replace)] [#:mode (U"
" 'binary 'text)] Void)"))
(check-prints-as? (-> Univ (-AnyValues -top)) "(-> Any AnyValues)")
(check-prints-as? (-> Univ (-AnyValues (-filter -String '(0 0))))
(check-prints-as? (-> Univ (-AnyValues -tt)) "(-> Any AnyValues)")
(check-prints-as? (-> Univ (-AnyValues (-is-type '(0 0) -String)))
"(-> Any AnyValues : (String @ (0 0)))")
(check-prints-as? (-AnyValues -top) "AnyValues")
(check-prints-as? (-AnyValues (-filter -String '(0 0)))
(check-prints-as? (-AnyValues -tt) "AnyValues")
(check-prints-as? (-AnyValues (-is-type '(0 0) -String))
"(AnyValues : (String @ (0 0)))")
(check-prints-as? (->opt Univ [] -Void) "(-> Any Void)")

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

File diff suppressed because it is too large Load Diff

4
typed-racket-test/unit-tests/typed-units-tests.rkt
View File

@ -23,8 +23,8 @@
base-types base-types-extra)
define lambda λ case-lambda)
(prefix-in tr: (only-in (base-env prims) define lambda λ case-lambda))
(for-syntax (rep type-rep filter-rep object-rep)
(rename-in (types abbrev union numeric-tower filter-ops utils)
(for-syntax (rep type-rep prop-rep object-rep)
(rename-in (types abbrev union numeric-tower prop-ops utils)
[Un t:Un]
[-> t:->])))