op (op_:_->_[_].) : Qid TypeList Type AttrSet -> OpDecl .
There are eleven places where white space can be inserted:
op _ : _ -> _ [ _ ] .
^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^
A format attribute must have an instruction word for each of these places. For example, the formatting specification for the above operator could be chosen to be:
[format (d d d d d d s d d s d)]
Instruction words are formed from the following alphabet:
| d | default spacing |
| (cannot be part of a larger word: must occur on its own) | |
| + | increment global indent counter |
| - | decrement global indent counter |
| s | space |
| t | tab |
| i | number of spaces determined by indent counter |
| n | newline |
Note that, in general, each place may have an entire word combining several of the above symbols. We can illustrate how this feature is used in several operators in (submodules of) the META-LEVEL module in the file prelude.maude (see Chapter 11).
op _<-_ : Variable Term -> Assignment
[ctor prec 63 format (nt d d d)] .
op __ : ImportList ImportList -> ImportList
[ctor assoc id: nil format (d ni d)] .
op fmod_is_sorts_.____endfm : Qid ImportList SortSet
SubsortDeclSet OpDeclSet MembAxSet EquationSet -> FModule
[ctor gather (& & & & & & &)
format (d d d n++i ni d d ni ni ni ni n--i d)] .
Whether the format attribute is actually used or not when printing is controlled by the command:
set print format on/off .
The following additional alphabet can be used to change the text color and style. These colors, perhaps combined with spacing directives, can greatly ease readability, particularly in complex terms for which they can serve as markers. They rely on ANSI escape sequences which are supported by most terminal emulators, most notably the Linux console, Xterm, and Mac Terminal windows, but not Emacs shell buffers, unless you use ansi-color.el.4.7
| r | red |
| g | green |
| y | yellow |
| b | blue |
| m | magenta |
| c | cyan |
| u | underline |
| ! | bold |
| o | revert to original color and style |
By default ANSI escape sequences are suppressed if the environment variable TERM is set equal to dumb (Emacs does this) or standard output is not a terminal; they are allowed otherwise. This behavior can be overridden by the command line options -ansi-color and -no-ansi-color.
You are allowed to give a format attribute even if there is no mixfix syntax. In this case the format attribute must have two instruction words, indicating the desired format before and after the operator's name. For example,
fmod COLOR-TEST is
sorts Color ColorList .
subsort Color < ColorList .
op red : -> Color [format (r! o)] .
op green : -> Color [format (g! o)] .
op blue : -> Color [format (b! o)] .
op yellow : -> Color [format (yu o)] .
op cyan : -> Color [format (cu o)] .
op magenta : -> Color [format (mu o)] .
op __ : ColorList ColorList -> ColorList [assoc] .
endfm
To see the colors in this module, load the COLOR-TEST module into Maude and execute the command:4.8
Maude> reduce red green blue yellow cyan magenta . reduce in COLOR-TEST : red green blue yellow cyan magenta . rewrites: 0 in 0ms cpu (0ms real) (~ rews/sec) result ColorList: red green blue yellow cyan magenta
Let us consider the following module FORMAT-DEMO, where a small programming language is defined.
fmod FORMAT-DEMO is
sorts Variable Expression BoolExp Statement .
subsort Variable < Expression .
ops a b c d : -> Variable .
op 1 : -> Expression .
op _+_ : Expression Expression -> Expression [assoc comm] .
op _;_ : Statement Statement -> Statement [assoc prec 50] .
op _<=_ : Expression Expression -> BoolExp .
op while_do_od : BoolExp Statement -> Statement
[format (nir! o r! o++ --nir! o)] .
op let_:=_ : Variable Expression -> Statement
[format (nir! o d d d)] .
endfm
Note the use of the format attribute for operators
while_do_od and let_:=_. Since both represent statements, which
should start in a new line, but at the current indentation level, both include
ni in the instruction words for their first positions; this
position also has characters r! in both cases, so that they start in
boldface red font. Since there is a o for the next position, reverting
to original color and style, only the first word (while and
let) is shown in red. In the case of while_do_od, the condition
of the loop starts at the second position. The do word is shown in
boldface red, and then the indentation counter is incremented, so that the body
of the while_do_od statement is indented. For the position marking the
beginning of od, the counter is decremented, so that it appears at the
level of while in a new line (n), in boldface red font
(r!). The last position reverts the original color and style, although
notice that the indentation counter remains the same, so that
successive statements will be given the same level of indentation. In the
case of let_:=_, the three last positions contain only d (default
spacing), since it is to be presented as a single-line statement in which
let is shown in boldface red.
We can illustrate the difference between using the format attribute and not using it with the following commands (as before, you should execute the example in your terminal to see the colors).
Maude> set print format off .
Maude> parse
while a <= d do
let a := a + b ;
while b <= d do
let b := b + c ;
let c := c + 1
od
od
.
Statement: while a <= d do let a := a + b ; while b <= d do let b :=
b + c ; let c := c + 1 od od
Maude> set print format on .
Maude> parse
while a <= d do
let a := a + b ;
while b <= d do
let b := b + c ;
let c := c + 1
od
od
.
Statement:
while a <= d do
let a := a + b ;
while b <= d do
let b := b + c ;
let c := c + 1
od
od
For more examples of format attributes, you can see the operator declarations in the module LTL (in the file model-checker.maude) discussed in Chapter 10, or in the modules META-TERM and META-MODULE (in the file prelude.maude), described in Chapter 11.