From bb99ad5a1e082c8f1f585d0acf36171c78af5b53 Mon Sep 17 00:00:00 2001 From: Steven Eker Date: Fri, 17 May 2024 22:30:03 -0700 Subject: [PATCH] alpha161 --- NEWS | 8 + configure | 20 +-- configure.ac | 2 +- doc/Makefile.am | 3 +- doc/Makefile.in | 3 +- doc/alpha160.txt | 8 +- doc/alpha161.txt | 227 ++++++++++++++++++++++++ src/Higher/ChangeLog | 105 +++++++++++ src/Higher/narrowingFolder.cc | 167 +++++++++++++---- src/Higher/narrowingFolder.hh | 77 +++++++- src/Higher/narrowingSequenceSearch3.cc | 10 +- src/Higher/narrowingSequenceSearch3.hh | 98 +++++++++- src/IO_Stuff/IO_Manager.cc | 2 +- src/Mixfix/ChangeLog | 96 ++++++++++ src/Mixfix/commands.yy | 9 +- src/Mixfix/execute.cc | 8 +- src/Mixfix/interpreter.hh | 3 + src/Mixfix/latexCommand.cc | 31 +++- src/Mixfix/latexResult.cc | 127 ++++++++++++- src/Mixfix/lexer.ll | 6 +- src/Mixfix/maudeLatexBuffer.cc | 43 +++++ src/Mixfix/maudeLatexBuffer.hh | 17 +- src/Mixfix/narrowing.cc | 185 +++++++++++++++++-- src/Mixfix/search.cc | 35 +++- src/Mixfix/top.yy | 4 +- src/Mixfix/userLevelRewritingContext.cc | 32 ++++ src/Mixfix/userLevelRewritingContext.hh | 5 + src/ObjectSystem/ChangeLog | 7 + src/ObjectSystem/processStuff.cc | 4 +- src/ObjectSystem/streamManagerSymbol.cc | 23 ++- 30 files changed, 1262 insertions(+), 103 deletions(-) create mode 100644 doc/alpha161.txt diff --git a/NEWS b/NEWS index 49cd5da1..95ade341 100755 --- a/NEWS +++ b/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 diff --git a/configure b/configure index 3e75c94e..f4945257 100755 --- a/configure +++ b/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 . # @@ -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='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 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\\" diff --git a/configure.ac b/configure.ac index 554ea3be..51558975 100755 --- a/configure.ac +++ b/configure.ac @@ -3,7 +3,7 @@ # # Initialize autoconf stuff. # -AC_INIT(Maude, alpha160, [maude-bugs@lists.cs.illinois.edu]) +AC_INIT(Maude, alpha161, [maude-bugs@lists.cs.illinois.edu]) # # Allow directory names that look like macros. # diff --git a/doc/Makefile.am b/doc/Makefile.am index 0cd4d4a6..3fba03ad 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -28,4 +28,5 @@ EXTRA_DIST = \ alpha157.txt \ alpha158.txt \ alpha159.txt \ - alpha160.txt + alpha160.txt \ + alpha161.txt diff --git a/doc/Makefile.in b/doc/Makefile.in index a0b7f918..63e73350 100644 --- a/doc/Makefile.in +++ b/doc/Makefile.in @@ -260,7 +260,8 @@ EXTRA_DIST = \ alpha157.txt \ alpha158.txt \ alpha159.txt \ - alpha160.txt + alpha160.txt \ + alpha161.txt all: all-am diff --git a/doc/alpha160.txt b/doc/alpha160.txt index d50f6c5c..e7f4ab47 100644 --- a/doc/alpha160.txt +++ b/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 diff --git a/doc/alpha161.txt b/doc/alpha161.txt new file mode 100644 index 00000000..be976dde --- /dev/null +++ b/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 . +and + show path states . +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. diff --git a/src/Higher/ChangeLog b/src/Higher/ChangeLog index e10ec3d0..210dde40 100755 --- a/src/Higher/ChangeLog +++ b/src/Higher/ChangeLog @@ -1,3 +1,108 @@ +2024-05-17 Steven Eker + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): + getUnexpandedState() becomes getUnexpandedStates() + (NarrowingSequenceSearch3::getUnexpandedState): becomes + getUnexpandedStates(); rewritten + + * narrowingFolder.hh (class NarrowingFolder): added decl for + getReturnedButUnexploredStates() + + * narrowingFolder.cc (NarrowingFolder::getReturnedButUnexploredStates): + added + + * narrowingFolder.hh (NarrowingFolder::setUnexplored): added + +2024-05-16 Steven Eker + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::markReachableNodes): protect goal + (NarrowingSequenceSearch3::findNextUnifier): use goal directly + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): goal + becomes a DagNode* rather than a DagRoot now that we have our own + markReachableNodes() to protect it + +2024-05-15 Steven Eker + + * narrowingFolder.hh (class NarrowingFolder): added decl for + doSubsumption() + + * narrowingFolder.cc (NarrowingFolder::doSubsumption): added + +2024-05-09 Steven Eker + + * narrowingFolder.hh (class NarrowingFolder): added decl for dump + + * narrowingFolder.cc (NarrowingFolder::dump): added + + * narrowingSequenceSearch3.hh (NarrowingSequenceSearch3::unexpandedState): + added + + * narrowingFolder.hh (class NarrowingFolder): added data member + returnedButUnexplored to struct RetainedState + +2024-05-08 Steven Eker + + * narrowingSequenceSearch3.hh + (NarrowingSequenceSearch3::getUnvisitedStates): added + + * narrowingFolder.hh (class NarrowingFolder): added decl for + getUnreturnedStates() + + * narrowingFolder.cc (NarrowingFolder::getUnreturnedStates): added + + * narrowingSequenceSearch3.hh + (NarrowingSequenceSearch3::getMostGeneralStates): added + + * narrowingFolder.hh (class NarrowingFolder): added decl for + getMostGeneralStates() + + * narrowingFolder.cc (NarrowingFolder::getMostGeneralStates): added + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): deleted + INVARIANT from enum Flags + +2024-05-07 Steven Eker + + * narrowingFolder.hh (NarrowingFolder::RetainedState::markedSubsumed): don't + assume stateTerm is non-null because we might support variant folding at + some point + +2024-05-06 Steven Eker + + * narrowingFolder.cc (NarrowingFolder::insertState): use markedSubsumed() + for states that got subsumed but can't be deleted because they are locked + for show path + + * narrowingFolder.hh (NarrowingFolder::RetainedState::markedSubsumed): added + + * narrowingFolder.cc (NarrowingFolder::getNextSurvivingState): handled + subsumed states; this can arise if a state produces, a solution and has + its path locked by the caller, and is subsequently subsumed but can't be + deleted because it is locked as it may be needed for a show path + +2024-05-03 Steven Eker + + * narrowingSequenceSearch3.cc (NarrowingSequenceSearch3::findNextUnifier): + use lockPathToState() + + * narrowingFolder.hh (class NarrowingFolder): lockPathToCurrentState()-> + lockPathToState() + + * narrowingFolder.cc (NarrowingFolder::lockPathToCurrentState): becomes + lockPathToState() + + * narrowingSequenceSearch3.hh (NarrowingSequenceSearch3::getStateParent): + added + + * narrowingFolder.hh (NarrowingFolder::exists): made const + (NarrowingFolder::getParent): added + + * narrowingSequenceSearch3.hh (NarrowingSequenceSearch3::locked): added + + * narrowingFolder.hh (NarrowingFolder::locked): added + 2024-05-02 Steven Eker * narrowingSequenceSearch3.cc: diff --git a/src/Higher/narrowingFolder.cc b/src/Higher/narrowingFolder.cc index 7735f748..4cbe45a0 100644 --- a/src/Higher/narrowingFolder.cc +++ b/src/Higher/narrowingFolder.cc @@ -90,6 +90,98 @@ NarrowingFolder::markReachableNodes() } } +void +NarrowingFolder::dump(ostream& s) +{ + for (auto& i : mostGeneralSoFar) + { + s << i.first << " : " << i.second->state << + " parent=" << i.second->parentIndex << + " depth=" << i.second->depth << + " locked=" << i.second->locked << + " subsumed=" << i.second->subsumed << endl; + } +} + +Vector +NarrowingFolder::getReturnedButUnexploredStates() const +{ + // + // We return all states that were marked as returnedButUnexplored and haven't been deleted or marked as subsumed. + // + Vector unexploredStates; + for (auto p : mostGeneralSoFar) + { + if (p.second->returnedButUnexplored && !(p.second->subsumed)) + unexploredStates.push_back(p.second->state); + } + return unexploredStates; +} + +Vector +NarrowingFolder::getUnreturnedStates() const +{ + Vector unreturnedStates; + // + // Return all states that have neither been returned as the next state, nor subsumed. + // Since they may have been considered for unification with the goal, they could be locked and subsumed. + // + for (RetainedStateMap::const_iterator i = mostGeneralSoFar.upper_bound(currentStateIndex); i != mostGeneralSoFar.end(); ++i) + { + //cerr << "unvisited state " << i->first << " : " << i->second->state << endl; + if (!(i->second->subsumed)) + unreturnedStates.push_back(i->second->state); + } + return unreturnedStates; +} + +Vector +NarrowingFolder::getMostGeneralStates() const +{ + Assert(fold, "not folding"); + Vector mostGeneralStates; + // + // If we're folding, all states should be most general unless they've been locked and subsumed. + // + for (auto i : mostGeneralSoFar) + { + if (!(i.second->subsumed)) + mostGeneralStates.push_back(i.second->state); + } + return mostGeneralStates; +} + +void +NarrowingFolder::doSubsumption(RetainedStateMap::iterator& subsumedStateIter, + StateSet& existingStatesSubsumed, + int subsumersParent, + const StateSet& subsumersAncestors) +{ + // + // Record this state as subsumed in current subsumption analysis. + // + int victimIndex = subsumedStateIter->first; + RetainedState* victimState = subsumedStateIter->second; + existingStatesSubsumed.insert(victimIndex); + // + // If the victim is locked, it is needed for printing the path to a success. + // Otherwise if it is the subsumer's parent, its needed to compute the subsumer's accumulated subsitution. + // Otherwise if we're keeping history and it is in the subsumer's ancestors, its potentially needed for a path. + // + if (victimState->locked || + victimIndex == subsumersParent || + (keepHistory && !(subsumersAncestors.find(victimIndex) == subsumersAncestors.end()))) + victimState->markedSubsumed(); + else + { + // + // No reason to keep this subsumed state. + // + delete victimState; + mostGeneralSoFar.erase(subsumedStateIter); + } +} + bool NarrowingFolder::insertState(int index, DagNode* state, int parentIndex) { @@ -145,7 +237,7 @@ NarrowingFolder::insertState(int index, DagNode* state, int parentIndex) { RetainedStateMap::iterator next = i; ++next; - if (!i->second->subsumed && ancestors.find(i->first) == ancestors.end()) // can't mess with ancestors of new state + if (!i->second->subsumed) // only look at states that haven't been subsumed { RetainedState* potentialVictim = i->second; if (existingStatesSubsumed.find(potentialVictim->parentIndex) != existingStatesSubsumed.end()) @@ -158,13 +250,7 @@ NarrowingFolder::insertState(int index, DagNode* state, int parentIndex) " evicted descendent of an older state " << i->second->state << " by subsuming an ancestor."); existingStatesSubsumed.insert(i->first); - if (potentialVictim->locked) - potentialVictim->subsumed = true; // can't delete this state because we might need it for a path - else - { - delete potentialVictim; - mostGeneralSoFar.erase(i); - } + doSubsumption(i, existingStatesSubsumed, parentIndex, ancestors); } else if (newState->subsumes(potentialVictim->state)) { @@ -174,13 +260,7 @@ NarrowingFolder::insertState(int index, DagNode* state, int parentIndex) DebugAdvisory("new state evicted an older state " << i->first); Verbose("New state " << state << " subsumed older state " << i->second->state); existingStatesSubsumed.insert(i->first); - if (potentialVictim->locked) - potentialVictim->subsumed = true; // can't delete this state because we might need it for a path - else - { - delete potentialVictim; - mostGeneralSoFar.erase(i); - } + doSubsumption(i, existingStatesSubsumed, parentIndex, ancestors); } } i = next; @@ -242,18 +322,32 @@ NarrowingFolder::getNextSurvivingState(DagNode*& nextState, // // Find the next state if there is one. // - RetainedStateMap::const_iterator nextStateIterator = mostGeneralSoFar.upper_bound(currentStateIndex); - if (nextStateIterator == mostGeneralSoFar.end()) - return NONE; - Assert(!nextStateIterator->second->locked, "unvisited state should not be locked"); - Assert(!nextStateIterator->second->subsumed, "unvisited state that is subsumed should have been deleted"); - - currentStateIndex = nextStateIterator->first; - nextState = nextStateIterator->second->state; - nextStateAccumulatedSubstitution = nextStateIterator->second->accumulatedSubstitution; - nextStateVariableFamily = nextStateIterator->second->variableFamily; - nextStateDepth = nextStateIterator->second->depth; - return currentStateIndex; + for (;;) + { + // + // Find next state. + // + RetainedStateMap::const_iterator nextStateIterator = mostGeneralSoFar.upper_bound(currentStateIndex); + if (nextStateIterator == mostGeneralSoFar.end()) + break; + currentStateIndex = nextStateIterator->first; + // + // The tricky thing is if it produced a solution, we may have locked it, and if so it could have + // subsequently been subsumed without being deleted, in which case we must skip over it. + // Because such a state must be locked, there's no point calling cleanGraph(). + // + if (!nextStateIterator->second->subsumed) + { + nextState = nextStateIterator->second->state; + nextStateAccumulatedSubstitution = nextStateIterator->second->accumulatedSubstitution; + nextStateVariableFamily = nextStateIterator->second->variableFamily; + nextStateDepth = nextStateIterator->second->depth; + //cerr << "****** returning " << currentStateIndex << endl; + return currentStateIndex; + } + Assert(nextStateIterator->second->locked, "unvisited state " << nextStateIterator->first << " subsumed but not locked"); + } + return NONE; } void @@ -268,12 +362,20 @@ NarrowingFolder::cleanGraph() if (currentStateIndex == NONE) return; // no current state to consider for deletion - RetainedStateMap::iterator stateIterator = mostGeneralSoFar.find(currentStateIndex); + auto stateIterator = mostGeneralSoFar.find(currentStateIndex); + if (stateIterator->second->returnedButUnexplored) + { + // + // The caller set a flag to say they didn't explore the state we just returned + // so it remains in the frontier and we can't delete it except by subsumption. + // + return; + } if (!keepHistory) { // // Since we are not keeping history and not folding we have no further need of a fully - // explored state. + // explored state. We cannot lock states if we are not keeping history. // Assert(!stateIterator->second->locked, "shouldn't have locked states if not keeping history"); delete stateIterator->second; @@ -307,20 +409,23 @@ NarrowingFolder::cleanGraph() } void -NarrowingFolder::lockPathToCurrentState() +NarrowingFolder::lockPathToState(int index) { Assert(keepHistory, "can't lock path if not keeping history"); // // We lock all the states on the current path back to the root state, so that they are never deleted and // are thus available for showing the complete path to this state at any point before our object is deleted. // - RetainedStateMap::iterator stateIterator = mostGeneralSoFar.find(currentStateIndex); + RetainedStateMap::iterator stateIterator = mostGeneralSoFar.find(index); + //cerr << "considering " << index << endl; while(!stateIterator->second->locked) { + //cerr << "locking" << endl; stateIterator->second->locked = true; int parentIndex = stateIterator->second->parentIndex; if (parentIndex == NONE) break; + //cerr << "considering " << parentIndex << endl; stateIterator = mostGeneralSoFar.find(parentIndex); } } diff --git a/src/Higher/narrowingFolder.hh b/src/Higher/narrowingFolder.hh index 7883c78e..bfd9e9b9 100644 --- a/src/Higher/narrowingFolder.hh +++ b/src/Higher/narrowingFolder.hh @@ -36,6 +36,8 @@ #define _narrowingFolder_hh_ #include #include +#include "term.hh" +#include "lhsAutomaton.hh" #include "simpleRootContainer.hh" #include "narrowingVariableInfo.hh" @@ -84,11 +86,22 @@ public: // // Ensures all the states from the interesting state back to the root are never deleted. // - void lockPathToCurrentState(); + void lockPathToState(int index); // - // Check if a state we previously entered still exists. + // If we don't explore a returned state, we can call this function to flag the last returned state, + // so it stays part of the frontier unless subsumed - though if we've stopped exploring states we + // don't expect a new state that could subsumed it to be entered. We can't use the locked flag + // because we might not be keeping history. // - bool exists(int index); + void setUnexplored(); + + bool exists(int index) const; + bool locked(int index) const; + int getParent(int index) const; + Vector getMostGeneralStates() const; + Vector getUnreturnedStates() const; + Vector getReturnedButUnexploredStates() const; + void dump(ostream& s); private: struct RetainedState @@ -96,6 +109,7 @@ private: RetainedState(DagNode* state, int parentIndex, int rootIndex, int depth, bool fold); ~RetainedState(); bool subsumes(DagNode* state) const; + void markedSubsumed(); DagNode* const state; const int parentIndex; // index of parent state @@ -128,6 +142,14 @@ private: // bool locked = false; bool subsumed = false; + // + // When we return a surviving state, we expect that the caller will explore it + // and insert all of its next states. But the caller may instead set this flag to + // record the state was not explored and remains part of the frontier. + // We can still remove this state by subsumption but we can't remove it just because + // it has no descendants since they might exist but weren't generated. + // + bool returnedButUnexplored = false; }; typedef map RetainedStateMap; @@ -135,6 +157,11 @@ private: void markReachableNodes(); void cleanGraph(); + void doSubsumption(RetainedStateMap::iterator& subsumedStateIter, + StateSet& existingStatesSubsumed, + int subsumersParent, + const StateSet& subsumersAncestors); + const bool fold; // we do folding to prune less general states const bool keepHistory; // we keep the history of how we arrived at each state @@ -215,9 +242,49 @@ NarrowingFolder::getHistory(int index, } inline bool -NarrowingFolder::exists(int index) +NarrowingFolder::exists(int index) const +{ + return mostGeneralSoFar.find(index) != mostGeneralSoFar.end(); +} + +inline bool +NarrowingFolder::locked(int index) const +{ + auto i = mostGeneralSoFar.find(index); + return i == mostGeneralSoFar.end() ? false : i->second->locked; +} + +inline int +NarrowingFolder::getParent(int index) const +{ + auto i = mostGeneralSoFar.find(index); + Assert(i != mostGeneralSoFar.end(), "couldn't find state with index " << index); + return i->second->parentIndex; +} + +inline void +NarrowingFolder::RetainedState::markedSubsumed() +{ + // + // Normally we delete a subsumed state, but if it is locked because it is on a path + // that produced a solution, we minimize it and mark it instead. + // + delete matchingAutomaton; + matchingAutomaton = nullptr; + if (stateTerm) + { + stateTerm->deepSelfDestruct(); + stateTerm = nullptr; + } + subsumed = true; +} + +inline void +NarrowingFolder::setUnexplored() { - return mostGeneralSoFar.find(index)!= mostGeneralSoFar.end(); + auto i = mostGeneralSoFar.find(currentStateIndex); + Assert(i != mostGeneralSoFar.end(), "couldn't find state with index " << currentStateIndex); + i->second->returnedButUnexplored = true; } #endif diff --git a/src/Higher/narrowingSequenceSearch3.cc b/src/Higher/narrowingSequenceSearch3.cc index c04f304c..9d9234f5 100644 --- a/src/Higher/narrowingSequenceSearch3.cc +++ b/src/Higher/narrowingSequenceSearch3.cc @@ -246,7 +246,7 @@ NarrowingSequenceSearch3::markReachableNodes() // // Protect start states in termDisjuction mode // - //goal->mark; // maybe use this rather than DagRoot + goal->mark(); for (InitialState& i : initialStates) i.state->mark(); if (protectedSubstitution) @@ -279,7 +279,7 @@ NarrowingSequenceSearch3::findNextUnifier() // becomes subsumed (if we're folding) or after all of its next states have been // generated. // - stateCollection.lockPathToCurrentState(); + stateCollection.lockPathToState(nextInterestingState); } return true; } @@ -297,7 +297,7 @@ NarrowingSequenceSearch3::findNextUnifier() Substitution* accumulatedSubstitution; stateCollection.getState(nextInterestingState, stateDag, variableFamily, accumulatedSubstitution); - DagNode* goalDag = goal.getNode(); // no change under instantiation + DagNode* goalDag = goal; // no change under instantiation if (!termDisjunction) { // @@ -397,8 +397,10 @@ NarrowingSequenceSearch3::findNextInterestingState() // // The new state will be at maxDepth + 1 so need not be considered. It's // enough to know that the parent state has a successor and thus isn't - // in normal form. + // in normal form. But we need to set a flag in stateCollection to say that + // we didn't explore the state just returned. // + stateCollection.setUnexplored(); delete stateBeingExpanded; stateBeingExpanded = nullptr; break; diff --git a/src/Higher/narrowingSequenceSearch3.hh b/src/Higher/narrowingSequenceSearch3.hh index d08e3ee6..d635e5dc 100644 --- a/src/Higher/narrowingSequenceSearch3.hh +++ b/src/Higher/narrowingSequenceSearch3.hh @@ -61,10 +61,6 @@ public: // user can ask for the path to any state that yielded a unifier (to be implemented). // KEEP_PATHS = 0x80000, - // - // This flag is just maintained as state information for users - // - INVARIANT = 0x100000, }; // // We take responsibility for protecting startStates and goal and deleting initial and freshVariableGenerator. @@ -117,6 +113,32 @@ public: int getNrInitialStates() const; int getVariantFlags() const; bool problemOK() const; + bool locked(int index) const; + int getStateParent(int index) const; + // + // Most general states only make sense if we're folding and they are the set of states that + // have not been subsumed. + // + Vector getMostGeneralStates() const; + // + // The set of states that have not been visited for expansion. This is the frontier, possibly + // minus one state. + // + Vector getUnvisitedStates() const; + // + // In the =>1, =>+, =>* cases: + // There might be a state that was visited but not (fully) expanded. This could be because it + // is at max depth or because we haven't finished expanding it. The should also be part of + // the frontier if it exists. If it doesn't exist, we expect the frontier to be empty, because + // as soon as we exhaust the expansion of the state, we look for another state to expand. + // stateBeingExpanded can only be NONE if there are no states in the frontier. + // + // In the =>! case: + // We visit states, but might not expand them if they are max depth. In this case we can have + // more than one unexpanded state, but none of them will be partially expanded since they can + // only be considered for unification with the goal if they have no descendants. + // + Vector getUnexpandedStates(bool& partiallyExpanded); private: // @@ -136,7 +158,7 @@ private: // Initial stuff. // RewritingContext* initial; - DagRoot goal; + DagNode* goal; int nrInitialStatesToTry; const int maxDepth; const bool normalFormNeeded; @@ -247,6 +269,60 @@ NarrowingSequenceSearch3::getHistory(int index, parentIndex); } +inline Vector +NarrowingSequenceSearch3::getMostGeneralStates() const +{ + return stateCollection.getMostGeneralStates(); +} + +inline Vector +NarrowingSequenceSearch3::getUnvisitedStates() const +{ + return stateCollection.getUnreturnedStates(); +} + +inline Vector +NarrowingSequenceSearch3::getUnexpandedStates(bool& partiallyExpanded) +{ + if (normalFormNeeded) + { + // + // If we have a stateBeingExpanded, we know it has no descendants, otherwise we would have + // gone on to the next state. If we don't have a stateBeingExpanded we may still have + // states that had descendants but we didn't expand them out to avoid exceeding a depth bound. + // + partiallyExpanded = false; + return stateCollection.getReturnedButUnexploredStates(); + } + // + // If we don't have state being expanded for other search types then we have no visited but unexpanded states. + // + if (stateBeingExpandedIndex == NONE) + { + partiallyExpanded = false; + return Vector(); + } + // + // If we made the NarrowingSearchState to expand it, it must be partly expanded. + // + partiallyExpanded = (stateBeingExpanded != nullptr); + // + // Because we haven't asked for another surviving state, stateBeingExpandedIndex shouldn't have been + // garbage collected by being considered fully expanded; furthermore the descendents of + // of a state are not allowed to subsume it, so even if we have partly expanded it, it + // should still exist in stateCollection. + // + Assert(stateCollection.exists(stateBeingExpandedIndex), "state " << stateBeingExpandedIndex << " doesn't exist"); + // + // Not very efficient but it is just done once to see the frontier. + // + Vector singleton(1); + int variableFamily; + Substitution* accumulatedSubstitution; + stateCollection.getState(stateBeingExpandedIndex, singleton[0], variableFamily, accumulatedSubstitution); + return singleton; +} + inline int NarrowingSequenceSearch3::getUnifierVariableFamily() const { @@ -280,4 +356,16 @@ NarrowingSequenceSearch3::getVariantFlags() const return variantFlags; } +inline bool +NarrowingSequenceSearch3::locked(int index) const +{ + return stateCollection.locked(index); +} + +inline int +NarrowingSequenceSearch3::getStateParent(int index) const +{ + return stateCollection.getParent(index); +} + #endif diff --git a/src/IO_Stuff/IO_Manager.cc b/src/IO_Stuff/IO_Manager.cc index 4003aee6..ced5f2d9 100644 --- a/src/IO_Stuff/IO_Manager.cc +++ b/src/IO_Stuff/IO_Manager.cc @@ -304,7 +304,7 @@ Rope IO_Manager::getLineFromStdin(const Rope& prompt) { // - // In case we have a child process that is accessing stding. + // In case we have a child process that is accessing stdin. // waitUntilSafeToAccessStdin(); // diff --git a/src/Mixfix/ChangeLog b/src/Mixfix/ChangeLog index 3b85cac7..9aec7048 100644 --- a/src/Mixfix/ChangeLog +++ b/src/Mixfix/ChangeLog @@ -1,3 +1,99 @@ +2024-05-17 Steven Eker + + * maudeLatexBuffer.hh (class MaudeLatexBuffer): added decl for + generateStateSet() + + * latexResult.cc (MaudeLatexBuffer::generateStateSet): added + + * narrowing.cc (Interpreter::showFrontierStates): rewritten to + use getUnexpandedStates() + +2024-05-16 Steven Eker + + * latexCommand.cc (MaudeLatexBuffer::generateSearch): fixed + missing space after filter/delay + + * latexResult.cc (MaudeLatexBuffer::generateNarrowingSearchPath): + use generateCompoundSubstitution() + + * maudeLatexBuffer.hh (class MaudeLatexBuffer): adde decl for + generateCompoundSubstitution() + + * maudeLatexBuffer.cc + (MaudeLatexBuffer::generateCompoundSubstitution): added + + * maudeLatexBuffer.hh (class MaudeLatexBuffer): added decl for + generateNarrowingSearchPath() + + * narrowing.cc: use generateNarrowingSearchPath() + + * latexResult.cc (MaudeLatexBuffer::generateNarrowingSearchPath): + added + + * latexCommand.cc (MaudeLatexBuffer::generateSearch): echo vfold, + path + + * search.cc (Interpreter::search): echo vfold and path flags + +2024-05-09 Steven Eker + + * narrowing.cc (Interpreter::showFrontierStates): use + getUnexpandedState() + (Interpreter::showFrontierStates): print a message for empty + frontier + (Interpreter::showFrontierStates): handle the case where we + have no visited but unexpanded state but still have unvisited states + +2024-05-08 Steven Eker + + * interpreter.hh (class Interpreter): added decls for + showFrontierStates(), showMostGeneralStates(); made + showNarrowingSearchPath() private + + * commands.yy (command): added syntax for show frontier states + and show most general states + + * narrowing.cc (Interpreter::showFrontierStates) + (Interpreter::showMostGeneralStates): added stubs + + * commands.yy (option): deleted KW_INVARIANT + + * top.yy: deleted KW_INVARIANT; added KW_FRONTIER, KW_MOST, + KW_GENERAL + + * lexer.ll: deleted KW_INVARIANT; added KW_FRONTIER, KW_MOST, + KW_GENERAL + +2024-05-07 Steven Eker + + * lexer.ll: return , in INITIAL for multiple vu-narrow options + +2024-05-06 Steven Eker + + * narrowing.cc (Interpreter::showNarrowingSearchPath): use + UserLevelRewritingContext::printCompoundSubstitution() to print the + variant unfier used for a narrowing step + + * userLevelRewritingContext.hh (class UserLevelRewritingContext): added + decl for printCompoundSubstitution() + + * userLevelRewritingContext.cc + (UserLevelRewritingContext::printCompoundSubstitution): added + +2024-05-03 Steven Eker + + * narrowing.cc (Interpreter::showNarrowingSearchPath): moved here + + * execute.cc (Interpreter::clearContinueInfo): use nullptr + + * narrowing.cc (Interpreter::doVuNarrowing): delete state and unprotect + module on abort; always save state and module for later inspection + + * search.cc (Interpreter::showNarrowingSearchPath): added + (Interpreter::doSearching): delete state and unprotect module on abort + +===================================Maude161=========================================== + 2024-05-02 Steven Eker * search.cc (Interpreter::search): delete terms and condition fragments diff --git a/src/Mixfix/commands.yy b/src/Mixfix/commands.yy index 69955529..460c368f 100644 --- a/src/Mixfix/commands.yy +++ b/src/Mixfix/commands.yy @@ -447,6 +447,14 @@ command : KW_SELECT { lexBubble(END_COMMAND, 1); } if (interpreter.setCurrentModule(lexerBubble)) interpreter.showProfile(); } + | KW_SHOW KW_FRONTIER KW_STATE '.' + { + interpreter.showFrontierStates(); + } + | KW_SHOW KW_MOST KW_GENERAL KW_STATE '.' + { + interpreter.showMostGeneralStates(); + } /* * Commands to set interpreter state variables. */ @@ -691,7 +699,6 @@ optionsList : option { $$ = $1; } option : KW_FOLD { $$ = NarrowingSequenceSearch3::FOLD; } | KW_VFOLD { $$ = NarrowingSequenceSearch3::VFOLD; } | KW_PATH { $$ = NarrowingSequenceSearch3::KEEP_PATHS; } - | KW_INVARIANT { $$ = NarrowingSequenceSearch3::INVARIANT; } ; importMode : KW_PROTECT { $$ = ImportModule::PROTECTING; } diff --git a/src/Mixfix/execute.cc b/src/Mixfix/execute.cc index 9211d35b..a26301e9 100644 --- a/src/Mixfix/execute.cc +++ b/src/Mixfix/execute.cc @@ -31,12 +31,12 @@ void Interpreter::clearContinueInfo() { delete savedState; - savedState = 0; - continueFunc = 0; - if (savedModule != 0) + savedState = nullptr; + continueFunc = nullptr; + if (savedModule != nullptr) { (void) savedModule->unprotect(); - savedModule = 0; + savedModule = nullptr; } } diff --git a/src/Mixfix/interpreter.hh b/src/Mixfix/interpreter.hh index 8fab47c1..397bcf05 100644 --- a/src/Mixfix/interpreter.hh +++ b/src/Mixfix/interpreter.hh @@ -195,6 +195,8 @@ public: void showSearchPath(int stateNr, bool showRule); void showSearchPathLabels(int stateNr); void showSearchGraph(); + void showFrontierStates(); + void showMostGeneralStates(); void loop(const Vector& subject); void contLoop(const Vector& input); @@ -338,6 +340,7 @@ private: Term* target, const Vector& condition, MixfixModule* module); + void showNarrowingSearchPath(int stateNr, bool showRule, NarrowingSequenceSearch3* savedNarrowingSequence) const; ofstream* xmlLog; MaudemlBuffer* xmlBuffer; diff --git a/src/Mixfix/latexCommand.cc b/src/Mixfix/latexCommand.cc index 9a81d596..63dc317a 100644 --- a/src/Mixfix/latexCommand.cc +++ b/src/Mixfix/latexCommand.cc @@ -364,6 +364,19 @@ MaudeLatexBuffer::generateSearch(bool showCommand, startComment(); if (debug) output << "debug "; + if (variantFlags & (NarrowingSequenceSearch3::FOLD | NarrowingSequenceSearch3::VFOLD | NarrowingSequenceSearch3::KEEP_PATHS)) + { + const char* sep = ", "; + if (variantFlags & NarrowingSequenceSearch3::FOLD) + output << "{fold"; + else if (variantFlags & NarrowingSequenceSearch3::VFOLD) + output << "{vfold"; + else + sep = "{"; + if (variantFlags & NarrowingSequenceSearch3::KEEP_PATHS) + output << sep << "path"; + output << "} "; + } if (variantFlags & NarrowingSequenceSearch3::FOLD) output << "{fold} "; output << searchKindName[searchKind] << ' '; @@ -406,8 +419,20 @@ MaudeLatexBuffer::generateSearch(bool showCommand, output << "$"; if (debug) output << "\\maudeKeyword{debug}\\maudeSpace"; - if (variantFlags & NarrowingSequenceSearch3::FOLD) - output << "\\maudeLeftBrace\\maudeKeyword{fold}\\maudeRightBrace\\maudeSpace"; + if (variantFlags & (NarrowingSequenceSearch3::FOLD | NarrowingSequenceSearch3::VFOLD | NarrowingSequenceSearch3::KEEP_PATHS)) + { + const char* sep = "\\maudePunctuation{,}\\maudeSpace"; + if (variantFlags & NarrowingSequenceSearch3::FOLD) + output << "\\maudeLeftBrace\\maudeKeyword{fold}"; + else if (variantFlags & NarrowingSequenceSearch3::VFOLD) + output << "\\maudeLeftBrace\\maudeKeyword{vfold}"; + else + sep = "\\maudeLeftBrace"; + if (variantFlags & NarrowingSequenceSearch3::KEEP_PATHS) + output << sep << "\\maudeKeyword{path}"; + output << "\\maudeRightBrace\\maudeSpace"; + } + output << "\\maudeKeyword{" << searchKindName[searchKind] << "}\\maudeSpace"; if (variantFlags & (VariantSearch::IRREDUNDANT_MODE | VariantUnificationProblem::FILTER_VARIANT_UNIFIERS)) @@ -421,7 +446,7 @@ MaudeLatexBuffer::generateSearch(bool showCommand, } if (variantFlags & VariantUnificationProblem::FILTER_VARIANT_UNIFIERS) output << sep << "\\maudeKeyword{filter}"; - output << "\\maudeRightBrace"; + output << "\\maudeRightBrace\\maudeSpace"; } generateModifiers(module, limit, depth); { diff --git a/src/Mixfix/latexResult.cc b/src/Mixfix/latexResult.cc index a434ceb3..8615a7c6 100644 --- a/src/Mixfix/latexResult.cc +++ b/src/Mixfix/latexResult.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 2023-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 @@ -297,6 +297,131 @@ MaudeLatexBuffer::generateSearchPath(const RewriteSequenceSearch* graph, output <<"\\end{maudeResultParagraph}\n%\n% End of show path\n%\n"; } +void +MaudeLatexBuffer::generateStateSet(bool showCommand, + const char* command, + const Vector& firstPart, + bool highlight, + const Vector& secondPart, + const char* emptyMessage) +{ + // + // Print comment. + // + startComment(); + output << command; + endComment(); + // + // Print latex version of command. + // + output << "\\begin{maudeResultParagraph}\n"; + if (showCommand) + output << "\\par\\maudeKeyword{" << command << "}\\maudeEndCommand\\newline\n"; + // + // Print state set. + // + const char* sep = ""; + for (DagNode* d : firstPart) + { + output << sep << "\\par$"; + if (highlight) + output << "\\color{red}"; + MixfixModule::latexPrintDagNode(output, d); + if (highlight) + output << "\\color{black}"; + sep = "\\maudeSpace\\maudeDisjunction$\n"; + } + for (DagNode* d : secondPart) + { + output << sep << "\\par$"; + MixfixModule::latexPrintDagNode(output, d); + sep = "\\maudeSpace\\maudeDisjunction$\n"; + } + if (*sep == '\0') + { + if (emptyMessage != nullptr) + output << "\\par" << emptyMessage; + } + else + output << "$"; + output << "\n\\end{maudeResultParagraph}\n%\n% End of " << command << "\n%\n"; +} + +void +MaudeLatexBuffer::generateNarrowingSearchPath(const NarrowingSequenceSearch3* state, + const Vector& steps, + int stateNr, + bool showCommand, + bool showRule) +{ + const char* command = (showRule ? "show path" : "show path state" ); + // + // Print comment. + // + startComment(); + output << command << " " << stateNr; + endComment(); + // + // Print latex version of command. + // + output << "\\begin{maudeResultParagraph}\n"; + if (showCommand) + output << "\\par\\maudeKeyword{" << command << "}\\maudeSpace\\maudeNumber{" << stateNr << "}\\maudeEndCommand\\newline\n"; + // + // Print latex version of path. + // + for (Index i = steps.size() - 1; i >= 0; --i) + { + int index = steps[i]; + DagNode* root; + DagNode* position; + Rule* rule; + const Substitution* unifier; + const NarrowingVariableInfo* unifierVariableInfo; + int variableFamily; + DagNode* newDag; + const Substitution* accumulatedSubstitution; + int parentIndex; + state->getHistory(index, + root, + position, + rule, + unifier, + unifierVariableInfo, + variableFamily, + newDag, + accumulatedSubstitution, + parentIndex); + if (parentIndex != NONE) + { + if (showRule) + { + output << "\\par$\\maudePathLeft"; + safeCastNonNull(rule->getModule())->latexPrintRule(output, nullptr, rule); + output << "\\maudePathRight$\n"; + generateHeading("variant unifier:"); + generateCompoundSubstitution(*unifier, *rule, *unifierVariableInfo, rule->getModule()); + } + else + { + int label = rule->getLabel().id(); + if (label != NONE) + output <<"\\par$\\maudePathWithLabel{\\maudeLabel{" << Token::latexName(label) << "}}$\n"; + else + output <<"\\par$\\maudePathWithoutLabel$\n"; + } + } + output << "\\par\\maudeResponse{state}\\maudeSpace\\maudeNumber{" << index << "}\\maudePunctuation{,}\\maudeSpace"; + generateType(newDag->getSort()); + output << "\\maudePunctuation{:}$\\maudeSpace\n"; + MixfixModule::latexPrintDagNode(output, newDag); + output << "$\n"; + generateHeading("accumulated substitution:"); + generateSubstitution(*accumulatedSubstitution, state->getInitialVariableInfo()); + } + output << "\\end{maudeResultParagraph}\n%\n% End of show path\n%\n"; +} + void MaudeLatexBuffer::generateSearchPathLabels(const RewriteSequenceSearch* graph, const Vector& steps, diff --git a/src/Mixfix/lexer.ll b/src/Mixfix/lexer.ll index 5060604f..e2ed1d19 100644 --- a/src/Mixfix/lexer.ll +++ b/src/Mixfix/lexer.ll @@ -262,12 +262,14 @@ vu-narrow return KW_VU_NARROW; fvu-narrow return KW_FVU_NARROW; fold return KW_FOLD; vfold return KW_VFOLD; -invariant return KW_INVARIANT; desugared return KW_DESUGARED; processed return KW_PROCESSED; hook|hooks return KW_HOOKS; combine return KW_COMBINE; -[.\[\](){}] return *yytext; +frontier return KW_FRONTIER; +most return KW_MOST; +general return KW_GENERAL; +[.,\[\](){}] return *yytext; 0|([1-9][0-9]*) { bool dummy; lvalp->yyInt64 = stringToInt64(yytext, dummy, 10); diff --git a/src/Mixfix/maudeLatexBuffer.cc b/src/Mixfix/maudeLatexBuffer.cc index 7704933f..b0761b27 100644 --- a/src/Mixfix/maudeLatexBuffer.cc +++ b/src/Mixfix/maudeLatexBuffer.cc @@ -289,3 +289,46 @@ MaudeLatexBuffer::generateState(DagNode* stateDag, const char* message) MixfixModule::latexPrintDagNode(output, stateDag); output << "$\n"; } + +void +MaudeLatexBuffer::generateCompoundSubstitution(const Substitution& substitution, + const VariableInfo& variableInfo, + const NarrowingVariableInfo& narrowingVariableInfo, + Module* m) +{ + // We deal with a substitution that is broken into two parts. + // The first part is bindings to variables from a PreEquation and + // the variable names are given by Terms in variableInfo. + // The second part is bindings to variables from a term being narrowed + // and the variable names are given by DagNodes in narrowingVariableInfo. + // + int nrVariables1 = variableInfo.getNrRealVariables(); + int nrVariables2 = narrowingVariableInfo.getNrVariables(); + for (int i = 0; i < nrVariables1; ++i) + { + Term* v = variableInfo.index2Variable(i); + DagNode* b = substitution.value(i); + output << "\\par$"; + MixfixModule::latexPrettyPrint(output, v); + output << "\\maudeIsAssigned"; + if (b == 0) + output << "\\maudeMisc{(unbound)}\n"; + else + MixfixModule::latexPrintDagNode(output, b); + output << "$\n"; + } + // + // Variables from the dag being narrowed start after the regular substitution. + // + int firstTargetSlot = m->getMinimumSubstitutionSize(); + for (int i = 0; i < nrVariables2; ++i) + { + DagNode* v = narrowingVariableInfo.index2Variable(i); + DagNode* b = substitution.value(firstTargetSlot + i); + output << "\\par$"; + MixfixModule::latexPrintDagNode(output, v); + output << "\\maudeIsAssigned"; + MixfixModule::latexPrintDagNode(output, b); + output << "$\n"; + } +} diff --git a/src/Mixfix/maudeLatexBuffer.hh b/src/Mixfix/maudeLatexBuffer.hh index f307a3b1..d77c5da0 100644 --- a/src/Mixfix/maudeLatexBuffer.hh +++ b/src/Mixfix/maudeLatexBuffer.hh @@ -99,7 +99,6 @@ public: void generateShow(bool showCommand, const string& command, View* module); void generateShow(bool showCommand, const string& command); void generateLoopTokens(bool showCommand, const Vector& tokens); - // // Functions to print results. // @@ -160,11 +159,22 @@ public: int stateNr, bool showCommand, bool showRule); + void generateNarrowingSearchPath(const NarrowingSequenceSearch3* state, + const Vector& steps, + int stateNr, + bool showCommand, + bool showRule); void generateSearchPathLabels(const RewriteSequenceSearch* graph, const Vector& steps, int stateNr, bool showCommand); void generateSearchGraph(const RewriteSequenceSearch* graph, bool showCommand); + void generateStateSet(bool showCommand, + const char* command, + const Vector& firstPart, + bool highlight, + const Vector& secondPart, + const char* emptyMessage); // // Three different representations of substitutions. // @@ -177,6 +187,11 @@ public: const NarrowingVariableInfo& variableInfo); void generateVariant(const Vector& variant, const NarrowingVariableInfo& variableInfo); + + void generateCompoundSubstitution(const Substitution& substitution, + const VariableInfo& variableInfo, + const NarrowingVariableInfo& narrowingVariableInfo, + Module* m); void generateWarning(const char* message); void generateAdvisory(const char* message); diff --git a/src/Mixfix/narrowing.cc b/src/Mixfix/narrowing.cc index dfc98210..971c4ce0 100644 --- a/src/Mixfix/narrowing.cc +++ b/src/Mixfix/narrowing.cc @@ -160,7 +160,15 @@ Interpreter::doVuNarrowing(Timer& timer, { bool result = state->findNextUnifier(); if (UserLevelRewritingContext::aborted()) - break; + { + // + // Tidy up and return. + // + delete state; + module->unprotect(); + UserLevelRewritingContext::clearDebug(); + return; + } Int64 real = 0; Int64 virt = 0; Int64 prof = 0; @@ -231,27 +239,176 @@ Interpreter::doVuNarrowing(Timer& timer, if (latexBuffer) latexBuffer->cleanUp(); clearContinueInfo(); // just in case debugger left info + // + // We always save these things even if we can't continue + // in order to allow inspection of the narrowing paths. + // + savedState = state; + savedModule = module; if (i == limit) // possible to continue { // - // The loop terminated because we hit user's limit so - // continuation is still possible. We save the state, - // solutionCount and module, and set a continutation function. + // The loop terminated because we hit user's limit so ontinuation is still possible. + // We save the state solutionCount and set a continutation function. // context->clearCount(); - savedState = state; savedSolutionCount = solutionCount; - savedModule = module; continueFunc = &Interpreter::vuNarrowingCont; } - else + UserLevelRewritingContext::clearDebug(); +} + +void +Interpreter::showNarrowingSearchPath(int stateNr, bool showRule, NarrowingSequenceSearch3* savedNarrowingSequence) const +{ + if (stateNr < 0 || !(savedNarrowingSequence->locked(stateNr))) { - // - // Either user aborted or we ran out of solutions; either - // way we need to tidy up. - // - delete state; - module->unprotect(); + IssueWarning("bad state number " << QUOTE(stateNr) << "."); + return; + } + Vector steps; + for (int i = stateNr; i != NONE; i = savedNarrowingSequence->getStateParent(i)) + steps.push_back(i); + for (Index i = steps.size() - 1; i >= 0; --i) + { + int index = steps[i]; + DagNode* root; + DagNode* position; + Rule* rule; + const Substitution* unifier; + const NarrowingVariableInfo* unifierVariableInfo; + int variableFamily; + DagNode* newDag; + const Substitution* accumulatedSubstitution; + int parentIndex; + savedNarrowingSequence->getHistory(index, + root, + position, + rule, + unifier, + unifierVariableInfo, + variableFamily, + newDag, + accumulatedSubstitution, + parentIndex); + if (parentIndex != NONE) + { + if (showRule) + { + cout << "===[ " << rule << " ]===>\n"; + cout << "variant unifier:" << endl; + UserLevelRewritingContext::printCompoundSubstitution(*unifier, *rule, *unifierVariableInfo, rule->getModule()); + } + else + { + const Label& l = rule->getLabel(); + cout << "---"; + if (l.id() != NONE) + cout << ' ' << &l << ' '; + cout << "--->\n"; + } + } + cout << "state " << index << ", " << newDag->getSort() << ": " << newDag << '\n'; + cout << "accumulated substitution:" << endl; + UserLevelRewritingContext::printSubstitution(*accumulatedSubstitution, savedNarrowingSequence->getInitialVariableInfo()); + } + if (latexBuffer) + { + latexBuffer->generateNarrowingSearchPath(savedNarrowingSequence, + steps, + stateNr, + getFlag(SHOW_COMMAND), + showRule); + } +} + +void +Interpreter::showFrontierStates() +{ + NarrowingSequenceSearch3* savedNarrowingSequence = dynamic_cast(savedState); + if (!savedNarrowingSequence) + { + IssueWarning("no narrowing state forest."); + return; + } + const char* sep = ""; + // + // In the =>1, =>+, =>* cases we may have visited a state without (fully) expanding it + // when we pause due to hitting the solution bound or halt due to hitting the depth bound. + // This state belongs in the frontier. + // + // In the =>! case we may have visited states, determined they have a descendant but + // not expanded them to avoid exceeding a depth bound. They also belong in the frontier. + // + bool partiallyExpanded; + Vector visitedButUnexpanded = savedNarrowingSequence->getUnexpandedStates(partiallyExpanded); + for (DagNode* d : visitedButUnexpanded) + { + cout << sep; + if (partiallyExpanded) + cout << Tty(Tty::RED) << d << Tty(Tty::RESET); // paused due to solution bound in =>1, =>+, =>* cases + else + cout << d; // halted due to depth bound, or in =>! case + sep = " /\\\n"; + } + // + // It's possible to have unvisited states even if we don't have a visited but unexpanded state. + // This happens if we pause due to solution bound before we finished unifying with initial states; + // At this point we have not started narrowing and therefore have visited no states, but we will + // have at least one initial state that is unvisited. + // + Vector unvisitedStates = savedNarrowingSequence->getUnvisitedStates(); + for (DagNode* d : unvisitedStates) + { + cout << sep << d; + sep = " /\\\n"; + } + // + // If we exhausted the search space before hitting a bound, this means the frontier is empty. + // + if (*sep == '\0') + cout << Tty(Tty::RED) << "*** frontier is empty ***" << Tty(Tty::RESET); + cout << endl; + if (latexBuffer) + { + latexBuffer->generateStateSet(getFlag(SHOW_COMMAND), + "show frontier states", + visitedButUnexpanded, + partiallyExpanded, + unvisitedStates, + "\\color{red}*** frontier is empty ***\\color{black}"); + } +} + +void +Interpreter::showMostGeneralStates() +{ + NarrowingSequenceSearch3* savedNarrowingSequence = dynamic_cast(savedState); + if (!savedNarrowingSequence) + { + IssueWarning("no narrowing state forest."); + return; + } + if (!(savedNarrowingSequence->getVariantFlags() & (NarrowingSequenceSearch3::FOLD | NarrowingSequenceSearch3::VFOLD))) + { + IssueWarning("most general states are only computed when folding."); + return; + } + Vector mostGeneralStates = savedNarrowingSequence->getMostGeneralStates(); + const char* sep = ""; + for (DagNode* d : mostGeneralStates) + { + cout << sep << d; + sep = " /\\\n"; + } + cout << endl; + if (latexBuffer) + { + latexBuffer->generateStateSet(getFlag(SHOW_COMMAND), + "show most general states", + Vector(), + false, + mostGeneralStates, + nullptr); } - UserLevelRewritingContext::clearDebug(); } diff --git a/src/Mixfix/search.cc b/src/Mixfix/search.cc index 84ae94a2..c8f20a98 100644 --- a/src/Mixfix/search.cc +++ b/src/Mixfix/search.cc @@ -177,8 +177,19 @@ Interpreter::search(const Vector& bubble, UserLevelRewritingContext::beginCommand(); if (debug) cout << "debug "; - if (variantFlags & NarrowingSequenceSearch3::FOLD) - cout << "{fold} "; + if (variantFlags & (NarrowingSequenceSearch3::FOLD | NarrowingSequenceSearch3::VFOLD | NarrowingSequenceSearch3::KEEP_PATHS)) + { + const char* sep = ", "; + if (variantFlags & NarrowingSequenceSearch3::FOLD) + cout << "{fold"; + else if (variantFlags & NarrowingSequenceSearch3::VFOLD) + cout << "{vfold"; + else + sep = "{"; + if (variantFlags & NarrowingSequenceSearch3::KEEP_PATHS) + cout << sep << "path"; + cout << "} "; + } cout << searchKindName[searchKind] << ' '; if (variantFlags & (VariantSearch::IRREDUNDANT_MODE | VariantUnificationProblem::FILTER_VARIANT_UNIFIERS)) @@ -319,7 +330,15 @@ Interpreter::doSearching(Timer& timer, { bool result = state->findNextMatch(); if (UserLevelRewritingContext::aborted()) - break; // HACK: Is this safe - shouldn't we destroy context? + { + // + // Tidy up and return. + // + delete state; + module->unprotect(); + UserLevelRewritingContext::clearDebug(); + return; + } Int64 real = 0; Int64 virt = 0; Int64 prof = 0; @@ -392,9 +411,8 @@ Interpreter::doSearching(Timer& timer, if (i == limit) { // - // The loop terminated because we hit user's limit so - // continuation is still possible. We save the state, - // solutionCount and module, and set a continutation function. + // The loop terminated because we hit user's limit so continuation is still possible. + // We save the solutionCount and set a continutation function. // state->getContext()->clearCount(); savedSolutionCount = solutionCount; @@ -427,6 +445,11 @@ Interpreter::searchCont(Int64 limit, bool debug) void Interpreter::showSearchPath(int stateNr, bool showRule) { + if (NarrowingSequenceSearch3* savedNarrowingSequence = dynamic_cast(savedState)) + { + showNarrowingSearchPath(stateNr, showRule, savedNarrowingSequence); + return; + } RewriteSequenceSearch* savedRewriteSequenceSearch = dynamic_cast(savedState); if (savedRewriteSequenceSearch == 0) { diff --git a/src/Mixfix/top.yy b/src/Mixfix/top.yy index 86c5e741..21f6acca 100644 --- a/src/Mixfix/top.yy +++ b/src/Mixfix/top.yy @@ -165,8 +165,8 @@ int yylex(YYSTYPE* lvalp); %token KW_NUMBER KW_RAT KW_COLOR KW_IMPLIED_STEP %token SIMPLE_NUMBER %token KW_PWD KW_CD KW_PUSHD KW_POPD KW_LS KW_LL KW_LOAD KW_SLOAD KW_QUIT -%token KW_EOF KW_TEST KW_SMT_SEARCH KW_VU_NARROW KW_FVU_NARROW KW_FOLD KW_VFOLD KW_INVARIANT -%token KW_DESUGARED KW_PROCESSED +%token KW_EOF KW_TEST KW_SMT_SEARCH KW_VU_NARROW KW_FVU_NARROW KW_FOLD KW_VFOLD +%token KW_DESUGARED KW_PROCESSED KW_FRONTIER KW_MOST KW_GENERAL /* * Start keywords: signal end of mixfix statement if following '.'. diff --git a/src/Mixfix/userLevelRewritingContext.cc b/src/Mixfix/userLevelRewritingContext.cc index 834e2977..8824f2e1 100644 --- a/src/Mixfix/userLevelRewritingContext.cc +++ b/src/Mixfix/userLevelRewritingContext.cc @@ -569,3 +569,35 @@ UserLevelRewritingContext::printSubstitution(const Substitution& substitution, if (!printedVariable) cout << "empty substitution\n"; } + +void +UserLevelRewritingContext::printCompoundSubstitution(const Substitution& substitution, + const VariableInfo& variableInfo, + const NarrowingVariableInfo& narrowingVariableInfo, + Module* m) +{ + // We deal with a substitution that is broken into two parts. + // The first part is bindings to variables from a PreEquation and + // the variable names are given by Terms in variableInfo. + // The second part is bindings to variables from a term being narrowed + // and the variable names are given by DagNodes in narrowingVariableInfo. + // + int nrVariables1 = variableInfo.getNrRealVariables(); + int nrVariables2 = narrowingVariableInfo.getNrVariables(); + for (int i = 0; i < nrVariables1; ++i) + { + Term* v = variableInfo.index2Variable(i); + DagNode* b = substitution.value(i); + cout << v << " --> " << b << '\n'; + } + // + // Variables from the dag being narrowed start after the regular substitution. + // + int firstTargetSlot = m->getMinimumSubstitutionSize(); + for (int i = 0; i < nrVariables2; ++i) + { + DagNode* v = narrowingVariableInfo.index2Variable(i); + DagNode* b = substitution.value(firstTargetSlot + i); + cout << v << " --> " << b << '\n'; + } +} diff --git a/src/Mixfix/userLevelRewritingContext.hh b/src/Mixfix/userLevelRewritingContext.hh index f3866a4e..c3655a3d 100644 --- a/src/Mixfix/userLevelRewritingContext.hh +++ b/src/Mixfix/userLevelRewritingContext.hh @@ -137,6 +137,11 @@ public: static void printSubstitution(const Substitution& substitution, const NarrowingVariableInfo& variableInfo); + static void printCompoundSubstitution(const Substitution& substitution, + const VariableInfo& variableInfo, + const NarrowingVariableInfo& narrowingVariableInfo, + Module* m); + bool interruptSeen(); private: diff --git a/src/ObjectSystem/ChangeLog b/src/ObjectSystem/ChangeLog index 9e00a583..dfe0b3ec 100755 --- a/src/ObjectSystem/ChangeLog +++ b/src/ObjectSystem/ChangeLog @@ -1,3 +1,10 @@ +2024-05-10 Steven Eker + + * streamManagerSymbol.cc (StreamManagerSymbol::nonblockingGetLine): + allow \n to be backslashed for continuation lines + +===================================Maude161=========================================== + 2024-04-10 Steven Eker * timeActions.cc (TimeManagerSymbol::getTimeSinceEpoch): use diff --git a/src/ObjectSystem/processStuff.cc b/src/ObjectSystem/processStuff.cc index 04e70641..27a8831b 100644 --- a/src/ObjectSystem/processStuff.cc +++ b/src/ObjectSystem/processStuff.cc @@ -81,9 +81,7 @@ ProcessManagerSymbol::doChildExit(pid_t childPid) // int wstatus; DebugSave(exitPid, waitpid(childPid, &wstatus, 0)); - //pid_t exitPid = waitpid(childPid, &wstatus, 0); - Assert(exitPid == childPid, "unexpected return value " << exitPid << - " from waidpid() for process " << childPid); + Assert(exitPid == childPid, "unexpected return value " << exitPid << " from waidpid() for process " << childPid); // // Recover original waitForProcessExit message and context. // diff --git a/src/ObjectSystem/streamManagerSymbol.cc b/src/ObjectSystem/streamManagerSymbol.cc index 2c800d20..073f1f3f 100644 --- a/src/ObjectSystem/streamManagerSymbol.cc +++ b/src/ObjectSystem/streamManagerSymbol.cc @@ -466,7 +466,7 @@ StreamManagerSymbol::nonblockingGetLine(FreeDagNode* message, // close(resultReturnPipe[READ_END]); DagNode* promptArg = message->getArgument(2); - const Rope& prompt = safeCast(StringDagNode*, promptArg)->getValue(); + Rope prompt = safeCast(StringDagNode*, promptArg)->getValue(); if (ioManager.usingTecla()) { // @@ -508,9 +508,26 @@ StreamManagerSymbol::nonblockingGetLine(FreeDagNode* message, // There is no need to unblock it ourselves after Tecla // returns because we're going to exit() anyway. // - // Now we can read a line. + // Now we can read a line. We treat \\\n as indicating an incomplete line. // - Rope line = ioManager.getLineFromStdin(prompt); + Rope line; + for (;;) + { + Rope partial = ioManager.getLineFromStdin(prompt); + if (partial.empty()) + break; // ^D + auto nrChars = partial.length(); + if (nrChars > 1 && partial[nrChars - 2] == '\\') + { + line += partial.substr(0, nrChars - 2); // remove \\\n + prompt = "> "; + } + else + { + line += partial; + break; + } + } // // Then we need to write the line to the pipe. //