Changeset 310


Ignore:
Timestamp:
Nov 26, 2010, 11:26:26 AM (9 years ago)
Author:
mulligan
Message:

Most of get_arg_16 done.

File:
1 edited

Legend:

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

    r294 r310  
    695695        ]
    696696      ] (subaddressing_modein … a).
     697     
     698naxiom half_add:
     699  ∀n: Nat.
     700  ∀b, c: BitVector n.
     701    BitVector n × Bool.
     702     
     703ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ;
     704                                          acc_a ; acc_b ; data ; acc_dptr ;
     705                                          acc_pc ; ext_indirect ;
     706                                          ext_indirect_dptr ]] → Byte ≝
     707  λs, l, a.
     708    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
     709                                                acc_a ; acc_b ; data ; acc_dptr ;
     710                                                acc_pc ; ext_indirect ;
     711                                                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
     716      | EXT_INDIRECT_DPTR ⇒
     717        λK: True.
     718          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
     719            lookup … sixteen address (external_ram s) (zero eight)
     720      | EXT_INDIRECT e ⇒
     721        λK: True.
     722          let address ≝ get_register s false false e in
     723          let padded_address ≝ pad eight eight address in
     724            lookup … sixteen padded_address (external_ram s)
     725      | ACC_DPTR ⇒
     726        λK: True.
     727          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
     728          let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
     729          let 〈 address, carry 〉 ≝ half_add sixteen dptr padded_acc in
     730            lookup … sixteen address (external_ram s) (zero eight)
     731      | ACC_PC ⇒
     732        λK: True.
     733          let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
     734          let 〈 address, carry 〉 ≝ half_add sixteen (program_counter s) padded_acc in
     735            lookup … sixteen address (external_ram s) (zero eight)
     736      | DIRECT d ⇒
     737        λK: True.
     738          ?
     739      | INDIRECT i ⇒
     740        λK: True. ?
     741      | _ ⇒ λK. ?
     742      ] (subaddressing_modein … a).
     743      nauto;
     744nqed.
Note: See TracChangeset for help on using the changeset viewer.