diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-06-01 01:13:21 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-06-01 01:13:21 +0000 |
commit | c6a8319b05cf1b156691132b3bec1f56ca6588e0 (patch) | |
tree | 44f204e88ad5e820181c88882759f727cc133332 /src | |
parent | 471352e0956d1e9e1f0636933e792ed8650d5526 (diff) |
minor fix, and better output for type errors
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/type_node.cpp | 3 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 6 |
2 files changed, 6 insertions, 3 deletions
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 7376b0080..b9047307d 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -209,8 +209,9 @@ bool TypeNode::isInstantiatedDatatype() const { } const Datatype& dt = (*this)[0].getConst<Datatype>(); unsigned n = dt.getNumParameters(); + Assert(n < getNumChildren()); for(unsigned i = 0; i < n; ++i) { - if(TypeNode::fromType(dt.getParameter(i)) == (*this)[n + 1]) { + if(TypeNode::fromType(dt.getParameter(i)) == (*this)[i + 1]) { return false; } } diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index cffc95ab2..f343848d8 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -82,8 +82,10 @@ class EqualityTypeRule { if ( lhsType != rhsType ) { std::stringstream ss; ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)); - ss << "Types do not match in equation "; - ss << "[" << lhsType << "<>" << rhsType << "]"; + ss << "Types do not match in equation:" << std::endl; + ss << "Equation: " << n << std::endl; + ss << "Type 1: " << lhsType << std::endl; + ss << "Type 2: " << rhsType << std::endl; throw TypeCheckingExceptionPrivate(n, ss.str()); } |