Ignore:
Timestamp:
Dec 2, 2010, 4:36:35 PM (9 years ago)
Author:
mulligan
Message:

Added subvector_with function.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Interpret.ma

    r363 r364  
    55  λb.
    66    zero eight @@ b.
    7 
    8 naxiom daemon: False.
    9 
     7   
     8naxiom eq_a: addressing_mode_tag → addressing_mode_tag → Bool.
     9   
     10nlemma execute_1_technical:
     11  ∀n,m: Nat.
     12  ∀v: Vector addressing_mode_tag (S n).
     13  ∀q: Vector addressing_mode_tag (S m).
     14  ∀a: addressing_mode.
     15    bool_to_Prop (is_in ? v a) →
     16    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
     17    bool_to_Prop (is_in ? q a).
     18  #n m v q a.
     19  ncases a.
     20  nnormalize.
     21   
    1022ndefinition execute_1: Status → Status ≝
    1123  λs.
     
    189201            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    190202            let new_cy_flag ≝ get_index' ? Z ? old_acc in
    191             let new_acc ≝ shift_left_bv eight one old_acc old_cy_flag in
     203            let new_acc ≝ shift_left ? eight one old_acc old_cy_flag in
    192204            let s ≝ set_arg_1 s CARRY new_cy_flag in
    193205              set_8051_sfr s SFR_ACC_A new_acc
     
    196208            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    197209            let new_cy_flag ≝ get_index' ? seven ? old_acc in
    198             let new_acc ≝ shift_right_bv eight one old_acc old_cy_flag in
     210            let new_acc ≝ shift_right ? eight one old_acc old_cy_flag in
    199211            let s ≝ set_arg_1 s CARRY new_cy_flag in
    200212              set_8051_sfr s SFR_ACC_A new_acc
     
    486498    in
    487499      s.
    488     ##[##2,3,4,8,9,10,14,15,16,43,104,106:
    489          nnormalize;
    490          nrepeat (napply (less_than_or_equal_monotone));
    491          napply (less_than_or_equal_zero);
    492     ##|##23,28,29,30,31,32,33,34,35,36,37,38,39,40,64,65,66,
    493          67,68,69,70,71,72,73,74,75,76,79,80,81,82,117,118,119,
    494          120,121,122,123,124,125,126,127,128,129,130,131,132,
    495          133,139,140,141,142,143,144,145,146,147,148,149,150,
    496          151,152,153,154,155,156,162,163,164,165,166,167,168,
    497          169,170,171,172,173,174,175,176,177,178,179,180,181,
    498          182,183,184,185,186,187,188,189,190,191,192,193,194,
    499          195,196,197,198,199,200,201,202,203,204,205,206,207,
    500          208,209,210,211,212,213:
    501            nassumption;
     500    ##[ ntry
     501          nassumption;
     502    ##| ntry (
     503          nnormalize
     504          nrepeat (napply (less_than_or_equal_monotone))
     505          napply (less_than_or_equal_zero)
     506        );
     507    ##| ntry (
     508          nnormalize
     509          //
     510        );
     511    ##| ntry (
     512          nnormalize
     513          //);
    502514    ##|
    503515nqed.
Note: See TracChangeset for help on using the changeset viewer.