Changeset 1946 for src/ASM/Assembly.ma


Ignore:
Timestamp:
May 15, 2012, 12:01:30 AM (9 years ago)
Author:
sacerdot
Message:

\snd half_add => add everywhere

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1943 r1946  
    818818  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    819819   let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels  pi) in
    820     sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
     820    sigma program pol (add ? ppc (bitvector_of_nat ? 1)) =
    821821     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    822822 #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl #Hppc
     
    824824 cases (sigma00 ???) #x #Hpmap #EQ
    825825 whd in match (sigma ???);
    826  whd in match (sigma program pol (\snd (half_add ???)));
     826 whd in match (sigma program pol (add ???));
    827827 whd in match sigma_safe; normalize nodelta
    828828 (*Problem1: backtracking cases (sigma0 program pol)*)
     
    834834 | #_ lapply (proj1 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) #Hpmap1
    835835   lapply ((proj2 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) (nat_of_bitvector 16 ppc) Hppc) #Hpmap2 -Hpmap
    836    <(bitvector_of_nat_nat_of_bitvector 16 ppc) >half_add_SO
     836   <(bitvector_of_nat_nat_of_bitvector 16 ppc) >add_SO
    837837   
    838838   >(Hpmap2 ? (refl …)) @eq_f @eq_f2 [%]
     
    946946   res = assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
    947947   let 〈len,code〉 ≝ res in
    948     sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
     948    sigma program pol (add ? ppc (bitvector_of_nat ? 1)) =
    949949     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
    950950≝ λprogram: pseudo_assembly_program.
     
    12701270        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels (\snd hd) in
    12711271        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
    1272         let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
     1272        let new_ppc ≝ add ? ppc (bitvector_of_nat ? 1) in
    12731273         〈new_pc, 〈new_ppc, (code @ program)〉〉)
    12741274      〈(zero ?), 〈(zero ?), [ ]〉〉
Note: See TracChangeset for help on using the changeset viewer.