Ignore:
Timestamp:
Nov 30, 2010, 4:56:42 PM (9 years ago)
Author:
mulligan
Message:

Fixed Status.ma so that it compiles.

File:
1 edited

Legend:

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

    r337 r343  
    696696      set_low_internal_ram s new_low_internal_ram.
    697697     
    698 alias id "get_index" = "cic:/matita/ng/BitVector/get_index.def(3)".
    699698ndefinition read_at_stack_pointer ≝
    700699  λs: Status.
    701700    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
    702     let m ≝ get_index … nu Z ? in
    703     let r1 ≝ get_index … nu one ? in
    704     let r2 ≝ get_index … nu two ? in
    705     let r3 ≝ get_index … nu three ? in
     701    let m ≝ get_index_bv … nu Z ? in
     702    let r1 ≝ get_index_bv … nu one ? in
     703    let r2 ≝ get_index_bv … nu two ? in
     704    let r3 ≝ get_index_bv … nu three ? in
    706705    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
    707706    let memory ≝
     
    765764        ]
    766765      ] (subaddressing_modein … a).
     766     
     767ncheck get_index_bv.
    767768     
    768769ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ;
     
    802803        λdirect: True.
    803804          let 〈 nu, nl 〉 ≝ split … four four d in
    804           let bit_one ≝ get_index … nu one ? in
     805          let bit_one ≝ get_index_bv … nu one ? in
    805806            match bit_one with
    806807              [ true ⇒
     
    814815          let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in
    815816          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    816           let bit_one ≝ get_index … bit_one_v Z ? in
     817          let bit_one ≝ get_index_bv … bit_one_v Z ? in
    817818          match bit_one with
    818819            [ true ⇒
     
    841842        λdirect: True.
    842843          let 〈 nu, nl 〉 ≝ split … four four d in
    843           let bit_one ≝ get_index … nu one ? in
     844          let bit_one ≝ get_index_bv … nu one ? in
    844845          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    845846            match bit_one with
     
    853854          let register ≝ get_register s [[ false; false; i ]] in
    854855          let 〈 nu, nl 〉 ≝ split ? four four register in
    855           let bit_one ≝ get_index ? nu one ? in
     856          let bit_one ≝ get_index_bv ? nu one ? in
    856857          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    857858          match bit_one with
     
    901902        λbit_addr: True.
    902903          let 〈 nu, nl 〉 ≝ split … four four b in
    903           let bit_one ≝ get_index … nu one ? in
     904          let bit_one ≝ get_index_bv … nu one ? in
    904905          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    905906            match bit_one with
     
    910911                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
    911912                let sfr ≝ get_bit_addressable_sfr s ? trans l in
    912                   get_index ? sfr m ?
     913                  get_index_bv ? sfr m ?
    913914              | false ⇒
    914915                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    915916                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
    916917                let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    917                   get_index ? t (modulus address eight) ?
     918                  get_index_bv ? t (modulus address eight) ?
    918919              ]
    919920      | N_BIT_ADDR n ⇒
    920921        λn_bit_addr: True.
    921922          let 〈 nu, nl 〉 ≝ split … four four n in
    922           let bit_one ≝ get_index … nu one ? in
     923          let bit_one ≝ get_index_bv … nu one ? in
    923924          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    924925            match bit_one with
     
    929930                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
    930931                let sfr ≝ get_bit_addressable_sfr s ? trans l in
    931                   negation (get_index ? sfr m ?)
     932                  negation (get_index_bv ? sfr m ?)
    932933              | false ⇒
    933934                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    934935                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
    935936                let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    936                   negation (get_index ? trans (modulus address eight) ?)
     937                  negation (get_index_bv ? trans (modulus address eight) ?)
    937938              ]
    938939      | CARRY ⇒ λcarry: True. get_cy_flag s
     
    955956      [ BIT_ADDR b ⇒ λbit_addr: True.
    956957          let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    957           let bit_one ≝ get_index ? nu one ? in
     958          let bit_one ≝ get_index_bv ? nu one ? in
    958959          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    959960          match bit_one with
Note: See TracChangeset for help on using the changeset viewer.