axiom-developer
[Top][All Lists]

## Re: [Axiom-developer] RE: Another question

 From: Martin Rubey Subject: Re: [Axiom-developer] RE: Another question Date: 22 Aug 2006 11:46:10 +0200 User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.3

Dear Ralf,

> Anyway, would it be a good start to take dhmatrix. We could tex->latex it
> while
> we try to get an html out of it.

The one thing I don't understand about all this is:

why won't we use ALLPROSE?

> On Monday, August 21, 2006 1:08 PM Martin Rubey wrote:

> > The main obstacle is, that ALLPROSE expects a semicolon to end a
> > definition. Thus, I cheated and wrote:

> > <<exports: testSPAD>>= double: R -> R --; @
> >
> > It seems that ALLPROSE also expects that the signature appears on one line,
> > Ralf? At least
> >
> >       double: R -> _
> >                    R --;
> > @
> >
> > did not work.
> >
> > The main principle obstacle however is pile syntax (sorry Bill). It does
> > not mix well with neither .pamphlet_s nor .nw_s:
>
> (: No problem. :)
>
> What is ".pamphlet_s nor .nw_s"?

I meant, neither with pamphlet (i.e., Axiom project) files, nor with noweb
(i.e., ALLPROSE) files.

> To deal with pile syntax maybe we could make use of the SPAD to Aldor
> translation option built into Axiom that you mentioned in another thread?
> Even if it is not perfect, perhaps it is good enough to enable ALLPROSE to
> more easily extract the necessary information?

No. First of all, I don't think it's necessary. You only have to teach ALLPROSE
how to find out where a line ends. Currently, in ALLPROSE, the regexp used is
described in Section tools/addaldortypedef.pl of the ALLPROSE documentation,
but Ralf certainly knows better than me.

That's one thing I cannot do.

> From my point of view the objectives of using ALLPROSE are a little different
> than the objectives satisfied by the Axiom pamphlet files.

Well, the pamphlets satisfy only a subset of our needs. In particular, there is
very little support for HyperDoc. Using ALLPROSE, you get that (nearly) for
free: the +++ environments are copied into the code. When compiling the file
with Axiom, they magically appear in HyperDoc. Of course, within the +++
environments, one would have to restrict oneself to those things hyperdoc
understands. For example, ALLPROSE produces

+++   \begin{ToDo}
+++     \begin{rhx} 14-Aug-2006:
+++       It is not yet clear what the type of this function/constant
+++       should be.
+++ %
+++       In general, isomorphism types are equivalence classes of
+++       structures. It could be reasonable to say that \adthisname{}
+++       returns (unique) representatives of these classes. (The
+++       \emph{unique} is probably a though thing, since we might have no
+++       order on the input set or on $L$ in general.
+++     \end{rhx}
+++   \end{ToDo}
--#line 384 "species.as.nw"
isomorphismTypes: Set L -> Generator %;

Now, the main problem are the commands \adthisname and \adthistype. In the dvi
(or html or whatever) generated by ALLPROSE, they are replaced by the
appropriate names. In the example above, one would read:

+++       structures. It could be reasonable to say that isomorphismTypes
+++       returns (unique) representatives of these classes. (The

HyperDoc cannot handle that, unfortunately.

Ralf, would it be very difficult to make ALLPROSE magically replace \adthisname
with \spadfun{isomorphismTypes} (or, if you like that better, with

That's the second thing I cannot do.

All the other things I can do within HyperDoc.

Martin