Changeset 2873 for extracted/interference.ml
 Timestamp:
 Mar 14, 2013, 10:37:39 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/interference.ml
r2867 r2873 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_2 1838 > h_decision_spill x_21838125  Decision_colour x_2 1839 > h_decision_colour x_21839124  Decision_spill x_22007 > h_decision_spill x_22007 125  Decision_colour x_22008 > h_decision_colour x_22008 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_2 1843 > h_decision_spill x_21843131  Decision_colour x_2 1844 > h_decision_colour x_21844130  Decision_spill x_22012 > h_decision_spill x_22012 131  Decision_colour x_22013 > h_decision_colour x_22013 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_2 1848 > h_decision_spill x_21848137  Decision_colour x_2 1849 > h_decision_colour x_21849136  Decision_spill x_22017 > h_decision_spill x_22017 137  Decision_colour x_22018 > h_decision_colour x_22018 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_2 1853 > h_decision_spill x_21853143  Decision_colour x_2 1854 > h_decision_colour x_21854142  Decision_spill x_22022 > h_decision_spill x_22022 143  Decision_colour x_22023 > h_decision_colour x_22023 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_2 1858 > h_decision_spill x_21858149  Decision_colour x_2 1859 > h_decision_colour x_21859148  Decision_spill x_22027 > h_decision_spill x_22027 149  Decision_colour x_22028 > h_decision_colour x_22028 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_2 1863 > h_decision_spill x_21863155  Decision_colour x_2 1864 > h_decision_colour x_21864154  Decision_spill x_22032 > h_decision_spill x_22032 155  Decision_colour x_22033 > h_decision_colour x_22033 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_2 1899=208 let { colouring = colouring0; spilled_no = spilled_no0 } = x_2 1899in207 let rec coloured_graph_rect_Type4 after h_mk_coloured_graph x_22068 = 208 let { colouring = colouring0; spilled_no = spilled_no0 } = x_22068 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_2 1901=215 let { colouring = colouring0; spilled_no = spilled_no0 } = x_2 1901in214 let rec coloured_graph_rect_Type5 after h_mk_coloured_graph x_22070 = 215 let { colouring = colouring0; spilled_no = spilled_no0 } = x_22070 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_2 1903=222 let { colouring = colouring0; spilled_no = spilled_no0 } = x_2 1903in221 let rec coloured_graph_rect_Type3 after h_mk_coloured_graph x_22072 = 222 let { colouring = colouring0; spilled_no = spilled_no0 } = x_22072 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_2 1905=229 let { colouring = colouring0; spilled_no = spilled_no0 } = x_2 1905in228 let rec coloured_graph_rect_Type2 after h_mk_coloured_graph x_22074 = 229 let { colouring = colouring0; spilled_no = spilled_no0 } = x_22074 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_2 1907=236 let { colouring = colouring0; spilled_no = spilled_no0 } = x_2 1907in235 let rec coloured_graph_rect_Type1 after h_mk_coloured_graph x_22076 = 236 let { colouring = colouring0; spilled_no = spilled_no0 } = x_22076 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_2 1909=243 let { colouring = colouring0; spilled_no = spilled_no0 } = x_2 1909in242 let rec coloured_graph_rect_Type0 after h_mk_coloured_graph x_22078 = 243 let { colouring = colouring0; spilled_no = spilled_no0 } = x_22078 in 244 244 h_mk_coloured_graph colouring0 spilled_no0 __ __ 245 245
Note: See TracChangeset
for help on using the changeset viewer.