[1075] | 1 | include "utilities/RegisterSet.ma". |
---|
[1076] | 2 | include "common/Identifiers.ma". |
---|
[2681] | 3 | include "RTL/RTL.ma". |
---|
[759] | 4 | include "ERTL/ERTL.ma". |
---|
[1280] | 5 | include "joint/TranslateUtils.ma". |
---|
[1252] | 6 | |
---|
[1995] | 7 | include alias "basics/lists/list.ma". |
---|
| 8 | |
---|
[2286] | 9 | definition save_hdws : |
---|
| 10 | ∀globals.list (register×Register) → list (joint_seq ERTL globals) ≝ |
---|
| 11 | λglobals. |
---|
[1254] | 12 | let save_hdws_internal ≝ |
---|
[2286] | 13 | λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in |
---|
| 14 | map ?? save_hdws_internal. |
---|
[1254] | 15 | |
---|
[2286] | 16 | definition restore_hdws : |
---|
| 17 | ∀globals.list (psd_argument×Register) → list (joint_seq ERTL globals) ≝ |
---|
| 18 | λglobals. |
---|
[1254] | 19 | let restore_hdws_internal ≝ |
---|
[2286] | 20 | λdestr_srcr:psd_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in |
---|
| 21 | map ? ? restore_hdws_internal. |
---|
[777] | 22 | |
---|
[2286] | 23 | definition get_params_hdw : |
---|
| 24 | ∀globals.list register → list (joint_seq ERTL globals) ≝ |
---|
| 25 | λglobals,params. |
---|
| 26 | save_hdws … (zip_pottier … params RegisterParams). |
---|
[777] | 27 | |
---|
[2286] | 28 | definition get_param_stack : |
---|
| 29 | ∀globals.register → register → register → |
---|
| 30 | list (joint_seq ERTL globals) ≝ |
---|
| 31 | λglobals,addr1,addr2,destr. |
---|
| 32 | (* liveness analysis will erase the last useless ops *) |
---|
| 33 | [ LOAD ?? destr addr1 addr2 ; |
---|
| 34 | addr1 ← addr1 .Add. (int_size : Byte) ; |
---|
| 35 | addr2 ← addr2 .Addc. zero_byte |
---|
| 36 | ]. |
---|
| 37 | |
---|
| 38 | definition get_params_stack : |
---|
[2806] | 39 | ∀globals.register → register → register → list register → |
---|
| 40 | list (joint_seq ERTL globals) ≝ |
---|
| 41 | λglobals. |
---|
| 42 | λtmpr,addr1,addr2,params. |
---|
[2286] | 43 | let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in |
---|
| 44 | [ (ertl_frame_size tmpr : joint_seq ??) ; |
---|
| 45 | CLEAR_CARRY ?? ; |
---|
| 46 | tmpr ← tmpr .Sub. params_length_byte ; (* will be constant later *) |
---|
| 47 | PSD addr1 ← HDW RegisterSPL ; |
---|
| 48 | PSD addr2 ← HDW RegisterSPH ; |
---|
| 49 | addr1 ← addr1 .Add. tmpr ; |
---|
| 50 | addr2 ← addr2 .Addc. zero_byte ] @ |
---|
| 51 | flatten … (map ?? (get_param_stack globals addr1 addr2) params). |
---|
[777] | 52 | |
---|
| 53 | definition get_params ≝ |
---|
[2806] | 54 | λglobals,tmpr,addr1,addr2,params. |
---|
[1257] | 55 | let n ≝ min (length … params) (length … RegisterParams) in |
---|
| 56 | let 〈hdw_params, stack_params〉 ≝ list_split … n params in |
---|
[2806] | 57 | get_params_hdw globals hdw_params @ get_params_stack … tmpr addr1 addr2 stack_params. |
---|
[1284] | 58 | |
---|
[2286] | 59 | definition save_return : |
---|
| 60 | ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝ |
---|
| 61 | λglobals,ret_regs. |
---|
[1075] | 62 | match reduce_strong ? ? RegisterSTS ret_regs with |
---|
[1601] | 63 | [ mk_Sig crl crl_proof ⇒ |
---|
[1071] | 64 | let commonl ≝ \fst (\fst crl) in |
---|
| 65 | let commonr ≝ \fst (\snd crl) in |
---|
| 66 | let restl ≝ \snd (\fst crl) in |
---|
[2286] | 67 | (* let restr ≝ \snd (\snd crl) in *) |
---|
| 68 | map2 … (λst.λr : psd_argument.HDW st ← r) commonl commonr crl_proof @ |
---|
| 69 | map … (λst.HDW st ← zero_byte) restl |
---|
[1071] | 70 | ]. |
---|
| 71 | |
---|
[2286] | 72 | definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝ |
---|
| 73 | λglobals. |
---|
| 74 | match reduce_strong ?? RegisterRets RegisterSTS with |
---|
[1601] | 75 | [ mk_Sig crl crl_proof ⇒ |
---|
[1075] | 76 | let commonl ≝ \fst (\fst crl) in |
---|
| 77 | let commonr ≝ \fst (\snd crl) in |
---|
[2286] | 78 | map2 … (λret,st.HDW ret ← HDW st) commonl commonr crl_proof |
---|
[1075] | 79 | ]. |
---|
| 80 | |
---|
[2681] | 81 | lemma All_map2 : ∀A,B,C,P,R,f,l1,l2,prf. |
---|
| 82 | All2 A B P l1 l2 → |
---|
| 83 | (∀x,y.P x y → R (f x y)) → |
---|
| 84 | All C R (map2 A B C f l1 l2 prf). |
---|
| 85 | #A #B #C #P #R #f #l1 elim l1 -l1 |
---|
| 86 | [ * [ #prf * #H % ] #hd' #tl' |
---|
| 87 | | #hd #tl #IH * [2: #hd' #tl' ] |
---|
| 88 | ] #prf normalize in prf; destruct |
---|
| 89 | * #H1 #H2 #H % [ @H @H1 | @IH assumption ] qed. |
---|
| 90 | |
---|
| 91 | lemma All2_True : ∀A,B,l1,l2.|l1| = |l2| → All2 A B (λ_.λ_.True) l1 l2. |
---|
| 92 | #A #B #l1 elim l1 -l1 |
---|
| 93 | [ * [ #prf % ] #hd' #tl' |
---|
| 94 | | #hd #tl #IH * [2: #hd' #tl' ] |
---|
| 95 | ] #prf normalize in prf; destruct %{I} @IH assumption |
---|
| 96 | qed. |
---|
| 97 | |
---|
| 98 | lemma All_True : ∀A,l.All A (λ_.True) l. |
---|
| 99 | #A #l elim l -l [ % | #hd #tl #IH %{I IH} ] qed. |
---|
| 100 | |
---|
[2286] | 101 | definition epilogue : |
---|
| 102 | ∀globals.list register → register → register → list (register × Register) → |
---|
[2681] | 103 | Σl : list (joint_seq ERTL globals). |
---|
| 104 | All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝ |
---|
[2286] | 105 | λglobals,ret_regs,sral,srah,sregs. |
---|
| 106 | save_return … (map … (Reg ?) ret_regs) @ |
---|
| 107 | restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @ |
---|
| 108 | [ PUSH ERTL ? srah ; |
---|
| 109 | PUSH … sral ; |
---|
| 110 | ertl_del_frame ] @ |
---|
| 111 | assign_result globals. |
---|
[2681] | 112 | @hide_prf |
---|
| 113 | @All_append |
---|
| 114 | [ whd in match save_return; normalize nodelta |
---|
| 115 | cases (reduce_strong ????) ** #a #b * #c #d #prf normalize nodelta |
---|
| 116 | @All_append |
---|
| 117 | [ @(All_map2 … (All2_True … prf)) #x #y #_ % |
---|
| 118 | | @(All_map … (All_True …)) #x #_ % |
---|
| 119 | ] |
---|
| 120 | | @All_append |
---|
| 121 | [ @(All_map … (All_True …)) #x #_ % |
---|
| 122 | | %{(refl …)} %{(refl …)} %{(refl …)} |
---|
| 123 | whd in match assign_result; |
---|
| 124 | generalize in match reduce_strong; #f normalize nodelta |
---|
| 125 | cases (f ????) #l #prf normalize nodelta |
---|
| 126 | @(All_map2 … (All2_True … prf)) #x #y #_ % |
---|
| 127 | ] |
---|
| 128 | ] |
---|
| 129 | qed. |
---|
[1258] | 130 | |
---|
[2681] | 131 | definition prologue : |
---|
[2806] | 132 | ∀globals.list register → register → register → register → register → register → |
---|
| 133 | list (register×Register) → |
---|
[2681] | 134 | bind_new register (list (joint_seq ERTL globals)) ≝ |
---|
[2806] | 135 | λglobals,params,sral,srah,tmpr,addr1,addr2,sregs. |
---|
[2681] | 136 | [ (ertl_new_frame : joint_seq ??) ; |
---|
| 137 | POP … sral ; |
---|
| 138 | POP … srah |
---|
[2806] | 139 | ] @ save_hdws … sregs @ get_params … tmpr addr1 addr2 params. |
---|
[1075] | 140 | |
---|
[2286] | 141 | definition set_params_hdw : |
---|
| 142 | ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝ |
---|
[1258] | 143 | λglobals,params. |
---|
[2286] | 144 | restore_hdws globals (zip_pottier ? ? params RegisterParams). |
---|
| 145 | |
---|
| 146 | (* Paolo: The following can probably be done way more efficiently with INC DPTR *) |
---|
| 147 | |
---|
| 148 | definition set_param_stack : |
---|
| 149 | ∀globals.register → register → psd_argument → |
---|
| 150 | list (joint_seq ERTL globals) ≝ |
---|
| 151 | λglobals,addr1,addr2,arg. |
---|
| 152 | [ STORE … addr1 addr2 arg ; |
---|
| 153 | addr1 ← addr1 .Add. (int_size : Byte) ; |
---|
| 154 | addr2 ← addr2 .Addc. zero_byte |
---|
[1075] | 155 | ]. |
---|
| 156 | |
---|
[2286] | 157 | definition set_params_stack : |
---|
[2681] | 158 | ∀globals.list psd_argument → bind_new register ? ≝ |
---|
[1259] | 159 | λglobals,params. |
---|
[2286] | 160 | νaddr1,addr2 in |
---|
| 161 | let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in |
---|
| 162 | [ PSD addr1 ← HDW RegisterSPL ; |
---|
| 163 | PSD addr2 ← HDW RegisterSPH ; |
---|
| 164 | CLEAR_CARRY ?? ; |
---|
| 165 | addr1 ← addr1 .Sub. params_length_byte ; |
---|
| 166 | addr2 ← addr2 .Sub. zero_byte |
---|
| 167 | ] @ |
---|
| 168 | flatten … (map … (set_param_stack globals addr1 addr2) params). |
---|
[1075] | 169 | |
---|
[2681] | 170 | definition set_params : |
---|
| 171 | ∀globals.list psd_argument → |
---|
| 172 | Σb : bind_new register (list (joint_seq ERTL globals)). |
---|
| 173 | BindNewP … (All (joint_seq ??) (λs.step_labels … s = [ ])) b ≝ |
---|
[1259] | 174 | λglobals,params. |
---|
[1149] | 175 | let n ≝ min (|params|) (|RegisterParams|) in |
---|
[2035] | 176 | let hdw_stack_params ≝ split ? params n in |
---|
[1075] | 177 | let hdw_params ≝ \fst hdw_stack_params in |
---|
| 178 | let stack_params ≝ \snd hdw_stack_params in |
---|
[2286] | 179 | set_params_hdw globals hdw_params @@ set_params_stack globals stack_params. |
---|
[2681] | 180 | @hide_prf |
---|
| 181 | @mp_bind [3: #l1 #H1 @mp_bind [3: #l2 #H2 @(All_append … H1 H2) ] |*:] |
---|
| 182 | [ #r1 #r2 |
---|
| 183 | %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)} |
---|
| 184 | @All_append [ % ] |
---|
| 185 | elim stack_params [ % ] #hd #tl #IH whd in match flatten; normalize nodelta |
---|
| 186 | whd in match (foldr ?????); %{(refl …)} %{(refl …)} %{(refl …)} @IH |
---|
| 187 | | whd whd in match set_params_hdw; normalize nodelta |
---|
| 188 | whd in match restore_hdws; normalize nodelta @(All_map … (All_True …)) |
---|
| 189 | #a #_ % |
---|
| 190 | ] |
---|
| 191 | qed. |
---|
[1075] | 192 | |
---|
[2286] | 193 | definition fetch_result : |
---|
[2681] | 194 | ∀globals.list register → |
---|
| 195 | Σl : list (joint_seq ERTL globals). |
---|
| 196 | All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝ |
---|
[2286] | 197 | λglobals,ret_regs. |
---|
| 198 | match reduce_strong ?? RegisterSTS RegisterRets with |
---|
| 199 | [ mk_Sig crl crl_proof ⇒ |
---|
[1075] | 200 | let commonl ≝ \fst (\fst crl) in |
---|
| 201 | let commonr ≝ \fst (\snd crl) in |
---|
[2286] | 202 | map2 … (λst,r.HDW st ← HDW r) commonl commonr crl_proof @ |
---|
| 203 | match reduce_strong ?? ret_regs RegisterSTS with |
---|
| 204 | [ mk_Sig crl crl_proof ⇒ |
---|
[1075] | 205 | let commonl ≝ \fst (\fst crl) in |
---|
| 206 | let commonr ≝ \fst (\snd crl) in |
---|
[2286] | 207 | map2 … (λret,st.PSD ret ← HDW st) commonl commonr crl_proof |
---|
| 208 | ] |
---|
| 209 | ]. |
---|
[2681] | 210 | @hide_prf |
---|
| 211 | @All_append |
---|
| 212 | [ @(All_map2 … (All2_True … crl_proof)) #x #y #_ % |
---|
| 213 | | cases (reduce_strong ????) #l #prf normalize nodelta |
---|
| 214 | @(All_map2 … (All2_True … prf)) #x #y #_ % |
---|
| 215 | ] |
---|
| 216 | qed. |
---|
[1075] | 217 | |
---|
[2286] | 218 | definition translate_step : |
---|
[2681] | 219 | ∀globals.label → joint_step RTL globals → |
---|
| 220 | bind_step_block ERTL globals ≝ |
---|
[2286] | 221 | λglobals.λ_.λs. |
---|
[2681] | 222 | match s return λ_.bind_step_block ?? with |
---|
[2286] | 223 | [ step_seq s ⇒ |
---|
[2806] | 224 | bret … match s return λ_.step_block ?? with |
---|
| 225 | [ PUSH _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *) |
---|
| 226 | | POP _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *) |
---|
| 227 | | MOVE rs ⇒ [PSD (\fst rs) ← \snd rs] |
---|
[2286] | 228 | | ADDRESS x prf r1 r2 ⇒ |
---|
[2806] | 229 | [ADDRESS ERTL ? x prf r1 r2] |
---|
[2286] | 230 | | OPACCS op destr1 destr2 srcr1 srcr2 ⇒ |
---|
[2806] | 231 | [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2] |
---|
[2286] | 232 | | OP1 op1 destr srcr ⇒ |
---|
[2806] | 233 | [OP1 ERTL ? op1 destr srcr] |
---|
[2286] | 234 | | OP2 op2 destr srcr1 srcr2 ⇒ |
---|
[2806] | 235 | [OP2 ERTL ? op2 destr srcr1 srcr2] |
---|
[2286] | 236 | | CLEAR_CARRY ⇒ |
---|
[2806] | 237 | [CLEAR_CARRY ??] |
---|
[2286] | 238 | | SET_CARRY ⇒ |
---|
[2806] | 239 | [SET_CARRY ??] |
---|
[2286] | 240 | | LOAD destr addr1 addr2 ⇒ |
---|
[2806] | 241 | [LOAD ERTL ? destr addr1 addr2] |
---|
[2286] | 242 | | STORE addr1 addr2 srcr ⇒ |
---|
[2806] | 243 | [STORE ERTL ? addr1 addr2 srcr] |
---|
[2286] | 244 | | COMMENT msg ⇒ |
---|
[2806] | 245 | [COMMENT … msg] |
---|
[2286] | 246 | | extension_seq ext ⇒ |
---|
[2806] | 247 | match ext return λ_.step_block ?? with |
---|
[2286] | 248 | [ rtl_stack_address addr1 addr2 ⇒ |
---|
[2806] | 249 | [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ] |
---|
[1075] | 250 | ] |
---|
[2286] | 251 | ] |
---|
[2689] | 252 | | COST_LABEL lbl ⇒ |
---|
| 253 | bret … 〈[ ], λ_.COST_LABEL ERTL ? lbl, [ ]〉 |
---|
[2681] | 254 | | CALL f args ret_regs ⇒ |
---|
| 255 | ! pref ← pi1 … (set_params ? args) ; |
---|
| 256 | bret ? (step_block ??) 〈add_dummy_variance … pref, |
---|
| 257 | λ_.CALL ERTL ? f (|args|) it, |
---|
| 258 | fetch_result ? ret_regs〉 |
---|
[2286] | 259 | | COND r ltrue ⇒ |
---|
[2681] | 260 | bret … 〈[ ], λ_.COND ERTL ? r ltrue, [ ]〉 |
---|
[2490] | 261 | ]. |
---|
[1075] | 262 | |
---|
[2286] | 263 | definition translate_fin_step : |
---|
[2681] | 264 | ∀globals.list register → register → register → list (register × Register) → |
---|
| 265 | label → joint_fin_step RTL → |
---|
| 266 | bind_fin_block ERTL globals ≝ |
---|
| 267 | λglobals.λret_regs,ral,rah,to_restore.λ_.λs. |
---|
| 268 | match s return λ_.bind_fin_block ERTL ? with |
---|
| 269 | [ GOTO lbl' ⇒ bret … 〈[ ], GOTO … lbl'〉 |
---|
| 270 | | RETURN ⇒ bret … 〈epilogue … ret_regs ral rah to_restore, RETURN ?〉 |
---|
| 271 | | TAILCALL b _ _ ⇒ match b in False with [ ] |
---|
[2286] | 272 | ]. |
---|
[1075] | 273 | |
---|
[2681] | 274 | definition allocate_regs : |
---|
| 275 | ∀X : Type[0]. |
---|
[2806] | 276 | (list (register×Register) → bind_new register X) → |
---|
[2681] | 277 | bind_new register X ≝ |
---|
| 278 | λX,f. |
---|
| 279 | let allocate_regs_internal ≝ |
---|
| 280 | λacc : bind_new register (list (register × Register)). |
---|
| 281 | λr: Register. |
---|
| 282 | ! tl ← acc ; |
---|
| 283 | νr' in return (〈r', r〉 :: tl) in |
---|
| 284 | ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSaved ; |
---|
[2806] | 285 | f to_save. |
---|
[1077] | 286 | |
---|
[2681] | 287 | definition translate_data : |
---|
| 288 | ∀globals.joint_closed_internal_function RTL globals → |
---|
[2806] | 289 | bound_b_graph_translate_data RTL ERTL globals ≝ |
---|
[2681] | 290 | λglobals,def. |
---|
| 291 | let params ≝ joint_if_params … def in |
---|
| 292 | let new_stacksize ≝ |
---|
| 293 | joint_if_stacksize … def + (|params| - |RegisterParams|) in |
---|
[2806] | 294 | allocate_regs ? |
---|
| 295 | (λto_save. |
---|
| 296 | νral,rah,tmpr,addr1,addr2 in |
---|
| 297 | ! prologue ← prologue globals params ral rah tmpr addr1 addr2 to_save ; |
---|
[2681] | 298 | return mk_b_graph_translate_data RTL ERTL globals |
---|
| 299 | (* init_ret ≝ *) it |
---|
| 300 | (* init_params ≝ *) (|params|) |
---|
| 301 | (* init_stack_size ≝ *) new_stacksize |
---|
| 302 | (* added_prologue ≝ *) prologue |
---|
[2862] | 303 | (* new_regs ≝ *) (reverse … (addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save)) |
---|
[2681] | 304 | (* f_step ≝ *) (translate_step globals) |
---|
| 305 | (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save) |
---|
[2806] | 306 | ????). |
---|
[2681] | 307 | @hide_prf |
---|
[2806] | 308 | [1,2: cases daemon (* TODO *) |
---|
| 309 | | #l #c % |
---|
| 310 | | #l * [ #c' | #f #args #dest | #a #ltrue | #s ] #c whd |
---|
| 311 | [2: #r1 #r2 ] whd #l' #EQ destruct try % |
---|
| 312 | cases s in EQ; whd in match ensure_step_block; normalize nodelta |
---|
| 313 | try #a try #b try #c try #d try #e try #f destruct |
---|
| 314 | cases a in b; #a1 #a2 normalize nodelta #EQ destruct |
---|
[2862] | 315 | | #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2 |
---|
[2861] | 316 | % (* XXX: FAILS, unintentional list reversal??? *) |
---|
[2806] | 317 | ] |
---|
| 318 | (* #l * |
---|
[2681] | 319 | [ #l whd %{I} %{I} %1 % |
---|
| 320 | | whd %{I} cases (epilogue ?????) @All_mp #s #EQ whd >EQ % |
---|
| 321 | | * |
---|
[2689] | 322 | | #c %{I} %{I} #l % |
---|
[2681] | 323 | | #called #args #dest @(mp_bind … (BindNewP …)) |
---|
| 324 | [2: @(pi2 ? (λ_.?)) |*:] #l1 #H1 whd % [%] |
---|
| 325 | [ @(All_map … H1) #a #EQ #l whd >EQ % |
---|
| 326 | | #l % |
---|
| 327 | | cases (fetch_result ??) @All_mp #s #EQ whd >EQ % |
---|
| 328 | ] |
---|
| 329 | | #a #l_true whd %{I} %{I} #l %{I} %2 %1 % |
---|
| 330 | | * try #a try #b try #c try #d try #e whd |
---|
| 331 | try (%{I} %{I} #l %) |
---|
| 332 | cases a -a #a #b whd %{I} % [ %{I} ] #l % |
---|
[2806] | 333 | ]*) |
---|
[2681] | 334 | qed. |
---|
| 335 | |
---|
[2286] | 336 | (* removing this because of how insert_prologue is now defined |
---|
[1077] | 337 | definition generate ≝ |
---|
[1262] | 338 | λglobals. |
---|
[1077] | 339 | λstmt. |
---|
[2286] | 340 | λdef: joint_internal_function globals ERTL. |
---|
[1284] | 341 | let 〈entry, def〉 ≝ fresh_label … def in |
---|
| 342 | let graph ≝ add … (joint_if_code … def) entry stmt in |
---|
[2286] | 343 | set_joint_if_graph … (ERTL globals) graph def ??. |
---|
[1284] | 344 | [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *) |
---|
| 345 | | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF |
---|
| 346 | *) cases daemon (*CSC: XXX *) |
---|
| 347 | ] |
---|
[1079] | 348 | qed. |
---|
[1262] | 349 | |
---|
| 350 | let rec find_and_remove_first_cost_label_internal (globals: list ident) |
---|
| 351 | (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat) |
---|
[1079] | 352 | on num_nodes ≝ |
---|
| 353 | match num_nodes with |
---|
| 354 | [ O ⇒ 〈None ?, def〉 |
---|
| 355 | | S num_nodes' ⇒ |
---|
[1262] | 356 | match lookup … (joint_if_code … def) lbl with |
---|
[1079] | 357 | [ None ⇒ 〈None ?, def〉 |
---|
[1262] | 358 | | Some stmt ⇒ |
---|
[1079] | 359 | match stmt with |
---|
[1282] | 360 | [ sequential inst lbl ⇒ |
---|
[1262] | 361 | match inst with |
---|
[1282] | 362 | [ COST_LABEL cost_lbl ⇒ |
---|
[2286] | 363 | 〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉 |
---|
[1262] | 364 | | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ] |
---|
[1282] | 365 | | RETURN ⇒ 〈None …, def〉 |
---|
| 366 | | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' |
---|
[1262] | 367 | ]]]. |
---|
[1079] | 368 | |
---|
| 369 | definition find_and_remove_first_cost_label ≝ |
---|
[1262] | 370 | λglobals,def. |
---|
| 371 | find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)). |
---|
[1077] | 372 | |
---|
[1079] | 373 | definition move_first_cost_label_up_internal ≝ |
---|
[1262] | 374 | λglobals,def. |
---|
| 375 | let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in |
---|
[1079] | 376 | match cost_label with |
---|
| 377 | [ None ⇒ def |
---|
[2286] | 378 | | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def |
---|
[1079] | 379 | ]. |
---|
[1077] | 380 | |
---|
[1262] | 381 | definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)). |
---|
[2286] | 382 | *) |
---|
[1262] | 383 | |
---|
[1995] | 384 | definition rtl_to_ertl : rtl_program → ertl_program ≝ |
---|
[2681] | 385 | b_graph_transform_program … translate_data. |
---|