alpha161

NEWS

@@ -1,3 +1,11 @@
+Overview of Changes in alpha161 (2023-05-17)
+============================================
+* reading from the stdin steam now supports continuation lines
+* path option for vu-narrow
+* show most general states .
+* show frontier states .
+* a state may now subsume its ancestors in vu-narrow
+
 Overview of Changes in alpha160 (2023-05-02)
 ============================================
 * initial equality operator handles more cases

configure

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

doc/Makefile.am

@@ -28,4 +28,5 @@ EXTRA_DIST = \
 	alpha157.txt \
 	alpha158.txt \
 	alpha159.txt \
-	alpha160.txt
+	alpha160.txt \
+	alpha161.txt

doc/Makefile.in

@@ -260,7 +260,8 @@ EXTRA_DIST = \
 	alpha157.txt \
 	alpha158.txt \
 	alpha159.txt \
-	alpha160.txt
+	alpha160.txt \
+	alpha161.txt
 
 all: all-am
 

doc/alpha160.txt

@@ -78,7 +78,7 @@ endfm
 The is*() functions follow the C++ standard. startsWith() and endWith()
 check if the first string starts with (resp. ends with) the second
 string. The trim*() functions remove white-space characters from
-the start, end, or bothe ends of the string argument.
+the start, end, or both ends of the string argument.
 The reason for placing theses function in a new fmod it that it
 is intended to extend it in future with operations that require
 lists of strings.
@@ -154,10 +154,10 @@ result Bool: Z .=. Y
 unequal and are both nonground, we examine subterms in the flattened argument
 lists; i.e. subterms headed by something other than _+_. Equal arguments on both
 sides can be canceled. If one side fully cancels we can return false; otherwise
-if one side onlyhas fixed subterms we can check if there are enough arguments to
+if one side only has fixed subterms we can check if there are enough arguments to
 pair up with the other side or return false. Then we can check for each fixed
 subterm on the other side, there is something for it to pair with, or return
-false. Finally if we had cancelations we can return the reduced initial equality.
+false. Finally if we had cancellations we can return the reduced initial equality.
 
 red g(A) + g(B) + g(C) .=. g(A) + B + h(C) .
 reduce in FOO : g(A) + B + h(C) .=. g(A) + g(B) + g(C) .
@@ -202,7 +202,7 @@ states:
 The same four search types, =>1, =>+, =>*, =>! are supported. Unlike the
 single initial state case, variables may not be shared between the
 states and the pattern. Nor may variables be shared between states.
-Essentially each initial state generates its own tree of descendents, but
+Essentially each initial state generates its own tree of descendants, but
 states from one tree may subsume states from another tree if the fold
 option is given; in fact one initial state may subsume another. If
 a disjunction of initial states is given, the result information includes

doc/alpha161.txt

@@ -0,0 +1,227 @@
+Alpha 161 release notes
+========================
+
+Bug fix
+========
+Missing space after {delay, filter} in latex output fixed.
+
+New features
+=============
+(1) The is a new option for vu-narrow, path. When this is given, the states
+on the path to each state yielding a solution are locked against deletion (at some
+cost in memory) and each solution includes a state number that can be used with
+  show path <state number> .
+and
+  show path states <state number> .
+that previoulsy only worked with search. For example:
+
+mod BAZ is
+  sort Foo .
+  ops f g h : Foo -> Foo .
+  ops i j k : Foo Foo -> Foo .
+
+vars X Y Z W A B C D : Foo .
+  eq j(f(X), Y) = i(f(Y), X) [variant] .
+  rl g(i(X, k(Y, Z))) => f(k(Z, X)) [narrowing] .
+  rl f(k(X, X)) => h(X) [narrowing] .
+endm
+
+{path} vu-narrow {filter,delay} g(j(A, B)) =>* C .
+
+Solution 1 (state 0)
+rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)
+state: g(j(#1:Foo, #2:Foo))
+accumulated substitution:
+A --> #1:Foo
+B --> #2:Foo
+variant unifier:
+C --> g(j(@1:Foo, @2:Foo))
+#1:Foo --> @1:Foo
+#2:Foo --> @2:Foo
+
+Solution 2 (state 1)
+rewrites: 4 in 0ms cpu (0ms real) (~ rewrites/second)
+state: f(k(%2:Foo, f(%3:Foo)))
+accumulated substitution:
+A --> f(k(%1:Foo, %2:Foo))
+B --> %3:Foo
+variant unifier:
+C --> f(k(@1:Foo, f(@2:Foo)))
+%2:Foo --> @1:Foo
+%3:Foo --> @2:Foo
+
+...
+
+show path 1 .
+
+state 0, Foo: g(j(#1:Foo, #2:Foo))
+accumulated substitution:
+A --> #1:Foo
+B --> #2:Foo
+===[ rl g(i(X, k(Y, Z))) => f(k(Z, X)) [narrowing] . ]===>
+variant unifier:
+X --> f(%3:Foo)
+Y --> %1:Foo
+Z --> %2:Foo
+#1:Foo --> f(k(%1:Foo, %2:Foo))
+#2:Foo --> %3:Foo
+state 1, Foo: f(k(%2:Foo, f(%3:Foo)))
+accumulated substitution:
+A --> f(k(%1:Foo, %2:Foo))
+B --> %3:Foo
+
+show path states 1 .
+
+state 0, Foo: g(j(#1:Foo, #2:Foo))
+accumulated substitution:
+A --> #1:Foo
+B --> #2:Foo
+------>
+state 1, Foo: f(k(%2:Foo, f(%3:Foo)))
+accumulated substitution:
+A --> f(k(%1:Foo, %2:Foo))
+B --> %3:Foo
+
+Naturally path can be combined with fold:
+
+{path,fold} vu-narrow {filter,delay} g(j(A, B)) =>* C .
+
+
+(2) There is a new command that can be executed after a vu-narrow command, if
+the fold option is used.
+
+show most general states .
+
+This displays a disjunction of the most general states encoutered (so far)
+in the narrowing search.
+
+(3) There is a new command that can be executed after a vu-narrow command.
+
+show frontier states .
+
+If the vu-narow command executes to completion, this will display
+*** frontier is empty ***
+indicating that the frontier is empty. But if there is a depth bound, the disjunction
+of states at the depth bound (that have not been narrowed due to the depth bound)
+will be displayed. In the case that vu-narrow stopped early due a bound on the
+number of solutions, In the =>1, =>+, =>* cases it maybe that there is one state in
+the frontier that has been partly explored and this will be shown first, in red.
+
+There is a subtle difference in the frontier for =>1, =>+, =>* cases vs the =>! case.
+This is because a state S at maximum depth will not have been explored in the former
+cases and therefore is part of the frontier, whereas in the latter case it will
+have been checked for the existence of descendants, even though they will not
+have been generated, and in the case that S is determined not to have descendants
+it will not be part of the frontier. This illustrated by the example:
+
+mod BAZ is
+  sort Foo .
+  ops f g h : Foo -> Foo .
+  ops i j k : Foo Foo -> Foo .
+
+vars X Y Z W A B C D : Foo .
+  eq j(f(X), Y) = i(f(Y), X) [variant] .
+  rl g(i(X, k(Y, Z))) => f(k(Z, X)) [narrowing] .
+  rl f(k(X, X)) => h(X) [narrowing] .
+endm
+
+{fold} vu-narrow {filter,delay} [,3]  in BAZ : g(j(A, B)) =>* C .
+show frontier states .
+show most general states .
+
+returns a single state frontier:
+
+h(h(%1:Foo))
+
+because h(h(%1:Foo)) as at depth 3 and hence was not explored while
+
+{fold} vu-narrow {filter,delay} [,3]  in BAZ : g(j(A, B)) =>! C .
+show frontier states .
+show most general states .
+
+returns the empty frontier because h(h(%1:Foo)) was determined no to
+have descendants when it was check for being in normal form.
+
+In both cases, exploring the narrowing tree to depth 3 yields the same set
+of most general states:
+
+g(j(#1:Foo, #2:Foo)) /\
+f(k(%2:Foo, f(%3:Foo))) /\
+h(f(@1:Foo)) /\
+f(k(@2:Foo, h(@1:Foo))) /\
+h(h(%1:Foo))
+
+If folding is used, the frontier will always be a subset of the most general states.
+
+Other changes
+==============
+(1) When doing sending a getLine() message to stdin, a backslash newline combination
+is now taken to indicate the input line with be continued. The backbackslash newline is
+deleted and the continuation lines are prompted with "> ". For example:
+
+load file
+
+omod HELLO is
+  inc STD-STREAM .
+  pr NAT .
+  class MyClass | state : Nat .
+  op myObj : -> Oid .
+  op run : -> Configuration .
+
+  eq run = <> < myObj : MyClass | state : 0 > .
+  rl < myObj : MyClass | state : 0 > => < myObj : MyClass | state : 1 > getLine(stdin, myObj, "What is your name? ") .
+endom
+
+Maude> erew run .
+erewrite in HELLO : run .
+What is your name? Zaphod \
+> Beeblebrox
+rewrites: 2 in 8ms cpu (38199ms real) (250 rewrites/second)
+result Configuration: <> < myObj : MyClass | state : 1 > gotLine(myObj, stdin, "Zaphod Beeblebrox\n")
+
+Change requested by Paco.
+
+(2) With vu-narrow we used to assume that a newly generated state could not subsume
+any of own ancestors, and thus we didn't even do the check. Now we check a new state
+that hasn't been subsumed by existing most general states against all existing most
+general states to see if subsumes them. Thus a state can actually subsume (and if path is
+not used, delete) its own branch of the search tree, except for itself. This situation
+trivially arises with a narrowing rule that rewrites to a more general pattern:
+
+mod FOO is
+  sort Foo .
+  ops f g : Foo -> Foo .
+vars X Y Z : Foo .
+  rl f(g(X)) => f(X) [narrowing] .
+endm
+
+set verbose on .
+
+{fold} vu-narrow f(g(Y)) =>* Z .
+
+Solution 1
+rewrites: 0 in 4ms cpu (0ms real) (0 rewrites/second)
+state: f(g(#1:Foo))
+accumulated substitution:
+Y --> #1:Foo
+variant unifier:
+Z --> f(g(@1:Foo))
+#1:Foo --> @1:Foo
+New state f(@1:Foo) subsumed older state f(g(#1:Foo))
+
+Solution 2
+rewrites: 1 in 4ms cpu (1ms real) (250 rewrites/second)
+state: f(@1:Foo)
+accumulated substitution:
+Y --> @1:Foo
+variant unifier:
+Z --> f(%1:Foo)
+@1:Foo --> %1:Foo
+New state f(%1:Foo) subsumed by f(@1:Foo)
+Total number of states seen = 3
+Of which 2 were considered for further narrowing.
+
+No more solutions.
+rewrites: 2 in 4ms cpu (1ms real) (500 rewrites/second)
+
+I'm interested to know if this improves performance.