|
|
|
last edited 16 years ago by Bill Page |
Edit detail for SandBoxSpeciesCategory revision 3 of 4
| 1 2 3 4 | ||
|
Editor: Bill Page
Time: 2008/11/12 22:07:50 GMT-8 |
||
| Note: Type-safe (rep,per) version with equality | ||
added:
From BillPage Wed Nov 12 22:07:43 -0800 2008
From: Bill Page
Date: Wed, 12 Nov 2008 22:07:43 -0800
Subject: Type-safe (rep,per) version with equality
Message-ID: <20081112220743-0800@axiom-wiki.newsynthesis.org>
The code above appears to be type unsafe because of the use of 'pretend'. OpenAxiom normally expects type-safe code written with 'rep' and 'per' in the following style:
\begin{spad}
)abb category SPECCAT SpeciesCategory
SpeciesCategory(L: SetCategory): Category == SetCategory with
structures: Set L -> List %
)abb domain CHARSPEC CharacteristicSpecies
CharacteristicSpecies(L: SetCategory, n: Integer): SpeciesCategory L
== add
Rep == Set L
coerce(t: %): OutputForm == coerce(rep t)
x=y == rep(x)=rep(y)
structures(s:Set L):List % == if #s = n then [per s] else []
)abb domain SPECIES Species
Species(L: SetCategory): Ring with
coerce: % -> SpeciesCategory L
== add
Rep == Domain
coerce(s: %): OutputForm == rep(s)::OutputForm
coerce(s: %): SpeciesCategory L == rep(s) pretend SpeciesCategory(L)
x=y == rep(x)=rep(y)
0 == per CharacteristicSpecies(L, 0)
1 == per CharacteristicSpecies(L, 1)
\end{spad}
\begin{axiom}
X := 0$Species INT
Y := 1$Species INT
(X=Y)@Boolean
X+Y
\end{axiom}
If a Species is a Ring, how can we define '+' and '*'?
\begin{spad}
)abb category SPECCAT SpeciesCategory
SpeciesCategory(L: SetCategory): Category == SetCategory with
structures: Set L -> List %
name: () -> String
)abb domain CHARSPEC CharacteristicSpecies
CharacteristicSpecies(L: SetCategory, n: Integer): SpeciesCategory L
== add
Rep := Set L
coerce(t: %): OutputForm == coerce(t)$Rep
structures s == if #s = n then [s] else []
name () == concat ["CharacteristicSpecies(", string n, ")"]
)abb domain SPECIES Species
Species(L: SetCategory): Ring with
coerce: % -> SpeciesCategory L
== add
Rep := SpeciesCategory L
coerce(s: %): OutputForm ==
S := s pretend SpeciesCategory(L)
name()$S::OutputForm
coerce(s: %): SpeciesCategory L == s pretend SpeciesCategory(L)
- == CharacteristicSpecies(L, 0) pretend Rep
1 == CharacteristicSpecies(L, 1) pretend Rep
\end{spad}
On Tue, Nov 11, 2008 at 7:38 PM Waldek Hebisch wrote:
Martin wrote:
I did the following experiment.
In FriCAS, I get an error when I uncomment the line containing the Rep in
SPECIES. This does not happen in Open-Axiom. Otherwise, it compiles and I can
do
(1) -> S1 := 1$Species INT
(1) "CharacteristicSpecies(1)"
Type: Species(Integer)
(2) -> S2 := S1::SpeciesCategory INT
You cannot use SpeciesCategory(Integer) or any other category in a
target, coercion, or package-call context.
I am slightly suprized that the file compiles and is doing someting
sensible.
This is message S2IE0014 (normal tactic when looking at simlar cases
is to search src/share/doc/msgs/s2-us.msgs to find message id and
then grep sources to find where the id is used). It appears twice
in i-spec1.boot:
grep -n S2IE0014 *
i-spec1.boot:383: categoryForm?(m) => throwKeyedMsg("S2IE0014",[m])
i-spec1.boot:408: categoryForm?(m) => throwKeyedMsg("S2IE0014",[m])
Try commenting out the checks.
\begin{boot}
import i_-analy
namespace BOOT
--% Handlers for TARGET
- upTARGET t ==
- Evaluates the rhs to a mode,which is used as the target type for -- the lhs. t isnt [op,lhs,rhs]? => nil -- do not (yet) support local variables on the rhs (not $genValue) and or/[CONTAINED(var,rhs) for var in $localVars]? => keyedMsgCompFailure("S2IC0010",[rhs]?) $declaredMode: local := NIL m:= evaluateType unabbrev rhs not isLegitimateMode(m,NIL,NIL) => throwKeyedMsg("S2IE0004",[m]?) --categoryForm?(m) => throwKeyedMsg("S2IE0014",[m]?) $declaredMode:= m not atom(lhs) and putTarget(lhs,m) ms := bottomUp lhs first ms ^= m => throwKeyedMsg("S2IC0011",[first ms,m]?) putValue(op,getValue lhs) putModeSet(op,ms)
--% Handlers for COERCE
- upCOERCE t ==
- evaluate the lhs and then tries to coerce the result to the -- mode which is the rhs. -- previous to 5/16/89, this had the same semantics as -- (lhs@rhs) :: rhs -- this must be made explicit now. t isnt [op,lhs,rhs]? => nil $useConvertForCoercions : local := true -- do not (yet) support local variables on the rhs (not $genValue) and or/[CONTAINED(var,rhs) for var in $localVars]? => keyedMsgCompFailure("S2IC0006",[rhs]?) $declaredMode: local := NIL m := evaluateType unabbrev rhs not isLegitimateMode(m,NIL,NIL) => throwKeyedMsg("S2IE0004",[m]?) --categoryForm?(m) => throwKeyedMsg("S2IE0014",[m]?) $declaredMode:= m -- 05/16/89 (RSS) following line commented out to give correct -- semantic difference between :: and @ bottomUp lhs type:=evalCOERCE(op,lhs,m) putModeSet(op,[type]?) \end{boot}
\begin{axiom} S1 := 1$Species INT S2 := coerce(S1)@SpeciesCategory?(Integer) structures([1]?)$S2 structures([1,2,3]?)$S2 S3 := S1::SpeciesCategory?(Integer) structures([1]?)$S3 structures([1,2,3]?)$S3 \end{axiom}
pretend. OpenAxiom? normally expects type-safe code written with rep and per in the following style:
\begin{spad}
)abb category SPECCAT SpeciesCategory?
SpeciesCategory?(L: SetCategory?): Category == SetCategory? with
structures: Set L -> List %
)abb domain CHARSPEC CharacteristicSpecies? CharacteristicSpecies?(L: SetCategory?, n: Integer): SpeciesCategory? L == add Rep == Set L
coerce(t: %): OutputForm? == coerce(rep t) x=y == rep(x)=rep(y) structures(s:Set L):List % == if #s = n then [per s]? else []
)abb domain SPECIES Species Species(L: SetCategory?): Ring with coerce: % -> SpeciesCategory? L == add Rep == Domain
coerce(s: %): OutputForm? == rep(s)::OutputForm? coerce(s: %): SpeciesCategory? L == rep(s) pretend SpeciesCategory?(L) x=y == rep(x)=rep(y) 0 == per CharacteristicSpecies?(L, 0) 1 == per CharacteristicSpecies?(L, 1) \end{spad}
\begin{axiom} X := 0$Species INT Y := 1$Species INT (X=Y)@Boolean X+Y \end{axiom}
If a Species is a Ring, how can we define + and *?
Some or all expressions may not have rendered properly, because Axiom returned the following error:
Error: export AXIOM=/usr/local/lib/open-axiom/x86_64-unknown-linux/1.3.0-2008-10-16; export ALDORROOT=/usr/local/aldor/linux/1.1.0; export PATH=$ALDORROOT/bin:$PATH; export HOME=/var/zope2/var/LatexWiki; ulimit -t 240; $AXIOM/bin/AXIOMsys < /var/zope2/var/LatexWiki/5387639654975607834-25px.axm Segmentation fault
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 (./5353839341242074957-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/geometry/geometry.sty (/usr/share/texmf-texlive/tex/latex/graphics/keyval.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: `setspace6.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/graphics/graphicx.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/graphics/dvips.def))) (/usr/share/texmf-texlive/tex/latex/graphics/color.sty (/etc/texmf/tex/latex/config/color.cfg) (/usr/share/texmf-texlive/tex/latex/graphics/dvipsnam.def)) (/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 5353839341242074957-16.0px.sage (./5353839341242074957-16.0px.sout)) (/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)) (./5353839341242074957-16.0px.aux) You can't use `macro parameter character #' in horizontal mode. l.76 structures s == if # s = n then [s] else [] (/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) Missing $ inserted. <inserted text> $ l.89
[1]
LaTeX Error: Environment boot undefined.
See the LaTeX manual or LaTeX Companion for explanation. Type H <return> for immediate help. ...
l.96 \begin{boot}
Missing $ inserted. <inserted text> $ l.97 import i_ -analy Missing $ inserted. <inserted text> $ l.99
Missing $ inserted. <inserted text> $ l.116 first ms ^ = m => Missing $ inserted. <inserted text> $ l.120
Overfull \hbox (6.33421pt too wide) in paragraph at lines 102--120 \OML/cmm/m/it/12 declaredMode \OT1/cmr/m/n/12 : \OML/cmm/m/it/12 local \OT1/cmr /m/n/12 := \OML/cmm/m/it/12 NILm \OT1/cmr/m/n/12 := \OML/cmm/m/it/12 evaluateTy peunabbrevrhsnotisLegitimateMode\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 m; NIL; NIL\O T1/cmr/m/n/12 ) =\OML/cmm/m/it/12 > throwKeyedMsg\OT1/cmr/m/n/12 ("\OML/cmm/m/i t/12 S\OT1/cmr/m/n/12 2\OML/cmm/m/it/12 IE\OT1/cmr/m/n/12 0004"\OML/cmm/m/it/12 ; \OT1/cmr/m/n/12 [\OML/cmm/m/it/12 m\OT1/cmr/m/n/12 ]) \OMS/cmsy/m/n/12 ^^@
LaTeX Error: \begin{document} ended by \end{boot}.
See the LaTeX manual or LaTeX Companion for explanation. Type H <return> for immediate help. ...
l.144 \end{boot}
Missing $ inserted. <inserted text> $ l.144 \end{boot}
Overfull \hbox (165.346pt too wide) in paragraph at lines 123--145 \OMS/cmsy/m/n/12 ^^@\OML/cmm/m/it/12 donot\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 yet \OT1/cmr/m/n/12 )\OML/cmm/m/it/12 supportlocalvariablesontherhs\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 not$\OT1/cmr/m/n/12 genValue) and or/[CONTAINED(var,rhs) for var in $\OML/cmm/m/it/12 localVars\OT1/cmr/m/n/12 ] =\OML/cmm/m/it/12 > keyedMs gCompFailure\OT1/cmr/m/n/12 ("\OML/cmm/m/it/12 S\OT1/cmr/m/n/12 2\OML/cmm/m/it/ 12 IC\OT1/cmr/m/n/12 0006"\OML/cmm/m/it/12 ; \OT1/cmr/m/n/12 [\OML/cmm/m/it/12 rhs\OT1/cmr/m/n/12 ])$declaredMode:
Overfull \hbox (46.1639pt too wide) in paragraph at lines 123--145 \OT1/cmr/m/n/12 throwKeyedMsg("S2IE0014",[m]) $\OML/cmm/m/it/12 declaredMode \O T1/cmr/m/n/12 := \OML/cmm/m/it/12 m \OMS/cmsy/m/n/12 ^^@ ^^@\OT1/cmr/m/n/12 05\ OML/cmm/m/it/12 =\OT1/cmr/m/n/12 16\OML/cmm/m/it/12 =\OT1/cmr/m/n/12 89(\OML/cm m/m/it/12 RSS\OT1/cmr/m/n/12 )\OML/cmm/m/it/12 followinglinecommentedouttogivec orrect \OMS/cmsy/m/n/12 ^^@ ^^@\OML/cmm/m/it/12 semanticdifferencebetween \OT1/ cmr/m/n/12 :: [2] [3] [4] [5] [6] (./5353839341242074957-16.0px.aux) ) (see the transcript file for additional information) Output written on 5353839341242074957-16.0px.dvi (6 pages, 5576 bytes). Transcript written on 5353839341242074957-16.0px.log.