Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha80/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes:
(1) A bug in the AU greedy matcher provoked by:

fmod AU_GREEDY_BUG is
  op l : List List -> List [assoc id: nil] .
  op nil : -> List .

  sort List Elt .
  subsort Elt < List .

  ops a b : -> Elt .

  var E : Elt .
  var M N : List .

  op f : List -> List .
  eq f(l(E, M, N)) = M .
endfm

red f(l(a, b)) .


(2) A really subtle bug in the AU Boyer-Moore based matcher provoked
by: 

mod AU_META is
  sort S .
  op l : S S -> S [assoc] .
  ops a b c d e : -> S .
  op g : S -> S .
  rl [1]: l(g(a), g(X:S)) => e .
endm

red in META-LEVEL :
metaXapply(
  ['AU_META],
  'l['b.S, 'g['a.S], 'g['b.S], 'c.S, 'd.S],
  '1,
  none,
  0, 0, 0) .


red in META-LEVEL :
metaXapply(
  ['AU_META],
  'l['b.S, 'g['a.S], 'g['b.S], 'c.S, 'd.S],
  '1,
  'X:S <- 'b.S,
  0, 0, 0) .

The problem is that since g(X:S) subsumes g(a) so when g(X:S) fails to
match something we get a shift of 2. However in the second example
g(X:S) fails to match g(a) because X:S is bound, and we cannot assume
that the subpattern g(a) will fail on subject g(a) (i.e. a shift of
1). Shifting by 2 causes us to miss the match.
The problem is that subsumption doesn't take account of variables
being bound by some external agency (the META-LEVEL).
The Boyer-Moore based AU matcher is probably overkill... does anyone
have real examples with an A/AU pattern where shifting the pattern
versus the subject benefits from the Boyer-Moore shift table?

Changes
========
(1) The big change is a new term representation along
with new matching and renormalization algorithms for the A and AU
theories. For some simple patterns, this enables rewrites that would
have taken time linear in the size of the subject (using the old
greedy matching) to execute in constant time (using the new greedy
matching). This can be a big win if the subject has thousands of alien
subterms under an A/AU operator. In particular you can now reverse an
associative list in linear time using any of the 3 obvious algorithms
- see revExample.maude - and remember to "unlimit stacksize".
The new representation is only supported for A/AU symbols that:

(a) don't have a 1-sided identity; and
(b) don't have equations that rewrite at the top.

(2) Some optimizations to reduce the number and size of stack frames
needed for deep recursions.

(3) For my convenience:

set print color on .

now colors terms appearing in modules by operator theory according to
the following scheme (previously only rewritten terms were colored
according their reduction status):

AC				red
ACU				magenta
A				green
AU, AUl, AUr			cyan
C, CU, CI CUI			blue
U, Ur, Ul, I, UI, UrI, UlI	yellow
iter, free			black

This color scheme may need to change if more theories are added.

(4) At Jose's request:

  eq f => g = [] (f -> g) .
  eq f <=> g = [] (f <-> g) .

added to model-checker.maude

(5) fmod EXT-BOOL added to prelude.maude

Steven