Dear Maude Abusers,

A new alpha release can be accessed at SRI-CSL in:

~eker/public_html/Maude/Alpha115/

or downloaded from:

http://www.csl.sri.com/~eker/Maude/Alpha115/

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
==========
(1) A bug where the show mod command would output parentheses even
for id-hooks even when there was no contents:

load socket
show mod .

    :
    id-hook SocketManagerSymbol ()
    :

(2) A bug where Maude wouldn't compile without either Yices2 or
CVC4 being selected. Reported by Julia Sanchis.

New features
=============
(1) There is support for basic file handling via the external object
mechanism. The API is declared in file.maude:

mod COMMON-MESSAGES is
  protecting STRING .
  including  CONFIGURATION .

  op gotLine : Oid Oid String -> Msg [ctor msg format (m o)] .
  op write : Oid Oid String -> Msg [ctor msg format (b o)] .
  op wrote : Oid Oid -> Msg [ctor msg format (m o)] .
endm

mod FILE is
  including COMMON-MESSAGES .
  protecting INT .

  sort Base .
  ops start current end : -> Base [ctor] .

  op file : Nat -> Oid [ctor] .

  op openFile : Oid Oid String String -> Msg [ctor msg format (b o)] .
  op openedFile : Oid Oid Oid -> Msg [ctor msg format (m o)] .

  op getLine : Oid Oid -> Msg [ctor msg format (b o)] .

  op getChars : Oid Oid Nat -> Msg [ctor msg format (b o)] .
  op gotChars : Oid Oid String -> Msg [ctor msg format (m o)] .

  op flush : Oid Oid -> Msg [ctor msg format (b o)] .
  op flushed : Oid Oid -> Msg [ctor msg format (m o)] .

  op setPosition : Oid Oid Int Base -> Msg [ctor msg format (b o)] .
  op positionSet : Oid Oid -> Msg [ctor msg format (m o)] .
  op getPosition : Oid Oid -> Msg [ctor msg format (b o)] .
  op positionGot : Oid Oid Nat -> Msg [ctor msg format (m o)] .

  op closeFile : Oid Oid -> Msg [ctor msg format (b o)] .
  op closedFile : Oid Oid -> Msg [ctor msg format (m o)] .

  op fileError : Oid Oid String -> Msg [ctor msg format (m o)] .

  op fileManager : -> Oid [special (...)] .
endm

This API basically wraps the C stdio library (I considered
wrapping the C++ file streams library but its complexity
and inaccurate representation of what the operating system
actually provides made this awkward).

To open a file you send fileManager a message:

openFile(fileManager, ME, PATH, MODE)

where ME is the name of the object the reply should be sent
to, PATH is the path of the file you want to open and MODE
is one of: r, r+, w, w+, a, a+
These have the semantics given by the fopen() library call.
As with fopen(), a 'b' may be appended or interposed to indicate
binary mode - which has no effect on UNIX based operating
systems but will allow compatibility if Maude is ever ported
to an operating system where line breaks are represented
differently and text mode does translation.
The reply is either:

openedFile(ME, fileManager, FILE-HANDLE) or
fileError(ME, fileManager, REASON)

where FILE-HANDLE is the name of the object using to
access the file, and REASON is operating system's terse
explanation of what went wrong.

If the file was opened for writing you can send:

write(FILE-HANDLE, ME, DATA)

to write data to the file, and receive a reply:

wrote(ME, FILE-HANDLE) or
fileError(ME, FILE-HANDLE, REASON)

A file that is opened for writing can also be set:

flush(FILE-HANDLE, ME)

to flush any buffered data and receive a reply:

flushed(ME, FILE-HANDLE) or
fileError(ME, FILE-HANDLE, REASON)

A file that is opened for reading can be read on a
line-by-line basis using the message:

getLine(FILE-HANDLE, ME)

where the reply is either:

gotLine(ME, FILE-HANDLE, TEXT) or
fileError(ME, FILE-HANDLE, REASON)

Here TEXT includes the newline character (if present -
end-of-file also ends the current line). TEXT is empty
to indicate end-of-file with no more characters to read.

A file that is opened for reading can be read on a
character basis (which is more appropriate for binary
files) using the message:

getChars(FILE-HANDLE, ME, #CHARS-TO-GET)

where the reply is either:

gotChars(ME, FILE-HANDLE, DATA) or
fileError(ME, FILE-HANDLE, REASON)

Here if DATA is shorter than requested, it indicates
the end-of-file was reached.

Reading and writing share a common position into the file
where the next read or write takes place. This position
in bytes from the start of the file can be obtained by
sending the message:

getPosition(FILE-HANDLE, ME)

where the reply is either:

positionGot(ME, FILE-HANDLE, OFFSET) or
fileError(ME, FILE-HANDLE, REASON)

The position may be changed with the message:

setPosition(FILE-HANDLE, ME, OFFSET, BASE)

Here the OFFSET is relative to BASE where BASE can take
one of three values:

start : the start of the file
current : the current position
end : the end of the file

In the current and end cases, negative values of OFFSET
are allowed. The reply is either:

positionSet(ME, FILE-HANDLE) or
fileError(ME, FILE-HANDLE, REASON)

Finally, an open file can be closed with the message

closeFile(FILE-HANDLE, ME)

Since it is always OK to close an open file, the
response is always:

closedFile(ME, FILE-HANDLE)

Note that messages that are not recognized or that are
sent to nonexistent objects will be silently ignored
and left in the configuration. Message that are recognized
but are not appropriate for the object they are sent to
or which have bad arguments will similarly be ignored but
will generate a "message declined" advisory.

(2) There is support for the standard UNIX streams stdin,
stdout and stderr. Originally I planned to use the file
mechanism above to handle them, but standard streams
are quite different in what messages they can handle and
on the backend, input typically comes from the Tecla
command line editor while output goes through Maude's
line wrapper, so it is cleaner to handle them with a
separate API, also included in file.maude:

mod STD-STREAM is
  including COMMON-MESSAGES .

  op getLine : Oid Oid String -> Msg [ctor msg format (b o)] .

  op stdin : -> Oid [special (...)] .
  op stdout : -> Oid [special (...)] .
  op stderr : -> Oid [special (...)] .
endm

I/O on standard streams is always line oriented and in
text mode. stdout and stderr accept the write() message
just like file handles. They are automatically flushed
so this is the only message they can accept. They always
return a wrote() message. After 22 years you can now
write a "Hello World!" program in Maude:

mod HELLO-WORLD is
  inc STD-STREAM .
  op myClass : -> Cid .
  ops myObj : -> Oid .
  op run : -> Configuration .
  eq run = <> < myObj : myClass | none > write(stdout, myObj, "Hello World!\n") .
endm

erew run .

stdin accepts a 3 argument getLine() message:

getLine(stdin, ME, PROMPT)

The reason for this is that Tecla must be given any
prompt that is to be written to the command line otherwise
it will ignore it and start your input on top of any
prompt you printed with write(). stdin replies
with a message

gotLine(ME, stdin, TEXT)

where TEXT contains just a "\n" character in the case of an empty
line and is empty in the case of an error or end-of-file (^D).
The following example illustrates the use of stdin and stdout
to do ROT13 encryption on text the user provides:

mod ROT13 is
  inc STD-STREAM .
  pr INT .
  op myClass : -> Cid .
  ops myObj : -> Oid .
  op run : -> Configuration .
  op rot13 : String -> String .

  vars O O2 : Oid .
  var A : AttributeSet .
  vars S T : String .
  var C : Char .

  eq rot13(C) = if C >= "A" and C <= "Z" then
                  char(ascii("A") + ((13 + (ascii(C) - ascii("A"))) rem 26))
                else if C >= "a" and C <= "z" then
                       char(ascii("a") + ((13 + (ascii(C) - ascii("a"))) rem 26))
                      else
                        C
		      fi
                fi .
  eq rot13(S) = rot13(substr(S, 0, 1)) + rot13(substr(S, 1, length(S))) [owise] .

  eq run = <> < myObj : myClass | none > write(stdout, myObj, "\nROT13 Encryption\n----------------\n") .
  rl < O : myClass | A > wrote(O, O2) => < O : myClass | A > getLine(stdin, O, "Enter plain text> ") .
  rl < O : myClass | A > gotLine(O, O2, T) => < O : myClass | A >
    if T == "" then none else write(stdout, O, "Cypher text: " + rot13(T)) fi .
endm

erew run .

(3) There is now support for converting between strings and lists of
quoted identifiers using Maude's lexical conventions, defined in
the module:

fmod LEXICAL is
  protecting QID-LIST .
  op printTokens : QidList -> String [special (...)] .
  op tokenize : String -> QidList [special (...)] .
endfm

printTokens() converts each quoted identifier to a string and
concatening with spaces where appropriate. The conversion
is slightly different from the pre-existing string() function.

For simple quoted identifers the conversions are the same:

printTokens('abc) = string('abc) = "abc"

However there are a number of character sequences that are
not legitimate identifiers, and hence don't have quoted
identifiers as such. However they are useful and so are instead
represented as quoted identifiers using the
metaPrettyPrint()/LOOP-MODE conventions:

For the 7 special tokens ( ) [ ] { } , the conversions of
the associated quoted identifiers differ, with printTokens()
returning a 1 character string while string() includes the
backquote:

printTokens('`() = "(" whereas string('`()) = "`("

For quoted identifers of the form '\x where x is a single
character, there are several possibilities. If x is n t or \
printTokens() understands the C escape convention:

printTokens('\n) = "\n" whereas string('\n) = "\\n"

The special case of '\s is used to have a quoted
identifer that represent a single space:

printTokens('\s) = " " whereas string('\s) = "\\s"

The 21 special values of x:

! ? u f x h o
p r g y m c w
P R G Y M X W

are used to represent ANSI control sequences, for
example:

printTokens('\r) = "\033[31m" whereas string('\r) = "\\r"

If x has any other value, printTokens() behaves
the same as string() to produce a 2 character string
(though of course when printing this string as an
identifier, it is surrounded by double quotes and
the \ itself is escaped):

printTokens('\q) = string('\q) = "\\q"

However printTokens() also works on lists of quoted
identifers. The nil list is mapped to the empty string:

printTokens(nil) = ""

Lists with more than one quoted identifier map to
the concatenation of strings produced for each quoted
identifier, with a single space inserted between
such strings with two exceptions:

No space is inserted before ( ) [ ] { } ,
No space is inserted after ( [ {

This is slight different from the LOOP-MODE convention, in
that a space will be inserted after ) ] } , if there
is a next token that is not one of ( ) [ ] { } ,
Thus:

reduce in LEXICAL : printTokens('f '`( 'a '`, 'b '`) '+ 'c) .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result String: "f(a, b) + c"

Furthermore the quoted identifiers forms of the 7
special symbols that include a backslash are not
recognized as special as they are in LOOP-MODE:

printTokens('\`() = string('\`() = "\\`("

tokenize() converts a string into a list of quoted
identifers. Characters that cannot be part of a token
terminate any partial token and are otherwise ignored.

reduce in LEXICAL : tokenize("f(a, b) + c") .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result NeQidList: 'f '`( 'a '`, 'b '`) '+ 'c

reduce in LEXICAL : tokenize("          ") .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result QidList: nil

reduce in LEXICAL : tokenize("") .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result QidList: nil

reduce in LEXICAL : tokenize("\"string identifier\"") .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result Qid: '"string identifier"

In particular, an unclosed double quote will terminate
the current token but otherwise be ignored:

reduce in LEXICAL : tokenize("foo\"bar") .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result NeQidList: 'foo 'bar

But a closed double quote is a legitimate continuation
of the current token:

reduce in LEXICAL : tokenize("foo\"bar\"") .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result Qid: 'foo"bar"

Backslash-newline pairs inside double quotes are edited
out:

reduce in LEXICAL : tokenize("\"foo\\\nbar\"") .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result Qid: '"foobar"

As an example of how these built-in operators can be used
with the metalevel, here is a program that reads Maude
arithmetic expressions from the terminal and evaluates
them:

load file

mod CALCULATOR is
  inc STD-STREAM .
  pr LEXICAL .
  pr META-LEVEL .

  op myClass : -> Cid .
  ops myObj : -> Oid .
  op run : -> Configuration .

  vars O O2 : Oid .
  var A : AttributeSet .
  vars S T : String .

  op compute : String -> String .
  eq compute(S) =  compute2(metaParse(['CONVERSION], tokenize(S), anyType)) .

  op compute2 : ResultPair? -> String .
  eq compute2({T:Term, Q:Qid}) = compute3(metaReduce(['CONVERSION], T:Term)) .
  eq compute2(noParse(N:Nat)) = printTokens('\r) + "syntax error" + printTokens('\o) .

  op compute3 : ResultPair? -> String .
  eq compute3({T:Term, Q:Qid}) = printTokens(metaPrettyPrint(['CONVERSION], T:Term)) .

  eq run = <> < myObj : myClass | none > write(stdout, myObj, "\nCalculator\n------------\n") .
  rl < O : myClass | A > wrote(O, O2) => < O : myClass | A > getLine(stdin, O, "Expression> ") .
  rl < O : myClass | A > gotLine(O, O2, T) => < O : myClass | A >
    if T == "" then none else write(stdout, O, "Answer: " + compute(T) + "\n") fi .
endm

erew run .

Expression> 3/6 + 12/32
Answer: 7/8

Other changes
==============
(1) In order to stop the lexical analyzer from buffering
input meant for a getLine() request, it is now obliged to
read input line at a time when it reading from stdin even
when stdin has been redirected to come from a file or pipe.
This has a knock on effect that prompt generation which
was rather arbitrary in file/pipe case, is now turned off in
this case, for behavior similar to in/load file commands.
Also in the -no-tecla case, continuation prompts are now
generated where they weren't previously.

(2) sort Bound and op unbounded now live in their own
fmod BOUND. I was going to use the notion of unbounded in
the FILE API but then dropped it; but I've left this
change since unbounded is a useful concept to have outside
of META-LEVEL.

Steven