source: extracted/joint_semantics.mli @ 2960

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

New extraction, it diverges in RTL execution now.

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