Changeset 2773 for extracted/interference.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/interference.ml
r2743 r2773 13 13 open LabelledObjects 14 14 15 open BitVectorTrie 16 15 17 open Graphs 16 18 … … 21 23 open Registers 22 24 23 open BitVectorTrie24 25 25 open CostLabel 26 26 … … 41 41 open Extralib 42 42 43 open Lists 44 45 open Identifiers 46 47 open Integers 48 49 open AST 50 51 open Division 52 53 open Exp 54 55 open Arithmetic 56 43 57 open Setoids 44 58 … … 46 60 47 61 open Option 48 49 open Lists50 51 open Identifiers52 53 open Integers54 55 open AST56 57 open Division58 59 open Exp60 61 open Arithmetic62 62 63 63 open Extranat … … 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_ 21583 > h_decision_spill x_21583125  Decision_colour x_ 21584 > h_decision_colour x_21584124  Decision_spill x_16893 > h_decision_spill x_16893 125  Decision_colour x_16894 > h_decision_colour x_16894 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_ 21588 > h_decision_spill x_21588131  Decision_colour x_ 21589 > h_decision_colour x_21589130  Decision_spill x_16898 > h_decision_spill x_16898 131  Decision_colour x_16899 > h_decision_colour x_16899 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_ 21593 > h_decision_spill x_21593137  Decision_colour x_ 21594 > h_decision_colour x_21594136  Decision_spill x_16903 > h_decision_spill x_16903 137  Decision_colour x_16904 > h_decision_colour x_16904 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_ 21598 > h_decision_spill x_21598143  Decision_colour x_ 21599 > h_decision_colour x_21599142  Decision_spill x_16908 > h_decision_spill x_16908 143  Decision_colour x_16909 > h_decision_colour x_16909 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_ 21603 > h_decision_spill x_21603149  Decision_colour x_ 21604 > h_decision_colour x_21604148  Decision_spill x_16913 > h_decision_spill x_16913 149  Decision_colour x_16914 > h_decision_colour x_16914 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_ 21608 > h_decision_spill x_21608155  Decision_colour x_ 21609 > h_decision_colour x_21609154  Decision_spill x_16918 > h_decision_spill x_16918 155  Decision_colour x_16919 > h_decision_colour x_16919 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_ 21644 =208 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 21644 in207 let rec coloured_graph_rect_Type4 after h_mk_coloured_graph x_16954 = 208 let { colouring = colouring0; spilled_no = spilled_no0 } = x_16954 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_ 21646 =215 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 21646 in214 let rec coloured_graph_rect_Type5 after h_mk_coloured_graph x_16956 = 215 let { colouring = colouring0; spilled_no = spilled_no0 } = x_16956 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_ 21648 =222 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 21648 in221 let rec coloured_graph_rect_Type3 after h_mk_coloured_graph x_16958 = 222 let { colouring = colouring0; spilled_no = spilled_no0 } = x_16958 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_ 21650 =229 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 21650 in228 let rec coloured_graph_rect_Type2 after h_mk_coloured_graph x_16960 = 229 let { colouring = colouring0; spilled_no = spilled_no0 } = x_16960 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_ 21652 =236 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 21652 in235 let rec coloured_graph_rect_Type1 after h_mk_coloured_graph x_16962 = 236 let { colouring = colouring0; spilled_no = spilled_no0 } = x_16962 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_ 21654 =243 let { colouring = colouring0; spilled_no = spilled_no0 } = x_ 21654 in242 let rec coloured_graph_rect_Type0 after h_mk_coloured_graph x_16964 = 243 let { colouring = colouring0; spilled_no = spilled_no0 } = x_16964 in 244 244 h_mk_coloured_graph colouring0 spilled_no0 __ __ 245 245
Note: See TracChangeset
for help on using the changeset viewer.