Changeset 2879


Ignore:
Timestamp:
Mar 15, 2013, 12:16:30 PM (4 years ago)
Author:
tranquil
Message:

changed coercion from list of joint_seq to blocks to a more efficient one

Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/blocks.ma

    r2674 r2879  
    134134list (joint_seq p globals) → step_block p globals ≝
    135135λp,g,l.
    136 match split_on_last … l return λ_.step_block ?? with
    137 [ None ⇒ 〈[ ], λ_.NOOP ??, [ ]〉
    138 | Some pr ⇒ 〈add_dummy_variance … (\fst pr), λ_.\snd pr, [ ]
     136match l return λ_.step_block ?? with
     137[ nil ⇒ 〈[ ], λ_.NOOP ??, [ ]〉
     138| cons hd tl ⇒ 〈[ ], λ_.hd, tl
    139139].
    140140
     
    337337| _ ⇒ seq_list_in_code … c src b l dst
    338338].
    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
     342destruct
     343[ % [| % [| %{tl_in} %{stp_in_code} % ]]
     344| @stp_in_code
     345]
    351346qed.
    352347
     
    366361    ]
    367362  ].
     363
     364lemma bind_new_instantiates_bind_inv : ∀B,X,Y,y.
     365  ∀b : bind_new B X.∀f : X → bind_new B Y.∀l.
     366bind_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]
     375qed.
     376
     377lemma bind_new_instantiates_bind : ∀B,X,Y,x,y.
     378  ∀b : bind_new B X.∀f : X → bind_new B Y.∀l1,l2.
     379bind_new_instantiates B X x b l1 →
     380bind_new_instantiates B Y y (f x) l2 →
     381bind_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]
     386qed.
    368387
    369388definition bind_step_block_in_code ≝
  • src/joint/semantics_blocks.ma

    r2869 r2879  
    22include "joint/Traces.ma".
    33include "joint/semanticsUtils.ma".
    4 
    5 include "common/StatusSimulation.ma". (* for trace_any_any_free *)
    64
    75(* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
     
    1412  λp : evaluation_params.λcurr_id.
    1513  m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id).
     14
     15lemma 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 ….
    1621
    1722lemma produce_step_trace :
Note: See TracChangeset for help on using the changeset viewer.