1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* A class representing a type matcher. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__EXPR__TYPE_MATCHER_H |
19 |
|
#define CVC5__EXPR__TYPE_MATCHER_H |
20 |
|
|
21 |
|
#include <vector> |
22 |
|
|
23 |
|
#include "expr/type_node.h" |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
|
27 |
|
/** |
28 |
|
* This class is used for inferring the parameters of an instantiated |
29 |
|
* parametric datatype. For example, given parameteric datatype: |
30 |
|
* (par (T) (List T)) |
31 |
|
* and instantiated parametric datatype (List Int), this class is used to |
32 |
|
* infer the mapping { T -> Int }. |
33 |
|
*/ |
34 |
|
class TypeMatcher |
35 |
|
{ |
36 |
|
public: |
37 |
104 |
TypeMatcher() {} |
38 |
|
/** Initialize this class to do matching with datatype type dt */ |
39 |
|
TypeMatcher(TypeNode dt); |
40 |
1910 |
~TypeMatcher() {} |
41 |
|
/** |
42 |
|
* Add the parameter types from datatype type dt to the above vectors, |
43 |
|
* initializing d_match to null. |
44 |
|
*/ |
45 |
|
void addTypesFromDatatype(TypeNode dt); |
46 |
|
/** |
47 |
|
* Do matching on type pattern and tn. |
48 |
|
* If this method returns true, then tn is an instantiation of parametric |
49 |
|
* datatype pattern. The parameters of tn that were inferred are stored in |
50 |
|
* d_match such that pattern * { d_types -> d_match } = tn. |
51 |
|
*/ |
52 |
|
bool doMatching(TypeNode pattern, TypeNode tn); |
53 |
|
|
54 |
|
/** Get the parameter types that this class matched on */ |
55 |
|
void getTypes(std::vector<TypeNode>& types) const; |
56 |
|
/** |
57 |
|
* Get the match for the parameter types based on the last call to doMatching. |
58 |
|
*/ |
59 |
|
void getMatches(std::vector<TypeNode>& types) const; |
60 |
|
|
61 |
|
private: |
62 |
|
/** The parameter types */ |
63 |
|
std::vector<TypeNode> d_types; |
64 |
|
/** The types they matched */ |
65 |
|
std::vector<TypeNode> d_match; |
66 |
|
/** Add a parameter type to the above vectors */ |
67 |
|
void addType(TypeNode t); |
68 |
|
/** Add parameter types to the above vectors */ |
69 |
|
void addTypes(const std::vector<TypeNode>& types); |
70 |
|
}; /* class TypeMatcher */ |
71 |
|
|
72 |
|
} // namespace cvc5 |
73 |
|
|
74 |
|
#endif /* CVC5__MATCHER_H */ |