Edit detail for SandBoxSum revision 4 of 14

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
  T == add
    --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"

axiom
size()$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?