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 think, I have not clearly understood why *you* say that the code is
| invalid.
(1) the current compiler does not allow for a variable to have
different modes in the same scope -- see, for example, nested
function modeCompare in intersectionContour().
(2) the rest of the compiler makes the assumption that a given
variable has exactly one mode, independently of the use context.
(see previous discussion on literals).
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'.
| 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".
Another point of view is that it is clear what the type of the
variable should be: the variable does not exist at all, in a model
where branches of if-statements carries their own scopes.
| According to the Aldor specification, it is not
| allowed that a variable has different types in the same scope.
Same is true in all Axioms.
| 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.
|
| > | 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. ;-)
well, I'm a legacy looking forward guy :-)
| But earnestly, I think it is unnecessary.
strictly speaking, nothing is necessary, starting with overloading.
If would be sufficient to have binary editors :-)
| I have never felt a need for having an extra scope for if's.
OK, but would you oppose others to have it?
| Branches should be short anyway
Except when they are not -- as in almost every interesting algebra file.
Note that '=>' if a short for `if-then-else'.
| and if one wants to have more computations inside the
| "then" and "else", why not calling two functions there?
Why would one _have_ to, if the computation is expressed in 2-3 lines?
| 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.
I prefer to have a language where the expression of the ideas match
the conceptual meaning. If the variable is conceptually local, then I
would like the language to support the expression of that idea.
|
| > 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).
For this _particular instance_ of the pattern, yes. But, what about
the general pattern?
| I believe that not having an extra scope for "if" forces the
| programmer to be more careful with the length of the branches.
I don't think in the case we are discussing, the program was not
careful. In fact, I believe the programmer was careful at the
conceptual level. It is only the compiler that fails to support the
expression of the concpetual ideas.
| So in
| some sense I believe it makes the code more readable. (... oh oh... I
| believe...)
yeah, we are all believers in some ways.
In fact, except for the declaration of the local variable `d', I think
the code was more readable without the manual mangling of the name --
it gave same name to conceptually same thing, and the computations
were 2-3 liners.
|
| > | 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.
As I noted, that is a bug that I was planning to fix, the fix of which
led me to look into why we got the `semantic error' in the first place.
-- 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
