Changeset 1921 for src/common


Ignore:
Timestamp:
May 8, 2012, 3:29:25 PM (8 years ago)
Author:
mulligan
Message:

Horror proof mostly finished (compiles all way until end of CostsProof?.ma).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1918 r1921  
    1212
    1313record abstract_status : Type[1] ≝
    14   { as_status :> Type[0]
     14{   
     15    as_status :> Type[0]
    1516  ; as_execute : as_status → as_status → Prop
    1617  ; as_pc : DeqSet
     
    112113 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
    113114 ].
     115 
     116definition as_trace_any_label_length':
     117    ∀S: abstract_status.
     118    ∀trace_ends_flag: trace_ends_with_ret.
     119    ∀start_status: S.
     120    ∀final_status: S.
     121    ∀the_trace: trace_any_label S trace_ends_flag start_status final_status.
     122      nat ≝
     123  λS: abstract_status.
     124  λtrace_ends_flag: trace_ends_with_ret.
     125  λstart_status: S.
     126  λfinal_status: S.
     127  λthe_trace: trace_any_label S trace_ends_flag start_status final_status.
     128    |tal_pc_list … the_trace|.
    114129
    115130let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝
     
    131146    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
    132147    tal_unrepeating … tl
     148  | tal_base_call status_pre_fun_call status_start_fun_call status_final _ _ _
     149      fun_call_trace _ ⇒ tlr_unrepeating … fun_call_trace
    133150  | _ ⇒ True
    134151  ].
Note: See TracChangeset for help on using the changeset viewer.