Ignore:
Timestamp:
Feb 18, 2013, 5:48:19 PM (7 years ago)
Author:
tranquil
Message:
  • another change in block definition
  • RTLabs -> RTL and ERTL -> ERTLptr passes fixed, others stil broken
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r2655 r2674  
    5353  eval_seq_no_pc p (globals p) (ev_genv p) curr_id curr_fn s st = return st' →
    5454  as_execute (joint_abstract_status p) st
    55     (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
     55    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ∧
     56  as_classifier (joint_abstract_status p) st cl_other.
    5657#p #st#curr_id #curr_fn #s #dst #st' #EQfetch * #nxt * #EQstmt_at #EQdst
    57 #EQeval whd whd in match eval_state; whd in match eval_statement_no_pc;
     58#EQeval whd in ⊢ (?%%); whd in ⊢ (?(??%?)(??%?));
     59whd in match eval_statement_no_pc;
    5860whd in match fetch_statement; normalize nodelta >EQfetch >m_return_bind
    59 >EQstmt_at >m_return_bind normalize nodelta >EQeval >m_return_bind
    60 whd in ⊢ (??%%); @eq_f whd in match next; normalize nodelta
    61 whd in match (pc ??);  whd in match succ_pc; normalize nodelta >EQdst %
     61>m_return_bind >EQstmt_at >m_return_bind normalize nodelta
     62% [2: % ]
     63whd in ⊢ (??%?); normalize nodelta >EQeval whd in ⊢ (??%%);
     64@eq_f whd in ⊢ (??%?); @eq_f2 [2: %]
     65whd in match succ_pc; normalize nodelta @eq_f @EQdst
    6266qed.
    6367
     
    7377    return 〈curr_id, curr_fn〉 →
    7478  let src ≝ point_of_pc p (pc … st) in
    75   step_list_in_code … (joint_if_code … curr_fn) src b l dst →
     79  seq_list_in_code … (joint_if_code … curr_fn) src b l dst →
    7680  All ? (no_cost_label …) b →
    7781  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     
    9094    match l return λx.∀dst,st'.?→?→?→?→Σtaaf.(True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
    9195    [ nil ⇒ λdst,st',fd_prf,in_code.⊥
    92     | cons mid rest ⇒
    93       λdst,st',fd_prf,in_code,all_other,EQ1.
     96    | cons _ rest ⇒ λdst.
     97      let mid ≝ match rest with [ nil ⇒ dst | cons mid _ ⇒ mid ] in
     98      λst',fd_prf,in_code,all_other,EQ1.
    9499      let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
    95100      match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st
     
    106111      ] (refl …)
    107112    ]
    108   ]. @hide_prf
     113  ].
     114@hide_prf
    109115[1,2: [2: % [*] generalize in ⊢ (?(???? (match % with [ _ ⇒ ?])) → ?); ]
    110116  whd in EQ1 : (??%%);
    111   cases l in in_code; whd in ⊢ (%→?); [2,4: #hd #tl * ] #EQ destruct
     117  cases l in in_code; whd in ⊢ (%→?); [2,4: #hd #tl * #ABS destruct ] * #_ #EQ destruct
    112118  >pc_of_point_of_pc cases st // #a #b #c #e >(K ?? e) normalize nodelta *
    113 | @in_code
     119| cases in_code #a * #b ** #ABS destruct
    114120|12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
    115 |4: cases tr_tl -tr_tl #tr_tl cases tl in in_code all_other;
    116   [ #_ #_ * #_ cases (taaf_non_empty ????)
    117     [ #ABS cases (ABS I) | #_ % ]
    118   | #hd' #tl' ** #nxt * #EQstmt_at #EQ_nxt cases rest [*] #mid' #rest' *
    119     * #nxt' * #EQstmt_at' #EQ_nxt' #_ * #hd_other * #hd_other'
    120     #_ * #H #_ >(H I) % whd in ⊢ (%→?);
    121     whd in ⊢ (?(??%?)→?); whd in match (as_pc_of ??);
    122     >fetch_statement_eq [2: whd in match point_of_pc;
    123     normalize nodelta >point_of_offset_of_point @EQstmt_at' |3: @fd_prf |*:]
    124     normalize nodelta
    125     >(no_label_uncosted … hd_other') * #ABS @ABS %
    126   ]
    127 |7: % [2: #_ %] * @taaf_cons_non_empty
     121|4: cases tr_tl -tr_tl #tr_tl * #_ #H
     122  @if_elim [2: #_ % ] #G lapply (H G) -H -G
     123 cases tl in in_code all_other; [ #_ #_ * ]
     124 #hd' #tl' * #mid' * #rest' ** #EQ * #nxt * #EQstmt_at #EQ_nxt
     125 * #mid'' * #rest'' ** #EQ' * #nxt' * #EQstmt_at' #EQnxt' #_
     126 normalize nodelta -mid_pc destruct
     127 * #_ * #H #_ #_ % whd in ⊢ (%→?);
     128 whd in ⊢ (?(??%?)→?); whd in match (as_pc_of ??);
     129  >fetch_statement_eq [2: whd in match point_of_pc;
     130  normalize nodelta >point_of_offset_of_point @EQstmt_at' |3: @fd_prf |*:]
     131  normalize nodelta
     132  >(no_label_uncosted … H) * #ABS @ABS %
     133|7: % [2: #_ %] #_ @taaf_cons_non_empty
    128134]
    129135change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
    130136>EQ2 in EQ1; >m_return_bind
    131 cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code
     137cases in_code -in_code #mid' * #rest' ** #EQ1 #step_in cases (step_in)
     138#nxt * #EQ_stmt_at #EQ_mid' #rest_in_code
     139normalize nodelta
    132140cases all_other -all_other #hd_no_cost #tl_other
    133 #EQ1
     141#EQ3 destruct skip (mid_pc)
    134142try assumption
    135 [2: whd whd in match eval_state; normalize nodelta
    136   >(fetch_statement_eq … fd_prf EQ_stmt_at)
    137   >m_return_bind
    138   whd in match eval_statement_no_pc; normalize nodelta
    139   >EQ2 >m_return_bind
    140   whd in match eval_statement_advance; normalize nodelta
    141   whd in match next; normalize nodelta
    142   whd in match succ_pc; normalize nodelta
    143   >EQ_mid %
    144 |1: whd whd in ⊢ (??%?);
     143[ whd whd in ⊢ (??%?);
    145144  >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta %
    146 |3: normalize nodelta >point_of_pc_of_point assumption
     145|*:
     146  cases tl in rest_in_code;
     147  [1,3: * #EQ4 #EQ5 destruct normalize nodelta
     148  |*: #hd' #tl' * #mid'' * #rest'' ** #EQ4 #step_in' #rest_in_code'
     149    destruct normalize nodelta
     150  ]
     151  [1,3: @(proj1 … (produce_step_trace … fd_prf … EQ2)) assumption
     152  |2: %[%] @point_of_pc_of_point
     153  |4: >point_of_pc_of_point %[| %[| %{rest_in_code'} %{step_in'} %]]
     154  ]
    147155]
    148156qed.
     
    159167    return 〈curr_id, curr_fn〉 →
    160168  let src ≝ point_of_pc p (pc … st) in
    161   step_list_in_code … (joint_if_code … curr_fn) src b l dst →
     169  seq_list_in_code … (joint_if_code … curr_fn) src b l dst →
    162170  All ? (no_cost_label …) b →
    163171  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     
    166174  λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3,prf4.
    167175  produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3 prf4.
     176
     177(* when a seq_list is coerced to a step_block *)
     178definition produce_trace_any_any_free_coerced :
     179  ∀p : evaluation_params.
     180  ∀st : state_pc p.
     181  ∀curr_id,curr_fn.
     182  ∀b : list (joint_seq p (globals p)).
     183  ∀l : list (code_point p).
     184  ∀dst : code_point p.
     185  ∀st' : state p.
     186  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
     187    return 〈curr_id, curr_fn〉 →
     188  let src ≝ point_of_pc p (pc … st) in
     189  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
     190  All ? (no_cost_label …) b →
     191  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     192  trace_any_any_free (joint_abstract_status p) st
     193    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝
     194  λp,st,curr_id,curr_fn,b.?.
     195#l #dst #st' #fd_prf #prf
     196lapply (coerced_step_list_in_code … prf)
     197inversion b normalize nodelta
     198[ #_ #in_code #_ whd in ⊢ (??%%→?); #EQ destruct
     199  cases (produce_step_trace … fd_prf … in_code (refl …))
     200  #H #G
     201  %2{(taa_base …)} assumption
     202| #hd #tl #_ #EQ <EQ -hd -tl @produce_trace_any_any_free assumption
     203]
     204qed.
Note: See TracChangeset for help on using the changeset viewer.