diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-04 03:42:56 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-04 03:42:56 +0000 |
commit | 1ce8e28d5976e1ab30099cb9e6943514497d2980 (patch) | |
tree | 1a9382fb62b38e3b5768da951b7c684f1b8688e7 /src/expr/expr_template.cpp | |
parent | 69c2d3e702f8ec0bd0eec4a481a07571131aabeb (diff) |
Type-checking classes and hooks (not tested yet).
Diffstat (limited to 'src/expr/expr_template.cpp')
-rw-r--r-- | src/expr/expr_template.cpp | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index ba7032e34..a1be2ece8 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -14,6 +14,7 @@ **/ #include "expr/expr.h" +#include "expr/expr_manager.h" #include "expr/node.h" #include "util/Assert.h" @@ -26,7 +27,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 30 "${template}" +#line 31 "${template}" using namespace CVC4::kind; @@ -37,6 +38,25 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) { return out; } +TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message) +: Exception(message), d_expr(new Expr(expr)) +{ +} + +TypeCheckingException::~TypeCheckingException() throw () { + delete d_expr; +} + +std::string TypeCheckingException::toString() const { + std::stringstream ss; + ss << "Error type-checking " << d_expr << ": " << d_msg; + return ss.str(); +} + +Expr TypeCheckingException::getExpression() const { + return *d_expr; +} + Expr::Expr() : d_node(new Node), d_exprManager(NULL) { @@ -129,7 +149,7 @@ Expr Expr::getOperator() const { return Expr(d_exprManager, new Node(d_node->getOperator())); } -Type Expr::getType() const { +Type Expr::getType() const throw (TypeCheckingException) { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); return d_exprManager->getType(*this); |