Changeset 2595
- Timestamp:
- Jan 30, 2013, 7:25:39 PM (8 years ago)
- Location:
- src/joint
- Files:
-
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/Joint.ma
r2562 r2595 88 88 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *) 89 89 ; paramsT : Type[0] 90 ; localsT: Type[0]91 90 }. 92 91 … … 409 408 joint_if_result : call_dest p; 410 409 joint_if_params : paramsT p; 411 joint_if_locals : list (localsT p); (* use void where no locals are present *)412 410 (*CSC: XXXXX stacksize unused for LTL-...*) 413 411 joint_if_stacksize: nat; 414 412 joint_if_code : codeT p globals ; 415 joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) ;416 joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) 413 joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) (*; 414 joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *) 417 415 }. 418 416 … … 431 429 λgraph: codeT pars globals. 432 430 λentry. 433 λexit.431 (*λexit.*) 434 432 mk_joint_internal_function pars globals 435 433 (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun) 436 (joint_if_params … int_fun) (joint_if_ locals … int_fun) (joint_if_stacksize … int_fun)437 graph entry exit.434 (joint_if_params … int_fun) (joint_if_stacksize … int_fun) 435 graph entry (*exit*). 438 436 439 437 definition set_joint_if_graph ≝ … … 442 440 λp:joint_internal_function pars globals. 443 441 λentry_prf. 444 λexit_prf.442 (*λexit_prf.*) 445 443 set_joint_code globals pars p 446 444 graph 447 445 (mk_Sig ?? (joint_if_entry ?? p) entry_prf) 448 ( mk_Sig … (joint_if_exit ?? p) exit_prf).446 (*(mk_Sig … (joint_if_exit ?? p) exit_prf)*). 449 447 450 448 definition set_luniverse ≝ … … 454 452 mk_joint_internal_function globals pars 455 453 luniverse (joint_if_runiverse … p) (joint_if_result … p) 456 (joint_if_params … p) (joint_if_ locals … p) (joint_if_stacksize … p)457 (joint_if_code … p) (joint_if_entry … p) ( joint_if_exit … p).454 (joint_if_params … p) (joint_if_stacksize … p) 455 (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*). 458 456 459 457 definition set_runiverse ≝ … … 463 461 mk_joint_internal_function globals pars 464 462 (joint_if_luniverse … p) runiverse (joint_if_result … p) 465 (joint_if_params … p) (joint_if_ locals … p) (joint_if_stacksize … p)466 (joint_if_code … p) (joint_if_entry … p) ( joint_if_exit … p).463 (joint_if_params … p) (joint_if_stacksize … p) 464 (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*). 467 465 468 466 (* Specialized for graph_params *) … … 473 471 mk_joint_internal_function … 474 472 (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) 475 (joint_if_params … p) (joint_if_ locals … p) (joint_if_stacksize … p)473 (joint_if_params … p) (joint_if_stacksize … p) 476 474 code 477 475 (pi1 … (joint_if_entry … p)) 478 ( pi1 … (joint_if_exit … p)).476 (*(pi1 … (joint_if_exit … p))*). 479 477 >graph_code_has_point whd in match code; >mem_set_add 480 @orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ]478 @orb_Prop_r elim (joint_if_entry ???) 481 479 #x #H <graph_code_has_point @H 482 480 qed. 483 481 484 definition set_locals ≝485 λpars,globals.486 λp : joint_internal_function pars globals.487 λlocals.488 mk_joint_internal_function pars globals489 (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)490 (joint_if_params … p) locals (joint_if_stacksize … p)491 (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).492 493 482 definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals). 494 483 -
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 -
src/joint/blocks.ma
r2422 r2595 42 42 (list (block_step p globals)) × A.*) 43 43 44 definition seq_block ≝ λp : stmt_params.λglobals,A. 45 (list (joint_seq p globals)) × A. 44 (* move *) 45 let rec bind_new_P R X (P : X → Prop) (b : bind_new R X) on b : Prop ≝ 46 match b with 47 [ bret x ⇒ P x 48 | bnew f ⇒ ∀x.bind_new_P … P (f x) 49 ]. 50 51 definition BindNewP : ∀R.MonadPred (BindNew R) ≝ 52 λR.mk_MonadPred (BindNew R) (bind_new_P R) ???. 53 [ #X #P #x #K @K 54 | #X #Y #Pin #Pout #m elim m -m 55 [ #x #H #f #G @G @H 56 | #g #IH #H #f #G #x @IH [ @H | @G ] 57 ] 58 | #X #P #Q #H #m elim m -m 59 [ #x #Px @H @Px 60 | #g #IH #Pg #x @IH @Pg 61 ] 62 ] 63 qed. 64 65 definition not_empty : ∀X.list X → Prop ≝ λX,l.match l with [ nil ⇒ False | _ ⇒ True ]. 66 67 definition head_ne : ∀X.(Σl.not_empty X l) → X ≝ 68 λX,l. 69 match l return λl.not_empty ? l → ? with 70 [ nil ⇒ Ⓧ 71 | cons hd _ ⇒ λ_.hd 72 ] (pi2 … l). 73 74 75 let rec split_on_last_ne_aux X l on l : not_empty X l → (list X) × X ≝ 76 match l return λx.not_empty ? x → ? with 77 [ nil ⇒ Ⓧ 78 | cons hd tl ⇒ λ_. 79 match tl return λtl.(not_empty X tl → ?) → ? with 80 [ nil ⇒ λ_.〈[ ], hd〉 81 | cons hd' tl' ⇒ λrec_call.let 〈pre, last〉 ≝ rec_call I in 〈hd :: pre, last〉 82 ] (split_on_last_ne_aux ? tl) 83 ]. 84 85 definition split_on_last_ne : ∀X.(Σl.not_empty X l) → (list X)×X ≝ 86 λX,l.split_on_last_ne_aux … (pi2 … l). 87 88 definition last_ne : ∀X.(Σl.not_empty X l) → X ≝ λX,l.\snd (split_on_last_ne … l). 89 definition chop_last_ne : ∀X.(Σl.not_empty X l) → list X ≝ λX,l.\fst (split_on_last_ne … l). 90 91 lemma split_on_last_ne_def : ∀X,pre,last,prf.split_on_last_ne X «pre@[last], prf» = 〈pre, last〉. 92 whd in match split_on_last_ne; normalize nodelta 93 #X #pre elim pre -pre [ #last #prf % ] 94 #hd * [2: #hd' #tl'] #IH #last * 95 [ whd in ⊢ (??%?); >IH % | % ] 96 qed. 97 98 lemma split_on_last_ne_inv : ∀X,l. 99 pi1 ?? l = (let 〈pre, last〉 ≝ split_on_last_ne X l in pre @ [last]). 100 whd in match split_on_last_ne; normalize nodelta 101 #X * #l elim l -l [ * ] 102 #hd * [2: #hd' #tl'] #IH * [2: % ] 103 whd in match (split_on_last_ne_aux ???); 104 lapply (IH I) @pair_elim #pre #last #_ #EQ >EQ % 105 qed. 106 107 (* the label input is to accomodate ERTptr pass *) 108 definition step_block ≝ λp,globals.Σl : list (code_point p → joint_step p globals).not_empty ? l. 109 unification hint 0 ≔ p : params, g; 110 S ≟ code_point p → joint_step p g, 111 L ≟ list S, 112 P ≟ not_empty S 113 (*---------------------------------------*)⊢ 114 step_block p g ≡ Sig L P. 115 116 definition fin_block ≝ λp,globals.(list (joint_step p globals))×(joint_fin_step p). 46 117 47 118 (*definition seq_to_skip_block : … … 53 124 seq_to_skip_block on _b : seq_block ??? to skip_block ???.*) 54 125 55 definition bind_s eq_block ≝ λp : stmt_params.λglobals,A.56 bind_new (localsT p) (seq_block p globals A).57 unification hint 0 ≔ p : stmt_params, g, X; 58 R ≟ localsT p, 59 P ≟ s eq_block p g X126 definition bind_step_block ≝ λp.λglobals. 127 bind_new register (step_block p globals). 128 129 unification hint 0 ≔ p, g; 130 P ≟ step_block p g 60 131 (*---------------------------------------*)⊢ 61 bind_seq_block p g X ≡ bind_new R P. 62 63 definition bind_seq_list ≝ λp : stmt_params.λglobals. 64 bind_new (localsT p) (list (joint_seq p globals)). 132 bind_step_block p g ≡ bind_new register P. 133 134 definition bind_fin_block ≝ λp : stmt_params.λglobals. 135 bind_new register (fin_block p globals). 136 65 137 unification hint 0 ≔ p : stmt_params, g; 66 R ≟ localsT p, 67 S ≟ joint_seq p g, 138 P ≟ fin_block p g 139 (*---------------------------------------*)⊢ 140 bind_fin_block p g ≡ bind_new register P. 141 142 definition bind_step_list ≝ λp : stmt_params.λglobals. 143 bind_new register (list (joint_step p globals)). 144 unification hint 0 ≔ p : stmt_params, g; 145 S ≟ joint_step p g, 68 146 L ≟ list S 69 147 (*---------------------------------------*)⊢ 70 bind_seq_list p g ≡ bind_new R L. 148 bind_step_list p g ≡ bind_new register L. 149 150 definition add_dummy_variance : ∀X,Y : Type[0].list Y → list (X → Y) ≝ λX,Y.map … (λx.λ_.x). 151 152 definition ensure_step_block : ∀p : params.∀globals. 153 list (joint_step p globals) → step_block p globals ≝ 154 λp,g,l.match add_dummy_variance … l return λ_.Σl.not_empty ? l with 155 [ nil ⇒ «[λ_.NOOP ??], I» 156 | cons hd tl ⇒ «hd :: tl, I» 157 ]. 158 159 definition ensure_step_list : ∀p,globals. 160 list (joint_seq p globals) → list (joint_step p globals) ≝ 161 λp,g.map … (step_seq …). 162 163 definition ensure_step_block_from_seq : ∀p : params.∀globals. 164 list (joint_seq p globals) → step_block p globals ≝ 165 λp,g.ensure_step_block ?? ∘ ensure_step_list ??. 166 167 coercion step_block_from_list nocomposites : ∀p : params.∀g.∀l : list (joint_step p g).step_block p g ≝ 168 ensure_step_block on _l : list (joint_step ??) to step_block ??. 169 170 coercion step_list_from_seq nocomposites : ∀p,g.∀l : list (joint_seq p g).list (joint_step p g) ≝ 171 ensure_step_list on _l : list (joint_seq ??) to list (joint_step ??). 172 173 coercion step_block_from_seq nocomposites : ∀p : params.∀g.∀l : list (joint_seq p g).step_block p g ≝ 174 ensure_step_block_from_seq on _l : list (joint_seq ??) to step_block ??. 175 71 176 72 177 (*definition bind_skip_block ≝ λp : stmt_params.λglobals,A. … … 90 195 seq_or_fin_step_classifier ?? (\snd b). 91 196 *) 92 93 let rec split_on_last A (dflt : A) (l : list A) on l : (list A) × A ≝ 94 match l with 95 [ nil ⇒ 〈[ ], dflt〉 96 | cons hd tl ⇒ 97 match tl with 98 [ nil ⇒ 〈[ ], hd〉 99 | _ ⇒ 100 let 〈pref, post〉 ≝ split_on_last A dflt tl in 101 〈hd :: pref, post〉 102 ] 103 ]. 104 105 lemma split_on_last_ok : 106 ∀A,dflt,l. 107 match l with 108 [ nil ⇒ True 109 | _ ⇒ l = (let 〈pre, post〉 ≝ split_on_last A dflt l in pre @ [post]) 110 ]. 111 #A #dflt #l elim l normalize nodelta 112 [ % 113 | #hd * [ #_ %] 114 #hd' #tl #IH whd in match (split_on_last ???); >IH in ⊢ (??%?); 115 elim (split_on_last ???) #a #b % 116 ] 117 qed. 118 119 definition seq_block_from_seq_list : 197 (*definition seq_block_from_seq_list : 120 198 ∀p : stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝ 121 199 λp,g,l.let 〈pre,post〉 ≝ split_on_last … (NOOP ??) l in 〈pre, (post : joint_step ??)〉. … … 176 254 ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝ 177 255 bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??). 256 *) 178 257 179 258 notation > "x ~❨ B , l ❩~> y 'in' c" with precedence 56 for … … 183 262 @{'block_in_code $c $x $B $l $y}. 184 263 264 notation > "x ~❨ B , l, r ❩~> y 'in' c" with precedence 56 for 265 @{'bind_block_in_code $c $x $B $l $r $y}. 266 267 notation < "hvbox(x ~❨ B , l, r ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for 268 @{'bind_block_in_code $c $x $B $l $r $y}. 269 185 270 definition step_in_code ≝ 186 271 λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_step p globals. … … 193 278 stmt_at … c src = Some ? (final … s). 194 279 195 let rec s eq_list_in_code p globals (c : codeT p globals)196 (src : code_point p) (B : list (joint_s eqp globals))280 let rec step_list_in_code p globals (c : codeT p globals) 281 (src : code_point p) (B : list (joint_step p globals)) 197 282 (l : list (code_point p)) (dst : code_point p) on B : Prop ≝ 198 283 match B with … … 206 291 [ nil ⇒ False 207 292 | cons mid rest ⇒ 208 step_in_code … c src hd mid ∧ s eq_list_in_code … c mid tl rest dst293 step_in_code … c src hd mid ∧ step_list_in_code … c mid tl rest dst 209 294 ] 210 295 ]. 211 296 212 interpretation "s eq list in code" 'block_in_code c x B l y = (seq_list_in_code ?? c x B l y).213 214 lemma s eq_list_in_code_append :297 interpretation "step list in code" 'block_in_code c x B l y = (step_list_in_code ?? c x B l y). 298 299 lemma step_list_in_code_append : 215 300 ∀p,globals.∀c : codeT p globals.∀src,B1,l1,mid,B2,l2,dst. 216 301 src ~❨B1,l1❩~> mid in c → mid ~❨B2,l2❩~> dst in c → … … 224 309 qed. 225 310 226 lemma s eq_list_in_code_append_inv :311 lemma step_list_in_code_append_inv : 227 312 ∀p,globals.∀c : codeT p globals.∀src,B1,B2,l,dst. 228 313 src ~❨B1@B2,l❩~> dst in c → 229 314 ∃l1,mid,l2.l = l1 @ l2 ∧ src ~❨B1,l1❩~> mid in c ∧ mid ~❨B2,l2❩~> dst in c. 230 #p #globals #c #src #B1 lapply src -src elim B1 315 #p #globals #c #src #B1 lapply src -src elim B1 -B1 231 316 [ #src #B2 #l #dst #H %{[ ]} %{src} %{l} %{H} % % 232 317 | #hd #tl #IH #src #B2 * [2: #mid #rest] #dst * #H1 #H2 … … 237 322 qed. 238 323 239 definition seq_block_step_in_code ≝ 240 λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_step p g).λl,dst. 241 ∃hd,tl.l = hd @ [tl] ∧ 242 src ~❨\fst B, l❩~> tl in c ∧ step_in_code … c tl (\snd B) dst. 243 244 definition seq_block_fin_step_in_code ≝ 245 λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit. 324 lemma append_not_empty_r : ∀X,l1,l2.not_empty X l2 → not_empty ? (l1 @ l2). 325 #X #l1 cases l1 -l1 [ #l2 #K @K | #hd #tl #l2 #_ % ] qed. 326 327 definition map_eval : ∀X,Y : Type[0].list (X → Y) → X → list Y ≝ λX,Y,l,x.map … (λf.f x) l. 328 329 definition step_block_in_code ≝ 330 λp,g.λc : codeT p g.λsrc.λb : step_block p g.λl,dst. 331 let 〈pref, last〉 ≝ split_on_last_ne … b in 332 ∃mid.src ~❨map_eval … pref mid, l❩~> mid in c ∧ step_in_code ?? c mid (last mid) dst. 333 334 lemma map_compose : ∀X,Y,Z,f,g.∀l : list X.map Y Z f (map X Y g l) = map … (f∘g) l. 335 #X #Y #Z #f #g #l elim l -l normalize // qed. 336 337 lemma map_ext_eq : ∀X,Y,f,g.∀l : list X.(∀x.f x = g x) → map X Y f l = map X Y g l. 338 #X #Y #f #g #l #H elim l -l normalize // qed. 339 340 lemma map_id : ∀X.∀l : list X.map X X (λx.x) l = l. 341 #X #l elim l -l normalize // qed. 342 343 lemma coerced_step_list_in_code : 344 ∀p : params.∀g,c,src.∀b : list (joint_step p g).∀l,dst. 345 step_block_in_code p g c src b l dst → 346 match b with 347 [ nil ⇒ step_in_code … c src (NOOP …) dst 348 | _ ⇒ step_list_in_code … c src b (l@[dst]) dst 349 ]. 350 #p #g #c #src @list_elim_left [2: #last #pref #_ ] #l #dst 351 [2: * #src' * cases l [2: #hd' #tl' *] whd in ⊢ (%→?); #EQ destruct #K @K ] 352 cases pref -pref [2: #hd #tl ] 353 whd in ⊢ (%→?); 354 [2: * #src' * cases l [2: #hd' #tl' *] whd in ⊢ (%→?); #EQ destruct #K %{K} % ] 355 whd in match (ensure_step_block ???); 356 <map_append 357 change with ((? :: ?) @ ?) in match (? :: ? @ ?); 358 >split_on_last_ne_def normalize nodelta * #mid * 359 whd in match (map_eval ????); 360 >map_compose >map_id #H1 #H2 361 @(step_list_in_code_append … H1) %{H2} % 362 qed. 363 364 definition fin_block_in_code ≝ 365 λp,g.λc:codeT p g.λsrc.λB : fin_block p g.λl.λdst : unit. 246 366 ∃hd,tl.l = hd @ [tl] ∧ 247 367 src ~❨\fst B, l❩~> tl in c ∧ fin_step_in_code … c tl (\snd B). 368 369 interpretation "step block in code" 'block_in_code c x B l y = (step_block_in_code ?? c x B l y). 370 interpretation "fin block in code" 'block_in_code c x B l y = (fin_block_in_code ?? c x B l y). 371 372 let rec bind_new_instantiates B X 373 (x : X) (b : bind_new B X) (l : list B) on b : Prop ≝ 374 match b with 375 [ bret B ⇒ 376 match l with 377 [ nil ⇒ x = B 378 | _ ⇒ False 379 ] 380 | bnew f ⇒ 381 match l with 382 [ nil ⇒ False 383 | cons r l' ⇒ 384 bind_new_instantiates B X x (f r) l' 385 ] 386 ]. 387 388 definition bind_step_block_in_code ≝ 389 λp,g.λc:codeT p g.λsrc.λB : bind_step_block p g.λlbls,regs.λdst. 390 ∃b.bind_new_instantiates … b B regs ∧ src ~❨b, lbls❩~> dst in c. 391 392 definition bind_fin_block_in_code ≝ 393 λp,g.λc:codeT p g.λsrc.λB : bind_fin_block p g.λlbls,regs.λdst. 394 ∃b.bind_new_instantiates … b B regs ∧ src ~❨b, lbls❩~> dst in c. 395 396 interpretation "bound step block in code" 'bind_block_in_code c x B l r y = (bind_step_block_in_code ?? c x B l r y). 397 interpretation "bound fin block in code" 'bind_block_in_code c x B l r y = (bind_fin_block_in_code ?? c x B l r y). 248 398 249 399 (* generates ambiguity even if it shouldn't -
src/joint/semantics.ma
r2592 r2595 197 197 198 198 (* Paolo: save_frame separated from call_setup to factorize tailcall code *) 199 ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars199 (* ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars *) 200 200 ; save_frame: call_kind → call_dest uns_pars → ident → state_pc st_pars → res (state st_pars) 201 201 (*CSC: setup_call returns a res only because we can call a function with the wrong number and … … 218 218 }. 219 219 220 (* 220 221 definition allocate_locals : 221 222 ∀p,F.∀sup : sem_unserialized_params p F. … … 223 224 λp,F,sup,l,st. 224 225 let r ≝ foldr … (allocate_locals_ … sup) (regs … st) l in 225 set_regs … r st. 226 set_regs … r st. *) 226 227 227 228 definition helper_def_retrieve : … … 526 527 527 528 definition eval_internal_call ≝ 528 λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args,st. 529 λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args. 530 λst : state p. 529 531 ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ; 530 ! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ; 531 return allocate_locals … p (joint_if_locals … fn) st'. 532 setup_call … stack_size (joint_if_params … globals fn) args st. 532 533 533 534 definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ]. -
src/joint/semantics_blocks.ma
r2529 r2595 2 2 include "joint/Traces.ma". 3 3 include "joint/semanticsUtils.ma". 4 5 include "common/StatusSimulation.ma". (* for trace_any_any_free *) 4 6 5 7 (* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝ … … 13 15 m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id curr_fn). 14 16 15 definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ]. 17 definition taaf_cons : ∀S : abstract_status.∀s1,s2,s3. 18 as_execute S s1 s2 → 19 as_classifier … s1 cl_other → 20 ∀taaf : trace_any_any_free S s2 s3. 21 (if taaf_non_empty … taaf then ¬as_costed … s2 else True) → 22 trace_any_any_free S s1 s3 ≝ 23 λS,s1,s2,s3,H,I,tl. 24 match tl return λs2,s3,tl. 25 as_execute … s1 s2 → 26 if taaf_non_empty … tl then ¬as_costed … s2 else True → 27 trace_any_any_free S s1 s3 28 with 29 [ taaf_base s2 ⇒ λH.λ_.taaf_step … (taa_base …) H I 30 | taaf_step s2 s3 s4 taa H' I' ⇒ 31 λH,J.taaf_step … (taa_step … H I J taa) H' I' 32 | taaf_step_jump s2 s3 s4 taa H' I' K' ⇒ 33 λH,J.taaf_step_jump … (taa_step ???? H I J taa) H' I' K' 34 ] H. 16 35 17 let rec produce_trace_any_any 36 lemma taaf_cons_non_empty : ∀S,s1,s2,s3,H,I,tl,J. 37 bool_to_Prop (taaf_non_empty … (taaf_cons S s1 s2 s3 H I tl J)). 38 #S #s1 #s2 #s3 #H #I #tl lapply H -H cases tl 39 [ #s #H * % |*: #s2 #s3 #s4 #taa #H' #I' [2: #K'] #H #J % ] 40 qed. 41 42 let rec produce_trace_any_any_free_aux 18 43 (p : evaluation_params) 19 44 (st : state_pc p) … … 26 51 return 〈curr_id, curr_fn〉 → 27 52 let src ≝ point_of_pc p (pc … st) in 28 if list_not_empty ? b then 29 ! x ← stmt_at ?? (joint_if_code … curr_fn) dst ; cost_label_of_stmt … x = None ? 30 else 31 True → 53 (* disambiguation: select 3rd (step list in code) *) 32 54 src ~❨b, l❩~> dst in joint_if_code … curr_fn → 33 All ? ( λx.And (no_call … x) (no_cost_label … x)) b →55 All ? (no_cost_label …) b → 34 56 repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' → 35 trace_any_any (joint_abstract_status p) st 36 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) ≝ match b 37 return λb.∀l,dst.?→?→?→?→?→?→? 57 Σtaaf : trace_any_any_free (joint_abstract_status p) st 58 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)). 59 (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝ 60 match b 61 return λb.∀l,dst.?→?→?→?→?→ Σtaaf.(not_empty ? b ↔ bool_to_Prop (taaf_non_empty … taaf)) 38 62 with 39 63 [ nil ⇒ 40 λl,dst,st',fd_prf, dst_prf,in_code,all_other,EQ1.41 (taa_base (joint_abstract_status p) st)42 ⌈trace_any_any ??? ↦ ?⌉64 λl,dst,st',fd_prf,in_code,all_other,EQ1. 65 «taaf_base (joint_abstract_status p) st 66 ⌈trace_any_any_free ??? ↦ ?⌉,?» 43 67 | cons hd tl ⇒ 44 68 λl. 45 match l return λx.∀dst,st'.?→?→?→?→ ?→?with46 [ nil ⇒ λdst,st',fd_prf, dst_prf,in_code.⊥69 match l return λx.∀dst,st'.?→?→?→?→Σtaaf.(True ↔ bool_to_Prop (taaf_non_empty … taaf)) with 70 [ nil ⇒ λdst,st',fd_prf,in_code.⊥ 47 71 | cons mid rest ⇒ 48 λdst,st',fd_prf, dst_prf,in_code,all_other,EQ1.72 λdst,st',fd_prf,in_code,all_other,EQ1. 49 73 let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in 50 74 match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st 51 75 return λx.eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st = x → 52 trace_any_any (joint_abstract_status p) st 53 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) with 54 [ Value st_mid ⇒ λEQ2. 55 let tr_tl ≝ produce_trace_any_any ? 56 (mk_state_pc ? st_mid mid_pc) 57 curr_id curr_fn tl rest dst ?????? in 58 taa_step … tr_tl 76 Σtaaf : trace_any_any_free (joint_abstract_status p) st 77 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)). 78 (True ↔ bool_to_Prop (taaf_non_empty … taaf)) with 79 [ OK st_mid ⇒ λEQ2. 80 let tr_tl ≝ produce_trace_any_any_free_aux ? 81 (mk_state_pc ? st_mid mid_pc (last_pop … st)) 82 curr_id curr_fn tl rest dst ????? in 83 «taaf_cons … tr_tl ?,?» 59 84 | _ ⇒ λEQ2.⊥ 60 85 ] (refl …) 61 86 ] 62 ]. 63 [ whd in EQ1 : (??%%); 64 cases l in in_code; whd in ⊢ (%→?); [2: #hd #tl * ] #EQ destruct 65 >pc_of_point_of_pc cases st // 87 ]. @hide_prf 88 [1,2: [2: % [*] generalize in ⊢ (?(???? (match % with [ _ ⇒ ?])) → ?); ] 89 whd in EQ1 : (??%%); 90 cases l in in_code; whd in ⊢ (%→?); [2,4: #hd #tl * ] #EQ destruct 91 >pc_of_point_of_pc cases st // #a #b #c #e >(K ?? e) normalize nodelta * 66 92 | @in_code 67 |3,12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1) 93 |12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1) 94 |4: cases tr_tl -tr_tl #tr_tl cases tl in in_code all_other; 95 [ #_ #_ * #_ cases (taaf_non_empty ????) 96 [ #ABS cases (ABS I) | #_ % ] 97 | #hd' #tl' ** #nxt * #EQstmt_at #EQ_nxt cases rest [*] #mid' #rest' * 98 * #nxt' * #EQstmt_at' #EQ_nxt' #_ * #hd_other * #hd_other' 99 #_ * #H #_ >(H I) % whd in ⊢ (%→?); 100 whd in ⊢ (?(??%?)→?); whd in match (as_pc_of ??); 101 >fetch_statement_eq [2: whd in match point_of_pc; 102 normalize nodelta >point_of_offset_of_point @EQstmt_at' |3: @fd_prf |*:] 103 normalize nodelta 104 >(no_label_uncosted … hd_other') * #ABS @ABS % 105 ] 106 |7: % [2: #_ %] * @taaf_cons_non_empty 68 107 ] 69 108 change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1; 70 109 >EQ2 in EQ1; >m_return_bind 71 110 cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code 72 cases all_other -all_other * #hd_no_call#hd_no_cost #tl_other111 cases all_other -all_other #hd_no_cost #tl_other 73 112 #EQ1 74 113 try assumption 75 [ whd whd in match eval_state; normalize nodelta114 [2: whd whd in match eval_state; normalize nodelta 76 115 >(fetch_statement_eq … fd_prf EQ_stmt_at) 77 116 >m_return_bind … … 79 118 >EQ2 >m_return_bind 80 119 whd in match eval_statement_advance; normalize nodelta 81 >(no_call_advance … hd_no_call)82 120 whd in match next; normalize nodelta 83 121 whd in match succ_pc; normalize nodelta 84 122 >EQ_mid % 85 | whd whd in ⊢ (??%?); 86 >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta 87 @(no_call_other … hd_no_call) 88 | whd in ⊢ (?%); 89 whd in match as_label; normalize nodelta 90 %* #H @H -H whd in ⊢ (??%?); 91 whd in match (as_pc_of ??); 92 inversion (fetch_statement ????) normalize nodelta 93 [2: // ] 94 ** #i' #f' #stmt' #EQ 95 elim (fetch_statement_inv … EQ) 96 >fd_prf 97 whd in ⊢ (??%?→?); #EQ destruct(EQ) 98 whd in ⊢ (%→?); 99 whd in match (point_of_pc ??); >point_of_offset_of_point 100 #EQ' 101 cases tl in tl_other rest_in_code; 102 [ * cases rest [2: #hd' #tl' * ] whd in ⊢ (%→?); #EQ destruct(EQ) 103 >EQ' in dst_prf; >m_return_bind #H @H 104 | #hd' #tl' ** #_ #hd_no_cost' #_ 105 cases rest [ * ] #mid' #rest' * * #nxt' * #EQ_stmt_at' #EQ_mid' #_ 106 >EQ_stmt_at' in EQ'; #EQ' destruct(EQ') 107 @(no_label_uncosted … hd_no_cost') 108 ] 109 | >dst_prf cases (list_not_empty ??) % 110 | normalize nodelta >point_of_pc_of_point assumption 123 |1: whd whd in ⊢ (??%?); 124 >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta % 125 |3: normalize nodelta >point_of_pc_of_point assumption 111 126 ] 112 127 qed. 128 129 definition produce_trace_any_any_free : 130 ∀p : evaluation_params. 131 ∀st : state_pc p. 132 ∀curr_id,curr_fn. 133 ∀b : list (joint_seq p (globals p)). 134 ∀l : list (code_point p). 135 ∀dst : code_point p. 136 ∀st' : state p. 137 fetch_internal_function … (ev_genv p) (pc_block (pc … st)) = 138 return 〈curr_id, curr_fn〉 → 139 let src ≝ point_of_pc p (pc … st) in 140 (* disambiguation: select 3rd (step list in code) *) 141 src ~❨b, l❩~> dst in joint_if_code … curr_fn → 142 All ? (no_cost_label …) b → 143 repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' → 144 trace_any_any_free (joint_abstract_status p) st 145 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝ 146 λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3,prf4. 147 produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3 prf4.
Note: See TracChangeset
for help on using the changeset viewer.