Changeset 2770 for src/ASM/Fetch.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/Fetch.ma

    r2754 r2770  
    1 include "ASM/BitVectorTrie.ma".
     1(*include "ASM/BitVectorTrie.ma".*)
    22include "ASM/Arithmetic.ma".
    3 include "ASM/ASM.ma".
     3include "ASM/ASM.ma". (* includes "ASM/BitVectorTrie.ma". *)
    44include "basics/russell.ma".
    55
Note: See TracChangeset for help on using the changeset viewer.