source: extracted/eRTLptrToLTL.mli @ 2890

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

Everything extracted again.

File size: 8.6 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 Joint_LTL_LIN
108
109open LTL
110
111open Fixpoints
112
113open Set_adt
114
115open ERTL
116
117open ERTLptr
118
119open Liveness
120
121open Interference
122
123open Deqsets_extra
124
125open State
126
127open Bind_new
128
129open BindLists
130
131open Blocks
132
133open TranslateUtils
134
135val dpi1__o__Reg_to_dec__o__inject :
136  (I8051.register, 'a1) Types.dPair -> Interference.decision Types.sig0
137
138val eject__o__Reg_to_dec__o__inject :
139  I8051.register Types.sig0 -> Interference.decision Types.sig0
140
141val reg_to_dec__o__inject :
142  I8051.register -> Interference.decision Types.sig0
143
144val dpi1__o__Reg_to_dec :
145  (I8051.register, 'a1) Types.dPair -> Interference.decision
146
147val eject__o__Reg_to_dec : I8051.register Types.sig0 -> Interference.decision
148
149type arg_decision =
150| Arg_decision_colour of I8051.register
151| Arg_decision_spill of Nat.nat
152| Arg_decision_imm of BitVector.byte
153
154val arg_decision_rect_Type4 :
155  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
156  arg_decision -> 'a1
157
158val arg_decision_rect_Type5 :
159  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
160  arg_decision -> 'a1
161
162val arg_decision_rect_Type3 :
163  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
164  arg_decision -> 'a1
165
166val arg_decision_rect_Type2 :
167  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
168  arg_decision -> 'a1
169
170val arg_decision_rect_Type1 :
171  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
172  arg_decision -> 'a1
173
174val arg_decision_rect_Type0 :
175  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
176  arg_decision -> 'a1
177
178val arg_decision_inv_rect_Type4 :
179  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
180  (BitVector.byte -> __ -> 'a1) -> 'a1
181
182val arg_decision_inv_rect_Type3 :
183  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
184  (BitVector.byte -> __ -> 'a1) -> 'a1
185
186val arg_decision_inv_rect_Type2 :
187  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
188  (BitVector.byte -> __ -> 'a1) -> 'a1
189
190val arg_decision_inv_rect_Type1 :
191  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
192  (BitVector.byte -> __ -> 'a1) -> 'a1
193
194val arg_decision_inv_rect_Type0 :
195  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
196  (BitVector.byte -> __ -> 'a1) -> 'a1
197
198val arg_decision_discr : arg_decision -> arg_decision -> __
199
200val arg_decision_jmdiscr : arg_decision -> arg_decision -> __
201
202val dpi1__o__Reg_to_arg_dec__o__inject :
203  (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0
204
205val eject__o__Reg_to_arg_dec__o__inject :
206  I8051.register Types.sig0 -> arg_decision Types.sig0
207
208val reg_to_arg_dec__o__inject : I8051.register -> arg_decision Types.sig0
209
210val dpi1__o__Reg_to_arg_dec :
211  (I8051.register, 'a1) Types.dPair -> arg_decision
212
213val eject__o__Reg_to_arg_dec : I8051.register Types.sig0 -> arg_decision
214
215val preserve_carry_bit :
216  AST.ident List.list -> Bool.bool -> Joint.joint_seq List.list ->
217  Joint.joint_seq List.list
218
219val a : Types.unit0
220
221val dpi1__o__beval_of_byte__o__inject :
222  (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval Types.sig0
223
224val eject__o__beval_of_byte__o__inject :
225  BitVector.byte Types.sig0 -> ByteValues.beval Types.sig0
226
227val beval_of_byte__o__inject : BitVector.byte -> ByteValues.beval Types.sig0
228
229val dpi1__o__beval_of_byte :
230  (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval
231
232val eject__o__beval_of_byte : BitVector.byte Types.sig0 -> ByteValues.beval
233
234val set_dp_by_offset :
235  AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
236
237val get_stack :
238  AST.ident List.list -> Nat.nat -> I8051.register -> Nat.nat ->
239  Joint.joint_seq List.list
240
241val set_stack_not_a :
242  AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
243  Joint.joint_seq List.list
244
245val set_stack_a :
246  AST.ident List.list -> Nat.nat -> Nat.nat -> Joint.joint_seq List.list
247
248val set_stack :
249  AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
250  Joint.joint_seq List.list
251
252val set_stack_int :
253  AST.ident List.list -> Nat.nat -> Nat.nat -> BitVector.byte ->
254  Joint.joint_seq List.list
255
256val move :
257  AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
258  arg_decision -> Joint.joint_seq List.list
259
260val arg_is_spilled : arg_decision -> Bool.bool
261
262val is_spilled : Interference.decision -> Bool.bool
263
264val newframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
265
266val delframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
267
268val commutative : BackEndOps.op2 -> Bool.bool
269
270val uses_carry : BackEndOps.op2 -> Bool.bool
271
272val sets_carry : BackEndOps.op2 -> Bool.bool
273
274val translate_op2 :
275  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
276  Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
277  List.list
278
279val translate_op2_smart :
280  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
281  Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
282  List.list
283
284val dec_to_arg_dec : Interference.decision -> arg_decision
285
286val reg_to_dec__o__dec_arg_dec__o__inject :
287  I8051.register -> arg_decision Types.sig0
288
289val dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject :
290  (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0
291
292val eject__o__Reg_to_dec__o__dec_arg_dec__o__inject :
293  I8051.register Types.sig0 -> arg_decision Types.sig0
294
295val dpi1__o__dec_arg_dec__o__inject :
296  (Interference.decision, 'a1) Types.dPair -> arg_decision Types.sig0
297
298val eject__o__dec_arg_dec__o__inject :
299  Interference.decision Types.sig0 -> arg_decision Types.sig0
300
301val dec_arg_dec__o__inject : Interference.decision -> arg_decision Types.sig0
302
303val reg_to_dec__o__dec_arg_dec : I8051.register -> arg_decision
304
305val dpi1__o__Reg_to_dec__o__dec_arg_dec :
306  (I8051.register, 'a1) Types.dPair -> arg_decision
307
308val eject__o__Reg_to_dec__o__dec_arg_dec :
309  I8051.register Types.sig0 -> arg_decision
310
311val dpi1__o__dec_arg_dec :
312  (Interference.decision, 'a1) Types.dPair -> arg_decision
313
314val eject__o__dec_arg_dec : Interference.decision Types.sig0 -> arg_decision
315
316val translate_op1 :
317  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op1 ->
318  Interference.decision -> Interference.decision -> Joint.joint_seq List.list
319
320val translate_opaccs :
321  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.opAccs ->
322  Interference.decision -> Interference.decision -> arg_decision ->
323  arg_decision -> Joint.joint_seq List.list
324
325val move_to_dp :
326  AST.ident List.list -> Nat.nat -> arg_decision -> arg_decision ->
327  Joint.joint_seq List.list
328
329val translate_store :
330  AST.ident List.list -> Nat.nat -> Bool.bool -> arg_decision -> arg_decision
331  -> arg_decision -> Joint.joint_seq List.list
332
333val translate_load :
334  AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
335  arg_decision -> arg_decision -> Joint.joint_seq List.list
336
337val translate_address :
338  __ List.list -> Nat.nat -> Bool.bool -> __ -> Interference.decision ->
339  Interference.decision -> Joint.joint_seq List.list
340
341val translate_low_address :
342  AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
343  Graphs.label -> Joint.joint_seq List.list
344
345val translate_high_address :
346  AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
347  Graphs.label -> Joint.joint_seq List.list
348
349val translate_step :
350  AST.ident List.list -> Nat.nat -> Fixpoints.valuation ->
351  Interference.coloured_graph -> Nat.nat -> Graphs.label -> Joint.joint_step
352  -> Blocks.bind_step_block
353
354val translate_fin_step :
355  AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
356  Blocks.bind_fin_block
357
358val translate_data :
359  Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
360  AST.ident List.list -> Joint.joint_closed_internal_function ->
361  (Registers.register, TranslateUtils.b_graph_translate_data)
362  Bind_new.bind_new
363
364val ertlptr_to_ltl :
365  Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
366  ERTLptr.ertlptr_program -> ((LTL.ltl_program, Joint.stack_cost_model)
367  Types.prod, Nat.nat) Types.prod
368
Note: See TracBrowser for help on using the repository browser.