format-check — checks whether an ATerm conforms to a given regular tree grammar (RTG)
format-check
[--rtg file]
[--rtg-nf file]
[-s s |--start s]
[--xhtml]
[--vis]
[--fast]
[--check]
[-i file | --input file]
[-o file | --output file]
[-b]
[-S | --silent]
[--verbose level]
[-k level | --keep level]
[-h | -? | --help]
[--about]
[--version]
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 (stdout
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 --vis option.
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 -r flag.
The XHTML mode is enabled with the --xhtml option.
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).
Grammar Options
--rtg file
Use the regular tree grammar defined in file.
--rtg-nf file
Use the normalized, regular tree grammar defined in file.
-s s, --start s
Use 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.
Reporting Options
--xhtmlOutput report as an XHTML document. See above for a detailed description.
--visOutput report as a coloured, pretty-printed ATerm. See above for a detailed description.
--fastRun as fast as possible. Might reduce quality of error messages.
Other Options
--checkCheck tool dependencies.
Common Input/Output Options
-i file
The input term given by the file name file
In the absence of the -i option, input
will be read from stdin.
-o file
The output will be written to the file given by the file name
file
In the absence of the -o option,
output will be written to stdout.
-bThe 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
--about
See --version.
-h, -?, --helpDisplay usage information.
--keep int
Keep intermediate results produced by the internal stages in the
pretty-printing process. This is only useful for debugging. A high
value of int indicates increased eagerness
for keeping intermediate results.
Default setting is 0, indicating that no intermediates will be kept.
-S, --silent
Silent execution. Same as --verbose .
0
--verbose int
Set verbosity level to numerical value int. The
higher the number, the more information about pp-aterm's inner workings are
printed.
Alternatively, int can be set to either of the
following verbosity levels, given in increasing order of verbosity:
emergency, alert, critical,
error, warning, notice,
info, debug, vomit.
--versionDisplays the tool name and version.
To check the ATerm tree.trm against the regular tree grammar in
tree-grammar.rtg, issue:
$ 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.
Copyright (C) 2002-2005 Eelco Visser <visser@acm.org>
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.