Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha119/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha119/ Alpha release site authentication: User Name: maudeabuser Password: bughunter Bug fixes ========== (1) An interaction between object-message rewriting and the trace/break/profile slow route rewriting that gives misleading results as shown by the following example: mod FOO is inc CONFIGURATION . op User : -> Cid . ops me other : -> Oid . op no-op : Oid Oid -> Msg [msg] . vars X Y : Oid . var AS : AttributeSet . rl < X : User | AS > no-op(X, Y) => < X : User | AS > . endm set trace on . set trace whole on . set profile on . frew < me : User | none > no-op(me, other) . frewrite in FOO : no-op(me, other) < me : User | none > . *********** rule rl no-op(X, Y) < X : User | AS > => < X : User | AS > . X --> me Y --> other AS --> (none).AttributeSet Old: no-op(me, other) < me : User | none > no-op(me, other) < me : User | none > ---> < me : User | none > New: < me : User | none > *********** rule (built-in rule for symbol __) Old: no-op(me, other) < me : User | none > no-op(me, other) < me : User | none > ---> < me : User | none > New: < me : User | none > rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second) result Object: < me : User | none > show profile . op __ : [Configuration] [Configuration] -> [Configuration] . built-in rl rewrites: 1 (50%) rl no-op(X, Y) < X : User | AS > => < X : User | AS > . rewrites: 1 (50%) Even though only one rewrite takes place, there is a "fake" rewrite generated because the rewrite happened inside of the configuration symbol code (which handles object-message rewriting and messages to/from external objects in a built-in way and generates any trace calls for them) and the traversal code believes a rewrite happened because the configuration symbol code returned a changed dag. Rather than make the generic traversal code aware of strangeness in the configuration symbol's handling of rule rewriting which would break the theory interface, the configuration symbol code now tells the trace/break/profile code to ignore the fake rewrite. (2) A pair of symmetric bugs in the metaMatch() and metaXmatch() descent functions where membership axiom applications and equational rewrites required to compute the sorts in the subject were counted twice in the the global total. Provoked by the following examples: fmod MATCH is sorts Foo Bar . subsorts Foo < Bar . op f : Bar Bar -> Bar [comm] . ops g h : Foo -> Foo . ops a b c d e : -> Foo . vars X Y : Bar . var Z : Foo . cmb f(X, Y) : Foo if h(X) = g(Y) . eq h(a) = b . eq g(c) = b . eq h(c) = d . eq g(a) = d . endfm set trace on . set show breakdown on . red in META-LEVEL : metaMatch(['MATCH], 'Z:Foo, 'f['a.Foo, 'c.Foo], nil, 0) . red in META-LEVEL : metaXmatch(['MATCH], 'Z:Foo, 'f['a.Foo, 'c.Foo], nil, 0, unbounded, 0) . (3) Symmetric bugs to the above for getMatch() and getXmatch() in the meta-interpreter. Illustrated by the following example: load metaInterpreter fmod MATCH is sorts Foo Bar . subsorts Foo < Bar . op f : Bar Bar -> Bar [comm] . ops g h : Foo -> Foo . ops a b c d e : -> Foo . vars X Y : Bar . var Z : Foo . cmb f(X, Y) : Foo if h(X) = g(Y) . eq h(a) = b . eq g(c) = b . eq h(c) = d . eq g(a) = d . endfm mod MATCH-TEST is pr META-INTERPRETER . op me : -> Oid . op User : -> Cid . op soln:_ : Nat -> Attribute . vars X Y Z : Oid . var AS : AttributeSet . var N : Nat . rl < X : User | AS > createdInterpreter(X, Y, Z) => < X : User | AS > insertModule(Z, X, upModule('MATCH, true)) . rl < X : User | soln: N, AS > insertedModule(X, Y) => < X : User | AS > getMatch(Y, X, 'MATCH, 'Z:Foo, 'f['a.Foo, 'c.Foo], nil, N) . endm set trace on . set show breakdown on . erew in MATCH-TEST : <> < me : User | soln: 0 > createInterpreter(interpreterManager, me, none) . (4) A memory leak in the functional metalevel descent function metaGetVariant() where the start term is successfully pulled down but the list of blocker terms is not. Illustrated by this example: fmod XOR is sorts Elem . op c : -> Elem . endfm fmod TEST is inc XOR . inc META-LEVEL . endfm red metaGetVariant(['XOR], 'c.Elem, 'bad.Elem, 0, 0) . (5) A bug in rewrite search where incorrect rule rewrite steps were made for AC(U) with repeated arguments. This is because of different conventions for storing nominal vs physical argument indices. For search it is advantageous only to consider an AC(U) argument of multiplicity > 1 just once. But in other code such as fair rewriting, such arguments need to be unshared. In alpha 111b I rationalized the argument stacking code to use nominal argument indicies everywhere, not realizing that certain argument replacement code was expecting physical argument indices. Illustrated by this example from Carolyn: mod VENDING-MACHINE is sorts Coin Item Place Marking . subsorts Coin Item < Place < Marking . op __ : Marking Marking -> Marking [ctor assoc comm id: null] . op null : -> Marking [ctor] . op $ : -> Coin [ctor format (r! o)] . op q : -> Coin [ctor format (r! o)] . op a : -> Item [ctor format (b! o)] . op c : -> Item [ctor format (b! o)] . rl [buy-c] : $ => c . rl [buy-a] : $ => a q . rl [change]: q q q q => $ . endm *** bad extra results srewrite in VENDING-MACHINE : $ $ $ using all . *** runaway execution search $ $ $ =>! a a M:Marking . (6) A related bug where top-down rule rewriting can make the wrong replacement and get stuck in an infinite loop. Illustrated by: mod FOO is sort Foo . op __ : Foo Foo -> Foo [assoc comm] . ops a b c : -> Foo . rl b => c . endm *** runaway execution rew a a b . New features ============= (1) There is a new smart load directive: sload that loads the named file only if it has changed (determined by the file system's modify time) since it was last read (via in, load, sload or command line argument). Also the maximum depth of nested file inclusions is increased from 10 to 100. These changes were motived by an email discussion with Everett Hildenbrandt regarding changes to support large Maude libraries. Note that since modify times are stored as seconds since Epoch, there is a potential race condition if a file is modified, loaded, and modified again within the space of a second, so sload is best used to load relatively static files rather than machine generated/updated ones. (2) There are a number of extensions to the meta-interpreter. (a) Finding the largest arities for a given operator that yield a sort less than or equal to a given sort is supported by: op getMaximalAritySet : Oid Oid Qid Qid TypeList Sort -> Msg [ctor msg format (b o)] . where the second Qid is the operator prefix name, TypeList is some arity that uniquely identifies the operator wrt ad hoc overloading and Sort is the given sort. The reply has the form: op gotMaximalAritySet : Oid Oid TypeListSet -> Msg [ctor msg format (m o)] . (b) Normalizing with respect to theories and computing the syntactic least sort is supported by: op normalizeTerm : Oid Oid Qid Term -> Msg [ctor msg format (b o)] . The reply has the form: op normalizedTerm : Oid Oid Term Type -> Msg [ctor msg format (m o)] . Note that this generalizes metaNormalize() and leastSort() from the functional metalevel. (c) Unification and disjoint unification are now supported. Unlike the descent functions in the functional metalevel, fresh variables are handled by the newer mechanism of disjoint families of fresh variables introduced with the new vu-narrowing descent functions rather than the old, ever-increasing indices on a single family of fresh variables. As with match and search, multiple results are obtained by passing an index to the required result. In order to handle result exhaustion, there is a new message: op noSuchResult : Oid Oid Bool -> Msg [ctor msg format (m o)] . where the Bool argument is true if the unification was complete and false if unifiers may have been missed due to an incomplete unification algorithm. Unification is handed by the request: op getUnifier : Oid Oid Qid UnificationProblem Qid Nat -> Msg [ctor msg format (b o)] . and the reply: op gotUnifier : Oid Oid Substitution Qid -> Msg [ctor msg format (m o)] . Here the final Qid must be '#, '%, or '@ and indicates a fresh variable family whose variables may occuring in the unificand, while the Qid in the reply indicates the fresh variable family used to express the unifiers which will be different from the one passed in the request. Disjoint unification is entirely analogeous, using the messages: op getDisjointUnifier : Oid Oid Qid UnificationProblem Qid Nat -> Msg [ctor msg format (b o)] . op gotDisjointUnifier : Oid Oid Substitution Substitution Qid -> Msg [ctor msg format (m o)] . The difference here is that variables occuring in terms on the left side of _=?_ are considered disjoint from variables occuring on the right side of _=?_ even if they have the same name. Unifiers are returned as a pair of substitutions, the first for variables occuring in terms on the left of _=?_ and the second for variables occuring in terms on the right of _=?_ (d) Variant generation is now suppored by: op getVariant : Oid Oid Qid Term TermList Bool Qid Nat -> Msg [ctor msg format (b o)] . Here the Term is the start term, the TermList is a list of blocker terms, the Bool is false for regular variant generation and true for irreducible variant generation. The Qid names a fresh variable family that may occur in the start term and the Nat is the number of the variant requested. The usual reply is the message: op gotVariant : Oid Oid RewriteCount Term Substitution Qid Parent Bool -> Msg [ctor msg format (m o)] . Here RewriteCount is the number of narrowing steps and equational rewrites, however its definition is a little complicated. Because it gets added to the top level rewrite count, these counts must be incremental. Variants are generated layer at a time. Assuming variants are generated in ascending order, for normal variant generation, all the narrowing steps and equational rewrites required to generate one layer from the next are assigned to the first variant extracted from that layer, since those narrowing steps and rewrites are done, regardless whether the other variants in that layer are ever requested. In the irredundant case, all the variants are generated up front, so that redundant variants can be eliminated and so all the narrowing steps and rewrites do to generate the complete set of variants is assigned to the first variant generated. For a variant generated out of order the count is complicated but faithfully represents the work done to generate that variant. The variant itself is the (Term, Substitution) pair and the Qid gives the family of fresh variables that appear in the variant Term and the right hand side of the Substitution. Parent is the index of the variant from which this variant was generated, except for the initial variant which has Parent none. Bool is true if there are more variants in the current layer and false if extracting the next variant forces generation of the next layer (unless it was already generated, in the irredundant case). When a request variant does not exist, the reply is: op noSuchResult : Oid Oid RewriteCount Bool -> Msg [ctor msg format (m o)] . In the usual case, assuming that variants are requested in order, RewriteCount accounts for any narrowing steps or rewrites performed while failing to generate new variants. In the irredundant case, the RewriteCount will be zero, unless a nonexistent variant is requested at the outset, in which case RewriteCount accounts for the entire cost of the variant narrowing search. The Bool argument is true if the variant search was complete and false if variants may have been missed due to incomplete unification algorithms. (e) Variant unifier find generation is supported by: op getVariantUnifier : Oid Oid Qid UnificationProblem TermList Qid Nat -> Msg [ctor msg format (b o)] . where TermList a list of blocker terms, Qid is a fresh variable family whose variables can occur in the UnificationProblem and Nat is the index of the wanted unifier. When the requested unifier exists, the reply is: op gotVariantUnifier : Oid Oid RewriteCount Substitution Qid -> Msg [ctor msg format (m o)] . where Qid is the fresh variable family used to express the assignments in the unifier. If the requested unifier does not exist, the message op noSuchResult : Oid Oid RewriteCount Bool -> Msg [ctor msg format (m o)] . is used, as with variant generation. Disjoint variant unifer generation is support by messages: op getDisjointVariantUnifier : Oid Oid Qid UnificationProblem TermList Qid Nat -> Msg [ctor msg format (b o)] . and op gotDisjointVariantUnifier : Oid Oid RewriteCount Substitution Substitution Qid -> Msg [ctor msg format (m o)] . which is entirely analogous, but with the reply returning two substitutions, one for variables occuring on the left of _=?_ in the problem and one for variables onccuring on the right. (f) Printing a meta-term into a list of Qids, with various printing options is supported by: op printTerm : Oid Oid Qid Term PrintOptionSet -> Msg [ctor msg format (b o)] . Here the PrintOptionSet argument take the same set of options supported by metaPrettyPrint(). The reply is: op printedTerm : Oid Oid QidList -> Msg [ctor msg format (m o)] . (g) Parsing a list of Qids to a meta-term, possibly specifying the Type is supported by: op parseQidList : Oid Oid Qid QidList Type? -> Msg [ctor msg format (b o)] . Here, as with metaParse(), anyType can be passed as the Type? argument. The reply is: op parsedQidList : Oid Oid ResultPair? -> Msg [ctor msg format (m o)] . Here the ResultPair? values are identical to those returned by metaParse(), including the possibilities of noParse() and ambiguity(). Steven