diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-06-03 05:30:54 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-06-03 05:30:54 +0000 |
commit | 4a696409769044ad155a56eeb00c9d85246ca0b4 (patch) | |
tree | 27a131cb40138049508150fc5aa2c0330b52f704 /src/util | |
parent | d935021323ca343da5359fa54bc62184d47ccd1b (diff) |
datatypes work
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 1 | ||||
-rw-r--r-- | src/util/datatype.cpp | 21 | ||||
-rw-r--r-- | src/util/datatype.h | 28 | ||||
-rw-r--r-- | src/util/matcher.h | 110 |
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 */ |