Dear Maude Abusers,

A new alpha release can be accessed at SRI in

~eker/public_html/Maude/Alpha63e/

or downloaded from

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

Currently only linux is supported. The changes from Alpha63d are:

(1) The following descent functions are now implemented:
      op wellFormed : Module Substitution ~> Bool .
      op metaApply : Module Term Qid Substitution MachineInt ~> ResultTriple? .
      op metaXapply : Module Term Qid Substitution MachineInt
                      MachineInt MachineInt ~> Result4Tuple? .
    They support caching in the case that multiple solutions are
    extracted in order. There are some subtle issues that arise if the
    interpreter is ^C interrupted midway through a metaApply and the
    metamodule it is working on is invalidated by changing a module in
    the database that it depends on.

(2) Operators whose sort structure allows a collapse from the kind
    level to an "output-sort" no longer generate a warning. Back in
    Feb 97 (accoding to my ChangeLog) we made a decision that
    collapsing from an error sort to an non-output-sort (i.e. a sort
    that the operator could not produce) was OK because this trivially
    happens when new sorts are added above in the component. I have
    been unable to reconstruct the justification for making a
    distinction between the non-output-sort case and the output-sort
    case and since we now allow rewriting at the kind level I cannot
    think of anything that might break. Incidently there was a bug in
    the output-sort computation loop that could cause memory
    corruption if the two argument components differed (as they can
    with a one sided identity).

(3) Several memory leaks plugged.

(4) A serious bug in the compilation of conditional collapse rules,
    provoked by an example such as:
	mod FOO is
	  sort Foo .
	  op a : -> Foo .
	  op b : -> Foo .
	  op f : Foo Foo -> Foo [comm] .
	
	  crl [k] : f(Y:Foo, Y:Foo) => Y:Foo
	      if Y:Foo =/= a .
	endm
        rew f(b, b) .
    has been fixed.

There are still several things in the metalevel that remain to be
implemented - the metaMatch/metaXmatch operators and some of the
specials in metamodules. I've slightly modified an old example to
demonstrate metaXapply:

fmod ALL-ONE-STEP-REWRITES is
  including META-LEVEL .
  sort TermSet .
  subsort Term < TermSet .
  op _|_ : TermSet TermSet -> TermSet [assoc comm id: mt ctor] .
  op mt : -> TermSet [ctor] .

  var T : Term .        var M : Module .
  var L : Qid .         var N : MachineInt .

  op findAllRews : Module Term Qid -> TermSet .
  op findAllRewsAux : Module Term Qid MachineInt -> TermSet .

  eq findAllRews(M, T, L) = findAllRewsAux(M, T, L, 0) .

  eq findAllRewsAux(M, T, L, N) =
    if metaXapply(M, T, L, none, 0, maxMachineInt, N) :: Result4Tuple then
      (getTerm(metaXapply(M, T, L, none, 0, maxMachineInt, N)) |
       findAllRewsAux(M, T, L, N + 1))
    else
      mt
    fi .
endfm

red findAllRews(mod 'FOO is
  protecting 'BOOL .
  sorts 'Foo ; 'Bar .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  op 'b : nil -> 'Foo [none] .
  op 'c : nil -> 'Foo [none] .
  op 'f : 'Foo 'Foo -> 'Foo [assoc comm] .
  none
  none
  rl ['k] : 'f['X:Foo, 'Y:Foo] => 'X:Foo .
  rl ['k] : 'a.Foo => 'c.Foo .
endm, 'f['a.Foo, 'b.Foo], 'k) .


Steven