"";;01B9F25A278238ACBDFCFA47173491B3A0F480509096C987A2BBD8BB0806 ""P test ""R base ""R check ""D 0 tt tf ta tb tc td tx ty tz tm to tO compiled-base compiled-test get-base0 ( " ) get-base1 ( " ) get-test0 ( " ) get-test1 ( " ) compile-test00 compile-test01 ( " ) compile-test02 ( " ) compile-test03 ( " , " ) compile-test04 ( " , " ) compile-test05 ( " , " ) compile-test06 ( " , " ) compile-test07 compile-test08 compile-test09 compile-test10 ( " , " ) compile-test11 ( " , " ) compile-test12 ( " , " ) compile-test13 ( " , " ) compile-test14 compile-test15 ( " , " ) compile-test16 ( " , " ) compile-test17 compile-test18 compile-test19 ( " , " ) ""B text "index.html" : ""-""; A Logiweb test page

A Logiweb test page

Up

Contents: Main text Chores

Klaus Grue

" end text ,, text "page.tex" : ""-""; \documentclass[fleqn]{article} % Mark overfull lines \setlength{\overfullrule}{1mm} % Include definitions generated by lgc \input{lgwinclude} % Make latexsym characters available \usepackage{latexsym} % Ensure reasonable rendering of strings \everymath{\rm} \everydisplay{\rm} % Enable generation of an index \usepackage{makeidx} \makeindex \newcommand{\intro}[1]{\emph{#1}} \newcommand{\indexintro}[1]{\index{#1}\intro{#1}} % Enable generation of a bibliography \bibliographystyle{plain} % Enable hyperlinks \usepackage[dvipdfm=true]{hyperref} \hypersetup{pdfpagemode=none} \hypersetup{pdfstartpage=1} \hypersetup{pdfstartview=FitBH} \hypersetup{pdfpagescrop={120 80 490 730}} \hypersetup{pdftitle=A Logiweb test page} \hypersetup{colorlinks=true} % Construct for listing statements with associated explanations \newenvironment{statements}{\begin{list}{}{ \setlength{\leftmargin}{5em} \setlength{\itemindent}{-5em}}}{\end{list}} \begin{document} \title{A Logiweb test page} \author{Klaus Grue} \maketitle \tableofcontents \section{Introduction} This paper tests some of the constructs introduced on the base and check pages. \section{Auxiliary definitions} "[ "\begin{statements} \item "[[ define value of tt as true end define ]]" \item "[[ define value of tf as false end define ]]" \item "[[ define value of ta as tt :: tt end define ]]" \item "[[ define value of tb as tt :: tf end define ]]" \item "[[ define value of tc as tf :: tt end define ]]" \item "[[ define value of td as tf :: tf end define ]]" \item "[[ define value of tx as exception end define ]]" \item "[[ define value of ty as 2 raise end define ]]" \item "[[ define value of tz as 3 raise end define ]]" \item "[[ define value of tm as map ( \ x . x ) end define ]]" \item "[[ define value of to as ( Zero Pair Nine ) Pair 1 end define ]]" \item "[[ define value of tO as ( One Pair Nine ) Pair 1 end define ]]" "";\item "[[ etst "print" ; print ( ( ty != tx ) catch ) end test ]]" "";\item "[[ etst ty ; ty = tx end test ]]" "";\item "[[ etst ty ; ty != tx end test ]]" "";\item "[[ etst ty ; ty = bottom end test ]]" \end{statements}" ]" \section{Test of test constructs} "[ "\begin{statements} \item "[[ ttst true end test ]]" \item "[[ ftst false end test ]]" \item "[[ etst tx ; exception end test ]]" \item "[[ etst ty ; 2 raise end test ]]" "";\item "[[ ttst false end test ]]" "";\item "[[ ttst exception end test ]]" "";\item "[[ ftst true end test ]]" "";\item "[[ ftst exception end test ]]" "";\item "[[ etst tx ; true end test ]]" "";\item "[[ etst tx ; false end test ]]" "";\item "[[ etst tx ; ty end test ]]" \end{statements}" ]" \section{Untagged Booleans} \subsection{Not} "[ "\begin{statements} \item "[[ ftst Not true end test ]]" \item "[[ ttst Not false end test ]]" \end{statements}" ]" \subsection{And} "[ "\begin{statements} \item "[[ ttst true And true end test ]]" \item "[[ ftst true And false end test ]]" \item "[[ ftst false And true end test ]]" \item "[[ ftst false And false end test ]]" \end{statements}" ]" \subsection{Or} "[ "\begin{statements} \item "[[ ttst true Or true end test ]]" \item "[[ ttst true Or false end test ]]" \item "[[ ttst false Or true end test ]]" \item "[[ ftst false Or false end test ]]" \end{statements}" ]" \subsection{Iff} "[ "\begin{statements} \item "[[ ttst true Iff true end test ]]" \item "[[ ftst true Iff false end test ]]" \item "[[ ftst false Iff true end test ]]" \item "[[ ttst false Iff false end test ]]" \end{statements}" ]" \subsection{TheBool} "[ "\begin{statements} \item "[[ ttst true TheBool end test ]]" \item "[[ ftst false TheBool end test ]]" \end{statements}" ]" \subsection{Equal} "[ "\begin{statements} \item "[[ ttst true Equal true end test ]]" \item "[[ ftst true Equal false end test ]]" \item "[[ ftst false Equal true end test ]]" \item "[[ ttst false Equal false end test ]]" \item "[[ ttst true Pair true Equal true Pair true end test ]]" \item "[[ ttst true Pair false Equal true Pair false end test ]]" \item "[[ ttst false Pair true Equal false Pair true end test ]]" \item "[[ ttst false Pair false Equal false Pair false end test ]]" \item "[[ ftst false Pair true Equal true Pair true end test ]]" \item "[[ ftst true Pair false Equal true Pair true end test ]]" \item "[[ ftst true Pair true Equal false Pair true end test ]]" \item "[[ ftst true Pair true Equal true Pair false end test ]]" \end{statements}" ]" \section{Untagged naturals} \subsection{Small naturals} "[ "\begin{statements} \item "[[ ttst Zero Equal true end test ]]" \item "[[ ttst One Equal false Pair true end test ]]" \item "[[ ttst Two Equal true Pair false Pair true end test ]]" \item "[[ ttst Three Equal false Pair false Pair true end test ]]" \end{statements}" ]" \subsection{NatPair} "[ "\begin{statements} \item "[[ ttst true NatPair Zero Equal Zero end test ]]" \item "[[ ttst true NatPair One Equal Two end test ]]" \item "[[ ttst Three NatPair true Equal One end test ]]" \item "[[ ttst Three NatPair One Equal Three end test ]]" \end{statements}" ]" \subsection{TheNat} "[ "\begin{statements} \item "[[ ttst ( true ) TheNat Equal Zero end test ]]" \item "[[ ttst ( true Pair true ) TheNat Equal Zero end test ]]" \item "[[ ttst ( true Pair true Pair true ) TheNat Equal Zero end test ]]" \item "[[ ttst ( true Pair true Pair true Pair true ) TheNat Equal Zero end test ]]" \item "[[ ttst ( true Pair false Pair true Pair true Pair true ) TheNat Equal Two end test ]]" \item "[[ ttst ( true Pair Three Pair true Pair true Pair true ) TheNat Equal Two end test ]]" \end{statements}" ]" \subsection{Xor} "[ "\begin{statements} \item "[[ ttst Xor ( Two , Two , true ) end test ]]" \item "[[ ftst Xor ( Two , Two , false ) end test ]]" \item "[[ ftst Xor ( Two , Three , true ) end test ]]" \item "[[ ttst Xor ( Two , Three , false ) end test ]]" \item "[[ ftst Xor ( Three , Two , true ) end test ]]" \item "[[ ttst Xor ( Three , Two , false ) end test ]]" \item "[[ ttst Xor ( Three , Three , true ) end test ]]" \item "[[ ftst Xor ( Three , Three , false ) end test ]]" \end{statements}" ]" \subsection{Carry} "[ "\begin{statements} \item "[[ ttst Carry ( Two , Two , true ) end test ]]" \item "[[ ttst Carry ( Two , Two , false ) end test ]]" \item "[[ ttst Carry ( Two , Three , true ) end test ]]" \item "[[ ftst Carry ( Two , Three , false ) end test ]]" \item "[[ ttst Carry ( Three , Two , true ) end test ]]" \item "[[ ftst Carry ( Three , Two , false ) end test ]]" \item "[[ ftst Carry ( Three , Three , true ) end test ]]" \item "[[ ftst Carry ( Three , Three , false ) end test ]]" \end{statements}" ]" \subsection{Borrow} "[ "\begin{statements} \item "[[ ttst Borrow ( Two , Two , true ) end test ]]" \item "[[ ftst Borrow ( Two , Two , false ) end test ]]" \item "[[ ftst Borrow ( Two , Three , true ) end test ]]" \item "[[ ftst Borrow ( Two , Three , false ) end test ]]" \item "[[ ttst Borrow ( Three , Two , true ) end test ]]" \item "[[ ttst Borrow ( Three , Two , false ) end test ]]" \item "[[ ttst Borrow ( Three , Three , true ) end test ]]" \item "[[ ftst Borrow ( Three , Three , false ) end test ]]" \end{statements}" ]" \subsection{Plus} "[ "\begin{statements} \item "[[ ttst Zero Plus Zero Equal Zero end test ]]" \item "[[ ttst Zero Plus One Equal One end test ]]" \item "[[ ttst Zero Plus Two Equal Two end test ]]" \item "[[ ttst Zero Plus Three Equal Three end test ]]" \item "[[ ttst One Plus Zero Equal One end test ]]" \item "[[ ttst One Plus One Equal Two end test ]]" \item "[[ ttst One Plus Two Equal Three end test ]]" \item "[[ ttst One Plus Three Equal Four end test ]]" \item "[[ ttst Two Plus Zero Equal Two end test ]]" \item "[[ ttst Two Plus One Equal Three end test ]]" \item "[[ ttst Two Plus Two Equal Four end test ]]" \item "[[ ttst Two Plus Three Equal Five end test ]]" \item "[[ ttst Three Plus Zero Equal Three end test ]]" \item "[[ ttst Three Plus One Equal Four end test ]]" \item "[[ ttst Three Plus Two Equal Five end test ]]" \item "[[ ttst Three Plus Three Equal Six end test ]]" \end{statements}" ]" \subsection{LT} "[ "\begin{statements} \item "[[ ttst Zero LT Zero Equal false end test ]]" \item "[[ ttst Zero LT One Equal true end test ]]" \item "[[ ttst Zero LT Two Equal true end test ]]" \item "[[ ttst Zero LT Three Equal true end test ]]" \item "[[ ttst One LT Zero Equal false end test ]]" \item "[[ ttst One LT One Equal false end test ]]" \item "[[ ttst One LT Two Equal true end test ]]" \item "[[ ttst One LT Three Equal true end test ]]" \item "[[ ttst Two LT Zero Equal false end test ]]" \item "[[ ttst Two LT One Equal false end test ]]" \item "[[ ttst Two LT Two Equal false end test ]]" \item "[[ ttst Two LT Three Equal true end test ]]" \item "[[ ttst Three LT Zero Equal false end test ]]" \item "[[ ttst Three LT One Equal false end test ]]" \item "[[ ttst Three LT Two Equal false end test ]]" \item "[[ ttst Three LT Three Equal false end test ]]" \end{statements}" ]" \subsection{Minus} "[ "\begin{statements} \item "[[ ttst Zero Minus Zero Equal Zero end test ]]" \item "[[ ttst One Minus Zero Equal One end test ]]" \item "[[ ttst One Minus One Equal Zero end test ]]" \item "[[ ttst Two Minus Zero Equal Two end test ]]" \item "[[ ttst Two Minus One Equal One end test ]]" \item "[[ ttst Two Minus Two Equal Zero end test ]]" \item "[[ ttst Three Minus Zero Equal Three end test ]]" \item "[[ ttst Three Minus One Equal Two end test ]]" \item "[[ ttst Three Minus Two Equal One end test ]]" \item "[[ ttst Three Minus Three Equal Zero end test ]]" \end{statements}" ]" \subsection{Times} "[ "\begin{statements} \item "[[ ttst Zero Times Zero Equal Zero end test ]]" \item "[[ ttst Zero Times One Equal Zero end test ]]" \item "[[ ttst Zero Times Two Equal Zero end test ]]" \item "[[ ttst Zero Times Three Equal Zero end test ]]" \item "[[ ttst One Times Zero Equal Zero end test ]]" \item "[[ ttst One Times One Equal One end test ]]" \item "[[ ttst One Times Two Equal Two end test ]]" \item "[[ ttst One Times Three Equal Three end test ]]" \item "[[ ttst Two Times Zero Equal Zero end test ]]" \item "[[ ttst Two Times One Equal Two end test ]]" \item "[[ ttst Two Times Two Equal Four end test ]]" \item "[[ ttst Two Times Three Equal Six end test ]]" \item "[[ ttst Three Times Zero Equal Zero end test ]]" \item "[[ ttst Three Times One Equal Three end test ]]" \item "[[ ttst Three Times Two Equal Six end test ]]" \end{statements}" ]" \section{Booleans} \subsection{boolp} "[ "\begin{statements} \item "[[ ttst tt boolp end test ]]" \item "[[ ttst tf boolp end test ]]" \item "[[ ftst 1 boolp end test ]]" \item "[[ ftst 2 boolp end test ]]" \item "[[ ftst -2 boolp end test ]]" \item "[[ ftst ta boolp end test ]]" \item "[[ ftst tb boolp end test ]]" \item "[[ ftst tc boolp end test ]]" \item "[[ ftst td boolp end test ]]" \item "[[ etst tx ; tx boolp end test ]]" \item "[[ etst ty ; ty boolp end test ]]" \item "[[ ftst tm boolp end test ]]" \item "[[ ftst to boolp end test ]]" \item "[[ ftst tO boolp end test ]]" \end{statements}" ]" \subsection{truep} "[ "\begin{statements} \item "[[ ttst tt truep end test ]]" \item "[[ ftst tf truep end test ]]" \item "[[ ftst 1 truep end test ]]" \item "[[ ftst 2 truep end test ]]" \item "[[ ftst -2 truep end test ]]" \item "[[ ftst ta truep end test ]]" \item "[[ ftst tb truep end test ]]" \item "[[ ftst tc truep end test ]]" \item "[[ ftst td truep end test ]]" \item "[[ etst tx ; tx truep end test ]]" \item "[[ etst ty ; ty truep end test ]]" \item "[[ ftst tm truep end test ]]" \item "[[ ftst to truep end test ]]" \item "[[ ftst tO truep end test ]]" \end{statements}" ]" \subsection{falsep} "[ "\begin{statements} \item "[[ ftst tt falsep end test ]]" \item "[[ ttst tf falsep end test ]]" \item "[[ ftst 1 falsep end test ]]" \item "[[ ftst 2 falsep end test ]]" \item "[[ ftst -2 falsep end test ]]" \item "[[ ftst ta falsep end test ]]" \item "[[ ftst tb falsep end test ]]" \item "[[ ftst tc falsep end test ]]" \item "[[ ftst td falsep end test ]]" \item "[[ etst tx ; tx falsep end test ]]" \item "[[ etst ty ; ty falsep end test ]]" \item "[[ ftst tm falsep end test ]]" \item "[[ ftst to falsep end test ]]" \item "[[ ftst tO falsep end test ]]" \end{statements}" ]" \subsection{if-then-else} "[ "\begin{statements} \item "[[ ttst if tt then tt else tt end test ]]" \item "[[ ttst if tt then tt else tf end test ]]" \item "[[ ftst if tt then tf else tt end test ]]" \item "[[ ftst if tt then tf else tf end test ]]" \item "[[ ttst if tf then tt else tt end test ]]" \item "[[ ftst if tf then tt else tf end test ]]" \item "[[ ttst if tf then tf else tt end test ]]" \item "[[ ftst if tf then tf else tf end test ]]" \item "[[ ftst if tf then tf else tf end test ]]" \item "[[ etst 8 ; if 1 then 7 else 8 end test ]]" \item "[[ etst 8 ; if 2 then 7 else 8 end test ]]" \item "[[ etst 8 ; if -2 then 7 else 8 end test ]]" \item "[[ etst 8 ; if ta then 7 else 8 end test ]]" \item "[[ etst 8 ; if tb then 7 else 8 end test ]]" \item "[[ etst 8 ; if tc then 7 else 8 end test ]]" \item "[[ etst 8 ; if td then 7 else 8 end test ]]" \item "[[ etst 8 ; if tm then 7 else 8 end test ]]" \item "[[ etst tx ; if tx then 7 else 8 end test ]]" \item "[[ etst ty ; if ty then 7 else 8 end test ]]" \item "[[ etst 8 ; if to then 7 else 8 end test ]]" \item "[[ etst 8 ; if tO then 7 else 8 end test ]]" \end{statements}" ]" \subsection{not} "[ "\begin{statements} \item "[[ ftst .not. tt end test ]]" \item "[[ ttst .not. tf end test ]]" \item "[[ ttst .not. 1 end test ]]" \item "[[ ttst .not. 2 end test ]]" \item "[[ ttst .not. -2 end test ]]" \item "[[ ttst .not. ta end test ]]" \item "[[ ttst .not. tb end test ]]" \item "[[ ttst .not. tc end test ]]" \item "[[ ttst .not. td end test ]]" \item "[[ etst tx ; .not. tx end test ]]" \item "[[ etst ty ; .not. ty end test ]]" \item "[[ ttst .not. tm end test ]]" \item "[[ ttst .not. to end test ]]" \item "[[ ttst .not. tO end test ]]" \end{statements}" ]" \subsection{notnot} "[ "\begin{statements} \item "[[ ttst notnot tt end test ]]" \item "[[ ftst notnot tf end test ]]" \item "[[ ftst notnot 1 end test ]]" \item "[[ ftst notnot 2 end test ]]" \item "[[ ftst notnot -2 end test ]]" \item "[[ ftst notnot ta end test ]]" \item "[[ ftst notnot tb end test ]]" \item "[[ ftst notnot tc end test ]]" \item "[[ ftst notnot td end test ]]" \item "[[ etst tx ; notnot tx end test ]]" \item "[[ etst ty ; notnot ty end test ]]" \item "[[ ftst notnot tm end test ]]" \item "[[ ftst notnot to end test ]]" \item "[[ ftst notnot tO end test ]]" \end{statements}" ]" \subsection{and} "[ "\begin{statements} \item "[[ ttst tt .and. tt end test ]]" \item "[[ ftst tt .and. tf end test ]]" \item "[[ etst tx ; tt .and. tx end test ]]" \item "[[ etst ty ; tt .and. ty end test ]]" \item "[[ ftst tf .and. tt end test ]]" \item "[[ ftst tf .and. tf end test ]]" \item "[[ ftst tf .and. tx end test ]]" \item "[[ ftst tf .and. ty end test ]]" \item "[[ ftst tf .and. bottom end test ]]" \item "[[ etst tx ; tx .and. tt end test ]]" \item "[[ etst tx ; tx .and. tf end test ]]" \item "[[ etst tx ; tx .and. tx end test ]]" \item "[[ etst tx ; tx .and. ty end test ]]" \item "[[ etst tx ; tx .and. bottom end test ]]" \item "[[ etst ty ; ty .and. tt end test ]]" \item "[[ etst ty ; ty .and. tf end test ]]" \item "[[ etst ty ; ty .and. tx end test ]]" \item "[[ etst ty ; ty .and. ty end test ]]" \item "[[ etst ty ; ty .and. bottom end test ]]" \item "[[ etst 1 ; 1 .and. tf end test ]]" \item "[[ etst 2 ; 2 .and. tf end test ]]" \item "[[ etst -2 ; -2 .and. tf end test ]]" \item "[[ etst ta ; ta .and. tf end test ]]" \item "[[ etst tb ; tb .and. tf end test ]]" \item "[[ etst tc ; tc .and. tf end test ]]" \item "[[ etst td ; td .and. tf end test ]]" \item "[[ etst tm ; tm .and. tf end test ]]" \item "[[ etst to ; to .and. tf end test ]]" \item "[[ etst tO ; tO .and. tf end test ]]" \item "[[ etst 1 ; tt .and. 1 end test ]]" \item "[[ etst 2 ; tt .and. 2 end test ]]" \item "[[ etst -2 ; tt .and. -2 end test ]]" \item "[[ etst ta ; tt .and. ta end test ]]" \item "[[ etst tb ; tt .and. tb end test ]]" \item "[[ etst tc ; tt .and. tc end test ]]" \item "[[ etst td ; tt .and. td end test ]]" \item "[[ etst tm ; tt .and. tm end test ]]" \item "[[ etst to ; tt .and. to end test ]]" \item "[[ etst tO ; tt .and. tO end test ]]" \end{statements}" ]" \subsection{or} "[ "\begin{statements} \item "[[ ttst tt .or. tt end test ]]" \item "[[ ttst tt .or. tf end test ]]" \item "[[ ttst tt .or. tx end test ]]" \item "[[ ttst tf .or. tt end test ]]" \item "[[ ftst tf .or. tf end test ]]" \item "[[ etst tx ; tf .or. tx end test ]]" \item "[[ etst tx ; tx .or. tt end test ]]" \item "[[ etst tx ; tx .or. tf end test ]]" \item "[[ etst ty ; ty .or. tx end test ]]" \item "[[ etst 8 ; 1 .or. 8 end test ]]" \item "[[ etst 8 ; 2 .or. 8 end test ]]" \item "[[ etst 8 ; -2 .or. 8 end test ]]" \item "[[ etst 8 ; ta .or. 8 end test ]]" \item "[[ etst 8 ; tb .or. 8 end test ]]" \item "[[ etst 8 ; tc .or. 8 end test ]]" \item "[[ etst 8 ; td .or. 8 end test ]]" \item "[[ etst 8 ; tm .or. 8 end test ]]" \item "[[ etst 8 ; to .or. 8 end test ]]" \item "[[ etst 8 ; tO .or. 8 end test ]]" \item "[[ etst 1 ; 2 .or. 1 end test ]]" \item "[[ etst 2 ; -2 .or. 2 end test ]]" \item "[[ etst -2 ; ta .or. -2 end test ]]" \item "[[ etst ta ; tb .or. ta end test ]]" \item "[[ etst tb ; tc .or. tb end test ]]" \item "[[ etst tc ; td .or. tc end test ]]" \item "[[ etst td ; tm .or. td end test ]]" \item "[[ etst tm ; to .or. tm end test ]]" \item "[[ etst to ; tO .or. to end test ]]" \item "[[ etst tO ; 1 .or. tO end test ]]" \end{statements}" ]" \subsection{"[[ x = y ]]"} "[ "\begin{statements} \item "[[ ttst tt = tt end test ]]" \item "[[ ftst tt = tf end test ]]" \item "[[ ftst tt = 1 end test ]]" \item "[[ ftst tt = 2 end test ]]" \item "[[ ftst tt = -2 end test ]]" \item "[[ ftst tt = ta end test ]]" \item "[[ ftst tt = tb end test ]]" \item "[[ ftst tt = tc end test ]]" \item "[[ ftst tt = td end test ]]" \item "[[ etst ty ; tt = ty end test ]]" \item "[[ ftst tt = tm end test ]]" \item "[[ ftst tt = to end test ]]" \item "[[ ftst tt = tO end test ]]" \item "[[ ftst tf = tt end test ]]" \item "[[ ttst tf = tf end test ]]" \item "[[ ftst tf = 1 end test ]]" \item "[[ ftst tf = 2 end test ]]" \item "[[ ftst tf = -2 end test ]]" \item "[[ ftst tf = ta end test ]]" \item "[[ ftst tf = tb end test ]]" \item "[[ ftst tf = tc end test ]]" \item "[[ ftst tf = td end test ]]" \item "[[ etst ty ; tf = ty end test ]]" \item "[[ ftst tf = tm end test ]]" \item "[[ ftst tf = to end test ]]" \item "[[ ftst tf = tO end test ]]" \item "[[ ftst 1 = tt end test ]]" \item "[[ ftst 1 = tf end test ]]" \item "[[ ttst 1 = 1 end test ]]" \item "[[ ftst 1 = 2 end test ]]" \item "[[ ftst 1 = -2 end test ]]" \item "[[ ftst 1 = ta end test ]]" \item "[[ ftst 1 = tb end test ]]" \item "[[ ftst 1 = tc end test ]]" \item "[[ ftst 1 = td end test ]]" \item "[[ etst ty ; 1 = ty end test ]]" \item "[[ ftst 1 = tm end test ]]" \item "[[ ftst 1 = to end test ]]" \item "[[ ftst 1 = tO end test ]]" \item "[[ ftst 2 = tt end test ]]" \item "[[ ftst 2 = tf end test ]]" \item "[[ ftst 2 = 1 end test ]]" \item "[[ ttst 2 = 2 end test ]]" \item "[[ ftst 2 = -2 end test ]]" \item "[[ ftst 2 = ta end test ]]" \item "[[ ftst 2 = tb end test ]]" \item "[[ ftst 2 = tc end test ]]" \item "[[ ftst 2 = td end test ]]" \item "[[ etst ty ; 2 = ty end test ]]" \item "[[ ftst 2 = tm end test ]]" \item "[[ ftst 2 = to end test ]]" \item "[[ ftst 2 = tO end test ]]" \item "[[ ftst -2 = tt end test ]]" \item "[[ ftst -2 = tf end test ]]" \item "[[ ftst -2 = 1 end test ]]" \item "[[ ftst -2 = 2 end test ]]" \item "[[ ttst -2 = -2 end test ]]" \item "[[ ftst -2 = ta end test ]]" \item "[[ ftst -2 = tb end test ]]" \item "[[ ftst -2 = tc end test ]]" \item "[[ ftst -2 = td end test ]]" \item "[[ etst ty ; -2 = ty end test ]]" \item "[[ ftst -2 = tm end test ]]" \item "[[ ftst -2 = to end test ]]" \item "[[ ftst -2 = tO end test ]]" \item "[[ ftst ta = tt end test ]]" \item "[[ ftst ta = tf end test ]]" \item "[[ ftst ta = 1 end test ]]" \item "[[ ftst ta = 2 end test ]]" \item "[[ ftst ta = -2 end test ]]" \item "[[ ttst ta = ta end test ]]" \item "[[ ftst ta = tb end test ]]" \item "[[ ftst ta = tc end test ]]" \item "[[ ftst ta = td end test ]]" \item "[[ etst ty ; ta = ty end test ]]" \item "[[ ftst ta = tm end test ]]" \item "[[ ftst ta = to end test ]]" \item "[[ ftst ta = tO end test ]]" \item "[[ ftst tb = tt end test ]]" \item "[[ ftst tb = tf end test ]]" \item "[[ ftst tb = 1 end test ]]" \item "[[ ftst tb = 2 end test ]]" \item "[[ ftst tb = -2 end test ]]" \item "[[ ftst tb = ta end test ]]" \item "[[ ttst tb = tb end test ]]" \item "[[ ftst tb = tc end test ]]" \item "[[ ftst tb = td end test ]]" \item "[[ etst ty ; tb = ty end test ]]" \item "[[ ftst tb = tm end test ]]" \item "[[ ftst tb = to end test ]]" \item "[[ ftst tb = tO end test ]]" \item "[[ ftst tc = tt end test ]]" \item "[[ ftst tc = tf end test ]]" \item "[[ ftst tc = 1 end test ]]" \item "[[ ftst tc = 2 end test ]]" \item "[[ ftst tc = -2 end test ]]" \item "[[ ftst tc = ta end test ]]" \item "[[ ftst tc = tb end test ]]" \item "[[ ttst tc = tc end test ]]" \item "[[ ftst tc = td end test ]]" \item "[[ etst ty ; tc = ty end test ]]" \item "[[ ftst tc = tm end test ]]" \item "[[ ftst tc = to end test ]]" \item "[[ ftst tc = tO end test ]]" \item "[[ ftst td = tt end test ]]" \item "[[ ftst td = tf end test ]]" \item "[[ ftst td = 1 end test ]]" \item "[[ ftst td = 2 end test ]]" \item "[[ ftst td = -2 end test ]]" \item "[[ ftst td = ta end test ]]" \item "[[ ftst td = tb end test ]]" \item "[[ ftst td = tc end test ]]" \item "[[ ttst td = td end test ]]" \item "[[ etst ty ; td = ty end test ]]" \item "[[ ftst td = tm end test ]]" \item "[[ ftst td = to end test ]]" \item "[[ ftst td = tO end test ]]" \item "[[ etst ty ; ty = tt end test ]]" \item "[[ etst ty ; ty = tf end test ]]" \item "[[ etst ty ; ty = 1 end test ]]" \item "[[ etst ty ; ty = 2 end test ]]" \item "[[ etst ty ; ty = -2 end test ]]" \item "[[ etst ty ; ty = ta end test ]]" \item "[[ etst ty ; ty = tb end test ]]" \item "[[ etst ty ; ty = tc end test ]]" \item "[[ etst ty ; ty = td end test ]]" \item "[[ etst ty ; ty = tx end test ]]" \item "[[ etst ty ; ty = tm end test ]]" \item "[[ etst ty ; ty = to end test ]]" \item "[[ etst ty ; ty = tO end test ]]" \item "[[ ftst tm = tt end test ]]" \item "[[ ftst tm = tf end test ]]" \item "[[ ftst tm = 1 end test ]]" \item "[[ ftst tm = 2 end test ]]" \item "[[ ftst tm = -2 end test ]]" \item "[[ ftst tm = ta end test ]]" \item "[[ ftst tm = tb end test ]]" \item "[[ ftst tm = tc end test ]]" \item "[[ ftst tm = td end test ]]" \item "[[ etst ty ; tm = ty end test ]]" \item "[[ ttst tm = tm end test ]]" \item "[[ ftst tm = to end test ]]" \item "[[ ftst tm = tO end test ]]" \item "[[ ftst to = tt end test ]]" \item "[[ ftst to = tf end test ]]" \item "[[ ftst to = 1 end test ]]" \item "[[ ftst to = 2 end test ]]" \item "[[ ftst to = -2 end test ]]" \item "[[ ftst to = ta end test ]]" \item "[[ ftst to = tb end test ]]" \item "[[ ftst to = tc end test ]]" \item "[[ ftst to = td end test ]]" \item "[[ etst ty ; to = ty end test ]]" \item "[[ ftst to = tm end test ]]" \item "[[ ttst to = to end test ]]" \item "[[ ftst to = tO end test ]]" \item "[[ ftst tO = tt end test ]]" \item "[[ ftst tO = tf end test ]]" \item "[[ ftst tO = 1 end test ]]" \item "[[ ftst tO = 2 end test ]]" \item "[[ ftst tO = -2 end test ]]" \item "[[ ftst tO = ta end test ]]" \item "[[ ftst tO = tb end test ]]" \item "[[ ftst tO = tc end test ]]" \item "[[ ftst tO = td end test ]]" \item "[[ etst ty ; tO = ty end test ]]" \item "[[ ftst tO = tm end test ]]" \item "[[ ftst tO = to end test ]]" \item "[[ ttst tO = tO end test ]]" \item "[[ ttst ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: tf ) :: ( ta :: tb ) ) end test ]]" \item "[[ ftst ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tc :: tf ) :: ( ta :: tb ) ) end test ]]" \item "[[ ftst ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: tc ) :: ( ta :: tb ) ) end test ]]" \item "[[ ftst ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: tf ) :: ( tc :: tb ) ) end test ]]" \item "[[ ftst ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: tf ) :: ( ta :: tc ) ) end test ]]" \item "[[ etst ty ; ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( ty :: tf ) :: ( ta :: tb ) ) end test ]]" \item "[[ etst ty ; ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: ty ) :: ( ta :: tb ) ) end test ]]" \item "[[ etst ty ; ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: tf ) :: ( ty :: tb ) ) end test ]]" \item "[[ etst ty ; ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: tf ) :: ( ta :: ty ) ) end test ]]" \item "[[ etst ty ; ( ( tt :: tf ) :: ( ta :: tb ) ) = ( ( tt :: ty ) :: ( tz :: tb ) ) end test ]]" \end{statements}" ]" \subsection{"[[ x != y ]]"} "[ "\begin{statements} \item "[[ ftst tt != tt end test ]]" \item "[[ ttst tt != tf end test ]]" \item "[[ etst ty ; tt != ty end test ]]" \item "[[ ttst tf != tt end test ]]" \item "[[ ftst tf != tf end test ]]" \item "[[ etst ty ; tf != ty end test ]]" \item "[[ etst ty ; ty != tt end test ]]" \item "[[ etst ty ; ty != tf end test ]]" \item "[[ etst ty ; ty != tx end test ]]" \end{statements}" ]" \section{Integers} \subsection{intp} "[ "\begin{statements} \item "[[ ftst tt intp end test ]]" \item "[[ ftst tf intp end test ]]" \item "[[ ttst 1 intp end test ]]" \item "[[ ttst 2 intp end test ]]" \item "[[ ttst -2 intp end test ]]" \item "[[ ftst ta intp end test ]]" \item "[[ ftst tb intp end test ]]" \item "[[ ftst tc intp end test ]]" \item "[[ ftst td intp end test ]]" \item "[[ etst ty ; ty intp end test ]]" \item "[[ ftst tm intp end test ]]" \item "[[ ftst to intp end test ]]" \item "[[ ftst tO intp end test ]]" \end{statements}" ]" \subsection{TheInt} "[ "\begin{statements} \item "[[ ttst TheInt ( true , Zero ) = TheInt ( false , Zero ) end test ]]" \item "[[ ttst TheInt ( true , Zero ) = 0 end test ]]" \item "[[ ttst TheInt ( true , One ) = 1 end test ]]" \item "[[ ttst TheInt ( true , Two ) = 2 end test ]]" \item "[[ ttst TheInt ( true , Three ) = 3 end test ]]" \item "[[ ttst TheInt ( true , Four ) = 4 end test ]]" \item "[[ ttst TheInt ( true , Five ) = 5 end test ]]" \item "[[ ttst TheInt ( true , Six ) = 6 end test ]]" \item "[[ ttst TheInt ( true , Seven ) = 7 end test ]]" \item "[[ ttst TheInt ( true , Eight ) = 8 end test ]]" \item "[[ ttst TheInt ( true , Nine ) = 9 end test ]]" \item "[[ ttst TheInt ( false , Zero ) = - 0 end test ]]" \item "[[ ttst TheInt ( false , One ) = -1 end test ]]" \item "[[ ttst TheInt ( false , Two ) = -2 end test ]]" \item "[[ ttst TheInt ( false , Three ) = -3 end test ]]" \item "[[ ttst TheInt ( false , Four ) = -4 end test ]]" \item "[[ ttst TheInt ( false , Five ) = -5 end test ]]" \item "[[ ttst TheInt ( false , Six ) = -6 end test ]]" \item "[[ ttst TheInt ( false , Seven ) = -7 end test ]]" \item "[[ ttst TheInt ( false , Eight ) = -8 end test ]]" \item "[[ ttst TheInt ( false , Nine ) = -9 end test ]]" \end{statements}" ]" \subsection{PlusTag} "[ "\begin{statements} \item "[[ ttst PlusTag ( Zero ) = 0 end test ]]" \item "[[ ttst PlusTag ( One ) = 1 end test ]]" \item "[[ ttst PlusTag ( Two ) = 2 end test ]]" \item "[[ ttst PlusTag ( Three ) = 3 end test ]]" \item "[[ ttst PlusTag ( Four ) = 4 end test ]]" \item "[[ ttst PlusTag ( Five ) = 5 end test ]]" \item "[[ ttst PlusTag ( Six ) = 6 end test ]]" \item "[[ ttst PlusTag ( Seven ) = 7 end test ]]" \item "[[ ttst PlusTag ( Eight ) = 8 end test ]]" \item "[[ ttst PlusTag ( Nine ) = 9 end test ]]" \end{statements}" ]" \subsection{MinusTag} "[ "\begin{statements} \item "[[ ttst MinusTag ( Zero ) = - 0 end test ]]" \item "[[ ttst MinusTag ( One ) = -1 end test ]]" \item "[[ ttst MinusTag ( Two ) = -2 end test ]]" \item "[[ ttst MinusTag ( Three ) = -3 end test ]]" \item "[[ ttst MinusTag ( Four ) = -4 end test ]]" \item "[[ ttst MinusTag ( Five ) = -5 end test ]]" \item "[[ ttst MinusTag ( Six ) = -6 end test ]]" \item "[[ ttst MinusTag ( Seven ) = -7 end test ]]" \item "[[ ttst MinusTag ( Eight ) = -8 end test ]]" \item "[[ ttst MinusTag ( Nine ) = -9 end test ]]" \end{statements}" ]" \subsection{"[[ x + y ]]"} "[ "\begin{statements} \item "[[ etst tx ; tt + 1 end test ]]" \item "[[ etst tx ; tf + 1 end test ]]" \item "[[ etst tx ; ta + 1 end test ]]" \item "[[ etst tx ; tb + 1 end test ]]" \item "[[ etst tx ; tc + 1 end test ]]" \item "[[ etst tx ; td + 1 end test ]]" \item "[[ etst tx ; tx + 1 end test ]]" \item "[[ etst ty ; ty + 1 end test ]]" \item "[[ etst tx ; tm + 1 end test ]]" \item "[[ etst tx ; to + 1 end test ]]" \item "[[ etst tx ; tO + 1 end test ]]" \item "[[ etst tx ; 1 + tt end test ]]" \item "[[ etst tx ; 1 + tf end test ]]" \item "[[ etst tx ; 1 + ta end test ]]" \item "[[ etst tx ; 1 + tb end test ]]" \item "[[ etst tx ; 1 + tc end test ]]" \item "[[ etst tx ; 1 + td end test ]]" \item "[[ etst tx ; 1 + tx end test ]]" \item "[[ etst ty ; 1 + ty end test ]]" \item "[[ etst tx ; 1 + tm end test ]]" \item "[[ etst tx ; 1 + to end test ]]" \item "[[ etst tx ; 1 + tO end test ]]" \item "[[ etst ty ; ta + ty end test ]]" \item "[[ etst ty ; ty + ta end test ]]" \item "[[ etst ty ; ty + bottom end test ]]" \item "[[ ttst 2 + 3 = 5 end test ]]" \item "[[ ttst 2 + -3 = -1 end test ]]" \item "[[ ttst -2 + 3 = 1 end test ]]" \item "[[ ttst -2 + -3 = -5 end test ]]" \item "[[ ttst 3 + 2 = 5 end test ]]" \item "[[ ttst -3 + 2 = -1 end test ]]" \item "[[ ttst 3 + -2 = 1 end test ]]" \item "[[ ttst -3 + -2 = -5 end test ]]" \end{statements}" ]" \subsection{"[[ x - y ]]"} "[ "\begin{statements} \item "[[ etst tx ; tt - 1 end test ]]" \item "[[ etst tx ; tf - 1 end test ]]" \item "[[ etst tx ; ta - 1 end test ]]" \item "[[ etst tx ; tb - 1 end test ]]" \item "[[ etst tx ; tc - 1 end test ]]" \item "[[ etst tx ; td - 1 end test ]]" \item "[[ etst tx ; tx - 1 end test ]]" \item "[[ etst ty ; ty - 1 end test ]]" \item "[[ etst tx ; tm - 1 end test ]]" \item "[[ etst tx ; to - 1 end test ]]" \item "[[ etst tx ; tO - 1 end test ]]" \item "[[ etst tx ; 1 - tt end test ]]" \item "[[ etst tx ; 1 - tf end test ]]" \item "[[ etst tx ; 1 - ta end test ]]" \item "[[ etst tx ; 1 - tb end test ]]" \item "[[ etst tx ; 1 - tc end test ]]" \item "[[ etst tx ; 1 - td end test ]]" \item "[[ etst tx ; 1 - tx end test ]]" \item "[[ etst ty ; 1 - ty end test ]]" \item "[[ etst tx ; 1 - tm end test ]]" \item "[[ etst tx ; 1 - to end test ]]" \item "[[ etst tx ; 1 - tO end test ]]" \item "[[ etst ty ; ty - ta end test ]]" \item "[[ etst ty ; ta - ty end test ]]" \item "[[ etst ty ; ty - bottom end test ]]" \item "[[ ttst 2 - 3 = -1 end test ]]" \item "[[ ttst 2 - -3 = 5 end test ]]" \item "[[ ttst -2 - 3 = -5 end test ]]" \item "[[ ttst -2 - -3 = 1 end test ]]" \item "[[ ttst 3 - 2 = 1 end test ]]" \item "[[ ttst -3 - 2 = -5 end test ]]" \item "[[ ttst 3 - -2 = 5 end test ]]" \item "[[ ttst -3 - -2 = -1 end test ]]" \end{statements}" ]" \subsection{"[[ x * y ]]"} "[ "\begin{statements} \item "[[ etst tx ; tt * 1 end test ]]" \item "[[ etst tx ; tf * 1 end test ]]" \item "[[ etst tx ; ta * 1 end test ]]" \item "[[ etst tx ; tb * 1 end test ]]" \item "[[ etst tx ; tc * 1 end test ]]" \item "[[ etst tx ; td * 1 end test ]]" \item "[[ etst tx ; tx * 1 end test ]]" \item "[[ etst ty ; ty * 1 end test ]]" \item "[[ etst tx ; tm * 1 end test ]]" \item "[[ etst tx ; to * 1 end test ]]" \item "[[ etst tx ; tO * 1 end test ]]" \item "[[ etst tx ; 1 * tt end test ]]" \item "[[ etst tx ; 1 * tf end test ]]" \item "[[ etst tx ; 1 * ta end test ]]" \item "[[ etst tx ; 1 * tb end test ]]" \item "[[ etst tx ; 1 * tc end test ]]" \item "[[ etst tx ; 1 * td end test ]]" \item "[[ etst tx ; 1 * tx end test ]]" \item "[[ etst ty ; 1 * ty end test ]]" \item "[[ etst tx ; 1 * tm end test ]]" \item "[[ etst tx ; 1 * to end test ]]" \item "[[ etst tx ; 1 * tO end test ]]" \item "[[ etst ty ; ty * ta end test ]]" \item "[[ etst ty ; ta * ty end test ]]" \item "[[ etst ty ; ty * bottom end test ]]" \item "[[ ttst 2 * 3 = 6 end test ]]" \item "[[ ttst 2 * -3 = -6 end test ]]" \item "[[ ttst -2 * 3 = -6 end test ]]" \item "[[ ttst -2 * -3 = 6 end test ]]" \item "[[ ttst 3 * 2 = 6 end test ]]" \item "[[ ttst -3 * 2 = -6 end test ]]" \item "[[ ttst 3 * -2 = -6 end test ]]" \item "[[ ttst -3 * -2 = 6 end test ]]" \end{statements}" ]" \subsection{"[[ x < y ]]"} "[ "\begin{statements} \item "[[ etst tx ; tt < 1 end test ]]" \item "[[ etst tx ; tf < 1 end test ]]" \item "[[ etst tx ; ta < 1 end test ]]" \item "[[ etst tx ; tb < 1 end test ]]" \item "[[ etst tx ; tc < 1 end test ]]" \item "[[ etst tx ; td < 1 end test ]]" \item "[[ etst tx ; tx < 1 end test ]]" \item "[[ etst ty ; ty < 1 end test ]]" \item "[[ etst tx ; tm < 1 end test ]]" \item "[[ etst tx ; to < 1 end test ]]" \item "[[ etst tx ; tO < 1 end test ]]" \item "[[ etst tx ; 1 < tt end test ]]" \item "[[ etst tx ; 1 < tf end test ]]" \item "[[ etst tx ; 1 < ta end test ]]" \item "[[ etst tx ; 1 < tb end test ]]" \item "[[ etst tx ; 1 < tc end test ]]" \item "[[ etst tx ; 1 < td end test ]]" \item "[[ etst tx ; 1 < tx end test ]]" \item "[[ etst ty ; 1 < ty end test ]]" \item "[[ etst tx ; 1 < tm end test ]]" \item "[[ etst tx ; 1 < to end test ]]" \item "[[ etst tx ; 1 < tO end test ]]" \item "[[ etst ty ; ty < ta end test ]]" \item "[[ etst ty ; ta < ty end test ]]" \item "[[ etst ty ; ty < bottom end test ]]" \item "[[ ttst 2 < 3 end test ]]" \item "[[ ftst 2 < -3 end test ]]" \item "[[ ttst -2 < 3 end test ]]" \item "[[ ftst -2 < -3 end test ]]" \item "[[ ftst 3 < 2 end test ]]" \item "[[ ttst -3 < 2 end test ]]" \item "[[ ftst 3 < -2 end test ]]" \item "[[ ttst -3 < -2 end test ]]" \item "[[ ftst 2 < 2 end test ]]" \item "[[ ftst -2 < -2 end test ]]" \end{statements}" ]" \subsection{"[[ x > y ]]"} "[ "\begin{statements} \item "[[ etst tx ; tt > 1 end test ]]" \item "[[ etst tx ; tf > 1 end test ]]" \item "[[ etst tx ; ta > 1 end test ]]" \item "[[ etst tx ; tb > 1 end test ]]" \item "[[ etst tx ; tc > 1 end test ]]" \item "[[ etst tx ; td > 1 end test ]]" \item "[[ etst tx ; tx > 1 end test ]]" \item "[[ etst ty ; ty > 1 end test ]]" \item "[[ etst tx ; tm > 1 end test ]]" \item "[[ etst tx ; to > 1 end test ]]" \item "[[ etst tx ; tO > 1 end test ]]" \item "[[ etst tx ; 1 > tt end test ]]" \item "[[ etst tx ; 1 > tf end test ]]" \item "[[ etst tx ; 1 > ta end test ]]" \item "[[ etst tx ; 1 > tb end test ]]" \item "[[ etst tx ; 1 > tc end test ]]" \item "[[ etst tx ; 1 > td end test ]]" \item "[[ etst tx ; 1 > tx end test ]]" \item "[[ etst ty ; 1 > ty end test ]]" \item "[[ etst tx ; 1 > tm end test ]]" \item "[[ etst tx ; 1 > to end test ]]" \item "[[ etst tx ; 1 > tO end test ]]" \item "[[ etst ty ; ty > ta end test ]]" \item "[[ etst ty ; ta > ty end test ]]" \item "[[ etst ty ; ty > bottom end test ]]" \item "[[ ftst 2 > 3 end test ]]" \item "[[ ttst 2 > -3 end test ]]" \item "[[ ftst -2 > 3 end test ]]" \item "[[ ttst -2 > -3 end test ]]" \item "[[ ttst 3 > 2 end test ]]" \item "[[ ftst -3 > 2 end test ]]" \item "[[ ttst 3 > -2 end test ]]" \item "[[ ftst -3 > -2 end test ]]" \item "[[ ftst 2 > 2 end test ]]" \item "[[ ftst -2 > -2 end test ]]" \end{statements}" ]" \subsection{"[[ x <= y ]]"} "[ "\begin{statements} \item "[[ etst tx ; tt <= 1 end test ]]" \item "[[ etst tx ; tf <= 1 end test ]]" \item "[[ etst tx ; ta <= 1 end test ]]" \item "[[ etst tx ; tb <= 1 end test ]]" \item "[[ etst tx ; tc <= 1 end test ]]" \item "[[ etst tx ; td <= 1 end test ]]" \item "[[ etst tx ; tx <= 1 end test ]]" \item "[[ etst ty ; ty <= 1 end test ]]" \item "[[ etst tx ; tm <= 1 end test ]]" \item "[[ etst tx ; to <= 1 end test ]]" \item "[[ etst tx ; tO <= 1 end test ]]" \item "[[ etst tx ; 1 <= tt end test ]]" \item "[[ etst tx ; 1 <= tf end test ]]" \item "[[ etst tx ; 1 <= ta end test ]]" \item "[[ etst tx ; 1 <= tb end test ]]" \item "[[ etst tx ; 1 <= tc end test ]]" \item "[[ etst tx ; 1 <= td end test ]]" \item "[[ etst tx ; 1 <= tx end test ]]" \item "[[ etst ty ; 1 <= ty end test ]]" \item "[[ etst tx ; 1 <= tm end test ]]" \item "[[ etst tx ; 1 <= to end test ]]" \item "[[ etst tx ; 1 <= tO end test ]]" \item "[[ etst ty ; ty <= ta end test ]]" \item "[[ etst ty ; ta <= ty end test ]]" \item "[[ etst ty ; ty <= bottom end test ]]" \item "[[ ttst 2 <= 3 end test ]]" \item "[[ ftst 2 <= -3 end test ]]" \item "[[ ttst -2 <= 3 end test ]]" \item "[[ ftst -2 <= -3 end test ]]" \item "[[ ftst 3 <= 2 end test ]]" \item "[[ ttst -3 <= 2 end test ]]" \item "[[ ftst 3 <= -2 end test ]]" \item "[[ ttst -3 <= -2 end test ]]" \item "[[ ttst 2 <= 2 end test ]]" \item "[[ ttst -2 <= -2 end test ]]" \end{statements}" ]" \subsection{"[[ x >= y ]]"} "[ "\begin{statements} \item "[[ etst tx ; tt >= 1 end test ]]" \item "[[ etst tx ; tf >= 1 end test ]]" \item "[[ etst tx ; ta >= 1 end test ]]" \item "[[ etst tx ; tb >= 1 end test ]]" \item "[[ etst tx ; tc >= 1 end test ]]" \item "[[ etst tx ; td >= 1 end test ]]" \item "[[ etst tx ; tx >= 1 end test ]]" \item "[[ etst ty ; ty >= 1 end test ]]" \item "[[ etst tx ; tm >= 1 end test ]]" \item "[[ etst tx ; to >= 1 end test ]]" \item "[[ etst tx ; tO >= 1 end test ]]" \item "[[ etst tx ; 1 >= tt end test ]]" \item "[[ etst tx ; 1 >= tf end test ]]" \item "[[ etst tx ; 1 >= ta end test ]]" \item "[[ etst tx ; 1 >= tb end test ]]" \item "[[ etst tx ; 1 >= tc end test ]]" \item "[[ etst tx ; 1 >= td end test ]]" \item "[[ etst tx ; 1 >= tx end test ]]" \item "[[ etst ty ; 1 >= ty end test ]]" \item "[[ etst tx ; 1 >= tm end test ]]" \item "[[ etst tx ; 1 >= to end test ]]" \item "[[ etst tx ; 1 >= tO end test ]]" \item "[[ etst ty ; ty >= ta end test ]]" \item "[[ etst ty ; ta >= ty end test ]]" \item "[[ etst ty ; ty >= bottom end test ]]" \item "[[ ftst 2 >= 3 end test ]]" \item "[[ ttst 2 >= -3 end test ]]" \item "[[ ftst -2 >= 3 end test ]]" \item "[[ ttst -2 >= -3 end test ]]" \item "[[ ttst 3 >= 2 end test ]]" \item "[[ ftst -3 >= 2 end test ]]" \item "[[ ttst 3 >= -2 end test ]]" \item "[[ ftst -3 >= -2 end test ]]" \item "[[ ttst 2 >= 2 end test ]]" \item "[[ ttst -2 >= -2 end test ]]" \end{statements}" ]" \subsection{Strings} "[ "\begin{statements} \item "[[ ttst "abc" intp end test ]]" \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 ]]" \item "[[ ttst "if" = %% %9 %1 %7 %5 %3 end test ]]" \end{statements}" ]" \section{Pairs} \subsection{pairp} "[ "\begin{statements} \item "[[ ftst tt pairp end test ]]" \item "[[ ftst tf pairp end test ]]" \item "[[ ftst 1 pairp end test ]]" \item "[[ ftst 2 pairp end test ]]" \item "[[ ftst -2 pairp end test ]]" \item "[[ ttst ta pairp end test ]]" \item "[[ ttst tb pairp end test ]]" \item "[[ ttst tc pairp end test ]]" \item "[[ ttst td pairp end test ]]" \item "[[ etst ty ; ty pairp end test ]]" \item "[[ ftst tm pairp end test ]]" \item "[[ ftst to pairp end test ]]" \item "[[ ftst tO pairp end test ]]" \end{statements}" ]" \subsection{head} "[ "\begin{statements} \item "[[ etst tt ; tt head end test ]]" \item "[[ etst tf ; tf head end test ]]" \item "[[ etst 1 ; 1 head end test ]]" \item "[[ etst 2 ; 2 head end test ]]" \item "[[ etst -2 ; -2 head end test ]]" \item "[[ ttst ta head = tt end test ]]" \item "[[ ttst tb head = tt end test ]]" \item "[[ ttst tc head = tf end test ]]" \item "[[ ttst td head = tf end test ]]" \item "[[ etst tx ; tx head end test ]]" \item "[[ etst ty ; ty head end test ]]" \item "[[ etst tm ; tm head end test ]]" \item "[[ etst to ; to head end test ]]" \item "[[ etst tO ; tO head end test ]]" \item "[[ ttst ( tt :: 1 ) head = tt end test ]]" \item "[[ ttst ( tf :: 1 ) head = tf end test ]]" \item "[[ ttst ( ta :: 1 ) head = ta end test ]]" \item "[[ ttst ( tb :: 1 ) head = tb end test ]]" \item "[[ ttst ( tc :: 1 ) head = tc end test ]]" \item "[[ ttst ( td :: 1 ) head = td end test ]]" \item "[[ etst ty ; ( ty :: 1 ) head = tt end test ]]" \item "[[ ttst ( tm :: 1 ) head = tm end test ]]" \item "[[ ttst ( to :: 1 ) head = to end test ]]" \item "[[ ttst ( tO :: 1 ) head = tO end test ]]" \end{statements}" ]" \subsection{tail} "[ "\begin{statements} \item "[[ etst tt ; tt tail end test ]]" \item "[[ etst tf ; tf tail end test ]]" \item "[[ etst 1 ; 1 tail end test ]]" \item "[[ etst 2 ; 2 tail end test ]]" \item "[[ etst -2 ; -2 tail end test ]]" \item "[[ ttst ta tail = tt end test ]]" \item "[[ ttst tb tail = tf end test ]]" \item "[[ ttst tc tail = tt end test ]]" \item "[[ ttst td tail = tf end test ]]" \item "[[ etst tx ; tx tail end test ]]" \item "[[ etst ty ; ty tail end test ]]" \item "[[ etst tm ; tm tail end test ]]" \item "[[ etst to ; to tail end test ]]" \item "[[ etst tO ; tO tail end test ]]" \item "[[ ttst ( 1 :: tt ) tail = tt end test ]]" \item "[[ ttst ( 1 :: tf ) tail = tf end test ]]" \item "[[ ttst ( 1 :: ta ) tail = ta end test ]]" \item "[[ ttst ( 1 :: tb ) tail = tb end test ]]" \item "[[ ttst ( 1 :: tc ) tail = tc end test ]]" \item "[[ ttst ( 1 :: td ) tail = td end test ]]" \item "[[ etst ty ; ( 1 :: ty ) tail = tt end test ]]" \item "[[ ttst ( 1 :: tm ) tail = tm end test ]]" \item "[[ ttst ( 1 :: to ) tail = to end test ]]" \item "[[ ttst ( 1 :: tO ) tail = tO end test ]]" \end{statements}" ]" \subsection{List operations} "[ "\begin{statements} \item "[[ etst revappend ( << 1 ,, 2 ,, 3 >> , << 4 ,, 5 ,, 6 >> ) ; << 3 ,, 2 ,, 1 ,, 4 ,, 5 ,, 6 >> end test ]]" \item "[[ etst reverse ( << 1 ,, 2 ,, 3 >> ) ; << 3 ,, 2 ,, 1 >> end test ]]" \item "[[ etst nth ( 2 , << 1 ,, 2 ,, 3 ,, 4 >> ) ; 3 end test ]]" \item "[[ etst length ( << 1 ,, 2 ,, 3 >> ) ; 3 end test ]]" \item "[[ etst list-prefix ( << 1 ,, 2 ,, 3 ,, 4 >> , 2 ) ; << 1 ,, 2 >> end test ]]" \item "[[ etst list-suffix ( << 1 ,, 2 ,, 3 ,, 4 >> , 2 ) ; << 3 ,, 4 >> end test ]]" \end{statements}" ]" \section{Exceptions} The following tests are merged from several sources. The merged test suite contains repetitions. "[ "\begin{statements} \item "[[ ttst exception catch head end test ]]" \item "[[ ftst true catch head end test ]]" \item "[[ ftst false catch head end test ]]" \item "[[ ftst %% %1 %1 %7 catch head end test ]]" \item "[[ ftst 0 catch head end test ]]" \item "[[ ftst ( - %% %1 %1 %7 ) catch head end test ]]" \item "[[ ftst ( true :: false ) catch head end test ]]" \item "[[ ftst map ( \ x . x ) catch head end test ]]" \item "[[ ttst exception catch tail = true end test ]]" \item "[[ ttst true catch tail = true end test ]]" \item "[[ ttst false catch tail = false end test ]]" \item "[[ ttst %% %1 %1 %7 catch tail = %% %1 %1 %7 end test ]]" \item "[[ ttst 0 catch tail = 0 end test ]]" \item "[[ ttst ( - %% %1 %1 %7 ) catch tail = ( - %% %1 %1 %7 ) end test ]]" \item "[[ ttst ( true :: false ) catch tail = ( true :: false ) end test ]]" \item "[[ ttst map ( \ x . x ) catch tail = map ( \ x . x ) end test ]]" \item "[[ ttst exception catch = true :: true end test ]]" \item "[[ ttst true catch = false :: true end test ]]" \item "[[ ttst false catch = false :: false end test ]]" \item "[[ ttst %% %1 %1 %7 catch = false :: %% %1 %1 %7 end test ]]" \item "[[ ttst 0 catch = false :: 0 end test ]]" \item "[[ ttst ( - %% %1 %1 %7 ) catch = false :: ( - %% %1 %1 %7 ) end test ]]" \item "[[ ttst ( true :: false ) catch = false :: ( true :: false ) end test ]]" \item "[[ ttst map ( \ x . x ) catch = false :: map ( \ x . x ) end test ]]" \item "[[ ttst tt catch = false :: tt end test ]]" \item "[[ ttst tf catch = false :: tf end test ]]" \item "[[ ttst 1 catch = false :: 1 end test ]]" \item "[[ ttst 2 catch = false :: 2 end test ]]" \item "[[ ttst -2 catch = false :: -2 end test ]]" \item "[[ ttst ta catch = false :: ta end test ]]" \item "[[ ttst tb catch = false :: tb end test ]]" \item "[[ ttst tc catch = false :: tc end test ]]" \item "[[ ttst td catch = false :: td end test ]]" \item "[[ ttst tx catch = true :: tt end test ]]" \item "[[ ttst ty catch = true :: 2 end test ]]" \item "[[ ttst tz catch = true :: 3 end test ]]" \item "[[ ttst tm catch = false :: tm end test ]]" \item "[[ ttst to catch = false :: to end test ]]" \item "[[ ttst tO catch = false :: tO end test ]]" \item "[[ ttst 2 raise catch = true :: 2 end test ]]" \item "[[ ttst 2 raise raise catch = true :: 2 end test ]]" \end{statements}" ]" \section{Maps} \subsection{mapp} "[ "\begin{statements} \item "[[ ftst tt mapp end test ]]" \item "[[ ftst tf mapp end test ]]" \item "[[ ftst 1 mapp end test ]]" \item "[[ ftst 2 mapp end test ]]" \item "[[ ftst -2 mapp end test ]]" \item "[[ ftst ta mapp end test ]]" \item "[[ ftst tb mapp end test ]]" \item "[[ ftst tc mapp end test ]]" \item "[[ ftst td mapp end test ]]" \item "[[ etst ty ; ty mapp end test ]]" \item "[[ ttst tm mapp end test ]]" \item "[[ ftst to mapp end test ]]" \item "[[ ftst tO mapp end test ]]" \end{statements}" ]" \subsection{map} "[ "\begin{statements} \item "[[ ttst map ( tt ) = tm end test ]]" \item "[[ ttst map ( tf ) = tm end test ]]" \item "[[ ttst map ( 1 ) = tm end test ]]" \item "[[ ttst map ( 2 ) = tm end test ]]" \item "[[ ttst map ( -2 ) = tm end test ]]" \item "[[ ttst map ( ta ) = tm end test ]]" \item "[[ ttst map ( tb ) = tm end test ]]" \item "[[ ttst map ( tc ) = tm end test ]]" \item "[[ ttst map ( td ) = tm end test ]]" \item "[[ ttst map ( tx ) = tm end test ]]" \item "[[ ttst map ( ty ) = tm end test ]]" \item "[[ ttst map ( tm ) = tm end test ]]" \item "[[ ttst map ( to ) = tm end test ]]" \item "[[ ttst map ( tO ) = tm end test ]]" \end{statements}" ]" \subsection{catching maptag} "[ "\begin{statements} \item "[[ ttst tt catching maptag = tm end test ]]" \item "[[ ttst tf catching maptag = tm end test ]]" \item "[[ ttst 1 catching maptag = tm end test ]]" \item "[[ ttst 2 catching maptag = tm end test ]]" \item "[[ ttst -2 catching maptag = tm end test ]]" \item "[[ ttst ta catching maptag = tm end test ]]" \item "[[ ttst tb catching maptag = tm end test ]]" \item "[[ ttst tc catching maptag = tm end test ]]" \item "[[ ttst td catching maptag = tm end test ]]" \item "[[ ttst tx catching maptag = tm end test ]]" \item "[[ ttst ty catching maptag = tm end test ]]" \item "[[ ttst tm catching maptag = tm end test ]]" \item "[[ ttst to catching maptag = tm end test ]]" \item "[[ ttst tO catching maptag = tm end test ]]" \end{statements}" ]" \subsection{maptag} "[ "\begin{statements} \item "[[ ttst tt maptag = tm end test ]]" \item "[[ ttst tf maptag = tm end test ]]" \item "[[ ttst 1 maptag = tm end test ]]" \item "[[ ttst 2 maptag = tm end test ]]" \item "[[ ttst -2 maptag = tm end test ]]" \item "[[ ttst ta maptag = tm end test ]]" \item "[[ ttst tb maptag = tm end test ]]" \item "[[ ttst tc maptag = tm end test ]]" \item "[[ ttst td maptag = tm end test ]]" \item "[[ etst tx ; tx maptag = tm end test ]]" \item "[[ etst ty ; ty maptag = tm end test ]]" \item "[[ ttst tm maptag = tm end test ]]" \item "[[ ttst to maptag = tm end test ]]" \item "[[ ttst tO maptag = tm end test ]]" \end{statements}" ]" \subsection{untag} "[ "\begin{statements} \item "[[ etst tx ; tt untag end test ]]" \item "[[ etst tx ; tf untag end test ]]" \item "[[ etst tx ; 1 untag end test ]]" \item "[[ etst tx ; 2 untag end test ]]" \item "[[ etst tx ; -2 untag end test ]]" \item "[[ etst tx ; ta untag end test ]]" \item "[[ etst tx ; tb untag end test ]]" \item "[[ etst tx ; tc untag end test ]]" \item "[[ etst tx ; td untag end test ]]" \item "[[ etst tx ; tx untag end test ]]" \item "[[ etst ty ; ty untag end test ]]" \item "[[ ttst tm untag = tf end test ]]" \item "[[ etst tx ; to untag end test ]]" \item "[[ etst tx ; tO untag end test ]]" \end{statements}" ]" \subsection{map+untag} "[ "\begin{statements} \item "[[ ttst map ( tt ) untag = tt end test ]]" \item "[[ ttst map ( tf ) untag = tf end test ]]" \item "[[ ttst map ( 1 ) untag = 1 end test ]]" \item "[[ ttst map ( 2 ) untag = 2 end test ]]" \item "[[ ttst map ( -2 ) untag = -2 end test ]]" \item "[[ ttst map ( ta ) untag = ta end test ]]" \item "[[ ttst map ( tb ) untag = tb end test ]]" \item "[[ ttst map ( tc ) untag = tc end test ]]" \item "[[ ttst map ( td ) untag = td end test ]]" \item "[[ etst tx ; map ( tx ) untag = tt end test ]]" \item "[[ etst ty ; map ( ty ) untag = tt end test ]]" \item "[[ ttst map ( tm ) untag = tm end test ]]" \item "[[ ttst map ( to ) untag = to end test ]]" \item "[[ ttst map ( tO ) untag = tO end test ]]" \end{statements}" ]" \subsection{catching maptag+untag} "[ "\begin{statements} \item "[[ ttst tt catching maptag untag = tt end test ]]" \item "[[ ttst tf catching maptag untag = tf end test ]]" \item "[[ ttst 1 catching maptag untag = 1 end test ]]" \item "[[ ttst 2 catching maptag untag = 2 end test ]]" \item "[[ ttst -2 catching maptag untag = -2 end test ]]" \item "[[ ttst ta catching maptag untag = ta end test ]]" \item "[[ ttst tb catching maptag untag = tb end test ]]" \item "[[ ttst tc catching maptag untag = tc end test ]]" \item "[[ ttst td catching maptag untag = td end test ]]" \item "[[ etst tx ; tx catching maptag untag = tt end test ]]" \item "[[ etst ty ; ty catching maptag untag = tt end test ]]" \item "[[ ttst tm catching maptag untag = tm end test ]]" \item "[[ ttst to catching maptag untag = to end test ]]" \item "[[ ttst tO catching maptag untag = tO end test ]]" \end{statements}" ]" \subsection{maptag+untag} "[ "\begin{statements} \item "[[ ttst tt maptag untag = tt end test ]]" \item "[[ ttst tf maptag untag = tf end test ]]" \item "[[ ttst 1 maptag untag = 1 end test ]]" \item "[[ ttst 2 maptag untag = 2 end test ]]" \item "[[ ttst -2 maptag untag = -2 end test ]]" \item "[[ ttst ta maptag untag = ta end test ]]" \item "[[ ttst tb maptag untag = tb end test ]]" \item "[[ ttst tc maptag untag = tc end test ]]" \item "[[ ttst td maptag untag = td end test ]]" \item "[[ etst tx ; tx maptag untag = tt end test ]]" \item "[[ etst ty ; ty maptag untag = tt end test ]]" \item "[[ ttst tm maptag untag = tm end test ]]" \item "[[ ttst to maptag untag = to end test ]]" \item "[[ ttst tO maptag untag = tO end test ]]" \end{statements}" ]" \subsection{root} "[ "\begin{statements} \item "[[ etst tx ; tt root end test ]]" \item "[[ etst tx ; tf root end test ]]" \item "[[ etst tx ; 1 root end test ]]" \item "[[ etst tx ; 2 root end test ]]" \item "[[ etst tx ; -2 root end test ]]" \item "[[ etst tx ; ta root end test ]]" \item "[[ etst tx ; tb root end test ]]" \item "[[ etst tx ; tc root end test ]]" \item "[[ etst tx ; td root end test ]]" \item "[[ etst tx ; tx root end test ]]" \item "[[ etst ty ; ty root end test ]]" \item "[[ ftst tm root end test ]]" \item "[[ etst tx ; to root end test ]]" \item "[[ etst tx ; tO root end test ]]" \end{statements}" ]" \subsection{map+root} "[ "\begin{statements} \item "[[ ttst map ( tt ) root end test ]]" \item "[[ ftst map ( tf ) root end test ]]" \item "[[ ftst map ( 1 ) root end test ]]" \item "[[ ftst map ( 2 ) root end test ]]" \item "[[ ftst map ( -2 ) root end test ]]" \item "[[ ftst map ( ta ) root end test ]]" \item "[[ ftst map ( tb ) root end test ]]" \item "[[ ftst map ( tc ) root end test ]]" \item "[[ ftst map ( td ) root end test ]]" \item "[[ ftst map ( tx ) root end test ]]" \item "[[ ftst map ( ty ) root end test ]]" \item "[[ ftst map ( tm ) root end test ]]" \item "[[ ftst map ( to ) root end test ]]" \item "[[ ftst map ( tO ) root end test ]]" \end{statements}" ]" \subsection{maptag+root} "[ "\begin{statements} \item "[[ ttst tt maptag root end test ]]" \item "[[ ftst tf maptag root end test ]]" \item "[[ ftst 1 maptag root end test ]]" \item "[[ ftst 2 maptag root end test ]]" \item "[[ ftst -2 maptag root end test ]]" \item "[[ ftst ta maptag root end test ]]" \item "[[ ftst tb maptag root end test ]]" \item "[[ ftst tc maptag root end test ]]" \item "[[ ftst td maptag root end test ]]" \item "[[ etst tx ; tx maptag root end test ]]" \item "[[ etst ty ; ty maptag root end test ]]" \item "[[ ftst tm maptag root end test ]]" \item "[[ ftst to maptag root end test ]]" \item "[[ ftst tO maptag root end test ]]" \end{statements}" ]" \subsection{apply} "[ "\begin{statements} \item "[[ ttst ( map ( \ x . x ) apply map ( tt ) ) root end test ]]" \item "[[ ftst ( map ( \ x . x ) apply map ( tf ) ) root end test ]]" \item "[[ ttst ( map ( \ x . \ y . x ) apply map ( tt ) apply map ( tt ) ) root end test ]]" \item "[[ ttst ( map ( \ x . \ y . x ) apply map ( tt ) apply map ( tf ) ) root end test ]]" \item "[[ ftst ( map ( \ x . \ y . x ) apply map ( tf ) apply map ( tt ) ) root end test ]]" \item "[[ ftst ( map ( \ x . \ y . x ) apply map ( tf ) apply map ( tf ) ) root end test ]]" \item "[[ ttst ( map ( \ x . \ y . y ) apply map ( tt ) apply map ( tt ) ) root end test ]]" \item "[[ ftst ( map ( \ x . \ y . y ) apply map ( tt ) apply map ( tf ) ) root end test ]]" \item "[[ ttst ( map ( \ x . \ y . y ) apply map ( tf ) apply map ( tt ) ) root end test ]]" \item "[[ ftst ( map ( \ x . \ y . y ) apply map ( tf ) apply map ( tf ) ) root end test ]]" \item "[[ ttst ( map ( \ f . \ x . f ' ( f ' x ) ) apply map ( \ f . \ x . f ' ( f ' x ) ) apply map ( \ x . x + 1 ) apply map ( 2 ) ) untag = 6 end test ]]" \end{statements}" ]" \section{Logical operations on integers} \subsection{half} "[ "\begin{statements} \item "[[ etst tx ; half ( tt ) end test ]]" \item "[[ etst ty ; half ( ty ) end test ]]" \item "[[ ttst 0 = half ( 0 ) end test ]]" \item "[[ ttst 0 = half ( 1 ) end test ]]" \item "[[ ttst 1 = half ( 2 ) end test ]]" \item "[[ ttst 1 = half ( 3 ) end test ]]" \item "[[ ttst 2 = half ( 4 ) end test ]]" \item "[[ ttst 2 = half ( 5 ) end test ]]" \item "[[ ttst 3 = half ( 6 ) end test ]]" \item "[[ ttst 3 = half ( 7 ) end test ]]" \item "[[ ttst 4 = half ( 8 ) end test ]]" \item "[[ ttst 4 = half ( 9 ) end test ]]" \item "[[ ttst 5 = half ( 10 ) end test ]]" \item "[[ ttst -1 = half ( -1 ) end test ]]" \item "[[ ttst -1 = half ( -2 ) end test ]]" \item "[[ ttst -2 = half ( -3 ) end test ]]" \item "[[ ttst -2 = half ( -4 ) end test ]]" \item "[[ ttst -3 = half ( -5 ) end test ]]" \item "[[ ttst -3 = half ( -6 ) end test ]]" \item "[[ ttst -4 = half ( -7 ) end test ]]" \item "[[ ttst -4 = half ( -8 ) end test ]]" \item "[[ ttst -5 = half ( -9 ) end test ]]" \item "[[ ttst -5 = half ( - 10 ) end test ]]" \item "[[ etst tx ; half ( ta ) end test ]]" \item "[[ etst tx ; half ( tb ) end test ]]" \item "[[ etst tx ; half ( tc ) end test ]]" \item "[[ etst tx ; half ( td ) end test ]]" \item "[[ etst tx ; half ( tx ) end test ]]" \item "[[ etst ty ; half ( ty ) end test ]]" \item "[[ etst tx ; half ( tm ) end test ]]" \item "[[ etst tx ; half ( to ) end test ]]" \item "[[ etst tx ; half ( tO ) end test ]]" \end{statements}" ]" \subsection{evenp} "[ "\begin{statements} \item "[[ etst tx ; evenp ( tt ) end test ]]" \item "[[ etst ty ; evenp ( ty ) end test ]]" \item "[[ ttst evenp ( 0 ) end test ]]" \item "[[ ftst evenp ( 1 ) end test ]]" \item "[[ ttst evenp ( 2 ) end test ]]" \item "[[ ftst evenp ( 3 ) end test ]]" \item "[[ ttst evenp ( 4 ) end test ]]" \item "[[ ftst evenp ( 5 ) end test ]]" \item "[[ ttst evenp ( 6 ) end test ]]" \item "[[ ftst evenp ( 7 ) end test ]]" \item "[[ ttst evenp ( 8 ) end test ]]" \item "[[ ftst evenp ( 9 ) end test ]]" \item "[[ ttst evenp ( 10 ) end test ]]" \item "[[ ftst evenp ( -1 ) end test ]]" \item "[[ ttst evenp ( -2 ) end test ]]" \item "[[ ftst evenp ( -3 ) end test ]]" \item "[[ ttst evenp ( -4 ) end test ]]" \item "[[ ftst evenp ( -5 ) end test ]]" \item "[[ ttst evenp ( -6 ) end test ]]" \item "[[ ftst evenp ( -7 ) end test ]]" \item "[[ ttst evenp ( -8 ) end test ]]" \item "[[ ftst evenp ( -9 ) end test ]]" \item "[[ ttst evenp ( - 10 ) end test ]]" \item "[[ etst tx ; evenp ( ta ) end test ]]" \item "[[ etst tx ; evenp ( tb ) end test ]]" \item "[[ etst tx ; evenp ( tc ) end test ]]" \item "[[ etst tx ; evenp ( td ) end test ]]" \item "[[ etst tx ; evenp ( tx ) end test ]]" \item "[[ etst ty ; evenp ( ty ) end test ]]" \item "[[ etst tx ; evenp ( tm ) end test ]]" \item "[[ etst tx ; evenp ( to ) end test ]]" \item "[[ etst tx ; evenp ( tO ) end test ]]" \end{statements}" ]" \subsection{small} "[ "\begin{statements} \item "[[ etst tx ; small ( tt ) end test ]]" \item "[[ etst tx ; small ( tf ) end test ]]" \item "[[ ttst small ( 0 ) end test ]]" \item "[[ ftst small ( 1 ) end test ]]" \item "[[ ftst small ( 2 ) end test ]]" \item "[[ ftst small ( 3 ) end test ]]" \item "[[ ftst small ( 4 ) end test ]]" \item "[[ ftst small ( 5 ) end test ]]" \item "[[ ftst small ( 6 ) end test ]]" \item "[[ ftst small ( 7 ) end test ]]" \item "[[ ftst small ( 8 ) end test ]]" \item "[[ ftst small ( 9 ) end test ]]" \item "[[ ftst small ( 10 ) end test ]]" \item "[[ ttst small ( -1 ) end test ]]" \item "[[ ftst small ( -2 ) end test ]]" \item "[[ ftst small ( -3 ) end test ]]" \item "[[ ftst small ( -4 ) end test ]]" \item "[[ ftst small ( -5 ) end test ]]" \item "[[ ftst small ( -6 ) end test ]]" \item "[[ ftst small ( -7 ) end test ]]" \item "[[ ftst small ( -8 ) end test ]]" \item "[[ ftst small ( -9 ) end test ]]" \item "[[ ftst small ( - 10 ) end test ]]" \item "[[ etst tx ; small ( ta ) end test ]]" \item "[[ etst tx ; small ( tb ) end test ]]" \item "[[ etst tx ; small ( tc ) end test ]]" \item "[[ etst tx ; small ( td ) end test ]]" \item "[[ etst tx ; small ( tx ) end test ]]" \item "[[ etst ty ; small ( ty ) end test ]]" \item "[[ etst tx ; small ( tm ) end test ]]" \item "[[ etst tx ; small ( to ) end test ]]" \item "[[ etst tx ; small ( tO ) end test ]]" \end{statements}" ]" \subsection{oddp} "[ "\begin{statements} \item "[[ etst tx ; oddp ( tt ) end test ]]" \item "[[ etst ty ; oddp ( ty ) end test ]]" \item "[[ ftst oddp ( 6 ) end test ]]" \item "[[ ftst oddp ( -6 ) end test ]]" \item "[[ ttst oddp ( 7 ) end test ]]" \item "[[ ttst oddp ( -7 ) end test ]]" \end{statements}" ]" \subsection{double} "[ "\begin{statements} \item "[[ etst tx ; double ( 1 , 2 ) end test ]]" \item "[[ etst tx ; double ( tt , tt ) end test ]]" \item "[[ etst ty ; double ( ty , bottom ) end test ]]" \item "[[ ttst 4 = double ( tf , 2 ) end test ]]" \item "[[ ttst 5 = double ( tt , 2 ) end test ]]" \item "[[ ttst -4 = double ( tf , -2 ) end test ]]" \item "[[ ttst -3 = double ( tt , -2 ) end test ]]" \end{statements}" ]" \subsection{lognot} "[ "\begin{statements} \item "[[ etst tx ; lognot ( tt ) end test ]]" \item "[[ etst ty ; lognot ( ty ) end test ]]" \item "[[ ttst 1 = lognot ( -2 ) end test ]]" \item "[[ ttst 0 = lognot ( -1 ) end test ]]" \item "[[ ttst -1 = lognot ( 0 ) end test ]]" \item "[[ ttst -2 = lognot ( 1 ) end test ]]" \end{statements}" ]" \subsection{logior} "[ "\begin{statements} \item "[[ etst tx ; logior ( tt , 2 ) end test ]]" \item "[[ etst tx ; logior ( 1 , tt ) end test ]]" \item "[[ etst ty ; logior ( ty , tz ) end test ]]" \item "[[ etst ty ; logior ( ty , bottom ) end test ]]" \item "[[ ttst 5 = logior ( 0 , 5 ) end test ]]" \item "[[ ttst 5 = logior ( 0 , 5 ) end test ]]" \item "[[ ttst 5 = logior ( 5 , 0 ) end test ]]" \item "[[ ttst -1 = logior ( -1 , 5 ) end test ]]" \item "[[ ttst -1 = logior ( 5 , -1 ) end test ]]" \item "[[ ttst 14 = logior ( 10 , 12 ) end test ]]" \end{statements}" ]" \subsection{logxor} "[ "\begin{statements} \item "[[ etst tx ; logxor ( tt , 2 ) end test ]]" \item "[[ etst tx ; logxor ( 1 , tt ) end test ]]" \item "[[ etst ty ; logxor ( ty , bottom ) end test ]]" \item "[[ ttst 5 = logxor ( 0 , 5 ) end test ]]" \item "[[ ttst 5 = logxor ( 5 , 0 ) end test ]]" \item "[[ ttst -6 = logxor ( -1 , 5 ) end test ]]" \item "[[ ttst -6 = logxor ( 5 , -1 ) end test ]]" \item "[[ ttst 6 = logxor ( 10 , 12 ) end test ]]" \end{statements}" ]" \subsection{logand} "[ "\begin{statements} \item "[[ etst tx ; logand ( tt , 2 ) end test ]]" \item "[[ etst tx ; logand ( 1 , tt ) end test ]]" \item "[[ etst ty ; logand ( ty , bottom ) end test ]]" \item "[[ ttst 0 = logand ( 0 , 5 ) end test ]]" \item "[[ ttst 0 = logand ( 5 , 0 ) end test ]]" \item "[[ ttst 5 = logand ( -1 , 5 ) end test ]]" \item "[[ ttst 5 = logand ( 5 , -1 ) end test ]]" \item "[[ ttst 8 = logand ( 10 , 12 ) end test ]]" \end{statements}" ]" \subsection{logeqv} "[ "\begin{statements} \item "[[ etst tx ; logeqv ( tt , 2 ) end test ]]" \item "[[ etst tx ; logeqv ( 1 , tt ) end test ]]" \item "[[ etst ty ; logeqv ( ty , bottom ) end test ]]" \item "[[ ttst -6 = logeqv ( 0 , 5 ) end test ]]" \item "[[ ttst -6 = logeqv ( 5 , 0 ) end test ]]" \item "[[ ttst 5 = logeqv ( -1 , 5 ) end test ]]" \item "[[ ttst 5 = logeqv ( 5 , -1 ) end test ]]" \item "[[ ttst -7 = logeqv ( 10 , 12 ) end test ]]" \end{statements}" ]" \subsection{lognand} "[ "\begin{statements} \item "[[ etst tx ; lognand ( tt , 2 ) end test ]]" \item "[[ etst tx ; lognand ( 1 , tt ) end test ]]" \item "[[ etst ty ; lognand ( ty , bottom ) end test ]]" \item "[[ ttst -1 = lognand ( 0 , 5 ) end test ]]" \item "[[ ttst -1 = lognand ( 5 , 0 ) end test ]]" \item "[[ ttst -6 = lognand ( -1 , 5 ) end test ]]" \item "[[ ttst -6 = lognand ( 5 , -1 ) end test ]]" \item "[[ ttst -9 = lognand ( 10 , 12 ) end test ]]" \end{statements}" ]" \subsection{lognor} "[ "\begin{statements} \item "[[ etst tx ; lognor ( tt , 2 ) end test ]]" \item "[[ etst tx ; lognor ( 1 , tt ) end test ]]" \item "[[ etst ty ; lognor ( ty , bottom ) end test ]]" \item "[[ ttst -6 = lognor ( 0 , 5 ) end test ]]" \item "[[ ttst -6 = lognor ( 5 , 0 ) end test ]]" \item "[[ ttst 0 = lognor ( -1 , 5 ) end test ]]" \item "[[ ttst 0 = lognor ( 5 , -1 ) end test ]]" \item "[[ ttst -15 = lognor ( 10 , 12 ) end test ]]" \end{statements}" ]" \subsection{logandc1} "[ "\begin{statements} \item "[[ etst tx ; logandc1 ( tt , 2 ) end test ]]" \item "[[ etst tx ; logandc1 ( 1 , tt ) end test ]]" \item "[[ etst ty ; logandc1 ( ty , bottom ) end test ]]" \item "[[ ttst 5 = logandc1 ( 0 , 5 ) end test ]]" \item "[[ ttst 0 = logandc1 ( 5 , 0 ) end test ]]" \item "[[ ttst 0 = logandc1 ( -1 , 5 ) end test ]]" \item "[[ ttst -6 = logandc1 ( 5 , -1 ) end test ]]" \item "[[ ttst 4 = logandc1 ( 10 , 12 ) end test ]]" \end{statements}" ]" \subsection{logandc2} "[ "\begin{statements} \item "[[ etst tx ; logandc2 ( tt , 2 ) end test ]]" \item "[[ etst tx ; logandc2 ( 1 , tt ) end test ]]" \item "[[ etst ty ; logandc2 ( ty , bottom ) end test ]]" \item "[[ ttst 0 = logandc2 ( 0 , 5 ) end test ]]" \item "[[ ttst 5 = logandc2 ( 5 , 0 ) end test ]]" \item "[[ ttst -6 = logandc2 ( -1 , 5 ) end test ]]" \item "[[ ttst 0 = logandc2 ( 5 , -1 ) end test ]]" \item "[[ ttst 2 = logandc2 ( 10 , 12 ) end test ]]" \end{statements}" ]" \subsection{logorc1} "[ "\begin{statements} \item "[[ etst tx ; logorc1 ( tt , 2 ) end test ]]" \item "[[ etst tx ; logorc1 ( 1 , tt ) end test ]]" \item "[[ etst ty ; logorc1 ( ty , bottom ) end test ]]" \item "[[ ttst -1 = logorc1 ( 0 , 5 ) end test ]]" \item "[[ ttst -6 = logorc1 ( 5 , 0 ) end test ]]" \item "[[ ttst 5 = logorc1 ( -1 , 5 ) end test ]]" \item "[[ ttst -1 = logorc1 ( 5 , -1 ) end test ]]" \item "[[ ttst -3 = logorc1 ( 10 , 12 ) end test ]]" \end{statements}" ]" \subsection{logorc2} "[ "\begin{statements} \item "[[ etst tx ; logorc2 ( tt , 2 ) end test ]]" \item "[[ etst tx ; logorc2 ( 1 , tt ) end test ]]" \item "[[ etst ty ; logorc2 ( ty , bottom ) end test ]]" \item "[[ ttst -6 = logorc2 ( 0 , 5 ) end test ]]" \item "[[ ttst -1 = logorc2 ( 5 , 0 ) end test ]]" \item "[[ ttst -1 = logorc2 ( -1 , 5 ) end test ]]" \item "[[ ttst 5 = logorc2 ( 5 , -1 ) end test ]]" \item "[[ ttst -5 = logorc2 ( 10 , 12 ) end test ]]" \end{statements}" ]" \subsection{logtest} "[ "\begin{statements} \item "[[ etst tx ; logtest ( tt , 2 ) end test ]]" \item "[[ etst tx ; logtest ( 1 , tt ) end test ]]" \item "[[ etst ty ; logtest ( ty , bottom ) end test ]]" \item "[[ ftst logtest ( 5 , 10 ) end test ]]" \item "[[ ftst logtest ( 5 , 0 ) end test ]]" \item "[[ ttst logtest ( 5 , 1 ) end test ]]" \item "[[ ftst logtest ( 5 , 2 ) end test ]]" \item "[[ ttst logtest ( 5 , 4 ) end test ]]" \item "[[ ftst logtest ( 5 , 8 ) end test ]]" \item "[[ ftst logtest ( 5 , 16 ) end test ]]" \item "[[ ftst logtest ( -11 , 10 ) end test ]]" \item "[[ ftst logtest ( -11 , 0 ) end test ]]" \item "[[ ttst logtest ( -11 , 1 ) end test ]]" \item "[[ ftst logtest ( -11 , 2 ) end test ]]" \item "[[ ttst logtest ( -11 , 4 ) end test ]]" \item "[[ ftst logtest ( -11 , 8 ) end test ]]" \item "[[ ttst logtest ( -11 , 16 ) end test ]]" \end{statements}" ]" \subsection{ash} "[ "\begin{statements} \item "[[ etst tx ; ash ( tt , 2 ) end test ]]" \item "[[ etst tx ; ash ( 1 , tt ) end test ]]" \item "[[ etst ty ; ash ( ty , bottom ) end test ]]" \item "[[ ttst 3 = ash ( 3 , 0 ) end test ]]" \item "[[ ttst 6 = ash ( 3 , 1 ) end test ]]" \item "[[ ttst 12 = ash ( 3 , 2 ) end test ]]" \item "[[ ttst 13 = ash ( 13 , 0 ) end test ]]" \item "[[ ttst 6 = ash ( 13 , -1 ) end test ]]" \item "[[ ttst 3 = ash ( 13 , -2 ) end test ]]" \item "[[ ttst 1 = ash ( 13 , -3 ) end test ]]" \item "[[ ttst 0 = ash ( 13 , -4 ) end test ]]" \item "[[ ttst 0 = ash ( 13 , -5 ) end test ]]" \item "[[ ttst -3 = ash ( -3 , 0 ) end test ]]" \item "[[ ttst -6 = ash ( -3 , 1 ) end test ]]" \item "[[ ttst -12 = ash ( -3 , 2 ) end test ]]" \item "[[ ttst -6 = ash ( -6 , 0 ) end test ]]" \item "[[ ttst -3 = ash ( -6 , -1 ) end test ]]" \item "[[ ttst -2 = ash ( -6 , -2 ) end test ]]" \item "[[ ttst -1 = ash ( -6 , -3 ) end test ]]" \item "[[ ttst -1 = ash ( -6 , -4 ) end test ]]" \end{statements}" ]" \subsection{logbitp} "[ "\begin{statements} \item "[[ etst tx ; logbitp ( tt , 2 ) end test ]]" \item "[[ etst tx ; logbitp ( 1 , tt ) end test ]]" \item "[[ etst ty ; logbitp ( ty , bottom ) end test ]]" \item "[[ ttst logbitp ( 0 , 13 ) end test ]]" \item "[[ ftst logbitp ( 1 , 13 ) end test ]]" \item "[[ ttst logbitp ( 2 , 13 ) end test ]]" \item "[[ ttst logbitp ( 3 , 13 ) end test ]]" \item "[[ ftst logbitp ( 4 , 13 ) end test ]]" \item "[[ ftst logbitp ( 5 , 13 ) end test ]]" \item "[[ ftst logbitp ( 6 , 13 ) end test ]]" \item "[[ ftst logbitp ( 0 , -6 ) end test ]]" \item "[[ ttst logbitp ( 1 , -6 ) end test ]]" \item "[[ ftst logbitp ( 2 , -6 ) end test ]]" \item "[[ ttst logbitp ( 3 , -6 ) end test ]]" \item "[[ ttst logbitp ( 4 , -6 ) end test ]]" \item "[[ ttst logbitp ( 5 , -6 ) end test ]]" \item "[[ ttst logbitp ( 6 , -6 ) end test ]]" \end{statements}" ]" \subsection{logcount} "[ "\begin{statements} \item "[[ etst tx ; logcount ( tt ) end test ]]" \item "[[ etst ty ; logcount ( ty ) end test ]]" \item "[[ ttst 0 = logcount ( 0 ) end test ]]" \item "[[ ttst 1 = logcount ( 1 ) end test ]]" \item "[[ ttst 1 = logcount ( 2 ) end test ]]" \item "[[ ttst 2 = logcount ( 3 ) end test ]]" \item "[[ ttst 1 = logcount ( 4 ) end test ]]" \item "[[ ttst 2 = logcount ( 5 ) end test ]]" \item "[[ ttst 2 = logcount ( 6 ) end test ]]" \item "[[ ttst 3 = logcount ( 7 ) end test ]]" \item "[[ ttst 1 = logcount ( 8 ) end test ]]" \item "[[ ttst 2 = logcount ( 9 ) end test ]]" \item "[[ ttst 0 = logcount ( -1 ) end test ]]" \item "[[ ttst 1 = logcount ( -2 ) end test ]]" \item "[[ ttst 1 = logcount ( -3 ) end test ]]" \item "[[ ttst 2 = logcount ( -4 ) end test ]]" \item "[[ ttst 1 = logcount ( -5 ) end test ]]" \item "[[ ttst 2 = logcount ( -6 ) end test ]]" \item "[[ ttst 2 = logcount ( -7 ) end test ]]" \item "[[ ttst 3 = logcount ( -8 ) end test ]]" \item "[[ ttst 1 = logcount ( -9 ) end test ]]" \end{statements}" ]" \subsection{integer-length} "[ "\begin{statements} \item "[[ etst tx ; integer-length ( tt ) end test ]]" \item "[[ etst ty ; integer-length ( ty ) end test ]]" \item "[[ ttst 0 = integer-length ( 0 ) end test ]]" \item "[[ ttst 1 = integer-length ( 1 ) end test ]]" \item "[[ ttst 2 = integer-length ( 2 ) end test ]]" \item "[[ ttst 2 = integer-length ( 3 ) end test ]]" \item "[[ ttst 3 = integer-length ( 4 ) end test ]]" \item "[[ ttst 3 = integer-length ( 5 ) end test ]]" \item "[[ ttst 3 = integer-length ( 6 ) end test ]]" \item "[[ ttst 3 = integer-length ( 7 ) end test ]]" \item "[[ ttst 4 = integer-length ( 8 ) end test ]]" \item "[[ ttst 4 = integer-length ( 9 ) end test ]]" \item "[[ ttst 0 = integer-length ( -1 ) end test ]]" \item "[[ ttst 1 = integer-length ( -2 ) end test ]]" \item "[[ ttst 2 = integer-length ( -3 ) end test ]]" \item "[[ ttst 2 = integer-length ( -4 ) end test ]]" \item "[[ ttst 3 = integer-length ( -5 ) end test ]]" \item "[[ ttst 3 = integer-length ( -6 ) end test ]]" \item "[[ ttst 3 = integer-length ( -7 ) end test ]]" \item "[[ ttst 3 = integer-length ( -8 ) end test ]]" \item "[[ ttst 4 = integer-length ( -9 ) end test ]]" \end{statements}" ]" \section{Numerals} "[ "\begin{statements} \item "[[ ttst quote 50 end quote t= quote %% %5 %0 end quote end test ]]" \item "[[ ttst quote 51 end quote t= quote %% %5 %1 end quote end test ]]" \item "[[ ttst quote 52 end quote t= quote %% %5 %2 end quote end test ]]" \item "[[ ttst quote 53 end quote t= quote %% %5 %3 end quote end test ]]" \item "[[ ttst quote 54 end quote t= quote %% %5 %4 end quote end test ]]" \item "[[ ttst quote 55 end quote t= quote %% %5 %5 end quote end test ]]" \item "[[ ttst quote 56 end quote t= quote %% %5 %6 end quote end test ]]" \item "[[ ttst quote 57 end quote t= quote %% %5 %7 end quote end test ]]" \item "[[ ttst quote 58 end quote t= quote %% %5 %8 end quote end test ]]" \item "[[ ttst quote 59 end quote t= quote %% %5 %9 end quote end test ]]" \item "[[ ttst quote 00 end quote t= quote %% %0 %0 end quote end test ]]" \item "[[ ttst quote 20 end quote t= quote %% %2 %0 end quote end test ]]" \item "[[ ttst quote 30 end quote t= quote %% %3 %0 end quote end test ]]" \item "[[ ttst quote 40 end quote t= quote %% %4 %0 end quote end test ]]" \item "[[ ttst quote 50 end quote t= quote %% %5 %0 end quote end test ]]" \item "[[ ttst quote 60 end quote t= quote %% %6 %0 end quote end test ]]" \item "[[ ttst quote 70 end quote t= quote %% %7 %0 end quote end test ]]" \item "[[ ttst quote 80 end quote t= quote %% %8 %0 end quote end test ]]" \item "[[ ttst quote 90 end quote t= quote %% %9 %0 end quote end test ]]" \item "[[ ttst quote 12345678901 end quote t= quote %% %1 %2 %3 %4 %5 %6 %7 %8 %9 %0 %1 end quote end test ]]" \item "[[ ttst quote 1x end quote t= quote exception end quote end test ]]" \item "[[ ttst 123 + 45 = 168 end test ]]" \item "[[ ttst 123 - 45 = 78 end test ]]" \item "[[ ttst 123 * 45 = 5535 end test ]]" \item "[[ ttst -123 + -45 = -168 end test ]]" \item "[[ ttst -123 - -45 = -78 end test ]]" \item "[[ ttst -123 * -45 = 5535 end test ]]" \end{statements}" ]" \section{Division} \subsection{floor} "[ "\begin{statements} \item "[[ etst floor ( -9 , 1 ) ; -9 :: +0 end test ]]" \item "[[ etst floor ( -8 , 1 ) ; -8 :: +0 end test ]]" \item "[[ etst floor ( -7 , 1 ) ; -7 :: +0 end test ]]" \item "[[ etst floor ( -6 , 1 ) ; -6 :: +0 end test ]]" \item "[[ etst floor ( -5 , 1 ) ; -5 :: +0 end test ]]" \item "[[ etst floor ( -4 , 1 ) ; -4 :: +0 end test ]]" \item "[[ etst floor ( -3 , 1 ) ; -3 :: +0 end test ]]" \item "[[ etst floor ( -2 , 1 ) ; -2 :: +0 end test ]]" \item "[[ etst floor ( -1 , 1 ) ; -1 :: +0 end test ]]" \item "[[ etst floor ( +0 , 1 ) ; +0 :: +0 end test ]]" \item "[[ etst floor ( +1 , 1 ) ; +1 :: +0 end test ]]" \item "[[ etst floor ( +2 , 1 ) ; +2 :: +0 end test ]]" \item "[[ etst floor ( +3 , 1 ) ; +3 :: +0 end test ]]" \item "[[ etst floor ( +4 , 1 ) ; +4 :: +0 end test ]]" \item "[[ etst floor ( +5 , 1 ) ; +5 :: +0 end test ]]" \item "[[ etst floor ( +6 , 1 ) ; +6 :: +0 end test ]]" \item "[[ etst floor ( +7 , 1 ) ; +7 :: +0 end test ]]" \item "[[ etst floor ( +8 , 1 ) ; +8 :: +0 end test ]]" \item "[[ etst floor ( +9 , 1 ) ; +9 :: +0 end test ]]" \item "[[ etst floor ( -9 , 2 ) ; -5 :: +1 end test ]]" \item "[[ etst floor ( -8 , 2 ) ; -4 :: +0 end test ]]" \item "[[ etst floor ( -7 , 2 ) ; -4 :: +1 end test ]]" \item "[[ etst floor ( -6 , 2 ) ; -3 :: +0 end test ]]" \item "[[ etst floor ( -5 , 2 ) ; -3 :: +1 end test ]]" \item "[[ etst floor ( -4 , 2 ) ; -2 :: +0 end test ]]" \item "[[ etst floor ( -3 , 2 ) ; -2 :: +1 end test ]]" \item "[[ etst floor ( -2 , 2 ) ; -1 :: +0 end test ]]" \item "[[ etst floor ( -1 , 2 ) ; -1 :: +1 end test ]]" \item "[[ etst floor ( +0 , 2 ) ; +0 :: +0 end test ]]" \item "[[ etst floor ( +1 , 2 ) ; +0 :: +1 end test ]]" \item "[[ etst floor ( +2 , 2 ) ; +1 :: +0 end test ]]" \item "[[ etst floor ( +3 , 2 ) ; +1 :: +1 end test ]]" \item "[[ etst floor ( +4 , 2 ) ; +2 :: +0 end test ]]" \item "[[ etst floor ( +5 , 2 ) ; +2 :: +1 end test ]]" \item "[[ etst floor ( +6 , 2 ) ; +3 :: +0 end test ]]" \item "[[ etst floor ( +7 , 2 ) ; +3 :: +1 end test ]]" \item "[[ etst floor ( +8 , 2 ) ; +4 :: +0 end test ]]" \item "[[ etst floor ( +9 , 2 ) ; +4 :: +1 end test ]]" \item "[[ etst floor ( -9 , 3 ) ; -3 :: +0 end test ]]" \item "[[ etst floor ( -8 , 3 ) ; -3 :: +1 end test ]]" \item "[[ etst floor ( -7 , 3 ) ; -3 :: +2 end test ]]" \item "[[ etst floor ( -6 , 3 ) ; -2 :: +0 end test ]]" \item "[[ etst floor ( -5 , 3 ) ; -2 :: +1 end test ]]" \item "[[ etst floor ( -4 , 3 ) ; -2 :: +2 end test ]]" \item "[[ etst floor ( -3 , 3 ) ; -1 :: +0 end test ]]" \item "[[ etst floor ( -2 , 3 ) ; -1 :: +1 end test ]]" \item "[[ etst floor ( -1 , 3 ) ; -1 :: +2 end test ]]" \item "[[ etst floor ( +0 , 3 ) ; +0 :: +0 end test ]]" \item "[[ etst floor ( +1 , 3 ) ; +0 :: +1 end test ]]" \item "[[ etst floor ( +2 , 3 ) ; +0 :: +2 end test ]]" \item "[[ etst floor ( +3 , 3 ) ; +1 :: +0 end test ]]" \item "[[ etst floor ( +4 , 3 ) ; +1 :: +1 end test ]]" \item "[[ etst floor ( +5 , 3 ) ; +1 :: +2 end test ]]" \item "[[ etst floor ( +6 , 3 ) ; +2 :: +0 end test ]]" \item "[[ etst floor ( +7 , 3 ) ; +2 :: +1 end test ]]" \item "[[ etst floor ( +8 , 3 ) ; +2 :: +2 end test ]]" \item "[[ etst floor ( +9 , 3 ) ; +3 :: +0 end test ]]" \item "[[ etst floor ( -9 , 4 ) ; -3 :: +3 end test ]]" \item "[[ etst floor ( -8 , 4 ) ; -2 :: +0 end test ]]" \item "[[ etst floor ( -7 , 4 ) ; -2 :: +1 end test ]]" \item "[[ etst floor ( -6 , 4 ) ; -2 :: +2 end test ]]" \item "[[ etst floor ( -5 , 4 ) ; -2 :: +3 end test ]]" \item "[[ etst floor ( -4 , 4 ) ; -1 :: +0 end test ]]" \item "[[ etst floor ( -3 , 4 ) ; -1 :: +1 end test ]]" \item "[[ etst floor ( -2 , 4 ) ; -1 :: +2 end test ]]" \item "[[ etst floor ( -1 , 4 ) ; -1 :: +3 end test ]]" \item "[[ etst floor ( +0 , 4 ) ; +0 :: +0 end test ]]" \item "[[ etst floor ( +1 , 4 ) ; +0 :: +1 end test ]]" \item "[[ etst floor ( +2 , 4 ) ; +0 :: +2 end test ]]" \item "[[ etst floor ( +3 , 4 ) ; +0 :: +3 end test ]]" \item "[[ etst floor ( +4 , 4 ) ; +1 :: +0 end test ]]" \item "[[ etst floor ( +5 , 4 ) ; +1 :: +1 end test ]]" \item "[[ etst floor ( +6 , 4 ) ; +1 :: +2 end test ]]" \item "[[ etst floor ( +7 , 4 ) ; +1 :: +3 end test ]]" \item "[[ etst floor ( +8 , 4 ) ; +2 :: +0 end test ]]" \item "[[ etst floor ( +9 , 4 ) ; +2 :: +1 end test ]]" \item "[[ etst floor ( -9 , 5 ) ; -2 :: +1 end test ]]" \item "[[ etst floor ( -8 , 5 ) ; -2 :: +2 end test ]]" \item "[[ etst floor ( -7 , 5 ) ; -2 :: +3 end test ]]" \item "[[ etst floor ( -6 , 5 ) ; -2 :: +4 end test ]]" \item "[[ etst floor ( -5 , 5 ) ; -1 :: +0 end test ]]" \item "[[ etst floor ( -4 , 5 ) ; -1 :: +1 end test ]]" \item "[[ etst floor ( -3 , 5 ) ; -1 :: +2 end test ]]" \item "[[ etst floor ( -2 , 5 ) ; -1 :: +3 end test ]]" \item "[[ etst floor ( -1 , 5 ) ; -1 :: +4 end test ]]" \item "[[ etst floor ( +0 , 5 ) ; +0 :: +0 end test ]]" \item "[[ etst floor ( +1 , 5 ) ; +0 :: +1 end test ]]" \item "[[ etst floor ( +2 , 5 ) ; +0 :: +2 end test ]]" \item "[[ etst floor ( +3 , 5 ) ; +0 :: +3 end test ]]" \item "[[ etst floor ( +4 , 5 ) ; +0 :: +4 end test ]]" \item "[[ etst floor ( +5 , 5 ) ; +1 :: +0 end test ]]" \item "[[ etst floor ( +6 , 5 ) ; +1 :: +1 end test ]]" \item "[[ etst floor ( +7 , 5 ) ; +1 :: +2 end test ]]" \item "[[ etst floor ( +8 , 5 ) ; +1 :: +3 end test ]]" \item "[[ etst floor ( +9 , 5 ) ; +1 :: +4 end test ]]" \item "[[ etst floor ( -5 , 0 ) ; exception end test ]]" \item "[[ etst floor ( -1 , 0 ) ; exception end test ]]" \item "[[ etst floor ( +0 , 0 ) ; exception end test ]]" \item "[[ etst floor ( +1 , 0 ) ; exception end test ]]" \item "[[ etst floor ( +5 , 0 ) ; exception end test ]]" \item "[[ etst floor ( -5 , -1 ) ; exception end test ]]" \item "[[ etst floor ( -1 , -1 ) ; exception end test ]]" \item "[[ etst floor ( +0 , -1 ) ; exception end test ]]" \item "[[ etst floor ( +1 , -1 ) ; exception end test ]]" \item "[[ etst floor ( +5 , -1 ) ; exception end test ]]" \end{statements}" ]" \subsection{div} "[ "\begin{statements} \item "[[ etst -9 div 1 ; -9 end test ]]" \item "[[ etst -8 div 1 ; -8 end test ]]" \item "[[ etst -7 div 1 ; -7 end test ]]" \item "[[ etst -6 div 1 ; -6 end test ]]" \item "[[ etst -5 div 1 ; -5 end test ]]" \item "[[ etst -4 div 1 ; -4 end test ]]" \item "[[ etst -3 div 1 ; -3 end test ]]" \item "[[ etst -2 div 1 ; -2 end test ]]" \item "[[ etst -1 div 1 ; -1 end test ]]" \item "[[ etst +0 div 1 ; +0 end test ]]" \item "[[ etst +1 div 1 ; +1 end test ]]" \item "[[ etst +2 div 1 ; +2 end test ]]" \item "[[ etst +3 div 1 ; +3 end test ]]" \item "[[ etst +4 div 1 ; +4 end test ]]" \item "[[ etst +5 div 1 ; +5 end test ]]" \item "[[ etst +6 div 1 ; +6 end test ]]" \item "[[ etst +7 div 1 ; +7 end test ]]" \item "[[ etst +8 div 1 ; +8 end test ]]" \item "[[ etst +9 div 1 ; +9 end test ]]" \item "[[ etst -9 div 2 ; -5 end test ]]" \item "[[ etst -8 div 2 ; -4 end test ]]" \item "[[ etst -7 div 2 ; -4 end test ]]" \item "[[ etst -6 div 2 ; -3 end test ]]" \item "[[ etst -5 div 2 ; -3 end test ]]" \item "[[ etst -4 div 2 ; -2 end test ]]" \item "[[ etst -3 div 2 ; -2 end test ]]" \item "[[ etst -2 div 2 ; -1 end test ]]" \item "[[ etst -1 div 2 ; -1 end test ]]" \item "[[ etst +0 div 2 ; +0 end test ]]" \item "[[ etst +1 div 2 ; +0 end test ]]" \item "[[ etst +2 div 2 ; +1 end test ]]" \item "[[ etst +3 div 2 ; +1 end test ]]" \item "[[ etst +4 div 2 ; +2 end test ]]" \item "[[ etst +5 div 2 ; +2 end test ]]" \item "[[ etst +6 div 2 ; +3 end test ]]" \item "[[ etst +7 div 2 ; +3 end test ]]" \item "[[ etst +8 div 2 ; +4 end test ]]" \item "[[ etst +9 div 2 ; +4 end test ]]" \item "[[ etst -9 div 3 ; -3 end test ]]" \item "[[ etst -8 div 3 ; -3 end test ]]" \item "[[ etst -7 div 3 ; -3 end test ]]" \item "[[ etst -6 div 3 ; -2 end test ]]" \item "[[ etst -5 div 3 ; -2 end test ]]" \item "[[ etst -4 div 3 ; -2 end test ]]" \item "[[ etst -3 div 3 ; -1 end test ]]" \item "[[ etst -2 div 3 ; -1 end test ]]" \item "[[ etst -1 div 3 ; -1 end test ]]" \item "[[ etst +0 div 3 ; +0 end test ]]" \item "[[ etst +1 div 3 ; +0 end test ]]" \item "[[ etst +2 div 3 ; +0 end test ]]" \item "[[ etst +3 div 3 ; +1 end test ]]" \item "[[ etst +4 div 3 ; +1 end test ]]" \item "[[ etst +5 div 3 ; +1 end test ]]" \item "[[ etst +6 div 3 ; +2 end test ]]" \item "[[ etst +7 div 3 ; +2 end test ]]" \item "[[ etst +8 div 3 ; +2 end test ]]" \item "[[ etst +9 div 3 ; +3 end test ]]" \item "[[ etst -9 div 4 ; -3 end test ]]" \item "[[ etst -8 div 4 ; -2 end test ]]" \item "[[ etst -7 div 4 ; -2 end test ]]" \item "[[ etst -6 div 4 ; -2 end test ]]" \item "[[ etst -5 div 4 ; -2 end test ]]" \item "[[ etst -4 div 4 ; -1 end test ]]" \item "[[ etst -3 div 4 ; -1 end test ]]" \item "[[ etst -2 div 4 ; -1 end test ]]" \item "[[ etst -1 div 4 ; -1 end test ]]" \item "[[ etst +0 div 4 ; +0 end test ]]" \item "[[ etst +1 div 4 ; +0 end test ]]" \item "[[ etst +2 div 4 ; +0 end test ]]" \item "[[ etst +3 div 4 ; +0 end test ]]" \item "[[ etst +4 div 4 ; +1 end test ]]" \item "[[ etst +5 div 4 ; +1 end test ]]" \item "[[ etst +6 div 4 ; +1 end test ]]" \item "[[ etst +7 div 4 ; +1 end test ]]" \item "[[ etst +8 div 4 ; +2 end test ]]" \item "[[ etst +9 div 4 ; +2 end test ]]" \item "[[ etst -9 div 5 ; -2 end test ]]" \item "[[ etst -8 div 5 ; -2 end test ]]" \item "[[ etst -7 div 5 ; -2 end test ]]" \item "[[ etst -6 div 5 ; -2 end test ]]" \item "[[ etst -5 div 5 ; -1 end test ]]" \item "[[ etst -4 div 5 ; -1 end test ]]" \item "[[ etst -3 div 5 ; -1 end test ]]" \item "[[ etst -2 div 5 ; -1 end test ]]" \item "[[ etst -1 div 5 ; -1 end test ]]" \item "[[ etst +0 div 5 ; +0 end test ]]" \item "[[ etst +1 div 5 ; +0 end test ]]" \item "[[ etst +2 div 5 ; +0 end test ]]" \item "[[ etst +3 div 5 ; +0 end test ]]" \item "[[ etst +4 div 5 ; +0 end test ]]" \item "[[ etst +5 div 5 ; +1 end test ]]" \item "[[ etst +6 div 5 ; +1 end test ]]" \item "[[ etst +7 div 5 ; +1 end test ]]" \item "[[ etst +8 div 5 ; +1 end test ]]" \item "[[ etst +9 div 5 ; +1 end test ]]" \item "[[ etst -5 div 0 ; exception end test ]]" \item "[[ etst -1 div 0 ; exception end test ]]" \item "[[ etst +0 div 0 ; exception end test ]]" \item "[[ etst +1 div 0 ; exception end test ]]" \item "[[ etst +5 div 0 ; exception end test ]]" \item "[[ etst -5 div -1 ; exception end test ]]" \item "[[ etst -1 div -1 ; exception end test ]]" \item "[[ etst +0 div -1 ; exception end test ]]" \item "[[ etst +1 div -1 ; exception end test ]]" \item "[[ etst +5 div -1 ; exception end test ]]" \end{statements}" ]" \subsection{mod} "[ "\begin{statements} \item "[[ etst -9 mod 1 ; +0 end test ]]" \item "[[ etst -8 mod 1 ; +0 end test ]]" \item "[[ etst -7 mod 1 ; +0 end test ]]" \item "[[ etst -6 mod 1 ; +0 end test ]]" \item "[[ etst -5 mod 1 ; +0 end test ]]" \item "[[ etst -4 mod 1 ; +0 end test ]]" \item "[[ etst -3 mod 1 ; +0 end test ]]" \item "[[ etst -2 mod 1 ; +0 end test ]]" \item "[[ etst -1 mod 1 ; +0 end test ]]" \item "[[ etst +0 mod 1 ; +0 end test ]]" \item "[[ etst +1 mod 1 ; +0 end test ]]" \item "[[ etst +2 mod 1 ; +0 end test ]]" \item "[[ etst +3 mod 1 ; +0 end test ]]" \item "[[ etst +4 mod 1 ; +0 end test ]]" \item "[[ etst +5 mod 1 ; +0 end test ]]" \item "[[ etst +6 mod 1 ; +0 end test ]]" \item "[[ etst +7 mod 1 ; +0 end test ]]" \item "[[ etst +8 mod 1 ; +0 end test ]]" \item "[[ etst +9 mod 1 ; +0 end test ]]" \item "[[ etst -9 mod 2 ; +1 end test ]]" \item "[[ etst -8 mod 2 ; +0 end test ]]" \item "[[ etst -7 mod 2 ; +1 end test ]]" \item "[[ etst -6 mod 2 ; +0 end test ]]" \item "[[ etst -5 mod 2 ; +1 end test ]]" \item "[[ etst -4 mod 2 ; +0 end test ]]" \item "[[ etst -3 mod 2 ; +1 end test ]]" \item "[[ etst -2 mod 2 ; +0 end test ]]" \item "[[ etst -1 mod 2 ; +1 end test ]]" \item "[[ etst +0 mod 2 ; +0 end test ]]" \item "[[ etst +1 mod 2 ; +1 end test ]]" \item "[[ etst +2 mod 2 ; +0 end test ]]" \item "[[ etst +3 mod 2 ; +1 end test ]]" \item "[[ etst +4 mod 2 ; +0 end test ]]" \item "[[ etst +5 mod 2 ; +1 end test ]]" \item "[[ etst +6 mod 2 ; +0 end test ]]" \item "[[ etst +7 mod 2 ; +1 end test ]]" \item "[[ etst +8 mod 2 ; +0 end test ]]" \item "[[ etst +9 mod 2 ; +1 end test ]]" \item "[[ etst -9 mod 3 ; +0 end test ]]" \item "[[ etst -8 mod 3 ; +1 end test ]]" \item "[[ etst -7 mod 3 ; +2 end test ]]" \item "[[ etst -6 mod 3 ; +0 end test ]]" \item "[[ etst -5 mod 3 ; +1 end test ]]" \item "[[ etst -4 mod 3 ; +2 end test ]]" \item "[[ etst -3 mod 3 ; +0 end test ]]" \item "[[ etst -2 mod 3 ; +1 end test ]]" \item "[[ etst -1 mod 3 ; +2 end test ]]" \item "[[ etst +0 mod 3 ; +0 end test ]]" \item "[[ etst +1 mod 3 ; +1 end test ]]" \item "[[ etst +2 mod 3 ; +2 end test ]]" \item "[[ etst +3 mod 3 ; +0 end test ]]" \item "[[ etst +4 mod 3 ; +1 end test ]]" \item "[[ etst +5 mod 3 ; +2 end test ]]" \item "[[ etst +6 mod 3 ; +0 end test ]]" \item "[[ etst +7 mod 3 ; +1 end test ]]" \item "[[ etst +8 mod 3 ; +2 end test ]]" \item "[[ etst +9 mod 3 ; +0 end test ]]" \item "[[ etst -9 mod 4 ; +3 end test ]]" \item "[[ etst -8 mod 4 ; +0 end test ]]" \item "[[ etst -7 mod 4 ; +1 end test ]]" \item "[[ etst -6 mod 4 ; +2 end test ]]" \item "[[ etst -5 mod 4 ; +3 end test ]]" \item "[[ etst -4 mod 4 ; +0 end test ]]" \item "[[ etst -3 mod 4 ; +1 end test ]]" \item "[[ etst -2 mod 4 ; +2 end test ]]" \item "[[ etst -1 mod 4 ; +3 end test ]]" \item "[[ etst +0 mod 4 ; +0 end test ]]" \item "[[ etst +1 mod 4 ; +1 end test ]]" \item "[[ etst +2 mod 4 ; +2 end test ]]" \item "[[ etst +3 mod 4 ; +3 end test ]]" \item "[[ etst +4 mod 4 ; +0 end test ]]" \item "[[ etst +5 mod 4 ; +1 end test ]]" \item "[[ etst +6 mod 4 ; +2 end test ]]" \item "[[ etst +7 mod 4 ; +3 end test ]]" \item "[[ etst +8 mod 4 ; +0 end test ]]" \item "[[ etst +9 mod 4 ; +1 end test ]]" \item "[[ etst -9 mod 5 ; +1 end test ]]" \item "[[ etst -8 mod 5 ; +2 end test ]]" \item "[[ etst -7 mod 5 ; +3 end test ]]" \item "[[ etst -6 mod 5 ; +4 end test ]]" \item "[[ etst -5 mod 5 ; +0 end test ]]" \item "[[ etst -4 mod 5 ; +1 end test ]]" \item "[[ etst -3 mod 5 ; +2 end test ]]" \item "[[ etst -2 mod 5 ; +3 end test ]]" \item "[[ etst -1 mod 5 ; +4 end test ]]" \item "[[ etst +0 mod 5 ; +0 end test ]]" \item "[[ etst +1 mod 5 ; +1 end test ]]" \item "[[ etst +2 mod 5 ; +2 end test ]]" \item "[[ etst +3 mod 5 ; +3 end test ]]" \item "[[ etst +4 mod 5 ; +4 end test ]]" \item "[[ etst +5 mod 5 ; +0 end test ]]" \item "[[ etst +6 mod 5 ; +1 end test ]]" \item "[[ etst +7 mod 5 ; +2 end test ]]" \item "[[ etst +8 mod 5 ; +3 end test ]]" \item "[[ etst +9 mod 5 ; +4 end test ]]" \item "[[ etst -5 mod 0 ; exception end test ]]" \item "[[ etst -1 mod 0 ; exception end test ]]" \item "[[ etst +0 mod 0 ; exception end test ]]" \item "[[ etst +1 mod 0 ; exception end test ]]" \item "[[ etst +5 mod 0 ; exception end test ]]" \item "[[ etst -5 mod -1 ; exception end test ]]" \item "[[ etst -1 mod -1 ; exception end test ]]" \item "[[ etst +0 mod -1 ; exception end test ]]" \item "[[ etst +1 mod -1 ; exception end test ]]" \item "[[ etst +5 mod -1 ; exception end test ]]" \end{statements}" ]" \subsection{ceiling} "[ "\begin{statements} \item "[[ etst ceiling ( +9 , 1 ) ; +9 :: -0 end test ]]" \item "[[ etst ceiling ( +8 , 1 ) ; +8 :: -0 end test ]]" \item "[[ etst ceiling ( +7 , 1 ) ; +7 :: -0 end test ]]" \item "[[ etst ceiling ( +6 , 1 ) ; +6 :: -0 end test ]]" \item "[[ etst ceiling ( +5 , 1 ) ; +5 :: -0 end test ]]" \item "[[ etst ceiling ( +4 , 1 ) ; +4 :: -0 end test ]]" \item "[[ etst ceiling ( +3 , 1 ) ; +3 :: -0 end test ]]" \item "[[ etst ceiling ( +2 , 1 ) ; +2 :: -0 end test ]]" \item "[[ etst ceiling ( +1 , 1 ) ; +1 :: -0 end test ]]" \item "[[ etst ceiling ( -0 , 1 ) ; -0 :: -0 end test ]]" \item "[[ etst ceiling ( -1 , 1 ) ; -1 :: -0 end test ]]" \item "[[ etst ceiling ( -2 , 1 ) ; -2 :: -0 end test ]]" \item "[[ etst ceiling ( -3 , 1 ) ; -3 :: -0 end test ]]" \item "[[ etst ceiling ( -4 , 1 ) ; -4 :: -0 end test ]]" \item "[[ etst ceiling ( -5 , 1 ) ; -5 :: -0 end test ]]" \item "[[ etst ceiling ( -6 , 1 ) ; -6 :: -0 end test ]]" \item "[[ etst ceiling ( -7 , 1 ) ; -7 :: -0 end test ]]" \item "[[ etst ceiling ( -8 , 1 ) ; -8 :: -0 end test ]]" \item "[[ etst ceiling ( -9 , 1 ) ; -9 :: -0 end test ]]" \item "[[ etst ceiling ( +9 , 2 ) ; +5 :: -1 end test ]]" \item "[[ etst ceiling ( +8 , 2 ) ; +4 :: -0 end test ]]" \item "[[ etst ceiling ( +7 , 2 ) ; +4 :: -1 end test ]]" \item "[[ etst ceiling ( +6 , 2 ) ; +3 :: -0 end test ]]" \item "[[ etst ceiling ( +5 , 2 ) ; +3 :: -1 end test ]]" \item "[[ etst ceiling ( +4 , 2 ) ; +2 :: -0 end test ]]" \item "[[ etst ceiling ( +3 , 2 ) ; +2 :: -1 end test ]]" \item "[[ etst ceiling ( +2 , 2 ) ; +1 :: -0 end test ]]" \item "[[ etst ceiling ( +1 , 2 ) ; +1 :: -1 end test ]]" \item "[[ etst ceiling ( -0 , 2 ) ; -0 :: -0 end test ]]" \item "[[ etst ceiling ( -1 , 2 ) ; -0 :: -1 end test ]]" \item "[[ etst ceiling ( -2 , 2 ) ; -1 :: -0 end test ]]" \item "[[ etst ceiling ( -3 , 2 ) ; -1 :: -1 end test ]]" \item "[[ etst ceiling ( -4 , 2 ) ; -2 :: -0 end test ]]" \item "[[ etst ceiling ( -5 , 2 ) ; -2 :: -1 end test ]]" \item "[[ etst ceiling ( -6 , 2 ) ; -3 :: -0 end test ]]" \item "[[ etst ceiling ( -7 , 2 ) ; -3 :: -1 end test ]]" \item "[[ etst ceiling ( -8 , 2 ) ; -4 :: -0 end test ]]" \item "[[ etst ceiling ( -9 , 2 ) ; -4 :: -1 end test ]]" \item "[[ etst ceiling ( +9 , 3 ) ; +3 :: -0 end test ]]" \item "[[ etst ceiling ( +8 , 3 ) ; +3 :: -1 end test ]]" \item "[[ etst ceiling ( +7 , 3 ) ; +3 :: -2 end test ]]" \item "[[ etst ceiling ( +6 , 3 ) ; +2 :: -0 end test ]]" \item "[[ etst ceiling ( +5 , 3 ) ; +2 :: -1 end test ]]" \item "[[ etst ceiling ( +4 , 3 ) ; +2 :: -2 end test ]]" \item "[[ etst ceiling ( +3 , 3 ) ; +1 :: -0 end test ]]" \item "[[ etst ceiling ( +2 , 3 ) ; +1 :: -1 end test ]]" \item "[[ etst ceiling ( +1 , 3 ) ; +1 :: -2 end test ]]" \item "[[ etst ceiling ( -0 , 3 ) ; -0 :: -0 end test ]]" \item "[[ etst ceiling ( -1 , 3 ) ; -0 :: -1 end test ]]" \item "[[ etst ceiling ( -2 , 3 ) ; -0 :: -2 end test ]]" \item "[[ etst ceiling ( -3 , 3 ) ; -1 :: -0 end test ]]" \item "[[ etst ceiling ( -4 , 3 ) ; -1 :: -1 end test ]]" \item "[[ etst ceiling ( -5 , 3 ) ; -1 :: -2 end test ]]" \item "[[ etst ceiling ( -6 , 3 ) ; -2 :: -0 end test ]]" \item "[[ etst ceiling ( -7 , 3 ) ; -2 :: -1 end test ]]" \item "[[ etst ceiling ( -8 , 3 ) ; -2 :: -2 end test ]]" \item "[[ etst ceiling ( -9 , 3 ) ; -3 :: -0 end test ]]" \item "[[ etst ceiling ( +9 , 4 ) ; +3 :: -3 end test ]]" \item "[[ etst ceiling ( +8 , 4 ) ; +2 :: -0 end test ]]" \item "[[ etst ceiling ( +7 , 4 ) ; +2 :: -1 end test ]]" \item "[[ etst ceiling ( +6 , 4 ) ; +2 :: -2 end test ]]" \item "[[ etst ceiling ( +5 , 4 ) ; +2 :: -3 end test ]]" \item "[[ etst ceiling ( +4 , 4 ) ; +1 :: -0 end test ]]" \item "[[ etst ceiling ( +3 , 4 ) ; +1 :: -1 end test ]]" \item "[[ etst ceiling ( +2 , 4 ) ; +1 :: -2 end test ]]" \item "[[ etst ceiling ( +1 , 4 ) ; +1 :: -3 end test ]]" \item "[[ etst ceiling ( -0 , 4 ) ; -0 :: -0 end test ]]" \item "[[ etst ceiling ( -1 , 4 ) ; -0 :: -1 end test ]]" \item "[[ etst ceiling ( -2 , 4 ) ; -0 :: -2 end test ]]" \item "[[ etst ceiling ( -3 , 4 ) ; -0 :: -3 end test ]]" \item "[[ etst ceiling ( -4 , 4 ) ; -1 :: -0 end test ]]" \item "[[ etst ceiling ( -5 , 4 ) ; -1 :: -1 end test ]]" \item "[[ etst ceiling ( -6 , 4 ) ; -1 :: -2 end test ]]" \item "[[ etst ceiling ( -7 , 4 ) ; -1 :: -3 end test ]]" \item "[[ etst ceiling ( -8 , 4 ) ; -2 :: -0 end test ]]" \item "[[ etst ceiling ( -9 , 4 ) ; -2 :: -1 end test ]]" \item "[[ etst ceiling ( +9 , 5 ) ; +2 :: -1 end test ]]" \item "[[ etst ceiling ( +8 , 5 ) ; +2 :: -2 end test ]]" \item "[[ etst ceiling ( +7 , 5 ) ; +2 :: -3 end test ]]" \item "[[ etst ceiling ( +6 , 5 ) ; +2 :: -4 end test ]]" \item "[[ etst ceiling ( +5 , 5 ) ; +1 :: -0 end test ]]" \item "[[ etst ceiling ( +4 , 5 ) ; +1 :: -1 end test ]]" \item "[[ etst ceiling ( +3 , 5 ) ; +1 :: -2 end test ]]" \item "[[ etst ceiling ( +2 , 5 ) ; +1 :: -3 end test ]]" \item "[[ etst ceiling ( +1 , 5 ) ; +1 :: -4 end test ]]" \item "[[ etst ceiling ( -0 , 5 ) ; -0 :: -0 end test ]]" \item "[[ etst ceiling ( -1 , 5 ) ; -0 :: -1 end test ]]" \item "[[ etst ceiling ( -2 , 5 ) ; -0 :: -2 end test ]]" \item "[[ etst ceiling ( -3 , 5 ) ; -0 :: -3 end test ]]" \item "[[ etst ceiling ( -4 , 5 ) ; -0 :: -4 end test ]]" \item "[[ etst ceiling ( -5 , 5 ) ; -1 :: -0 end test ]]" \item "[[ etst ceiling ( -6 , 5 ) ; -1 :: -1 end test ]]" \item "[[ etst ceiling ( -7 , 5 ) ; -1 :: -2 end test ]]" \item "[[ etst ceiling ( -8 , 5 ) ; -1 :: -3 end test ]]" \item "[[ etst ceiling ( -9 , 5 ) ; -1 :: -4 end test ]]" \item "[[ etst ceiling ( +5 , 0 ) ; exception end test ]]" \item "[[ etst ceiling ( +1 , 0 ) ; exception end test ]]" \item "[[ etst ceiling ( -0 , 0 ) ; exception end test ]]" \item "[[ etst ceiling ( -1 , 0 ) ; exception end test ]]" \item "[[ etst ceiling ( -5 , 0 ) ; exception end test ]]" \item "[[ etst ceiling ( +5 , -1 ) ; exception end test ]]" \item "[[ etst ceiling ( +1 , -1 ) ; exception end test ]]" \item "[[ etst ceiling ( -0 , -1 ) ; exception end test ]]" \item "[[ etst ceiling ( -1 , -1 ) ; exception end test ]]" \item "[[ etst ceiling ( -5 , -1 ) ; exception end test ]]" \end{statements}" ]" \subsection{truncate} "[ "\begin{statements} \item "[[ etst truncate ( +0 , 1 ) ; +0 :: +0 end test ]]" \item "[[ etst truncate ( +1 , 1 ) ; +1 :: +0 end test ]]" \item "[[ etst truncate ( +2 , 1 ) ; +2 :: +0 end test ]]" \item "[[ etst truncate ( +3 , 1 ) ; +3 :: +0 end test ]]" \item "[[ etst truncate ( +4 , 1 ) ; +4 :: +0 end test ]]" \item "[[ etst truncate ( +5 , 1 ) ; +5 :: +0 end test ]]" \item "[[ etst truncate ( +6 , 1 ) ; +6 :: +0 end test ]]" \item "[[ etst truncate ( +7 , 1 ) ; +7 :: +0 end test ]]" \item "[[ etst truncate ( +8 , 1 ) ; +8 :: +0 end test ]]" \item "[[ etst truncate ( +9 , 1 ) ; +9 :: +0 end test ]]" \item "[[ etst truncate ( -0 , 1 ) ; -0 :: -0 end test ]]" \item "[[ etst truncate ( -1 , 1 ) ; -1 :: -0 end test ]]" \item "[[ etst truncate ( -2 , 1 ) ; -2 :: -0 end test ]]" \item "[[ etst truncate ( -3 , 1 ) ; -3 :: -0 end test ]]" \item "[[ etst truncate ( -4 , 1 ) ; -4 :: -0 end test ]]" \item "[[ etst truncate ( -5 , 1 ) ; -5 :: -0 end test ]]" \item "[[ etst truncate ( -6 , 1 ) ; -6 :: -0 end test ]]" \item "[[ etst truncate ( -7 , 1 ) ; -7 :: -0 end test ]]" \item "[[ etst truncate ( -8 , 1 ) ; -8 :: -0 end test ]]" \item "[[ etst truncate ( -9 , 1 ) ; -9 :: -0 end test ]]" \item "[[ etst truncate ( +0 , 2 ) ; +0 :: +0 end test ]]" \item "[[ etst truncate ( +1 , 2 ) ; +0 :: +1 end test ]]" \item "[[ etst truncate ( +2 , 2 ) ; +1 :: +0 end test ]]" \item "[[ etst truncate ( +3 , 2 ) ; +1 :: +1 end test ]]" \item "[[ etst truncate ( +4 , 2 ) ; +2 :: +0 end test ]]" \item "[[ etst truncate ( +5 , 2 ) ; +2 :: +1 end test ]]" \item "[[ etst truncate ( +6 , 2 ) ; +3 :: +0 end test ]]" \item "[[ etst truncate ( +7 , 2 ) ; +3 :: +1 end test ]]" \item "[[ etst truncate ( +8 , 2 ) ; +4 :: +0 end test ]]" \item "[[ etst truncate ( +9 , 2 ) ; +4 :: +1 end test ]]" \item "[[ etst truncate ( -0 , 2 ) ; -0 :: -0 end test ]]" \item "[[ etst truncate ( -1 , 2 ) ; -0 :: -1 end test ]]" \item "[[ etst truncate ( -2 , 2 ) ; -1 :: -0 end test ]]" \item "[[ etst truncate ( -3 , 2 ) ; -1 :: -1 end test ]]" \item "[[ etst truncate ( -4 , 2 ) ; -2 :: -0 end test ]]" \item "[[ etst truncate ( -5 , 2 ) ; -2 :: -1 end test ]]" \item "[[ etst truncate ( -6 , 2 ) ; -3 :: -0 end test ]]" \item "[[ etst truncate ( -7 , 2 ) ; -3 :: -1 end test ]]" \item "[[ etst truncate ( -8 , 2 ) ; -4 :: -0 end test ]]" \item "[[ etst truncate ( -9 , 2 ) ; -4 :: -1 end test ]]" \item "[[ etst truncate ( +0 , 3 ) ; +0 :: +0 end test ]]" \item "[[ etst truncate ( +1 , 3 ) ; +0 :: +1 end test ]]" \item "[[ etst truncate ( +2 , 3 ) ; +0 :: +2 end test ]]" \item "[[ etst truncate ( +3 , 3 ) ; +1 :: +0 end test ]]" \item "[[ etst truncate ( +4 , 3 ) ; +1 :: +1 end test ]]" \item "[[ etst truncate ( +5 , 3 ) ; +1 :: +2 end test ]]" \item "[[ etst truncate ( +6 , 3 ) ; +2 :: +0 end test ]]" \item "[[ etst truncate ( +7 , 3 ) ; +2 :: +1 end test ]]" \item "[[ etst truncate ( +8 , 3 ) ; +2 :: +2 end test ]]" \item "[[ etst truncate ( +9 , 3 ) ; +3 :: +0 end test ]]" \item "[[ etst truncate ( -0 , 3 ) ; -0 :: -0 end test ]]" \item "[[ etst truncate ( -1 , 3 ) ; -0 :: -1 end test ]]" \item "[[ etst truncate ( -2 , 3 ) ; -0 :: -2 end test ]]" \item "[[ etst truncate ( -3 , 3 ) ; -1 :: -0 end test ]]" \item "[[ etst truncate ( -4 , 3 ) ; -1 :: -1 end test ]]" \item "[[ etst truncate ( -5 , 3 ) ; -1 :: -2 end test ]]" \item "[[ etst truncate ( -6 , 3 ) ; -2 :: -0 end test ]]" \item "[[ etst truncate ( -7 , 3 ) ; -2 :: -1 end test ]]" \item "[[ etst truncate ( -8 , 3 ) ; -2 :: -2 end test ]]" \item "[[ etst truncate ( -9 , 3 ) ; -3 :: -0 end test ]]" \item "[[ etst truncate ( +0 , 4 ) ; +0 :: +0 end test ]]" \item "[[ etst truncate ( +1 , 4 ) ; +0 :: +1 end test ]]" \item "[[ etst truncate ( +2 , 4 ) ; +0 :: +2 end test ]]" \item "[[ etst truncate ( +3 , 4 ) ; +0 :: +3 end test ]]" \item "[[ etst truncate ( +4 , 4 ) ; +1 :: +0 end test ]]" \item "[[ etst truncate ( +5 , 4 ) ; +1 :: +1 end test ]]" \item "[[ etst truncate ( +6 , 4 ) ; +1 :: +2 end test ]]" \item "[[ etst truncate ( +7 , 4 ) ; +1 :: +3 end test ]]" \item "[[ etst truncate ( +8 , 4 ) ; +2 :: +0 end test ]]" \item "[[ etst truncate ( +9 , 4 ) ; +2 :: +1 end test ]]" \item "[[ etst truncate ( -0 , 4 ) ; -0 :: -0 end test ]]" \item "[[ etst truncate ( -1 , 4 ) ; -0 :: -1 end test ]]" \item "[[ etst truncate ( -2 , 4 ) ; -0 :: -2 end test ]]" \item "[[ etst truncate ( -3 , 4 ) ; -0 :: -3 end test ]]" \item "[[ etst truncate ( -4 , 4 ) ; -1 :: -0 end test ]]" \item "[[ etst truncate ( -5 , 4 ) ; -1 :: -1 end test ]]" \item "[[ etst truncate ( -6 , 4 ) ; -1 :: -2 end test ]]" \item "[[ etst truncate ( -7 , 4 ) ; -1 :: -3 end test ]]" \item "[[ etst truncate ( -8 , 4 ) ; -2 :: -0 end test ]]" \item "[[ etst truncate ( -9 , 4 ) ; -2 :: -1 end test ]]" \item "[[ etst truncate ( +0 , 5 ) ; +0 :: +0 end test ]]" \item "[[ etst truncate ( +1 , 5 ) ; +0 :: +1 end test ]]" \item "[[ etst truncate ( +2 , 5 ) ; +0 :: +2 end test ]]" \item "[[ etst truncate ( +3 , 5 ) ; +0 :: +3 end test ]]" \item "[[ etst truncate ( +4 , 5 ) ; +0 :: +4 end test ]]" \item "[[ etst truncate ( +5 , 5 ) ; +1 :: +0 end test ]]" \item "[[ etst truncate ( +6 , 5 ) ; +1 :: +1 end test ]]" \item "[[ etst truncate ( +7 , 5 ) ; +1 :: +2 end test ]]" \item "[[ etst truncate ( +8 , 5 ) ; +1 :: +3 end test ]]" \item "[[ etst truncate ( +9 , 5 ) ; +1 :: +4 end test ]]" \item "[[ etst truncate ( -0 , 5 ) ; -0 :: -0 end test ]]" \item "[[ etst truncate ( -1 , 5 ) ; -0 :: -1 end test ]]" \item "[[ etst truncate ( -2 , 5 ) ; -0 :: -2 end test ]]" \item "[[ etst truncate ( -3 , 5 ) ; -0 :: -3 end test ]]" \item "[[ etst truncate ( -4 , 5 ) ; -0 :: -4 end test ]]" \item "[[ etst truncate ( -5 , 5 ) ; -1 :: -0 end test ]]" \item "[[ etst truncate ( -6 , 5 ) ; -1 :: -1 end test ]]" \item "[[ etst truncate ( -7 , 5 ) ; -1 :: -2 end test ]]" \item "[[ etst truncate ( -8 , 5 ) ; -1 :: -3 end test ]]" \item "[[ etst truncate ( -9 , 5 ) ; -1 :: -4 end test ]]" \item "[[ etst truncate ( -5 , 0 ) ; exception end test ]]" \item "[[ etst truncate ( -1 , 0 ) ; exception end test ]]" \item "[[ etst truncate ( +0 , 0 ) ; exception end test ]]" \item "[[ etst truncate ( +1 , 0 ) ; exception end test ]]" \item "[[ etst truncate ( +5 , 0 ) ; exception end test ]]" \item "[[ etst truncate ( -5 , -1 ) ; exception end test ]]" \item "[[ etst truncate ( -1 , -1 ) ; exception end test ]]" \item "[[ etst truncate ( +0 , -1 ) ; exception end test ]]" \item "[[ etst truncate ( +1 , -1 ) ; exception end test ]]" \item "[[ etst truncate ( +5 , -1 ) ; exception end test ]]" \end{statements}" ]" \subsection{round} "[ "\begin{statements} \item "[[ etst round ( -9 , 1 ) ; -9 :: +0 end test ]]" \item "[[ etst round ( -8 , 1 ) ; -8 :: +0 end test ]]" \item "[[ etst round ( -7 , 1 ) ; -7 :: +0 end test ]]" \item "[[ etst round ( -6 , 1 ) ; -6 :: +0 end test ]]" \item "[[ etst round ( -5 , 1 ) ; -5 :: +0 end test ]]" \item "[[ etst round ( -4 , 1 ) ; -4 :: +0 end test ]]" \item "[[ etst round ( -3 , 1 ) ; -3 :: +0 end test ]]" \item "[[ etst round ( -2 , 1 ) ; -2 :: +0 end test ]]" \item "[[ etst round ( -1 , 1 ) ; -1 :: +0 end test ]]" \item "[[ etst round ( +0 , 1 ) ; +0 :: +0 end test ]]" \item "[[ etst round ( +1 , 1 ) ; +1 :: +0 end test ]]" \item "[[ etst round ( +2 , 1 ) ; +2 :: +0 end test ]]" \item "[[ etst round ( +3 , 1 ) ; +3 :: +0 end test ]]" \item "[[ etst round ( +4 , 1 ) ; +4 :: +0 end test ]]" \item "[[ etst round ( +5 , 1 ) ; +5 :: +0 end test ]]" \item "[[ etst round ( +6 , 1 ) ; +6 :: +0 end test ]]" \item "[[ etst round ( +7 , 1 ) ; +7 :: +0 end test ]]" \item "[[ etst round ( +8 , 1 ) ; +8 :: +0 end test ]]" \item "[[ etst round ( +9 , 1 ) ; +9 :: +0 end test ]]" \item "[[ etst round ( -9 , 2 ) ; -4 :: -1 end test ]]" \item "[[ etst round ( -8 , 2 ) ; -4 :: +0 end test ]]" \item "[[ etst round ( -7 , 2 ) ; -4 :: +1 end test ]]" \item "[[ etst round ( -6 , 2 ) ; -3 :: +0 end test ]]" \item "[[ etst round ( -5 , 2 ) ; -2 :: -1 end test ]]" \item "[[ etst round ( -4 , 2 ) ; -2 :: +0 end test ]]" \item "[[ etst round ( -3 , 2 ) ; -2 :: +1 end test ]]" \item "[[ etst round ( -2 , 2 ) ; -1 :: +0 end test ]]" \item "[[ etst round ( -1 , 2 ) ; -0 :: -1 end test ]]" \item "[[ etst round ( +0 , 2 ) ; +0 :: +0 end test ]]" \item "[[ etst round ( +1 , 2 ) ; +0 :: +1 end test ]]" \item "[[ etst round ( +2 , 2 ) ; +1 :: +0 end test ]]" \item "[[ etst round ( +3 , 2 ) ; +2 :: -1 end test ]]" \item "[[ etst round ( +4 , 2 ) ; +2 :: +0 end test ]]" \item "[[ etst round ( +5 , 2 ) ; +2 :: +1 end test ]]" \item "[[ etst round ( +6 , 2 ) ; +3 :: +0 end test ]]" \item "[[ etst round ( +7 , 2 ) ; +4 :: -1 end test ]]" \item "[[ etst round ( +8 , 2 ) ; +4 :: +0 end test ]]" \item "[[ etst round ( +9 , 2 ) ; +4 :: +1 end test ]]" \item "[[ etst round ( -9 , 3 ) ; -3 :: +0 end test ]]" \item "[[ etst round ( -8 , 3 ) ; -3 :: +1 end test ]]" \item "[[ etst round ( -7 , 3 ) ; -2 :: -1 end test ]]" \item "[[ etst round ( -6 , 3 ) ; -2 :: +0 end test ]]" \item "[[ etst round ( -5 , 3 ) ; -2 :: +1 end test ]]" \item "[[ etst round ( -4 , 3 ) ; -1 :: -1 end test ]]" \item "[[ etst round ( -3 , 3 ) ; -1 :: +0 end test ]]" \item "[[ etst round ( -2 , 3 ) ; -1 :: +1 end test ]]" \item "[[ etst round ( -1 , 3 ) ; +0 :: -1 end test ]]" \item "[[ etst round ( +0 , 3 ) ; +0 :: +0 end test ]]" \item "[[ etst round ( +1 , 3 ) ; +0 :: +1 end test ]]" \item "[[ etst round ( +2 , 3 ) ; +1 :: -1 end test ]]" \item "[[ etst round ( +3 , 3 ) ; +1 :: +0 end test ]]" \item "[[ etst round ( +4 , 3 ) ; +1 :: +1 end test ]]" \item "[[ etst round ( +5 , 3 ) ; +2 :: -1 end test ]]" \item "[[ etst round ( +6 , 3 ) ; +2 :: +0 end test ]]" \item "[[ etst round ( +7 , 3 ) ; +2 :: +1 end test ]]" \item "[[ etst round ( +8 , 3 ) ; +3 :: -1 end test ]]" \item "[[ etst round ( +9 , 3 ) ; +3 :: +0 end test ]]" \item "[[ etst round ( -9 , 4 ) ; -2 :: -1 end test ]]" \item "[[ etst round ( -8 , 4 ) ; -2 :: +0 end test ]]" \item "[[ etst round ( -7 , 4 ) ; -2 :: +1 end test ]]" \item "[[ etst round ( -6 , 4 ) ; -2 :: +2 end test ]]" \item "[[ etst round ( -5 , 4 ) ; -1 :: -1 end test ]]" \item "[[ etst round ( -4 , 4 ) ; -1 :: +0 end test ]]" \item "[[ etst round ( -3 , 4 ) ; -1 :: +1 end test ]]" \item "[[ etst round ( -2 , 4 ) ; +0 :: -2 end test ]]" \item "[[ etst round ( -1 , 4 ) ; +0 :: -1 end test ]]" \item "[[ etst round ( +0 , 4 ) ; +0 :: +0 end test ]]" \item "[[ etst round ( +1 , 4 ) ; +0 :: +1 end test ]]" \item "[[ etst round ( +2 , 4 ) ; +0 :: +2 end test ]]" \item "[[ etst round ( +3 , 4 ) ; +1 :: -1 end test ]]" \item "[[ etst round ( +4 , 4 ) ; +1 :: +0 end test ]]" \item "[[ etst round ( +5 , 4 ) ; +1 :: +1 end test ]]" \item "[[ etst round ( +6 , 4 ) ; +2 :: -2 end test ]]" \item "[[ etst round ( +7 , 4 ) ; +2 :: -1 end test ]]" \item "[[ etst round ( +8 , 4 ) ; +2 :: +0 end test ]]" \item "[[ etst round ( +9 , 4 ) ; +2 :: +1 end test ]]" \item "[[ etst round ( -9 , 5 ) ; -2 :: +1 end test ]]" \item "[[ etst round ( -8 , 5 ) ; -2 :: +2 end test ]]" \item "[[ etst round ( -7 , 5 ) ; -1 :: -2 end test ]]" \item "[[ etst round ( -6 , 5 ) ; -1 :: -1 end test ]]" \item "[[ etst round ( -5 , 5 ) ; -1 :: +0 end test ]]" \item "[[ etst round ( -4 , 5 ) ; -1 :: +1 end test ]]" \item "[[ etst round ( -3 , 5 ) ; -1 :: +2 end test ]]" \item "[[ etst round ( -2 , 5 ) ; +0 :: -2 end test ]]" \item "[[ etst round ( -1 , 5 ) ; +0 :: -1 end test ]]" \item "[[ etst round ( +0 , 5 ) ; +0 :: +0 end test ]]" \item "[[ etst round ( +1 , 5 ) ; +0 :: +1 end test ]]" \item "[[ etst round ( +2 , 5 ) ; +0 :: +2 end test ]]" \item "[[ etst round ( +3 , 5 ) ; +1 :: -2 end test ]]" \item "[[ etst round ( +4 , 5 ) ; +1 :: -1 end test ]]" \item "[[ etst round ( +5 , 5 ) ; +1 :: +0 end test ]]" \item "[[ etst round ( +6 , 5 ) ; +1 :: +1 end test ]]" \item "[[ etst round ( +7 , 5 ) ; +1 :: +2 end test ]]" \item "[[ etst round ( +8 , 5 ) ; +2 :: -2 end test ]]" \item "[[ etst round ( +9 , 5 ) ; +2 :: -1 end test ]]" \item "[[ etst round ( -5 , 0 ) ; exception end test ]]" \item "[[ etst round ( -1 , 0 ) ; exception end test ]]" \item "[[ etst round ( +0 , 0 ) ; exception end test ]]" \item "[[ etst round ( +1 , 0 ) ; exception end test ]]" \item "[[ etst round ( +5 , 0 ) ; exception end test ]]" \item "[[ etst round ( -5 , -1 ) ; exception end test ]]" \item "[[ etst round ( -1 , -1 ) ; exception end test ]]" \item "[[ etst round ( +0 , -1 ) ; exception end test ]]" \item "[[ etst round ( +1 , -1 ) ; exception end test ]]" \item "[[ etst round ( +5 , -1 ) ; exception end test ]]" \end{statements}" ]" \section{Vectors} \subsection{Elementary operations} "[ "\begin{statements} \item "[[ ttst vector-empty ( "". ) end test ]]" \item "[[ ftst vector-empty ( "a" ) end test ]]" \item "[[ ttst vector-empty ( -1 ) end test ]]" \item "[[ ttst vector-empty ( 255 ) end test ]]" \item "[[ etst vector-head1 ( show "abc" end show ) ; 97 end test ]]" \item "[[ etst vector-tail1 ( show "abc" end show ) ; show "bc" end show end test ]]" \end{statements}" ]" \subsection{vector} "[ "\begin{statements} \item "[[ etst vector ( show "abc" end show ) ; show "abc" end show end test ]]" \item "[[ etst vector ( 0 ) ; show "". end show end test ]]" \item "[[ etst vector ( 1 ) ; show "". end show end test ]]" \item "[[ etst vector ( 97 ) ; show "". end show end test ]]" \item "[[ etst vector ( 97 + 256 * 1 ) ; show "a" end show end test ]]" \item "[[ etst vector ( 97 + 256 * 2 ) ; show "a" end show end test ]]" \item "[[ etst vector ( 97 + 256 * 255 ) ; show "a" end show end test ]]" \item "[[ etst vector ( 97 + 256 * 256 ) ; 97 + 256 * 256 end test ]]" \item "[[ etst vector ( -1 ) ; show "". end show end test ]]" \item "[[ etst vector ( -1000 ) ; show "". end show end test ]]" \end{statements}" ]" \subsection{vector-norm} "[ "\begin{statements} \item "[[ etst vector-norm ( show "abc" end show ) ; show "abc" end show end test ]]" \item "[[ etst vector-norm ( 0 ) ; show true end show end test ]]" \item "[[ etst vector-norm ( 1 ) ; show "". end show end test ]]" \item "[[ etst vector-norm ( 97 ) ; show true end show end test ]]" \item "[[ etst vector-norm ( 97 + 256 * 1 ) ; show "a" end show end test ]]" \item "[[ etst vector-norm ( 97 + 256 * 2 ) ; show true end show end test ]]" \item "[[ etst vector-norm ( 97 + 256 * 255 ) ; show true end show end test ]]" \item "[[ etst vector-norm ( 97 + 256 * 256 ) ; 97 + 256 * 256 end test ]]" \item "[[ etst vector-norm ( -1 ) ; show true end show end test ]]" \item "[[ etst vector-norm ( -1000 ) ; show true end show end test ]]" \end{statements}" ]" \subsection{vector-prefix} "[ "\begin{statements} \item "[[ etst vector-prefix ( show "abc" end show , -1 ) ; show "". end show end test ]]" \item "[[ etst vector-prefix ( show "abc" end show , 0 ) ; show "". end show end test ]]" \item "[[ etst vector-prefix ( show "abc" end show , 1 ) ; show "a" end show end test ]]" \item "[[ etst vector-prefix ( show "abc" end show , 2 ) ; show "ab" end show end test ]]" \item "[[ etst vector-prefix ( show "abc" end show , 3 ) ; show "abc" end show end test ]]" \item "[[ etst vector-prefix ( show "abc" end show , 4 ) ; show "abc" end show end test ]]" \item "[[ etst vector-prefix ( 97 + 98 * 256 + 2 * 65536 , -1 ) ; show "". end show end test ]]" \item "[[ etst vector-prefix ( 97 + 98 * 256 + 2 * 65536 , 0 ) ; show "". end show end test ]]" \item "[[ etst vector-prefix ( 97 + 98 * 256 + 2 * 65536 , 1 ) ; show "a" end show end test ]]" \item "[[ etst vector-prefix ( 97 + 98 * 256 + 2 * 65536 , 2 ) ; show "ab" end show end test ]]" \item "[[ etst vector-prefix ( 97 + 98 * 256 + 2 * 65536 , 3 ) ; show "ab" end show end test ]]" \item "[[ etst vector-prefix ( -1000 , 3 ) ; show "". end show end test ]]" \end{statements}" ]" \subsection{vector-suffix} "[ "\begin{statements} \item "[[ etst vector-suffix ( show "abc" end show , -1 ) ; show "abc" end show end test ]]" \item "[[ etst vector-suffix ( show "abc" end show , 0 ) ; show "abc" end show end test ]]" \item "[[ etst vector-suffix ( show "abc" end show , 1 ) ; show "bc" end show end test ]]" \item "[[ etst vector-suffix ( show "abc" end show , 2 ) ; show "c" end show end test ]]" \item "[[ etst vector-suffix ( show "abc" end show , 3 ) ; show "". end show end test ]]" \item "[[ etst vector-suffix ( show "abc" end show , 4 ) ; show "". end show end test ]]" \item "[[ etst vector-suffix ( 97 + 98 * 256 + 2 * 65536 , -1 ) ; show "ab" end show end test ]]" \item "[[ etst vector-suffix ( 97 + 98 * 256 + 2 * 65536 , 0 ) ; show "ab" end show end test ]]" \item "[[ etst vector-suffix ( 97 + 98 * 256 + 2 * 65536 , 1 ) ; show "b" end show end test ]]" \item "[[ etst vector-suffix ( 97 + 98 * 256 + 2 * 65536 , 2 ) ; show "". end show end test ]]" \item "[[ etst vector-suffix ( 97 + 98 * 256 + 2 * 65536 , 3 ) ; show "". end show end test ]]" \item "[[ etst vector-suffix ( -1000 , 0 ) ; show "". end show end test ]]" \end{statements}" ]" \subsection{vector-subseq} "[ "\begin{statements} \item "[[ etst vector-subseq ( show "ab" end show , -1 , -1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , -1 , 0 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , -1 , 1 ) ; show "a" end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , -1 , 2 ) ; show "ab" end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , -1 , 3 ) ; show "ab" end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 0 , -1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 0 , 0 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 0 , 1 ) ; show "a" end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 0 , 2 ) ; show "ab" end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 0 , 3 ) ; show "ab" end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 1 , -1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 1 , 0 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 1 , 1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 1 , 2 ) ; show "b" end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 1 , 3 ) ; show "b" end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 2 , -1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 2 , 0 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 2 , 1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 2 , 2 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 2 , 3 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 3 , -1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 3 , 0 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 3 , 1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 3 , 2 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( show "ab" end show , 3 , 3 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , -1 , -1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , -1 , 0 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , -1 , 1 ) ; show "a" end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , -1 , 2 ) ; show "ab" end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , -1 , 3 ) ; show "ab" end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 0 , -1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 0 , 0 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 0 , 1 ) ; show "a" end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 0 , 2 ) ; show "ab" end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 0 , 3 ) ; show "ab" end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 1 , -1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 1 , 0 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 1 , 1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 1 , 2 ) ; show "b" end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 1 , 3 ) ; show "b" end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 2 , -1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 2 , 0 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 2 , 1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 2 , 2 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 2 , 3 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 3 , -1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 3 , 0 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 3 , 1 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 3 , 2 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( 97 + 98 * 256 + 2 * 65536 , 3 , 3 ) ; show "". end show end test ]]" \item "[[ etst vector-subseq ( -1000 , 0 , 3 ) ; show "". end show end test ]]" \end{statements}" ]" \subsection{vector-length} "[ "\begin{statements} \item "[[ etst vector-length ( show "". end show ) ; 0 end test ]]" \item "[[ etst vector-length ( show "a" end show ) ; 1 end test ]]" \item "[[ etst vector-length ( show "abc" end show ) ; 3 end test ]]" \item "[[ etst vector-length ( 97 + 98 * 256 + 2 * 65536 ) ; 2 end test ]]" \item "[[ etst vector-length ( -1000 ) ; 0 end test ]]" \end{statements}" ]" \subsection{vector-index} "[ "\begin{statements} \item "[[ etst vector-index ( show "abc" end show , -1 ) ; exception end test ]]" \item "[[ etst vector-index ( show "abc" end show , 0 ) ; 97 end test ]]" \item "[[ etst vector-index ( show "abc" end show , 1 ) ; 98 end test ]]" \item "[[ etst vector-index ( show "abc" end show , 2 ) ; 99 end test ]]" \item "[[ etst vector-index ( show "abc" end show , 3 ) ; exception end test ]]" \item "[[ etst vector-index ( show "". end show , -1 ) ; exception end test ]]" \item "[[ etst vector-index ( show "". end show , 0 ) ; exception end test ]]" \item "[[ etst vector-index ( 97 + 98 * 256 + 2 * 65536 , -1 ) ; exception end test ]]" \item "[[ etst vector-index ( 97 + 98 * 256 + 2 * 65536 , 0 ) ; 97 end test ]]" \item "[[ etst vector-index ( 97 + 98 * 256 + 2 * 65536 , 1 ) ; 98 end test ]]" \item "[[ etst vector-index ( 97 + 98 * 256 + 2 * 65536 , 2 ) ; exception end test ]]" \end{statements}" ]" \subsection{vector-head and vector-tail} "[ "\begin{statements} \item "[[ etst vector-head ( show "ABC" end show ) ; 65 end test ]]" \item "[[ etst vector-tail ( show "ABC" end show ) ; show "BC" end show end test ]]" \end{statements}" ]" \subsection{vector2byte*} "[ "\begin{statements} \item "[[ etst vector2byte* ( show "". end show ) ; <<>> end test ]]" \item "[[ etst vector2byte* ( show "A" end show ) ; << 65 >> end test ]]" \item "[[ etst vector2byte* ( show "ABC" end show ) ; << 65 ,, 66 ,, 67 >> end test ]]" \end{statements}" ]" \subsection{vector2vector*} "[ "\begin{statements} \item "[[ etst vector2vector* ( show "". end show ) ; <<>> end test ]]" \item "[[ etst vector2vector* ( show "A" end show ) ; << "A" >> end test ]]" \item "[[ etst vector2vector* ( show "ABC" end show ) ; << "A" ,, "B" ,, "C" >> end test ]]" \end{statements}" ]" \subsection{bt2byte*} "[ "\begin{statements} \item "[[ etst bt2byte* ( 65 ) ; << 65 >> end test ]]" \item "[[ etst bt2byte* ( -1 ) ; <<>> end test ]]" \item "[[ etst bt2byte* ( 256 ) ; <<>> end test ]]" \item "[[ etst bt2byte* ( true ) ; <<>> end test ]]" \item "[[ etst bt2byte* ( false ) ; <<>> end test ]]" \item "[[ etst bt2byte* ( map ( \ x . x ) ) ; <<>> end test ]]" \item "[[ etst bt2byte* ( 65 :: 66 ) ; << 65 ,, 66 >> end test ]]" \item "[[ etst bt2byte* ( ( 65 :: 66 ) :: ( 67 :: 68 ) ) ; << 65 ,, 66 ,, 67 ,, 68 >> end test ]]" \item "[[ etst bt2byte* ( ( 65 :: 66 ) :: true :: 67 :: false :: 68 ) ; << 65 ,, 66 ,, 67 ,, 68 >> end test ]]" \end{statements}" ]" \subsection{bt2vector*} "[ "\begin{statements} \item "[[ etst bt2vector* ( 65 ) ; << 65 + 256 >> end test ]]" \item "[[ etst bt2vector* ( -1 ) ; <<>> end test ]]" \item "[[ etst bt2vector* ( 256 ) ; <<>> end test ]]" \item "[[ etst bt2vector* ( true ) ; <<>> end test ]]" \item "[[ etst bt2vector* ( false ) ; <<>> end test ]]" \item "[[ etst bt2vector* ( map ( \ x . x ) ) ; <<>> end test ]]" \item "[[ etst bt2vector* ( 65 :: 66 ) ; << "A" ,, "B" >> end test ]]" \item "[[ etst bt2vector* ( ( 65 :: 66 ) :: ( 67 :: 68 ) ) ; << "A" ,, "B" ,, "C" ,, "D" >> end test ]]" \item "[[ etst bt2vector* ( ( 65 :: 66 ) :: true :: 67 :: false :: 68 ) ; << "A" ,, "B" ,, "C" ,, "D" >> end test ]]" \end{statements}" ]" \subsection{bt2vector} "[ "\begin{statements} \item "[[ etst bt2vector ( 65 ) ; show "A" end show end test ]]" \item "[[ etst bt2vector ( -1 ) ; show "". end show end test ]]" \item "[[ etst bt2vector ( 256 ) ; show "". end show end test ]]" \item "[[ etst bt2vector ( true ) ; show "". end show end test ]]" \item "[[ etst bt2vector ( false ) ; show "". end show end test ]]" \item "[[ etst bt2vector ( map ( \ x . x ) ) ; show "". end show end test ]]" \item "[[ etst bt2vector ( 65 :: 66 ) ; show "AB" end show end test ]]" \item "[[ etst bt2vector ( ( 65 :: 66 ) :: ( 67 :: 68 ) ) ; show "ABCD" end show end test ]]" \item "[[ etst bt2vector ( ( 65 :: 66 ) :: true :: 67 :: false :: 68 ) ; show "ABCD" end show end test ]]" \end{statements}" ]" \subsection{vt2byte*} "[ "\begin{statements} \item "[[ etst vt2byte* ( show "". end show ) ; <<>> end test ]]" \item "[[ etst vt2byte* ( show "A" end show ) ; << 65 >> end test ]]" \item "[[ etst vt2byte* ( show "AB" end show ) ; << 65 ,, 66 >> end test ]]" \item "[[ etst vt2byte* ( -1 ) ; <<>> end test ]]" \item "[[ etst vt2byte* ( 65 + 2 * 256 ) ; << 65 >> end test ]]" \item "[[ etst vt2byte* ( true ) ; <<>> end test ]]" \item "[[ etst vt2byte* ( false ) ; <<>> end test ]]" \item "[[ etst vt2byte* ( map ( \ x . x ) ) ; <<>> end test ]]" \item "[[ etst vt2byte* ( show "AB" end show :: "CD" ) ; << 65 ,, 66 ,, 67 ,, 68 >> end test ]]" \item "[[ etst vt2byte* ( ( show "A" end show :: show "B" end show ) :: ( show "C" end show :: "D" ) ) ; << 65 ,, 66 ,, 67 ,, 68 >> end test ]]" \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 ]]" \end{statements}" ]" \subsection{vt2vector*} "[ "\begin{statements} \item "[[ etst vt2vector* ( show "". end show ) ; <<>> end test ]]" \item "[[ etst vt2vector* ( show "A" end show ) ; << "A" >> end test ]]" \item "[[ etst vt2vector* ( show "AB" end show ) ; << "A" ,, "B" >> end test ]]" \item "[[ etst vt2vector* ( -1 ) ; <<>> end test ]]" \item "[[ etst vt2vector* ( 65 + 2 * 256 ) ; << "A" >> end test ]]" \item "[[ etst vt2vector* ( true ) ; <<>> end test ]]" \item "[[ etst vt2vector* ( false ) ; <<>> end test ]]" \item "[[ etst vt2vector* ( map ( \ x . x ) ) ; <<>> end test ]]" \item "[[ etst vt2vector* ( show "AB" end show :: "CD" ) ; << "A" ,, "B" ,, "C" ,, "D" >> end test ]]" \item "[[ etst vt2vector* ( ( show "A" end show :: show "B" end show ) :: ( show "C" end show :: "D" ) ) ; << "A" ,, "B" ,, "C" ,, "D" >> end test ]]" \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 ]]" \end{statements}" ]" \subsection{vt2vector} "[ "\begin{statements} \item "[[ etst vt2vector ( show "". end show ) ; show "". end show end test ]]" \item "[[ etst vt2vector ( show "A" end show ) ; show "A" end show end test ]]" \item "[[ etst vt2vector ( show "AB" end show ) ; show "AB" end show end test ]]" \item "[[ etst vt2vector ( -1 ) ; show "". end show end test ]]" \item "[[ etst vt2vector ( 65 + 2 * 256 ) ; show "A" end show end test ]]" \item "[[ etst vt2vector ( true ) ; show "". end show end test ]]" \item "[[ etst vt2vector ( false ) ; show "". end show end test ]]" \item "[[ etst vt2vector ( map ( \ x . x ) ) ; show "". end show end test ]]" \item "[[ etst vt2vector ( show "AB" end show :: "CD" ) ; show "ABCD" end show end test ]]" \item "[[ etst vt2vector ( ( show "A" end show :: show "B" end show ) :: ( show "C" end show :: "D" ) ) ; show "ABCD" end show end test ]]" \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 ]]" \end{statements}" ]" \section{Structures} \subsection{List access} "[ "\begin{statements} \item "[[ ttst 2 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) zeroth end test ]]" \item "[[ ttst 3 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) first end test ]]" \item "[[ ttst 4 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) second end test ]]" \item "[[ ttst 5 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) third end test ]]" \item "[[ ttst 6 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) fourth end test ]]" \item "[[ ttst 7 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) fifth end test ]]" \item "[[ ttst 8 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) sixth end test ]]" \item "[[ ttst 9 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) seventh end test ]]" \item "[[ ttst 0 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) eighth end test ]]" \item "[[ ttst 1 = ( 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 0 :: 1 :: true ) ninth end test ]]" \end{statements}" ]" \subsection{Tree access} "[ "\begin{statements} \item "[[ ttst quote base end quote ref = quote x + y end quote ref end test ]]" \item "[[ ttst quote base end quote idx = 0 end test ]]" \item "[[ ttst quote "abc" end quote ref = 0 end test ]]" \item "[[ ttst quote "abc" end quote idx = "abc" end test ]]" \end{statements}" ]" \subsection{Tree equality} "[ "\begin{statements} \item "[[ ttst quote x + y end quote t= quote x + y end quote end test ]]" \item "[[ ftst quote x + y end quote t= quote z + y end quote end test ]]" \item "[[ ftst quote x + y end quote t= quote x + z end quote end test ]]" \item "[[ ftst quote x + y end quote t= quote x - y end quote end test ]]" \item "[[ ttst 1 = lookup ( quote x end quote , ( quote x end quote :: 1 ) :: ( quote y _ { 1 } end quote :: 2 ) :: ( quote y _ { 2 } end quote :: 3 ) :: true , true ) end test ]]" \item "[[ ttst 2 = lookup ( quote y _ { 1 } end quote , ( quote x end quote :: 1 ) :: ( quote y _ { 1 } end quote :: 2 ) :: ( quote y _ { 2 } end quote :: 3 ) :: true , true ) end test ]]" \item "[[ ttst 3 = lookup ( quote y _ { 2 } end quote , ( quote x end quote :: 1 ) :: ( quote y _ { 1 } end quote :: 2 ) :: ( quote y _ { 2 } end quote :: 3 ) :: true , true ) end test ]]" \item "[[ ttst true = lookup ( quote y _ { 3 } end quote , ( quote x end quote :: 1 ) :: ( quote y _ { 1 } end quote :: 2 ) :: ( quote y _ { 2 } end quote :: 3 ) :: true , true ) end test ]]" \item "[[ ttst false = lookup ( quote y _ { 3 } end quote , ( quote x end quote :: 1 ) :: ( quote y _ { 1 } end quote :: 2 ) :: ( quote y _ { 2 } end quote :: 3 ) :: true , false ) end test ]]" \end{statements}" ]" \subsection{Arrays} "[ "\begin{statements} \item "[[ ttst true [[ 2 ]] end test ]]" \item "[[ ttst 12 = true [[ 2 -> 12 ]] [[ 2 ]] end test ]]" \item "[[ ttst true [[ 2 -> 12 ]] [[ 3 ]] end test ]]" \item "[[ ttst 12 = true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 2 ]] end test ]]" \item "[[ ttst 13 = true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 3 ]] end test ]]" \item "[[ ttst true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 4 ]] end test ]]" \item "[[ ttst 12 = true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 10 -> 14 ]] [[ 2 ]] end test ]]" \item "[[ ttst 13 = true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 10 -> 14 ]] [[ 3 ]] end test ]]" \item "[[ ttst 14 = true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 10 -> 14 ]] [[ 10 ]] end test ]]" \item "[[ ttst true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 10 -> 14 ]] [[ 5 ]] end test ]]" \item "[[ ttst true [[ 2 -> 12 ]] [[ 3 -> 13 ]] [[ 10 -> 14 ]] [[ 2 -> true ]] = true [[ 10 -> 14 ]] [[ 3 -> 13 ]] end test ]]" \item "[[ etst true [[ 2 :: 3 :: 4 :: true => 5 ]] [[ 2 :: 4 :: true => 6 ]] [[ 2 ]] [[ 3 ]] [[ 4 ]] ; 5 end test ]]" \item "[[ etst true [[ 2 :: 3 :: 4 :: true => 5 ]] [[ 2 :: 4 :: true => 6 ]] [[ 2 ]] [[ 4 ]] ; 6 end test ]]" \item "[[ etst true [[ 2 :: 3 :: 4 :: true => 5 ]] [[ 2 :: 4 :: true => 6 ]] [[ 2 ]] [[ 5 ]] ; true end test ]]" \item "[[ etst true [[ "code" -> 3 ]] [[ "codex" -> 4 ]] [[ "code" ]] ; 3 end test ]]" \item "[[ etst true [[ "code" :: true => 3 ]] [[ "codex" :: true => 4 ]] [[ "code" ]] ; 3 end test ]]" \item "[[ etst true [[ 1 :: "code" :: true => 3 ]] [[ 1 :: "codex" :: true => 4 ]] [[ 1 ]] [[ "code" ]] ; 3 end test ]]" \item "[[ etst true [[ 1 :: "code" :: 2 :: true => 3 ]] [[ 1 :: "codex" :: 2 :: true => 4 ]] [[ 1 ]] [[ "code" ]] [[ 2 ]] ; 3 end test ]]" \end{statements}" ]" \section{Evaluation} \subsection{The page symbol} "[ "\begin{statements} \item "[[ ttst base [[ 0 ]] = quote base end quote ref end test ]]" \item "[[ ttst base [[ quote base end quote ref ]] [[ "vector" ]] intp end test ]]" \item "[[ ttst base [[ quote base end quote ref ]] [[ "bibliography" ]] = quote base end quote ref :: true end test ]]" \item "[[ ttst base [[ quote base end quote ref ]] [[ "dictionary" ]] [[ quote x + y end quote idx ]] = 2 end test ]]" \item "[[ ttst base [[ quote base end quote ref ]] [[ "body" ]] pairp end test ]]" \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 ]]" \item "[[ ttst base [[ quote base end quote ref ]] [[ "expansion" ]] pairp end test ]]" \item "[[ ttst base [[ quote base end quote ref ]] [[ "code" ]] [[ quote x - y end quote idx ]] Tail ' 2 ' 3 = -1 end test ]]" \item "[[ ttst base [[ quote base end quote ref ]] [[ "cluster" ]] = true end test ]]" \item "[[ ttst base [[ quote base end quote ref ]] [[ "diagnose" ]] untag = true end test ]]" \end{statements}" ]" \subsection{eval} "[ "\begin{statements} \item "[[ ttst 2 = eval ( quote 2 end quote , true , base ) untag end test ]]" \item "[[ ttst -1 = eval ( quote 2 - 3 end quote , true , base ) untag end test ]]" \item "[[ ttst "abc" = eval ( quote "abc" end quote , true , base ) untag end test ]]" \item "[[ ttst quote x + y end quote ref = eval ( quote base [[ 0 ]] end quote , true , base ) untag end test ]]" \item "[[ ttst quote 2 - 3 end quote t= eval ( quote quote 2 - 3 end quote end quote , true , base ) untag end test ]]" \item "[[ ttst -1 = eval ( quote \ x . x - 3 end quote , true , base ) Tail ' 2 end test ]]" \item "[[ ttst -1 = eval ( quote ( \ x . x - 3 ) ' 2 end quote , true , base ) untag end test ]]" \item "[[ ttst 6 = eval ( quote ( \ x . x ' x ) ' ( \ f . \ x . f ' ( f ' x ) ) ' ( \ x . x + 1 ) ' 2 end quote , true , base ) untag end test ]]" \end{statements}" ]" \section{Macro expansion} \subsection{Parentheses} "[ "\begin{statements} \item "[[ ttst quote ( 2 ) end quote t= quote 2 end quote end test ]]" \item "[[ ttst quote newline 2 end quote t= quote 2 end quote end test ]]" \end{statements}" ]" \subsection{Tuples} "[ "\begin{statements} \item "[[ ttst quote << 2 ,, 3 ,, 4 >> end quote t= quote 2 :: 3 :: 4 :: <<>> end quote end test ]]" \end{statements}" ]" \subsection{Eager definitions} "[ "\begin{statements} \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 ]]" \end{statements}" ]" \subsection{Let} "[ "\begin{statements} \item "[[ ttst quote let 3 := 4 in 2 end quote t= quote 2 end quote end test ]]" \item "[[ ttst quote let 3 := 4 in 3 end quote t= quote 4 end quote end test ]]" \item "[[ ttst quote let 3 := 4 in 4 end quote t= quote 4 end quote end test ]]" \item "[[ ttst make-var ( quote x end quote ) t= quote asterisk end quote end test ]]" \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 ]]" \item "[[ ttst make-prime ( quote x end quote ) t= quote x prime end quote end test ]]" \item "[[ ttst make-head ( quote x end quote ) t= quote x head end quote end test ]]" \item "[[ ttst make-tail ( quote x end quote ) t= quote x tail end quote end test ]]" \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 ]]" \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 ]]" \item "[[ ttst let1 ( protect quote let u :: v = y in z end quote end protect :: macrostate0 :: self :: true ) t= quote newline LET y BE asterisk IN newline LET ( if asterisk atom then asterisk else asterisk head ) :: ( if asterisk atom then asterisk else asterisk tail ) :: true BE asterisk prime IN newline LET asterisk prime head BE asterisk IN newline LET asterisk prime tail BE asterisk prime IN newline LET asterisk BE u IN newline LET asterisk prime head BE asterisk IN newline LET asterisk prime tail BE asterisk prime IN newline LET asterisk BE v IN z end quote end test ]]" \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 ]]" \item "[[ ttst quote let 2 = y in z end quote t= quote LET y BE asterisk IN z end quote end test ]]" \item "[[ ttst quote let u :: v = y in z end quote t= quote newline LET y BE asterisk IN newline LET ( if asterisk atom then asterisk else asterisk head ) :: ( if asterisk atom then asterisk else asterisk tail ) :: true BE asterisk prime IN newline LET asterisk prime head BE asterisk IN newline LET asterisk prime tail BE asterisk prime IN newline LET asterisk BE u IN newline LET asterisk prime head BE asterisk IN newline LET asterisk prime tail BE asterisk prime IN newline LET asterisk BE v IN z end quote end test ]]" \item "[[ etst let u = 2 in u ; 2 end test ]]" \item "[[ etst let u :: v = 2 in u ; 2 end test ]]" \item "[[ etst let u :: v = 2 in v ; 2 end test ]]" \item "[[ etst let u :: v = 3 in v ; 3 end test ]]" \item "[[ etst let u :: v = 2 :: 3 in u ; 2 end test ]]" \item "[[ etst let u :: v = 2 :: 3 in v ; 3 end test ]]" \item "[[ etst let u :: v = 2 :: 3 in 4 ; 4 end test ]]" \item "[[ etst let ( u ) = 2 in u ; 2 end test ]]" \item "[[ etst let ( ( u :: v ) :: ( w :: x ) ) = ( ( 1 :: 2 ) :: ( 3 :: 4 ) ) in u ; 1 end test ]]" \item "[[ etst let ( ( u :: v ) :: ( w :: x ) ) = ( ( 1 :: 2 ) :: ( 3 :: 4 ) ) in v ; 2 end test ]]" \item "[[ etst let ( ( u :: v ) :: ( w :: x ) ) = ( ( 1 :: 2 ) :: ( 3 :: 4 ) ) in w ; 3 end test ]]" \item "[[ etst let ( ( u :: v ) :: ( w :: x ) ) = ( ( 1 :: 2 ) :: ( 3 :: 4 ) ) in x ; 4 end test ]]" \item "[[ etst let << u ,, v ,, w >> = << 1 ,, 2 ,, 3 >> in << v ,, w ,, u >> ; << 2 ,, 3 ,, 1 >> end test ]]" \end{statements}" ]" \subsection{Backquote} "[ "\begin{statements} \item "[[ ttst make-pair ( 1 , quote 2 end quote , quote 3 end quote ) t= quote 2 :: 3 end quote end test ]]" \item "[[ ttst make-quote ( 1 , quote 2 end quote ) t= quote quote 2 end quote end quote end test ]]" \item "[[ ttst make-make-root ( 1 , quote 2 end quote , quote 3 end quote ) t= quote make-root ( 2 , 3 ) end quote end test ]]" \item "[[ ttst backquote2 ( ( true :: true :: 1 ) :: true , ( 2 :: 3 :: true ) :: true , ( 4 :: 5 :: true ) :: true , macrostate0 , self ) = ( ( quote true :: true end quote ref :: quote true :: true end quote idx :: 1 ) :: ( ( quote make-root ( true , true ) end quote ref :: quote make-root ( true , true ) end quote idx :: 1 ) :: ( ( 2 :: 3 :: true ) :: true ) :: ( ( quote quote true end quote end quote ref :: quote quote true end quote end quote idx :: 1 ) :: ( ( 4 :: 5 :: true ) :: true ) :: true ) :: true ) :: ( ( quote true end quote ref :: quote true end quote idx :: 1 ) :: true ) :: true ) end test ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \item "[[ ttst back quote 2 end quote quote 3 end quote t= quote 3 end quote end test ]]" \item "[[ ttst back quote 2 end quote quote quote 3 end quote unquote end quote t= quote 3 end quote end test ]]" \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 ]]" \item "[[ ttst back quote 2 end quote quote 3 + 4 end quote t= quote 3 + 4 end quote end test ]]" \item "[[ ttst back quote 2 end quote quote 3 + 4 end quote t= quote 3 + 4 end quote end test ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \end{statements}" ]" \section{Proof checking} \subsection{Term sets} "[ "\begin{statements} \item "[[ ttst quote 2 end quote member << quote 2 end quote ,, quote 3 end quote >> end test ]]" \item "[[ ttst quote 3 end quote member << quote 2 end quote ,, quote 3 end quote >> end test ]]" \item "[[ ftst quote 4 end quote member << quote 2 end quote ,, quote 3 end quote >> end test ]]" \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 ]]" \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 ]]" \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 ]]" \item "[[ ttst << quote 2 end quote ,, quote 3 end quote >> set- quote 2 end quote t=* << quote 3 end quote >> end test ]]" \item "[[ ttst << quote 2 end quote ,, quote 3 end quote >> set- quote 3 end quote t=* << quote 2 end quote >> end test ]]" \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 ]]" \item "[[ ttst << 1 ,, 2 ,, 3 >> union << 4 ,, 2 >> = << 3 ,, 1 ,, 4 ,, 2 >> end test ]]" \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 ]]" \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 ]]" \end{statements}" ]" \subsection{Meta variables} "[ "\begin{statements} \item "[[ ttst quote #a end quote metavar ( self ) end test ]]" \item "[[ ftst quote x end quote metavar ( self ) end test ]]" \end{statements}" ]" \subsection{Object terms} "[ "\begin{statements} \item "[[ ttst quote #a end quote objectterm ( self ) end test ]]" \item "[[ ftst quote #a infer #b end quote objectterm ( self ) end test ]]" \item "[[ ttst quote x end quote objectterm ( self ) end test ]]" \item "[[ ttst quote x _ { y infer z } end quote objectterm ( self ) end test ]]" \item "[[ ttst quote quote x infer y end quote end quote objectterm ( self ) end test ]]" \item "[[ ttst quote \ x . y end quote objectterm ( self ) end test ]]" \item "[[ ftst quote \ x . ( y infer z ) end quote objectterm ( self ) end test ]]" \item "[[ ftst quote \ ( x infer y ) . z end quote objectterm ( self ) end test ]]" \item "[[ ttst quote x + y end quote objectterm ( self ) end test ]]" \item "[[ ftst quote ( x infer y ) + z end quote objectterm ( self ) end test ]]" \item "[[ ftst quote 1 + ( x infer y ) end quote objectterm ( self ) end test ]]" \end{statements}" ]" \subsection{Meta terms} "[ "\begin{statements} \item "[[ ttst quote #a end quote metaterm ( self ) end test ]]" \item "[[ ttst quote #a infer #b end quote metaterm ( self ) end test ]]" \item "[[ ttst quote x end quote metaterm ( self ) end test ]]" \item "[[ ttst quote x _ { y infer z } end quote metaterm ( self ) end test ]]" \item "[[ ttst quote quote x infer y end quote end quote metaterm ( self ) end test ]]" \item "[[ ttst quote \ x . y end quote metaterm ( self ) end test ]]" \item "[[ ftst quote \ x . ( y infer z ) end quote metaterm ( self ) end test ]]" \item "[[ ftst quote \ ( x infer y ) . z end quote metaterm ( self ) end test ]]" \item "[[ ftst quote \ 2 . z end quote metaterm ( self ) end test ]]" \item "[[ ttst quote x + y end quote metaterm ( self ) end test ]]" \item "[[ ftst quote ( x infer y ) + z end quote metaterm ( self ) end test ]]" \item "[[ ftst quote 1 + ( x infer y ) end quote metaterm ( self ) end test ]]" \item "[[ ttst quote ( #a infer x ) infer ( 1 infer 2 ) end quote metaterm ( self ) end test ]]" \item "[[ ttst quote ( 1 + 2 + 3 ) infer ( 4 + 5 + 6 ) end quote metaterm ( self ) end test ]]" \item "[[ ftst quote ( ( 1 infer 2 ) + 3 ) infer ( 4 + 5 + 6 ) end quote metaterm ( self ) end test ]]" \item "[[ ftst quote ( 1 + ( 2 infer 3 ) ) infer ( 4 + 5 + 6 ) end quote metaterm ( self ) end test ]]" \item "[[ ftst quote ( 1 + 2 + 3 ) infer ( ( 4 infer 5 ) + 6 ) end quote metaterm ( self ) end test ]]" \item "[[ ftst quote ( 1 + 2 + 3 ) infer ( 4 + ( 5 infer 6 ) ) end quote metaterm ( self ) end test ]]" \item "[[ ttst quote All #a : #a infer #a end quote metaterm ( self ) end test ]]" \item "[[ ftst quote All ( 1 infer 2 ) + 3 : 4 end quote metaterm ( self ) end test ]]" \item "[[ ftst quote All 1 : ( 2 infer 3 ) + 4 end quote metaterm ( self ) end test ]]" \end{statements}" ]" \subsection{Avoidance} "[ "\begin{statements} \item "[[ ftst quote #a end quote metaavoid ( self ) quote #a end quote end test ]]" \item "[[ ttst quote #a end quote metaavoid ( self ) quote #b end quote end test ]]" \item "[[ ftst quote x end quote metaavoid ( self ) quote b end quote end test ]]" \item "[[ ftst quote #a end quote metaavoid ( self ) quote #a infer #a end quote end test ]]" \item "[[ ftst quote #a end quote metaavoid ( self ) quote #b infer #a end quote end test ]]" \item "[[ ftst quote #a end quote metaavoid ( self ) quote #a infer #c end quote end test ]]" \item "[[ ttst quote #a end quote metaavoid ( self ) quote #b infer #c end quote end test ]]" \item "[[ ttst quote #a end quote metaavoid ( self ) quote All #a : #a end quote end test ]]" \item "[[ ttst quote #a end quote metaavoid ( self ) quote All #a : #b end quote end test ]]" \item "[[ ftst quote #a end quote metaavoid ( self ) quote All #b : #a end quote end test ]]" \item "[[ ttst quote #a end quote metaavoid ( self ) quote All #b : #b end quote end test ]]" \item "[[ ftst quote #a end quote metaavoid ( self ) quote #a + #a end quote end test ]]" \item "[[ ftst quote #a end quote metaavoid ( self ) quote #b + #a end quote end test ]]" \item "[[ ftst quote #a end quote metaavoid ( self ) quote #a + #c end quote end test ]]" \item "[[ ttst quote #a end quote metaavoid ( self ) quote #b + #c end quote end test ]]" \item "[[ ftst quote #a end quote metaavoid ( self ) quote \ #a . #a end quote end test ]]" \item "[[ ftst quote #a end quote metaavoid ( self ) quote \ #b . #a end quote end test ]]" \item "[[ ftst quote #a end quote metaavoid ( self ) quote \ #a . #c end quote end test ]]" \item "[[ ttst quote #a end quote metaavoid ( self ) quote \ #b . #c end quote end test ]]" \item "[[ ttst quote #a end quote metaavoid ( self ) quote quote #a end quote end quote end test ]]" \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 ]]" \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 ]]" \item "[[ ttst quote #a end quote metaavoid* ( self ) << quote #b + #c end quote ,, quote #d + #e end quote >> end test ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \item "[[ ttst distinctvar ( <<>> , self ) end test ]]" \item "[[ ttst distinctvar ( << quote x end quote >> , self ) end test ]]" \item "[[ ttst distinctvar ( << quote x end quote ,, quote y end quote >> , self ) end test ]]" \item "[[ ttst distinctvar ( << quote x end quote ,, quote y end quote ,, quote z end quote >> , self ) end test ]]" \item "[[ ftst distinctvar ( << quote x end quote ,, quote #y end quote ,, quote z end quote >> , self ) end test ]]" \item "[[ ftst distinctvar ( << quote x end quote ,, quote y end quote ,, quote x end quote >> , self ) end test ]]" \item "[[ ftst distinctvar ( << quote x end quote ,, quote y end quote ,, quote y end quote >> , self ) end test ]]" \item "[[ ftst quote x end quote objectavoid ( self ) quote x end quote end test ]]" \item "[[ ttst quote x end quote objectavoid ( self ) quote y end quote end test ]]" \item "[[ ftst quote x end quote objectavoid ( self ) quote x + x end quote end test ]]" \item "[[ ftst quote x end quote objectavoid ( self ) quote y + x end quote end test ]]" \item "[[ ftst quote x end quote objectavoid ( self ) quote x + z end quote end test ]]" \item "[[ ttst quote x end quote objectavoid ( self ) quote y + z end quote end test ]]" \item "[[ ttst quote x end quote objectavoid ( self ) quote \ x . x end quote end test ]]" \item "[[ ftst quote x end quote objectavoid ( self ) quote \ y . x end quote end test ]]" \item "[[ ttst quote x end quote objectavoid ( self ) quote \ x . y end quote end test ]]" \item "[[ ttst quote x end quote objectavoid ( self ) quote \ y . y end quote end test ]]" \item "[[ ttst quote x end quote objectavoid ( self ) quote quote x end quote end quote end test ]]" \item "[[ ttst quote x end quote objectavoid ( self ) quote #a end quote set= << quote #a end quote >> end test ]]" \item "[[ ttst quote x end quote objectavoid ( self ) quote #a + #b end quote set= << quote #a end quote ,, quote #b end quote >> end test ]]" \item "[[ ttst quote x end quote objectavoid ( self ) quote \ x . #a end quote set= <<>> end test ]]" \item "[[ ttst quote x end quote objectavoid ( self ) quote \ y . #a end quote set= << quote #a end quote >> end test ]]" \item "[[ ttst quote x end quote objectavoid ( self ) quote quote #a end quote end quote set= <<>> end test ]]" \item "[[ ftst quote x end quote objectavoid ( self ) quote \ #a . x end quote end test ]]". \item "[[ ftst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote x end quote end test ]]". \item "[[ ftst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote y end quote end test ]]". \item "[[ ttst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote z end quote end test ]]". \item "[[ ftst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote x + y end quote end test ]]". \item "[[ ftst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote \ x . x + y end quote end test ]]". \item "[[ ftst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote \ y . x + y end quote end test ]]". \item "[[ ttst << quote x end quote ,, quote y end quote >> objectavoid* ( self ) quote \ x . \ y . x + y end quote end test ]]". \item "[[ ttst << quote x end quote ,, quote v end quote >> objectavoid* ( self ) quote y end quote end test ]]". \end{statements}" ]" \subsection{Sequent equality} "[ "\begin{statements} \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 ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \end{statements}" ]" \subsection{Substitution freeness} "[ "\begin{statements} \item "[[ ttst metafree ( quote #a end quote , quote #a end quote , quote #a end quote , self ) end test ]]" \item "[[ ttst metafree ( quote #a infer #b end quote , quote #a end quote , quote All #c : ( #c infer #b ) end quote , self ) end test ]]" \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 ]]" \item "[[ ftst metafree ( quote All #b : #a end quote , quote #a end quote , quote All #c : ( #c infer #b ) end quote , self ) end test ]]" \item "[[ ttst metafree ( quote All #b : #b end quote , quote #a end quote , quote All #c : ( #c infer #b ) end quote , self ) end test ]]" \item "[[ ttst metafree ( quote All #c : #a end quote , quote #a end quote , quote All #c : ( #c infer #b ) end quote , self ) end test ]]" \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 ]]" \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 ]]" \item "[[ ttst metafree ( quote #a + #b end quote , quote #a end quote , quote x + y end quote , self ) end test ]]" \item "[[ ftst metafree ( quote #a + #b end quote , quote #a end quote , quote x infer y end quote , self ) end test ]]" \item "[[ ttst metafree ( quote #c + #b end quote , quote #a end quote , quote x infer y end quote , self ) end test ]]" \item "[[ ttst objectfree ( quote a end quote , quote a end quote , quote a end quote , self ) end test ]]" \item "[[ ttst objectfree ( quote a + b end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" \item "[[ ttst objectfree ( quote \ a . ( a + b ) end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" \item "[[ ftst objectfree ( quote \ b . a end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" \item "[[ ttst objectfree ( quote \ b . b end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" \item "[[ ttst objectfree ( quote \ c . a end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" \item "[[ ttst objectfree ( quote \ c . \ d . a end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" \item "[[ ftst objectfree ( quote \ c . \ b . a end quote , quote a end quote , quote \ c . c + b end quote , self ) end test ]]" \end{statements}" ]" \subsection{Substitution} "[ "\begin{statements} \item "[[ ttst metasubst ( quote #a end quote , << quote #a end quote :: quote #b end quote >> , self ) t= quote #b end quote end test ]]" \item "[[ ttst metasubst ( quote #a end quote , << quote #c end quote :: quote #b end quote >> , self ) t= quote #a end quote end test ]]" \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 ]]" \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 ]]" \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 ]]" \end{statements}" ]" \subsection{Sequent operators} "[ "\begin{statements} \item "[[ ttst eval-Init ( quote 1 end quote , self ) sequent= << << quote 1 end quote >> ,, <<>> ,, quote 1 end quote >> end test ]]" \item "[[ ttst eval-Init ( quote 1 + #a end quote , self ) sequent= << << quote 1 + #a end quote >> ,, <<>> ,, quote 1 + #a end quote >> end test ]]" \item "[[ ttst eval-Init ( quote 1 + ( #a infer #a ) end quote , self ) catch head end test ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \item "[[ ttst eval-Verify ( << <<>> ,, <<>> ,, quote \ c . 2 + 2 = 5 endorse 5 end quote >> , quote true end quote , self ) catch head end test ]]" \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 ]]" \item "[[ ttst eval-Curry ( << <<>> ,, <<>> ,, quote ( 1 infer 2 ) infer 3 end quote >> , quote true end quote , self ) catch head end test ]]" \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 ]]" \item "[[ ttst eval-Uncurry ( << <<>> ,, <<>> ,, quote 1 infer 2 endorse 3 end quote >> , quote true end quote , self ) catch head end test ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \item "[[ ttst eval-at ( quote ( #a infer #b ) Init at #c end quote , true , self ) catch head end test ]]" \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 ]]" \item "[[ ttst eval-at ( quote ( All #a : All #b : ( #a infer #b ) ) Init at #b end quote , true , self ) catch head end test ]]" \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 ]]" \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 ]]" \item "[[ ttst eval-Deref ( << <<>> ,, <<>> ,, quote true end quote >> , quote true end quote , self ) catch head end test ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \end{statements}" ]" \subsection{Verification} "[ "\begin{statements} \item "[[ ttst claiming ( quote 1 end quote , quote 1 &c 2 end quote ) end test ]]" \item "[[ ttst claiming ( quote 1 end quote , quote 2 &c 1 end quote ) end test ]]" \item "[[ ftst claiming ( quote 1 end quote , quote 2 &c 3 end quote ) end test ]]" \end{statements}" ]" \subsection{Conversions from values to terms} "[ "\begin{statements} \item "[[ etst int2string ( true , 0 ) ; << 0 :: "0" :: true >> end test ]]" \item "[[ etst int2string ( true , 1 ) ; << 0 :: "1" :: true >> end test ]]" \item "[[ etst int2string ( true , 2 ) ; << 0 :: "2" :: true >> end test ]]" \item "[[ etst int2string ( true , 5 ) ; << 0 :: "5" :: true >> end test ]]" \item "[[ etst int2string ( true , 10 ) ; << 0 :: "10" :: true >> end test ]]" \item "[[ etst int2string ( true , 123 ) ; << 0 :: "123" :: true >> end test ]]" \item "[[ etst int2string ( true , -1 ) ; << 0 :: "-1" :: true >> end test ]]" \item "[[ etst int2string ( true , -2 ) ; << 0 :: "-2" :: true >> end test ]]" \item "[[ etst int2string ( true , -5 ) ; << 0 :: "-5" :: true >> end test ]]" \item "[[ etst int2string ( true , -10 ) ; << 0 :: "-10" :: true >> end test ]]" \item "[[ etst int2string ( true , -123 ) ; << 0 :: "-123" :: true >> end test ]]" \item "[[ ttst val2term ( true , true ) t= quote true end quote end test ]]" \item "[[ ttst val2term ( true , false ) t= quote false end quote end test ]]" \item "[[ ttst val2term ( true , true :: false ) t= quote true :: false end quote end test ]]" \item "[[ ttst val2term ( true , map ( x ) ) t= quote map ( *** ) end quote end test ]]" \item "[[ ttst val2term ( true , 0 ) t= quote 0 end quote end test ]]" \item "[[ ttst val2term ( true , 1 ) t= quote %% %1 end quote end test ]]" \item "[[ ttst val2term ( true , 2 ) t= quote %% %1 %0 end quote end test ]]" \item "[[ ttst val2term ( true , - 1 ) t= quote - %% %1 end quote end test ]]" \item "[[ ttst val2term ( true , - 2 ) t= quote - %% %1 %0 end quote end test ]]" \item "[[ ttst val2term ( true , object ( ( 1 :: 2 ) :: 3 ) ) t= quote object ( ( %% %1 :: %% %1 %0 ) :: %% %1 %1 ) end quote end test ]]" \end{statements}" ]" \subsection{Unification} "[ "\begin{statements} \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 ]]" \item "[[ ftst unify ( quote 2 end quote , quote 2 end quote , true ) catch head end test ]]" \item "[[ ttst unify ( quote 2 end quote , quote 3 end quote , true ) catch head end test ]]" \item "[[ ftst unify ( quote 2 + 3 end quote , quote 2 + 3 end quote , true ) catch head end test ]]" \item "[[ ttst unify ( quote 2 + 3 end quote , quote 2 * 3 end quote , true ) catch head end test ]]" \item "[[ ttst unify ( quote 2 + 3 end quote , quote 3 + 3 end quote , true ) catch head end test ]]" \item "[[ ttst unify ( quote 2 + 3 end quote , quote 2 + 2 end quote , true ) catch head end test ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \end{statements}" ]" \subsection{Testing of rack functions} \begin{statements} \item "[[ etst sl2rack ( bt2vector* ( 3 ) ) ; true end test ]]" \item "[[ etst sl2rack ( bt2vector* ( 1 :: 1 :: 4 ) ) ; true :: true end test ]]" \item "[[ etst sl2rack ( bt2vector* ( 0 :: 7 :: 4 ) ) ; 7 end test ]]" \item "[[ etst sl2rack ( bt2vector* ( 2 :: 3 :: 7 :: 8 :: 9 :: 4 ) ) ; bt2vector ( 7 :: 8 :: 9 ) end test ]]" \item "[[ etst sl2rack ( bt2vector* ( 0 :: 6 :: 2 :: 3 :: 7 :: 8 :: 9 :: 3 :: 4 :: 6 ) ) ; 6 :: bt2vector ( 7 :: 8 :: 9 ) end test ]]" \item "[[ etst sl2rack ( bt2vector* ( 0 :: 6 :: 2 :: 3 :: 7 :: 8 :: 9 :: 3 :: 4 :: 6 :: 0 ) ) ; 6 :: bt2vector ( 7 :: 8 :: 9 ) end test ]]" \item "[[ etst sl2rack ( append ( bt2vector* ( 0 :: 6 :: 2 :: 3 :: 7 :: 8 :: 9 :: 3 :: 4 :: 6 ) , << false >> ) ) ; 6 :: bt2vector ( 7 :: 8 :: 9 ) end test ]]" \item "[[ etst sl2rack ( append ( bt2vector* ( 0 :: 6 :: 2 :: 3 :: 7 :: 8 :: 9 :: 3 :: 4 ) , << false >> ) ) ; exception end test ]]" \item "[[ etst sl2rack ( bt2vector* ( 0 :: 6 :: 2 :: 3 :: 7 :: 8 :: 9 :: 3 :: 4 ) ) ; exception end test ]]" \item "[[ etst bt2vector* ( << 3 >> ) ; rack2sl ( true ) end test ]]" \item "[[ etst bt2vector* ( << 1 ,, 1 ,, 4 >> ) ; rack2sl ( true :: true ) end test ]]" \item "[[ etst bt2vector* ( << 0 ,, 7 ,, 4 >> ) ; rack2sl ( 7 ) end test ]]" \item "[[ etst bt2vector* ( << 2 ,, 3 ,, 7 ,, 8 ,, 9 ,, 4 >> ) ; rack2sl ( bt2vector ( 7 :: 8 :: 9 ) ) end test ]]" \item "[[ etst bt2vector* ( << 0 ,, 6 ,, 2 ,, 3 ,, 7 ,, 8 ,, 9 ,, 3 ,, 4 ,, 6 >> ) ; rack2sl ( 6 :: bt2vector ( 7 :: 8 :: 9 ) ) end test ]]" \item "[[ etst bt2vector* ( << 0 ,, 7 ,, 3 ,, 3 ,, 5 >> ) ; rack2sl ( 7 :: 7 ) end test ]]" \item "[[ etst bt2vector* ( << 1 ,, 1 ,, 3 ,, 3 ,, 5 >> ) ; rack2sl ( ( true :: true ) :: ( true :: true ) ) end test ]]" \item "[[ etst exception ; rack2sl ( ( true :: true ) :: ( true :: - 1 ) ) end test ]]" \item "[[ etst exception ; rack2sl ( ( true :: true ) :: ( true :: false ) ) end test ]]" \end{statements} \subsection{Test of Ripemd} \begin{statements} \item "[[ etst !"9C1185A5C5E9FC54612808977EE8F548B2258D31" ; ripemds ( !"". ) end test ]]" \item "[[ etst !"0BDC9D2D256B3EE9DAAE347BE6F4DC835A467FFE" ; ripemds ( !"a" ) end test ]]" \item "[[ etst !"8EB208F7E05D987A9B044A8E98C6B087F15A0BFC" ; ripemds ( !"abc" ) end test ]]" \item "[[ etst !"8EB208F7E05D987A9B044A8E98C6B087F15A0BFC" ; ripemds ( << !"a" ,, !"bc" >> ) end test ]]" \item "[[ etst !"5D0689EF49D2FAE572B881B123A85FFA21595F36" ; ripemds ( !"message digest" ) end test ]]" \item "[[ etst !"F71C27109C692C1B56BBDCEB5B9D2865B3708DBC" ; ripemds ( !"abcdefghijklmnopqrstuvwxyz" ) end test ]]" \item "[[ etst !"12A053384A9C0C88E405A06C27DCF49ADA62EB2B" ; ripemds ( !"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq" ) end test ]]" \item "[[ etst !"B0E20B6E3116640286ED3A87A5713079B21F5189" ; ripemds ( !"ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789" ) end test ]]" \item "[[ etst !"9B752E45573D4B39F4DBD3323CAB82BF63326BFB" ; ripemds ( repeat ( 8 , !"1234567890" ) ) end test ]]" \end{statements} \subsection{Compilation} "[ "\begin{statements} \item "[[ define value of compiled-base as norm compile ( base ) end define ]]" \item "[[ define value of compiled-test as norm compile ( test ) end define ]]" \item "[[ define value of get-base0 ( x ) as base [[ x ref ]] [[ "code" ]] [[ x idx ]] end define ]]" \item "[[ define value of get-base1 ( x ) as compiled-base [[ x ref ]] [[ "code" ]] [[ x idx ]] end define ]]" \item "[[ define value of get-test0 ( x ) as test [[ x ref ]] [[ "code" ]] [[ x idx ]] end define ]]" \item "[[ define value of get-test1 ( x ) as compiled-test [[ x ref ]] [[ "code" ]] [[ x idx ]] end define ]]" \item "[[ ftst notnot test [[ test [[ 0 ]] ]] [[ "expansion" ]] end test ]]" \item "[[ ftst notnot compile ( test ) [[ test [[ 0 ]] ]] [[ "expansion" ]] end test ]]" \item "[[ ftst notnot ( norm compile ( test ) ) [[ test [[ 0 ]] ]] [[ "expansion" ]] end test ]]" \item "[[ ftst notnot compiled-test [[ test [[ 0 ]] ]] [[ "expansion" ]] end test ]]" \item "[[ etst get-base0 ( quote \ x . y end quote ) ; 0 end test ]]" \item "[[ etst get-base1 ( quote \ x . y end quote ) ; 0 end test ]]" \item "[[ etst get-base0 ( quote quote x end quote end quote ) ; 1 end test ]]" \item "[[ etst get-base1 ( quote quote x end quote end quote ) ; 1 end test ]]" \item "[[ etst get-base0 ( quote true end quote ) ; map ( true ) end test ]]" \item "[[ etst get-base1 ( quote true end quote ) ; map ( true ) end test ]]" \item "[[ etst get-base0 ( quote x ' y end quote ) ; map ( true ) end test ]]" \item "[[ etst get-base1 ( quote x ' y end quote ) ; map ( true ) end test ]]" \item "[[ etst get-base0 ( quote If x then y else z end quote ) ; map ( true ) end test ]]" \item "[[ etst get-base1 ( quote If x then y else z end quote ) ; map ( true ) end test ]]" \item "[[ etst get-base0 ( quote true end quote ) Tail ; true end test ]]" \item "[[ etst get-base1 ( quote true end quote ) Tail ; true end test ]]" \item "[[ etst get-base0 ( quote x ' y end quote ) Tail ' ( \ x . x ) ' 2 ; 2 end test ]]" \item "[[ etst get-base1 ( quote x ' y end quote ) Tail ' ( \ x . x ) ' 2 ; 2 end test ]]" \item "[[ etst get-base0 ( quote x ' y end quote ) Tail ' ( \ x . 3 ) ' 2 ; 3 end test ]]" \item "[[ etst get-base1 ( quote x ' y end quote ) Tail ' ( \ x . 3 ) ' 2 ; 3 end test ]]" \item "[[ etst get-base0 ( quote If x then y else z end quote ) Tail ' true ' 1 ' 2 ; 1 end test ]]" \item "[[ etst get-base1 ( quote If x then y else z end quote ) Tail ' true ' 1 ' 2 ; 1 end test ]]" \item "[[ etst get-base0 ( quote If x then y else z end quote ) Tail ' false ' 1 ' 2 ; 2 end test ]]" \item "[[ etst get-base1 ( quote If x then y else z end quote ) Tail ' false ' 1 ' 2 ; 2 end test ]]" \item "[[ ttst make-constant ( quote 123 end quote ) Tail ' ( 2 LazyPair 3 ) t= quote 123 end quote end test ]]" \item "[[ ttst make-lambda ( make-constant ( quote 123 end quote ) ) Tail ' true ' 4 t= quote 123 end quote end test ]]" \item "[[ define value of compile-test00 as quote 123 end quote end define ]]" \item "[[ ttst get-test0 ( quote compile-test00 end quote ) Tail t= quote 123 end quote end test ]]" \item "[[ ttst get-test1 ( quote compile-test00 end quote ) Tail t= quote 123 end quote end test ]]" \item "[[ define value of compile-test01 ( x ) as quote 123 end quote end define ]]" \item "[[ ttst get-test0 ( quote compile-test01 ( x ) end quote ) Tail ' 9 t= quote 123 end quote end test ]]" \item "[[ ttst get-test1 ( quote compile-test01 ( x ) end quote ) Tail ' 9 t= quote 123 end quote end test ]]" \item "[[ define value of compile-test02 ( x ) as x end define ]]" \item "[[ etst get-test0 ( quote compile-test02 ( x ) end quote ) Tail ' 9 ; 9 end test ]]" \item "[[ etst get-test1 ( quote compile-test02 ( x ) end quote ) Tail ' 9 ; 9 end test ]]" \item "[[ define value of compile-test03 ( x , y ) as x end define ]]" \item "[[ etst get-test0 ( quote compile-test03 ( x , y ) end quote ) Tail ' 8 ' 9 ; 8 end test ]]" \item "[[ etst get-test1 ( quote compile-test03 ( x , y ) end quote ) Tail ' 8 ' 9 ; 8 end test ]]" \item "[[ define value of compile-test04 ( x , y ) as y end define ]]" \item "[[ etst get-test0 ( quote compile-test04 ( x , y ) end quote ) Tail ' 8 ' 9 ; 9 end test ]]" \item "[[ etst get-test1 ( quote compile-test04 ( x , y ) end quote ) Tail ' 8 ' 9 ; 9 end test ]]" \item "[[ define value of compile-test05 ( x , y ) as z end define ]]" \item "[[ etst get-test0 ( quote compile-test05 ( x , y ) end quote ) Tail ' 8 ' 9 ; true end test ]]" \item "[[ etst get-test1 ( quote compile-test05 ( x , y ) end quote ) Tail ' 8 ' 9 ; true end test ]]" \item "[[ define value of compile-test06 ( x , x ) as x end define ]]" \item "[[ etst get-test0 ( quote compile-test06 ( x , y ) end quote ) Tail ' 8 ' 9 ; 8 end test ]]" \item "[[ etst get-test1 ( quote compile-test06 ( x , y ) end quote ) Tail ' 8 ' 9 ; 8 end test ]]" \item "[[ define value of compile-test07 as "abc" end define ]]" \item "[[ etst get-test0 ( quote compile-test07 end quote ) Tail ; "abc" end test ]]" \item "[[ etst get-test1 ( quote compile-test07 end quote ) Tail ; "abc" end test ]]" \item "[[ define value of compile-test08 as test end define ]]" \item "[[ etst get-test0 ( quote compile-test08 end quote ) Tail [[ 0 ]] ; quote test end quote ref end test ]]" \item "[[ etst get-test1 ( quote compile-test08 end quote ) Tail [[ 0 ]] ; quote test end quote ref end test ]]" \item "[[ define value of compile-test09 as base end define ]]" \item "[[ etst get-test0 ( quote compile-test09 end quote ) Tail [[ 0 ]] ; quote base end quote ref end test ]]" \item "[[ etst get-test1 ( quote compile-test09 end quote ) Tail [[ 0 ]] ; quote base end quote ref end test ]]" \item "[[ define value of compile-test10 ( u , v ) as \ x . \ y . u end define ]]" \item "[[ etst get-test0 ( quote compile-test10 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 1 end test ]]" \item "[[ etst get-test1 ( quote compile-test10 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 1 end test ]]" \item "[[ define value of compile-test11 ( u , v ) as \ x . \ y . v end define ]]" \item "[[ etst get-test0 ( quote compile-test11 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 2 end test ]]" \item "[[ etst get-test1 ( quote compile-test11 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 2 end test ]]" \item "[[ define value of compile-test12 ( u , v ) as \ x . \ y . x end define ]]" \item "[[ etst get-test0 ( quote compile-test12 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 3 end test ]]" \item "[[ etst get-test1 ( quote compile-test12 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 3 end test ]]" \item "[[ define value of compile-test13 ( u , v ) as \ x . \ y . y end define ]]" \item "[[ etst get-test0 ( quote compile-test13 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 4 end test ]]" \item "[[ etst get-test1 ( quote compile-test13 ( x , y ) end quote ) Tail ' 1 ' 2 ' 3 ' 4 ; 4 end test ]]" \item "[[ define value of compile-test14 as Base end define ]]" \item "[[ etst get-test0 ( quote compile-test14 end quote ) Tail ; 10 end test ]]" \item "[[ etst get-test1 ( quote compile-test14 end quote ) Tail ; 10 end test ]]" \item "[[ define value of compile-test15 ( Base , x ) as Base end define ]]" \item "[[ etst get-test0 ( quote compile-test15 ( x , y ) end quote ) Tail ' 1 ' 2 ; 10 end test ]]" \item "[[ etst get-test1 ( quote compile-test15 ( x , y ) end quote ) Tail ' 1 ' 2 ; 10 end test ]]" \item "[[ define value of compile-test16 ( Base , x ) as x end define ]]" \item "[[ etst get-test0 ( quote compile-test16 ( x , y ) end quote ) Tail ' 1 ' 2 ; 2 end test ]]" \item "[[ etst get-test1 ( quote compile-test16 ( x , y ) end quote ) Tail ' 1 ' 2 ; 2 end test ]]" \item "[[ define value of compile-test17 as 123 end define ]]" \item "[[ etst get-test0 ( quote compile-test17 end quote ) Tail ; 123 end test ]]" \item "[[ etst get-test1 ( quote compile-test17 end quote ) Tail ; 123 end test ]]" \item "[[ define value of compile-test18 as 123 - 23 end define ]]" \item "[[ etst get-test0 ( quote compile-test18 end quote ) Tail ; 100 end test ]]" \item "[[ etst get-test1 ( quote compile-test18 end quote ) Tail ; 100 end test ]]" \item "[[ define value of compile-test19 ( x , y ) as if x then y else compile-test19 ( x tail , x head :: y ) end define ]]" \item "[[ etst << 3 ,, 4 >> ; ( get-test0 ( quote compile-test19 ( x , y ) end quote ) apply true maptag apply << 3 ,, 4 >> maptag ) untag end test ]]" \item "[[ etst << 3 ,, 4 >> ; ( get-test1 ( quote compile-test19 ( x , y ) end quote ) apply true maptag apply << 3 ,, 4 >> maptag ) untag end test ]]" \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 ]]" \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 ]]" \item "[[ etst true ; ( get-base0 ( quote true end quote ) ) Tail end test ]]" \item "[[ etst true ; ( get-base1 ( quote true end quote ) ) Tail end test ]]" \item "[[ etst false ; ( get-base0 ( quote false end quote ) ) Tail end test ]]" \item "[[ etst false ; ( get-base1 ( quote false end quote ) ) Tail end test ]]" \item "[[ ttst 2 LazyPair 3 Equal get-base0 ( quote x LazyPair y end quote ) Tail ' 2 ' 3 end test ]]" \item "[[ ttst 2 LazyPair 3 Equal get-base1 ( quote x LazyPair y end quote ) Tail ' 2 ' 3 end test ]]" \item "[[ ftst 3 LazyPair 2 Equal get-base0 ( quote x LazyPair y end quote ) Tail ' 2 ' 3 Tail end test ]]" \item "[[ ftst 3 LazyPair 2 Equal get-base1 ( quote x LazyPair y end quote ) Tail ' 2 ' 3 Tail end test ]]" \item "[[ ttst 2 LazyPair 3 Equal get-base0 ( quote x Pair y end quote ) Tail ' 2 ' 3 end test ]]" \item "[[ ttst 2 LazyPair 3 Equal get-base1 ( quote x Pair y end quote ) Tail ' 2 ' 3 end test ]]" \item "[[ ttst get-base0 ( quote x Equal y end quote ) Tail ' 2 ' 2 end test ]]" \item "[[ ttst get-base1 ( quote x Equal y end quote ) Tail ' 2 ' 2 end test ]]" \item "[[ ftst get-base0 ( quote x Equal y end quote ) Tail ' 2 ' 3 maptag end test ]]" \item "[[ ftst get-base1 ( quote x Equal y end quote ) Tail ' 2 ' 3 maptag end test ]]" \item "[[ ttst 10 LazyPair true Equal get-base0 ( quote x Pair y end quote ) Tail ' 10 ' true end test ]]" \item "[[ ttst 10 LazyPair true Equal get-base1 ( quote x Pair y end quote ) Tail ' 10 ' true end test ]]" \item "[[ ttst 10 LazyPair false Equal get-base0 ( quote x Pair y end quote ) Tail ' 10 ' false end test ]]" \item "[[ ttst 10 LazyPair false Equal get-base1 ( quote x Pair y end quote ) Tail ' 10 ' false end test ]]" \item "[[ ttst true LazyPair true Equal get-base0 ( quote x Pair y end quote ) Tail ' true ' true end test ]]" \item "[[ ttst true LazyPair true Equal get-base1 ( quote x Pair y end quote ) Tail ' true ' true end test ]]" \item "[[ ttst true LazyPair 10 Equal get-base0 ( quote x Pair y end quote ) Tail ' true ' 10 end test ]]" \item "[[ ttst true LazyPair 10 Equal get-base1 ( quote x Pair y end quote ) Tail ' true ' 10 end test ]]" \item "[[ ttst false LazyPair 10 Equal get-base0 ( quote x Pair y end quote ) Tail ' false ' 10 end test ]]" \item "[[ ttst false LazyPair 10 Equal get-base1 ( quote x Pair y end quote ) Tail ' false ' 10 end test ]]" \item "[[ ttst true LazyPair false Equal get-base0 ( quote x Pair y end quote ) Tail ' true ' false end test ]]" \item "[[ ttst true LazyPair false Equal get-base1 ( quote x Pair y end quote ) Tail ' true ' false end test ]]" \item "[[ ttst false LazyPair true Equal get-base0 ( quote x Pair y end quote ) Tail ' false ' true end test ]]" \item "[[ ttst false LazyPair true Equal get-base1 ( quote x Pair y end quote ) Tail ' false ' true end test ]]" \item "[[ ttst Zero Equal ( get-base0 ( quote Zero end quote ) ) Tail end test ]]" \item "[[ ttst Zero Equal ( get-base1 ( quote Zero end quote ) ) Tail end test ]]" \item "[[ ttst One Equal ( get-base0 ( quote x Pair y end quote ) apply map ( false ) apply map ( Zero ) ) Tail end test ]]" \item "[[ ttst One Equal ( get-base1 ( quote x Pair y end quote ) apply map ( false ) apply map ( Zero ) ) Tail end test ]]" \item "[[ ttst One Equal ( get-base0 ( quote One end quote ) ) Tail end test ]]" \item "[[ ttst One Equal ( get-base1 ( quote One end quote ) ) Tail end test ]]" \item "[[ ttst Two Equal ( get-base0 ( quote Two end quote ) ) Tail end test ]]" \item "[[ ttst Two Equal ( get-base1 ( quote Two end quote ) ) Tail end test ]]" \item "[[ ttst Five Equal ( get-base0 ( quote x Plus y end quote ) apply map ( Three ) apply map ( Two ) ) Tail end test ]]" \item "[[ ttst Five Equal ( get-base1 ( quote x Plus y end quote ) apply map ( Three ) apply map ( Two ) ) Tail end test ]]" \item "[[ etst 10 ; ( get-base0 ( quote Base end quote ) ) untag end test ]]" \item "[[ etst 10 ; ( get-base1 ( quote Base end quote ) ) untag end test ]]" \item "[[ etst << 1 ,, 2 ,, 3 >> ; ( get-base0 ( quote revappend ( x , y ) end quote ) apply << 1 >> maptag apply << 2 ,, 3 >> maptag ) untag end test ]]" \item "[[ etst << 1 ,, 2 ,, 3 >> ; ( get-base1 ( quote revappend ( x , y ) end quote ) apply << 1 >> maptag apply << 2 ,, 3 >> maptag ) untag end test ]]" \item "[[ ttst prune ( quote 1 + 2 end quote , test ) t= quote 1 + 2 end quote end test ]]" \item "[[ ttst prune ( quote 1 + 2 end quote , base ) t= quote 1 + 2 end quote end test ]]" \item "[[ ttst prune ( quote 1 + compile-test00 end quote , test ) t= quote 1 + compile-test00 end quote end test ]]" \item "[[ ttst prune ( quote 1 + compile-test00 end quote , base ) t= quote 1 + base end quote end test ]]" \item "[[ ttst prune ( quote compile-test03 ( 1 , 2 ) end quote , test ) t= quote compile-test03 ( 1 , 2 ) end quote end test ]]" \item "[[ ttst prune ( quote compile-test03 ( 1 , 2 ) end quote , base ) t= quote base end quote end test ]]" \item "[[ etst compiled-base [[ base [[ 0 ]] ]] [[ "diagnose" ]] ; true maptag end test ]]" \item "[[ ttst compile ( test [[ << test [[ 0 ]] ,, "expansion" >> => quote test end quote ]] ) [[ test [[ 0 ]] ]] [[ "diagnose" ]] = true maptag end test ]]" \item "[[ ttst compile ( test [[ << test [[ 0 ]] ,, "expansion" >> => quote test end quote ]] ) [[ test [[ 0 ]] ]] [[ "diagnose" ]] untag = true end test ]]" \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 ]]" \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 ]]" \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 ]]" \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 ]]" \item "[[ define value of test as 2 + 3 end define ]]" \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 ]]" \item "[[ etst get-test0 ( quote test end quote ) Tail ; 5 end test ]]" \item "[[ etst get-test1 ( quote test end quote ) Tail ; 5 end test ]]" \end{statements}" ]" \end{document} " end text ,, latex ( "page" ) ,, latex ( "page" ) ,, dvipdfm ( "page" ) ,, text "chores.tex" : ""-""; \documentclass[fleqn]{article} % Mark overfull lines \setlength{\overfullrule}{1mm} % Include definitions generated by lgc \input{lgwinclude} % Make latexsym characters available \usepackage{latexsym} % Ensure reasonable rendering of strings \everymath{\rm} \everydisplay{\rm} % Enable generation of an index \usepackage{makeidx} \makeindex \newcommand{\intro}[1]{\emph{#1}} \newcommand{\indexintro}[1]{\index{#1}\intro{#1}} % Enable generation of a bibliography \bibliographystyle{plain} % Enable hyperlinks \usepackage[dvipdfm=true]{hyperref} \hypersetup{pdfpagemode=none} \hypersetup{pdfstartpage=1} \hypersetup{pdfstartview=FitBH} \hypersetup{pdfpagescrop={120 80 490 730}} \hypersetup{pdftitle=A Logiweb test page - chores} \hypersetup{colorlinks=true} % Construct for listing statements with associated explanations \newenvironment{statements}{\begin{list}{}{ \setlength{\leftmargin}{5em} \setlength{\itemindent}{-5em}}}{\end{list}} \begin{document} \title{A Logiweb test page - chores} \author{Klaus Grue} \maketitle \tableofcontents \section{\TeX\ definitions} \section{Name definitions} "[[ protect ""N end protect ]]" \section{Charge definitions} "[[ protect ""C end protect ]]" \end{document}%\item $ttst0\linebreak [0]\ " end text ,, latex ( "chores" ) ,, latex ( "chores" ) ,, dvipdfm ( "chores" )