Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha92a/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
----------
(1) A bug caused by the on demand construction of BDD encodings of
sort functions introduced in alpha92. The delayed construction of the
the BDD encodings of sort functions meant that  meant that BDD
variables used to encode the argument sorts were not allocated until
after they were first used, cause a BuDDy error. In addition to fixing
the bug, this version traps BuDDy errors and reports them as internal
errors. Provoked by an example of Santiago.

(2) A truly evil bug in the unification sort computation
algorithm. Free variables which were also fresh variables were not
having their sort indices constrained to be valid; and the BDD based
generalized sort computation mechanism doesn't enforce this, and
in general can't because there may not be an invalid sort index in the
range kind to mapped invalid domain sort indices to. Reported by
Paco, and provoked by this simplified example:

fmod FOO is
  sorts Int Nat NzInt NzNat Zero .
  subsorts NzNat < NzInt Nat < Int .
  subsort Zero < Nat .
  op 0 : -> Zero  .
  op + : Int Int -> Int [assoc comm] .
  op + : Nat Nat -> Nat [assoc comm] .

  vars M  : NzNat .
  vars I J : [Int] .
endfm

unify +(M, I) =? +(0, J) .

(3) A symmetric bug in the narrowing unification code provoked by:

mod FOO is
  sorts Int Nat NzInt NzNat Zero .
  subsorts NzNat < NzInt Nat < Int .
  subsort Zero < Nat .
  op 0 : -> Zero  .
  op + : Int Int -> Int [assoc comm] .
  op + : Nat Nat -> Nat [assoc comm] .

  vars M  : NzNat .
  vars I J X : [Int] .
  rl +(0, J) => J .
endm

narrow +(M, I) =>+ X .

(4) A performance bug in matching huge highly nonlinear patterns where
Maude would spend an unreasonable amount of time doing constraint
propagation analysis during compilation of the pattern. This is only
partly fixed. Bug reported by Santiago.

Other changes
--------------
There is limited support for the strat attribute in the builtin
metalevel operators. The zero in any such strategy must end the
strategy. This is because the metalevel code has no way to run user
equations for a non-final zero without passing control to the free
theory code, nor anyway to replace semi-eager arguments with copies to
avoid evaluating shared lazy arguments.

Really the user shouldn't be messing with builtins anyway, but Grigori
wanted to have:

fmod LAZY is
  pr META-LEVEL .

  op lazyUpTerm : Universal -> Term
        [poly (1) strat(0)
         special (
           id-hook MetaLevelOpSymbol (metaUpTerm)
           op-hook shareWith  (metaReduce : Module Term ~> ResultPair))] .
endfm

red upTerm(1 + 2) .
red lazyUpTerm(1 + 2) .

Perhaps this one extra ascent function should be added to the standard
prelude and the partial support for strat in metalevel builtins not
documented?

Steven