Re: [Axiom-mail] Spad and inductive types

[Ralf Hemmecke]

Gaby,

because you wanted a contruction of the data structure without any 
functionality, I think the following is the best (at the moment) I can 
think of.

I know the definitions in aaa.as look quite lengthy, but it probably 
shows how one could generically generate appropriate Aldor code from a 
more concise Syntax. All the exports that appear are basically the 
exports of the Union (OK, Union still has a few more.)

I couln't compile the code if it was in just one file. But that seems to 
be clear for Aldor. Or haven't I read the AUG clearly enough?

Ralf

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

define ET: Category == with; -- ExpressionType
Expr: ET with {
        MkInt: Integer -> %;
        MkAdd: (%, %) -> %;
        MkMul: (%, %) -> %;
        apply: (%, 'MkInt') -> Integer;
        apply: (%, 'MkAdd') -> (%, %);
        apply: (%, 'MkMul') -> (%, %);
        case: (%, 'MkInt') -> Boolean;
        case: (%, 'MkAdd') -> Boolean;
        case: (%, 'MkMul') -> Boolean;
} == add {
        Rep == Union(
            Mkint: Integer,
            Mkadd: Record(left: %, right: %),
            Mkmul: Record(left: %, right: %)
        );
        import from Rep;
        MkInt(i: Integer): % == per union i;
        MkAdd(x: %, y: %): % == per [Mkadd == [x, y]];
        MkMul(x: %, y: %): % == per [Mkmul == [x, y]];
        
        apply(x: %, t:'MkInt'): Integer == rep(x).Mkint;
        apply(x: %, t:'MkAdd'): (%, %) == explode rep(x).Mkadd;
        apply(x: %, t:'MkMul'): (%, %) == explode rep(x).Mkmul;

        (x: %) case (t:'MkInt'): Boolean == rep(x) case Mkint;
        (x: %) case (t:'MkAdd'): Boolean == rep(x) case Mkadd;
        (x: %) case (t:'MkMul'): Boolean == rep(x) case Mkmul;
}
---END aaa.as
--------------------------------------------------------------------
---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;
        }
}

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