Changeset 2490 for src/RTLabs/RTLabsToRTL.ma
 Timestamp:
 Nov 25, 2012, 1:33:09 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL.ma
r2290 r2490 26 26 [ ASTint isize sign ⇒ 27 27 match isize with [ I8 ⇒ 1  I16 ⇒ 2  I32 ⇒ 4 ] 28  ASTfloat _ ⇒ ? (* dpm: not implemented *)29 28  ASTptr ⇒ 2 (* rgn ⇒ nat_of_bitvector ? ptr_size *) 30 29 ]. 31 cases not_implemented32 qed.33 30 34 31 inductive register_type: Type[0] ≝ … … 161 158 λr,lenv,prf. make_addr ? (find_local_env r lenv prf). 162 159 160 definition find_and_addr_arg ≝ 161 λr,lenv,prf. make_addr ? (find_local_env_arg r lenv prf). 162 163 163 include alias "common/Identifiers.ma". 164 164 let rec rtl_args (args : list register) (env : local_env) on args : … … 270 270 definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with 271 271 [ Ointconst size _ _ ⇒ size_intsize size 272  Ofloatconst _ _ ⇒ ? (* not implemented *)273 272  _ ⇒ 2 274 273 ]. 275 cases not_implemented qed.276 274 277 275 definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst. … … 296 294 map2 … (λr.λb : Byte.r ← b) destrs 297 295 (split_into_bytes size const) ? 298  Ofloatconst _ _ ⇒ ?299 296  Oaddrsymbol id offset ⇒ λcst_prf,prf. 300 297 let 〈r1, r2〉 ≝ make_addr … destrs ? in … … 304 301 [(rtl_stack_address r1 r2 : joint_seq RTL globals)] 305 302 ] (pi2 … cst_sig). 306 [2: cases not_implemented 307 1: cases (split_into_bytes ??) #lst 303 [ cases (split_into_bytes ??) #lst 308 304 #EQ >EQ >prf whd in ⊢ (??%?); cases size % 309  3:@cst_prf305  @cst_prf 310 306 *: >prf % 311 307 ] … … 337 333 destr ← .Inc. destr ; 338 334 destr ← .Cmpl. destr ] 339  Imm by ⇒ 340 match by with 341 [ BVByte b ⇒ 342 if sign_bit … b then 343 [ destr ← (maximum … : Byte) ] 344 else 345 [ destr ← zero_byte ] 346  _ ⇒ (* should not happend ... *) [ ] 347 ] 335  Imm b ⇒ 336 if sign_bit … b then 337 [ destr ← (maximum … : Byte) ] 338 else 339 [ destr ← zero_byte ] 348 340 ]. 349 341 … … 531 523  _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *) 532 524 ] (refl …) (refl …). 533 [3,4,5,6,7,8,9: (* floats *) cases not_implemented 534 *: destruct >prf1 >prf2 [3: >length_map ] // 535 ] 525 destruct >prf1 >prf2 [3: >length_map ] // 536 526 qed. 537 527 538 528 include alias "arithmetics/nat.ma". 539 540 let rec range_strong_internal (start : ℕ) (count : ℕ)541 (* Paolo: no notation to avoid ambiguity *)542 on count : list (Σn : ℕ.lt n (plus start count)) ≝543 match count return λx.count = x → list (Σn : ℕ. n < start + count)544 with545 [ O ⇒ λ_.[ ]546  S count' ⇒ λEQ.547 let f : (Σn : ℕ. lt n (S start + count')) → Σn : ℕ. lt n (start + count) ≝548 λsig.match sig with [mk_Sig n prf ⇒ n] in549 start :: map … f (range_strong_internal (S start) count')550 ] (refl …).551 destruct(EQ) // qed.552 553 definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝554 λend.range_strong_internal 0 end.555 529 556 530 definition translate_mul_i : … … 1009 983 (find_local_env_arg srcr lenv ?), lbl'❭ 1010 984  St_call_id f args retr lbl' ⇒ λstmt_typed. 1011 ❬(match retr with 1012 [ Some retr ⇒ 1013 CALL_ID RTL ? f (rtl_args args lenv ?) (find_local_env retr lenv ?) 1014  None ⇒ 1015 CALL_ID RTL ? f (rtl_args args lenv ?) [ ] 1016 ] : bind_seq_block ???), lbl'❭ 985 ❬(CALL RTL ? (inl … f) (rtl_args args lenv ?) 986 (match retr with 987 [ Some retr ⇒ find_local_env retr lenv ? 988  None ⇒ [ ] 989 ]) : bind_seq_block ???), lbl'❭ 1017 990  St_call_ptr f args retr lbl' ⇒ λstmt_typed. 1018 let fs ≝ find_and_addr f lenv ?? in1019 ❬( rtl_call_ptr (\fst fs) (\sndfs) (rtl_args args lenv ?)991 let fs ≝ find_and_addr_arg f lenv ?? in 992 ❬(CALL RTL ? (inr ?? fs) (rtl_args args lenv ?) 1020 993 (match retr with 1021 994 [ Some retr ⇒ … … 1044 1017  @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_prf) 1045 1018 ] 1046 *: whd in stmt_typed; cases daemon (* TODO need more stringent statement_typed*)1019 *: cases daemon (* TODO *) 1047 1020 ] 1048 1021 qed. … … 1052 1025 the start and end nodes to ensure that they are in, and place dummy 1053 1026 skip instructions at these nodes. *) 1054 definition translate_internal ≝ 1027 definition translate_internal : 1028 ∀globals.internal_function → (* insert here more properties *) 1029 joint_closed_internal_function RTL globals ≝ 1055 1030 λglobals: list ident. 1056 1031 λdef.
Note: See TracChangeset
for help on using the changeset viewer.