Skip to content

Commit

Permalink
alpha154
Browse files Browse the repository at this point in the history
  • Loading branch information
stevenmeker committed Nov 30, 2023
1 parent a99e7cb commit 2a73395
Show file tree
Hide file tree
Showing 59 changed files with 2,323 additions and 1,077 deletions.
19 changes: 18 additions & 1 deletion NEWS
Original file line number Diff line number Diff line change
@@ -1,4 +1,21 @@
Overview of Changes in alpha153
Overview of Changes in alpha154
============================================
* conventions for printing spaces around unparsed tokens made
uniform
* fixed bug where set print const with sorts on . did not work
for built-in constants in terms
* new with-sorts PrintOption constant
* added metaPrintToString() descent function
* added printToString() message
* metaPrettyPrint() descent function supports concealed
argument lists via an extra argument
* printTerm() message supports concealed argument lists via an
extra argument
* concealed argument lists support for printing terms in modules
* fixed bug where color for terms in modules produces bad LaTeX
* fixed bug in LaTeX for disambiguation of iter operators

Overview of Changes in alpha153 (2023-11-07)
============================================
* smarter sort disambiguation for printing statements and
operator identities
Expand Down
20 changes: 10 additions & 10 deletions configure
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
#! /bin/sh
# Guess values for system-dependent variables and create Makefiles.
# Generated by GNU Autoconf 2.69 for Maude alpha153.
# Generated by GNU Autoconf 2.69 for Maude alpha154.
#
# Report bugs to <[email protected]>.
#
Expand Down Expand Up @@ -580,8 +580,8 @@ MAKEFLAGS=
# Identity of this package.
PACKAGE_NAME='Maude'
PACKAGE_TARNAME='maude'
PACKAGE_VERSION='alpha153'
PACKAGE_STRING='Maude alpha153'
PACKAGE_VERSION='alpha154'
PACKAGE_STRING='Maude alpha154'
PACKAGE_BUGREPORT='[email protected]'
PACKAGE_URL=''

Expand Down Expand Up @@ -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 alpha153 to adapt to many kinds of systems.
\`configure' configures Maude alpha154 to adapt to many kinds of systems.
Usage: $0 [OPTION]... [VAR=VALUE]...
Expand Down Expand Up @@ -1383,7 +1383,7 @@ fi

if test -n "$ac_init_help"; then
case $ac_init_help in
short | recursive ) echo "Configuration of Maude alpha153:";;
short | recursive ) echo "Configuration of Maude alpha154:";;
esac
cat <<\_ACEOF
Expand Down Expand Up @@ -1490,7 +1490,7 @@ fi
test -n "$ac_init_help" && exit $ac_status
if $ac_init_version; then
cat <<\_ACEOF
Maude configure alpha153
Maude configure alpha154
generated by GNU Autoconf 2.69
Copyright (C) 2012 Free Software Foundation, Inc.
Expand Down Expand Up @@ -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 alpha153, which was
It was created by Maude $as_me alpha154, which was
generated by GNU Autoconf 2.69. Invocation command line was
$ $0 $@
Expand Down Expand Up @@ -2962,7 +2962,7 @@ fi

# Define the identity of the package.
PACKAGE='maude'
VERSION='alpha153'
VERSION='alpha154'


cat >>confdefs.h <<_ACEOF
Expand Down Expand Up @@ -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 alpha153, which was
This file was extended by Maude $as_me alpha154, which was
generated by GNU Autoconf 2.69. Invocation command line was
CONFIG_FILES = $CONFIG_FILES
Expand Down Expand Up @@ -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 alpha153
Maude config.status alpha154
configured by $0, generated by GNU Autoconf 2.69,
with options \\"\$ac_cs_config\\"
Expand Down
2 changes: 1 addition & 1 deletion configure.ac
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
#
# Initialize autoconf stuff.
#
AC_INIT(Maude, alpha153, [[email protected]])
AC_INIT(Maude, alpha154, [[email protected]])
#
# Allow directory names that look like macros.
#
Expand Down
3 changes: 2 additions & 1 deletion doc/Makefile.am
Original file line number Diff line number Diff line change
Expand Up @@ -21,4 +21,5 @@ EXTRA_DIST = \
alpha150.txt \
alpha151.txt \
alpha152.txt \
alpha153.txt
alpha153.txt \
alpha154.txt
3 changes: 2 additions & 1 deletion doc/Makefile.in
Original file line number Diff line number Diff line change
Expand Up @@ -253,7 +253,8 @@ EXTRA_DIST = \
alpha150.txt \
alpha151.txt \
alpha152.txt \
alpha153.txt
alpha153.txt \
alpha154.txt

all: all-am

Expand Down
18 changes: 6 additions & 12 deletions doc/alpha153.txt
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ or equivalently
Note that as this shows the unparsed module, hooks, identity terms,
membership axioms, equations, rules, and strategy definitions are just
bubbles of tokens which are printed using the \maudeRaw{} command which uses
the typewritter font.
the typewriter font.
Also parameterized sorts and constants in renamings in module expressions
are just printed using the naive \maudeSort{} rather than as a structured
name with \maudeParameter{} and \maudeView{} since they haven't been evaluated
Expand Down Expand Up @@ -90,13 +90,13 @@ in both text and LaTeX.
Note that as this shows the view module, terms on either side of op to
term mappings and strategy expressions on either side of strat to expr
mappings are just bubbles of tokens which are printed using the \maudeRaw{}
command which uses the typewritter font.
command which uses the typewriter font.

(7) There is a new command
set print combine vars on/off .
which controls whether each variable alias is printed on its own line
or whether variable aliases with the same sort are combined in a
single declaration. This flag is supported for show desugares/all vars
single declaration. This flag is supported for show desugared/all vars
The default is off for backward compatibility.

Other changes
Expand All @@ -120,7 +120,7 @@ Here, previously, each occurrence of 0 required disambiguation. Now
the right hand sides of =, => and := are assumed to have a known
kind based on the left hand side, while the left hand side of : is
assumed to have a known kind base on the sort in the rhs so none of
the occurrences of 0 recieve sort disambiguation.
the occurrences of 0 receive sort disambiguation.

(2) A similar change to the printing of operator identities since
the range kind will always be defined by the operator.
Expand Down Expand Up @@ -178,7 +178,7 @@ objects contain a portal was merely to avoid the degenerate case of
a lone object waiting for a reply from an external object, which
would not be received because object-message rewriting and external
object interaction is special behavior that is attached to the
configuration contructor
configuration constructor
op __ : Configuration Configuration -> Configuration [ctor config assoc comm id: none] .
With a portal present, this operator will always appear at the top
of a configuration that communicates with external objects.
Expand All @@ -198,7 +198,7 @@ in different configurations that have the same Oid and as long as only
one such configuration has a portal, messages from external objects
will not be misdelivered. This requirement arises with nested
configurations where the outer configuration manages communication
between external objects and objects in the inner configurarion and
between external objects and objects in the inner configuration and
objects in both configurations share Oids. In this case only the outer
configuration would have a portal and would be able to communicate
directly with external objects.
Expand Down Expand Up @@ -247,9 +247,3 @@ and before the single character tokens
) ] }
in mixfix syntax. This greatly reduces the overfull \hbox issue and
approximates the line breaking rules used by the line wrapper in the text case.

(11) In LaTeX output only for show all/desugared/ops, backquotes are not shown
in op-hooks (they haven't been shown in op declarations for a while). I'm
considering making this the convention for text output in the future, for
both op-hooks and op declarations but there are some subtle cases for reparsing
output.
115 changes: 115 additions & 0 deletions doc/alpha154.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,115 @@
Alpha 154 release notes
========================

Bug fixes
==========

(1) The command
set print const with sorts on .
introduced alpha 126 released 11/22/2019 was implemented for all
kinds of constants when printing dag nodes but only regular constants
and not built-in constants when printing terms. This shows up in the
following example:

fmod FOO is inc NAT .
eq 0 = 0 .
eq 1 = 1 .
endfm

set print const with sorts on .

show desugared .

Here 0 is a regular constant but 1 is a special constant that is really
s 0. This omission is now fixed.

(2) A bug where colors generated for operators with various attributes
generated bad LaTeX when printed as in terms:

fmod FOO is
sort Foo .
op foo : Foo Foo -> Foo [assoc comm] .
op bar : Foo Foo -> Foo [assoc] .
ops a b c : -> Foo .
eq foo(a, b) = bar(c, c) .
endfm

set print color on .

show desugared FOO .

Here the terminal color sequence was being used rather than the LaTeX one.

(3) A very obscure bug where sort disambiguation of iter symbols used
the wrong font for the sort. Triggered by this rather dubious example:

fmod FOO is
sort Foo .
op s : Foo -> Foo [iter] .
op 0 : -> Foo .
sort Bar .
op s^2 : Foo -> Bar .
eq s(s(0)) = 0 .
endfm

show desugared .

New features
=============

(1) There is a new constant
op with-sorts : -> PrintOption [ctor] .
in META-LEVEL that is the metalevel equivalent of
set print const with sorts on .
i.e. each constant in the printed term will have sort disambiguation.

(2) There is a new descent function
op metaPrintToString : Module VariableSet Term PrintOptionSet QidSet ~> String [special (...)] .
that works like metaPrettyPrint() except that it prints to a string.
Here the final argument is a set of operator names whose arguments
should be concealed. There is no PrintOption constant for the print
concealed flag - it is implicitly assumed to be true if the QidSet is
non-empty.

(3) The meta-interpreter has a new pair of messages
op printTermToString : Oid Oid Qid VariableSet Term PrintOptionSet QidSet -> Msg [ctor msg format (b o)] .
op printedTermToString : Oid Oid String -> Msg [ctor msg format (m o)] .
that provide similar functionality for meta-interpreter objects.

Other changes
==============

(1) The printTokens() function in fmod LEXICAL now prints space in front
of ( [ { unless the previous token was ( [ {

(2) Printing of raw tokens for unparsed statements and identities with
show module now print space in front of ( unless the previous token was
( [ {. This was already done for [ {. This change is for both text and
LaTeX output.

(3) The descent function metaPrettyPrint() now takes an extra QidSet
argument to indicate which operators should have the arguments concealed.

op metaPrettyPrint : Module VariableSet Term PrintOptionSet Qid ~> QidList [special (...)] .

For backward compatibility there is also:

op metaPrettyPrint : Module VariableSet Term PrintOptionSet ~> QidList .
eq metaPrettyPrint(M:Module, VS:VariableSet, T:Term, P:PrintOptionSet) =
metaPrettyPrint(M:Module, VS:VariableSet, T:Term, P:PrintOptionSet, none) .

(4) The meta-interpreter message printTerm() now takes an extra QidSet
argument to indicate which operators should have the arguments concealed.

op printTerm : Oid Oid Qid VariableSet Term PrintOptionSet QidSet -> Msg [ctor msg format (b o)] .

For backward compatibility there is also:

op printTerm : Oid Oid Qid VariableSet Term PrintOptionSet -> Msg [ctor msg format (b o)] .
eq printTerm(T:Oid, M:Oid, Q:Qid, VS:VariableSet, T:Term, P:PrintOptionSet) =
printTerm(T:Oid, M:Oid, Q:Qid, VS:VariableSet, T:Term, P:PrintOptionSet, none) .

(5) Printing of terms (as opposed to dags) such as in modules, now supports
set print conceal on .
for both text and LaTeX output. Previously this only worked for dags.

24 changes: 24 additions & 0 deletions src/Main/ChangeLog
Original file line number Diff line number Diff line change
@@ -1,3 +1,27 @@
2023-11-22 Steven Eker <eker@pup>

* metaInterpreter.maude: added printTermToString, printedTermToString
messages
printTerm message now takes a conseal symbols argument; added backward
compatibility symbol

* prelude.maude: metaPrettyPrint() now takes a final QidSet argument for
conceal symbols; added backward compatibility definition

2023-11-21 Steven Eker <eker@pup>

* prelude.maude: added constant with-sorts of sort PrintOption
in META-LEVEL
added descent function
metaPrintToString : Module VariableSet Term PrintOptionSet Qid ~> String

2023-11-16 Steven Eker <eker@pup>

* main.cc (main): Interpreter::PRINT_MIXFIX ->
PrintSettings::PRINT_MIXFIX

===================================Maude154===========================================

2023-11-06 Steven Eker <eker@pup>

* maude.sty: added \maudeAllowLineBreak and use it for \maudeComma
Expand Down
2 changes: 1 addition & 1 deletion src/Main/main.cc
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ main(int argc, char* argv[])
else if (strcmp(arg, "--version") == 0)
printVersion();
else if (strcmp(arg, "-no-mixfix") == 0)
interpreter.setPrintFlag(Interpreter::PRINT_MIXFIX, false);
interpreter.setPrintFlag(PrintSettings::PRINT_MIXFIX, false);
else if (strcmp(arg, "-ansi-color") == 0)
ansiColor = true;
else if (strcmp(arg, "-no-ansi-color") == 0)
Expand Down
Loading

0 comments on commit 2a73395

Please sign in to comment.