RE: [Axiom-mail] Equivalence between named domain and %

[Page, Bill]

On Monday, October 16, 2006 7:30 PM Gabriel Dos Reis wrote:

> | >   Consider the following code snipet:
> | >
> | >      )abbrev domain T T
> | >
> | >      Decl := Record(name: Symbol, type: T)
> | >
> | >      T(): Public == Private where
> | >        Public ==> with
> | >          type: Symbol -> %
> | >          decl: (Symbol, %) -> Decl
> | >        Private ==> add
> | >          decl(n,t) == [n,t]
> | >
> | > The SPAD compiler complains on the definition of decl with the
> | > following message
> |
> 
> On Mon, 16 Oct 2006, Page, Bill wrote:
> | Why would you consider the type T itself to be known in the scope
> | where the value of Decl is computed?
> 
> Because inside the definition of T(), % is supposed to refer to the
> domain defined, i.e. T.

Yes that is correct. But you are asking SPAD explicitly to evaluate
Record(name: Symbol, type: T) outside of and *prior to* the definition
of T(). It seems that in the normal mode of operation of the SPAD
compiler this is out of context for T. (But see how this can be
changed below.)

> Notice that the only thing that is needed to be known is the type
> name.

I think it is instructive to see what Aldor says about this
construction:

Decl := Record(name: Symbol, type: T)
^
[L4 C1] #7 (Error) `Decl' is used in a type, so must be constant,
  and so cannot be assigned to.

After correcting the definition, Aldor compiles this thing without
complaint:

-------
#pile
#include "axiom"

Decl == Record(name: Symbol, type: T)

T: Public == Private where
  Public ==> with
    type: Symbol -> %
    decl: (Symbol, %) -> Decl
  Private ==> add
    decl(n:Symbol,t:%):Decl == [n,t]
    type(x:Symbol):% == x pretend %

------

Even more exciting is the fact that using the $bootStrapMode flag
discovered by Waldek the same code is compiled by SPAD without
complaint!

-------
)lisp (setq |$bootStrapMode| t)
)abbrev domain T T

Decl == Record(name: Symbol, type: T)

T(): Public == Private where
  Public ==> with
    type: Symbol -> %
    decl: (Symbol, %) -> Decl
  Private ==> add
    decl(n:Symbol,t:%):Decl == [n,t]
    type(x:Symbol):% == x pretend %

-------

I wonder why '$bootStrapMode t' is not the normal default mode of
operation for SPAD? Is the generated code less efficient?

> 
> | Perhaps you meant to write
> |
> |       Decl := Record(name: Symbol, type: %)
> 
> what would that % refers to?

As far as I know, in SPAD the Type % is not resolved statically at
compile time instead it remains a placeholder for "this domain" in
whatever context it occurs. (In contrast to Aldor.)

> 
> | which seems to compile as expected?
> 
> But, we don't know the compiler is right.  Which is I'm asking.
> 

I don't know. Maybe you need to extend your example to actually
do some computation which tests the semantics and/or take a look
at the generated Lisp code.

Regards,
Bill Page.