22.1 Basic Axiom Types Extended
Since the extend Aldor keyword cannot yet be used for existing Axiom
domains, we have to introduce new domains ACInteger, ACString, ACCharacter,
ACMachineInteger that take care of the additional structure we need for
Combinat.
The domains starting with the AC prefix will later be used throughout Combinat
instead of the corresponding domains without that prefix. The macros in include/combinat.as.nw take care of renaming appropriately.
Let us first introduce an equivalent to Aldor’s OutputType. Doing it that
way, we don’t have to modify current code of Combinat. However, we have
to add CoercibleTo(OutputForm) in order to allow printing in Axiom.
570⟨cat: OutputType 570⟩≡ (569a)
OutputType: Category == with {
CoercibleTo OutputForm;
<<: (TextWriter, %) -> TextWriter;
default {
coerce(x: %): OutputForm == empty() << x;
}
}
Defines:
OutputType, used in chunks 62, 289, 329, 486, 503, 504, 523, 524, 572, 577, 580a, 581b,
585a, 587–89, 601, 610b, 611a, 615–17, 620a, 623, and 624a.
The type TotallyOrderedType is needed for the implementation of polynomials
in Combinat. Although it would have been possible to implement the polynomial
domains by just requiring a function <: (%, %) -> Boolean, it is much cleaner to
give a proper category for it.
571⟨cat: TotallyOrderedType 571⟩≡ (569a)
TotallyOrderedType: Category == with {
PrimitiveType;
<: (%, %) -> Boolean;
>: (%, %) -> Boolean;
<=: (%, %) -> Boolean;
>=: (%, %) -> Boolean;
compare: (%, %) -> ACMachineInteger;
default {
(x: %) > (y: %): Boolean == y < x;
(x: %) <= (y: %): Boolean == not (y < x);
(x: %) >= (y: %): Boolean == not (x < y);
compare(x: %, y: %): ACMachineInteger == {
x < y => -1;
x > y => 1;
0;
}
}
}
Defines:
TotallyOrderedType, used in chunks 329, 465, 484, 489, 495, 501, 506, 509a, 526, 581b,
585a, and 606.
Uses ACMachineInteger 584.
ToDo ⊲ 80 ⊳ rhx ⊲ 61 ⊳ 09-Dec-2006: This is and should always be a verbatim
copy of
LabelType as defined in
src/species.as.nw. The only reason that it
appears here and further below is that
Axiom cannot currently deal with extended
domains as for example is done for
String,
Integer, and
MachineInteger in
src/species.as.nw.
The exports of the domains ACString, ACCharacter, ACInteger, and
ACMachineInteger, include all the exports that are listed via
-
-
% aldor -gloop
#include "axiom"
String
Character
Integer
SingleInteger
respectively.
ToDo ⊲ 81 ⊳ mrx ⊲ 22 ⊳ However, this does not work entirely. Uncommenting
ListExtendCategory in the exports of
ACList below exhibits the following
behaviour in
Axiom:
l := [1,2,3]::List ACInteger::ACList ACInteger;
s := structures(set l)$Partition ACInteger;
next! s
>> System error:
The variable FOAM-USER::|G-axiom_ListExtendCategory_813754629| is unbound.
next! s
Looking in Array(ACList(ACInteger)) for new with code 100475244
>> System error:
FOAM-USER::|fiRaiseException| is invalid as a function.
|
rhx ⊲ 62 ⊳ 29-Jan-2007: Let me cite from a mail of Peter Broadbery (02-Jan-2007
19:43:38):
> Could you help with "ListExtendCategory". I cannot find any source for
> it in Axiom or in your code that compiles libaxiom.al. Still, that
> identifier is in libaxiom.al. The only reasonable file is
> int/aldor/ap/LIST.ap, but that is generated.
The short answer is that xxxExtendCategory is just a name for ’the axiom
definition of xxx’. The reason they exist is that certain domains are
declared as stubs then extended in the libaxiom build process.
In more detail, in genax.boot (which turns spad signatures into aldor
syntax files), any domain which needs to be extended from a basic
definition will be extended with a type of ’XxxExtendCategory’. In the
same file, this category is defined to be export the same operations as
the corresponding axiom type.
For example, List is defined originally in stub.as as
Vector(T: Type): with;
this is just enough to build the basic categories in libaxiom.
In VECTOR.ap:
define VectorExtendCategory(T: Type): Category == VectorCategory(T) with
extend Vector(T: Type): VectorExtendCategory(T);
|
rhx ⊲ 63 ⊳ 04-Feb-2007: The following steps are used to produce an error similar to
the above one of Martin.
cd combinat/trunk/combinat
notangle -t8 Makefile.nw > Makefile
make VARIANTSTOBUILD=axiom
cd src
for f in $(ar t libcombinatax.al); do ar x libcombinatax.al $f; done
for f in $(ar t libcombinatax.al); do echo ")lib $f" >> combinat.input; done
axiom
)read combinat
l: List ACInteger := [1,2,3] :: List(ACInteger)
ll: ACList(ACInteger) := l :: ACList(ACInteger)
s: SetSpecies(ACInteger) := set(ll)$SetSpecies(ACInteger);
|
The error reads as follows.
Looking in SingleInteger() for integer with code 475196805
>> System error:
FOAM-USER::|fiRaiseException| is invalid as a function.
|
This error even happens with and without ListExtendCategory compiled in to the
exports of ACList.
For Combinat we only need a few additional exports to make the types
from the Axiom library behaving like the ones from the Aldor library. All
those
<<exports of ... from LibAxiom>>
|
chunks could go away if proper extend works with Axiom.
22.1.1 ACCharacter
577⟨dom: ACCharacter 577⟩≡ (569a)
ACCharacter: with {
OutputType;
coerce: Character -> %;
coerce: % -> Character;
⟨exports of Character from LibAxiom 578⟩
} == Character add {
Rep == Character;
(tw: TextWriter) << (x: %): TextWriter == hconcat(tw, x::OutputForm);
coerce(x: %): Character == rep x;
coerce(x: Character): % == per x;
}
Defines:
ACCharacter, used in chunks 54 and 580.
Uses OutputType 570.
578⟨exports of Character from LibAxiom 578⟩≡ (577)
OrderedFinite;
ord: (%) -> Integer;
char: (Integer) -> %;
char: (String) -> %;
space: () -> %;
quote: () -> %;
escape: () -> %;
upperCase: (%) -> %;
lowerCase: (%) -> %;
digit?: (%) -> Boolean;
hexDigit?: (%) -> Boolean;
alphabetic?: (%) -> Boolean;
upperCase?: (%) -> Boolean;
lowerCase?: (%) -> Boolean;
alphanumeric?: (%) -> Boolean;
Uses Integer 66 and String 65.
22.1.2 ACString
ToDo ⊲ 82 ⊳ rhx ⊲ 64 ⊳ 09-Dec-2006: The (re-)implementation of
string and
integer seems to be necessary since otherwise one gets an error message
for
5) -> binomial(22,7)$MultinomialTools
Loading /home/hemmecke/software/Axiom/mnt/linux/algebra/ORDSET-.o
for domain OrderedSet&
Loading /home/hemmecke/software/Axiom/mnt/linux/algebra/RETRACT-.o
for domain RetractableTo&
Looking in ACInteger for integer with code 225876518
>> System error:
FOAM-USER::|fiRaiseException| is invalid as a function.
|
The thread starting at http://lists.nongnu.org/archive/html/axiom-developer/2006-12/msg00079.html
might be relavant to that problem.
Note that the first character of a string in Aldor has index zero, while in Axiom it
has index one. Thus, for writing portable code we cannot use the absolute
position to determine a character in the string. Maybe we can use generators
instead.
580b⟨implementation of String from LibAldor 580b⟩≡ (579)
(tw: TextWriter) << (x: %): TextWriter == hconcat(tw, message rep x);
generator(a: %): Generator ACCharacter == generate {
import from Integer, NNI, ACCharacter;
for i in 1..(#a::Integer) repeat yield((a.i)::ACCharacter);
}
bracket(g: Generator ACCharacter): % == {
import from ACCharacter;
l: List Character := [c::Character for c in g];
coerce construct l;
}
empty: % == per empty();
(x: %) + (y: %): % == per concat(rep x, rep y);
string(l: Literal): % == (string(l)$Rep) :: %;
leftTrim(s: %, c: ACCharacter): % == per leftTrim(rep s, coerce c);
rightTrim(s: %, c: ACCharacter): % == per rightTrim(rep s, coerce c);
Uses ACCharacter 577, Generator 617, and Integer 66.
580c⟨exports of String from LibAxiom 580c⟩≡ (579)
StringCategory;
22.1.3 ACInteger
581a⟨dom: ACInteger 581a⟩≡ (569a)
ACInteger: with {
ACLabelType;
⟨exports of Integer from LibAldor 581b⟩
⟨exports of Integer from LibAxiom 583⟩
} == Integer add {
Rep == Integer; import from Rep;
elements(): Generator % == generate {
for i: Integer in 1 .. repeat yield per i;
}
⟨implementation of Integer from LibAldor 582⟩
coerce(x: %): Integer == rep x;
coerce(x: Integer): % == per x;
integer(l: Literal): % == (integer(l)$Rep) :: %;
}
Defines:
ACInteger, used in chunks 54, 569b, 584, 585, and 595.
Uses ACLabelType 572, Generator 617, and Integer 66.
582⟨implementation of Integer from LibAldor 582⟩≡ (581a)
(tw: TextWriter) << (x: %): TextWriter == hconcat(tw, x::OutputForm);
bit?(x: %, i: I): Boolean == bit?(x, i::Z);
shift(x: %, i: I): % == shift(x, i::Z);
divide(x: %, y: %): (%, %) == {
R ==> Record(quotient: Integer, remainder: Integer);
r: R := divide(rep x, rep y);
(per(r.quotient), per(r.remainder));
}
(x: %)^(i: I): % == x^(i :: NonNegativeInteger);
Uses I 47, Integer 66, and Z 47.
583⟨exports of Integer from LibAxiom 583⟩≡ (581a)
IntegralDomain;
IntegerNumberSystem;
ConvertibleTo(String);
OpenMath;
random: (%) -> %;
canonical @ Category;
canonicalsClosed @ Category;
noetherian @ Category;
infinite @ Category;
integer: Literal -> %;
-: % -> %;
+: (%, %) -> %;
-: (%, %) -> %;
*: (%, %) -> %;
=: (%, %) -> Boolean;
<: (%, %) -> Boolean;
<=: (%, %) -> Boolean;
>: (%, %) -> Boolean;
>=: (%, %) -> Boolean;
coerce: SingleInteger -> %;
coerce: Integer -> %;
coerce: % -> Integer;
coerce: % -> %;
one: () -> %;
zero: () -> %;
zero?: % -> Boolean;
1: %;
0: %;
quo: (%, %) -> %;
rem: (%, %) -> %;
export from UniversalSegment(%);
Uses Integer 66 and String 65.
22.1.4 ACMachineInteger
584⟨dom: ACMachineInteger 584⟩≡ (569a)
ACMachineInteger: with {
ACLabelType;
coerce: % -> Integer;
coerce: % -> ACInteger;
coerce: % -> SingleInteger;
coerce: SingleInteger -> %;
coerce: % -> NNI;
coerce: NNI -> %;
⟨exports of SingleInteger from LibAldor 585a⟩
⟨exports of SingleInteger from LibAxiom 586⟩
} == SingleInteger add {
Rep == SingleInteger;
import from Rep, Integer;
elements(): Generator % == generate {
for i: SingleInteger in 1 .. repeat yield per i;
}
coerce(x: %): SingleInteger == rep x;
coerce(x: SingleInteger): % == per x;
coerce(x: %): ACInteger == rep(x) :: Integer :: ACInteger;
coerce(x: %): Integer == rep(x) :: Integer;
coerce(x: Integer): % == per(x::SingleInteger);
coerce(x: %): NNI == rep(x) :: NNI;
coerce(x: NNI): % == per(x::SingleInteger);
⟨implementation of SingleInteger from LibAldor 585b⟩
integer(l: Literal): % == (integer(l)$Rep) :: %;
}
Defines:
ACMachineInteger, used in chunks 54, 569b, 571, 588c, 589, and 591.
Uses ACInteger 581a, ACLabelType 572, Generator 617, and Integer 66.
585b⟨implementation of SingleInteger from LibAldor 585b⟩≡ (584)
(tw: TextWriter) << (x: %): TextWriter == hconcat(tw, x::OutputForm);
machine(z: ACInteger): % == z :: Integer :: %;
prev(i: %): % == dec i;
next(i: %): % == inc i;
max: % == max();
min: % == min();
divide(x: %, y: %): (%, %) == {
import from Record(quotient: %, remainder: %);
explode divide(x, y);
}
(x: %)^(y: %): % == x^(y::NonNegativeInteger);
Uses ACInteger 581a and Integer 66.
586⟨exports of SingleInteger from LibAxiom 586⟩≡ (584)
IntegerNumberSystem;
Logic;
OpenMath;
canonical @ Category;
canonicalsClosed @ Category;
noetherian @ Category;
max: () -> %;
min: () -> %;
--not: (%) -> %;
~: (%) -> %;
/\: (%, %) -> %;
\/: (%, %) -> %;
xor: (%, %) -> %;
Not: (%) -> %;
And: (%, %) -> %;
Or: (%, %) -> %;
integer: Literal -> %;
coerce: Integer -> %;
zero: () -> %;
one: () -> %;
inc: % -> %;
dec: % -> %;
leq: (%, %) -> Boolean;
spit: % -> ();
+: (%, %) -> %;
-: (%, %) -> %;
*: (%, %) -> %;
=: (%, %) -> Boolean;
~=: (%, %) -> Boolean;
>=: (%, %) -> Boolean;
<=: (%, %) -> Boolean;
>: (%, %) -> Boolean;
<: (%, %) -> Boolean;
zero?: % -> Boolean;
export from UniversalSegment(%);
1: %;
0: %;
Defines:
Or, never used.
Uses Integer 66.
22.1.5 ACSymbol
587a⟨dom: ACSymbol 587a⟩≡ (569a)
ACSymbol: with {
coerce: Symbol -> %;
coerce: % -> Symbol;
⟨exports of Symbol from LibAldor 587b⟩
⟨exports of Symbol from LibAxiom 588a⟩
} == Symbol add {
Rep == Symbol;
coerce(x: %): Symbol == rep x;
coerce(x: Symbol): % == per x;
⟨implementation of Symbol from LibAldor 587c⟩
}
Defines:
ACSymbol, used in chunk 54.
587c⟨implementation of Symbol from LibAldor 587c⟩≡ (587a)
(tw: TextWriter) << (x: %): TextWriter == hconcat(tw, x::OutputForm);
-(x: ACString): % == per(coerce(x::String)$Symbol);
name(x: %): ACString == string(rep x)$Symbol::ACString;
Uses ACString 579, name 198, and String 65.
588a⟨exports of Symbol from LibAxiom 588a⟩≡ (587a)
SetCategory;
22.1.6 ACList
588b⟨dom: ACList 588b⟩≡ (569a)
ACList(S: Type): with {
coerce: % -> List S;
coerce: List S -> %;
⟨exports of List from LibAldor 588c⟩
⟨exports of List from LibAxiom 590⟩
} == List S add {
Rep == List S;
import from Rep;
coerce(x: %): List S == rep x;
coerce(x: List S): % == per x;
⟨implementation of List from LibAldor 589⟩
}
Defines:
ACList, used in chunks 54 and 624.
589⟨implementation of List from LibAldor 589⟩≡ (588b)
if S has OutputType then {
(tw: TextWriter) << (x: %): TextWriter == {
import from S, ACString;
empty? x => tw << "[]";
tw := tw << "[";
s := first x; x := rest x; tw := tw << s;
while not empty? x repeat {
s := first x; x := rest x; tw := tw << ", " << s;
}
tw << "]";
}
}
#(x: %): I == (# rep x) :: I;
empty: % == per empty();
apply(l: %, n: ACMachineInteger): S == apply(l::List S, n::Integer);
set!(l: %, n: ACMachineInteger, s: S): S == {
(l::List S).(n::Integer) := s;
}
map(f: S -> S)(x: %): % == [f s for s in x];
setRest!(l: %, k: %): % == setrest!(l, k);
Uses ACMachineInteger 584, ACString 579, I 47, Integer 66, and OutputType 570.
Note that uncommenting ListExtendCategory makes the Axiom interpreter fail, see
Section 22.1.
590⟨exports of List from LibAxiom 590⟩≡ (588b)
--ListExtendCategory(S);
ListAggregate(S);
bracket: Tuple(S) -> %;
nil: %;
first: % -> S;
rest: % -> %;
cons: (S, %) -> %;
empty: () -> %;
empty?: % -> Boolean;
test: % -> Boolean;
setfirst!: (%, S) -> S;
setrest!: (%, %) -> %;
#: % -> NonNegativeInteger;
reverse!: % -> %;
sort: ((S, S) -> Boolean, %) -> %;
generator: % -> Generator(S);
bracket: Generator(S) -> %;
Uses Generator 617.