source: extracted/eRTLptrToLTL.mli @ 2746

Last change on this file since 2746 was 2743, checked in by sacerdot, 7 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 8.4 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 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 -> I8051.register -> Nat.nat -> Joint.joint_seq
239  List.list
240
241val set_stack_not_a :
242  AST.ident List.list -> Nat.nat -> I8051.register -> Joint.joint_seq
243  List.list
244
245val set_stack_a : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
246
247val set_stack :
248  AST.ident List.list -> Nat.nat -> I8051.register -> Joint.joint_seq
249  List.list
250
251val set_stack_int :
252  AST.ident List.list -> Nat.nat -> BitVector.byte -> Joint.joint_seq
253  List.list
254
255val move :
256  AST.ident List.list -> Bool.bool -> Interference.decision -> arg_decision
257  -> Joint.joint_seq List.list
258
259val arg_is_spilled : arg_decision -> Bool.bool
260
261val is_spilled : Interference.decision -> Bool.bool
262
263val newframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
264
265val delframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
266
267val commutative : BackEndOps.op2 -> Bool.bool
268
269val uses_carry : BackEndOps.op2 -> Bool.bool
270
271val sets_carry : BackEndOps.op2 -> Bool.bool
272
273val translate_op2 :
274  AST.ident List.list -> Bool.bool -> BackEndOps.op2 -> Interference.decision
275  -> arg_decision -> arg_decision -> Joint.joint_seq List.list
276
277val translate_op2_smart :
278  AST.ident List.list -> Bool.bool -> BackEndOps.op2 -> Interference.decision
279  -> arg_decision -> arg_decision -> Joint.joint_seq List.list
280
281val dec_to_arg_dec : Interference.decision -> arg_decision
282
283val reg_to_dec__o__dec_arg_dec__o__inject :
284  I8051.register -> arg_decision Types.sig0
285
286val dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject :
287  (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0
288
289val eject__o__Reg_to_dec__o__dec_arg_dec__o__inject :
290  I8051.register Types.sig0 -> arg_decision Types.sig0
291
292val dpi1__o__dec_arg_dec__o__inject :
293  (Interference.decision, 'a1) Types.dPair -> arg_decision Types.sig0
294
295val eject__o__dec_arg_dec__o__inject :
296  Interference.decision Types.sig0 -> arg_decision Types.sig0
297
298val dec_arg_dec__o__inject : Interference.decision -> arg_decision Types.sig0
299
300val reg_to_dec__o__dec_arg_dec : I8051.register -> arg_decision
301
302val dpi1__o__Reg_to_dec__o__dec_arg_dec :
303  (I8051.register, 'a1) Types.dPair -> arg_decision
304
305val eject__o__Reg_to_dec__o__dec_arg_dec :
306  I8051.register Types.sig0 -> arg_decision
307
308val dpi1__o__dec_arg_dec :
309  (Interference.decision, 'a1) Types.dPair -> arg_decision
310
311val eject__o__dec_arg_dec : Interference.decision Types.sig0 -> arg_decision
312
313val translate_op1 :
314  AST.ident List.list -> Bool.bool -> BackEndOps.op1 -> Interference.decision
315  -> Interference.decision -> Joint.joint_seq List.list
316
317val translate_opaccs :
318  AST.ident List.list -> Bool.bool -> BackEndOps.opAccs ->
319  Interference.decision -> Interference.decision -> arg_decision ->
320  arg_decision -> Joint.joint_seq List.list
321
322val move_to_dp :
323  AST.ident List.list -> arg_decision -> arg_decision -> Joint.joint_seq
324  List.list
325
326val translate_store :
327  AST.ident List.list -> Bool.bool -> arg_decision -> arg_decision ->
328  arg_decision -> Joint.joint_seq List.list
329
330val translate_load :
331  AST.ident List.list -> Bool.bool -> Interference.decision -> arg_decision
332  -> arg_decision -> Joint.joint_seq List.list
333
334val translate_address :
335  __ List.list -> Bool.bool -> __ -> Interference.decision ->
336  Interference.decision -> Joint.joint_seq List.list
337
338val translate_low_address :
339  AST.ident List.list -> Bool.bool -> Interference.decision -> Graphs.label
340  -> Joint.joint_seq List.list
341
342val translate_high_address :
343  AST.ident List.list -> Bool.bool -> Interference.decision -> Graphs.label
344  -> Joint.joint_seq List.list
345
346val translate_step :
347  AST.ident List.list -> Fixpoints.valuation -> Interference.coloured_graph
348  -> Nat.nat -> Graphs.label -> Joint.joint_step -> Blocks.bind_step_block
349
350val translate_fin_step :
351  AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
352  Blocks.bind_fin_block
353
354val translate_data :
355  Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
356  AST.ident List.list -> Joint.joint_closed_internal_function ->
357  (Registers.register, TranslateUtils.b_graph_translate_data)
358  Bind_new.bind_new
359
360val ertlptr_to_ltl :
361  Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
362  ERTLptr.ertlptr_program -> LTL.ltl_program
363
Note: See TracBrowser for help on using the repository browser.