Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha111b/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

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

(1) A bug in narrowing where a binding substituted into a context can
be shared between an eager position and an eager position that that occurs
beneath a lazy symbol if the narrowing step took place below that lazy symbol,
with the result that a binding might be reduced even though there is no eager
path to it. This is shown in the following example.

mod TEST is
  sort Foo .
  op f : Foo Foo -> Foo .
  op g : Foo -> Foo .
  op h : Foo Foo  -> Foo .
  op l : Foo -> Foo [strat (0)] .
  ops a b c d e : -> Foo .

  vars X Y Z : Foo .

  rl f(a, X) => g(X) .
  eq a = b .
endm

narrow h(l(h(f(Y, Y), Y)), Y)  =>+ Z .

Solution 1
Z --> h(l(h(g(a), b)), b)

Here the narrowing step binds Y to a; and a copy of binding is shared between
the two Y's underneath h symbols. Then equation reduction reduces this
shared dag to b, but the inner occurrence of a appears is below the lazy
symbol l and should not be reduced.

A symmetric bug occurs in variant narrowing:

fmod TEST2 is
  sort Foo .
  op f : Foo Foo -> Foo .
  op g : Foo -> Foo .
  op h : Foo Foo  -> Foo .
  op l : Foo -> Foo [strat (0)] .
  ops a b c d e : -> Foo .

  vars X Y Z : Foo .

  eq f(a, X) = g(X) [variant] .
  eq a = b .
endfm

get variants  h(l(h(f(Y, Y), Y)), Y) .

Variant #1
rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
Foo: h(l(h(f(#1:Foo, #1:Foo), #1:Foo)), #1:Foo)
Y --> #1:Foo

Variant #2
rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)
Foo: h(l(h(g(a), b)), b)
Y --> a

(2) A bug in rewriting modulo SMT where 0 step rewrites can result in an
unsatisfiable constraint being returned. Found by Everett Hildenbrandt <hildenb2@illinois.edu>
and shown by the following example:

load smt

mod FOO is pr INTEGER .
  sort State .
  op f : Integer -> State .
  crl f(X:Integer) => f(2 * X:Integer) if (X:Integer < 0) = true .
endm

smt-search f(5) =>* f(X:Integer) s.t. 2 + 2 = X:Integer .

Solution 1
empty substitution
where 2 + 2 === X:Integer and X:Integer === 5

(3) A bug where narrowing steps and some equational steps were not
being counted in metaNarrow(), demonstrated by the following example:

mod FOO is
  sort Foo .
  op f : Foo Foo -> Foo [assoc] .
  ops g h : Foo -> Foo .
  ops a b c d e : -> Foo .

vars X Y Z W : Foo .
  rl g(f(X, X)) => h(X) [label nar].
endm

set show breakdown on .

red in META-LEVEL :
  metaNarrow(
    ['FOO],
    'g['f['Y:Foo, 'Z:Foo, 'Z:Foo]],
    'W:Foo,
    '!,
    unbounded,
    0) .

(4) A bug in the module system where an attempt to parametrize a module
by a parametrized module is not detected until after attempting to make
a parameter copy of the parametrized module, resulting in a crash. Provoked
by this example from Benjamin Edward Oliver <benjamin.e.oliver@gmail.com>:

fmod FOO{X :: TRIV} is
    sort Foo{X} .
    subsort X$Elt < Foo{X} .
endfm

fmod BAR{X :: FOO} is
endfm

There was a related issue at the metalevel where a descent function would quietly
fail:

fmod FOO{X :: TRIV} is
    sort Foo{X} .
    subsort X$Elt < Foo{X} .
endfm

red in META-LEVEL : 
metaReduce(fmod 'BAR {'X :: 'FOO} is including 'BOOL .
sorts none . none none none none endfm, 'true.Bool) .

New feature
============

There is a new narrow command that does a breathfirst narrowing search
using variant unification, looking for states that variant unify with the
given pattern:

vu-narrow [<#solns>,<depth>] in <module> : <term> <relation> <pattern> .

where <relation> is one of =>*, =>+, =>1, =>!
As with search these correspond to 0 or more, 1 or more, exactly 1 or normal form
(no more steps possible). If <term> only contains #variables then it is used
as it, otherwise all variables in <term> are renamed to #variables. <pattern>
may not contain variables from any built-in family. Solutions consist of a reached
state, and a unifier between the state and <pattern>. There is no detection of
previously reached states, nor is there currently support for the cont command.
Either <#solns> or ,<depth> may be omitted. As always the [] and in <module> :
parts are optional.

For example:

mod BAZ is
  sort Foo .
  ops f g h : Foo -> Foo .
  ops i j k : Foo Foo -> Foo .

vars X Y Z W A B C D : Foo .
  eq j(f(X), Y) = i(f(Y), X) [variant] .
  rl g(i(X, k(Y, Z))) => f(k(Z, X)) .
  rl f(k(X, X)) => h(X) .
endm

vu-narrow [2] g(j(A, B)) =>* C .
vu-narrow [2,2] g(j(A, B)) =>+ C .
vu-narrow [,3] g(j(A, B)) =>! C .

This functionality is reflected by a descent function:

  op metaNarrowingSearch : Module Term Term Qid Bound Qid Qid Nat -> NarrowingSearchResult? .

The arguments are:
  Module to work in
  Term to narrow (after reducing)
  Term that is pattern to be reached
  Qid giving search type
  Bound on depth of search
  Qid giving label of rules to use
  Qid giving fresh variable family that might appear in the Term to narrow.
  Nat giving which of many solutions is wanted

The rules that are to be used for narrowing are required to be given a label
that is passed to the descent function. If any of the variables in the
Term to narrow don't belong to the specified variable family, all the
variables in the term are renamed. The variables in the pattern should not
belong to any built-in variable family. Allowable search types are: '+ '* '!
The bound on the number of narrowing steps may be the constant unbounded.

Return values are constructed using:

  op [_,_,_,_,_] : Term Type Substitution Qid Qid -> NarrowingSearchResult [ctor] .
  op failure : -> NarrowingSearchResult? [ctor] .
  op failureIncomplete : -> NarrowingSearchResult? [ctor] .

Here a successful result has the following arguments:
  Term reached after narrowing and reducing
  Type of Term
  Substitution giving the variant unifier between narrowed term and pattern
  Qid giving fresh variable family used to express result Term
  Qid giving fresh variable family used to express unifier

As usual there are two failure ctors with failureIncomplete indicating that
unification incompleteness was encountered during the variant narrowing
used to implement variant unification.

For example:

mod BAZ is
  sort Foo .
  ops f g h : Foo -> Foo .
  ops i j k : Foo Foo -> Foo .

vars X Y Z W A B C D : Foo .
  eq j(f(X), Y) = i(f(Y), X) [variant] .
  rl g(i(X, k(Y, Z))) => f(k(Z, X)) [label nar] .
  rl f(k(X, X)) => h(X)  [label nar] .
endm

reduce in META-LEVEL :
metaNarrowingSearch(['BAZ], 'g['j['#1:Foo, '#2:Foo]], 'C:Foo,
  '!, unbounded, 'nar, '#, 0) .

Note that the result tuple uses []s rather than {}s. This is necessary because otherwise
the arguments can be grouped with the _,_ operator on the kind that includes Qid and Type,
causing an ambiguity with an existing result tuple. In the interests of consistency,
I've changed the NarrowingResult ctor introduced in alpha111 to:

  op [_,_,_,_,_,_] : Term Type Substitution Substitution Context Qid -> NarrowingResult

The idea is that all descent functions that used Qids to specify variable families
will use [] ctors.

Other changes
==============
(1) The handled of conditional equations is partly optimized, with the set-up/tear-down
costs for the state information reduced.

(2) More special casing for the construction of free right hand sides in equational reduction.

(3) Ambiguity warnings for terms now print the sort of each of the two alternative
parsings generated - this proved useful figuring out the ambiguity issues with the
NarrowingSearchResult ctor.

One final note, I plan to remove xg-narrow and its descent function in the next
release as part of a refactoring of the narrowing code. This idiosyncratic notion of 
narrowing was a hack for the XG project and the code has not been maintained
in many years. If anyone actually uses this functionality, please let me know.

Steven