/usr/share/axiom-20170501/src/algebra/GTSET.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 | )abbrev domain GTSET GeneralTriangularSet
++ Author: Marc Moreno Maza (marc@nag.co.uk)
++ Date Created: 10/06/1995
++ Date Last Updated: 06/12/1996
++ References :
++ [1] P. AUBRY, D. LAZARD and M. MORENO MAZA "On the Theories
++ of Triangular Sets" Journal of Symbol. Comp. (to appear)
++ Description:
++ A domain constructor of the category \axiomType{TriangularSetCategory}.
++ The only requirement for a list of polynomials to be a member of such
++ a domain is the following: no polynomial is constant and two distinct
++ polynomials have distinct main variables. Such a triangular set may
++ not be auto-reduced or consistent. Triangular sets are stored
++ as sorted lists w.r.t. the main variables of their members but they
++ are displayed in reverse order.
GeneralTriangularSet(R,E,V,P) : SIG == CODE where
R : IntegralDomain
E : OrderedAbelianMonoidSup
V : OrderedSet
P : RecursivePolynomialCategory(R,E,V)
N ==> NonNegativeInteger
Z ==> Integer
B ==> Boolean
LP ==> List P
PtoP ==> P -> P
SIG ==> TriangularSetCategory(R,E,V,P)
CODE ==> add
Rep ==> LP
rep(s:$):Rep == s pretend Rep
per(l:Rep):$ == l pretend $
copy ts ==
per(copy(rep(ts))$LP)
empty() ==
per([])
empty?(ts:$) ==
empty?(rep(ts))
parts ts ==
rep(ts)
members ts ==
rep(ts)
map (f : PtoP, ts : $) : $ ==
construct(map(f,rep(ts))$LP)$$
map! (f : PtoP, ts : $) : $ ==
construct(map!(f,rep(ts))$LP)$$
member? (p,ts) ==
member?(p,rep(ts))$LP
unitIdealIfCan() ==
"failed"::Union($,"failed")
roughUnitIdeal? ts ==
false
-- the following assume that rep(ts) is decreasingly sorted
-- w.r.t. the main variavles of the polynomials in rep(ts)
coerce(ts:$) : OutputForm ==
lp : List(P) := reverse(rep(ts))
brace([p::OutputForm for p in lp]$List(OutputForm))$OutputForm
mvar ts ==
empty? ts => error"failed in mvar : $ -> V from GTSET"
mvar(first(rep(ts)))$P
first ts ==
empty? ts => "failed"::Union(P,"failed")
first(rep(ts))::Union(P,"failed")
last ts ==
empty? ts => "failed"::Union(P,"failed")
last(rep(ts))::Union(P,"failed")
rest ts ==
empty? ts => "failed"::Union($,"failed")
per(rest(rep(ts)))::Union($,"failed")
coerce(ts:$) : (List P) ==
rep(ts)
collectUpper (ts,v) ==
empty? ts => ts
lp := rep(ts)
newlp : Rep := []
while (not empty? lp) and (mvar(first(lp)) > v) repeat
newlp := cons(first(lp),newlp)
lp := rest lp
per(reverse(newlp))
collectUnder (ts,v) ==
empty? ts => ts
lp := rep(ts)
while (not empty? lp) and (mvar(first(lp)) >= v) repeat
lp := rest lp
per(lp)
-- for another domain of TSETCAT build on this domain GTSET
-- the following operations must be redefined
extendIfCan(ts:$,p:P) ==
ground? p => "failed"::Union($,"failed")
empty? ts => (per([unitCanonical(p)]$LP))::Union($,"failed")
not (mvar(ts) < mvar(p)) => "failed"::Union($,"failed")
(per(cons(p,rep(ts))))::Union($,"failed")
|