Waldek Hebisch <[EMAIL PROTECTED]> writes: | Gabriel Dos Reis wrote: | > | > The definition of the function recip$NormalizationPackage elicites | > a `semantic error' from the compiler because the local variable | > `hesrg' is defined in the two branches of an if-statement with two | > differen types. That looks like a bug to me. Opinion? | > | > recip(p:P,ts:TS): Record(num:P, den:P) == | > -- ASSUME p is invertible w.r.t. ts | > -- ASSUME mvar(p) is algebraic w.r.t. ts | > v := mvar(p) | > ts_v := select(ts,v)::P | > if mdeg(p) < mdeg(ts_v) | > then | > hesrg: Record (gcd : P, coef2 : P) := halfExtendedSubResultantGcd2(ts_v,p)$P | > d: P := hesrg.gcd; n: P := hesrg.coef2 | > else | > hesrg: Record (gcd : P, coef1 : P) := halfExtendedSubResultantGcd1(p,ts_v)$P | > d: P := hesrg.gcd; n: P := hesrg.coef1 | > g := gcd(n,d) | > (n, d) := ((n exquo g)::P, (d exquo g)::P) | > remn, remd: Record(rnum:R,polnum:P,den:R) | > remn := remainder(n,ts); remd := remainder(d,ts) | > cn := remn.rnum; pn := remn.polnum; dn := remn.den | > cd := remd.rnum; pd := remd.polnum; dp := remd.den | > k: K := (cn / cd) * (dp / dn) | > pn := removeZero(pn,ts) | > pd := removeZero(pd,ts) | > [numer(k) * pn, denom(k) * pd]$Record(num:P, den:P) | > | > | | I belive that Axiom creators considered this function legal, | so generating error message would be a bug.
Hmm, could you give me hints at to why they considered the function legal? | OTOH I am not | sure if I want this function to be legal. The function | captures important pattern where in in both branches of | conditional computation is almost the same, but one has to use | different types. One can use different variable names | in both branches, but it also makes sense to use the same | name to stress similarity. The are two separate but losely related issues: (1) What should be the content of the meet of both branches? (2) Should if-statement have their own scopes? In the current semantics, branches of if-statements do not have their own scopes, so the meet environment of an if-statement is the union of environment of both branches. And this is where the error comes in: One cannot declared the same variable in the same environment with different modes. One way is to say that each branch has its own scope, of the if-statement would be OK, but will have a completely different meaning from the one intended -- and the functions would be an error because hesrg will not be visible after the meet point. Another way is saying that the meet contains common variables (with coherent modes); in that case he program will be an error because at the meet point, the variable will have two modes (a bit like today). This option can have its benefit, but I'm not sure it is one that I'm comfortable with. | So I see some benefits of original design. The original design produces an error on the construct. The only reason we don't usually see it is that there is a bug in the compiler (all Axiom flavours) where the compiler fails not to produce a .o -- when it actually says so. | But making | this function illegal would make Spad closer to conventional | languages which has its own advantages. >From my perspective, it is less a desire to be close to conventional languages, than having a clear well-though of semantics that support modularity. I tend to have a preference for localization because, localization plays well with modularization. When you say making the function illegal, do you think it is because you think the declaration from both branches should be exported to the enclosing scope? -- Gaby ------------------------------------------------------------------------- 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
