Ignore:
Timestamp:
Mar 1, 2013, 1:05:21 PM (7 years ago)
Author:
sacerdot
Message:

WARNING: this commit breaks things, sorry, Paolo is going to fix compiler.ma
in a minute...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r2755 r2756  
    1  include "basics/types.ma".
    21include "basics/bool.ma".
    32include "basics/jmeq.ma".
     
    54include "utilities/option.ma".
    65include "basics/lists/listb.ma".
    7 include "ASM/Util.ma".
    86include "common/IO.ma".
    97include "utilities/hide.ma".
     8include "ASM/Util.ma".
    109
    1110inductive status_class: Type[0] ≝
     
    1918  { as_status :> Type[0]
    2019  ; as_eval : as_status → IO io_out io_in as_status
     20  ; as_init : res as_status
    2121  ; as_pc : DeqSet
    2222  ; as_pc_of : as_status → as_pc
    23   ; as_classify : as_status → option status_class
     23  ; as_classify : as_status → status_class
    2424  ; as_label_of_pc : as_pc → option costlabel
    25   ; as_after_return : (Σs:as_status. as_classify s = Some ? cl_call) → as_status → Prop
     25  ; as_after_return : (Σs:as_status. as_classify s = cl_call) → as_status → Prop
    2626  ; as_result: as_status → option int
    27   ; as_call_ident : (Σs:as_status.as_classify s = Some ? cl_call) → ident
    28   ; as_tailcall_ident : (Σs:as_status.as_classify s = Some ? cl_tailcall) → ident
     27  ; as_call_ident : (Σs:as_status.as_classify s = cl_call) → ident
     28  ; as_tailcall_ident : (Σs:as_status.as_classify s = cl_tailcall) → ident
    2929  }.
    3030
    31 definition as_classifier ≝ λS,s,cl.as_classify S s = Some ? cl.
     31definition as_classifier ≝ λS,s,cl.as_classify S s = cl.
    3232definition as_call ≝ λS,s,f.as_call_ident S s = f.
    3333definition as_final ≝ λS,s.as_result S s ≠ None ?.
Note: See TracChangeset for help on using the changeset viewer.