20 #ifndef SEC_JCB_IMPL_H 21 #define SEC_JCB_IMPL_H 23 #ifndef SHEAF_DLL_SPEC_H 24 #include "SheafSystem/sheaf_dll_spec.h" 27 #ifndef ASSERT_CONTRACT_H 28 #include "SheafSystem/assert_contract.h" 32 #include "SheafSystem/sec_jcb.h" 45 template <
typename VJCB,
typename VCOVECTOR,
typename VR>
47 pull_functor<VJCB, VCOVECTOR, VR>::
48 operator()(
const VJCB& xjcb,
const VCOVECTOR& xcovector, VR& xresult)
52 require(precondition_of(
pull(xjcb, xcovector, xresult)));
56 pull(xjcb, xcovector, xresult);
60 ensure(postcondition_of(
pull(xjcb, xcovector, xresult)));
68 template <
typename VJCB,
typename VVECTOR,
typename VR>
70 push_functor<VJCB, VVECTOR, VR>::
71 operator()(
const VJCB& xjcb,
const VVECTOR& xvector, VR& xresult)
75 require(precondition_of(
push(xjcb, xvector, xresult)));
79 push(xjcb, xvector, xresult);
83 ensure(postcondition_of(
push(xjcb, xvector, xresult)));
94 template <
typename SJCB,
typename SCOVECTOR,
typename SR>
95 void pull(
const SJCB& xjcb,
const SCOVECTOR& xcovector, SR& xresult,
100 require(xjcb.state_is_auto_read_accessible(xauto_access));
101 require(xcovector.state_is_auto_read_accessible(xauto_access));
102 require(xresult.state_is_auto_read_write_accessible(xauto_access));
103 require(xcovector.is_p_form(xauto_access));
109 xjcb.get_read_access();
110 xcovector.get_read_access();
111 xresult.get_read_write_access(
true);
114 typedef typename SJCB::fiber_type::volatile_type VJCB;
115 typedef typename SCOVECTOR::fiber_type::volatile_type VCOVECTOR;
116 typedef typename SR::fiber_type::volatile_type VR;
117 pull_functor<VJCB, VCOVECTOR, VR> f;
118 binary_op(xjcb, xcovector, xresult, f, xauto_access);
122 xresult.put_is_p_form(
false);
127 xjcb.release_access();
128 xcovector.release_access();
129 xresult.release_access();
134 ensure(xresult.is_p_form(xauto_access));
142 template <
typename SJCB,
typename SVECTOR,
typename SR>
143 void push(
const SJCB& xjcb,
const SVECTOR& xvector, SR& xresult,
148 require(xjcb.state_is_auto_read_accessible(xauto_access));
149 require(xvector.state_is_auto_read_accessible(xauto_access));
150 require(xresult.state_is_auto_read_write_accessible(xauto_access));
151 require(xvector.is_p_vector(xauto_access));
157 xjcb.get_read_access();
158 xvector.get_read_access();
159 xresult.get_read_write_access(
true);
162 typedef typename SJCB::fiber_type::volatile_type VJCB;
163 typedef typename SVECTOR::fiber_type::volatile_type VVECTOR;
164 typedef typename SR::fiber_type::volatile_type VR;
165 push_functor<VJCB, VVECTOR, VR> f;
166 binary_op(xjcb, xvector, xresult, f, xauto_access);
170 xresult.put_is_p_vector(
false);
174 xjcb.release_access();
175 xvector.release_access();
176 xresult.release_access();
181 ensure(xresult.is_p_vector(xauto_access));
190 #endif // ifndef SEC_JCB_IMPL_H void pull(const SJCB &xjcb, const SCOVECTOR &xcovector, SR &xresult, bool xauto_access)
void push(const SJCB &xjcb, const SVECTOR &xvector, SR &xresult, bool xauto_access)
void binary_op(const S0 &x0, const S1 &x1, SR &xresult, F xfunctor, bool xauto_access)
Binary operator.
Namespace for the fiber_bundles component of the sheaf system.