Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha117/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

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

(1) A bug in the new parser where the location of a syntax error
caused by too large a precedence could detected one token too far
to the right. Provoked by the following example:

fmod FOO is
  sort Foo .
  op a_ : Foo -> Foo [prec 1 gather(e)] .
  op b_ : Foo -> Foo [prec 1] .
  op c : -> Foo .
endfm

parse a b c .

Here b is the problem because it has prec 1 while a_ demands prec 0
for it's argument, however c was reported as being the problem.

(2) A bug where views that become stale because of modules changing
under them do not get re-evaluated by show view shown by the following
example:

fmod FOO is
  op _+_ : Bool Bool -> Bool [prec 10] .
  op p_ : Bool -> Bool [prec 20] .
endfm

view V from STRICT-TOTAL-ORDER to FOO is
  sort Elt to Bool .
  op X:Elt < Y:Elt to term p X:Bool + Y:Bool .
endv

show view V .

fmod FOO is
  op _+_ : Bool Bool -> Bool [prec 20] .
  op p_ : Bool -> Bool [prec 10] .
endfm

show view V .

Here the mapping for _<_ has been deleted because V is stale.

(3) A symmetric bug in upView(); shown by the following
example:

fmod FOO is
  op _+_ : Bool Bool -> Bool [prec 10] .
  op p_ : Bool -> Bool [prec 20] .
endfm

view V from STRICT-TOTAL-ORDER to FOO is
  sort Elt to Bool .
  op X:Elt < Y:Elt to term p X:Bool + Y:Bool .
endv

red in META-LEVEL : upView('V) .

fmod FOO is
  op _+_ : Bool Bool -> Bool [prec 20] .
  op p_ : Bool -> Bool [prec 10] .
endfm

red in META-LEVEL : upView('V) .

(4) A bug in the meta-interpreter where imports were omitted
when replying to a showModule message requesting an unflattened
module:

load metaInterpreter

mod TEST is
  pr META-INTERPRETER .

  op FOO : -> Module .
  eq FOO = (
    fmod 'FOO is
      nil
      sorts 'Foo .
      none
      op 'a : nil -> 'Foo [none] .
      op 'b : nil -> 'Foo [none] .
      none
      eq 'a.Foo = 'b.Foo [none] .
    endfm ).

  op BAR : -> Module .
  eq BAR = (
    fmod 'BAR is
      including 'FOO .
      sorts none .
      none
      none
      none
      none
    endfm ).

  op me : -> Oid .
  op User : -> Cid .

  var X Y Z : Oid .
  var N : Nat .
  var T : Term .
  var S : Sort .

  sort State .
  ops 1 2 3 4 : -> State [ctor] .
  op state:_ : State -> Attribute [ctor] .

  rl < X : User | state: 1 > createdInterpreter(X, Y, Z) => < X : User | state: 2 >
       insertModule(Z, X, FOO) .

  rl < X : User | state: 2 > insertedModule(X, Y) => < X : User | state: 3 >
       insertModule(Y, X, BAR) .

  rl < X : User | state: 3 > insertedModule(X, Y) => < X : User | state: 4 > 
       showModule(Y, X, 'BAR, false) .
endm

erew  <> 
< me : User | state: 1 > 
createInterpreter(interpreterManager, me) .

(5) A bug in the erewrite command where doing a control-C
interrupt followed by an abort command resulted in a hang:

mod FOO is
  sort Foo .
  ops a b : -> Foo .

  rl a => b .
  rl b => a .
endm

erew a .

^C

abort .

(6) A bug where doing object-message rewriting caused a crash
when used with

set clear rules off .

because various data structures need for object-message rewriting
were not being initialized properly. Illustrated by:

mod TEST is
  including CONFIGURATION .
  op m   : Oid Oid -> Msg [msg] .
  ops 1 2 : -> Oid .
  op User : -> Cid .

  var A : AttributeSet .
  vars X Y : Oid .

  rl < X : User | A > m(X, Y) => < X : User | A > m(Y, X) .
endm

set clear rules off .

frew [1] < 1 : User | none > m(1, 2) .

(7) A related bug in the meta-interpreter where the next rule
to try pointers were not being reset with the rewriteTerm() and
frewriteTerm() messages. Illustrated by:

load metaInterpreter

mod FOO is
  sort Foo .
  ops a b c : -> Foo .
  rl a => b .
  rl a => c .
endm

mod TEST is
  pr META-INTERPRETER .

  op me : -> Oid .
  op User : -> Cid .

  vars X Y Z : Oid .
  var T : Term .
  var S : Sort .
  var A : AttributeSet .
  var N : Nat .

  op prev:_ : Term -> Attribute [ctor] .

  rl < X : User | A > createdInterpreter(X, Y, Z) => < X : User | A >
       insertModule(Z, X, upModule('FOO, true)) .

  rl < X : User | A > insertedModule(X, Y) => < X : User | A >
       rewriteTerm(Y, X, unbounded, 'FOO, 'a.Foo) .

  rl  < X : User | none > rewroteTerm(X, Y, N, T, S) => < X : User | prev: T >
       rewriteTerm(Y, X, unbounded, 'FOO, 'a.Foo) .
endm

*** second rewriteTerm returns different result from first.
erew  <> 
< me : User | none > 
createInterpreter(interpreterManager, me) .


(8) A bug where modules cached by the functional metalevel
were incorrectly being used by the meta-interpreter. Illustrated
by the following example:

fmod FOO is
  sort Foo .
  ops a b : -> Foo .
  eq a = b .
endfm

load metaInterpreter 

mod TEST is
  pr META-INTERPRETER .
  op me : -> Oid .
  op User : -> Cid .
  op state:_ : Nat -> Attribute .

  vars X Y Z : Oid .

  rl < X : User | state: 0 > createdInterpreter(X, Y, Z) =>
     < X : User | state: 1 > insertModule(Z, X, foo) .

  rl < X : User | state: 1 > insertedModule(X, Y) =>
     < X : User | state: 2 > insertModule(Y, X, bar) .

  rl < X : User | state: 2 > insertedModule(X, Y) =>
     < X : User | state: 3 > reduceTerm(Y, X, 'BAR, 'a.Foo) .

  op foo : -> Module .
  eq foo = (
fmod 'FOO is
  nil
  sorts 'Foo .
  none
  op 'a : nil -> 'Foo [none] .
  op 'c : nil -> 'Foo [none] .
  none
  eq 'a.Foo = 'c.Foo [none] .
endfm ) .

  op bar : -> Module .
  eq bar = (
fmod 'BAR is
  protecting 'FOO .
  sorts none .
  none
  none
  none
  none
endfm ) .
endm

*** correct result
erew  <> < me : User | state: 0 > createInterpreter(interpreterManager, me) .

*** put a fmod BAR with same meta-syntax but different semantics in cache
red metaReduce(bar, 'a.Foo) .

*** wrong result
erew  <> < me : User | state: 0 > createInterpreter(interpreterManager, me) .

(9) A related bug where using the functional metalevel from the
meta-interpreter pulls imported modules from the object level
interpreter rather than the meta-interpreter. Illustrated
by the following example:

fmod FOO is
  sort Foo .
  ops a b : -> Foo .
  eq a = b .
endfm

load metaInterpreter 

mod TEST is
  pr META-INTERPRETER .
  op me : -> Oid .
  op User : -> Cid .
  op state:_ : Nat -> Attribute .

  vars X Y Z : Oid .

  rl < X : User | state: 0 > createdInterpreter(X, Y, Z) =>
     < X : User | state: 1 > insertModule(Z, X, foo) .

  rl < X : User | state: 1 > insertedModule(X, Y) =>
     < X : User | state: 2 > insertModule(Y, X, upModule('META-LEVEL, true)) .

  rl < X : User | state: 2 > insertedModule(X, Y) =>
     < X : User | state: 3 > reduceTerm(Y, X, 'META-LEVEL,
        'metaReduce[upTerm(bar) , upTerm('a.Foo)]) .

  op foo : -> Module .
  eq foo = (
fmod 'FOO is
  nil
  sorts 'Foo .
  none
  op 'a : nil -> 'Foo [none] .
  op 'c : nil -> 'Foo [none] .
  none
  eq 'a.Foo = 'c.Foo [none] .
endfm ) .

  op bar : -> Module .
  eq bar = (
fmod 'BAR is
  protecting 'FOO .
  sorts none .
  none
  none
  none
  none
endfm ) .
endm

*** expecting ''c.Foo.Constant but get ''b.Foo.Constant
erew  <> < me : User | state: 0 > createInterpreter(interpreterManager, me) .

(10) A related bug in the ascent functions that cause them to pull data
from the object level interpreter, even when called from the
meta-interpreter. Illustrated by the following example:

set include BOOL off .

fmod FOO is
  sort ObjectLevelFoo .
endfm

load metaInterpreter 

mod TEST is
  pr META-INTERPRETER .
  op me : -> Oid .
  op User : -> Cid .
  op state:_ : Nat -> Attribute .

  op foo : -> Module .
  eq foo = (
fmod 'FOO is
  nil
  sorts 'MetaLevelFoo .
  none
  none
  none
  none
endfm) .

  vars X Y Z : Oid .

  rl < X : User | state: 0 > createdInterpreter(X, Y, Z) =>
     < X : User | state: 1 > insertModule(Z, X, foo) .

  rl < X : User | state: 1 > insertedModule(X, Y) =>
     < X : User | state: 2 > insertModule(Y, X, upModule('META-LEVEL, true)) .

  rl < X : User | state: 2 > insertedModule(X, Y) =>
     < X : User | state: 3 > reduceTerm(Y, X, 'META-LEVEL,
        'upModule[''FOO.Qid, 'true.Bool]) .

  op foo : -> Module .
  eq foo = (
fmod 'FOO is
  nil
  sorts 'MetaLevelFoo .
  none
  none
  none
  none
endfm) .

endm

*** expecting meta-meta-module to contain sort MetaLevelFoo but get ObjectLevelFoo
erew  <> < me : User | state: 0 > createInterpreter(interpreterManager, me) .

(11) An obscure memory leak where a module wasn't unprotected if a
unify command gave up due to a bad unification problem; triggered by:

unify in BOOL : #1:Bool =? true .


New features
=============

(1) The existing meta-interpreter (metaInterpreter.maude) is extended:

(a) Views can now be inserted with the message:
  op insertView : Oid Oid View -> Msg [ctor msg format (b o)] .

On success the meta-interpeter object responds with the message:
  op insertedView : Oid Oid -> Msg [ctor msg format (m o)] .

(b) The meta-representation of a view in a meta-interpreter can
be obtained with by sending the message:
  op showView : Oid Oid Qid -> Msg [ctor msg format (b o)] .

The meta-interpreter responds with the message:
  op showingView : Oid Oid View -> Msg [ctor msg format (m o)] .

(c) External rewriting from the meta-interpreter is possible 
using the message:
  op erewriteTerm : Oid Oid Bound Nat Qid Term -> Msg [ctor msg format (b o)] .
where Bound is a bound on the number of rewrites, Nat is the
amount of gas per redex, Qid is the name of the module to
erewrite in and Term is the term to erewrite.

On success the meta-interpeter object responds with the message:
  op erewroteTerm : Oid Oid Nat Term Sort -> Msg [ctor msg format (m o)] .
where Nat is the totatlnumber of rewrites (equation/membership/rule),
Term is the result term and Sort is its sort. This allows sockets
and file handling to be used from the metalevel.

One interesting feature of erewrite being available in the
meta-interpreter, is that within a meta-interpreter, another
meta-interpreter can be created, and within that meta-interpreter
another and so on. Of course in order to instantiate a
meta-interpreter I2 within a meta-interpreter I1, I1 must contain
the contents of module META-INTERPRETER.  This can accomplished a
module applying upModule() to itself and inserting the meta-module
obtained into I1. The same trick can be playing one level
up and so on. Consider the following example:

load metaInterpreter

mod RUSSIAN-DOLLS is
  pr META-INTERPRETER .

  op me : -> Oid .
  op User : -> Cid .
  op level:_ : Nat -> Attribute .

  vars X Y Z : Oid .
  var AS : AttributeSet .
  var N : Nat .

  op problem : Nat -> Term .
  eq problem(s N) =
  '__['<>.Portal,'createInterpreter['interpreterManager.Oid,'me.Oid],
    '<_:_|_>['me.Oid, 'User.Cid, 'level:_[upTerm(N)]]] .
  eq problem(0) = '_+_['s_^2['0.Zero], 's_^2['0.Zero]] .

  rl < X : User | AS > createdInterpreter(X, Y, Z) =>
     < X : User | AS > insertModule(Z, X, upModule('RUSSIAN-DOLLS, true)) .

  rl < X : User | level: N, AS > insertedModule(X, Y) =>
     < X : User | AS > erewriteTerm(Y, X, unbounded, 1, 'RUSSIAN-DOLLS, problem(N)) .
endm

erew in RUSSIAN-DOLLS : <> 
< me : User | level: 4 > 
createInterpreter(interpreterManager, me) .

Here we build collection of nested meta-interpreters, with each
meta-interpreter except the last using upModule() to get a
meta-representation of its contents and insert it
into a new meta-interpreter one level up. The final meta-interpreter
does a trivial 2 + 2 computation in order to have a result to
report.

(2) There is an experimental feature to find out what Maude is doing
during execution without sending it a control-C (which will close
files and mess up socket communication among other things since
it has to exit blocked system calls to respond to the user).

On Mac, this feature uses the BSD SIGINFO extension, which
is activated by control-T from a terminal where Maude is the
foreground process. It can also be activated by kill -INFO <pid>
however this does not give the load and timing information
beforehand as control-T does.

On Linux, there is no equivalent capability so I've adopted the
dd convention and kill -USR1 <pid> can be used instead.

When activated, at the next eq/rl/mb application, Maude will
print out the current time, rewrite counts and a summary of
what it is doing on stderr.

Other changes
==============

(1) There is some initial optimization of the Leo's algorithm based
parser introduced in Alpha 116.

(2) The execution model for erewrite has changed: rather than wait
until no more internal rewrites are possible before before checking
for external events, a check is made after each traversal of the
current term. I'm interested to know if this behavior is more useful
- it does come with an overhead of more system calls to check for
external events.

(3) The "show mod" command now expands importation modes
(inc -> including etc). Also warnings about the obsolete using
importation mode are generated earlier in the processing of a module
and not repeated if the module is re-analyzed due to changes
in its dependencies. This is because more processing is done
on modules up front to make the backend processing compatible
with the meta-interpreter. The "show all" command has always done
this expansion since it works with fully processed modules.

(4) The edge case behavior in versions before Alpha 115 where
Maude would act on the closing parenthesis rather then waiting
for a \n when using loop mode and stdin is a pipe is reproduced.

This behavior arises from bypassing the stdlib input functionality
and using the read() system call directly, which returns whatever
is available immediately if the source is a pipe. Unfortunately
this also reads past \n characters which is was a problem for
the STD-STREAM functionality introduced in Alpha 115 because
the lexer could take characters that should go to the 
getLine() message, if stdin is a file, pipe or socket, and hence
the change to using stdlib input functionality to read up to
\n and buffer the rest.

This is now resolved by using read() directly and buffering
characters past \n until it is clear who they belong to.
This reversion to old behavior is needed for IOP compatibility.

Steven