1 /********************* */ 2 /*! \file theory_datatypes_type_rules.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Morgan Deters, Tim King 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief Theory of datatypes 13 ** 14 ** Theory of datatypes. 15 **/ 16 17 #include "cvc4_private.h" 18 19 #ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H 20 #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H 21 22 #include "expr/matcher.h" 23 //#include "expr/attribute.h" 24 25 namespace CVC4 { 26 27 namespace expr { 28 namespace attr { 29 struct DatatypeConstructorTypeGroundTermTag {}; 30 } /* CVC4::expr::attr namespace */ 31 } /* CVC4::expr namespace */ 32 33 namespace theory { 34 namespace datatypes { 35 36 typedef expr::Attribute<expr::attr::DatatypeConstructorTypeGroundTermTag, Node> 37 GroundTermAttr; 38 39 struct DatatypeConstructorTypeRule { computeTypeDatatypeConstructorTypeRule40 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, 41 bool check) { 42 Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); 43 TypeNode consType = n.getOperator().getType(check); 44 Type t = consType.getConstructorRangeType().toType(); 45 Assert(t.isDatatype()); 46 DatatypeType dt = DatatypeType(t); 47 TNode::iterator child_it = n.begin(); 48 TNode::iterator child_it_end = n.end(); 49 TypeNode::iterator tchild_it = consType.begin(); 50 if ((dt.isParametric() || check) && 51 n.getNumChildren() != consType.getNumChildren() - 1) { 52 throw TypeCheckingExceptionPrivate( 53 n, "number of arguments does not match the constructor type"); 54 } 55 if (dt.isParametric()) { 56 Debug("typecheck-idt") << "typecheck parameterized datatype " << n 57 << std::endl; 58 Matcher m(dt); 59 for (; child_it != child_it_end; ++child_it, ++tchild_it) { 60 TypeNode childType = (*child_it).getType(check); 61 if (!m.doMatching(*tchild_it, childType)) { 62 throw TypeCheckingExceptionPrivate( 63 n, "matching failed for parameterized constructor"); 64 } 65 } 66 std::vector<Type> instTypes; 67 m.getMatches(instTypes); 68 TypeNode range = TypeNode::fromType(dt.instantiate(instTypes)); 69 Debug("typecheck-idt") << "Return " << range << std::endl; 70 return range; 71 } else { 72 if (check) { 73 Debug("typecheck-idt") << "typecheck cons: " << n << " " 74 << n.getNumChildren() << std::endl; 75 Debug("typecheck-idt") << "cons type: " << consType << " " 76 << consType.getNumChildren() << std::endl; 77 for (; child_it != child_it_end; ++child_it, ++tchild_it) { 78 TypeNode childType = (*child_it).getType(check); 79 Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " 80 << (*tchild_it) << std::endl; 81 TypeNode argumentType = *tchild_it; 82 if (!childType.isSubtypeOf(argumentType)) { 83 std::stringstream ss; 84 ss << "bad type for constructor argument:\n" 85 << "child type: " << childType << "\n" 86 << "not subtype: " << argumentType << "\n" 87 << "in term : " << n; 88 throw TypeCheckingExceptionPrivate(n, ss.str()); 89 } 90 } 91 } 92 return consType.getConstructorRangeType(); 93 } 94 } 95 computeIsConstDatatypeConstructorTypeRule96 inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { 97 Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); 98 NodeManagerScope nms(nodeManager); 99 for (TNode::const_iterator i = n.begin(); i != n.end(); ++i) { 100 if (!(*i).isConst()) { 101 return false; 102 } 103 } 104 //if we support subtyping for tuples, enable this 105 /* 106 //check whether it is in normal form? 107 TypeNode tn = n.getType(); 108 if( tn.isTuple() ){ 109 const Datatype& dt = tn.getDatatype(); 110 //may be the wrong constructor, if children types are subtypes 111 for( unsigned i=0; i<n.getNumChildren(); i++ ){ 112 if( n[i].getType()!=TypeNode::fromType( dt[0][i].getRangeType() ) ){ 113 return false; 114 } 115 } 116 }else if( tn.isCodatatype() ){ 117 //TODO? 118 } 119 */ 120 return true; 121 } 122 }; /* struct DatatypeConstructorTypeRule */ 123 124 struct DatatypeSelectorTypeRule { computeTypeDatatypeSelectorTypeRule125 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, 126 bool check) { 127 Assert(n.getKind() == kind::APPLY_SELECTOR || 128 n.getKind() == kind::APPLY_SELECTOR_TOTAL); 129 TypeNode selType = n.getOperator().getType(check); 130 Type t = selType[0].toType(); 131 Assert(t.isDatatype()); 132 DatatypeType dt = DatatypeType(t); 133 if ((dt.isParametric() || check) && n.getNumChildren() != 1) { 134 throw TypeCheckingExceptionPrivate( 135 n, "number of arguments does not match the selector type"); 136 } 137 if (dt.isParametric()) { 138 Debug("typecheck-idt") << "typecheck parameterized sel: " << n 139 << std::endl; 140 Matcher m(dt); 141 TypeNode childType = n[0].getType(check); 142 if (!childType.isInstantiatedDatatype()) { 143 throw TypeCheckingExceptionPrivate( 144 n, "Datatype type not fully instantiated"); 145 } 146 if (!m.doMatching(selType[0], childType)) { 147 throw TypeCheckingExceptionPrivate( 148 n, 149 "matching failed for selector argument of parameterized datatype"); 150 } 151 std::vector<Type> types, matches; 152 m.getTypes(types); 153 m.getMatches(matches); 154 Type range = selType[1].toType(); 155 range = range.substitute(types, matches); 156 Debug("typecheck-idt") << "Return " << range << std::endl; 157 return TypeNode::fromType(range); 158 } else { 159 if (check) { 160 Debug("typecheck-idt") << "typecheck sel: " << n << std::endl; 161 Debug("typecheck-idt") << "sel type: " << selType << std::endl; 162 TypeNode childType = n[0].getType(check); 163 if (!selType[0].isComparableTo(childType)) { 164 Debug("typecheck-idt") << "ERROR: " << selType[0].getKind() << " " 165 << childType.getKind() << std::endl; 166 throw TypeCheckingExceptionPrivate(n, 167 "bad type for selector argument"); 168 } 169 } 170 return selType[1]; 171 } 172 } 173 }; /* struct DatatypeSelectorTypeRule */ 174 175 struct DatatypeTesterTypeRule { computeTypeDatatypeTesterTypeRule176 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, 177 bool check) { 178 Assert(n.getKind() == kind::APPLY_TESTER); 179 if (check) { 180 if (n.getNumChildren() != 1) { 181 throw TypeCheckingExceptionPrivate( 182 n, "number of arguments does not match the tester type"); 183 } 184 TypeNode testType = n.getOperator().getType(check); 185 TypeNode childType = n[0].getType(check); 186 Type t = testType[0].toType(); 187 Assert(t.isDatatype()); 188 DatatypeType dt = DatatypeType(t); 189 if (dt.isParametric()) { 190 Debug("typecheck-idt") << "typecheck parameterized tester: " << n 191 << std::endl; 192 Matcher m(dt); 193 if (!m.doMatching(testType[0], childType)) { 194 throw TypeCheckingExceptionPrivate( 195 n, 196 "matching failed for tester argument of parameterized datatype"); 197 } 198 } else { 199 Debug("typecheck-idt") << "typecheck test: " << n << std::endl; 200 Debug("typecheck-idt") << "test type: " << testType << std::endl; 201 if (!testType[0].isComparableTo(childType)) { 202 throw TypeCheckingExceptionPrivate(n, "bad type for tester argument"); 203 } 204 } 205 } 206 return nodeManager->booleanType(); 207 } 208 }; /* struct DatatypeTesterTypeRule */ 209 210 struct DatatypeAscriptionTypeRule { computeTypeDatatypeAscriptionTypeRule211 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, 212 bool check) { 213 Debug("typecheck-idt") << "typechecking ascription: " << n << std::endl; 214 Assert(n.getKind() == kind::APPLY_TYPE_ASCRIPTION); 215 TypeNode t = TypeNode::fromType( 216 n.getOperator().getConst<AscriptionType>().getType()); 217 if (check) { 218 TypeNode childType = n[0].getType(check); 219 220 Matcher m; 221 if (childType.getKind() == kind::CONSTRUCTOR_TYPE) { 222 m.addTypesFromDatatype( 223 ConstructorType(childType.toType()).getRangeType()); 224 } else if (childType.getKind() == kind::DATATYPE_TYPE) { 225 m.addTypesFromDatatype(DatatypeType(childType.toType())); 226 } 227 if (!m.doMatching(childType, t)) { 228 throw TypeCheckingExceptionPrivate(n, 229 "matching failed for type " 230 "ascription argument of " 231 "parameterized datatype"); 232 } 233 } 234 return t; 235 } 236 }; /* struct DatatypeAscriptionTypeRule */ 237 238 struct ConstructorProperties { computeCardinalityConstructorProperties239 inline static Cardinality computeCardinality(TypeNode type) { 240 // Constructors aren't exactly functions, they're like 241 // parameterized ground terms. So the cardinality is more like 242 // that of a tuple than that of a function. 243 AssertArgument(type.isConstructor(), type); 244 Cardinality c = 1; 245 for (unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i) { 246 c *= type[i].getCardinality(); 247 } 248 return c; 249 } 250 }; /* struct ConstructorProperties */ 251 252 struct TupleUpdateTypeRule { computeTypeTupleUpdateTypeRule253 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, 254 bool check) { 255 Assert(n.getKind() == kind::TUPLE_UPDATE); 256 const TupleUpdate& tu = n.getOperator().getConst<TupleUpdate>(); 257 TypeNode tupleType = n[0].getType(check); 258 TypeNode newValue = n[1].getType(check); 259 if (check) { 260 if (!tupleType.isTuple()) { 261 throw TypeCheckingExceptionPrivate( 262 n, "Tuple-update expression formed over non-tuple"); 263 } 264 if (tu.getIndex() >= tupleType.getTupleLength()) { 265 std::stringstream ss; 266 ss << "Tuple-update expression index `" << tu.getIndex() 267 << "' is not a valid index; tuple type only has " 268 << tupleType.getTupleLength() << " fields"; 269 throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); 270 } 271 } 272 return tupleType; 273 } 274 }; /* struct TupleUpdateTypeRule */ 275 276 class TupleUpdateOpTypeRule 277 { 278 public: computeType(NodeManager * nodeManager,TNode n,bool check)279 inline static TypeNode computeType(NodeManager* nodeManager, 280 TNode n, 281 bool check) 282 { 283 Assert(n.getKind() == kind::TUPLE_UPDATE_OP); 284 return nodeManager->builtinOperatorType(); 285 } 286 }; /* class TupleUpdateOpTypeRule */ 287 288 struct RecordUpdateTypeRule { computeTypeRecordUpdateTypeRule289 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, 290 bool check) { 291 Assert(n.getKind() == kind::RECORD_UPDATE); 292 NodeManagerScope nms(nodeManager); 293 const RecordUpdate& ru = n.getOperator().getConst<RecordUpdate>(); 294 TypeNode recordType = n[0].getType(check); 295 TypeNode newValue = n[1].getType(check); 296 if (check) { 297 if (!recordType.isRecord()) { 298 throw TypeCheckingExceptionPrivate( 299 n, "Record-update expression formed over non-record"); 300 } 301 const Record& rec = recordType.getRecord(); 302 if (!rec.contains(ru.getField())) { 303 std::stringstream ss; 304 ss << "Record-update field `" << ru.getField() 305 << "' is not a valid field name for the record type"; 306 throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); 307 } 308 } 309 return recordType; 310 } 311 }; /* struct RecordUpdateTypeRule */ 312 313 class RecordUpdateOpTypeRule 314 { 315 public: computeType(NodeManager * nodeManager,TNode n,bool check)316 inline static TypeNode computeType(NodeManager* nodeManager, 317 TNode n, 318 bool check) 319 { 320 Assert(n.getKind() == kind::RECORD_UPDATE_OP); 321 return nodeManager->builtinOperatorType(); 322 } 323 }; /* class RecordUpdateOpTypeRule */ 324 325 class DtSizeTypeRule { 326 public: computeType(NodeManager * nodeManager,TNode n,bool check)327 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, 328 bool check) { 329 if (check) { 330 TypeNode t = n[0].getType(check); 331 if (!t.isDatatype()) { 332 throw TypeCheckingExceptionPrivate( 333 n, "expecting datatype size term to have datatype argument."); 334 } 335 } 336 return nodeManager->integerType(); 337 } 338 }; /* class DtSizeTypeRule */ 339 340 class DtBoundTypeRule { 341 public: computeType(NodeManager * nodeManager,TNode n,bool check)342 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, 343 bool check) { 344 if (check) { 345 TypeNode t = n[0].getType(check); 346 if (!t.isDatatype()) { 347 throw TypeCheckingExceptionPrivate( 348 n, 349 "expecting datatype bound term to have datatype argument."); 350 } 351 if (n[1].getKind() != kind::CONST_RATIONAL) { 352 throw TypeCheckingExceptionPrivate( 353 n, "datatype bound must be a constant"); 354 } 355 if (n[1].getConst<Rational>().getNumerator().sgn() == -1) { 356 throw TypeCheckingExceptionPrivate( 357 n, "datatype bound must be non-negative"); 358 } 359 } 360 return nodeManager->booleanType(); 361 } 362 }; /* class DtBoundTypeRule */ 363 364 class DtSygusBoundTypeRule { 365 public: computeType(NodeManager * nodeManager,TNode n,bool check)366 inline static TypeNode computeType(NodeManager* nodeManager, TNode n, 367 bool check) { 368 if (check) { 369 if (!n[0].getType().isDatatype()) { 370 throw TypeCheckingExceptionPrivate( 371 n, "datatype sygus bound takes a datatype"); 372 } 373 if (n[1].getKind() != kind::CONST_RATIONAL) { 374 throw TypeCheckingExceptionPrivate( 375 n, "datatype sygus bound must be a constant"); 376 } 377 if (n[1].getConst<Rational>().getNumerator().sgn() == -1) { 378 throw TypeCheckingExceptionPrivate( 379 n, "datatype sygus bound must be non-negative"); 380 } 381 } 382 return nodeManager->booleanType(); 383 } 384 }; /* class DtSygusBoundTypeRule */ 385 386 class DtSyguEvalTypeRule 387 { 388 public: computeType(NodeManager * nodeManager,TNode n,bool check)389 inline static TypeNode computeType(NodeManager* nodeManager, 390 TNode n, 391 bool check) 392 { 393 TypeNode headType = n[0].getType(check); 394 if (!headType.isDatatype()) 395 { 396 throw TypeCheckingExceptionPrivate( 397 n, "datatype sygus eval takes a datatype head"); 398 } 399 const Datatype& dt = 400 static_cast<DatatypeType>(headType.toType()).getDatatype(); 401 if (!dt.isSygus()) 402 { 403 throw TypeCheckingExceptionPrivate( 404 n, "datatype sygus eval must have a datatype head that is sygus"); 405 } 406 if (check) 407 { 408 Node svl = Node::fromExpr(dt.getSygusVarList()); 409 if (svl.getNumChildren() + 1 != n.getNumChildren()) 410 { 411 throw TypeCheckingExceptionPrivate(n, 412 "wrong number of arguments to a " 413 "datatype sygus evaluation " 414 "function"); 415 } 416 for (unsigned i = 0, nvars = svl.getNumChildren(); i < nvars; i++) 417 { 418 TypeNode vtype = svl[i].getType(check); 419 TypeNode atype = n[i + 1].getType(check); 420 if (!vtype.isComparableTo(atype)) 421 { 422 throw TypeCheckingExceptionPrivate( 423 n, 424 "argument type mismatch in a datatype sygus evaluation function"); 425 } 426 } 427 } 428 return TypeNode::fromType(dt.getSygusType()); 429 } 430 }; /* class DtSygusBoundTypeRule */ 431 432 } /* CVC4::theory::datatypes namespace */ 433 } /* CVC4::theory namespace */ 434 } /* CVC4 namespace */ 435 436 #endif /* __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H */ 437