diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-27 21:01:54 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-27 21:01:54 -0500 |
commit | e25f99329c9905c67a565481dcb0d6a4499a7557 (patch) | |
tree | a85e7f998c4d4e722c80c8bcdedbc6292432bdb2 /src/parser/smt2/Smt2.g | |
parent | b2447df23d473184a7881ead02aa0b1e8f547d53 (diff) |
Support smt2 language "match" term (#3258)
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 176 |
1 files changed, 80 insertions, 96 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 21e09317d..9a8232df9 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1810,15 +1810,14 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] std::string attr; Expr attexpr; std::vector<Expr> patexprs; - std::vector<Expr> patconds; + std::vector<Expr> matchcases; std::unordered_set<std::string> names; std::vector< std::pair<std::string, Expr> > binders; - int match_vindex = -1; - std::vector<Type> match_ptypes; Type type; Type type2; api::Term atomTerm; ParseOp p; + std::vector<Type> argTypes; } : LPAREN_TOK quantOp[kind] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK @@ -1912,107 +1911,92 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] } LPAREN_TOK ( - /* match cases */ - LPAREN_TOK INDEX_TOK term[f, f2] { - if( match_vindex==-1 ){ - match_vindex = (int)patexprs.size(); + // case with non-nullary pattern + LPAREN_TOK LPAREN_TOK term[f, f2] { + args.clear(); + PARSER_STATE->pushScope(true); + // f should be a constructor + type = f.getType(); + Debug("parser-dt") << "Pattern head : " << f << " " << type << std::endl; + if (!type.isConstructor()) + { + PARSER_STATE->parseError("Pattern must be application of a constructor or a variable."); + } + if (Datatype::datatypeOf(f).isParametric()) + { + type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType()); + } + argTypes = static_cast<ConstructorType>(type).getArgTypes(); + } + // arguments of the pattern + ( symbol[name,CHECK_NONE,SYM_VARIABLE] { + if (args.size() >= argTypes.size()) + { + PARSER_STATE->parseError("Too many arguments for pattern."); + } + //make of proper type + Expr arg = PARSER_STATE->mkBoundVar(name, argTypes[args.size()]); + args.push_back( arg ); } - patexprs.push_back( f ); - patconds.push_back(MK_CONST(bool(true))); + )* + RPAREN_TOK term[f3, f2] { + // make the match case + std::vector<Expr> cargs; + cargs.push_back(f); + cargs.insert(cargs.end(),args.begin(),args.end()); + Expr c = MK_EXPR(kind::APPLY_CONSTRUCTOR,cargs); + Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST,args); + Expr mc = MK_EXPR(kind::MATCH_BIND_CASE, bvl, c, f3); + matchcases.push_back(mc); + // now, pop the scope + PARSER_STATE->popScope(); } RPAREN_TOK - | LPAREN_TOK LPAREN_TOK term[f, f2] { - args.clear(); - PARSER_STATE->pushScope(true); - //f should be a constructor - type = f.getType(); - Debug("parser-dt") << "Pattern head : " << f << " " << f.getType() << std::endl; - if( !type.isConstructor() ){ - PARSER_STATE->parseError("Pattern must be application of a constructor or a variable."); - } - if( Datatype::datatypeOf(f).isParametric() ){ - type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType()); - } - match_ptypes = ((ConstructorType)type).getArgTypes(); - } - //arguments - ( symbol[name,CHECK_NONE,SYM_VARIABLE] { - if( args.size()>=match_ptypes.size() ){ - PARSER_STATE->parseError("Too many arguments for pattern."); - } - //make of proper type - Expr arg = PARSER_STATE->mkBoundVar(name, match_ptypes[args.size()]); - args.push_back( arg ); - } - )* - RPAREN_TOK - term[f3, f2] { - const DatatypeConstructor& dtc = Datatype::datatypeOf(f)[Datatype::indexOf(f)]; - if( args.size()!=dtc.getNumArgs() ){ - PARSER_STATE->parseError("Bad number of arguments for application of constructor in pattern."); - } - //FIXME: make MATCH a kind and make this a rewrite - // build a lambda - std::vector<Expr> largs; - largs.push_back( MK_EXPR( CVC4::kind::BOUND_VAR_LIST, args ) ); - largs.push_back( f3 ); - std::vector< Expr > aargs; - aargs.push_back( MK_EXPR( CVC4::kind::LAMBDA, largs ) ); - for( unsigned i=0; i<dtc.getNumArgs(); i++ ){ - //can apply total version since we will be guarded by ITE condition - // however, we need to apply partial version since we don't have the internal selector available - aargs.push_back( MK_EXPR( CVC4::kind::APPLY_SELECTOR, dtc[i].getSelector(), expr ) ); - } - patexprs.push_back( MK_EXPR( CVC4::kind::APPLY_UF, aargs ) ); - patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) ); - } - RPAREN_TOK - { PARSER_STATE->popScope(); } - | LPAREN_TOK symbol[name,CHECK_DECLARED,SYM_VARIABLE] { - f = PARSER_STATE->getVariable(name); - type = f.getType(); - if( !type.isConstructor() || !((ConstructorType)type).getArgTypes().empty() ){ - PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern."); - } - } - term[f3, f2] { - const DatatypeConstructor& dtc = Datatype::datatypeOf(f)[Datatype::indexOf(f)]; - patexprs.push_back( f3 ); - patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) ); - } - RPAREN_TOK - )+ - RPAREN_TOK RPAREN_TOK { - if( match_vindex==-1 ){ - const Datatype& dt = ((DatatypeType)expr.getType()).getDatatype(); - std::map< unsigned, bool > processed; - unsigned count = 0; - //ensure that all datatype constructors are matched (to ensure exhaustiveness) - for( unsigned i=0; i<patconds.size(); i++ ){ - unsigned curr_index = Datatype::indexOf(patconds[i].getOperator()); - if( curr_index<0 && curr_index>=dt.getNumConstructors() ){ - PARSER_STATE->parseError("Pattern is not legal for the head of a match."); + // case with nullary or variable pattern + | LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] { + if (PARSER_STATE->isDeclared(name,SYM_VARIABLE)) + { + f = PARSER_STATE->getVariable(name); + type = f.getType(); + if (!type.isConstructor() || + !((ConstructorType)type).getArgTypes().empty()) + { + PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern."); + } + // make nullary constructor application + f = MK_EXPR(kind::APPLY_CONSTRUCTOR, f); } - if( processed.find( curr_index )==processed.end() ){ - processed[curr_index] = true; - count++; + else + { + // it has the type of the head expr + f = PARSER_STATE->mkBoundVar(name, expr.getType()); } } - if( count!=dt.getNumConstructors() ){ - PARSER_STATE->parseError("Patterns are not exhaustive in a match construct."); - } - } - //now, make the ITE - int end_index = match_vindex==-1 ? patexprs.size()-1 : match_vindex; - bool first_time = true; - for( int index = end_index; index>=0; index-- ){ - if( first_time ){ - expr = patexprs[index]; - first_time = false; - }else{ - expr = MK_EXPR( CVC4::kind::ITE, patconds[index], patexprs[index], expr ); + term[f3, f2] { + Expr mc; + if (f.getKind() == kind::BOUND_VARIABLE) + { + Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, f); + mc = MK_EXPR(kind::MATCH_BIND_CASE, bvl, f, f3); + } + else + { + mc = MK_EXPR(kind::MATCH_CASE, f, f3); + } + matchcases.push_back(mc); } + RPAREN_TOK + )+ + RPAREN_TOK RPAREN_TOK { + //now, make the match + if (matchcases.empty()) + { + PARSER_STATE->parseError("Must have at least one case in match."); } + std::vector<Expr> mchildren; + mchildren.push_back(expr); + mchildren.insert(mchildren.end(), matchcases.begin(), matchcases.end()); + expr = MK_EXPR(kind::MATCH, mchildren); } /* attributed expressions */ |