source: extracted/translateUtils.mli @ 2890

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

Pretty printing of the LTL program.

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