Changeset 294


Ignore:
Timestamp:
Nov 25, 2010, 3:51:56 PM (9 years ago)
Author:
mulligan
Message:

get and set_arg_16 implemented.

File:
1 edited

Legend:

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

    r290 r294  
    669669    ##]
    670670nqed.
     671
     672include "ASM.ma".
     673
     674ndefinition set_arg_16: Status → Word → [[ dptr ]] → Status ≝
     675  λs,v,a.
     676   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with
     677     [ DPTR ⇒ λ_:True.
     678       let 〈 bu, bl 〉 ≝ split … eight eight v in
     679       let status ≝ set_8051_sfr s SFR_DPH bu in
     680       let status ≝ set_8051_sfr status SFR_DPL bl in
     681         status
     682     | _ ⇒ λK.
     683       match K in False with
     684       [
     685       ]
     686     ] (subaddressing_modein … a).
     687   
     688ndefinition get_arg_16: Status → [[ data16 ]] → Word ≝
     689  λs, a.
     690    match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
     691      [ DATA16 d ⇒ λ_:True. d
     692      | _ ⇒ λK.
     693        match K in False with
     694        [
     695        ]
     696      ] (subaddressing_modein … a).
Note: See TracChangeset for help on using the changeset viewer.