source: extracted/interference.ml @ 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: 8.7 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
135(** val decision_rect_Type4 :
136    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
137let rec decision_rect_Type4 h_decision_spill h_decision_colour = function
138| Decision_spill x_19110 -> h_decision_spill x_19110
139| Decision_colour x_19111 -> h_decision_colour x_19111
140
141(** val decision_rect_Type5 :
142    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
143let rec decision_rect_Type5 h_decision_spill h_decision_colour = function
144| Decision_spill x_19115 -> h_decision_spill x_19115
145| Decision_colour x_19116 -> h_decision_colour x_19116
146
147(** val decision_rect_Type3 :
148    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
149let rec decision_rect_Type3 h_decision_spill h_decision_colour = function
150| Decision_spill x_19120 -> h_decision_spill x_19120
151| Decision_colour x_19121 -> h_decision_colour x_19121
152
153(** val decision_rect_Type2 :
154    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
155let rec decision_rect_Type2 h_decision_spill h_decision_colour = function
156| Decision_spill x_19125 -> h_decision_spill x_19125
157| Decision_colour x_19126 -> h_decision_colour x_19126
158
159(** val decision_rect_Type1 :
160    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
161let rec decision_rect_Type1 h_decision_spill h_decision_colour = function
162| Decision_spill x_19130 -> h_decision_spill x_19130
163| Decision_colour x_19131 -> h_decision_colour x_19131
164
165(** val decision_rect_Type0 :
166    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
167let rec decision_rect_Type0 h_decision_spill h_decision_colour = function
168| Decision_spill x_19135 -> h_decision_spill x_19135
169| Decision_colour x_19136 -> h_decision_colour x_19136
170
171(** val decision_inv_rect_Type4 :
172    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
173    'a1 **)
174let decision_inv_rect_Type4 hterm h1 h2 =
175  let hcut = decision_rect_Type4 h1 h2 hterm in hcut __
176
177(** val decision_inv_rect_Type3 :
178    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
179    'a1 **)
180let decision_inv_rect_Type3 hterm h1 h2 =
181  let hcut = decision_rect_Type3 h1 h2 hterm in hcut __
182
183(** val decision_inv_rect_Type2 :
184    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
185    'a1 **)
186let decision_inv_rect_Type2 hterm h1 h2 =
187  let hcut = decision_rect_Type2 h1 h2 hterm in hcut __
188
189(** val decision_inv_rect_Type1 :
190    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
191    'a1 **)
192let decision_inv_rect_Type1 hterm h1 h2 =
193  let hcut = decision_rect_Type1 h1 h2 hterm in hcut __
194
195(** val decision_inv_rect_Type0 :
196    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
197    'a1 **)
198let decision_inv_rect_Type0 hterm h1 h2 =
199  let hcut = decision_rect_Type0 h1 h2 hterm in hcut __
200
201(** val decision_discr : decision -> decision -> __ **)
202let decision_discr x y =
203  Logic.eq_rect_Type2 x
204    (match x with
205     | Decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
206     | Decision_colour a0 -> Obj.magic (fun _ dH -> dH __)) y
207
208(** val decision_jmdiscr : decision -> decision -> __ **)
209let decision_jmdiscr x y =
210  Logic.eq_rect_Type2 x
211    (match x with
212     | Decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
213     | Decision_colour a0 -> Obj.magic (fun _ dH -> dH __)) y
214
215type coloured_graph = { colouring : (Liveness.vertex -> decision);
216                        spilled_no : Nat.nat }
217
218(** val coloured_graph_rect_Type4 :
219    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
220    __ -> 'a1) -> coloured_graph -> 'a1 **)
221let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_19171 =
222  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19171 in
223  h_mk_coloured_graph colouring0 spilled_no0 __ __
224
225(** val coloured_graph_rect_Type5 :
226    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
227    __ -> 'a1) -> coloured_graph -> 'a1 **)
228let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_19173 =
229  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19173 in
230  h_mk_coloured_graph colouring0 spilled_no0 __ __
231
232(** val coloured_graph_rect_Type3 :
233    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
234    __ -> 'a1) -> coloured_graph -> 'a1 **)
235let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_19175 =
236  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19175 in
237  h_mk_coloured_graph colouring0 spilled_no0 __ __
238
239(** val coloured_graph_rect_Type2 :
240    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
241    __ -> 'a1) -> coloured_graph -> 'a1 **)
242let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_19177 =
243  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19177 in
244  h_mk_coloured_graph colouring0 spilled_no0 __ __
245
246(** val coloured_graph_rect_Type1 :
247    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
248    __ -> 'a1) -> coloured_graph -> 'a1 **)
249let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_19179 =
250  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19179 in
251  h_mk_coloured_graph colouring0 spilled_no0 __ __
252
253(** val coloured_graph_rect_Type0 :
254    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
255    __ -> 'a1) -> coloured_graph -> 'a1 **)
256let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_19181 =
257  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19181 in
258  h_mk_coloured_graph colouring0 spilled_no0 __ __
259
260(** val colouring :
261    Fixpoints.valuation -> coloured_graph -> Liveness.vertex -> decision **)
262let rec colouring before xxx =
263  xxx.colouring
264
265(** val spilled_no : Fixpoints.valuation -> coloured_graph -> Nat.nat **)
266let rec spilled_no before xxx =
267  xxx.spilled_no
268
269(** val coloured_graph_inv_rect_Type4 :
270    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
271    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
272let coloured_graph_inv_rect_Type4 x1 hterm h1 =
273  let hcut = coloured_graph_rect_Type4 x1 h1 hterm in hcut __
274
275(** val coloured_graph_inv_rect_Type3 :
276    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
277    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
278let coloured_graph_inv_rect_Type3 x1 hterm h1 =
279  let hcut = coloured_graph_rect_Type3 x1 h1 hterm in hcut __
280
281(** val coloured_graph_inv_rect_Type2 :
282    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
283    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
284let coloured_graph_inv_rect_Type2 x1 hterm h1 =
285  let hcut = coloured_graph_rect_Type2 x1 h1 hterm in hcut __
286
287(** val coloured_graph_inv_rect_Type1 :
288    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
289    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
290let coloured_graph_inv_rect_Type1 x1 hterm h1 =
291  let hcut = coloured_graph_rect_Type1 x1 h1 hterm in hcut __
292
293(** val coloured_graph_inv_rect_Type0 :
294    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
295    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
296let coloured_graph_inv_rect_Type0 x1 hterm h1 =
297  let hcut = coloured_graph_rect_Type0 x1 h1 hterm in hcut __
298
299(** val coloured_graph_discr :
300    Fixpoints.valuation -> coloured_graph -> coloured_graph -> __ **)
301let coloured_graph_discr a1 x y =
302  Logic.eq_rect_Type2 x
303    (let { colouring = a0; spilled_no = a10 } = x in
304    Obj.magic (fun _ dH -> dH __ __ __ __)) y
305
306(** val coloured_graph_jmdiscr :
307    Fixpoints.valuation -> coloured_graph -> coloured_graph -> __ **)
308let coloured_graph_jmdiscr a1 x y =
309  Logic.eq_rect_Type2 x
310    (let { colouring = a0; spilled_no = a10 } = x in
311    Obj.magic (fun _ dH -> dH __ __ __ __)) y
312
313type coloured_graph_computer =
314  AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation
315  -> coloured_graph
316
Note: See TracBrowser for help on using the repository browser.