Changeset 2047 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jun 12, 2012, 2:18:16 PM (7 years ago)
Author:
mulligan
Message:

Big bugs in policy calculations found. Waiting for Jaap's commit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r2040 r2047  
    990990        match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
    991991        [ ADDR11 a ⇒ λaddr11: True.
    992           let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 program_counter in
    993           let 〈nu, nl〉 ≝ vsplit ? 4 4 pc_bu in
    994           let bit ≝ get_index' ? O ? nl in
    995           let 〈relevant1, relevant2〉 ≝ vsplit ? 3 8 a in
    996           let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    997           let 〈carry, new_pc〉 ≝ half_add ? program_counter new_addr in
    998             new_pc
     992          let 〈pc_bu, pc_bl〉 ≝ vsplit ? 5 11 program_counter in
     993          let new_addr ≝ pc_bu @@ a in
     994            new_addr
    999995        | _ ⇒ λother: False. ⊥
    1000996        ] (subaddressing_modein … addr)
Note: See TracChangeset for help on using the changeset viewer.