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