source: extracted/toRTLabs.mli @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 8 years ago

...

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