Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha109/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This is an alpha quality release to allow experimentation with a new metalevel interface to variant narrowing.

Changes
========

(1) The constructor for variant has changed; it is now:
  op {_,_,_,_,_} : Term Substitution Nat Parent Bool -> Variant [ctor] .
where the Parent sort is defined thus:

  sort Parent .
  subsort Nat < Parent .
  op none : -> Parent .

The old constructor is no longer supported; both
  op metaGetVariant : Module Term TermList Nat Nat ~> Variant? [...]
and
  op metaGetIrredundantVariant : Module Term TermList Nat Nat ~> Variant? [...]
return variants in this new format. The variant unification descent functions are unaffected by this change.
While this change breaks compatibility with the recent Maude 2.7 release, since variants are a relatively
new feature this shouldn't break too much code, and any break should be easy to patch since the new
functionality is a superset of the old.

The fields are in the new variant constructor are:
  <term, substitution> representation of the variant (as before).

  natural number equal to the largest index of any fresh variable appearing in the variant;
    indices of variables start at one more than at the index passed as the 4th argument of
    the descent function (as before).

  Parent (natural number or none) giving the index (as passed in the last argument of the descent
    function) of the variant from which the current variant is derived in one step. This is a
    new field that allows the derivation tree of the variants to be easily reconstructed.

  Bool is a new field indicating whether there is another variant in the current layer. 

The variant derivation tree is expanded breadth-first, one layer at a time. If Bool flag is false
it means that there are no more variants in the current layer. Asking for the next variant will
force generation of the next layer (for metaGetVariant), and either a variant from the next layer
will be returned or noVariant will be returned if the next layer is empty.
Thus this flag can be used to generate all variants up to a given depth without having to generate
the next layer in order to recognize when we're done.

(2) A new item, meseguerFiniteVariant has been added to the test suite. These is a set of variant
narrowing tests based on examples sent to me by Jose.

Steven