Thanks to Gaby, I was looking at the micro-semantics of the loop in the following:
lift?(p1:SUPP,p2:SUPP,uterm:UTerm,ldeg:List NNI, lvar:List OV) : Union(s:SUPP,failed:"failed",notCoprime:"notCoprime") == leadpol:Boolean:=false (listpol,lval):=(uterm.lpol,uterm.lint.first) d:=listpol.first listpol:=listpol.rest nolift:Boolean:=true for uf in listpol repeat --note uf and d not necessarily primitive degree gcd(uf,d) =0 => nolift:=false nolift => ["notCoprime"] f:SUPP:=([p1,p2]$List(SUPP)).(position(uf,listpol)) lgcd:=gcd(leadingCoefficient p1, leadingCoefficient p2) (l:=lift(f,d,uf,lgcd,lvar,ldeg,lval)) case "failed" => ["failed"] [l :: SUPP] 1) Suppose that for all uf in listpol, degree gcd(uf, d) is at least one. In this case, nolift's value after the loop is true, and the function exits with ["notCoprime"]. 2) Otherwise, there is a uf in listpol with degree gcd(uf, d) vanishing. In this case, after the loop, nolift is false after the loop, and uf is the *last* element in listpol OH NO! Who is able to predict the result of foo1 [1,2,0,3] foo2 [1,2,0,3] foo3 [1,2,0,3] after compiling TEST below? Martin )abb package TEST Test Test: with foo1: List Integer -> Integer foo2: List Integer -> Integer foo3: List Integer -> Integer == add foo1 l == tst := true for e in l repeat output(e::OutputForm)$OutputPackage e = 0 => tst := false tst => -1 e foo2 l == tst := true for e in l repeat e = 0 => tst := false output(e::OutputForm)$OutputPackage tst => -1 e foo3 l == tst := true for e in l repeat e = 0 => tst := false tst => -1 e ------------------------------------------------------------------------- This SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio 2008. http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel