113 open Hints_declaration
130 | Decision_spill of Nat.nat
131 | Decision_colour of I8051.register
133 (** val decision_rect_Type4 :
134 (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
135 let 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
139 (** val decision_rect_Type5 :
140 (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
141 let 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
145 (** val decision_rect_Type3 :
146 (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
147 let 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
151 (** val decision_rect_Type2 :
152 (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
153 let 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
157 (** val decision_rect_Type1 :
158 (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
159 let 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
163 (** val decision_rect_Type0 :
164 (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
165 let 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
169 (** val decision_inv_rect_Type4 :
170 decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
172 let decision_inv_rect_Type4 hterm h1 h2 =
173 let hcut = decision_rect_Type4 h1 h2 hterm in hcut __
175 (** val decision_inv_rect_Type3 :
176 decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
178 let decision_inv_rect_Type3 hterm h1 h2 =
179 let hcut = decision_rect_Type3 h1 h2 hterm in hcut __
181 (** val decision_inv_rect_Type2 :
182 decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
184 let decision_inv_rect_Type2 hterm h1 h2 =
185 let hcut = decision_rect_Type2 h1 h2 hterm in hcut __
187 (** val decision_inv_rect_Type1 :
188 decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
190 let decision_inv_rect_Type1 hterm h1 h2 =
191 let hcut = decision_rect_Type1 h1 h2 hterm in hcut __
193 (** val decision_inv_rect_Type0 :
194 decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
196 let decision_inv_rect_Type0 hterm h1 h2 =
197 let hcut = decision_rect_Type0 h1 h2 hterm in hcut __
199 (** val decision_discr : decision -> decision -> __ **)
200 let decision_discr x y =
201 Logic.eq_rect_Type2 x
203 | Decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
204 | Decision_colour a0 -> Obj.magic (fun _ dH -> dH __)) y
206 (** val decision_jmdiscr : decision -> decision -> __ **)
207 let decision_jmdiscr x y =
208 Logic.eq_rect_Type2 x
210 | Decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
211 | Decision_colour a0 -> Obj.magic (fun _ dH -> dH __)) y
213 type coloured_graph = { colouring : (Liveness.vertex -> decision);
214 spilled_no : Nat.nat }
216 (** val coloured_graph_rect_Type4 :
217 Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
218 __ -> 'a1) -> coloured_graph -> 'a1 **)
219 let 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 __ __
223 (** val coloured_graph_rect_Type5 :
224 Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
225 __ -> 'a1) -> coloured_graph -> 'a1 **)
226 let 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 __ __
230 (** val coloured_graph_rect_Type3 :
231 Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
232 __ -> 'a1) -> coloured_graph -> 'a1 **)
233 let 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 __ __
237 (** val coloured_graph_rect_Type2 :
238 Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
239 __ -> 'a1) -> coloured_graph -> 'a1 **)
240 let 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 __ __
244 (** val coloured_graph_rect_Type1 :
245 Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
246 __ -> 'a1) -> coloured_graph -> 'a1 **)
247 let 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 __ __
251 (** val coloured_graph_rect_Type0 :
252 Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
253 __ -> 'a1) -> coloured_graph -> 'a1 **)
254 let 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 __ __
259 Fixpoints.valuation -> coloured_graph -> Liveness.vertex -> decision **)
260 let rec colouring before xxx =
263 (** val spilled_no : Fixpoints.valuation -> coloured_graph -> Nat.nat **)
264 let rec spilled_no before xxx =
267 (** val coloured_graph_inv_rect_Type4 :
268 Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
269 -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
270 let coloured_graph_inv_rect_Type4 x1 hterm h1 =
271 let hcut = coloured_graph_rect_Type4 x1 h1 hterm in hcut __
273 (** val coloured_graph_inv_rect_Type3 :
274 Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
275 -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
276 let coloured_graph_inv_rect_Type3 x1 hterm h1 =
277 let hcut = coloured_graph_rect_Type3 x1 h1 hterm in hcut __
279 (** val coloured_graph_inv_rect_Type2 :
280 Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
281 -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
282 let coloured_graph_inv_rect_Type2 x1 hterm h1 =
283 let hcut = coloured_graph_rect_Type2 x1 h1 hterm in hcut __
285 (** val coloured_graph_inv_rect_Type1 :
286 Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
287 -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
288 let coloured_graph_inv_rect_Type1 x1 hterm h1 =
289 let hcut = coloured_graph_rect_Type1 x1 h1 hterm in hcut __
291 (** val coloured_graph_inv_rect_Type0 :
292 Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
293 -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
294 let coloured_graph_inv_rect_Type0 x1 hterm h1 =
295 let hcut = coloured_graph_rect_Type0 x1 h1 hterm in hcut __
297 (** val coloured_graph_discr :
298 Fixpoints.valuation -> coloured_graph -> coloured_graph -> __ **)
299 let 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
304 (** val coloured_graph_jmdiscr :
305 Fixpoints.valuation -> coloured_graph -> coloured_graph -> __ **)
306 let 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
311 type coloured_graph_computer =
312 AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation