/usr/share/axiom-20170501/src/algebra/ONECOMP.spad is in axiom-source 20170501-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 | )abbrev domain ONECOMP OnePointCompletion
++ Author: Manuel Bronstein
++ Date Created: 4 Oct 1989
++ Date Last Updated: 1 Nov 1989
++ Description:
++ Completion with infinity.
++ Adjunction of a complex infinity to a set.
OnePointCompletion(R) : SIG == CODE where
R : SetCategory
B ==> Boolean
SIG ==> Join(SetCategory, FullyRetractableTo R) with
infinity : () -> %
++ infinity() returns infinity.
finite? : % -> B
++ finite?(x) tests if x is finite.
infinite?: % -> B
++ infinite?(x) tests if x is infinite.
if R has AbelianGroup then AbelianGroup
if R has OrderedRing then OrderedRing
if R has IntegerNumberSystem then
rational? : % -> Boolean
++ rational?(x) tests if x is a finite rational number.
rational : % -> Fraction Integer
++ rational(x) returns x as a finite rational number.
++ Error: if x is not a rational number.
rationalIfCan : % -> Union(Fraction Integer, "failed")
++ rationalIfCan(x) returns x as a finite rational number if
++ it is one, "failed" otherwise.
CODE ==> add
Rep := Union(R, "infinity")
coerce(r:R):% == r
retract(x:%):R == (x case R => x::R; error "Not finite")
finite? x == x case R
infinite? x == x case "infinity"
infinity() == "infinity"
retractIfCan(x:%):Union(R, "failed") == (x case R => x::R; "failed")
coerce(x:%):OutputForm ==
x case "infinity" => "infinity"::OutputForm
x::R::OutputForm
x = y ==
x case "infinity" => y case "infinity"
y case "infinity" => false
x::R = y::R
if R has AbelianGroup then
0 == 0$R
n:Integer * x:% ==
x case "infinity" =>
zero? n => error "Undefined product"
infinity()
n * x::R
- x ==
x case "infinity" => error "Undefined inverse"
- (x::R)
x + y ==
x case "infinity" => x
y case "infinity" => y
x::R + y::R
if R has OrderedRing then
fininf: R -> %
1 == 1$R
characteristic() == characteristic()$R
fininf r ==
zero? r => error "Undefined product"
infinity()
x:% * y:% ==
x case "infinity" =>
y case "infinity" => y
fininf(y::R)
y case "infinity" => fininf(x::R)
x::R * y::R
recip x ==
x case "infinity" => 0
zero?(x::R) => infinity()
(u := recip(x::R)) case "failed" => "failed"
u::R::%
x < y ==
x case "infinity" => false -- do not change the order
y case "infinity" => true -- of those two tests
x::R < y::R
if R has IntegerNumberSystem then
rational? x == finite? x
rational x == rational(retract(x)@R)
rationalIfCan x ==
(r:= retractIfCan(x)@Union(R,"failed")) case "failed" =>"failed"
rational(r::R)
|