Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha85/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This version is a pure alpha release - it is not destined for the
Maude website though of course you may redistribute it under the GPL.
Because of this I have only made binaries for Linux and Darwin.

Bug Fixes
==========
(1) A bug where the up of a kind variable was incorrect; illustrated
by the following code:

fmod FOO is
  sort Foo .
  op a : -> [Foo] .
  op foo : [Foo] -> [Foo] .
  var X : [Foo] .
  eq foo(X) = a .
endfm

red in META-LEVEL : upEqs('FOO, false) .

Bug reported by Manuel.

(2) Operators notFound in fmod STRING and unbounded in fmod
META-MODULE were not declared as constructors. Found by Joe Hendrix
with his sufficient completeness checker.

(3) A bug where FloatOpSymbol hooks were converted to NumberOpSymbol
hooks by the ascent functions; for example:

red in META-LEVEL : upOpDecls('FLOAT, false) .

Bug reported by Joe Hendrix.

(4) A bug where 0.0 ^ -1.0 evaluated to Infinity rather than being
returned unevaluated as a [Float].

(5) A bug where module selectors such as getEqs() were not defined for
theories. Bug reported by Carolyn.


New features
=============
(1) There are now builtin min() and max() functions in NAT, INT and
RAT. Note that these operators are AC and so can be used with any
number of arguments. In order to make the sort structure of max()
associative it turned out to be necessary to a new sort PosRat to RAT.
Otherwise consider the following triple of sorts

Rat Rat NzNat

Since the max of a Rat and a NzNat is necessarily a NzRat, grouping
((Rat Rat) NzNat) yields a NzRat while grouping (Rat (Rat NzNat))
yeilds only a Rat. Adding the sort PosRat fixes this, though all of
the other declarations in RAT need to take PosRat into account.
This feature was requested by Manuel.

(2) The operator glbSorts() which computes the greatest lower bounds
of a pair of sorts in a metamodule now works on types rather than
sorts and is declared:

  op glbSorts : Module Type Type ~> TypeSet [special (...)] .

TypeSets are added and become subsort polymorphic with SortSets and
KindSets; this means that KindSets are now formed by the _;_ operator
rather than the _&_ operator. Also the prec of _;_ is changed from the
default (41) to 43 to allow TypeListSets (see below) to parse
naturally. The empty constant is moved to the new sort EmptyTypeSet to
avoid preregularity issues. The reason the return sort is a TypeSet is
that the result will either be a Kind or a SortSet asn thus a
supersort is needed. This extension was requested by Jose.

(3) A new metalevel operator:

  op maximalAritySet : Module Qid TypeList Sort ~> TypeListSet [special (...)] .

is added. For an operation in metamodule M specified by name F and
domain D, maximalAritySet(M, F, D, S) computes the set of maximal arities
(lists of types) that F could take and have a sort S' <= S. This might
be the empty set if S is small or F is only defined at the kind level.
The sort TypeListSet is added, which is a super sort of both TypeList
(for single sets) and TypeSet (for arities of a unary operator). This
feature was requested Jose.

(4) A new metalevel operator:

  op metaSearchPath : Module Term Term Condition Qid Bound Nat ~> Trace? [special (...)] .

where trace is a list of triples constructed by

  subsort TraceStep < Trace .
  op {_,_,_} : Term Type Rule -> TraceStep [ctor] .
  op nil : -> Trace [ctor] .
  op __ : Trace Trace -> Trace [ctor assoc id: nil format (d n d)] .

metaSearchPath() is complementary to metaSeach() and carries out the
same search, but instead of returning the final state and matching
substitution returns the sequence of states and rules on a path
starting with the reduced initial state and leading to (but not
including) the final state. metaSearchPath() shares caching with
metaSearch() so calling one after the other on the same arguments only
performs a single search. This feature was requested by Carolyn.

(5) There is a new command

  show path labels <number> .

that is like the show path command but only show labels rather than
the full path. This feature was requested Merrill.

(6) The show profile command now shows percentages as well as absolute
rewrite counts. This extension was requested by Manuel.

(7) There is a new command

  set clear rules on/off .

Normally each rewrite or frewrite command and each loop mode
invocation resets the rule state for each symbol. For most symbols the
rule state consists of the next rule to be executed in a round robin
scheme but for counter symbols the rule state consists of the next
number to rewrite to. Setting "clear rules" to "off" means the rule
state will not be reset between commands. This feature (in the special
case of counters) was requested by Jose and Koushik Sen.

Also there a number of changes under the hood: non-ANSI C++ code has
cleaned up, allowing Maude to be compiled with the g++ 3.4.* series of
compilers and the latest versions of Tecla, GMP and BuDDy have been
used.

Steven