Changeset 2217 for src/RTLabs/RTLabsToRTL_paolo.ma
 Timestamp:
 Jul 19, 2012, 6:13:54 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL_paolo.ma
r2214 r2217 8 8 include alias "ASM/BitVector.ma". 9 9 include alias "arithmetics/nat.ma". 10 11 definition rtl_fresh_reg: 12 ∀globals.freshT RTL globals register ≝ 13 λglobals,def. 14 let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in 15 〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉. 16 17 definition rtl_fresh_reg_no_local : 18 ∀globals.freshT RTL globals register ≝ 19 λglobals,def. 20 let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in 21 〈set_runiverse ?? def runiverse, r〉. 22 10 23 definition size_of_sig_type ≝ 11 24 λsig. … … 48 61 λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf). 49 62 50 definition m_fresh : ∀tag.state_monad (universe tag) (identifier tag) ≝51 λtag,univ.let pr ≝ fresh … univ in 〈\snd pr, \fst pr〉.52 53 let rec register_freshes (n: nat) on n :54 state_monad (universe RegisterTag) (Σl.l = n) ≝55 match n return λx.state_monad ? (Σl.l = x) with56 [ O ⇒ return «[ ],?»57  S n' ⇒58 ! r ← m_fresh ?;59 ! res ← register_freshes n';60 return «r::res,?»61 ].[2: cases res res #res #EQ <EQ] % qed.62 63 63 definition initialize_local_env_internal : 64 (universe RegisterTag × local_env) → (register×typ) → (universe RegisterTag × local_env) ≝ 65 λlenv_runiverse,r_sig. 66 let 〈runiverse,lenv〉 ≝ lenv_runiverse in 64 ∀globals. 65 ((joint_internal_function RTL globals) × local_env) → (register×typ) → 66 ((joint_internal_function RTL globals) × local_env) ≝ 67 λglobals,def_env,r_sig. 68 let 〈def,lenv〉 ≝ def_env in 67 69 let 〈r, sig〉 ≝ r_sig in 68 70 let size ≝ size_of_sig_type sig in 69 let 〈runiverse,rs〉 ≝ register_freshes size runiverse in 70 〈runiverse,add … lenv r rs〉. 71 72 definition initialize_local_env : 73 list (register×typ) → 74 state_monad (universe RegisterTag) local_env ≝ 75 λregisters,runiverse. 76 foldl … initialize_local_env_internal 〈runiverse,empty_map …〉 registers. 71 let 〈def,rs〉 ≝ repeat_fresh … (rtl_fresh_reg_no_local globals) size def in 72 〈def,add … lenv r rs〉. 77 73 78 74 include alias "common/Identifiers.ma". … … 84 80  cons hd tl ⇒ λprf.find_local_env (\fst hd) lenv ? @ map_list_local_env lenv tl ? 85 81 ].cases prf #A #B assumption qed. 82 83 definition initialize_local_env : 84 ∀globals. 85 list (register×typ) → 86 freshT RTL globals local_env ≝ 87 λglobals,registers,def. 88 foldl ?? (initialize_local_env_internal globals) 〈def,empty_map …〉 registers. 89 90 lemma initialize_local_env_in : ∀globals,l,def,r. 91 Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env globals l def). 92 #globals #l #U #r @(list_elim_left … l) 93 [ * 94  * #tl #sig #hd #IH #G elim (Exists_append … G) G 95 whd in match initialize_local_env; normalize nodelta 96 >foldl_step change with (initialize_local_env ???) in match (foldl ?????); 97 [ #H lapply (IH H) 98  * [2: *] #EQ destruct(EQ) 99 ] 100 cases (initialize_local_env ???) 101 #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta 102 elim (repeat_fresh ??????) #U'' #rs 103 [ >mem_set_add @orb_Prop_r assumption 104  @mem_set_add_id 105 ] 106 qed. 107 108 example proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr. 109 // qed. 110 example proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr. 111 // qed. 112 113 definition initialize_locals_params_ret : 114 ∀globals. 115 (* locals *) list (register×typ) → 116 (* params *) list (register×typ) → 117 (* return *) option (register×typ) → 118 freshT RTL globals local_env ≝ 119 λglobals,locals,params,ret,def. 120 let 〈def',lenv〉 as EQ ≝ 121 initialize_local_env globals 122 ((match ret with 123 [ Some r_sig ⇒ [r_sig] 124  None ⇒ [ ] 125 ]) @ locals @ params) def in 126 let locals' ≝ map_list_local_env lenv locals ? in 127 let params' ≝ map_list_local_env lenv params ? in 128 let ret' ≝ match ret return λx.ret = x → ? with 129 [ Some r_sig ⇒ λprf.find_local_env (\fst r_sig) lenv ? 130  None ⇒ λ_.[ ] 131 ] (refl …) in 132 let def'' ≝ 133 mk_joint_internal_function RTL globals 134 (joint_if_luniverse … def') (joint_if_runiverse … def') ret' 135 params' locals' (joint_if_stacksize … def') 136 (joint_if_code … def') (joint_if_entry … def') (joint_if_exit … def') in 137 〈def'', lenv〉. @hide_prf 138 [ >(proj2_rewrite ????? EQ) 139 @initialize_local_env_in >prf %1 % 140 *: >(proj2_rewrite ????? EQ) 141 @(All_mp ??? (λpr.initialize_local_env_in ??? (\fst pr))) 142 [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) params)) 143 [ #a #H @Exists_append_r @Exists_append_r @H 144  generalize in match params; 145 ] 146  @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) locals)) 147 [ #a #H @Exists_append_r @Exists_append_l @H 148  generalize in match locals; 149 ] 150 ] 151 #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G} 152 ] 153 qed. 86 154 87 155 definition make_addr ≝ … … 834 902 qed. 835 903 836 lemma initialize_local_env_in : ∀l,runiverse,r.837 Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env l runiverse).838 #l #U #r @(list_elim_left … l)839 [ *840  * #tl #sig #hd #IH #G elim (Exists_append … G) G841 whd in match initialize_local_env; normalize nodelta842 >foldl_step change with (initialize_local_env ??) in match (foldl ?????);843 [ #H lapply (IH H)844  * [2: *] #EQ destruct(EQ)845 ]846 cases (initialize_local_env ??)847 #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta848 elim (register_freshes ??) #U'' #rs849 [ >mem_set_add @orb_Prop_r assumption850  @mem_set_add_id851 ]852 qed.853 854 definition proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr.855 // qed.856 definition proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr.857 // qed.858 859 860 904 (* XXX: we use a "hack" here to circumvent the proof obligations required to 861 905 create res, an empty internal_function record. we insert into our graph … … 865 909 λglobals: list ident. 866 910 λdef. 867 let runiverse ≝ f_reggen def in 868 let 〈runiverse',lenv〉 as pr_eq ≝ initialize_local_env 869 (match f_result def with [ None ⇒ [ ]  Some r_sig ⇒ [r_sig]] @ 870 f_params def @ f_locals def) runiverse in 871 let params' ≝ map_list_local_env lenv (f_params def) ? in 872 let locals' ≝ map_list_local_env lenv (f_locals def) ? in 873 let result' ≝ 874 match (f_result def) return λx.f_result def = x → ? with 875 [ None ⇒ λ_.[ ] 876  Some r_typ ⇒ λEQ. 877 find_local_env (\fst r_typ) lenv ? 878 ] (refl …) 879 in 911 let runiverse' ≝ f_reggen def in 880 912 let luniverse' ≝ f_labgen def in 881 913 let stack_size' ≝ f_stacksize def in … … 887 919 let graph' ≝ add LabelTag ? graph' exit' 888 920 (RETURN …) in 921 let init ≝ 922 mk_joint_internal_function RTL globals luniverse' runiverse' [ ] [ ] 923 [ ] stack_size' graph' (pi1 … entry') (pi1 … exit') in 924 let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals 925 (f_locals def) (f_params def) (f_result def) init in 889 926 let f_trans ≝ λlbl,stmt,def. 890 927 let pr ≝ translate_statement … lenv stmt in 891 b_adds_graph … (rtl_ertl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in 892 let res ≝ 893 mk_joint_internal_function RTL globals luniverse' runiverse' result' params' 894 locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in 895 foldi … f_trans (f_graph def) res. 896 897 [1,2: >graph_code_has_point @map_mem_prop [@graph_add_lookup] @graph_add 898  >(proj2_rewrite ????? pr_eq) 899 @initialize_local_env_in >EQ normalize nodelta %1 % 900 *: >(proj2_rewrite ????? pr_eq) 901 @(All_mp ??? (λpr.initialize_local_env_in ?? (\fst pr))) 902 [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) (f_locals def))) 903 [ #a #H @Exists_append_r @Exists_append_r @H 904  generalize in match (f_locals def); 905 ] 906  @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) (f_params def))) 907 [ #a #H @Exists_append_r @Exists_append_l @H 908  generalize in match (f_params def); 909 ] 910 ] 911 #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G} 912 ] 928 b_adds_graph … (rtl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in 929 foldi … f_trans (f_graph def) init'. 930 @hide_prf 931 >graph_code_has_point @map_mem_prop [@graph_add_lookup] @graph_add 913 932 qed. 914 933
Note: See TracChangeset
for help on using the changeset viewer.