Changeset 2879
 Timestamp:
 Mar 15, 2013, 12:16:30 PM (5 years ago)
 Location:
 src/joint
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/blocks.ma
r2674 r2879 134 134 list (joint_seq p globals) → step_block p globals ≝ 135 135 λp,g,l. 136 match split_on_last …l return λ_.step_block ?? with137 [ None⇒ 〈[ ], λ_.NOOP ??, [ ]〉138  Some pr ⇒ 〈add_dummy_variance … (\fst pr), λ_.\snd pr, [ ]〉136 match l return λ_.step_block ?? with 137 [ nil ⇒ 〈[ ], λ_.NOOP ??, [ ]〉 138  cons hd tl ⇒ 〈[ ], λ_.hd, tl〉 139 139 ]. 140 140 … … 337 337  _ ⇒ seq_list_in_code … c src b l dst 338 338 ]. 339 #p #g #c #src @list_elim_left [2: #last #pref #_ ] #l #dst 340 [2: * #pref * #mid1 * #mid2 * #post *** #EQ * #EQ' #EQ'' 341 #H * #EQ''' #EQ'''' destruct @H ] 342 whd in ⊢ (?????%??→?); >split_on_last_hit normalize nodelta 343 *#l1*#mid1*#mid2*#l2*** #EQ1 344 whd in match map_eval; whd in match add_dummy_variance; normalize nodelta 345 >map_compose >map_id #pref_in_code #last_in_code * #EQ2 #EQ3 destruct 346 cut (∃hd,tl.pref@[last] = hd::tl) 347 [ cases pref [ %{last} %{[ ]} %  #hd #tl %{hd} %{(tl@[last])} % ]] * #hd * #tl 348 #EQ >EQ in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?]); normalize nodelta hd tl 349 @(seq_list_in_code_append … pref_in_code) 350 %[ %[ % [2: %%] %{last_in_code} % ]] 339 #p #g #c #src * [2: #hd #tl] 340 #l #dst * #pref * #mid1 * #mid2 * #post *** #EQ * #EQ' #EQ'' 341 #stp_in_code [ #tl_in  * #EQ''' #EQ''''] whd 342 destruct 343 [ % [ % [ %{tl_in} %{stp_in_code} % ]] 344  @stp_in_code 345 ] 351 346 qed. 352 347 … … 366 361 ] 367 362 ]. 363 364 lemma bind_new_instantiates_bind_inv : ∀B,X,Y,y. 365 ∀b : bind_new B X.∀f : X → bind_new B Y.∀l. 366 bind_new_instantiates B Y y (!y ← b; f y) l → 367 ∃x,l1,l2.l = l1@l2 ∧ bind_new_instantiates B X x b l1 ∧ 368 bind_new_instantiates B Y y (f x) l2. 369 #B #X #Y #y #b elim b b 370 [ #x #f #l >m_return_bind #H %{x} %{[ ]} %{l} %{H} %% 371  #g #IH #f * [ * ] #hd #tl whd in ⊢ (%→?); #H 372 cases (IH … H) #x * #l1 * #l2 ** #EQ #H1 #H2 %{x} %{(hd::l1)} %{l2} 373 %{H2} %{H1} >EQ % 374 ] 375 qed. 376 377 lemma bind_new_instantiates_bind : ∀B,X,Y,x,y. 378 ∀b : bind_new B X.∀f : X → bind_new B Y.∀l1,l2. 379 bind_new_instantiates B X x b l1 → 380 bind_new_instantiates B Y y (f x) l2 → 381 bind_new_instantiates B Y y (!y ← b; f y) (l1@l2). 382 #B #X #Y #x #y #b elim b b 383 [ #x' #f * [2: #hd #tl ] #l2 * #H @H 384  #g #IH #f * [ #l2 * ] #hd #tl #l2 #H1 #H2 whd @IH assumption 385 ] 386 qed. 368 387 369 388 definition bind_step_block_in_code ≝ 
src/joint/semantics_blocks.ma
r2869 r2879 2 2 include "joint/Traces.ma". 3 3 include "joint/semanticsUtils.ma". 4 5 include "common/StatusSimulation.ma". (* for trace_any_any_free *)6 4 7 5 (* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝ … … 14 12 λp : evaluation_params.λcurr_id. 15 13 m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id). 14 15 lemma repeat_eval_seq_no_pc_append : 16 ∀p,curr_id,L1,L2,s. 17 repeat_eval_seq_no_pc p curr_id (L1@L2) s = 18 ! s' ← repeat_eval_seq_no_pc p curr_id L1 s; 19 repeat_eval_seq_no_pc p curr_id L2 s' ≝ 20 λp,curr_id.m_fold_append …. 16 21 17 22 lemma produce_step_trace :
Note: See TracChangeset
for help on using the changeset viewer.