 Timestamp:
 Mar 13, 2013, 4:21:43 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL.ma
r2823 r2866 173 173 definition split_into_bytes: 174 174 ∀size. ∀int: bvint size. Σbytes: list Byte. bytes = size_intsize size ≝ 175 λsize.vrsplit ? (size_intsize size) 8. 175 λsize,int.reverse … (vrsplit ? (size_intsize size) 8 int). 176 >length_reverse @pi2 qed. 176 177 177 178 let rec list_inject_All_aux A P (l : list A) on l : All A P l → list (Σx.P x) ≝ … … 180 181  cons hd tl ⇒ λprf.«hd, proj1 … prf» :: list_inject_All_aux A P tl (proj2 … prf) 181 182 ]. 183 184 definition translate_op_aux: 185 ∀globals. Op2 → 186 ∀dests : list register. 187 ∀srcrs1 : list psd_argument. 188 ∀srcrs2 : list psd_argument. 189 dests = srcrs1 → srcrs1 = srcrs2 → 190 list (joint_seq RTL globals) 191 ≝ 192 λglobals: list ident. 193 λop. 194 λdestrs. 195 λsrcrs1. 196 λsrcrs2. 197 λprf1,prf2. 198 (* first, clear carry if op relies on it *) 199 map3 ???? (OP2 RTL globals op) destrs srcrs1 srcrs2 prf1 prf2. 182 200 183 201 definition translate_op: … … 194 212 λsrcrs1. 195 213 λsrcrs2. 196 λprf1,prf2.197 (* first, clear carry if op relies on it *)198 214 match op with 199 [ Addc ⇒ [CLEAR_CARRY ??] 200  Sub ⇒ [CLEAR_CARRY ??] 201  _ ⇒ [ ] 202 ] @ map3 ???? (OP2 RTL globals op) destrs srcrs1 srcrs2 prf1 prf2. 215 [ Add ⇒ 216 match destrs return λdestrs.destrs = srcrs1 → srcrs1 = srcrs2 → ? with 217 [ nil ⇒ λ_.λ_.[ ] 218  cons destr destrs' ⇒ 219 match srcrs1 return λsrcrs1.S(destrs') = srcrs1 → srcrs1 = srcrs2 → ? with 220 [ nil ⇒ λprf1.⊥ 221  cons srcr1 srcrs1' ⇒ 222 λprf1. 223 match srcrs2 return λsrcrs2.S(srcrs1') = srcrs2 → ? with 224 [ nil ⇒ λprf2.⊥ 225  cons srcr2 srcrs2' ⇒ 226 λprf2.OP2 ?? Add destr srcr1 srcr2 :: translate_op_aux … Addc destrs' srcrs1' srcrs2' ?? 227 ] 228 ] 229 ] 230  Sub ⇒ λprf1,prf2.[ CLEAR_CARRY ?? ] @ translate_op_aux … Sub … prf1 prf2 231  Addc ⇒ λprf1,prf2.[ CLEAR_CARRY ?? ] @ translate_op_aux … Addc … prf1 prf2 232  _ ⇒ translate_op_aux … op destrs srcrs1 srcrs2 233 ]. 234 normalize in prf1 prf2; destruct assumption qed. 203 235 204 236 definition cast_list : ∀A.A → ℕ → list A → list A ≝ … … 249 281 qed. 250 282 251 let rec nat_to_args (size : nat) (k : nat) on size : Σl : list psd_argument.l = size ≝ 252 match size with 253 [ O ⇒ [ ] 254  S size' ⇒ 255 (byte_of_nat k : psd_argument) :: nat_to_args size' (k ÷ 8) 256 ]. @hide_prf [ %  cases (nat_to_args ??) #res #EQ normalize >EQ % ] qed. 283 definition zero_args : ∀size.Σl : list psd_argument.l = size ≝ 284 λsize. 285 «make_list psd_argument (zero_byte) size, length_make_list …». 286 287 definition one_args : ∀size.Σl : list psd_argument.l = size ≝ 288 λsize.match size return λsize.Σl : list psd_argument.l = size with 289 [ O ⇒ «[ ], refl …» 290  S k ⇒ (byte_of_nat 1 : psd_argument) :: zero_args k 291 ]. 292 whd in ⊢ (??%?); @eq_f @pi2 qed. 257 293 258 294 definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with … … 347 383 list register → list (joint_seq RTL globals) ≝ 348 384 λglobals,destrs. 349 match nat_to_args (destrs) 0 with 350 [ mk_Sig res prf ⇒ translate_move ? destrs res ?]. 351 // qed. 385 translate_move ? destrs (zero_args (destrs)) ?. 386 @sym_eq @pi2 qed. 352 387 353 388 let rec last A (l : list A) on l : option A ≝ … … 450 485 λprf: destrs = srcrs. (* assert in caml code *) 451 486 translate_notint … destrs srcrs prf @@ 452 translate_op ? Add destrs (map … (Reg ?) destrs) (nat_to_args (destrs) 1) ??. 453 @hide_prf >length_map [ cases (nat_to_args ??) ] // qed. 487 translate_op ? Add destrs (map … (Reg ?) destrs) (one_args (destrs)) ??. 488 @hide_prf 489 >length_map [ @sym_eq @pi2  % ] qed. 454 490 455 491 definition translate_notbool:
Note: See TracChangeset
for help on using the changeset viewer.