Changeset 2817


Ignore:
Timestamp:
Mar 7, 2013, 10:31:19 PM (6 years ago)
Author:
sacerdot
Message:

Repaired after Paolo's commit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r2760 r2817  
    1212
    1313definition repeat_eval_seq_no_pc ≝
    14   λp : evaluation_params.λcurr_id,curr_fn.
    15   m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id curr_fn).
     14  λp : evaluation_params.λcurr_id.
     15  m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id).
    1616
    1717definition taaf_cons : ∀S : abstract_status.∀s1,s2,s3.
     
    5151  let src ≝ point_of_pc p (pc … st) in
    5252  step_in_code … (joint_if_code … curr_fn) src s dst →
    53   eval_seq_no_pc p (globals p) (ev_genv p) curr_id curr_fn s st = return st' →
     53  eval_seq_no_pc p (globals p) (ev_genv p) curr_id s st = return st' →
    5454  as_execute (joint_abstract_status p) st
    5555    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ∧
     
    7878  let src ≝ point_of_pc p (pc … st) in
    7979  seq_list_in_code … (joint_if_code … curr_fn) src b l dst →
    80   repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     80  repeat_eval_seq_no_pc p curr_id b st = return st' →
    8181  Σtaaf : trace_any_any_free (joint_abstract_status p) st
    8282    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
     
    9797      λst',fd_prf,in_code,EQ1.
    9898      let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
    99       match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st
    100       return λx.eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st = x →
     99      match eval_seq_no_pc … (ev_genv p) curr_id hd st
     100      return λx.eval_seq_no_pc … (ev_genv p) curr_id hd st = x →
    101101      Σtaaf : trace_any_any_free (joint_abstract_status p) st
    102102        (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
     
    131131|7: % [2: #_ %] #_ @taaf_cons_non_empty
    132132]
    133 change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
     133change with (! y ← ? ; repeat_eval_seq_no_pc ???? = ?) in EQ1;
    134134>EQ2 in EQ1; >m_return_bind
    135135cases in_code -in_code #mid' * #rest' ** #EQ1 #step_in cases (step_in)
     
    165165  let src ≝ point_of_pc p (pc … st) in
    166166  seq_list_in_code … (joint_if_code … curr_fn) src b l dst →
    167   repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     167  repeat_eval_seq_no_pc p curr_id b st = return st' →
    168168  trace_any_any_free (joint_abstract_status p) st
    169169    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝
     
    184184  let src ≝ point_of_pc p (pc … st) in
    185185  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
    186   repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     186  repeat_eval_seq_no_pc p curr_id b st = return st' →
    187187  trace_any_any_free (joint_abstract_status p) st
    188188    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝
Note: See TracChangeset for help on using the changeset viewer.