Changeset 1063 for src/RTLabs


Ignore:
Timestamp:
Jul 11, 2011, 5:52:11 PM (8 years ago)
Author:
mulligan
Message:

changes from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1062 r1063  
    7373  ].
    7474
     75axiom fresh_regs_length:
     76  ∀def: rtl_internal_function.
     77  ∀n: nat.
     78    |(\snd (fresh_regs def n))| = n.
     79   
    7580definition addr_regs ≝
    7681  λregs.
     
    487492  λsrcrs1.
    488493  λsrcrs2.
     494  λprf: |srcrs1| = |srcrs2|.
    489495  λstart_lbl.
    490496  λdest_lbl.
    491497  λdef.
    492   λprf: |srcrs1| = |srcrs2|.
    493498  match reduce_strong ? srcrs1 srcrs2 with
    494499  [ dp reduced first_reduced_proof ⇒
     
    586591  λdestrs: list register.
    587592  λtmp_destrs: list register.
     593  λdestrs_prf: |destrs| = |tmp_destrs|.
    588594  λsrcrs1: list register.
    589595  λdummy_lbl: label.
    590596  λi: nat.
    591   λtranslates.
    592   λsrcr2i.
    593   let 〈tmp_destrs1, tmp_destrs2〉 ≝ ? in ?.
    594 
    595 let 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])
     597  λi_prf.
     598  λtranslates: list ?.
     599  λsrcr2i: register.
     600  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split ? tmp_destrs i i_prf in
     601  let tmp_destrs2' ≝
     602    match tmp_destrs2 with
     603    [ nil ⇒ [ ]
     604    | cons tmp_destr2 tmp_destrs2 ⇒ [
     605        adds_graph [
     606          rtl_st_clear_carry dummy_lbl;
     607          rtl_st_int tmp_destr2 (zero ?) dummy_lbl
     608        ];
     609        translate_mul1 dummy tmpr tmp_destrs2 srcrs1 srcr2i;
     610        translate_cst (Ointconst I8 (zero ?)) tmp_destrs1;
     611        adds_graph [
     612          rtl_st_clear_carry dummy_lbl
     613        ];
     614        translate_op Addc destrs destrs tmp_destrs destrs_prf
     615      ]
     616    ]
     617  in
     618    translates @ tmp_destrs2'.
     619
     620definition translate_mul ≝
     621  λdestrs: list register.
     622  λsrcrs1: list register.
     623  λsrcrs2: list register.
     624  λstart_lbl: label.
     625  λdest_lbl: label.
     626  λdef: rtl_internal_function.
     627  let 〈def, dummy〉 ≝ fresh_reg def in
     628  let 〈def, tmpr〉 ≝ fresh_reg def in
     629  let 〈def, tmp_destrs〉 ≝ fresh_regs def (|destrs|) in
     630  let 〈def, fresh_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
     631  let 〈def, fresh_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
     632  let insts_init ≝ [
     633    translate_move fresh_srcrs1 srcrs1;
     634    translate_move fresh_srcrs2 srcrs2;
     635    translate_cst (Ointconst I8 (zero ?)) destrs
     636  ]
     637  in
     638  let f ≝ λi. translate_muli dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in
     639  let insts_mul ≝ foldi ? ? [ ] srcrs2 in ?. [5: check insts_init.
     640    add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
     641
     642let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
     643  let (def, dummy) = fresh_reg def in
     644  let (def, tmpr) = fresh_reg def in
     645  let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
     646  let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in
     647  let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in
     648  let insts_init =
     649    [translate_move fresh_srcrs1 srcrs1 ;
     650     translate_move fresh_srcrs2 srcrs2 ;
     651     translate_cst (AST.Cst_int 0) destrs] in
     652  let f = λi. translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl i ? in
     653  let insts_mul = MiscPottier.foldi f [] srcrs2 in
     654  add_translates (insts_init @ insts_mul) start_lbl dest_lbl def
    608655
    609656definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset for help on using the changeset viewer.