help links subscribe changes refresh edit

	SandBox
SandBoxINFSUM ←	↑	→ SandBoxInequation

SandBoxInductiveType

Edit detail for SandBoxInductiveType revision 1 of 1

	1
Editor: Time: 2007/11/18 18:04:46 GMT-8
Note: Martin wrote ...

changed:
-
**On May 6, 2007 11:01 PM Gabriel Dos Reis wrote:**

While writing a tutorial on programming with Spad, I realize that
I don't have a good way to present inductive types in Spad.  I know
what they would like in my ideal Spad, but we don't have that ideal
Spad yet.  So, I'm asking here how you would write inductive types
today in Spad.

For concreteness, here is a very classic example of inductive type
along with a function working on expression of such type, written in
both Haskell and New Boot.  How would you best write that in Spad?

Haskell code::

  data Expr = MkInt Int
          | MkAdd Expr Expr
	  | MkMul Expr Expr

  eval::Expr -> Int
  eval (MkInt i) = i
  eval (MkAdd x y) = (eval x) + (eval y)
  eval (MkMul x y) = (eval x) * (eval y)

Here is the same thing written in New Boot::

  structure Expr == 
     MkInt(Integer)
     MkAdd(Expr, Expr)
     MkMul(Expr, Expr)

  eval e ==
    case e of
       MkInt(i) => i
       MkAdd(x, y) => eval(x) + eval(y)
       MkMul(x, y) => eval(x) * eval(y)
       otherwise => error "should not happen"


**On Sent: May 7, 2007 9:11 AM Gabriel Dos Reis wrote:**

An inductive type is a kind of union whose members are
inductively defined.  Here I took a very simplistic datatype,
that of an arithmetic expression over integers:

      -- An arithmetic expression over integer is:

      * an integer, or 

      * addition of two expressions over integer, or

      * multiplication of two expressions over integer.

!MkInt, !MkAdd and !MkMul (in both Boot and Haskell) are data
constructors.  Given an integer, !MkInt turn it into an Expr.
Simirlarly, !MkAdd and !MkMul combines two expressions into an Expr.
So, they have types::

    MkInt :: Int -> Expr
    MkAdd :: Expr -> Expr -> Expr
    MkMul :: Expr -> Expr -> Expr

Furthermore, they can also serves as "tags" to indicate how
expressions of Expr are constructed.  That is useful in pattern
matching.  In pattern matching, the data constructor serves as tag,
and the operands are variables that are bound to the operands.

**On May 7, 2007 4:14 AM Martin Rubey wrote:**

\begin{spad}
)abbrev domain EX Expr
Expr(): with
    eval: % -> Integer
    coerce: Integer -> %
    coerce: % -> OutputForm
    _+: (%,%) -> %
    _*: (%,%) -> %
  == add
    MkInt ==> Integer
    MkAdd ==> Record(lAdd:%,rAdd:%)
    MkMul ==> Record(lMul:%,rMul:%)
    Rep := Union(MkInt, MkAdd, MkMul)

    eval(x:%): Integer ==
      x case MkInt => x
      x case MkAdd => (eval(x.lAdd) + eval(x.rAdd))$Integer
      x case MkMul => (eval(x.lMul) * eval(x.rMul))$Integer

    coerce(n: Integer) == n

    x + y == [x,y]$MkAdd

    x * y == [x,y]$MkMul

    coerce(x: %): OutputForm ==
      x case MkInt => outputForm x
      x case MkAdd => hconcat [message "(",          _
                               (x.lAdd)::OutputForm, _
                               message "+",          _
                               (x.rAdd)::OutputForm, _
                               message ")"] 
      x case MkMul => hconcat [message "(",          _
                               (x.lMul)::OutputForm, _
                               message "*",          _
                               (x.rMul)::OutputForm, _
                               message ")"]

\end{spad}

\begin{axiom}
n:Expr:=3
m:Expr:=4
p:=n+m
eval(p)
q:=p*5
eval(q)
\end{axiom}

**Ralf Hemmecke wrote:**

Here is a similar thing in Aldor. Actually it should be called BinaryExpressionTree.
Note that according to the "Aldor User Guide (Type Union)":http://aldor.org/docs/HTML/chap13.html#8
one cannot use the type as the second argument of a "case" expression.
So the above representation would rather look like::

    Rep == Union(
        MkInt: Integer,
        MkAdd: Record(lAdd:%, rAdd:%),
        MkMul: Record(lMul:%, rMul:%)
    );

in an Aldor equivalent. I only see a problem if there were additionally an entry like::

        MkInt2: Integer

whose type is identical to some other type of the union, because then the function "union(i)"
where i is an integer would not know whether it belongs to MkInt or MkInt2.

\begin{aldor}
#include "axiom"

macro Z == Integer;
BinExpr: with {
	eval: % -> Integer;
	coerce: Integer -> %;
	+: (%,%) -> %;
	*: (%,%) -> %;
	coerce: % -> OutputForm;
} == add {
	Rep == Union(
	    z: Z,
	    tuple: Record(print: String, op: (Z, Z) -> Z, left: %, right: %);
	);
	import from Rep;
	coerce(i: Integer): % == per union i;
	(x: %) + (y: %): % == per union ["+", +, x, y];
	(x: %) * (y: %): % == per union ["*", *, x, y];
	eval(x: %): Integer == {
		rep x case z => rep(x).z;
		(s, f, a, b) := explode(rep(x).tuple);
		f(eval a, eval b);
	}
	coerce(x: %): OutputForm == {
		import from List OutputForm;
		rep x case z => coerce(rep(x).z);
		(s, f, a, b) := explode(rep(x).tuple);
		hconcat [
		    message "(",
		    a :: OutputForm,
		    message s,
		    b :: OutputForm,
		    message ")"
		];
	}
}
\end{aldor}

\begin{axiom}
nBin: BinExpr := 3
mBin: BinExpr := 4
pBin := nBin + mBin
eval(pBin)
qBin := pBin*(5::BinExpr)
eval(qBin)
\end{axiom}


**On May 8 12:40 AM Bill Page writes:**

Here is one way of writing this by defining the appropriate types
for the expressions and sub-expressions.

\begin{spad}
)abbrev category EXCAT ExprCat
++ Description:
++ Category of Integer-valued Arthemetic Expresions
ExprCat:Category == with
    eval: % -> Integer
    ++ \spad{eval} evaluates the expression as an Integer
    coerce: % -> OutputForm
    ++ \spad{coerce} displays the expression

)abbrev domain MI MkInt
++ Description:
++ Constructor for atomic Integers
MkInt(Z:IntegerNumberSystem): ExprCat with
    coerce:Z -> %
    ++ \spad{coerce} converts a Z-valued object to an atomic Integer
  == add
    Rep := Integer
    coerce(i:Z):% == convert(i)@%
    eval(x:%):Integer == x pretend Integer
    coerce(x:%):OutputForm == outputForm eval x

)abbrev domain MA MkAdd
++ Description:
++ Constructor for additions
MkAdd(X:ExprCat,Y:ExprCat): ExprCat with
    _+: (X,Y) -> %
    ++ \spad{+} returns an expression representing the sum
  == add
    Rep:=Record(left:X,right:Y)
    x + y == [x,y]$Rep
    eval(x:%):Integer == (eval((x@Rep).left) + eval((x@Rep).right))$Integer
    coerce(x:%):OutputForm == 
      hconcat [
        message "(",                 _
        ((x@Rep).left)::OutputForm,  _
        message "+",                 _
        ((x@Rep).right)::OutputForm, _
        message ")"] 

)abbrev domain MM MkMul
++ Description:
++ Constructor for multiplications
MkMul(X:ExprCat,Y:ExprCat): ExprCat with
    _*: (X,Y) -> %
    ++ \spad{*} returns an expression representing the product
  == add
    Rep:=Record(left:X,right:Y)
    x * y == [x,y]$Rep
    eval(x:%):Integer == (eval((x@Rep).left) * eval((x@Rep).right))$Integer
    coerce(x:%):OutputForm == 
      hconcat [message "(",          _
        ((x@Rep).left)::OutputForm,  _
        message "*",                 _
        ((x@Rep).right)::OutputForm, _
        message ")"] 

)abbrev domain EX2 Expr2
++ Description:
++ Constructor of Arithmetic Expressions over the Integers
Expr2: ExprCat with
    coerce: Integer -> %
    _+:(%,%) -> %
    _*:(%,%) -> %
  == add
    Rep := Union(MkInt(Integer), MkAdd(%,%), MkMul(%,%))
    eval(x:%): Integer ==
      x case MkInt(Integer) => eval(x)$MkInt(Integer)
      x case MkAdd(%,%) => eval(x)$MkAdd(%,%)
      x case MkMul(%,%) => eval(x)$MkMul(%,%)
    coerce(n: Integer):% == n::MkInt(Integer)
    x + y == (x@Rep + y@Rep)$MkAdd(%,%)
    x * y == (x@Rep * y@Rep)$MkMul(%,%)
    coerce(x:%): OutputForm ==
      x case MkInt(Integer) => coerce(x)$MkInt(Integer)
      x case MkAdd(%,%) => coerce(x)$MkAdd(%,%)
      x case MkMul(%,%) => coerce(x)$MkMul(%,%)
\end{spad}


\begin{axiom}
n2:Expr2:=3
m2:Expr2:=4
p2:=n2+m2
eval(p2)
q2:=p2*5
eval(q2)
\end{axiom}

On May 6, 2007 11:01 PM Gabriel Dos Reis wrote:

While writing a tutorial on programming with Spad, I realize that I don't have a good way to present inductive types in Spad. I know what they would like in my ideal Spad, but we don't have that ideal Spad yet. So, I'm asking here how you would write inductive types today in Spad.

For concreteness, here is a very classic example of inductive type along with a function working on expression of such type, written in both Haskell and New Boot. How would you best write that in Spad?

Haskell code:

  data Expr = MkInt Int
          | MkAdd Expr Expr
          | MkMul Expr Expr

  eval::Expr -> Int
  eval (MkInt i) = i
  eval (MkAdd x y) = (eval x) + (eval y)
  eval (MkMul x y) = (eval x) * (eval y)

Here is the same thing written in New Boot:

  structure Expr == 
     MkInt(Integer)
     MkAdd(Expr, Expr)
     MkMul(Expr, Expr)

  eval e ==
    case e of
       MkInt(i) => i
       MkAdd(x, y) => eval(x) + eval(y)
       MkMul(x, y) => eval(x) * eval(y)
       otherwise => error "should not happen"

On Sent: May 7, 2007 9:11 AM Gabriel Dos Reis wrote:

An inductive type is a kind of union whose members are inductively defined. Here I took a very simplistic datatype, that of an arithmetic expression over integers:

-- An arithmetic expression over integer is:

an integer, or
addition of two expressions over integer, or
multiplication of two expressions over integer.

MkInt, MkAdd and MkMul (in both Boot and Haskell) are data constructors. Given an integer, MkInt turn it into an Expr. Simirlarly, MkAdd and MkMul combines two expressions into an Expr. So, they have types:

    MkInt :: Int -> Expr
    MkAdd :: Expr -> Expr -> Expr
    MkMul :: Expr -> Expr -> Expr

Furthermore, they can also serves as "tags" to indicate how expressions of Expr are constructed. That is useful in pattern matching. In pattern matching, the data constructor serves as tag, and the operands are variables that are bound to the operands.

On May 7, 2007 4:14 AM Martin Rubey wrote:

fricas

(1) -> <spad>

fricas

)abbrev domain EX Expr
Expr(): with
    eval: % -> Integer
    coerce: Integer -> %
    coerce: % -> OutputForm
    _+: (%,%) -> %
    _*: (%,%) -> %
  == add
    MkInt ==> Integer
    MkAdd ==> Record(lAdd:%,rAdd:%)
    MkMul ==> Record(lMul:%,rMul:%)
    Rep := Union(MkInt, MkAdd, MkMul)

    eval(x:%): Integer ==
      x case MkInt => x
      x case MkAdd => (eval(x.lAdd) + eval(x.rAdd))$Integer
      x case MkMul => (eval(x.lMul) * eval(x.rMul))$Integer

    coerce(n: Integer) == n

    x + y == [x,y]$MkAdd

    x * y == [x,y]$MkMul

    coerce(x: %): OutputForm ==
      x case MkInt => outputForm x
      x case MkAdd => hconcat [message "(",          _
                               (x.lAdd)::OutputForm, _
                               message "+",          _
                               (x.rAdd)::OutputForm, _
                               message ")"] 
      x case MkMul => hconcat [message "(",          _
                               (x.lMul)::OutputForm, _
                               message "*",          _
                               (x.rMul)::OutputForm, _
                               message ")"]</spad>

fricas

Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3998018739717071210-25px001.spad
      using old system compiler.
   EX abbreviates domain Expr 
------------------------------------------------------------------------
   initializing NRLIB EX for Expr 
   compiling into NRLIB EX 
   processing macro definition MkInt ==> Integer 
   processing macro definition MkAdd ==> Record(lAdd: %,rAdd: %) 
   processing macro definition MkMul ==> Record(lMul: %,rMul: %) 
   compiling exported eval : % -> Integer
Time: 0 SEC.

   compiling exported coerce : Integer -> %
      EX;coerce;I%;2 is replaced by CONS0n 
Time: 0 SEC.

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

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

   compiling exported coerce : % -> OutputForm
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |Expr| REDEFINED

;;;     ***       |Expr| REDEFINED
Time: 0 SEC.

   Warnings: 
      [1] eval:  lAdd has no value
      [2] eval:  rAdd has no value
      [3] eval:  lMul has no value
      [4] eval:  rMul has no value
      [5] coerce:  lAdd has no value
      [6] coerce:  rAdd has no value
      [7] coerce:  lMul has no value
      [8] coerce:  rMul has no value

   Cumulative Statistics for Constructor Expr
      Time: 0 seconds

   finalizing NRLIB EX 
   Processing Expr for Browser database:
--->-->Expr(constructor): Not documented!!!!
--->-->Expr((eval ((Integer) %))): Not documented!!!!
--->-->Expr((coerce (% (Integer)))): Not documented!!!!
--->-->Expr((coerce ((OutputForm) %))): Not documented!!!!
--->-->Expr((+ (% % %))): Not documented!!!!
--->-->Expr((* (% % %))): Not documented!!!!
--->-->Expr(): Missing Description
; compiling file "/var/aw/var/LatexWiki/EX.NRLIB/EX.lsp" (written 01 NOV 2024 01:13:20 AM):

; wrote /var/aw/var/LatexWiki/EX.NRLIB/EX.fasl
; compilation finished in 0:00:00.012
------------------------------------------------------------------------
   Expr is now explicitly exposed in frame initial 
   Expr will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/EX.NRLIB/EX

fricas

n:Expr:=3

$\label{eq1}3$

(1)

Type: Expr

fricas

m:Expr:=4

$\label{eq2}4$

(2)

Type: Expr

fricas

p:=n+m

$\label{eq3}(3 + 4)$

(3)

Type: Expr

fricas

eval(p)

$\label{eq4}7$

(4)

Type: PositiveInteger?

fricas

q:=p*5

$\label{eq5}({(3 + 4)}<em> 5)$

(5)

Type: Expr

fricas

eval(q)

$\label{eq6}35$

(6)

Type: PositiveInteger?

Ralf Hemmecke wrote:

Here is a similar thing in Aldor. Actually it should be called BinaryExpressionTree?. Note that according to the Aldor User Guide (Type Union) one cannot use the type as the second argument of a "case" expression. So the above representation would rather look like:

    Rep == Union(
        MkInt: Integer,
        MkAdd: Record(lAdd:%, rAdd:%),
        MkMul: Record(lMul:%, rMul:%)
    );

in an Aldor equivalent. I only see a problem if there were additionally an entry like:

        MkInt2: Integer

whose type is identical to some other type of the union, because then the function "union(i)" where i is an integer would not know whether it belongs to MkInt? or MkInt2?.

aldor

#include "axiom"

macro Z == Integer;
BinExpr: with {
        eval: % -> Integer;
        coerce: Integer -> %;
        +: (%,%) -> %;
        *: (%,%) -> %;
        coerce: % -> OutputForm;
} == add {
        Rep == Union(
            z: Z,
            tuple: Record(print: String, op: (Z, Z) -> Z, left: %, right: %);
        );
        import from Rep;
        coerce(i: Integer): % == per union i;
        (x: %) + (y: %): % == per union ["+", +, x, y];
        (x: %) * (y: %): % == per union ["*", *, x, y];
        eval(x: %): Integer == {
                rep x case z => rep(x).z;
                (s, f, a, b) := explode(rep(x).tuple);
                f(eval a, eval b);
        }
        coerce(x: %): OutputForm == {
                import from List OutputForm;
                rep x case z => coerce(rep(x).z);
                (s, f, a, b) := explode(rep(x).tuple);
                hconcat [
                    message "(",
                    a :: OutputForm,
                    message s,
                    b :: OutputForm,
                    message ")"
                ];
        }
}

aldor

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/9147585987609704779-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/9147585987609704779-25px003.as", line 1: 
#include "axiom"
^
[L1 C1] #1 (Error) Could not open file `axiom'.

   The )library system command was not called after compilation.

fricas

nBin: BinExpr := 3

   BinExpr is not a valid type.

On May 8 12:40 AM Bill Page writes:

Here is one way of writing this by defining the appropriate types for the expressions and sub-expressions.

spad

)abbrev category EXCAT ExprCat
++ Description:
++ Category of Integer-valued Arthemetic Expresions
ExprCat:Category == with
    eval: % -> Integer
    ++ \spad{eval} evaluates the expression as an Integer
    coerce: % -> OutputForm
    ++ \spad{coerce} displays the expression

)abbrev domain MI MkInt
++ Description:
++ Constructor for atomic Integers
MkInt(Z:IntegerNumberSystem): ExprCat with
    coerce:Z -> %
    ++ \spad{coerce} converts a Z-valued object to an atomic Integer
  == add
    Rep := Integer
    coerce(i:Z):% == convert(i)@%
    eval(x:%):Integer == x pretend Integer
    coerce(x:%):OutputForm == outputForm eval x

)abbrev domain MA MkAdd
++ Description:
++ Constructor for additions
MkAdd(X:ExprCat,Y:ExprCat): ExprCat with
    _+: (X,Y) -> %
    ++ \spad{+} returns an expression representing the sum
  == add
    Rep:=Record(left:X,right:Y)
    x + y == [x,y]$Rep
    eval(x:%):Integer == (eval((x@Rep).left) + eval((x@Rep).right))$Integer
    coerce(x:%):OutputForm == 
      hconcat [
        message "(",                 _
        ((x@Rep).left)::OutputForm,  _
        message "+",                 _
        ((x@Rep).right)::OutputForm, _
        message ")"] 

)abbrev domain MM MkMul
++ Description:
++ Constructor for multiplications
MkMul(X:ExprCat,Y:ExprCat): ExprCat with
    _*: (X,Y) -> %
    ++ \spad{*} returns an expression representing the product
  == add
    Rep:=Record(left:X,right:Y)
    x * y == [x,y]$Rep
    eval(x:%):Integer == (eval((x@Rep).left) * eval((x@Rep).right))$Integer
    coerce(x:%):OutputForm == 
      hconcat [message "(",          _
        ((x@Rep).left)::OutputForm,  _
        message "*",                 _
        ((x@Rep).right)::OutputForm, _
        message ")"] 

)abbrev domain EX2 Expr2
++ Description:
++ Constructor of Arithmetic Expressions over the Integers
Expr2: ExprCat with
    coerce: Integer -> %
    _+:(%,%) -> %
    _*:(%,%) -> %
  == add
    Rep := Union(MkInt(Integer), MkAdd(%,%), MkMul(%,%))
    eval(x:%): Integer ==
      x case MkInt(Integer) => eval(x)$MkInt(Integer)
      x case MkAdd(%,%) => eval(x)$MkAdd(%,%)
      x case MkMul(%,%) => eval(x)$MkMul(%,%)
    coerce(n: Integer):% == n::MkInt(Integer)
    x + y == (x@Rep + y@Rep)$MkAdd(%,%)
    x * y == (x@Rep * y@Rep)$MkMul(%,%)
    coerce(x:%): OutputForm ==
      x case MkInt(Integer) => coerce(x)$MkInt(Integer)
      x case MkAdd(%,%) => coerce(x)$MkAdd(%,%)
      x case MkMul(%,%) => coerce(x)$MkMul(%,%)

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2270268880364130397-25px005.spad
      using old system compiler.
   EXCAT abbreviates category ExprCat 
------------------------------------------------------------------------
   initializing NRLIB EXCAT for ExprCat 
   compiling into NRLIB EXCAT 

;;;     ***       |ExprCat| REDEFINED
Time: 0 SEC.

   finalizing NRLIB EXCAT 
   Processing ExprCat for Browser database:
--------constructor---------
--------(eval ((Integer) %))---------
--------(coerce ((OutputForm) %))---------
; compiling file "/var/aw/var/LatexWiki/EXCAT.NRLIB/EXCAT.lsp" (written 01 NOV 2024 01:13:20 AM):

; wrote /var/aw/var/LatexWiki/EXCAT.NRLIB/EXCAT.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
   ExprCat is now explicitly exposed in frame initial 
   ExprCat will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/EXCAT.NRLIB/EXCAT

   MI abbreviates domain MkInt 
------------------------------------------------------------------------
   initializing NRLIB MI for MkInt 
   compiling into NRLIB MI 
Local variable Rep type redefined: (Join (IntegerNumberSystem) (LinearlyExplicitOver (Integer)) (PolynomialFactorizationExplicit) (ConvertibleTo (String)) (OpenMath) (Canonical) (canonicalsClosed) (Hashable) (CATEGORY domain (SIGNATURE random (% %)) (SIGNATURE seedRandom ((Void))))) to (Join (SetCategory) (CATEGORY domain (SIGNATURE ~= ((Boolean) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE coerce ((OutputForm) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE autoCoerce ((Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Integer))) (SIGNATURE coerce ((Integer) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE autoCoerce ((Integer) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE case ((Boolean) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Integer))) (SIGNATURE autoCoerce ((Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Record (: lAdd %) (: rAdd %)))) (SIGNATURE coerce ((Record (: lAdd %) (: rAdd %)) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE autoCoerce ((Record (: lAdd %) (: rAdd %)) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE case ((Boolean) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Record (: lAdd %) (: rAdd %)))) (SIGNATURE autoCoerce ((Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Record (: lMul %) (: rMul %)))) (SIGNATURE coerce ((Record (: lMul %) (: rMul %)) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE autoCoerce ((Record (: lMul %) (: rMul %)) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))))) (SIGNATURE case ((Boolean) (Union (Integer) (Record (: lAdd %) (: rAdd %)) (Record (: lMul %) (: rMul %))) (Record (: lMul %) (: rMul %))))))
   compiling exported coerce : Z -> %
Time: 0 SEC.

   compiling exported eval : % -> Integer
      MI;eval;%I;2 is replaced by x 
Time: 0 SEC.

   compiling exported coerce : % -> OutputForm
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |MkInt| REDEFINED

;;;     ***       |MkInt| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor MkInt
      Time: 0 seconds

   finalizing NRLIB MI 
   Processing MkInt for Browser database:
--------constructor---------
--------(coerce (% Z))---------
; compiling file "/var/aw/var/LatexWiki/MI.NRLIB/MI.lsp" (written 01 NOV 2024 01:13:20 AM):

; wrote /var/aw/var/LatexWiki/MI.NRLIB/MI.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
   MkInt is now explicitly exposed in frame initial 
   MkInt will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/MI.NRLIB/MI

   MA abbreviates domain MkAdd 
------------------------------------------------------------------------
   initializing NRLIB MA for MkAdd 
   compiling into NRLIB MA 
Local variable Rep type redefined: (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: left X) (: right Y)) X Y)) (SIGNATURE ~= ((Boolean) (Record (: left X) (: right Y)) (Record (: left X) (: right Y)))) (SIGNATURE coerce ((OutputForm) (Record (: left X) (: right Y)))) (SIGNATURE elt (X (Record (: left X) (: right Y)) left)) (SIGNATURE elt (Y (Record (: left X) (: right Y)) right)) (SIGNATURE setelt! (X (Record (: left X) (: right Y)) left X)) (SIGNATURE setelt! (Y (Record (: left X) (: right Y)) right Y)) (SIGNATURE copy ((Record (: left X) (: right Y)) (Record (: left X) (: right Y)))))) to (Join (IntegerNumberSystem) (LinearlyExplicitOver (Integer)) (PolynomialFactorizationExplicit) (ConvertibleTo (String)) (OpenMath) (Canonical) (canonicalsClosed) (Hashable) (CATEGORY domain (SIGNATURE random (% %)) (SIGNATURE seedRandom ((Void)))))
   compiling exported + : (X,Y) -> %
      MA;+;XY%;1 is replaced by CONS 
Time: 0 SEC.

   compiling exported eval : % -> Integer
Time: 0 SEC.

   compiling exported coerce : % -> OutputForm
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |MkAdd| REDEFINED

;;;     ***       |MkAdd| REDEFINED
Time: 0 SEC.

   Warnings: 
      [1] eval:  left has no value
      [2] eval:  right has no value

   Cumulative Statistics for Constructor MkAdd
      Time: 0 seconds

   finalizing NRLIB MA 
   Processing MkAdd for Browser database:
--------constructor---------
--------(+ (% X Y))---------
; compiling file "/var/aw/var/LatexWiki/MA.NRLIB/MA.lsp" (written 01 NOV 2024 01:13:20 AM):

; wrote /var/aw/var/LatexWiki/MA.NRLIB/MA.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
   MkAdd is now explicitly exposed in frame initial 
   MkAdd will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/MA.NRLIB/MA

   MM abbreviates domain MkMul 
------------------------------------------------------------------------
   initializing NRLIB MM for MkMul 
   compiling into NRLIB MM 
   compiling exported * : (X,Y) -> %
      MM;*;XY%;1 is replaced by CONS 
Time: 0 SEC.

   compiling exported eval : % -> Integer
Time: 0 SEC.

   compiling exported coerce : % -> OutputForm
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |MkMul| REDEFINED

;;;     ***       |MkMul| REDEFINED
Time: 0 SEC.

   Warnings: 
      [1] eval:  left has no value
      [2] eval:  right has no value

   Cumulative Statistics for Constructor MkMul
      Time: 0 seconds

   finalizing NRLIB MM 
   Processing MkMul for Browser database:
--------constructor---------
--------(* (% X Y))---------
; compiling file "/var/aw/var/LatexWiki/MM.NRLIB/MM.lsp" (written 01 NOV 2024 01:13:20 AM):

; wrote /var/aw/var/LatexWiki/MM.NRLIB/MM.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
   MkMul is now explicitly exposed in frame initial 
   MkMul will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/MM.NRLIB/MM

   EX2 abbreviates domain Expr2 
------------------------------------------------------------------------
   initializing NRLIB EX2 for Expr2 
   compiling into NRLIB EX2 
Local variable Rep type redefined: (Join (SetCategory) (CATEGORY domain (SIGNATURE ~= ((Boolean) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE coerce ((OutputForm) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE autoCoerce ((Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (MkInt (Integer)))) (SIGNATURE coerce ((MkInt (Integer)) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE autoCoerce ((MkInt (Integer)) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE case ((Boolean) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (MkInt (Integer)))) (SIGNATURE autoCoerce ((Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (MkAdd % %))) (SIGNATURE coerce ((MkAdd % %) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE autoCoerce ((MkAdd % %) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE case ((Boolean) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (MkAdd % %))) (SIGNATURE autoCoerce ((Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (MkMul % %))) (SIGNATURE coerce ((MkMul % %) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE autoCoerce ((MkMul % %) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)))) (SIGNATURE case ((Boolean) (Union (MkInt (Integer)) (MkAdd % %) (MkMul % %)) (MkMul % %))))) to (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: left X) (: right Y)) X Y)) (SIGNATURE ~= ((Boolean) (Record (: left X) (: right Y)) (Record (: left X) (: right Y)))) (SIGNATURE coerce ((OutputForm) (Record (: left X) (: right Y)))) (SIGNATURE elt (X (Record (: left X) (: right Y)) left)) (SIGNATURE elt (Y (Record (: left X) (: right Y)) right)) (SIGNATURE setelt! (X (Record (: left X) (: right Y)) left X)) (SIGNATURE setelt! (Y (Record (: left X) (: right Y)) right Y)) (SIGNATURE copy ((Record (: left X) (: right Y)) (Record (: left X) (: right Y))))))
   compiling exported eval : % -> Integer
Time: 0 SEC.

   compiling exported coerce : Integer -> %
Time: 0 SEC.

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

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

   compiling exported coerce : % -> OutputForm
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |Expr2| REDEFINED

;;;     ***       |Expr2| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor Expr2
      Time: 0 seconds

   finalizing NRLIB EX2 
   Processing Expr2 for Browser database:
--------constructor---------
--->-->Expr2((coerce (% (Integer)))): Not documented!!!!
--->-->Expr2((+ (% % %))): Not documented!!!!
--->-->Expr2((* (% % %))): Not documented!!!!
; compiling file "/var/aw/var/LatexWiki/EX2.NRLIB/EX2.lsp" (written 01 NOV 2024 01:13:20 AM):

; wrote /var/aw/var/LatexWiki/EX2.NRLIB/EX2.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
   Expr2 is now explicitly exposed in frame initial 
   Expr2 will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/EX2.NRLIB/EX2