Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/eRTLptrToLTL.ml

    r2740 r2743  
    132132
    133133open TranslateUtils
     134
     135(** val dpi1__o__Reg_to_dec__o__inject :
     136    (I8051.register, 'a1) Types.dPair -> Interference.decision Types.sig0 **)
     137let 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 **)
     142let 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 **)
     147let 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 **)
     152let 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 **)
     157let eject__o__Reg_to_dec x1 =
     158  Interference.Decision_colour (Types.pi1 x1)
    134159
    135160type arg_decision =
     
    142167    arg_decision -> 'a1 **)
    143168let 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_492
    145 | Arg_decision_spill x_493 -> h_arg_decision_spill x_493
    146 | Arg_decision_imm x_494 -> h_arg_decision_imm x_494
     169| 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
    147172
    148173(** val arg_decision_rect_Type5 :
     
    150175    arg_decision -> 'a1 **)
    151176let 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_499
    153 | Arg_decision_spill x_500 -> h_arg_decision_spill x_500
    154 | Arg_decision_imm x_501 -> h_arg_decision_imm x_501
     177| 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
    155180
    156181(** val arg_decision_rect_Type3 :
     
    158183    arg_decision -> 'a1 **)
    159184let 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_506
    161 | Arg_decision_spill x_507 -> h_arg_decision_spill x_507
    162 | Arg_decision_imm x_508 -> h_arg_decision_imm x_508
     185| 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
    163188
    164189(** val arg_decision_rect_Type2 :
     
    166191    arg_decision -> 'a1 **)
    167192let 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_513
    169 | Arg_decision_spill x_514 -> h_arg_decision_spill x_514
    170 | Arg_decision_imm x_515 -> h_arg_decision_imm x_515
     193| 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
    171196
    172197(** val arg_decision_rect_Type1 :
     
    174199    arg_decision -> 'a1 **)
    175200let 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_520
    177 | Arg_decision_spill x_521 -> h_arg_decision_spill x_521
    178 | Arg_decision_imm x_522 -> h_arg_decision_imm x_522
     201| 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
    179204
    180205(** val arg_decision_rect_Type0 :
     
    182207    arg_decision -> 'a1 **)
    183208let 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_527
    185 | Arg_decision_spill x_528 -> h_arg_decision_spill x_528
    186 | Arg_decision_imm x_529 -> h_arg_decision_imm x_529
     209| 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
    187212
    188213(** val arg_decision_inv_rect_Type4 :
     
    231256     | Arg_decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
    232257     | 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 **)
     261let 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 **)
     266let 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 **)
     271let 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 **)
     276let 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 **)
     281let eject__o__Reg_to_arg_dec x1 =
     282  Arg_decision_colour (Types.pi1 x1)
    233283
    234284(** val preserve_carry_bit :
     
    246296let a =
    247297  Types.It
     298
     299(** val dpi1__o__beval_of_byte__o__inject :
     300    (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval Types.sig0 **)
     301let 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 **)
     306let 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 **)
     311let 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 **)
     316let 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 **)
     321let eject__o__beval_of_byte x1 =
     322  ByteValues.BVByte (Types.pi1 x1)
    248323
    249324(** val set_dp_by_offset :
     
    514589| Interference.Decision_colour r -> Arg_decision_colour r
    515590
     591(** val reg_to_dec__o__dec_arg_dec__o__inject :
     592    I8051.register -> arg_decision Types.sig0 **)
     593let 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 **)
     598let 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 **)
     603let 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 **)
     608let 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 **)
     613let 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 **)
     618let 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 **)
     622let 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 **)
     627let 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 **)
     632let 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 **)
     637let 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 **)
     642let eject__o__dec_arg_dec x1 =
     643  dec_to_arg_dec (Types.pi1 x1)
     644
    516645(** val translate_op1 :
    517646    AST.ident List.list -> Bool.bool -> BackEndOps.op1 ->
Note: See TracChangeset for help on using the changeset viewer.