Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha90/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
----------
(1) A bug in the C unification algorithm where constraints could be
lost if the first pairwise unification of subterms failed and the
second succeeded. Illustrated by the following example, derived from
an example of Santiago:

reduce in META-LEVEL : metaUnify(mod 'FOO is
   nil
   sorts 'T .
   none
   op 'u : 'T 'T -> 'T [comm] .
   op 'g : 'T 'T -> 'T [comm] .
   op 'f : 'T 'T -> 'T [comm] .
   op '1 : nil -> 'T [none] .
   none
   none
   none
endm, 'f['f['X1:T,'X2:T],'X3:T] =? 'f['f['Y1:T,'g['Y2:T,'Y3:T]],'u['f 
['Y4:T,'1.T],'Y5:T]], 13, 0) .

(2) A bug in the C unification algorithm that caused it to produce
redundant unifiers that can easiy be avoided. Reported Ralf Sasse and
illustrated by the following example:

fmod TEST is
  sort Foo .
  op f : Foo Foo -> Foo [comm] .
  op a : -> Foo .
  vars X Y : Foo .
endfm

unify f(a, X) =? f(Y, a) .

(3) A bug in the AC unification algorithm where solving two AC
unifications for two or more subterms in the same theory connected by
shared variables could result in a cycle generating more and more AC
unifications until memory fills up. Reported Ralf Sasse and
illustrated by the following example:

fmod TEST is
  sort Foo .
  op g : Foo Foo -> Foo .
  op f  : Foo Foo -> Foo [assoc comm] .
  vars A B M N X Y Z : Foo .
endfm

unify g(f(A, B), f(A, B)) =? g(f(X, Y), f(X, Z)) .

Other changes
--------------
(1) Because of a problem reported by Manuel where the bison stack
overflows when parsing deeply nested parentheses (such as
f(f(f(...)))) I've heavily modified the surface parser. Previously
bubbles of user defined syntax were parsed by a bison parser, which
led to the stack overflow. The shoe horning of bubbles of abitrary
syntax into a LALR(1) framework resulted in an extremely complicated
grammar which I no longer understood.

Now bubbles are handled using custom states in flex and parenthesis
depth is maintained as simple counter. This has a number of other
advantages:

Operator syntax is now uniform across modules, views and
renaming. Previous operators begining with  "(" were allowed naked in
views but had to be enclosed in parentheses for modules and views. The
following examples are now parsed correctly:

fmod FOO is
  sort Foo .
  op (_)f : Foo -> Foo .
endfm

fmod BAR is
  inc FOO * (op (_)f to g) .
endfm

fmod FOO is
  sort Foo .
  op () : -> Foo .
  op f : Foo Foo -> Foo [id: ()] .
endfm

More overparsing is done allowing syntax error recovery in more
situations and more detailed error messages. For example commands that
end in mixfix syntax can now recover from a missing space before the
final period:

red false.

(2) The XG specific metaNarrow descent function now takes a Bool
argument:

  op metaNarrow : Module Term Qid Bound Nat ~> ResultPair? [...] .

If false is passed, the behaviour is as before. If true is passed, in
each state reached, Maude will only apply rules at a single
redex. This drastically cuts the search space at the cost of
completeness. This functionality is also available at the object level
by using "xg-narrow" rather than "narrow".

Steven