Skip to content
Merged
Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
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
Original file line number Diff line number Diff line change
Expand Up @@ -169,7 +169,7 @@
#:with ty #'t))
(define-splicing-syntax-class optional-standalone-annotation
(pattern (~optional a:standalone-annotation)
#:attr ty (if (attribute a) #'a.ty #f)))
#:attr ty (and (attribute a) #'a.ty)))

(define-syntax-class type-variables
#:attributes ((vars 1))
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,64 +25,63 @@
#:property prop:combinator-name "dep->/sc"
#:methods gen:sc
[(define (sc->contract v rec)
(match v
[(->i/sc typed-side? ids dom/scs dom-deps pre pre-deps rng/scs rng-deps)
(with-syntax ([(id ...) ids]
[(c ...) (for/list ([d/sc (in-list dom/scs)]
[dep-ids (in-list dom-deps)])
(cond
[(not (null? dep-ids))
(parameterize ([static-contract-may-contain-free-ids? #t])
(rec d/sc))]
[else (rec d/sc)]))]
[(dep ...) dom-deps]
[(r-deps ...) rng-deps]
[(p-deps ...) pre-deps])
#`(->i ([id dep c] ...)
#,@(cond
[(not pre) #'()]
[else #`(#:pre (p-deps ...)
#,(cond
[(not (null? pre-deps))
(parameterize ([static-contract-may-contain-free-ids? #t])
(rec pre))]
[else (rec pre)]))])
#,(cond
[(and typed-side? (andmap any/sc? rng-deps)) #'any]
[(null? rng-deps)
#`[_ () (values #,@(map rec rng/scs))]]
[else
(parameterize ([static-contract-may-contain-free-ids? #t])
#`[_ (r-deps ...) (values #,@(map rec rng/scs))])])))]))
(match-define (->i/sc typed-side? ids dom/scs dom-deps pre pre-deps rng/scs rng-deps) v)
(with-syntax ([(id ...) ids]
[(c ...) (for/list ([d/sc (in-list dom/scs)]
[dep-ids (in-list dom-deps)])
(cond
[(not (null? dep-ids))
(parameterize ([static-contract-may-contain-free-ids? #t])
(rec d/sc))]
[else (rec d/sc)]))]
[(dep ...) dom-deps]
[(r-deps ...) rng-deps]
[(p-deps ...) pre-deps])
#`(->i ([id dep c] ...)
#,@(cond
[(not pre) #'()]
[else
#`(#:pre (p-deps ...)
#,(cond
[(not (null? pre-deps))
(parameterize ([static-contract-may-contain-free-ids? #t])
(rec pre))]
[else (rec pre)]))])
#,(cond
[(and typed-side? (andmap any/sc? rng-deps)) #'any]
[(null? rng-deps) #`[_ () (values #,@(map rec rng/scs))]]
[else
(parameterize ([static-contract-may-contain-free-ids? #t])
#`[_ (r-deps ...) (values #,@(map rec rng/scs))])]))))
(define (sc-map v f)
(match v
[(->i/sc typed-side? ids dom/scs dom-deps pre pre-deps rng/scs rng-deps)
(->i/sc typed-side?
ids
(for/list ([d/sc (in-list dom/scs)])
(f d/sc 'contravariant))
dom-deps
(and pre (f pre 'contravariant))
pre-deps
(for/list ([r/sc (in-list rng/scs)])
(f r/sc 'covariant))
rng-deps)]))
(match-define (->i/sc typed-side? ids dom/scs dom-deps pre pre-deps rng/scs rng-deps) v)
(->i/sc typed-side?
ids
(for/list ([d/sc (in-list dom/scs)])
(f d/sc 'contravariant))
dom-deps
(and pre (f pre 'contravariant))
pre-deps
(for/list ([r/sc (in-list rng/scs)])
(f r/sc 'covariant))
rng-deps))
(define (sc-traverse v f)
(match v
[(->i/sc _ _ dom/scs _ pre _ rng/scs _)
(for ([d/sc (in-list dom/scs)])
(f d/sc 'contravariant))
(when pre (f pre 'contravariant))
(for ([r/sc (in-list rng/scs)])
(f r/sc 'covariant))]))
(match-define (->i/sc _ _ dom/scs _ pre _ rng/scs _) v)
(for ([d/sc (in-list dom/scs)])
(f d/sc 'contravariant))
(when pre
(f pre 'contravariant))
(for ([r/sc (in-list rng/scs)])
(f r/sc 'covariant)))
(define (sc-terminal-kind v) 'impersonator)
(define (sc->constraints v f)
(match v
[(->i/sc _ _ dom/scs _ pre _ rng/scs _)
(merge-restricts* 'impersonator
(append (if pre (list (f pre)) (list))
(map f rng/scs)
(map f dom/scs)))]))])
(match-define (->i/sc _ _ dom/scs _ pre _ rng/scs _) v)
(merge-restricts* 'impersonator
(append (if pre
(list (f pre))
(list))
(map f rng/scs)
(map f dom/scs))))])

(require-for-cond-contract "proposition.rkt")

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,9 @@
#:transparent
#:property prop:combinator-name "unit/sc"
#:methods gen:sc
[(define (sc-map v f)
(match v
[(unit-combinator unit-spec)
(unit-combinator (unit-spec-sc-map f unit-spec))]))
[(define (sc-map v f)
(match-define (unit-combinator unit-spec) v)
(unit-combinator (unit-spec-sc-map f unit-spec)))
(define (sc-traverse v f)
(match v
[(unit-combinator unit-spec)
Expand Down
47 changes: 16 additions & 31 deletions typed-racket-lib/typed-racket/types/base-abbrev.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -102,15 +102,11 @@
(foldr -pair b l))

;; Recursive types
(define-syntax -v
(syntax-rules ()
[(_ x) (make-F 'x)]))
(define-syntax-rule (-v x)
(make-F 'x))

(define-syntax -mu
(syntax-rules ()
[(_ var ty)
(let ([var (-v var)])
(make-Mu 'var ty))]))
(define-syntax-rule (-mu var ty)
(let ([var (-v var)]) (make-Mu 'var ty)))

;; Results
(define/cond-contract (-result t [pset -tt-propset] [o -empty-obj])
Expand Down Expand Up @@ -493,31 +489,20 @@


;; Convenient syntax for polymorphic types
(define-syntax -poly
(syntax-rules ()
[(_ (vars ...) ty)
(let ([vars (-v vars)] ...)
(make-Poly (list 'vars ...) ty))]))

(define-syntax -polydots
(syntax-rules ()
[(_ (vars ... dotted) ty)
(let ([dotted (-v dotted)]
[vars (-v vars)] ...)
(make-PolyDots (list 'vars ... 'dotted) ty))]))

(define-syntax -polyrow
(syntax-rules ()
[(_ (var) consts ty)
(let ([var (-v var)])
(make-PolyRow (list 'var) ty consts))]))
(define-syntax-rule (-poly (vars ...) ty)
(let ([vars (-v vars)] ...) (make-Poly (list 'vars ...) ty)))

(define-syntax-rule (-polydots (vars ... dotted) ty)
(let ([dotted (-v dotted)]
[vars (-v vars)] ...)
(make-PolyDots (list 'vars ... 'dotted) ty)))

(define-syntax-rule (-polyrow (var) consts ty)
(let ([var (-v var)]) (make-PolyRow (list 'var) ty consts)))

;; abbreviation for existential types
(define-syntax -some
(syntax-rules ()
[(_ (vars ...) ty)
(let ([vars (-v vars)] ...)
(make-Some (list 'vars ...) ty))]))
(define-syntax-rule (-some (vars ...) ty)
(let ([vars (-v vars)] ...) (make-Some (list 'vars ...) ty)))

;; abbreviation for existential type results
(define-syntax -some-res
Expand Down
18 changes: 9 additions & 9 deletions typed-racket-lib/typed-racket/types/generalize.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -45,15 +45,15 @@
[(Pair: t1 (== -Null)) (-lst t1)]
[(MPair: t1 (== -Null)) (-mlst t1)]
[(or (Pair: t1 t2) (MPair: t1 t2))
(let ([t-new (loop t2)])
(define -lst-type
((match t*
[(Pair: _ _) -lst]
[(MPair: _ _) -mlst])
t1))
(if (type-equiv? -lst-type t-new)
-lst-type
(exit t)))]
(define t-new (loop t2))
(define -lst-type
((match t*
[(Pair: _ _) -lst]
[(MPair: _ _) -mlst])
t1))
(if (type-equiv? -lst-type t-new)
-lst-type
(exit t))]
[(ListDots: t bound) (-lst (substitute Univ bound t))]
[(? (lambda (t) (subtype t -Symbol))) -Symbol]
[(== -True) -Boolean]
Expand Down
64 changes: 33 additions & 31 deletions typed-racket-lib/typed-racket/types/kw-types.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -172,36 +172,38 @@
;; set and set->list to retain determinism
(remove-duplicates
(for/list ([(arrow arrow-mand-arg-count) (in-assoc mand-arg-table)])
(match arrow
[(Arrow: dom rst kws rng rng-T+)
(define kws* (if actual-kws
(handle-extra-or-missing-kws kws actual-kws)
kws))
(define kw-opts-supplied (if actual-kws
(lambda-kws-opt-supplied actual-kws)
'()))
(define mand-arg-count (if actual-kws
(lambda-kws-pos-mand-count actual-kws)
arrow-mand-arg-count))
(define opt-arg-count (- (length dom) mand-arg-count))
(define extra-opt-arg-count
;; In case `dom` has too many arguments that we try to treat
;; as optional:
(if actual-kws
(max 0 (- opt-arg-count (length (lambda-kws-pos-opt-supplied? actual-kws))))
0))
(convert kws*
kw-opts-supplied
(take dom mand-arg-count)
(drop dom mand-arg-count)
(if actual-kws
(append (lambda-kws-pos-opt-supplied? actual-kws)
(make-list extra-opt-arg-count #f))
(make-list opt-arg-count #f))
rng
rst
split?
rng-T+)]))))
(match-define (Arrow: dom rst kws rng rng-T+) arrow)
(define kws*
(if actual-kws
(handle-extra-or-missing-kws kws actual-kws)
kws))
(define kw-opts-supplied
(if actual-kws
(lambda-kws-opt-supplied actual-kws)
'()))
(define mand-arg-count
(if actual-kws
(lambda-kws-pos-mand-count actual-kws)
arrow-mand-arg-count))
(define opt-arg-count (- (length dom) mand-arg-count))
(define extra-opt-arg-count
;; In case `dom` has too many arguments that we try to treat
;; as optional:
(if actual-kws
(max 0 (- opt-arg-count (length (lambda-kws-pos-opt-supplied? actual-kws))))
0))
(convert kws*
kw-opts-supplied
(take dom mand-arg-count)
(drop dom mand-arg-count)
(if actual-kws
(append (lambda-kws-pos-opt-supplied? actual-kws)
(make-list extra-opt-arg-count #f))
(make-list opt-arg-count #f))
rng
rst
split?
rng-T+))))
(apply cl->* fns))

;; kw-convert : Type (Option LambdaKeywords) [Boolean] -> Type
Expand Down Expand Up @@ -269,7 +271,7 @@
(take opt-types to-take))
(erase-props/Values rng)
#:kws actual-kws
#:rest (if (= to-take opt-types-count) rest-type #f)
#:rest (and (= to-take opt-types-count) rest-type)
#:T+ rng-T+)))]
[else (int-err "unsupported arrs in keyword function type")])]
[(Poly-names: names f) (make-Poly names (loop f))]
Expand Down
49 changes: 23 additions & 26 deletions typed-racket-lib/typed-racket/types/printer.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -149,20 +149,19 @@
;; instead of (<= x y) (<= y x) when we have both inequalities
(define-values (leqs others) (partition LeqProp? ps))
(define-values (eqs simple-leqs)
(for/fold ([eqs '()] [simple-leqs '()])
(for/fold ([eqs '()]
[simple-leqs '()])
([leq (in-list leqs)])
(match leq
[(LeqProp: lhs rhs)
(define flip (-leq rhs lhs))
(cond
[(not (member flip leqs))
(values eqs (cons leq simple-leqs))]
[(member flip eqs) (values eqs simple-leqs)]
[else (values (cons leq eqs) simple-leqs)])])))
(match-define (LeqProp: lhs rhs) leq)
(define flip (-leq rhs lhs))
(cond
[(not (member flip leqs)) (values eqs (cons leq simple-leqs))]
[(member flip eqs) (values eqs simple-leqs)]
[else (values (cons leq eqs) simple-leqs)])))
(let ([simple-leqs (map prop->sexp simple-leqs)]
[eqs (for/list ([leq (in-list eqs)])
(match leq
[(LeqProp: lhs rhs) `(= ,(object->sexp lhs) ,(object->sexp rhs))]))]
(match-define (LeqProp: lhs rhs) leq)
`(= ,(object->sexp lhs) ,(object->sexp rhs)))]
[others (map prop->sexp others)])
(match (append eqs simple-leqs others)
[(list sexp) sexp]
Expand Down Expand Up @@ -365,11 +364,10 @@
;; as long as the resulting s-expressions are `display`ed
;; this is fine, though it may not pretty-print well.
(for/list ([kw (in-list kws)])
(match kw
[(Keyword: k t req?)
(if req?
(format "~a ~a" k (type->sexp t))
(format "[~a ~a]" k (type->sexp t)))]))
(match-define (Keyword: k t req?) kw)
(if req?
(format "~a ~a" k (type->sexp t))
(format "[~a ~a]" k (type->sexp t))))
(match rst
[(Rest: (list rst-t)) `(,(type->sexp rst-t) *)]
[(Rest: rst-ts) `(#:rest-star ,(map type->sexp rst-ts))]
Expand Down Expand Up @@ -478,16 +476,15 @@
;; case-lambda->sexp : Type -> S-expression
;; Convert a case-> type to an s-expression
(define (case-lambda->sexp type)
(match type
[(Fun: arrows)
(match arrows
[(list) '(case->)]
[(list a) (arr->sexp a)]
[(and arrs (list a b ...))
(define cover (cover-case-lambda arrs))
(if (> (length cover) 1)
`(case-> ,@cover)
(car cover))])]))
(match-define (Fun: arrows) type)
(match arrows
[(list) '(case->)]
[(list a) (arr->sexp a)]
[(and arrs (list a b ...))
(define cover (cover-case-lambda arrs))
(if (> (length cover) 1)
`(case-> ,@cover)
(car cover))]))

;; class->sexp : Class [#:object? Boolean] -> S-expression
;; Convert a class or object type to an s-expression
Expand Down
Loading