login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit
SandBox Aldor
SandBox Aldor Join and Meet  ← ↑ →  SandBox Aldor Sieve

SandBox Aldor Semantics
  
last edited 7 months ago by test1

Edit detail for SandBox Aldor Semantics revision 4 of 5
1 2 3 4 5
Editor: page
Time: 2008/11/25 08:23:19 GMT-8
Note: FOAM errors in new Aldor interface 
added:

\begin{axiom}
)version
\end{axiom}


The following Aldor code was given as an example by Ralf Hemmecke
and added to the wiki by Martin Rubey. See the thread:


http://lists.gnu.org/archive/html/axiom-developer/2006-07/msg00046.html


\begin{axiom}
)version
\end{axiom}


\begin{aldor}
#include "axiom"
define CatA: Category == with { }
define CatB: Category == with { }
define SomeCat: Category == with { CatA; CatB; }
Dom: SomeCat == Integer add;
A == Dom;
B: CatA == Dom;
H: CatA == Dom add;
main1():List Record(expression:String,result:Boolean) == [
  ["A has CatA",A has CatA],
  ["A has CatB",A has CatB],
  ["A has SomeCat",A has SomeCat],
  ["B has CatA",B has CatA],
  ["B has CatB",B has CatB],
  ["B has SomeCat",B has SomeCat],
  ["H has CatA",H has CatA],
  ["H has CatB",H has CatB],
  ["H has SomeCat",H has SomeCat]];


\end{aldor}


You get...
\begin{axiom}
main1()
)clear completely
\end{axiom}


In particular, that "B has CatB" is a bit surprising, isn't it?


Bill Page replied:

  I think you are dealing here with two separate but related issues:
  1) *static* typing, and 2) inheritance rules. All types in Aldor
  are static (or at least *nearly static*) meaning that they must be
  resolved during the compilation phase.





\begin{aldor}
#include "axiom"


define CatA?: Category == with;
define CatB?: Category == with;
define CatX?: Category == with {CatA?; CatB?;}


A: Join(CatX?, CatA?) == add;
B: Join(CatX?, CatB?) == add;
import from Integer;
X: CatX? == if odd? random(10) then A else B;
\end{aldor}


Try a little harder to create dynamic types:
\begin{aldor}
#include "axiom"


import from Integer;


define CatA?: Category == with {n:Integer};
define CatB?: Category == with {n:Integer};
define CatX?: Category == with {n:Integer};


A: Join(CatX?, CatA?) == add { n:Integer==1 };
B: Join(CatX?, CatB?) == add { n:Integer==2 };
X1: CatX? == if odd? random(10) then (A add) else (B add);
X2: CatX? == if even? random(10) then (A add) else (B add);
\end{aldor}


\begin{axiom}
for i in 1..10 repeat output [n()$X1,n()$X2]?
)clear completely
\end{axiom}


Or this way:
\begin{aldor}
#include "axiom"
import from Integer;


define CatA?: Category == with {n:Integer};
define CatB?: Category == with {n:Integer};
define CatX?: Category == with {CatA?; CatB?; n:Integer};


A: Join(CatX?, CatA?) == add { n:Integer==1 };
B: Join(CatX?, CatB?) == add { n:Integer==2 };
Y1: CatX? == if odd? random(10) then A else B;
Y2: CatX? == if even? random(10) then A else B;
\end{aldor}


\begin{axiom}
for i in 1..10 repeat output [n()$Y1,n()$Y2]?
)clear completely
\end{axiom}


Or like this:
\begin{aldor}
#include "axiom"
import from Integer;
define CatX?: Category == with {foo: () -> Integer}
A: CatX? == add {foo(): Integer == 0;}
B: CatX? == add {foo(): Integer == 1;}
Z: CatX? == if odd? random(10) then A else B;
\end{aldor}


\begin{axiom}
for i in 1..10 repeat output foo()$Z
)clear completely
\end{axiom}


Ralf Hemmecke asked:
Why does the compiler reject the program without the "add"
in line (*)?
\begin{aldor}
#include "axiom"


define CatA?: Category == with;
define CatB?: Category == with;
define CatX?: Category == with;
A: CatX? with { CatA? } == add;
B: CatX? with { CatB? } == add;
X: CatX? == if true then (A add) else (B add); -- (*)


main2():List Record(expression:String,result:Boolean) == [
  ["X has CatA",X has CatA]?,
  ["X has CatB",X has CatB]?,
  ["X has CatX",X has CatX]]?;


\end{aldor}


\begin{axiom}
main2()
)clear completely
\end{axiom}


Christian Aistleitner provided this answer:


I'd consider that a bug in comparison of exports. Replacing your (*) line  
by:

   X: CatX == if true then (A@CatX) else (B@CatX);





gives a working program.
\begin{aldor}
#include "axiom"


define CatA?: Category == with;
define CatB?: Category == with;
define CatX?: Category == with;
A: CatX? with { CatA? } == add;
B: CatX? with { CatB? } == add;
X: CatX? == if true then A@CatX? else B@CatX?; -- (*)


main3():List Record(expression:String,result:Boolean) == [
  ["X has CatA",X has CatA]?,
  ["X has CatB",X has CatB]?,
  ["X has CatX",X has CatX]]?;


\end{aldor}


\begin{axiom}
main3()
)clear completely
\end{axiom}


So the problem (wild guess) is that the compiler Has problems with  
seeing that the if statement gives CatX? in both branches of the if  
statement. Mainly because the types of A and B aro not equal. However, you  
can hint the compiler. My code is telling him "The if part gives CatX? and  
the else part gives CatX?". Then the compiler can infer, that the whole  
"if" statement gives CatX?. And it is at least the type of X (which is  
CatX?). So it matches.


\begin{aldor}
#include "axiom"
import from Integer;
define CatA?: Category == with;
define CatB?: Category == with;
define CatX?: Category == with;
A: Join(CatX?, CatA?) == add;
B: Join(CatX?, CatB?) == add;


MyPkg?(X: CatX?): with {isA?: () -> Boolean} == add {
        isA?(): Boolean == X has CatA?;
}
main4(n:Integer): Boolean == {
        X: CatX? == if zero? n then (A@CatX?) else (B@CatX?);
        isA?()$MyPkg?(X);
}
\end{aldor}


\begin{axiom}
main4(0)
main4(1)
)clear completely
\end{axiom}


In the following code we have the correspondence:

    A      <--> B
    String <--> with
    "x"    <--> String
    "y"    <--> Integer





\begin{aldor}
#include "axiom"
define CatA?(s: String): Category == with;
A(s: String): CatA?(s) == add;


define CatB?(s: with): Category == with;
B(s: with): CatB?(s) == add;


rhxmain(): List Record(s: String, b: Boolean) == [
    ["A x has CatA x", (A("x") has CatA("x"))]?,
    ["A y has CatA x", (A("y") has CatA("x"))]?,
    ["B String has CatB String", (B(String)  has CatB(String))]?,
    ["B Integer has CatB String",(B(Integer) has CatB(String))]?
];
\end{aldor}


The interesting part is that the truth value of the second and fourth list elements do not agree.
\begin{axiom}
rhxmain()
)clear completely
\end{axiom}



An example of a domain-valued variable
\begin{aldor}
#include "axiom"
#pile


main5(n:Integer):List Boolean ==
  local x:IntegralDomain?
  local y:Category
  if n=1 then
    y := Field
  else
    y := Ring


  x := Integer
  test1:Boolean := x has y
  x := Fraction Integer
  test2:Boolean := x has y
  [test1,test2]?
\end{aldor}




\begin{axiom}
main5(1)
main5(2)
)clear completely
\end{axiom}


The compiler checks static types.
\begin{aldor}
#include "axiom"
#pile


main6():List Boolean ==
  local x:IntegralDomain?
  x := Integer
  test1:Boolean := x has Field
  x := String
  test2:Boolean := x has Field
  [test1,test2]?
\end{aldor}




But note that we cannot define domain-valued variables in
the Axiom interpreter.
\begin{axiom}
  x:IntegralDomain?
\end{axiom}





Try to write a self-describing domain --Bill Page,  Wed, 26 Jul 2006 06:28:37 -0500 reply
\begin{aldor}
#include "axiom"
#pile


MyDom?: with
  sigs:List Category
  add2:(MyDom?,MyDom?) -> MyDom?
  sub2:(MyDom?,MyDom?) -> MyDom?
  neg: MyDom? -> MyDom?
 == add
  import from Integer
  Rep == Integer
  sigs:List Category ==
    [with {add2:(MyDom?,MyDom?)->MyDom?},
     with {sub2:(MyDom?,MyDom?)->MyDom?},
     with {neg:MyDom?->MyDom?}]


  add2(x:%,y:%):% == per(rep(x) + rep(y))
  sub2(x:%,y:%):% == per(rep(x) - rep(y))
  neg(x:%):% == per(-rep(x))




main8():List Boolean ==
  import from ListFunctions2?(Category,Boolean)
  map((i:Category):Boolean+->(MyDom? has i), sigs$MyDom?)
\end{aldor}




\begin{axiom}
)sh MyDom?
main8()
\end{axiom}




    Some or all expressions may not have rendered properly,
    because Axiom returned the following error:
Error: export FRICAS=/usr/local/lib/fricas/target/x86_64-unknown-linux; export ALDORROOT=/usr/local/aldor/linux/1.1.0; export PATH=$ALDORROOT/bin:$PATH; export HOME=/var/zope2/var/LatexWiki; ulimit -t 600; export LD_LIBRARY_PATH=/usr/local/lib/fricas/target/x86_64-unknown-linux/lib; LANG=en_US.UTF-8 $FRICAS/bin/FRICASsys < /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/6598524089962682384-25px.axm
/bin/sh: /usr/local/lib/fricas/target/x86_64-unknown-linux/bin/FRICASsys: not found
Some or all expressions may not have rendered properly, because Latex returned the following error:
This is pdfTeXk, Version 3.141592-1.40.3 (Web2C 7.5.6)
 \write18 enabled.
 %&-line parsing enabled.
entering extended mode
(./1608597482377099233-16.0px.tex
LaTeX2e <2005/12/01>
Babel <v3.8h> and hyphenation patterns for english, usenglishmax, dumylang, noh
yphenation, arabic, farsi, croatian, ukrainian, russian, bulgarian, czech, slov
ak, danish, dutch, finnish, basque, french, german, ngerman, ibycus, greek, mon
ogreek, ancientgreek, hungarian, italian, latin, mongolian, norsk, icelandic, i
nterlingua, turkish, coptic, romanian, welsh, serbian, slovenian, estonian, esp
eranto, uppersorbian, indonesian, polish, portuguese, spanish, catalan, galicia
n, swedish, ukenglish, pinyin, loaded.
(/usr/share/texmf-texlive/tex/latex/base/article.cls
Document Class: article 2005/09/16 v1.4f Standard LaTeX document class
(/usr/share/texmf-texlive/tex/latex/base/size12.clo))
(/usr/share/texmf-texlive/tex/latex/ucs/ucs.sty
(/usr/share/texmf-texlive/tex/latex/ucs/data/uni-global.def))
(/usr/share/texmf-texlive/tex/latex/base/inputenc.sty
(/usr/share/texmf-texlive/tex/latex/ucs/utf8x.def))
(/usr/share/texmf-texlive/tex/latex/bbm/bbm.sty)
(/usr/share/texmf-texlive/tex/latex/jknapltx/mathrsfs.sty)
(/usr/share/texmf-texlive/tex/latex/base/fontenc.sty
(/usr/share/texmf-texlive/tex/latex/base/t1enc.def))
(/usr/share/texmf-texlive/tex/latex/pstricks/pstricks.sty
(/usr/share/texmf-texlive/tex/generic/pstricks/pstricks.tex
`PSTricks' v1.15  <2006/12/22> (tvz)
(/usr/share/texmf-texlive/tex/generic/pstricks/pstricks.con))
(/usr/share/texmf/tex/latex/xcolor/xcolor.sty
(/etc/texmf/tex/latex/config/color.cfg)
(/usr/share/texmf-texlive/tex/latex/graphics/dvips.def)
(/usr/share/texmf-texlive/tex/latex/graphics/dvipsnam.def)))
(/usr/share/texmf-texlive/tex/latex/graphics/epsfig.sty
(/usr/share/texmf-texlive/tex/latex/graphics/graphicx.sty
(/usr/share/texmf-texlive/tex/latex/graphics/keyval.sty)
(/usr/share/texmf-texlive/tex/latex/graphics/graphics.sty
(/usr/share/texmf-texlive/tex/latex/graphics/trig.sty)
(/etc/texmf/tex/latex/config/graphics.cfg))))
(/usr/share/texmf-texlive/tex/latex/pst-grad/pst-grad.sty
(/usr/share/texmf-texlive/tex/generic/pst-grad/pst-grad.tex
(/usr/share/texmf-texlive/tex/latex/xkeyval/pst-xkey.tex
(/usr/share/texmf-texlive/tex/latex/xkeyval/xkeyval.sty
(/usr/share/texmf-texlive/tex/latex/xkeyval/xkeyval.tex)))
`pst-plot' v1.05, 2006/11/04 (tvz,dg,hv)))
(/usr/share/texmf-texlive/tex/latex/pstricks/pst-plot.sty
(/usr/share/texmf-texlive/tex/generic/pstricks/pst-plot.tex
 v97 patch 2, 1999/12/12
(/usr/share/texmf-texlive/tex/generic/multido/multido.tex
 v1.41, 2004/05/18 <tvz>)))
(/usr/share/texmf-texlive/tex/latex/geometry/geometry.sty
(/usr/share/texmf-texlive/tex/xelatex/xetexconfig/geometry.cfg)


Package geometry Warning: `lmargin' and `rmargin' result in NEGATIVE (-108.405p
t).
    `width' should be shortened in length.


) (/usr/share/texmf-texlive/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `? option.
(/usr/share/texmf-texlive/tex/latex/amsmath/amstext.sty
(/usr/share/texmf-texlive/tex/latex/amsmath/amsgen.sty))
(/usr/share/texmf-texlive/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texmf-texlive/tex/latex/amsmath/amsopn.sty))
(/usr/share/texmf-texlive/tex/latex/amsfonts/amsfonts.sty)
(/usr/share/texmf-texlive/tex/latex/amsfonts/amssymb.sty)
(/usr/share/texmf-texlive/tex/latex/amscls/amsthm.sty)
(/usr/share/texmf-texlive/tex/latex/setspace/setspace.sty
Package: `setspace 6.7 <2000/12/01>
) (/usr/share/texmf-texlive/tex/generic/xypic/xy.sty
(/usr/share/texmf-texlive/tex/generic/xypic/xy.tex Bootstrap'ing: catcodes,
docmode, (/usr/share/texmf-texlive/tex/generic/xypic/xyrecat.tex)
(/usr/share/texmf-texlive/tex/generic/xypic/xyidioms.tex)
 Xy-pic version 3.7 <1999/02/16>
 Copyright (c) 1991-1998 by Kristoffer H. Rose <krisrose@ens-lyon.fr>
 Xy-pic is free software: see the User's Guide for details.




Loading kernel: messages; fonts; allocations: state, direction,
utility macros; pictures: \xy, positions, objects, decorations;
kernel objects: directionals, circles, text; options; algorithms: directions,
edges, connections;  Xy-pic loaded))
(/usr/share/texmf-texlive/tex/generic/xypic/xyall.tex
 Xy-pic option: All features v.3.3
(/usr/share/texmf-texlive/tex/generic/xypic/xycurve.tex
 Xy-pic option: Curve and Spline extension v.3.7 curve, circles, loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xyframe.tex
 Xy-pic option: Frame and Bracket extension v.3.7 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xycmtip.tex
 Xy-pic option: Computer Modern tip extension v.3.3
(/usr/share/texmf-texlive/tex/generic/xypic/xytips.tex
 Xy-pic option: More Tips extension v.3.3 loaded) loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xyline.tex
 Xy-pic option: Line styles extension v.3.6 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xyrotate.tex
 Xy-pic option: Rotate and Scale extension v.3.3 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xycolor.tex
 Xy-pic option: Colour extension v.3.3 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xymatrix.tex
 Xy-pic option: Matrix feature v.3.4 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xyarrow.tex
 Xy-pic option: Arrow and Path feature v.3.5 path, \ar, loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xygraph.tex
 Xy-pic option: Graph feature v.3.7 loaded) loaded)
(/usr/share/texmf-texlive/tex/latex/tools/verbatim.sty)
(/usr/share/texmf/tex/latex/graphviz/graphviz.sty
(/usr/share/texmf-texlive/tex/latex/psfrag/psfrag.sty))
(/usr/share/texmf/tex/latex/sagetex.sty
Writing sage input file 1608597482377099233-16.0px.sage
) (/usr/share/texmf-texlive/tex/latex/gnuplottex/gnuplottex.sty
(/usr/share/texmf-texlive/tex/latex/base/latexsym.sty)
(/usr/share/texmf-texlive/tex/latex/moreverb/moreverb.sty)
(/usr/share/texmf-texlive/tex/latex/base/ifthen.sty))
(./1608597482377099233-16.0px.aux)
(/usr/share/texmf-texlive/tex/latex/ucs/ucsencs.def)
(/usr/share/texmf-texlive/tex/latex/base/t1cmtt.fd)


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 123.


 You can't use `macro parameter character #' in vertical mode.
l.125 #
       include "axiom"
[1]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 148.


 You can't use `macro parameter character #' in vertical mode.
l.150 #
       include "axiom"
[2]
 You can't use `macro parameter character #' in vertical mode.
l.162 #
       include "axiom"
[3]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 178.


 You can't use `macro parameter character #' in vertical mode.
l.180 #
       include "axiom"
[4]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 195.


 You can't use `macro parameter character #' in vertical mode.
l.197 #
       include "axiom"
[5]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 207.


 You can't use `macro parameter character #' in vertical mode.
l.209 #
       include "axiom"
[6]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 227.


 You can't use `macro parameter character #' in vertical mode.
l.229 #
       include "axiom"
[7]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 247.


 You can't use `macro parameter character #' in vertical mode.
l.249 #
       include "axiom"
(/usr/share/texmf-texlive/tex/latex/jknapltx/ursfs.fd)
(/usr/share/texmf-texlive/tex/latex/amsfonts/umsa.fd)
(/usr/share/texmf-texlive/tex/latex/amsfonts/umsb.fd)
(/usr/share/texmf-texlive/tex/latex/base/ulasy.fd)
 Extra }, or forgotten $.
l.263 }


 Missing $ inserted.
<inserted text> 
                $
l.264 \end{aldor}
                 \newpage
 Missing } inserted.
<inserted text> 
                }
l.264 \end{aldor}
                 \newpage
[8]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 269.


 You can't use `macro parameter character #' in vertical mode.
l.271 #
       include "axiom"
[9]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 288.


 You can't use `macro parameter character #' in vertical mode.
l.290 #
       include "axiom"
 You can't use `macro parameter character #' in horizontal mode.
l.291 #
       pile
[10]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 312.


 You can't use `macro parameter character #' in vertical mode.
l.314 #
       include "axiom"
 You can't use `macro parameter character #' in horizontal mode.
l.315 #
       pile
[11]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 328.


 You can't use `macro parameter character #' in vertical mode.
l.330 #
       include "axiom"
 You can't use `macro parameter character #' in horizontal mode.
l.331 #
       pile
 Missing $ inserted.
<inserted text> 
                $
l.355 \end{aldor}
                 \newpage
[12]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 359.


[13] (./1608597482377099233-16.0px.aux) )
(see the transcript file for additional information)
Output written on 1608597482377099233-16.0px.dvi (13 pages, 8544 bytes).
Transcript written on 1608597482377099233-16.0px.log.