Changeset 364 for Deliverables


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

Added subvector_with function.

Location:
Deliverables/D4.1/Matita
Files:
4 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.
  • Deliverables/D4.1/Matita/List.ma

    r357 r364  
    5353  for @{ 'append $l $r }.   
    5454 
    55 interpretation "List append" 'append = (append ?). 
     55interpretation "List append" 'append = (append ?).
     56
     57(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     58(* Maps and zips.                                                             *)
     59(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     60
     61nlet rec map (A: Type[0]) (B: Type[0])
     62             (f: A → B) (l: List A) on l ≝
     63  match l with
     64    [ Empty ⇒ Empty B
     65    | Cons hd tl ⇒ f hd :: map A B f tl
     66    ].
     67   
     68nlet rec flatten (A: Type[0]) (l: List (List A)) on l ≝
     69  match l with
     70    [ Empty ⇒ Empty A
     71    | Cons hd tl ⇒ hd @ (flatten A tl)
     72    ].
     73   
     74ndefinition map_flatten ≝
     75  λA: Type[0].
     76  λf: A → List A.
     77  λl: List A.
     78    flatten A (map A (List A) f l).
    5679 
    5780(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    6992    [ Empty ⇒ Empty A
    7093    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
     94    ].
     95   
     96nlet rec power_list (A: Type[0]) (l: List A) on l ≝
     97  match l with
     98    [ Empty ⇒ [ [ ] ]
     99    | Cons hd tl ⇒
     100        let r ≝ power_list A tl in
     101          (map ? ? (λx. hd :: x) r) @ r
    71102    ].
    72103 
     
    284315
    285316(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    286 (* Maps and zips.                                                             *)
    287 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    288 
    289 nlet rec map (A: Type[0]) (B: Type[0])
    290              (f: A → B) (l: List A) on l ≝
    291   match l with
    292     [ Empty ⇒ Empty B
    293     | Cons hd tl ⇒ f hd :: map A B f tl
    294     ].
    295    
    296 nlet rec flatten (A: Type[0]) (l: List (List A)) on l ≝
    297   match l with
    298     [ Empty ⇒ Empty A
    299     | Cons hd tl ⇒ hd @ (flatten A tl)
    300     ].
    301    
    302 ndefinition map_flatten ≝
    303   λA: Type[0].
    304   λf: A → List A.
    305   λl: List A.
    306     flatten A (map A (List A) f l).
    307 
    308 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    309317(* Set-like operations.                                                       *)
    310318(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    340348  λm: Nat.
    341349    reverse A (rotate_left A (reverse A l) m).
     350
     351(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     352(* Decidable equality.                                                        *)
     353(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     354
     355nlet rec eq_l (A: Type[0]) (f: A → A → Bool) (l: List A) (m: List A) on l ≝
     356  match l with
     357    [ Empty ⇒
     358      match m with
     359        [ Empty ⇒ true
     360        | Cons hd tl ⇒ false
     361        ]
     362    | Cons hd tl ⇒
     363      match m with
     364        [ Empty ⇒ false
     365        | Cons hd' tl' ⇒ conjunction (f hd hd') (eq_l A f tl tl')
     366        ]
     367    ].     
    342368
    343369(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • Deliverables/D4.1/Matita/Vector.ma

    r363 r364  
    410410        napply tl' ]
    411411nqed.
     412
     413(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     414(* Subvectors.                                                                *)
     415(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     416
     417ndefinition subvector_with ≝
     418  λA: Type[0].
     419  λn: Nat.
     420  λm: Nat.
     421  λf: A → A → Bool.
     422  λv: Vector A n.
     423  λq: Vector A m.
     424    let list_q ≝ list_of_vector A m q in
     425    let list_v ≝ list_of_vector A n v in
     426    let power ≝ power_list A list_q in
     427      member_with ? list_v (λx, y. eq_l ? f x y) power.
    412428   
    413429(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • Deliverables/D4.1/Matita/depends

    r357 r364  
     1Exponential.ma Nat.ma
     2Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    13Arithmetic.ma BitVector.ma Exponential.ma
    2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    3 Exponential.ma Nat.ma
    44BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
    55Cartesian.ma Universes.ma
     6Universes.ma
    67Maybe.ma Bool.ma Plogic/equality.ma
    78Either.ma Bool.ma
    8 Universes.ma
    9 DoTest.ma Interpret.ma Test.ma
     9DoTest.ma Assembly.ma Interpret.ma Test.ma
    1010ASM.ma BitVector.ma Either.ma String.ma
    11 Vector.ma List.ma Nat.ma
    1211Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    1312Char.ma Universes.ma
    1413Test.ma ASM.ma
     14Vector.ma List.ma Nat.ma
    1515Connectives.ma Plogic/equality.ma
    1616Bool.ma Universes.ma
    1717Assembly.ma ASM.ma
    1818List.ma Maybe.ma Util.ma
     19Interpret.ma Fetch.ma Status.ma
    1920Util.ma Nat.ma
    20 Interpret.ma Fetch.ma Status.ma
    2121BitVector.ma Vector.ma
    2222String.ma Char.ma List.ma
Note: See TracChangeset for help on using the changeset viewer.