Ralf Hemmecke <[EMAIL PROTECTED]> writes: | On 05/15/2008 03:01 AM, Gabriel Dos Reis wrote: | > Ralf Hemmecke <[EMAIL PROTECTED]> writes: | > | On 05/14/2008 06:27 PM, Gabriel Dos Reis wrote: | > | > Ralf Hemmecke <[EMAIL PROTECTED]> writes: | > | > | On 05/14/2008 05:26 PM, Gabriel Dos Reis wrote: | > | > | > 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? | > | > | | Gaby, this case looks so simple. Rename hesrg in the "then" | > | > branch to | > | > | hesrg2 and to hesrg1 in the "else" branch. | > | > This *particular* case looks simple; I agree. However, I suspect my | > | > question is more about the *pattern* of the code. Said differently, | > | > is this type of code, something that should be valid? (Waldek says | > | > `no', and I tend to agree with him, but for different reasons). | > | | | > I believe that the code could become legal with the same semantics if | > (a) branches of if-statements carry their own scopes; and | > (b) the declaration of `d' is moved just before the `if'. | | The code can also be made legal by changing the definition of | halfExtendedSubResultantGcd1 and halfExtendedSubResultantGcd2 to | return something of type | | Record (gcd: P, coef: P) | | No "1" or "2" in the tag of the second field. *That* is an artificial | complication that is completely unnecessary.
Yes, yes, yes. That would solve this *particular issue*. I'm concerned with the _pattern_. | > | Since | > | "if" does not introduce a new scope, the above code should be as | > | invalid as | > | | x: A := foo1() | > | x: B := foo2() | > Yes, that is what current Axiom compilers do. | > [...] | > | With "==" however, these lines in "main" are (according to the AUG) | > | equivalent to | > | | x(a: Integer): Boolean == foo1()(a); | > | x(a: Integer): Integer == foo2()(a); | > | | I think, you agree that this should be allowed. | > As it current is in all AXIOMs. These issues are orthogonal, I | > think. | | What is orthogonal? That one forbids | | x: A := foo1() | x: B := foo2() | | but allows | | x: A == foo1() | x: B == foo2() No. | if A is X->Y and B is U->V with (X,Y) not identical to (U,V)? | | The problem is that the latter does not work properly in Axiom. | | (1) -> foo1()(x:Integer):Integer == x | Type: Void | (2) -> x: Integer -> Integer == foo1() | Type: Void | (3) -> foo2()(x:Boolean):Boolean == x | Type: Void | (4) -> x: Boolean -> Boolean == foo2() | Type: Void | (5) -> x(true) | There are no library operations named x | Use HyperDoc Browse or issue | )what op x | to learn if there is any operation containing " x " in its name. | | Cannot find a definition or applicable library operation named x | with argument type(s) | Boolean | | Perhaps you should use "@" to indicate the required return type, | or "$" to specify which version of the function you need. | | It looks like a bug, but I cannot exactly say why, because the meaning | of "==" in Axiom is not the same as in Aldor (I believe). You have to decide whether you're talking about the compiler or the interpreter. So far, I thought we have been talking about the compiler. In the interpreter, '==' has a whole different meaning -- from both the compiler and Aldor. | | > | I have never felt a need for having an extra scope for if's. | > OK, but would you oppose others to have it? | | How can I oppose. Open-Axiom is your project. You are the dictator. I You must be right. I therefore end listening to you. -- 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
