Compare commits

..

2 Commits

278 changed files with 3694 additions and 9248 deletions

View File

@ -20,12 +20,12 @@ install:
- raco setup typed typed-racket typed-racket-test typed-scheme
script:
- racket -l typed-racket-test -- --unit
- racket -l typed-racket-test -- --int
- racket -l typed-racket-test -- --opt
- racket -l typed-racket-test -- --missed-opt
- racket -l typed-racket-test/run -- --unit
- racket -l typed-racket-test/run -- --int
- racket -l typed-racket-test/run -- --opt
- racket -l typed-racket-test/run -- --missed-opt
- raco setup -j 1 math
- racket -l typed-racket-test -- --math
- racket -l typed-racket-test/run -- --math
- racket -l typed-racket-test/test-docs-complete
- echo "done"

View File

@ -1,7 +0,0 @@
### What version of Racket are you using?
### What program did you run?
### What should have happened?
### If you got an error message, please include it here.

View File

@ -11,4 +11,4 @@
(define pkg-authors '(samth stamourv))
(define version "1.5")
(define version "1.1")

View File

@ -6,11 +6,14 @@ typed-scheme
#:read-syntax r:read-syntax
#:info make-info
(require (prefix-in r: typed-racket/typed-reader)
typed-racket/private/oc-button)
(require (prefix-in r: typed-racket/typed-reader))
(define (make-info key default use-default)
(case key
[(drscheme:toolbar-buttons)
(maybe-show-OC)]
;; If Optimization Coach is installed, load it.
(with-handlers ([exn:fail:filesystem? (lambda _ '())]) ; not found
(collection-path "optimization-coach")
(list (dynamic-require 'optimization-coach/tool
'optimization-coach-drracket-button)))]
[else (use-default key default)]))

View File

@ -7,12 +7,14 @@ typed/scheme/base
#:info make-info
#:language-info make-language-info
(require typed-racket/private/oc-button)
(define (make-info key default use-default)
(case key
[(drscheme:toolbar-buttons)
(maybe-show-OC)]
;; If Optimization Coach is installed, load it.
(with-handlers ([exn:fail:filesystem? (lambda _ '())]) ; not found
(collection-path "optimization-coach")
(list (dynamic-require 'optimization-coach/tool
'optimization-coach-drracket-button)))]
[else (use-default key default)]))
(define make-language-info

View File

@ -7,12 +7,14 @@ typed/scheme
#:info make-info
#:language-info make-language-info
(require typed-racket/private/oc-button)
(define (make-info key default use-default)
(case key
[(drscheme:toolbar-buttons)
(maybe-show-OC)]
;; If Optimization Coach is installed, load it.
(with-handlers ([exn:fail:filesystem? (lambda _ '())]) ; not found
(collection-path "optimization-coach")
(list (dynamic-require 'optimization-coach/tool
'optimization-coach-drracket-button)))]
[else (use-default key default)]))
(define make-language-info

View File

@ -10,13 +10,12 @@
"r6rs-lib"
"sandbox-lib"
"at-exp-lib"
("scribble-lib" #:version "1.16")
"scribble-lib"
"pict-lib"
("typed-racket-lib" #:version "1.5")
"typed-racket-lib"
"typed-racket-compatibility"
"typed-racket-more"
"racket-doc"
"draw-lib"))
"racket-doc"))
(define deps '("base"))
(define update-implies '("typed-racket-lib"))
@ -24,4 +23,4 @@
(define pkg-authors '(samth stamourv))
(define version "1.5")
(define version "1.1")

View File

@ -1,7 +1,6 @@
#lang scribble/manual
@begin[(require (for-label (only-meta-in 0 typed/racket))
scribble/example
@begin[(require (for-label (only-meta-in 0 typed/racket)) scribble/eval
"../utils.rkt" (only-in "quick.scrbl" typed-mod))]
@(define the-eval (make-base-eval))
@ -24,7 +23,7 @@ are provided as well; for example, the
@racketmodname[typed/racket/base] language corresponds to
@racketmodname[racket/base].
@examples[#:no-result #:eval the-eval (struct pt ([x : Real] [y : Real]))]
@racketblock+eval[#:eval the-eval (struct pt ([x : Real] [y : Real]))]
@margin-note{Typed Racket provides modified versions of core Racket forms,
which permit type annotations. Previous versions of Typed Racket provided
@ -35,11 +34,11 @@ This defines a new structure, named @racket[pt], with two fields,
@racket[Real], which corresponds to the @rtech{real numbers}.
The
@racket[struct] form corresponds to its untyped counterpart from
@racketmodname[racket]---when porting a program from
from @racketmodname[racket]---when porting a program from
@racketmodname[racket] to @racketmodname[typed/racket], simply add
type annotations to existing field declarations.
@examples[#:no-result #:eval the-eval (: distance (-> pt pt Real))]
@racketblock+eval[#:eval the-eval (: distance (-> pt pt Real))]
This declares that @racket[distance] has the type @racket[(-> pt pt Real)].
@;{@racket[distance] must be defined at the top-level of the module containing
@ -55,7 +54,7 @@ function type, in this case @racket[Real].
If you are familiar with @rtech{contracts}, the notation for function
types is similar to function contract combinators.
@examples[#:no-result #:eval the-eval
@racketblock+eval[#:eval the-eval
(define (distance p1 p2)
(sqrt (+ (sqr (- (pt-x p2) (pt-x p1)))
(sqr (- (pt-y p2) (pt-y p1))))))
@ -72,14 +71,14 @@ the program is accepted.
In the Typed Racket @gtech{REPL}, calling @racket[distance] will
show the result as usual and will also print the result's type:
@examples[#:label #f #:eval the-eval (distance (pt 0 0) (pt 3.1415 2.7172))]
@interaction[#:eval the-eval (distance (pt 0 0) (pt 3.1415 2.7172))]
Just evaluating the function name will print the function value and its type,
which can be useful for discovering the types that Typed Racket ascribes to
Racket functions. Alternatively, the @racket[:print-type] command will just
print the type:
@examples[#:label #f #:eval the-eval distance string-length (:print-type string-ref)]
@interaction[#:eval the-eval distance string-length (:print-type string-ref)]
@section{Datatypes and Unions}
@ -142,14 +141,14 @@ When Typed Racket detects a type error in the module, it raises an
error before running the program.
@examples[#:eval the-eval
(eval:error (add1 "not a number"))
(add1 "not a number")
]
@;{
Typed Racket also attempts to detect more than one error in the module.
@examples[#:eval the-eval
(eval:error (string-append "a string" (add1 "not a number")))
(string-append "a string" (add1 "not a number"))
]
}

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@(require "../utils.rkt"
scribble/example
scribble/eval
(for-label (only-meta-in 0 typed/racket)))
@(define the-eval (make-base-eval))
@ -38,19 +38,19 @@ on higher-order arguments that are themselves polymorphic.
For example, the following program results in a type error
that demonstrates this limitation:
@examples[#:label #f #:eval the-eval
(eval:error (map cons '(a b c d) '(1 2 3 4)))
@interaction[#:eval the-eval
(map cons '(a b c d) '(1 2 3 4))
]
The issue is that the type of @racket[cons] is also polymorphic:
@examples[#:label #f #:eval the-eval cons]
@interaction[#:eval the-eval cons]
To make this expression type-check, the @racket[inst] form can
be used to instantiate the polymorphic argument (e.g., @racket[cons])
at a specific type:
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
(map (inst cons Symbol Integer) '(a b c d) '(1 2 3 4))
]
@ -69,11 +69,10 @@ fixed in a future release.
The following illustrates an example type that cannot be
converted to a contract:
@examples[#:label #f #:eval the-eval
(eval:error
(require/typed racket/base
[object-name (case-> (-> Struct-Type-Property Symbol)
(-> Regexp (U String Bytes)))]))
@interaction[#:eval the-eval
(require/typed racket/base
[object-name (case-> (-> Struct-Type-Property Symbol)
(-> Regexp (U String Bytes)))])
]
This function type by cases is a valid type, but a corresponding
@ -84,7 +83,7 @@ supported with dependent contracts.
A more approximate type will work for this case, but with a loss
of type precision at use sites:
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
(require/typed racket/base
[object-name (-> (U Struct-Type-Property Regexp)
(U String Bytes Symbol))])
@ -95,8 +94,8 @@ Use of @racket[define-predicate] also involves contract generation, and
so some types cannot have predicates generated for them. The following
illustrates a type for which a predicate can't be generated:
@examples[#:label #f #:eval the-eval
(eval:error (define-predicate p? (All (A) (Listof A))))]
@interaction[#:eval the-eval
(define-predicate p? (All (A) (Listof A)))]
@section{Unsupported features}
@ -110,7 +109,7 @@ To make programming with invariant type constructors (such as @racket[Boxof])
easier, Typed Racket generalizes types that are used as arguments to invariant
type constructors. For example:
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
0
(define b (box 0))
b
@ -124,7 +123,7 @@ initialize it with @racket[0]. Type generalization does exactly that.
In some cases, however, type generalization can lead to unexpected results:
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
(box (ann 1 Fixnum))
]
@ -132,7 +131,7 @@ The intent of this code may be to create of box of @racket[Fixnum], but Typed
Racket will generalize it anyway. To create a box of @racket[Fixnum], the box
itself should have a type annotation:
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
(ann (box 1) (Boxof Fixnum))
((inst box Fixnum) 1)
]
@ -147,24 +146,22 @@ occur inside macros---are not checked.
Concretely, this means that expressions inside, for example, a
@racket[begin-for-syntax] block are not checked:
@examples[#:label #f #:eval the-eval
(eval:error (begin-for-syntax (+ 1 "foo")))
@interaction[#:eval the-eval
(begin-for-syntax (+ 1 "foo"))
]
Similarly, expressions inside of macros defined in Typed Racket are
not type-checked. On the other hand, the macro's expansion is always
type-checked:
@examples[#:label #f #:eval the-eval
(eval:no-prompt
(define-syntax (example-1 stx)
@defs+int[#:eval the-eval
((define-syntax (example-1 stx)
(+ 1 "foo")
#'1))
(eval:no-prompt
#'1)
(define-syntax (example-2 stx)
#'(+ 1 "foo")))
(eval:error (example-1))
(eval:error (example-2))
(example-1)
(example-2)
]
Note that functions defined in Typed Racket that are used at

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@begin[(require "../utils.rkt"
scribble/core scribble/example
scribble/core scribble/eval
(for-label (only-meta-in 0 typed/racket)
(prefix-in base: racket)))]
@ -127,8 +127,8 @@ This ensures that the expression, here @racket[(+ 7 1)], has the
desired type, here @racket[Number]. Otherwise, the type checker
signals an error. For example:
@examples[#:label #f #:eval the-eval
(eval:error (ann "not a number" Number))]
@interaction[#:eval the-eval
(ann "not a number" Number)]
@section{Type Inference}

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@begin[(require "../utils.rkt"
scribble/core scribble/example
scribble/core scribble/eval
(for-label (only-meta-in 0 typed/racket)))]
@(define the-eval (make-base-eval))
@ -18,7 +18,7 @@ fails.
To illustrate, consider the following code:
@examples[#:no-result #:eval the-eval
@racketblock+eval[#:eval the-eval
(: flexible-length (-> (U String (Listof Any)) Integer))
(define (flexible-length str-or-lst)
(if (string? str-or-lst)
@ -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 "propositions-and-predicates"]{Propositions and Predicates}
@section[#:tag "filters-and-predicates"]{Filters and Predicates}
In the previous section, we demonstrated that a Typed Racket programmer
can take advantage of occurrence typing to type-check functions
@ -59,30 +59,26 @@ 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 logical @deftech{propositions} that tell the typechecker what additional
with @deftech{filters} 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?]:
@examples[#:label #f #:eval the-eval string?]
@interaction[#:eval the-eval 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[_:], represents the logical @tech{propositions}
the typechecker learns from the result of applying the function:
the @racket[_:], is a @tech{filter} that tells the typechecker two
things:
@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]}
]
@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.
Predicates for all built-in types are annotated with similar filters
that allow the type system to reason about predicate checks.
@section{Other conditionals and assertions}
@ -97,7 +93,7 @@ control flow constructs that are present in Racket such as
For example, the @racket[_flexible-length] function from earlier can
be re-written to use @racket[cond] with no additional effort:
@examples[#:no-result #:eval the-eval
@racketblock+eval[#:eval the-eval
(: flexible-length/cond (-> (U String (Listof Any)) Integer))
(define (flexible-length/cond str-or-lst)
(cond [(string? str-or-lst) (string-length str-or-lst)]
@ -108,13 +104,13 @@ In some cases, the type system does not have enough information or is
too conservative to typecheck an expression. For example, consider
the following interaction:
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
(: a Positive-Integer)
(define a 15)
(: b Positive-Integer)
(define b 20)
(: c Positive-Integer)
(eval:error (define c (- b a)))
(define c (- b a))
]
In this case, the type system only knows that @racket[_a] and
@ -123,13 +119,13 @@ difference will always be positive in defining @racket[_c]. In cases
like this, occurrence typing can be used to make the code type-check
using an @emph{assertion}. For example,
@examples[#:no-result #:eval the-eval
@racketblock+eval[#:eval the-eval
(: d Positive-Integer)
(define d (assert (- b a) positive?))
]
Using the logical propositions on @racket[positive?], Typed Racket can
assign the type @racket[Positive-Integer] to the whole @racket[assert]
Using the filter 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].
@ -137,7 +133,7 @@ Note that @racket[assert] is a derived concept in Typed Racket and is
a natural consequence of occurrence typing. The assertion above is
essentially equivalent to the following:
@examples[#:no-result #:eval the-eval
@racketblock+eval[#:eval the-eval
(: e Positive-Integer)
(define e (let ([diff (- b a)])
(if (positive? diff)
@ -169,7 +165,7 @@ by let-expressions alias other values (e.g. when they alias non-mutated identifi
This allows programs which explicitly rely on occurrence typing and aliasing to
typecheck:
@examples[#:no-result #:eval the-eval
@racketblock+eval[#:eval the-eval
(: f (Any -> Number))
(define (f x)
(let ([y x])
@ -184,7 +180,7 @@ typecheck:
It also allows the typechecker to check programs which use macros
that heavily rely on let-bindings internally (such as @racket[match]):
@examples[#:no-result #:eval the-eval
@racketblock+eval[#:eval the-eval
(: g (Any -> Number))
(define (g x)
(match x

View File

@ -1,6 +1,7 @@
#lang scribble/manual
@begin[(require (for-label (only-meta-in 0 typed/racket))
scribble/eval racket/sandbox
"../utils.rkt" (only-in "quick.scrbl" typed-mod))]
@title[#:tag "optimization"]{Optimization in Typed Racket}
@ -29,9 +30,9 @@ Racket idioms. However, it does a better job on some idioms than on
others. By writing your programs using the right idioms, you can help
the optimizer help you.
To best take advantage of the Typed Racket optimizer, consult
@other-doc['(lib "optimization-coach/scribblings/optimization-coach.scrbl")
#:indirect "Optimization Coach"]{}.
To best take advantage of the Typed Racket optimizer, keep the following in
mind. The @emph{Optimization Coach} package provides optimization coaching
support to help you in this task.
@subsection{Numeric types}

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@(require "../utils.rkt"
scribble/example
scribble/eval
(for-label (only-meta-in 0 typed/racket)))
@(define the-eval (make-base-eval))
@ -49,7 +49,7 @@ typed/racket
[#:struct pt ([x : Real] [y : Real])]
[distance (-> pt pt Real)])
(distance (pt 3 5) (pt 7 0))
(distance (pt 3 5) (p 7 0))
]
The @racket[require/typed] form has several kinds of clauses. The
@ -100,17 +100,17 @@ function:
@margin-note{For general information on Racket's contract system
, see @secref[#:doc '(lib "scribblings/guide/guide.scrbl")]{contracts}.}
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
(module increment racket
(provide increment)
(code:contract increment : exact-integer? -> exact-integer?)
(code:contract "increment : exact-integer? -> exact-integer?")
(define (increment x) "this is broken"))
]
and a typed module that uses it:
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
(module client typed/racket
(require/typed 'increment [increment (-> Integer Integer)])
@ -127,7 +127,7 @@ strings.
On the other hand, when the program is run:
@examples[#:label #f #:eval the-eval (eval:error (require 'client))]
@interaction[#:eval the-eval (require 'client)]
we find that the contract system checks the assumption made by the typed
module and correctly finds that the assumption failed because of the

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@begin[(require "../utils.rkt"
scribble/core scribble/example
scribble/core scribble/eval
(for-label (only-meta-in 0 typed/racket)))]
@(define the-eval (make-base-eval))
@ -18,7 +18,7 @@ The most basic types in Typed Racket are those for primitive data,
such as @racket[True] and @racket[False] for booleans, @racket[String]
for strings, and @racket[Char] for characters.
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
'"hello, world"
#\f
#t
@ -27,14 +27,14 @@ for strings, and @racket[Char] for characters.
Each symbol is given a unique type containing only that symbol. The
@racket[Symbol] type includes all symbols.
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
'foo
'bar]
Typed Racket also provides a rich hierarchy for describing particular
kinds of numbers.
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
0
-7
14
@ -43,7 +43,7 @@ kinds of numbers.
Finally, any value is itself a type:
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
(ann 23 23)]
@section{Function Types}
@ -65,7 +65,7 @@ one argument, and produces @rtech{multiple values}, of types
@racket[String] and @racket[Natural]. Here are example functions for
each of these types.
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
(lambda ([x : Number]) x)
(lambda ([a : String] [b : String]) (equal? a b))
(lambda ([c : Char]) (values (string c) (char->integer c)))]
@ -106,7 +106,7 @@ The result is two values of type @racket[Number].
Sometimes a value can be one of several types. To specify this, we
can use a union type, written with the type constructor @racket[U].
@examples[#:label #f #:eval the-eval
@interaction[#:eval the-eval
(let ([a-number 37])
(if (even? a-number)
'yes
@ -141,9 +141,9 @@ type defintion could also be written like this.
Of course, types which directly refer to themselves are not
permitted. For example, both of these definitions are illegal.
@examples[#:label #f #:eval the-eval
(eval:error (define-type BinaryTree BinaryTree))
(eval:error (define-type BinaryTree (U Number BinaryTree)))]
@interaction[#:eval the-eval
(define-type BinaryTree BinaryTree)
(define-type BinaryTree (U Number BinaryTree))]
@section{Structure Types}

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 PropSet? Object?)))
(struct/c tc-results ((listof (struct/c tc-result (Type/c FilterSet? Object?)))
(or/c #f (cons/c Type/c symbol?))))
(struct/c tc-any-results (or/c Prop? #f))
(struct/c tc-any-results (or/c Filter/c NoFilter?))
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 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
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
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 proposition. This is useful in cases like
the Type or the Object, but we do store a filter. This is useful in cases like
(let ((x (read)))
(unless (number? x) (error 'bad-input))
(do-stuff x))

View File

@ -1,13 +1,8 @@
#lang scribble/manual
@begin[(require "../utils.rkt" scribble/example)
@begin[(require "../utils.rkt")
(require (for-label (only-meta-in 0 [except-in typed/racket for])))]
@(define the-top-eval (make-base-eval #:lang 'typed/racket))
@(define-syntax-rule (ex . args)
(examples #:eval the-top-eval . args))
@title{Experimental Features}
These features are currently experimental and subject to change.
@ -20,27 +15,3 @@ predicate @racket[id], which must have been specified with
@racket[declare-refinement].}
@defform[(define-typed-struct/exec forms ...)]{Defines an executable structure.}
@defform[(define-new-subtype name (constructor t))]{
Defines a new type @racket[name] that is a subtype of @racket[t].
The @racket[constructor] is defined as a function that takes a value of type
@racket[t] and produces a value of the new type @racket[name].
A @racket[define-new-subtype] definition is only allowed at the top level of a
file or module.
This is purely a type-level distinction, with no way to distinguish the new type
from the base type at runtime. Predicates made by @racket[make-predicate]
won't be able distinguish them properly, so they will return true for all values
that the base type's predicate would return true for. This is usually not what
you want, so you shouldn't use @racket[make-predicate] with these types.
@ex[(module m typed/racket
(provide Radians radians f)
(define-new-subtype Radians (radians Real))
(: f : [Radians -> Real])
(define (f a)
(sin a)))
(require 'm)
(radians 0)
(f (radians 0))]
}

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@begin[(require "../utils.rkt")
(require scribble/example)
(require scribble/eval)
(require (for-label (only-meta-in 0 [except-in typed/racket for])))]
@(define the-top-eval (make-base-eval))

View File

@ -1,7 +1,7 @@
#lang scribble/manual
@begin[(require "../utils.rkt")
(require scribble/example
(require scribble/eval
(for-label (only-meta-in 0 [except-in typed/racket for])))]
@(define the-eval (make-base-eval))

View File

@ -4,21 +4,14 @@
(require (for-label (only-meta-in 0 [except-in typed/racket for])
(only-in racket/base for)
racket/list srfi/14 net/url
version/check
;; Specific libraries wrapped for TR:
file/gif
net/http-client
net/url-structs
net/url
openssl
json))]
version/check))]
@title{Libraries Provided With Typed Racket}
The @racketmodname[typed/racket] language corresponds to the
@racketmodname[racket] language---that is, any identifier provided
by @racketmodname[racket], such as @racket[modulo], is available by default in
by @racketmodname[racket], such as @racket[modulo] is available by default in
@racketmodname[typed/racket].
@racketmod[typed/racket
@ -51,66 +44,25 @@ Other libraries can be used with Typed Racket via
The following libraries are included with Typed Racket in the
@racketfont{typed} collection:
@(define-syntax-rule @defmodule/incl[name rest ...]
(list
(section #:style '(hidden toc-hidden unnumbered)
(string-append "Typed for " (symbol->string 'name)))
@defmodule[name rest ...]))
@(define-syntax-rule @defmodule/incl[name]
@defmodule[name #:no-declare])
@(define-syntax-rule (deftype name . parts)
(defidform #:kind "type" name . parts))
@;; framework and mred left out until support for classes
@;; is more complete
@defmodule/incl[typed/file/gif]
@deftype[GIF-Stream]{
Describe a GIF stream, as produced by @racket[gif-start]
and accepted by the other functions from @racketmodname[file/gif].
}
@deftype[GIF-Colormap]{
Type alias for a list of three-element (R,G,B) vectors representing an image.
}
@defmodule/incl[typed/file/md5]
@defmodule/incl[typed/file/tar]
@defmodule/incl[typed/framework]
@defmodule/incl[typed/json]
@deftype[JSExpr]{
Describes a @tech["jsexpr" #:doc '(lib "json/json.scrbl")].
}
@defmodule/incl[typed/mred/mred]
@defmodule/incl[typed/net/base64]
@defmodule/incl[typed/net/cgi]
@defmodule/incl[typed/net/cookie]
@deftype[Cookie]{
Describes an HTTP cookie as implemented by @racketmodname[net/cookie].
}
@defmodule/incl[typed/net/dns]
@defmodule/incl[typed/net/ftp]
@deftype[FTP-Connection]{
Describes an open FTP connection.
}
@defmodule/incl[typed/net/gifwrite]
@defmodule/incl[typed/net/git-checkout]
@defmodule/incl[typed/net/head]
@defmodule/incl[typed/net/http-client]
@deftype[HTTP-Connection]{
Describes an HTTP connection, corresponding to @racket[http-conn?].
}
@defmodule/incl[typed/net/imap]
@deftype[IMAP-Connection]{
Describes an IMAP connection.
}
@defmodule/incl[typed/net/mime]
@defmodule/incl[typed/net/nntp]
@defmodule/incl[typed/net/pop3]
@ -121,61 +73,15 @@ The following libraries are included with Typed Racket in the
@defmodule/incl[typed/net/uri-codec]
@defmodule/incl[typed/net/url-connect]
@defmodule/incl[typed/net/url-structs]
@deftype[Path/Param]{
Describes the @racket[path/param] struct from @racketmodname[net/url-structs].
}
@deftype[URL]{
Describes an @racket[url] struct from @racketmodname[net/url-structs].
}
@defmodule/incl[typed/net/url]
In addition to defining the following types, this module also provides the
@racket[HTTP-Connection] type defined by @racketmodname[typed/net/http-client],
and the @racket[URL] and @racket[Path/Param] types from
@racketmodname[typed/net/url-structs].
@deftype[URL-Exception]{
Describes exceptions raised by URL-related functions; corresponds
to @racket[url-exception?].
}
@deftype[PortT]{
Describes the functions @racket[head-pure-port], @racket[delete-pure-port],
@racket[get-impure-port], @racket[head-impure-port], and
@racket[delete-impure-port].
}
@deftype[PortT/Bytes]{
Like @racket[PortT], but describes the functions that make POST and PUT
requests, which require an additional byte-string argument for POST or PUT
data.
}
@defmodule/incl[typed/openssl]
@deftype[SSL-Protocol]{
Describes an SSL protocol, defined as
@racket[(U 'auto 'sslv2-or-v3 'sslv2 'sslv3 'tls 'tls11 'tls12)].
}
@deftogether[(@deftype[SSL-Server-Context]
@deftype[SSL-Client-Context])]{
Describes an OpenSSL server or client context.
}
@deftype[SSL-Context]{Supertype of OpenSSL server and client contexts.}
@deftype[SSL-Listener]{
Describes an SSL listener, as produced by @racket[ssl-listen].
}
@deftype[SSL-Verify-Source]{
Describes a verification source usable by @racket[ssl-load-verify-source!]
and the @racket[ssl-default-verify-sources] parameter.
}
@defmodule/incl[typed/openssl/md5]
@defmodule/incl[typed/openssl/sha1]
@defmodule/incl[typed/racket/async-channel @history[#:added "1.1"]]
@defmodule/incl[typed/openssl]
@defmodule/incl[typed/pict]
@defmodule[typed/racket/async-channel #:no-declare @history[#:added "1.1"]]
@defmodule/incl[typed/racket/date]
@defmodule/incl[typed/racket/draw]
@defmodule/incl[typed/racket/gui]
@defmodule/incl[typed/racket/random @history[#:added "1.5"]]
@defmodule/incl[typed/racket/sandbox]
@defmodule/incl[typed/racket/snip]
@defmodule/incl[typed/racket/system]
@ -184,24 +90,8 @@ and the @racket[URL] and @racket[Path/Param] types from
@defmodule/incl[typed/rackunit/text-ui]
@defmodule/incl[typed/rackunit]
@defmodule/incl[typed/srfi/14]
@deftype[Char-Set]{
Describes a character set usable by the @racketmodname[srfi/14] functions.
}
@deftype[Cursor]{
Describes a cursor for iterating over character sets.
}
@defmodule/incl[typed/srfi/19]
@deftogether[(@defidform[#:kind "type" Time]
@defidform[#:kind "type" Date])]{
Describes an SRFI 19 time or date structure.
}
@defmodule/incl[typed/syntax/stx]
@defmodule/incl[typed/web-server/configuration/responders]
@defmodule/incl[typed/web-server/http]
In some cases, these typed adapters may not contain all of exports of the
original module, or their types may be more limited.
@ -213,11 +103,7 @@ written in Typed Racket or have adapter modules that are typed:
@defmodule[name #:no-declare #:link-target? #f #:indirect])
@defmodule/also[math]
@defmodule/also[plot]
@defmodule/incl[typed/pict]
@defmodule/also[images/flomap]
@defmodule/incl[typed/images/logos]
@defmodule/incl[typed/images/icons]
@defmodule/also[plot/typed]
@section{Porting Untyped Modules to Typed Racket}

View File

@ -1,6 +1,6 @@
#lang scribble/manual
@begin[(require "../utils.rkt" scribble/example racket/sandbox)
@begin[(require "../utils.rkt" scribble/eval racket/sandbox)
(require (for-label (only-meta-in 0 [except-in typed/racket])
(only-in racket/base)))]
@ -229,7 +229,12 @@ variants.
@defform[(for/hasheq type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/hasheqv type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/vector type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/flvector type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/extflvector type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/and type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/or type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/first type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/last type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/sum type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/product type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/set type-ann-maybe (for-clause ...) expr ...+)]
@ -255,16 +260,6 @@ type @racket[u]. For example, a @racket[for/list] form would be
annotated with a @racket[Listof] type. All annotations are optional.
}
@deftogether[[
@defform[(for/flvector type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/extflvector type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/and type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/first type-ann-maybe (for-clause ...) expr ...+)]
@defform[(for/last type-ann-maybe (for-clause ...) expr ...+)]
]]{
Like the above, except they are not yet supported by the typechecker.
}
@deftogether[[
@defform[(for/lists type-ann-maybe ([id : t] ...)
(for-clause ...)
@ -378,19 +373,14 @@ those functions.
@section{Structure Definitions}
@defform/subs[#:literals (:)
@defform/subs[
(struct maybe-type-vars name-spec ([f : t] ...) options ...)
([maybe-type-vars code:blank (v ...)]
[name-spec name-id (code:line name-id parent)]
[options #:transparent #:mutable #:prefab
(code:line #:constructor-name constructor-id)
(code:line #:extra-constructor-name constructor-id)
(code:line #:type-name type-id)])]{
Defines a @rtech{structure} with the name @racket[name-id], where the
[name-spec name (code:line name parent)]
[options #:transparent #:mutable #:prefab])]{
Defines a @rtech{structure} with the name @racket[name], where the
fields @racket[f] have types @racket[t], similar to the behavior of @|struct-id|
from @racketmodname[racket/base]. If @racket[type-id] is specified, then it will
be used for the name of the type associated with instances of the declared
structure, otherwise @racket[name-id] will be used for both.
from @racketmodname[racket/base].
When @racket[parent] is present, the
structure is a substructure of @racket[parent].
@ -407,47 +397,36 @@ amount it needs.
@ex[
(struct (X Y) 2-tuple ([first : X] [second : Y]))
(struct (X Y Z) 3-tuple 2-tuple ([third : Z]))
(struct (X Y Z) 3-tuple 2-tuple ([first : X] [second : Y] [third : Z]))
]
Options provided have the same meaning as for the @|struct-id| form
from @racketmodname[racket/base] (with the exception of @racket[#:type-name], as
described above).
from @racketmodname[racket/base].
A prefab structure type declaration will bind the given @racket[name-id]
or @racket[type-id] to a @racket[Prefab] type. Unlike the @|struct-id| form from
@racketmodname[racket/base], a non-prefab structure type cannot extend
a prefab structure type.
A prefab structure type declaration will bind the given @racket[name] to a
@racket[Prefab] type. Unlike in @racketmodname[racket/base], a non-prefab
structure type cannot extend a prefab structure type.
@ex[
(struct a-prefab ([x : String]) #:prefab)
(:type a-prefab)
(eval:error (struct not-allowed a-prefab ()))
(struct not-allowed a-prefab ())
]
@history[#:changed "1.4" @elem{Added the @racket[#:type-name] option.}]
}
@defform/subs[#:literals (:)
@defform/subs[
(define-struct maybe-type-vars name-spec ([f : t] ...) options ...)
([maybe-type-vars code:blank (v ...)]
[name-spec name-id (code:line name-id parent)]
[options #:transparent #:mutable
(code:line #:type-name type-id)])]{
Legacy version of @racket[struct], corresponding to @|define-struct-id|
from @racketmodname[racket/base].
@history[#:changed "1.4" @elem{Added the @racket[#:type-name] option.}]}
[name-spec name (name parent)]
[options #:transparent #:mutable])]{Legacy version of @racket[struct],
corresponding to @|define-struct-id| from @racketmodname[racket/base].}
@defform/subs[#:literals (:)
(define-struct/exec name-spec ([f : t] ...) [e : proc-t] maybe-type-name)
([name-spec name-id (code:line name-id parent)]
[maybe-type-name (code:line)
(code:line #:type-name type-id)])]{
@defform/subs[
(define-struct/exec name-spec ([f : t] ...) [e : proc-t])
([name-spec name (name parent)])]{
Like @racket[define-struct], but defines a procedural structure.
The procedure @racket[e] is used as the value for @racket[prop:procedure],
and must have type @racket[proc-t].
@history[#:changed "1.4" @elem{Added the @racket[#:type-name] option.}]}
The procdure @racket[e] is used as the value for @racket[prop:procedure], and must have type @racket[proc-t].}
@section{Names for Types}
@defform*[[(define-type name t maybe-omit-def)
@ -482,8 +461,27 @@ back to itself.
However, the recursive reference may not occur immediately inside
the type:
@ex[(eval:error (define-type Foo Foo))
(eval:error (define-type Bar (U Bar False)))]
@ex[(define-type Foo Foo)
(define-type Bar (U Bar False))]
}
@section{Defining New Subtypes}
@defform[(define-new-subtype name (constructor t))]{
Defines a new type @racket[name] that is a subtype of @racket[t].
The @racket[constructor] is defined as a function that takes a value of type
@racket[t] and produces a value of the new type @racket[name].
A @racket[define-new-subtype] definition is only allowed at the top level of a
file or module.
@ex[(module m typed/racket
(provide Radians radians f)
(define-new-subtype Radians (radians Real))
(: f : [Radians -> Real])
(define (f a)
(sin a)))
(require 'm)
(radians 0)
(f (radians 0))]
}
@section{Generating Predicates Automatically}
@ -540,19 +538,10 @@ returned by @racket[e], protected by a contract ensuring that it has type
@racket[t]. This is legal only in expression contexts.
@ex[(cast 3 Integer)
(eval:error (cast 3 String))
(cast (lambda ([x : Any]) x) (String -> String))
((cast (lambda ([x : Any]) x) (String -> String)) "hello")
(cast 3 String)
(cast (lambda: ([x : Any]) x) (String -> String))
]
The value is actually protected with two contracts. The second contract checks
the new type, but the first contract is put there to enforce the old type, to
protect higher-order uses of the value.
@ex[
((cast (lambda ([s : String]) s) (Any -> Any)) "hello")
(eval:error ((cast (lambda ([s : String]) s) (Any -> Any)) 5))
]}
}
@defform*[[(inst e t ...)
(inst e t ... t ooo bound)]]{
@ -583,12 +572,12 @@ Here, @racket[_m] is a module spec, @racket[_pred] is an identifier
naming a predicate, and @racket[_maybe-renamed] is an
optionally-renamed identifier.
@defform/subs[#:literals (struct :)
@defform/subs[#:literals (struct)
(require/typed m rt-clause ...)
([rt-clause [maybe-renamed t]
[#:struct name-id ([f : t] ...)
[#:struct name ([f : t] ...)
struct-option ...]
[#:struct (name-id parent) ([f : t] ...)
[#:struct (name parent) ([f : t] ...)
struct-option ...]
[#:opaque t pred]
[#:signature name ([id : t] ...)]]
@ -596,21 +585,21 @@ optionally-renamed identifier.
(orig-id new-id)]
[struct-option
(code:line #:constructor-name constructor-id)
(code:line #:extra-constructor-name constructor-id)
(code:line #:type-name type-id)])]
(code:line #:extra-constructor-name constructor-id)])]
This form requires identifiers from the module @racket[m], giving
them the specified types.
The first case requires @racket[_maybe-renamed], giving it type @racket[t].
The first case requires @racket[_maybe-renamed], giving it type
@racket[t].
@index["struct"]{The second and third cases} require the struct with name
@racket[name-id] and creates a new type with the name @racket[type-id], or
@racket[name-id] if no @racket[type-id] is provided, with fields @racket[f ...],
where each field has type @racket[t]. The third case allows a @racket[parent]
structure type to be specified. The parent type must already be a structure type
known to Typed Racket, either built-in or via @racket[require/typed]. The
structure predicate has the appropriate Typed Racket filter type so that it may
be used as a predicate in @racket[if] expressions in Typed Racket.
@index["struct"]{The second and third cases} require the struct with name @racket[name]
with fields @racket[f ...], where each field has type @racket[t]. The
third case allows a @racket[parent] structure type to be specified.
The parent type must already be a structure type known to Typed
Racket, either built-in or via @racket[require/typed]. The
structure predicate has the appropriate Typed Racket filter type so
that it may be used as a predicate in @racket[if] expressions in Typed
Racket.
@ex[(module UNTYPED racket/base
@ -669,9 +658,7 @@ a @racket[require/typed] form. Here is an example of using
Any])]))
@racket[file-or-directory-modify-seconds] has some arguments which are optional,
so we need to use @racket[case->].
@history[#:changed "1.4" @elem{Added the @racket[#:type-name] option.}]}
so we need to use @racket[case->].}
@defform[(require/typed/provide m rt-clause ...)]{
Similar to @racket[require/typed], but also provides the imported identifiers.
@ -716,7 +703,7 @@ but provides additional annotations to assist the typechecker.
(default-continuation-prompt-tag)
(code:comment "the function cannot be passed an argument")
(λ (f) (f 3))))
(eval:error (require 'untyped))
(require 'untyped)
]
}

View File

@ -1,6 +1,6 @@
#lang scribble/manual
@begin[(require "../utils.rkt" scribble/example racket/sandbox)
@begin[(require "../utils.rkt" scribble/eval racket/sandbox)
(require (for-label (only-meta-in 0 [except-in typed/racket for])))]
@(define the-eval (make-base-eval))
@ -127,10 +127,9 @@ additional provides all other bindings from @racketmodname[racket/class].
class form's clauses) are restricted.
@ex[
(eval:error
(class object%
(code:comment "Note the missing `super-new`")
(init-field [x : Real 0] [y : Real 0])))
(class object%
(code:comment "Note the missing `super-new`")
(init-field [x : Real 0] [y : Real 0]))
]
If any identifier with an optional type annotation is left without an

View File

@ -1,6 +1,6 @@
#lang scribble/manual
@begin[(require "../utils.rkt" scribble/example racket/sandbox)
@begin[(require "../utils.rkt" scribble/eval racket/sandbox)
(require (for-label (only-meta-in 0 [except-in typed/racket for])))]
@(define the-eval (make-base-eval))
@ -35,21 +35,19 @@ have the types ascribed to them; these types are converted to contracts and chec
@examples[#:eval the-eval
(with-type #:result Number 3)
(eval:error
((with-type #:result (Number -> Number)
(lambda: ([x : Number]) (add1 x)))
#f))
((with-type #:result (Number -> Number)
(lambda: ([x : Number]) (add1 x)))
#f)
(let ([x "hello"])
(with-type #:result String
#:freevars ([x String])
(string-append x ", world")))
(eval:error
(let ([x 'hello])
(with-type #:result String
#:freevars ([x String])
(string-append x ", world"))))
(let ([x 'hello])
(with-type #:result String
#:freevars ([x String])
(string-append x ", world")))
(with-type ([fun (Number -> Number)]
[val Number])

View File

@ -1,6 +1,6 @@
#lang scribble/manual
@begin[(require "../utils.rkt" scribble/example racket/sandbox)
@begin[(require "../utils.rkt" scribble/eval racket/sandbox)
(require (for-label (only-meta-in 0 [except-in typed/racket for]))
(for-label (only-in racket/unit tag unit/c)))]
@ -290,12 +290,11 @@ not present in the signature environment.
(define-signature a^ (a1))
(define-signature a-sub^ extends a^ (a2)))
(eval:error
(module TYPED-2 typed/racket
(require/typed 'UNTYPED-2
[#:signature a-sub^
([a1 : Integer]
[a2 : String])])))]
(module TYPED-2 typed/racket
(require/typed 'UNTYPED-2
[#:signature a-sub^
([a1 : Integer]
[a2 : String])]))]
Requiring a signature from an untyped module that contains variable definitions is an error
@ -306,12 +305,11 @@ in Typed Racket.
(provide bad^)
(define-signature bad^ (bad (define-values (bad-ref) (car bad)))))
(eval:error
(module TYPED typed/racket
(require/typed 'UNTYPED
[#:signature bad^
([bad : (Pairof Integer Integer)]
[bad-ref : Integer])])))]
(module TYPED typed/racket
(require/typed 'UNTYPED
[#:signature bad^
([bad : (Pairof Integer Integer)]
[bad-ref : Integer])]))]
@ -333,10 +331,9 @@ signature that contains definitions in a typed module will result in an error.
@ex[(module UNTYPED racket
(provide bad^)
(define-signature bad^ ((define-values (bad) 13))))
(eval:error
(module TYPED typed/racket
(require/typed 'UNTYPED
[#:signature bad^ ([bad : Integer])])))]
(module TYPED typed/racket
(require/typed 'UNTYPED
[#:signature bad^ ([bad : Integer])]))]
@subsection{Contracts and Unit Static Information}
Unit values that flow between typed and untyped contexts are wrapped in
@ -350,11 +347,10 @@ becoming inaccessible.
(module UNTYPED racket
(provide u@)
(define-unit u@ (import) (export) "Hello!"))
(eval:error
(module TYPED typed/racket
(require/typed 'UNTYPED
[u@ (Unit (import) (export) String)])
(invoke-unit/infer u@)))]
(module TYPED typed/racket
(require/typed 'UNTYPED
[u@ (Unit (import) (export) String)])
(invoke-unit/infer u@))]
When an identifier bound to static unit information flows from a typed module to
an untyped module, however, the situation is worse. Because unit static
@ -365,10 +361,9 @@ typed unit is disallowed in untyped contexts.
(module TYPED typed/racket
(provide u@)
(define-unit u@ (import) (export) "Hello!"))
(eval:error
(module UNTYPED racket
(require 'TYPED)
u@))]
(module UNTYPED racket
(require 'TYPED)
u@)]
@subsection{Signatures and Internal Definition Contexts}
Typed Racket's @racket[define-signature] form is allowed in both top-level and
@ -376,14 +371,13 @@ internal definition contexts. As the following example shows, defining
signatures in internal definiition contexts can be problematic.
@ex[
(eval:error
(module TYPED typed/racket
(define-signature a^ ())
(define u@
(let ()
(define-signature a^ ())
(unit (import a^) (export) (init-depend a^) 5)))
(invoke-unit u@ (import a^))))]
(module TYPED typed/racket
(define-signature a^ ())
(define u@
(let ()
(define-signature a^ ())
(unit (import a^) (export) (init-depend a^) 5)))
(invoke-unit u@ (import a^)))]
Even though the unit imports a signature named @racket[a^], the @racket[a^]
provided for the import refers to the top-level @racket[a^] signature and the

View File

@ -2,7 +2,7 @@
@begin[(require "../utils.rkt"
"numeric-tower-pict.rkt"
scribble/example
scribble/eval
racket/sandbox)
(require (for-label (only-meta-in 0 [except-in typed/racket for])
racket/async-channel))]
@ -372,10 +372,7 @@ corresponding to @racket[trest], where @racket[bound]
@defidform[FlVector]{An @rtech{flvector}.
@ex[(flvector 1.0 2.0 3.0)]}
@defidform[ExtFlVector]{An @rtech{extflvector}.
@ex[(eval:alts (extflvector 1.0t0 2.0t0 3.0t0)
(eval:result @racketresultfont{#<extflvector>}
"- : ExtFlVector"
""))]}
@ex[(extflvector 1.0t0 2.0t0 3.0t0)]}
@defidform[FxVector]{An @rtech{fxvector}.
@ex[(fxvector 1 2 3)]}
@ -402,11 +399,8 @@ corresponding to @racket[trest], where @racket[bound]
@ex[(lambda: ([x : Any]) (if (hash? x) x (error "not a hash table!")))]
}
@defform[(Setof t)]{is the type of a @rtech{hash set} of
@racket[t]. This includes custom hash sets, but not mutable hash set
or sets that are implemented using @racket[gen:set].
@defform[(Setof t)]{is the type of a @rtech{set} of @racket[t].
@ex[(set 0 1 2 3)]
@ex[(seteq 0 1 2 3)]
}
@defform[(Channelof t)]{A @rtech{channel} on which only @racket[t]s can be sent.
@ -568,33 +562,29 @@ functions and continuation mark functions.
@section{Other Type Constructors}
@defform*/subs[#:id -> #:literals (|@| * ... ! and or implies car cdr)
[(-> dom ... rng opt-proposition)
[(-> dom ... rng optional-filter)
(-> dom ... rest * rng)
(-> dom ... rest ooo bound rng)
(dom ... -> rng opt-proposition)
(dom ... -> rng optional-filter)
(dom ... rest * -> rng)
(dom ... rest ooo bound -> rng)]
([ooo #,(racket ...)]
[dom type
mandatory-kw
opt-kw]
optional-kw]
[mandatory-kw (code:line keyword type)]
[opt-kw [keyword type]]
[opt-proposition (code:line)
[optional-kw [keyword type]]
[optional-filter (code:line)
(code:line : type)
(code:line : pos-proposition
neg-proposition
object)]
[pos-proposition (code:line)
(code:line #:+ proposition ...)]
[neg-proposition (code:line)
(code:line #:- proposition ...)]
(code:line : pos-filter neg-filter object)]
[pos-filter (code:line)
(code:line #:+ proposition ...)]
[neg-filter (code:line)
(code:line #:- proposition ...)]
[object (code:line)
(code:line #:object index)]
[proposition Top
Bot
type
[proposition type
(! type)
(type |@| path-elem ... index)
(! type |@| path-elem ... index)
@ -608,15 +598,15 @@ functions and continuation mark functions.
The type of functions from the (possibly-empty)
sequence @racket[dom ....] to the @racket[rng] type.
@ex[(λ ([x : Number]) x)
(λ () 'hello)]
@ex[(λ: ([x : Number]) x)
: () 'hello)]
The second form specifies a uniform rest argument of type @racket[rest], and the
third form specifies a non-uniform rest argument of type
@racket[rest] with bound @racket[bound]. The bound refers to the type variable
that is in scope within the rest argument type.
@ex[(λ ([x : Number] . [y : String *]) (length y))
@ex[(λ: ([x : Number] . [y : String *]) (length y))
ormap]
In the third form, the @racket[...] introduced by @racket[ooo] is literal,
@ -633,24 +623,20 @@ functions and continuation mark functions.
(is-zero? 2 #:equality =)
(is-zero? 2 #:equality eq? #:zero 2.0)]
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
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
@racket[:], are necessary:
@ex[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].
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].
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:
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:
@ex[filter]
@ -661,7 +647,7 @@ functions and continuation mark functions.
Conversely, @racket[#:-] specifies that a function provides information for the
false branch of a conditional.
The other proposition cases are rarely needed, but the grammar documents them
The other filter 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[->]
@ -703,7 +689,7 @@ functions and continuation mark functions.
@ex[(: +all (->* (Integer) #:rest Integer (Listof Integer)))
(define (+all inc . rst)
(map (λ ([x : Integer]) (+ x inc)) rst))
(map (λ: ([x : Integer]) (+ x inc)) rst))
(+all 20 1 2 3)]
Both the mandatory and optional argument lists may contain keywords paired
@ -718,9 +704,9 @@ functions and continuation mark functions.
@deftogether[(
@defidform[Top]
@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.
@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.
}
@ -736,17 +722,13 @@ functions and continuation mark functions.
@ex[
(: my-list Procedure)
(define my-list list)
(eval:error (my-list "zwiebelkuchen" "socca"))
(my-list "zwiebelkuchen" "socca")
]
}
@defform[(U t ...)]{is the union of the types @racket[t ...].
@ex[(λ ([x : Real]) (if (> 0 x) "yes" 'no))]}
@defform[(∩ t ...)]{is the intersection of the types @racket[t ...].
@ex[((λ #:forall (A) ([x : (∩ Symbol A)]) x) 'foo)]}
@ex[(λ: ([x : Real])(if (> 0 x) "yes" 'no))]}
@defform[(case-> fun-ty ...)]{is a function that behaves like all of
the @racket[fun-ty]s, considered in order from first to last. The @racket[fun-ty]s must all be function
types constructed with @racket[->].

View File

@ -1,75 +0,0 @@
#lang scribble/manual
@(require scribble/example
(for-label (only-meta-in 0 [except-in typed/racket for])))
@(define eval (make-base-eval))
@(eval '(require typed/racket/base))
@title{Unsafe Typed Racket operations}
@defmodule[typed/racket/unsafe]
@bold{Warning}: the operations documented in this section are @emph{unsafe},
meaning that they can circumvent the invariants of the type system. Unless the
@racket[#:no-optimize] language option is used, this may result in unpredictable
behavior and may even crash Typed Racket.
@defform[(unsafe-require/typed m rt-clause ...)]{
This form requires identifiers from the module @racket[m] with the same
import specifications as @racket[require/typed].
Unlike @racket[require/typed], this form is unsafe and will not generate
contracts that correspond to the specified types to check that the values
actually match their types.
@examples[#:eval eval
(require typed/racket/unsafe)
(code:comment "import with a bad type")
(unsafe-require/typed racket/base [values (-> String Integer)])
(code:comment "unchecked call, the result type is wrong")
(values "foo")
]
@history[#:added "1.3"]
}
@defform[(unsafe-provide provide-spec ...)]{
This form declares exports from a module with the same syntax as
the @racket[provide] form.
Unlike @racket[provide], this form is unsafe and Typed Racket will not generate
any contracts that correspond to the specified types. This means that uses of the
exports in other modules may circumvent the type system's invariants.
Additionally, importing an identififer that is exported with
@racket[unsafe-provide] into another typed module, and then
re-exporting it with @racket[provide] will not cause contracts to be
generated.
Uses of the provided identifiers in other typed modules are not
affected by @racket[unsafe-provide]---in these situations it behaves
identically to @racket[provide]. Furthermore, other typed modules
that @emph{use} a binding that is in an @racket[unsafe-provide] will
still have contracts generated as usual.
@examples[#:eval eval
(module t typed/racket/base
(require typed/racket/unsafe)
(: f (-> Integer Integer))
(define (f x) (add1 x))
(code:comment "unsafe export, does not install checks")
(unsafe-provide f))
(module u racket/base
(require 't)
(code:comment "bad call that's unchecked")
(f "foo"))
(eval:error (require 'u))
]
@history[#:added "1.3"]
}
@close-eval[eval]

View File

@ -1,6 +1,6 @@
#lang scribble/manual
@begin[(require "../utils.rkt" scribble/example racket/sandbox)
@begin[(require "../utils.rkt" scribble/eval racket/sandbox)
(require (for-label (only-meta-in 0 [except-in typed/racket for])
typed/untyped-utils))]
@ -30,7 +30,7 @@ x
(define: y : (U String Symbol) "hello")
y
(assert y string?)
(eval:error (assert y boolean?))]
(assert y boolean?)]
@defform*/subs[[(with-asserts ([id maybe-pred] ...) body ...+)]
([maybe-pred code:blank
@ -64,11 +64,10 @@ the error message.
#`(cond clause ... [else (typecheck-fail #,stx "incomplete coverage"
#:covered-id x)])]))
(eval:error
(define: (f [x : (U String Integer)]) : Boolean
(cond* x
[(string? x) #t]
[(exact-nonnegative-integer? x) #f])))
(define: (f [x : (U String Integer)]) : Boolean
(cond* x
[(string? x) #t]
[(exact-nonnegative-integer? x) #f]))
]
}

View File

@ -35,7 +35,6 @@ For a friendly introduction, see the companion manual
@include-section["reference/no-check.scrbl"]
@include-section["reference/typed-regions.scrbl"]
@include-section["reference/optimization.scrbl"]
@include-section["reference/unsafe.scrbl"]
@include-section["reference/legacy.scrbl"]
@include-section["reference/compatibility-languages.scrbl"]
@include-section["reference/experimental.scrbl"]

View File

@ -2,7 +2,7 @@
(define collection 'multi)
(define deps '(("base" #:version "6.4.0.5")
(define deps '(("base" #:version "6.2.900.16")
"pconvert-lib"
"source-syntax"
"compatibility-lib" ;; to assign types
@ -12,4 +12,4 @@
(define pkg-authors '(samth stamourv))
(define version "1.5")
(define version "1.1")

View File

@ -1,24 +1,5 @@
6.5
- Added `simple-result->` to improve generated contract performance.
- Improve error message printing.
- Add `typed/racket/random`.
- Internal: populate type table unconditionally, for use in tooltips.
6.4
- Contract performance improvements, including generating code that
the contract system can optimize
- Make `any-wrap/c` more permissive on opaque structs.
- Soundly check opaque predicates.
- Add `#:type-name` option to `struct`.
6.3
(add1 6.2)
- Startup time reduction
- Tightening and cleanup of numeric types
- Sealing contracts for row polymorphic types
- `define-new-subtype`
- More robust compound pair operations optimizations
- Redesign of top-level support, using trampolining macros
- Static contract caching more conservative, causes contract generation slowdowns
- Experimental unit support
- `typed/racket/unsafe`, with `unsafe-require/typed` and `unsafe-provide`
6.2
- Use submodules to avoid allocating contract wrappers when not needed.
- Class types and contract generation are significantly improved, but still experimental.

File diff suppressed because it is too large Load Diff

View File

@ -17,7 +17,7 @@
racket/logging
racket/private/stx
(only-in mzscheme make-namespace)
(only-in racket/match/runtime match:error matchable? match-equality-test syntax-srclocs))
(only-in racket/match/runtime match:error matchable? match-equality-test))
"base-structs.rkt"
racket/file
(only-in racket/private/pre-base new-apply-proc)
@ -66,8 +66,8 @@
;; Section 4.2.2.7 (Random Numbers)
[random
(cl->* (->opt -Int -Int [-Pseudo-Random-Generator] -NonNegFixnum)
(->opt -Int [-Pseudo-Random-Generator] -NonNegFixnum)
(cl->* (->opt -PosFixnum [-Pseudo-Random-Generator] -NonNegFixnum)
(->opt -Int [-Pseudo-Random-Generator] -Nat)
(->opt [-Pseudo-Random-Generator] -Flonum))]
[random-seed (-> -PosInt -Void)]
@ -177,11 +177,6 @@
#:repeat? Univ #f
-String)]
[non-empty-string? (make-pred-ty -String)]
[string-contains? (-> -String -String -Boolean)]
[string-prefix? (-> -String -String -Boolean)]
[string-suffix? (-> -String -String -Boolean)]
;; Section 4.3.6 (racket/format)
[~a (->optkey []
#:rest Univ
@ -637,18 +632,15 @@
[memq (-poly (a) (-> Univ (-lst a) (-opt (-ne-lst a))))]
[memv (-poly (a) (-> Univ (-lst a) (-opt (-ne-lst a))))]
[memf (-poly (a) ((a . -> . Univ) (-lst a) . -> . (-opt (-ne-lst a))))]
[member (-poly (a b)
[member (-poly (a)
(cl->* (Univ (-lst a) . -> . (-opt (-ne-lst a)))
(b (-lst a) (-> b a Univ)
(Univ (-lst a) (-> a a Univ)
. -> . (-opt (-ne-lst a)))))]
[findf (-poly (a) ((a . -> . B) (-lst a) . -> . (-opt a)))]
[assq (-poly (a b) (Univ (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
[assv (-poly (a b) (Univ (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
[assoc (-poly (a b c)
(cl->* (Univ (-lst (-pair a b)) . -> . (-opt (-pair a b)))
(c (-lst (-pair a b)) (-> c a Univ)
. -> . (-opt (-pair a b)))))]
[assoc (-poly (a b) (Univ (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
[assf (-poly (a b) ((a . -> . Univ) (-lst (-pair a b))
. -> . (-opt (-pair a b))))]
@ -677,7 +669,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 (-PS (-is-type 0 b) -tt))
((asym-pred a Univ (-FS (-filter b 0) -top))
(-lst a)
. -> .
(-lst b))
@ -717,7 +709,7 @@
-Index))]
[partition
(-poly (a b) (cl->*
(-> (asym-pred b Univ (-PS (-is-type 0 a) -tt)) (-lst b) (-values (list (-lst a) (-lst b))))
(-> (asym-pred b Univ (-FS (-filter a 0) -top)) (-lst b) (-values (list (-lst a) (-lst b))))
(-> (-> a Univ) (-lst a) (-values (list (-lst a) (-lst a))))))]
[last (-poly (a) ((-lst a) . -> . a))]
@ -735,7 +727,7 @@
(-poly (a b)
(cl->*
(-> (-lst a)
(asym-pred a Univ (-PS (-is-type 0 b) -tt))
(asym-pred a Univ (-FS (-filter b 0) -top))
(-lst b))
(-> (-lst a) (-> a Univ) (-lst a))))]
[dropf (-poly (a) (-> (-lst a) (-> a Univ) (-lst a)))]
@ -743,14 +735,14 @@
(-poly (a b)
(cl->*
(-> (-lst a)
(asym-pred a Univ (-PS (-is-type 0 b) -tt))
(asym-pred a Univ (-FS (-filter b 0) -top))
(-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 (-PS (-is-type 0 b) -tt))
(asym-pred a Univ (-FS (-filter b 0) -top))
(-lst b))
(-> (-lst a) (-> a Univ) (-lst a))))]
[dropf-right (-poly (a) (-> (-lst a) (-> a Univ) (-lst a)))]
@ -758,7 +750,7 @@
(-poly (a b)
(cl->*
(-> (-lst a)
(asym-pred a Univ (-PS (-is-type 0 b) -tt))
(asym-pred a Univ (-FS (-filter b 0) -top))
(-values (list (-lst a) (-lst b))))
(-> (-lst a) (-> a Univ) (-values (list (-lst a) (-lst a))))))]
@ -776,14 +768,6 @@
((-lst b) b) . ->... .(-lst c)))]
[append*
(-poly (a) ((-lst (-lst a)) . -> . (-lst a)))]
[flatten
(Univ . -> . (-lst Univ))]
[combinations (-poly (a) (cl->*
(-> (-lst a) (-lst (-lst a)))
(-> (-lst a) -Nat (-lst (-lst a)))))]
[in-combinations (-poly (a) (cl->*
(-> (-lst a) (-seq (-lst a)))
(-> (-lst a) -Nat (-seq (-lst a)))))]
[permutations (-poly (a) (-> (-lst a) (-lst (-lst a))))]
[in-permutations (-poly (a) (-> (-lst a) (-seq (-lst a))))]
[argmin (-poly (a) ((a . -> . -Real) (-lst a) . -> . a))]
@ -853,7 +837,7 @@
. ->... .
-Index))]
[vector-filter (-poly (a b) (cl->*
((asym-pred a Univ (-PS (-is-type 0 b) -tt))
((asym-pred a Univ (-FS (-filter b 0) -top))
(-vec a)
. -> .
(-vec b))
@ -887,7 +871,6 @@
((-box a) . -> . a)
((make-BoxTop) . -> . Univ)))]
[set-box! (-poly (a) ((-box a) a . -> . -Void))]
[box-cas! (-poly (a) ((-box a) a a . -> . -Boolean))]
[unsafe-unbox (-poly (a) (cl->*
((-box a) . -> . a)
((make-BoxTop) . -> . Univ)))]
@ -896,7 +879,6 @@
((-box a) . -> . a)
((make-BoxTop) . -> . Univ)))]
[unsafe-set-box*! (-poly (a) ((-box a) a . -> . -Void))]
[unsafe-box*-cas! (-poly (a) ((-box a) a a . -> . -Boolean))]
[box? (make-pred-ty (make-BoxTop))]
;; Section 4.13 (Hash Tables)
@ -970,25 +952,13 @@
[equal-hash-code (-> Univ -Fixnum)]
[equal-secondary-hash-code (-> Univ -Fixnum)]
[hash-iterate-first (-poly (a b)
(cl->*
((-HT a b) . -> . (Un (-val #f) -Integer))
(-> -HashTop (Un (-val #f) -Integer))))]
((-HT a b) . -> . (Un (-val #f) -Integer)))]
[hash-iterate-next (-poly (a b)
(cl->*
((-HT a b) -Integer . -> . (Un (-val #f) -Integer))
(-> -HashTop -Integer (Un (-val #f) -Integer))))]
((-HT a b) -Integer . -> . (Un (-val #f) -Integer)))]
[hash-iterate-key (-poly (a b)
(cl->* ((-HT a b) -Integer . -> . a)
(-> -HashTop -Integer Univ)))]
((-HT a b) -Integer . -> . a))]
[hash-iterate-value (-poly (a b)
(cl->* ((-HT a b) -Integer . -> . b)
(-> -HashTop -Integer Univ)))]
[hash-iterate-pair (-poly (a b)
(cl->* ((-HT a b) -Integer . -> . (-pair a b))
(-> -HashTop -Integer Univ)))]
[hash-iterate-key+value (-poly (a b)
(cl->* ((-HT a b) -Integer . -> . (-values (list a b)))
(-> -HashTop -Integer (-values (list Univ Univ)))))]
((-HT a b) -Integer . -> . b))]
[make-custom-hash (->opt (-> Univ Univ Univ) (-> Univ -Nat) [(-> Univ -Nat)] Univ)]
[make-immutable-custom-hash (->opt (-> Univ Univ Univ) (-> Univ -Nat) [(-> Univ -Nat)] Univ)]
@ -1041,7 +1011,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 (-PS (-is-type 0 b) -tt))
((asym-pred a Univ (-FS (-filter b 0) -top))
(-seq a)
. -> .
(-seq b))
@ -1071,7 +1041,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 (-PS -tt (-not-type 0 (-set Univ))))]
[generic-set? (asym-pred Univ B (-FS -top (-not-filter (-set Univ) 0)))]
[set? (make-pred-ty (-set Univ))]
[set-equal? (-poly (e) (-> (-set e) B))]
[set-eqv? (-poly (e) (-> (-set e) B))]
@ -1110,14 +1080,14 @@
[identity (-poly (a) (->acc (list a) a null))]
[const (-poly (a) (-> a (->* '() Univ a)))]
[negate (-polydots (a b c d)
(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))))
(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))))
(-> ((list) [d d] . ->... . Univ)
((list) [d d] . ->... . -Boolean))))]
[conjoin (-polydots (a) (->* '() (->... '() (a a) Univ) (->... '() (a a) Univ)))]
@ -1200,7 +1170,6 @@
;[match:error (Univ . -> . (Un))]
[match-equality-test (-Param (Univ Univ . -> . Univ) (Univ Univ . -> . Univ))]
[matchable? (make-pred-ty (Un -String -Bytes))]
[syntax-srclocs (Univ . -> . Univ)]
;; Section 10.1
[values (-polydots (a b) (cl->*
@ -1303,7 +1272,7 @@
[call-with-continuation-barrier (-poly (a) (-> (-> a) a))]
[continuation-prompt-available? (-> (make-Prompt-TagTop) B)]
[continuation?
(asym-pred Univ B (-PS (-is-type 0 top-func) -tt))]
(asym-pred Univ B (-FS (-filter top-func 0) -top))]
[continuation-prompt-tag? (make-pred-ty (make-Prompt-TagTop))]
[dynamic-wind (-poly (a) (-> (-> ManyUniv) (-> a) (-> ManyUniv) a))]
@ -1424,7 +1393,7 @@
[never-evt (-evt (Un))]
[system-idle-evt (-> (-evt -Void))]
[alarm-evt (-> -Real (-mu x (-evt x)))]
[handle-evt? (asym-pred Univ B (-PS (-is-type 0 (-evt Univ)) -tt))]
[handle-evt? (asym-pred Univ B (-FS (-filter (-evt Univ) 0) -top))]
[current-evt-pseudo-random-generator
(-Param -Pseudo-Random-Generator -Pseudo-Random-Generator)]
@ -1435,7 +1404,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 (-PS (-is-type 0 (-mu x (-evt x))) -tt))]
[channel-put-evt? (asym-pred Univ B (-FS (-filter (-mu x (-evt x)) 0) -top))]
;; Section 11.2.3 (Semaphores)
[semaphore? (make-pred-ty -Semaphore)]
@ -1445,7 +1414,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 (-PS (-is-type 0 (-mu x (-evt x))) -tt))]
[semaphore-peek-evt? (asym-pred Univ B (-FS (-filter (-mu x (-evt x)) 0) -top))]
[call-with-semaphore
(-polydots (b a)
(cl->* (->... (list -Semaphore (->... '() [a a] b))
@ -1541,10 +1510,7 @@
[syntax-original? (-poly (a) (-> (-Syntax a) B))]
[syntax-source-module (->opt (-Syntax Univ) [Univ] (Un (-val #f) -Path Sym -Module-Path-Index))]
[syntax-e (-poly (a) (->acc (list (-Syntax a)) a (list -syntax-e)))]
[syntax->list (-poly (a)
(cl->* (-> (-Syntax (-lst a)) (-lst a))
(-> (-Syntax Univ)
(Un (-val #f) (-lst (-Syntax Univ))))))]
[syntax->list (-poly (a) (-> (-Syntax (-lst a)) (-lst a)))]
[syntax->datum (cl->* (-> Any-Syntax -Sexp)
(-> (-Syntax Univ) Univ))]
@ -1790,7 +1756,7 @@
[file-stream-buffer-mode (cl-> [(-Port) (one-of/c 'none 'line 'block #f)]
[(-Port (one-of/c 'none 'line 'block)) -Void])]
[file-position (cl-> [(-Port) -Nat]
[(-Port (Un -Integer (-val eof))) -Void])]
[(-Port -Integer) -Void])]
[file-position* (-> -Port (Un -Nat (-val #f)))]
;; Section 13.1.4
@ -1849,8 +1815,8 @@
[port-file-identity (-> (Un -Input-Port -Output-Port) -PosInt)]
;; Section 13.1.6
[open-input-string (->opt -String [Univ] -Input-Port)]
[open-input-bytes (->opt -Bytes [Univ] -Input-Port)]
[open-input-string (-> -String -Input-Port)]
[open-input-bytes (-> -Bytes -Input-Port)]
[open-output-string
([Univ] . ->opt . -Output-Port)]
[open-output-bytes
@ -1863,7 +1829,7 @@
;; Section 13.1.7
[make-pipe
(cl->* [->opt [N Univ Univ] (-values (list -Input-Port -Output-Port))])]
(cl->* [->opt [N] (-values (list -Input-Port -Output-Port))])]
[pipe-content-length (-> (Un -Input-Port -Output-Port) -Nat)]
;; Section 13.1.8
@ -1965,10 +1931,8 @@
[make-pipe-with-specials (->opt [-Nat Univ Univ] (-values (list -Input-Port -Output-Port)))]
[merge-input (->opt -Input-Port -Input-Port [(-opt -Nat)] -Input-Port)]
[open-output-nowhere (->opt [Univ Univ] -Output-Port)]
[peeking-input-port (->optkey -Input-Port [Univ -Nat]
#:init-position -Nat #f
-Input-Port)]
[open-output-nowhere (-> -Output-Port)]
[peeking-input-port (->opt -Input-Port [Univ -Nat] -Input-Port)]
[reencode-input-port
(->opt -Input-Port -String (-opt -Bytes) [Univ Univ Univ (-> -String -Input-Port ManyUniv)] -Input-Port)]
@ -1976,7 +1940,7 @@
(->opt -Output-Port -String (-opt -Bytes) [Univ Univ (-opt -Bytes) (-> -String -Output-Port ManyUniv)] -Output-Port)]
[dup-input-port (-Input-Port (B) . ->opt . -Input-Port)]
[dup-output-port (-Output-Port (B) . ->opt . -Output-Port)]
[dup-output-port (-Output-Port (B) . ->opt . -Input-Port)]
[relocate-input-port (->opt -Input-Port (-opt -PosInt) (-opt -Nat) -PosInt [Univ] -Input-Port)]
[relocate-output-port (->opt -Output-Port (-opt -PosInt) (-opt -Nat) -PosInt [Univ] -Output-Port)]
@ -2316,7 +2280,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 (-PS (-is-type 0 -Module-Path) -tt))]
[module-path? (asym-pred Univ B (-FS (-filter -Module-Path 0) -top))]
[current-module-name-resolver (-Param (cl->* (-Resolved-Module-Path Univ . -> . Univ)
((Un -Module-Path -Path)
@ -2500,8 +2464,8 @@
;; Section 15.1 (Path Manipulation)
[path? (make-pred-ty -Path)]
[path-string? (asym-pred Univ B
(-PS (-is-type 0 (Un -Path -String))
(-not-type 0 -Path)))]
(-FS (-filter (Un -Path -String) 0)
(-not-filter -Path 0)))]
[path-for-some-system? (make-pred-ty -SomeSystemPath)]
[string->path (-> -String -Path)]
@ -2566,16 +2530,6 @@
(Un -SomeSystemPath (one-of/c 'up 'same))
B))))]
[path-replace-extension
(cl->*
(-> -Pathlike (Un -String -Bytes) -Path)
(-> -SomeSystemPathlike (Un -String -Bytes) -SomeSystemPath))]
[path-add-extension
(cl->*
(-> -Pathlike (Un -String -Bytes) -Path)
(-> -SomeSystemPathlike (Un -String -Bytes) -SomeSystemPath))]
[path-replace-suffix
(cl->*
(-> -Pathlike (Un -String -Bytes) -Path)
@ -2650,14 +2604,8 @@
-Void)]
[delete-directory/files (->key -Pathlike #:must-exist? Univ #f -Void)]
[find-files (->optkey (-> -Path Univ) [(-opt -Pathlike)]
#:skip-filtered-directories? Univ #f
#:follow-links? Univ #f
(-lst -Path))]
[pathlist-closure (->key (-lst -Pathlike)
#:path-filter (Un (-val #f) (-Path . -> . Univ)) #f
#:follow-links? Univ #f
(-lst -Path))]
[find-files (->optkey (-> -Path Univ) [(-opt -Pathlike)] #:follow-links? Univ #f (-lst -Path))]
[pathlist-closure (->key (-lst -Pathlike) #:follow-links? Univ #f (-lst -Path))]
[fold-files
(-poly
@ -2701,10 +2649,10 @@
[tcp-abandon-port (-Port . -> . -Void)]
[tcp-addresses (cl->*
((Un -TCP-Listener -Port) [(-val #f)] . ->opt . (-values (list -String -String)))
((Un -TCP-Listener -Port) (-val #t) . -> . (-values (list -String -Index -String -Index))))]
(-Port [(-val #f)] . ->opt . (-values (list -String -String)))
(-Port (-val #t) . -> . (-values (list -String -Index -String -Index))))]
[tcp-port? (asym-pred Univ B (-PS (-is-type 0 (Un -Input-Port -Output-Port)) -tt))]
[tcp-port? (asym-pred Univ B (-FS (-filter (Un -Input-Port -Output-Port) 0) -top))]
;; Section 15.3.2 (racket/udp)
[udp-open-socket (->opt [(-opt -String) (-opt -String)] -UDP-Socket)]
@ -2970,7 +2918,6 @@
;; Section 15.8
[system-type
(cl->*
(-> (Un (-val 'unix) (-val 'windows) (-val 'macosx)))
(-> (-val 'os) (Un (-val 'unix) (-val 'windows) (-val 'macosx)))
(-> (-val 'gc) (Un (-val 'cgc) (-val '3m)))
(-> (-val 'link) (Un (-val 'static) (-val 'shared) (-val 'dll) (-val 'framework)))
@ -3020,9 +2967,7 @@
[will-try-execute (-> -Will-Executor ManyUniv)]
;; Section 16.4
[collect-garbage (cl->*
(-> -Void)
(-> (Un (-val 'minor) (-val 'major) (-val 'incremental)) -Void))]
[collect-garbage (-> -Void)]
[current-memory-use (-> -Nat)]
[dump-memory-stats (-> Univ)]
@ -3063,7 +3008,7 @@
[assert (-poly (a b) (cl->*
(Univ (make-pred-ty (list a) Univ b) . -> . b)
(-> (Un a (-val #f)) a)))]
[defined? (->* (list Univ) -Boolean : (-PS (-not-type 0 -Undefined) (-is-type 0 -Undefined)))]
[defined? (->* (list Univ) -Boolean : (-FS (-not-filter -Undefined 0) (-filter -Undefined 0)))]
;; Syntax Manual
;; Section 2.1 (syntax/stx)

View File

@ -46,10 +46,6 @@
(cl->*
(-> (-lst a) -Null (-lst a))
(-> (-lst a) (-lst b) (-lst (Un a b)))))]
;; normalise-inputs
[(make-template-identifier 'normalise-inputs 'racket/private/for)
(-poly (a)
(-> -Symbol -String (-> a -Boolean) (-> a -Nat) a -Nat (Un (-val #f) -Nat) -Nat (-values (list a -Index -Index -Index))))]
;; make-sequence
[(make-template-identifier 'make-sequence 'racket/private/for)
(-poly (a b)
@ -116,75 +112,25 @@
[(make-template-identifier 'in-bytes 'racket/private/for)
(->opt -Bytes [-Int (-opt -Int) -Int] (-seq -Byte))]
;; in-hash and friends
[(make-template-identifier 'default-in-hash 'racket/private/for)
[(make-template-identifier 'in-hash 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a b)]
[(-HashTop) (-seq Univ Univ)]))]
[(make-template-identifier 'default-in-hash-keys 'racket/private/for)
[(make-template-identifier 'in-hash-keys 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a)]
[(-HashTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-hash-values 'racket/private/for)
[(make-template-identifier 'in-hash-values 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq b)]
[(-HashTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-hash-pairs 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq (-pair a b))]
[(-HashTop) (-seq (-pair Univ Univ))]))]
[(make-template-identifier 'default-in-immutable-hash 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a b)]
[(-HashTop) (-seq Univ Univ)]))]
[(make-template-identifier 'default-in-immutable-hash-keys 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a)]
[(-HashTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-immutable-hash-values 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq b)]
[(-HashTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-immutable-hash-pairs 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq (-pair a b))]
[(-HashTop) (-seq (-pair Univ Univ))]))]
[(make-template-identifier 'default-in-mutable-hash 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a b)]
[(-HashTop) (-seq Univ Univ)]))]
[(make-template-identifier 'default-in-mutable-hash-keys 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a)]
[(-HashTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-mutable-hash-values 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq b)]
[(-HashTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-mutable-hash-pairs 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq (-pair a b))]
[(-HashTop) (-seq (-pair Univ Univ))]))]
[(make-template-identifier 'default-in-weak-hash 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a b)]
[(-HashTop) (-seq Univ Univ)]))]
[(make-template-identifier 'default-in-weak-hash-keys 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq a)]
[(-HashTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-weak-hash-values 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq b)]
[(-HashTop) (-seq Univ)]))]
[(make-template-identifier 'default-in-weak-hash-pairs 'racket/private/for)
[(make-template-identifier 'in-hash-pairs 'racket/private/for)
(-poly (a b)
(cl-> [((-HT a b)) (-seq (-pair a b))]
[(-HashTop) (-seq (-pair Univ Univ))]))]
;; in-port
[(make-template-identifier 'in-port 'racket/private/for)
(-poly (a)
(cl->* (-> (-seq Univ))
(->opt (-> -Input-Port (Un a (-val eof))) [-Input-Port] (-seq a))))]
(->opt [(-> -Input-Port Univ) -Input-Port] (-seq Univ))]
;; in-input-port-bytes
[(make-template-identifier 'in-input-port-bytes 'racket/private/for)
(-> -Input-Port (-seq -Byte))]

View File

@ -70,10 +70,7 @@
([message : -String] [continuation-marks : -Cont-Mark-Set])
(define-hierarchy exn:break (#:kernel-maker k:exn:break)
([continuation : top-func])
(define-hierarchy exn:break:hang-up (#:kernel-maker k:exn:break:hang-up) ())
(define-hierarchy exn:break:terminate (#:kernel-maker k:exn:break:terminate) ()))
([continuation : top-func]))
(define-hierarchy exn:fail (#:kernel-maker k:exn:fail) ()
@ -84,10 +81,7 @@
(define-hierarchy exn:fail:contract:continuation (#:kernel-maker k:exn:fail:contract:continuation) ())
(define-hierarchy exn:fail:contract:variable (#:kernel-maker k:exn:fail:contract:variable) ()))
(define-hierarchy exn:fail:syntax (#:kernel-maker k:exn:fail:syntax) ([exprs : (-lst Any-Syntax)])
(define-hierarchy exn:fail:syntax:unbound (#:kernel-maker k:exn:fail:syntax:unbound) ())
(define-hierarchy exn:fail:syntax:missing-module (#:kernel-maker k:exn:fail:syntax:missing-module)
([path : -Module-Path])))
(define-hierarchy exn:fail:syntax (#:kernel-maker k:exn:fail:syntax) ([exprs : (-lst Any-Syntax)]))
(define-hierarchy exn:fail:read (#:kernel-maker k:exn:fail:read)
([srclocs : (-lst Univ)]) ;; cce: Univ here should be srcloc
@ -96,15 +90,9 @@
(define-hierarchy exn:fail:filesystem (#:kernel-maker k:exn:fail:filesystem) ()
(define-hierarchy exn:fail:filesystem:exists (#:kernel-maker k:exn:fail:filesystem:exists) ())
(define-hierarchy exn:fail:filesystem:version (#:kernel-maker k:exn:fail:filesystem:version) ())
(define-hierarchy exn:fail:filesystem:errno (#:kernel-maker k:exn:fail:filesystem:errno)
([errno : (-pair -Integer (one-of/c 'posix 'windows 'gai))]))
(define-hierarchy exn:fail:filesystem:missing-module (#:kernel-maker k:exn:fail:filesystem:missing-module)
([path : -Module-Path])))
(define-hierarchy exn:fail:filesystem:version (#:kernel-maker k:exn:fail:filesystem:version) ()))
(define-hierarchy exn:fail:network (#:kernel-maker k:exn:fail:network) ()
(define-hierarchy exn:fail:network:errno (#:kernel-maker k:exn:fail:network:errno)
([errno : (-pair -Integer (one-of/c 'posix 'windows 'gai))])))
(define-hierarchy exn:fail:network (#:kernel-maker k:exn:fail:network) ())
(define-hierarchy exn:fail:out-of-memory (#:kernel-maker k:exn:fail:out-of-memory) ())

View File

@ -7,12 +7,7 @@
[(_ nm ...)
#'(begin (define-syntax nm
(lambda (stx)
(raise-syntax-error 'type-check
(format "type name used out of context\n type: ~a\n in: ~a"
(syntax->datum (if (stx-pair? stx)
(stx-car stx)
stx))
(syntax->datum stx))
(raise-syntax-error 'type-check "type name used out of context"
stx
(and (stx-pair? stx) (stx-car stx)))))
...
@ -22,8 +17,7 @@
(define-other-types
-> ->* case-> U Rec All Opaque Vector
Parameterof List List* Class Object Unit Values AnyValues Instance Refinement
pred Struct Struct-Type Prefab Top Bot Distinction Sequenceof
)
pred Struct Struct-Type Prefab Top Bot Distinction)
(provide (rename-out [All ]
[U Un]
@ -32,3 +26,4 @@
[List Tuple]
[Rec mu]
[Parameterof Parameter]))

View File

@ -187,6 +187,7 @@
[Pairof (-poly (a b) (-pair a b))]
[MPairof (-poly (a b) (-mpair a b))]
[MListof (-poly (a) (-mlst a))]
[Sequenceof (-poly (a) (-seq a))]
[Thread-Cellof (-poly (a) (-thread-cell a))]
[Custodian-Boxof (-poly (a) (make-CustodianBox a))]

View File

@ -282,7 +282,7 @@
[_ #f]))
;; clauses->names : (-> Clause Boolean) Listof<Clause> -> Listof<Id>
;; prop clauses by some property and spit out the names in those clauses
;; filter 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)]

View File

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

View File

@ -11,7 +11,7 @@
(for-syntax racket/base
syntax/parse
syntax/stx)
(for-syntax (types abbrev numeric-tower union prop-ops)))
(for-syntax (types abbrev numeric-tower union filter-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 prop-ops)))
(for-syntax (types-out abbrev numeric-tower union filter-ops)))
;; syntax classes for type clauses in the type-environment macro
(begin-for-syntax
@ -52,11 +52,7 @@
;; lift out to utility module maybe
(define-syntax (type stx)
(raise-syntax-error 'type-check
(format "type name used out of context\n type: ~a\n in: ~a"
(syntax->datum (if (stx-pair? stx)
(stx-car stx)
stx))
(syntax->datum stx))
"type name used out of context"
stx
(and (stx-pair? stx) (stx-car stx))))
(provide type pred))))

View File

@ -19,7 +19,7 @@
(provide require/opaque-type require-typed-struct-legacy require-typed-struct
require/typed-legacy require/typed require/typed/provide
require-typed-struct/provide core-cast make-predicate define-predicate
require-typed-struct/provide cast make-predicate define-predicate
require-typed-signature)
(module forms racket/base
@ -31,7 +31,7 @@
require-typed-struct-legacy
require-typed-struct
require/typed-legacy require/typed require/typed/provide
require-typed-struct/provide core-cast make-predicate define-predicate)]))
require-typed-struct/provide cast make-predicate define-predicate)]))
(define-syntax (def stx)
(syntax-case stx ()
[(_ id ...)
@ -43,25 +43,7 @@
require-typed-struct-legacy
require-typed-struct
require/typed-legacy require/typed require/typed/provide
require-typed-struct/provide make-predicate define-predicate)
;; Expand `cast` to a `core-cast` with an extra `#%expression` in order
;; to prevent the contract generation pass from executing too early
;; (i.e., before the `cast` typechecks)
(define-syntax (-core-cast stx) (core-cast stx))
(define-syntax (cast stx)
(syntax-case stx ()
[(_ e ty) (quasisyntax/loc stx (#%expression #,(syntax/loc stx (-core-cast e ty))))]))
(provide cast))
;; unsafe operations go in this submodule
(module* unsafe #f
;; turned into a macro on the requiring side
(provide -unsafe-require/typed))
;; used for private unsafe functionality in require macros
;; *do not export*
(define-syntax unsafe-kw (syntax-rules ()))
require-typed-struct/provide cast make-predicate define-predicate))
(require (for-template (submod "." forms) "../utils/require-contract.rkt"
(submod "../typecheck/internal-forms.rkt" forms)
@ -81,10 +63,8 @@
racket/struct-info
syntax/struct
syntax/location
(for-template "../utils/any-wrap.rkt")
"../utils/tc-utils.rkt"
"../private/syntax-properties.rkt"
"../private/cast-table.rkt"
"../typecheck/internal-forms.rkt"
;; struct-extraction is actually used at both of these phases
"../utils/struct-extraction.rkt"
@ -94,9 +74,11 @@
;; Lazily loaded b/c they're only used sometimes, so we save a lot
;; of loading by not having them when they are unneeded
(lazy-require ["../rep/type-rep.rkt" (Error?)]
(lazy-require ["../rep/type-rep.rkt" (make-Opaque Error?)]
["../types/utils.rkt" (fv)]
[typed-racket/private/parse-type (parse-type)])
[syntax/define (normalize-definition)]
[typed-racket/private/parse-type (parse-type)]
[typed-racket/env/type-alias-env (register-resolved-type-alias)])
(define (with-type* expr ty)
(with-type #`(ann #,expr #,ty)))
@ -110,12 +92,11 @@
(pattern (nm:id parent:id)))
(define-values (require/typed-legacy require/typed -unsafe-require/typed)
(define-values (require/typed-legacy require/typed)
(let ()
(define-syntax-class opt-rename
#:attributes (nm orig-nm spec)
#:attributes (nm spec)
(pattern nm:id
#:with orig-nm #'nm
#:with spec #'nm)
(pattern (orig-nm:id internal-nm:id)
#:with spec #'(orig-nm internal-nm)
@ -125,24 +106,23 @@
#:attributes (nm ty)
(pattern [nm:opt-rename ty]))
(define-splicing-syntax-class (struct-opts legacy struct-name)
#:attributes (ctor-value type)
(pattern (~seq (~optional (~seq (~and key (~or #:extra-constructor-name #:constructor-name))
name:id))
(~optional (~seq #:type-name type:id) #:defaults ([type struct-name])))
#:attr ctor-value (if (attribute key) #'(key name)
(if legacy
#`(#:extra-constructor-name
#,(format-id struct-name "make-~a" struct-name))
#'()))))
(define-splicing-syntax-class (opt-constructor legacy struct-name)
#:attributes (value)
(pattern (~seq)
#:attr value (if legacy
#`(#:extra-constructor-name
#,(format-id struct-name "make-~a" struct-name))
#'()))
(pattern (~seq (~and key (~or #:extra-constructor-name #:constructor-name)) name:id)
#:attr value #'(key name)))
(define-syntax-class (struct-clause legacy)
#:attributes (nm type (body 1) (constructor-parts 1))
;#:literals (struct)
#:attributes (nm (body 1) (constructor-parts 1))
(pattern [(~or (~datum struct) #:struct)
nm:opt-parent (body ...)
(~var opts (struct-opts legacy #'nm.nm))]
#:with (constructor-parts ...) #'opts.ctor-value
#:attr type #'opts.type))
(~var constructor (opt-constructor legacy #'nm.nm))]
#:with (constructor-parts ...) #'constructor.value))
(define-syntax-class signature-clause
#:literals (:)
@ -157,63 +137,44 @@
(pattern [(~or (~datum opaque) #:opaque) opaque ty:id pred:id #:name-exists]
#:with opt #'(#:name-exists)))
(define-syntax-class (clause legacy unsafe? lib)
(define-syntax-class (clause legacy lib)
#:attributes (spec)
(pattern oc:opaque-clause #:attr spec
#`(require/opaque-type oc.ty oc.pred #,lib . oc.opt))
(pattern (~var strc (struct-clause legacy)) #:attr spec
#`(require-typed-struct strc.nm (strc.body ...) strc.constructor-parts ...
#:type-name strc.type
#,@(if unsafe? #'(unsafe-kw) #'())
#,lib))
#`(require-typed-struct strc.nm (strc.body ...) strc.constructor-parts ... #,lib))
(pattern sig:signature-clause #:attr spec
#`(require-typed-signature sig.sig-name (sig.var ...) (sig.type ...) #,lib))
(pattern sc:simple-clause #:attr spec
#`(require/typed #:internal sc.nm sc.ty #,lib
#,@(if unsafe? #'(unsafe-kw) #'()))))
#`(require/typed #:internal sc.nm sc.ty #,lib)))
(define ((r/t-maker legacy unsafe?) stx)
(define ((r/t-maker legacy) stx)
(unless (or (unbox typed-context?) (eq? (syntax-local-context) 'module-begin))
(raise-syntax-error #f "only allowed in a typed module" stx))
(syntax-parse stx
[(_ lib:expr (~var c (clause legacy unsafe? #'lib)) ...)
[(_ lib:expr (~var c (clause legacy #'lib)) ...)
(when (zero? (syntax-length #'(c ...)))
(raise-syntax-error #f "at least one specification is required" stx))
#`(begin c.spec ...)]
[(_ #:internal nm:opt-rename ty lib
(~optional [~seq #:struct-maker parent])
(~optional (~and (~seq (~literal unsafe-kw))
(~bind [unsafe? #t]))
#:defaults ([unsafe? #f])))
[(_ #:internal nm:opt-rename ty lib (~optional [~seq #:struct-maker parent]) ...)
(define/with-syntax hidden (generate-temporary #'nm.nm))
(define/with-syntax sm (if (attribute parent)
#'(#:struct-maker parent)
#'()))
(cond [(not (attribute unsafe?))
;; define `cnt*` to be fixed up later by the module type-checking
(define cnt*
(syntax-local-lift-expression
(make-contract-def-rhs #'ty #f (attribute parent))))
(quasisyntax/loc stx
(begin
;; register the identifier so that it has a binding (for top-level)
#,@(if (eq? (syntax-local-context) 'top-level)
(list #'(define-syntaxes (hidden) (values)))
null)
#,(internal #'(require/typed-internal hidden ty . sm))
#,(ignore #`(require/contract nm.spec hidden #,cnt* lib))))]
[else
(define/with-syntax hidden2 (generate-temporary #'nm.nm))
(quasisyntax/loc stx
(begin
(require (only-in lib [nm.orig-nm hidden]))
;; need this indirection since `hidden` may expand
;; to a different identifier that TR doesn't know about
#,(ignore #'(define hidden2 hidden))
(rename-without-provide nm.nm hidden2)
#,(internal #'(require/typed-internal hidden2 ty . sm))))])]))
(values (r/t-maker #t #f) (r/t-maker #f #f) (r/t-maker #f #t))))
;; define `cnt*` to be fixed up later by the module type-checking
(define cnt*
(syntax-local-lift-expression
(make-contract-def-rhs #'ty #f (attribute parent))))
(quasisyntax/loc stx
(begin
;; register the identifier so that it has a binding (for top-level)
#,@(if (eq? (syntax-local-context) 'top-level)
(list #'(define-syntaxes (hidden) (values)))
null)
#,(internal #'(require/typed-internal hidden ty . sm))
#,(ignore #`(require/contract nm.spec hidden #,cnt* lib))))]))
(values (r/t-maker #t) (r/t-maker #f))))
(define (require/typed/provide stx)
@ -260,28 +221,9 @@
;; make-predicate
;; cast
;; Helpers to construct syntax for contract definitions
;; make-contract-def-rhs : Type-Stx Boolean Boolean -> Syntax
;; Helper to construct syntax for contract definitions
(define (make-contract-def-rhs type flat? maker?)
(define contract-def `#s(contract-def ,type ,flat? ,maker? untyped))
(contract-def-property #'#f (λ () contract-def)))
;; make-contract-def-rhs/from-typed : Id Boolean Boolean -> Syntax
(define (make-contract-def-rhs/from-typed id flat? maker?)
(contract-def-property
#'#f
;; This function should only be called after the type-checking pass has finished.
;; By then `tc/#%expression` will have recognized the `casted-expr` property and
;; will have added the casted expression's original type to the cast-table, so
;; that `(cast-table-ref id)` can get that type here.
(λ ()
(define type-stx
(or (cast-table-ref id)
(int-err (string-append
"contract-def-property: thunk called too early\n"
" This should only be called after the type-checking pass has finished."))))
`#s(contract-def ,type-stx ,flat? ,maker? typed))))
(contract-def-property #'#f `#s(contract-def ,type ,flat? ,maker? untyped)))
(define (define-predicate stx)
(syntax-parse stx
@ -313,21 +255,21 @@
#`(#,(external-check-property #'#%expression check-valid-type)
#,(ignore-some/expr #`(flat-contract-predicate #,name) #'(Any -> Boolean : ty)))]))
;; wrapped above in the `forms` submodule
(define (core-cast stx)
(define (cast stx)
(syntax-parse stx
[(_ v:expr ty:expr)
(define (apply-contract v ctc-expr pos neg)
(define (apply-contract ctc-expr)
#`(#%expression
#,(ignore-some/expr
#`(let-values (((val) #,(with-type* v #'Any)))
#`(let-values (((val) #,(with-type* #'v #'Any)))
#,(syntax-property
(quasisyntax/loc stx
(contract
#,ctc-expr
val
'#,pos
'#,neg
'cast
'typed-world
val
(quote-srcloc #,stx)))
'feature-profile:TR-dynamic-check #t))
@ -336,13 +278,8 @@
(cond [(not (unbox typed-context?)) ; no-check, don't check
#'v]
[else
(define new-ty-ctc (syntax-local-lift-expression
(make-contract-def-rhs #'ty #f #f)))
(define existing-ty-id new-ty-ctc)
(define existing-ty-ctc (syntax-local-lift-expression
(make-contract-def-rhs/from-typed existing-ty-id #f #f)))
(define (store-existing-type existing-type)
(cast-table-set! existing-ty-id existing-type))
(define ctc (syntax-local-lift-expression
(make-contract-def-rhs #'ty #f #f)))
(define (check-valid-type _)
(define type (parse-type #'ty))
(define vars (fv type))
@ -352,12 +289,7 @@
"Type ~a could not be converted to a contract because it contains free variables."
type)))
#`(#,(external-check-property #'#%expression check-valid-type)
#,(apply-contract
(apply-contract
#`(#,(casted-expr-property #'#%expression store-existing-type)
v)
existing-ty-ctc 'typed-world 'cast)
new-ty-ctc 'cast 'typed-world))])]))
#,(apply-contract ctc))])]))
@ -365,25 +297,21 @@
(define-syntax-class name-exists-kw
(pattern #:name-exists))
(syntax-parse stx
[_ #:when (eq? 'module-begin (syntax-local-context))
;; it would be inconvenient to find the correct #%module-begin here, so we rely on splicing
#`(begin #,stx (begin))]
[(_ ty:id pred:id lib (~optional ne:name-exists-kw) ...)
;; This line appears redundant with the use of `define-type-alias` below, but
;; it's actually necessary for top-level uses because this opaque type may appear
;; in subsequent `require/typed` clauses, which needs to parse the types at
;; expansion-time, not at typechecking time when aliases are installed.
(register-resolved-type-alias #'ty (make-Opaque #'pred))
(with-syntax ([hidden (generate-temporary #'pred)])
(define pred-cnt
(syntax-local-lift-expression
(make-contract-def-rhs #'(-> Any Boolean) #f #f)))
(quasisyntax/loc stx
(begin
;; register the identifier for the top-level (see require/typed)
#,@(if (eq? (syntax-local-context) 'top-level)
(list #'(define-syntaxes (hidden) (values)))
null)
#,(ignore #'(define pred-cnt (any/c . c-> . boolean?)))
#,(internal #'(require/typed-internal hidden (Any -> Boolean : (Opaque pred))))
#,(if (attribute ne)
(internal (syntax/loc stx (define-type-alias-internal ty (Opaque pred))))
(syntax/loc stx (define-type-alias ty (Opaque pred))))
#,(ignore #`(require/contract pred hidden #,pred-cnt lib)))))]))
#,(ignore #'(require/contract pred hidden pred-cnt lib)))))]))
@ -428,18 +356,10 @@
(pattern (~seq #:constructor-name name:id) #:attr extra #f)
(pattern (~seq #:extra-constructor-name name:id) #:attr extra #t))
(define-splicing-syntax-class unsafe-clause
(pattern (~seq) #:attr unsafe? #f)
(pattern (~seq (~literal unsafe-kw)) #:attr unsafe? #t))
(define ((rts legacy) stx)
(syntax-parse stx #:literals (:)
[(_ name:opt-parent
([fld : ty] ...)
(~var input-maker (constructor-term legacy #'name.nm))
(~optional (~seq #:type-name type:id) #:defaults ([type #'name.nm]))
unsafe:unsafe-clause
lib)
[(_ name:opt-parent ([fld : ty] ...) (~var input-maker (constructor-term legacy #'name.nm)) lib)
(with-syntax* ([nm #'name.nm]
[parent #'name.parent]
[hidden (generate-temporary #'name.nm)]
@ -515,38 +435,21 @@
(make-struct-info-self-ctor #'internal-maker si)
si))
(dtsi* () spec type ([fld : ty] ...) #:maker maker-name #:type-only)
#,(ignore #'(require/contract pred hidden (or/c struct-predicate-procedure?/c (c-> any-wrap/c boolean?)) lib))
#,(internal #'(require/typed-internal hidden (Any -> Boolean : type)))
(require/typed #:internal (maker-name real-maker) type lib
#:struct-maker parent
#,@(if (attribute unsafe.unsafe?) #'(unsafe-kw) #'()))
(dtsi* () spec ([fld : ty] ...) #:maker maker-name #:type-only)
#,(ignore #'(require/contract pred hidden (any/c . c-> . boolean?) lib))
#,(internal #'(require/typed-internal hidden (Any -> Boolean : nm)))
(require/typed #:internal (maker-name real-maker) nm lib
#:struct-maker parent)
;This needs to be a different identifier to meet the specifications
;of struct (the id constructor shouldn't expand to it)
#,(if (syntax-e #'extra-maker)
#`(require/typed #:internal (maker-name extra-maker) type lib
#:struct-maker parent
#,@(if (attribute unsafe.unsafe?) #'(unsafe-kw) #'()))
#'(require/typed #:internal (maker-name extra-maker) nm lib
#:struct-maker parent)
#'(begin))
#,(if (not (free-identifier=? #'nm #'type))
#'(define-syntax type
(lambda (stx)
(raise-syntax-error
'type-check
(format "type name ~a used out of context in ~a"
(syntax->datum (if (stx-pair? stx)
(stx-car stx)
stx))
(syntax->datum stx))
stx
(and (stx-pair? stx) (stx-car stx)))))
#'(begin))
#,@(if (attribute unsafe.unsafe?)
#'((require/typed #:internal sel (type -> ty) lib unsafe-kw) ...)
#'((require/typed lib [sel (type -> ty)]) ...)))))]))
(require/typed lib
[sel (nm -> ty)]) ...)))]))
(values (rts #t) (rts #f))))

View File

@ -46,7 +46,7 @@
(format "field `~a' requires a type annotation"
(syntax-e #'fld))
#:with form 'dummy))
(define-syntax-class struct-name
#:description "struct name (with optional super-struct name)"
#:attributes (name super)
@ -72,31 +72,16 @@
(define-splicing-syntax-class struct-options
#:description "typed structure type options"
#:attributes (guard mutable? transparent? prefab? cname ecname type untyped
[prop 1] [prop-val 1])
#:attributes (guard mutable? transparent? prefab? [prop 1] [prop-val 1])
(pattern (~seq (~or (~optional (~seq (~and #:mutable mutable?)))
(~optional (~seq (~and #:transparent transparent?)))
(~optional (~seq (~and #:prefab prefab?)))
(~optional (~or (~and (~seq #:constructor-name cname)
(~bind [ecname #f]))
(~and (~seq #:extra-constructor-name ecname)
(~bind [cname #f]))))
(~optional (~seq #:type-name type:id))
;; FIXME: unsound, but relied on in core libraries
;; #:guard ought to be supportable with some work
;; #:property is harder
(~optional (~seq #:guard guard:expr))
(~seq #:property prop:expr prop-val:expr))
...)
#:attr untyped #`(#,@(if (attribute mutable?) #'(#:mutable) #'())
#,@(if (attribute transparent?) #'(#:transparent) #'())
#,@(if (attribute prefab?) #'(#:prefab) #'())
#,@(if (attribute cname) #'(#:constructor-name cname) #'())
#,@(if (attribute ecname) #'(#:extra-constructor-name ecname) #'())
#,@(if (attribute guard) #'(#:guard guard) #'())
#,@(append* (for/list ([prop (in-list (attribute prop))]
[prop-val (in-list (attribute prop-val))])
(list #'#:property prop prop-val))))))
...)))
(define-syntax-class dtsi-struct-name
#:description "struct name (with optional super-struct name)"
@ -109,27 +94,13 @@
(define-syntax (define-typed-struct/exec stx)
(syntax-parse stx #:literals (:)
[(_ nm:struct-name ((~describe "field specification" [fld:optionally-annotated-name]) ...)
[proc : proc-ty] (~optional (~seq #:type-name type:id)))
[(_ nm ((~describe "field specification" [fld:optionally-annotated-name]) ...) [proc : proc-ty])
(with-syntax*
([type (or (attribute type) #'nm.name)]
[proc* (with-type* #'proc #'proc-ty)]
([proc* (with-type* #'proc #'proc-ty)]
[d-s (ignore-some (syntax/loc stx (define-struct nm (fld.name ...)
#:property prop:procedure proc*)))]
[stx-err-fun (if (not (free-identifier=? #'nm.name #'type))
(syntax/loc stx
(define-syntax type
(lambda (stx)
(raise-syntax-error
'type-check
(format "type name ~a used out of context in ~a"
(syntax->datum (if (stx-pair? stx) (stx-car stx) stx))
(syntax->datum stx))
stx
(and (stx-pair? stx) (stx-car stx))))))
#'(begin))]
[dtsi (quasisyntax/loc stx (dtsi/exec* () nm type (fld ...) proc-ty))])
#'(begin d-s stx-err-fun dtsi))]))
[dtsi (quasisyntax/loc stx (dtsi/exec* () nm (fld ...) proc-ty))])
#'(begin d-s dtsi))]))
(define-syntaxes (dtsi* dtsi/exec*)
(let ()
@ -150,63 +121,39 @@
;; User-facing macros for defining typed structure types
(define-syntax (define-typed-struct stx)
(syntax-parse stx
[(_ vars:maybe-type-vars nm:struct-name (fs:fld-spec ...) opts:struct-options)
(quasisyntax/loc stx
(-struct #,@#'vars
#,@(if (stx-pair? #'nm)
#'nm
(list #'nm))
(fs ...)
;; If there's already a (extra) constructor name supplied,
;; then Racket's `define-struct` doesn't define a `make-`
;; constructor either so don't pass anything extra.
#,@(if (or (attribute opts.cname)
(attribute opts.ecname))
null
(list #'#:extra-constructor-name
(second (build-struct-names #'nm.name null #t #t))))
. opts))]))
(define-syntaxes (define-typed-struct -struct)
(values
(lambda (stx)
(syntax-parse stx
[(_ vars:maybe-type-vars nm:struct-name (fs:fld-spec ...)
opts:struct-options)
(let ([mutable? (if (attribute opts.mutable?) #'(#:mutable) #'())]
[cname (second (build-struct-names #'nm.name null #t #t))]
[prefab? (if (attribute opts.prefab?) #'(#:prefab) #'())])
(with-syntax ([d-s (ignore-some
(syntax/loc stx (define-struct nm (fs.fld ...) . opts)))]
[dtsi (quasisyntax/loc stx
(dtsi* (vars.vars ...) nm (fs.form ...)
#:maker #,cname
#,@mutable?
#,@prefab?))])
#'(begin d-s dtsi)))]))
(lambda (stx)
(syntax-parse stx
[(_ vars:maybe-type-vars nm:struct-name/new (fs:fld-spec ...)
opts:struct-options)
(let ([mutable? (if (attribute opts.mutable?) #'(#:mutable) #'())]
[prefab? (if (attribute opts.prefab?) #'(#:prefab) #'())])
(with-syntax ([d-s (ignore (quasisyntax/loc stx
(struct #,@(attribute nm.new-spec) (fs.fld ...)
. opts)))]
[dtsi (quasisyntax/loc stx
(dtsi* (vars.vars ...)
nm.old-spec (fs.form ...)
#,@mutable?
#,@prefab?))])
#'(begin d-s dtsi)))]))))
(define-syntax (-struct stx)
(syntax-parse stx
[(_ vars:maybe-type-vars nm:struct-name/new (fs:fld-spec ...)
opts:struct-options)
(let ([mutable? (if (attribute opts.mutable?) #'(#:mutable) #'())]
[prefab? (if (attribute opts.prefab?) #'(#:prefab) #'())]
[maker (if (attribute opts.cname)
#`(#:maker #,(attribute opts.cname))
#'())]
[extra-maker (if (attribute opts.ecname)
#`(#:extra-maker #,(attribute opts.ecname))
#'())])
(with-syntax* ([type (or (attribute opts.type) #'nm.name)]
[d-s (ignore (quasisyntax/loc stx
(struct #,@(attribute nm.new-spec) (fs.fld ...)
. opts.untyped)))]
[stx-err-fun (if (not (free-identifier=? #'nm.name #'type))
(syntax/loc stx
(define-syntax type
(lambda (stx)
(raise-syntax-error
'type-check
(format "type name ~a used out of context in ~a"
(syntax->datum (if (stx-pair? stx)
(stx-car stx)
stx))
(syntax->datum stx))
stx
(and (stx-pair? stx) (stx-car stx))))))
#'(begin))]
[dtsi (quasisyntax/loc stx
(dtsi* (vars.vars ...)
nm.old-spec type (fs.form ...)
#,@mutable?
#,@prefab?
#,@maker
#,@extra-maker))])
#'(begin d-s stx-err-fun dtsi)))]))
;; this has to live here because it's used below
(define-syntax (define-type-alias stx)
@ -235,9 +182,7 @@
#'(lambda (stx)
(raise-syntax-error
'type-check
(format "type name used out of context\n type: ~a\n in: ~a"
(syntax->datum (if (stx-pair? stx) (stx-car stx) stx))
(syntax->datum stx))
"type name used out of context"
stx
(and (stx-pair? stx) (stx-car stx)))))
#`(begin

View File

@ -145,12 +145,9 @@ the typed racket language.
(provide (all-from-out "base-contracted.rkt")))
(begin-for-syntax
(require racket/runtime-path
(for-syntax racket/base))
(define-runtime-module-path-index contract-defs-submod
'(submod "." #%contract-defs))
(require racket/base "../utils/redirect-contract.rkt")
(define mk (make-make-redirect-to-contract contract-defs-submod)))
(define varref (#%variable-reference))
(define mk (make-make-redirect-to-contract varref)))
(define-syntax-rule (def-redirect id ...)
(begin (define-syntax id (mk (quote-syntax id))) ... (provide id ...)))
@ -160,7 +157,11 @@ the typed racket language.
;; Lazily loaded b/c they're only used sometimes, so we save a lot
;; of loading by not having them when they are unneeded
(begin-for-syntax
(lazy-require [syntax/define (normalize-definition)]))
(lazy-require ["../rep/type-rep.rkt" (make-Opaque Error?)]
["../types/utils.rkt" (fv)]
[syntax/define (normalize-definition)]
[typed-racket/private/parse-type (parse-type)]
[typed-racket/env/type-alias-env (register-resolved-type-alias)]))
(define-for-syntax (with-type* expr ty)
(with-type #`(ann #,expr #,ty)))
@ -811,13 +812,7 @@ the typed racket language.
(define i 0)
(for (clauses ...)
(define v body-expr)
;; can't use `unsafe-fx=` here
;; if `n` is larger than a fixnum, this is unsafe, and we
;; don't know whether that's the case until we try creating
;; the vector
;; other unsafe ops are after vector allocation, and so are
;; fine
(cond [(= i 0) (define new-vs (ann (make-vector n v) T))
(cond [(unsafe-fx= i 0) (define new-vs (ann (make-vector n v) T))
(set! vs new-vs)]
[else (unsafe-vector-set! vs i v)])
(set! i (unsafe-fx+ i 1))

View File

@ -43,7 +43,7 @@
"../tc-setup.rkt"
(private parse-type syntax-properties)
(types utils abbrev printer)
(typecheck possible-domains typechecker)
(typecheck tc-app-helper typechecker)
(rep type-rep)
(utils tc-utils)
(for-syntax racket/base syntax/parse)

View File

@ -9,10 +9,7 @@
(begin
(define-syntax (nm stx)
(raise-syntax-error
'type-check
(format "type name used out of context\n type: ~a\n in: ~a"
(syntax->datum (if (stx-pair? stx) (stx-car stx) stx))
(syntax->datum stx))
'type-check "type name used out of context"
stx
(and (stx-pair? stx) (stx-car stx))))
...

View File

@ -1,14 +0,0 @@
#lang racket/base
(require racket/dict racket/sequence)
(provide id< sorted-dict-map in-sorted-dict)
(define (id< a b) (symbol<? (syntax-e a) (syntax-e b)))
(define (sorted-dict-map dict f <)
(define sorted (sort #:key car (dict-map dict cons) <))
(map (lambda (a) (f (car a) (cdr a))) sorted))
(define (in-sorted-dict dict <)
(define sorted (sort #:key car (dict-map dict cons) <))
(in-dict sorted))

View File

@ -5,7 +5,6 @@
(require "../types/tc-error.rkt"
"../utils/tc-utils.rkt"
"env-utils.rkt"
syntax/parse
syntax/id-table
racket/lazy-require)
@ -103,4 +102,4 @@
;; map over the-mapping, producing a list
;; (id type -> T) -> listof[T]
(define (type-env-map f)
(sorted-dict-map the-mapping f id<))
(free-id-table-map the-mapping f))

View File

@ -10,10 +10,10 @@
"mvar-env.rkt"
"signature-env.rkt"
(rename-in racket/private/sort [sort raw-sort])
(rep type-rep object-rep prop-rep rep-utils free-variance)
(rep type-rep object-rep filter-rep rep-utils free-variance)
(for-syntax syntax/parse racket/base)
(types abbrev union)
racket/dict racket/list racket/set racket/promise
racket/dict racket/list racket/promise
mzlib/pconvert racket/match)
(provide ;; convenience form for defining an initial environment
@ -64,28 +64,22 @@
[(? 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
(PropSet: (TrueProp:)
(TrueProp:))
(Empty:))))
#f #f '())))
[(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (Top:) (Top:)) (Empty:)))) #f #f '())))
`(simple-> (list ,@(map sub dom)) ,(sub t))]
[(Function: (list (arr: dom (Values: (list (Result: t (PropSet: (TypeProp: pth ft)
(NotTypeProp: pth ft))
[(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (TypeFilter: ft pth)
(NotTypeFilter: ft pth))
(Empty:))))
#f #f '())))
`(make-pred-ty (list ,@(map sub dom)) ,(sub t) ,(sub ft) ,(sub pth))]
[(Function: (list (arr: dom (Values: (list (Result: t (PropSet: (NotTypeProp: (Path: pth (list 0 0))
(== -False))
(TypeProp: (Path: pth (list 0 0))
(== -False)))
[(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (NotTypeFilter: (== -False)
(Path: pth (list 0 0)))
(TypeFilter: (== -False)
(Path: pth (list 0 0))))
(Path: pth (list 0 0)))))
#f #f '())))
`(->acc (list ,@(map sub dom)) ,(sub t) ,(sub pth))]
[(Result: t (PropSet: (TrueProp:) (TrueProp:)) (Empty:)) `(-result ,(sub t))]
[(Result: t (FilterSet: (Top:) (Top:)) (Empty:)) `(-result ,(sub t))]
[(Union: elems) (split-union elems)]
[(Intersection: elems) `(make-Intersection (set ,@(for/list ([elem (in-immutable-set elems)])
(sub elem))))]
[(Base: n cnt pred _) (int-err "Base type ~a not in predefined-type-table" n)]
[(Name: stx args struct?)
`(make-Name (quote-syntax ,stx) ,args ,struct?)]
@ -133,16 +127,15 @@
(define ty (force (cdr id/ty)))
`(cons (quote-syntax ,id) ,(sub ty)))
m))
(define serialized-extends (and extends `(quote-syntax ,extends)))
`(make-Signature (quote-syntax ,name)
,serialized-extends
(quote-syntax ,extends)
(list ,@(serialize-mapping mapping)))]
[(arr: dom rng rest drest kws)
`(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws))]
[(TypeProp: o t)
`(make-TypeProp ,(sub o) ,(sub t))]
[(NotTypeProp: o t)
`(make-NotTypeProp ,(sub o) ,(sub t))]
[(TypeFilter: t p)
`(make-TypeFilter ,(sub t) ,(sub p))]
[(NotTypeFilter: t p)
`(make-NotTypeFilter ,(sub t) ,(sub p))]
[(Path: p i)
`(make-Path ,(sub p) ,(if (identifier? i)
`(quote-syntax ,i)

View File

@ -6,7 +6,6 @@
(provide register-signature!
finalize-signatures!
lookup-signature
lookup-signature/check
signature-env-map
with-signature-env/extend)
@ -14,7 +13,6 @@
racket/match
racket/promise
(for-syntax syntax/parse racket/base)
"env-utils.rkt"
"../utils/utils.rkt"
(utils tc-utils)
(rep type-rep))
@ -67,15 +65,5 @@
(define (lookup-signature id)
(free-id-table-ref (signature-env) id #f))
;; lookup-signature/check : identifier? -> Signature?
;; lookup the identifier in the signature environment
;; errors if there is no such typed signature
(define (lookup-signature/check id)
(or (lookup-signature id)
(tc-error/fields "use of untyped signature in typed code"
#:more "consider using `require/typed' to import it"
"signature" (syntax-e id)
#:stx id)))
(define (signature-env-map f)
(sorted-dict-map (signature-env) f id<))
(free-id-table-map (signature-env) f))

View File

@ -1,7 +1,6 @@
#lang racket/base
(require "../utils/utils.rkt"
"env-utils.rkt"
syntax/id-table racket/dict
(utils tc-utils)
(typecheck renamer)
@ -62,6 +61,6 @@
;; map over the-mapping, producing a list
;; (id type -> T) -> listof[T]
(define (type-alias-env-map f)
(for/list ([(id t) (in-sorted-dict the-mapping id<)]
(for/list ([(id t) (in-dict the-mapping)]
#:when (resolved? t))
(f id (resolved-ty t))))

View File

@ -6,12 +6,12 @@
(contract-req)
(rep object-rep))
(require-for-cond-contract (rep type-rep prop-rep))
(require-for-cond-contract (rep type-rep filter-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 Prop?)]
[props (listof Filter/c)]
[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 Prop?))]
[replace-props (env? (listof Prop?) . -> . env?)]
[env-props (env? . -> . (listof Filter/c))]
[replace-props (env? (listof Filter/c) . -> . 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?))])

View File

@ -2,8 +2,7 @@
;; Environment for type names
(require "../utils/utils.rkt"
"env-utils.rkt")
(require "../utils/utils.rkt")
(require syntax/id-table
(contract-req)
@ -59,7 +58,7 @@
;; map over the-mapping, producing a list
;; (id type -> T) -> listof[T]
(define (type-name-env-map f)
(sorted-dict-map the-mapping f id<))
(free-id-table-map the-mapping f))
(define (add-alias from to)
(when (lookup-type-name to (lambda () #f))
@ -84,7 +83,7 @@
;; map over the-mapping, producing a list
;; (id variance -> T) -> listof[T]
(define (type-variance-env-map f)
(sorted-dict-map variance-mapping f id<))
(free-id-table-map variance-mapping f))
;; Refines the variance of a type in the name environment
(define (refine-variance! names types tvarss)

View File

@ -7,7 +7,7 @@
racket/match
racket/list)
(import intersect^ dmap^)
(import restrict^ dmap^)
(export constraints^)
;; Widest constraint possible
@ -34,7 +34,7 @@
;; intersect the given types. produces a lower bound on both, but
;; perhaps not the GLB
(define (meet S T)
(let ([s* (intersect S T)])
(let ([s* (restrict S T)])
(if (and (subtype s* S)
(subtype s* T))
s*

View File

@ -14,7 +14,7 @@
#'((early-return rhs ...))))
(syntax-parse stx
[(_ e [c . r:rhs] ...)
(syntax/loc stx (match* e [c . r.r] ...))]))
#'(match* e [c . r.r] ...)]))
(begin-for-syntax
(define-splicing-syntax-class arg

View File

@ -11,7 +11,7 @@
(except-in
(combine-in
(utils tc-utils)
(rep free-variance type-rep prop-rep object-rep rep-utils)
(rep free-variance type-rep filter-rep object-rep rep-utils)
(types utils abbrev numeric-tower union subtype resolve
substitute generalize prefab)
(env index-env tvar-env))
@ -19,7 +19,7 @@
"constraint-structs.rkt"
"signatures.rkt" "fail.rkt"
"promote-demote.rkt"
racket/match racket/set
racket/match
mzlib/etc
(contract-req)
(for-syntax
@ -212,7 +212,7 @@
[(_ seq) #'(app List->seq (? values seq))])))
;; generate-dbound-prefix: Symbol Type/c Natural (U Symbol #f) -> (Values (Listof Symbol) (Listof Type/c))
;; generate-dbound-prefix: Symbol Type/c Natural Symbol -> (Values (Listof Symbol) (Listof Type/c))
;; Substitutes n fresh new variables, replaces dotted occurences of v in t with the variables (and
;; maybe new-end), and then for each variable substitutes it in for regular occurences of v.
(define (generate-dbound-prefix v ty n new-end)
@ -224,23 +224,23 @@
(substitute (make-F var) v ty*))))
(define/cond-contract (cgen/prop context s t)
(context? Prop? Prop? . -> . (or/c #f cset?))
(define/cond-contract (cgen/filter context s t)
(context? Filter? Filter? . -> . (or/c #f cset?))
(match* (s t)
[(e e) (empty-cset/context context)]
[(e (TrueProp:)) (empty-cset/context context)]
[(e (Top:)) (empty-cset/context context)]
;; FIXME - is there something to be said about the logical ones?
[((TypeProp: o s) (TypeProp: o t)) (cgen/inv context s t)]
[((NotTypeProp: o s) (NotTypeProp: o t)) (cgen/inv context s t)]
[((TypeFilter: s p) (TypeFilter: t p)) (cgen/inv context s t)]
[((NotTypeFilter: s p) (NotTypeFilter: t p)) (cgen/inv context s t)]
[(_ _) #f]))
;; s and t must be *latent* prop sets
(define/cond-contract (cgen/prop-set context s t)
(context? PropSet? PropSet? . -> . (or/c #f cset?))
;; s and t must be *latent* filter sets
(define/cond-contract (cgen/filter-set context s t)
(context? FilterSet? FilterSet? . -> . (or/c #f cset?))
(match* (s t)
[(e e) (empty-cset/context context)]
[((PropSet: p+ p-) (PropSet: q+ q-))
(% cset-meet (cgen/prop context p+ q+) (cgen/prop context p- q-))]
[((FilterSet: s+ s-) (FilterSet: t+ t-))
(% cset-meet (cgen/filter context s+ t+) (cgen/filter context s- t-))]
[(_ _) #f]))
(define/cond-contract (cgen/object context s t)
@ -320,7 +320,7 @@
(% move-dotted-rest-to-dmap (cgen (context-add-var context dbound) s-dty t-dty) dbound dbound*)))]
[((seq ss (dotted-end s-dty dbound))
(seq ts (dotted-end t-dty dbound*)))
#:return-unless (inferable-index? context dbound*) #f
#:when (inferable-index? context dbound*)
#:return-unless (= (length ss) (length ts)) #f
(% cset-meet
(cgen/list context ss ts)
@ -439,26 +439,26 @@
;; CG-Top
[(_ (Univ:)) empty]
;; AnyValues
[((AnyValues: p) (AnyValues: q))
(cgen/prop context p q)]
[((AnyValues: s-f) (AnyValues: t-f))
(cgen/filter context s-f t-f)]
[((or (Values: (list (Result: _ psets _) ...))
(ValuesDots: (list (Result: _ psets _) ...) _ _))
(AnyValues: q))
[((or (Values: (list (Result: _ fs _) ...))
(ValuesDots: (list (Result: _ fs _) ...) _ _))
(AnyValues: t-f))
(cset-join
(filter identity
(for/list ([pset (in-list psets)])
(match pset
[(PropSet: p+ p-)
(% cset-meet (cgen/prop context p+ q) (cgen/prop context p- q))]))))]
(for/list ([f (in-list fs)])
(match f
[(FilterSet: f+ f-)
(% cset-meet (cgen/filter context f+ t-f) (cgen/filter context f- t-f))]))))]
;; check all non Type/c first so that calling subtype is safe
;; check each element
[((Result: s pset-s o-s)
(Result: t pset-t o-t))
[((Result: s f-s o-s)
(Result: t f-t o-t))
(% cset-meet (cg s t)
(cgen/prop-set context pset-s pset-t)
(cgen/filter-set context f-s f-t)
(cgen/object context o-s o-t))]
;; Values just delegate to cgen/seq, except special handling for -Bottom.
@ -525,19 +525,6 @@
[((? Mu? s) t) (cg (unfold s) t)]
[(s (? Mu? t)) (cg s (unfold t))]
;; find *an* element of elems which can be made a subtype of T
[((Intersection: ts) T)
(cset-join
(for*/list ([t (in-immutable-set ts)]
[v (in-value (cg t T))]
#:when v)
v))]
;; constrain S to be below *each* element of elems, and then combine the constraints
[(S (Intersection: ts))
(define cs (for/list/fail ([ts (in-immutable-set ts)]) (cg S ts)))
(and cs (cset-meet* (cons empty cs)))]
;; constrain *each* element of es to be below T, and then combine the constraints
[((Union: es) T)
(define cs (for/list/fail ([e (in-list es)]) (cg e T)))
@ -881,22 +868,21 @@
(early-return
(define short-S (take S (length T)))
(define rest-S (drop S (length T)))
;; Generate a new type corresponding to T-dotted for every extra arg.
(define-values (new-vars new-Ts)
(generate-dbound-prefix dotted-var T-dotted (length rest-S) #f))
(define (subst t)
(substitute-dots (map make-F new-vars) #f dotted-var t))
(define ctx (context null (append new-vars X) (list dotted-var)))
(define ctx (context null X (list dotted-var)))
(define expected-cset (if expected
(cgen ctx (subst R) expected)
(cgen ctx R expected)
(empty-cset '() '())))
#:return-unless expected-cset #f
(define cs (% move-vars-to-dmap
(% cset-meet
(cgen/list ctx short-S (map subst T) #:expected-cset expected-cset)
(cgen/list ctx rest-S new-Ts #:expected-cset expected-cset))
dotted-var new-vars))
(define cs-short (cgen/list ctx short-S T #:expected-cset expected-cset))
#:return-unless cs-short #f
(define-values (new-vars new-Ts)
(generate-dbound-prefix dotted-var T-dotted (length rest-S) #f))
(define cs-dotted (cgen/list (context-add-vars ctx new-vars) rest-S new-Ts
#:expected-cset expected-cset))
#:return-unless cs-dotted #f
(define cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars))
#:return-unless cs-dotted* #f
(define cs (cset-meet cs-short cs-dotted*))
#:return-unless cs #f
(define m (cset-meet cs expected-cset))
#:return-unless m #f

View File

@ -1,11 +1,11 @@
#lang racket/base
(require "infer-unit.rkt" "constraints.rkt" "dmap.rkt" "signatures.rkt"
"intersect.rkt"
"restrict.rkt"
(only-in racket/unit provide-signature-elements
define-values/invoke-unit/infer link))
(provide-signature-elements intersect^ infer^)
(provide-signature-elements restrict^ infer^)
(define-values/invoke-unit/infer
(link infer@ constraints@ dmap@ intersect@))
(link infer@ constraints@ dmap@ restrict@))

View File

@ -1,71 +0,0 @@
#lang racket/unit
(require "../utils/utils.rkt")
(require (rep type-rep)
(types abbrev base-abbrev union subtype resolve)
"signatures.rkt"
racket/match
racket/set)
(import infer^)
(export intersect^)
;; compute the intersection of two types
;; (note: previously called restrict)
(define (intersect t1 t2)
;; build-type: build a type while propogating bottom
(define (build-type constructor . args)
(if (memf Bottom? args) -Bottom (apply constructor args)))
;; resolved is a set tracking previously seen intersect cases
;; (i.e. pairs of t1 t2) to prevent infinite unfolding.
;; subtyping performs a similar check for the same
;; reason
(let intersect
([t1 t1] [t2 t2] [resolved (set)])
(match*/no-order
(t1 t2)
;; already a subtype
[(t1 t2) #:no-order #:when (subtype t1 t2) t1]
;; polymorphic intersect
[(t1 (Poly: vars t))
#:no-order
#:when (infer vars null (list t1) (list t) #f)
t1]
;; structural recursion on types
[((Pair: a1 d1) (Pair: a2 d2))
(build-type -pair
(intersect a1 a2 resolved)
(intersect d1 d2 resolved))]
;; FIXME: support structural updating for structs when structs are updated to
;; contain not only *if* they are polymorphic, but *which* fields are too
;;[((Struct: _ _ _ _ _ _)
;; (Struct: _ _ _ _ _ _))]
[((Syntax: t1*) (Syntax: t2*))
(build-type -Syntax (intersect t1* t2* resolved))]
[((Promise: t1*) (Promise: t2*))
(build-type -Promise (intersect t1* t2* resolved))]
;; unions
[((Union: t1s) t2)
#:no-order
(apply Un (map (λ (t1) (intersect t1 t2 resolved)) t1s))]
;; intersections
[((Intersection: t1s) t2)
#:no-order
(apply -unsafe-intersect (for/list ([t1 (in-immutable-set t1s)])
(intersect t1 t2 resolved)))]
;; resolve resolvable types if we haven't already done so
[((? needs-resolving? t1) t2)
#:no-order
#:when (not (or (set-member? resolved (cons t1 t2))
(set-member? resolved (cons t2 t1))))
(intersect (resolve t1) t2 (set-add resolved (cons t1 t2)))]
;; t2 and t1 have a complex relationship, so we build an intersection
;; (note: intersection checks for overlap)
[(t1 t2) (-unsafe-intersect t1 t2)])))

View File

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

View File

@ -0,0 +1,68 @@
#lang racket/unit
(require "../utils/utils.rkt")
(require (rep type-rep)
(types abbrev base-abbrev union subtype remove-intersect resolve)
"signatures.rkt"
racket/match
racket/set)
(import infer^)
(export restrict^)
;; restrict t1 to be a subtype of t2
;; if `pref' is 'new, use t2 when giving up, otherwise use t1
(define (restrict t1 t2 [pref 'new])
;; build-type: build a type while propogating bottom
(define (build-type constructor . args)
(if (memf Bottom? args) -Bottom (apply constructor args)))
;; resolved is a set tracking previously seen restrict cases
;; (i.e. pairs of t1 t2) to prevent infinite unfolding.
;; subtyping performs a similar check for the same
;; reason
(define (restrict* t1 t2 pref resolved)
(match* (t1 t2)
;; already a subtype
[(_ _) #:when (subtype t1 t2)
t1]
;; polymorphic restrict
[(_ (Poly: vars t)) #:when (infer vars null (list t1) (list t) #f)
t1]
;; structural recursion on types
[((Pair: a1 d1) (Pair: a2 d2))
(build-type -pair
(restrict* a1 a2 pref resolved)
(restrict* d1 d2 pref resolved))]
;; FIXME: support structural updating for structs when structs are updated to
;; contain not only *if* they are polymorphic, but *which* fields are too
;;[((Struct: _ _ _ _ _ _)
;; (Struct: _ _ _ _ _ _))]
[((Syntax: t1*) (Syntax: t2*))
(build-type -Syntax (restrict* t1* t2* pref resolved))]
[((Promise: t1*) (Promise: t2*))
(build-type -Promise (restrict* t1* t2* pref resolved))]
;; unions
[((Union: t1s) _) (apply Un (map (λ (t1*) (restrict* t1* t2 pref resolved)) t1s))]
[(_ (Union: t2s)) (apply Un (map (λ (t2*) (restrict* t1 t2* pref resolved)) t2s))]
;; resolve resolvable types if we haven't already done so
[((? needs-resolving?) _) #:when (not (set-member? resolved (cons t1 t2)))
(restrict* (resolve t1) t2 pref (set-add resolved (cons t1 t2)))]
[(_ (? needs-resolving?)) #:when (not (set-member? resolved (cons t1 t2)))
(restrict* t1 (resolve t2) pref (set-add resolved (cons t1 t2)))]
;; we don't actually want this - want something that's a part of t1
[(_ _) #:when (subtype t2 t1)
t2]
;; there's no overlap, so the restriction is empty
[(_ _) #:when (not (overlap t1 t2))
(Un)]
;; t2 and t1 have a complex relationship, so we punt
[(_ _) (if (eq? pref 'new) t2 t1)]))
(restrict* t1 t2 pref (set)))

View File

@ -20,8 +20,8 @@
[cond-contracted cset-join ((listof cset?) . -> . cset?)]
[cond-contracted c-meet ((c? c?) (symbol?) . ->* . (or/c #f c?))]))
(define-signature intersect^
([cond-contracted intersect (Type/c Type/c . -> . Type/c)]))
(define-signature restrict^
([cond-contracted restrict ((Type/c Type/c) ((or/c 'new 'orig)) . ->* . Type/c)]))
(define-signature infer^
([cond-contracted infer ((;; variables from the forall

View File

@ -1,12 +1,11 @@
#lang racket/base
(require syntax/parse syntax/stx syntax/id-table racket/promise
(require syntax/parse syntax/stx racket/promise
racket/syntax racket/match syntax/parse/experimental/specialize
"../utils/utils.rkt" racket/unsafe/ops racket/sequence
(for-template racket/base racket/math racket/flonum racket/unsafe/ops)
(types numeric-tower subtype type-table utils)
(optimizer utils numeric-utils logging float unboxed-tables)
(utils tc-utils))
(optimizer utils numeric-utils logging float unboxed-tables))
(provide float-complex-opt-expr
float-complex-expr
@ -51,56 +50,14 @@
"The optimizer could optimize it better if it had type Float-Complex.")
this-syntax))
;; keep track of operands that were reals (and thus had exact 0 as imaginary part)
(define real-id-table (make-free-id-table))
(define (was-real? stx)
(free-id-table-ref real-id-table stx #f))
(define (mark-as-real stx)
(free-id-table-set! real-id-table stx #t)
stx)
;; keep track of operands that were not floats (i.e. rationals and single floats)
;; to avoid prematurely converting to floats, which may change results
(define non-float-table (make-hash))
(define (as-non-float stx)
(hash-ref non-float-table stx #f))
(define (mark-as-non-float stx [orig stx])
(hash-set! non-float-table stx orig)
stx)
;; If a part is 0.0?
(define (0.0? stx)
(equal? (syntax->datum stx) 0.0))
(define (n-ary->binary/non-floats op unsafe this-syntax cs)
(let loop ([o (stx-car cs)] [cs (stx-cdr cs)])
;; we're guaranteed to hit non-"non-float" operands before
;; we hit the end of the list. otherwise we wouldn't be doing
;; float-complex optimizations
(define c1 (stx-car cs))
(define o-nf (as-non-float o))
(define c1-nf (as-non-float c1))
(if (or o-nf c1-nf)
;; can't convert those to floats just yet, or may change
;; the result
(let ([new-o (mark-as-non-float
(quasisyntax/loc this-syntax
(#,op #,(or o-nf o) #,(or c1-nf c1))))])
(if (stx-null? (stx-cdr cs))
new-o
(loop new-o
(stx-cdr cs))))
;; we've hit floats, can start coercing
(n-ary->binary this-syntax unsafe (cons #`(real->double-flonum #,(or o-nf o)) cs)))))
;; a+bi / c+di, names for real and imag parts of result -> one let-values binding clause
(define (unbox-one-complex-/ a b c d res-real res-imag)
(define first-arg-real? (was-real? b))
(define second-arg-real? (was-real? d))
;; if both are real, we can short-circuit a lot
(define both-real? (and first-arg-real? second-arg-real?))
(define first-non-float (as-non-float a))
(define second-non-float (as-non-float c))
(when (and first-non-float (not second-non-float))
;; we're going from non-float to float operands, so need to coerce the first
(set! a #`(real->double-flonum #,a)))
(define both-real? (and (0.0? b) (0.0? d)))
;; we have the same cases as the Racket `/' primitive (except for the non-float ones)
(define d=0-case
#`(values (unsafe-fl+ (unsafe-fl/ #,a #,c)
@ -128,42 +85,10 @@
(unsafe-fl/ (unsafe-fl- (unsafe-fl* b r) a) den))])
(values (unsafe-fl/ (unsafe-fl+ b (unsafe-fl* a r)) den)
i)))
(cond [(and first-non-float second-non-float both-real?)
;; we haven't hit float operands, so we shouldn't coerce to float yet
#`[(#,(mark-as-non-float res-real)
#,(mark-as-real res-imag)) ; this case implies real
(values (/ #,first-non-float #,second-non-float)
0.0)]]
[second-non-float
;; may be dividing by exact 0, be conservative to preserve error
;; (res-real can't be non-float, since we've hit a float, so we either
;; error or coerce)
#`[(#,res-real #,(if both-real?
(mark-as-real res-imag)
res-imag))
(let-values ([(res-div)
(/ #,(if first-arg-real?
a
#`(make-rectangular #,a #,b))
#,(if second-arg-real?
second-non-float
#`(make-rectangular #,second-non-float
#,d)))])
#,(if both-real?
#'(values res-div 0.0)
#'(values (real-part res-div)
(imag-part res-div))))]]
[both-real?
#`[(#,res-real #,(mark-as-real res-imag))
(values (unsafe-fl/ #,a #,c)
0.0)]] ; currently not propagated
[second-arg-real?
(cond [both-real?
#`[(#,res-real #,res-imag)
(values (unsafe-fl/ #,a #,c)
(unsafe-fl/ #,b #,c))]]
[first-arg-real?
(unbox-one-float-complex-/ a c d res-real res-imag)]
0.0)]] ; currently not propagated
[else
#`[(#,res-real #,res-imag)
(cond [(unsafe-fl= #,d 0.0) #,d=0-case]
@ -187,7 +112,7 @@
#`(let* ([cm (unsafe-flabs #,c)]
[dm (unsafe-flabs #,d)]
[swap? (unsafe-fl< cm dm)]
[a #,a] ; don't swap with `b` (`0`) here, but handle below
[a #,a]
[c (if swap? #,d #,c)]
[d (if swap? #,c #,d)]
[r (unsafe-fl/ c d)]
@ -220,25 +145,15 @@
#:with (bindings ...)
#`(cs.bindings ... ...
#,@(let ()
(define (fl-sum cs)
(n-ary->binary/non-floats #'+ #'unsafe-fl+ this-syntax cs))
(define non-0-imags
;; to preserve result sign, ignore exact 0s
;; o/w, can have (+ -0.0 (->fl 0)) => 0.0, but would be -0.0
;; without the coercion
(for/list ([i (syntax->list #'(cs.imag-binding ...))]
#:unless (was-real? i))
i))
(define (fl-sum cs) (n-ary->binary this-syntax #'unsafe-fl+ cs))
(list
#`((real-binding) #,(fl-sum #'(cs.real-binding ...)))
#`((imag-binding)
#,(if (null? (cdr non-0-imags)) ; only one actual imag part
(car non-0-imags)
(fl-sum non-0-imags)))))))
#`((imag-binding) #,(fl-sum #'(cs.imag-binding ...)))))))
(pattern (#%plain-app op:+^ :unboxed-float-complex-opt-expr)
#:when (subtypeof? this-syntax -FloatComplex)
#:do [(log-unboxing-opt "unboxed unary float complex")])
(pattern (#%plain-app op:-^ (~between cs:unboxed-float-complex-opt-expr 2 +inf.0) ...)
#:when (subtypeof? this-syntax -FloatComplex)
#:with (real-binding imag-binding) (binding-names)
@ -246,21 +161,10 @@
#:with (bindings ...)
#`(cs.bindings ... ...
#,@(let ()
(define (fl-subtract cs)
(n-ary->binary/non-floats #'- #'unsafe-fl- this-syntax cs))
(define (fl-subtract cs) (n-ary->binary this-syntax #'unsafe-fl- cs))
(list
#`((real-binding) #,(fl-subtract #'(cs.real-binding ...)))
#`((imag-binding)
;; can't ignore exact 0 imag parts from real numbers, as with
;; addition, because the first value is special
;; so just conservatively use generic subtraction
#,(if (ormap was-real? (syntax->list #'(cs.imag-binding ...)))
(n-ary->binary
this-syntax
#'-
(for/list ([i (syntax->list #'(cs.imag-binding ...))])
(if (was-real? i) #'0 i)))
(fl-subtract #'(cs.imag-binding ...))))))))
#`((imag-binding) #,(fl-subtract #'(cs.imag-binding ...)))))))
(pattern (#%plain-app op:-^ c1:unboxed-float-complex-opt-expr) ; unary -
#:when (subtypeof? this-syntax -FloatComplex)
#:with (real-binding imag-binding) (binding-names)
@ -294,45 +198,27 @@
#'(cs.imag-binding ...))
(list #'imag-binding))]
[res '()])
(cond
[(null? e1)
(reverse res)]
[else
(define o-real? (was-real? o2))
(define e-real? (was-real? (car e2)))
(define both-real? (and o-real? e-real?))
(define o-nf (as-non-float o1))
(define e-nf (as-non-float (car e1)))
(define new-imag-id (if both-real?
(mark-as-real (car is))
(car is)))
(loop (car rs) new-imag-id (cdr e1) (cdr e2) (cdr rs) (cdr is)
;; complex multiplication, imag part, then real part (reverse)
;; we eliminate operations on the imaginary parts of reals
(list* #`((#,new-imag-id)
#,(cond ((and o-real? e-real?) #'0.0)
(o-real? #`(unsafe-fl* #,o1 #,(car e2)))
(e-real? #`(unsafe-fl* #,o2 #,(car e1)))
(else
#`(unsafe-fl+ (unsafe-fl* #,o2 #,(car e1))
(unsafe-fl* #,o1 #,(car e2))))))
#`((#,(car rs))
#,(cond [(and o-nf e-nf both-real?)
;; we haven't seen float operands yet, so
;; shouldn't prematurely convert to floats
(mark-as-non-float (car rs))
#`(* #,o-nf #,e-nf)]
[(or o-real? e-real?)
#`(unsafe-fl*
#,(if (as-non-float o1)
;; we hit floats, need to coerce
#`(real->double-flonum #,o1)
o1)
#,(car e1))]
[else
#`(unsafe-fl- (unsafe-fl* #,o1 #,(car e1))
(unsafe-fl* #,o2 #,(car e2)))]))
res))])))))
(if (null? e1)
(reverse res)
(loop (car rs) (car is) (cdr e1) (cdr e2) (cdr rs) (cdr is)
;; complex multiplication, imag part, then real part (reverse)
;; we eliminate operations on the imaginary parts of reals
(let ((o-real? (0.0? o2))
(e-real? (0.0? (car e2))))
(list* #`((#,(car is))
#,(cond ((and o-real? e-real?) #'0.0)
(o-real? #`(unsafe-fl* #,o1 #,(car e2)))
(e-real? #`(unsafe-fl* #,o2 #,(car e1)))
(else
#`(unsafe-fl+ (unsafe-fl* #,o2 #,(car e1))
(unsafe-fl* #,o1 #,(car e2))))))
#`((#,(car rs))
#,(cond ((or o-real? e-real?)
#`(unsafe-fl* #,o1 #,(car e1)))
(else
#`(unsafe-fl- (unsafe-fl* #,o1 #,(car e1))
(unsafe-fl* #,o2 #,(car e2))))))
res))))))))
(pattern (#%plain-app op:*^ :unboxed-float-complex-opt-expr)
#:when (subtypeof? this-syntax -FloatComplex)
#:do [(log-unboxing-opt "unboxed unary float complex")])
@ -446,21 +332,10 @@
((real-binding) (unsafe-flreal-part e*))
((imag-binding) (unsafe-flimag-part e*))))
;; The following optimization is incorrect and causes bugs because it turns exact numbers into inexact
(pattern e:number-expr
#:with e* (generate-temporary)
#:with (real-binding* imag-binding*) (binding-names)
#:with real-binding (if (and (subtypeof? #'e -Real)
(not (subtypeof? #'e -Flonum)))
;; values that were originally non-floats (e.g.
;; rationals or single floats) may need to be
;; handled specially
(mark-as-non-float #'real-binding* #'e*)
#'real-binding*)
#:with imag-binding (if (subtypeof? #'e -Real)
;; values that were originally reals may need to be
;; handled specially
(mark-as-real #'imag-binding*)
#'imag-binding*)
#:with (real-binding imag-binding) (binding-names)
#:do [(log-unboxing-opt
(if (subtypeof? #'e -Flonum)
"float in complex ops"
@ -568,13 +443,9 @@
[(#%plain-app op:magnitude^ c:unboxed-float-complex-opt-expr)
(log-unboxing-opt "unboxed unary float complex")
#`(let*-values (c.bindings ...)
;; reuses the algorithm used by the Racket runtime
(let*-values ([(r) (unsafe-flabs c.real-binding)]
[(i) (unsafe-flabs c.imag-binding)]
[(q) (unsafe-fl/ r i)])
(unsafe-fl* i
(unsafe-flsqrt (unsafe-fl+ 1.0
(unsafe-fl* q q))))))])))
(unsafe-flsqrt
(unsafe-fl+ (unsafe-fl* c.real-binding c.real-binding)
(unsafe-fl* c.imag-binding c.imag-binding))))])))
(pattern (#%plain-app op:float-complex-op e:expr ...)

View File

@ -4,7 +4,7 @@
(for-template racket/base)
"../utils/utils.rkt"
(optimizer utils logging)
(types abbrev numeric-tower struct-table))
(types abbrev struct-table))
(provide hidden-cost-log-expr)
@ -45,6 +45,18 @@
#:do [(log-optimization-info "hidden parameter (random)" #'op)]
#:with opt (syntax/loc this-syntax (op args.opt ...)))
;; Log calls to struct constructors, so that OC can report those used in
;; hot loops.
;; Note: Sometimes constructors are wrapped in `#%expression', need to watch
;; for that too.
(pattern (#%plain-app (~and op-part (~or op:id (#%expression op:id)))
args:opt-expr ...)
#:when (let ([constructor-for (syntax-property #'op 'constructor-for)])
(or (and constructor-for (struct-constructor? constructor-for))
(struct-constructor? #'op)))
#:do [(log-optimization-info "struct constructor" #'op)]
#:with opt (syntax/loc this-syntax (op-part args.opt ...)))
;; regexp-match (or other regexp operation) with non-regexp pattern argument
;; (i.e. string or bytes)
(pattern (#%plain-app op:regexp-function pattern-arg:opt-expr
@ -52,12 +64,4 @@
#:when (not (or (subtypeof? #'pattern-arg -Regexp)
(subtypeof? #'pattern-arg -Byte-Regexp)))
#:do [(log-optimization-info "non-regexp pattern" #'pattern-arg)]
#:with opt (syntax/loc this-syntax (op pattern-arg.opt args.opt ...)))
;; vectors of floats can be replaced with flvectors in most cases
;; need to deconstruct to not infinite loop
(pattern (#%plain-app es ...)
#:when (subtypeof? this-syntax (-vec -Flonum))
#:with (es*:opt-expr ...) #'(es ...)
#:do [(log-optimization-info "vector of floats" this-syntax)]
#:with opt (syntax/loc this-syntax (es*.opt ...))))
#:with opt (syntax/loc this-syntax (op pattern-arg.opt args.opt ...))))

View File

@ -24,9 +24,9 @@
(pattern opt:ignore-table^)
;; Can't optimize the body of this code because it isn't typechecked
(pattern (~and (~or _:kw-lambda^ _:opt-lambda^)
((~and op let-values)
([(i:id) e-rhs:opt-expr]) e-body:expr ...))
(pattern (~and _:kw-lambda^
((~and op let-values)
([(i:id) e-rhs:opt-expr]) e-body:expr ...))
#:with opt (quasisyntax/loc/origin this-syntax #'op
(op ([(i) e-rhs.opt]) e-body ...)))

View File

@ -138,7 +138,7 @@
[res #'e.arg])
([accessor (in-list (reverse (syntax->list #'e.alt)))])
(cond
[(and t (subtype t (-pair Univ Univ))) ; safe to optimize this one layer
[(subtype t (-pair Univ Univ)) ; safe to optimize this one layer
(syntax-parse accessor
[op:pair-op
(log-pair-opt)

View File

@ -1,25 +0,0 @@
#lang racket/base
(provide cast-table-ref
cast-table-set!)
(require syntax/id-table)
;; A module that helps store information about the original types of casted
;; expressions.
;;
;; Casts in Typed Racket must generate two contracts. One from typed to untyped,
;; and another from untyped to typed. The contract from typed to untyped is
;; generated based on the existing type of the expression, which must be stored
;; in this table so that it can be looked up later in the contract-generation
;; pass.
(define cast-table (make-free-id-table))
;; cast-table-set! : Id Type-Stx -> Void
(define (cast-table-set! id type-stx)
(free-id-table-set! cast-table id type-stx))
;; cast-table-ref : Id -> (U False Type-Stx)
(define (cast-table-ref id)
(free-id-table-ref cast-table id #f))

View File

@ -1,16 +0,0 @@
#lang racket/base
;; Control whether the OC button show up for TR files in DrR.
(provide maybe-show-OC)
(define (maybe-show-OC)
;; If Optimization Coach is installed, load it.
(with-handlers ([exn:fail:filesystem? (lambda _ '())]) ; not found
(collection-path "optimization-coach")
(if (dynamic-require 'optimization-coach/tool
'optimization-coach-loaded?)
;; OC is loaded, show button
(list (dynamic-require 'optimization-coach/tool
'optimization-coach-drracket-button))
'())))

View File

@ -2,12 +2,11 @@
;; This module provides functions for parsing types written by the user
(require (rename-in "../utils/utils.rkt" [infer infer-in])
(require "../utils/utils.rkt"
(except-in (rep type-rep object-rep) make-arr)
(rename-in (types abbrev union utils prop-ops resolve
(rename-in (types abbrev union utils filter-ops resolve
classes prefab signatures)
[make-arr* make-arr])
(only-in (infer-in infer) intersect)
(utils tc-utils stxclass-util literal-syntax-class)
syntax/stx (prefix-in c: (contract-req))
syntax/parse racket/sequence
@ -109,8 +108,6 @@
(define-literal-syntax-class #:for-label Top)
(define-literal-syntax-class #:for-label Bot)
(define-literal-syntax-class #:for-label Distinction)
(define-literal-syntax-class #:for-label Sequenceof)
(define-literal-syntax-class #:for-label )
;; (Syntax -> Type) -> Syntax Any -> Syntax
;; See `parse-type/id`. This is a curried generalization.
@ -229,7 +226,7 @@
#:attributes (type)
(pattern (~optional (~seq #:rest type:non-keyword-ty))))
;; syntax classes for props, objects, and related things
;; syntax classes for filters, objects, and related things
(define-syntax-class path-elem
#:description "path element"
(pattern :car^
@ -246,8 +243,8 @@
#:description "!"
(pattern (~datum !)))
(define-splicing-syntax-class simple-latent-prop
#:description "latent prop"
(define-splicing-syntax-class simple-latent-filter
#:description "latent filter"
(pattern (~seq t:expr :@ pe:path-elem ...)
#:attr type (parse-type #'t)
#:attr path (attribute pe.pe))
@ -256,54 +253,54 @@
#:attr path '()))
(define-syntax-class (prop doms)
#:description "proposition"
#:description "filter proposition"
#:attributes (prop)
(pattern :Top^ #:attr prop -tt)
(pattern :Bot^ #:attr prop -ff)
(pattern :Top^ #:attr prop -top)
(pattern :Bot^ #:attr prop -bot)
;; Here is wrong check
(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)))
(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))))
;; Here is wrong check
(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 :@ ~! 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)
#:attr prop (-not-type 0 (parse-type #'t)))
#:attr prop (-not-filter (parse-type #'t) 0))
(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 (-or (negate-prop (attribute p1.prop)) (attribute p2.prop)))
#:attr prop (-imp (attribute p1.prop) (attribute p2.prop)))
(pattern t:expr
#:attr prop (-is-type 0 (parse-type #'t))))
#:attr prop (-filter (parse-type #'t) 0)))
(define-splicing-syntax-class (prop-object doms)
#:description "prop object"
(define-splicing-syntax-class (filter-object doms)
#:description "filter object"
#:attributes (obj)
(pattern i:id
#:fail-unless (identifier-binding #'i)
"Propositions for predicates may not reference identifiers that are unbound"
"Filters for predicates may not reference identifiers that are unbound"
#:fail-when (is-var-mutated? #'i)
"Propositions for predicates may not reference identifiers that are mutated"
"Filters 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 "Proposition's object index ~a is larger than argument length ~a"
(format "Filter 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 proposition, but the use is only within ~a enclosing functions"
(format "Index ~a used in a filter, 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 "Proposition's object index ~a is larger than argument length ~a"
(format "Filter proposition's object index ~a is larger than argument length ~a"
depth actual-arg)
#:attr obj (-arg-path arg (syntax-e #'depth-idx))))
@ -468,10 +465,6 @@
t*))))]
[(:U^ ts ...)
(apply Un (parse-types #'(ts ...)))]
[(:∩^ ts ...)
(for/fold ([ty Univ])
([t (in-list (parse-types #'(ts ...)))])
(intersect ty t))]
[(:quote^ t)
(parse-quoted-type #'t)]
[(:All^ . rest)
@ -485,13 +478,6 @@
(-Param ty ty))]
[(:Parameter^ t1 t2)
(-Param (parse-type #'t1) (parse-type #'t2))]
[((~and p :Parameter^) args ...)
(parse-error
#:stx stx
(~a (syntax-e #'p) " expects one or two type arguments, given "
(sub1 (length (syntax->list #'(args ...))))))]
[(:Sequenceof^ t ...)
(apply -seq (parse-types #'(t ...)))]
;; curried function notation
[((~and dom:non-keyword-ty (~not :->^)) ...
:->^
@ -504,9 +490,9 @@
(list (make-arr
doms
(parse-type (syntax/loc stx (rest-dom ...))))))))]
[(~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
[(~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
(with-arity 1
(make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (attribute latent.type)
(-acc-path (attribute latent.path) (-arg-path 0))))]
@ -566,11 +552,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 props from the pred-ty
;; use parse-type instead of parse-values-type because we need to add the filters from the pred-ty
(with-arity (length (syntax->list #'(dom ...)))
(->* (parse-types #'(dom ...))
(parse-type #'rng)
: (-PS (attribute latent.positive) (attribute latent.negative))
: (-FS (attribute latent.positive) (attribute latent.negative))
: (attribute latent.object)))]
[(:->*^ (~var mand (->*-args #t))
(~optional (~var opt (->*-args #f))
@ -606,8 +592,7 @@
(when (current-referenced-aliases)
(define alias-box (current-referenced-aliases))
(set-box! alias-box (cons #'id (unbox alias-box))))
(and (syntax-transforming?)
(add-disappeared-use (syntax-local-introduce #'id)))
(add-disappeared-use (syntax-local-introduce #'id))
t)]
[else
(parse-error #:delayed? #t (~a "type name `" (syntax-e #'id) "' is unbound"))
@ -930,12 +915,11 @@
(define (parse-tc-results stx)
(syntax-parse stx
[((~or :Values^ :values^) t ...)
(define empties (stx-map (λ (x) #f) #'(t ...)))
(ret (parse-types #'(t ...))
empties
empties)]
[:AnyValues^ (tc-any-results #f)]
[t (ret (parse-type #'t) #f #f)]))
(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)]))
(define parse-type/id (parse/id parse-type))

View File

@ -50,10 +50,9 @@
(ignore typechecker:ignore #:mark)
(ignore-some typechecker:ignore-some #:mark)
(ignore-some-expr typechecker:ignore-some)
(contract-def typechecker:contract-def) ; -> Contract-Def (struct in type-contract.rkt)
(contract-def typechecker:contract-def)
(contract-def/provide typechecker:contract-def/provide)
(external-check typechecker:external-check)
(casted-expr typechecker:casted-expr) ; Type -> Void, takes the original type of the casted expr
(with-type typechecker:with-type #:mark)
(type-ascription type-ascription)
(type-inst type-inst)
@ -80,5 +79,5 @@
(tr:unit:invoke tr:unit:invoke)
(tr:unit:invoke:expr tr:unit:invoke:expr)
(tr:unit:compound tr:unit:compound)
(tr:unit:from-context tr:unit:from-context #:mark)
(unsafe-provide unsafe-provide #:mark))
(tr:unit:from-context tr:unit:from-context #:mark))

View File

@ -5,19 +5,19 @@
(require
"../utils/utils.rkt"
syntax/parse
(rep type-rep prop-rep object-rep)
(rep type-rep filter-rep object-rep)
(utils tc-utils)
(env type-name-env row-constraint-env)
(rep rep-utils)
(types resolve union utils printer)
(prefix-in t: (types abbrev numeric-tower subtype))
(prefix-in t: (types abbrev numeric-tower))
(private parse-type syntax-properties)
racket/match racket/syntax racket/list
racket/format
racket/dict racket/set
racket/dict
syntax/flatten-begin
(only-in (types abbrev) -Bottom -Boolean)
(static-contracts instantiate optimize structures combinators constraints)
(only-in (types abbrev) -Bottom)
(static-contracts instantiate optimize structures combinators)
;; TODO make this from contract-req
(prefix-in c: racket/contract)
(contract-req)
@ -39,26 +39,14 @@
;; submod for testing
(module* test-exports #f (provide type->contract))
;; has-contrat-def-property? : Syntax -> Boolean
(define (has-contract-def-property? stx)
(syntax-parse stx
#:literal-sets (kernel-literals)
[(define-values (_) e)
(and (contract-def-property #'e)
#t)]
[_ #f]))
(struct contract-def (type flat? maker? typed-side) #:prefab)
;; get-contract-def-property : Syntax -> (U False Contract-Def)
;; Checks if the given syntax needs to be fixed up for contract generation
;; and if yes it returns the information stored in the property
(define (get-contract-def-property stx)
(syntax-parse stx
#:literal-sets (kernel-literals)
[(define-values (_) e)
(and (contract-def-property #'e)
((contract-def-property #'e)))]
[(define-values (_) e) (contract-def-property #'e)]
[_ #f]))
;; type->contract-fail : Syntax Type #:ctc-str String
@ -123,7 +111,7 @@
(λ (#:reason [reason #f]) (set! failure-reason reason))))
(syntax-parse stx
#:literal-sets (kernel-literals)
[(define-values (ctc-id) _)
[(define-values ctc-id _)
;; no need for ignore, the optimizer doesn't run on this code
(cond [failure-reason
#`(define-syntax (#,untyped-id stx)
@ -134,15 +122,10 @@
"type" #,(pretty-format-type type #:indent 8)))]
[else
(match-define (list defs ctc) result)
(define maybe-inline-val
(should-inline-contract?/cache ctc cache))
#`(begin #,@defs
#,@(if maybe-inline-val
null
(list #`(define-values (ctc-id) #,ctc)))
(define ctc-id #,ctc)
(define-module-boundary-contract #,untyped-id
#,orig-id
#,(or maybe-inline-val #'ctc-id)
#,orig-id ctc-id
#:pos-source #,blame-id
#:srcloc (vector (quote #,(syntax-source orig-id))
#,(syntax-line orig-id)
@ -150,16 +133,6 @@
#,(syntax-position orig-id)
#,(syntax-span orig-id))))])]))
;; Syntax (Dict Static-Contract (Cons Id Syntax)) -> (Option Syntax)
;; A helper for generate-contract-def/provide that helps inline contract
;; expressions when needed to cooperate with the contract system's optimizations
(define (should-inline-contract?/cache ctc-stx cache)
(and (identifier? ctc-stx)
(let ([match? (assoc ctc-stx (hash-values cache) free-identifier=?)])
(and match?
(should-inline-contract? (cdr match?))
(cdr match?)))))
;; The below requires are needed since they provide identifiers that
;; may appear in the residual program.
@ -174,8 +147,6 @@
typed-racket/utils/opaque-object
typed-racket/utils/evt-contract
typed-racket/utils/sealing-contract
typed-racket/utils/promise-not-name-contract
typed-racket/utils/simple-result-arrow
racket/sequence
racket/contract/parametric))
@ -190,7 +161,7 @@
(define sc-cache (make-hash))
(with-new-name-tables
(for/list ((e (in-list forms)))
(if (not (has-contract-def-property? e))
(if (not (get-contract-def-property e))
e
(begin (set-box! include-extra-requires? #t)
(generate-contract-def e ctc-cache sc-cache))))))
@ -216,15 +187,6 @@
ctc-cache sc-cache)))]
[_ form]))))
;; get-max-contract-kind
;; static-contract -> (or/c 'flat 'chaperone 'impersonator)
;; recurse into a contract finding the max
;; kind (e.g. flat < chaperone < impersonator)
(define (get-max-contract-kind sc)
(define (get-restriction sc)
(sc->constraints sc get-restriction))
(kind-max-max (contract-restrict-value (get-restriction sc))))
;; To avoid misspellings
(define impersonator-sym 'impersonator)
(define chaperone-sym 'chaperone)
@ -399,32 +361,6 @@
(if numeric-sc
(apply or/sc numeric-sc (map t->sc non-numeric))
(apply or/sc (map t->sc elems)))]
[(Intersection: ts)
(define-values (chaperones/impersonators others)
(for/fold ([cs/is null] [others null])
([elem (in-immutable-set ts)])
(define c (t->sc elem))
(if (equal? flat-sym (get-max-contract-kind c))
(values cs/is (cons c others))
(values (cons c cs/is) others))))
(cond
[(> (length chaperones/impersonators) 1)
(fail #:reason (~a "Intersection type contract contains"
" more than 1 non-flat contract: "
type))]
[else
(apply and/sc (append others chaperones/impersonators))])]
[(and t (Function: arrs))
#:when (any->bool? arrs)
;; Avoid putting (-> any T) contracts on struct predicates (where Boolean <: T)
;; Optimization: if the value is typed, we can assume it's not wrapped
;; in a type-unsafe chaperone/impersonator and use the unsafe contract
(let* ([unsafe-spp/sc (flat/sc #'struct-predicate-procedure?)]
[safe-spp/sc (flat/sc #'struct-predicate-procedure?/c)]
[optimized/sc (if (from-typed? typed-side)
unsafe-spp/sc
safe-spp/sc)])
(or/sc optimized/sc (t->sc/fun t)))]
[(and t (Function: _)) (t->sc/fun t)]
[(Set: t) (set/sc (t->sc t))]
[(Sequence: ts) (apply sequence/sc (map t->sc ts))]
@ -619,14 +555,7 @@
[(Syntax: t)
(syntax/sc (t->sc t))]
[(Value: v)
(if (and (c:flat-contract? v)
;; numbers used as contracts compare with =, but TR
;; requires an equal? check
(not (number? v))
;; regexps don't match themselves when used as contracts
(not (regexp? v)))
(flat/sc #`(quote #,v))
(flat/sc #`(flat-named-contract '#,v (lambda (x) (equal? x '#,v))) v))]
(flat/sc #`(flat-named-contract '#,v (lambda (x) (equal? x '#,v))) v)]
[(Param: in out)
(parameter/sc (t->sc in) (t->sc out))]
[(Hashtable: k v)
@ -649,21 +578,17 @@
;; and call the given thunk or raise an error
(define (handle-range arr convert-arr)
(match arr
;; functions with no props or objects
[(arr: dom (Values: (list (Result: rngs
(PropSet: (TrueProp:)
(TrueProp:))
(Empty:)) ...))
rst drst kws)
;; functions with no filters or objects
[(arr: dom (Values: (list (Result: rngs (FilterSet: (Top:) (Top:)) (Empty:)) ...)) rst drst kws)
(convert-arr)]
;; Functions that don't return
[(arr: dom (Values: (list (Result: (== -Bottom) _ _) ...)) rst drst kws)
(convert-arr)]
;; functions with props or objects
;; functions with filters 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 props or objects."))
" with filters or objects."))
(convert-arr))]
[(arr: dom (? ValuesDots?) rst drst kws)
(fail #:reason (~a "cannot generate contract for function type"
@ -705,7 +630,7 @@
(map conv opt-kws))))
(define range (map t->sc rngs))
(define rest (and rst (listof/sc (t->sc/neg rst))))
(function/sc (from-typed? typed-side) (process-dom mand-args) opt-args mand-kws opt-kws rest range))
(function/sc (process-dom mand-args) opt-args mand-kws opt-kws rest range))
(handle-range first-arr convert-arr)]
[else
(define ((f case->) a)
@ -722,7 +647,6 @@
(and rst (listof/sc (t->sc/neg rst)))
(map t->sc rngs))
(function/sc
(from-typed? typed-side)
(process-dom (map t->sc/neg dom))
null
(map conv mand-kws)
@ -837,7 +761,7 @@
(let/ec escape
(let loop ([type type])
(type-case
(#:Type loop #:Prop (sub-f loop) #:Object (sub-o loop))
(#:Type loop #:Filter (sub-f loop) #:Object (sub-o loop))
type
[#:App arg _ _
(match arg
@ -845,15 +769,6 @@
[_ type])]))
#f))
;; True if the arities `arrs` are what we'd expect from a struct predicate
(define (any->bool? arrs)
(match arrs
[(list (arr: (list (Univ:))
(Values: (list (Result: t _ _)))
#f #f '()))
(t:subtype -Boolean t)]
[_ #f]))
(module predicates racket/base
(require racket/extflonum)
(provide nonnegative? nonpositive?

View File

@ -154,11 +154,10 @@
(define (type-stxs->ids+defs type-stxs typed-side)
(for/lists (_1 _2) ([t (in-list type-stxs)])
(define ctc-id (generate-temporary))
(define contract-def `#s(contract-def ,t #f #f ,typed-side))
(values ctc-id
#`(define-values (#,ctc-id)
#,(contract-def-property
#'#f (λ () contract-def))))))
#'#f `#s(contract-def ,t #f #f ,typed-side))))))
(define (wt-core stx)
(define-syntax-class typed-id

View File

@ -1,4 +1,67 @@
#lang racket/base
(require "prop-rep.rkt")
(provide (all-from-out "prop-rep.rkt"))
;;TODO use contract-req
(require "rep-utils.rkt" "free-variance.rkt" racket/contract/base
racket/lazy-require)
;; TODO use something other than lazy-require.
(lazy-require ["type-rep.rkt" (Type/c Univ? Bottom?)]
["object-rep.rkt" (Path?)])
(provide Filter/c FilterSet/c name-ref/c hash-name filter-equal?)
(define (Filter/c-predicate? e)
(and (Filter? e) (not (NoFilter? e)) (not (FilterSet? e))))
(define Filter/c (flat-named-contract 'Filter Filter/c-predicate?))
(define 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 name-ref/c (or/c identifier? (list/c integer? integer?)))
(define (hash-name v) (if (identifier? v) (hash-id v) (list v)))
(define ((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)))

View File

@ -5,7 +5,7 @@
;;
;; See "Logical Types for Untyped Languages" pg.3
(require "rep-utils.rkt" "free-variance.rkt" "prop-rep.rkt" "../utils/utils.rkt" (contract-req))
(require "rep-utils.rkt" "free-variance.rkt" "filter-rep.rkt" "../utils/utils.rkt" (contract-req))
(provide object-equal?)
(def-pathelem CarPE () [#:fold-rhs #:base])
@ -25,4 +25,16 @@
[#: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)])
|#

View File

@ -1,56 +0,0 @@
#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)))

View File

@ -7,6 +7,7 @@
"interning.rkt"
racket/lazy-require
racket/stxparam
racket/unsafe/ops
(for-syntax
racket/match
(except-in syntax/parse id identifier keyword)
@ -20,7 +21,7 @@
(lazy-require
["../types/printer.rkt" (print-type print-prop print-object print-pathelem)])
["../types/printer.rkt" (print-type print-filter print-object print-pathelem)])
(provide == defintern hash-id (for-syntax fold-target))
@ -32,9 +33,9 @@
(define-struct Rep (seq free-vars free-idxs stx) #:transparent
#:methods gen:equal+hash
[(define (equal-proc x y recur)
(eq? (Rep-seq x) (Rep-seq y)))
(define (hash-proc x recur) (Rep-seq x))
(define (hash2-proc x recur) (Rep-seq x))])
(eq? (unsafe-Rep-seq x) (unsafe-Rep-seq y)))
(define (hash-proc x recur) (unsafe-Rep-seq x))
(define (hash2-proc x recur) (unsafe-Rep-seq x))])
;; evil tricks for hygienic yet unhygienic-looking reference
;; in say def-type for type-ref-id
@ -135,7 +136,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/prop/etc.'s
;; This tricky beast is for defining the type/filter/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 +205,7 @@
provides))])))
;; rec-ids are identifiers that are of the folded type, so we recur on them.
;; kws is e.g. '(#:Type #:Prop #:Object #:PathElem)
;; kws is e.g. '(#:Type #:Filter #:Object #:PathElem)
(define-for-syntax (mk-fold hashtable rec-ids kws)
(lambda (stx)
(define new-hashtable (make-hasheq))
@ -217,7 +218,7 @@
(syntax/loc this-syntax (pats ...))
(lambda () #'e)
this-syntax))
;; Match on a type (or prop etc) case with keyword k
;; Match on a type (or filter 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 +352,23 @@
;; [unsyntax (*1)]
(mk-fold ht
rec-ids
;; '(#:Type #:Prop #:Object #:PathElem)
;; '(#:Type #:Filter #: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]
[Prop def-prop #:Prop prop-case print-prop prop-name-ht prop-rec-id]
[Filter def-filter #:Filter filter-case print-filter filter-name-ht filter-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])
;; NOTE: change these if the definitions above change, or everything will segfault
(define-syntax-rule (unsafe-Rep-seq v) (unsafe-struct*-ref v 0))
(define-syntax-rule (unsafe-Type-key v) (unsafe-struct*-ref v 4))
(provide unsafe-Rep-seq unsafe-Type-key)
(define (Rep-values rep)
(match rep
[(? (lambda (e) (or (Prop? e)
[(? (lambda (e) (or (Filter? e)
(Object? e)
(PathElem? e)))
(app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx vals)))
@ -386,7 +392,7 @@
(provide/cond-contract
[rename rep-equal? type-equal? (Type? Type? . -> . boolean?)]
[rename rep<? type<? (Type? Type? . -> . boolean?)]
[rename rep<? prop<? (Prop? Prop? . -> . boolean?)]
[rename rep<? filter<? (Filter? Filter? . -> . boolean?)]
[struct Rep ([seq exact-nonnegative-integer?]
[free-vars (hash/c symbol? variance?)]
[free-idxs (hash/c symbol? variance?)]

View File

@ -7,8 +7,8 @@
;; TODO use contract-req
(require (utils tc-utils)
"rep-utils.rkt" "object-rep.rkt" "prop-rep.rkt" "free-variance.rkt"
racket/match racket/list racket/set
"rep-utils.rkt" "object-rep.rkt" "filter-rep.rkt" "free-variance.rkt"
racket/match racket/list
racket/contract
racket/lazy-require
racket/promise
@ -19,11 +19,10 @@
PolyDots-names:
PolyRow-names: PolyRow-fresh:
Type-seq
-unsafe-intersect
Mu-unsafe: Poly-unsafe:
PolyDots-unsafe:
Mu? Poly? PolyDots? PolyRow?
Prop? Object?
Filter? Object?
Type/c Type/c?
Values/c SomeValues/c
Bottom?
@ -54,15 +53,15 @@
;; Ugly hack - should use units
(lazy-require
("../types/union.rkt" (Un))
("../types/overlap.rkt" (overlap?))
("../types/resolve.rkt" (resolve-app)))
("../types/union.rkt" (Un))
("../types/resolve.rkt" (resolve-app)))
(define name-table (make-weak-hasheq))
(define Type/c?
(λ (e)
(and (Type? e)
(not (Scope? e))
(not (arr? e))
(not (fld? e))
(not (Values? e))
@ -76,6 +75,7 @@
(define Values/c?
(λ (e)
(and (Type? e)
(not (Scope? e))
(not (arr? e))
(not (fld? e))
(not (ValuesDots? e))
@ -93,6 +93,19 @@
;; Type is defined in rep-utils.rkt
;; t must be a Type
(def-type Scope ([t (or/c Type/c Scope?)]) [#:key (Type-key t)])
(define (scope-depth k)
(flat-named-contract
(format "Scope of depth ~a" k)
(lambda (sc)
(define (f k sc)
(cond [(= 0 k) (Type/c? sc)]
[(not (Scope? sc)) #f]
[else (f (sub1 k) (Scope-t sc))]))
(f k sc))))
;; this is ONLY used when a type error ocurrs
(def-type Error () [#:frees #f] [#:fold-rhs #:base])
@ -226,43 +239,48 @@
[(Keyword) 'keyword]
[else #f]))])
(def-type Mu ([body Type/c]) #:no-provide [#:frees (λ (f) (f body))]
[#:fold-rhs (*Mu (type-rec-id body))]
;; body is a Scope
(def-type Mu ([body (scope-depth 1)]) #:no-provide [#:frees (λ (f) (f body))]
[#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))]
[#:key (Type-key body)])
;; n is how many variables are bound here
;; body is a type
;; body is a Scope
(def-type Poly (n body) #:no-provide
[#:contract (->i ([n natural-number/c]
[body Type/c])
[#:contract (->i ([n natural-number/c]
[body (n) (scope-depth n)])
(#:syntax [stx (or/c #f syntax?)])
[result Poly?])]
[#:frees (λ (f) (f body))]
[#:fold-rhs (*Poly n (type-rec-id body))]
[#:fold-rhs (let ([body* (remove-scopes n body)])
(*Poly n (add-scopes n (type-rec-id body*))))]
[#:key (Type-key body)])
;; n is how many variables are bound here
;; there are n-1 'normal' vars and 1 ... var
;; body is a Scope
(def-type PolyDots (n body) #:no-provide
[#:contract (->i ([n natural-number/c]
[body Type/c])
[body (n) (scope-depth n)])
(#:syntax [stx (or/c #f syntax?)])
[result PolyDots?])]
[#:key (Type-key body)]
[#:frees (λ (f) (f body))]
[#:fold-rhs (*PolyDots n (type-rec-id body))])
[#:fold-rhs (let ([body* (remove-scopes n body)])
(*PolyDots n (add-scopes n (type-rec-id body*))))])
;; interp. A row polymorphic function type
;; constraints are row absence constraints, represented
;; as a set for each of init, field, methods
(def-type PolyRow (constraints body) #:no-provide
[#:contract (->i ([constraints (list/c list? list? list? list?)]
[body Type/c])
[body (scope-depth 1)])
(#:syntax [stx (or/c #f syntax?)])
[result PolyRow?])]
[#:frees (λ (f) (f body))]
[#:fold-rhs (*PolyRow constraints
(type-rec-id body))]
[#:fold-rhs (let ([body* (remove-scopes 1 body)])
(*PolyRow constraints
(add-scopes 1 (type-rec-id body*))))]
[#:key (Type-key body)])
;; pred : identifier
@ -276,9 +294,9 @@
[#:frees (λ (f) (f ty))]
[#:fold-rhs (*Keyword kw (type-rec-id ty) required?)])
(def-type Result ([t Type/c] [f PropSet?] [o Object?])
(def-type Result ([t Type/c] [f FilterSet?] [o Object?])
[#:frees (λ (frees) (combine-frees (map frees (list t f o))))]
[#:fold-rhs (*Result (type-rec-id t) (prop-rec-id f) (object-rec-id o))])
[#:fold-rhs (*Result (type-rec-id t) (filter-rec-id f) (object-rec-id o))])
(def-type Values ([rs (listof Result?)])
[#:intern (map Rep-seq rs)]
@ -286,7 +304,7 @@
[#:fold-rhs (*Values (map type-rec-id rs))])
(def-type AnyValues ([f Prop?])
(def-type AnyValues ([f Filter/c])
[#:fold-rhs #:base])
(def-type ValuesDots ([rs (listof Result?)] [dty Type/c] [dbound (or/c symbol? natural-number/c)])
@ -451,55 +469,6 @@
(define d* (remove-duplicates d))
(if (and (pair? d*) (null? (cdr d*))) (car d*) d*))])
;; Intersection
(def-type Intersection ([elems (and/c (set/c Type/c)
(λ (s) (>= (set-count s) 2)))])
[#:intern (for/set ([e (in-immutable-set elems)])
(Rep-seq e))]
[#:frees (λ (f) (combine-frees (for/list ([elem (in-immutable-set elems)])
(f elem))))]
[#:fold-rhs (let ([elems (for/list ([elem (in-immutable-set elems)])
(type-rec-id elem))])
(apply -unsafe-intersect elems))]
[#:key (let ()
(define d
(let loop ([ts (set->list elems)] [res null])
(cond [(null? ts) res]
[else
(define k (Type-key (car ts)))
(cond [(not k) (list #f)]
[(pair? k) (loop (cdr ts) (append k res))]
[else (loop (cdr ts) (cons k res))])])))
(define d* (remove-duplicates d))
(if (and (pair? d*) (null? (cdr d*))) (car d*) d*))])
;; constructor for intersections
;; in general, intersections should be built
;; using the 'intersect' operator, which worries
;; about actual subtyping, etc...
(define (-unsafe-intersect . ts)
(let loop ([elems (set)]
[ts ts])
(match ts
[(list)
(cond
[(set-empty? elems) (Univ)]
;; size = 1 ?
[(= 1 (set-count elems)) (set-first elems)]
;; size > 1, build an intersection
[else (*Intersection elems)])]
[(cons t ts)
(match t
[(? Bottom?) t]
[(Univ:) (loop elems ts)]
[(Intersection: ts*) (loop (set-union elems ts*) ts)]
[t (cond
[(for/or ([elem (in-immutable-set elems)]) (not (overlap? elem t)))
(*Union (list))]
[else (loop (set-add elems t) ts)])])])))
(def-type Univ () [#:frees #f] [#:fold-rhs #:base])
;; in : Type
@ -667,11 +636,24 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (add-scopes n t)
(if (zero? n) t
(add-scopes (sub1 n) (*Scope t))))
(define (remove-scopes n sc)
(if (zero? n)
sc
(match sc
[(Scope: sc*) (remove-scopes (sub1 n) sc*)]
[_ (int-err "Tried to remove too many scopes: ~a" sc)])))
(define ((sub-f st) e)
(prop-case (#:Type st
#:Prop (sub-f st)
#:PathElem (sub-pe st))
e))
(filter-case (#:Type st
#:Filter (sub-f st)
#:PathElem (sub-pe st))
e))
(define ((sub-o st) e)
@ -687,11 +669,11 @@
(define ((sub-t st) e)
(type-case (#:Type st
#:Prop (sub-f st))
#:Filter (sub-f st))
e))
;; abstract-many : Names Type -> Type
;; abstract-many : Names Type -> Scope^n
;; where n is the length of names
(define (abstract-many names ty)
;; mapping : dict[Type -> Natural]
@ -708,7 +690,7 @@
(f (+ (cdr pr) outer)))]
[else default]))
(type-case
(#:Type sb #:Prop (sub-f sb) #:Object (sub-o sb))
(#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb))
ty
[#:F name* (transform name* *B ty)]
;; necessary to avoid infinite loops
@ -731,23 +713,27 @@
[#:ListDots dty dbound
(*ListDots (sb dty)
(transform dbound values dbound))]
[#:Mu body (*Mu (loop (add1 outer) body))]
[#:PolyRow constraints body
(*PolyRow constraints (loop (+ 1 outer) body))]
[#:PolyDots n body
(*PolyDots n (loop (+ n outer) body))]
[#:Poly n body
(*Poly n (loop (+ n outer) body))])))
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
[#:PolyRow constraints body*
(let ([body (remove-scopes 1 body*)])
(*PolyRow constraints
(add-scopes 1 (loop (+ 1 outer) body))))]
[#:PolyDots n body*
(let ([body (remove-scopes n body*)])
(*PolyDots n (add-scopes n (loop (+ n outer) body))))]
[#:Poly n body*
(let ([body (remove-scopes n body*)])
(*Poly n (add-scopes n (loop (+ n outer) body))))])))
(define n (length names))
(define mapping (for/list ([nm (in-list names)]
[i (in-range n 0 -1)])
(cons nm (sub1 i))))
(nameTo mapping ty))
(add-scopes n (nameTo mapping ty)))
;; instantiate-many : List[Type] Type -> Type
;; instantiate-many : List[Type] Scope^n -> Type
;; where n is the length of types
;; all of the types MUST be Fs
(define (instantiate-many images ty)
(define (instantiate-many images sc)
;; mapping : dict[Natural -> Type]
(define (replace mapping type)
(let loop ([outer 0] [ty type])
@ -762,7 +748,7 @@
(define (sb t) (loop outer t))
(define sf (sub-f sb))
(type-case
(#:Type sb #:Prop sf #:Object (sub-o sb))
(#:Type sb #:Filter sf #:Object (sub-o sb))
ty
[#:B idx (transform idx values ty)]
;; necessary to avoid infinite loops
@ -784,18 +770,21 @@
[#:ListDots dty dbound
(*ListDots (sb dty)
(transform dbound F-n dbound))]
[#:Mu body (*Mu (loop (add1 outer) body))]
[#:PolyRow constraints body
(*PolyRow constraints (loop (+ 1 outer) body))]
[#:PolyDots n body
(*PolyDots n (loop (+ n outer) body))]
[#:Poly n body
(*Poly n (loop (+ n outer) body))])))
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
[#:PolyRow constraints body*
(let ([body (remove-scopes 1 body*)])
(*PolyRow constraints (add-scopes 1 (loop (+ 1 outer) body))))]
[#:PolyDots n body*
(let ([body (remove-scopes n body*)])
(*PolyDots n (add-scopes n (loop (+ n outer) body))))]
[#:Poly n body*
(let ([body (remove-scopes n body*)])
(*Poly n (add-scopes n (loop (+ n outer) body))))])))
(define n (length images))
(define mapping (for/list ([img (in-list images)]
[i (in-range n 0 -1)])
(cons (sub1 i) img)))
(replace mapping ty))
(replace mapping (remove-scopes n sc)))
(define (abstract name ty)
(abstract-many (list name) ty))
@ -812,8 +801,8 @@
;; the 'smart' destructor
(define (Mu-body* name t)
(match t
[(Mu: body)
(instantiate (*F name) body)]))
[(Mu: scope)
(instantiate (*F name) scope)]))
;; the 'smart' constructor
;;
@ -836,10 +825,10 @@
;; the 'smart' destructor
(define (Poly-body* names t)
(match t
[(Poly: n body)
[(Poly: n scope)
(unless (= (length names) n)
(int-err "Wrong number of names: expected ~a got ~a" n (length names)))
(instantiate-many (map *F names) body)]))
(instantiate-many (map *F names) scope)]))
;; the 'smart' constructor
(define (PolyDots* names body)
@ -851,10 +840,10 @@
;; the 'smart' destructor
(define (PolyDots-body* names t)
(match t
[(PolyDots: n body)
[(PolyDots: n scope)
(unless (= (length names) n)
(int-err "Wrong number of names: expected ~a got ~a" n (length names)))
(instantiate-many (map *F names) body)]))
(instantiate-many (map *F names) scope)]))
;; Constructor and destructor for row polymorphism
;;
@ -869,15 +858,15 @@
(define (PolyRow-body* names t)
(match t
[(PolyRow: constraints body)
(instantiate-many (map *F names) body)]))
[(PolyRow: constraints scope)
(instantiate-many (map *F names) scope)]))
(print-struct #t)
(define-match-expander Mu-unsafe:
(lambda (stx)
(syntax-case stx ()
[(_ bp) #'(? Mu? (app (lambda (t) (Mu-body t)) bp))])))
[(_ bp) #'(? Mu? (app (lambda (t) (Scope-t (Mu-body t))) bp))])))
(define-match-expander Poly-unsafe:
(lambda (stx)

View File

@ -28,8 +28,7 @@
[(define (sc-map v f) v)
(define (sc-traverse v f) (void))
(define (sc->contract v f) #'any/c)
(define (sc->constraints v f) (simple-contract-restrict 'flat))
(define (sc-terminal-kind v) 'flat)]
(define (sc->constraints v f) (simple-contract-restrict 'flat))]
#:methods gen:custom-write [(define write-proc any-write-proc)])
(define-match-expander any/sc:

View File

@ -6,13 +6,12 @@
(require "../structures.rkt" "../constraints.rkt"
racket/list racket/match
racket/contract
(for-template racket/base racket/contract/base "../../utils/simple-result-arrow.rkt")
(for-template racket/base racket/contract/base)
(for-syntax racket/base syntax/parse))
(provide
(contract-out
[function/sc (-> boolean?
(listof static-contract?)
[function/sc (-> (listof static-contract?)
(listof static-contract?)
(listof (list/c keyword? static-contract?))
(listof (list/c keyword? static-contract?))
@ -22,7 +21,7 @@
->/sc:)
(struct function-combinator combinator (indices mand-kws opt-kws typed-side?)
(struct function-combinator combinator (indices mand-kws opt-kws)
#:property prop:combinator-name "->/sc"
#:methods gen:equal+hash [(define (equal-proc a b recur) (function-sc-equal? a b recur))
(define (hash-proc v recur) (function-sc-hash v recur))
@ -31,7 +30,6 @@
[(define (sc->contract v f) (function-sc->contract v f))
(define (sc-map v f) (function-sc-map v f))
(define (sc-traverse v f) (function-sc-map v f) (void))
(define (sc-terminal-kind v) (function-sc-terminal-kind v))
(define (sc->constraints v f) (function-sc-constraints v f))])
(define (split-function-args ctcs mand-args-end opt-args-end
@ -46,10 +44,7 @@
(and range-end (drop (take ctcs range-end) rest-end))))
(define (function-sc->contract sc recur)
(match-define (function-combinator args indices mand-kws opt-kws typed-side?) sc)
(define-values (mand-scs opt-scs mand-kw-scs opt-kw-scs rest-sc range-scs)
(apply split-function-args args indices))
(match-define (function-combinator args indices mand-kws opt-kws) sc)
(define-values (mand-ctcs opt-ctcs mand-kw-ctcs opt-kw-ctcs rest-ctc range-ctcs)
(apply split-function-args (map recur args) indices))
@ -66,24 +61,14 @@
#`(values #,@range-ctcs)
#'any))
(cond
[(and (null? mand-kws) (null? opt-kws)
(null? opt-ctcs)
(not rest-ctc)
;; currently simple-result-> only handles up to arity 3
(member (length mand-ctcs) '(0 1 2 3))
(and range-ctcs (= 1 (length range-ctcs)))
(for/and ([a args]) (eq? 'flat (sc-terminal-kind a)))
(not typed-side?))
#`(simple-result-> #,@range-ctcs #,(length mand-ctcs))]
[else
#`((#,@mand-ctcs #,@mand-kws-stx)
(#,@opt-ctcs #,@opt-kws-stx)
#,@rest-ctc-stx
. ->* . #,range-ctc)]))
#`((#,@mand-ctcs #,@mand-kws-stx)
(#,@opt-ctcs #,@opt-kws-stx)
#,@rest-ctc-stx
. ->* . #,range-ctc))
(define (function/sc typed-side? mand-args opt-args mand-kw-args opt-kw-args rest range)
(define (function/sc mand-args opt-args mand-kw-args opt-kw-args rest range)
(define mand-args-end (length mand-args))
(define opt-args-end (+ mand-args-end (length opt-args)))
(define mand-kw-args-end (+ opt-args-end (length mand-kw-args)))
@ -105,15 +90,14 @@
(or range null))
end-indices
mand-kws
opt-kws
typed-side?))
opt-kws))
(define-match-expander ->/sc:
(syntax-parser
[(_ mand-args opt-args mand-kw-args opt-kw-args rest range)
#'(and (? function-combinator?)
(app (match-lambda
[(function-combinator args indices mand-kws opt-kws typed-side?)
[(function-combinator args indices mand-kws opt-kws)
(define-values (mand-args* opt-args* mand-kw-args* opt-kw-args* rest* range*)
(apply split-function-args args indices))
(list
@ -125,13 +109,13 @@
(list mand-args opt-args mand-kw-args opt-kw-args rest range)))]))
(define (function-sc-map v f)
(match-define (function-combinator args indices mand-kws opt-kws typed-side?) v)
(match-define (function-combinator args indices mand-kws opt-kws) v)
(define-values (mand-args opt-args mand-kw-args opt-kw-args rest-arg range-args)
(apply split-function-args args indices))
(define new-args
(append
(append
(map (lambda (arg) (f arg 'contravariant))
(append mand-args opt-args mand-kw-args opt-kw-args (if rest-arg (list rest-arg) null)))
(if range-args
@ -140,49 +124,26 @@
empty)))
(function-combinator new-args indices mand-kws opt-kws typed-side?))
(define (function-sc-terminal-kind v)
(match-define (function-combinator args indices mand-kws opt-kws typed-side?) v)
(define-values (mand-args opt-args mand-kw-args opt-kw-args rest-arg range-args)
(apply split-function-args args indices))
(if (and (not rest-arg)
(null? (append mand-kw-args mand-args opt-kw-args opt-args))
typed-side?)
;; currently we only handle this trivial case
;; we could probably look at the actual kind of `range-args` as well
(if (not range-args) 'flat #f)
#f))
(function-combinator new-args indices mand-kws opt-kws))
(define (function-sc-constraints v f)
(match-define (function-combinator args indices mand-kws opt-kws typed-side?) v)
(define-values (mand-args opt-args mand-kw-args opt-kw-args rest-arg range-args)
(apply split-function-args args indices))
(if (and (not rest-arg)
(null? (append mand-kw-args mand-args opt-kw-args opt-args))
typed-side?)
;; arity-0 functions end up being flat contracts when they're
;; from the typed side and the result is flat
(if range-args
(merge-restricts* 'flat (map f range-args))
(merge-restricts* 'flat null))
(merge-restricts* 'chaperone (map f args))))
(match-define (function-combinator args indices mand-kws opt-kws) v)
(merge-restricts* 'chaperone (map f args)))
(define (function-sc-equal? a b recur)
(match-define (function-combinator a-args a-indices a-mand-kws a-opt-kws a-typed-side?) a)
(match-define (function-combinator b-args b-indices b-mand-kws b-opt-kws b-typed-side?) b)
(match-define (function-combinator a-args a-indices a-mand-kws a-opt-kws) a)
(match-define (function-combinator b-args b-indices b-mand-kws b-opt-kws) b)
(and
(equal? a-typed-side? b-typed-side?)
(recur a-indices b-indices)
(recur a-mand-kws b-mand-kws)
(recur a-opt-kws b-opt-kws)
(recur a-args b-args)))
(define (function-sc-hash v recur)
(match-define (function-combinator v-args v-indices v-mand-kws v-opt-kws typed-side?) v)
(match-define (function-combinator v-args v-indices v-mand-kws v-opt-kws) v)
(+ (recur v-indices) (recur v-mand-kws) (recur v-opt-kws) (recur v-args)))
(define (function-sc-hash2 v recur)
(match-define (function-combinator v-args v-indices v-mand-kws v-opt-kws typed-side?) v)
(match-define (function-combinator v-args v-indices v-mand-kws v-opt-kws) v)
(+ (recur v-indices) (recur v-mand-kws) (recur v-opt-kws) (recur v-args)))

View File

@ -33,25 +33,6 @@
(struct simple-contract static-contract (syntax kind name)
#:transparent
#:methods gen:equal+hash
[(define (equal-proc s1 s2 recur)
(and ;; only check s-expression equality because it's
;; unlikely that TR will compile contracts that are
;; s-exp equal but aren't actually the same contract
(recur (syntax->datum (simple-contract-syntax s1))
(syntax->datum (simple-contract-syntax s2)))
(recur (simple-contract-kind s1)
(simple-contract-kind s2))
(recur (simple-contract-name s1)
(simple-contract-name s2))))
(define (hash-proc sc hash-code)
(hash-code (list (syntax->datum (simple-contract-syntax sc))
(simple-contract-kind sc)
(simple-contract-name sc))))
(define (hash2-proc sc hash-code)
(hash-code (list (syntax->datum (simple-contract-syntax sc))
(simple-contract-kind sc)
(simple-contract-name sc))))]
#:methods gen:sc
[(define (sc-map v f) v)
(define (sc-traverse v f) (void))

View File

@ -15,8 +15,7 @@
racket/async-channel
racket/sequence
racket/promise
"../../utils/evt-contract.rkt"
"../../utils/promise-not-name-contract.rkt")
"../../utils/evt-contract.rkt")
racket/contract
racket/async-channel)
@ -154,7 +153,7 @@
((set/sc (#:covariant #:chaperone)) set/c #:flat)
((vector/sc . (#:invariant)) vector/c #:chaperone)
((vectorof/sc (#:invariant)) vectorof #:chaperone)
((promise/sc (#:covariant)) promise-not-name/c #:chaperone)
((promise/sc (#:covariant)) (λ (x) (and/c (promise/c x) (not/c promise/name?))) #:chaperone)
((syntax/sc (#:covariant #:flat)) syntax/c #:flat)
((hash/sc (#:invariant #:flat) (#:invariant)) hash/c #:chaperone)
((box/sc (#:invariant)) box/c #:chaperone)

View File

@ -61,8 +61,7 @@
contract-restrict-recursive-values
contract-restrict?
contract-restrict-value
kind-max-max)
)
(module structs racket/base
(require racket/contract

View File

@ -23,8 +23,7 @@
[instantiate
(parametric->/c (a) ((static-contract? (-> #:reason (or/c #f string?) a))
(contract-kind? #:cache hash?)
. ->* . (or/c a (list/c (listof syntax?) syntax?))))]
[should-inline-contract? (-> syntax? boolean?)]))
. ->* . (or/c a (list/c (listof syntax?) syntax?))))]))
;; Providing these so that tests can work directly with them.
(module* internals #f
@ -48,42 +47,9 @@
(contract-restrict-recursive-values (compute-constraints sc kind)))
cache))))
;; computes the definitions that are in / used by `sc`
;; `(get-all-name-defs)` is not what we want directly, since it also includes
;; definitions that were optimized away
;; we restrict it to only variables bound in `sc`
(define (compute-defs sc)
(define all-name-defs (get-all-name-defs))
;; all-name-defs maps lists of ids to defs
;; we want to match if any id in the list matches
(define (ref b) (for/first ([(k v) (in-dict all-name-defs)]
#:when (for/or ([k* (in-list k)])
(free-identifier=? b k*)))
(cons k v)))
(define bound '())
;; ignores its second argument (variance, passed by sc-traverse)
(let loop ([sc sc] [_ #f])
(match sc
[(name/sc: name*)
(unless (member name* bound free-identifier=?)
(set! bound (cons name* bound))
;; traverse what `name` refers to
(define r (ref name*))
;; ref returns a rib, get the one definition we want
(define target (for/first ([k (car r)]
[v (cdr r)]
#:when (free-identifier=? name* k))
v))
(loop target #f))]
[else (sc-traverse sc loop)]))
(for*/hash ([b (in-list bound)]
[v (in-value (ref b))]
#:when v)
(values (car v) (cdr v))))
(define (compute-constraints sc max-kind)
(define memo-table (make-hash))
(define name-defs (compute-defs sc))
(define name-defs (get-all-name-defs))
(define (recur sc)
(cond [(hash-ref memo-table sc #f)]
[else
@ -130,9 +96,7 @@
(define bound-names (make-parameter null))
;; sc-queue : records the order in which to return syntax objects
(define sc-queue null)
;; top-level? is #t only for the first call and not for recursive
;; calls, which helps for inlining
(define (recur sc [top-level? #f])
(define (recur sc)
(cond [(and cache (hash-ref cache sc #f)) => car]
[(arr/sc? sc) (make-contract sc)]
[(or (parametric->/sc? sc) (sealing->/sc? sc))
@ -147,14 +111,7 @@
(make-contract sc)]
[else
(define ctc (make-contract sc))
(cond [(and ;; when a contract benefits from inlining
;; (e.g., ->) and this contract appears
;; directly in a define-module-boundary-contract
;; position (i.e, top-level? is #t) then
;; don't generate a new identifier for it
(or (not (should-inline-contract? ctc))
(not top-level?))
cache)
(cond [cache
(define fresh-id (generate-temporary))
(hash-set! cache sc (cons fresh-id ctc))
(set! sc-queue (cons sc sc-queue))
@ -180,8 +137,8 @@
(recur body)))]
[(? sc? sc)
(sc->contract sc recur)]))
(define ctc (recur sc #t))
(define name-defs (compute-defs sc))
(define ctc (recur sc))
(define name-defs (get-all-name-defs))
;; These are extra contract definitions for the name static contracts
;; that are used for this type. Since these are shared across multiple
;; contracts from a single contract fixup pass, we use the name-defined
@ -206,17 +163,6 @@
#`(define #,id #,ctc)))
ctc))
;; Determine whether the given contract syntax should be inlined or not.
(define (should-inline-contract? stx)
(or
;; no need to generate an extra def for things that are already identifiers
(identifier? stx)
;; ->* are handled specially by the contract system
(let ([sexp (syntax-e stx)])
(and (pair? sexp)
(or (free-identifier=? (car sexp) #'->)
(free-identifier=? (car sexp) #'->*))))))
;; determine if a given name is free in the sc
(define (name-free-in? name sc)
(let/ec escape

View File

@ -93,7 +93,6 @@
(fail))
;; All the checks passed
(function/sc
#t
(take longest-args (length shortest-args))
(drop longest-args (length shortest-args))
empty
@ -111,7 +110,7 @@
(define (trusted-side-reduce sc)
(match sc
[(->/sc: mand-args opt-args mand-kw-args opt-kw-args rest-arg (list (any/sc:) ...))
(function/sc #t mand-args opt-args mand-kw-args opt-kw-args rest-arg #f)]
(function/sc mand-args opt-args mand-kw-args opt-kw-args rest-arg #f)]
[(arr/sc: args rest (list (any/sc:) ...))
(arr/sc args rest #f)]
[(none/sc:) any/sc]

View File

@ -76,8 +76,9 @@
(tc-setup orig-stx stx 'top-level
local-expand/capture* (kernel-form-identifier-list)
(λ (head-expanded-stx)
(do-time "Trampoline the top-level checker")
(tc-toplevel-start (or (orig-module-stx) orig-stx) head-expanded-stx))))
(parameterize ([orig-module-stx (or (orig-module-stx) orig-stx)])
(do-time "Trampoline the top-level checker")
(tc-toplevel-start head-expanded-stx)))))
(define (tc-module/full orig-stx stx k)
(tc-setup orig-stx stx 'module-begin local-expand (list #'module*)

View File

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

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)
;; Prop top level expressions into several groups, each processed
;; Filter top level expressions into several groups, each processed
;; into appropriate data structures
;;
;; Augment annotations go in their own table, because they're
@ -550,10 +550,21 @@
#:when (set-member? (hash-ref parse-info 'private-fields) name))
(hash-set! private-field-types name (list type)))
;; Hash<Syntax -> Listof<Listof<Syntax>, Listof<Type>>>
;; Maps the outermost `let-values` expressions introduced by the expansion of
;; `define-values` within the class body to a list of identifier syntaxes
;; that represent variables and a list of corresponding types.
;; The variables temporarily hold the values of the initializer expression;
;; a field mutator is called on each one in the body of the `let-values`.
;; Typechecking of these calls is done in `check-field-set!s` and requires
;; the types of the initial values.
(define inits-temporaries-types (make-hasheq))
(define synthesized-init-val-stxs
(synthesize-private-field-types private-field-stxs
local-private-field-table
private-field-types))
private-field-types
inits-temporaries-types))
;; Detect mutation of private fields for occurrence typing
(for ([stx (in-sequences
@ -598,7 +609,8 @@
(with-lexical-env/extend-types lexical-names/top-level lexical-types/top-level
(check-field-set!s (hash-ref parse-info 'initializer-body)
synthesized-init-val-stxs
inits))
inits
inits-temporaries-types))
(do-timestamp "checked field initializers")
(define checked-method-types
(with-lexical-env/extend-types lexical-names lexical-types
@ -983,7 +995,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
;; prop when it's provided. This allows us to, say, only
;; filter 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))
@ -1023,11 +1035,11 @@
(tc-expr/t xformed-stx)])))
;; check-field-set!s : Syntax Listof<Syntax> Dict<Symbol, Type>
;; -> Void
;; Dict<Syntax, List<Listof<Syntax>, Listof<Type>> -> Void
;; Check that fields are initialized to the correct type
;; FIXME: use syntax classes for matching and clearly separate the handling
;; of field initialization and set! uses
(define (check-field-set!s stx synthed-stxs inits)
(define (check-field-set!s stx synthed-stxs inits inits-temporaries-types)
(for ([form (syntax->list stx)])
(syntax-parse form
#:literal-sets (kernel-literals)
@ -1094,21 +1106,12 @@
(tc-expr/check processed (ret type)))]
;; multiple private fields
[(let-values ([(names:id ...) val-expr]) begins ... (#%plain-app _))
;; This seems like it's duplicating work since the synthesis pass
;; earlier had to do this, but it needs to be re-checked in this context
;; so that it has the right environment. An earlier approach did
;; check this only in the synthesis stage, but caused some regressions.
(define temp-names (syntax->list #'(names ...)))
(define init-types
(match (tc-expr #'val-expr)
[(tc-results: xs ) xs]))
(unless (= (length temp-names) (length init-types))
(tc-error/expr "wrong number of values: expected ~a but got ~a"
(length temp-names) (length init-types)))
(match-define (list t-names t-types)
(hash-ref inits-temporaries-types form (list empty empty)))
;; Extend lexical type env with temporaries introduced in the
;; expansion of the field initialization or setter
(with-lexical-env/extend-types temp-names init-types
(check-field-set!s #'(begins ...) synthed-stxs inits))]
(with-lexical-env/extend-types t-names t-types
(check-field-set!s #'(begins ...) synthed-stxs inits inits-temporaries-types))]
[_ (void)])))
;; setter->type : Id -> Type
@ -1141,11 +1144,11 @@
[else
(tc-expr/check init-val (ret init-type))])))
;; synthesize-private-field-types : Listof<Syntax> Dict Hash -> Listof<Syntax>
;; synthesize-private-field-types : Listof<Syntax> Dict Hash Hash -> Listof<Syntax>
;; Given top-level expressions in the class, synthesize types from
;; the initialization expressions for private fields. Returns the initial
;; value expressions that were type synthesized.
(define (synthesize-private-field-types stxs locals types)
(define (synthesize-private-field-types stxs locals types inits-temporaries-types)
(for/fold ([synthed-stxs null])
([stx (in-list stxs)])
(syntax-parse stx
@ -1183,18 +1186,23 @@
(define field-names (map syntax-e (syntax-e (tr:class:def-property stx))))
(define temporary-stxs (syntax-e #'(initial-value-name ...)))
(define init-types
;; this gets re-checked later, so don't throw any errors yet
(match (tc-expr/check? #'initial-values #f)
[(tc-results: xs ) xs]
;; We have to return something here so use the most conservative type
[#f (make-list (length field-names) Univ)]))
(for ([name (in-list field-names)]
[temp-stx (in-list temporary-stxs)]
[type (in-list init-types)])
(define type-table-val (generalize type))
(unless (hash-has-key? types name)
(hash-set! types name (list type-table-val)))
(cons temp-stx type-table-val))
(match (tc-expr/check #'initial-values #f)
[(tc-results: xs ) xs]))
(unless (= (length field-names) (length init-types))
(tc-error/expr "wrong number of values: expected ~a but got ~a"
(length field-names) (length init-types)))
(define temporaries-types
(for/list
([name (in-list field-names)]
[temp-stx (in-list temporary-stxs)]
[type (in-list init-types)])
(define type-table-val (generalize type))
(unless (hash-has-key? types name)
(hash-set! types name (list type-table-val)))
(cons temp-stx type-table-val)))
(hash-set! inits-temporaries-types stx
(list (map car temporaries-types)
(map cdr temporaries-types)))
(cons #'initial-values synthed-stxs)])))
;; Syntax -> Dict<Symbol, Id> Dict<Symbol, Id>
@ -1597,7 +1605,7 @@
(make-PolyRow ns constraints (method->function type))]
[_ (tc-error/expr #:return -Bottom "expected a function type for method")]))
;; process-method-syntax : Syntax Type (Option Type) -> Syntax
;; process-method-syntax : Syntax (Option Type) -> Syntax
;; Register types for identifiers in a method that don't come with types and
;; propagate syntax properties as needed
(define (process-method-syntax stx self-type method-type)

View File

@ -11,7 +11,7 @@
(utils tc-utils)
(for-syntax racket/base syntax/parse)
(for-template racket/base)
(rep type-rep prop-rep object-rep))
(rep type-rep filter-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 prop-type)
(define (get-range-result stx t filter-type)
(let loop ((t t))
(match t
[(Function: (list _ ... (arr: (list arg1) _ _ #f (list (Keyword: _ _ #f) ...)) _ ...))
#:when (subtype prop-type arg1)
#:when (subtype filter-type arg1)
(tc/funapp #'here #'(here) t (list (ret arg1)) #f)]
[(Function: (list _ ... (arr: '() _ (? values rest) #f (list (Keyword: _ _ #f) ...)) _ ...))
#:when (subtype prop-type rest)
#:when (subtype filter-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 (-> prop-type Univ)))
(not (subtype t (-> filter-type Univ)))
(parameterize ([current-orig-stx stx])
(check-below t (-> prop-type Univ)))]
[else (int-err "get-range-result: should not happen. type ~a prop ~a"
t prop-type)])
(check-below t (-> filter-type Univ)))]
[else (int-err "get-range-result: should not happen. type ~a filter ~a"
t filter-type)])
(ret (Un))])))
;; Syntax Type -> (Option Type)
;; Extract the type for the prop in a predicate type, or #f if
;; Extract the type for the filter in a predicate type, or #f if
;; the type is an invalid predicate type.
(define (get-prop-type stx pred-type)
(define (get-filter-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.
[(PredicateProp: ps)
(match ps
[(PropSet: (TypeProp: (Path: '() '(0 0)) ft) _) ft]
[(FalseProp:) (Un)]
[(PredicateFilter: fs)
(match fs
[(FilterSet: (TypeFilter: ft (Path: '() '(0 0))) _) ft]
[(Bot:) (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 prop-type
(get-prop-type predicate-stx predicate-type))
(define filter-type
(get-filter-type predicate-stx predicate-type))
;; if the predicate doesn't check, then don't bother
;; with the RHS and return no result
(if prop-type
(get-range-result handler-stx handler-type prop-type)
(if filter-type
(get-range-result handler-stx handler-type filter-type)
(ret (Un)))))
(find-syntax form

View File

@ -70,7 +70,7 @@
(private parse-type syntax-properties type-annotation)
(only-in (base-env base-special-env) make-template-identifier)
(env lexical-env tvar-env global-env
signature-env)
signature-env signature-helper)
(types utils abbrev union subtype resolve generalize signatures)
(typecheck check-below internal-forms)
(utils tc-utils)
@ -170,7 +170,7 @@
(values (for/list ([sig-id (in-list import-sigs)]
[sig-internal-ids (in-list import-internal-ids)])
(sig-info sig-id
(map car (Signature-mapping (lookup-signature/check sig-id)))
(map car (Signature-mapping (lookup-signature sig-id)))
sig-internal-ids))
;; export-temp-ids is a flat list which must be processed
;; sequentially to map them to the correct internal/external identifiers
@ -179,7 +179,7 @@
[sig-infos '()])
([sig (in-list export-sigs)])
(define external-ids
(map car (Signature-mapping (lookup-signature/check sig))))
(map car (Signature-mapping (lookup-signature sig))))
(define len (length external-ids))
(values (drop temp-ids len)
(cons (sig-info sig
@ -391,7 +391,7 @@
;; Returns a mapping of link-ids to sig-ids, a list of imported sig ids
;; a list of exported link-ids
(define (parse-compound-unit stx)
(define (list->sigs l) (map lookup-signature/check l))
(define (list->sigs l) (map lookup-signature l))
(syntax-parse stx
[cu:compound-unit-expansion
(define link-binding-info (tr:unit:compound-property stx))
@ -407,7 +407,7 @@
(let ()
(define link-syms (append cu-import-syms (flatten unit-export-syms)))
(define sig-ids (append compound-imports (flatten unit-exports)))
(map cons link-syms (map lookup-signature/check sig-ids))))
(map cons link-syms (map lookup-signature sig-ids))))
(define cu-exprs
(for/list ([unit-expr (in-list unit-exprs)]
[import-sigs (in-list unit-imports)]
@ -428,7 +428,7 @@
;; GIVEN: signature information
;; RETURNS: a mapping from internal names to types
(define (make-local-type-mapping si)
(define sig (lookup-signature/check (sig-info-name si)))
(define sig (lookup-signature (sig-info-name si)))
(define internal-names (sig-info-internals si))
(define sig-types
(map cdr (Signature-mapping sig)))
@ -475,7 +475,7 @@
(define (parse-and-check-unit-from-context form expected-type)
(syntax-parse form
[u:unit-expansion
(define export-sigs (map lookup-signature/check (attribute u.export-sigs)))
(define export-sigs (map lookup-signature (attribute u.export-sigs)))
(define body-stx (attribute u.body-stx))
(for ([sig (in-list export-sigs)])
(define ids (extract-definitions body-stx))
@ -558,8 +558,8 @@
(syntax-parse form
[cu:compound-unit-expansion
(define unit-exprs (attribute cu.unit-exprs))
(define compound-imports (map lookup-signature/check (attribute cu.compound-imports)))
(define compound-exports (map lookup-signature/check (attribute cu.compound-exports)))
(define compound-imports (map lookup-signature (attribute cu.compound-imports)))
(define compound-exports (map lookup-signature (attribute cu.compound-exports)))
(define import-vector (apply vector compound-imports))
(define import-length (vector-length import-vector))
(unless (and (list? init-depend-refs)
@ -579,7 +579,7 @@
[iu:invoke-unit-expansion
(define infer? (eq? 'infer (tr:unit:invoke-property form)))
(define invoked-unit (attribute iu.expr))
(define import-sigs (map lookup-signature/check (attribute iu.imports)))
(define import-sigs (map lookup-signature (attribute iu.imports)))
(define linking-units (attribute iu.units))
(define unit-expr-type (tc-expr/t invoked-unit))
;; TODO: Better error message/handling when the folling check-below "fails"
@ -630,9 +630,9 @@
init-depend-tags))
;; Get Signatures to build Unit type
(define import-signatures (map lookup-signature/check (map sig-info-name imports-info)))
(define export-signatures (map lookup-signature/check (map sig-info-name exports-info)))
(define init-depend-signatures (map lookup-signature/check init-depends))
(define import-signatures (map lookup-signature (map sig-info-name imports-info)))
(define export-signatures (map lookup-signature (map sig-info-name exports-info)))
(define init-depend-signatures (map lookup-signature init-depends))
(unless (distinct-signatures? import-signatures)
(tc-error/expr "unit expressions must import distinct signatures"))

View File

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

View File

@ -74,13 +74,12 @@
;;; Helpers
(define-splicing-syntax-class dtsi-fields
#:attributes (mutable prefab type-only maker extra-maker)
#:attributes (mutable prefab type-only maker)
(pattern
(~seq
(~or (~optional (~and #:mutable (~bind (mutable #t))))
(~optional (~and #:prefab (~bind (prefab #t))))
(~optional (~and #:type-only (~bind (type-only #t))))
(~optional (~seq #:extra-maker extra-maker))
(~optional (~seq #:maker maker))) ...)))
(define-syntax-class struct-name
@ -89,16 +88,14 @@
(define-syntax-class define-typed-struct-body
#:attributes (name type-name mutable prefab type-only maker extra-maker nm
(tvars 1) (fields 1) (types 1))
#:attributes (name mutable prefab type-only maker nm (tvars 1) (fields 1) (types 1))
(pattern ((~optional (tvars:id ...) #:defaults (((tvars 1) null)))
nm:struct-name type-name:id ([fields:id : types:expr] ...) options:dtsi-fields)
nm:struct-name ([fields:id : types:expr] ...) options:dtsi-fields)
#:attr name #'nm.nm
#:attr mutable (attribute options.mutable)
#:attr prefab (attribute options.prefab)
#:attr type-only (attribute options.type-only)
#:attr maker (or (attribute options.maker) #'nm.nm)
#:attr extra-maker (attribute options.extra-maker)))
#:attr maker (or (attribute options.maker) #'nm.nm)))
(define-syntax-class dviu-import/export
(pattern (sig-id:id member-id:id ...)
@ -151,7 +148,7 @@
[typed-struct
(define-typed-struct-internal . :define-typed-struct-body)]
[typed-struct/exec
(define-typed-struct/exec-internal nm type-name ([fields:id : types] ...) proc-type)]
(define-typed-struct/exec-internal nm ([fields:id : types] ...) proc-type)]
[typed-require
(require/typed-internal name type)]
[typed-require/struct

View File

@ -1,167 +0,0 @@
#lang racket/base
(require "../utils/utils.rkt"
(contract-req)
racket/list
racket/match
(rep type-rep prop-rep)
(except-in (types abbrev subtype tc-result)
-> ->* one-of/c))
(provide possible-domains)
(provide/cond-contract
[cleanup-type ((Type/c) ((or/c #f Type/c) any/c) . ->* . Type/c)])
;; to avoid long and confusing error messages, in the case of functions with
;; multiple similar domains (<, >, +, -, etc.), we show only the domains that
;; 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 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
;; - we can disregard domains that are more restricted than required to get
;; the expected type (or all but the most liberal domain when no type is
;; expected)
;; ex: if we have the 2 following possible domains for an operator:
;; Fixnum -> Fixnum
;; Integer -> Integer
;; and an expected type of Integer for the result of the application,
;; we can disregard the Fixnum domain since it imposes a restriction that
;; is not necessary to get the expected type
;; This function can be used in permissive or restrictive mode.
;; in permissive mode, domains that are not consistent with the expected type
;; may still be considered possible. This is useful for error messages, where
;; we want to collapse domains always, regardless of expected type. In
;; restrictive mode, only domains that are consistent with the expected type can
;; be considered possible. This is useful when computing the possibly empty set
;; of domains that would *satisfy* the expected type, e.g. for the :query-type
;; forms.
;; TODO separating pruning and collapsing into separate functions may be nicer
(define (possible-domains doms rests drests rngs expected [permissive? #t])
;; is fun-ty subsumed by a function type in others?
(define (is-subsumed-in? fun-ty others)
;; a case subsumes another if the first one is a subtype of the other
(ormap (lambda (x) (subtype x fun-ty))
others))
;; currently does not take advantage of multi-valued or arbitrary-valued expected types,
(define expected-ty
(and expected
(match expected
[(tc-result1: t) t]
[(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
(eq? expected-ty #t) ; expected is tc-anyresults, anything is fine
(and expected-ty ; not some unknown expected tc-result
(match fun-ty
[(Function: (list (arr: _ rng _ _ _)))
(let ([rng (match rng
[(Values: (list (Result: t _ _)))
t]
[(ValuesDots: (list (Result: t _ _)) _ _)
t]
[_ #f])])
(and rng (subtype rng expected-ty)))]))))
(define orig (map list doms rngs rests drests))
(define cases
(map (compose make-Function list make-arr)
doms
(map (match-lambda ; strip props
[(AnyValues: f) (-AnyValues -tt)]
[(Values: (list (Result: t _ _) ...))
(-values t)]
[(ValuesDots: (list (Result: t _ _) ...) _ _)
(-values t)])
rngs)
rests drests (make-list (length doms) null)))
;; iterate in lock step over the function types we analyze and the parts
;; that we will need to print the error message, to make sure we throw
;; away cases consistently
(define-values (candidates* parts-acc*)
(for/fold ([candidates '()] ; from cases
[parts-acc '()]) ; from orig
([c (in-list cases)]
;; the parts we'll need to print the error message
[p (in-list orig)])
(if (returns-subtype-of-expected? c)
(values (cons c candidates) ; we keep this one
(cons p parts-acc))
;; we discard this one
(values candidates parts-acc))))
;; if none of the cases return a subtype of the expected type, still do some
;; merging, but do it on the entire type
;; only do this if we're in permissive mode
(define-values (candidates parts-acc)
(if (and permissive? (null? candidates*))
(values cases orig)
(values candidates* parts-acc*)))
;; among the domains that fit with the expected type, we only need to
;; keep the most liberal
;; since we only care about permissiveness of domains, we reconstruct
;; function types with a return type of any then test for subtyping
(define fun-tys-ret-any
(map (match-lambda
[(Function: (list (arr: dom _ rest drest _)))
(make-Function (list (make-arr dom
(-values (list Univ))
rest drest null)))])
candidates))
;; Heuristic: often, the last case in the definition (first at this
;; point, we've reversed the list) is the most general of all, subsuming
;; all the others. If that's the case, just go with it. Otherwise, go
;; the slow way.
(cond [(and (not (null? fun-tys-ret-any))
(andmap (lambda (c) (subtype (car fun-tys-ret-any) c))
fun-tys-ret-any))
;; Yep. Return early.
(map list (car parts-acc))]
[else
;; No luck, do it the slow way
(define parts-res
;; final pass, we only need the parts to print the error message
(for/fold ([parts-res '()])
([c (in-list fun-tys-ret-any)]
[p (in-list parts-acc)]
;; if a case is a supertype of another, we discard it
#:unless (is-subsumed-in? c (remove c fun-tys-ret-any)))
(cons p parts-res)))
(call-with-values
(λ ()
(for/lists (_1 _2 _3 _4) ([xs (in-list (reverse parts-res))])
(values (car xs) (cadr xs) (caddr xs) (cadddr xs))))
list)]))
;; Wrapper over possible-domains that works on types.
(define (cleanup-type t [expected #f] [permissive? #t])
(match t
;; function type, prune if possible.
[(Function/arrs: doms rngs rests drests kws)
(match-let ([(list pdoms rngs rests drests)
(possible-domains doms rests drests rngs
(and expected (ret expected))
permissive?)])
(if (= (length pdoms) (length doms))
;; pruning didn't improve things, return the original
;; (Note: pruning may have reordered clauses, so may not be `equal?' to
;; the original, which may confuse `:print-type''s pruning detection)
t
;; pruning helped, return pruned type
(make-Function (map make-arr
pdoms rngs rests drests (make-list (length pdoms) null)))))]
;; not a function type. keep as is.
[_ t]))

View File

@ -8,19 +8,15 @@
(private syntax-properties)
(typecheck renamer def-binding)
(utils tc-utils)
(env env-utils)
(for-syntax racket/base)
(for-template racket/base))
(provide remove-provides provide? generate-prov)
;; Returns #t for safe provides. Returns #f for non-provide forms
;; and unsafe provides for which contracts will not be generated.
(define (provide? form)
(syntax-parse form
#:literal-sets (kernel-literals)
[(~and (#%provide . rest) (~not _:unsafe-provide^))
form]
[(#%provide . rest) form]
[_ #f]))
(define (remove-provides forms)
@ -187,10 +183,9 @@
new-id
null)))
;; Build the final provide with auxilliary definitions
(for/lists (defs export-defs provides aliases)
;; sort provs to generate deterministic output
([(internal-id external-ids) (in-sorted-dict provs id<)])
(for/lists (defs export-defs provides aliases) ([(internal-id external-ids) (in-dict provs)])
(define-values (defs export-def id alias) (mk internal-id))
(define provide-forms
(for/list ([external-id (in-list external-ids)])

View File

@ -4,10 +4,10 @@
racket/match racket/sequence racket/set racket/list
(only-in racket/list make-list)
(contract-req)
(typecheck check-below tc-subst tc-metafunctions possible-domains)
(typecheck check-below tc-subst tc-metafunctions)
(utils tc-utils)
(rep type-rep prop-rep)
(except-in (types utils abbrev subtype type-table)
(rep type-rep filter-rep)
(except-in (types utils abbrev subtype)
-> ->* one-of/c))
(require-for-cond-contract
syntax/stx)
@ -18,8 +18,6 @@
(#:check boolean?)
. ->* . full-tc-results/c)])
(define (tc/funapp1 f-stx args-stx ftype0 argtys expected #:check [check? #t])
;; update tooltip-table with inferred function type
(add-typeof-expr f-stx (ret (make-Function (list ftype0))))
(match* (ftype0 argtys)
;; we check that all kw args are optional
[((arr: dom rng rest #f (and kws (list (Keyword: _ _ #f) ...)))
@ -75,11 +73,9 @@
(define (make-printable t)
(match t
[(tc-result1: t) (cleanup-type t)]
[(or (tc-results: ts)
(tc-results: ts _ _ _ _))
(-values (map cleanup-type ts))]
[(tc-any-results: f) (-AnyValues -tt)]
[_ t]))
[(tc-results: ts) (-values (map cleanup-type ts))]
[(tc-any-results: f) (-AnyValues -top)]
[_ (cleanup-type t)]))
(define (stringify-domain dom rst drst [rng #f])
(let ([doms-string (if (null? dom) "" (string-append (stringify (map make-printable dom)) " "))]
@ -180,12 +176,13 @@
return]
[else
;; if not, print the message as usual
(define pdoms* (map make-printable pdoms))
(define err-doms
(string-append
label
(stringify (if expected
(map stringify-domain pdoms rests drests rngs)
(map stringify-domain pdoms rests drests))
(map stringify-domain pdoms* rests drests rngs)
(map stringify-domain pdoms* rests drests))
nl+spc)
"\nArguments: "
arguments-str
@ -198,6 +195,161 @@
(msg-thunk err-doms))])))])) ; generate message
;; to avoid long and confusing error messages, in the case of functions with
;; multiple similar domains (<, >, +, -, etc.), we show only the domains that
;; 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
;; 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
;; - we can disregard domains that are more restricted than required to get
;; the expected type (or all but the most liberal domain when no type is
;; expected)
;; ex: if we have the 2 following possible domains for an operator:
;; Fixnum -> Fixnum
;; Integer -> Integer
;; and an expected type of Integer for the result of the application,
;; we can disregard the Fixnum domain since it imposes a restriction that
;; is not necessary to get the expected type
;; This function can be used in permissive or restrictive mode.
;; in permissive mode, domains that are not consistent with the expected type
;; may still be considered possible. This is useful for error messages, where
;; we want to collapse domains always, regardless of expected type. In
;; restrictive mode, only domains that are consistent with the expected type can
;; be considered possible. This is useful when computing the possibly empty set
;; of domains that would *satisfy* the expected type, e.g. for the :query-type
;; forms.
;; TODO separating pruning and collapsing into separate functions may be nicer
(define (possible-domains doms rests drests rngs expected [permissive? #t])
;; is fun-ty subsumed by a function type in others?
(define (is-subsumed-in? fun-ty others)
;; a case subsumes another if the first one is a subtype of the other
(ormap (lambda (x) (subtype x fun-ty))
others))
;; currently does not take advantage of multi-valued or arbitrary-valued expected types,
(define expected-ty
(and expected
(match expected
[(tc-result1: t) t]
[(tc-any-results: (or (Top:) (NoFilter:))) #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
(eq? expected-ty #t) ; expected is tc-anyresults, anything is fine
(and expected-ty ; not some unknown expected tc-result
(match fun-ty
[(Function: (list (arr: _ rng _ _ _)))
(let ([rng (match rng
[(Values: (list (Result: t _ _)))
t]
[(ValuesDots: (list (Result: t _ _)) _ _)
t]
[_ #f])])
(and rng (subtype rng expected-ty)))]))))
(define orig (map list doms rngs rests drests))
(define cases
(map (compose make-Function list make-arr)
doms
(map (match-lambda ; strip filters
[(AnyValues: f) (-AnyValues -top)]
[(Values: (list (Result: t _ _) ...))
(-values t)]
[(ValuesDots: (list (Result: t _ _) ...) _ _)
(-values t)])
rngs)
rests drests (make-list (length doms) null)))
;; iterate in lock step over the function types we analyze and the parts
;; that we will need to print the error message, to make sure we throw
;; away cases consistently
(define-values (candidates* parts-acc*)
(for/fold ([candidates '()] ; from cases
[parts-acc '()]) ; from orig
([c (in-list cases)]
;; the parts we'll need to print the error message
[p (in-list orig)])
(if (returns-subtype-of-expected? c)
(values (cons c candidates) ; we keep this one
(cons p parts-acc))
;; we discard this one
(values candidates parts-acc))))
;; if none of the cases return a subtype of the expected type, still do some
;; merging, but do it on the entire type
;; only do this if we're in permissive mode
(define-values (candidates parts-acc)
(if (and permissive? (null? candidates*))
(values cases orig)
(values candidates* parts-acc*)))
;; among the domains that fit with the expected type, we only need to
;; keep the most liberal
;; since we only care about permissiveness of domains, we reconstruct
;; function types with a return type of any then test for subtyping
(define fun-tys-ret-any
(map (match-lambda
[(Function: (list (arr: dom _ rest drest _)))
(make-Function (list (make-arr dom
(-values (list Univ))
rest drest null)))])
candidates))
;; Heuristic: often, the last case in the definition (first at this
;; point, we've reversed the list) is the most general of all, subsuming
;; all the others. If that's the case, just go with it. Otherwise, go
;; the slow way.
(cond [(and (not (null? fun-tys-ret-any))
(andmap (lambda (c) (subtype (car fun-tys-ret-any) c))
fun-tys-ret-any))
;; Yep. Return early.
(map list (car parts-acc))]
[else
;; No luck, do it the slow way
(define parts-res
;; final pass, we only need the parts to print the error message
(for/fold ([parts-res '()])
([c (in-list fun-tys-ret-any)]
[p (in-list parts-acc)]
;; if a case is a supertype of another, we discard it
#:unless (is-subsumed-in? c (remove c fun-tys-ret-any)))
(cons p parts-res)))
(call-with-values
(λ ()
(for/lists (_1 _2 _3 _4) ([xs (in-list (reverse parts-res))])
(values (car xs) (cadr xs) (caddr xs) (cadddr xs))))
list)]))
;; Wrapper over possible-domains that works on types.
(provide/cond-contract
[cleanup-type ((Type/c) ((or/c #f Type/c) any/c) . ->* . Type/c)])
(define (cleanup-type t [expected #f] [permissive? #t])
(match t
;; function type, prune if possible.
[(Function/arrs: doms rngs rests drests kws)
(match-let ([(list pdoms rngs rests drests)
(possible-domains doms rests drests rngs
(and expected (ret expected))
permissive?)])
(if (= (length pdoms) (length doms))
;; pruning didn't improve things, return the original
;; (Note: pruning may have reordered clauses, so may not be `equal?' to
;; the original, which may confuse `:print-type''s pruning detection)
t
;; pruning helped, return pruned type
(make-Function (map make-arr
pdoms rngs rests drests (make-list (length pdoms) null)))))]
;; not a function type. keep as is.
[_ t]))
(provide/cond-contract
[poly-fail ((syntax? syntax? Type/c (listof tc-results?))
(#:name (or/c #f syntax?)

View File

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

View File

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

View File

@ -6,7 +6,7 @@
"utils.rkt"
syntax/parse syntax/stx racket/match racket/set
(typecheck signatures tc-app-helper tc-funapp tc-metafunctions)
(types abbrev utils substitute subtype type-table)
(types abbrev utils substitute subtype)
(rep type-rep)
(utils tc-utils)
(r:infer infer)
@ -35,7 +35,6 @@
;; If #t, then the contract system has inserted an extra argument which we
;; need to ignore
#:attr boundary-ctc? (contract-neg-party-property #'fn)
#:do [(for-each register-ignored! (syntax->list #'form))] ; no type info, so can't optimize
#:with pos-args (if (attribute boundary-ctc?)
(stx-cdr #'*pos-args)
#'*pos-args)

View File

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

View File

@ -7,7 +7,7 @@
racket/format
racket/list
(typecheck signatures)
(types base-abbrev resolve subtype type-table union utils)
(types base-abbrev resolve subtype union utils)
(rep type-rep)
(utils tc-utils)
@ -25,21 +25,10 @@
(define-tc/app-syntax-class (tc/app-objects expected)
#:literal-sets (kernel-literals object-literals)
(pattern (dmo b cl
(~and pos-arg-list (#%plain-app list . pos-args))
(~and named-arg-list (#%plain-app list (#%plain-app cons (quote names) named-args) ...)))
(#%plain-app list . pos-args)
(#%plain-app list (#%plain-app cons (quote names) named-args) ...))
#:declare dmo (id-from 'do-make-object 'racket/private/class-internal)
(begin0
(check-do-make-object #'cl #'pos-args #'(names ...) #'(named-args ...))
;; synthesize a type for #'pos-arg-list, for the optimizer
(add-typeof-expr #'pos-arg-list
(ret (for/fold ([res (-val '())])
([a (in-list (reverse (syntax->list #'pos-args)))])
(-pair (match (type-of a) [(tc-result1: t) t])
res))))
;; making the optimizer ignore named args is conservative, but safe
;; if we could give #'named-arg-list a type, then we'd be able to
;; optimize it
(register-ignored! #'named-arg-list)))
(check-do-make-object #'cl #'pos-args #'(names ...) #'(named-args ...)))
(pattern (dmo . args)
#:declare dmo (id-from 'do-make-object 'racket/private/class-internal)
(int-err "unexpected arguments to do-make-object"))

View File

@ -7,9 +7,9 @@
syntax/stx
racket/sequence
(typecheck signatures tc-funapp)
(types abbrev type-table utils)
(types abbrev utils)
(private type-annotation)
(rep type-rep prop-rep)
(rep type-rep filter-rep)
(utils tc-utils)
(for-label racket/base racket/bool '#%paramz))
@ -26,7 +26,6 @@
;; parameterize
(pattern (extend-parameterization pmz (~seq params args) ...)
(begin
(register-ignored! #'pmz)
(for ([param (in-syntax #'(params ...))]
[arg (in-syntax #'(args ...))])
(match (single-value param)
@ -50,11 +49,11 @@
Univ))
(list (ret Univ) (single-value #'arg))
expected)]))
;; special-case for not - flip the props
;; special-case for not - flip the filters
(pattern ((~or false? not) arg)
(match (single-value #'arg)
[(tc-result1: t (PropSet: p+ p-) _)
(ret -Boolean (make-PropSet p- p+))]))
[(tc-result1: t (FilterSet: f+ f-) _)
(ret -Boolean (make-FilterSet f- f+))]))
;; 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

View File

@ -5,7 +5,7 @@
"utils.rkt"
syntax/parse racket/match racket/sequence
(typecheck signatures tc-funapp)
(types base-abbrev utils)
(types utils)
(for-label racket/base))
@ -34,24 +34,29 @@
[(tc-result1: tp)
(single-value #'arg expected)]
[(tc-results: ts)
(single-value #'arg)] ;Type check the argument, to find other errors
(single-value #'arg) ;Type check the argument, to find other errors
(tc-error/expr
"wrong number of values: expected ~a but got one"
(length ts))]
;; match polydots case and error
[(tc-results: ts _ _ dty dbound)
(single-value #'arg)]))
(single-value #'arg)
(tc-error/expr
"Expected ~a ..., but got only one value" dty)]))
;; handle `values' specially
(pattern (values . args)
(match expected
[(tc-results: ets efs eos)
(match-let ([(list (tc-result1: ts fs os) ...)
(for/list
([arg (in-syntax #'args)]
[et (in-sequences (in-list ets) (in-cycle (in-value #f)))]
[ef (in-sequences (in-list efs) (in-cycle (in-value #f)))]
[eo (in-sequences (in-list eos) (in-cycle (in-value #f)))])
(if et
(single-value arg (ret et ef eo))
(single-value arg)))])
(ret ts fs os))]
(for/list ([arg (in-syntax #'args)]
[et (in-list ets)]
[ef (in-list efs)]
[eo (in-list eos)])
(single-value arg (ret et ef eo)))])
(if (= (length ts) (length ets) (syntax-length #'args))
(ret ts fs os)
(tc-error/expr "wrong number of values: expected ~a but got ~a"
(length ets) (syntax-length #'args))))]
[_ (match-let ([(list (tc-result1: ts fs os) ...)
(for/list ([arg (in-syntax #'args)])
(single-value arg))])

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)]) -tt-propset)
(for/list ([t (in-list ts)]) -top-filter)
(for/list ([t (in-list ts)]) -empty-obj)
dty dbound)]
[_ (int-err "do-ret fails: ~a" t)]))

View File

@ -1,12 +1,13 @@
#lang racket/base
(require "../utils/utils.rkt"
racket/match racket/list
(require (rename-in "../utils/utils.rkt" [infer infer-in]))
(require racket/match racket/list
(for-syntax racket/base syntax/parse)
(contract-req)
(rep type-rep prop-rep object-rep rep-utils)
(infer-in infer)
(rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils)
(types tc-result resolve subtype remove update union prop-ops)
(types tc-result resolve subtype remove-intersect union filter-ops)
(env type-env-structs lexical-env)
(rename-in (types abbrev)
[-> -->]
@ -16,18 +17,82 @@
(provide with-lexical-env/extend-props)
(define/cond-contract (update t ft pos? lo)
(Type/c Type/c boolean? (listof PathElem?) . -> . Type/c)
;; build-type: build a type while propogating bottom
(define (build-type constructor . args)
(if (memf Bottom? args) -Bottom (apply constructor args)))
(match* ((resolve t) lo)
;; pair ops
[((Pair: t s) (list rst ... (CarPE:)))
(build-type -pair (update t ft pos? rst) s)]
[((Pair: t s) (list rst ... (CdrPE:)))
(build-type -pair t (update s ft pos? rst))]
;; syntax ops
[((Syntax: t) (list rst ... (SyntaxPE:)))
(build-type -Syntax (update t ft pos? rst))]
;; promise op
[((Promise: t) (list rst ... (ForcePE:)))
(build-type -Promise (update t ft pos? rst))]
;; struct ops
[((Struct: nm par flds proc poly pred)
(list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)))
;; note: this updates fields regardless of whether or not they are
;; a polymorphic field. Because subtyping is nominal and accessor
;; functions do not reflect this, this behavior is unobservable
;; except when an a variable aliases the field in a let binding
(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)]
[_ (int-err "update on mutable struct field")])])
(cond
[(Bottom? ty*) ty*]
[else (let ([flds* (append lhs (cons (make-fld ty* acc-id #f) (cdr rhs)))])
(make-Struct nm par flds* proc poly pred))]))]
;; class field ops
;;
;; A refinement of a private field in a class is really a refinement of the
;; return type of the accessor function for that field (rather than a variable).
;; We cannot just refine the type of the argument to the accessor, since that
;; is an object type that doesn't mention private fields. Thus we use the
;; FieldPE path element as a marker to refine the result of the accessor
;; function.
[((Function: (list (arr: doms (Values: (list (Result: rng _ _))) _ _ _)))
(list rst ... (FieldPE:)))
(make-Function
(list (make-arr* doms (update rng ft pos? rst))))]
;; otherwise
[(t '())
(if pos?
(restrict t ft)
(remove t ft))]
[((Union: ts) lo)
(apply Un (map (λ (t) (update t ft 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
;;(int-err "update along ill-typed path: ~a ~a ~a" t t* lo)
t]))
;; Returns #f if anything becomes (U)
(define (env+ env ps)
(define (env+ env fs)
(let/ec exit*
(define (exit) (exit* #f empty))
(define-values (props atoms) (combine-props ps (env-props env) exit))
(define-values (props atoms) (combine-props fs (env-props env) exit))
(values
(for/fold ([Γ (replace-props env props)]) ([p (in-list atoms)])
(match p
[(or (TypeProp: (Path: lo x) pt) (NotTypeProp: (Path: lo x) pt))
(for/fold ([Γ (replace-props env props)]) ([f (in-list atoms)])
(match f
[(or (TypeFilter: ft (Path: lo x)) (NotTypeFilter: ft (Path: lo x)))
(update-type/lexical
(lambda (x t)
(define new-t (update t pt (TypeProp? p) lo))
(define new-t (update t ft (TypeFilter? f) lo))
(when (type-equal? new-t -Bottom)
(exit))
new-t)
@ -37,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 prop.
;; include the interesting props in its filter.
;; WARNING: this may bail out when code is unreachable
(define-syntax (with-lexical-env/extend-props stx)
(define-splicing-syntax-class unreachable?

View File

@ -6,10 +6,10 @@
"signatures.rkt"
"check-below.rkt" "../types/kw-types.rkt"
(types utils abbrev union subtype type-table path-type
prop-ops overlap resolve generalize)
filter-ops remove-intersect resolve generalize)
(private-in syntax-properties)
(rep type-rep prop-rep object-rep)
(only-in (infer infer) intersect)
(rep type-rep filter-rep object-rep)
(only-in (infer infer) restrict)
(utils tc-utils)
(env lexical-env)
racket/list
@ -21,7 +21,6 @@
racket/extflonum
;; Needed for current implementation of typechecking letrec-syntax+values
(for-template (only-in racket/base letrec-values)
(only-in racket/base list)
;; see tc-app-contracts.rkt
racket/contract/private/provide)
@ -54,9 +53,9 @@
(define ty (path-type alias-path (lookup-type/lexical alias-id)))
(ret ty
(if (overlap? ty (-val #f))
(-PS (-not-type obj (-val #f)) (-is-type obj (-val #f)))
-true-propset)
(if (overlap ty (-val #f))
(-FS (-not-filter (-val #f) obj) (-filter (-val #f) obj))
-true-filter)
obj))
;; typecheck an expression, but throw away the effect
@ -140,21 +139,21 @@
[t:typecheck-failure
(explicit-fail #'t.stx #'t.message #'t.var)]
;; data
[(quote #f) (ret (-val #f) -false-propset)]
[(quote #t) (ret (-val #t) -true-propset)]
[(quote #f) (ret (-val #f) -false-filter)]
[(quote #t) (ret (-val #t) -true-filter)]
[(quote val)
(match expected
[(tc-result1: t)
(ret (tc-literal #'val t) -true-propset)]
(ret (tc-literal #'val t) -true-filter)]
[_
(ret (tc-literal #'val) -true-propset)])]
(ret (tc-literal #'val) -true-filter)])]
;; syntax
[(quote-syntax datum . _)
(define expected-type
(match expected
[(tc-result1: t) t]
[_ #f]))
(ret (find-stx-type #'datum expected-type) -true-propset)]
(ret (find-stx-type #'datum expected-type) -true-filter)]
;; mutation!
[(set! id val)
(match-let* ([(tc-result1: id-t) (single-value #'id)]
@ -200,7 +199,7 @@
[(begin0 e . es)
(begin0
(tc-expr/check #'e expected)
(tc-body/check #'es (tc-any-results -tt)))]
(tc-body/check #'es (tc-any-results -top)))]
;; if
[(if tst thn els) (tc/if-twoarm #'tst #'thn #'els expected)]
;; lambda
@ -236,7 +235,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-propset)]
(ret f -true-filter)]
[(or (tc-results: _) (tc-any-results: _))
(tc-expr/check form #f)])]
;; opt function def
@ -274,40 +273,8 @@
(ret (opt-unconvert (tc-expr/t #'fun)
(syntax->list #'(formals ...))))]
;; let
[(let-values bindings . body)
(define bindings*
(syntax-parse #'body
#:literal-sets (kernel-literals)
;; special case: let-values that originates from an application of a
;; kw function. we may need to ignore contract-related arguments
[((kw-app1 (kw-app2 cpce s-kp fn kpe kws num) ; see tc-app/tc-app-keywords.rkt
kw-list
(kw-app3 list . kw-arg-list)
. *pos-args))
#:declare cpce (id-from 'checked-procedure-check-and-extract 'racket/private/kw)
#:declare s-kp (id-from 'struct:keyword-procedure 'racket/private/kw)
#:declare kpe (id-from 'keyword-procedure-extract 'racket/private/kw)
#:declare kw-app1 (id-from '#%app 'racket/private/kw)
#:declare kw-app2 (id-from '#%app 'racket/private/kw)
#:declare kw-app3 (id-from '#%app 'racket/private/kw)
#:declare list (id-from 'list 'racket/private/kw)
#:when (contract-neg-party-property #'fn) ; contracted
;; ignore the rhs which refers to a contract-lifted definition
;; this code may compute the negative blame party, which may involve
;; things that are not typecheckable
(syntax-parse #'bindings
[(c1 [(contract-lhs) contract-rhs] cs ...)
;; give up on optimizing the whole let, part of it is missing type info
;; (not that this expansion could be optimized anyway)
(register-ignored! form)
#'(c1 cs ...)]
[_
(int-err "malformed kw arg let-values ~a" #'bindings)])]
[_ ; not the special case, leave bindings as is
#'bindings]))
(syntax-parse bindings*
[([(name ...) expr] ...)
(tc/let-values #'((name ...) ...) #'(expr ...) #'body expected)])]
[(let-values ([(name ...) expr] ...) . body)
(tc/let-values #'((name ...) ...) #'(expr ...) #'body expected)]
[(letrec-values ([(name ...) expr] ...) . body)
(tc/letrec-values #'((name ...) ...) #'(expr ...) #'body expected)]
;; other
@ -344,14 +311,14 @@
[else
;; Typecheck the first form.
(define e (first es))
(define results (tc-expr/check e (tc-any-results #f)))
(define results (tc-expr/check e (tc-any-results -no-filter)))
(define props
(match results
[(tc-any-results: f) (list f)]
[(tc-results: _ (list (PropSet: p+ p-) ...) _)
(map -or p+ p-)]
[(tc-results: _ (list (PropSet: p+ p-) ...) _ _ _)
(map -or p+ p-)]))
[(tc-results: _ (list (FilterSet: f+ f-) ...) _)
(map -or f+ f-)]
[(tc-results: _ (list (FilterSet: f+ f-) ...) _ _ _)
(map -or f+ f-)]))
(with-lexical-env/extend-props
props
;; If `e` bails out, mark the rest as ignored.
@ -366,18 +333,18 @@
(define (find-stx-type datum-stx [expected #f])
(match datum-stx
[(? syntax? (app syntax-e stx-e))
(match (and expected (resolve (intersect expected (-Syntax Univ))))
(match (and expected (resolve (restrict expected (-Syntax Univ) 'orig)))
[(Syntax: t) (-Syntax (find-stx-type stx-e t))]
[_ (-Syntax (find-stx-type stx-e))])]
[(or (? symbol?) (? null?) (? number?) (? extflonum?) (? boolean?) (? string?) (? char?)
(? bytes?) (? regexp?) (? byte-regexp?) (? keyword?))
(tc-literal #`#,datum-stx expected)]
[(cons car cdr)
(match (and expected (resolve (intersect expected (-pair Univ Univ))))
(match (and expected (resolve (restrict expected (-pair Univ Univ) 'orig)))
[(Pair: car-t cdr-t) (-pair (find-stx-type car car-t) (find-stx-type cdr cdr-t))]
[_ (-pair (find-stx-type car) (find-stx-type cdr))])]
[(vector xs ...)
(match (and expected (resolve (intersect expected -VectorTop)))
(match (and expected (resolve (restrict expected -VectorTop 'orig)))
[(Vector: t)
(make-Vector
(check-below
@ -393,11 +360,11 @@
[_ (make-HeterogeneousVector (for/list ([x (in-list xs)])
(generalize (find-stx-type x #f))))])]
[(box x)
(match (and expected (resolve (intersect expected -BoxTop)))
(match (and expected (resolve (restrict expected -BoxTop 'orig)))
[(Box: t) (-box (check-below (find-stx-type x t) t))]
[_ (-box (generalize (find-stx-type x)))])]
[(? hash? h)
(match (and expected (resolve (intersect expected -HashTop)))
(match (and expected (resolve (restrict expected -HashTop 'orig)))
[(Hashtable: kt vt)
(define kts (hash-map h (lambda (x y) (find-stx-type x kt))))
(define vts (hash-map h (lambda (x y) (find-stx-type y vt))))

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