Skip to content
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

Added TreeLists to Typed-Racket along with type-checking tests. #1439

Merged
merged 5 commits into from
Mar 21, 2025
Merged
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
Original file line number Diff line number Diff line change
Expand Up @@ -352,6 +352,8 @@ corresponding to @racket[trest], where @racket[bound]
@deftypeconstr[(MListof t)]{Returns the type of a homogeneous @rtech{mutable list} of @racket[t].}
@deftypeconstr[(MPairof t u)]{Returns the type of a @rtech{Mutable pair} of @racket[t] and @racket[u].}

@deftypeconstr[(TreeListof t)]{Returns the type of @rtech{treelist} of @racket[t]}

@deftype[MPairTop]{Is the type of a @rtech{mutable pair} with unknown
element types and is the supertype of all mutable pair types.
This type typically appears in programs via the combination of
Expand Down
51 changes: 51 additions & 0 deletions typed-racket-lib/typed-racket/base-env/base-env.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
racket/unsafe/ops
racket/unsafe/undefined
racket/hash
racket/treelist
(only-in racket/extflonum floating-point-bytes->extfl extfl->floating-point-bytes)
;(only-in rnrs/lists-6 fold-left)
'#%paramz
Expand Down Expand Up @@ -1294,6 +1295,56 @@

[unsafe-undefined -Unsafe-Undefined]

;; Section 4.21 (TreeLists)

[treelist (-poly (a) (->* (list) a (-treelist a)))]
[treelist-empty? (-> (-treelist Univ) B)]
[treelist-length (-> (-treelist Univ) -Index)]
[treelist-member?
(-poly (a)
(cl->* ((-treelist a) a . -> . Univ)
((-treelist a) a (-> a a Univ) . -> . B)))]
[treelist-first (-poly (a) (-> (-treelist a) a :T+ #f))]
[treelist-last (-poly (a) (-> (-treelist a) a :T+ #f))]
[treelist-rest (-poly (a) (-> (-treelist a) (-treelist a)))]
[treelist-add (-poly (a) (-> (-treelist a) a (-treelist a)))]
[treelist-cons (-poly (a) (-> (-treelist a) a (-treelist a)))]
[treelist-delete (-poly (a) (-> (-treelist a) -Index (-treelist a)))]
[make-treelist (-poly (a) (-> -Nat a (-treelist a)))]
[treelist-ref (-poly (a) (-> (-treelist a) -Index a :T+ #f))]
[treelist-insert (-poly (a) (-> (-treelist a) -Index a (-treelist a)))]
[treelist-set (-poly (a) (-> (-treelist a) -Index a (-treelist a)))]
[treelist-take (-poly (a) (-> (-treelist a) -Index (-treelist a)))]
[treelist-drop (-poly (a) (-> (-treelist a) -Index (-treelist a)))]
[treelist-take-right (-poly (a) (-> (-treelist a) -Index (-treelist a)))]
[treelist-drop-right (-poly (a) (-> (-treelist a) -Index (-treelist a)))]
[treelist-sublist (-poly (a) (-> (-treelist a) -Index -Index (-treelist a)))]
[treelist-reverse (-poly (a) (-> (-treelist a) (-treelist a)))]
[treelist->list (-poly (a) (-> (-treelist a) (-lst a)))]
[list->treelist (-poly (a) (-> (-lst a) (-treelist a)))]
[treelist->vector (-poly (a) (-> (-treelist a) (-vec a)))]
[vector->treelist (-poly (a) (-> (-vec a) (-treelist a)))]
[in-treelist (-poly (a) (-> (-treelist a) (-seq a)))]
[treelist? (unsafe-shallow:make-pred-ty (-treelist Univ))]
[treelist-append (-poly (a) (->* (list) (-treelist a) (-treelist a)))]
[treelist-map (-poly (a b) (-> (-treelist a) (-> a b) (-treelist b)))]
[treelist-for-each (-poly (a b) (-> (-treelist a) (-> a b) -Void))]
[treelist-filter (-poly (a) (-> (-> a Univ) (-treelist a) (-treelist a)))]
[treelist-find (-poly (a) (-> (-treelist a) (-> a Univ) a :T+ #f))]
[treelist-index-of
(-poly (a)
(cl->* ((-treelist a) a . -> . -Index)
((-treelist a) a (-> a a Univ) . -> . -Index)))]
[treelist-flatten (Univ . -> . (-treelist Univ))]
[treelist-append* (-poly (a) (-> (-treelist (-treelist a)) (-treelist a)))]
[treelist-sort
(-poly
(a b)
(cl->*
(->key (-treelist a) (-> a a -Boolean) #:key (-opt (-> a a :T+ #f)) #f #:cache-keys? -Boolean #f (-treelist a))
(->key (-treelist a) (-> b b -Boolean) #:key (-> a b :T+ #f) #t #:cache-keys? -Boolean #f (-treelist a))))]


;; Section 5.2 (Structure Types)
[make-struct-type
(->opt -Symbol
Expand Down
1 change: 1 addition & 0 deletions typed-racket-lib/typed-racket/base-env/base-types.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -197,6 +197,7 @@
[Async-Channelof -async-channel]
[Ephemeronof -Ephemeron]
[Setof -set]
[TreeListof -treelist]
[Evtof -evt]
[Continuation-Mark-Set -Cont-Mark-Set]
[False -False]
Expand Down
2 changes: 2 additions & 0 deletions typed-racket-lib/typed-racket/env/init-envs.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,8 @@
`(-CustodianBox ,(type->sexp ty))]
[(Set: ty)
`(make-Set ,(type->sexp ty))]
[(TreeList: ty)
`(make-TreeList ,(type->sexp ty))]
[(Evt: ty)
`(make-Evt ,(type->sexp ty))]
[(Future: ty)
Expand Down
2 changes: 2 additions & 0 deletions typed-racket-lib/typed-racket/infer/infer-unit.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -827,6 +827,8 @@
(cg e e*)]
[((Set: a) (Set: a*))
(cg a a*)]
[((TreeList: a) (TreeList: a*))
(cg a a*)]
[((Evt: a) (Evt: a*))
(cg a a*)]
[((? Base:Semaphore?) (Evt: t))
Expand Down
3 changes: 3 additions & 0 deletions typed-racket-lib/typed-racket/private/type-contract.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@
racket/format
racket/string
racket/set
racket/treelist
syntax/flatten-begin
(only-in "../types/abbrev.rkt" -Bottom -Boolean)
"../static-contracts/instantiate.rkt"
Expand Down Expand Up @@ -564,6 +565,7 @@
[(? Fun? t) (t->sc/fun t)]
[(? DepFun? t) (t->sc/fun t)]
[(Set: t) (set/sc (t->sc t))]
[(TreeList: t) (treelist/sc (t->sc t))]
[(Sequence: (list t))
#:when (subtype t:-Nat t)
;; sequence/c is always a wrapper, so avoid it when we just have a number
Expand Down Expand Up @@ -930,6 +932,7 @@
none/sc
(make-procedure-arity-flat/sc num-mand-args '() '()))]
[(Set: _) set?/sc]
[(TreeList: _) treelist?/sc]
[(or (Sequence: _)
(SequenceTop:)
(SequenceDots: _ _ _))
Expand Down
1 change: 1 addition & 0 deletions typed-racket-lib/typed-racket/rep/type-mask.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -143,6 +143,7 @@
mask:future
mask:other-box
mask:set
mask:treelist
mask:procedure
mask:prompt-tag
mask:continuation-mark-key
Expand Down
7 changes: 7 additions & 0 deletions typed-racket-lib/typed-racket/rep/type-rep.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -353,6 +353,13 @@
(def-structural Set ([elem #:covariant])
[#:mask mask:set])

;;------
;; Treelist (Immutable)
;;------

(def-structural TreeList ([elem #:covariant])
[#:mask mask:treelist])

;;------------
;; HashTable
;;------------
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@
racket/list
racket/promise
racket/set
racket/treelist
racket/unit)
"simple.rkt"
"structural.rkt")
Expand All @@ -30,6 +31,9 @@
(define set?/sc (flat/sc #'(lambda (x) (or (set? x) (set-mutable? x) (set-weak? x)))))
(define empty-set/sc (and/sc set?/sc (flat/sc #'set-empty?)))

(define treelist?/sc (flat/sc #'treelist?))
(define empty-treelist/sc (and/sc treelist?/sc (flat/sc #'treelist-empty?)))

(define vector?/sc (flat/sc #'vector?))
(define immutable-vector?/sc (and/sc vector?/sc
(flat/sc #'immutable?)))
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,12 @@
racket/match
(for-syntax racket/base racket/syntax syntax/stx syntax/parse)
racket/set
racket/treelist
racket/sequence
(for-template racket/base
racket/contract/base
racket/set
racket/treelist
racket/async-channel
racket/sequence
racket/promise
Expand Down Expand Up @@ -160,6 +162,7 @@
((listof/sc (#:covariant)) listof #:flat)
((cons/sc (#:covariant) (#:covariant)) cons/c #:flat)
((set/sc (#:covariant #:chaperone)) set/c #:flat)
((treelist/sc (#:covariant #:chaperone)) treelist/c #:flat)
((struct-property/sc (#:invariant)) struct-type-property/c #:impersonator)
((immutable-vectorof/sc (#:covariant)) immutable-vectorof/c #:flat)
((mutable-vectorof/sc (#:invariant)) mutable-vectorof/c #:chaperone)
Expand Down
1 change: 1 addition & 0 deletions typed-racket-lib/typed-racket/types/abbrev.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@
(define -thread-cell make-ThreadCell)
(define -Promise make-Promise)
(define -set make-Set)
(define -treelist make-TreeList)
(define -mvec make-Mutable-Vector)
(define -ivec make-Immutable-Vector)

Expand Down
1 change: 1 addition & 0 deletions typed-racket-lib/typed-racket/types/printer.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -687,6 +687,7 @@
[(Ephemeron: e) `(Ephemeronof ,(t->s e))]
[(CustodianBox: e) `(CustodianBoxof ,(t->s e))]
[(Set: e) `(Setof ,(t->s e))]
[(TreeList: e) `(TreeListof ,(t->s e))]
[(Evt: r) `(Evtof ,(t->s r))]
[(? Union? (app normalize-type type))
(match type
Expand Down
6 changes: 6 additions & 0 deletions typed-racket-lib/typed-racket/types/subtype.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -1278,6 +1278,12 @@
[(? ThreadCellTop?) A]
[(ThreadCell: elem2) (type≡? A elem1 elem2)]
[_ (continue<: A t1 t2 obj)])]
[(case: TreeList (TreeList: elem1))
(match t2
[(TreeList: elem2) (subtype* A elem1 elem2)]
[(SequenceTop:) A]
[(Sequence: (list seq-t)) (subtype* A elem1 seq-t)]
[_ (continue<: A t1 t2 obj)])]
[(case: Union (Union/set: base1 ts1 elems1))
(let ([A (subtype* A base1 t2 obj)])
(and A
Expand Down
9 changes: 9 additions & 0 deletions typed-racket-test/succeed/treelist-contract.rkt
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
#lang typed/racket

(require racket/treelist)

(define-predicate string-treelist? (TreeListof String))

(string-treelist? (treelist 1 2 3))

(string-treelist? (treelist "1" "2" "3"))
69 changes: 69 additions & 0 deletions typed-racket-test/succeed/treelist.rkt
Original file line number Diff line number Diff line change
@@ -0,0 +1,69 @@
#lang typed/racket

(require racket/treelist)

(define tl (treelist 0 1 2 3))

(treelist-empty? tl)

(treelist-length tl)

(treelist-member? tl 1)

(treelist-first tl)

(treelist-rest tl)

(treelist-last tl)

(treelist-add tl 1)

(treelist-cons tl 1)

(treelist-delete tl 1)

(make-treelist 5 1)

(treelist-ref tl 1)

(treelist-insert tl 1 1)

(treelist-set tl 0 1)

(treelist-take tl 2)

(treelist-take tl 2)
(treelist-drop tl 2)
(treelist-take-right tl 2)
(treelist-drop-right tl 2)

(treelist-sublist tl 1 3)

(treelist-reverse tl)

(treelist->list tl)
(list->treelist (list 0 1 2 3))

(treelist->vector tl)
(vector->treelist (vector 0 1 2 3))

(treelist? treelist)

(treelist-append tl tl tl)

(treelist-map tl (λ ([x : Byte]) (+ x 1)))

(treelist-for-each tl (λ ([x : Byte]) (+ x 1)))

(treelist-filter (λ ([x : Byte]) (equal? x 1)) tl)

(treelist-find tl (λ ([x : Byte]) (equal? x 1)))

(treelist-index-of tl 3)
(treelist-index-of tl 3 equal?)

(treelist-flatten (treelist tl tl))

(treelist-append (treelist (treelist tl) tl))

(treelist-sort tl >)
5 changes: 5 additions & 0 deletions typed-racket-test/unit-tests/subtype-tests.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -179,6 +179,7 @@
[make-Immutable-Vector ()]
[make-Immutable-HashTable () ()]
[make-Set ()]
[make-TreeList ()]
[make-Evt ()]
[make-Syntax ()]
[make-Future ()])
Expand Down Expand Up @@ -298,6 +299,10 @@
[(-mu x (make-Listof x)) (-mu x* (make-Listof x*))]
[(-pair -Number -Number) (-pair Univ -Number)]
[(-pair -Number -Number) (-pair -Number -Number)]
;; simple treelist types
[(-treelist -Number) (-treelist Univ)]
[(-treelist -Number) (-treelist -Number)]
[FAIL (-treelist -Number) (-treelist -Symbol)]
;; from page 7 (my favorite page! But seriously, page 7 of... what???)
[(-mu t (-> t t)) (-mu s (-> s s))]
[(-mu s (-> -Number s)) (-mu t (-> -Number (-> -Number t)))]
Expand Down
57 changes: 57 additions & 0 deletions typed-racket-test/unit-tests/typecheck-tests.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -381,6 +381,7 @@
racket/port
racket/sequence
racket/set
racket/treelist
racket/string
racket/system
racket/tcp
Expand Down Expand Up @@ -1900,6 +1901,62 @@
(tc-e (list->seteqv (list 'one 'two)) (-set (one-of/c 'one 'two)))
(tc-e (set->list (set 'one 'two)) (-lst (one-of/c 'one 'two)))

;;Treelist operations

(tc-e (treelist-empty? (treelist)) -Boolean)
(tc-e (treelist-empty? (treelist "a" "b")) -Boolean)
(tc-e (treelist-length (treelist "a" "b" "c")) -Index)
(tc-e (treelist-member? (treelist 1) 1 =) -Boolean)
(tc-e (treelist-first (treelist "a")) -String)
(tc-e (treelist-last (treelist "a")) -String)
(tc-e (treelist-rest (treelist "a" "b")) (-treelist -String))
(tc-e (treelist-add (treelist "a") "b") (-treelist -String))
(tc-e (treelist-cons (treelist "a") "b") (-treelist -String))
(tc-e (treelist-cons (treelist "a") 9) (-treelist (t:Un -PosByte -String)))
(tc-e (treelist-delete (treelist "a") 0) (-treelist -String))
(tc-err (treelist-delete (treelist "a") "b"))
(tc-e (make-treelist 5 "a") (-treelist -String))
(tc-e (treelist-ref (treelist "a" "b") 1) -String)
(tc-err (treelist-ref (treelist "a" "b") "b"))
(tc-e (treelist-insert (treelist "a" "c") 1 "b") (-treelist -String))
(tc-e (treelist-insert (treelist "a" "c") 1 9) (-treelist (t:Un -PosByte -String)))
(tc-err (treelist-insert (treelist "a" "c") "b" "b"))
(tc-e (treelist-set (treelist "a" "c") 1 "b") (-treelist -String))
(tc-e (treelist-set (treelist "a" "c") 1 9) (-treelist (t:Un -PosByte -String)))
(tc-err (treelist-set (treelist "a" "c") "b" "b"))
(tc-e (treelist-take (treelist "a" "b") 1) (-treelist -String))
(tc-err (treelist-take (treelist "a" "b") "a"))
(tc-e (treelist-drop (treelist "a" "b") 1) (-treelist -String))
(tc-err (treelist-drop (treelist "a" "b") "a"))
(tc-e (treelist-take-right (treelist "a" "b") 1) (-treelist -String))
(tc-err (treelist-take-right (treelist "a" "b") "a"))
(tc-e (treelist-drop-right (treelist "a" "b") 1) (-treelist -String))
(tc-err (treelist-drop-right (treelist "a" "b") "a"))
(tc-e (treelist-sublist (treelist "a" "b" "c") 1 2) (-treelist -String))
(tc-err (treelist-sublist (treelist "a" "b" "c") 1 "c"))
(tc-err (treelist-sublist (treelist "a" "b" "c") "b" 1))
(tc-e (treelist-reverse (treelist "a" "b")) (-treelist -String))
(tc-e (treelist->list (treelist "a")) (-lst -String))
(tc-e (treelist->vector (treelist "a")) (-vec -String))
;;(tc-e (in-treelist (treelist "a")) (-seq -String)) FIXME: "missing type identifier"
(tc-e (list->treelist (list "a")) (-treelist -String))
(tc-e (vector->treelist (vector "a")) (-treelist -String))
(tc-e (treelist? (treelist "a")) #:ret (tc-ret -Boolean -true-propset))
(tc-e (treelist? (list "a")) #:ret (tc-ret -Boolean -false-propset))
(tc-e (treelist-append (treelist "a") (treelist "b")) (-treelist -String))
(tc-e (treelist-append (treelist "a") (treelist "b") (treelist "c")) (-treelist -String))
(tc-e (treelist-append (treelist "a") (treelist 9)) (-treelist (t:Un -PosByte -String)))
(tc-e (treelist-map (treelist "a" "b") (λ (x) "c")) (-treelist -String))
(tc-e (treelist-map (treelist "a" "b") (λ (x) 9)) (-treelist -PosByte))
(tc-e (treelist-for-each (treelist "a" "b") (λ (x) x)) -Void)
(tc-e (treelist-find (treelist "a" "b") (λ (x) (if (equal? x "a") #t #f))) -String)
(tc-e (treelist-filter even? (treelist 1 2 3 4 5)) (-treelist -PosByte))
(tc-e (treelist-flatten (treelist (treelist (treelist (treelist "a"))))) (-treelist Univ))
(tc-e (treelist-flatten "a") (-treelist Univ))
(tc-e (treelist-append* (treelist (treelist "a" "b") (treelist "c" (treelist "d") "e") (treelist))) (-treelist Univ))
(tc-e (treelist-index-of (treelist "a" "b" "c") "b") -Index)
(tc-e (treelist-index-of (treelist "a" "b" "c") "b" equal?) -Index)
(tc-e (treelist-sort (treelist "c" "a" "b") string<?) (-treelist -String))

;Syntax

Expand Down