Changeset 1938 for src/common


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/common/StructuredTraces.ma

    r1935 r1938  
    44include "common/CostLabel.ma".
    55include "utilities/option.ma".
     6include "basics/lists/listb.ma".
    67include "ASM/Util.ma".
    7 include "ASM/Interpret.ma".
     8
     9inductive status_class : Type[0] ≝
     10| cl_return : status_class
     11| cl_jump   : status_class
     12| cl_call   : status_class
     13| cl_other : status_class.
    814
    915record abstract_status : Type[1] ≝
     
    1824  ; as_final: as_status → Prop
    1925}.
    20 
    21 definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
    22   λcode_memory.
    23   λcost_labels.
    24     mk_abstract_status
    25       (Status code_memory)
    26       (λs,s'. (execute_1 … s) = s')
    27       word_deqset
    28       (program_counter …)
    29       (λs,class. ASM_classify … s = class)
    30       (current_instruction_label code_memory cost_labels)
    31       (next_instruction_properly_relates_program_counters code_memory)
    32       ?.
    33   cases daemon (* XXX: is final predicate *)
    34 qed.
    3526
    3627(* temporary alias for backward compatibility *)
     
    442433  ].
    443434
    444 include "ASM/BitVectorTrie.ma".
    445 include "ASM/Status.ma".
    446 include "ASM/Fetch.ma".
    447 
    448435let rec as_compute_cost_trace_label_label
    449436  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
Note: See TracChangeset for help on using the changeset viewer.