Changeset 1939 for src/common


Ignore:
Timestamp:
May 14, 2012, 10:37:08 AM (8 years ago)
Author:
mulligan
Message:

Changes to get things to compile and to avoid the dependency circularity between ASM/Interpret.ma and common/StructuredTraces.ma. New file ASM/AbstractStatus.ma factors out the definition (not the implementation!) of an abstract status, which both of the previously mentioned files require.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1938 r1939  
    66include "basics/lists/listb.ma".
    77include "ASM/Util.ma".
    8 
    9 inductive 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 
    15 record 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 }.
     8include "ASM/AbstractStatus.ma".
    269
    2710(* temporary alias for backward compatibility *)
     
    436419  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
    437420    (start_status: S) (final_status: S)
     421     
    438422      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
    439423        on the_trace: list (Σl: costlabel. ∃s. as_label S s = Some … l) ≝
     
    492476  ]
    493477qed.
     478
     479(* XXX: dependent type madness *)
     480
     481let rec tll_rel_to_traces_same_cost
     482  (S: abstract_status) (S': abstract_status)
     483    (trace_ends_flag_l: trace_ends_with_ret) (trace_ends_flag_r: trace_ends_with_ret)
     484    (start_status_l: S) (final_status_l: S) (start_status_r: S') (final_status_r: S')
     485      (the_trace_l: trace_label_label S trace_ends_flag_l start_status_l final_status_l)
     486        (the_trace_r: trace_label_label S' trace_ends_flag_r start_status_r final_status_r)
     487          on the_trace_l:
     488            tll_rel … the_trace_l the_trace_r →
     489              as_compute_cost_trace_label_label … the_trace_l =
     490                as_compute_cost_trace_label_label S' trace_ends_flag_r ? ? the_trace_r ≝ ?.
     491and tal_rel_to_traces_same_cost
     492  (S: abstract_status) (S': abstract_status) (trace_ends_flag_l: trace_ends_with_ret)
     493    (trace_ends_flag_r: trace_ends_with_ret)
     494      (start_status_l: S) (final_status_l: S) (start_status_r: S') (final_status_r: S')
     495        (the_trace_l: trace_any_label S trace_ends_flag_l start_status_l final_status_l)
     496          (the_trace_r: trace_any_label S' trace_ends_flag_r start_status_r final_status_r)
     497          on the_trace_l:
     498            tal_rel … the_trace_l the_trace_r →
     499              as_compute_cost_trace_any_label … the_trace_l =
     500                as_compute_cost_trace_any_label … the_trace_r ≝ ?
     501and tlr_rel_to_traces_same_cost
     502  (S: abstract_status) (S': abstract_status) (start_status_l: S) (final_status_l: S)
     503    (start_status_r: S') (final_status_r: S')
     504      (the_trace_l: trace_label_return S start_status_l final_status_l)
     505        (the_trace_r: trace_label_return S' start_status_r final_status_r)
     506        on the_trace_l:
     507          tlr_rel … the_trace_l the_trace_r →
     508            as_compute_cost_trace_label_return … the_trace_l =
     509              as_compute_cost_trace_label_return … the_trace_r ≝ ?.
     510  cases daemon
     511qed.
Note: See TracChangeset for help on using the changeset viewer.