Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha91a/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This version is intended to be released as 2.4 assuming no show
stoppers are found and identifies itself as such.

Bug fixes
----------
(1) A bug in the Diophantine solver that caused it to barf on results
over  2^31 - 1.

load linear

*** works
red natSystemSolve(((0,0) |-> 2 ^ 31 - 1 ; (0,1) |-> -1), zeroVector) .

*** fails
red natSystemSolve(((0,0) |-> 2 ^ 31 ; (0,1) |-> -1), zeroVector) .

(2) A bug in the build system that resulted in the .maude files not
being installed in the data directory. Reported by Rick van der Zwet
<rick@wzoeterwoude.net>.

(3) A bug introduced by the free theory discrimination net
optimization of alpha90a, where subsumptions such as

fmod SUBSUMPTION is
  sort Foo .
  ops a b : -> Foo .
  op f : Foo -> Foo .
  var X : Foo .
  eq f(X) = a .
  eq f(a) = b .
endfm

red f(a) .

were no longer being detected. This is an efficiency issue that is
only visible when Maude is compiled in debug mode.

(4) I've fixed a number of incompatibilites with gcc 4.* reported by
Marcel Kyas <kyas@ifi.uio.no>. I've also fixed a number of compiler
warnings.

(5) A bug where subsort overloading an operator f from a parameter and
then subsequently mapping f to a term in a view caused an internal
error on instantiation. For example:

fth T is
  sort Elt .
  op f : Elt -> Elt .
endfth

view V from T to NAT is
  sort Elt to NzNat .
  op f(X:Elt) to term X:NzNat .
endv

fmod MOD{M :: T} is
  op f : M$Elt -> M$Elt .
endfm

fmod TEST is
  protecting MOD{V} .
endfm

This example is adapted from a larger, more realistic example from
Marc Nieper-Wißkirchen <marc@nieper-wisskirchen.de>
This is fixed by disallowing modules to subsort overload operators
from their parameters. Doing so provokes a warning and makes the
parameterized module unusable. For consistancy I have added the same
restriction to parameterized metamodules, although at the moment with
a purely functional metatleve, there is no way such metamodules could
be instantiated.

(6) A stream synchronization bug which occasionally showed up a make
check failure on certain platforms as the interleaving of echoing of
commands to stdout with printing error messages to stderr varied. In
fact the reference order in the test suite was wrong but most
platforms produced this interleaving most of the time.


Other changes
--------------
(1) The unify command now accepts systems of unification problems with the
=? pairs separated by /\ tokens; for
example:

fmod FOO is
  sort Foo .
  ops g h : Foo -> Foo .
endfm

unify g(X:Foo) =? Y:Foo /\ h(X:Foo) =? h(Z:Foo) .

This change was requested by Narciso.

(2) Statements (rule, equations and membership axioms) can now take a
print attribute. This looks like: 

  eq f(X) = b [print "X = " X] .

Here the keyword print is followed by a possibly empty list of items
which each item is a string constant or a variable. Mentioned
variables must actually occur in the statement, with non-occurring
variables being pruned with a warning.

Print attribute mode can be turn on with the command:

set print attribute on .

attribute is a new keyword that can be abbreviated to attr

In print attribute mode, when a statement is executed the items in its
print attribute are printed, with variables taking their value in the
current subsitution. By default a newline is printed following the
items (even if there are no items) but this behavior can be turned off
with the command:

set print attribute newline off .

Print attribute mode is like trace mode, break mode and profile mode
in that all execution takes the slow path. This is true even if no
print attributes are encountered.

Since Maude has few restrictions on variable names it is possible to
introduce ambiguity by using strings or attribute names as variables:

mod AMBIGUOUS is
  sort Foo .
  op a : -> Foo .
  ops f g h : Foo -> Foo .
vars metadata "here" : Foo .
  eq f("here") = g("here") [print "here"] .
  rl g(metadata) => h(metadata)
    [print "metadata = " metadata "g->h rule"] .
endm

In this case Maude reports the ambiguity and you get whichever parse
MSCP10 finds first.

The print attribute is reflected by the operator

  op print : QidList -> Attr [ctor] .

where each Qid in the possibly empty QidList must be a metastring, say
'"X = " or a metavariable, say 'X:Foo that occurs in the
metastatement. As with metalevel tracing, the value of a variable in a
substitution created during metarewriting is printed out as an object
level term.

(3) Diophantine equations arising from unification problems are now
solved over ints that than GMP bignums although the performance
improvement on most unification problems is likely to be small.

Steven