source: extracted/interference.ml @ 3019

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

New extraction after ERTLptr abortion.

File size: 8.5 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_7 -> h_decision_spill x_7
137| Decision_colour x_8 -> h_decision_colour x_8
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_12 -> h_decision_spill x_12
143| Decision_colour x_13 -> h_decision_colour x_13
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_17 -> h_decision_spill x_17
149| Decision_colour x_18 -> h_decision_colour x_18
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_22 -> h_decision_spill x_22
155| Decision_colour x_23 -> h_decision_colour x_23
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_27 -> h_decision_spill x_27
161| Decision_colour x_28 -> h_decision_colour x_28
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_32 -> h_decision_spill x_32
167| Decision_colour x_33 -> h_decision_colour x_33
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_68 =
220  let { colouring = colouring0; spilled_no = spilled_no0 } = x_68 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_70 =
227  let { colouring = colouring0; spilled_no = spilled_no0 } = x_70 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_72 =
234  let { colouring = colouring0; spilled_no = spilled_no0 } = x_72 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_74 =
241  let { colouring = colouring0; spilled_no = spilled_no0 } = x_74 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_76 =
248  let { colouring = colouring0; spilled_no = spilled_no0 } = x_76 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_78 =
255  let { colouring = colouring0; spilled_no = spilled_no0 } = x_78 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.