diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-23 05:15:56 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-23 05:15:56 +0000 |
commit | 57b8c4c8581d2d3ffcf3d3a1bb228271cb4d074a (patch) | |
tree | 1c1781cc83118e4bbd2ad6939b16734c30a69f1a /src/parser/antlr_tracing.h | |
parent | 673d0e86b91094a58433c3ca71591fb0a0c60f84 (diff) |
* reviewed BooleanSimplification, added documentation & unit test
* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work
Diffstat (limited to 'src/parser/antlr_tracing.h')
-rw-r--r-- | src/parser/antlr_tracing.h | 87 |
1 files changed, 87 insertions, 0 deletions
diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h new file mode 100644 index 000000000..2c3e66c12 --- /dev/null +++ b/src/parser/antlr_tracing.h @@ -0,0 +1,87 @@ +/********************* */ +/*! \file antlr_tracing.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#ifndef __CVC4__PARSER__ANTLR_TRACING_H +#define __CVC4__PARSER__ANTLR_TRACING_H + +// only enable the hack with -DCVC4_TRACE_ANTLR +#ifdef CVC4_TRACE_ANTLR + +#include <iostream> +#include <string> +#include "util/output.h" + +/* The ANTLR lexer generator, as of v3.2, puts Java trace commands + * into our beautiful generated C lexer! How awful! This is clearly + * a bug (the parser generator traces with printf()), but we have to + * do something about it. Basically, the things look like this: + * + * System.out.println("something"+somethingElse+"another thing"); + * + * What to do to make this C++?! Alas, you cannot + * "#define System.out.println", because it has dots in it. + * So we do the following. Sigh. + * + * This is all C++, and the generated lexer/parser is C++, but that's + * ok here, we use the C++ compiler anyway! Plus, this is only code + * for **debugging** lexers and parsers. + */ + +/** A "System" object, just like in Java! */ +static struct __Cvc4System { + /** + * Helper class just to handle arbitrary string concatenation + * with Java syntax. In C++ you cannot do "char*" + "char*", + * so instead we fool the type system into calling + * JavaPrinter::operator+() for each item successively. + */ + struct JavaPrinter { + template <class T> + JavaPrinter operator+(const T& t) const { + ::CVC4::Message() << t; + return JavaPrinter(); + } + };/* struct JavaPrinter */ + + /** A "System.out" object, just like in Java! */ + struct { + /** + * By the time println() is called, we've completely + * evaluated (and thus printed) its entire argument, thanks + * to the call-by-value semantics of C. All that's left to + * do is print the newline. + */ + void println(JavaPrinter) { ::CVC4::Message() << std::endl; } + } out; +} System; + +// Now define println(): this kicks off the successive operator+() calls +// Also define "failed" because ANTLR 3.3 uses "failed" improperly. +// These are highly dependent on the bugs in a particular ANTLR release. +// These seem to work with ANTLR 3.3 as of 4/23/2011. A different trick +// works with ANTLR 3.2. EXPECT LOTS OF COMPILER WARNINGS. +#define println(x) println(({int failed=0;__Cvc4System::JavaPrinter()+x;})) +#undef ANTLR3_FPRINTF +#define ANTLR3_FPRINTF(args...) {int failed=0;fprintf(args);} +#undef ANTLR3_PRINTF +#define ANTLR3_PRINTF(args...) {int failed=0;printf(args);} + +#endif /* CVC4_TRACE_ANTLR */ + +#endif /* __CVC4__PARSER__ANTLR_TRACING_H */ |