Edit detail for SandBoxSum revision 7 of 14

The Sum domain constructor is intended to be the Categorical Dual of the Product domain constructor

)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
       c: PositiveInteger
       d: Integer

    --define
       coerce(x:%):OutputForm == coerce(rep(x))$Rep
       x=y == rep(x)=rep(y)
       selectsum(x:%) == rep(x)
       makefirst(a: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) ==
                      rep(x) case acomp => (lookup(rep(x).acomp)$A::NonNegativeInteger + size$B)::PositiveInteger
                      lookup(rep(x).bcomp)$B
          hash(x) ==
                      rep(x) case acomp => hash(rep(x).acomp)$A + size$B::SingleInteger
                      hash(rep(x).bcomp)$B

       if A has Group and B has Group then
          inv(x) ==
                    rep(x) case acomp => per [inv(rep(x).acomp)]
                    per [inv(rep(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 [0$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 x=0 and rep(y) case bcomp => y
                   rep(x) case bcomp and y=0 and rep(y) case acomp => x
                   error "not same type"
          c * x ==
                   rep(x) case acomp => per [c * rep(x).acomp]
                   per [c* rep(x).bcomp]

       if A has AbelianGroup and B has AbelianGroup then
          - x ==
                 rep(x) case acomp => per [- rep(x).acomp]
                 per [- rep(x).bcomp]
          (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 x=0 and rep(y) case bcomp => - y
                   rep(x) case bcomp and y=0 and rep(y) case acomp => x
                   error "not same type"

          d * x ==
                   rep(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) ==
                   rep(x) case acomp and rep(y) case acomp => per [sup(rep(x).acomp,rep(y).acomp)]
                   rep(x) case bcomp and rep(y) case bcomp => per [sup(rep(x).bcomp,rep(y).bcomp)]
                   rep(x) case acomp and rep(y) case bcomp => y
                   x

       if A has OrderedSet and B has OrderedSet then
          x < y ==
                   rep(x) case acomp and rep(y) case acomp => rep(x).acomp < rep(y).acomp
                   rep(x) case bcomp and rep(y) case bcomp => rep(x).bcomp < rep(y).bcomp
                   rep(x) case acomp and rep(y) case bcomp => true
                   false

   Compiling OpenAxiom source code from file 
      /var/zope2/var/LatexWiki/2909875847865617877-25px001.spad using 
      Spad compiler.
   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 G1435 
Time: 0.02 SEC.

   compiling local per : Union(acomp: A,bcomp: B) -> %
      SUM;per is replaced by G1435 
Time: 0 SEC.

   importing Rep
   compiling exported coerce : % -> OutputForm
Time: 0.01 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.06 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
Time: 0.01 SEC.

   compiling exported hash : % -> SingleInteger
Time: 0.01 SEC.

****** Domain: A already in scope
augmenting A: (Group)
****** Domain: B already in scope
augmenting B: (Group)
   compiling exported inv : % -> %
Time: 0.01 SEC.

****** Domain: A already in scope
augmenting A: (AbelianMonoid)
****** Domain: B already in scope
augmenting B: (AbelianMonoid)
   compiling exported Zero : () -> %
Time: 0 SEC.

   compiling exported + : (%,%) -> %
Time: 0.01 SEC.

   compiling exported * : (PositiveInteger,%) -> %
Time: 0.07 SEC.

****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
   compiling exported - : % -> %
Time: 0.01 SEC.

   compiling exported - : (%,%) -> %
Time: 0.02 SEC.

   compiling exported * : (Integer,%) -> %
Time: 0.01 SEC.

****** Domain: A already in scope
augmenting A: (OrderedAbelianMonoidSup)
****** Domain: B already in scope
augmenting B: (OrderedAbelianMonoidSup)
   compiling exported sup : (%,%) -> %
Time: 0.02 SEC.

****** Domain: A already in scope
augmenting A: (OrderedSet)
****** Domain: B already in scope
augmenting B: (OrderedSet)
   compiling exported < : (%,%) -> Boolean
Time: 0.01 SEC.

****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
****** Domain: A already in scope
augmenting A: (Finite)
****** Domain: B already in scope
augmenting B: (Finite)
****** Domain: A already in scope
augmenting A: (Group)
****** Domain: B already in scope
augmenting B: (Group)
****** Domain: A already in scope
augmenting A: (OrderedAbelianMonoidSup)
****** Domain: B already in scope
augmenting B: (OrderedAbelianMonoidSup)
****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
****** Domain: A already in scope
augmenting A: (AbelianGroup)
****** Domain: B already in scope
augmenting B: (AbelianGroup)
****** Domain: A already in scope
augmenting A: (Group)
****** Domain: B already in scope
augmenting B: (Group)
****** Domain: A already in scope
augmenting A: (OrderedAbelianMonoidSup)
****** Domain: B already in scope
augmenting B: (OrderedAbelianMonoidSup)
(time taken in buildFunctor:  2)

;;;     ***       |Sum| REDEFINED

;;;     ***       |Sum| REDEFINED
Time: 0.09 SEC.

   Warnings: 
      [1] *:  acomp has no value
      [2] *:  bcomp has no value
      [3] **:  acomp has no value
      [4] **:  bcomp has no value
      [5] lookup:  acomp has no value
      [6] lookup:  bcomp has no value
      [7] hash:  acomp has no value
      [8] hash:  bcomp has no value
      [9] inv:  acomp has no value
      [10] inv:  bcomp has no value
      [11] +:  acomp has no value
      [12] +:  bcomp has no value
      [13] -:  acomp has no value
      [14] -:  bcomp has no value
      [15] sup:  acomp has no value
      [16] sup:  bcomp has no value
      [17] <:  acomp has no value
      [18] <:  bcomp has no value

   Cumulative Statistics for Constructor Sum
      Time: 0.39 seconds

   finalizing NRLIB SUM 
   Processing Sum for Browser database:
     -- selectsum : % -> Union(acomp: A,bcomp: B)
--->-->Sum((selectsum ((Union (: acomp A) (: bcomp B)) %))): Unexpected HT command: \spad
"\\spad{selectsum(x)} \\undocumented"
     -- makefirst : A -> %
--->-->Sum((makefirst (% A))): Unexpected HT command: \spad
"\\spad{makefirst(a)} \\undocumented"
     -- makesecond : B -> %
--->-->Sum((makesecond (% B))): Unexpected HT command: \spad
"\\spad{makesecond(b)} \\undocumented"
     -- constructor
------------------------------------------------------------------------
   Sum is now explicitly exposed in frame initial 
   Sum will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/SUM.NRLIB/code.o

size()$Sum(PF 7,PF 13)

(1)

size()$Sum(PF 7,Product(PF 3,PF 13))

(2)

makefirst(10)$Sum(Integer,Integer)

(3)

makefirst(10)$Sum(Integer,Integer)<makesecond(10)$Sum(Integer,Integer)

(4)

sup(makefirst(99)$Sum(NNI,NNI),makesecond(10)$Sum(NNI,NNI))

(5)