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<Node::iterator*>(it.d_iterator));
+ }
+}
+Expr::const_iterator& Expr::const_iterator::operator=(const const_iterator& it) {
+ if(d_iterator != NULL) {
+ delete reinterpret_cast<Node::iterator*>(d_iterator);
+ }
+ d_iterator = new Node::iterator(*reinterpret_cast<Node::iterator*>(it.d_iterator));
+ return *this;
+}
+Expr::const_iterator::~const_iterator() {
+ if(d_iterator != NULL) {
+ delete reinterpret_cast<Node::iterator*>(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<Node::iterator*>(d_iterator) ==
+ *reinterpret_cast<Node::iterator*>(it.d_iterator);
+}
+Expr::const_iterator& Expr::const_iterator::operator++() {
+ Assert(d_iterator != NULL);
+ ++*reinterpret_cast<Node::iterator*>(d_iterator);
+ return *this;
+}
+Expr::const_iterator Expr::const_iterator::operator++(int) {
+ Assert(d_iterator != NULL);
+ const_iterator it = *this;
+ ++*reinterpret_cast<Node::iterator*>(d_iterator);
+ return it;
+}
+Expr Expr::const_iterator::operator*() const {
+ Assert(d_iterator != NULL);
+ return (**reinterpret_cast<Node::iterator*>(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!");
#include <string>
#include <iostream>
+#include <iterator>
#include <stdint.h>
#include "util/exception.h"
// 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 {
*/
Expr operator[](unsigned i) const;
+ /**
+ * Returns the children of this Expr.
+ */
+ std::vector<Expr> getChildren() const {
+ return std::vector<Expr>(begin(), end());
+ }
+
+ /**
+ * Iterator type for the children of an Expr.
+ */
+ class const_iterator : public std::iterator<std::input_iterator_tag, Expr> {
+ 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.
*
${getConst_instantiations}
-#line 754 "${template}"
+#line 795 "${template}"
namespace expr {
)*/
)*
( 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.");
"::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"
"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 \
#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 {
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<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++ ){
- 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<expr::attr::DatatypeConstructorTypeGroundTermTag, Node> GroundTermAttr;
struct DatatypeConstructorTypeRule {
ascription_type.h \
datatype.h \
datatype.cpp \
+ matcher.h \
gmp_util.h \
sexpr.h \
stats.h \
#include "expr/node_manager.h"
#include "expr/node.h"
#include "util/recursion_breaker.h"
+#include "util/matcher.h"
using namespace std;
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;
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<Type> subst;
+ m.getMatches(subst);
+ vector<Type> 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;
// 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) {
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;
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
*/
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).
/** 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();
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<Type> Datatype::getParameters() const {
+ CheckArgument(isParametric(), this, "cannot get type parameters of a non-parametric datatype");
return d_params;
}
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#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<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++ ){
+ 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 */
projects / cvc5.git / commitdiff