Gabriel Dos Reis wrote:
>
> Waldek Hebisch <[email protected]> writes:
>
> | Gabriel Dos Reis wrote:
> | > Waldek Hebisch <[email protected]> writes:
> | >
> | > | But above we need to "expand" where to see what
> | > | type is defined (the 'some category expression' part). Worse,
> | > | freqently we have things like:
> | > |
> | > | SomeFunctor(A : CA, B : CB) : Public == Private where
> | > | CA ==> cata
> | > | CB ==> catb
> | >
> | > I am not sure this is as complicated as it sounds.
> | > I believe all flavours of AXIOM do (or at least used to do) the
> | > following for this where-expression:
> | >
> | > 1. elaborate of the side conditions.
> | > This essentially means that the environment is augmented with
> | > the constant/macro definitions.
> | >
> | > 2. in the resulting environment, pull our types and names from the
> | > parameter declarations.
> | >
> | > 3. elaborate the type declarations in the resulting environment.
> | >
> | > 4. elaborate SomeFunctor(A,B) == Private
> | >
> | >
> | > Did FriCAS change that sequence of events?
> |
> | Yes. Toplevel 'where' is macro expanded (and '==' and ':'
> | contained there are converted to macros). So when compiler sees
> | the code there is _no_ where at toplevel. The reason is
> | that currently compiler need substantial amount of type
> | information. Normally this information is taken from
> | databases, but during bootstap databases contain almost
> | no data. FriCAS collects needed information directly
> | from constructor definitions, but for that needs macro
> | expanded form.
>
> my sense is that it is possible to do that kind of bootstrapping without
> changing the compilation scheme above. At any rate, can you tell me
> whether FriCAS has invalidated the description (i.e. including syntax)
> of the AXIOM book in section 13.2 which uses '==' to define exports and
> implemetations instead of '==>' or 'macro'?
>
For FriCAS 13.2 is valid at least to degree it is valid for
original Axiom. But 13.2 lacks details and is very imprecise.
Given 'first class type' propaganda one can expect the following
to work:
if true then
-- define constructor
....
AFAIK this form is rejected by all Axiom flavours.
Similarly:
Foo : X == Y where
Z ==> f : Integer -> Integer
X ==> with Z
Y ==> add (f(x) == x)
The following apparently worked in original Axiom, but no
longer works in FriCAS:
(Foo : X == Y where X ==> Ring) where Y ==> Integer
OTOH the following works in FriCAS, but failed in original:
Foo : X == Y where
Z ==> Integer -> Integer
X ==> with f : Z
Y ==> add (f(x) == x)
If you think about elaborating declarations in environment,
then failures above are bugs. But examining implementation
we see that implemented model is different and patterns
of working and non working constructs is explained by
the implemented model.
--
Waldek Hebisch
[email protected]
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
