source: extracted/joint_semantics.mli @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 51.8 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               stack_usage : Nat.nat }
390
391val state_rect_Type4 :
392  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
393  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
394
395val state_rect_Type5 :
396  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
397  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
398
399val state_rect_Type3 :
400  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
401  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
402
403val state_rect_Type2 :
404  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
405  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
406
407val state_rect_Type1 :
408  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
409  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
410
411val state_rect_Type0 :
412  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
413  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
414
415val st_frms : sem_state_params -> state -> __ Types.option
416
417val istack : sem_state_params -> state -> internal_stack
418
419val carry : sem_state_params -> state -> ByteValues.bebit
420
421val regs : sem_state_params -> state -> __
422
423val m : sem_state_params -> state -> BEMem.bemem
424
425val stack_usage : sem_state_params -> state -> Nat.nat
426
427val state_inv_rect_Type4 :
428  sem_state_params -> state -> (__ Types.option -> internal_stack ->
429  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
430
431val state_inv_rect_Type3 :
432  sem_state_params -> state -> (__ Types.option -> internal_stack ->
433  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
434
435val state_inv_rect_Type2 :
436  sem_state_params -> state -> (__ Types.option -> internal_stack ->
437  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
438
439val state_inv_rect_Type1 :
440  sem_state_params -> state -> (__ Types.option -> internal_stack ->
441  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
442
443val state_inv_rect_Type0 :
444  sem_state_params -> state -> (__ Types.option -> internal_stack ->
445  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
446
447val state_jmdiscr : sem_state_params -> state -> state -> __
448
449val sp : sem_state_params -> state -> ByteValues.xpointer Errors.res
450
451type state_pc = { st_no_pc : state; pc : ByteValues.program_counter;
452                  last_pop : ByteValues.program_counter }
453
454val state_pc_rect_Type4 :
455  sem_state_params -> (state -> ByteValues.program_counter ->
456  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
457
458val state_pc_rect_Type5 :
459  sem_state_params -> (state -> ByteValues.program_counter ->
460  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
461
462val state_pc_rect_Type3 :
463  sem_state_params -> (state -> ByteValues.program_counter ->
464  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
465
466val state_pc_rect_Type2 :
467  sem_state_params -> (state -> ByteValues.program_counter ->
468  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
469
470val state_pc_rect_Type1 :
471  sem_state_params -> (state -> ByteValues.program_counter ->
472  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
473
474val state_pc_rect_Type0 :
475  sem_state_params -> (state -> ByteValues.program_counter ->
476  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
477
478val st_no_pc : sem_state_params -> state_pc -> state
479
480val pc : sem_state_params -> state_pc -> ByteValues.program_counter
481
482val last_pop : sem_state_params -> state_pc -> ByteValues.program_counter
483
484val state_pc_inv_rect_Type4 :
485  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
486  ByteValues.program_counter -> __ -> 'a1) -> 'a1
487
488val state_pc_inv_rect_Type3 :
489  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
490  ByteValues.program_counter -> __ -> 'a1) -> 'a1
491
492val state_pc_inv_rect_Type2 :
493  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
494  ByteValues.program_counter -> __ -> 'a1) -> 'a1
495
496val state_pc_inv_rect_Type1 :
497  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
498  ByteValues.program_counter -> __ -> 'a1) -> 'a1
499
500val state_pc_inv_rect_Type0 :
501  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
502  ByteValues.program_counter -> __ -> 'a1) -> 'a1
503
504val state_pc_discr : sem_state_params -> state_pc -> state_pc -> __
505
506val state_pc_jmdiscr : sem_state_params -> state_pc -> state_pc -> __
507
508val dpi1__o__st_no_pc__o__inject :
509  sem_state_params -> (state_pc, 'a1) Types.dPair -> state Types.sig0
510
511val eject__o__st_no_pc__o__inject :
512  sem_state_params -> state_pc Types.sig0 -> state Types.sig0
513
514val st_no_pc__o__inject : sem_state_params -> state_pc -> state Types.sig0
515
516val dpi1__o__st_no_pc :
517  sem_state_params -> (state_pc, 'a1) Types.dPair -> state
518
519val eject__o__st_no_pc : sem_state_params -> state_pc Types.sig0 -> state
520
521val init_pc : ByteValues.program_counter
522
523val null_pc : Positive.pos -> ByteValues.program_counter
524
525val set_m : sem_state_params -> BEMem.bemem -> state -> state
526
527val set_regs : sem_state_params -> __ -> state -> state
528
529val set_sp : sem_state_params -> ByteValues.xpointer -> state -> state
530
531val set_carry : sem_state_params -> ByteValues.bebit -> state -> state
532
533val set_istack : sem_state_params -> internal_stack -> state -> state
534
535val set_pc :
536  sem_state_params -> ByteValues.program_counter -> state_pc -> state_pc
537
538val set_no_pc : sem_state_params -> state -> state_pc -> state_pc
539
540val set_last_pop :
541  sem_state_params -> state -> ByteValues.program_counter -> 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 serialized_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 serialized_params_rect_Type4 :
1072  (Joint.params -> Joint.joint_closed_internal_function
1073  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1074  __ -> __ -> 'a1) -> serialized_params -> 'a1
1075
1076val serialized_params_rect_Type5 :
1077  (Joint.params -> Joint.joint_closed_internal_function
1078  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1079  __ -> __ -> 'a1) -> serialized_params -> 'a1
1080
1081val serialized_params_rect_Type3 :
1082  (Joint.params -> Joint.joint_closed_internal_function
1083  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1084  __ -> __ -> 'a1) -> serialized_params -> 'a1
1085
1086val serialized_params_rect_Type2 :
1087  (Joint.params -> Joint.joint_closed_internal_function
1088  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1089  __ -> __ -> 'a1) -> serialized_params -> 'a1
1090
1091val serialized_params_rect_Type1 :
1092  (Joint.params -> Joint.joint_closed_internal_function
1093  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1094  __ -> __ -> 'a1) -> serialized_params -> 'a1
1095
1096val serialized_params_rect_Type0 :
1097  (Joint.params -> Joint.joint_closed_internal_function
1098  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1099  __ -> __ -> 'a1) -> serialized_params -> 'a1
1100
1101val spp : serialized_params -> Joint.params
1102
1103val msu_pars :
1104  serialized_params -> Joint.joint_closed_internal_function
1105  sem_unserialized_params
1106
1107val offset_of_point : serialized_params -> __ -> Positive.pos
1108
1109val point_of_offset : serialized_params -> Positive.pos -> __
1110
1111val serialized_params_inv_rect_Type4 :
1112  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1113  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1114  __ -> __ -> __ -> 'a1) -> 'a1
1115
1116val serialized_params_inv_rect_Type3 :
1117  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1118  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1119  __ -> __ -> __ -> 'a1) -> 'a1
1120
1121val serialized_params_inv_rect_Type2 :
1122  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1123  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1124  __ -> __ -> __ -> 'a1) -> 'a1
1125
1126val serialized_params_inv_rect_Type1 :
1127  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1128  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1129  __ -> __ -> __ -> 'a1) -> 'a1
1130
1131val serialized_params_inv_rect_Type0 :
1132  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1133  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1134  __ -> __ -> __ -> 'a1) -> 'a1
1135
1136val serialized_params_jmdiscr : serialized_params -> serialized_params -> __
1137
1138val spp__o__stmt_pars : serialized_params -> Joint.stmt_params
1139
1140val spp__o__stmt_pars__o__uns_pars : serialized_params -> Joint.uns_params
1141
1142val spp__o__stmt_pars__o__uns_pars__o__u_pars :
1143  serialized_params -> Joint.unserialized_params
1144
1145val msu_pars__o__st_pars : serialized_params -> sem_state_params
1146
1147type sem_params = { spp' : serialized_params;
1148                    pre_main_generator : (Joint.joint_program ->
1149                                         Joint.joint_closed_internal_function) }
1150
1151val sem_params_rect_Type4 :
1152  (serialized_params -> (Joint.joint_program ->
1153  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1154
1155val sem_params_rect_Type5 :
1156  (serialized_params -> (Joint.joint_program ->
1157  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1158
1159val sem_params_rect_Type3 :
1160  (serialized_params -> (Joint.joint_program ->
1161  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1162
1163val sem_params_rect_Type2 :
1164  (serialized_params -> (Joint.joint_program ->
1165  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1166
1167val sem_params_rect_Type1 :
1168  (serialized_params -> (Joint.joint_program ->
1169  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1170
1171val sem_params_rect_Type0 :
1172  (serialized_params -> (Joint.joint_program ->
1173  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1174
1175val spp' : sem_params -> serialized_params
1176
1177val pre_main_generator :
1178  sem_params -> Joint.joint_program -> Joint.joint_closed_internal_function
1179
1180val sem_params_inv_rect_Type4 :
1181  sem_params -> (serialized_params -> (Joint.joint_program ->
1182  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1183
1184val sem_params_inv_rect_Type3 :
1185  sem_params -> (serialized_params -> (Joint.joint_program ->
1186  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1187
1188val sem_params_inv_rect_Type2 :
1189  sem_params -> (serialized_params -> (Joint.joint_program ->
1190  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1191
1192val sem_params_inv_rect_Type1 :
1193  sem_params -> (serialized_params -> (Joint.joint_program ->
1194  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1195
1196val sem_params_inv_rect_Type0 :
1197  sem_params -> (serialized_params -> (Joint.joint_program ->
1198  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1199
1200val sem_params_jmdiscr : sem_params -> sem_params -> __
1201
1202val spp'__o__msu_pars :
1203  sem_params -> Joint.joint_closed_internal_function sem_unserialized_params
1204
1205val spp'__o__msu_pars__o__st_pars : sem_params -> sem_state_params
1206
1207val spp'__o__spp : sem_params -> Joint.params
1208
1209val spp'__o__spp__o__stmt_pars : sem_params -> Joint.stmt_params
1210
1211val spp'__o__spp__o__stmt_pars__o__uns_pars : sem_params -> Joint.uns_params
1212
1213val spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
1214  sem_params -> Joint.unserialized_params
1215
1216val pc_of_point :
1217  sem_params -> Pointers.block Types.sig0 -> __ -> ByteValues.program_counter
1218
1219val point_of_pc : sem_params -> ByteValues.program_counter -> __
1220
1221val fetch_statement :
1222  sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
1223  -> ByteValues.program_counter -> ((AST.ident,
1224  Joint.joint_closed_internal_function) Types.prod, Joint.joint_statement)
1225  Types.prod Errors.res
1226
1227val pc_of_label :
1228  sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
1229  -> Pointers.block Types.sig0 -> Graphs.label -> ByteValues.program_counter
1230  Errors.res
1231
1232val succ_pc :
1233  sem_params -> ByteValues.program_counter -> __ ->
1234  ByteValues.program_counter
1235
1236val goto :
1237  sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
1238  -> Graphs.label -> state_pc -> state_pc Errors.res
1239
1240val next : sem_params -> __ -> state_pc -> state_pc
1241
1242val next_of_call_pc :
1243  sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
1244  -> ByteValues.program_counter -> __ Errors.res
1245
1246val eval_seq_no_pc :
1247  sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_seq
1248  -> state -> state Errors.res
1249
1250val code_block_of_block :
1251  Pointers.block -> Pointers.block Types.sig0 Types.option
1252
1253val block_of_funct_id :
1254  sem_state_params -> 'a1 Globalenvs.genv_t -> PreIdentifiers.identifier ->
1255  Pointers.block Types.sig0 Errors.res
1256
1257val block_of_call :
1258  sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
1259  -> (PreIdentifiers.identifier, (__, __) Types.prod) Types.sum -> state ->
1260  __
1261
1262val eval_external_call :
1263  sem_params -> AST.external_function -> __ -> __ -> state -> __
1264
1265val increment_stack_usage : sem_state_params -> Nat.nat -> state -> state
1266
1267val decrement_stack_usage : sem_state_params -> Nat.nat -> state -> state
1268
1269val eval_internal_call :
1270  sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
1271  Joint.joint_internal_function -> __ -> state -> __
1272
1273val is_inl : ('a1, 'a2) Types.sum -> Bool.bool
1274
1275val eval_call :
1276  sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
1277  (__, __) Types.prod) Types.sum -> __ -> __ -> __ -> state_pc -> __
1278
1279val eval_statement_no_pc :
1280  sem_params -> AST.ident List.list -> genv -> AST.ident ->
1281  Joint.joint_statement -> state -> state Errors.res
1282
1283val eval_return :
1284  sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
1285  __ -> state -> __
1286
1287val eval_tailcall :
1288  sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
1289  (__, __) Types.prod) Types.sum -> __ -> PreIdentifiers.identifier -> __ ->
1290  state_pc -> __
1291
1292val eval_statement_advance :
1293  sem_params -> AST.ident List.list -> genv -> AST.ident ->
1294  Joint.joint_closed_internal_function -> Joint.joint_statement -> state_pc
1295  -> (IO.io_out, IO.io_in, state_pc) IOMonad.iO
1296
1297val eval_state :
1298  sem_params -> AST.ident List.list -> genv -> state_pc -> (IO.io_out,
1299  IO.io_in, state_pc) IOMonad.iO
1300
Note: See TracBrowser for help on using the repository browser.