 Timestamp:
 Mar 28, 2013, 1:48:14 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL.ma
r2946 r3004 13 13 match isize with [ I8 ⇒ 1  I16 ⇒ 2  I32 ⇒ 4 ] 14 14  ASTptr ⇒ 2 (* rgn ⇒ nat_of_bitvector ? ptr_size *) 15 ]. 16 17 definition sign_of_sig_type ≝ 18 λsig. 19 match sig with 20 [ ASTint _ sign ⇒ sign 21  ASTptr ⇒ Unsigned 15 22 ]. 16 23 … … 411 418 412 419 definition translate_op_asym_signed : 420 (* first argument will dictate size, second will be casted signedly *) 413 421 ∀globals.Op2 → list register → list psd_argument → list psd_argument → 414 422 bind_new register (list (joint_seq RTL globals)) ≝ … … 418 426 let cast_srcrs ≝ λsrcrs,tmp. 419 427 let srcrs_l ≝ srcrs in 420 if leb srcrs_ll then428 if leb (S srcrs_l) l then 421 429 match last ? srcrs with 422 430 [ Some last ⇒ … … 440 448 [ >length_make_list % 441 449  #_ >length_append >length_make_list 442 @minus_to_plus //450 @minus_to_plus [ @(transitive_le … H) ] // 443 451 ] 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 445 456 ] 446 457 qed.
Note: See TracChangeset
for help on using the changeset viewer.