source: driver/extracted/toRTLabs.mli @ 3106

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

New extraction.

File size: 22.0 KB
Line 
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
39open Coqlib
40
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
71open Exp
72
73open Arithmetic
74
75open Vector
76
77open FoldStuff
78
79open BitVector
80
81open Extranat
82
83open Integers
84
85open AST
86
87open ErrorMessages
88
89open Positive
90
91open PreIdentifiers
92
93open Errors
94
95open Globalenvs
96
97open CostLabel
98
99open FrontEndOps
100
101open Cminor_syntax
102
103open BitVectorTrie
104
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 -> __ ->
286  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
287  partial_fn -> 'a1
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 -> __ ->
295  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
296  partial_fn -> 'a1
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 -> __ ->
304  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
305  partial_fn -> 'a1
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 -> __ ->
313  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
314  partial_fn -> 'a1
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 -> __ ->
322  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
323  partial_fn -> 'a1
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 -> __ ->
331  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
332  partial_fn -> 'a1
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 -> __ ->
366  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
367  'a1
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 -> __ ->
375  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
376  'a1
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 -> __ ->
384  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
385  'a1
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 -> __ ->
393  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
394  'a1
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 -> __ ->
402  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
403  'a1
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
617val stmt_inv_rect_Type4 :
618  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
619
620val stmt_inv_rect_Type5 :
621  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
622
623val stmt_inv_rect_Type3 :
624  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
625
626val stmt_inv_rect_Type2 :
627  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
628
629val stmt_inv_rect_Type1 :
630  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
631
632val stmt_inv_rect_Type0 :
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
654val expr_is_cst_ident :
655  AST.typ -> Cminor_syntax.expr -> AST.ident Types.option
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 :
680  Cminor_syntax.cminor_program -> RTLabs_syntax.rTLabs_program
681
Note: See TracBrowser for help on using the repository browser.