Skip to content

Automated Resyntax fixes #1452

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 17 commits into from
May 27, 2025
Merged
Show file tree
Hide file tree
Changes from all 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
14 changes: 6 additions & 8 deletions typed-racket-lib/typed-racket/infer/constraints.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,10 @@

;; add the constraints S <: var <: T to every map in cs
(define (insert cs var S T)
(match cs
[(struct cset (maps))
(make-cset (for/list ([map-entry (in-list maps)])
(match-define (cons map dmap) map-entry)
(cons (hash-set map var (make-c S T))
dmap)))]))
(match-define (struct cset (maps)) cs)
(make-cset (for/list ([map-entry (in-list maps)])
(match-define (cons map dmap) map-entry)
(cons (hash-set map var (make-c S T)) dmap))))

;; meet: Type Type -> Type
;; intersect the given types, producing the greatest lower bound
Expand Down Expand Up @@ -86,8 +84,8 @@
;; produces a cset of all of the maps in all of the given csets
;; FIXME: should this call `remove-duplicates`?
(define (cset-join l)
(let ([mapss (map cset-maps l)])
(make-cset (apply stream-append mapss))))
(define mapss (map cset-maps l))
(make-cset (apply stream-append mapss)))

(define (stream-remove-duplicates st)
(define seen (mutable-set))
Expand Down
122 changes: 52 additions & 70 deletions typed-racket-lib/typed-racket/infer/infer-unit.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -65,34 +65,28 @@
[indices (listof symbol?)]) #:transparent)

(define (context-add-vars ctx vars)
(match ctx
[(context V X Y)
(context V (append vars X) Y)]))
(match-define (context V X Y) ctx)
(context V (append vars X) Y))

(define (context-add-var ctx var)
(match ctx
[(context V X Y)
(context V (cons var X) Y)]))
(match-define (context V X Y) ctx)
(context V (cons var X) Y))

(define (context-add ctx #:bounds [bounds empty] #:vars [vars empty] #:indices [indices empty])
(match ctx
[(context V X Y)
(context (append bounds V) (append vars X) (append indices Y))]))
(match-define (context V X Y) ctx)
(context (append bounds V) (append vars X) (append indices Y)))

(define (inferable-index? ctx bound)
(match ctx
[(context _ _ Y)
(memq bound Y)]))
(match-define (context _ _ Y) ctx)
(memq bound Y))

(define ((inferable-var? ctx) var)
(match ctx
[(context _ X _)
(memq var X)]))
(match-define (context _ X _) ctx)
(memq var X))

(define (empty-cset/context ctx)
(match ctx
[(context _ X Y)
(empty-cset X Y)]))
(match-define (context _ X Y) ctx)
(empty-cset X Y))



Expand Down Expand Up @@ -766,9 +760,8 @@
(list values -Nat)))
(define type
(for/or ([pred-type (in-list possibilities)])
(match pred-type
[(list pred? type)
(and (pred? n) type)])))
(match-define (list pred? type) pred-type)
(and (pred? n) type)))
(cgen/seq context (seq (list type) -null-end) ts*)]
;; numeric? == #true
[((Base-bits: #t _) (SequenceSeq: ts*))
Expand Down Expand Up @@ -917,16 +910,12 @@
;; c : Constaint
;; variance : Variance
(define (constraint->type v variance)
(match v
[(c S T)
(match variance
[(? variance:const?) S]
[(? variance:co?) S]
[(? variance:contra?) T]
[(? variance:inv?) (let ([gS (generalize S)])
(if (subtype gS T)
gS
S))])]))
(match-define (c S T) v)
(match variance
[(? variance:const?) S]
[(? variance:co?) S]
[(? variance:contra?) T]
[(? variance:inv?) (let ([gS (generalize S)]) (if (subtype gS T) gS S))]))

;; Since we don't add entries to the empty cset for index variables (since there is no
;; widest constraint, due to dcon-exacts), we must add substitutions here if no constraint
Expand All @@ -936,47 +925,40 @@
(hash-union
(for/hash ([v (in-list Y)]
#:unless (hash-has-key? S v))
(let ([var (hash-ref idx-hash v variance:const)])
(values v
(match var
[(? variance:const?) (i-subst null)]
[(? variance:co?) (i-subst null)]
[(? variance:contra?) (i-subst/starred null Univ)]
;; TODO figure out if there is a better subst here
[(? variance:inv?) (i-subst null)]))))
(define var (hash-ref idx-hash v variance:const))
(values v
(match var
[(? variance:const?) (i-subst null)]
[(? variance:co?) (i-subst null)]
[(? variance:contra?) (i-subst/starred null Univ)]
;; TODO figure out if there is a better subst here
[(? variance:inv?) (i-subst null)])))
S))
(define (build-subst m)
(match m
[(cons cmap (dmap dm))
(let* ([subst (hash-union
(for/hash ([(k dc) (in-hash dm)])
(define (c->t c) (constraint->type c (hash-ref idx-hash k variance:const)))
(values
k
(match dc
[(dcon fixed #f)
(i-subst (map c->t fixed))]
[(or (dcon fixed rest) (dcon-exact fixed rest))
(i-subst/starred
(map c->t fixed)
(c->t rest))]
[(dcon-dotted fixed dc dbound)
(i-subst/dotted
(map c->t fixed)
(c->t dc)
dbound)])))
(for/hash ([(k v) (in-hash cmap)])
(values k (t-subst (constraint->type v (hash-ref var-hash k variance:const))))))]
[subst (for/fold ([subst subst]) ([v (in-list X)])
(let ([entry (hash-ref subst v #f)])
;; Make sure we got a subst entry for a type var
;; (i.e. just a type to substitute)
;; If we don't have one, there are no constraints on this variable
(if (and entry (t-subst? entry))
subst
(hash-set subst v (t-subst Univ)))))])
;; verify that we got all the important variables
(extend-idxs subst))]))
(match-define (cons cmap (dmap dm)) m)
(let* ([subst (hash-union
(for/hash ([(k dc) (in-hash dm)])
(define (c->t c)
(constraint->type c (hash-ref idx-hash k variance:const)))
(values k
(match dc
[(dcon fixed #f) (i-subst (map c->t fixed))]
[(or (dcon fixed rest) (dcon-exact fixed rest))
(i-subst/starred (map c->t fixed) (c->t rest))]
[(dcon-dotted fixed dc dbound)
(i-subst/dotted (map c->t fixed) (c->t dc) dbound)])))
(for/hash ([(k v) (in-hash cmap)])
(values k (t-subst (constraint->type v (hash-ref var-hash k variance:const))))))]
[subst (for/fold ([subst subst]) ([v (in-list X)])
(define entry (hash-ref subst v #f))
;; Make sure we got a subst entry for a type var
;; (i.e. just a type to substitute)
;; If we don't have one, there are no constraints on this variable
(if (and entry (t-subst? entry))
subst
(hash-set subst v (t-subst Univ))))])
;; verify that we got all the important variables
(extend-idxs subst)))
(if multiple-substitutions?
(for/list ([md (in-stream (cset-maps C))])
(build-subst md))
Expand Down
116 changes: 59 additions & 57 deletions typed-racket-lib/typed-racket/infer/intersect.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -116,20 +116,16 @@
(nbits-intersect nbits1 nbits2))]
[((BaseUnion: bbits nbits)
(Base-bits: numeric? bits))
(cond [numeric? (if (nbits-overlap? nbits bits)
t2
-Bottom)]
[else (if (bbits-overlap? bbits bits)
t2
-Bottom)])]
(cond
[numeric? (if (nbits-overlap? nbits bits) t2 -Bottom)]
[(bbits-overlap? bbits bits) t2]
[else -Bottom])]
[((Base-bits: numeric? bits)
(BaseUnion: bbits nbits))
(cond [numeric? (if (nbits-overlap? nbits bits)
t1
-Bottom)]
[else (if (bbits-overlap? bbits bits)
t1
-Bottom)])]
(cond
[numeric? (if (nbits-overlap? nbits bits) t1 -Bottom)]
[(bbits-overlap? bbits bits) t1]
[else -Bottom])]
[((BaseUnion-bases: bases1) t2)
(apply Un (for/list ([b (in-list bases1)])
(rec b t2 obj)))]
Expand Down Expand Up @@ -161,52 +157,58 @@
;; If the back pointer is never used, we don't create a μ-type, we just
;; return the result
(define (resolvable-intersect initial-t1 initial-t2 seen obj additive?)
(let ([t1 (if (resolvable? initial-t1)
(resolve-once initial-t1)
initial-t1)])
(cond
[(assoc (cons initial-t1 initial-t2) seen)
;; we've seen these types before! -- use the stored symbol
;; as a back pointer with an 'F' type (i.e. a type variable)
=> (match-lambda
[(cons _ record)
;; record that we did indeed use the back
;; pointer by set!-ing the flag
(set-mcdr! record #t)
(make-F (mcar record))])]
;; if t1 is not a fully defined type, do the simple thing
[(not t1) (if additive?
(-unsafe-intersect initial-t1 initial-t2)
initial-t1)]
[else
(let ([t2 (if (resolvable? initial-t2)
(resolve-once initial-t2)
initial-t2)])
(cond
;; if t2 is not a fully defined type, do the simple thing
[(not t2) (if additive?
(-unsafe-intersect t1 initial-t2)
t1)]
[else
;; we've never seen these types together before! let's gensym a symbol
;; so that if we do encounter them again, we can create a μ type.
(define name (gensym 'rec))
;; the 'record' contains the back pointer symbol we may or may not use in
;; the car, and a flag for whether or not we actually used the back pointer
;; in the cdr.
(define record (mcons name #f))
(define seen* (list* (cons (cons initial-t1 initial-t2) record)
(cons (cons initial-t2 initial-t1) record)
seen))
(define t (cond
[additive? (internal-intersect t1 t2 seen* obj)]
[else (internal-restrict t1 t2 seen* obj)]))
(define t1
(if (resolvable? initial-t1)
(resolve-once initial-t1)
initial-t1))
(cond
[(assoc (cons initial-t1 initial-t2) seen)
;; we've seen these types before! -- use the stored symbol
;; as a back pointer with an 'F' type (i.e. a type variable)
=>
(match-lambda
[(cons _ record)
;; record that we did indeed use the back
;; pointer by set!-ing the flag
(set-mcdr! record #t)
(make-F (mcar record))])]
;; if t1 is not a fully defined type, do the simple thing
[(not t1)
(if additive?
(-unsafe-intersect initial-t1 initial-t2)
initial-t1)]
[else
(let ([t2 (if (resolvable? initial-t2)
(resolve-once initial-t2)
initial-t2)])
(cond
;; if t2 is not a fully defined type, do the simple thing
[(not t2)
(if additive?
(-unsafe-intersect t1 initial-t2)
t1)]
[else
;; we've never seen these types together before! let's gensym a symbol
;; so that if we do encounter them again, we can create a μ type.
(define name (gensym 'rec))
;; the 'record' contains the back pointer symbol we may or may not use in
;; the car, and a flag for whether or not we actually used the back pointer
;; in the cdr.
(define record (mcons name #f))
(define seen*
(list* (cons (cons initial-t1 initial-t2) record)
(cons (cons initial-t2 initial-t1) record)
seen))
(define t
(cond
;; check if we used the backpointer, if so,
;; make a recursive type using that name
[(mcdr record) (make-Mu name t)]
;; otherwise just return the result
[else t])]))])))
[additive? (internal-intersect t1 t2 seen* obj)]
[else (internal-restrict t1 t2 seen* obj)]))
(cond
;; check if we used the backpointer, if so,
;; make a recursive type using that name
[(mcdr record) (make-Mu name t)]
;; otherwise just return the result
[else t])]))]))


;; intersect
Expand Down
28 changes: 7 additions & 21 deletions typed-racket-lib/typed-racket/infer/promote-demote.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
[var-demote (c:-> Type? (c:listof symbol?) Type?)])

(define (V-in? V . ts)
(for/or ([e (in-list (append* (map fv ts)))])
(for/or ([e (in-list (append-map fv ts))])
(memq e V)))

;; get-propset : SomeValues -> PropSet
Expand All @@ -39,26 +39,12 @@
;; arr? -> (or/c #f arr?)
;; Returns the changed arr or #f if there is no arr above it
(define (arr-change arr)
(match arr
[(Arrow: dom rst kws rng rng-T+)
(cond
[(apply V-in? V (get-propsets rng))
#f]
[(and (RestDots? rst)
(memq (RestDots-nm rst) V))
(make-Arrow
(map contra dom)
(contra (RestDots-ty rst))
(map contra kws)
(co rng)
rng-T+)]
[else
(make-Arrow
(map contra dom)
(and rst (contra rst))
(map contra kws)
(co rng)
rng-T+)])]))
(match-define (Arrow: dom rst kws rng rng-T+) arr)
(cond
[(apply V-in? V (get-propsets rng)) #f]
[(and (RestDots? rst) (memq (RestDots-nm rst) V))
(make-Arrow (map contra dom) (contra (RestDots-ty rst)) (map contra kws) (co rng) rng-T+)]
[else (make-Arrow (map contra dom) (and rst (contra rst)) (map contra kws) (co rng) rng-T+)]))
(define (change-elems ts)
(for/list ([t (in-list ts)])
(if (V-in? V t)
Expand Down
Loading