test-tiny.hl.rkt (20160B)
1 #lang hyper-literate #:꩜ envlang/tiny 2 3 ꩜title[#:tag "test-tiny"]{Tests and examples for ꩜racketmodname[envlang/tiny]} 4 5 ꩜section{Identity} 6 7 ꩜chunk[<id-λ> 8 (λ (x) x)] 9 ꩜chunk[<id> 10 (⧵ env env args args)] 11 ꩜chunk[<id-result> 12 (⧵ #f env args args)] 13 14 ꩜section{Dummy value} 15 16 ꩜chunk[<dummy-λ> 17 <id-λ>] 18 19 ꩜chunk[<dummy> 20 <id>] 21 22 ꩜section{Example: identity applied to identity} 23 24 ꩜chunk[<id-id-λ> 25 (<id-λ> <id-λ>)] 26 ꩜chunk[<id-id> 27 (@ <id> env <id>)] 28 ꩜chunk[<id-id-result> 29 <id-result>] 30 31 ꩜section{False} 32 33 a.k.a second-of-two 34 35 ꩜chunk[<false-λ> 36 (λ (if-true) (λ (if-false) if-false))] 37 ꩜chunk[<false> 38 (⧵ env env args (⧵ args env args args))] 39 ꩜chunk[<false-result> 40 (⧵ #f env args (⧵ args env args args))] 41 42 ꩜section{True} 43 44 a.k.a first-of-two 45 46 ꩜chunk[<true-λ> 47 (λ (if-true) (λ (if-false) if-true))] 48 ꩜chunk[<true> 49 (⧵ env env args (⧵ args env args captured))] 50 ꩜chunk[<true-result> 51 (⧵ #f env args (⧵ args env args captured))] 52 53 ꩜subsection{Boolean usage example: if true} 54 55 ꩜chunk[<if-true-example-λ> 56 ((<true-λ> <true-λ>) <false-λ>)] 57 ꩜chunk[<if-true-example> 58 (@ (@ <true> env <true>) env <false>)] 59 ꩜chunk[<if-false-example-result> 60 <true-result>] 61 62 ꩜subsection{Boolean usage example: if false} 63 64 ꩜chunk[<if-false-example-λ> 65 ((<false-λ> <true-λ>) <false-λ>)] 66 ꩜chunk[<if-false-example> 67 (@ (@ <false> env <true>) env <false>)] 68 ꩜chunk[<if-false-example-result> 69 <false-result>] 70 71 ꩜; TODO: take my own red pill / blue pill picture 72 ꩜; ꩜image{/tmp/Two-Buttons.jpg} 73 74 ꩜section{Pairs} 75 76 ꩜chunk[<pair-λ> 77 (λ (a) (λ (b) (λ (f) ((f a) b))))] 78 ꩜chunk[<pair-failed-attempt-1> 79 ; ↑ a a ↓ ↑ b a ↓ f ↑ f ↓ a ↓ 80 (⧵ env env args (⧵ args env args (⧵ captured env args (@ (@ args env captured) env BBBBBBBB))))] 81 ꩜chunk[<pair-failed-attempt-2> 82 ; ↑ a a ↓ ↑ b b ↓ f ↑ f ↓ b ↓ 83 (⧵ env env args (⧵ args env args (⧵ args env args (@ (@ args env AAAAAAAA) env captured))))] 84 85 Can't be done because our capture can only close over a single value. We use a primitive: 86 87 ꩜chunk[<pair> 88 ×] 89 90 ꩜chunk[<pair-result> 91 ×] 92 93 ꩜chunk[<pair-example> 94 (@ × <true> <false>)] 95 96 ꩜chunk[<pair-example-result> 97 (⧵ #f env args (@ (@ args env <true-result>) env <false-result>))] 98 99 ꩜subsection{Fst} 100 101 ꩜chunk[<fst-λ> 102 (λ (p) (p <true-λ>))] 103 104 ꩜chunk[<fst> 105 (⧵ captured env args (@ args env <true>))] 106 107 ꩜subsection{Snd} 108 109 ꩜chunk[<snd-λ> 110 (λ (p) (p <false-λ>))] 111 112 ꩜chunk[<snd> 113 (⧵ captured env args (@ args env <false>))] 114 115 ꩜section{Either} 116 117 ꩜subsection{Left} 118 119 ꩜chunk[<left-λ> 120 (λ (v) (λ (if-left) (λ (if-right) (if-left v))))] 121 ꩜chunk[<left> 122 ; ↑ v v ↓ ↑ if-left ↓ if-left ↓ v ↑ if-right ↓ if-left × v 123 (⧵ env env args (⧵ args env args (⧵ (@ <pair> args captured) env args (@ captured env <appfv>))))] 124 ꩜chunk[<appfv> 125 ; ↑ f f ↓ ↑ v ↓ f ↓ v 126 (⧵ env env args (⧵ args env args (@ captured env args)))] 127 ꩜chunk[<left-result> 128 (⧵ #f env args (⧵ args env args (⧵ (@ × args captured) env args (@ captured env (⧵ env env args (⧵ args env args (@ captured env args)))))))] 129 130 ꩜subsection{Right} 131 132 ꩜chunk[<right-λ> 133 (λ (v) (λ (if-left) (λ (if-right) (if-right v))))] 134 ꩜chunk[<right> 135 ; ↑ v ↓v↑ if-left ↓ v ↑ ↑ if-right ↓ if-right ↓ v 136 (⧵ env env args (⧵ args env args (⧵ captured env args (@ args env captured))))] 137 ꩜chunk[<right-result> 138 (⧵ #f env args (⧵ args env args (⧵ captured env args (@ args env captured))))] 139 140 ꩜section{If} 141 142 ꩜chunk[<if-λ-long> 143 (λ (c) (λ (if-true) (λ (if-false) ((c if-true) if-false))))] 144 145 When passed a boolean as the first argument (as should be the case), it is equivalent to: 146 147 ꩜chunk[<if-λ> 148 (λ (c) c)] 149 150 ꩜chunk[<if> 151 <id>] 152 153 ꩜chunk[<if-result> 154 <id-result>] 155 156 ꩜subsection{Match "either"} 157 158 ꩜chunk[<match-either-λ-long> 159 (λ (either) (λ (if-left) (λ (if-right) ((either if-true) if-false))))] 160 161 When passed a constructor of the "either" variant as the first argument (as should be the case), it is equivalent to: 162 163 ꩜chunk[<match-either-λ> 164 <id-λ>] 165 166 ꩜chunk[<match-either> 167 <id>] 168 169 ꩜chunk[<match-either-result> 170 <id-result>] 171 172 ꩜chunk[<match-left-example-λ> 173 (((<match-either-λ> (<left-λ> <id-λ>)) <id-λ>) (λ (v) <false-λ>))] 174 ꩜chunk[<match-left-example> 175 (@ (@ (@ <match-either> env (@ <left> env <id>)) env <id>) env (⧵ captured env args <false>))] 176 ꩜chunk[<match-left-example-result> 177 <id-result>] 178 179 ꩜chunk[<match-right-example-λ> 180 (((<match-either-λ (<right-λ> <id-λ>)) (λ (v) <false-λ>)) <id-λ>)] 181 ꩜chunk[<match-right-example> 182 (@ (@ (@ <match-either> env (@ <right> env <id>)) env (⧵ captured env args <false>)) env <id>)] 183 ꩜chunk[<match-right-example-result> 184 <id-result>] 185 186 ꩜section{Null} 187 188 ꩜chunk[<null-λ> 189 (<left-λ> <dummy-λ>)] 190 ꩜chunk[<null> 191 (@ <left> env <dummy>)] 192 ꩜chunk[<null-result> 193 (⧵ (⧵ #f env args args) env args (⧵ (@ × args captured) env args (@ captured env (⧵ env env args (⧵ args env args (@ captured env args))))))] 194 195 ꩜section{Cons} 196 197 ꩜chunk[<cons-λ> 198 (λ (a) (λ (b) (<right-λ> (<pair-λ> a b))))] 199 ꩜chunk[<cons> 200 (⧵ captured env args (⧵ args env args (@ <right> env (@ <pair> captured args))))] 201 ꩜chunk[<cons-result> 202 (⧵ #f env args (⧵ args env args (@ (⧵ env env args (⧵ args env args (⧵ captured env args (@ args env captured)))) env (@ × captured args))))] 203 204 ꩜subsection{Match "list"} 205 206 ꩜chunk[<match-null-cons-λ> 207 <match-either-λ>] 208 209 ꩜chunk[<match-null-cons> 210 <match-either>] 211 212 ꩜section{null?} 213 214 ꩜chunk[<null?-λ> 215 (λ (l) (((<match-null-cons-λ> l) (λ (v) <true>)) (λ (v) <false-λ>)))] 216 217 ꩜chunk[<null?> 218 (⧵ captured env args (@ (@ (@ <match-null-cons> env args) env (⧵ captured env args <true>)) env (⧵ captured env args <false>)))] 219 220 ꩜section{Car} 221 222 Since we don't have an error reporting mechanism, we make (car null) = null and (cdr null) = null 223 224 ꩜chunk[<car-λ> 225 (λ (l) (((<match-null-cons-λ> l) <null-λ>) <fst-λ>))] 226 227 ꩜chunk[<car> 228 (⧵ captured env args (@ (@ (@ <match-null-cons> env args) env (⧵ captured env args <null>)) env <fst>))] 229 230 ꩜chunk[<car-example> 231 (@ <car> env (@ (@ <cons> env <true>) env <null>))] 232 233 ꩜chunk[<car-example-result> 234 <true-result>] 235 236 ꩜chunk[<car-example2> 237 (@ <car> env (@ (@ <cons> env <false>) env <null>))] 238 239 ꩜chunk[<car-example2-result> 240 <false-result>] 241 242 ꩜chunk[<car-example3> 243 (@ <car> env <null>)] 244 245 ꩜chunk[<car-example3-result> 246 <null-result>] 247 248 ꩜section{Cdr} 249 250 Since we don't have an error reporting mechanism, we make (car null) = null and (cdr null) = null 251 252 ꩜chunk[<cdr-λ> 253 (λ (l) (((<match-null-cons-λ> l) <null-λ>) <snd-λ>))] 254 255 ꩜chunk[<cdr> 256 (⧵ captured env args (@ (@ (@ <match-null-cons> env args) env (⧵ captured env args <null>)) env <snd>))] 257 258 ꩜chunk[<cdr-example> 259 (@ <cdr> env (@ (@ <cons> env <true>) env <null>))] 260 261 ꩜chunk[<cdr-example-result> 262 <true-result>] 263 264 ꩜chunk[<cdr-example2> 265 (@ <cdr> env (@ (@ <cons> env <true>) env (@ (@ <cons> env <false>) env <null>)))] 266 267 ꩜chunk[<cdr-example2-result> 268 <cdr-example2-list-false-result>] 269 270 ꩜chunk[<cdr-example2-list-false> 271 (@ (@ <cons> env <false>) env <null>)] 272 273 ꩜chunk[<cdr-example2-list-false-result> 274 (⧵ (⧵ #f env args (@ (@ args env <false-result>) env <null-result>)) 275 env 276 args 277 (⧵ captured env args (@ args env captured)))] 278 279 ꩜chunk[<cdr-example3> 280 (@ <car> env (@ <cdr> env (@ (@ <cons> env <true>) env (@ (@ <cons> env <false>) env <null>))))] 281 282 ꩜chunk[<car-example3-result> 283 <false-result>] 284 285 ꩜section{Zero} 286 287 ꩜chunk[<zero-λ> 288 <null-λ>] 289 290 ꩜chunk[<zero> 291 <null>] 292 293 ꩜section{Not} 294 295 ꩜chunk[<not-λ> 296 (λ (a) (((<if-λ> a) <false>) <true>))] 297 298 ꩜chunk[<not> 299 (⧵ captured env args (@ (@ (@ <if> env args) env <false>) env <true>))] 300 301 ꩜section{And} 302 303 ꩜chunk[<and-λ> 304 (λ (a) (λ (b) (((<if-λ> a) b) <false-λ>)))] 305 306 ꩜chunk[<and> 307 ; a a b a b 308 (⧵ captured env args (⧵ args env args (@ (@ (@ <if> env captured) env args) env <false>)))] 309 310 ꩜chunk[<and-example-ff> 311 (@ (@ <and> env <false>) env <false>)] 312 313 ꩜chunk[<and-example-ft> 314 (@ (@ <and> env <false>) env <true>)] 315 316 ꩜chunk[<and-example-tf> 317 (@ (@ <and> env <true>) env <false>)] 318 319 ꩜chunk[<and-example-tt> 320 (@ (@ <and> env <true>) env <true>)] 321 322 ꩜section{Or} 323 324 ꩜chunk[<or-λ> 325 (λ (a) (λ (b) (((<if-λ> a) <true>) b)))] 326 327 ꩜chunk[<or> 328 ; a a b a b 329 (⧵ captured env args (⧵ args env args (@ (@ (@ <if> env captured) env <true>) env args)))] 330 331 ꩜chunk[<or-example-ff> 332 (@ (@ <or> env <false>) env <false>)] 333 334 ꩜chunk[<or-example-ft> 335 (@ (@ <or> env <false>) env <true>)] 336 337 ꩜chunk[<or-example-tf> 338 (@ (@ <or> env <true>) env <false>)] 339 340 ꩜chunk[<or-example-tt> 341 (@ (@ <or> env <true>) env <true>)] 342 343 ꩜section{Equal bools} 344 345 ꩜chunk[<eqbool-λ> 346 (λ (a) (λ (b) (((<if-λ> a) b) (<not-λ> b))))] 347 348 ꩜chunk[<eqbool> 349 (⧵ captured env args (⧵ args env args (@ (@ (@ <if> env captured) env args) env (@ <not> env args))))] 350 351 ꩜chunk[<eqbool-example-ff> 352 (@ (@ <eqbool> env <false>) env <false>)] 353 354 ꩜chunk[<eqbool-example-ft> 355 (@ (@ <eqbool> env <false>) env <true>)] 356 357 ꩜chunk[<eqbool-example-tf> 358 (@ (@ <eqbool> env <true>) env <false>)] 359 360 ꩜chunk[<eqbool-example-tt> 361 (@ (@ <eqbool> env <true>) env <true>)] 362 363 ꩜section{Z combinator} 364 365 ꩜chunk[<Z-λ> 366 (λ (f) (<half-Z-λ> <half-Z-λ>))] 367 368 ꩜chunk[<half-Z-λ> 369 (λ (x) (f (λ (v) ((x x) v))))] 370 371 ꩜chunk[<Z> 372 ; ↑ f 373 (⧵ captured env args (@ <half-Z> env <half-Z>))] 374 375 ꩜chunk[<half-Z> 376 ; ↓f↑ ↑ x ↓ f ↓x↑ ↑v ↓ x ↓ x ↓ v 377 (⧵ args env args (@ captured env (⧵ args env args (@ (@ captured env captured) env args))))] 378 379 ꩜section{Equality of lists} 380 381 ꩜chunk[<eqlist-λ> 382 (λ (recur) 383 (λ (cmp) 384 (λ (a) 385 (λ (b) 386 ((<if-λ> ((<or-λ> (<null?-λ> a)) (<null?-λ> b)) 387 (λ (_) ((<and-λ> (<null?-λ> a)) (<null?-λ> b))) 388 (λ (_) ((<if-λ> ((cmp (<car-λ> a)) (<car-λ> b)) 389 (λ (_) (((recur cmp) (<cdr-λ> a)) (<cdr-λ> b))) 390 (λ (_) <false-λ>)) 391 <dummy-λ>))) 392 <dummy-λ>)))))] 393 394 ꩜chunk[<eqlist-noZ> 395 ; recur 396 (⧵ captured env args 397 ; recur cmp 398 (⧵ args env args 399 ; recur cmp a 400 (⧵ (@ <pair> captured args) env args 401 ; recur+cmp a b 402 (⧵ (@ <pair> captured args) env args 403 ; a b 404 (@ (@ (@ (@ <if> env (@ (@ <or> env (@ <null?> env (@ <snd> env captured))) env (@ <null?> env args))) 405 ; a b 406 env (⧵ captured env args (@ (@ <and> env (@ <null?> env (@ <snd> env captured))) env (@ <null?> env args)))) 407 ; cmp a 408 env (⧵ captured env args (@ (@ (@ (@ <if> env (@ (@ (@ <snd> env (@ <fst> env captured)) env (@ <car> env (@ <snd> env captured))) 409 ; b 410 env (@ <car> env args))) 411 env (⧵ captured env args 412 ; recur 413 (@ (@ (@ (@ <fst> env (@ <fst> env captured)) 414 ; cmp 415 env (@ <snd> env (@ <fst> env captured))) 416 ; a 417 env (@ <cdr> env (@ <snd> env captured))) 418 ; b 419 env (@ <cdr> env args)))) 420 env (⧵ captured env args 421 <false>)) 422 env 423 args))) 424 env 425 args)))))] 426 427 ꩜chunk[<eqlist> 428 (@ <Z> env <eqlist-noZ>)] 429 430 ꩜chunk[<eqlist-bool> 431 (@ <eqlist> env <eqbool>)] 432 433 ꩜chunk[<eqlist-list-bool> 434 (@ <eqlist> env (@ <eqlist> env <eqbool>))] 435 436 ꩜chunk[<eqlist-examples> 437 ;; These return true 438 (@ (@ <eqlist-bool> env <null>) env <null>) 439 (@ (@ <eqlist-bool> env (@ (@ <cons> env <true>) env <null>)) env (@ (@ <cons> env <true>) env <null>)) 440 (@ (@ <eqlist-bool> env (@ (@ <cons> env <false>) env <null>)) env (@ (@ <cons> env <false>) env <null>)) 441 (@ (@ <eqlist-bool> env (@ (@ <cons> env <false>) env (@ (@ <cons> env <true>) env <null>))) env (@ (@ <cons> env <false>) env (@ (@ <cons> env <true>) env <null>))) 442 ;; These return false 443 (@ (@ <eqlist-bool> env <null>) env (@ (@ <cons> env <true>) env <null>)) 444 (@ (@ <eqlist-bool> env (@ (@ <cons> env <true>) env <null>)) env <null>) 445 (@ (@ <eqlist-bool> env (@ (@ <cons> env <true>) env (@ (@ <cons> env <true>) env <null>))) env <null>) 446 (@ (@ <eqlist-bool> env <null>) env (@ (@ <cons> env <true>) env (@ (@ <cons> env <true>) env <null>))) 447 (@ (@ <eqlist-bool> env (@ (@ <cons> env <true>) env <null>)) env (@ (@ <cons> env <false>) env <null>)) 448 (@ (@ <eqlist-bool> env (@ (@ <cons> env <false>) env (@ (@ <cons> env <true>) env <null>))) env (@ (@ <cons> env <false>) env (@ (@ <cons> env <false>) env <null>))) 449 ] 450 451 ꩜section{Associative lists} 452 453 ꩜chunk[<assoc-λ> 454 (λ (recur) 455 (λ (k) 456 (λ (l) 457 ((if (<null?-λ> l) 458 (λ (_) <false-λ>) 459 ((<if-λ> (<eqlist-list-bool-λ> (<fst-λ> (<car-λ> l)) k) 460 (λ (_) (<snd-λ> (<car-λ> l))) 461 (λ (_) (recur k (<cdr-λ> l)))) 462 <dummy-λ>)) 463 <dummy-λ>))))] 464 465 ꩜chunk[<assoc-noZ> 466 ; ↑recur 467 (⧵ captured env args 468 ; ↓recur↑ ↓k↑ 469 (⧵ args env args 470 ; ↓recur ↓k ↓l 471 (⧵ (@ <pair> captured args) env args 472 (@ ; ↓l 473 (@ (@ (@ <if> env (@ <null?> env args)) 474 env (⧵ captured env args <false>)) 475 env (⧵ captured env args 476 ; ↓l ↓k 477 (@ (@ (@ (@ <if> env (@ (@ <eqlist-list-bool> env (@ <car> env (@ <car> env args))) env (@ <snd> env captured))) 478 ; ↓l 479 env (⧵ captured env args(@ <cdr> env (@ <car> env args)))) 480 ; ↓recur ↓k ↓l 481 env (⧵ captured env args(@ (@ (@ <fst> env captured) env (@ <snd> env captured)) env (@ <cdr> env args)))) 482 env args))) 483 env args))))] 484 ꩜chunk[<assoc> 485 (@ <Z> env <assoc-noZ>)] 486 487 ꩜chunk[<assoc-example-letter-a> 488 (@ (@ <cons-bits> env <bit-1>) env (@ (@ <cons-bits> env <bit-1>) env <null-bits>))] 489 ꩜chunk[<assoc-example-letter-b> 490 (@ (@ <cons-bits> env <bit-1>) env (@ (@ <cons-bits> env <bit-0>) env <null-bits>))] 491 ꩜chunk[<assoc-example-k> 492 (@ (@ <cons-bytes> env <assoc-example-letter-a>) env (@ (@ <cons-bytes> env <assoc-example-letter-b>) env <null-bytes>))] 493 ꩜chunk[<assoc-example-other-k> 494 (@ (@ <cons-bytes> env <assoc-example-letter-a>) env (@ (@ <cons-bytes> env <assoc-example-letter-a>) env <null-bytes>))] 495 ꩜chunk[<assoc-example-kv> 496 (@ (@ <cons-k-v> env <assoc-example-other-k>) env <false>)] 497 ꩜chunk[<assoc-example-other-kv> 498 (@ (@ <cons-k-v> env <assoc-example-k>) env <true>)] 499 ꩜chunk[<assoc-example-env> 500 (@ (@ <env-push> env <assoc-example-other-kv>) 501 env (@ (@ <env-push> env <assoc-example-kv>) 502 env <env-null>))] 503 ꩜chunk[<assoc-example> 504 (@ (@ <env-ref> env <assoc-example-k>) 505 env 506 <assoc-example-env>)] 507 508 ꩜section{environment-manipulation functions} 509 510 ꩜chunk[<bit-0> 511 <false>] 512 ꩜chunk[<bit-1> 513 <true>] 514 515 ꩜chunk[<null-bits> 516 <null>] 517 ꩜chunk[<cons-bits> 518 <cons>] 519 520 ꩜chunk[<null-bytes> 521 <null>] 522 ꩜chunk[<cons-bytes> 523 <cons>] 524 525 ꩜chunk[<cons-k-v> 526 <cons>] 527 528 ꩜chunk[<env-null> 529 <null>] 530 ꩜chunk[<env-push> 531 <cons>] 532 ꩜chunk[<env-ref> 533 <assoc>] 534 535 ꩜section{todo} 536 537 ꩜chunk[<TODO> 538 (@ (⧵ #hash() env args 539 (list (((λλ x (λλ x 1)) 1) 2) 540 (((λλ x (λλ x x)) 1) 2) 541 (((λλ x (λλ y y)) 1) 2) 542 (((λλ x (λλ y x)) 1) 2))) 543 (hash-set env "λλ" <todo-lam-impl>) 544 (list))] 545 546 ꩜chunk[<todo-lam-impl> 547 (⧵ #hash() env args 548 (⧵ (hash "arg-name" (symbol->string (@ inspect-promise-root env (car (@ force env args)))) 549 "body" (car (cdr (@ force env args))) 550 "saved-env" env) 551 env 552 args 553 (@ (hash-ref closure "body") 554 (hash-set (hash-ref closure "saved-env") 555 (hash-ref closure "arg-name") 556 (map (make-racket-proc (⧵ #hash() env args 557 (@ force env (car args))) 558 env) 559 (@ force env args))) 560 args)))] 561 562 ꩜chunk[<*> 563 <assoc-example>]