From 471352e0956d1e9e1f0636933e792ed8650d5526 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 1 Jun 2011 00:49:37 +0000 Subject: [PATCH] type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT] --- src/expr/node_manager.cpp | 5 +- src/expr/type.cpp | 8 +++ src/expr/type.h | 15 ++++- src/expr/type_node.cpp | 26 +++++++++ src/expr/type_node.h | 6 ++ src/parser/cvc/Cvc.g | 23 ++++---- .../datatypes/theory_datatypes_type_rules.h | 56 +++++++++++++++++-- src/util/ascription_type.h | 7 +-- src/util/datatype.h | 2 +- 9 files changed, 122 insertions(+), 26 deletions(-) diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 716e2a3b3..4cde0c624 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -238,7 +238,7 @@ void NodeManager::reclaimZombies() { }/* NodeManager::reclaimZombies() */ TypeNode NodeManager::computeType(TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode typeNode; // Infer the type @@ -444,6 +444,9 @@ TypeNode NodeManager::computeType(TNode n, bool check) case kind::APPLY_TESTER: typeNode = CVC4::theory::datatypes::DatatypeTesterTypeRule::computeType(this, n, check); break; + case kind::APPLY_TYPE_ASCRIPTION: + typeNode = CVC4::theory::datatypes::DatatypeAscriptionTypeRule::computeType(this, n, check); + break; default: Debug("getType") << "FAILURE" << std::endl; Unhandled(n.getKind()); diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 8320a7053..077fc5ee2 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -537,6 +537,14 @@ bool DatatypeType::isParametric() const { return d_typeNode->isParametricDatatype(); } +bool DatatypeType::isInstantiated() const { + return d_typeNode->isInstantiatedDatatype(); +} + +bool DatatypeType::isParameterInstantiated(unsigned n) const { + return d_typeNode->isParameterInstantiatedDatatype(n); +} + size_t DatatypeType::getArity() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->getNumChildren() - 1; diff --git a/src/expr/type.h b/src/expr/type.h index 4b260185b..14ca3baf3 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -540,9 +540,22 @@ public: /** Get the underlying datatype */ const Datatype& getDatatype() const; - /** Is this this datatype parametric? */ + /** Is this datatype parametric? */ bool isParametric() const; + /** + * Has this datatype been fully instantiated ? + * + * @return true if this datatype is not parametric or, if it is, it + * has been fully instantiated + */ + bool isInstantiated() const; + + /** + * Has this datatype been instantiated for parameter N ? + */ + bool isParameterInstantiated(unsigned n) const; + /** Get the parameter types */ std::vector getParamTypes() const; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index f77182d5d..7376b0080 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -199,6 +199,32 @@ bool TypeNode::isParametricDatatype() const { return getKind() == kind::PARAMETRIC_DATATYPE; } +/** Is this an instantiated datatype type */ +bool TypeNode::isInstantiatedDatatype() const { + if(getKind() == kind::DATATYPE_TYPE) { + return true; + } + if(getKind() != kind::PARAMETRIC_DATATYPE) { + return false; + } + const Datatype& dt = (*this)[0].getConst(); + unsigned n = dt.getNumParameters(); + for(unsigned i = 0; i < n; ++i) { + if(TypeNode::fromType(dt.getParameter(i)) == (*this)[n + 1]) { + return false; + } + } + return true; +} + +/** Is this an instantiated datatype parameter */ +bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const { + AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this); + const Datatype& dt = (*this)[0].getConst(); + AssertArgument(n < dt.getNumParameters(), *this); + return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1]; +} + /** Is this a constructor type */ bool TypeNode::isConstructor() const { return getKind() == kind::CONSTRUCTOR_TYPE; diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 90fee7f1b..0f4b122db 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -488,6 +488,12 @@ public: /** Is this a parameterized datatype type */ bool isParametricDatatype() const; + /** Is this a fully instantiated datatype type */ + bool isInstantiatedDatatype() const; + + /** Is this an instantiated datatype parameter */ + bool isParameterInstantiatedDatatype(unsigned n) const; + /** Is this a constructor type */ bool isConstructor() const; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 3c8d6e1ce..ca006daab 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1461,9 +1461,16 @@ postfixTerm[CVC4::Expr& f] f = EXPR_MANAGER->mkVar(TupleType(f.getType()).getTypes()[k]); } )*/ )* - (typeAscription[f, t] - { //f = MK_EXPR(CVC4::kind::APPLY_TYPE_ANNOTATION, MK_CONST(t), f); - } )? + ( typeAscription[f, t] + { if(t.isDatatype()) { + f = MK_EXPR(CVC4::kind::APPLY_TYPE_ASCRIPTION, MK_CONST(AscriptionType(t)), f); + } else { + if(f.getType() != t) { + PARSER_STATE->parseError("Type ascription not satisfied."); + } + } + } + )? ; bvTerm[CVC4::Expr& f] @@ -1666,16 +1673,6 @@ typeAscription[const CVC4::Expr& f, CVC4::Type& t] @init { } : COLON COLON type[t,CHECK_DECLARED] - { //if(f.getType() != t) { - // std::stringstream ss; - // ss << Expr::setlanguage(language::output::LANG_CVC4) - // << "type ascription not satisfied\n" - // << "term: " << f << '\n' - // << "has type: " << f.getType() << '\n' - // << "ascribed: " << t; - // PARSER_STATE->parseError(ss.str()); - //} - } ; /** diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 3fe43657f..c9c76a15b 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -41,6 +41,13 @@ public: 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(){} @@ -55,9 +62,11 @@ public: } 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{ @@ -79,20 +88,23 @@ public: } TypeNode getMatch( unsigned int i ){ return d_match[i]; } - void getTypes( std::vector& types ) { + void getTypes( std::vector& types ) { types.clear(); for( int i=0; i<(int)d_match.size(); i++ ){ types.push_back( d_types[i].toType() ); } } - void getMatches( std::vector& types ) { + void getMatches( std::vector& types ) { types.clear(); for( int i=0; i<(int)d_match.size(); i++ ){ - Assert( !d_match[i].isNull() ); //verify that all types have been set - types.push_back( d_match[i].toType() ); + 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 GroundTermAttr; @@ -157,6 +169,9 @@ struct DatatypeSelectorTypeRule { Debug("typecheck-idt") << "typecheck parameterized sel: " << n << std::endl; Matcher m( dt ); TypeNode childType = n[0].getType(check); + if(! childType.isInstantiatedDatatype()) { + throw TypeCheckingExceptionPrivate(n, "Datatype type not fully instantiated"); + } if( !m.doMatching( selType[0], childType ) ){ throw TypeCheckingExceptionPrivate(n, "matching failed for selector argument of parameterized datatype"); } @@ -211,7 +226,36 @@ struct DatatypeTesterTypeRule { } return nodeManager->booleanType(); } -};/* struct DatatypeSelectorTypeRule */ +};/* struct DatatypeTesterTypeRule */ + +struct DatatypeAscriptionTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + Debug("typecheck-idt") << "typechecking ascription: " << n << std::endl; + Assert(n.getKind() == kind::APPLY_TYPE_ASCRIPTION); + TypeNode t = TypeNode::fromType(n.getOperator().getConst().getType()); + if(check) { + TypeNode childType = n[0].getType(check); + if(!t.getKind() == kind::DATATYPE_TYPE) { + throw TypeCheckingExceptionPrivate(n, "bad type for datatype type ascription"); + } + DatatypeType dt = DatatypeType(childType.toType()); + if( dt.isParametric() ){ + Debug("typecheck-idt") << "typecheck parameterized ascription: " << n << std::endl; + Matcher m( dt ); + if( !m.doMatching( childType, t ) ){ + throw TypeCheckingExceptionPrivate(n, "matching failed for type ascription argument of parameterized datatype"); + } + }else{ + Debug("typecheck-idt") << "typecheck test: " << n << std::endl; + if(t != childType) { + throw TypeCheckingExceptionPrivate(n, "bad type for type ascription argument"); + } + } + } + return t; + } +};/* struct DatatypeAscriptionTypeRule */ struct ConstructorProperties { inline static Cardinality computeCardinality(TypeNode type) { diff --git a/src/util/ascription_type.h b/src/util/ascription_type.h index 85a51d8a4..81289572c 100644 --- a/src/util/ascription_type.h +++ b/src/util/ascription_type.h @@ -18,8 +18,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__TYPE_ASCRIPTION_H -#define __CVC4__TYPE_ASCRIPTION_H +#ifndef __CVC4__ASCRIPTION_TYPE_H +#define __CVC4__ASCRIPTION_TYPE_H #include "expr/type.h" @@ -62,5 +62,4 @@ inline std::ostream& operator<<(std::ostream& out, AscriptionType at) { }/* CVC4 namespace */ -#endif /* __CVC4__TYPE_ASCRIPTION_H */ - +#endif /* __CVC4__ASCRIPTION_TYPE_H */ diff --git a/src/util/datatype.h b/src/util/datatype.h index 6aeb93bcf..90dd8775f 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -369,7 +369,7 @@ public: /** Get the number of constructors (so far) for this Datatype. */ inline size_t getNumConstructors() const throw(); - /** Get the nubmer of parameters */ + /** Get the nubmer of type parameters */ inline size_t getNumParameters() const throw(); /** Get parameter */ -- 2.30.2