Changeset 2032 for src/ASM/Arithmetic.ma


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/Arithmetic.ma

    r2028 r2032  
    55  λpc: Word.
    66  λa: Word11.
    7   let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
    8   let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
    9   let 〈b123, b〉 ≝ split … 3 8 a in
     7  let 〈pc_upper, ignore〉 ≝ vsplit … 8 8 pc in
     8  let 〈n1, n2〉 ≝ vsplit … 4 4 pc_upper in
     9  let 〈b123, b〉 ≝ vsplit … 3 8 a in
    1010  let b1 ≝ get_index_v … b123 0 ? in
    1111  let b2 ≝ get_index_v … b123 1 ? in
     
    454454      [ None ⇒ None ?
    455455      | Some result ⇒
    456           let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in
     456          let 〈high_bits, low_bits〉 ≝ vsplit bool ? n (multiplication n result c) in
    457457            Some ? (subtraction n b low_bits)
    458458      ].
     
    571571  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
    572572  | nat_eq n' ⇒ λv. v
    573   | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
     573  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
    574574  ].
    575575
     
    579579  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
    580580  | nat_eq n' ⇒ λv. v
    581   | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
     581  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
    582582  ].
    583583
Note: See TracChangeset for help on using the changeset viewer.