Changeset 2032 for src/common


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/common
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r1878 r2032  
    244244  [ Vint sz1 n1 ⇒ match v2 with
    245245    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    246                     (λn1. Some ? (Vint ? (\snd (split … (multiplication ? n1 n2)))))
     246                    (λn1. Some ? (Vint ? (\snd (vsplit … (multiplication ? n1 n2)))))
    247247                    (None ?)
    248248    | _ ⇒ None ? ]
  • src/common/FrontEndVal.ma

    r1987 r2032  
    2525match n return λn. BitVector (n*8) → ? with
    2626[ O ⇒ λ_. [ ]
    27 | S m ⇒ λv. let 〈h,t〉 ≝ split ??? v in h::(bytes_of_bitvector m t)
     27| S m ⇒ λv. let 〈h,t〉 ≝ vsplit ??? v in h::(bytes_of_bitvector m t)
    2828] v.
    2929
  • src/common/Integers.ma

    r1516 r2032  
    136136
    137137definition neg : int → int ≝ two_complement_negation wordsize.
    138 definition mul ≝ λx,y. \snd (split ? wordsize wordsize (multiplication wordsize x y)).
     138definition mul ≝ λx,y. \snd (vsplit ? wordsize wordsize (multiplication wordsize x y)).
    139139
    140140definition zero_ext_n : ∀w,n:nat. BitVector w → BitVector w ≝
     
    142142  match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with
    143143  [ nat_lt n' w' ⇒ λi.
    144       let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in
     144      let 〈h,l〉 ≝ vsplit ? (S w') n' (switch_bv_plus ??? i) in
    145145      switch_bv_plus ??? (pad ?? l)
    146146  | _ ⇒ λi.i
     
    153153  match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with
    154154  [ nat_lt n' w' ⇒ λi.
    155       let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in
     155      let 〈h,l〉 ≝ vsplit ? (S w') n' (switch_bv_plus ??? i) in
    156156      switch_bv_plus ??? (pad_vector ? (match l with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ]) ?? l)
    157157  | _ ⇒ λi.i
  • src/common/Values.ma

    r1872 r2032  
    214214  [ Vint sz1 n1 ⇒ match v2 with
    215215    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    216                     (λn1. Vint sz2 (\snd (split … (multiplication ? n1 n2))))
     216                    (λn1. Vint sz2 (\snd (vsplit … (multiplication ? n1 n2))))
    217217                    Vundef
    218218    | _ ⇒ Vundef ]
Note: See TracChangeset for help on using the changeset viewer.