Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha118/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
==========

(1) A memory leak in metaXmatch() where if the subject was
bad, the pattern was not freed. Provoked by:

red in META-LEVEL : metaXmatch(['NAT], 'X:Nat, 'a.Nat, nil, 0, 20, 0) .

(2) A related memory leak in metaXmatch() where if the condition
was bad, neither the pattern nor subject were freed.
Provoked by:

red in META-LEVEL : metaXmatch(['NAT], 'X:Nat, '0.Nat, 'X:Nat = 'b.Nat, 0, 20, 0) .

New features
=============
(1) There are a number of changes and extensions to the
meta-interpreter.

(a) The createInterpreter() message now takes an extra
argument:

  op createInterpreter : Oid Oid InterpreterOptionSet -> Msg [ctor msg format (b o)] .

Currently the only valid value for this argument is "none":

  sorts InterpreterOption InterpreterOptionSet .
  subsort InterpreterOption < InterpreterOptionSet .
  op none : -> InterpreterOptionSet [ctor] .

However this argument will be needed for future developments
and so I'd rather break backward compatibility now (while the
meta-interpreter is not yet documented in the Maude manual)
rather than later.

(b) Return messages from the meta-interpreter hold a
RewriteCount rather than a Nat. Since we define:

  sort RewriteCount .
  subsort Nat < RewriteCount .

this shouldn't break backward compatibility and is needed
for future developments.

(c) Return messages from the metaInterpreter hold a Type rather
than a Sort to avoid the message going to the kind level when
the meta-result is at the kind level.

(d) Sort computations are supported by messages:

  op getLesserSorts : Oid Oid Qid Type -> Msg [ctor msg format (b o)] .
requests the set of sorts that a strictly less than a given type.
The reply has the form:
  op gotLesserSorts : Oid Oid SortSet -> Msg [ctor msg format (m o)] .
If the given type happens to be a kind, the complete set of
sorts in that kind is returned. If the given type happens
to be a minimal sort then the empty set of sorts is returned.

  op getMaximalSorts : Oid Oid Qid Kind -> Msg [ctor msg format (b o)] .
requests the set of sorts that are maximal in a given kind.
The reply has the form:
  op gotMinimalSorts : Oid Oid SortSet -> Msg [ctor msg format (m o)] .

  op getMinimalSorts : Oid Oid Qid Kind -> Msg [ctor msg format (b o)] .
requests the set of sorts that are minimal in a given kind.
The reply has the form:
  op gotMinimalSorts : Oid Oid SortSet -> Msg [ctor msg format (m o)] .

  op compareTypes : Oid Oid Qid Type Type -> Msg [ctor msg format (b o)] .
requests the comparison of two types.
The reply has the form:
  op comparedTypes : Oid Oid Bool Bool Bool -> Msg [ctor msg format (m o)] .
Here the anwser contains 3 Bool flags. The first indicates
whether the types belong to the same kind. The second indicates
whether the first type is <= the second type and the third
flag indicates whether the first type is >= the second type.
Thus this message pair is equivalent to sameKind() and two calls
to sortLeq() in the functional metalevel. The rationale for this
implementation is the cost of calculating this information is
insignificant compared to the processing of an external message
pair.

  op getKind : Oid Oid Qid Type -> Msg [ctor msg format (b o)] .
requests the kind where the given type resides.
The reply has the form:
  op gotKind : Oid Oid Kind -> Msg [ctor msg format (m o)] .
Note that since the kind is always returned in canonical
form, this obliviates the need for a feature analogous to
completeName() since types that aren't kinds must be regular
sorts and these are always cannonical. Actually completeName()
from the function metalevel is already redundant for this
reason but is retained in the interest of backwards compatibility.

  op getKinds : Oid Oid Qid -> Msg [ctor msg format (b o)] .
requests the set of kinds in a named module.
The reply has the form:
  op gotKinds : Oid Oid KindSet -> Msg [ctor msg format (m o)] .

  op getGlbTypes : Oid Oid Qid TypeSet -> Msg [ctor msg format (b o)] .
requests the set of greatest types that are <= to all the
types in the given type set.
The reply has the form:
  op gotGlbTypes : Oid Oid TypeSet -> Msg [ctor msg format (m o)] .
Note that this generalizes getGlbSorts() in the functional
meta-level since you can pass as many types as you like. In
the degenerate cases of empty or singleton type sets, the
given type set is considered to be its own glb (though of
course kinds are canonicalized). If two or more types
disagree on their kind then the result is the empty type
set, none.

(e) Search is supported by messages:

  op getSearchResult : Oid Oid Qid Term Term Condition Qid Bound Nat -> Msg [ctor msg format (b o)] .
requests a search entirely analogeous to metaSearch(). In paricular
the results are indexed by the last Nat argument. The rationale
for this design is that it is entirely reasonable to get a result,
do some more processing on it using the same meta-intepreter object,
and then resume extracting the next search result. As with the
functional metalevel, state caching makes this efficient.
The reply has the form:
  op gotSearchResult : Oid Oid RewriteCount Term Type Substitution -> Msg [ctor msg format (m o)] .

  op getSearchResultAndPath : Oid Oid Qid Term Term Condition Qid Bound Nat -> Msg [ctor msg format (b o)] .
with reply:
  op gotSearchResultAndPath : Oid Oid RewriteCount Term Type Substitution Trace -> Msg [ctor msg format (m o)] .
are similar, except the search path using the format inherited from
metaSearchPath() is returned as the last argument.

(f) Matching without and with extension is supported by messages:

  op getMatch : Oid Oid Qid Term Term Condition Nat -> Msg [ctor msg format (b o)] .
with reply:
  op gotMatch : Oid Oid RewriteCount Substitution -> Msg [ctor msg format (m o)] .
This is entirely analogeous to metaMatch().

  op getXmatch : Oid Oid Qid Term Term Condition Nat Bound Nat -> Msg [ctor msg format (b o)] .
with reply:
  op gotXmatch : Oid Oid RewriteCount Substitution Context -> Msg [ctor msg format (m o)] .
This is entirely analogeous to metaXmatch().

(2) There is a -show-pid command line option which prints the
process id to stderr on start up - intended for use with the
kill -INFO (Mac), kill -USR1 (Linux) feature.

(3) There are two new built-in functions in fmod STRING:

  op upperCase : String -> String .
  op lowerCase : String -> String .

These convert alphabetic characters in the string to upper case
and lower case respectively. Requested by Carolyn.

Other changes
==============
(1) Ctrl-T (Mac) and kill -USR1 (Linux) now produce a status
report immediately if Maude is blocked on socket operations (which
can only happen if no local rewrites are available), rather
than waiting until the next rewrite happens.

(2) The buffer size for socket reads is increased from 4K to 208K
to match the Linux default.

Steven