source: extracted/toRTLabs.mli @ 2746

Last change on this file since 2746 was 2717, checked in by sacerdot, 7 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
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 BitVectorTrie
98
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.