- Timestamp:
- Jun 15, 2011, 4:15:55 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Animation.ma
r961 r963 2 2 include "common/IO.ma". 3 3 include "common/SmallstepExec.ma". 4 include "arithmetics/nat.ma". 4 5 5 6 (* Functions to allow programs to be executed up to some number of steps, given … … 43 44 λfx,p,n,i. up_to_nth_step n fx i (exec_inf ?? fx p) E0. 44 45 46 (* A version of exec_up_to that reports the state prior to failure. *) 47 48 inductive snapshot' (state:Type[0]) : Type[0] ≝ 49 | running' : trace → state → snapshot' state 50 | finished' : nat → trace → int → mem → snapshot' state 51 | input_exhausted' : trace → snapshot' state 52 | failed' : errmsg → nat → state → snapshot' state 53 | init_state_fail' : errmsg → snapshot' state. 54 55 let rec up_to_nth_step' (n:nat) (total:nat) (ex:execstep io_out io_in) (input:list eventval) (e:execution (state ?? ex) io_out io_in) (prev:state ?? ex) (t:trace) : snapshot' (state ?? ex) ≝ 56 match n with 57 [ O ⇒ match e with [ e_step tr s _ ⇒ running' ? (t⧺tr) s 58 | e_stop tr r m ⇒ finished' ? total (t⧺tr) r m 59 | e_interact o k ⇒ failed' ? (msg StoppedMidIO) total prev 60 | e_wrong m ⇒ failed' ? m total prev ] 61 | S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step' m total ex input e' s (t⧺tr) 62 | e_stop tr r m ⇒ finished' ? (minus total n) (t⧺tr) r m 63 | e_interact o k ⇒ 64 match input with 65 [ nil ⇒ input_exhausted' ? t 66 | cons h tl ⇒ match get_input o h with 67 [ OK i ⇒ up_to_nth_step' m total ex tl (k i) prev t 68 | Error m ⇒ failed' ? m (minus total n) prev 69 ] 70 ] 71 | e_wrong m ⇒ failed' ? m (minus total n) prev 72 ] 73 ]. 74 75 definition exec_up_to' : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → snapshot' (state ?? fx) ≝ 76 λfx,p,n,i. 77 match make_initial_state ?? fx p with 78 [ OK gs ⇒ up_to_nth_step' n n fx i (exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)) (\snd gs) E0 79 | Error m ⇒ init_state_fail' ? m 80 ]. 81 45 82 (* Provide an easy way to get a term in proof mode for reduction. 46 83 For example,
Note: See TracChangeset
for help on using the changeset viewer.