login  home  contents  what's new  discussion  bug reports help  links  subscribe  changes  refresh  edit

# Edit detail for SandBoxSum revision 4 of 14

 1 2 3 4 5 6 7 8 9 10 11 12 13 14 Editor: Bill Page Time: 2008/05/16 19:01:42 GMT-7 Note: Sum is dual to Product

```changed:
-       Rep := Union(acomp:A,bcomp:B)
Rep == Union(acomp:A,bcomp:B)
import Rep

changed:
-       coerce(x):OutputForm ==
-         x case acomp => (x.acomp)::OutputForm
-         (x.bcomp)::OutputForm
-       x=y == rep(x)= rep(y)
coerce(x:%):OutputForm == coerce(rep(x))\$Rep
x=y == rep(x)=rep(y)

changed:
-       makefirst(a:A) : %   == per construct(a)\$REP
-       makesecond (b:B) : % == per construct(b)\$REP
makefirst(a)   == per [a]
makesecond(b:B) : % == per [b]

changed:
-          1 == per construct(1\$A)\$REP
1 == per [1\$A]

changed:
-                   x case acomp and y case acomp => per construct(rep(x).acomp * rep(y).acomp)\$REP
-                   x case bcomp and y case bcomp => per construct(rep(x).bcomp * rep(y).bcomp)\$REP
rep(x) case acomp and rep(y) case acomp => per [rep(x).acomp * rep(y).acomp]
rep(x) case bcomp and rep(y) case bcomp => per [rep(x).bcomp * rep(y).bcomp]

changed:
-                   x case acomp and x.acomp=1\$A and y case bcomp => y
rep(x) case acomp and rep(x).acomp=1\$A and rep(y) case bcomp => y

changed:
-                   x case acomp => per construct(rep(x).acomp ** p)\$REP
-                   per construct(rep(x).bcomp ** p)\$REP
rep(x) case acomp => per [rep(x).acomp ** p]
per [rep(x).bcomp ** p]

changed:
-                      n > size\$B => per construct(index((n::Integer - size\$B)::PositiveInteger)\$A)\$REP
-                      per construct(index(n)\$B)\$REP
n > size\$B => per [index((n::Integer - size\$B)::PositiveInteger)\$A]
per [index(n)\$B]

changed:
-                      random()\$Boolean => per construct(random()\$A)\$REP
-                      per construct(random()\$B)REP
random()\$Boolean => per [random()\$A]
per [random()\$B]

changed:
-                    x case acomp => per construct(inv(x.acomp))\$REP
-                    per construct(inv(x.bcomp))\$REP
x case acomp => per [inv(x.acomp)]
per [inv(x.bcomp)]

changed:
-          0 == per construct(1\$A)\$REP
0 == per [1\$A]

changed:
-                   x case acomp and y case acomp => per construct(rep(x).acomp + rep(y).acomp)\$REP
-                   x case bcomp and y case bcomp => per construct(rep(x).bcomp + rep(y).bcomp)\$REP
rep(x) case acomp and rep(y) case acomp => per [rep(x).acomp + rep(y).acomp]
rep(x) case bcomp and rep(y) case bcomp => per [rep(x).bcomp + rep(y).bcomp]

changed:
-                   x case acomp and x.acomp=1\$A and y case bcomp => y
rep(x) case acomp and rep(x).acomp=1\$A and rep(y) case bcomp => y

changed:
-                   x case acomp => per construct(c * rep(x).acomp)\$REP
-                   per construct(c* rep(x).bcomp)\$REP
x case acomp => per [c * rep(x).acomp]
per [c* rep(x).bcomp]

changed:
-                   x case acomp and y case acomp => per construct(rep(x).acomp - rep(y).acomp)\$REP
-                   x case bcomp and y case bcomp => per construct(rep(x).bcomp - rep(y).bcomp)\$REP
x case acomp and y case acomp => per [rep(x).acomp - rep(y).acomp]
x case bcomp and y case bcomp => per [rep(x).bcomp - rep(y).bcomp]

changed:
-                   x case acomp => per construct(d * rep(x).acomp)\$REP
-                   per construct(d* rep(x).bcomp)\$REP
x case acomp => per [d * rep(x).acomp]
per [d* rep(x).bcomp]

changed:
-                   x case acomp and y case acomp => per construct(sup(rep(x).acomp,rep(y).acomp))\$REP
-                   x case bcomp and y case bcomp => per construct(sup(rep(x).bcomp,rep(y).bcomp))\$REP
x case acomp and y case acomp => per [sup(rep(x).acomp,rep(y).acomp)]
x case bcomp and y case bcomp => per [sup(rep(x).bcomp,rep(y).bcomp)]
```

The Sum domain constructor is intended to be the CategoricalDual? of the Product domain constructor

```spad)abbrev domain SUM Sum
++ Description:
++ This domain implements direct union
Sum (A:SetCategory,B:SetCategory) : C == T
where
C == SetCategory  with
if A has Finite and B has Finite then Finite
if A has Monoid and B has Monoid then Monoid
if A has AbelianMonoid and B has AbelianMonoid then AbelianMonoid
if A has CancellationAbelianMonoid and
B has CancellationAbelianMonoid then CancellationAbelianMonoid
if A has Group  and B has Group  then  Group
if A has AbelianGroup and B has AbelianGroup then  AbelianGroup
if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup
then OrderedAbelianMonoidSup
if A has OrderedSet and B has OrderedSet then  OrderedSet
selectsum     : % -> Union(acomp:A,bcomp:B)
++ selectsum(x) \undocumented
makefirst  :   A -> %
++ makefirst(a) \undocumented
makesecond :   B -> %
++ makesecond(b) \undocumented
--representations
Rep == Union(acomp:A,bcomp:B)
import Rep
--declarations
x,y: %
i: NonNegativeInteger
p: NonNegativeInteger
a: A
b: B
d: Integer
--define
coerce(x:%):OutputForm == coerce(rep(x))\$Rep
x=y == rep(x)=rep(y)
selectsum(x:%) == rep(x)
makefirst(a)   == per [a]
makesecond(b:B) : % == per [b]
if A has Monoid and B has Monoid then
-- represent unit of Sum(A,B) as 1\$A (We could use either 1\$A or 1\$B)
1 == per [1\$A]
x * y ==
rep(x) case acomp and rep(y) case acomp => per [rep(x).acomp * rep(y).acomp]
rep(x) case bcomp and rep(y) case bcomp => per [rep(x).bcomp * rep(y).bcomp]
-- unit of Sum(A,B)=1\$A is unit for B
rep(x) case acomp and rep(x).acomp=1\$A and rep(y) case bcomp => y
error "not same type"
x ** p ==
rep(x) case acomp => per [rep(x).acomp ** p]
per [rep(x).bcomp ** p]
if A has Finite and B has Finite then
size == size\$A + size\$B
index(n) ==
n > size\$B => per [index((n::Integer - size\$B)::PositiveInteger)\$A]
per [index(n)\$B]
random() ==
random()\$Boolean => per [random()\$A]
per [random()\$B]
lookup(x) ==
x case acomp => lookup(x.acomp)\$A + size\$B::Integer
lookup(x.bcomp)\$B
hash(x) ==
x case acomp => hash(x.acomp)\$A + size\$B::SingleInteger
hash(x.bcomp)\$B
if A has Group and B has Group then
inv(x) ==
x case acomp => per [inv(x.acomp)]
per [inv(x.bcomp)]
if A has AbelianMonoid and B has AbelianMonoid then
-- represent zero of Sum(A,B) as 0\$A (We could use either 0\$A or 0\$B)
0 == per [1\$A]
x + y ==
rep(x) case acomp and rep(y) case acomp => per [rep(x).acomp + rep(y).acomp]
rep(x) case bcomp and rep(y) case bcomp => per [rep(x).bcomp + rep(y).bcomp]
-- zero of Sum(A,B)=0\$A is zero for B
rep(x) case acomp and rep(x).acomp=1\$A and rep(y) case bcomp => y
error "not same type"
c * x ==
x case acomp => per [c * rep(x).acomp]
per [c* rep(x).bcomp]
if A has AbelianGroup and B has AbelianGroup then
- x ==
x case acomp => per(- rep(x).acomp)
per(- rep(x).bcomp)
(x - y):% ==
x case acomp and y case acomp => per [rep(x).acomp - rep(y).acomp]
x case bcomp and y case bcomp => per [rep(x).bcomp - rep(y).bcomp]
-- zero of Sum(A,B)=0\$A is zero for B
x case acomp and x.acomp=0\$A and y case bcomp => - y
x case acomp and y.bcomp=0\$A and y case bcomp => y
error "not same type"
d * x ==
x case acomp => per [d * rep(x).acomp]
per [d* rep(x).bcomp]
if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup then
sup(x,y) == [sup(x.acomp,y.acomp),sup(x.bcomp,y.bcomp)]
x case acomp and y case acomp => per [sup(rep(x).acomp,rep(y).acomp)]
x case bcomp and y case bcomp => per [sup(rep(x).bcomp,rep(y).bcomp)]
error "not same type"
if A has OrderedSet and B has OrderedSet then
x < y ==
x case acomp and y case acomp => rep(x).acomp < rep(y).acomp
x case bcomp and y case bcomp => rep(x).bcomp < rep(y).bcomp
error "not same type"```
```   Compiling OpenAxiom source code from file
SUM abbreviates domain Sum
------------------------------------------------------------------------
initializing NRLIB SUM for Sum
compiling into NRLIB SUM
compiling local rep : % -> Union(acomp: A,bcomp: B)
SUM;rep is replaced by G1410
Time: 0.01 SEC.
compiling local per : Union(acomp: A,bcomp: B) -> %
SUM;per is replaced by G1410
Time: 0 SEC.
importing Rep
compiling exported coerce : % -> OutputForm
Time: 0 SEC.
compiling exported = : (%,%) -> Boolean
Time: 0 SEC.
compiling exported selectsum : % -> Union(acomp: A,bcomp: B)
Time: 0 SEC.
compiling exported makefirst : A -> %
Time: 0 SEC.
compiling exported makesecond : B -> %
Time: 0 SEC.
****** Domain: A already in scope
augmenting A: (Monoid)
****** Domain: B already in scope
augmenting B: (Monoid)
compiling exported One : () -> %
Time: 0.01 SEC.
compiling exported * : (%,%) -> %
Time: 0.07 SEC.
compiling exported ** : (%,NonNegativeInteger) -> %
Time: 0.01 SEC.
****** Domain: A already in scope
augmenting A: (Finite)
****** Domain: B already in scope
augmenting B: (Finite)
compiling exported size : () -> NonNegativeInteger
Time: 0.01 SEC.
compiling exported index : PositiveInteger -> %
Time: 0 SEC.
compiling exported random : () -> %
Time: 0 SEC.
compiling exported lookup : % -> PositiveInteger
****** comp fails at level 2 with expression: ******
error in function lookup
(IF | << | (|case| |x| |acomp|) | >> |
(+ ((|elt| A |lookup|) (|x| |acomp|))
(|::| (|elt| B |size|) (|Integer|)))
((|elt| B |lookup|) (|x| |bcomp|)))
****** level 2  ******
\$x:= (case x acomp)
\$m:= (Boolean)
\$f:=
((((|x| # . #0=(#)) (|\$Information| #) (B # . #35=(#))
(~= # . #48=(# #)) ...)
((|per| #) (|rep| #))
((|rep| #) (|case| # . #228=(# #)) (|elt| # . #237=(# #))
(|construct| # . #242=(# #)) ...)))
>> Apparent user error:
acomp
is an unknown mode```

```axiomsize()\$Sum(PF 7,PF 13)
Sum is an unknown constructor and so is unavailable. Did you mean to
use -> but type something different instead?
size()\$Sum(PF 7,Product(PF 3,PF 13))
Sum is an unknown constructor and so is unavailable. Did you mean to
use -> but type something different instead?```