Literals and Symbols in Axiom
I think Axiom needs a Literal domain that works in a
manner similar to the Aldor language. SPAD and the Axiom
interpreter should not automatically treat a constant like
2 is a PositiveInteger.
\begin{axiom}
2
\end{axiom}
There are many situations when I might want it to mean
something else, e.g. the mathematical category 2 or the
some Boolean-like lattice domain, but I do not want to
or cannot provide an artificial means of coercing
PositiveInteger to things of the kind I want 2 to
represent. Instead we should see:
2
Type: Literal
Then if I use 2 in a context that requires, for example
a PositiveInteger the interpreter should use it's normal
function selection mechanism to choose coercions for 2
and 3 and and a suitable operation for +. So the end
result for
\begin{axiom}
2+3
\end{axiom}
would be the same.
If SPAD and the Axiom interpreter where changed to deal with
literals in this way, then some Axiom domains would need to
be extended to provide the needed coercions. Because Aldor
already does this, the code required would be similar to
that used in the Aldor-Axiom interface.
Here is the code from the Aldor interface for Axiom that deals
with coercions from the domain Literal that is created by
the Aldor compiler. (Some code is commented out to enable it
to compile from within Axiom.) The point is that it must be
possible to convert literals like 2 appearing in the Aldor
source to something that Axiom can also understand, like
Integer or however else it might be used.
\begin{aldor}
#include "axiom"
-----------------------------------------------------------------------------
----
---- axlit.as: Function definitions needed by the Axiom library.
----
-----------------------------------------------------------------------------
---- Copyright (c) 1990-2007 Aldor Software Organization Ltd (Aldor.org).
-----------------------------------------------------------------------------
- -- This file extends some Axiom types provide literal formers and other
- functions for compiling Axiom-generated .ax files.
--import from AxiomLib?;
--inline from AxiomLib?;
- macro {
- rep x == x @ % pretend Rep;
-- per r == r @ Rep pretend %;
Bit == Boolean;
Str == String;
SI == SingleInteger?;
I == Integer;
NNI == NonNegativeInteger?;
PI == PositiveInteger?;
BVal? == BuiltinValue?;
BArr? == BuiltinArray?;
SEG == Segment;
UNISEG == UniversalSegment?;
}
import {
AXL_-error: String -> Exit;
} from Foreign Lisp;
--error (s: String) : Exit == AXL_-error s;
integer (l: Literal) : Literal == l;
--- Builtin value type. Used to store data values which fit in a single word.
--BuiltinValue? : with == add;
--- Builtin array type. 0-based indexing.
--BuiltinArray? : with {
-- new: SI -> %;
-- #: % -> SI;
-- apply: (%, SI) -> BVal?;
-- set!: (%, SI, BVal?) -> ();
--}
--== add {
-- import {
-- AXL_-arrayNew: SI -> %;
-- AXL_-arraySize: % -> SI;
-- AXL_-arrayRef: (%, SI) -> BVal?;
-- AXL_-arraySet: (%, SI, BVal?) -> ();
-- } from Foreign Lisp;
--
-- new (n: SI) : % == AXL_-arrayNew n;
-- # (x: %) : SI == AXL_-arraySize x;
--
-- apply (x: %, n: SI) : BVal? ==
-- AXL_-arrayRef(x, n);
--
-- set! (x: %, n: SI, v: BVal?) : () ==
-- - AXL_-arraySet(x, n, v);
--}
extend String : with {
string: Literal -> %;
}
== add {
import {
AXL_-LiteralToString?: Literal -> %;
} from Foreign Lisp;
string (l: Literal) : % == AXL_-LiteralToString? l;
}
extend Symbol : with {
string: Literal -> %;
}
== add {
string (l: Literal) : % == string(l)$String::%;
}
extend SingleInteger? : with {
integer: Literal -> %;
coerce: I -> %;
zero: () -> %;
one: () -> %;
inc: % -> %;
dec: % -> %;
leq: (%, %) -> Bit;
spit: % -> ();
}
== add {
Rep ==> Integer;
import {
AXL_-LiteralToSingleInteger?: Literal -> %;
AXL_-zerofnSingleInteger: () -> %;
AXL_-onefnSingleInteger: () -> %;
AXL_-incSingleInteger: % -> %;
AXL_-decSingleInteger: % -> %;
AXL_-leSingleInteger: (%, %) -> Bit;
AXL_-spitSInt: % -> ();
} from Foreign Lisp;
integer (l: Literal) : % == AXL_-LiteralToSingleInteger? l;
coerce (n: I) : % == per n;
zero () : % == AXL_-zerofnSingleInteger();
one () : % == AXL_-onefnSingleInteger();
inc (n: %) : % == AXL_-incSingleInteger n;
dec (n: %) : % == AXL_-decSingleInteger n;
leq (x: %, y: %) : Bit == AXL_-leSingleInteger(x, y);
spit (x: %) : () == AXL_-spitSInt x;
}
extend Integer : with {
integer: Literal -> %;
}
== add {
import {
AXL_-LiteralToInteger?: Literal -> %;
} from Foreign Lisp;
integer (l: Literal) : % == AXL_-LiteralToInteger? l;
}
extend NonNegativeInteger? : with {
integer: Literal -> %;
coerce: Integer -> %;
}
== add {
import {
AXL_-IntegerIsNonNegative?: Integer -> Bit;
} from Foreign Lisp;
Rep ==> Integer;
import from Rep, String;
integer (l: Literal) : % == integer(l)$Integer::%;
coerce (i: Integer) : % == {
if AXL_-IntegerIsNonNegative? i then
per i
else
error "Need a non-negative integer"
}
}
extend PositiveInteger? : with {
integer: Literal -> %;
coerce: Integer -> %;
}
== add {
import {
AXL_-IntegerIsPositive?: Integer -> Bit;
} from Foreign Lisp;
Rep ==> Integer;
import from Rep, String;
integer (l: Literal) : % == integer(l)$Integer::%;
coerce (i: Integer) : % == {
if AXL_-IntegerIsPositive? i then
per i
else
error "Need a positive integer"
}
}
extend DoubleFloat?: with {
float: Literal -> %;
}
== add {
import {
AXL_-LiteralToDoubleFloat?: Literal -> %;
} from Foreign Lisp;
float (l: Literal) : % == AXL_-LiteralToDoubleFloat? l;
}
extend Float: with {
float: Literal -> %;
}
== add {
import {
AXL_-StringToFloat?: String -> %;
} from Foreign Lisp;
import from String;
float (l: Literal) : % == AXL_-StringToFloat? string l;
}
- --extend Tuple (T: Type) : with {
- length: % -> SI;
-- element: (%, SI) -> T;
--
-- export from T;
--}
--== add {
-- Rep ==> Record(sz: SI, values: BArr?);
-- import from Rep;
--
-- length (t: %) : SI == rep(t).sz;
-- element(t: %, n: SI): T == (rep(t).values.(dec n)) pretend T;
--}
extend List (S: Type) : with {
bracket: Tuple S -> %;
nil: %;
first: % -> S;
rest: % -> %;
cons: (S, %) -> %;
empty: () -> %;
empty?: % -> Bit;
test: % -> Bit;
setfirst!: (%, S) -> S;
setrest!: (%, %) -> %;
}
== add {
import {
AXL_-nilfn: () -> %;
AXL_-car: % -> S;
AXL_-cdr: % -> %;
AXL_-cons: (S, %) -> %;
AXL_-rplaca: (%, S) -> S;
AXL_-rplacd: (%, %) -> %;
AXL_-null?: % -> Bit;
} from Foreign Lisp;
[t: Tuple S]?: % == {
import {
one: () -> %;
dec: % -> %;
leq: (%, %) -> Bit;
} from SI;
--!! Remove the local when we can use the export.
local nil: % := empty();
l := nil;
i := length t;
while leq(one(), i) repeat {
l := cons(element(t, i), l);
i := dec i;
}
l;
}
-- Redefine a selection of List operations for efficiency.
nil : % == AXL_-nilfn();
first (x: %): S == AXL_-car x;
rest (x: %): % == AXL_-cdr x;
cons (x: S, y: %): % == AXL_-cons(x, y);
setfirst!(x: %, y: S): S == AXL_-rplaca(x, y);
setrest! (x: %, y: %): % == AXL_-rplacd(x, y);
empty (): % == AXL_-nilfn();
empty? (x: %): Bit == AXL_-null? x;
test (x: %): Bit == not empty? x;
}
\end{aldor}
If SPAD and the Axiom interpreter created values from the
domain
Literal then it would be unnecessary to treat
constants like
0 and
1 in a special manner, i.e. as
unary functions. The coercions from
Literal would do
that job.
Some or all expressions may not have rendered properly,
because Axiom returned the following error:
Error: export FRICAS=/usr/local/lib/axiom/target/x86_64-unknown-linux; export ALDORROOT=/usr/local/aldor/linux/1.1.0; export PATH=$ALDORROOT/bin:$PATH; export HOME=/var/zope2/var/LatexWiki; ulimit -t 600; export LD_LIBRARY_PATH=/usr/local/lib/axiom/target/x86_64-unknown-linux/lib; LANG=en_US.UTF-8 $FRICAS/bin/FRICASsys < /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/7176996356010151088-25px.axm
/bin/sh: /usr/local/lib/axiom/target/x86_64-unknown-linux/bin/FRICASsys: not found
Some or all expressions may not have rendered properly,
because Latex returned the following error:
This is pdfTeXk, Version 3.141592-1.40.3 (Web2C 7.5.6)
\write18 enabled.
%&-line parsing enabled.
entering extended mode
(./3893344738967034407-16.0px.tex
LaTeX2e <2005/12/01>
Babel <v3.8h> and hyphenation patterns for english, usenglishmax, dumylang, noh
yphenation, arabic, farsi, croatian, ukrainian, russian, bulgarian, czech, slov
ak, danish, dutch, finnish, basque, french, german, ngerman, ibycus, greek, mon
ogreek, ancientgreek, hungarian, italian, latin, mongolian, norsk, icelandic, i
nterlingua, turkish, coptic, romanian, welsh, serbian, slovenian, estonian, esp
eranto, uppersorbian, indonesian, polish, portuguese, spanish, catalan, galicia
n, swedish, ukenglish, pinyin, loaded.
(/usr/share/texmf-texlive/tex/latex/base/article.cls
Document Class: article 2005/09/16 v1.4f Standard LaTeX document class
(/usr/share/texmf-texlive/tex/latex/base/size12.clo))
(/usr/share/texmf-texlive/tex/latex/ucs/ucs.sty
(/usr/share/texmf-texlive/tex/latex/ucs/data/uni-global.def))
(/usr/share/texmf-texlive/tex/latex/base/inputenc.sty
(/usr/share/texmf-texlive/tex/latex/ucs/utf8x.def))
(/usr/share/texmf-texlive/tex/latex/bbm/bbm.sty)
(/usr/share/texmf-texlive/tex/latex/jknapltx/mathrsfs.sty)
(/usr/share/texmf-texlive/tex/latex/base/fontenc.sty
(/usr/share/texmf-texlive/tex/latex/base/t1enc.def))
(/usr/share/texmf-texlive/tex/latex/pstricks/pstricks.sty
(/usr/share/texmf-texlive/tex/generic/pstricks/pstricks.tex
`PSTricks' v1.15 <2006/12/22> (tvz)
(/usr/share/texmf-texlive/tex/generic/pstricks/pstricks.con))
(/usr/share/texmf/tex/latex/xcolor/xcolor.sty
(/etc/texmf/tex/latex/config/color.cfg)
(/usr/share/texmf-texlive/tex/latex/graphics/dvips.def)
(/usr/share/texmf-texlive/tex/latex/graphics/dvipsnam.def)))
(/usr/share/texmf-texlive/tex/latex/graphics/epsfig.sty
(/usr/share/texmf-texlive/tex/latex/graphics/graphicx.sty
(/usr/share/texmf-texlive/tex/latex/graphics/keyval.sty)
(/usr/share/texmf-texlive/tex/latex/graphics/graphics.sty
(/usr/share/texmf-texlive/tex/latex/graphics/trig.sty)
(/etc/texmf/tex/latex/config/graphics.cfg))))
(/usr/share/texmf-texlive/tex/latex/pst-grad/pst-grad.sty
(/usr/share/texmf-texlive/tex/generic/pst-grad/pst-grad.tex
(/usr/share/texmf-texlive/tex/latex/xkeyval/pst-xkey.tex
(/usr/share/texmf-texlive/tex/latex/xkeyval/xkeyval.sty
(/usr/share/texmf-texlive/tex/latex/xkeyval/xkeyval.tex)))
`pst-plot' v1.05, 2006/11/04 (tvz,dg,hv)))
(/usr/share/texmf-texlive/tex/latex/pstricks/pst-plot.sty
(/usr/share/texmf-texlive/tex/generic/pstricks/pst-plot.tex
v97 patch 2, 1999/12/12
(/usr/share/texmf-texlive/tex/generic/multido/multido.tex
v1.41, 2004/05/18 <tvz>)))
(/usr/share/texmf-texlive/tex/latex/geometry/geometry.sty
(/usr/share/texmf-texlive/tex/xelatex/xetexconfig/geometry.cfg)
Package geometry Warning: `lmargin' and `rmargin' result in NEGATIVE (-108.405p
t).
`width' should be shortened in length.
) (/usr/share/texmf-texlive/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `? option.
(/usr/share/texmf-texlive/tex/latex/amsmath/amstext.sty
(/usr/share/texmf-texlive/tex/latex/amsmath/amsgen.sty))
(/usr/share/texmf-texlive/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texmf-texlive/tex/latex/amsmath/amsopn.sty))
(/usr/share/texmf-texlive/tex/latex/amsfonts/amsfonts.sty)
(/usr/share/texmf-texlive/tex/latex/amsfonts/amssymb.sty)
(/usr/share/texmf-texlive/tex/latex/amscls/amsthm.sty)
(/usr/share/texmf-texlive/tex/latex/setspace/setspace.sty
Package: `setspace 6.7 <2000/12/01>
) (/usr/share/texmf-texlive/tex/generic/xypic/xy.sty
(/usr/share/texmf-texlive/tex/generic/xypic/xy.tex Bootstrap'ing: catcodes,
docmode, (/usr/share/texmf-texlive/tex/generic/xypic/xyrecat.tex)
(/usr/share/texmf-texlive/tex/generic/xypic/xyidioms.tex)
Xy-pic version 3.7 <1999/02/16>
Copyright (c) 1991-1998 by Kristoffer H. Rose <krisrose@ens-lyon.fr>
Xy-pic is free software: see the User's Guide for details.
Loading kernel: messages; fonts; allocations: state, direction,
utility macros; pictures: \xy, positions, objects, decorations;
kernel objects: directionals, circles, text; options; algorithms: directions,
edges, connections; Xy-pic loaded))
(/usr/share/texmf-texlive/tex/generic/xypic/xyall.tex
Xy-pic option: All features v.3.3
(/usr/share/texmf-texlive/tex/generic/xypic/xycurve.tex
Xy-pic option: Curve and Spline extension v.3.7 curve, circles, loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xyframe.tex
Xy-pic option: Frame and Bracket extension v.3.7 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xycmtip.tex
Xy-pic option: Computer Modern tip extension v.3.3
(/usr/share/texmf-texlive/tex/generic/xypic/xytips.tex
Xy-pic option: More Tips extension v.3.3 loaded) loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xyline.tex
Xy-pic option: Line styles extension v.3.6 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xyrotate.tex
Xy-pic option: Rotate and Scale extension v.3.3 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xycolor.tex
Xy-pic option: Colour extension v.3.3 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xymatrix.tex
Xy-pic option: Matrix feature v.3.4 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xyarrow.tex
Xy-pic option: Arrow and Path feature v.3.5 path, \ar, loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xygraph.tex
Xy-pic option: Graph feature v.3.7 loaded) loaded)
(/usr/share/texmf-texlive/tex/latex/tools/verbatim.sty)
(/usr/share/texmf/tex/latex/graphviz/graphviz.sty
(/usr/share/texmf-texlive/tex/latex/psfrag/psfrag.sty))
(/usr/share/texmf/tex/latex/sagetex.sty
Writing sage input file 3893344738967034407-16.0px.sage
(./3893344738967034407-16.0px.sout))
(/usr/share/texmf-texlive/tex/latex/gnuplottex/gnuplottex.sty
(/usr/share/texmf-texlive/tex/latex/base/latexsym.sty)
(/usr/share/texmf-texlive/tex/latex/moreverb/moreverb.sty)
(/usr/share/texmf-texlive/tex/latex/base/ifthen.sty))
(./3893344738967034407-16.0px.aux)
(/usr/share/texmf-texlive/tex/latex/ucs/ucsencs.def)
(/usr/share/texmf-texlive/tex/latex/base/t1cmtt.fd)
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 123.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 126.
You can't use `macro parameter character #' in vertical mode.
l.128 #
include "axiom"
Missing $ inserted.
<inserted text>
$
l.160 AXL_
-error: String -> Exit;
(/usr/share/texmf-texlive/tex/latex/jknapltx/ursfs.fd)
(/usr/share/texmf-texlive/tex/latex/amsfonts/umsa.fd)
(/usr/share/texmf-texlive/tex/latex/amsfonts/umsb.fd)
(/usr/share/texmf-texlive/tex/latex/base/ulasy.fd)
Extra }, or forgotten $.
l.161 }
from Foreign Lisp;
Missing $ inserted.
<inserted text>
$
l.162
Missing $ inserted.
<inserted text>
$
l.163 --error (s: String) : Exit == AXL_
-error s;
Missing $ inserted.
<inserted text>
$
l.165
You can't use `macro parameter character #' in horizontal mode.
l.172 -- #
: % -> SI;
Missing $ inserted.
<inserted text>
$
l.178 -- AXL_
-arrayNew: SI -> %;
Extra }, or forgotten $.
l.182 -- }
from Foreign Lisp;
You can't use `macro parameter character #' in math mode.
l.185 -- #
(x: %) : SI == AXL_-arraySize x;
Extra }, or forgotten $.
l.192 --}
Missing $ inserted.
<inserted text>
$
l.193
Missing $ inserted.
<inserted text>
$
l.199 AXL_
-LiteralToString: Literal -> %;
Extra }, or forgotten $.
l.200 }
from Foreign Lisp;
Missing $ inserted.
<inserted text>
$
l.201
Missing $ inserted.
<inserted text>
$
l.227 AXL_
-LiteralToSingleInteger: Literal -> %;
Extra }, or forgotten $.
l.234 }
from Foreign Lisp;
Missing $ inserted.
<inserted text>
$
l.235
Overfull \hbox (71.42375pt too wide) in paragraph at lines 226--235
[]\T1/cmr/m/n/12 import AXL$[]\OML/cmm/m/it/12 LiteralToSingleInteger \OT1/cmr
/m/n/12 : \OML/cmm/m/it/12 Literal\OMS/cmsy/m/n/12 ^^@ \OML/cmm/m/it/12 > AXL[]
zerofnSingleInteger \OT1/cmr/m/n/12 : ()\OMS/cmsy/m/n/12 ^^@ \OML/cmm/m/it/12 >
AXL[]onefnSingleInteger \OT1/cmr/m/n/12 : ()\OMS/cmsy/m/n/12 ^^@ \OML/cmm/m/it
/12 > AXL[]incSingleInteger \OT1/cmr/m/n/12 :
Missing $ inserted.
<inserted text>
$
l.252 AXL_
-LiteralToInteger: Literal -> %;
Extra }, or forgotten $.
l.253 }
from Foreign Lisp;
Missing $ inserted.
<inserted text>
$
l.254
Missing $ inserted.
<inserted text>
$
l.264 AXL_
-IntegerIsNonNegative: Integer -> Bit;
Extra }, or forgotten $.
l.265 }
from Foreign Lisp;
Missing $ inserted.
<inserted text>
$
l.268
Missing $ inserted.
<inserted text>
$
l.272 if AXL_
-IntegerIsNonNegative i then
Extra }, or forgotten $.
l.276 }
Extra }, or forgotten $.
l.277 }
Missing $ inserted.
<inserted text>
$
l.278
Missing $ inserted.
<inserted text>
$
l.285 AXL_
-IntegerIsPositive: Integer -> Bit;
Extra }, or forgotten $.
l.286 }
from Foreign Lisp;
Extra }, or forgotten $.
l.295 }
Missing $ inserted.
<inserted text>
$
l.296
Overfull \hbox (205.97543pt too wide) in paragraph at lines 279--296
\OML/cmm/m/it/12 Bit\OT1/cmr/m/n/12 ; \OML/cmm/m/it/12 fromForeignLisp\OT1/cmr/
m/n/12 ; \OML/cmm/m/it/12 Rep \OT1/cmr/m/n/12 ==\OML/cmm/m/it/12 > Integer\OT1/
cmr/m/n/12 ; \OML/cmm/m/it/12 importfromRep; String\OT1/cmr/m/n/12 ; \OML/cmm/m
/it/12 integer\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 l \OT1/cmr/m/n/12 : \OML/cmm/m/
it/12 Literal\OT1/cmr/m/n/12 ) : \OML/cmm/m/it/12 coerce\OT1/cmr/m/n/12 (\OML/c
mm/m/it/12 i \OT1/cmr/m/n/12 : \OML/cmm/m/it/12 Integer\OT1/cmr/m/n/12 ) : \OML
/cmm/m/it/12 ifAXL[]IntegerIsPositiveithenperielseerror\OT1/cmr/m/n/12 "\OML/cm
m/m/it/12 Needapositiveinteger\OT1/cmr/m/n/12 "$
Missing $ inserted.
<inserted text>
$
l.304 AXL_
-LiteralToDoubleFloat: Literal -> %;
Extra }, or forgotten $.
l.305 }
from Foreign Lisp;
Missing $ inserted.
<inserted text>
$
l.306
Missing $ inserted.
<inserted text>
$
l.315 AXL_
-StringToFloat: String -> %;
Extra }, or forgotten $.
l.316 }
from Foreign Lisp;
Missing $ inserted.
<inserted text>
$
l.317
[1]
Missing $ inserted.
<inserted text>
$
l.353 AXL_
-nilfn: () -> %;
Extra }, or forgotten $.
l.360 }
from Foreign Lisp;
Missing $ inserted.
<inserted text>
$
l.361
Missing } inserted.
<inserted text>
}
l.395 \end{aldor}
\newpage
Missing } inserted.
<inserted text>
}
l.395 \end{aldor}
\newpage
Missing } inserted.
<inserted text>
}
l.395 \end{aldor}
\newpage
Missing } inserted.
<inserted text>
}
l.395 \end{aldor}
\newpage
Missing } inserted.
<inserted text>
}
l.395 \end{aldor}
\newpage
Missing } inserted.
<inserted text>
}
l.395 \end{aldor}
\newpage
Missing } inserted.
<inserted text>
}
l.395 \end{aldor}
\newpage
Missing } inserted.
<inserted text>
}
l.395 \end{aldor}
\newpage
Missing } inserted.
<inserted text>
}
l.395 \end{aldor}
\newpage
Missing } inserted.
<inserted text>
}
l.395 \end{aldor}
\newpage
Missing } inserted.
<inserted text>
}
l.395 \end{aldor}
\newpage
[2] [3] (./3893344738967034407-16.0px.aux) )
(see the transcript file for additional information)
Output written on 3893344738967034407-16.0px.dvi (3 pages, 7120 bytes).
Transcript written on 3893344738967034407-16.0px.log.