"Bill Page" <[EMAIL PROTECTED]> writes: | On Thu, May 15, 2008 at 6:02 AM, Gabriel Dos Reis wrote: | > Ralf Hemmecke writes: | > | > | > If the scope of 'x' is intended to be global, then the type of 'x' | > | > must be a Union. | > | > x:Union(Integer,Float) | > | > if cond then | > | > x := 1 | > | > else | > | > x := 2.3 | > | | > | Of course that cannot work. What function pointer for | > | multiplication should the compiler put in for the following | > | | > | x := x*x | > | | > | ? Union does not export a multiplication. | > | > True, and given that why | > | > x := x * x | > | > would have to be valid at all? | > | | ??? No, it is not true.
I disagree. See below. | I guess you didn't try it before you wrote ... :-) Did not try what exactly? | The code example I provided works as advertised in both the | interpreter and the SPAD compiler: Again, in this discussion my focus is on the compiler, because it is the one that presents the most challenges: How to generate code for dependent types (that depend not only values but on data flow). The interpreter is a `toy', compared to the rest. Mostly because, the interpreter does a small-step semantics, therefore always holds the most accurate type. The compiler must do a sound abstract interpretation of the code where it has no access to the actual data and control flow. | (1) -> x:Union(Integer,Float) | Type: Void | | (2) -> if 0<1 then x:=1 else x:=2.3 | | (2) 1 | Type: Union(Integer,...) | | (3) -> x := x*x | | (3) 1 | Type: Union(Integer,...) | | (4) -> if 1<0 then x:=1 else x:=2.3 | | (4) 2.3 | Type: Union(Float,...) | | (5) -> x := x*x | | (5) 5.29 | Type: Union(Float,...) For the interpreter, it is not a problem because it always holds the most accurate type, as displayed i the `Type:' annotation. I keep your interpreter code just to show that you did NOT present the same code to the compiler. | --------- | | For the compiler see: | | http://axiom-wiki.newsynthesis.org/SandBoxLexicalScope#bottom | | \begin{spad} | )abbrev domain BBB Bbb | Bbb: with | foo: Integer -> Integer | == add | foo(a: Integer): Integer == | x:Union(Integer,Float) | if a>0 then | x := 1 | else | x := 2.3 | x case Integer => (x*x)::Integer ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Here, you are *manually inserting* the right coercion. This is not the same thing you did in the interpreter case. This is precisely where I was commenting. So, ether you do the same thing in the interpreter and the compiler or you compare oranges to apples. If you're going to manually insert the right coercions, you may just as well declare the variable explicitly as being a Union. You were wondering about `autoCoerce' in another message. They are exactly for this case. Let me explain. When you have a union, usualy you have to do a `case' to take a branch, such as above x case Integer => (x*x)::Integer this is equivalent to if x case Integer then return (x*x)::Integer else ... Now, the compiler keeps track of control flow (see compIf), and when it is in the success branch it knows that that `the Integer branch' is taken -- the environment is augmented with a `condition' property that records the `case expression -- and if you use `x' in that branch where an Integer is used, it will call autoCoerce with Integer as target -- see coerceExtraHard() -- which will insert by right coercion by simple modemap selection. Notice that I extended this mechanism to user defined `case' operator back then when I introduced the Syntax domain. When the compiler is in the `else' branch, it compiles the code in the `inverse environment' -- see compBoolean. The inverse environment is computed by removing all `success' tags from the success environment. In the specific case where your union contains only two branches you have the impression that you don't have to say anything in the else branch, precisely because there remains only one `autoCoerce' for use. If you have more branches you will have to manually chose the `right coercions'. | wholePart(x*x) | \end{spad} | | \begin{axiom} | foo(0) | foo(1) | \end{axiom} | | This outputs 5 and 1 respectively. Even the compiler is smart enough | to select the right * operation given enough context. you manually inserted the coercions, that is a different ball game. Try: )abbrev package BILLPAGE BillPageUnion BillPageUnion(): Public == Private where Public ==> with foo: () -> Void Private ==> add makeU(): Union(Integer,Float) == even? random()$Integer => 1 3.14 foo() == x: Union(Integer,Float) := makeU() y: Union(Integer,Float) := makeU() x ** y -- 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
