source: extracted/interference.ml @ 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: 8.5 KB
Line 
1open Preamble
2
3open Fixpoints
4
5open Set_adt
6
7open String
8
9open Sets
10
11open Listb
12
13open LabelledObjects
14
15open Graphs
16
17open I8051
18
19open Order
20
21open Registers
22
23open BitVectorTrie
24
25open CostLabel
26
27open Hide
28
29open Proper
30
31open PositiveMap
32
33open Deqsets
34
35open ErrorMessages
36
37open PreIdentifiers
38
39open Errors
40
41open Extralib
42
43open Setoids
44
45open Monad
46
47open Option
48
49open Lists
50
51open Identifiers
52
53open Integers
54
55open AST
56
57open Division
58
59open Exp
60
61open Arithmetic
62
63open Extranat
64
65open Vector
66
67open FoldStuff
68
69open BitVector
70
71open Positive
72
73open Z
74
75open BitVectorZ
76
77open Pointers
78
79open ByteValues
80
81open BackEndOps
82
83open Joint
84
85open ERTL
86
87open ERTLptr
88
89open Div_and_mod
90
91open Jmeq
92
93open Russell
94
95open Bool
96
97open Relations
98
99open Nat
100
101open Hints_declaration
102
103open Core_notation
104
105open Pts
106
107open Logic
108
109open Types
110
111open List
112
113open Util
114
115open Liveness
116
117type decision =
118| Decision_spill of Nat.nat
119| Decision_colour of I8051.register
120
121(** val decision_rect_Type4 :
122    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
123let rec decision_rect_Type4 h_decision_spill h_decision_colour = function
124| Decision_spill x_18503 -> h_decision_spill x_18503
125| Decision_colour x_18504 -> h_decision_colour x_18504
126
127(** val decision_rect_Type5 :
128    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
129let rec decision_rect_Type5 h_decision_spill h_decision_colour = function
130| Decision_spill x_18508 -> h_decision_spill x_18508
131| Decision_colour x_18509 -> h_decision_colour x_18509
132
133(** val decision_rect_Type3 :
134    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
135let rec decision_rect_Type3 h_decision_spill h_decision_colour = function
136| Decision_spill x_18513 -> h_decision_spill x_18513
137| Decision_colour x_18514 -> h_decision_colour x_18514
138
139(** val decision_rect_Type2 :
140    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
141let rec decision_rect_Type2 h_decision_spill h_decision_colour = function
142| Decision_spill x_18518 -> h_decision_spill x_18518
143| Decision_colour x_18519 -> h_decision_colour x_18519
144
145(** val decision_rect_Type1 :
146    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
147let rec decision_rect_Type1 h_decision_spill h_decision_colour = function
148| Decision_spill x_18523 -> h_decision_spill x_18523
149| Decision_colour x_18524 -> h_decision_colour x_18524
150
151(** val decision_rect_Type0 :
152    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
153let rec decision_rect_Type0 h_decision_spill h_decision_colour = function
154| Decision_spill x_18528 -> h_decision_spill x_18528
155| Decision_colour x_18529 -> h_decision_colour x_18529
156
157(** val decision_inv_rect_Type4 :
158    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
159    'a1 **)
160let decision_inv_rect_Type4 hterm h1 h2 =
161  let hcut = decision_rect_Type4 h1 h2 hterm in hcut __
162
163(** val decision_inv_rect_Type3 :
164    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
165    'a1 **)
166let decision_inv_rect_Type3 hterm h1 h2 =
167  let hcut = decision_rect_Type3 h1 h2 hterm in hcut __
168
169(** val decision_inv_rect_Type2 :
170    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
171    'a1 **)
172let decision_inv_rect_Type2 hterm h1 h2 =
173  let hcut = decision_rect_Type2 h1 h2 hterm in hcut __
174
175(** val decision_inv_rect_Type1 :
176    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
177    'a1 **)
178let decision_inv_rect_Type1 hterm h1 h2 =
179  let hcut = decision_rect_Type1 h1 h2 hterm in hcut __
180
181(** val decision_inv_rect_Type0 :
182    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
183    'a1 **)
184let decision_inv_rect_Type0 hterm h1 h2 =
185  let hcut = decision_rect_Type0 h1 h2 hterm in hcut __
186
187(** val decision_discr : decision -> decision -> __ **)
188let decision_discr x y =
189  Logic.eq_rect_Type2 x
190    (match x with
191     | Decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
192     | Decision_colour a0 -> Obj.magic (fun _ dH -> dH __)) y
193
194(** val decision_jmdiscr : decision -> decision -> __ **)
195let decision_jmdiscr x y =
196  Logic.eq_rect_Type2 x
197    (match x with
198     | Decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
199     | Decision_colour a0 -> Obj.magic (fun _ dH -> dH __)) y
200
201type coloured_graph = { colouring : (Liveness.vertex -> decision);
202                        spilled_no : Nat.nat }
203
204(** val coloured_graph_rect_Type4 :
205    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
206    __ -> 'a1) -> coloured_graph -> 'a1 **)
207let rec coloured_graph_rect_Type4 after h_mk_coloured_graph x_18564 =
208  let { colouring = colouring0; spilled_no = spilled_no0 } = x_18564 in
209  h_mk_coloured_graph colouring0 spilled_no0 __ __
210
211(** val coloured_graph_rect_Type5 :
212    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
213    __ -> 'a1) -> coloured_graph -> 'a1 **)
214let rec coloured_graph_rect_Type5 after h_mk_coloured_graph x_18566 =
215  let { colouring = colouring0; spilled_no = spilled_no0 } = x_18566 in
216  h_mk_coloured_graph colouring0 spilled_no0 __ __
217
218(** val coloured_graph_rect_Type3 :
219    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
220    __ -> 'a1) -> coloured_graph -> 'a1 **)
221let rec coloured_graph_rect_Type3 after h_mk_coloured_graph x_18568 =
222  let { colouring = colouring0; spilled_no = spilled_no0 } = x_18568 in
223  h_mk_coloured_graph colouring0 spilled_no0 __ __
224
225(** val coloured_graph_rect_Type2 :
226    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
227    __ -> 'a1) -> coloured_graph -> 'a1 **)
228let rec coloured_graph_rect_Type2 after h_mk_coloured_graph x_18570 =
229  let { colouring = colouring0; spilled_no = spilled_no0 } = x_18570 in
230  h_mk_coloured_graph colouring0 spilled_no0 __ __
231
232(** val coloured_graph_rect_Type1 :
233    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
234    __ -> 'a1) -> coloured_graph -> 'a1 **)
235let rec coloured_graph_rect_Type1 after h_mk_coloured_graph x_18572 =
236  let { colouring = colouring0; spilled_no = spilled_no0 } = x_18572 in
237  h_mk_coloured_graph colouring0 spilled_no0 __ __
238
239(** val coloured_graph_rect_Type0 :
240    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
241    __ -> 'a1) -> coloured_graph -> 'a1 **)
242let rec coloured_graph_rect_Type0 after h_mk_coloured_graph x_18574 =
243  let { colouring = colouring0; spilled_no = spilled_no0 } = x_18574 in
244  h_mk_coloured_graph colouring0 spilled_no0 __ __
245
246(** val colouring :
247    Fixpoints.valuation -> coloured_graph -> Liveness.vertex -> decision **)
248let rec colouring after xxx =
249  xxx.colouring
250
251(** val spilled_no : Fixpoints.valuation -> coloured_graph -> Nat.nat **)
252let rec spilled_no after xxx =
253  xxx.spilled_no
254
255(** val coloured_graph_inv_rect_Type4 :
256    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
257    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
258let coloured_graph_inv_rect_Type4 x1 hterm h1 =
259  let hcut = coloured_graph_rect_Type4 x1 h1 hterm in hcut __
260
261(** val coloured_graph_inv_rect_Type3 :
262    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
263    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
264let coloured_graph_inv_rect_Type3 x1 hterm h1 =
265  let hcut = coloured_graph_rect_Type3 x1 h1 hterm in hcut __
266
267(** val coloured_graph_inv_rect_Type2 :
268    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
269    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
270let coloured_graph_inv_rect_Type2 x1 hterm h1 =
271  let hcut = coloured_graph_rect_Type2 x1 h1 hterm in hcut __
272
273(** val coloured_graph_inv_rect_Type1 :
274    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
275    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
276let coloured_graph_inv_rect_Type1 x1 hterm h1 =
277  let hcut = coloured_graph_rect_Type1 x1 h1 hterm in hcut __
278
279(** val coloured_graph_inv_rect_Type0 :
280    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
281    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
282let coloured_graph_inv_rect_Type0 x1 hterm h1 =
283  let hcut = coloured_graph_rect_Type0 x1 h1 hterm in hcut __
284
285(** val coloured_graph_discr :
286    Fixpoints.valuation -> coloured_graph -> coloured_graph -> __ **)
287let coloured_graph_discr a1 x y =
288  Logic.eq_rect_Type2 x
289    (let { colouring = a0; spilled_no = a10 } = x in
290    Obj.magic (fun _ dH -> dH __ __ __ __)) y
291
292(** val coloured_graph_jmdiscr :
293    Fixpoints.valuation -> coloured_graph -> coloured_graph -> __ **)
294let coloured_graph_jmdiscr a1 x y =
295  Logic.eq_rect_Type2 x
296    (let { colouring = a0; spilled_no = a10 } = x in
297    Obj.magic (fun _ dH -> dH __ __ __ __)) y
298
299type coloured_graph_computer = Fixpoints.valuation -> coloured_graph
300
Note: See TracBrowser for help on using the repository browser.