Changeset 2770 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Mar 3, 2013, 9:58:28 PM (7 years ago)
Author:
mckinna
Message:

WARNING: another big commit, touching many files in ASM/*.ma

This edit
a) prunes many redundant "include"s from ASM/*.ma hierarchy
b) adjusts the use of aliases from ASM/ and elsewhere (big, annoying, hard-to-debug disambiguation errors), from the earlier adjustment to ASM/ASM.ma
c) adds ONE (and once repeated) type annotation to ASM/Interpret.ma

As with the continual failures with Clight/switchRemoval.ma, the (revised) definition of execute_1_preinstruction causes no end of disambiguation thrashing. One type annotation (in the JMP case, to ensure that program_counter calculations actually produce values in Word) is enough to cut that particular Gordian knot. By russell-style reasoning, the annotation then gets repeated later, though in fact in that later instance is redundant...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r2760 r2770  
    1 include "basics/lists/listb.ma".
    2 include "ASM/StatusProofs.ma".
    3 include "ASM/Fetch.ma".
    4 include "ASM/AbstractStatus.ma".
     1
     2include "ASM/StatusProofs.ma". (* includes "basics/lists/listb.ma".*)
     3
     4include "ASM/AbstractStatus.ma". (* includes "ASM/Fetch.ma".*)
    55   
    66lemma execute_1_technical:
     
    6464qed.
    6565
     66(* JHM: order of includes changes *)
    6667include alias "ASM/Arithmetic.ma".
     68include alias "ASM/BitVectorTrie.ma".
    6769include alias "arithmetics/nat.ma".
    68 include alias "ASM/BitVectorTrie.ma".
    6970
    7071definition execute_1_preinstruction:
     
    190191          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
    191192          let jmp_addr ≝ add … big_acc dptr in
    192           let new_pc ≝ add … (program_counter … s) jmp_addr in
    193             set_program_counter … s new_pc
     193          let new_pc : Word ≝ add … (program_counter … s) jmp_addr in (* JHM: type annotation *)
     194            set_program_counter … s new_pc 
    194195        | NOP ⇒ λinstr_refl.
    195196           let s ≝ add_ticks1 s in
     
    617618          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
    618619          let jmp_addr ≝ add … big_acc dptr in
    619           let new_pc ≝ add … (program_counter … s) jmp_addr in
     620          let new_pc : Word ≝ add … (program_counter … s) jmp_addr in (* JHM: type annotation *)
    620621            set_program_counter … s new_pc
    621622        | NOP ⇒ λinstr_refl.
     
    10281029qed.
    10291030
     1031(* JHM: redundant includes
    10301032include alias "arithmetics/nat.ma".
    10311033include alias "ASM/BitVectorTrie.ma".
    10321034include alias "ASM/Vector.ma".
     1035*)
    10331036
    10341037definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
Note: See TracChangeset for help on using the changeset viewer.