Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha126/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha126/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This is the first public alpha release that integrates the work of Rubén Rafael Rubio Cuéllar on extending the strategy language and reflecting it in the functional metalevel into the main development source tree (this is the reason the number has jumped from 123 to 126). This version comes with Linux binaries only for the moment due to my new Mac build environment not being set up yet. Rubén has volunteered to make the Mac binaries and I'll put them up as soon as he does. Bug fixes ========== (1) A memory leak in the case of a failed view instantiation. Found and fixed by Rubén. (2) A bug where condition fragments were not being profiled unless tracing was enabled. Found by Rubén and illustrated by the following example: fmod COLLATZ is pr NAT . op f : Nat -> Nat . var N : NzNat . ceq f(s N) = f((s N) quo 2) if (s N) rem 2 = 0 . ceq f(s N) = f(3 * (s N) + 1) if (s N) rem 2 = 1 . endfm set profile on . red f(27) . show profile . (3) A bug where an end-of-file occurring inside a comment sent Maude into a loop, spitting out the message "Saw null character in comment." This appear to be due to a bug in the flex scanner generator which turns the end-of-file condition into an infinite string of NUL characters. For the moment there is an ugly workaround where a NUL occurring in a file is treated as an EOF. Reported by Carolyn and Rubén. New features ============= (1) The internal strategy language has been extended with several new operators and the ability to have strategy modules which allow the definition of recursive strategies. These are described in section 4 of the recently published paper on Maude: https://doi.org/10.1016/j.jlamp.2019.100497 with further discussion of parameterized strategies in: https://link.springer.com/chapter/10.1007%2F978-3-030-23220-7_2 More details and examples also appear in the webpage devoted to this subject: http://maude.sip.ucm.es/strategies/ (2) The internal strategy language is reflected in the metalevel. The srewrite/dsrewrite commands are reflect by the descent function: op metaSrewrite : Module Term Strategy SrewriteOption Nat ~> ResultPair? where the SrewriteOption is used to control whether srewrite or dsrewrite operational semantics is required. sort SrewriteOption . ops breadthFirst depthFirst : -> SrewriteOption [ctor] . (3) The internal strategy language is reflected in the meta-interpreter by request/reply messages corresponding to the commands srewrite/dsrewrite. op srewriteTerm : Oid Oid Qid Term Strategy SrewriteOption Nat -> Msg . op srewroteTerm : Oid Oid RewriteCount Term Type -> Msg . (4) There is a new command line option: -erewrite-loop-mode This is intended to ease the transition from the LOOP-MODE/META-LEVEL way of doing things to the more general object-oriented STD-STREAM/LEXICAL/META-INTERPRETER approach, by executing loop mode rewrites using erewrite rather than rewrite. Previously one could use META-LEVEL with STD-STREAM/LEXICAL but there was no way to use META-INTERPRETER from LOOP-MODE since meta-interpreters are external objects. (5) The is a new print option: set print constants with sorts on . that forces a constant c of sort s to be printed as (c).s even if disambiguation is not strictly needed. It applies to built-in constants such as -1/2 and "foo" as well as user constants. For signatures that are strictly preregular, when combined with set print with aliases off . this allows the overloading in a term to be disambiguated in a strictly bottom up manner as is done with metaterms. Note that as usual, sorts may be abbreviated to sort. Also constants may be abbreviated to constant or const. Requested by Mark-Oliver Stehr Other changes ============== (1) Bubbles now only disallow excluded tokens when they are outside of the chosen parentheses (if parentheses are part of the bubble spec). (2) The following 6 descent functions which previously took a Nat specifying a variable index as there second to last argument, now take a Qid specifying a variable family. op metaUnify : Module UnificationProblem Qid Nat ~> UnificationPair? . op metaDisjointUnify : Module UnificationProblem Qid Nat ~> UnificationTriple? . op metaGetVariant : Module Term TermList Qid Nat ~> Variant? . op metaGetIrredundantVariant : Module Term TermList Qid Nat ~> Variant? . op metaVariantUnify : Module UnificationProblem TermList Qid Nat ~> UnificationPair? . op metaVariantDisjointUnify : Module UnificationProblem TermList Qid Nat ~> UnificationTriple? . The 3 result constructors that previously returned a Nat specify a variable index now return a Qid specifying a variable family. op {_,_} : Substitution Qid -> UnificationPair [ctor] . op {_,_,_} : Substitution Substitution Qid -> UnificationTriple [ctor] . op {_,_,_,_,_} : Term Substitution Qid Parent Bool -> Variant [ctor] . Because the domain of: op {_,_} : Substitution Qid -> UnificationPair [ctor] . clashes with the domain of the longstanding operator: op {_,_} : Substitution Context -> MatchPair [ctor] . due to Context and Qid being in the same kind, the following hack: sort MatchOrUnificationPair . subsort MatchPair UnificationPair < MatchOrUnificationPair . is used to make them subsort polymorphic and avoid a preregularity error. Only matchPairSymbol is hooked to the metalevel since all op-hooks are at the kind level where the above constructors for MatchPair and UnificationPair are indistinguishable. Of course non-error terms constructed with matchPairSymbol will have sort MatchPair or UnificationPair depending on the sort of the second argument. The reason for this change is that variable indices don't scale as we have no way to garbage collect and reuse variable indices. By using the variable families '#, '% and '@, the space of fresh variable names is divided into thirds and only one third is used to express the problem and a disjoint third is used to express solutions. For these descent functions, we only need two families; however three are needed for the narrowing with variant unification descent functions which prompted the introduction of variable families in the first place. In the case that a problem uses fresh variable names outside of the family passed in the descent function call, Maude will issue a warning and the descent function will not reduce and the result will be at the kind level. The old versions of these 6 descent functions and 3 result constructors are still available for backwards compatibility with Maude 2.* and will remain at least in the upcoming Maude 3.* series, but are deprecated and may disappear in Maude 4. Their hooks now start with the word "legacy" to distinguish them from the new versions, but the actual operators are merely ad hoc overloaded so as not to break existing code. (3) The sort EmptyTypeSet had been renamed EmptyQidSet This sort only exists for a technical reason: to move none to a sort below SortSet and KindSet so it should not normally appear in user code. (4) META-LEVEL contains declarations for VariableSet that are completely analogeous to SortSet, KindSet and TypeSet: sorts NeVariableSet VariableSet . subsort Variable < NeVariableSet < VariableSet . subsort EmptyQidSet < VariableSet . op _;_ : VariableSet VariableSet -> VariableSet [ctor ditto] . op _;_ : NeVariableSet VariableSet -> NeVariableSet [ctor ditto] . This is pure subsorting and subsort polymorphism with no new operators introduced. (5) metaParse(), metaPrettyPrint(), take an extra agument to specify variables that can be abbreviated. (6) Symmetric changes in the meta-interpreter with parseQidList()/ parsedQidList() being renamed parseTerm()/parsedTerm() op printTerm : Oid Oid Qid Term PrintOptionSet -> Msg [ctor msg format (b o)] . op printedTerm : Oid Oid QidList -> Msg [ctor msg format (m o)] . op parseTerm : Oid Oid Qid QidList Type? -> Msg [ctor msg format (b o)] . op parsedTerm : Oid Oid ResultPair? -> Msg [ctor msg format (m o)] . Steven