Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha93/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This version identifies itself as Maude 2.5 and will be released as
such unless show stoppers are reported.

Bug fixes
---------
(1) A performance bug where right hand sides containing thousands of
AC/ACU symbols could take minutes and gigabytes to semi-compile due to
a quadratic number of arcs in the slot conflict graph. This was made
worse because the default parsing order for infix symbols is right
associative which is the worst possible order for slot conflicts.
This is fixed by the crude heuristic of sorting the arguments to an
AC/ACU symbol and compiling/building the heaviest first. Bug triggered
by a biological specification from Carolyn.

(2) Symmetric performance bug in A/AU theory.

(3) A critical bug in the partial replacement code for A/AU rewriting
with extension - essentially a normalization status was not being
update when part of an A/AU argument list was replaced with a rhs
instance and this could lead to failures to reduce or compute the sort
of the rhs instance, and failure to renormalize the A/AU node.
Illustrated by the following example:

fmod BUG is
  sort Foo .
  ops a b c d e : -> Foo .
  op f : Foo Foo -> Foo [assoc] .
var X : Foo .
  eq f(a, X) = X .  *** X is labeled as being in normal form
  eq f(b, c) = d .  *** partial replace
  eq d = e .
endfm

red f(a, b, c, a) .

Here matching the first equation produced X = f(b, c, a) which is in
theory normal form. Matching the second equation with extension
produces a partial replacement of b, c with d in f(b, c, a) giving
f(d, a). But unless the theory normal form status is revoked, the d
will never be rewritten. This bug was reported by  
Adrián Riesco <ariesco@fdi.ucm.es> in a very complex example where the
failure to revoke the theory normal form status after a partial
replace resulting in AU terms being left nested, with extra parens
occuring in the output; the simplest example I can find is:

fmod BUG2 is
  sort Foo .
  ops a b c d e  : -> Foo .
  op __ : Foo Foo -> Foo [assoc] .
var X : Foo .
  eq d = a b .
  eq a X a = X .  *** X is labeled as being in normal form
  eq b c = a a .  *** partial replace
endfm

red d c e a .

(4) Tabs occuring in string literals are now handled more gracefully
by printing a warning and converting the offending tab to a
space. This only applies to string literals read from a file unless
Maude is run with the -no-tecla flag since tecla eats tabs in command
line input. For example:

fmod FOO is inc STRING .
  op a : -> String .
  eq a = "foo bar\
	baz" .
endfm

fmod FOO2 is inc STRING .
  op a : -> String .
  eq a = "foo bar	baz" .
endfm

fmod FOO3 is
   op a : -> Bool [metadata "a		b"] .
endfm

fmod FOO4 is
   op a : -> Bool [metadata "a\
		b"] .
endfm

Problem reported by Carolyn.

(5) A bug where single token symbols that contains a string literal
subsection were treated as having mixfix syntax. This led to a couple
of issues illustrated by these examples from Traian:

fmod DOESN'T-WORK-UNARY is sort S .
  op lab:"_+_" : S -> S .
endfm

Maude would complain about the number of underscores (0) not matching
the number of arguments (1).

fmod DOESN'T-WORK-CONSTANT is sort S .
  op lab"_+_" : -> S .
endfm

red lab"_+_" .

Maude would generate two parses: a prefix parse and a mixfix parse.

Other changes
--------------
The construction of rhs instances in the free and AC/ACU/A/AU theories
has some minor optimizations. Unification code cleaned up; potential
but undemonstrated bug fixed.

Currently there are binaries for x86 and x86-64 Linux and x86
Darwin. Our PPC Darwin server is currently switched off, and Apple is
no longer releasing new OS versions for this hardware, so it might be
time to discontinue Maude support as well. If anyone wants a PPC
Darwin binary let me know and I will build one on Monday.
Also is there any interest in a x86-64 Darwin build?

I am thinking of only supporting x86-64 on unix like operating
systems (Linux/FreeBSD/Darwin) for the future Maude 3 (aka
multicore-Maude) series so I make use of the 64-bit MMU (via mmap())
to synchronize between the cores.

Steven