1 
2 /*
3  * File Reflection.hpp.
4  *
5  * This file is part of the source code of the software program
6  * Vampire. It is protected by applicable
7  * copyright laws.
8  *
9  * This source code is distributed under the licence found here
10  * https://vprover.github.io/license.html
11  * and in the source directory
12  *
13  * In summary, you are allowed to use Vampire for non-commercial
14  * purposes but not allowed to distribute, modify, copy, create derivatives,
15  * or use in competitions.
16  * For other uses of Vampire please contact developers for a different
17  * licence, which we will make an effort to provide.
18  */
19 /**
20  * @file Reflection.hpp
21  * Defines class Reflection.
22  */
23 
24 
25 #ifndef __Reflection__
26 #define __Reflection__
27 
28 ///@addtogroup Reflection
29 ///@{
30 
31 
32 //The obvious way to define this macro would be
33 //#define DECL_ELEMENT_TYPE(T) typedef T _ElementType
34 //but the preprocessor understands for example
35 //M(pair<A,B>)
36 //as an instantiation of  macro M with two arguments --
37 //pair<A is first and B> second.
38 
39 /**
40  * Declare type returned by an iterator
41  *
42  * To be used inside a public block of a class declaration
43  *
44  * There is no need to use this macro in a descendant of the
45  * @b IteratorCore class, as this class already contains this
46  * declaration.
47  *
48  * Although the macro formally takes variable number of arguments, it
49  * should be used only with a single argument. The variable number
50  * of formal arguments is to allow for the use of template types,
51  * such as pair<int,int>, since the preprocessor considers every
52  * comma as an argument separator.
53  */
54 #define DECL_ELEMENT_TYPE(...) typedef __VA_ARGS__ _ElementType
55 
56 /**
57  * Type of elements in the iterator/collection @b Cl
58  *
59  * The class @b Cl must have its element type declared by the
60  * @b DECL_ELEMENT_TYPE macro in order for this macro to be applicable
61  * (Except for cases that are handled by a partial specialization
62  * of the @b Lib::ElementTypeInfo template class.)
63  *
64  * @see DECL_ELEMENT_TYPE, Lib::ElementTypeInfo
65  */
66 #define ELEMENT_TYPE(Cl) typename Lib::ElementTypeInfo<Cl>::Type
67 
68 /**
69  * Type of elements of the current class
70  *
71  * The current class must have its element type declared by the
72  * @b DECL_ELEMENT_TYPE macro in order for this macro to be applicable
73  *
74  * @see DECL_ELEMENT_TYPE
75  */
76 #define OWN_ELEMENT_TYPE _ElementType
77 
78 /**
79  * Declare type returned by a functor class
80  *
81  * To be used inside a public block of declaration of a functor class.
82  *
83  * A functor class is a class with @b operator() defined, so that its
84  * objects can be called as functions. The return type to be declared
85  * by this macro is the return type of this operator.
86  *
87  * Although the macro formally takes variable number of arguments, it
88  * should be used only with a single argument. The variable number
89  * of formal arguments is to allow for the use of template types,
90  * such as pair<int,int>, since the preprocessor considers every
91  * comma as an argument separator.
92  */
93 #define DECL_RETURN_TYPE(...) typedef __VA_ARGS__ _ReturnType
94 
95 /**
96  * Return type of the functor class @b Cl
97  *
98  * The class @b Cl must have its return type declared by the
99  * @b DECL_RETURN_TYPE macro in order for this macro to be applicable
100  *
101  * @see DECL_RETURN_TYPE
102  */
103 #define RETURN_TYPE(Cl) typename Cl::_ReturnType
104 
105 /**
106  * Return type of the current functor class
107  *
108  * The current class must have its return type declared by the
109  * @b DECL_RETURN_TYPE macro in order for this macro to be applicable
110  *
111  * @see DECL_RETURN_TYPE
112  */
113 #define OWN_RETURN_TYPE _ReturnType
114 
115 
116 /**
117  * Declare the iterator type for a container class
118  *
119  * To be used inside a public block of declaration of a container class.
120  *
121  * An iterator type is a class with a constructor that takes (a reference
122  * to) an instance of the container class, and then provides functions
123  * @b hasNext() and @b next() to iterate through elements of the
124  * container.
125  *
126  * Although the macro formally takes variable number of arguments, it
127  * should be used only with a single argument. The variable number
128  * of formal arguments is to allow for the use of template types,
129  * such as pair<int,int>, since the preprocessor considers every
130  * comma as an argument separator.
131  */
132 #define DECL_ITERATOR_TYPE(...) typedef __VA_ARGS__ _IteratorType
133 
134 /**
135  * Return iterator type of the container class @b Cl
136  *
137  * An iterator type is a class with a constructor that takes (a reference
138  * to) an instance of the container class, and then provides functions
139  * @b hasNext() and @b next() to iterate through elements of the
140  * container.
141  *
142  * The class @b Cl must have its iterator type declared by the
143  * @b DECL_ITERATOR_TYPE macro in order for this macro to be applicable.
144  * (Except for cases that are handled by a partial specialization
145  * of the @b Lib::IteratorTypeInfo template class.)
146  *
147  * @see DECL_ITERATOR_TYPE, Lib::IteratorTypeInfo
148  */
149 #define ITERATOR_TYPE(Cl) typename Lib::IteratorTypeInfo<Cl>::Type
150 
151 /**
152  * Iterator type of the current container class
153  *
154  * An iterator type is a class with a constructor that takes (a reference
155  * to) an instance of the container class, and then provides functions
156  * @b hasNext() and @b next() to iterate through elements of the
157  * container.
158  *
159  * The current class must have its iterator type declared by the
160  * @b DECL_ITERATOR_TYPE macro in order for this macro to be applicable
161  *
162  * @see DECL_ITERATOR_TYPE
163  */
164 #define OWN_ITERATOR_TYPE _IteratorType
165 
166 namespace Lib {
167 
168 /**
169  * A helper class that is used by the @b ELEMENT_TYPE macro to obtain
170  * element types in iterator and container types
171  *
172  * The default implementation uses the @b _ElementType typedef which
173  * is being declared by the @b DECL_ELEMENT_TYPE macro inside a class.
174  *
175  * If the use of the @b DECL_ELEMENT_TYPE macro is not suitable for some
176  * type, the same effect can be achieved by a partial specialization of
177  * this class that contains a typedef of the appropriate element type
178  * to a new type @b Type. An example of this can be @b ElementTypeInfo<T[]>
179  * which is this kin of specialisation for arrays.
180  *
181  * @see ELEMENT_TYPE, DECL_ELEMENT_TYPE
182  */
183 template<typename T>
184 struct ElementTypeInfo
185 {
186   typedef typename T::_ElementType Type;
187 };
188 
189 /**
190  * ElementTypeInfo for arrays.
191  *
192  * @see ElementTypeInfo
193  */
194 template<typename T>
195 struct ElementTypeInfo<T[]>
196 {
197   typedef T Type;
198 };
199 
200 /**
201  * ElementTypeInfo for pointers
202  *
203  * @see ElementTypeInfo
204  */
205 template<typename T>
206 struct ElementTypeInfo<T*>
207 {
208   typedef T Type;
209 };
210 
211 /**
212  * A helper class that is used by the @b ITERATOR_TYPE macro to obtain
213  * iterator types for container classes
214  *
215  * The default implementation uses the @b _IteratorType typedef which
216  * is being declared by the @b DECL_ITERATOR_TYPE macro inside a class.
217  *
218  * If the use of the @b DECL_ITERATOR_TYPE macro is not suitable for some
219  * type, the same effect can be achieved by a partial specialization of
220  * this class that contains a typedef of the appropriate element type
221  * to a new type @b Type. An example of this can be @b IteratorTypeInfo<List<T>*>
222  * in the List.hpp file which is this kind of specialisation for lists.
223  *
224  * @see ITERATOR_TYPE, DECL_ITERATOR_TYPE
225  */
226 template<typename T>
227 struct IteratorTypeInfo
228 {
229   typedef typename T::_IteratorType Type;
230 };
231 
232 /**
233  * IteratorTypeInfo for const types
234  *
235  * @see IteratorTypeInfo
236  */
237 template<typename T>
238 struct IteratorTypeInfo<T const>
239 {
240   typedef typename IteratorTypeInfo<T>::Type Type;
241 };
242 
243 
244 };
245 
246 ///@}�
247 
248 #endif /* __Reflection__ */
249