Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha80a/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter


Bug fixes:
===========
(1) A bug where metadata was not copied on importation:

fmod METADATA is
  sort Foo .
  ops a b : -> Foo .
  eq a = b [metadata "bar"] .
endfm

fmod IMPORTER is inc METADATA .
endfm

show all .
red in META-LEVEL : upEqs('IMPORTER, true ) .


Changes
========
(1) The AC/ACU theory now uses a simpler, faster version of red-black
trees where the size of subtrees are no longer stored in each node.
I've eliminated much special case code that no longer gives a
performance win. One user visible change is that AC/ACU contexts at
the metalevel are no longer flattened. For example:

reduce in META-LEVEL : metaXmatch(fmod 'FOO is
  protecting 'BOOL .
  sorts 'Foo ; 'Bar .
  subsort 'Bar < 'Foo .
  ((op 'f : 'Foo 'Foo -> 'Foo [assoc comm] .
  op 'c : nil -> 'Foo [none] .)
  op 'b : nil -> 'Foo [none] .)
  op 'a : nil -> 'Foo [none] .
  none
  none
endfm, 'f['X:Foo,'Y:Foo], 'f['a.Foo,'b.Foo,'c.Foo,'c.Foo], nil, 0, s_^100(0),
    s_^30(0)) .

used to produce:

rewrites: 1 in 0ms cpu (2ms real) (~ rewrites/second)
result MatchPair: {
	'X:Foo <- 'b.Foo ; 
	'Y:Foo <- 'a.Foo,'f['c.Foo,'c.Foo,[]]}

but will now produce:

rewrites: 1 in 0ms cpu (3ms real) (~ rewrites/second)
result MatchPair: {
	'X:Foo <- 'b.Foo ; 
	'Y:Foo <- 'a.Foo,'f['f['c.Foo,'c.Foo],[]]}


(2) There is a first implementation of object-message rewriting.
The special behaviour is associated with configuration constructors
which must be AC and may optionally have an identity.

  op c : Foo Foo -> Foo [ctor config assoc comm] .

Configuration only have their special behavior wrt arguments that have
object and message constructors on top. Object and message
constructors must have at least one argument:

  op ob : Bar -> Foo [ctor object].
  op m : Bar -> Foo [ctor msg].

An operator can have at most one of the 3 new attributes: config,
object and msg. For object constructors, the first argument is
considered to be the objects name. For message constructors, the first
argument is considered to be the messages target.
There may be multiple configuration, object and message constructors.
A rule is consider to be an object-message rule if all the following
hold:

(a)    Its lhs has a configuration constructor on top with two
       arguments A and B
(b)    A and B are stable (cannot change their top symbol under a
       substitution).
(c)    A has a message constructor on top.
(d)    B has an object constructor on top.
(e)    The first arguments of A and B are identical.

The new behavior appears with the command frewrite and the descent
function metaFrewrite().
When the fair traversal attempts to perform a single rewrite on
a term headed by a configuration constructor, the following happens:

(a)	Arguments headed by object constructors are collected. It is a
	runtime error for more than one object to have the same name.
(b)	For each object, messages with its name as first argument are
	collected and placed in a queue.
(c)	Any remaining argments are placed on a remainder list.
(d)	For each object, and for each message in its queue, an attempt
	is made to deliver the message by performing a rewrite with an
	object-message rule. If all applicable rules fail, the message
	is placed on the remainder list. If a rule succeeds, the rhs
	is constructed, reduced, and the result is searched for the
	object. Any other arguments in the result configuration go
	onto the remainder list. If the object cannot be found, any
	messages left in its queue go onto the remainder list. Once
	its message queue is exhausted, the object itself is placed on
	the remainder list.
(e)	A new term is constructed using the configuration constructor
	on top of the arguments in the remainder list. This is
	reduced, and a single rewrite using the non-message-object
	rules is attempted.

There is no restriction on object names, other than uniqueness. An
object may change its object constructor during the course of a
rewrite and delivery of any remaining message will still be
attempted. If the configuration constructor changes during the course
of a rewrite, the resulting term is considered alien, and does not
participate any further in the object-message rewriting for the
original term. The order in which objects are considered and messages
delivered is system dependent, but note that newly created message are
not delivered until some future visit to the configuration (though
all arguments including new messages and alien configurations could
potentially participate in the single non-message-object rewrite
attempt. Message delivery is "just" rather than "fair" - in order for
message delivery to be guarenteed, an object must always be willing to
accept the message. If multiple object-message rules contain the same
message constructor they are tried in a round robin fashion.
Non-message-object rules are also tried in a round robin fashion for
the single non-message-object rewrite attempt.

The counting of object-message rewrites is strange: For the purposes
of the rewrite argument given to frewrite, a visit to a configuration
that results in one or more rewrites counts as a single rewrite;
though for other accounting purposes all rewrites are counted.
Finally, for tracing, profiling and breakpoints only, there is a fake
rewrite at the top of the configuration in the case that
object-message rewriting takes place but the single non-message-object
rewrite attempt fails. It is not included in the reported rewrite
total, but is inserted to keep tracing consistent.

Object-message rewriting is reflected by

  op config : -> Attr [ctor] .
  op object : -> Attr [ctor] .
  op msg : -> Attr [ctor] .

in fmod META-MODULE.


(3) The nonexec statement attribute is supported. Inadmissable rules,
equations and memberships are required to use it. When a statement
has the nonexec attribute, it is not used for rewriting. Nonexec rules
can be used by metaApply()/metaXapply() and nonexec statements can be
upped with the ascent functions.
As a temporary backward compatibility hack for FullMaude users,
inadmissable rules that don't use nonexec get a warning, but then the
nonexec attributed is then added rather than ignoring the rule.
The nonexec statement attribute is reflected by

  op nonexec : -> Attr [ctor] .

in fmod META-MODULE.

Paco has released Full Maude 80-1 which is compatible with
Alpha80/80a and I have put this in the release directory.
You should not use an older prelude.maude with Alpha80a since the
metalevel hooks have changed.

Steven