Changeset 2599 for src/joint


Ignore:
Timestamp:
Jan 31, 2013, 5:15:49 PM (8 years ago)
Author:
tranquil
Message:
  • map_opt and map on positive maps are now clean (erase empty subtrees)
  • minor changes to blocks
Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/blocks.ma

    r2595 r2599  
    296296
    297297interpretation "step list in code" 'block_in_code c x B l y = (step_list_in_code ?? c x B l y).
     298
     299lemma step_list_in_code_ne : ∀p,globals.∀c : codeT p globals.∀src,B,l,dst.
     300  not_empty ? B →
     301  src ~❨B,l❩~> dst in c →
     302  ∃prf : not_empty … l.
     303  \snd (split_on_last_ne … «l, prf») = dst.
     304#p #globals #c #src #b lapply src -src elim b -b [ #src #l #dst * ]
     305#hd * [2: #hd' #tl ] #IH #src * [1,3: #dst #_ * ]
     306#mid * [ #dst #_ * #_ * |4: #mid' #tl #dst #_ * #_ * ]
     307[2: #dst * * #_ whd in ⊢ (%→?); #EQ destruct %{I} % ]
     308#mid' #rest #dst * * #H1 #H2 %{I}
     309cases (IH … I H2) * #EQ <EQ
     310whd in match (split_on_last_ne ??);
     311whd in match split_on_last_ne; normalize nodelta
     312@pair_elim #a #b #_ %
     313qed.
    298314
    299315lemma step_list_in_code_append :
  • src/joint/semantics_blocks.ma

    r2595 r2599  
    5151    return 〈curr_id, curr_fn〉 →
    5252  let src ≝ point_of_pc p (pc … st) in
    53   (* disambiguation: select 3rd (step list in code) *)
    54   src ~❨b, l❩~> dst in joint_if_code … curr_fn →
     53  step_list_in_code … (joint_if_code … curr_fn) src b l dst →
    5554  All ? (no_cost_label …) b →
    5655  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     
    138137    return 〈curr_id, curr_fn〉 →
    139138  let src ≝ point_of_pc p (pc … st) in
    140   (* disambiguation: select 3rd (step list in code) *)
    141   src ~❨b, l❩~> dst in joint_if_code … curr_fn →
     139  step_list_in_code … (joint_if_code … curr_fn) src b l dst →
    142140  All ? (no_cost_label …) b →
    143141  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
Note: See TracChangeset for help on using the changeset viewer.