source: extracted/joint_semantics.mli @ 2829

Last change on this file since 2829 was 2829, checked in by sacerdot, 7 years ago

Semantics files committed.

File size: 48.9 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open Hide
12
13open ByteValues
14
15open Division
16
17open Z
18
19open BitVectorZ
20
21open Pointers
22
23open GenMem
24
25open FrontEndMem
26
27open Proper
28
29open PositiveMap
30
31open Deqsets
32
33open Extralib
34
35open Lists
36
37open Identifiers
38
39open Exp
40
41open Arithmetic
42
43open Vector
44
45open Div_and_mod
46
47open Util
48
49open FoldStuff
50
51open BitVector
52
53open Extranat
54
55open Integers
56
57open AST
58
59open ErrorMessages
60
61open Option
62
63open Setoids
64
65open Monad
66
67open Jmeq
68
69open Russell
70
71open Positive
72
73open PreIdentifiers
74
75open Bool
76
77open Relations
78
79open Nat
80
81open List
82
83open Hints_declaration
84
85open Core_notation
86
87open Pts
88
89open Logic
90
91open Types
92
93open Errors
94
95open Globalenvs
96
97open CostLabel
98
99open Events
100
101open IOMonad
102
103open IO
104
105open BEMem
106
107open String
108
109open Sets
110
111open Listb
112
113open LabelledObjects
114
115open BitVectorTrie
116
117open Graphs
118
119open I8051
120
121open Order
122
123open Registers
124
125open BackEndOps
126
127open Joint
128
129open I8051bis
130
131open ExtraGlobalenvs
132
133type 'f genv_gen = { ge : 'f AST.fundef Globalenvs.genv_t;
134                     stack_sizes : (AST.ident -> Nat.nat Types.option);
135                     get_pc_from_label : (AST.ident -> Graphs.label ->
136                                         ByteValues.program_counter
137                                         Errors.res) }
138
139val genv_gen_rect_Type4 :
140  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
141  (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
142  ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2
143
144val genv_gen_rect_Type5 :
145  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
146  (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
147  ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2
148
149val genv_gen_rect_Type3 :
150  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
151  (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
152  ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2
153
154val genv_gen_rect_Type2 :
155  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
156  (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
157  ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2
158
159val genv_gen_rect_Type1 :
160  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
161  (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
162  ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2
163
164val genv_gen_rect_Type0 :
165  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
166  (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
167  ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2
168
169val ge :
170  AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t
171
172val stack_sizes :
173  AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Nat.nat Types.option
174
175val get_pc_from_label :
176  AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
177  ByteValues.program_counter Errors.res
178
179val genv_gen_inv_rect_Type4 :
180  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
181  __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
182  ByteValues.program_counter Errors.res) -> __ -> 'a2) -> 'a2
183
184val genv_gen_inv_rect_Type3 :
185  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
186  __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
187  ByteValues.program_counter Errors.res) -> __ -> 'a2) -> 'a2
188
189val genv_gen_inv_rect_Type2 :
190  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
191  __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
192  ByteValues.program_counter Errors.res) -> __ -> 'a2) -> 'a2
193
194val genv_gen_inv_rect_Type1 :
195  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
196  __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
197  ByteValues.program_counter Errors.res) -> __ -> 'a2) -> 'a2
198
199val genv_gen_inv_rect_Type0 :
200  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
201  __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
202  ByteValues.program_counter Errors.res) -> __ -> 'a2) -> 'a2
203
204val genv_gen_discr :
205  AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __
206
207val genv_gen_jmdiscr :
208  AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __
209
210val dpi1__o__ge__o__inject :
211  AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
212  Globalenvs.genv_t Types.sig0
213
214val eject__o__ge__o__inject :
215  AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
216  Globalenvs.genv_t Types.sig0
217
218val ge__o__inject :
219  AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t
220  Types.sig0
221
222val dpi1__o__ge :
223  AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
224  Globalenvs.genv_t
225
226val eject__o__ge :
227  AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
228  Globalenvs.genv_t
229
230type genv = Joint.joint_closed_internal_function genv_gen
231
232val dpi1__o__genv_to_genv_t__o__inject :
233  Joint.params -> AST.ident List.list -> (genv, 'a1) Types.dPair ->
234  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
235  Types.sig0
236
237val eject__o__genv_to_genv_t__o__inject :
238  Joint.params -> AST.ident List.list -> genv Types.sig0 ->
239  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
240  Types.sig0
241
242val genv_to_genv_t__o__inject :
243  Joint.params -> AST.ident List.list -> genv ->
244  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
245  Types.sig0
246
247val dpi1__o__genv_to_genv_t :
248  Joint.params -> AST.ident List.list -> (genv, 'a1) Types.dPair ->
249  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
250
251val eject__o__genv_to_genv_t :
252  Joint.params -> AST.ident List.list -> genv Types.sig0 ->
253  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
254
255type sem_state_params = { empty_framesT : __;
256                          empty_regsT : (ByteValues.xpointer -> __);
257                          load_sp : (__ -> ByteValues.xpointer Errors.res);
258                          save_sp : (__ -> ByteValues.xpointer -> __) }
259
260val sem_state_params_rect_Type4 :
261  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
262  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
263  'a1) -> sem_state_params -> 'a1
264
265val sem_state_params_rect_Type5 :
266  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
267  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
268  'a1) -> sem_state_params -> 'a1
269
270val sem_state_params_rect_Type3 :
271  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
272  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
273  'a1) -> sem_state_params -> 'a1
274
275val sem_state_params_rect_Type2 :
276  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
277  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
278  'a1) -> sem_state_params -> 'a1
279
280val sem_state_params_rect_Type1 :
281  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
282  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
283  'a1) -> sem_state_params -> 'a1
284
285val sem_state_params_rect_Type0 :
286  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
287  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
288  'a1) -> sem_state_params -> 'a1
289
290type framesT
291
292val empty_framesT : sem_state_params -> __
293
294type regsT
295
296val empty_regsT : sem_state_params -> ByteValues.xpointer -> __
297
298val load_sp : sem_state_params -> __ -> ByteValues.xpointer Errors.res
299
300val save_sp : sem_state_params -> __ -> ByteValues.xpointer -> __
301
302val sem_state_params_inv_rect_Type4 :
303  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
304  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
305  __ -> 'a1) -> 'a1
306
307val sem_state_params_inv_rect_Type3 :
308  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
309  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
310  __ -> 'a1) -> 'a1
311
312val sem_state_params_inv_rect_Type2 :
313  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
314  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
315  __ -> 'a1) -> 'a1
316
317val sem_state_params_inv_rect_Type1 :
318  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
319  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
320  __ -> 'a1) -> 'a1
321
322val sem_state_params_inv_rect_Type0 :
323  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
324  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
325  __ -> 'a1) -> 'a1
326
327val sem_state_params_jmdiscr : sem_state_params -> sem_state_params -> __
328
329type internal_stack =
330| Empty_is
331| One_is of ByteValues.beval
332| Both_is of ByteValues.beval * ByteValues.beval
333
334val internal_stack_rect_Type4 :
335  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
336  -> 'a1) -> internal_stack -> 'a1
337
338val internal_stack_rect_Type5 :
339  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
340  -> 'a1) -> internal_stack -> 'a1
341
342val internal_stack_rect_Type3 :
343  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
344  -> 'a1) -> internal_stack -> 'a1
345
346val internal_stack_rect_Type2 :
347  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
348  -> 'a1) -> internal_stack -> 'a1
349
350val internal_stack_rect_Type1 :
351  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
352  -> 'a1) -> internal_stack -> 'a1
353
354val internal_stack_rect_Type0 :
355  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
356  -> 'a1) -> internal_stack -> 'a1
357
358val internal_stack_inv_rect_Type4 :
359  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
360  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
361
362val internal_stack_inv_rect_Type3 :
363  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
364  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
365
366val internal_stack_inv_rect_Type2 :
367  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
368  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
369
370val internal_stack_inv_rect_Type1 :
371  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
372  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
373
374val internal_stack_inv_rect_Type0 :
375  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
376  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
377
378val internal_stack_discr : internal_stack -> internal_stack -> __
379
380val internal_stack_jmdiscr : internal_stack -> internal_stack -> __
381
382val is_push : internal_stack -> ByteValues.beval -> internal_stack Errors.res
383
384val is_pop :
385  internal_stack -> (ByteValues.beval, internal_stack) Types.prod Errors.res
386
387type state = { st_frms : __ Types.option; istack : internal_stack;
388               carry : ByteValues.bebit; regs : __; m : BEMem.bemem }
389
390val state_rect_Type4 :
391  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
392  -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1
393
394val state_rect_Type5 :
395  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
396  -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1
397
398val state_rect_Type3 :
399  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
400  -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1
401
402val state_rect_Type2 :
403  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
404  -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1
405
406val state_rect_Type1 :
407  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
408  -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1
409
410val state_rect_Type0 :
411  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
412  -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1
413
414val st_frms : sem_state_params -> state -> __ Types.option
415
416val istack : sem_state_params -> state -> internal_stack
417
418val carry : sem_state_params -> state -> ByteValues.bebit
419
420val regs : sem_state_params -> state -> __
421
422val m : sem_state_params -> state -> BEMem.bemem
423
424val state_inv_rect_Type4 :
425  sem_state_params -> state -> (__ Types.option -> internal_stack ->
426  ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1
427
428val state_inv_rect_Type3 :
429  sem_state_params -> state -> (__ Types.option -> internal_stack ->
430  ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1
431
432val state_inv_rect_Type2 :
433  sem_state_params -> state -> (__ Types.option -> internal_stack ->
434  ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1
435
436val state_inv_rect_Type1 :
437  sem_state_params -> state -> (__ Types.option -> internal_stack ->
438  ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1
439
440val state_inv_rect_Type0 :
441  sem_state_params -> state -> (__ Types.option -> internal_stack ->
442  ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1
443
444val state_discr : sem_state_params -> state -> state -> __
445
446val state_jmdiscr : sem_state_params -> state -> state -> __
447
448val sp : sem_state_params -> state -> ByteValues.xpointer Errors.res
449
450type state_pc = { st_no_pc : state; pc : ByteValues.program_counter;
451                  last_pop : ByteValues.program_counter }
452
453val state_pc_rect_Type4 :
454  sem_state_params -> (state -> ByteValues.program_counter ->
455  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
456
457val state_pc_rect_Type5 :
458  sem_state_params -> (state -> ByteValues.program_counter ->
459  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
460
461val state_pc_rect_Type3 :
462  sem_state_params -> (state -> ByteValues.program_counter ->
463  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
464
465val state_pc_rect_Type2 :
466  sem_state_params -> (state -> ByteValues.program_counter ->
467  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
468
469val state_pc_rect_Type1 :
470  sem_state_params -> (state -> ByteValues.program_counter ->
471  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
472
473val state_pc_rect_Type0 :
474  sem_state_params -> (state -> ByteValues.program_counter ->
475  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
476
477val st_no_pc : sem_state_params -> state_pc -> state
478
479val pc : sem_state_params -> state_pc -> ByteValues.program_counter
480
481val last_pop : sem_state_params -> state_pc -> ByteValues.program_counter
482
483val state_pc_inv_rect_Type4 :
484  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
485  ByteValues.program_counter -> __ -> 'a1) -> 'a1
486
487val state_pc_inv_rect_Type3 :
488  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
489  ByteValues.program_counter -> __ -> 'a1) -> 'a1
490
491val state_pc_inv_rect_Type2 :
492  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
493  ByteValues.program_counter -> __ -> 'a1) -> 'a1
494
495val state_pc_inv_rect_Type1 :
496  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
497  ByteValues.program_counter -> __ -> 'a1) -> 'a1
498
499val state_pc_inv_rect_Type0 :
500  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
501  ByteValues.program_counter -> __ -> 'a1) -> 'a1
502
503val state_pc_discr : sem_state_params -> state_pc -> state_pc -> __
504
505val state_pc_jmdiscr : sem_state_params -> state_pc -> state_pc -> __
506
507val dpi1__o__st_no_pc__o__inject :
508  sem_state_params -> (state_pc, 'a1) Types.dPair -> state Types.sig0
509
510val eject__o__st_no_pc__o__inject :
511  sem_state_params -> state_pc Types.sig0 -> state Types.sig0
512
513val st_no_pc__o__inject : sem_state_params -> state_pc -> state Types.sig0
514
515val dpi1__o__st_no_pc :
516  sem_state_params -> (state_pc, 'a1) Types.dPair -> state
517
518val eject__o__st_no_pc : sem_state_params -> state_pc Types.sig0 -> state
519
520val exit_pc : ByteValues.program_counter
521
522val null_pc : Positive.pos -> ByteValues.program_counter
523
524val set_m : sem_state_params -> BEMem.bemem -> state -> state
525
526val set_regs : sem_state_params -> __ -> state -> state
527
528val set_sp : sem_state_params -> ByteValues.xpointer -> state -> state
529
530val set_carry : sem_state_params -> ByteValues.bebit -> state -> state
531
532val set_istack : sem_state_params -> internal_stack -> state -> state
533
534val set_pc :
535  sem_state_params -> ByteValues.program_counter -> state_pc -> state_pc
536
537val set_no_pc : sem_state_params -> state -> state_pc -> state_pc
538
539val set_last_pop :
540  sem_state_params -> ByteValues.program_counter -> (state,
541  ByteValues.program_counter) Types.prod -> state_pc
542
543val set_frms : sem_state_params -> __ -> state -> state
544
545val fetch_function :
546  'a1 Globalenvs.genv_t -> Pointers.block Types.sig0 -> (AST.ident, 'a1)
547  Types.prod Errors.res
548
549val fetch_internal_function :
550  'a1 AST.fundef Globalenvs.genv_t -> Pointers.block Types.sig0 ->
551  (AST.ident, 'a1) Types.prod Errors.res
552
553type call_kind =
554| PTR
555| ID
556
557val call_kind_rect_Type4 : 'a1 -> 'a1 -> call_kind -> 'a1
558
559val call_kind_rect_Type5 : 'a1 -> 'a1 -> call_kind -> 'a1
560
561val call_kind_rect_Type3 : 'a1 -> 'a1 -> call_kind -> 'a1
562
563val call_kind_rect_Type2 : 'a1 -> 'a1 -> call_kind -> 'a1
564
565val call_kind_rect_Type1 : 'a1 -> 'a1 -> call_kind -> 'a1
566
567val call_kind_rect_Type0 : 'a1 -> 'a1 -> call_kind -> 'a1
568
569val call_kind_inv_rect_Type4 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
570
571val call_kind_inv_rect_Type3 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
572
573val call_kind_inv_rect_Type2 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
574
575val call_kind_inv_rect_Type1 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
576
577val call_kind_inv_rect_Type0 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
578
579val call_kind_discr : call_kind -> call_kind -> __
580
581val call_kind_jmdiscr : call_kind -> call_kind -> __
582
583val kind_of_call :
584  Joint.unserialized_params -> (AST.ident, (__, __) Types.prod) Types.sum ->
585  call_kind
586
587type 'f sem_unserialized_params = { st_pars : sem_state_params;
588                                    acca_store_ : (__ -> ByteValues.beval ->
589                                                  __ -> __ Errors.res);
590                                    acca_retrieve_ : (__ -> __ ->
591                                                     ByteValues.beval
592                                                     Errors.res);
593                                    acca_arg_retrieve_ : (__ -> __ ->
594                                                         ByteValues.beval
595                                                         Errors.res);
596                                    accb_store_ : (__ -> ByteValues.beval ->
597                                                  __ -> __ Errors.res);
598                                    accb_retrieve_ : (__ -> __ ->
599                                                     ByteValues.beval
600                                                     Errors.res);
601                                    accb_arg_retrieve_ : (__ -> __ ->
602                                                         ByteValues.beval
603                                                         Errors.res);
604                                    dpl_store_ : (__ -> ByteValues.beval ->
605                                                 __ -> __ Errors.res);
606                                    dpl_retrieve_ : (__ -> __ ->
607                                                    ByteValues.beval
608                                                    Errors.res);
609                                    dpl_arg_retrieve_ : (__ -> __ ->
610                                                        ByteValues.beval
611                                                        Errors.res);
612                                    dph_store_ : (__ -> ByteValues.beval ->
613                                                 __ -> __ Errors.res);
614                                    dph_retrieve_ : (__ -> __ ->
615                                                    ByteValues.beval
616                                                    Errors.res);
617                                    dph_arg_retrieve_ : (__ -> __ ->
618                                                        ByteValues.beval
619                                                        Errors.res);
620                                    snd_arg_retrieve_ : (__ -> __ ->
621                                                        ByteValues.beval
622                                                        Errors.res);
623                                    pair_reg_move_ : (__ -> __ -> __
624                                                     Errors.res);
625                                    save_frame : (call_kind -> __ -> state_pc
626                                                 -> state Errors.res);
627                                    setup_call : (Nat.nat -> __ -> __ ->
628                                                 state -> state Errors.res);
629                                    fetch_external_args : (AST.external_function
630                                                          -> state -> __ ->
631                                                          Values.val0
632                                                          List.list
633                                                          Errors.res);
634                                    set_result : (Values.val0 List.list -> __
635                                                 -> state -> state
636                                                 Errors.res);
637                                    call_args_for_main : __;
638                                    call_dest_for_main : __;
639                                    read_result : (AST.ident List.list -> 'f
640                                                  AST.fundef
641                                                  Globalenvs.genv_t -> __ ->
642                                                  state -> ByteValues.beval
643                                                  List.list Errors.res);
644                                    eval_ext_seq : (AST.ident List.list -> 'f
645                                                   genv_gen -> __ ->
646                                                   AST.ident -> state ->
647                                                   state Errors.res);
648                                    pop_frame : (AST.ident List.list -> 'f
649                                                genv_gen -> AST.ident -> __
650                                                -> state -> (state,
651                                                ByteValues.program_counter)
652                                                Types.prod Errors.res) }
653
654val sem_unserialized_params_rect_Type4 :
655  Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
656  -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
657  -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
658  __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
659  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
660  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
661  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
662  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
663  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
664  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
665  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
666  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
667  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
668  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
669  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
670  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
671  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
672  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
673  sem_unserialized_params -> 'a2
674
675val sem_unserialized_params_rect_Type5 :
676  Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
677  -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
678  -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
679  __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
680  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
681  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
682  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
683  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
684  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
685  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
686  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
687  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
688  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
689  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
690  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
691  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
692  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
693  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
694  sem_unserialized_params -> 'a2
695
696val sem_unserialized_params_rect_Type3 :
697  Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
698  -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
699  -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
700  __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
701  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
702  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
703  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
704  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
705  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
706  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
707  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
708  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
709  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
710  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
711  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
712  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
713  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
714  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
715  sem_unserialized_params -> 'a2
716
717val sem_unserialized_params_rect_Type2 :
718  Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
719  -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
720  -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
721  __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
722  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
723  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
724  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
725  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
726  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
727  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
728  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
729  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
730  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
731  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
732  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
733  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
734  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
735  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
736  sem_unserialized_params -> 'a2
737
738val sem_unserialized_params_rect_Type1 :
739  Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
740  -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
741  -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
742  __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
743  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
744  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
745  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
746  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
747  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
748  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
749  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
750  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
751  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
752  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
753  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
754  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
755  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
756  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
757  sem_unserialized_params -> 'a2
758
759val sem_unserialized_params_rect_Type0 :
760  Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval
761  -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__
762  -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ ->
763  __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
764  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
765  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
766  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
767  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
768  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
769  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
770  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
771  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
772  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
773  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
774  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
775  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
776  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
777  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
778  sem_unserialized_params -> 'a2
779
780val st_pars :
781  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
782  sem_state_params
783
784val acca_store_ :
785  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
786  ByteValues.beval -> __ -> __ Errors.res
787
788val acca_retrieve_ :
789  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
790  ByteValues.beval Errors.res
791
792val acca_arg_retrieve_ :
793  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
794  ByteValues.beval Errors.res
795
796val accb_store_ :
797  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
798  ByteValues.beval -> __ -> __ Errors.res
799
800val accb_retrieve_ :
801  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
802  ByteValues.beval Errors.res
803
804val accb_arg_retrieve_ :
805  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
806  ByteValues.beval Errors.res
807
808val dpl_store_ :
809  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
810  ByteValues.beval -> __ -> __ Errors.res
811
812val dpl_retrieve_ :
813  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
814  ByteValues.beval Errors.res
815
816val dpl_arg_retrieve_ :
817  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
818  ByteValues.beval Errors.res
819
820val dph_store_ :
821  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
822  ByteValues.beval -> __ -> __ Errors.res
823
824val dph_retrieve_ :
825  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
826  ByteValues.beval Errors.res
827
828val dph_arg_retrieve_ :
829  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
830  ByteValues.beval Errors.res
831
832val snd_arg_retrieve_ :
833  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
834  ByteValues.beval Errors.res
835
836val pair_reg_move_ :
837  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> __
838  Errors.res
839
840val save_frame :
841  Joint.unserialized_params -> 'a1 sem_unserialized_params -> call_kind -> __
842  -> state_pc -> state Errors.res
843
844val setup_call :
845  Joint.unserialized_params -> 'a1 sem_unserialized_params -> Nat.nat -> __
846  -> __ -> state -> state Errors.res
847
848val fetch_external_args :
849  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
850  AST.external_function -> state -> __ -> Values.val0 List.list Errors.res
851
852val set_result :
853  Joint.unserialized_params -> 'a1 sem_unserialized_params -> Values.val0
854  List.list -> __ -> state -> state Errors.res
855
856val call_args_for_main :
857  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __
858
859val call_dest_for_main :
860  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __
861
862val read_result :
863  Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
864  List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state ->
865  ByteValues.beval List.list Errors.res
866
867val eval_ext_seq :
868  Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
869  List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res
870
871val pop_frame :
872  Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
873  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
874  ByteValues.program_counter) Types.prod Errors.res
875
876val sem_unserialized_params_inv_rect_Type4 :
877  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
878  (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
879  -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
880  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
881  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
882  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
883  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
884  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
885  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
886  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
887  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
888  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
889  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
890  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
891  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
892  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
893  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
894  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
895  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
896
897val sem_unserialized_params_inv_rect_Type3 :
898  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
899  (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
900  -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
901  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
902  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
903  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
904  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
905  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
906  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
907  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
908  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
909  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
910  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
911  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
912  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
913  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
914  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
915  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
916  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
917
918val sem_unserialized_params_inv_rect_Type2 :
919  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
920  (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
921  -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
922  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
923  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
924  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
925  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
926  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
927  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
928  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
929  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
930  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
931  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
932  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
933  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
934  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
935  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
936  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
937  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
938
939val sem_unserialized_params_inv_rect_Type1 :
940  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
941  (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
942  -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
943  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
944  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
945  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
946  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
947  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
948  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
949  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
950  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
951  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
952  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
953  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
954  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
955  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
956  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
957  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
958  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
959
960val sem_unserialized_params_inv_rect_Type0 :
961  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
962  (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__
963  -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
964  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
965  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
966  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
967  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
968  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
969  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
970  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
971  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
972  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
973  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
974  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
975  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
976  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
977  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
978  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
979  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
980
981val sem_unserialized_params_jmdiscr :
982  Joint.unserialized_params -> 'a1 sem_unserialized_params -> 'a1
983  sem_unserialized_params -> __
984
985val helper_def_retrieve :
986  (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> __ -> 'a1
987  -> ByteValues.beval Errors.res) -> Joint.unserialized_params -> 'a2
988  sem_unserialized_params -> state -> 'a1 -> ByteValues.beval Errors.res
989
990val helper_def_store :
991  (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> 'a1 ->
992  ByteValues.beval -> __ -> __ Errors.res) -> Joint.unserialized_params ->
993  'a2 sem_unserialized_params -> 'a1 -> ByteValues.beval -> state -> state
994  Errors.res
995
996val acca_retrieve :
997  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
998  ByteValues.beval Errors.res
999
1000val acca_store :
1001  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1002  ByteValues.beval -> state -> state Errors.res
1003
1004val acca_arg_retrieve :
1005  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1006  ByteValues.beval Errors.res
1007
1008val accb_store :
1009  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1010  ByteValues.beval -> state -> state Errors.res
1011
1012val accb_retrieve :
1013  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1014  ByteValues.beval Errors.res
1015
1016val accb_arg_retrieve :
1017  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1018  ByteValues.beval Errors.res
1019
1020val dpl_store :
1021  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1022  ByteValues.beval -> state -> state Errors.res
1023
1024val dpl_retrieve :
1025  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1026  ByteValues.beval Errors.res
1027
1028val dpl_arg_retrieve :
1029  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1030  ByteValues.beval Errors.res
1031
1032val dph_store :
1033  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1034  ByteValues.beval -> state -> state Errors.res
1035
1036val dph_retrieve :
1037  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1038  ByteValues.beval Errors.res
1039
1040val dph_arg_retrieve :
1041  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1042  ByteValues.beval Errors.res
1043
1044val snd_arg_retrieve :
1045  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1046  ByteValues.beval Errors.res
1047
1048val pair_reg_move :
1049  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1050  __
1051
1052val push : sem_state_params -> state -> ByteValues.beval -> state Errors.res
1053
1054val pop :
1055  sem_state_params -> state -> (ByteValues.beval, state) Types.prod
1056  Errors.res
1057
1058val push_ra :
1059  sem_state_params -> state -> ByteValues.program_counter -> state Errors.res
1060
1061val pop_ra :
1062  sem_state_params -> state -> (state, ByteValues.program_counter) Types.prod
1063  Errors.res
1064
1065type sem_params = { spp : Joint.params;
1066                    msu_pars : Joint.joint_closed_internal_function
1067                               sem_unserialized_params;
1068                    offset_of_point : (__ -> Positive.pos);
1069                    point_of_offset : (Positive.pos -> __) }
1070
1071val sem_params_rect_Type4 :
1072  (Joint.params -> Joint.joint_closed_internal_function
1073  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1074  __ -> __ -> 'a1) -> sem_params -> 'a1
1075
1076val sem_params_rect_Type5 :
1077  (Joint.params -> Joint.joint_closed_internal_function
1078  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1079  __ -> __ -> 'a1) -> sem_params -> 'a1
1080
1081val sem_params_rect_Type3 :
1082  (Joint.params -> Joint.joint_closed_internal_function
1083  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1084  __ -> __ -> 'a1) -> sem_params -> 'a1
1085
1086val sem_params_rect_Type2 :
1087  (Joint.params -> Joint.joint_closed_internal_function
1088  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1089  __ -> __ -> 'a1) -> sem_params -> 'a1
1090
1091val sem_params_rect_Type1 :
1092  (Joint.params -> Joint.joint_closed_internal_function
1093  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1094  __ -> __ -> 'a1) -> sem_params -> 'a1
1095
1096val sem_params_rect_Type0 :
1097  (Joint.params -> Joint.joint_closed_internal_function
1098  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1099  __ -> __ -> 'a1) -> sem_params -> 'a1
1100
1101val spp : sem_params -> Joint.params
1102
1103val msu_pars :
1104  sem_params -> Joint.joint_closed_internal_function sem_unserialized_params
1105
1106val offset_of_point : sem_params -> __ -> Positive.pos
1107
1108val point_of_offset : sem_params -> Positive.pos -> __
1109
1110val sem_params_inv_rect_Type4 :
1111  sem_params -> (Joint.params -> Joint.joint_closed_internal_function
1112  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1113  __ -> __ -> __ -> 'a1) -> 'a1
1114
1115val sem_params_inv_rect_Type3 :
1116  sem_params -> (Joint.params -> Joint.joint_closed_internal_function
1117  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1118  __ -> __ -> __ -> 'a1) -> 'a1
1119
1120val sem_params_inv_rect_Type2 :
1121  sem_params -> (Joint.params -> Joint.joint_closed_internal_function
1122  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1123  __ -> __ -> __ -> 'a1) -> 'a1
1124
1125val sem_params_inv_rect_Type1 :
1126  sem_params -> (Joint.params -> Joint.joint_closed_internal_function
1127  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1128  __ -> __ -> __ -> 'a1) -> 'a1
1129
1130val sem_params_inv_rect_Type0 :
1131  sem_params -> (Joint.params -> Joint.joint_closed_internal_function
1132  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1133  __ -> __ -> __ -> 'a1) -> 'a1
1134
1135val sem_params_jmdiscr : sem_params -> sem_params -> __
1136
1137val spp__o__stmt_pars : sem_params -> Joint.stmt_params
1138
1139val spp__o__stmt_pars__o__uns_pars : sem_params -> Joint.uns_params
1140
1141val spp__o__stmt_pars__o__uns_pars__o__u_pars :
1142  sem_params -> Joint.unserialized_params
1143
1144val msu_pars__o__st_pars : sem_params -> sem_state_params
1145
1146val pc_of_point :
1147  sem_params -> Pointers.block Types.sig0 -> __ -> ByteValues.program_counter
1148
1149val point_of_pc : sem_params -> ByteValues.program_counter -> __
1150
1151val fetch_statement :
1152  sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
1153  -> ByteValues.program_counter -> ((AST.ident,
1154  Joint.joint_closed_internal_function) Types.prod, Joint.joint_statement)
1155  Types.prod Errors.res
1156
1157val pc_of_label :
1158  sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
1159  -> Pointers.block Types.sig0 -> Graphs.label -> ByteValues.program_counter
1160  Errors.res
1161
1162val succ_pc :
1163  sem_params -> ByteValues.program_counter -> __ ->
1164  ByteValues.program_counter
1165
1166val goto :
1167  sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
1168  -> Graphs.label -> state_pc -> state_pc Errors.res
1169
1170val next : sem_params -> __ -> state_pc -> state_pc
1171
1172val next_of_call_pc :
1173  sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
1174  -> ByteValues.program_counter -> __ Errors.res
1175
1176val eval_seq_no_pc :
1177  sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_seq
1178  -> state -> state Errors.res
1179
1180val code_block_of_block :
1181  Pointers.block -> Pointers.block Types.sig0 Types.option
1182
1183val block_of_funct_id :
1184  sem_state_params -> 'a1 Globalenvs.genv_t -> PreIdentifiers.identifier ->
1185  Pointers.block Types.sig0 Errors.res
1186
1187val block_of_call :
1188  sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
1189  -> (PreIdentifiers.identifier, (__, __) Types.prod) Types.sum -> state ->
1190  __
1191
1192val eval_external_call :
1193  sem_params -> AST.external_function -> __ -> __ -> state -> __
1194
1195val eval_internal_call :
1196  sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
1197  Joint.joint_internal_function -> __ -> state -> __
1198
1199val is_inl : ('a1, 'a2) Types.sum -> Bool.bool
1200
1201val eval_call :
1202  sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
1203  (__, __) Types.prod) Types.sum -> __ -> __ -> __ -> state_pc -> __
1204
1205val eval_statement_no_pc :
1206  sem_params -> AST.ident List.list -> genv -> AST.ident ->
1207  Joint.joint_statement -> state -> state Errors.res
1208
1209val eval_return :
1210  sem_params -> AST.ident List.list -> genv -> AST.ident -> __ -> state -> __
1211
1212val eval_tailcall :
1213  sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
1214  (__, __) Types.prod) Types.sum -> __ -> AST.ident -> __ -> state_pc -> __
1215
1216val eval_statement_advance :
1217  sem_params -> AST.ident List.list -> genv -> AST.ident ->
1218  Joint.joint_closed_internal_function -> Joint.joint_statement -> state_pc
1219  -> (IO.io_out, IO.io_in, state_pc) IOMonad.iO
1220
1221val eval_state :
1222  sem_params -> AST.ident List.list -> genv -> state_pc -> (IO.io_out,
1223  IO.io_in, state_pc) IOMonad.iO
1224
1225val is_final :
1226  sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter ->
1227  state_pc -> Integers.int Types.option
1228
Note: See TracBrowser for help on using the repository browser.