Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha130/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
==========
(1) A memory leak in the object level filtered variant unify command.

(2) A bug in the object level filtered variant unify command where
using reserved variable names such as #1:Elt was not being checked
for.

(3) A bug in the meta-printing of strategies where '`{ was generated
rather than '`(. Found and fixed by Rubén.

(4) A bug in unification modulo identity where the operator is treated
as commutative even when it isn't.

fmod U-TEST is
  sort Foo .
  op 1 : -> Foo .
  op f : Foo Foo -> Foo [id: 1] .
  op g : Foo -> Foo .
vars X Y Z : Foo .
endfm

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

Unifier 1
X --> g(#1:Foo)
Z --> #1:Foo
Y --> 1

Unifier 2
X --> f(#2:Foo, g(#1:Foo))
Z --> #1:Foo
Y --> #2:Foo

Here the theory purification code for the f-theory treats it as
being commutative so the second unifier is wrong.

New feature
============
In the functional metalevel, the following descent functions that use
variant unification for narrowing now take an extra argument of sort
VariantOptionSet that can be used to pass the delay and filter
options to variant unification:

  op metaNarrowingApply : Module Term TermList Qid VariantOptionSet
                          Nat -> NarrowingApplyResult? [...] .
			  
  op metaNarrowingSearch : Module Term Term Qid Bound Qid
                           VariantOptionSet Nat ->
                           NarrowingSearchResult? [...] .
			   
  op metaNarrowingSearchPath : Module Term Term Qid Bound Qid
     			       VariantOptionSet Nat ->
                               NarrowingSearchPathResult? [...] .

Likewise in the meta-interpreter, the following messages that use
variant unification for narrowing now take an extra argument of sort
VariantOptionSet that can be used to pass the delay and filter
options to variant unification:

  op getOneStepNarrowing : Oid Oid Qid Term TermList Qid
     			   VariantOptionSet Nat -> Msg [...] .

  op getNarrowingSearchResult : Oid Oid Qid Term Term Qid Bound Qid
     			      	VariantOptionSet Nat -> Msg [...] .

  op getNarrowingSearchResultAndPath : Oid Oid Qid Term Term Qid Bound Qid
     				       VariantOptionSet Nat -> Msg [...] .

In all 6 cases, there is an equation to rewrite the old operator to
the new operator for backwards compatibility.

Other
======
In the release notes for Alpha129, I forget to mention that the
new object level commands for irredundant unification, filtered
variant unification and variant matching all support the
  in <module> :
and
  [nr-of-solutions]
modifiers so you can write:

irredundant unify [1] in BAG : L M =? P Q .
filtered variant unify [1] in ID-UNSORTED : X Y =? W a .
variant match [1] in VARIANT-MATCH-TEST : f(X) <=? g(Y) /\ g(Y) <=? f(b) .

If the end of the solutions has not been detected because of the
  [nr-of-solutions]
modifier, they also support the
  continue .
  continue <nr-extra-solutions> .
commands.

Because they involve rewriting and narrowing, filtered variant
unification and variant matching also support the debug prefix to
start execution in the debugger:

debug filtered variant unify [1] in ID-UNSORTED : X Y =? W a .
debug variant match [1] in VARIANT-MATCH-TEST : f(X) <=? g(Y) /\ g(Y) <=? f(b) .

While in principle these commands support
  debug continue .
  debug continue <nr-extra-solutions> .
in practice the debug prefix has no effect because the only things
that can be traced or halted on in the debugger are rewrite steps and
narrowing steps and with these commands, the point is that all the
rewriting and narrowing is done upfront before the first result is
returned.

Steven