[1280] | 1 | include "joint/Joint.ma". |
---|
[2286] | 2 | include "joint/blocks.ma". |
---|
| 3 | include "utilities/hide.ma". |
---|
[2716] | 4 | include "utilities/deqsets_extras.ma". |
---|
[1280] | 5 | |
---|
[2595] | 6 | (*include alias "basics/lists/list.ma". |
---|
[2286] | 7 | let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ) |
---|
| 8 | on n : |
---|
| 9 | freshT pars globals (Σl : list A. |l| = n) ≝ |
---|
| 10 | match n return λx.freshT … (Σl.|l| = x) with |
---|
| 11 | [ O ⇒ return «[ ], ?» |
---|
[1280] | 12 | | S n' ⇒ |
---|
[2286] | 13 | ! regs' ← repeat_fresh … fresh n'; |
---|
| 14 | ! reg ← fresh ; |
---|
| 15 | return «reg::regs',?» |
---|
[2595] | 16 | ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.*) |
---|
[2286] | 17 | |
---|
| 18 | definition fresh_label: |
---|
[2595] | 19 | ∀g_pars,globals.state_monad (joint_internal_function g_pars globals) label ≝ |
---|
[2286] | 20 | λg_pars,globals,def. |
---|
| 21 | let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in |
---|
| 22 | 〈set_luniverse … def luniverse, r〉. |
---|
| 23 | |
---|
[2595] | 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〉. |
---|
| 29 | |
---|
[2674] | 30 | (* insert into a graph a list of instructions *) |
---|
| 31 | let rec adds_graph_pre |
---|
| 32 | X |
---|
[2286] | 33 | (g_pars: graph_params) |
---|
| 34 | (globals: list ident) |
---|
[2674] | 35 | (* for ERTLptr: the label parameter is filled by the last label *) |
---|
| 36 | (pre_process : label → X → joint_seq g_pars globals) |
---|
| 37 | (insts: list X) |
---|
| 38 | (src : label) on insts : |
---|
| 39 | state_monad (joint_internal_function g_pars globals) label ≝ |
---|
| 40 | match insts with |
---|
| 41 | [ nil ⇒ return src |
---|
| 42 | | cons i rest ⇒ |
---|
| 43 | ! mid ← fresh_label … ; |
---|
| 44 | ! dst ← adds_graph_pre … pre_process rest mid ; |
---|
| 45 | !_ state_update … (add_graph … src (sequential … (pre_process dst i) mid)) ; |
---|
| 46 | return dst |
---|
[1280] | 47 | ]. |
---|
[2286] | 48 | |
---|
[2674] | 49 | let rec adds_graph_post |
---|
| 50 | (g_pars: graph_params) |
---|
| 51 | (globals: list ident) |
---|
| 52 | (insts: list (joint_seq g_pars globals)) |
---|
| 53 | (dst : label) on insts : |
---|
| 54 | state_monad (joint_internal_function g_pars globals) label ≝ |
---|
| 55 | match insts with |
---|
| 56 | [ nil ⇒ return dst |
---|
| 57 | | cons i rest ⇒ |
---|
| 58 | ! src ← fresh_label … ; |
---|
| 59 | ! mid ← adds_graph_post … rest dst ; |
---|
| 60 | !_ state_update … (add_graph … src (sequential … i mid)) ; |
---|
| 61 | return src |
---|
| 62 | ]. |
---|
| 63 | |
---|
[2595] | 64 | definition adds_graph : |
---|
| 65 | ∀g_pars : graph_params. |
---|
| 66 | ∀globals: list ident. |
---|
| 67 | ∀b : step_block g_pars globals. |
---|
| 68 | label → label → |
---|
| 69 | joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝ |
---|
| 70 | λg_pars,globals,insts,src,dst,def. |
---|
[2674] | 71 | let pref ≝ \fst (\fst insts) in |
---|
| 72 | let op ≝ \snd (\fst insts) in |
---|
| 73 | let post ≝ \snd insts in |
---|
| 74 | let 〈def, mid〉 ≝ adds_graph_pre … (λlbl,inst.inst lbl) pref src def in |
---|
| 75 | let 〈def, mid'〉 ≝ adds_graph_post … post dst def in |
---|
| 76 | add_graph … mid (sequential … (op mid) mid') def. |
---|
[2286] | 77 | |
---|
[2595] | 78 | definition fin_adds_graph : |
---|
[2286] | 79 | ∀g_pars : graph_params. |
---|
| 80 | ∀globals: list ident. |
---|
[2595] | 81 | ∀b : fin_block g_pars globals. |
---|
| 82 | label → |
---|
[2286] | 83 | joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝ |
---|
[2595] | 84 | λg_pars,globals,insts,src,def. |
---|
[2674] | 85 | let pref ≝ \fst insts in |
---|
| 86 | let last ≝ \snd insts in |
---|
| 87 | let 〈def, mid〉 ≝ adds_graph_pre … (λ_.λi.i) pref src def in |
---|
| 88 | add_graph … mid (final … last) def. |
---|
[2286] | 89 | |
---|
[2443] | 90 | (* ignoring register allocation for now *) |
---|
| 91 | |
---|
[2681] | 92 | (* |
---|
[2443] | 93 | definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝ |
---|
| 94 | λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def). |
---|
[2681] | 95 | *) |
---|
[2443] | 96 | (* |
---|
| 97 | lemma All_fresh_not_memb : ∀tag,u,l,id,u'. |
---|
| 98 | All (identifier tag) (λid'.¬fresh_for_univ tag id' u) l → |
---|
| 99 | 〈id, u'〉 = fresh tag u → |
---|
| 100 | ¬id ∈ l. |
---|
| 101 | #tag #u #l elim l [2: #hd #tl #IH] #id #u' * |
---|
| 102 | [ #hd_fresh #tl_fresh #EQfresh |
---|
| 103 | whd in ⊢ (?(?%)); |
---|
| 104 | change with (eq_identifier ???) in match (?==?); |
---|
| 105 | >eq_identifier_sym |
---|
| 106 | >(eq_identifier_false … (fresh_distinct … hd_fresh EQfresh)) |
---|
| 107 | normalize nodelta @(IH … tl_fresh EQfresh) |
---|
| 108 | | #_ % |
---|
| 109 | ] |
---|
| 110 | qed. |
---|
| 111 | |
---|
[2681] | 112 | |
---|
[2443] | 113 | lemma fresh_was_fresh : ∀tag,id,id',u,u'. |
---|
| 114 | 〈id,u'〉 = fresh tag u → |
---|
| 115 | fresh_for_univ tag id' u' → |
---|
| 116 | id' ≠ id → |
---|
| 117 | fresh_for_univ tag id' u. |
---|
| 118 | #tag * #id * #id' * #u * #u' |
---|
| 119 | normalize #EQfresh destruct |
---|
| 120 | #H #NEQ |
---|
| 121 | elim (le_to_or_lt_eq … H) |
---|
| 122 | [ (* not recompiling... /2 by monotonic_pred/ *) /2/ ] |
---|
| 123 | #H >(succ_injective … H) in NEQ; |
---|
| 124 | * #G elim (G (refl …)) |
---|
| 125 | qed. |
---|
| 126 | |
---|
[2595] | 127 | lemma fresh_not_in_univ : ∀tag,id,u,u'. |
---|
| 128 | 〈id, u'〉 = fresh tag u → |
---|
| 129 | ¬fresh_for_univ tag id u. |
---|
| 130 | #tag * #id * #u * #u' normalize #EQ destruct // |
---|
| 131 | qed. |
---|
[2681] | 132 | *) |
---|
[2674] | 133 | (* |
---|
[2595] | 134 | lemma adds_graph_list_fresh_preserve : |
---|
| 135 | ∀g_pars,globals,b,src,dst,def. |
---|
| 136 | let def' ≝ adds_graph_list g_pars globals b src dst def in |
---|
| 137 | ∀lbl.fresh_for_univ … lbl (joint_if_luniverse … def) → |
---|
| 138 | fresh_for_univ … lbl (joint_if_luniverse … def'). |
---|
| 139 | #g_pars #globals #l elim l -l |
---|
| 140 | [ #src #dst #def whd #lbl #H @H ] |
---|
| 141 | #hd1 * [ #_ #src #dst #def whd #lbl #H @H ] #hd2 #tl #IH #src #dst #def whd #lbl #H |
---|
| 142 | whd in match (adds_graph_list ??????); |
---|
| 143 | whd in match fresh_label; normalize nodelta |
---|
| 144 | inversion (fresh ??) #mid #luniv' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh |
---|
| 145 | normalize nodelta |
---|
| 146 | @IH whd in match (joint_if_luniverse ???); |
---|
| 147 | @(fresh_remains_fresh … EQfresh) @H |
---|
| 148 | qed. |
---|
| 149 | |
---|
| 150 | lemma with_last_not_empty : ∀X,pref,last.not_empty X (pref @ [last]). |
---|
| 151 | #X * [2: #hd #tl ] #last % qed. |
---|
| 152 | |
---|
| 153 | lemma split_on_last_ne_elim : ∀X,l.∀P : ((list X) × X) → Prop. |
---|
| 154 | (∀pref,last.pi1 ?? l = pref @ [last] → P 〈pref, last〉) → |
---|
| 155 | P (split_on_last_ne X l). |
---|
| 156 | #X * @list_elim_left [ * ] #last #pref #_ #prf #P #H |
---|
| 157 | >split_on_last_ne_def @H % qed. |
---|
| 158 | |
---|
[2443] | 159 | (* use Russell? *) |
---|
[2595] | 160 | lemma adds_graph_list_ok : |
---|
| 161 | ∀g_pars,globals,b,src,dst,def. |
---|
[2443] | 162 | fresh_for_univ … src (joint_if_luniverse … def) → |
---|
| 163 | luniverse_ok ?? def → |
---|
[2595] | 164 | let def' ≝ adds_graph_list g_pars globals b src dst def in |
---|
[2443] | 165 | luniverse_ok ?? def' ∧ |
---|
[2595] | 166 | (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) → |
---|
| 167 | stmt_at … (joint_if_code … def') lbl = |
---|
| 168 | stmt_at … (joint_if_code … def) lbl) ∧ |
---|
| 169 | let B ≝ ensure_step_block … b in |
---|
[2443] | 170 | ∃l.bool_to_Prop (uniqueb … l) ∧ |
---|
[2595] | 171 | All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ |
---|
| 172 | fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ |
---|
| 173 | src ~❨B,l❩~> dst in joint_if_code … def'. |
---|
| 174 | #p #g #l elim l -l [2: #hd1 * [ #_ | #hd2 #tl #IH ]] |
---|
| 175 | #src #dst #def #Hsrc #Hdef |
---|
| 176 | [1,3: % |
---|
| 177 | [1,3: % |
---|
| 178 | [1,3: #lbl @(eq_identifier_elim … lbl src) #H destruct [1,3: #_ @Hsrc ] |
---|
| 179 | whd in ⊢ (%→?); whd in match (adds_graph_list ??????); |
---|
| 180 | >(lookup_add_miss ?????? H) @Hdef |
---|
| 181 | |*: #lbl #H #G @lookup_add_miss @H |
---|
| 182 | ] |
---|
| 183 | |*: %{[]} % [1,3: %% ] %{src} % [1,3:%] %{dst} % [1,3: @lookup_add_hit ] % |
---|
| 184 | ] |
---|
| 185 | ] |
---|
| 186 | whd in match (adds_graph_list ??????); |
---|
[2557] | 187 | whd in match (fresh_label ???); |
---|
[2595] | 188 | inversion (fresh ??) normalize nodelta |
---|
| 189 | #mid #luniverse' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh |
---|
| 190 | letin def' ≝ (add_graph p g src (sequential … hd1 mid) (set_luniverse … def luniverse')) |
---|
| 191 | lapply (IH mid dst def' ??) |
---|
| 192 | [ #lbl @(eq_identifier_elim … lbl src) #H destruct |
---|
| 193 | [2: whd in ⊢ (%→?); whd in match (adds_graph_list ??????); |
---|
| 194 | >(lookup_add_miss ?????? H) ] |
---|
| 195 | #Hpres @(fresh_remains_fresh … EQfresh) [ @Hdef ] assumption |
---|
| 196 | | whd in match def'; |
---|
| 197 | @(fresh_is_fresh … EQfresh) |
---|
| 198 | ] |
---|
| 199 | whd in match (joint_if_luniverse ???); |
---|
| 200 | whd in match (joint_if_code ???); |
---|
| 201 | ** #Hdef'' #stmt_preserved * #l ** #Hl1 #Hl2 |
---|
| 202 | whd in ⊢ (%→?); @split_on_last_ne_elim #pref #last #EQ * #mid' * #Hl3 #Hl4 |
---|
| 203 | % |
---|
| 204 | [ %{Hdef''} #lbl #NEQ |
---|
| 205 | @(eq_identifier_elim ?? lbl mid) |
---|
| 206 | [ #EQ destruct #ABS cases (absurd ? ABS ?) @(fresh_not_in_univ … EQfresh) |
---|
| 207 | | #NEQ' #H >(stmt_preserved … NEQ') |
---|
| 208 | [ whd in match (joint_if_code ???); |
---|
| 209 | whd in match (stmt_at ????); >lookup_add_miss [2: @NEQ ] % |
---|
| 210 | | @(fresh_remains_fresh … EQfresh) @H |
---|
[2443] | 211 | ] |
---|
| 212 | ] |
---|
[2595] | 213 | ] |
---|
| 214 | %{(mid::l)} |
---|
| 215 | % [ % ] |
---|
| 216 | [ whd in ⊢ (?%); |
---|
| 217 | cut (Not (bool_to_Prop (mid∈l))) |
---|
| 218 | [ % #H elim (All_memb … Hl2 H) |
---|
| 219 | whd in match (joint_if_luniverse ???); |
---|
| 220 | #G #_ @(absurd ?? G) |
---|
| 221 | @ (fresh_is_fresh … EQfresh) |
---|
| 222 | | #H >H assumption |
---|
| 223 | ] |
---|
| 224 | | % |
---|
| 225 | [ %{(fresh_not_in_univ … EQfresh)} |
---|
| 226 | @adds_graph_list_fresh_preserve @(fresh_is_fresh … EQfresh) |
---|
| 227 | | @(All_mp … Hl2) #lbl * * #H1 #H2 %{H2} % #H3 @H1 |
---|
| 228 | @(fresh_remains_fresh … EQfresh) assumption |
---|
| 229 | ] |
---|
| 230 | | whd in match (ensure_step_block ???) in EQ ⊢ %; |
---|
| 231 | whd in match (map ??? (hd2 :: ?)); >EQ whd |
---|
| 232 | change with ((?::?)@?) in match (?::?@?); >split_on_last_ne_def |
---|
| 233 | %{mid'} % [2: @Hl4 ] |
---|
| 234 | %{Hl3} %{mid} >stmt_preserved |
---|
| 235 | [ % [2: % ] @lookup_add_hit |
---|
| 236 | | @(fresh_remains_fresh … EQfresh) assumption |
---|
| 237 | | % #ABS destruct @(absurd ? Hsrc) @(fresh_not_in_univ … EQfresh) |
---|
| 238 | ] |
---|
| 239 | ] |
---|
| 240 | qed. |
---|
[2674] | 241 | *) |
---|
[2681] | 242 | (* |
---|
[2595] | 243 | axiom adds_graph_ok : |
---|
| 244 | ∀g_pars,globals,B,src,dst,def. |
---|
| 245 | fresh_for_univ … src (joint_if_luniverse … def) → |
---|
| 246 | luniverse_ok ?? def → |
---|
| 247 | let def' ≝ adds_graph g_pars globals B src dst def in |
---|
| 248 | luniverse_ok ?? def' ∧ |
---|
| 249 | (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) → |
---|
| 250 | stmt_at … (joint_if_code … def') lbl = |
---|
| 251 | stmt_at … (joint_if_code … def) lbl) ∧ |
---|
| 252 | ∃l.bool_to_Prop (uniqueb … l) ∧ |
---|
| 253 | All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ |
---|
| 254 | fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ |
---|
[2675] | 255 | src ~❨B,src::l❩~> dst in joint_if_code … def'. |
---|
[2595] | 256 | |
---|
| 257 | axiom fin_adds_graph_ok : |
---|
| 258 | ∀g_pars,globals,B,src,def. |
---|
| 259 | fresh_for_univ … src (joint_if_luniverse … def) → |
---|
| 260 | luniverse_ok ?? def → |
---|
| 261 | let def' ≝ fin_adds_graph g_pars globals B src def in |
---|
| 262 | luniverse_ok ?? def' ∧ |
---|
| 263 | (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) → |
---|
| 264 | stmt_at … (joint_if_code … def') lbl = |
---|
| 265 | stmt_at … (joint_if_code … def) lbl) ∧ |
---|
| 266 | ∃l.bool_to_Prop (uniqueb … l) ∧ |
---|
| 267 | All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ |
---|
| 268 | fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ |
---|
[2675] | 269 | src ~❨B,src::l❩~> it in joint_if_code … def'. |
---|
[2681] | 270 | *) |
---|
[2595] | 271 | |
---|
[2681] | 272 | definition append_seq_list : |
---|
| 273 | ∀p,g.bind_step_block p g → bind_new register (list (joint_seq p g)) → |
---|
| 274 | bind_step_block p g ≝ |
---|
| 275 | λp,g,bbl,bl. |
---|
| 276 | ! 〈pref, op, post〉 ← bbl ; ! l ← bl ; return 〈pref, op, post @ l〉. |
---|
[2286] | 277 | |
---|
[2595] | 278 | (* |
---|
[2286] | 279 | definition insert_epilogue ≝ |
---|
| 280 | λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals). |
---|
| 281 | λdef : joint_internal_function g_pars globals. |
---|
| 282 | let exit ≝ joint_if_exit … def in |
---|
| 283 | match stmt_at … exit |
---|
| 284 | return λx.match x with [None ⇒ false | Some _ ⇒ true] → ? |
---|
| 285 | with |
---|
| 286 | [ Some s ⇒ λ_. |
---|
| 287 | let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in |
---|
| 288 | let def'' ≝ add_graph … tmp s def' in |
---|
| 289 | set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp |
---|
| 290 | | None ⇒ Ⓧ |
---|
| 291 | ] (pi2 … exit). |
---|
| 292 | whd in match def''; >graph_code_has_point // |
---|
[1280] | 293 | qed. |
---|
[2595] | 294 | *) |
---|
[1280] | 295 | |
---|
[2286] | 296 | definition b_adds_graph : |
---|
| 297 | ∀g_pars: graph_params. |
---|
| 298 | ∀globals: list ident. |
---|
[2595] | 299 | ∀b : bind_step_block g_pars globals. |
---|
| 300 | label → label → |
---|
[2286] | 301 | joint_internal_function g_pars globals→ |
---|
| 302 | joint_internal_function g_pars globals ≝ |
---|
[2595] | 303 | λg_pars,globals,insts,src,dst,def. |
---|
| 304 | let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in |
---|
| 305 | adds_graph … stmts src dst def. |
---|
[2286] | 306 | |
---|
[2681] | 307 | (* |
---|
[2595] | 308 | axiom b_adds_graph_ok : |
---|
| 309 | ∀g_pars,globals,B,src,dst,def. |
---|
| 310 | fresh_for_univ … src (joint_if_luniverse … def) → |
---|
| 311 | luniverse_ok ?? def → |
---|
| 312 | let def' ≝ b_adds_graph g_pars globals B src dst def in |
---|
| 313 | luniverse_ok ?? def' ∧ |
---|
| 314 | (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) → |
---|
| 315 | stmt_at … (joint_if_code … def') lbl = |
---|
| 316 | stmt_at … (joint_if_code … def) lbl) ∧ |
---|
| 317 | ∃l,r. |
---|
| 318 | bool_to_Prop (uniqueb … l) ∧ |
---|
| 319 | bool_to_Prop (uniqueb … r) ∧ |
---|
| 320 | All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ |
---|
| 321 | fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ |
---|
| 322 | All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧ |
---|
| 323 | fresh_for_univ … reg (joint_if_runiverse … def')) r ∧ |
---|
[2675] | 324 | src ~❨B,src::l,r❩~> dst in joint_if_code … def'. |
---|
[2681] | 325 | *) |
---|
[2595] | 326 | definition b_fin_adds_graph : |
---|
| 327 | ∀g_pars: graph_params. |
---|
| 328 | ∀globals: list ident. |
---|
| 329 | ∀b : bind_fin_block g_pars globals. |
---|
| 330 | label → |
---|
| 331 | joint_internal_function g_pars globals→ |
---|
| 332 | joint_internal_function g_pars globals ≝ |
---|
| 333 | λg_pars,globals,insts,src,def. |
---|
| 334 | let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in |
---|
| 335 | fin_adds_graph … stmts src def. |
---|
[2443] | 336 | |
---|
[2681] | 337 | (* |
---|
[2595] | 338 | axiom b_fin_adds_graph_ok : |
---|
| 339 | ∀g_pars,globals,B,src,def. |
---|
| 340 | fresh_for_univ … src (joint_if_luniverse … def) → |
---|
| 341 | luniverse_ok ?? def → |
---|
| 342 | let def' ≝ b_fin_adds_graph g_pars globals B src def in |
---|
| 343 | luniverse_ok ?? def' ∧ |
---|
| 344 | (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) → |
---|
| 345 | stmt_at … (joint_if_code … def') lbl = |
---|
| 346 | stmt_at … (joint_if_code … def) lbl) ∧ |
---|
| 347 | ∃l,r. |
---|
| 348 | bool_to_Prop (uniqueb … l) ∧ |
---|
| 349 | bool_to_Prop (uniqueb … r) ∧ |
---|
| 350 | All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ |
---|
| 351 | fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ |
---|
| 352 | All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧ |
---|
| 353 | fresh_for_univ … reg (joint_if_runiverse … def')) r ∧ |
---|
[2675] | 354 | src ~❨B,src::l,r❩~> it in joint_if_code … def'. |
---|
[2681] | 355 | *) |
---|
[2595] | 356 | |
---|
| 357 | definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝ |
---|
| 358 | λX,Y,f. |
---|
| 359 | (∀x.opt_All … (λys.bool_to_Prop (uniqueb … ys)) (f x)) ∧ |
---|
| 360 | (∀x1,x2. |
---|
| 361 | opt_All … |
---|
| 362 | (λys1. |
---|
| 363 | opt_All … |
---|
| 364 | (λys2. |
---|
| 365 | ∀y.y ∈ ys1 → y ∈ ys2 → x1 = x2) |
---|
| 366 | (f x2)) |
---|
| 367 | (f x1)). |
---|
| 368 | |
---|
| 369 | lemma opt_All_intro : ∀X,P,o. |
---|
| 370 | (∀x.o = Some ? x → P x) → opt_All X P o. #X #P * [//] #x #H @H % qed. |
---|
| 371 | |
---|
| 372 | (* |
---|
| 373 | definition points_of : ∀p,g.joint_internal_function p g → Type[0] ≝ |
---|
| 374 | λp,g,def.Σl.bool_to_Prop (code_has_point … (joint_if_code … def) l). |
---|
| 375 | |
---|
| 376 | unification hint 0 ≔ p, g, def; |
---|
| 377 | points ≟ code_point p, |
---|
| 378 | code ≟ joint_if_code p g def, |
---|
| 379 | P ≟ λl : points.bool_to_Prop (code_has_point p g code l) |
---|
| 380 | ⊢ |
---|
| 381 | points_of p g def ≡ Sig points P. |
---|
| 382 | |
---|
| 383 | definition stmt_at_safe : ∀p,g,def.points_of p g def → joint_statement p g ≝ |
---|
| 384 | λp,g,def,pt.opt_safe ? (stmt_at ?? (joint_if_code ?? def) (pi1 … pt)) ?. |
---|
| 385 | @hide_prf cases pt -pt #pt whd in ⊢ (?%→?); #H % #G >G in H; * qed. |
---|
| 386 | *) |
---|
| 387 | |
---|
[2681] | 388 | record b_graph_translate_data |
---|
| 389 | (src, dst : graph_params) |
---|
| 390 | (globals : list ident) : Type[0] ≝ |
---|
| 391 | { init_ret : call_dest dst |
---|
| 392 | ; init_params : paramsT dst |
---|
| 393 | ; init_stack_size : ℕ |
---|
| 394 | ; added_prologue : list (joint_seq dst globals) |
---|
| 395 | ; f_step : label → joint_step src globals → bind_step_block dst globals |
---|
| 396 | ; f_fin : label → joint_fin_step src → bind_fin_block dst globals |
---|
| 397 | ; good_f_step_good : |
---|
| 398 | ∀l,s.bind_new_P ?? |
---|
| 399 | (λblock.let 〈pref, op, post〉 ≝ block in |
---|
| 400 | All (label → joint_seq ??) |
---|
| 401 | (λs'.∀l.step_forall_labels … (In ? (l :: step_labels … s)) (s' l)) |
---|
| 402 | pref ∧ |
---|
| 403 | (∀l.step_forall_labels … (In ? (l :: step_labels … s)) (op l)) ∧ |
---|
| 404 | All (joint_seq ??) (step_forall_labels … (In ? (step_labels … s))) post) |
---|
| 405 | (f_step l s) |
---|
| 406 | ; good_f_fin : |
---|
| 407 | ∀l,s.bind_new_P ?? |
---|
| 408 | (λblock.let 〈pref, op〉 ≝ block in |
---|
| 409 | All (joint_seq ??) (step_forall_labels … (In ? (fin_step_labels … s))) pref ∧ |
---|
| 410 | All … (In ? (fin_step_labels … s)) (fin_step_labels … op)) |
---|
| 411 | (f_fin l s) |
---|
| 412 | ; f_step_on_cost : |
---|
[2688] | 413 | ∀l,c.f_step l (COST_LABEL … c) = |
---|
| 414 | bret ? (step_block ??) 〈[ ], λ_.COST_LABEL dst globals c, [ ]〉 |
---|
[2681] | 415 | }. |
---|
[2674] | 416 | |
---|
[2681] | 417 | definition get_first_costlabel : ∀p,g. |
---|
| 418 | joint_closed_internal_function p g → costlabel × (succ p) ≝ |
---|
| 419 | λp,g,def. |
---|
| 420 | match stmt_at … (joint_if_code … def) (joint_if_entry … def) |
---|
| 421 | return λx.stmt_at ???? = x → ? with |
---|
| 422 | [ Some s ⇒ |
---|
| 423 | match s return λx.stmt_at ???? = Some ? x → ? with |
---|
| 424 | [ sequential s' nxt ⇒ |
---|
| 425 | match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with |
---|
[2688] | 426 | [ COST_LABEL c ⇒ λ_.〈c, nxt〉 |
---|
[2681] | 427 | | _ ⇒ λabs.⊥ |
---|
| 428 | ] |
---|
| 429 | | _ ⇒ λabs.⊥ |
---|
| 430 | ] |
---|
| 431 | | _ ⇒ λabs.⊥ |
---|
| 432 | ] (refl …). |
---|
| 433 | @hide_prf |
---|
| 434 | cases def in abs; -def #def #good_def |
---|
| 435 | cases (entry_costed … good_def) #c * #nxt' #EQ >EQ #ABS destruct |
---|
| 436 | qed. |
---|
| 437 | |
---|
| 438 | record b_graph_translate_props |
---|
| 439 | (src_g_pars, dst_g_pars : graph_params) |
---|
| 440 | (globals: list ident) |
---|
| 441 | (data : b_graph_translate_data src_g_pars dst_g_pars globals) |
---|
| 442 | (data_regs : list register) |
---|
| 443 | (def_in : joint_closed_internal_function src_g_pars globals) |
---|
| 444 | (def_out : joint_closed_internal_function dst_g_pars globals) |
---|
| 445 | (f_lbls : label → option (list label)) |
---|
| 446 | (f_regs : label → option (list register)) : Prop ≝ |
---|
| 447 | { res_def_out_eq : |
---|
| 448 | joint_if_result … def_out = init_ret … data |
---|
| 449 | ; pars_def_out_eq : |
---|
| 450 | joint_if_params … def_out = init_params … data |
---|
| 451 | ; ss_def_out_eq : |
---|
| 452 | joint_if_stacksize … def_out = init_stack_size … data |
---|
| 453 | ; entry_eq : |
---|
| 454 | pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in) |
---|
| 455 | ; partition_lbls : partial_partition … f_lbls |
---|
| 456 | ; partition_regs : partial_partition … f_regs |
---|
| 457 | ; freshness_lbls : |
---|
[2595] | 458 | (∀l.opt_All … (All … |
---|
| 459 | (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ |
---|
[2681] | 460 | fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l)) |
---|
| 461 | ; freshness_regs : |
---|
[2595] | 462 | (∀l.opt_All … (All … |
---|
| 463 | (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ |
---|
[2681] | 464 | fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l)) |
---|
| 465 | ; freshness_data_regs : |
---|
| 466 | All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ |
---|
| 467 | fresh_for_univ … reg (joint_if_runiverse … def_out)) data_regs |
---|
| 468 | ; data_regs_disjoint : ∀l.opt_All … (λregs.∀r.r ∈ regs → r ∈ data_regs → False) (f_regs l) |
---|
| 469 | ; multi_fetch_ok : |
---|
[2595] | 470 | ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s → |
---|
| 471 | ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧ |
---|
| 472 | match s with |
---|
| 473 | [ sequential s' nxt ⇒ |
---|
[2681] | 474 | let block ≝ |
---|
| 475 | if eq_identifier … (joint_if_entry … def_in) l then |
---|
| 476 | append_seq_list … (f_step … data l s') (added_prologue … data) |
---|
| 477 | else |
---|
| 478 | f_step … data l s' in |
---|
| 479 | l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out |
---|
[2595] | 480 | | final s' ⇒ |
---|
[2681] | 481 | l ~❨f_fin … data l s', l::lbls, regs❩~> it in joint_if_code … def_out |
---|
[2595] | 482 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
[2681] | 483 | ] |
---|
| 484 | }. |
---|
[2595] | 485 | |
---|
[2681] | 486 | lemma if_merge_right : ∀A.∀b.∀x,y : A.x = y → if b then x else y = y. |
---|
| 487 | #A * #x #y #EQ >EQ % qed. |
---|
| 488 | |
---|
| 489 | lemma append_seq_list_nil : ∀p,g,b.append_seq_list p g b [ ] = b. |
---|
| 490 | #p #g #b elim b -b |
---|
| 491 | [ ** #a #b #c normalize >append_nil % |
---|
| 492 | | #f #IH @bnew_proper #r @IH |
---|
| 493 | ] |
---|
| 494 | qed. |
---|
| 495 | |
---|
| 496 | definition pair_swap : ∀A,B.(A × B) → B × A ≝ λA,B,pr.〈\snd pr, \fst pr〉. |
---|
| 497 | |
---|
| 498 | (* translation with inline fresh register allocation *) |
---|
| 499 | definition b_graph_translate : |
---|
| 500 | ∀src_g_pars,dst_g_pars : graph_params. |
---|
| 501 | ∀globals: list ident. |
---|
| 502 | (* initialization info *) |
---|
| 503 | ∀data : bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals). |
---|
| 504 | (* source function *) |
---|
| 505 | ∀def_in : joint_closed_internal_function src_g_pars globals. |
---|
| 506 | (* destination function *) |
---|
| 507 | Σdef_out : joint_closed_internal_function dst_g_pars globals. |
---|
| 508 | ∃data',regs,f_lbls,f_regs. |
---|
| 509 | bind_new_instantiates … data' data regs ∧ |
---|
| 510 | b_graph_translate_props … data' regs def_in def_out f_lbls f_regs |
---|
| 511 | ≝ |
---|
| 512 | λsrc_g_pars,dst_g_pars,globals,data,def. |
---|
| 513 | let runiv_data ≝ bcompile … (pair_swap ?? ∘ fresh RegisterTag) data (joint_if_runiverse … def) in |
---|
| 514 | let runiv ≝ \fst runiv_data in |
---|
| 515 | let data ≝ \snd runiv_data in |
---|
| 516 | let entry ≝ joint_if_entry … def in |
---|
| 517 | let init ≝ |
---|
| 518 | mk_joint_internal_function dst_g_pars globals |
---|
| 519 | (joint_if_luniverse … def) |
---|
| 520 | runiv |
---|
| 521 | (init_ret … data) (init_params … data) (init_stack_size … data) |
---|
| 522 | (add ?? (empty_map ? (joint_statement ??)) entry (RETURN …)) |
---|
| 523 | («pi1 … entry, mem_set_add_id …») in |
---|
| 524 | let f : label → joint_statement (src_g_pars : params) globals → |
---|
| 525 | joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ |
---|
| 526 | λlbl,stmt,def. |
---|
| 527 | match stmt with |
---|
| 528 | [ sequential inst next ⇒ |
---|
| 529 | b_adds_graph … (f_step … data lbl inst) lbl next def |
---|
| 530 | | final inst ⇒ |
---|
| 531 | b_fin_adds_graph … (f_fin … data lbl inst) lbl def |
---|
| 532 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
| 533 | ] in |
---|
| 534 | let def_out ≝ foldi ??? f (joint_if_code … def) init in |
---|
| 535 | let init_c_nxt ≝ get_first_costlabel … def in |
---|
| 536 | let def_out_nxt ≝ adds_graph_post … (added_prologue … data) (\snd (init_c_nxt)) def_out in |
---|
| 537 | ««add_graph … entry (sequential … (COST_LABEL … (\fst init_c_nxt)) (\snd def_out_nxt)) (\fst def_out_nxt), ?», ?». |
---|
| 538 | @hide_prf |
---|
| 539 | [ cases daemon |
---|
| 540 | | cases daemon (* TODO *) |
---|
| 541 | ] qed. |
---|
| 542 | |
---|
[2675] | 543 | definition b_graph_transform_program : |
---|
| 544 | ∀src_g_pars,dst_g_pars : graph_params. |
---|
| 545 | (* initialization *) |
---|
| 546 | (∀globals.joint_closed_internal_function src_g_pars globals → |
---|
[2681] | 547 | bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals)) → |
---|
| 548 | joint_program src_g_pars → |
---|
| 549 | joint_program dst_g_pars ≝ |
---|
| 550 | λsrc,dst,init,p. |
---|
[2675] | 551 | transform_program ??? p |
---|
| 552 | (λvarnames.transf_fundef ?? (λdef_in. |
---|
[2681] | 553 | b_graph_translate … (init varnames def_in) def_in)). |
---|
[2675] | 554 | |
---|
[2595] | 555 | definition added_registers : |
---|
| 556 | ∀p : graph_params.∀g. |
---|
| 557 | joint_internal_function p g → (label → option (list register)) → list register ≝ |
---|
| 558 | λp,g,def,f_regs. |
---|
| 559 | let f ≝ λlbl : label.λ_.λacc. |
---|
| 560 | match f_regs lbl with [ None ⇒ acc | Some regs ⇒ regs@acc ] in |
---|
| 561 | foldi … f (joint_if_code p g def) [ ]. |
---|
| 562 | |
---|
| 563 | axiom added_registers_ok : |
---|
| 564 | ∀p,g,def,f_regs. |
---|
| 565 | ∀l,s.stmt_at … (joint_if_code … def) l = Some ? s → |
---|
| 566 | opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l). |
---|
| 567 | |
---|
[2681] | 568 | (*(* translation without register allocation (more or less an alias) *) |
---|
[2286] | 569 | definition graph_translate : |
---|
| 570 | ∀src_g_pars,dst_g_pars : graph_params. |
---|
| 571 | ∀globals: list ident. |
---|
[2674] | 572 | (* initialization info *) |
---|
| 573 | call_dest dst_g_pars → (* joint_if_result *) |
---|
| 574 | paramsT dst_g_pars → (* joint_if_params *) |
---|
| 575 | ℕ → (* joint_if_stacksize *) |
---|
[2286] | 576 | (* functions dictating the translation *) |
---|
[2595] | 577 | (label → joint_step src_g_pars globals → step_block dst_g_pars globals) → |
---|
| 578 | (label → joint_fin_step src_g_pars → fin_block dst_g_pars globals) → |
---|
[2286] | 579 | (* source function *) |
---|
| 580 | joint_internal_function src_g_pars globals → |
---|
| 581 | (* destination function *) |
---|
| 582 | joint_internal_function dst_g_pars globals ≝ |
---|
[2674] | 583 | λsrc_g_pars,dst_g_pars,globals,init1,init2,init3,trans_step,trans_fin_step. |
---|
| 584 | b_graph_translate … init1 init2 init3 |
---|
[2595] | 585 | (λl,s.return trans_step l s) |
---|
| 586 | (λl,s.return trans_fin_step l s). |
---|
[2681] | 587 | *) |
---|
[2286] | 588 | (* |
---|
[1280] | 589 | let rec add_translates |
---|
| 590 | (pars1: params1) (globals: list ident) |
---|
| 591 | (translate_list: list ?) (start_lbl: label) (dest_lbl: label) |
---|
| 592 | (def: joint_internal_function … (graph_params pars1 globals)) |
---|
| 593 | on translate_list ≝ |
---|
| 594 | match translate_list with |
---|
[1282] | 595 | [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def |
---|
[1280] | 596 | | cons trans translate_list ⇒ |
---|
| 597 | match translate_list with |
---|
| 598 | [ nil ⇒ trans start_lbl dest_lbl def |
---|
| 599 | | _ ⇒ |
---|
[1284] | 600 | let 〈tmp_lbl, def〉 ≝ fresh_label … def in |
---|
[1280] | 601 | let def ≝ trans start_lbl tmp_lbl def in |
---|
[1284] | 602 | add_translates pars1 globals translate_list tmp_lbl dest_lbl def]]. |
---|
| 603 | |
---|
| 604 | definition adds_graph ≝ |
---|
| 605 | λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals). |
---|
[2286] | 606 | add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list). |
---|
| 607 | *) |
---|