mCRL2
Loading...
Searching...
No Matches
jittycpreamble.h
Go to the documentation of this file.
1// Author(s): Muck van Weerdenburg
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//
10
11#ifndef MCRL2_DATA_DETAIL_REWR_JITTYC_PREAMBLE_H
12#define MCRL2_DATA_DETAIL_REWR_JITTYC_PREAMBLE_H
13
14#include "mcrl2/utilities/toolset_version_const.h"
18
19using namespace mcrl2::data::detail;
20using namespace mcrl2::data;
22
23//
24// Declaration of rewriter library interface
25//
26
27extern "C" {
28 MCRL2_EXPORT bool init(rewriter_interface* i, RewriterCompilingJitty* this_rewriter);
29}
30
31// A rewrite_term is a term that may or may not be in normal form. If the method"
32// normal_form is invoked, it will calculate a normal form for itself as efficiently as possible."
33template <class REWRITE_TERM>
34static data_expression& local_rewrite(const REWRITE_TERM& t)
35{
36 return t.normal_form();
37}
38
39template <class REWRITE_TERM>
40static void local_rewrite(data_expression& result, const REWRITE_TERM& t)
41{
42 t.normal_form(result);
43}
44
46{
47 return t;
48}
49
50static void local_rewrite(data_expression& result, const data_expression& t)
51{
52 result=t;
53}
54
55//
56// Forward declarations
57//
58static void set_the_precompiled_rewrite_functions_in_a_lookup_table(RewriterCompilingJitty* this_rewriter);
59
60template <bool ARGUMENTS_IN_NORMAL_FORM>
61static void rewrite_aux(data_expression& result, const data_expression& t, RewriterCompilingJitty* this_rewriter);
62static void rewrite_abstraction_aux(data_expression& result, const abstraction& a, const data_expression& t, RewriterCompilingJitty* this_rewriter);
63
65 data_expression& result,
66 const data_expression& t,
67 RewriterCompilingJitty* this_rewriter)
68{
69 rewrite_aux<true>(result, t, this_rewriter);
70 return;
71}
72
73static data_expression rewrite_with_arguments_in_normal_form(const data_expression& t, RewriterCompilingJitty* this_rewriter)
74{
75 data_expression result; // TODO: Optimize
76 rewrite_aux<true>(result, t, this_rewriter);
77 return result;
78}
79
80static void rewrite(data_expression& result, const data_expression& t, RewriterCompilingJitty* this_rewriter)
81{
82 rewrite_aux<false>(result, t, this_rewriter);
83 return;
84}
85
86//
87// Type definitions
88//
89typedef void(*rewriter_function)(data_expression&, const application&, RewriterCompilingJitty*);
90
91// A class that contains terms which are explicitly tagged to be
92// not in normal form. By invoking normal_form the normalform
93// of this term is calculated.
95{
96 protected:
98 RewriterCompilingJitty* this_rewriter;
99
100 public:
101 term_not_in_normal_form(const data_expression& term, RewriterCompilingJitty* tr)
102 : m_term(term), this_rewriter(tr)
103 {}
104
106 {
107 data_expression& local_store = this_rewriter->m_rewrite_stack.new_stack_position();
108 rewrite_aux<false>(local_store, m_term, this_rewriter);
109 return local_store;
110 }
111
112 void normal_form(data_expression& result) const
113 {
114 rewrite_aux<false>(result, m_term, this_rewriter);
115 }
116};
117
118// This is an abstraction, of which the arguments are not yet
119// in normal form. This is done when the method "normal_form" is invoked.
120template <class TERM_TO_BE_REWRITTEN>
122{
123 protected:
126 const TERM_TO_BE_REWRITTEN& m_body;
127 RewriterCompilingJitty* this_rewriter;
128 public:
129 delayed_abstraction(const binder_type& binding_operator,
130 const variable_list& variables,
131 const TERM_TO_BE_REWRITTEN& body,
132 RewriterCompilingJitty* tr)
133 : m_binding_operator(binding_operator), m_variables(variables), m_body(body), this_rewriter(tr)
134 {}
135
137 {
138 data_expression& t = this_rewriter->m_rewrite_stack.new_stack_position();
140 data_expression& result = this_rewriter->m_rewrite_stack.new_stack_position();
141 rewrite_abstraction_aux(result, atermpp::down_cast<abstraction>(t),t,this_rewriter);
142 return result;
143 }
144
145 void normal_form(data_expression& result) const
146 {
147 local_rewrite(result, m_body); // TODO: HERE m_body is rewritten twice, even if it is in normal form.
149 rewrite_abstraction_aux(result, atermpp::down_cast<abstraction>(result),result,this_rewriter);
150 }
151};
152
153
155{
156 RewriterCompilingJitty* this_rewriter;
157
158 rewrite_functor(RewriterCompilingJitty* tr)
159 : this_rewriter(tr)
160 {}
161
163 {
164 data_expression result;
165 rewrite_aux<false>(result, arg, this_rewriter);
166 return result;
167 }
168};
169
170
171// Miscellaneous helper functions
172//
173static inline
175{
176 result=t;
177}
178
179static inline
181{
182 l.push_front(e);
183 return l;
184}
185
186static inline
187std::size_t get_index(const function_symbol& func)
188{
190}
191
192static inline
193RewriterCompilingJitty::substitution_type& sigma(RewriterCompilingJitty* this_rewriter)
194{
195 return *(this_rewriter->global_sigma);
196}
197
198static inline
199uintptr_t uint_address(const atermpp::aterm& t)
200{
201 return reinterpret_cast<uintptr_t>(atermpp::detail::address(t));
202}
203
204//
205// Rewriting functions
206//
207
208template <bool ARGUMENTS_IN_NORMAL_FORM>
210 const function_symbol& f,
211 const std::size_t arity,
212 RewriterCompilingJitty* this_rewriter)
213{
214 const std::size_t index = get_index(f);
215 if (index>=this_rewriter->index_bound || arity>=this_rewriter->arity_bound)
216 {
217 return nullptr;
218 }
219 if (ARGUMENTS_IN_NORMAL_FORM)
220 {
221 assert(this_rewriter -> arity_bound * index + arity<this_rewriter->functions_when_arguments_are_in_normal_form.size());
222 return this_rewriter->functions_when_arguments_are_in_normal_form[this_rewriter->arity_bound * index + arity];
223 }
224 else
225 {
226 assert(this_rewriter->arity_bound * index + arity<this_rewriter->functions_when_arguments_are_not_in_normal_form.size());
227 return this_rewriter->functions_when_arguments_are_not_in_normal_form[this_rewriter->arity_bound * index + arity];
228 }
229}
230
231static inline
232void rewrite_abstraction_aux(data_expression& result, const abstraction& head, const data_expression& a, RewriterCompilingJitty* this_rewriter)
233{
234 const binder_type& binder(head.binding_operator());
235 if (is_lambda_binder(binder))
236 {
237 this_rewriter->rewrite_lambda_application(result, a, sigma(this_rewriter));
238 assert(result.sort()==a.sort());
239 return;
240 }
241 if (is_exists_binder(binder))
242 {
243 this_rewriter->existential_quantifier_enumeration(result, head, sigma(this_rewriter));
244 assert(result.sort()==a.sort());
245 return;
246 }
247 assert(is_forall_binder(binder));
248 this_rewriter->universal_quantifier_enumeration(result, head, sigma(this_rewriter));
249 assert(result.sort()==a.sort());
250 return;
251}
252
253
254static inline
255void rewrite_appl_aux(data_expression& result, const application& t, RewriterCompilingJitty* this_rewriter)
256{
257 const data_expression& thead=get_nested_head(t);
258 if (is_function_symbol(thead))
259 {
260 const std::size_t arity=recursive_number_of_args(t);
261 const rewriter_function f = get_precompiled_rewrite_function<false>(atermpp::down_cast<function_symbol>(thead),arity,this_rewriter);
262 if (f != nullptr)
263 {
264 f(result, t,this_rewriter);
265 assert(t.sort()==result.sort());
266 return;
267 }
268 make_application(result, t.head(), t.begin(), t.end(), rewrite_functor(this_rewriter));
269 return;
270 }
271 // Here the head symbol of, which can be deeply nested, is not a function_symbol.
272 const data_expression& head0 = get_nested_head(t);
273 data_expression head;
274 if (is_variable(head0))
275 {
276 head=sigma(this_rewriter)(down_cast<const variable>(head0));
277 }
278 else if (is_where_clause(head0))
279 {
280 this_rewriter->rewrite_where(head, atermpp::down_cast<where_clause>(head0), sigma(this_rewriter));
281 }
282 else
283 {
284 head= head0;
285 }
286
287 // Reconstruct term t.
288 const application t1((head0 == head) ? t : replace_nested_head(t, head));
289
290 const data_expression head1(get_nested_head(t1));
291 // Here head1 has the shape
292 // variable, function_symbol, lambda y1,....,ym.u, forall y1,....,ym.u or exists y1,....,ym.u,
293 if (is_variable(head1))
294 {
295 rewrite_all_arguments(result, t1, rewrite_functor(this_rewriter));
296 return;
297 }
298 else
299 if (is_abstraction(head1))
300 {
301 const abstraction& ha=down_cast<abstraction>(head1);
302 rewrite_abstraction_aux(result, ha,t1,this_rewriter);
303 return;
304 }
305 else
306 {
307 assert(is_function_symbol(head1));
308 const std::size_t arity = recursive_number_of_args(t1);
309 const rewriter_function f = get_precompiled_rewrite_function<false>(down_cast<function_symbol>(head1),arity,this_rewriter);
310 if (f != nullptr)
311 {
312 f(result, t1, this_rewriter);
313 assert(t1.sort()==result.sort());
314 return;
315 }
316 make_application(result, head1, t1.begin(), t1.end(), rewrite_functor(this_rewriter));
317 return;
318 }
319}
320
321template <bool ARGUMENTS_IN_NORMAL_FORM>
322static inline
323void rewrite_aux(data_expression& result, const data_expression& t, RewriterCompilingJitty* this_rewriter)
324{
325 if (is_machine_number(t))
326 {
327 result=t;
328 return;
329 }
330 else
331 if (is_function_symbol(t))
332 {
333 const std::size_t index = get_index(down_cast<function_symbol>(t));
334 if (index<this_rewriter->normal_forms_for_constants.size())
335 {
336 // In this case we can use an unprotected_assign as the normal_forms_for_constants will
337 // not change anymore, while rewriting is going on.
338 result.unprotected_assign<false>(this_rewriter->normal_forms_for_constants[index]);
339
340 if (!result.is_default_data_expression())
341 {
342 assert(t.sort()==result.sort());
343 return;
344 }
345 }
346 result=t;
347 return;
348 }
349 else
351 {
352 const application& appl = down_cast<application>(t);
353 const data_expression& head = appl.head();
354 if (is_function_symbol(head))
355 {
356 const std::size_t appl_size=appl.size();
357 const rewriter_function f = get_precompiled_rewrite_function<ARGUMENTS_IN_NORMAL_FORM>(down_cast<function_symbol>(head), appl_size, this_rewriter);
358 if (f != nullptr)
359 {
360 f(result, appl,this_rewriter);
361 assert(result.sort()==t.sort());
362 return;
363 }
364 make_application(result, appl.head(), appl.begin(), appl.end(), rewrite_functor(this_rewriter));
365 return;
366 }
367 else
368 {
369 rewrite_appl_aux(result, appl, this_rewriter);
370 assert(result.sort()==appl.sort());
371 return;
372 }
373 }
374 else
375 if (is_variable(t))
376 {
377 sigma(this_rewriter).apply(down_cast<variable>(t),result,
378 *this_rewriter->m_thread_aterm_pool);
379 return;
380 }
381 else
382 if (is_abstraction(t))
383 {
384 const abstraction& abstr=down_cast<abstraction>(t);
385 const binder_type& binder(abstr.binding_operator());
386 if (is_exists_binder(binder))
387 {
388 this_rewriter->existential_quantifier_enumeration(result, abstr, sigma(this_rewriter));
389 assert(result.sort()==t.sort());
390 return;
391 }
392 if (is_forall_binder(binder))
393 {
394 this_rewriter->universal_quantifier_enumeration(result, abstr, sigma(this_rewriter));
395 assert(result.sort()==t.sort());
396 return;
397 }
398 assert(is_lambda_binder(binder));
399 this_rewriter->rewrite_single_lambda(result, abstr.variables(), abstr.body(), false, sigma(this_rewriter));
400 return;
401 }
402 else
403 {
404 assert(is_where_clause(t));
405 this_rewriter->rewrite_where(result,down_cast<where_clause>(t), sigma(this_rewriter));
406 return;
407 }
408}
409
410static
412{
413}
414
415bool init(rewriter_interface* i, RewriterCompilingJitty* this_rewriter)
416{
417 if (mcrl2::utilities::MCRL2_VERSION != i->caller_toolset_version)
418 {
419 i->status = "rewriter version does not match the version of the calling application.";
420 return false;
421 }
422
423 i->rewrite_external = &rewrite;
424 i->rewrite_cleanup = &rewrite_cleanup;
426 i->status = "rewriter loaded successfully.";
427 return true;
428}
429
430#endif // MCRL2_DATA_DETAIL_REWR_JITTYC_PREAMBLE_H
aterm_core & unprotected_assign(const aterm_core &other) noexcept
Assignment operator, to be used when the busy flags do not need to be set.
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
const TERM_TO_BE_REWRITTEN & m_body
data_expression & normal_form() const
delayed_abstraction(const binder_type &binding_operator, const variable_list &variables, const TERM_TO_BE_REWRITTEN &body, RewriterCompilingJitty *tr)
RewriterCompilingJitty * this_rewriter
const binder_type & m_binding_operator
void normal_form(data_expression &result) const
const variable_list & m_variables
An abstraction expression.
Definition abstraction.h:26
const variable_list & variables() const
Definition abstraction.h:63
const data_expression & body() const
Definition abstraction.h:68
const binder_type & binding_operator() const
Definition abstraction.h:58
An application of a data expression to a number of arguments.
const_iterator end() const
Returns an iterator pointing past the last argument of the application.
const_iterator begin() const
Returns an iterator pointing to the first argument of the application.
const data_expression & head() const
Get the function at the head of this expression.
std::size_t size() const
\brief Assignment of a data expression to a variable
Definition assignment.h:91
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
bool is_default_data_expression() const
A function to efficiently determine whether a data expression is made by the default constructor.
\brief A function symbol
const data_expression & m_term
RewriterCompilingJitty * this_rewriter
void normal_form(data_expression &result) const
data_expression & normal_form() const
term_not_in_normal_form(const data_expression &term, RewriterCompilingJitty *tr)
Defines annotations to force exports.
#define MCRL2_EXPORT
Definition export.h:18
static void rewrite_abstraction_aux(data_expression &result, const abstraction &a, const data_expression &t, RewriterCompilingJitty *this_rewriter)
static void rewrite_with_arguments_in_normal_form(data_expression &result, const data_expression &t, RewriterCompilingJitty *this_rewriter)
void(* rewriter_function)(data_expression &, const application &, RewriterCompilingJitty *)
MCRL2_EXPORT bool init(rewriter_interface *i, RewriterCompilingJitty *this_rewriter)
static void rewrite_appl_aux(data_expression &result, const application &t, RewriterCompilingJitty *this_rewriter)
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
static void set_the_precompiled_rewrite_functions_in_a_lookup_table(RewriterCompilingJitty *this_rewriter)
static void rewrite_cleanup()
static assignment_expression_list jittyc_local_push_front(assignment_expression_list l, const assignment &e)
static void pass_on(data_expression &result, const data_expression &t)
static uintptr_t uint_address(const atermpp::aterm &t)
static void rewrite(data_expression &result, const data_expression &t, RewriterCompilingJitty *this_rewriter)
static std::size_t get_index(const function_symbol &func)
static rewriter_function get_precompiled_rewrite_function(const function_symbol &f, const std::size_t arity, RewriterCompilingJitty *this_rewriter)
static data_expression & local_rewrite(const REWRITE_TERM &t)
static void rewrite_aux(data_expression &result, const data_expression &t, RewriterCompilingJitty *this_rewriter)
@ func
Definition linearise.cpp:77
_aterm * address(const unprotected_aterm_core &t)
Definition aterm_core.h:239
const Derived & down_cast(const Base &t, typename std::enable_if< is_convertible< Base, Derived >::value &&!std::is_base_of< Derived, Base >::value >::type *=nullptr)
A cheap cast from one aterm based type to another When casting one aterm based type into another,...
Definition aterm.h:337
void rewrite_all_arguments(data_expression &result, const application &t, const ARGUMENT_REWRITER rewriter)
std::size_t recursive_number_of_args(const data_expression &t)
const data_expression replace_nested_head(const data_expression &t, const data_expression &head)
const data_expression & get_nested_head(const data_expression &t)
Namespace for all data library functionality.
Definition abstraction.h:22
bool is_application_no_check(const atermpp::aterm &x)
Returns true if the term t is an application, but it does not check whether an application symbol of ...
bool is_where_clause(const atermpp::aterm &x)
Returns true if the term t is a where clause.
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
bool is_exists_binder(const atermpp::aterm &x)
bool is_lambda_binder(const atermpp::aterm &x)
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
void make_abstraction(atermpp::aterm &result, ARGUMENTS... arguments)
Definition abstraction.h:75
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
bool is_forall_binder(const atermpp::aterm &x)
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
void make_application(atermpp::aterm &result)
Make function for an application.
static std::size_t index(const Variable &x)
Returns the index of the variable.
data_expression operator()(const data_expression &arg) const
RewriterCompilingJitty * this_rewriter
rewrite_functor(RewriterCompilingJitty *tr)