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

Tidy up measurable a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r2487 r2618  
    355355
    356356
     357
     358
     359definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state).
     360
     361let rec split_trace O I (state:Type[0]) (x:execution state O I) (n:nat) on n : option (execution_prefix state × (execution state O I)) ≝
     362match n with
     363[ O ⇒ Some ? 〈[ ], x〉
     364| S n' ⇒
     365  match x with
     366  [ e_step tr s x' ⇒
     367    ! 〈pre,x''〉 ← split_trace ?? state x' n';
     368    Some ? 〈〈tr,s〉::pre,x''〉
     369    (* Necessary for a measurable trace at the end of the program *)
     370  | e_stop tr r s ⇒
     371    match n' with
     372    [ O ⇒ Some ? 〈[〈tr,s〉], x〉
     373    | _ ⇒ None ?
     374    ]
     375  | _ ⇒ None ?
     376  ]
     377].
     378
     379
Note: See TracChangeset for help on using the changeset viewer.