diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-06-01 00:49:37 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-06-01 00:49:37 +0000 |
| commit | 471352e0956d1e9e1f0636933e792ed8650d5526 (patch) | |
| tree | dfacaaf551794af187b9b70ef59a82b42b68d45a /src/parser | |
| parent | 46a299aa48bcb0bff64bdb607f61f75a05987962 (diff) | |
type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 23 |
1 files changed, 10 insertions, 13 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 3c8d6e1ce..ca006daab 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1461,9 +1461,16 @@ postfixTerm[CVC4::Expr& f] f = EXPR_MANAGER->mkVar(TupleType(f.getType()).getTypes()[k]); } )*/ )* - (typeAscription[f, t] - { //f = MK_EXPR(CVC4::kind::APPLY_TYPE_ANNOTATION, MK_CONST(t), f); - } )? + ( typeAscription[f, t] + { if(t.isDatatype()) { + f = MK_EXPR(CVC4::kind::APPLY_TYPE_ASCRIPTION, MK_CONST(AscriptionType(t)), f); + } else { + if(f.getType() != t) { + PARSER_STATE->parseError("Type ascription not satisfied."); + } + } + } + )? ; bvTerm[CVC4::Expr& f] @@ -1666,16 +1673,6 @@ typeAscription[const CVC4::Expr& f, CVC4::Type& t] @init { } : COLON COLON type[t,CHECK_DECLARED] - { //if(f.getType() != t) { - // std::stringstream ss; - // ss << Expr::setlanguage(language::output::LANG_CVC4) - // << "type ascription not satisfied\n" - // << "term: " << f << '\n' - // << "has type: " << f.getType() << '\n' - // << "ascribed: " << t; - // PARSER_STATE->parseError(ss.str()); - //} - } ; /** |