Changeset 1062 for src/RTLabs


Ignore:
Timestamp:
Jul 11, 2011, 2:09:03 PM (8 years ago)
Author:
mulligan
Message:

separated jmeq and coercions from foldstuff.ma in order to fix the ongoing mess in util.ma surrounding reduce_strong

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1061 r1062  
    33include "common/AssocList.ma".
    44include "common/Graphs.ma".
    5 (* include "common/IntValue.ma". *)
    65include "common/FrontEndOps.ma".
    76
     
    463462  λdest_lbl.
    464463  λdef.
    465   λprf: | destrs | = | srcrs |.
     464  λprf: |destrs| = |srcrs|.
    466465  match op1 with
    467466  [ intermediate_op1_cast src_size src_sign dest_size ⇒
     
    523522    ]
    524523  ].
    525   [ 1: @third_reduced_proof
    526   | 3: @first_reduced_proof
    527  
    528 let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def =
    529   let ((srcrs1_common, srcrs1_rest), (srcrs2_common, srcrs2_rest)) =
    530     MiscPottier.reduce srcrs1 srcrs2 in
    531   let srcrs_rest = choose_rest srcrs1_rest srcrs2_rest in
    532   let ((destrs_common, destrs_rest), _) =
    533     MiscPottier.reduce destrs srcrs1_common in
    534   let ((destrs_cted, destrs_rest), (srcrs_cted, _)) =
    535     MiscPottier.reduce destrs_rest srcrs_rest in
    536   let (def, tmpr) = fresh_reg def in
    537   let insts_init =
    538     [RTL.St_clear_carry start_lbl ;
    539      RTL.St_int (tmpr, 0, start_lbl)] in
    540   let f_add destr srcr1 srcr2 =
    541     RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
    542   let insts_add =
    543     MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in
    544   let f_add_cted destr srcr =
    545     RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in
    546   let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in
    547   let f_rest destr =
    548     RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in
    549   let insts_rest = List.map f_rest destrs_rest in
    550   adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest)
    551     start_lbl dest_lbl def
     524cases not_implemented (* problem here with lengths of lists: possible bug? *)
     525qed.
     526
     527let rec translate_mul1
     528  (dummy: register) (tmpr: register) (destrs: list register)
     529  (srcrs1: list register) (srcr2: register) (start_lbl: label)
     530    on srcrs1 ≝
     531  match destrs with
     532  [ nil ⇒ adds_graph [ rtl_st_skip start_lbl ] start_lbl
     533  | cons destr tl ⇒
     534    match tl with
     535    [ nil ⇒
     536      match srcrs1 with
     537      [ nil ⇒
     538        adds_graph [
     539          rtl_st_int tmpr (zero ?) start_lbl;
     540          rtl_st_op2 Addc destr destr tmpr start_lbl
     541        ] start_lbl
     542      | cons srcr1 tl' ⇒
     543        adds_graph [
     544          rtl_st_opaccs Mul tmpr dummy srcr2 srcr1 start_lbl;
     545          rtl_st_op2 Addc destr destr tmpr start_lbl
     546        ] start_lbl
     547      ]
     548    | cons destr2 destrs ⇒
     549      match srcrs1 with
     550      [ nil ⇒
     551        add_translates [
     552          adds_graph [
     553            rtl_st_int tmpr (zero ?) start_lbl;
     554            rtl_st_op2 Addc destr destr tmpr start_lbl;
     555            rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
     556          ];
     557          translate_cst (Ointconst I8 (zero ?)) destrs
     558        ] start_lbl
     559      | cons srcr1 srcrs1 ⇒
     560        match destrs with
     561        [ nil ⇒
     562          add_translates [
     563            adds_graph [
     564              rtl_st_int tmpr (zero ?) start_lbl;
     565              rtl_st_op2 Addc destr destr tmpr start_lbl;
     566              rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
     567            ];
     568            translate_cst (Ointconst I8 (zero ?)) destrs
     569          ] start_lbl
     570        | cons destr2 destrs ⇒
     571          add_translates [
     572            adds_graph [
     573              rtl_st_opaccs Mul tmpr destr2 srcr2 srcr1 start_lbl;
     574              rtl_st_op2 Addc destr destr tmpr start_lbl
     575            ];
     576            translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2
     577          ] start_lbl
     578        ]
     579      ]
     580    ]
     581  ].
     582
     583definition translate_muli ≝
     584  λdummy: register.
     585  λtmpr: register.
     586  λdestrs: list register.
     587  λtmp_destrs: list register.
     588  λsrcrs1: list register.
     589  λdummy_lbl: label.
     590  λi: nat.
     591  λtranslates.
     592  λsrcr2i.
     593  let 〈tmp_destrs1, tmp_destrs2〉 ≝ ? in ?.
     594
     595let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates
     596    srcr2i =
     597  let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in
     598  translates @
     599    (match tmp_destrs2 with
     600      | [] -> []
     601      | tmp_destr2 :: tmp_destrs2 ->
     602        [adds_graph [RTL.St_clear_carry dummy_lbl ;
     603                     RTL.St_int (tmp_destr2, 0, dummy_lbl)] ;
     604         translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
     605         translate_cst (AST.Cst_int 0) tmp_destrs1 ;
     606         adds_graph [RTL.St_clear_carry dummy_lbl] ;
     607         translate_op I8051.Addc destrs destrs tmp_destrs])
    552608
    553609definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset for help on using the changeset viewer.