/usr/share/axiom-20170501/src/algebra/SPLNODE.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 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 | )abbrev domain SPLNODE SplittingNode
++ Author: Marc Moereno Maza
++ Date Created: 07/05/1996
++ Date Last Updated: 07/19/1996
++ Description:
++ This domain exports a modest implementation for the
++ vertices of splitting trees. These vertices are called
++ here splitting nodes. Every of these nodes store 3 informations.
++ The first one is its value, that is the current expression
++ to evaluate. The second one is its condition, that is the
++ hypothesis under which the value has to be evaluated.
++ The last one is its status, that is a boolean flag
++ which is true iff the value is the result of its
++ evaluation under its condition. Two splitting vertices
++ are equal iff they have the sane values and the same
++ conditions (so their status do not matter).
SplittingNode(V,C) : SIG == CODE where
V : Join(SetCategory,Aggregate)
C : Join(SetCategory,Aggregate)
Z ==> Integer
B ==> Boolean
O ==> OutputForm
VT ==> Record(val:V, tower:C)
VTB ==> Record(val:V, tower:C, flag:B)
SIG ==> SetCategory with
empty : () -> %
++ \axiom{empty()} returns the same as
++ \axiom{[empty()$V,empty()$C,false]$%}
empty? : % -> B
++ \axiom{empty?(n)} returns true iff the node n is \axiom{empty()$%}.
value : % -> V
++ \axiom{value(n)} returns the value of the node n.
condition : % -> C
++ \axiom{condition(n)} returns the condition of the node n.
status : % -> B
++ \axiom{status(n)} returns the status of the node n.
construct : (V,C,B) -> %
++ \axiom{construct(v,t,b)} returns the non-empty node with
++ value v, condition t and flag b
construct : (V,C) -> %
++ \axiom{construct(v,t)} returns the same as
++ \axiom{construct(v,t,false)}
construct : VT -> %
++ \axiom{construct(vt)} returns the same as
++ \axiom{construct(vt.val,vt.tower)}
construct : List VT -> List %
++ \axiom{construct(lvt)} returns the same as
++ \axiom{[construct(vt.val,vt.tower) for vt in lvt]}
construct : (V, List C) -> List %
++ \axiom{construct(v,lt)} returns the same as
++ \axiom{[construct(v,t) for t in lt]}
copy : % -> %
++ \axiom{copy(n)} returns a copy of n.
setValue! : (%,V) -> %
++ \axiom{setValue!(n,v)} returns n whose value
++ has been replaced by v if it is not
++ empty, else an error is produced.
setCondition! : (%,C) -> %
++ \axiom{setCondition!(n,t)} returns n whose condition
++ has been replaced by t if it is not
++ empty, else an error is produced.
setStatus!: (%,B) -> %
++ \axiom{setStatus!(n,b)} returns n whose status
++ has been replaced by b if it is not
++ empty, else an error is produced.
setEmpty! : % -> %
++ \axiom{setEmpty!(n)} replaces n by \axiom{empty()$%}.
infLex? : (%,%,(V,V) -> B,(C,C) -> B) -> B
++ \axiom{infLex?(n1,n2,o1,o2)} returns true iff
++ \axiom{o1(value(n1),value(n2))} or
++ \axiom{value(n1) = value(n2)} and
++ \axiom{o2(condition(n1),condition(n2))}.
subNode? : (%,%,(C,C) -> B) -> B
++ \axiom{subNode?(n1,n2,o2)} returns true iff
++ \axiom{value(n1) = value(n2)} and
++ \axiom{o2(condition(n1),condition(n2))}
CODE ==> add
Rep ==> VTB
rep(n:%):Rep == n pretend Rep
per(r:Rep):% == r pretend %
empty() == per [empty()$V,empty()$C,false]$Rep
empty?(n:%) == empty?((rep n).val)$V and empty?((rep n).tower)$C
value(n:%) == (rep n).val
condition(n:%) == (rep n).tower
status(n:%) == (rep n).flag
construct(v:V,t:C,b:B) == per [v,t,b]$Rep
construct(v:V,t:C) == [v,t,false]$%
construct(vt:VT) == [vt.val,vt.tower]$%
construct(lvt:List VT) == [[vt]$% for vt in lvt]
construct(v:V,lt: List C) == [[v,t]$% for t in lt]
copy(n:%) == per copy rep n
setValue!(n:%,v:V) ==
(rep n).val := v
n
setCondition!(n:%,t:C) ==
(rep n).tower := t
n
setStatus!(n:%,b:B) ==
(rep n).flag := b
n
setEmpty!(n:%) ==
(rep n).val := empty()$V
(rep n).tower := empty()$C
n
infLex?(n1,n2,o1,o2) ==
o1((rep n1).val,(rep n2).val) => true
(rep n1).val = (rep n2).val =>
o2((rep n1).tower,(rep n2).tower)
false
subNode?(n1,n2,o2) ==
(rep n1).val = (rep n2).val =>
o2((rep n1).tower,(rep n2).tower)
false
n1:% = n2:% ==
(rep n1).val ~= (rep n2).val => false
(rep n1).tower = (rep n2).tower
n1:% ~= n2:% ==
(rep n1).val = (rep n2).val => false
(rep n1).tower ~= (rep n2).tower
coerce(n:%):O ==
l1,l2,l3,l : List O
l1 := [message("value == "), ((rep n).val)::O]
o1 : O := blankSeparate l1
l2 := [message(" tower == "), ((rep n).tower)::O]
o2 : O := blankSeparate l2
if ((rep n).flag)
then
o3 := message(" closed == true")
else
o3 := message(" closed == false")
l := [o1,o2,o3]
bracket commaSeparate l
|