From: Morgan Deters Date: Sat, 14 May 2011 00:15:43 +0000 (+0000) Subject: add AscriptionType stuff to support nullary parameterized datatypes; also, review... X-Git-Tag: cvc5-1.0.0~8549 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=11bb98ba5b1e9e88053a7bd6adc1d48d48a4bb21;p=cvc5.git add AscriptionType stuff to support nullary parameterized datatypes; also, review of Andy's earlier commit, with some minor code clean-up and documentation --- 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, 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& 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& 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& 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 SortType::getParamTypes() const -{ +std::vector SortType::getParamTypes() const { vector params; return params; } @@ -526,11 +524,11 @@ std::vector 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(); return dt; - }else{ + } else { return d_typeNode->getConst(); } } @@ -544,13 +542,13 @@ size_t DatatypeType::getArity() const { return d_typeNode->getNumChildren() - 1; } -std::vector DatatypeType::getParamTypes() const{ +std::vector DatatypeType::getParamTypes() const { NodeManagerScope nms(d_nodeManager); vector params; vector paramNodes = d_typeNode->getParamTypes(); vector::iterator it = paramNodes.begin(); vector::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 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::getArgTypes() const { std::vector TypeNode::getParamTypes() const { vector 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 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 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& params){ + +SortConstructorType +Parser::mkUnresolvedTypeConstructor(const std::string& name, + const std::vector& 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& 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& 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(); 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" 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(); return DatatypeType(t[t.getNumChildren() - 1].toType()).getDatatype(); case kind::SELECTOR_TYPE: case kind::TESTER_TYPE: - //return t[0].getConst(); 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& params) const throw(AssertionException) { +DatatypeType Datatype::getDatatypeType(const std::vector& 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;