diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-05-13 22:02:52 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-05-13 22:02:52 +0000 |
commit | 8d54316e7ff784a8d66da9ecc2d289ab463761c2 (patch) | |
tree | c7b5351b372cb360780ce62935fb2cfb5792299a /src/theory | |
parent | 69c9ec0e1e42f3f2f2f79d3e98398c5cd1559c66 (diff) |
added support for parametric datatypes, updated cvc parser to handle parametric datatypes, type ascriptions are not implemented yet
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 3 | ||||
-rw-r--r-- | src/theory/datatypes/kinds | 9 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 3 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 169 |
4 files changed, 155 insertions, 29 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index eea15d6b6..df8cb6eb8 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -43,7 +43,8 @@ public: return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(result)); } else { - const Datatype& dt = in[0].getType().getConst<Datatype>(); + //const Datatype& dt = in[0].getType().getConst<Datatype>(); + const Datatype& dt = DatatypeType(in[0].getType().toType()).getDatatype(); if(dt.getNumConstructors() == 1) { // only one constructor, so it must be Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 37a65a2b0..d08e3875c 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -53,4 +53,13 @@ well-founded DATATYPE_TYPE \ "%TYPE%.getConst<Datatype>().mkGroundTerm()" \ "util/datatype.h" +operator PARAMETRIC_DATATYPE 1: "parametric datatype" +cardinality PARAMETRIC_DATATYPE \ + "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality()" \ + "util/datatype.h" +well-founded PARAMETRIC_DATATYPE\ + "DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \ + "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm()" \ + "util/datatype.h" + endtheory diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 6808ef749..2f0b82f7c 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -851,7 +851,8 @@ void TheoryDatatypes::addTermToLabels( Node t ) { const Datatype& dt = ((DatatypeType)(t.getType()).toType()).getDatatype(); if( dt.getNumConstructors()==1 ){ Node tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), t ); - addTester( tester ); + lbl->push_back( tester ); + d_checkMap[ t ] = true; d_em.addNodeAxiom( tester, Reason::idt_texhaust ); } d_labels.insertDataFromContextMemory(tmp, lbl); diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index bc1581f14..dc2e95f9d 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -32,6 +32,70 @@ namespace expr { namespace theory { namespace datatypes { +class Matcher +{ +private: + std::vector< TypeNode > d_types; + std::vector< TypeNode > d_match; +public: + Matcher(){} + Matcher( DatatypeType dt ){ + std::vector< Type > argTypes = dt.getParamTypes(); + addTypes( argTypes ); + } + ~Matcher(){} + + void addType( Type t ){ + d_types.push_back( TypeNode::fromType( t ) ); + d_match.push_back( TypeNode::null() ); + } + void addTypes( std::vector< Type > types ){ + for( int i=0; i<(int)types.size(); i++ ){ + addType( types[i] ); + } + } + + bool doMatching( TypeNode base, TypeNode match ){ + std::vector< TypeNode >::iterator i = std::find( d_types.begin(), d_types.end(), base ); + if( i!=d_types.end() ){ + int index = i - d_types.begin(); + if( !d_match[index].isNull() && d_match[index]!=match ){ + return false; + }else{ + d_match[ i - d_types.begin() ] = match; + return true; + } + }else if( base==match ){ + return true; + }else if( base.getKind()!=match.getKind() || base.getNumChildren()!=match.getNumChildren() ){ + return false; + }else{ + for( int i=0; i<(int)base.getNumChildren(); i++ ){ + if( !doMatching( base[i], match[i] ) ){ + return false; + } + } + return true; + } + } + + TypeNode getMatch( unsigned int i ){ return d_match[i]; } + void getTypes( std::vector<Type>& types ) { + types.clear(); + for( int i=0; i<(int)d_match.size(); i++ ){ + types.push_back( d_types[i].toType() ); + } + } + void getMatches( std::vector<Type>& types ) { + types.clear(); + for( int i=0; i<(int)d_match.size(); i++ ){ + Assert( !d_match[i].isNull() ); //verify that all types have been set + types.push_back( d_match[i].toType() ); + } + } +}; + + typedef expr::Attribute<expr::attr::DatatypeConstructorTypeGroundTermTag, Node> GroundTermAttr; struct DatatypeConstructorTypeRule { @@ -39,24 +103,43 @@ struct DatatypeConstructorTypeRule { throw(TypeCheckingExceptionPrivate) { Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); TypeNode consType = n.getOperator().getType(check); - if(check) { - Debug("typecheck-idt") << "typecheck cons: " << n << " " << n.getNumChildren() << std::endl; - Debug("typecheck-idt") << "cons type: " << consType << " " << consType.getNumChildren() << std::endl; - if(n.getNumChildren() != consType.getNumChildren() - 1) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the constructor type"); - } - TNode::iterator child_it = n.begin(); - TNode::iterator child_it_end = n.end(); - TypeNode::iterator tchild_it = consType.begin(); + Type t = consType.getConstructorRangeType().toType(); + Assert( t.isDatatype() ); + DatatypeType dt = DatatypeType(t); + TNode::iterator child_it = n.begin(); + TNode::iterator child_it_end = n.end(); + TypeNode::iterator tchild_it = consType.begin(); + if( ( dt.isParametric() || check ) && n.getNumChildren() != consType.getNumChildren() - 1 ){ + throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the constructor type"); + } + if( dt.isParametric() ){ + Debug("typecheck-idt") << "typecheck parameterized datatype " << n << std::endl; + Matcher m( dt ); for(; child_it != child_it_end; ++child_it, ++tchild_it) { TypeNode childType = (*child_it).getType(check); - Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl; - if(childType != *tchild_it) { - throw TypeCheckingExceptionPrivate(n, "bad type for constructor argument"); + if( !m.doMatching( *tchild_it, childType ) ){ + throw TypeCheckingExceptionPrivate(n, "matching failed for parameterized constructor"); + } + } + std::vector< Type > instTypes; + m.getMatches( instTypes ); + TypeNode range = TypeNode::fromType( dt.instantiate( instTypes ) ); + Debug("typecheck-idt") << "Return " << range << std::endl; + return range; + }else{ + if(check) { + Debug("typecheck-idt") << "typecheck cons: " << n << " " << n.getNumChildren() << std::endl; + Debug("typecheck-idt") << "cons type: " << consType << " " << consType.getNumChildren() << std::endl; + for(; child_it != child_it_end; ++child_it, ++tchild_it) { + TypeNode childType = (*child_it).getType(check); + Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl; + if(childType != *tchild_it) { + throw TypeCheckingExceptionPrivate(n, "bad type for constructor argument"); + } } } + return consType.getConstructorRangeType(); } - return consType.getConstructorRangeType(); } };/* struct DatatypeConstructorTypeRule */ @@ -65,18 +148,38 @@ struct DatatypeSelectorTypeRule { throw(TypeCheckingExceptionPrivate) { Assert(n.getKind() == kind::APPLY_SELECTOR); TypeNode selType = n.getOperator().getType(check); - Debug("typecheck-idt") << "typecheck sel: " << n << std::endl; - Debug("typecheck-idt") << "sel type: " << selType << std::endl; - if(check) { - if(n.getNumChildren() != 1) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the selector type"); - } + Type t = selType[0].toType(); + Assert( t.isDatatype() ); + DatatypeType dt = DatatypeType(t); + if( ( dt.isParametric() || check ) && n.getNumChildren() != 1 ){ + throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the selector type"); + } + if( dt.isParametric() ){ + Debug("typecheck-idt") << "typecheck parameterized sel: " << n << std::endl; + Matcher m( dt ); TypeNode childType = n[0].getType(check); - if(selType[0] != childType) { - throw TypeCheckingExceptionPrivate(n, "bad type for selector argument"); + if( !m.doMatching( selType[0], childType ) ){ + throw TypeCheckingExceptionPrivate(n, "matching failed for selector argument of parameterized datatype"); } + std::vector< Type > types, matches; + m.getTypes( types ); + m.getMatches( matches ); + Type range = selType[1].toType(); + range = range.substitute( types, matches ); + Debug("typecheck-idt") << "Return " << range << std::endl; + return TypeNode::fromType( range ); + }else{ + if(check) { + Debug("typecheck-idt") << "typecheck sel: " << n << std::endl; + Debug("typecheck-idt") << "sel type: " << selType << std::endl; + TypeNode childType = n[0].getType(check); + if(selType[0] != childType) { + Debug("typecheck-idt") << "ERROR: " << selType[0].getKind() << " " << childType.getKind() << std::endl; + throw TypeCheckingExceptionPrivate(n, "bad type for selector argument"); + } + } + return selType[1]; } - return selType[1]; } };/* struct DatatypeSelectorTypeRule */ @@ -90,10 +193,21 @@ struct DatatypeTesterTypeRule { } TypeNode testType = n.getOperator().getType(check); TypeNode childType = n[0].getType(check); - Debug("typecheck-idt") << "typecheck test: " << n << std::endl; - Debug("typecheck-idt") << "test type: " << testType << std::endl; - if(testType[0] != childType) { - throw TypeCheckingExceptionPrivate(n, "bad type for tester argument"); + Type t = testType[0].toType(); + Assert( t.isDatatype() ); + DatatypeType dt = DatatypeType(t); + if( dt.isParametric() ){ + Debug("typecheck-idt") << "typecheck parameterized tester: " << n << std::endl; + Matcher m( dt ); + if( !m.doMatching( testType[0], childType ) ){ + throw TypeCheckingExceptionPrivate(n, "matching failed for tester argument of parameterized datatype"); + } + }else{ + Debug("typecheck-idt") << "typecheck test: " << n << std::endl; + Debug("typecheck-idt") << "test type: " << testType << std::endl; + if(testType[0] != childType) { + throw TypeCheckingExceptionPrivate(n, "bad type for tester argument"); + } } } return nodeManager->booleanType(); @@ -140,7 +254,8 @@ struct ConstructorProperties { // Constructors within the same Datatype could share the same // type. So we scan through the datatype to find one that // matches. - const Datatype& dt = type[type.getNumChildren() - 1].getConst<Datatype>(); + //const Datatype& dt = type[type.getNumChildren() - 1].getConst<Datatype>(); + const Datatype& dt = DatatypeType(type[type.getNumChildren() - 1].toType()).getDatatype(); for(Datatype::const_iterator i = dt.begin(), i_end = dt.end(); i != i_end; |