/usr/share/axiom-20170501/src/algebra/MAGMA.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 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 | )abbrev domain MAGMA Magma
++ Author: Michel Petitot (petitot@lifl.fr).
++ Date Created: 91
++ Date Last Updated: 7 Juillet 92
++ Fix History: compilation v 2.1 le 13 dec 98
++ Description:
++ This type is the basic representation of
++ parenthesized words (binary trees over arbitrary symbols)
++ useful in \spadtype{LiePolynomial}.
Magma(VarSet) : SIG == CODE where
VarSet : OrderedSet
WORD ==> OrderedFreeMonoid(VarSet)
EX ==> OutputForm
SIG ==> Join(OrderedSet,RetractableTo VarSet) with
"*" : ($,$) -> $
++ \axiom{x*y} returns the tree \axiom{[x,y]}.
coerce : $ -> WORD
++ \axiom{coerce(x)} returns the element of
++\axiomType{OrderedFreeMonoid}(VarSet)
++ corresponding to \axiom{x} by removing parentheses.
first : $ -> VarSet
++ \axiom{first(x)} returns the first entry of the tree \axiom{x}.
left : $ -> $
++ \axiom{left(x)} returns left subtree of \axiom{x} or
++ error if retractable?(x) is true.
length : $ -> PositiveInteger
++ \axiom{length(x)} returns the number of entries in \axiom{x}.
lexico : ($,$) -> Boolean
++ \axiom{lexico(x,y)} returns \axiom{true} iff \axiom{x} is smaller
++ than \axiom{y} w.r.t. the lexicographical ordering induced by
++ \axiom{VarSet}.
++ N.B. This operation does not take into account the tree structure of
++ its arguments. Thus this is not a total ordering.
mirror : $ -> $
++ \axiom{mirror(x)} returns the reversed word of \axiom{x}.
++ That is \axiom{x} itself if retractable?(x) is true and
++ \axiom{mirror(z) * mirror(y)} if \axiom{x} is \axiom{y*z}.
rest : $ -> $
++ \axiom{rest(x)} return \axiom{x} without the first entry or
++ error if retractable?(x) is true.
retractable? : $ -> Boolean
++ \axiom{retractable?(x)} tests if \axiom{x} is a tree with
++ only one entry.
right : $ -> $
++ \axiom{right(x)} returns right subtree of \axiom{x} or
++ error if retractable?(x) is true.
varList : $ -> List VarSet
++ \axiom{varList(x)} returns the list of distinct entries of \axiom{x}
CODE ==> add
-- representation
VWORD := Record(left:$ ,right:$)
Rep:= Union(VarSet,VWORD)
recursif: ($,$) -> Boolean
-- define
x:$ = y:$ ==
x case VarSet =>
y case VarSet => x::VarSet = y::VarSet
false
y case VWORD => x::VWORD = y::VWORD
false
varList x ==
x case VarSet => [x::VarSet]
lv: List VarSet := setUnion(varList x.left, varList x.right)
sort_!(lv)
left x ==
x case VarSet => error "x has only one entry"
x.left
right x ==
x case VarSet => error "x has only one entry"
x.right
retractable? x == (x case VarSet)
retract x ==
x case VarSet => x::VarSet
error "Not retractable"
retractIfCan x == (retractable? x => x::VarSet ; "failed")
coerce(l:VarSet):$ == l
mirror x ==
x case VarSet => x
[mirror x.right, mirror x.left]$VWORD
coerce(x:$): WORD ==
x case VarSet => x::VarSet::WORD
x.left::WORD * x.right::WORD
coerce(x:$):EX ==
x case VarSet => x::VarSet::EX
bracket [x.left::EX, x.right::EX]
x * y == [x,y]$VWORD
first x ==
x case VarSet => x::VarSet
first x.left
rest x ==
x case VarSet => error "rest$Magma: inexistant rest"
lx:$ := x.left
lx case VarSet => x.right
[rest lx , x.right]$VWORD
length x ==
x case VarSet => 1
length(x.left) + length(x.right)
recursif(x,y) ==
x case VarSet =>
y case VarSet => x::VarSet < y::VarSet
true
y case VarSet => false
x.left = y.left => x.right < y.right
x.left < y.left
lexico(x,y) == -- peut etre amelioree !!!!!!!!!!!
x case VarSet =>
y case VarSet => x::VarSet < y::VarSet
x::VarSet <= first y
y case VarSet => first x < retract y
fx:VarSet := first x ; fy:VarSet := first y
fx = fy => lexico(rest x , rest y)
fx < fy
x < y == -- recursif par longueur
lx,ly: PositiveInteger
lx:= length x ; ly:= length y
lx = ly => recursif(x,y)
lx < ly
|