diff --git a/ChangeLog b/ChangeLog index d0864058..1b2b592e 100755 --- a/ChangeLog +++ b/ChangeLog @@ -1,6 +1,20 @@ +2023-04-13 Steven Eker + + * tests/Corner/attributeOverparsing.maude: added latex examples + +2023-04-11 Steven Eker + + * tests/Corner/attributeOverparsing.maude: added + + * tests/Corner/fakeParameterConstant.maude: added + + * tests/Corner/fakeParameterSort.maude: added + +===================================Maude144=========================================== + 2023-04-10 Steven Eker - * tests/ResolvedBugs/pseudoParameterTheoryConstantMarch2023.maude: created + * tests/ResolvedBugs/pseudoParameterTheoryConstantMarch2023.maude: added * tests/ResolvedBugs/pseudoParametersMarch2023.maude: added diff --git a/NEWS b/NEWS index 4db0bed3..c7297b81 100755 --- a/NEWS +++ b/NEWS @@ -1,19 +1,27 @@ -Overview of Changes in alpha144 +Overview of Changes in Maude 3.3.1 (alpha145) (2023-04-13) +========================================================== +* fixed a bug where internal error and stack overflow messages +didn't appear on Macs by not stripping Mac binary +* overparsing for attributes with missing information in operator +declarations and mappings + +Overview of Changes in alpha144 (2023-04-10) ============================================ * fixed a bug where special symbols other than strings that started with " were not recognized. * fixed a bug where renamings that mapped parameterized constants were not being correctly instantiated -* fixed a bug where operator with the same name but different +* fixed a bug where operators with the same name but different arities could confuse renamings generated to instantiate modules * fixed a bug where a change of parameter was not supported for -parameterized polymorpic constants +parameterized polymorphic constants * fixed a large family of bugs where identifiers that looked like parameters but which were not ("pseudo parameters") could clash with actual parameters by enforcing new constraints * fixed a bug where a constant from a parameter theory that looked like a parameterized constant was being treated as such for various operations +* different message for self-check failure Overview of Changes in Maude 3.3 (alpha143) (2023-03-22) ======================================================== diff --git a/README.md b/README.md index 30f6893a..c548933e 100755 --- a/README.md +++ b/README.md @@ -9,6 +9,12 @@ Rewriting logic is a logic of concurrent change that can naturally deal with sta Maude supports in a systematic and efficient way logical reflection. This makes Maude remarkably extensible and powerful, supports an extensible algebra of module composition operations, and allows many advanced metaprogramming and metalanguage applications. Indeed, some of the most interesting applications of Maude are metalanguage applications, in which Maude is used to create executable environments for different logics, theorem provers, languages, and models of computation. +## Maude 3.3.1 + +* Restrictions on pseudo-parameters +* More overparsing +* Many bug fixes + ## Maude 3.3 * Support for object-oriented syntactic sugar (omods/oths) diff --git a/configure b/configure index bd8b3d25..c9937938 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 alpha144. +# Generated by GNU Autoconf 2.69 for Maude 3.3.1. # # Report bugs to . # @@ -580,8 +580,8 @@ MAKEFLAGS= # Identity of this package. PACKAGE_NAME='Maude' PACKAGE_TARNAME='maude' -PACKAGE_VERSION='alpha144' -PACKAGE_STRING='Maude alpha144' +PACKAGE_VERSION='3.3.1' +PACKAGE_STRING='Maude 3.3.1' 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 alpha144 to adapt to many kinds of systems. +\`configure' configures Maude 3.3.1 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 alpha144:";; + short | recursive ) echo "Configuration of Maude 3.3.1:";; 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 alpha144 +Maude configure 3.3.1 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 alpha144, which was +It was created by Maude $as_me 3.3.1, 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='alpha144' + VERSION='3.3.1' 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 alpha144, which was +This file was extended by Maude $as_me 3.3.1, 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 alpha144 +Maude config.status 3.3.1 configured by $0, generated by GNU Autoconf 2.69, with options \\"\$ac_cs_config\\" diff --git a/configure.ac b/configure.ac index 605b578c..2f4dc28b 100755 --- a/configure.ac +++ b/configure.ac @@ -3,7 +3,7 @@ # # Initialize autoconf stuff. # -AC_INIT(Maude, alpha144, [maude-bugs@lists.cs.illinois.edu]) +AC_INIT(Maude, 3.3.1, [maude-bugs@lists.cs.illinois.edu]) # # Allow directory names that look like macros. # diff --git a/doc/Makefile.am b/doc/Makefile.am index a1bbe4c8..1d00d89f 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -12,4 +12,5 @@ EXTRA_DIST = \ alpha141.txt \ alpha142.txt \ alpha143.txt \ - alpha144.txt + alpha144.txt \ + alpha145.txt diff --git a/doc/Makefile.in b/doc/Makefile.in index 9d2f96b7..2aa5e195 100644 --- a/doc/Makefile.in +++ b/doc/Makefile.in @@ -244,7 +244,8 @@ EXTRA_DIST = \ alpha141.txt \ alpha142.txt \ alpha143.txt \ - alpha144.txt + alpha144.txt \ + alpha145.txt all: all-am diff --git a/doc/alpha145.txt b/doc/alpha145.txt new file mode 100644 index 00000000..6221b2cd --- /dev/null +++ b/doc/alpha145.txt @@ -0,0 +1,27 @@ +Alpha 145 release notes +======================== + +Bug fix +======== + +A bug where internal error and stack overflow messages were being +lost on Macs. This seems to be due to stripped binaries so the Mac binary +is no longer stripped. + +Other changes +============== + +(1) Overparsing for prec/gather/format/strat/strategy/poly attributes +without their needed information in operator declarations. For example: + +fmod FOO is + op _+_ : Bool Bool -> Bool [prec gather format strat strategy poly] . +endfm + + +(2) Overparsing for prec/gather/format attributes without their needed +information in operator mappings. For example: + +fmod FOO is + inc NAT * (op _+_ to _++_ [format prec gather]) . +endfm diff --git a/src/ACU_Theory/ACU_LhsAutomaton.hh b/src/ACU_Theory/ACU_LhsAutomaton.hh index b0ba7e42..17c2ee73 100644 --- a/src/ACU_Theory/ACU_LhsAutomaton.hh +++ b/src/ACU_Theory/ACU_LhsAutomaton.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-2023 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 @@ -244,10 +244,10 @@ private: ACU_ExtensionInfo* extensionInfo); ACU_Symbol* const topSymbol; - const Bool matchAtTop; - const Bool collapsePossible; - Bool treeMatchOK; - Bool collectorSeen; + const bool matchAtTop; + const bool collapsePossible; + bool treeMatchOK; + bool collectorSeen; MatchStrategy matchStrategy; int totalLowerBound; // must have at least this total mutiplicity of subjects int totalUpperBound; // can't have more than this total mutiplicity of subjects diff --git a/src/ACU_Theory/ACU_LhsCompiler1.cc b/src/ACU_Theory/ACU_LhsCompiler1.cc index 375d43b6..e3786ab8 100644 --- a/src/ACU_Theory/ACU_LhsCompiler1.cc +++ b/src/ACU_Theory/ACU_LhsCompiler1.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-2023 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 @@ -77,14 +77,14 @@ ACU_Term::analyseConstraintPropagation(NatSet& boundUniquely) const } if (lastUnboundVariable != UNDEFINED) { - Assert(nonGroundAliens.size() == 0, "ACU_Term::analyseConstraintPropagation() : shouldn't have NGAs"); + Assert(nonGroundAliens.empty(), "ACU_Term::analyseConstraintPropagation() : shouldn't have NGAs"); // // If the only thing that doesn't ground out is a variable we can // bind it uniquely. // boundUniquely.insert(lastUnboundVariable); } - else if (nonGroundAliens.length() != 0) + else if (!nonGroundAliens.empty()) { // // If the only things that don't ground out are NGAs we can choose a diff --git a/src/ACU_Theory/ACU_NonLinearLhsAutomaton.hh b/src/ACU_Theory/ACU_NonLinearLhsAutomaton.hh index 9e6bd49e..bd14ee65 100644 --- a/src/ACU_Theory/ACU_NonLinearLhsAutomaton.hh +++ b/src/ACU_Theory/ACU_NonLinearLhsAutomaton.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-2023 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 @@ -59,8 +59,8 @@ private: const int varIndex; const int multiplicity; Sort* const varSort; - const Bool unitSort; - const Bool pureSort; + const bool unitSort; + const bool pureSort; }; #endif diff --git a/src/ACU_Theory/ACU_Term.hh b/src/ACU_Theory/ACU_Term.hh index 471a28cf..5cb1ded9 100644 --- a/src/ACU_Theory/ACU_Term.hh +++ b/src/ACU_Theory/ACU_Term.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-2023 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 @@ -77,8 +77,8 @@ private: Term* term; int multiplicity; short abstractionVariableIndex; // if subterm could enter our theory we abstract it - Bool collapseToOurSymbol; // first possible reason for variable abstraction - Bool matchOurIdentity; // second possible reason for variable abstraction + bool collapseToOurSymbol; // first possible reason for variable abstraction + bool matchOurIdentity; // second possible reason for variable abstraction }; struct CP_Sequence; diff --git a/src/ACU_Theory/ChangeLog b/src/ACU_Theory/ChangeLog index 277bd254..f4b94206 100755 --- a/src/ACU_Theory/ChangeLog +++ b/src/ACU_Theory/ChangeLog @@ -1,3 +1,19 @@ +2023-04-13 Steven Eker + + * ACU_LhsCompiler1.cc (ACU_Term::analyseConstraintPropagation): use + empty() (2 places) + +2023-04-12 Steven Eker + + * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): Bool -> bool + + * ACU_Term.hh (class ACU_Term): Bool -> bool + + * ACU_NonLinearLhsAutomaton.hh (class ACU_NonLinearLhsAutomaton): + Bool -> bool + +===================================Maude145=========================================== + 2023-03-27 Steven Eker * ACU_RhsAutomaton.cc (ACU_RhsAutomaton::ACU_RhsAutomaton): use diff --git a/src/AU_Theory/AU_Layer.hh b/src/AU_Theory/AU_Layer.hh index 585a13c9..8797ab40 100644 --- a/src/AU_Theory/AU_Layer.hh +++ b/src/AU_Theory/AU_Layer.hh @@ -56,8 +56,8 @@ private: // // For solve-time use // - Bool boundByUs; - Bool extraId; + bool boundByUs; + bool extraId; }; struct Node @@ -77,10 +77,10 @@ private: const AU_DagNode* subject; int lastSubjectSubterm; // index of last subterm in subject - Bool oneSidedId; // true if subject has a one sided identity - Bool leftId; // true if subject has left identity only - Bool leftExtend; // have left extension before variable block - Bool rightExtend; // have right extension after variable block + bool oneSidedId; // true if subject has a one sided identity + bool leftId; // true if subject has left identity only + bool leftExtend; // have left extension before variable block + bool rightExtend; // have right extension after variable block int totalLowerBound; // sum of lowerBounds for prevVariables int totalUpperBound; // sum of upperBounds for prevVariables + extension AU_ExtensionInfo* extensionInfo; // for layers with leftExtend/rightExtend only diff --git a/src/AU_Theory/AU_LhsAutomaton.hh b/src/AU_Theory/AU_LhsAutomaton.hh index 58bc99bb..f8bf0120 100644 --- a/src/AU_Theory/AU_LhsAutomaton.hh +++ b/src/AU_Theory/AU_LhsAutomaton.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-2023 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,8 +118,8 @@ private: struct TopVariable { short index; - Bool takeIdentity; // take identity instead of piece of subject (always) - Bool awkward; // take identity instead of piece of subject (special) + bool takeIdentity; // take identity instead of piece of subject (always) + bool awkward; // take identity instead of piece of subject (special) Sort* sort; int upperBound; LhsAutomaton* abstracted; // automaton for abstracted term diff --git a/src/AU_Theory/AU_LhsCompiler.cc b/src/AU_Theory/AU_LhsCompiler.cc index 0fe5cace..355db6d6 100644 --- a/src/AU_Theory/AU_LhsCompiler.cc +++ b/src/AU_Theory/AU_LhsCompiler.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-2023 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 @@ -26,7 +26,7 @@ struct AU_Term::CP_Sequence { - Vector sequence; // true = take left term, false = take right term + Vector sequence; // true = take left term, false = take right term NatSet bound; int cardinality; int firstFlex; @@ -354,14 +354,14 @@ AU_Term::findConstraintPropagationSequence(const NatSet& boundUniquely, { DebugAdvisory("toplevel findConstraintPropagationSequence() - array length = " << argArray.length() << " subterm = " << this); - Vector currentSequence; + Vector currentSequence; bestSequence.cardinality = -1; findConstraintPropagationSequence(currentSequence, boundUniquely, 0, argArray.length() - 1, bestSequence); } void -AU_Term::findConstraintPropagationSequence(const Vector& currentSequence, +AU_Term::findConstraintPropagationSequence(const Vector& currentSequence, const NatSet& boundUniquely, int leftPos, int rightPos, @@ -380,7 +380,7 @@ AU_Term::findConstraintPropagationSequence(const Vector& currentSequence, if (!leftBad && boundUniquely.contains(lt.term->occursBelow())) { DebugAdvisory("lower level findConstraintPropagationSequence() - ground out left " << leftPos); - Vector newSequence(currentSequence); + Vector newSequence(currentSequence); newSequence.append(true); findConstraintPropagationSequence(newSequence, boundUniquely, leftPos + 1, rightPos, bestSequence); @@ -392,7 +392,7 @@ AU_Term::findConstraintPropagationSequence(const Vector& currentSequence, if (!rightBad && boundUniquely.contains(rt.term->occursBelow())) { DebugAdvisory("lower level findConstraintPropagationSequence() - ground out right " << rightPos); - Vector newSequence(currentSequence); + Vector newSequence(currentSequence); newSequence.append(false); findConstraintPropagationSequence(newSequence, boundUniquely, leftPos, rightPos - 1, bestSequence); @@ -406,7 +406,7 @@ AU_Term::findConstraintPropagationSequence(const Vector& currentSequence, if (unitVariable(ltVar, leftPos)) { DebugAdvisory("lower level findConstraintPropagationSequence() - unit var left " << leftPos); - Vector newSequence(currentSequence); + Vector newSequence(currentSequence); newSequence.append(true); NatSet newBound(boundUniquely); newBound.insert(ltVar->getIndex()); @@ -418,7 +418,7 @@ AU_Term::findConstraintPropagationSequence(const Vector& currentSequence, if (leftPos < rightPos && unitVariable(rtVar, rightPos)) { DebugAdvisory("lower level findConstraintPropagationSequence() - unit var right " << rightPos); - Vector newSequence(currentSequence); + Vector newSequence(currentSequence); newSequence.append(false); NatSet newBound(boundUniquely); newBound.insert(rtVar->getIndex()); @@ -434,7 +434,7 @@ AU_Term::findConstraintPropagationSequence(const Vector& currentSequence, if (!leftBad && ltVar == 0) { DebugAdvisory("lower level findConstraintPropagationSequence() - alien left " << leftPos); - Vector newSequence(currentSequence); + Vector newSequence(currentSequence); newSequence.append(true); NatSet newBound(boundUniquely); lt.term->analyseConstraintPropagation(newBound); @@ -454,7 +454,7 @@ AU_Term::findConstraintPropagationSequence(const Vector& currentSequence, if (!rightBad && rtVar == 0) { DebugAdvisory("lower level findConstraintPropagationSequence() - alien right " << rightPos); - Vector newSequence(currentSequence); + Vector newSequence(currentSequence); newSequence.append(false); NatSet newBound(boundUniquely); rt.term->analyseConstraintPropagation(newBound); diff --git a/src/AU_Theory/AU_Matcher.cc b/src/AU_Theory/AU_Matcher.cc index 61232ae1..175535c5 100644 --- a/src/AU_Theory/AU_Matcher.cc +++ b/src/AU_Theory/AU_Matcher.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-2023 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 @@ -66,8 +66,7 @@ AU_LhsAutomaton::match(DagNode* subject, if (e == 0) { if (!matchRigidPart(s, solution, subproblems) || - (flexPart.length() != 0 && - !checkForRigidEnds(s, solution, subproblems))) + (!flexPart.empty() && !checkForRigidEnds(s, solution, subproblems))) return false; int flexRemaining = flexRightPos - flexLeftPos + 1; if (flexRemaining == 0) diff --git a/src/AU_Theory/AU_Symbol.hh b/src/AU_Theory/AU_Symbol.hh index 6760eb18..fa278a59 100644 --- a/src/AU_Theory/AU_Symbol.hh +++ b/src/AU_Theory/AU_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-2023 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 @@ -99,15 +99,15 @@ private: RewritingContext& context); void copyAndReduceSubterms(AU_DagNode* subject, RewritingContext& context); - const Bool leftIdFlag; - const Bool rightIdFlag; - const Bool oneSidedIdFlag; + const bool leftIdFlag; + const bool rightIdFlag; + const bool oneSidedIdFlag; // // Deque represention of arguments can be used if there is no // one-sided identity, no fancy strategy and there are no equations // at the top. // - Bool useDequeFlag; + bool useDequeFlag; }; inline bool diff --git a/src/AU_Theory/AU_Term.hh b/src/AU_Theory/AU_Term.hh index 4b349589..56e0aa04 100644 --- a/src/AU_Theory/AU_Term.hh +++ b/src/AU_Theory/AU_Term.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-2023 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 @@ -79,8 +79,8 @@ private: Term* term; short abstractionVariableIndex; // if subterm could enter our theory // we abstract it - Bool collapseToOurSymbol; // 1st possible reason for variable abstraction - Bool matchOurIdentity; // 2nd possible reason for variable abstraction + bool collapseToOurSymbol; // 1st possible reason for variable abstraction + bool matchOurIdentity; // 2nd possible reason for variable abstraction }; struct CP_Sequence; @@ -89,7 +89,7 @@ private: bool unitVariable(VariableTerm* vt, int index) const; void findConstraintPropagationSequence(const NatSet& boundUniquely, CP_Sequence& bestSequence) const; - void findConstraintPropagationSequence(const Vector& currentSequence, + void findConstraintPropagationSequence(const Vector& currentSequence, const NatSet& boundUniquely, int leftPos, int rightPos, diff --git a/src/AU_Theory/ChangeLog b/src/AU_Theory/ChangeLog index 59b5f4bf..fba88452 100755 --- a/src/AU_Theory/ChangeLog +++ b/src/AU_Theory/ChangeLog @@ -1,3 +1,21 @@ +2023-04-13 Steven Eker + + * AU_Matcher.cc (AU_LhsAutomaton::match): use empty() + +2023-04-12 Steven Eker + + * AU_LhsCompiler.cc: Bool -> bool throughout + + * AU_LhsAutomaton.hh (class AU_LhsAutomaton): Bool -> bool + + * AU_Term.hh (class AU_Term): Bool -> bool + + * AU_Layer.hh (class AU_Layer): Bool -> bool + + * AU_Symbol.hh (class AU_Symbol): Bool -> bool + +===================================Maude145=========================================== + 2023-03-27 Steven Eker * AU_RhsAutomaton.cc (AU_RhsAutomaton::AU_RhsAutomaton): use diff --git a/src/BuiltIn/ChangeLog b/src/BuiltIn/ChangeLog index e98b6b07..a97c6305 100755 --- a/src/BuiltIn/ChangeLog +++ b/src/BuiltIn/ChangeLog @@ -1,3 +1,15 @@ +2023-04-13 Steven Eker + + * minusSymbol.cc (MinusSymbol::attachData): use empty() + +===================================Maude144=========================================== + +2023-04-12 Steven Eker + + * bindingMacros.hh (NULL_DATA): use empty() + + * sortTestSymbol.cc (SortTestSymbol::makeLazyStrategy): use empty() + 2023-03-27 Steven Eker * stringOpSymbol.cc (StringOpSymbol::eqRewrite): don't use preallocate ctor diff --git a/src/BuiltIn/bindingMacros.hh b/src/BuiltIn/bindingMacros.hh index 62725bb4..fa71d8d3 100755 --- a/src/BuiltIn/bindingMacros.hh +++ b/src/BuiltIn/bindingMacros.hh @@ -77,7 +77,7 @@ #define NULL_DATA(purpose, className, data) \ if (strcmp(purpose, #className) == 0) \ { \ - return data.length() == 0; \ + return data.empty(); \ } #define BIND_SYMBOL(purpose, symbol, name, symbolType) \ diff --git a/src/BuiltIn/minusSymbol.cc b/src/BuiltIn/minusSymbol.cc index 43badaa7..613c9801 100644 --- a/src/BuiltIn/minusSymbol.cc +++ b/src/BuiltIn/minusSymbol.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-2023 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 @@ -64,7 +64,7 @@ MinusSymbol::attachData(const Vector& opDeclaration, { if (strcmp(purpose, "MinusSymbol") == 0) { - if (data.length() != 0) + if (!data.empty()) return false; Vector t(1); t[0] = "-"; diff --git a/src/BuiltIn/sortTestSymbol.cc b/src/BuiltIn/sortTestSymbol.cc index e9adf745..65b8de0f 100644 --- a/src/BuiltIn/sortTestSymbol.cc +++ b/src/BuiltIn/sortTestSymbol.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-2023 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 @@ -52,7 +52,7 @@ const Vector& SortTestSymbol::makeLazyStrategy() { static Vector lazyStrategy; - if (lazyStrategy.length() == 0) + if (lazyStrategy.empty()) lazyStrategy.append(0); return lazyStrategy; } diff --git a/src/Core/ChangeLog b/src/Core/ChangeLog index d3faacba..b5f9ac01 100644 --- a/src/Core/ChangeLog +++ b/src/Core/ChangeLog @@ -1,3 +1,17 @@ +2023-04-13 Steven Eker + + * preEquation.cc (PreEquation::checkCondition): use empty() + +2023-04-12 Steven Eker + + * connectedComponent.hh (class ConnectedComponent): Bool -> bool + + * strategy.hh (class Strategy): Bool -> bool + + * rewriteStrategy.cc (RewriteStrategy::RewriteStrategy): use empty() + +===================================Maude145=========================================== + 2023-03-28 Steven Eker * sortTable.cc (SortTable::buildSortDiagram): contractTo(0) -> clear() diff --git a/src/Core/connectedComponent.hh b/src/Core/connectedComponent.hh index 2e40b5b4..3bca84ee 100644 --- a/src/Core/connectedComponent.hh +++ b/src/Core/connectedComponent.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-2023 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 @@ -63,7 +63,7 @@ public: private: int sortCount; short nrMaxSorts; - Bool errorFreeFlag; + bool errorFreeFlag; Vector sorts; // // For new engine. diff --git a/src/Core/preEquation.cc b/src/Core/preEquation.cc index a2826853..c72f9686 100644 --- a/src/Core/preEquation.cc +++ b/src/Core/preEquation.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2020 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2023 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 @@ -150,7 +150,7 @@ PreEquation::checkCondition(bool findFirst, int& trialRef, Stack& state) const { - Assert(condition.length() != 0, "no condition"); + Assert(!condition.empty(), "no condition"); Assert(!findFirst || state.empty(), "non-empty condition state stack"); if (findFirst) trialRef = UNDEFINED; diff --git a/src/Core/rewriteStrategy.cc b/src/Core/rewriteStrategy.cc index d30bb9f1..9115f9fc 100644 --- a/src/Core/rewriteStrategy.cc +++ b/src/Core/rewriteStrategy.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-2023 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 @@ -51,7 +51,7 @@ RewriteStrategy::RewriteStrategy(int id, domain(domain), subjectSort(subjectSort), symbol(auxSymbol), - simple(domain.length() == 0) + simple(domain.empty()) { Assert(auxSymbol != 0, "null auxiliary symbol"); diff --git a/src/Core/strategy.hh b/src/Core/strategy.hh index 9546dfc1..b75c43dc 100644 --- a/src/Core/strategy.hh +++ b/src/Core/strategy.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-2023 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 @@ -46,8 +46,8 @@ protected: static const Vector standard; private: - Bool stdStrategy; - Bool unevalArgs; + bool stdStrategy; + bool unevalArgs; Vector strategy; NatSet eager; NatSet evaluated; diff --git a/src/FreeTheory/ChangeLog b/src/FreeTheory/ChangeLog index ff6f1db1..fb0b3faf 100755 --- a/src/FreeTheory/ChangeLog +++ b/src/FreeTheory/ChangeLog @@ -1,3 +1,80 @@ +2023-04-13 Steven Eker + + * freeSymbol.cc (FreeSymbol::newFreeSymbol): use empty() + +2023-04-12 Steven Eker + + * freeTerm.hh (class FreeTerm): Bool -> bool + + * freeTerm.cc (FreeTerm::arguments): use empty() + + * freeNet.cc (FreeNet::dump): use empty() + + * freeNet.hh (class FreeNet): make TestNode::symbolIndex an int; + make position an Index + (class FreeNet): TestNode::position an Index + + * freeNetExec.cc (FreeNet::applyReplace2): make diff an int rather + long + (FreeNet::applyReplaceFast2): make diff an int rather than long + (FreeNet::applyReplaceNoOwise2): make diff an int rather than long + + * freeRemainder.hh (FreeRemainder::fastMatchReplace): use range-based + for loop in place of FOR_EACH_CONST() (2 places) + (FreeRemainder::fastCheckAndBind): use range-based for loop in place + of FOR_EACH_CONST() (2 places) + (FreeRemainder::generalCheckAndBind): use range-based for loop in + place of FOR_EACH_CONST() (2 places) + +2023-04-11 Steven Eker + + * freeLhsCompiler.cc (FreeTerm::analyseConstraintPropagation): + use range-based for loop in place of FOR_EACH_CONST() + (FreeTerm::compileRemainder): use range-based for loop in place of + FOR_EACH_CONST() + (FreeTerm::compileLhs2): use range-based for loop in place of + FOR_EACH_CONST() + + * freeNet.cc (FreeNet::buildRemainders): use range-based for loop in + place of FOR_EACH_CONST() (2 places) + (FreeNet::dump): use range-based for loop in place of FOR_EACH_CONST() + + * freeTerm.cc (FreeTerm::partialCompareArguments): use range-based for + loop in place of FOR_EACH_CONST(); use size() rather than length() + (FreeTerm::computeMatchIndices): use range-based for loop in place of + FOR_EACH_CONST() + (FreeTerm::compileRhs3): use range-based for loop in place of + FOR_EACH_CONST() (2 places) + + * freePreNet.cc (FreePreNet::buildNet): replaced commented out cerr << + statements with DebugEnter()/DebugInfo()/DebugExit() + (FreePreNet::buildNet): use range-based for loop in place of + FOR_EACH_CONST() + (FreePreNet::reduceFringe): use range-based for loop in place of + FOR_EACH_CONST() + (FreePreNet::findLiveSet): use range-based for loop in place of + FOR_EACH_CONST() + (FreePreNet::partitionLiveSet): use range-based for loop in place of + FOR_EACH_CONST() (3 places) + (FreePreNet::partiallySubsumed): use range-based for loop in place of + FOR_EACH_CONST() + (FreePreNet::findBestPosition): use range-based for loop in place of + FOR_EACH_CONST() + (FreePreNet::dumpLiveSet): use range-based for loop in place of + FOR_EACH_CONST() + (FreePreNet::makeNode): replaced commented out cerr << statement with + DebugEnter() + + * freePreNetSemiCompiler.cc (FreePreNet::setVisitedFlags): use range-based + for loop in place of FOR_EACH_CONST() + (FreePreNet::allocateSlot): use range-based for loop in place of + FOR_EACH_CONST() + + * freeRhsAutomaton.cc (FreeRhsAutomaton::recordInfo): use range-based for + loop in place of FOR_EACH_CONST() + +===================================Maude145=========================================== + 2023-03-14 Steven Eker * freeDagNode.hh (class FreeDagNode): union Word deleted; use diff --git a/src/FreeTheory/freeLhsCompiler.cc b/src/FreeTheory/freeLhsCompiler.cc index 7cefe770..c47df9f7 100644 --- a/src/FreeTheory/freeLhsCompiler.cc +++ b/src/FreeTheory/freeLhsCompiler.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2009 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2023 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 @@ -45,15 +45,15 @@ FreeTerm::analyseConstraintPropagation(NatSet& boundUniquely) const // that lie directly under the free skeleton and thus will receive an unique binding. // Vector nonGroundAliens; - FOR_EACH_CONST(i, Vector, otherSymbols) + for (const FreeOccurrence& i : otherSymbols) { - Term* t = i->term(); + Term* t = i.term(); if (VariableTerm* v = dynamic_cast(t)) boundUniquely.insert(v->getIndex()); else { if (!(t->ground())) - nonGroundAliens.append(*i); + nonGroundAliens.append(i); } } if (!(nonGroundAliens.empty())) @@ -88,26 +88,26 @@ FreeTerm::compileRemainder(Equation* equation, const Vector& slotTranslatio Vector groundAliens; // ground alien subterms Vector nonGroundAliens; // non-ground alien subterms NatSet boundUniquely; - FOR_EACH_CONST(i, Vector, otherSymbols) + for (const FreeOccurrence& i : otherSymbols) { - Term* t = i->term(); + Term* t = i.term(); if (VariableTerm* v = dynamic_cast(t)) { int index = v->getIndex(); if (boundUniquely.contains(index)) - boundVariables.append(*i); + boundVariables.append(i); else { boundUniquely.insert(index); - freeVariables.append(*i); + freeVariables.append(i); } } else { if (t->ground()) - groundAliens.append(*i); + groundAliens.append(i); else - nonGroundAliens.append(*i); + nonGroundAliens.append(i); } } CP_Sequence bestSequence; @@ -152,26 +152,26 @@ FreeTerm::compileLhs2(bool /* matchAtTop */, Vector uncertainVariables; // status when matched against uncertain Vector groundAliens; // ground alien subterms Vector nonGroundAliens; // non-ground alien subterms - FOR_EACH_CONST(i, Vector, otherSymbols) + for (const FreeOccurrence& i : otherSymbols) { - Term* t = i->term(); + Term* t = i.term(); if (VariableTerm* v = dynamic_cast(t)) { int index = v->getIndex(); if (boundUniquely.contains(index)) - boundVariables.append(*i); + boundVariables.append(i); else { boundUniquely.insert(index); - uncertainVariables.append(*i); + uncertainVariables.append(i); } } else { if (t->ground()) - groundAliens.append(*i); + groundAliens.append(i); else - nonGroundAliens.append(*i); + nonGroundAliens.append(i); } } CP_Sequence bestSequence; diff --git a/src/FreeTheory/freeNet.cc b/src/FreeTheory/freeNet.cc index fdc24f9c..928fb79f 100755 --- a/src/FreeTheory/freeNet.cc +++ b/src/FreeTheory/freeNet.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-2023 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 @@ -149,13 +149,13 @@ FreeNet::buildRemainders(const Vector& equations, remainders.expandTo(nrEquations); for (int i = 0; i < nrEquations; i++) remainders[i] = 0; - FOR_EACH_CONST(i, PatternSet, patternsUsed) + for (int i : patternsUsed) { - Equation* e = equations[*i]; + Equation* e = equations[i]; if (FreeTerm* f = dynamic_cast(e->getLhs())) { FreeRemainder* r = f->compileRemainder(e, slotTranslation); - remainders[*i] = r; + remainders[i] = r; // // If a remainder doesn't have fast handling, neither can the discrimination net. // @@ -164,7 +164,7 @@ FreeNet::buildRemainders(const Vector& equations, } else { - remainders[*i] = new FreeRemainder(e); // remainder for "foreign" equation + remainders[i] = new FreeRemainder(e); // remainder for "foreign" equation fast = false; // a foreign equation always disables fast handling for the net } } @@ -179,8 +179,8 @@ FreeNet::buildRemainders(const Vector& equations, Vector& rems = fastApplicable[i]; rems.resize(liveSet.size() + 1); Vector::iterator r = rems.begin(); - FOR_EACH_CONST(j, PatternSet, liveSet) - *r++ = remainders[*j]; + for (int j : liveSet) + *r++ = remainders[j]; *r = 0; } } @@ -264,7 +264,7 @@ FreeNet::moreImportant(Symbol* first, Symbol* second) void FreeNet::dump(ostream& s, int indentLevel) { - if (applicable.length() == 0) + if (applicable.empty()) { s << Indent(indentLevel) << "Empty FreeNet\n"; return; @@ -290,8 +290,8 @@ FreeNet::dump(ostream& s, int indentLevel) for (int i = 0; i < applicable.length(); i++) { s << Indent(indentLevel) << "Applicable sequence " << -1 - i << ':'; - FOR_EACH_CONST(j, PatternSet, applicable[i]) - s << ' ' << *j; + for (int j : applicable[i]) + s << ' ' << j; s << '\n'; } diff --git a/src/FreeTheory/freeNet.hh b/src/FreeTheory/freeNet.hh index 02fb2be6..9a9c03fc 100755 --- a/src/FreeTheory/freeNet.hh +++ b/src/FreeTheory/freeNet.hh @@ -76,12 +76,15 @@ private: GREATER = 0 }; + // + // This is the data structure most accessed in the critical loops. + // struct TestNode { int notEqual[2]; // index of next test node to take for > and < cases (-ve encodes index of applicable list, 0 encodes failure) - int position; // stack slot to get free dagnode argument list from (-1 indicates use old argument) + Index position; // stack slot to get free dagnode argument list from (-1 indicates use old argument) int argIndex; // index of argument to test - long symbolIndex; // index within module of symbol we test against + int symbolIndex; // index within module of symbol we test against int slot; // index of stack slot to store free dagnode argument list in (-1 indicates do not store) int equal; // index of next test node to take for == case (-ve encode index of applicable list) @@ -90,28 +93,6 @@ private: #endif }; - /* - struct TestNode - { - int symbolIndex; // index within module of symbol we test against - // - //QUICK HACK - //int position; // stack slot to get free dagnode argument list from (-1 indicates use old argument) - //int slot; // index of stack slot to store free dagnode argument list in (-1 indicates do not store) - - short position; // stack slot to get free dagnode argument list from (-1 indicates use old argument) - short slot; // index of stack slot to store free dagnode argument list in (-1 indicates do not store) - int argIndex; // index of argument to test - int equal; // index of next test node to take for == case (-ve encode index of applicable list) - long notEqual[2]; // index of next test node to take for > and < cases (-ve encodes index of applicable list, 0 encodes failure) - -#if SIZEOF_LONG == 4 // 32-bit machines - int pad_struct_to_32_bytes; - int on_32_bit_machines; -#endif - }; - */ - struct Triple { Symbol* symbol; diff --git a/src/FreeTheory/freeNetExec.cc b/src/FreeTheory/freeNetExec.cc index 4dfbafc9..5da4a083 100755 --- a/src/FreeTheory/freeNetExec.cc +++ b/src/FreeTheory/freeNetExec.cc @@ -48,7 +48,7 @@ FreeNet::applyReplace2(DagNode* subject, RewritingContext& context) for (;;) { long p; - long diff = symbolIndex - n->symbolIndex; + int diff = symbolIndex - n->symbolIndex; if (diff != 0) { i = n->notEqual[diff < 0]; @@ -120,7 +120,7 @@ FreeNet::applyReplaceFast2(DagNode* subject, RewritingContext& context) for (;;) { long p; - long diff = symbolIndex - n->symbolIndex; + int diff = symbolIndex - n->symbolIndex; if (diff != 0) { i = n->notEqual[diff < 0]; @@ -189,7 +189,7 @@ FreeNet::applyReplaceNoOwise2(DagNode* subject, RewritingContext& context) for (;;) { long p; - long diff = symbolIndex - n->symbolIndex; + int diff = symbolIndex - n->symbolIndex; if (diff != 0) { i = n->notEqual[diff < 0]; diff --git a/src/FreeTheory/freePreNet.cc b/src/FreeTheory/freePreNet.cc index ce2b82b3..5447b277 100755 --- a/src/FreeTheory/freePreNet.cc +++ b/src/FreeTheory/freePreNet.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-2023 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 @@ -83,7 +83,7 @@ FreePreNet::FreePreNet(bool expandRemainderNodes) void FreePreNet::buildNet(FreeSymbol* symbol) { - //cout << "buildNet for " << symbol << endl; + DebugEnter("for " << symbol); topSymbol = symbol; nrFailParents = 0; nrFailVisits = 0; @@ -91,9 +91,7 @@ FreePreNet::buildNet(FreeSymbol* symbol) int nrEquations = equations.length(); if (nrEquations == 0) return; - - //cout << "nrEquations = " << nrEquations << endl; - + DebugInfo("nrEquations = " << nrEquations); patterns.expandTo(nrEquations); LiveSet liveSet; LiveSet potentialSubsumers; @@ -103,9 +101,9 @@ FreePreNet::buildNet(FreeSymbol* symbol) Equation* e = equations[i]; Term* p = e->getLhs(); patterns[i].term = p; - FOR_EACH_CONST(j, LiveSet, potentialSubsumers) + for (int j : potentialSubsumers) { - if (patterns[*j].term->subsumes(p, false)) + if (patterns[j].term->subsumes(p, false)) { DebugAdvisory(e << " subsumed"); goto subsumedAtTop; @@ -142,7 +140,7 @@ FreePreNet::buildNet(FreeSymbol* symbol) NatSet positionsTested; (void) makeNode(liveSet, fringe, positionsTested); // dump(cerr, 0); - //cout << "buildNet for " << symbol << " done; nodes = " << net.size() << endl; + DebugExit("for " << symbol << " done; nodes = " << net.size()); } int @@ -150,7 +148,7 @@ FreePreNet::makeNode(const LiveSet& liveSet, const NatSet& reducedFringe, const NatSet& positionsTested) { - //cerr << "liveSet has " << liveSet.size() << " patterns" << endl; + DebugEnter("liveSet has " << liveSet.size() << " patterns"); // // First check to see if there is already a node with the same set // of live patterns and the same reduced fringe that we can share. @@ -318,9 +316,9 @@ FreePreNet::reduceFringe(const LiveSet& liveSet, NatSet& fringe) const // // See if at least one live pattern has a stable symbol at this position. // - FOR_EACH_CONST(j, LiveSet, liveSet) + for (int j : liveSet) { - if (FreeTerm* f = dynamic_cast(patterns[*j].term)) + if (FreeTerm* f = dynamic_cast(patterns[j].term)) { if (Term* t = f->locateSubterm(position)) { @@ -343,10 +341,9 @@ FreePreNet::findLiveSet(const LiveSet& original, LiveSet& liveSet) { const Vector position(positions.index2Position(positionIndex)); // deep copy - because ref become stale - - FOR_EACH_CONST(i, LiveSet, original) + + for (int patternIndex : original) { - int patternIndex = *i; if (FreeTerm* f = dynamic_cast(patterns[patternIndex].term)) { if (Term* t = f->locateSubterm(position)) @@ -389,9 +386,8 @@ FreePreNet::partitionLiveSet(const LiveSet& original, { const Vector& position = positions.index2Position(positionIndex); // safe because we won't add new positions - FOR_EACH_CONST(i, LiveSet, original) + for (int patternIndex : original) { - int patternIndex = *i; if (FreeTerm* f = dynamic_cast(patterns[patternIndex].term)) { if (Term* t = f->locateSubterm(position)) @@ -409,9 +405,9 @@ FreePreNet::partitionLiveSet(const LiveSet& original, // Need to consider pattern for the live set of each active // symbol that could match our unstable subpattern. // - FOR_EACH_CONST(j, Vector, arcs) + for (const Arc& j : arcs) { - Symbol* symbol = j->label; + Symbol* symbol = j.label; if (symbol->mightMatchPattern(t)) liveSets[symbol->getIndexWithinModule()].insert(patternIndex); } @@ -424,8 +420,8 @@ FreePreNet::partitionLiveSet(const LiveSet& original, // Either way we add it to all live sets. // defaultLiveSet.insert(patternIndex); - FOR_EACH_CONST(j, Vector, arcs) - liveSets[j->label->getIndexWithinModule()].insert(patternIndex); + for (const Arc& j : arcs) + liveSets[j.label->getIndexWithinModule()].insert(patternIndex); } } @@ -437,11 +433,11 @@ FreePreNet::partiallySubsumed(const LiveSet& liveSet, if (liveSet.empty()) return false; Term* vp = patterns[victim].term; - FOR_EACH_CONST(i, LiveSet, liveSet) + for (int i : liveSet) { - Assert(*i < victim, "current liveSet contains pattern >= victim"); - if ((patterns[*i].flags & SUBSUMER) && - subsumesWrtReducedFringe(patterns[*i].term, vp, topPositionIndex, fringe)) + Assert(i < victim, "current liveSet contains pattern >= victim"); + if ((patterns[i].flags & SUBSUMER) && + subsumesWrtReducedFringe(patterns[i].term, vp, topPositionIndex, fringe)) return true; } return false; @@ -473,9 +469,9 @@ FreePreNet::findBestPosition(const NodeIndex& ni, NodeBody& n) const // Gather the set of symbols that occur at this position // in a live pattern. // - FOR_EACH_CONST(j, LiveSet, ni.liveSet) + for (int j : ni.liveSet) { - if (FreeTerm* f = dynamic_cast(patterns[*j].term)) + if (FreeTerm* f = dynamic_cast(patterns[j].term)) { Term* t = f->locateSubterm(path); if (t != 0 && t->stable()) @@ -483,7 +479,7 @@ FreePreNet::findBestPosition(const NodeIndex& ni, NodeBody& n) const ++nrStable; symbols.insert(t->symbol()); } - else if (nrStable == 0 && patterns[*j].flags & SUBSUMER) + else if (nrStable == 0 && patterns[j].flags & SUBSUMER) ++nrUnstableSubsumersAbove; } ++nrLive; @@ -677,13 +673,13 @@ FreePreNet::dumpLiveSet(ostream& s, const LiveSet& liveSet) else { bool first = true; - FOR_EACH_CONST(j, LiveSet, liveSet) + for (int j : liveSet) { if (first) first = false; else s << ", "; - s << *j; + s << j; } } } diff --git a/src/FreeTheory/freePreNetSemiCompiler.cc b/src/FreeTheory/freePreNetSemiCompiler.cc index 1081f8d4..3f8dff48 100644 --- a/src/FreeTheory/freePreNetSemiCompiler.cc +++ b/src/FreeTheory/freePreNetSemiCompiler.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-2023 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 @@ -121,9 +121,9 @@ FreePreNet::setVisitedFlags(const LiveSet& liveSet, const Vector& position, bool state) { - FOR_EACH_CONST(i, LiveSet, liveSet) + for (int i : liveSet) { - if (FreeTerm* f = dynamic_cast(patterns[*i].term)) + if (FreeTerm* f = dynamic_cast(patterns[i].term)) { Term* t = f->locateSubterm(position); if (t != 0 && (f = dynamic_cast(t)) != 0) @@ -143,10 +143,9 @@ FreePreNet::allocateSlot(const LiveSet& liveSet, "slot/conflict data structures out of sync"); // cerr << symbol << endl; - FOR_EACH_CONST(i, LiveSet, liveSet) + for (int patternIndex : liveSet) { // cerr << patterns[*i].term << endl; - int patternIndex = *i; Term* pattern = patterns[patternIndex].term; if (FreeTerm* f = dynamic_cast(pattern)) { diff --git a/src/FreeTheory/freeRemainder.hh b/src/FreeTheory/freeRemainder.hh index 4a12cbcb..fd7587dc 100755 --- a/src/FreeTheory/freeRemainder.hh +++ b/src/FreeTheory/freeRemainder.hh @@ -102,6 +102,12 @@ FreeRemainder::fastHandling() const return fast != 0; } +inline bool +FreeRemainder::isOwise() const +{ + return equation->isOwise(); +} + inline bool FreeRemainder::fastMatchReplace(DagNode* subject, RewritingContext& context, @@ -112,22 +118,22 @@ FreeRemainder::fastMatchReplace(DagNode* subject, if (fast > 0) { Vector::const_iterator stackBase = stack.begin(); - FOR_EACH_CONST(i, Vector, freeVariables) + for (const FreeVariable& i : freeVariables) { - DagNode* d = stackBase[i->position][i->argIndex]; + DagNode* d = stackBase[i.position][i.argIndex]; Assert(d->getSortIndex() != Sort::SORT_UNKNOWN, "missing sort information"); - context.bind(i->varIndex, d); + context.bind(i.varIndex, d); } } else if (fast < 0) { Vector::const_iterator stackBase = stack.begin(); - FOR_EACH_CONST(i, Vector, freeVariables) + for (const FreeVariable& i : freeVariables) { - DagNode* d = stackBase[i->position][i->argIndex]; + DagNode* d = stackBase[i.position][i.argIndex]; Assert(d->getSortIndex() != Sort::SORT_UNKNOWN, "missing sort information"); - if (d->fastLeq(i->sort)) - context.bind(i->varIndex, d); + if (d->fastLeq(i.sort)) + context.bind(i.varIndex, d); else return false; } @@ -143,12 +149,6 @@ slow: return slowMatchReplace(subject, context, stack); } -inline bool -FreeRemainder::isOwise() const -{ - return equation->isOwise(); -} - inline bool FreeRemainder::fastCheckAndBind(DagNode** binding, Vector& stack) const { @@ -161,12 +161,12 @@ FreeRemainder::fastCheckAndBind(DagNode** binding, Vector& stack) con // // Super-fast case: bind variables without sort check. // - FOR_EACH_CONST(i, Vector, freeVariables) + for (const FreeVariable& i : freeVariables) { - DagNode* d = stackBase[i->position][i->argIndex]; + DagNode* d = stackBase[i.position][i.argIndex]; Assert(d->getSortIndex() != Sort::SORT_UNKNOWN, "missing sort information"); - Assert(d->leq(i->sort), "super-fast case fails sort check"); - binding[i->varIndex] = d; + Assert(d->leq(i.sort), "super-fast case fails sort check"); + binding[i.varIndex] = d; } } else @@ -175,12 +175,12 @@ FreeRemainder::fastCheckAndBind(DagNode** binding, Vector& stack) con // // Fast case: bind variables after fast sort check. // - FOR_EACH_CONST(i, Vector, freeVariables) + for (const FreeVariable& i : freeVariables) { - DagNode* d = stackBase[i->position][i->argIndex]; + DagNode* d = stackBase[i.position][i.argIndex]; Assert(d->getSortIndex() != Sort::SORT_UNKNOWN, "missing sort information"); - if (d->fastLeq(i->sort)) - binding[i->varIndex] = d; + if (d->fastLeq(i.sort)) + binding[i.varIndex] = d; else return false; } @@ -204,12 +204,12 @@ FreeRemainder::generalCheckAndBind(DagNode** binding, Vector& stack) // // Super-fast case: bind variables without sort check. // - FOR_EACH_CONST(i, Vector, freeVariables) + for (const FreeVariable& i : freeVariables) { - DagNode* d = stackBase[i->position][i->argIndex]; + DagNode* d = stackBase[i.position][i.argIndex]; Assert(d->getSortIndex() != Sort::SORT_UNKNOWN, "missing sort information"); - Assert(d->leq(i->sort), "super-fast case fails sort check"); - binding[i->varIndex] = d; + Assert(d->leq(i.sort), "super-fast case fails sort check"); + binding[i.varIndex] = d; } } else if (fast < 0) @@ -217,12 +217,12 @@ FreeRemainder::generalCheckAndBind(DagNode** binding, Vector& stack) // // Fast case: bind variables after fast sort check. // - FOR_EACH_CONST(i, Vector, freeVariables) + for (const FreeVariable& i : freeVariables) { - DagNode* d = stackBase[i->position][i->argIndex]; + DagNode* d = stackBase[i.position][i.argIndex]; Assert(d->getSortIndex() != Sort::SORT_UNKNOWN, "missing sort information"); - if (d->fastLeq(i->sort)) - binding[i->varIndex] = d; + if (d->fastLeq(i.sort)) + binding[i.varIndex] = d; else return false; } diff --git a/src/FreeTheory/freeRhsAutomaton.cc b/src/FreeTheory/freeRhsAutomaton.cc index 8ad0b496..ed6bb4eb 100755 --- a/src/FreeTheory/freeRhsAutomaton.cc +++ b/src/FreeTheory/freeRhsAutomaton.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-2023 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 @@ -63,8 +63,8 @@ FreeRhsAutomaton::addFree(Symbol* symbol, bool FreeRhsAutomaton::recordInfo(StackMachineRhsCompiler& compiler) { - FOR_EACH_CONST(i, Vector, instructions) - compiler.recordFunctionEval(i->symbol, i->destination, i->sources); + for (const Instruction& i : instructions) + compiler.recordFunctionEval(i.symbol, i.destination, i.sources); return true; } diff --git a/src/FreeTheory/freeSymbol.cc b/src/FreeTheory/freeSymbol.cc index 387ff421..5ef8da36 100755 --- a/src/FreeTheory/freeSymbol.cc +++ b/src/FreeTheory/freeSymbol.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-2023 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 @@ -78,7 +78,7 @@ FreeSymbol::newFreeSymbol(int id, int arity, const Vector& strategy, bool m { if (arity <= 3) { - if (memoFlag || strategy.length() != 0) + if (memoFlag || !strategy.empty()) { FreeSymbol* t = new FreeSymbol(id, arity, strategy, memoFlag); if (!(t->standardStrategy())) diff --git a/src/FreeTheory/freeTerm.cc b/src/FreeTheory/freeTerm.cc index 05679cc8..26262599 100755 --- a/src/FreeTheory/freeTerm.cc +++ b/src/FreeTheory/freeTerm.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-2023 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 @@ -103,7 +103,7 @@ FreeTerm::~FreeTerm() RawArgumentIterator* FreeTerm::arguments() { - if (argArray.length() == 0) + if (argArray.empty()) return 0; else return new FreeArgumentIterator(&argArray); @@ -198,17 +198,16 @@ FreeTerm::compareArguments(const DagNode* other) const } int -FreeTerm::partialCompareArguments(const Substitution& partialSubstitution, - DagNode* other) const +FreeTerm::partialCompareArguments(const Substitution& partialSubstitution, DagNode* other) const { Assert(symbol() == other->symbol(), "symbols differ"); - int nrArgs = argArray.length(); + int nrArgs = argArray.size(); if (nrArgs != 0) { DagNode** da = safeCast(FreeDagNode*, other)->argArray(); - FOR_EACH_CONST(i, Vector, argArray) + for (Term* t : argArray) { - int r = (*i)->partialCompare(partialSubstitution, *da); + int r = t->partialCompare(partialSubstitution, *da); if (r != EQUAL) return r; ++da; @@ -250,9 +249,8 @@ FreeTerm::computeMatchIndices() const // Make sure each stable symbol at the top of one of our arguments has // a non-zero match index. This is done recursively. // - FOR_EACH_CONST(i, Vector, argArray) + for (Term* t : argArray) { - Term* t = *i; Symbol* s = t->symbol(); if (s->isStable() && s->getMatchIndex() == 0) s->setMatchIndex(s->rangeComponent()->getNewMatchIndex()); @@ -518,9 +516,9 @@ FreeTerm::compileRhs3(FreeRhsAutomaton* automaton, // FreeSymbol* s = symbol(); Vector sources(nrArgs); - FOR_EACH_CONST(i, PairVec, order) + for (const auto& p : order) { - int argNr = i->second; + int argNr = p.second; bool argEager = eagerContext && s->eagerArgument(argNr); Term* t = argArray[argNr]; if (FreeTerm* f = dynamic_cast(t)) @@ -549,10 +547,8 @@ FreeTerm::compileRhs3(FreeRhsAutomaton* automaton, // // Need to flag last use of each source. // - { - FOR_EACH_CONST(i, Vector, sources) - variableInfo.useIndex(*i); - } + for (int i : sources) + variableInfo.useIndex(i); // // Add to free step to automaton. // diff --git a/src/FreeTheory/freeTerm.hh b/src/FreeTheory/freeTerm.hh index 5c1f3896..ccc64231 100755 --- a/src/FreeTheory/freeTerm.hh +++ b/src/FreeTheory/freeTerm.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-2023 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 @@ -89,7 +89,7 @@ public: // Gross hack to allow surgery on free theory terms from ouside of the theory. // Only safe if there has been no processing on the term. // Garbage collection of the old argument (parts of which the caller - // may have reused in newArgument) is the callers responsibility. + // may have reused in newArgument) is the caller's responsibility. // Term* replaceArgument(Index index, Term* newArgument); @@ -129,7 +129,7 @@ private: Vector argArray; short slotIndex; - Bool visitedFlag; + bool visitedFlag; }; inline FreeSymbol* diff --git a/src/Higher/ChangeLog b/src/Higher/ChangeLog index 02899186..e288e21c 100755 --- a/src/Higher/ChangeLog +++ b/src/Higher/ChangeLog @@ -1,3 +1,9 @@ +2023-04-12 Steven Eker + + * searchState.cc (SearchState::initSubstitution): use empty() + +===================================Maude145=========================================== + 2023-03-28 Steven Eker * satSolverSymbol.cc (makeFormulaList): contractTo(0) -> clear() diff --git a/src/Higher/searchState.cc b/src/Higher/searchState.cc index 9a3788e2..997aab3e 100644 --- a/src/Higher/searchState.cc +++ b/src/Higher/searchState.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-2023 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 @@ -143,7 +143,7 @@ SearchState::findNextSolution() bool SearchState::initSubstitution(const VariableInfo& varInfo) { - if (substVariables.length() == 0) + if (substVariables.empty()) return varInfo.getUnboundVariables().empty(); int nrUserVars = substVariables.length(); int nrVars = varInfo.getNrRealVariables(); diff --git a/src/IO_Stuff/ChangeLog b/src/IO_Stuff/ChangeLog index 0d6a60b7..8952017e 100644 --- a/src/IO_Stuff/ChangeLog +++ b/src/IO_Stuff/ChangeLog @@ -1,3 +1,9 @@ +2023-04-12 Steven Eker + + * autoWrapBuffer.hh (class AutoWrapBuffer): Bool -> bool + +===================================Maude145=========================================== + 2021-04-02 Steven Eker * IO_Manager.hh (IO_Manager::safeToAccessStdin) diff --git a/src/IO_Stuff/autoWrapBuffer.hh b/src/IO_Stuff/autoWrapBuffer.hh index b7a1002b..c679c6aa 100644 --- a/src/IO_Stuff/autoWrapBuffer.hh +++ b/src/IO_Stuff/autoWrapBuffer.hh @@ -82,11 +82,11 @@ private: WaitFunction waitFunction; int cursorPosition; // cursor position if we were to print pendingBuffer - Bool seenBackQuote; // last char was a ` - Bool seenBackSlash; // inside a "string" and last char was an unescaped + bool seenBackQuote; // last char was a ` + bool seenBackSlash; // inside a "string" and last char was an unescaped // backslash - Bool inString; // inside a "string" - Bool inEscape; // inside an ESC sequence + bool inString; // inside a "string" + bool inEscape; // inside an ESC sequence string pendingBuffer; int pendingWidth; // number of chars in buffer excluding \t and ESC sequences }; diff --git a/src/Meta/ChangeLog b/src/Meta/ChangeLog index 7c281ee3..d19cd7f8 100644 --- a/src/Meta/ChangeLog +++ b/src/Meta/ChangeLog @@ -1,3 +1,11 @@ +2023-04-12 Steven Eker + + * miSort.cc (InterpreterManagerSymbol::getMinimalSorts): use empty() + + * descentFunctions.cc (MetaLevelOpSymbol::metaMinimalSorts): use empty() + +===================================Maude145=========================================== + 2023-03-28 Steven Eker * metaModuleCache.cc (MetaModuleCache::flush): contractTo(0) -> clear() diff --git a/src/Meta/descentFunctions.cc b/src/Meta/descentFunctions.cc index b2185c51..8ac46ffe 100644 --- a/src/Meta/descentFunctions.cc +++ b/src/Meta/descentFunctions.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-2023 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 @@ -251,7 +251,7 @@ MetaLevelOpSymbol::metaMinimalSorts(FreeDagNode* subject, RewritingContext& cont for (int i = 1; i < nrSorts; i++) { Sort* s = component->sort(i); - if (s->getSubsorts().length() == 0) + if (s->getSubsorts().empty()) minimalSorts.append(s); } return context.builtInReplace(subject, metaLevel->upSortSet(minimalSorts)); diff --git a/src/Meta/miSort.cc b/src/Meta/miSort.cc index 0ef48b0c..1aa87079 100644 --- a/src/Meta/miSort.cc +++ b/src/Meta/miSort.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2020 SRI International, Menlo Park, CA 94025, USA. + Copyright 2023 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 @@ -102,7 +102,7 @@ InterpreterManagerSymbol::getMinimalSorts(FreeDagNode* message, for (int i = 1; i < nrSorts; i++) { Sort* s = component->sort(i); - if (s->getSubsorts().length() == 0) + if (s->getSubsorts().empty()) minimalSorts.append(s); } diff --git a/src/Mixfix/ChangeLog b/src/Mixfix/ChangeLog index 4ade4e8e..aa05686b 100644 --- a/src/Mixfix/ChangeLog +++ b/src/Mixfix/ChangeLog @@ -1,3 +1,66 @@ +2023-04-13 Steven Eker + + * banner.cc (printBanner): adjust indentation for 3.3.1 + + * modules.yy (toAttribute): overparse latex attribute without string + (attribute): overparse latex attribute without string + + * termPrint.cc (MixfixModule::prettyPrint): use empty() + + * loopMode.cc (Interpreter::contLoop): use empty() + + * bufferPrint.cc (MixfixModule::prettyPrint): use empty() + + * fixUp.cc (SyntacticPreModule::fixUpSymbol): use empty() + (SyntacticPreModule::fixUpPolymorph): use empty() + + * dagNodePrint.cc (MixfixModule::prettyPrint): use empty() + +2023-04-12 Steven Eker + + * syntacticPreModule.hh (class SyntacticPreModule): Bool -> bool + + * entry.cc (MixfixModule::addOpDeclaration): use empty() + (MixfixModule::addPolymorph): use empty() + +2023-04-11 Steven Eker + + * quotedIdentifierSymbol.cc (QuotedIdentifierSymbol::attachData): use + empty() + + * loopSymbol.cc (LoopSymbol::attachData): use empty() + + * ops.cc (SyntacticPreModule::makeDeclsConsistent): use empty() (2 places) + + * modules.yy (attribute): overparse prec/gather/format/strat/strategy/poly + attributes without required information + (toAttribute): overparse prec/gather/format attributes without required + information + (moduleExprDot): use Token* version of operator<<() + (skipStrayArrow): use Token* version of operator<<() + (parameter): use Token* version of operator<<() + (declaration): use Token* version of operator<<() + (skipStrayColon): use Token* version of operator<<() + (domainRangeAttr): use Token* version of operator<<(); use $1 rather than + lineNumber + (viewStratMap): use Token* version of operator<<() + + * token.hh: added decl for Token* version of operator<<() + + * token.cc (operator<<): added Token* version + + * interact.cc (UserLevelRewritingContext::internalErrorHandler): call + exit() rather than _exit() to avoid losing message on Macs + (UserLevelRewritingContext::stackOverflowHandler): call exit() rather + than _exit() to avoid losing message on Macs + +2023-04-10 Steven Eker + + * interact.cc (UserLevelRewritingContext::stackOverflowHandler): fix + grammar in message + +===================================Maude145=========================================== + 2023-04-07 Steven Eker * instantiateModuleWithFreeParameters.cc diff --git a/src/Mixfix/banner.cc b/src/Mixfix/banner.cc index caca6839..226325fa 100644 --- a/src/Mixfix/banner.cc +++ b/src/Mixfix/banner.cc @@ -53,7 +53,7 @@ printBanner(std::ostream& s) Tty(Tty::GREEN) << 'e' << Tty(Tty::RESET) << " ---\n"; s << "\t\t /||||||||||||||||||\\\n"; - s << "\t " << PACKAGE_STRING << " built: " << + s << "\t " << PACKAGE_STRING << " built: " << __DATE__ << ' ' << __TIME__ << '\n'; s << "\t Copyright 1997-2023 SRI International\n"; s << "\t\t " << ctime(&secs); diff --git a/src/Mixfix/bufferPrint.cc b/src/Mixfix/bufferPrint.cc index 436fcd1f..eabe638e 100644 --- a/src/Mixfix/bufferPrint.cc +++ b/src/Mixfix/bufferPrint.cc @@ -322,8 +322,7 @@ MixfixModule::prettyPrint(Vector& buffer, int nrArgs = symbol->arity(); prefix(buffer, needDisambig); - if (((printFlags & Interpreter::PRINT_MIXFIX) && si.mixfixSyntax.length() != 0) || - (basicType == SymbolType::SORT_TEST)) + if (((printFlags & Interpreter::PRINT_MIXFIX) && !si.mixfixSyntax.empty()) || (basicType == SymbolType::SORT_TEST)) { // // Mixfix case. diff --git a/src/Mixfix/dagNodePrint.cc b/src/Mixfix/dagNodePrint.cc index 33f6b719..1936c506 100644 --- a/src/Mixfix/dagNodePrint.cc +++ b/src/Mixfix/dagNodePrint.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2014 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2023 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 @@ -394,7 +394,7 @@ MixfixModule::prettyPrint(ostream& s, if (needDisambig) s << '('; bool printConceal = interpreter.concealedSymbol(symbol); - if ((interpreter.getPrintFlag(Interpreter::PRINT_MIXFIX) && si.mixfixSyntax.length() != 0 && !printConceal) || + if ((interpreter.getPrintFlag(Interpreter::PRINT_MIXFIX) && !si.mixfixSyntax.empty() && !printConceal) || (basicType == SymbolType::SORT_TEST)) { // diff --git a/src/Mixfix/entry.cc b/src/Mixfix/entry.cc index 17f58d2d..2d102a21 100644 --- a/src/Mixfix/entry.cc +++ b/src/Mixfix/entry.cc @@ -421,7 +421,7 @@ MixfixModule::addOpDeclaration(Token prefixName, symbolInfo.expandBy(1); SymbolInfo& si = symbolInfo[nrSymbols]; int nrUnderscores = Token::extractMixfix(name, si.mixfixSyntax); - if (si.mixfixSyntax.length() == 0) + if (si.mixfixSyntax.empty()) { si.prec = 0; WarningCheck(!(symbolType.hasFlag(SymbolType::PREC)), @@ -646,7 +646,7 @@ MixfixModule::addPolymorph(Token prefixName, p.identity = 0; p.metadata = metadata; int nrUnderscores = Token::extractMixfix(prefixName.code(), p.symbolInfo.mixfixSyntax); - if (p.symbolInfo.mixfixSyntax.length() == 0) + if (p.symbolInfo.mixfixSyntax.empty()) { p.symbolInfo.prec = 0; WarningCheck(!(symbolType.hasFlag(SymbolType::PREC)), diff --git a/src/Mixfix/fixUp.cc b/src/Mixfix/fixUp.cc index 09eac4af..4be07214 100644 --- a/src/Mixfix/fixUp.cc +++ b/src/Mixfix/fixUp.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-2023 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 @@ -189,7 +189,7 @@ SyntacticPreModule::fixUpSymbol(const OpDecl& opDecl) // // Might not have an identity to parse if it is a ditto declaration. // - if (opDef.identity.length() != 0) + if (!opDef.identity.empty()) { // // The validation of attributes in the flattened module may have @@ -263,7 +263,7 @@ SyntacticPreModule::fixUpPolymorph(const OpDecl& opDecl) // // Might not have an identity to parse if it is a ditto declaration. // - if (opDef.identity.length() != 0) + if (!opDef.identity.empty()) { // // The validation of attributes in the flattened module may have diff --git a/src/Mixfix/interact.cc b/src/Mixfix/interact.cc index e03d36b3..7aa49dbd 100644 --- a/src/Mixfix/interact.cc +++ b/src/Mixfix/interact.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2022 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2023 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 @@ -160,7 +160,7 @@ UserLevelRewritingContext::stackOverflowHandler(int emergency, stackoverflow_con // static char message[] = "\nFatal error: stack overflow.\n\ This can happen because you have an infinite computation, say a runaway\n\ -recursion, or model checking an infinite model. It can also happen because\n\ +recursion, or are model checking an infinite model. It can also happen because\n\ the stacksize limit in your environment is set too low for the computation\n\ you are trying to do. You can find the value of your stacksize with the\n\ tcsh command 'limit stacksize' or the bash command 'ulimit -s'.\n\ @@ -169,7 +169,7 @@ Depending on your operating system configuration you may be able to\n\ increase your stacksize with the tcsh command 'unlimit stacksize'\n\ or the bash command 'ulimit -s unlimited'.\n\n"; returnValueDump = write(STDERR_FILENO, message, sizeof(message) - 1); - _exit(STACK_OVERFLOW); // don't call atexit() functions with a bad machine state + exit(STACK_OVERFLOW); // calling _exit() loses the message on Macs } int @@ -197,7 +197,7 @@ runtime to the bug being visible is greater than 10 seconds.\n\n"; returnValueDump = write(STDERR_FILENO, message1, sizeof(message1) - 1); returnValueDump = write(STDERR_FILENO, message2, sizeof(message2) - 1); returnValueDump = write(STDERR_FILENO, message3, sizeof(message3) - 1); - _exit(INTERNAL_ERROR); // don't call atexit() functions with a bad machine state + exit(INTERNAL_ERROR); // calling _exit() loses the message on Macs } void diff --git a/src/Mixfix/loopMode.cc b/src/Mixfix/loopMode.cc index 75070fca..37649f34 100644 --- a/src/Mixfix/loopMode.cc +++ b/src/Mixfix/loopMode.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-2023 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 @@ -75,7 +75,7 @@ Interpreter::contLoop2(const Vector& input) void Interpreter::contLoop(const Vector& input) { - if (!contLoop2(input) && savedLoopSubject.length() != 0) + if (!contLoop2(input) && !savedLoopSubject.empty()) { Vector savedInput(input); // in case input gets overwritten, say in debugger IssueAdvisory("attempting to reinitialize loop."); diff --git a/src/Mixfix/loopSymbol.cc b/src/Mixfix/loopSymbol.cc index 92ed719a..95aac07f 100644 --- a/src/Mixfix/loopSymbol.cc +++ b/src/Mixfix/loopSymbol.cc @@ -84,8 +84,8 @@ LoopSymbol::attachData(const Vector& opDeclaration, const Vector& data) { if (strcmp(purpose, "LoopSymbol") == 0) - return data.length() == 0; - return FreeSymbol::attachData(opDeclaration, purpose, data); + return data.empty(); + return FreeSymbol::attachData(opDeclaration, purpose, data); } bool diff --git a/src/Mixfix/modules.yy b/src/Mixfix/modules.yy index e6ff450b..03aedb34 100644 --- a/src/Mixfix/modules.yy +++ b/src/Mixfix/modules.yy @@ -40,8 +40,7 @@ moduleExprDot : tokenBarDot expectedDot $$ = new ModuleExpression($1, $3); else { - IssueWarning(LineNumber($2.lineNumber()) << - ": missing module expression after " << QUOTE($2) << "."); + IssueWarning(&($2) << ": missing module expression after " << QUOTE($2) << "."); $$ = $1; } } @@ -217,12 +216,16 @@ toAttributeList : toAttributeList toAttribute ; toAttribute : KW_PREC IDENTIFIER { currentRenaming->setPrec($2); } + | KW_PREC { IssueWarning(&($1) << ": prec attribute without value in operator mapping."); } | KW_GATHER '(' { tokensClear(); } idList ')' { currentRenaming->setGather(tokenSequence); } + | KW_GATHER { IssueWarning(&($1) << ": gather attribute without pattern in operator mapping."); } | KW_FORMAT '(' { tokensClear(); } idList ')' { currentRenaming->setFormat(tokenSequence); } + | KW_FORMAT { IssueWarning(&($1) << ": format attribute without specification in operator mapping."); } | KW_LATEX '(' { lexerLatexMode(); } LATEX_STRING ')' { currentRenaming->setLatexMacro($4); } + | KW_LATEX { IssueWarning(&($1) << ": latex attribute without latex code in operator mapping."); } ; /* @@ -256,8 +259,7 @@ viewDecList : viewDecList viewDeclaration skipStrayArrow : KW_ARROW { - IssueWarning(LineNumber($1.lineNumber()) << - ": skipping " << QUOTE("->") << " in variable declaration."); + IssueWarning(&($1) << ": skipping " << QUOTE("->") << " in variable declaration."); } | {} ; @@ -458,10 +460,10 @@ viewStratMap : stratName CV->addStratMapping(strategyCall[0]); CV->addStratTarget(lexerBubble[0]); } - else { - IssueWarning(LineNumber(strategyCall[0].lineNumber()) << - ": bad syntax for strategy mapping."); - } + else + { + IssueWarning(&(strategyCall[0]) << ": bad syntax for strategy mapping."); + } } ; @@ -512,9 +514,7 @@ parameter : token colon2 moduleExpr colon2 : KW_COLON2 {} | ':' { - IssueWarning(LineNumber($1.lineNumber()) << - ": saw " << QUOTE(':') << " instead of " << - QUOTE("::") << " in parameter declaration."); + IssueWarning(&($1) << ": saw " << QUOTE(':') << " instead of " << QUOTE("::") << " in parameter declaration."); } ; @@ -541,8 +541,7 @@ declaration : KW_IMPORT moduleExprDot CM->addImport($1, $2); else { - IssueWarning(LineNumber($1.lineNumber()) << - ": missing module expression after " << QUOTE($1) << "."); + IssueWarning(&($1) << ": missing module expression after " << QUOTE($1) << "."); } } @@ -700,8 +699,7 @@ domainRangeAttr : typeName typeList dra2 | rangeAttr | badType { - IssueWarning(LineNumber(lineNumber) << - ": missing " << QUOTE("->") << " in constant declaration."); + IssueWarning(&($1) << ": missing " << QUOTE("->") << " in constant declaration."); } ; @@ -734,9 +732,7 @@ stratAttrList : KW_METADATA IDENTIFIER skipStrayColon : ':' { - IssueWarning(LineNumber($1.lineNumber()) << - ": skipping stray " << QUOTE(":") << " in operator declaration."); - + IssueWarning(&($1) << ": skipping stray " << QUOTE(":") << " in operator declaration."); } | {} ; @@ -744,13 +740,11 @@ skipStrayColon : ':' dra2 : skipStrayColon rangeAttr | '.' { - IssueWarning(LineNumber($1.lineNumber()) << - ": missing " << QUOTE("->") << " in operator declaration."); + IssueWarning(&($1) << ": missing " << QUOTE("->") << " in operator declaration."); } | badType { - IssueWarning(LineNumber($1.lineNumber()) << - ": missing " << QUOTE("->") << " in operator declaration."); + IssueWarning(&($1) << ": missing " << QUOTE("->") << " in operator declaration."); } ; @@ -861,16 +855,22 @@ attribute : KW_ASSOC CM->setFlag(SymbolType::ITER); } | KW_PREC IDENTIFIER { CM->setPrec($2); } + | KW_PREC { IssueWarning(&($1) << ": prec attribute without value in operator declaration."); } | KW_GATHER '(' { tokensClear(); } idList ')' { CM->setGather(tokenSequence); } + | KW_GATHER { IssueWarning(&($1) << ": gather attribute without pattern in operator declaration."); } | KW_FORMAT '(' { tokensClear(); } idList ')' { CM->setFormat(tokenSequence); } + | KW_FORMAT { IssueWarning(&($1) << ": format attribute without specification in operator declaration."); } | KW_STRAT '(' { tokensClear(); } idList ')' { CM->setStrat(tokenSequence); } + | KW_STRAT { IssueWarning(&($1) << ": strat attribute without strategy in operator declaration."); } | KW_ASTRAT '(' { tokensClear(); } idList ')' { CM->setStrat(tokenSequence); } + | KW_ASTRAT { IssueWarning(&($1) << ": strategy attribute without strategy in operator declaration."); } | KW_POLY '(' { tokensClear(); } idList ')' { CM->setPoly(tokenSequence); } + | KW_POLY { IssueWarning(&($1) << ": poly attribute without specification in operator declaration."); } | KW_MEMO { CM->setFlag(SymbolType::MEMO); @@ -904,6 +904,7 @@ attribute : KW_ASSOC } | KW_LATEX '(' { lexerLatexMode(); } LATEX_STRING ')' { CM->setLatexMacro($4); } + | KW_LATEX { IssueWarning(&($1) << ": latex attribute without latex code in operator declaration."); } | KW_SPECIAL '(' hookList ')' {} | KW_DITTO { @@ -943,8 +944,7 @@ hook : KW_ID_HOOK token { tokensClear(); CM->addHook(SyntacticPreModule::ID_HO expectedIs : KW_IS {} | { - IssueWarning(LineNumber(lineNumber) << ": missing " << - QUOTE("is") << " keyword."); + IssueWarning(LineNumber(lineNumber) << ": missing " << QUOTE("is") << " keyword."); } ; diff --git a/src/Mixfix/ops.cc b/src/Mixfix/ops.cc index 1f5036f9..7599f11e 100644 --- a/src/Mixfix/ops.cc +++ b/src/Mixfix/ops.cc @@ -462,7 +462,7 @@ SyntacticPreModule::makeDeclsConsistent() if (nrOpDefs != 0) { int lastDefIndex = nrOpDefs - 1; - if(opDefs[lastDefIndex].types.length() == 0) + if(opDefs[lastDefIndex].types.empty()) { // // Problem: we have op decls for which op def has not been @@ -481,7 +481,7 @@ SyntacticPreModule::makeDeclsConsistent() // if (stratDecls.empty()) return; - if (stratDecls.back().types.length() == 0) + if (stratDecls.back().types.empty()) { stratDecls.pop_back(); lastSawOpDecl = false; diff --git a/src/Mixfix/quotedIdentifierSymbol.cc b/src/Mixfix/quotedIdentifierSymbol.cc index 84f95dc6..c3a041f7 100644 --- a/src/Mixfix/quotedIdentifierSymbol.cc +++ b/src/Mixfix/quotedIdentifierSymbol.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-2023 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 @@ -66,7 +66,7 @@ QuotedIdentifierSymbol::attachData(const Vector& opDeclaration, { if (strcmp(purpose, "QuotedIdentifierSymbol") == 0) { - if (data.length() == 0) + if (data.empty()) return true; if (data.length() == 1) { diff --git a/src/Mixfix/syntacticPreModule.hh b/src/Mixfix/syntacticPreModule.hh index 2e585d6e..483f9e83 100644 --- a/src/Mixfix/syntacticPreModule.hh +++ b/src/Mixfix/syntacticPreModule.hh @@ -336,9 +336,9 @@ private: void garbageCollectAttributeSet(Term* attributeSet, Symbol* attributeSetSymbol) const; int startTokenCode; - Bool lastSawOpDecl; - Bool isStrategy; - Bool isCompleteFlag; + bool lastSawOpDecl; + bool isStrategy; + bool isCompleteFlag; Vector > sortDecls; Vector > subsortDecls; Vector opDecls; diff --git a/src/Mixfix/termPrint.cc b/src/Mixfix/termPrint.cc index 30287ccf..9c3131ad 100644 --- a/src/Mixfix/termPrint.cc +++ b/src/Mixfix/termPrint.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2014 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2023 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 @@ -349,8 +349,7 @@ MixfixModule::prettyPrint(ostream& s, if (needDisambig) s << '('; - if ((interpreter.getPrintFlag(Interpreter::PRINT_MIXFIX) && si.mixfixSyntax.length() != 0) || - basicType == SymbolType::SORT_TEST) + if ((interpreter.getPrintFlag(Interpreter::PRINT_MIXFIX) && !si.mixfixSyntax.empty()) || basicType == SymbolType::SORT_TEST) { // // Mixfix case. diff --git a/src/Mixfix/token.cc b/src/Mixfix/token.cc index 1593ca17..52d20942 100644 --- a/src/Mixfix/token.cc +++ b/src/Mixfix/token.cc @@ -56,6 +56,13 @@ operator<<(ostream& s, const Vector& tokens) return s; } +ostream& +operator<<(ostream& s, const Token* token) +{ + s << LineNumber(token->lineNumber()); + return s; +} + void Token::printTokens(ostream& s, const Vector& tokens, diff --git a/src/Mixfix/token.hh b/src/Mixfix/token.hh index 51050cfa..ea7595ff 100644 --- a/src/Mixfix/token.hh +++ b/src/Mixfix/token.hh @@ -294,5 +294,6 @@ Token::codeToRope(int code) ostream& operator<<(ostream& s, const Token& token); ostream& operator<<(ostream& s, const Vector& tokens); +ostream& operator<<(ostream& s, const Token* token); #endif diff --git a/src/Parser/ChangeLog b/src/Parser/ChangeLog index a44cb37b..669173e1 100644 --- a/src/Parser/ChangeLog +++ b/src/Parser/ChangeLog @@ -1,3 +1,9 @@ +2023-04-12 Steven Eker + + * pass2.cc (Parser::extractNextParse): use empty() + + * parser.cc (Parser::parseSentence): use empty() + 2023-04-10 Steven Eker * parser.hh (class Parser): union nextRule and equal in struct Rule diff --git a/src/Parser/parser.cc b/src/Parser/parser.cc index eb4e3706..111b2fd2 100644 --- a/src/Parser/parser.cc +++ b/src/Parser/parser.cc @@ -157,7 +157,7 @@ Parser::parseSentence(const Vector& sentence, int root) "bad root nonterminal " << root << " only " << firstTerminalRules.length() << " nonterminals in grammar"); - if (expansions.length() == 0) + if (expansions.empty()) { buildExpansionTables(); firstRealCall = calls.size(); diff --git a/src/Parser/pass2.cc b/src/Parser/pass2.cc index b8a90960..a815f000 100644 --- a/src/Parser/pass2.cc +++ b/src/Parser/pass2.cc @@ -33,7 +33,7 @@ Parser::extractNextParse() #endif int lastIndex = firstReturns.length() - 1; - if (parseTree.length() == 0) + if (parseTree.empty()) { ParserLog(" first attempt"); // diff --git a/src/Temporal/ChangeLog b/src/Temporal/ChangeLog index f67e195a..e44254f0 100644 --- a/src/Temporal/ChangeLog +++ b/src/Temporal/ChangeLog @@ -1,3 +1,7 @@ +2023-04-12 Steven Eker + + * logicFormula.hh (class LogicFormula): Bool -> bool + 2017-03-15 Steven Eker * transitionSet.cc (insert): added comments to explain subtle code @@ -66,7 +70,7 @@ * buchiAutomaton2.cc: removed #pragma * buchiAutomaton2.hh: removed #pragma - + ===================================Maude79=========================================== 2002-03-01 Steven Eker diff --git a/src/Temporal/logicFormula.hh b/src/Temporal/logicFormula.hh index 23922b56..3658062c 100644 --- a/src/Temporal/logicFormula.hh +++ b/src/Temporal/logicFormula.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-2023 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 @@ -70,7 +70,7 @@ private: struct Node { short op; - Bool propositional; + bool propositional; int args[2]; }; diff --git a/src/Utility/ChangeLog b/src/Utility/ChangeLog index 61625656..c07e4484 100644 --- a/src/Utility/ChangeLog +++ b/src/Utility/ChangeLog @@ -1,3 +1,29 @@ +2023-04-13 Steven Eker + + * intSet.cc (IntSet::findEntry): use empty() + +2023-04-12 Steven Eker + + * macros.hh: deleted typedef Bool - all reasonable compilers have + sizeof(bool) == 1 and for those that don't we don't care about + wasting some memory + (pluralize): use int rather than Int32 + deleted typedef Int32 + + * digraph.hh (class Digraph): Bool -> bool + + * macros.hh: include + +2023-04-11 Steven Eker + + * intSet.cc (IntSet::intersect): use empty(); contractTo(0) -> + clear() (2 places) + (IntSet::insert): use empty() + (IntSet::subtract): use empty() + (IntSet::disjoint): use empty() + +===================================Maude145=================================== + 2023-04-06 Steven Eker * macros.hh: added decl for selfCheckFailHandler(); call it diff --git a/src/Utility/digraph.hh b/src/Utility/digraph.hh index 28d65fe2..34be8d01 100644 --- a/src/Utility/digraph.hh +++ b/src/Utility/digraph.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-2023 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 @@ private: void extendPath(int i, Vector& current, Vector& longest); const int nodeCount; - Vector adjMatrix; + Vector adjMatrix; }; inline void diff --git a/src/Utility/intSet.cc b/src/Utility/intSet.cc index ed5834c9..6d4886b0 100644 --- a/src/Utility/intSet.cc +++ b/src/Utility/intSet.cc @@ -43,7 +43,7 @@ IntSet::hash2(int i) // 2nd hash function must always return an odd value int IntSet::insert(int k) { - if (intTable.length() == 0) + if (intTable.empty()) resize(STARTING_HASH_TABLE_SIZE); int i = findEntry(k); int j = hashTable[i]; @@ -99,7 +99,7 @@ void IntSet::subtract(const IntSet& other) { int n = intTable.length(); - if (n == 0 || other.intTable.length() == 0) + if (n == 0 || other.intTable.empty()) return; int j = 0; for (int i = 0; i < n; i++) @@ -121,10 +121,10 @@ IntSet::intersect(const IntSet& other) int n = intTable.length(); if (n == 0) return; - if (other.intTable.length() == 0) + if (other.intTable.empty()) { - intTable.contractTo(0); - hashTable.contractTo(0); + intTable.clear(); + hashTable.clear(); return; } int j = 0; @@ -140,7 +140,7 @@ IntSet::intersect(const IntSet& other) rehash(); } } - + bool IntSet::contains(const IntSet& other) const { @@ -161,7 +161,7 @@ bool IntSet::disjoint(const IntSet& other) const { int i = other.intTable.length(); - if (i == 0 || intTable.length() == 0) + if (i == 0 || intTable.empty()) return true; for (i--; i >= 0; i--) { @@ -174,7 +174,7 @@ IntSet::disjoint(const IntSet& other) const int IntSet::findEntry(int k) const { - Assert(hashTable.length() != 0, "zero length hash table"); + Assert(!hashTable.empty(), "empty length hash table"); int mask = hashTable.length() - 1; int i = hash(k) & mask; int j = hashTable[i]; diff --git a/src/Utility/macros.hh b/src/Utility/macros.hh index 308168e4..703e1ff1 100644 --- a/src/Utility/macros.hh +++ b/src/Utility/macros.hh @@ -56,6 +56,7 @@ // // C++ stuff. // +#include #include #include #include @@ -103,7 +104,6 @@ typedef ptrdiff_t Index; // // Types for storage efficiency. // -typedef char Bool; typedef signed char Byte; typedef unsigned char Ubyte; // @@ -142,7 +142,6 @@ typedef unsigned long long int Uint64; // // 32 bit arithmetic; sometime we need guarentee of left truncation. // -typedef int Int32; typedef unsigned int Uint32; // @@ -453,7 +452,7 @@ ceilingDivision(int dividend, int divisor) } inline const char* -pluralize(Int32 quantity) +pluralize(int quantity) { return (quantity == 1) ? "" : "s"; } diff --git a/tests/Corner/Makefile.am b/tests/Corner/Makefile.am index 5f444f85..ac7fa823 100644 --- a/tests/Corner/Makefile.am +++ b/tests/Corner/Makefile.am @@ -2,18 +2,27 @@ TESTS = \ badOmod \ badRenaming \ badView \ - badStatement + badStatement \ + fakeParameterSort \ + fakeParameterConstant \ + attributeOverparsing MAUDE_FILES = \ badOmod.maude \ badRenaming.maude \ badView.maude \ - badStatement.maude + badStatement.maude \ + fakeParameterSort.maude \ + fakeParameterConstant.maude \ + attributeOverparsing.maude RESULT_FILES = \ badOmod.expected \ badRenaming.expected \ badView.expected \ - badStatement.expected + badStatement.expected \ + fakeParameterSort.expected \ + fakeParameterConstant.expected \ + attributeOverparsing.expected EXTRA_DIST = $(TESTS) $(MAUDE_FILES) $(RESULT_FILES) diff --git a/tests/Corner/Makefile.in b/tests/Corner/Makefile.in index ab54a6d5..288c1247 100644 --- a/tests/Corner/Makefile.in +++ b/tests/Corner/Makefile.in @@ -439,19 +439,28 @@ TESTS = \ badOmod \ badRenaming \ badView \ - badStatement + badStatement \ + fakeParameterSort \ + fakeParameterConstant \ + attributeOverparsing MAUDE_FILES = \ badOmod.maude \ badRenaming.maude \ badView.maude \ - badStatement.maude + badStatement.maude \ + fakeParameterSort.maude \ + fakeParameterConstant.maude \ + attributeOverparsing.maude RESULT_FILES = \ badOmod.expected \ badRenaming.expected \ badView.expected \ - badStatement.expected + badStatement.expected \ + fakeParameterSort.expected \ + fakeParameterConstant.expected \ + attributeOverparsing.expected EXTRA_DIST = $(TESTS) $(MAUDE_FILES) $(RESULT_FILES) all: all-am @@ -663,6 +672,27 @@ badStatement.log: badStatement --log-file $$b.log --trs-file $$b.trs \ $(am__common_driver_flags) $(AM_LOG_DRIVER_FLAGS) $(LOG_DRIVER_FLAGS) -- $(LOG_COMPILE) \ "$$tst" $(AM_TESTS_FD_REDIRECT) +fakeParameterSort.log: fakeParameterSort + @p='fakeParameterSort'; \ + b='fakeParameterSort'; \ + $(am__check_pre) $(LOG_DRIVER) --test-name "$$f" \ + --log-file $$b.log --trs-file $$b.trs \ + $(am__common_driver_flags) $(AM_LOG_DRIVER_FLAGS) $(LOG_DRIVER_FLAGS) -- $(LOG_COMPILE) \ + "$$tst" $(AM_TESTS_FD_REDIRECT) +fakeParameterConstant.log: fakeParameterConstant + @p='fakeParameterConstant'; \ + b='fakeParameterConstant'; \ + $(am__check_pre) $(LOG_DRIVER) --test-name "$$f" \ + --log-file $$b.log --trs-file $$b.trs \ + $(am__common_driver_flags) $(AM_LOG_DRIVER_FLAGS) $(LOG_DRIVER_FLAGS) -- $(LOG_COMPILE) \ + "$$tst" $(AM_TESTS_FD_REDIRECT) +attributeOverparsing.log: attributeOverparsing + @p='attributeOverparsing'; \ + b='attributeOverparsing'; \ + $(am__check_pre) $(LOG_DRIVER) --test-name "$$f" \ + --log-file $$b.log --trs-file $$b.trs \ + $(am__common_driver_flags) $(AM_LOG_DRIVER_FLAGS) $(LOG_DRIVER_FLAGS) -- $(LOG_COMPILE) \ + "$$tst" $(AM_TESTS_FD_REDIRECT) .test.log: @p='$<'; \ $(am__set_b); \ diff --git a/tests/Corner/attributeOverparsing b/tests/Corner/attributeOverparsing new file mode 100755 index 00000000..51ef4352 --- /dev/null +++ b/tests/Corner/attributeOverparsing @@ -0,0 +1,10 @@ +#!/bin/sh + +MAUDE_LIB=$srcdir/../../src/Main +export MAUDE_LIB + +../../src/Main/maude \ + < $srcdir/attributeOverparsing.maude -no-banner -no-advise \ + > attributeOverparsing.out 2>&1 + +diff $srcdir/attributeOverparsing.expected attributeOverparsing.out > /dev/null 2>&1 diff --git a/tests/Corner/attributeOverparsing.expected b/tests/Corner/attributeOverparsing.expected new file mode 100644 index 00000000..f2fc40e0 --- /dev/null +++ b/tests/Corner/attributeOverparsing.expected @@ -0,0 +1,51 @@ +Warning: , line 6 (fmod FOO): prec attribute without value in + operator declaration. +Warning: , line 10 (fmod FOO): gather attribute without pattern + in operator declaration. +Warning: , line 14 (fmod FOO): format attribute without + specification in operator declaration. +Warning: , line 18 (fmod FOO): strat attribute without strategy + in operator declaration. +Warning: , line 22 (fmod FOO): strategy attribute without + strategy in operator declaration. +Warning: , line 26 (fmod FOO): poly attribute without + specification in operator declaration. +Warning: , line 30 (fmod FOO): prec attribute without value in + operator declaration. +Warning: , line 34 (fmod FOO): gather attribute without pattern + in operator declaration. +Warning: , line 38 (fmod FOO): format attribute without + specification in operator declaration. +Warning: , line 42 (fmod FOO): strat attribute without strategy + in operator declaration. +Warning: , line 46 (fmod FOO): strategy attribute without + strategy in operator declaration. +Warning: , line 50 (fmod FOO): poly attribute without + specification in operator declaration. +Warning: , line 54 (fmod FOO): prec attribute without value in + operator mapping. +Warning: , line 58 (fmod FOO): prec attribute without value in + operator mapping. +Warning: , line 58 (fmod FOO): gather attribute without pattern + in operator mapping. +Warning: , line 62 (fmod FOO): gather attribute without pattern + in operator mapping. +Warning: , line 66 (fmod FOO): format attribute without + specification in operator mapping. +Warning: , line 70 (fmod FOO): format attribute without + specification in operator mapping. +Warning: , line 70 (fmod FOO): prec attribute without value in + operator mapping. +Warning: , line 70 (fmod FOO): gather attribute without pattern + in operator mapping. +Warning: , line 74 (fmod FOO): latex attribute without latex + code in operator declaration. +Warning: , line 78 (fmod FOO): latex attribute without latex + code in operator declaration. +Warning: , line 82 (fmod FOO): latex attribute without latex + code in operator mapping. +Warning: , line 86 (fmod FOO): latex attribute without latex + code in operator mapping. +Warning: , line 86 (fmod FOO): prec attribute without value in + operator mapping. +Bye. diff --git a/tests/Corner/attributeOverparsing.maude b/tests/Corner/attributeOverparsing.maude new file mode 100644 index 00000000..9c82068a --- /dev/null +++ b/tests/Corner/attributeOverparsing.maude @@ -0,0 +1,87 @@ +*** +*** Test that attributes without their required information overparse. +*** + +fmod FOO is + op _+_ : Bool Bool -> Bool [prec ctor] . +endfm + +fmod FOO is + op _+_ : Bool Bool -> Bool [gather ctor] . +endfm + +fmod FOO is + op _+_ : Bool Bool -> Bool [format ctor] . +endfm + +fmod FOO is + op _+_ : Bool Bool -> Bool [strat ctor] . +endfm + +fmod FOO is + op _+_ : Bool Bool -> Bool [strategy ctor] . +endfm + +fmod FOO is + op _+_ : Bool Bool -> Bool [poly ctor] . +endfm + +fmod FOO is + op _+_ : Bool Bool -> Bool [prec] . +endfm + +fmod FOO is + op _+_ : Bool Bool -> Bool [gather] . +endfm + +fmod FOO is + op _+_ : Bool Bool -> Bool [format] . +endfm + +fmod FOO is + op _+_ : Bool Bool -> Bool [strat] . +endfm + +fmod FOO is + op _+_ : Bool Bool -> Bool [strategy] . +endfm + +fmod FOO is + op _+_ : Bool Bool -> Bool [poly] . +endfm + +fmod FOO is + inc NAT * (op _+_ to _++_ [prec]) . +endfm + +fmod FOO is + inc NAT * (op _+_ to _++_ [prec gather]) . +endfm + +fmod FOO is + inc NAT * (op _+_ to _++_ [gather]) . +endfm + +fmod FOO is + inc NAT * (op _+_ to _++_ [format]) . +endfm + +fmod FOO is + inc NAT * (op _+_ to _++_ [format prec gather]) . +endfm + +fmod FOO is + op _+_ : Bool Bool -> Bool [latex] . +endfm + +fmod FOO is + op _+_ : Bool Bool -> Bool [latex ctor] . +endfm + +fmod FOO is + inc NAT * (op _+_ to _++_ [latex]) . +endfm + +fmod FOO is + inc NAT * (op _+_ to _++_ [latex prec]) . +endfm diff --git a/tests/Corner/fakeParameterConstant b/tests/Corner/fakeParameterConstant new file mode 100755 index 00000000..aa17fef9 --- /dev/null +++ b/tests/Corner/fakeParameterConstant @@ -0,0 +1,10 @@ +#!/bin/sh + +MAUDE_LIB=$srcdir/../../src/Main +export MAUDE_LIB + +../../src/Main/maude \ + < $srcdir/fakeParameterConstant.maude -no-banner \ + > fakeParameterConstant.out 2>&1 + +diff $srcdir/fakeParameterConstant.expected fakeParameterConstant.out > /dev/null 2>&1 diff --git a/tests/Corner/fakeParameterConstant.expected b/tests/Corner/fakeParameterConstant.expected new file mode 100644 index 00000000..58d7c07f --- /dev/null +++ b/tests/Corner/fakeParameterConstant.expected @@ -0,0 +1,40 @@ +fmod BAR{Y :: T} is + sorts Y$Elt Bool . + op if_then_else_fi : Bool Universal Universal -> Universal [poly (2 3 0) prec + 0 gather (& & &) special ( + id-hook BranchSymbol + term-hook 1 (true) + term-hook 2 (false))] . + op _==_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E) + special ( + id-hook EqualitySymbol + term-hook equalTerm (true) + term-hook notEqualTerm (false))] . + op _=/=_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E) + special ( + id-hook EqualitySymbol + term-hook equalTerm (false) + term-hook notEqualTerm (true))] . + op Y$c : -> Y$Elt [pconst] . + op true : -> Bool [ctor special ( + id-hook SystemTrue)] . + op false : -> Bool [ctor special ( + id-hook SystemFalse)] . + op _and_ : Bool Bool -> Bool [assoc comm prec 55 gather (e E)] . + op _or_ : Bool Bool -> Bool [assoc comm prec 59 gather (e E)] . + op _xor_ : Bool Bool -> Bool [assoc comm prec 57 gather (e E)] . + op not_ : Bool -> Bool [prec 53 gather (E)] . + op _implies_ : Bool Bool -> Bool [prec 61 gather (e E)] . + op X$d : -> Y$Elt [pconst] . + eq true and A:Bool = A:Bool . + eq false and A:Bool = false . + eq A:Bool and A:Bool = A:Bool . + eq false xor A:Bool = A:Bool . + eq A:Bool xor A:Bool = false . + eq A:Bool and (B:Bool xor C:Bool) = A:Bool and B:Bool xor A:Bool and C:Bool . + eq not A:Bool = true xor A:Bool . + eq A:Bool or B:Bool = A:Bool and B:Bool xor A:Bool xor B:Bool . + eq A:Bool implies B:Bool = not (A:Bool xor A:Bool and B:Bool) . + eq Y$c = X$d . +endfm +Bye. diff --git a/tests/Corner/fakeParameterConstant.maude b/tests/Corner/fakeParameterConstant.maude new file mode 100644 index 00000000..87f155e1 --- /dev/null +++ b/tests/Corner/fakeParameterConstant.maude @@ -0,0 +1,19 @@ +*** +*** Test that fake parameter constant isn't treated like one. +*** + +fth T is + sort Elt . + op c : -> Elt [pconst] . +endfth + +fmod FOO{X :: T} is + op X$d : -> X$Elt [pconst] . + eq X$c = X$d . +endfm + +fmod BAR{Y :: T} is + inc FOO{Y} . +endfm + +show all . diff --git a/tests/Corner/fakeParameterSort b/tests/Corner/fakeParameterSort new file mode 100755 index 00000000..38453960 --- /dev/null +++ b/tests/Corner/fakeParameterSort @@ -0,0 +1,10 @@ +#!/bin/sh + +MAUDE_LIB=$srcdir/../../src/Main +export MAUDE_LIB + +../../src/Main/maude \ + < $srcdir/fakeParameterSort.maude -no-banner \ + > fakeParameterSort.out 2>&1 + +diff $srcdir/fakeParameterSort.expected fakeParameterSort.out > /dev/null 2>&1 diff --git a/tests/Corner/fakeParameterSort.expected b/tests/Corner/fakeParameterSort.expected new file mode 100644 index 00000000..7a7ad880 --- /dev/null +++ b/tests/Corner/fakeParameterSort.expected @@ -0,0 +1,38 @@ +fmod BAR{Y :: T} is + sorts Y$Elt Bool X$Foo . + subsort X$Foo < Y$Elt . + op if_then_else_fi : Bool Universal Universal -> Universal [poly (2 3 0) prec + 0 gather (& & &) special ( + id-hook BranchSymbol + term-hook 1 (true) + term-hook 2 (false))] . + op _==_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E) + special ( + id-hook EqualitySymbol + term-hook equalTerm (true) + term-hook notEqualTerm (false))] . + op _=/=_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E) + special ( + id-hook EqualitySymbol + term-hook equalTerm (false) + term-hook notEqualTerm (true))] . + op true : -> Bool [ctor special ( + id-hook SystemTrue)] . + op false : -> Bool [ctor special ( + id-hook SystemFalse)] . + op _and_ : Bool Bool -> Bool [assoc comm prec 55 gather (e E)] . + op _or_ : Bool Bool -> Bool [assoc comm prec 59 gather (e E)] . + op _xor_ : Bool Bool -> Bool [assoc comm prec 57 gather (e E)] . + op not_ : Bool -> Bool [prec 53 gather (E)] . + op _implies_ : Bool Bool -> Bool [prec 61 gather (e E)] . + eq true and A:Bool = A:Bool . + eq false and A:Bool = false . + eq A:Bool and A:Bool = A:Bool . + eq false xor A:Bool = A:Bool . + eq A:Bool xor A:Bool = false . + eq A:Bool and (B:Bool xor C:Bool) = A:Bool and B:Bool xor A:Bool and C:Bool . + eq not A:Bool = true xor A:Bool . + eq A:Bool or B:Bool = A:Bool and B:Bool xor A:Bool xor B:Bool . + eq A:Bool implies B:Bool = not (A:Bool xor A:Bool and B:Bool) . +endfm +Bye. diff --git a/tests/Corner/fakeParameterSort.maude b/tests/Corner/fakeParameterSort.maude new file mode 100644 index 00000000..a56b031a --- /dev/null +++ b/tests/Corner/fakeParameterSort.maude @@ -0,0 +1,18 @@ +*** +*** Test that fake parameter sort isn't treated like one. +*** + +fth T is + sort Elt . +endfth + +fmod FOO{X :: T} is + sort X$Foo . + subsort X$Foo < X$Elt . +endfm + +fmod BAR{Y :: T} is + inc FOO{Y} . +endfm + +show all .