65 open Hints_declaration
83 val divmodZ : Z.z -> Z.z -> (Z.z, Z.z) Types.prod
89 val opAccs_rect_Type4 : 'a1 -> 'a1 -> opAccs -> 'a1
91 val opAccs_rect_Type5 : 'a1 -> 'a1 -> opAccs -> 'a1
93 val opAccs_rect_Type3 : 'a1 -> 'a1 -> opAccs -> 'a1
95 val opAccs_rect_Type2 : 'a1 -> 'a1 -> opAccs -> 'a1
97 val opAccs_rect_Type1 : 'a1 -> 'a1 -> opAccs -> 'a1
99 val opAccs_rect_Type0 : 'a1 -> 'a1 -> opAccs -> 'a1
101 val opAccs_inv_rect_Type4 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
103 val opAccs_inv_rect_Type3 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
105 val opAccs_inv_rect_Type2 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
107 val opAccs_inv_rect_Type1 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
109 val opAccs_inv_rect_Type0 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
111 val opAccs_discr : opAccs -> opAccs -> __
113 val opAccs_jmdiscr : opAccs -> opAccs -> __
120 val op1_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
122 val op1_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
124 val op1_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
126 val op1_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
128 val op1_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
130 val op1_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
132 val op1_inv_rect_Type4 :
133 op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
135 val op1_inv_rect_Type3 :
136 op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
138 val op1_inv_rect_Type2 :
139 op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
141 val op1_inv_rect_Type1 :
142 op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
144 val op1_inv_rect_Type0 :
145 op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
147 val op1_discr : op1 -> op1 -> __
149 val op1_jmdiscr : op1 -> op1 -> __
159 val op2_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
161 val op2_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
163 val op2_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
165 val op2_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
167 val op2_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
169 val op2_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
171 val op2_inv_rect_Type4 :
172 op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
173 'a1) -> (__ -> 'a1) -> 'a1
175 val op2_inv_rect_Type3 :
176 op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
177 'a1) -> (__ -> 'a1) -> 'a1
179 val op2_inv_rect_Type2 :
180 op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
181 'a1) -> (__ -> 'a1) -> 'a1
183 val op2_inv_rect_Type1 :
184 op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
185 'a1) -> (__ -> 'a1) -> 'a1
187 val op2_inv_rect_Type0 :
188 op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
189 'a1) -> (__ -> 'a1) -> 'a1
191 val op2_discr : op2 -> op2 -> __
193 val op2_jmdiscr : op2 -> op2 -> __
195 type eval = { opaccs : (opAccs -> BitVector.byte -> BitVector.byte ->
196 (BitVector.byte, BitVector.byte) Types.prod);
197 op0 : (op1 -> BitVector.byte -> BitVector.byte);
198 op3 : (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte
199 -> (BitVector.byte, BitVector.bit) Types.prod) }
201 val eval_rect_Type4 :
202 ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
203 BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
204 (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
205 (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
207 val eval_rect_Type5 :
208 ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
209 BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
210 (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
211 (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
213 val eval_rect_Type3 :
214 ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
215 BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
216 (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
217 (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
219 val eval_rect_Type2 :
220 ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
221 BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
222 (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
223 (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
225 val eval_rect_Type1 :
226 ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
227 BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
228 (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
229 (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
231 val eval_rect_Type0 :
232 ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
233 BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
234 (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
235 (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
238 eval -> opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
239 BitVector.byte) Types.prod
241 val op0 : eval -> op1 -> BitVector.byte -> BitVector.byte
244 eval -> BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
245 (BitVector.byte, BitVector.bit) Types.prod
247 val eval_inv_rect_Type4 :
248 eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
249 BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
250 (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
251 (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
253 val eval_inv_rect_Type3 :
254 eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
255 BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
256 (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
257 (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
259 val eval_inv_rect_Type2 :
260 eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
261 BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
262 (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
263 (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
265 val eval_inv_rect_Type1 :
266 eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
267 BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
268 (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
269 (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
271 val eval_inv_rect_Type0 :
272 eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
273 BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
274 (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
275 (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
277 val eval_discr : eval -> eval -> __
279 val eval_jmdiscr : eval -> eval -> __
281 val opaccs_implementation :
282 opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
283 BitVector.byte) Types.prod
285 val op1_implementation : op1 -> BitVector.byte -> BitVector.byte
287 val op2_implementation :
288 BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
289 (BitVector.byte, BitVector.bit) Types.prod
294 opAccs -> ByteValues.beval -> ByteValues.beval -> (ByteValues.beval,
295 ByteValues.beval) Types.prod Errors.res
297 val be_op1 : op1 -> ByteValues.beval -> ByteValues.beval Errors.res
300 op2 -> Nat.nat -> BitVector.bit -> BitVector.byte Vector.vector ->
301 BitVector.byte Vector.vector -> (BitVector.byte Vector.vector,
302 BitVector.bit) Types.prod
304 val op_of_add_or_sub : ByteValues.add_or_sub -> op2
306 val be_add_sub_byte :
307 ByteValues.add_or_sub -> ByteValues.bebit -> ByteValues.beval ->
308 BitVector.byte -> (ByteValues.beval, ByteValues.bebit) Types.prod
311 val byte_at : Nat.nat -> BitVector.bitVector -> Nat.nat -> BitVector.byte
314 ('a1 -> 'a1 -> Bool.bool) -> 'a1 Types.option -> 'a1 Types.option ->
318 ByteValues.bebit -> op2 -> ByteValues.beval -> ByteValues.beval ->
319 (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res