summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Makefile.am1
-rw-r--r--src/util/datatype.cpp21
-rw-r--r--src/util/datatype.h28
-rw-r--r--src/util/matcher.h110
4 files changed, 151 insertions, 9 deletions
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<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;
@@ -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
@@ -273,6 +273,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<Type> 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 <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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback