Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha86b/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This version is a pure alpha release - it is not destined for the
Maude website though of course you may redistribute it under the GPL.
Because of this I have only made binaries for Linux and Darwin.

We are now quite close to having a 2.2 release; I have put a lot of
effort in to bullet proofing it and I would appreciate folks trying to
break it. I will be on vacation thru Aug 15 but I will intermittantly
check StevenEker@gmail.com

Bug fixes
==========
(1) A reference count bug where modules created for module
expresssions that are no longer in use were not garbage collected. In
the following example the module constructed for
  FOO * (sort Foo to Bar)
is not garbage collected.

fmod FOO is
  sort Foo .
endfm

fmod BAR is
  pr FOO * (sort Foo to Bar) .
endfm

fmod BAR is
  pr FOO .
  op a : -> Foo .
endfm

show modules .

(2) A bug in the handling of meta-summations that resulted in only the
last module being used; exposed by:

red in META-LEVEL : metaReduce(
fmod 'FOO is
  including 'RAT + 'STRING .
  sorts 'Foo .
  none
  none
  none
  none
endfm, '_+_['_/_['s_['0.Rat], 's_['s_['0.Rat]]],
'length['"foo".String]]) .

(3) Module-views now check that the target module has no free
parameters, thus:

view Bad from TRIV to MAP is
  sort Elt to Bool .
endv

now results in a warning and an unusable view.

Other changes
==============
(1) Illegal importations whether a theory is imported using a mode
other than include now have a modified error message that says that
the mode is being treated as if it were including. Other illegal
importations now have an error message that says they are being
ignored, and they are now ignored rather than tolerated. The reason
for this change is to sidestep some tricky situations that can arise
with parameterization and views such as the following example which
breaks alpha86a:

fmod M is
  sort Foo .
  op a : -> Foo .
endfm

fth T is
  sort Foo .
  op b : -> Foo .
endfth

fth T' is
  pr M .
  inc T .
  eq b = a .
endfth

fmod FOO{X :: T'} is
endfm

show all .

(2) View checking takes into account that sorts declared in modules
are not mapped during module instantiations. Attempts so map such
sorts produced an advisory, and if there is no matching sort in the
target module, the view is unusable. This avoids examples such as:

fmod M is
  sort Elt .
endfm

fth T is
  pr M .
  sort Elt2 .
endfth

view V from T to NAT is
  sort Elt to Nat .
  sort Elt2 to NzNat .
endv

fmod P{X :: T} is
  op f : X$Elt2 -> Elt .
endfm

fmod TEST is
  inc P{V} .
endfm

that break alpha86a.

(3) Sort mappings and op mappings that would rename sorts and
operators coming from parameters are now ignored and omitted from the
canonical version of a renaming of a parameterized module.
This is important since renamings are not applied to parameter
theories when a parameterized module is renamed so allowing such sort
and operators to be renamed in the module would cause chaos. The
following examples break alpha86a:

fmod P{X :: TRIV} is
  op a : -> X$Elt .
endfm

fmod TEST is
  inc (P * (sort X$Elt to Foo)){Nat} .
endfm

and

fmod P{X :: TAO-SET} is
  var X : X$Elt .
  eq X < X = false .
endfm

fmod TEST is
  inc (P * (op _<_ to f)){Nat<} .
endfm

show all .

When a mapping is omitted for this reason an advisory is generated.


New features
=============
(1) Operator mappings are now permitted in views. For a view

view V from T to M is
  ...
endv

where M may be a theory or module expression, there are three
forms allowed. In the following description, for each sort s, its
mapping under V is given by s'. 

Generic
--------
  op f to g .

All operators with the name f in T will be mapped on to operators with
the name g in M. Existence of appropriate operators in the target is
checked for.

Specific
---------
  op f : Foo Bar -> Baz to g .

The specific operator f with domain Foo Bar and range Baz will be
mapped to an operator:

  op g : Foo' Bar' -> Baz' .

Operator to term
-----------------
  op f(X:Foo, Y:Bar) to term t(X:Foo', Y:Bar') .

Here f(X:Foo, Y:Bar) must parse to a unique term in T (_without_ the
variable aliases declared in T) which consists of an operator with
only variable arguments, each such variable having a unique base name
(using both X:Foo and X:Bar in the same argument list is disallowed).

Also t(X:Foo', Y:Bar') must parse to a unique term in M (_without_ the
variable aliases declared in M). The only variables that may occur in
t(X:Foo', Y:Bar') are X:Foo' and Y:Bar' however they may occur
multiple times or not at all. If f(X:Foo, Y:Bar) parses to sort u or
kind [u] then t(X:Foo', Y:Bar') must parse to sort v or kind [v] such
that v and u' are belong to the same kind.

Views may also contain variable alias declarations. The syntax is
identical to that in modules and theories, however the semantics is
subltly different. Instead of declaring a single alias,

  var X : Foo .

declares two aliases with the same name; in the lefthand side of an
operator mapping, X is an alias for X:Foo while in the righthand side
of an operator mapping, X is an alias for X:Foo'.

Operator mappings are not applied to operators that have at least one
declaration in a module (as oposed to a theory); if a mapping would
apply to such an operator, an advisory is generated.

Some subtle issues can arise with operator mappings:

assoc operators
----------------
Nested occurrences of assoc operators may have been flattened, or have
been entered in a flattened way (say f(a, a, b, b) for example). In
order to map this to an operator that has different attributes
(perhaps including assoc) or to a term, flattened occurrances will be
temporarily unflattened into a regular term before translation. The
precise choice of unflattening is left unspecified.

iter operators
---------------
Mapping an iter operator to a non-iter operator causes the efficient
representation of towers of symbols to be expanded out, with a
potential exponential blow up. Mapping an iter operator to a term
in which the single argument variable occurs more than once causes a
doubly exponential blow up. Maude operates under the principle of "you
asked for it, you got it" and if the expansion is too large it will
die with a virtual memory exhausted error.

builtin operators
------------------
The following builtin operators for holding non-algebraically defined
data:
  StringSymbol
  FloatSymbol
  QuotedIdentifierSymbol
have a special internal represention for their terms and can only be
mapped to operators of identical type.

polymorphic operators
----------------------
Polymorphic operators must map to polymorphic operators that are
polymorhic on the same arguments. Only generic mappings are considered
when mapping polymorphic operators.

(2) Dependency tracking now supports views. This means that every view
keeps track of what modules it depends on, and each module keeps track
of what modules and views it depends on. When a module or view is
overwritten, all modules and views that (transitively) depend on it
are marked as "dirty" and are reanalyzed if they or something that
depends on them is subsequently used.

There is an important limitation with dependency tracking that existed
even when only simple imports between modules were allow but is now
more apparent given the complexity of module expressions allowed and
the ways in which they can fail: a view or module A cannot be dependent
on a view or module B that is nonexistent, badly formed, not able to
be constructed or that contains unpatchable errors at the time A is
entered. The simplest example is:

fmod FOO is
  pr BAR .
endfm

fmod BAR is
  op a : -> Bool .
endfm

red in FOO : a .

Here FOO is not marked as dirty when BAR is entered since BAR did not
exist when FOO was entered so FOO cannot be dependent on it.

A more subtle example is

fmod FOO is
  pr LIST{Nat<} .
endfm

view Nat< from TRIV to NAT is
  sort Elt to Nat .
endv

red in FOO : 1 2 3 .

Here the module expression LIST{Nat<} cannot be evalutated because of
a theory clash and so there is no module LIST{Nat<} for FOO to be
dependent on. Thus if module LIST or view Nat< are later redefined so
that LIST{Nat<} can be evaluated, FOO will not marked as dirty and
will not be reanalyzed.

(3) Parameterization is now partly reflected in the metalevel. Meta
modules may now take a header in place of the name Qid, where a header
is a name and parameter list pair built from the following signature:

  sorts ParameterDecl NeParameterDeclList ParameterDeclList .
  subsorts ParameterDecl < NeParameterDeclList < ParameterDeclList .
  op _::_ : Sort ModuleExpression -> ParameterDecl .
  op nil : -> ParameterDeclList [ctor] .
  op _,_ : ParameterDeclList ParameterDeclList -> ParameterDeclList [ctor assoc id: nil prec 121] .
  op _,_ : NeParameterDeclList ParameterDeclList -> NeParameterDeclList [ctor ditto] .
  op _,_ : ParameterDeclList NeParameterDeclList -> NeParameterDeclList [ctor ditto] .

  sort Header .
  subsort Qid < Header .
  op _{_}  : Qid ParameterDeclList -> Header .

Note that parameter names have the same syntactic form as sort
names. Meta-module-expressions may now include module instantiations
built from the following signature:

  sort NeParameterList ParameterList .
  subsorts Sort < NeParameterList < ParameterList .
  subsort EmptyQidList < ParameterList .
  op _,_ : ParameterList ParameterList -> ParameterList [ctor ditto] .
  op _,_ : NeParameterList ParameterList -> NeParameterList [ctor ditto] .
  op _,_ : ParameterList NeParameterList -> NeParameterList [ctor ditto] .
  op _,_ : EmptyQidList EmptyQidList -> EmptyQidList [ctor ditto] .
  op _{_} : ModuleExpression ParameterList -> ModuleExpression [ctor prec 37].

Note that _,_ is a subsort overloading of the argument constructor for
terms because of the Qid base sort.

The rules for constructing parameterized meta-modules, and
instantiating existing parameterized modules existing in the data base
reflect the object level rules; in particular bound parameters are
permitted; for example:

red in META-LEVEL : metaReduce(
fmod 'FOO{'X :: 'TRIV} is
  including 'MAP{'String, 'X} .
  sorts 'Foo .
  none
  none
  none
  none
endfm, 'insert['"foo".String, 'A:X$Elt, 'empty.Map`{String`,X`}]) .

Parameterized modules, and the instantiation thereof in module
expressions, are also grokked by metaUpModule(); for example:

red in META-LEVEL : upModule('SORTABLE-LIST, false) .

The one area where parameterization is not reflected is views; there
are no meta-views and no way construct new views or inspect existing
views.

(4) Along with the parameterization extensions to the metalevel, there
are now identity elements for various lists that were previously
non-empty, along with the necessary rearrangement of the sort
structure to maintain preregularity and associativity (see my previous
emails for the gory details). Modules QID-LIST and NAT-LIST is now renamed
instantiations of LIST.

Steven