Changeset 1944


Ignore:
Timestamp:
May 14, 2012, 7:56:15 PM (8 years ago)
Author:
sacerdot
Message:

common/StructuredTraces no longer depends on ASM/AbstractStatus (again)

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AbstractStatus.ma

    r1939 r1944  
    22include "ASM/Status.ma".
    33include "ASM/Fetch.ma".
     4include "common/StructuredTraces.ma".
    45
    56include "basics/lists/listb.ma".
    6 
    7 inductive status_class: Type[0] ≝
    8   | cl_return: status_class
    9   | cl_jump: status_class
    10   | cl_call: status_class
    11   | cl_other: status_class.
    127
    138definition ASM_classify00: ∀a. preinstruction a → status_class ≝
     
    7570  λs: Status code_memory.
    7671    ASM_classify0 (current_instruction … s).
    77 
    78 record abstract_status : Type[1] ≝
    79 {
    80     as_status :> Type[0]
    81   ; as_execute : as_status → as_status → Prop
    82   ; as_pc : DeqSet
    83   ; as_pc_of : as_status → as_pc
    84   ; as_classifier : as_status → status_class → Prop
    85   ; as_label : as_status → option costlabel
    86   ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
    87   ; as_final: as_status → Prop
    88 }.
  • src/common/StructuredTraces.ma

    r1939 r1944  
    66include "basics/lists/listb.ma".
    77include "ASM/Util.ma".
    8 include "ASM/AbstractStatus.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.
     14
     15record abstract_status : Type[1] ≝
     16{
     17    as_status :> Type[0]
     18  ; as_execute : as_status → as_status → Prop
     19  ; as_pc : DeqSet
     20  ; as_pc_of : as_status → as_pc
     21  ; as_classifier : as_status → status_class → Prop
     22  ; as_label : as_status → option costlabel
     23  ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
     24  ; as_final: as_status → Prop
     25}.
    926
    1027(* temporary alias for backward compatibility *)
     
    478495
    479496(* XXX: dependent type madness *)
    480 
     497(*
    481498let rec tll_rel_to_traces_same_cost
    482499  (S: abstract_status) (S': abstract_status)
     
    510527  cases daemon
    511528qed.
     529*)
Note: See TracChangeset for help on using the changeset viewer.