source: extracted/toRTLabs.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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