Changeset 2770


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...

Location:
src
Files:
6 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;
  • 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 ≝
  • 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
  • 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.
  • src/ASM/Status.ma

    r2757 r2770  
    33(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    44
    5 include "ASM/ASM.ma".
     5include "ASM/ASM.ma". (* includes "ASM/BitVectorTrie.ma".*)
    66include "ASM/Arithmetic.ma".
    7 include "ASM/BitVectorTrie.ma".
     7(*include "ASM/BitVectorTrie.ma".*)
    88include "basics/russell.ma".
    99
  • src/utilities/option.ma

    r2767 r2770  
     1include "basics/types.ma".
    12include "utilities/monad.ma".
    2 include "basics/types.ma".
    33
    44definition Option ≝ MakeMonadProps
Note: See TracChangeset for help on using the changeset viewer.