Changeset 1938 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
May 14, 2012, 10:05:36 AM (8 years ago)
Author:
sacerdot
Message:

Definitions moved to the right places, now everything compiles again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1935 r1938  
    44include "ASM/Interpret.ma".
    55include "common/StructuredTraces.ma".
     6
     7definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
     8  λcode_memory.
     9  λcost_labels.
     10    mk_abstract_status
     11      (Status code_memory)
     12      (λs,s'. (execute_1 … s) = s')
     13      word_deqset
     14      (program_counter …)
     15      (λs,class. ASM_classify … s = class)
     16      (current_instruction_label code_memory cost_labels)
     17      (next_instruction_properly_relates_program_counters code_memory)
     18      ?.
     19  cases daemon (* XXX: is final predicate *)
     20qed.
    621
    722definition trace_any_label_length ≝
Note: See TracChangeset for help on using the changeset viewer.