Changeset 2951 for extracted/interference.ml
 Timestamp:
 Mar 25, 2013, 11:30:01 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/interference.ml
r2873 r2951 4 4 5 5 open Set_adt 6 7 open Extra_bool 8 9 open Coqlib 10 11 open Values 12 13 open FrontEndVal 14 15 open GenMem 16 17 open FrontEndMem 18 19 open Globalenvs 6 20 7 21 open String … … 122 136 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 123 137 let rec decision_rect_Type4 h_decision_spill h_decision_colour = function 124  Decision_spill x_ 22007 > h_decision_spill x_22007125  Decision_colour x_ 22008 > h_decision_colour x_22008138  Decision_spill x_19110 > h_decision_spill x_19110 139  Decision_colour x_19111 > h_decision_colour x_19111 126 140 127 141 (** val decision_rect_Type5 : 128 142 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 129 143 let rec decision_rect_Type5 h_decision_spill h_decision_colour = function 130  Decision_spill x_ 22012 > h_decision_spill x_22012131  Decision_colour x_ 22013 > h_decision_colour x_22013144  Decision_spill x_19115 > h_decision_spill x_19115 145  Decision_colour x_19116 > h_decision_colour x_19116 132 146 133 147 (** val decision_rect_Type3 : 134 148 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 135 149 let rec decision_rect_Type3 h_decision_spill h_decision_colour = function 136  Decision_spill x_ 22017 > h_decision_spill x_22017137  Decision_colour x_ 22018 > h_decision_colour x_22018150  Decision_spill x_19120 > h_decision_spill x_19120 151  Decision_colour x_19121 > h_decision_colour x_19121 138 152 139 153 (** val decision_rect_Type2 : 140 154 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 141 155 let rec decision_rect_Type2 h_decision_spill h_decision_colour = function 142  Decision_spill x_ 22022 > h_decision_spill x_22022143  Decision_colour x_ 22023 > h_decision_colour x_22023156  Decision_spill x_19125 > h_decision_spill x_19125 157  Decision_colour x_19126 > h_decision_colour x_19126 144 158 145 159 (** val decision_rect_Type1 : 146 160 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 147 161 let rec decision_rect_Type1 h_decision_spill h_decision_colour = function 148  Decision_spill x_ 22027 > h_decision_spill x_22027149  Decision_colour x_ 22028 > h_decision_colour x_22028162  Decision_spill x_19130 > h_decision_spill x_19130 163  Decision_colour x_19131 > h_decision_colour x_19131 150 164 151 165 (** val decision_rect_Type0 : 152 166 (Nat.nat > 'a1) > (I8051.register > 'a1) > decision > 'a1 **) 153 167 let rec decision_rect_Type0 h_decision_spill h_decision_colour = function 154  Decision_spill x_ 22032 > h_decision_spill x_22032155  Decision_colour x_ 22033 > h_decision_colour x_22033168  Decision_spill x_19135 > h_decision_spill x_19135 169  Decision_colour x_19136 > h_decision_colour x_19136 156 170 157 171 (** val decision_inv_rect_Type4 : … … 205 219 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 206 220 __ > 'a1) > coloured_graph > 'a1 **) 207 let rec coloured_graph_rect_Type4 after h_mk_coloured_graph x_22068=208 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 22068in221 let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_19171 = 222 let { colouring = colouring0; spilled_no = spilled_no0 } = x_19171 in 209 223 h_mk_coloured_graph colouring0 spilled_no0 __ __ 210 224 … … 212 226 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 213 227 __ > 'a1) > coloured_graph > 'a1 **) 214 let rec coloured_graph_rect_Type5 after h_mk_coloured_graph x_22070=215 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 22070in228 let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_19173 = 229 let { colouring = colouring0; spilled_no = spilled_no0 } = x_19173 in 216 230 h_mk_coloured_graph colouring0 spilled_no0 __ __ 217 231 … … 219 233 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 220 234 __ > 'a1) > coloured_graph > 'a1 **) 221 let rec coloured_graph_rect_Type3 after h_mk_coloured_graph x_22072=222 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 22072in235 let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_19175 = 236 let { colouring = colouring0; spilled_no = spilled_no0 } = x_19175 in 223 237 h_mk_coloured_graph colouring0 spilled_no0 __ __ 224 238 … … 226 240 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 227 241 __ > 'a1) > coloured_graph > 'a1 **) 228 let rec coloured_graph_rect_Type2 after h_mk_coloured_graph x_22074=229 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 22074in242 let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_19177 = 243 let { colouring = colouring0; spilled_no = spilled_no0 } = x_19177 in 230 244 h_mk_coloured_graph colouring0 spilled_no0 __ __ 231 245 … … 233 247 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 234 248 __ > 'a1) > coloured_graph > 'a1 **) 235 let rec coloured_graph_rect_Type1 after h_mk_coloured_graph x_22076=236 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 22076in249 let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_19179 = 250 let { colouring = colouring0; spilled_no = spilled_no0 } = x_19179 in 237 251 h_mk_coloured_graph colouring0 spilled_no0 __ __ 238 252 … … 240 254 Fixpoints.valuation > ((Liveness.vertex > decision) > Nat.nat > __ > 241 255 __ > 'a1) > coloured_graph > 'a1 **) 242 let rec coloured_graph_rect_Type0 after h_mk_coloured_graph x_22078=243 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 22078in256 let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_19181 = 257 let { colouring = colouring0; spilled_no = spilled_no0 } = x_19181 in 244 258 h_mk_coloured_graph colouring0 spilled_no0 __ __ 245 259 246 260 (** val colouring : 247 261 Fixpoints.valuation > coloured_graph > Liveness.vertex > decision **) 248 let rec colouring afterxxx =262 let rec colouring before xxx = 249 263 xxx.colouring 250 264 251 265 (** val spilled_no : Fixpoints.valuation > coloured_graph > Nat.nat **) 252 let rec spilled_no afterxxx =266 let rec spilled_no before xxx = 253 267 xxx.spilled_no 254 268
Note: See TracChangeset
for help on using the changeset viewer.