|
|
last edited 16 years ago by Bill Page |
1 2 3 4 | ||
Editor: Bill Page
Time: 2008/07/27 02:58:28 GMT-7 |
||
Note: Literals and Symbols in Axiom |
changed: - Literals and Symbols in Axiom I think Axiom needs a 'Literal' domain that works in a manner 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:: (1) -> 2 (1) 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}
I think Axiom needs a Literal
domain that works in a
manner the Aldor language. SPAD and the Axiom interpreter
should not automatically treat a constant like 2
is a
PositiveInteger
.
axiom2
(1) |
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:
(1) -> 2 <a href="#eq1">(1)</a> 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
axiom2+3
(2) |
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.
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; }
Compiling FriCAS source code from file /var/zope2/var/LatexWiki/7096130453832849089-25px003.as using AXIOM-XL compiler and options -O -Fasy -Fao -Flsp -laxiom -Mno-AXL_W_WillObsolete -DAxiom -Y $AXIOM/algebra Use the system command )set compiler args to change these options. #1 (Warning) Deprecated message prefix: use `ALDOR_' instead of `_AXL' Compiling Lisp source code from file ./7096130453832849089-25px003.lsp Issuing )library command for 7096130453832849089-25px003 Reading /var/zope2/var/LatexWiki/7096130453832849089-25px003.asy Integer is now explicitly exposed in frame initial Integer will be automatically loaded when needed from /var/zope2/var/LatexWiki/7096130453832849089-25px003 List is now explicitly exposed in frame initial List will be automatically loaded when needed from /var/zope2/var/LatexWiki/7096130453832849089-25px003 Float is now explicitly exposed in frame initial Float will be automatically loaded when needed from /var/zope2/var/LatexWiki/7096130453832849089-25px003 PositiveInteger is now explicitly exposed in frame initial PositiveInteger will be automatically loaded when needed from /var/zope2/var/LatexWiki/7096130453832849089-25px003 DoubleFloat is now explicitly exposed in frame initial DoubleFloat will be automatically loaded when needed from /var/zope2/var/LatexWiki/7096130453832849089-25px003 String is now explicitly exposed in frame initial String will be automatically loaded when needed from /var/zope2/var/LatexWiki/7096130453832849089-25px003 NonNegativeInteger is now explicitly exposed in frame initial NonNegativeInteger will be automatically loaded when needed from /var/zope2/var/LatexWiki/7096130453832849089-25px003 SingleInteger is now explicitly exposed in frame initial SingleInteger will be automatically loaded when needed from /var/zope2/var/LatexWiki/7096130453832849089-25px003 Symbol is now explicitly exposed in frame initial Symbol will be automatically loaded when needed from /var/zope2/var/LatexWiki/7096130453832849089-25px003 integer is now explicitly exposed in frame initial integer will be automatically loaded when needed from /var/zope2/var/LatexWiki/7096130453832849089-25px003