source: extracted/eRTLptrToLTL.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: 6.0 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
124
125open State
126
127open Bind_new
128
129open BindLists
130
131open Blocks
132
133open TranslateUtils
134
135type arg_decision =
136| Arg_decision_colour of I8051.register
137| Arg_decision_spill of Nat.nat
138| Arg_decision_imm of BitVector.byte
139
140val arg_decision_rect_Type4 :
141  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
142  arg_decision -> 'a1
143
144val arg_decision_rect_Type5 :
145  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
146  arg_decision -> 'a1
147
148val arg_decision_rect_Type3 :
149  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
150  arg_decision -> 'a1
151
152val arg_decision_rect_Type2 :
153  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
154  arg_decision -> 'a1
155
156val arg_decision_rect_Type1 :
157  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
158  arg_decision -> 'a1
159
160val arg_decision_rect_Type0 :
161  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
162  arg_decision -> 'a1
163
164val arg_decision_inv_rect_Type4 :
165  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
166  (BitVector.byte -> __ -> 'a1) -> 'a1
167
168val arg_decision_inv_rect_Type3 :
169  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
170  (BitVector.byte -> __ -> 'a1) -> 'a1
171
172val arg_decision_inv_rect_Type2 :
173  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
174  (BitVector.byte -> __ -> 'a1) -> 'a1
175
176val arg_decision_inv_rect_Type1 :
177  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
178  (BitVector.byte -> __ -> 'a1) -> 'a1
179
180val arg_decision_inv_rect_Type0 :
181  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
182  (BitVector.byte -> __ -> 'a1) -> 'a1
183
184val arg_decision_discr : arg_decision -> arg_decision -> __
185
186val arg_decision_jmdiscr : arg_decision -> arg_decision -> __
187
188val preserve_carry_bit :
189  AST.ident List.list -> Bool.bool -> Joint.joint_seq List.list ->
190  Joint.joint_seq List.list
191
192val a : Types.unit0
193
194val set_dp_by_offset :
195  AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
196
197val get_stack :
198  AST.ident List.list -> I8051.register -> Nat.nat -> Joint.joint_seq
199  List.list
200
201val set_stack_not_a :
202  AST.ident List.list -> Nat.nat -> I8051.register -> Joint.joint_seq
203  List.list
204
205val set_stack_a : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
206
207val set_stack :
208  AST.ident List.list -> Nat.nat -> I8051.register -> Joint.joint_seq
209  List.list
210
211val set_stack_int :
212  AST.ident List.list -> Nat.nat -> BitVector.byte -> Joint.joint_seq
213  List.list
214
215val move :
216  AST.ident List.list -> Bool.bool -> Interference.decision -> arg_decision
217  -> Joint.joint_seq List.list
218
219val arg_is_spilled : arg_decision -> Bool.bool
220
221val is_spilled : Interference.decision -> Bool.bool
222
223val newframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
224
225val delframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
226
227val commutative : BackEndOps.op2 -> Bool.bool
228
229val uses_carry : BackEndOps.op2 -> Bool.bool
230
231val sets_carry : BackEndOps.op2 -> Bool.bool
232
233val translate_op2 :
234  AST.ident List.list -> Bool.bool -> BackEndOps.op2 -> Interference.decision
235  -> arg_decision -> arg_decision -> Joint.joint_seq List.list
236
237val translate_op2_smart :
238  AST.ident List.list -> Bool.bool -> BackEndOps.op2 -> Interference.decision
239  -> arg_decision -> arg_decision -> Joint.joint_seq List.list
240
241val dec_to_arg_dec : Interference.decision -> arg_decision
242
243val translate_op1 :
244  AST.ident List.list -> Bool.bool -> BackEndOps.op1 -> Interference.decision
245  -> Interference.decision -> Joint.joint_seq List.list
246
247val translate_opaccs :
248  AST.ident List.list -> Bool.bool -> BackEndOps.opAccs ->
249  Interference.decision -> Interference.decision -> arg_decision ->
250  arg_decision -> Joint.joint_seq List.list
251
252val move_to_dp :
253  AST.ident List.list -> arg_decision -> arg_decision -> Joint.joint_seq
254  List.list
255
256val translate_store :
257  AST.ident List.list -> Bool.bool -> arg_decision -> arg_decision ->
258  arg_decision -> Joint.joint_seq List.list
259
260val translate_load :
261  AST.ident List.list -> Bool.bool -> Interference.decision -> arg_decision
262  -> arg_decision -> Joint.joint_seq List.list
263
264val translate_address :
265  __ List.list -> Bool.bool -> __ -> Interference.decision ->
266  Interference.decision -> Joint.joint_seq List.list
267
268val translate_low_address :
269  AST.ident List.list -> Bool.bool -> Interference.decision -> Graphs.label
270  -> Joint.joint_seq List.list
271
272val translate_high_address :
273  AST.ident List.list -> Bool.bool -> Interference.decision -> Graphs.label
274  -> Joint.joint_seq List.list
275
276val translate_step :
277  AST.ident List.list -> Fixpoints.valuation -> Interference.coloured_graph
278  -> Nat.nat -> Graphs.label -> Joint.joint_step -> Blocks.bind_step_block
279
280val translate_fin_step :
281  AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
282  Blocks.bind_fin_block
283
284val translate_data :
285  Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
286  AST.ident List.list -> Joint.joint_closed_internal_function ->
287  (Registers.register, TranslateUtils.b_graph_translate_data)
288  Bind_new.bind_new
289
290val ertlptr_to_ltl :
291  Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
292  ERTLptr.ertlptr_program -> LTL.ltl_program
293
Note: See TracBrowser for help on using the repository browser.