source: extracted/translateUtils.mli @ 2717

Last change on this file since 2717 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: 13.9 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open Graphs
12
13open I8051
14
15open Order
16
17open Registers
18
19open BitVectorTrie
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 Setoids
40
41open Monad
42
43open Option
44
45open Lists
46
47open Identifiers
48
49open Integers
50
51open AST
52
53open Division
54
55open Exp
56
57open Arithmetic
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
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
159type b_graph_translate_data = { init_ret : __; init_params : __;
160                                init_stack_size : Nat.nat;
161                                added_prologue : Joint.joint_seq List.list;
162                                f_step : (Graphs.label -> Joint.joint_step ->
163                                         Blocks.bind_step_block);
164                                f_fin : (Graphs.label -> Joint.joint_fin_step
165                                        -> Blocks.bind_fin_block) }
166
167val b_graph_translate_data_rect_Type4 :
168  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
169  __ -> Nat.nat -> Joint.joint_seq List.list -> (Graphs.label ->
170  Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
171  Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> 'a1) ->
172  b_graph_translate_data -> 'a1
173
174val b_graph_translate_data_rect_Type5 :
175  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
176  __ -> Nat.nat -> Joint.joint_seq List.list -> (Graphs.label ->
177  Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
178  Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> 'a1) ->
179  b_graph_translate_data -> 'a1
180
181val b_graph_translate_data_rect_Type3 :
182  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
183  __ -> Nat.nat -> Joint.joint_seq List.list -> (Graphs.label ->
184  Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
185  Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> 'a1) ->
186  b_graph_translate_data -> 'a1
187
188val b_graph_translate_data_rect_Type2 :
189  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
190  __ -> Nat.nat -> Joint.joint_seq List.list -> (Graphs.label ->
191  Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
192  Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> 'a1) ->
193  b_graph_translate_data -> 'a1
194
195val b_graph_translate_data_rect_Type1 :
196  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
197  __ -> Nat.nat -> Joint.joint_seq List.list -> (Graphs.label ->
198  Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
199  Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> 'a1) ->
200  b_graph_translate_data -> 'a1
201
202val b_graph_translate_data_rect_Type0 :
203  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
204  __ -> Nat.nat -> Joint.joint_seq List.list -> (Graphs.label ->
205  Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
206  Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> 'a1) ->
207  b_graph_translate_data -> 'a1
208
209val init_ret :
210  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
211  b_graph_translate_data -> __
212
213val init_params :
214  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
215  b_graph_translate_data -> __
216
217val init_stack_size :
218  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
219  b_graph_translate_data -> Nat.nat
220
221val added_prologue :
222  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
223  b_graph_translate_data -> Joint.joint_seq List.list
224
225val f_step :
226  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
227  b_graph_translate_data -> Graphs.label -> Joint.joint_step ->
228  Blocks.bind_step_block
229
230val f_fin :
231  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
232  b_graph_translate_data -> Graphs.label -> Joint.joint_fin_step ->
233  Blocks.bind_fin_block
234
235val b_graph_translate_data_inv_rect_Type4 :
236  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
237  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
238  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
239  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
240  -> __ -> __ -> 'a1) -> 'a1
241
242val b_graph_translate_data_inv_rect_Type3 :
243  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
244  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
245  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
246  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
247  -> __ -> __ -> 'a1) -> 'a1
248
249val b_graph_translate_data_inv_rect_Type2 :
250  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
251  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
252  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
253  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
254  -> __ -> __ -> 'a1) -> 'a1
255
256val b_graph_translate_data_inv_rect_Type1 :
257  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
258  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
259  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
260  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
261  -> __ -> __ -> 'a1) -> 'a1
262
263val b_graph_translate_data_inv_rect_Type0 :
264  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
265  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
266  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
267  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
268  -> __ -> __ -> 'a1) -> 'a1
269
270val b_graph_translate_data_jmdiscr :
271  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
272  b_graph_translate_data -> b_graph_translate_data -> __
273
274val get_first_costlabel :
275  Joint.params -> AST.ident List.list -> Joint.joint_closed_internal_function
276  -> (CostLabel.costlabel, __) Types.prod
277
278val b_graph_translate_props_rect_Type4 :
279  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
280  b_graph_translate_data -> Registers.register List.list ->
281  Joint.joint_closed_internal_function ->
282  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
283  List.list Types.option) -> (Graphs.label -> Registers.register List.list
284  Types.option) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
285  -> __ -> 'a1) -> 'a1
286
287val b_graph_translate_props_rect_Type5 :
288  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
289  b_graph_translate_data -> Registers.register List.list ->
290  Joint.joint_closed_internal_function ->
291  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
292  List.list Types.option) -> (Graphs.label -> Registers.register List.list
293  Types.option) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
294  -> __ -> 'a1) -> 'a1
295
296val b_graph_translate_props_rect_Type3 :
297  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
298  b_graph_translate_data -> Registers.register List.list ->
299  Joint.joint_closed_internal_function ->
300  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
301  List.list Types.option) -> (Graphs.label -> Registers.register List.list
302  Types.option) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
303  -> __ -> 'a1) -> 'a1
304
305val b_graph_translate_props_rect_Type2 :
306  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
307  b_graph_translate_data -> Registers.register List.list ->
308  Joint.joint_closed_internal_function ->
309  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
310  List.list Types.option) -> (Graphs.label -> Registers.register List.list
311  Types.option) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
312  -> __ -> 'a1) -> 'a1
313
314val b_graph_translate_props_rect_Type1 :
315  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
316  b_graph_translate_data -> Registers.register List.list ->
317  Joint.joint_closed_internal_function ->
318  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
319  List.list Types.option) -> (Graphs.label -> Registers.register List.list
320  Types.option) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
321  -> __ -> 'a1) -> 'a1
322
323val b_graph_translate_props_rect_Type0 :
324  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
325  b_graph_translate_data -> Registers.register List.list ->
326  Joint.joint_closed_internal_function ->
327  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
328  List.list Types.option) -> (Graphs.label -> Registers.register List.list
329  Types.option) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
330  -> __ -> 'a1) -> 'a1
331
332val b_graph_translate_props_inv_rect_Type4 :
333  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
334  b_graph_translate_data -> Registers.register List.list ->
335  Joint.joint_closed_internal_function ->
336  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
337  List.list Types.option) -> (Graphs.label -> Registers.register List.list
338  Types.option) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
339  -> __ -> __ -> 'a1) -> 'a1
340
341val b_graph_translate_props_inv_rect_Type3 :
342  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
343  b_graph_translate_data -> Registers.register List.list ->
344  Joint.joint_closed_internal_function ->
345  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
346  List.list Types.option) -> (Graphs.label -> Registers.register List.list
347  Types.option) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
348  -> __ -> __ -> 'a1) -> 'a1
349
350val b_graph_translate_props_inv_rect_Type2 :
351  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
352  b_graph_translate_data -> Registers.register List.list ->
353  Joint.joint_closed_internal_function ->
354  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
355  List.list Types.option) -> (Graphs.label -> Registers.register List.list
356  Types.option) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
357  -> __ -> __ -> 'a1) -> 'a1
358
359val b_graph_translate_props_inv_rect_Type1 :
360  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
361  b_graph_translate_data -> Registers.register List.list ->
362  Joint.joint_closed_internal_function ->
363  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
364  List.list Types.option) -> (Graphs.label -> Registers.register List.list
365  Types.option) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
366  -> __ -> __ -> 'a1) -> 'a1
367
368val b_graph_translate_props_inv_rect_Type0 :
369  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
370  b_graph_translate_data -> Registers.register List.list ->
371  Joint.joint_closed_internal_function ->
372  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
373  List.list Types.option) -> (Graphs.label -> Registers.register List.list
374  Types.option) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
375  -> __ -> __ -> 'a1) -> 'a1
376
377val b_graph_translate_props_jmdiscr :
378  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
379  b_graph_translate_data -> Registers.register List.list ->
380  Joint.joint_closed_internal_function ->
381  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
382  List.list Types.option) -> (Graphs.label -> Registers.register List.list
383  Types.option) -> __
384
385val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod
386
387val b_graph_translate :
388  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
389  (Registers.register, b_graph_translate_data) Bind_new.bind_new ->
390  Joint.joint_closed_internal_function ->
391  Joint.joint_closed_internal_function Types.sig0
392
393val b_graph_transform_program :
394  Joint.graph_params -> Joint.graph_params -> (AST.ident List.list ->
395  Joint.joint_closed_internal_function -> (Registers.register,
396  b_graph_translate_data) Bind_new.bind_new) -> Joint.joint_program ->
397  Joint.joint_program
398
399val added_registers :
400  Joint.graph_params -> AST.ident List.list -> Joint.joint_internal_function
401  -> (Graphs.label -> Registers.register List.list Types.option) ->
402  Registers.register List.list
403
Note: See TracBrowser for help on using the repository browser.