63 Up 64
65 66 72 73 Klaus Grue 74 75 " end text ,, 76 77 78 79 text "page.tex" : ""-""; 80 81 \documentclass[fleqn]{article} 82 83 % Mark overfull lines 84 \setlength{\overfullrule}{1mm} 85 86 % Include definitions generated by lgc 87 \input{lgwinclude} 88 89 % Make latexsym characters available 90 \usepackage{latexsym} 91 92 % Ensure reasonable rendering of strings 93 \everymath{\rm} 94 \everydisplay{\rm} 95 96 % Enable generation of an index 97 \usepackage{makeidx} 98 \makeindex 99 \newcommand{\intro}[1]{\emph{#1}} 100 \newcommand{\indexintro}[1]{\index{#1}\intro{#1}} 101 102 % Enable generation of a bibliography 103 \bibliographystyle{plain} 104 105 % Enable hyperlinks 106 \usepackage[dvipdfm=true]{hyperref} 107 \hypersetup{pdfpagemode=none} 108 \hypersetup{pdfstartpage=1} 109 \hypersetup{pdfstartview=FitBH} 110 \hypersetup{pdfpagescrop={120 80 490 730}} 111 \hypersetup{pdftitle=A Logiweb test page} 112 \hypersetup{colorlinks=true} 113 114 % Construct for listing statements with associated explanations 115 \newenvironment{statements}{\begin{list}{}{ 116 \setlength{\leftmargin}{5em} 117 \setlength{\itemindent}{-5em}}}{\end{list}} 118 119 \begin{document} 120 \title{A Logiweb test page} 121 \author{Klaus Grue} 122 \maketitle 123 \tableofcontents 124 125 \section{Introduction} 126 127 This paper tests some of the constructs introduced on the base and check pages. 128 129 \section{Auxiliary definitions} 130 131 "[ "\begin{statements} 132 133 \item "[[ define value of tt as true end define ]]" 134 135 \item "[[ define value of tf as false end define ]]" 136 137 \item "[[ define value of ta as tt :: tt end define ]]" 138 139 \item "[[ define value of tb as tt :: tf end define ]]" 140 141 \item "[[ define value of tc as tf :: tt end define ]]" 142 143 \item "[[ define value of td as tf :: tf end define ]]" 144 145 \item "[[ define value of tx as exception end define ]]" 146 147 \item "[[ define value of ty as 2 raise end define ]]" 148 149 \item "[[ define value of tz as 3 raise end define ]]" 150 151 \item "[[ define value of tm as map ( \ x . x ) end define ]]" 152 153 \item "[[ define value of to as ( Zero Pair Nine ) Pair 1 end define ]]" 154 155 \item "[[ define value of tO as ( One Pair Nine ) Pair 1 end define ]]" 156 157 "";\item "[[ etst "print" ; print ( ( ty != tx ) catch ) end test ]]" 158 159 "";\item "[[ etst ty ; ty = tx end test ]]" 160 161 "";\item "[[ etst ty ; ty != tx end test ]]" 162 163 "";\item "[[ etst ty ; ty = bottom end test ]]" 164 165 \end{statements}" ]" 166 167 168 169 \section{Test of test constructs} 170 171 "[ "\begin{statements} 172 173 \item "[[ ttst true end test ]]" 174 175 \item "[[ ftst false end test ]]" 176 177 \item "[[ etst tx ; exception end test ]]" 178 179 \item "[[ etst ty ; 2 raise end test ]]" 180 181 182 183 "";\item "[[ ttst false end test ]]" 184 185 "";\item "[[ ttst exception end test ]]" 186 187 "";\item "[[ ftst true end test ]]" 188 189 "";\item "[[ ftst exception end test ]]" 190 191 "";\item "[[ etst tx ; true end test ]]" 192 193 "";\item "[[ etst tx ; false end test ]]" 194 195 "";\item "[[ etst tx ; ty end test ]]" 196 197 \end{statements}" ]" 198 199 200 201 \section{Untagged Booleans} 202 203 204 205 \subsection{Not} 206 207 "[ "\begin{statements} 208 209 \item "[[ ftst Not true end test ]]" 210 211 \item "[[ ttst Not false end test ]]" 212 213 \end{statements}" ]" 214 215 216 217 \subsection{And} 218 219 "[ "\begin{statements} 220 221 \item "[[ ttst true And true end test ]]" 222 223 \item "[[ ftst true And false end test ]]" 224 225 \item "[[ ftst false And true end test ]]" 226 227 \item "[[ ftst false And false end test ]]" 228 229 \end{statements}" ]" 230 231 232 233 \subsection{Or} 234 235 "[ "\begin{statements} 236 237 \item "[[ ttst true Or true end test ]]" 238 239 \item "[[ ttst true Or false end test ]]" 240 241 \item "[[ ttst false Or true end test ]]" 242 243 \item "[[ ftst false Or false end test ]]" 244 245 \end{statements}" ]" 246 247 248 249 \subsection{Iff} 250 251 "[ "\begin{statements} 252 253 \item "[[ ttst true Iff true end test ]]" 254 255 \item "[[ ftst true Iff false end test ]]" 256 257 \item "[[ ftst false Iff true end test ]]" 258 259 \item "[[ ttst false Iff false end test ]]" 260 261 \end{statements}" ]" 262 263 264 265 \subsection{TheBool} 266 267 "[ "\begin{statements} 268 269 \item "[[ ttst true TheBool end test ]]" 270 271 \item "[[ ftst false TheBool end test ]]" 272 273 \end{statements}" ]" 274 275 276 277 \subsection{Equal} 278 279 "[ "\begin{statements} 280 281 \item "[[ ttst true Equal true end test ]]" 282 283 \item "[[ ftst true Equal false end test ]]" 284 285 \item "[[ ftst false Equal true end test ]]" 286 287 \item "[[ ttst false Equal false end test ]]" 288 289 290 291 \item "[[ ttst true Pair true Equal true Pair true end test ]]" 292 293 \item "[[ ttst true Pair false Equal true Pair false end test ]]" 294 295 \item "[[ ttst false Pair true Equal false Pair true end test ]]" 296 297 \item "[[ ttst false Pair false Equal false Pair false end test ]]" 298 299 \item "[[ ftst false Pair true Equal true Pair true end test ]]" 300 301 \item "[[ ftst true Pair false Equal true Pair true end test ]]" 302 303 \item "[[ ftst true Pair true Equal false Pair true end test ]]" 304 305 \item "[[ ftst true Pair true Equal true Pair false end test ]]" 306 307 \end{statements}" ]" 308 309 310 311 \section{Untagged naturals} 312 313 \subsection{Small naturals} 314 315 "[ "\begin{statements} 316 317 \item "[[ ttst Zero Equal true end test ]]" 318 319 \item "[[ ttst One Equal false Pair true end test ]]" 320 321 \item "[[ ttst Two Equal true Pair false Pair true end test ]]" 322 323 \item "[[ ttst Three Equal false Pair false Pair true end test ]]" 324 325 \end{statements}" ]" 326 327 328 329 \subsection{NatPair} 330 331 "[ "\begin{statements} 332 333 \item "[[ ttst true NatPair Zero Equal Zero end test ]]" 334 335 \item "[[ ttst true NatPair One Equal Two end test ]]" 336 337 \item "[[ ttst Three NatPair true Equal One end test ]]" 338 339 \item "[[ ttst Three NatPair One Equal Three end test ]]" 340 341 \end{statements}" ]" 342 343 344 345 \subsection{TheNat} 346 347 "[ "\begin{statements} 348 349 \item "[[ ttst ( true ) TheNat Equal Zero end test ]]" 350 351 \item "[[ ttst ( true Pair true ) TheNat Equal Zero end test ]]" 352 353 \item "[[ ttst ( true Pair true Pair true ) TheNat Equal Zero end test ]]" 354 355 \item "[[ ttst ( true Pair true Pair true Pair true ) TheNat Equal Zero end test ]]" 356 357 \item "[[ ttst ( true Pair false Pair true Pair true Pair true ) TheNat Equal Two end test ]]" 358 359 \item "[[ ttst ( true Pair Three Pair true Pair true Pair true ) TheNat Equal Two end test ]]" 360 361 \end{statements}" ]" 362 363 364 365 \subsection{Xor} 366 367 "[ "\begin{statements} 368 369 \item "[[ ttst Xor ( Two , Two , true ) end test ]]" 370 371 \item "[[ ftst Xor ( Two , Two , false ) end test ]]" 372 373 \item "[[ ftst Xor ( Two , Three , true ) end test ]]" 374 375 \item "[[ ttst Xor ( Two , Three , false ) end test ]]" 376 377 \item "[[ ftst Xor ( Three , Two , true ) end test ]]" 378 379 \item "[[ ttst Xor ( Three , Two , false ) end test ]]" 380 381 \item "[[ ttst Xor ( Three , Three , true ) end test ]]" 382 383 \item "[[ ftst Xor ( Three , Three , false ) end test ]]" 384 385 \end{statements}" ]" 386 387 388 389 \subsection{Carry} 390 391 "[ "\begin{statements} 392 393 \item "[[ ttst Carry ( Two , Two , true ) end test ]]" 394 395 \item "[[ ttst Carry ( Two , Two , false ) end test ]]" 396 397 \item "[[ ttst Carry ( Two , Three , true ) end test ]]" 398 399 \item "[[ ftst Carry ( Two , Three , false ) end test ]]" 400 401 \item "[[ ttst Carry ( Three , Two , true ) end test ]]" 402 403 \item "[[ ftst Carry ( Three , Two , false ) end test ]]" 404 405 \item "[[ ftst Carry ( Three , Three , true ) end test ]]" 406 407 \item "[[ ftst Carry ( Three , Three , false ) end test ]]" 408 409 \end{statements}" ]" 410 411 412 413 \subsection{Borrow} 414 415 "[ "\begin{statements} 416 417 \item "[[ ttst Borrow ( Two , Two , true ) end test ]]" 418 419 \item "[[ ftst Borrow ( Two , Two , false ) end test ]]" 420 421 \item "[[ ftst Borrow ( Two , Three , true ) end test ]]" 422 423 \item "[[ ftst Borrow ( Two , Three , false ) end test ]]" 424 425 \item "[[ ttst Borrow ( Three , Two , true ) end test ]]" 426 427 \item "[[ ttst Borrow ( Three , Two , false ) end test ]]" 428 429 \item "[[ ttst Borrow ( Three , Three , true ) end test ]]" 430 431 \item "[[ ftst Borrow ( Three , Three , false ) end test ]]" 432 433 \end{statements}" ]" 434 435 436 437 \subsection{Plus} 438 439 "[ "\begin{statements} 440 441 \item "[[ ttst Zero Plus Zero Equal Zero end test ]]" 442 443 \item "[[ ttst Zero Plus One Equal One end test ]]" 444 445 \item "[[ ttst Zero Plus Two Equal Two end test ]]" 446 447 \item "[[ ttst Zero Plus Three Equal Three end test ]]" 448 449 \item "[[ ttst One Plus Zero Equal One end test ]]" 450 451 \item "[[ ttst One Plus One Equal Two end test ]]" 452 453 \item "[[ ttst One Plus Two Equal Three end test ]]" 454 455 \item "[[ ttst One Plus Three Equal Four end test ]]" 456 457 \item "[[ ttst Two Plus Zero Equal Two end test ]]" 458 459 \item "[[ ttst Two Plus One Equal Three end test ]]" 460 461 \item "[[ ttst Two Plus Two Equal Four end test ]]" 462 463 \item "[[ ttst Two Plus Three Equal Five end test ]]" 464 465 \item "[[ ttst Three Plus Zero Equal Three end test ]]" 466 467 \item "[[ ttst Three Plus One Equal Four end test ]]" 468 469 \item "[[ ttst Three Plus Two Equal Five end test ]]" 470 471 \item "[[ ttst Three Plus Three Equal Six end test ]]" 472 473 \end{statements}" ]" 474 475 476 477 \subsection{LT} 478 479 "[ "\begin{statements} 480 481 \item "[[ ttst Zero LT Zero Equal false end test ]]" 482 483 \item "[[ ttst Zero LT One Equal true end test ]]" 484 485 \item "[[ ttst Zero LT Two Equal true end test ]]" 486 487 \item "[[ ttst Zero LT Three Equal true end test ]]" 488 489 \item "[[ ttst One LT Zero Equal false end test ]]" 490 491 \item "[[ ttst One LT One Equal false end test ]]" 492 493 \item "[[ ttst One LT Two Equal true end test ]]" 494 495 \item "[[ ttst One LT Three Equal true end test ]]" 496 497 \item "[[ ttst Two LT Zero Equal false end test ]]" 498 499 \item "[[ ttst Two LT One Equal false end test ]]" 500 501 \item "[[ ttst Two LT Two Equal false end test ]]" 502 503 \item "[[ ttst Two LT Three Equal true end test ]]" 504 505 \item "[[ ttst Three LT Zero Equal false end test ]]" 506 507 \item "[[ ttst Three LT One Equal false end test ]]" 508 509 \item "[[ ttst Three LT Two Equal false end test ]]" 510 511 \item "[[ ttst Three LT Three Equal false end test ]]" 512 513 \end{statements}" ]" 514 515 516 517 \subsection{Minus} 518 519 "[ "\begin{statements} 520 521 \item "[[ ttst Zero Minus Zero Equal Zero end test ]]" 522 523 \item "[[ ttst One Minus Zero Equal One end test ]]" 524 525 \item "[[ ttst One Minus One Equal Zero end test ]]" 526 527 \item "[[ ttst Two Minus Zero Equal Two end test ]]" 528 529 \item "[[ ttst Two Minus One Equal One end test ]]" 530 531 \item "[[ ttst Two Minus Two Equal Zero end test ]]" 532 533 \item "[[ ttst Three Minus Zero Equal Three end test ]]" 534 535 \item "[[ ttst Three Minus One Equal Two end test ]]" 536 537 \item "[[ ttst Three Minus Two Equal One end test ]]" 538 539 \item "[[ ttst Three Minus Three Equal Zero end test ]]" 540 541 \end{statements}" ]" 542 543 544 545 \subsection{Times} 546 547 "[ "\begin{statements} 548 549 \item "[[ ttst Zero Times Zero Equal Zero end test ]]" 550 551 \item "[[ ttst Zero Times One Equal Zero end test ]]" 552 553 \item "[[ ttst Zero Times Two Equal Zero end test ]]" 554 555 \item "[[ ttst Zero Times Three Equal Zero end test ]]" 556 557 \item "[[ ttst One Times Zero Equal Zero end test ]]" 558 559 \item "[[ ttst One Times One Equal One end test ]]" 560 561 \item "[[ ttst One Times Two Equal Two end test ]]" 562 563 \item "[[ ttst One Times Three Equal Three end test ]]" 564 565 \item "[[ ttst Two Times Zero Equal Zero end test ]]" 566 567 \item "[[ ttst Two Times One Equal Two end test ]]" 568 569 \item "[[ ttst Two Times Two Equal Four end test ]]" 570 571 \item "[[ ttst Two Times Three Equal Six end test ]]" 572 573 \item "[[ ttst Three Times Zero Equal Zero end test ]]" 574 575 \item "[[ ttst Three Times One Equal Three end test ]]" 576 577 \item "[[ ttst Three Times Two Equal Six end test ]]" 578 579 \end{statements}" ]" 580 581 582 583 \section{Booleans} 584 585 \subsection{boolp} 586 587 "[ "\begin{statements} 588 589 \item "[[ ttst tt boolp end test ]]" 590 591 \item "[[ ttst tf boolp end test ]]" 592 593 \item "[[ ftst 1 boolp end test ]]" 594 595 \item "[[ ftst 2 boolp end test ]]" 596 597 \item "[[ ftst -2 boolp end test ]]" 598 599 \item "[[ ftst ta boolp end test ]]" 600 601 \item "[[ ftst tb boolp end test ]]" 602 603 \item "[[ ftst tc boolp end test ]]" 604 605 \item "[[ ftst td boolp end test ]]" 606 607 \item "[[ etst tx ; tx boolp end test ]]" 608 609 \item "[[ etst ty ; ty boolp end test ]]" 610 611 \item "[[ ftst tm boolp end test ]]" 612 613 \item "[[ ftst to boolp end test ]]" 614 615 \item "[[ ftst tO boolp end test ]]" 616 617 \end{statements}" ]" 618 619 620 621 \subsection{truep} 622 623 "[ "\begin{statements} 624 625 \item "[[ ttst tt truep end test ]]" 626 627 \item "[[ ftst tf truep end test ]]" 628 629 \item "[[ ftst 1 truep end test ]]" 630 631 \item "[[ ftst 2 truep end test ]]" 632 633 \item "[[ ftst -2 truep end test ]]" 634 635 \item "[[ ftst ta truep end test ]]" 636 637 \item "[[ ftst tb truep end test ]]" 638 639 \item "[[ ftst tc truep end test ]]" 640 641 \item "[[ ftst td truep end test ]]" 642 643 \item "[[ etst tx ; tx truep end test ]]" 644 645 \item "[[ etst ty ; ty truep end test ]]" 646 647 \item "[[ ftst tm truep end test ]]" 648 649 \item "[[ ftst to truep end test ]]" 650 651 \item "[[ ftst tO truep end test ]]" 652 653 \end{statements}" ]" 654 655 656 657 \subsection{falsep} 658 659 "[ "\begin{statements} 660 661 \item "[[ ftst tt falsep end test ]]" 662 663 \item "[[ ttst tf falsep end test ]]" 664 665 \item "[[ ftst 1 falsep end test ]]" 666 667 \item "[[ ftst 2 falsep end test ]]" 668 669 \item "[[ ftst -2 falsep end test ]]" 670 671 \item "[[ ftst ta falsep end test ]]" 672 673 \item "[[ ftst tb falsep end test ]]" 674 675 \item "[[ ftst tc falsep end test ]]" 676 677 \item "[[ ftst td falsep end test ]]" 678 679 \item "[[ etst tx ; tx falsep end test ]]" 680 681 \item "[[ etst ty ; ty falsep end test ]]" 682 683 \item "[[ ftst tm falsep end test ]]" 684 685 \item "[[ ftst to falsep end test ]]" 686 687 \item "[[ ftst tO falsep end test ]]" 688 689 \end{statements}" ]" 690 691 692 693 \subsection{if-then-else} 694 695 "[ "\begin{statements} 696 697 \item "[[ ttst if tt then tt else tt end test ]]" 698 699 \item "[[ ttst if tt then tt else tf end test ]]" 700 701 \item "[[ ftst if tt then tf else tt end test ]]" 702 703 \item "[[ ftst if tt then tf else tf end test ]]" 704 705 \item "[[ ttst if tf then tt else tt end test ]]" 706 707 \item "[[ ftst if tf then tt else tf end test ]]" 708 709 \item "[[ ttst if tf then tf else tt end test ]]" 710 711 \item "[[ ftst if tf then tf else tf end test ]]" 712 713 \item "[[ ftst if tf then tf else tf end test ]]" 714 715 \item "[[ etst 8 ; if 1 then 7 else 8 end test ]]" 716 717 \item "[[ etst 8 ; if 2 then 7 else 8 end test ]]" 718 719 \item "[[ etst 8 ; if -2 then 7 else 8 end test ]]" 720 721 \item "[[ etst 8 ; if ta then 7 else 8 end test ]]" 722 723 \item "[[ etst 8 ; if tb then 7 else 8 end test ]]" 724 725 \item "[[ etst 8 ; if tc then 7 else 8 end test ]]" 726 727 \item "[[ etst 8 ; if td then 7 else 8 end test ]]" 728 729 \item "[[ etst 8 ; if tm then 7 else 8 end test ]]" 730 731 \item "[[ etst tx ; if tx then 7 else 8 end test ]]" 732 733 \item "[[ etst ty ; if ty then 7 else 8 end test ]]" 734 735 \item "[[ etst 8 ; if to then 7 else 8 end test ]]" 736 737 \item "[[ etst 8 ; if tO then 7 else 8 end test ]]" 738 739 \end{statements}" ]" 740 741 742 743 \subsection{not} 744 745 "[ "\begin{statements} 746 747 \item "[[ ftst .not. tt end test ]]" 748 749 \item "[[ ttst .not. tf end test ]]" 750 751 \item "[[ ttst .not. 1 end test ]]" 752 753 \item "[[ ttst .not. 2 end test ]]" 754 755 \item "[[ ttst .not. -2 end test ]]" 756 757 \item "[[ ttst .not. ta end test ]]" 758 759 \item "[[ ttst .not. tb end test ]]" 760 761 \item "[[ ttst .not. tc end test ]]" 762 763 \item "[[ ttst .not. td end test ]]" 764 765 \item "[[ etst tx ; .not. tx end test ]]" 766 767 \item "[[ etst ty ; .not. ty end test ]]" 768 769 \item "[[ ttst .not. tm end test ]]" 770 771 \item "[[ ttst .not. to end test ]]" 772 773 \item "[[ ttst .not. tO end test ]]" 774 775 \end{statements}" ]" 776 777 778 779 \subsection{notnot} 780 781 "[ "\begin{statements} 782 783 \item "[[ ttst notnot tt end test ]]" 784 785 \item "[[ ftst notnot tf end test ]]" 786 787 \item "[[ ftst notnot 1 end test ]]" 788 789 \item "[[ ftst notnot 2 end test ]]" 790 791 \item "[[ ftst notnot -2 end test ]]" 792 793 \item "[[ ftst notnot ta end test ]]" 794 795 \item "[[ ftst notnot tb end test ]]" 796 797 \item "[[ ftst notnot tc end test ]]" 798 799 \item "[[ ftst notnot td end test ]]" 800 801 \item "[[ etst tx ; notnot tx end test ]]" 802 803 \item "[[ etst ty ; notnot ty end test ]]" 804 805 \item "[[ ftst notnot tm end test ]]" 806 807 \item "[[ ftst notnot to end test ]]" 808 809 \item "[[ ftst notnot tO end test ]]" 810 811 \end{statements}" ]" 812 813 814 815 \subsection{and} 816 817 "[ "\begin{statements} 818 819 \item "[[ ttst tt .and. tt end test ]]" 820 821 \item "[[ ftst tt .and. tf end test ]]" 822 823 \item "[[ etst tx ; tt .and. tx end test ]]" 824 825 \item "[[ etst ty ; tt .and. ty end test ]]" 826 827 \item "[[ ftst tf .and. tt end test ]]" 828 829 \item "[[ ftst tf .and. tf end test ]]" 830 831 \item "[[ ftst tf .and. tx end test ]]" 832 833 \item "[[ ftst tf .and. ty end test ]]" 834 835 \item "[[ ftst tf .and. bottom end test ]]" 836 837 \item "[[ etst tx ; tx .and. tt end test ]]" 838 839 \item "[[ etst tx ; tx .and. tf end test ]]" 840 841 \item "[[ etst tx ; tx .and. tx end test ]]" 842 843 \item "[[ etst tx ; tx .and. ty end test ]]" 844 845 \item "[[ etst tx ; tx .and. bottom end test ]]" 846 847 \item "[[ etst ty ; ty .and. tt end test ]]" 848 849 \item "[[ etst ty ; ty .and. tf end test ]]" 850 851 \item "[[ etst ty ; ty .and. tx end test ]]" 852 853 \item "[[ etst ty ; ty .and. ty end test ]]" 854 855 \item "[[ etst ty ; ty .and. bottom end test ]]" 856 857 \item "[[ etst 1 ; 1 .and. tf end test ]]" 858 859 \item "[[ etst 2 ; 2 .and. tf end test ]]" 860 861 \item "[[ etst -2 ; -2 .and. tf end test ]]" 862 863 \item "[[ etst ta ; ta .and. tf end test ]]" 864 865 \item "[[ etst tb ; tb .and. tf end test ]]" 866 867 \item "[[ etst tc ; tc .and. tf end test ]]" 868 869 \item "[[ etst td ; td .and. tf end test ]]" 870 871 \item "[[ etst tm ; tm .and. tf end test ]]" 872 873 \item "[[ etst to ; to .and. tf end test ]]" 874 875 \item "[[ etst tO ; tO .and. tf end test ]]" 876 877 \item "[[ etst 1 ; tt .and. 1 end test ]]" 878 879 \item "[[ etst 2 ; tt .and. 2 end test ]]" 880 881 \item "[[ etst -2 ; tt .and. -2 end test ]]" 882 883 \item "[[ etst ta ; tt .and. ta end test ]]" 884 885 \item "[[ etst tb ; tt .and. tb end test ]]" 886 887 \item "[[ etst tc ; tt .and. tc end test ]]" 888 889 \item "[[ etst td ; tt .and. td end test ]]" 890 891 \item "[[ etst tm ; tt .and. tm end test ]]" 892 893 \item "[[ etst to ; tt .and. to end test ]]" 894 895 \item "[[ etst tO ; tt .and. tO end test ]]" 896 897 \end{statements}" ]" 898 899 900 901 \subsection{or} 902 903 "[ "\begin{statements} 904 905 \item "[[ ttst tt .or. tt end test ]]" 906 907 \item "[[ ttst tt .or. tf end test ]]" 908 909 \item "[[ ttst tt .or. tx end test ]]" 910 911 \item "[[ ttst tf .or. tt end test ]]" 912 913 \item "[[ ftst tf .or. tf end test ]]" 914 915 \item "[[ etst tx ; tf .or. tx end test ]]" 916 917 \item "[[ etst tx ; tx .or. tt end test ]]" 918 919 \item "[[ etst tx ; tx .or. tf end test ]]" 920 921 \item "[[ etst ty ; ty .or. tx end test ]]" 922 923 \item "[[ etst 8 ; 1 .or. 8 end test ]]" 924 925 \item "[[ etst 8 ; 2 .or. 8 end test ]]" 926 927 \item "[[ etst 8 ; -2 .or. 8 end test ]]" 928 929 \item "[[ etst 8 ; ta .or. 8 end test ]]" 930 931 \item "[[ etst 8 ; tb .or. 8 end test ]]" 932 933 \item "[[ etst 8 ; tc .or. 8 end test ]]" 934 935 \item "[[ etst 8 ; td .or. 8 end test ]]" 936 937 \item "[[ etst 8 ; tm .or. 8 end test ]]" 938 939 \item "[[ etst 8 ; to .or. 8 end test ]]" 940 941 \item "[[ etst 8 ; tO .or. 8 end test ]]" 942 943 \item "[[ etst 1 ; 2 .or. 1 end test ]]" 944 945 \item "[[ etst 2 ; -2 .or. 2 end test ]]" 946 947 \item "[[ etst -2 ; ta .or. -2 end test ]]" 948 949 \item "[[ etst ta ; tb .or. ta end test ]]" 950 951 \item "[[ etst tb ; tc .or. tb end test ]]" 952 953 \item "[[ etst tc ; td .or. tc end test ]]" 954 955 \item "[[ etst td ; tm .or. td end test ]]" 956 957 \item "[[ etst tm ; to .or. tm end test ]]" 958 959 \item "[[ etst to ; tO .or. to end test ]]" 960 961 \item "[[ etst tO ; 1 .or. tO end test ]]" 962 963 \end{statements}" ]" 964 965 966 967 \subsection{"[[ x = y ]]"} 968 969 "[ "\begin{statements} 970 971 \item "[[ ttst tt = tt end test ]]" 972 973 \item "[[ ftst tt = tf end test ]]" 974 975 \item "[[ ftst tt = 1 end test ]]" 976 977 \item "[[ ftst tt = 2 end test ]]" 978 979 \item "[[ ftst tt = -2 end test ]]" 980 981 \item "[[ ftst tt = ta end test ]]" 982 983 \item "[[ ftst tt = tb end test ]]" 984 985 \item "[[ ftst tt = tc end test ]]" 986 987 \item "[[ ftst tt = td end test ]]" 988 989 \item "[[ etst ty ; tt = ty end test ]]" 990 991 \item "[[ ftst tt = tm end test ]]" 992 993 \item "[[ ftst tt = to end test ]]" 994 995 \item "[[ ftst tt = tO end test ]]" 996 997 998 999 \item "[[ ftst tf = tt end test ]]" 1000 1001 \item "[[ ttst tf = tf end test ]]" 1002 1003 \item "[[ ftst tf = 1 end test ]]" 1004 1005 \item "[[ ftst tf = 2 end test ]]" 1006 1007 \item "[[ ftst tf = -2 end test ]]" 1008 1009 \item "[[ ftst tf = ta end test ]]" 1010 1011 \item "[[ ftst tf = tb end test ]]" 1012 1013 \item "[[ ftst tf = tc end test ]]" 1014 1015 \item "[[ ftst tf = td end test ]]" 1016 1017 \item "[[ etst ty ; tf = ty end test ]]" 1018 1019 \item "[[ ftst tf = tm end test ]]" 1020 1021 \item "[[ ftst tf = to end test ]]" 1022 1023 \item "[[ ftst tf = tO end test ]]" 1024 1025 1026 1027 \item "[[ ftst 1 = tt end test ]]" 1028 1029 \item "[[ ftst 1 = tf end test ]]" 1030 1031 \item "[[ ttst 1 = 1 end test ]]" 1032 1033 \item "[[ ftst 1 = 2 end test ]]" 1034 1035 \item "[[ ftst 1 = -2 end test ]]" 1036 1037 \item "[[ ftst 1 = ta end test ]]" 1038 1039 \item "[[ ftst 1 = tb end test ]]" 1040 1041 \item "[[ ftst 1 = tc end test ]]" 1042 1043 \item "[[ ftst 1 = td end test ]]" 1044 1045 \item "[[ etst ty ; 1 = ty end test ]]" 1046 1047 \item "[[ ftst 1 = tm end test ]]" 1048 1049 \item "[[ ftst 1 = to end test ]]" 1050 1051 \item "[[ ftst 1 = tO end test ]]" 1052 1053 1054 1055 \item "[[ ftst 2 = tt end test ]]" 1056 1057 \item "[[ ftst 2 = tf end test ]]" 1058 1059 \item "[[ ftst 2 = 1 end test ]]" 1060 1061 \item "[[ ttst 2 = 2 end test ]]" 1062 1063 \item "[[ ftst 2 = -2 end test ]]" 1064 1065 \item "[[ ftst 2 = ta end test ]]" 1066 1067 \item "[[ ftst 2 = tb end test ]]" 1068 1069 \item "[[ ftst 2 = tc end test ]]" 1070 1071 \item "[[ ftst 2 = td end test ]]" 1072 1073 \item "[[ etst ty ; 2 = ty end test ]]" 1074 1075 \item "[[ ftst 2 = tm end test ]]" 1076 1077 \item "[[ ftst 2 = to end test ]]" 1078 1079 \item "[[ ftst 2 = tO end test ]]" 1080 1081 1082 1083 \item "[[ ftst -2 = tt end test ]]" 1084 1085 \item "[[ ftst -2 = tf end test ]]" 1086 1087 \item "[[ ftst -2 = 1 end test ]]" 1088 1089 \item "[[ ftst -2 = 2 end test ]]" 1090 1091 \item "[[ ttst -2 = -2 end test ]]" 1092 1093 \item "[[ ftst -2 = ta end test ]]" 1094 1095 \item "[[ ftst -2 = tb end test ]]" 1096 1097 \item "[[ ftst -2 = tc end test ]]" 1098 1099 \item "[[ ftst -2 = td end test ]]" 1100 1101 \item "[[ etst ty ; -2 = ty end test ]]" 1102 1103 \item "[[ ftst -2 = tm end test ]]" 1104 1105 \item "[[ ftst -2 = to end test ]]" 1106 1107 \item "[[ ftst -2 = tO end test ]]" 1108 1109 1110 1111 \item "[[ ftst ta = tt end test ]]" 1112 1113 \item "[[ ftst ta = tf end test ]]" 1114 1115 \item "[[ ftst ta = 1 end test ]]" 1116 1117 \item "[[ ftst ta = 2 end test ]]" 1118 1119 \item "[[ ftst ta = -2 end test ]]" 1120 1121 \item "[[ ttst ta = ta end test ]]" 1122 1123 \item "[[ ftst ta = tb end test ]]" 1124 1125 \item "[[ ftst ta = tc end test ]]" 1126 1127 \item "[[ ftst ta = td end test ]]" 1128 1129 \item "[[ etst ty ; ta = ty end test ]]" 1130 1131 \item "[[ ftst ta = tm end test ]]" 1132 1133 \item "[[ ftst ta = to end test ]]" 1134 1135 \item "[[ ftst ta = tO end test ]]" 1136 1137 1138 1139 \item "[[ ftst tb = tt end test ]]" 1140 1141 \item "[[ ftst tb = tf end test ]]" 1142 1143 \item "[[ ftst tb = 1 end test ]]" 1144 1145 \item "[[ ftst tb = 2 end test ]]" 1146 1147 \item "[[ ftst tb = -2 end test ]]" 1148 1149 \item "[[ ftst tb = ta end test ]]" 1150 1151 \item "[[ ttst tb = tb end test ]]" 1152 1153 \item "[[ ftst tb = tc end test ]]" 1154 1155 \item "[[ ftst tb = td end test ]]" 1156 1157 \item "[[ etst ty ; tb = ty end test ]]" 1158 1159 \item "[[ ftst tb = tm end test ]]" 1160 1161 \item "[[ ftst tb = to end test ]]" 1162 1163 \item "[[ ftst tb = tO end test ]]" 1164 1165 1166 1167 \item "[[ ftst tc = tt end test ]]" 1168 1169 \item "[[ ftst tc = tf end test ]]" 1170 1171 \item "[[ ftst tc = 1 end test ]]" 1172 1173 \item "[[ ftst tc = 2 end test ]]" 1174 1175 \item "[[ ftst tc = -2 end test ]]" 1176 1177 \item "[[ ftst tc = ta end test ]]" 1178 1179 \item "[[ ftst tc = tb end test ]]" 1180 1181 \item "[[ ttst tc = tc end test ]]" 1182 1183 \item "[[ ftst tc = td end test ]]" 1184 1185 \item "[[ etst ty ; tc = ty end test ]]" 1186 1187 \item "[[ ftst tc = tm end test ]]" 1188 1189 \item "[[ ftst tc = to end test ]]" 1190 1191 \item "[[ ftst tc = tO end test ]]" 1192 1193 1194 1195 \item "[[ ftst td = tt end test ]]" 1196 1197 \item "[[ ftst td = tf end test ]]" 1198 1199 \item "[[ ftst td = 1 end test ]]" 1200 1201 \item "[[ ftst td = 2 end test ]]" 1202 1203 \item "[[ ftst td = -2 end test ]]" 1204 1205 \item "[[ ftst td = ta end test ]]" 1206 1207 \item "[[ ftst td = tb end test ]]" 1208 1209 \item "[[ ftst td = tc end test ]]" 1210 1211 \item "[[ ttst td = td end test ]]" 1212 1213 \item "[[ etst ty ; td = ty end test ]]" 1214 1215 \item "[[ ftst td = tm end test ]]" 1216 1217 \item "[[ ftst td = to end test ]]" 1218 1219 \item "[[ ftst td = tO end test ]]" 1220 1221 1222 1223 \item "[[ etst ty ; ty = tt end test ]]" 1224 1225 \item "[[ etst ty ; ty = tf end test ]]" 1226 1227 \item "[[ etst ty ; ty = 1 end test ]]" 1228 1229 \item "[[ etst ty ; ty = 2 end test ]]" 1230 1231 \item "[[ etst ty ; ty = -2 end test ]]" 1232 1233 \item "[[ etst ty ; ty = ta end test ]]" 1234 1235 \item "[[ etst ty ; ty = tb end test ]]" 1236 1237 \item "[[ etst ty ; ty = tc end test ]]" 1238 1239 \item "[[ etst ty ; ty = td end test ]]" 1240 1241 \item "[[ etst ty ; ty = tx end test ]]" 1242 1243 \item "[[ etst ty ; ty = tm end test ]]" 1244 1245 \item "[[ etst ty ; ty = to end test ]]" 1246 1247 \item "[[ etst ty ; ty = tO end test ]]" 1248 1249 1250 1251 \item "[[ ftst tm = tt end test ]]" 1252 1253 \item "[[ ftst tm = tf end test ]]" 1254 1255 \item "[[ ftst tm = 1 end test ]]" 1256 1257 \item "[[ ftst tm = 2 end test ]]" 1258 1259 \item "[[ ftst tm = -2 end test ]]" 1260 1261 \item "[[ ftst tm = ta end test ]]" 1262 1263 \item "[[ ftst tm = tb end test ]]" 1264 1265 \item "[[ ftst tm = tc end test ]]" 1266 1267 \item "[[ ftst tm = td end test ]]" 1268 1269 \item "[[ etst ty ; tm = ty end test ]]" 1270 1271 \item "[[ ttst tm = tm end test ]]" 1272 1273 \item "[[ ftst tm = to end test ]]" 1274 1275 \item "[[ ftst tm = tO end test ]]" 1276 1277 1278 1279 \item "[[ ftst to = tt end test ]]" 1280 1281 \item "[[ ftst to = tf end test ]]" 1282 1283 \item "[[ ftst to = 1 end test ]]" 1284 1285 \item "[[ ftst to = 2 end test ]]" 1286 1287 \item "[[ ftst to = -2 end test ]]" 1288 1289 \item "[[ ftst to = ta end test ]]" 1290 1291 \item "[[ ftst to = tb end test ]]" 1292 1293 \item "[[ ftst to = tc end test ]]" 1294 1295 \item "[[ ftst to = td end test ]]" 1296 1297 \item "[[ etst ty ; to = ty end test ]]" 1298 1299 \item "[[ ftst to = tm end test ]]" 1300 1301 \item "[[ ttst to = to end test ]]" 1302 1303 \item "[[ ftst to = tO end test ]]" 1304 1305 1306 1307 \item "[[ ftst tO = tt end test ]]" 1308 1309 \item "[[ ftst tO = tf end test ]]" 1310 1311 \item "[[ ftst tO = 1 end test ]]" 1312 1313 \item "[[ ftst tO = 2 end test ]]" 1314 1315 \item "[[ ftst tO = -2 end test ]]" 1316 1317 \item "[[ ftst tO = ta end test ]]" 1318 1319 \item "[[ ftst tO = tb end test ]]" 1320 1321 \item "[[ ftst tO = tc end test ]]" 1322 1323 \item "[[ ftst tO = td end test ]]" 1324 1325 \item "[[ etst ty ; tO = ty end test ]]" 1326 1327 \item "[[ ftst tO = tm end test ]]" 1328 1329 \item "[[ ftst tO = to end test ]]" 1330 1331 \item "[[ ttst tO = tO end test ]]" 1332 1333 1334 1335 \item "[[ ttst ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: tf ) :: ( ta :: tb ) ) end test ]]" 1336 1337 \item "[[ ftst ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tc :: tf ) :: ( ta :: tb ) ) end test ]]" 1338 1339 \item "[[ ftst ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: tc ) :: ( ta :: tb ) ) end test ]]" 1340 1341 \item "[[ ftst ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: tf ) :: ( tc :: tb ) ) end test ]]" 1342 1343 \item "[[ ftst ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: tf ) :: ( ta :: tc ) ) end test ]]" 1344 1345 \item "[[ etst ty ; ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( ty :: tf ) :: ( ta :: tb ) ) end test ]]" 1346 1347 \item "[[ etst ty ; ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: ty ) :: ( ta :: tb ) ) end test ]]" 1348 1349 \item "[[ etst ty ; ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: tf ) :: ( ty :: tb ) ) end test ]]" 1350 1351 \item "[[ etst ty ; ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: tf ) :: ( ta :: ty ) ) end test ]]" 1352 1353 \item "[[ etst ty ; ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: ty ) :: ( tz :: tb ) ) end test ]]" 1354 1355 \end{statements}" ]" 1356 1357 1358 1359 \subsection{"[[ x != y ]]"} 1360 1361 "[ "\begin{statements} 1362 1363 \item "[[ ftst tt != tt end test ]]" 1364 1365 \item "[[ ttst tt != tf end test ]]" 1366 1367 \item "[[ etst ty ; tt != ty end test ]]" 1368 1369 \item "[[ ttst tf != tt end test ]]" 1370 1371 \item "[[ ftst tf != tf end test ]]" 1372 1373 \item "[[ etst ty ; tf != ty end test ]]" 1374 1375 \item "[[ etst ty ; ty != tt end test ]]" 1376 1377 \item "[[ etst ty ; ty != tf end test ]]" 1378 1379 \item "[[ etst ty ; ty != tx end test ]]" 1380 1381 \end{statements}" ]" 1382 1383 1384 1385 \section{Integers} 1386 1387 \subsection{intp} 1388 1389 "[ "\begin{statements} 1390 1391 \item "[[ ftst tt intp end test ]]" 1392 1393 \item "[[ ftst tf intp end test ]]" 1394 1395 \item "[[ ttst 1 intp end test ]]" 1396 1397 \item "[[ ttst 2 intp end test ]]" 1398 1399 \item "[[ ttst -2 intp end test ]]" 1400 1401 \item "[[ ftst ta intp end test ]]" 1402 1403 \item "[[ ftst tb intp end test ]]" 1404 1405 \item "[[ ftst tc intp end test ]]" 1406 1407 \item "[[ ftst td intp end test ]]" 1408 1409 \item "[[ etst ty ; ty intp end test ]]" 1410 1411 \item "[[ ftst tm intp end test ]]" 1412 1413 \item "[[ ftst to intp end test ]]" 1414 1415 \item "[[ ftst tO intp end test ]]" 1416 1417 \end{statements}" ]" 1418 1419 1420 1421 \subsection{TheInt} 1422 1423 "[ "\begin{statements} 1424 1425 \item "[[ ttst TheInt ( true , Zero ) = TheInt ( false , Zero ) end test ]]" 1426 1427 \item "[[ ttst TheInt ( true , Zero ) = 0 end test ]]" 1428 1429 \item "[[ ttst TheInt ( true , One ) = 1 end test ]]" 1430 1431 \item "[[ ttst TheInt ( true , Two ) = 2 end test ]]" 1432 1433 \item "[[ ttst TheInt ( true , Three ) = 3 end test ]]" 1434 1435 \item "[[ ttst TheInt ( true , Four ) = 4 end test ]]" 1436 1437 \item "[[ ttst TheInt ( true , Five ) = 5 end test ]]" 1438 1439 \item "[[ ttst TheInt ( true , Six ) = 6 end test ]]" 1440 1441 \item "[[ ttst TheInt ( true , Seven ) = 7 end test ]]" 1442 1443 \item "[[ ttst TheInt ( true , Eight ) = 8 end test ]]" 1444 1445 \item "[[ ttst TheInt ( true , Nine ) = 9 end test ]]" 1446 1447 \item "[[ ttst TheInt ( false , Zero ) = - 0 end test ]]" 1448 1449 \item "[[ ttst TheInt ( false , One ) = -1 end test ]]" 1450 1451 \item "[[ ttst TheInt ( false , Two ) = -2 end test ]]" 1452 1453 \item "[[ ttst TheInt ( false , Three ) = -3 end test ]]" 1454 1455 \item "[[ ttst TheInt ( false , Four ) = -4 end test ]]" 1456 1457 \item "[[ ttst TheInt ( false , Five ) = -5 end test ]]" 1458 1459 \item "[[ ttst TheInt ( false , Six ) = -6 end test ]]" 1460 1461 \item "[[ ttst TheInt ( false , Seven ) = -7 end test ]]" 1462 1463 \item "[[ ttst TheInt ( false , Eight ) = -8 end test ]]" 1464 1465 \item "[[ ttst TheInt ( false , Nine ) = -9 end test ]]" 1466 1467 \end{statements}" ]" 1468 1469 1470 1471 \subsection{PlusTag} 1472 1473 "[ "\begin{statements} 1474 1475 \item "[[ ttst PlusTag ( Zero ) = 0 end test ]]" 1476 1477 \item "[[ ttst PlusTag ( One ) = 1 end test ]]" 1478 1479 \item "[[ ttst PlusTag ( Two ) = 2 end test ]]" 1480 1481 \item "[[ ttst PlusTag ( Three ) = 3 end test ]]" 1482 1483 \item "[[ ttst PlusTag ( Four ) = 4 end test ]]" 1484 1485 \item "[[ ttst PlusTag ( Five ) = 5 end test ]]" 1486 1487 \item "[[ ttst PlusTag ( Six ) = 6 end test ]]" 1488 1489 \item "[[ ttst PlusTag ( Seven ) = 7 end test ]]" 1490 1491 \item "[[ ttst PlusTag ( Eight ) = 8 end test ]]" 1492 1493 \item "[[ ttst PlusTag ( Nine ) = 9 end test ]]" 1494 1495 \end{statements}" ]" 1496 1497 1498 1499 \subsection{MinusTag} 1500 1501 "[ "\begin{statements} 1502 1503 \item "[[ ttst MinusTag ( Zero ) = - 0 end test ]]" 1504 1505 \item "[[ ttst MinusTag ( One ) = -1 end test ]]" 1506 1507 \item "[[ ttst MinusTag ( Two ) = -2 end test ]]" 1508 1509 \item "[[ ttst MinusTag ( Three ) = -3 end test ]]" 1510 1511 \item "[[ ttst MinusTag ( Four ) = -4 end test ]]" 1512 1513 \item "[[ ttst MinusTag ( Five ) = -5 end test ]]" 1514 1515 \item "[[ ttst MinusTag ( Six ) = -6 end test ]]" 1516 1517 \item "[[ ttst MinusTag ( Seven ) = -7 end test ]]" 1518 1519 \item "[[ ttst MinusTag ( Eight ) = -8 end test ]]" 1520 1521 \item "[[ ttst MinusTag ( Nine ) = -9 end test ]]" 1522 1523 \end{statements}" ]" 1524 1525 1526 1527 \subsection{"[[ x + y ]]"} 1528 1529 "[ "\begin{statements} 1530 1531 \item "[[ etst tx ; tt + 1 end test ]]" 1532 1533 \item "[[ etst tx ; tf + 1 end test ]]" 1534 1535 \item "[[ etst tx ; ta + 1 end test ]]" 1536 1537 \item "[[ etst tx ; tb + 1 end test ]]" 1538 1539 \item "[[ etst tx ; tc + 1 end test ]]" 1540 1541 \item "[[ etst tx ; td + 1 end test ]]" 1542 1543 \item "[[ etst tx ; tx + 1 end test ]]" 1544 1545 \item "[[ etst ty ; ty + 1 end test ]]" 1546 1547 \item "[[ etst tx ; tm + 1 end test ]]" 1548 1549 \item "[[ etst tx ; to + 1 end test ]]" 1550 1551 \item "[[ etst tx ; tO + 1 end test ]]" 1552 1553 \item "[[ etst tx ; 1 + tt end test ]]" 1554 1555 \item "[[ etst tx ; 1 + tf end test ]]" 1556 1557 \item "[[ etst tx ; 1 + ta end test ]]" 1558 1559 \item "[[ etst tx ; 1 + tb end test ]]" 1560 1561 \item "[[ etst tx ; 1 + tc end test ]]" 1562 1563 \item "[[ etst tx ; 1 + td end test ]]" 1564 1565 \item "[[ etst tx ; 1 + tx end test ]]" 1566 1567 \item "[[ etst ty ; 1 + ty end test ]]" 1568 1569 \item "[[ etst tx ; 1 + tm end test ]]" 1570 1571 \item "[[ etst tx ; 1 + to end test ]]" 1572 1573 \item "[[ etst tx ; 1 + tO end test ]]" 1574 1575 \item "[[ etst ty ; ta + ty end test ]]" 1576 1577 \item "[[ etst ty ; ty + ta end test ]]" 1578 1579 \item "[[ etst ty ; ty + bottom end test ]]" 1580 1581 \item "[[ ttst 2 + 3 = 5 end test ]]" 1582 1583 \item "[[ ttst 2 + -3 = -1 end test ]]" 1584 1585 \item "[[ ttst -2 + 3 = 1 end test ]]" 1586 1587 \item "[[ ttst -2 + -3 = -5 end test ]]" 1588 1589 \item "[[ ttst 3 + 2 = 5 end test ]]" 1590 1591 \item "[[ ttst -3 + 2 = -1 end test ]]" 1592 1593 \item "[[ ttst 3 + -2 = 1 end test ]]" 1594 1595 \item "[[ ttst -3 + -2 = -5 end test ]]" 1596 1597 \end{statements}" ]" 1598 1599 1600 1601 \subsection{"[[ x - y ]]"} 1602 1603 "[ "\begin{statements} 1604 1605 \item "[[ etst tx ; tt - 1 end test ]]" 1606 1607 \item "[[ etst tx ; tf - 1 end test ]]" 1608 1609 \item "[[ etst tx ; ta - 1 end test ]]" 1610 1611 \item "[[ etst tx ; tb - 1 end test ]]" 1612 1613 \item "[[ etst tx ; tc - 1 end test ]]" 1614 1615 \item "[[ etst tx ; td - 1 end test ]]" 1616 1617 \item "[[ etst tx ; tx - 1 end test ]]" 1618 1619 \item "[[ etst ty ; ty - 1 end test ]]" 1620 1621 \item "[[ etst tx ; tm - 1 end test ]]" 1622 1623 \item "[[ etst tx ; to - 1 end test ]]" 1624 1625 \item "[[ etst tx ; tO - 1 end test ]]" 1626 1627 \item "[[ etst tx ; 1 - tt end test ]]" 1628 1629 \item "[[ etst tx ; 1 - tf end test ]]" 1630 1631 \item "[[ etst tx ; 1 - ta end test ]]" 1632 1633 \item "[[ etst tx ; 1 - tb end test ]]" 1634 1635 \item "[[ etst tx ; 1 - tc end test ]]" 1636 1637 \item "[[ etst tx ; 1 - td end test ]]" 1638 1639 \item "[[ etst tx ; 1 - tx end test ]]" 1640 1641 \item "[[ etst ty ; 1 - ty end test ]]" 1642 1643 \item "[[ etst tx ; 1 - tm end test ]]" 1644 1645 \item "[[ etst tx ; 1 - to end test ]]" 1646 1647 \item "[[ etst tx ; 1 - tO end test ]]" 1648 1649 \item "[[ etst ty ; ty - ta end test ]]" 1650 1651 \item "[[ etst ty ; ta - ty end test ]]" 1652 1653 \item "[[ etst ty ; ty - bottom end test ]]" 1654 1655 \item "[[ ttst 2 - 3 = -1 end test ]]" 1656 1657 \item "[[ ttst 2 - -3 = 5 end test ]]" 1658 1659 \item "[[ ttst -2 - 3 = -5 end test ]]" 1660 1661 \item "[[ ttst -2 - -3 = 1 end test ]]" 1662 1663 \item "[[ ttst 3 - 2 = 1 end test ]]" 1664 1665 \item "[[ ttst -3 - 2 = -5 end test ]]" 1666 1667 \item "[[ ttst 3 - -2 = 5 end test ]]" 1668 1669 \item "[[ ttst -3 - -2 = -1 end test ]]" 1670 1671 \end{statements}" ]" 1672 1673 1674 1675 \subsection{"[[ x * y ]]"} 1676 1677 "[ "\begin{statements} 1678 1679 \item "[[ etst tx ; tt * 1 end test ]]" 1680 1681 \item "[[ etst tx ; tf * 1 end test ]]" 1682 1683 \item "[[ etst tx ; ta * 1 end test ]]" 1684 1685 \item "[[ etst tx ; tb * 1 end test ]]" 1686 1687 \item "[[ etst tx ; tc * 1 end test ]]" 1688 1689 \item "[[ etst tx ; td * 1 end test ]]" 1690 1691 \item "[[ etst tx ; tx * 1 end test ]]" 1692 1693 \item "[[ etst ty ; ty * 1 end test ]]" 1694 1695 \item "[[ etst tx ; tm * 1 end test ]]" 1696 1697 \item "[[ etst tx ; to * 1 end test ]]" 1698 1699 \item "[[ etst tx ; tO * 1 end test ]]" 1700 1701 \item "[[ etst tx ; 1 * tt end test ]]" 1702 1703 \item "[[ etst tx ; 1 * tf end test ]]" 1704 1705 \item "[[ etst tx ; 1 * ta end test ]]" 1706 1707 \item "[[ etst tx ; 1 * tb end test ]]" 1708 1709 \item "[[ etst tx ; 1 * tc end test ]]" 1710 1711 \item "[[ etst tx ; 1 * td end test ]]" 1712 1713 \item "[[ etst tx ; 1 * tx end test ]]" 1714 1715 \item "[[ etst ty ; 1 * ty end test ]]" 1716 1717 \item "[[ etst tx ; 1 * tm end test ]]" 1718 1719 \item "[[ etst tx ; 1 * to end test ]]" 1720 1721 \item "[[ etst tx ; 1 * tO end test ]]" 1722 1723 \item "[[ etst ty ; ty * ta end test ]]" 1724 1725 \item "[[ etst ty ; ta * ty end test ]]" 1726 1727 \item "[[ etst ty ; ty * bottom end test ]]" 1728 1729 \item "[[ ttst 2 * 3 = 6 end test ]]" 1730 1731 \item "[[ ttst 2 * -3 = -6 end test ]]" 1732 1733 \item "[[ ttst -2 * 3 = -6 end test ]]" 1734 1735 \item "[[ ttst -2 * -3 = 6 end test ]]" 1736 1737 \item "[[ ttst 3 * 2 = 6 end test ]]" 1738 1739 \item "[[ ttst -3 * 2 = -6 end test ]]" 1740 1741 \item "[[ ttst 3 * -2 = -6 end test ]]" 1742 1743 \item "[[ ttst -3 * -2 = 6 end test ]]" 1744 1745 \end{statements}" ]" 1746 1747 1748 1749 \subsection{"[[ x < y ]]"} 1750 1751 "[ "\begin{statements} 1752 1753 \item "[[ etst tx ; tt < 1 end test ]]" 1754 1755 \item "[[ etst tx ; tf < 1 end test ]]" 1756 1757 \item "[[ etst tx ; ta < 1 end test ]]" 1758 1759 \item "[[ etst tx ; tb < 1 end test ]]" 1760 1761 \item "[[ etst tx ; tc < 1 end test ]]" 1762 1763 \item "[[ etst tx ; td < 1 end test ]]" 1764 1765 \item "[[ etst tx ; tx < 1 end test ]]" 1766 1767 \item "[[ etst ty ; ty < 1 end test ]]" 1768 1769 \item "[[ etst tx ; tm < 1 end test ]]" 1770 1771 \item "[[ etst tx ; to < 1 end test ]]" 1772 1773 \item "[[ etst tx ; tO < 1 end test ]]" 1774 1775 \item "[[ etst tx ; 1 < tt end test ]]" 1776 1777 \item "[[ etst tx ; 1 < tf end test ]]" 1778 1779 \item "[[ etst tx ; 1 < ta end test ]]" 1780 1781 \item "[[ etst tx ; 1 < tb end test ]]" 1782 1783 \item "[[ etst tx ; 1 < tc end test ]]" 1784 1785 \item "[[ etst tx ; 1 < td end test ]]" 1786 1787 \item "[[ etst tx ; 1 < tx end test ]]" 1788 1789 \item "[[ etst ty ; 1 < ty end test ]]" 1790 1791 \item "[[ etst tx ; 1 < tm end test ]]" 1792 1793 \item "[[ etst tx ; 1 < to end test ]]" 1794 1795 \item "[[ etst tx ; 1 < tO end test ]]" 1796 1797 \item "[[ etst ty ; ty < ta end test ]]" 1798 1799 \item "[[ etst ty ; ta < ty end test ]]" 1800 1801 \item "[[ etst ty ; ty < bottom end test ]]" 1802 1803 \item "[[ ttst 2 < 3 end test ]]" 1804 1805 \item "[[ ftst 2 < -3 end test ]]" 1806 1807 \item "[[ ttst -2 < 3 end test ]]" 1808 1809 \item "[[ ftst -2 < -3 end test ]]" 1810 1811 \item "[[ ftst 3 < 2 end test ]]" 1812 1813 \item "[[ ttst -3 < 2 end test ]]" 1814 1815 \item "[[ ftst 3 < -2 end test ]]" 1816 1817 \item "[[ ttst -3 < -2 end test ]]" 1818 1819 \item "[[ ftst 2 < 2 end test ]]" 1820 1821 \item "[[ ftst -2 < -2 end test ]]" 1822 1823 \end{statements}" ]" 1824 1825 1826 1827 \subsection{"[[ x > y ]]"} 1828 1829 "[ "\begin{statements} 1830 1831 \item "[[ etst tx ; tt > 1 end test ]]" 1832 1833 \item "[[ etst tx ; tf > 1 end test ]]" 1834 1835 \item "[[ etst tx ; ta > 1 end test ]]" 1836 1837 \item "[[ etst tx ; tb > 1 end test ]]" 1838 1839 \item "[[ etst tx ; tc > 1 end test ]]" 1840 1841 \item "[[ etst tx ; td > 1 end test ]]" 1842 1843 \item "[[ etst tx ; tx > 1 end test ]]" 1844 1845 \item "[[ etst ty ; ty > 1 end test ]]" 1846 1847 \item "[[ etst tx ; tm > 1 end test ]]" 1848 1849 \item "[[ etst tx ; to > 1 end test ]]" 1850 1851 \item "[[ etst tx ; tO > 1 end test ]]" 1852 1853 \item "[[ etst tx ; 1 > tt end test ]]" 1854 1855 \item "[[ etst tx ; 1 > tf end test ]]" 1856 1857 \item "[[ etst tx ; 1 > ta end test ]]" 1858 1859 \item "[[ etst tx ; 1 > tb end test ]]" 1860 1861 \item "[[ etst tx ; 1 > tc end test ]]" 1862 1863 \item "[[ etst tx ; 1 > td end test ]]" 1864 1865 \item "[[ etst tx ; 1 > tx end test ]]" 1866 1867 \item "[[ etst ty ; 1 > ty end test ]]" 1868 1869 \item "[[ etst tx ; 1 > tm end test ]]" 1870 1871 \item "[[ etst tx ; 1 > to end test ]]" 1872 1873 \item "[[ etst tx ; 1 > tO end test ]]" 1874 1875 \item "[[ etst ty ; ty > ta end test ]]" 1876 1877 \item "[[ etst ty ; ta > ty end test ]]" 1878 1879 \item "[[ etst ty ; ty > bottom end test ]]" 1880 1881 \item "[[ ftst 2 > 3 end test ]]" 1882 1883 \item "[[ ttst 2 > -3 end test ]]" 1884 1885 \item "[[ ftst -2 > 3 end test ]]" 1886 1887 \item "[[ ttst -2 > -3 end test ]]" 1888 1889 \item "[[ ttst 3 > 2 end test ]]" 1890 1891 \item "[[ ftst -3 > 2 end test ]]" 1892 1893 \item "[[ ttst 3 > -2 end test ]]" 1894 1895 \item "[[ ftst -3 > -2 end test ]]" 1896 1897 \item "[[ ftst 2 > 2 end test ]]" 1898 1899 \item "[[ ftst -2 > -2 end test ]]" 1900 1901 \end{statements}" ]" 1902 1903 1904 1905 \subsection{"[[ x <= y ]]"} 1906 1907 "[ "\begin{statements} 1908 1909 \item "[[ etst tx ; tt <= 1 end test ]]" 1910 1911 \item "[[ etst tx ; tf <= 1 end test ]]" 1912 1913 \item "[[ etst tx ; ta <= 1 end test ]]" 1914 1915 \item "[[ etst tx ; tb <= 1 end test ]]" 1916 1917 \item "[[ etst tx ; tc <= 1 end test ]]" 1918 1919 \item "[[ etst tx ; td <= 1 end test ]]" 1920 1921 \item "[[ etst tx ; tx <= 1 end test ]]" 1922 1923 \item "[[ etst ty ; ty <= 1 end test ]]" 1924 1925 \item "[[ etst tx ; tm <= 1 end test ]]" 1926 1927 \item "[[ etst tx ; to <= 1 end test ]]" 1928 1929 \item "[[ etst tx ; tO <= 1 end test ]]" 1930 1931 \item "[[ etst tx ; 1 <= tt end test ]]" 1932 1933 \item "[[ etst tx ; 1 <= tf end test ]]" 1934 1935 \item "[[ etst tx ; 1 <= ta end test ]]" 1936 1937 \item "[[ etst tx ; 1 <= tb end test ]]" 1938 1939 \item "[[ etst tx ; 1 <= tc end test ]]" 1940 1941 \item "[[ etst tx ; 1 <= td end test ]]" 1942 1943 \item "[[ etst tx ; 1 <= tx end test ]]" 1944 1945 \item "[[ etst ty ; 1 <= ty end test ]]" 1946 1947 \item "[[ etst tx ; 1 <= tm end test ]]" 1948 1949 \item "[[ etst tx ; 1 <= to end test ]]" 1950 1951 \item "[[ etst tx ; 1 <= tO end test ]]" 1952 1953 \item "[[ etst ty ; ty <= ta end test ]]" 1954 1955 \item "[[ etst ty ; ta <= ty end test ]]" 1956 1957 \item "[[ etst ty ; ty <= bottom end test ]]" 1958 1959 \item "[[ ttst 2 <= 3 end test ]]" 1960 1961 \item "[[ ftst 2 <= -3 end test ]]" 1962 1963 \item "[[ ttst -2 <= 3 end test ]]" 1964 1965 \item "[[ ftst -2 <= -3 end test ]]" 1966 1967 \item "[[ ftst 3 <= 2 end test ]]" 1968 1969 \item "[[ ttst -3 <= 2 end test ]]" 1970 1971 \item "[[ ftst 3 <= -2 end test ]]" 1972 1973 \item "[[ ttst -3 <= -2 end test ]]" 1974 1975 \item "[[ ttst 2 <= 2 end test ]]" 1976 1977 \item "[[ ttst -2 <= -2 end test ]]" 1978 1979 \end{statements}" ]" 1980 1981 1982 1983 \subsection{"[[ x >= y ]]"} 1984 1985 "[ "\begin{statements} 1986 1987 \item "[[ etst tx ; tt >= 1 end test ]]" 1988 1989 \item "[[ etst tx ; tf >= 1 end test ]]" 1990 1991 \item "[[ etst tx ; ta >= 1 end test ]]" 1992 1993 \item "[[ etst tx ; tb >= 1 end test ]]" 1994 1995 \item "[[ etst tx ; tc >= 1 end test ]]" 1996 1997 \item "[[ etst tx ; td >= 1 end test ]]" 1998 1999 \item "[[ etst tx ; tx >= 1 end test ]]" 2000 2001 \item "[[ etst ty ; ty >= 1 end test ]]" 2002 2003 \item "[[ etst tx ; tm >= 1 end test ]]" 2004 2005 \item "[[ etst tx ; to >= 1 end test ]]" 2006 2007 \item "[[ etst tx ; tO >= 1 end test ]]" 2008 2009 \item "[[ etst tx ; 1 >= tt end test ]]" 2010 2011 \item "[[ etst tx ; 1 >= tf end test ]]" 2012 2013 \item "[[ etst tx ; 1 >= ta end test ]]" 2014 2015 \item "[[ etst tx ; 1 >= tb end test ]]" 2016 2017 \item "[[ etst tx ; 1 >= tc end test ]]" 2018 2019 \item "[[ etst tx ; 1 >= td end test ]]" 2020 2021 \item "[[ etst tx ; 1 >= tx end test ]]" 2022 2023 \item "[[ etst ty ; 1 >= ty end test ]]" 2024 2025 \item "[[ etst tx ; 1 >= tm end test ]]" 2026 2027 \item "[[ etst tx ; 1 >= to end test ]]" 2028 2029 \item "[[ etst tx ; 1 >= tO end test ]]" 2030 2031 \item "[[ etst ty ; ty >= ta end test ]]" 2032 2033 \item "[[ etst ty ; ta >= ty end test ]]" 2034 2035 \item "[[ etst ty ; ty >= bottom end test ]]" 2036 2037 \item "[[ ftst 2 >= 3 end test ]]" 2038 2039 \item "[[ ttst 2 >= -3 end test ]]" 2040 2041 \item "[[ ftst -2 >= 3 end test ]]" 2042 2043 \item "[[ ttst -2 >= -3 end test ]]" 2044 2045 \item "[[ ttst 3 >= 2 end test ]]" 2046 2047 \item "[[ ftst -3 >= 2 end test ]]" 2048 2049 \item "[[ ttst 3 >= -2 end test ]]" 2050 2051 \item "[[ ftst -3 >= -2 end test ]]" 2052 2053 \item "[[ ttst 2 >= 2 end test ]]" 2054 2055 \item "[[ ttst -2 >= -2 end test ]]" 2056 2057 \end{statements}" ]" 2058 2059 2060 2061 \subsection{Strings} 2062 2063 "[ "\begin{statements} 2064 2065 \item "[[ ttst "abc" intp end test ]]" 2066 2067 \item "[[ ttst "abc" = %% %9 %7 + %% %2 %5 %6 * %% %9 %8 + %% %2 %5 %6 * %% %2 %5 %6 * %% %9 %9 + %% %2 %5 %6 * %% %2 %5 %6 * %% %2 %5 %6 end test ]]" 2068 2069 \item "[[ ttst "if" = %% %9 %1 %7 %5 %3 end test ]]" 2070 2071 \end{statements}" ]" 2072 2073 2074 2075 \section{Pairs} 2076 2077 \subsection{pairp} 2078 2079 "[ "\begin{statements} 2080 2081 \item "[[ ftst tt pairp end test ]]" 2082 2083 \item "[[ ftst tf pairp end test ]]" 2084 2085 \item "[[ ftst 1 pairp end test ]]" 2086 2087 \item "[[ ftst 2 pairp end test ]]" 2088 2089 \item "[[ ftst -2 pairp end test ]]" 2090 2091 \item "[[ ttst ta pairp end test ]]" 2092 2093 \item "[[ ttst tb pairp end test ]]" 2094 2095 \item "[[ ttst tc pairp end test ]]" 2096 2097 \item "[[ ttst td pairp end test ]]" 2098 2099 \item "[[ etst ty ; ty pairp end test ]]" 2100 2101 \item "[[ ftst tm pairp end test ]]" 2102 2103 \item "[[ ftst to pairp end test ]]" 2104 2105 \item "[[ ftst tO pairp end test ]]" 2106 2107 \end{statements}" ]" 2108 2109 2110 2111 \subsection{head} 2112 2113 "[ "\begin{statements} 2114 2115 \item "[[ etst tt ; tt head end test ]]" 2116 2117 \item "[[ etst tf ; tf head end test ]]" 2118 2119 \item "[[ etst 1 ; 1 head end test ]]" 2120 2121 \item "[[ etst 2 ; 2 head end test ]]" 2122 2123 \item "[[ etst -2 ; -2 head end test ]]" 2124 2125 \item "[[ ttst ta head = tt end test ]]" 2126 2127 \item "[[ ttst tb head = tt end test ]]" 2128 2129 \item "[[ ttst tc head = tf end test ]]" 2130 2131 \item "[[ ttst td head = tf end test ]]" 2132 2133 \item "[[ etst tx ; tx head end test ]]" 2134 2135 \item "[[ etst ty ; ty head end test ]]" 2136 2137 \item "[[ etst tm ; tm head end test ]]" 2138 2139 \item "[[ etst to ; to head end test ]]" 2140 2141 \item "[[ etst tO ; tO head end test ]]" 2142 2143 \item "[[ ttst ( tt :: 1 ) head = tt end test ]]" 2144 2145 \item "[[ ttst ( tf :: 1 ) head = tf end test ]]" 2146 2147 \item "[[ ttst ( ta :: 1 ) head = ta end test ]]" 2148 2149 \item "[[ ttst ( tb :: 1 ) head = tb end test ]]" 2150 2151 \item "[[ ttst ( tc :: 1 ) head = tc end test ]]" 2152 2153 \item "[[ ttst ( td :: 1 ) head = td end test ]]" 2154 2155 \item "[[ etst ty ; ( ty :: 1 ) head = tt end test ]]" 2156 2157 \item "[[ ttst ( tm :: 1 ) head = tm end test ]]" 2158 2159 \item "[[ ttst ( to :: 1 ) head = to end test ]]" 2160 2161 \item "[[ ttst ( tO :: 1 ) head = tO end test ]]" 2162 2163 \end{statements}" ]" 2164 2165 2166 2167 \subsection{tail} 2168 2169 "[ "\begin{statements} 2170 2171 \item "[[ etst tt ; tt tail end test ]]" 2172 2173 \item "[[ etst tf ; tf tail end test ]]" 2174 2175 \item "[[ etst 1 ; 1 tail end test ]]" 2176 2177 \item "[[ etst 2 ; 2 tail end test ]]" 2178 2179 \item "[[ etst -2 ; -2 tail end test ]]" 2180 2181 \item "[[ ttst ta tail = tt end test ]]" 2182 2183 \item "[[ ttst tb tail = tf end test ]]" 2184 2185 \item "[[ ttst tc tail = tt end test ]]" 2186 2187 \item "[[ ttst td tail = tf end test ]]" 2188 2189 \item "[[ etst tx ; tx tail end test ]]" 2190 2191 \item "[[ etst ty ; ty tail end test ]]" 2192 2193 \item "[[ etst tm ; tm tail end test ]]" 2194 2195 \item "[[ etst to ; to tail end test ]]" 2196 2197 \item "[[ etst tO ; tO tail end test ]]" 2198 2199 \item "[[ ttst ( 1 :: tt ) tail = tt end test ]]" 2200 2201 \item "[[ ttst ( 1 :: tf ) tail = tf end test ]]" 2202 2203 \item "[[ ttst ( 1 :: ta ) tail = ta end test ]]" 2204 2205 \item "[[ ttst ( 1 :: tb ) tail = tb end test ]]" 2206 2207 \item "[[ ttst ( 1 :: tc ) tail = tc end test ]]" 2208 2209 \item "[[ ttst ( 1 :: td ) tail = td end test ]]" 2210 2211 \item "[[ etst ty ; ( 1 :: ty ) tail = tt end test ]]" 2212 2213 \item "[[ ttst ( 1 :: tm ) tail = tm end test ]]" 2214 2215 \item "[[ ttst ( 1 :: to ) tail = to end test ]]" 2216 2217 \item "[[ ttst ( 1 :: tO ) tail = tO end test ]]" 2218 2219 \end{statements}" ]" 2220 2221 2222 2223 \subsection{List operations} 2224 2225 "[ "\begin{statements} 2226 2227 \item "[[ etst revappend ( << 1 ,, 2 ,, 3 >> , << 4 ,, 5 ,, 6 >> ) ; << 3 ,, 2 ,, 1 ,, 4 ,, 5 ,, 6 >> end test ]]" 2228 2229 \item "[[ etst reverse ( << 1 ,, 2 ,, 3 >> ) ; << 3 ,, 2 ,, 1 >> end test ]]" 2230 2231 \item "[[ etst nth ( 2 , << 1 ,, 2 ,, 3 ,, 4 >> ) ; 3 end test ]]" 2232 2233 \item "[[ etst length ( << 1 ,, 2 ,, 3 >> ) ; 3 end test ]]" 2234 2235 \item "[[ etst list-prefix ( << 1 ,, 2 ,, 3 ,, 4 >> , 2 ) ; << 1 ,, 2 >> end test ]]" 2236 2237 \item "[[ etst list-suffix ( << 1 ,, 2 ,, 3 ,, 4 >> , 2 ) ; << 3 ,, 4 >> end test ]]" 2238 2239 \end{statements}" ]" 2240 2241 2242 2243 \section{Exceptions} 2244 2245 The following tests are merged from several sources. The merged test suite contains repetitions. 2246 2247 "[ "\begin{statements} 2248 2249 \item "[[ ttst exception catch head end test ]]" 2250 2251 \item "[[ ftst true catch head end test ]]" 2252 2253 \item "[[ ftst false catch head end test ]]" 2254 2255 \item "[[ ftst %% %1 %1 %7 catch head end test ]]" 2256 2257 \item "[[ ftst 0 catch head end test ]]" 2258 2259 \item "[[ ftst ( - %% %1 %1 %7 ) catch head end test ]]" 2260 2261 \item "[[ ftst ( true :: false ) catch head end test ]]" 2262 2263 \item "[[ ftst map ( \ x . x ) catch head end test ]]" 2264 2265 2266 2267 \item "[[ ttst exception catch tail = true end test ]]" 2268 2269 \item "[[ ttst true catch tail = true end test ]]" 2270 2271 \item "[[ ttst false catch tail = false end test ]]" 2272 2273 \item "[[ ttst %% %1 %1 %7 catch tail = %% %1 %1 %7 end test ]]" 2274 2275 \item "[[ ttst 0 catch tail = 0 end test ]]" 2276 2277 \item "[[ ttst ( - %% %1 %1 %7 ) catch tail = ( - %% %1 %1 %7 ) end test ]]" 2278 2279 \item "[[ ttst ( true :: false ) catch tail = ( true :: false ) end test ]]" 2280 2281 \item "[[ ttst map ( \ x . x ) catch tail = map ( \ x . x ) end test ]]" 2282 2283 2284 2285 \item "[[ ttst exception catch = true :: true end test ]]" 2286 2287 \item "[[ ttst true catch = false :: true end test ]]" 2288 2289 \item "[[ ttst false catch = false :: false end test ]]" 2290 2291 \item "[[ ttst %% %1 %1 %7 catch = false :: %% %1 %1 %7 end test ]]" 2292 2293 \item "[[ ttst 0 catch = false :: 0 end test ]]" 2294 2295 \item "[[ ttst ( - %% %1 %1 %7 ) catch = false :: ( - %% %1 %1 %7 ) end test ]]" 2296 2297 \item "[[ ttst ( true :: false ) catch = false :: ( true :: false ) end test ]]" 2298 2299 \item "[[ ttst map ( \ x . x ) catch = false :: map ( \ x . x ) end test ]]" 2300 2301 2302 2303 \item "[[ ttst tt catch = false :: tt end test ]]" 2304 2305 \item "[[ ttst tf catch = false :: tf end test ]]" 2306 2307 \item "[[ ttst 1 catch = false :: 1 end test ]]" 2308 2309 \item "[[ ttst 2 catch = false :: 2 end test ]]" 2310 2311 \item "[[ ttst -2 catch = false :: -2 end test ]]" 2312 2313 \item "[[ ttst ta catch = false :: ta end test ]]" 2314 2315 \item "[[ ttst tb catch = false :: tb end test ]]" 2316 2317 \item "[[ ttst tc catch = false :: tc end test ]]" 2318 2319 \item "[[ ttst td catch = false :: td end test ]]" 2320 2321 \item "[[ ttst tx catch = true :: tt end test ]]" 2322 2323 \item "[[ ttst ty catch = true :: 2 end test ]]" 2324 2325 \item "[[ ttst tz catch = true :: 3 end test ]]" 2326 2327 \item "[[ ttst tm catch = false :: tm end test ]]" 2328 2329 \item "[[ ttst to catch = false :: to end test ]]" 2330 2331 \item "[[ ttst tO catch = false :: tO end test ]]" 2332 2333 \item "[[ ttst 2 raise catch = true :: 2 end test ]]" 2334 2335 \item "[[ ttst 2 raise raise catch = true :: 2 end test ]]" 2336 2337 \end{statements}" ]" 2338 2339 2340 2341 \section{Maps} 2342 2343 \subsection{mapp} 2344 2345 "[ "\begin{statements} 2346 2347 \item "[[ ftst tt mapp end test ]]" 2348 2349 \item "[[ ftst tf mapp end test ]]" 2350 2351 \item "[[ ftst 1 mapp end test ]]" 2352 2353 \item "[[ ftst 2 mapp end test ]]" 2354 2355 \item "[[ ftst -2 mapp end test ]]" 2356 2357 \item "[[ ftst ta mapp end test ]]" 2358 2359 \item "[[ ftst tb mapp end test ]]" 2360 2361 \item "[[ ftst tc mapp end test ]]" 2362 2363 \item "[[ ftst td mapp end test ]]" 2364 2365 \item "[[ etst ty ; ty mapp end test ]]" 2366 2367 \item "[[ ttst tm mapp end test ]]" 2368 2369 \item "[[ ftst to mapp end test ]]" 2370 2371 \item "[[ ftst tO mapp end test ]]" 2372 2373 \end{statements}" ]" 2374 2375 2376 2377 \subsection{map} 2378 2379 "[ "\begin{statements} 2380 2381 \item "[[ ttst map ( tt ) = tm end test ]]" 2382 2383 \item "[[ ttst map ( tf ) = tm end test ]]" 2384 2385 \item "[[ ttst map ( 1 ) = tm end test ]]" 2386 2387 \item "[[ ttst map ( 2 ) = tm end test ]]" 2388 2389 \item "[[ ttst map ( -2 ) = tm end test ]]" 2390 2391 \item "[[ ttst map ( ta ) = tm end test ]]" 2392 2393 \item "[[ ttst map ( tb ) = tm end test ]]" 2394 2395 \item "[[ ttst map ( tc ) = tm end test ]]" 2396 2397 \item "[[ ttst map ( td ) = tm end test ]]" 2398 2399 \item "[[ ttst map ( tx ) = tm end test ]]" 2400 2401 \item "[[ ttst map ( ty ) = tm end test ]]" 2402 2403 \item "[[ ttst map ( tm ) = tm end test ]]" 2404 2405 \item "[[ ttst map ( to ) = tm end test ]]" 2406 2407 \item "[[ ttst map ( tO ) = tm end test ]]" 2408 2409 \end{statements}" ]" 2410 2411 2412 2413 \subsection{catching maptag} 2414 2415 "[ "\begin{statements} 2416 2417 \item "[[ ttst tt catching maptag = tm end test ]]" 2418 2419 \item "[[ ttst tf catching maptag = tm end test ]]" 2420 2421 \item "[[ ttst 1 catching maptag = tm end test ]]" 2422 2423 \item "[[ ttst 2 catching maptag = tm end test ]]" 2424 2425 \item "[[ ttst -2 catching maptag = tm end test ]]" 2426 2427 \item "[[ ttst ta catching maptag = tm end test ]]" 2428 2429 \item "[[ ttst tb catching maptag = tm end test ]]" 2430 2431 \item "[[ ttst tc catching maptag = tm end test ]]" 2432 2433 \item "[[ ttst td catching maptag = tm end test ]]" 2434 2435 \item "[[ ttst tx catching maptag = tm end test ]]" 2436 2437 \item "[[ ttst ty catching maptag = tm end test ]]" 2438 2439 \item "[[ ttst tm catching maptag = tm end test ]]" 2440 2441 \item "[[ ttst to catching maptag = tm end test ]]" 2442 2443 \item "[[ ttst tO catching maptag = tm end test ]]" 2444 2445 \end{statements}" ]" 2446 2447 2448 2449 \subsection{maptag} 2450 2451 "[ "\begin{statements} 2452 2453 \item "[[ ttst tt maptag = tm end test ]]" 2454 2455 \item "[[ ttst tf maptag = tm end test ]]" 2456 2457 \item "[[ ttst 1 maptag = tm end test ]]" 2458 2459 \item "[[ ttst 2 maptag = tm end test ]]" 2460 2461 \item "[[ ttst -2 maptag = tm end test ]]" 2462 2463 \item "[[ ttst ta maptag = tm end test ]]" 2464 2465 \item "[[ ttst tb maptag = tm end test ]]" 2466 2467 \item "[[ ttst tc maptag = tm end test ]]" 2468 2469 \item "[[ ttst td maptag = tm end test ]]" 2470 2471 \item "[[ etst tx ; tx maptag = tm end test ]]" 2472 2473 \item "[[ etst ty ; ty maptag = tm end test ]]" 2474 2475 \item "[[ ttst tm maptag = tm end test ]]" 2476 2477 \item "[[ ttst to maptag = tm end test ]]" 2478 2479 \item "[[ ttst tO maptag = tm end test ]]" 2480 2481 \end{statements}" ]" 2482 2483 2484 2485 \subsection{untag} 2486 2487 "[ "\begin{statements} 2488 2489 \item "[[ etst tx ; tt untag end test ]]" 2490 2491 \item "[[ etst tx ; tf untag end test ]]" 2492 2493 \item "[[ etst tx ; 1 untag end test ]]" 2494 2495 \item "[[ etst tx ; 2 untag end test ]]" 2496 2497 \item "[[ etst tx ; -2 untag end test ]]" 2498 2499 \item "[[ etst tx ; ta untag end test ]]" 2500 2501 \item "[[ etst tx ; tb untag end test ]]" 2502 2503 \item "[[ etst tx ; tc untag end test ]]" 2504 2505 \item "[[ etst tx ; td untag end test ]]" 2506 2507 \item "[[ etst tx ; tx untag end test ]]" 2508 2509 \item "[[ etst ty ; ty untag end test ]]" 2510 2511 \item "[[ ttst tm untag = tf end test ]]" 2512 2513 \item "[[ etst tx ; to untag end test ]]" 2514 2515 \item "[[ etst tx ; tO untag end test ]]" 2516 2517 \end{statements}" ]" 2518 2519 2520 2521 \subsection{map+untag} 2522 2523 "[ "\begin{statements} 2524 2525 \item "[[ ttst map ( tt ) untag = tt end test ]]" 2526 2527 \item "[[ ttst map ( tf ) untag = tf end test ]]" 2528 2529 \item "[[ ttst map ( 1 ) untag = 1 end test ]]" 2530 2531 \item "[[ ttst map ( 2 ) untag = 2 end test ]]" 2532 2533 \item "[[ ttst map ( -2 ) untag = -2 end test ]]" 2534 2535 \item "[[ ttst map ( ta ) untag = ta end test ]]" 2536 2537 \item "[[ ttst map ( tb ) untag = tb end test ]]" 2538 2539 \item "[[ ttst map ( tc ) untag = tc end test ]]" 2540 2541 \item "[[ ttst map ( td ) untag = td end test ]]" 2542 2543 \item "[[ etst tx ; map ( tx ) untag = tt end test ]]" 2544 2545 \item "[[ etst ty ; map ( ty ) untag = tt end test ]]" 2546 2547 \item "[[ ttst map ( tm ) untag = tm end test ]]" 2548 2549 \item "[[ ttst map ( to ) untag = to end test ]]" 2550 2551 \item "[[ ttst map ( tO ) untag = tO end test ]]" 2552 2553 \end{statements}" ]" 2554 2555 2556 2557 \subsection{catching maptag+untag} 2558 2559 "[ "\begin{statements} 2560 2561 \item "[[ ttst tt catching maptag untag = tt end test ]]" 2562 2563 \item "[[ ttst tf catching maptag untag = tf end test ]]" 2564 2565 \item "[[ ttst 1 catching maptag untag = 1 end test ]]" 2566 2567 \item "[[ ttst 2 catching maptag untag = 2 end test ]]" 2568 2569 \item "[[ ttst -2 catching maptag untag = -2 end test ]]" 2570 2571 \item "[[ ttst ta catching maptag untag = ta end test ]]" 2572 2573 \item "[[ ttst tb catching maptag untag = tb end test ]]" 2574 2575 \item "[[ ttst tc catching maptag untag = tc end test ]]" 2576 2577 \item "[[ ttst td catching maptag untag = td end test ]]" 2578 2579 \item "[[ etst tx ; tx catching maptag untag = tt end test ]]" 2580 2581 \item "[[ etst ty ; ty catching maptag untag = tt end test ]]" 2582 2583 \item "[[ ttst tm catching maptag untag = tm end test ]]" 2584 2585 \item "[[ ttst to catching maptag untag = to end test ]]" 2586 2587 \item "[[ ttst tO catching maptag untag = tO end test ]]" 2588 2589 \end{statements}" ]" 2590 2591 2592 2593 \subsection{maptag+untag} 2594 2595 "[ "\begin{statements} 2596 2597 \item "[[ ttst tt maptag untag = tt end test ]]" 2598 2599 \item "[[ ttst tf maptag untag = tf end test ]]" 2600 2601 \item "[[ ttst 1 maptag untag = 1 end test ]]" 2602 2603 \item "[[ ttst 2 maptag untag = 2 end test ]]" 2604 2605 \item "[[ ttst -2 maptag untag = -2 end test ]]" 2606 2607 \item "[[ ttst ta maptag untag = ta end test ]]" 2608 2609 \item "[[ ttst tb maptag untag = tb end test ]]" 2610 2611 \item "[[ ttst tc maptag untag = tc end test ]]" 2612 2613 \item "[[ ttst td maptag untag = td end test ]]" 2614 2615 \item "[[ etst tx ; tx maptag untag = tt end test ]]" 2616 2617 \item "[[ etst ty ; ty maptag untag = tt end test ]]" 2618 2619 \item "[[ ttst tm maptag untag = tm end test ]]" 2620 2621 \item "[[ ttst to maptag untag = to end test ]]" 2622 2623 \item "[[ ttst tO maptag untag = tO end test ]]" 2624 2625 \end{statements}" ]" 2626 2627 2628 2629 \subsection{root} 2630 2631 "[ "\begin{statements} 2632 2633 \item "[[ etst tx ; tt root end test ]]" 2634 2635 \item "[[ etst tx ; tf root end test ]]" 2636 2637 \item "[[ etst tx ; 1 root end test ]]" 2638 2639 \item "[[ etst tx ; 2 root end test ]]" 2640 2641 \item "[[ etst tx ; -2 root end test ]]" 2642 2643 \item "[[ etst tx ; ta root end test ]]" 2644 2645 \item "[[ etst tx ; tb root end test ]]" 2646 2647 \item "[[ etst tx ; tc root end test ]]" 2648 2649 \item "[[ etst tx ; td root end test ]]" 2650 2651 \item "[[ etst tx ; tx root end test ]]" 2652 2653 \item "[[ etst ty ; ty root end test ]]" 2654 2655 \item "[[ ftst tm root end test ]]" 2656 2657 \item "[[ etst tx ; to root end test ]]" 2658 2659 \item "[[ etst tx ; tO root end test ]]" 2660 2661 \end{statements}" ]" 2662 2663 2664 2665 \subsection{map+root} 2666 2667 "[ "\begin{statements} 2668 2669 \item "[[ ttst map ( tt ) root end test ]]" 2670 2671 \item "[[ ftst map ( tf ) root end test ]]" 2672 2673 \item "[[ ftst map ( 1 ) root end test ]]" 2674 2675 \item "[[ ftst map ( 2 ) root end test ]]" 2676 2677 \item "[[ ftst map ( -2 ) root end test ]]" 2678 2679 \item "[[ ftst map ( ta ) root end test ]]" 2680 2681 \item "[[ ftst map ( tb ) root end test ]]" 2682 2683 \item "[[ ftst map ( tc ) root end test ]]" 2684 2685 \item "[[ ftst map ( td ) root end test ]]" 2686 2687 \item "[[ ftst map ( tx ) root end test ]]" 2688 2689 \item "[[ ftst map ( ty ) root end test ]]" 2690 2691 \item "[[ ftst map ( tm ) root end test ]]" 2692 2693 \item "[[ ftst map ( to ) root end test ]]" 2694 2695 \item "[[ ftst map ( tO ) root end test ]]" 2696 2697 \end{statements}" ]" 2698 2699 2700 2701 \subsection{maptag+root} 2702 2703 "[ "\begin{statements} 2704 2705 \item "[[ ttst tt maptag root end test ]]" 2706 2707 \item "[[ ftst tf maptag root end test ]]" 2708 2709 \item "[[ ftst 1 maptag root end test ]]" 2710 2711 \item "[[ ftst 2 maptag root end test ]]" 2712 2713 \item "[[ ftst -2 maptag root end test ]]" 2714 2715 \item "[[ ftst ta maptag root end test ]]" 2716 2717 \item "[[ ftst tb maptag root end test ]]" 2718 2719 \item "[[ ftst tc maptag root end test ]]" 2720 2721 \item "[[ ftst td maptag root end test ]]" 2722 2723 \item "[[ etst tx ; tx maptag root end test ]]" 2724 2725 \item "[[ etst ty ; ty maptag root end test ]]" 2726 2727 \item "[[ ftst tm maptag root end test ]]" 2728 2729 \item "[[ ftst to maptag root end test ]]" 2730 2731 \item "[[ ftst tO maptag root end test ]]" 2732 2733 \end{statements}" ]" 2734 2735 2736 2737 \subsection{apply} 2738 2739 "[ "\begin{statements} 2740 2741 \item "[[ ttst ( map ( \ x . x ) apply map ( tt ) ) root end test ]]" 2742 2743 \item "[[ ftst ( map ( \ x . x ) apply map ( tf ) ) root end test ]]" 2744 2745 2746 \item "[[ ttst ( map ( \ x . \ y . x ) apply map ( tt ) apply map ( tt ) ) root end test ]]" 2747 2748 \item "[[ ttst ( map ( \ x . \ y . x ) apply map ( tt ) apply map ( tf ) ) root end test ]]" 2749 2750 \item "[[ ftst ( map ( \ x . \ y . x ) apply map ( tf ) apply map ( tt ) ) root end test ]]" 2751 2752 \item "[[ ftst ( map ( \ x . \ y . x ) apply map ( tf ) apply map ( tf ) ) root end test ]]" 2753 2754 \item "[[ ttst ( map ( \ x . \ y . y ) apply map ( tt ) apply map ( tt ) ) root end test ]]" 2755 2756 \item "[[ ftst ( map ( \ x . \ y . y ) apply map ( tt ) apply map ( tf ) ) root end test ]]" 2757 2758 \item "[[ ttst ( map ( \ x . \ y . y ) apply map ( tf ) apply map ( tt ) ) root end test ]]" 2759 2760 \item "[[ ftst ( map ( \ x . \ y . y ) apply map ( tf ) apply map ( tf ) ) root end test ]]" 2761 2762 \item "[[ ttst ( 2763 map ( \ f . \ x . f ' ( f ' x ) ) apply 2764 map ( \ f . \ x . f ' ( f ' x ) ) apply 2765 map ( \ x . x + 1 ) apply 2766 map ( 2 ) ) untag = 6 end test ]]" 2767 2768 \end{statements}" ]" 2769 2770 2771 2772 \section{Logical operations on integers} 2773 2774 \subsection{half} 2775 2776 "[ "\begin{statements} 2777 2778 \item "[[ etst tx ; half ( tt ) end test ]]" 2779 2780 \item "[[ etst ty ; half ( ty ) end test ]]" 2781 2782 \item "[[ ttst 0 = half ( 0 ) end test ]]" 2783 2784 \item "[[ ttst 0 = half ( 1 ) end test ]]" 2785 2786 \item "[[ ttst 1 = half ( 2 ) end test ]]" 2787 2788 \item "[[ ttst 1 = half ( 3 ) end test ]]" 2789 2790 \item "[[ ttst 2 = half ( 4 ) end test ]]" 2791 2792 \item "[[ ttst 2 = half ( 5 ) end test ]]" 2793 2794 \item "[[ ttst 3 = half ( 6 ) end test ]]" 2795 2796 \item "[[ ttst 3 = half ( 7 ) end test ]]" 2797 2798 \item "[[ ttst 4 = half ( 8 ) end test ]]" 2799 2800 \item "[[ ttst 4 = half ( 9 ) end test ]]" 2801 2802 \item "[[ ttst 5 = half ( 10 ) end test ]]" 2803 2804 \item "[[ ttst -1 = half ( -1 ) end test ]]" 2805 2806 \item "[[ ttst -1 = half ( -2 ) end test ]]" 2807 2808 \item "[[ ttst -2 = half ( -3 ) end test ]]" 2809 2810 \item "[[ ttst -2 = half ( -4 ) end test ]]" 2811 2812 \item "[[ ttst -3 = half ( -5 ) end test ]]" 2813 2814 \item "[[ ttst -3 = half ( -6 ) end test ]]" 2815 2816 \item "[[ ttst -4 = half ( -7 ) end test ]]" 2817 2818 \item "[[ ttst -4 = half ( -8 ) end test ]]" 2819 2820 \item "[[ ttst -5 = half ( -9 ) end test ]]" 2821 2822 \item "[[ ttst -5 = half ( - 10 ) end test ]]" 2823 2824 \item "[[ etst tx ; half ( ta ) end test ]]" 2825 2826 \item "[[ etst tx ; half ( tb ) end test ]]" 2827 2828 \item "[[ etst tx ; half ( tc ) end test ]]" 2829 2830 \item "[[ etst tx ; half ( td ) end test ]]" 2831 2832 \item "[[ etst tx ; half ( tx ) end test ]]" 2833 2834 \item "[[ etst ty ; half ( ty ) end test ]]" 2835 2836 \item "[[ etst tx ; half ( tm ) end test ]]" 2837 2838 \item "[[ etst tx ; half ( to ) end test ]]" 2839 2840 \item "[[ etst tx ; half ( tO ) end test ]]" 2841 2842 \end{statements}" ]" 2843 2844 2845 2846 \subsection{evenp} 2847 2848 "[ "\begin{statements} 2849 2850 \item "[[ etst tx ; evenp ( tt ) end test ]]" 2851 2852 \item "[[ etst ty ; evenp ( ty ) end test ]]" 2853 2854 \item "[[ ttst evenp ( 0 ) end test ]]" 2855 2856 \item "[[ ftst evenp ( 1 ) end test ]]" 2857 2858 \item "[[ ttst evenp ( 2 ) end test ]]" 2859 2860 \item "[[ ftst evenp ( 3 ) end test ]]" 2861 2862 \item "[[ ttst evenp ( 4 ) end test ]]" 2863 2864 \item "[[ ftst evenp ( 5 ) end test ]]" 2865 2866 \item "[[ ttst evenp ( 6 ) end test ]]" 2867 2868 \item "[[ ftst evenp ( 7 ) end test ]]" 2869 2870 \item "[[ ttst evenp ( 8 ) end test ]]" 2871 2872 \item "[[ ftst evenp ( 9 ) end test ]]" 2873 2874 \item "[[ ttst evenp ( 10 ) end test ]]" 2875 2876 \item "[[ ftst evenp ( -1 ) end test ]]" 2877 2878 \item "[[ ttst evenp ( -2 ) end test ]]" 2879 2880 \item "[[ ftst evenp ( -3 ) end test ]]" 2881 2882 \item "[[ ttst evenp ( -4 ) end test ]]" 2883 2884 \item "[[ ftst evenp ( -5 ) end test ]]" 2885 2886 \item "[[ ttst evenp ( -6 ) end test ]]" 2887 2888 \item "[[ ftst evenp ( -7 ) end test ]]" 2889 2890 \item "[[ ttst evenp ( -8 ) end test ]]" 2891 2892 \item "[[ ftst evenp ( -9 ) end test ]]" 2893 2894 \item "[[ ttst evenp ( - 10 ) end test ]]" 2895 2896 \item "[[ etst tx ; evenp ( ta ) end test ]]" 2897 2898 \item "[[ etst tx ; evenp ( tb ) end test ]]" 2899 2900 \item "[[ etst tx ; evenp ( tc ) end test ]]" 2901 2902 \item "[[ etst tx ; evenp ( td ) end test ]]" 2903 2904 \item "[[ etst tx ; evenp ( tx ) end test ]]" 2905 2906 \item "[[ etst ty ; evenp ( ty ) end test ]]" 2907 2908 \item "[[ etst tx ; evenp ( tm ) end test ]]" 2909 2910 \item "[[ etst tx ; evenp ( to ) end test ]]" 2911 2912 \item "[[ etst tx ; evenp ( tO ) end test ]]" 2913 2914 \end{statements}" ]" 2915 2916 2917 2918 \subsection{small} 2919 2920 "[ "\begin{statements} 2921 2922 \item "[[ etst tx ; small ( tt ) end test ]]" 2923 2924 \item "[[ etst tx ; small ( tf ) end test ]]" 2925 2926 \item "[[ ttst small ( 0 ) end test ]]" 2927 2928 \item "[[ ftst small ( 1 ) end test ]]" 2929 2930 \item "[[ ftst small ( 2 ) end test ]]" 2931 2932 \item "[[ ftst small ( 3 ) end test ]]" 2933 2934 \item "[[ ftst small ( 4 ) end test ]]" 2935 2936 \item "[[ ftst small ( 5 ) end test ]]" 2937 2938 \item "[[ ftst small ( 6 ) end test ]]" 2939 2940 \item "[[ ftst small ( 7 ) end test ]]" 2941 2942 \item "[[ ftst small ( 8 ) end test ]]" 2943 2944 \item "[[ ftst small ( 9 ) end test ]]" 2945 2946 \item "[[ ftst small ( 10 ) end test ]]" 2947 2948 \item "[[ ttst small ( -1 ) end test ]]" 2949 2950 \item "[[ ftst small ( -2 ) end test ]]" 2951 2952 \item "[[ ftst small ( -3 ) end test ]]" 2953 2954 \item "[[ ftst small ( -4 ) end test ]]" 2955 2956 \item "[[ ftst small ( -5 ) end test ]]" 2957 2958 \item "[[ ftst small ( -6 ) end test ]]" 2959 2960 \item "[[ ftst small ( -7 ) end test ]]" 2961 2962 \item "[[ ftst small ( -8 ) end test ]]" 2963 2964 \item "[[ ftst small ( -9 ) end test ]]" 2965 2966 \item "[[ ftst small ( - 10 ) end test ]]" 2967 2968 \item "[[ etst tx ; small ( ta ) end test ]]" 2969 2970 \item "[[ etst tx ; small ( tb ) end test ]]" 2971 2972 \item "[[ etst tx ; small ( tc ) end test ]]" 2973 2974 \item "[[ etst tx ; small ( td ) end test ]]" 2975 2976 \item "[[ etst tx ; small ( tx ) end test ]]" 2977 2978 \item "[[ etst ty ; small ( ty ) end test ]]" 2979 2980 \item "[[ etst tx ; small ( tm ) end test ]]" 2981 2982 \item "[[ etst tx ; small ( to ) end test ]]" 2983 2984 \item "[[ etst tx ; small ( tO ) end test ]]" 2985 2986 \end{statements}" ]" 2987 2988 2989 2990 \subsection{oddp} 2991 2992 "[ "\begin{statements} 2993 2994 \item "[[ etst tx ; oddp ( tt ) end test ]]" 2995 2996 \item "[[ etst ty ; oddp ( ty ) end test ]]" 2997 2998 \item "[[ ftst oddp ( 6 ) end test ]]" 2999 3000 \item "[[ ftst oddp ( -6 ) end test ]]" 3001 3002 \item "[[ ttst oddp ( 7 ) end test ]]" 3003 3004 \item "[[ ttst oddp ( -7 ) end test ]]" 3005 3006 \end{statements}" ]" 3007 3008 3009 3010 \subsection{double} 3011 3012 "[ "\begin{statements} 3013 3014 \item "[[ etst tx ; double ( 1 , 2 ) end test ]]" 3015 3016 \item "[[ etst tx ; double ( tt , tt ) end test ]]" 3017 3018 \item "[[ etst ty ; double ( ty , bottom ) end test ]]" 3019 3020 \item "[[ ttst 4 = double ( tf , 2 ) end test ]]" 3021 3022 \item "[[ ttst 5 = double ( tt , 2 ) end test ]]" 3023 3024 \item "[[ ttst -4 = double ( tf , -2 ) end test ]]" 3025 3026 \item "[[ ttst -3 = double ( tt , -2 ) end test ]]" 3027 3028 \end{statements}" ]" 3029 3030 3031 3032 \subsection{lognot} 3033 3034 "[ "\begin{statements} 3035 3036 \item "[[ etst tx ; lognot ( tt ) end test ]]" 3037 3038 \item "[[ etst ty ; lognot ( ty ) end test ]]" 3039 3040 \item "[[ ttst 1 = lognot ( -2 ) end test ]]" 3041 3042 \item "[[ ttst 0 = lognot ( -1 ) end test ]]" 3043 3044 \item "[[ ttst -1 = lognot ( 0 ) end test ]]" 3045 3046 \item "[[ ttst -2 = lognot ( 1 ) end test ]]" 3047 3048 \end{statements}" ]" 3049 3050 3051 3052 \subsection{logior} 3053 3054 "[ "\begin{statements} 3055 3056 \item "[[ etst tx ; logior ( tt , 2 ) end test ]]" 3057 3058 \item "[[ etst tx ; logior ( 1 , tt ) end test ]]" 3059 3060 \item "[[ etst ty ; logior ( ty , tz ) end test ]]" 3061 3062 \item "[[ etst ty ; logior ( ty , bottom ) end test ]]" 3063 3064 \item "[[ ttst 5 = logior ( 0 , 5 ) end test ]]" 3065 3066 \item "[[ ttst 5 = logior ( 0 , 5 ) end test ]]" 3067 3068 \item "[[ ttst 5 = logior ( 5 , 0 ) end test ]]" 3069 3070 \item "[[ ttst -1 = logior ( -1 , 5 ) end test ]]" 3071 3072 \item "[[ ttst -1 = logior ( 5 , -1 ) end test ]]" 3073 3074 \item "[[ ttst 14 = logior ( 10 , 12 ) end test ]]" 3075 3076 \end{statements}" ]" 3077 3078 3079 3080 \subsection{logxor} 3081 3082 "[ "\begin{statements} 3083 3084 \item "[[ etst tx ; logxor ( tt , 2 ) end test ]]" 3085 3086 \item "[[ etst tx ; logxor ( 1 , tt ) end test ]]" 3087 3088 \item "[[ etst ty ; logxor ( ty , bottom ) end test ]]" 3089 3090 \item "[[ ttst 5 = logxor ( 0 , 5 ) end test ]]" 3091 3092 \item "[[ ttst 5 = logxor ( 5 , 0 ) end test ]]" 3093 3094 \item "[[ ttst -6 = logxor ( -1 , 5 ) end test ]]" 3095 3096 \item "[[ ttst -6 = logxor ( 5 , -1 ) end test ]]" 3097 3098 \item "[[ ttst 6 = logxor ( 10 , 12 ) end test ]]" 3099 3100 \end{statements}" ]" 3101 3102 3103 3104 \subsection{logand} 3105 3106 "[ "\begin{statements} 3107 3108 \item "[[ etst tx ; logand ( tt , 2 ) end test ]]" 3109 3110 \item "[[ etst tx ; logand ( 1 , tt ) end test ]]" 3111 3112 \item "[[ etst ty ; logand ( ty , bottom ) end test ]]" 3113 3114 \item "[[ ttst 0 = logand ( 0 , 5 ) end test ]]" 3115 3116 \item "[[ ttst 0 = logand ( 5 , 0 ) end test ]]" 3117 3118 \item "[[ ttst 5 = logand ( -1 , 5 ) end test ]]" 3119 3120 \item "[[ ttst 5 = logand ( 5 , -1 ) end test ]]" 3121 3122 \item "[[ ttst 8 = logand ( 10 , 12 ) end test ]]" 3123 3124 \end{statements}" ]" 3125 3126 3127 3128 \subsection{logeqv} 3129 3130 "[ "\begin{statements} 3131 3132 \item "[[ etst tx ; logeqv ( tt , 2 ) end test ]]" 3133 3134 \item "[[ etst tx ; logeqv ( 1 , tt ) end test ]]" 3135 3136 \item "[[ etst ty ; logeqv ( ty , bottom ) end test ]]" 3137 3138 \item "[[ ttst -6 = logeqv ( 0 , 5 ) end test ]]" 3139 3140 \item "[[ ttst -6 = logeqv ( 5 , 0 ) end test ]]" 3141 3142 \item "[[ ttst 5 = logeqv ( -1 , 5 ) end test ]]" 3143 3144 \item "[[ ttst 5 = logeqv ( 5 , -1 ) end test ]]" 3145 3146 \item "[[ ttst -7 = logeqv ( 10 , 12 ) end test ]]" 3147 3148 \end{statements}" ]" 3149 3150 3151 3152 \subsection{lognand} 3153 3154 "[ "\begin{statements} 3155 3156 \item "[[ etst tx ; lognand ( tt , 2 ) end test ]]" 3157 3158 \item "[[ etst tx ; lognand ( 1 , tt ) end test ]]" 3159 3160 \item "[[ etst ty ; lognand ( ty , bottom ) end test ]]" 3161 3162 \item "[[ ttst -1 = lognand ( 0 , 5 ) end test ]]" 3163 3164 \item "[[ ttst -1 = lognand ( 5 , 0 ) end test ]]" 3165 3166 \item "[[ ttst -6 = lognand ( -1 , 5 ) end test ]]" 3167 3168 \item "[[ ttst -6 = lognand ( 5 , -1 ) end test ]]" 3169 3170 \item "[[ ttst -9 = lognand ( 10 , 12 ) end test ]]" 3171 3172 \end{statements}" ]" 3173 3174 3175 3176 \subsection{lognor} 3177 3178 "[ "\begin{statements} 3179 3180 \item "[[ etst tx ; lognor ( tt , 2 ) end test ]]" 3181 3182 \item "[[ etst tx ; lognor ( 1 , tt ) end test ]]" 3183 3184 \item "[[ etst ty ; lognor ( ty , bottom ) end test ]]" 3185 3186 \item "[[ ttst -6 = lognor ( 0 , 5 ) end test ]]" 3187 3188 \item "[[ ttst -6 = lognor ( 5 , 0 ) end test ]]" 3189 3190 \item "[[ ttst 0 = lognor ( -1 , 5 ) end test ]]" 3191 3192 \item "[[ ttst 0 = lognor ( 5 , -1 ) end test ]]" 3193 3194 \item "[[ ttst -15 = lognor ( 10 , 12 ) end test ]]" 3195 3196 \end{statements}" ]" 3197 3198 3199 3200 \subsection{logandc1} 3201 3202 "[ "\begin{statements} 3203 3204 \item "[[ etst tx ; logandc1 ( tt , 2 ) end test ]]" 3205 3206 \item "[[ etst tx ; logandc1 ( 1 , tt ) end test ]]" 3207 3208 \item "[[ etst ty ; logandc1 ( ty , bottom ) end test ]]" 3209 3210 \item "[[ ttst 5 = logandc1 ( 0 , 5 ) end test ]]" 3211 3212 \item "[[ ttst 0 = logandc1 ( 5 , 0 ) end test ]]" 3213 3214 \item "[[ ttst 0 = logandc1 ( -1 , 5 ) end test ]]" 3215 3216 \item "[[ ttst -6 = logandc1 ( 5 , -1 ) end test ]]" 3217 3218 \item "[[ ttst 4 = logandc1 ( 10 , 12 ) end test ]]" 3219 3220 \end{statements}" ]" 3221 3222 3223 3224 \subsection{logandc2} 3225 3226 "[ "\begin{statements} 3227 3228 \item "[[ etst tx ; logandc2 ( tt , 2 ) end test ]]" 3229 3230 \item "[[ etst tx ; logandc2 ( 1 , tt ) end test ]]" 3231 3232 \item "[[ etst ty ; logandc2 ( ty , bottom ) end test ]]" 3233 3234 \item "[[ ttst 0 = logandc2 ( 0 , 5 ) end test ]]" 3235 3236 \item "[[ ttst 5 = logandc2 ( 5 , 0 ) end test ]]" 3237 3238 \item "[[ ttst -6 = logandc2 ( -1 , 5 ) end test ]]" 3239 3240 \item "[[ ttst 0 = logandc2 ( 5 , -1 ) end test ]]" 3241 3242 \item "[[ ttst 2 = logandc2 ( 10 , 12 ) end test ]]" 3243 3244 \end{statements}" ]" 3245 3246 3247 3248 \subsection{logorc1} 3249 3250 "[ "\begin{statements} 3251 3252 \item "[[ etst tx ; logorc1 ( tt , 2 ) end test ]]" 3253 3254 \item "[[ etst tx ; logorc1 ( 1 , tt ) end test ]]" 3255 3256 \item "[[ etst ty ; logorc1 ( ty , bottom ) end test ]]" 3257 3258 \item "[[ ttst -1 = logorc1 ( 0 , 5 ) end test ]]" 3259 3260 \item "[[ ttst -6 = logorc1 ( 5 , 0 ) end test ]]" 3261 3262 \item "[[ ttst 5 = logorc1 ( -1 , 5 ) end test ]]" 3263 3264 \item "[[ ttst -1 = logorc1 ( 5 , -1 ) end test ]]" 3265 3266 \item "[[ ttst -3 = logorc1 ( 10 , 12 ) end test ]]" 3267 3268 \end{statements}" ]" 3269 3270 3271 3272 \subsection{logorc2} 3273 3274 "[ "\begin{statements} 3275 3276 \item "[[ etst tx ; logorc2 ( tt , 2 ) end test ]]" 3277 3278 \item "[[ etst tx ; logorc2 ( 1 , tt ) end test ]]" 3279 3280 \item "[[ etst ty ; logorc2 ( ty , bottom ) end test ]]" 3281 3282 \item "[[ ttst -6 = logorc2 ( 0 , 5 ) end test ]]" 3283 3284 \item "[[ ttst -1 = logorc2 ( 5 , 0 ) end test ]]" 3285 3286 \item "[[ ttst -1 = logorc2 ( -1 , 5 ) end test ]]" 3287 3288 \item "[[ ttst 5 = logorc2 ( 5 , -1 ) end test ]]" 3289 3290 \item "[[ ttst -5 = logorc2 ( 10 , 12 ) end test ]]" 3291 3292 \end{statements}" ]" 3293 3294 3295 3296 \subsection{logtest} 3297 3298 "[ "\begin{statements} 3299 3300 \item "[[ etst tx ; logtest ( tt , 2 ) end test ]]" 3301 3302 \item "[[ etst tx ; logtest ( 1 , tt ) end test ]]" 3303 3304 \item "[[ etst ty ; logtest ( ty , bottom ) end test ]]" 3305 3306 \item "[[ ftst logtest ( 5 , 10 ) end test ]]" 3307 3308 \item "[[ ftst logtest ( 5 , 0 ) end test ]]" 3309 3310 \item "[[ ttst logtest ( 5 , 1 ) end test ]]" 3311 3312 \item "[[ ftst logtest ( 5 , 2 ) end test ]]" 3313 3314 \item "[[ ttst logtest ( 5 , 4 ) end test ]]" 3315 3316 \item "[[ ftst logtest ( 5 , 8 ) end test ]]" 3317 3318 \item "[[ ftst logtest ( 5 , 16 ) end test ]]" 3319 3320 \item "[[ ftst logtest ( -11 , 10 ) end test ]]" 3321 3322 \item "[[ ftst logtest ( -11 , 0 ) end test ]]" 3323 3324 \item "[[ ttst logtest ( -11 , 1 ) end test ]]" 3325 3326 \item "[[ ftst logtest ( -11 , 2 ) end test ]]" 3327 3328 \item "[[ ttst logtest ( -11 , 4 ) end test ]]" 3329 3330 \item "[[ ftst logtest ( -11 , 8 ) end test ]]" 3331 3332 \item "[[ ttst logtest ( -11 , 16 ) end test ]]" 3333 3334 \end{statements}" ]" 3335 3336 3337 3338 \subsection{ash} 3339 3340 "[ "\begin{statements} 3341 3342 \item "[[ etst tx ; ash ( tt , 2 ) end test ]]" 3343 3344 \item "[[ etst tx ; ash ( 1 , tt ) end test ]]" 3345 3346 \item "[[ etst ty ; ash ( ty , bottom ) end test ]]" 3347 3348 \item "[[ ttst 3 = ash ( 3 , 0 ) end test ]]" 3349 3350 \item "[[ ttst 6 = ash ( 3 , 1 ) end test ]]" 3351 3352 \item "[[ ttst 12 = ash ( 3 , 2 ) end test ]]" 3353 3354 \item "[[ ttst 13 = ash ( 13 , 0 ) end test ]]" 3355 3356 \item "[[ ttst 6 = ash ( 13 , -1 ) end test ]]" 3357 3358 \item "[[ ttst 3 = ash ( 13 , -2 ) end test ]]" 3359 3360 \item "[[ ttst 1 = ash ( 13 , -3 ) end test ]]" 3361 3362 \item "[[ ttst 0 = ash ( 13 , -4 ) end test ]]" 3363 3364 \item "[[ ttst 0 = ash ( 13 , -5 ) end test ]]" 3365 3366 \item "[[ ttst -3 = ash ( -3 , 0 ) end test ]]" 3367 3368 \item "[[ ttst -6 = ash ( -3 , 1 ) end test ]]" 3369 3370 \item "[[ ttst -12 = ash ( -3 , 2 ) end test ]]" 3371 3372 \item "[[ ttst -6 = ash ( -6 , 0 ) end test ]]" 3373 3374 \item "[[ ttst -3 = ash ( -6 , -1 ) end test ]]" 3375 3376 \item "[[ ttst -2 = ash ( -6 , -2 ) end test ]]" 3377 3378 \item "[[ ttst -1 = ash ( -6 , -3 ) end test ]]" 3379 3380 \item "[[ ttst -1 = ash ( -6 , -4 ) end test ]]" 3381 3382 \end{statements}" ]" 3383 3384 3385 3386 \subsection{logbitp} 3387 3388 "[ "\begin{statements} 3389 3390 \item "[[ etst tx ; logbitp ( tt , 2 ) end test ]]" 3391 3392 \item "[[ etst tx ; logbitp ( 1 , tt ) end test ]]" 3393 3394 \item "[[ etst ty ; logbitp ( ty , bottom ) end test ]]" 3395 3396 \item "[[ ttst logbitp ( 0 , 13 ) end test ]]" 3397 3398 \item "[[ ftst logbitp ( 1 , 13 ) end test ]]" 3399 3400 \item "[[ ttst logbitp ( 2 , 13 ) end test ]]" 3401 3402 \item "[[ ttst logbitp ( 3 , 13 ) end test ]]" 3403 3404 \item "[[ ftst logbitp ( 4 , 13 ) end test ]]" 3405 3406 \item "[[ ftst logbitp ( 5 , 13 ) end test ]]" 3407 3408 \item "[[ ftst logbitp ( 6 , 13 ) end test ]]" 3409 3410 \item "[[ ftst logbitp ( 0 , -6 ) end test ]]" 3411 3412 \item "[[ ttst logbitp ( 1 , -6 ) end test ]]" 3413 3414 \item "[[ ftst logbitp ( 2 , -6 ) end test ]]" 3415 3416 \item "[[ ttst logbitp ( 3 , -6 ) end test ]]" 3417 3418 \item "[[ ttst logbitp ( 4 , -6 ) end test ]]" 3419 3420 \item "[[ ttst logbitp ( 5 , -6 ) end test ]]" 3421 3422 \item "[[ ttst logbitp ( 6 , -6 ) end test ]]" 3423 3424 \end{statements}" ]" 3425 3426 3427 3428 \subsection{logcount} 3429 3430 "[ "\begin{statements} 3431 3432 \item "[[ etst tx ; logcount ( tt ) end test ]]" 3433 3434 \item "[[ etst ty ; logcount ( ty ) end test ]]" 3435 3436 \item "[[ ttst 0 = logcount ( 0 ) end test ]]" 3437 3438 \item "[[ ttst 1 = logcount ( 1 ) end test ]]" 3439 3440 \item "[[ ttst 1 = logcount ( 2 ) end test ]]" 3441 3442 \item "[[ ttst 2 = logcount ( 3 ) end test ]]" 3443 3444 \item "[[ ttst 1 = logcount ( 4 ) end test ]]" 3445 3446 \item "[[ ttst 2 = logcount ( 5 ) end test ]]" 3447 3448 \item "[[ ttst 2 = logcount ( 6 ) end test ]]" 3449 3450 \item "[[ ttst 3 = logcount ( 7 ) end test ]]" 3451 3452 \item "[[ ttst 1 = logcount ( 8 ) end test ]]" 3453 3454 \item "[[ ttst 2 = logcount ( 9 ) end test ]]" 3455 3456 \item "[[ ttst 0 = logcount ( -1 ) end test ]]" 3457 3458 \item "[[ ttst 1 = logcount ( -2 ) end test ]]" 3459 3460 \item "[[ ttst 1 = logcount ( -3 ) end test ]]" 3461 3462 \item "[[ ttst 2 = logcount ( -4 ) end test ]]" 3463 3464 \item "[[ ttst 1 = logcount ( -5 ) end test ]]" 3465 3466 \item "[[ ttst 2 = logcount ( -6 ) end test ]]" 3467 3468 \item "[[ ttst 2 = logcount ( -7 ) end test ]]" 3469 3470 \item "[[ ttst 3 = logcount ( -8 ) end test ]]" 3471 3472 \item "[[ ttst 1 = logcount ( -9 ) end test ]]" 3473 3474 \end{statements}" ]" 3475 3476 3477 3478 \subsection{integer-length} 3479 3480 "[ "\begin{statements} 3481 3482 \item "[[ etst tx ; integer-length ( tt ) end test ]]" 3483 3484 \item "[[ etst ty ; integer-length ( ty ) end test ]]" 3485 3486 \item "[[ ttst 0 = integer-length ( 0 ) end test ]]" 3487 3488 \item "[[ ttst 1 = integer-length ( 1 ) end test ]]" 3489 3490 \item "[[ ttst 2 = integer-length ( 2 ) end test ]]" 3491 3492 \item "[[ ttst 2 = integer-length ( 3 ) end test ]]" 3493 3494 \item "[[ ttst 3 = integer-length ( 4 ) end test ]]" 3495 3496 \item "[[ ttst 3 = integer-length ( 5 ) end test ]]" 3497 3498 \item "[[ ttst 3 = integer-length ( 6 ) end test ]]" 3499 3500 \item "[[ ttst 3 = integer-length ( 7 ) end test ]]" 3501 3502 \item "[[ ttst 4 = integer-length ( 8 ) end test ]]" 3503 3504 \item "[[ ttst 4 = integer-length ( 9 ) end test ]]" 3505 3506 \item "[[ ttst 0 = integer-length ( -1 ) end test ]]" 3507 3508 \item "[[ ttst 1 = integer-length ( -2 ) end test ]]" 3509 3510 \item "[[ ttst 2 = integer-length ( -3 ) end test ]]" 3511 3512 \item "[[ ttst 2 = integer-length ( -4 ) end test ]]" 3513 3514 \item "[[ ttst 3 = integer-length ( -5 ) end test ]]" 3515 3516 \item "[[ ttst 3 = integer-length ( -6 ) end test ]]" 3517 3518 \item "[[ ttst 3 = integer-length ( -7 ) end test ]]" 3519 3520 \item "[[ ttst 3 = integer-length ( -8 ) end test ]]" 3521 3522 \item "[[ ttst 4 = integer-length ( -9 ) end test ]]" 3523 3524 \end{statements}" ]" 3525 3526 3527 3528 \section{Numerals} 3529 3530 "[ "\begin{statements} 3531 3532 \item "[[ ttst quote 50 end quote t= quote %% %5 %0 end quote end test ]]" 3533 3534 \item "[[ ttst quote 51 end quote t= quote %% %5 %1 end quote end test ]]" 3535 3536 \item "[[ ttst quote 52 end quote t= quote %% %5 %2 end quote end test ]]" 3537 3538 \item "[[ ttst quote 53 end quote t= quote %% %5 %3 end quote end test ]]" 3539 3540 \item "[[ ttst quote 54 end quote t= quote %% %5 %4 end quote end test ]]" 3541 3542 \item "[[ ttst quote 55 end quote t= quote %% %5 %5 end quote end test ]]" 3543 3544 \item "[[ ttst quote 56 end quote t= quote %% %5 %6 end quote end test ]]" 3545 3546 \item "[[ ttst quote 57 end quote t= quote %% %5 %7 end quote end test ]]" 3547 3548 \item "[[ ttst quote 58 end quote t= quote %% %5 %8 end quote end test ]]" 3549 3550 \item "[[ ttst quote 59 end quote t= quote %% %5 %9 end quote end test ]]" 3551 3552 \item "[[ ttst quote 00 end quote t= quote %% %0 %0 end quote end test ]]" 3553 3554 \item "[[ ttst quote 20 end quote t= quote %% %2 %0 end quote end test ]]" 3555 3556 \item "[[ ttst quote 30 end quote t= quote %% %3 %0 end quote end test ]]" 3557 3558 \item "[[ ttst quote 40 end quote t= quote %% %4 %0 end quote end test ]]" 3559 3560 \item "[[ ttst quote 50 end quote t= quote %% %5 %0 end quote end test ]]" 3561 3562 \item "[[ ttst quote 60 end quote t= quote %% %6 %0 end quote end test ]]" 3563 3564 \item "[[ ttst quote 70 end quote t= quote %% %7 %0 end quote end test ]]" 3565 3566 \item "[[ ttst quote 80 end quote t= quote %% %8 %0 end quote end test ]]" 3567 3568 \item "[[ ttst quote 90 end quote t= quote %% %9 %0 end quote end test ]]" 3569 3570 \item "[[ ttst quote 12345678901 end quote t= quote %% %1 %2 %3 %4 %5 %6 %7 %8 %9 %0 %1 end quote end test ]]" 3571 3572 \item "[[ ttst quote 1x end quote t= quote exception end quote end test ]]" 3573 3574 \item "[[ ttst 123 + 45 = 168 end test ]]" 3575 3576 \item "[[ ttst 123 - 45 = 78 end test ]]" 3577 3578 \item "[[ ttst 123 * 45 = 5535 end test ]]" 3579 3580 \item "[[ ttst -123 + -45 = -168 end test ]]" 3581 3582 \item "[[ ttst -123 - -45 = -78 end test ]]" 3583 3584 \item "[[ ttst -123 * -45 = 5535 end test ]]" 3585 3586 \end{statements}" ]" 3587 3588 3589 3590 \section{Division} 3591 3592 \subsection{floor} 3593 3594 "[ "\begin{statements} 3595 3596 \item "[[ etst floor ( -9 , 1 ) ; -9 :: +0 end test ]]" 3597 3598 \item "[[ etst floor ( -8 , 1 ) ; -8 :: +0 end test ]]" 3599 3600 \item "[[ etst floor ( -7 , 1 ) ; -7 :: +0 end test ]]" 3601 3602 \item "[[ etst floor ( -6 , 1 ) ; -6 :: +0 end test ]]" 3603 3604 \item "[[ etst floor ( -5 , 1 ) ; -5 :: +0 end test ]]" 3605 3606 \item "[[ etst floor ( -4 , 1 ) ; -4 :: +0 end test ]]" 3607 3608 \item "[[ etst floor ( -3 , 1 ) ; -3 :: +0 end test ]]" 3609 3610 \item "[[ etst floor ( -2 , 1 ) ; -2 :: +0 end test ]]" 3611 3612 \item "[[ etst floor ( -1 , 1 ) ; -1 :: +0 end test ]]" 3613 3614 \item "[[ etst floor ( +0 , 1 ) ; +0 :: +0 end test ]]" 3615 3616 \item "[[ etst floor ( +1 , 1 ) ; +1 :: +0 end test ]]" 3617 3618 \item "[[ etst floor ( +2 , 1 ) ; +2 :: +0 end test ]]" 3619 3620 \item "[[ etst floor ( +3 , 1 ) ; +3 :: +0 end test ]]" 3621 3622 \item "[[ etst floor ( +4 , 1 ) ; +4 :: +0 end test ]]" 3623 3624 \item "[[ etst floor ( +5 , 1 ) ; +5 :: +0 end test ]]" 3625 3626 \item "[[ etst floor ( +6 , 1 ) ; +6 :: +0 end test ]]" 3627 3628 \item "[[ etst floor ( +7 , 1 ) ; +7 :: +0 end test ]]" 3629 3630 \item "[[ etst floor ( +8 , 1 ) ; +8 :: +0 end test ]]" 3631 3632 \item "[[ etst floor ( +9 , 1 ) ; +9 :: +0 end test ]]" 3633 3634 3635 3636 \item "[[ etst floor ( -9 , 2 ) ; -5 :: +1 end test ]]" 3637 3638 \item "[[ etst floor ( -8 , 2 ) ; -4 :: +0 end test ]]" 3639 3640 \item "[[ etst floor ( -7 , 2 ) ; -4 :: +1 end test ]]" 3641 3642 \item "[[ etst floor ( -6 , 2 ) ; -3 :: +0 end test ]]" 3643 3644 \item "[[ etst floor ( -5 , 2 ) ; -3 :: +1 end test ]]" 3645 3646 \item "[[ etst floor ( -4 , 2 ) ; -2 :: +0 end test ]]" 3647 3648 \item "[[ etst floor ( -3 , 2 ) ; -2 :: +1 end test ]]" 3649 3650 \item "[[ etst floor ( -2 , 2 ) ; -1 :: +0 end test ]]" 3651 3652 \item "[[ etst floor ( -1 , 2 ) ; -1 :: +1 end test ]]" 3653 3654 \item "[[ etst floor ( +0 , 2 ) ; +0 :: +0 end test ]]" 3655 3656 \item "[[ etst floor ( +1 , 2 ) ; +0 :: +1 end test ]]" 3657 3658 \item "[[ etst floor ( +2 , 2 ) ; +1 :: +0 end test ]]" 3659 3660 \item "[[ etst floor ( +3 , 2 ) ; +1 :: +1 end test ]]" 3661 3662 \item "[[ etst floor ( +4 , 2 ) ; +2 :: +0 end test ]]" 3663 3664 \item "[[ etst floor ( +5 , 2 ) ; +2 :: +1 end test ]]" 3665 3666 \item "[[ etst floor ( +6 , 2 ) ; +3 :: +0 end test ]]" 3667 3668 \item "[[ etst floor ( +7 , 2 ) ; +3 :: +1 end test ]]" 3669 3670 \item "[[ etst floor ( +8 , 2 ) ; +4 :: +0 end test ]]" 3671 3672 \item "[[ etst floor ( +9 , 2 ) ; +4 :: +1 end test ]]" 3673 3674 3675 3676 \item "[[ etst floor ( -9 , 3 ) ; -3 :: +0 end test ]]" 3677 3678 \item "[[ etst floor ( -8 , 3 ) ; -3 :: +1 end test ]]" 3679 3680 \item "[[ etst floor ( -7 , 3 ) ; -3 :: +2 end test ]]" 3681 3682 \item "[[ etst floor ( -6 , 3 ) ; -2 :: +0 end test ]]" 3683 3684 \item "[[ etst floor ( -5 , 3 ) ; -2 :: +1 end test ]]" 3685 3686 \item "[[ etst floor ( -4 , 3 ) ; -2 :: +2 end test ]]" 3687 3688 \item "[[ etst floor ( -3 , 3 ) ; -1 :: +0 end test ]]" 3689 3690 \item "[[ etst floor ( -2 , 3 ) ; -1 :: +1 end test ]]" 3691 3692 \item "[[ etst floor ( -1 , 3 ) ; -1 :: +2 end test ]]" 3693 3694 \item "[[ etst floor ( +0 , 3 ) ; +0 :: +0 end test ]]" 3695 3696 \item "[[ etst floor ( +1 , 3 ) ; +0 :: +1 end test ]]" 3697 3698 \item "[[ etst floor ( +2 , 3 ) ; +0 :: +2 end test ]]" 3699 3700 \item "[[ etst floor ( +3 , 3 ) ; +1 :: +0 end test ]]" 3701 3702 \item "[[ etst floor ( +4 , 3 ) ; +1 :: +1 end test ]]" 3703 3704 \item "[[ etst floor ( +5 , 3 ) ; +1 :: +2 end test ]]" 3705 3706 \item "[[ etst floor ( +6 , 3 ) ; +2 :: +0 end test ]]" 3707 3708 \item "[[ etst floor ( +7 , 3 ) ; +2 :: +1 end test ]]" 3709 3710 \item "[[ etst floor ( +8 , 3 ) ; +2 :: +2 end test ]]" 3711 3712 \item "[[ etst floor ( +9 , 3 ) ; +3 :: +0 end test ]]" 3713 3714 3715 3716 \item "[[ etst floor ( -9 , 4 ) ; -3 :: +3 end test ]]" 3717 3718 \item "[[ etst floor ( -8 , 4 ) ; -2 :: +0 end test ]]" 3719 3720 \item "[[ etst floor ( -7 , 4 ) ; -2 :: +1 end test ]]" 3721 3722 \item "[[ etst floor ( -6 , 4 ) ; -2 :: +2 end test ]]" 3723 3724 \item "[[ etst floor ( -5 , 4 ) ; -2 :: +3 end test ]]" 3725 3726 \item "[[ etst floor ( -4 , 4 ) ; -1 :: +0 end test ]]" 3727 3728 \item "[[ etst floor ( -3 , 4 ) ; -1 :: +1 end test ]]" 3729 3730 \item "[[ etst floor ( -2 , 4 ) ; -1 :: +2 end test ]]" 3731 3732 \item "[[ etst floor ( -1 , 4 ) ; -1 :: +3 end test ]]" 3733 3734 \item "[[ etst floor ( +0 , 4 ) ; +0 :: +0 end test ]]" 3735 3736 \item "[[ etst floor ( +1 , 4 ) ; +0 :: +1 end test ]]" 3737 3738 \item "[[ etst floor ( +2 , 4 ) ; +0 :: +2 end test ]]" 3739 3740 \item "[[ etst floor ( +3 , 4 ) ; +0 :: +3 end test ]]" 3741 3742 \item "[[ etst floor ( +4 , 4 ) ; +1 :: +0 end test ]]" 3743 3744 \item "[[ etst floor ( +5 , 4 ) ; +1 :: +1 end test ]]" 3745 3746 \item "[[ etst floor ( +6 , 4 ) ; +1 :: +2 end test ]]" 3747 3748 \item "[[ etst floor ( +7 , 4 ) ; +1 :: +3 end test ]]" 3749 3750 \item "[[ etst floor ( +8 , 4 ) ; +2 :: +0 end test ]]" 3751 3752 \item "[[ etst floor ( +9 , 4 ) ; +2 :: +1 end test ]]" 3753 3754 3755 3756 \item "[[ etst floor ( -9 , 5 ) ; -2 :: +1 end test ]]" 3757 3758 \item "[[ etst floor ( -8 , 5 ) ; -2 :: +2 end test ]]" 3759 3760 \item "[[ etst floor ( -7 , 5 ) ; -2 :: +3 end test ]]" 3761 3762 \item "[[ etst floor ( -6 , 5 ) ; -2 :: +4 end test ]]" 3763 3764 \item "[[ etst floor ( -5 , 5 ) ; -1 :: +0 end test ]]" 3765 3766 \item "[[ etst floor ( -4 , 5 ) ; -1 :: +1 end test ]]" 3767 3768 \item "[[ etst floor ( -3 , 5 ) ; -1 :: +2 end test ]]" 3769 3770 \item "[[ etst floor ( -2 , 5 ) ; -1 :: +3 end test ]]" 3771 3772 \item "[[ etst floor ( -1 , 5 ) ; -1 :: +4 end test ]]" 3773 3774 \item "[[ etst floor ( +0 , 5 ) ; +0 :: +0 end test ]]" 3775 3776 \item "[[ etst floor ( +1 , 5 ) ; +0 :: +1 end test ]]" 3777 3778 \item "[[ etst floor ( +2 , 5 ) ; +0 :: +2 end test ]]" 3779 3780 \item "[[ etst floor ( +3 , 5 ) ; +0 :: +3 end test ]]" 3781 3782 \item "[[ etst floor ( +4 , 5 ) ; +0 :: +4 end test ]]" 3783 3784 \item "[[ etst floor ( +5 , 5 ) ; +1 :: +0 end test ]]" 3785 3786 \item "[[ etst floor ( +6 , 5 ) ; +1 :: +1 end test ]]" 3787 3788 \item "[[ etst floor ( +7 , 5 ) ; +1 :: +2 end test ]]" 3789 3790 \item "[[ etst floor ( +8 , 5 ) ; +1 :: +3 end test ]]" 3791 3792 \item "[[ etst floor ( +9 , 5 ) ; +1 :: +4 end test ]]" 3793 3794 3795 3796 \item "[[ etst floor ( -5 , 0 ) ; exception end test ]]" 3797 3798 \item "[[ etst floor ( -1 , 0 ) ; exception end test ]]" 3799 3800 \item "[[ etst floor ( +0 , 0 ) ; exception end test ]]" 3801 3802 \item "[[ etst floor ( +1 , 0 ) ; exception end test ]]" 3803 3804 \item "[[ etst floor ( +5 , 0 ) ; exception end test ]]" 3805 3806 3807 3808 \item "[[ etst floor ( -5 , -1 ) ; exception end test ]]" 3809 3810 \item "[[ etst floor ( -1 , -1 ) ; exception end test ]]" 3811 3812 \item "[[ etst floor ( +0 , -1 ) ; exception end test ]]" 3813 3814 \item "[[ etst floor ( +1 , -1 ) ; exception end test ]]" 3815 3816 \item "[[ etst floor ( +5 , -1 ) ; exception end test ]]" 3817 3818 \end{statements}" ]" 3819 3820 3821 3822 \subsection{div} 3823 3824 "[ "\begin{statements} 3825 3826 \item "[[ etst -9 div 1 ; -9 end test ]]" 3827 3828 \item "[[ etst -8 div 1 ; -8 end test ]]" 3829 3830 \item "[[ etst -7 div 1 ; -7 end test ]]" 3831 3832 \item "[[ etst -6 div 1 ; -6 end test ]]" 3833 3834 \item "[[ etst -5 div 1 ; -5 end test ]]" 3835 3836 \item "[[ etst -4 div 1 ; -4 end test ]]" 3837 3838 \item "[[ etst -3 div 1 ; -3 end test ]]" 3839 3840 \item "[[ etst -2 div 1 ; -2 end test ]]" 3841 3842 \item "[[ etst -1 div 1 ; -1 end test ]]" 3843 3844 \item "[[ etst +0 div 1 ; +0 end test ]]" 3845 3846 \item "[[ etst +1 div 1 ; +1 end test ]]" 3847 3848 \item "[[ etst +2 div 1 ; +2 end test ]]" 3849 3850 \item "[[ etst +3 div 1 ; +3 end test ]]" 3851 3852 \item "[[ etst +4 div 1 ; +4 end test ]]" 3853 3854 \item "[[ etst +5 div 1 ; +5 end test ]]" 3855 3856 \item "[[ etst +6 div 1 ; +6 end test ]]" 3857 3858 \item "[[ etst +7 div 1 ; +7 end test ]]" 3859 3860 \item "[[ etst +8 div 1 ; +8 end test ]]" 3861 3862 \item "[[ etst +9 div 1 ; +9 end test ]]" 3863 3864 3865 3866 \item "[[ etst -9 div 2 ; -5 end test ]]" 3867 3868 \item "[[ etst -8 div 2 ; -4 end test ]]" 3869 3870 \item "[[ etst -7 div 2 ; -4 end test ]]" 3871 3872 \item "[[ etst -6 div 2 ; -3 end test ]]" 3873 3874 \item "[[ etst -5 div 2 ; -3 end test ]]" 3875 3876 \item "[[ etst -4 div 2 ; -2 end test ]]" 3877 3878 \item "[[ etst -3 div 2 ; -2 end test ]]" 3879 3880 \item "[[ etst -2 div 2 ; -1 end test ]]" 3881 3882 \item "[[ etst -1 div 2 ; -1 end test ]]" 3883 3884 \item "[[ etst +0 div 2 ; +0 end test ]]" 3885 3886 \item "[[ etst +1 div 2 ; +0 end test ]]" 3887 3888 \item "[[ etst +2 div 2 ; +1 end test ]]" 3889 3890 \item "[[ etst +3 div 2 ; +1 end test ]]" 3891 3892 \item "[[ etst +4 div 2 ; +2 end test ]]" 3893 3894 \item "[[ etst +5 div 2 ; +2 end test ]]" 3895 3896 \item "[[ etst +6 div 2 ; +3 end test ]]" 3897 3898 \item "[[ etst +7 div 2 ; +3 end test ]]" 3899 3900 \item "[[ etst +8 div 2 ; +4 end test ]]" 3901 3902 \item "[[ etst +9 div 2 ; +4 end test ]]" 3903 3904 3905 3906 \item "[[ etst -9 div 3 ; -3 end test ]]" 3907 3908 \item "[[ etst -8 div 3 ; -3 end test ]]" 3909 3910 \item "[[ etst -7 div 3 ; -3 end test ]]" 3911 3912 \item "[[ etst -6 div 3 ; -2 end test ]]" 3913 3914 \item "[[ etst -5 div 3 ; -2 end test ]]" 3915 3916 \item "[[ etst -4 div 3 ; -2 end test ]]" 3917 3918 \item "[[ etst -3 div 3 ; -1 end test ]]" 3919 3920 \item "[[ etst -2 div 3 ; -1 end test ]]" 3921 3922 \item "[[ etst -1 div 3 ; -1 end test ]]" 3923 3924 \item "[[ etst +0 div 3 ; +0 end test ]]" 3925 3926 \item "[[ etst +1 div 3 ; +0 end test ]]" 3927 3928 \item "[[ etst +2 div 3 ; +0 end test ]]" 3929 3930 \item "[[ etst +3 div 3 ; +1 end test ]]" 3931 3932 \item "[[ etst +4 div 3 ; +1 end test ]]" 3933 3934 \item "[[ etst +5 div 3 ; +1 end test ]]" 3935 3936 \item "[[ etst +6 div 3 ; +2 end test ]]" 3937 3938 \item "[[ etst +7 div 3 ; +2 end test ]]" 3939 3940 \item "[[ etst +8 div 3 ; +2 end test ]]" 3941 3942 \item "[[ etst +9 div 3 ; +3 end test ]]" 3943 3944 3945 3946 \item "[[ etst -9 div 4 ; -3 end test ]]" 3947 3948 \item "[[ etst -8 div 4 ; -2 end test ]]" 3949 3950 \item "[[ etst -7 div 4 ; -2 end test ]]" 3951 3952 \item "[[ etst -6 div 4 ; -2 end test ]]" 3953 3954 \item "[[ etst -5 div 4 ; -2 end test ]]" 3955 3956 \item "[[ etst -4 div 4 ; -1 end test ]]" 3957 3958 \item "[[ etst -3 div 4 ; -1 end test ]]" 3959 3960 \item "[[ etst -2 div 4 ; -1 end test ]]" 3961 3962 \item "[[ etst -1 div 4 ; -1 end test ]]" 3963 3964 \item "[[ etst +0 div 4 ; +0 end test ]]" 3965 3966 \item "[[ etst +1 div 4 ; +0 end test ]]" 3967 3968 \item "[[ etst +2 div 4 ; +0 end test ]]" 3969 3970 \item "[[ etst +3 div 4 ; +0 end test ]]" 3971 3972 \item "[[ etst +4 div 4 ; +1 end test ]]" 3973 3974 \item "[[ etst +5 div 4 ; +1 end test ]]" 3975 3976 \item "[[ etst +6 div 4 ; +1 end test ]]" 3977 3978 \item "[[ etst +7 div 4 ; +1 end test ]]" 3979 3980 \item "[[ etst +8 div 4 ; +2 end test ]]" 3981 3982 \item "[[ etst +9 div 4 ; +2 end test ]]" 3983 3984 3985 3986 \item "[[ etst -9 div 5 ; -2 end test ]]" 3987 3988 \item "[[ etst -8 div 5 ; -2 end test ]]" 3989 3990 \item "[[ etst -7 div 5 ; -2 end test ]]" 3991 3992 \item "[[ etst -6 div 5 ; -2 end test ]]" 3993 3994 \item "[[ etst -5 div 5 ; -1 end test ]]" 3995 3996 \item "[[ etst -4 div 5 ; -1 end test ]]" 3997 3998 \item "[[ etst -3 div 5 ; -1 end test ]]" 3999 4000 \item "[[ etst -2 div 5 ; -1 end test ]]" 4001 4002 \item "[[ etst -1 div 5 ; -1 end test ]]" 4003 4004 \item "[[ etst +0 div 5 ; +0 end test ]]" 4005 4006 \item "[[ etst +1 div 5 ; +0 end test ]]" 4007 4008 \item "[[ etst +2 div 5 ; +0 end test ]]" 4009 4010 \item "[[ etst +3 div 5 ; +0 end test ]]" 4011 4012 \item "[[ etst +4 div 5 ; +0 end test ]]" 4013 4014 \item "[[ etst +5 div 5 ; +1 end test ]]" 4015 4016 \item "[[ etst +6 div 5 ; +1 end test ]]" 4017 4018 \item "[[ etst +7 div 5 ; +1 end test ]]" 4019 4020 \item "[[ etst +8 div 5 ; +1 end test ]]" 4021 4022 \item "[[ etst +9 div 5 ; +1 end test ]]" 4023 4024 4025 4026 \item "[[ etst -5 div 0 ; exception end test ]]" 4027 4028 \item "[[ etst -1 div 0 ; exception end test ]]" 4029 4030 \item "[[ etst +0 div 0 ; exception end test ]]" 4031 4032 \item "[[ etst +1 div 0 ; exception end test ]]" 4033 4034 \item "[[ etst +5 div 0 ; exception end test ]]" 4035 4036 4037 4038 \item "[[ etst -5 div -1 ; exception end test ]]" 4039 4040 \item "[[ etst -1 div -1 ; exception end test ]]" 4041 4042 \item "[[ etst +0 div -1 ; exception end test ]]" 4043 4044 \item "[[ etst +1 div -1 ; exception end test ]]" 4045 4046 \item "[[ etst +5 div -1 ; exception end test ]]" 4047 4048 \end{statements}" ]" 4049 4050 4051 4052 \subsection{mod} 4053 4054 "[ "\begin{statements} 4055 4056 \item "[[ etst -9 mod 1 ; +0 end test ]]" 4057 4058 \item "[[ etst -8 mod 1 ; +0 end test ]]" 4059 4060 \item "[[ etst -7 mod 1 ; +0 end test ]]" 4061 4062 \item "[[ etst -6 mod 1 ; +0 end test ]]" 4063 4064 \item "[[ etst -5 mod 1 ; +0 end test ]]" 4065 4066 \item "[[ etst -4 mod 1 ; +0 end test ]]" 4067 4068 \item "[[ etst -3 mod 1 ; +0 end test ]]" 4069 4070 \item "[[ etst -2 mod 1 ; +0 end test ]]" 4071 4072 \item "[[ etst -1 mod 1 ; +0 end test ]]" 4073 4074 \item "[[ etst +0 mod 1 ; +0 end test ]]" 4075 4076 \item "[[ etst +1 mod 1 ; +0 end test ]]" 4077 4078 \item "[[ etst +2 mod 1 ; +0 end test ]]" 4079 4080 \item "[[ etst +3 mod 1 ; +0 end test ]]" 4081 4082 \item "[[ etst +4 mod 1 ; +0 end test ]]" 4083 4084 \item "[[ etst +5 mod 1 ; +0 end test ]]" 4085 4086 \item "[[ etst +6 mod 1 ; +0 end test ]]" 4087 4088 \item "[[ etst +7 mod 1 ; +0 end test ]]" 4089 4090 \item "[[ etst +8 mod 1 ; +0 end test ]]" 4091 4092 \item "[[ etst +9 mod 1 ; +0 end test ]]" 4093 4094 4095 4096 \item "[[ etst -9 mod 2 ; +1 end test ]]" 4097 4098 \item "[[ etst -8 mod 2 ; +0 end test ]]" 4099 4100 \item "[[ etst -7 mod 2 ; +1 end test ]]" 4101 4102 \item "[[ etst -6 mod 2 ; +0 end test ]]" 4103 4104 \item "[[ etst -5 mod 2 ; +1 end test ]]" 4105 4106 \item "[[ etst -4 mod 2 ; +0 end test ]]" 4107 4108 \item "[[ etst -3 mod 2 ; +1 end test ]]" 4109 4110 \item "[[ etst -2 mod 2 ; +0 end test ]]" 4111 4112 \item "[[ etst -1 mod 2 ; +1 end test ]]" 4113 4114 \item "[[ etst +0 mod 2 ; +0 end test ]]" 4115 4116 \item "[[ etst +1 mod 2 ; +1 end test ]]" 4117 4118 \item "[[ etst +2 mod 2 ; +0 end test ]]" 4119 4120 \item "[[ etst +3 mod 2 ; +1 end test ]]" 4121 4122 \item "[[ etst +4 mod 2 ; +0 end test ]]" 4123 4124 \item "[[ etst +5 mod 2 ; +1 end test ]]" 4125 4126 \item "[[ etst +6 mod 2 ; +0 end test ]]" 4127 4128 \item "[[ etst +7 mod 2 ; +1 end test ]]" 4129 4130 \item "[[ etst +8 mod 2 ; +0 end test ]]" 4131 4132 \item "[[ etst +9 mod 2 ; +1 end test ]]" 4133 4134 4135 4136 \item "[[ etst -9 mod 3 ; +0 end test ]]" 4137 4138 \item "[[ etst -8 mod 3 ; +1 end test ]]" 4139 4140 \item "[[ etst -7 mod 3 ; +2 end test ]]" 4141 4142 \item "[[ etst -6 mod 3 ; +0 end test ]]" 4143 4144 \item "[[ etst -5 mod 3 ; +1 end test ]]" 4145 4146 \item "[[ etst -4 mod 3 ; +2 end test ]]" 4147 4148 \item "[[ etst -3 mod 3 ; +0 end test ]]" 4149 4150 \item "[[ etst -2 mod 3 ; +1 end test ]]" 4151 4152 \item "[[ etst -1 mod 3 ; +2 end test ]]" 4153 4154 \item "[[ etst +0 mod 3 ; +0 end test ]]" 4155 4156 \item "[[ etst +1 mod 3 ; +1 end test ]]" 4157 4158 \item "[[ etst +2 mod 3 ; +2 end test ]]" 4159 4160 \item "[[ etst +3 mod 3 ; +0 end test ]]" 4161 4162 \item "[[ etst +4 mod 3 ; +1 end test ]]" 4163 4164 \item "[[ etst +5 mod 3 ; +2 end test ]]" 4165 4166 \item "[[ etst +6 mod 3 ; +0 end test ]]" 4167 4168 \item "[[ etst +7 mod 3 ; +1 end test ]]" 4169 4170 \item "[[ etst +8 mod 3 ; +2 end test ]]" 4171 4172 \item "[[ etst +9 mod 3 ; +0 end test ]]" 4173 4174 4175 4176 \item "[[ etst -9 mod 4 ; +3 end test ]]" 4177 4178 \item "[[ etst -8 mod 4 ; +0 end test ]]" 4179 4180 \item "[[ etst -7 mod 4 ; +1 end test ]]" 4181 4182 \item "[[ etst -6 mod 4 ; +2 end test ]]" 4183 4184 \item "[[ etst -5 mod 4 ; +3 end test ]]" 4185 4186 \item "[[ etst -4 mod 4 ; +0 end test ]]" 4187 4188 \item "[[ etst -3 mod 4 ; +1 end test ]]" 4189 4190 \item "[[ etst -2 mod 4 ; +2 end test ]]" 4191 4192 \item "[[ etst -1 mod 4 ; +3 end test ]]" 4193 4194 \item "[[ etst +0 mod 4 ; +0 end test ]]" 4195 4196 \item "[[ etst +1 mod 4 ; +1 end test ]]" 4197 4198 \item "[[ etst +2 mod 4 ; +2 end test ]]" 4199 4200 \item "[[ etst +3 mod 4 ; +3 end test ]]" 4201 4202 \item "[[ etst +4 mod 4 ; +0 end test ]]" 4203 4204 \item "[[ etst +5 mod 4 ; +1 end test ]]" 4205 4206 \item "[[ etst +6 mod 4 ; +2 end test ]]" 4207 4208 \item "[[ etst +7 mod 4 ; +3 end test ]]" 4209 4210 \item "[[ etst +8 mod 4 ; +0 end test ]]" 4211 4212 \item "[[ etst +9 mod 4 ; +1 end test ]]" 4213 4214 4215 4216 \item "[[ etst -9 mod 5 ; +1 end test ]]" 4217 4218 \item "[[ etst -8 mod 5 ; +2 end test ]]" 4219 4220 \item "[[ etst -7 mod 5 ; +3 end test ]]" 4221 4222 \item "[[ etst -6 mod 5 ; +4 end test ]]" 4223 4224 \item "[[ etst -5 mod 5 ; +0 end test ]]" 4225 4226 \item "[[ etst -4 mod 5 ; +1 end test ]]" 4227 4228 \item "[[ etst -3 mod 5 ; +2 end test ]]" 4229 4230 \item "[[ etst -2 mod 5 ; +3 end test ]]" 4231 4232 \item "[[ etst -1 mod 5 ; +4 end test ]]" 4233 4234 \item "[[ etst +0 mod 5 ; +0 end test ]]" 4235 4236 \item "[[ etst +1 mod 5 ; +1 end test ]]" 4237 4238 \item "[[ etst +2 mod 5 ; +2 end test ]]" 4239 4240 \item "[[ etst +3 mod 5 ; +3 end test ]]" 4241 4242 \item "[[ etst +4 mod 5 ; +4 end test ]]" 4243 4244 \item "[[ etst +5 mod 5 ; +0 end test ]]" 4245 4246 \item "[[ etst +6 mod 5 ; +1 end test ]]" 4247 4248 \item "[[ etst +7 mod 5 ; +2 end test ]]" 4249 4250 \item "[[ etst +8 mod 5 ; +3 end test ]]" 4251 4252 \item "[[ etst +9 mod 5 ; +4 end test ]]" 4253 4254 4255 4256 \item "[[ etst -5 mod 0 ; exception end test ]]" 4257 4258 \item "[[ etst -1 mod 0 ; exception end test ]]" 4259 4260 \item "[[ etst +0 mod 0 ; exception end test ]]" 4261 4262 \item "[[ etst +1 mod 0 ; exception end test ]]" 4263 4264 \item "[[ etst +5 mod 0 ; exception end test ]]" 4265 4266 4267 4268 \item "[[ etst -5 mod -1 ; exception end test ]]" 4269 4270 \item "[[ etst -1 mod -1 ; exception end test ]]" 4271 4272 \item "[[ etst +0 mod -1 ; exception end test ]]" 4273 4274 \item "[[ etst +1 mod -1 ; exception end test ]]" 4275 4276 \item "[[ etst +5 mod -1 ; exception end test ]]" 4277 4278 \end{statements}" ]" 4279 4280 4281 4282 \subsection{ceiling} 4283 4284 "[ "\begin{statements} 4285 4286 \item "[[ etst ceiling ( +9 , 1 ) ; +9 :: -0 end test ]]" 4287 4288 \item "[[ etst ceiling ( +8 , 1 ) ; +8 :: -0 end test ]]" 4289 4290 \item "[[ etst ceiling ( +7 , 1 ) ; +7 :: -0 end test ]]" 4291 4292 \item "[[ etst ceiling ( +6 , 1 ) ; +6 :: -0 end test ]]" 4293 4294 \item "[[ etst ceiling ( +5 , 1 ) ; +5 :: -0 end test ]]" 4295 4296 \item "[[ etst ceiling ( +4 , 1 ) ; +4 :: -0 end test ]]" 4297 4298 \item "[[ etst ceiling ( +3 , 1 ) ; +3 :: -0 end test ]]" 4299 4300 \item "[[ etst ceiling ( +2 , 1 ) ; +2 :: -0 end test ]]" 4301 4302 \item "[[ etst ceiling ( +1 , 1 ) ; +1 :: -0 end test ]]" 4303 4304 \item "[[ etst ceiling ( -0 , 1 ) ; -0 :: -0 end test ]]" 4305 4306 \item "[[ etst ceiling ( -1 , 1 ) ; -1 :: -0 end test ]]" 4307 4308 \item "[[ etst ceiling ( -2 , 1 ) ; -2 :: -0 end test ]]" 4309 4310 \item "[[ etst ceiling ( -3 , 1 ) ; -3 :: -0 end test ]]" 4311 4312 \item "[[ etst ceiling ( -4 , 1 ) ; -4 :: -0 end test ]]" 4313 4314 \item "[[ etst ceiling ( -5 , 1 ) ; -5 :: -0 end test ]]" 4315 4316 \item "[[ etst ceiling ( -6 , 1 ) ; -6 :: -0 end test ]]" 4317 4318 \item "[[ etst ceiling ( -7 , 1 ) ; -7 :: -0 end test ]]" 4319 4320 \item "[[ etst ceiling ( -8 , 1 ) ; -8 :: -0 end test ]]" 4321 4322 \item "[[ etst ceiling ( -9 , 1 ) ; -9 :: -0 end test ]]" 4323 4324 4325 4326 \item "[[ etst ceiling ( +9 , 2 ) ; +5 :: -1 end test ]]" 4327 4328 \item "[[ etst ceiling ( +8 , 2 ) ; +4 :: -0 end test ]]" 4329 4330 \item "[[ etst ceiling ( +7 , 2 ) ; +4 :: -1 end test ]]" 4331 4332 \item "[[ etst ceiling ( +6 , 2 ) ; +3 :: -0 end test ]]" 4333 4334 \item "[[ etst ceiling ( +5 , 2 ) ; +3 :: -1 end test ]]" 4335 4336 \item "[[ etst ceiling ( +4 , 2 ) ; +2 :: -0 end test ]]" 4337 4338 \item "[[ etst ceiling ( +3 , 2 ) ; +2 :: -1 end test ]]" 4339 4340 \item "[[ etst ceiling ( +2 , 2 ) ; +1 :: -0 end test ]]" 4341 4342 \item "[[ etst ceiling ( +1 , 2 ) ; +1 :: -1 end test ]]" 4343 4344 \item "[[ etst ceiling ( -0 , 2 ) ; -0 :: -0 end test ]]" 4345 4346 \item "[[ etst ceiling ( -1 , 2 ) ; -0 :: -1 end test ]]" 4347 4348 \item "[[ etst ceiling ( -2 , 2 ) ; -1 :: -0 end test ]]" 4349 4350 \item "[[ etst ceiling ( -3 , 2 ) ; -1 :: -1 end test ]]" 4351 4352 \item "[[ etst ceiling ( -4 , 2 ) ; -2 :: -0 end test ]]" 4353 4354 \item "[[ etst ceiling ( -5 , 2 ) ; -2 :: -1 end test ]]" 4355 4356 \item "[[ etst ceiling ( -6 , 2 ) ; -3 :: -0 end test ]]" 4357 4358 \item "[[ etst ceiling ( -7 , 2 ) ; -3 :: -1 end test ]]" 4359 4360 \item "[[ etst ceiling ( -8 , 2 ) ; -4 :: -0 end test ]]" 4361 4362 \item "[[ etst ceiling ( -9 , 2 ) ; -4 :: -1 end test ]]" 4363 4364 4365 4366 \item "[[ etst ceiling ( +9 , 3 ) ; +3 :: -0 end test ]]" 4367 4368 \item "[[ etst ceiling ( +8 , 3 ) ; +3 :: -1 end test ]]" 4369 4370 \item "[[ etst ceiling ( +7 , 3 ) ; +3 :: -2 end test ]]" 4371 4372 \item "[[ etst ceiling ( +6 , 3 ) ; +2 :: -0 end test ]]" 4373 4374 \item "[[ etst ceiling ( +5 , 3 ) ; +2 :: -1 end test ]]" 4375 4376 \item "[[ etst ceiling ( +4 , 3 ) ; +2 :: -2 end test ]]" 4377 4378 \item "[[ etst ceiling ( +3 , 3 ) ; +1 :: -0 end test ]]" 4379 4380 \item "[[ etst ceiling ( +2 , 3 ) ; +1 :: -1 end test ]]" 4381 4382 \item "[[ etst ceiling ( +1 , 3 ) ; +1 :: -2 end test ]]" 4383 4384 \item "[[ etst ceiling ( -0 , 3 ) ; -0 :: -0 end test ]]" 4385 4386 \item "[[ etst ceiling ( -1 , 3 ) ; -0 :: -1 end test ]]" 4387 4388 \item "[[ etst ceiling ( -2 , 3 ) ; -0 :: -2 end test ]]" 4389 4390 \item "[[ etst ceiling ( -3 , 3 ) ; -1 :: -0 end test ]]" 4391 4392 \item "[[ etst ceiling ( -4 , 3 ) ; -1 :: -1 end test ]]" 4393 4394 \item "[[ etst ceiling ( -5 , 3 ) ; -1 :: -2 end test ]]" 4395 4396 \item "[[ etst ceiling ( -6 , 3 ) ; -2 :: -0 end test ]]" 4397 4398 \item "[[ etst ceiling ( -7 , 3 ) ; -2 :: -1 end test ]]" 4399 4400 \item "[[ etst ceiling ( -8 , 3 ) ; -2 :: -2 end test ]]" 4401 4402 \item "[[ etst ceiling ( -9 , 3 ) ; -3 :: -0 end test ]]" 4403 4404 4405 4406 \item "[[ etst ceiling ( +9 , 4 ) ; +3 :: -3 end test ]]" 4407 4408 \item "[[ etst ceiling ( +8 , 4 ) ; +2 :: -0 end test ]]" 4409 4410 \item "[[ etst ceiling ( +7 , 4 ) ; +2 :: -1 end test ]]" 4411 4412 \item "[[ etst ceiling ( +6 , 4 ) ; +2 :: -2 end test ]]" 4413 4414 \item "[[ etst ceiling ( +5 , 4 ) ; +2 :: -3 end test ]]" 4415 4416 \item "[[ etst ceiling ( +4 , 4 ) ; +1 :: -0 end test ]]" 4417 4418 \item "[[ etst ceiling ( +3 , 4 ) ; +1 :: -1 end test ]]" 4419 4420 \item "[[ etst ceiling ( +2 , 4 ) ; +1 :: -2 end test ]]" 4421 4422 \item "[[ etst ceiling ( +1 , 4 ) ; +1 :: -3 end test ]]" 4423 4424 \item "[[ etst ceiling ( -0 , 4 ) ; -0 :: -0 end test ]]" 4425 4426 \item "[[ etst ceiling ( -1 , 4 ) ; -0 :: -1 end test ]]" 4427 4428 \item "[[ etst ceiling ( -2 , 4 ) ; -0 :: -2 end test ]]" 4429 4430 \item "[[ etst ceiling ( -3 , 4 ) ; -0 :: -3 end test ]]" 4431 4432 \item "[[ etst ceiling ( -4 , 4 ) ; -1 :: -0 end test ]]" 4433 4434 \item "[[ etst ceiling ( -5 , 4 ) ; -1 :: -1 end test ]]" 4435 4436 \item "[[ etst ceiling ( -6 , 4 ) ; -1 :: -2 end test ]]" 4437 4438 \item "[[ etst ceiling ( -7 , 4 ) ; -1 :: -3 end test ]]" 4439 4440 \item "[[ etst ceiling ( -8 , 4 ) ; -2 :: -0 end test ]]" 4441 4442 \item "[[ etst ceiling ( -9 , 4 ) ; -2 :: -1 end test ]]" 4443 4444 4445 4446 \item "[[ etst ceiling ( +9 , 5 ) ; +2 :: -1 end test ]]" 4447 4448 \item "[[ etst ceiling ( +8 , 5 ) ; +2 :: -2 end test ]]" 4449 4450 \item "[[ etst ceiling ( +7 , 5 ) ; +2 :: -3 end test ]]" 4451 4452 \item "[[ etst ceiling ( +6 , 5 ) ; +2 :: -4 end test ]]" 4453 4454 \item "[[ etst ceiling ( +5 , 5 ) ; +1 :: -0 end test ]]" 4455 4456 \item "[[ etst ceiling ( +4 , 5 ) ; +1 :: -1 end test ]]" 4457 4458 \item "[[ etst ceiling ( +3 , 5 ) ; +1 :: -2 end test ]]" 4459 4460 \item "[[ etst ceiling ( +2 , 5 ) ; +1 :: -3 end test ]]" 4461 4462 \item "[[ etst ceiling ( +1 , 5 ) ; +1 :: -4 end test ]]" 4463 4464 \item "[[ etst ceiling ( -0 , 5 ) ; -0 :: -0 end test ]]" 4465 4466 \item "[[ etst ceiling ( -1 , 5 ) ; -0 :: -1 end test ]]" 4467 4468 \item "[[ etst ceiling ( -2 , 5 ) ; -0 :: -2 end test ]]" 4469 4470 \item "[[ etst ceiling ( -3 , 5 ) ; -0 :: -3 end test ]]" 4471 4472 \item "[[ etst ceiling ( -4 , 5 ) ; -0 :: -4 end test ]]" 4473 4474 \item "[[ etst ceiling ( -5 , 5 ) ; -1 :: -0 end test ]]" 4475 4476 \item "[[ etst ceiling ( -6 , 5 ) ; -1 :: -1 end test ]]" 4477 4478 \item "[[ etst ceiling ( -7 , 5 ) ; -1 :: -2 end test ]]" 4479 4480 \item "[[ etst ceiling ( -8 , 5 ) ; -1 :: -3 end test ]]" 4481 4482 \item "[[ etst ceiling ( -9 , 5 ) ; -1 :: -4 end test ]]" 4483 4484 4485 4486 \item "[[ etst ceiling ( +5 , 0 ) ; exception end test ]]" 4487 4488 \item "[[ etst ceiling ( +1 , 0 ) ; exception end test ]]" 4489 4490 \item "[[ etst ceiling ( -0 , 0 ) ; exception end test ]]" 4491 4492 \item "[[ etst ceiling ( -1 , 0 ) ; exception end test ]]" 4493 4494 \item "[[ etst ceiling ( -5 , 0 ) ; exception end test ]]" 4495 4496 4497 4498 \item "[[ etst ceiling ( +5 , -1 ) ; exception end test ]]" 4499 4500 \item "[[ etst ceiling ( +1 , -1 ) ; exception end test ]]" 4501 4502 \item "[[ etst ceiling ( -0 , -1 ) ; exception end test ]]" 4503 4504 \item "[[ etst ceiling ( -1 , -1 ) ; exception end test ]]" 4505 4506 \item "[[ etst ceiling ( -5 , -1 ) ; exception end test ]]" 4507 4508 \end{statements}" ]" 4509 4510 4511 4512 \subsection{truncate} 4513 4514 "[ "\begin{statements} 4515 4516 \item "[[ etst truncate ( +0 , 1 ) ; +0 :: +0 end test ]]" 4517 4518 \item "[[ etst truncate ( +1 , 1 ) ; +1 :: +0 end test ]]" 4519 4520 \item "[[ etst truncate ( +2 , 1 ) ; +2 :: +0 end test ]]" 4521 4522 \item "[[ etst truncate ( +3 , 1 ) ; +3 :: +0 end test ]]" 4523 4524 \item "[[ etst truncate ( +4 , 1 ) ; +4 :: +0 end test ]]" 4525 4526 \item "[[ etst truncate ( +5 , 1 ) ; +5 :: +0 end test ]]" 4527 4528 \item "[[ etst truncate ( +6 , 1 ) ; +6 :: +0 end test ]]" 4529 4530 \item "[[ etst truncate ( +7 , 1 ) ; +7 :: +0 end test ]]" 4531 4532 \item "[[ etst truncate ( +8 , 1 ) ; +8 :: +0 end test ]]" 4533 4534 \item "[[ etst truncate ( +9 , 1 ) ; +9 :: +0 end test ]]" 4535 4536 \item "[[ etst truncate ( -0 , 1 ) ; -0 :: -0 end test ]]" 4537 4538 \item "[[ etst truncate ( -1 , 1 ) ; -1 :: -0 end test ]]" 4539 4540 \item "[[ etst truncate ( -2 , 1 ) ; -2 :: -0 end test ]]" 4541 4542 \item "[[ etst truncate ( -3 , 1 ) ; -3 :: -0 end test ]]" 4543 4544 \item "[[ etst truncate ( -4 , 1 ) ; -4 :: -0 end test ]]" 4545 4546 \item "[[ etst truncate ( -5 , 1 ) ; -5 :: -0 end test ]]" 4547 4548 \item "[[ etst truncate ( -6 , 1 ) ; -6 :: -0 end test ]]" 4549 4550 \item "[[ etst truncate ( -7 , 1 ) ; -7 :: -0 end test ]]" 4551 4552 \item "[[ etst truncate ( -8 , 1 ) ; -8 :: -0 end test ]]" 4553 4554 \item "[[ etst truncate ( -9 , 1 ) ; -9 :: -0 end test ]]" 4555 4556 4557 4558 \item "[[ etst truncate ( +0 , 2 ) ; +0 :: +0 end test ]]" 4559 4560 \item "[[ etst truncate ( +1 , 2 ) ; +0 :: +1 end test ]]" 4561 4562 \item "[[ etst truncate ( +2 , 2 ) ; +1 :: +0 end test ]]" 4563 4564 \item "[[ etst truncate ( +3 , 2 ) ; +1 :: +1 end test ]]" 4565 4566 \item "[[ etst truncate ( +4 , 2 ) ; +2 :: +0 end test ]]" 4567 4568 \item "[[ etst truncate ( +5 , 2 ) ; +2 :: +1 end test ]]" 4569 4570 \item "[[ etst truncate ( +6 , 2 ) ; +3 :: +0 end test ]]" 4571 4572 \item "[[ etst truncate ( +7 , 2 ) ; +3 :: +1 end test ]]" 4573 4574 \item "[[ etst truncate ( +8 , 2 ) ; +4 :: +0 end test ]]" 4575 4576 \item "[[ etst truncate ( +9 , 2 ) ; +4 :: +1 end test ]]" 4577 4578 \item "[[ etst truncate ( -0 , 2 ) ; -0 :: -0 end test ]]" 4579 4580 \item "[[ etst truncate ( -1 , 2 ) ; -0 :: -1 end test ]]" 4581 4582 \item "[[ etst truncate ( -2 , 2 ) ; -1 :: -0 end test ]]" 4583 4584 \item "[[ etst truncate ( -3 , 2 ) ; -1 :: -1 end test ]]" 4585 4586 \item "[[ etst truncate ( -4 , 2 ) ; -2 :: -0 end test ]]" 4587 4588 \item "[[ etst truncate ( -5 , 2 ) ; -2 :: -1 end test ]]" 4589 4590 \item "[[ etst truncate ( -6 , 2 ) ; -3 :: -0 end test ]]" 4591 4592 \item "[[ etst truncate ( -7 , 2 ) ; -3 :: -1 end test ]]" 4593 4594 \item "[[ etst truncate ( -8 , 2 ) ; -4 :: -0 end test ]]" 4595 4596 \item "[[ etst truncate ( -9 , 2 ) ; -4 :: -1 end test ]]" 4597 4598 4599 4600 \item "[[ etst truncate ( +0 , 3 ) ; +0 :: +0 end test ]]" 4601 4602 \item "[[ etst truncate ( +1 , 3 ) ; +0 :: +1 end test ]]" 4603 4604 \item "[[ etst truncate ( +2 , 3 ) ; +0 :: +2 end test ]]" 4605 4606 \item "[[ etst truncate ( +3 , 3 ) ; +1 :: +0 end test ]]" 4607 4608 \item "[[ etst truncate ( +4 , 3 ) ; +1 :: +1 end test ]]" 4609 4610 \item "[[ etst truncate ( +5 , 3 ) ; +1 :: +2 end test ]]" 4611 4612 \item "[[ etst truncate ( +6 , 3 ) ; +2 :: +0 end test ]]" 4613 4614 \item "[[ etst truncate ( +7 , 3 ) ; +2 :: +1 end test ]]" 4615 4616 \item "[[ etst truncate ( +8 , 3 ) ; +2 :: +2 end test ]]" 4617 4618 \item "[[ etst truncate ( +9 , 3 ) ; +3 :: +0 end test ]]" 4619 4620 \item "[[ etst truncate ( -0 , 3 ) ; -0 :: -0 end test ]]" 4621 4622 \item "[[ etst truncate ( -1 , 3 ) ; -0 :: -1 end test ]]" 4623 4624 \item "[[ etst truncate ( -2 , 3 ) ; -0 :: -2 end test ]]" 4625 4626 \item "[[ etst truncate ( -3 , 3 ) ; -1 :: -0 end test ]]" 4627 4628 \item "[[ etst truncate ( -4 , 3 ) ; -1 :: -1 end test ]]" 4629 4630 \item "[[ etst truncate ( -5 , 3 ) ; -1 :: -2 end test ]]" 4631 4632 \item "[[ etst truncate ( -6 , 3 ) ; -2 :: -0 end test ]]" 4633 4634 \item "[[ etst truncate ( -7 , 3 ) ; -2 :: -1 end test ]]" 4635 4636 \item "[[ etst truncate ( -8 , 3 ) ; -2 :: -2 end test ]]" 4637 4638 \item "[[ etst truncate ( -9 , 3 ) ; -3 :: -0 end test ]]" 4639 4640 4641 4642 \item "[[ etst truncate ( +0 , 4 ) ; +0 :: +0 end test ]]" 4643 4644 \item "[[ etst truncate ( +1 , 4 ) ; +0 :: +1 end test ]]" 4645 4646 \item "[[ etst truncate ( +2 , 4 ) ; +0 :: +2 end test ]]" 4647 4648 \item "[[ etst truncate ( +3 , 4 ) ; +0 :: +3 end test ]]" 4649 4650 \item "[[ etst truncate ( +4 , 4 ) ; +1 :: +0 end test ]]" 4651 4652 \item "[[ etst truncate ( +5 , 4 ) ; +1 :: +1 end test ]]" 4653 4654 \item "[[ etst truncate ( +6 , 4 ) ; +1 :: +2 end test ]]" 4655 4656 \item "[[ etst truncate ( +7 , 4 ) ; +1 :: +3 end test ]]" 4657 4658 \item "[[ etst truncate ( +8 , 4 ) ; +2 :: +0 end test ]]" 4659 4660 \item "[[ etst truncate ( +9 , 4 ) ; +2 :: +1 end test ]]" 4661 4662 \item "[[ etst truncate ( -0 , 4 ) ; -0 :: -0 end test ]]" 4663 4664 \item "[[ etst truncate ( -1 , 4 ) ; -0 :: -1 end test ]]" 4665 4666 \item "[[ etst truncate ( -2 , 4 ) ; -0 :: -2 end test ]]" 4667 4668 \item "[[ etst truncate ( -3 , 4 ) ; -0 :: -3 end test ]]" 4669 4670 \item "[[ etst truncate ( -4 , 4 ) ; -1 :: -0 end test ]]" 4671 4672 \item "[[ etst truncate ( -5 , 4 ) ; -1 :: -1 end test ]]" 4673 4674 \item "[[ etst truncate ( -6 , 4 ) ; -1 :: -2 end test ]]" 4675 4676 \item "[[ etst truncate ( -7 , 4 ) ; -1 :: -3 end test ]]" 4677 4678 \item "[[ etst truncate ( -8 , 4 ) ; -2 :: -0 end test ]]" 4679 4680 \item "[[ etst truncate ( -9 , 4 ) ; -2 :: -1 end test ]]" 4681 4682 4683 4684 \item "[[ etst truncate ( +0 , 5 ) ; +0 :: +0 end test ]]" 4685 4686 \item "[[ etst truncate ( +1 , 5 ) ; +0 :: +1 end test ]]" 4687 4688 \item "[[ etst truncate ( +2 , 5 ) ; +0 :: +2 end test ]]" 4689 4690 \item "[[ etst truncate ( +3 , 5 ) ; +0 :: +3 end test ]]" 4691 4692 \item "[[ etst truncate ( +4 , 5 ) ; +0 :: +4 end test ]]" 4693 4694 \item "[[ etst truncate ( +5 , 5 ) ; +1 :: +0 end test ]]" 4695 4696 \item "[[ etst truncate ( +6 , 5 ) ; +1 :: +1 end test ]]" 4697 4698 \item "[[ etst truncate ( +7 , 5 ) ; +1 :: +2 end test ]]" 4699 4700 \item "[[ etst truncate ( +8 , 5 ) ; +1 :: +3 end test ]]" 4701 4702 \item "[[ etst truncate ( +9 , 5 ) ; +1 :: +4 end test ]]" 4703 4704 \item "[[ etst truncate ( -0 , 5 ) ; -0 :: -0 end test ]]" 4705 4706 \item "[[ etst truncate ( -1 , 5 ) ; -0 :: -1 end test ]]" 4707 4708 \item "[[ etst truncate ( -2 , 5 ) ; -0 :: -2 end test ]]" 4709 4710 \item "[[ etst truncate ( -3 , 5 ) ; -0 :: -3 end test ]]" 4711 4712 \item "[[ etst truncate ( -4 , 5 ) ; -0 :: -4 end test ]]" 4713 4714 \item "[[ etst truncate ( -5 , 5 ) ; -1 :: -0 end test ]]" 4715 4716 \item "[[ etst truncate ( -6 , 5 ) ; -1 :: -1 end test ]]" 4717 4718 \item "[[ etst truncate ( -7 , 5 ) ; -1 :: -2 end test ]]" 4719 4720 \item "[[ etst truncate ( -8 , 5 ) ; -1 :: -3 end test ]]" 4721 4722 \item "[[ etst truncate ( -9 , 5 ) ; -1 :: -4 end test ]]" 4723 4724 4725 4726 \item "[[ etst truncate ( -5 , 0 ) ; exception end test ]]" 4727 4728 \item "[[ etst truncate ( -1 , 0 ) ; exception end test ]]" 4729 4730 \item "[[ etst truncate ( +0 , 0 ) ; exception end test ]]" 4731 4732 \item "[[ etst truncate ( +1 , 0 ) ; exception end test ]]" 4733 4734 \item "[[ etst truncate ( +5 , 0 ) ; exception end test ]]" 4735 4736 4737 4738 \item "[[ etst truncate ( -5 , -1 ) ; exception end test ]]" 4739 4740 \item "[[ etst truncate ( -1 , -1 ) ; exception end test ]]" 4741 4742 \item "[[ etst truncate ( +0 , -1 ) ; exception end test ]]" 4743 4744 \item "[[ etst truncate ( +1 , -1 ) ; exception end test ]]" 4745 4746 \item "[[ etst truncate ( +5 , -1 ) ; exception end test ]]" 4747 4748 \end{statements}" ]" 4749 4750 4751 4752 \subsection{round} 4753 4754 "[ "\begin{statements} 4755 4756 \item "[[ etst round ( -9 , 1 ) ; -9 :: +0 end test ]]" 4757 4758 \item "[[ etst round ( -8 , 1 ) ; -8 :: +0 end test ]]" 4759 4760 \item "[[ etst round ( -7 , 1 ) ; -7 :: +0 end test ]]" 4761 4762 \item "[[ etst round ( -6 , 1 ) ; -6 :: +0 end test ]]" 4763 4764 \item "[[ etst round ( -5 , 1 ) ; -5 :: +0 end test ]]" 4765 4766 \item "[[ etst round ( -4 , 1 ) ; -4 :: +0 end test ]]" 4767 4768 \item "[[ etst round ( -3 , 1 ) ; -3 :: +0 end test ]]" 4769 4770 \item "[[ etst round ( -2 , 1 ) ; -2 :: +0 end test ]]" 4771 4772 \item "[[ etst round ( -1 , 1 ) ; -1 :: +0 end test ]]" 4773 4774 \item "[[ etst round ( +0 , 1 ) ; +0 :: +0 end test ]]" 4775 4776 \item "[[ etst round ( +1 , 1 ) ; +1 :: +0 end test ]]" 4777 4778 \item "[[ etst round ( +2 , 1 ) ; +2 :: +0 end test ]]" 4779 4780 \item "[[ etst round ( +3 , 1 ) ; +3 :: +0 end test ]]" 4781 4782 \item "[[ etst round ( +4 , 1 ) ; +4 :: +0 end test ]]" 4783 4784 \item "[[ etst round ( +5 , 1 ) ; +5 :: +0 end test ]]" 4785 4786 \item "[[ etst round ( +6 , 1 ) ; +6 :: +0 end test ]]" 4787 4788 \item "[[ etst round ( +7 , 1 ) ; +7 :: +0 end test ]]" 4789 4790 \item "[[ etst round ( +8 , 1 ) ; +8 :: +0 end test ]]" 4791 4792 \item "[[ etst round ( +9 , 1 ) ; +9 :: +0 end test ]]" 4793 4794 4795 4796 \item "[[ etst round ( -9 , 2 ) ; -4 :: -1 end test ]]" 4797 4798 \item "[[ etst round ( -8 , 2 ) ; -4 :: +0 end test ]]" 4799 4800 \item "[[ etst round ( -7 , 2 ) ; -4 :: +1 end test ]]" 4801 4802 \item "[[ etst round ( -6 , 2 ) ; -3 :: +0 end test ]]" 4803 4804 \item "[[ etst round ( -5 , 2 ) ; -2 :: -1 end test ]]" 4805 4806 \item "[[ etst round ( -4 , 2 ) ; -2 :: +0 end test ]]" 4807 4808 \item "[[ etst round ( -3 , 2 ) ; -2 :: +1 end test ]]" 4809 4810 \item "[[ etst round ( -2 , 2 ) ; -1 :: +0 end test ]]" 4811 4812 \item "[[ etst round ( -1 , 2 ) ; -0 :: -1 end test ]]" 4813 4814 \item "[[ etst round ( +0 , 2 ) ; +0 :: +0 end test ]]" 4815 4816 \item "[[ etst round ( +1 , 2 ) ; +0 :: +1 end test ]]" 4817 4818 \item "[[ etst round ( +2 , 2 ) ; +1 :: +0 end test ]]" 4819 4820 \item "[[ etst round ( +3 , 2 ) ; +2 :: -1 end test ]]" 4821 4822 \item "[[ etst round ( +4 , 2 ) ; +2 :: +0 end test ]]" 4823 4824 \item "[[ etst round ( +5 , 2 ) ; +2 :: +1 end test ]]" 4825 4826 \item "[[ etst round ( +6 , 2 ) ; +3 :: +0 end test ]]" 4827 4828 \item "[[ etst round ( +7 , 2 ) ; +4 :: -1 end test ]]" 4829 4830 \item "[[ etst round ( +8 , 2 ) ; +4 :: +0 end test ]]" 4831 4832 \item "[[ etst round ( +9 , 2 ) ; +4 :: +1 end test ]]" 4833 4834 4835 4836 \item "[[ etst round ( -9 , 3 ) ; -3 :: +0 end test ]]" 4837 4838 \item "[[ etst round ( -8 , 3 ) ; -3 :: +1 end test ]]" 4839 4840 \item "[[ etst round ( -7 , 3 ) ; -2 :: -1 end test ]]" 4841 4842 \item "[[ etst round ( -6 , 3 ) ; -2 :: +0 end test ]]" 4843 4844 \item "[[ etst round ( -5 , 3 ) ; -2 :: +1 end test ]]" 4845 4846 \item "[[ etst round ( -4 , 3 ) ; -1 :: -1 end test ]]" 4847 4848 \item "[[ etst round ( -3 , 3 ) ; -1 :: +0 end test ]]" 4849 4850 \item "[[ etst round ( -2 , 3 ) ; -1 :: +1 end test ]]" 4851 4852 \item "[[ etst round ( -1 , 3 ) ; +0 :: -1 end test ]]" 4853 4854 \item "[[ etst round ( +0 , 3 ) ; +0 :: +0 end test ]]" 4855 4856 \item "[[ etst round ( +1 , 3 ) ; +0 :: +1 end test ]]" 4857 4858 \item "[[ etst round ( +2 , 3 ) ; +1 :: -1 end test ]]" 4859 4860 \item "[[ etst round ( +3 , 3 ) ; +1 :: +0 end test ]]" 4861 4862 \item "[[ etst round ( +4 , 3 ) ; +1 :: +1 end test ]]" 4863 4864 \item "[[ etst round ( +5 , 3 ) ; +2 :: -1 end test ]]" 4865 4866 \item "[[ etst round ( +6 , 3 ) ; +2 :: +0 end test ]]" 4867 4868 \item "[[ etst round ( +7 , 3 ) ; +2 :: +1 end test ]]" 4869 4870 \item "[[ etst round ( +8 , 3 ) ; +3 :: -1 end test ]]" 4871 4872 \item "[[ etst round ( +9 , 3 ) ; +3 :: +0 end test ]]" 4873 4874 4875 4876 \item "[[ etst round ( -9 , 4 ) ; -2 :: -1 end test ]]" 4877 4878 \item "[[ etst round ( -8 , 4 ) ; -2 :: +0 end test ]]" 4879 4880 \item "[[ etst round ( -7 , 4 ) ; -2 :: +1 end test ]]" 4881 4882 \item "[[ etst round ( -6 , 4 ) ; -2 :: +2 end test ]]" 4883 4884 \item "[[ etst round ( -5 , 4 ) ; -1 :: -1 end test ]]" 4885 4886 \item "[[ etst round ( -4 , 4 ) ; -1 :: +0 end test ]]" 4887 4888 \item "[[ etst round ( -3 , 4 ) ; -1 :: +1 end test ]]" 4889 4890 \item "[[ etst round ( -2 , 4 ) ; +0 :: -2 end test ]]" 4891 4892 \item "[[ etst round ( -1 , 4 ) ; +0 :: -1 end test ]]" 4893 4894 \item "[[ etst round ( +0 , 4 ) ; +0 :: +0 end test ]]" 4895 4896 \item "[[ etst round ( +1 , 4 ) ; +0 :: +1 end test ]]" 4897 4898 \item "[[ etst round ( +2 , 4 ) ; +0 :: +2 end test ]]" 4899 4900 \item "[[ etst round ( +3 , 4 ) ; +1 :: -1 end test ]]" 4901 4902 \item "[[ etst round ( +4 , 4 ) ; +1 :: +0 end test ]]" 4903 4904 \item "[[ etst round ( +5 , 4 ) ; +1 :: +1 end test ]]" 4905 4906 \item "[[ etst round ( +6 , 4 ) ; +2 :: -2 end test ]]" 4907 4908 \item "[[ etst round ( +7 , 4 ) ; +2 :: -1 end test ]]" 4909 4910 \item "[[ etst round ( +8 , 4 ) ; +2 :: +0 end test ]]" 4911 4912 \item "[[ etst round ( +9 , 4 ) ; +2 :: +1 end test ]]" 4913 4914 4915 4916 \item "[[ etst round ( -9 , 5 ) ; -2 :: +1 end test ]]" 4917 4918 \item "[[ etst round ( -8 , 5 ) ; -2 :: +2 end test ]]" 4919 4920 \item "[[ etst round ( -7 , 5 ) ; -1 :: -2 end test ]]" 4921 4922 \item "[[ etst round ( -6 , 5 ) ; -1 :: -1 end test ]]" 4923 4924 \item "[[ etst round ( -5 , 5 ) ; -1 :: +0 end test ]]" 4925 4926 \item "[[ etst round ( -4 , 5 ) ; -1 :: +1 end test ]]" 4927 4928 \item "[[ etst round ( -3 , 5 ) ; -1 :: +2 end test ]]" 4929 4930 \item "[[ etst round ( -2 , 5 ) ; +0 :: -2 end test ]]" 4931 4932 \item "[[ etst round ( -1 , 5 ) ; +0 :: -1 end test ]]" 4933 4934 \item "[[ etst round ( +0 , 5 ) ; +0 :: +0 end test ]]" 4935 4936 \item "[[ etst round ( +1 , 5 ) ; +0 :: +1 end test ]]" 4937 4938 \item "[[ etst round ( +2 , 5 ) ; +0 :: +2 end test ]]" 4939 4940 \item "[[ etst round ( +3 , 5 ) ; +1 :: -2 end test ]]" 4941 4942 \item "[[ etst round ( +4 , 5 ) ; +1 :: -1 end test ]]" 4943 4944 \item "[[ etst round ( +5 , 5 ) ; +1 :: +0 end test ]]" 4945 4946 \item "[[ etst round ( +6 , 5 ) ; +1 :: +1 end test ]]" 4947 4948 \item "[[ etst round ( +7 , 5 ) ; +1 :: +2 end test ]]" 4949 4950 \item "[[ etst round ( +8 , 5 ) ; +2 :: -2 end test ]]" 4951 4952 \item "[[ etst round ( +9 , 5 ) ; +2 :: -1 end test ]]" 4953 4954 4955 4956 \item "[[ etst round ( -5 , 0 ) ; exception end test ]]" 4957 4958 \item "[[ etst round ( -1 , 0 ) ; exception end test ]]" 4959 4960 \item "[[ etst round ( +0 , 0 ) ; exception end test ]]" 4961 4962 \item "[[ etst round ( +1 , 0 ) ; exception end test ]]" 4963 4964 \item "[[ etst round ( +5 , 0 ) ; exception end test ]]" 4965 4966 4967 4968 \item "[[ etst round ( -5 , -1 ) ; exception end test ]]" 4969 4970 \item "[[ etst round ( -1 , -1 ) ; exception end test ]]" 4971 4972 \item "[[ etst round ( +0 , -1 ) ; exception end test ]]" 4973 4974 \item "[[ etst round ( +1 , -1 ) ; exception end test ]]" 4975 4976 \item "[[ etst round ( +5 , -1 ) ; exception end test ]]" 4977 4978 \end{statements}" ]" 4979 4980 4981 4982 \section{Vectors} 4983 4984 \subsection{Elementary operations} 4985 4986 "[ "\begin{statements} 4987 4988 \item "[[ ttst vector-empty ( "". ) end test ]]" 4989 4990 \item "[[ ftst vector-empty ( "a" ) end test ]]" 4991 4992 \item "[[ ttst vector-empty ( -1 ) end test ]]" 4993 4994 \item "[[ ttst vector-empty ( 255 ) end test ]]" 4995 4996 \item "[[ etst vector-head1 ( show "abc" end show ) ; 97 end test ]]" 4997 4998 \item "[[ etst vector-tail1 ( show "abc" end show ) ; show "bc" end show end test ]]" 4999 5000 \end{statements}" ]" 5001 5002 5003 5004 \subsection{vector} 5005 5006 "[ "\begin{statements} 5007 5008 \item "[[ etst vector ( show "abc" end show ) ; show "abc" end show end test ]]" 5009 5010 \item "[[ etst vector ( 0 ) ; show "". end show end test ]]" 5011 5012 \item "[[ etst vector ( 1 ) ; show "". end show end test ]]" 5013 5014 \item "[[ etst vector ( 97 ) ; show "". end show end test ]]" 5015 5016 \item "[[ etst vector ( 97 + 256 * 1 ) ; show "a" end show end test ]]" 5017 5018 \item "[[ etst vector ( 97 + 256 * 2 ) ; show "a" end show end test ]]" 5019 5020 \item "[[ etst vector ( 97 + 256 * 255 ) ; show "a" end show end test ]]" 5021 5022 \item "[[ etst vector ( 97 + 256 * 256 ) ; 97 + 256 * 256 end test ]]" 5023 5024 \item "[[ etst vector ( -1 ) ; show "". end show end test ]]" 5025 5026 \item "[[ etst vector ( -1000 ) ; show "". end show end test ]]" 5027 5028 \end{statements}" ]" 5029 5030 5031 5032 \subsection{vector-norm} 5033 5034 "[ "\begin{statements} 5035 5036 \item "[[ etst vector-norm ( show "abc" end show ) ; show "abc" end show end test ]]" 5037 5038 \item "[[ etst vector-norm ( 0 ) ; show true end show end test ]]" 5039 5040 \item "[[ etst vector-norm ( 1 ) ; show "". end show end test ]]" 5041 5042 \item "[[ etst vector-norm ( 97 ) ; show true end show end test ]]" 5043 5044 \item "[[ etst vector-norm ( 97 + 256 * 1 ) ; show "a" end show end test ]]" 5045 5046 \item "[[ etst vector-norm ( 97 + 256 * 2 ) ; show true end show end test ]]" 5047 5048 \item "[[ etst vector-norm ( 97 + 256 * 255 ) ; show true end show end test ]]" 5049 5050 \item "[[ etst vector-norm ( 97 + 256 * 256 ) ; 97 + 256 * 256 end test ]]" 5051 5052 \item "[[ etst vector-norm ( -1 ) ; show true end show end test ]]" 5053 5054 \item "[[ etst vector-norm ( -1000 ) ; show true end show end test ]]" 5055 5056 \end{statements}" ]" 5057 5058 5059 5060 \subsection{vector-prefix} 5061 5062 "[ "\begin{statements} 5063 5064 \item "[[ etst vector-prefix ( show "abc" end show , -1 ) ; show "". end show end test ]]" 5065 5066 \item "[[ etst vector-prefix ( show "abc" end show , 0 ) ; show "". end show end test ]]" 5067 5068 \item "[[ etst vector-prefix ( show "abc" end show , 1 ) ; show "a" end show end test ]]" 5069 5070 \item "[[ etst vector-prefix ( show "abc" end show , 2 ) ; show "ab" end show end test ]]" 5071 5072 \item "[[ etst vector-prefix ( show "abc" end show , 3 ) ; show "abc" end show end test ]]" 5073 5074 \item "[[ etst vector-prefix ( show "abc" end show , 4 ) ; show "abc" end show end test ]]" 5075 5076 \item "[[ etst vector-prefix ( 97 + 98 * 256 + 2 * 65536 , -1 ) ; show "". end show end test ]]" 5077 5078 \item "[[ etst vector-prefix ( 97 + 98 * 256 + 2 * 65536 , 0 ) ; show "". end show end test ]]" 5079 5080 \item "[[ etst vector-prefix ( 97 + 98 * 256 + 2 * 65536 , 1 ) ; show "a" end show end test ]]" 5081 5082 \item "[[ etst vector-prefix ( 97 + 98 * 256 + 2 * 65536 , 2 ) ; show "ab" end show end test ]]" 5083 5084 \item "[[ etst vector-prefix ( 97 + 98 * 256 + 2 * 65536 , 3 ) ; show "ab" end show end test ]]" 5085 5086 \item "[[ etst vector-prefix ( -1000 , 3 ) ; show "". end show end test ]]" 5087 5088 \end{statements}" ]" 5089 5090 5091 5092 \subsection{vector-suffix} 5093 5094 "[ "\begin{statements} 5095 5096 \item "[[ etst vector-suffix ( show "abc" end show , -1 ) ; show "abc" end show end test ]]" 5097 5098 \item "[[ etst vector-suffix ( show "abc" end show , 0 ) ; show "abc" end show end test ]]" 5099 5100 \item "[[ etst vector-suffix ( show "abc" end show , 1 ) ; show "bc" end show end test ]]" 5101 5102 \item "[[ etst vector-suffix ( show "abc" end show , 2 ) ; show "c" end show end test ]]" 5103 5104 \item "[[ etst vector-suffix ( show "abc" end show , 3 ) ; show "". end show end test ]]" 5105 5106 \item "[[ etst vector-suffix ( show "abc" end show , 4 ) ; show "". end show end test ]]" 5107 5108 \item "[[ etst vector-suffix ( 97 + 98 * 256 + 2 * 65536 , -1 ) ; show "ab" end show end test ]]" 5109 5110 \item "[[ etst vector-suffix ( 97 + 98 * 256 + 2 * 65536 , 0 ) ; show "ab" end show end test ]]" 5111 5112 \item "[[ etst vector-suffix ( 97 + 98 * 256 + 2 * 65536 , 1 ) ; show "b" end show end test ]]" 5113 5114 \item "[[ etst vector-suffix ( 97 + 98 * 256 + 2 * 65536 , 2 ) ; show "". end show end test ]]" 5115 5116 \item "[[ etst vector-suffix ( 97 + 98 * 256 + 2 * 65536 , 3 ) ; show "". end show end test ]]" 5117 5118 \item "[[ etst vector-suffix ( -1000 , 0 ) ; show "". end show end test ]]" 5119 5120 \end{statements}" ]" 5121 5122 5123 5124 \subsection{vector-subseq} 5125 5126 "[ "\begin{statements} 5127 5128 \item "[[ etst vector-subseq ( show "ab" end show , -1 , -1 ) ; show "". end show end test ]]" 5129 5130 \item "[[ etst vector-subseq ( show "ab" end show , -1 , 0 ) ; show "". end show end test ]]" 5131 5132 \item "[[ etst vector-subseq ( show "ab" end show , -1 , 1 ) ; show "a" end show end test ]]" 5133 5134 \item "[[ etst vector-subseq ( show "ab" end show , -1 , 2 ) ; show "ab" end show end test ]]" 5135 5136 \item "[[ etst vector-subseq ( show "ab" end show , -1 , 3 ) ; show "ab" end show end test ]]" 5137 5138 \item "[[ etst vector-subseq ( show "ab" end show , 0 , -1 ) ; show "". end show end test ]]" 5139 5140 \item "[[ etst vector-subseq ( show "ab" end show , 0 , 0 ) ; show "". end show end test ]]" 5141 5142 \item "[[ etst vector-subseq ( show "ab" end show , 0 , 1 ) ; show "a" end show end test ]]" 5143 5144 \item "[[ etst vector-subseq ( show "ab" end show , 0 , 2 ) ; show "ab" end show end test ]]" 5145 5146 \item "[[ etst vector-subseq ( show "ab" end show , 0 , 3 ) ; show "ab" end show end test ]]" 5147 5148 \item "[[ etst vector-subseq ( show "ab" end show , 1 , -1 ) ; show "". end show end test ]]" 5149 5150 \item "[[ etst vector-subseq ( show "ab" end show , 1 , 0 ) ; show "". end show end test ]]" 5151 5152 \item "[[ etst vector-subseq ( show "ab" end show , 1 , 1 ) ; show "". end show end test ]]" 5153 5154 \item "[[ etst vector-subseq ( show "ab" end show , 1 , 2 ) ; show "b" end show end test ]]" 5155 5156 \item "[[ etst vector-subseq ( show "ab" end show , 1 , 3 ) ; show "b" end show end test ]]" 5157 5158 \item "[[ etst vector-subseq ( show "ab" end show , 2 , -1 ) ; show "". end show end test ]]" 5159 5160 \item "[[ etst vector-subseq ( show "ab" end show , 2 , 0 ) ; show "". end show end test ]]" 5161 5162 \item "[[ etst vector-subseq ( show "ab" end show , 2 , 1 ) ; show "". end show end test ]]" 5163 5164 \item "[[ etst vector-subseq ( show "ab" end show , 2 , 2 ) ; show "". end show end test ]]" 5165 5166 \item "[[ etst vector-subseq ( show "ab" end show , 2 , 3 ) ; show "". end show end test ]]" 5167 5168 \item "[[ etst vector-subseq ( show "ab" end show , 3 , -1 ) ; show "". end show end test ]]" 5169 5170 \item "[[ etst vector-subseq ( show "ab" end show , 3 , 0 ) ; show "". end show end test ]]" 5171 5172 \item "[[ etst vector-subseq ( show "ab" end show , 3 , 1 ) ; show "". end show end test ]]" 5173 5174 \item "[[ etst vector-subseq ( show "ab" end show , 3 , 2 ) ; show "". end show end test ]]" 5175 5176 \item "[[ etst vector-subseq ( show "ab" end show , 3 , 3 ) ; show "". end show end test ]]" 5177 5178 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , -1 , -1 ) ; show "". end show end test ]]" 5179 5180 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , -1 , 0 ) ; show "". end show end test ]]" 5181 5182 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , -1 , 1 ) ; show "a" end show end test ]]" 5183 5184 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , -1 , 2 ) ; show "ab" end show end test ]]" 5185 5186 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , -1 , 3 ) ; show "ab" end show end test ]]" 5187 5188 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 0 , -1 ) ; show "". end show end test ]]" 5189 5190 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 0 , 0 ) ; show "". end show end test ]]" 5191 5192 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 0 , 1 ) ; show "a" end show end test ]]" 5193 5194 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 0 , 2 ) ; show "ab" end show end test ]]" 5195 5196 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 0 , 3 ) ; show "ab" end show end test ]]" 5197 5198 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 1 , -1 ) ; show "". end show end test ]]" 5199 5200 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 1 , 0 ) ; show "". end show end test ]]" 5201 5202 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 1 , 1 ) ; show "". end show end test ]]" 5203 5204 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 1 , 2 ) ; show "b" end show end test ]]" 5205 5206 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 1 , 3 ) ; show "b" end show end test ]]" 5207 5208 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 2 , -1 ) ; show "". end show end test ]]" 5209 5210 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 2 , 0 ) ; show "". end show end test ]]" 5211 5212 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 2 , 1 ) ; show "". end show end test ]]" 5213 5214 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 2 , 2 ) ; show "". end show end test ]]" 5215 5216 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 2 , 3 ) ; show "". end show end test ]]" 5217 5218 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 3 , -1 ) ; show "". end show end test ]]" 5219 5220 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 3 , 0 ) ; show "". end show end test ]]" 5221 5222 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 3 , 1 ) ; show "". end show end test ]]" 5223 5224 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 3 , 2 ) ; show "". end show end test ]]" 5225 5226 \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 3 , 3 ) ; show "". end show end test ]]" 5227 5228 \item "[[ etst vector-subseq ( -1000 , 0 , 3 ) ; show "". end show end test ]]" 5229 5230 \end{statements}" ]" 5231 5232 5233 5234 \subsection{vector-length} 5235 5236 "[ "\begin{statements} 5237 5238 \item "[[ etst vector-length ( show "". end show ) ; 0 end test ]]" 5239 5240 \item "[[ etst vector-length ( show "a" end show ) ; 1 end test ]]" 5241 5242 \item "[[ etst vector-length ( show "abc" end show ) ; 3 end test ]]" 5243 5244 \item "[[ etst vector-length ( 97 + 98 * 256 + 2 * 65536 ) ; 2 end test ]]" 5245 5246 \item "[[ etst vector-length ( -1000 ) ; 0 end test ]]" 5247 5248 \end{statements}" ]" 5249 5250 5251 5252 \subsection{vector-index} 5253 5254 "[ "\begin{statements} 5255 5256 \item "[[ etst vector-index ( show "abc" end show , -1 ) ; exception end test ]]" 5257 5258 \item "[[ etst vector-index ( show "abc" end show , 0 ) ; 97 end test ]]" 5259 5260 \item "[[ etst vector-index ( show "abc" end show , 1 ) ; 98 end test ]]" 5261 5262 \item "[[ etst vector-index ( show "abc" end show , 2 ) ; 99 end test ]]" 5263 5264 \item "[[ etst vector-index ( show "abc" end show , 3 ) ; exception end test ]]" 5265 5266 \item "[[ etst vector-index ( show "". end show , -1 ) ; exception end test ]]" 5267 5268 \item "[[ etst vector-index ( show "". end show , 0 ) ; exception end test ]]" 5269 5270 \item "[[ etst vector-index ( 97 + 98 * 256 + 2 * 65536 , -1 ) ; exception end test ]]" 5271 5272 \item "[[ etst vector-index ( 97 + 98 * 256 + 2 * 65536 , 0 ) ; 97 end test ]]" 5273 5274 \item "[[ etst vector-index ( 97 + 98 * 256 + 2 * 65536 , 1 ) ; 98 end test ]]" 5275 5276 \item "[[ etst vector-index ( 97 + 98 * 256 + 2 * 65536 , 2 ) ; exception end test ]]" 5277 5278 \end{statements}" ]" 5279 5280 5281 5282 \subsection{vector-head and vector-tail} 5283 5284 "[ "\begin{statements} 5285 5286 \item "[[ etst vector-head ( show "ABC" end show ) ; 65 end test ]]" 5287 5288 \item "[[ etst vector-tail ( show "ABC" end show ) ; show "BC" end show end test ]]" 5289 5290 \end{statements}" ]" 5291 5292 5293 5294 \subsection{vector2byte*} 5295 5296 "[ "\begin{statements} 5297 5298 \item "[[ etst vector2byte* ( show "". end show ) ; <<>> end test ]]" 5299 5300 \item "[[ etst vector2byte* ( show "A" end show ) ; << 65 >> end test ]]" 5301 5302 \item "[[ etst vector2byte* ( show "ABC" end show ) ; << 65 ,, 66 ,, 67 >> end test ]]" 5303 5304 \end{statements}" ]" 5305 5306 5307 5308 \subsection{vector2vector*} 5309 5310 "[ "\begin{statements} 5311 5312 \item "[[ etst vector2vector* ( show "". end show ) ; <<>> end test ]]" 5313 5314 \item "[[ etst vector2vector* ( show "A" end show ) ; << "A" >> end test ]]" 5315 5316 \item "[[ etst vector2vector* ( show "ABC" end show ) ; << "A" ,, "B" ,, "C" >> end test ]]" 5317 5318 \end{statements}" ]" 5319 5320 5321 5322 \subsection{bt2byte*} 5323 5324 "[ "\begin{statements} 5325 5326 \item "[[ etst bt2byte* ( 65 ) ; << 65 >> end test ]]" 5327 5328 \item "[[ etst bt2byte* ( -1 ) ; <<>> end test ]]" 5329 5330 \item "[[ etst bt2byte* ( 256 ) ; <<>> end test ]]" 5331 5332 \item "[[ etst bt2byte* ( true ) ; <<>> end test ]]" 5333 5334 \item "[[ etst bt2byte* ( false ) ; <<>> end test ]]" 5335 5336 \item "[[ etst bt2byte* ( map ( \ x . x ) ) ; <<>> end test ]]" 5337 5338 \item "[[ etst bt2byte* ( 65 :: 66 ) ; << 65 ,, 66 >> end test ]]" 5339 5340 \item "[[ etst bt2byte* ( ( 65 :: 66 ) :: ( 67 :: 68 ) ) ; << 65 ,, 66 ,, 67 ,, 68 >> end test ]]" 5341 5342 \item "[[ etst bt2byte* ( ( 65 :: 66 ) :: true :: 67 :: false :: 68 ) ; << 65 ,, 66 ,, 67 ,, 68 >> end test ]]" 5343 5344 \end{statements}" ]" 5345 5346 5347 5348 \subsection{bt2vector*} 5349 5350 "[ "\begin{statements} 5351 5352 \item "[[ etst bt2vector* ( 65 ) ; << 65 + 256 >> end test ]]" 5353 5354 \item "[[ etst bt2vector* ( -1 ) ; <<>> end test ]]" 5355 5356 \item "[[ etst bt2vector* ( 256 ) ; <<>> end test ]]" 5357 5358 \item "[[ etst bt2vector* ( true ) ; <<>> end test ]]" 5359 5360 \item "[[ etst bt2vector* ( false ) ; <<>> end test ]]" 5361 5362 \item "[[ etst bt2vector* ( map ( \ x . x ) ) ; <<>> end test ]]" 5363 5364 \item "[[ etst bt2vector* ( 65 :: 66 ) ; << "A" ,, "B" >> end test ]]" 5365 5366 \item "[[ etst bt2vector* ( ( 65 :: 66 ) :: ( 67 :: 68 ) ) ; << "A" ,, "B" ,, "C" ,, "D" >> end test ]]" 5367 5368 \item "[[ etst bt2vector* ( ( 65 :: 66 ) :: true :: 67 :: false :: 68 ) ; << "A" ,, "B" ,, "C" ,, "D" >> end test ]]" 5369 5370 \end{statements}" ]" 5371 5372 5373 5374 \subsection{bt2vector} 5375 5376 "[ "\begin{statements} 5377 5378 \item "[[ etst bt2vector ( 65 ) ; show "A" end show end test ]]" 5379 5380 \item "[[ etst bt2vector ( -1 ) ; show "". end show end test ]]" 5381 5382 \item "[[ etst bt2vector ( 256 ) ; show "". end show end test ]]" 5383 5384 \item "[[ etst bt2vector ( true ) ; show "". end show end test ]]" 5385 5386 \item "[[ etst bt2vector ( false ) ; show "". end show end test ]]" 5387 5388 \item "[[ etst bt2vector ( map ( \ x . x ) ) ; show "". end show end test ]]" 5389 5390 \item "[[ etst bt2vector ( 65 :: 66 ) ; show "AB" end show end test ]]" 5391 5392 \item "[[ etst bt2vector ( ( 65 :: 66 ) :: ( 67 :: 68 ) ) ; show "ABCD" end show end test ]]" 5393 5394 \item "[[ etst bt2vector ( ( 65 :: 66 ) :: true :: 67 :: false :: 68 ) ; show "ABCD" end show end test ]]" 5395 5396 \end{statements}" ]" 5397 5398 5399 5400 \subsection{vt2byte*} 5401 5402 "[ "\begin{statements} 5403 5404 \item "[[ etst vt2byte* ( show "". end show ) ; <<>> end test ]]" 5405 5406 \item "[[ etst vt2byte* ( show "A" end show ) ; << 65 >> end test ]]" 5407 5408 \item "[[ etst vt2byte* ( show "AB" end show ) ; << 65 ,, 66 >> end test ]]" 5409 5410 \item "[[ etst vt2byte* ( -1 ) ; <<>> end test ]]" 5411 5412 \item "[[ etst vt2byte* ( 65 + 2 * 256 ) ; << 65 >> end test ]]" 5413 5414 \item "[[ etst vt2byte* ( true ) ; <<>> end test ]]" 5415 5416 \item "[[ etst vt2byte* ( false ) ; <<>> end test ]]" 5417 5418 \item "[[ etst vt2byte* ( map ( \ x . x ) ) ; <<>> end test ]]" 5419 5420 \item "[[ etst vt2byte* ( show "AB" end show :: "CD" ) ; << 65 ,, 66 ,, 67 ,, 68 >> end test ]]" 5421 5422 \item "[[ etst vt2byte* ( ( show "A" end show :: show "B" end show ) :: ( show "C" end show :: "D" ) ) ; << 65 ,, 66 ,, 67 ,, 68 >> end test ]]" 5423 5424 \item "[[ etst vt2byte* ( ( show "AB" end show :: show "C" end show ) :: map ( \ x . x ) :: true :: show "". end show :: "D" ) ; << 65 ,, 66 ,, 67 ,, 68 >> end test ]]" 5425 5426 \end{statements}" ]" 5427 5428 5429 5430 \subsection{vt2vector*} 5431 5432 "[ "\begin{statements} 5433 5434 \item "[[ etst vt2vector* ( show "". end show ) ; <<>> end test ]]" 5435 5436 \item "[[ etst vt2vector* ( show "A" end show ) ; << "A" >> end test ]]" 5437 5438 \item "[[ etst vt2vector* ( show "AB" end show ) ; << "A" ,, "B" >> end test ]]" 5439 5440 \item "[[ etst vt2vector* ( -1 ) ; <<>> end test ]]" 5441 5442 \item "[[ etst vt2vector* ( 65 + 2 * 256 ) ; << "A" >> end test ]]" 5443 5444 \item "[[ etst vt2vector* ( true ) ; <<>> end test ]]" 5445 5446 \item "[[ etst vt2vector* ( false ) ; <<>> end test ]]" 5447 5448 \item "[[ etst vt2vector* ( map ( \ x . x ) ) ; <<>> end test ]]" 5449 5450 \item "[[ etst vt2vector* ( show "AB" end show :: "CD" ) ; << "A" ,, "B" ,, "C" ,, "D" >> end test ]]" 5451 5452 \item "[[ etst vt2vector* ( ( show "A" end show :: show "B" end show ) :: ( show "C" end show :: "D" ) ) ; << "A" ,, "B" ,, "C" ,, "D" >> end test ]]" 5453 5454 \item "[[ etst vt2vector* ( ( show "AB" end show :: show "C" end show ) :: map ( \ x . x ) :: true :: show "". end show :: "D" ) ; << "A" ,, "B" ,, "C" ,, "D" >> end test ]]" 5455 5456 \end{statements}" ]" 5457 5458 5459 5460 \subsection{vt2vector} 5461 5462 "[ "\begin{statements} 5463 5464 \item "[[ etst vt2vector ( show "". end show ) ; show "". end show end test ]]" 5465 5466 \item "[[ etst vt2vector ( show "A" end show ) ; show "A" end show end test ]]" 5467 5468 \item "[[ etst vt2vector ( show "AB" end show ) ; show "AB" end show end test ]]" 5469 5470 \item "[[ etst vt2vector ( -1 ) ; show "". end show end test ]]" 5471 5472 \item "[[ etst vt2vector ( 65 + 2 * 256 ) ; show "A" end show end test ]]" 5473 5474 \item "[[ etst vt2vector ( true ) ; show "". end show end test ]]" 5475 5476 \item "[[ etst vt2vector ( false ) ; show "". end show end test ]]" 5477 5478 \item "[[ etst vt2vector ( map ( \ x . x ) ) ; show "". end show end test ]]" 5479 5480 \item "[[ etst vt2vector ( show "AB" end show :: "CD" ) ; show "ABCD" end show end test ]]" 5481 5482 \item "[[ etst vt2vector ( ( show "A" end show :: show "B" end show ) :: ( show "C" end show :: "D" ) ) ; show "ABCD" end show end test ]]" 5483 5484 \item "[[ etst vt2vector ( ( show "AB" end show :: show "C" end show ) :: map ( \ x . x ) :: true :: show "". end show :: "D" ) ; show "ABCD" end show end test ]]" 5485 5486 \end{statements}" ]" 5487 5488 5489 5490 \section{Structures} 5491 5492 \subsection{List access} 5493 5494 "[ "\begin{statements} 5495 5496 \item "[[ ttst 2 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) zeroth end test ]]" 5497 5498 \item "[[ ttst 3 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) first end test ]]" 5499 5500 \item "[[ ttst 4 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) second end test ]]" 5501 5502 \item "[[ ttst 5 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) third end test ]]" 5503 5504 \item "[[ ttst 6 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) fourth end test ]]" 5505 5506 \item "[[ ttst 7 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) fifth end test ]]" 5507 5508 \item "[[ ttst 8 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) sixth end test ]]" 5509 5510 \item "[[ ttst 9 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) seventh end test ]]" 5511 5512 \item "[[ ttst 0 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) eighth end test ]]" 5513 5514 \item "[[ ttst 1 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) ninth end test ]]" 5515 5516 \end{statements}" ]" 5517 5518 5519 5520 \subsection{Tree access} 5521 5522 "[ "\begin{statements} 5523 5524 \item "[[ ttst quote base end quote ref = quote x + y end quote ref end test ]]" 5525 5526 \item "[[ ttst quote base end quote idx = 0 end test ]]" 5527 5528 \item "[[ ttst quote "abc" end quote ref = 0 end test ]]" 5529 5530 \item "[[ ttst quote "abc" end quote idx = "abc" end test ]]" 5531 5532 \end{statements}" ]" 5533 5534 5535 5536 \subsection{Tree equality} 5537 5538 "[ "\begin{statements} 5539 5540 \item "[[ ttst quote x + y end quote t= quote x + y end quote end test ]]" 5541 5542 \item "[[ ftst quote x + y end quote t= quote z + y end quote end test ]]" 5543 5544 \item "[[ ftst quote x + y end quote t= quote x + z end quote end test ]]" 5545 5546 \item "[[ ftst quote x + y end quote t= quote x - y end quote end test ]]" 5547 5548 \item "[[ ttst 1 = lookup ( quote x end quote , 5549 ( quote x end quote :: 1 ) :: 5550 ( quote y _ { 1 } end quote :: 2 ) :: 5551 ( quote y _ { 2 } end quote :: 3 ) :: true , 5552 true ) end test ]]" 5553 5554 \item "[[ ttst 2 = lookup ( quote y _ { 1 } end quote , 5555 ( quote x end quote :: 1 ) :: 5556 ( quote y _ { 1 } end quote :: 2 ) :: 5557 ( quote y _ { 2 } end quote :: 3 ) :: true , 5558 true ) end test ]]" 5559 5560 \item "[[ ttst 3 = lookup ( quote y _ { 2 } end quote , 5561 ( quote x end quote :: 1 ) :: 5562 ( quote y _ { 1 } end quote :: 2 ) :: 5563 ( quote y _ { 2 } end quote :: 3 ) :: true , 5564 true ) end test ]]" 5565 5566 \item "[[ ttst true = lookup ( quote y _ { 3 } end quote , 5567 ( quote x end quote :: 1 ) :: 5568 ( quote y _ { 1 } end quote :: 2 ) :: 5569 ( quote y _ { 2 } end quote :: 3 ) :: true , 5570 true ) end test ]]" 5571 5572 \item "[[ ttst false = lookup ( quote y _ { 3 } end quote , 5573 ( quote x end quote :: 1 ) :: 5574 ( quote y _ { 1 } end quote :: 2 ) :: 5575 ( quote y _ { 2 } end quote :: 3 ) :: true , 5576 false ) end test ]]" 5577 5578 \end{statements}" ]" 5579 5580 5581 5582 \subsection{Arrays} 5583 5584 "[ "\begin{statements} 5585 5586 \item "[[ ttst true [[ 2 ]] end test ]]" 5587 5588 \item "[[ ttst 12 = true [[ 2 -> 12 ]] [[ 2 ]] end test ]]" 5589 5590 \item "[[ ttst true [[ 2 -> 12 ]] [[ 3 ]] end test ]]" 5591 5592 \item "[[ ttst 12 = true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 2 ]] end test ]]" 5593 5594 \item "[[ ttst 13 = true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 3 ]] end test ]]" 5595 5596 \item "[[ ttst true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 4 ]] end test ]]" 5597 5598 \item "[[ ttst 12 = true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 10 -> 14 ]] [[ 2 ]] end test ]]" 5599 5600 \item "[[ ttst 13 = true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 10 -> 14 ]] [[ 3 ]] end test ]]" 5601 5602 \item "[[ ttst 14 = true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 10 -> 14 ]] [[ 10 ]] end test ]]" 5603 5604 \item "[[ ttst true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 10 -> 14 ]] [[ 5 ]] end test ]]" 5605 5606 \item "[[ ttst true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 10 -> 14 ]] [[ 2 -> true ]] = true [[ 10 -> 14 ]] [[ 3 -> 13 ]] end test ]]" 5607 5608 \item "[[ etst true [[ 2 :: 3 :: 4 :: true => 5 ]] [[ 2 :: 4 :: true => 6 ]] [[ 2 ]] [[ 3 ]] [[ 4 ]] ; 5 end test ]]" 5609 5610 \item "[[ etst true [[ 2 :: 3 :: 4 :: true => 5 ]] [[ 2 :: 4 :: true => 6 ]] [[ 2 ]] [[ 4 ]] ; 6 end test ]]" 5611 5612 \item "[[ etst true [[ 2 :: 3 :: 4 :: true => 5 ]] [[ 2 :: 4 :: true => 6 ]] [[ 2 ]] [[ 5 ]] ; true end test ]]" 5613 5614 \item "[[ etst true [[ "code" -> 3 ]] [[ "codex" -> 4 ]] [[ "code" ]] ; 3 end test ]]" 5615 5616 \item "[[ etst true [[ "code" :: true => 3 ]] [[ "codex" :: true => 4 ]] [[ "code" ]] ; 3 end test ]]" 5617 5618 \item "[[ etst true [[ 1 :: "code" :: true => 3 ]] [[ 1 :: "codex" :: true => 4 ]] [[ 1 ]] [[ "code" ]] ; 3 end test ]]" 5619 5620 \item "[[ etst true [[ 1 :: "code" :: 2 :: true => 3 ]] [[ 1 :: "codex" :: 2 :: true => 4 ]] [[ 1 ]] [[ "code" ]] [[ 2 ]] ; 3 end test ]]" 5621 5622 \end{statements}" ]" 5623 5624 5625 5626 \section{Evaluation} 5627 5628 \subsection{The page symbol} 5629 5630 "[ "\begin{statements} 5631 5632 \item "[[ ttst base [[ 0 ]] = quote base end quote ref end test ]]" 5633 5634 \item "[[ ttst base [[ quote base end quote ref ]] [[ "vector" ]] intp end test ]]" 5635 5636 \item "[[ ttst base [[ quote base end quote ref ]] [[ "bibliography" ]] = quote base end quote ref :: true end test ]]" 5637 5638 \item "[[ ttst base [[ quote base end quote ref ]] [[ "dictionary" ]] [[ quote x + y end quote idx ]] = 2 end test ]]" 5639 5640 \item "[[ ttst base [[ quote base end quote ref ]] [[ "body" ]] pairp end test ]]" 5641 5642 \item "[[ ttst base [[ quote base end quote ref ]] [[ "codex" ]] [[ quote false end quote ref ]] [[ quote false end quote idx ]] [[ 0 ]] [[ "value" ]] t= hiding show quote optimized define value of false as true LazyPair true end define end quote end show end test ]]" 5643 5644 \item "[[ ttst base [[ quote base end quote ref ]] [[ "expansion" ]] pairp end test ]]" 5645 5646 \item "[[ ttst base [[ quote base end quote ref ]] [[ "code" ]] [[ quote x - y end quote idx ]] Tail ' 2 ' 3 = -1 end test ]]" 5647 5648 \item "[[ ttst base [[ quote base end quote ref ]] [[ "cluster" ]] = true end test ]]" 5649 5650 \item "[[ ttst base [[ quote base end quote ref ]] [[ "diagnose" ]] untag = true end test ]]" 5651 5652 \end{statements}" ]" 5653 5654 5655 5656 \subsection{eval} 5657 5658 "[ "\begin{statements} 5659 5660 \item "[[ ttst 2 = eval ( quote 2 end quote , true , base ) untag end test ]]" 5661 5662 \item "[[ ttst -1 = eval ( quote 2 - 3 end quote , true , base ) untag end test ]]" 5663 5664 \item "[[ ttst "abc" = eval ( quote "abc" end quote , true , base ) untag end test ]]" 5665 5666 \item "[[ ttst quote x + y end quote ref = eval ( quote base [[ 0 ]] end quote , true , base ) untag end test ]]" 5667 5668 \item "[[ ttst quote 2 - 3 end quote t= eval ( quote quote 2 - 3 end quote end quote , true , base ) untag end test ]]" 5669 5670 \item "[[ ttst -1 = eval ( quote \ x . x - 3 end quote , true , base ) Tail ' 2 end test ]]" 5671 5672 \item "[[ ttst -1 = eval ( quote ( \ x . x - 3 ) ' 2 end quote , true , base ) untag end test ]]" 5673 5674 \item "[[ ttst 6 = eval ( quote ( \ x . x ' x ) ' ( \ f . \ x . f ' ( f ' x ) ) ' ( \ x . x + 1 ) ' 2 end quote , true , base ) untag end test ]]" 5675 5676 \end{statements}" ]" 5677 5678 5679 5680 \section{Macro expansion} 5681 5682 \subsection{Parentheses} 5683 5684 "[ "\begin{statements} 5685 5686 \item "[[ ttst quote ( 2 ) end quote t= quote 2 end quote end test ]]" 5687 5688 \item "[[ ttst quote newline 2 end quote t= quote 2 end quote end test ]]" 5689 5690 \end{statements}" ]" 5691 5692 5693 5694 \subsection{Tuples} 5695 5696 "[ "\begin{statements} 5697 5698 \item "[[ ttst quote << 2 ,, 3 ,, 4 >> end quote t= quote 2 :: 3 :: 4 :: <<>> end quote end test ]]" 5699 5700 \end{statements}" ]" 5701 5702 5703 5704 \subsection{Eager definitions} 5705 5706 "[ "\begin{statements} 5707 5708 \item "[[ ttst hide quote eager define x + y as x * y end define end quote t= quote define value of x + y as norm x is val : y is val : x * y end define end quote end hide end test ]]" 5709 5710 \end{statements}" ]" 5711 5712 5713 5714 \subsection{Let} 5715 5716 "[ "\begin{statements} 5717 5718 \item "[[ ttst quote let 3 := 4 in 2 end quote t= quote 2 end quote end test ]]" 5719 5720 \item "[[ ttst quote let 3 := 4 in 3 end quote t= quote 4 end quote end test ]]" 5721 5722 \item "[[ ttst quote let 3 := 4 in 4 end quote t= quote 4 end quote end test ]]" 5723 5724 \item "[[ ttst make-var ( quote x end quote ) t= quote asterisk end quote end test ]]" 5725 5726 \item "[[ ttst make-let ( quote x end quote , quote y end quote , quote z end quote ) t= quote LET y BE x IN z end quote end test ]]" 5727 5728 \item "[[ ttst make-prime ( quote x end quote ) t= quote x prime end quote end test ]]" 5729 5730 \item "[[ ttst make-head ( quote x end quote ) t= quote x head end quote end test ]]" 5731 5732 \item "[[ ttst make-tail ( quote x end quote ) t= quote x tail end quote end test ]]" 5733 5734 \item "[[ ttst let1 ( protect quote let x = y in z end quote end protect :: macrostate0 :: self :: true ) t= quote LET y BE asterisk IN LET asterisk BE x IN z end quote end test ]]" 5735 5736 \item "[[ ttst let1 ( protect quote let 2 = y in z end quote end protect :: macrostate0 :: self :: true ) t= quote LET y BE asterisk IN z end quote end test ]]" 5737 5738 \item "[[ ttst let1 ( protect quote let u :: v = y in z end quote end protect :: macrostate0 :: self :: true ) t= quote newline 5739 5740 LET y BE asterisk IN newline 5741 5742 LET ( if asterisk atom then asterisk else asterisk head ) :: ( if asterisk atom then asterisk else asterisk tail ) :: true BE asterisk prime IN newline 5743 5744 LET asterisk prime head BE asterisk IN newline 5745 5746 LET asterisk prime tail BE asterisk prime IN newline 5747 5748 LET asterisk BE u IN newline 5749 5750 LET asterisk prime head BE asterisk IN newline 5751 5752 LET asterisk prime tail BE asterisk prime IN newline 5753 5754 LET asterisk BE v IN z end quote end test ]]" 5755 5756 \item "[[ ttst quote let x = y in z end quote t= quote LET y BE asterisk IN LET asterisk BE x IN z end quote end test ]]" 5757 5758 \item "[[ ttst quote let 2 = y in z end quote t= quote LET y BE asterisk IN z end quote end test ]]" 5759 5760 \item "[[ ttst quote let u :: v = y in z end quote t= quote newline 5761 5762 LET y BE asterisk IN newline 5763 5764 LET ( if asterisk atom then asterisk else asterisk head ) :: ( if asterisk atom then asterisk else asterisk tail ) :: true BE asterisk prime IN newline 5765 5766 LET asterisk prime head BE asterisk IN newline 5767 5768 LET asterisk prime tail BE asterisk prime IN newline 5769 5770 LET asterisk BE u IN newline 5771 5772 LET asterisk prime head BE asterisk IN newline 5773 5774 LET asterisk prime tail BE asterisk prime IN newline 5775 5776 LET asterisk BE v IN z end quote end test ]]" 5777 5778 \item "[[ etst let u = 2 in u ; 2 end test ]]" 5779 5780 \item "[[ etst let u :: v = 2 in u ; 2 end test ]]" 5781 5782 \item "[[ etst let u :: v = 2 in v ; 2 end test ]]" 5783 5784 \item "[[ etst let u :: v = 3 in v ; 3 end test ]]" 5785 5786 \item "[[ etst let u :: v = 2 :: 3 in u ; 2 end test ]]" 5787 5788 \item "[[ etst let u :: v = 2 :: 3 in v ; 3 end test ]]" 5789 5790 \item "[[ etst let u :: v = 2 :: 3 in 4 ; 4 end test ]]" 5791 5792 \item "[[ etst let ( u ) = 2 in u ; 2 end test ]]" 5793 5794 \item "[[ etst let ( ( u :: v ) :: ( w :: x ) ) = ( ( 1 :: 2 ) :: ( 3 :: 4 ) ) in u ; 1 end test ]]" 5795 5796 \item "[[ etst let ( ( u :: v ) :: ( w :: x ) ) = ( ( 1 :: 2 ) :: ( 3 :: 4 ) ) in v ; 2 end test ]]" 5797 5798 \item "[[ etst let ( ( u :: v ) :: ( w :: x ) ) = ( ( 1 :: 2 ) :: ( 3 :: 4 ) ) in w ; 3 end test ]]" 5799 5800 \item "[[ etst let ( ( u :: v ) :: ( w :: x ) ) = ( ( 1 :: 2 ) :: ( 3 :: 4 ) ) in x ; 4 end test ]]" 5801 5802 \item "[[ etst let << u ,, v ,, w >> = << 1 ,, 2 ,, 3 >> in << v ,, w ,, u >> ; << 2 ,, 3 ,, 1 >> end test ]]" 5803 5804 \end{statements}" ]" 5805 5806 5807 5808 \subsection{Backquote} 5809 5810 "[ "\begin{statements} 5811 5812 \item "[[ ttst make-pair ( 1 , quote 2 end quote , quote 3 end quote ) t= quote 2 :: 3 end quote end test ]]" 5813 5814 \item "[[ ttst make-quote ( 1 , quote 2 end quote ) t= quote quote 2 end quote end quote end test ]]" 5815 5816 \item "[[ ttst make-make-root ( 1 , quote 2 end quote , quote 3 end quote ) t= quote make-root ( 2 , 3 ) end quote end test ]]" 5817 5818 \item "[[ ttst backquote2 ( ( true :: true :: 1 ) :: true , ( 2 :: 3 :: true ) :: true , ( 4 :: 5 :: true ) :: true , macrostate0 , self ) = 5819 ( ( quote true :: true end quote ref :: 5820 quote true :: true end quote idx :: 1 ) :: 5821 ( ( quote make-root ( true , true ) end quote ref :: 5822 quote make-root ( true , true ) end quote idx :: 1 ) :: 5823 ( ( 2 :: 3 :: true ) :: true ) :: 5824 ( ( quote quote true end quote end quote ref :: 5825 quote quote true end quote end quote idx :: 1 ) :: 5826 ( ( 4 :: 5 :: true ) :: true ) :: 5827 true ) :: 5828 true ) :: 5829 ( ( quote true end quote ref :: 5830 quote true end quote idx :: 1 ) :: 5831 true ) :: 5832 true ) end test ]]" 5833 5834 \item "[[ ttst backquote2 ( quote 1 end quote , quote 2 end quote , quote 3 end quote , macrostate0 , self ) t= quote make-root ( 2 , quote 3 end quote ) :: true end quote end test ]]" 5835 5836 \item "[[ ttst backquote2 ( quote 1 end quote , quote 2 end quote , quote 3 unquote end quote , macrostate0 , self ) t= quote 3 end quote end test ]]" 5837 5838 \item "[[ ttst quote back 2 quote 3 end quote end quote t= quote make-root ( 2 , quote 3 end quote ) :: true end quote end test ]]" 5839 5840 \item "[[ ttst quote back 2 quote quote 3 end quote unquote end quote end quote t= quote quote 3 end quote end quote end test ]]" 5841 5842 \item "[[ ttst back quote 2 end quote quote 3 end quote t= quote 3 end quote end test ]]" 5843 5844 \item "[[ ttst back quote 2 end quote quote quote 3 end quote unquote end quote t= quote 3 end quote end test ]]" 5845 5846 \item "[[ ttst let x = quote 3 end quote in back quote 2 end quote quote x unquote end quote t= quote 3 end quote end test ]]" 5847 5848 \item "[[ ttst back quote 2 end quote quote 3 + 4 end quote t= quote 3 + 4 end quote end test ]]" 5849 5850 \item "[[ ttst back quote 2 end quote quote 3 + 4 end quote t= quote 3 + 4 end quote end test ]]" 5851 5852 \item "[[ ttst LET x BE quote 1 end quote IN LET y BE quote 2 end quote IN back x quote 3 + 4 end quote t= quote 3 + 4 end quote end test ]]" 5853 5854 \item "[[ ttst let x = quote 1 end quote in let y = quote 2 end quote in back x quote y unquote + 4 end quote t= quote 2 + 4 end quote end test ]]" 5855 5856 \item "[[ ttst let x = quote 1 end quote in let y = quote 2 end quote in back x quote 3 + y unquote end quote t= quote 3 + 2 end quote end test ]]" 5857 5858 \item "[[ ttst let x = quote 1 end quote in let y = quote 2 end quote in back x quote 3 + y unquote end quote debug = x debug end test ]]" 5859 5860 \end{statements}" ]" 5861 5862 5863 5864 \section{Proof checking} 5865 5866 \subsection{Term sets} 5867 5868 "[ "\begin{statements} 5869 5870 \item "[[ ttst quote 2 end quote member << quote 2 end quote ,, quote 3 end quote >> end test ]]" 5871 5872 \item "[[ ttst quote 3 end quote member << quote 2 end quote ,, quote 3 end quote >> end test ]]" 5873 5874 \item "[[ ftst quote 4 end quote member << quote 2 end quote ,, quote 3 end quote >> end test ]]" 5875 5876 \item "[[ ttst << quote 2 end quote ,, quote 3 end quote >> set+ quote 2 end quote t=* << quote 2 end quote ,, quote 3 end quote >> end test ]]" 5877 5878 \item "[[ ttst << quote 2 end quote ,, quote 3 end quote >> set+ quote 3 end quote t=* << quote 2 end quote ,, quote 3 end quote >> end test ]]" 5879 5880 \item "[[ ttst << quote 2 end quote ,, quote 3 end quote >> set+ quote 4 end quote t=* << quote 4 end quote ,, quote 2 end quote ,, quote 3 end quote >> end test ]]" 5881 5882 \item "[[ ttst << quote 2 end quote ,, quote 3 end quote >> set- quote 2 end quote t=* << quote 3 end quote >> end test ]]" 5883 5884 \item "[[ ttst << quote 2 end quote ,, quote 3 end quote >> set- quote 3 end quote t=* << quote 2 end quote >> end test ]]" 5885 5886 \item "[[ ttst << quote 2 end quote ,, quote 3 end quote >> set- quote 4 end quote t=* << quote 2 end quote ,, quote 3 end quote >> end test ]]" 5887 5888 \item "[[ ttst << 1 ,, 2 ,, 3 >> union << 4 ,, 2 >> = << 3 ,, 1 ,, 4 ,, 2 >> end test ]]" 5889 5890 \item "[[ ttst << quote 1 end quote ,, quote 2 end quote ,, quote 3 end quote >> set= << quote 3 end quote ,, quote 1 end quote ,, quote 2 end quote >> end test ]]" 5891 5892 \item "[[ ftst << quote 1 end quote ,, quote 2 end quote ,, quote 3 end quote >> set= << quote 3 end quote ,, quote 1 end quote >> end test ]]" 5893 5894 \end{statements}" ]" 5895 5896 5897 5898 \subsection{Meta variables} 5899 5900 "[ "\begin{statements} 5901 5902 \item "[[ ttst quote #a end quote metavar ( self ) end test ]]" 5903 5904 \item "[[ ftst quote x end quote metavar ( self ) end test ]]" 5905 5906 \end{statements}" ]" 5907 5908 5909 5910 \subsection{Object terms} 5911 5912 "[ "\begin{statements} 5913 5914 \item "[[ ttst quote #a end quote objectterm ( self ) end test ]]" 5915 5916 \item "[[ ftst quote #a infer #b end quote objectterm ( self ) end test ]]" 5917 5918 \item "[[ ttst quote x end quote objectterm ( self ) end test ]]" 5919 5920 \item "[[ ttst quote x _ { y infer z } end quote objectterm ( self ) end test ]]" 5921 5922 \item "[[ ttst quote quote x infer y end quote end quote objectterm ( self ) end test ]]" 5923 5924 \item "[[ ttst quote \ x . y end quote objectterm ( self ) end test ]]" 5925 5926 \item "[[ ftst quote \ x . ( y infer z ) end quote objectterm ( self ) end test ]]" 5927 5928 \item "[[ ftst quote \ ( x infer y ) . z end quote objectterm ( self ) end test ]]" 5929 5930 \item "[[ ttst quote x + y end quote objectterm ( self ) end test ]]" 5931 5932 \item "[[ ftst quote ( x infer y ) + z end quote objectterm ( self ) end test ]]" 5933 5934 \item "[[ ftst quote 1 + ( x infer y ) end quote objectterm ( self ) end test ]]" 5935 5936 \end{statements}" ]" 5937 5938 5939 5940 \subsection{Meta terms} 5941 5942 "[ "\begin{statements} 5943 5944 \item "[[ ttst quote #a end quote metaterm ( self ) end test ]]" 5945 5946 \item "[[ ttst quote #a infer #b end quote metaterm ( self ) end test ]]" 5947 5948 \item "[[ ttst quote x end quote metaterm ( self ) end test ]]" 5949 5950 \item "[[ ttst quote x _ { y infer z } end quote metaterm ( self ) end test ]]" 5951 5952 \item "[[ ttst quote quote x infer y end quote end quote metaterm ( self ) end test ]]" 5953 5954 \item "[[ ttst quote \ x . y end quote metaterm ( self ) end test ]]" 5955 5956 \item "[[ ftst quote \ x . ( y infer z ) end quote metaterm ( self ) end test ]]" 5957 5958 \item "[[ ftst quote \ ( x infer y ) . z end quote metaterm ( self ) end test ]]" 5959 5960 \item "[[ ftst quote \ 2 . z end quote metaterm ( self ) end test ]]" 5961 5962 \item "[[ ttst quote x + y end quote metaterm ( self ) end test ]]" 5963 5964 \item "[[ ftst quote ( x infer y ) + z end quote metaterm ( self ) end test ]]" 5965 5966 \item "[[ ftst quote 1 + ( x infer y ) end quote metaterm ( self ) end test ]]" 5967 5968 \item "[[ ttst quote ( #a infer x ) infer ( 1 infer 2 ) end quote metaterm ( self ) end test ]]" 5969 5970 \item "[[ ttst quote ( 1 + 2 + 3 ) infer ( 4 + 5 + 6 ) end quote metaterm ( self ) end test ]]" 5971 5972 \item "[[ ftst quote ( ( 1 infer 2 ) + 3 ) infer ( 4 + 5 + 6 ) end quote metaterm ( self ) end test ]]" 5973 5974 \item "[[ ftst quote ( 1 + ( 2 infer 3 ) ) infer ( 4 + 5 + 6 ) end quote metaterm ( self ) end test ]]" 5975 5976 \item "[[ ftst quote ( 1 + 2 + 3 ) infer ( ( 4 infer 5 ) + 6 ) end quote metaterm ( self ) end test ]]" 5977 5978 \item "[[ ftst quote ( 1 + 2 + 3 ) infer ( 4 + ( 5 infer 6 ) ) end quote metaterm ( self ) end test ]]" 5979 5980 \item "[[ ttst quote All #a : #a infer #a end quote metaterm ( self ) end test ]]" 5981 5982 \item "[[ ftst quote All ( 1 infer 2 ) + 3 : 4 end quote metaterm ( self ) end test ]]" 5983 5984 \item "[[ ftst quote All 1 : ( 2 infer 3 ) + 4 end quote metaterm ( self ) end test ]]" 5985 5986 \end{statements}" ]" 5987 5988 5989 5990 \subsection{Avoidance} 5991 5992 "[ "\begin{statements} 5993 5994 \item "[[ ftst quote #a end quote metaavoid ( self ) quote #a end quote end test ]]" 5995 5996 \item "[[ ttst quote #a end quote metaavoid ( self ) quote #b end quote end test ]]" 5997 5998 \item "[[ ftst quote x end quote metaavoid ( self ) quote b end quote end test ]]" 5999 6000 \item "[[ ftst quote #a end quote metaavoid ( self ) quote #a infer #a end quote end test ]]" 6001 6002 \item "[[ ftst quote #a end quote metaavoid ( self ) quote #b infer #a end quote end test ]]" 6003 6004 \item "[[ ftst quote #a end quote metaavoid ( self ) quote #a infer #c end quote end test ]]" 6005 6006 \item "[[ ttst quote #a end quote metaavoid ( self ) quote #b infer #c end quote end test ]]" 6007 6008 \item "[[ ttst quote #a end quote metaavoid ( self ) quote All #a : #a end quote end test ]]" 6009 6010 \item "[[ ttst quote #a end quote metaavoid ( self ) quote All #a : #b end quote end test ]]" 6011 6012 \item "[[ ftst quote #a end quote metaavoid ( self ) quote All #b : #a end quote end test ]]" 6013 6014 \item "[[ ttst quote #a end quote metaavoid ( self ) quote All #b : #b end quote end test ]]" 6015 6016 \item "[[ ftst quote #a end quote metaavoid ( self ) quote #a + #a end quote end test ]]" 6017 6018 \item "[[ ftst quote #a end quote metaavoid ( self ) quote #b + #a end quote end test ]]" 6019 6020 \item "[[ ftst quote #a end quote metaavoid ( self ) quote #a + #c end quote end test ]]" 6021 6022 \item "[[ ttst quote #a end quote metaavoid ( self ) quote #b + #c end quote end test ]]" 6023 6024 \item "[[ ftst quote #a end quote metaavoid ( self ) quote \ #a . #a end quote end test ]]" 6025 6026 \item "[[ ftst quote #a end quote metaavoid ( self ) quote \ #b . #a end quote end test ]]" 6027 6028 \item "[[ ftst quote #a end quote metaavoid ( self ) quote \ #a . #c end quote end test ]]" 6029 6030 \item "[[ ttst quote #a end quote metaavoid ( self ) quote \ #b . #c end quote end test ]]" 6031 6032 \item "[[ ttst quote #a end quote metaavoid ( self ) quote quote #a end quote end quote end test ]]" 6033 6034 \item "[[ ttst quote #a end quote metaavoid ( self ) quote ( All #a : #a ) infer ( #b infer quote #a end quote ) endorse False end quote end test ]]" 6035 6036 \item "[[ ftst quote #a end quote metaavoid ( self ) quote ( All #a : #a ) infer ( #a infer quote #a end quote ) endorse False end quote end test ]]" 6037 6038 \item "[[ ttst quote #a end quote metaavoid* ( self ) << quote #b + #c end quote ,, quote #d + #e end quote >> end test ]]" 6039 6040 \item "[[ ttst quote #b end quote metaavoid* ( self ) << quote #b + #c end quote ,, quote #d + #e end quote >> t= quote #b + #c end quote end test ]]" 6041 6042 \item "[[ ttst quote #c end quote metaavoid* ( self ) << quote #b + #c end quote ,, quote #d + #e end quote >> t= quote #b + #c end quote end test ]]" 6043 6044 \item "[[ ttst quote #d end quote metaavoid* ( self ) << quote #b + #c end quote ,, quote #d + #e end quote >> t= quote #d + #e end quote end test ]]" 6045 6046 \item "[[ ttst quote #e end quote metaavoid* ( self ) << quote #b + #c end quote ,, quote #d + #e end quote >> t= quote #d + #e end quote end test ]]" 6047 6048 \item "[[ ttst distinctvar ( <<>> , self ) end test ]]" 6049 6050 \item "[[ ttst distinctvar ( << quote x end quote >> , self ) end test ]]" 6051 6052 \item "[[ ttst distinctvar ( << quote x end quote ,, quote y end quote >> , self ) end test ]]" 6053 6054 \item "[[ ttst distinctvar ( << quote x end quote ,, quote y end quote ,, quote z end quote >> , self ) end test ]]" 6055 6056 \item "[[ ftst distinctvar ( << quote x end quote ,, quote #y end quote ,, quote z end quote >> , self ) end test ]]" 6057 6058 \item "[[ ftst distinctvar ( << quote x end quote ,, quote y end quote ,, quote x end quote >> , self ) end test ]]" 6059 6060 \item "[[ ftst distinctvar ( << quote x end quote ,, quote y end quote ,, quote y end quote >> , self ) end test ]]" 6061 6062 \item "[[ ftst quote x end quote objectavoid ( self ) quote x end quote end test ]]" 6063 6064 \item "[[ ttst quote x end quote objectavoid ( self ) quote y end quote end test ]]" 6065 6066 \item "[[ ftst quote x end quote objectavoid ( self ) quote x + x end quote end test ]]" 6067 6068 \item "[[ ftst quote x end quote objectavoid ( self ) quote y + x end quote end test ]]" 6069 6070 \item "[[ ftst quote x end quote objectavoid ( self ) quote x + z end quote end test ]]" 6071 6072 \item "[[ ttst quote x end quote objectavoid ( self ) quote y + z end quote end test ]]" 6073 6074 \item "[[ ttst quote x end quote objectavoid ( self ) quote \ x . x end quote end test ]]" 6075 6076 \item "[[ ftst quote x end quote objectavoid ( self ) quote \ y . x end quote end test ]]" 6077 6078 \item "[[ ttst quote x end quote objectavoid ( self ) quote \ x . y end quote end test ]]" 6079 6080 \item "[[ ttst quote x end quote objectavoid ( self ) quote \ y . y end quote end test ]]" 6081 6082 \item "[[ ttst quote x end quote objectavoid ( self ) quote quote x end quote end quote end test ]]" 6083 6084 \item "[[ ttst quote x end quote objectavoid ( self ) quote #a end quote set= << quote #a end quote >> end test ]]" 6085 6086 \item "[[ ttst quote x end quote objectavoid ( self ) quote #a + #b end quote set= << quote #a end quote ,, quote #b end quote >> end test ]]" 6087 6088 \item "[[ ttst quote x end quote objectavoid ( self ) quote \ x . #a end quote set= <<>> end test ]]" 6089 6090 \item "[[ ttst quote x end quote objectavoid ( self ) quote \ y . #a end quote set= << quote #a end quote >> end test ]]" 6091 6092 \item "[[ ttst quote x end quote objectavoid ( self ) quote quote #a end quote end quote set= <<>> end test ]]" 6093 6094 \item "[[ ftst quote x end quote objectavoid ( self ) quote \ #a . x end quote end test ]]". 6095 6096 \item "[[ ftst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote x end quote end test ]]". 6097 6098 \item "[[ ftst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote y end quote end test ]]". 6099 6100 \item "[[ ttst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote z end quote end test ]]". 6101 6102 \item "[[ ftst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote x + y end quote end test ]]". 6103 6104 \item "[[ ftst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote \ x . x + y end quote end test ]]". 6105 6106 \item "[[ ftst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote \ y . x + y end quote end test ]]". 6107 6108 \item "[[ ttst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote \ x . \ y . x + y end quote end test ]]". 6109 6110 \item "[[ ttst << quote x end quote ,, quote v end quote >> objectavoid* ( self ) quote y end quote end test ]]". 6111 6112 \end{statements}" ]" 6113 6114 6115 6116 \subsection{Sequent equality} 6117 6118 "[ "\begin{statements} 6119 6120 \item "[[ ttst << << quote 1 end quote ,, quote 2 end quote >> ,, << quote 3 end quote ,, quote 4 end quote >> ,, quote 5 end quote >> sequent= << << quote 2 end quote ,, quote 1 end quote >> ,, << quote 4 end quote ,, quote 3 end quote >> ,, quote 5 end quote >> end test ]]" 6121 6122 \item "[[ ftst << << quote 6 end quote ,, quote 2 end quote >> ,, << quote 3 end quote ,, quote 4 end quote >> ,, quote 5 end quote >> sequent= << << quote 1 end quote ,, quote 2 end quote >> ,, << quote 3 end quote ,, quote 4 end quote >> ,, quote 5 end quote >> end test ]]" 6123 6124 \item "[[ ftst << << quote 1 end quote ,, quote 6 end quote >> ,, << quote 3 end quote ,, quote 4 end quote >> ,, quote 5 end quote >> sequent= << << quote 1 end quote ,, quote 2 end quote >> ,, << quote 3 end quote ,, quote 4 end quote >> ,, quote 5 end quote >> end test ]]" 6125 6126 \item "[[ ftst << << quote 1 end quote ,, quote 2 end quote >> ,, << quote 6 end quote ,, quote 4 end quote >> ,, quote 5 end quote >> sequent= << << quote 1 end quote ,, quote 2 end quote >> ,, << quote 3 end quote ,, quote 4 end quote >> ,, quote 5 end quote >> end test ]]" 6127 6128 \item "[[ ftst << << quote 1 end quote ,, quote 2 end quote >> ,, << quote 3 end quote ,, quote 6 end quote >> ,, quote 5 end quote >> sequent= << << quote 1 end quote ,, quote 2 end quote >> ,, << quote 3 end quote ,, quote 4 end quote >> ,, quote 5 end quote >> end test ]]" 6129 6130 \item "[[ ftst << << quote 1 end quote ,, quote 2 end quote >> ,, << quote 3 end quote ,, quote 4 end quote >> ,, quote 6 end quote >> sequent= << << quote 1 end quote ,, quote 2 end quote >> ,, << quote 3 end quote ,, quote 4 end quote >> ,, quote 5 end quote >> end test ]]" 6131 6132 \end{statements}" ]" 6133 6134 6135 6136 \subsection{Substitution freeness} 6137 6138 "[ "\begin{statements} 6139 6140 \item "[[ ttst metafree ( quote #a end quote , quote #a end quote , quote #a end quote , self ) end test ]]" 6141 6142 \item "[[ ttst metafree ( quote #a infer #b end quote , quote #a end quote , quote All #c : ( #c infer #b ) end quote , self ) end test ]]" 6143 6144 \item "[[ ttst metafree ( quote All #a : ( #a infer #b ) end quote , quote #a end quote , quote All #c : ( #c infer #b ) end quote , self ) end test ]]" 6145 6146 \item "[[ ftst metafree ( quote All #b : #a end quote , quote #a end quote , quote All #c : ( #c infer #b ) end quote , self ) end test ]]" 6147 6148 \item "[[ ttst metafree ( quote All #b : #b end quote , quote #a end quote , quote All #c : ( #c infer #b ) end quote , self ) end test ]]" 6149 6150 \item "[[ ttst metafree ( quote All #c : #a end quote , quote #a end quote , quote All #c : ( #c infer #b ) end quote , self ) end test ]]" 6151 6152 \item "[[ ttst metafree ( quote All #c : All #d : #a end quote , quote #a end quote , quote All #c : ( #c infer #b ) end quote , self ) end test ]]" 6153 6154 \item "[[ ftst metafree ( quote All #c : All #b : #a end quote , quote #a end quote , quote All #c : ( #c infer #b ) end quote , self ) end test ]]" 6155 6156 \item "[[ ttst metafree ( quote #a + #b end quote , quote #a end quote , quote x + y end quote , self ) end test ]]" 6157 6158 \item "[[ ftst metafree ( quote #a + #b end quote , quote #a end quote , quote x infer y end quote , self ) end test ]]" 6159 6160 \item "[[ ttst metafree ( quote #c + #b end quote , quote #a end quote , quote x infer y end quote , self ) end test ]]" 6161 6162 \item "[[ ttst objectfree ( quote a end quote , quote a end quote , quote a end quote , self ) end test ]]" 6163 6164 \item "[[ ttst objectfree ( quote a + b end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" 6165 6166 \item "[[ ttst objectfree ( quote \ a . ( a + b ) end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" 6167 6168 \item "[[ ftst objectfree ( quote \ b . a end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" 6169 6170 \item "[[ ttst objectfree ( quote \ b . b end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" 6171 6172 \item "[[ ttst objectfree ( quote \ c . a end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" 6173 6174 \item "[[ ttst objectfree ( quote \ c . \ d . a end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" 6175 6176 \item "[[ ftst objectfree ( quote \ c . \ b . a end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" 6177 6178 \end{statements}" ]" 6179 6180 6181 6182 \subsection{Substitution} 6183 6184 "[ "\begin{statements} 6185 6186 \item "[[ ttst metasubst ( quote #a end quote , << quote #a end quote :: quote #b end quote >> , self ) t= quote #b end quote end test ]]" 6187 6188 \item "[[ ttst metasubst ( quote #a end quote , << quote #c end quote :: quote #b end quote >> , self ) t= quote #a end quote end test ]]" 6189 6190 \item "[[ ttst metasubst ( quote All #a : #a end quote , << quote #a end quote :: quote #b end quote >> , self ) t= quote All #a : #a end quote end test ]]" 6191 6192 \item "[[ ttst metasubst ( quote All #b : #a end quote , << quote #a end quote :: quote #b end quote >> , self ) t= quote All #b : #b end quote end test ]]" 6193 6194 \item "[[ ttst metasubst ( quote #a infer #c end quote , << quote #a end quote :: quote #b end quote >> , self ) t= quote #b infer #c end quote end test ]]" 6195 6196 \end{statements}" ]" 6197 6198 6199 6200 \subsection{Sequent operators} 6201 6202 "[ "\begin{statements} 6203 6204 \item "[[ ttst eval-Init ( quote 1 end quote , self ) sequent= << << quote 1 end quote >> ,, <<>> ,, quote 1 end quote >> end test ]]" 6205 6206 \item "[[ ttst eval-Init ( quote 1 + #a end quote , self ) sequent= << << quote 1 + #a end quote >> ,, <<>> ,, quote 1 + #a end quote >> end test ]]" 6207 6208 \item "[[ ttst eval-Init ( quote 1 + ( #a infer #a ) end quote , self ) catch head end test ]]" 6209 6210 \item "[[ ttst eval-Ponens ( << << quote 1 end quote >> ,, << quote 2 end quote >> ,, quote 3 infer 4 end quote >> , quote true end quote , self ) sequent= << << quote 3 end quote ,, quote 1 end quote >> ,, << quote 2 end quote >> ,, quote 4 end quote >> end test ]]" 6211 6212 \item "[[ ttst eval-Ponens ( << << quote 1 end quote >> ,, << quote 2 end quote >> ,, quote 3 endorse 4 end quote >> , quote true end quote , self ) catch head end test ]]" 6213 6214 \item "[[ ttst eval-Probans ( << << quote 1 end quote >> ,, << quote 2 end quote >> ,, quote 3 endorse 4 end quote >> , quote true end quote , self ) sequent= << << quote 1 end quote >> ,, << quote 3 end quote ,, quote 2 end quote >> ,, quote 4 end quote >> end test ]]" 6215 6216 \item "[[ ttst eval-Probans ( << << quote 1 end quote >> ,, << quote 2 end quote >> ,, quote 3 infer 4 end quote >> , quote true end quote , self ) catch head end test ]]" 6217 6218 \item "[[ ttst eval-Verify ( << <<>> ,, <<>> ,, quote \ c . 2 + 2 = 4 endorse 5 end quote >> , quote true end quote , self ) sequent= << <<>> ,, <<>> ,, quote 5 end quote >> end test ]]" 6219 6220 \item "[[ ttst eval-Verify ( << <<>> ,, <<>> ,, quote \ c . 2 + 2 = 5 endorse 5 end quote >> , quote true end quote , self ) catch head end test ]]" 6221 6222 \item "[[ ttst eval-Curry ( << <<>> ,, <<>> ,, quote ( 1 oplus 2 ) infer 3 end quote >> , quote true end quote , self ) sequent= << <<>> ,, <<>> ,, quote 1 infer 2 infer 3 end quote >> end test ]]" 6223 6224 \item "[[ ttst eval-Curry ( << <<>> ,, <<>> ,, quote ( 1 infer 2 ) infer 3 end quote >> , quote true end quote , self ) catch head end test ]]" 6225 6226 \item "[[ ttst eval-Uncurry ( << <<>> ,, <<>> ,, quote 1 infer 2 infer 3 end quote >> , quote true end quote , self ) sequent= << <<>> ,, <<>> ,, quote ( 1 oplus 2 ) infer 3 end quote >> end test ]]" 6227 6228 \item "[[ ttst eval-Uncurry ( << <<>> ,, <<>> ,, quote 1 infer 2 endorse 3 end quote >> , quote true end quote , self ) catch head end test ]]" 6229 6230 \item "[[ ttst eval-Deref ( << <<>> ,, <<>> ,, quote p.A1 end quote >> , quote true end quote , self ) sequent= << <<>> ,, <<>> ,, quote All #x : All #y : #x p.imply #y p.imply #x end quote >> end test ]]" 6231 6232 \item "[[ ttst eval-at ( quote ( All #a : ( #a infer #b ) ) Init at #a end quote , true , self ) sequent= << << quote All #a : ( #a infer #b ) end quote >> ,, <<>> ,, quote #a infer #b end quote >> end test ]]" 6233 6234 \item "[[ ttst eval-at ( quote ( All #a : ( #a infer #b ) ) Init at #b end quote , true , self ) sequent= << << quote All #a : ( #a infer #b ) end quote >> ,, <<>> ,, quote #b infer #b end quote >> end test ]]" 6235 6236 \item "[[ ttst eval-at ( quote ( All #a : ( #a infer #b ) ) Init at #c end quote , true , self ) sequent= << << quote All #a : ( #a infer #b ) end quote >> ,, <<>> ,, quote #c infer #b end quote >> end test ]]" 6237 6238 \item "[[ ttst eval-at ( quote ( #a infer #b ) Init at #c end quote , true , self ) catch head end test ]]" 6239 6240 \item "[[ ttst eval-at ( quote ( All #a : All #b : ( #a infer #b ) ) Init at #a end quote , true , self ) sequent= << << quote All #a : All #b : ( #a infer #b ) end quote >> ,, <<>> ,, quote All #b : #a infer #b end quote >> end test ]]" 6241 6242 \item "[[ ttst eval-at ( quote ( All #a : All #b : ( #a infer #b ) ) Init at #b end quote , true , self ) catch head end test ]]" 6243 6244 \item "[[ ttst eval-at ( quote ( All #a : All #b : ( #a infer #b ) ) Init at #c end quote , true , self ) sequent= << << quote All #a : All #b : ( #a infer #b ) end quote >> ,, <<>> ,, quote All #b : #c infer #b end quote >> end test ]]" 6245 6246 \item "[[ ttst eval-at ( quote ( All #a : All #b : ( #a infer #b ) ) Init at #b at #a end quote , true , self ) sequent= << << quote All #a : All #b : ( #a infer #b ) end quote >> ,, <<>> ,, quote #b infer #a end quote >> end test ]]" 6247 6248 \item "[[ ttst eval-Deref ( << <<>> ,, <<>> ,, quote true end quote >> , quote true end quote , self ) catch head end test ]]" 6249 6250 \item "[[ ttst eval-infer ( quote 2 end quote , << << quote 1 end quote ,, quote 2 end quote >> ,, <<>> ,, quote 3 end quote >> , quote true end quote , self ) sequent= << << quote 1 end quote >> ,, <<>> ,, quote 2 infer 3 end quote >> end test ]]" 6251 6252 \item "[[ ttst eval-infer ( quote 2 + All #a : #a end quote , << << quote 1 end quote ,, quote 2 end quote >> ,, <<>> ,, quote 3 end quote >> , quote true end quote , self ) catch head end test ]]" 6253 6254 \item "[[ ttst eval-endorse ( quote 2 end quote , << <<>> ,, << quote 1 end quote ,, quote 2 end quote >> ,, quote 3 end quote >> , quote true end quote , self ) sequent= << <<>> ,, << quote 1 end quote >> ,, quote 2 endorse 3 end quote >> end test ]]" 6255 6256 \item "[[ ttst eval-endorse ( quote 2 + All #a : #a end quote , << <<>> ,, << quote 1 end quote ,, quote 2 end quote >> ,, quote 3 end quote >> , quote true end quote , self ) catch head end test ]]" 6257 6258 \item "[[ ttst eval-ie ( << <<>> ,, <<>> ,, quote All #x : All #y : #x p.imply #y p.imply #x end quote >> , quote p.A1 end quote , quote true end quote , self ) sequent= << <<>> ,, <<>> ,, quote p.A1 end quote >> end test ]]" 6259 6260 \item "[[ ttst eval-ie ( << <<>> ,, <<>> ,, quote All #a : All #b : #a p.imply #b p.imply #a end quote >> , quote p.A2 end quote , quote true end quote , self ) catch head end test ]]" 6261 6262 \item "[[ ttst eval-all ( quote #a end quote , << << quote #b end quote >> ,, << quote #c end quote >> ,, quote #a infer #b end quote >> , quote true end quote , self ) sequent= << << quote #b end quote >> ,, << quote #c end quote >> ,, quote All #a : #a infer #b end quote >> end test ]]" 6263 6264 \item "[[ ttst eval-all ( << << quote #a end quote >> ,, <<>> ,, quote #a infer #b end quote >> , quote #a end quote , quote true end quote , self ) catch head end test ]]" 6265 6266 \item "[[ ttst eval-all ( << <<>> ,, << quote #a end quote >> ,, quote #a infer #b end quote >> , quote #a end quote , quote true end quote , self ) catch head end test ]]" 6267 6268 \item "[[ ttst eval-cut ( << << quote 1 end quote ,, quote 2 end quote >> ,, << quote 3 end quote ,, quote 4 end quote >> ,, quote 5 end quote >> , << << quote 6 end quote ,, quote 5 end quote >> ,, << quote 7 end quote ,, quote 8 end quote >> ,, quote 9 end quote >> , self ) sequent= << << quote 1 end quote ,, quote 2 end quote ,, quote 6 end quote >> ,, << quote 3 end quote ,, quote 4 end quote ,, quote 7 end quote ,, quote 8 end quote >> ,, quote 9 end quote >> end test ]]" 6269 6270 \end{statements}" ]" 6271 6272 6273 6274 \subsection{Verification} 6275 6276 "[ "\begin{statements} 6277 6278 \item "[[ ttst claiming ( quote 1 end quote , quote 1 &c 2 end quote ) end test ]]" 6279 6280 \item "[[ ttst claiming ( quote 1 end quote , quote 2 &c 1 end quote ) end test ]]" 6281 6282 \item "[[ ftst claiming ( quote 1 end quote , quote 2 &c 3 end quote ) end test ]]" 6283 6284 \end{statements}" ]" 6285 6286 6287 6288 \subsection{Conversions from values to terms} 6289 6290 "[ "\begin{statements} 6291 6292 \item "[[ etst int2string ( true , 0 ) ; << 0 :: "0" :: true >> end test ]]" 6293 6294 \item "[[ etst int2string ( true , 1 ) ; << 0 :: "1" :: true >> end test ]]" 6295 6296 \item "[[ etst int2string ( true , 2 ) ; << 0 :: "2" :: true >> end test ]]" 6297 6298 \item "[[ etst int2string ( true , 5 ) ; << 0 :: "5" :: true >> end test ]]" 6299 6300 \item "[[ etst int2string ( true , 10 ) ; << 0 :: "10" :: true >> end test ]]" 6301 6302 \item "[[ etst int2string ( true , 123 ) ; << 0 :: "123" :: true >> end test ]]" 6303 6304 \item "[[ etst int2string ( true , -1 ) ; << 0 :: "-1" :: true >> end test ]]" 6305 6306 \item "[[ etst int2string ( true , -2 ) ; << 0 :: "-2" :: true >> end test ]]" 6307 6308 \item "[[ etst int2string ( true , -5 ) ; << 0 :: "-5" :: true >> end test ]]" 6309 6310 \item "[[ etst int2string ( true , -10 ) ; << 0 :: "-10" :: true >> end test ]]" 6311 6312 \item "[[ etst int2string ( true , -123 ) ; << 0 :: "-123" :: true >> end test ]]" 6313 6314 \item "[[ ttst val2term ( true , true ) t= quote true end quote end test ]]" 6315 6316 \item "[[ ttst val2term ( true , false ) t= quote false end quote end test ]]" 6317 6318 \item "[[ ttst val2term ( true , true :: false ) t= quote true :: false end quote end test ]]" 6319 6320 \item "[[ ttst val2term ( true , map ( x ) ) t= quote map ( *** ) end quote end test ]]" 6321 6322 \item "[[ ttst val2term ( true , 0 ) t= quote 0 end quote end test ]]" 6323 6324 \item "[[ ttst val2term ( true , 1 ) t= quote %% %1 end quote end test ]]" 6325 6326 \item "[[ ttst val2term ( true , 2 ) t= quote %% %1 %0 end quote end test ]]" 6327 6328 \item "[[ ttst val2term ( true , - 1 ) t= quote - %% %1 end quote end test ]]" 6329 6330 \item "[[ ttst val2term ( true , - 2 ) t= quote - %% %1 %0 end quote end test ]]" 6331 6332 \item "[[ ttst val2term ( true , object ( ( 1 :: 2 ) :: 3 ) ) t= quote object ( ( %% %1 :: %% %1 %0 ) :: %% %1 %1 ) end quote end test ]]" 6333 6334 \end{statements}" ]" 6335 6336 6337 6338 \subsection{Unification} 6339 6340 "[ "\begin{statements} 6341 6342 \item "[[ ttst inst ( pterm ( quote All #x : All #y : #x infer #y infer 5 end quote , self ) , quote true end quote , true [[ "1" -> quote 3 end quote ]] [[ "2" -> quote 4 end quote ]] ) t= quote All 3 : All 4 : 3 infer 4 infer 5 end quote end test ]]" 6343 6344 \item "[[ ftst unify ( quote 2 end quote , quote 2 end quote , true ) catch head end test ]]" 6345 6346 \item "[[ ttst unify ( quote 2 end quote , quote 3 end quote , true ) catch head end test ]]" 6347 6348 \item "[[ ftst unify ( quote 2 + 3 end quote , quote 2 + 3 end quote , true ) catch head end test ]]" 6349 6350 \item "[[ ttst unify ( quote 2 + 3 end quote , quote 2 * 3 end quote , true ) catch head end test ]]" 6351 6352 \item "[[ ttst unify ( quote 2 + 3 end quote , quote 3 + 3 end quote , true ) catch head end test ]]" 6353 6354 \item "[[ ttst unify ( quote 2 + 3 end quote , quote 2 + 2 end quote , true ) catch head end test ]]" 6355 6356 \item "[[ ttst unify ( quote unifresh ( quote v end quote , "1" ) end quote , quote 2 end quote , true ) [[ "1" ]] t= quote 2 end quote end test ]]" 6357 6358 \item "[[ ttst unify ( pterm ( quote All #x : #x end quote , self ) second , quote 2 end quote , true ) [[ "1" ]] t= quote 2 end quote end test ]]" 6359 6360 \item "[[ ttst unify ( pterm ( quote All #x : All #y : #x :: #x :: #y :: #y end quote , self ) second second , pterm ( quote All #x : All #y : All #u : All #v : 2 :: #u :: #u :: #v end quote , self ) second second second second , true ) [[ "1" ]] t= quote 2 end quote end test ]]" 6361 6362 \item "[[ ttst unify ( pterm ( quote All #x : All #y : #x :: #x :: #y :: #y end quote , self ) second second , pterm ( quote All #x : All #y : All #u : All #v : 2 :: #u :: #u :: #v end quote , self ) second second second second , true ) [[ "2" ]] t= quote unifresh ( #u , "3" ) end quote end test ]]" 6363 6364 \item "[[ ttst unify ( pterm ( quote All #x : All #y : #x :: #x :: #y :: #y end quote , self ) second second , pterm ( quote All #x : All #y : All #u : All #v : 2 :: #u :: #u :: #v end quote , self ) second second second second , true ) [[ "3" ]] t= quote 2 end quote end test ]]" 6365 6366 \item "[[ ttst unify ( pterm ( quote All #x : All #y : #x :: #x :: #y :: #y end quote , self ) second second , pterm ( quote All #x : All #y : All #u : All #v : 2 :: #u :: #u :: #v end quote , self ) second second second second , true ) [[ "4" ]] t= quote 2 end quote end test ]]" 6367 6368 \end{statements}" ]" 6369 6370 6371 6372 \subsection{Testing of rack functions} 6373 6374 \begin{statements} 6375 6376 \item "[[ etst sl2rack ( bt2vector* ( 3 ) ) ; true end test ]]" 6377 6378 \item "[[ etst sl2rack ( bt2vector* ( 1 :: 1 :: 4 ) ) ; true :: true end test ]]" 6379 6380 \item "[[ etst sl2rack ( bt2vector* ( 0 :: 7 :: 4 ) ) ; 7 end test ]]" 6381 6382 \item "[[ etst sl2rack ( bt2vector* ( 2 :: 3 :: 7 :: 8 :: 9 :: 4 ) ) ; bt2vector ( 7 :: 8 :: 9 ) end test ]]" 6383 6384 \item "[[ etst sl2rack ( bt2vector* ( 0 :: 6 :: 2 :: 3 :: 7 :: 8 :: 9 :: 3 :: 4 :: 6 ) ) ; 6 :: bt2vector ( 7 :: 8 :: 9 ) end test ]]" 6385 6386 \item "[[ etst sl2rack ( bt2vector* ( 0 :: 6 :: 2 :: 3 :: 7 :: 8 :: 9 :: 3 :: 4 :: 6 :: 0 ) ) ; 6 :: bt2vector ( 7 :: 8 :: 9 ) end test ]]" 6387 6388 \item "[[ etst sl2rack ( append ( bt2vector* ( 0 :: 6 :: 2 :: 3 :: 7 :: 8 :: 9 :: 3 :: 4 :: 6 ) , << false >> ) ) ; 6 :: bt2vector ( 7 :: 8 :: 9 ) end test ]]" 6389 6390 \item "[[ etst sl2rack ( append ( bt2vector* ( 0 :: 6 :: 2 :: 3 :: 7 :: 8 :: 9 :: 3 :: 4 ) , << false >> ) ) ; exception end test ]]" 6391 6392 \item "[[ etst sl2rack ( bt2vector* ( 0 :: 6 :: 2 :: 3 :: 7 :: 8 :: 9 :: 3 :: 4 ) ) ; exception end test ]]" 6393 6394 \item "[[ etst bt2vector* ( << 3 >> ) ; rack2sl ( true ) end test ]]" 6395 6396 \item "[[ etst bt2vector* ( << 1 ,, 1 ,, 4 >> ) ; rack2sl ( true :: true ) end test ]]" 6397 6398 \item "[[ etst bt2vector* ( << 0 ,, 7 ,, 4 >> ) ; rack2sl ( 7 ) end test ]]" 6399 6400 \item "[[ etst bt2vector* ( << 2 ,, 3 ,, 7 ,, 8 ,, 9 ,, 4 >> ) ; rack2sl ( bt2vector ( 7 :: 8 :: 9 ) ) end test ]]" 6401 6402 \item "[[ etst bt2vector* ( << 0 ,, 6 ,, 2 ,, 3 ,, 7 ,, 8 ,, 9 ,, 3 ,, 4 ,, 6 >> ) ; rack2sl ( 6 :: bt2vector ( 7 :: 8 :: 9 ) ) end test ]]" 6403 6404 \item "[[ etst bt2vector* ( << 0 ,, 7 ,, 3 ,, 3 ,, 5 >> ) ; rack2sl ( 7 :: 7 ) end test ]]" 6405 6406 \item "[[ etst bt2vector* ( << 1 ,, 1 ,, 3 ,, 3 ,, 5 >> ) ; rack2sl ( ( true :: true ) :: ( true :: true ) ) end test ]]" 6407 6408 \item "[[ etst exception ; rack2sl ( ( true :: true ) :: ( true :: - 1 ) ) end test ]]" 6409 6410 \item "[[ etst exception ; rack2sl ( ( true :: true ) :: ( true :: false ) ) end test ]]" 6411 6412 \end{statements} 6413 6414 6415 6416 \subsection{Test of Ripemd} 6417 6418 \begin{statements} 6419 6420 \item "[[ etst !"9C1185A5C5E9FC54612808977EE8F548B2258D31" ; ripemds ( !"". ) end test ]]" 6421 6422 \item "[[ etst !"0BDC9D2D256B3EE9DAAE347BE6F4DC835A467FFE" ; ripemds ( !"a" ) end test ]]" 6423 6424 \item "[[ etst !"8EB208F7E05D987A9B044A8E98C6B087F15A0BFC" ; ripemds ( !"abc" ) end test ]]" 6425 6426 \item "[[ etst !"8EB208F7E05D987A9B044A8E98C6B087F15A0BFC" ; ripemds ( << !"a" ,, !"bc" >> ) end test ]]" 6427 6428 \item "[[ etst !"5D0689EF49D2FAE572B881B123A85FFA21595F36" ; ripemds ( !"message digest" ) end test ]]" 6429 6430 \item "[[ etst !"F71C27109C692C1B56BBDCEB5B9D2865B3708DBC" ; ripemds ( !"abcdefghijklmnopqrstuvwxyz" ) end test ]]" 6431 6432 \item "[[ etst !"12A053384A9C0C88E405A06C27DCF49ADA62EB2B" ; ripemds ( !"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq" ) end test ]]" 6433 6434 \item "[[ etst !"B0E20B6E3116640286ED3A87A5713079B21F5189" ; ripemds ( !"ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789" ) end test ]]" 6435 6436 \item "[[ etst !"9B752E45573D4B39F4DBD3323CAB82BF63326BFB" ; ripemds ( repeat ( 8 , !"1234567890" ) ) end test ]]" 6437 6438 \end{statements} 6439 6440 6441 6442 \subsection{Compilation} 6443 6444 "[ "\begin{statements} 6445 6446 \item "[[ define value of compiled-base as norm compile ( base ) end define ]]" 6447 6448 \item "[[ define value of compiled-test as norm compile ( test ) end define ]]" 6449 6450 \item "[[ define value of get-base0 ( x ) as base [[ x ref ]] [[ "code" ]] [[ x idx ]] end define ]]" 6451 6452 \item "[[ define value of get-base1 ( x ) as compiled-base [[ x ref ]] [[ "code" ]] [[ x idx ]] end define ]]" 6453 6454 \item "[[ define value of get-test0 ( x ) as test [[ x ref ]] [[ "code" ]] [[ x idx ]] end define ]]" 6455 6456 \item "[[ define value of get-test1 ( x ) as compiled-test [[ x ref ]] [[ "code" ]] [[ x idx ]] end define ]]" 6457 6458 6459 6460 \item "[[ ftst notnot test [[ test [[ 0 ]] ]] [[ "expansion" ]] end test ]]" 6461 6462 \item "[[ ftst notnot compile ( test ) [[ test [[ 0 ]] ]] [[ "expansion" ]] end test ]]" 6463 6464 \item "[[ ftst notnot ( norm compile ( test ) ) [[ test [[ 0 ]] ]] [[ "expansion" ]] end test ]]" 6465 6466 \item "[[ ftst notnot compiled-test [[ test [[ 0 ]] ]] [[ "expansion" ]] end test ]]" 6467 6468 6469 6470 \item "[[ etst get-base0 ( quote \ x . y end quote ) ; 0 end test ]]" 6471 6472 \item "[[ etst get-base1 ( quote \ x . y end quote ) ; 0 end test ]]" 6473 6474 \item "[[ etst get-base0 ( quote quote x end quote end quote ) ; 1 end test ]]" 6475 6476 \item "[[ etst get-base1 ( quote quote x end quote end quote ) ; 1 end test ]]" 6477 6478 \item "[[ etst get-base0 ( quote true end quote ) ; map ( true ) end test ]]" 6479 6480 \item "[[ etst get-base1 ( quote true end quote ) ; map ( true ) end test ]]" 6481 6482 \item "[[ etst get-base0 ( quote x ' y end quote ) ; map ( true ) end test ]]" 6483 6484 \item "[[ etst get-base1 ( quote x ' y end quote ) ; map ( true ) end test ]]" 6485 6486 \item "[[ etst get-base0 ( quote If x then y else z end quote ) ; map ( true ) end test ]]" 6487 6488 \item "[[ etst get-base1 ( quote If x then y else z end quote ) ; map ( true ) end test ]]" 6489 6490 \item "[[ etst get-base0 ( quote true end quote ) Tail ; true end test ]]" 6491 6492 \item "[[ etst get-base1 ( quote true end quote ) Tail ; true end test ]]" 6493 6494 \item "[[ etst get-base0 ( quote x ' y end quote ) Tail ' ( \ x . x ) ' 2 ; 2 end test ]]" 6495 6496 \item "[[ etst get-base1 ( quote x ' y end quote ) Tail ' ( \ x . x ) ' 2 ; 2 end test ]]" 6497 6498 \item "[[ etst get-base0 ( quote x ' y end quote ) Tail ' ( \ x . 3 ) ' 2 ; 3 end test ]]" 6499 6500 \item "[[ etst get-base1 ( quote x ' y end quote ) Tail ' ( \ x . 3 ) ' 2 ; 3 end test ]]" 6501 6502 \item "[[ etst get-base0 ( quote If x then y else z end quote ) Tail ' true ' 1 ' 2 ; 1 end test ]]" 6503 6504 \item "[[ etst get-base1 ( quote If x then y else z end quote ) Tail ' true ' 1 ' 2 ; 1 end test ]]" 6505 6506 \item "[[ etst get-base0 ( quote If x then y else z end quote ) Tail ' false ' 1 ' 2 ; 2 end test ]]" 6507 6508 \item "[[ etst get-base1 ( quote If x then y else z end quote ) Tail ' false ' 1 ' 2 ; 2 end test ]]" 6509 6510 \item "[[ ttst make-constant ( quote 123 end quote ) Tail ' ( 2 LazyPair 3 ) t= quote 123 end quote end test ]]" 6511 6512 \item "[[ ttst make-lambda ( make-constant ( quote 123 end quote ) ) Tail ' true ' 4 t= quote 123 end quote end test ]]" 6513 6514 \item "[[ define value of compile-test00 as quote 123 end quote end define ]]" 6515 6516 \item "[[ ttst get-test0 ( quote compile-test00 end quote ) Tail t= quote 123 end quote end test ]]" 6517 6518 \item "[[ ttst get-test1 ( quote compile-test00 end quote ) Tail t= quote 123 end quote end test ]]" 6519 6520 \item "[[ define value of compile-test01 ( x ) as quote 123 end quote end define ]]" 6521 6522 \item "[[ ttst get-test0 ( quote compile-test01 ( x ) end quote ) Tail ' 9 t= quote 123 end quote end test ]]" 6523 6524 \item "[[ ttst get-test1 ( quote compile-test01 ( x ) end quote ) Tail ' 9 t= quote 123 end quote end test ]]" 6525 6526 \item "[[ define value of compile-test02 ( x ) as x end define ]]" 6527 6528 \item "[[ etst get-test0 ( quote compile-test02 ( x ) end quote ) Tail ' 9 ; 9 end test ]]" 6529 6530 \item "[[ etst get-test1 ( quote compile-test02 ( x ) end quote ) Tail ' 9 ; 9 end test ]]" 6531 6532 \item "[[ define value of compile-test03 ( x , y ) as x end define ]]" 6533 6534 \item "[[ etst get-test0 ( quote compile-test03 ( x , y ) end quote ) Tail ' 8 ' 9 ; 8 end test ]]" 6535 6536 \item "[[ etst get-test1 ( quote compile-test03 ( x , y ) end quote ) Tail ' 8 ' 9 ; 8 end test ]]" 6537 6538 \item "[[ define value of compile-test04 ( x , y ) as y end define ]]" 6539 6540 \item "[[ etst get-test0 ( quote compile-test04 ( x , y ) end quote ) Tail ' 8 ' 9 ; 9 end test ]]" 6541 6542 \item "[[ etst get-test1 ( quote compile-test04 ( x , y ) end quote ) Tail ' 8 ' 9 ; 9 end test ]]" 6543 6544 \item "[[ define value of compile-test05 ( x , y ) as z end define ]]" 6545 6546 \item "[[ etst get-test0 ( quote compile-test05 ( x , y ) end quote ) Tail ' 8 ' 9 ; true end test ]]" 6547 6548 \item "[[ etst get-test1 ( quote compile-test05 ( x , y ) end quote ) Tail ' 8 ' 9 ; true end test ]]" 6549 6550 \item "[[ define value of compile-test06 ( x , x ) as x end define ]]" 6551 6552 \item "[[ etst get-test0 ( quote compile-test06 ( x , y ) end quote ) Tail ' 8 ' 9 ; 8 end test ]]" 6553 6554 \item "[[ etst get-test1 ( quote compile-test06 ( x , y ) end quote ) Tail ' 8 ' 9 ; 8 end test ]]" 6555 6556 \item "[[ define value of compile-test07 as "abc" end define ]]" 6557 6558 \item "[[ etst get-test0 ( quote compile-test07 end quote ) Tail ; "abc" end test ]]" 6559 6560 \item "[[ etst get-test1 ( quote compile-test07 end quote ) Tail ; "abc" end test ]]" 6561 6562 \item "[[ define value of compile-test08 as test end define ]]" 6563 6564 \item "[[ etst get-test0 ( quote compile-test08 end quote ) Tail [[ 0 ]] ; quote test end quote ref end test ]]" 6565 6566 \item "[[ etst get-test1 ( quote compile-test08 end quote ) Tail [[ 0 ]] ; quote test end quote ref end test ]]" 6567 6568 \item "[[ define value of compile-test09 as base end define ]]" 6569 6570 \item "[[ etst get-test0 ( quote compile-test09 end quote ) Tail [[ 0 ]] ; quote base end quote ref end test ]]" 6571 6572 \item "[[ etst get-test1 ( quote compile-test09 end quote ) Tail [[ 0 ]] ; quote base end quote ref end test ]]" 6573 6574 \item "[[ define value of compile-test10 ( u , v ) as \ x . \ y . u end define ]]" 6575 6576 \item "[[ etst get-test0 ( quote compile-test10 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 1 end test ]]" 6577 6578 \item "[[ etst get-test1 ( quote compile-test10 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 1 end test ]]" 6579 6580 \item "[[ define value of compile-test11 ( u , v ) as \ x . \ y . v end define ]]" 6581 6582 \item "[[ etst get-test0 ( quote compile-test11 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 2 end test ]]" 6583 6584 \item "[[ etst get-test1 ( quote compile-test11 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 2 end test ]]" 6585 6586 \item "[[ define value of compile-test12 ( u , v ) as \ x . \ y . x end define ]]" 6587 6588 \item "[[ etst get-test0 ( quote compile-test12 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 3 end test ]]" 6589 6590 \item "[[ etst get-test1 ( quote compile-test12 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 3 end test ]]" 6591 6592 \item "[[ define value of compile-test13 ( u , v ) as \ x . \ y . y end define ]]" 6593 6594 \item "[[ etst get-test0 ( quote compile-test13 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 4 end test ]]" 6595 6596 \item "[[ etst get-test1 ( quote compile-test13 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 4 end test ]]" 6597 6598 \item "[[ define value of compile-test14 as Base end define ]]" 6599 6600 \item "[[ etst get-test0 ( quote compile-test14 end quote ) Tail ; 10 end test ]]" 6601 6602 \item "[[ etst get-test1 ( quote compile-test14 end quote ) Tail ; 10 end test ]]" 6603 6604 \item "[[ define value of compile-test15 ( Base , x ) as Base end define ]]" 6605 6606 \item "[[ etst get-test0 ( quote compile-test15 ( x , y ) end quote ) Tail ' 1 ' 2 ; 10 end test ]]" 6607 6608 \item "[[ etst get-test1 ( quote compile-test15 ( x , y ) end quote ) Tail ' 1 ' 2 ; 10 end test ]]" 6609 6610 \item "[[ define value of compile-test16 ( Base , x ) as x end define ]]" 6611 6612 \item "[[ etst get-test0 ( quote compile-test16 ( x , y ) end quote ) Tail ' 1 ' 2 ; 2 end test ]]" 6613 6614 \item "[[ etst get-test1 ( quote compile-test16 ( x , y ) end quote ) Tail ' 1 ' 2 ; 2 end test ]]" 6615 6616 \item "[[ define value of compile-test17 as 123 end define ]]" 6617 6618 \item "[[ etst get-test0 ( quote compile-test17 end quote ) Tail ; 123 end test ]]" 6619 6620 \item "[[ etst get-test1 ( quote compile-test17 end quote ) Tail ; 123 end test ]]" 6621 6622 \item "[[ define value of compile-test18 as 123 - 23 end define ]]" 6623 6624 \item "[[ etst get-test0 ( quote compile-test18 end quote ) Tail ; 100 end test ]]" 6625 6626 \item "[[ etst get-test1 ( quote compile-test18 end quote ) Tail ; 100 end test ]]" 6627 6628 \item "[[ define value of compile-test19 ( x , y ) as if x then y else compile-test19 ( x tail , x head :: y ) end define ]]" 6629 6630 \item "[[ etst << 3 ,, 4 >> ; ( get-test0 ( quote compile-test19 ( x , y ) end quote ) apply true maptag apply << 3 ,, 4 >> maptag ) untag end test ]]" 6631 6632 \item "[[ etst << 3 ,, 4 >> ; ( get-test1 ( quote compile-test19 ( x , y ) end quote ) apply true maptag apply << 3 ,, 4 >> maptag ) untag end test ]]" 6633 6634 \item "[[ etst << 1 ,, 2 ,, 3 ,, 4 >> ; ( get-test0 ( quote compile-test19 ( x , y ) end quote ) apply << 2 ,, 1 >> maptag apply << 3 ,, 4 >> maptag ) untag end test ]]" 6635 6636 \item "[[ etst << 1 ,, 2 ,, 3 ,, 4 >> ; ( get-test1 ( quote compile-test19 ( x , y ) end quote ) apply << 2 ,, 1 >> maptag apply << 3 ,, 4 >> maptag ) untag end test ]]" 6637 6638 \item "[[ etst true ; ( get-base0 ( quote true end quote ) ) Tail end test ]]" 6639 6640 \item "[[ etst true ; ( get-base1 ( quote true end quote ) ) Tail end test ]]" 6641 6642 \item "[[ etst false ; ( get-base0 ( quote false end quote ) ) Tail end test ]]" 6643 6644 \item "[[ etst false ; ( get-base1 ( quote false end quote ) ) Tail end test ]]" 6645 6646 \item "[[ ttst 2 LazyPair 3 Equal get-base0 ( quote x LazyPair y end quote ) Tail ' 2 ' 3 end test ]]" 6647 6648 \item "[[ ttst 2 LazyPair 3 Equal get-base1 ( quote x LazyPair y end quote ) Tail ' 2 ' 3 end test ]]" 6649 6650 \item "[[ ftst 3 LazyPair 2 Equal get-base0 ( quote x LazyPair y end quote ) Tail ' 2 ' 3 Tail end test ]]" 6651 6652 \item "[[ ftst 3 LazyPair 2 Equal get-base1 ( quote x LazyPair y end quote ) Tail ' 2 ' 3 Tail end test ]]" 6653 6654 \item "[[ ttst 2 LazyPair 3 Equal get-base0 ( quote x Pair y end quote ) Tail ' 2 ' 3 end test ]]" 6655 6656 \item "[[ ttst 2 LazyPair 3 Equal get-base1 ( quote x Pair y end quote ) Tail ' 2 ' 3 end test ]]" 6657 6658 \item "[[ ttst get-base0 ( quote x Equal y end quote ) Tail ' 2 ' 2 end test ]]" 6659 6660 \item "[[ ttst get-base1 ( quote x Equal y end quote ) Tail ' 2 ' 2 end test ]]" 6661 6662 \item "[[ ftst get-base0 ( quote x Equal y end quote ) Tail ' 2 ' 3 maptag end test ]]" 6663 6664 \item "[[ ftst get-base1 ( quote x Equal y end quote ) Tail ' 2 ' 3 maptag end test ]]" 6665 6666 \item "[[ ttst 10 LazyPair true Equal get-base0 ( quote x Pair y end quote ) Tail ' 10 ' true end test ]]" 6667 6668 \item "[[ ttst 10 LazyPair true Equal get-base1 ( quote x Pair y end quote ) Tail ' 10 ' true end test ]]" 6669 6670 \item "[[ ttst 10 LazyPair false Equal get-base0 ( quote x Pair y end quote ) Tail ' 10 ' false end test ]]" 6671 6672 \item "[[ ttst 10 LazyPair false Equal get-base1 ( quote x Pair y end quote ) Tail ' 10 ' false end test ]]" 6673 6674 \item "[[ ttst true LazyPair true Equal get-base0 ( quote x Pair y end quote ) Tail ' true ' true end test ]]" 6675 6676 \item "[[ ttst true LazyPair true Equal get-base1 ( quote x Pair y end quote ) Tail ' true ' true end test ]]" 6677 6678 \item "[[ ttst true LazyPair 10 Equal get-base0 ( quote x Pair y end quote ) Tail ' true ' 10 end test ]]" 6679 6680 \item "[[ ttst true LazyPair 10 Equal get-base1 ( quote x Pair y end quote ) Tail ' true ' 10 end test ]]" 6681 6682 \item "[[ ttst false LazyPair 10 Equal get-base0 ( quote x Pair y end quote ) Tail ' false ' 10 end test ]]" 6683 6684 \item "[[ ttst false LazyPair 10 Equal get-base1 ( quote x Pair y end quote ) Tail ' false ' 10 end test ]]" 6685 6686 \item "[[ ttst true LazyPair false Equal get-base0 ( quote x Pair y end quote ) Tail ' true ' false end test ]]" 6687 6688 \item "[[ ttst true LazyPair false Equal get-base1 ( quote x Pair y end quote ) Tail ' true ' false end test ]]" 6689 6690 \item "[[ ttst false LazyPair true Equal get-base0 ( quote x Pair y end quote ) Tail ' false ' true end test ]]" 6691 6692 \item "[[ ttst false LazyPair true Equal get-base1 ( quote x Pair y end quote ) Tail ' false ' true end test ]]" 6693 6694 \item "[[ ttst Zero Equal ( get-base0 ( quote Zero end quote ) ) Tail end test ]]" 6695 6696 \item "[[ ttst Zero Equal ( get-base1 ( quote Zero end quote ) ) Tail end test ]]" 6697 6698 \item "[[ ttst One Equal ( get-base0 ( quote x Pair y end quote ) apply map ( false ) apply map ( Zero ) ) Tail end test ]]" 6699 6700 \item "[[ ttst One Equal ( get-base1 ( quote x Pair y end quote ) apply map ( false ) apply map ( Zero ) ) Tail end test ]]" 6701 6702 \item "[[ ttst One Equal ( get-base0 ( quote One end quote ) ) Tail end test ]]" 6703 6704 \item "[[ ttst One Equal ( get-base1 ( quote One end quote ) ) Tail end test ]]" 6705 6706 \item "[[ ttst Two Equal ( get-base0 ( quote Two end quote ) ) Tail end test ]]" 6707 6708 \item "[[ ttst Two Equal ( get-base1 ( quote Two end quote ) ) Tail end test ]]" 6709 6710 \item "[[ ttst Five Equal ( get-base0 ( quote x Plus y end quote ) apply map ( Three ) apply map ( Two ) ) Tail end test ]]" 6711 6712 \item "[[ ttst Five Equal ( get-base1 ( quote x Plus y end quote ) apply map ( Three ) apply map ( Two ) ) Tail end test ]]" 6713 6714 \item "[[ etst 10 ; ( get-base0 ( quote Base end quote ) ) untag end test ]]" 6715 6716 \item "[[ etst 10 ; ( get-base1 ( quote Base end quote ) ) untag end test ]]" 6717 6718 \item "[[ etst << 1 ,, 2 ,, 3 >> ; ( get-base0 ( quote revappend ( x , y ) end quote ) apply << 1 >> maptag apply << 2 ,, 3 >> maptag ) untag end test ]]" 6719 6720 \item "[[ etst << 1 ,, 2 ,, 3 >> ; ( get-base1 ( quote revappend ( x , y ) end quote ) apply << 1 >> maptag apply << 2 ,, 3 >> maptag ) untag end test ]]" 6721 6722 \item "[[ ttst prune ( quote 1 + 2 end quote , test ) t= quote 1 + 2 end quote end test ]]" 6723 6724 \item "[[ ttst prune ( quote 1 + 2 end quote , base ) t= quote 1 + 2 end quote end test ]]" 6725 6726 \item "[[ ttst prune ( quote 1 + compile-test00 end quote , test ) t= quote 1 + compile-test00 end quote end test ]]" 6727 6728 \item "[[ ttst prune ( quote 1 + compile-test00 end quote , base ) t= quote 1 + base end quote end test ]]" 6729 6730 \item "[[ ttst prune ( quote compile-test03 ( 1 , 2 ) end quote , test ) t= quote compile-test03 ( 1 , 2 ) end quote end test ]]" 6731 6732 \item "[[ ttst prune ( quote compile-test03 ( 1 , 2 ) end quote , base ) t= quote base end quote end test ]]" 6733 6734 \item "[[ etst compiled-base [[ base [[ 0 ]] ]] [[ "diagnose" ]] ; true maptag end test ]]" 6735 6736 \item "[[ ttst compile ( test [[ << test [[ 0 ]] ,, "expansion" >> => quote test end quote ]] ) [[ test [[ 0 ]] ]] [[ "diagnose" ]] = true maptag end test ]]" 6737 6738 \item "[[ ttst compile ( test [[ << test [[ 0 ]] ,, "expansion" >> => quote test end quote ]] ) [[ test [[ 0 ]] ]] [[ "diagnose" ]] untag = true end test ]]" 6739 6740 \item "[[ ttst compile ( test [[ << test [[ 0 ]] ,, "expansion" >> => quote ttst 2 + 3 = 5 end test .then. ttst 2 + 4 = 6 end test end quote ]] ) [[ test [[ 0 ]] ]] [[ "diagnose" ]] untag = true end test ]]" 6741 6742 \item "[[ ttst compile ( test [[ << test [[ 0 ]] ,, "expansion" >> => quote ttst 2 + 3 = 0 end test .then. ttst 2 + 4 = 6 end test end quote ]] ) [[ test [[ 0 ]] ]] [[ "diagnose" ]] untag first first t= quote ttst 2 + 3 = 0 end test end quote end test ]]" 6743 6744 \item "[[ ttst compile ( test [[ << test [[ 0 ]] ,, "expansion" >> => quote ttst 2 + 3 = 5 end test .then. ttst 2 + 4 = 0 end test end quote ]] ) [[ test [[ 0 ]] ]] [[ "diagnose" ]] untag first first t= quote ttst 2 + 4 = 0 end test end quote end test ]]" 6745 6746 \item "[[ ttst compile ( test [[ << test [[ 0 ]] ,, "expansion" >> => quote ttst 2 + 3 = 0 end test .then. ttst 2 + 4 = 0 end test end quote ]] ) [[ test [[ 0 ]] ]] [[ "diagnose" ]] untag first first t= quote ttst 2 + 3 = 0 end test end quote end test ]]" 6747 6748 \item "[[ define value of test as 2 + 3 end define ]]" 6749 6750 \item "[[ ttst show test [[ test [[ 0 ]] ]] [[ "codex" ]] [[ quote test end quote ref ]] [[ quote test end quote idx ]] [[ 0 ]] [[ "value" ]] t= quote define value of test as 2 + 3 end define end quote end show end test ]]" 6751 6752 \item "[[ etst get-test0 ( quote test end quote ) Tail ; 5 end test ]]" 6753 6754 \item "[[ etst get-test1 ( quote test end quote ) Tail ; 5 end test ]]" 6755 6756 \end{statements}" ]" 6757 6758 6759 6760 \end{document} 6761 6762 " end text ,, 6763 6764 6765 6766 latex ( "page" ) ,, 6767 latex ( "page" ) ,, 6768 dvipdfm ( "page" ) ,, 6769 6770 6771 6772 text "chores.tex" : ""-""; 6773 6774 \documentclass[fleqn]{article} 6775 6776 % Mark overfull lines 6777 \setlength{\overfullrule}{1mm} 6778 6779 % Include definitions generated by lgc 6780 \input{lgwinclude} 6781 6782 % Make latexsym characters available 6783 \usepackage{latexsym} 6784 6785 % Ensure reasonable rendering of strings 6786 \everymath{\rm} 6787 \everydisplay{\rm} 6788 6789 % Enable generation of an index 6790 \usepackage{makeidx} 6791 \makeindex 6792 \newcommand{\intro}[1]{\emph{#1}} 6793 \newcommand{\indexintro}[1]{\index{#1}\intro{#1}} 6794 6795 % Enable generation of a bibliography 6796 \bibliographystyle{plain} 6797 6798 % Enable hyperlinks 6799 \usepackage[dvipdfm=true]{hyperref} 6800 \hypersetup{pdfpagemode=none} 6801 \hypersetup{pdfstartpage=1} 6802 \hypersetup{pdfstartview=FitBH} 6803 \hypersetup{pdfpagescrop={120 80 490 730}} 6804 \hypersetup{pdftitle=A Logiweb test page - chores} 6805 \hypersetup{colorlinks=true} 6806 6807 % Construct for listing statements with associated explanations 6808 \newenvironment{statements}{\begin{list}{}{ 6809 \setlength{\leftmargin}{5em} 6810 \setlength{\itemindent}{-5em}}}{\end{list}} 6811 6812 \begin{document} 6813 \title{A Logiweb test page - chores} 6814 \author{Klaus Grue} 6815 \maketitle 6816 \tableofcontents 6817 6818 6819 6820 \section{\TeX\ definitions} 6821 6822 6823 6824 \section{Name definitions} 6825 6826 "[[ protect ""N end protect ]]" 6827 6828 6829 6830 \section{Charge definitions} 6831 6832 "[[ protect ""C end protect ]]" 6833 6834 6835 6836 \end{document}%\item $ttst0\linebreak [0]\ 6837 6838 6839 6840 " end text ,, 6841 6842 6843 6844 latex ( "chores" ) ,, 6845 latex ( "chores" ) ,, 6846 dvipdfm ( "chores" ) 6847 6848 6849