"";;01AB1F51C8C17606A5C0331B5689B4858C796547B9A0A4AEF0BCB2BB0806
""{ Logiweb, a system for electronic distribution of mathematics
    Copyright (C) 2004-2009 Klaus Grue

    This program is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    This program is distributed IN the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program; if not, write to the Free Software
    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  021111307  USA

    Contact: Klaus Grue, DIKU, Universitetsparken 1, DK2100 Copenhagen,
    Denmark, grue@diku.dk, http://logiweb.eu/, http://www.diku.dk/~grue/

    Logiweb is a system for distribution of mathematical definitions,
    lemmas, and proofs. For more on Logiweb, consult http://logiweb.eu/.
""}

""P base


""D 0
proclaim " as " end proclaim
lgcend
lgcvar
lgcdef " of " as " enddef
lgcname
lgccharge
empty
preassociative " greater than "
postassociative " greater than "
priority " equal "
priority " end priority
asterisk
name
Define " of " as " end define
math " end math
display math " end math
ensure math " end math
make math " end math
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
x
y
z
v
w
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
true
quote " end quote
optimized define " of " as " end define
tex use
tex show
priority
value
macro
render
claim
message
unpack
execute
exampleaspect0
exampleaspect1
exampleaspect2
show " end show
macro show " end show
hiding show " end show
hide " end hide
array ( " ) " end array
left
center
right
%%
( " )
include ( " )
< " | " := " >
bottom
false
define " of " as " end define
...
***
Zero
One
Two
Three
Four
Five
Six
Seven
Eight
Nine
Ten
Base
Xor ( " , " , " )
Carry ( " , " , " )
Plus ( " , " , " )
Borrow ( " , " , " )
Compare ( " , " , " )
Minus ( " , " , " )
BoolTag
IntTag
PairTag
ExTag
MapTag
equal1 ( " , " )
TheInt ( " , " )
int ( " )
plus1 ( " , " )
plus2 ( " , " , " , " )
minus1 ( " )
minus2 ( " , " )
times1 ( " , " )
times2 ( " , " , " , " )
lt1 ( " , " )
lt2 ( " , " , " , " )
append ( " , " )
reverse ( " )
revappend ( " , " )
nth ( " , " )
exception
map ( " )
Catch ( " )
catch ( " )
object ( " )
Object ( " , " , " )
destruct ( " )
0
1
2
3
4
5
6
7
8
9
numeral ( " )
num1 ( " , " , " )
num2 ( " , " , " )
evenp ( " )
oddp ( " )
half ( " )
small ( " )
double ( " , " )
lognot ( " )
logior ( " , " )
logxor ( " , " )
logand ( " , " )
logeqv ( " , " )
lognand ( " , " )
lognor ( " , " )
logandc1 ( " , " )
logandc2 ( " , " )
logorc1 ( " , " )
logorc2 ( " , " )
logtest ( " , " )
ash ( " , " )
ash+ ( " , " )
ash- ( " , " )
logbitp ( " , " )
logcount ( " )
logcount1 ( " )
integer-length ( " )
vector-mask
octet-base
vector-empty ( " )
vector-head1 ( " )
vector-tail1 ( " )
vector-cons ( " , " )
vector ( " )
vector-norm ( " )
vector-suffix ( " , " )
vector-prefix ( " , " )
vector-subseq ( " , " , " )
vector-length ( " )
vector-index ( " , " )
vector-head ( " )
vector-tail ( " )
vector2byte* ( " )
vector2byte*1 ( " , " )
vector2vector* ( " )
vector2vector*1 ( " , " )
bt2byte* ( " )
bt2byte*1 ( " , " )
bt2vector* ( " )
bt2vector*1 ( " , " )
bt2vector ( " )
revbyte*2vector ( " , " )
vector-revappend ( " , " )
vt2byte* ( " )
vt2byte*1 ( " , " )
vector-revappend1 ( " , " )
vt2vector* ( " )
vt2vector*1 ( " , " )
vt2vector ( " )
floor1 ( " , " )
ceiling1 ( " , " )
round1 ( " , " )
floor ( " , " )
ceiling ( " , " )
truncate ( " , " )
round ( " , " )
reverse quotient ( " )
length ( " )
length1 ( " , " )
list-prefix ( " , " )
list-suffix ( " , " )
lookup ( " , " , " )
zip ( " , " )
array1 ( " , " , " )
array2 ( " , " , " , " )
array3 ( " , " )
array4 ( " , " )
array5 ( " , " , " , " , " )
push ( " , " , " )
pop ( " , " )
get* ( " , " )
push* ( " , " , " )
pop* ( " , " )
array-domain ( " )
sort-merge ( " , " )
sort-merge1 ( " , " )
eval ( " , " , " )
eval1 ( " , " , " , " )
spy ( " )
trace ( " )
print ( " )
timer ( " )
measure ( " , " )
test1
test2 ( " )
diagnose " end diagnose
test3 ( " , " )
test3* ( " , " )
ttst1 ( " )
ftst1 ( " )
etst1 ( " )
ttst " end test
ftst " end test
etst " ; " end test
texshow " end texshow
testfunc1 ( " )
testfunc2 ( " , " )
testfunc3
testfunc4
testfunc5 ( " )
testfunc6 ( " )
testfunc7 ( " )
testfunc8 ( " , " )
YY
compile ( " )
compile1 ( " , " , " )
compile2 ( " , " , " )
compile3 ( " , " , " )
compile4 ( " , " )
make-constant ( " )
deBruijn ( " , " , " )
deBruijn1 ( " , " )
deBruijn2 ( " )
lazy-nth ( " , " )
make-variable ( " , " , " )
make-lambda ( " )
make-lambdas ( " , " )
compile-code ( " , " )
compile-code1 ( " , " , " )
compile-code2 ( " , " , " , " )
compile-code2* ( " , " , " , " , " )
prune ( " , " )
prune1 ( " , " )
prune* ( " , " , " )
eval-claim
compile-claim ( " , " , " )
macro1
macro2 ( " )
macro3 ( " , " , " )
macro3* ( " , " , " )
macro4 ( " )
macrostate0
stateexpand ( " , " , " )
stateexpand* ( " , " , " )
substitute ( " , " , " )
substitute* ( " , " , " )
expand ( " , " )
protect " end protect
Macro define " as " end define
Macrodefine ( " )
macro define " as " end define
macrodefine ( " )
self
makeself ( " )
root protect " end protect
rootprotect ( " )
render define " as " end define
tex use define " as " end define
tex show define " as " end define
value define " as " end define
message define " as " end define
execute define " as " end define
priority table "
verifier " end verifier
unpacker " end unpacker
renderer " end renderer
expander " end expander
ragged right
make macro expanded version ragged right
<<>>
<< " >>
tuple1 ( " )
tuple2 ( " , " )
eager define " as " end define
eager1 ( " )
eager2 ( " , " , " )
eager message define " as " end define
late eager define " as " end define
late unhide " end unhide
late optimized define " as " end define
macrolet1 ( " )
destructure
destructure define " as " end define
let1 ( " )
let2 ( " , " , " , " )
let3 ( " , " , " , " )
make-var ( " )
make-let ( " , " , " )
make-prime ( " )
make-head ( " )
make-tail ( " )
back " quote " end quote
make-root ( " , " )
make-pair ( " , " , " )
make-true ( " )
make-quote ( " , " )
make-make-root ( " , " , " )
backquote0 ( " )
backquote1 ( " , " , " )
backquote2 ( " , " , " , " , " )
backquote2* ( " , " , " , " , " )
text " : " end text
tex ( " )
latex ( " )
bibtex ( " )
makeindex ( " )
dvipdfm ( " )
page ( " , " ) title " bib " main text " appendix " end page
page1 ( " )
tex-file ( " , " , " )
tex-command ( " , " )
quit request ( " )
boot event ( " , " , " , " )
write request ( " )
writeln request ( " )
println ( " )
read request
read reply ( " )
exec request ( " , " )
exec reply ( " , " )
extend request ( " , " )
extend reply ( " )
exit interrupt
time interrupt
memory interrupt
Hello World
Echo
Echo1 ( " )
Eecho
Eecho1 ( " )
verbatim define " as " end define
lgcio ( " )
EOS
FileWrite
FileWriteExec
FileRead
FileRm
FileSymlink
FileReadLink
FileMkdir
FileRmdir
FileDir
FileType
FileTypeRead
TextWrite
TextWriteExec
FileGetCwd
UnixTime
Demonize
Execlp1
TcpQuery
FileTypeNonexistent
FileTypeOther
FileTypeRegular
FileTypeDirectory
FileTypeLink
NULL
TAB
LF
FF
CR
SP
QQ
V128
V255
CRLF
LFCR
''
septet*2card ( " , " )
septet-base
parse-card ( " )
parse-card1 ( " , " )
exp10 ( " )
parse-unixTime ( " )
make-card ( " )
fileWrite ( " , " )
fileWriteExec ( " , " )
fileRead ( " )
fileRm ( " )
fileSymlink ( " , " )
fileReadLink ( " )
fileMkdir ( " )
fileRmdir ( " )
fileDir ( " )
fileType ( " )
fileTypeRead ( " )
textWrite ( " , " , " )
textWriteExec ( " , " , " )
fileGetCwd
unixTime
demonize ( " , " , " )
execlp1 ( " , " , " )
tcpQuery ( " , " , " , " , " )
lgcio-interface
lgcio1
lgcio2 ( " )
lgcio3
lgcio4 ( " )
default ( " , " )
repeat ( " , " )
lgc-string2mixed ( " )
lgc-string2mixed1 ( " )
lgc-hexdigit ( " )
rack2sl ( " )
rack2sl1 ( " , " )
rack2sl-card ( " , " )
rack2sl-pair ( " , " )
sl2rack ( " )
sl2rack1 ( " , " , " )
sl2rack-vector ( " , " , " , " , " )
lgr-rack-clean ( " )
lgr-cache-restore ( " )
lgr-cluster-closure ( " , " )
lgr-cluster-closure1 ( " , " )
lgr-array-add ( " , " )
lgr-cluster-closure2 ( " , " )
ripemd-mask0
ripemd-mask1 ( " )
ripemd-rol ( " , " )
ripemd-f ( " , " , " )
ripemd-g ( " , " , " )
ripemd-h ( " , " , " )
ripemd-i ( " , " , " )
ripemd-j ( " , " , " )
ripemd-gg-const
ripemd-hh-const
ripemd-ii-const
ripemd-jj-const
ripemd-ggg-const
ripemd-hhh-const
ripemd-iii-const
ripemd-jjj-const
ripemd-init
ripemd-compress ( " , " )
ripemd-buffer2array ( " )
ripemd-buffer2array1 ( " , " , " )
ripemd-chunk
ripemd-pad
ripemd ( " )
ripemds ( " )
ripemd1 ( " , " , " , " )
ripemd-finish ( " , " , " , " )
ripemd-length ( " , " )
ripemd2 ( " )

""D 2
+"
-"
0"
1"
2"
3"
4"
5"
6"
7"
8"
9"
tight newline "
!"

""D 4
" factorial
" _ { " }
" prime
"_"
" %0
" %1
" %2
" %3
" %4
" %5
" %6
" %7
" %8
" %9
" head
" tail
" raise
" catch
" catching maptag
" maptag
" untag
" boolp
" truep
" falsep
" intp
" pairp
" atom
" mapp
" objectp
" root
" Head
" Tail
" TheBool
" TheNat
" norm
" Tag
" BoolP
" IntP
" PairP
" ExP
" MapP
" ObjectP
" Sign
" Mag
" zeroth
" first
" second
" third
" fourth
" fifth
" sixth
" seventh
" eighth
" ninth
" ref
" idx
" debug
" [[ " ]]
" [[ " -> " ]]
" [[ " => " ]]
" tight endline
" unquote
" last

""D 6
" ' "
" apply "

""D 8
- "
+ "

""D 10
" Times "
" * "

""D 12
" Plus "
" Minus "
" + "
" - "

""D 14
PlusTag "
MinusTag "

""D 16
" div "
" mod "

""D 17
" LazyPair "
" Pair "
" NatPair "
" :: "

""D 19
" ,, "

""D 20
" = "
" != "
" Equal "
" LT "
" < "
" <= "
" > "
" >= "
" r= "
" t= "
" t=* "

""D 22
Not "
.not. "
notnot "

""D 24
" And "
" .and. "
" .then. "
" .prog1. "
" &c "

""D 26
" Or "
" .or. "

""D 29
" Iff "

""D 30
" Select " else " end select
" IN "

""D 32
\ " . "
If " then " else "
if " then " else "
newline "
LET " BE "
let " := " in "
let " = " in "
ripemd-ff ( " , " , " , " , " , " , " ); "
ripemd-gg ( " , " , " , " , " , " , " ); "
ripemd-hh ( " , " , " , " , " , " , " ); "
ripemd-ii ( " , " , " , " , " , " , " ); "
ripemd-jj ( " , " , " , " , " , " , " ); "
ripemd-fff ( " , " , " , " , " , " , " ); "
ripemd-ggg ( " , " , " , " , " , " , " ); "
ripemd-hhh ( " , " , " , " , " , " , " ); "
ripemd-iii ( " , " , " , " , " , " , " ); "
ripemd-jjj ( " , " , " , " , " , " , " ); "

""D 33
norm "
" Guard "
" is val : "
" is bool : "
" is int : "
" is pair : "
" is map : "
" is object : "

""D 34
" reduce to "
" == "

""D 51
" lgcthen "
","
"[ " ]"
"[[ " ]]"
"[[[ " ]]]"

""D 50
" endline

""D 52
" linebreak "

""D 54
" & "

""D 56
" \\ "

""B

text "index.html" : ""-"";
<head>
<title>
A Logiweb base page
</title>
</head>

<body>
<h2>
A Logiweb base page
</h2>

<p>
<a href='../index.html'>Up</a>
</p>

<p>

Contents:
<a href='page.pdf'>Main text</a>
<a href='chores.pdf'>Chores</a>
</p>

<p><address>Klaus Grue</address></p>
</body>
" end text ,,



text "page.bib" : ""-"";

@article      {berline97,
  author    = {C. Berline and K. Grue},
  title     = {A $\kappa$-denotational semantics for {M}ap {T}heory
               in {ZFC+SI}},
  journal   = TCS,
  year      = {1997},
  volume    = {179},
  number    = {1--2},
  pages     = {137--202},
  month     = {jun}}

@inproceedings{Logiweb,
  author    = {K. Grue},
  title     = {Logiweb},
  editor    = {Fairouz Kamareddine},
  booktitle = {Mathematical Knowledge Management Symposium 2003},
  publisher = {Elsevier},
  series    = {Electronic Notes in Theoretical Computer Science},
  volume    = {93},
  year      = {2004},
  pages     = {70--101}}

@techreport{chores,
  author    = {K. Grue},
  year      = {2006},
  title     = {A Logiweb base page - chores},
  institution={Logiweb},
  note      = {\href {\lgwBlockRelay \lgwBlockThis
/page/appendix.pdf}{\lgwBreakRelay \lgwBreakThis /page/appendix.pdf}}}

" end text ,,



text "page.tex" : ""-"";
\documentclass[fleqn]{article}

% Include definitions generated by the Logiweb compiler
\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=UseNone}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
% (x,y)=(120,80) lower left, (x,y)=(490,730) upper right
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle=A Logiweb base 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 base page}
\author{Klaus Grue}
\maketitle
\tableofcontents

"[ make macro expanded version ragged right ]"



\section{Introduction}"[ "

\indexintro{Logiweb} \cite{Logiweb} is an open source system available under GNU GPL for distribution of mathematical definitions, lemmas, and proofs.

The present document is part of a \index{page, Logiweb}\indexintro{Logiweb page}. A Logiweb page is a cluster of documents which has been submitted to the Logiweb system. Such a cluster typically consists of a main document like the present one plus a number of electronic appendices.

The present Logiweb page (i.e.\ the document cluster to which the present document belongs) is a Logiweb \index{base page}\intro{base} page. A Logiweb base page is a Logiweb page which references no other Logiweb pages. Logiweb base pages are self-contained pages which define elementary concepts.



\subsection{Electronic appendices}

The present Logiweb page comprises one html and two PDF files, located the following places:

\begin{itemize}
\item \href {\lgwBlockRelay \lgwBlockThis /page/page.pdf}{%
\lgwBreakRelay \lgwBreakThis /page/page.pdf}
\item \href {\lgwBlockRelay \lgwBlockThis /page/appendix.pdf}{%
\lgwBreakRelay \lgwBreakThis /page/appendix.pdf}
\item \href {\lgwBlockRelay \lgwBlockThis /page/page.pdf}{%
\lgwBreakRelay \lgwBreakThis /page/page.pdf} \cite{chores}
\item \href {\lgwBlockRelay \lgwBlockThis /page/page.html}{%
\lgwBreakRelay \lgwBreakThis /page/page.html}
\end{itemize}

The first link points to the present paper. The second link points to an electronic appendix with definitions that would bore most readers (such as definitions of how each construct should be rendered). The second link is included in the \textsc{Bib}\TeX\ bibliography \cite{chores} for easy reference. The third link points to a table of contents.



\subsection{Proclamations}\label{sec:Proclamations}

Logiweb has a number of predefined semantic concepts. Each predefined concept has a name where a name is a string of characters.

Furthermore, Logiweb has a \indexintro{proclamation} mechanism which allows to connect syntactic constructs with semantic concepts. Some proclamations are given in the following.

\begin{statements}

\item "[[ proclaim \ x . y as "lambda" end proclaim ]]"\index{lambda} connects the syntactic construct "[[ \ x . y ]]" with the semantic concept whose name reads ``lambda''. This proclamation tells Logiweb that "[[ \ x . y ]]" denotes \index{abstraction, lambda}\indexintro{lambda abstraction} in the present context. The proclamation has effect on the present Logiweb page and all Logiweb pages which reference the present page.

\item "[[ proclaim x ' y as "apply" end proclaim ]]"\index{apply} proclaims "[[ x ' y ]]" to denote \index{application, functional}\indexintro{functional application}.

\item "[[ proclaim true as "true" end proclaim ]]"\index{true} proclaims "[[ true ]]" to denote \indexintro{truth}.

\item "[[ proclaim If x then y else z as "if" end proclaim ]]"\index{if} proclaims "[[ If x then y else z ]]"  to denote an \index{construct, if-then-else}\indexintro{if-then-else construct}. This and the previous 3 constructs are explained in more detail in Section \ref{sec:Computation}.

\item "[[ proclaim quote x end quote as "quote" end proclaim ]]"\index{quote} proclaims "[[ quote x end quote ]]" to denote a data structure which represents the term "[[ x ]]". This is explained in more detail in Section \ref{sec:RepresentationOfTerms}.

\item "[[ proclaim proclaim x as y end proclaim as "proclaim" end proclaim ]]"\index{proclaim} proclaims "[[ proclaim x as y end proclaim ]]" to denote \indexintro{proclamation}. Each construct in Logiweb is identified by a reference and an index, both of which are integers. The reference identifies the Logiweb page which introduces the construct. If a page is a `base' page in the sense that it references no other pages, then the construct with index 1 of that page is born as a proclamation construct. Such a proclamation construct can declare other constructs to be proclamation constructs. But it also has to secure itself by declaring itself as a proclamation construct as it otherwise looses its proclamation ability. The present page happens to be a base page and the construct above happens to be construct number 1 of the present page.

\item "[[ proclaim define x of y as z end define as "define" end proclaim ]]"\index{define} says that "[[ define x of y as z end define ]]" \index{definition}\intro{defines} the "[[ x ]]" \indexintro{aspect} of "[[ y ]]" to be "[[ z ]]". As an example of use, "[[ define value of x factorial as if x = 0 then 1 else x * ( x - 1 ) factorial end define ]]" defines the \index{aspect, value}\indexintro{value aspect} of "[[ x factorial ]]" such that "[[ ttst 3 factorial = 6 end test ]]".

\item "[[ proclaim Define x of y as z end define as "define" end proclaim ]]" says that "[[ Define x of y as z end define ]]" means exactly the same as "[[ define x of y as z end define ]]". The difference is in how the right hand side of the definition is rendered. "[[ define x of y as z end define ]]" renders "[[ z ]]" using the \index{aspect, tex use}\index{use aspect, tex}\indexintro{tex use aspect} of "[[ z ]]" whereas "[[ Define x of y as z end define ]]" uses the \index{aspect, tex show}\index{show aspect, tex}\indexintro{tex show aspect}. For more on the tex use and tex show aspects see Section \ref{sec:AspectDeclarations} and see the newline construct at the end of Section \ref{sec:ElementaryDefinitions}.

\item "[[ proclaim lgcdef x of y as z enddef as "define" end proclaim ]]" defines "[[ lgcdef x of y as z enddef ]]" as an alternative for "[[ Define x of y as z end define ]]". "[[ lgcdef x of y as z enddef ]]" is used by the lgc compiler for translating the "[[ !""-""!""!N" ]]" and "[[ !""-""!""!C" ]]" directives into name and charge definitions for all constructs on a page.

\item "[[ proclaim optimized define x of y as z end define as "introduce" end proclaim ]]"\index{introduce} says that "[[ optimized define x of y as z end define ]]" means exactly the same as "[[ Define x of y as z end define ]]", except that "[[ optimized define x of y as z end define ]]" may affect CPU run time dramatically in a few, vital cases c.f.\ Section \ref{sec:ElementaryDefinitions}.

\item "[[ proclaim hide x end hide as "hide" end proclaim ]]"\index{hide} proclaims that "[[ x ]]" in "[[ show hide x end hide end show ]]" should be hidden from \indexintro{harvesting}. Harvesting is the process in which proclamations, definitions, and other Logiweb \index{revelation}\intro{revelations} are collected from a page. Hiding may be useful e.g.\ when talking about revelation constructs without wanting them to take effect. For more on hiding see Section \ref{sec:VisibilityConstructs}.

\end{statements}

Logiweb has predefined concepts with the names used above (apply, lambda, true, if, quote, proclaim, define, introduce, hide, pre, and post). Logiweb has no other predefined concepts than those. Attempts to proclaim a construct to denote some unknown concept are ignored. The \index{compiler, Logiweb}\indexintro{Logiweb compiler} (a tool for constructing Logiweb pages) issues a warning in case of unrecognized proclamations.



\subsection{Aspect declarations}\label{sec:AspectDeclarations}

On Logiweb, constructs that assign meaning to constructs always assign meaning to a particular \indexintro{aspect} of the construct. Some aspects are defined by the following \index{aspect declaration}\index{declaration, aspect}\intro{aspect declarations}.

\begin{statements}

\item "[[ Define "message" of message as "message" end define ]]"\index{message} defines "[[ message ]]" to represent the \index{aspect, message}\indexintro{message aspect}. The message aspect of a construct indicates which aspect the construct represents. For an example of use, see the next entry.

Section \ref{sec:Proclamations} proclaimed two definitions constructs, one with and one without an exclamation mark. The one with the exclamation mark renders its arguments using the tex show aspect whereas the one without renders its aspect and right hand side using the tex use aspect. The tex show aspect of a string comprises the string with quotes around whereas the tex use aspect of a string is the string without quotes. The exclamation mark version of the definition construct is used here to make it easy distinguish strings from non-strings.

\item "[[ Define message of value as "value" end define ]]"\index{value} defines "[[ value ]]" to represent the \index{aspect, value}\indexintro{value aspect}. As an example, the definition "[[ Define value of x factorial as if x = 0 then 1 else x * ( x - 1 ) factorial end define ]]" from Section \ref{sec:Proclamations} used "[[ value ]]" to represent the value aspect. One may replace "[[ message ]]" and "[[ value ]]" by the strings they denote as in "[[ Define "message" of value as "value" end define ]]" and "[[ Define "value" of x factorial as if x = 0 then 1 else x * ( x - 1 ) factorial end define ]]".

\item "[[ Define message of name as "name" end define ]]"\index{name} defines "[[ name ]]" to represent the \index{aspect, logiweb name}\index{name aspect, logiweb}\indexintro{logiweb name aspect}. The name aspect of a construct is a plain text representation for the construct. Such a plain text representation is useful when editing Logiweb pages using an ordinary text editor. As an example, the name aspects of "[[ \ x . y ]]", "[[ u ]]", and "[[ v ]]" are \verb+\""!.""!+, \verb+vu+, and \verb+vv+, respectively. For that reason, one may type \verb+\ u . vv+ in a text editor, run the text through a Logiweb compiler, and get a Logiweb page containing "[[ \ u . v ]]". For examples of name definitions see Section ``Name definitions'' in \cite{chores}.

\item "[[ Define message of lgcname as "name" end define ]]"\index{lgcname} defines "[[ lgcname ]]" the same way as "[[ name ]]". "[[ lgcname ]]" is used by the lgc compiler for translating the "[[ !""-""!""!N" ]]" escape sequence to name definitions for all constructs on a page.

\item "[[ Define message of lgccharge as "charge" end define ]]"\index{lgccharge} defines "[[ lgccharge ]]" to represent the \index{aspect, logiweb charge}\index{charge aspect, logiweb}\indexintro{logiweb charge aspect}. "[[ lgccharge ]]" is used by the lgc compiler for translating the "[[ !""-""!""!C" ]]" escape sequence to charge definitions for all constructs on a page. The charge aspect of a construct is a dotted list of integers represented as a string. Charges define the precedence of operators such that constructs with high charges have low priority and vice versa. As an example, "[[ x + y ]]" has greater charge than "[[ x * y ]]" so "[[ a * b + c * d ]]" means "[[ ( a * b ) + ( c * d ) ]]".

\item "[[ Define message of tex use as "use" end define ]]"\index{tex use}\index{use, tex} defines "[[ tex use ]]" to represent the \index{aspect, tex use}\index{use aspect, tex}\indexintro{tex use aspect}. The tex use aspect of a construct indicates how the aspect should be rendered in \TeX\ when using the construct. For examples of tex use definitions see Section ``\TeX\ definitions'' in \cite{chores}.

\item "[[ Define message of tex show as "show" end define ]]"\index{show, tex}\index{tex show} defines "[[ tex show ]]" to represent the \index{show aspect, tex}\index{aspect, tex show}\indexintro{tex show aspect}. The tex show aspect of a construct indicates how the aspect should be rendered in \TeX\ when talking about the construct. Most constructs look the same when using them and when talking about them. For that reason, the tex show aspect defaults to the tex use aspect. As an example, "[[ \ x . y ]]" has no tex show aspect so "[[ \ x . y ]]" looks the same when using lambda abstraction and when talking about lambda abstraction. Some constructs look different when using them and when talking about them, c.f.\ Section \ref{sec:VisibilityConstructs}. For examples of tex show definitions see Section ``\TeX\ definitions'' in \cite{chores}. For more on the use of tex use and tex show aspects, see the newline construct at the end of Section \ref{sec:ElementaryDefinitions}.

\item "[[ Define message of priority as "priority" end define ]]"\index{priority} defines "[[ priority ]]" to represent the \index{aspect, priority}\indexintro{priority aspect}. Before Logiweb Version 0.2.0, the priority aspect of a Logiweb page indicated the priority and associativity of all constructs on the page itself plus all constructs on directly referenced Logiweb pages. From Logiweb Version 0.2.0, the charge aspect is used in place of the priority aspect. However, a Logiweb Version 0.1.x compiler is required for compiling the Logiweb Version 0.2.0 compiler, and 0.1.x compilers need the priority aspect. For that reason, the priority aspect is kept until further.

The statement above that the priority aspect of a Logiweb page indicates the priorities is not completely true. Aspects attach to constructs, not to pages. However, each Logiweb page has a \index{construct, page}\indexintro{page construct} which represents the page (c.f.\ Section \ref{sec:RepresentationOfTerms}). The page construct of the present page reads ``"[[ base ]]"'' and the priority table in \cite{chores} is indeed a definition of the priority aspect of this ``"[[ base ]]"'' construct.

\item "[[ Define message of macro as "macro" end define ]]"\index{macro} defines "[[ macro ]]" to represent the \index{aspect, macro}\indexintro{macro aspect}. The macro aspect defines how a Logiweb page is macro expanded, c.f.\ Section \ref{sec:MacroExpansion}.

\item "[[ Define message of render as "render" end define ]]"\index{render} defines "[[ render ]]" to represent the \index{aspect, render}\indexintro{render aspect}. Logiweb has a predefined way of rendering Logiweb pages, but rendering can be modified using the render aspect.

\item "[[ Define message of claim as "claim" end define ]]"\index{claim} defines "[[ claim ]]" to represent the \index{aspect, claim}\indexintro{claim aspect}. The claim aspect defines how a Logiweb page is verified, c.f.\ Section \ref{sec:Verification}.

\item "[[ Define message of unpack as "unpack" end define ]]"\index{unpack} defines "[[ unpack ]]" to represent the \index{aspect, unpack}\indexintro{unpack aspect}. When stored on disk or transmitted over a network, Logiweb pages are stored as \index{Logiweb vector}\index{vector, Logiweb}\intro{Logiweb vectors}, i.e.\ as sequences of bytes. Logiweb has a predefined way of unpacking Logiweb vectors into Logiweb pages, but unpacking can be modified using the unpack aspect.

\item "[[ Define message of execute as "execute" end define ]]"\index{execute} defines "[[ execute ]]" to represent the \index{aspect, execute}\indexintro{execute aspect}. If the execute aspect of a string "[[ s ]]" is defined then the Logiweb compiler generates an executable named "[[ s ]]" whose behavior is defined by the right hand side of the execute definition.

\item "[[ Define message of exampleaspect0 as "example aspect/kg" end define ]]" defines "[[ exampleaspect0 ]]" to represent an aspect named `example aspect/kg'. The exampleaspect0 aspect is a \index{aspect, user}\indexintro{user aspect} in the sense that Logiweb does not know about it in advance. To avoid name conflicts, one should give any user aspect a personal touch. The exampleaspect0 aspect above is represented by a string which includes the initials of the present author. In general, user aspects should contain at least one character which is not a small latin letter (a to z) and not a space. The example aspect above is ok since it contains a slash. Aspects which contain only small latin letters and spaces are reserved for future extensions of Logiweb. The only exception is the 'destructure' aspect defined later which consists of only small latin letters for historical reasons.

\item "[[ Define message of exampleaspect1 as exampleaspect2 end define ]]" defines "[[ exampleaspect1 ]]" to represent a user aspect represented by the construct "[[ exampleaspect2 ]]". "[[ exampleaspect2 ]]" is a construct introduced on the present page. Like any other Logiweb construct, it is identified by a \indexintro{reference} and an \indexintro{index}. The reference is a world-wide unique natural number which identifies the present page. The index is a natural number which distinguishes the "[[ exampleaspect2 ]]" construct from the other constructs introduced on the present page. The definition of "[[ exampleaspect1 ]]" above defines "[[ exampleaspect1 ]]" to denote an aspect which is represented by the reference and identifier of "[[ exampleaspect2 ]]". Contrary to the definition of the exampleaspect0 aspects above, there is no risk of name conflicts. On the other hand, the "[[ exampleaspect2 ]]" ceases to exist if the present page is ever deleted from Logiweb.

\item "[[ Define message of exampleaspect2 as exampleaspect2 end define ]]" defines "[[ exampleaspect2 ]]" to represent the user aspect represented by "[[ exampleaspect2 ]]" itself. Hence, "[[ exampleaspect1 ]]" and "[[ exampleaspect2 ]]" denote the same aspect.

\end{statements}

Logiweb assigns a particular semantics to the value, name, use, show, priority, macro, claim, message, unpack, and execute aspects. Logiweb does not assign semantics to any other aspects, but it allows users to declare arbitrary user aspects like the example aspects above. It is up to the authors of Logiweb pages to assign semantics to user aspects. As an example, the present page declares a `destructure' user aspect in Section \ref{sec:LetConstructs} and defines a destructuring `let' macro such that `let' uses the `destructure' aspect. Apart from the destructure aspect, any user defined aspect should contain at least one character which is neither a small latin letter (a to z) nor a space.



\subsection{Definition of pre- and post-associativity}

\begin{statements}

\item "[[ Define priority of preassociative x greater than y as "pre" end define ]]"\index{pre} defines "[[ show preassociative x greater than y end show ]]" to denote \index{preassociative}\intro{preassociativity}. A preassociative construct is leftassociative in text that runs left to right, rightassociative in text that runs right to left, topassociative in text that runs from top to bottom, counter-clock-wise-associative in text written in clock-wise spirals, and so on. "[[ show preassociative x greater than y end show ]]" states that all constructs listed in the "[[ x ]]" position are preassociative and that all of them have greater priority than those listed in the "[[ y ]]" position. For a table of associativites and priorities see the chapter named ``Priority table'' in \cite{chores}.

\item "[[ Define priority of postassociative x greater than y as "post" end define ]]"\index{post} defines "[[ show postassociative x greater than y end show ]]" to denote \index{postassociative}\intro{postassociativity}.

\end{statements}



\subsection{The Logiweb system}\label{sec:TheLogiwebSystem}

From a standardization point of view, the Logiweb system comprises two standards, one which defines the syntax and semantics of Logiweb pages and one which defines a protocol for exchanging information about Logiweb pages.

From an implementation point of view, the current implementation of the Logiweb system comprises two programs called the \index{compiler, Logiweb}\indexintro{Logiweb compiler} and the \index{server, Logiweb}\indexintro{Logiweb server}, respectively, plus a number of auxilliary files and programs.

From a user point of view, Logiweb comprises a number of Logiweb pages which the user can browse using an ordinary web browser or search using an ordinary web search engine.

Users who merely want to read existing Logiweb pages can do with an ordinary web browser. Users will need the Logiweb compiler in the following cases:

\begin{enumerate}

\item\label{enum:author} when authoring and submitting new Logiweb pages.

\item\label{enum:mirror} when mirroring Logiweb pages, i.e.\ when a user wants to make a particular Logiweb page available on the users own web site.

\item\label{enum:execute} when executing computable functions on Logiweb pages (c.f.\ the ``execute'' aspect in Section \ref{sec:AspectDeclarations}).

\end{enumerate}

In general, users will not be aware of Logiweb servers. All Logiweb servers in the world cooperate on indexing all Logiweb pages in the world, which is needed in connection with the internal referencing system of Logiweb. When searching for Logiweb pages, users should use an ordinary web search engine.

Even though Logiweb has several components and even though one can view Logiweb from several points of view, the only piece of Logiweb software users will typically meet is the Logiweb compiler. Typically, when the present paper states that Logiweb is able to perform various tasks, those tasks are actually undertaken by the Logiweb compiler.

Note that the Logiweb compiler is just one, possible implementation of Logiweb. A wysiwyg Logiweb browser/editor was once implemented but is not currently maintained, but one may foresee other tools than the Logiweb compiler for viewing, authoring, mirroring, and executing Logiweb pages.



" ]"\section{Computation}\label{sec:Computation}"[ "

Logiweb (i.e.\ the Logiweb compiler, c.f.\ Section \ref{sec:TheLogiwebSystem}) is able to \indexintro{reduce} computable terms to \index{form, normal}\indexintro{normal form}. It does so using the \index{computing engine, Logiweb}\index{engine, Logiweb computing}\indexintro{Logiweb computing engine}.

The Logiweb engine is just a computing engine; it has no facilities for communicating with the outside world. The Logiweb machine (c.f.\ Section \ref{sec:Interaction}) contains the Logiweb engine and also contains facilities for input/output.



\subsection{Reduction system}\label{sec:ReductionSystem}

The engine reduces terms according to the following reduction system:

"[[[ array ( left,left,left )

( \ x . y ) ' z & %% reduce to %% & < y | x := z > \\

true ' z & %% reduce to %% & true \\

If true then u else v & %% reduce to %% & u \\

If \ x . y then u else v & %% reduce to %% & v

end array ]]]"

\noindent "[[ < x | y := z > ]]" denotes the result of replacing all free occurrences of the variable "[[ y ]]" in the term "[[ x ]]" by the term "[[ z ]]", possibly renaming bound variables as needed.



\subsection{Normal forms}\label{sec:NormalForms}

We shall say that a term "[[ z ]]" is on \index{normal form}\indexintro{truth normal form} if the term "[[ z ]]" is identical to "[[ true ]]". We shall say that a term "[[ z ]]" is on \indexintro{function normal form} if the term "[[ z ]]" has form "[[ \ x . y ]]" where "[[ x ]]" is a variable and "[[ y ]]" is a term. We shall say that a term is on \indexintro{root normal form} if the term is on truth or function normal form.

When given a term, the Logiweb engine starts reducing the term using leftmost reduction. The Logiweb engine stops again when the term reaches root normal form, if ever.

We shall say that a term is a \indexintro{true term} if the engine reduces it to a truth normal form and that a term is a \indexintro{function term} if the engine reduces it to a function normal form. We shall say that a term is a \indexintro{bottom term} if the engine reduces the term forever without reaching a root normal form.



\subsection{Maps}\label{sec:Maps}

The reduction system above is pure lambda calculus extended with an uhr-element "[[ true ]]" and an if-then-else construct which can test for equality to "[[ true ]]". It is out of the scope of the present page to explain why that extension is vital.

It is possible to reason about lambda calculus extended with "[[ true ]]" and "[[ If x then y else z ]]" using \index{theory, map}\indexintro{map theory} \cite{berline97}. Using the terminology of \cite{berline97} we shall refer to values of terms built from "[[ \ x . y ]]", "[[ x ' y ]]", "[[ true ]]", and "[[ If x then y else z ]]" as \index{map}\intro{maps}.

Map theory defines a notion of equality named "[[ x == y ]]". We shall use "[[ x = y ]]" to denote that "[[ x ]]" and "[[ y ]]" are equal modulo identifications whereas we use "[[ x == y ]]" to denote genuine equality.

In other words, we use a sign with two horizontal bars, "[[ x = y ]]" to denote that "[[ x ]]" and "[[ y ]]" are very much equal and one with 3 horizontal bars, "[[ x == y ]]" to denote that "[[ x ]]" and "[[ y ]]" are even more equal.

The use of "[[ x = y ]]" to denote an equivalence relation (equality modulo identifications) and "[[ x == y ]]" to denote equality is apparently opposite to normal mathematical use. In practice, the use of "[[ x = y ]]" to denote equality modulo identification is very much in line with mathematical litterature. As an example, if one identifies the bidual of a Hilbert space with the Hilbert space itself, then it is common practice to use "[[ x = y ]]" between members of the bidual and members of the Hilbert space.

Anyone who can come up with a better name than "[[ x == y ]]" for true, identification disrespecting equality is welcome to contact the author.

Note that "[[ x == y ]]" has much lower priority than "[[ x = y ]]" according to the priority table in \cite{chores}. As an example, "[[ \ x . x = x == y ]]" means "[[ ( \ x . ( x = x ) ) == y ]]".

The reduction rules of Section \ref{sec:ReductionSystem} correspond to the following axioms of map theory:

"[[[ array ( left,left,left )

( \ x . y ) ' z & %% == %% & < y | x := z > \\

true ' z & %% == %% & true \\

If true then u else v & %% == %% & u \\

If \ x . y then u else v & %% == %% & v

end array ]]]"



\subsection{Full reduction system}\label{sec:FullReductionSystem}

The reduction system in Section \ref{sec:ReductionSystem} gives a good description of the Logiweb engine from a theoretical point of view, but a more complete description is given in the following:

\begin{itemize}

\item The engine reduces constructs proclaimed to denote lambda abstraction, functional application, truth, and if-then-else as indicated in Section \ref{sec:ReductionSystem}. Section \ref{sec:Proclamations} proclaimed "[[ \ x . y ]]", "[[ x ' y ]]", "[[ true ]]", and "[[ If x then y else z ]]" to denote these concepts, respectively.

\item The engine reduces constructs proclaimed to denote quoting to the value described in Section \ref{sec:RepresentationOfTerms}. Section \ref{sec:Proclamations} proclaimed "[[ quote x end quote ]]" to denote quoting. "[[ quote x end quote ]]" reduces to a term built up from "[[ \ x . y ]]", "[[ x ' y ]]", "[[ true ]]", and "[[ If x then y else z ]]". The value of "[[ quote x end quote ]]" represents the term "[[ x ]]".

\item The engine reduces constructs that have a value definition according to that definition, c.f. Section \ref{sec:ElementaryDefinitions}.

\item The engine reduces page constructs to terms which (in principle) are built up from "[[ \ x . y ]]", "[[ x ' y ]]", "[[ true ]]", and "[[ If x then y else z ]]". The value of a page construct is called the \indexintro{cache} of the given page. The cache of a page is a huge data structure which represents a lot of information about the given page and all its transitively referenced pages. Among other, the cache contains the page before and after macro expansion, a structure which contains all definitions harvested from the page, and a structure which contains compiled versions of all value definitions.

\item The engine reduces all other constructs (non-page constructs that are neither proclaimed nor defined) to "[[ true ]]". This rather arbitrary convention is made to make the behaviour of the engine well-defined in all cases.

\item The engine would be rediculously slow if it wasn't for the optimizations explained in Section \ref{sec:ElementaryDefinitions}.

\end{itemize}



\subsection{Elementary definitions}\label{sec:ElementaryDefinitions}

Consider the following definitions:

\begin{statements}

\item "[[ define value of x LazyPair y as \ z . If z then x else y end define ]]". The engine reduces "[[ x LazyPair y ]]" to the function normal form "[[ \ z . If z then x else y ]]". As we shall see, it is possible to extract "[[ x ]]" and "[[ y ]]" from the return value, so the return value is a \indexintro{pairing} construct.

\item "[[ optimized define value of false as true LazyPair true end define ]]". The engine reduces "[[ false ]]" to the function normal form "[[ \ x . If x then true else true ]]". We shall use "[[ false ]]" to represent \indexintro{falsehood} as opposed to "[[ true ]]" which we use to represent truth.

\item "[[ define value of x Head as x ' true end define ]]". We have "[[[ array ( left )

( u LazyPair v ) Head == %% \\

( \ x . If x then u else v ) Head == %% \\

( \ x . If x then u else v ) ' true == %% \\

If true then u else v == %% \\

u

end array ]]]" Hence, "[[ ( u LazyPair v ) Head == u ]]" whenever "[[ u ]]" and "[[ v ]]" differ from "[[ bottom ]]".

\item "[[ define value of x Tail as x ' false end define ]]". Like above, we have that "[[ ( u LazyPair v ) Tail == v ]]" whenever "[[ u ]]" and "[[ v ]]" differ from "[[ bottom ]]". This supports the claim above that "[[ x LazyPair y ]]" is a pairing construct.

\item "[[ define value of x Guard y as If x then y else y end define ]]". The engine reduces "[[ x Guard y ]]" by reducing "[[ x ]]", discarding the value, reducing "[[ y ]]", and returning the value of "[[ y ]]". Hence "[[ x Guard y ]]" has the following properties:

\begin{itemize}

\item "[[ true Guard y == y ]]"

\item "[[ \ u . v Guard y == y ]]"

\item "[[ bottom Guard y == bottom ]]".

\end{itemize}

"[[ bottom ]]" above is defined in Section \ref{sec:Bottom}. "[[ bottom ]]" is a bottom term, i.e.\ a term which the engine reduces forever without reaching a root normal form (c.f.\ Section \ref{sec:NormalForms}).

\item "[[ define value of x Pair y as x Guard y Guard x LazyPair y end define ]]". The engine reduces "[[ x Pair y ]]" by reducing "[[ x ]]", discarding the value, reducing "[[ y ]]", discarding the value, and then returning the function normal form "[[ \ z . If z then x else y ]]". "[[ x Pair y ]]" is \indexintro{eager} or \indexintro{strict} in the sense that

\begin{itemize}

\item "[[ bottom Pair y == bottom ]]"

\item "[[ x Pair bottom == bottom ]]"

\end{itemize}

\item "[[ protect optimized define value of ( x ) as x end define end protect ]]". This definition says that a parenthesis does not affect the value of its contents. Section \ref{sec:Parentheses} macro defines parentheses such that they disappear during macro expansion which is another way of saying that a parenthesis does not affect the value of its contents. The purpose of the value definition above is to ensure that "[[ ( x ) == x ]]" even in situations where "[[ ( x ) ]]" is not macro expanded. The definition above is itself protected against macro expansion with the "[[ protect x end protect ]]" construct which is defined in Section \ref{sec:ElementaryMacros}. Without that protection, the left hand side of the definition above would be macro expanded from "[[ ( x ) ]]" to "[[ x ]]" so that the definition would define "[[ x ]]" to be equal to itself. Due to the minimal semantics convention, that would define "[[ x ]]" to be equal to "[[ bottom ]]".

\item "[[ protect optimized define value of newline x as x end define end protect ]]". This construct leaves its argument unaffected just like parentheses do; and it is macro defined in Section \ref{sec:Parentheses} just like parentheses are. But the newline construct is rendered differently. When talking about the construct, it is rendered as above. But when using it as in the formula "[[ 2 + newline 3 ]]" it affects line breaking. In the formula, the newline construct appears right after the plus sign. This effect is acheived by definitions in \cite{chores}. In \cite{chores}, the 'tex show' definition of the newline construct defines how the construct should be rendered when it occurs in the left hand side of a definition or some other context where the construct is talked about. Furthermore, the 'tex use' definition of the newline construct in \cite{chores} defines how the newline construct should be rendered when it is used rather than talked about. Finally, in \cite{chores}, the 'tex use' definition of the definition construct specifies that the left hand side of a definition should be rendered using the 'tex show' definition rather than the 'tex use' definition.

\end{statements}

The definition of "[[ false ]]" above is an example of an ``introduction''. Formally, an introduction has exactly the same meaning as a definition. However, each implementation of Logiweb is supposed so contain a finite list of functions which have been hand-coded for efficiency. The nulary function "[[ false ]]" is one such function.

For each hand-coded function, the implementation must contain a definition for an equivalent function expressed solely using the reduction system in \ref{sec:ReductionSystem} plus quoting. When the implementation sees an introduction, it runs through the list of equivalent functions to see if the right hand side matches one of them. If a match is found then the introduced construct is translated into the associated hand-coded function. If no match is found then the introduction is treated as an ordinary definition. As long as implementors are careful to ensure equivalence between hand-coded functions and equivalent functions, this ensures portability of code between different implementations of Logiweb.

Matching of right hand sides against equivalent functions is quite strict: One may change names of variables and names of functions, but apart from that, an exact match is required. It is decidable (and fast to decide) whether two functions match.



\subsection{Booleans}

\begin{statements}

\item "[[ proclaim x Select y else z end select as "if" end proclaim ]]"

\item "[[ define value of Not x as If x then false else true end define ]]"

\item "[[ define value of x And y as x Select If y then true else false else If y then false else false end select end define ]]"

\item "[[ define value of x Or y as x Select If y then true else true else If y then true else false end select end define ]]"

\item "[[ define value of x Iff y as x Select If y then true else false else If y then false else true end select end define ]]"

\item "[[ define value of x TheBool as If x then true else false end define ]]"

\item "[[ define value of x Equal y as If x then newline If y then true else false else newline If y then false else x Head Equal y Head And x Tail Equal y Tail end define ]]"

\end{statements}



\subsection{Naturals}\label{sec:Naturals}

We shall refer to the \index{number, natural}\index{natural number}\intro{natural numbers} 0, 1, 2, and so on as \indexintro{naturals}. We shall say that a list "[[ b _ { 0 } Pair b _ { 1 } Pair ... Pair b _ { n } Pair true ]]" is an \index{representation, untagged}\indexintro{untagged representation} of the natural \[
\sum_{i=0}^{n} 2^i c_i
\] where "[[ c _ { i } ]]" is zero or one when "[[ b _ { i } ]]" is true or false, respectively. When a list is used as an untagged representation of a natural, we shall refer to the list as an \index{natural, untagged}\indexintro{untagged natural}. The following functions apply to untagged naturals.

\begin{statements}

\item "[[ define value of Zero as true end define ]]"

\item "[[ define value of x NatPair y as If x And y then Zero else x TheBool Pair y end define ]]"

\item "[[ define value of x TheNat as If x then Zero else x Head NatPair x Tail TheNat end define ]]"

\item "[[ define value of One as false Pair Zero end define ]]"

\item "[[ define value of Two as true Pair One end define ]]"

\item "[[ define value of Three as false Pair One end define ]]"

\item "[[ define value of Four as true Pair Two end define ]]"

\item "[[ define value of Five as false Pair Two end define ]]"

\item "[[ define value of Six as true Pair Three end define ]]"

\item "[[ define value of Seven as false Pair Three end define ]]"

\item "[[ define value of Eight as true Pair Four end define ]]"

\item "[[ define value of Nine as false Pair Four end define ]]"

\item "[[ define value of Ten as true Pair Five end define ]]"

\item "[[ define value of Xor ( x , y , c ) as x Head Iff y Head Iff c end define ]]"

\item "[[ define value of Carry ( x , y , c ) as If x Head then y Head Or c else y Head And c end define ]]"

\item "[[ define value of Plus ( x , y , c ) as If x And y And c then Zero else Xor ( x , y , c ) NatPair Plus ( x Tail , y Tail , Carry ( x , y , c ) ) end define ]]"

\item "[[ define value of x Plus y as Plus ( x , y , true ) end define ]]"

\item "[[ define value of Borrow ( x , y , b ) as If x Head then y Head And b else y Head Or b end define ]]"

\item "[[ define value of Compare ( x , y , b ) as If x And y then b else Compare ( x Tail , y Tail , Borrow ( x , y , b ) ) end define ]]"

\item "[[ define value of x LT y as Compare ( y , x , false ) end define ]]"

\item "[[ define value of Minus ( x , y , b ) as If x And y then Zero else Xor ( x , y , b ) NatPair Minus ( x Tail , y Tail , Borrow ( x , y , b ) ) end define ]]"

\item "[[ define value of x Minus y as Minus ( x , y , true ) end define ]]"

\item "[[ define value of x Times y as If x then Zero else ( If x Head then Zero else y ) Plus ( true Pair x Tail Times y ) end define ]]"

\end{statements}



\subsection{Bottom}\label{sec:Bottom}

\begin{statements}

\item "[[ optimized define value of bottom as ( \ x . x ' x ) ' ( \ x . x ' x ) end define ]]"

Optimized bottom is a peculiar optimized function. Evaluation of the right hand side above takes forever. So the semantics of "[[ bottom ]]" is that it does not return a value. Optimized bottom is faithful to that: it never returns a value. What it does do is that it prints and error message and kills its caller. So the user can sit comfortably one step further away and watch the caller being killed.

One could suggest some ``bessermachen'' and suggest some sort of catcher which allows to test whether or not some computation results in a call to optimized bottom. That, however, will give grave portability problems and grave problems for reasoning about programs. What you need if you think of this ``bessermachen'' are the exceptions described in Section \ref{sec:TaggedValues}.

It should be noted that not only users can sit comfortably one step away and see a caller being killed by "[[ bottom ]]". Also computers can do that. In the Logiweb machine described in Section \ref{sec:Interaction}, a handler could use its interface to the outside world to look into the machine itself and inspect the fate of a subordinate process.

\end{statements}



" ]"\section{Tagged values}\label{sec:TaggedValues}"[ "

\subsection{Tags}\label{sec:Tags}

\index{tagged value}\index{value, tagged}\intro{Tagged values} have form "[[ t LazyPair v ]]" where "[[ t ]]" is a \indexintro{tag} which identifies the type of the value and "[[ v ]]" represents the value itself.

Tags have form "[[ r Pair i ]]" where "[[ r ]]" and "[[ i ]]" are untagged naturals. We shall refer to "[[ r ]]" and "[[ i ]]" as the \indexintro{reference} and \indexintro{index} of the tag, respectively.

The reference of a tag is supposed to be either zero or to be the reference of a Logiweb page. The former case is used for the \index{predefined type}\index{type, predefined}\intro{predefined} types listed later. Individual users who want to introduce their own types should use tags of form "[[ r Pair i ]]" where "[[ r ]]" is the reference of a Logiweb page they have published.

The predefined types are: \index{Boolean type}\index{type, boolean}\intro{Booleans}, \index{integer type}\index{type, integer}\intro{integers}, \index{pair type}\index{type, pair}\intro{pairs}, \index{exception type}\index{type, exception}\intro{exceptions}, and \index{map type}\index{type, map}\intro{maps}. Maps are just arbitrary values with a tag on.

The tags of the predefined types are:

\begin{statements}

\item "[[ define value of BoolTag as Zero Pair Zero end define ]]"

\item "[[ define value of IntTag as Zero Pair One end define ]]"

\item "[[ define value of PairTag as Zero Pair Two end define ]]"

\item "[[ define value of ExTag as Zero Pair Three end define ]]"

\item "[[ define value of MapTag as Zero Pair Four end define ]]"

\end{statements}



\subsection{Tag querying}\label{sec:TagQuerying}

\begin{statements}

\item "[[ define value of x Tag as x Head Head TheNat Pair x Head Tail TheNat end define ]]"

\item "[[ define value of x BoolP as x Tag Equal BoolTag end define ]]"

\item "[[ define value of x IntP as x Tag Equal IntTag end define ]]"

\item "[[ define value of x PairP as x Tag Equal PairTag end define ]]"

\item "[[ define value of x ExP as x Tag Equal ExTag end define ]]"

\item "[[ define value of x MapP as x Tag Equal MapTag end define ]]"

\item "[[ define value of x ObjectP as Not ( x BoolP Or x IntP Or x PairP Or x ExP Or x MapP ) end define ]]"

\end{statements}



\subsection{Guards}

\begin{statements}

\item "[[ optimized define value of x is val : y as If x norm ExP then x else y end define ]]"

\item "[[ optimized define value of x .then. y as If x norm ExP then x else y end define ]]"

\item "[[ optimized define value of x is bool : y as x is val : y is val : If x norm BoolP then y else exception end define ]]"

\item "[[ optimized define value of x is int : y as x is val : y is val : If x norm IntP then y else exception end define ]]"

\item "[[ optimized define value of x is pair : y as x is val : y is val : If x norm PairP then y else exception end define ]]"

\item "[[ optimized define value of x is map : y as x is val : y is val : If x norm MapP then y else exception end define ]]"

\item "[[ optimized define value of x is object : y as x is val : y is val : If x norm ObjectP then y else exception end define ]]"

\end{statements}



\subsection{Normalization}\label{sec:Normalization}

\begin{statements}

\item "[[ optimized define value of x norm as newline

If x BoolP then x TheBool else newline

If x IntP then int ( x Tail ) else newline

If x PairP then x Tail Head :: x Tail Tail else newline

If x ExP then x Tail raise else newline

If x MapP then map ( x Tail ) else newline

x Tag Pair x Tail norm end define ]]"

\item "[[ optimized define value of norm x as x norm end define ]]"

\end{statements}



\subsection{Booleans}\label{sec:OperationsOnBooleans}

\begin{statements}

\item "[[ optimized define value of x boolp as x is val : x BoolP end define ]]"

\item "[[ optimized define value of if x then y else z as x is val : If norm x then y else z end define ]]"

\item "[[ optimized define value of .not. x as norm x is val : if x then false else true end define ]]"

\item "[[ optimized define value of notnot x as norm x is val : if x then true else false end define ]]"

\item "[[ optimized define value of x .and. y as If x norm then y norm else x norm end define ]]"

\item "[[ optimized define value of x .or. y as if x norm then true else y norm end define ]]"

\item "[[ optimized define value of x = y as norm x is val : y is val : equal1 ( x norm , y norm ) end define ]]"

\item "[[ define value of equal1 ( x , y ) as newline

if x boolp then x Equal y else newline

if x intp then x Equal y else newline

if x pairp then y pairp .and. x head = y head .and. x tail = y tail else newline

if x mapp then y mapp else newline

x Tag Equal y Tag .and. x Tail = y Tail end define ]]"

\item "[[ define value of x != y as norm x is val : y is val : .not. x = y end define ]]"

\item "[[ define value of x truep as x is val : x boolp .and. notnot x end define ]]"

\item "[[ define value of x falsep as x is val : x boolp .and. .not. x end define ]]"

\end{statements}



\subsection{Integers}\label{sec:Integers}

\begin{statements}

\item "[[ optimized define value of x intp as norm x is val : x IntP end define ]]"

\item "[[ define value of int ( x ) as TheInt ( x Head TheBool , x Tail TheNat ) end define ]]"

\item "[[ define value of PlusTag x as TheInt ( true , x ) end define ]]"

\item "[[ define value of MinusTag x as TheInt ( false , x ) end define ]]"

\item "[[ define value of x Sign as x Tail Head end define ]]"

\item "[[ define value of x Mag as x Tail Tail end define ]]"

\item "[[ optimized define value of + x as norm x is val : x is int : x end define ]]"

\item "[[ optimized define value of +x as + x end define ]]"

\end{statements}



\subsection{Integer addition}\label{sec:IntegerAddition}

\begin{statements}

\item "[[ define value of TheInt ( s , v ) as IntTag Pair ( s Or v ) Pair v end define ]]"

\item "[[ optimized define value of x + y as norm x is val : y is val : plus1 ( x norm , y norm ) end define ]]"

\item "[[ define value of plus1 ( x , y ) as x is int : y is int : plus2 ( x Sign , y Sign , x Mag , y Mag ) end define ]]"

\item "[[ define value of plus2 ( s , t , x , y ) as

s Select ""; x>0

t Select ""; x>0, y>0

PlusTag x Plus y

else ""; x>0, y<0

x LT y Select ""; x>0, y<0, |x|<|y|

MinusTag y Minus x

else ""; x>0, y<0, |x|>|y|

PlusTag x Minus y end select end select

else ""; x<0

t Select ""; x<0, y>0

x LT y Select ""; x<0, y>0, |x|<|y|

PlusTag y Minus x

else ""; x<0, y>0, |x|>|y|

MinusTag x Minus y end select

else ""; x<0, y<0

MinusTag x Plus y end select end select end define ]]"

\end{statements}



\subsection{Integer subtraction}\label{sec:IntegerSubtraction}

\begin{statements}

\item "[[ optimized define value of - x as norm x is val : minus1 ( x norm ) end define ]]"

\item "[[ optimized define value of -x as - x end define ]]"

\item "[[ define value of minus1 ( x ) as x is int : minus2 ( x Sign , x Mag ) end define ]]"

\item "[[ define value of minus2 ( s , x ) as TheInt ( Not s , x ) end define ]]"

\item "[[ optimized define value of x - y as norm x is val : y is val : x + - y end define ]]"

\end{statements}



\subsection{Integer multiplication}\label{sec:IntegerMultiplication}

\begin{statements}

\item "[[ optimized define value of x * y as norm x is val : y is val : times1 ( x norm , y norm ) end define ]]"

\item "[[ define value of times1 ( x , y ) as x is int : y is int : times2 ( x Sign , y Sign , x Mag , y Mag ) end define ]]"

\item "[[ define value of times2 ( s , t , x , y ) as TheInt ( s Iff t , x Times y ) end define ]]"

\end{statements}



\subsection{Integer comparison}\label{sec:IntegerComparison}

\begin{statements}

\item "[[ optimized define value of x < y as norm x is val : y is val : x is int : y is int : lt1 ( x norm , y norm ) end define ]]"

\item "[[ define value of lt1 ( x , y ) as lt2 ( x Sign , y Sign , x Mag , y Mag ) end define ]]"

\item "[[ define value of lt2 ( s , t , x , y ) as

s Select ""; x>0

t Select ""; x>0, y>0

x LT y

else ""; x>0, y<0

false end select

else ""; x<0

t Select ""; x<0, y>0

true

else ""; x<0, y<0

y LT x end select end select end define ]]"

\item "[[ optimized define value of x > y as norm x is val : y is val : x is int : y is int : y < x end define ]]"

\item "[[ optimized define value of x <= y as norm x is val : y is val : x is int : y is int : .not. x > y end define ]]"

\item "[[ optimized define value of x >= y as norm x is val : y is val : x is int : y is int : .not. x < y end define ]]"

\end{statements}



\subsection{Integer construction}\label{sec:IntegerConstruction}

An integer like "[[ %% %1 %2 %3 ]]" can be expressed as an invisible zero followed by three suffix operators "[[ x %1 ]]", "[[ x %2 ]]", and "[[ x %3 ]]". The suffix operators multiply "[[ x ]]" by ten and add one, two, and three, respectively.

\begin{statements}

\item "[[ optimized define value of Base as norm PlusTag Ten end define ]]"

\item "[[ optimized define value of %% as norm PlusTag Zero end define ]]"

Invisible zero.

\item "[[ optimized define value of x %0 as norm x is val : x * Base end define ]]"

\item "[[ optimized define value of x %1 as norm x is val : x * Base + PlusTag One end define ]]"

\item "[[ optimized define value of x %2 as norm x is val : x * Base + PlusTag Two end define ]]"

\item "[[ optimized define value of x %3 as norm x is val : x * Base + PlusTag Three end define ]]"

\item "[[ optimized define value of x %4 as norm x is val : x * Base + PlusTag Four end define ]]"

\item "[[ optimized define value of x %5 as norm x is val : x * Base + PlusTag Five end define ]]"

\item "[[ optimized define value of x %6 as norm x is val : x * Base + PlusTag Six end define ]]"

\item "[[ optimized define value of x %7 as norm x is val : x * Base + PlusTag Seven end define ]]"

\item "[[ optimized define value of x %8 as norm x is val : x * Base + PlusTag Eight end define ]]"

\item "[[ optimized define value of x %9 as norm x is val : x * Base + PlusTag Nine end define ]]"

\item "[[ define value of 0 as norm %% %0 end define ]]"

\item "[[ define value of 1 as norm %% %1 end define ]]"

\item "[[ define value of 2 as norm %% %2 end define ]]"

\item "[[ define value of 3 as norm %% %3 end define ]]"

\item "[[ define value of 4 as norm %% %4 end define ]]"

\item "[[ define value of 5 as norm %% %5 end define ]]"

\item "[[ define value of 6 as norm %% %6 end define ]]"

\item "[[ define value of 7 as norm %% %7 end define ]]"

\item "[[ define value of 8 as norm %% %8 end define ]]"

\item "[[ define value of 9 as norm %% %9 end define ]]"

\end{statements}



\subsection{Logical operations on integers}

\begin{statements}

\item "[[ optimized define value of evenp ( x ) as norm x is val : x is int : x Mag Head TheBool end define ]]"

\item "[[ define value of oddp ( x ) as norm x is val : x is int : .not. evenp ( x ) end define ]]"

\item "[[ optimized define value of half ( x ) as norm x is val : x is int : norm If x Sign then PlusTag x Mag Tail else MinusTag ( x Plus One ) Mag Tail end define ]]"

\item "[[ define value of small ( x ) as norm x is val : norm x is int : -1 <= x .and. x <= 0 end define ]]"

\item "[[ define value of double ( b , i ) as norm b is val : i is val : b is bool : i is int : if b then 1 + 2 * i else 2 * i end define ]]"

\item "[[ optimized define value of lognot ( x ) as norm x is val : x is int : -1 - x end define ]]"

\item "[[ optimized define value of logior ( x , y ) as norm x is val : y is val : x is int : y is int : newline

if x = -1 then -1 else if y = -1 then -1 else newline

if x = 0 then y else if y = 0 then x else double ( oddp ( x ) .or. oddp ( y ) , logior ( half ( x ) , half ( y ) ) ) end define ]]"

\item "[[ optimized define value of logxor ( x , y ) as norm x is val : y is val : x is int : y is int : newline

if x = -1 then lognot ( y ) else if y = -1 then lognot ( x ) else newline

if x = 0 then y else if y = 0 then x else double ( oddp ( x ) != oddp ( y ) , logxor ( half ( x ) , half ( y ) ) ) end define ]]"

\item "[[ optimized define value of logand ( x , y ) as norm x is val : y is val : x is int : y is int : newline

if x = -1 then y else if y = -1 then x else newline

if x = 0 then 0 else if y = 0 then 0 else double ( oddp ( x ) .and. oddp ( y ) , logand ( half ( x ) , half ( y ) ) ) end define ]]"

\item "[[ optimized define value of logeqv ( x , y ) as norm x is val : y is val : x is int : y is int : lognot ( logxor ( x , y ) ) end define ]]"

\item "[[ optimized define value of lognand ( x , y ) as norm x is val : y is val : x is int : y is int : lognot ( logand ( x , y ) ) end define ]]"

\item "[[ optimized define value of lognor ( x , y ) as norm x is val : y is val : x is int : y is int : lognot ( logior ( x , y ) ) end define ]]"

\item "[[ optimized define value of logandc1 ( x , y ) as norm x is val : y is val : x is int : y is int : logand ( lognot ( x ) , y ) end define ]]"

\item "[[ optimized define value of logandc2 ( x , y ) as norm x is val : y is val : x is int : y is int : logand ( x , lognot ( y ) ) end define ]]"

\item "[[ optimized define value of logorc1 ( x , y ) as norm x is val : y is val : x is int : y is int : logior ( lognot ( x ) , y ) end define ]]"

\item "[[ optimized define value of logorc2 ( x , y ) as norm x is val : y is val : x is int : y is int : logior ( x , lognot ( y ) ) end define ]]"

\item "[[ optimized define value of logtest ( x , y ) as norm x is val : y is val : x is int : y is int : logand ( x , y ) != 0 end define ]]"

\item "[[ optimized define value of ash ( i , c ) as norm i is val : c is val : i is int : c is int : if c >= 0 then ash+ ( i , c ) else ash- ( i , - c ) end define ]]"

\item "[[ define value of ash+ ( i , c ) as norm i is val : c is val : i is int : c is int : if c = 0 then i else ash+ ( 2 * i , c - 1 ) end define ]]"

\item "[[ define value of ash- ( i , c ) as norm i is val : c is val : i is int : c is int : if c = 0 then i else ash- ( half ( i ) , c - 1 ) end define ]]"

\item "[[ optimized define value of logbitp ( x , i ) as norm x is val : i is val : x is int : i is int : if x < 0 then exception else oddp ( ash ( i , - x ) ) end define ]]"

\item "[[ optimized define value of logcount ( x ) as norm x is val : x is int : if x < 0 then logcount1 ( lognot ( x ) ) else logcount1 ( x ) end define ]]"

\item "[[ define value of logcount1 ( x ) as norm x is val : x is int : if x = 0 then 0 else logcount1 ( half ( x ) ) + if evenp ( x ) then 0 else 1 end define ]]"

\item "[[ optimized define value of integer-length ( x ) as norm x is val : x is int : if small ( x ) then 0 else 1 + integer-length ( half ( x ) ) end define ]]"

\end{statements}



\subsection{Vector operations}

A byte is an integer in the range 0..255. We shall represent sequences of bytes as \index{vector}\emph{vectors} as follows: Given a sequence of bytes, add the number "[[ 1 ]]" at the end of the sequence, then interpret the sequence little endian base 256. In that way, sequences of bytes are represented by cardinals (positive integers). As an example, the sequence "[[ << 65 ,, 66 >> ]]" is represented by the number "[[ 65 + 256 * 66 + 256 * 256 * 1 ]]".

Strings like "[[ !"AB" ]]" are treated as vectors. The value of "[[ !"AB" ]]" is "[[ 65 + 256 * 66 + 256 * 256 * 1 ]]" because A and B have unicode 65 and 66, respectively. Strings are encoded using UTF-8 so strings are always sequences of bytes even when characters in the strings have unicodes above 255.

If a number like "[[ 65 + 256 * 66 + 256 * 256 * 2 ]]" is interpreted as a vector, it represents the vector consisting of the bytes 65 and 66. Hence, when translating integers to vectors, the stop byte can have any, non-zero value.

We define the following functions on vectors:

\begin{statements}

\item "[[ vector ( x ) ]]". Normalize the vector (change the stop byte to a one-byte).

\item "[[ vector-suffix ( x , b ) ]]". Return the subvector beginning at byte number "[[ b ]]" (where the first byte is byte number zero): "[[ vector-suffix ( !"ABCD" , 2 ) = !"CD" ]]".

\item "[[ vector-prefix ( x , e ) ]]". Return the subvector ending before byte number "[[ e ]]": "[[ vector-prefix ( !"ABCD" , 2 ) = !"AB" ]]".

\item "[[ vector-subseq ( x , b , e ) ]]". Return the subvector beginning at "[[ b ]]" and ending before "[[ e ]]": "[[ vector-subseq ( !"ABCD" , 1 , 3 ) = !"BC" ]]".

\item "[[ vector-length ( x ) ]]". Return the length of the vector: "[[ vector-length ( !"ABCD" ) = 4 ]]".

\item "[[ vector-index ( x , i ) ]]". Return the i'th byte: "[[ vector-index ( !"ABCD" , 1 ) = 66 ]]".

\item "[[ eager define vector-head ( x ) as vector-index ( x , 0 ) end define ]]".

\item "[[ eager define vector-tail ( x ) as vector-suffix ( x , 1 ) end define ]]".

\end{statements}

We shall represent byte sequences in four ways:

\begin{description}

\item[byte*] A list of bytes.

\item[vector] An integer which encodes the list little endian base 256 with a stop byte at the end.

\item[bt] A \index{byte tree}\index{tree, byte}\emph{byte tree}, i.e.\ a structure built up from bytes and conses. To convert it to a sequence, scan the tree root to leaf, left to right, and collect all bytes found. Ignore anything which is not a byte.

\item[t] A \index{vector tree}\index{tree, vector}\emph{byte vector}, i.e.\ a structure built up from vectors and conses. To convert it to a sequence, scan the tree root to leaf, left to right, and append all vectors (integers) found. Ignore anything which is not a vector.

\end{description}

\noindent The following functions convert between the representations. Examples:

\[\begin{array}{lll}

"[ vector2byte* ( !"ABC" ) ]" & = & "[ << 65 ,, 66 ,, 67 >> ]" \\

"[ bt2byte* ( ( 65 :: 66 ) :: - 1 :: 256 :: true :: 67 :: false :: 68 ) ]" & = & "[ << 65 ,, 66 ,, 67 ,, 68 >> ]" \\

"[ bt2vector ( ( 65 :: 66 ) :: - 1 :: 256 :: true :: 67 :: false :: 68 ) ]" & = & "[ !"ABCD" ]" \\

"[ vt2byte* ( ( !"A" :: !"BC" ) :: - 1 :: !"". :: false :: !"D" ) ]" & = & "[ << 65 ,, 66 ,, 67 ,, 68 >> ]" \\

"[ vt2vector ( ( !"A" :: !"BC" ) :: - 1 :: !"". :: false :: !"D" ) ]" & = & "[ !"ABCD" ]" \\

\end{array}\]

\noindent In the implementations, care is taken to make the functions tail recursive. Furthermore, whenever tail recursion had to favor either recursion in the head or in the tail of pairs, recursion in the tail has been favored. For that reason, the functions can handle very long lists without stack overflow. This is done at the cost of having to reverse lists occasionally.

\noindent The definitions read:

\begin{statements}

\item "[[ define value of vector-mask as norm %% %2 %5 %5 end define ]]"

\item "[[ define value of octet-base as norm %% %2 %5 %6 end define ]]"

\item "[[ optimized define value of vector-empty ( x ) as norm x is val : x <= vector-mask end define ]]"

\item "[[ define value of vector-head1 ( x ) as norm x is val : logand ( vector-mask , x ) end define ]]"

\item "[[ define value of vector-tail1 ( x ) as norm x is val : ash ( x , -8 ) end define ]]"

\item "[[ define value of vector-cons ( x , y ) as norm x is val : y is val : logior ( x , ash ( y , 8 ) ) end define ]]"

\item "[[ optimized define value of vector ( x ) as norm x is val : if vector-empty ( x ) then "". else vector-cons ( vector-head1 ( x ) , vector ( vector-tail1 ( x ) ) ) end define ]]"

\item "[[ optimized define value of vector-norm ( x ) as norm x is val : if x < 0 then true else if integer-length ( x ) mod 8 = 1 then x else true end define ]]"

\item "[[ optimized define value of vector-suffix ( x , b ) as norm x is val : b is val : if b <= 0 then vector ( x ) else vector-suffix ( vector-tail1 ( x ) , b - 1 ) end define ]]"

\item "[[ optimized define value of vector-prefix ( x , e ) as norm x is val : e is val : e is int : if vector-empty ( x ) .or. e <= 0 then "". else vector-cons ( vector-head1 ( x ) , vector-prefix ( vector-tail1 ( x ) , e - 1 ) ) end define ]]"

\item "[[ optimized define value of vector-subseq ( x , b , e ) as norm x is val : b is val : e is val : if b <= 0 then vector-prefix ( x , e ) else vector-subseq ( vector-tail1 ( x ) , b - 1 , e - 1 ) end define ]]"

\item "[[ optimized define value of vector-length ( x ) as norm x is val : if vector-empty ( x ) then 0 else 1 + vector-length ( vector-tail1 ( x ) ) end define ]]"

\item "[[ optimized define value of vector-index ( x , i ) as if i < 0 .or. vector-length ( x ) <= i then exception else vector-head1 ( vector-suffix ( x , i ) ) end define ]]"

\item "[[ optimized define value of vector2byte* ( x ) as norm x is val : vector2byte*1 ( x , true ) end define ]]"

\item "[[ define value of vector2byte*1 ( x , r ) as norm x is val : r is val : newline

if vector-empty ( x ) then reverse ( r ) else newline

vector2byte*1 ( vector-tail1 ( x ) , vector-head1 ( x ) :: r ) end define ]]"

\item "[[ optimized define value of vector2vector* ( x ) as norm x is val : vector2vector*1 ( x , true ) end define ]]"

\item "[[ define value of vector2vector*1 ( x , r ) as norm x is val : r is val : newline

if vector-empty ( x ) then reverse ( r ) else newline

vector2vector*1 ( vector-tail1 ( x ) , vector-head1 ( x ) + octet-base :: r ) end define ]]"

\item "[[ optimized define value of bt2byte* ( x ) as norm x is val : reverse ( bt2byte*1 ( x , true ) ) end define ]]"

\item "[[ define value of bt2byte*1 ( x , r ) as norm x is val : r is val : newline

if x pairp then bt2byte*1 ( x tail , bt2byte*1 ( x head , r ) ) else newline

if x intp .and. 0 <= x .and. x <= vector-mask then x :: r else r end define ]]"

\item "[[ optimized define value of bt2vector* ( x ) as norm x is val : reverse ( bt2vector*1 ( x , true ) ) end define ]]"

\item "[[ define value of bt2vector*1 ( x , r ) as norm x is val : r is val : newline

if x pairp then bt2vector*1 ( x tail , bt2vector*1 ( x head , r ) ) else newline

if x intp .and. 0 <= x .and. x <= vector-mask then x + octet-base :: r else r end define ]]"

\item "[[ optimized define value of bt2vector ( x ) as norm x is val : revbyte*2vector ( bt2byte*1 ( x , true ) , !"". ) end define ]]"

\item "[[ define value of revbyte*2vector ( x , r ) as norm x is val : r is val : newline

if x atom then r else newline

revbyte*2vector ( x tail , vector-cons ( x head , r ) ) end define ]]"

Reverse the list "[[ x ]]" of bytes, revappend them to the vector "[[ r ]]", and return them as a vector.

\item "[[ define value of vector-revappend ( x , y ) as norm x is val : y is val : newline

if vector-empty ( x ) then y else newline

vector-revappend ( vector-tail1 ( x ) , vector-head1 ( x ) :: y ) end define ]]"

Convert the vector "[[ x ]]" to a sequence of bytes and revappend it to the sequence "[[ y ]]" of bytes.

\item "[[ optimized define value of vt2byte* ( x ) as norm x is val : reverse ( vt2byte*1 ( x , true ) ) end define ]]"

\item "[[ define value of vt2byte*1 ( x , r ) as norm x is val : r is val : newline

if x pairp then vt2byte*1 ( x tail , vt2byte*1 ( x head , r ) ) else newline

if x intp then vector-revappend ( x , r ) else r end define ]]"

\item "[[ define value of vector-revappend1 ( x , y ) as norm x is val : y is val : newline

if vector-empty ( x ) then y else newline

vector-revappend1 ( vector-tail1 ( x ) , vector-head1 ( x ) + octet-base :: y ) end define ]]"

Convert the vector "[[ x ]]" to a sequence of bytes and revappend it to the sequence "[[ y ]]" of bytes.

\item "[[ optimized define value of vt2vector* ( x ) as norm x is val : reverse ( vt2vector*1 ( x , true ) ) end define ]]"

\item "[[ define value of vt2vector*1 ( x , r ) as norm x is val : r is val : newline

if x pairp then vt2vector*1 ( x tail , vt2vector*1 ( x head , r ) ) else newline

if x intp then vector-revappend1 ( x , r ) else r end define ]]"

\item "[[ optimized define value of vt2vector ( x ) as norm x is val : revbyte*2vector ( vt2byte*1 ( x , true ) , !"". ) end define ]]"

\end{statements}



\subsection{Division}

The division routines in the following return quotient/remainder pairs of form "[[ q :: r ]]" where "[[ q ]]" is the quotient and "[[ r ]]" is the remainder. When dividing the dividend "[[ x ]]" by the divisor "[[ y ]]", the resulting quotient/remainder pair satisfies "[[ x = q * y + r ]]". The differences between the various kinds of divisions lie in the direction in which the quotient is rounded and, hence, the possible interval for the remainder.

There is general agreement about how negative dividends "[[ x ]]" should be handled. But there is no similar agreement about the handling of negative divisors "[[ y ]]". For that reason, we simply proclaim division by negative numbers to be as undefined as division by zero.

We now define four division routines, "[[ floor ( x , y ) ]]", "[[ ceiling ( x , y ) ]]", "[[ truncate ( x , y ) ]]", and "[[ round ( x , y ) ]]", one for each kind of rounding defined by the IEEE floating point standard. These division routines raise an exception in case of division by zero or division by a negative number. The names of the division routines are inspired by Common Lisp, c.f.\ the Common Lisp Hyperspec, which is available on the World Wide Web.

We consider "[[ floor ( x , y ) ]]", which does rounding towards minus infinity, to be the most useful integer division routine, and introduce "[[ x div y ]]" and "[[ x mod y ]]" to denote the quotient and remainder, respectively, returned by "[[ floor ( x , y ) ]]".

To define division, we first define restricted forms of division "[[ floor1 ( x , y ) ]]", "[[ ceiling1 ( x , y ) ]]", and "[[ round1 ( x , y ) ]]" which can handle positive arguments. We also introduce a construct "[[ reverse quotient ( p ) ]]" for changing the sign of both quotient and remainder in a quotient/remainder pair. The restricted division routines may loop indefinitely when the input values are out of range.

\begin{statements}

\item "[[ define value of floor1 ( x , y ) as newline

if x < y then 0 :: x else newline

LET floor1 ( x , 2 * y ) BE z IN newline

if z tail < y then 2 * z head :: z tail else 2 * z head + 1 :: z tail - y end define ]]"

Divide the natural "[[ x ]]" by the positive integer "[[ y ]]" with rounding towards minus infinity.

\item "[[ define value of ceiling1 ( x , y ) as newline

LET floor1 ( x , y ) BE z IN newline

if z tail = 0 then z else z head + 1 :: z tail - y end define ]]"

Divide the positive integer "[[ x ]]" by the positive integer "[[ y ]]" with rounding towards plus infinity and return af pair "[[ q :: r ]]" of quotient "[[ d ]]" and remainder "[[ r ]]".

\item "[[ define value of round1 ( x , y ) as newline

LET floor1 ( x , y ) BE z IN newline

if z tail * 2 < y then z else newline

if z tail * 2 > y then z head + 1 :: z tail - y else newline

if evenp ( z head ) then z else newline z head + 1 :: z tail - y end define ]]"

Divide the natural "[[ x ]]" by the positive integer "[[ y ]]" with rounding towards nearest/even, c.f.\ the IEEE floating point standard or the Common Lisp Hyperspec.

\item "[[ define value of reverse quotient ( p ) as - p head :: - p tail end define ]]"

Negate both quotient and remainder of a quotient/remainder pair.

\item "[[ optimized define value of truncate ( x , y ) as newline

if y <= 0 then exception else newline

if 0 <= x then floor1 ( x , y ) else newline

reverse quotient ( floor1 ( - x , y ) ) end define ]]"

Divide the integer "[[ x ]]" by the positive integer "[[ y ]]" with rouding towards zero.

\item "[[ optimized define value of floor ( x , y ) as newline

if y <= 0 then exception else newline

if 0 <= x then floor1 ( x , y ) else newline

reverse quotient ( ceiling1 ( - x , y ) ) end define ]]"

Divide the integer "[[ x ]]" by the positive integer "[[ y ]]" with rouding towards minus infinity.

\item "[[ optimized define value of ceiling ( x , y ) as newline

if y <= 0 then exception else newline

if 0 < x then ceiling1 ( x , y ) else newline

reverse quotient ( floor1 ( - x , y ) ) end define ]]"

Divide the integer "[[ x ]]" by the positive integer "[[ y ]]" with rouding towards plus infinity.

\item "[[ optimized define value of round ( x , y ) as newline

if y <= 0 then exception else newline

if 0 < x then round1 ( x , y ) else newline

reverse quotient ( round1 ( - x , y ) ) end define ]]"

Divide the integer "[[ x ]]" by the positive integer "[[ y ]]" with rouding towards nearest/even, c.f.\ the IEEE floating point standard or the Common Lisp Hyperspec.

\item "[[ optimized define value of x div y as floor ( x , y ) head end define ]]"

\item "[[ optimized define value of x mod y as floor ( x , y ) tail end define ]]"

\end{statements}



\subsection{Pairs}\label{sec:Pairs}

\begin{statements}

\item "[[ optimized define value of x pairp as norm x is val : x PairP end define ]]"

\item "[[ define value of a atom as norm a is val : norm a is val : .not. a pairp end define ]]"

\item "[[ optimized define value of x :: y as x is val : y is val : PairTag Pair x norm Pair y norm end define ]]"

\item "[[ optimized define value of x head as norm x is val : if x atom then x norm else x norm Tail Head end define ]]"

\item "[[ optimized define value of x tail as norm x is val : if x atom then x norm else x norm Tail Tail end define ]]"

\item "[[ define value of append ( x , y ) as norm x is val : y is val : newline

if x atom then y else x head :: append ( x tail , y ) end define ]]"

\item "[[ define value of reverse ( x ) as norm x is val : revappend ( x , true ) end define ]]"

\item "[[ define value of revappend ( x , y ) as norm x is val : y is val : newline

if x atom then y else revappend ( x tail , x head :: y ) end define ]]"

\item "[[ define value of nth ( n , x ) as norm n is val : x is val : newline

if n <= 0 then x head else nth ( n - 1 , x tail )

end define ]]"

\item "[[ eager define length ( x ) as length1 ( x , 0 ) end define ]]".

Compute length of list.

\item "[[ eager define length1 ( x , r ) as if x atom then r else length1 ( x tail , r + 1 ) end define ]]".

Compute the sum of the integer "[[ r ]]" and the length of the list "[[ x ]]".

\item "[[ eager define list-prefix ( l , n ) as newline

if n = 0 .or. l atom then true else l head :: list-prefix ( l tail , n - 1 ) end define ]]"

Return the first "[[ n ]]" elements of the list "[[ l ]]".

\item "[[ eager define list-suffix ( l , n ) as newline

if n = 0 then l else list-suffix ( l tail , n - 1 ) end define ]]"

Remove the first "[[ n ]]" elements from the list "[[ l ]]".

\end{statements}



\subsection{Exceptions}\label{sec:Exceptions}

\begin{statements}

\item "[[ optimized define value of x raise as x is val : ExTag Pair x norm end define ]]"

\item "[[ optimized define value of exception as norm true raise end define ]]"

\item "[[ optimized define value of catch ( x ) as Catch ( x norm ) end define ]]"

\item "[[ optimized define value of x catch as Catch ( x norm ) end define ]]"

\item "[[ define value of Catch ( x ) as If x ExP then true :: x Tail else false :: x end define ]]"

\end{statements}



\subsection{Maps}\label{sec:TaggedMaps}

\begin{statements}

\item "[[ optimized define value of x mapp as norm x is val : x MapP end define ]]"

\item "[[ optimized define value of map ( x ) as MapTag LazyPair x end define ]]"

\item "[[ optimized define value of x catching maptag as map ( x norm ) end define ]]"

\item "[[ optimized define value of x maptag as norm x is val : x catching maptag end define ]]"

\item "[[ optimized define value of x untag as norm x is val : x is map : x Tail norm end define ]]"

\item "[[ optimized define value of x apply y as norm x is val : y is val : x is map : y is map : map ( x Tail ' y Tail ) end define ]]"

\item "[[ optimized define value of x root as norm x is val : x is map : x Tail TheBool end define ]]"

\end{statements}



\subsection{Objects}\label{sec:Objects}

\begin{statements}

\item "[[ optimized define value of x objectp as norm x is val : x ObjectP end define ]]"

\item "[[ optimized define value of object ( x ) as norm x is val : Object ( x head head , x head tail , x tail ) end define ]]"

\item "[[ define value of Object ( x , y , z ) as x is int : y is int : z is val : if x < 0 .or. y < 0 .or. x = 0 .and. y <= %% %4 then exception else ( x Mag Pair y Mag ) Pair z end define ]]"

\item "[[ optimized define value of destruct ( x ) as norm x is val : x is object : ( ( PlusTag ( x Head Head ) :: PlusTag ( x Head Tail ) ) :: x Tail ) norm end define ]]"

\end{statements}



" ]"\section{Evaluation}"[ "

\subsection{Let construct}

"[[ optimized define value of LET x BE y as x is val : y ' x end define ]]"

"[[ proclaim x IN y as "lambda" end proclaim ]]"



\subsection{Simple accessors}

\begin{statements}

\item "[[ define value of x zeroth as norm x is val : x head end define ]]"

\item "[[ define value of x first as norm x is val : x tail zeroth end define ]]"

\item "[[ define value of x second as norm x is val : x tail first end define ]]"

\item "[[ define value of x third as norm x is val : x tail second end define ]]"

\item "[[ define value of x fourth as norm x is val : x tail third end define ]]"

\item "[[ define value of x fifth as norm x is val : x tail fourth end define ]]"

\item "[[ define value of x sixth as norm x is val : x tail fifth end define ]]"

\item "[[ define value of x seventh as norm x is val : x tail sixth end define ]]"

\item "[[ define value of x eighth as norm x is val : x tail seventh end define ]]"

\item "[[ define value of x ninth as norm x is val : x tail eighth end define ]]"

\end{statements}



\subsection{Representation of terms}\label{sec:RepresentationOfTerms}

Section \ref{sec:Proclamations} proclaimed "[[ quote x end quote ]]" to denote \indexintro{quoting}. The value of "[[ quote x end quote ]]" is a structure which represents the term "[[ x ]]". As an example, the value of "[[ quote u + 2 end quote ]]" represents the plus construct applied to the "[[ u ]]" construct and the "[[ 2 ]]" construct.

As mentioned in Section \ref{sec:AspectDeclarations}, every Logiweb construct is represented by a \indexintro{reference} and an \indexintro{index}. The reference is a world-wide unique natural number which identifies the \index{page, home}\indexintro{home page} of the construct, i.e.\ the page on which the construct is introduced. The index is a natural number which distinguishes the construct from the other constructs introduced on that home page.

The value of "[[ quote u + 2 end quote ]]" has form "[[[ ( r :: i :: d ) :: x :: y :: true ]]]" where "[[ r ]]" and "[[ i ]]" are the reference and index, respectively, of the plus construct. "[[ x ]]" and "[[ y ]]" represent the terms "[[ u ]]" and "[[ 2 ]]" respectively. "[[ d ]]" is \index{information, debugging}\index{debugging information}.

The purpose of debugging information is to allow users to locate the source of errors. When a user receives an error message saying e.g.\ that a particular proof is in error, then the error message is likely to contain a term from the macro expanded version of the page. On the present page, the debugging information of a term indicates the location a term had before macro expansion. Users have control over the debugging information through the unpacking and macro expansion machinery.

On the present page, the debugging information of a term has form "[[[ ( p _ { n } :: *** :: p _ { 1 } :: r prime :: true ) :: true ]]]" where "[[ r prime ]]" is the reference of the page on which the term occurs and "[[ p _ { n } ,, ... ,, p _ { 1 } ]]" indicate that before macro expansion, the term was subtree number "[[ p _ { n } ]]" of subtree number "[[ p _ { n - 1 } ]]" and so on of the root of the page.

Strings are represented in a particular way in that they have form "[[[ ( r :: i :: d ) :: true ]]]" where "[[ r ]]" is zero and "[[ i ]]" is a natural number which represents the string. "[[ i ]]" is constructed thus: write the string as a sequence of bytes using Unicode and UTF-8 encoding (a \indexintro{byte} is a natural number between 0 and 255, inclusive). Then add a byte with value "[[ 1 ]]" at the end. Finally, convert the sequence of bytes to a natural number using little endian radix 256 representation.

On many occasions, there is a need to assign aspects to a page. As an example, Section \ref{sec:Verification} assigns a `claim' aspect to the present page. As another example, Section \ref{sec:MacroExpansion} assigns a `macro' aspect to the present page. Formally, definitions can only assign aspects to constructs and not to pages. That problem is solved by the convention that every page has a \index{construct, page}\indexintro{page construct} which represents the page. The page construct of a page has index zero and aspects of the page construct should be interpretted as aspects of the page. As examples, the "[[ name ]]" and "[[ tex show ]]" aspects of a page symbol define the name of the page expressed in plain text (UTF-8) and \TeX, respectively.

The following constructs allows to access the reference, index, and debugging information of a term "[[ x ]]"

\begin{statements}

\item "[[ define value of x ref as norm x is val : x head head end define ]]"

\item "[[ define value of x idx as norm x is val : x head tail head end define ]]"

\item "[[ define value of x debug as norm x is val : x head tail tail end define ]]"

\end{statements}



\subsection{Tree equality}

\begin{statements}

\item "[[ define value of x t= y as norm x is val : y is val : x ref = y ref .and. x idx = y idx .and. x tail t=* y tail end define ]]" True if the terms "[[ x ]]" and "[[ y ]]" are equal modulo differences in debugging information. As an example, "[[ quote z end quote = quote z end quote ]]" is false because the two instances of "[[ z ]]" occur different places on the page whereas "[[ quote z end quote t= quote z end quote ]]" because the "[[ %% t= %% ]]" operation disregards debugging information.

\item "[[ define value of x t=* y as norm x is val : y is val : if x atom then y atom else if y atom then false else x head t= y head .and. x tail t=* y tail end define ]]" Coordinatewise application of "[[ u t= v ]]" to the lists "[[ x ]]" and "[[ y ]]" of terms.

\item "[[ define value of x r= y as norm x is val : y is val : x ref = y ref .and. x idx = y idx end define ]]" True if the roots of terms "[[ x ]]" and "[[ y ]]" are equal modulo differences in debugging information.

\item "[[ define value of lookup ( x , s , d ) as norm x is val : s is val : d is val : if s atom then d else if x t= s head head then s head tail else lookup ( x , s tail , d ) end define ]]" Look up the term "[[ x ]]" in the stack "[[ s ]]". A \indexintro{stack} is an association list which associates terms to values. When the term "[[ x ]]" is not found in the stack "[[ s ]]", the default "[[ d ]]" is returned.

\item "[[ define value of zip ( x , y ) as norm x is val : y is val : newline

if x atom .or. y atom then true else newline

( x head :: y head ) :: zip ( x tail , y tail ) end define ]]" Zip the list "[[ x ]]" of terms and the list "[[ y ]]" of values into a stack (may of course be used for arbitrary lists).

\end{statements}



\subsection{Arrays}

\begin{statements}

\item "[[ define value of a [[ i ]] as norm a is val : i is val : i is int : array1 ( a , i , 0 ) end define ]]"

\item "[[ define value of array1 ( a , i , x ) as norm a is val : i is val : x is val : i is int : x is int : newline

if a atom then true else newline

if a head intp then if i = a head then a tail else true else newline

array1 ( if logbitp ( x , i ) then a tail else a head , i , x + 1 )

end define ]]"

\item "[[ define value of a [[ i -> v ]] as norm a is val : i is val : v is val : i is int : array2 ( a , i , v , 0 ) end define ]]"

\item "[[ define value of array2 ( a , i , v , x ) as norm a is val : i is val : v is val : x is val : i is int : x is int : newline

if a atom then array3 ( i , v ) else newline

if a head intp then newline

if i = a head then newline

array3 ( i , v ) else newline

if v then a else newline

array5 ( a head , a tail , i , v , x ) else newline

if logbitp ( x , i ) then newline

array4 ( a head , array2 ( a tail , i , v , x + 1 ) ) else newline

array4 ( array2 ( a head , i , v , x + 1 ) , a tail )

end define ]]"

\item "[[ define value of array3 ( i , v ) as norm i is val : v is val : i is int : if v = true then true else i :: v end define ]]"

\item "[[ define value of array4 ( a , b ) as norm a is val : b is val : newline

if a atom then newline

if b atom then true else if b head intp then b else a :: b else newline

if b atom .and. a head intp then a else a :: b end define ]]"

\item "[[ define value of array5 ( i , v , j , w , x ) as norm i is val : v is val : j is val : w is val : x is val : i is int : j is int : x is int : newline

if logbitp ( x , i ) then newline

if logbitp ( x , j ) then newline

true :: array5 ( i , v , j , w , x + 1 ) else newline

( j :: w ) :: ( i :: v ) else newline

if logbitp ( x , j ) then newline

( i :: v ) :: ( j :: w ) else newline

array5 ( i , v , j , w , x + 1 ) :: true end define ]]"

\item "[[ define value of a [[ i => v ]] as norm a is val : i is val : v is val : if i atom then v else a [[ i head -> a [[ i head ]] [[ i tail => v ]] ]] end define ]]"

\item "[[ define value of push ( a , i , v ) as norm a is val : i is val : v is val : a [[ i -> v :: a [[ i ]] ]] end define ]]"

\item "[[ define value of pop ( a , i ) as norm a is val : i is val : a [[ i -> a [[ i ]] tail ]] end define ]]"

\item "[[ define value of get* ( a , i ) as norm a is val : i is val : if i atom then a else get* ( a [[ i head ]] , i tail ) end define ]]"

\item "[[ define value of push* ( a , i , v ) as norm a is val : i is val : v is val : a [[ i => v :: get* ( a , i ) ]] end define ]]"

\item "[[ define value of pop* ( a , i ) as norm a is val : i is val : a [[ i => get* ( a , i ) tail ]] end define ]]"

\item "[[ late eager define array-domain ( x ) as newline

if x atom then true else newline

if x head intp then << x head >> else newline

sort-merge ( array-domain ( x head ) , array-domain ( x tail ) ) end define ]]"

Return the domain of the array "[[ x ]]" sorted in ascending order.

\item "[[ late eager define sort-merge ( x , y ) as newline

if x atom then y else sort-merge1 ( y , x ) end define ]]"

Merge the ascending lists "[[ x ]]" and "[[ y ]]" into a new, ascending list.

\item "[[ late eager define sort-merge1 ( x , y ) as newline

if x atom then y else newline

if x head < y head then newline

x head :: sort-merge1 ( x tail , y ) else newline

y head :: sort-merge1 ( y tail , x ) end define ]]"

Same as "[[ sort-merge ( x , y ) ]]" but assumes "[[ y ]]" to be a pair.

\end{statements}



\subsection{Evaluator}

\begin{statements}

\item "[[ define value of eval ( t , s , c ) as norm t is val : s is val : c is val : newline

LET t ref BE r IN newline

LET t idx BE i IN newline

if r = 0 then i maptag else newline

if i = 0 then if r = c [[ 0 ]] then c maptag else c [[ c [[ 0 ]] ]] [[ "cluster" ]] [[ r ]] maptag else newline

LET c [[ r ]] [[ "code" ]] [[ i ]] BE f IN newline

if f mapp then eval1 ( f , t tail , s , c ) else newline

if f = true then lookup ( t , s , map ( true ) ) else newline

if f = 1 then t first maptag else newline

map ( \ t . \ s . \ c . \ x . eval ( t second , ( t first :: map ( x ) ) :: s , c ) Tail ) apply t maptag apply s maptag apply c maptag

end define ]]"

\item "[[ define value of eval1 ( f , t , s , c ) as norm f is val : t is val : s is val : c is val : f is map : newline

if t atom then f else newline

eval1 ( f apply eval ( t head , s , c ) , t tail , s , c ) end define ]]"

\end{statements}



\subsection{Debugging aids}

\begin{statements}

\item "[[ optimized define value of spy ( x ) as norm x is val : "spy" end define ]]"

\item "[[ optimized define value of trace ( x ) as norm x is val : "trace" end define ]]"

\item "[[ optimized define value of print ( x ) as norm x is val : "print" end define ]]"

\item "[[ optimized define value of timer ( x ) as norm x is val : "timer" end define ]]"

\end{statements}

"[[ spy ( x ) ]]" is faithful to the definition above in that it discards "[[ x ]]" and returns "[[ "spy" ]]". As a side effect, however, it sets a variable named *spy* to the value of "[[ x ]]". It is possible to inspect that variable in several ways: One may ask the Logiweb compiler to print it out using the spy flag. Or one may use the quit flag to enter a read-eval-print loop in which one may issue commands like (spy), (spycd $\ldots$), (spyls $\ldots$), (spy/), (spy..), and (spypwd) to navigate and inspect the value of the *spy* variable. The *spy* variable is set by all test constructs so that if a test case makes the computer loop indefinitely then one has a chance of finding out which one by inspection of the *spy* variable.

"[[ trace ( x ) ]]" is like "[[ spy ( x ) ]]" but prints out the value of "[[ x ]]" to standard output. To get output from a "[[ trace ( x ) ]]", the construct has to be executed, which may happen during testing, macro expansion, custom unpacking, or custom rendering. The easiest way to get output from trace is to include it in a test construct.

"[[ print ( x ) ]]" is like "[[ trace ( x ) ]]" but just dumps the vector tree "[[ x ]]" to standard output as a sequence of bytes. Note the "[[ print ( x ) ]]" does not even append a newline at the end ("[[ println ( x ) ]]" defined later does that). Printing a linefeed (code 10) is supposed to generate the newline sequence of the host operating system.

"[[ timer ( x ) ]]" returns the string ``timer'' and is thus easy to recognize from the other ones. The timer construct is supposed to be used as the "[[ x ]]" in the "[[ x .then. y ]]" construct which discards "[[ x ]]" and returns "[[ y ]]". Whenever "[[ timer ( x ) ]]" is evaluated, the timer associated with "[[ x ]]" starts counting. If no timer is associated with "[[ x ]]", then one is created. The timer counts until a call of "[[ timer ( y ) ]]" which causes the timer associated with "[[ x ]]" to stop and the one associated with "[[ y ]]" to start counting. Just before the Logiweb compiler exits, it prints the values of all timers except the one associated with "[[ true ]]". Hence, "[[ timer ( true ) ]]" effectively stops counting. Note that the active timer keeps counting until the timer values are reported.

\begin{statements}

\item "[[ late eager define x .prog1. y as x end define ]]"

\item "[[ macro define measure ( x , y ) as trace ( x ) .then. timer ( x ) .then. y .prog1. timer ( true ) end define ]]"

\end{statements}



\subsection{Verification}\label{sec:Verification}

\begin{statements}

\item "[[ define claim of base as test1 end define ]]"

\item "[[ define value of x &c y as \ c . x ' c .and. y ' c end define ]]"

\item "[[ define value of test1 as \ c . test2 ( c ) end define ]]"

\item "[[ define value of test2 ( c ) as norm c is val : newline

LET test3 ( c [[ c [[ 0 ]] ]] [[ "expansion" ]] , c ) catch BE p IN newline

if p tail != true then diagnose p tail end diagnose else newline

if p head then show quote "In testsuite: unprocessed exception" end quote end show else newline

spy ( true ) .then. true end define ]]"

\item "[[ define value of diagnose x end diagnose as norm x is val : newline

( quote diagnose x end diagnose end quote ref :: quote diagnose x end diagnose end quote idx :: x debug ) :: x :: true end define ]]"

\item "[[ define value of test3 ( t , c ) as norm t is val : c is val : newline

LET t ref BE r IN newline

LET t idx BE i IN newline

if r = 0 .or. i = 0 then true else newline

LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ "claim" ]] BE d IN newline

if d pairp then ( eval ( d third , true , c ) apply ( t :: c :: true ) maptag ) untag else newline

if c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ "definition" ]] != true then true else test3* ( t tail , c ) end define ]]"

\item "[[ define value of test3* ( t , c ) as norm t is val : c is val : if t atom then true else test3 ( t head , c ) .and. test3* ( t tail , c ) end define ]]"

\item "[[ define value of make math x end math as norm x is val : ( show quote math x end math end quote end show ref :: show quote math x end math end quote end show idx :: x debug ) :: x :: true end define ]]"

\item "[[ define claim of ttst u end test as \ x . ttst1 ( x ) end define ]]"

\item "[[ define value of ttst1 ( x ) as norm x is val : LET x zeroth BE t IN LET x first BE c IN spy ( t ) .then. if eval ( t first , true , c ) untag catch = false :: true then true else make math t end math end define ]]"

\item "[[ define claim of ftst u end test as \ x . ftst1 ( x ) end define ]]"

\item "[[ define value of ftst1 ( x ) as norm x is val : LET x zeroth BE t IN LET x first BE c IN spy ( t ) .then. if eval ( t first , true , c ) untag catch = false :: false then true else make math t end math end define ]]"

\item "[[ define claim of etst u ; v end test as \ x . etst1 ( x ) end define ]]"

\item "[[ define value of etst1 ( x ) as norm x is val : LET x zeroth BE t IN LET x first BE c IN spy ( t ) .then. if eval ( t first , true , c ) untag catch = eval ( t second , true , c ) untag catch then true else make math t end math end define ]]"

\item "[[ ttst true end test ]]"

\item "[[ ftst false end test ]]"

\item "[[ etst 2 ; 2 end test ]]"

\item "[[ etst 2 raise ; 2 raise end test ]]"

\end{statements}



\subsection{Idiosyncrasies}

Logiweb reacts in a predictable way to definitions, even if they look dubious:

\begin{statements}

\item "[[ value define testfunc1 ( x ) as x + 3 end define ]]"

This is an ordinary definition. Thus we have: "[[ etst testfunc1 ( 2 ) ; 5 end test ]]".

\item "[[ value define testfunc2 ( x , x ) as x end define ]]"

When parameters are repeated, the first one is used: "[[ etst testfunc2 ( 2 , 3 ) ; 2 end test ]]". In the codex, the definition is recorded as it is: "[[ ttst self [[ quote testfunc2 ( 2 , 3 ) end quote ref ]] [[ "codex" ]] [[ quote testfunc2 ( 2 , 3 ) end quote ref ]] [[ quote testfunc2 ( 2 , 3 ) end quote idx ]] [[ 0 ]] [[ "value" ]] t= hide quote value define testfunc2 ( x , x ) as x end define end quote end hide end test ]]".

\item "[[ value define testfunc3 as 2 end define ]]" and "[[ value define testfunc3 as 3 end define ]]"

When a definition is stated more than once, then the rightmost one counts: "[[ etst testfunc3 ; 3 end test ]]". The codex always contains the definition that counts.

\item "[[ value define testfunc4 as quote value define testfunc4 as 2 end define end quote end define ]]"

When a page is harvested, all functions that occur inside other functions are disregarded: "[[ ttst testfunc4 t= show hide quote value define testfunc4 as 2 end define end quote end hide end show end test ]]". Without the use of "[[ show hide x end hide end show ]]" above, the definition of "[[ testfunc4 ]]" inside the test case would override the first definition of "[[ testfunc4 ]]".

\item "[[ value define testfunc5 ( x ) as y end define ]]"

Unbound variables equal "[[ true ]]": "[[ etst testfunc5 ( 2 ) ; true end test ]]". "[[ y ]]" is a variable because its root has no value definition: "[[ etst self [[ quote y end quote ref ]] [[ "code" ]] [[ quote y end quote idx ]] ; true end test ]]"

\item "[[ value define testfunc6 ( 2 ) as 2 end define ]]"

One may foolishly use non-variables as parameters, but it is impossible to get access to their values since their value definitions take precedence over their dynamic bindings: "[[ etst testfunc6 ( 3 ) ; 2 end test ]]"

\item "[[ value define testfunc7 ( x _ { 4 } ) as x _ { 4 } + 3 end define ]]"

Compound variables work: "[[ etst testfunc7 ( 2 ) ; 5 end test ]]". The variable "[[ x _ { 4 } ]]" consists of a binary subscript operator applied to "[[ x ]]" and "[[ 4 ]]". "[[ x _ { 4 } ]]" is a variable because the subscript operator has no value definition. When deciding whether or not a term is a variable, only the root of the term matters. The fact that "[[ 4 ]]" does have a value definition has no influence here.

\item "[[ value define testfunc8 ( x _ { 2 + 2 } , x _ { 4 } ) as x _ { 2 + 2 } + x _ { 4 } end define ]]"

"[[ x _ { 2 + 2 } ]]" and "[[ x _ { 4 } ]]" are distinct variables: "[[ etst testfunc8 ( 2 , 3 ) ; 5 end test ]]". "[[ x _ { 2 + 2 } ]]" and "[[ x _ { 4 } ]]" are distinct variables because they are distinct trees: "[[ etst quote x _ { 2 + 2 } end quote t= quote x _ { 4 } end quote ; false end test ]]". The fact that "[[ 2 + 2 = 4 ]]" has no influence here.

\item "[[ define value of base as 2 + 3 end define ]]"

One cannot change the value of the page symbol, but the definition is still recorded in the codex: "[[ ttst show base [[ base [[ 0 ]] ]] [[ "codex" ]] [[ quote base end quote ref ]] [[ quote base end quote idx ]] [[ 0 ]] [[ "value" ]] t= quote define value of base as 2 + 3 end define end quote end show end test ]]"

Furthermore, and more important, the definition is compiled and stored in the code: "[[ show etst base [[ base [[ 0 ]] ]] [[ "code" ]] [[ 0 ]] Tail ; 5 end test end show ]]". This could be useful for recording values which are costly to compute and thus should only be computed once.

\end{statements}



" ]"\section{Compilation}\label{sec:Compilation}"[ "

\subsection{Fixed point combinator}

\begin{statements}

\item "[[ optimized define value of YY as \ f . ( \ x . f ' ( x ' x ) ) ' ( \ x . f ' ( x ' x ) ) end define ]]"

The compiler defined in the following uses the fixed point operator "[[ YY ]]". On some systems, the fixed point operator may be optimized using circular structures. Doing so may give a huge speedup in cases where the compiler itself runs non-optimized.

\end{statements}



\subsection{Compiler}

\begin{statements}

\item "[[ optimized define value of compile ( c ) as norm c is val : newline

( map ( \ c . YY ' \ C . compile1 ( c [[ 0 ]] , c , map ( C ) ) ) apply c maptag ) untag end define ]]"

Compile the cache "[[ c ]]". "[[ c [[ 0 ]] ]]" is the reference "[[ r ]]" of the cache. "[[ C ]]" is the cache being returned from "[[ compile ( c ) ]]". That result is made available to compile1 by the "[[ YY ]]" combinator. The compile1 function has to approach "[[ C ]]" with caution: if compile1 untags "[[ C ]]", then the fixed point operator will return "[[ bottom ]]".

The compile function sets "[[ c [[ r ]] [[ "code" ]] ]]" to a compiled version of "[[ c [[ r ]] [[ "codex" ]] ]]" and sets "[[ c [[ r ]] [[ "diagnose" ]] ]]" to the result of applying "[[ c [[ r ]] [[ "claim" ]] ]]" to "[[ c ]]". The diagnose "[[ c [[ r ]] [[ "diagnose" ]] ]]" and each compiled function "[[ c [[ r ]] [[ "code" ]] [[ i ]] ]]" is map tagged (using "[[ map ( x ) ]]") such that the diagnose and the compiled functions are computed lazily.

The compile1 function performs a few sanity checks and throws an exception if it finds something wrong.



\item "[[ define value of compile1 ( r , c , C ) as norm r is val : c is val : C is val : newline

if .not. r intp then exception else newline

LET c [[ r :: "code" :: true => compile2 ( r , c , C ) ]] BE c IN newline

LET c [[ r :: "diagnose" :: true => compile-claim ( r , c , C ) ]] BE c IN c end define ]]"

Compile cache "[[ c ]]" which has reference "[[ r ]]". "[[ C ]]" is the compiled cache as explained above.



\item "[[ define value of compile2 ( r , c , C ) as norm r is val : c is val : C is val : newline

compile3 ( C , c [[ r ]] [[ "codex" ]] [[ r ]] , true ) end define ]]"

Compile the codex part of the cache "[[ c ]]". "[[ C ]]" is the compiled cache (see above).



\item "[[ define value of compile3 ( C , x , X ) as norm C is val : x is val : X is val : newline

if x then X else newline

if x head intp then X [[ x head -> compile4 ( x tail , C ) ]] else newline

compile3 ( C , x head , compile3 ( C , x tail , X ) ) end define ]]"

Compile the codex part "[[ x ]]" of the cache "[[ c ]]". "[[ C ]]" is the compiled cache (see above) and the result is accumulated in "[[ X ]]".



\item "[[ define value of compile4 ( x , C ) as norm x is val : C is val : newline

LET x [[ 0 ]] [[ "value" ]] BE d IN newline

if d then true else newline

if .not. d pairp .or. .not. d head pairp then exception else newline

if d ref != 0 then newline

map ( \ d . \ C . compile-code ( d , C ) Tail ' true ) apply d maptag apply C else newline

if .not. d head tail pairp then exception else newline

LET d head tail head BE i IN newline

if i = "lambda" then 0 else newline

if i = "quote" then 1 else newline

if i = "true" then true maptag else newline

if i = "apply" then map ( \ x . \ y . x ' y ) else newline

if i = "if" then map ( \ x . \ y . \ z . If x then y else z ) else exception end define ]]"

Compile the codex branch "[[ x ]]" by looking up the value definition "[[ d ]]" in it (if any) and compile "[[ d ]]".

\end{statements}



\subsection{Code constructors}

\begin{statements}

\item "[[ define value of make-constant ( v ) as norm v is val : map ( \ v . \ s . v ) apply v maptag end define ]]"

Convert the value "[[ v ]]" into an uncurried function which returns "[[ v ]]". "[[ s ]]" is the ``stack'', i.e.\ the list of values of all bound variables.



\item "[[ define value of deBruijn ( v , a , b ) as norm v is val : a is val : b is val : newline

if a then deBruijn1 ( v , b ) else newline

if .not. a pairp then exception else newline

if v t= a head then 0 else 1 + deBruijn ( v , a tail , b ) end define ]]"

\item "[[ define value of deBruijn1 ( v , b ) as norm v is val : b is val : newline

if .not. b pairp then exception else newline

if v t= b head then deBruijn2 ( b tail ) else deBruijn1 ( v , b tail ) end define ]]"

\item "[[ define value of deBruijn2 ( b ) as norm b is val : newline

if b then 0 else if b pairp then 1 + deBruijn2 ( b tail ) else exception end define ]]"

Find the position of the variable "[[ v ]]" in the variable lists "[[ a ]]" and "[[ b ]]". Throw exception if the variable is not found. The list "[[ a ]]" contains variables bound by lambdas in deBruijn index order. The list "[[ b ]]" contains arguments in order of appearance which is opposite to the deBruijn index order.



\item "[[ define value of lazy-nth ( i , s ) as If i = 0 then s Head else lazy-nth ( i - 1 , s Tail ) end define ]]"



\item "[[ define value of make-variable ( v , a , b ) as norm v is val : a is val : b is val : newline

LET deBruijn ( v , a , b ) catch tail BE i IN newline

if i then make-constant ( true ) else newline

map ( \ i . \ s . lazy-nth ( i , s ) ) apply i maptag end define ]]"

Convert the variable "[[ v ]]" into an uncurried function which returns "[[ v ]]". "[[ a ]]" is the argument list, i.e.\ the list of names of all bound variables. make-variable looks up the deBruijn index of "[[ v ]]" in "[[ a ]]" and "[[ b ]]" and returns an accessor for that index.



\item "[[ define value of make-lambda ( f ) as norm f is val : newline

map ( \ f . \ s . \ x . f ' ( x LazyPair s ) ) apply f end define ]]"

Add lambda abstraction to the uncurried function "[[ f ]]". "[[ s ]]" is the stack and "[[ x ]]" is the lambda variable to be pushed on the stack.



\item "[[ define value of make-lambdas ( a , f ) as norm a is val : f is val : newline

if .not. a pairp then f else newline

make-lambda ( make-lambdas ( a tail , f ) ) end define ]]"

Add one lambda per argument in the argument list "[[ a ]]".

\end{statements}



\subsection{Compilation of individual constructs}

\begin{statements}

\item "[[ define value of compile-code ( d , c ) as norm d is val : c is val : newline

if .not. d tail tail tail pairp .or. .not. d tail tail tail tail .or. .not. d second pairp then exception else newline

compile-code1 ( d second tail , d third , c ) end define ]]"



\item "[[ define value of compile-code1 ( b , t , c ) as norm b is val : t is val : c is val : newline

make-lambdas ( b , compile-code2 ( true , b , t , c ) ) end define ]]"

Compile "[[ t ]]" and add one lambda per argument.



\item "[[ define value of compile-code2 ( a , b , t , c ) as norm a is val : b is val : t is val : c is val : newline

if .not. t pairp .or. .not. t head pairp .or. .not. t head tail pairp then exception else newline

LET t ref BE r IN newline

LET t idx BE i IN newline

if .not. r intp .or. .not. i intp then exception else newline

if r = 0 then make-constant ( i ) else newline

if i = 0 then if r = c [[ 0 ]] then make-constant ( c ) else newline

make-constant ( c [[ c [[ 0 ]] ]] [[ "cluster" ]] [[ r ]] ) else newline

LET c [[ r ]] [[ "code" ]] [[ i ]] BE f IN newline

if f mapp then newline

compile-code2* ( map ( \ f . \ s . f ) apply f , a , b , t tail , c ) else newline

if f = true then make-variable ( t , a , b ) else newline

if f = 1 then make-constant ( t first ) else newline

make-lambda ( compile-code2 ( t first :: a , b , t second , c ) ) end define ]]"

Compile the right hand side "[[ t ]]" of the definition being compiled in the environment defined by the association list "[[ s ]]". First set "[[ r ]]" and "[[ i ]]" to the reference and index, respectively, of the root of "[[ t ]]". If "[[ r = 0 ]]" then "[[ t ]]" is a string and "[[ i ]]" is the value to be returned. If "[[ i ]]" is zero then "[[ t ]]" is a page symbol whose value is either "[[ c ]]" or can be looked up in the cache branch. Otherwise look up the definition "[[ f ]]" of the root of "[[ t ]]".

If "[[ f ]]" is a map then apply it to compiled versions of the subterms of "[[ t ]]". If "[[ f ]]" is "[[ true ]]" then "[[ t ]]" is a variable to be looked up in the environment "[[ s ]]". If "[[ f ]]" is "[[ 1 ]]" then "[[ t ]]" is a quote construct whose sole argument is returned. Otherwise, "[[ t ]]" is a lambda construct.



\item "[[ define value of compile-code2* ( f , a , b , t , c ) as norm f is val : a is val : b is val : t is val : c is val : newline

if t then f else newline

compile-code2* ( map ( \ f . \ x . \ s . f ' s ' ( x ' s ) ) apply f apply newline

compile-code2 ( a , b , t head , c ) , a , b , t tail , c ) end define ]]"

Apply the function "[[ f ]]" to compiled versions of the elements of the list "[[ t ]]" of terms.

\end{statements}



\subsection{Claim evaluation}

\begin{statements}

\item "[[ define value of prune ( t , C ) as norm t is val : C is val : if t then true else prune1 ( t , C ) end define ]]"



\item "[[ define value of prune1 ( t , C ) as norm t is val : C is val : newline

LET ( C [[ 0 ]] :: 0 ) :: true BE b IN newline

if .not. t pairp .or. .not. t head pairp .or. .not. t head tail pairp then b else newline

LET t ref BE r IN newline

LET t idx BE i IN newline

if .not. r intp .or. .not. i intp then b else newline

if r = 0 then if t tail then t else b else newline

if i = 0 then if t tail then t else b else newline

LET C [[ r ]] [[ "dictionary" ]] [[ i ]] BE a IN newline

if .not. a intp .or. a < 0 then b else newline

LET prune* ( a , t tail , C ) catch BE v IN newline

if v head then b else t head :: v tail end define ]]"



\item "[[ define value of prune* ( a , t , C ) as norm a is val : t is val : C is val : newline

if a = 0 then if t then true else exception else newline

if .not. t pairp then exception else newline

prune1 ( t head , C ) :: prune* ( a - 1 , t tail , C ) end define ]]"



\item "[[ define value of eval-claim as norm map ( \ d . \ C . prune ( ( eval ( d third , true , C ) apply C maptag ) untag , C ) ) end define ]]"



\item "[[ define value of compile-claim ( r , c , C ) as norm r is val : c is val : C is val : newline

LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ 0 ]] [[ 0 ]] [[ "claim" ]] BE d IN newline

if d pairp then eval-claim apply d maptag apply C else newline

LET c [[ r ]] [[ "bibliography" ]] first BE r IN

if r then true maptag else newline

LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ 0 ]] [[ 0 ]] [[ "claim" ]] BE d IN newline

if d pairp then eval-claim apply d maptag apply C else true maptag

end define ]]"

\end{statements}



" ]"\section{Macro expansion}\label{sec:MacroExpansion}"[ "

\subsection{Macro expansion engine}

\begin{statements}

\item "[[ define macro of base as macro1 end define ]]"

\item "[[ define value of macro1 as \ c . macro2 ( c ) end define ]]"

\item "[[ define value of macro2 ( c ) as norm c is val : newline

macro3 ( c [[ c [[ 0 ]] ]] [[ "body" ]] , macrostate0 , c ) end define ]]"

\item "[[ define value of macro3 ( t , s , c ) as norm t is val : s is val : c is val : newline

LET t ref BE r IN newline

LET t idx BE i IN newline

if r = 0 then t else newline

if i = 0 then t else newline

LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ "macro" ]] BE d IN newline

if d = true then t head :: macro3* ( t tail , s , c ) else newline

( eval ( d third , true , c ) apply ( t :: s :: c :: true ) maptag ) untag end define ]]"

\item "[[ define value of macro3* ( t , s , c ) as norm t is val : s is val : c is val : newline

if t atom then true else

macro3 ( t head , s , c ) :: macro3* ( t tail , s , c )

end define ]]"

\item "[[ define value of macro4 ( x ) as norm x is val : macro3 ( x zeroth , x first , x second ) end define ]]"

\item "[[ define value of macrostate0 as norm map ( \ x . macro4 ( x ) ) :: true end define ]]"

\item "[[ define value of stateexpand ( t , s , c ) as norm t is val : s is val : c is val : ( s head apply ( t :: s :: c :: true ) maptag ) untag end define ]]"

\item "[[ define value of stateexpand* ( t , s , c ) as norm t is val : s is val : c is val : newline

if t atom then true else newline

stateexpand ( t head , s , c ) :: stateexpand* ( t tail , s , c ) end define ]]"

\end{statements}



\subsection{Backquoting}

\begin{statements}

\item "[[ define value of substitute ( r , t , s ) as norm r is val : t is val : s is val : newline

LET lookup ( t , s , true ) BE d IN newline

if d = true then ( t ref :: t idx :: r debug ) :: substitute* ( r , t tail , s ) else d end define ]]" Replace subterms of "[[ t ]]" according to the stack "[[ s ]]". Set the debugging information of nodes taken from "[[ t ]]" to the debugging information of the root of "[[ r ]]"

\item "[[ define value of substitute* ( r , t , s ) as norm r is val : t is val : s is val : newline

if t atom then true else newline

substitute ( r , t head , s ) :: substitute* ( r , t tail , s ) end define ]]" Coordinatwise application of substitute to the elements of the list "[[ t ]]".

\item "[[ define value of expand ( d , x ) as norm d is val : x is val : newline

LET x zeroth BE t IN LET zip ( d first tail , t tail ) BE s IN newline

stateexpand ( substitute ( t , d second , s ) , x first , x second ) end define ]]"

"[[ x ]]" is supposed to have form "[[ t :: s :: c :: true ]]". Expand the term "[[ t ]]" accoding the the macro definition "[[ d ]]", then macro expand the result as specified by "[[ x ]]". The macro definition is supposed to have form "[[ hide macro define x as y end define end hide ]]" where the root of "[[ x ]]" equals the root of "[[ t ]]".

\end{statements}



\subsection{Elementary macros}\label{sec:ElementaryMacros}

\begin{statements}

\item "[[ protect define macro of protect u end protect as \ x . x zeroth first end define end protect ]]"

The "[[ protect x end protect ]]" construct protects "[[ x ]]" against macro expansion. During macro expansion, the protection construct itself disappears. Note that the protection construct is used to protect the definition itself. Otherwise the left hand side of the definition would be macro expanded!

\item "[[ protect define macro of Macro define u as v end define as \ x . Macrodefine ( x ) end define end protect ]]"

The "[[ hide Macro define u as v end define end hide ]]" construct macro expands into "[[ hide protect define macro of u as v end define end protect end hide ]]". Thus it allows to state a macro definition which is itself protected against macro definition.

\item "[[ define value of Macrodefine ( x ) as norm x is val : newline

if x = true then quote true end quote else newline

LET x zeroth BE t IN newline

LET t first BE u IN LET t second BE v IN newline

LET ( quote u end quote :: u ) :: ( quote v end quote :: v ) :: true BE s IN newline

substitute ( t , quote protect define macro of u as v end define end protect end quote , s ) end define ]]"

This function performs the actual work of the "[[ hide Macro define u as v end define end hide ]]" macro. If "[[ x ]]" equals "[[ true ]]" then we are probably at a stage of codification where the argument has not yet get a sensible value. In this case just return a valid term. Otherwise, the argument "[[ x ]]" is supposed to have form "[[ t :: s :: c :: true ]]" where "[[ t ]]" is the term to be expanded, "[[ s ]]" is the macro state, and "[[ c ]]" is the cache of the page on which that term occurs. "[[ Macrodefine ( x ) ]]" does not need the state and cache but extracts the term "[[ t ]]" from "[[ x ]]". The term has form "[[ hide Macro define u as v end define end hide ]]" where "[[ u ]]" and "[[ v ]]" are the actual left and right hand sides of the macro definition. "[[ Macrodefine ( x ) ]]" extracts these two terms end forms a stack "[[ s ]]" which maps the variables "[[ u ]]" and "[[ v ]]" to their respective values. Then "[[ Macrodefine ( x ) ]]" calls "[[ substitute ( t , quote *** end quote , s ) ]]" to construct "[[ hide protect define macro of u as v end define end protect end hide ]]". The debugging information of the latter is set to the debugging information of the original term "[[ t ]]" so that one can locate where the macro expanded term came from.

\item "[[ Macro define macro define u as v end define as \ x . macrodefine ( x ) end define ]]"

This construct allows to state simple macro definitions in which a left hand side is macro expanded into a right hand side by simple substitution.

\item "[[ define value of macrodefine ( x ) as norm x is val : newline

LET x zeroth BE t IN newline

LET t first BE u IN newline

LET ( quote t end quote :: t ) :: ( quote u end quote :: u ) :: true BE s IN newline

substitute ( t , quote define macro of u as \ x . expand ( quote t end quote , x ) end define end quote , s ) end define ]]"

This construct is similar to "[[ Macrodefine ( x ) ]]".

\item "[[ Macro define self as \ x . makeself ( x ) end define ]]" The "[[ self ]]" construct expands into the page symbol of the page on which the "[[ self ]]" construct occurs.

\item "[[ define value of makeself ( x ) as norm x is val : newline

LET x zeroth BE t IN LET x second BE c IN newline

LET t debug BE d IN LET c [[ 0 ]] BE r IN newline

( ( r :: 0 :: d ) :: true ) end define ]]"

The "[[ makeself ( x ) ]]" extracts the term "[[ t ]]" of form "[[ self ]]" as well as the cache "[[ c ]]" of the page on which "[[ self ]]" occurs. Then "[[ makeself ( x ) ]]" extracts the debugging information "[[ d ]]" from "[[ t ]]" and extracts the reference "[[ r ]]" of the page on which "[[ self ]]" occurs. Finally, "[[ makeself ( x ) ]]" constructs a tree with reference "[[ r ]]", index "[[ 0 ]]", debugging information "[[ d ]]", and no subtrees.

\item "[[ Macro define root protect u end protect as \ x . rootprotect ( x ) end define ]]"

The "[[ root protect u end protect ]]" construct protects the root of the term "[[ u ]]" against macro expansion but does allow the subtrees of "[[ u ]]" to be expanded.

\item "[[ define value of rootprotect ( x ) as norm x is val : newline

LET x zeroth BE t IN LET t first BE u IN newline

LET u ref BE r IN LET u idx BE i IN LET t debug BE d IN newline

( r :: i :: d ) :: stateexpand* ( u tail , x first , x second ) end define ]]"

\end{statements}



\subsection{Definition macros}

\begin{statements}

\item "[[ macro define render define x as y end define as Define render of root protect x end protect as y end define end define ]]"

Define the render aspect of a construct. The construct itself is protected against macro expansion.

\item "[[ macro define tex use define x as y end define as Define tex use of root protect x end protect as y end define end define ]]"

Define the tex use aspect of a construct. The construct itself is protected against macro expansion.

\item "[[ macro define tex show define x as y end define as Define tex show of root protect x end protect as y end define end define ]]"

\item "[[ macro define value define x as y end define as define value of root protect x end protect as y end define end define ]]"

\item "[[ macro define message define x as y end define as define message of root protect x end protect as y end define end define ]]"

\item "[[ macro define execute define x as y end define as define execute of root protect x end protect as y end define end define ]]"

\item "[[ macro define priority table x as define priority of self as protect x end protect end define end define ]]"

Define the priority table of the page.

\item "[[ macro define verifier x end verifier as define claim of self as x end define end define ]]"

Define the claim of the page.

\item "[[ macro define unpacker x end unpacker as define unpack of self as x end define end define ]]"

Define the unpacker of the page.

\item "[[ macro define renderer x end renderer as define render of self as x end define end define ]]"

Define the renderer of the page.

\item "[[ macro define expander x end expander as define macro of self as x end define end define ]]"

Define the macro expansion engine of the page.

\item "[[ protect proclaim tex use define x as y end define as "hide" end proclaim end protect ]]"

Ensure that the tex use definition construct can be used on the present page. If a tex use definition construct is used to define the tex use aspect of a revelation construct (e.g. a definition or proclamation construct) and if the tex use definition construct is not macro expanded (e.g. early in the codification process where the macro expander is not yet operational) then the hiding specified above ensures that the revelation construct in the left hand side of the tex use definition has no effect.

\item "[[ protect proclaim tex show define x as y end define as "hide" end proclaim end protect ]]"

Ensure that the tex show definition construct can be used on the present page.

\item "[[ protect proclaim priority table x as "hide" end proclaim end protect ]]"

Ensure that the priority table construct can be used on the present page.

\item "[[ protect proclaim macro define x as y end define as "hide" end proclaim end protect ]]"

Ensure that macro definitions can expand into definitions without causing trouble at early stages of codification.

\end{statements}



\subsection{Parentheses}\label{sec:Parentheses}

\begin{statements}

\item "[[ macro define ( x ) as x end define ]]"

Ordinary parentheses.

\item "[[ macro define newline x as x end define ]]"

Put newline before x. The construct has charge 32.

\item "[[ macro define tight newline x as x end define ]]"

Put newline before x. The construct has charge 2.

\item "[[ late eager define include ( x ) as x end define ]]"

This has value x but renders x as an elipsis.

\item "[[ macro define x tight endline as x end define ]]"

Put newline after x. The construct has charge 4.

\item "[[ macro define x endline as x end define ]]"

Put newline after x. The construct has charge 50.

\end{statements}



\subsection{Numerals}\label{sec:Numerals}

As mentioned in Section \ref{sec:IntegerConstruction}, an integer like "[[ %% %1 %2 %3 ]]" can be expressed as an invisible zero followed by three suffix operators "[[ x %1 ]]", "[[ x %2 ]]", and "[[ x %3 ]]". The source of "[[ %% %1 %2 %3 ]]" reads \verb+%% %1 %2 %3+ where \verb+%%+ is the invisible zero and \verb+%1+, \verb+%2+, and \verb+%3+ are the three suffix operators. This way of entering numbers is rather inconvenient, however.

It is more convenient to enter a number like "[[ 123 ]]" as \verb+123+ where \verb+3+ is a nulary operator and \verb+1+ and \verb+2+ are prefix operators. Macros which support that are given in the following. The macros defined in the following convert \verb+123+ into \verb+%% %1 %2 %3+.

Seen in isolation, it would be much easier to treat \verb+123+ as a nulary operator \verb+1+ followed by suffix operators \verb+2+ and \verb+3+. Doing so, however, is a waste of good names. As an example, it is convenient to have constructs named things like \verb+myname+ and \verb+myname2+ in Logiweb source files. If we introduced a suffix \verb+2+, however, \verb+myname2+ could be interpreted either as the \verb+myname+ construct followed by a suffix \verb+2+ or as the \verb+myname2+ construct. This is why numerals are constructed by prefix operators and why the burden of reversing the digit lists is left to the macro expander.

\begin{statements}

\item "[[ Macro define 0x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 1x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 2x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 3x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 4x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 5x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 6x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 7x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 8x as \ x . numeral ( x ) end define ]]"

\item "[[ Macro define 9x as \ x . numeral ( x ) end define ]]"

\item "[[ define value of numeral ( x ) as norm x is val : num1 ( x zeroth , x zeroth , substitute ( x zeroth , quote %% end quote , true ) ) end define ]]"

\item "[[ protect define value of num1 ( r , t , u ) as norm r is val : t is val : u is val : newline

if t tail then num2 ( r , t , u ) else newline

LET ( quote x end quote :: u ) :: true BE s IN newline

if t r= quote 0x end quote then num1 ( r , t first , substitute ( r , quote x %0 end quote , s ) ) else newline

if t r= quote 1x end quote then num1 ( r , t first , substitute ( r , quote x %1 end quote , s ) ) else newline

if t r= quote 2x end quote then num1 ( r , t first , substitute ( r , quote x %2 end quote , s ) ) else newline

if t r= quote 3x end quote then num1 ( r , t first , substitute ( r , quote x %3 end quote , s ) ) else newline

if t r= quote 4x end quote then num1 ( r , t first , substitute ( r , quote x %4 end quote , s ) ) else newline

if t r= quote 5x end quote then num1 ( r , t first , substitute ( r , quote x %5 end quote , s ) ) else newline

if t r= quote 6x end quote then num1 ( r , t first , substitute ( r , quote x %6 end quote , s ) ) else newline

if t r= quote 7x end quote then num1 ( r , t first , substitute ( r , quote x %7 end quote , s ) ) else newline

if t r= quote 8x end quote then num1 ( r , t first , substitute ( r , quote x %8 end quote , s ) ) else newline

if t r= quote 9x end quote then num1 ( r , t first , substitute ( r , quote x %9 end quote , s ) ) else newline

substitute ( r , quote exception end quote , true ) end define end protect ]]"

\item "[[ define value of num2 ( r , t , u ) as norm r is val : t is val : u is val : newline

LET ( quote x end quote :: u ) :: true BE s IN newline

if t r= quote 0 end quote then substitute ( r , quote x %0 end quote , s ) else newline

if t r= quote 1 end quote then substitute ( r , quote x %1 end quote , s ) else newline

if t r= quote 2 end quote then substitute ( r , quote x %2 end quote , s ) else newline

if t r= quote 3 end quote then substitute ( r , quote x %3 end quote , s ) else newline

if t r= quote 4 end quote then substitute ( r , quote x %4 end quote , s ) else newline

if t r= quote 5 end quote then substitute ( r , quote x %5 end quote , s ) else newline

if t r= quote 6 end quote then substitute ( r , quote x %6 end quote , s ) else newline

if t r= quote 7 end quote then substitute ( r , quote x %7 end quote , s ) else newline

if t r= quote 8 end quote then substitute ( r , quote x %8 end quote , s ) else newline

if t r= quote 9 end quote then substitute ( r , quote x %9 end quote , s ) else newline

substitute ( r , quote exception end quote , true ) end define ]]"

\end{statements}



\subsection{Formating of the expansion}

\begin{statements}

\item "[[ macro define make macro expanded version ragged right as ragged right end define ]]"

\end{statements}



\subsection{Visibility constructs}\label{sec:VisibilityConstructs}

The following constructs affect \indexintro{visibility}:

\begin{statements}

\item "[[ show show x end show end show ]]" renders the constructs in "[[ x ]]" using the tex show aspect.

\item "[[ show !x end show ]]": Save as "[[ show show x end show end show ]]" but shorter.

\item "[[ show macro show x end show end show ]]" is similar to "[[ show show x end show end show ]]" but also macro expands like parentheses so that it disappears in the expansion of the page.

\item "[[ show hide x end hide end show ]]" hides "[[ x ]]" from harvesting, c.f. Section \ref{sec:Proclamations}.

\item "[[ show hiding show x end show end show ]]" renders the constructs in "[[ x ]]" using the tex show aspect, protects "[[ x ]]" from macro expansion, and and hides "[[ x ]]" from harvesting.

\end{statements}

All constructs above are themselves invisible when rendered using the tex use aspect. They are visible above because they are all enclosed in a "[[ show show x end show end show ]]" construct. The properties of the constructs are declared in the following:

\begin{statements}

\item "[[ optimized define value of show x end show as x end define ]]"

\item "[[ optimized define value of !x as x end define ]]"

\item "[[ macro define macro show x end show as x end define ]]"

\item "[[ optimized define value of hide x end hide as x end define ]]"

\item "[[ proclaim hide x end hide as "hide" end proclaim ]]"

\item "[[ optimized define value of hiding show x end show as x end define ]]"

\item "[[ macro define hiding show x end show as protect hiding show x end show end protect end define ]]"

\item "[[ proclaim hiding show x end show as "hide" end proclaim ]]"

\end{statements}



\subsection{Tuples}

\begin{statements}

\item "[[ value define <<>> as norm true end define ]]"

\item "[[ Macro define << u >> as \ x . tuple1 ( x ) end define ]]"

\item "[[ define value of tuple1 ( x ) as norm x is val : stateexpand ( tuple2 ( x zeroth , x zeroth first ) , x first , x second ) end define ]]"

\item "[[ define value of tuple2 ( t , u ) as norm t is val : u is val : newline

if .not. u r= quote x ,, y end quote then newline

substitute ( t , quote u :: <<>> end quote , ( quote u end quote :: u ) :: true ) else newline

substitute ( t , quote x :: y end quote , ( quote x end quote :: u first ) :: ( quote y end quote :: tuple2 ( t , u second ) ) :: true ) end define ]]"

\end{statements}



\subsection{Eager definitions}\label{sec:EagerDefinitions}

\begin{statements}

\item "[[ Macro define eager define u as v end define as \ x . eager1 ( x ) end define ]]"

Construct of eager definitions.

\item "[[ define value of eager1 ( x ) as norm x is val : newline

LET x zeroth BE t IN newline

LET t first BE u IN LET t second BE v IN newline

LET ( quote u end quote :: u ) :: ( quote w end quote :: eager2 ( t , u tail , v ) ) :: true BE s IN newline

stateexpand ( substitute ( t , quote define value of u as norm w end define end quote , s ) , x first , x second ) end define ]]"

\item "[[ define value of eager2 ( t , p , v ) as norm t is val : p is val : v is val : newline

if p atom then v else newline

LET ( quote x end quote :: p head ) :: ( quote v end quote :: eager2 ( t , p tail , v ) ) :: true BE s IN newline

substitute ( t , quote x is val : v end quote , s ) end define ]]"

\item "[[ macro define eager message define x as y end define as message define x as y end define,eager define x as y end define end define ]]"

\end{statements}



\subsection{Late definitions}

The following constructs allow to state ``late definitions'' which only work after macros are in place. Useful only on the present page to avoid spurious warnings about mistakenly unfit functions or unrecognized optimized functions.

\begin{statements}

\item "[[ macro define late eager define u as v end define as eager define u as v end define end define ]]"

\item "[[ proclaim late unhide x end unhide as "hide" end proclaim ]]"

\item "[[ macro define late unhide x end unhide as x end define ]]"

\item "[[ macro define late optimized define u as v end define as late unhide optimized define value of u as v end define end unhide end define ]]"

\end{statements}



\subsection{Let constructs}\label{sec:LetConstructs}

We now define two let constructs. The first one allows to make a local macro definition. The second one allows to bind a pattern to a value. When binding a pattern to a value, the value is destructured according to the pattern and each variable in the pattern is bound to a component of the value. Destructuring is user definable. Below, we merely define how a pair is destructured into head and tail.

\begin{statements}

\item "[[ Macro define let u := v in w as \ x . macrolet1 ( x ) end define ]]"

The construct above locally defines "[[ u ]]" to macro expand to "[[ v ]]" inside "[[ w ]]".

\item "[[ define value of macrolet1 ( x ) as norm x is val : newline

LET x zeroth BE t IN LET x first BE s IN LET x second BE c IN newline

LET t first BE u IN LET t third BE w IN newline

LET u ref BE r IN LET u idx BE i IN newline

LET c [[ r :: "codex" :: r :: i :: 0 :: "macro" :: true => macrodefine ( x ) ]] BE c IN newline

stateexpand ( w , s , c ) end define ]]"

The function above implements local macro definitions.

\item "[[ define message of destructure as "destructure" end define ]]"

The destructure aspect allows to define how a value is destructured by a particular pattern. We only define destructuring of pairs in the following.

\item "[[ define destructure of u :: v as ( if asterisk atom then asterisk else asterisk head ) :: ( if asterisk atom then asterisk else asterisk tail ) :: true end define ]]"

The definition above describes how a pair is destructured into head and tail. If a non-pair "[[ x ]]" is destructured as a pair then both the head and the tail part is bound to "[[ x ]]". In the definition, "[[ asterisk ]]" denotes the value to be destructured.

\item "[[ macro define destructure define x as y end define as define destructure of root protect x end protect as y end define end define ]]"

The macro above allows to define destructuring properties of a construct. We do not use the macro on the present page, however, to avoid problems with late definitions, c.f.\ Section \ref{sec:EagerDefinitions}.

\item "[[ Macro define let u = v in w as \ x . let1 ( x ) end define ]]"

\item "[[ define value of let1 ( x ) as norm x is val : newline

LET x zeroth BE t IN LET x first BE s IN LET x second BE c IN newline

LET t first BE u IN LET t second BE v IN LET t third BE w IN newline

LET stateexpand ( u , s , c ) BE u IN newline

LET stateexpand ( v , s , c ) BE v IN newline

LET stateexpand ( w , s , c ) BE w IN newline

LET make-prime ( make-var ( t ) ) BE x IN newline

LET let2 ( x , u , w , c ) BE w IN newline

make-let ( quote asterisk end quote , v , w )

end define ]]"

\item "[[ define value of let2 ( x , p , w , c ) as norm x is val : p is val : w is val : c is val : newline

LET p ref BE r IN LET p idx BE i IN newline

LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] BE c prime IN newline

LET c prime [[ "destructure" ]] BE d IN newline

if d = true then newline

if c prime [[ "value" ]] != true then w else make-let ( p , quote asterisk end quote , w ) else newline

LET let3 ( x , p tail , w , c ) BE w IN newline

make-let ( x , d third , w )

end define ]]"

\item "[[ define value of let3 ( x , p prime , w , c ) as norm x is val : p prime is val : w is val : c is val : newline

if p prime = true then w else newline

LET p prime head BE p IN LET p prime tail BE p prime IN newline

LET let3 ( x , p prime , w , c ) BE w IN newline

LET let2 ( make-prime ( x ) , p , w , c ) BE w IN newline

LET make-let ( x , make-tail ( x ) , w ) BE w IN newline

make-let ( quote asterisk end quote , make-head ( x ) , w ) end define ]]"

\item "[[ define value of make-var ( t ) as norm t is val : newline

substitute ( t , quote asterisk end quote , true ) end define ]]"

\item "[[ define value of make-let ( u , v , w ) as norm u is val : v is val : w is val : newline

LET ( quote u end quote :: u ) :: ( quote v end quote :: v ) :: ( quote w end quote :: w ) :: true BE s IN newline

substitute ( u , quote LET v BE u IN w end quote , s ) end define ]]"

\item "[[ define value of make-prime ( x ) as norm x is val : newline

LET ( quote x end quote :: x ) :: true BE s IN newline

substitute ( x , quote x prime end quote , s ) end define ]]"

\item "[[ define value of make-head ( x ) as norm x is val : newline

LET ( quote x end quote :: x ) :: true BE s IN newline

substitute ( x , quote x head end quote , s ) end define ]]"

\item "[[ define value of make-tail ( x ) as norm x is val : newline

LET ( quote x end quote :: x ) :: true BE s IN newline

substitute ( x , quote x tail end quote , s ) end define ]]"

\end{statements}



\subsection{Backquoting}

\begin{statements}

\item "[[ Macro define back u quote v end quote as \ x . backquote0 ( x ) end define ]]"

\item "[[ define value of make-root ( t , x ) as norm t is val : x is val : x ref :: x idx :: t debug end define ]]"

\item "[[ define value of make-pair ( t , x , y ) as norm t is val : x is val : y is val : make-root ( t , quote true :: true end quote ) :: x :: y :: true end define ]]"

\item "[[ define value of make-true ( t ) as norm t is val : make-root ( t , quote true end quote ) :: true end define ]]"

\item "[[ define value of make-quote ( t , x ) as norm t is val : x is val : make-root ( t , quote quote true end quote end quote ) :: x :: true end define ]]"

\item "[[ define value of make-make-root ( t , x , y ) as norm t is val : x is val : y is val : make-root ( t , quote make-root ( true , true ) end quote ) :: x :: y :: true end define ]]"

\item "[[ define value of backquote0 ( x ) as norm x is val : backquote1 ( x zeroth , x first , x second ) end define ]]"

\item "[[ define value of backquote1 ( t , s , c ) as norm t is val : s is val : c is val : backquote2 ( t , stateexpand ( t first , s , c ) , stateexpand ( t second , s , c ) , s , c ) end define ]]"

\item "[[ define value of backquote2 ( t , u , v , s , c ) as norm t is val : u is val : v is val : s is val : c is val : newline

if v r= quote true unquote end quote then v first else newline

make-pair ( t , make-make-root ( t , u , make-quote ( t , v ) ) , backquote2* ( t , u , v tail , s , c ) ) end define ]]"

\item "[[ define value of backquote2* ( t , u , v , s , c ) as norm t is val : u is val : v is val : s is val : c is val : newline

if v atom then make-true ( t ) else newline

make-pair ( t , backquote2 ( t , u , v head , s , c ) , backquote2* ( t , u , v tail , s , c ) ) end define ]]"

\end{statements}



\subsection{Rendering}

We define a number of constructs for rendering. To see how most of them are used, consult the source of the present Logiweb page.

\begin{statements}

\item "[[ show text x : y end text end show ]]". Store the text "[[ y ]]" in a file named "[[ x ]]".

\item "[[ show latex ( x ) end show ]]". Run latex on the file named "[[ x ]]".

\item "[[ show bibtex ( x ) end show ]]". Run bibtex on the file named "[[ x ]]".

\item "[[ show makeindex ( x ) end show ]]". Run makeindex on the file named "[[ x ]]".

\item "[[ show dvipdfm ( x ) end show ]]". Run dvipdfm on the file named "[[ x ]]".

\item "[[ show tex-file ( c , x , y ) end show ]]". Equivalent to "[[ show text x : y end text end show ]]" when "[[ c ]]" is the string ``text''.

\item "[[ show tex-command ( c , x ) end show ]]". Equivalent to "[[ show latex ( x ) end show ]]", "[[ show bibtex ( x ) end show ]]", "[[ show makeindex ( x ) end show ]]", and "[[ show dvipdfm ( x ) end show ]]", respectively, when "[[ c ]]" is one of the strings ``latex'', ``bibtex'', ``makeindex'', and ``dvipdfm''.

\item "[[ show page ( x , y ) title t bib b main text m appendix a end page end show ]]". A construct for defining a document with title "[[ t ]]", bib-file "[[ b ]]", main text "[[ m ]]", and appendix "[[ a ]]". The main text is processed by latex, bibtex, makeindex, latex, and latex. The appendix is processed by latex three times. "[[ x ]]" and "[[ y ]]" must be Name and Priority, respectively, where the Logiweb compiler expands the two into name and priority definitions, respectively.

\end{statements}

Only the `page' construct needs a definition here. All the other ones just have tex use definitions which are stated later.

\begin{statements}

\item "[[ Macro define page ( x , y ) title t bib b main text m appendix a end page as \ z . page1 ( z ) end define ]]"

\item "[[ define value of page1 ( z ) as norm z is val : newline

LET z zeroth BE t IN newline

LET z first BE s IN newline

LET z second BE c IN newline

LET t second BE y IN newline

LET stateexpand ( t fifth , s , c ) BE m IN newline

LET stateexpand ( t sixth , s , c ) BE a IN newline

LET show quote protect page ( x , y ) title t bib b main text m appendix a end page end protect end quote end show BE p IN newline

( p ref :: p idx :: t debug ) :: t first :: y :: t third :: t fourth :: m :: a :: true end define ]]"

\end{statements}



" ]"\section{The Logiweb machine}\label{sec:Interaction}"[ "

A \index{machine, Logiweb}\indexintro{Logiweb machine} is an abstract machine which consists of

\begin{itemize}

\item a Logiweb computing engine,

\item an \indexintro{interface},

\item a \index{handler, boot}\indexintro{boot handler}, and

\item a \indexintro{cache}.

\end{itemize}

\noindent The engine and interface comprise the `hardware' of the abstract machine whereas the handler and cache comprise software which is preloaded on the machine.

Each Logiweb page may define one or more Logiweb machines. When a Logiweb page is rendered, all machines defined on the page (if any) are output as executable files. The cache of each machine equals the cache of the page defining the machine whereas each machine has its own, individual handler.

The interface of a Logiweb machine performs an input-eval-output-loop in which it converts input to a list of \index{input message}\index{message, index}\intro{input messages} and applies the handler to that input list. The return value is supposed to be a list of \index{output message}\index{message, output}\intro{output messages} which the interface executes. We shall refer to output messages as \index{request}\intro{requests}. We shall refer to input messages as \index{reply}\intro{replies} when they are direct responses to requests and as \index{event}\intro{events} otherwise.

The interface has the ability to load code dynamically into the running machine. Such code can improve the efficiency of the engine and can add new abilities to the interface. A Logiweb machine is {\em virgin} from it starts and until first time it loads code. The virgin Logiweb machine has very few abilities.



\subsection{Messages}\label{section:Messages}

The virgin Logiweb machine knows the following output events:

\["[ array ( left )

late eager define quit request ( x ) as << << 0 ,, "quit" >> ,, x >> end define \\

late eager define write request ( s ) as << << 0 ,, "write" >> ,, s >> end define \\

late eager define read request as << << 0 ,, "read" >> >> end define \\

late eager define exec request ( p , h ) as << << 0 ,, "exec" >> ,, p ,, h >> end define \\

late eager define extend request ( r , s ) as << << 0 ,, "extend" >> ,, r ,, s >> end define

end array ]"\]

\noindent And the following input messages:

\["[ array ( left )

late eager define boot event ( a , e , c , s ) as << << 0 ,, "boot" >> ,, a ,, e ,, c ,, s >> end define \\

late eager define read reply ( c ) as << << 0 ,, "read" >> ,, c >> end define \\

late eager define exec reply ( i , p ) as << << 0 ,, "exec" >> ,, i ,, p >> end define \\

late eager define extend reply ( x ) as << << 0 ,, "extend" >> ,, x >> end define

end array ]"\]

\noindent Each exec reply contains an ``interrupt''. The following interrupts are predefined:

\["[ array ( left )

late eager define exit interrupt as << << 0 ,, "exit" >> >> end define \\

late eager define time interrupt as << << 0 ,, "time" >> >> end define \\

late eager define memory interrupt as << << 0 ,, "memory" >> >> end define

end array ]"\]



\subsection{Machine invocation}

A user may start a Logiweb machine by typing its name followed by arguments on a command line. The machine then forms the term "[[ t = h apply << boot event ( a , e , c , s ) >> ]]" where "[[ h ]]" is the boot handler, "[[ a ]]" is \verb+argv+, "[[ e ]]" is the current environment, "[[ c ]]" is the cache, and "[[ s ]]" is system specific information in the same format as "[[ e ]]". Then the machine enters an input-eval-output-loop.



\subsection{Input-eval-output-loop}

When the machine enters the input-eval-output-loop, the interface asks the engine to reduce "[[ t ]]". The result of that is supposed to be a list of output messages. The interface then executes the output messages one at a time as follows:

A "[[ quit request ( x ) ]]" makes the machine exit immediately with return code "[[ x ]]".

A "[[ write request ( s ) ]]" makes the interface write the strings in "[[ s ]]" to standard output. If "[[ s ]]" is a cardinal then the cardinal is interpretted as a list of bytes encoded little endian base 256. Bytes are written in little endian order, leaving any interpretation of the bytes the the receiver. If "[[ s ]]" has form "[[ u :: v ]]" then the interface recursively outputs first "[[ u ]]" and then "[[ v ]]". If "[[ s ]]" is neither a cardinal nor a pair then it is ignored.

A "[[ read request ]]" makes the interface read one byte from standard input. Usually, reading is blocking, but this may be system dependent. Each read request results in a "[[ read reply ( c ) ]]" input message. The value of "[[ c ]]" is a cardinal which represents the input byte as a one byte string. The value of "[[ c ]]" is the empty string if reading is non-blocking and no input is available. The value of "[[ c ]]" is zero if the end of standard input has been reached.

An "[[ extend request ( r , s ) ]]" makes the interface treat "[[ s ]]" as a piece of source code which the interface compiles and loads. The details are system dependent. Each extend request results in an "[[ extend reply ( x ) ]]" input message where the semantics of "[[ x ]]" is system dependent.

An "[[ exec request ( p , h ) ]]" makes the machine discard all messages following the Exec and asks the engine to reduce "[[ p ]]". During execution of "[[ p ]]" there is an upper, system dependent limit on the time and memory the engine may use. Reduction of "[[ p ]]" may stop because of timeout, memory overflow, or external interupts. Reduction may also stop because the engine succeeds to reduce "[[ p ]]". We shall refer to the latter situation as an {\em exit} interrupt so that reduction of "[[ p ]]" always ends with an interrupt. Then the interface forms the term

\["[ t = h apply << exec reply ( << i ,, a _ { 1 } ,, "\ldots" ,, a _ { m } >> , p ) ,, e _ { 1 } ,, "\ldots" ,, e _ { n } >> ]"\]

\noindent where "[[ i ]]" identifies the interrupt, "[[ a _ { 1 } ,, "\ldots" ,, a _ { m } ]]" are possible interrupt parameters, and "[[ e _ { 1 } ,, "\ldots" ,, e _ { n } ]]" are input messages that have occurred since last. Then the interface reenters the input-eval-output-loop.

The predefined interrupts (exit, time, and memory) take no parameters. An exit interrupt indicates that "[[ p ]]" has been reduced. A time interrupt indicates that execution of "[[ p ]]" was stopped by a timer. A memory interrupt indicates that execution of "[[ p ]]" ran out of memory. As a minimum, Logiweb machines must support the exit interrupt.

On the virgin machine, the input messages comprise one extend reply for each extend request plus one read reply for each read request. Replies occur in the reverse order of their associated requests.



\subsection{Handlers and processes}

The "[[ exec request ( p , h ) ]]" event makes the machine evaluate the {\em process} "[[ p ]]" and, when that is interrupted, the {\em handler} "[[ h ]]". Hence, "[[ h ]]" corresponds to an interrupt handler and "[[ p ]]" corresponds to a less privileged user, operating system, or driver process. The handler "[[ h ]]" has full control over the machine in that it receives all input, generates all output, and cannot be interrupted.



\subsection{Character constants}

We now define a number of often used character constants.

\begin{statements}

\item "[[ late eager define NULL as bt2vector ( 0 ) end define ]]"

\item "[[ late eager define TAB as bt2vector ( 9 ) end define ]]"

\item "[[ late eager define LF as bt2vector ( 10 ) end define ]]"

\item "[[ late eager define FF as bt2vector ( 12 ) end define ]]"

\item "[[ late eager define CR as bt2vector ( 13 ) end define ]]"

\item "[[ late eager define SP as !" " end define ]]"

\item "[[ late eager define QQ as !""-""!" end define ]]"

\item "[[ late eager define V128 as bt2vector ( 128 ) end define ]]"

\item "[[ late eager define V255 as bt2vector ( 255 ) end define ]]"

\end{statements}

Some auxiliary definitions that use these constants read:

\begin{statements}

\item "[[ late eager define CRLF as CR :: LF end define ]]"

ASCII Carriage Return followed by Linefeed.

\item "[[ late eager define LFCR as LF :: CR end define ]]"

ASCII Linefeed followed by Carriage Return.

\item "[[ late eager define '' as vt2vector ( true ) end define ]]"

A convenience function for expressing the empty string.

\item "[[ late eager define writeln request ( x ) as write request ( x :: LF ) end define ]]"

\item "[[ late eager define println ( x ) as print ( x :: LF ) end define ]]"

\end{statements}



\subsection{Hello World}

A machine with "[[ late eager define Hello World as map ( \ x . << writeln request ( "Hello World" ) >> ) end define ]]" as boot handler writes ``Hello World'' and exits. The example abuses the high privilege boot handler to do the writing. In the absence of Exec and Quit events, the machine quits with return code 0 after writing `Hello World'.



\subsection{Echo}

A machine with "[[ Echo ]]" below as boot handler echos all characters typed except that it quits when the user types `q':

\begin{quote}

\noindent "[[ late eager define Echo as map ( \ x . Echo1 ( x ) ) end define ]]"

\noindent "[[ late eager define Echo1 ( x ) as newline

if x atom then newline

<< read request ,, exec request ( true , Echo ) >> else newline

LET x head BE e IN newline

LET Echo1 ( x tail ) BE r IN newline

if .not. e head = << 0 ,, "read" >> then r else newline

if e first = "q" then << writeln request ( true ) ,, quit request ( 0 ) >> else

write request ( e first ) :: r end define ]]"

\end{quote}



\subsection{Eecho}

A machine with "[[ Eecho ]]" below as boot handler echos all characters typed twice except that it quits when the user types `q':

\begin{quote}

\noindent "[[ late eager define Eecho as map ( \ x . Eecho1 ( x ) ) end define ]]"

\noindent "[[ late eager define Eecho1 ( x ) as newline

if x atom then newline

<< read request ,, exec request ( true , Eecho ) >> else newline

LET x head BE e IN newline

LET Eecho1 ( x tail ) BE r IN newline

if .not. e head = << 0 ,, "read" >> then r else newline

if e first = "q" then << writeln request ( true ) ,, quit request ( 0 ) >> else

write request ( e first :: e first ) :: r end define ]]"

\end{quote}



\subsection{Execution constructs}\label{Sec:ExecutionConstructs}

A definition like "[[ execute define "eecho" as << Eecho >> end define ]]" makes the Logiweb compiler generate a machine named "[[ !"eecho" ]]" whose handler is "[[ Eecho ]]".

After macro expansion, the principal operator of the right hand side of the definition must have arity at least two. The first subtree of the principal operator is used as handler. The system specific information "[[ s ]]" of the boot event is derived from the second subtree of the principal operator.

Actually, generation of machines is part of the rendering process which may be customized by the user. For more on this see the Logiweb page which defines the Logiweb compiler.

In some cases one may want a page to represent one and only one anonymous machine. In that case it is suggested to name that machine "[[ !"main" ]]" (so that it is not \emph{really} anonymous). As an example, if one wants to construct a Logiweb browser which can display pages with dynamic behavior, then one could let the anonymous machine of the page define the behavior.

Each machine defined on a page needs its own definition:

\begin{statements}

\item "[[ execute define "hello" as << Hello World >> end define ]]"

\item "[[ execute define "echo" as << Echo >>  end define ]]"

\item "[[ execute define "lgciotest" as << lgcio1 >> end define ]]"

\end{statements}



" ]"\section{The lgcio interface}"[ "

The lgcio interface provides all the input/output facilities needed by the lgc compiler. These features are:

\begin{description}

\item[FileWrite] Write given contents to given file. If the file does not exist, create it in mode 0666 (read/write access to everybody). For the typical value of umask (0022) this results in mode 0644 (read/write to user, read to everybody).

\item[FileWriteExec] Same as above, but using mode 0777 instead of mode 0666. Hence, created files become executable.

\item[FileRead] Read all contents of a given file.

\item[FileRm] Remove given file. If the file does not exist, do nothing.

\item[FileSymlink] Create symbolic link.

\item[FileReadLink] Read symbolic link. In contrast, a FileRead on a symbolic link reads the contents of the file pointed to by the symbolic link.

\item[FileMkdir] Create directories containing given path. Examples: Given path abc/def/ghi create abc/ and abc/def/. Given path abc/def/ghi/ create abc/, abc/def/, and abc/def/ghi/.

\item[FileRmdir] Remove given, empty directory. If the directory does not exist, do nothing.

\item[FileDir] Read all entries of given directory.

\item[FileType] Read the type of the given file (regular, directory, symbolic link, non-existent, or other).

\item[FileTypeRead] Combination of FileRead and FileType: Return "[[ t :: c ]]" where "[[ t ]]" is the type of the given file (non-existent or regular) and "[[ c ]]" is the contents of the file (if any).

\item[TextWrite] Same as FileWrite, but changes newline sequences to given sequence.

\item[TextWriteExec] Same as FileWriteExec, but changes newline sequences to given sequence.

\item[FileGetCwd] Return current working directory.

\item[UnixTime] Read the clock.

\item[Demonize] Turn the running process into a demon (i.e.\ get rid of the controlling terminal). Redirect stdout and stderr. Optionally try to change user id. Optionally write the process id of the process after demonization to a file.

\item[Execlp1] In a given directory, run a given command with one argument. The search path is used to locate the command.

\item[TcpQuery] Send given bytes to given port of given domain.

\end{description}



\subsection{The lgcio request}

The "[[ lgcio ( c ) ]]" request carries communication between the computing engine and the lgcio interface.

To load the lgcio interface and link it to the "[[ lgcio ( c ) ]]" request, place an event of form "[[[ extend request ( lgcio ( true ) , lgcio-interface ) ]]]" on the list of output events from the computing engine.

Afterwards, to invoke a feature of the lgcio interface, place an "[[ lgcio ( c ) ]]" request in the list of output events from the computing engine. That will make the lgcio interface execute the command encoded by "[[ c ]]" and place an "[[ lgcio ( c ) ]]" reply in the list of input events to the computing engine.

The command "[[ c ]]" of an "[[ lgcio ( c ) ]]" request is interpreted as a string tree. The response "[[ c ]]" of an "[[ lgcio ( c ) ]]" reply is a list of one element strings. Actually, this holds true for all requests and replies that are defined using extend events.

We define "[[ lgcio ( c ) ]]" such that "[[ quote lgcio ( c ) end quote t= lgcio ( quote c end quote ) ]]":

"[[[ late eager define lgcio ( c ) as << quote lgcio ( c ) end quote head ,, c >> end define ]]]"



\subsection{Constants used by the lgcio interface}

Each feature provided by the lgcio interface is identified by a command identifier. A command identifier is a single byte. Those command identifiers are defined in the following. Additionally, null bytes are used as end markers for strings. For that reason we also define "[[ EOS ]]" to denote a null byte.

\begin{statements}

\item "[[ late eager define EOS as bt2vector ( 0 ) end define ]]"

\item "[[ late eager define FileWrite as bt2vector ( 1 ) end define ]]"

\item "[[ late eager define FileWriteExec as bt2vector ( 2 ) end define ]]"

\item "[[ late eager define FileRead as bt2vector ( 3 ) end define ]]"

\item "[[ late eager define FileRm as bt2vector ( 4 ) end define ]]"

\item "[[ late eager define FileSymlink as bt2vector ( 5 ) end define ]]"

\item "[[ late eager define FileReadLink as bt2vector ( 6 ) end define ]]"

\item "[[ late eager define FileMkdir as bt2vector ( 7 ) end define ]]"

\item "[[ late eager define FileRmdir as bt2vector ( 8 ) end define ]]"

\item "[[ late eager define FileDir as bt2vector ( 9 ) end define ]]"

\item "[[ late eager define FileType as bt2vector ( 10 ) end define ]]"

\item "[[ late eager define FileTypeRead as bt2vector ( 11 ) end define ]]"

\item "[[ late eager define TextWrite as bt2vector ( 12 ) end define ]]"

\item "[[ late eager define TextWriteExec as bt2vector ( 13 ) end define ]]"

\item "[[ late eager define FileGetCwd as bt2vector ( 14 ) end define ]]"

\item "[[ late eager define UnixTime as bt2vector ( 20 ) end define ]]"

\item "[[ late eager define Demonize as bt2vector ( 30 ) end define ]]"

\item "[[ late eager define Execlp1 as bt2vector ( 31 ) end define ]]"

\item "[[ late eager define TcpQuery as bt2vector ( 40 ) end define ]]"

\end{statements}

The reply from a FileType request represents the type of the queried file thus:

\begin{statements}

\item "[[ late eager define FileTypeNonexistent as bt2vector ( 0 ) end define ]]"

\item "[[ late eager define FileTypeOther as bt2vector ( 1 ) end define ]]"

\item "[[ late eager define FileTypeRegular as bt2vector ( 2 ) end define ]]"

\item "[[ late eager define FileTypeDirectory as bt2vector ( 3 ) end define ]]"

\item "[[ late eager define FileTypeLink as bt2vector ( 4 ) end define ]]"

The reply from a FileTypeRead request is of form "[[ t :: c ]]" where "[[ t ]]" is "[[ FileTypeNonexistent ]]" or "[[ FileTypeRegular ]]" and "[[ c ]]" is the contents of the file (if any).

\end{statements}



\subsection{Data conversion}

The following functions allow to construct arguments of request and analyse arguments of replies.

\begin{statements}

\item "[[ late eager define septet*2card ( r , s ) as newline

if s atom then r else septet*2card ( s head + septet-base * r , s tail ) end define ]]"

Convert the big endian list "[[ s ]]" of septets to a cardinal. Septets are numbers in the range from 0 to 127, inclusive. Lists of septets represent numbers base 128. The result is accumulated in "[[ r ]]"

\item "[[ late eager define septet-base as 128 end define ]]"

\item "[[ late eager define parse-card ( v ) as parse-card1 ( true , v ) end define ]]"

Parse the cardinal at the beginning of the singleton list "[[ v ]]" and return "[[ c :: v prime ]]" where "[[ c ]]" is the cardinal and "[[ v prime ]]" is the unparsed part of "[[ v ]]". The cardinal is expressed as a little endian sequence of septets. Bytes "[[ b ]]" in the range from 128 to 255, inclusive, are treated as \emph{middle septets}; they represent the septet "[[ v - 128 ]]" and also indicate that the given septet is not the last one in the cardinal. Bytes "[[ b ]]" in the range from 0 to 127 are treated as \emph{end septets}; they represent the septet "[[ v ]]" and also indicate that the given septet is the last one in the cardinal.

\item "[[ late eager define parse-card1 ( r , v ) as newline

if v atom then exception else newline

let b :: v = v in newline

if b < NULL .or. b > V255 then exception else newline

if b < V128 then septet*2card ( 0 , b - NULL :: r ) :: v else newline

parse-card1 ( b - V128 :: r , v ) end define ]]"

\item "[[ late eager define exp10 ( e ) as if e = 0 then 1 else 10 * exp10 ( e - 1 ) end define ]]"

Raise 10 to power "[[ e ]]".

\item "[[ late eager define parse-unixTime ( v ) as newline

let f :: v = parse-card ( v first ) in newline

let s :: v = parse-card ( v ) in newline

let e :: v = parse-card ( v ) in newline

<< s * exp10 ( e ) + f ,, e >> end define ]]"

Parse the reply from unixTime of form "[[ lgcio ( c ) ]]" into a number of seconds "[[ s ]]", a fraction of seconds "[[ f ]]", and an exponent "[[ e ]]". Those values represent the value $ s + f \cdot 10 ^ { - e } $. Then return "[[ m :: e ]]" such that $ m \cdot 10 ^ { - e } = s + f \cdot 10 ^ { - e } $.

\item "[[ late eager define make-card ( c ) as newline

if c < 128 then bt2vector ( c ) else newline

bt2vector ( ( c mod 128 ) + 128 ) :: make-card ( c div 128 ) end define ]]"

Convert the cardinal "[[ c ]]" into a little endian sequence of singletons base 128. The end byte (the last byte) is in the range from 0 to 127. The middle bytes (the other bytes) are represented offset 128.

\end{statements}



\subsection{Individual lgcio requests}

Constructors for the individual commands understood by the lgcio interface are defined in the following.

\begin{statements}

\item "[[ late eager define fileWrite ( p , c ) as lgcio ( FileWrite :: p :: EOS :: c ) end define ]]"

Write the contents "[[ c ]]" to a file with pathname "[[ p ]]". If the file does not exist, create it with file permissions 666 which assigns read and write access to everybody. Most users will have a file-creation mask (umask) which restricts write access for others than the user. The reply has form "[[ lgcio ( <<>> ) ]]". In other words, the reply contains an empty byte vector. On errors, an error message is written to standard output and the lgcio interface makes the Logiweb machine exit.

\item "[[ late eager define fileWriteExec ( p , c ) as lgcio ( FileWriteExec :: p :: EOS :: c ) end define ]]"

Same as "[[ fileWrite ( p , c ) ]]" but uses file permissions 777 (read, write, and execute).

\item "[[ late eager define fileRead ( p ) as lgcio ( FileRead :: p :: EOS ) end define ]]"

Read the file with pathname "[[ p ]]". The reply has form "[[ lgcio ( c ) ]]" where "[[ c ]]" is the contents of the file encoded as a byte vector.

\item "[[ late eager define fileRm ( p ) as lgcio ( FileRm :: p :: EOS ) end define ]]"

Remove the file or symbolic link with pathname "[[ p ]]". The reply has form "[[ lgcio ( <<>> ) ]]".

\item "[[ late eager define fileSymlink ( p , l ) as lgcio ( FileSymlink :: p :: EOS :: l :: EOS ) end define ]]"

Create a symbolic link at pathname "[[ l ]]" which points to pathname "[[ p ]]". The reply has form "[[ lgcio ( <<>> ) ]]".

\item "[[ late eager define fileReadLink ( l ) as lgcio ( FileReadLink :: l :: EOS ) end define ]]"

Read the symbolic link with pathname "[[ l ]]". The reply has form "[[ lgcio ( p ) ]]" where "[[ p ]]" is the contents of the symbolic link. Note that "[[ p ]]" is not zero terminated.

\item "[[ late eager define fileMkdir ( p ) as lgcio ( FileMkdir :: p :: EOS ) end define ]]"

Create a directory with pathname "[[ p ]]". The reply has form "[[ lgcio ( <<>> ) ]]".

\item "[[ late eager define fileRmdir ( p ) as lgcio ( FileRmdir :: p :: EOS ) end define ]]"

Remove the directory with pathname "[[ p ]]". The directory must be empty. The reply has form "[[ lgcio ( <<>> ) ]]".

\item "[[ late eager define fileDir ( p ) as lgcio ( FileDir :: p :: EOS ) end define ]]"

Read the directory with pathname "[[ p ]]". The reply has form "[[ lgcio ( c ) ]]" where "[[ c ]]" is a list of strings each ended by "[[ EOS ]]". The list of strings may or may not include ``.'' and ``..''.

\item "[[ late eager define fileType ( p ) as lgcio ( FileType :: p :: EOS ) end define ]]"

Stat the given pathname. The result is of form "[[ lgcio ( t ) ]]" where "[[ t ]]" is a byte vector containing a single byte. The value of "[[ t ]]" is:

\begin{description}
\item["[[ FileTypeNonexistent ]]"] File does not exist
\item["[[ FileTypeRegular ]]"] File is regular
\item["[[ FileTypeDirectory ]]"] File is directory
\item["[[ FileTypeLink ]]"] File is link
\item["[[ FileTypeOther ]]"] Otherwise
\end{description}

\item "[[ late eager define fileTypeRead ( p ) as lgcio ( FileTypeRead :: p :: EOS ) end define ]]"

Read the file with pathname "[[ p ]]". The reply has form "[[ lgcio ( t :: c ) ]]" where "[[ t ]]" is "[[ FileTypeNonexistent ]]" or "[[ FileTypeRegular ]]". "[[ c ]]" is the contents, if any, of the file encoded as a byte vector.

\item "[[ late eager define textWrite ( p , n , c ) as lgcio ( TextWrite :: p :: EOS :: n :: EOS :: c ) end define ]]"

Same as "[[ fileWrite ( p , c ) ]]" but changes newline sequences in "[[ c ]]" to "[[ n ]]".

\item "[[ late eager define textWriteExec ( p , n , c ) as lgcio ( TextWriteExec :: p :: EOS :: n :: EOS :: c ) end define ]]"

\item "[[ late eager define fileGetCwd as lgcio ( FileGetCwd ) end define ]]"

Same as "[[ fileWriteExec ( p , c ) ]]" but changes newline sequences in "[[ c ]]" to "[[ n ]]".

\item "[[ late eager define unixTime as lgcio ( UnixTime ) end define ]]"

Return the number of seconds since the Unix epoch. Ignore leap seconds in the sense that the count stops during leap seconds.

\item "[[ late eager define demonize ( l , p , u ) as lgcio ( Demonize :: l :: EOS :: p :: EOS :: u :: EOS ) end define ]]"

Turn the running Logiweb machine into a demon by getting rid of the controlling terminal. Redirect standard output and standard error to a log file with pathname "[[ l ]]". During demonization, the Logiweb machine changes process identifier (pid). Write the pid to the file with pathname "[[ p ]]". If "[[ p ]]" is the empty string, do not write the pid to any file. Change user and group identifier (uid and gid) to the user with login name "[[ u ]]". If "[[ u ]]" is the empty string, do not change uid and gid.

\item "[[ late eager define execlp1 ( d , p , a ) as lgcio ( Execlp1 :: d :: EOS :: p :: EOS :: a :: EOS ) end define ]]"

In directory d, run the program "[[ p ]]" with argument "[[ a ]]". Search the PATH and use the current environment. Wait for the program to exit. Return the return value.

\item "[[ late eager define tcpQuery ( d , p , m , e , q ) as newline

LET floor ( m , exp10 ( e ) ) BE v IN newline

lgcio ( TcpQuery :: d :: EOS :: make-card ( p ) :: make-card ( v head ) :: newline

make-card ( v tail ) :: make-card ( e ) :: q ) end define ]]"

Send the query "[[ q ]]" to domain "[[ d ]]" port "[[ p ]]" and wait up to $ m \cdot 10 ^ { - e } $ seconds for a reply. The reply has form "[[ lgcio ( c ) ]]" where "[[ c ]]" is the response. In case of error/timeout, chop the response, i.e.\ just return all bytes received. As an example, if the domain "[[ d ]]" cannot be resolved, the response is "[[ lgcio ( <<>> ) ]]".

\end{statements}



\subsection{The lgcio interface definition}

"[ verbatim define lgcio-interface as "
/*
The lgcio interface provides all the input/output facilities
needed by the Logiweb lgc compiler.
*/

#include <stdio.h>
#include <errno.h>
#include <string.h>
#include <stdlib.h>
#include <fcntl.h>
#include <unistd.h>
#include <pwd.h>
#include <dirent.h>
#include <netdb.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <sys/time.h>
#include <sys/socket.h>
#include <sys/select.h>
#include <sys/wait.h>
#ifdef __CYGWIN__
#include <process.h>
#include <cygwin/in.h>
#endif /* __CYGWIN__ */

#define TRUE                   1
#define FALSE                  0

#define PUT0                   0
#define PUT1                   1
#define GET0                   2
#define GET1                   3

#define BUFSIZE                1048576
#define S_rw_r_r               S_IRUSR|S_IWUSR|S_IRGRP|S_IROTH

/* PATHSIZE is _POSIX_PATH_MAX, so a path of this size is supported on
 * all POSIX platforms.
 * We do not want to depend on _POSIX_PATH_MAX being defined, however */
#define PATHSIZE               256

#define FileWrite              1
#define FileWriteExec          2
#define FileRead               3
#define FileRm                 4
#define FileSymlink            5
#define FileReadLink           6
#define FileMkdir              7
#define FileRmdir              8
#define FileDir                9
#define FileType               10
#define FileTypeRead           11
#define TextWrite              12
#define TextWriteExec          13
#define FileGetCwd             14
#define UnixTime               20
#define Demonize               30
#define Execlp1                31
#define TcpQuery               40

#define FILE_TYPE_NONEXISTENT  0
#define FILE_TYPE_OTHER        1
#define FILE_TYPE_REGULAR      2
#define FILE_TYPE_DIRECTORY    3
#define FILE_TYPE_LINK         4



/* Error handling */

void die(char *msg){
  printf(""!%s\n""!,msg);
  exit(0);}

void perror1(char* msg){
  printf(""!%s: %s\n""!,msg,strerror(errno));}

void pdie(char *msg){
  perror1(msg);
  exit(0);}

void Pdie(char *msg){
  perror(msg);
  exit(-1);}

#define PDIE2(x) strcpy(pdiemsg2,x)
char pdiemsg2[BUFSIZE+1];
void pdie2(char *msg1,char *msg2){
  perror1(msg1);
  printf(""!%s: %s\n""!,msg2,pdiemsg2);
  exit(0);}

#define PDIE3(x,y) strcpy(pdiemsg2,x);strcpy(pdiemsg3,y)
char pdiemsg3[BUFSIZE+1];
void pdie3(char *msg1,char *msg2,char *msg3){
  perror1(msg1);
  printf(""!%s: %s\n""!,msg2,pdiemsg2);
  printf(""!%s: %s\n""!,msg3,pdiemsg3);
  exit(0);}

#define PDIE4(x,y,z) strcpy(pdiemsg2,x);strcpy(pdiemsg3,y);strcpy(pdiemsg4,z)
char pdiemsg4[BUFSIZE+1];
void pdie4(char *msg1,char *msg2,char *msg3,char *msg4){
  perror1(msg1);
  printf(""!%s: %s\n""!,msg2,pdiemsg2);
  printf(""!%s: %s\n""!,msg3,pdiemsg3);
  printf(""!%s: %s\n""!,msg4,pdiemsg4);
  exit(0);}



/* Argument handling */

int skipString(char buffer[],int bufsize,int bufpnt,char *msg){
  char *pnt=memchr(buffer+bufpnt,0,bufsize-bufpnt);
  if(pnt==NULL) die(msg);
  return (pnt-buffer)+1;}

int skipInt(char buffer[],int bufsize,int bufpnt,char *msg){
  char *pnt;
  for(pnt=buffer+bufpnt;(pnt-buffer)<bufsize;pnt++)
  if(((*pnt)&128)==0) return (pnt-buffer)+1;
  die(msg);}

int getInt(char *buffer){
  if(((*buffer)&128)==0) return *buffer;
  return *buffer&127+128*getInt(buffer+1);}



/* Write file */

int fileWrite2(int fd,char *pnt,char *end){
  int length;
  while(pnt!=end){
    length=write(fd,pnt,end-pnt);
    if(length<0) pdie2(""!fileWrite()/write()""!,""!path""!);
    pnt+=length;}}

int fileWrite1(int state,char buffer[],int bufsize,mode_t mode){
  static int fd;
  int bufpnt=0;
  switch(state){
  case PUT0:
    bufpnt=skipString(buffer,bufsize,1,
      ""!fileWrite(): invalid path name""!);
    fd=creat(buffer+1,mode);
    PDIE2(buffer+1);
    if(fd<0) pdie2(""!fileWrite()/open()""!,""!path""!);
  case PUT1:
    fileWrite2(fd,buffer+bufpnt,buffer+bufsize);
/*
    while(bufpnt<bufsize){
      length=write(fd,buffer+bufpnt,bufsize-bufpnt);
      if(length<0) pdie2(""!fileWrite()/write()""!,""!path""!);
      bufpnt+=length;}
*/
    return 0;
  case GET0:
    if(close(fd)!=0) pdie2(""!fileWrite()/close()""!,""!path""!);
  case GET1:
    return 0;}}

int fileWrite(int state,char buffer[],int bufsize){
  return fileWrite1(state,buffer,bufsize,0666);}

int fileWriteExec(int state,char buffer[],int bufsize){
  return fileWrite1(state,buffer,bufsize,0777);}



/* Read file */

int fileRead(int state,char buffer[],int bufsize){
  static int fd=-1;
  ssize_t length;
  switch(state){
  case PUT0:
    skipString(buffer,bufsize,1,
      ""!fileRead(): invalid path name""!);
    if(fd>=0) close(fd);
    fd=open(buffer+1,O_RDONLY);
    PDIE2(buffer+1);
    if(fd<0) pdie2(""!fileRead()/open()""!,""!path""!);
  case PUT1:
    return 0;
  case GET0:
  case GET1:
    if(fd<0) return 0;
    length=read(fd,buffer,BUFSIZE);
    if(length<0) pdie2(""!fileRead()/read()""!,""!path""!);
    if(length>0) return length;
    if(close(fd)!=0) pdie2(""!fileRead()/close()""!,""!path""!);
    fd=-1;
    return 0;}}



/* Remove file */

int fileRm(int state,char buffer[],int bufsize){
  switch(state){
  case PUT0:
    skipString(buffer,bufsize,1,""!fileRm(): invalid path name""!);
    PDIE2(buffer+1);
    if(unlink(buffer+1)&&errno!=ENOENT) pdie2(""!fileRm()/unlink()""!,""!path""!);
  case PUT1:
  case GET0:
  case GET1:
    return 0;}}



/* Symlink */

int fileSymlink(int state,char buffer[],int bufsize){
  int arg1,arg2;
  switch(state){
  case PUT0:
    arg1=1;
    arg2=skipString(buffer,bufsize,arg1,
      ""!fileSymlink(): invalid arguments""!);
    skipString(buffer,bufsize,arg2,
      ""!fileSymlink(): invalid arguments""!);
    PDIE3(buffer+arg1,buffer+arg2);
    if(symlink(buffer+arg1,buffer+arg2))
    pdie3(""!fileSymlink()/symlink()""!,""!dest""!,""!link""!);
  case PUT1:
  case GET0:
  case GET1:
    return 0;}}



/* Read link */

int fileReadLink(int state,char buffer[],int bufsize){
  int length;
  static char path[PATHSIZE];
  switch(state){
  case PUT0:
    length=skipString(buffer,bufsize,1,
      ""!fileReadLink(): invalid path name""!);
    if(length-1>PATHSIZE) die(""!fileReadLink(): invalid path""!);
    PDIE2(buffer+1);
    strcpy(path,buffer+1);
  case PUT1:
  case GET1:
    return 0;
  case GET0:
    length=readlink(path,buffer,bufsize);
    if(length<0) pdie2(""!fileReadLink()/readlink()""!,""!path""!);
    if(length>=bufsize) die(""!fileReadLink(): link too long""!);
    return length;}}



/* Make directory */

int fileMkdir(int state,char buffer[],int bufsize){
  char *bufpnt;
  int result;
  switch(state){
  case PUT0:
    skipString(buffer,bufsize,1,
      ""!fileMkdir(): invalid path name""!);
    PDIE2(buffer+1);
    result=0;
    if(buffer[1]==0) return 0;
    for(bufpnt=buffer+2;*bufpnt!=0;bufpnt++)
    if(*bufpnt=='/'){*bufpnt=0;result=mkdir(buffer+1,0777);*bufpnt='/';}
    if(result<0&&errno!=EEXIST) pdie2(""!fileMkdir()/mkdir()""!,""!path""!);
  case PUT1:
  case GET0:
  case GET1:
    return 0;}}



/* Remove directory */

int fileRmdir(int state,char buffer[],int bufsize){
  switch(state){
  case PUT0:
    skipString(buffer,bufsize,1,
      ""!fileRmdir(): invalid path name""!);
    PDIE2(buffer+1);
    if(rmdir(buffer+1)<0&&errno!=ENOENT){
      pdie2(""!fileRmdir()/rmdir()""!,""!path""!);}
  case PUT1:
  case GET0:
  case GET1:
    return 0;}}



/* Read directory */

int fileDir(int state,char buffer[],int bufsize){
  static DIR *dir=NULL;
  struct dirent *entry;
  size_t length;
  switch(state){
  case PUT0:
    skipString(buffer,bufsize,1,
      ""!fileDir(): invalid path name""!);
    if(dir!=NULL){if(closedir(dir)<0) pdie(""!fileDir()/closedir()""!);}
    dir=opendir(buffer+1);
    PDIE2(buffer+1);
    if(dir==NULL) pdie2(""!fileDir()/opendir()""!,""!path""!);
  case PUT1:
    return 0;
  case GET0:
  case GET1:
    if(dir==NULL) return 0;
    errno=0;
    entry=readdir(dir);
    if(errno!=0) pdie2(""!fileDir()/readdir()""!,""!path""!);
    if(entry==NULL){
      if(closedir(dir)<0) pdie2(""!fileDir()/closedir()""!,""!path""!);
      dir=NULL;
      return 0;}
    length=strlen(entry->d_name);
    if(length+1>bufsize)
    die(""!fileDir(): invalid directory entry""!);
    strcpy(buffer,entry->d_name);
    return length+1;}}



/* Query file existence and type */

int fileType(int state,char buffer[],int bufsize){
  struct stat buf;
  static char result;
  switch(state){
  case PUT0:
    skipString(buffer,bufsize,1,
      ""!fileType(): invalid path name""!);
    PDIE2(buffer+1);
    if(lstat(buffer+1,&buf)<0){
      if(errno==ENOENT) result=FILE_TYPE_NONEXISTENT; else
      pdie2(""!fileType()/lstat()""!,""!path""!);
      return 0;}
    if(S_ISREG(buf.st_mode)) result=FILE_TYPE_REGULAR; else
    if(S_ISDIR(buf.st_mode)) result=FILE_TYPE_DIRECTORY; else
    if(S_ISLNK(buf.st_mode)) result=FILE_TYPE_LINK; else
    result=FILE_TYPE_OTHER;
  case PUT1:
  case GET1:
    return 0;
  case GET0:
    buffer[0]=result;
    return 1;}}



/* Read file if it exists */

int fileTypeRead(int state,char buffer[],int bufsize){
  struct stat buf;
  static int fd=-1;
  ssize_t length;
  switch(state){
  case PUT0:
    skipString(buffer,bufsize,1,
      ""!fileTypeRead(): invalid path name""!);
    if(fd>=0) close(fd);
    fd=-1;
    PDIE2(buffer+1);
    if(stat(buffer+1,&buf)<0){
      if(errno==ENOENT) return 0; else
      pdie2(""!fileType()/lstat()""!,""!path""!);}
    if(S_ISDIR(buf.st_mode)) return 0;
    fd=open(buffer+1,O_RDONLY);
  case PUT1:
    return 0;
  case GET0:
    if(fd<0) {buffer[0]=FILE_TYPE_NONEXISTENT; return 1;}
    buffer[0]=FILE_TYPE_REGULAR;
    length=read(fd,buffer+1,BUFSIZE-1);
    if(length<0) pdie2(""!fileTypeRead()/read()""!,""!path""!);
    if(length>0) return length+1;
    if(close(fd)!=0) pdie2(""!fileTypeRead()/close()""!,""!path""!);
    fd=-1;
    return 1;
  case GET1:
    if(fd<0) return 0;
    length=read(fd,buffer,BUFSIZE);
    if(length<0) pdie2(""!fileTypeRead()/read()""!,""!path""!);
    if(length>0) return length;
    if(close(fd)!=0) pdie2(""!fileTypeRead()/close()""!,""!path""!);
    fd=-1;
    return 0;}}



/* Write text file */

int textWrite1(int state,char buffer[],int bufsize,mode_t mode){
  int arg1,arg2;
  static int fd;
  int bufpnt=0;
  int length;
  static char newlineseq[BUFSIZE+1];
  static int newlinelength;
  static int ignore;
  int p;
  switch(state){
  case PUT0:
    arg1=1;
    arg2=skipString(buffer,bufsize,arg1,
      ""!textWrite(): invalid path name""!);
    bufpnt=skipString(buffer,bufsize,arg2,
      ""!textWrite(): invalid newline sequence""!);
    strcpy(newlineseq,buffer+arg2);
    newlinelength=strlen(newlineseq);
    ignore=256;
    fd=creat(buffer+arg1,mode);
    PDIE2(buffer+arg1);
    if(fd<0) pdie2(""!textWrite()/open()""!,""!path""!);
  case PUT1:
    while(bufpnt<bufsize){
      if(buffer[bufpnt]==ignore){
        bufpnt++;
        ignore=256;}
      if(buffer[bufpnt]==10){
        fileWrite2(fd,newlineseq,newlineseq+newlinelength);
        bufpnt++;
        ignore=13;}
      else if(buffer[bufpnt]==13){
        fileWrite2(fd,newlineseq,newlineseq+newlinelength);
        bufpnt++;
        ignore=10;}
      else{
        for(p=bufpnt+1;p<bufsize&&buffer[p]!=10&&buffer[p]!=13;p++);
        fileWrite2(fd,buffer+bufpnt,buffer+p);
        bufpnt=p;
        ignore=256;}}
    return 0;
  case GET0:
    if(close(fd)!=0) pdie2(""!textWrite()/close()""!,""!path""!);
  case GET1:
    return 0;}}

int textWrite(int state,char buffer[],int bufsize){
  return textWrite1(state,buffer,bufsize,0666);}

int textWriteExec(int state,char buffer[],int bufsize){
  return textWrite1(state,buffer,bufsize,0777);}



/* Get Current Working Directory */

int fileGetCwd(int state,char buffer[],int bufsize){
  char *dir;
  if(state!=GET0) return 0;
  dir=getcwd(buffer,BUFSIZE);
  if(dir==0) pdie(""!fileGetCwd""!);
  return strlen(dir);}



/* Time */

#define putInt(x) {\
  if(x<0) die(""!putInt(): Negative integer""!);\
  for(;x>=128;x/=128){\
    buffer[bufpnt++]=x%128+128;\
    if(bufpnt>=bufsize) die(""!Buffer overflow""!);}\
  buffer[bufpnt++]=x;}

int unixTime(int state,char buffer[],int bufsize){
  struct timeval tv;
  int exponent=6;
  int bufpnt=0;
  if(state!=GET0) return 0;
  if(gettimeofday(&tv,NULL)) pdie(""!time()/gettimeofday()""!);
  putInt(tv.tv_usec);
  putInt(tv.tv_sec);
  putInt(exponent);
  return bufpnt;}



/* Demonize */

void demon_dief(FILE* file,char* msg){
  fprintf(file,""!demonize()/%s: %s\n""!,msg,strerror(errno));
  exit(0);}

void demon_die(char* msg){
  demon_dief(stderr,msg);}

void open_log_file(int fd0,char* path,int flags){
  int fd1;
  FILE* file=(fd0==2)?stdout:stderr;
  if(close(fd0)==-1) demon_dief(file,""!close()""!);
  fd1=open(path,flags,S_rw_r_r);
  if(fd1<0) demon_dief(file,""!open()""!);
  if(fd1==fd0) return;
  fprintf(file,
    ""!Opened fd=%d, should have opened fd=%d\n""!,fd1,fd0);
  exit(0);}

void demonize1(char* log_file,char* pid_file,char* usr_name){
  pid_t pid;
  FILE *pid_stream;
  struct passwd *user;
  int fd;
  pid=fork();
  if(pid==-1) demon_die(""!first fork()""!);
  if(pid) exit(0);
  if(setsid()==-1) demon_die(""!setsid()""!);
  pid=fork();
  if(pid==-1) demon_die(""!second fork()""!);
  if(pid) exit(0);
  if(pid_file[0]){
    fd=open(pid_file,O_WRONLY|O_CREAT|O_EXCL,S_rw_r_r);
    if(fd<0) demon_die(""!open(pid_file)""!);
    if(!(pid_stream=fdopen(fd,""!w""!))) demon_die(""!fdopen()""!);
    if(fprintf(pid_stream,""!%d\n""!,getpid())<0)
    demon_die(""!fprintf(pid_stream)""!);
    if(fclose(pid_stream)) demon_die(""!fclose(pid_stream)""!);}
  if(usr_name[0]){
    user=getpwnam(usr_name);
    if(!user) demon_die(""!getpwnam()""!);
    if(setgid(user->pw_uid)) demon_die(""!setgid()""!);
    if(setuid(user->pw_uid)) demon_die(""!setuid()""!);}
  if(chdir(""!/""!)==-1) demon_die(""!chdir()""!);
  umask(022);
  if(close(0)==-1) demon_die(""!close(0)""!);
  if(open(""!/dev/null""!,O_RDONLY)!=0) demon_die(""!open(0)""!);
  open_log_file(1,log_file,O_WRONLY|O_CREAT|O_TRUNC);
  open_log_file(2,log_file,O_WRONLY|O_CREAT|O_TRUNC);}

int demonize(int state,char buffer[],int bufsize){
  int arg1,arg2,arg3;
  switch(state){
  case PUT0:
    arg1=1;
    arg2=skipString(buffer,bufsize,arg1,
      ""!demonize(): invalid arguments""!);
    arg3=skipString(buffer,bufsize,arg2,
      ""!demonize(): invalid arguments""!);
    skipString(buffer,bufsize,arg3,
      ""!demonize(): invalid arguments""!);
    demonize1(buffer+arg1,buffer+arg2,buffer+arg3);
  case PUT1:
  case GET0:
  case GET1:
    return 0;}}



/* execlp1 */

int execlp1(int state,char buffer[],int bufsize){
  int arg1,arg2,arg3;
  int fd,fd0,fd1,fd2;
  pid_t pid;
  static int status;
  switch(state){
  case PUT0:
    arg1=1;
    arg2=skipString(buffer,bufsize,arg1,
      ""!execlp1(): invalid argument 1""!);
    arg3=skipString(buffer,bufsize,arg2,
      ""!execlp1(): invalid argument 2""!);
    skipString(buffer,bufsize,arg3,
      ""!execlp1(): invalid argument 3""!);
    PDIE4(buffer+arg1,buffer+arg2,buffer+arg3);
#ifndef __CYGWIN__
    pid=fork();
    if(pid<0) pdie(""!fork()""!);
    if(pid==0){
      if(chdir(buffer+arg1)) pdie2(""!execlp1()/chdir()""!,""!path""!);
      fd=open(""!/dev/null""!,O_RDWR);
      if(fd<0) Pdie(""!execlp1()/open(): Cannot open /dev/null""!);
      if(close(STDIN_FILENO)<0) Pdie(""!execlp1()/close() failed for stdin""!);
      if(dup2(fd,STDIN_FILENO)<0) Pdie(""!execlp1()/dup2() failed for stdin""!);
      if(close(STDOUT_FILENO)<0)
      Pdie(""!execlp1()/close() failed for stdout""!);
      if(dup2(fd,STDOUT_FILENO)<0)
      Pdie(""!execlp1()/dup2() failed for stdout""!);
      if(close(STDERR_FILENO)<0)
      Pdie(""!execlp1()/close() failed for stderr""!);
      if(dup2(fd,STDERR_FILENO)<0) exit(-1);
      execlp(buffer+arg2,buffer+arg2,buffer+arg3,(char *)NULL);
      exit(-1);}
    if(wait(&status)<0)
    pdie4(""!execlp1()/wait()""!,""!path""!,""!prog""!,""!arg""!);
#else
    if(chdir(buffer+arg1)) pdie2(""!execlp1()/chdir()""!,""!path""!);
    fd=open(""!/dev/null""!,O_RDWR);
    if(fd<0) Pdie(""!execlp1()/open(): Cannot open /dev/null""!);
    fd0=dup(STDOUT_FILENO);
    if(fd0<0) Pdie(""!execlp1()/dup(): Cannot duplicate stdin""!);
    fd1=dup(STDOUT_FILENO);
    if(fd1<0) Pdie(""!execlp1()/dup(): Cannot duplicate stdout""!);
    fd2=dup(STDOUT_FILENO);
    if(fd2<0) Pdie(""!execlp1()/dup(): Cannot duplicate stderr""!);
    if(dup2(fd,STDIN_FILENO)<0) Pdie(""!execlp1()/dup2() failed for stdin""!);
    if(dup2(fd,STDOUT_FILENO)<0) Pdie(""!execlp1()/dup2() failed for stdout""!);
    if(dup2(fd,STDERR_FILENO)<0) Pdie(""!execlp1()/dup2() failed for stderr""!);
    status=spawnlp(_P_WAIT,buffer+arg2,buffer+arg2,buffer+arg3,(char *)NULL);
    if(dup2(fd2,STDERR_FILENO)<0) Pdie(""!execlp1()/dup2() failed for fd2""!);
    if(dup2(fd1,STDOUT_FILENO)<0) Pdie(""!execlp1()/dup2() failed for fd1""!);
    if(dup2(fd0,STDIN_FILENO)<0) Pdie(""!execlp1()/dup2() failed for fd0""!);
    if(close(fd)) Pdie(""!execlp1()/close() failed for fd""!);
    if(close(fd0)) Pdie(""!execlp1()/close() failed for fd1""!);
    if(close(fd1)) Pdie(""!execlp1()/close() failed for fd1""!);
    if(close(fd2)) Pdie(""!execlp1()/close() failed for fd1""!);
#endif /* __CYGWIN__ */
  case PUT1:
  case GET1:
    return 0;
  case GET0:
    buffer[0]=(char)(-1);
    if(WIFEXITED(status)) buffer[0]=(char)(WEXITSTATUS(status));
    return 1;}}

/* tcpQuery */

void print_herror(void){
  switch(h_errno){
    case HOST_NOT_FOUND:
    fprintf(stderr,""!The specified host is unknown.\n""!);
    break;
    case NO_ADDRESS:
    fprintf(stderr,
      ""!The requested name is valid but does not have\n""!);
    fprintf(stderr,""!an IP address.\n""!);
    break;
    case NO_RECOVERY:
    fprintf(stderr,
      ""!A non-recoverable name server error occurred.\n""!);
    break;
    case TRY_AGAIN:
    fprintf(stderr,
      ""!A temporary error occurred on an authoritative\n""!);
    fprintf(stderr,""!name server. Try again later.\n""!);
    break;
    default:
    fprintf(stderr,""!Unknown error.\n""!);}}

int set_addr(struct sockaddr_in *addr,char* domain,int port){
  struct hostent *host=gethostbyname(domain);
  if(!host){
    fprintf(stderr,""!Unix call: gethostbyname(%s)\n""!,domain);
    print_herror();
    return -1;}
  addr->sin_family=AF_INET;
  addr->sin_port=htons(port);
  memcpy(&(addr->sin_addr),host->h_addr_list[0],host->h_length);
  return 0;}

#define GIVE_UP(x) {close(fd);fd=-1;return 0;}
int tcpQuery(int state,char* buffer,int bufsize){
  int arg1,arg2,arg3,arg4,arg5,arg6;
  char *domain;
  int port,secs,frac,expo;
  struct timeval tv;
  static int fd=-1;
  fd_set set;
  static long secs0,frac0;
  struct sockaddr_in to;
  ssize_t length1;
  int result;
  int flags;
  switch(state){
  case PUT0:
    arg1=1;
    arg2=skipString(buffer,bufsize,arg1,
      ""!tcpQuery(): invalid argument 1""!);
    arg3=skipInt(buffer,bufsize,arg2,
      ""!tcpQuery(): invalid argument 2""!);
    arg4=skipInt(buffer,bufsize,arg3,
      ""!tcpQuery(): invalid argument 3""!);
    arg5=skipInt(buffer,bufsize,arg4,
      ""!tcpQuery(): invalid argument 4""!);
    arg6=skipInt(buffer,bufsize,arg5,
      ""!tcpQuery(): invalid argument 5""!);
    domain=buffer+arg1;
    port=getInt(buffer+arg2);
    secs=getInt(buffer+arg3);
    frac=getInt(buffer+arg4);
    expo=getInt(buffer+arg5);
    PDIE3(buffer+arg1,buffer+arg3);
    for(;expo>6;expo--) frac/=10;
    for(;expo<6;expo++) frac*=10;
    if(gettimeofday(&tv, NULL))
    pdie3(""!tcpQuery()/gettimeofday()""!,""!domain""!,""!seconds""!);
    secs0=secs+tv.tv_sec-1;
    frac0=frac+tv.tv_usec+1000000;
    if(fd>=0) close(fd);
    fd=socket(AF_INET,SOCK_STREAM,0);
    if(fd<0) pdie3(""!tcpQuery()/socket()""!,""!domain""!,""!seconds""!);
    if(set_addr(&to,domain,port)) GIVE_UP(1)
    flags=fcntl(fd,F_GETFL,0);
    fcntl(fd,F_SETFL,flags|O_NONBLOCK);
    if(connect(fd,(void *)&to,sizeof(to))){
      if(errno!=EINPROGRESS) GIVE_UP(2);
      FD_ZERO(&set);
      FD_SET(fd,&set);
      if(gettimeofday(&tv,NULL)) 
      pdie3(""!tcpQuery()/gettimeofday()""!,""!domain""!,""!seconds""!);
      secs=secs0-tv.tv_sec;
      frac=frac0-tv.tv_usec;
      secs=secs+frac/1000000;
      frac=frac%1000000;
      if(secs<0) GIVE_UP(3)
      tv.tv_sec=secs;
      tv.tv_usec=frac;
      result=select(fd+1,0,&set,0,&tv);
      if(result<0) pdie3(""!tcpQuery()/select()""!,""!domain""!,""!seconds""!);
      if(result==0) GIVE_UP(4)
      result=select(fd+1,0,&set,0,&tv);
      if(result<0) pdie3(""!tcpQuery()/select()""!,""!domain""!,""!seconds""!);
      if(result==0) GIVE_UP(5)}
    bufsize=bufsize-arg6;
    buffer=buffer+arg6;
  case PUT1:
    do{
      FD_ZERO(&set);
      FD_SET(fd,&set);
      if(gettimeofday(&tv,NULL)) 
      pdie3(""!tcpQuery()/gettimeofday()""!,""!domain""!,""!seconds""!);
      secs=secs0-tv.tv_sec;
      frac=frac0-tv.tv_usec;
      secs=secs+frac/1000000;
      frac=frac%1000000;
      if(secs<0) GIVE_UP(6)
      tv.tv_sec=secs;
      tv.tv_usec=frac;
      result=select(fd+1,0,&set,0,&tv);
      if(result<0) pdie3(""!tcpQuery()/select()""!,""!domain""!,""!seconds""!);
      if(result==0) GIVE_UP(7)
      length1=send(fd,buffer,bufsize,0);
      if(length1<0) GIVE_UP(8)
      buffer+=length1;
      bufsize-=length1;}
    while(bufsize>0);
    return 0;
  case GET0:
  case GET1:
    if(fd<0) return 0;
    FD_ZERO(&set);
    FD_SET(fd,&set);
    if(gettimeofday(&tv,NULL)) 
    pdie3(""!tcpQuery()/gettimeofday()""!,""!domain""!,""!seconds""!);
    secs=secs0-tv.tv_sec;
    frac=frac0-tv.tv_usec;
    secs=secs+frac/1000000;
    frac=frac%1000000;
    if(secs<0) GIVE_UP(9)
    tv.tv_sec=secs;
    tv.tv_usec=frac;
    result=select(fd+1,&set,0,&set,&tv);
    if(result<0) pdie3(""!tcpQuery()/select()""!,""!domain""!,""!seconds""!);
    if(result==0) GIVE_UP(10)
    length1=recv(fd,buffer,bufsize,0);
    if(length1<=0) GIVE_UP(11)
    return length1;}}



/* Dispatch on command */

#define CASE(x,y) case x:return y(state,buffer,bufsize)
int trigger2(int state,char command,char buffer[],int bufsize){
  switch(command){
    CASE(FileWrite    ,fileWrite);
    CASE(FileWriteExec,fileWriteExec);
    CASE(FileRead     ,fileRead);
    CASE(FileRm       ,fileRm);
    CASE(FileSymlink  ,fileSymlink);
    CASE(FileReadLink ,fileReadLink);
    CASE(FileMkdir    ,fileMkdir);
    CASE(FileRmdir    ,fileRmdir);
    CASE(FileDir      ,fileDir);
    CASE(FileType     ,fileType);
    CASE(FileTypeRead ,fileTypeRead);
    CASE(TextWrite    ,textWrite);
    CASE(TextWriteExec,textWriteExec);
    CASE(FileGetCwd   ,fileGetCwd);
    CASE(UnixTime     ,unixTime);
    CASE(Demonize     ,demonize);
    CASE(Execlp1      ,execlp1);
    CASE(TcpQuery     ,tcpQuery);
    default: return 0;}}



/* Transfer one buffer */

int trigger1(int push1,char buffer[],int bufsize){
  static int push0=FALSE;
  static char command;
  if(push1){
    if(push0) return trigger2(PUT1,command,buffer,bufsize);
    push0=TRUE;
    command=buffer[0];
    return trigger2(PUT0,command,buffer,bufsize);}
  if(!push0) return trigger2(GET1,command,buffer,bufsize);
  push0=FALSE;
  return trigger2(GET0,command,buffer,bufsize);}



/* Transfer one byte */

int trigger(int c){
  static int push0=FALSE;
  static char buffer[BUFSIZE+1];
  static int bufpnt=0;
  static int bufsize;
  int push1=(c>=0);
  if(push1){
    if(!push0){push0=TRUE;bufpnt=0;}
    if(bufpnt>=BUFSIZE){trigger1(TRUE,buffer,bufpnt);bufpnt=0;}
    buffer[bufpnt++]=c;
    return -1;}
  if(push0){push0=FALSE;trigger1(TRUE,buffer,bufpnt);bufsize=0;}
  if(bufpnt>=bufsize){
    bufsize=trigger1(FALSE,buffer,BUFSIZE);
    bufpnt=0;}
  if(bufpnt>=bufsize) return -1;
  return (unsigned char)buffer[bufpnt++];}
" end define ]"



\subsection{Test of the lgcio interface}

In Section \ref{Sec:ExecutionConstructs} we defined that the lgciotest machine uses "[[ lgcio1 ]]" as handler. That handler is defined in the following. When executed, the lgciotest machine invokes all the features of the lgcio interface.

\begin{statements}

\item "[[ late eager define lgcio1 as map ( \ x . lgcio2 ( x ) ) end define ]]"

\item "[[ late eager define lgcio2 ( x ) as newline

extend request ( lgcio ( true ) , lgcio-interface ) :: newline

fileMkdir ( "testdir/" ) :: newline

fileWrite ( "testdir/testfile1" , "abc""n" ) :: newline

fileWriteExec ( "testdir/testfile2" , "def""n" ) :: newline

fileRead ( "testdir/testfile1" ) :: newline

fileRead ( "testdir/testfile2" ) :: newline

fileSymlink ( "testfile2" , "testdir/testfile3" ) :: newline

fileSymlink ( "testfile3" , "testdir/testfile4" ) :: newline

fileRead ( "testdir/testfile4" ) :: newline

fileReadLink ( "testdir/testfile4" ) :: newline

fileType ( "testdir/testfile0" ) :: newline

fileType ( "/dev/tty" ) :: newline

fileType ( "testdir/testfile1" ) :: newline

fileType ( "testdir" ) :: newline

fileType ( "testdir/testfile3" ) :: newline

fileTypeRead ( "testdir/testfile0" ) :: newline

fileTypeRead ( "testdir/testfile1" ) :: newline

fileTypeRead ( "testdir" ) :: newline

fileTypeRead ( "testdir/testfile3" ) :: newline

fileDir ( "testdir" ) :: newline

textWrite ( "testdir/testtext1" , "12" , "a""nb""nc""n" ) :: newline

textWriteExec ( "testdir/testtext2" , "12" , "d""ne""nf""n" ) :: newline

fileRead ( "testdir/testtext1" ) :: newline

fileRead ( "testdir/testtext2" ) :: newline

unixTime :: newline

write request ( "tcpQuery""n" ) :: newline

tcpQuery ( "logiweb.eu" , 80 , 21 , 1 , "GET /test.html" :: CRLF ) :: newline

unixTime :: newline

fileGetCwd :: newline

fileRm ( "testdir/testfile1" ) :: newline

fileRm ( "testdir/testfile2" ) :: newline

fileRm ( "testdir/testfile3" ) :: newline

fileRm ( "testdir/testfile4" ) :: newline

fileRm ( "testdir/testfile5" ) :: newline

fileRm ( "testdir/testtext1" ) :: newline

fileRm ( "testdir/testtext2" ) :: newline

fileRmdir ( "testdir" ) :: newline

fileRmdir ( "testdir2" ) :: newline

"";demonize ( "/home/grue/log_file" , "". , "". ) :: newline

exec request ( true , lgcio3 ) :: true end define ]]"

\item "[[ late eager define lgcio3 as map ( \ x . lgcio4 ( x ) ) end define ]]"

\item "[[ late eager define lgcio4 ( x ) as newline

if newline

println ( !"exec reply" ) .then. newline

let e :: x = x in e r= exec reply ( true , true ) .and. newline

let x = reverse ( x ) in newline

println ( !"extend reply lgcio-interface" ) .then. newline

let e :: x = x in e r= extend reply ( true ) .and. newline

println ( !"fileMkdir testdir/" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileWrite testdir/testfile1" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileWriteExec testdir/testfile2" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileRead testdir/testfile1" ) .then. newline

let e :: x = x in vt2vector ( e first ) = !"abc""n" .and. newline

println ( !"fileRead testdir/testfile2" ) .then. newline

let e :: x = x in vt2vector ( e first ) = !"def""n" .and. newline

println ( !"fileSymlink testfile2 testdir/testfile3" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileSymlink testfile3 testdir/testfile4" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileRead testdir/testfile4" ) .then. newline

let e :: x = x in vt2vector ( e first ) = !"def""n" .and. newline

println ( !"fileReadLink testdir/testfile4" ) .then. newline

let e :: x = x in vt2vector ( e first ) = "testfile3" .and. newline

println ( !"fileType testdir/testfile0" ) .then. newline

let e :: x = x in e first = FileTypeNonexistent :: true .and. newline

println ( !"fileType /dev/tty" ) .then. newline

let e :: x = x in e first = FileTypeOther :: true .and. newline

println ( !"fileType testdir/testfile1" ) .then. newline

let e :: x = x in e first = FileTypeRegular :: true .and. newline

println ( !"fileType testdir" ) .then. newline

let e :: x = x in e first = FileTypeDirectory :: true .and. newline

println ( !"fileType testdir/testfile3" ) .then. newline

let e :: x = x in e first = FileTypeLink :: true .and. newline

println ( !"fileTypeRead testdir/testfile0" ) .then. newline

let e :: x = x in e first = FileTypeNonexistent :: true .and. newline

println ( !"fileTypeRead testdir/testfile1" ) .then. newline

let e :: x = x in e first = FileTypeRegular :: "a" :: "b" :: "c" :: LF :: true .and. newline

println ( !"fileTypeRead testdir" ) .then. newline

let e :: x = x in e first = FileTypeNonexistent :: true .and. newline

println ( !"fileTypeRead testdir/testfile3" ) .then. newline

let e :: x = x in e first = FileTypeRegular :: "d" :: "e" :: "f" :: LF :: true .and. newline

println ( !"fileDir testdir" ) .then. newline

let e :: x = x in e r= lgcio ( true ) .and. newline

println ( !"textWrite testdir/testtext1" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"textWriteExec testdir/testtext2" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileRead testdir/testtext1" ) .then. newline

let e :: x = x in vt2vector ( e first ) = !"a12b12c12" .and. newline

println ( !"fileRead testdir/testtext2" ) .then. newline

let e :: x = x in vt2vector ( e first ) = !"d12e12f12" .and. newline

println ( !"unixTime" ) .then. newline

let e :: x = x in e r= lgcio ( true ) .and. trace ( parse-unixTime ( e ) ) .then. newline

println ( !"tcpQuery logiweb.eu 80 GET /test.html" ) .then. newline

let e :: x = x in e r= lgcio ( true ) .and. trace ( vt2vector ( e first ) ) .then. newline

println ( !"unixTime" ) .then. newline

let e :: x = x in e r= lgcio ( true ) .and. trace ( parse-unixTime ( e ) ) .then. newline

println ( !"fileGetCwd" ) .then. newline

let e :: x = x in e r= lgcio ( true ) .and. println ( e first ) .then. newline

println ( !"fileRm testdir/testfile1" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileRm testdir/testfile2" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileRm testdir/testfile3" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileRm testdir/testfile4" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileRm testdir/testfile5" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileRm testdir/testtext1" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileRm testdir/testtext2" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileRmdir testdir" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

println ( !"fileRmdir testdir2" ) .then. newline

let e :: x = x in e = lgcio ( true ) .and. newline

x = true then newline

<< write request ( "Test succeeded.""n" ) >> else newline

<< write request ( "Test failed.""n" ) ,, quit request ( 1 ) >> end define ]]"

\end{statements}



" ]"\section{Compiler support functions}"[ "

\subsection{General functions}

\begin{statements}

\item "[[ late eager define x last as if x tail then x head else x tail last end define ]]"

\item "[[ late eager define default ( x , y ) as if y then x else y end define ]]"

\item "[[ late eager define repeat ( n , x ) as newline

if n <= 0 then true else x :: repeat ( n - 1 , x ) end define ]]"

\end{statements}



\subsection{Conversion to mixed endian hexadecimal}

\begin{statements}

\item "[[ late eager define lgc-string2mixed ( a ) as lgc-string2mixed1 ( vt2vector* ( a ) ) end define ]]"

\item "[[ late eager define lgc-string2mixed1 ( a ) as newline

if a then true else newline

let c :: a = a in newline

let m :: n = floor ( c - NULL , 16 ) in newline

lgc-hexdigit ( m ) :: lgc-hexdigit ( n ) :: lgc-string2mixed1 ( a ) end define ]]"

\item "[[ late eager define lgc-hexdigit ( m ) as newline

if m <= 9 then m + !"0" else m + !"A" - Base end define ]]"

\end{statements}



\subsection{Rack conversion}

Recall that the rack "[[ R ]]" of a page is an array which is non-uniform in the sense that "[[ R [[ i ]] ]]" has different types for different values of "[[ i ]]". For the sake of efficiency, the lgc-compiler is able to dump the rack of a page to a file so that it can read it back again later.

We refer to a directory which contains rack files as a cache directory. Cache directories typically do not contain rack files directly. Rather, they contain directories which in turn contain the rack files. Rack files are typically named \verb+page.lgr+. The directory containing the rack file of a page is typically named "[[ a ]]" where "[[ a ]]" is the reference of the page expressed in mixed endian hexadecimal.

The "[[ rack2sl ( R ) ]]" function converts the rack "[[ R ]]" on internal form to a list of singleton strings suited for writing to a rack file.

The "[[ sl2rack ( r ) ]]" converts the other way. For racks "[[ R ]]" we have "[[ sl2rack ( rack2sl ( R ) ) = R ]]".

A rack is expressed as a sequence "[[ << s _ { 3 } ,, s _ { 4 } ,, s _ { 5 } ,, *** >> ]]" of items. Each item can be:

Each element "[[ s _ { k } ]]" can represent one of the following:

\begin{itemize}

\item A zero byte followed by a cardinal "[[ c ]]" expressed base 128 represents that cardinal.

\item A one byte represents "[[ true ]]".

\item A two byte followed by a cardinal "[[ c ]]" expressed base 128 followed by "[[ c ]]" bytes represents the vector comprising those bytes.

\item Two cardinals "[[ i ,, j < k ]]" expressed base 128 represents "[[ s _ { i } :: s _ { j } ]]".

\item One cardinal "[[ i = k ]]" expressed base 128 marks the end of the rack.

\end{itemize}

\begin{statements}

\item "[[ late optimized define rack2sl ( R ) as norm R is val : newline

if R then bt2vector* ( 3 ) else newline

let s = rack2sl1 ( R , true [[ 0 -> 3 ]] ) in newline

vt2vector* ( s [[ 2 ]] :: make-card ( s [[ 0 ]] ) ) end define ]]"

Convert the rack "[[ R ]]" to external form.

\item "[[ late eager define rack2sl1 ( R , s ) as newline

if R then s [[ 1 -> 1 ]] else newline

if R intp then rack2sl-card ( R , s ) else newline

if R pairp then rack2sl-pair ( R , s ) else exception end define ]]"

Convert the rack "[[ R ]]" to external form and store it in "[[ s [[ 2 ]] ]]". During conversion, "[[ s [[ 0 ]] ]]" is the value of the next unused index, "[[ s [[ 1 ]] ]]" is the index of the converted rack, "[[ s [[ 3 ]] [[ i ]] ]]" is the index of the cardinal "[[ i ]]", and "[[ s [[ 4 ]] [[ i ]] [[ j ]] ]]" is the index of "[[ v _ { i } :: v _ { j } ]]" where "[[ v _ { i } ]]" is the value with index "[[ i ]]".

\item "[[ late eager define rack2sl-card ( R , s ) as newline

if R < 0 then exception else newline

let i = s [[ 3 ]] [[ R ]] in newline

if .not. i then s [[ 1 -> i ]] else newline

let n = s [[ 0 ]] in newline

let s = s [[ 0 -> n + 1 ]] in newline

let s = s [[ 1 -> n ]] in newline

let s = s [[ << 3 ,, R >> => n ]] in newline

let d :: q = floor ( integer-length ( R ) , 8 ) in newline

let r = s [[ 2 ]] in newline

if q != 1 then s [[ 2 -> r :: make-card ( 0 ) :: make-card ( R ) ]] else newline

s [[ 2 -> r :: make-card ( 2 ) :: make-card ( d ) :: vector ( R ) ]] end define ]]"

Same as "[[ rack2sl1 ( R , s ) ]]" except that "[[ R ]]" is assumed to be a cardinal.

\item "[[ late eager define rack2sl-pair ( R , s ) as newline

let s = rack2sl1 ( R head , s ) in newline

let i = s [[ 1 ]] in newline

let s = rack2sl1 ( R tail , s ) in newline

let j = s [[ 1 ]] in newline

let k = s [[ 4 ]] [[ i ]] [[ j ]] in newline

if .not. k then s [[ 1 -> k ]] else newline

let n = s [[ 0 ]] in newline

let s = s [[ 0 -> n + 1 ]] in newline

let s = s [[ 1 -> n ]] in newline

let s = s [[ << 4 ,, i ,, j >> => n ]] in newline

let r = s [[ 2 ]] in newline

s [[ 2 -> r :: make-card ( i ) :: make-card ( j ) ]] end define ]]"

\item "[[ late optimized define sl2rack ( r ) as norm r is val : newline

sl2rack1 ( r , 3 , true ) end define ]]"

\item "[[ late eager define sl2rack1 ( r , n , s ) as newline

let c :: r = parse-card ( r ) in newline

if c = n then s [[ n - 1 ]] else newline

let C :: r = parse-card ( r ) in newline

if c = 0 then sl2rack1 ( r , n + 1 , s [[ n -> C ]] ) else newline

if c = 2 then sl2rack-vector ( C , r , n , s , true ) else newline

sl2rack1 ( r , n + 1 , s [[ n -> s [[ c ]] :: s [[ C ]] ]] ) end define ]]"

Convert the rack "[[ r ]]" to internal form. The "[[ n ]]" parameter is the next unused index and "[[ s ]]" must be an array which maps indices into "[[ r ]]" to values.

\item "[[ late eager define sl2rack-vector ( C , r , n , s , v ) as newline

if C = 0 then sl2rack1 ( r , n + 1 , s [[ n -> vt2vector ( v ) ]] ) else newline

let b :: r = r in newline

if b < NULL .or. b > V255 then exception else newline

sl2rack-vector ( C - 1 , r , n , s , v :: b ) end define ]]"

Accumulate the first "[[ C ]]" bytes of "[[ r ]]" in "[[ v ]]". When "[[ C ]]" reaches zero, convert "[[ v ]]" to a vector, put it in "[[ s ]]" under the next unused index, and continue conversion.

\end{statements}



\subsection{Rack cleaning and restoring}

Not all information in a rack is suited for dumping to a file. The branches of a rack which are not suited for dumping are:

\begin{itemize}

\item "[[ R [[ !"code" ]] ]]" This branch is the only branch which contains compiled code. Since rack files are platform independent, the code branch has to be reconstructed each time a rack file is read.

\item "[[ R [[ !"cluster" ]] ]]" This branch is very big, contains redundant information, and is very fast to reconstruct. For that reason, it is omitted from the rack file and reconstructed each time a rack file is read.

\item "[[ R [[ !"diagnose" ]] ]]" This branch is map-tagged and, hence, its value is computed lazily. However, when rack files are written, the value is forced to be computed and the map-tag is removed. The map-tag is added again when each time the rack file is read.

\end{itemize}

Functions for removing and restoring the three branches above are defined in the following.

\begin{statements}

\item "[[ late eager define lgr-rack-clean ( R ) as newline

let R = R [[ !"code" -> true ]] in newline

let R = R [[ !"cluster" -> true ]] in newline

let d = R [[ !"diagnose" ]] untag in newline

R [[ !"diagnose" -> d ]] end define ]]"

Remove the code and cluster branches and untag the diagnose branch of the rack "[[ R ]]".

\item "[[ late eager define lgr-cache-restore ( c ) as newline

let r = c [[ 0 ]] in newline

let d = c [[ r ]] [[ !"diagnose" ]] maptag in newline

let c = compile ( c ) in newline

c [[ << r ,, !"diagnose" >> => d ]] end define ]]"

Restore the diagnose and code branches in the cache "[[ c ]]". Note that the call to "[[ compile ( c ) ]]" verifies the page lazily, leading to a maptagged, unevaluated diagnose, but that diagnose is overwritten by the known diagnose so it is never evaluated.

\item "[[ late eager define lgr-cluster-closure ( r , C ) as newline

let c = C [[ r ]] in newline

let true :: b = c [[ r ]] [[ !"bibliography" ]] in newline

let C prime = lgr-cluster-closure1 ( b , C ) in newline

let c = c [[ << r ,, !"cluster" >> => C prime ]] in newline

let c = lgr-cluster-closure2 ( c , C prime ) in newline

C [[ r -> c ]] end define ]]"

Lookup the cache "[[ c ]]" in the cluster "[[ C ]]". Set "[[ C prime ]]" to the cluster of all transitively referenced pages and install it in the cluster branch of the rack. Then add racks of all transitively referenced pages to the cache "[[ c ]]" and install it in the cluster "[[ C ]]".

\item "[[ late eager define lgr-cluster-closure1 ( b , C ) as newline

if b atom then true else newline

let r :: b = b in newline

let C prime = lgr-cluster-closure1 ( b , C ) in newline

let C prime = C prime [[ r -> C [[ r ]] ]] in newline

lgr-array-add ( C prime , C [[ r ]] [[ r ]] [[ !"cluster" ]] ) end define ]]"

Construct the subcluster "[[ C prime ]]" of "[[ C ]]" which comprises all caches reflexively and transitively referenced from the bibliography "[[ b ]]".

\item "[[ late eager define lgr-array-add ( a , A ) as newline

if A atom then a else newline

if A head intp then a [[ A head -> A tail ]] else newline

lgr-array-add ( lgr-array-add ( a , A head ) , A tail ) end define ]]"

Add all elements of the array "[[ A ]]" to the array "[[ a ]]".

\item "[[ late eager define lgr-cluster-closure2 ( c , C ) as newline

if C atom then c else newline

let r = C head in newline

if r intp then c [[ r -> C [[ r ]] [[ r ]] ]] else newline

lgr-cluster-closure2 ( lgr-cluster-closure2 ( c , C head ) , C tail ) end define ]]"

Add all racks in the cluster "[[ C ]]" to the cache "[[ c ]]".

\end{statements}



" ]"\section{Ripemd160}

\subsection{Introduction}

Ripemd-160 is described in: H. Dobbertin, A. Bosselaers, B. Preneel, ``RIPEMD-160, a strengthened version of RIPEMD'', which is available on the net in ps and pdf. The article is an updated and corrected version of the article published in Fast Software Encryption, LNCS 1039, D. Gollmann, Ed., Springer-Verlag, 1996, pp. 71-82.

The code in the following is an adaption of C code taken from http://homes.esat.kuleuven.be/~bosselae/ripemd160.html. The software came with the following header:

\begin{verbatim}
    FILE:     rmd160.c

    CONTENTS: A sample C-implementation of the RIPEMD-160
              hash-function.
    TARGET:   any computer with an ANSI C compiler

    AUTHOR:   Antoon Bosselaers, ESAT-COSIC
    DATE:     1 March 1996
    VERSION:  1.0

    Copyright (c) Katholieke Universiteit Leuven
    1996, All Rights Reserved

Conditions for use of the RIPEMD-160 Software

The RIPEMD-160 software is freely available for use under the terms and
conditions described hereunder, which shall be deemed to be accepted by
any user of the software and applicable on any use of the software:

1. K.U.Leuven Department of Electrical Engineering-ESAT/COSIC shall for
   all purposes be considered the owner of the RIPEMD-160 software and of
   all copyright, trade secret, patent or other intellectual property
   rights therein.
2. The RIPEMD-160 software is provided on an ""!as is""! basis without
   warranty of any sort, express or implied. K.U.Leuven makes no
   representation that the use of the software will not infringe any
   patent or proprietary right of third parties. User will indemnify
   K.U.Leuven and hold K.U.Leuven harmless from any claims or liabilities
   which may arise as a result of its use of the software. In no
   circumstances K.U.Leuven R&D will be held liable for any deficiency,
   fault or other mishappening with regard to the use or performance of
   the software.
3. User agrees to give due credit to K.U.Leuven in scientific publications 
   or communications in relation with the use of the RIPEMD-160 software 
   as follows: RIPEMD-160 software written by Antoon Bosselaers, 
   available at http://www.esat.kuleuven.be/~cosicart/ps/AB-9601/.
\end{verbatim}



\subsection{Elementary 32 bit functions}

\begin{statements}

\item "[[ late eager define ripemd-mask0 as newline

ash ( 1 , 32 ) - 1 end define ]]"

A cardinal whose 32 least significant bits are one bits.

\item "[[ late eager define ripemd-mask1 ( x ) as newline

logand ( x , ripemd-mask0 ) end define ]]"

\item "[[ late eager define ripemd-rol ( x , n ) as newline

ripemd-mask1 ( logior ( ash ( x , n ) , ash ( x , n - 32 ) ) ) end define ]]"

"[[ ripemd-rol ( x , n ) ]]" cyclically rotates "[[ n ]]" bits to the left. "[[ x ]]" must be of a 32 bit cardinal and "[[ n ]]" must satisfy "[[ 0 <= n < 32 ]]".

\end{statements}



\subsection{Bit combination functions}

\begin{statements}

\item "[[ late eager define ripemd-f ( x , y , z ) as newline

logxor ( x , logxor ( y , z ) ) end define ]]"

\item "[[ late eager define ripemd-g ( x , y , z ) as newline

logior ( logand ( x , y ) , logand ( lognot ( x ) , z ) ) end define ]]"

\item "[[ late eager define ripemd-h ( x , y , z ) as newline

ripemd-mask1 ( logxor ( logior ( x , lognot ( y ) ) , z ) ) end define ]]"

\item "[[ late eager define ripemd-i ( x , y , z ) as newline

logior ( logand ( x , z ) , logand ( y , lognot ( z ) ) ) end define ]]"

\item "[[ late eager define ripemd-j ( x , y , z ) as newline

ripemd-mask1 ( logxor ( x , logior ( y , lognot ( z ) ) ) ) end define ]]"

\end{statements}



\subsection{Constants}

\begin{statements}

\item "[[ late eager define ripemd-gg-const as 1518500249 end define ]]"

\item "[[ late eager define ripemd-hh-const as 1859775393 end define ]]"

\item "[[ late eager define ripemd-ii-const as 2400959708 end define ]]"

\item "[[ late eager define ripemd-jj-const as 2840853838 end define ]]"

\item "[[ late eager define ripemd-ggg-const as 2053994217 end define ]]"

\item "[[ late eager define ripemd-hhh-const as 1836072691 end define ]]"

\item "[[ late eager define ripemd-iii-const as 1548603684 end define ]]"

\item "[[ late eager define ripemd-jjj-const as 1352829926 end define ]]"

\end{statements}



\subsection{Macros used in rounds}

\begin{statements}

\item "[[ macro define ripemd-ff ( a , b , c , d , e , x , s ); z as newline

let a = ripemd-mask1 ( a + ripemd-f ( b , c , d ) + x ) in newline

let a = ripemd-mask1 ( ripemd-rol ( a , s ) + e ) in newline

let c = ripemd-rol ( c , 10 ) in z end define ]]"

\item "[[ macro define ripemd-gg ( a , b , c , d , e , x , s ); z as newline

let a = ripemd-mask1 ( a + ripemd-g ( b , c , d ) + x + ripemd-gg-const ) in newline

let a = ripemd-mask1 ( ripemd-rol ( a , s ) + e ) in newline

let c = ripemd-rol ( c , 10 ) in z end define ]]"

\item "[[ macro define ripemd-hh ( a , b , c , d , e , x , s ); z as newline

let a = ripemd-mask1 ( a + ripemd-h ( b , c , d ) + x + ripemd-hh-const ) in newline

let a = ripemd-mask1 ( ripemd-rol ( a , s ) + e ) in newline

let c = ripemd-rol ( c , 10 ) in z end define ]]"

\item "[[ macro define ripemd-ii ( a , b , c , d , e , x , s ); z as newline

let a = ripemd-mask1 ( a + ripemd-i ( b , c , d ) + x + ripemd-ii-const ) in newline

let a = ripemd-mask1 ( ripemd-rol ( a , s ) + e ) in newline

let c = ripemd-rol ( c , 10 ) in z end define ]]"

\item "[[ macro define ripemd-jj ( a , b , c , d , e , x , s ); z as newline

let a = ripemd-mask1 ( a + ripemd-j ( b , c , d ) + x + ripemd-jj-const ) in newline

let a = ripemd-mask1 ( ripemd-rol ( a , s ) + e ) in newline

let c = ripemd-rol ( c , 10 ) in z end define ]]"

\item "[[ macro define ripemd-fff ( a , b , c , d , e , x , s ); z as newline

let a = ripemd-mask1 ( a + ripemd-f ( b , c , d ) + x ) in newline

let a = ripemd-mask1 ( ripemd-rol ( a , s ) + e ) in newline

let c = ripemd-rol ( c , 10 ) in z end define ]]"

\item "[[ macro define ripemd-ggg ( a , b , c , d , e , x , s ); z as newline

let a = ripemd-mask1 ( a + ripemd-g ( b , c , d ) + x + ripemd-ggg-const ) in newline

let a = ripemd-mask1 ( ripemd-rol ( a , s ) + e ) in newline

let c = ripemd-rol ( c , 10 ) in z end define ]]"

\item "[[ macro define ripemd-hhh ( a , b , c , d , e , x , s ); z as newline

let a = ripemd-mask1 ( a + ripemd-h ( b , c , d ) + x + ripemd-hhh-const ) in newline

let a = ripemd-mask1 ( ripemd-rol ( a , s ) + e ) in newline

let c = ripemd-rol ( c , 10 ) in z end define ]]"

\item "[[ macro define ripemd-iii ( a , b , c , d , e , x , s ); z as newline

let a = ripemd-mask1 ( a + ripemd-i ( b , c , d ) + x + ripemd-iii-const ) in newline

let a = ripemd-mask1 ( ripemd-rol ( a , s ) + e ) in newline

let c = ripemd-rol ( c , 10 ) in z end define ]]"

\item "[[ macro define ripemd-jjj ( a , b , c , d , e , x , s ); z as newline

let a = ripemd-mask1 ( a + ripemd-j ( b , c , d ) + x + ripemd-jjj-const ) in newline

let a = ripemd-mask1 ( ripemd-rol ( a , s ) + e ) in newline

let c = ripemd-rol ( c , 10 ) in z end define ]]"

\end{statements}



\subsection{Initial quintuple}

\begin{statements}

\item "[[ late eager define ripemd-init as newline

<< 1732584193 ,, 4023233417 ,, 2562383102 ,, 271733878 ,, 3285377520 >> end define ]]"

\end{statements}



\subsection{Compress function}

The "[[ ripemd-compress ( Q , X ) ]]" function combines the quintuple "[[ Q = << a ,, b ,, c ,, d ,, e >> ]]" and the array "[[ A ]]" into a new quintuple. "[[ X [[ i ]] ]]" is supposed to be a 32-bit cardinal for all "[[ i ]]" between 0 and 15, inclusive.

\begin{statements}

\item "[[ late eager define ripemd-compress ( Q , X ) as newline

let a :: b :: c :: d :: e :: true = Q in newline

let A :: B :: C :: D :: E :: true = Q in newline

ripemd-ff ( a , b , c , d , e , X [[  0 ]] , 11 ); newline
ripemd-ff ( e , a , b , c , d , X [[  1 ]] , 14 ); newline
ripemd-ff ( d , e , a , b , c , X [[  2 ]] , 15 ); newline
ripemd-ff ( c , d , e , a , b , X [[  3 ]] , 12 ); newline
ripemd-ff ( b , c , d , e , a , X [[  4 ]] ,  5 ); newline
ripemd-ff ( a , b , c , d , e , X [[  5 ]] ,  8 ); newline
ripemd-ff ( e , a , b , c , d , X [[  6 ]] ,  7 ); newline
ripemd-ff ( d , e , a , b , c , X [[  7 ]] ,  9 ); newline
ripemd-ff ( c , d , e , a , b , X [[  8 ]] , 11 ); newline
ripemd-ff ( b , c , d , e , a , X [[  9 ]] , 13 ); newline
ripemd-ff ( a , b , c , d , e , X [[ 10 ]] , 14 ); newline
ripemd-ff ( e , a , b , c , d , X [[ 11 ]] , 15 ); newline
ripemd-ff ( d , e , a , b , c , X [[ 12 ]] ,  6 ); newline
ripemd-ff ( c , d , e , a , b , X [[ 13 ]] ,  7 ); newline
ripemd-ff ( b , c , d , e , a , X [[ 14 ]] ,  9 ); newline
ripemd-ff ( a , b , c , d , e , X [[ 15 ]] ,  8 ); newline
                            
ripemd-gg ( e , a , b , c , d , X [[  7 ]] ,  7 ); newline
ripemd-gg ( d , e , a , b , c , X [[  4 ]] ,  6 ); newline
ripemd-gg ( c , d , e , a , b , X [[ 13 ]] ,  8 ); newline
ripemd-gg ( b , c , d , e , a , X [[  1 ]] , 13 ); newline
ripemd-gg ( a , b , c , d , e , X [[ 10 ]] , 11 ); newline
ripemd-gg ( e , a , b , c , d , X [[  6 ]] ,  9 ); newline
ripemd-gg ( d , e , a , b , c , X [[ 15 ]] ,  7 ); newline
ripemd-gg ( c , d , e , a , b , X [[  3 ]] , 15 ); newline
ripemd-gg ( b , c , d , e , a , X [[ 12 ]] ,  7 ); newline
ripemd-gg ( a , b , c , d , e , X [[  0 ]] , 12 ); newline
ripemd-gg ( e , a , b , c , d , X [[  9 ]] , 15 ); newline
ripemd-gg ( d , e , a , b , c , X [[  5 ]] ,  9 ); newline
ripemd-gg ( c , d , e , a , b , X [[  2 ]] , 11 ); newline
ripemd-gg ( b , c , d , e , a , X [[ 14 ]] ,  7 ); newline
ripemd-gg ( a , b , c , d , e , X [[ 11 ]] , 13 ); newline
ripemd-gg ( e , a , b , c , d , X [[  8 ]] , 12 ); newline

ripemd-hh ( d , e , a , b , c , X [[  3 ]] , 11 ); newline
ripemd-hh ( c , d , e , a , b , X [[ 10 ]] , 13 ); newline
ripemd-hh ( b , c , d , e , a , X [[ 14 ]] ,  6 ); newline
ripemd-hh ( a , b , c , d , e , X [[  4 ]] ,  7 ); newline
ripemd-hh ( e , a , b , c , d , X [[  9 ]] , 14 ); newline
ripemd-hh ( d , e , a , b , c , X [[ 15 ]] ,  9 ); newline
ripemd-hh ( c , d , e , a , b , X [[  8 ]] , 13 ); newline
ripemd-hh ( b , c , d , e , a , X [[  1 ]] , 15 ); newline
ripemd-hh ( a , b , c , d , e , X [[  2 ]] , 14 ); newline
ripemd-hh ( e , a , b , c , d , X [[  7 ]] ,  8 ); newline
ripemd-hh ( d , e , a , b , c , X [[  0 ]] , 13 ); newline
ripemd-hh ( c , d , e , a , b , X [[  6 ]] ,  6 ); newline
ripemd-hh ( b , c , d , e , a , X [[ 13 ]] ,  5 ); newline
ripemd-hh ( a , b , c , d , e , X [[ 11 ]] , 12 ); newline
ripemd-hh ( e , a , b , c , d , X [[  5 ]] ,  7 ); newline
ripemd-hh ( d , e , a , b , c , X [[ 12 ]] ,  5 ); newline

ripemd-ii ( c , d , e , a , b , X [[  1 ]] , 11 ); newline
ripemd-ii ( b , c , d , e , a , X [[  9 ]] , 12 ); newline
ripemd-ii ( a , b , c , d , e , X [[ 11 ]] , 14 ); newline
ripemd-ii ( e , a , b , c , d , X [[ 10 ]] , 15 ); newline
ripemd-ii ( d , e , a , b , c , X [[  0 ]] , 14 ); newline
ripemd-ii ( c , d , e , a , b , X [[  8 ]] , 15 ); newline
ripemd-ii ( b , c , d , e , a , X [[ 12 ]] ,  9 ); newline
ripemd-ii ( a , b , c , d , e , X [[  4 ]] ,  8 ); newline
ripemd-ii ( e , a , b , c , d , X [[ 13 ]] ,  9 ); newline
ripemd-ii ( d , e , a , b , c , X [[  3 ]] , 14 ); newline
ripemd-ii ( c , d , e , a , b , X [[  7 ]] ,  5 ); newline
ripemd-ii ( b , c , d , e , a , X [[ 15 ]] ,  6 ); newline
ripemd-ii ( a , b , c , d , e , X [[ 14 ]] ,  8 ); newline
ripemd-ii ( e , a , b , c , d , X [[  5 ]] ,  6 ); newline
ripemd-ii ( d , e , a , b , c , X [[  6 ]] ,  5 ); newline
ripemd-ii ( c , d , e , a , b , X [[  2 ]] , 12 ); newline

ripemd-jj ( b , c , d , e , a , X [[  4 ]] ,  9 ); newline
ripemd-jj ( a , b , c , d , e , X [[  0 ]] , 15 ); newline
ripemd-jj ( e , a , b , c , d , X [[  5 ]] ,  5 ); newline
ripemd-jj ( d , e , a , b , c , X [[  9 ]] , 11 ); newline
ripemd-jj ( c , d , e , a , b , X [[  7 ]] ,  6 ); newline
ripemd-jj ( b , c , d , e , a , X [[ 12 ]] ,  8 ); newline
ripemd-jj ( a , b , c , d , e , X [[  2 ]] , 13 ); newline
ripemd-jj ( e , a , b , c , d , X [[ 10 ]] , 12 ); newline
ripemd-jj ( d , e , a , b , c , X [[ 14 ]] ,  5 ); newline
ripemd-jj ( c , d , e , a , b , X [[  1 ]] , 12 ); newline
ripemd-jj ( b , c , d , e , a , X [[  3 ]] , 13 ); newline
ripemd-jj ( a , b , c , d , e , X [[  8 ]] , 14 ); newline
ripemd-jj ( e , a , b , c , d , X [[ 11 ]] , 11 ); newline
ripemd-jj ( d , e , a , b , c , X [[  6 ]] ,  8 ); newline
ripemd-jj ( c , d , e , a , b , X [[ 15 ]] ,  5 ); newline
ripemd-jj ( b , c , d , e , a , X [[ 13 ]] ,  6 ); newline

ripemd-jjj ( A , B , C , D , E , X [[  5 ]] ,  8 ); newline
ripemd-jjj ( E , A , B , C , D , X [[ 14 ]] ,  9 ); newline
ripemd-jjj ( D , E , A , B , C , X [[  7 ]] ,  9 ); newline
ripemd-jjj ( C , D , E , A , B , X [[  0 ]] , 11 ); newline
ripemd-jjj ( B , C , D , E , A , X [[  9 ]] , 13 ); newline
ripemd-jjj ( A , B , C , D , E , X [[  2 ]] , 15 ); newline
ripemd-jjj ( E , A , B , C , D , X [[ 11 ]] , 15 ); newline
ripemd-jjj ( D , E , A , B , C , X [[  4 ]] ,  5 ); newline
ripemd-jjj ( C , D , E , A , B , X [[ 13 ]] ,  7 ); newline
ripemd-jjj ( B , C , D , E , A , X [[  6 ]] ,  7 ); newline
ripemd-jjj ( A , B , C , D , E , X [[ 15 ]] ,  8 ); newline
ripemd-jjj ( E , A , B , C , D , X [[  8 ]] , 11 ); newline
ripemd-jjj ( D , E , A , B , C , X [[  1 ]] , 14 ); newline
ripemd-jjj ( C , D , E , A , B , X [[ 10 ]] , 14 ); newline
ripemd-jjj ( B , C , D , E , A , X [[  3 ]] , 12 ); newline
ripemd-jjj ( A , B , C , D , E , X [[ 12 ]] ,  6 ); newline

ripemd-iii ( E , A , B , C , D , X [[  6 ]] ,  9 ); newline 
ripemd-iii ( D , E , A , B , C , X [[ 11 ]] , 13 ); newline
ripemd-iii ( C , D , E , A , B , X [[  3 ]] , 15 ); newline
ripemd-iii ( B , C , D , E , A , X [[  7 ]] ,  7 ); newline
ripemd-iii ( A , B , C , D , E , X [[  0 ]] , 12 ); newline
ripemd-iii ( E , A , B , C , D , X [[ 13 ]] ,  8 ); newline
ripemd-iii ( D , E , A , B , C , X [[  5 ]] ,  9 ); newline
ripemd-iii ( C , D , E , A , B , X [[ 10 ]] , 11 ); newline
ripemd-iii ( B , C , D , E , A , X [[ 14 ]] ,  7 ); newline
ripemd-iii ( A , B , C , D , E , X [[ 15 ]] ,  7 ); newline
ripemd-iii ( E , A , B , C , D , X [[  8 ]] , 12 ); newline
ripemd-iii ( D , E , A , B , C , X [[ 12 ]] ,  7 ); newline
ripemd-iii ( C , D , E , A , B , X [[  4 ]] ,  6 ); newline
ripemd-iii ( B , C , D , E , A , X [[  9 ]] , 15 ); newline
ripemd-iii ( A , B , C , D , E , X [[  1 ]] , 13 ); newline
ripemd-iii ( E , A , B , C , D , X [[  2 ]] , 11 ); newline

ripemd-hhh ( D , E , A , B , C , X [[ 15 ]] ,  9 ); newline
ripemd-hhh ( C , D , E , A , B , X [[  5 ]] ,  7 ); newline
ripemd-hhh ( B , C , D , E , A , X [[  1 ]] , 15 ); newline
ripemd-hhh ( A , B , C , D , E , X [[  3 ]] , 11 ); newline
ripemd-hhh ( E , A , B , C , D , X [[  7 ]] ,  8 ); newline
ripemd-hhh ( D , E , A , B , C , X [[ 14 ]] ,  6 ); newline
ripemd-hhh ( C , D , E , A , B , X [[  6 ]] ,  6 ); newline
ripemd-hhh ( B , C , D , E , A , X [[  9 ]] , 14 ); newline
ripemd-hhh ( A , B , C , D , E , X [[ 11 ]] , 12 ); newline
ripemd-hhh ( E , A , B , C , D , X [[  8 ]] , 13 ); newline
ripemd-hhh ( D , E , A , B , C , X [[ 12 ]] ,  5 ); newline
ripemd-hhh ( C , D , E , A , B , X [[  2 ]] , 14 ); newline
ripemd-hhh ( B , C , D , E , A , X [[ 10 ]] , 13 ); newline
ripemd-hhh ( A , B , C , D , E , X [[  0 ]] , 13 ); newline
ripemd-hhh ( E , A , B , C , D , X [[  4 ]] ,  7 ); newline
ripemd-hhh ( D , E , A , B , C , X [[ 13 ]] ,  5 ); newline

ripemd-ggg ( C , D , E , A , B , X [[  8 ]] , 15 ); newline
ripemd-ggg ( B , C , D , E , A , X [[  6 ]] ,  5 ); newline
ripemd-ggg ( A , B , C , D , E , X [[  4 ]] ,  8 ); newline
ripemd-ggg ( E , A , B , C , D , X [[  1 ]] , 11 ); newline
ripemd-ggg ( D , E , A , B , C , X [[  3 ]] , 14 ); newline
ripemd-ggg ( C , D , E , A , B , X [[ 11 ]] , 14 ); newline
ripemd-ggg ( B , C , D , E , A , X [[ 15 ]] ,  6 ); newline
ripemd-ggg ( A , B , C , D , E , X [[  0 ]] , 14 ); newline
ripemd-ggg ( E , A , B , C , D , X [[  5 ]] ,  6 ); newline
ripemd-ggg ( D , E , A , B , C , X [[ 12 ]] ,  9 ); newline
ripemd-ggg ( C , D , E , A , B , X [[  2 ]] , 12 ); newline
ripemd-ggg ( B , C , D , E , A , X [[ 13 ]] ,  9 ); newline
ripemd-ggg ( A , B , C , D , E , X [[  9 ]] , 12 ); newline
ripemd-ggg ( E , A , B , C , D , X [[  7 ]] ,  5 ); newline
ripemd-ggg ( D , E , A , B , C , X [[ 10 ]] , 15 ); newline
ripemd-ggg ( C , D , E , A , B , X [[ 14 ]] ,  8 ); newline

ripemd-fff ( B , C , D , E , A , X [[ 12 ]] ,  8 ); newline
ripemd-fff ( A , B , C , D , E , X [[ 15 ]] ,  5 ); newline
ripemd-fff ( E , A , B , C , D , X [[ 10 ]] , 12 ); newline
ripemd-fff ( D , E , A , B , C , X [[  4 ]] ,  9 ); newline
ripemd-fff ( C , D , E , A , B , X [[  1 ]] , 12 ); newline
ripemd-fff ( B , C , D , E , A , X [[  5 ]] ,  5 ); newline
ripemd-fff ( A , B , C , D , E , X [[  8 ]] , 14 ); newline
ripemd-fff ( E , A , B , C , D , X [[  7 ]] ,  6 ); newline
ripemd-fff ( D , E , A , B , C , X [[  6 ]] ,  8 ); newline
ripemd-fff ( C , D , E , A , B , X [[  2 ]] , 13 ); newline
ripemd-fff ( B , C , D , E , A , X [[ 13 ]] ,  6 ); newline
ripemd-fff ( A , B , C , D , E , X [[ 14 ]] ,  5 ); newline
ripemd-fff ( E , A , B , C , D , X [[  0 ]] , 15 ); newline
ripemd-fff ( D , E , A , B , C , X [[  3 ]] , 13 ); newline
ripemd-fff ( C , D , E , A , B , X [[  9 ]] , 11 ); newline
ripemd-fff ( B , C , D , E , A , X [[ 11 ]] , 11 ); newline

let a prime :: b prime :: c prime :: d prime :: e prime :: true = Q in newline

let A prime = ripemd-mask1 ( b prime + c + D ) in newline

let B prime = ripemd-mask1 ( c prime + d + E ) in newline

let C prime = ripemd-mask1 ( d prime + e + A ) in newline

let D prime = ripemd-mask1 ( e prime + a + B ) in newline

let E prime = ripemd-mask1 ( a prime + b + C ) in newline

<< A prime ,, B prime ,, C prime ,, D prime ,, E prime >> end define ]]"

\end{statements}



\subsection{Conversion of buffer to array}

\begin{statements}

\item "[[ late eager define ripemd-buffer2array ( B ) as newline

ripemd-buffer2array1 ( B , 0 , true ) end define ]]"

\item "[[ late eager define ripemd-buffer2array1 ( B , n , X ) as newline

if n >= 16 then X :: B else newline

let c = ripemd-mask1 ( vt2vector ( list-prefix ( B , 4 ) ) ) in newline

let B = list-suffix ( B , 4 ) in newline

let X = X [[ n -> c ]] in newline

ripemd-buffer2array1 ( B , n + 1 , X ) end define ]]"

\item "[[ late eager define ripemd-chunk as 64 end define ]]"

\item "[[ late eager define ripemd-pad as repeat ( ripemd-chunk , NULL ) end define ]]"

\end{statements}



\subsection{Conversion of buffer to Ripemd-160 code}

\begin{statements}

\item "[[ late optimized define ripemd ( B ) as norm B is val : newline

let B = vt2vector* ( B ) in newline

let l = length ( B ) in newline

let Q = ripemd1 ( l , l , ripemd-init , B ) in newline

ripemd2 ( Q ) end define ]]"

Convert the singleton list "[[ B ]]" to a Ripemd-160 hash code. The hash code is also expressed as a singleton list.

\item "[[ late eager define ripemds ( s ) as newline

vt2vector ( lgc-string2mixed ( ripemd ( s ) ) ) end define ]]"

Same as above but takes a string as input and delivers a string in mixed endian hexadecimal as output.

\item "[[ late eager define ripemd1 ( L , l , Q , B ) as newline

if l < ripemd-chunk then ripemd-finish ( L , l , Q , B ) else

let X :: B = ripemd-buffer2array ( B ) in newline

let Q = ripemd-compress ( Q , X ) in newline

ripemd1 ( l , l - ripemd-chunk , Q , B ) end define ]]"

Successively compress the buffer "[[ B ]]" into the quintuple "[[ Q ]]". "[[ L ]]" and "[[ l ]]" are the original and remaining length of "[[ B ]]", respectively.

\item "[[ late eager define ripemd-finish ( L , l , Q , B ) as newline

let B = append ( B , V128 :: ripemd-pad ) in newline

let X :: B = ripemd-buffer2array ( B ) in newline

if l < 56 then ripemd-compress ( Q , ripemd-length ( X , L ) ) else newline

let Q = ripemd-compress ( Q , X ) in newline

let X :: B = ripemd-buffer2array ( ripemd-pad ) in newline

ripemd-compress ( Q , ripemd-length ( X , L ) ) end define ]]"

Pad the buffer "[[ B ]]" with an end byte followed by zeros, put the original length of "[[ B ]]" in "[[ X [[ 14 ]] ]]" and "[[ X [[ 15 ]] ]]", and do a final compress. If "[[ B ]]" plus end byte occupies all or part of "[[ X [[ 14 ]] ]]" and "[[ X [[ 15 ]] ]]" then "[[ B ]]" is padded with an additional chunk of zeros.

\item "[[ late eager define ripemd-length ( X , L ) as newline

let X = X [[ 14 -> ripemd-mask1 ( ash ( L , 3 ) ) ]] in

X [[ 15 -> ripemd-mask1 ( ash ( L , -29 ) ) ]] end define ]]"

Place the original length "[[ L ]]" of the buffer in "[[ X [[ 14 ]] ]]" and "[[ X [[ 15 ]] ]]".

\item "[[ late eager define ripemd2 ( Q ) as newline

if Q then true else newline

let C :: Q = Q in newline

let C = vt2vector* ( C + ash ( 1 , 32 ) ) in newline

append ( C , ripemd2 ( Q ) ) end define ]]"

Convert quintuple "[[ Q ]]" to a list of singleton strings.

\end{statements}



\printindex



\bibliography{./page}



\end{document}
" end text ,,



latex ( "page" ) ,,
makeindex ( "page" ) ,,
bibtex ( "page" ) ,,
latex ( "page" ) ,,
makeindex ( "page" ) ,,
latex ( "page" ) ,,
dvipdfm ( "page" ) ,,



text "chores.tex" : ""-"";

\documentclass[fleqn]{article}

% Include definitions generated by the Logiweb compiler
\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=UseNone}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle=A Logiweb base 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 base page - chores}
\author{Klaus Grue}
\maketitle
\tableofcontents



\section{\TeX\ definitions}

\begin{statements}

\item "[[ tex show define proclaim x as y end proclaim as "
[ "[ texshow x end texshow ]"
\bowtie "[ texshow y end texshow ]"
]" end define ]]"

\item "[[ tex use define lgcend as "\mbox{}" end define ]]"

\item "[[ tex show define lgcvar as "
\mbox{\tt\char34}" end define ]]"

\item "[[ tex show define lgcdef x of y as z enddef as "
[ def
\linebreak [0]\ "[ x ]"
\linebreak [0]\ of
\linebreak [0]\ "[ texshow y end texshow ]"
\linebreak [0]\ as
\linebreak [0]\ "[ texshow z end texshow ]"
]" end define ]]"

\item "[[ tex use define lgcname as "
name" end define ]]"

\item "[[ tex use define lgccharge as "
charge" end define ]]"

\item "[[ tex use define empty as "". end define ]]"

\item "[[ tex use define preassociative x greater than y as "
\newline \mathbf {Preassociative} \newline "[ x ]"
; "[ y ]"". end define ]]"

\item "[[ tex show define preassociative x greater than y as "
\mathbf{Preassociative}\,"[ x ]"
; "[ y ]"". end define ]]"

\item "[[ tex use define postassociative x greater than y as "
\newline\mathbf{Postassociative} \newline "[ x ]"
; "[ y ]"". end define ]]"

\item "[[ tex show define postassociative x greater than y as "
\mathbf{Postassociative}\,"[ x ]"
; "[ y ]"". end define ]]"

\item "[[ tex use define priority x equal y as "
["[ texshow x end texshow ]"
] , \linebreak [0] "[ y ]"". end define ]]"

\item "[[ tex show define priority x equal y as "
["[ x ]"
] , \linebreak [0] "[ y ]"". end define ]]"

\item "[[ tex use define priority x end priority as "
["[ texshow x end texshow ]"
]" end define ]]"

\item "[[ tex show define priority x end priority as "
priority \ "[ x ]"
\ end" end define ]]"

\item "[[ tex show define asterisk as "
\ast " end define ]]"

\item "[[ tex show define name as "
name" end define ]]"

\item "[[ tex show define define x of y as z end define as "
[ "[ texshow y end texshow ]"
\stackrel{"[ x ]"
}{\rightarrow}"[ z ]"
]" end define ]]"

\item "[[ tex use define math x end math as "$"[ x ]"$" end define ]]"

\item "[[ tex show define math x end math as "
\ \$"[ x ]"\$\linebreak[0]\ " end define ]]"

\item "[[ tex use define display math x end math as "$$"[ x ]"$$" end define ]]"

\item "[[ tex show define display math x end math as "
\ \$\$"[ x ]"\$\$\linebreak[0]\ " end define ]]"

\item "[[ tex use define ensure math x end math as "
\ensuremath{ "[ x ]"
}" end define ]]"

\item "[[ tex show define ensure math x end math as "
\backslash ensuremath \{ "[ x ]"
\}" end define ]]"

\item "[[ tex show define a as "
\mathit{a}" end define ]]"

\item "[[ tex show define b as "
\mathit{b}" end define ]]"

\item "[[ tex show define c as "
\mathit{c}" end define ]]"

\item "[[ tex show define d as "
\mathit{d}" end define ]]"

\item "[[ tex show define e as "
\mathit{e}" end define ]]"

\item "[[ tex show define f as "
\mathit{f}" end define ]]"

\item "[[ tex show define g as "
\mathit{g}" end define ]]"

\item "[[ tex show define h as "
\mathit{h}" end define ]]"

\item "[[ tex show define i as "
\mathit{i}" end define ]]"

\item "[[ tex show define j as "
\mathit{j}" end define ]]"

\item "[[ tex show define k as "
\mathit{k}" end define ]]"

\item "[[ tex show define l as "
\mathit{l}" end define ]]"

\item "[[ tex show define m as "
\mathit{m}" end define ]]"

\item "[[ tex show define n as "
\mathit{n}" end define ]]"

\item "[[ tex show define o as "
\mathit{o}" end define ]]"

\item "[[ tex show define p as "
\mathit{p}" end define ]]"

\item "[[ tex show define q as "
\mathit{q}" end define ]]"

\item "[[ tex show define r as "
\mathit{r}" end define ]]"

\item "[[ tex show define s as "
\mathit{s}" end define ]]"

\item "[[ tex show define t as "
\mathit{t}" end define ]]"

\item "[[ tex show define u as "
\mathit{u}" end define ]]"

\item "[[ tex show define v as "
\mathit{v}" end define ]]"

\item "[[ tex show define w as "
\mathit{w}" end define ]]"

\item "[[ tex show define x as "
\mathit{x}" end define ]]"

\item "[[ tex show define y as "
\mathit{y}" end define ]]"

\item "[[ tex show define z as "
\mathit{z}" end define ]]"

\item "[[ tex show define A as "
\mathit{A}" end define ]]"

\item "[[ tex show define B as "
\mathit{B}" end define ]]"

\item "[[ tex show define C as "
\mathit{C}" end define ]]"

\item "[[ tex show define D as "
\mathit{D}" end define ]]"

\item "[[ tex show define E as "
\mathit{E}" end define ]]"

\item "[[ tex show define F as "
\mathit{F}" end define ]]"

\item "[[ tex show define G as "
\mathit{G}" end define ]]"

\item "[[ tex show define H as "
\mathit{H}" end define ]]"

\item "[[ tex show define I as "
\mathit{I}" end define ]]"

\item "[[ tex show define J as "
\mathit{J}" end define ]]"

\item "[[ tex show define K as "
\mathit{K}" end define ]]"

\item "[[ tex show define L as "
\mathit{L}" end define ]]"

\item "[[ tex show define M as "
\mathit{M}" end define ]]"

\item "[[ tex show define N as "
\mathit{N}" end define ]]"

\item "[[ tex show define O as "
\mathit{O}" end define ]]"

\item "[[ tex show define P as "
\mathit{P}" end define ]]"

\item "[[ tex show define Q as "
\mathit{Q}" end define ]]"

\item "[[ tex show define R as "
\mathit{R}" end define ]]"

\item "[[ tex show define S as "
\mathit{S}" end define ]]"

\item "[[ tex show define T as "
\mathit{T}" end define ]]"

\item "[[ tex show define U as "
\mathit{U}" end define ]]"

\item "[[ tex show define V as "
\mathit{V}" end define ]]"

\item "[[ tex show define W as "
\mathit{W}" end define ]]"

\item "[[ tex show define X as "
\mathit{X}" end define ]]"

\item "[[ tex show define Y as "
\mathit{Y}" end define ]]"

\item "[[ tex show define Z as "
\mathit{Z}" end define ]]"

\item "[[ tex show define true as "
\mathsf{T}" end define ]]"

\item "[[ tex show define quote x end quote as "
\lceil "[ x ]"
\rceil " end define ]]"

\item "[[ tex show define optimized define x of y as z end define as "
["[ texshow y end texshow ]"
\stackrel {"[ x ]"
}{\rightarrow\rightarrow }"[ z ]"
]" end define ]]"

\item "[[ tex show define tex use as "
use" end define ]]"

\item "[[ tex show define tex show as "
show" end define ]]"

\item "[[ tex show define priority as "
prio" end define ]]"

\item "[[ tex show define value as "
val" end define ]]"

\item "[[ tex show define macro as "
macro" end define ]]"

\item "[[ tex show define claim as "
claim" end define ]]"

\item "[[ tex show define message as "
msg" end define ]]"

\item "[[ tex use define show x end show as "".[ texshow x end texshow ]"". end define ]]"

\item "[[ tex use define !x as "".[ texshow x end texshow ]"". end define ]]"

\item "[[ tex show define show x end show as "
show("[ x ]"
)" end define ]]"

\item "[[ tex use define macro show x end show as "".[ texshow x end texshow ]"". end define ]]"

\item "[[ tex show define macro show x end show as "
macroshow("[ x ]"
)" end define ]]"

\item "[[ tex use define hiding show x end show as "".[ texshow x end texshow ]"". end define ]]"

\item "[[ tex show define hiding show x end show as "
hideshow("[ x ]"
)" end define ]]"

\item "[[ tex use define hide x end hide as x end define ]]"

\item "[[ tex show define hide x end hide as "
hide("[ x ]"
)" end define ]]"

\item "[[ tex use define array ( x ) y end array as "
\begin{array}{"[ x ]"}
"[ y ]"
\end{array}" end define ]]"

\item "[[ tex show define array ( x ) y end array as "
array("[ x ]"
)\{"[ y ]"
\}" end define ]]"

\item "[[ tex show define left as "l" end define ]]"

\item "[[ tex show define center as "c" end define ]]"

\item "[[ tex show define right as "r" end define ]]"

\item "[[ tex use define %% as "". end define ]]"

\item "[[ tex show define %% as "\{\}" end define ]]"

\item "[[ tex show define ( x ) as "
("[ x ]"
)" end define ]]"

\item "[[ tex use define include ( x ) as "
include ( \cdots ) " end define ]]"

\item "[[ tex show define < x | y := z > as "
\langle "[ x ]"
\,{|}"[ y ]"
{:=}\,"[ z ]"
\rangle " end define ]]"

\item "[[ tex show define bottom as "
\bot " end define ]]"

\item "[[ tex show define false as "
\mathsf{F}" end define ]]"

\item "[[ tex show define Define x of y as z end define as "
[ "[ texshow y end texshow ]"
\stackrel{"[ texshow x end texshow ]"
!}{\rightarrow}"[ texshow z end texshow ]"
]" end define ]]"

\item "[[ tex show define ... as "
\ldots " end define ]]"

\item "[[ tex show define *** as "
\cdots " end define ]]"

\item "[[ tex show define exception as "
\bullet " end define ]]"

\item "[[ tex show define 0 as "
0" end define ]]"

\item "[[ tex show define 1 as "
1" end define ]]"

\item "[[ tex show define 2 as "
2" end define ]]"

\item "[[ tex show define 3 as "
3" end define ]]"

\item "[[ tex show define 4 as "
4" end define ]]"

\item "[[ tex show define 5 as "
5" end define ]]"

\item "[[ tex show define 6 as "
6" end define ]]"

\item "[[ tex show define 7 as "
7" end define ]]"

\item "[[ tex show define 8 as "
8" end define ]]"

\item "[[ tex show define 9 as "
9" end define ]]"

\item "[[ tex use define diagnose x end diagnose as x end define ]]"

\item "[[ tex show define YY as "
\mathsf{Y}" end define ]]"

\item "[[ tex show define protect x end protect as "
protect("[ x ]"
)" end define ]]"

\item "[[ tex show define root protect x end protect as "
root\ protect( "[ x ]"
)" end define ]]"

\item "[[ tex show define render define x as y end define as "
[ "[ texshow x end texshow ]"
\stackrel{render}{=} "[ texshow y end texshow ]"
]" end define ]]"

\item "[[ tex show define tex use define x as y end define as "
[ "[ texshow x end texshow ]"
\stackrel{use}{=} "[ texshow y end texshow ]"
]" end define ]]"

\item "[[ tex show define tex show define x as y end define as "
[ "[ texshow x end texshow ]"
\stackrel{show}{=} "[ texshow y end texshow ]"
]" end define ]]"

\item "[[ tex show define value define x as y end define as "
[ "[ texshow x end texshow ]"
\mathrel{\dot{=}} "[ y ]"
]" end define ]]"

\item "[[ tex show define message define x as y end define as "
[ "[ texshow x end texshow ]"
\stackrel{msg}{=} "[ y ]"
]" end define ]]"

\item "[[ tex show define execute define x as y end define as "
[ "[ texshow x end texshow ]"
\stackrel{exec}{=} "[ y ]"
]" end define ]]"

\item "[[ tex show define Macro define x as y end define as "
[ "[ texshow x end texshow ]"
\stackrel{\circ}{=} "[ y ]"
]" end define ]]"

\item "[[ tex show define macro define x as y end define as "
[ "[ texshow x end texshow ]"
\mathrel{\ddot{=}} "[ y ]"
]" end define ]]"

\item "[[ tex use define priority table x as "
\mathbf{Priority\ table} \linebreak[4] "[ x ]"". end define ]]"

\item "[[ tex show define priority table x as "
\mathbf{Priority\ table} \ "[ x ]"". end define ]]"

\item "[[ tex show define verifier x end verifier as "
[ \mathbf{Verifier\colon} "[ x ]"
]" end define ]]"

\item "[[ tex show define unpacker x end unpacker as "
[ \mathbf{Unpacker\colon} "[ x ]"
]" end define ]]"

\item "[[ tex show define renderer x end renderer as "
[ \mathbf{Renderer\colon} "[ x ]"
]" end define ]]"

\item "[[ tex show define expander x end expander as "
[ \mathbf{Expander\colon} "[ x ]"
]" end define ]]"

\item "[[ tex use define ragged right as "
\raggedright" end define ]]"

\item "[[ tex show define ragged right as "
\backslash raggedright " end define ]]"

\item "[[ tex use define make macro expanded version ragged right as "". end define ]]"

\item "[[ tex show define <<>> as "
\langle \, \rangle" end define ]]"

\item "[[ tex show define << x >> as "
\langle "[ x ]"
\rangle " end define ]]"

\item "[[ tex show define eager define x as y end define as "
[ "[ texshow x end texshow ]"
\stackrel{\bullet}{=} "[ y ]"
]" end define ]]"

\item "[[ tex show define late eager define x as y end define as "
[ "[ texshow x end texshow ]"
\stackrel{\bullet\bullet}{=} "[ y ]"
]" end define ]]"

\item "[[ tex show define late optimized define x as y end define as "
["[ texshow x end texshow ]"
\stackrel {Late}{\rightarrow\rightarrow }"[ y ]"
]" end define ]]"

\item "[[ tex show define eager message define x as y end define as "
[ message\ "[ texshow x end texshow ]"
: "[ texshow y end texshow ]"
]" end define ]]"

\item "[[ tex show define destructure as "
dest" end define ]]"

\item "[[ tex show define destructure define x as y end define as "
[ "[ texshow x end texshow ]"
\stackrel{dest}{=} "[ y ]"
]" end define ]]"

\item "[[ tex show define back x quote y end quote as "
\lceil_{\!"[ x ]"
\,} "[ y ]"
\rceil " end define ]]"

\item "[[ tex use define text x : y end text as "text"[ x ]y end define ]]"

\item "[[ macro define verbatim define x as y end define as ensure math eager define x as show y end show end define end math end define ]]"

\item "[[ tex use define verbatim define x as y end define as "
$ "[ x ]"
\stackrel{\bullet}{=} {} $
\begin{verbatim}"[ y ]"
\end{verbatim}" end define ]]"

\item "[[ tex use define tex ( x ) as "tex",x end define ]]"

\item "[[ tex use define latex ( x ) as "latex",x end define ]]"

\item "[[ tex use define bibtex ( x ) as "bibtex",x end define ]]"

\item "[[ tex use define makeindex ( x ) as "makeindex",x end define ]]"

\item "[[ tex use define dvipdfm ( x ) as "dvipdfm",x end define ]]"

\item "[[ tex show define page ( x , y ) title t bib b main text m appendix a end page as "
page ( "[ x ]"
 , "[ y ]"
 , "[ t ]"
 , "[ b ]"
 , "[ m ]"
 , "[ a ]"
 ) " end define ]]"

\item "[[ tex use define page ( x , y ) title t bib b main text m appendix a end page as

tex-file ( "text" , "index.html" , ""-"";
<head><title>"[ t ]"</title></head>
<body><h2>"[ t ]"</h2>
<p><a href='../index.html'>Up</a></p>
<p>Contents:
<a href='page.pdf'>Main text</a>
<a href='appendix.pdf'>Appendix</a>
<a href='chores.pdf'>Chores</a>
</p>
<p><address>The
<a href=""!http://logiweb.eu/""!>Logiweb</a> compiler</address></p>
</body>
" ) ,,

tex-file ( "text" , "page.bib" , b ) ,,

tex-file ( "text" , "page.tex" , ""-"";
\documentclass[fleqn]{article}
% Include definitions generated by the Logiweb compiler
\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=UseNone}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle="[ t ]"}
\hypersetup{colorlinks=true}
% Construct for listing statements with associated explanations
\newenvironment{statements}{\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}}{\end{list}}
\begin{document}
"[ m ]"
\end{document}
" ) ,,
tex-command ( "latex" , "page" ) ,,
tex-command ( "bibtex" , "page" ) ,,
tex-command ( "makeindex" , "page" ) ,,
tex-command ( "latex" , "page" ) ,,
tex-command ( "latex" , "page" ) ,,
tex-command ( "dvipdfm" , "page" ) ,,

tex-file ( "text" , "appendix.tex" , ""-"";
\documentclass[fleqn]{article}
% Include definitions generated by the Logiweb compiler
\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=UseNone}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle="[ t ]" - appendix}
\hypersetup{colorlinks=true}
% Construct for listing statements with associated explanations
\newenvironment{statements}{\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}}{\end{list}}
\begin{document}
"[ a ]"
\end{document}
" ) ,,
tex-command ( "latex" , "appendix" ) ,,
tex-command ( "latex" , "appendix" ) ,,
tex-command ( "latex" , "appendix" ) ,,
tex-command ( "dvipdfm" , "appendix" ) ,,

tex-file ( "text" , "chores.tex" , ""-"";
\documentclass[fleqn]{article}
% Include definitions generated by the Logiweb compiler
\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=UseNone}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 730}}
\hypersetup{pdftitle="[ t ]" - 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{"[ t ]"}
\author{The \href{http://logiweb.eu/}{Logiweb} compiler}
\maketitle
\tableofcontents
\section{Name definitions}
\begin{flushleft}
$ "[ x ]" $
\end{flushleft}
\section{Charge definitions}
\begin {flushleft}
$ "[ y ]" $
\end {flushleft}
\end{document}
" ) ,,
tex-command ( "latex" , "chores" ) ,,
tex-command ( "latex" , "chores" ) ,,
tex-command ( "latex" , "chores" ) ,,
tex-command ( "dvipdfm" , "chores" )

end define ]]"



\item "[[ tex show define -x as "
{}^{-}\! ",x end define ]]"

\item "[[ tex show define +x as "
{}^{+}\! ",x end define ]]"

\item "[[ tex use define tight newline x as "
\newline "[ x ]"". end define ]]"



\item "[[ tex show define x factorial as "".[ x ]"
!" end define ]]"

\item "[[ tex use define x _ { y } as "".[ x ]"
_{"[ y ]"
}" end define ]]"

\item "[[ tex use define x_y as "".[ x ]"
_{"[ y ]"
}" end define ]]"

\item "[[ tex use define x prime as "".[ x ]"
{}' " end define ]]"

\item "[[ tex show define x %0 as "".[ x ]"0" end define ]]"

\item "[[ tex show define x %1 as "".[ x ]"1" end define ]]"

\item "[[ tex show define x %2 as "".[ x ]"2" end define ]]"

\item "[[ tex show define x %3 as "".[ x ]"3" end define ]]"

\item "[[ tex show define x %4 as "".[ x ]"4" end define ]]"

\item "[[ tex show define x %5 as "".[ x ]"5" end define ]]"

\item "[[ tex show define x %6 as "".[ x ]"6" end define ]]"

\item "[[ tex show define x %7 as "".[ x ]"7" end define ]]"

\item "[[ tex show define x %8 as "".[ x ]"8" end define ]]"

\item "[[ tex show define x %9 as "".[ x ]"9" end define ]]"

\item "[[ tex show define x head as "".[ x ]"
{}^h" end define ]]"

\item "[[ tex show define x tail as "".[ x ]"
{}^t" end define ]]"

\item "[[ tex show define x raise as "".[ x ]"
{}^{\bullet}" end define ]]"

\item "[[ tex show define x catch as "".[ x ]"
{}^{\circ}" end define ]]"

\item "[[ tex show define x catching maptag as "".[ x ]"
{}^{M^{\circ}}" end define ]]"

\item "[[ tex show define x maptag as "".[ x ]"
{}^M" end define ]]"

\item "[[ tex show define x untag as "".[ x ]"
{}^U" end define ]]"

\item "[[ tex show define x root as "".[ x ]"
{}^R" end define ]]"

\item "[[ tex show define x norm as "".[ x ]"
{}^N" end define ]]"

\item "[[ tex show define x boolp as "".[ x ]"
\in \mathbf{B}" end define ]]"

\item "[[ tex show define x truep as "".[ x ]"
\in \mathbf{T}" end define ]]"

\item "[[ tex show define x falsep as "".[ x ]"
\in \mathbf{F}" end define ]]"

\item "[[ tex show define x intp as "".[ x ]"
\in \mathbf{Z}" end define ]]"

\item "[[ tex show define x pairp as "".[ x ]"
\in \mathbf{P}" end define ]]"

\item "[[ tex show define x atom as "".[ x ]"
\in \mathbf{A}" end define ]]"

\item "[[ tex show define x mapp as "".[ x ]"
\in \mathbf{M}" end define ]]"

\item "[[ tex show define x objectp as "".[ x ]"
\in \mathbf{O}" end define ]]"

\item "[[ tex show define x zeroth as "".[ x ]"
{}^0" end define ]]"

\item "[[ tex show define x first as "".[ x ]"
{}^1" end define ]]"

\item "[[ tex show define x second as "".[ x ]"
{}^2" end define ]]"

\item "[[ tex show define x third as "".[ x ]"
{}^3" end define ]]"

\item "[[ tex show define x fourth as "".[ x ]"
{}^4" end define ]]"

\item "[[ tex show define x fifth as "".[ x ]"
{}^5" end define ]]"

\item "[[ tex show define x sixth as "".[ x ]"
{}^6" end define ]]"

\item "[[ tex show define x seventh as "".[ x ]"
{}^7" end define ]]"

\item "[[ tex show define x eighth as "".[ x ]"
{}^8" end define ]]"

\item "[[ tex show define x ninth as "".[ x ]"
{}^9" end define ]]"

\item "[[ tex show define x ref as "".[ x ]"
{}^r" end define ]]"

\item "[[ tex show define x idx as "".[ x ]"
{}^i" end define ]]"

\item "[[ tex show define x debug as "".[ x ]"
{}^d" end define ]]"

\item "[[ tex show define a [[ i ]] as "".[ a ]"
\linebreak[0][ "[ i ]"
]" end define ]]"

\item "[[ tex show define a [[ i -> v ]] as "".[ a ]"
\linebreak[0][ "[ i ]"
{\rightarrow} "[ v ]"
]" end define ]]"

\item "[[ tex show define a [[ i => v ]] as "".[ a ]"
\linebreak[0][ "[ i ]"
{\Rightarrow} "[ v ]"
]" end define ]]"

\item "[[ tex use define x tight endline as "".[ x ]"
\newline " end define ]]"

\item "[[ tex use define x unquote as "
\underline{ "[ x ]"
} " end define ]]"



\item "[[ tex use define newline x as "
\newline "[ x ]"". end define ]]"



\item "[[ tex show define x ' y as "".[ x ]"
\mathbin {\mbox {'}}"[ y ]"". end define ]]"

\item "[[ tex show define x apply y as "".[ x ]"
\mathbin {\mbox {''}}"[ y ]"". end define ]]"

\item "[[ tex show define texshow x end texshow as "
\underline{ "[ x ]"
}" end define ]]"



\item "[[ tex show define - x as "
{-} "[ x ]"". end define ]]"

\item "[[ tex show define + x as "
{+} "[ x ]"". end define ]]"



\item "[[ tex show define x * y as "".[ x ]"
\cdot "[ y ]"". end define ]]"



\item "[[ tex show define x + y as "".[ x ]"
+ "[ y ]"". end define ]]"

\item "[[ tex show define x - y as "".[ x ]"
- "[ y ]"". end define ]]"





\item "[[ tex show define x :: y as "".[ x ]"
\mathop{:\,:} "[ y ]"". end define ]]"



\item "[[ tex show define x ,, y as "".[ x ]"
, "[ y ]"". end define ]]"



\item "[[ tex show define x = y as "".[ x ]"
= "[ y ]"". end define ]]"

\item "[[ tex show define x != y as "".[ x ]"
\neq "[ y ]"". end define ]]"

\item "[[ tex show define x < y as "".[ x ]"
< "[ y ]"". end define ]]"

\item "[[ tex show define x > y as "".[ x ]"
> "[ y ]"". end define ]]"

\item "[[ tex show define x <= y as "".[ x ]"
\le "[ y ]"". end define ]]"

\item "[[ tex show define x >= y as "".[ x ]"
\ge "[ y ]"". end define ]]"

\item "[[ tex show define x r= y as "".[ x ]"
\stackrel{r}{=} "[ y ]"". end define ]]"

\item "[[ tex show define x t= y as "".[ x ]"
\stackrel{t}{=} "[ y ]"". end define ]]"

\item "[[ tex show define x t=* y as "".[ x ]"
\stackrel{t^*}{=} "[ y ]"". end define ]]"



\item "[[ tex show define .not. x as "
{\bf not} \ \linebreak [0]"[ x ]"". end define ]]"



\item "[[ tex show define x .and. y as "".[ x ]"
\ {\bf and} \ \linebreak [0]"[ y ]"". end define ]]"

\item "[[ tex show define x .prog1. y as "".[ x ]"
\ {\bf prog1} \ \linebreak [0]"[ y ]"". end define ]]"

\item "[[ tex show define x &c y as "".[ x ]"
\wedge_c "[ y ]"". end define ]]"



\item "[[ tex show define x .or. y as "".[ x ]"
\ {\bf or} \ \linebreak [0]"[ y ]"". end define ]]"



\item "[[ tex show define x is val : y as "".[ x ]"
{\in} \mathbf{V} \colon "[ y ]"". end define ]]"

\item "[[ tex show define x is bool : y as "".[ x ]"
{\in} \mathbf{B} \colon "[ y ]"". end define ]]"

\item "[[ tex show define x is int : y as "".[ x ]"
{\in} \mathbf{Z} \colon "[ y ]"". end define ]]"

\item "[[ tex show define x is pair : y as "".[ x ]"
{\in} \mathbf{P} \colon "[ y ]"". end define ]]"

\item "[[ tex show define x is map : y as "".[ x ]"
{\in} \mathbf{M} \colon "[ y ]"". end define ]]"

\item "[[ tex show define x is object : y as "".[ x ]"
{\in} \mathbf{O} \colon "[ y ]"". end define ]]"



\item "[[ tex show define x Select y else z end select as
"".[ x ]"
\left\langle\protect \begin {array}{l}"[ y ]"
\\"[ z ]"
\protect \end {array}\right." end define ]]"

\item "[[ tex show define x IN y as "".[ x ]"
\ \mathbf{in}\ \linebreak [0] "[ y ]"". end define ]]"



\item "[[ tex show define \ x . y as "
\lambda "[ x ]"
."[ y ]"". end define ]]"

\item "[[ tex show define If x then y else z as "
{\bf If} \ \linebreak [0]"[ x ]"
\ {\bf then} \ \linebreak [0]"[ y ]"
\ {\bf else} \ \linebreak [0]"[ z ]"". end define ]]"

\item "[[ tex show define if x then y else z as "
{\bf if} \ \linebreak [0]"[ x ]"
\ {\bf then} \ \linebreak [0]"[ y ]"
\ {\bf else} \ \linebreak [0]"[ z ]"". end define ]]"

\item "[[ tex show define LET x BE y as "
{\bf let} \ \linebreak [0]"[ x ]"
\ {\bf be} \ \linebreak [0]"[ y ]"". end define ]]"

\item "[[ tex show define let x := y in z as "
{\bf let} \ \linebreak [0]"[ x ]"
\mathrel{\ddot{=}} "[ y ]"
\ {\bf in} \ \linebreak [0]"[ z ]"". end define ]]"

\item "[[ tex show define let x = y in z as "
{\bf let} \ \linebreak [0]"[ x ]"
= "[ y ]"
\ {\bf in} \ \linebreak [0]"[ z ]"". end define ]]"

\item "[[ tex show define ttst x end test as "
[ "[ x ]"
]^{\cdot}" end define ]]"

\item "[[ tex show define ftst x end test as "
[ "[ x ]"
]^{-}" end define ]]"

\item "[[ tex show define etst x ; y end test as "
[ "[ x ]"
= "[ y ]"
]^{=}" end define ]]"

\item "[[ tex show define x reduce to y as "".[ x ]"
\stackrel {+}{\rightarrow }"[ y ]"". end define ]]"

\item "[[ tex show define x == y as "".[ x ]"
\equiv "[ y ]"". end define ]]"



\item "[[ tex use define x lgcthen y as x,"
\newline ",y end define ]]"

\item "[[ tex use define x,y as "".[ x ]"".[ y ]"". end define ]]"

\item "[[ tex use define x[ y ]z as "".[ x ]"".[ y ]"".[ z ]"". end define ]]"

\item "[[ tex use define x[[ y ]]z as "".[ x ]"$"[ y ]"$"[ z ]"". end define ]]"

\item "[[ tex show define x[[ y ]]z as "".[ x ]"
{\$}"[ y ]"
{\$}"[ z ]"". end define ]]"

\item "[[ tex use define x[[[ y ]]]z as "".[ x ]"\["[ y ]"\]"[ z ]"". end define ]]"

\item "[[ tex show define x[[[ y ]]]z as "".[ x ]"
{\backslash[}"[ y ]"
{\backslash]}"[ z ]"". end define ]]"



\item "[[ tex use define x endline as "".[ x ]"
\newline " end define ]]"



\item "[[ tex use define x linebreak y as "".[ x ]"
\linebreak[4] "[ y ]"". end define ]]"



\item "[[ tex use define x & y as "".[ x ]"
& "[ y ]"". end define ]]"



\item "[[ tex use define x \\ y as "".[ x ]"
\\{}"[ y ]"". end define ]]"

\end{statements}



\section{Name definitions}

"[[ protect ""N end protect ]]"



\section{Charge definitions}

"[[ protect ""C end protect ]]"



\end{document}
" end text ,,



latex ( "chores" ) ,,
latex ( "chores" ) ,,
dvipdfm ( "chores" )