source: driver/extracted/joint_semantics.mli @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 51.4 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                     premain : 'f;
136                     pc_from_label : (Pointers.block Types.sig0 -> 'f ->
137                                     Graphs.label ->
138                                     ByteValues.program_counter Types.option) }
139
140val genv_gen_rect_Type4 :
141  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
142  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
143  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
144  'a1 genv_gen -> 'a2
145
146val genv_gen_rect_Type5 :
147  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
148  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
149  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
150  'a1 genv_gen -> 'a2
151
152val genv_gen_rect_Type3 :
153  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
154  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
155  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
156  'a1 genv_gen -> 'a2
157
158val genv_gen_rect_Type2 :
159  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
160  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
161  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
162  'a1 genv_gen -> 'a2
163
164val genv_gen_rect_Type1 :
165  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
166  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
167  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
168  'a1 genv_gen -> 'a2
169
170val genv_gen_rect_Type0 :
171  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
172  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
173  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
174  'a1 genv_gen -> 'a2
175
176val ge :
177  AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t
178
179val stack_sizes :
180  AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Nat.nat Types.option
181
182val premain : AST.ident List.list -> 'a1 genv_gen -> 'a1
183
184val pc_from_label :
185  AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 -> 'a1 ->
186  Graphs.label -> ByteValues.program_counter Types.option
187
188val genv_gen_inv_rect_Type4 :
189  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
190  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
191  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
192  Types.option) -> __ -> 'a2) -> 'a2
193
194val genv_gen_inv_rect_Type3 :
195  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
196  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
197  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
198  Types.option) -> __ -> 'a2) -> 'a2
199
200val genv_gen_inv_rect_Type2 :
201  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
202  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
203  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
204  Types.option) -> __ -> 'a2) -> 'a2
205
206val genv_gen_inv_rect_Type1 :
207  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
208  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
209  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
210  Types.option) -> __ -> 'a2) -> 'a2
211
212val genv_gen_inv_rect_Type0 :
213  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
214  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
215  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
216  Types.option) -> __ -> 'a2) -> 'a2
217
218val genv_gen_discr :
219  AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __
220
221val genv_gen_jmdiscr :
222  AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __
223
224val dpi1__o__ge__o__inject :
225  AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
226  Globalenvs.genv_t Types.sig0
227
228val eject__o__ge__o__inject :
229  AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
230  Globalenvs.genv_t Types.sig0
231
232val ge__o__inject :
233  AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t
234  Types.sig0
235
236val dpi1__o__ge :
237  AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef
238  Globalenvs.genv_t
239
240val eject__o__ge :
241  AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
242  Globalenvs.genv_t
243
244val pre_main_id : AST.ident
245
246val fetch_function :
247  AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
248  (AST.ident, 'a1 AST.fundef) Types.prod Errors.res
249
250val fetch_internal_function :
251  AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
252  (AST.ident, 'a1) Types.prod Errors.res
253
254val code_block_of_block :
255  Pointers.block -> Pointers.block Types.sig0 Types.option
256
257val block_of_funct_id :
258  'a1 Globalenvs.genv_t -> PreIdentifiers.identifier -> Pointers.block
259  Types.sig0 Errors.res
260
261val gen_pc_from_label :
262  AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
263  ByteValues.program_counter Errors.res
264
265type genv = Joint.joint_closed_internal_function genv_gen
266
267type sem_state_params = { empty_framesT : __;
268                          empty_regsT : (ByteValues.xpointer -> __);
269                          load_sp : (__ -> ByteValues.xpointer Errors.res);
270                          save_sp : (__ -> ByteValues.xpointer -> __) }
271
272val sem_state_params_rect_Type4 :
273  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
274  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
275  'a1) -> sem_state_params -> 'a1
276
277val sem_state_params_rect_Type5 :
278  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
279  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
280  'a1) -> sem_state_params -> 'a1
281
282val sem_state_params_rect_Type3 :
283  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
284  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
285  'a1) -> sem_state_params -> 'a1
286
287val sem_state_params_rect_Type2 :
288  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
289  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
290  'a1) -> sem_state_params -> 'a1
291
292val sem_state_params_rect_Type1 :
293  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
294  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
295  'a1) -> sem_state_params -> 'a1
296
297val sem_state_params_rect_Type0 :
298  (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ ->
299  ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
300  'a1) -> sem_state_params -> 'a1
301
302type framesT
303
304val empty_framesT : sem_state_params -> __
305
306type regsT
307
308val empty_regsT : sem_state_params -> ByteValues.xpointer -> __
309
310val load_sp : sem_state_params -> __ -> ByteValues.xpointer Errors.res
311
312val save_sp : sem_state_params -> __ -> ByteValues.xpointer -> __
313
314val sem_state_params_inv_rect_Type4 :
315  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
316  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
317  __ -> 'a1) -> 'a1
318
319val sem_state_params_inv_rect_Type3 :
320  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
321  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
322  __ -> 'a1) -> 'a1
323
324val sem_state_params_inv_rect_Type2 :
325  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
326  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
327  __ -> 'a1) -> 'a1
328
329val sem_state_params_inv_rect_Type1 :
330  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
331  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
332  __ -> 'a1) -> 'a1
333
334val sem_state_params_inv_rect_Type0 :
335  sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__
336  -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
337  __ -> 'a1) -> 'a1
338
339val sem_state_params_jmdiscr : sem_state_params -> sem_state_params -> __
340
341type internal_stack =
342| Empty_is
343| One_is of ByteValues.beval
344| Both_is of ByteValues.beval * ByteValues.beval
345
346val internal_stack_rect_Type4 :
347  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
348  -> 'a1) -> internal_stack -> 'a1
349
350val internal_stack_rect_Type5 :
351  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
352  -> 'a1) -> internal_stack -> 'a1
353
354val internal_stack_rect_Type3 :
355  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
356  -> 'a1) -> internal_stack -> 'a1
357
358val internal_stack_rect_Type2 :
359  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
360  -> 'a1) -> internal_stack -> 'a1
361
362val internal_stack_rect_Type1 :
363  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
364  -> 'a1) -> internal_stack -> 'a1
365
366val internal_stack_rect_Type0 :
367  'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval
368  -> 'a1) -> internal_stack -> 'a1
369
370val internal_stack_inv_rect_Type4 :
371  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
372  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
373
374val internal_stack_inv_rect_Type3 :
375  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
376  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
377
378val internal_stack_inv_rect_Type2 :
379  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
380  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
381
382val internal_stack_inv_rect_Type1 :
383  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
384  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
385
386val internal_stack_inv_rect_Type0 :
387  internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) ->
388  (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1
389
390val internal_stack_discr : internal_stack -> internal_stack -> __
391
392val internal_stack_jmdiscr : internal_stack -> internal_stack -> __
393
394val is_push : internal_stack -> ByteValues.beval -> internal_stack Errors.res
395
396val is_pop :
397  internal_stack -> (ByteValues.beval, internal_stack) Types.prod Errors.res
398
399type state = { st_frms : __ Types.option; istack : internal_stack;
400               carry : ByteValues.bebit; regs : __; m : BEMem.bemem;
401               stack_usage : Nat.nat }
402
403val state_rect_Type4 :
404  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
405  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
406
407val state_rect_Type5 :
408  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
409  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
410
411val state_rect_Type3 :
412  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
413  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
414
415val state_rect_Type2 :
416  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
417  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
418
419val state_rect_Type1 :
420  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
421  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
422
423val state_rect_Type0 :
424  sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit
425  -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1
426
427val st_frms : sem_state_params -> state -> __ Types.option
428
429val istack : sem_state_params -> state -> internal_stack
430
431val carry : sem_state_params -> state -> ByteValues.bebit
432
433val regs : sem_state_params -> state -> __
434
435val m : sem_state_params -> state -> BEMem.bemem
436
437val stack_usage : sem_state_params -> state -> Nat.nat
438
439val state_inv_rect_Type4 :
440  sem_state_params -> state -> (__ Types.option -> internal_stack ->
441  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
442
443val state_inv_rect_Type3 :
444  sem_state_params -> state -> (__ Types.option -> internal_stack ->
445  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
446
447val state_inv_rect_Type2 :
448  sem_state_params -> state -> (__ Types.option -> internal_stack ->
449  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
450
451val state_inv_rect_Type1 :
452  sem_state_params -> state -> (__ Types.option -> internal_stack ->
453  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
454
455val state_inv_rect_Type0 :
456  sem_state_params -> state -> (__ Types.option -> internal_stack ->
457  ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1
458
459val state_jmdiscr : sem_state_params -> state -> state -> __
460
461val sp : sem_state_params -> state -> ByteValues.xpointer Errors.res
462
463type state_pc = { st_no_pc : state; pc : ByteValues.program_counter;
464                  last_pop : ByteValues.program_counter }
465
466val state_pc_rect_Type4 :
467  sem_state_params -> (state -> ByteValues.program_counter ->
468  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
469
470val state_pc_rect_Type5 :
471  sem_state_params -> (state -> ByteValues.program_counter ->
472  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
473
474val state_pc_rect_Type3 :
475  sem_state_params -> (state -> ByteValues.program_counter ->
476  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
477
478val state_pc_rect_Type2 :
479  sem_state_params -> (state -> ByteValues.program_counter ->
480  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
481
482val state_pc_rect_Type1 :
483  sem_state_params -> (state -> ByteValues.program_counter ->
484  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
485
486val state_pc_rect_Type0 :
487  sem_state_params -> (state -> ByteValues.program_counter ->
488  ByteValues.program_counter -> 'a1) -> state_pc -> 'a1
489
490val st_no_pc : sem_state_params -> state_pc -> state
491
492val pc : sem_state_params -> state_pc -> ByteValues.program_counter
493
494val last_pop : sem_state_params -> state_pc -> ByteValues.program_counter
495
496val state_pc_inv_rect_Type4 :
497  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
498  ByteValues.program_counter -> __ -> 'a1) -> 'a1
499
500val state_pc_inv_rect_Type3 :
501  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
502  ByteValues.program_counter -> __ -> 'a1) -> 'a1
503
504val state_pc_inv_rect_Type2 :
505  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
506  ByteValues.program_counter -> __ -> 'a1) -> 'a1
507
508val state_pc_inv_rect_Type1 :
509  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
510  ByteValues.program_counter -> __ -> 'a1) -> 'a1
511
512val state_pc_inv_rect_Type0 :
513  sem_state_params -> state_pc -> (state -> ByteValues.program_counter ->
514  ByteValues.program_counter -> __ -> 'a1) -> 'a1
515
516val state_pc_discr : sem_state_params -> state_pc -> state_pc -> __
517
518val state_pc_jmdiscr : sem_state_params -> state_pc -> state_pc -> __
519
520val dpi1__o__st_no_pc__o__inject :
521  sem_state_params -> (state_pc, 'a1) Types.dPair -> state Types.sig0
522
523val eject__o__st_no_pc__o__inject :
524  sem_state_params -> state_pc Types.sig0 -> state Types.sig0
525
526val st_no_pc__o__inject : sem_state_params -> state_pc -> state Types.sig0
527
528val dpi1__o__st_no_pc :
529  sem_state_params -> (state_pc, 'a1) Types.dPair -> state
530
531val eject__o__st_no_pc : sem_state_params -> state_pc Types.sig0 -> state
532
533val init_pc : ByteValues.program_counter
534
535val null_pc : Positive.pos -> ByteValues.program_counter
536
537val set_m : sem_state_params -> BEMem.bemem -> state -> state
538
539val set_regs : sem_state_params -> __ -> state -> state
540
541val set_sp : sem_state_params -> ByteValues.xpointer -> state -> state
542
543val set_carry : sem_state_params -> ByteValues.bebit -> state -> state
544
545val set_istack : sem_state_params -> internal_stack -> state -> state
546
547val set_pc :
548  sem_state_params -> ByteValues.program_counter -> state_pc -> state_pc
549
550val set_no_pc : sem_state_params -> state -> state_pc -> state_pc
551
552val set_last_pop :
553  sem_state_params -> state -> ByteValues.program_counter -> state_pc
554
555val set_frms : sem_state_params -> __ -> state -> state
556
557type call_kind =
558| PTR
559| ID
560
561val call_kind_rect_Type4 : 'a1 -> 'a1 -> call_kind -> 'a1
562
563val call_kind_rect_Type5 : 'a1 -> 'a1 -> call_kind -> 'a1
564
565val call_kind_rect_Type3 : 'a1 -> 'a1 -> call_kind -> 'a1
566
567val call_kind_rect_Type2 : 'a1 -> 'a1 -> call_kind -> 'a1
568
569val call_kind_rect_Type1 : 'a1 -> 'a1 -> call_kind -> 'a1
570
571val call_kind_rect_Type0 : 'a1 -> 'a1 -> call_kind -> 'a1
572
573val call_kind_inv_rect_Type4 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
574
575val call_kind_inv_rect_Type3 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
576
577val call_kind_inv_rect_Type2 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
578
579val call_kind_inv_rect_Type1 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
580
581val call_kind_inv_rect_Type0 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
582
583val call_kind_discr : call_kind -> call_kind -> __
584
585val call_kind_jmdiscr : call_kind -> call_kind -> __
586
587val kind_of_call :
588  Joint.unserialized_params -> (AST.ident, (__, __) Types.prod) Types.sum ->
589  call_kind
590
591type 'f sem_unserialized_params = { st_pars : sem_state_params;
592                                    acca_store_ : (__ -> ByteValues.beval ->
593                                                  __ -> __ Errors.res);
594                                    acca_retrieve_ : (__ -> __ ->
595                                                     ByteValues.beval
596                                                     Errors.res);
597                                    acca_arg_retrieve_ : (__ -> __ ->
598                                                         ByteValues.beval
599                                                         Errors.res);
600                                    accb_store_ : (__ -> ByteValues.beval ->
601                                                  __ -> __ Errors.res);
602                                    accb_retrieve_ : (__ -> __ ->
603                                                     ByteValues.beval
604                                                     Errors.res);
605                                    accb_arg_retrieve_ : (__ -> __ ->
606                                                         ByteValues.beval
607                                                         Errors.res);
608                                    dpl_store_ : (__ -> ByteValues.beval ->
609                                                 __ -> __ Errors.res);
610                                    dpl_retrieve_ : (__ -> __ ->
611                                                    ByteValues.beval
612                                                    Errors.res);
613                                    dpl_arg_retrieve_ : (__ -> __ ->
614                                                        ByteValues.beval
615                                                        Errors.res);
616                                    dph_store_ : (__ -> ByteValues.beval ->
617                                                 __ -> __ Errors.res);
618                                    dph_retrieve_ : (__ -> __ ->
619                                                    ByteValues.beval
620                                                    Errors.res);
621                                    dph_arg_retrieve_ : (__ -> __ ->
622                                                        ByteValues.beval
623                                                        Errors.res);
624                                    snd_arg_retrieve_ : (__ -> __ ->
625                                                        ByteValues.beval
626                                                        Errors.res);
627                                    pair_reg_move_ : (__ -> __ -> __
628                                                     Errors.res);
629                                    save_frame : (call_kind -> __ -> state_pc
630                                                 -> state Errors.res);
631                                    setup_call : (Nat.nat -> __ -> __ ->
632                                                 state -> state Errors.res);
633                                    fetch_external_args : (AST.external_function
634                                                          -> state -> __ ->
635                                                          Values.val0
636                                                          List.list
637                                                          Errors.res);
638                                    set_result : (Values.val0 List.list -> __
639                                                 -> state -> state
640                                                 Errors.res);
641                                    call_args_for_main : __;
642                                    call_dest_for_main : __;
643                                    read_result : (AST.ident List.list -> 'f
644                                                  AST.fundef
645                                                  Globalenvs.genv_t -> __ ->
646                                                  state -> ByteValues.beval
647                                                  List.list Errors.res);
648                                    eval_ext_seq : (AST.ident List.list -> 'f
649                                                   genv_gen -> __ ->
650                                                   AST.ident -> state ->
651                                                   state Errors.res);
652                                    pop_frame : (AST.ident List.list -> 'f
653                                                genv_gen -> AST.ident -> __
654                                                -> state -> (state,
655                                                ByteValues.program_counter)
656                                                Types.prod Errors.res) }
657
658val sem_unserialized_params_rect_Type4 :
659  Joint.unserialized_params -> (sem_state_params -> (__ -> 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 -> __ -> __
664  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
665  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
666  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
667  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
668  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
669  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
670  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
671  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
672  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
673  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
674  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
675  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
676  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
677  sem_unserialized_params -> 'a2
678
679val sem_unserialized_params_rect_Type5 :
680  Joint.unserialized_params -> (sem_state_params -> (__ -> 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 -> __ -> __
685  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
686  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
687  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
688  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
689  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
690  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
691  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
692  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
693  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
694  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
695  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
696  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
697  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
698  sem_unserialized_params -> 'a2
699
700val sem_unserialized_params_rect_Type3 :
701  Joint.unserialized_params -> (sem_state_params -> (__ -> 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 -> __ -> __
706  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
707  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
708  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
709  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
710  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
711  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
712  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
713  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
714  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
715  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
716  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
717  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
718  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
719  sem_unserialized_params -> 'a2
720
721val sem_unserialized_params_rect_Type2 :
722  Joint.unserialized_params -> (sem_state_params -> (__ -> 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 -> __ -> __
727  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
728  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
729  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
730  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
731  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
732  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
733  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
734  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
735  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
736  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
737  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
738  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
739  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
740  sem_unserialized_params -> 'a2
741
742val sem_unserialized_params_rect_Type1 :
743  Joint.unserialized_params -> (sem_state_params -> (__ -> 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 -> __ -> __
748  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
749  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
750  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
751  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
752  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
753  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
754  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
755  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
756  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
757  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
758  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
759  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
760  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
761  sem_unserialized_params -> 'a2
762
763val sem_unserialized_params_rect_Type0 :
764  Joint.unserialized_params -> (sem_state_params -> (__ -> 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 -> __ -> __
769  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
770  ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __
771  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ ->
772  ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res)
773  -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state
774  Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
775  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
776  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
777  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
778  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
779  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
780  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
781  ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1
782  sem_unserialized_params -> 'a2
783
784val st_pars :
785  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
786  sem_state_params
787
788val acca_store_ :
789  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
790  ByteValues.beval -> __ -> __ Errors.res
791
792val acca_retrieve_ :
793  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
794  ByteValues.beval Errors.res
795
796val acca_arg_retrieve_ :
797  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
798  ByteValues.beval Errors.res
799
800val accb_store_ :
801  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
802  ByteValues.beval -> __ -> __ Errors.res
803
804val accb_retrieve_ :
805  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
806  ByteValues.beval Errors.res
807
808val accb_arg_retrieve_ :
809  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
810  ByteValues.beval Errors.res
811
812val dpl_store_ :
813  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
814  ByteValues.beval -> __ -> __ Errors.res
815
816val dpl_retrieve_ :
817  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
818  ByteValues.beval Errors.res
819
820val dpl_arg_retrieve_ :
821  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
822  ByteValues.beval Errors.res
823
824val dph_store_ :
825  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
826  ByteValues.beval -> __ -> __ Errors.res
827
828val dph_retrieve_ :
829  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
830  ByteValues.beval Errors.res
831
832val dph_arg_retrieve_ :
833  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
834  ByteValues.beval Errors.res
835
836val snd_arg_retrieve_ :
837  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ ->
838  ByteValues.beval Errors.res
839
840val pair_reg_move_ :
841  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> __
842  Errors.res
843
844val save_frame :
845  Joint.unserialized_params -> 'a1 sem_unserialized_params -> call_kind -> __
846  -> state_pc -> state Errors.res
847
848val setup_call :
849  Joint.unserialized_params -> 'a1 sem_unserialized_params -> Nat.nat -> __
850  -> __ -> state -> state Errors.res
851
852val fetch_external_args :
853  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
854  AST.external_function -> state -> __ -> Values.val0 List.list Errors.res
855
856val set_result :
857  Joint.unserialized_params -> 'a1 sem_unserialized_params -> Values.val0
858  List.list -> __ -> state -> state Errors.res
859
860val call_args_for_main :
861  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __
862
863val call_dest_for_main :
864  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __
865
866val read_result :
867  Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
868  List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state ->
869  ByteValues.beval List.list Errors.res
870
871val eval_ext_seq :
872  Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
873  List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res
874
875val pop_frame :
876  Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident
877  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
878  ByteValues.program_counter) Types.prod Errors.res
879
880val sem_unserialized_params_inv_rect_Type4 :
881  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
882  (sem_state_params -> (__ -> 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  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
888  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
889  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
890  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
891  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
892  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
893  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
894  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
895  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
896  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
897  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
898  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
899  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
900
901val sem_unserialized_params_inv_rect_Type3 :
902  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
903  (sem_state_params -> (__ -> 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  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
909  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
910  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
911  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
912  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
913  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
914  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
915  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
916  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
917  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
918  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
919  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
920  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
921
922val sem_unserialized_params_inv_rect_Type2 :
923  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
924  (sem_state_params -> (__ -> 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  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
930  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
931  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
932  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
933  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
934  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
935  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
936  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
937  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
938  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
939  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
940  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
941  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
942
943val sem_unserialized_params_inv_rect_Type1 :
944  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
945  (sem_state_params -> (__ -> 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  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
951  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
952  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
953  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
954  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
955  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
956  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
957  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
958  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
959  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
960  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
961  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
962  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
963
964val sem_unserialized_params_inv_rect_Type0 :
965  Joint.unserialized_params -> 'a1 sem_unserialized_params ->
966  (sem_state_params -> (__ -> 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  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
972  Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __
973  -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval
974  Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __
975  Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) ->
976  (Nat.nat -> __ -> __ -> state -> state Errors.res) ->
977  (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res)
978  -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __
979  -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state
980  -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1
981  genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident
982  List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state,
983  ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2
984
985val sem_unserialized_params_jmdiscr :
986  Joint.unserialized_params -> 'a1 sem_unserialized_params -> 'a1
987  sem_unserialized_params -> __
988
989val helper_def_retrieve :
990  (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> __ -> 'a1
991  -> ByteValues.beval Errors.res) -> Joint.unserialized_params -> 'a2
992  sem_unserialized_params -> state -> 'a1 -> ByteValues.beval Errors.res
993
994val helper_def_store :
995  (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> 'a1 ->
996  ByteValues.beval -> __ -> __ Errors.res) -> Joint.unserialized_params ->
997  'a2 sem_unserialized_params -> 'a1 -> ByteValues.beval -> state -> state
998  Errors.res
999
1000val acca_retrieve :
1001  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1002  ByteValues.beval Errors.res
1003
1004val acca_store :
1005  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1006  ByteValues.beval -> state -> state Errors.res
1007
1008val acca_arg_retrieve :
1009  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1010  ByteValues.beval Errors.res
1011
1012val accb_store :
1013  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1014  ByteValues.beval -> state -> state Errors.res
1015
1016val accb_retrieve :
1017  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1018  ByteValues.beval Errors.res
1019
1020val accb_arg_retrieve :
1021  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1022  ByteValues.beval Errors.res
1023
1024val dpl_store :
1025  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1026  ByteValues.beval -> state -> state Errors.res
1027
1028val dpl_retrieve :
1029  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1030  ByteValues.beval Errors.res
1031
1032val dpl_arg_retrieve :
1033  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1034  ByteValues.beval Errors.res
1035
1036val dph_store :
1037  Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ ->
1038  ByteValues.beval -> state -> state Errors.res
1039
1040val dph_retrieve :
1041  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1042  ByteValues.beval Errors.res
1043
1044val dph_arg_retrieve :
1045  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1046  ByteValues.beval Errors.res
1047
1048val snd_arg_retrieve :
1049  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1050  ByteValues.beval Errors.res
1051
1052val pair_reg_move :
1053  Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ ->
1054  __
1055
1056val push : sem_state_params -> state -> ByteValues.beval -> state Errors.res
1057
1058val pop :
1059  sem_state_params -> state -> (ByteValues.beval, state) Types.prod
1060  Errors.res
1061
1062val push_ra :
1063  sem_state_params -> state -> ByteValues.program_counter -> state Errors.res
1064
1065val pop_ra :
1066  sem_state_params -> state -> (state, ByteValues.program_counter) Types.prod
1067  Errors.res
1068
1069type serialized_params = { spp : Joint.params;
1070                           msu_pars : Joint.joint_closed_internal_function
1071                                      sem_unserialized_params;
1072                           offset_of_point : (__ -> Positive.pos);
1073                           point_of_offset : (Positive.pos -> __) }
1074
1075val serialized_params_rect_Type4 :
1076  (Joint.params -> Joint.joint_closed_internal_function
1077  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1078  __ -> __ -> 'a1) -> serialized_params -> 'a1
1079
1080val serialized_params_rect_Type5 :
1081  (Joint.params -> Joint.joint_closed_internal_function
1082  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1083  __ -> __ -> 'a1) -> serialized_params -> 'a1
1084
1085val serialized_params_rect_Type3 :
1086  (Joint.params -> Joint.joint_closed_internal_function
1087  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1088  __ -> __ -> 'a1) -> serialized_params -> 'a1
1089
1090val serialized_params_rect_Type2 :
1091  (Joint.params -> Joint.joint_closed_internal_function
1092  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1093  __ -> __ -> 'a1) -> serialized_params -> 'a1
1094
1095val serialized_params_rect_Type1 :
1096  (Joint.params -> Joint.joint_closed_internal_function
1097  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1098  __ -> __ -> 'a1) -> serialized_params -> 'a1
1099
1100val serialized_params_rect_Type0 :
1101  (Joint.params -> Joint.joint_closed_internal_function
1102  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1103  __ -> __ -> 'a1) -> serialized_params -> 'a1
1104
1105val spp : serialized_params -> Joint.params
1106
1107val msu_pars :
1108  serialized_params -> Joint.joint_closed_internal_function
1109  sem_unserialized_params
1110
1111val offset_of_point : serialized_params -> __ -> Positive.pos
1112
1113val point_of_offset : serialized_params -> Positive.pos -> __
1114
1115val serialized_params_inv_rect_Type4 :
1116  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1117  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1118  __ -> __ -> __ -> 'a1) -> 'a1
1119
1120val serialized_params_inv_rect_Type3 :
1121  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1122  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1123  __ -> __ -> __ -> 'a1) -> 'a1
1124
1125val serialized_params_inv_rect_Type2 :
1126  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1127  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1128  __ -> __ -> __ -> 'a1) -> 'a1
1129
1130val serialized_params_inv_rect_Type1 :
1131  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1132  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1133  __ -> __ -> __ -> 'a1) -> 'a1
1134
1135val serialized_params_inv_rect_Type0 :
1136  serialized_params -> (Joint.params -> Joint.joint_closed_internal_function
1137  sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) ->
1138  __ -> __ -> __ -> 'a1) -> 'a1
1139
1140val serialized_params_jmdiscr : serialized_params -> serialized_params -> __
1141
1142val spp__o__stmt_pars : serialized_params -> Joint.stmt_params
1143
1144val spp__o__stmt_pars__o__uns_pars : serialized_params -> Joint.uns_params
1145
1146val spp__o__stmt_pars__o__uns_pars__o__u_pars :
1147  serialized_params -> Joint.unserialized_params
1148
1149val msu_pars__o__st_pars : serialized_params -> sem_state_params
1150
1151type sem_params = { spp' : serialized_params;
1152                    pre_main_generator : (Joint.joint_program ->
1153                                         Joint.joint_closed_internal_function) }
1154
1155val sem_params_rect_Type4 :
1156  (serialized_params -> (Joint.joint_program ->
1157  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1158
1159val sem_params_rect_Type5 :
1160  (serialized_params -> (Joint.joint_program ->
1161  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1162
1163val sem_params_rect_Type3 :
1164  (serialized_params -> (Joint.joint_program ->
1165  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1166
1167val sem_params_rect_Type2 :
1168  (serialized_params -> (Joint.joint_program ->
1169  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1170
1171val sem_params_rect_Type1 :
1172  (serialized_params -> (Joint.joint_program ->
1173  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1174
1175val sem_params_rect_Type0 :
1176  (serialized_params -> (Joint.joint_program ->
1177  Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1
1178
1179val spp' : sem_params -> serialized_params
1180
1181val pre_main_generator :
1182  sem_params -> Joint.joint_program -> Joint.joint_closed_internal_function
1183
1184val sem_params_inv_rect_Type4 :
1185  sem_params -> (serialized_params -> (Joint.joint_program ->
1186  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1187
1188val sem_params_inv_rect_Type3 :
1189  sem_params -> (serialized_params -> (Joint.joint_program ->
1190  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1191
1192val sem_params_inv_rect_Type2 :
1193  sem_params -> (serialized_params -> (Joint.joint_program ->
1194  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1195
1196val sem_params_inv_rect_Type1 :
1197  sem_params -> (serialized_params -> (Joint.joint_program ->
1198  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1199
1200val sem_params_inv_rect_Type0 :
1201  sem_params -> (serialized_params -> (Joint.joint_program ->
1202  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
1203
1204val sem_params_jmdiscr : sem_params -> sem_params -> __
1205
1206val spp'__o__msu_pars :
1207  sem_params -> Joint.joint_closed_internal_function sem_unserialized_params
1208
1209val spp'__o__msu_pars__o__st_pars : sem_params -> sem_state_params
1210
1211val spp'__o__spp : sem_params -> Joint.params
1212
1213val spp'__o__spp__o__stmt_pars : sem_params -> Joint.stmt_params
1214
1215val spp'__o__spp__o__stmt_pars__o__uns_pars : sem_params -> Joint.uns_params
1216
1217val spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
1218  sem_params -> Joint.unserialized_params
1219
1220val pc_of_point :
1221  sem_params -> Pointers.block Types.sig0 -> __ -> ByteValues.program_counter
1222
1223val point_of_pc : sem_params -> ByteValues.program_counter -> __
1224
1225val fetch_statement :
1226  sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter ->
1227  ((AST.ident, Joint.joint_closed_internal_function) Types.prod,
1228  Joint.joint_statement) Types.prod Errors.res
1229
1230val pc_of_label :
1231  sem_params -> AST.ident List.list -> genv -> Pointers.block Types.sig0 ->
1232  Graphs.label -> ByteValues.program_counter Errors.res
1233
1234val succ_pc :
1235  sem_params -> ByteValues.program_counter -> __ ->
1236  ByteValues.program_counter
1237
1238val goto :
1239  sem_params -> AST.ident List.list -> genv -> Graphs.label -> state_pc ->
1240  state_pc Errors.res
1241
1242val next : sem_params -> __ -> state_pc -> state_pc
1243
1244val next_of_call_pc :
1245  sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter ->
1246  __ Errors.res
1247
1248val eval_seq_no_pc :
1249  sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_seq
1250  -> state -> state Errors.res
1251
1252val block_of_call :
1253  sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
1254  (__, __) Types.prod) Types.sum -> state -> __
1255
1256val eval_external_call :
1257  sem_params -> AST.external_function -> __ -> __ -> state -> __
1258
1259val increment_stack_usage : sem_state_params -> Nat.nat -> state -> state
1260
1261val decrement_stack_usage : sem_state_params -> Nat.nat -> state -> state
1262
1263val eval_internal_call :
1264  sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
1265  Joint.joint_internal_function -> __ -> state -> __
1266
1267val is_inl : ('a1, 'a2) Types.sum -> Bool.bool
1268
1269val eval_call :
1270  sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
1271  (__, __) Types.prod) Types.sum -> __ -> __ -> __ -> state_pc -> __
1272
1273val eval_statement_no_pc :
1274  sem_params -> AST.ident List.list -> genv -> AST.ident ->
1275  Joint.joint_statement -> state -> state Errors.res
1276
1277val eval_return :
1278  sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
1279  __ -> state -> __
1280
1281val eval_tailcall :
1282  sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
1283  (__, __) Types.prod) Types.sum -> __ -> PreIdentifiers.identifier -> __ ->
1284  state_pc -> __
1285
1286val eval_statement_advance :
1287  sem_params -> AST.ident List.list -> genv -> AST.ident ->
1288  Joint.joint_closed_internal_function -> Joint.joint_statement -> state_pc
1289  -> (IO.io_out, IO.io_in, state_pc) IOMonad.iO
1290
1291val eval_state :
1292  sem_params -> AST.ident List.list -> genv -> state_pc -> (IO.io_out,
1293  IO.io_in, state_pc) IOMonad.iO
1294
Note: See TracBrowser for help on using the repository browser.