Changeset 2617


Ignore:
Timestamp:
Feb 6, 2013, 5:03:14 PM (6 years ago)
Author:
campbell
Message:

Trivial simplification on split_trace.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Measurable.ma

    r2596 r2617  
    1515definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state).
    1616
    17 let rec split_trace FE (g:global io_out io_in FE) (x:execution (state ?? FE g) io_out io_in) (n:nat) on n : option (execution_prefix (state … FE g) × (execution (state ?? FE g) io_out io_in)) ≝
     17let rec split_trace (state:Type[0]) (x:execution state io_out io_in) (n:nat) on n : option (execution_prefix state × (execution state io_out io_in)) ≝
    1818match n with
    1919[ O ⇒ Some ? 〈[ ], x〉
     
    2121  match x with
    2222  [ e_step tr s x' ⇒
    23     ! 〈pre,x''〉 ← split_trace FE g x' n';
     23    ! 〈pre,x''〉 ← split_trace state x' n';
    2424    Some ? 〈〈tr,s〉::pre,x''〉
    2525    (* Necessary for a measurable trace at the end of the program *)
     
    102102  let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) (pcs_stack C stack_cost ?) in
    103103  let cl_trace ≝ exec_inf … (cs_exec … C') p in
    104   split_trace C' ? cl_trace m = Some ? 〈prefix,suffix〉 ∧
    105   split_trace C' ? suffix n = Some ? 〈interesting,remainder〉 ∧
     104  split_trace ? cl_trace m = Some ? 〈prefix,suffix〉 ∧
     105  split_trace ? suffix n = Some ? 〈interesting,remainder〉 ∧
    106106  trace_is_label_to_return C' interesting ∧
    107107  bool_to_Prop (will_return' C' interesting) ∧
     
    116116λFE,p,m,n.
    117117  let trace ≝ exec_inf … FE p in
    118   match split_trace FE ? trace m with
     118  match split_trace ? trace m with
    119119  [ Some x ⇒
    120120    let 〈prefix,suffix〉 ≝ x in
    121     match split_trace FE ? suffix n with
     121    match split_trace ? suffix n with
    122122    [ Some y ⇒
    123123      let interesting ≝ \fst y in
     
    131131λFE,p,m.
    132132  let trace ≝ exec_inf … FE p in
    133   match split_trace FE ? trace m with
     133  match split_trace ? trace m with
    134134  [ Some x ⇒
    135135    match \snd x with
Note: See TracChangeset for help on using the changeset viewer.