diff --git a/NEWS b/NEWS index c0f57997..a2f2cfad 100755 --- a/NEWS +++ b/NEWS @@ -1,3 +1,18 @@ +Overview of Changes in Maude 3.4 beta (alpha158) (2023-03-12) +============================================================= +* fixed bug where LaTeX for op names in declarations, renamings +and views sometimes used the wrong font +* comments in LaTeX no longer use the comment environment +* fixed bug where the strategy part of an srewrite command was +omitted in the LaTeX comment +* fixed bug where show desugared omitted local op declarations +that overloaded imported operators +* changed the LaTeX vertical spacing +* fixed bug where color generated by a format attribute could +run in the followed text in LaTeX output +* fixed bug where a newline generated by a format attribute +reset the color to black in LaTeX output + Overview of Changes in alpha157 (2024-02-27) ============================================ * fixed bug where debugging information was being printed to diff --git a/configure b/configure index 7e095a82..20c28ff1 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 alpha157. +# Generated by GNU Autoconf 2.69 for Maude 3.4beta. # # Report bugs to . # @@ -580,8 +580,8 @@ MAKEFLAGS= # Identity of this package. PACKAGE_NAME='Maude' PACKAGE_TARNAME='maude' -PACKAGE_VERSION='alpha157' -PACKAGE_STRING='Maude alpha157' +PACKAGE_VERSION='3.4beta' +PACKAGE_STRING='Maude 3.4beta' PACKAGE_BUGREPORT='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 alpha157 to adapt to many kinds of systems. +\`configure' configures Maude 3.4beta to adapt to many kinds of systems. Usage: $0 [OPTION]... [VAR=VALUE]... @@ -1383,7 +1383,7 @@ fi if test -n "$ac_init_help"; then case $ac_init_help in - short | recursive ) echo "Configuration of Maude alpha157:";; + short | recursive ) echo "Configuration of Maude 3.4beta:";; esac cat <<\_ACEOF @@ -1490,7 +1490,7 @@ fi test -n "$ac_init_help" && exit $ac_status if $ac_init_version; then cat <<\_ACEOF -Maude configure alpha157 +Maude configure 3.4beta generated by GNU Autoconf 2.69 Copyright (C) 2012 Free Software Foundation, Inc. @@ -2013,7 +2013,7 @@ cat >config.log <<_ACEOF This file contains any messages produced by compilers while running configure, to aid debugging if configure makes a mistake. -It was created by Maude $as_me alpha157, which was +It was created by Maude $as_me 3.4beta, which was generated by GNU Autoconf 2.69. Invocation command line was $ $0 $@ @@ -2962,7 +2962,7 @@ fi # Define the identity of the package. PACKAGE='maude' - VERSION='alpha157' + VERSION='3.4beta' cat >>confdefs.h <<_ACEOF @@ -6623,7 +6623,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 # report actual input values of CONFIG_FILES etc. instead of their # values after options handling. ac_log=" -This file was extended by Maude $as_me alpha157, which was +This file was extended by Maude $as_me 3.4beta, which was generated by GNU Autoconf 2.69. Invocation command line was CONFIG_FILES = $CONFIG_FILES @@ -6689,7 +6689,7 @@ _ACEOF cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`" ac_cs_version="\\ -Maude config.status alpha157 +Maude config.status 3.4beta configured by $0, generated by GNU Autoconf 2.69, with options \\"\$ac_cs_config\\" diff --git a/configure.ac b/configure.ac index 92e9d9dc..3dd84600 100755 --- a/configure.ac +++ b/configure.ac @@ -3,7 +3,7 @@ # # Initialize autoconf stuff. # -AC_INIT(Maude, alpha157, [maude-bugs@lists.cs.illinois.edu]) +AC_INIT(Maude, 3.4beta, [maude-bugs@lists.cs.illinois.edu]) # # Allow directory names that look like macros. # diff --git a/doc/Makefile.am b/doc/Makefile.am index fb70ac8e..46d193b6 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -25,4 +25,5 @@ EXTRA_DIST = \ alpha154.txt \ alpha155.txt \ alpha156.txt \ - alpha157.txt + alpha157.txt\ + alpha158.txt diff --git a/doc/Makefile.in b/doc/Makefile.in index 849c696c..197c1e94 100644 --- a/doc/Makefile.in +++ b/doc/Makefile.in @@ -257,7 +257,8 @@ EXTRA_DIST = \ alpha154.txt \ alpha155.txt \ alpha156.txt \ - alpha157.txt + alpha157.txt\ + alpha158.txt all: all-am diff --git a/doc/alpha157.txt b/doc/alpha157.txt index b7c27b15..34c6535e 100644 --- a/doc/alpha157.txt +++ b/doc/alpha157.txt @@ -143,7 +143,7 @@ red `(_`)`)(a) . red `)_`((a) . (2) Previously integer exponents and left shifts were limited to 1,000,000 to avoid -inadvertently runing out of memory. The limit is now ULONG_MAX (9,223,372,036,854,775,807 +inadvertently running out of memory. The limit is now ULONG_MAX (9,223,372,036,854,775,807 on 64-bit hardware, 4,294,967,295 on 32-bit hardware) which is a hard limit imposed by GMP, although as before, if the first argument is 0, 1 or -1 for exponentiation or 0 for left shift, then the answer is trivial and arbitrary second arguments can diff --git a/doc/alpha158.txt b/doc/alpha158.txt new file mode 100644 index 00000000..ec5864e8 --- /dev/null +++ b/doc/alpha158.txt @@ -0,0 +1,58 @@ +Alpha 158 release notes +======================== + +Bug fixes +========== + +(1) A bug where the LaTeX for op names in op declarations, renaming and views +did not use math italic for single character names like f and regular italic +for simple multi-character names like infinity. Reported by Paco. + +(2) A bug where the strategy part of an srewrite command was not printed in the +LaTeX comment. + +(3) A bug where show desugared did not show overloaded declarations for +imported operators. Illustrated by: + +fmod TEST is + sort ExtBool . + subsort Bool < ExtBool . + op _or_ : ExtBool ExtBool -> ExtBool [ditto] . +endfm + +show desugared . + +This bug also affected the LaTeX output. + +(4) A bug where color generated by a format attribute could run into +the text following a term in LaTeX output: + +mod FOO is + op a b : -> Bool [format (r d d)] . +endm + +set print format on . + +search a b =>* X:Bool such that a b . + +(5) A bug where generating a newline using a format attribute reset the color +to black in the LaTeX output (this is a LaTeX feature). Illustrated by: + +mod FOO is + op a b : -> Bool [format (r n o)] . +endm + +set print format on . + +search a b =>* X:Bool such that a b . + +Other changes +============== + +(1) Comments at the start of each command in latex output no longer use +\begin{comment} ... \end{comment} to avoid Paco's pathological case. +Instead just % is used and the printing of user's formatting attributes which +could included a newline is suppressed. + +(2) Changed the LaTeX spacing of show commands so that the command is closer +to its result than it is to the previous result. diff --git a/src/ACU_Theory/ACU_Term.cc b/src/ACU_Theory/ACU_Term.cc index d0e2764a..846001f7 100644 --- a/src/ACU_Theory/ACU_Term.cc +++ b/src/ACU_Theory/ACU_Term.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2021 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -118,7 +118,7 @@ ACU_Term::ACU_Term(const ACU_Term& original, ACU_Symbol* symbol, SymbolMap* tran } RawArgumentIterator* -ACU_Term::arguments() +ACU_Term::arguments() const { return new ACU_ArgumentIterator(&argArray); } diff --git a/src/ACU_Theory/ACU_Term.hh b/src/ACU_Theory/ACU_Term.hh index 5cb1ded9..53bb45a2 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-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -38,7 +38,7 @@ public: // // Member functions required by theory interface. // - RawArgumentIterator* arguments(); + RawArgumentIterator* arguments() const; void deepSelfDestruct(); Term* deepCopy2(SymbolMap* translator) const; Term* normalize(bool full, bool& changed); diff --git a/src/ACU_Theory/ChangeLog b/src/ACU_Theory/ChangeLog index 6a5cf69e..7b3efa05 100755 --- a/src/ACU_Theory/ChangeLog +++ b/src/ACU_Theory/ChangeLog @@ -1,3 +1,11 @@ +2024-03-05 Steven Eker + + * ACU_Term.cc (ACU_Term::arguments): made const + + * ACU_Term.hh (class ACU_Term): made arguments() const + +===================================Maude158=========================================== + 2024-01-16 Steven Eker * ACU_Symbol.cc (ACU_Symbol::stackArguments): support diff --git a/src/AU_Theory/AU_DagNode.cc b/src/AU_Theory/AU_DagNode.cc index dc59d413..e39e4737 100755 --- a/src/AU_Theory/AU_DagNode.cc +++ b/src/AU_Theory/AU_DagNode.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2021 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -274,7 +274,7 @@ AU_DagNode::matchVariableWithExtension(int index, AU_ExtensionInfo* e = safeCast(AU_ExtensionInfo*, extensionInfo); AU_Subproblem* subproblem = new AU_Subproblem(this, 0, argArray.length() - 1, 1, e); int min = symbol()->oneSidedId() ? 1 : 2; - subproblem->addTopVariable(0, index, min, UNBOUNDED, const_cast(sort)); // HACK + subproblem->addTopVariable(0, index, min, UNBOUNDED, sort); subproblem->complete(); returnedSubproblem = subproblem; extensionInfo->setValidAfterMatch(false); diff --git a/src/AU_Theory/AU_Layer.cc b/src/AU_Theory/AU_Layer.cc index be3683d0..befc060d 100644 --- a/src/AU_Theory/AU_Layer.cc +++ b/src/AU_Theory/AU_Layer.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -107,7 +107,7 @@ AU_Layer::initializeLast(int last, AU_ExtensionInfo* extension) } void -AU_Layer::addTopVariable(int index, int lowerBound, int upperBound, Sort* sort) +AU_Layer::addTopVariable(int index, int lowerBound, int upperBound, const Sort* sort) { int nrVariables = prevVariables.length(); prevVariables.expandBy(1); diff --git a/src/AU_Theory/AU_Layer.hh b/src/AU_Theory/AU_Layer.hh index 8797ab40..acc321f2 100644 --- a/src/AU_Theory/AU_Layer.hh +++ b/src/AU_Theory/AU_Layer.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -36,7 +36,7 @@ public: void initialize(AU_DagNode* subjectDag); void initializeFirst(int first, AU_ExtensionInfo* extension); void initializeLast(int last, AU_ExtensionInfo* extension); - void addTopVariable(int index, int lowerBound, int upperBound, Sort* sort); + void addTopVariable(int index, int lowerBound, int upperBound, const Sort* sort); void addNode(LocalBinding* difference, Subproblem* subproblem, int firstSubterm, @@ -52,7 +52,7 @@ private: int index; int lowerBound; int upperBound; - Sort* sort; + const Sort* sort; // // For solve-time use // diff --git a/src/AU_Theory/AU_Subproblem.hh b/src/AU_Theory/AU_Subproblem.hh index 8fa9fb3a..b7e4c1ed 100644 --- a/src/AU_Theory/AU_Subproblem.hh +++ b/src/AU_Theory/AU_Subproblem.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -44,7 +44,7 @@ public: int index, int lowerBound, int upperBound, - Sort* sort); + const Sort* sort); void addNode(int layerNr, LocalBinding* difference, Subproblem* subproblem, @@ -65,7 +65,7 @@ AU_Subproblem::addTopVariable(int layerNr, int index, int lowerBound, int upperBound, - Sort* sort) + const Sort* sort) { layers[layerNr].addTopVariable(index, lowerBound, upperBound, sort); } diff --git a/src/AU_Theory/AU_Term.cc b/src/AU_Theory/AU_Term.cc index 222030b3..64bf4dc5 100644 --- a/src/AU_Theory/AU_Term.cc +++ b/src/AU_Theory/AU_Term.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2021 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -81,7 +81,7 @@ AU_Term::AU_Term(const AU_Term& original, AU_Symbol* symbol, SymbolMap* translat } RawArgumentIterator* -AU_Term::arguments() +AU_Term::arguments() const { return new AU_ArgumentIterator(argArray); } diff --git a/src/AU_Theory/AU_Term.hh b/src/AU_Theory/AU_Term.hh index 56e0aa04..4fa9740a 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-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -38,7 +38,7 @@ public: // // Functions required by theory interface. // - RawArgumentIterator* arguments(); + RawArgumentIterator* arguments() const; void deepSelfDestruct(); Term* deepCopy2(SymbolMap* translator) const; Term* normalize(bool full, bool& changed); diff --git a/src/AU_Theory/ChangeLog b/src/AU_Theory/ChangeLog index 5cfdbb84..bad30b67 100755 --- a/src/AU_Theory/ChangeLog +++ b/src/AU_Theory/ChangeLog @@ -1,3 +1,22 @@ +2024-03-05 Steven Eker + + * AU_Term.cc (AU_Term::arguments): made const + + * AU_Term.hh (class AU_Term): made arguments() const + + * AU_DagNode.cc (AU_DagNode::matchVariableWithExtension): get + rid of const_cast<> + + * AU_Subproblem.hh (AU_Subproblem::addTopVariable): pass sort arg + as const + + * AU_Layer.cc (AU_Layer::addTopVariable): pass sort arg as const + + * AU_Layer.hh (class AU_Layer): made sort const in struct TopVariable; + updated decl for addTopVariable() + +===================================Maude158=========================================== + 2024-01-16 Steven Eker * AU_Symbol.cc (AU_Symbol::stackArguments): handle diff --git a/src/BuiltIn/ChangeLog b/src/BuiltIn/ChangeLog index 7f9cd667..d1a5f951 100755 --- a/src/BuiltIn/ChangeLog +++ b/src/BuiltIn/ChangeLog @@ -1,3 +1,35 @@ +2024-03-06 Steven Eker + + * divisionSymbol.cc (DivisionSymbol::isRat): (both versions) + removed unneeded cast in Assert() + (DivisionSymbol::getRat) (both versions) ditto + + * minusSymbol.cc (MinusSymbol::isNeg): (both versions) removed + unneeded cast in Assert() + (MinusSymbol::getNeg): (both versions) ditto + (MinusSymbol::getSignedInt64): ditto + + * divisionSymbol.hh (class DivisionSymbol): updated decls for + Term* versions of isRat() and getRat() + + * divisionSymbol.cc (DivisionSymbol::isRat): (Term* version) + made arg const + (DivisionSymbol::getRat): (Term* version) made arg const + + * minusSymbol.hh (class MinusSymbol): updated decls for Term* + versions of isNet() and getNeg() + + * minusSymbol.cc (MinusSymbol::isNeg): (Term* version) make arg const + (MinusSymbol::getNeg): (Term* version) make arg const + +2024-03-04 Steven Eker + + * stringOpSymbol.cc (StringOpSymbol::eqRewrite): use unsigned long rather + than Uint to correspond with GMP return type + (StringOpSymbol::eqRewrite): use ULONG_MAX rather than UINT max + +===================================Maude158=========================================== + 2024-02-09 Steven Eker * numberOpSymbol.cc (NumberOpSymbol::eqRewrite): use mpz_fits_ulong_p() diff --git a/src/BuiltIn/divisionSymbol.cc b/src/BuiltIn/divisionSymbol.cc index 73376a1d..b801ed57 100755 --- a/src/BuiltIn/divisionSymbol.cc +++ b/src/BuiltIn/divisionSymbol.cc @@ -162,8 +162,7 @@ DivisionSymbol::makeRatDag(const mpz_class& nr, const mpz_class& dr) bool DivisionSymbol::isRat(const DagNode* dagNode) const { - Assert(this == static_cast(dagNode->symbol()), - "bad symbol"); + Assert(this == dagNode->symbol(), "bad symbol"); const FreeDagNode* d = safeCast(const FreeDagNode*, dagNode); DagNode* d0 = d->getArgument(0); DagNode* d1 = d->getArgument(1); @@ -176,9 +175,8 @@ DivisionSymbol::isRat(const DagNode* dagNode) const const mpz_class& DivisionSymbol::getRat(const DagNode* dagNode, mpz_class& numerator) const { - Assert(this == static_cast(dagNode->symbol()), - "bad symbol"); - const FreeDagNode* d = safeCast(const FreeDagNode*, dagNode); + Assert(this == dagNode->symbol(), "bad symbol"); + const FreeDagNode* d = safeCast(const FreeDagNode*, dagNode); DagNode* d0 = d->getArgument(0); if (d0->symbol() == minusSymbol) (void) minusSymbol->getNeg(d0, numerator); @@ -203,10 +201,9 @@ DivisionSymbol::makeRatTerm(const mpz_class& nr, const mpz_class& dr) } bool -DivisionSymbol::isRat(/* const */ Term* term) const +DivisionSymbol::isRat(const Term* term) const { - Assert(this == static_cast(term->symbol()), - "bad symbol"); + Assert(this == term->symbol(), "bad symbol"); ArgumentIterator i(*term); Term* t0 = i.argument(); i.next(); @@ -218,10 +215,9 @@ DivisionSymbol::isRat(/* const */ Term* term) const const mpz_class& -DivisionSymbol::getRat(/* const */ Term* term, mpz_class& numerator) const +DivisionSymbol::getRat(const Term* term, mpz_class& numerator) const { - Assert(this == static_cast(term->symbol()), - "bad symbol"); + Assert(this == term->symbol(), "bad symbol"); ArgumentIterator i(*term); Term* t0 = i.argument(); if (t0->symbol() == minusSymbol) diff --git a/src/BuiltIn/divisionSymbol.hh b/src/BuiltIn/divisionSymbol.hh index f31366b1..b3c05eb8 100644 --- a/src/BuiltIn/divisionSymbol.hh +++ b/src/BuiltIn/divisionSymbol.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -51,8 +51,8 @@ public: bool isRat(const DagNode* dagNode) const; const mpz_class& getRat(const DagNode* dagNode, mpz_class& numerator) const; Term* makeRatTerm(const mpz_class& nr, const mpz_class& dr); - bool isRat(/* const */ Term* term) const; - const mpz_class& getRat(/* const */ Term* term, mpz_class& numerator) const; + bool isRat(const Term* term) const; + const mpz_class& getRat(const Term* term, mpz_class& numerator) const; SuccSymbol* succSymbol; MinusSymbol* minusSymbol; diff --git a/src/BuiltIn/minusSymbol.cc b/src/BuiltIn/minusSymbol.cc index 613c9801..821f5fee 100644 --- a/src/BuiltIn/minusSymbol.cc +++ b/src/BuiltIn/minusSymbol.cc @@ -98,8 +98,7 @@ MinusSymbol::makeNegDag(const mpz_class& integer) bool MinusSymbol::isNeg(const DagNode* dagNode) const { - Assert(static_cast(dagNode->symbol()) == this, - "symbol mismatch"); + Assert(dagNode->symbol() == this, "symbol mismatch"); DagNode* a = safeCast(const FreeDagNode*, dagNode)->getArgument(0); return a->symbol() == getSuccSymbol() && getSuccSymbol()->isNat(a); } @@ -107,8 +106,7 @@ MinusSymbol::isNeg(const DagNode* dagNode) const const mpz_class& MinusSymbol::getNeg(const DagNode* dagNode, mpz_class& result) const { - Assert(static_cast(dagNode->symbol()) == this, - "symbol mismatch"); + Assert(dagNode->symbol() == this, "symbol mismatch"); result = - getSuccSymbol()->getNat(safeCast(const FreeDagNode*, dagNode)->getArgument(0)); return result; } @@ -131,20 +129,18 @@ MinusSymbol::makeIntTerm(const mpz_class& integer) } bool -MinusSymbol::isNeg(/* const */ Term* term) const +MinusSymbol::isNeg(const Term* term) const { - Assert(static_cast(term->symbol()) == this, - "symbol mismatch"); + Assert(term->symbol() == this, "symbol mismatch"); ArgumentIterator i(*term); Term* t = i.argument(); return t->symbol() == getSuccSymbol() && getSuccSymbol()->isNat(t); } const mpz_class& -MinusSymbol::getNeg(/* const */ Term* term, mpz_class& result) const +MinusSymbol::getNeg(const Term* term, mpz_class& result) const { - Assert(static_cast(term->symbol()) == this, - "symbol mismatch"); + Assert(term->symbol() == this, "symbol mismatch"); ArgumentIterator i(*term); result = - getSuccSymbol()->getNat(i.argument()); return result; @@ -153,7 +149,7 @@ MinusSymbol::getNeg(/* const */ Term* term, mpz_class& result) const bool MinusSymbol::getSignedInt64(const DagNode* dagNode, Int64& value) const { - if (static_cast(dagNode->symbol()) == this) + if (dagNode->symbol() == this) { const FreeDagNode* f = safeCast(const FreeDagNode*, dagNode); if (getSuccSymbol()->getSignedInt64(f->getArgument(0), value)) diff --git a/src/BuiltIn/minusSymbol.hh b/src/BuiltIn/minusSymbol.hh index 07c97b4a..b1798312 100644 --- a/src/BuiltIn/minusSymbol.hh +++ b/src/BuiltIn/minusSymbol.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -46,8 +46,8 @@ public: const mpz_class& getNeg(const DagNode* dagNode, mpz_class& result) const; DagNode* makeIntDag(const mpz_class& integer); Term* makeIntTerm(const mpz_class& integer); - bool isNeg(/* const */ Term* term) const; - const mpz_class& getNeg(/* const */ Term* term, mpz_class& result) const; + bool isNeg(const Term* term) const; + const mpz_class& getNeg(const Term* term, mpz_class& result) const; bool getSignedInt64(const DagNode* dagNode, Int64& value) const; }; diff --git a/src/BuiltIn/stringOpSymbol.cc b/src/BuiltIn/stringOpSymbol.cc index b621873d..24a3d35c 100755 --- a/src/BuiltIn/stringOpSymbol.cc +++ b/src/BuiltIn/stringOpSymbol.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -342,9 +342,9 @@ StringOpSymbol::eqRewrite(DagNode* subject, RewritingContext& context) if (succSymbol->isNat(a1) && succSymbol->isNat(a2)) { const mpz_class& n1 = succSymbol->getNat(a1); - Uint index = n1.fits_uint_p() ? n1.get_ui() : UINT_MAX; + unsigned long index = n1.fits_uint_p() ? n1.get_ui() : ULONG_MAX; const mpz_class& n2 = succSymbol->getNat(a2); - Uint length = n2.fits_uint_p() ? n2.get_ui() : UINT_MAX; + unsigned long length = n2.fits_uint_p() ? n2.get_ui() : ULONG_MAX; return rewriteToString(subject, context, substring(left, index, length)); } break; @@ -360,7 +360,7 @@ StringOpSymbol::eqRewrite(DagNode* subject, RewritingContext& context) if (succSymbol->isNat(a2)) { const mpz_class& n2 = succSymbol->getNat(a2); - Uint index = n2.fits_uint_p() ? n2.get_ui() : UINT_MAX; + unsigned long index = n2.fits_uint_p() ? n2.get_ui() : ULONG_MAX; int r; switch (op) { diff --git a/src/CUI_Theory/CUI_Term.cc b/src/CUI_Theory/CUI_Term.cc index 530b40e7..acbb22f7 100644 --- a/src/CUI_Theory/CUI_Term.cc +++ b/src/CUI_Theory/CUI_Term.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -78,7 +78,7 @@ CUI_Term::CUI_Term(const CUI_Term& original, CUI_Symbol* symbol, SymbolMap* tran } RawArgumentIterator* -CUI_Term::arguments() +CUI_Term::arguments() const { return new CUI_ArgumentIterator(argArray); } diff --git a/src/CUI_Theory/CUI_Term.hh b/src/CUI_Theory/CUI_Term.hh index 162ddb42..cfd519ec 100644 --- a/src/CUI_Theory/CUI_Term.hh +++ b/src/CUI_Theory/CUI_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-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -36,7 +36,7 @@ public: // // Member functions required by theory interface. // - RawArgumentIterator* arguments(); + RawArgumentIterator* arguments() const; void deepSelfDestruct(); Term* deepCopy2(SymbolMap* translator) const; Term* normalize(bool full, bool& changed); diff --git a/src/CUI_Theory/ChangeLog b/src/CUI_Theory/ChangeLog index 69704a8b..ed8b7ace 100755 --- a/src/CUI_Theory/ChangeLog +++ b/src/CUI_Theory/ChangeLog @@ -1,3 +1,11 @@ +2024-03-05 Steven Eker + + * CUI_Term.cc (CUI_Term::arguments): made const + + * CUI_Term.hh (class CUI_Term): made arguments() const + +===================================Maude158=========================================== + 2024-01-16 Steven Eker * CUI_Symbol.cc (CUI_Symbol::stackArguments): handle diff --git a/src/Core/ChangeLog b/src/Core/ChangeLog index fb61a1d0..1b3f90c6 100644 --- a/src/Core/ChangeLog +++ b/src/Core/ChangeLog @@ -1,3 +1,10 @@ +2024-03-05 Steven Eker + + * argumentIterator.hh (ArgumentIterator::ArgumentIterator): take + const arg + +===================================Maude158=========================================== + 2024-01-19 Steven Eker * module.cc (Module::checkEquation): added AdvisoryCheck() for diff --git a/src/Core/argumentIterator.hh b/src/Core/argumentIterator.hh index f525c3b2..a2034b36 100644 --- a/src/Core/argumentIterator.hh +++ b/src/Core/argumentIterator.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -30,7 +30,7 @@ class ArgumentIterator { public: - ArgumentIterator(Term& t); + ArgumentIterator(const Term& t); ~ArgumentIterator(); bool valid() const; Term* argument() const; @@ -41,7 +41,7 @@ private: }; inline -ArgumentIterator::ArgumentIterator(Term& t) +ArgumentIterator::ArgumentIterator(const Term& t) { argumentIterator = t.arguments(); } diff --git a/src/FreeTheory/ChangeLog b/src/FreeTheory/ChangeLog index cd5b8e50..6b63b42d 100755 --- a/src/FreeTheory/ChangeLog +++ b/src/FreeTheory/ChangeLog @@ -1,3 +1,16 @@ +2024-03-12 Steven Eker + + * freeDagNode.hh (class FreeDagNode): deleted commented out + ctor decls + +2024-03-05 Steven Eker + + * freeTerm.cc (FreeTerm::arguments): made const + + * freeTerm.hh (class FreeTerm): made arguments() const + +===================================Maude158=========================================== + 2024-01-16 Steven Eker * freeSymbol.cc (FreeSymbol::stackArguments): handle diff --git a/src/FreeTheory/freeDagNode.hh b/src/FreeTheory/freeDagNode.hh index 52ab8886..d5dc9d6e 100755 --- a/src/FreeTheory/freeDagNode.hh +++ b/src/FreeTheory/freeDagNode.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -43,11 +43,6 @@ public: FreeDagNode(Symbol* symbol, DagNode* a0); FreeDagNode(Symbol* symbol, DagNode* a0, DagNode* a1); FreeDagNode(Symbol* symbol, DagNode* a0, DagNode* a1, DagNode* a2); - /* - FreeDagNode(Symbol* symbol, int dummy, DagNode* a0); - FreeDagNode(Symbol* symbol, int dummy, DagNode* a1, DagNode* a2); - FreeDagNode(Symbol* symbol, int dummy, DagNode* a0, DagNode* a1, DagNode* a2); - */ ~FreeDagNode(); RawDagArgumentIterator* arguments(); diff --git a/src/FreeTheory/freeTerm.cc b/src/FreeTheory/freeTerm.cc index b4f55515..648179da 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-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -101,7 +101,7 @@ FreeTerm::~FreeTerm() } RawArgumentIterator* -FreeTerm::arguments() +FreeTerm::arguments() const { if (argArray.empty()) return 0; diff --git a/src/FreeTheory/freeTerm.hh b/src/FreeTheory/freeTerm.hh index 89ec0696..c929d734 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-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -37,7 +37,7 @@ public: // // functions required by theory interface // - RawArgumentIterator* arguments(); + RawArgumentIterator* arguments() const; void deepSelfDestruct(); Term* deepCopy2(SymbolMap* translator) const; Term* normalize(bool full, bool& changed); diff --git a/src/Interface/ChangeLog b/src/Interface/ChangeLog index 776a7c89..a90999f5 100755 --- a/src/Interface/ChangeLog +++ b/src/Interface/ChangeLog @@ -1,3 +1,9 @@ +2024-03-05 Steven Eker + + * term.hh (class Term): make arguments() const + +===================================Maude158========================================= + 2024-01-19 Steven Eker * dagNode.cc (DagNode::reducibleByVariantEquation): don't check diff --git a/src/Interface/term.hh b/src/Interface/term.hh index 49a369d3..13baf462 100755 --- a/src/Interface/term.hh +++ b/src/Interface/term.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -112,7 +112,7 @@ public: // // These member functions must be defined for each derived class // - virtual RawArgumentIterator* arguments() = 0; + virtual RawArgumentIterator* arguments() const = 0; virtual void deepSelfDestruct() = 0; virtual Term* deepCopy2(SymbolMap* translator) const = 0; virtual Term* normalize(bool full, bool& changed) = 0; diff --git a/src/Main/ChangeLog b/src/Main/ChangeLog index e3fb3d8b..2062da3c 100755 --- a/src/Main/ChangeLog +++ b/src/Main/ChangeLog @@ -1,3 +1,7 @@ +2024-03-11 Steven Eker + + * maude.sty: added \maudeShowSpace + 2024-02-20 Steven Eker * maude.sty: adjust the spacing around, and hieght of * in diff --git a/src/Main/maude.sty b/src/Main/maude.sty index af344902..bf02908b 100644 --- a/src/Main/maude.sty +++ b/src/Main/maude.sty @@ -17,11 +17,11 @@ % along with this program; if not, write to the Free Software % Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA. % -% Latex package for use with the -latex-log= feature. -% Version alpha157. +% LaTeX package for use with the -latex-log= feature. +% Version 3.4beta. % \NeedsTeXFormat{LaTeX2e} -\ProvidesPackage{maude}[2024/02/20 Package for Maude logs] +\ProvidesPackage{maude}[2024/03/12 Package for Maude logs] \RequirePackage{amssymb,extarrows,longtable,tabto,xcolor,verbatim,alltt,seqsplit} \RequirePackage[T1]{fontenc} % @@ -35,6 +35,7 @@ \newcommand{\maudeBigSpace}{\hspace{0.6em}} \newcommand{\maudeHardSpace}{\hspace*{0.5em}} % doesn't disappear at the start of a new line \newcommand{\maudeAllowLineBreak}{\linebreak[0]} +\newcommand{\maudeShowSpace}{\vspace{1ex}} % space between a show command and the thing shown % % To get a newline that is not indented we actually start a new paragraph, which means we % need to drop out of math mode and use {} to protect from double dollar signs. diff --git a/src/Main/metaInterpreter.maude b/src/Main/metaInterpreter.maude index 3a90c769..42cdc081 100644 --- a/src/Main/metaInterpreter.maude +++ b/src/Main/metaInterpreter.maude @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2009-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 2009-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -22,7 +22,7 @@ *** *** Maude meta-interpreters. -*** Version alpha154 +*** Version 3.4beta. *** mod META-INTERPRETER is diff --git a/src/Main/model-checker.maude b/src/Main/model-checker.maude index b420a83d..99946eed 100644 --- a/src/Main/model-checker.maude +++ b/src/Main/model-checker.maude @@ -2,7 +2,7 @@ This file is part of the Maude 2 interpreter. - Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -22,7 +22,7 @@ *** *** Maude LTL satisfiability solver and model checker. -*** Version 2.3. +*** Version 3.4beta. *** fmod LTL is diff --git a/src/Main/prelude.maude b/src/Main/prelude.maude index d5a05325..594d4a31 100644 --- a/src/Main/prelude.maude +++ b/src/Main/prelude.maude @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -22,7 +22,7 @@ *** *** Maude interpreter standard prelude. -*** Version alpha155. +*** Version 3.4beta. *** *** Some of the overall structure is taken from the OBJ3 *** interpreter standard prelude. diff --git a/src/Main/prng.maude b/src/Main/prng.maude index 916eb372..450be9b9 100644 --- a/src/Main/prng.maude +++ b/src/Main/prng.maude @@ -2,7 +2,7 @@ This file is part of the Maude 2 interpreter. - Copyright 2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 2023-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -22,7 +22,7 @@ *** *** Maude pseudo-random number generator external objects -*** Version Alpha149. +*** Version 3.4beta. *** mod PRNG is diff --git a/src/Meta/ChangeLog b/src/Meta/ChangeLog index 29807b7f..b900e42e 100644 --- a/src/Meta/ChangeLog +++ b/src/Meta/ChangeLog @@ -1,3 +1,13 @@ +2024-03-06 Steven Eker + + * metaUp.cc (MetaLevel::upQid): got rid of const_cast<> + +2024-03-05 Steven Eker + + * metaUp.cc (MetaLevel::upTerm): remove const_cast<> + +===================================Maude158=========================================== + 2024-01-09 Steven Eker * metaLevel.hh (MetaLevel::downSearchType): support '# diff --git a/src/Meta/metaUp.cc b/src/Meta/metaUp.cc index 46db413f..6c0c962b 100644 --- a/src/Meta/metaUp.cc +++ b/src/Meta/metaUp.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -23,9 +23,9 @@ DagNode* MetaLevel::upQid(int id, PointerMap& qidMap) { - void* p = const_cast(static_cast(Token::name(id))); + const void* p = Token::name(id); DagNode* d = static_cast(qidMap.getMap(p)); - if (d == 0) + if (d == nullptr) { d = new QuotedIdentifierDagNode(qidSymbol, Token::backQuoteSpecials(id)); (void) qidMap.setMap(p, d); @@ -259,7 +259,7 @@ MetaLevel::upTerm(const Term* term, MixfixModule* m, PointerMap& qidMap) } } args[0] = upQid(id, qidMap); - ArgumentIterator a(*(const_cast(term))); + ArgumentIterator a(*term); if (nrArgs == 1) args[1] = upTerm(a.argument(), m, qidMap); else diff --git a/src/Mixfix/ChangeLog b/src/Mixfix/ChangeLog index 9b707b3c..ce990291 100644 --- a/src/Mixfix/ChangeLog +++ b/src/Mixfix/ChangeLog @@ -1,3 +1,195 @@ +2024-03-12 Steven Eker + + * latexCommon.cc (MixfixModule::latexFancySpace): set + restoreColor rather than attributeUsed + (MixfixModule::latexFancySpace): use restoreColor after a + newline + (MixfixModule::latexPrintBubble): use latexRed etc + + * mixfixModule.hh (class MixfixModule): added static data + member restoreColor + (MixfixModule::latexClearColor): use restoreColor + + * latexCommon.cc: added restoreColor static data member + + * latexDagNodePrint.cc (MixfixModule::latexPrintDagNode): call + latexClearColor() + + * latexTermPrint.cc (MixfixModule::latexPrettyPrint): call + latexClearColor() + + * mixfixModule.hh (MixfixModule::latexClearColor): added + + * latexCommon.cc (MixfixModule::latexFancySpace): set + attributeUsed and use latexClearColor(s) + (MixfixModule::latexFancySpace): use latexRed etc + + * prettyPrint.cc (MixfixModule::prettyPrint): (dagNode version) + remove unnecessary MixfixModule:: qualifications + +2024-03-11 Steven Eker + + * token.cc (Token::splitKind): reimplemented to avoid + const_cast<> + + * latexCommand.cc (MaudeLatexBuffer::generateShow): use + \maudeShowSpace (all three versions) + + * latexModulePrint.cc (VisibleModule::latexShowOps): symmetric + change + + * visibleModule.cc (VisibleModule::showOps): consider all + ops for potential printing because we may have local declarations + even if an op is imported + +2024-03-06 Steven Eker + + * prettyPrint.cc (MixfixModule::prettyPrint): (Term* version) + got rid of const_cast<> + + * quotedIdentifierOpSymbol.cc (QuotedIdentifierOpSymbol::makeQid): + got rid of const_cast<> + + * mixfixModule.hh (class MixfixModule): updated decls for suffix(), + handleIter(), handleMinus(), handleDivision(), handleFloat(), + handleString(), handleQuotedIdentifier(), handleVariable(), + handleSMT_Number(), prettyPrint() (Term* versions) + + * termPrint.cc (MixfixModule::suffix, MixfixModule::handleIter) + (MixfixModule::handleMinus, MixfixModule::handleDivision) + (MixfixModule::handleFloat, MixfixModule::handleString) + (MixfixModule::handleQuotedIdentifier) + (MixfixModule::handleVariable, MixfixModule::handleSMT_Number) + (MixfixModule::prettyPrint): make Term* arg const + +2024-03-05 Steven Eker + + * importTranslation.cc (ImportTranslation::translateExpr): + removed const_cast<> + (ImportTranslation::translateTerm): removed const_cast<> + +2024-03-04 Steven Eker + + * latexDagNodePrint.cc (MixfixModule::latexPrettyPrint): + deleted + + * mixfixModule.hh (class MixfixModule): deleted decl for 2 + argument DagNode* version of latexPrettyPrint() + +2024-03-01 Steven Eker + + * latexCommand.cc (MaudeLatexBuffer::generateCommand): print + strategy in comment if non-null + + * mixfixModule.hh (class MixfixModule): updated decl for + StrategyExpression* version of prettyPrint() + + * global.cc (operator<<): (StrategyExpression* version) moved + here; pass interpreter + + * strategyPrint.cc (MixfixModule::prettyPrint): take and pass + printSettings + + * global.cc (operator<<): reimplmented using + MixfixModule::printConditionFragment() + + * mixfixModule.hh (class MixfixModule): deleted decls for both + 2 argument versions of printCondition() + + * prettyPrint.cc (MixfixModule::printCondition): deleted both + 2 argument versions + + * strategyPrint.cc (MixfixModule::prettyPrint): use 3 argument + printCondition() + + * search.cc (Interpreter::search): use 3 argument printCondition() + + * global.cc (operator<<): (SortConstraint*, Equation*, Rule*, + StrategyDefinition* versions) use 3 argument printCondition() + + * match.cc (Interpreter::match): use 3 argument printCondition() + + * mixfixModule.hh (class MixfixModule): added decl for 3 argument + reEquation* version of printCondition() + + * prettyPrint.cc (MixfixModule::printCondition): added 3 argument + PreEquation* version + + * latexCommand.cc (MaudeLatexBuffer::generateMatch): use 3 argument + version of printCondition() with commentSettings + (MaudeLatexBuffer::generateSearch): ditto + + * mixfixModule.hh (class MixfixModule): added decl for + printConditionFragment() and 3 argument version of printCondition() + + * prettyPrint.cc (MixfixModule::printConditionFragment): added + (MixfixModule::printCondition): added 3 arg version + +2024-02-29 Steven Eker + + * token.cc (Token::makePrettyOpName): return empty string + if not prettified to alert caller + + * latexCommon.cc (MixfixModule::latexPrettyOpName): handle + empty string as indicating that no prettification was done by + Token::makePrettyOpName() and call Token::latexIdentifier() to + figure out the correct font to use + + * prettyPrint.cc (MixfixModule::prettyOpName): handle empty + string as indicating that no prettification was done by + Token::makePrettyOpName() + +2024-02-28 Steven Eker + + * interpreter.cc (Interpreter::quit): don't use comment + environment + + * latexResult.cc (MaudeLatexBuffer::generateSearchPath): use + startComment(), endComment() + (MaudeLatexBuffer::generateSearchPathLabels): ditto + (MaudeLatexBuffer::generateSearchGraph): ditto + + * latexCommand.cc (MaudeLatexBuffer::generateGetVariants): use + startComment(), endComment(), commentTerm(), commentDagNode(); + don't use Tty::blockEscapeSequences(), Tty::unblockEscapeSequences() + (MaudeLatexBuffer::generateVariantMatch): use startComment(), + endComment(), commentTerm(); don't use Tty::blockEscapeSequences(), + Tty::unblockEscapeSequences() + (MaudeLatexBuffer::generateVariantUnify): ditto + (MaudeLatexBuffer::generateUnify): ditto + (MaudeLatexBuffer::generateSearch): ditto + (MaudeLatexBuffer::generateMatch): ditto + (MaudeLatexBuffer::generateLoopTokens): don't use comment environment + (MaudeLatexBuffer::generateCommand): (both versions) use startComment(), + endComment() + (MaudeLatexBuffer::generateContinue): use startComment(), endComment() + (MaudeLatexBuffer::generateShow): (3 versions) use startComment(), + endComment() + + * maudeLatexBuffer.hh (MaudeLatexBuffer::startComment): added + (MaudeLatexBuffer::endComment): added + + * latexCommand.cc (MaudeLatexBuffer::generateCommand): (Term* + version) use commentDagNode(); don't use Tty::blockEscapeSequences() + and Tty::unblockEscapeSequences() + + * printSettings.hh (class PrintSettings): added PLAIN_PRINT_FLAGS + to enum PrintFlags + + * maudeLatexBuffer.cc: init commentSettings() + + * latexCommand.cc (MaudeLatexBuffer::generateCommand): (DagNode* + version) use commentDagNode(); don't use Tty::blockEscapeSequences() + and Tty::unblockEscapeSequences() + + * maudeLatexBuffer.hh (class MaudeLatexBuffer): deleted + commented out pendingClose data member + (class MaudeLatexBuffer): added data member commentSettings; + (MaudeLatexBuffer::commentTerm): added + (MaudeLatexBuffer::commentDagNode): added + +===================================Maude158=========================================== + 2024-02-26 Steven Eker * latexCommand.cc (MaudeLatexBuffer::generateGetVariants) diff --git a/src/Mixfix/auxProperty.cc b/src/Mixfix/auxProperty.cc index a5736f3e..364034d4 100644 --- a/src/Mixfix/auxProperty.cc +++ b/src/Mixfix/auxProperty.cc @@ -37,7 +37,7 @@ Token::skipSortName(const char* tokenString, bool& parameterized) // // A sort name can be terminated by \0, `, `] `} // If a legal sort name followed by a legal terminator is seen, the - // addess of the first terminator charater is returned otherwise 0 is + // addess of the first terminator character is returned otherwise 0 is // returned. // In the first case, parameterized is true iff the sort name contained `{ // In the second case, parameterized is undefined. diff --git a/src/Mixfix/global.cc b/src/Mixfix/global.cc index 28bf91a2..edd293d5 100644 --- a/src/Mixfix/global.cc +++ b/src/Mixfix/global.cc @@ -174,7 +174,7 @@ operator<<(ostream& s, const SortConstraint* sc) MixfixModule::prettyPrint(s, sc->getLhs(), interpreter, true); s << " : " << sc->getSort(); if (sc->hasCondition()) - MixfixModule::printCondition(s, sc); + MixfixModule::printCondition(s, sc, interpreter); MixfixModule* m = safeCast(MixfixModule*, sc->getModule()); m->printAttributes(s, sc, MixfixModule::MEMB_AX, interpreter); s << " ."; @@ -196,7 +196,7 @@ operator<<(ostream& s, const Equation* e) s << e->getLhs() << " = "; MixfixModule::prettyPrint(s, e->getRhs(), interpreter, true); if (e->hasCondition()) - MixfixModule::printCondition(s, e); + MixfixModule::printCondition(s, e, interpreter); MixfixModule* m = safeCast(MixfixModule*, e->getModule()); m->printAttributes(s, e, MixfixModule::EQUATION, interpreter); s << " ."; @@ -218,7 +218,7 @@ operator<<(ostream& s, const Rule* r) s << r->getLhs() << " => "; MixfixModule::prettyPrint(s, r->getRhs(), interpreter, true); if (r->hasCondition()) - MixfixModule::printCondition(s, r); + MixfixModule::printCondition(s, r, interpreter); MixfixModule* m = safeCast(MixfixModule*, r->getModule()); m->printAttributes(s, r, MixfixModule::RULE, interpreter); s << " ."; @@ -228,28 +228,7 @@ operator<<(ostream& s, const Rule* r) ostream& operator<<(ostream& s, const ConditionFragment* c) { - if (const EqualityConditionFragment* e = dynamic_cast(c)) - { - s << e->getLhs() << " = "; - MixfixModule::prettyPrint(s, e->getRhs(), interpreter, true); - } - else if (const SortTestConditionFragment* t = dynamic_cast(c)) - { - MixfixModule::prettyPrint(s, t->getLhs(), interpreter, true); - s << " : " << t->getSort(); - } - else if(const AssignmentConditionFragment* a = dynamic_cast(c)) - { - s << a->getLhs() << " := "; - MixfixModule::prettyPrint(s, a->getRhs(), interpreter, true); - } - else if(const RewriteConditionFragment* r = dynamic_cast(c)) - { - s << r->getLhs() << " => "; - MixfixModule::prettyPrint(s, r->getRhs(), interpreter, true); - } - else - CantHappen("bad condition fragment"); + MixfixModule::printConditionFragment(s, c, interpreter); return s; } @@ -264,7 +243,7 @@ operator<<(ostream& s, const StrategyDefinition* e) m->printStrategyTerm(s, e->getStrategy(), e->getLhs()); s << " := " << e->getRhs(); if (e->hasCondition()) - MixfixModule::printCondition(s, e); + MixfixModule::printCondition(s, e, interpreter); m->printAttributes(s, e, MixfixModule::STRAT_DEF, interpreter); s << " ."; @@ -344,3 +323,10 @@ operator<<(ostream& s, const RewriteStrategy* rs) s << " ."; return s; } + +ostream& +operator<<(ostream& s, StrategyExpression* strategy) +{ + (void) MixfixModule::prettyPrint(s, strategy, UNBOUNDED, interpreter); + return s; +} diff --git a/src/Mixfix/importTranslation.cc b/src/Mixfix/importTranslation.cc index 3352f44f..a3f8f108 100644 --- a/src/Mixfix/importTranslation.cc +++ b/src/Mixfix/importTranslation.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -269,7 +269,7 @@ ImportTranslation::translateExpr(const CallStrategy* cs) // Vector varBindings(strat->arity()); int j = 0; - for (ArgumentIterator i(*(const_cast(cs->getTerm()))); i.valid(); i.next(), ++j) + for (ArgumentIterator i(*(cs->getTerm())); i.valid(); i.next(), ++j) varBindings[j] = i.argument(); StrategyExpression* instantiated = @@ -320,7 +320,7 @@ ImportTranslation::translateTerm(const Term* term) // Vector varBindings(symbol->arity()); int j = 0; - for (ArgumentIterator i(*(const_cast(term))); i.valid(); i.next(), ++j) + for (ArgumentIterator i(*term); i.valid(); i.next(), ++j) varBindings[j] = i.argument(); // // Now we can instantiate the toTerm on copies of these diff --git a/src/Mixfix/interpreter.cc b/src/Mixfix/interpreter.cc index 491abf38..8b5c603c 100644 --- a/src/Mixfix/interpreter.cc +++ b/src/Mixfix/interpreter.cc @@ -134,7 +134,7 @@ Interpreter::quit() { ostream* latexStream = latexBuffer ? &(latexBuffer->getStream()) : nullptr; if (latexStream) - *latexStream << "\\begin{comment}\n%\n% quit\n%\n\\end{comment}\n\\begin{maudeResultParagraph}\n"; + *latexStream << "%\n% quit\n%\n\\begin{maudeResultParagraph}\n"; MemoryCell::maybeShowResources(cout, latexStream); cout << "Bye.\n"; if (latexStream) diff --git a/src/Mixfix/latexCommand.cc b/src/Mixfix/latexCommand.cc index 788af307..75e4c8ab 100644 --- a/src/Mixfix/latexCommand.cc +++ b/src/Mixfix/latexCommand.cc @@ -53,24 +53,23 @@ MaudeLatexBuffer::generateGetVariants(bool showCommand, // // Print comment. // - Tty::blockEscapeSequences(); - output << "\\begin{comment}\n%\n% "; + startComment(); output << command << " "; safeCastNonNull(module)->printModifiers(output, limit); - output << dag; + commentDagNode(dag); if (!constraint.empty()) { output << " such that "; const char* sep = ""; - for (const Term* t : constraint) + for (Term* t : constraint) { - output << sep << t; + output << sep; + commentTerm(t); sep = ", "; } output << " irreducible" << endl; } - output << " .\n%\n\\end{comment}\n"; - Tty::unblockEscapeSequences(); + endComment(); // // Print latex version of command. // @@ -113,25 +112,29 @@ MaudeLatexBuffer::generateVariantMatch(bool showCommand, // // Print comment. // - Tty::blockEscapeSequences(); - output << "\\begin{comment}\n%\n% "; + startComment(); output << command << " "; safeCastNonNull(module)->printModifiers(output, limit); for (Index i = 0; i < nrPairs; ++i) - output << lhs[i] << " <=? " << rhs[i] << ((i == nrPairs - 1) ? " " : " /\\ "); + { + commentTerm(lhs[i]); + output << " <=? "; + commentTerm(rhs[i]); + output << ((i == nrPairs - 1) ? "" : " /\\ "); + } if (!constraint.empty()) { output << " such that "; const char* sep = ""; - for (const Term* t : constraint) + for (Term* t : constraint) { - output << sep << t; + output << sep; + commentTerm(t); sep = ", "; } output << " irreducible" << endl; } - output << ".\n%\n\\end{comment}\n"; - Tty::unblockEscapeSequences(); + endComment(); // // Print latex version of command. // @@ -184,25 +187,29 @@ MaudeLatexBuffer::generateVariantUnify(bool showCommand, // // Print comment. // - Tty::blockEscapeSequences(); - output << "\\begin{comment}\n%\n% "; + startComment(); output << command << " "; safeCastNonNull(module)->printModifiers(output, limit); for (Index i = 0; i < nrPairs; ++i) - output << lhs[i] << " =? " << rhs[i] << ((i == nrPairs - 1) ? " " : " /\\ "); + { + commentTerm(lhs[i]); + output << " =? "; + commentTerm(rhs[i]); + output << ((i == nrPairs - 1) ? "" : " /\\ "); + } if (!constraint.empty()) { output << " such that "; const char* sep = ""; - for (const Term* t : constraint) + for (Term* t : constraint) { - output << sep << t; + output << sep; + commentTerm(t); sep = ", "; } output << " irreducible" << endl; } - output << ".\n%\n\\end{comment}\n"; - Tty::unblockEscapeSequences(); + endComment(); // // Print latex version of command. // @@ -250,13 +257,17 @@ MaudeLatexBuffer::generateUnify(bool showCommand, // // Print comment. // - Tty::blockEscapeSequences(); - output << "\\begin{comment}\n%\n% " << command << " "; + startComment(); + output << command << " "; safeCastNonNull(module)->printModifiers(output, limit); for (Index i = 0; i < nrPairs; ++i) - output << lhs[i] << " =? " << rhs[i] << ((i == nrPairs - 1) ? " ." : " /\\ "); - output << "\n%\n\\end{comment}\n"; - Tty::unblockEscapeSequences(); + { + commentTerm(lhs[i]); + output << " =? "; + commentTerm(rhs[i]); + output << ((i == nrPairs - 1) ? "" : " /\\ "); + } + endComment(); // // Print latex version of command. // @@ -292,17 +303,18 @@ MaudeLatexBuffer::generateMatch(bool showCommand, // // Print comment. // - Tty::blockEscapeSequences(); - output << "\\begin{comment}\n%\n% " << command << " "; + startComment(); + output << command << " "; safeCastNonNull(module)->printModifiers(output, limit); - output << pattern << " <=? " << subject; + commentTerm(pattern); + output << " <=? "; + commentDagNode(subject); if (!condition.empty()) { output << " such that "; - MixfixModule::printCondition(output, condition); + MixfixModule::printCondition(output, condition, commentSettings); } - output << " .\n%\n\\end{comment}\n"; - Tty::unblockEscapeSequences(); + endComment(); // // Print latex version of command. // @@ -349,8 +361,7 @@ MaudeLatexBuffer::generateSearch(bool showCommand, // // Print comment. // - Tty::blockEscapeSequences(); - output << "\\begin{comment}\n%\n% "; + startComment(); if (debug) output << "debug "; if (variantFlags & NarrowingSequenceSearch3::FOLD) @@ -370,14 +381,15 @@ MaudeLatexBuffer::generateSearch(bool showCommand, output << "} "; } safeCastNonNull(module)->printModifiers(output, limit, depth); - output << subject << ' ' << searchTypeSymbol[searchType] << ' ' << target; + commentDagNode(subject); + output << ' ' << searchTypeSymbol[searchType] << ' '; + commentTerm(target); if (!condition.empty()) { output << " such that "; - MixfixModule::printCondition(output, condition); + MixfixModule::printCondition(output, condition, commentSettings); } - output << " .\n%\n\\end{comment}\n"; - Tty::unblockEscapeSequences(); + endComment(); // // Print latex version of command. // @@ -426,10 +438,10 @@ MaudeLatexBuffer::generateLoopTokens(bool showCommand, const Vector& toke // // Print comment. // - output << "\\begin{comment}\n%\n% loop tokens: ("; + output << "% loop tokens: ("; int nrTokens = tokens.size(); // might be 0 so must be signed Token::printTokenVector(output, tokens, 0, nrTokens - 1, true); - output << ")\n%\n\\end{comment}\n"; + output << ")\n%\n"; // // Print latex version. // @@ -450,11 +462,11 @@ MaudeLatexBuffer::generateCommand(bool showCommand, const string& command, Term* // // Print comment. // - Tty::blockEscapeSequences(); - output << "\\begin{comment}\n%\n% " << command << " "; + startComment(); + output << command << " "; safeCastNonNull(module)->printModifiers(output); - output << subject << " .\n%\n\\end{comment}\n"; - Tty::unblockEscapeSequences(); + commentTerm(subject); + endComment(); // // Print latex version of command. // @@ -482,11 +494,16 @@ MaudeLatexBuffer::generateCommand(bool showCommand, // // Print comment. // - Tty::blockEscapeSequences(); - output << "\\begin{comment}\n%\n% " << command << " "; + startComment(); + output << command << " "; safeCastNonNull(module)->printModifiers(output, number, number2); - output << subject << " .\n%\n\\end{comment}\n"; - Tty::unblockEscapeSequences(); + commentDagNode(subject); + if (strategy != nullptr) + { + output << " using "; + MixfixModule::prettyPrint(output, strategy, UNBOUNDED, commentSettings); + } + endComment(); // // Print latex version of command. // @@ -496,7 +513,7 @@ MaudeLatexBuffer::generateCommand(bool showCommand, output << "$\\maudeKeyword{" << command << "}\\maudeSpace"; generateModifiers(module, number, number2); MixfixModule::latexPrintDagNode(output, subject); - if (strategy != 0) + if (strategy != nullptr) { output << "\\maudeSpace\\maudeKeyword{using}\\maudeSpace"; safeCastNonNull(subject->symbol()->getModule())->latexPrintStrategy(output, strategy); @@ -510,10 +527,11 @@ MaudeLatexBuffer::generateCommand(bool showCommand, void MaudeLatexBuffer::generateContinue(bool showCommand, Int64 limit, bool debug) { - string command = debug ? "debug continue" : "continue"; - Tty::blockEscapeSequences(); - output << "\\begin{comment}\n%\n% " << command << " " << limit << " .\n%\n\\end{comment}\n\\begin{maudeResultParagraph}\n"; - Tty::unblockEscapeSequences(); + string command = debug ? "debug continue" : "continue"; + startComment(); + output << command << " " << limit; + endComment(); + output << "\\begin{maudeResultParagraph}\n"; if (showCommand) output << "\\maudeKeyword{" << command << "} \\maudeNumber{" << limit << "}\\maudeEndCommand\n"; // @@ -526,12 +544,15 @@ MaudeLatexBuffer::generateContinue(bool showCommand, Int64 limit, bool debug) void MaudeLatexBuffer::generateShow(bool showCommand, const string& command, NamedEntity* module) { - output << "\\begin{comment}\n%\n% " << command << " " << module << " .\n%\n\\end{comment}\n\\begin{maudeShowParagraph}"; + startComment(); + output << command << " " << module; + endComment(); + output << "\\begin{maudeShowParagraph}"; if (showCommand) { output << "\\maudeKeyword{" << command << "}\\maudeSpace"; generateModuleName(module); - output << "\\maudeEndCommand\\newline\n"; + output << "\\maudeEndCommand\\maudeShowSpace\n"; } pendingCloseStack.push("\\end{maudeShowParagraph}\n%\n% End of " + command + "\n%\n"); } @@ -539,17 +560,23 @@ MaudeLatexBuffer::generateShow(bool showCommand, const string& command, NamedEnt void MaudeLatexBuffer::generateShow(bool showCommand, const string& command, View* view) { - output << "\\begin{comment}\n%\n% " << command << " " << view << " .\n%\n\\end{comment}\n\\begin{maudeShowParagraph}"; + startComment(); + output << command << " " << view; + endComment(); + output << "\\begin{maudeShowParagraph}"; if (showCommand) - output << "\\maudeKeyword{" << command << "}\\maudeSpace\\maudeView{" << view << "}\\maudeEndCommand\\newline\n"; + output << "\\maudeKeyword{" << command << "}\\maudeSpace\\maudeView{" << view << "}\\maudeEndCommand\\maudeShowSpace\n"; pendingCloseStack.push("\\end{maudeShowParagraph}\n%\n% End of " + command + "\n%\n"); } void MaudeLatexBuffer::generateShow(bool showCommand, const string& command) { - output << "\\begin{comment}\n%\n% " << command << " .\n%\n\\end{comment}\n\\begin{maudeShowParagraph}"; + startComment(); + output << command; + endComment(); + output << "\\begin{maudeShowParagraph}"; if (showCommand) - output << "\\maudeKeyword{" << command << "}\\maudeEndCommand\\newline\n"; + output << "\\maudeKeyword{" << command << "}\\maudeEndCommand\\maudeShowSpace\n"; pendingCloseStack.push("\\end{maudeShowParagraph}\n%\n% End of " + command + "\n%\n"); } diff --git a/src/Mixfix/latexCommon.cc b/src/Mixfix/latexCommon.cc index dbba9f6f..685eb72d 100644 --- a/src/Mixfix/latexCommon.cc +++ b/src/Mixfix/latexCommon.cc @@ -31,6 +31,8 @@ const char* MixfixModule::latexMagenta = "\\color{magenta}"; const char* MixfixModule::latexYellow = "\\color{yellow}"; const char* MixfixModule::latexResetColor = "\\color{black}"; +const char* MixfixModule::restoreColor = ""; + string MixfixModule::latexNumber(const mpz_class& number) { @@ -209,12 +211,19 @@ MixfixModule::latexPrettyOpName(int code, int situations) { // // We have a problem. If we're concerned about BARE_COLON we're in an op-hook and we return the single token - // ugly name. Otherwise we just put a set of parentheses around the pretty name. + // ugly name. Otherwise we just put a set of parentheses around the pretty name if it exists or the original + // name if it doesn't. For original names we use Token::latexIdentifier() which may use a different font. // - return (situations & Token::BARE_COLON) ? ("\\maudeSymbolic{" + Token::latexName(code) + "}") : - ("\\maudeLeftParen\\maudeSymbolic{" + Token::latexName(pair.first) + "}\\maudeRightParen"); + if (situations & Token::BARE_COLON) + return Token::latexIdentifier(code); + string nameToUse = pair.first.empty() ? Token::latexIdentifier(code) : ("\\maudeSymbolic{" + Token::latexName(pair.first) + "}"); + return "\\maudeLeftParen" + nameToUse + "\\maudeRightParen"; } - return ("\\maudeSymbolic{" + Token::latexName(pair.first) + "}"); + // + // If we didn't prettify the name, use Token::latexIdentifier() on the original name; otherwise print the + // the prettified name using \maudeSymbolic. + // + return pair.first.empty() ? Token::latexIdentifier(code) : ("\\maudeSymbolic{" + Token::latexName(pair.first) + "}"); } void @@ -286,7 +295,7 @@ MixfixModule::latexFancySpace(ostream& s, int spaceToken, const PrintSettings& p } case 'n': { - s << "\\maudeNewline"; + s << "\\maudeNewline" << restoreColor; // a newline will lose the current color space = true; break; } @@ -320,38 +329,38 @@ MixfixModule::latexFancySpace(ostream& s, int spaceToken, const PrintSettings& p { case 'r': { - s << "\\color{red}"; + s << (restoreColor = latexRed); break; } case 'g': { - s << "\\color{green}"; + s << (restoreColor = latexGreen); break; } case 'b': { - s << "\\color{blue}"; + s << (restoreColor = latexBlue); break; } case 'c': { - s << "\\color{cyan}"; + s << (restoreColor = latexCyan); break; } case 'm': { - s << "\\color{magenta}"; + s << (restoreColor = latexMagenta); break; } case 'y': { - s << "\\color{yellow}"; + s << (restoreColor = latexYellow); break; } case 'p': case 'o': { - s << "\\color{black}"; + latexClearColor(s); break; } } @@ -362,11 +371,6 @@ MixfixModule::latexFancySpace(ostream& s, int spaceToken, const PrintSettings& p case m: { s << Tty(Tty::t); attributeUsed = true; break; } #include "ansiEscapeSequences.cc" #undef MACRO - case 'o': - { - s << Tty(Tty::RESET); - break; - } } */ } @@ -671,38 +675,38 @@ MixfixModule::latexPrintBubble(ostream& s, const Vector& bubble) } case 'r': { - s << "\\color{red}"; + s << latexRed; continue; } case 'g': { - s << "\\color{green}"; + s << latexGreen; continue; } case 'b': { - s << "\\color{blue}"; + s << latexBlue; continue; } case 'c': { - s << "\\color{cyan}"; + s << latexCyan; continue; } case 'm': { - s << "\\color{magenta}"; + s << latexMagenta; continue; } case 'y': { - s << "\\color{yellow}"; + s << latexYellow; continue; } case 'p': case 'o': { - s << "\\color{black}"; + s << latexResetColor; continue; } } diff --git a/src/Mixfix/latexDagNodePrint.cc b/src/Mixfix/latexDagNodePrint.cc index b13f0058..a1eaa717 100644 --- a/src/Mixfix/latexDagNodePrint.cc +++ b/src/Mixfix/latexDagNodePrint.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 2023-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -24,38 +24,6 @@ // DagNode* -> ostream& LaTeX pretty printer. // -void -MixfixModule::latexPrettyPrint(ostream& s, DagNode* dagNode) -{ - if (dagNode == 0) - { - s << "\\maudeMisc{(null DagNode*)}"; - return; - } - const PrintSettings& printSettings = interpreter; // HACK - MixfixModule* module = static_cast(dagNode->symbol()->getModule()); - if (printSettings.getPrintFlag(PrintSettings::PRINT_GRAPH)) - { - s << "$"; - module->latexGraphPrint(s, dagNode, printSettings); - s << "$"; - } - else - { - clearIndent(); - s << "$"; - ColoringInfo coloringInfo; - if (printSettings.getPrintFlag(PrintSettings::PRINT_COLOR)) - { - computeGraphStatus(dagNode, coloringInfo.visited, coloringInfo.statusVec); - coloringInfo.reducedAbove = false; - coloringInfo.reducedDirectlyAbove = false; - } - module->latexPrettyPrint(s, printSettings, coloringInfo, dagNode, UNBOUNDED, UNBOUNDED, 0, UNBOUNDED, 0, false); - s << "$"; - } -} - void MixfixModule::latexPrintDagNode(ostream& s, DagNode* dagNode) { @@ -74,6 +42,7 @@ MixfixModule::latexPrintDagNode(ostream& s, DagNode* dagNode) coloringInfo.reducedDirectlyAbove = false; } module->latexPrettyPrint(s, printSettings, coloringInfo, dagNode, UNBOUNDED, UNBOUNDED, 0, UNBOUNDED, 0, false); + latexClearColor(s); } } diff --git a/src/Mixfix/latexModulePrint.cc b/src/Mixfix/latexModulePrint.cc index 10e5f841..d269060a 100644 --- a/src/Mixfix/latexModulePrint.cc +++ b/src/Mixfix/latexModulePrint.cc @@ -424,9 +424,8 @@ VisibleModule::latexShowDecls(ostream& s, const char* indent, Index index, bool void VisibleModule::latexShowOps(ostream& s, const char* indent, bool all) { - Index begin = all ? 0 : getNrImportedSymbols(); Index end = getNrUserSymbols(); - for (Index i = begin; i < end; ++i) + for (Index i = 0; i < end; ++i) { if (UserLevelRewritingContext::interrupted()) return; diff --git a/src/Mixfix/latexResult.cc b/src/Mixfix/latexResult.cc index b378e9c5..5c756d20 100644 --- a/src/Mixfix/latexResult.cc +++ b/src/Mixfix/latexResult.cc @@ -253,7 +253,9 @@ MaudeLatexBuffer::generateSearchPath(const RewriteSequenceSearch* graph, // // Print comment. // - output << "\\begin{comment}\n%\n% " << command << " " << stateNr << " .\n%\n\\end{comment}\n"; + startComment(); + output << command << " " << stateNr; + endComment(); // // Print latex version of command. // @@ -304,7 +306,9 @@ MaudeLatexBuffer::generateSearchPathLabels(const RewriteSequenceSearch* graph, // // Print comment. // - output << "\\begin{comment}\n%\n% show path labels " << stateNr << " .\n%\n\\end{comment}\n"; + startComment(); + output << "show path labels " << stateNr; + endComment(); // // Print latex version of command. // @@ -334,7 +338,12 @@ MaudeLatexBuffer::generateSearchPathLabels(const RewriteSequenceSearch* graph, void MaudeLatexBuffer::generateSearchGraph(const RewriteSequenceSearch* graph, bool showCommand) { - output << "\\begin{comment}\n%\n% show graph .\n%\n\\end{comment}\n"; + // + // Print comment. + // + startComment(); + output << "show graph"; + endComment(); // // Print latex version of command. // diff --git a/src/Mixfix/latexTermPrint.cc b/src/Mixfix/latexTermPrint.cc index 13b2674a..6a461237 100644 --- a/src/Mixfix/latexTermPrint.cc +++ b/src/Mixfix/latexTermPrint.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 2023-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -31,6 +31,7 @@ MixfixModule::latexPrettyPrint(ostream& s, Term* term, bool rangeKnown) const PrintSettings& printSettings = interpreter; // HACK MixfixModule* module = safeCastNonNull(term->symbol()->getModule()); module->latexPrettyPrint(s, printSettings, term, UNBOUNDED, UNBOUNDED, 0, UNBOUNDED, 0, rangeKnown); + latexClearColor(s); } void diff --git a/src/Mixfix/match.cc b/src/Mixfix/match.cc index 345473dd..9e2bb107 100644 --- a/src/Mixfix/match.cc +++ b/src/Mixfix/match.cc @@ -74,7 +74,7 @@ Interpreter::match(const Vector& bubble, bool withExtension, Int64 limit) if (condition.length() > 0) { cout << " such that "; - MixfixModule::printCondition(cout, condition); + MixfixModule::printCondition(cout, condition, *this); } cout << " ." << endl; } diff --git a/src/Mixfix/maudeLatexBuffer.cc b/src/Mixfix/maudeLatexBuffer.cc index dffda82b..56a21f33 100644 --- a/src/Mixfix/maudeLatexBuffer.cc +++ b/src/Mixfix/maudeLatexBuffer.cc @@ -117,7 +117,8 @@ #include "latexResult.cc" MaudeLatexBuffer::MaudeLatexBuffer(const char* fileName) -: output(fileName) +: output(fileName), + commentSettings(PrintSettings::PLAIN_PRINT_FLAGS) // no color, format or graph printing in comments { needNewline = false; output << "\\documentclass{article}\n"; diff --git a/src/Mixfix/maudeLatexBuffer.hh b/src/Mixfix/maudeLatexBuffer.hh index ccb72053..50cedd13 100644 --- a/src/Mixfix/maudeLatexBuffer.hh +++ b/src/Mixfix/maudeLatexBuffer.hh @@ -183,11 +183,16 @@ public: void cleanUp(); private: + void commentTerm(Term* t); + void commentDagNode(DagNode* d); + void startComment(); + void endComment(); void generateType(Sort* sort); void generateModifiers(Module* module, int64_t number = NONE, int64_t number2 = NONE); + ofstream output; - //string pendingClose; + PrintSettings commentSettings; // for terms and dagnodes printed in comments stack pendingCloseStack; bool needNewline; }; @@ -211,4 +216,28 @@ MaudeLatexBuffer::generateHeading(const char* message) output << "\\par\\maudeResponse{" << message << "}\n"; } +inline void +MaudeLatexBuffer::commentTerm(Term* t) +{ + MixfixModule::prettyPrint(output, t, commentSettings, false); +} + +inline void +MaudeLatexBuffer::commentDagNode(DagNode* d) +{ + MixfixModule::prettyPrint(output, d, commentSettings, false); +} + +inline void +MaudeLatexBuffer::startComment() +{ + output << "%\n% "; +} + +inline void +MaudeLatexBuffer::endComment() +{ + output << " .\n%\n"; +} + #endif diff --git a/src/Mixfix/mixfixModule.hh b/src/Mixfix/mixfixModule.hh index 01b42e7d..2d39a2a2 100644 --- a/src/Mixfix/mixfixModule.hh +++ b/src/Mixfix/mixfixModule.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -146,8 +146,10 @@ public: DagNode* makeUnificationProblemDag(Vector& lhs, Vector& rhs); pair makeMatchProblemDags(Vector& lhs, Vector& rhs); - static void printCondition(ostream& s, const Vector& condition); - static void printCondition(ostream& s, const PreEquation* pe); + static void printConditionFragment(ostream& s, const ConditionFragment* cf, const PrintSettings& printSettings); + static void printCondition(ostream& s, const Vector& condition, const PrintSettings& printSettings); + static void printCondition(ostream& s, const PreEquation* pe, const PrintSettings& printSettings); + void printAttributes(ostream& s, const PreEquation* pe, ItemType itemType, const PrintSettings& printSettings); void printStrategyTerm(ostream& s, RewriteStrategy* strat, Term* term); // @@ -287,7 +289,7 @@ public: void printModifiers(ostream& s, Int64 number = NONE, Int64 number2 = NONE); static void prettyPrint(ostream& s, const Term* term, const PrintSettings& printSettings, bool rangeKnown = false); static void prettyPrint(ostream& s, DagNode* dagNode, const PrintSettings& printSettings, bool rangeKnown = false); - static bool prettyPrint(ostream& s, StrategyExpression* strategy, int requiredPrec); + static bool prettyPrint(ostream& s, StrategyExpression* strategy, int requiredPrec, const PrintSettings& printSettings); static void clearIndent(); static void clearColor(ostream& s); static string prettyOpName(int code, int situations = Token::UNKNOWN_CONTEXT); @@ -311,7 +313,6 @@ public: // // Latex pretty print functions. // - static void latexPrettyPrint(ostream& s, DagNode* dagNode); static void latexPrettyPrint(ostream& s, Term* term, bool rangeKnown = false); static void latexPrintDagNode(ostream& s, DagNode* dagNode); static void latexPrintGather(ostream& s, const Vector& gather); @@ -703,6 +704,7 @@ private: static Vector gatherAny0; static int globalIndent; static bool attributeUsed; + static const char* restoreColor; ModuleType moduleType; Sort* boolSort; @@ -891,43 +893,44 @@ private: // Member functions for Term* -> ostream& pretty printer. // static const char* computeColor(SymbolType st, const PrintSettings& printSettings); - static void suffix(ostream& s, Term* term, bool needDisambig); + static void suffix(ostream& s, const Term* term, bool needDisambig); bool handleIter(ostream& s, - Term* term, + const Term* term, SymbolInfo& si, bool rangeKnown, const PrintSettings& printSettings); - bool handleMinus(ostream& s, Term* term, + bool handleMinus(ostream& s, + const Term* term, bool rangeKnown, const PrintSettings& printSettings); bool handleDivision(ostream& s, - Term* term, + const Term* term, bool rangeKnown, const PrintSettings& printSettings); void handleFloat(ostream& s, - Term* term, + const Term* term, bool rangeKnown, const PrintSettings& printSettings); void handleString(ostream& s, - Term* term, + const Term* term, bool rangeKnown, const PrintSettings& printSettings); void handleQuotedIdentifier(ostream& s, - Term* term, + const Term* term, bool rangeKnown, const PrintSettings& printSettings); void handleVariable(ostream& s, - Term* term, + const Term* term, bool rangeKnown, const PrintSettings& printSettings); void handleSMT_Number(ostream& s, - Term* term, + const Term* term, bool rangeKnown, const PrintSettings& printSettings); public: void prettyPrint(ostream& s, const PrintSettings& printSettings, - Term* term, + const Term* term, int requiredPrec, int leftCapture, const ConnectedComponent* leftCaptureComponent, @@ -952,6 +955,7 @@ private: const PrintSettings& printSettings); static bool latexFancySpace(ostream& s, int spaceToken, const PrintSettings& printSettings); void latexPrintStructuredConstant(ostream& s, Symbol* symbol, const char* color, const PrintSettings& printSettings) const; + static void latexClearColor(ostream& s); // // Member functions for Term* -> LaTeX pretty printer. // @@ -1319,6 +1323,19 @@ MixfixModule::clearColor(ostream& s) } } +inline void +MixfixModule::latexClearColor(ostream& s) +{ + if (*restoreColor != '\0') + { + // + // If we are printing in color, reset the color to black. + // + restoreColor = ""; + s << latexResetColor; + } +} + inline string MixfixModule::latexString(int code) { diff --git a/src/Mixfix/prettyPrint.cc b/src/Mixfix/prettyPrint.cc index b05f3e35..0481aea2 100644 --- a/src/Mixfix/prettyPrint.cc +++ b/src/Mixfix/prettyPrint.cc @@ -32,7 +32,7 @@ MixfixModule::prettyPrint(ostream& s, const Term* term, const PrintSettings& pri { clearIndent(); MixfixModule* parentModule = safeCastNonNull(term->symbol()->getModule()); - parentModule->prettyPrint(s, printSettings, const_cast(term), UNBOUNDED, UNBOUNDED, 0, UNBOUNDED, 0, rangeKnown); + parentModule->prettyPrint(s, printSettings, term, UNBOUNDED, UNBOUNDED, 0, UNBOUNDED, 0, rangeKnown); clearColor(s); } @@ -44,22 +44,22 @@ MixfixModule::prettyPrint(ostream& s, DagNode* dagNode, const PrintSettings& pri s << "(null DagNode*)"; return; } - MixfixModule::clearIndent(); + clearIndent(); MixfixModule* module = safeCastNonNull(dagNode->symbol()->getModule()); if (printSettings.getPrintFlag(PrintSettings::PRINT_GRAPH)) module->graphPrint(s, dagNode, printSettings); else { - MixfixModule::ColoringInfo coloringInfo; + ColoringInfo coloringInfo; if (printSettings.getPrintFlag(PrintSettings::PRINT_COLOR)) { - MixfixModule::computeGraphStatus(dagNode, coloringInfo.visited, coloringInfo.statusVec); + computeGraphStatus(dagNode, coloringInfo.visited, coloringInfo.statusVec); coloringInfo.reducedAbove = false; coloringInfo.reducedDirectlyAbove = false; } module->prettyPrint(s, coloringInfo, printSettings, dagNode, UNBOUNDED, UNBOUNDED, 0, UNBOUNDED, 0, rangeKnown); } - MixfixModule::clearColor(s); + clearColor(s); } void @@ -143,22 +143,52 @@ MixfixModule::printStrategyTerm(ostream& s, RewriteStrategy* strat, Term* term) } void -MixfixModule::printCondition(ostream& s, const Vector& condition) +MixfixModule::printConditionFragment(ostream& s, const ConditionFragment* cf, const PrintSettings& printSettings) { - int nrFragments = condition.length(); - for (int i = 0; i < nrFragments; i++) + if (const EqualityConditionFragment* e = dynamic_cast(cf)) { - s << condition[i]; - if (i + 1 < nrFragments) - s << " /\\ "; + prettyPrint(s, e->getLhs(), printSettings, false); + s << " = "; + prettyPrint(s, e->getRhs(), printSettings, true); } + else if (const SortTestConditionFragment* t = dynamic_cast(cf)) + { + prettyPrint(s, t->getLhs(), printSettings, true); + s << " : " << t->getSort(); + } + else if(const AssignmentConditionFragment* a = dynamic_cast(cf)) + { + prettyPrint(s, a->getLhs(), printSettings, false); + s << " := "; + prettyPrint(s, a->getRhs(), printSettings, true); + } + else if(const RewriteConditionFragment* r = dynamic_cast(cf)) + { + prettyPrint(s, r->getLhs(), printSettings, false); + s << " => "; + prettyPrint(s, r->getRhs(), printSettings, true); + } + else + CantHappen("bad condition fragment"); } void -MixfixModule::printCondition(ostream& s, const PreEquation* pe) +MixfixModule::printCondition(ostream& s, const Vector& condition, const PrintSettings& printSettings) +{ + const char* sep = ""; + for (ConditionFragment* cf : condition) + { + s << sep; + sep = " /\\ "; + printConditionFragment(s, cf, printSettings); + } +} + +void +MixfixModule::printCondition(ostream& s, const PreEquation* pe, const PrintSettings& printSettings) { s << " if "; - printCondition(s, pe->getCondition()); + printCondition(s, pe->getCondition(), printSettings); } void @@ -435,9 +465,16 @@ MixfixModule::prettyOpName(int code, int situations) { // // We have a problem. If we're concerned about BARE_COLON we're in an op-hook and we return the single token - // ugly name. Otherwise we just put a set of parentheses around the pretty name. + // ugly name. Otherwise we just put a set of parentheses around the pretty name if it exists or the regular + // name if it doesn't. // - return (situations & Token::BARE_COLON) ? Token::name(code) : ("(" + pair.first + ")"); + if (situations & Token::BARE_COLON) + return Token::name(code); + string nameToUse = pair.first.empty() ? Token::name(code) : pair.first; + return "(" + nameToUse + ")"; } - return pair.first; + // + // If we didn't prettify the name, return the original name. + // + return pair.first.empty() ? Token::name(code) : pair.first; } diff --git a/src/Mixfix/printSettings.hh b/src/Mixfix/printSettings.hh index 6e3cb57a..f2aa384c 100644 --- a/src/Mixfix/printSettings.hh +++ b/src/Mixfix/printSettings.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 2023-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -55,8 +55,14 @@ public: PRINT_RAT = 0x800, // for rats PRINT_HOOKS = 0x1000, // for built-ins PRINT_COMBINE_VARS = 0x2000, // for variables - - DEFAULT_PRINT_FLAGS = PRINT_FORMAT | PRINT_MIXFIX | PRINT_WITH_ALIASES | PRINT_FLAT | PRINT_NUMBER | PRINT_RAT | PRINT_HOOKS + // + // Default settings for Maude interpreter. + // + DEFAULT_PRINT_FLAGS = PRINT_FORMAT | PRINT_MIXFIX | PRINT_WITH_ALIASES | PRINT_FLAT | PRINT_NUMBER | PRINT_RAT | PRINT_HOOKS, + // + // Turn off formatting where it could cause issues. + // + PLAIN_PRINT_FLAGS = PRINT_MIXFIX | PRINT_WITH_ALIASES | PRINT_FLAT | PRINT_NUMBER | PRINT_RAT | PRINT_HOOKS }; PrintSettings(PrintFlags initialValue = PRINT_CLEARED_FLAGS); diff --git a/src/Mixfix/quotedIdentifierOpSymbol.cc b/src/Mixfix/quotedIdentifierOpSymbol.cc index 45344b79..e3dc8a86 100644 --- a/src/Mixfix/quotedIdentifierOpSymbol.cc +++ b/src/Mixfix/quotedIdentifierOpSymbol.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -292,9 +292,9 @@ QuotedIdentifierOpSymbol::eqRewrite(DagNode* subject, RewritingContext& context) DagNode* QuotedIdentifierOpSymbol::makeQid(int id, PointerMap& qidMap) { - void* p = const_cast(static_cast(Token::name(id))); - DagNode *d = static_cast(qidMap.getMap(p)); - if (d == 0) + const void* p = Token::name(id); + DagNode* d = static_cast(qidMap.getMap(p)); + if (d == nullptr) { d = new QuotedIdentifierDagNode(quotedIdentifierSymbol, Token::backQuoteSpecials(id)); (void) qidMap.setMap(p, d); @@ -302,7 +302,6 @@ QuotedIdentifierOpSymbol::makeQid(int id, PointerMap& qidMap) return d; } - bool QuotedIdentifierOpSymbol::printQidList(DagNode* qidList, Rope& output) { diff --git a/src/Mixfix/search.cc b/src/Mixfix/search.cc index 5bc454c1..9b988ca9 100644 --- a/src/Mixfix/search.cc +++ b/src/Mixfix/search.cc @@ -189,7 +189,7 @@ Interpreter::search(const Vector& bubble, if (!condition.empty()) { cout << " such that "; - MixfixModule::printCondition(cout, condition); + MixfixModule::printCondition(cout, condition, *this); } cout << " ." << endl; diff --git a/src/Mixfix/strategyPrint.cc b/src/Mixfix/strategyPrint.cc index 875f9a51..b0391ef5 100644 --- a/src/Mixfix/strategyPrint.cc +++ b/src/Mixfix/strategyPrint.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -29,15 +29,8 @@ // know about these details. // -ostream& -operator<<(ostream& s, StrategyExpression* strategy) -{ - (void) MixfixModule::prettyPrint(s, strategy, UNBOUNDED); - return s; -} - bool -MixfixModule::prettyPrint(ostream& s, StrategyExpression* strategy, int requiredPrec) +MixfixModule::prettyPrint(ostream& s, StrategyExpression* strategy, int requiredPrec, const PrintSettings& printSettings) { bool needParen = false; bool needSpace = true; @@ -99,7 +92,7 @@ MixfixModule::prettyPrint(ostream& s, StrategyExpression* strategy, int required int nrStrategies = strategies.size(); for (int i = 0;;) { - (void) prettyPrint(s, strategies[i], STRAT_SEQ_PREC); + (void) prettyPrint(s, strategies[i], STRAT_SEQ_PREC, printSettings); if (++i == nrStrategies) break; s << " ; "; @@ -114,7 +107,7 @@ MixfixModule::prettyPrint(ostream& s, StrategyExpression* strategy, int required int nrStrategies = strategies.size(); for (int i = 0;;) { - (void) prettyPrint(s, strategies[i], STRAT_UNION_PREC); + (void) prettyPrint(s, strategies[i], STRAT_UNION_PREC, printSettings); if (++i == nrStrategies) break; s << " | "; @@ -122,7 +115,7 @@ MixfixModule::prettyPrint(ostream& s, StrategyExpression* strategy, int required } else if (IterationStrategy* i = dynamic_cast(strategy)) { - if (prettyPrint(s, i->getStrategy(), 0)) + if (prettyPrint(s, i->getStrategy(), 0, printSettings)) s << ' '; s << (i->getZeroAllowed() ? '*' : '+'); } @@ -161,9 +154,9 @@ MixfixModule::prettyPrint(ostream& s, StrategyExpression* strategy, int required needParen = requiredPrec < STRAT_ORELSE_PREC; if (needParen) s << '('; - (void) prettyPrint(s, b->getInitialStrategy(), STRAT_ORELSE_PREC); + (void) prettyPrint(s, b->getInitialStrategy(), STRAT_ORELSE_PREC, printSettings); s << " or-else "; - (void) prettyPrint(s, b->getFailureStrategy(), STRAT_ORELSE_PREC); + (void) prettyPrint(s, b->getFailureStrategy(), STRAT_ORELSE_PREC, printSettings); } break; } @@ -173,11 +166,11 @@ MixfixModule::prettyPrint(ostream& s, StrategyExpression* strategy, int required needParen = requiredPrec < STRAT_BRANCH_PREC; if (needParen) s << '('; - (void) prettyPrint(s, b->getInitialStrategy(), STRAT_BRANCH_PREC); + (void) prettyPrint(s, b->getInitialStrategy(), STRAT_BRANCH_PREC, printSettings); s << " ? "; - (void) prettyPrint(s, b->getSuccessStrategy(), STRAT_BRANCH_PREC); + (void) prettyPrint(s, b->getSuccessStrategy(), STRAT_BRANCH_PREC, printSettings); s << " : "; - (void) prettyPrint(s, b->getFailureStrategy(), STRAT_BRANCH_PREC); + (void) prettyPrint(s, b->getFailureStrategy(), STRAT_BRANCH_PREC, printSettings); break; } case BranchStrategy::ITERATE: @@ -185,7 +178,7 @@ MixfixModule::prettyPrint(ostream& s, StrategyExpression* strategy, int required Assert(b->getFailureAction() == BranchStrategy::IDLE && b->getSuccessStrategy() == 0 && b->getFailureStrategy() == 0, "unknown branch strategy"); - if (prettyPrint(s, b->getInitialStrategy(), 0)) + if (prettyPrint(s, b->getInitialStrategy(), 0, printSettings)) s << ' '; s << '!'; break; @@ -207,7 +200,7 @@ MixfixModule::prettyPrint(ostream& s, StrategyExpression* strategy, int required if (!condition.empty()) { s << " such that "; - printCondition(s, condition); + printCondition(s, condition, printSettings); } } else if (SubtermStrategy* t = dynamic_cast(strategy)) @@ -223,7 +216,7 @@ MixfixModule::prettyPrint(ostream& s, StrategyExpression* strategy, int required if (!condition.empty()) { s << " such that "; - printCondition(s, condition); + printCondition(s, condition, printSettings); } const Vector& subterms = t->getSubterms(); const Vector& strategies = t->getStrategies(); @@ -232,7 +225,7 @@ MixfixModule::prettyPrint(ostream& s, StrategyExpression* strategy, int required { s << ((i == 0) ? " by " : ", "); s << subterms[i] << " using "; - (void) prettyPrint(s, strategies[i], STRAT_USING_PREC - 1); + (void) prettyPrint(s, strategies[i], STRAT_USING_PREC - 1, printSettings); } } else if (CallStrategy* t = dynamic_cast(strategy)) diff --git a/src/Mixfix/termPrint.cc b/src/Mixfix/termPrint.cc index 72e8fbea..9709c8d0 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-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -55,7 +55,7 @@ MixfixModule::computeColor(SymbolType st, const PrintSettings& printSettings) } void -MixfixModule::suffix(ostream& s, Term* term, bool needDisambig) +MixfixModule::suffix(ostream& s, const Term* term, bool needDisambig) { if (needDisambig) s << ")." << disambiguatorSort(term); @@ -63,7 +63,7 @@ MixfixModule::suffix(ostream& s, Term* term, bool needDisambig) bool MixfixModule::handleIter(ostream& s, - Term* term, + const Term* term, SymbolInfo& si, bool rangeKnown, const PrintSettings& printSettings) @@ -85,7 +85,7 @@ MixfixModule::handleIter(ostream& s, return true; } } - S_Term* st = safeCast(S_Term*, term); + const S_Term* st = safeCast(const S_Term*, term); const mpz_class& number = st->getNumber(); if (number == 1) return false; // do default thing @@ -109,7 +109,7 @@ MixfixModule::handleIter(ostream& s, bool MixfixModule::handleMinus(ostream& s, - Term* term, + const Term* term, bool rangeKnown, const PrintSettings& printSettings) { @@ -133,7 +133,7 @@ MixfixModule::handleMinus(ostream& s, bool MixfixModule::handleDivision(ostream& s, - Term* term, + const Term* term, bool rangeKnown, const PrintSettings& printSettings) { @@ -157,11 +157,11 @@ MixfixModule::handleDivision(ostream& s, void MixfixModule::handleFloat(ostream& s, - Term* term, + const Term* term, bool rangeKnown, const PrintSettings& printSettings) { - double mfValue = safeCast(FloatTerm*, term)->getValue(); + double mfValue = safeCast(const FloatTerm*, term)->getValue(); bool needDisambig = printSettings.getPrintFlag(PrintSettings::PRINT_DISAMBIG_CONST) || (!rangeKnown && (floatSymbols.size() > 1 || overloadedFloats.count(mfValue))); prefix(s, needDisambig); @@ -171,12 +171,12 @@ MixfixModule::handleFloat(ostream& s, void MixfixModule::handleString(ostream& s, - Term* term, + const Term* term, bool rangeKnown, const PrintSettings& printSettings) { string strValue; - Token::ropeToString(safeCast(StringTerm*, term)->getValue(), strValue); + Token::ropeToString(safeCast(const StringTerm*, term)->getValue(), strValue); bool needDisambig = printSettings.getPrintFlag(PrintSettings::PRINT_DISAMBIG_CONST) || (!rangeKnown && (stringSymbols.size() > 1 || overloadedStrings.count(strValue))); prefix(s, needDisambig); @@ -186,11 +186,11 @@ MixfixModule::handleString(ostream& s, void MixfixModule::handleQuotedIdentifier(ostream& s, - Term* term, + const Term* term, bool rangeKnown, const PrintSettings& printSettings) { - int qidCode = safeCast(QuotedIdentifierTerm*, term)->getIdIndex(); + int qidCode = safeCast(const QuotedIdentifierTerm*, term)->getIdIndex(); bool needDisambig = printSettings.getPrintFlag(PrintSettings::PRINT_DISAMBIG_CONST) || (!rangeKnown && (quotedIdentifierSymbols.size() > 1 || overloadedQuotedIdentifiers.count(qidCode))); prefix(s, needDisambig); @@ -200,11 +200,11 @@ MixfixModule::handleQuotedIdentifier(ostream& s, void MixfixModule::handleVariable(ostream& s, - Term* term, + const Term* term, bool rangeKnown, const PrintSettings& printSettings) { - VariableTerm* v = safeCast(VariableTerm*, term); + const VariableTerm* v = safeCast(const VariableTerm*, term); Sort* sort = safeCast(VariableSymbol*, term->symbol())->getSort(); pair p(v->id(), sort->id()); bool needDisambig = !rangeKnown && overloadedVariables.count(p); // kinds not handled @@ -215,14 +215,14 @@ MixfixModule::handleVariable(ostream& s, void MixfixModule::handleSMT_Number(ostream& s, - Term* term, + const Term* term, bool rangeKnown, const PrintSettings& printSettings) { // // Get value. // - SMT_NumberTerm* n = safeCast(SMT_NumberTerm*, term); + const SMT_NumberTerm* n = safeCast(const SMT_NumberTerm*, term); const mpq_class& value = n->getValue(); // // Look up the index of our sort. @@ -258,7 +258,7 @@ MixfixModule::handleSMT_Number(ostream& s, void MixfixModule::prettyPrint(ostream& s, const PrintSettings& printSettings, - Term* term, + const Term* term, int requiredPrec, int leftCapture, const ConnectedComponent* leftCaptureComponent, diff --git a/src/Mixfix/token.cc b/src/Mixfix/token.cc index ab634bc8..f4becad7 100644 --- a/src/Mixfix/token.cc +++ b/src/Mixfix/token.cc @@ -236,13 +236,15 @@ Token::makePrettyOpName(int prefixNameCode, int situations) // indicating that the caller needs to wrap the result in parentheses. // // Unbalanced parentheses are always an issue and blocks prettification. - // Having a result that is already wrapped in parenthese is always problematic. + // Having a result that is already wrapped in parentheses is always problematic. + // + // If we don't change the original, flag this by returning the empty string. // const char* original = stringTable.name(prefixNameCode); DebugInfo("original = " << original); int sp = specialProperties[prefixNameCode]; if (sp != NONE && sp != CONTAINS_COLON && sp != ENDS_IN_COLON && sp != ITER_SYMBOL) - return {original, false}; // looks like something that doen't need prettifying + return {"", false}; // looks like something that doen't need prettifying and is unproblematic bool problematic = false; // @@ -257,6 +259,7 @@ Token::makePrettyOpName(int prefixNameCode, int situations) // // Prettify by removing backquotes, checking if we expose problematic tokens outside of parentheses. // + bool prettified = false; string result; int parenDepth = 0; bool disconnected = true; @@ -273,7 +276,7 @@ Token::makePrettyOpName(int prefixNameCode, int situations) { --parenDepth; if (parenDepth < 0) - return {original, false}; // don't prettify unbalanced parentheses - leave as an unproblematic single token + return {"", false}; // don't prettify unbalanced parentheses; single token will not be problematic } if (specialChar(c)) { @@ -296,6 +299,11 @@ Token::makePrettyOpName(int prefixNameCode, int situations) } else result += ' '; // white space + // + // Either we removed a backquote or turned the backquote into a space. + // Both count as prettified. + // + prettified = true; if (!problematic && (situations & MULTIPLE_TOKENS)) { // @@ -336,7 +344,7 @@ Token::makePrettyOpName(int prefixNameCode, int situations) } } if (parenDepth != 0) - return {original, false}; // don't prettify unbalanced parentheses - leave as an unproblematic single token + return {"", false}; // don't prettify unbalanced parentheses; single token will not be problematic // // If the first and last characters of the prettified name are ( and ), they will be eliminated // during parsing which is always problematic. @@ -344,7 +352,10 @@ Token::makePrettyOpName(int prefixNameCode, int situations) if (!problematic && result.front() == '(' && result.back() == ')') problematic = true; DebugInfo("result = " << result << " problematic = " << problematic); - return {result, problematic}; + if (prettified) + return {result, problematic}; + else + return {"", problematic}; } int @@ -640,29 +651,38 @@ Token::splitKind(int code, Vector& codes) const char* p = stringTable.name(code); buffer.resize(strlen(p) + 1); p = strcpy(buffer.data(), p); + // + // A kind must start with `[ + // if (*p++ =='`' && *p++ == '[') { for(;;) { bool dummy; - char *p2 = const_cast(skipSortName(p, dummy)); - if (p2 != 0 && *p2 == '`') + const char* p2 = skipSortName(p, dummy); + if (p2 != nullptr && *p2 == '`') { - *p2 = 0; - codes.append(encode(p)); + // + // Terminator is a backquoted special character. Only `, and `] are legal within a kind. + // + Index length = p2 - p; + for (Index i = 0; i < length; ++i) + buffer[i] = p[i]; + buffer[length] = '\0'; + codes.append(encode(buffer.data())); p = p2 + 1; switch (*p++) { case ']': - { - if (*p == '\0') - return true; - } + return *p == '\0'; // we're good as long as there were no surplus characters case ',': - continue; + continue; // look for another sort name } } - break; + // + // Bad sort name or illegal terminator; return false. + // + return false; } } return false; diff --git a/src/Mixfix/visibleModule.cc b/src/Mixfix/visibleModule.cc index 8afab232..e9ddf171 100644 --- a/src/Mixfix/visibleModule.cc +++ b/src/Mixfix/visibleModule.cc @@ -623,9 +623,8 @@ VisibleModule::showPolymorphDecl(ostream& s, bool indent, int index) const void VisibleModule::showOps(ostream& s, bool indent, bool all) const { - int begin = all ? 0 : getNrImportedSymbols(); int end = getNrUserSymbols(); - for (int i = begin; i < end; i++) + for (int i = 0; i < end; ++i) { if (UserLevelRewritingContext::interrupted()) return; diff --git a/src/NA_Theory/ChangeLog b/src/NA_Theory/ChangeLog index 680f2985..77e615c7 100644 --- a/src/NA_Theory/ChangeLog +++ b/src/NA_Theory/ChangeLog @@ -1,3 +1,11 @@ +2024-03-05 Steven Eker + + * NA_Term.cc (NA_Term::arguments): made const + + * NA_Term.hh (class NA_Term): makde arguments() const + +===================================Maude158=========================================== + 2023-07-24 Steven Eker * NA_Symbol.cc (NA_Symbol::determineGround): added diff --git a/src/NA_Theory/NA_Term.cc b/src/NA_Theory/NA_Term.cc index b74cf5ba..244e0057 100644 --- a/src/NA_Theory/NA_Term.cc +++ b/src/NA_Theory/NA_Term.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -57,7 +57,7 @@ NA_Term::NA_Term(NA_Symbol* symbol) : Term(symbol) } RawArgumentIterator* -NA_Term::arguments() +NA_Term::arguments() const { return 0; } diff --git a/src/NA_Theory/NA_Term.hh b/src/NA_Theory/NA_Term.hh index 0ee7c7fe..527ea5ab 100644 --- a/src/NA_Theory/NA_Term.hh +++ b/src/NA_Theory/NA_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-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -39,7 +39,7 @@ public: // int compareArguments(const Term* other) const // int compareArguments(const DagNode* other) const // - RawArgumentIterator* arguments(); + RawArgumentIterator* arguments() const; void deepSelfDestruct(); void findEagerVariables(bool atTop, NatSet& eagerVariables) const; void analyseConstraintPropagation(NatSet& BoundUniquely) const; diff --git a/src/S_Theory/ChangeLog b/src/S_Theory/ChangeLog index 16103fa0..f29be34b 100755 --- a/src/S_Theory/ChangeLog +++ b/src/S_Theory/ChangeLog @@ -1,3 +1,11 @@ +2024-03-05 Steven Eker + + * S_Term.cc (S_Term::arguments): made const + + * S_Term.hh (class S_Term): made arguments() const + +===================================Maude158=========================================== + 2024-01-16 Steven Eker * S_Symbol.cc (S_Symbol::stackArguments): handle diff --git a/src/S_Theory/S_Term.cc b/src/S_Theory/S_Term.cc index 3266375d..abafbb20 100644 --- a/src/S_Theory/S_Term.cc +++ b/src/S_Theory/S_Term.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -70,7 +70,7 @@ S_Term::S_Term(const S_Term& original, S_Symbol* symbol, SymbolMap* translator) } RawArgumentIterator* -S_Term::arguments() +S_Term::arguments() const { return new S_ArgumentIterator(arg); } diff --git a/src/S_Theory/S_Term.hh b/src/S_Theory/S_Term.hh index 6cc9caea..e2bff27a 100644 --- a/src/S_Theory/S_Term.hh +++ b/src/S_Theory/S_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-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -37,7 +37,7 @@ public: // // Functions required by theory interface. // - RawArgumentIterator* arguments(); + RawArgumentIterator* arguments() const; void deepSelfDestruct(); Term* deepCopy2(SymbolMap* map) const; Term* normalize(bool full, bool& changed); diff --git a/src/StrategyLanguage/ChangeLog b/src/StrategyLanguage/ChangeLog index 249884e7..fdbb4055 100644 --- a/src/StrategyLanguage/ChangeLog +++ b/src/StrategyLanguage/ChangeLog @@ -1,3 +1,30 @@ +2024-03-04 Steven Eker + + * subtermProcess.hh (class SubtermProcess): SharedValue -> shared_ptr + + * applicationProcess.hh (class ApplicationProcess): SharedValue -> + shared_ptr + + * matchProcess.hh (class MatchProcess): SharedValue -> shared_ptr + + * subtermTask.hh (class SubtermTask): SharedValue -> shared_ptr + + * rewriteTask.hh (class RewriteTask): SharedValue -> shared_ptr + + * matchProcess.cc (MatchProcess::MatchProcess): SharedValue -> shared_ptr + + * applicationProcess.cc (ApplicationProcess::doRewrite) + (ApplicationProcess::resolveRemainingConditionFragments): SharedValue -> + shared_ptr + + * rewriteTask.cc (RewriteTask::RewriteTask): SharedValue -> shared_ptr + + * subtermTask.cc (SubtermTask::SubtermTask): SharedValue -> shared_ptr + + * sharedValue.hh: deleted + +===================================Maude158=========================================== + 2024-01-23 Steven Eker * applicationProcess.cc (ApplicationProcess::ApplicationProcess): always diff --git a/src/StrategyLanguage/Makefile.am b/src/StrategyLanguage/Makefile.am index cd358cdf..b5b55eaf 100644 --- a/src/StrategyLanguage/Makefile.am +++ b/src/StrategyLanguage/Makefile.am @@ -60,7 +60,6 @@ noinst_HEADERS = \ strategicSearch.hh \ depthFirstStrategicSearch.hh \ fairStrategicSearch.hh \ - sharedValue.hh \ matchProcess.hh \ subtermProcess.hh \ rewriteTask.hh \ diff --git a/src/StrategyLanguage/Makefile.in b/src/StrategyLanguage/Makefile.in index 0467a252..f04633c2 100644 --- a/src/StrategyLanguage/Makefile.in +++ b/src/StrategyLanguage/Makefile.in @@ -405,7 +405,6 @@ noinst_HEADERS = \ strategicSearch.hh \ depthFirstStrategicSearch.hh \ fairStrategicSearch.hh \ - sharedValue.hh \ matchProcess.hh \ subtermProcess.hh \ rewriteTask.hh \ diff --git a/src/StrategyLanguage/applicationProcess.cc b/src/StrategyLanguage/applicationProcess.cc index b99bfbe7..c525d6a2 100644 --- a/src/StrategyLanguage/applicationProcess.cc +++ b/src/StrategyLanguage/applicationProcess.cc @@ -198,7 +198,7 @@ ApplicationProcess::run(StrategicSearch& searchObject) int ApplicationProcess::doRewrite(StrategicSearch& searchObject, - SharedValue rewriteState, + shared_ptr rewriteState, PositionState::PositionIndex redexIndex, ExtensionInfo* extensionInfo, Substitution* substitution, @@ -273,7 +273,7 @@ ApplicationProcess::doRewrite(StrategicSearch& searchObject, StrategicExecution::Survival ApplicationProcess::resolveRemainingConditionFragments(StrategicSearch& searchObject, - SharedValue rewriteState, + shared_ptr rewriteState, PositionState::PositionIndex redexIndex, ExtensionInfo* extensionInfo, Substitution* substitutionSoFar, diff --git a/src/StrategyLanguage/applicationProcess.hh b/src/StrategyLanguage/applicationProcess.hh index 31643001..4bfb2957 100644 --- a/src/StrategyLanguage/applicationProcess.hh +++ b/src/StrategyLanguage/applicationProcess.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -24,10 +24,10 @@ // Class for applying rls. // #ifndef _applicationProcess_hh_ +#include #define _applicationProcess_hh_ #include "strategicProcess.hh" #include "rewriteSearchState.hh" -#include "sharedValue.hh" #include "strategyStackManager.hh" class ApplicationProcess : public StrategicProcess @@ -48,7 +48,7 @@ public: static StrategicExecution::Survival resolveRemainingConditionFragments(StrategicSearch& searchObject, - SharedValue rewriteState, + shared_ptr rewriteState, PositionState::PositionIndex redexIndex, ExtensionInfo* extensionInfo, Substitution* substitutionSoFar, @@ -62,13 +62,13 @@ public: private: static int doRewrite(StrategicSearch& searchObject, - SharedValue rewriteState, + shared_ptr rewriteState, PositionState::PositionIndex redexIndex, ExtensionInfo* extensionInfo, Substitution* substitution, Rule* rule); - SharedValue rewriteState; + shared_ptr rewriteState; StrategyStackManager::StackId pending; ApplicationStrategy* strategy; diff --git a/src/StrategyLanguage/matchProcess.cc b/src/StrategyLanguage/matchProcess.cc index b232a295..7120f987 100644 --- a/src/StrategyLanguage/matchProcess.cc +++ b/src/StrategyLanguage/matchProcess.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -55,7 +55,7 @@ #include "applicationProcess.hh" #include "matchProcess.hh" -MatchProcess::MatchProcess(const SharedValue& rewriteState, +MatchProcess::MatchProcess(const shared_ptr& rewriteState, PositionState::PositionIndex redexIndex, ExtensionInfo* extensionInfo, RewritingContext* matchContext, diff --git a/src/StrategyLanguage/matchProcess.hh b/src/StrategyLanguage/matchProcess.hh index 088f6b0c..40587904 100644 --- a/src/StrategyLanguage/matchProcess.hh +++ b/src/StrategyLanguage/matchProcess.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -25,9 +25,9 @@ // #ifndef _matchProcess_hh_ #define _matchProcess_hh_ +#include #include "strategicProcess.hh" #include "rewriteSearchState.hh" -#include "sharedValue.hh" #include "strategyStackManager.hh" class MatchProcess : public StrategicProcess @@ -35,7 +35,7 @@ class MatchProcess : public StrategicProcess NO_COPYING(MatchProcess); public: - MatchProcess(const SharedValue& rewriteState, + MatchProcess(const shared_ptr& rewriteState, PositionState::PositionIndex redexIndex, ExtensionInfo* extensionInfo, RewritingContext* matchContext, @@ -52,7 +52,7 @@ public: Survival run(StrategicSearch& searchObject); private: - SharedValue rewriteState; // smart pointer to rewrite state that found our redex + shared_ptr rewriteState; // smart pointer to rewrite state that found our redex const PositionState::PositionIndex redexIndex; // index of redex withing rewrite state ExtensionInfo* extensionInfoCopy; // copy of extension info from original rule match RewritingContext* matchContext; // rewrite context associated with our fragment match diff --git a/src/StrategyLanguage/rewriteTask.cc b/src/StrategyLanguage/rewriteTask.cc index c37723b6..538652a6 100644 --- a/src/StrategyLanguage/rewriteTask.cc +++ b/src/StrategyLanguage/rewriteTask.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -57,7 +57,7 @@ #include "rewriteTask.hh" RewriteTask::RewriteTask(StrategicSearch& searchObject, - SharedValue rewriteState, + shared_ptr rewriteState, PositionState::PositionIndex redexIndex, ExtensionInfo* extensionInfo, Substitution* substitutionSoFar, diff --git a/src/StrategyLanguage/rewriteTask.hh b/src/StrategyLanguage/rewriteTask.hh index d5b93e19..c20e8f75 100644 --- a/src/StrategyLanguage/rewriteTask.hh +++ b/src/StrategyLanguage/rewriteTask.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -26,6 +26,7 @@ // #ifndef _rewriteTask_hh_ #define _rewriteTask_hh_ +#include #include "strategicTask.hh" class RewriteTask : public StrategicTask @@ -34,7 +35,7 @@ class RewriteTask : public StrategicTask public: RewriteTask(StrategicSearch& searchObject, - SharedValue rewriteState, + shared_ptr rewriteState, PositionState::PositionIndex redexIndex, ExtensionInfo* extensionInfo, Substitution* substitutionSoFar, @@ -54,7 +55,7 @@ public: private: const HashConsSet& hashConsSet; // reference to shared hash cons set - SharedValue rewriteState; // smart pointer to rewrite state that found our redex + shared_ptr rewriteState; // smart pointer to rewrite state that found our redex const PositionState::PositionIndex redexIndex; // index of redex withing rewrite state ExtensionInfo* extensionInfoCopy; // copy of extension info from original match Rule* const rule; // pointer to rule whose lhs matched diff --git a/src/StrategyLanguage/sharedValue.hh b/src/StrategyLanguage/sharedValue.hh deleted file mode 100644 index 217daf8a..00000000 --- a/src/StrategyLanguage/sharedValue.hh +++ /dev/null @@ -1,76 +0,0 @@ -/* - - This file is part of the Maude 3 interpreter. - - Copyright 1997-2006 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 - the Free Software Foundation; either version 2 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this program; if not, write to the Free Software - Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA. - -*/ - -// -// Class for a simplified RewriteSearchState, together with reference counting smart pointers to -// determine when it is deleted, when it gets shared between multiple users. -// -#ifndef _sharedValue_hh_ -#define _sharedValue_hh_ - -template -class SharedValue -{ -public: - SharedValue(T* value); - SharedValue(const SharedValue& other); - ~SharedValue(); - T* operator->(); - -private: - T* value; - int* refCount; -}; - -template -inline T* -SharedValue::operator->() -{ - return value; -} - -template -SharedValue::SharedValue(T* value) - : value(value), - refCount(new int(1)) -{ -} - -template -SharedValue::SharedValue(const SharedValue& other) -{ - value = other.value; - refCount = other.refCount; - ++(*refCount); -} - -template -SharedValue::~SharedValue() -{ - if (--(*refCount) == 0) - { - delete value; - delete refCount; - } -} - -#endif diff --git a/src/StrategyLanguage/subtermProcess.hh b/src/StrategyLanguage/subtermProcess.hh index 82417e43..cfde9f62 100644 --- a/src/StrategyLanguage/subtermProcess.hh +++ b/src/StrategyLanguage/subtermProcess.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -25,8 +25,8 @@ // #ifndef _subtermProcess_hh_ #define _subtermProcess_hh_ +#include #include "strategicProcess.hh" -#include "sharedValue.hh" class SubtermProcess : public StrategicProcess { @@ -43,7 +43,7 @@ public: private: // Will be shared with the matchrew tasks it will create - SharedValue matchState; + shared_ptr matchState; SubtermStrategy* strategy; StrategyStackManager::StackId pending; }; diff --git a/src/StrategyLanguage/subtermTask.cc b/src/StrategyLanguage/subtermTask.cc index 5400f704..1174f929 100644 --- a/src/StrategyLanguage/subtermTask.cc +++ b/src/StrategyLanguage/subtermTask.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-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -204,7 +204,7 @@ SubtermTask::RemainingProcess::run(StrategicSearch&) SubtermTask::SubtermTask(StrategicSearch& searchObject, SubtermStrategy* strategy, - SharedValue searchState, + shared_ptr searchState, ExtensionInfo* extensionInfo, MatchSearchState::PositionIndex searchPosition, StrategyStackManager::StackId pending, diff --git a/src/StrategyLanguage/subtermTask.hh b/src/StrategyLanguage/subtermTask.hh index 975cc734..9cc50180 100644 --- a/src/StrategyLanguage/subtermTask.hh +++ b/src/StrategyLanguage/subtermTask.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -25,7 +25,7 @@ // #ifndef _subtermTask_hh_ #define _subtermTask_hh_ - +#include #include // core class definitions @@ -36,7 +36,6 @@ #include "matchSearchState.hh" // strategy language definitions -#include "sharedValue.hh" #include "strategyLanguage.hh" #include "strategicTask.hh" #include "variableBindingsManager.hh" @@ -61,7 +60,7 @@ public: // SubtermTask(StrategicSearch& searchObject, SubtermStrategy* strategy, - SharedValue searchState, + shared_ptr searchState, ExtensionInfo* extensionInfo, MatchSearchState::PositionIndex searchPosition, StrategyStackManager::StackId pending, @@ -86,7 +85,7 @@ private: // The following 3 contain the information about where the main pattern has been found // (and allow to replace the main pattern match with the result) - SharedValue searchState; + shared_ptr searchState; ExtensionInfo* extensionInfo; MatchSearchState::PositionIndex searchIndex; diff --git a/src/Utility/ChangeLog b/src/Utility/ChangeLog index e302de53..0d444237 100644 --- a/src/Utility/ChangeLog +++ b/src/Utility/ChangeLog @@ -1,3 +1,35 @@ +2024-03-06 Steven Eker + + * pointerMap.cc (PointerMap::PointerMap, PointerMap::setMap): + code cleaning + (PointerMap::getMap): code cleaning + (PointerMap::findEntry): code cleaning + (PointerMap::resize): code cleaning + + * pointerMap.hh (class PointerMap): updated decls for + setMap(), getMap(), hash(), hash2(), findEntry(); struct Pair + now has const void* field from + + * pointerMap.cc (PointerMap::hash, PointerMap::hash2): take + const arg + (PointerMap::setMap): take const from arg + (PointerMap::getMap): take const from arg + (PointerMap::findEntry): take const from arg + +2024-03-04 Steven Eker + + * macros.hh: deleted typedef unsigned int Uint + +2024-03-01 Steven Eker + + * tty.cc: deleted Tty::savedFlag + + * tty.hh (Tty::blockEscapeSequences): deleted + (Tty::unblockEscapeSequences): deleted + (class Tty): deleted static data member savedFlag + +===================================Maude158=================================== + 2024-02-14 Steven Eker * checkedConstIterator.hh (Vector::iterator::operator>): added diff --git a/src/Utility/macros.hh b/src/Utility/macros.hh index a53aa1a5..5aab4eb7 100644 --- a/src/Utility/macros.hh +++ b/src/Utility/macros.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -108,10 +108,6 @@ typedef ptrdiff_t Index; typedef signed char Byte; typedef unsigned char Ubyte; // -// Shorthand. -// -typedef unsigned int Uint; -// // 64 bit arithmetic; since it's now practical to deal with quantities // of rewrites/matchers/unifiers etc that overflow 32 bits. // diff --git a/src/Utility/pointerMap.cc b/src/Utility/pointerMap.cc index eec35404..fca644e5 100644 --- a/src/Utility/pointerMap.cc +++ b/src/Utility/pointerMap.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -32,14 +32,14 @@ #include "pointerMap.hh" inline int -PointerMap::hash(void* pointer) +PointerMap::hash(const void* pointer) { int i = reinterpret_cast(pointer); return (i >> NR_PTR_LOSE_BITS) ^ (i >> (2 * NR_PTR_LOSE_BITS)); } inline int -PointerMap::hash2(void* pointer) // 2nd hash function must always return an odd value +PointerMap::hash2(const void* pointer) // 2nd hash function must always return an odd value { int i = reinterpret_cast(pointer); return ((i >> NR_PTR_LOSE_BITS) ^ (i >> (WORD_SIZE / 2))) | 1; @@ -52,22 +52,22 @@ PointerMap::PointerMap(int size) s *= 2; s *= 2; hashTable.expandTo(s); - for (int i = 0; i < s; i++) - hashTable[i].from = 0; + for (int i = 0; i < s; ++i) + hashTable[i].from = nullptr; used = 0; } void* -PointerMap::setMap(void* from, void* to) +PointerMap::setMap(const void* from, void* to) { - Assert(from != 0, "can't map null pointer"); + Assert(from != nullptr, "can't map null pointer"); if (hashTable.length() <= 2 * used) resize(); Pair& p = hashTable[findEntry(from)]; void* r; - if (p.from == 0) + if (p.from == nullptr) { - r = 0; + r = nullptr; p.from = from; ++used; } @@ -78,24 +78,24 @@ PointerMap::setMap(void* from, void* to) } void* -PointerMap::getMap(void* from) const +PointerMap::getMap(const void* from) const { - Assert(from != 0, "can't map null pointer"); + Assert(from != nullptr, "can't map null pointer"); const Pair& p = hashTable[findEntry(from)]; - return (p.from == 0) ? 0 : p.to; + return (p.from == nullptr) ? nullptr : p.to; } int -PointerMap::findEntry(void* from) const +PointerMap::findEntry(const void* from) const { int mask = hashTable.length() - 1; int i = hash(from) & mask; - if (hashTable[i].from == 0 || hashTable[i].from == from) + if (hashTable[i].from == nullptr || hashTable[i].from == from) return i; int step = hash2(from); do i = (i + step) & mask; - while (hashTable[i].from != 0 && hashTable[i].from != from); + while (hashTable[i].from != nullptr && hashTable[i].from != from); return i; } @@ -105,21 +105,21 @@ PointerMap::resize() int s = hashTable.length(); int n = 2 * s; Vector newHashTable(n); - for (int i = 0; i < n; i++) - newHashTable[i].from = 0; + for (int i = 0; i < n; ++i) + newHashTable[i].from = nullptr; int mask = n - 1; - for (int i = 0; i < s; i++) + for (int i = 0; i < s; ++i) { Pair& p = hashTable[i]; - if (p.from != 0 && p.to != 0) + if (p.from != nullptr && p.to != nullptr) { int j = hash(p.from) & mask; - if (newHashTable[j].from != 0) + if (newHashTable[j].from != nullptr) { int step = hash2(p.from); do j = (j + step) & mask; - while (newHashTable[j].from != 0); + while (newHashTable[j].from != nullptr); } newHashTable[j] = p; } diff --git a/src/Utility/pointerMap.hh b/src/Utility/pointerMap.hh index 268fa02d..909c9a47 100644 --- a/src/Utility/pointerMap.hh +++ b/src/Utility/pointerMap.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -33,19 +33,19 @@ class PointerMap public: PointerMap(int size = 8); - void* setMap(void* from, void* to); - void* getMap(void* from) const; + void* setMap(const void* from, void* to); + void* getMap(const void* from) const; private: struct Pair { - void* from; + const void* from; void* to; }; - static int hash(void* pointer); - static int hash2(void* pointer); - int findEntry(void* from) const; + static int hash(const void* pointer); + static int hash2(const void* pointer); + int findEntry(const void* from) const; void resize(); int used; diff --git a/src/Utility/tty.cc b/src/Utility/tty.cc index cbf2dd56..04744c3d 100644 --- a/src/Utility/tty.cc +++ b/src/Utility/tty.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -56,7 +56,6 @@ const char* const Tty::ansiCode[] = }; bool Tty::allowedFlag = true; -bool Tty::savedFlag = false; const char* Tty::ctrlSequence() const diff --git a/src/Utility/tty.hh b/src/Utility/tty.hh index dbaef24f..2b711a48 100644 --- a/src/Utility/tty.hh +++ b/src/Utility/tty.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -68,7 +68,6 @@ public: private: static const char* const ansiCode[]; static bool allowedFlag; - static bool savedFlag; const Attribute attr; }; @@ -85,19 +84,6 @@ Tty::setEscapeSequencesAllowed(bool flag) allowedFlag = flag; } -inline void -Tty::blockEscapeSequences() -{ - savedFlag = allowedFlag; - allowedFlag = false; -} - -inline void -Tty::unblockEscapeSequences() -{ - allowedFlag = savedFlag; -} - inline ostream& operator<<(ostream& s, const Tty& t) { diff --git a/src/Variable/ChangeLog b/src/Variable/ChangeLog index f00117dd..8b998ef3 100755 --- a/src/Variable/ChangeLog +++ b/src/Variable/ChangeLog @@ -1,3 +1,23 @@ +2024-03-12 Steven Eker + + * variableDagNode.hh (class VariableDagNode): deleted old + commented out computeSolvedForm2() decl + +2024-03-11 Steven Eker + + * variableDagNode.cc (VariableDagNode::computeSolvedForm2): avoid + casting now that we have a VariableDagNode specific symbol() + + * variableDagNode.hh (symbol): added + +2024-03-05 Steven Eker + + * variableTerm.hh (class VariableTerm): made arguments() const + + * variableTerm.cc (VariableTerm::arguments): made const + +===================================Maude158=========================================== + 2023-07-24 Steven Eker * variableSymbol.cc (VariableSymbol::determineGround): added diff --git a/src/Variable/variableDagNode.cc b/src/Variable/variableDagNode.cc index 29484517..2cee65a6 100755 --- a/src/Variable/variableDagNode.cc +++ b/src/Variable/variableDagNode.cc @@ -154,8 +154,7 @@ VariableDagNode::computeSolvedForm2(DagNode* rhs, // have the lowest sort if they are comparable and unequal. // We do this by ensuring rv has the largest sort index. // - if (safeCast(VariableSymbol*, lv->symbol())->getSort()->index() > - safeCast(VariableSymbol*, rv->symbol())->getSort()->index()) + if (lv->symbol()->getSort()->index() > rv->symbol()->getSort()->index()) swap(lv, rv); // // Need to replace one variable by the other throughout the problem. We do this diff --git a/src/Variable/variableDagNode.hh b/src/Variable/variableDagNode.hh index 5d4d01d6..0e93b2f9 100644 --- a/src/Variable/variableDagNode.hh +++ b/src/Variable/variableDagNode.hh @@ -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-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -27,6 +27,7 @@ #define _variableDagNode_hh_ #include "dagNode.hh" #include "namedEntity.hh" +#include "variableSymbol.hh" class VariableDagNode : public DagNode, public NamedEntity { @@ -41,21 +42,12 @@ public: void overwriteWithClone(DagNode* old); DagNode* makeClone(); DagNode* copyWithReplacement(int argIndex, DagNode* replacement); - DagNode* copyWithReplacement(Vector& redexStack, - int first, - int last); + DagNode* copyWithReplacement(Vector& redexStack, int first, int last); // // Unification member functions. // ReturnResult computeBaseSortForGroundSubterms(bool warnAboutUnimplemented); - /* - bool computeSolvedForm2(DagNode* rhs, - Substitution& solution, - Subproblem*& returnedSubproblem, - ExtensionInfo* extensionInfo); - */ bool computeSolvedForm2(DagNode* rhs, UnificationContext& solution, PendingUnificationStack& pending); - void insertVariables2(NatSet& occurs); DagNode* instantiate2(const Substitution& substitution, bool maintainInvariants); // @@ -71,6 +63,7 @@ public: // Functions specific to VariableDagNode. // int getIndex() const; + VariableSymbol* symbol() const; VariableDagNode* lastVariableInChain(Substitution& solution); private: @@ -95,6 +88,12 @@ VariableDagNode::VariableDagNode(Symbol* symbol, int name, int index) { } +inline VariableSymbol* +VariableDagNode::symbol() const +{ + return safeCastNonNull(DagNode::symbol()); +} + inline int VariableDagNode::getIndex() const { diff --git a/src/Variable/variableTerm.cc b/src/Variable/variableTerm.cc index de62ef1b..6c9a3daa 100644 --- a/src/Variable/variableTerm.cc +++ b/src/Variable/variableTerm.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -59,7 +59,7 @@ VariableTerm::VariableTerm(VariableSymbol* symbol, int name) } RawArgumentIterator* -VariableTerm::arguments() +VariableTerm::arguments() const { return 0; } diff --git a/src/Variable/variableTerm.hh b/src/Variable/variableTerm.hh index 82edee44..bf4cabc9 100644 --- a/src/Variable/variableTerm.hh +++ b/src/Variable/variableTerm.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -36,7 +36,7 @@ class VariableTerm : public Term, public NamedEntity public: VariableTerm(VariableSymbol* symbol, int name); - RawArgumentIterator* arguments(); + RawArgumentIterator* arguments() const; void deepSelfDestruct(); Term* deepCopy2(SymbolMap* translator) const; Term* normalize(bool full, bool& changed);