Changeset 314


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

Finished all get_ and set_arg_* functions.

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

Legend:

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

    r313 r314  
    4444  λp: m < n.
    4545  λc: Bool.
    46     set_index_weak Bool n b m c.
     46    set_index Bool n b m c.
    4747   
    4848ndefinition drop ≝
  • Deliverables/D4.1/Matita/Status.ma

    r313 r314  
    33(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    44
    5 (* include "ASM.ma". *)
     5include "ASM.ma".
    66include "Arithmetic.ma".
    77include "BitVectorTrie.ma".
     
    691691    ##]
    692692nqed.
    693 
    694 include "ASM.ma".
    695693
    696694ndefinition set_arg_16: Status → Word → [[ dptr ]] → Status ≝
     
    783781nqed.
    784782
    785 (*
    786 ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
    787                        Bool → Bool ≝
    788   λs, a, l.
    789     match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
    790                                                  n_bit_addr ;
    791                                                  carry ]] x) → ? with
    792       [ BIT_ADDR b ⇒
    793         λbit_addr: True.
    794           let 〈 nu, nl 〉 ≝ split … four four b in
    795           let bit_one ≝ get_index … nu one ? in
    796           let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    797             match bit_one with
    798               [ true ⇒
    799                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    800                 let d ≝ address ÷ eight in
    801                 let m ≝ address mod eight in
    802                 let trans ≝ bitvector_of_nat ((d * eight) + one_hundred_and_twenty_eight) eight in
    803                 let sfr ≝ get_bit_addressable_sfr s ? trans l in
    804                   get_index ? sfr m ?
    805               | false ⇒
    806                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    807                 let address' ≝ bitvector_of_nat ((address ÷ eight) + thirty_two) seven in
    808                 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    809                   get_index ? t (modulus address eight) ?
    810               ]
    811       | N_BIT_ADDR n ⇒
    812         λn_bit_addr: True.
    813           let 〈 nu, nl 〉 ≝ split … four four n in
    814           let bit_one ≝ get_index … nu one ? in
    815           let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    816             match bit_one with
    817               [ true ⇒
    818                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    819                 let d ≝ address ÷ eight in
    820                 let m ≝ address mod eight in
    821                 let trans ≝ bitvector_of_nat ((d * eight) + one_hundred_and_twenty_eight) eight in
    822                 let sfr ≝ get_bit_addressable_sfr s ? trans l in
    823                   negation (get_index ? sfr m ?)
    824               | false ⇒
    825                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    826                 let address' ≝ bitvector_of_nat ((address ÷ eight) + thirty_two) seven in
    827                 let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    828                   negation (get_index ? trans (modulus address eight) ?)
    829               ]
    830       | CARRY ⇒ λcarry: True. get_cy_flag s
    831       | _ ⇒ λother.
    832         match other in False with [ ]
    833       ] (subaddressing_modein … a). *)
    834 
    835783ndefinition set_arg_8: Status → [[ direct ; indirect ; register ;
    836784                                   acc_a ; acc_b ; ext_indirect ;
     
    852800              ]
    853801      | INDIRECT i ⇒
    854         λindirect: True. ?
     802        λindirect: True.
     803          let register ≝ get_register s false false i in
     804          let 〈 nu, nl 〉 ≝ split ? four four register in
     805          let bit_one ≝ get_index ? nu one ? in
     806          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
     807          match bit_one with
     808            [ true ⇒
     809              let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
     810                set_low_internal_ram s memory
     811            | false ⇒
     812              let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in
     813                set_high_internal_ram s memory
     814            ]
    855815      | REGISTER r1 r2 r3 ⇒ λregister: True. set_register s r1 r2 r3 v
    856816      | ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v
     
    871831          match other in False with [ ]
    872832      ] (subaddressing_modein … a).
     833      ##[##1,2:
     834          nnormalize;
     835          nrepeat (napply less_than_or_equal_monotone);
     836          napply less_than_or_equal_zero
     837      ##]
     838nqed.
     839
     840naxiom modulus_less_than:
     841  ∀m,n: Nat.
     842    (m mod n) < n.
     843
     844ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
     845                       Bool → Bool ≝
     846  λs, a, l.
     847    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
     848                                                 n_bit_addr ;
     849                                                 carry ]] x) → ? with
     850      [ BIT_ADDR b ⇒
     851        λbit_addr: True.
     852          let 〈 nu, nl 〉 ≝ split … four four b in
     853          let bit_one ≝ get_index … nu one ? in
     854          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
     855            match bit_one with
     856              [ true ⇒
     857                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     858                let d ≝ address ÷ eight in
     859                let m ≝ address mod eight in
     860                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
     861                let sfr ≝ get_bit_addressable_sfr s ? trans l in
     862                  get_index ? sfr m ?
     863              | false ⇒
     864                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     865                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
     866                let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
     867                  get_index ? t (modulus address eight) ?
     868              ]
     869      | N_BIT_ADDR n ⇒
     870        λn_bit_addr: True.
     871          let 〈 nu, nl 〉 ≝ split … four four n in
     872          let bit_one ≝ get_index … nu one ? in
     873          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
     874            match bit_one with
     875              [ true ⇒
     876                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     877                let d ≝ address ÷ eight in
     878                let m ≝ address mod eight in
     879                let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
     880                let sfr ≝ get_bit_addressable_sfr s ? trans l in
     881                  negation (get_index ? sfr m ?)
     882              | false ⇒
     883                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     884                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
     885                let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
     886                  negation (get_index ? trans (modulus address eight) ?)
     887              ]
     888      | CARRY ⇒ λcarry: True. get_cy_flag s
     889      | _ ⇒ λother.
     890        match other in False with [ ]
     891      ] (subaddressing_modein … a).
     892      ##[##3,6:
     893          nnormalize;
     894          nrepeat (napply less_than_or_equal_monotone);
     895          napply less_than_or_equal_zero;
     896      ##|##1,2,4,5:
     897          napply modulus_less_than;
     898      ##]
     899nqed.
     900     
     901ndefinition set_arg_1: Status → [[ bit_addr ; carry ]] →
     902                       Bit → Status ≝
     903  λs, a, v.
     904    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with
     905      [ BIT_ADDR b ⇒ λbit_addr: True.
     906          let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
     907          let bit_one ≝ get_index ? nu one ? in
     908          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
     909          match bit_one with
     910            [ true ⇒
     911                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     912                let d ≝ address ÷ eight in
     913                let m ≝ address mod eight in
     914                let t ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
     915                let sfr ≝ get_bit_addressable_sfr s ? t true in
     916                let new_sfr ≝ set_index … sfr m v ? in
     917                  set_bit_addressable_sfr s new_sfr t
     918            | false ⇒
     919                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     920                let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
     921                let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
     922                let n_bit ≝ set_index … t (modulus address eight) v ? in
     923                let memory ≝ insert ? seven address' n_bit (low_internal_ram s) in
     924                  set_low_internal_ram s memory
     925            ]
     926      | CARRY ⇒
     927        λcarry: True.
     928          let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
     929          let bit_one ≝ get_index … nu one ? in
     930          let bit_two ≝ get_index … nu two ? in
     931          let bit_three ≝ get_index … nu three ? in
     932          let new_psw ≝ [[ v; bit_one ; bit_two; bit_three ]] @@ nl in
     933            set_8051_sfr s SFR_PSW new_psw
     934      | _ ⇒
     935        λother: False.
     936          match other in False with
     937            [ ]
     938      ] (subaddressing_modein … a).
     939      ##[##1,2,3,6:
     940          nnormalize;
     941          nrepeat (napply less_than_or_equal_monotone);
     942          napply less_than_or_equal_zero;
     943      ##|##4,5:
     944          napply (modulus_less_than address eight);
     945      ##]
     946nqed.
Note: See TracChangeset for help on using the changeset viewer.