Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha92/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha92/ Alpha release site authentication: User Name: maudeabuser Password: bughunter Bug fixes ---------- (1) A bug where the instantiation of a polymorph in a unification problem following a first unification problem caused a crash; provoked by: fmod FOO is sort Foo . ops f g : Foo -> Foo . endfm unify f(X:Foo) =? f(Y:Foo) . unify B:Bool =? f(X:Foo) == g(X:Foo) . What happens is the first unification builds the BDD encodings of the sort structure of each operator needed for order-sorted unification; then the second unification instantiates _==_ and the instantiation doesn't get its BDDs. Now all BDD encodings are built on demand - this potentially save time and space when only a few operators in a module are involved with unification at the cost of checking if the needed ecodings have already been built each time they are needed. Bug reported by Paco. (2) A critical bug in the module system when during the construction of a module corresponding to a complex module expression, the reparsing of a module that has another module change below it can cause the module under construction to be garbage collected (because it doesn't yet have users) cause massive memory corruption. Bug reported by Marc Boyer . This is the simplest example I can find that reliably triggers it: fmod A is sort Foo . endfm *** A will change fmod B is inc A . endfm *** B will be reparsed fmod C is inc A . endfm *** C will be reparsed also fmod A is sort Foo . endfm *** new A fmod D is inc B * (sort Foo to Bar) + C * (sort Foo to Baz) . endfm *** free memory reads all over the place (3) A truly evil bug in the CUI matcher that only occurs under "perfect storm" situations; namely a complex A/AU/AC/ACU matching problem inside a C/CU/CI/CUI/U/UI matching problem which fails to match in a very specific way (to leave unexpected A/AU/AC/ACU subproblems containing root pointers) and is invoked from the metalevel and is followed by the metamodule being booted from the metamodule cache (to make stuff accessible from the unexpected root pointers become stale) and is followed by a garbage collect (to access stuff via stale pointers) Triggered by a Church-Rosser Checker example from Paco, and also by an example from Traian and Grigore. (4) A similar bug in the pending unification stack code that I found by accident while looking for Paco's bug. It's hard to make it crash reliably but free memory reads show up under Purify. (5) A bug where different parts of the module instantiation code disagreed about the renaming of sorts in pathological cases; provoked by this illegal example from Adrian Riesco (ariesco@fdi.ucm.es): view A from TRIV to TRIV + NAT is sort Elt to Nat . endv fmod B is pr LIST{A} . endfm but also by a slight modification to make it legal: view A from TRIV to TRIV + NAT is sort Elt to Nat . endv fmod B{Y :: TRIV + NAT} is pr LIST{A}{Y} . endfm Thanks to Paco for clarifying how this pathological case should be handled. Other changes -------------- (1) The BranchSymbol special now uses the standard sort computation mechanism rather than hand crafted code. This has a couple of visible effects: (a) if_then_else_fi now works properly with order-sorted unification. If the first argument is <= Bool then the sort of the term headed by if_then_else_fi is lub of its other two arguments. (b) if_then_else_fi can report preregularity warnings if it is instantiated on a kind where not all lubs exist. In this case the standard sort computation mechanism picks an arbitrary minimal upper bound. It turns out that (b) bites in the metalevel where: subsorts Constant Variable < Qid Term . Here Constant and Variable do not have a lub so if B:Bool then C:Constant else V:Variable fi has an ambiguous sort. In Maude 1.0 missing lubs were handled using the rather awkward mechanism of union sorts whereas in Maude 2.0 we ditched union sorts and swept the problem under the carpet. In order to avoid warnings in the metalevel (and potentially missing order-sorted unifiers) there is now a new sort TermQid which intuitively corresponds to a Qid that is also Term and: subsorts Constant Variable < TermQid < Qid Term . (2) More overparsing; recovers gracefully from: fmod FOO{X : TRIV} is sort Foo{X} . endfm (3) The search command now allows rewrite condition fragments for consistancy with metaSearch(). For example: mod FOO is sort Foo . ops a b c : -> Foo . rl a => b . rl b => c . rl c => a . endm search a =>+ X:Foo such that X:Foo => c . Note that results that yield different values for variables in the side condition are considered to be distinct so: search a =>+ X:Foo such that X:Foo => Y:Foo /\ Y:Foo => c . yields 9 solutions. (4) There is now meta-syntax for views: fmod META-VIEW is protecting META-MODULE . *** sort mappings sorts SortMapping SortMappingSet . subsort SortMapping < SortMappingSet . op sort_to_. : Sort Sort -> SortMapping [ctor] . op none : -> SortMappingSet [ctor] . op __ : SortMappingSet SortMappingSet -> SortMappingSet [ctor assoc comm id: none format (d ni d)] . eq S:SortMapping S:SortMapping = S:SortMapping . *** operator mappings sorts OpMapping OpMappingSet . subsort OpMapping < OpMappingSet . op (op_to_.) : Qid Qid -> OpMapping [ctor] . op (op_:_->_to_.) : Qid TypeList Type Qid -> OpMapping [ctor] . op (op_to term_.) : Term Term -> OpMapping [ctor] . op none : -> OpMappingSet [ctor] . op __ : OpMappingSet OpMappingSet -> OpMappingSet [ctor assoc comm id: none format (d ni d)] . eq O:OpMapping O:OpMapping = O:OpMapping . sort View . op view_from_to_is__endv : Header ModuleExpression ModuleExpression SortMappingSet OpMappingSet -> View [ctor gather (& & & & &) format (d d d d d d d n++i ni n--i d)] . endfm and a new function for op upView : Qid ~> View [...] . for getting a the metarepresentation of a view from the interpreters view data base. (5) There is now a very crude meta-interpreter. Essentially most of Maude has been virtualized and lives in a class, so that multiple maude interpreter objects can be created. The meta-interpreter is an interface to these objects using Maude's object system. Meta-interpreters are created much like sockets by sending them a message to a special interpreterManager object and have names like interpreter(0). The signature of messages implemented so far is: od META-INTERPRETER is protecting META-LEVEL . including CONFIGURATION . op interpreter : Nat -> Oid . op createInterpreter : Oid Oid -> Msg [ctor msg format (b o)] . op createdInterpreter : Oid Oid Oid -> Msg [ctor msg format (m o)] . op insertModule : Oid Oid Module -> Msg [ctor msg format (b o)] . op insertedModule : Oid Oid -> Msg [ctor msg format (m o)] . op showModule : Oid Oid Qid Bool -> Msg [ctor msg format (b o)] . op showingModule : Oid Oid Module -> Msg [ctor msg format (m o)] . op reduceTerm : Oid Oid Qid Term -> Msg [ctor msg format (b o)] . op reducedTerm : Oid Oid Nat Term Sort -> Msg [ctor msg format (m o)] . op rewriteTerm : Oid Oid Bound Qid Term -> Msg [ctor msg format (b o)] . op rewroteTerm : Oid Oid Nat Term Sort -> Msg [ctor msg format (m o)] . op frewriteTerm : Oid Oid Bound Nat Qid Term -> Msg [ctor msg format (b o)] . op frewroteTerm : Oid Oid Nat Term Sort -> Msg [ctor msg format (m o)] . op quit : Oid Oid -> Msg [ctor msg format (b o)] . op bye : Oid Oid -> Msg [ctor msg format (m o)] . op interpreterManager : -> Oid [special ...] . endm It should be self explanatory. Remember that a new meta-interpreter is empty, without any of the stuff in the prelude. At some point there should be a way for an meta-interpreter to read from a file, but file handling is one of the areas that has not yet been virtualized. Meta-interpreters have an advantage over the current metalevel in that return messages need not be functional, and thus the number of rewrites (which may vary, depending on memoization) can be returned. Here is an example that shows how to create a meta-interpeter and how to insert modules and reduce a term: load metaInterpreter.maude mod TEST is pr META-INTERPRETER . op me : -> Oid . op User : -> Cid . var X Y Z : Oid . op triv : -> Module . eq triv = ( fmod 'FACT is nil sorts 'Nat . none op '! : 'Nat -> 'Nat [none] . op '* : 'Nat 'Nat -> 'Nat [none] . op '+ : 'Nat 'Nat -> 'Nat [none] . op '0 : nil -> 'Nat [none] . op 's : 'Nat -> 'Nat [none] . none eq '!['0.Nat] = 's['0.Nat] [none] . eq '!['s['X:Nat]] = '*['s['X:Nat],'!['X:Nat]] [none] . eq '*['0.Nat,'Y:Nat] = '0.Nat [none] . eq '*['s['X:Nat],'Y:Nat] = '+['*['X:Nat,'Y:Nat],'Y:Nat] [none] . eq '+['0.Nat,'Y:Nat] = 'Y:Nat [none] . eq '+['s['X:Nat],'Y:Nat] = 's['+['X:Nat,'Y:Nat]] [none] . endfm ) . op test : -> Module . eq test = ( fmod 'TEST is including 'FACT . sorts none . none op 't : 'Nat -> 'Nat [none] . none eq 't['X:Nat] = '+['X:Nat,'!['X:Nat]] [none] . endfm ) . sort State . ops 1 2 3 4 5 6 7 : -> State [ctor] . op state:_ : State -> Attribute [ctor] . rl < X : User | state: 1 > createdInterpreter(X, Y, Z) => < X : User | state: 2 > insertModule(Z, X, triv) . rl < X : User | state: 2 > insertedModule(X, Y) => < X : User | state: 3 > insertModule(Y, X, test) . rl < X : User | state: 3 > insertedModule(X, Y) => < X : User | state: 4 > reduceTerm(Y, X, 'TEST, 't['s['s['s['0.Nat]]]]) . endm erew <> < me : User | state: 1 > createInterpreter(interpreterManager, me) . In this release I've dropped binary support for PPC Macs and 32-bit Linux boxes though these versions could be built from source if needed. Steven