Ignore:
Timestamp:
Jun 8, 2012, 4:32:03 PM (8 years ago)
Author:
sacerdot
Message:

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/WellLabeled.ma

    r1494 r2032  
    3131        match acall return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    3232        [ ADDR11 addr11 ⇒ λ_.
    33           let 〈pc_bu, pc_bl〉 ≝ split … 8 8 pc in
    34           let 〈thr, eig〉 ≝ split … 3 8 addr11 in
    35           let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
     33          let 〈pc_bu, pc_bl〉 ≝ vsplit … 8 8 pc in
     34          let 〈thr, eig〉 ≝ vsplit … 3 8 addr11 in
     35          let 〈fiv, thr'〉 ≝ vsplit … 5 3 pc_bu in
    3636          let new_pc ≝ (fiv @@ thr) @@ pc_bl in
    3737            match lookup_opt … new_pc cost_labels with
     
    4444        match ajmp return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    4545        [ ADDR11 addr11 ⇒ λ_.
    46           let 〈pc_bu, pc_bl〉 ≝ split … 8 8 pc in
    47           let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
     46          let 〈pc_bu, pc_bl〉 ≝ vsplit … 8 8 pc in
     47          let 〈nu, nl〉 ≝ vsplit … 4 4 pc_bu in
    4848          let bit ≝ get_index' … O ? nl in
    49           let 〈relevant1, relevant2〉 ≝ split … 3 8 addr11 in
     49          let 〈relevant1, relevant2〉 ≝ vsplit … 3 8 addr11 in
    5050          let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    5151          let 〈carry, new_pc〉 ≝ half_add … pc new_addr in
Note: See TracChangeset for help on using the changeset viewer.