"Bill Page" <[EMAIL PROTECTED]> writes:
[...]
| >> Does it apply to all types?
| >
| > Almost -- except function types, which is already weird in
| > all AXIOM systems.
| >
| >> What
| >> happens if I write:
| >>
| >> x:Polynomial Integer
| >>
| >> without providing any value. Is 'x' evaluated as Symbolic Polynomial
| >> Integer? If not, how is that prevented?
| >
| > the *expression* x evaluates to a Symbolic Polynomial Integer.
| > The type of of the *variable* x remains Polynomial Integer in the
| > evaluation environment.
| >
|
| It occurs to me that I do not understand how interpreter avoids the message:
|
| x is declared as being in Polynomial Integer but has not been given a value
|
| when used in an expression like the following:
|
| p:=x+1
|
| although experience shows it does and the result is of type
| 'Polynomial Integer'. So this would represent a potentially
| significant change in behavior. If the result will be 'Symbolic
| Polynomial Integer' then I presume that I will have to write something
| like:
|
| x:='x
|
| and then re-evaluate p in order to get 'Polynomial Integer'. Is there
| another way? Or does it get more complicated? I wonder if having two
| "levels" of symbolic expressions such as in this case, might sometimes
| lead to confusion.
There are various shortcuts in bottomUpIdentifier. The one you are
looking for is this (existing unmodified OpenAxiom):
-- 1. declared mode but no value case
(m := getMode t) =>
m is ['Mapping,:.] => throwKeyedMsg('"S2IB0003",[getUnname t])
-- hmm, try to treat it like target mode or declared mode
if isPartialMode(m) then m := resolveTM(['Variable,id],m)
-- if there is a target, probably want it to be that way and not
-- declared mode. Like "x" in second line:
-- x : P[x] I
-- y : P[x] I
target and not isSub and
(val := coerceInteractive(objNewWrap(id,['Variable,id]),target))=>
putValue(t,val)
[target]
-- Ok, see if we can make it into declared mode from symbolic form
-- For example, (x : P[x] I; x + 1)
not target and not isSub and m and
(val := coerceInteractive(objNewWrap(id,['Variable,id]),m)) =>
putValue(t,val)
[m]
-- give up
throwKeyedMsg('"S2IB0004",[id,m])
I thought a systematic rule was better that one with lot os special
cases. If people feel strongly that the existing beahviour needs to
be preserved, then that makes `soundness proof' even more harder to
attain. But, I'm open to suggestions.
Note how
-- Ok, see if we can make it into declared mode from symbolic form
-- For example, (x : P[x] I; x + 1)
not target and not isSub and m and
(val := coerceInteractive(objNewWrap(id,['Variable,id]),m)) =>
putValue(t,val)
[m]
is very similar to the proposed Symbolic T in deduction rule and
synthesis of objects.
-- Gaby
-------------------------------------------------------------------------
Sponsored by: SourceForge.net Community Choice Awards: VOTE NOW!
Studies have shown that voting for your favorite open source project,
along with a healthy diet, reduces your potential for chronic lameness
and boredom. Vote Now at http://www.sourceforge.net/community/cca08
_______________________________________________
open-axiom-devel mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
