Dear Maude Abusers,

A new alpha release can be accessed at SRI-CSL in:

~eker/public_html/Maude/Alpha86a/

or downloaded from:

http://www.csl.sri.com/~eker/Maude/Alpha86a/

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This version is a pure alpha release - it is not destined for the
Maude website though of course you may redistribute it under the GPL.
Because of this I have only made binaries for Linux and Darwin.

It largely consists of critical bug fixes and other changes to make
the handling of parameterized modules more compatible with Full
Maude. It _does not_ address the limitations (a)-(e) documented in the
alpha86 release notes and operator mappings in views are still not
implemented.


Bug Fixes
==========
(1) A bug where bound parameters were used for theory checking when
only free parameters should be; exposed by:

fmod FOO{X :: TRIV, Y :: TRIV} is
  sort Foo{X,Y} .
endfm

fmod BAR{X :: TRIV, Y :: TAO-SET} is
  inc FOO{X, TAO-SET}{Y} .
endfm

(2) The "show module" command now prints structured sorts
correctly. Bug reported by Paco.

(3) Instantiation of a parameter by a theory-view now causes the
theory-view name to be placed in parameterized sorts containing that
parameter, as documented in Full Maude portion of the Maude manual. So
for example

LIST{TAO-SET}

will have parameterized sorts NeList{TAO-SET}{X} and List{TAO-SET}{X}
rather than NeList{X} and List{X}. This means that fmod SORTABLE-LIST
in prelude.maude now uses a renaming of these sorts to maintain the
same API:

fmod SORTABLE-LIST{X :: TAO-SET} is
  protecting (LIST{TAO-SET} *
              (sort NeList{TAO-SET}{X} to NeList{X},
               sort List{TAO-SET}{X} to List{X})){X} .
  ...
endfm

Note that the occurrences of X in the renaming refer to the free
parameter X of LIST{TAO-SET} and are not bound by the free parameter
X of SORTABLE-LIST. Thus if SORTABLE-LIST were to use a different
parameter name we would have:

fmod SORTABLE-LIST{Y :: TAO-SET} is
  protecting (LIST{TAO-SET} *
              (sort NeList{TAO-SET}{X} to NeList{X},
               sort List{TAO-SET}{X} to List{X})){Y} .
  ...
endfm

Bug reported by Paco.


Other Changes
==============
(1) Parameterized fmods may now be instantiated with views that have a
mod as their target; the instantiated module is promoted to a mod.

(2) The print mixfix flag is no longer used to decide whether omitable
backquotes are omitted from a structured sort name - they now are
always omitted.

(3) The "show module" and "show all" commands now display the
parameters of parameterized modules.

(4) The naming conventions for modules created on-the-fly have
changed: summations are no longer enclosed in parentheses unless they
are the left argument of a renaming, and renamings are now enclosed in
parentheses if they are subject to an instantiation.

(5) Renaming of modules with bound parameters is no longer
allowed. Thus any renaming of a module must be done before any
instantiation using parameters from the module enclosing the module
expression. This is a pragmatic decision to avoid having to handle the
instantiation of renamings, which seems hard to do in a consistent
way. Renaming of modules with only free parameters (as in
SORTABLE-LIST above) is still OK.

(6) The instantiation of a modules bound parameters is now handled
using the following technique which is an extension of the
(undocumented) technique used by Full Maude. This results in better
sharing properties.

In alpha86, bound parameter instantiation (BPI) was handled exactly
like regular parameter instantiation. Consider for example:

fmod FOO{X :: TRIV} is
  sort Foo{X} .
endfm

fmod BAR{Y :: TRIV} is
  inc FOO{Y} .
endfm

fmod TEST is
  inc BAR{Nat} .
endfm

Here BAR has an import module expression  FOO{Y} that evalutates to a
module FOO{[Y]} (note the []s to distiguish a bound parameter from a
view of the same name). When BAR is instatiated by the view Nat, the
instantiation of FOO{[Y]} by the view Nat would proceed just as if it
were a free parameter to yield FOO{[Y]}{Nat} which would be imported
by BAR{Nat}. As Paco pointed out to me this leads to module sharing
problems such as


fmod FOO{X :: TRIV} is
  inc SET{X} .
endfm

fmod BAR{Y :: TRIV} is
  inc SET{Y} .
  inc FOO{Y} .
endfm

Here BAR would import two modules, SET{[Y]} and FOO{[Y]}, where
FOO{[Y]} imports SET{[X]}{[Y]}. SET{[Y]} and SET{[X]}{[Y]}
essentially have the same contents are are not shared.
Now BPI is handle as a completely different operation, just as in Full
Maude. When a module has bound parameters, the module keeps track of
how it was made. When the bound parameters are instantiated, a new
module is made, using the information on construction from the old
module, but substituting for the bound parameters. Thus in the above
example, FOO{[Y]} would import SET{[Y]} which could be shared.

There are some subtleties with this approach; when a bound parameter
is instantiated by a theory-view it escapes and must be rebound in a
later instantiation. Full Maude minimizes this complication by
restricting use of parameters to final instantiation however alpha86a
allows parameters to be used anywhere in a chain of instantiations and
will recapture those parameters as needed should they end up
instantiated by theory views. Here's an example that shows how the
recapturing happens in a complex case:

view TRIV from TRIV to TRIV is
  sort Elt to Elt .
endv

fmod TRIPLE{X :: TRIV, Y :: TRIV, Z :: TRIV} is
  sort Triple{X,Y,Z} .
endfm

fmod FOO{A :: TRIV, B :: TRIV, C :: TRIV}  is
  inc TRIPLE{TRIV, A, TRIV}{B, C} .
endfm

fmod BAR{I :: TRIV, J :: TRIV, K :: TRIV}  is
  inc FOO{TRIV, J, TRIV}{I, K} .
endfm

show modules .

(7) There is now a -no-advise command line flag that switches off
advisories at start up. This was added just to fix an issue with the
test suite.

(8) Messages targeted at external objects that for some reason cannot
be delivered immediately (perhaps the message is malformed or the
object does not exist or is in the wrong state), now generate
advisories as an aid to debugging.

Steven