Changeset 2617 for src

Timestamp:

Feb 6, 2013, 5:03:14 PM (7 years ago)

Author:

campbell

Message:

Trivial simplification on split_trace.

File:

• src/common/Measurable.ma (modified) (5 diffs)

src/common/Measurable.ma

@@ -15 +15 @@
 definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state).
 
-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)) ≝
+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)) ≝
 match n with
 [ O ⇒ Some ? 〈[ ], x〉
@@ -21 +21 @@
   match x with
   [ e_step tr s x' ⇒
-    ! 〈pre,x''〉 ← split_trace FE g x' n';
+    ! 〈pre,x''〉 ← split_trace state x' n';
     Some ? 〈〈tr,s〉::pre,x''〉
     (* 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
   let cl_trace ≝ exec_inf … (cs_exec … C') p in
-  split_trace C' ? cl_trace m = Some ? 〈prefix,suffix〉 ∧ 
-  split_trace C' ? suffix n = Some ? 〈interesting,remainder〉 ∧
+  split_trace ? cl_trace m = Some ? 〈prefix,suffix〉 ∧ 
+  split_trace ? suffix n = Some ? 〈interesting,remainder〉 ∧
   trace_is_label_to_return C' interesting ∧
   bool_to_Prop (will_return' C' interesting) ∧
@@ -116 +116 @@
 λFE,p,m,n.
   let trace ≝ exec_inf … FE p in
-  match split_trace FE ? trace m with
+  match split_trace ? trace m with
   [ Some x ⇒
     let 〈prefix,suffix〉 ≝ x in
-    match split_trace FE ? suffix n with
+    match split_trace ? suffix n with
     [ Some y ⇒
       let interesting ≝ \fst y in
@@ -131 +131 @@
 λFE,p,m.
   let trace ≝ exec_inf … FE p in
-  match split_trace FE ? trace m with
+  match split_trace ? trace m with
   [ Some x ⇒
     match \snd x with