source: extracted/interference.mli @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 4.4 KB
Line 
1open Preamble
2
3open Fixpoints
4
5open Set_adt
6
7open Extra_bool
8
9open Coqlib
10
11open Values
12
13open FrontEndVal
14
15open GenMem
16
17open FrontEndMem
18
19open Globalenvs
20
21open String
22
23open Sets
24
25open Listb
26
27open LabelledObjects
28
29open BitVectorTrie
30
31open Graphs
32
33open I8051
34
35open Order
36
37open Registers
38
39open CostLabel
40
41open Hide
42
43open Proper
44
45open PositiveMap
46
47open Deqsets
48
49open ErrorMessages
50
51open PreIdentifiers
52
53open Errors
54
55open Extralib
56
57open Lists
58
59open Identifiers
60
61open Integers
62
63open AST
64
65open Division
66
67open Exp
68
69open Arithmetic
70
71open Setoids
72
73open Monad
74
75open Option
76
77open Extranat
78
79open Vector
80
81open FoldStuff
82
83open BitVector
84
85open Positive
86
87open Z
88
89open BitVectorZ
90
91open Pointers
92
93open ByteValues
94
95open BackEndOps
96
97open Joint
98
99open ERTL
100
101open ERTLptr
102
103open Div_and_mod
104
105open Jmeq
106
107open Russell
108
109open Bool
110
111open Relations
112
113open Nat
114
115open Hints_declaration
116
117open Core_notation
118
119open Pts
120
121open Logic
122
123open Types
124
125open List
126
127open Util
128
129open Liveness
130
131type decision =
132| Decision_spill of Nat.nat
133| Decision_colour of I8051.register
134
135val decision_rect_Type4 :
136  (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
137
138val decision_rect_Type5 :
139  (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
140
141val decision_rect_Type3 :
142  (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
143
144val decision_rect_Type2 :
145  (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
146
147val decision_rect_Type1 :
148  (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
149
150val decision_rect_Type0 :
151  (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
152
153val decision_inv_rect_Type4 :
154  decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
155
156val decision_inv_rect_Type3 :
157  decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
158
159val decision_inv_rect_Type2 :
160  decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
161
162val decision_inv_rect_Type1 :
163  decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
164
165val decision_inv_rect_Type0 :
166  decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
167
168val decision_discr : decision -> decision -> __
169
170val decision_jmdiscr : decision -> decision -> __
171
172type coloured_graph = { colouring : (Liveness.vertex -> decision);
173                        spilled_no : Nat.nat }
174
175val coloured_graph_rect_Type4 :
176  Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
177  __ -> 'a1) -> coloured_graph -> 'a1
178
179val coloured_graph_rect_Type5 :
180  Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
181  __ -> 'a1) -> coloured_graph -> 'a1
182
183val coloured_graph_rect_Type3 :
184  Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
185  __ -> 'a1) -> coloured_graph -> 'a1
186
187val coloured_graph_rect_Type2 :
188  Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
189  __ -> 'a1) -> coloured_graph -> 'a1
190
191val coloured_graph_rect_Type1 :
192  Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
193  __ -> 'a1) -> coloured_graph -> 'a1
194
195val coloured_graph_rect_Type0 :
196  Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
197  __ -> 'a1) -> coloured_graph -> 'a1
198
199val colouring :
200  Fixpoints.valuation -> coloured_graph -> Liveness.vertex -> decision
201
202val spilled_no : Fixpoints.valuation -> coloured_graph -> Nat.nat
203
204val coloured_graph_inv_rect_Type4 :
205  Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
206  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
207
208val coloured_graph_inv_rect_Type3 :
209  Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
210  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
211
212val coloured_graph_inv_rect_Type2 :
213  Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
214  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
215
216val coloured_graph_inv_rect_Type1 :
217  Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
218  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
219
220val coloured_graph_inv_rect_Type0 :
221  Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
222  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
223
224val coloured_graph_discr :
225  Fixpoints.valuation -> coloured_graph -> coloured_graph -> __
226
227val coloured_graph_jmdiscr :
228  Fixpoints.valuation -> coloured_graph -> coloured_graph -> __
229
230type coloured_graph_computer =
231  AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation
232  -> coloured_graph
233
Note: See TracBrowser for help on using the repository browser.