Changeset 1529 for src/RTLabs
- Timestamp:
- Nov 22, 2011, 12:28:04 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabsToRTL.ma
r1521 r1529 431 431 definition translate_op1 ≝ 432 432 λglobals: list ident. 433 λop1: unary_operation. 433 λty, ty'. 434 λop1: unary_operation ty ty'. 434 435 λdestrs: list register. 435 436 λsrcrs: list register. … … 439 440 λdef: rtl_internal_function globals. 440 441 match op1 with 441 [ Ocastint src_si gn src_size_ _ ⇒442 [ Ocastint src_size src_sign _ _ ⇒ 442 443 let dest_size ≝ |destrs| * 8 in 443 444 let src_size ≝ bitsize_of_intsize src_size in 444 445 translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def 445 | Onegint ⇒446 | Onegint _ _ ⇒ 446 447 translate_negint globals destrs srcrs start_lbl dest_lbl def prf 447 | Onotbool ⇒448 | Onotbool _ _ _ _ ⇒ 448 449 translate_notbool globals destrs srcrs start_lbl dest_lbl def 449 | Onotint ⇒450 | Onotint _ _ ⇒ 450 451 let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in 451 452 let l ≝ map2 … f destrs srcrs prf in 452 453 adds_graph rtl_params1 globals l start_lbl dest_lbl def 453 | Optrofint r ⇒454 | Optrofint _ _ r ⇒ 454 455 translate_move globals destrs srcrs start_lbl dest_lbl def 455 | Ointofptr r ⇒456 | Ointofptr _ _ r ⇒ 456 457 translate_move globals destrs srcrs start_lbl dest_lbl def 457 | Oid ⇒458 | Oid _ ⇒ 458 459 translate_move globals destrs srcrs start_lbl dest_lbl def 459 460 | _ ⇒ ? (* float operations implemented in runtime *) … … 860 861 [2: >tmp_destrs_proof @prf_destrs 861 862 |1: normalize nodelta 862 generalize in match srcrs12_proof 863 generalize in match srcrs12_proof; 863 864 #HYP >rev_length >rev_length @HYP 864 865 ] … … 971 972 add_translates rtl_params1 globals [ 972 973 translate_ne globals destrs srcrs1 srcrs2; 973 translate_op1 globals Onotbooldestrs destrs (refl ? (|destrs|))974 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|)) 974 975 ] start_lbl dest_lbl def 975 976 | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def … … 979 980 add_translates rtl_params1 globals [ 980 981 translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ?; 981 translate_op1 globals Onotbooldestrs destrs (refl ? (|destrs|))982 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|)) 982 983 ] start_lbl dest_lbl def 983 984 | Cge ⇒ 984 985 add_translates rtl_params1 globals [ 985 986 translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ?; 986 translate_op1 globals Onotbooldestrs destrs (refl ? (|destrs|))987 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|)) 987 988 ] start_lbl dest_lbl def 988 989 ] … … 992 993 add_translates rtl_params1 globals [ 993 994 translate_ne globals destrs srcrs1 srcrs2; 994 translate_op1 globals Onotbooldestrs destrs (refl ? (|destrs|))995 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|)) 995 996 ] start_lbl dest_lbl def 996 997 | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def … … 1000 1001 add_translates rtl_params1 globals [ 1001 1002 translate_lt globals destrs destrs_prf srcrs2 srcrs1; 1002 translate_op1 globals Onotbooldestrs destrs (refl ? (|destrs|))1003 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|)) 1003 1004 ] start_lbl dest_lbl def 1004 1005 | Cge ⇒ 1005 1006 add_translates rtl_params1 globals [ 1006 1007 translate_lt globals destrs destrs_prf srcrs1 srcrs2; 1007 translate_op1 globals Onotbooldestrs destrs (refl ? (|destrs|))1008 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|)) 1008 1009 ] start_lbl dest_lbl def 1009 1010 ] … … 1013 1014 add_translates rtl_params1 globals [ 1014 1015 translate_ne globals destrs srcrs1 srcrs2; 1015 translate_op1 globals Onotbooldestrs destrs (refl ? (|destrs|))1016 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|)) 1016 1017 ] start_lbl dest_lbl def 1017 1018 | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def … … 1021 1022 add_translates rtl_params1 globals [ 1022 1023 translate_lt globals destrs destrs_prf srcrs2 srcrs1; 1023 translate_op1 globals Onotbooldestrs destrs (refl ? (|destrs|))1024 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|)) 1024 1025 ] start_lbl dest_lbl def 1025 1026 | Cge ⇒ 1026 1027 add_translates rtl_params1 globals [ 1027 1028 translate_lt globals destrs destrs_prf srcrs1 srcrs2; 1028 translate_op1 globals Onotbooldestrs destrs (refl ? (|destrs|))1029 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|)) 1029 1030 ] start_lbl dest_lbl def 1030 1031 ] … … 1168 1169 | St_const destr cst lbl' ⇒ 1169 1170 translate_cst globals cst (find_local_env destr lenv) lbl lbl' def 1170 | St_op1 op1 destr srcr lbl' ⇒1171 translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def1171 | St_op1 ty ty' op1 destr srcr lbl' ⇒ 1172 translate_op1 globals ty ty' op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def 1172 1173 | St_op2 op2 destr srcr1 srcr2 lbl' ⇒ 1173 1174 translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
Note: See TracChangeset
for help on using the changeset viewer.