752 Up 753
754 755756 757 Contents: 758 Main text 759 Chores 760
761 762 Klaus Grue 763 764 " end text ,, 765 766 767 768 text "page.bib" : ""-""; 769 770 @article {berline97, 771 author = {C. Berline and K. Grue}, 772 title = {A $\kappa$-denotational semantics for {M}ap {T}heory 773 in {ZFC+SI}}, 774 journal = TCS, 775 year = {1997}, 776 volume = {179}, 777 number = {1--2}, 778 pages = {137--202}, 779 month = {jun}} 780 781 @inproceedings{Logiweb, 782 author = {K. Grue}, 783 title = {Logiweb}, 784 editor = {Fairouz Kamareddine}, 785 booktitle = {Mathematical Knowledge Management Symposium 2003}, 786 publisher = {Elsevier}, 787 series = {Electronic Notes in Theoretical Computer Science}, 788 volume = {93}, 789 year = {2004}, 790 pages = {70--101}} 791 792 @techreport{chores, 793 author = {K. Grue}, 794 year = {2006}, 795 title = {A Logiweb base page - chores}, 796 institution={Logiweb}, 797 note = {\href {\lgwBlockRelay \lgwBlockThis 798 /page/appendix.pdf}{\lgwBreakRelay \lgwBreakThis /page/appendix.pdf}}} 799 800 " end text ,, 801 802 803 804 text "page.tex" : ""-""; 805 \documentclass[fleqn]{article} 806 807 % Include definitions generated by the Logiweb compiler 808 \input{lgwinclude} 809 810 % Make latexsym characters available 811 \usepackage{latexsym} 812 813 % Ensure reasonable rendering of strings 814 \everymath{\rm} 815 \everydisplay{\rm} 816 817 % Enable generation of an index 818 \usepackage{makeidx} 819 \makeindex 820 \newcommand{\intro}[1]{\emph{#1}} 821 \newcommand{\indexintro}[1]{\index{#1}\intro{#1}} 822 823 % Enable generation of a bibliography 824 \bibliographystyle{plain} 825 826 % Enable hyperlinks 827 \usepackage[dvipdfm=true]{hyperref} 828 \hypersetup{pdfpagemode=UseNone} 829 \hypersetup{pdfstartpage=1} 830 \hypersetup{pdfstartview=FitBH} 831 % (x,y)=(120,80) lower left, (x,y)=(490,730) upper right 832 \hypersetup{pdfpagescrop={120 80 490 730}} 833 \hypersetup{pdftitle=A Logiweb base page} 834 \hypersetup{colorlinks=true} 835 836 % Construct for listing statements with associated explanations 837 \newenvironment{statements}{\begin{list}{}{ 838 \setlength{\leftmargin}{5em} 839 \setlength{\itemindent}{-5em}}}{\end{list}} 840 841 \begin{document} 842 \title{A Logiweb base page} 843 \author{Klaus Grue} 844 \maketitle 845 \tableofcontents 846 847 "[ make macro expanded version ragged right ]" 848 849 850 851 \section{Introduction}"[ " 852 853 \indexintro{Logiweb} \cite{Logiweb} is an open source system available under GNU GPL for distribution of mathematical definitions, lemmas, and proofs. 854 855 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. 856 857 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. 858 859 860 861 \subsection{Electronic appendices} 862 863 The present Logiweb page comprises one html and two PDF files, located the following places: 864 865 \begin{itemize} 866 \item \href {\lgwBlockRelay \lgwBlockThis /page/page.pdf}{% 867 \lgwBreakRelay \lgwBreakThis /page/page.pdf} 868 \item \href {\lgwBlockRelay \lgwBlockThis /page/appendix.pdf}{% 869 \lgwBreakRelay \lgwBreakThis /page/appendix.pdf} 870 \item \href {\lgwBlockRelay \lgwBlockThis /page/page.pdf}{% 871 \lgwBreakRelay \lgwBreakThis /page/page.pdf} \cite{chores} 872 \item \href {\lgwBlockRelay \lgwBlockThis /page/page.html}{% 873 \lgwBreakRelay \lgwBreakThis /page/page.html} 874 \end{itemize} 875 876 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. 877 878 879 880 \subsection{Proclamations}\label{sec:Proclamations} 881 882 Logiweb has a number of predefined semantic concepts. Each predefined concept has a name where a name is a string of characters. 883 884 Furthermore, Logiweb has a \indexintro{proclamation} mechanism which allows to connect syntactic constructs with semantic concepts. Some proclamations are given in the following. 885 886 \begin{statements} 887 888 \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. 889 890 \item "[[ proclaim x ' y as "apply" end proclaim ]]"\index{apply} proclaims "[[ x ' y ]]" to denote \index{application, functional}\indexintro{functional application}. 891 892 \item "[[ proclaim true as "true" end proclaim ]]"\index{true} proclaims "[[ true ]]" to denote \indexintro{truth}. 893 894 \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}. 895 896 \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}. 897 898 \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. 899 900 \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 ]]". 901 902 \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}. 903 904 \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. 905 906 \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}. 907 908 \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}. 909 910 \end{statements} 911 912 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. 913 914 915 916 \subsection{Aspect declarations}\label{sec:AspectDeclarations} 917 918 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}. 919 920 \begin{statements} 921 922 \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. 923 924 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. 925 926 \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 ]]". 927 928 \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}. 929 930 \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. 931 932 \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 ) ]]". 933 934 \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}. 935 936 \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}. 937 938 \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. 939 940 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. 941 942 \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}. 943 944 \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. 945 946 \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}. 947 948 \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. 949 950 \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. 951 952 \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. 953 954 \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. 955 956 \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. 957 958 \end{statements} 959 960 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. 961 962 963 964 \subsection{Definition of pre- and post-associativity} 965 966 \begin{statements} 967 968 \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}. 969 970 \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}. 971 972 \end{statements} 973 974 975 976 \subsection{The Logiweb system}\label{sec:TheLogiwebSystem} 977 978 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. 979 980 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. 981 982 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. 983 984 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: 985 986 \begin{enumerate} 987 988 \item\label{enum:author} when authoring and submitting new Logiweb pages. 989 990 \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. 991 992 \item\label{enum:execute} when executing computable functions on Logiweb pages (c.f.\ the ``execute'' aspect in Section \ref{sec:AspectDeclarations}). 993 994 \end{enumerate} 995 996 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. 997 998 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. 999 1000 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. 1001 1002 1003 1004 " ]"\section{Computation}\label{sec:Computation}"[ " 1005 1006 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}. 1007 1008 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. 1009 1010 1011 1012 \subsection{Reduction system}\label{sec:ReductionSystem} 1013 1014 The engine reduces terms according to the following reduction system: 1015 1016 "[[[ array ( left,left,left ) 1017 1018 ( \ x . y ) ' z & %% reduce to %% & < y | x := z > \\ 1019 1020 true ' z & %% reduce to %% & true \\ 1021 1022 If true then u else v & %% reduce to %% & u \\ 1023 1024 If \ x . y then u else v & %% reduce to %% & v 1025 1026 end array ]]]" 1027 1028 \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. 1029 1030 1031 1032 \subsection{Normal forms}\label{sec:NormalForms} 1033 1034 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. 1035 1036 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. 1037 1038 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. 1039 1040 1041 1042 \subsection{Maps}\label{sec:Maps} 1043 1044 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. 1045 1046 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}. 1047 1048 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. 1049 1050 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. 1051 1052 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. 1053 1054 Anyone who can come up with a better name than "[[ x == y ]]" for true, identification disrespecting equality is welcome to contact the author. 1055 1056 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 ]]". 1057 1058 The reduction rules of Section \ref{sec:ReductionSystem} correspond to the following axioms of map theory: 1059 1060 "[[[ array ( left,left,left ) 1061 1062 ( \ x . y ) ' z & %% == %% & < y | x := z > \\ 1063 1064 true ' z & %% == %% & true \\ 1065 1066 If true then u else v & %% == %% & u \\ 1067 1068 If \ x . y then u else v & %% == %% & v 1069 1070 end array ]]]" 1071 1072 1073 1074 \subsection{Full reduction system}\label{sec:FullReductionSystem} 1075 1076 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: 1077 1078 \begin{itemize} 1079 1080 \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. 1081 1082 \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 ]]". 1083 1084 \item The engine reduces constructs that have a value definition according to that definition, c.f. Section \ref{sec:ElementaryDefinitions}. 1085 1086 \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. 1087 1088 \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. 1089 1090 \item The engine would be rediculously slow if it wasn't for the optimizations explained in Section \ref{sec:ElementaryDefinitions}. 1091 1092 \end{itemize} 1093 1094 1095 1096 \subsection{Elementary definitions}\label{sec:ElementaryDefinitions} 1097 1098 Consider the following definitions: 1099 1100 \begin{statements} 1101 1102 \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. 1103 1104 \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. 1105 1106 \item "[[ define value of x Head as x ' true end define ]]". We have "[[[ array ( left ) 1107 1108 ( u LazyPair v ) Head == %% \\ 1109 1110 ( \ x . If x then u else v ) Head == %% \\ 1111 1112 ( \ x . If x then u else v ) ' true == %% \\ 1113 1114 If true then u else v == %% \\ 1115 1116 u 1117 1118 end array ]]]" Hence, "[[ ( u LazyPair v ) Head == u ]]" whenever "[[ u ]]" and "[[ v ]]" differ from "[[ bottom ]]". 1119 1120 \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. 1121 1122 \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: 1123 1124 \begin{itemize} 1125 1126 \item "[[ true Guard y == y ]]" 1127 1128 \item "[[ \ u . v Guard y == y ]]" 1129 1130 \item "[[ bottom Guard y == bottom ]]". 1131 1132 \end{itemize} 1133 1134 "[[ 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}). 1135 1136 \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 1137 1138 \begin{itemize} 1139 1140 \item "[[ bottom Pair y == bottom ]]" 1141 1142 \item "[[ x Pair bottom == bottom ]]" 1143 1144 \end{itemize} 1145 1146 \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 ]]". 1147 1148 \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. 1149 1150 \end{statements} 1151 1152 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. 1153 1154 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. 1155 1156 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. 1157 1158 1159 1160 \subsection{Booleans} 1161 1162 \begin{statements} 1163 1164 \item "[[ proclaim x Select y else z end select as "if" end proclaim ]]" 1165 1166 \item "[[ define value of Not x as If x then false else true end define ]]" 1167 1168 \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 ]]" 1169 1170 \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 ]]" 1171 1172 \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 ]]" 1173 1174 \item "[[ define value of x TheBool as If x then true else false end define ]]" 1175 1176 \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 ]]" 1177 1178 \end{statements} 1179 1180 1181 1182 \subsection{Naturals}\label{sec:Naturals} 1183 1184 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 \[ 1185 \sum_{i=0}^{n} 2^i c_i 1186 \] 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. 1187 1188 \begin{statements} 1189 1190 \item "[[ define value of Zero as true end define ]]" 1191 1192 \item "[[ define value of x NatPair y as If x And y then Zero else x TheBool Pair y end define ]]" 1193 1194 \item "[[ define value of x TheNat as If x then Zero else x Head NatPair x Tail TheNat end define ]]" 1195 1196 \item "[[ define value of One as false Pair Zero end define ]]" 1197 1198 \item "[[ define value of Two as true Pair One end define ]]" 1199 1200 \item "[[ define value of Three as false Pair One end define ]]" 1201 1202 \item "[[ define value of Four as true Pair Two end define ]]" 1203 1204 \item "[[ define value of Five as false Pair Two end define ]]" 1205 1206 \item "[[ define value of Six as true Pair Three end define ]]" 1207 1208 \item "[[ define value of Seven as false Pair Three end define ]]" 1209 1210 \item "[[ define value of Eight as true Pair Four end define ]]" 1211 1212 \item "[[ define value of Nine as false Pair Four end define ]]" 1213 1214 \item "[[ define value of Ten as true Pair Five end define ]]" 1215 1216 \item "[[ define value of Xor ( x , y , c ) as x Head Iff y Head Iff c end define ]]" 1217 1218 \item "[[ define value of Carry ( x , y , c ) as If x Head then y Head Or c else y Head And c end define ]]" 1219 1220 \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 ]]" 1221 1222 \item "[[ define value of x Plus y as Plus ( x , y , true ) end define ]]" 1223 1224 \item "[[ define value of Borrow ( x , y , b ) as If x Head then y Head And b else y Head Or b end define ]]" 1225 1226 \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 ]]" 1227 1228 \item "[[ define value of x LT y as Compare ( y , x , false ) end define ]]" 1229 1230 \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 ]]" 1231 1232 \item "[[ define value of x Minus y as Minus ( x , y , true ) end define ]]" 1233 1234 \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 ]]" 1235 1236 \end{statements} 1237 1238 1239 1240 \subsection{Bottom}\label{sec:Bottom} 1241 1242 \begin{statements} 1243 1244 \item "[[ optimized define value of bottom as ( \ x . x ' x ) ' ( \ x . x ' x ) end define ]]" 1245 1246 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. 1247 1248 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}. 1249 1250 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. 1251 1252 \end{statements} 1253 1254 1255 1256 " ]"\section{Tagged values}\label{sec:TaggedValues}"[ " 1257 1258 \subsection{Tags}\label{sec:Tags} 1259 1260 \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. 1261 1262 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. 1263 1264 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. 1265 1266 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. 1267 1268 The tags of the predefined types are: 1269 1270 \begin{statements} 1271 1272 \item "[[ define value of BoolTag as Zero Pair Zero end define ]]" 1273 1274 \item "[[ define value of IntTag as Zero Pair One end define ]]" 1275 1276 \item "[[ define value of PairTag as Zero Pair Two end define ]]" 1277 1278 \item "[[ define value of ExTag as Zero Pair Three end define ]]" 1279 1280 \item "[[ define value of MapTag as Zero Pair Four end define ]]" 1281 1282 \end{statements} 1283 1284 1285 1286 \subsection{Tag querying}\label{sec:TagQuerying} 1287 1288 \begin{statements} 1289 1290 \item "[[ define value of x Tag as x Head Head TheNat Pair x Head Tail TheNat end define ]]" 1291 1292 \item "[[ define value of x BoolP as x Tag Equal BoolTag end define ]]" 1293 1294 \item "[[ define value of x IntP as x Tag Equal IntTag end define ]]" 1295 1296 \item "[[ define value of x PairP as x Tag Equal PairTag end define ]]" 1297 1298 \item "[[ define value of x ExP as x Tag Equal ExTag end define ]]" 1299 1300 \item "[[ define value of x MapP as x Tag Equal MapTag end define ]]" 1301 1302 \item "[[ define value of x ObjectP as Not ( x BoolP Or x IntP Or x PairP Or x ExP Or x MapP ) end define ]]" 1303 1304 \end{statements} 1305 1306 1307 1308 \subsection{Guards} 1309 1310 \begin{statements} 1311 1312 \item "[[ optimized define value of x is val : y as If x norm ExP then x else y end define ]]" 1313 1314 \item "[[ optimized define value of x .then. y as If x norm ExP then x else y end define ]]" 1315 1316 \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 ]]" 1317 1318 \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 ]]" 1319 1320 \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 ]]" 1321 1322 \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 ]]" 1323 1324 \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 ]]" 1325 1326 \end{statements} 1327 1328 1329 1330 \subsection{Normalization}\label{sec:Normalization} 1331 1332 \begin{statements} 1333 1334 \item "[[ optimized define value of x norm as newline 1335 1336 If x BoolP then x TheBool else newline 1337 1338 If x IntP then int ( x Tail ) else newline 1339 1340 If x PairP then x Tail Head :: x Tail Tail else newline 1341 1342 If x ExP then x Tail raise else newline 1343 1344 If x MapP then map ( x Tail ) else newline 1345 1346 x Tag Pair x Tail norm end define ]]" 1347 1348 \item "[[ optimized define value of norm x as x norm end define ]]" 1349 1350 \end{statements} 1351 1352 1353 1354 \subsection{Booleans}\label{sec:OperationsOnBooleans} 1355 1356 \begin{statements} 1357 1358 \item "[[ optimized define value of x boolp as x is val : x BoolP end define ]]" 1359 1360 \item "[[ optimized define value of if x then y else z as x is val : If norm x then y else z end define ]]" 1361 1362 \item "[[ optimized define value of .not. x as norm x is val : if x then false else true end define ]]" 1363 1364 \item "[[ optimized define value of notnot x as norm x is val : if x then true else false end define ]]" 1365 1366 \item "[[ optimized define value of x .and. y as If x norm then y norm else x norm end define ]]" 1367 1368 \item "[[ optimized define value of x .or. y as if x norm then true else y norm end define ]]" 1369 1370 \item "[[ optimized define value of x = y as norm x is val : y is val : equal1 ( x norm , y norm ) end define ]]" 1371 1372 \item "[[ define value of equal1 ( x , y ) as newline 1373 1374 if x boolp then x Equal y else newline 1375 1376 if x intp then x Equal y else newline 1377 1378 if x pairp then y pairp .and. x head = y head .and. x tail = y tail else newline 1379 1380 if x mapp then y mapp else newline 1381 1382 x Tag Equal y Tag .and. x Tail = y Tail end define ]]" 1383 1384 \item "[[ define value of x != y as norm x is val : y is val : .not. x = y end define ]]" 1385 1386 \item "[[ define value of x truep as x is val : x boolp .and. notnot x end define ]]" 1387 1388 \item "[[ define value of x falsep as x is val : x boolp .and. .not. x end define ]]" 1389 1390 \end{statements} 1391 1392 1393 1394 \subsection{Integers}\label{sec:Integers} 1395 1396 \begin{statements} 1397 1398 \item "[[ optimized define value of x intp as norm x is val : x IntP end define ]]" 1399 1400 \item "[[ define value of int ( x ) as TheInt ( x Head TheBool , x Tail TheNat ) end define ]]" 1401 1402 \item "[[ define value of PlusTag x as TheInt ( true , x ) end define ]]" 1403 1404 \item "[[ define value of MinusTag x as TheInt ( false , x ) end define ]]" 1405 1406 \item "[[ define value of x Sign as x Tail Head end define ]]" 1407 1408 \item "[[ define value of x Mag as x Tail Tail end define ]]" 1409 1410 \item "[[ optimized define value of + x as norm x is val : x is int : x end define ]]" 1411 1412 \item "[[ optimized define value of +x as + x end define ]]" 1413 1414 \end{statements} 1415 1416 1417 1418 \subsection{Integer addition}\label{sec:IntegerAddition} 1419 1420 \begin{statements} 1421 1422 \item "[[ define value of TheInt ( s , v ) as IntTag Pair ( s Or v ) Pair v end define ]]" 1423 1424 \item "[[ optimized define value of x + y as norm x is val : y is val : plus1 ( x norm , y norm ) end define ]]" 1425 1426 \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 ]]" 1427 1428 \item "[[ define value of plus2 ( s , t , x , y ) as 1429 1430 s Select ""; x>0 1431 1432 t Select ""; x>0, y>0 1433 1434 PlusTag x Plus y 1435 1436 else ""; x>0, y<0 1437 1438 x LT y Select ""; x>0, y<0, |x|<|y| 1439 1440 MinusTag y Minus x 1441 1442 else ""; x>0, y<0, |x|>|y| 1443 1444 PlusTag x Minus y end select end select 1445 1446 else ""; x<0 1447 1448 t Select ""; x<0, y>0 1449 1450 x LT y Select ""; x<0, y>0, |x|<|y| 1451 1452 PlusTag y Minus x 1453 1454 else ""; x<0, y>0, |x|>|y| 1455 1456 MinusTag x Minus y end select 1457 1458 else ""; x<0, y<0 1459 1460 MinusTag x Plus y end select end select end define ]]" 1461 1462 \end{statements} 1463 1464 1465 1466 \subsection{Integer subtraction}\label{sec:IntegerSubtraction} 1467 1468 \begin{statements} 1469 1470 \item "[[ optimized define value of - x as norm x is val : minus1 ( x norm ) end define ]]" 1471 1472 \item "[[ optimized define value of -x as - x end define ]]" 1473 1474 \item "[[ define value of minus1 ( x ) as x is int : minus2 ( x Sign , x Mag ) end define ]]" 1475 1476 \item "[[ define value of minus2 ( s , x ) as TheInt ( Not s , x ) end define ]]" 1477 1478 \item "[[ optimized define value of x - y as norm x is val : y is val : x + - y end define ]]" 1479 1480 \end{statements} 1481 1482 1483 1484 \subsection{Integer multiplication}\label{sec:IntegerMultiplication} 1485 1486 \begin{statements} 1487 1488 \item "[[ optimized define value of x * y as norm x is val : y is val : times1 ( x norm , y norm ) end define ]]" 1489 1490 \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 ]]" 1491 1492 \item "[[ define value of times2 ( s , t , x , y ) as TheInt ( s Iff t , x Times y ) end define ]]" 1493 1494 \end{statements} 1495 1496 1497 1498 \subsection{Integer comparison}\label{sec:IntegerComparison} 1499 1500 \begin{statements} 1501 1502 \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 ]]" 1503 1504 \item "[[ define value of lt1 ( x , y ) as lt2 ( x Sign , y Sign , x Mag , y Mag ) end define ]]" 1505 1506 \item "[[ define value of lt2 ( s , t , x , y ) as 1507 1508 s Select ""; x>0 1509 1510 t Select ""; x>0, y>0 1511 1512 x LT y 1513 1514 else ""; x>0, y<0 1515 1516 false end select 1517 1518 else ""; x<0 1519 1520 t Select ""; x<0, y>0 1521 1522 true 1523 1524 else ""; x<0, y<0 1525 1526 y LT x end select end select end define ]]" 1527 1528 \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 ]]" 1529 1530 \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 ]]" 1531 1532 \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 ]]" 1533 1534 \end{statements} 1535 1536 1537 1538 \subsection{Integer construction}\label{sec:IntegerConstruction} 1539 1540 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. 1541 1542 \begin{statements} 1543 1544 \item "[[ optimized define value of Base as norm PlusTag Ten end define ]]" 1545 1546 \item "[[ optimized define value of %% as norm PlusTag Zero end define ]]" 1547 1548 Invisible zero. 1549 1550 \item "[[ optimized define value of x %0 as norm x is val : x * Base end define ]]" 1551 1552 \item "[[ optimized define value of x %1 as norm x is val : x * Base + PlusTag One end define ]]" 1553 1554 \item "[[ optimized define value of x %2 as norm x is val : x * Base + PlusTag Two end define ]]" 1555 1556 \item "[[ optimized define value of x %3 as norm x is val : x * Base + PlusTag Three end define ]]" 1557 1558 \item "[[ optimized define value of x %4 as norm x is val : x * Base + PlusTag Four end define ]]" 1559 1560 \item "[[ optimized define value of x %5 as norm x is val : x * Base + PlusTag Five end define ]]" 1561 1562 \item "[[ optimized define value of x %6 as norm x is val : x * Base + PlusTag Six end define ]]" 1563 1564 \item "[[ optimized define value of x %7 as norm x is val : x * Base + PlusTag Seven end define ]]" 1565 1566 \item "[[ optimized define value of x %8 as norm x is val : x * Base + PlusTag Eight end define ]]" 1567 1568 \item "[[ optimized define value of x %9 as norm x is val : x * Base + PlusTag Nine end define ]]" 1569 1570 \item "[[ define value of 0 as norm %% %0 end define ]]" 1571 1572 \item "[[ define value of 1 as norm %% %1 end define ]]" 1573 1574 \item "[[ define value of 2 as norm %% %2 end define ]]" 1575 1576 \item "[[ define value of 3 as norm %% %3 end define ]]" 1577 1578 \item "[[ define value of 4 as norm %% %4 end define ]]" 1579 1580 \item "[[ define value of 5 as norm %% %5 end define ]]" 1581 1582 \item "[[ define value of 6 as norm %% %6 end define ]]" 1583 1584 \item "[[ define value of 7 as norm %% %7 end define ]]" 1585 1586 \item "[[ define value of 8 as norm %% %8 end define ]]" 1587 1588 \item "[[ define value of 9 as norm %% %9 end define ]]" 1589 1590 \end{statements} 1591 1592 1593 1594 \subsection{Logical operations on integers} 1595 1596 \begin{statements} 1597 1598 \item "[[ optimized define value of evenp ( x ) as norm x is val : x is int : x Mag Head TheBool end define ]]" 1599 1600 \item "[[ define value of oddp ( x ) as norm x is val : x is int : .not. evenp ( x ) end define ]]" 1601 1602 \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 ]]" 1603 1604 \item "[[ define value of small ( x ) as norm x is val : norm x is int : -1 <= x .and. x <= 0 end define ]]" 1605 1606 \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 ]]" 1607 1608 \item "[[ optimized define value of lognot ( x ) as norm x is val : x is int : -1 - x end define ]]" 1609 1610 \item "[[ optimized define value of logior ( x , y ) as norm x is val : y is val : x is int : y is int : newline 1611 1612 if x = -1 then -1 else if y = -1 then -1 else newline 1613 1614 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 ]]" 1615 1616 \item "[[ optimized define value of logxor ( x , y ) as norm x is val : y is val : x is int : y is int : newline 1617 1618 if x = -1 then lognot ( y ) else if y = -1 then lognot ( x ) else newline 1619 1620 if x = 0 then y else if y = 0 then x else double ( oddp ( x ) != oddp ( y ) , logxor ( half ( x ) , half ( y ) ) ) end define ]]" 1621 1622 \item "[[ optimized define value of logand ( x , y ) as norm x is val : y is val : x is int : y is int : newline 1623 1624 if x = -1 then y else if y = -1 then x else newline 1625 1626 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 ]]" 1627 1628 \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 ]]" 1629 1630 \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 ]]" 1631 1632 \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 ]]" 1633 1634 \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 ]]" 1635 1636 \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 ]]" 1637 1638 \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 ]]" 1639 1640 \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 ]]" 1641 1642 \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 ]]" 1643 1644 \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 ]]" 1645 1646 \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 ]]" 1647 1648 \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 ]]" 1649 1650 \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 ]]" 1651 1652 \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 ]]" 1653 1654 \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 ]]" 1655 1656 \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 ]]" 1657 1658 \end{statements} 1659 1660 1661 1662 \subsection{Vector operations} 1663 1664 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 ]]". 1665 1666 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. 1667 1668 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. 1669 1670 We define the following functions on vectors: 1671 1672 \begin{statements} 1673 1674 \item "[[ vector ( x ) ]]". Normalize the vector (change the stop byte to a one-byte). 1675 1676 \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" ]]". 1677 1678 \item "[[ vector-prefix ( x , e ) ]]". Return the subvector ending before byte number "[[ e ]]": "[[ vector-prefix ( !"ABCD" , 2 ) = !"AB" ]]". 1679 1680 \item "[[ vector-subseq ( x , b , e ) ]]". Return the subvector beginning at "[[ b ]]" and ending before "[[ e ]]": "[[ vector-subseq ( !"ABCD" , 1 , 3 ) = !"BC" ]]". 1681 1682 \item "[[ vector-length ( x ) ]]". Return the length of the vector: "[[ vector-length ( !"ABCD" ) = 4 ]]". 1683 1684 \item "[[ vector-index ( x , i ) ]]". Return the i'th byte: "[[ vector-index ( !"ABCD" , 1 ) = 66 ]]". 1685 1686 \item "[[ eager define vector-head ( x ) as vector-index ( x , 0 ) end define ]]". 1687 1688 \item "[[ eager define vector-tail ( x ) as vector-suffix ( x , 1 ) end define ]]". 1689 1690 \end{statements} 1691 1692 We shall represent byte sequences in four ways: 1693 1694 \begin{description} 1695 1696 \item[byte*] A list of bytes. 1697 1698 \item[vector] An integer which encodes the list little endian base 256 with a stop byte at the end. 1699 1700 \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. 1701 1702 \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. 1703 1704 \end{description} 1705 1706 \noindent The following functions convert between the representations. Examples: 1707 1708 \[\begin{array}{lll} 1709 1710 "[ vector2byte* ( !"ABC" ) ]" & = & "[ << 65 ,, 66 ,, 67 >> ]" \\ 1711 1712 "[ bt2byte* ( ( 65 :: 66 ) :: - 1 :: 256 :: true :: 67 :: false :: 68 ) ]" & = & "[ << 65 ,, 66 ,, 67 ,, 68 >> ]" \\ 1713 1714 "[ bt2vector ( ( 65 :: 66 ) :: - 1 :: 256 :: true :: 67 :: false :: 68 ) ]" & = & "[ !"ABCD" ]" \\ 1715 1716 "[ vt2byte* ( ( !"A" :: !"BC" ) :: - 1 :: !"". :: false :: !"D" ) ]" & = & "[ << 65 ,, 66 ,, 67 ,, 68 >> ]" \\ 1717 1718 "[ vt2vector ( ( !"A" :: !"BC" ) :: - 1 :: !"". :: false :: !"D" ) ]" & = & "[ !"ABCD" ]" \\ 1719 1720 \end{array}\] 1721 1722 \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. 1723 1724 \noindent The definitions read: 1725 1726 \begin{statements} 1727 1728 \item "[[ define value of vector-mask as norm %% %2 %5 %5 end define ]]" 1729 1730 \item "[[ define value of octet-base as norm %% %2 %5 %6 end define ]]" 1731 1732 \item "[[ optimized define value of vector-empty ( x ) as norm x is val : x <= vector-mask end define ]]" 1733 1734 \item "[[ define value of vector-head1 ( x ) as norm x is val : logand ( vector-mask , x ) end define ]]" 1735 1736 \item "[[ define value of vector-tail1 ( x ) as norm x is val : ash ( x , -8 ) end define ]]" 1737 1738 \item "[[ define value of vector-cons ( x , y ) as norm x is val : y is val : logior ( x , ash ( y , 8 ) ) end define ]]" 1739 1740 \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 ]]" 1741 1742 \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 ]]" 1743 1744 \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 ]]" 1745 1746 \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 ]]" 1747 1748 \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 ]]" 1749 1750 \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 ]]" 1751 1752 \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 ]]" 1753 1754 \item "[[ optimized define value of vector2byte* ( x ) as norm x is val : vector2byte*1 ( x , true ) end define ]]" 1755 1756 \item "[[ define value of vector2byte*1 ( x , r ) as norm x is val : r is val : newline 1757 1758 if vector-empty ( x ) then reverse ( r ) else newline 1759 1760 vector2byte*1 ( vector-tail1 ( x ) , vector-head1 ( x ) :: r ) end define ]]" 1761 1762 \item "[[ optimized define value of vector2vector* ( x ) as norm x is val : vector2vector*1 ( x , true ) end define ]]" 1763 1764 \item "[[ define value of vector2vector*1 ( x , r ) as norm x is val : r is val : newline 1765 1766 if vector-empty ( x ) then reverse ( r ) else newline 1767 1768 vector2vector*1 ( vector-tail1 ( x ) , vector-head1 ( x ) + octet-base :: r ) end define ]]" 1769 1770 \item "[[ optimized define value of bt2byte* ( x ) as norm x is val : reverse ( bt2byte*1 ( x , true ) ) end define ]]" 1771 1772 \item "[[ define value of bt2byte*1 ( x , r ) as norm x is val : r is val : newline 1773 1774 if x pairp then bt2byte*1 ( x tail , bt2byte*1 ( x head , r ) ) else newline 1775 1776 if x intp .and. 0 <= x .and. x <= vector-mask then x :: r else r end define ]]" 1777 1778 \item "[[ optimized define value of bt2vector* ( x ) as norm x is val : reverse ( bt2vector*1 ( x , true ) ) end define ]]" 1779 1780 \item "[[ define value of bt2vector*1 ( x , r ) as norm x is val : r is val : newline 1781 1782 if x pairp then bt2vector*1 ( x tail , bt2vector*1 ( x head , r ) ) else newline 1783 1784 if x intp .and. 0 <= x .and. x <= vector-mask then x + octet-base :: r else r end define ]]" 1785 1786 \item "[[ optimized define value of bt2vector ( x ) as norm x is val : revbyte*2vector ( bt2byte*1 ( x , true ) , !"". ) end define ]]" 1787 1788 \item "[[ define value of revbyte*2vector ( x , r ) as norm x is val : r is val : newline 1789 1790 if x atom then r else newline 1791 1792 revbyte*2vector ( x tail , vector-cons ( x head , r ) ) end define ]]" 1793 1794 Reverse the list "[[ x ]]" of bytes, revappend them to the vector "[[ r ]]", and return them as a vector. 1795 1796 \item "[[ define value of vector-revappend ( x , y ) as norm x is val : y is val : newline 1797 1798 if vector-empty ( x ) then y else newline 1799 1800 vector-revappend ( vector-tail1 ( x ) , vector-head1 ( x ) :: y ) end define ]]" 1801 1802 Convert the vector "[[ x ]]" to a sequence of bytes and revappend it to the sequence "[[ y ]]" of bytes. 1803 1804 \item "[[ optimized define value of vt2byte* ( x ) as norm x is val : reverse ( vt2byte*1 ( x , true ) ) end define ]]" 1805 1806 \item "[[ define value of vt2byte*1 ( x , r ) as norm x is val : r is val : newline 1807 1808 if x pairp then vt2byte*1 ( x tail , vt2byte*1 ( x head , r ) ) else newline 1809 1810 if x intp then vector-revappend ( x , r ) else r end define ]]" 1811 1812 \item "[[ define value of vector-revappend1 ( x , y ) as norm x is val : y is val : newline 1813 1814 if vector-empty ( x ) then y else newline 1815 1816 vector-revappend1 ( vector-tail1 ( x ) , vector-head1 ( x ) + octet-base :: y ) end define ]]" 1817 1818 Convert the vector "[[ x ]]" to a sequence of bytes and revappend it to the sequence "[[ y ]]" of bytes. 1819 1820 \item "[[ optimized define value of vt2vector* ( x ) as norm x is val : reverse ( vt2vector*1 ( x , true ) ) end define ]]" 1821 1822 \item "[[ define value of vt2vector*1 ( x , r ) as norm x is val : r is val : newline 1823 1824 if x pairp then vt2vector*1 ( x tail , vt2vector*1 ( x head , r ) ) else newline 1825 1826 if x intp then vector-revappend1 ( x , r ) else r end define ]]" 1827 1828 \item "[[ optimized define value of vt2vector ( x ) as norm x is val : revbyte*2vector ( vt2byte*1 ( x , true ) , !"". ) end define ]]" 1829 1830 \end{statements} 1831 1832 1833 1834 \subsection{Division} 1835 1836 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. 1837 1838 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. 1839 1840 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. 1841 1842 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 ) ]]". 1843 1844 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. 1845 1846 \begin{statements} 1847 1848 \item "[[ define value of floor1 ( x , y ) as newline 1849 1850 if x < y then 0 :: x else newline 1851 1852 LET floor1 ( x , 2 * y ) BE z IN newline 1853 1854 if z tail < y then 2 * z head :: z tail else 2 * z head + 1 :: z tail - y end define ]]" 1855 1856 Divide the natural "[[ x ]]" by the positive integer "[[ y ]]" with rounding towards minus infinity. 1857 1858 \item "[[ define value of ceiling1 ( x , y ) as newline 1859 1860 LET floor1 ( x , y ) BE z IN newline 1861 1862 if z tail = 0 then z else z head + 1 :: z tail - y end define ]]" 1863 1864 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 ]]". 1865 1866 \item "[[ define value of round1 ( x , y ) as newline 1867 1868 LET floor1 ( x , y ) BE z IN newline 1869 1870 if z tail * 2 < y then z else newline 1871 1872 if z tail * 2 > y then z head + 1 :: z tail - y else newline 1873 1874 if evenp ( z head ) then z else newline z head + 1 :: z tail - y end define ]]" 1875 1876 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. 1877 1878 \item "[[ define value of reverse quotient ( p ) as - p head :: - p tail end define ]]" 1879 1880 Negate both quotient and remainder of a quotient/remainder pair. 1881 1882 \item "[[ optimized define value of truncate ( x , y ) as newline 1883 1884 if y <= 0 then exception else newline 1885 1886 if 0 <= x then floor1 ( x , y ) else newline 1887 1888 reverse quotient ( floor1 ( - x , y ) ) end define ]]" 1889 1890 Divide the integer "[[ x ]]" by the positive integer "[[ y ]]" with rouding towards zero. 1891 1892 \item "[[ optimized define value of floor ( x , y ) as newline 1893 1894 if y <= 0 then exception else newline 1895 1896 if 0 <= x then floor1 ( x , y ) else newline 1897 1898 reverse quotient ( ceiling1 ( - x , y ) ) end define ]]" 1899 1900 Divide the integer "[[ x ]]" by the positive integer "[[ y ]]" with rouding towards minus infinity. 1901 1902 \item "[[ optimized define value of ceiling ( x , y ) as newline 1903 1904 if y <= 0 then exception else newline 1905 1906 if 0 < x then ceiling1 ( x , y ) else newline 1907 1908 reverse quotient ( floor1 ( - x , y ) ) end define ]]" 1909 1910 Divide the integer "[[ x ]]" by the positive integer "[[ y ]]" with rouding towards plus infinity. 1911 1912 \item "[[ optimized define value of round ( x , y ) as newline 1913 1914 if y <= 0 then exception else newline 1915 1916 if 0 < x then round1 ( x , y ) else newline 1917 1918 reverse quotient ( round1 ( - x , y ) ) end define ]]" 1919 1920 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. 1921 1922 \item "[[ optimized define value of x div y as floor ( x , y ) head end define ]]" 1923 1924 \item "[[ optimized define value of x mod y as floor ( x , y ) tail end define ]]" 1925 1926 \end{statements} 1927 1928 1929 1930 \subsection{Pairs}\label{sec:Pairs} 1931 1932 \begin{statements} 1933 1934 \item "[[ optimized define value of x pairp as norm x is val : x PairP end define ]]" 1935 1936 \item "[[ define value of a atom as norm a is val : norm a is val : .not. a pairp end define ]]" 1937 1938 \item "[[ optimized define value of x :: y as x is val : y is val : PairTag Pair x norm Pair y norm end define ]]" 1939 1940 \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 ]]" 1941 1942 \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 ]]" 1943 1944 \item "[[ define value of append ( x , y ) as norm x is val : y is val : newline 1945 1946 if x atom then y else x head :: append ( x tail , y ) end define ]]" 1947 1948 \item "[[ define value of reverse ( x ) as norm x is val : revappend ( x , true ) end define ]]" 1949 1950 \item "[[ define value of revappend ( x , y ) as norm x is val : y is val : newline 1951 1952 if x atom then y else revappend ( x tail , x head :: y ) end define ]]" 1953 1954 \item "[[ define value of nth ( n , x ) as norm n is val : x is val : newline 1955 1956 if n <= 0 then x head else nth ( n - 1 , x tail ) 1957 1958 end define ]]" 1959 1960 \item "[[ eager define length ( x ) as length1 ( x , 0 ) end define ]]". 1961 1962 Compute length of list. 1963 1964 \item "[[ eager define length1 ( x , r ) as if x atom then r else length1 ( x tail , r + 1 ) end define ]]". 1965 1966 Compute the sum of the integer "[[ r ]]" and the length of the list "[[ x ]]". 1967 1968 \item "[[ eager define list-prefix ( l , n ) as newline 1969 1970 if n = 0 .or. l atom then true else l head :: list-prefix ( l tail , n - 1 ) end define ]]" 1971 1972 Return the first "[[ n ]]" elements of the list "[[ l ]]". 1973 1974 \item "[[ eager define list-suffix ( l , n ) as newline 1975 1976 if n = 0 then l else list-suffix ( l tail , n - 1 ) end define ]]" 1977 1978 Remove the first "[[ n ]]" elements from the list "[[ l ]]". 1979 1980 \end{statements} 1981 1982 1983 1984 \subsection{Exceptions}\label{sec:Exceptions} 1985 1986 \begin{statements} 1987 1988 \item "[[ optimized define value of x raise as x is val : ExTag Pair x norm end define ]]" 1989 1990 \item "[[ optimized define value of exception as norm true raise end define ]]" 1991 1992 \item "[[ optimized define value of catch ( x ) as Catch ( x norm ) end define ]]" 1993 1994 \item "[[ optimized define value of x catch as Catch ( x norm ) end define ]]" 1995 1996 \item "[[ define value of Catch ( x ) as If x ExP then true :: x Tail else false :: x end define ]]" 1997 1998 \end{statements} 1999 2000 2001 2002 \subsection{Maps}\label{sec:TaggedMaps} 2003 2004 \begin{statements} 2005 2006 \item "[[ optimized define value of x mapp as norm x is val : x MapP end define ]]" 2007 2008 \item "[[ optimized define value of map ( x ) as MapTag LazyPair x end define ]]" 2009 2010 \item "[[ optimized define value of x catching maptag as map ( x norm ) end define ]]" 2011 2012 \item "[[ optimized define value of x maptag as norm x is val : x catching maptag end define ]]" 2013 2014 \item "[[ optimized define value of x untag as norm x is val : x is map : x Tail norm end define ]]" 2015 2016 \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 ]]" 2017 2018 \item "[[ optimized define value of x root as norm x is val : x is map : x Tail TheBool end define ]]" 2019 2020 \end{statements} 2021 2022 2023 2024 \subsection{Objects}\label{sec:Objects} 2025 2026 \begin{statements} 2027 2028 \item "[[ optimized define value of x objectp as norm x is val : x ObjectP end define ]]" 2029 2030 \item "[[ optimized define value of object ( x ) as norm x is val : Object ( x head head , x head tail , x tail ) end define ]]" 2031 2032 \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 ]]" 2033 2034 \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 ]]" 2035 2036 \end{statements} 2037 2038 2039 2040 " ]"\section{Evaluation}"[ " 2041 2042 \subsection{Let construct} 2043 2044 "[[ optimized define value of LET x BE y as x is val : y ' x end define ]]" 2045 2046 "[[ proclaim x IN y as "lambda" end proclaim ]]" 2047 2048 2049 2050 \subsection{Simple accessors} 2051 2052 \begin{statements} 2053 2054 \item "[[ define value of x zeroth as norm x is val : x head end define ]]" 2055 2056 \item "[[ define value of x first as norm x is val : x tail zeroth end define ]]" 2057 2058 \item "[[ define value of x second as norm x is val : x tail first end define ]]" 2059 2060 \item "[[ define value of x third as norm x is val : x tail second end define ]]" 2061 2062 \item "[[ define value of x fourth as norm x is val : x tail third end define ]]" 2063 2064 \item "[[ define value of x fifth as norm x is val : x tail fourth end define ]]" 2065 2066 \item "[[ define value of x sixth as norm x is val : x tail fifth end define ]]" 2067 2068 \item "[[ define value of x seventh as norm x is val : x tail sixth end define ]]" 2069 2070 \item "[[ define value of x eighth as norm x is val : x tail seventh end define ]]" 2071 2072 \item "[[ define value of x ninth as norm x is val : x tail eighth end define ]]" 2073 2074 \end{statements} 2075 2076 2077 2078 \subsection{Representation of terms}\label{sec:RepresentationOfTerms} 2079 2080 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. 2081 2082 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. 2083 2084 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}. 2085 2086 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. 2087 2088 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. 2089 2090 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. 2091 2092 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. 2093 2094 The following constructs allows to access the reference, index, and debugging information of a term "[[ x ]]" 2095 2096 \begin{statements} 2097 2098 \item "[[ define value of x ref as norm x is val : x head head end define ]]" 2099 2100 \item "[[ define value of x idx as norm x is val : x head tail head end define ]]" 2101 2102 \item "[[ define value of x debug as norm x is val : x head tail tail end define ]]" 2103 2104 \end{statements} 2105 2106 2107 2108 \subsection{Tree equality} 2109 2110 \begin{statements} 2111 2112 \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. 2113 2114 \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. 2115 2116 \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. 2117 2118 \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. 2119 2120 \item "[[ define value of zip ( x , y ) as norm x is val : y is val : newline 2121 2122 if x atom .or. y atom then true else newline 2123 2124 ( 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). 2125 2126 \end{statements} 2127 2128 2129 2130 \subsection{Arrays} 2131 2132 \begin{statements} 2133 2134 \item "[[ define value of a [[ i ]] as norm a is val : i is val : i is int : array1 ( a , i , 0 ) end define ]]" 2135 2136 \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 2137 2138 if a atom then true else newline 2139 2140 if a head intp then if i = a head then a tail else true else newline 2141 2142 array1 ( if logbitp ( x , i ) then a tail else a head , i , x + 1 ) 2143 2144 end define ]]" 2145 2146 \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 ]]" 2147 2148 \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 2149 2150 if a atom then array3 ( i , v ) else newline 2151 2152 if a head intp then newline 2153 2154 if i = a head then newline 2155 2156 array3 ( i , v ) else newline 2157 2158 if v then a else newline 2159 2160 array5 ( a head , a tail , i , v , x ) else newline 2161 2162 if logbitp ( x , i ) then newline 2163 2164 array4 ( a head , array2 ( a tail , i , v , x + 1 ) ) else newline 2165 2166 array4 ( array2 ( a head , i , v , x + 1 ) , a tail ) 2167 2168 end define ]]" 2169 2170 \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 ]]" 2171 2172 \item "[[ define value of array4 ( a , b ) as norm a is val : b is val : newline 2173 2174 if a atom then newline 2175 2176 if b atom then true else if b head intp then b else a :: b else newline 2177 2178 if b atom .and. a head intp then a else a :: b end define ]]" 2179 2180 \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 2181 2182 if logbitp ( x , i ) then newline 2183 2184 if logbitp ( x , j ) then newline 2185 2186 true :: array5 ( i , v , j , w , x + 1 ) else newline 2187 2188 ( j :: w ) :: ( i :: v ) else newline 2189 2190 if logbitp ( x , j ) then newline 2191 2192 ( i :: v ) :: ( j :: w ) else newline 2193 2194 array5 ( i , v , j , w , x + 1 ) :: true end define ]]" 2195 2196 \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 ]]" 2197 2198 \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 ]]" 2199 2200 \item "[[ define value of pop ( a , i ) as norm a is val : i is val : a [[ i -> a [[ i ]] tail ]] end define ]]" 2201 2202 \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 ]]" 2203 2204 \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 ]]" 2205 2206 \item "[[ define value of pop* ( a , i ) as norm a is val : i is val : a [[ i => get* ( a , i ) tail ]] end define ]]" 2207 2208 \item "[[ late eager define array-domain ( x ) as newline 2209 2210 if x atom then true else newline 2211 2212 if x head intp then << x head >> else newline 2213 2214 sort-merge ( array-domain ( x head ) , array-domain ( x tail ) ) end define ]]" 2215 2216 Return the domain of the array "[[ x ]]" sorted in ascending order. 2217 2218 \item "[[ late eager define sort-merge ( x , y ) as newline 2219 2220 if x atom then y else sort-merge1 ( y , x ) end define ]]" 2221 2222 Merge the ascending lists "[[ x ]]" and "[[ y ]]" into a new, ascending list. 2223 2224 \item "[[ late eager define sort-merge1 ( x , y ) as newline 2225 2226 if x atom then y else newline 2227 2228 if x head < y head then newline 2229 2230 x head :: sort-merge1 ( x tail , y ) else newline 2231 2232 y head :: sort-merge1 ( y tail , x ) end define ]]" 2233 2234 Same as "[[ sort-merge ( x , y ) ]]" but assumes "[[ y ]]" to be a pair. 2235 2236 \end{statements} 2237 2238 2239 2240 \subsection{Evaluator} 2241 2242 \begin{statements} 2243 2244 \item "[[ define value of eval ( t , s , c ) as norm t is val : s is val : c is val : newline 2245 2246 LET t ref BE r IN newline 2247 2248 LET t idx BE i IN newline 2249 2250 if r = 0 then i maptag else newline 2251 2252 if i = 0 then if r = c [[ 0 ]] then c maptag else c [[ c [[ 0 ]] ]] [[ "cluster" ]] [[ r ]] maptag else newline 2253 2254 LET c [[ r ]] [[ "code" ]] [[ i ]] BE f IN newline 2255 2256 if f mapp then eval1 ( f , t tail , s , c ) else newline 2257 2258 if f = true then lookup ( t , s , map ( true ) ) else newline 2259 2260 if f = 1 then t first maptag else newline 2261 2262 map ( \ t . \ s . \ c . \ x . eval ( t second , ( t first :: map ( x ) ) :: s , c ) Tail ) apply t maptag apply s maptag apply c maptag 2263 2264 end define ]]" 2265 2266 \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 2267 2268 if t atom then f else newline 2269 2270 eval1 ( f apply eval ( t head , s , c ) , t tail , s , c ) end define ]]" 2271 2272 \end{statements} 2273 2274 2275 2276 \subsection{Debugging aids} 2277 2278 \begin{statements} 2279 2280 \item "[[ optimized define value of spy ( x ) as norm x is val : "spy" end define ]]" 2281 2282 \item "[[ optimized define value of trace ( x ) as norm x is val : "trace" end define ]]" 2283 2284 \item "[[ optimized define value of print ( x ) as norm x is val : "print" end define ]]" 2285 2286 \item "[[ optimized define value of timer ( x ) as norm x is val : "timer" end define ]]" 2287 2288 \end{statements} 2289 2290 "[[ 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. 2291 2292 "[[ 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. 2293 2294 "[[ 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. 2295 2296 "[[ 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. 2297 2298 \begin{statements} 2299 2300 \item "[[ late eager define x .prog1. y as x end define ]]" 2301 2302 \item "[[ macro define measure ( x , y ) as trace ( x ) .then. timer ( x ) .then. y .prog1. timer ( true ) end define ]]" 2303 2304 \end{statements} 2305 2306 2307 2308 \subsection{Verification}\label{sec:Verification} 2309 2310 \begin{statements} 2311 2312 \item "[[ define claim of base as test1 end define ]]" 2313 2314 \item "[[ define value of x &c y as \ c . x ' c .and. y ' c end define ]]" 2315 2316 \item "[[ define value of test1 as \ c . test2 ( c ) end define ]]" 2317 2318 \item "[[ define value of test2 ( c ) as norm c is val : newline 2319 2320 LET test3 ( c [[ c [[ 0 ]] ]] [[ "expansion" ]] , c ) catch BE p IN newline 2321 2322 if p tail != true then diagnose p tail end diagnose else newline 2323 2324 if p head then show quote "In testsuite: unprocessed exception" end quote end show else newline 2325 2326 spy ( true ) .then. true end define ]]" 2327 2328 \item "[[ define value of diagnose x end diagnose as norm x is val : newline 2329 2330 ( quote diagnose x end diagnose end quote ref :: quote diagnose x end diagnose end quote idx :: x debug ) :: x :: true end define ]]" 2331 2332 \item "[[ define value of test3 ( t , c ) as norm t is val : c is val : newline 2333 2334 LET t ref BE r IN newline 2335 2336 LET t idx BE i IN newline 2337 2338 if r = 0 .or. i = 0 then true else newline 2339 2340 LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ "claim" ]] BE d IN newline 2341 2342 if d pairp then ( eval ( d third , true , c ) apply ( t :: c :: true ) maptag ) untag else newline 2343 2344 if c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ "definition" ]] != true then true else test3* ( t tail , c ) end define ]]" 2345 2346 \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 ]]" 2347 2348 \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 ]]" 2349 2350 \item "[[ define claim of ttst u end test as \ x . ttst1 ( x ) end define ]]" 2351 2352 \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 ]]" 2353 2354 \item "[[ define claim of ftst u end test as \ x . ftst1 ( x ) end define ]]" 2355 2356 \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 ]]" 2357 2358 \item "[[ define claim of etst u ; v end test as \ x . etst1 ( x ) end define ]]" 2359 2360 \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 ]]" 2361 2362 \item "[[ ttst true end test ]]" 2363 2364 \item "[[ ftst false end test ]]" 2365 2366 \item "[[ etst 2 ; 2 end test ]]" 2367 2368 \item "[[ etst 2 raise ; 2 raise end test ]]" 2369 2370 \end{statements} 2371 2372 2373 2374 \subsection{Idiosyncrasies} 2375 2376 Logiweb reacts in a predictable way to definitions, even if they look dubious: 2377 2378 \begin{statements} 2379 2380 \item "[[ value define testfunc1 ( x ) as x + 3 end define ]]" 2381 2382 This is an ordinary definition. Thus we have: "[[ etst testfunc1 ( 2 ) ; 5 end test ]]". 2383 2384 \item "[[ value define testfunc2 ( x , x ) as x end define ]]" 2385 2386 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 ]]". 2387 2388 \item "[[ value define testfunc3 as 2 end define ]]" and "[[ value define testfunc3 as 3 end define ]]" 2389 2390 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. 2391 2392 \item "[[ value define testfunc4 as quote value define testfunc4 as 2 end define end quote end define ]]" 2393 2394 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 ]]". 2395 2396 \item "[[ value define testfunc5 ( x ) as y end define ]]" 2397 2398 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 ]]" 2399 2400 \item "[[ value define testfunc6 ( 2 ) as 2 end define ]]" 2401 2402 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 ]]" 2403 2404 \item "[[ value define testfunc7 ( x _ { 4 } ) as x _ { 4 } + 3 end define ]]" 2405 2406 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. 2407 2408 \item "[[ value define testfunc8 ( x _ { 2 + 2 } , x _ { 4 } ) as x _ { 2 + 2 } + x _ { 4 } end define ]]" 2409 2410 "[[ 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. 2411 2412 \item "[[ define value of base as 2 + 3 end define ]]" 2413 2414 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 ]]" 2415 2416 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. 2417 2418 \end{statements} 2419 2420 2421 2422 " ]"\section{Compilation}\label{sec:Compilation}"[ " 2423 2424 \subsection{Fixed point combinator} 2425 2426 \begin{statements} 2427 2428 \item "[[ optimized define value of YY as \ f . ( \ x . f ' ( x ' x ) ) ' ( \ x . f ' ( x ' x ) ) end define ]]" 2429 2430 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. 2431 2432 \end{statements} 2433 2434 2435 2436 \subsection{Compiler} 2437 2438 \begin{statements} 2439 2440 \item "[[ optimized define value of compile ( c ) as norm c is val : newline 2441 2442 ( map ( \ c . YY ' \ C . compile1 ( c [[ 0 ]] , c , map ( C ) ) ) apply c maptag ) untag end define ]]" 2443 2444 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 ]]". 2445 2446 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. 2447 2448 The compile1 function performs a few sanity checks and throws an exception if it finds something wrong. 2449 2450 2451 2452 \item "[[ define value of compile1 ( r , c , C ) as norm r is val : c is val : C is val : newline 2453 2454 if .not. r intp then exception else newline 2455 2456 LET c [[ r :: "code" :: true => compile2 ( r , c , C ) ]] BE c IN newline 2457 2458 LET c [[ r :: "diagnose" :: true => compile-claim ( r , c , C ) ]] BE c IN c end define ]]" 2459 2460 Compile cache "[[ c ]]" which has reference "[[ r ]]". "[[ C ]]" is the compiled cache as explained above. 2461 2462 2463 2464 \item "[[ define value of compile2 ( r , c , C ) as norm r is val : c is val : C is val : newline 2465 2466 compile3 ( C , c [[ r ]] [[ "codex" ]] [[ r ]] , true ) end define ]]" 2467 2468 Compile the codex part of the cache "[[ c ]]". "[[ C ]]" is the compiled cache (see above). 2469 2470 2471 2472 \item "[[ define value of compile3 ( C , x , X ) as norm C is val : x is val : X is val : newline 2473 2474 if x then X else newline 2475 2476 if x head intp then X [[ x head -> compile4 ( x tail , C ) ]] else newline 2477 2478 compile3 ( C , x head , compile3 ( C , x tail , X ) ) end define ]]" 2479 2480 Compile the codex part "[[ x ]]" of the cache "[[ c ]]". "[[ C ]]" is the compiled cache (see above) and the result is accumulated in "[[ X ]]". 2481 2482 2483 2484 \item "[[ define value of compile4 ( x , C ) as norm x is val : C is val : newline 2485 2486 LET x [[ 0 ]] [[ "value" ]] BE d IN newline 2487 2488 if d then true else newline 2489 2490 if .not. d pairp .or. .not. d head pairp then exception else newline 2491 2492 if d ref != 0 then newline 2493 2494 map ( \ d . \ C . compile-code ( d , C ) Tail ' true ) apply d maptag apply C else newline 2495 2496 if .not. d head tail pairp then exception else newline 2497 2498 LET d head tail head BE i IN newline 2499 2500 if i = "lambda" then 0 else newline 2501 2502 if i = "quote" then 1 else newline 2503 2504 if i = "true" then true maptag else newline 2505 2506 if i = "apply" then map ( \ x . \ y . x ' y ) else newline 2507 2508 if i = "if" then map ( \ x . \ y . \ z . If x then y else z ) else exception end define ]]" 2509 2510 Compile the codex branch "[[ x ]]" by looking up the value definition "[[ d ]]" in it (if any) and compile "[[ d ]]". 2511 2512 \end{statements} 2513 2514 2515 2516 \subsection{Code constructors} 2517 2518 \begin{statements} 2519 2520 \item "[[ define value of make-constant ( v ) as norm v is val : map ( \ v . \ s . v ) apply v maptag end define ]]" 2521 2522 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. 2523 2524 2525 2526 \item "[[ define value of deBruijn ( v , a , b ) as norm v is val : a is val : b is val : newline 2527 2528 if a then deBruijn1 ( v , b ) else newline 2529 2530 if .not. a pairp then exception else newline 2531 2532 if v t= a head then 0 else 1 + deBruijn ( v , a tail , b ) end define ]]" 2533 2534 \item "[[ define value of deBruijn1 ( v , b ) as norm v is val : b is val : newline 2535 2536 if .not. b pairp then exception else newline 2537 2538 if v t= b head then deBruijn2 ( b tail ) else deBruijn1 ( v , b tail ) end define ]]" 2539 2540 \item "[[ define value of deBruijn2 ( b ) as norm b is val : newline 2541 2542 if b then 0 else if b pairp then 1 + deBruijn2 ( b tail ) else exception end define ]]" 2543 2544 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. 2545 2546 2547 2548 \item "[[ define value of lazy-nth ( i , s ) as If i = 0 then s Head else lazy-nth ( i - 1 , s Tail ) end define ]]" 2549 2550 2551 2552 \item "[[ define value of make-variable ( v , a , b ) as norm v is val : a is val : b is val : newline 2553 2554 LET deBruijn ( v , a , b ) catch tail BE i IN newline 2555 2556 if i then make-constant ( true ) else newline 2557 2558 map ( \ i . \ s . lazy-nth ( i , s ) ) apply i maptag end define ]]" 2559 2560 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. 2561 2562 2563 2564 \item "[[ define value of make-lambda ( f ) as norm f is val : newline 2565 2566 map ( \ f . \ s . \ x . f ' ( x LazyPair s ) ) apply f end define ]]" 2567 2568 Add lambda abstraction to the uncurried function "[[ f ]]". "[[ s ]]" is the stack and "[[ x ]]" is the lambda variable to be pushed on the stack. 2569 2570 2571 2572 \item "[[ define value of make-lambdas ( a , f ) as norm a is val : f is val : newline 2573 2574 if .not. a pairp then f else newline 2575 2576 make-lambda ( make-lambdas ( a tail , f ) ) end define ]]" 2577 2578 Add one lambda per argument in the argument list "[[ a ]]". 2579 2580 \end{statements} 2581 2582 2583 2584 \subsection{Compilation of individual constructs} 2585 2586 \begin{statements} 2587 2588 \item "[[ define value of compile-code ( d , c ) as norm d is val : c is val : newline 2589 2590 if .not. d tail tail tail pairp .or. .not. d tail tail tail tail .or. .not. d second pairp then exception else newline 2591 2592 compile-code1 ( d second tail , d third , c ) end define ]]" 2593 2594 2595 2596 \item "[[ define value of compile-code1 ( b , t , c ) as norm b is val : t is val : c is val : newline 2597 2598 make-lambdas ( b , compile-code2 ( true , b , t , c ) ) end define ]]" 2599 2600 Compile "[[ t ]]" and add one lambda per argument. 2601 2602 2603 2604 \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 2605 2606 if .not. t pairp .or. .not. t head pairp .or. .not. t head tail pairp then exception else newline 2607 2608 LET t ref BE r IN newline 2609 2610 LET t idx BE i IN newline 2611 2612 if .not. r intp .or. .not. i intp then exception else newline 2613 2614 if r = 0 then make-constant ( i ) else newline 2615 2616 if i = 0 then if r = c [[ 0 ]] then make-constant ( c ) else newline 2617 2618 make-constant ( c [[ c [[ 0 ]] ]] [[ "cluster" ]] [[ r ]] ) else newline 2619 2620 LET c [[ r ]] [[ "code" ]] [[ i ]] BE f IN newline 2621 2622 if f mapp then newline 2623 2624 compile-code2* ( map ( \ f . \ s . f ) apply f , a , b , t tail , c ) else newline 2625 2626 if f = true then make-variable ( t , a , b ) else newline 2627 2628 if f = 1 then make-constant ( t first ) else newline 2629 2630 make-lambda ( compile-code2 ( t first :: a , b , t second , c ) ) end define ]]" 2631 2632 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 ]]". 2633 2634 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. 2635 2636 2637 2638 \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 2639 2640 if t then f else newline 2641 2642 compile-code2* ( map ( \ f . \ x . \ s . f ' s ' ( x ' s ) ) apply f apply newline 2643 2644 compile-code2 ( a , b , t head , c ) , a , b , t tail , c ) end define ]]" 2645 2646 Apply the function "[[ f ]]" to compiled versions of the elements of the list "[[ t ]]" of terms. 2647 2648 \end{statements} 2649 2650 2651 2652 \subsection{Claim evaluation} 2653 2654 \begin{statements} 2655 2656 \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 ]]" 2657 2658 2659 2660 \item "[[ define value of prune1 ( t , C ) as norm t is val : C is val : newline 2661 2662 LET ( C [[ 0 ]] :: 0 ) :: true BE b IN newline 2663 2664 if .not. t pairp .or. .not. t head pairp .or. .not. t head tail pairp then b else newline 2665 2666 LET t ref BE r IN newline 2667 2668 LET t idx BE i IN newline 2669 2670 if .not. r intp .or. .not. i intp then b else newline 2671 2672 if r = 0 then if t tail then t else b else newline 2673 2674 if i = 0 then if t tail then t else b else newline 2675 2676 LET C [[ r ]] [[ "dictionary" ]] [[ i ]] BE a IN newline 2677 2678 if .not. a intp .or. a < 0 then b else newline 2679 2680 LET prune* ( a , t tail , C ) catch BE v IN newline 2681 2682 if v head then b else t head :: v tail end define ]]" 2683 2684 2685 2686 \item "[[ define value of prune* ( a , t , C ) as norm a is val : t is val : C is val : newline 2687 2688 if a = 0 then if t then true else exception else newline 2689 2690 if .not. t pairp then exception else newline 2691 2692 prune1 ( t head , C ) :: prune* ( a - 1 , t tail , C ) end define ]]" 2693 2694 2695 2696 \item "[[ define value of eval-claim as norm map ( \ d . \ C . prune ( ( eval ( d third , true , C ) apply C maptag ) untag , C ) ) end define ]]" 2697 2698 2699 2700 \item "[[ define value of compile-claim ( r , c , C ) as norm r is val : c is val : C is val : newline 2701 2702 LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ 0 ]] [[ 0 ]] [[ "claim" ]] BE d IN newline 2703 2704 if d pairp then eval-claim apply d maptag apply C else newline 2705 2706 LET c [[ r ]] [[ "bibliography" ]] first BE r IN 2707 2708 if r then true maptag else newline 2709 2710 LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ 0 ]] [[ 0 ]] [[ "claim" ]] BE d IN newline 2711 2712 if d pairp then eval-claim apply d maptag apply C else true maptag 2713 2714 end define ]]" 2715 2716 \end{statements} 2717 2718 2719 2720 " ]"\section{Macro expansion}\label{sec:MacroExpansion}"[ " 2721 2722 \subsection{Macro expansion engine} 2723 2724 \begin{statements} 2725 2726 \item "[[ define macro of base as macro1 end define ]]" 2727 2728 \item "[[ define value of macro1 as \ c . macro2 ( c ) end define ]]" 2729 2730 \item "[[ define value of macro2 ( c ) as norm c is val : newline 2731 2732 macro3 ( c [[ c [[ 0 ]] ]] [[ "body" ]] , macrostate0 , c ) end define ]]" 2733 2734 \item "[[ define value of macro3 ( t , s , c ) as norm t is val : s is val : c is val : newline 2735 2736 LET t ref BE r IN newline 2737 2738 LET t idx BE i IN newline 2739 2740 if r = 0 then t else newline 2741 2742 if i = 0 then t else newline 2743 2744 LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ "macro" ]] BE d IN newline 2745 2746 if d = true then t head :: macro3* ( t tail , s , c ) else newline 2747 2748 ( eval ( d third , true , c ) apply ( t :: s :: c :: true ) maptag ) untag end define ]]" 2749 2750 \item "[[ define value of macro3* ( t , s , c ) as norm t is val : s is val : c is val : newline 2751 2752 if t atom then true else 2753 2754 macro3 ( t head , s , c ) :: macro3* ( t tail , s , c ) 2755 2756 end define ]]" 2757 2758 \item "[[ define value of macro4 ( x ) as norm x is val : macro3 ( x zeroth , x first , x second ) end define ]]" 2759 2760 \item "[[ define value of macrostate0 as norm map ( \ x . macro4 ( x ) ) :: true end define ]]" 2761 2762 \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 ]]" 2763 2764 \item "[[ define value of stateexpand* ( t , s , c ) as norm t is val : s is val : c is val : newline 2765 2766 if t atom then true else newline 2767 2768 stateexpand ( t head , s , c ) :: stateexpand* ( t tail , s , c ) end define ]]" 2769 2770 \end{statements} 2771 2772 2773 2774 \subsection{Backquoting} 2775 2776 \begin{statements} 2777 2778 \item "[[ define value of substitute ( r , t , s ) as norm r is val : t is val : s is val : newline 2779 2780 LET lookup ( t , s , true ) BE d IN newline 2781 2782 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 ]]" 2783 2784 \item "[[ define value of substitute* ( r , t , s ) as norm r is val : t is val : s is val : newline 2785 2786 if t atom then true else newline 2787 2788 substitute ( r , t head , s ) :: substitute* ( r , t tail , s ) end define ]]" Coordinatwise application of substitute to the elements of the list "[[ t ]]". 2789 2790 \item "[[ define value of expand ( d , x ) as norm d is val : x is val : newline 2791 2792 LET x zeroth BE t IN LET zip ( d first tail , t tail ) BE s IN newline 2793 2794 stateexpand ( substitute ( t , d second , s ) , x first , x second ) end define ]]" 2795 2796 "[[ 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 ]]". 2797 2798 \end{statements} 2799 2800 2801 2802 \subsection{Elementary macros}\label{sec:ElementaryMacros} 2803 2804 \begin{statements} 2805 2806 \item "[[ protect define macro of protect u end protect as \ x . x zeroth first end define end protect ]]" 2807 2808 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! 2809 2810 \item "[[ protect define macro of Macro define u as v end define as \ x . Macrodefine ( x ) end define end protect ]]" 2811 2812 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. 2813 2814 \item "[[ define value of Macrodefine ( x ) as norm x is val : newline 2815 2816 if x = true then quote true end quote else newline 2817 2818 LET x zeroth BE t IN newline 2819 2820 LET t first BE u IN LET t second BE v IN newline 2821 2822 LET ( quote u end quote :: u ) :: ( quote v end quote :: v ) :: true BE s IN newline 2823 2824 substitute ( t , quote protect define macro of u as v end define end protect end quote , s ) end define ]]" 2825 2826 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. 2827 2828 \item "[[ Macro define macro define u as v end define as \ x . macrodefine ( x ) end define ]]" 2829 2830 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. 2831 2832 \item "[[ define value of macrodefine ( x ) as norm x is val : newline 2833 2834 LET x zeroth BE t IN newline 2835 2836 LET t first BE u IN newline 2837 2838 LET ( quote t end quote :: t ) :: ( quote u end quote :: u ) :: true BE s IN newline 2839 2840 substitute ( t , quote define macro of u as \ x . expand ( quote t end quote , x ) end define end quote , s ) end define ]]" 2841 2842 This construct is similar to "[[ Macrodefine ( x ) ]]". 2843 2844 \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. 2845 2846 \item "[[ define value of makeself ( x ) as norm x is val : newline 2847 2848 LET x zeroth BE t IN LET x second BE c IN newline 2849 2850 LET t debug BE d IN LET c [[ 0 ]] BE r IN newline 2851 2852 ( ( r :: 0 :: d ) :: true ) end define ]]" 2853 2854 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. 2855 2856 \item "[[ Macro define root protect u end protect as \ x . rootprotect ( x ) end define ]]" 2857 2858 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. 2859 2860 \item "[[ define value of rootprotect ( x ) as norm x is val : newline 2861 2862 LET x zeroth BE t IN LET t first BE u IN newline 2863 2864 LET u ref BE r IN LET u idx BE i IN LET t debug BE d IN newline 2865 2866 ( r :: i :: d ) :: stateexpand* ( u tail , x first , x second ) end define ]]" 2867 2868 \end{statements} 2869 2870 2871 2872 \subsection{Definition macros} 2873 2874 \begin{statements} 2875 2876 \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 ]]" 2877 2878 Define the render aspect of a construct. The construct itself is protected against macro expansion. 2879 2880 \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 ]]" 2881 2882 Define the tex use aspect of a construct. The construct itself is protected against macro expansion. 2883 2884 \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 ]]" 2885 2886 \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 ]]" 2887 2888 \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 ]]" 2889 2890 \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 ]]" 2891 2892 \item "[[ macro define priority table x as define priority of self as protect x end protect end define end define ]]" 2893 2894 Define the priority table of the page. 2895 2896 \item "[[ macro define verifier x end verifier as define claim of self as x end define end define ]]" 2897 2898 Define the claim of the page. 2899 2900 \item "[[ macro define unpacker x end unpacker as define unpack of self as x end define end define ]]" 2901 2902 Define the unpacker of the page. 2903 2904 \item "[[ macro define renderer x end renderer as define render of self as x end define end define ]]" 2905 2906 Define the renderer of the page. 2907 2908 \item "[[ macro define expander x end expander as define macro of self as x end define end define ]]" 2909 2910 Define the macro expansion engine of the page. 2911 2912 \item "[[ protect proclaim tex use define x as y end define as "hide" end proclaim end protect ]]" 2913 2914 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. 2915 2916 \item "[[ protect proclaim tex show define x as y end define as "hide" end proclaim end protect ]]" 2917 2918 Ensure that the tex show definition construct can be used on the present page. 2919 2920 \item "[[ protect proclaim priority table x as "hide" end proclaim end protect ]]" 2921 2922 Ensure that the priority table construct can be used on the present page. 2923 2924 \item "[[ protect proclaim macro define x as y end define as "hide" end proclaim end protect ]]" 2925 2926 Ensure that macro definitions can expand into definitions without causing trouble at early stages of codification. 2927 2928 \end{statements} 2929 2930 2931 2932 \subsection{Parentheses}\label{sec:Parentheses} 2933 2934 \begin{statements} 2935 2936 \item "[[ macro define ( x ) as x end define ]]" 2937 2938 Ordinary parentheses. 2939 2940 \item "[[ macro define newline x as x end define ]]" 2941 2942 Put newline before x. The construct has charge 32. 2943 2944 \item "[[ macro define tight newline x as x end define ]]" 2945 2946 Put newline before x. The construct has charge 2. 2947 2948 \item "[[ late eager define include ( x ) as x end define ]]" 2949 2950 This has value x but renders x as an elipsis. 2951 2952 \item "[[ macro define x tight endline as x end define ]]" 2953 2954 Put newline after x. The construct has charge 4. 2955 2956 \item "[[ macro define x endline as x end define ]]" 2957 2958 Put newline after x. The construct has charge 50. 2959 2960 \end{statements} 2961 2962 2963 2964 \subsection{Numerals}\label{sec:Numerals} 2965 2966 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. 2967 2968 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+. 2969 2970 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. 2971 2972 \begin{statements} 2973 2974 \item "[[ Macro define 0x as \ x . numeral ( x ) end define ]]" 2975 2976 \item "[[ Macro define 1x as \ x . numeral ( x ) end define ]]" 2977 2978 \item "[[ Macro define 2x as \ x . numeral ( x ) end define ]]" 2979 2980 \item "[[ Macro define 3x as \ x . numeral ( x ) end define ]]" 2981 2982 \item "[[ Macro define 4x as \ x . numeral ( x ) end define ]]" 2983 2984 \item "[[ Macro define 5x as \ x . numeral ( x ) end define ]]" 2985 2986 \item "[[ Macro define 6x as \ x . numeral ( x ) end define ]]" 2987 2988 \item "[[ Macro define 7x as \ x . numeral ( x ) end define ]]" 2989 2990 \item "[[ Macro define 8x as \ x . numeral ( x ) end define ]]" 2991 2992 \item "[[ Macro define 9x as \ x . numeral ( x ) end define ]]" 2993 2994 \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 ]]" 2995 2996 \item "[[ protect define value of num1 ( r , t , u ) as norm r is val : t is val : u is val : newline 2997 2998 if t tail then num2 ( r , t , u ) else newline 2999 3000 LET ( quote x end quote :: u ) :: true BE s IN newline 3001 3002 if t r= quote 0x end quote then num1 ( r , t first , substitute ( r , quote x %0 end quote , s ) ) else newline 3003 3004 if t r= quote 1x end quote then num1 ( r , t first , substitute ( r , quote x %1 end quote , s ) ) else newline 3005 3006 if t r= quote 2x end quote then num1 ( r , t first , substitute ( r , quote x %2 end quote , s ) ) else newline 3007 3008 if t r= quote 3x end quote then num1 ( r , t first , substitute ( r , quote x %3 end quote , s ) ) else newline 3009 3010 if t r= quote 4x end quote then num1 ( r , t first , substitute ( r , quote x %4 end quote , s ) ) else newline 3011 3012 if t r= quote 5x end quote then num1 ( r , t first , substitute ( r , quote x %5 end quote , s ) ) else newline 3013 3014 if t r= quote 6x end quote then num1 ( r , t first , substitute ( r , quote x %6 end quote , s ) ) else newline 3015 3016 if t r= quote 7x end quote then num1 ( r , t first , substitute ( r , quote x %7 end quote , s ) ) else newline 3017 3018 if t r= quote 8x end quote then num1 ( r , t first , substitute ( r , quote x %8 end quote , s ) ) else newline 3019 3020 if t r= quote 9x end quote then num1 ( r , t first , substitute ( r , quote x %9 end quote , s ) ) else newline 3021 3022 substitute ( r , quote exception end quote , true ) end define end protect ]]" 3023 3024 \item "[[ define value of num2 ( r , t , u ) as norm r is val : t is val : u is val : newline 3025 3026 LET ( quote x end quote :: u ) :: true BE s IN newline 3027 3028 if t r= quote 0 end quote then substitute ( r , quote x %0 end quote , s ) else newline 3029 3030 if t r= quote 1 end quote then substitute ( r , quote x %1 end quote , s ) else newline 3031 3032 if t r= quote 2 end quote then substitute ( r , quote x %2 end quote , s ) else newline 3033 3034 if t r= quote 3 end quote then substitute ( r , quote x %3 end quote , s ) else newline 3035 3036 if t r= quote 4 end quote then substitute ( r , quote x %4 end quote , s ) else newline 3037 3038 if t r= quote 5 end quote then substitute ( r , quote x %5 end quote , s ) else newline 3039 3040 if t r= quote 6 end quote then substitute ( r , quote x %6 end quote , s ) else newline 3041 3042 if t r= quote 7 end quote then substitute ( r , quote x %7 end quote , s ) else newline 3043 3044 if t r= quote 8 end quote then substitute ( r , quote x %8 end quote , s ) else newline 3045 3046 if t r= quote 9 end quote then substitute ( r , quote x %9 end quote , s ) else newline 3047 3048 substitute ( r , quote exception end quote , true ) end define ]]" 3049 3050 \end{statements} 3051 3052 3053 3054 \subsection{Formating of the expansion} 3055 3056 \begin{statements} 3057 3058 \item "[[ macro define make macro expanded version ragged right as ragged right end define ]]" 3059 3060 \end{statements} 3061 3062 3063 3064 \subsection{Visibility constructs}\label{sec:VisibilityConstructs} 3065 3066 The following constructs affect \indexintro{visibility}: 3067 3068 \begin{statements} 3069 3070 \item "[[ show show x end show end show ]]" renders the constructs in "[[ x ]]" using the tex show aspect. 3071 3072 \item "[[ show !x end show ]]": Save as "[[ show show x end show end show ]]" but shorter. 3073 3074 \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. 3075 3076 \item "[[ show hide x end hide end show ]]" hides "[[ x ]]" from harvesting, c.f. Section \ref{sec:Proclamations}. 3077 3078 \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. 3079 3080 \end{statements} 3081 3082 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: 3083 3084 \begin{statements} 3085 3086 \item "[[ optimized define value of show x end show as x end define ]]" 3087 3088 \item "[[ optimized define value of !x as x end define ]]" 3089 3090 \item "[[ macro define macro show x end show as x end define ]]" 3091 3092 \item "[[ optimized define value of hide x end hide as x end define ]]" 3093 3094 \item "[[ proclaim hide x end hide as "hide" end proclaim ]]" 3095 3096 \item "[[ optimized define value of hiding show x end show as x end define ]]" 3097 3098 \item "[[ macro define hiding show x end show as protect hiding show x end show end protect end define ]]" 3099 3100 \item "[[ proclaim hiding show x end show as "hide" end proclaim ]]" 3101 3102 \end{statements} 3103 3104 3105 3106 \subsection{Tuples} 3107 3108 \begin{statements} 3109 3110 \item "[[ value define <<>> as norm true end define ]]" 3111 3112 \item "[[ Macro define << u >> as \ x . tuple1 ( x ) end define ]]" 3113 3114 \item "[[ define value of tuple1 ( x ) as norm x is val : stateexpand ( tuple2 ( x zeroth , x zeroth first ) , x first , x second ) end define ]]" 3115 3116 \item "[[ define value of tuple2 ( t , u ) as norm t is val : u is val : newline 3117 3118 if .not. u r= quote x ,, y end quote then newline 3119 3120 substitute ( t , quote u :: <<>> end quote , ( quote u end quote :: u ) :: true ) else newline 3121 3122 substitute ( t , quote x :: y end quote , ( quote x end quote :: u first ) :: ( quote y end quote :: tuple2 ( t , u second ) ) :: true ) end define ]]" 3123 3124 \end{statements} 3125 3126 3127 3128 \subsection{Eager definitions}\label{sec:EagerDefinitions} 3129 3130 \begin{statements} 3131 3132 \item "[[ Macro define eager define u as v end define as \ x . eager1 ( x ) end define ]]" 3133 3134 Construct of eager definitions. 3135 3136 \item "[[ define value of eager1 ( x ) as norm x is val : newline 3137 3138 LET x zeroth BE t IN newline 3139 3140 LET t first BE u IN LET t second BE v IN newline 3141 3142 LET ( quote u end quote :: u ) :: ( quote w end quote :: eager2 ( t , u tail , v ) ) :: true BE s IN newline 3143 3144 stateexpand ( substitute ( t , quote define value of u as norm w end define end quote , s ) , x first , x second ) end define ]]" 3145 3146 \item "[[ define value of eager2 ( t , p , v ) as norm t is val : p is val : v is val : newline 3147 3148 if p atom then v else newline 3149 3150 LET ( quote x end quote :: p head ) :: ( quote v end quote :: eager2 ( t , p tail , v ) ) :: true BE s IN newline 3151 3152 substitute ( t , quote x is val : v end quote , s ) end define ]]" 3153 3154 \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 ]]" 3155 3156 \end{statements} 3157 3158 3159 3160 \subsection{Late definitions} 3161 3162 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. 3163 3164 \begin{statements} 3165 3166 \item "[[ macro define late eager define u as v end define as eager define u as v end define end define ]]" 3167 3168 \item "[[ proclaim late unhide x end unhide as "hide" end proclaim ]]" 3169 3170 \item "[[ macro define late unhide x end unhide as x end define ]]" 3171 3172 \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 ]]" 3173 3174 \end{statements} 3175 3176 3177 3178 \subsection{Let constructs}\label{sec:LetConstructs} 3179 3180 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. 3181 3182 \begin{statements} 3183 3184 \item "[[ Macro define let u := v in w as \ x . macrolet1 ( x ) end define ]]" 3185 3186 The construct above locally defines "[[ u ]]" to macro expand to "[[ v ]]" inside "[[ w ]]". 3187 3188 \item "[[ define value of macrolet1 ( x ) as norm x is val : newline 3189 3190 LET x zeroth BE t IN LET x first BE s IN LET x second BE c IN newline 3191 3192 LET t first BE u IN LET t third BE w IN newline 3193 3194 LET u ref BE r IN LET u idx BE i IN newline 3195 3196 LET c [[ r :: "codex" :: r :: i :: 0 :: "macro" :: true => macrodefine ( x ) ]] BE c IN newline 3197 3198 stateexpand ( w , s , c ) end define ]]" 3199 3200 The function above implements local macro definitions. 3201 3202 \item "[[ define message of destructure as "destructure" end define ]]" 3203 3204 The destructure aspect allows to define how a value is destructured by a particular pattern. We only define destructuring of pairs in the following. 3205 3206 \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 ]]" 3207 3208 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. 3209 3210 \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 ]]" 3211 3212 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}. 3213 3214 \item "[[ Macro define let u = v in w as \ x . let1 ( x ) end define ]]" 3215 3216 \item "[[ define value of let1 ( x ) as norm x is val : newline 3217 3218 LET x zeroth BE t IN LET x first BE s IN LET x second BE c IN newline 3219 3220 LET t first BE u IN LET t second BE v IN LET t third BE w IN newline 3221 3222 LET stateexpand ( u , s , c ) BE u IN newline 3223 3224 LET stateexpand ( v , s , c ) BE v IN newline 3225 3226 LET stateexpand ( w , s , c ) BE w IN newline 3227 3228 LET make-prime ( make-var ( t ) ) BE x IN newline 3229 3230 LET let2 ( x , u , w , c ) BE w IN newline 3231 3232 make-let ( quote asterisk end quote , v , w ) 3233 3234 end define ]]" 3235 3236 \item "[[ define value of let2 ( x , p , w , c ) as norm x is val : p is val : w is val : c is val : newline 3237 3238 LET p ref BE r IN LET p idx BE i IN newline 3239 3240 LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] BE c prime IN newline 3241 3242 LET c prime [[ "destructure" ]] BE d IN newline 3243 3244 if d = true then newline 3245 3246 if c prime [[ "value" ]] != true then w else make-let ( p , quote asterisk end quote , w ) else newline 3247 3248 LET let3 ( x , p tail , w , c ) BE w IN newline 3249 3250 make-let ( x , d third , w ) 3251 3252 end define ]]" 3253 3254 \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 3255 3256 if p prime = true then w else newline 3257 3258 LET p prime head BE p IN LET p prime tail BE p prime IN newline 3259 3260 LET let3 ( x , p prime , w , c ) BE w IN newline 3261 3262 LET let2 ( make-prime ( x ) , p , w , c ) BE w IN newline 3263 3264 LET make-let ( x , make-tail ( x ) , w ) BE w IN newline 3265 3266 make-let ( quote asterisk end quote , make-head ( x ) , w ) end define ]]" 3267 3268 \item "[[ define value of make-var ( t ) as norm t is val : newline 3269 3270 substitute ( t , quote asterisk end quote , true ) end define ]]" 3271 3272 \item "[[ define value of make-let ( u , v , w ) as norm u is val : v is val : w is val : newline 3273 3274 LET ( quote u end quote :: u ) :: ( quote v end quote :: v ) :: ( quote w end quote :: w ) :: true BE s IN newline 3275 3276 substitute ( u , quote LET v BE u IN w end quote , s ) end define ]]" 3277 3278 \item "[[ define value of make-prime ( x ) as norm x is val : newline 3279 3280 LET ( quote x end quote :: x ) :: true BE s IN newline 3281 3282 substitute ( x , quote x prime end quote , s ) end define ]]" 3283 3284 \item "[[ define value of make-head ( x ) as norm x is val : newline 3285 3286 LET ( quote x end quote :: x ) :: true BE s IN newline 3287 3288 substitute ( x , quote x head end quote , s ) end define ]]" 3289 3290 \item "[[ define value of make-tail ( x ) as norm x is val : newline 3291 3292 LET ( quote x end quote :: x ) :: true BE s IN newline 3293 3294 substitute ( x , quote x tail end quote , s ) end define ]]" 3295 3296 \end{statements} 3297 3298 3299 3300 \subsection{Backquoting} 3301 3302 \begin{statements} 3303 3304 \item "[[ Macro define back u quote v end quote as \ x . backquote0 ( x ) end define ]]" 3305 3306 \item "[[ define value of make-root ( t , x ) as norm t is val : x is val : x ref :: x idx :: t debug end define ]]" 3307 3308 \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 ]]" 3309 3310 \item "[[ define value of make-true ( t ) as norm t is val : make-root ( t , quote true end quote ) :: true end define ]]" 3311 3312 \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 ]]" 3313 3314 \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 ]]" 3315 3316 \item "[[ define value of backquote0 ( x ) as norm x is val : backquote1 ( x zeroth , x first , x second ) end define ]]" 3317 3318 \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 ]]" 3319 3320 \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 3321 3322 if v r= quote true unquote end quote then v first else newline 3323 3324 make-pair ( t , make-make-root ( t , u , make-quote ( t , v ) ) , backquote2* ( t , u , v tail , s , c ) ) end define ]]" 3325 3326 \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 3327 3328 if v atom then make-true ( t ) else newline 3329 3330 make-pair ( t , backquote2 ( t , u , v head , s , c ) , backquote2* ( t , u , v tail , s , c ) ) end define ]]" 3331 3332 \end{statements} 3333 3334 3335 3336 \subsection{Rendering} 3337 3338 We define a number of constructs for rendering. To see how most of them are used, consult the source of the present Logiweb page. 3339 3340 \begin{statements} 3341 3342 \item "[[ show text x : y end text end show ]]". Store the text "[[ y ]]" in a file named "[[ x ]]". 3343 3344 \item "[[ show latex ( x ) end show ]]". Run latex on the file named "[[ x ]]". 3345 3346 \item "[[ show bibtex ( x ) end show ]]". Run bibtex on the file named "[[ x ]]". 3347 3348 \item "[[ show makeindex ( x ) end show ]]". Run makeindex on the file named "[[ x ]]". 3349 3350 \item "[[ show dvipdfm ( x ) end show ]]". Run dvipdfm on the file named "[[ x ]]". 3351 3352 \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''. 3353 3354 \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''. 3355 3356 \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. 3357 3358 \end{statements} 3359 3360 Only the `page' construct needs a definition here. All the other ones just have tex use definitions which are stated later. 3361 3362 \begin{statements} 3363 3364 \item "[[ Macro define page ( x , y ) title t bib b main text m appendix a end page as \ z . page1 ( z ) end define ]]" 3365 3366 \item "[[ define value of page1 ( z ) as norm z is val : newline 3367 3368 LET z zeroth BE t IN newline 3369 3370 LET z first BE s IN newline 3371 3372 LET z second BE c IN newline 3373 3374 LET t second BE y IN newline 3375 3376 LET stateexpand ( t fifth , s , c ) BE m IN newline 3377 3378 LET stateexpand ( t sixth , s , c ) BE a IN newline 3379 3380 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 3381 3382 ( p ref :: p idx :: t debug ) :: t first :: y :: t third :: t fourth :: m :: a :: true end define ]]" 3383 3384 \end{statements} 3385 3386 3387 3388 " ]"\section{The Logiweb machine}\label{sec:Interaction}"[ " 3389 3390 A \index{machine, Logiweb}\indexintro{Logiweb machine} is an abstract machine which consists of 3391 3392 \begin{itemize} 3393 3394 \item a Logiweb computing engine, 3395 3396 \item an \indexintro{interface}, 3397 3398 \item a \index{handler, boot}\indexintro{boot handler}, and 3399 3400 \item a \indexintro{cache}. 3401 3402 \end{itemize} 3403 3404 \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. 3405 3406 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. 3407 3408 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. 3409 3410 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. 3411 3412 3413 3414 \subsection{Messages}\label{section:Messages} 3415 3416 The virgin Logiweb machine knows the following output events: 3417 3418 \["[ array ( left ) 3419 3420 late eager define quit request ( x ) as << << 0 ,, "quit" >> ,, x >> end define \\ 3421 3422 late eager define write request ( s ) as << << 0 ,, "write" >> ,, s >> end define \\ 3423 3424 late eager define read request as << << 0 ,, "read" >> >> end define \\ 3425 3426 late eager define exec request ( p , h ) as << << 0 ,, "exec" >> ,, p ,, h >> end define \\ 3427 3428 late eager define extend request ( r , s ) as << << 0 ,, "extend" >> ,, r ,, s >> end define 3429 3430 end array ]"\] 3431 3432 \noindent And the following input messages: 3433 3434 \["[ array ( left ) 3435 3436 late eager define boot event ( a , e , c , s ) as << << 0 ,, "boot" >> ,, a ,, e ,, c ,, s >> end define \\ 3437 3438 late eager define read reply ( c ) as << << 0 ,, "read" >> ,, c >> end define \\ 3439 3440 late eager define exec reply ( i , p ) as << << 0 ,, "exec" >> ,, i ,, p >> end define \\ 3441 3442 late eager define extend reply ( x ) as << << 0 ,, "extend" >> ,, x >> end define 3443 3444 end array ]"\] 3445 3446 \noindent Each exec reply contains an ``interrupt''. The following interrupts are predefined: 3447 3448 \["[ array ( left ) 3449 3450 late eager define exit interrupt as << << 0 ,, "exit" >> >> end define \\ 3451 3452 late eager define time interrupt as << << 0 ,, "time" >> >> end define \\ 3453 3454 late eager define memory interrupt as << << 0 ,, "memory" >> >> end define 3455 3456 end array ]"\] 3457 3458 3459 3460 \subsection{Machine invocation} 3461 3462 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. 3463 3464 3465 3466 \subsection{Input-eval-output-loop} 3467 3468 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: 3469 3470 A "[[ quit request ( x ) ]]" makes the machine exit immediately with return code "[[ x ]]". 3471 3472 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. 3473 3474 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. 3475 3476 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. 3477 3478 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 3479 3480 \["[ t = h apply << exec reply ( << i ,, a _ { 1 } ,, "\ldots" ,, a _ { m } >> , p ) ,, e _ { 1 } ,, "\ldots" ,, e _ { n } >> ]"\] 3481 3482 \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. 3483 3484 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. 3485 3486 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. 3487 3488 3489 3490 \subsection{Handlers and processes} 3491 3492 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. 3493 3494 3495 3496 \subsection{Character constants} 3497 3498 We now define a number of often used character constants. 3499 3500 \begin{statements} 3501 3502 \item "[[ late eager define NULL as bt2vector ( 0 ) end define ]]" 3503 3504 \item "[[ late eager define TAB as bt2vector ( 9 ) end define ]]" 3505 3506 \item "[[ late eager define LF as bt2vector ( 10 ) end define ]]" 3507 3508 \item "[[ late eager define FF as bt2vector ( 12 ) end define ]]" 3509 3510 \item "[[ late eager define CR as bt2vector ( 13 ) end define ]]" 3511 3512 \item "[[ late eager define SP as !" " end define ]]" 3513 3514 \item "[[ late eager define QQ as !""-""!" end define ]]" 3515 3516 \item "[[ late eager define V128 as bt2vector ( 128 ) end define ]]" 3517 3518 \item "[[ late eager define V255 as bt2vector ( 255 ) end define ]]" 3519 3520 \end{statements} 3521 3522 Some auxiliary definitions that use these constants read: 3523 3524 \begin{statements} 3525 3526 \item "[[ late eager define CRLF as CR :: LF end define ]]" 3527 3528 ASCII Carriage Return followed by Linefeed. 3529 3530 \item "[[ late eager define LFCR as LF :: CR end define ]]" 3531 3532 ASCII Linefeed followed by Carriage Return. 3533 3534 \item "[[ late eager define '' as vt2vector ( true ) end define ]]" 3535 3536 A convenience function for expressing the empty string. 3537 3538 \item "[[ late eager define writeln request ( x ) as write request ( x :: LF ) end define ]]" 3539 3540 \item "[[ late eager define println ( x ) as print ( x :: LF ) end define ]]" 3541 3542 \end{statements} 3543 3544 3545 3546 \subsection{Hello World} 3547 3548 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'. 3549 3550 3551 3552 \subsection{Echo} 3553 3554 A machine with "[[ Echo ]]" below as boot handler echos all characters typed except that it quits when the user types `q': 3555 3556 \begin{quote} 3557 3558 \noindent "[[ late eager define Echo as map ( \ x . Echo1 ( x ) ) end define ]]" 3559 3560 \noindent "[[ late eager define Echo1 ( x ) as newline 3561 3562 if x atom then newline 3563 3564 << read request ,, exec request ( true , Echo ) >> else newline 3565 3566 LET x head BE e IN newline 3567 3568 LET Echo1 ( x tail ) BE r IN newline 3569 3570 if .not. e head = << 0 ,, "read" >> then r else newline 3571 3572 if e first = "q" then << writeln request ( true ) ,, quit request ( 0 ) >> else 3573 3574 write request ( e first ) :: r end define ]]" 3575 3576 \end{quote} 3577 3578 3579 3580 \subsection{Eecho} 3581 3582 A machine with "[[ Eecho ]]" below as boot handler echos all characters typed twice except that it quits when the user types `q': 3583 3584 \begin{quote} 3585 3586 \noindent "[[ late eager define Eecho as map ( \ x . Eecho1 ( x ) ) end define ]]" 3587 3588 \noindent "[[ late eager define Eecho1 ( x ) as newline 3589 3590 if x atom then newline 3591 3592 << read request ,, exec request ( true , Eecho ) >> else newline 3593 3594 LET x head BE e IN newline 3595 3596 LET Eecho1 ( x tail ) BE r IN newline 3597 3598 if .not. e head = << 0 ,, "read" >> then r else newline 3599 3600 if e first = "q" then << writeln request ( true ) ,, quit request ( 0 ) >> else 3601 3602 write request ( e first :: e first ) :: r end define ]]" 3603 3604 \end{quote} 3605 3606 3607 3608 \subsection{Execution constructs}\label{Sec:ExecutionConstructs} 3609 3610 A definition like "[[ execute define "eecho" as << Eecho >> end define ]]" makes the Logiweb compiler generate a machine named "[[ !"eecho" ]]" whose handler is "[[ Eecho ]]". 3611 3612 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. 3613 3614 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. 3615 3616 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. 3617 3618 Each machine defined on a page needs its own definition: 3619 3620 \begin{statements} 3621 3622 \item "[[ execute define "hello" as << Hello World >> end define ]]" 3623 3624 \item "[[ execute define "echo" as << Echo >> end define ]]" 3625 3626 \item "[[ execute define "lgciotest" as << lgcio1 >> end define ]]" 3627 3628 \end{statements} 3629 3630 3631 3632 " ]"\section{The lgcio interface}"[ " 3633 3634 The lgcio interface provides all the input/output facilities needed by the lgc compiler. These features are: 3635 3636 \begin{description} 3637 3638 \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). 3639 3640 \item[FileWriteExec] Same as above, but using mode 0777 instead of mode 0666. Hence, created files become executable. 3641 3642 \item[FileRead] Read all contents of a given file. 3643 3644 \item[FileRm] Remove given file. If the file does not exist, do nothing. 3645 3646 \item[FileSymlink] Create symbolic link. 3647 3648 \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. 3649 3650 \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/. 3651 3652 \item[FileRmdir] Remove given, empty directory. If the directory does not exist, do nothing. 3653 3654 \item[FileDir] Read all entries of given directory. 3655 3656 \item[FileType] Read the type of the given file (regular, directory, symbolic link, non-existent, or other). 3657 3658 \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). 3659 3660 \item[TextWrite] Same as FileWrite, but changes newline sequences to given sequence. 3661 3662 \item[TextWriteExec] Same as FileWriteExec, but changes newline sequences to given sequence. 3663 3664 \item[FileGetCwd] Return current working directory. 3665 3666 \item[UnixTime] Read the clock. 3667 3668 \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. 3669 3670 \item[Execlp1] In a given directory, run a given command with one argument. The search path is used to locate the command. 3671 3672 \item[TcpQuery] Send given bytes to given port of given domain. 3673 3674 \end{description} 3675 3676 3677 3678 \subsection{The lgcio request} 3679 3680 The "[[ lgcio ( c ) ]]" request carries communication between the computing engine and the lgcio interface. 3681 3682 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. 3683 3684 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. 3685 3686 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. 3687 3688 We define "[[ lgcio ( c ) ]]" such that "[[ quote lgcio ( c ) end quote t= lgcio ( quote c end quote ) ]]": 3689 3690 "[[[ late eager define lgcio ( c ) as << quote lgcio ( c ) end quote head ,, c >> end define ]]]" 3691 3692 3693 3694 \subsection{Constants used by the lgcio interface} 3695 3696 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. 3697 3698 \begin{statements} 3699 3700 \item "[[ late eager define EOS as bt2vector ( 0 ) end define ]]" 3701 3702 \item "[[ late eager define FileWrite as bt2vector ( 1 ) end define ]]" 3703 3704 \item "[[ late eager define FileWriteExec as bt2vector ( 2 ) end define ]]" 3705 3706 \item "[[ late eager define FileRead as bt2vector ( 3 ) end define ]]" 3707 3708 \item "[[ late eager define FileRm as bt2vector ( 4 ) end define ]]" 3709 3710 \item "[[ late eager define FileSymlink as bt2vector ( 5 ) end define ]]" 3711 3712 \item "[[ late eager define FileReadLink as bt2vector ( 6 ) end define ]]" 3713 3714 \item "[[ late eager define FileMkdir as bt2vector ( 7 ) end define ]]" 3715 3716 \item "[[ late eager define FileRmdir as bt2vector ( 8 ) end define ]]" 3717 3718 \item "[[ late eager define FileDir as bt2vector ( 9 ) end define ]]" 3719 3720 \item "[[ late eager define FileType as bt2vector ( 10 ) end define ]]" 3721 3722 \item "[[ late eager define FileTypeRead as bt2vector ( 11 ) end define ]]" 3723 3724 \item "[[ late eager define TextWrite as bt2vector ( 12 ) end define ]]" 3725 3726 \item "[[ late eager define TextWriteExec as bt2vector ( 13 ) end define ]]" 3727 3728 \item "[[ late eager define FileGetCwd as bt2vector ( 14 ) end define ]]" 3729 3730 \item "[[ late eager define UnixTime as bt2vector ( 20 ) end define ]]" 3731 3732 \item "[[ late eager define Demonize as bt2vector ( 30 ) end define ]]" 3733 3734 \item "[[ late eager define Execlp1 as bt2vector ( 31 ) end define ]]" 3735 3736 \item "[[ late eager define TcpQuery as bt2vector ( 40 ) end define ]]" 3737 3738 \end{statements} 3739 3740 The reply from a FileType request represents the type of the queried file thus: 3741 3742 \begin{statements} 3743 3744 \item "[[ late eager define FileTypeNonexistent as bt2vector ( 0 ) end define ]]" 3745 3746 \item "[[ late eager define FileTypeOther as bt2vector ( 1 ) end define ]]" 3747 3748 \item "[[ late eager define FileTypeRegular as bt2vector ( 2 ) end define ]]" 3749 3750 \item "[[ late eager define FileTypeDirectory as bt2vector ( 3 ) end define ]]" 3751 3752 \item "[[ late eager define FileTypeLink as bt2vector ( 4 ) end define ]]" 3753 3754 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). 3755 3756 \end{statements} 3757 3758 3759 3760 \subsection{Data conversion} 3761 3762 The following functions allow to construct arguments of request and analyse arguments of replies. 3763 3764 \begin{statements} 3765 3766 \item "[[ late eager define septet*2card ( r , s ) as newline 3767 3768 if s atom then r else septet*2card ( s head + septet-base * r , s tail ) end define ]]" 3769 3770 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 ]]" 3771 3772 \item "[[ late eager define septet-base as 128 end define ]]" 3773 3774 \item "[[ late eager define parse-card ( v ) as parse-card1 ( true , v ) end define ]]" 3775 3776 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. 3777 3778 \item "[[ late eager define parse-card1 ( r , v ) as newline 3779 3780 if v atom then exception else newline 3781 3782 let b :: v = v in newline 3783 3784 if b < NULL .or. b > V255 then exception else newline 3785 3786 if b < V128 then septet*2card ( 0 , b - NULL :: r ) :: v else newline 3787 3788 parse-card1 ( b - V128 :: r , v ) end define ]]" 3789 3790 \item "[[ late eager define exp10 ( e ) as if e = 0 then 1 else 10 * exp10 ( e - 1 ) end define ]]" 3791 3792 Raise 10 to power "[[ e ]]". 3793 3794 \item "[[ late eager define parse-unixTime ( v ) as newline 3795 3796 let f :: v = parse-card ( v first ) in newline 3797 3798 let s :: v = parse-card ( v ) in newline 3799 3800 let e :: v = parse-card ( v ) in newline 3801 3802 << s * exp10 ( e ) + f ,, e >> end define ]]" 3803 3804 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 } $. 3805 3806 \item "[[ late eager define make-card ( c ) as newline 3807 3808 if c < 128 then bt2vector ( c ) else newline 3809 3810 bt2vector ( ( c mod 128 ) + 128 ) :: make-card ( c div 128 ) end define ]]" 3811 3812 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. 3813 3814 \end{statements} 3815 3816 3817 3818 \subsection{Individual lgcio requests} 3819 3820 Constructors for the individual commands understood by the lgcio interface are defined in the following. 3821 3822 \begin{statements} 3823 3824 \item "[[ late eager define fileWrite ( p , c ) as lgcio ( FileWrite :: p :: EOS :: c ) end define ]]" 3825 3826 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. 3827 3828 \item "[[ late eager define fileWriteExec ( p , c ) as lgcio ( FileWriteExec :: p :: EOS :: c ) end define ]]" 3829 3830 Same as "[[ fileWrite ( p , c ) ]]" but uses file permissions 777 (read, write, and execute). 3831 3832 \item "[[ late eager define fileRead ( p ) as lgcio ( FileRead :: p :: EOS ) end define ]]" 3833 3834 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. 3835 3836 \item "[[ late eager define fileRm ( p ) as lgcio ( FileRm :: p :: EOS ) end define ]]" 3837 3838 Remove the file or symbolic link with pathname "[[ p ]]". The reply has form "[[ lgcio ( <<>> ) ]]". 3839 3840 \item "[[ late eager define fileSymlink ( p , l ) as lgcio ( FileSymlink :: p :: EOS :: l :: EOS ) end define ]]" 3841 3842 Create a symbolic link at pathname "[[ l ]]" which points to pathname "[[ p ]]". The reply has form "[[ lgcio ( <<>> ) ]]". 3843 3844 \item "[[ late eager define fileReadLink ( l ) as lgcio ( FileReadLink :: l :: EOS ) end define ]]" 3845 3846 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. 3847 3848 \item "[[ late eager define fileMkdir ( p ) as lgcio ( FileMkdir :: p :: EOS ) end define ]]" 3849 3850 Create a directory with pathname "[[ p ]]". The reply has form "[[ lgcio ( <<>> ) ]]". 3851 3852 \item "[[ late eager define fileRmdir ( p ) as lgcio ( FileRmdir :: p :: EOS ) end define ]]" 3853 3854 Remove the directory with pathname "[[ p ]]". The directory must be empty. The reply has form "[[ lgcio ( <<>> ) ]]". 3855 3856 \item "[[ late eager define fileDir ( p ) as lgcio ( FileDir :: p :: EOS ) end define ]]" 3857 3858 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 ``..''. 3859 3860 \item "[[ late eager define fileType ( p ) as lgcio ( FileType :: p :: EOS ) end define ]]" 3861 3862 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: 3863 3864 \begin{description} 3865 \item["[[ FileTypeNonexistent ]]"] File does not exist 3866 \item["[[ FileTypeRegular ]]"] File is regular 3867 \item["[[ FileTypeDirectory ]]"] File is directory 3868 \item["[[ FileTypeLink ]]"] File is link 3869 \item["[[ FileTypeOther ]]"] Otherwise 3870 \end{description} 3871 3872 \item "[[ late eager define fileTypeRead ( p ) as lgcio ( FileTypeRead :: p :: EOS ) end define ]]" 3873 3874 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. 3875 3876 \item "[[ late eager define textWrite ( p , n , c ) as lgcio ( TextWrite :: p :: EOS :: n :: EOS :: c ) end define ]]" 3877 3878 Same as "[[ fileWrite ( p , c ) ]]" but changes newline sequences in "[[ c ]]" to "[[ n ]]". 3879 3880 \item "[[ late eager define textWriteExec ( p , n , c ) as lgcio ( TextWriteExec :: p :: EOS :: n :: EOS :: c ) end define ]]" 3881 3882 \item "[[ late eager define fileGetCwd as lgcio ( FileGetCwd ) end define ]]" 3883 3884 Same as "[[ fileWriteExec ( p , c ) ]]" but changes newline sequences in "[[ c ]]" to "[[ n ]]". 3885 3886 \item "[[ late eager define unixTime as lgcio ( UnixTime ) end define ]]" 3887 3888 Return the number of seconds since the Unix epoch. Ignore leap seconds in the sense that the count stops during leap seconds. 3889 3890 \item "[[ late eager define demonize ( l , p , u ) as lgcio ( Demonize :: l :: EOS :: p :: EOS :: u :: EOS ) end define ]]" 3891 3892 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. 3893 3894 \item "[[ late eager define execlp1 ( d , p , a ) as lgcio ( Execlp1 :: d :: EOS :: p :: EOS :: a :: EOS ) end define ]]" 3895 3896 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. 3897 3898 \item "[[ late eager define tcpQuery ( d , p , m , e , q ) as newline 3899 3900 LET floor ( m , exp10 ( e ) ) BE v IN newline 3901 3902 lgcio ( TcpQuery :: d :: EOS :: make-card ( p ) :: make-card ( v head ) :: newline 3903 3904 make-card ( v tail ) :: make-card ( e ) :: q ) end define ]]" 3905 3906 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 ( <<>> ) ]]". 3907 3908 \end{statements} 3909 3910 3911 3912 \subsection{The lgcio interface definition} 3913 3914 "[ verbatim define lgcio-interface as " 3915 /* 3916 The lgcio interface provides all the input/output facilities 3917 needed by the Logiweb lgc compiler. 3918 */ 3919 3920 #includeContents: 6434 Main text 6435 Appendix 6436 Chores 6437
6438 The 6439 Logiweb compiler 6440 6441 " ) ,, 6442 6443 tex-file ( "text" , "page.bib" , b ) ,, 6444 6445 tex-file ( "text" , "page.tex" , ""-""; 6446 \documentclass[fleqn]{article} 6447 % Include definitions generated by the Logiweb compiler 6448 \input{lgwinclude} 6449 % Make latexsym characters available 6450 \usepackage{latexsym} 6451 % Ensure reasonable rendering of strings 6452 \everymath{\rm} 6453 \everydisplay{\rm} 6454 % Enable generation of an index 6455 \usepackage{makeidx} 6456 \makeindex 6457 \newcommand{\intro}[1]{\emph{#1}} 6458 \newcommand{\indexintro}[1]{\index{#1}\intro{#1}} 6459 % Enable generation of a bibliography 6460 \bibliographystyle{plain} 6461 % Enable hyperlinks 6462 \usepackage[dvipdfm=true]{hyperref} 6463 \hypersetup{pdfpagemode=UseNone} 6464 \hypersetup{pdfstartpage=1} 6465 \hypersetup{pdfstartview=FitBH} 6466 \hypersetup{pdfpagescrop={120 80 490 730}} 6467 \hypersetup{pdftitle="[ t ]"} 6468 \hypersetup{colorlinks=true} 6469 % Construct for listing statements with associated explanations 6470 \newenvironment{statements}{\begin{list}{}{ 6471 \setlength{\leftmargin}{5em} 6472 \setlength{\itemindent}{-5em}}}{\end{list}} 6473 \begin{document} 6474 "[ m ]" 6475 \end{document} 6476 " ) ,, 6477 tex-command ( "latex" , "page" ) ,, 6478 tex-command ( "bibtex" , "page" ) ,, 6479 tex-command ( "makeindex" , "page" ) ,, 6480 tex-command ( "latex" , "page" ) ,, 6481 tex-command ( "latex" , "page" ) ,, 6482 tex-command ( "dvipdfm" , "page" ) ,, 6483 6484 tex-file ( "text" , "appendix.tex" , ""-""; 6485 \documentclass[fleqn]{article} 6486 % Include definitions generated by the Logiweb compiler 6487 \input{lgwinclude} 6488 % Make latexsym characters available 6489 \usepackage{latexsym} 6490 % Ensure reasonable rendering of strings 6491 \everymath{\rm} 6492 \everydisplay{\rm} 6493 % Enable generation of an index 6494 \usepackage{makeidx} 6495 \makeindex 6496 \newcommand{\intro}[1]{\emph{#1}} 6497 \newcommand{\indexintro}[1]{\index{#1}\intro{#1}} 6498 % Enable generation of a bibliography 6499 \bibliographystyle{plain} 6500 % Enable hyperlinks 6501 \usepackage[dvipdfm=true]{hyperref} 6502 \hypersetup{pdfpagemode=UseNone} 6503 \hypersetup{pdfstartpage=1} 6504 \hypersetup{pdfstartview=FitBH} 6505 \hypersetup{pdfpagescrop={120 80 490 730}} 6506 \hypersetup{pdftitle="[ t ]" - appendix} 6507 \hypersetup{colorlinks=true} 6508 % Construct for listing statements with associated explanations 6509 \newenvironment{statements}{\begin{list}{}{ 6510 \setlength{\leftmargin}{5em} 6511 \setlength{\itemindent}{-5em}}}{\end{list}} 6512 \begin{document} 6513 "[ a ]" 6514 \end{document} 6515 " ) ,, 6516 tex-command ( "latex" , "appendix" ) ,, 6517 tex-command ( "latex" , "appendix" ) ,, 6518 tex-command ( "latex" , "appendix" ) ,, 6519 tex-command ( "dvipdfm" , "appendix" ) ,, 6520 6521 tex-file ( "text" , "chores.tex" , ""-""; 6522 \documentclass[fleqn]{article} 6523 % Include definitions generated by the Logiweb compiler 6524 \input{lgwinclude} 6525 % Make latexsym characters available 6526 \usepackage{latexsym} 6527 % Ensure reasonable rendering of strings 6528 \everymath{\rm} 6529 \everydisplay{\rm} 6530 % Enable generation of an index 6531 \usepackage{makeidx} 6532 \makeindex 6533 \newcommand{\intro}[1]{\emph{#1}} 6534 \newcommand{\indexintro}[1]{\index{#1}\intro{#1}} 6535 % Enable generation of a bibliography 6536 \bibliographystyle{plain} 6537 % Enable hyperlinks 6538 \usepackage[dvipdfm=true]{hyperref} 6539 \hypersetup{pdfpagemode=UseNone} 6540 \hypersetup{pdfstartpage=1} 6541 \hypersetup{pdfstartview=FitBH} 6542 \hypersetup{pdfpagescrop={120 80 490 730}} 6543 \hypersetup{pdftitle="[ t ]" - chores} 6544 \hypersetup{colorlinks=true} 6545 % Construct for listing statements with associated explanations 6546 \newenvironment{statements}{\begin{list}{}{ 6547 \setlength{\leftmargin}{5em} 6548 \setlength{\itemindent}{-5em}}}{\end{list}} 6549 \begin{document} 6550 \title{"[ t ]"} 6551 \author{The \href{http://logiweb.eu/}{Logiweb} compiler} 6552 \maketitle 6553 \tableofcontents 6554 \section{Name definitions} 6555 \begin{flushleft} 6556 $ "[ x ]" $ 6557 \end{flushleft} 6558 \section{Charge definitions} 6559 \begin {flushleft} 6560 $ "[ y ]" $ 6561 \end {flushleft} 6562 \end{document} 6563 " ) ,, 6564 tex-command ( "latex" , "chores" ) ,, 6565 tex-command ( "latex" , "chores" ) ,, 6566 tex-command ( "latex" , "chores" ) ,, 6567 tex-command ( "dvipdfm" , "chores" ) 6568 6569 end define ]]" 6570 6571 6572 6573 \item "[[ tex show define -x as " 6574 {}^{-}\! ",x end define ]]" 6575 6576 \item "[[ tex show define +x as " 6577 {}^{+}\! ",x end define ]]" 6578 6579 \item "[[ tex use define tight newline x as " 6580 \newline "[ x ]"". end define ]]" 6581 6582 6583 6584 \item "[[ tex show define x factorial as "".[ x ]" 6585 !" end define ]]" 6586 6587 \item "[[ tex use define x _ { y } as "".[ x ]" 6588 _{"[ y ]" 6589 }" end define ]]" 6590 6591 \item "[[ tex use define x_y as "".[ x ]" 6592 _{"[ y ]" 6593 }" end define ]]" 6594 6595 \item "[[ tex use define x prime as "".[ x ]" 6596 {}' " end define ]]" 6597 6598 \item "[[ tex show define x %0 as "".[ x ]"0" end define ]]" 6599 6600 \item "[[ tex show define x %1 as "".[ x ]"1" end define ]]" 6601 6602 \item "[[ tex show define x %2 as "".[ x ]"2" end define ]]" 6603 6604 \item "[[ tex show define x %3 as "".[ x ]"3" end define ]]" 6605 6606 \item "[[ tex show define x %4 as "".[ x ]"4" end define ]]" 6607 6608 \item "[[ tex show define x %5 as "".[ x ]"5" end define ]]" 6609 6610 \item "[[ tex show define x %6 as "".[ x ]"6" end define ]]" 6611 6612 \item "[[ tex show define x %7 as "".[ x ]"7" end define ]]" 6613 6614 \item "[[ tex show define x %8 as "".[ x ]"8" end define ]]" 6615 6616 \item "[[ tex show define x %9 as "".[ x ]"9" end define ]]" 6617 6618 \item "[[ tex show define x head as "".[ x ]" 6619 {}^h" end define ]]" 6620 6621 \item "[[ tex show define x tail as "".[ x ]" 6622 {}^t" end define ]]" 6623 6624 \item "[[ tex show define x raise as "".[ x ]" 6625 {}^{\bullet}" end define ]]" 6626 6627 \item "[[ tex show define x catch as "".[ x ]" 6628 {}^{\circ}" end define ]]" 6629 6630 \item "[[ tex show define x catching maptag as "".[ x ]" 6631 {}^{M^{\circ}}" end define ]]" 6632 6633 \item "[[ tex show define x maptag as "".[ x ]" 6634 {}^M" end define ]]" 6635 6636 \item "[[ tex show define x untag as "".[ x ]" 6637 {}^U" end define ]]" 6638 6639 \item "[[ tex show define x root as "".[ x ]" 6640 {}^R" end define ]]" 6641 6642 \item "[[ tex show define x norm as "".[ x ]" 6643 {}^N" end define ]]" 6644 6645 \item "[[ tex show define x boolp as "".[ x ]" 6646 \in \mathbf{B}" end define ]]" 6647 6648 \item "[[ tex show define x truep as "".[ x ]" 6649 \in \mathbf{T}" end define ]]" 6650 6651 \item "[[ tex show define x falsep as "".[ x ]" 6652 \in \mathbf{F}" end define ]]" 6653 6654 \item "[[ tex show define x intp as "".[ x ]" 6655 \in \mathbf{Z}" end define ]]" 6656 6657 \item "[[ tex show define x pairp as "".[ x ]" 6658 \in \mathbf{P}" end define ]]" 6659 6660 \item "[[ tex show define x atom as "".[ x ]" 6661 \in \mathbf{A}" end define ]]" 6662 6663 \item "[[ tex show define x mapp as "".[ x ]" 6664 \in \mathbf{M}" end define ]]" 6665 6666 \item "[[ tex show define x objectp as "".[ x ]" 6667 \in \mathbf{O}" end define ]]" 6668 6669 \item "[[ tex show define x zeroth as "".[ x ]" 6670 {}^0" end define ]]" 6671 6672 \item "[[ tex show define x first as "".[ x ]" 6673 {}^1" end define ]]" 6674 6675 \item "[[ tex show define x second as "".[ x ]" 6676 {}^2" end define ]]" 6677 6678 \item "[[ tex show define x third as "".[ x ]" 6679 {}^3" end define ]]" 6680 6681 \item "[[ tex show define x fourth as "".[ x ]" 6682 {}^4" end define ]]" 6683 6684 \item "[[ tex show define x fifth as "".[ x ]" 6685 {}^5" end define ]]" 6686 6687 \item "[[ tex show define x sixth as "".[ x ]" 6688 {}^6" end define ]]" 6689 6690 \item "[[ tex show define x seventh as "".[ x ]" 6691 {}^7" end define ]]" 6692 6693 \item "[[ tex show define x eighth as "".[ x ]" 6694 {}^8" end define ]]" 6695 6696 \item "[[ tex show define x ninth as "".[ x ]" 6697 {}^9" end define ]]" 6698 6699 \item "[[ tex show define x ref as "".[ x ]" 6700 {}^r" end define ]]" 6701 6702 \item "[[ tex show define x idx as "".[ x ]" 6703 {}^i" end define ]]" 6704 6705 \item "[[ tex show define x debug as "".[ x ]" 6706 {}^d" end define ]]" 6707 6708 \item "[[ tex show define a [[ i ]] as "".[ a ]" 6709 \linebreak[0][ "[ i ]" 6710 ]" end define ]]" 6711 6712 \item "[[ tex show define a [[ i -> v ]] as "".[ a ]" 6713 \linebreak[0][ "[ i ]" 6714 {\rightarrow} "[ v ]" 6715 ]" end define ]]" 6716 6717 \item "[[ tex show define a [[ i => v ]] as "".[ a ]" 6718 \linebreak[0][ "[ i ]" 6719 {\Rightarrow} "[ v ]" 6720 ]" end define ]]" 6721 6722 \item "[[ tex use define x tight endline as "".[ x ]" 6723 \newline " end define ]]" 6724 6725 \item "[[ tex use define x unquote as " 6726 \underline{ "[ x ]" 6727 } " end define ]]" 6728 6729 6730 6731 \item "[[ tex use define newline x as " 6732 \newline "[ x ]"". end define ]]" 6733 6734 6735 6736 \item "[[ tex show define x ' y as "".[ x ]" 6737 \mathbin {\mbox {'}}"[ y ]"". end define ]]" 6738 6739 \item "[[ tex show define x apply y as "".[ x ]" 6740 \mathbin {\mbox {''}}"[ y ]"". end define ]]" 6741 6742 \item "[[ tex show define texshow x end texshow as " 6743 \underline{ "[ x ]" 6744 }" end define ]]" 6745 6746 6747 6748 \item "[[ tex show define - x as " 6749 {-} "[ x ]"". end define ]]" 6750 6751 \item "[[ tex show define + x as " 6752 {+} "[ x ]"". end define ]]" 6753 6754 6755 6756 \item "[[ tex show define x * y as "".[ x ]" 6757 \cdot "[ y ]"". end define ]]" 6758 6759 6760 6761 \item "[[ tex show define x + y as "".[ x ]" 6762 + "[ y ]"". end define ]]" 6763 6764 \item "[[ tex show define x - y as "".[ x ]" 6765 - "[ y ]"". end define ]]" 6766 6767 6768 6769 6770 6771 \item "[[ tex show define x :: y as "".[ x ]" 6772 \mathop{:\,:} "[ y ]"". end define ]]" 6773 6774 6775 6776 \item "[[ tex show define x ,, y as "".[ x ]" 6777 , "[ y ]"". end define ]]" 6778 6779 6780 6781 \item "[[ tex show define x = y as "".[ x ]" 6782 = "[ y ]"". end define ]]" 6783 6784 \item "[[ tex show define x != y as "".[ x ]" 6785 \neq "[ y ]"". end define ]]" 6786 6787 \item "[[ tex show define x < y as "".[ x ]" 6788 < "[ y ]"". end define ]]" 6789 6790 \item "[[ tex show define x > y as "".[ x ]" 6791 > "[ y ]"". end define ]]" 6792 6793 \item "[[ tex show define x <= y as "".[ x ]" 6794 \le "[ y ]"". end define ]]" 6795 6796 \item "[[ tex show define x >= y as "".[ x ]" 6797 \ge "[ y ]"". end define ]]" 6798 6799 \item "[[ tex show define x r= y as "".[ x ]" 6800 \stackrel{r}{=} "[ y ]"". end define ]]" 6801 6802 \item "[[ tex show define x t= y as "".[ x ]" 6803 \stackrel{t}{=} "[ y ]"". end define ]]" 6804 6805 \item "[[ tex show define x t=* y as "".[ x ]" 6806 \stackrel{t^*}{=} "[ y ]"". end define ]]" 6807 6808 6809 6810 \item "[[ tex show define .not. x as " 6811 {\bf not} \ \linebreak [0]"[ x ]"". end define ]]" 6812 6813 6814 6815 \item "[[ tex show define x .and. y as "".[ x ]" 6816 \ {\bf and} \ \linebreak [0]"[ y ]"". end define ]]" 6817 6818 \item "[[ tex show define x .prog1. y as "".[ x ]" 6819 \ {\bf prog1} \ \linebreak [0]"[ y ]"". end define ]]" 6820 6821 \item "[[ tex show define x &c y as "".[ x ]" 6822 \wedge_c "[ y ]"". end define ]]" 6823 6824 6825 6826 \item "[[ tex show define x .or. y as "".[ x ]" 6827 \ {\bf or} \ \linebreak [0]"[ y ]"". end define ]]" 6828 6829 6830 6831 \item "[[ tex show define x is val : y as "".[ x ]" 6832 {\in} \mathbf{V} \colon "[ y ]"". end define ]]" 6833 6834 \item "[[ tex show define x is bool : y as "".[ x ]" 6835 {\in} \mathbf{B} \colon "[ y ]"". end define ]]" 6836 6837 \item "[[ tex show define x is int : y as "".[ x ]" 6838 {\in} \mathbf{Z} \colon "[ y ]"". end define ]]" 6839 6840 \item "[[ tex show define x is pair : y as "".[ x ]" 6841 {\in} \mathbf{P} \colon "[ y ]"". end define ]]" 6842 6843 \item "[[ tex show define x is map : y as "".[ x ]" 6844 {\in} \mathbf{M} \colon "[ y ]"". end define ]]" 6845 6846 \item "[[ tex show define x is object : y as "".[ x ]" 6847 {\in} \mathbf{O} \colon "[ y ]"". end define ]]" 6848 6849 6850 6851 \item "[[ tex show define x Select y else z end select as 6852 "".[ x ]" 6853 \left\langle\protect \begin {array}{l}"[ y ]" 6854 \\"[ z ]" 6855 \protect \end {array}\right." end define ]]" 6856 6857 \item "[[ tex show define x IN y as "".[ x ]" 6858 \ \mathbf{in}\ \linebreak [0] "[ y ]"". end define ]]" 6859 6860 6861 6862 \item "[[ tex show define \ x . y as " 6863 \lambda "[ x ]" 6864 ."[ y ]"". end define ]]" 6865 6866 \item "[[ tex show define If x then y else z as " 6867 {\bf If} \ \linebreak [0]"[ x ]" 6868 \ {\bf then} \ \linebreak [0]"[ y ]" 6869 \ {\bf else} \ \linebreak [0]"[ z ]"". end define ]]" 6870 6871 \item "[[ tex show define if x then y else z as " 6872 {\bf if} \ \linebreak [0]"[ x ]" 6873 \ {\bf then} \ \linebreak [0]"[ y ]" 6874 \ {\bf else} \ \linebreak [0]"[ z ]"". end define ]]" 6875 6876 \item "[[ tex show define LET x BE y as " 6877 {\bf let} \ \linebreak [0]"[ x ]" 6878 \ {\bf be} \ \linebreak [0]"[ y ]"". end define ]]" 6879 6880 \item "[[ tex show define let x := y in z as " 6881 {\bf let} \ \linebreak [0]"[ x ]" 6882 \mathrel{\ddot{=}} "[ y ]" 6883 \ {\bf in} \ \linebreak [0]"[ z ]"". end define ]]" 6884 6885 \item "[[ tex show define let x = y in z as " 6886 {\bf let} \ \linebreak [0]"[ x ]" 6887 = "[ y ]" 6888 \ {\bf in} \ \linebreak [0]"[ z ]"". end define ]]" 6889 6890 \item "[[ tex show define ttst x end test as " 6891 [ "[ x ]" 6892 ]^{\cdot}" end define ]]" 6893 6894 \item "[[ tex show define ftst x end test as " 6895 [ "[ x ]" 6896 ]^{-}" end define ]]" 6897 6898 \item "[[ tex show define etst x ; y end test as " 6899 [ "[ x ]" 6900 = "[ y ]" 6901 ]^{=}" end define ]]" 6902 6903 \item "[[ tex show define x reduce to y as "".[ x ]" 6904 \stackrel {+}{\rightarrow }"[ y ]"". end define ]]" 6905 6906 \item "[[ tex show define x == y as "".[ x ]" 6907 \equiv "[ y ]"". end define ]]" 6908 6909 6910 6911 \item "[[ tex use define x lgcthen y as x," 6912 \newline ",y end define ]]" 6913 6914 \item "[[ tex use define x,y as "".[ x ]"".[ y ]"". end define ]]" 6915 6916 \item "[[ tex use define x[ y ]z as "".[ x ]"".[ y ]"".[ z ]"". end define ]]" 6917 6918 \item "[[ tex use define x[[ y ]]z as "".[ x ]"$"[ y ]"$"[ z ]"". end define ]]" 6919 6920 \item "[[ tex show define x[[ y ]]z as "".[ x ]" 6921 {\$}"[ y ]" 6922 {\$}"[ z ]"". end define ]]" 6923 6924 \item "[[ tex use define x[[[ y ]]]z as "".[ x ]"\["[ y ]"\]"[ z ]"". end define ]]" 6925 6926 \item "[[ tex show define x[[[ y ]]]z as "".[ x ]" 6927 {\backslash[}"[ y ]" 6928 {\backslash]}"[ z ]"". end define ]]" 6929 6930 6931 6932 \item "[[ tex use define x endline as "".[ x ]" 6933 \newline " end define ]]" 6934 6935 6936 6937 \item "[[ tex use define x linebreak y as "".[ x ]" 6938 \linebreak[4] "[ y ]"". end define ]]" 6939 6940 6941 6942 \item "[[ tex use define x & y as "".[ x ]" 6943 & "[ y ]"". end define ]]" 6944 6945 6946 6947 \item "[[ tex use define x \\ y as "".[ x ]" 6948 \\{}"[ y ]"". end define ]]" 6949 6950 \end{statements} 6951 6952 6953 6954 \section{Name definitions} 6955 6956 "[[ protect ""N end protect ]]" 6957 6958 6959 6960 \section{Charge definitions} 6961 6962 "[[ protect ""C end protect ]]" 6963 6964 6965 6966 \end{document} 6967 " end text ,, 6968 6969 6970 6971 latex ( "chores" ) ,, 6972 latex ( "chores" ) ,, 6973 dvipdfm ( "chores" ) 6974 6975 6976 6977 6978