source: extracted/toRTLabs.mli @ 3009

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

New extraction.

File size: 22.0 KB
RevLine 
[2601]1open Preamble
2
3open Setoids
4
5open Monad
6
7open Option
8
9open Div_and_mod
10
11open Jmeq
12
13open Russell
14
15open Util
16
17open Bool
18
19open Relations
20
21open Nat
22
23open Hints_declaration
24
25open Core_notation
26
27open Pts
28
29open Logic
30
31open Types
32
33open List
34
35open Lists
36
37open Extra_bool
38
[2649]39open Coqlib
40
[2601]41open Values
42
43open FrontEndVal
44
45open Hide
46
47open ByteValues
48
49open Division
50
51open Z
52
53open BitVectorZ
54
55open Pointers
56
57open GenMem
58
59open FrontEndMem
60
61open Proper
62
63open PositiveMap
64
65open Deqsets
66
67open Extralib
68
69open Identifiers
70
[2717]71open Exp
72
[2601]73open Arithmetic
74
75open Vector
76
77open FoldStuff
78
79open BitVector
80
81open Extranat
82
83open Integers
84
85open AST
86
[2649]87open ErrorMessages
88
[2601]89open Positive
90
91open PreIdentifiers
92
93open Errors
94
95open Globalenvs
96
97open CostLabel
98
99open FrontEndOps
100
101open Cminor_syntax
102
[2773]103open BitVectorTrie
104
[2601]105open Graphs
106
107open Order
108
109open Registers
110
111open RTLabs_syntax
112
113type env =
114  (Registers.register, AST.typ) Types.prod Identifiers.identifier_map
115
116val populate_env :
117  env -> Identifiers.universe -> (AST.ident, AST.typ) Types.prod List.list ->
118  (((Registers.register, AST.typ) Types.prod List.list, env) Types.prod,
119  Identifiers.universe) Types.prod
120
121val lookup_reg : env -> AST.ident -> AST.typ -> Registers.register
122
123type fixed = { fx_gotos : Identifiers.identifier_set; fx_env : env;
124               fx_rettyp : AST.typ Types.option }
125
126val fixed_rect_Type4 :
127  (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
128  -> 'a1
129
130val fixed_rect_Type5 :
131  (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
132  -> 'a1
133
134val fixed_rect_Type3 :
135  (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
136  -> 'a1
137
138val fixed_rect_Type2 :
139  (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
140  -> 'a1
141
142val fixed_rect_Type1 :
143  (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
144  -> 'a1
145
146val fixed_rect_Type0 :
147  (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
148  -> 'a1
149
150val fx_gotos : fixed -> Identifiers.identifier_set
151
152val fx_env : fixed -> env
153
154val fx_rettyp : fixed -> AST.typ Types.option
155
156val fixed_inv_rect_Type4 :
157  fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
158  -> 'a1) -> 'a1
159
160val fixed_inv_rect_Type3 :
161  fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
162  -> 'a1) -> 'a1
163
164val fixed_inv_rect_Type2 :
165  fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
166  -> 'a1) -> 'a1
167
168val fixed_inv_rect_Type1 :
169  fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
170  -> 'a1) -> 'a1
171
172val fixed_inv_rect_Type0 :
173  fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
174  -> 'a1) -> 'a1
175
176val fixed_discr : fixed -> fixed -> __
177
178val fixed_jmdiscr : fixed -> fixed -> __
179
180type resultok = __
181
182type goto_map =
183  PreIdentifiers.identifier Identifiers.identifier_map
184  (* singleton inductive, whose constructor was mk_goto_map *)
185
186val goto_map_rect_Type4 :
187  fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
188  Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
189
190val goto_map_rect_Type5 :
191  fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
192  Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
193
194val goto_map_rect_Type3 :
195  fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
196  Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
197
198val goto_map_rect_Type2 :
199  fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
200  Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
201
202val goto_map_rect_Type1 :
203  fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
204  Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
205
206val goto_map_rect_Type0 :
207  fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
208  Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
209
210val gm_map :
211  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
212  PreIdentifiers.identifier Identifiers.identifier_map
213
214val goto_map_inv_rect_Type4 :
215  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
216  (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
217  'a1) -> 'a1
218
219val goto_map_inv_rect_Type3 :
220  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
221  (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
222  'a1) -> 'a1
223
224val goto_map_inv_rect_Type2 :
225  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
226  (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
227  'a1) -> 'a1
228
229val goto_map_inv_rect_Type1 :
230  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
231  (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
232  'a1) -> 'a1
233
234val goto_map_inv_rect_Type0 :
235  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
236  (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
237  'a1) -> 'a1
238
239val goto_map_discr :
240  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map -> __
241
242val goto_map_jmdiscr :
243  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map -> __
244
245val dpi1__o__gm_map__o__inject :
246  fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
247  Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map
248  Types.sig0
249
250val eject__o__gm_map__o__inject :
251  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
252  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0
253
254val gm_map__o__inject :
255  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
256  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0
257
258val dpi1__o__gm_map :
259  fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
260  Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map
261
262val eject__o__gm_map :
263  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
264  PreIdentifiers.identifier Identifiers.identifier_map
265
266type partial_fn = { pf_labgen : Identifiers.universe;
267                    pf_reggen : Identifiers.universe;
268                    pf_params : (Registers.register, AST.typ) Types.prod
269                                List.list;
270                    pf_locals : (Registers.register, AST.typ) Types.prod
271                                List.list; pf_result : resultok;
272                    pf_stacksize : Nat.nat;
273                    pf_graph : RTLabs_syntax.statement Graphs.graph;
274                    pf_gotos : goto_map;
275                    pf_labels : PreIdentifiers.identifier
276                                Identifiers.identifier_map Types.sig0;
277                    pf_entry : Graphs.label Types.sig0;
278                    pf_exit : Graphs.label Types.sig0 }
279
280val partial_fn_rect_Type4 :
281  fixed -> (Identifiers.universe -> Identifiers.universe ->
282  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
283  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
284  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
285  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
[2997]286  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
287  partial_fn -> 'a1
[2601]288
289val partial_fn_rect_Type5 :
290  fixed -> (Identifiers.universe -> Identifiers.universe ->
291  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
292  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
293  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
294  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
[2997]295  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
296  partial_fn -> 'a1
[2601]297
298val partial_fn_rect_Type3 :
299  fixed -> (Identifiers.universe -> Identifiers.universe ->
300  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
301  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
302  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
303  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
[2997]304  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
305  partial_fn -> 'a1
[2601]306
307val partial_fn_rect_Type2 :
308  fixed -> (Identifiers.universe -> Identifiers.universe ->
309  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
310  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
311  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
312  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
[2997]313  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
314  partial_fn -> 'a1
[2601]315
316val partial_fn_rect_Type1 :
317  fixed -> (Identifiers.universe -> Identifiers.universe ->
318  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
319  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
320  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
321  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
[2997]322  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
323  partial_fn -> 'a1
[2601]324
325val partial_fn_rect_Type0 :
326  fixed -> (Identifiers.universe -> Identifiers.universe ->
327  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
328  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
329  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
330  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
[2997]331  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
332  partial_fn -> 'a1
[2601]333
334val pf_labgen : fixed -> partial_fn -> Identifiers.universe
335
336val pf_reggen : fixed -> partial_fn -> Identifiers.universe
337
338val pf_params :
339  fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list
340
341val pf_locals :
342  fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list
343
344val pf_result : fixed -> partial_fn -> resultok
345
346val pf_stacksize : fixed -> partial_fn -> Nat.nat
347
348val pf_graph : fixed -> partial_fn -> RTLabs_syntax.statement Graphs.graph
349
350val pf_gotos : fixed -> partial_fn -> goto_map
351
352val pf_labels :
353  fixed -> partial_fn -> PreIdentifiers.identifier Identifiers.identifier_map
354  Types.sig0
355
356val pf_entry : fixed -> partial_fn -> Graphs.label Types.sig0
357
358val pf_exit : fixed -> partial_fn -> Graphs.label Types.sig0
359
360val partial_fn_inv_rect_Type4 :
361  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
362  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
363  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
364  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
365  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
[2997]366  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
367  'a1
[2601]368
369val partial_fn_inv_rect_Type3 :
370  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
371  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
372  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
373  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
374  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
[2997]375  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
376  'a1
[2601]377
378val partial_fn_inv_rect_Type2 :
379  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
380  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
381  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
382  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
383  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
[2997]384  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
385  'a1
[2601]386
387val partial_fn_inv_rect_Type1 :
388  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
389  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
390  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
391  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
392  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
[2997]393  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
394  'a1
[2601]395
396val partial_fn_inv_rect_Type0 :
397  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
398  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
399  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
400  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
401  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
[2997]402  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
403  'a1
[2601]404
405val partial_fn_jmdiscr : fixed -> partial_fn -> partial_fn -> __
406
407val fn_contains_rect_Type4 :
408  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
409
410val fn_contains_rect_Type5 :
411  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
412
413val fn_contains_rect_Type3 :
414  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
415
416val fn_contains_rect_Type2 :
417  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
418
419val fn_contains_rect_Type1 :
420  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
421
422val fn_contains_rect_Type0 :
423  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
424
425val fn_contains_inv_rect_Type4 :
426  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
427
428val fn_contains_inv_rect_Type3 :
429  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
430
431val fn_contains_inv_rect_Type2 :
432  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
433
434val fn_contains_inv_rect_Type1 :
435  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
436
437val fn_contains_inv_rect_Type0 :
438  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
439
440val fn_contains_discr : fixed -> partial_fn -> partial_fn -> __
441
442val fn_contains_jmdiscr : fixed -> partial_fn -> partial_fn -> __
443
444val fill_in_statement :
445  fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
446  partial_fn Types.sig0
447
448val add_to_graph :
449  fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
450  partial_fn Types.sig0
451
452val change_entry :
453  fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0
454
455val add_fresh_to_graph :
456  fixed -> (Graphs.label -> RTLabs_syntax.statement) -> partial_fn ->
457  partial_fn Types.sig0
458
459val fresh_reg :
460  fixed -> partial_fn -> AST.typ -> (partial_fn Types.sig0,
461  Registers.register Types.sig0) Types.dPair
462
463val choose_reg :
464  fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> (partial_fn
465  Types.sig0, Registers.register Types.sig0) Types.dPair
466
467val foldr_all : ('a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2
468
469val foldr_all' :
470  ('a1 -> __ -> 'a1 List.list -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2
471
472val eject' : ('a1, 'a2) Types.dPair -> 'a1
473
474val choose_regs :
475  fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list -> partial_fn
476  -> (partial_fn Types.sig0, Registers.register List.list Types.sig0)
477  Types.dPair
478
479val add_stmt_inv_rect_Type4 :
480  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
481  'a1) -> 'a1
482
483val add_stmt_inv_rect_Type5 :
484  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
485  'a1) -> 'a1
486
487val add_stmt_inv_rect_Type3 :
488  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
489  'a1) -> 'a1
490
491val add_stmt_inv_rect_Type2 :
492  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
493  'a1) -> 'a1
494
495val add_stmt_inv_rect_Type1 :
496  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
497  'a1) -> 'a1
498
499val add_stmt_inv_rect_Type0 :
500  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
501  'a1) -> 'a1
502
503val add_stmt_inv_inv_rect_Type4 :
504  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
505  -> 'a1) -> 'a1
506
507val add_stmt_inv_inv_rect_Type3 :
508  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
509  -> 'a1) -> 'a1
510
511val add_stmt_inv_inv_rect_Type2 :
512  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
513  -> 'a1) -> 'a1
514
515val add_stmt_inv_inv_rect_Type1 :
516  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
517  -> 'a1) -> 'a1
518
519val add_stmt_inv_inv_rect_Type0 :
520  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
521  -> 'a1) -> 'a1
522
523val add_stmt_inv_discr :
524  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __
525
526val add_stmt_inv_jmdiscr :
527  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __
528
529type fn_con_because =
530| Fn_con_eq of partial_fn
531| Fn_con_sig of partial_fn * partial_fn * partial_fn Types.sig0
532| Fn_con_addinv of partial_fn * partial_fn * Cminor_syntax.stmt
533   * partial_fn Types.sig0
534
535val fn_con_because_rect_Type4 :
536  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
537  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
538  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
539  fn_con_because -> 'a1
540
541val fn_con_because_rect_Type5 :
542  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
543  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
544  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
545  fn_con_because -> 'a1
546
547val fn_con_because_rect_Type3 :
548  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
549  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
550  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
551  fn_con_because -> 'a1
552
553val fn_con_because_rect_Type2 :
554  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
555  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
556  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
557  fn_con_because -> 'a1
558
559val fn_con_because_rect_Type1 :
560  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
561  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
562  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
563  fn_con_because -> 'a1
564
565val fn_con_because_rect_Type0 :
566  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
567  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
568  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
569  fn_con_because -> 'a1
570
571val fn_con_because_inv_rect_Type4 :
572  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
573  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
574  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
575  Types.sig0 -> __ -> __ -> 'a1) -> 'a1
576
577val fn_con_because_inv_rect_Type3 :
578  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
579  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
580  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
581  Types.sig0 -> __ -> __ -> 'a1) -> 'a1
582
583val fn_con_because_inv_rect_Type2 :
584  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
585  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
586  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
587  Types.sig0 -> __ -> __ -> 'a1) -> 'a1
588
589val fn_con_because_inv_rect_Type1 :
590  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
591  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
592  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
593  Types.sig0 -> __ -> __ -> 'a1) -> 'a1
594
595val fn_con_because_inv_rect_Type0 :
596  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
597  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
598  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
599  Types.sig0 -> __ -> __ -> 'a1) -> 'a1
600
601val fn_con_because_discr :
602  fixed -> partial_fn -> fn_con_because -> fn_con_because -> __
603
604val fn_con_because_jmdiscr :
605  fixed -> partial_fn -> fn_con_because -> fn_con_because -> __
606
607val fn_con_because_left : fixed -> partial_fn -> fn_con_because -> partial_fn
608
609val add_expr :
610  fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> Registers.register
611  Types.sig0 -> partial_fn Types.sig0
612
613val add_exprs :
614  fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
615  Registers.register List.list -> partial_fn -> partial_fn Types.sig0
616
[2773]617val stmt_inv_rect_Type4 :
[2601]618  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
619
[2773]620val stmt_inv_rect_Type5 :
[2601]621  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
622
[2773]623val stmt_inv_rect_Type3 :
[2601]624  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
625
[2773]626val stmt_inv_rect_Type2 :
[2601]627  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
628
[2773]629val stmt_inv_rect_Type1 :
[2601]630  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
631
[2773]632val stmt_inv_rect_Type0 :
[2601]633  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
634
635val stmt_inv_inv_rect_Type4 :
636  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
637
638val stmt_inv_inv_rect_Type3 :
639  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
640
641val stmt_inv_inv_rect_Type2 :
642  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
643
644val stmt_inv_inv_rect_Type1 :
645  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
646
647val stmt_inv_inv_rect_Type0 :
648  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
649
650val stmt_inv_discr : fixed -> Cminor_syntax.stmt -> __
651
652val stmt_inv_jmdiscr : fixed -> Cminor_syntax.stmt -> __
653
[2951]654val expr_is_cst_ident :
655  AST.typ -> Cminor_syntax.expr -> AST.ident Types.option
[2601]656
657val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __
658
659val dPair_jmdiscr : ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __
660
661val add_return :
662  fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.option ->
663  partial_fn -> partial_fn Types.sig0
664
665val record_goto_label :
666  fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn
667
668val add_goto_dummy :
669  fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0
670
671val add_stmt :
672  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn Types.sig0
673
674val patch_gotos : fixed -> partial_fn -> partial_fn Types.sig0
675
676val c2ra_function :
677  Cminor_syntax.internal_function -> RTLabs_syntax.internal_function
678
679val cminor_to_rtlabs :
[2951]680  Cminor_syntax.cminor_program -> RTLabs_syntax.rTLabs_program
[2601]681
Note: See TracBrowser for help on using the repository browser.