Line data Source code
1 : // Author(s): Jeroen Keiren 2 : // Copyright: see the accompanying file COPYING or copy at 3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING 4 : // 5 : // Distributed under the Boost Software License, Version 1.0. 6 : // (See accompanying file LICENSE_1_0.txt or copy at 7 : // http://www.boost.org/LICENSE_1_0.txt) 8 : // 9 : /// \file mcrl2/data/data_expression.h 10 : /// \brief The class data_expression. 11 : 12 : #ifndef MCRL2_DATA_DATA_EXPRESSION_H 13 : #define MCRL2_DATA_DATA_EXPRESSION_H 14 : 15 : #include "mcrl2/data/container_sort.h" 16 : #include "mcrl2/data/function_sort.h" 17 : #include "mcrl2/data/untyped_sort.h" 18 : 19 : namespace mcrl2 20 : { 21 : 22 : namespace data 23 : { 24 : 25 : /// \brief Returns true if the term t is an abstraction 26 91231582 : inline bool is_abstraction(const atermpp::aterm& x) 27 : { 28 91231582 : return x.function() == core::detail::function_symbols::Binder; 29 : } 30 : 31 : /// \brief Returns true if the term t is a lambda abstraction 32 329696 : inline bool is_lambda(const atermpp::aterm_appl& x) 33 : { 34 329696 : return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::Lambda; 35 : } 36 : 37 : /// \brief Returns true if the term t is a universal quantification 38 354593 : inline bool is_forall(const atermpp::aterm_appl& x) 39 : { 40 354593 : return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::Forall; 41 : } 42 : 43 : /// \brief Returns true if the term t is an existential quantification 44 328675 : inline bool is_exists(const atermpp::aterm_appl& x) 45 : { 46 328675 : return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::Exists; 47 : } 48 : 49 : /// \brief Returns true if the term t is a set comprehension 50 320302 : inline bool is_set_comprehension(const atermpp::aterm_appl& x) 51 : { 52 320302 : return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::SetComp; 53 : } 54 : 55 : /// \brief Returns true if the term t is a bag comprehension 56 320274 : inline bool is_bag_comprehension(const atermpp::aterm_appl& x) 57 : { 58 320274 : return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::BagComp; 59 : } 60 : 61 : /// \brief Returns true if the term t is a set/bag comprehension. 62 287096 : inline bool is_untyped_set_or_bag_comprehension(const atermpp::aterm_appl& x) 63 : { 64 287096 : return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::UntypedSetBagComp; 65 : } 66 : 67 : /// \brief Returns true if the term t is a function symbol 68 134152701 : inline bool is_function_symbol(const atermpp::aterm_appl& x) 69 : { 70 134152701 : return x.function() == core::detail::function_symbols::OpId; 71 : } 72 : 73 : /// \brief Returns true if the term t is a variable 74 128147615 : inline bool is_variable(const atermpp::aterm& x) 75 : { 76 128147615 : return x.function() == core::detail::function_symbols::DataVarId; 77 : } 78 : 79 : /// \brief Returns true if the term t is an application 80 : /// \details This function is inefficient as the arity of a term must 81 : /// be determined and an inspection must take place in an 82 : /// array of function symbols. Therefore, there is an more efficient overload 83 : /// is_application(const data_expression& x). 84 5847076 : inline bool is_application(const atermpp::aterm_appl& x) 85 : { 86 5847076 : return core::detail::gsIsDataAppl(x); 87 : } 88 : 89 : /// \brief Returns true if the term t is an application, but it does not check 90 : /// whether an application symbol of sufficient arity exists, assuming 91 : /// this is ok. 92 18824 : inline bool is_application_no_check(const atermpp::aterm_appl& x) 93 : { 94 18824 : return core::detail::gsIsDataAppl_no_check(x); 95 : } 96 : 97 : /// \brief Returns true if the term t is a where clause 98 37623800 : inline bool is_where_clause(const atermpp::aterm_appl& x) 99 : { 100 37623800 : return x.function() == core::detail::function_symbols::Whr; 101 : } 102 : 103 : /// \brief Returns true if the term t is an identifier 104 29392018 : inline bool is_untyped_identifier(const atermpp::aterm_appl& x) 105 : { 106 29392018 : return x.function() == core::detail::function_symbols::UntypedIdentifier; 107 : } 108 : 109 : class application; // prototype 110 : 111 : /// \brief data expression. 112 : /// 113 : /// A data expression can be any of: 114 : /// - variable 115 : /// - function symbol 116 : /// - application 117 : /// - abstraction 118 : /// - where clause 119 : /// - set enumeration 120 : /// - bag enumeration 121 : 122 : //--- start generated class data_expression ---// 123 : /// \\brief A data expression 124 : class data_expression: public atermpp::aterm_appl 125 : { 126 : public: 127 : /// \\brief Default constructor. 128 7867927 : data_expression() 129 7867927 : : atermpp::aterm_appl(core::detail::default_values::DataExpr) 130 7867927 : {} 131 : 132 : /// \\brief Constructor. 133 : /// \\param term A term 134 204385585 : explicit data_expression(const atermpp::aterm& term) 135 204385585 : : atermpp::aterm_appl(term) 136 : { 137 204385585 : assert(core::detail::check_rule_DataExpr(*this)); 138 204385585 : } 139 : 140 : /// Move semantics 141 31700282 : data_expression(const data_expression&) noexcept = default; 142 5473792 : data_expression(data_expression&&) noexcept = default; 143 5825910 : data_expression& operator=(const data_expression&) noexcept = default; 144 442365 : data_expression& operator=(data_expression&&) noexcept = default; 145 : //--- start user section data_expression ---// 146 : /// \brief A function to efficiently determine whether a data expression is 147 : /// made by the default constructor. 148 726474 : bool is_default_data_expression() const 149 : { 150 726474 : return *this==core::detail::default_values::DataExpr; 151 : } 152 : 153 : application operator()(const data_expression& e) const; 154 : 155 : application operator()(const data_expression& e1, 156 : const data_expression& e2) const; 157 : 158 : application operator()(const data_expression& e1, 159 : const data_expression& e2, 160 : const data_expression& e3) const; 161 : 162 : application operator()(const data_expression& e1, 163 : const data_expression& e2, 164 : const data_expression& e3, 165 : const data_expression& e4) const; 166 : 167 : /// \brief Returns the sort of the data expression 168 : 169 : sort_expression sort() const; 170 : 171 : private: 172 : // The following methods are not to be used in a data_expression. 173 : // They are restricted to a data_appl. 174 : const_iterator begin() const; 175 : const_iterator end() const; 176 : 177 : //--- end user section data_expression ---// 178 : }; 179 : 180 : /// \\brief list of data_expressions 181 : typedef atermpp::term_list<data_expression> data_expression_list; 182 : 183 : /// \\brief vector of data_expressions 184 : typedef std::vector<data_expression> data_expression_vector; 185 : 186 : // prototype declaration 187 : std::string pp(const data_expression& x); 188 : 189 : /// \\brief Outputs the object to a stream 190 : /// \\param out An output stream 191 : /// \\param x Object x 192 : /// \\return The output stream 193 : inline 194 2957 : std::ostream& operator<<(std::ostream& out, const data_expression& x) 195 : { 196 2957 : return out << data::pp(x); 197 : } 198 : 199 : /// \\brief swap overload 200 : inline void swap(data_expression& t1, data_expression& t2) 201 : { 202 : t1.swap(t2); 203 : } 204 : //--- end generated class data_expression ---// 205 : 206 : inline void make_data_expression(data_expression& result) 207 : { 208 : static_cast<atermpp::aterm_appl&>(result)=core::detail::default_values::DataExpr; 209 : } 210 : 211 : /// \brief Test for a data_expression expression 212 : /// \param x A term 213 : /// \return True if it is a data_expression expression 214 : inline 215 287077 : bool is_data_expression(const atermpp::aterm_appl& x) 216 : { 217 287077 : return is_lambda(x) || 218 287077 : is_forall(x) || 219 287071 : is_exists(x) || 220 287071 : is_set_comprehension(x) || 221 287071 : is_bag_comprehension(x) || 222 287071 : is_untyped_set_or_bag_comprehension(x) || 223 557722 : is_function_symbol(x) || 224 270651 : is_variable(x) || 225 270184 : is_application(x) || 226 779891 : is_where_clause(x) || 227 492814 : is_untyped_identifier(x); 228 : } 229 : 230 : /// \brief Converts an container with data expressions to data_expression_list 231 : /// \param r A range of data expressions. 232 : /// \note This function uses implementation details of the iterator type 233 : /// and hence is sometimes efficient than copying all elements of the list. 234 : template < typename Container > 235 0 : inline data_expression_list make_data_expression_list(Container const& r, typename atermpp::enable_if_container< Container, data_expression >::type* = nullptr) 236 : { 237 0 : return data_expression_list(r.begin(),r.end()); 238 : } 239 : 240 : class variable; 241 : 242 : // template function overloads 243 : std::string pp(const data_expression_list& x); 244 : std::string pp(const data_expression_vector& x); 245 : data::data_expression translate_user_notation(const data::data_expression& x); 246 : std::set<data::sort_expression> find_sort_expressions(const data::data_expression& x); 247 : std::set<data::variable> find_all_variables(const data::data_expression& x); 248 : std::set<data::variable> find_all_variables(const data::data_expression_list& x); 249 : std::set<data::variable> find_free_variables(const data::data_expression& x); 250 : std::set<data::variable> find_free_variables(const data::data_expression_list& x); 251 : bool search_variable(const data::data_expression& x, const data::variable& v); 252 : 253 : inline 254 2534 : bool is_constant(const data_expression& x) 255 : { 256 2534 : return find_free_variables(x).empty(); 257 : } 258 : 259 : typedef atermpp::term_list<variable> variable_list; 260 : variable_list free_variables(const data_expression& x); 261 : 262 : } // namespace data 263 : 264 : } // namespace mcrl2 265 : 266 : // The trick of including application.h only at this point is needed to break 267 : // the circular dependencies between application and data_expression. This 268 : // dependency was introduced to allow the application operator to be defined for 269 : // all data expression types. 270 : #ifndef MCRL2_DATA_APPLICATION_H 271 : #include "mcrl2/data/application.h" 272 : #endif 273 : 274 : namespace mcrl2 275 : { 276 : namespace data 277 : { 278 : /// \brief Returns true if the term t is an application. 279 : /// \param t The variable that is checked. 280 35016930 : inline bool is_application(const data_expression& t) 281 : { 282 65145626 : return !(is_function_symbol(t) || 283 30128696 : is_variable(t) || 284 26542038 : is_where_clause(t) || 285 26541455 : is_abstraction(t) || 286 61545426 : is_untyped_identifier(t)); 287 : } 288 : 289 : /// \brief Transform a variable_list into a data_expression_list 290 : inline 291 4769 : const data_expression_list& variable_list_to_data_expression_list(const variable_list& l) 292 : { 293 4769 : return atermpp::down_cast<data_expression_list>(static_cast<const atermpp::aterm&>(l)); 294 : } 295 : 296 : /// \brief Apply a data expression to a data expression. 297 : inline 298 3140591 : application data_expression::operator()(const data_expression& e) const 299 : { 300 3140591 : return application(*this, e); 301 : } 302 : 303 : /// \brief Apply data expression to two data expressions 304 : inline 305 4469594 : application data_expression::operator()(const data_expression& e1, const data_expression& e2) const 306 : { 307 4469594 : return application(*this, e1, e2); 308 : } 309 : 310 : /// \brief Apply data expression to three data expressions 311 : inline 312 825045 : application data_expression::operator()(const data_expression& e1, const data_expression& e2, const data_expression& e3) const 313 : { 314 825045 : return application(*this, e1, e2, e3); 315 : } 316 : 317 : /// \brief Apply data expression to four data expressions 318 : inline 319 122892 : application data_expression::operator()(const data_expression& e1, const data_expression& e2, const data_expression& e3, const data_expression& e4) const 320 : { 321 122892 : return application(*this, e1, e2, e3, e4); 322 : } 323 : 324 : } // namespace data 325 : } // namespace mcrl2 326 : 327 : 328 : namespace std 329 : { 330 : 331 : template<> 332 : struct hash<mcrl2::data::data_expression> 333 : { 334 4740 : std::size_t operator()(const mcrl2::data::data_expression& v) const 335 : { 336 : const hash<atermpp::aterm> hasher; 337 4740 : return hasher(v); 338 : } 339 : }; 340 : 341 : } // namespace std 342 : 343 : 344 : 345 : #endif // MCRL2_DATA_DATA_EXPRESSION_H 346 :