Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha83a/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha83a/ 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, Solaris and Darwin. Since this version contains a lot of new code and will likely be used as the basis for a 2.1 release at WRLA 2004 I would appreciate people trying to break it. Also the linux version was built on my Mandrake 9.2 home box rather than on my Red Hat 7.3 desktop so I'm hoping it will resolve the tecla/library issue people have been complaining about under newer linux distros. Bug fixes ========== (1) An internal error that occurred when bubbles were imported: fmod FOO is inc QID . sorts Token Foo . op token : Qid -> Token [special(id-hook Bubble (1 1) op-hook qidSymbol ( : ~> Qid))] . op [_] : Token -> Foo . endfm fmod BAR is inc FOO . endfm (2) An nasty memory corruption bug when copying persistent representations of dag nodes. Copying of dags only occurs for non-eager strategies and conditional membership axioms (because cmbs can potentially be applied in lazy subdags) to avoid side effects in shared subdags. Thus this problem only shows up in rare examples such as one by Jose, and the effect of the memory corruption may not be immediately visible even then. (3) An internal error that occurred when a meta-module is incompletely pulled down, and one of the modules it depended on is overwritten: red in META-LEVEL : metaReduce( fmod 'FOO is including 'NAT . sorts 'Foo . none none none X:EquationSet endfm, '0.Nat) . fmod NAT is endfm Other changes ============== The main change is a major overhaul of the module system which now supports simple module expressions formed by summation and renaming. Module expressions can only be used in importation statements. The they have the syntax: ::= | "(" ")" | "+" | "*" := "(" { "," }* ")" := "sort" "to" | "label" "to" | "op" | "op" ":" * "->" := "to" [ "[" + "]" ] + is associative; * binds tighter than + and groups to the left. The only attributes currently allowed are prec, gather and format - the idea is that when you rename an operator, the old syntactic properties may no longer be legal and are reset to defaults unless you explicitly set them with these attributes. Modules are constructed for each subexpression of a module expression and so each signature must be legal. Modules and module expressions are cached both to save time and so that the same module corresponding to a module expression will not be imported twice via a diamond import. Mutually or self recursive imports occurring through module expressions are detected and disallowed. Cached modules generated by module expressions that no longer have any users (if the module(s) containing the module expression have been replaced) are deleted. When a named module A, used in a module expression is replaced, any modules generated for module expressions that (possibly indirectly) depend on A are deleted and any named modules that (possibly indirectly) depend on A are reevaluated if you attempt to use them. Here the notion of "depends on" is transitive through arbitrary nesting of importation and module expressions. Summations are flattened before being evaluated so A + (B + C) creates a single new module A + B + C, which is considered to be an otherwise empty module that includes A, B and C. A summation is an fmod if all the summands are fmods and a mod otherwise. Renaming a module that has imports is a subtle issue. To avoid duplicating imported modules unnecessarily and ending up with a lot of duplicated contents (say many identical copies of BOOL), the module importation structure is maintained throughout the renaming. A module expression A * R evaluates to A if A contains no contents that are affected by R. Otherwise A * R evaluates to a new module A * R' where R' is obtained by deleting those renaming items that don't affect A, and canonizing the types in operator renamings wrt A (see later). If A imports modules B and C, A * R' will import modules found by evaluating B * R' and C * R'. Operators with the poly attribute are only affected by operator renamings that don't specify types. Renaming a module does not change its module type. There are some subtle cases to handle. Consider: fmod A is sort Foo . op a : -> Foo . op f : Foo -> Foo . endfm fmod B is including A . sort Bar . subsort Foo < Bar . op f : Bar -> Bar . endfm fmod C is inc B * (op f : Bar -> Bar to g) . endfm Here the f in A looks as though is isn't affected by the renaming, but because of the subsort declaration in B, it should be renamed for consistency. This is handled is by canonizing the type Bar occurring in the renaming (op f : Bar -> Bar to g) to the kind expression [Foo,Bar] which includes _all_ of the sorts in the kind [Bar] occurring in B. Thus B * (op f : Bar -> Bar to g) evaluates to a new module B * (op f : [Foo,Bar] -> [Foo,Bar] to g) which includes the module expression A * (op f : [Foo,Bar] -> [Foo,Bar] to g) which evaluates to a new module A * (op f : [Foo] -> [Foo] to g) in which f has been renamed. Consider also: fmod A is sorts Foo Bar . endfm fmod B is inc A . op f : Foo -> Foo . endfm fmod C is inc A . subsort Foo < Bar . op f : Bar -> Bar . endfm It is _not_ the case that (B + C) * (op f : Bar -> Bar to g) and (B * (op f : Bar -> Bar to g)) + (C * (op f : Bar -> Bar to g)) evaluate to the same module because in the latter, the f occurring in B will not be renamed. Hence in general * does not distribute over +. Note that this behavior differs from Full Maude where both module expressions evaluate to the same module - which module depends on the order that Full Maude sees the module expressions. Module expressions are reflected in the metalevel through the new META-MODULE declarations: sorts Renaming RenamingSet . subsort Renaming < RenamingSet . op sort_to_ : Qid Qid -> Renaming [ctor] . op op_to_[_] : Qid Qid AttrSet -> Renaming [ctor format (d d d d s d d d)] . op op_:_->_to_[_] : Qid TypeList Type Qid AttrSet -> Renaming [ctor format (d d d d d d d d s d d d)] . op label_to_ : Qid Qid -> Renaming [ctor] . op _,_ : RenamingSet RenamingSet -> RenamingSet [ctor assoc comm prec 43 format (d d ni d)] . op _+_ : ModuleExpression ModuleExpression -> ModuleExpression [ctor assoc comm] . op _*(_) : ModuleExpression RenamingSet -> ModuleExpression [ctor prec 39 format (d d s n++i n--i d)] . in the obvious way. Bashing together of previously unrelated sorts operators and used to be regarded as illegal; however it is now legal and the previous warnings have been downgraded to advisories: fmod FOO is sort Foo . op a : -> Foo . endfm fmod BAR is sort Foo . op a : -> Foo . endfm fmod BAZ is inc FOO + BAR . endfm Note that you get two sets of advisories - one for (FOO + BAR) and one for BAZ. There is a new command show modules . which shows the named and created modules currently in the system. The latter are ephemeral and the garbage collection policy for created modules may change. Operators with the poly attribute may now be ad hoc overloaded (but not subsort polymorphic overloaded). This is not recommended since it can lead to ambiguities for parsing and pretty-printing. Steven