[Axiom-developer] 20080619.03.tpd.patch (add Ralf Hemmecke documentation to ax.boot)

[daly]

Add Ralf Hemmecke documentation to ax.boot.
=========================================================================
diff --git a/changelog b/changelog
index 5c6a0b8..47c791c 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,4 @@
+20080619 rhx src/interp/ax.boot document makeAxExportForm
 20080619 tpd books/bookvol8 systematically index chunks
 20080619 tpd readme add Anatoly Raportirenko
 20080619 tpd src/interp/setq.lisp add Anatoly Raportirenko
diff --git a/src/interp/ax.boot.pamphlet b/src/interp/ax.boot.pamphlet
index 2234b1e..19a8ba8 100644
--- a/src/interp/ax.boot.pamphlet
+++ b/src/interp/ax.boot.pamphlet
@@ -1,10 +1,13 @@
 \documentclass{article}
 \usepackage{axiom}
+\newcommand{\file}[1]{\texttt{#1}}
 \begin{document}
 \title{\$SPAD/src/interp ax.boot}
-\author{The Axiom Team}
+\author{Ralf Hemmecke}
 \maketitle
 \begin{abstract}
+We give an overview of what \file{ax.boot} does and in particular
+describe the function \verb'makeAxExportForm'.
 \end{abstract}
 \eject
 \tableofcontents
@@ -21,7 +24,29 @@ but was changed to read:
   axForm := ['Sequence, _
                ['Import, [], 'AxiomLib], ['Import, [], 'Boolean], :axForms]
 @
+\section{Overview}
 \subsection{makeAxExportForm}
+The most important function in \file{ax.boot} is the function
+\verb'makeAxExportForm'.
+
+The function takes as input a filename and a list of constructors.
+Via LISP it would be called like
+\begin{verbatim}
+(|makeAxExportForm| filename constructors)
+\end{verbatim}
+where \verb'filename' is actually unused and could be removed and
+\verb'constructors' should be a list of constructor names, i.e., names
+of categories, domains, and packages in their unabbreviated form.
+
+It returns a list that represents the \texttt{.ap} (parsed source)
+(see \verb'aldor -hall') form of the constructors. However, since the
+output is only needed for a construction of an Aldor-Axiom
+interaction, \verb'makeAxExportForm' will only construct the category
+part of the constructor.
+
+The function is actually used in \file{src/aldor/genax.lsp} and is an
+auxiliary part in the construction of the interface for the
+interaction of the Aldor compiler with Axiom.
 <<makeAxExportForm>>=
 makeAxExportForm(filename, constructors) ==
   $defaultFlag : local := false
@@ -42,7 +67,417 @@ makeAxExportForm(filename, constructors) ==
   axForm
 
 @
-\subsection{axFormatPref}
+The basic translation is easily demonstrated with a few examples. For
+better readability, we look at the corresponding SPAD form of the
+constructor (instead of its internal LISP representation).
+
+Let us first state what different situations we identified.
+\begin{enumerate}
+\item Ordinary domains. See Section~\ref{sec:Domain}.
+\item Ordinary categories. See Section~\ref{sec:Category}.
+\item Ordinary categories with default packages. See
+  Section~\ref{sec:Category+Default}.
+\item Initial domains, i.e., domains that will be extended in the
+  course of building \file{libaxiom.al}. These domains are listed in
+  the variable \verb'$extendedDomains'. %$
+
+  See Sections~\ref{sec:InitDomain} and
+  \ref{sec:ParametrizedInitDomain}. There is a subdivision for these
+  domains.
+  \begin{enumerate}
+  \item For domains that take no arguments, see
+    Section~\ref{sec:InitDomain}.
+  \item For domains that take arguments, see
+    Section~\ref{sec:ParametrizedInitDomain}.
+  \end{enumerate}
+\end{enumerate}
+\section{Ordinary Domains}\label{sec:Domain}
+The domain \verb'Stack'.
+\begin{verbatim}
+Stack(S:SetCategory): StackAggregate S with
+    stack: List S -> %
+  == add
+    Rep := Reference List S
+    ...
+\end{verbatim}
+It is translated into \ldots
+\begin{verbatim}
+(|Sequence| (|Import| NIL |AxiomLib|) (|Import| NIL |Boolean|)
+    (|Export|
+        (|Declare| |Stack|
+            (|Apply| -> (|Declare| |#1| |SetCategory|)
+                     (|With| NIL
+                             (|Sequence|
+                                 (|Apply| |StackAggregate| |#1|)
+                                 (|Declare| |stack|
+                                     (|Apply| ->
+                                      (|Comma| (|Apply| |List| |#1|))
+                                      %))))))
+        NIL NIL))
+\end{verbatim}
+That is the parsed source of the Aldor code \ldots
+\begin{verbatim}
+import from AxiomLib;
+import from Boolean;
+export Stack: (T: SetCategory) -> with {
+                                        StackAggregate T;
+                                        stack: List T -> %;
+                                  }
+\end{verbatim}
+Note that nothing appears before the \verb'with'. No problem because
+that is equivalent to a \verb'Join' in Aldor.
+\section{Ordinary Categories}\label{sec:Category}
+The category \verb'SquareFreeNormalizedTriangularSetCategory' without
+a default package.
+\begin{verbatim}
+SquareFreeNormalizedTriangularSetCategory(_
+        R: GcdDomain,_
+        E: OrderedAbelianMonoidSup,_
+        V: OrderedSet,_
+        P:RecursivePolynomialCategory(R, E, V)): Category ==
+    Join(_
+        SquareFreeRegularTriangularSetCategory(R,E,V,P),_
+         NormalizedTriangularSetCategory(R,E,V,P))
+\end{verbatim}
+It is translated into \ldots
+\begin{verbatim}
+(|Sequence| (|Import| NIL |AxiomLib|) (|Import| NIL |Boolean|)
+    (|Define|
+        (|Declare| |SquareFreeNormalizedTriangularSetCategory|
+            (|Apply| ->
+                     (|Comma| (|Declare| |#1| |GcdDomain|)
+                              (|Declare| |#2|
+                                  |OrderedAbelianMonoidSup|)
+                              (|Declare| |#3| |OrderedSet|)
+                              (|Declare| |#4|
+                                  (|Apply| |RecursivePolynomialCategory|
+                                           |#1| |#2| |#3|)))
+                     |Category|))
+        (|Lambda|
+            (|Comma| (|Declare| |#1| |GcdDomain|)
+                     (|Declare| |#2| |OrderedAbelianMonoidSup|)
+                     (|Declare| |#3| |OrderedSet|)
+                     (|Declare| |#4|
+                         (|Apply| |RecursivePolynomialCategory| |#1|
+                                  |#2| |#3|)))
+            |Category|
+            (|Label| |SquareFreeNormalizedTriangularSetCategory|
+                     (|With| NIL
+                             (|Sequence|
+                                 (|Apply| 
|SquareFreeRegularTriangularSetCategory|
+                                          |#1| |#2| |#3| |#4|)
+                                 (|Apply| |NormalizedTriangularSetCategory|
+                                          |#1| |#2| |#3| |#4|)))))))
+\end{verbatim}
+That is the parsed source of the Aldor code \ldots
+\begin{verbatim}
+import from AxiomLib;
+import from Boolean;
+SquareFreeNormalizedTriangularSetCategory: (
+        R: GcdDomain,
+        E: OrderedAbelianMonoidSup,
+        V: OrderedSet,
+        P: RecursivePolynomialCategory(R, E, V)
+) -> Category == (
+        R: GcdDomain,
+        E: OrderedAbelianMonoidSup,
+        V: OrderedSet,
+        P: RecursivePolynomialCategory(R, E, V)
+): Category +-> with {
+        SquareFreeRegularTriangularSetCategory(R, E, V, P),
+        NormalizedTriangularSetCategory(R, E, V, P)
+}
+\end{verbatim}
+  Again, nothing appears in front of the \verb'with'. No problem
+  because that is equivalent to a \verb'Join' in Aldor.
+\section{Ordinary Categories with Default Packages}
+\label{sec:Category+Default}
+The category \verb'StringAggregate' with default package.
+\begin{verbatim}
+StringAggregate: Category == OneDimensionalArrayAggregate Character with
+    lowerCase       : % -> %
+    lowerCase_!: % -> %
+    upperCase       : % -> %
+    ...
+    rightTrim: (%, CharacterClass) -> %
+    elt: (%, %) -> %
+ add
+   trim(s: %, c:  Character)      == leftTrim(rightTrim(s, c),  c)
+   trim(s: %, cc: CharacterClass) == leftTrim(rightTrim(s, cc), cc)
+   lowerCase s           == lowerCase_! copy s
+   upperCase s           == upperCase_! copy s
+   prefix?(s, t)         == substring?(s, t, minIndex t)
+   coerce(c:Character):% == new(1, c)
+   elt(s:%, t:%): %      == concat(s,t)$%
+\end{verbatim}
+It is translated into \ldots
+\begin{verbatim}
+(|Sequence| (|Import| NIL |AxiomLib|) (|Import| NIL |Boolean|)
+    (|Foreign| (|Declare| |dummyDefault| |Exit|) |Lisp|)
+    (|Define| (|Declare| |StringAggregate| |Category|)
+        (|With| NIL
+                (|Sequence|
+                    (|Apply| |OneDimensionalArrayAggregate|
+                             |Character|)
+                    (|Declare| |lowerCase| (|Apply| -> (|Comma| %) %))
+                    (|Declare| |lowerCase!| (|Apply| -> (|Comma| %) %))
+                    (|Declare| |upperCase| (|Apply| -> (|Comma| %) %))
+                    ...
+                    (|Declare| |rightTrim|
+                        (|Apply| -> (|Comma| % |CharacterClass|) %))
+                    (|Declare| |apply| (|Apply| -> (|Comma| % %) %))
+                    (|Default|
+                        (|Sequence|
+                            (|Define|
+                                (|Declare| |coerce|
+                                    (|Apply| -> (|Comma| |Character|)
+                                     %))
+                                (|Lambda|
+                                    (|Comma|
+                                     (|Declare| |t#1| |Character|))
+                                    %
+                                    (|Label| |coerce| |dummyDefault|)))
+                            (|Define|
+                                (|Declare| |apply|
+                                    (|Apply| -> (|Comma| % %) %))
+                                (|Lambda|
+                                    (|Comma| (|Declare| |t#1| %)
+                                     (|Declare| |t#2| %))
+                                    % (|Label| |apply| |dummyDefault|)))
+                            (|Define|
+                                (|Declare| |lowerCase|
+                                    (|Apply| -> (|Comma| %) %))
+                                (|Lambda| (|Comma| (|Declare| |t#1| %))
+                                    %
+                                    (|Label| |lowerCase|
+                                     |dummyDefault|)))
+                            ...
+                            ))))))
+\end{verbatim}
+That is the parsed source of the Aldor code \ldots
+\begin{verbatim}
+import from AxiomLib;
+import from Boolean;
+import dummyDefault: Exit from Foreign Lisp;
+StringAggregate: Category == with {
+    OneDimensionalArrayAggregate Character;
+    lowerCase: % -> %;
+    lowerCase!: % -> %;
+    upperCase: % -> %;
+    ...
+    rightTrim: (%, CharacterClass) -> %;
+    apply: (%, %) -> %
+ default {
+   coerce: Character -> % == (t: Character): % +-> dummyDefault;
+   apply: (%, %) -> %     == (t1: %, t2: %): % +-> dummyDefault;
+   lowerCase: % -> %      == (t: %): %         +-> dummyDefault;
+   ...
+}
+\end{verbatim}
+It is important to note that the actual default functions are given by
+a dummy implementation that is imported from LISP.
+
+And again, nothing appears in front of the \verb'with'. No problem
+because that is equivalent to a \verb'Join' in Aldor.
+
+Note that the \verb'elt' function is translated into \verb'apply'.
+\section{Initial Domains without Arguments}
+\label{sec:InitDomain}
+\begin{verbatim}
+SingleInteger(): Join(IntegerNumberSystem,Logic,OpenMath) with
+   canonical
+   canonicalsClosed
+   noetherian
+   max      : () -> %
+   min      : () -> %
+   "not":   % -> %
+   "~"  :   % -> %
+   "/\": (%, %) -> %
+   "\/" : (%, %) -> %
+   "xor": (%, %) -> %
+   Not  : % -> %
+   And  : (%,%) -> %
+   Or   : (%,%) -> %
+ == add
+   ...
+\end{verbatim}
+It is translated into \ldots
+\begin{verbatim}
+(|Sequence| (|Import| NIL |AxiomLib|) (|Import| NIL |Boolean|)
+    (|Extend|
+        (|Define|
+            (|Declare| |SingleInteger|
+                (|With| NIL
+                        (|Sequence| |IntegerNumberSystem| |Logic|
+                            |OpenMath|
+                            (|RestrictTo| |canonical| |Category|)
+                            (|RestrictTo| |canonicalsClosed|
+                                |Category|)
+                            (|RestrictTo| |noetherian| |Category|)
+                            (|Declare| |max| (|Apply| -> (|Comma|) %))
+                            (|Declare| |min| (|Apply| -> (|Comma|) %))
+                            (|Declare| |not|
+                                (|Apply| -> (|Comma| %) %))
+                            (|Declare| ~ (|Apply| -> (|Comma| %) %))
+                            (|Declare| |/\\|
+                                (|Apply| -> (|Comma| % %) %))
+                            (|Declare| |\\/|
+                                (|Apply| -> (|Comma| % %) %))
+                            (|Declare| |xor|
+                                (|Apply| -> (|Comma| % %) %))
+                            (|Declare| |Not|
+                                (|Apply| -> (|Comma| %) %))
+                            (|Declare| |And|
+                                (|Apply| -> (|Comma| % %) %))
+                            (|Declare| |Or|
+                                (|Apply| -> (|Comma| % %) %)))))
+            (|Add| (|PretendTo| (|Add| NIL NIL)
+                       (|With| NIL
+                               (|Sequence| |IntegerNumberSystem|
+                                   |Logic| |OpenMath|
+                                   (|RestrictTo| |canonical|
+                                    |Category|)
+                                   (|RestrictTo| |canonicalsClosed|
+                                    |Category|)
+                                   (|RestrictTo| |noetherian|
+                                    |Category|)
+                                   (|Declare| |max|
+                                    (|Apply| -> (|Comma|) %))
+                                   (|Declare| |min|
+                                    (|Apply| -> (|Comma|) %))
+                                   (|Declare| |not|
+                                    (|Apply| -> (|Comma| %) %))
+                                   (|Declare| ~
+                                    (|Apply| -> (|Comma| %) %))
+                                   (|Declare| |/\\|
+                                    (|Apply| -> (|Comma| % %) %))
+                                   (|Declare| |\\/|
+                                    (|Apply| -> (|Comma| % %) %))
+                                   (|Declare| |xor|
+                                    (|Apply| -> (|Comma| % %) %))
+                                   (|Declare| |Not|
+                                    (|Apply| -> (|Comma| %) %))
+                                   (|Declare| |And|
+                                    (|Apply| -> (|Comma| % %) %))
+                                   (|Declare| |Or|
+                                    (|Apply| -> (|Comma| % %) %)))))
+                   NIL))))
+\end{verbatim}
+That is the parsed source of the Aldor code \ldots
+\begin{verbatim}
+import from AxiomLib;
+import from Boolean;
+extend SingleInteger: with {
+        IntegerNumberSystem;
+        Logic;
+        OpenMath;
+        canonical @ Category;
+        canonicalsClosed @ Category;
+        noetherian @ Category;
+        max: () -> %;
+        min: () -> %;
+        _not: % -> %;
+        ~:   % -> %;
+        /\:  (%, %) -> %;
+        \/:  (%, %) -> %;
+        xor: (%, %) -> %;
+        Not: % -> %;
+        And: (%,%) -> %;
+        Or : (%,%) -> %;
+}
+ == (add pretend with {
+        IntegerNumberSystem;
+        Logic;
+        OpenMath;
+        canonical @ Category;
+        canonicalsClosed @ Category;
+        noetherian @ Category;
+        max: () -> %;
+        min: () -> %;
+        _not: % -> %;
+        ~:   % -> %;
+        /\:  (%, %) -> %;
+        \/:  (%, %) -> %;
+        xor: (%, %) -> %;
+        Not: % -> %;
+        And: (%,%) -> %;
+        Or : (%,%) -> %;
+}) add;
+\end{verbatim}
+\section{Initial Domains with Arguments}
+\label{sec:ParametrizedInitDomain}
+\begin{verbatim}
+SegmentBinding(S:Type): Type with
+  equation: (Symbol, Segment S) -> %
+  variable: % -> Symbol
+  segment : % -> Segment S
+  if S has SetCategory then SetCategory
+ == add
+  Rep := Record(var:Symbol, seg:Segment S)
+  ...
+\end{verbatim}
+It is translated into \ldots
+\begin{verbatim}
+(|Sequence| (|Import| NIL |AxiomLib|) (|Import| NIL |Boolean|)
+    (|Sequence|
+        (|Define|
+            (|Declare| |SegmentBindingExtendCategory|
+                (|Apply| -> (|Declare| |#1| |Type|) |Category|))
+            (|Lambda| (|Comma| (|Declare| |#1| |Type|)) |Category|
+                (|Label| |SegmentBindingExtendCategory|
+                         (|With| NIL
+                                 (|Sequence|
+                                     (|Declare| |equation|
+                                      (|Apply| ->
+                                       (|Comma| |Symbol|
+                                        (|Apply| |Segment| |#1|))
+                                       %))
+                                     (|Declare| |variable|
+                                      (|Apply| -> (|Comma| %) |Symbol|))
+                                     (|Declare| |segment|
+                                      (|Apply| -> (|Comma| %)
+                                       (|Apply| |Segment| |#1|)))
+                                     (|If|
+                                      (|Test|
+                                       (|Has| |#1| |SetCategory|))
+                                      |SetCategory| NIL))))))
+        (|Extend|
+            (|Define|
+                (|Declare| |SegmentBinding|
+                    (|Apply| -> (|Declare| |#1| |Type|)
+                             (|Apply| |SegmentBindingExtendCategory|
+                                      |#1|)))
+                (|Lambda| (|Comma| (|Declare| |#1| |Type|))
+                    (|Apply| |SegmentBindingExtendCategory| |#1|)
+                    (|Label| |SegmentBinding|
+                             (|Add| (|PretendTo| (|Add| NIL NIL)
+                                     (|Apply|
+                                      |SegmentBindingExtendCategory|
+                                      |#1|))
+                                    NIL)))))))
+\end{verbatim}
+That is the parsed source of the Aldor code \ldots
+\begin{verbatim}
+import from AxiomLib;
+import from Boolean;
+SegmentBindingExtendCategory: (S: Type) -> Category ==
+  (T: Type): Category +-> with {
+  equation: (Symbol, Segment S) -> %;
+  variable: % -> Symbol;
+  segment : % -> Segment S;
+  if S has SetCategory then SetCategory;
+}
+extend SegmentBinding: (S: Type) -> SegmentBindingExtendCategory S ==
+  (S: Type): SegmentBindingExtendCategory S +->
+    (add pretend SegmentBindingExtendCategory S) add;
+\end{verbatim}
+The last lines are actually equivalent to
+\begin{verbatim}
+extend SegmentBinding(S: Type): SegmentBindingExtendCategory S ==
+    (add pretend SegmentBindingExtendCategory S) add;
+\end{verbatim}
+
+\section{axFormatPref}
 Here we add an else clause. The original code read:
 \begin{verbatim}
       if name = '$ then name := '%