diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-06-03 05:30:54 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-06-03 05:30:54 +0000 |
commit | 4a696409769044ad155a56eeb00c9d85246ca0b4 (patch) | |
tree | 27a131cb40138049508150fc5aa2c0330b52f704 /src/parser/cvc/Cvc.g | |
parent | d935021323ca343da5359fa54bc62184d47ccd1b (diff) |
datatypes work
Diffstat (limited to 'src/parser/cvc/Cvc.g')
-rw-r--r-- | src/parser/cvc/Cvc.g | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index ca006daab..d6165b435 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1462,8 +1462,14 @@ postfixTerm[CVC4::Expr& f] )*/ )* ( typeAscription[f, t] - { if(t.isDatatype()) { - f = MK_EXPR(CVC4::kind::APPLY_TYPE_ASCRIPTION, MK_CONST(AscriptionType(t)), f); + { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) { + std::vector<CVC4::Expr> v; + Expr e = f.getOperator(); + const Datatype::Constructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)]; + v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION, + MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator()[0] )); + v.insert(v.end(), f.begin(), f.end()); + f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v); } else { if(f.getType() != t) { PARSER_STATE->parseError("Type ascription not satisfied."); |