Edit detail for SandBoxAldorInductiveTypes revision 2 of 2

This implementation of an Inductive (recursive) data type involves the categorical co-product construction. See: LimitsAndColimits

(1) -> )library colimits

Reading #P"/var/aw/var/LatexWiki/colimits.asy"
   Sum2 is now explicitly exposed in frame initial 

   Sum2Functions is now explicitly exposed in frame initial 

   Sum3 is now explicitly exposed in frame initial 

   Sum3Functions is now explicitly exposed in frame initial

An example of Arithmetic Expressions as an Inductive Type

#pile
#include "axiom"
#library COLIMIT "colimits.ao"
import from COLIMIT
+++ Category of Integer-valued Arthemetic Expresions

ExprCat:Category == with
    eval: % -> Integer
    -- evaluates the expression as an Integer
    coerce: % -> OutputForm
    -- displays the expression

+++ Constructor for atomic Integers
MkInt(Z:IntegerNumberSystem): ExprCat
  == add
    Rep == Integer
    -- Export
    eval(x:%):Integer == rep(x)
    coerce(x:%):OutputForm == outputForm rep x

+++ Constructor for additions
MkAdd(X:ExprCat,Y:ExprCat): ExprCat
  == add
    Rep==Record(left:X,right:Y)
    import from Rep, OutputForm
    -- Local:
    plus(x:X,y:Y):OutputForm == paren(x::OutputForm + y::OutputForm);
    sum(x:X,y:Y):Integer     == eval(x) + eval(y);
    -- Export:
    eval(x:%):Integer == sum explode rep x
    coerce(x:%):OutputForm == plus explode rep x

+++ Constructor for multiplications
MkMul(X:ExprCat,Y:ExprCat): ExprCat
  == add
    Rep==Record(left:X,right:Y)
    import from Rep, OutputForm
    -- Local:
    times(x:X,y:Y):OutputForm== paren(x::OutputForm * y::OutputForm);
    product(x:X,y:Y):Integer == eval(x) * eval(y);
    -- Export:
    eval(x:%):Integer == product explode rep x
    coerce(x:%):OutputForm == times explode rep x

MI==>MkInt(Integer)
MA==>MkAdd(%,%)
MM==>MkMul(%,%)

+++ Constructor of Arithmetic Expressions over the Integers
Expr: ExprCat
  == add
    Rep == Sum(MI,MA,MM)
    import from Rep, MI, MA, MM
    -- Export:
    eval(x:%):Integer == sum(Integer,eval,eval,eval)(rep x)
    coerce(x:%):OutputForm == sum(OutputForm,coerce,coerce,coerce)(rep x)

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/expr.as using
      Aldor compiler and options 
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
      Use the system command )set compiler args to change these 
      options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/expr.as", line 2: 
#include "axiom"
^
[L2 C1] #1 (Error) Could not open file `axiom'.

   The )library system command was not called after compilation.

Now extend it to provide the Axiom interpreter interface.

#pile
#include "axiom"
#library EXPR "expr.ao"
import from EXPR
#library COLIMIT "colimits.ao"
import from COLIMIT

extend MkInt(Z:IntegerNumberSystem): with
    coerce: Z -> %
    -- converts a Z-valued object to an atomic Integer
  == add
    Rep == Integer
    -- Export
    coerce(i:Z):% == per(convert(i))

extend MkAdd(X:ExprCat,Y:ExprCat): with
    +: (X,Y) -> %
    -- returns an expression representing the sum
  == add
    Rep==Record(left:X,right:Y)
    import from Rep
    -- Export
    ((x:X) + (y:Y)):% == per [x,y]

extend MkMul(X:ExprCat,Y:ExprCat): with
    *: (X,Y) -> %
    -- returns an expression representing the product
  == add
    Rep==Record(left:X,right:Y)
    import from Rep
    -- Export
    ((x:X) * (y:Y)):% == per [x,y]

MI==>MkInt(Integer)
MA==>MkAdd(%,%)
MM==>MkMul(%,%)

+++ extends domain Expr as above
extend Expr:  with
    coerce: Integer -> %
    +:(%,%) -> %
    *:(%,%) -> %
  == add
    Rep == Sum(MI,MA,MM)
    import from Rep, MI, MA, MM
    -- Export:
    coerce(n: Integer):% == per(inject( n::MI ))
    ((x:%) + (y:%)):% ==    per(inject( (x + y)$MA ))
    ((x:%) * (y:%)):% ==    per(inject( (x * y)$MM ))

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/1062037838131250571-25px003.as
      using Aldor compiler and options 
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
      Use the system command )set compiler args to change these 
      options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/1062037838131250571-25px003.as", line 2: 
#include "axiom"
^
[L2 C1] #1 (Error) Could not open file `axiom'.

   The )library system command was not called after compilation.

n:Expr:=3

   Expr is not a valid type.

Ralf Hemmecke and Bill Page wrote:

Recursive Types

#include "axiom"
RecExpr:with {
    coerce: Integer -> %;
    +: (%, %) -> %;
    *: (%, %) -> %;
    coerce: % -> OutputForm;
    eval: % -> Integer;
}  == add {
    Rep == Union(MakeInt:Integer,
                 MakeAdd:Record(l:%, r:%),
                 MakeMul:Record(l:%, r:%));
    import from Rep;
    import from 'MakeInt', 'MakeAdd', 'MakeMul';
    import from OutputForm;
    --
    -- Local
    plus(x:%,y:%):OutputForm == paren(x::OutputForm + y::OutputForm);
    times(x:%,y:%):OutputForm== paren(x::OutputForm * y::OutputForm);
    sum(x:%,y:%):Integer     == eval(x) + eval(y);
    product(x:%,y:%):Integer == eval(x) * eval(y);
    --
    -- Input
    coerce(n: Integer):% == per [MakeInt==n];
    ((x:%) + (y:%)): %   == per [MakeAdd==[x,y]];
    ((x:%) * (y:%)): %   == per [MakeMul==[x,y]];
    --
    -- Output
    coerce(i:%):OutputForm == { n:=rep(i);
      n case MakeInt => outputForm    n.MakeInt;
      n case MakeAdd => plus  explode n.MakeAdd;
      n case MakeMul => times explode n.MakeMul;
      never;
    };
    --
    -- Evaluation
    eval(i:%):Integer == { n:=rep(i);
      n case MakeInt =>                 n.MakeInt;
      n case MakeAdd => sum     explode n.MakeAdd;
      n case MakeMul => product explode n.MakeMul;
      never;
    }
}

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4075514935174965511-25px005.as
      using Aldor compiler and options 
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
      Use the system command )set compiler args to change these 
      options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4075514935174965511-25px005.as", line 1: 
#include "axiom"
^
[L1 C1] #1 (Error) Could not open file `axiom'.

   The )library system command was not called after compilation.

Here is an example expression

10::RecExpr

   RecExpr is not a valid type.