Re: [Axiom-developer] Re: fixing SPAD

[Gabriel Dos Reis]

On Sat, 19 May 2007, Waldek Hebisch wrote:

| Gabriel Dos Reis wrote:
| > On Sat, 19 May 2007, Martin Rubey wrote:
| > | Are you saying:
| > | 
| > |   if A and B or C then ...
| > | 
| > | should be, but currently isn't allowed in the context of conditional 
exports?
| > | (I think it is allowed already now.)
| > 
| > I'm saying that we seriously consider the above when A, B or C
| > happen to be patterns (`is form') or attribute queries (`has form').
| > Note that from Spad point of view, they are just predicates.
| > 
| 
| From aggcat.spad.pamphlet:
| 
|    if Entry has SetCategory and % has finiteAggregate then
|       entry?: (Entry,%) -> Boolean
|         ++ entry?(x,u) tests if x equals \axiom{u . i} for some index i.
| 
| Form aggcat2.spad.pamphlet:
| 
|       if B has ListAggregate(R) or not(B has shallowlyMutable) then
|         -- A is a list-oid, and B is either list-oids or not mutable
|         map(f, l) == construct [f s for s in entries l]
| 
| So, as Martin wrote simple boolean operators already work.  I belive
| that there are restrictions, namely that more complicated expressions
| do not work.  I agree that also complicated expressions should be
| allowed, but support (or lack of it) does not cause conceptual or
| practical difficulties: complicated expressions are just syntatic
| sugar for combinations of simple expressions.

I don't see what you guys are trying to make as a point.

    )abbrev domain FOO Foo
    Foo(T: Type): Public == Private where
      Public ==> with
        if T has Ring or T is Double then
           bar: % -> Boolean

      Private ==> add
        if T has Ring or T is Double then
           bar x == false


I'm out of this discussion.

-- Gaby