Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha89g/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter


Bug fixes
----------
(1) A subtle bug in the AC unification algorithm where the variables
holding the current selection from a Diophantine basis were not being
properly reinitialized if the AC unification subproblem had to be
solved again from scratch - in the example provided by Santiago this
was triggered by two AC unification subproblems when the 2nd had to be
solved from scratch for each solution to the 1st.

(2) The handling of unimplemented theories in unification has been
cleaned up - all unimplemented theories may be freely used in ground
subterms since the resulting subterm can be treated as a fresh
constant. Use of symbols from unimplemented theories on top of
nonground arguments produces a suitable error message. Thus for
example

fmod UNIF-UNSUP is
  sort Foo .
  ops a b  : -> Foo .
  op f : Foo Foo -> Foo [assoc] .
  op i : Foo Foo -> Foo [idem] .
  vars X Y : Foo .
endfm

unify i(b, a) =? i(a, b) .

no longer produces an incorrect unifier. The one execeptional case is
the use of a symbol from an unimplemented theory on top of a unificand
in a xunify problem - here a ground term isn't really ground because
of the need to handle extension and an error message is produced:

xunify f(a, b) =? f(a, b, c) .

Steven