Ignore:
Timestamp:
Jul 1, 2015, 11:45:08 PM (4 years ago)
Author:
piccolo
Message:

baco

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable_stack_pass.ma

    r3577 r3578  
    203203qed.
    204204
    205 (*
    206 let rec create_silent_trace_from_eval_combinators (st : (l : list guard_combinators)
    207 (prf: m_fold Option … eval_combinators l st = return st')
    208 *)
     205definition safe_cast : ∀A,B : Type[0].A = B → A → B ≝
     206λA,B,prf.match prf with [refl ⇒ λx : A.x].
     207
     208let rec create_silent_trace_from_eval_combinators (prog : Program stack_env_params stack_instr_params flat_labels)
     209(bound : ℕ) (st,st' : state stack_state_params) (l : list guard_combinators) 
     210on l :
     211 m_fold Option … eval_combinators l (store … st) = return (store … st') →
     212  code … st = list_combinators_to_instructions l (code … st') →
     213  cont … st = cont … st' → io_info … st = io_info … st' →
     214  raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st' ≝
     215match l return λx.(m_fold Option … eval_combinators x ? = ? → ? = list_combinators_to_instructions x ? → ?) with
     216[ nil ⇒ λprf1,prf2,prf3,prf4.safe_cast (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st)
     217     (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st') ? (t_base ?? st)
     218| cons x xs ⇒ λprf1,prf2,prf3,prf4.
     219   let next_store ≝ (opt_safe … (eval_combinators x (store … st)) ?) in
     220   let next_st ≝ mk_state stack_state_params (list_combinators_to_instructions xs (code … st')) (cont … st')
     221                   next_store (io_info … st') in
     222   let tail ≝ create_silent_trace_from_eval_combinators prog bound next_st st' xs ? (refl …) (refl …) (refl …) in
     223   t_ind … (cost_act … (None ?)) … tail
     224].
     225@hide_prf
     226[ cases st in prf1 prf2 prf3 prf4; cases st' #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 whd in H9 : (??%%);
     227  whd in H10 : (??%%); destruct %
     228|4: change with (m_bind ?????) in prf1 :(??%?); cases(bind_inversion ????? prf1) -prf1 #w * #EQw #_ >EQw %
     229   whd in ⊢ (??%% → ?); #EQ destruct
     230| whd @seq_sil
     231  [4: >prf2 in ⊢ (??%?); %
     232  |8: %
     233  |5: change with (eval_combinators ??) in ⊢ (??%?); normalize nodelta @opt_safe_elim #w #H assumption
     234  |6: %
     235  |7: assumption
     236  |9,10: cases daemon (*io*)
     237  |*:
     238  ]
     239| normalize nodelta @opt_safe_elim #w #EQw change with (m_bind ?????) in prf1 :(??%?); >EQw in prf1;
     240  >m_return_bind //
     241]
     242qed.
     243
     244lemma create_silent_trace_from_eval_combinators_ok : ∀prog,bound,st,st',l,prf1,prf2,prf3,prf4,t.
     245create_silent_trace_from_eval_combinators prog bound st st' l prf1 prf2 prf3 prf4 = t →
     246pre_silent_trace … t.
     247#prog #bound #st #st' #l lapply st -st lapply st' -st' elim l
     248[ * #code' #cont' #store' #io' * #code #cont #store #io whd in ⊢ (??%% → ??%% → ?); #EQ destruct #EQ1 #EQ2 #EQ3 destruct
     249  #t whd in ⊢ (??%% → ?); #EQ destruct % cases daemon (*io*)
     250| #x #xs #IH #st' #st #H cases(bind_inversion ????? H) #w * #EQw #EQstore_st'
     251  whd in ⊢ (???% → ?); change with (list_combinators_to_instructions ??) in match (foldr ?????);
     252  #prf2 #EQcont #EQio #t whd in ⊢ (??%? → ?); #EQ destruct %2 [cases daemon (* io *)] @IH [|*: %]
     253]
     254qed.
     255
     256(*  [ @opt_safe_elim #w' >EQw whd in ⊢ (??%% → ?); #EQ destruct assumption
     257  | %
     258  | % c'e' un baco????*)
    209259
    210260definition simulation_imp_frame :
Note: See TracChangeset for help on using the changeset viewer.