source: driver/extracted/translateUtils.mli @ 3106

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

New extraction after code simplification.

File size: 14.2 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
25open BitVectorTrie
26
27open Graphs
28
29open I8051
30
31open Order
32
33open Registers
34
35open CostLabel
36
37open Hide
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open Div_and_mod
78
79open Jmeq
80
81open Russell
82
83open List
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Types
92
93open Bool
94
95open Relations
96
97open Nat
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Positive
108
109open Z
110
111open BitVectorZ
112
113open Pointers
114
115open ByteValues
116
117open BackEndOps
118
119open Joint
120
121open State
122
123open Bind_new
124
125open BindLists
126
127open Blocks
128
129open Deqsets_extra
130
131val fresh_label :
132  Joint.params -> AST.ident List.list -> Graphs.label
133  Monad.smax_def__o__monad
134
135val fresh_register :
136  Joint.params -> AST.ident List.list -> Registers.register
137  Monad.smax_def__o__monad
138
139val adds_graph_pre :
140  Joint.graph_params -> AST.ident List.list -> (Graphs.label -> 'a1 ->
141  Joint.joint_seq) -> 'a1 List.list -> Graphs.label -> Graphs.label
142  Monad.smax_def__o__monad
143
144val adds_graph_post :
145  Joint.graph_params -> AST.ident List.list -> Joint.joint_seq List.list ->
146  Graphs.label -> Graphs.label Monad.smax_def__o__monad
147
148val adds_graph :
149  Joint.graph_params -> AST.ident List.list -> Blocks.step_block ->
150  Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
151  Joint.joint_internal_function
152
153val fin_adds_graph :
154  Joint.graph_params -> AST.ident List.list -> Blocks.fin_block ->
155  Graphs.label -> Joint.joint_internal_function ->
156  Joint.joint_internal_function
157
158val b_adds_graph :
159  Joint.graph_params -> AST.ident List.list -> Blocks.bind_step_block ->
160  Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
161  Joint.joint_internal_function
162
163val b_fin_adds_graph :
164  Joint.graph_params -> AST.ident List.list -> Blocks.bind_fin_block ->
165  Graphs.label -> Joint.joint_internal_function ->
166  Joint.joint_internal_function
167
168val step_registers :
169  Joint.uns_params -> AST.ident List.list -> Joint.joint_step ->
170  Registers.register List.list
171
172val fin_step_registers :
173  Joint.uns_params -> Joint.joint_fin_step -> Registers.register List.list
174
175type b_graph_translate_data = { init_ret : __; init_params : __;
176                                init_stack_size : Nat.nat;
177                                added_prologue : Joint.joint_seq List.list;
178                                new_regs : Registers.register List.list;
179                                f_step : (Graphs.label -> Joint.joint_step ->
180                                         Blocks.bind_step_block);
181                                f_fin : (Graphs.label -> Joint.joint_fin_step
182                                        -> Blocks.bind_fin_block) }
183
184val b_graph_translate_data_rect_Type4 :
185  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
186  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
187  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
188  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
189  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
190
191val b_graph_translate_data_rect_Type5 :
192  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
193  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
194  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
195  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
196  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
197
198val b_graph_translate_data_rect_Type3 :
199  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
200  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
201  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
202  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
203  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
204
205val b_graph_translate_data_rect_Type2 :
206  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
207  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
208  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
209  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
210  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
211
212val b_graph_translate_data_rect_Type1 :
213  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
214  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
215  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
216  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
217  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
218
219val b_graph_translate_data_rect_Type0 :
220  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
221  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
222  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
223  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
224  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
225
226val init_ret :
227  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
228  b_graph_translate_data -> __
229
230val init_params :
231  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
232  b_graph_translate_data -> __
233
234val init_stack_size :
235  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
236  b_graph_translate_data -> Nat.nat
237
238val added_prologue :
239  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
240  b_graph_translate_data -> Joint.joint_seq List.list
241
242val new_regs :
243  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
244  b_graph_translate_data -> Registers.register List.list
245
246val f_step :
247  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
248  b_graph_translate_data -> Graphs.label -> Joint.joint_step ->
249  Blocks.bind_step_block
250
251val f_fin :
252  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
253  b_graph_translate_data -> Graphs.label -> Joint.joint_fin_step ->
254  Blocks.bind_fin_block
255
256val b_graph_translate_data_inv_rect_Type4 :
257  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
258  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
259  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
260  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
261  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
262
263val b_graph_translate_data_inv_rect_Type3 :
264  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
265  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
266  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
267  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
268  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
269
270val b_graph_translate_data_inv_rect_Type2 :
271  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
272  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
273  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
274  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
275  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
276
277val b_graph_translate_data_inv_rect_Type1 :
278  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
279  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
280  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
281  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
282  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
283
284val b_graph_translate_data_inv_rect_Type0 :
285  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
286  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
287  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
288  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
289  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
290
291val b_graph_translate_data_jmdiscr :
292  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
293  b_graph_translate_data -> b_graph_translate_data -> __
294
295type bound_b_graph_translate_data =
296  (Registers.register, b_graph_translate_data) Bind_new.bind_new Types.sig0
297
298val get_first_costlabel_next :
299  Joint.params -> AST.ident List.list -> Joint.joint_closed_internal_function
300  -> (CostLabel.costlabel, __) Types.prod
301
302val get_first_costlabel :
303  Joint.params -> AST.ident List.list -> Joint.joint_closed_internal_function
304  -> CostLabel.costlabel
305
306val not_emptyb : 'a1 List.list -> Bool.bool
307
308val b_graph_translate_props_rect_Type4 :
309  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
310  b_graph_translate_data -> Joint.joint_closed_internal_function ->
311  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
312  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
313  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
314
315val b_graph_translate_props_rect_Type5 :
316  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
317  b_graph_translate_data -> Joint.joint_closed_internal_function ->
318  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
319  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
320  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
321
322val b_graph_translate_props_rect_Type3 :
323  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
324  b_graph_translate_data -> Joint.joint_closed_internal_function ->
325  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
326  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
327  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
328
329val b_graph_translate_props_rect_Type2 :
330  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
331  b_graph_translate_data -> Joint.joint_closed_internal_function ->
332  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
333  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
334  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
335
336val b_graph_translate_props_rect_Type1 :
337  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
338  b_graph_translate_data -> Joint.joint_closed_internal_function ->
339  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
340  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
341  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
342
343val b_graph_translate_props_rect_Type0 :
344  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
345  b_graph_translate_data -> Joint.joint_closed_internal_function ->
346  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
347  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
348  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
349
350val b_graph_translate_props_inv_rect_Type4 :
351  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
352  b_graph_translate_data -> Joint.joint_closed_internal_function ->
353  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
354  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
355  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
356
357val b_graph_translate_props_inv_rect_Type3 :
358  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
359  b_graph_translate_data -> Joint.joint_closed_internal_function ->
360  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
361  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
362  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
363
364val b_graph_translate_props_inv_rect_Type2 :
365  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
366  b_graph_translate_data -> Joint.joint_closed_internal_function ->
367  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
368  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
369  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
370
371val b_graph_translate_props_inv_rect_Type1 :
372  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
373  b_graph_translate_data -> Joint.joint_closed_internal_function ->
374  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
375  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
376  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
377
378val b_graph_translate_props_inv_rect_Type0 :
379  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
380  b_graph_translate_data -> Joint.joint_closed_internal_function ->
381  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
382  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
383  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
384
385val b_graph_translate_props_jmdiscr :
386  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
387  b_graph_translate_data -> Joint.joint_closed_internal_function ->
388  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
389  List.list) -> (Graphs.label -> Registers.register List.list) -> __
390
391val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod
392
393val set_entry :
394  AST.ident List.list -> Joint.params -> Joint.joint_internal_function -> __
395  -> Joint.joint_internal_function
396
397val b_graph_translate :
398  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
399  bound_b_graph_translate_data -> Joint.joint_closed_internal_function ->
400  Joint.joint_closed_internal_function Types.sig0
401
402val b_graph_transform_program :
403  Joint.graph_params -> Joint.graph_params -> (AST.ident List.list ->
404  Joint.joint_closed_internal_function -> bound_b_graph_translate_data) ->
405  Joint.joint_program -> Joint.joint_program
406
407val added_registers :
408  Joint.graph_params -> AST.ident List.list -> Joint.joint_internal_function
409  -> (Graphs.label -> Registers.register List.list) -> Registers.register
410  List.list
411
Note: See TracBrowser for help on using the repository browser.