/usr/share/axiom-20170501/src/algebra/UNISEG.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 125 126 127 | )abbrev domain UNISEG UniversalSegment
++ Author: Robert S. Sutor
++ Date Created: 1987
++ Date Last Updated: June 4, 1991
++ Description:
++ This domain provides segments which may be half open.
++ That is, ranges of the form \spad{a..} or \spad{a..b}.
UniversalSegment(S) : SIG == CODE where
S : Type
SIG ==> SegmentCategory(S) with
SEGMENT : S -> %
++ \spad{l..} produces a half open segment,
++ that is, one with no upper bound.
segment : S -> %
++ segment(l) is an alternate way to construct the segment \spad{l..}.
coerce : Segment S -> %
++ coerce(x) allows \spadtype{Segment} values to be used as %.
hasHi : % -> Boolean
++ hasHi(s) tests whether the segment s has an upper bound.
if S has SetCategory then SetCategory
if S has OrderedRing then
SegmentExpansionCategory(S, Stream S)
CODE ==> add
Rec ==> Record(low: S, high: S, incr: Integer)
Rec2 ==> Record(low: S, incr: Integer)
SEG ==> Segment S
Rep := Union(Rec2, Rec)
a,b : S
s : %
i: Integer
ls : List %
segment a == [a, 1]$Rec2 :: Rep
segment(a,b) == [a,b,1]$Rec :: Rep
BY(s,i) ==
s case Rec => [lo s, hi s, i]$Rec ::Rep
[lo s, i]$Rec2 :: Rep
lo s ==
s case Rec2 => (s :: Rec2).low
(s :: Rec).low
low s ==
s case Rec2 => (s :: Rec2).low
(s :: Rec).low
hasHi s == s case Rec
hi s ==
not hasHi(s) => error "hi: segment has no upper bound"
(s :: Rec).high
high s ==
not hasHi(s) => error "high: segment has no upper bound"
(s :: Rec).high
incr s ==
s case Rec2 => (s :: Rec2).incr
(s :: Rec).incr
SEGMENT(a) == segment a
SEGMENT(a,b) == segment(a,b)
coerce(sg : SEG): % == segment(lo sg, hi sg)
convert a == [a,a,1]
if S has SetCategory then
(s1:%) = (s2:%) ==
s1 case Rec2 =>
s2 case Rec2 =>
s1.low = s2.low and s1.incr = s2.incr
false
s1 case Rec =>
s2 case Rec =>
s2.low = s2.low and s1.high=s2.high and s1.incr=s2.incr
false
false
coerce(s: %): OutputForm ==
seg :=
e := (lo s)::OutputForm
hasHi s => SEGMENT(e, (hi s)::OutputForm)
SEGMENT e
inc := incr s
inc = 1 => seg
infix(" by "::OutputForm, seg, inc::OutputForm)
if S has OrderedRing then
expand(s:%) == expand([s])
map(f:S->S, s:%) == map(f, expand s)
plusInc(t: S, a: S): S == t + a
expand(ls: List %):Stream S ==
st:Stream S := empty()
null ls => st
lb:List(Segment S) := nil()
while not null ls and hasHi first ls repeat
s := first ls
ls := rest ls
ns := BY(SEGMENT(lo s, hi s), incr s)$Segment(S)
lb := concat_!(lb,ns)
if not null ls then
s := first ls
st: Stream S := generate(x +-> x+incr(s)::S, lo s)
else
st: Stream S := empty()
concat(construct expand(lb), st)
|