Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha120/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
==========
(1) A memory leak in the metaInterpreter normalizeTerm() message.
Provoked by the normalizeTerm() example in the test suite file
metaIntSort.maude and reported by Rafael Rubio Cuéllar <rubenrub@ucm.es>

(2) An bug where metaApply() and metaXapply() double counted
any equational rewrites and membership axiom applications
performed to reduce the start term before applying rules.

mod APPLY is
  sorts Foo Bar .
  subsort Foo < Bar .
  ops a c  : -> Bar .
  op b : -> Foo .
  op f : Foo Foo -> Foo [comm] .

  eq a = c .
  mb c : Foo .
  rl f(X:Foo, Y:Foo) => X:Foo [label k] .
endm

set trace on .
set show breakdown on .

red in META-LEVEL : metaApply(['APPLY], 'f['a.Foo, 'b.Foo], 'k, 'Y:Foo <- 'b.Foo, 0) .
red in META-LEVEL : metaXapply(['APPLY], 'f['a.Foo, 'b.Foo], 'k, 'Y:Foo <- 'b.Foo, 0, 0, 0) .

Here the use of eq a = c . and mb c : Foo . at the beginning are
each counted twice.

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

There are a number of extensions to the meta-interpreter.

(a) Application of named rules, with and without extension
is supported. In the first case, the application happens at the top
of the given term, without extension:
  op applyRule : Oid Oid Qid Term Qid Substitution Nat -> Msg [ctor msg format (b o)] .
Oid		target meta-interpreter object
Oid		sender object
Qid		name of module to work in
Term		term to rewrite (after reduction by equations)
Qid		label of rule to use
Substitution	partial substitution to use
Nat		index of wanted solution.

On success the reply is:
  op appliedRule : Oid Oid RewriteCount Term Type Substitution -> Msg [ctor msg format (m o)] .
Oid		target user object
Oid		meta-interpreter object
RewriteCount 	count of rewrite steps
Term		result after reduction by equations
Type		type of result
Substitution	matching substitution

In the second case application happens with extension at a
specified depth in the term:
  op applyRule : Oid Oid Qid Term Qid Substitution Nat Bound Nat -> Msg [ctor msg format (b o)] .
Oid		target meta-interpreter object
Oid		sender object
Qid		name of module to work in
Term		term to rewrite (after reduction by equations)
Qid		label of rule to use
Substitution	partial substitution to use
Nat		minimum depth (0 is at top)
Bound		maximum depth (can be unbounded)
Nat		index of wanted solution.

On success the reply is:
  op appliedRule : Oid Oid RewriteCount Term Type Substitution Context -> Msg [ctor msg format (m o)] .
Oid		target user object
Oid		meta-interpreter object
RewriteCount 	count of rewrite steps
Term		result after reduction by equations
Type		type of result
Substitution	matching substitution
Context		context in the reduced term where the rule was applied

In both cases, the failure reply is:
  op noSuchResult : Oid Oid RewriteCount -> Msg [ctor msg format (m o)] .
Oid		target user object
Oid		meta-interpreter object
RewriteCount 	count of equational rewrite steps

(b) One step narrowing with variant unification is supported.
  op getOneStepNarrowing : Oid Oid Qid Term TermList Qid Nat -> Msg [ctor msg format (b o)] .
Oid		target meta-interpreter object
Oid		sender object
Qid		name of module to work in
Term		term to narrow
TermList	blocker terms for variant unification
Qid		name of fresh variable family that may occur in start term
Nat		index of wanted solution

On success the reply is:
  gotOneStepNarrowing : Oid Oid RewriteCount Term Type Context
                        Qid Substitution Substitution Qid -> Msg [ctor msg format (m o)] .
Oid		target user object
Oid		meta-interpreter object
RewriteCount 	count of narrowing and rewrite steps
Term		result after reduction by equations
Type		type of result
Context		context in the start term where the narrowing happened
Qid		label of the narrowing rule used; ' if rule unlabeled
Substitution	unifier substitution for variables in the start term
Substitution	unifier substitution for variables in the narrowing rule
Qid		name of fresh variable family used to express the unifier
		and result term

On failure the reply is:
  noSuchResult : Oid Oid RewriteCount Bool -> Msg [ctor msg format (m o)] .
Oid		target user object
Oid		meta-interpreter object
RewriteCount 	count of narrowing and rewrite steps
Bool		complete; true if there are guaranteed no solutions with
		>= request index, false if there are potentially more
		solutions that were missed due to incomplete unification
		algorithm(s).

(c) Narrowing search with variant unification is supported by a pair
of messages:
  op getNarrowingSearchResult :        Oid Oid Qid Term Term Qid Bound Qid Nat -> Msg [ctor msg format (b o)] .
  op getNarrowingSearchResultAndPath : Oid Oid Qid Term Term Qid Bound Qid Nat -> Msg [ctor msg format (b o)] .
The only different between these messages is that the second one requests
the path of narrowing steps as well as the result.

In both messages the arguments are identical:
Oid		target meta-interpreter object
Oid		sender object
Qid		name of module to work in
Term		term to narrow
Term		goal pattern to reach
Qid		search type, '+, '* or '!
Bound		depth of the search; can be unbounded
Qid		folding strategy, current 'none or 'match
Nat		index of wanted solution

On success the reply to the first message is:
  op gotNarrowingSearchResult : Oid Oid RewriteCount Term Type Substitution Qid Substitution Qid -> Msg [ctor msg format (m o)] .

Oid		target user object
Oid		meta-interpreter object
RewriteCount 	count of narrowing and rewrite steps
Term		result term after equational reduction
Type		type of above term
Substitution	accumulated substitution
Qid		name of fresh variable family used to express result
		term and accumulated substitution
Substitution	variant unifier between result term and instantiated goal pattern
Qid		name of fresh variable family used to express this unifier

On success the reply to the second message is:
  op gotNarrowingSearchResultAndPath : Oid Oid RewriteCount Term Type Substitution NarrowingTrace Substitution Qid -> Msg [ctor msg format (m o)] .

Oid		target user object
Oid		meta-interpreter object
RewriteCount 	count of narrowing and rewrite steps
Term		start term after replacing original variables with # variables
Type		type of above term
Substitution	initial renaming of start term to # variables
NarrowingTrace	path of narrowing steps
Substitution	variant unifier between result term and instantiated goal pattern
Qid		name of fresh variable family used to express this unifier

The NarrowingTrace argument is constructed using the same signature
and semantics as used in the  metaNarrowingSearchPath() descent
function first documented in Alpha 113:

  op nil : -> NarrowingTrace [ctor] .
  op __ : NarrowingTrace NarrowingTrace -> NarrowingTrace [ctor assoc id: nil] .
  op {_,_,_,_,_,_,_} : Context Qid Substitution Qid Term Type Substitution -> NarrowingStep [ctor] .

where the arguments to the NarrowingStep constructor are:
Context		context where narrowing happened
Qid		label of the rule used for narrowing
Substitution	variant unifier used for narrowing
Qid		name of fresh variable family used to express this unifier
Term		new term (after reducing with equations)
Type		type of this term
Substitution	accumulated substitution

Steven