Changeset 3019 for extracted/interference.ml
- Timestamp:
- Mar 28, 2013, 5:27:46 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
extracted/interference.ml
r3001 r3019 98 98 99 99 open ERTL 100 101 open ERTLptr102 100 103 101 open Div_and_mod … … 136 134 (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **) 137 135 let rec decision_rect_Type4 h_decision_spill h_decision_colour = function 138 | Decision_spill x_ 5765 -> h_decision_spill x_5765139 | Decision_colour x_ 5766 -> h_decision_colour x_5766136 | Decision_spill x_7 -> h_decision_spill x_7 137 | Decision_colour x_8 -> h_decision_colour x_8 140 138 141 139 (** val decision_rect_Type5 : 142 140 (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **) 143 141 let rec decision_rect_Type5 h_decision_spill h_decision_colour = function 144 | Decision_spill x_ 5770 -> h_decision_spill x_5770145 | Decision_colour x_ 5771 -> h_decision_colour x_5771142 | Decision_spill x_12 -> h_decision_spill x_12 143 | Decision_colour x_13 -> h_decision_colour x_13 146 144 147 145 (** val decision_rect_Type3 : 148 146 (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **) 149 147 let rec decision_rect_Type3 h_decision_spill h_decision_colour = function 150 | Decision_spill x_ 5775 -> h_decision_spill x_5775151 | Decision_colour x_ 5776 -> h_decision_colour x_5776148 | Decision_spill x_17 -> h_decision_spill x_17 149 | Decision_colour x_18 -> h_decision_colour x_18 152 150 153 151 (** val decision_rect_Type2 : 154 152 (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **) 155 153 let rec decision_rect_Type2 h_decision_spill h_decision_colour = function 156 | Decision_spill x_ 5780 -> h_decision_spill x_5780157 | Decision_colour x_ 5781 -> h_decision_colour x_5781154 | Decision_spill x_22 -> h_decision_spill x_22 155 | Decision_colour x_23 -> h_decision_colour x_23 158 156 159 157 (** val decision_rect_Type1 : 160 158 (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **) 161 159 let rec decision_rect_Type1 h_decision_spill h_decision_colour = function 162 | Decision_spill x_ 5785 -> h_decision_spill x_5785163 | Decision_colour x_ 5786 -> h_decision_colour x_5786160 | Decision_spill x_27 -> h_decision_spill x_27 161 | Decision_colour x_28 -> h_decision_colour x_28 164 162 165 163 (** val decision_rect_Type0 : 166 164 (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **) 167 165 let rec decision_rect_Type0 h_decision_spill h_decision_colour = function 168 | Decision_spill x_ 5790 -> h_decision_spill x_5790169 | Decision_colour x_ 5791 -> h_decision_colour x_5791166 | Decision_spill x_32 -> h_decision_spill x_32 167 | Decision_colour x_33 -> h_decision_colour x_33 170 168 171 169 (** val decision_inv_rect_Type4 : … … 219 217 Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ -> 220 218 __ -> 'a1) -> coloured_graph -> 'a1 **) 221 let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_ 5826=222 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 5826in219 let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_68 = 220 let { colouring = colouring0; spilled_no = spilled_no0 } = x_68 in 223 221 h_mk_coloured_graph colouring0 spilled_no0 __ __ 224 222 … … 226 224 Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ -> 227 225 __ -> 'a1) -> coloured_graph -> 'a1 **) 228 let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_ 5828=229 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 5828in226 let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_70 = 227 let { colouring = colouring0; spilled_no = spilled_no0 } = x_70 in 230 228 h_mk_coloured_graph colouring0 spilled_no0 __ __ 231 229 … … 233 231 Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ -> 234 232 __ -> 'a1) -> coloured_graph -> 'a1 **) 235 let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_ 5830=236 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 5830in233 let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_72 = 234 let { colouring = colouring0; spilled_no = spilled_no0 } = x_72 in 237 235 h_mk_coloured_graph colouring0 spilled_no0 __ __ 238 236 … … 240 238 Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ -> 241 239 __ -> 'a1) -> coloured_graph -> 'a1 **) 242 let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_ 5832=243 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 5832in240 let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_74 = 241 let { colouring = colouring0; spilled_no = spilled_no0 } = x_74 in 244 242 h_mk_coloured_graph colouring0 spilled_no0 __ __ 245 243 … … 247 245 Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ -> 248 246 __ -> 'a1) -> coloured_graph -> 'a1 **) 249 let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_ 5834=250 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 5834in247 let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_76 = 248 let { colouring = colouring0; spilled_no = spilled_no0 } = x_76 in 251 249 h_mk_coloured_graph colouring0 spilled_no0 __ __ 252 250 … … 254 252 Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ -> 255 253 __ -> 'a1) -> coloured_graph -> 'a1 **) 256 let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_ 5836=257 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 5836in254 let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_78 = 255 let { colouring = colouring0; spilled_no = spilled_no0 } = x_78 in 258 256 h_mk_coloured_graph colouring0 spilled_no0 __ __ 259 257
Note: See TracChangeset
for help on using the changeset viewer.