From 4a696409769044ad155a56eeb00c9d85246ca0b4 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 3 Jun 2011 05:30:54 +0000 Subject: [PATCH] datatypes work --- src/expr/expr_template.cpp | 56 +++++++++ src/expr/expr_template.h | 45 ++++++- src/parser/cvc/Cvc.g | 10 +- src/theory/datatypes/kinds | 4 +- .../datatypes/theory_datatypes_type_rules.h | 77 +----------- src/util/Makefile.am | 1 + src/util/datatype.cpp | 21 +++- src/util/datatype.h | 28 ++++- src/util/matcher.h | 110 ++++++++++++++++++ 9 files changed, 262 insertions(+), 90 deletions(-) create mode 100644 src/util/matcher.h diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 286ddf611..7c2d02809 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -208,6 +208,62 @@ Type Expr::getType(bool check) const throw (TypeCheckingException) { return d_exprManager->getType(*this, check); } +Expr::const_iterator::const_iterator() : + d_iterator(NULL) { +} +Expr::const_iterator::const_iterator(void* v) : + d_iterator(v) { +} +Expr::const_iterator::const_iterator(const const_iterator& it) { + if(it.d_iterator == NULL) { + d_iterator = NULL; + } else { + d_iterator = new Node::iterator(*reinterpret_cast(it.d_iterator)); + } +} +Expr::const_iterator& Expr::const_iterator::operator=(const const_iterator& it) { + if(d_iterator != NULL) { + delete reinterpret_cast(d_iterator); + } + d_iterator = new Node::iterator(*reinterpret_cast(it.d_iterator)); + return *this; +} +Expr::const_iterator::~const_iterator() { + if(d_iterator != NULL) { + delete reinterpret_cast(d_iterator); + } +} +bool Expr::const_iterator::operator==(const const_iterator& it) const { + if(d_iterator == NULL || it.d_iterator == NULL) { + return false; + } + return *reinterpret_cast(d_iterator) == + *reinterpret_cast(it.d_iterator); +} +Expr::const_iterator& Expr::const_iterator::operator++() { + Assert(d_iterator != NULL); + ++*reinterpret_cast(d_iterator); + return *this; +} +Expr::const_iterator Expr::const_iterator::operator++(int) { + Assert(d_iterator != NULL); + const_iterator it = *this; + ++*reinterpret_cast(d_iterator); + return it; +} +Expr Expr::const_iterator::operator*() const { + Assert(d_iterator != NULL); + return (**reinterpret_cast(d_iterator)).toExpr(); +} + +Expr::const_iterator Expr::begin() const { + return Expr::const_iterator(new Node::iterator(d_node->begin())); +} + +Expr::const_iterator Expr::end() const { + return Expr::const_iterator(new Node::iterator(d_node->end())); +} + std::string Expr::toString() const { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index b0157adbf..bffb37ddb 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -30,6 +30,7 @@ ${includes} #include #include +#include #include #include "util/exception.h" @@ -39,7 +40,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 43 "${template}" +#line 44 "${template}" namespace CVC4 { @@ -261,6 +262,46 @@ public: */ Expr operator[](unsigned i) const; + /** + * Returns the children of this Expr. + */ + std::vector getChildren() const { + return std::vector(begin(), end()); + } + + /** + * Iterator type for the children of an Expr. + */ + class const_iterator : public std::iterator { + void* d_iterator; + explicit const_iterator(void*); + + friend class Expr;// to access void* constructor + + public: + const_iterator(); + const_iterator(const const_iterator& it); + const_iterator& operator=(const const_iterator& it); + ~const_iterator(); + bool operator==(const const_iterator& it) const; + bool operator!=(const const_iterator& it) const { + return !(*this == it); + } + const_iterator& operator++(); + const_iterator operator++(int); + Expr operator*() const; + };/* class Expr::const_iterator */ + + /** + * Returns an iterator to the first child of this Expr. + */ + const_iterator begin() const; + + /** + * Returns an iterator to one-off-the-last child of this Expr. + */ + const_iterator end() const; + /** * Check if this is an expression that has an operator. * @@ -750,7 +791,7 @@ public: ${getConst_instantiations} -#line 754 "${template}" +#line 795 "${template}" namespace expr { 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 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."); diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 1cdefa60b..47896b1e0 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -34,7 +34,7 @@ cardinality TESTER_TYPE \ "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" -parameterized APPLY_CONSTRUCTOR CONSTRUCTOR_TYPE 0: "constructor application" +parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application" parameterized APPLY_SELECTOR SELECTOR_TYPE 1: "selector application" @@ -63,7 +63,7 @@ well-founded PARAMETRIC_DATATYPE\ "util/datatype.h" parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \ - "type ascription, for nullary, parameteric datatype constructors" + "type ascription, for datatype constructor applications" constant ASCRIPTION_TYPE \ ::CVC4::AscriptionType \ ::CVC4::AscriptionTypeHashStrategy \ diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 270313e0f..5ff01924b 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -21,6 +21,8 @@ #ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H +#include "util/matcher.h" + namespace CVC4 { namespace expr { @@ -32,81 +34,6 @@ 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 ); - Debug("typecheck-idt") << "instantiating matcher for " << dt << std::endl; - for(unsigned i = 0; i < argTypes.size(); ++i) { - if(dt.isParameterInstantiated(i)) { - Debug("typecheck-idt") << "++ instantiate param " << i << " : " << d_types[i] << std::endl; - d_match[i] = d_types[i]; - } - } - } - ~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 ){ - Debug("typecheck-idt") << "doMatching() : " << base << " : " << match << std::endl; - 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(); - Debug("typecheck-idt") << "++ match on " << index << " : " << d_match[index] << std::endl; - 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& types ) { - types.clear(); - for( int i=0; i<(int)d_match.size(); i++ ){ - types.push_back( d_types[i].toType() ); - } - } - void getMatches( std::vector& types ) { - types.clear(); - for( int i=0; i<(int)d_match.size(); i++ ){ - if(d_match[i].isNull()) { - types.push_back( d_types[i].toType() ); - } else { - types.push_back( d_match[i].toType() ); - } - } - } -};/* class Matcher */ - - typedef expr::Attribute GroundTermAttr; struct DatatypeConstructorTypeRule { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index b8f336f2d..dc1da0659 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -41,6 +41,7 @@ libutil_la_SOURCES = \ ascription_type.h \ datatype.h \ datatype.cpp \ + matcher.h \ gmp_util.h \ sexpr.h \ stats.h \ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 4b84d2955..a06a7c2b5 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -27,6 +27,7 @@ #include "expr/node_manager.h" #include "expr/node.h" #include "util/recursion_breaker.h" +#include "util/matcher.h" using namespace std; @@ -261,7 +262,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) { CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!"); }else{ if( t!=groundTerm.getType() ){ - groundTerm = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + groundTerm = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, NodeManager::currentNM()->mkConst(AscriptionType(t)), groundTerm).toExpr(); } return groundTerm; @@ -511,6 +512,19 @@ Expr Datatype::Constructor::getConstructor() const { return d_constructor; } +Type Datatype::Constructor::getSpecializedConstructorType(Type returnType) const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + const Datatype& dt = Datatype::datatypeOf(d_constructor); + CheckArgument(dt.isParametric(), this, "this datatype constructor is not yet resolved"); + DatatypeType dtt = DatatypeType(dt.d_self); + Matcher m(dtt); + m.doMatching( TypeNode::fromType(dtt), TypeNode::fromType(returnType) ); + vector subst; + m.getMatches(subst); + vector params = dt.getParameters(); + return d_constructor.getType().substitute(subst, params); +} + Expr Datatype::Constructor::getTester() const { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_tester; @@ -625,9 +639,10 @@ Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionExceptio // for each selector, get a ground term Assert( t.isDatatype() ); - std::vector< Type > instTypes; - std::vector< Type > paramTypes = DatatypeType(t).getDatatype().getParameters(); + std::vector< Type > instTypes; + std::vector< Type > paramTypes; if( DatatypeType(t).isParametric() ){ + paramTypes = DatatypeType(t).getDatatype().getParameters(); instTypes = DatatypeType(t).getParamTypes(); } for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { diff --git a/src/util/datatype.h b/src/util/datatype.h index 3506616d6..477b16f66 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -169,8 +169,8 @@ public: Expr getSelector() const; /** - * Get the associated constructor for this constructor argument; this call is - * only permitted after resolution. + * Get the associated constructor for this constructor argument; + * this call is only permitted after resolution. */ Expr getConstructor() const; @@ -216,10 +216,10 @@ public: throw(AssertionException, DatatypeResolutionException); friend class Datatype; - /** */ - Type doParametricSubstitution( Type range, - const std::vector< SortConstructorType >& paramTypes, - const std::vector< DatatypeType >& paramReplacements ); + /** @FIXME document this! */ + Type doParametricSubstitution(Type range, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements); public: /** * Create a new Datatype constructor with the given name for the @@ -272,6 +272,12 @@ public: */ inline size_t getNumArgs() const throw(); + /** + * Get the specialized constructor type for a parametric + * constructor; this call is only permitted after resolution. + */ + Type getSpecializedConstructorType(Type returnType) const; + /** * Return the cardinality of this constructor (the product of the * cardinalities of its arguments). @@ -369,6 +375,9 @@ public: /** Get the number of constructors (so far) for this Datatype. */ inline size_t getNumConstructors() const throw(); + /** Is this datatype parametric? */ + inline bool isParametric() const throw(); + /** Get the nubmer of type parameters */ inline size_t getNumParameters() const throw(); @@ -527,15 +536,22 @@ inline size_t Datatype::getNumConstructors() const throw() { return d_constructors.size(); } +inline bool Datatype::isParametric() const throw() { + return d_params.size() > 0; +} + inline size_t Datatype::getNumParameters() const throw() { return d_params.size(); } inline Type Datatype::getParameter( unsigned int i ) const { + CheckArgument(isParametric(), this, "cannot get type parameter of a non-parametric datatype"); + CheckArgument(i < d_params.size(), i, "type parameter index out of range for datatype"); return d_params[i]; } inline std::vector Datatype::getParameters() const { + CheckArgument(isParametric(), this, "cannot get type parameters of a non-parametric datatype"); return d_params; } diff --git a/src/util/matcher.h b/src/util/matcher.h new file mode 100644 index 000000000..2c55309d3 --- /dev/null +++ b/src/util/matcher.h @@ -0,0 +1,110 @@ +/********************* */ +/*! \file matcher.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A class representing a type matcher + ** + ** A class representing a type matcher. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__MATCHER_H +#define __CVC4__MATCHER_H + +#include +#include +#include +#include +#include "util/Assert.h" +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { + +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 ); + Debug("typecheck-idt") << "instantiating matcher for " << dt << std::endl; + for(unsigned i = 0; i < argTypes.size(); ++i) { + if(dt.isParameterInstantiated(i)) { + Debug("typecheck-idt") << "++ instantiate param " << i << " : " << d_types[i] << std::endl; + d_match[i] = d_types[i]; + } + } + } + ~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 ){ + Debug("typecheck-idt") << "doMatching() : " << base << " : " << match << std::endl; + 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(); + Debug("typecheck-idt") << "++ match on " << index << " : " << d_match[index] << std::endl; + 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& types ) { + types.clear(); + for( int i=0; i<(int)d_match.size(); i++ ){ + types.push_back( d_types[i].toType() ); + } + } + void getMatches( std::vector& types ) { + types.clear(); + for( int i=0; i<(int)d_match.size(); i++ ){ + if(d_match[i].isNull()) { + types.push_back( d_types[i].toType() ); + } else { + types.push_back( d_match[i].toType() ); + } + } + } +};/* class Matcher */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__MATCHER_H */ -- 2.30.2