Changeset 2743 for extracted/rTL.ml


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/rTL.ml

    r2730 r2743  
    111111    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    112112let rec rtl_seq_rect_Type4 h_rtl_stack_address = function
    113 | Rtl_stack_address (x_581, x_580) -> h_rtl_stack_address x_581 x_580
     113| Rtl_stack_address (x_20569, x_20568) -> h_rtl_stack_address x_20569 x_20568
    114114
    115115(** val rtl_seq_rect_Type5 :
    116116    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    117117let rec rtl_seq_rect_Type5 h_rtl_stack_address = function
    118 | Rtl_stack_address (x_585, x_584) -> h_rtl_stack_address x_585 x_584
     118| Rtl_stack_address (x_20573, x_20572) -> h_rtl_stack_address x_20573 x_20572
    119119
    120120(** val rtl_seq_rect_Type3 :
    121121    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    122122let rec rtl_seq_rect_Type3 h_rtl_stack_address = function
    123 | Rtl_stack_address (x_589, x_588) -> h_rtl_stack_address x_589 x_588
     123| Rtl_stack_address (x_20577, x_20576) -> h_rtl_stack_address x_20577 x_20576
    124124
    125125(** val rtl_seq_rect_Type2 :
    126126    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    127127let rec rtl_seq_rect_Type2 h_rtl_stack_address = function
    128 | Rtl_stack_address (x_593, x_592) -> h_rtl_stack_address x_593 x_592
     128| Rtl_stack_address (x_20581, x_20580) -> h_rtl_stack_address x_20581 x_20580
    129129
    130130(** val rtl_seq_rect_Type1 :
    131131    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    132132let rec rtl_seq_rect_Type1 h_rtl_stack_address = function
    133 | Rtl_stack_address (x_597, x_596) -> h_rtl_stack_address x_597 x_596
     133| Rtl_stack_address (x_20585, x_20584) -> h_rtl_stack_address x_20585 x_20584
    134134
    135135(** val rtl_seq_rect_Type0 :
    136136    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    137137let rec rtl_seq_rect_Type0 h_rtl_stack_address = function
    138 | Rtl_stack_address (x_601, x_600) -> h_rtl_stack_address x_601 x_600
     138| Rtl_stack_address (x_20589, x_20588) -> h_rtl_stack_address x_20589 x_20588
    139139
    140140(** val rtl_seq_inv_rect_Type4 :
     
    186186type rtl_program = Joint.joint_program
    187187
     188(** val dpi1__o__reg_to_rtl_snd_argument__o__inject :
     189    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
     190let dpi1__o__reg_to_rtl_snd_argument__o__inject x2 =
     191  Joint.psd_argument_from_reg x2.Types.dpi1
     192
     193(** val eject__o__reg_to_rtl_snd_argument__o__inject :
     194    Registers.register Types.sig0 -> Joint.psd_argument Types.sig0 **)
     195let eject__o__reg_to_rtl_snd_argument__o__inject x2 =
     196  Joint.psd_argument_from_reg (Types.pi1 x2)
     197
     198(** val reg_to_rtl_snd_argument__o__inject :
     199    Registers.register -> Joint.psd_argument Types.sig0 **)
     200let reg_to_rtl_snd_argument__o__inject x1 =
     201  Joint.psd_argument_from_reg x1
     202
     203(** val dpi1__o__reg_to_rtl_snd_argument :
     204    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument **)
     205let dpi1__o__reg_to_rtl_snd_argument x1 =
     206  Joint.psd_argument_from_reg x1.Types.dpi1
     207
     208(** val eject__o__reg_to_rtl_snd_argument :
     209    Registers.register Types.sig0 -> Joint.psd_argument **)
     210let eject__o__reg_to_rtl_snd_argument x1 =
     211  Joint.psd_argument_from_reg (Types.pi1 x1)
     212
     213(** val dpi1__o__byte_to_rtl_snd_argument__o__inject :
     214    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
     215let dpi1__o__byte_to_rtl_snd_argument__o__inject x2 =
     216  Joint.psd_argument_from_byte x2.Types.dpi1
     217
     218(** val eject__o__byte_to_rtl_snd_argument__o__inject :
     219    BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0 **)
     220let eject__o__byte_to_rtl_snd_argument__o__inject x2 =
     221  Joint.psd_argument_from_byte (Types.pi1 x2)
     222
     223(** val byte_to_rtl_snd_argument__o__inject :
     224    BitVector.byte -> Joint.psd_argument Types.sig0 **)
     225let byte_to_rtl_snd_argument__o__inject x1 =
     226  Joint.psd_argument_from_byte x1
     227
     228(** val dpi1__o__byte_to_rtl_snd_argument :
     229    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument **)
     230let dpi1__o__byte_to_rtl_snd_argument x1 =
     231  Joint.psd_argument_from_byte x1.Types.dpi1
     232
     233(** val eject__o__byte_to_rtl_snd_argument :
     234    BitVector.byte Types.sig0 -> Joint.psd_argument **)
     235let eject__o__byte_to_rtl_snd_argument x1 =
     236  Joint.psd_argument_from_byte (Types.pi1 x1)
     237
Note: See TracChangeset for help on using the changeset viewer.