format-check — checks whether an ATerm conforms to a given regular tree grammar (RTG)
file | --input
file | --output
[-S | --silent]
level | --keep
[-h | -? | --help]
format-check checks the input ATerm against a regular tree grammar (RTG), to see if this term is part of the language defined in the RTG. If this is not the case, then the ATerm contains format errors, analogous to syntax errors in normal source code. format-check can operate in three modes: plain, visualize and XHTML.
The plain mode is used by default. In this mode, format errors are
reported and no result is written the the output (
or file). Hence, if format-check is included in
a pipeline, then the following tool will probably fail. If the input
term is correct, then it is written to the output.
The visualize mode is enabled with the
In visualize mode, format errors are reported and in a
pretty-printed ATerm will be written to the output. All
innermost parts of the ATerm that cause format errors are
printed in red, if your terminal supports control characters for
colors. If you want to inspect the ATerm with a pager, like
more or less, then
you should use the
The XHTML mode is enabled with the
In XHTML mode, format errors are reported and a report in XHTML will
be written to the output. The result should be inspected in a web
browser (not IE6). As with the visualize mode, this report shows the
parts of the ATerm that are not formatted correctly. By moving your
mouse over the nodes of ATerm, you can see the non-terminals that have
be inferred by format-check.
format-check reports all innermost format errors. That is, only the deepest format errors are reported. A format error is reported by showing the ATerm that is not in the correct format, and the inferred types of the children of the ATerm. In XHTML and visualize mode a format error of term in a list is presented by a red comma and term. This means that a type has been inferred for the term itself, but that it is not expected at this point in the list. If only the term is red, then no type could be inferred for the term itself.
In all modes format-check succeeds (exit code 0) if the ATerm contains no format errors. If the term does contain format errors, then format-check fails (exit code 1).
Use the regular tree grammar defined in
Use the normalized, regular tree grammar defined in
s as the start symbol, i.e. root of the ATerm. By default,
the start non-terminals defined for in the regular tree grammar are used.
Output report as an XHTML document. See above for a detailed description.
Output report as a coloured, pretty-printed ATerm. See above for a detailed description.
Run as fast as possible. Might reduce quality of error messages.
Check tool dependencies.
Common Input/Output Options
The input term given by the file name
In the absence of the
-i option, input
will be read from
The output will be written to the file given by the file name
In the absence of the
output will be written to
The output will be written in the binary (BAF) ATerm format.
ATerms in the BAF format require a lot less space than ones in the TAF format, but the Java ATerm library does not currently support baf ATerms. ATerms in the baf format is the preferred format of exchange between Stratego tools.
Common Debugging Options
Display usage information.
Keep intermediate results produced by the internal stages in the
pretty-printing process. This is only useful for debugging. A high
int indicates increased eagerness
for keeping intermediate results.
Default setting is 0, indicating that no intermediates will be kept.
Silent execution. Same as
Set verbosity level to numerical value
higher the number, the more information about pp-aterm's inner workings are
int can be set to either of the
following verbosity levels, given in increasing order of verbosity:
Displays the tool name and version.
To check the ATerm
tree.trm against the regular tree grammar in
$format-check --rtg tree-grammar.rtg -i tree.trm -o tree.checked.trm
If the term in
tree.trm is syntactially valid, i.e. it conforms to
the regular tree grammar, it will be copied to
tree.checked.trm. If not,
format-check wille exit with an error code and
tree.checked.trm will not be written to.
Please report bugs to
Copyright (C) 2002-2005 Eelco Visser
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.