Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions typed-racket-lib/typed-racket/private/parse-classes.rkt
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
#lang racket/base

(require syntax/parse/pre
"../utils/literal-syntax-class.rkt"
(for-label "../base-env/base-types-extra.rkt"))
(require (for-label "../base-env/base-types-extra.rkt")
syntax/parse/pre
"../utils/literal-syntax-class.rkt")
(provide star ddd ddd/bound omit-parens)

(define-literal-syntax-class #:for-label ->)
Expand Down
23 changes: 11 additions & 12 deletions typed-racket-lib/typed-racket/private/parse-type.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -183,8 +183,8 @@
;; (Syntax -> Type) -> Syntax Any -> Syntax
;; See `parse-type/id`. This is a curried generalization.
(define ((parse/id p) loc datum)
(let* ([stx* (datum->syntax loc datum loc loc)])
(p stx*)))
(define stx* (datum->syntax loc datum loc loc))
(p stx*))

(define (parse-literal-alls stx)
(syntax-parse stx
Expand Down Expand Up @@ -1507,10 +1507,9 @@
;; Merge all the non-duplicate entries from the parent types
(define (merge-clause parent-clause clause)
(for/fold ([clause clause])
([(k v) (in-dict parent-clause)])
(if (dict-has-key? clause k)
clause
(dict-set clause k v))))
([(k v) (in-dict parent-clause)]
#:unless (dict-has-key? clause k))
(dict-set clause k v)))

(define (match-parent-type parent-type)
(define resolved (resolve parent-type))
Expand Down Expand Up @@ -1655,12 +1654,12 @@
;; of init arguments.
(define parent-inits (get-parent-inits parent/init-type))

(define class-type
(make-Class row-var
(append given-inits parent-inits)
fields methods augments given-init-rest))

class-type]
(make-Class row-var
(append given-inits parent-inits)
fields
methods
augments
given-init-rest)]
[else
;; Conservatively assume that if there *are* #:implements
;; clauses, then the current type alias will be recursive
Expand Down
206 changes: 110 additions & 96 deletions typed-racket-lib/typed-racket/private/shallow-rewrite.rkt

Large diffs are not rendered by default.

7 changes: 4 additions & 3 deletions typed-racket-lib/typed-racket/private/syntax-properties.rkt
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
#lang racket/base
(require
syntax/parse/pre
(for-syntax racket/base syntax/parse/pre racket/syntax))
(require (for-syntax racket/base
racket/syntax
syntax/parse/pre)
syntax/parse/pre)

(define-syntax define-matcher
(syntax-parser
Expand Down
83 changes: 43 additions & 40 deletions typed-racket-lib/typed-racket/private/type-annotation.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -89,46 +89,49 @@
(listof tc-result?))
(match stxs
[(list stx ...)
(let ([anns (for/list ([s (in-list stxs)])
(cond
;; if the lhs identifier is the rest parameter, its type is
;; (Listof ty), where ty is the annotated type
[(rst-arg-property s)
(make-Listof (type-annotation s #:infer #t))]
[else (type-annotation s #:infer #t)]))])
(if (for/and ([a (in-list anns)]) a)
(match (tc-expr/check expr (ret anns))
[(tc-results: tcrs _) tcrs])
(match (tc-expr expr)
[(tc-any-results: _)
(tc-error/expr
#:return (map (λ _ (-tc-result -Bottom)) stxs)
"Expression should produce ~a values, but produces an unknown number of values"
(length stxs))]
[(tc-result1: (== -Bottom))
(for/list ([_ (in-range (length stxs))])
(-tc-result -Bottom))]
[(tc-results: tcrs _)
(cond
[(not (= (length stxs) (length tcrs)))
(tc-error/expr #:return (map (λ _ (-tc-result -Bottom)) stxs)
"Expression should produce ~a values, but produces ~a values of types ~a"
(length stxs)
(length tcrs)
(stringify (map tc-result-t tcrs)))]
[else
(for/list ([stx (in-list stxs)]
[tcr (in-list tcrs)]
[a (in-list anns)])
(match tcr
[(tc-result: ty ps o)
(cond [a (check-type stx ty a)
(-tc-result a ps o)]
;; mutated variables get generalized, so that we don't
;; infer too small a type
[(is-var-mutated? stx)
(-tc-result (generalize ty) ps o)]
[else (-tc-result ty ps o)])]))])])))]))
(define anns
(for/list ([s (in-list stxs)])
(cond
;; if the lhs identifier is the rest parameter, its type is
;; (Listof ty), where ty is the annotated type
[(rst-arg-property s) (make-Listof (type-annotation s #:infer #t))]
[else (type-annotation s #:infer #t)])))
(if (for/and ([a (in-list anns)])
a)
(match (tc-expr/check expr (ret anns))
[(tc-results: tcrs _) tcrs])
(match (tc-expr expr)
[(tc-any-results: _)
(tc-error/expr
#:return (map (λ _ (-tc-result -Bottom)) stxs)
"Expression should produce ~a values, but produces an unknown number of values"
(length stxs))]
[(tc-result1: (== -Bottom))
(for/list ([_ (in-range (length stxs))])
(-tc-result -Bottom))]
[(tc-results: tcrs _)
(cond
[(not (= (length stxs) (length tcrs)))
(tc-error/expr
#:return (map (λ _ (-tc-result -Bottom)) stxs)
"Expression should produce ~a values, but produces ~a values of types ~a"
(length stxs)
(length tcrs)
(stringify (map tc-result-t tcrs)))]
[else
(for/list ([stx (in-list stxs)]
[tcr (in-list tcrs)]
[a (in-list anns)])
(match tcr
[(tc-result: ty ps o)
(cond
[a
(check-type stx ty a)
(-tc-result a ps o)]
;; mutated variables get generalized, so that we don't
;; infer too small a type
[(is-var-mutated? stx) (-tc-result (generalize ty) ps o)]
[else (-tc-result ty ps o)])]))])]))]))

;; check that e-type is compatible with ty in context of stx
;; otherwise, error
Expand Down
136 changes: 59 additions & 77 deletions typed-racket-lib/typed-racket/private/type-contract.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -239,10 +239,11 @@
(define (change-contract-fixups forms [ctc-cache (make-hash)])
(with-new-name-tables
(for/list ((e (in-list forms)))
(if (not (has-contract-def-property? e))
e
(begin (set-box! include-extra-requires? #t)
(generate-contract-def e ctc-cache))))))
(cond
[(not (has-contract-def-property? e)) e]
[else
(set-box! include-extra-requires? #t)
(generate-contract-def e ctc-cache)]))))

;; TODO: These are probably all in a specific place, which could avoid
;; the big traversal
Expand Down Expand Up @@ -386,8 +387,8 @@
(loop t (flip-side typed-side) recursive-values))
(define (t->sc/both t #:recursive-values (recursive-values recursive-values))
(loop t 'both recursive-values))
(define (t->sc/fun t #:maybe-existential [opt-exi #f]) (t->sc/function t fail typed-side recursive-values loop #f #:maybe-existential opt-exi))
(define (t->sc/meth t) (t->sc/method t fail typed-side recursive-values loop))
(define (t->sc/meth t)
(t->sc/method t fail typed-side recursive-values loop))

(define (struct->recursive-sc name-base key flds sc-ctor)
(define key* (generate-temporary name-base))
Expand Down Expand Up @@ -554,13 +555,11 @@
;; 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)]
[spt-pred-procedure?/sc (flat/sc #'struct-type-property-predicate-procedure?)])
(or/sc optimized/sc spt-pred-procedure?/sc (t->sc/fun t)))]
(define unsafe-spp/sc (flat/sc #'struct-predicate-procedure?))
(define safe-spp/sc (flat/sc #'struct-predicate-procedure?/c))
(define optimized/sc (if (from-typed? typed-side) unsafe-spp/sc safe-spp/sc))
(define spt-pred-procedure?/sc (flat/sc #'struct-type-property-predicate-procedure?))
(or/sc optimized/sc spt-pred-procedure?/sc (t->sc/fun t))]
[(? Fun? t) (t->sc/fun t)]
[(? DepFun? t) (t->sc/fun t)]
[(Set: t) (set/sc (t->sc t))]
Expand Down Expand Up @@ -835,10 +834,10 @@
[else (is-flat-type/sc (obj->sc o) sc)])]
[(NotTypeProp: o t)
(define sc (t->sc t bound-all-vars))
(cond
[(not (equal? flat-sym (get-max-contract-kind sc)))
(raise-user-error 'type->static-contract/shallow "proposition contract generation not supported for non-flat types")]
[else (not-flat-type/sc (obj->sc o) sc)])]
(unless (equal? flat-sym (get-max-contract-kind sc))
(raise-user-error 'type->static-contract/shallow
"proposition contract generation not supported for non-flat types"))
(not-flat-type/sc (obj->sc o) sc)]
[(LeqProp: (app obj->sc lhs) (app obj->sc rhs))
(leq/sc lhs rhs)]
[(AndProp: ps)
Expand Down Expand Up @@ -1136,39 +1135,34 @@
(define (t->sc/function f fail typed-side recursive-values loop method? #:maybe-existential [opt-exi #f])
(define (t->sc t #:recursive-values (recursive-values recursive-values))
(loop t typed-side recursive-values))
(define (t->sc/neg t #:recursive-values (recursive-values recursive-values))
(loop t (flip-side typed-side) recursive-values))

(define (arr-params->exist/sc exi dom rst kw rng prop+type)
(define (occur? t)
(if (or (not t) (empty? t)) #f
(if (or (not t) (empty? t))
#f
(set-member? (free-vars-names (free-vars* t)) exi)))

(match* (rng prop+type)
[((Fun: (list (Arrow: (list-rest (F: n1) a ... _) rst_i kw_i _))) (F: n1))
#:when (and (not (ormap occur? (list rst kw rst_i kw_i)))
(eq? n1 exi))
#:when (and (not (ormap occur? (list rst kw rst_i kw_i))) (eq? n1 exi))
(void)]
[(_ _) (fail #:reason
"contract generation only supports Some Type in this form: (Some (X) (-> ty1 ... (-> X ty ... ty2) : X)) or (-> ty1 ... (Some (X) (-> X ty ... ty2) : X))")])

[(_ _)
(fail
#:reason
"contract generation only supports Some Type in this form: (Some (X) (-> ty1 ... (-> X ty ... ty2) : X)) or (-> ty1 ... (Some (X) (-> X ty ... ty2) : X))")])

(define/with-syntax name exi)
(define lhs (t->sc/neg dom))
(define eq-name (flat/sc #'(eq/c name)))
(define rhs (t->sc rng
#:recursive-values (hash-set recursive-values exi
(same eq-name))))
(define rhs (t->sc rng #:recursive-values (hash-set recursive-values exi (same eq-name))))
(exist/sc (list #'name) lhs rhs))


;; handle-arrow-range : Arr (-> Static-Contact) -> Static-Contract
;; Match the range of an arr and determine if a contract can be generated
;; and call the given thunk or raise an error
(define (handle-arrow-range arrow proceed)
(match arrow
[(or (Arrow: _ _ _ rng)
(DepFun: _ _ rng))
(handle-range rng proceed)]))
(match-define (or (Arrow: _ _ _ rng) (DepFun: _ _ rng)) arrow)
(handle-range rng proceed))
(define (handle-range rng proceed)
(match rng
[(Values: (list (Result: _
Expand Down Expand Up @@ -1267,8 +1261,7 @@
(when (and (not (empty? kws)))
(fail #:reason (~a "cannot generate contract for case function type"
" with optional keyword arguments")))
(when (ormap (lambda (n-exi)
(> n-exi 0))
(when (ormap positive?
n-exis)
(fail #:reason (~a "cannot generate contract for case function type with existentials")))

Expand All @@ -1287,51 +1280,35 @@
(handle-arrow-range (first arrows)
(lambda ()
(convert-single-arrow (first arrows))))
(case->/sc (map (lambda (arr)
(handle-arrow-range arr (lambda ()
(convert-one-arrow-in-many arr))))
arrows)))])]
(case->/sc (for/list ([arr (in-list arrows)])
(handle-arrow-range arr (lambda () (convert-one-arrow-in-many arr))))))])]
[(DepFun/ids: ids dom pre rng)
(define (continue)
(match rng
[(Values: (list (Result: rngs _ _) ...))
(define (dom-id? id) (member id ids free-identifier=?))
(define-values (dom* dom-deps)
(for/lists (_1 _2) ([d (in-list dom)])
(values (t->sc/neg d)
(filter dom-id? (free-ids d)))))
(define pre* (if (TrueProp? pre) #f (t->sc/neg pre)))
(define pre-deps (filter dom-id? (free-ids pre)))
(define rng* (map t->sc rngs))
(define rng-deps (filter dom-id?
(remove-duplicates
(apply append (map free-ids rngs))
free-identifier=?)))
(->i/sc (from-typed? typed-side)
ids
dom*
dom-deps
pre*
pre-deps
rng*
rng-deps)]))
(match-define (Values: (list (Result: rngs _ _) ...)) rng)
(define (dom-id? id)
(member id ids free-identifier=?))
(define-values (dom* dom-deps)
(for/lists (_1 _2) ([d (in-list dom)]) (values (t->sc/neg d) (filter dom-id? (free-ids d)))))
(define pre*
(if (TrueProp? pre)
#f
(t->sc/neg pre)))
(define pre-deps (filter dom-id? (free-ids pre)))
(define rng* (map t->sc rngs))
(define rng-deps
(filter dom-id? (remove-duplicates (apply append (map free-ids rngs)) free-identifier=?)))
(->i/sc (from-typed? typed-side) ids dom* dom-deps pre* pre-deps rng* rng-deps))
(handle-range rng continue)]))

;; Generate a contract for a object/class method clause
;; Precondition: type is a valid method type
(define (t->sc/method type fail typed-side recursive-values loop)
;; helper for mutually recursive calls in Poly cases
(define (rec body #:recursive-values rv)
(t->sc/method body fail typed-side rv loop))
(match type
[(? Poly?)
(t->sc/poly type fail typed-side recursive-values rec)]
[(? PolyDots?)
(t->sc/polydots type fail typed-side recursive-values rec)]
[(? PolyRow?)
(t->sc/polyrow type fail typed-side recursive-values rec)]
[(? Fun?)
(t->sc/function type fail typed-side recursive-values loop #t)]
[(? Poly?) (t->sc/poly type fail typed-side recursive-values rec)]
[(? PolyDots?) (t->sc/polydots type fail typed-side recursive-values rec)]
[(? PolyRow?) (t->sc/polyrow type fail typed-side recursive-values rec)]
[(? Fun?) (t->sc/function type fail typed-side recursive-values loop #t)]
[_ (fail #:reason "invalid method type")]))

(define (is-a-function-type? initial)
Expand Down Expand Up @@ -1546,11 +1523,16 @@
(require racket/extflonum)
(provide nonnegative? nonpositive?
extflonum? extflzero? extflnonnegative? extflnonpositive?)
(define nonnegative? (lambda (x) (>= x 0)))
(define nonpositive? (lambda (x) (<= x 0)))
(define extflzero? (lambda (x) (extfl= x 0.0t0)))
(define extflnonnegative? (lambda (x) (extfl>= x 0.0t0)))
(define extflnonpositive? (lambda (x) (extfl<= x 0.0t0))))
(define (nonnegative? x)
(>= x 0))
(define (nonpositive? x)
(<= x 0))
(define (extflzero? x)
(extfl= x 0.0t0))
(define (extflnonnegative? x)
(extfl>= x 0.0t0))
(define (extflnonpositive? x)
(extfl<= x 0.0t0)))

(module numeric-contracts racket/base
(require
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
#lang racket/base
(require "../rep/type-constr.rkt"
(require racket/lazy-require
racket/match
racket/lazy-require)
"../rep/type-constr.rkt")

(lazy-require ["../types/substitute.rkt"
(subst-all make-simple-substitution)])
Expand Down Expand Up @@ -30,7 +30,8 @@
[_ #f]))

(define (recursive-type-constr? constr)
(match constr
[(struct* TypeConstructor
([real-trep-constr (struct* user-defined-type-op ([recursive? recursive?]))]))
recursive?]))
(match-define (struct* TypeConstructor
([real-trep-constr
(struct* user-defined-type-op ([recursive? recursive?]))]))
constr)
recursive?)
Loading
Loading