Changeset 2032 for src/RTLabs


Ignore:
Timestamp:
Jun 8, 2012, 4:32:03 PM (7 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.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r1995 r2032  
    134134  [ I8 ⇒ λint. ? | I16 ⇒ λint. ? | I32 ⇒ λint. ? ].
    135135[ %[@[int]] //
    136 | %[@(let 〈h,l〉 ≝ split ? 8 … int in [l;h])] cases (split ????) //
    137 | %[@(let 〈h1,l〉 ≝ split ? 8 … int in
    138       let 〈h2,l〉 ≝ split ? 8 … l in
    139       let 〈h3,l〉 ≝ split ? 8 … l in
     136| %[@(let 〈h,l〉 ≝ vsplit ? 8 … int in [l;h])] cases (vsplit ????) //
     137| %[@(let 〈h1,l〉 ≝ vsplit ? 8 … int in
     138      let 〈h2,l〉 ≝ vsplit ? 8 … l in
     139      let 〈h3,l〉 ≝ vsplit ? 8 … l in
    140140       [l;h3;h2;h1])]
    141   cases (split ????) #h1 #l normalize
    142   cases (split ????) #h2 #l normalize
    143   cases (split ????) // ]
     141  cases (vsplit ????) #h1 #l normalize
     142  cases (vsplit ????) #h2 #l normalize
     143  cases (vsplit ????) // ]
    144144qed.
    145145
     
    533533  λtranslates: list ?.
    534534  λsrcr2i: register.
    535   let 〈tmp_destrs1, tmp_destrs2〉 ≝ split … tmp_destrs i i_prf in
     535  let 〈tmp_destrs1, tmp_destrs2〉 ≝ vsplit … tmp_destrs i i_prf in
    536536  let tmp_destrs2' ≝
    537537    match tmp_destrs2 with
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r1882 r2032  
    119119  [ I8 ⇒ λint. ? | I16 ⇒ λint. ? | I32 ⇒ λint. ? ].
    120120[ %[@[int]] //
    121 | %[@(let 〈h,l〉 ≝ split ? 8 … int in [l;h])] cases (split ????) normalize //
    122 | %[@(let 〈h1,l〉 ≝ split ? 8 … int in
    123       let 〈h2,l〉 ≝ split ? 8 … l in
    124       let 〈h3,l〉 ≝ split ? 8 … l in
     121| %[@(let 〈h,l〉 ≝ vsplit ? 8 … int in [l;h])] cases (vsplit ????) normalize //
     122| %[@(let 〈h1,l〉 ≝ vsplit ? 8 … int in
     123      let 〈h2,l〉 ≝ vsplit ? 8 … l in
     124      let 〈h3,l〉 ≝ vsplit ? 8 … l in
    125125       [l;h3;h2;h1])]
    126   cases (split ????) #h1 #l normalize
    127   cases (split ????) #h2 #l normalize
    128   cases (split ????) // ]
     126  cases (vsplit ????) #h1 #l normalize
     127  cases (vsplit ????) #h2 #l normalize
     128  cases (vsplit ????) // ]
    129129qed.
    130130
Note: See TracChangeset for help on using the changeset viewer.