Re: [Axiom-developer] Unions in Spad

[Ralf Hemmecke]

See below...

> > Try this:  testu2.spad
> > -------
> > )abbrev domain BAR Bar
> >
> > Bar() : Exp == Impl where
> >    Exp == with
> >      inj1 : Integer -> %
> >      inj2 : Integer -> %
> >      prj : % -> Integer
> >    Impl == add
> >      Rep := Union(tag1: Integer, tag2: Integer)
> >      inj1 (n : Integer) : % == [n]
> >      inj2 (s : Integer) : % == [2*s]
> >      prj p == (p::Rep).tag1
> > -------
> > After compiling,
> >
> > (4) -> i1:= inj1 1
> >
> >  LISP output:
> > (0 . 1)
> >                                                                     Type: Bar
> > (5) -> i2:= inj2 1
> >
> >  LISP output:
> > (0 . 2)
> >                                                                     Type: Bar
> > (6) -> prj i1
> >
> >    (6)  1
> >                                                         Type: PositiveInteger
> > (7) -> prj i2
> >
> >    (7)  2
> >                                                         Type: PositiveInteger
>
> > Note the answer is even *correct*! Axiom should have signaled a failure or 
> > error.

In Aldor you would have written that as

---BEGIN aaa.as
#pile
#include "aldor"
#include "aldorio"

Bar : Exp == Impl where
  Exp ==> with
    inj1 : Integer -> %
    inj2 : Integer -> %
    prj1 : % -> Integer
    prj2 : % -> Integer
  Impl ==> add
    Rep == Union(tag1: Integer, tag2: Integer)
    import from Rep
    inj1(n : Integer) : % == per [tag1==n]
    inj2(s : Integer) : % == per [tag2==2*s]
    prj1(p: %): Integer == (rep p).tag1
    prj2(p: %): Integer == (rep p).tag2

main(): () == {
  z: Integer := 1;
  b1: Bar := inj1 z;
  b2: Bar := inj2 z;
  stdout << "prj1 b1 = " << prj1 b1 << newline;
  stdout << "prj2 b2 = " << prj2 b2 << newline;
  stdout << "prj1 b2 = " << prj1 b2 << newline;
}
main();
---END aaa.as

woodpecker:~>aldor -fx -laldor aaa.as
woodpecker:~>aaa
prj1 b1 = 1
prj2 b2 = 2
Unhandled Exception: RuntimeError()
(Aldor error) Bad union branch.
prj1 b2 = woodpecker:~>

Does that make someone more happy?

Ralf