Changeset 963 for src

Timestamp:

Jun 15, 2011, 4:15:55 PM (10 years ago)

Author:

campbell

Message:

Extra debugging aid for animation of semantics.

File:

• src/common/Animation.ma (modified) (2 diffs)

src/common/Animation.ma

@@ -2 +2 @@
 include "common/IO.ma".
 include "common/SmallstepExec.ma".
+include "arithmetics/nat.ma".
 
 (* 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.
 
+(* A version of exec_up_to that reports the state prior to failure. *)
+
+inductive snapshot' (state:Type[0]) : Type[0] ≝
+| running' : trace → state → snapshot' state
+| finished' : nat → trace → int → mem → snapshot' state
+| input_exhausted' : trace → snapshot' state
+| failed' : errmsg → nat → state → snapshot' state
+| init_state_fail' : errmsg → snapshot' state.
+
+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) ≝
+match n with
+[ O ⇒ match e with [ e_step tr s _ ⇒ running' ? (t⧺tr) s
+                   | e_stop tr r m ⇒ finished' ? total (t⧺tr) r m
+                   | e_interact o k ⇒ failed' ? (msg StoppedMidIO) total prev
+                   | e_wrong m ⇒ failed' ? m total prev ]
+| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step' m total ex input e' s (t⧺tr)
+                     | e_stop tr r m ⇒ finished' ? (minus total n) (t⧺tr) r m
+                     | e_interact o k ⇒ 
+                         match input with
+                         [ nil ⇒ input_exhausted' ? t
+                         | cons h tl ⇒ match get_input o h with
+                                       [ OK i ⇒ up_to_nth_step' m total ex tl (k i) prev t
+                                       | Error m ⇒ failed' ? m (minus total n) prev
+                                       ]
+                         ]
+                     | e_wrong m ⇒ failed' ? m (minus total n) prev
+                     ]
+].
+
+definition exec_up_to' : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → snapshot' (state ?? fx) ≝
+λfx,p,n,i. 
+match make_initial_state ?? fx p with
+[ OK gs ⇒ up_to_nth_step' n n fx i (exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)) (\snd gs) E0
+| Error m ⇒ init_state_fail' ? m
+].
+
 (* Provide an easy way to get a term in proof mode for reduction.
    For example,