[Axiom-developer] Latest Axiom update pushed... Volume 15 included

[Tim Daly]

The major change is the addition of book volume 15,
the Axiom Sane Compiler. As usual, this is in the
spirit of "working in public". There is nothing to
execute yet at the user level.
https://github.com/daly/PDFS/blob/master/bookvol0.pdf

This is just the "work in progress". The whole of Axiom's
Categories, Domains, and Packages are there and the
inheritance chain is correctly implemented.

The compiler is being built "middle-out". I've written
several compilers before but this turns out to be a very
useful way to construct one. The idea is to write code
in the intermediate langage (lisp) that executes and
"sugar" it with the Spad syntax. Since we'll be adding
new syntactic forms (e.g. axioms) we need to be very
flexible so we can "research" surface syntax ideas.

The Categories, Domains, and Packages are valid Lisp
types (via CLOS defclass) which will help with several
features such as direct-from-lisp calls to Axiom domains,
lisp level, as well as Spad-level, type checking, and a
much cleaner ability to debug (via CLOS wrappers).

Some of the signatures have been added to the chain,
mostly to prototype the CLOS data structures.

The initial handling of the new parser is there, including
a set of finite-state machine macros / functions which
mirror the EBNF handling.

Since the Spad parser just translates Spad code to
the CLOS structures, Axiom should be able to be
completely embedded in any other Lisp project as
a library.

The near term effort involves constructing the new parser.
The plan is to have the Spad grammar explicitly represented
and to mirror this representation in the code so that it is
relatively easy to modify the grammar and the code.

Musings are ongoing about automating the translation
from EBNF to lisp code but that seems to be a future
optimization as there is much else to do.

Current musings involve a search for a specification
language, an invariant language, an axiom/lemma
language, a proof mechanism, and a verification
machine for proof-carrying code.

Tim