diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-05-27 00:06:42 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-05-27 10:57:16 -0400 |
commit | 8d3aca31964a314b4c84679d6ec0a223bcc30dda (patch) | |
tree | 6609948d9041366cb5d5f87d7828593971fe3f07 /src | |
parent | d6267f3afa9b535a4a858011533382a518ee0e1a (diff) |
Improved type-checking for tuple and record selects.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index d08b511dd..09d43b3bc 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -282,6 +282,9 @@ struct TupleTypeRule { struct TupleSelectTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { Assert(n.getKind() == kind::TUPLE_SELECT); + if(n.getOperator().getKind() != kind::TUPLE_SELECT_OP) { + throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator"); + } const TupleSelect& ts = n.getOperator().getConst<TupleSelect>(); TypeNode tupleType = n[0].getType(check); if(!tupleType.isTuple()) { @@ -422,6 +425,9 @@ struct RecordSelectTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { Assert(n.getKind() == kind::RECORD_SELECT); NodeManagerScope nms(nodeManager); + if(n.getOperator().getKind() != kind::RECORD_SELECT_OP) { + throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator"); + } const RecordSelect& rs = n.getOperator().getConst<RecordSelect>(); TypeNode recordType = n[0].getType(check); if(!recordType.isRecord()) { |