Ignore:
Timestamp:
Apr 1, 2011, 1:35:18 PM (9 years ago)
Author:
campbell
Message:

Common definition for animation semantics, and factor out IO definitions.

File:
1 moved

Legend:

Unmodified
Added
Removed
  • src/common/Animation.ma

    r730 r731  
    11
    2 include "Clight/Cexec.ma".
     2include "common/IO.ma".
     3include "common/SmallstepExec.ma".
    34
    45(* Functions to allow programs to be executed up to some number of steps, given
     
    1415].
    1516
    16 let rec up_to_nth_step (n:nat) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (trace × state) ≝
     17inductive snapshot (state:Type[0]) : Type[0] ≝
     18| running : trace → state → snapshot state
     19| finished : trace → int → mem → snapshot state
     20| input_exhausted : trace → snapshot state.
     21
     22let rec up_to_nth_step (n:nat) (ex:execstep io_out io_in) (input:list eventval) (e:execution (state ?? ex) io_out io_in) (t:trace) : res (snapshot (state ?? ex)) ≝
    1723match n with
    18 [ O ⇒ match e with [ e_step tr s _ ⇒ OK ? 〈t⧺tr, s〉
    19                    | e_stop tr r m ⇒ OK ? 〈t⧺tr, Returnstate (Vint r) Kstop m〉
     24[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s)
     25                   | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
    2026                   | _ ⇒ Error ? ]
    21 | S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m input e' (t⧺tr)
    22                      | e_stop tr r m ⇒ OK ? 〈t⧺tr, Returnstate (Vint r) Kstop m〉
     27| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m ex input e' (t⧺tr)
     28                     | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
    2329                     | e_interact o k ⇒
    2430                         match input with
    25                          [ nil ⇒ Error ?
     31                         [ nil ⇒ OK ? (input_exhausted ? t)
    2632                         | cons h tl ⇒ do i ← get_input o h;
    27                                        up_to_nth_step m tl (k i) t
     33                                       up_to_nth_step m ex tl (k i) t
    2834                         ]
    2935                     | e_wrong ⇒ Error ?
     
    3137].
    3238
    33 definition exec_up_to : clight_program → nat → list eventval → res (trace × state) ≝
    34 λp,n,i. up_to_nth_step n i (exec_inf p) E0.
     39definition exec_up_to : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → res (snapshot (state ?? fx)) ≝
     40λfx,p,n,i. up_to_nth_step n fx i (exec_inf ?? fx p) E0.
    3541
    3642(* Provide an easy way to get a term in proof mode for reduction.
     
    4652| witness : ∀a:A. result A a.
    4753
     54definition finishes_with : int → ∀S.res (snapshot S) → Prop ≝
     55λr,S,s. match s with [ OK s' ⇒ match s' with [ finished t r' _ ⇒ r = r' | _ ⇒ False ] | _ ⇒ False ].
     56
    4857(* Hide the representation of memory to make displaying the results easier. *)
    4958
Note: See TracChangeset for help on using the changeset viewer.