source: extracted/toRTLabs.mli @ 2731

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 22.1 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
[2717]97open BitVectorTrie
98
[2601]99open CostLabel
100
101open FrontEndOps
102
103open Cminor_syntax
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) -> partial_fn ->
287  '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) -> partial_fn ->
296  '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) -> partial_fn ->
305  '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) -> partial_fn ->
314  '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) -> partial_fn ->
323  '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) -> partial_fn ->
332  '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) -> 'a1
367
368val partial_fn_inv_rect_Type3 :
369  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
370  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
371  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
372  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
373  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
374  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1
375
376val partial_fn_inv_rect_Type2 :
377  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
378  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
379  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
380  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
381  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
382  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1
383
384val partial_fn_inv_rect_Type1 :
385  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
386  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
387  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
388  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
389  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
390  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1
391
392val partial_fn_inv_rect_Type0 :
393  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
394  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
395  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
396  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
397  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
398  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1
399
400val partial_fn_jmdiscr : fixed -> partial_fn -> partial_fn -> __
401
402val fn_contains_rect_Type4 :
403  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
404
405val fn_contains_rect_Type5 :
406  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
407
408val fn_contains_rect_Type3 :
409  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
410
411val fn_contains_rect_Type2 :
412  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
413
414val fn_contains_rect_Type1 :
415  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
416
417val fn_contains_rect_Type0 :
418  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
419
420val fn_contains_inv_rect_Type4 :
421  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
422
423val fn_contains_inv_rect_Type3 :
424  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
425
426val fn_contains_inv_rect_Type2 :
427  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
428
429val fn_contains_inv_rect_Type1 :
430  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
431
432val fn_contains_inv_rect_Type0 :
433  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
434
435val fn_contains_discr : fixed -> partial_fn -> partial_fn -> __
436
437val fn_contains_jmdiscr : fixed -> partial_fn -> partial_fn -> __
438
439val fill_in_statement :
440  fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
441  partial_fn Types.sig0
442
443val add_to_graph :
444  fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
445  partial_fn Types.sig0
446
447val change_entry :
448  fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0
449
450val add_fresh_to_graph :
451  fixed -> (Graphs.label -> RTLabs_syntax.statement) -> partial_fn ->
452  partial_fn Types.sig0
453
454val fresh_reg :
455  fixed -> partial_fn -> AST.typ -> (partial_fn Types.sig0,
456  Registers.register Types.sig0) Types.dPair
457
458val choose_reg :
459  fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> (partial_fn
460  Types.sig0, Registers.register Types.sig0) Types.dPair
461
462val foldr_all : ('a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2
463
464val foldr_all' :
465  ('a1 -> __ -> 'a1 List.list -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2
466
467val eject' : ('a1, 'a2) Types.dPair -> 'a1
468
469val choose_regs :
470  fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list -> partial_fn
471  -> (partial_fn Types.sig0, Registers.register List.list Types.sig0)
472  Types.dPair
473
474val add_stmt_inv_rect_Type4 :
475  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
476  'a1) -> 'a1
477
478val add_stmt_inv_rect_Type5 :
479  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
480  'a1) -> 'a1
481
482val add_stmt_inv_rect_Type3 :
483  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
484  'a1) -> 'a1
485
486val add_stmt_inv_rect_Type2 :
487  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
488  'a1) -> 'a1
489
490val add_stmt_inv_rect_Type1 :
491  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
492  'a1) -> 'a1
493
494val add_stmt_inv_rect_Type0 :
495  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
496  'a1) -> 'a1
497
498val add_stmt_inv_inv_rect_Type4 :
499  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
500  -> 'a1) -> 'a1
501
502val add_stmt_inv_inv_rect_Type3 :
503  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
504  -> 'a1) -> 'a1
505
506val add_stmt_inv_inv_rect_Type2 :
507  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
508  -> 'a1) -> 'a1
509
510val add_stmt_inv_inv_rect_Type1 :
511  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
512  -> 'a1) -> 'a1
513
514val add_stmt_inv_inv_rect_Type0 :
515  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
516  -> 'a1) -> 'a1
517
518val add_stmt_inv_discr :
519  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __
520
521val add_stmt_inv_jmdiscr :
522  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __
523
524type fn_con_because =
525| Fn_con_eq of partial_fn
526| Fn_con_sig of partial_fn * partial_fn * partial_fn Types.sig0
527| Fn_con_addinv of partial_fn * partial_fn * Cminor_syntax.stmt
528   * partial_fn Types.sig0
529
530val fn_con_because_rect_Type4 :
531  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
532  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
533  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
534  fn_con_because -> 'a1
535
536val fn_con_because_rect_Type5 :
537  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
538  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
539  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
540  fn_con_because -> 'a1
541
542val fn_con_because_rect_Type3 :
543  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
544  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
545  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
546  fn_con_because -> 'a1
547
548val fn_con_because_rect_Type2 :
549  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
550  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
551  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
552  fn_con_because -> 'a1
553
554val fn_con_because_rect_Type1 :
555  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
556  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
557  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
558  fn_con_because -> 'a1
559
560val fn_con_because_rect_Type0 :
561  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
562  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
563  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
564  fn_con_because -> 'a1
565
566val fn_con_because_inv_rect_Type4 :
567  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
568  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
569  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
570  Types.sig0 -> __ -> __ -> 'a1) -> 'a1
571
572val fn_con_because_inv_rect_Type3 :
573  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
574  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
575  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
576  Types.sig0 -> __ -> __ -> 'a1) -> 'a1
577
578val fn_con_because_inv_rect_Type2 :
579  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
580  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
581  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
582  Types.sig0 -> __ -> __ -> 'a1) -> 'a1
583
584val fn_con_because_inv_rect_Type1 :
585  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
586  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
587  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
588  Types.sig0 -> __ -> __ -> 'a1) -> 'a1
589
590val fn_con_because_inv_rect_Type0 :
591  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
592  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
593  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
594  Types.sig0 -> __ -> __ -> 'a1) -> 'a1
595
596val fn_con_because_discr :
597  fixed -> partial_fn -> fn_con_because -> fn_con_because -> __
598
599val fn_con_because_jmdiscr :
600  fixed -> partial_fn -> fn_con_because -> fn_con_because -> __
601
602val fn_con_because_left : fixed -> partial_fn -> fn_con_because -> partial_fn
603
604val add_expr :
605  fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> Registers.register
606  Types.sig0 -> partial_fn Types.sig0
607
608val add_exprs :
609  fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
610  Registers.register List.list -> partial_fn -> partial_fn Types.sig0
611
612val stmt_inv_rect_Type5 :
613  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
614
615val stmt_inv_rect_Type6 :
616  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
617
618val stmt_inv_rect_Type7 :
619  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
620
621val stmt_inv_rect_Type8 :
622  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
623
624val stmt_inv_rect_Type9 :
625  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
626
627val stmt_inv_rect_Type10 :
628  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
629
630val stmt_inv_inv_rect_Type4 :
631  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
632
633val stmt_inv_inv_rect_Type3 :
634  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
635
636val stmt_inv_inv_rect_Type2 :
637  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
638
639val stmt_inv_inv_rect_Type1 :
640  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
641
642val stmt_inv_inv_rect_Type0 :
643  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
644
645val stmt_inv_discr : fixed -> Cminor_syntax.stmt -> __
646
647val stmt_inv_jmdiscr : fixed -> Cminor_syntax.stmt -> __
648
649val expr_is_Id : AST.typ -> Cminor_syntax.expr -> AST.ident Types.option
650
651val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __
652
653val dPair_jmdiscr : ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __
654
655val add_return :
656  fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.option ->
657  partial_fn -> partial_fn Types.sig0
658
659val record_goto_label :
660  fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn
661
662val add_goto_dummy :
663  fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0
664
665val add_stmt :
666  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn Types.sig0
667
668val patch_gotos : fixed -> partial_fn -> partial_fn Types.sig0
669
670val c2ra_function :
671  Cminor_syntax.internal_function -> RTLabs_syntax.internal_function
672
673val cminor_noinit_to_rtlabs :
674  Cminor_syntax.cminor_noinit_program -> RTLabs_syntax.rTLabs_program
675
676open Initialisation
677
678val cminor_to_rtlabs :
679  CostLabel.costlabel -> Cminor_syntax.cminor_program ->
680  RTLabs_syntax.rTLabs_program
681
Note: See TracBrowser for help on using the repository browser.