Changeset 1944 for src/common


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.