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/AbstractStatus.ma

    r2705 r2770  
    1 include "ASM/ASM.ma".
    2 include "ASM/Status.ma".
     1include "common/StructuredTraces.ma". (* includes "basics/lists/listb.ma".*)
     2
     3include "ASM/Status.ma". (* includes "ASM/ASM.ma". *)
    34include "ASM/Fetch.ma".
    4 include "common/StructuredTraces.ma".
    5 
    6 include "basics/lists/listb.ma".
    75
    86definition ASM_classify00: ∀a. preinstruction a → status_class ≝
Note: See TracChangeset for help on using the changeset viewer.