3.4beta

NEWS

@@ -1,3 +1,18 @@
+Overview of Changes in Maude 3.4 beta (alpha158) (2023-03-12)
+=============================================================
+* fixed bug where LaTeX for op names in declarations, renamings
+and views sometimes used the wrong font
+* comments in LaTeX no longer use the comment environment
+* fixed bug where the strategy part of an srewrite command was
+omitted in the LaTeX comment
+* fixed bug where show desugared omitted local op declarations
+that overloaded imported operators
+* changed the LaTeX vertical spacing
+* fixed bug where color generated by a format attribute could
+run in the followed text in LaTeX output
+* fixed bug where a newline generated by a format attribute
+reset the color to black in LaTeX output
+
 Overview of Changes in alpha157 (2024-02-27)
 ============================================
 * fixed bug where debugging information was being printed to

configure

@@ -1,6 +1,6 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.69 for Maude alpha157.
+# Generated by GNU Autoconf 2.69 for Maude 3.4beta.
 #
 # Report bugs to <[email protected]>.
 #
@@ -580,8 +580,8 @@ MAKEFLAGS=
 # Identity of this package.
 PACKAGE_NAME='Maude'
 PACKAGE_TARNAME='maude'
-PACKAGE_VERSION='alpha157'
-PACKAGE_STRING='Maude alpha157'
+PACKAGE_VERSION='3.4beta'
+PACKAGE_STRING='Maude 3.4beta'
 PACKAGE_BUGREPORT='[email protected]'
 PACKAGE_URL=''
 
@@ -1312,7 +1312,7 @@ if test "$ac_init_help" = "long"; then
   # Omit some internal or obsolete options to make the list less imposing.
   # This message is too long to be a string in the A/UX 3.1 sh.
   cat <<_ACEOF
-\`configure' configures Maude alpha157 to adapt to many kinds of systems.
+\`configure' configures Maude 3.4beta to adapt to many kinds of systems.
 
 Usage: $0 [OPTION]... [VAR=VALUE]...
 
@@ -1383,7 +1383,7 @@ fi
 
 if test -n "$ac_init_help"; then
   case $ac_init_help in
-     short | recursive ) echo "Configuration of Maude alpha157:";;
+     short | recursive ) echo "Configuration of Maude 3.4beta:";;
    esac
   cat <<\_ACEOF
 
@@ -1490,7 +1490,7 @@ fi
 test -n "$ac_init_help" && exit $ac_status
 if $ac_init_version; then
   cat <<\_ACEOF
-Maude configure alpha157
+Maude configure 3.4beta
 generated by GNU Autoconf 2.69
 
 Copyright (C) 2012 Free Software Foundation, Inc.
@@ -2013,7 +2013,7 @@ cat >config.log <<_ACEOF
 This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 
-It was created by Maude $as_me alpha157, which was
+It was created by Maude $as_me 3.4beta, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   $ $0 $@
@@ -2962,7 +2962,7 @@ fi
 
 # Define the identity of the package.
  PACKAGE='maude'
- VERSION='alpha157'
+ VERSION='3.4beta'
 
 
 cat >>confdefs.h <<_ACEOF
@@ -6623,7 +6623,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
 # report actual input values of CONFIG_FILES etc. instead of their
 # values after options handling.
 ac_log="
-This file was extended by Maude $as_me alpha157, which was
+This file was extended by Maude $as_me 3.4beta, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
@@ -6689,7 +6689,7 @@ _ACEOF
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`"
 ac_cs_version="\\
-Maude config.status alpha157
+Maude config.status 3.4beta
 configured by $0, generated by GNU Autoconf 2.69,
   with options \\"\$ac_cs_config\\"
 

configure.ac

@@ -3,7 +3,7 @@
 #
 #	Initialize autoconf stuff.
 #
-AC_INIT(Maude, alpha157, [[email protected]])
+AC_INIT(Maude, 3.4beta, [[email protected]])
 #
 #	Allow directory names that look like macros.
 #

doc/Makefile.am

@@ -25,4 +25,5 @@ EXTRA_DIST = \
 	alpha154.txt \
 	alpha155.txt \
 	alpha156.txt \
-	alpha157.txt
+	alpha157.txt\
+	alpha158.txt

doc/Makefile.in

@@ -257,7 +257,8 @@ EXTRA_DIST = \
 	alpha154.txt \
 	alpha155.txt \
 	alpha156.txt \
-	alpha157.txt
+	alpha157.txt\
+	alpha158.txt
 
 all: all-am
 

doc/alpha157.txt

@@ -143,7 +143,7 @@ red `(_`)`)(a) .
 red `)_`((a) .
 
 (2) Previously integer exponents and left shifts were limited to 1,000,000 to avoid
-inadvertently runing out of memory. The limit is now ULONG_MAX (9,223,372,036,854,775,807
+inadvertently running out of memory. The limit is now ULONG_MAX (9,223,372,036,854,775,807
 on 64-bit hardware, 4,294,967,295 on 32-bit hardware) which is a hard limit imposed
 by GMP, although as before, if the first argument is 0, 1 or -1 for exponentiation
 or 0 for left shift, then the answer is trivial and arbitrary second arguments can

doc/alpha158.txt

@@ -0,0 +1,58 @@
+Alpha 158 release notes
+========================
+
+Bug fixes
+==========
+
+(1) A bug where the LaTeX for op names in op declarations, renaming and views
+did not use math italic for single character names like f and regular italic
+for simple multi-character names like infinity. Reported by Paco.
+
+(2) A bug where the strategy part of an srewrite command was not printed in the
+LaTeX comment.
+
+(3) A bug where show desugared did not show overloaded declarations for
+imported operators. Illustrated by:
+
+fmod TEST is
+  sort ExtBool .
+  subsort Bool < ExtBool .
+  op _or_ : ExtBool ExtBool -> ExtBool [ditto] .
+endfm
+
+show desugared .
+
+This bug also affected the LaTeX output.
+
+(4) A bug where color generated by a format attribute could run into
+the text following a term in LaTeX output:
+
+mod FOO is
+  op a b : -> Bool [format (r d d)] .
+endm
+
+set print format on .
+
+search a b =>* X:Bool such that a b .
+
+(5) A bug where generating a newline using a format attribute reset the color
+to black in the LaTeX output (this is a LaTeX feature). Illustrated by:
+
+mod FOO is
+  op a b : -> Bool [format (r n o)] .
+endm
+
+set print format on .
+
+search a b =>* X:Bool such that a b .
+
+Other changes
+==============
+
+(1) Comments at the start of each command in latex output no longer use
+\begin{comment} ... \end{comment} to avoid Paco's pathological case.
+Instead just % is used and the printing of user's formatting attributes which
+could included a newline is suppressed.
+
+(2) Changed the LaTeX spacing of show commands so that the command is closer
+to its result than it is to the previous result. 

src/ACU_Theory/ACU_Term.cc

@@ -2,7 +2,7 @@
 
     This file is part of the Maude 3 interpreter.
 
-    Copyright 1997-2021 SRI International, Menlo Park, CA 94025, USA.
+    Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA.
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -118,7 +118,7 @@ ACU_Term::ACU_Term(const ACU_Term& original, ACU_Symbol* symbol, SymbolMap* tran
 }
 
 RawArgumentIterator*
-ACU_Term::arguments()
+ACU_Term::arguments() const
 {
   return new ACU_ArgumentIterator(&argArray);
 }

src/ACU_Theory/ACU_Term.hh

@@ -2,7 +2,7 @@
 
     This file is part of the Maude 3 interpreter.
 
-    Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA.
+    Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA.
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -38,7 +38,7 @@ public:
   //
   //    Member functions required by theory interface.
   //
-  RawArgumentIterator* arguments();
+  RawArgumentIterator* arguments() const;
   void deepSelfDestruct();
   Term* deepCopy2(SymbolMap* translator) const;
   Term* normalize(bool full, bool& changed);

src/ACU_Theory/ChangeLog

@@ -1,3 +1,11 @@
+2024-03-05  Steven Eker  <eker@pup>
+
+	* ACU_Term.cc (ACU_Term::arguments): made const
+
+	* ACU_Term.hh (class ACU_Term): made arguments() const
+
+===================================Maude158===========================================
+
 2024-01-16  Steven Eker  <eker@pup>
 
 	* ACU_Symbol.cc (ACU_Symbol::stackArguments): support

src/AU_Theory/AU_DagNode.cc

@@ -2,7 +2,7 @@
 
     This file is part of the Maude 3 interpreter.
 
-    Copyright 1997-2021 SRI International, Menlo Park, CA 94025, USA.
+    Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA.
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -274,7 +274,7 @@ AU_DagNode::matchVariableWithExtension(int index,
   AU_ExtensionInfo* e = safeCast(AU_ExtensionInfo*, extensionInfo);
   AU_Subproblem* subproblem = new AU_Subproblem(this, 0, argArray.length() - 1, 1, e);
   int min = symbol()->oneSidedId() ? 1 : 2;
-  subproblem->addTopVariable(0, index, min, UNBOUNDED, const_cast<Sort*>(sort));  // HACK
+  subproblem->addTopVariable(0, index, min, UNBOUNDED, sort);
   subproblem->complete();
   returnedSubproblem = subproblem;
   extensionInfo->setValidAfterMatch(false);

src/AU_Theory/AU_Layer.cc

@@ -2,7 +2,7 @@
 
     This file is part of the Maude 3 interpreter.
 
-    Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
+    Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA.
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -107,7 +107,7 @@ AU_Layer::initializeLast(int last, AU_ExtensionInfo* extension)
 }
 
 void
-AU_Layer::addTopVariable(int index, int lowerBound, int upperBound, Sort* sort)
+AU_Layer::addTopVariable(int index, int lowerBound, int upperBound, const Sort* sort)
 {
   int nrVariables = prevVariables.length();
   prevVariables.expandBy(1);

src/AU_Theory/AU_Layer.hh

@@ -2,7 +2,7 @@
 
     This file is part of the Maude 3 interpreter.
 
-    Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
+    Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA.
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -36,7 +36,7 @@ public:
   void initialize(AU_DagNode* subjectDag);
   void initializeFirst(int first, AU_ExtensionInfo* extension);
   void initializeLast(int last, AU_ExtensionInfo* extension);
-  void addTopVariable(int index, int lowerBound, int upperBound, Sort* sort);
+  void addTopVariable(int index, int lowerBound, int upperBound, const Sort* sort);
   void addNode(LocalBinding* difference,
 	       Subproblem* subproblem,
 	       int firstSubterm,
@@ -52,7 +52,7 @@ private:
     int index;
     int lowerBound;
     int upperBound;
-    Sort* sort;
+    const Sort* sort;
     //
     //	For solve-time use
     //

src/AU_Theory/AU_Subproblem.hh

@@ -2,7 +2,7 @@
 
     This file is part of the Maude 3 interpreter.
 
-    Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
+    Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA.
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -44,7 +44,7 @@ public:
 		      int index,
 		      int lowerBound,
 		      int upperBound,
-		      Sort* sort);
+		      const Sort* sort);
   void addNode(int layerNr,
 	       LocalBinding* difference,
 	       Subproblem* subproblem,
@@ -65,7 +65,7 @@ AU_Subproblem::addTopVariable(int layerNr,
 			      int index,
 			      int lowerBound,
 			      int upperBound,
-			      Sort* sort)
+			      const Sort* sort)
 {
   layers[layerNr].addTopVariable(index, lowerBound, upperBound, sort);
 }

src/AU_Theory/AU_Term.cc

@@ -2,7 +2,7 @@
 
     This file is part of the Maude 3 interpreter.
 
-    Copyright 1997-2021 SRI International, Menlo Park, CA 94025, USA.
+    Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA.
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -81,7 +81,7 @@ AU_Term::AU_Term(const AU_Term& original, AU_Symbol* symbol, SymbolMap* translat
 }
 
 RawArgumentIterator*
-AU_Term::arguments()
+AU_Term::arguments() const
 {
   return new AU_ArgumentIterator(argArray);
 }

src/AU_Theory/AU_Term.hh

@@ -2,7 +2,7 @@
 
     This file is part of the Maude 3 interpreter.
 
-    Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA.
+    Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA.
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -38,7 +38,7 @@ public:
   //
   //    Functions required by theory interface.
   //
-  RawArgumentIterator* arguments();
+  RawArgumentIterator* arguments() const;
   void deepSelfDestruct();
   Term* deepCopy2(SymbolMap* translator) const;
   Term* normalize(bool full, bool& changed);

src/AU_Theory/ChangeLog

@@ -1,3 +1,22 @@
+2024-03-05  Steven Eker  <eker@pup>
+
+	* AU_Term.cc (AU_Term::arguments): made const
+
+	* AU_Term.hh (class AU_Term): made arguments() const
+
+	* AU_DagNode.cc (AU_DagNode::matchVariableWithExtension): get
+	rid of const_cast<>
+
+	* AU_Subproblem.hh (AU_Subproblem::addTopVariable): pass sort arg
+	as const
+
+	* AU_Layer.cc (AU_Layer::addTopVariable): pass sort arg as const
+
+	* AU_Layer.hh (class AU_Layer): made sort const in struct TopVariable;
+	updated decl for addTopVariable()
+
+===================================Maude158===========================================
+
 2024-01-16  Steven Eker  <eker@pup>
 
 	* AU_Symbol.cc (AU_Symbol::stackArguments): handle