Changeset 259


Ignore:
Timestamp:
Nov 23, 2010, 12:56:26 PM (9 years ago)
Author:
mulligan
Message:

Need stronger set_ and get_index functions on vectors (current ones return a Maybe type).

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

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

    r258 r259  
    44
    55(* include "ASM.ma". *)
     6include "Arithmetic.ma".
    67include "BitVectorTrie.ma".
    7 include "Arithmetic.ma".
    88
    99ninductive SFR8051: Type[0] ≝
     
    8585}.
    8686
     87alias id "replicate" = "cic:/matita/Cerco/Vector/replicate.fix(0,1,1)".
    8788
     89ndefinition set_8051_sfr ≝
     90  λs: Status.
     91  λi: SFR8051.
     92  λb: Byte.
     93    let index ≝ sfr_8051_status i in
     94    let
    8895
    8996ndefinition initialise_status ≝
    90   mk_Status
    91     (Stub Byte sixteen)
    92     (Stub Byte seven)
    93     (Stub Byte seven)
    94     (Stub Byte sixteen)
    95     (zero sixteen)
    96     ([ zero eight; zero eight; zero eight; zero eight;
    97        zero eight; zero eight; zero eight; zero eight ]).
     97  let status ≝ mk_Status (Stub Byte sixteen)
     98                         (Stub Byte seven)
     99                         (Stub Byte seven)
     100                         (Stub Byte sixteen)
     101                         (zero sixteen)
     102                         (replicate Byte nineteen (zero eight))
     103                         (replicate Byte five (zero eight)) in
     104  status.
  • Deliverables/D4.1/Matita/Vector.ma

    r256 r259  
    5454interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
    5555   
    56 nlet rec set_index (A: Type[0]) (n: Nat)
    57                    (v: Vector A n) (m: Nat) (a: A) on m ≝
     56nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) on m ≝
     57  match m return (λx. x < n → A) with
     58    [ Z ⇒
     59      match v with
     60        [ Empty ⇒ λ_.?
     61        | Cons p hd tl ⇒ λ_.hd
     62        ]
     63    | S o ⇒
     64      match v with
     65        [ Empty ⇒ λ_.?
     66        | Cons p hd tl ⇒ λprf: m < p. set_index A p tl o a
     67        ]
     68    ].
     69   
     70nlet rec set_index_weak (A: Type[0]) (n: Nat)
     71                        (v: Vector A n) (m: Nat) (a: A) on m ≝
    5872  match m with
    5973    [ Z ⇒
     
    6680        [ Empty ⇒ Nothing (Vector A n)
    6781        | Cons p hd tl ⇒
    68             let settail ≝ set_index A p tl o a in
     82            let settail ≝ set_index_weak A p tl o a in
    6983              match settail with
    7084                [ Nothing ⇒ Nothing (Vector A n)
Note: See TracChangeset for help on using the changeset viewer.