Changeset 2730 for extracted/interference.ml
 Timestamp:
 Feb 25, 2013, 9:54:49 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/interference.ml
r2717 r2730 122 122 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 123 123 let rec decision_rect_Type4 h_decision_spill h_decision_colour = function 124  Decision_spill x_ 18503 > h_decision_spill x_18503125  Decision_colour x_ 18504 > h_decision_colour x_18504124  Decision_spill x_394 > h_decision_spill x_394 125  Decision_colour x_395 > h_decision_colour x_395 126 126 127 127 (** val decision_rect_Type5 : 128 128 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 129 129 let rec decision_rect_Type5 h_decision_spill h_decision_colour = function 130  Decision_spill x_ 18508 > h_decision_spill x_18508131  Decision_colour x_ 18509 > h_decision_colour x_18509130  Decision_spill x_399 > h_decision_spill x_399 131  Decision_colour x_400 > h_decision_colour x_400 132 132 133 133 (** val decision_rect_Type3 : 134 134 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 135 135 let rec decision_rect_Type3 h_decision_spill h_decision_colour = function 136  Decision_spill x_ 18513 > h_decision_spill x_18513137  Decision_colour x_ 18514 > h_decision_colour x_18514136  Decision_spill x_404 > h_decision_spill x_404 137  Decision_colour x_405 > h_decision_colour x_405 138 138 139 139 (** val decision_rect_Type2 : 140 140 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 141 141 let rec decision_rect_Type2 h_decision_spill h_decision_colour = function 142  Decision_spill x_ 18518 > h_decision_spill x_18518143  Decision_colour x_ 18519 > h_decision_colour x_18519142  Decision_spill x_409 > h_decision_spill x_409 143  Decision_colour x_410 > h_decision_colour x_410 144 144 145 145 (** val decision_rect_Type1 : 146 146 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 147 147 let rec decision_rect_Type1 h_decision_spill h_decision_colour = function 148  Decision_spill x_ 18523 > h_decision_spill x_18523149  Decision_colour x_ 18524 > h_decision_colour x_18524148  Decision_spill x_414 > h_decision_spill x_414 149  Decision_colour x_415 > h_decision_colour x_415 150 150 151 151 (** val decision_rect_Type0 : 152 152 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 153 153 let rec decision_rect_Type0 h_decision_spill h_decision_colour = function 154  Decision_spill x_ 18528 > h_decision_spill x_18528155  Decision_colour x_ 18529 > h_decision_colour x_18529154  Decision_spill x_419 > h_decision_spill x_419 155  Decision_colour x_420 > h_decision_colour x_420 156 156 157 157 (** val decision_inv_rect_Type4 : … … 205 205 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 206 206 __ > 'a1) > coloured_graph > 'a1 **) 207 let rec coloured_graph_rect_Type4 after h_mk_coloured_graph x_ 18564=208 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 18564in207 let rec coloured_graph_rect_Type4 after h_mk_coloured_graph x_455 = 208 let { colouring = colouring0; spilled_no = spilled_no0 } = x_455 in 209 209 h_mk_coloured_graph colouring0 spilled_no0 __ __ 210 210 … … 212 212 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 213 213 __ > 'a1) > coloured_graph > 'a1 **) 214 let rec coloured_graph_rect_Type5 after h_mk_coloured_graph x_ 18566=215 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 18566in214 let rec coloured_graph_rect_Type5 after h_mk_coloured_graph x_457 = 215 let { colouring = colouring0; spilled_no = spilled_no0 } = x_457 in 216 216 h_mk_coloured_graph colouring0 spilled_no0 __ __ 217 217 … … 219 219 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 220 220 __ > 'a1) > coloured_graph > 'a1 **) 221 let rec coloured_graph_rect_Type3 after h_mk_coloured_graph x_ 18568=222 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 18568in221 let rec coloured_graph_rect_Type3 after h_mk_coloured_graph x_459 = 222 let { colouring = colouring0; spilled_no = spilled_no0 } = x_459 in 223 223 h_mk_coloured_graph colouring0 spilled_no0 __ __ 224 224 … … 226 226 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 227 227 __ > 'a1) > coloured_graph > 'a1 **) 228 let rec coloured_graph_rect_Type2 after h_mk_coloured_graph x_ 18570=229 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 18570in228 let rec coloured_graph_rect_Type2 after h_mk_coloured_graph x_461 = 229 let { colouring = colouring0; spilled_no = spilled_no0 } = x_461 in 230 230 h_mk_coloured_graph colouring0 spilled_no0 __ __ 231 231 … … 233 233 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 234 234 __ > 'a1) > coloured_graph > 'a1 **) 235 let rec coloured_graph_rect_Type1 after h_mk_coloured_graph x_ 18572=236 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 18572in235 let rec coloured_graph_rect_Type1 after h_mk_coloured_graph x_463 = 236 let { colouring = colouring0; spilled_no = spilled_no0 } = x_463 in 237 237 h_mk_coloured_graph colouring0 spilled_no0 __ __ 238 238 … … 240 240 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 241 241 __ > 'a1) > coloured_graph > 'a1 **) 242 let rec coloured_graph_rect_Type0 after h_mk_coloured_graph x_ 18574=243 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 18574in242 let rec coloured_graph_rect_Type0 after h_mk_coloured_graph x_465 = 243 let { colouring = colouring0; spilled_no = spilled_no0 } = x_465 in 244 244 h_mk_coloured_graph colouring0 spilled_no0 __ __ 245 245
Note: See TracChangeset
for help on using the changeset viewer.