Ignore:
Timestamp:
Mar 8, 2013, 9:07:28 PM (8 years ago)
Author:
sacerdot
Message:

Everything extracted again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabsToRTL.ml

    r2797 r2827  
    150150    -> 'a1) -> register_type -> 'a1 **)
    151151let rec register_type_rect_Type4 h_register_int h_register_ptr = function
    152 | Register_int x_21002 -> h_register_int x_21002
    153 | Register_ptr (x_21004, x_21003) -> h_register_ptr x_21004 x_21003
     152| Register_int x_21128 -> h_register_int x_21128
     153| Register_ptr (x_21130, x_21129) -> h_register_ptr x_21130 x_21129
    154154
    155155(** val register_type_rect_Type5 :
     
    157157    -> 'a1) -> register_type -> 'a1 **)
    158158let rec register_type_rect_Type5 h_register_int h_register_ptr = function
    159 | Register_int x_21008 -> h_register_int x_21008
    160 | Register_ptr (x_21010, x_21009) -> h_register_ptr x_21010 x_21009
     159| Register_int x_21134 -> h_register_int x_21134
     160| Register_ptr (x_21136, x_21135) -> h_register_ptr x_21136 x_21135
    161161
    162162(** val register_type_rect_Type3 :
     
    164164    -> 'a1) -> register_type -> 'a1 **)
    165165let rec register_type_rect_Type3 h_register_int h_register_ptr = function
    166 | Register_int x_21014 -> h_register_int x_21014
    167 | Register_ptr (x_21016, x_21015) -> h_register_ptr x_21016 x_21015
     166| Register_int x_21140 -> h_register_int x_21140
     167| Register_ptr (x_21142, x_21141) -> h_register_ptr x_21142 x_21141
    168168
    169169(** val register_type_rect_Type2 :
     
    171171    -> 'a1) -> register_type -> 'a1 **)
    172172let rec register_type_rect_Type2 h_register_int h_register_ptr = function
    173 | Register_int x_21020 -> h_register_int x_21020
    174 | Register_ptr (x_21022, x_21021) -> h_register_ptr x_21022 x_21021
     173| Register_int x_21146 -> h_register_int x_21146
     174| Register_ptr (x_21148, x_21147) -> h_register_ptr x_21148 x_21147
    175175
    176176(** val register_type_rect_Type1 :
     
    178178    -> 'a1) -> register_type -> 'a1 **)
    179179let rec register_type_rect_Type1 h_register_int h_register_ptr = function
    180 | Register_int x_21026 -> h_register_int x_21026
    181 | Register_ptr (x_21028, x_21027) -> h_register_ptr x_21028 x_21027
     180| Register_int x_21152 -> h_register_int x_21152
     181| Register_ptr (x_21154, x_21153) -> h_register_ptr x_21154 x_21153
    182182
    183183(** val register_type_rect_Type0 :
     
    185185    -> 'a1) -> register_type -> 'a1 **)
    186186let rec register_type_rect_Type0 h_register_int h_register_ptr = function
    187 | Register_int x_21032 -> h_register_int x_21032
    188 | Register_ptr (x_21034, x_21033) -> h_register_ptr x_21034 x_21033
     187| Register_int x_21158 -> h_register_int x_21158
     188| Register_ptr (x_21160, x_21159) -> h_register_ptr x_21160 x_21159
    189189
    190190(** val register_type_inv_rect_Type4 :
     
    317317      Joint.joint_if_result = (Obj.magic ret'); Joint.joint_if_params =
    318318      (Obj.magic params'); Joint.joint_if_stacksize =
    319       def'.Joint.joint_if_stacksize; Joint.joint_if_code =
     319      def'.Joint.joint_if_stacksize; Joint.joint_if_local_stacksize =
     320      def'.Joint.joint_if_local_stacksize; Joint.joint_if_code =
    320321      def'.Joint.joint_if_code; Joint.joint_if_entry =
    321322      def'.Joint.joint_if_entry }
     
    451452         let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in
    452453         List.Cons ((Joint.ADDRESS (id, (Obj.magic r1), (Obj.magic r2))),
    453          List.Nil))
     454         (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic r1),
     455         (Obj.magic (Joint.psd_argument_from_reg r1)),
     456         (Obj.magic
     457           (Joint.psd_argument_from_byte (Joint.byte_of_nat offset))))),
     458         (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic r2),
     459         (Obj.magic (Joint.psd_argument_from_reg r2)),
     460         (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
     461         List.Nil))))))
    454462     | FrontEndOps.Oaddrstack offset ->
    455463       (fun _ _ ->
     
    459467             (Obj.magic (RTL.Rtl_stack_address (r1, r2)))
    460468           in
    461           x), List.Nil))) __ __
     469          x), (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic r1),
     470         (Obj.magic (Joint.psd_argument_from_reg r1)),
     471         (Obj.magic
     472           (Joint.psd_argument_from_byte (Joint.byte_of_nat offset))))),
     473         (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic r2),
     474         (Obj.magic (Joint.psd_argument_from_reg r2)),
     475         (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
     476         List.Nil))))))) __ __
    462477  in
    463478  Bind_new.Bret l
     
    11591174  let luniverse' = def.RTLabs_syntax.f_labgen in
    11601175  let stack_size' = def.RTLabs_syntax.f_stacksize in
    1161   let entry' = def.RTLabs_syntax.f_entry in
     1176  let entry' = Types.pi1 def.RTLabs_syntax.f_entry in
    11621177  let init = { Joint.joint_if_luniverse = luniverse';
    11631178    Joint.joint_if_runiverse = runiverse'; Joint.joint_if_result =
    11641179    (Obj.magic List.Nil); Joint.joint_if_params = (Obj.magic List.Nil);
    1165     Joint.joint_if_stacksize = stack_size'; Joint.joint_if_code =
     1180    Joint.joint_if_stacksize = stack_size'; Joint.joint_if_local_stacksize =
     1181    stack_size'; Joint.joint_if_code =
    11661182    (Obj.magic
    11671183      (Identifiers.add PreIdentifiers.LabelTag
    1168         (Identifiers.empty_map PreIdentifiers.LabelTag) (Types.pi1 entry')
    1169         (Joint.Final Joint.RETURN))); Joint.joint_if_entry =
    1170     (Types.pi1 (Obj.magic entry')) }
     1184        (Identifiers.empty_map PreIdentifiers.LabelTag) entry' (Joint.Final
     1185        Joint.RETURN))); Joint.joint_if_entry = (Obj.magic entry') }
    11711186  in
    11721187  (let { Types.fst = init'; Types.snd = lenv } =
Note: See TracChangeset for help on using the changeset viewer.