Changes from 2.0.1 (alpha81) to alpha82 Bug fixes ========== (1) Infinity and -Infinity now work on MacOSX (and FreeBSD) - previously Infinity was converted to 0. Reported by Carolyn. (2) Various bugs in show module (and show all) commands fixed. Reported by Narciso. (3) Break points no longer cause an internal error when executing builtin function symbols. Reported by Christiano Braga. (4) metaPrettyPrint() now handles variables at the kind level correctly. Reported by Joe Hendrix. (5) Printing a sort redeclaration warning from the metalevel no longer causes an internal error. Reported by Peter Olveczky. (6) Various files (ChangeLogs and compiler code) that were accidently left out of the last source tree are included - automake files are fixed. Other changes ============== (1) The semantics over owise equations wrt operator level strategies has changed. Now owise equations can only be used in evaluating the final 0 of a strategy. This change was suggested by Joe Hendrix. (2) The Int operators quo, rem, gcd, lcm, divides now work on Rats. quo gives the number of whole times a rational can be divided by another, rem gives the rational remainder. divides returns true if a rational divides a rational a whole number of times. gcd returns the largest rational that divides into each of its arguments a whole number of times while lcm returns the smallest rational that is an integer multiple of its arguments. (3) Ctor coloring is now supported for iter symbols: set print color on . fmod ITER-COLOR is sorts Nat0 Nat1 Nat2 Nat . subsort Nat0 Nat1 Nat2 < Nat . op s_ : Nat0 -> Nat1 [iter ctor] . op s_ : Nat1 -> Nat2 [iter ctor] . op s_ : Nat2 -> Nat0 [iter] . op 0 : -> Nat0 [ctor] . endfm red s 0 . red s s 0 . red s s s 0 . red s s s s 0 . (4) META-LEVEL has two new polymorpic functions: op upTerm : Universal -> Term [special (...)] . op downTerm : Term Universal -> Universal [special (...)] . upTerm() converts a term into it's meta-representation, while downTerm() converts a meta-term into a regular term. They can handle regular terms at the kind level. The 2nd argument to downTerm is a term belonging to the appropriate component that is returned should the meta-term not represent a valid term in that component. fmod UP-DOWN-TEST is inc META-LEVEL . sort Foo . ops a b c d e : -> Foo . op f : Foo Foo -> Foo . eq c = d . endfm red upTerm(upTerm(f(a, f(b, c)))) . red downTerm(downTerm(upTerm(upTerm(f(a, f(b, c)))), X:Term), a) . (5) The configuration now supports building without Tecla (--with-tecla=no). Requested by Ambarish. Changes from alpha82 to alpha83 Bug fixes ========== (1) A bug in the meta-context code where iter operators were not properly handled. Reported by Alberto Verdejo, and provoked by the following example: red in META-LEVEL : metaXmatch(mod 'SORTING is protecting 'BOOL . protecting 'STRING . protecting 'NAT . sorts 'Pair ; 'PairSet . subsort 'Pair < 'PairSet . op '<_;_> : 'Nat 'String -> 'Pair [none] . op '__ : 'PairSet 'PairSet -> 'PairSet [assoc comm id('empty.PairSet)] . op 'empty : nil -> 'PairSet [none] . none none rl '__['<_;_>['J:Nat,'X:String],'<_;_>['I:Nat,'Y:String]]=> '__['<_;_>[ 'J:Nat,'Y:String],'<_;_>['I:Nat,'X:String]] [label('switch)] . endm, '__['<_;_>['B:Nat,'C:String],'<_;_>['A:Nat,'D:String]], '__['<_;_>['s_['0.Zero],'"d".Char],'__['<_;_>['s_^2['0.Zero], '"b".Char],'__['<_;_>['s_^3['0.Zero],'"a".Char],'<_;_>['s_^4['0.Zero], '"c".Char]]]], '_and_['_<_['B:Nat,'A:Nat],'_>_['C:String,'D:String]] = 'true.Bool, 0, unbounded, 0) . (2) A bug in the handling of bubbles at the object level where adding an "Exclude" id-hook caused the bubble property to be ignored. Provoked by the following example: fmod BUBBLE-TEST is inc QID-LIST . sort Text . op text : QidList -> Text [special ( id-hook Bubble (1 -1 ( )) id-hook Exclude ( x y z ) op-hook qidSymbol ( : ~> Qid) op-hook qidListSymbol (__ : QidList QidList ~> QidList))] . op f : Text -> Bool . endfm red f( a c b ) . Other changes ============== (1) Polymorphic operators are now declared explicitly by the polymorphic (abbreviates to poly) attribute. This take a set of integers enclosed in parentheses that indicates which arguments are polymorphic; 0 indicates the range. For polymorphic operators that are not constants, at least one argument should be polymorphic to avoid ambiguities. Since there are no polymorphic equations, polymorphic operators are limited to constructors and builtins. Polymorphs are always instantiated with the polymorphic arguments going to the kind level which further limits their generality. The sort name in a polymorphic position is purely a place holder - any legal type name could be used but it seems a useful convention to use "Universal". One reasonable use for polymorphic operators beyond the existing builtins is to define hetrogeneous lists: fmod HET-LIST is inc CONVERSION . sort List . op nil : -> List . op __ : Universal List -> List [ctor poly (1)] . endfm red 4 "foo" 4.5 1/2 nil . The polymorphic attribute is reflected by: op poly : NatList -> Attr [ctor] . (2) The show all and show mod commands now print out the special attribute and its hooks. (3) The set of ascent functions is completed with: op upModule : Qid Bool ~> Module . op upImports : Qid ~> ImportList . op upSorts : Qid Bool ~> SortSet . op upSubsortDecls : Qid Bool ~> SubsortDeclSet . op upOpDecls : Qid Bool ~> OpDeclSet . These work in an analogous fashion to the existing ascent functions. Note that upImports() does not take a Bool since it is not useful to query the imports of a flattened module. Changes from alpha83 to alpha83a 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. Changes from alpha83a to 2.1 (alpha84) Bug fix ======== A bug in the post syntax error clean up code which freed module expression structures that it should not, resulting in memory corruption, random warnings, and an internal error following a syntax error. Reported by Azadeh Farzan and Carolyn. For example: fmod FOO is protecting NAT . op f : -> Nat Nat . endfm fmod FOO is endfm Other changes ============== This version uses recently released Tecla 1.5.0 which resolves various issues on newer linux versions. Unfortunately I haven't been able to get this Tecla version to build under Panther so the Darwin binary still uses Tecla 1.4.1. The is also to possibility that the Darwin binary may not run under earlier MacOS X versions. There is now a rudimentary test suite in the source tree; use make check to run it after building from source. In order to support automated testing the is a new command line flag -no-banner which suppresses the banner (which will differ between versions making output comparison harder).