Changeset 911 for src/ASM/Status.ma


Ignore:
Timestamp:
Jun 9, 2011, 10:38:21 AM (9 years ago)
Author:
sacerdot
Message:

Type of set_code_memory generalized.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r843 r911  
    305305               
    306306definition set_code_memory ≝
    307   λM: Type[0].
    308   λs: PreStatus M.
    309   λr: M.
     307  λM,M': Type[0].
     308  λs: PreStatus M.
     309  λr: M'.
    310310    let old_low_internal_ram ≝ low_internal_ram ? s in
    311311    let old_high_internal_ram ≝ high_internal_ram ? s in
     
    317317    let old_p3_latch ≝ p3_latch ? s in
    318318    let old_clock ≝ clock ? s in
    319       mk_PreStatus M r
     319      mk_PreStatus M' r
    320320                old_low_internal_ram
    321321                old_high_internal_ram
     
    10761076 λl.
    10771077 λstatus.
    1078    set_code_memory ? status (load_code_memory l).
     1078   set_code_memory (BitVectorTrie Word 16) ? status (load_code_memory l).
    10791079
    10801080definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝
Note: See TracChangeset for help on using the changeset viewer.