Changeset 2960 for extracted/interference.ml
 Timestamp:
 Mar 26, 2013, 4:51:40 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/interference.ml
r2951 r2960 136 136 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 137 137 let rec decision_rect_Type4 h_decision_spill h_decision_colour = function 138  Decision_spill x_ 19110 > h_decision_spill x_19110139  Decision_colour x_ 19111 > h_decision_colour x_19111138  Decision_spill x_281 > h_decision_spill x_281 139  Decision_colour x_282 > h_decision_colour x_282 140 140 141 141 (** val decision_rect_Type5 : 142 142 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 143 143 let rec decision_rect_Type5 h_decision_spill h_decision_colour = function 144  Decision_spill x_ 19115 > h_decision_spill x_19115145  Decision_colour x_ 19116 > h_decision_colour x_19116144  Decision_spill x_286 > h_decision_spill x_286 145  Decision_colour x_287 > h_decision_colour x_287 146 146 147 147 (** val decision_rect_Type3 : 148 148 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 149 149 let rec decision_rect_Type3 h_decision_spill h_decision_colour = function 150  Decision_spill x_ 19120 > h_decision_spill x_19120151  Decision_colour x_ 19121 > h_decision_colour x_19121150  Decision_spill x_291 > h_decision_spill x_291 151  Decision_colour x_292 > h_decision_colour x_292 152 152 153 153 (** val decision_rect_Type2 : 154 154 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 155 155 let rec decision_rect_Type2 h_decision_spill h_decision_colour = function 156  Decision_spill x_ 19125 > h_decision_spill x_19125157  Decision_colour x_ 19126 > h_decision_colour x_19126156  Decision_spill x_296 > h_decision_spill x_296 157  Decision_colour x_297 > h_decision_colour x_297 158 158 159 159 (** val decision_rect_Type1 : 160 160 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 161 161 let rec decision_rect_Type1 h_decision_spill h_decision_colour = function 162  Decision_spill x_ 19130 > h_decision_spill x_19130163  Decision_colour x_ 19131 > h_decision_colour x_19131162  Decision_spill x_301 > h_decision_spill x_301 163  Decision_colour x_302 > h_decision_colour x_302 164 164 165 165 (** val decision_rect_Type0 : 166 166 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 167 167 let rec decision_rect_Type0 h_decision_spill h_decision_colour = function 168  Decision_spill x_ 19135 > h_decision_spill x_19135169  Decision_colour x_ 19136 > h_decision_colour x_19136168  Decision_spill x_306 > h_decision_spill x_306 169  Decision_colour x_307 > h_decision_colour x_307 170 170 171 171 (** val decision_inv_rect_Type4 : … … 219 219 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 220 220 __ > 'a1) > coloured_graph > 'a1 **) 221 let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_ 19171=222 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 19171in221 let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_342 = 222 let { colouring = colouring0; spilled_no = spilled_no0 } = x_342 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_Type5 before h_mk_coloured_graph x_ 19173=229 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 19173in228 let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_344 = 229 let { colouring = colouring0; spilled_no = spilled_no0 } = x_344 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_Type3 before h_mk_coloured_graph x_ 19175=236 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 19175in235 let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_346 = 236 let { colouring = colouring0; spilled_no = spilled_no0 } = x_346 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_Type2 before h_mk_coloured_graph x_ 19177=243 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 19177in242 let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_348 = 243 let { colouring = colouring0; spilled_no = spilled_no0 } = x_348 in 244 244 h_mk_coloured_graph colouring0 spilled_no0 __ __ 245 245 … … 247 247 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 248 248 __ > 'a1) > coloured_graph > 'a1 **) 249 let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_ 19179=250 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 19179in249 let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_350 = 250 let { colouring = colouring0; spilled_no = spilled_no0 } = x_350 in 251 251 h_mk_coloured_graph colouring0 spilled_no0 __ __ 252 252 … … 254 254 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 255 255 __ > 'a1) > coloured_graph > 'a1 **) 256 let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_ 19181=257 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 19181in256 let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_352 = 257 let { colouring = colouring0; spilled_no = spilled_no0 } = x_352 in 258 258 h_mk_coloured_graph colouring0 spilled_no0 __ __ 259 259
Note: See TracChangeset
for help on using the changeset viewer.