Changeset 2595 for src/joint/TranslateUtils.ma
 Timestamp:
 Jan 30, 2013, 7:25:39 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/TranslateUtils.ma
r2557 r2595 4 4 include "utilities/deqsets.ma". 5 5 6 (* general type of functions generating fresh things *) 7 definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g). 8 9 include alias "basics/lists/list.ma". 6 (*include alias "basics/lists/list.ma". 10 7 let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ) 11 8 on n : … … 17 14 ! reg ← fresh ; 18 15 return «reg::regs',?» 19 ]. [%  @hide_prf cases regs' #l #EQ normalize >EQ % ] qed. 16 ]. [%  @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.*) 20 17 21 18 definition fresh_label: 22 ∀g_pars,globals. freshT globals g_parslabel ≝19 ∀g_pars,globals.state_monad (joint_internal_function g_pars globals) label ≝ 23 20 λg_pars,globals,def. 24 21 let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in 25 22 〈set_luniverse … def luniverse, r〉. 23 24 definition fresh_register: 25 ∀g_pars,globals.state_monad (joint_internal_function g_pars globals) register ≝ 26 λg_pars,globals,def. 27 let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in 28 〈set_runiverse … def runiverse, r〉. 26 29 27 30 (* insert into a graph a block of instructions *) … … 29 32 (g_pars: graph_params) 30 33 (globals: list ident) 31 (insts: list (joint_s eqg_pars globals))32 (src : label) on insts : state_monad (joint_internal_function g_pars globals) label≝33 match insts with34 [ nil ⇒ return src34 (insts: list (joint_step g_pars globals)) 35 (src : label) (dst : label) on insts : joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝ 36 λdef.match insts with 37 [ nil ⇒ add_graph … src (sequential … (NOOP …) dst) def 35 38  cons instr others ⇒ 36 ! mid ← fresh_label … ; 37 ! def ← state_get … ; 38 !_ state_set … (add_graph … src (sequential … instr mid) def) ; 39 adds_graph_list g_pars globals others mid 40 ]. 41 42 definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with 43 [ inl _ ⇒ true 44  inr _ ⇒ false 45 ]. 46 definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with 47 [ inl _ ⇒ true 48  inr _ ⇒ false 39 match others with 40 [ nil ⇒ add_graph … src (sequential … instr dst) def 41  _ ⇒ 42 let 〈def', mid〉 ≝ fresh_label … def in 43 let def'' ≝ add_graph … src (sequential … instr mid) def' in 44 adds_graph_list … others mid dst def'' 45 ] 49 46 ]. 50 47 … … 52 49 ∀g_pars : graph_params. 53 50 ∀globals: list ident. 54 ∀b : seq_block g_pars globals (joint_step g_pars globals) + 55 seq_block g_pars globals (joint_fin_step g_pars). 56 label → if is_inl … b then label else unit → 51 ∀b : step_block g_pars globals. 52 label → label → 57 53 joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝ 58 λg_pars,globals,insts,src. 59 match insts return λx.if is_inl … x then ? else ? → ? → ? with 60 [ inl b ⇒ λdst,def. 61 let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in 62 add_graph … mid (sequential … (\snd b) dst) def 63  inr b ⇒ λdst,def. 64 let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in 65 add_graph … mid (final … (\snd b)) def 54 λg_pars,globals,insts,src,dst,def. 55 let 〈pref, last〉 ≝ split_on_last_ne … insts in 56 match pref with 57 [ nil ⇒ add_graph … src (sequential … (last src) dst) def 58  _ ⇒ 59 let 〈def', lbl〉 ≝ fresh_label … def in 60 let def'' ≝ adds_graph_list … (map_eval … pref lbl) src lbl def' in 61 add_graph … lbl (sequential … (last lbl) dst) def'' 62 ]. 63 64 definition fin_adds_graph : 65 ∀g_pars : graph_params. 66 ∀globals: list ident. 67 ∀b : fin_block g_pars globals. 68 label → 69 joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝ 70 λg_pars,globals,insts,src,def. 71 let 〈pref, last〉 ≝ insts in 72 match pref with 73 [ nil ⇒ add_graph … src (final … last) def 74  _ ⇒ 75 let 〈def', lbl〉 ≝ fresh_label … def in 76 let def'' ≝ adds_graph_list … pref src lbl def' in 77 add_graph … lbl (final … last) def'' 66 78 ]. 67 79 … … 70 82 definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝ 71 83 λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def). 72 73 lemma present_to_memb : ∀tag,A,l,m.present tag A m l → bool_to_Prop (l∈m).74 #tag #A * #l * #m whd in ⊢ (%→?%);75 elim (lookup tag ???)76 [ * #ABS elim (ABS ?) %77  #a #_ %78 ] qed.79 80 lemma memb_to_present : ∀tag,A,l,m.l∈m → present tag A m l.81 #tag #A * #l * #m whd in ⊢ (?%→%);82 elim (lookup tag ???)83 [ *  #a * % #ABS destruct(ABS) ] qed.84 84 85 85 (* … … 114 114 qed. 115 115 116 lemma fresh_not_in_univ : ∀tag,id,u,u'. 117 〈id, u'〉 = fresh tag u → 118 ¬fresh_for_univ tag id u. 119 #tag * #id * #u * #u' normalize #EQ destruct // 120 qed. 121 122 lemma adds_graph_list_fresh_preserve : 123 ∀g_pars,globals,b,src,dst,def. 124 let def' ≝ adds_graph_list g_pars globals b src dst def in 125 ∀lbl.fresh_for_univ … lbl (joint_if_luniverse … def) → 126 fresh_for_univ … lbl (joint_if_luniverse … def'). 127 #g_pars #globals #l elim l l 128 [ #src #dst #def whd #lbl #H @H ] 129 #hd1 * [ #_ #src #dst #def whd #lbl #H @H ] #hd2 #tl #IH #src #dst #def whd #lbl #H 130 whd in match (adds_graph_list ??????); 131 whd in match fresh_label; normalize nodelta 132 inversion (fresh ??) #mid #luniv' #EQfresh lapply (sym_eq ??? EQfresh) EQfresh #EQfresh 133 normalize nodelta 134 @IH whd in match (joint_if_luniverse ???); 135 @(fresh_remains_fresh … EQfresh) @H 136 qed. 137 138 lemma with_last_not_empty : ∀X,pref,last.not_empty X (pref @ [last]). 139 #X * [2: #hd #tl ] #last % qed. 140 141 lemma split_on_last_ne_elim : ∀X,l.∀P : ((list X) × X) → Prop. 142 (∀pref,last.pi1 ?? l = pref @ [last] → P 〈pref, last〉) → 143 P (split_on_last_ne X l). 144 #X * @list_elim_left [ * ] #last #pref #_ #prf #P #H 145 >split_on_last_ne_def @H % qed. 146 116 147 (* use Russell? *) 117 axiomadds_graph_list_ok :118 ∀g_pars,globals,b,src,d ef.148 lemma adds_graph_list_ok : 149 ∀g_pars,globals,b,src,dst,def. 119 150 fresh_for_univ … src (joint_if_luniverse … def) → 120 151 luniverse_ok ?? def → 121 let 〈def', dst〉 ≝ adds_graph_list g_pars globals b srcdef in152 let def' ≝ adds_graph_list g_pars globals b src dst def in 122 153 luniverse_ok ?? def' ∧ 154 (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) → 155 stmt_at … (joint_if_code … def') lbl = 156 stmt_at … (joint_if_code … def) lbl) ∧ 157 let B ≝ ensure_step_block … b in 123 158 ∃l.bool_to_Prop (uniqueb … l) ∧ 124 All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ 125 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ 126 src ~❨b,l❩~> dst in joint_if_code … def'. 127 (* 128 #p #g #l elim l l 129 [ #src #def #_ #Hdef whd 130 %{Hdef} %{[ ]} %%% ] 131 #hd #tl #IH #src #def #src_fresh #Hdef 132 whd in match (adds_graph_list ?????); 159 All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ 160 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ 161 src ~❨B,l❩~> dst in joint_if_code … def'. 162 #p #g #l elim l l [2: #hd1 * [ #_  #hd2 #tl #IH ]] 163 #src #dst #def #Hsrc #Hdef 164 [1,3: % 165 [1,3: % 166 [1,3: #lbl @(eq_identifier_elim … lbl src) #H destruct [1,3: #_ @Hsrc ] 167 whd in ⊢ (%→?); whd in match (adds_graph_list ??????); 168 >(lookup_add_miss ?????? H) @Hdef 169 *: #lbl #H #G @lookup_add_miss @H 170 ] 171 *: %{[]} % [1,3: %% ] %{src} % [1,3:%] %{dst} % [1,3: @lookup_add_hit ] % 172 ] 173 ] 174 whd in match (adds_graph_list ??????); 133 175 whd in match (fresh_label ???); 134 @(pair_elim … (fresh ??)) normalize nodelta 135 #mid #luniverse' #EQfresh 136 whd in ⊢ (match % with [ _ ⇒ ?]); 137 letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse')) 138 cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def) 139 [ % ] #EQ_aux 140 lapply (IH mid def' ??) 141 [ #l whd in match def'; #Hpres 142 lapply (present_to_memb … Hpres) Hpres 143 >mem_set_add @eq_identifier_elim 144 [ #EQ destruct(EQ) * 145  #NEQ change with (? ∈ joint_if_code p ??) in ⊢ (?%→?); >EQ_aux 146 #l_in 176 inversion (fresh ??) normalize nodelta 177 #mid #luniverse' #EQfresh lapply (sym_eq ??? EQfresh) EQfresh #EQfresh 178 letin def' ≝ (add_graph p g src (sequential … hd1 mid) (set_luniverse … def luniverse')) 179 lapply (IH mid dst def' ??) 180 [ #lbl @(eq_identifier_elim … lbl src) #H destruct 181 [2: whd in ⊢ (%→?); whd in match (adds_graph_list ??????); 182 >(lookup_add_miss ?????? H) ] 183 #Hpres @(fresh_remains_fresh … EQfresh) [ @Hdef ] assumption 184  whd in match def'; 185 @(fresh_is_fresh … EQfresh) 186 ] 187 whd in match (joint_if_luniverse ???); 188 whd in match (joint_if_code ???); 189 ** #Hdef'' #stmt_preserved * #l ** #Hl1 #Hl2 190 whd in ⊢ (%→?); @split_on_last_ne_elim #pref #last #EQ * #mid' * #Hl3 #Hl4 191 % 192 [ %{Hdef''} #lbl #NEQ 193 @(eq_identifier_elim ?? lbl mid) 194 [ #EQ destruct #ABS cases (absurd ? ABS ?) @(fresh_not_in_univ … EQfresh) 195  #NEQ' #H >(stmt_preserved … NEQ') 196 [ whd in match (joint_if_code ???); 197 whd in match (stmt_at ????); >lookup_add_miss [2: @NEQ ] % 198  @(fresh_remains_fresh … EQfresh) @H 147 199 ] 148 @(fresh_remains_fresh … (sym_eq … EQfresh))149 [2: @Hdef @memb_to_present ] assumption150  whd in match def';151 cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9152 whd in match (set_luniverse ????);153 @(fresh_is_fresh … (sym_eq … EQfresh))154 200 ] 155 elim (adds_graph_list ?????) #def'' #mid' normalize nodelta 156 * #Hdef'' * #l ** #Hl1 #Hl2 #Hl3 %{Hdef''} %{(mid::l)} 157 % [ % ] 158 [ whd in ⊢ (?%); 159 cut (Not (bool_to_Prop (mid∈l))) 160 [ % #H elim (All_memb … Hl2 H) 161 whd in match (joint_if_luniverse ???); 162 #G #_ @(absurd ?? G) 163 @ (fresh_is_fresh … (sym_eq … EQfresh)) 164  #H >H assumption 165 ] 166  % 167 [ % 168 [ 169 normalize #H10 #H11 170 171 >(All_fresh_not_memb … (sym_eq … EQfresh)) 172 [ assumption ] 173 @(All_mp … Hl2) #lbl * 174 cases def in EQfresh; #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 175 normalize #EQfresh #H #lbl_not_mid 176 lapply(fresh_remains_fresh … H (sym_eq … EQfresh)) 177 178 elim (true_or_false_Prop (mid∈l)) #mid_l >mid_l 179 [ normalize 180 *) 201 ] 202 %{(mid::l)} 203 % [ % ] 204 [ whd in ⊢ (?%); 205 cut (Not (bool_to_Prop (mid∈l))) 206 [ % #H elim (All_memb … Hl2 H) 207 whd in match (joint_if_luniverse ???); 208 #G #_ @(absurd ?? G) 209 @ (fresh_is_fresh … EQfresh) 210  #H >H assumption 211 ] 212  % 213 [ %{(fresh_not_in_univ … EQfresh)} 214 @adds_graph_list_fresh_preserve @(fresh_is_fresh … EQfresh) 215  @(All_mp … Hl2) #lbl * * #H1 #H2 %{H2} % #H3 @H1 216 @(fresh_remains_fresh … EQfresh) assumption 217 ] 218  whd in match (ensure_step_block ???) in EQ ⊢ %; 219 whd in match (map ??? (hd2 :: ?)); >EQ whd 220 change with ((?::?)@?) in match (?::?@?); >split_on_last_ne_def 221 %{mid'} % [2: @Hl4 ] 222 %{Hl3} %{mid} >stmt_preserved 223 [ % [2: % ] @lookup_add_hit 224  @(fresh_remains_fresh … EQfresh) assumption 225  % #ABS destruct @(absurd ? Hsrc) @(fresh_not_in_univ … EQfresh) 226 ] 227 ] 228 qed. 229 230 axiom adds_graph_ok : 231 ∀g_pars,globals,B,src,dst,def. 232 fresh_for_univ … src (joint_if_luniverse … def) → 233 luniverse_ok ?? def → 234 let def' ≝ adds_graph g_pars globals B src dst def in 235 luniverse_ok ?? def' ∧ 236 (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) → 237 stmt_at … (joint_if_code … def') lbl = 238 stmt_at … (joint_if_code … def) lbl) ∧ 239 ∃l.bool_to_Prop (uniqueb … l) ∧ 240 All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ 241 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ 242 src ~❨B,l❩~> dst in joint_if_code … def'. 243 244 axiom fin_adds_graph_ok : 245 ∀g_pars,globals,B,src,def. 246 fresh_for_univ … src (joint_if_luniverse … def) → 247 luniverse_ok ?? def → 248 let def' ≝ fin_adds_graph g_pars globals B src def in 249 luniverse_ok ?? def' ∧ 250 (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) → 251 stmt_at … (joint_if_code … def') lbl = 252 stmt_at … (joint_if_code … def) lbl) ∧ 253 ∃l.bool_to_Prop (uniqueb … l) ∧ 254 All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ 255 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ 256 src ~❨B,l❩~> it in joint_if_code … def'. 181 257 182 258 (* preserves first statement if a cost label (should be an invariant) *) … … 189 265 with 190 266 [ Some s ⇒ λ_. 267 let default_add ≝ λ_ : unit. 268 let 〈def', lbl〉 ≝ fresh_label … def in 269 let def'' ≝ add_graph … lbl s def' in 270 adds_graph … insts entry lbl def'' in 191 271 match s with 192 272 [ sequential s' next ⇒ … … 195 275 match s'' with 196 276 [ COST_LABEL _ ⇒ 197 adds_graph ?? ( inl … (s'' :: insts)) entry next def277 adds_graph ?? (s'' :: insts) entry next def 198 278  _ ⇒ 199 let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in 200 add_graph … tmp s def' 279 default_add it 201 280 ] 202 281  _ ⇒ 203 let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in 204 add_graph … tmp s def' 282 default_add it 205 283 ] 206 284  _ ⇒ 207 let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in 208 add_graph … tmp s def' 285 default_add it 209 286 ] 210 287  None ⇒ Ⓧ 211 288 ] (pi2 … entry). 212 289 290 (* 213 291 definition insert_epilogue ≝ 214 292 λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals). … … 226 304 whd in match def''; >graph_code_has_point // 227 305 qed. 306 *) 228 307 229 308 definition b_adds_graph : 230 309 ∀g_pars: graph_params. 231 310 ∀globals: list ident. 232 (* fresh register creation *) 233 freshT g_pars globals (localsT … g_pars) → 234 ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) + 235 bind_seq_block g_pars globals (joint_fin_step g_pars). 236 label → if is_inl … b then label else unit → 311 ∀b : bind_step_block g_pars globals. 312 label → label → 237 313 joint_internal_function g_pars globals→ 238 314 joint_internal_function g_pars globals ≝ 239 λg_pars,globals,fresh_r,insts,src. 240 match insts return λx.if is_inl … x then ? else ? → ? → ? with 241 [ inl b ⇒ λdst,def. 242 let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in 243 adds_graph … (inl … stmts) src dst def 244  inr b ⇒ λdst,def. 245 let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in 246 adds_graph … (inr … stmts) src dst def 247 ]. 248 249 315 λg_pars,globals,insts,src,dst,def. 316 let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in 317 adds_graph … stmts src dst def. 318 319 axiom b_adds_graph_ok : 320 ∀g_pars,globals,B,src,dst,def. 321 fresh_for_univ … src (joint_if_luniverse … def) → 322 luniverse_ok ?? def → 323 let def' ≝ b_adds_graph g_pars globals B src dst def in 324 luniverse_ok ?? def' ∧ 325 (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) → 326 stmt_at … (joint_if_code … def') lbl = 327 stmt_at … (joint_if_code … def) lbl) ∧ 328 ∃l,r. 329 bool_to_Prop (uniqueb … l) ∧ 330 bool_to_Prop (uniqueb … r) ∧ 331 All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ 332 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ 333 All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧ 334 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧ 335 src ~❨B,l,r❩~> dst in joint_if_code … def'. 336 337 definition b_fin_adds_graph : 338 ∀g_pars: graph_params. 339 ∀globals: list ident. 340 ∀b : bind_fin_block g_pars globals. 341 label → 342 joint_internal_function g_pars globals→ 343 joint_internal_function g_pars globals ≝ 344 λg_pars,globals,insts,src,def. 345 let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in 346 fin_adds_graph … stmts src def. 347 348 axiom b_fin_adds_graph_ok : 349 ∀g_pars,globals,B,src,def. 350 fresh_for_univ … src (joint_if_luniverse … def) → 351 luniverse_ok ?? def → 352 let def' ≝ b_fin_adds_graph g_pars globals B src def in 353 luniverse_ok ?? def' ∧ 354 (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) → 355 stmt_at … (joint_if_code … def') lbl = 356 stmt_at … (joint_if_code … def) lbl) ∧ 357 ∃l,r. 358 bool_to_Prop (uniqueb … l) ∧ 359 bool_to_Prop (uniqueb … r) ∧ 360 All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ 361 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ 362 All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧ 363 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧ 364 src ~❨B,l,r❩~> it in joint_if_code … def'. 250 365 251 366 (* translation with inline fresh register allocation *) … … 253 368 ∀src_g_pars,dst_g_pars : graph_params. 254 369 ∀globals: list ident. 255 (* fresh register creation *)256 freshT dst_g_pars globals (localsT dst_g_pars) →257 370 (* initialized function definition with empty graph *) 258 371 joint_internal_function dst_g_pars globals → 259 372 (* functions dictating the translation *) 260 (label → joint_step src_g_pars globals → 261 bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) → 262 (label → joint_fin_step src_g_pars → 263 bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) → 373 (label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) → 374 (label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) → 264 375 (* source function *) 265 376 joint_internal_function src_g_pars globals → 266 377 (* destination function *) 267 378 joint_internal_function dst_g_pars globals ≝ 268 λsrc_g_pars,dst_g_pars,globals, fresh_reg,empty,trans_step,trans_fin_step,def.379 λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def. 269 380 let f : label → joint_statement (src_g_pars : params) globals → 270 381 joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ … … 272 383 match stmt with 273 384 [ sequential inst next ⇒ 274 b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def385 b_adds_graph … (trans_step lbl inst) lbl next def 275 386  final inst ⇒ 276 b_ adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl itdef387 b_fin_adds_graph … (trans_fin_step lbl inst) lbl def 277 388  FCOND abs _ _ _ ⇒ Ⓧabs 278 389 ] in 279 390 foldi … f (joint_if_code … def) empty. 280 391 281 (* translation without register allocation *) 392 definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝ 393 λX,Y,f. 394 (∀x.opt_All … (λys.bool_to_Prop (uniqueb … ys)) (f x)) ∧ 395 (∀x1,x2. 396 opt_All … 397 (λys1. 398 opt_All … 399 (λys2. 400 ∀y.y ∈ ys1 → y ∈ ys2 → x1 = x2) 401 (f x2)) 402 (f x1)). 403 404 lemma opt_All_intro : ∀X,P,o. 405 (∀x.o = Some ? x → P x) → opt_All X P o. #X #P * [//] #x #H @H % qed. 406 407 (* 408 definition points_of : ∀p,g.joint_internal_function p g → Type[0] ≝ 409 λp,g,def.Σl.bool_to_Prop (code_has_point … (joint_if_code … def) l). 410 411 unification hint 0 ≔ p, g, def; 412 points ≟ code_point p, 413 code ≟ joint_if_code p g def, 414 P ≟ λl : points.bool_to_Prop (code_has_point p g code l) 415 ⊢ 416 points_of p g def ≡ Sig points P. 417 418 definition stmt_at_safe : ∀p,g,def.points_of p g def → joint_statement p g ≝ 419 λp,g,def,pt.opt_safe ? (stmt_at ?? (joint_if_code ?? def) (pi1 … pt)) ?. 420 @hide_prf cases pt pt #pt whd in ⊢ (?%→?); #H % #G >G in H; * qed. 421 *) 422 423 axiom b_graph_translate_ok : 424 ∀src_g_pars,dst_g_pars : graph_params. 425 ∀globals: list ident.∀empty.∀f_step,f_fin,def_in. 426 luniverse_ok ?? def_in → 427 let def_out ≝ 428 b_graph_translate src_g_pars dst_g_pars globals empty f_step f_fin def_in in 429 luniverse_ok … def_out ∧ 430 joint_if_result … def_out = joint_if_result … empty ∧ 431 joint_if_params … def_out = joint_if_params … empty ∧ 432 joint_if_stacksize … def_out = joint_if_stacksize … empty ∧ 433 pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in) ∧ 434 ∃f_lbls : label → option (list label). 435 ∃f_regs : label → option (list register). 436 partial_partition … f_lbls ∧ 437 partial_partition … f_regs ∧ 438 (∀l.opt_All … (All … 439 (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ 440 fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l)) ∧ 441 (∀l.opt_All … (All … 442 (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 443 fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l)) ∧ 444 ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s → 445 ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧ 446 match s with 447 [ sequential s' nxt ⇒ 448 l ~❨f_step l s', lbls, regs❩~> nxt in joint_if_code … def_out 449  final s' ⇒ 450 l ~❨f_fin l s', lbls, regs❩~> it in joint_if_code … def_out 451  FCOND abs _ _ _ ⇒ Ⓧabs 452 ]. 453 454 definition added_registers : 455 ∀p : graph_params.∀g. 456 joint_internal_function p g → (label → option (list register)) → list register ≝ 457 λp,g,def,f_regs. 458 let f ≝ λlbl : label.λ_.λacc. 459 match f_regs lbl with [ None ⇒ acc  Some regs ⇒ regs@acc ] in 460 foldi … f (joint_if_code p g def) [ ]. 461 462 axiom added_registers_ok : 463 ∀p,g,def,f_regs. 464 ∀l,s.stmt_at … (joint_if_code … def) l = Some ? s → 465 opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l). 466 467 (* translation without register allocation (more or less an alias) *) 282 468 definition graph_translate : 283 469 ∀src_g_pars,dst_g_pars : graph_params. … … 286 472 joint_internal_function dst_g_pars globals → 287 473 (* functions dictating the translation *) 288 (label → joint_step src_g_pars globals → 289 seq_block dst_g_pars globals (joint_step dst_g_pars globals)) → 290 (label → joint_fin_step src_g_pars → 291 seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) → 474 (label → joint_step src_g_pars globals → step_block dst_g_pars globals) → 475 (label → joint_fin_step src_g_pars → fin_block dst_g_pars globals) → 292 476 (* source function *) 293 477 joint_internal_function src_g_pars globals → 294 478 (* destination function *) 295 479 joint_internal_function dst_g_pars globals ≝ 296 λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def. 297 let f : label → joint_statement (src_g_pars : params) globals → 298 joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 299 λlbl,stmt,def. 300 match stmt with 301 [ sequential inst next ⇒ 302 adds_graph … (inl … (trans_step lbl inst)) lbl next def 303  final inst ⇒ 304 adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def 305  FCOND abs _ _ _ ⇒ Ⓧabs 306 ] in 307 foldi … f (joint_if_code … def) empty. 308 480 λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step. 481 b_graph_translate … empty 482 (λl,s.return trans_step l s) 483 (λl,s.return trans_fin_step l s). 484 485 (* helper for initializing a valid init graph (with a valid entry) *) 309 486 definition init_graph_if ≝ 310 487 λg_pars : graph_params.λglobals. 311 λluniverse,runiverse,ret,params,locals,stack_size,entry,exit. 312 let graph ≝ add ? ? (empty_map ? (joint_statement ??)) entry (GOTO … exit) in 313 let graph ≝ add ? ? graph exit (RETURN …) in 488 λluniverse,runiverse,ret,params,stack_size,entry. 489 let graph ≝ add ?? (empty_map ? (joint_statement ??)) entry (RETURN …) in 314 490 mk_joint_internal_function g_pars globals 315 luniverse runiverse ret params locals stack_size 316 graph entry exit. 317 >graph_code_has_point @map_mem_prop 318 [@graph_add_lookup] @graph_add 491 luniverse runiverse ret params stack_size 492 graph entry. 493 @hide_prf >graph_code_has_point @map_mem_prop @graph_add 319 494 qed. 320 495
Note: See TracChangeset
for help on using the changeset viewer.