flexible-with2.hl.rkt (41529B)
1 #lang hyper-literate #:꩜ #:no-auto-require (dotlambda/unhygienic 2 . type-expander/lang) 3 4 ꩜require[scriblib/footnote 5 scriblib/figure 6 hyper-literate/diff1 7 hyper-literate/spoiler1 8 racket/runtime-path 9 scribble-math 10 (for-label delay-pure 11 "flexible-with-utils.hl.rkt" 12 phc-toolkit/syntax-parse 13 (rename-in racket/base [... …]) 14 syntax/parse 15 syntax/stx 16 racket/syntax 17 racket/list 18 syntax/id-table 19 racket/set 20 racket/sequence 21 racket/vector 22 racket/contract 23 type-expander/expander 24 ;phc-toolkit/untyped/syntax-parse 25 racket/base 26 (prefix-in tr: (only-in typed/racket ∀)) 27 racket/splicing)] 28 29 ꩜require[scribble/core 30 scribble/html-properties] 31 32 ꩜title[#:style (with-html5 manual-doc-style) 33 #:tag "flexible-with" 34 #:tag-prefix "phc-graph/flexible-with"]{Flexible functional 35 modification and extension of records} 36 37 ꩜(chunks-toc-prefix 38 '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)" 39 "phc-graph/flexible-with")) 40 41 ꩜elem[#:style (style #f (list (css-addition 42 #" 43 .Figure, 44 .FigureMulti, 45 .FigureMultiWide, 46 .Herefigure { 47 border-color: #b5b5b5 !important; 48 }")))] 49 50 ꩜section{Goals} 51 52 Our goal here is to have strongly typed records, with row polymorphism (a 53 ꩜racket[Rest] row type variable can range over multiple possibly-present 54 fields), and structural type equivalence (two record types are identical if 55 they have the same fields and the type of the fields is the same in both record 56 types). 57 58 ꩜section{Overview} 59 60 We represent a flexible record as a tree, where the leaves are field values. 61 Every field which occurs anywhere in the program is assigned a constant index. 62 This index determines which leaf is used to store that field's values. In 63 order to avoid storing in-memory a huge tree for every record, the actual 64 fields are captured by a closure, and the tree is lazily generated (node by 65 node) upon access. 66 67 The type for a flexible record can support row polymorphism: the type of 68 fields which may optionally be present are represented by a polymorphic type 69 ꩜; TODO: "not only one" sounds like "¬only … but also" instead of "¬limited to…" 70 variable. Note that this means that not only one type variable is used, but 71 several꩜note{In principle, each potentially-present field would need a 72 distinct type variable, but whole potentially-present branches may be 73 collapsed to a single type variable if no access is made to the variables 74 within.}. 75 76 77 ꩜section{Generating the tree type with polymorphic holes} 78 79 We define in this section facilities to automatically generate this list of 80 polymorphic type variables. In order to avoid having a huge number of type 81 variables, a branch containing only optional fields can be collapsed into a 82 single type variable. An exception to this rule is when a field needs to be 83 added or modified by the user code: in this case the polymorphic type variable 84 for that field must be preserved, and the branch may not entirely be 85 collapsed. 86 87 We take as an example the case where that there are 8 fields (꩜racketid[f1], 88 ꩜racketid[f2], ꩜racketid[a], ꩜racketid[b], ꩜racketid[f5], ꩜racketid[f6], 89 ꩜racketid[f7] and ꩜racketid[u]) used in the whole program. Records are 90 therefore represented as a tree of depth 4 (including the root node) with 8 91 leaves. A record with the fields ꩜racketid[a] and ꩜racketid[b] will be 92 represented as a tree where the branch containing ꩜racketid[f1] and 93 ꩜racketid[f2] is collapsed. Furthermore, the right branch of the root, 94 containing ꩜racketid[f5], ꩜racketid[f6], ꩜racketid[f7] and ꩜racketid[u] will 95 also be collapsed. 96 97 ꩜define-runtime-path[scribblings/collapse.png 98 "scribblings/collapsed.png"] 99 ꩜figure["fig:flex-with-tree:collapsed" 100 ꩜elem{The tree representing the type for a record with fields 101 ꩜racketid[a] and ꩜racketid[b] is ꩜racket[((C¹ . (a . b)) . C²)], where 102 ꩜racket[Cⁱ] indicates that a single polymorphic type is used to 103 represent the type of the whole collapsed branch.} 104 ꩜image[scribblings/collapse.png]{}] 105 106 ꩜define-runtime-path[scribblings/collapsed-updated.png 107 "scribblings/collapsed-updated.png"] 108 ꩜figure["fig:flex-with-tree:collapsed-updated" 109 ꩜elem{Updating the node ꩜racketid[u], which appears somewhere in the 110 collapsed branch ꩜racketid[C²] is not possible, because the type 111 abstracted away by ꩜racketid[C²] may be different before and after the 112 update.} 113 ꩜image[scribblings/collapsed-updated.png]{}] 114 115 ꩜define-runtime-path[scribblings/collapsed-breakdown.png 116 "scribblings/collapsed-breakdown.png"] 117 ꩜figure["fig:flex-with-tree:collapsed-updated" 118 ꩜elem{We therefore break apart the collapsed branch ꩜racketid[C²]. The 119 tree representing the type for a record with fields ꩜racketid[a] and 120 ꩜racketid[b], and where the field ꩜racketid[u] may be updated or added, 121 is ꩜racket[((C¹ . (a . b)) . (|C²′| . (C³ . u)))]. Note that 122 ꩜racketid[u] may refer to a possibly absent field (in which case the 123 polymorphic type variable will be instantiated with ꩜racket[None].} 124 ꩜image[scribblings/collapsed-breakdown.png]{}] 125 126 ꩜section{From a selection of field indieces to a tree shape} 127 128 ꩜defproc[#:kind "phase 1 procedure" 129 (idx→tree [none-wrapper (->d [depth exact-nonnegative-integer?] 130 any/c)] 131 [leaf-wrapper (->d [i-in-vec exact-nonnegative-integer?] 132 [leaf-idx exact-nonnegative-integer?] 133 any/c)] 134 [node-wrapper (->d [left any/c] 135 [right any/c] 136 any/c)] 137 [vec (vectorof exact-nonnegative-integer?)]) 138 r]{ 139 Given a flat list of field indicies (that is, leaf positions in the tree 140 representation), ꩜racket[idx→tree] generates tree-shaped code, transforming 141 each leaf with ꩜racket[_leaf-wrapper], each intermediate node with 142 ꩜racket[_node-wrapper] and each leaf not present in the initial list with 143 ꩜racket[none-wrapper].} 144 145 ꩜chunk[<idx→tree> 146 (define/contract (idx→tree #:none-wrapper none-wrapper 147 #:leaf-wrapper leaf-wrapper 148 #:node-wrapper node-wrapper 149 #:vec vec) 150 <idx→tree/ctc> 151 (define (r #:depth depth 152 #:vec-bounds vec-start vec-after-end 153 #:leaf-bounds first-leaf after-last-leaf) 154 (cond 155 |<idx→tree cases>|)) 156 r)] 157 158 ꩜spler[<idx→tree/ctc> 159 (code:comment "; contract for idx→tree, as specified above") 160 #:expanded 161 (code:comment "; contract for idx→tree, as specified above") 162 (-> #:none-wrapper (->d ([depth exact-nonnegative-integer?]) 163 [result any/c]) 164 #:leaf-wrapper (->d ([i-in-vec exact-nonnegative-integer?] 165 [leaf-idx exact-nonnegative-integer?]) 166 any) 167 #:node-wrapper (->d ([left any/c] 168 [right any/c]) 169 any) 170 #:vec (vectorof exact-nonnegative-integer?) 171 (-> #:depth exact-nonnegative-integer? 172 #:vec-bounds exact-nonnegative-integer? 173 #;| | exact-nonnegative-integer? 174 #:leaf-bounds exact-nonnegative-integer? 175 #;| | exact-nonnegative-integer? 176 any/c))] 177 178 The ꩜racket[idx→tree] is a two-step curried function, and the first step 179 returns a function with the following signature: 180 181 ꩜defproc[(r [#:depth depth exact-nonnegative-integer?] 182 [#:vec-bounds vec-start exact-nonnegative-integer?] 183 #;| | [vec-after-end exact-nonnegative-integer?] 184 [#:leaf-bounds first-leaf exact-nonnegative-integer?] 185 #;| | [after-last-leaf exact-nonnegative-integer?]) 186 any/c]{} 187 188 The ꩜racket[idx→tree] function works by performing repeated dichotomy on the 189 vector of present fields ꩜racket[vec]. 190 191 ꩜hlite[|<idx→tree cases>| {-/ (cond = _ _ _)} 192 (cond 193 [(= vec-start vec-after-end) 194 (none-wrapper depth)] 195 [(= (+ first-leaf 1) after-last-leaf) 196 (leaf-wrapper vec-start (vector-ref vec vec-start))] 197 [else 198 (let* ([leftmost-right-leaf (/ (+ first-leaf after-last-leaf) 2)] 199 [vec-left-branch-start vec-start] 200 [vec-left-branch-after-end 201 (find-≥ leftmost-right-leaf vec vec-start vec-after-end)] 202 [vec-right-branch-start vec-left-branch-after-end] 203 [vec-right-branch-after-end vec-after-end]) 204 (node-wrapper 205 (r #:depth (sub1 depth) 206 #:vec-bounds vec-left-branch-start 207 #;| | vec-left-branch-after-end 208 #:leaf-bounds first-leaf 209 #;| | leftmost-right-leaf) 210 (r #:depth (sub1 depth) 211 #:vec-bounds vec-right-branch-start 212 #;| | vec-right-branch-after-end 213 #:leaf-bounds leftmost-right-leaf 214 #;| | after-last-leaf)))])] 215 216 The ꩜racket[find-≥] function performs the actual dichotomy, and finds the 217 first index within the given bounds for which ꩜racket[(vector-ref vec result)] 218 is greater than or equal to ꩜racket[val] (if there is none, then the upper 219 exclusive bound is returned). 220 221 ꩜chunk[<dichotomy> 222 (define/contract (find-≥ val vec start end) 223 (->i ([val exact-nonnegative-integer?] 224 [vec vector?] ;; (sorted-vectorof exact-nonnegative-integer? <) 225 [start (vec) (integer-in 0 (sub1 (vector-length vec)))] 226 [end (vec start) (integer-in (add1 start) (vector-length vec))]) 227 #:pre (val vec start) (or (= start 0) 228 (< (vector-ref vec (sub1 start)) val)) 229 #:pre (val vec end) (or (= end (vector-length vec)) 230 (> (vector-ref vec end) val)) 231 [result (start end) (integer-in start end)]) 232 (if (= (- end start) 1) ;; there is only one element 233 (if (>= (vector-ref vec start) val) 234 start 235 end) 236 (let () 237 (define mid (ceiling (/ (+ start end) 2))) 238 (if (>= (vector-ref vec mid) val) 239 (find-≥ val vec start mid) 240 (find-≥ val vec mid end)))))] 241 242 ꩜section{Empty branches (branches only containing missing fields)} 243 244 For efficiency and to reduce memory overhead, we pre-define values for 245 branches of depth ꩜racket[_d ∈ (range 0 _n)] which only contain missing 246 fields. 247 248 ꩜chunk[<empty-branches> 249 ;; TODO: clean this up (use subtemplate). 250 (define-syntax defempty 251 (syntax-parser 252 [(_ n:nat) 253 #:with (empty1 emptyA …) 254 (map (λ (depth) 255 (string->symbol (format "empty~a" (expt 2 depth)))) 256 (range (add1 (syntax-e #'n)))) 257 #:with (emptyB … _) #'(empty1 emptyA …) 258 #:with (empty1/τ emptyA/τ …) (stx-map λ.(format-id % "~a/τ" %) 259 #'(empty1 emptyA …)) 260 #:with (emptyB/τ … _) #'(empty1/τ emptyA/τ …) 261 (syntax-local-introduce 262 #'(begin (define-type empty1/τ 'none) 263 (define-type emptyA/τ (Pairof emptyB/τ emptyB/τ)) 264 … 265 (define empty1 : empty1/τ 'none) 266 (define emptyA : emptyA/τ (cons emptyB emptyB)) 267 … 268 (provide empty1 emptyA … 269 empty1/τ emptyA/τ …)))])) 270 (defempty 10)] 271 272 ꩜section{Creating a record builder given a set of field indices} 273 274 ꩜chunk[<record-builder> 275 (define-syntax record-builder 276 (syntax-parser 277 ;; depth ≥ 0. 0 ⇒ a single node, 1 ⇒ 2 nodes, 2 ⇒ 4 nodes and so on. 278 [(_ depth:nat idx:nat …) 279 #:when (not (check-duplicates (syntax->datum #'(idx …)))) 280 (define vec (list->vector (sort (syntax->datum #'(idx …)) <))) 281 (define arg-vec (vector-map (λ (idx) 282 (format-id #;TODO:FIXME: (syntax-local-introduce #'here) 283 "arg~a" 284 idx)) 285 vec)) 286 (define/with-syntax #(arg …) arg-vec) 287 288 (define/with-syntax tree 289 ((idx→tree <record-builder/wrappers> 290 #:vec vec) 291 #:depth (syntax-e #'depth) 292 #:vec-bounds 0 (vector-length vec) 293 #:leaf-bounds 0 (expt 2 (syntax-e #'depth)))) 294 (define/with-syntax (arg/τ …) (stx-map (λ (arg) 295 (format-id arg "~a/τ" arg)) 296 #'(arg …))) 297 #'(λ #:∀ (arg/τ …) ([arg : arg/τ] …) 298 tree)]))] 299 300 ꩜hlite[<record-builder/wrappers> {-/ (_ = _ _ _ _ _ _ _ _ _ -/ _ vec)} 301 (idx→tree 302 #:none-wrapper λdepth.(format-id #'here "empty~a" (expt 2 depth)) 303 #:leaf-wrapper λi.idx.(vector-ref arg-vec i) 304 #:node-wrapper λl.r.(list #'cons l r) 305 #:vec vec)] 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 ꩜section{Row typing} 352 353 Row type variable identifiers are bound as transformers to instances of the 354 ꩜racket[ρ-wrapper] struct, so that they are easily recognisable by special 355 forms such as ꩜racket[record]. 356 357 ꩜spler[<ρ-wrapper> 358 (begin-for-syntax 359 (struct ρ-wrapper (id))) 360 #:expanded 361 (begin-for-syntax 362 (struct ρ-wrapper (id) 363 #:property prop:procedure 364 (λ (self stx) 365 (raise-syntax-error (syntax-e (ρ-wrapper-id self)) 366 "invalid use of row type variable" 367 stx))))] 368 369 The row type variable actually expands to several polymorphic type variables. 370 In order to know which fields are relevant, we remember which fields are used 371 along a given row type variable, while compiling the current file. The set of 372 field names used with a given row types variable is stored as an entry of the 373 ꩜racket[ρ-table]. 374 375 ꩜chunk[<ρ-table> 376 (define-for-syntax ρ-table (make-free-id-table))] 377 378 A record type which includes a row type variable is expanded to the type of a 379 binary tree. Fields which are used along that row type variable matter, and 380 must be explicitly indicated as optional leaves (so that operations which add 381 or remove fields later in the body of a row-polymorphic function may refer to 382 that leaf). Branches which only contain irrelevant leaves can be collapsed to 383 a single polymorphic type. The core implementation of record types (in which 384 the depth of the tree is explicitly given, and ) follows. Since the code is 385 very similar to the defintion of ꩜racket[idx→tree], the unchanged parts are 386 dimmed below. 387 388 ꩜; TODO: this is near identical to record-builder, refactor. 389 ꩜hlite[<record-type> 390 {(dte rt / (sp [sig when dup vec arg-vec arg 391 (d/ws tree (= idx→tree / a b c d e f g h)) = _ _ _]))} 392 (define-type-expander record-type 393 (syntax-parser 394 [(_ depth:nat idx:nat …) 395 #:when (not (check-duplicates (syntax->datum #'(idx …)))) 396 (define vec (list->vector (sort (syntax->datum #'(idx …)) <))) 397 (define arg-vec (vector-map (λ (idx) 398 (format-id #;TODO:FIXME: (syntax-local-introduce #'here) 399 "arg~a" 400 idx)) 401 vec)) 402 (define/with-syntax #(arg …) arg-vec) 403 404 (define/with-syntax tree 405 ((idx→tree <record-type/wrappers> 406 #:vec vec) 407 #:depth (syntax-e #'depth) 408 #:vec-bounds 0 (vector-length vec) 409 #:leaf-bounds 0 (expt 2 (syntax-e #'depth)))) 410 (define sidekicks-len 0) 411 (define sidekicks '()) 412 #`(∀ (arg … #,@sidekicks) tree)]))] 413 414 The results of ꩜racket[record-type] and ꩜racket[record-builder] differ in two 415 aspects: the result of ꩜racket[record-type] is a polymorphic type, not a 416 function, and the empty branches are handled differently. When a branch only 417 containing ꩜racket[none] elements is encountered, it is replaced with a single 418 polymorphic type. 419 420 ꩜hlite[<record-type/wrappers> {-/ (_ = _ _ _ _ _ _ _ _ _ -/ _ vec)} 421 (idx→tree 422 #:none-wrapper λdepth.(begin 423 (define sidekick (format-id #'here "row~a" sidekicks-len)) 424 (set! sidekicks-len (add1 sidekicks-len)) 425 (set! sidekicks (cons sidekick sidekicks)) 426 sidekick) 427 #:leaf-wrapper λi.idx.(vector-ref arg-vec i) 428 #:node-wrapper λl.r.(list #'Pairof l r) 429 #:vec vec)] 430 431 Since the list of fields may be amended long after the type was initially 432 expanded, we delay the expansion of the type. This is done by initially 433 expanding to a placeholder type name, and later patching the expanded code to 434 replace that placeholder with the actual expanded record type. 435 ꩜racket[current-patch-table] maps each placeholder to an anonymous function 436 which will produce the syntax for the desired type when called. 437 438 ꩜chunk[<current-patch-table> 439 (define-for-syntax current-patch-table (make-parameter #f))] 440 441 Type-level forms like ꩜racket[∀ρ], ꩜racket[ρ-inst] and ꩜racket[record] add 442 placeholders to ꩜racket[current-patch-table]. 443 444 The form ꩜racket[with-ρ] is used to declare row type variables and collect 445 patches in ꩜racket[current-patch-table]. The explicit declaration of row type 446 variables is necessary because type variables which are logically ``bound'' 447 with ꩜racket[∀] are not actually bound as identifiers during macro expansion 448 (instead, Typed Racket performs its own resolution while typechecking, i.e. 449 after the program is expanded). If a row type variable is introduced in the 450 type declaration for a function, we need to be able to detect the binding when 451 processing type-level forms within the body of the function. 452 453 ꩜chunk[<with-ρ> 454 (define-syntax with-ρ 455 (syntax-parser 456 [(_ (ρ …) . body) 457 #'(splicing-letrec-syntax ([ρ (ρ-wrapper #'ρ)] …) 458 (with-ρ-chain (ρ …) . body))]))] 459 460 Once the bindings have been introduced via ꩜racket[splicing-letrec-syntax], 461 the expansion continues within the context of these identifiers, via the 462 ꩜racket[with-ρ-chain] macro. 463 464 ꩜chunk[<with-ρ-chain> 465 (define-syntax with-ρ-chain 466 (syntax-parser 467 [(_ (ρ …) . body) 468 (parameterize ([current-patch-table (make-free-id-table)]) 469 (define expanded-form 470 (local-expand #'(begin . body) 'top-level '())) 471 (patch expanded-form (current-patch-table)))]))] 472 473 ꩜subsection{Type of a record, with a multiple fields} 474 475 The ꩜racket[∀ρ] type-level form translates to a ꩜racket[∀] form. The 476 ꩜racket[∀] form is expanded, so that uses of the row type variables within can 477 be detected. The ꩜racket[∀ρ] then expands to a placeholder 478 ꩜racket[delayed-type], which will be patched by the surrounding 479 ꩜racket[with-ρ]. 480 481 ꩜;TODO: use a table to track the pre-declared collapsed-branch types? 482 ꩜chunk[<∀ρ> 483 (define-type-expander ∀ρ 484 (syntax-parser 485 [(_ (A:id … #:ρ ρ:id …) τ) 486 (for ([ρ (in-syntax #'(ρ …))]) 487 (free-id-table-set! ρ-table ρ <make-lifo-set>)) 488 (define expanded (expand-type #'(∀ (A …) (Let ([ρ 'NOT-IMPL-YET] …) τ)))) 489 (define/syntax-parse ({~literal tr:∀} (A′ …) . τ′) expanded) 490 (free-id-table-set! (current-patch-table) 491 #'delayed-type 492 (λ (self) (delayed-∀ρ #'{(A′ …) (ρ …) τ′}))) 493 #'delayed-type]))] 494 495 When the ꩜racket[delayed-type] is replaced, the type variables associated with 496 each row type variable are injected as extra arguments to the 497 previously-expanded polymorphic type. 498 499 ꩜chunk[<delayed-∀ρ> 500 (define-for-syntax/case-args (delayed-∀ρ {(A′ …) (ρ …) τ′}) 501 (define/syntax-parse ((ρ′ …) …) 502 (for/list ([ρ (in-syntax #'(ρ …))]) 503 (for/list ([ρ′ (sort (<lifo-set→list> (free-id-table-ref ρ-table 504 ρ)) 505 symbol<?)]) 506 ;; TODO: the format-id shouldn't be here, it should be when 507 ;; the id is added to the list. Also #'here is probably the 508 ;; wrong srcloc 509 (format-id #'here "~a.~a" ρ ρ′)))) 510 #'(∀ (A′ … ρ′ … …) . τ′))] 511 512 513 514 ꩜chunk[<record-type> 515 <ρ-wrapper> 516 <current-patch-table> 517 518 <with-ρ-chain> 519 <with-ρ> 520 521 <ρ-table> 522 <∀ρ> 523 524 <delayed-∀ρ> 525 526 (define-type-expander record 527 (syntax-parser 528 [(_ f:id … . {~or (#:ρ ρ:id) ρ:id}) 529 (define set 530 (free-id-table-ref! ρ-table #'ρ (λ () <make-lifo-set>))) 531 (for ([f (in-syntax #'(f …))]) 532 (<lifo-set-add!> set (syntax->datum f))) 533 #'(List 'f … 'ρ)])) 534 535 (define-syntax ρ-inst 536 (syntax-parser 537 [(_ f A:id … #:ρ ρ:id …) 538 #'TODO]))] 539 540 ꩜chunk[<make-lifo-set> 541 ;; ordered free-identifier-set, last added = first in the order. 542 (cons (box '()) (mutable-set))] 543 544 ꩜chunk[<lifo-member?> 545 (λ (s v) (set-member? (cdr s) v))] 546 547 ꩜chunk[<lifo-set-add!> 548 (λ (s v) 549 (unless (<lifo-member?> s v) 550 (set-box! (car s) (cons v (unbox (car s))))) 551 (set-add! (cdr s) v))] 552 553 ꩜chunk[<lifo-set→list> 554 (λ (s) (unbox (car s)))] 555 556 ꩜chunk[<patch> 557 (define-for-syntax (patch e tbl) 558 (define (patch* e) 559 (cond 560 ;[(syntax-case e () 561 ; [(x y) 562 ; (free-id-table-ref tbl x (λ () #f)) 563 ; (values #t ((free-id-table-ref tbl x) e))] 564 ; [_ #f])] 565 [(and (identifier? e) 566 (free-id-table-ref tbl e (λ () #f))) 567 => (λ (f) (values #t (f e)))] 568 [(syntax? e) 569 (let-values ([(a b) (patch* (syntax-e e))]) 570 (if a 571 (values a (datum->syntax e b e e)) 572 (values a e)))] 573 [(pair? e) 574 (let-values ([(a1 b1) (patch* (car e))] 575 [(a2 b2) (patch* (cdr e))]) 576 (if (or a1 a2) 577 (values #t (cons b1 b2)) 578 (values #f e)))] 579 ;; TODO: hash, prefab etc. 580 [else 581 (values #f e)])) 582 (let-values ([(a b) (patch* e)]) 583 b))] 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 ꩜chunk[<expand-ρ> 608 (define-for-syntax identifier<? (∘ symbol<? syntax-e)) 609 (define-for-syntax (sort-ids ids) (sort (syntax->list ids) identifier<?)) 610 (define-type-expander ρ/fields 611 (syntax-parser 612 [(_ (important-field …) (all-field …)) 613 #:with (sorted-important-field …) (sort-ids #'(important-field …)) 614 #:with (sorted-all-field …) (sort-ids #'(all-field …)) 615 616 #'~]))] 617 618 ꩜; TODO: build the expansion of ρ by determining which are the dangling branches 619 ꩜; for a given set of fields. 620 ꩜; TODO: use the expansion of ρ in the generated ∀ 621 ꩜; TODO: write the "record" type (tree with the desired leaves + dangling branches 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 ꩜section{Type of a record, with a single hole} 646 647 In order to functionally update records, the updating functions will take a 648 tree where the type of a single leaf needs to be known. This of course means 649 that branches that spawn off on the path from the root have to be given a 650 polymorphic type, so that the result can have the same type for these branches 651 as the original value to update. 652 653 ꩜CHUNK[<tree-type-with-replacement> 654 (define-for-syntax (tree-type-with-replacement n last τ*) 655 (define-values (next mod) (quotient/remainder n 2)) 656 (cond [(null? τ*) last] 657 [(= mod 0) 658 (tree-type-with-replacement next 659 #`(Pairof #,last #,(car τ*)) 660 (cdr τ*))] 661 [else 662 (tree-type-with-replacement next 663 #`(Pairof #,(car τ*) #,last) 664 (cdr τ*))]))] 665 666 ꩜section{Functionally updating a tree-record} 667 668 ꩜subsection{Adding and modifying fields} 669 670 Since we only deal with functional updates of immutable records, modifying a 671 field does little more than discarding the old value, and injecting the new 672 value instead into the new, updated record. 673 674 Adding a new field is done using the same exact operation: missing fields are 675 denoted by a special value, ꩜racket['NONE], while present fields are 676 represented as instances of the polymorphic struct ꩜racket[(Some T)]. Adding a 677 new field is therefore as simple as discarding the old ꩜racket['NONE] marker, 678 and replacing it with the new value, wrapped with ꩜racket[Some]. A field 679 update would instead discard the old instance of ꩜racket[Some], and replace it 680 with a new one. 681 682 ꩜CHUNK[<make-replace-in-tree-body> 683 (if (= i 1) 684 #'(delay/pure/stateless replacement) 685 (let* ([bits (to-bits i)] 686 [next (from-bits (cons #t (cddr bits)))] 687 [mod (cadr bits)]) 688 (define/with-syntax next-id (vector-ref low-names (sub1 next))) 689 (if mod 690 #`(replace-right (inst next-id #,@τ*-limited+T-next) 691 tree-thunk 692 replacement) 693 #`(replace-left (inst next-id #,@τ*-limited+T-next) 694 tree-thunk 695 replacement))))] 696 697 ꩜CHUNK[<define-replace-in-tree> 698 (define-pure/stateless 699 (: replace-right (∀ (A B C R) (→ (→ (Promise B) R (Promise C)) 700 (Promise (Pairof A B)) 701 R 702 (Promise (Pairof A C))))) 703 (define 704 #:∀ (A B C R) 705 (replace-right [next-id : (→ (Promise B) R (Promise C))] 706 [tree-thunk : (Promise (Pairof A B))] 707 [replacement : R]) 708 (delay/pure/stateless 709 (let ([tree (force tree-thunk)]) 710 (let ([left-subtree (car tree)] 711 [right-subtree (cdr tree)]) 712 (cons left-subtree 713 (force (next-id (delay/pure/stateless right-subtree) 714 replacement)))))))) 715 (define-pure/stateless 716 (: replace-left (∀ (A B C R) (→ (→ (Promise A) R (Promise C)) 717 (Promise (Pairof A B)) 718 R 719 (Promise (Pairof C B))))) 720 (define 721 #:∀ (A B C R) 722 (replace-left [next-id : (→ (Promise A) R (Promise C))] 723 [tree-thunk : (Promise (Pairof A B))] 724 [replacement : R]) 725 (delay/pure/stateless 726 (let ([tree (force tree-thunk)]) 727 (let ([left-subtree (car tree)] 728 [right-subtree (cdr tree)]) 729 (cons (force (next-id (delay/pure/stateless left-subtree) 730 replacement)) 731 right-subtree)))))) 732 733 (define-for-syntax (define-replace-in-tree 734 low-names names rm-names τ* i depth) 735 (define/with-syntax name (vector-ref names (sub1 i))) 736 (define/with-syntax rm-name (vector-ref rm-names (sub1 i))) 737 (define/with-syntax low-name (vector-ref low-names (sub1 i))) 738 (define/with-syntax tree-type-with-replacement-name 739 (gensym 'tree-type-with-replacement)) 740 (define/with-syntax tree-replacement-type-name 741 (gensym 'tree-replacement-type)) 742 (define τ*-limited (take τ* depth)) 743 (define τ*-limited+T-next (if (= depth 0) 744 (list #'T) 745 (append (take τ* (sub1 depth)) 746 (list #'T)))) 747 #`(begin 748 (provide name rm-name) 749 (define-type (tree-type-with-replacement-name #,@τ*-limited T) 750 (Promise #,(tree-type-with-replacement i #'T τ*-limited))) 751 752 (define-pure/stateless 753 (: low-name 754 (∀ (#,@τ*-limited T) 755 (→ (tree-type-with-replacement-name #,@τ*-limited Any) 756 T 757 (tree-type-with-replacement-name #,@τ*-limited T)))) 758 (define 759 #:∀ (#,@τ*-limited T) 760 (low-name [tree-thunk : (tree-type-with-replacement-name 761 #,@τ*-limited Any)] 762 [replacement : T]) 763 : (Promise #,(tree-type-with-replacement i #'T τ*-limited)) 764 #,<make-replace-in-tree-body>)) 765 766 (: name 767 (∀ (#,@τ*-limited T) 768 (→ (tree-type-with-replacement-name #,@τ*-limited Any) 769 T 770 (tree-type-with-replacement-name #,@τ*-limited 771 (Some T))))) 772 (define (name tree-thunk replacement) 773 (low-name tree-thunk (Some replacement))) 774 775 (: rm-name 776 (∀ (#,@τ*-limited) 777 (→ (tree-type-with-replacement-name #,@τ*-limited (Some Any)) 778 (tree-type-with-replacement-name #,@τ*-limited 'NONE)))) 779 (define (rm-name tree-thunk) 780 (low-name tree-thunk 'NONE))))] 781 782 ꩜section{Auxiliary values} 783 784 The following sections reuse a few values which are derived from the list of 785 fields: 786 787 ꩜CHUNK[<utils> 788 (define all-fields #'(field …)) 789 (define depth-above (ceiling-log2 (length (syntax->list #'(field …))))) 790 (define offset (expt 2 depth-above)) 791 (define i*-above (range 1 (expt 2 depth-above))) 792 (define names (list->vector 793 (append (map (λ (i) (format-id #'here "-with-~a" i)) 794 i*-above) 795 (stx-map (λ (f) (format-id f "with-~a" f)) 796 #'(field …))))) 797 (define rm-names (list->vector 798 (append (map (λ (i) (format-id #'here "-without-~a" i)) 799 i*-above) 800 (stx-map (λ (f) (format-id f "without-~a" f)) 801 #'(field …))))) 802 (define low-names (list->vector 803 (append (map (λ (i) (format-id #'here "-u-with-~a" i)) 804 i*-above) 805 (stx-map (λ (f) (format-id f "u-with-~a" f)) 806 #'(field …)))))] 807 808 ꩜section{Type of a tree-record} 809 810 ꩜CHUNK[<τ-tree-with-fields> 811 (define-for-syntax (τ-tree-with-fields struct-fields fields) 812 (define/with-syntax (struct-field …) struct-fields) 813 (define/with-syntax (field …) fields) 814 <utils> 815 ;; Like in convert-from-struct 816 (define lookup 817 (make-free-id-table 818 (for/list ([n (in-syntax all-fields)] 819 [i (in-naturals)]) 820 (cons n (+ i offset))))) 821 (define fields+indices 822 (sort (stx-map λ.(cons % (free-id-table-ref lookup %)) 823 #'(struct-field …)) 824 < 825 #:key cdr)) 826 827 (define up (* offset 2)) 828 829 ;; Like in convert-fields, but with Pairof 830 (define (f i) 831 (if (and (pair? fields+indices) (= i (cdar fields+indices))) 832 (begin0 833 `(Some ,(caar fields+indices)) 834 (set! fields+indices (cdr fields+indices))) 835 (if (>= (* i 2) up) ;; DEPTH 836 ''NONE 837 (begin 838 `(Pairof ,(f (* i 2)) 839 ,(f (add1 (* i 2)))))))) 840 (f 1))] 841 842 ꩜section{Conversion to and from record-trees} 843 844 ꩜CHUNK[<define-struct↔tree> 845 (define-for-syntax (define-struct↔tree 846 offset all-fields τ* struct-name fields) 847 (define/with-syntax (field …) fields) 848 (define/with-syntax fields→tree-name 849 (format-id struct-name "~a→tree" struct-name)) 850 (define/with-syntax tree→fields-name 851 (format-id struct-name "tree→~a" struct-name)) 852 (define lookup 853 (make-free-id-table 854 (for/list ([n (in-syntax all-fields)] 855 [i (in-naturals)]) 856 (cons n (+ i offset))))) 857 (define fields+indices 858 (sort (stx-map λ.(cons % (free-id-table-ref lookup %)) 859 fields) 860 < 861 #:key cdr)) 862 #`(begin 863 (: fields→tree-name (∀ (field …) 864 (→ field … 865 (Promise 866 #,(τ-tree-with-fields #'(field …) 867 all-fields))))) 868 (define (fields→tree-name field …) 869 (delay/pure/stateless 870 #,(convert-fields (* offset 2) fields+indices))) 871 872 (: tree→fields-name (∀ (field …) 873 (→ (Promise 874 #,(τ-tree-with-fields #'(field …) 875 all-fields)) 876 (Values field …)))) 877 (define (tree→fields-name tree-thunk) 878 (define tree (force tree-thunk)) 879 #,(convert-back-fields (* offset 2) fields+indices))))] 880 881 ꩜subsection{Creating a new tree-record} 882 883 ꩜CHUNK[<convert-fields> 884 (define-for-syntax (convert-fields up fields+indices) 885 (define (f i) 886 (if (and (pair? fields+indices) (= i (cdar fields+indices))) 887 (begin0 888 `(Some ,(caar fields+indices)) 889 (set! fields+indices (cdr fields+indices))) 890 (if (>= (* i 2) up) ;; DEPTH 891 ''NONE 892 `(cons ,(f (* i 2)) 893 ,(f (add1 (* i 2))))))) 894 (f 1))] 895 896 897 ꩜subsection{Extracting all the fields from a tree-record} 898 899 We traverse the tree in preorder, and accumulate definitions naming the 900 interesting subparts of the trees (those where there are fields). 901 902 ꩜CHUNK[<convert-back-fields> 903 (define-for-syntax (convert-back-fields up fields+indices) 904 (define result '()) 905 (define definitions '()) 906 (define (f i t) 907 (if (and (pair? fields+indices) (= i (cdar fields+indices))) 908 (begin0 909 (begin 910 (set! result (cons #`(Some-v #,t) result)) 911 #t) 912 (set! fields+indices (cdr fields+indices))) 913 (if (>= (* i 2) up) ;; DEPTH 914 #f 915 (let* ([left-t (string->symbol 916 (format "subtree-~a" (* i 2)))] 917 [right-t (string->symbol 918 (format "subtree-~a" (add1 (* i 2))))] 919 [left (f (* i 2) left-t)] 920 [right (f (add1 (* i 2)) right-t)]) 921 (cond 922 [(and left right) 923 (set! definitions (cons #`(define #,left-t (car #,t)) 924 definitions)) 925 (set! definitions (cons #`(define #,right-t (cdr #,t)) 926 definitions)) 927 #t] 928 [left 929 (set! definitions (cons #`(define #,left-t (car #,t)) 930 definitions)) 931 #t] 932 [right 933 (set! definitions (cons #`(define #,right-t (cdr #,t)) 934 definitions)) 935 #t] 936 [else 937 #f]))))) 938 (f 1 #'tree) 939 #`(begin #,@definitions (values . #,(reverse result))))] 940 941 ꩜section{Defining the converters and accessors for each known record type} 942 943 ꩜CHUNK[<define-trees> 944 (define-for-syntax (define-trees stx) 945 (syntax-case stx () 946 [(bt-fields-id (field …) [struct struct-field …] …) 947 (let () 948 <utils> 949 (define ∀-types (map λ.(format-id #'here "τ~a" %) 950 (range (add1 depth-above)))) 951 (define total-nb-functions (vector-length names)) 952 <define-trees-result>)]))] 953 954 ꩜CHUNK[<bt-fields-type> 955 (define-for-syntax (bt-fields-type fields) 956 (λ (stx) 957 (syntax-case stx () 958 [(_ . fs) 959 #`(∀ fs (Promise #,(τ-tree-with-fields #'fs 960 fields)))])))] 961 962 ꩜CHUNK[<define-trees-result> 963 #`(begin 964 (define-type-expander bt-fields-id 965 (bt-fields-type #'#,(syntax-local-introduce #'(field …)))) 966 #,@(map λ.(define-replace-in-tree low-names 967 names rm-names ∀-types % (floor-log2 %)) 968 (range 1 (add1 total-nb-functions))) 969 #;#,@(map λ.(define-remove-in-tree rm-names ∀-types % (floor-log2 %)) 970 (range 1 (add1 total-nb-functions))) 971 #,@(map λ.(define-struct↔tree 972 offset all-fields ∀-types %1 %2) 973 (syntax->list #'(struct …)) 974 (syntax->list #'([struct-field …] …))))] 975 976 ꩜subsection{Putting it all together} 977 978 ꩜chunk[<maybe> 979 (struct (T) Some ([v : T]) #:transparent) 980 (define-type (Maybe T) (U (Some T) 'NONE))] 981 982 ꩜chunk[<*> 983 (require delay-pure 984 "flexible-with-utils.hl.rkt" 985 phc-toolkit/syntax-parse 986 (for-syntax (rename-in racket/base [... …]) 987 syntax/parse 988 syntax/stx 989 racket/syntax 990 racket/list 991 syntax/id-table 992 racket/set 993 racket/sequence 994 racket/vector 995 racket/contract 996 type-expander/expander 997 phc-toolkit/untyped/syntax-parse) 998 (for-meta 2 racket/base) 999 (prefix-in tr: (only-in typed/racket ∀)) 1000 racket/splicing) 1001 1002 (provide (for-syntax define-trees) 1003 ;; For tests: 1004 (struct-out Some) 1005 1006 ;;DEBUG: 1007 (for-syntax τ-tree-with-fields) 1008 record-builder 1009 ∀ρ 1010 with-ρ 1011 record) 1012 1013 <maybe> 1014 <tree-type-with-replacement> 1015 <define-replace-in-tree> 1016 ;<define-remove-in-tree> 1017 <convert-fields> 1018 <convert-back-fields> 1019 <τ-tree-with-fields> 1020 <define-struct↔tree> 1021 <define-trees> 1022 <bt-fields-type> 1023 (begin-for-syntax 1024 <dichotomy> 1025 <idx→tree>) 1026 <empty-branches> 1027 <record-builder> 1028 <patch> 1029 <record-type>] 1030 1031 ꩜include-section[(submod "flexible-with-utils.hl.rkt" doc)]