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 think, I have not clearly understood why *you* say that the code is
invalid. I haven't tested that in Aldor, but even there I would want
that code to be illegal since (as you said) the variable hesrg is
created inside the "if" and it is not clear what type it should have
after the "if". According to the Aldor specification, it is not allowed
that a variable has different types in the same scope. Since "if" does
not introduce a new scope, the above code should be as invalid as
x: A := foo1()
x: B := foo2()
As you know Aldor has a difference between Variables and constants.
The following code is OK in Aldor and prints T and 1.
---BEGIN aaa.as
#include "aldor"
#include "aldorio"
foo1(): Integer -> Boolean == (x: Integer): Boolean +-> true;
foo2(): Integer -> Integer == (x: Integer): Integer +-> x;
main(): () == {
import from Integer;
x: Integer -> Boolean == foo1();
x: Integer -> Integer == foo2();
stdout << x(1)@Boolean << newline;
stdout << x(1)@Integer << newline;
}
main();
---END aaa.as
However, if you replace "==" by ":=" in the main function, then it again
applies that a variable cannot have different types in the same scope.
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.
> | Do you really think because of code such as this, you would have to
> | introduce separate scopes for "then" end "else"?
>
> This is a separate issue.
> It is certainly helped by having separate scope for each branches.
> As you note below, the variable is local to each branch, so why not
> make that supported by the compiler?
I am a legacy guy, you would destroy my understanding of the current
situation. ;-) But earnestly, I think it is unnecessary. I have never
felt a need for having an extra scope for if's. Branches should be short
anyway and if one wants to have more computations inside the "then" and
"else", why not calling two functions there? That would make the "if"
shorter and clearer and you get an extra scope inside the function anyway.
> | The variable hesrg is completely local to each of the branches
> | respectively. It is not needed outside the "if".
> That is not correct for the current compiler point of view (all
> AXIOMs) -- but it is correct at the `conceptual' level.
I, of course, meant the "conceptual level" here. That hesrg is not
locals according to current SPAD or Aldor specification is clear.
> The question is
> whether we should have the compiler match the conceptual understanding.
As you have seen in my previous posting, this particular code can be
made without introducing any "local" variables, if the language is
strong enough (ie, with multivalues or Cross).
I believe that not having an extra scope for "if" forces the programmer
to be more careful with the length of the branches. So in some sense I
believe it makes the code more readable. (... oh oh... I believe...)
> | The code is legacy stuff and is wrong (as you pointed out) because the
> | compiler did not signal an error.
> Again, as I said in the original mail, the compiler *did signal* an
> error. What the compiler did not do was to stop producing a object
> file. But, the compiler did definitely produce an error.
OK, but then I agree the compiler should abort the compilation.
Ralf
-------------------------------------------------------------------------
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
