alpha156

ChangeLog

@@ -1,3 +1,10 @@
+2024-01-24  Steven Eker  <eker@pup>
+
+	* tests/ResolvedBugs/conditionSideEffectInStrategyLanguageDecember2023.maude:
+	added
+
+==================================Maude156===========================================
+
 2023-10-02  Steven Eker  <eker@pup>
 
 	* tests/ResolvedBugs/filteredVariantUnifyJune2023.maude: added

NEWS

@@ -1,14 +1,31 @@
+Overview of Changes in alpha156 (2034-01-29)
+============================================
+* LaTeX support for more commands and features
+* big numbers, strings, qids and unparsed tokens are now broken
+across multiple lines in LaTeX to avoid an "Overfull \hbox"
+* fixed bug where bad LaTeX was generated by show mod for
+certain characters in metadata
+* added =># search type
+* fixed bug where srewrite could miss a rewrite due to a side-effect
+from a condition
+* equations with both variant and nonexec attributes produce
+an advisory and are no longer used for variant narrowing
+* in/load/sload no longer attempt to read non-regular files
+* increased line length and history size with Tecla
+* the narrow command now respects frozen positions
+
 Overview of Changes in alpha155 (2023-12-12)
 ============================================
-* fixed bug in latex output for format attribute
-* fixed missing space in latex output between format and
+* fixed bug in LaTeX output for format attribute
+* fixed missing space in LaTeX output between format and
 metadata attributes
-* fixed bad latex for dags with print color on
+* fixed bad LaTeX for dags with print color on
 * latex attribute supported
-* fixed bug where latex for structured constants didn't
+* fixed bug where LaTeX for structured constants didn't
 support the format attribute
 * fixed bug where format s and i commands didn't work at the
-start of a latex line
+start of a LaTeX line
+* fixed CVC4 bindings for latest version
 
 Overview of Changes in alpha154 (2023-11-30)
 ============================================

configure

@@ -1,6 +1,6 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.69 for Maude alpha155.
+# Generated by GNU Autoconf 2.69 for Maude alpha156.
 #
 # Report bugs to <maude-bugs@lists.cs.illinois.edu>.
 #
@@ -580,8 +580,8 @@ MAKEFLAGS=
 # Identity of this package.
 PACKAGE_NAME='Maude'
 PACKAGE_TARNAME='maude'
-PACKAGE_VERSION='alpha155'
-PACKAGE_STRING='Maude alpha155'
+PACKAGE_VERSION='alpha156'
+PACKAGE_STRING='Maude alpha156'
 PACKAGE_BUGREPORT='maude-bugs@lists.cs.illinois.edu'
 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 alpha155 to adapt to many kinds of systems.
+\`configure' configures Maude alpha156 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 alpha155:";;
+     short | recursive ) echo "Configuration of Maude alpha156:";;
    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 alpha155
+Maude configure alpha156
 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 alpha155, which was
+It was created by Maude $as_me alpha156, 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='alpha155'
+ VERSION='alpha156'
 
 
 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 alpha155, which was
+This file was extended by Maude $as_me alpha156, 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 alpha155
+Maude config.status alpha156
 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, alpha155, [maude-bugs@lists.cs.illinois.edu])
+AC_INIT(Maude, alpha156, [maude-bugs@lists.cs.illinois.edu])
 #
 #	Allow directory names that look like macros.
 #

doc/Makefile.am

@@ -23,4 +23,5 @@ EXTRA_DIST = \
 	alpha152.txt \
 	alpha153.txt \
 	alpha154.txt \
-	alpha155.txt
+	alpha155.txt \
+	alpha156.txt

doc/Makefile.in

@@ -255,7 +255,8 @@ EXTRA_DIST = \
 	alpha152.txt \
 	alpha153.txt \
 	alpha154.txt \
-	alpha155.txt
+	alpha155.txt \
+	alpha156.txt
 
 all: all-am
 

doc/alpha156.txt

@@ -0,0 +1,101 @@
+Alpha 156 release notes
+========================
+
+Bug fixes
+==========
+
+(1) A bug where certain characters in metadata resulted in bad LaTeX being
+produced by show mod. For example:
+
+fmod FOO is
+  sort Foo .
+  op b : -> Foo [metadata "`'\\^'"] .
+endfm
+
+show mod .
+
+(2) A bug where rewriting in a condition has a side effect on flags in
+a dag that causes strategic rewriting with nonexec rules to fail.
+Illustrated by this example from Paco:
+
+mod NONEXEC is
+  sorts Foo Bar .
+  ops a b : -> Foo [ctor] .
+  op <_> : Foo -> Bar [ctor] .
+  vars F G : Foo .
+  crl < F > => < G > if F => G /\ F =/= G .
+  rl [ab] : a => b [nonexec] .
+endm
+
+srew < a > using try(all) ; ab .
+
+Here the try(all) strategy on < a > attempt to use
+  crl < F > => < G > if F => G /\ F =/= G .
+and in particuar tries to rewrite the subterm a using executable rules.
+When it fails, a is marked as being unrewritable as an optimization.
+Then attemption to rewrite with the label ab, rewriting fails, even
+though the nonexec rule can be used with this strategy, because a is
+marked as being unrewritable. The fix is that flags that indicate a
+subterm is unrewritable, or should not be explored (unstackable) are ignored
+if nonexec rules are in play.
+
+New features
+=============
+
+(1) The resouces information printed on exit with
+  set show resouces on .
+is now supported in LaTeX.
+
+(2) LaTeX support for more commands:
+(a) smt-search
+(b) check
+(c) loop and loop mode bubbles
+
+(3) There is a new search arrow, =>#, which searches for states having multiple
+distinct successors. For example:
+
+mod TEST is
+  sort Foo .
+  ops a b c d e f : -> Foo .
+  rl a => b .
+  rl b => c .
+  rl c => d .
+  rl c => e .
+  rl d => e .
+  rl d => f .
+endm
+
+search a =># X:Foo .
+
+This is only supported for search, and not for smt-search or any version of
+narrowing. At the metalevel, the Qid '# is used to indicate this search type.
+Feature requested by Dwight Guth <dwight.guth@runtimeverification.com>.
+
+(4) Printing dags in graph from with
+  set print graph on .
+is now supported in LaTeX.
+
+Other changes
+==============
+
+(1) Large numbers, strings of sort String as well as strings occurring in metadata and
+print attributes, Qids and unparsed tokens in show mod and show view are now allowed
+to be broken over multiple lines in LaTeX to avoid an "Overfull \hbox".
+
+(2) Various changes to LaTeX spacing.
+
+(3) Equations having both the variant and nonexec attributes now produce an advisory,
+and are ignored for variant generation.
+
+(4) Directories and other non-regular files are no longer considered for
+reading with the directives in, load and sload. This is to avoid
+  load .
+attempting to read in the current directory as if it were a Maude file.
+Change requested by Carolyn.
+
+(5) The maximum line length when using Tecla is increased from 1024 characters
+to 100 * 1024 characters. Change requested by Paco.
+
+(6) The amount of history kept by Tecla is increased from 4 KB to 100 KB.
+
+(7) The narrow command now respects frozen positions just like the vu-narrow command.

src/ACU_Theory/ACU_Symbol.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
@@ -336,6 +336,7 @@ ACU_Symbol::stackArguments(DagNode* subject,
 			   Vector<RedexPosition>& stack,
 			   int parentIndex,
 			   bool respectFrozen,
+			   bool respectUnstackable,
 			   bool eagerContext)
 {
   if (respectFrozen && !(getFrozen().empty()))  // under AC, any frozen argument affects all
@@ -349,7 +350,7 @@ ACU_Symbol::stackArguments(DagNode* subject,
 	{
 	  DagNode* d = i.getDagNode();
 	  int m = i.getMultiplicity();
-	  if (d->isUnstackable())
+	  if (respectUnstackable && d->isUnstackable())
 	    argNr += m;
 	  else
 	    {
@@ -368,7 +369,7 @@ ACU_Symbol::stackArguments(DagNode* subject,
 	{
 	  DagNode* d = i.dagNode;
 	  int m = i.multiplicity;
-	  if (d->isUnstackable())
+	  if (respectUnstackable && d->isUnstackable())
 	    argNr += m;
 	  else
 	    {
@@ -387,6 +388,7 @@ ACU_Symbol::stackPhysicalArguments(DagNode* subject,
 				   Vector<RedexPosition>& stack,
 				   int parentIndex,
 				   bool respectFrozen,
+				   bool respectUnstackable,
 				   bool eagerContext)
 {
   if (respectFrozen && !(getFrozen().empty()))  // under AC, any frozen argument affects all
@@ -399,7 +401,7 @@ ACU_Symbol::stackPhysicalArguments(DagNode* subject,
       for (ACU_FastIter i(tree); i.valid(); i.next())
 	{
 	  DagNode* d = i.getDagNode();
-	  if (!(d->isUnstackable()))
+	  if (!(respectUnstackable && d->isUnstackable()))
 	    stack.append(RedexPosition(d, parentIndex, argNr, eager));
 	  ++argNr;
 	}
@@ -411,7 +413,7 @@ ACU_Symbol::stackPhysicalArguments(DagNode* subject,
       for (int i = 0; i < nrArgs; i++)
 	{
 	  DagNode* d = argArray[i].dagNode;
-	  if (!(d->isUnstackable()))
+	  if (!(respectUnstackable && d->isUnstackable()))
 	    stack.append(RedexPosition(d, parentIndex, i, eager));
 	}
     }

src/ACU_Theory/ACU_Symbol.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
@@ -48,11 +48,13 @@ public:
 		      Vector<RedexPosition>& stack,
 		      int parentIndex,
 		      bool respectFrozen,
+		      bool respectUnstackable,
 		      bool eagerContext);
   void stackPhysicalArguments(DagNode* subject,
 			      Vector<RedexPosition>& stack,
 			      int parentIndex,
 			      bool respectFrozen,
+			      bool respectUnstackable,
 			      bool eagerContext);
   Term* termify(DagNode* dagNode);
   bool determineGround(DagNode* dagNode);

src/ACU_Theory/ChangeLog

@@ -1,3 +1,14 @@
+2024-01-16  Steven Eker  <eker@pup>
+
+	* ACU_Symbol.cc (ACU_Symbol::stackArguments): support
+	respectUnstackable argument
+	(ACU_Symbol::stackPhysicalArguments): ditto
+
+	* ACU_Symbol.hh (class ACU_Symbol): updated decls for stackArguments()
+	and stackPhysicalArguments()
+
+===================================Maude156===========================================
+
 2023-07-24  Steven Eker  <eker@pup>
 
 	* ACU_Symbol.cc (ACU_Symbol::determineGround): added

src/AU_Theory/AU_Symbol.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
@@ -453,6 +453,7 @@ AU_Symbol::stackArguments(DagNode* subject,
 			  Vector<RedexPosition>& stack,
 			  int parentIndex,
 			  bool respectFrozen,
+			  bool respectUnstackable,
 			  bool eagerContext)
 {
   if (respectFrozen && !(getFrozen().empty()))  // under A, any frozen argument affects all
@@ -469,7 +470,7 @@ AU_Symbol::stackArguments(DagNode* subject,
 	   i.valid(); i.next(), ++j)
 	{
 	  DagNode* d = i.getDagNode();
-	  if (!(d->isUnstackable()))
+	  if (!(respectUnstackable && d->isUnstackable()))
 	    stack.append(RedexPosition(d, parentIndex, j, eager));
 	}
     }
@@ -483,7 +484,7 @@ AU_Symbol::stackArguments(DagNode* subject,
       for (int i = 0; i < nrArgs; i++)
 	{
 	  DagNode* d = args[i];
-	  if (!(d->isUnstackable()))
+	  if (!(respectUnstackable && d->isUnstackable()))
 	    stack.append(RedexPosition(d, parentIndex, i, eager));
 	}
     }