Changeset 343 for Deliverables


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

Fixed Status.ma so that it compiles.

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

Legend:

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

    r337 r343  
    9494(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    9595   
    96 ndefinition conjunction
     96ndefinition conjunction_bv
    9797  λn: Nat.
    9898  λb: BitVector n.
     
    102102interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c).
    103103   
    104 ndefinition inclusive_disjunction
     104ndefinition inclusive_disjunction_bv
    105105  λn: Nat.
    106106  λb: BitVector n.
     
    111111  'inclusive_disjunction b c = (inclusive_disjunction ? b c).
    112112         
    113 ndefinition exclusive_disjunction
     113ndefinition exclusive_disjunction_bv
    114114  λn: Nat.
    115115  λb: BitVector n.
  • Deliverables/D4.1/Matita/Interpret.ma

    r341 r343  
    4545            let s ≝ set_arg_8 s ACC_A result in
    4646              set_flags s cy_flag (Just Bit ac_flag) ov_flag
     47        | ANL addr ⇒
     48          match addr with
     49            [ Left l ⇒
     50              match l with
     51                [ Left l' ⇒
     52                  let 〈addr1, addr2〉 ≝ l' in
     53                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
     54                    set_arg_8 s addr1 and_val
     55                | Right r ⇒
     56                  let 〈addr1, addr2〉 ≝ r in
     57                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
     58                    set_arg_8 s addr1 and_val
     59                ]
     60            | Right r ⇒
     61              let 〈addr1, addr2〉 ≝ r in
     62              let and_val ≝ conjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
     63                set_flags s and_val (Nothing ?) (get_ov_flag s)
     64            ]
     65        | ORL addr ⇒
     66          match addr with
     67            [ Left l ⇒
     68              match l with
     69                [ Left l' ⇒
     70                  let 〈addr1, addr2〉 ≝ l' in
     71                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
     72                    set_arg_8 s addr1 or_val
     73                | Right r ⇒
     74                  let 〈addr1, addr2〉 ≝ r in
     75                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
     76                    set_arg_8 s addr1 or_val
     77                ]
     78            | Right r ⇒
     79              let 〈addr1, addr2〉 ≝ r in
     80              let or_val ≝ inclusive_disjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
     81                set_flags s or_val (Nothing ?) (get_ov_flag s)
     82            ]
     83        | XRL addr ⇒
     84          match addr with
     85            [ Left l' ⇒
     86              let 〈addr1, addr2〉 ≝ l' in
     87              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
     88                set_arg_8 s addr1 xor_val
     89            | Right r ⇒
     90              let 〈addr1, addr2〉 ≝ r in
     91              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
     92                set_arg_8 s addr1 xor_val
     93            ]
    4794        | INC addr ⇒
    4895            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
     
    185232            let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
    186233              set_arg_8 s addr2 new_arg
     234        | RET ⇒
     235            let high_bits ≝ read_at_stack_pointer s in
     236            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
     237            let s ≝ set_8051_sfr s SFR_SP new_sp in
     238            let low_bits ≝ read_at_stack_pointer s in
     239            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
     240            let s ≝ set_8051_sfr s SFR_SP new_sp in
     241            let new_pc ≝ high_bits @@ low_bits in
     242              set_program_counter s new_pc
     243        | RETI ⇒
     244            let high_bits ≝ read_at_stack_pointer s in
     245            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
     246            let s ≝ set_8051_sfr s SFR_SP new_sp in
     247            let low_bits ≝ read_at_stack_pointer s in
     248            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
     249            let s ≝ set_8051_sfr s SFR_SP new_sp in
     250            let new_pc ≝ high_bits @@ low_bits in
     251              set_program_counter s new_pc
    187252        | Jump j ⇒
    188253          match j with
     
    258323                | _ ⇒ λother: False. ?
    259324                ] (subaddressing_modein … addr)
    260             | CJNE addr1 addr2 ⇒ ?
    261               match addr1 with
    262                 [ Left l ⇒ ?
    263                 | Right r ⇒ ?
    264                 ]
     325            | CJNE addr1 addr2 ⇒
     326              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     327                [ RELATIVE r ⇒ λrelative: True.
     328                  match addr1 with
     329                    [ Left l ⇒
     330                        let 〈addr1, addr2〉 ≝ l in
     331                        let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
     332                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
     333                          if negation (eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
     334                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     335                            let s ≝ set_program_counter s new_pc in
     336                              set_flags s new_cy (Nothing ?) (get_ov_flag s)
     337                          else
     338                            (set_flags s new_cy (Nothing ?) (get_ov_flag s))
     339                    | Right r' ⇒
     340                        let 〈addr1, addr2〉 ≝ r' in
     341                        let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
     342                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
     343                          if negation (eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
     344                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     345                            let s ≝ set_program_counter s new_pc in
     346                              set_flags s new_cy (Nothing ?) (get_ov_flag s)
     347                          else
     348                            (set_flags s new_cy (Nothing ?) (get_ov_flag s))
     349                    ]
     350                | _ ⇒ λother: False. ?
     351                ] (subaddressing_modein … addr2)
    265352            | DJNZ addr1 addr2 ⇒
    266353              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     
    276363                ] (subaddressing_modein … addr2)
    277364            ]
     365        | JMP _ ⇒ (* DPM: always indirect_dptr *)
     366          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
     367          let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
     368          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
     369          let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
     370            set_program_counter s new_pc
     371        | LJMP addr ⇒
     372          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
     373            [ ADDR16 a ⇒ λaddr16: True.
     374                set_program_counter s a
     375            | _ ⇒ λother: False. ?
     376            ] (subaddressing_modein … addr)
     377        | SJMP addr ⇒
     378          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     379            [ RELATIVE r ⇒ λrelative: True.
     380                let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     381                  set_program_counter s new_pc
     382            | _ ⇒ λother: False. ?
     383            ] (subaddressing_modein … addr)
     384        | AJMP addr ⇒
     385          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
     386            [ ADDR11 a ⇒ λaddr11: True.
     387              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
     388              let 〈nu, nl〉 ≝ split ? four four pc_bu in
     389              let bit ≝ cic:/matita/ng/Vector/get_index.fix(0,3,2) ? ? nl Z ? in
     390              let 〈relevant1, relevant2〉 ≝ split ? three eight a in
     391              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
     392              let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
     393                set_program_counter s new_pc
     394            | _ ⇒ λother: False. ?
     395            ] (subaddressing_modein … addr)
     396        | MOVC addr1 addr2 ⇒
     397          match addr2 return λx. bool_to_Prop (is_in [[ acc_dptr; acc_pc ]] x) → ? with
     398            [ ACC_DPTR ⇒ λacc_dptr: True. ?
     399            | ACC_PC ⇒ λacc_pc: True. ?
     400            | _ ⇒ λother: False. ?
     401            ] (subaddressing_modein … ?)
    278402        | NOP ⇒ s
    279403        | _ ⇒ s
  • Deliverables/D4.1/Matita/Nat.ma

    r330 r343  
    229229
    230230naxiom greater_than_b: Nat → Nat → Bool.
     231naxiom less_than_b: Nat → Nat → Bool.
    231232
    232233naxiom succ_less_than_injective:
  • 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.