Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha89a/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This is a bug fix release. There are binaries for Darwin on PPC and
x86 and for Linux on x86 and x86-64.

Bug fixes
==========
(1) A bug where a syntax error could leave a renaming containing a
partly created op mapping that lacks a target name, and cause an internal
error. Provoked by this example from Jasmin Blanchette
<jasmin.blanchette@gmail.com>:

fmod MYMOD is
  protecting META-LEVEL *
      (op none : -> Substitution [ctor] -> noSubstitution) .
endfm

This is now handled by giving each op mapping a default target of the
source op when it is created, and updating it to the real target when
and if that part of the operator mapping syntax is parsed.

(2) A bug where the "Maude variable"->"BDD variables" mapping used by
the unification sort computations was passed by value rather than by
reference. This manifests itself as wasted cpu time and memory rather
than an actual bug.

(3) A bug where local substitutions used in branches of C unification
were not being cleared before use. This has the potential to cause
memory corruption.

(4) A bug where unification data structures from old unification
problems were not being deleted, causing internal errors during the
mark phase of the garbage collector if the module that the
unification problem belonged to had been deleted. This is provoked by
the following example:

fmod AC+C is
   sort Elt Set .
   subsort Elt < Set .
   ops a b c d e z : -> Elt .
   op f : Set Set -> Set [assoc comm] .
   op g : Set Set -> Set [comm] .
   vars U V W X Y Z : Set .
   vars A B C D E F : Elt .
 endfm

 fmod UNIFICATION is
   inc META-LEVEL .

   var A : AnalysisList .
   var N : Nat .
   var M : STheory .
   vars L R : Term .
   var S : Substitution .
   var C : Constant .
   var V : Variable .
   var Q : Qid .
   var T : Term .
   var TL : NeTermList .

   sorts Analysis AnalysisList .
   subsort Analysis < AnalysisList .
   op nil : -> AnalysisList [ctor] .
   op _|_ : AnalysisList AnalysisList -> AnalysisList [ctor assoc id: nil format (d d n d)] .

   op badUnifier : Substitution -> Analysis [ctor] .
   op goodUnifier : Substitution -> Analysis [ctor] .

   op analyze : STheory Term Term -> AnalysisList .
   eq analyze(M, L, R) = analyze2(M, L, R, nil, 0) .

   op analyze2 : STheory Term Term AnalysisList Nat -> AnalysisList .
   eq analyze2(M, L, R, A, N) =
     if metaUnify(M, L, R, N) =/= noMatch then
       analyze2(M, L, R, A | check(M, L, R, metaUnify(M, L, R, N)), s N)
     else
       A
     fi .

   op check : STheory Term Term Substitution -> Analysis .
   eq check(M, L, R, S) =
     if metaNormalize(M, instantiate(L, S)) == metaNormalize(M, instantiate(R, S)) then
       goodUnifier(S)
     else
       badUnifier(S)
     fi .

   op instantiate : NeTermList Substitution -> NeTermList .
   eq instantiate(C, S) = C .
   eq instantiate(V, (V <- T) ; S) =  T .
   eq instantiate(V, S) = V [owise] .
   eq instantiate(Q[TL], S) = Q[instantiate(TL, S)] .
   eq instantiate((T, TL), S) = instantiate(T, S), instantiate(TL, S) .
 endfm

 red analyze(['AC+C],
 'g['f['X:Set, 'Y:Set], 'f['X:Set, 'U:Set, 'Z:Set]],
 'g['f['U:Set, 'V:Set], 'f['W:Set, 'A:Elt]]
 ) .

fmod COMBINE is
   inc UNIFICATION .
   inc AC+C .
   vars U V W X Y Z : Set .
   vars A B C D E F : Elt .
   op _=?_ : Set Set -> AnalysisList .
   eq X =? Y = analyze(['AC+C], upTerm(X), upTerm(Y)) .
 endfm

red f(g(X, Y), g(X, Z), U) =? f(g(Y, Z), V) .
red g(f(X, Y), f(X, U, Z)) =? g(f(U, V), f(W, A)) .

Other changes
==============
There is much cleaning of the unification code and an optimization for
AC unification sort computations.

Steven
