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

    r1962 r2032  
    2727  #m #s #v
    2828  whd in match write_at_stack_pointer; normalize nodelta
    29   cases(split … 4 4 ?) #nu #nl normalize nodelta
     29  cases(vsplit … 4 4 ?) #nu #nl normalize nodelta
    3030  cases(get_index_v … 4 nu 0 ?) //
    3131qed.
     
    178178  whd in match set_arg_8; normalize nodelta
    179179  whd in match set_arg_8'; normalize nodelta
    180   cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
    181   cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
     180  cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta
     181  cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta
    182182  cases (get_index_v bool 4 nu' 0 ?) normalize nodelta
    183183  try % @set_bit_addressable_sfr_set_code_memory
     
    201201  whd in match set_arg_8; normalize nodelta
    202202  whd in match set_arg_8'; normalize nodelta
    203   cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
    204   cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
     203  cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta
     204  cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta
    205205  cases (get_index_v bool 4 nu' 0 ?) normalize nodelta
    206206  try % cases daemon (*@(set_bit_addressable_sfr_set_program_counter)*)
     
    238238  = special_function_registers_8051 T cm s.
    239239 #T #cm #s #x whd in ⊢ (??(???%)?);
    240  cases (split ????) #nu #nl normalize nodelta;
     240 cases (vsplit ????) #nu #nl normalize nodelta;
    241241 cases (get_index_v bool ????) %
    242242qed.
     
    250250 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
    251251 #T #s #x whd in ⊢ (??(??%)?);
    252  cases (split ????) #nu #nl normalize nodelta;
     252 cases (vsplit ????) #nu #nl normalize nodelta;
    253253 cases (get_index_v bool ????) %
    254254qed.*)
     
    299299 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s.
    300300 #T #cm #s #x whd in ⊢ (??(???%)?);
    301  cases (split ????) #nu #nl normalize nodelta;
     301 cases (vsplit ????) #nu #nl normalize nodelta;
    302302 cases (get_index_v bool ????) %
    303303qed.
     
    308308  = special_function_registers_8052 T cm s.
    309309 #T #cm #s #x whd in ⊢ (??(???%)?);
    310  cases (split ????) #nu #nl normalize nodelta;
     310 cases (vsplit ????) #nu #nl normalize nodelta;
    311311 cases (get_index_v bool ????) %
    312312qed.
     
    315315 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s.
    316316 #T #cm #s #x whd in ⊢ (??(???%)?);
    317  cases (split ????) #nu #nl normalize nodelta;
     317 cases (vsplit ????) #nu #nl normalize nodelta;
    318318 cases (get_index_v bool ????) %
    319319qed.
     
    322322 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s.
    323323 #T #cm #s #x whd in ⊢ (??(???%)?);
    324  cases (split ????) #nu #nl normalize nodelta;
     324 cases (vsplit ????) #nu #nl normalize nodelta;
    325325 cases (get_index_v bool ????) %
    326326qed.
     
    356356  try (#ignore #addr normalize in addr; cases addr)
    357357  normalize nodelta try #_ try /demod/ try %
    358   cases (split bool 4 4 ?) #nu #nl normalize nodelta
    359   cases (split bool 1 3 ?) #ignore #three_bits normalize nodelta
     358  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta
     359  cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta
    360360  cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try %
    361361qed.
     
    373373  try (#addr normalize in addr; cases addr)
    374374  normalize nodelta
    375   cases (split bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try %
    376   cases (split bool 1 3 ?) #ignore #three_bits normalize nodelta
     375  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try %
     376  cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta
    377377  cases (get_index_v bool 4 nu ??) normalize nodelta
    378378  (* XXX: try /demod/ try % *)
     
    391391  try (#addr normalize in addr; cases addr)
    392392  normalize nodelta
    393   cases (split bool 8 8 v) #bu #bl normalize nodelta /demod/ %
     393  cases (vsplit bool 8 8 v) #bu #bl normalize nodelta /demod/ %
    394394qed.
    395395
     
    413413  #m #cm #s #v
    414414  whd in match write_at_stack_pointer; normalize nodelta
    415   cases (split bool 4 4 ?) #nu #nl normalize nodelta
     415  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta
    416416  cases (get_index_v bool 4 nu ??) normalize nodelta /demod/ %
    417417qed.
Note: See TracChangeset for help on using the changeset viewer.