119 open Hints_declaration
150 PreIdentifiers.identifier -> ByteValues.beval -> ByteValues.beval
151 Identifiers.identifier_map -> ByteValues.beval Identifiers.identifier_map
154 ByteValues.beval Registers.register_env -> Registers.register ->
155 ByteValues.beval Errors.res
157 type hw_register_env = { reg_env : ByteValues.beval
158 BitVectorTrie.bitVectorTrie;
159 other_bit : ByteValues.bebit }
161 val hw_register_env_rect_Type4 :
162 (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
163 -> hw_register_env -> 'a1
165 val hw_register_env_rect_Type5 :
166 (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
167 -> hw_register_env -> 'a1
169 val hw_register_env_rect_Type3 :
170 (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
171 -> hw_register_env -> 'a1
173 val hw_register_env_rect_Type2 :
174 (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
175 -> hw_register_env -> 'a1
177 val hw_register_env_rect_Type1 :
178 (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
179 -> hw_register_env -> 'a1
181 val hw_register_env_rect_Type0 :
182 (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
183 -> hw_register_env -> 'a1
185 val reg_env : hw_register_env -> ByteValues.beval BitVectorTrie.bitVectorTrie
187 val other_bit : hw_register_env -> ByteValues.bebit
189 val hw_register_env_inv_rect_Type4 :
190 hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
191 ByteValues.bebit -> __ -> 'a1) -> 'a1
193 val hw_register_env_inv_rect_Type3 :
194 hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
195 ByteValues.bebit -> __ -> 'a1) -> 'a1
197 val hw_register_env_inv_rect_Type2 :
198 hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
199 ByteValues.bebit -> __ -> 'a1) -> 'a1
201 val hw_register_env_inv_rect_Type1 :
202 hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
203 ByteValues.bebit -> __ -> 'a1) -> 'a1
205 val hw_register_env_inv_rect_Type0 :
206 hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
207 ByteValues.bebit -> __ -> 'a1) -> 'a1
209 val hw_register_env_discr : hw_register_env -> hw_register_env -> __
211 val hw_register_env_jmdiscr : hw_register_env -> hw_register_env -> __
213 val hwreg_retrieve : hw_register_env -> I8051.register -> ByteValues.beval
216 I8051.register -> ByteValues.beval -> hw_register_env -> hw_register_env
218 val hwreg_set_other : ByteValues.bebit -> hw_register_env -> hw_register_env
220 val hwreg_retrieve_sp : hw_register_env -> ByteValues.xpointer Errors.res
223 hw_register_env -> ByteValues.xpointer -> hw_register_env
225 val init_hw_register_env : ByteValues.xpointer -> hw_register_env
227 type sem_graph_params = { sgp_pars : Joint.uns_params;
229 Joint_semantics.sem_unserialized_params);
230 graph_pre_main_generator : (Joint.joint_program ->
231 Joint.joint_closed_internal_function) }
233 val sem_graph_params_rect_Type4 :
234 (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
235 (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
236 sem_graph_params -> 'a1
238 val sem_graph_params_rect_Type5 :
239 (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
240 (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
241 sem_graph_params -> 'a1
243 val sem_graph_params_rect_Type3 :
244 (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
245 (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
246 sem_graph_params -> 'a1
248 val sem_graph_params_rect_Type2 :
249 (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
250 (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
251 sem_graph_params -> 'a1
253 val sem_graph_params_rect_Type1 :
254 (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
255 (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
256 sem_graph_params -> 'a1
258 val sem_graph_params_rect_Type0 :
259 (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
260 (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
261 sem_graph_params -> 'a1
263 val sgp_pars : sem_graph_params -> Joint.uns_params
266 sem_graph_params -> 'a1 Joint_semantics.sem_unserialized_params
268 val graph_pre_main_generator :
269 sem_graph_params -> Joint.joint_program ->
270 Joint.joint_closed_internal_function
272 val sem_graph_params_inv_rect_Type4 :
273 sem_graph_params -> (Joint.uns_params -> (__ -> __
274 Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
275 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
277 val sem_graph_params_inv_rect_Type3 :
278 sem_graph_params -> (Joint.uns_params -> (__ -> __
279 Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
280 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
282 val sem_graph_params_inv_rect_Type2 :
283 sem_graph_params -> (Joint.uns_params -> (__ -> __
284 Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
285 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
287 val sem_graph_params_inv_rect_Type1 :
288 sem_graph_params -> (Joint.uns_params -> (__ -> __
289 Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
290 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
292 val sem_graph_params_inv_rect_Type0 :
293 sem_graph_params -> (Joint.uns_params -> (__ -> __
294 Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
295 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
297 val sem_graph_params_jmdiscr : sem_graph_params -> sem_graph_params -> __
299 val sem_graph_params_to_graph_params : sem_graph_params -> Joint.graph_params
301 val sem_graph_params_to_sem_params :
302 sem_graph_params -> Joint_semantics.sem_params
304 val sem_params_from_sem_graph_params__o__spp' :
305 sem_graph_params -> Joint_semantics.serialized_params
307 val sem_params_from_sem_graph_params__o__spp'__o__msu_pars :
308 sem_graph_params -> Joint.joint_closed_internal_function
309 Joint_semantics.sem_unserialized_params
311 val sem_params_from_sem_graph_params__o__spp'__o__msu_pars__o__st_pars :
312 sem_graph_params -> Joint_semantics.sem_state_params
314 val sem_params_from_sem_graph_params__o__spp'__o__spp :
315 sem_graph_params -> Joint.params
317 val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars :
318 sem_graph_params -> Joint.stmt_params
320 val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
321 sem_graph_params -> Joint.uns_params
323 val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
324 sem_graph_params -> Joint.unserialized_params
326 type sem_lin_params = { slp_pars : Joint.uns_params;
328 Joint_semantics.sem_unserialized_params);
329 lin_pre_main_generator : (Joint.joint_program ->
330 Joint.joint_closed_internal_function) }
332 val sem_lin_params_rect_Type4 :
333 (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
334 (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
335 sem_lin_params -> 'a1
337 val sem_lin_params_rect_Type5 :
338 (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
339 (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
340 sem_lin_params -> 'a1
342 val sem_lin_params_rect_Type3 :
343 (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
344 (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
345 sem_lin_params -> 'a1
347 val sem_lin_params_rect_Type2 :
348 (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
349 (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
350 sem_lin_params -> 'a1
352 val sem_lin_params_rect_Type1 :
353 (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
354 (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
355 sem_lin_params -> 'a1
357 val sem_lin_params_rect_Type0 :
358 (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
359 (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
360 sem_lin_params -> 'a1
362 val slp_pars : sem_lin_params -> Joint.uns_params
364 val slp_sup0 : sem_lin_params -> 'a1 Joint_semantics.sem_unserialized_params
366 val lin_pre_main_generator :
367 sem_lin_params -> Joint.joint_program ->
368 Joint.joint_closed_internal_function
370 val sem_lin_params_inv_rect_Type4 :
371 sem_lin_params -> (Joint.uns_params -> (__ -> __
372 Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
373 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
375 val sem_lin_params_inv_rect_Type3 :
376 sem_lin_params -> (Joint.uns_params -> (__ -> __
377 Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
378 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
380 val sem_lin_params_inv_rect_Type2 :
381 sem_lin_params -> (Joint.uns_params -> (__ -> __
382 Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
383 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
385 val sem_lin_params_inv_rect_Type1 :
386 sem_lin_params -> (Joint.uns_params -> (__ -> __
387 Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
388 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
390 val sem_lin_params_inv_rect_Type0 :
391 sem_lin_params -> (Joint.uns_params -> (__ -> __
392 Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
393 Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
395 val sem_lin_params_jmdiscr : sem_lin_params -> sem_lin_params -> __
397 val sem_lin_params_to_lin_params : sem_lin_params -> Joint.lin_params
399 val sem_lin_params_to_sem_params :
400 sem_lin_params -> Joint_semantics.sem_params
402 val sem_params_from_sem_lin_params__o__spp' :
403 sem_lin_params -> Joint_semantics.serialized_params
405 val sem_params_from_sem_lin_params__o__spp'__o__msu_pars :
406 sem_lin_params -> Joint.joint_closed_internal_function
407 Joint_semantics.sem_unserialized_params
409 val sem_params_from_sem_lin_params__o__spp'__o__msu_pars__o__st_pars :
410 sem_lin_params -> Joint_semantics.sem_state_params
412 val sem_params_from_sem_lin_params__o__spp'__o__spp :
413 sem_lin_params -> Joint.params
415 val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars :
416 sem_lin_params -> Joint.stmt_params
418 val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
419 sem_lin_params -> Joint.uns_params
421 val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
422 sem_lin_params -> Joint.unserialized_params
424 val match_genv_t_rect_Type4 :
425 AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
426 Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
428 val match_genv_t_rect_Type5 :
429 AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
430 Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
432 val match_genv_t_rect_Type3 :
433 AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
434 Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
436 val match_genv_t_rect_Type2 :
437 AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
438 Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
440 val match_genv_t_rect_Type1 :
441 AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
442 Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
444 val match_genv_t_rect_Type0 :
445 AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
446 Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
448 val match_genv_t_inv_rect_Type4 :
449 AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
450 Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
452 val match_genv_t_inv_rect_Type3 :
453 AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
454 Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
456 val match_genv_t_inv_rect_Type2 :
457 AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
458 Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
460 val match_genv_t_inv_rect_Type1 :
461 AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
462 Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
464 val match_genv_t_inv_rect_Type0 :
465 AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
466 Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
468 val match_genv_t_discr :
469 AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
470 Globalenvs.genv_t -> __
472 val match_genv_t_jmdiscr :
473 AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
474 Globalenvs.genv_t -> __
476 val joint_globalenv :
477 Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
478 Types.option) -> Joint_semantics.genv