Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha121/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha121/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This version introduces a reimplementation of the module system to fix various bugs and support parameterized views. Bug fixes ========== (1) A bug where the arguments of module summation were commuted. This really only affects error reporting and the show mod command: fmod FOO is pr NAT + QID . endfm show mod . produced: fmod FOO is protecting QID + NAT . endfm (2) A memory leak where a partial module expression was not garbage collected because of a syntax error; provoked by: fmod FOO is pr NAT + FLOAT + . endfm and visible with a memory analysis tool. (3) A bug where the number of sorts imported from parameter theories isn't recorded unless the parameterized module has at least one regular import. This leads to a situation where uses of a sort from a parameter theory can be renamed, while the imported sort is not, causing memory corruption. Illustrated by: parameter theories: set include BOOL off . fmod FOO{P :: TRIV} is op a : -> P$Elt . endfm fmod BAR{Q :: TRIV} is inc FOO{Q} * (sort Q$Elt to Bad{Q}) . endfm (4) A symmetric bug in the recording of the number of operators imported from a parameter theory, allowing the use of such an operator to be renamed while the operator declaration is not. Illustrated by: set include BOOL off . fth T is sort Elt . op 0 : -> Elt . endfth fmod FOO{P :: T} is op a : -> P$Elt . eq a = 0 . endfm fmod BAR{Q :: T} is inc FOO{Q} * (op 0 to 1) . endfm show all . (5) A symmetric bug in the recording of the number of polymorphic operators imported from a parameter theory, allowing the use of such an operator to be renamed while the operator declaration is not. Illustrated by: set include BOOL off . fth T is sort Elt . op f : Poly -> Elt [poly (1)] . endfth fmod FOO{P :: T} is op a : -> P$Elt . op b : -> P$Elt . eq f(a) = b . endfm fmod BAR{Q :: T} is inc FOO{Q} * (op f to g) . endfm show all . (6) A bug in parameterization where the construction of parameter copies of theories was assumed not to fail, but could be tricked into failing by a funky user sort. Illustrated by: fmod FOO is sort Z$Elt . *** nasty endfm fth TRIV' is inc FOO . sort Elt . endfth fmod BAR{Y :: TRIV'} is sort Bar{Y} . endfm fmod BAZ{Z :: TRIV'} is inc BAR{Z} . endfm (7) A bug where a parameterized module has two polymorphic operators with the same name from different theory parameters that are then instantiated by views to differently named polymophic operators. There is an issue that the view mapping syntax (which is also used internally computing instantiations) is not rich enough to properly distinguish between two polymorphic operators with the same name. Illustrated by: fmod COMMON is sort Common . endfm fth T1 is inc COMMON . op g : Universal Common -> Universal [poly (1 0)] . endfth fth T2 is inc COMMON . op g : Universal -> Common [poly (1)] . endfth fmod M{X :: T1, Y :: T2} is sort Dummy{X,Y} . eq g(A:Dummy{X,Y}) = g(A:Dummy{X,Y}) . *** just to track g endfm fmod M2 is inc COMMON . op h : Universal Common -> Universal [poly (1 0)] . endfm view V2 from T1 to M2 is op g to h . endv fmod M3 is inc COMMON . op not-h : Universal -> Common [poly (1)] . endfm view V3 from T2 to M3 is op g to not-h . endv fmod TEST is inc M{V2,V3} . endfm show all . Another manifestation of this problem is when one polymorphic operator comes from a parameter theory and the other from the parameterized module itself: fth T1 is sort Common . op g : Universal Common -> Universal [poly (1 0)] . endfth fmod M{X :: T1} is op g : Universal -> X$Common [poly (1)] . eq g(A:X$Common) = g(A:X$Common) . *** just to track g endfm fmod M2 is sort Real . op h : Universal Real -> Universal [poly (1 0)] . endfm view V2 from T1 to M2 is sort Common to Real . op g to h . endv fmod TEST is inc M{V2} . endfm show all . Here the operator in the equation became h though it belongs the the module and should not have been mapped. Since these are such pathological examples, rather than come up with a richer internal notation for handling the mapping of polymorphic operators with all the complexity that would add, I simply forbid a parameterized module from having two distinct polymorphic operators with the same name. (8) A bug where infinite view recursion was not detected, resulting in a stack overflow. Illustrated by: view NatSet from TRIV to SET{NatSet} is sort Elt to Set{NatSet} . endv New features ============= (1) Module expressions with bound parameters can now be summed; for example: fmod FOO{X :: TRIV, Y :: TRIV} is inc MAP{X, Y} + SET{X} . endfm In most cases this isn't particularly useful - you could just import the summands separately. Two useful cases are when the summation is subject to a big gnarly renaming or when the resulting module expression is used the to-module for a parameterized view. Summing modules with free parameters is still illegal since free parameters are instantiated by position rather than by name, there is no consistent way to interprete MAP + SET for example. (2) Module-views can now be parameterized. For example: view SetAsDefault{X :: TRIV} from DEFAULT to SET*{X} is sort Elt to Set{X} . op 0 to {} . endv This can then be used in a module instantiation; for example fmod ARRAY-OF-SETS{X :: TRIV, Y :: TRIV} is inc ARRAY{X, SetAsDefault{Y}} . endfm which in turn can be instantiated: fmod TEST is inc ARRAY-OF-SETS{String, Nat} . endfm red in TEST : insert("one", {1}, insert("one-two", {1,2}, empty)) . red in TEST : insert("one", {1}, insert("one-two", {1,2}, empty))["unseen"] . red in TEST : insert("one", {1}, insert("one-two", {1,2}, empty))["one"] . Of course, views can be instantiated directly with another view rather than a parameter from an enclosing module or view. fmod TEST2 is inc ARRAY{String, SetAsDefault{Nat}} . endfm Furthermore, nesting of views is allowed: view ArrayOfSets{X :: TRIV, Y :: TRIV} from TRIV to ARRAY{X, SetAsDefault{Y}} is sort Elt to Array{X,SetAsDefault{Y}} . endv fmod LIST-OF-ARRAYS-OF-SETS{X :: TRIV, Y :: TRIV} is inc LIST{ArrayOfSets{X, Y}} . endfm fmod TEST3 is inc LIST-OF-ARRAYS-OF-SETS{String, Nat} . endfm red in TEST3 : insert("one", {1}, insert("one-two", {1,2}, empty)) insert("one", {1}, insert("one-two-three", {1,2,3}, empty)) insert("two", {2}, insert("one-two-three", {1,2,3}, empty)) . Parameterized views can also be instantiated on theory-views to change the theory of parameters. A rather pointless example would be: fmod TEST4 is inc ARRAY{String, SetAsDefault{DEFAULT}{Nat0}} . endfm red in TEST4 : insert("one", {1}, insert("one-two", {1,2}, empty))["one"] . Just as with module instantiation, a view instantiation that includes a theory-view is nonfinal since the parameter taking the theory-view must be recaptured or instantiated in a final instantiation. Note that as with module instantiations, bound parameters may not be passed in a nonfinal instantiation. Furthermore for both module instantiations and view instantiations, nested view instantiations with bound parameters may not be passed in a nonfinal instantiation. In other words view instantiations with bound parameters must obey the same rule as bare bound parameters. One subtle point is that an operator-to-term mapping in a parameterized view may use any operators in the (parameterized) to-module in its to-term, including operators from parameter-theories. Thus by extension, operator-to-operator mappings may map operators in the from-theory to operators in a parameter-theory and sort-to-sort mappings may map sorts in a from-theory to sorts in a parameter-theory: set include BOOL off . fth T is sort Elt . endfth fth T2 is sort Elt2 . endfth fmod M{X :: T} is sort Foo{X} . op f : X$Elt -> Foo{X} . endfm view V{A :: T} from T2 to M{A} is sort Elt2 to A$Elt . *** mapping from-theory sort to parameter-theory sort endv This can also happen implicitly; though this trick is not recommended: set include BOOL off . fth T is sort Elt . endfth fth T2 is sort A$Elt . *** highly dubious name endfth fmod M{X :: T} is sort Foo{X} . op f : X$Elt -> Foo{X} . endfm view V{A :: T} from T2 to M{A} is *** A$Elt in from-theory is implicitly mapped to A$Elt in parameter-theory endv With these changes, the rules for what can be done with modules and module-views can be summarized in the following tables: Modules: inclusion summation renaming instantiation ------------------------------------------------------------------------------------- no parameters yes yes yes n/a free parameters no no yes yes bound parameters yes yes yes no Module-views: instantiation arg-in-nonfinal-inst arg-in-final-inst --------------------------------------------------------------------------------- no parameters n/a yes yes free parameters yes no no bound parameters no no yes Having parameterized views allows complex nesting of instantiations with bound parameters which can be difficult or impossible to evaluate correctly when the bound parameters are instantiated. Thus 2 technical restrictions are enforced on the use of parameterized views: (i) Every parameter of a parameterized view must appear as a bound parameter in its to-module. If a parameter doesn't appear in the to-module then it is effectively useless and should be removed. While the pathological cases eliminated by this restriction could, in principle, be handled in a consistent way, I see no reason to complicate what is already very complex code in order to do so. This restriction implicitly rules out parameterized theory-views since there it is not legal to have a parameterized theory that could be the to-theory of such a view. (ii) We introduce the notion of a conflict between parameters: Two bound parameters, X and Y are in conflict if X is an argument to a module or view final-instantiation, and Y is a bound parameter in some view expression that is also an argument in the same final-instantiation. For example the module expressions M2{X, V{Y}} and M{V2{X, V{Y}}} both induce a conflict on bound parameters X and Y. Conflicts on bound parameters in a module expression are propagated to the free parameters of a view that uses that module expression as its to-module and to the free parameters of a module that imports that module expression. So for example: view V3{X :: TRIV, Y :: TRIV} from TRIV to M{X, V{Y}} is ... endv receives a conflict between its X and Y parameters. Conflicts are also propagated when parameters are directly instantiated by parameters from an enclosing module or view; so for example fmod M3{A :: TRIV, B :: TRIV} is inc M{V3{A, B}} . ... endfm receives a conflict between its A and B parameters because they are used to instantiate conflicting parameters in V3. A parameter may have a conflict with itself; for example fmod MMAP{X :: TRIV} is inc MAP{X, Set{X}} . endfm For the most part, conflicts are quietly generated and propagated through arbitrarily deep nesting of importations and instantiations without users being aware of them. The only place they become important is in nonfinal instantiations, when the following restriction is enforced: The nonfinal instantiation of a module or view may not pass theory-view arguments to two parameters that have a conflict (or to a parameter that has a conflict with itself). Passing a theory-view to one of a pair of conflicting parameters is allowed as long as the other receives a (unparameterized) module-view (recall bound parameters are not allowed in nonfinal instantiations). This restriction avoids situations where the recapture of a bound parameter following instantiation by a theory-view results in the bound parameter appearing in a nonfinal instantiation. For example, if X and Y were instantiation by theory-views TV1 and TV2 respectively then: M{V2{X, V{Y}}} would become: M{V2{TV1, V{TV2}{Y}}{X}} and Y appears as a bound parameter in a nonfinal instantiation of view V2: V2{TV1, V{TV2}{Y}} (3) The command show views . now includes the instances of parameterized views that have been constructed. Note that since there is no context to distinguish between views and bound parameters, bound parameters are indicated by []s, using the same convention that is used for modules with bound parameters; for example: view SetAsDefault{[Y]} view ArrayOfSets{[X], [Y]} (4) The prelude now contains several parameterized views, from TRIV to the corresponding predefined parameterized modules: view List{X :: TRIV} view WeaklySortableList{X :: STRICT-WEAK-ORDER} view SortableList{X :: STRICT-TOTAL-ORDER} view WeaklySortableList'{X :: TOTAL-PREORDER} view SortableList'{X :: TOTAL-ORDER} view Set{X :: TRIV} view List*{X :: TRIV} view Set*{X :: TRIV} view Map{X :: TRIV, Y :: TRIV} view Array{X :: TRIV, Y :: DEFAULT} So you can now import module expressions such as LIST{Set{Nat}} and SET{List{String}}. But you can also keep the arguments abstract: fmod LIST-TO-SET-MAP{X :: TRIV, Y :: TRIV} is inc MAP{List{X}, Set{Y}} . endfm (5) The above changes to the module system are reflected in the metalevel. The metalevel syntax already supported parameters in view declarations. In order to accomodate view instantiations, which look just like module instantiations at a syntactic level, the metalevel signature is changed with new sorts Expression and ViewExpression and a subsort overloaded instantiation operator: sort Expression ViewExpression ModuleExpression . subsort Sort < Expression < ViewExpression ModuleExpression . op _{_} : Expression NeParameterList -> Expression [ctor prec 37] . op _{_} : ViewExpression NeParameterList -> ViewExpression [ctor ditto] . op _{_} : ModuleExpression NeParameterList -> ModuleExpression [ctor ditto] . Here the sort Expression exists to hold terms like 'I{'Nat} which could be either an instantiation of module 'I or an instantiation of view 'I, depending on context. Note that parameter lists are now required to be nonempty. Also Qids used for module names are required to be valid sort names; so you cannot refer to module names like 'V:Nat , '0.Nat or even '`[Nat`] in module expressions. This is to avoid preregularity issues. Since _,_ for forming parameter lists is shared with terms this restriction previously applied to views and parameter names, but now ViewExpression and ModuleExpression are in the same kind, the restriction has to be extended to module names. The functional metalevel function upView() now understands parameterized views; for example: view ListOfSets{X :: TRIV} from TRIV to LIST{Set*{X}} is sort Elt to List{Set*{X}} . endv red in META-LEVEL : upView('ListOfSets) . Ascent and descent functions now understand view instantiations appearing in module expressions; for example: red in META-LEVEL : metaReduce( fmod 'TEST is including 'BOOL . including 'LIST{'Set*{'String}} . sorts none . none none none none endfm, 'reverse[ '__['`{_`}['_`,_['"a".Char,'"e".Char]], '`{_`}['_`,_['"i".Char,'"y".Char]], '`{_`}['_`,_['"b".Char,'"c".Char]] ] ] ) . The meta-interpreter likewise understands parameterized views and view instantiations, using the same meta-syntax. Currently CVC4 is only supported under Linux - it seems to have been dropped from Mac Ports and I haven't been able to build it from source under Darwin. Steven