Changeset 2743 for extracted/eRTLptrToLTL.ml
- Timestamp:
- Feb 27, 2013, 9:27:58 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
extracted/eRTLptrToLTL.ml
r2740 r2743 132 132 133 133 open TranslateUtils 134 135 (** val dpi1__o__Reg_to_dec__o__inject : 136 (I8051.register, 'a1) Types.dPair -> Interference.decision Types.sig0 **) 137 let dpi1__o__Reg_to_dec__o__inject x2 = 138 Interference.Decision_colour x2.Types.dpi1 139 140 (** val eject__o__Reg_to_dec__o__inject : 141 I8051.register Types.sig0 -> Interference.decision Types.sig0 **) 142 let eject__o__Reg_to_dec__o__inject x2 = 143 Interference.Decision_colour (Types.pi1 x2) 144 145 (** val reg_to_dec__o__inject : 146 I8051.register -> Interference.decision Types.sig0 **) 147 let reg_to_dec__o__inject x1 = 148 Interference.Decision_colour x1 149 150 (** val dpi1__o__Reg_to_dec : 151 (I8051.register, 'a1) Types.dPair -> Interference.decision **) 152 let dpi1__o__Reg_to_dec x1 = 153 Interference.Decision_colour x1.Types.dpi1 154 155 (** val eject__o__Reg_to_dec : 156 I8051.register Types.sig0 -> Interference.decision **) 157 let eject__o__Reg_to_dec x1 = 158 Interference.Decision_colour (Types.pi1 x1) 134 159 135 160 type arg_decision = … … 142 167 arg_decision -> 'a1 **) 143 168 let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 144 | Arg_decision_colour x_ 492 -> h_arg_decision_colour x_492145 | Arg_decision_spill x_ 493 -> h_arg_decision_spill x_493146 | Arg_decision_imm x_ 494 -> h_arg_decision_imm x_494169 | Arg_decision_colour x_21681 -> h_arg_decision_colour x_21681 170 | Arg_decision_spill x_21682 -> h_arg_decision_spill x_21682 171 | Arg_decision_imm x_21683 -> h_arg_decision_imm x_21683 147 172 148 173 (** val arg_decision_rect_Type5 : … … 150 175 arg_decision -> 'a1 **) 151 176 let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 152 | Arg_decision_colour x_ 499 -> h_arg_decision_colour x_499153 | Arg_decision_spill x_ 500 -> h_arg_decision_spill x_500154 | Arg_decision_imm x_ 501 -> h_arg_decision_imm x_501177 | Arg_decision_colour x_21688 -> h_arg_decision_colour x_21688 178 | Arg_decision_spill x_21689 -> h_arg_decision_spill x_21689 179 | Arg_decision_imm x_21690 -> h_arg_decision_imm x_21690 155 180 156 181 (** val arg_decision_rect_Type3 : … … 158 183 arg_decision -> 'a1 **) 159 184 let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 160 | Arg_decision_colour x_ 506 -> h_arg_decision_colour x_506161 | Arg_decision_spill x_ 507 -> h_arg_decision_spill x_507162 | Arg_decision_imm x_ 508 -> h_arg_decision_imm x_508185 | Arg_decision_colour x_21695 -> h_arg_decision_colour x_21695 186 | Arg_decision_spill x_21696 -> h_arg_decision_spill x_21696 187 | Arg_decision_imm x_21697 -> h_arg_decision_imm x_21697 163 188 164 189 (** val arg_decision_rect_Type2 : … … 166 191 arg_decision -> 'a1 **) 167 192 let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 168 | Arg_decision_colour x_ 513 -> h_arg_decision_colour x_513169 | Arg_decision_spill x_ 514 -> h_arg_decision_spill x_514170 | Arg_decision_imm x_ 515 -> h_arg_decision_imm x_515193 | Arg_decision_colour x_21702 -> h_arg_decision_colour x_21702 194 | Arg_decision_spill x_21703 -> h_arg_decision_spill x_21703 195 | Arg_decision_imm x_21704 -> h_arg_decision_imm x_21704 171 196 172 197 (** val arg_decision_rect_Type1 : … … 174 199 arg_decision -> 'a1 **) 175 200 let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 176 | Arg_decision_colour x_ 520 -> h_arg_decision_colour x_520177 | Arg_decision_spill x_ 521 -> h_arg_decision_spill x_521178 | Arg_decision_imm x_ 522 -> h_arg_decision_imm x_522201 | Arg_decision_colour x_21709 -> h_arg_decision_colour x_21709 202 | Arg_decision_spill x_21710 -> h_arg_decision_spill x_21710 203 | Arg_decision_imm x_21711 -> h_arg_decision_imm x_21711 179 204 180 205 (** val arg_decision_rect_Type0 : … … 182 207 arg_decision -> 'a1 **) 183 208 let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 184 | Arg_decision_colour x_ 527 -> h_arg_decision_colour x_527185 | Arg_decision_spill x_ 528 -> h_arg_decision_spill x_528186 | Arg_decision_imm x_ 529 -> h_arg_decision_imm x_529209 | Arg_decision_colour x_21716 -> h_arg_decision_colour x_21716 210 | Arg_decision_spill x_21717 -> h_arg_decision_spill x_21717 211 | Arg_decision_imm x_21718 -> h_arg_decision_imm x_21718 187 212 188 213 (** val arg_decision_inv_rect_Type4 : … … 231 256 | Arg_decision_spill a0 -> Obj.magic (fun _ dH -> dH __) 232 257 | Arg_decision_imm a0 -> Obj.magic (fun _ dH -> dH __)) y 258 259 (** val dpi1__o__Reg_to_arg_dec__o__inject : 260 (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0 **) 261 let dpi1__o__Reg_to_arg_dec__o__inject x2 = 262 Arg_decision_colour x2.Types.dpi1 263 264 (** val eject__o__Reg_to_arg_dec__o__inject : 265 I8051.register Types.sig0 -> arg_decision Types.sig0 **) 266 let eject__o__Reg_to_arg_dec__o__inject x2 = 267 Arg_decision_colour (Types.pi1 x2) 268 269 (** val reg_to_arg_dec__o__inject : 270 I8051.register -> arg_decision Types.sig0 **) 271 let reg_to_arg_dec__o__inject x1 = 272 Arg_decision_colour x1 273 274 (** val dpi1__o__Reg_to_arg_dec : 275 (I8051.register, 'a1) Types.dPair -> arg_decision **) 276 let dpi1__o__Reg_to_arg_dec x1 = 277 Arg_decision_colour x1.Types.dpi1 278 279 (** val eject__o__Reg_to_arg_dec : 280 I8051.register Types.sig0 -> arg_decision **) 281 let eject__o__Reg_to_arg_dec x1 = 282 Arg_decision_colour (Types.pi1 x1) 233 283 234 284 (** val preserve_carry_bit : … … 246 296 let a = 247 297 Types.It 298 299 (** val dpi1__o__beval_of_byte__o__inject : 300 (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval Types.sig0 **) 301 let dpi1__o__beval_of_byte__o__inject x2 = 302 ByteValues.BVByte x2.Types.dpi1 303 304 (** val eject__o__beval_of_byte__o__inject : 305 BitVector.byte Types.sig0 -> ByteValues.beval Types.sig0 **) 306 let eject__o__beval_of_byte__o__inject x2 = 307 ByteValues.BVByte (Types.pi1 x2) 308 309 (** val beval_of_byte__o__inject : 310 BitVector.byte -> ByteValues.beval Types.sig0 **) 311 let beval_of_byte__o__inject x1 = 312 ByteValues.BVByte x1 313 314 (** val dpi1__o__beval_of_byte : 315 (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval **) 316 let dpi1__o__beval_of_byte x1 = 317 ByteValues.BVByte x1.Types.dpi1 318 319 (** val eject__o__beval_of_byte : 320 BitVector.byte Types.sig0 -> ByteValues.beval **) 321 let eject__o__beval_of_byte x1 = 322 ByteValues.BVByte (Types.pi1 x1) 248 323 249 324 (** val set_dp_by_offset : … … 514 589 | Interference.Decision_colour r -> Arg_decision_colour r 515 590 591 (** val reg_to_dec__o__dec_arg_dec__o__inject : 592 I8051.register -> arg_decision Types.sig0 **) 593 let reg_to_dec__o__dec_arg_dec__o__inject x0 = 594 dec_to_arg_dec (Interference.Decision_colour x0) 595 596 (** val dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject : 597 (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0 **) 598 let dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 = 599 dec_to_arg_dec (dpi1__o__Reg_to_dec x2) 600 601 (** val eject__o__Reg_to_dec__o__dec_arg_dec__o__inject : 602 I8051.register Types.sig0 -> arg_decision Types.sig0 **) 603 let eject__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 = 604 dec_to_arg_dec (eject__o__Reg_to_dec x2) 605 606 (** val dpi1__o__dec_arg_dec__o__inject : 607 (Interference.decision, 'a1) Types.dPair -> arg_decision Types.sig0 **) 608 let dpi1__o__dec_arg_dec__o__inject x2 = 609 dec_to_arg_dec x2.Types.dpi1 610 611 (** val eject__o__dec_arg_dec__o__inject : 612 Interference.decision Types.sig0 -> arg_decision Types.sig0 **) 613 let eject__o__dec_arg_dec__o__inject x2 = 614 dec_to_arg_dec (Types.pi1 x2) 615 616 (** val dec_arg_dec__o__inject : 617 Interference.decision -> arg_decision Types.sig0 **) 618 let dec_arg_dec__o__inject x1 = 619 dec_to_arg_dec x1 620 621 (** val reg_to_dec__o__dec_arg_dec : I8051.register -> arg_decision **) 622 let reg_to_dec__o__dec_arg_dec x0 = 623 dec_to_arg_dec (Interference.Decision_colour x0) 624 625 (** val dpi1__o__Reg_to_dec__o__dec_arg_dec : 626 (I8051.register, 'a1) Types.dPair -> arg_decision **) 627 let dpi1__o__Reg_to_dec__o__dec_arg_dec x1 = 628 dec_to_arg_dec (dpi1__o__Reg_to_dec x1) 629 630 (** val eject__o__Reg_to_dec__o__dec_arg_dec : 631 I8051.register Types.sig0 -> arg_decision **) 632 let eject__o__Reg_to_dec__o__dec_arg_dec x1 = 633 dec_to_arg_dec (eject__o__Reg_to_dec x1) 634 635 (** val dpi1__o__dec_arg_dec : 636 (Interference.decision, 'a1) Types.dPair -> arg_decision **) 637 let dpi1__o__dec_arg_dec x1 = 638 dec_to_arg_dec x1.Types.dpi1 639 640 (** val eject__o__dec_arg_dec : 641 Interference.decision Types.sig0 -> arg_decision **) 642 let eject__o__dec_arg_dec x1 = 643 dec_to_arg_dec (Types.pi1 x1) 644 516 645 (** val translate_op1 : 517 646 AST.ident List.list -> Bool.bool -> BackEndOps.op1 ->
Note: See TracChangeset
for help on using the changeset viewer.