Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha116/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
==========
(1) A bug where abstraction variables were not be accounted for
during the matching need for unifier filtering duing variant narrowing,
leading to memory corruption. Provoked by this example from Paco:

reduce in META-LEVEL : metaNarrowingSearch(mod 'NAT-ACU is
  nil
  sorts 'Nat ; 'NzNat ; 'Zero .
  subsort 'NzNat < 'Nat .
  subsort 'Zero < 'Nat .
  ((((((op '_+_ : 'NzNat 'Nat -> 'NzNat [assoc comm ctor id('0.Zero)] .
  op '_+_ : 'NzNat 'NzNat -> 'NzNat [assoc comm ctor id('0.Zero)] .)
  op '_+_ : 'Nat 'NzNat -> 'NzNat [assoc comm ctor id('0.Zero)] .)
  op '_+_ : 'Nat 'Nat -> 'Nat [assoc comm ctor id('0.Zero)] .)
  op '_*_ : 'NzNat 'NzNat -> 'NzNat [assoc comm] .)
  op '_*_ : 'Nat 'Nat -> 'Nat [assoc comm] .)
  op '1 : nil -> 'NzNat [ctor] .)
  op '0 : nil -> 'Zero [ctor] .
  none
  none
  rl '_*_['N':NzNat,'_+_['M':NzNat,'K':NzNat]] => '_+_['_*_['N':NzNat,'M':NzNat],'_*_['N':NzNat,'K':NzNat]] [narrowing] .
endm, '_*_['N':NzNat,'_+_['M':NzNat,'K':NzNat]], '#V:`[Nat`], '+, 1, 'none, 1) .

(2) A symmetric bug in variant folding during variant narrowing.

(3) A symmetric bug in narrowing state folding during folded vu narrowing.

(4) A bug in term coloring caused by constructor calculations for
associative operators, where any an associative operator that had both
ctor and non-ctor declarations was treat as being non-ctor everywhere.
Illustrated by the following example:

fmod FOO is
  sorts Lo Hi .
  subsort Lo < Hi .
  ops a b : -> Lo [ctor] .
  op f : Hi Hi -> Hi [assoc] .
  op f : Lo Lo -> Lo [assoc ctor] .
endfm

set print color on .

red f(a, b) .

Here the unreduced f operator was colored red, even though it is a
contructor when applied to arguments of sort Lo.

Changes
========
(1) Constructor declarations for associative operators are now checked
for consistency in manner analogous to sort declarations. The actual check
performed is a little subtle.

For a term t, we define constructor status, denoted cs(t), to be true
iff each operator in t is a contructor. For every term t, we want the
constructor declarations to be such that every maximally collapsed term
in [t]_E has the same constructor status. For commutativity, completion
was already done; i.e. every time there is an operator declaration
  op f : Foo Bar -> Baz [comm ctor] .
an operator declaration:
  op f : Bar Foo -> Baz [comm ctor] .
is added if it doesn't already exist. For associativity, we need to
enforce some constraint on the declarations of associative ctor symbols.

For a binary operator f, we define s_f : Sorts * Sorts -> Sorts that
returns the output sort of f when given the input sorts. We also define
c_f : Sorts * Sorts -> Boolean that gives the constructor status of
f when given the input sorts.

The "obvious" constraint to enforce for an associative operators f,
namely that:
  (for all sorts x, y, z).[ c_f(s_f(x, y), z) = c_f(x, s_f(y, z)) ]
doesn't work as the following counterexample shows:

fmod FOO is
  sorts Lo Hi .
  subsort Lo < Hi .
  op f : Lo Hi -> Lo [assoc ctor] .
  op f : Hi Hi -> Hi [assoc] .
endfm

Here the declarations for f give rise to a sorting function s_f which
is associative and a constructor function c_f which satisfies the above
constraint wrt to s_f, however if we look at
  f(f(X:Lo, Y:Hi), Z:Lo)
we have both f's being constructors while with
  f(X:Lo, f(Y:Hi, Z:Lo))
the inner f is not a ctor.

It can be shown that the following constraint, which I call
"associative constructor consistency" is both necessary and sufficient
to ensure a rewrite of a term t by the associativity axiom for f does
not change the constructor status of t.

(for all sorts x, y, z).[
  c_f(s_f(x, y), z) /\ c_f(x, y)) <=>
  c_f(x, s_f(y, z)) /\ c_f(y, z))
]

It's clearly neccessary since otherwise for some variables X:x, Y:y and Z:z,
we would have cs(f(f(X, Y), Z) ) != cs(f(X, f(Y, Z))).

To see that it is sufficent, consider two terms, t and t' such that t
rewrites to t' one application of the associative axiom for f.
It must be possible to write t = C[f(u, f(v, w))] and t' = C[f(f(u, v), w))]
(or vice versa) for context C and subterms u, v, w. We note that the
constructor status of the symbols in C only depend on the sorts of
f(u, f(v, w)) and f(f(u, v), w)) which must be the same because of the
associativity of s_f. Now the sorts and constructor statuses of u, v, w
are the same in both t and t', so the only place the constructor status of
t and t' might differ and in the explicitly mentioned f symbols. But
by associative constructor consistency, either both f's are ctors in
both f(u, f(v, w)) and f(f(u, v), w) or at least one f in each term is a
non-ctor. Either way cs(f(u, f(v, w))) = cs(f(f(u, v), w)) and
thus cs(t) = cs(t').

(2) The -interactive flag now forces the output of a "Maude> " prompt
(but not ">" continuation prompts) before reading from stdin, even if stdin
is not a terminal. ">" continuation prompts are now only generated from
tecla. These changes were made because the I/O cleanup in Alpha115 broke
code wrapping Maude.

(3) The MSCP10 CFG + prec/gather + bubbles parser is replaced by
a new parser based on extending Leo's algorithm [1] for CFG to handle
prec/gather and bubbles. The MSCP10 code is undocumented and unmaintainable
and has a large number of bugs in its handling of bubbles that are
fixed by the new parser:

(a) Strange location of parse errors in bubbles. 

fmod FOO is
  including QID-LIST .
  sorts Foo Tokens .

  op start_ : Tokens -> Foo .
  op tokens : QidList -> Tokens [special(
    id-hook Bubble (0 -1 < >) 

    op-hook qidSymbol (<Qids> : ~> Qid)
    op-hook nilQidListSymbol (nil : ~> QidList)
    op-hook qidListSymbol (__ : QidList QidList ~> QidList)
  )] .
endfm

parse start a b < c .

Here we have a bubble with requiring balenced paren tokens < and > and
a term that doesn't parse because there is no closing >.

MSCP10 claims the problem is:
Warning: <standard input>, line 15: didn't expect token <:
start a b < <---*HERE*

But since there are legal continuations, a better error message is:
Warning: <standard input>, line 15 : unexpected end of tokens.

(b) A related problem with upper bounds on bubbles:

fmod FOO is
  including QID-LIST .
  sorts Foo Tokens .

  op start_ : Tokens -> Foo .
  op tokens : QidList -> Tokens [special(
    id-hook Bubble (0 3 < >) 

    op-hook qidSymbol (<Qids> : ~> Qid)
    op-hook nilQidListSymbol (nil : ~> QidList)
    op-hook qidListSymbol (__ : QidList QidList ~> QidList)
  )] .
endfm

parse start a < b c > .

Here the bubble is 4 tokens when we have an upper bound of 3.

MSCP10 claims the problem is:
Warning: <standard input>, line 15: didn't expect token <:
start a < <---*HERE*

But there are legal continuations; say

parse start a < b > .

so a better error message is
Warning: <standard input>, line 15: didn't expect token <:
start a < b c <---*HERE*

At this point there is no legal continuation since the
matching parenthesis token would make the bubble too large.

(c) Failing to parse adjacent possibly empty bubbles:

fmod FOO is
  including QID-LIST .
  sorts Foo Tokens Tokens2 .

  op [__] : Tokens Tokens2 -> Foo .

  op tokens : QidList -> Tokens [special(
    id-hook Bubble (0 -1 < >) 

    op-hook qidSymbol (<Qids> : ~> Qid)
    op-hook nilQidListSymbol (nil : ~> QidList)
    op-hook qidListSymbol (__ : QidList QidList ~> QidList)
  )] .

  op tokens2 : QidList -> Tokens2 [special(
    id-hook Bubble (0 -1 < >) 

    op-hook qidSymbol (<Qids> : ~> Qid)
    op-hook nilQidListSymbol (nil : ~> QidList)
    op-hook qidListSymbol (__ : QidList QidList ~> QidList)
  )] .

endfm

parse [ ] .
parse [ a ] .
parse [ a b ] .

(d) While MSCP10 handles competing bubbles correctly in the first
two cases, it doesn't notice the ambiguity in the 3 case:

fmod FOO is
  including QID-LIST .
  sorts Tokens Foo .
  op start_ :  Tokens -> Foo .

  op tokens : QidList -> Tokens [special(
    id-hook Bubble (0 -1 < >) 

    op-hook qidSymbol (<Qids> : ~> Qid)
    op-hook nilQidListSymbol (nil : ~> QidList)
    op-hook qidListSymbol (__ : QidList QidList ~> QidList)
  )] .

  op _;_ : QidList QidList -> QidList [assoc] .

  op tokens : QidList -> Tokens [special(
    id-hook Bubble (0 -1 <| |>) 

    op-hook qidSymbol (<Qids> : ~> Qid)
    op-hook nilQidListSymbol (nil : ~> QidList)
    op-hook qidListSymbol (_;_ : QidList QidList ~> QidList)
  )] .
endfm

parse start a < .
parse start a <| .
parse start a b .

(e) MSCP10 can hang in what appears to be an infinite loop:

fmod HANG is
  including QID-LIST .
  sorts Tokens Foo Bar .
  op start__ : Tokens Bar -> Foo .
  op __ : Tokens Tokens -> Bar .

  op tokens : QidList -> Tokens [special(
    id-hook Bubble (0 -1 < >) 
    id-hook Exclude (start)

    op-hook qidSymbol (<Qids> : ~> Qid)
    op-hook nilQidListSymbol (nil : ~> QidList)
    op-hook qidListSymbol (__ : QidList QidList ~> QidList)
  )] .
endfm

parse start .

(f) MSCP10 has issues even with single token bubbles if invisible
syntax is involved:

fmod FOO is
  inc QID .
  sort Bar .
  op k : -> Bar .
  sorts Token Foo FooList .
  subsort Foo < FooList .

  op token : Qid -> Token [special(id-hook Bubble (1 1)
                                   op-hook qidSymbol (<Qids> : ~> Qid))] .
  op _#_ : Token Token -> Foo .
  op __ : FooList FooList -> FooList .

  op g : -> Token .
endfm

parse unseen # unseen1 k # unseen3 .    *** parse missed
parse unseen # unseen1 g # unseen3 .    *** ambiguity missed

(4) There is a subtle change to where bubbles are allowed. In previous
versions, terms from bubble components were prohibited from being generic
terms (for example the term in a parse command) and from being the
polymorphic kind in a polymorphic operator such as _==_
However by an oversight they were allowed to be the kind in the built-in
membership test operators. This results is a counterintuitive error message
if one tries to parse a bubble at the top:

fmod FOO is
  including QID-LIST .
  sorts Foo Tokens Tokens2 .

  op [_] : Tokens -> Foo .

  op tokens : QidList -> Tokens [special(
    id-hook Bubble (0 -1 < >) 

    op-hook qidSymbol (<Qids> : ~> Qid)
    op-hook nilQidListSymbol (nil : ~> QidList)
    op-hook qidListSymbol (__ : QidList QidList ~> QidList)
  )] .

endfm

parse a a a .

The reason an unexpected end of tokens message is given rather than
an error at the first a is because the following had a valid parse:

parse a a a :: Tokens .

This is now forbidden and kinds containing bubbles can no longer be
used with sort test operators (in the same way that they have always
been forbidden with polymorphic operators or as the kind of a top
level term). None of the following has ever had a legal parse:

parse a a =/= a .
parse tokens(nil) == tokens(nil) .
parse tokens(nil) .

Steven

---

[1] Joop M. I. M. Leo, "A general context-free parsing algorithm
running in linear time on every LR(k) grammar without using lookahead",
Theoretical Computer Science Volume 82, Issue 1, 22 May 1991, Pages 165-176.