Changeset 3019 for extracted/joint_LTL_LIN.ml
 Timestamp:
 Mar 28, 2013, 5:27:46 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/joint_LTL_LIN.ml
r3001 r3019 130 130 BitVector.byte > 'a1) > registers_move > 'a1 **) 131 131 let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function 132  From_acc (x_ 5280, x_5279) > h_from_acc x_5280 x_5279133  To_acc (x_ 5282, x_5281) > h_to_acc x_5282 x_5281134  Int_to_reg (x_ 5284, x_5283) > h_int_to_reg x_5284 x_5283135  Int_to_acc (x_ 5286, x_5285) > h_int_to_acc x_5286 x_5285132  From_acc (x_16, x_15) > h_from_acc x_16 x_15 133  To_acc (x_18, x_17) > h_to_acc x_18 x_17 134  Int_to_reg (x_20, x_19) > h_int_to_reg x_20 x_19 135  Int_to_acc (x_22, x_21) > h_int_to_acc x_22 x_21 136 136 137 137 (** val registers_move_rect_Type5 : … … 140 140 BitVector.byte > 'a1) > registers_move > 'a1 **) 141 141 let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function 142  From_acc (x_ 5293, x_5292) > h_from_acc x_5293 x_5292143  To_acc (x_ 5295, x_5294) > h_to_acc x_5295 x_5294144  Int_to_reg (x_ 5297, x_5296) > h_int_to_reg x_5297 x_5296145  Int_to_acc (x_ 5299, x_5298) > h_int_to_acc x_5299 x_5298142  From_acc (x_29, x_28) > h_from_acc x_29 x_28 143  To_acc (x_31, x_30) > h_to_acc x_31 x_30 144  Int_to_reg (x_33, x_32) > h_int_to_reg x_33 x_32 145  Int_to_acc (x_35, x_34) > h_int_to_acc x_35 x_34 146 146 147 147 (** val registers_move_rect_Type3 : … … 150 150 BitVector.byte > 'a1) > registers_move > 'a1 **) 151 151 let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function 152  From_acc (x_ 5306, x_5305) > h_from_acc x_5306 x_5305153  To_acc (x_ 5308, x_5307) > h_to_acc x_5308 x_5307154  Int_to_reg (x_ 5310, x_5309) > h_int_to_reg x_5310 x_5309155  Int_to_acc (x_ 5312, x_5311) > h_int_to_acc x_5312 x_5311152  From_acc (x_42, x_41) > h_from_acc x_42 x_41 153  To_acc (x_44, x_43) > h_to_acc x_44 x_43 154  Int_to_reg (x_46, x_45) > h_int_to_reg x_46 x_45 155  Int_to_acc (x_48, x_47) > h_int_to_acc x_48 x_47 156 156 157 157 (** val registers_move_rect_Type2 : … … 160 160 BitVector.byte > 'a1) > registers_move > 'a1 **) 161 161 let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function 162  From_acc (x_5 319, x_5318) > h_from_acc x_5319 x_5318163  To_acc (x_5 321, x_5320) > h_to_acc x_5321 x_5320164  Int_to_reg (x_5 323, x_5322) > h_int_to_reg x_5323 x_5322165  Int_to_acc (x_ 5325, x_5324) > h_int_to_acc x_5325 x_5324162  From_acc (x_55, x_54) > h_from_acc x_55 x_54 163  To_acc (x_57, x_56) > h_to_acc x_57 x_56 164  Int_to_reg (x_59, x_58) > h_int_to_reg x_59 x_58 165  Int_to_acc (x_61, x_60) > h_int_to_acc x_61 x_60 166 166 167 167 (** val registers_move_rect_Type1 : … … 170 170 BitVector.byte > 'a1) > registers_move > 'a1 **) 171 171 let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function 172  From_acc (x_ 5332, x_5331) > h_from_acc x_5332 x_5331173  To_acc (x_ 5334, x_5333) > h_to_acc x_5334 x_5333174  Int_to_reg (x_ 5336, x_5335) > h_int_to_reg x_5336 x_5335175  Int_to_acc (x_ 5338, x_5337) > h_int_to_acc x_5338 x_5337172  From_acc (x_68, x_67) > h_from_acc x_68 x_67 173  To_acc (x_70, x_69) > h_to_acc x_70 x_69 174  Int_to_reg (x_72, x_71) > h_int_to_reg x_72 x_71 175  Int_to_acc (x_74, x_73) > h_int_to_acc x_74 x_73 176 176 177 177 (** val registers_move_rect_Type0 : … … 180 180 BitVector.byte > 'a1) > registers_move > 'a1 **) 181 181 let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function 182  From_acc (x_ 5345, x_5344) > h_from_acc x_5345 x_5344183  To_acc (x_ 5347, x_5346) > h_to_acc x_5347 x_5346184  Int_to_reg (x_ 5349, x_5348) > h_int_to_reg x_5349 x_5348185  Int_to_acc (x_ 5351, x_5350) > h_int_to_acc x_5351 x_5350182  From_acc (x_81, x_80) > h_from_acc x_81 x_80 183  To_acc (x_83, x_82) > h_to_acc x_83 x_82 184  Int_to_reg (x_85, x_84) > h_int_to_reg x_85 x_84 185  Int_to_acc (x_87, x_86) > h_int_to_acc x_87 x_86 186 186 187 187 (** val registers_move_inv_rect_Type4 : … … 246 246  SAVE_CARRY 247 247  RESTORE_CARRY 248  LOW_ADDRESS of I8051.register *Graphs.label249  HIGH_ADDRESS of I8051.register *Graphs.label248  LOW_ADDRESS of Graphs.label 249  HIGH_ADDRESS of Graphs.label 250 250 251 251 (** val ltl_lin_seq_rect_Type4 : 252 'a1 > 'a1 > ( I8051.register > Graphs.label > 'a1) > (I8051.register253 > Graphs.label > 'a1) >ltl_lin_seq > 'a1 **)252 'a1 > 'a1 > (Graphs.label > 'a1) > (Graphs.label > 'a1) > 253 ltl_lin_seq > 'a1 **) 254 254 let rec ltl_lin_seq_rect_Type4 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function 255 255  SAVE_CARRY > h_SAVE_CARRY 256 256  RESTORE_CARRY > h_RESTORE_CARRY 257  LOW_ADDRESS (x_5445, x_5444) > h_LOW_ADDRESS x_5445 x_5444258  HIGH_ADDRESS (x_5447, x_5446) > h_HIGH_ADDRESS x_5447 x_5446257  LOW_ADDRESS x_178 > h_LOW_ADDRESS x_178 258  HIGH_ADDRESS x_179 > h_HIGH_ADDRESS x_179 259 259 260 260 (** val ltl_lin_seq_rect_Type5 : 261 'a1 > 'a1 > ( I8051.register > Graphs.label > 'a1) > (I8051.register262 > Graphs.label > 'a1) >ltl_lin_seq > 'a1 **)261 'a1 > 'a1 > (Graphs.label > 'a1) > (Graphs.label > 'a1) > 262 ltl_lin_seq > 'a1 **) 263 263 let rec ltl_lin_seq_rect_Type5 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function 264 264  SAVE_CARRY > h_SAVE_CARRY 265 265  RESTORE_CARRY > h_RESTORE_CARRY 266  LOW_ADDRESS (x_5454, x_5453) > h_LOW_ADDRESS x_5454 x_5453267  HIGH_ADDRESS (x_5456, x_5455) > h_HIGH_ADDRESS x_5456 x_5455266  LOW_ADDRESS x_185 > h_LOW_ADDRESS x_185 267  HIGH_ADDRESS x_186 > h_HIGH_ADDRESS x_186 268 268 269 269 (** val ltl_lin_seq_rect_Type3 : 270 'a1 > 'a1 > ( I8051.register > Graphs.label > 'a1) > (I8051.register271 > Graphs.label > 'a1) >ltl_lin_seq > 'a1 **)270 'a1 > 'a1 > (Graphs.label > 'a1) > (Graphs.label > 'a1) > 271 ltl_lin_seq > 'a1 **) 272 272 let rec ltl_lin_seq_rect_Type3 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function 273 273  SAVE_CARRY > h_SAVE_CARRY 274 274  RESTORE_CARRY > h_RESTORE_CARRY 275  LOW_ADDRESS (x_5463, x_5462) > h_LOW_ADDRESS x_5463 x_5462276  HIGH_ADDRESS (x_5465, x_5464) > h_HIGH_ADDRESS x_5465 x_5464275  LOW_ADDRESS x_192 > h_LOW_ADDRESS x_192 276  HIGH_ADDRESS x_193 > h_HIGH_ADDRESS x_193 277 277 278 278 (** val ltl_lin_seq_rect_Type2 : 279 'a1 > 'a1 > ( I8051.register > Graphs.label > 'a1) > (I8051.register280 > Graphs.label > 'a1) >ltl_lin_seq > 'a1 **)279 'a1 > 'a1 > (Graphs.label > 'a1) > (Graphs.label > 'a1) > 280 ltl_lin_seq > 'a1 **) 281 281 let rec ltl_lin_seq_rect_Type2 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function 282 282  SAVE_CARRY > h_SAVE_CARRY 283 283  RESTORE_CARRY > h_RESTORE_CARRY 284  LOW_ADDRESS (x_5472, x_5471) > h_LOW_ADDRESS x_5472 x_5471285  HIGH_ADDRESS (x_5474, x_5473) > h_HIGH_ADDRESS x_5474 x_5473284  LOW_ADDRESS x_199 > h_LOW_ADDRESS x_199 285  HIGH_ADDRESS x_200 > h_HIGH_ADDRESS x_200 286 286 287 287 (** val ltl_lin_seq_rect_Type1 : 288 'a1 > 'a1 > ( I8051.register > Graphs.label > 'a1) > (I8051.register289 > Graphs.label > 'a1) >ltl_lin_seq > 'a1 **)288 'a1 > 'a1 > (Graphs.label > 'a1) > (Graphs.label > 'a1) > 289 ltl_lin_seq > 'a1 **) 290 290 let rec ltl_lin_seq_rect_Type1 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function 291 291  SAVE_CARRY > h_SAVE_CARRY 292 292  RESTORE_CARRY > h_RESTORE_CARRY 293  LOW_ADDRESS (x_5481, x_5480) > h_LOW_ADDRESS x_5481 x_5480294  HIGH_ADDRESS (x_5483, x_5482) > h_HIGH_ADDRESS x_5483 x_5482293  LOW_ADDRESS x_206 > h_LOW_ADDRESS x_206 294  HIGH_ADDRESS x_207 > h_HIGH_ADDRESS x_207 295 295 296 296 (** val ltl_lin_seq_rect_Type0 : 297 'a1 > 'a1 > ( I8051.register > Graphs.label > 'a1) > (I8051.register298 > Graphs.label > 'a1) >ltl_lin_seq > 'a1 **)297 'a1 > 'a1 > (Graphs.label > 'a1) > (Graphs.label > 'a1) > 298 ltl_lin_seq > 'a1 **) 299 299 let rec ltl_lin_seq_rect_Type0 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function 300 300  SAVE_CARRY > h_SAVE_CARRY 301 301  RESTORE_CARRY > h_RESTORE_CARRY 302  LOW_ADDRESS (x_5490, x_5489) > h_LOW_ADDRESS x_5490 x_5489303  HIGH_ADDRESS (x_5492, x_5491) > h_HIGH_ADDRESS x_5492 x_5491302  LOW_ADDRESS x_213 > h_LOW_ADDRESS x_213 303  HIGH_ADDRESS x_214 > h_HIGH_ADDRESS x_214 304 304 305 305 (** val ltl_lin_seq_inv_rect_Type4 : 306 ltl_lin_seq > (__ > 'a1) > (__ > 'a1) > (I8051.register > 307 Graphs.label > __ > 'a1) > (I8051.register > Graphs.label > __ > 308 'a1) > 'a1 **) 306 ltl_lin_seq > (__ > 'a1) > (__ > 'a1) > (Graphs.label > __ > 'a1) 307 > (Graphs.label > __ > 'a1) > 'a1 **) 309 308 let ltl_lin_seq_inv_rect_Type4 hterm h1 h2 h3 h4 = 310 309 let hcut = ltl_lin_seq_rect_Type4 h1 h2 h3 h4 hterm in hcut __ 311 310 312 311 (** val ltl_lin_seq_inv_rect_Type3 : 313 ltl_lin_seq > (__ > 'a1) > (__ > 'a1) > (I8051.register > 314 Graphs.label > __ > 'a1) > (I8051.register > Graphs.label > __ > 315 'a1) > 'a1 **) 312 ltl_lin_seq > (__ > 'a1) > (__ > 'a1) > (Graphs.label > __ > 'a1) 313 > (Graphs.label > __ > 'a1) > 'a1 **) 316 314 let ltl_lin_seq_inv_rect_Type3 hterm h1 h2 h3 h4 = 317 315 let hcut = ltl_lin_seq_rect_Type3 h1 h2 h3 h4 hterm in hcut __ 318 316 319 317 (** val ltl_lin_seq_inv_rect_Type2 : 320 ltl_lin_seq > (__ > 'a1) > (__ > 'a1) > (I8051.register > 321 Graphs.label > __ > 'a1) > (I8051.register > Graphs.label > __ > 322 'a1) > 'a1 **) 318 ltl_lin_seq > (__ > 'a1) > (__ > 'a1) > (Graphs.label > __ > 'a1) 319 > (Graphs.label > __ > 'a1) > 'a1 **) 323 320 let ltl_lin_seq_inv_rect_Type2 hterm h1 h2 h3 h4 = 324 321 let hcut = ltl_lin_seq_rect_Type2 h1 h2 h3 h4 hterm in hcut __ 325 322 326 323 (** val ltl_lin_seq_inv_rect_Type1 : 327 ltl_lin_seq > (__ > 'a1) > (__ > 'a1) > (I8051.register > 328 Graphs.label > __ > 'a1) > (I8051.register > Graphs.label > __ > 329 'a1) > 'a1 **) 324 ltl_lin_seq > (__ > 'a1) > (__ > 'a1) > (Graphs.label > __ > 'a1) 325 > (Graphs.label > __ > 'a1) > 'a1 **) 330 326 let ltl_lin_seq_inv_rect_Type1 hterm h1 h2 h3 h4 = 331 327 let hcut = ltl_lin_seq_rect_Type1 h1 h2 h3 h4 hterm in hcut __ 332 328 333 329 (** val ltl_lin_seq_inv_rect_Type0 : 334 ltl_lin_seq > (__ > 'a1) > (__ > 'a1) > (I8051.register > 335 Graphs.label > __ > 'a1) > (I8051.register > Graphs.label > __ > 336 'a1) > 'a1 **) 330 ltl_lin_seq > (__ > 'a1) > (__ > 'a1) > (Graphs.label > __ > 'a1) 331 > (Graphs.label > __ > 'a1) > 'a1 **) 337 332 let ltl_lin_seq_inv_rect_Type0 hterm h1 h2 h3 h4 = 338 333 let hcut = ltl_lin_seq_rect_Type0 h1 h2 h3 h4 hterm in hcut __ … … 344 339  SAVE_CARRY > Obj.magic (fun _ dH > dH) 345 340  RESTORE_CARRY > Obj.magic (fun _ dH > dH) 346  LOW_ADDRESS (a0, a1) > Obj.magic (fun _ dH > dH ____)347  HIGH_ADDRESS (a0, a1) > Obj.magic (fun _ dH > dH ____)) y341  LOW_ADDRESS a0 > Obj.magic (fun _ dH > dH __) 342  HIGH_ADDRESS a0 > Obj.magic (fun _ dH > dH __)) y 348 343 349 344 (** val ltl_lin_seq_jmdiscr : ltl_lin_seq > ltl_lin_seq > __ **) … … 353 348  SAVE_CARRY > Obj.magic (fun _ dH > dH) 354 349  RESTORE_CARRY > Obj.magic (fun _ dH > dH) 355  LOW_ADDRESS (a0, a1) > Obj.magic (fun _ dH > dH ____)356  HIGH_ADDRESS (a0, a1) > Obj.magic (fun _ dH > dH ____)) y350  LOW_ADDRESS a0 > Obj.magic (fun _ dH > dH __) 351  HIGH_ADDRESS a0 > Obj.magic (fun _ dH > dH __)) y 357 352 358 353 (** val ltl_lin_seq_labels : ltl_lin_seq > Graphs.label List.list **) … … 360 355  SAVE_CARRY > List.Nil 361 356  RESTORE_CARRY > List.Nil 362  LOW_ADDRESS (x, lbl)> List.Cons (lbl, List.Nil)363  HIGH_ADDRESS (x, lbl)> List.Cons (lbl, List.Nil)357  LOW_ADDRESS lbl > List.Cons (lbl, List.Nil) 358  HIGH_ADDRESS lbl > List.Cons (lbl, List.Nil) 364 359 365 360 (** val lTL_LIN_uns : Joint.unserialized_params **)
Note: See TracChangeset
for help on using the changeset viewer.