Changeset 3057


Ignore:
Timestamp:
Apr 1, 2013, 9:14:03 PM (4 years ago)
Author:
tranquil
Message:

lookup of function identifiers was not corrected with sigma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r3039 r3057  
    664664    let labels ≝ \fst (create_label_cost_map instr_list) in
    665665    let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    666     let lookup_datalabels ≝ λx. lookup_def … (construct_datalabels preamble) x (lookup_labels x) in
     666    let lookup_datalabels ≝ λx. lookup_def … (construct_datalabels preamble) x (sigma (lookup_labels x)) in
    667667    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
    668668    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
     
    837837       let datalabels ≝ construct_datalabels preamble in
    838838       let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
    839        let lookup_datalabels ≝ λx.lookup_def … datalabels x (lookup_labels x) in
     839       let lookup_datalabels ≝ λx.lookup_def … datalabels x (sigma (lookup_labels x)) in
    840840       ∀ppc. ∀ppc_ok:nat_of_bitvector … ppc < |instr_list|.
    841841         let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc ppc_ok in
     
    856856  let datalabels ≝ construct_datalabels preamble in
    857857  let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
    858   let lookup_datalabels ≝ λx.lookup_def … datalabels x (lookup_labels x) in
     858  let lookup_datalabels ≝ λx.lookup_def … datalabels x (sigma (lookup_labels x)) in
    859859  let 〈next_pc,revcode〉 ≝ pi1 … (
    860860     foldl_strong
Note: See TracChangeset for help on using the changeset viewer.