Changeset 2957


Ignore:
Timestamp:
Mar 26, 2013, 4:41:25 PM (4 years ago)
Author:
tranquil
Message:

fixed semantics_blocks

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r2883 r2957  
    1010
    1111definition repeat_eval_seq_no_pc ≝
    12   λp : evaluation_params.λcurr_id.
    13   m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id).
     12  λp.λpars : evaluation_params p.λcurr_id.
     13  m_fold … (eval_seq_no_pc … (ev_genv … pars) curr_id).
    1414
    1515lemma 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  ∀p,pars,curr_id,L1,L2,s.
     17  repeat_eval_seq_no_pc p pars curr_id (L1@L2) s =
     18  ! s' ← repeat_eval_seq_no_pc p pars curr_id L1 s;
     19  repeat_eval_seq_no_pc p pars curr_id L2 s' ≝
     20  λp,pars,curr_id.m_fold_append ….
    2121
    2222lemma produce_step_trace :
     
    2424  ∀st : state_pc p.
    2525  ∀curr_id,curr_fn.
    26   ∀s : joint_seq p (globals p).
     26  ∀s : joint_seq p (globals p).
    2727  ∀dst : code_point p.
    2828  ∀st' : state p.
    29   fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
     29  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
    3030    return 〈curr_id, curr_fn〉 →
    3131  let src ≝ point_of_pc p (pc … st) in
    3232  step_in_code … (joint_if_code … curr_fn) src s dst →
    33   eval_seq_no_pc p (globals p) (ev_genv p) curr_id s st = return st' →
     33  eval_seq_no_pc p (globals … p) (ev_genv … p) curr_id s st = return st' →
    3434  as_execute (joint_abstract_status p) st
    3535    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ∧
     
    5050  (st : state_pc p)
    5151  curr_id curr_fn
    52   (b : list (joint_seq p (globals p))) on b :
     52  (b : list (joint_seq p (globals p))) on b :
    5353  ∀l : list (code_point p).
    5454  ∀dst : code_point p.
    5555  ∀st' : state p.
    56   fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
     56  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
    5757    return 〈curr_id, curr_fn〉 →
    5858  let src ≝ point_of_pc p (pc … st) in
    5959  seq_list_in_code … (joint_if_code … curr_fn) src b l dst →
    60   repeat_eval_seq_no_pc p curr_id b st = return st' →
     60  repeat_eval_seq_no_pc p curr_id b st = return st' →
    6161  Σtaaf : trace_any_any_free (joint_abstract_status p) st
    6262    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
     
    7777      λst',fd_prf,in_code,EQ1.
    7878      let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
    79       match eval_seq_no_pc … (ev_genv p) curr_id hd st
    80       return λx.eval_seq_no_pc … (ev_genv p) curr_id hd st = x →
     79      match eval_seq_no_pc … (ev_genv p) curr_id hd st
     80      return λx.eval_seq_no_pc … (ev_genv p) curr_id hd st = x →
    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)).
     
    111111|7: % [2: #_ %] #_ @taaf_cons_non_empty
    112112]
    113 change with (! y ← ? ; repeat_eval_seq_no_pc ???? = ?) in EQ1;
     113change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
    114114>EQ2 in EQ1; >m_return_bind
    115115cases in_code -in_code #mid' * #rest' ** #EQ1 #step_in cases (step_in)
     
    137137  ∀st : state_pc p.
    138138  ∀curr_id,curr_fn.
    139   ∀b : list (joint_seq p (globals p)).
     139  ∀b : list (joint_seq p (globals p)).
    140140  ∀l : list (code_point p).
    141141  ∀dst : code_point p.
    142142  ∀st' : state p.
    143   fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
     143  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
    144144    return 〈curr_id, curr_fn〉 →
    145145  let src ≝ point_of_pc p (pc … st) in
    146146  seq_list_in_code … (joint_if_code … curr_fn) src b l dst →
    147   repeat_eval_seq_no_pc p curr_id b st = return st' →
     147  repeat_eval_seq_no_pc p curr_id b st = return st' →
    148148  Σtaaf :trace_any_any_free (joint_abstract_status p) st
    149149    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
     
    157157  ∀st : state_pc p.
    158158  ∀curr_id,curr_fn.
    159   ∀b : list (joint_seq p (globals p)).
     159  ∀b : list (joint_seq p (globals p)).
    160160  ∀l : list (code_point p).
    161161  ∀dst : code_point p.
    162162  ∀st' : state p.
    163   fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
     163  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
    164164    return 〈curr_id, curr_fn〉 →
    165165  let src ≝ point_of_pc p (pc … st) in
    166166  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
    167   repeat_eval_seq_no_pc p curr_id 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)) ≝
Note: See TracChangeset for help on using the changeset viewer.