summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/declaration_scope.cpp8
-rw-r--r--src/expr/declaration_scope.h2
-rw-r--r--src/expr/expr_manager_template.cpp17
-rw-r--r--src/expr/type.cpp18
-rw-r--r--src/expr/type.h5
-rw-r--r--src/expr/type_node.cpp4
-rw-r--r--src/expr/type_node.h3
-rw-r--r--src/parser/parser.cpp16
-rw-r--r--src/parser/parser.h7
-rw-r--r--src/theory/datatypes/datatypes_rewriter.h1
-rw-r--r--src/theory/datatypes/kinds10
-rw-r--r--src/theory/datatypes/theory_datatypes_type_rules.h3
-rw-r--r--src/util/Makefile.am1
-rw-r--r--src/util/ascription_type.h66
-rw-r--r--src/util/datatype.cpp34
-rw-r--r--src/util/datatype.h2
16 files changed, 136 insertions, 61 deletions
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index 79accf43a..ae91efa68 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -144,10 +144,10 @@ Type DeclarationScope::lookupType(const std::string& name,
Debug("sort") << "instance is " << instantiation << endl;
return instantiation;
- }else if( p.second.isDatatype() ){
- Assert( DatatypeType( p.second ).isParametric() );
+ } else if(p.second.isDatatype()) {
+ Assert( DatatypeType(p.second).isParametric() );
return DatatypeType(p.second).instantiate(params);
- }else {
+ } else {
if(Debug.isOn("sort")) {
Debug("sort") << "instantiating using a sort substitution" << endl;
Debug("sort") << "have formals [";
@@ -170,7 +170,7 @@ Type DeclarationScope::lookupType(const std::string& name,
}
}
-size_t DeclarationScope::lookupArity( const std::string& name ){
+size_t DeclarationScope::lookupArity(const std::string& name) {
pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
return p.first.size();
}
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 4cdb71ddc..d695a3bf8 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -177,7 +177,7 @@ public:
/**
* Lookup the arity of a bound parameterized type.
*/
- size_t lookupArity( const std::string& name );
+ size_t lookupArity(const std::string& name);
/**
* Pop a scope level. Deletes all bindings since the last call to
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index c32dbbc7d..038f58f95 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -506,16 +506,17 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
i != i_end;
++i) {
TypeNode* typeNode;
- if( (*i).getNumParameters()==0 ){
+ if( (*i).getNumParameters() == 0 ) {
typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
- }else{
+ } else {
TypeNode cons = d_nodeManager->mkTypeConst(*i);
std::vector< TypeNode > params;
params.push_back( cons );
- for( unsigned int ip=0; ip<(*i).getNumParameters(); ip++ ){
+ for( unsigned int ip = 0; ip < (*i).getNumParameters(); ++ip ) {
params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) );
}
- typeNode = new TypeNode( d_nodeManager->mkTypeNode( kind::PARAMETRIC_DATATYPE, params ) );
+
+ typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params));
}
Type type(d_nodeManager, typeNode);
DatatypeType dtt(type);
@@ -546,9 +547,9 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
i != i_end;
++i) {
std::string name;
- if( (*i).isSort() ){
+ if( (*i).isSort() ) {
name = SortType(*i).getName();
- }else{
+ } else {
Assert( (*i).isSortConstructor() );
name = SortConstructorType(*i).getName();
}
@@ -562,10 +563,10 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
// unresolved SortType used as a placeholder in complex types)
// with "(*resolver).second" (the DatatypeType we created in the
// first step, above).
- if( (*i).isSort() ){
+ if( (*i).isSort() ) {
placeholders.push_back(*i);
replacements.push_back( (*resolver).second );
- }else{
+ } else {
Assert( (*i).isSortConstructor() );
paramTypes.push_back( SortConstructorType(*i) );
paramReplacements.push_back( (*resolver).second );
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 2bcdcedfa..8320a7053 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -222,7 +222,7 @@ Type::operator DatatypeType() const throw(AssertionException) {
return DatatypeType(*this);
}
-/** Is this the Datatype type? */
+/** Is this a datatype type? */
bool Type::isDatatype() const {
NodeManagerScope nms(d_nodeManager);
return d_typeNode->isDatatype() || d_typeNode->isParametricDatatype();
@@ -388,14 +388,12 @@ string SortType::getName() const {
return d_typeNode->getAttribute(expr::VarNameAttr());
}
-bool SortType::isParameterized() const
-{
+bool SortType::isParameterized() const {
return false;
}
/** Get the parameter types */
-std::vector<Type> SortType::getParamTypes() const
-{
+std::vector<Type> SortType::getParamTypes() const {
vector<Type> params;
return params;
}
@@ -526,11 +524,11 @@ std::vector<Type> ConstructorType::getArgTypes() const {
}
const Datatype& DatatypeType::getDatatype() const {
- if( d_typeNode->isParametricDatatype() ){
- Assert( (*d_typeNode)[0].getKind()==kind::DATATYPE_TYPE );
+ if( d_typeNode->isParametricDatatype() ) {
+ Assert( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE );
const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>();
return dt;
- }else{
+ } else {
return d_typeNode->getConst<Datatype>();
}
}
@@ -544,13 +542,13 @@ size_t DatatypeType::getArity() const {
return d_typeNode->getNumChildren() - 1;
}
-std::vector<Type> DatatypeType::getParamTypes() const{
+std::vector<Type> DatatypeType::getParamTypes() const {
NodeManagerScope nms(d_nodeManager);
vector<Type> params;
vector<TypeNode> paramNodes = d_typeNode->getParamTypes();
vector<TypeNode>::iterator it = paramNodes.begin();
vector<TypeNode>::iterator it_end = paramNodes.end();
- for(; it != it_end; ++ it) {
+ for(; it != it_end; ++it) {
params.push_back(makeType(*it));
}
return params;
diff --git a/src/expr/type.h b/src/expr/type.h
index 096336b0c..4b260185b 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -470,11 +470,12 @@ public:
/** Get the name of the sort */
std::string getName() const;
- /** is parameterized */
+ /** Is this type parameterized? */
bool isParameterized() const;
/** Get the parameter types */
std::vector<Type> getParamTypes() const;
+
};/* class SortType */
/**
@@ -539,7 +540,7 @@ public:
/** Get the underlying datatype */
const Datatype& getDatatype() const;
- /** is parameterized */
+ /** Is this this datatype parametric? */
bool isParametric() const;
/** Get the parameter types */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 9283da13a..f77182d5d 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -138,7 +138,7 @@ std::vector<TypeNode> TypeNode::getArgTypes() const {
std::vector<TypeNode> TypeNode::getParamTypes() const {
vector<TypeNode> params;
- Assert( isParametricDatatype() );
+ Assert(isParametricDatatype());
for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) {
params.push_back((*this)[i]);
}
@@ -194,7 +194,7 @@ bool TypeNode::isDatatype() const {
return getKind() == kind::DATATYPE_TYPE;
}
-/** Is this a datatype type */
+/** Is this a parametric datatype type */
bool TypeNode::isParametricDatatype() const {
return getKind() == kind::PARAMETRIC_DATATYPE;
}
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index d6c685a75..90fee7f1b 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -452,7 +452,8 @@ public:
std::vector<TypeNode> getArgTypes() const;
/**
- * Get the paramater types of a parameterized datatype.
+ * Get the paramater types of a parameterized datatype. Fails an
+ * assertion if this type is not a parametric datatype.
*/
std::vector<TypeNode> getParamTypes() const;
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index efe01fb40..78e70572a 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -242,15 +242,17 @@ SortType Parser::mkUnresolvedType(const std::string& name) {
return unresolved;
}
-SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name,
- size_t arity)
-{
+SortConstructorType
+Parser::mkUnresolvedTypeConstructor(const std::string& name,
+ size_t arity) {
SortConstructorType unresolved = mkSortConstructor(name,arity);
d_unresolved.insert(unresolved);
return unresolved;
}
-SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name,
- const std::vector<Type>& params){
+
+SortConstructorType
+Parser::mkUnresolvedTypeConstructor(const std::string& name,
+ const std::vector<Type>& params) {
Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")"
<< std::endl;
SortConstructorType unresolved = d_exprManager->mkSortConstructor(name, params.size());
@@ -283,10 +285,10 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
if(isDeclared(name, SYM_SORT)) {
throw ParserException(name + " already declared");
}
- if( t.isParametric() ){
+ if( t.isParametric() ) {
std::vector< Type > paramTypes = t.getParamTypes();
defineType(name, paramTypes, t );
- }else{
+ } else {
defineType(name, t);
}
for(Datatype::const_iterator j = dt.begin(),
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 6d55e195e..2e7e3ca3d 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -373,10 +373,15 @@ public:
SortType mkUnresolvedType(const std::string& name);
/**
- * Creates a new "unresolved type," used only during parsing.
+ * Creates a new unresolved (parameterized) type constructor of the given
+ * arity.
*/
SortConstructorType mkUnresolvedTypeConstructor(const std::string& name,
size_t arity);
+ /**
+ * Creates a new unresolved (parameterized) type constructor given the type
+ * parameters.
+ */
SortConstructorType mkUnresolvedTypeConstructor(const std::string& name,
const std::vector<Type>& params);
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index df8cb6eb8..b493b8c41 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -43,7 +43,6 @@ public:
return RewriteResponse(REWRITE_DONE,
NodeManager::currentNM()->mkConst(result));
} else {
- //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
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index d08e3875c..a11990075 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -61,5 +61,13 @@ well-founded PARAMETRIC_DATATYPE\
"DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \
"DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm()" \
"util/datatype.h"
-
+
+parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
+ "type ascription, for nullary, parameteric datatype constructors"
+constant ASCRIPTION_TYPE \
+ ::CVC4::AscriptionType \
+ ::CVC4::AscriptionTypeHashStrategy \
+ "util/ascription_type.h" \
+ "a type parameter for type ascription"
+
endtheory
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index dc2e95f9d..3fe43657f 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -32,8 +32,7 @@ namespace expr {
namespace theory {
namespace datatypes {
-class Matcher
-{
+class Matcher {
private:
std::vector< TypeNode > d_types;
std::vector< TypeNode > d_match;
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 20806464d..5672d1eb2 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -37,6 +37,7 @@ libutil_la_SOURCES = \
configuration_private.h \
configuration.cpp \
bitvector.h \
+ ascription_type.h \
datatype.h \
datatype.cpp \
gmp_util.h \
diff --git a/src/util/ascription_type.h b/src/util/ascription_type.h
new file mode 100644
index 000000000..85a51d8a4
--- /dev/null
+++ b/src/util/ascription_type.h
@@ -0,0 +1,66 @@
+/********************* */
+/*! \file ascription_type.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** 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 ascription
+ **
+ ** A class representing a parameter for the type ascription operator.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__TYPE_ASCRIPTION_H
+#define __CVC4__TYPE_ASCRIPTION_H
+
+#include "expr/type.h"
+
+namespace CVC4 {
+
+/**
+ * A class used to parameterize a type ascription. For example,
+ * "nil :: list<nat>" is an expression of kind APPLY_TYPE_ASCRIPTION.
+ * The parameter is an ASCRIPTION_TYPE-kinded expression with an
+ * AscriptionType payload. (Essentially, all of this is a way to
+ * coerce a Type into the expression tree.)
+ */
+class CVC4_PUBLIC AscriptionType {
+ Type d_type;
+public:
+ AscriptionType(Type t) throw() : d_type(t) {}
+ Type getType() const throw() { return d_type; }
+ bool operator==(const AscriptionType& other) const throw() {
+ return d_type == other.d_type;
+ }
+ bool operator!=(const AscriptionType& other) const throw() {
+ return d_type != other.d_type;
+ }
+};/* class AscriptionType */
+
+/**
+ * A hash strategy for type ascription operators.
+ */
+struct CVC4_PUBLIC AscriptionTypeHashStrategy {
+ static inline size_t hash(const AscriptionType& at) {
+ return TypeHashFunction()(at.getType());
+ }
+};/* struct AscriptionTypeHashStrategy */
+
+/** An output routine for AscriptionTypes */
+inline std::ostream& operator<<(std::ostream& out, AscriptionType at) {
+ out << at.getType();
+ return out;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__TYPE_ASCRIPTION_H */
+
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index ecb089658..31b68c9a4 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -54,15 +54,13 @@ const Datatype& Datatype::datatypeOf(Expr item) {
TypeNode t = Node::fromExpr(item).getType();
switch(t.getKind()) {
case kind::CONSTRUCTOR_TYPE:
- //return t[t.getNumChildren() - 1].getConst<Datatype>();
return DatatypeType(t[t.getNumChildren() - 1].toType()).getDatatype();
case kind::SELECTOR_TYPE:
case kind::TESTER_TYPE:
- //return t[0].getConst<Datatype>();
return DatatypeType(t[0].toType()).getDatatype();
default:
Unhandled("arg must be a datatype constructor, selector, or tester");
- }
+ }
}
size_t Datatype::indexOf(Expr item) {
@@ -84,7 +82,6 @@ void Datatype::resolve(ExprManager* em,
const std::vector< DatatypeType >& paramReplacements)
throw(AssertionException, DatatypeResolutionException) {
- //cout << "resolve " << *this << "..." << std::endl;
AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager");
CheckArgument(!d_resolved, "cannot resolve a Datatype twice");
AssertArgument(resolutions.find(d_name) != resolutions.end(),
@@ -104,8 +101,6 @@ void Datatype::resolve(ExprManager* em,
}
d_self = self;
Assert(index == getNumConstructors());
-
- //cout << "done resolve " << *this << std::endl;
}
void Datatype::addConstructor(const Constructor& c) {
@@ -274,7 +269,8 @@ DatatypeType Datatype::getDatatypeType() const throw(AssertionException) {
return DatatypeType(d_self);
}
-DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params) const throw(AssertionException) {
+DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params)
+ const throw(AssertionException) {
CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
Assert(!d_self.isNull() && DatatypeType(d_self).isParametric());
return DatatypeType(d_self).instantiate(params);
@@ -367,8 +363,6 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self,
const std::vector< DatatypeType >& paramReplacements)
throw(AssertionException, DatatypeResolutionException) {
- //cout << "resolve " << *this << "..." << std::endl;
-
AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager");
CheckArgument(!isResolved(),
"cannot resolve a Datatype constructor twice; "
@@ -401,7 +395,7 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self,
if(!placeholders.empty()) {
range = range.substitute(placeholders, replacements);
}
- if(!paramTypes.empty() ){
+ if(!paramTypes.empty() ) {
range = doParametricSubstitution( range, paramTypes, paramReplacements );
}
(*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, range));
@@ -424,13 +418,11 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self,
for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
(*i).d_constructor = d_constructor;
}
-
- //cout << "done resolve " << *this << std::endl;
}
-Type Datatype::Constructor::doParametricSubstitution( Type range,
- const std::vector< SortConstructorType >& paramTypes,
- const std::vector< DatatypeType >& paramReplacements ){
+Type Datatype::Constructor::doParametricSubstitution( Type range,
+ const std::vector< SortConstructorType >& paramTypes,
+ const std::vector< DatatypeType >& paramReplacements ) {
TypeNode typn = TypeNode::fromType( range );
if(typn.getNumChildren() == 0) {
return range;
@@ -441,16 +433,16 @@ Type Datatype::Constructor::doParametricSubstitution( Type range,
origChildren.push_back( (*i).toType() );
children.push_back( doParametricSubstitution( (*i).toType(), paramTypes, paramReplacements ) );
}
- for( int i=0; i<(int)paramTypes.size(); i++ ){
- if( paramTypes[i].getArity()==origChildren.size() ){
+ for( int i=0; i<(int)paramTypes.size(); i++ ) {
+ if( paramTypes[i].getArity()==origChildren.size() ) {
Type tn = paramTypes[i].instantiate( origChildren );
- if( range==tn ){
+ if( range==tn ) {
return paramReplacements[i].instantiate( children );
}
}
}
NodeBuilder<> nb(typn.getKind());
- for( int i=0; i<(int)children.size(); i++ ){
+ for( int i=0; i<(int)children.size(); i++ ) {
nb << TypeNode::fromType( children[i] );
}
return nb.constructTypeNode().toType();
@@ -662,12 +654,12 @@ Expr Datatype::Constructor::Arg::getSelector() const {
}
Expr Datatype::Constructor::Arg::getConstructor() const {
- CheckArgument(isResolved(), this,
+ CheckArgument(isResolved(), this,
"cannot get a associated constructor for argument of an unresolved datatype constructor");
return d_constructor;
}
-Type Datatype::Constructor::Arg::getSelectorType() const{
+Type Datatype::Constructor::Arg::getSelectorType() const {
return getSelector().getType();
}
diff --git a/src/util/datatype.h b/src/util/datatype.h
index abc9e3258..842be9b45 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -359,11 +359,13 @@ public:
/** Get the name of this Datatype. */
inline std::string getName() const throw();
+
/** Get the number of constructors (so far) for this Datatype. */
inline size_t getNumConstructors() const throw();
/** Get the nubmer of parameters */
inline size_t getNumParameters() const throw();
+
/** Get parameter */
inline Type getParameter( unsigned int i ) const;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback