/usr/share/axiom-20170501/src/algebra/UDPO.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 | )abbrev package UDPO UserDefinedPartialOrdering
++ Author: Manuel Bronstein
++ Date Created: March 1990
++ Date Last Updated: 9 April 1991
++ Description:
++ Provides functions to force a partial ordering on any set.
UserDefinedPartialOrdering(S) : SIG == CODE where
S : SetCategory
SIG ==> with
setOrder : List S -> Void
++ setOrder([a1,...,an]) defines a partial ordering on S given by:
++ (1) \spad{a1 < a2 < ... < an}.
++ (2) \spad{b < ai for i = 1..n} and b not among the ai's.
++ (3) undefined on \spad{(b, c)} if neither is among the ai's.
setOrder : (List S, List S) -> Void
++ setOrder([b1,...,bm], [a1,...,an]) defines a partial
++ ordering on S given by:
++ (1) \spad{b1 < b2 < ... < bm < a1 < a2 < ... < an}.
++ (2) \spad{bj < c < ai} for c not among the ai's and bj's.
++ (3) undefined on \spad{(c,d)} if neither is among the ai's,bj's.
getOrder : () -> Record(low: List S, high: List S)
++ getOrder() returns \spad{[[b1,...,bm], [a1,...,an]]} such that the
++ partial ordering on S was given by
++ \spad{setOrder([b1,...,bm],[a1,...,an])}.
less? : (S, S) -> Union(Boolean, "failed")
++ less?(a, b) compares \spad{a} and b in the partial ordering induced by
++ setOrder.
less? : (S, S, (S, S) -> Boolean) -> Boolean
++ less?(a, b, fn) compares \spad{a} and b in the partial ordering induced
++ by setOrder, and returns \spad{fn(a, b)} if \spad{a}
++ and b are not comparable
++ in that ordering.
largest : (List S, (S, S) -> Boolean) -> S
++ largest(l, fn) returns the largest element of l where the partial
++ ordering induced by setOrder is completed into a total one by fn.
userOrdered? : () -> Boolean
++ userOrdered?() tests if the partial ordering induced by
++ setOrder is not empty.
if S has OrderedSet then
largest : List S -> S
++ largest l returns the largest element of l where the partial
++ ordering induced by setOrder is completed into a total one by
++ the ordering on S.
more? : (S, S) -> Boolean
++ more?(a, b) compares a and b in the partial ordering induced
++ by setOrder, and uses the ordering on S if a and b are not
++ comparable in the partial ordering.
CODE ==> add
llow :Reference List S := ref nil()
lhigh:Reference List S := ref nil()
userOrdered?() == not(empty? deref llow) or not(empty? deref lhigh)
getOrder() == [deref llow, deref lhigh]
setOrder l == setOrder(nil(), l)
setOrder(l, h) ==
setref(llow, removeDuplicates l)
setref(lhigh, removeDuplicates h)
void
less?(a, b, f) ==
(u := less?(a, b)) case "failed" => f(a, b)
u::Boolean
largest(x, f) ==
empty? x => error "largest: empty list"
empty? rest x => first x
a := largest(rest x, f)
less?(first x, a, f) => a
first x
less?(a, b) ==
for x in deref llow repeat
x = a => return(a ^= b)
x = b => return false
aa := bb := false$Boolean
for x in deref lhigh repeat
if x = a then
bb => return false
aa := true
if x = b then
aa => return(a ^= b)
bb := true
aa => false
bb => true
"failed"
if S has OrderedSet then
more?(a, b) == not less?(a, b, (y,z) +-> y <$S z)
largest x == largest(x, (y,z) +-> y <$S z)
|