source: driver/extracted/interference.ml @ 3106

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

New extraction

File size: 8.6 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 Div_and_mod
102
103open Jmeq
104
105open Russell
106
107open Bool
108
109open Relations
110
111open Nat
112
113open Hints_declaration
114
115open Core_notation
116
117open Pts
118
119open Logic
120
121open Types
122
123open List
124
125open Util
126
127open Liveness
128
129type decision =
130| Decision_spill of Nat.nat
131| Decision_colour of I8051.register
132
133(** val decision_rect_Type4 :
134    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
135let rec decision_rect_Type4 h_decision_spill h_decision_colour = function
136| Decision_spill x_18946 -> h_decision_spill x_18946
137| Decision_colour x_18947 -> h_decision_colour x_18947
138
139(** val decision_rect_Type5 :
140    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
141let rec decision_rect_Type5 h_decision_spill h_decision_colour = function
142| Decision_spill x_18951 -> h_decision_spill x_18951
143| Decision_colour x_18952 -> h_decision_colour x_18952
144
145(** val decision_rect_Type3 :
146    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
147let rec decision_rect_Type3 h_decision_spill h_decision_colour = function
148| Decision_spill x_18956 -> h_decision_spill x_18956
149| Decision_colour x_18957 -> h_decision_colour x_18957
150
151(** val decision_rect_Type2 :
152    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
153let rec decision_rect_Type2 h_decision_spill h_decision_colour = function
154| Decision_spill x_18961 -> h_decision_spill x_18961
155| Decision_colour x_18962 -> h_decision_colour x_18962
156
157(** val decision_rect_Type1 :
158    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
159let rec decision_rect_Type1 h_decision_spill h_decision_colour = function
160| Decision_spill x_18966 -> h_decision_spill x_18966
161| Decision_colour x_18967 -> h_decision_colour x_18967
162
163(** val decision_rect_Type0 :
164    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
165let rec decision_rect_Type0 h_decision_spill h_decision_colour = function
166| Decision_spill x_18971 -> h_decision_spill x_18971
167| Decision_colour x_18972 -> h_decision_colour x_18972
168
169(** val decision_inv_rect_Type4 :
170    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
171    'a1 **)
172let decision_inv_rect_Type4 hterm h1 h2 =
173  let hcut = decision_rect_Type4 h1 h2 hterm in hcut __
174
175(** val decision_inv_rect_Type3 :
176    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
177    'a1 **)
178let decision_inv_rect_Type3 hterm h1 h2 =
179  let hcut = decision_rect_Type3 h1 h2 hterm in hcut __
180
181(** val decision_inv_rect_Type2 :
182    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
183    'a1 **)
184let decision_inv_rect_Type2 hterm h1 h2 =
185  let hcut = decision_rect_Type2 h1 h2 hterm in hcut __
186
187(** val decision_inv_rect_Type1 :
188    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
189    'a1 **)
190let decision_inv_rect_Type1 hterm h1 h2 =
191  let hcut = decision_rect_Type1 h1 h2 hterm in hcut __
192
193(** val decision_inv_rect_Type0 :
194    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
195    'a1 **)
196let decision_inv_rect_Type0 hterm h1 h2 =
197  let hcut = decision_rect_Type0 h1 h2 hterm in hcut __
198
199(** val decision_discr : decision -> decision -> __ **)
200let decision_discr x y =
201  Logic.eq_rect_Type2 x
202    (match x with
203     | Decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
204     | Decision_colour a0 -> Obj.magic (fun _ dH -> dH __)) y
205
206(** val decision_jmdiscr : decision -> decision -> __ **)
207let decision_jmdiscr x y =
208  Logic.eq_rect_Type2 x
209    (match x with
210     | Decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
211     | Decision_colour a0 -> Obj.magic (fun _ dH -> dH __)) y
212
213type coloured_graph = { colouring : (Liveness.vertex -> decision);
214                        spilled_no : Nat.nat }
215
216(** val coloured_graph_rect_Type4 :
217    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
218    __ -> 'a1) -> coloured_graph -> 'a1 **)
219let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_19007 =
220  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19007 in
221  h_mk_coloured_graph colouring0 spilled_no0 __ __
222
223(** val coloured_graph_rect_Type5 :
224    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
225    __ -> 'a1) -> coloured_graph -> 'a1 **)
226let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_19009 =
227  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19009 in
228  h_mk_coloured_graph colouring0 spilled_no0 __ __
229
230(** val coloured_graph_rect_Type3 :
231    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
232    __ -> 'a1) -> coloured_graph -> 'a1 **)
233let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_19011 =
234  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19011 in
235  h_mk_coloured_graph colouring0 spilled_no0 __ __
236
237(** val coloured_graph_rect_Type2 :
238    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
239    __ -> 'a1) -> coloured_graph -> 'a1 **)
240let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_19013 =
241  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19013 in
242  h_mk_coloured_graph colouring0 spilled_no0 __ __
243
244(** val coloured_graph_rect_Type1 :
245    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
246    __ -> 'a1) -> coloured_graph -> 'a1 **)
247let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_19015 =
248  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19015 in
249  h_mk_coloured_graph colouring0 spilled_no0 __ __
250
251(** val coloured_graph_rect_Type0 :
252    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
253    __ -> 'a1) -> coloured_graph -> 'a1 **)
254let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_19017 =
255  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19017 in
256  h_mk_coloured_graph colouring0 spilled_no0 __ __
257
258(** val colouring :
259    Fixpoints.valuation -> coloured_graph -> Liveness.vertex -> decision **)
260let rec colouring before xxx =
261  xxx.colouring
262
263(** val spilled_no : Fixpoints.valuation -> coloured_graph -> Nat.nat **)
264let rec spilled_no before xxx =
265  xxx.spilled_no
266
267(** val coloured_graph_inv_rect_Type4 :
268    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
269    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
270let coloured_graph_inv_rect_Type4 x1 hterm h1 =
271  let hcut = coloured_graph_rect_Type4 x1 h1 hterm in hcut __
272
273(** val coloured_graph_inv_rect_Type3 :
274    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
275    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
276let coloured_graph_inv_rect_Type3 x1 hterm h1 =
277  let hcut = coloured_graph_rect_Type3 x1 h1 hterm in hcut __
278
279(** val coloured_graph_inv_rect_Type2 :
280    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
281    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
282let coloured_graph_inv_rect_Type2 x1 hterm h1 =
283  let hcut = coloured_graph_rect_Type2 x1 h1 hterm in hcut __
284
285(** val coloured_graph_inv_rect_Type1 :
286    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
287    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
288let coloured_graph_inv_rect_Type1 x1 hterm h1 =
289  let hcut = coloured_graph_rect_Type1 x1 h1 hterm in hcut __
290
291(** val coloured_graph_inv_rect_Type0 :
292    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
293    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
294let coloured_graph_inv_rect_Type0 x1 hterm h1 =
295  let hcut = coloured_graph_rect_Type0 x1 h1 hterm in hcut __
296
297(** val coloured_graph_discr :
298    Fixpoints.valuation -> coloured_graph -> coloured_graph -> __ **)
299let coloured_graph_discr a1 x y =
300  Logic.eq_rect_Type2 x
301    (let { colouring = a0; spilled_no = a10 } = x in
302    Obj.magic (fun _ dH -> dH __ __ __ __)) y
303
304(** val coloured_graph_jmdiscr :
305    Fixpoints.valuation -> coloured_graph -> coloured_graph -> __ **)
306let coloured_graph_jmdiscr a1 x y =
307  Logic.eq_rect_Type2 x
308    (let { colouring = a0; spilled_no = a10 } = x in
309    Obj.magic (fun _ dH -> dH __ __ __ __)) y
310
311type coloured_graph_computer =
312  AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation
313  -> coloured_graph
314
Note: See TracBrowser for help on using the repository browser.