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

    r2760 r2770  
     1(* JHM: redundant includes
    12include "ASM/ASM.ma".
    23include "ASM/Arithmetic.ma".
    3 include "ASM/Fetch.ma".
    4 include "ASM/Interpret.ma". (* includes ASM/AbstractStatus.ma *)
    5 
    6 (*include "common/StructuredTraces.ma". (* already included by ASM/AbstractStatus.ma *) *)
    7 
    8 (* could this definition be moved to ASM/AbstractStatus.ma ???
    9    no: requires ASM/Interpret/execute_1 *)
     4include "ASM/Fetch.ma".     (* includes ASM/ASM.ma and ASM/Arithmetic.ma *)
     5*)
     6
     7include "ASM/Interpret.ma". (* includes ASM/Fetch.ma and ASM/AbstractStatus.ma *)
     8
     9(*include "common/StructuredTraces.ma". (* included by ASM/AbstractStatus.ma *) *)
    1010
    1111definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
     
    2525  cases daemon (* XXX: is_final predicate, (tail)call_ident function *)
    2626qed.
    27 
    28 lemma Some_inv : ∀A.∀a,b. Some A a = Some A b → a = b.
    29   #A#a #b #eq destruct //
    30   qed.
    3127
    3228definition trace_any_label_length ≝
     
    311307        #None_lookup_opt_assm normalize nodelta #_
    312308        generalize in match recursive_assm;
    313         (*lapply (execute_1_and_program_counter_after_other_in_lockstep0 code_memory' ? (Some_inv … classifier_assm))*)
    314309        lapply (execute_1_and_program_counter_after_other_in_lockstep … classifier_assm)
    315310        <FETCH normalize nodelta #rewrite_assm >rewrite_assm in None_lookup_opt_assm;
Note: See TracChangeset for help on using the changeset viewer.