Changeset 2032 for src/Clight/casts.ma


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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/casts.ma

    r1599 r2032  
    22
    33definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝
    4 λm,n,x. \snd (split … x).
    5 
    6 lemma split_O_n : ∀A,n,x. split A O n x = 〈[[ ]], x〉.
     4λm,n,x. \snd (vsplit … x).
     5
     6lemma vsplit_O_n : ∀A,n,x. vsplit A O n x = 〈[[ ]], x〉.
    77#A #n cases n [ #x @(vector_inv_n … x) @refl | #m #x @(vector_inv_n … x) // ]
    88qed.
    99
    1010lemma truncate_eq : ∀n,x. truncate 0 n x = x.
    11 #n #x normalize >split_O_n @refl
     11#n #x normalize >vsplit_O_n @refl
    1212qed.
    1313
     
    6666qed.
    6767
    68 lemma split_eq' : ∀A,m,n,v. split A m n v = split' A m n v.
     68lemma vsplit_eq' : ∀A,m,n,v. vsplit A m n v = vsplit' A m n v.
    6969#A #m cases m
    7070[ #n cases n
     
    7575] qed. 
    7676
    77 lemma split_left : ∀A,m,n,h,t.
    78   split A (S m) n (h:::t) = (let 〈l,r〉 ≝ split A m n t in 〈h:::l,r〉).
    79 #A #m #n #h #t normalize >split_eq' @refl
     77lemma vsplit_left : ∀A,m,n,h,t.
     78  vsplit A (S m) n (h:::t) = (let 〈l,r〉 ≝ vsplit A m n t in 〈h:::l,r〉).
     79#A #m #n #h #t normalize >vsplit_eq' @refl
    8080qed.
    8181
    8282lemma truncate_head : ∀m,n,h,t.
    8383  truncate (S m) n (h:::t) = truncate m n t.
    84 #m #n #h #t normalize >split_eq' cases (split' bool m n t) //
     84#m #n #h #t normalize >vsplit_eq' cases (vsplit' bool m n t) //
    8585qed.
    8686
Note: See TracChangeset for help on using the changeset viewer.