Changeset 1522 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Nov 21, 2011, 3:49:04 PM (8 years ago)
Author:
mulligan
Message:

changes to preamble and lin to asm pass, resolved conflict in interpret

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1519 r1522  
    1 include "ASM/Status.ma". 
     1include "ASM/Status.ma".
    22include "ASM/Fetch.ma".
    33
     
    4040   # H2
    4141   normalize
    42    change in H2: (??%?); with (orb ??)
     42   change with (orb ??) in H2: (??%?);
    4343   cases (inclusive_disjunction_true … H2)
    4444   [ # K
     
    8888     [ # K1
    8989       # _
    90        change in K1; with ((andb ? (subvector_with …)) = true)
     90       change with ((andb ? (subvector_with …)) = true) in K1;
    9191       cases (conjunction_true … K1)
    9292       # K3
     
    105105     | # K1
    106106       # K2
    107        (normalize in K2;)
     107       normalize in K2;
    108108       cases K2;
    109109     ]
     
    528528qed.
    529529
    530 definition execute_1_0: Status → instruction × Word × nat → Status ≝
     530include "ASM/JMCoercions.ma".
     531
     532definition execute_1_0: ∀s: Status. instruction × Word × nat → Σs': Status. clock … s ≤ clock … s' ≝
    531533  λs,instr_pc_ticks.
    532534    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
     
    541543        | _ ⇒ λabsd. ⊥
    542544        ] (subaddressing_modein … x)) instr s
     545      | _ ⇒ ?
     546      ] in s.
    543547      | ACALL addr ⇒
    544548          let s ≝ set_clock ? s (ticks + clock ? s) in
Note: See TracChangeset for help on using the changeset viewer.