Changeset 1288 for src/RTLabs
- Timestamp:
- Oct 3, 2011, 5:33:11 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLAbstoRTL.ma
r1287 r1288 806 806 807 807 definition translate_op2 ≝ 808 λglobals: list ident. 808 809 λop2. 809 810 λdestrs: list register. … … 817 818 λstart_lbl: label. 818 819 λdest_lbl: label. 819 λdef: rtl_internal_function .820 λdef: rtl_internal_function globals. 820 821 match op2 with 821 822 [ Oadd ⇒ 822 translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def823 translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def 823 824 | Oaddp ⇒ 824 translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def825 translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def 825 826 | Osub ⇒ 826 translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def827 translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 827 828 | Osubpi ⇒ 828 translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def829 translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 829 830 | Osubpp sz ⇒ 830 translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def831 translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 831 832 | Omul ⇒ 832 translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def833 translate_mul globals destrs srcrs1 srcrs2 start_lbl dest_lbl def 833 834 | Odivu ⇒ 834 match srcrs1 return λx. 0 < |x| → rtl_internal_function with835 match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with 835 836 [ cons hd tl ⇒ λcons_prf. 836 837 match tl with 837 [ nil ⇒ translate_divumodu8 true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def838 [ nil ⇒ translate_divumodu8 globals true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def 838 839 | _ ⇒ ? (* not implemented *) 839 840 ] … … 841 842 ] srcrs1_prf 842 843 | Omodu ⇒ 843 match srcrs1 return λx. 0 < |x| → rtl_internal_function with844 match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with 844 845 [ cons hd tl ⇒ λcons_prf. 845 846 match tl with 846 [ nil ⇒ translate_divumodu8 false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def847 [ nil ⇒ translate_divumodu8 globals false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def 847 848 | _ ⇒ ? (* not implemented *) 848 849 ] … … 850 851 ] srcrs1_prf 851 852 | Oand ⇒ 852 translate_op And destrs srcrs1 srcrs2 start_lbl dest_lbl def853 translate_op globals And destrs srcrs1 srcrs2 start_lbl dest_lbl def 853 854 | Oor ⇒ 854 translate_op Or destrs srcrs1 srcrs2 start_lbl dest_lbl def855 translate_op globals Or destrs srcrs1 srcrs2 start_lbl dest_lbl def 855 856 | Oxor ⇒ 856 translate_op Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def857 translate_op globals Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def 857 858 | Ocmp c ⇒ 858 859 match c with 859 860 [ Ceq ⇒ 860 add_translates [861 translate_ne destrs srcrs1 srcrs2;862 translate_op1 Onotbool destrs destrs (refl ? (|destrs|))861 add_translates rtl_params1 globals [ 862 translate_ne globals destrs srcrs1 srcrs2; 863 translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) 863 864 ] start_lbl dest_lbl def 864 | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def865 | Clt ⇒ translate_lts destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def866 | Cgt ⇒ translate_lts destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def865 | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def 866 | Clt ⇒ translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def 867 | Cgt ⇒ translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def 867 868 | Cle ⇒ 868 add_translates [869 translate_lts destrs destrs_prf srcrs2 srcrs1 ? ?;870 translate_op1 Onotbool destrs destrs (refl ? (|destrs|))869 add_translates rtl_params1 globals [ 870 translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ?; 871 translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) 871 872 ] start_lbl dest_lbl def 872 873 | Cge ⇒ 873 add_translates [874 translate_lts destrs destrs_prf srcrs1 srcrs2 ? ?;875 translate_op1 Onotbool destrs destrs (refl ? (|destrs|))874 add_translates rtl_params1 globals [ 875 translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ?; 876 translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) 876 877 ] start_lbl dest_lbl def 877 878 ] … … 879 880 match c with 880 881 [ Ceq ⇒ 881 add_translates [882 translate_ne destrs srcrs1 srcrs2;883 translate_op1 Onotbool destrs destrs (refl ? (|destrs|))882 add_translates rtl_params1 globals [ 883 translate_ne globals destrs srcrs1 srcrs2; 884 translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) 884 885 ] start_lbl dest_lbl def 885 | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def886 | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def887 | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def886 | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def 887 | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def 888 | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def 888 889 | Cle ⇒ 889 add_translates [890 translate_lt destrs destrs_prf srcrs2 srcrs1;891 translate_op1 Onotbool destrs destrs (refl ? (|destrs|))890 add_translates rtl_params1 globals [ 891 translate_lt globals destrs destrs_prf srcrs2 srcrs1; 892 translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) 892 893 ] start_lbl dest_lbl def 893 894 | Cge ⇒ 894 add_translates [895 translate_lt destrs destrs_prf srcrs1 srcrs2;896 translate_op1 Onotbool destrs destrs (refl ? (|destrs|))895 add_translates rtl_params1 globals [ 896 translate_lt globals destrs destrs_prf srcrs1 srcrs2; 897 translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) 897 898 ] start_lbl dest_lbl def 898 899 ] … … 900 901 match c with 901 902 [ Ceq ⇒ 902 add_translates [903 translate_ne destrs srcrs1 srcrs2;904 translate_op1 Onotbool destrs destrs (refl ? (|destrs|))903 add_translates rtl_params1 globals [ 904 translate_ne globals destrs srcrs1 srcrs2; 905 translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) 905 906 ] start_lbl dest_lbl def 906 | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def907 | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def908 | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def907 | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def 908 | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def 909 | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def 909 910 | Cle ⇒ 910 add_translates [911 translate_lt destrs destrs_prf srcrs2 srcrs1;912 translate_op1 Onotbool destrs destrs (refl ? (|destrs|))911 add_translates rtl_params1 globals [ 912 translate_lt globals destrs destrs_prf srcrs2 srcrs1; 913 translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) 913 914 ] start_lbl dest_lbl def 914 915 | Cge ⇒ 915 add_translates [916 translate_lt destrs destrs_prf srcrs1 srcrs2;917 translate_op1 Onotbool destrs destrs (refl ? (|destrs|))916 add_translates rtl_params1 globals [ 917 translate_lt globals destrs destrs_prf srcrs1 srcrs2; 918 translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) 918 919 ] start_lbl dest_lbl def 919 920 ] … … 929 930 qed. 930 931 931 definition translate_cond ≝ 932 definition translate_cond: ∀globals: list ident. list register → label → label → label → rtl_internal_function globals → rtl_internal_function globals ≝ 933 λglobals: list ident. 932 934 λsrcrs: list register. 933 935 λstart_lbl: label. 934 936 λlbl_true: label. 935 937 λlbl_false: label. 936 λdef: rtl_internal_function .937 let 〈def, tmpr〉 ≝ fresh_reg def in938 let 〈 def, tmp_lbl〉 ≝ fresh_labeldef in939 let init ≝ rtl_st_int tmpr (zero ?) start_lblin940 let f ≝ λsrcr. rtl_st_op2 Or tmpr tmpr srcr start_lblin941 let def ≝ adds_graph (init :: (map …f srcrs)) start_lbl tmp_lbl def in942 add_graph tmp_lbl (rtl_st_cond tmpr lbl_true lbl_false) def.938 λdef: rtl_internal_function globals. 939 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 940 let 〈tmp_lbl, def〉 ≝ fresh_label rtl_params1 globals def in 941 let init ≝ sequential rtl_params_ globals (INT rtl_params_ globals tmpr (zero …)) in 942 let f ≝ λsrcr. sequential rtl_params_ globals (OP2 rtl_params_ globals Or tmpr tmpr srcr) in 943 let def ≝ adds_graph rtl_params1 globals (init :: (map ? ? f srcrs)) start_lbl tmp_lbl def in 944 add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true lbl_false)) def. 943 945 944 946 definition translate_load ≝
Note: See TracChangeset
for help on using the changeset viewer.