- Timestamp:
- Feb 6, 2013, 5:03:14 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Measurable.ma
r2596 r2617 15 15 definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state). 16 16 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)) ≝17 let 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)) ≝ 18 18 match n with 19 19 [ O ⇒ Some ? 〈[ ], x〉 … … 21 21 match x with 22 22 [ e_step tr s x' ⇒ 23 ! 〈pre,x''〉 ← split_trace FE gx' n';23 ! 〈pre,x''〉 ← split_trace state x' n'; 24 24 Some ? 〈〈tr,s〉::pre,x''〉 25 25 (* Necessary for a measurable trace at the end of the program *) … … 102 102 let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) (pcs_stack C stack_cost ?) in 103 103 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〉 ∧ 106 106 trace_is_label_to_return C' interesting ∧ 107 107 bool_to_Prop (will_return' C' interesting) ∧ … … 116 116 λFE,p,m,n. 117 117 let trace ≝ exec_inf … FE p in 118 match split_trace FE? trace m with118 match split_trace ? trace m with 119 119 [ Some x ⇒ 120 120 let 〈prefix,suffix〉 ≝ x in 121 match split_trace FE? suffix n with121 match split_trace ? suffix n with 122 122 [ Some y ⇒ 123 123 let interesting ≝ \fst y in … … 131 131 λFE,p,m. 132 132 let trace ≝ exec_inf … FE p in 133 match split_trace FE? trace m with133 match split_trace ? trace m with 134 134 [ Some x ⇒ 135 135 match \snd x with
Note: See TracChangeset
for help on using the changeset viewer.