considerable bindings interface work, some improvements to build

8 files changed, 56 insertions, 6 deletions

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index f1802c6c5..d87db20f5 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -19,7 +19,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 SUBDIRS = smt smt2 cvc
 
-nobase_lib_LTLIBRARIES = libcvc4parser.la
+lib_LTLIBRARIES = libcvc4parser.la
 if HAVE_CXXTESTGEN
 noinst_LTLIBRARIES = libcvc4parser_noinst.la
 endif
@@ -32,12 +32,14 @@ libcvc4parser_la_LIBADD = \
 	@builddir@/smt/libparsersmt.la \
 	@builddir@/smt2/libparsersmt2.la \
 	@builddir@/cvc/libparsercvc.la \
-	@builddir@/../lib/libreplacements.la
+	@builddir@/../lib/libreplacements.la \
+	-L@builddir@/.. -lcvc4
 libcvc4parser_noinst_la_LIBADD = \
 	@builddir@/smt/libparsersmt.la \
 	@builddir@/smt2/libparsersmt2.la \
 	@builddir@/cvc/libparsercvc.la \
-	@builddir@/../lib/libreplacements.la
+	@builddir@/../lib/libreplacements.la \
+	-L@builddir@/.. -lcvc4
 
 libcvc4parser_la_SOURCES = \
 	antlr_input.h \
diff --git a/src/parser/cvc4parser.i b/src/parser/cvc4parser.i
new file mode 100644
index 000000000..2ad3bf01d
--- /dev/null
+++ b/src/parser/cvc4parser.i
@@ -0,0 +1,15 @@
+%import "bindings/swig.h"
+
+%module CVC4Parser
+// nspace completely broken with Java packaging
+//%nspace;
+
+%{
+namespace CVC4 {}
+using namespace CVC4;
+%}
+
+%include "parser/parser_exception.i"
+%include "parser/input.i"
+%include "parser/parser.i"
+%include "parser/parser_builder.i"
diff --git a/src/parser/input.i b/src/parser/input.i
new file mode 100644
index 000000000..2a76e2b7a
--- /dev/null
+++ b/src/parser/input.i
@@ -0,0 +1,5 @@
+%{
+#include "parser/input.h"
+%}
+
+%include "parser/input.h"
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 5ce016b85..46544559a 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -53,12 +53,13 @@ enum DeclarationCheck {
   CHECK_UNDECLARED,
   /** Don't check anything */
   CHECK_NONE
-};
+};/* enum DeclarationCheck */
 
 /**
  * Returns a string representation of the given object (for
  * debugging).
  */
+inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) {
   switch(check) {
   case CHECK_NONE:
@@ -80,12 +81,13 @@ enum SymbolType {
   SYM_VARIABLE,
   /** Sorts */
   SYM_SORT
-};
+};/* enum SymbolType */
 
 /**
  * Returns a string representation of the given object (for
  * debugging).
  */
+inline std::ostream& operator<<(std::ostream& out, SymbolType type) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out, SymbolType type) {
   switch(type) {
   case SYM_VARIABLE:
diff --git a/src/parser/parser.i b/src/parser/parser.i
new file mode 100644
index 000000000..55119be9a
--- /dev/null
+++ b/src/parser/parser.i
@@ -0,0 +1,14 @@
+%{
+#include "parser/parser.h"
+%}
+
+namespace CVC4 {
+  namespace parser {
+    enum DeclarationCheck;
+    enum SymbolType;
+    %ignore operator<<(std::ostream&, DeclarationCheck);
+    %ignore operator<<(std::ostream&, SymbolType);
+  }/* namespace CVC4::parser */
+}/* namespace CVC4 */
+
+%include "parser/parser.h"
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 6f4f051ec..0463a079f 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -23,7 +23,7 @@
 
 #include <string>
 
-#include "input.h"
+#include "parser/input.h"
 
 #include "util/language.h"
 
diff --git a/src/parser/parser_builder.i b/src/parser/parser_builder.i
new file mode 100644
index 000000000..6b77356bc
--- /dev/null
+++ b/src/parser/parser_builder.i
@@ -0,0 +1,5 @@
+%{
+#include "parser/parser_builder.h"
+%}
+
+%include "parser/parser_builder.h"
diff --git a/src/parser/parser_exception.i b/src/parser/parser_exception.i
new file mode 100644
index 000000000..5be81034d
--- /dev/null
+++ b/src/parser/parser_exception.i
@@ -0,0 +1,7 @@
+%{
+#include "parser/parser_exception.h"
+%}
+
+%ignore CVC4::parser::ParserException::ParserException(const char*);
+
+%include "parser/parser_exception.h"