Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha86/

or downloaded from:

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

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.

It is a lot more alpha-like than usual - I'm am releasing it at this
time because of the need to put together a demo for RTA 2005.

Bug Fixes
==========
(1) Loop mode now treats Qid's of the form '\c where c is a single
character as nonspecial for printing purposes unless c is one the
following 25 characters:

n t s \
! ? u f x h o
p r g y m c w
P R G Y M X W

In particular, '\/ will now print out as \/ rather than be
ignored. Note that the following 7 Qids

'\`(  '\`,  '\`)  '\`{  '\`}  '\`[  '\`] 

 are still special for loop mode output as they have been since
 Alpha63b. The problem with '\/ was reported by Fabricio Chalub.


(2) A bug where metaXmatch() would attempt matching even when pattern
and subject are in different components; illustrated by this example
from Alberto Verdejo:

mod P is
   pr NAT .
   pr META-LEVEL .
   sorts S SS .
   subsort S < SS .
   ops a b c : -> S .
   op __ : SS SS -> SS [assoc comm] .
endm

red metaXmatch(upModule('P,false),
   'B:Bool,
   upTerm(a b c), nil, 0, unbounded, 0) .


(3) A problem where creating a server TCP socket bound to the same
port as one that had just closed would generate an "Address already in
use" error. This isn't really a bug but rather a property of TCP.
The situation arises when there is a "local close" of connection C
esablished thought a server socket S bound to port P. If S is then
closed there is a time wait period of several minutes following the
closure of C before a new server socket can be bound to port P.

The problem is somewhat alleviated in this version by setting the
SO_REUSEADDR flag on server sockets which allows the reuse of ports
before the end of the timeout. The down side is that this makes TCP
less reliable and there are rare but difficult to diagnose failure
modes. The problem was reported by Alberto Verdejo.

Of course the real answer is to write robust network code that doesn't
assume the availability of a given port and where possible, avoids
doing a local close (have the remote/client end close the connection).


Minor Changes
==============
(1) Theories no longer have automatic imports (e.g. BOOL) at the
object level.

(2) The characters { and } are no longer legal sort names. Note
that the characters [ ] and , have not been legal sort names since the
introduction of the current kind notation and the characters ( and )
have never been legal sort names. The characters : and . have not been
legal _anywhere_ in sort names since the Maude 2 metalevel.
`{ and `, and `} are now banned from sort names except as noted below.


New features
=============
(1) metaPrettyPrint() can now take options to control how the term is
printed. The global options controlled by "set print ..." are now
ignored. The print options argument is formed by the following
signature:

  sorts PrintOption PrintOptionSet .
  subsort PrintOption < PrintOptionSet .
  ops mixfix with-parens flat format number rat : -> PrintOption [ctor] .
  op none : -> PrintOptionSet [ctor] .
  op __ : PrintOptionSet PrintOptionSet -> PrintOptionSet [ctor assoc comm id: none] .

Note that four of the global print options are not present:

with aliases:	doesn't make sense as there are no variable aliases at
		the metalevel.
graph:		term graph printing has never been supported at the
		metalevel and doesn't seem to be much used at the
		object level.
color:		ctor coloring doesn't make sense as the term has not
		been reduced.
conceal:	would require passed a set of operator names to have
		their arguments concealed - could be implemented in
		the future if there is any demand.

metaPrettyPrint() is now declared as:

  op metaPrettyPrint : Module Term PrintOptionSet ~> QidList [...] .

For backwards compatibility we also have:

  op metaPrettyPrint : Module Term ~> QidList .
  eq metaPrettyPrint(M:Module, T:Term) = metaPrettyPrint(M:Module, T:Term, mixfix flat format number rat) .

This feature was requested by Carolyn.


(2) When an operator has preregularity or constructor consistency
problems, Maude now prints out a single informative message rather
than a slew of uninformative messages. For example:

fmod PROBLEM is
  pr META-LEVEL .
  op f : KindSet SortSet TypeSet -> KindSet .
  op f : SortSet KindSet TypeSet -> SortSet [ctor] .
endfm

red 0 .

produces a warning for each problem:

Warning: sort declarations for operator f failed preregularity
    check on 7 out of 12167 sort tuples. First such tuple is (
    EmptyTypeSet, EmptyTypeSet, TypeSet).
Warning: constructor declarations for operator f failed
    constructor consistency check on 7 out of 12167 sort tuples.
    First such tuple is (EmptyTypeSet, EmptyTypeSet, TypeSet).

Note that as usual, sort analysis is delayed until actual work is done
in the module. Also the number of bad tuples is computed symbolically
so very large domain spaces (billions of tuples) can be handled
efficiently. This change was requested by Carolyn.


(3) There are two new options for tracing:

set trace rewrite off .

turns off the printing of the redex and it's replacement;

set trace body off .

turns off the printing of the "start of rewrite" line (i.e. the one
beginning with *'s), the body of the eq/rl/mb being used - instead
just the label is printed, and the substitution. Used together these
options reduce a trace to a list of labels much like that produced by
the

show path labels <number> .

command. This capability was requested by Andy Poggio.


(4) There is now the notion of a structured sort name. The a
structured sort name contains at least one pair of `{ `} symbols and
is constructed according to the following BNF grammar, without any
white space bewteen teminals:

<S>  ::= <regular sort name>
      |  <S> `{ <SL> `}

<SL> ::= <S>
      |  <SL> `, <S>

Notice that structured sort _are_ allowed to contain `{ `, and `}
but only in accordance with the above grammar.
Thus the following are structured sort names:

a`{X`}
a`{X`,Y`}
a`{b`,c`{d`}`}`{e`}
a`{`(`}

while the following are not legal sort names:

`{X`}			(no regular sort name prefix)
a`(X`,Y`)		(`, not inside braces)
a`{b`,`{d`}`}`{e`}	(`{d`}` lacks regular sort name prefix)
a`(`{`)			(`{ without closing `})

At the object level, structured sort names can be written omiting
the backquotes for `{ `, `} but not for `( `) in the following places:

(a) sort declarations
(b) subsort declarations
(c) sort mappings (in renamings and views)
(d) the range and domain parts of operator declarations
(e) variable (alias) declarations
(f) as part of a kind
(g) as part of an mb/cmb
(h) as part of sort test condition fragment
(i) as part of a sort test operator
(j) as part of an on-the-fly variable
(k) in (term).sort disambiguation notation

If any omitable backquote is omitted, all omitable backquotes must be
omitted; hybrid notation such as a{b`,c} is not allowed.
When backquotes are omited, the sort name becomes a sequence of tokens
according to Maude's usual tokenizations rule and arbitrary white
space may be inserted between tokens. For example the following are
equivalent:

  ops a b c : -> Foo`{X`,Y`} .
  ops a b c : -> Foo{X,Y} .
  ops a b c : -> Foo{X, Y} .

Backquotes may not be omitted in structured sort names occurring
inside op-hooks or in metasyntax. Structured sort names are printed
with omitted backquotes in the 11 places mentioned above if the "set
print mixfix" setting is "on" (the default at start up).
Structured sort names always have backquotes omitted when used in the
canonical form of a renaming.

The multitoken form of structured sort names is supported for parsing
by metaParse() and for pretty-printing by metaPrettyPrint().

Apart from their special syntax, and their use as parameterized sorts
in parameterized modules (see below), structured sort names behave just
like regular sort names.


(5) There is a first attempt at supporting parameterization. There are
many known problems and limitations.

Currently only mods and fmods can be parameterized. A parameterized
module has the syntax:

mod M{X1 :: T1, ..., Xn :: Tn} is
...
endm

with n >= 1. Parameterized fmods have symmetric syntax.

The {X1 :: T1, ..., Xn :: Tn} part is called the "interface".
Each pair Xi :: Ti is a parameter.
Each Xi is an identifier - the "parameter name" or "parameter label".
Each parameter name in an interface must be unique. Each Ti is an
expression that yields a theory - the "parameter theory". There is no
uniqueness requirement. The parameter theories of an fmod must be
fths.

The parameterized module M is flattened as follows. For each parameter
Xi :: Ti, a renamed copy of T1, called Xi :: Ti is included.
The renaming maps each TDS s to Xi$s and each label l of a statement
occurring in T to Xi$l .
The renaming percolates down through nested inclusions of theories but
has no effect on importations of modules. Thus if Ti includes a theory
T', when the renamed module Xi :: Ti is created and included into M,
the renamed module Xi :: T' will also be created and included into
Xi :: Ti. These renamed modules are visible as names when using the
  show modules .
command and will be shared; however they cannot be referred to
directly in module expressions.

Sorts declared in the parameterized module M may be parameterized:

sort Foo{Y1,...,Ym} .

with m >= 1. Each Yj must be an Xi. It is recommended that all sorts
declared in a parameterized module be parameterized with m=n and Yj=Xj
but this is not enforced - parameterized sorts may duplicate, omit or
reorder parameters and unparameterized sorts are also allowed.

Only very simple views are currently supported. Views have the syntax

view V from T to M is
...
endv

V is a name, the name space of views being separate from the name
space of modules and theories. T is a module expression that evaluates
to a theory. M is module expression that evaluates to a module or a
theory. In the former case, V is called a module-view; in the latter
case V is called a theory view.

The only statements that are allowed in a view body are sort mappings
of the form

sort Foo to Bar .

The view body may be empty. For each sort s in T, there must exist a
sort s' in M which is it's mapping under V; unmentioned sorts get the
identity mapping. Furthermore if sorts s and t in T are in the same
kind then sorts s' and t' in M must be in the same kind.
Furthermore, if s < t then it must be true that s' < t'.
Operators may not be explicity mapped, however for each operator
  f : d1 ... dn -> r
in T there must exist an operator
  f : d1' ... dn' -> r'
in M.

The are commands
  show view V .
  show views .
to show a given view and see what views are in the view database.

A parameterized module M with n free parameters is instantiated by
the module expression
  M{A1, ..., An}
where the Ai are called the arguments. There are three possibilities
for an argument Ai:

(a) The name Yj of a parameter of the correct theory from the module
enclosing the module expression. In this case the parameter becomes a
bound parameter in the module resulting from the instantiation.
Each sort Xi$s is mapped to Yj$s. Each Xi occuring as a parameter in a
parameterized sort becomes Yj.

(b) The name of a theory-view V with the correct from theory. In this
case the parameter becomes a free parameter with V's target theory in
the in the module resulting from the instantiation.
Each sort Xi$s is mapped to Xi$s' where s' is the mapping of s under
V.

(c) The  name of a module-view V with the correct from theory. In this
case the parameter disappears. Each sort Xi$s is mapped to s' where s'
is the mapping of s under V. Each Xi occuring as a parameter in a
parameterized sort becomes V.

Parameterized modules with free parameters may not be imported - all
of the free parameters must be instantiated away. 
Parameterized modules with bound parameters only may be imported since
they were created for module expressions in a context where the
parameters are bound by an enclosing parameterized module.

Parameterized modules may not be summed even if all the parameters are
bound.

Parameterized modules may be renamed but the renaming must not touch
any sorts or operators comming from a parameter theory. The result of
renaming a parameterized module is a parameterized module with the
same parameters.

There are some additional serious limitations in the current
implementation:

(a) Renaming a parameterized module allows you to rename stuff from
the parameter theories - doing so causes internal corruption.

(b) There is no metalevel support for parameterization whatsoever -
attempting to up a parameterized module causes internal corruption.

(c) Things that look like parameterized sorts (but are not because of
the context where they were declared) may get mapped as if they were -
this is usually benign.

(d) Each operator in the from theory of a view must exist in the
target of the view and have the same semantic attributes (assoc, comm,
etc). This is not checked and failure causes internal corruption.

(e) Dependency tracking between views, theories and modules is not
working so if you reenter just part of a complicated system of
views, theories and modules, the usually recomputation of things that
depend on stuff that changed will not be done properly.


(6) There are many predefined theories, views and parameterized
modules in prelude.maude which are the beginning of a library
analogous to C++'s standard template library. It is intended that
where possible the computational complexity of operations in this
library should be the same as the ones in the STL.

A quick overview (I will write a more lengthy explanation of why
things are done the way they are, and what semantic and complexity
guarantees are maintained later).

fth TRIV
---------
Theory consisting of a single sort; Many views of the form

view Foo from TRIV to FOO is
  sort Elt to Foo .
endv

for the main sort Foo of built in modules FOO.

fth TAO-SET
------------
Theory of a set with a Transitive, Antisymmetric Order (TAO). This
generalizes regular posets and strictly partial orders. View from TRIV
to TAO-SET that forgets the order and views of the form

view Foo< from TAO-SET to FOO is
  sort Elt to Foo .
endv

for the main sort Foo of built in modules FOO.

fmod LIST{X :: TRIV}
---------------------
Associative lists formed from nil and the empty syntax.
For example:

fmod TEST is
  inc LIST{Nat} .
endfm

red reverse(1 2 3 4 5 6) .

fmod SORTABLE-LIST{X :: TAO-SET}
---------------------------------
Requires a TAO-SET; adds merge and sort operators to regular list.
For example:

fmod TEST2 is
  inc SORTABLE-LIST{String<} .
endfm

red sort("a" "quick" "brown" "fox" "jumps" "over" "the" "lazy" "dog") .

fmod SET{X :: TRIV}
--------------------
Sets fromed from empty and _,_ .

fmod LIST*{X :: TRIV}
----------------------
Nestable lists.

fmod SET*{X :: TRIV}
---------------------
Nestable sets with a powerset operator.
For example:

fmod TEST3 is
  inc SET*{Qid} .
endfm

red 2^ {'a, 'b, 'c, 'd} .

fmod MAP{X :: TRIV, Y :: TRIV}
-------------------------------
Map between to sets with efficient update and lookup; think of it as an
associative array.
For example:

fmod TEST4 is
  inc MAP{String, Nat} .
endfm

red (insert("one", 1, insert("two", 2, insert("three", 3, empty)))) .
red (insert("one", 1, insert("two", 2, insert("three", 3, empty)))) ["two"] .
red (insert("one", 1, insert("two", 2, insert("three", 3, empty)))) ["four"] .


Steven