Changeset 3004


Ignore:
Timestamp:
Mar 28, 2013, 1:48:14 PM (4 years ago)
Author:
tranquil
Message:

fixed a bug where when doing an asymetrical op, cast initialization was inserted also when sizes matched

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2946 r3004  
    1313    match isize with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    1414  | ASTptr ⇒ 2 (* rgn ⇒ nat_of_bitvector ? ptr_size *)
     15  ].
     16
     17definition sign_of_sig_type ≝
     18  λsig.
     19  match sig with
     20  [ ASTint _ sign ⇒ sign
     21  | ASTptr ⇒ Unsigned
    1522  ].
    1623
     
    411418
    412419definition translate_op_asym_signed :
     420  (* first argument will dictate size, second will be casted signedly *)
    413421  ∀globals.Op2 → list register → list psd_argument → list psd_argument →
    414422  bind_new register (list (joint_seq RTL globals)) ≝
     
    418426  let cast_srcrs ≝ λsrcrs,tmp.
    419427    let srcrs_l ≝ |srcrs| in
    420     if leb srcrs_l l then
     428    if leb (S srcrs_l) l then
    421429      match last ? srcrs with
    422430      [ Some last ⇒
     
    440448    [ >length_make_list %
    441449    | #_ >length_append >length_make_list
    442       @minus_to_plus //
     450      @minus_to_plus [ @(transitive_le … H) ] //
    443451    ]
    444   | >length_lhd normalize >(not_le_to_leb_false … H) %
     452  | >length_lhd lapply (le_S_S_to_le … (not_le_to_lt … H))
     453    lapply (|destrs|) lapply (|srcrs|) -destrs
     454    #n #m * -n [2: #n #H] whd in ⊢ (???%); [2: @if_elim #_ % ]
     455    >not_le_to_leb_false [%] @lt_to_not_le @le_S_S assumption
    445456  ]
    446457qed.
Note: See TracChangeset for help on using the changeset viewer.