Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha75a/

or downloaded from

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

This version needs the same dynamic libraries as Alpha73.

Bug fixes:
1	Bug in the tracing of polymorphic ops:
	set trace on .
	set trace select on .
	red in BOOL : true == false .
	Reported by Paco.

2	Bug in the metalevel uping of constants and variables
	at the kind level cause (illegal) Qids like 'a.'[Foo`] rather
	than 'a.`[Foo`] - reported by Paco.

Other changes:
1     	Free theory uses new style order-sorted discrimination nets for
	equational rewriting. This allows subsumed equations to be
	discarded.

2	Interpretation of discrimination nets optimized.

3	Special handling for free theory ternary symbols.

4	Substitution coloring; this helps with a performance bug noted
	in earlier release notes where there is a equation with a huge
	ground rhs. This would previously force all substitutions
	to have a slot for every subterm in such a rhs. Substitution
	coloring allows slots to be reused.

5	Two of the four pretty pinters rewritten to handle more
	disambiguation corner cases. There are 11 classes of operator
	that have special i/o representation and disambiguation needs:

	Polymorphs
	sort tests
	itor symbols

	variables
	flattened assoc symbols
	nats
	ints
	rats

	floats
	strings
	qids

	The last 3 have always been handled. The first 3 are still not
	handled. The middle 5 are now handled correctly by the object
	level. The two remaining pretty printers (metaPrettyPrint and
	term graph pretty printer) still need to be rewritten. The
	following ambiguous examples shows some of the corner cases
	now handled.

fmod OVERLOAD is pr NUMBER-CONVERSION .
  sorts Foo Bar .
  ops 1 -42 1/2 N:Nat : -> Foo .
  op a : -> Foo .
  op a : -> Bar .
  op f : Foo Foo -> Foo [assoc] .
  op f : Bar Bar Bar -> Bar .
endfm

red 1 .
red -42 .
red 1/2 .
red N:Nat .
red f(a, a, a) .

	There are some new error messages for cases where a signature
	is created such that no disambiguation is possible.

6	Ctor declarations are now stored and printed out correctly with
	show all <module> .
	whereas previously they were just comments. Ditto attribute
	does not copy ctor attribute but allows a ctor attribute to be
	included - this is because subsort polymorphic overloaded
	operators may reasonably have differing ctor status.

7	Term coloring partly implemented. This feature was called ctor
	debugging in previous discussions. The command is
	set print color on .

	Symbols within terms that are being executed (i.e. in trace or
	the final result of a reduce) are colored as follows:

	reduced, ctor					not colored
	reduced, non-ctor, strangeness below		blue
	reduced, non-ctor, no strangeness below		red
	unreduced, no reduced above			green
	unreduced, reduced directly above		magenta
	unreduced, reduced not directly above		cyan

	Strangeness is a colored operator.

	The idea is that red and magenta indicate initial locus of a
	bug while blue and cyan indicate secondary damage. Green
	denotes reduction pended and cannot appear in final result.

	It is instructive to run a trace of a reduction involving
	lazy operators:

fmod SIEVE is
  pr NAT .
  sort List .
  subsort Nat < List .

  op nil : -> List [ctor].
  op _,_ : Nat List -> List [ctor prec 31 gather (e E) strat (1 2 0)] .

  op l : Nat List -> List [ctor strat (0)] .
  op force : List Nat -> List .
  op ints-from : Nat -> List [ctor] .
  op sieve : List -> List .
  op filter : List Nat -> List .

  var N M : Nat .
  var L : List .

  eq ints-from(N) = l(N, ints-from(s(N))) .        *** infinite list of Nats
  eq sieve(l(N, L)) = l(N, sieve(filter(L, N))) .  *** the actual sieve 
  eq filter(l(N, L), M) =
	if M divides N then
	  filter(L, M)
	else
	  l(N, filter(L, M))
	fi .
  eq force(L, 0) = nil .                         
  eq force(l(N, L), s(M)) = N, force(L, M) .    *** force lazy list
endfm

set trace on .
set trace whole on .
set print color on .
red force(sieve(ints-from(2)), 10) .

	There is also Jose's missing case example:

fmod NAT-MSET-MIN is
  sorts Nat NatMSet .
  subsort Nat < NatMSet .
  op 0 : -> Nat [ctor] .
  op s : Nat -> Nat [ctor] .
  op _ _ : NatMSet NatMSet -> NatMSet [assoc comm ctor] .
  op _<_ : Nat Nat -> Bool .
  op min : NatMSet -> Nat .
  vars N M : Nat .
  var  S : NatMSet .
  eq 0 < s(N) = true .
  eq s(N) < 0 = false .
  eq s(N) < s(M) = N < M .
  eq min(N N S) = min(N S) .
  ceq min(N M S) = min(N S) if N < M .
  ceq min(N M) = N if N < M .
  eq min(N) = N .
endfm

set print color on .
red min(s(0) s(s(0))) .
red min(s(s(0)) min(s(0) s(0))) .

	Color & style due to format attributes are implicitly turned
	off to avoid confusion when "print color" is on.

	Operators that have assoc or iter attributes need to have all
	of their declarations have ctor or be without ctor. For other
	operators, if they have both with and without ctor
	declarations, ctorness is computed from arguments sorts.

Finally there is a command introduced in Alpha73 that I forgot to
document:

set print rat off .

switches off the special printing for _/_ in fmod RAT.

Steven