Changeset 311


Ignore:
Timestamp:
Nov 26, 2010, 1:28:13 PM (9 years ago)
Author:
mulligan
Message:

get_arg_16 complete.

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

Legend:

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

    r310 r311  
    710710                                                acc_pc ; ext_indirect ;
    711711                                                ext_indirect_dptr ]] x) → ? with
    712       [ ACC_A ⇒ λK: True. get_8051_sfr s SFR_ACC_A
    713       | ACC_B ⇒ λK: True. get_8051_sfr s SFR_ACC_B
    714       | DATA d ⇒ λK: True. d
    715       | REGISTER r1 r2 r3 ⇒ λK: True. get_register s r1 r2 r3
     712      [ ACC_A ⇒ λacc_a: True. get_8051_sfr s SFR_ACC_A
     713      | ACC_B ⇒ λacc_b: True. get_8051_sfr s SFR_ACC_B
     714      | DATA d ⇒ λdata: True. d
     715      | REGISTER r1 r2 r3 ⇒ λregister: True. get_register s r1 r2 r3
    716716      | EXT_INDIRECT_DPTR ⇒
    717         λK: True.
     717        λext_indirect_dptr: True.
    718718          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    719719            lookup … sixteen address (external_ram s) (zero eight)
    720720      | EXT_INDIRECT e ⇒
    721         λK: True.
     721        λext_indirect: True.
    722722          let address ≝ get_register s false false e in
    723723          let padded_address ≝ pad eight eight address in
    724             lookup … sixteen padded_address (external_ram s)
     724            lookup … sixteen padded_address (external_ram s) (zero eight)
    725725      | ACC_DPTR ⇒
    726         λK: True.
     726        λacc_dptr: True.
    727727          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    728728          let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
     
    730730            lookup … sixteen address (external_ram s) (zero eight)
    731731      | ACC_PC ⇒
    732         λK: True.
     732        λacc_pc: True.
    733733          let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
    734734          let 〈 address, carry 〉 ≝ half_add sixteen (program_counter s) padded_acc in
    735735            lookup … sixteen address (external_ram s) (zero eight)
    736736      | DIRECT d ⇒
    737         λK: True.
    738           ?
     737        λdirect: True.
     738          let 〈 nu, nl 〉 ≝ split … four four d in
     739          let bit_one ≝ get_index … nu one ? in
     740            match bit_one with
     741              [ true ⇒
     742                  let 〈 bit_one, three_bits 〉 ≝ split ? one three nu in
     743                  let address ≝ three_bits @@ nl in
     744                    lookup ? seven address (low_internal_ram s) (zero eight)
     745              | false ⇒ get_bit_addressable_sfr s eight d l
     746              ]
    739747      | INDIRECT i ⇒
    740         λK: True. ?
    741       | _ ⇒ λK. ?
     748        λindirect: True.
     749          let 〈 nu, nl 〉 ≝ split ? four four (get_register s false false i) in
     750          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
     751          let bit_one ≝ get_index … bit_one_v Z ? in
     752          match bit_one with
     753            [ true ⇒
     754                lookup ? seven (three_bits @@ nl) (low_internal_ram s) (zero eight)
     755            | false ⇒
     756                lookup ? seven (three_bits @@ nl) (high_internal_ram s) (zero eight)
     757            ]
     758      | _ ⇒ λother.
     759        match other in False with [ ]
    742760      ] (subaddressing_modein … a).
    743       nauto;
    744 nqed.
     761      ##[##1,2:
     762          nnormalize;
     763          nrepeat (napply less_than_or_equal_monotone);
     764          napply less_than_or_equal_zero;
     765      ##]
     766nqed.
     767nqed.
  • Deliverables/D4.1/Matita/Vector.ma

    r272 r311  
    133133nqed.
    134134
    135 nlet rec split (A: Type[0]) (n,m: Nat) on m
     135nlet rec split (A: Type[0]) (m,n: Nat) on m
    136136             : Vector A (m+n) → (Vector A m) × (Vector A n)
    137137
     
    142142      [ Empty ⇒ λK.⊥
    143143      | Cons o he tl ⇒ λK.
    144          match split A n m' (tl⌈Vector A (m'+n)↦Vector A o⌉) with
     144         match split A m' n (tl⌈Vector A (m'+n)↦Vector A o⌉) with
    145145          [ mk_Cartesian v1 v2 ⇒ 〈he::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
    146146//; ndestruct; //.
Note: See TracChangeset for help on using the changeset viewer.