Re: [Axiom-mail] Spad and inductive types

[Ralf Hemmecke]

Ooops, I overlooked something.

> > ---BEGIN bbb.as
> > #include "aldor"
> > #include "aldorio"
> >
> > #library EXPR "aaa.ao"
> > import from EXPR;
> >
> > extend Expr: OutputType == add {
> >     import from 'MkInt', 'MkAdd', 'MkMul';
> >     import from Integer;
> >     (tw: TextWriter) << (x: %): TextWriter == {
> >         x case MkInt => tw << x.MkInt;
> >         x case MkAdd => {
> >             (a, b) := x.MkAdd;
> >             tw << "(" << a << "+" << b << ")";
> >         }
> >         x case MkMul => {
> >             (a, b) := x.MkMul;
> >             tw << "(" << a << "*" << b << ")";
> >         }
> >         tw;
> >     }
> > }

> The use of case above seems very unnatural to me. Is it
> possible to extend each constructor (e.g. MkInt, MkMul, etc.)
> separately.

I don't understand. In my case Mk??? are not domain constructors, so I 
have no way to "extend" anyway.

On the other hand, why is that case business so unnatural? Expr is a 
Union, so in order to be type safe, I have to figure out in which part 
of the union the element actually lives. You do the same thing in your 
implementation of eval on 
http://wiki.axiom-developer.org/SandBoxInductiveType .

> > main(): () == {
> >     import from Integer;
> >     e1: Expr := MkInt 1;       stdout << "e1 = " << e1 << newline;
> >     e2: Expr := MkInt 2;       stdout << "e2 = " << e2 << newline;
> >     e3: Expr := MkInt 3;       stdout << "e3 = " << e3 << newline;
> >     a1: Expr := MkAdd(e1, e2); stdout << "a1 = " << a1 << newline;
> >     m1: Expr := MkMul(a1, e3); stdout << "m1 = " << m1 << newline;
> > }
> > main();
> > ---END bbb.as

> Ralf, these are just general comments about your approach and
> aren't intended to be particularly critical.

Although I felt that it was the most critical reaction on one of my 
mails that I have ever experienced from you, I know that you do that to 
contribute to understanding the situation. I don't feel offended.

By the way. Today I have learned how to include an integer into the 
"left" or "right" part of Union(left: Integer, right: Integer). There 
appears only an example in the AUG, but not a formal description.

Ralf