Ignore:
Timestamp:
Dec 2, 2010, 11:53:49 AM (10 years ago)
Author:
sacerdot
Message:

Less ambiguous definitions.

File:
1 edited

Legend:

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

    r357 r362  
    191191    let sfr ≝ special_function_registers_8051 s in
    192192    let index ≝ sfr_8051_index i in
    193       get_index ?? sfr index ?.
    194     napply (sfr8051_index_nineteen i).
     193      get_index_v … sfr index ?.
     194    napply sfr8051_index_nineteen.
    195195nqed.
    196196
     
    200200    let sfr ≝ special_function_registers_8052 s in
    201201    let index ≝ sfr_8052_index i in
    202       get_index ?? sfr index ?.
    203     napply (sfr8052_index_five i).
     202      get_index_v … sfr index ?.
     203    napply sfr8052_index_five.
    204204nqed.
    205205
     
    383383  λs: Status.
    384384    let sfr ≝ special_function_registers_8051 s in
    385     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    386       get_index Bool eight psw Z ?.
     385    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     386      get_index_v Bool eight psw Z ?.
    387387    nnormalize.
    388388    napply (less_than_or_equal_monotone ? ?).
     
    395395  λs: Status.
    396396    let sfr ≝ special_function_registers_8051 s in
    397     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    398       get_index Bool eight psw (S Z) ?.
     397    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     398      get_index_v Bool eight psw (S Z) ?.
    399399    nnormalize.
    400400    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    407407  λs: Status.
    408408    let sfr ≝ special_function_registers_8051 s in
    409     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    410       get_index Bool eight psw two ?.
     409    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     410      get_index_v Bool eight psw two ?.
    411411    nnormalize.
    412412    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    419419  λs: Status.
    420420    let sfr ≝ special_function_registers_8051 s in
    421     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    422       get_index Bool eight psw three ?.
     421    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     422      get_index_v Bool eight psw three ?.
    423423    nnormalize.
    424424    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    431431  λs: Status.
    432432    let sfr ≝ special_function_registers_8051 s in
    433     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    434       get_index Bool eight psw four ?.
     433    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     434      get_index_v Bool eight psw four ?.
    435435    nnormalize.
    436436    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    443443  λs: Status.
    444444    let sfr ≝ special_function_registers_8051 s in
    445     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    446       get_index Bool eight psw five ?.
     445    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     446      get_index_v Bool eight psw five ?.
    447447    nnormalize.
    448448    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    455455  λs: Status.
    456456    let sfr ≝ special_function_registers_8051 s in
    457     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    458       get_index Bool eight psw six ?.
     457    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     458      get_index_v Bool eight psw six ?.
    459459    nnormalize.
    460460    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    467467  λs: Status.
    468468    let sfr ≝ special_function_registers_8051 s in
    469     let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    470       get_index Bool eight psw seven ?.
     469    let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
     470      get_index_v Bool eight psw seven ?.
    471471    nnormalize.
    472472    nrepeat (napply (less_than_or_equal_monotone ? ?)).
     
    482482  λov: Bit.
    483483    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
    484     let old_cy ≝ get_index … nu Z ? in
    485     let old_ac ≝ get_index … nu one ? in
    486     let old_fo ≝ get_index … nu two ? in
    487     let old_rs1 ≝ get_index … nu three ? in
    488     let old_rs0 ≝ get_index … nl Z ? in
    489     let old_ov ≝ get_index … nl one ? in
    490     let old_ud ≝ get_index … nl two ? in
    491     let old_p ≝ get_index … nl three ? in
     484    let old_cy ≝ get_index_v… nu Z ? in
     485    let old_ac ≝ get_index_v… nu one ? in
     486    let old_fo ≝ get_index_v… nu two ? in
     487    let old_rs1 ≝ get_index_v… nu three ? in
     488    let old_rs0 ≝ get_index_v… nl Z ? in
     489    let old_ov ≝ get_index_v… nl one ? in
     490    let old_ud ≝ get_index_v… nl two ? in
     491    let old_p ≝ get_index_v… nl three ? in
    492492    let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in
    493493    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
     
    655655  λs: Status.
    656656  λr: BitVector three.
    657     let b ≝ get_index_bv ? r Z ? in
    658     let c ≝ get_index_bv ? r one ? in
    659     let d ≝ get_index_bv ? r two ? in
     657    let b ≝ get_index_v … r Z ? in
     658    let c ≝ get_index_v … r one ? in
     659    let d ≝ get_index_v … r two ? in
    660660    let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    661     let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_bv four un two ?) (get_index_bv four un three ?) in
     661    let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_v … four un two ?) (get_index_v … four un three ?) in
    662662    let offset ≝
    663663      if conjunction (negation r1) (negation r0) then
     
    696696  λs: Status.
    697697    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
    698     let m ≝ get_index_bv … nu Z ? in
    699     let r1 ≝ get_index_bv … nu one ? in
    700     let r2 ≝ get_index_bv … nu two ? in
    701     let r3 ≝ get_index_bv … nu three ? in
     698    let m ≝ get_index_v … nu Z ? in
     699    let r1 ≝ get_index_v … nu one ? in
     700    let r2 ≝ get_index_v … nu two ? in
     701    let r3 ≝ get_index_v … nu three ? in
    702702    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
    703703    let memory ≝
     
    719719  λv: Byte.
    720720    let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
    721     let bit_zero ≝ get_index … nu Z ? in
    722     let bit_one ≝ get_index … nu one ? in
    723     let bit_two ≝ get_index … nu two ? in
    724     let bit_three ≝ get_index … nu three ? in
     721    let bit_zero ≝ get_index_v… nu Z ? in
     722    let bit_one ≝ get_index_v… nu one ? in
     723    let bit_two ≝ get_index_v… nu two ? in
     724    let bit_three ≝ get_index_v… nu three ? in
    725725      if bit_zero then
    726726        let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
     
    798798        λdirect: True.
    799799          let 〈 nu, nl 〉 ≝ split … four four d in
    800           let bit_one ≝ get_index_bv … nu one ? in
     800          let bit_one ≝ get_index_v … nu one ? in
    801801            match bit_one with
    802802              [ true ⇒
     
    810810          let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in
    811811          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    812           let bit_one ≝ get_index_bv … bit_one_v Z ? in
     812          let bit_one ≝ get_index_v … bit_one_v Z ? in
    813813          match bit_one with
    814814            [ true ⇒
     
    837837        λdirect: True.
    838838          let 〈 nu, nl 〉 ≝ split … four four d in
    839           let bit_one ≝ get_index_bv … nu one ? in
     839          let bit_one ≝ get_index_v … nu one ? in
    840840          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    841841            match bit_one with
     
    849849          let register ≝ get_register s [[ false; false; i ]] in
    850850          let 〈 nu, nl 〉 ≝ split ? four four register in
    851           let bit_one ≝ get_index_bv ? nu one ? in
     851          let bit_one ≝ get_index_v … nu one ? in
    852852          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    853853          match bit_one with
     
    909909        λbit_addr: True.
    910910          let 〈 nu, nl 〉 ≝ split … four four b in
    911           let bit_one ≝ get_index_bv … nu one ? in
     911          let bit_one ≝ get_index_v … nu one ? in
    912912          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    913913            match bit_one with
     
    918918                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
    919919                let sfr ≝ get_bit_addressable_sfr s ? trans l in
    920                   get_index_bv ? sfr m ?
     920                  get_index_v … sfr m ?
    921921              | false ⇒
    922922                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    923923                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
    924924                let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    925                   get_index_bv ? t (modulus address eight) ?
     925                  get_index_v … t (modulus address eight) ?
    926926              ]
    927927      | N_BIT_ADDR n ⇒
    928928        λn_bit_addr: True.
    929929          let 〈 nu, nl 〉 ≝ split … four four n in
    930           let bit_one ≝ get_index_bv … nu one ? in
     930          let bit_one ≝ get_index_v … nu one ? in
    931931          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    932932            match bit_one with
     
    937937                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
    938938                let sfr ≝ get_bit_addressable_sfr s ? trans l in
    939                   negation (get_index_bv ? sfr m ?)
     939                  negation (get_index_v … sfr m ?)
    940940              | false ⇒
    941941                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    942942                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
    943943                let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    944                   negation (get_index_bv ? trans (modulus address eight) ?)
     944                  negation (get_index_v … trans (modulus address eight) ?)
    945945              ]
    946946      | CARRY ⇒ λcarry: True. get_cy_flag s
     
    963963      [ BIT_ADDR b ⇒ λbit_addr: True.
    964964          let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    965           let bit_one ≝ get_index_bv ? nu one ? in
     965          let bit_one ≝ get_index_v … nu one ? in
    966966          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    967967          match bit_one with
     
    985985        λcarry: True.
    986986          let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    987           let bit_one ≝ get_index … nu one ? in
    988           let bit_two ≝ get_index … nu two ? in
    989           let bit_three ≝ get_index … nu three ? in
     987          let bit_one ≝ get_index_v… nu one ? in
     988          let bit_two ≝ get_index_v… nu two ? in
     989          let bit_three ≝ get_index_v… nu three ? in
    990990          let new_psw ≝ [[ v; bit_one ; bit_two; bit_three ]] @@ nl in
    991991            set_8051_sfr s SFR_PSW new_psw
Note: See TracChangeset for help on using the changeset viewer.