Changeset 963 for src/common


Ignore:
Timestamp:
Jun 15, 2011, 4:15:55 PM (9 years ago)
Author:
campbell
Message:

Extra debugging aid for animation of semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Animation.ma

    r961 r963  
    22include "common/IO.ma".
    33include "common/SmallstepExec.ma".
     4include "arithmetics/nat.ma".
    45
    56(* Functions to allow programs to be executed up to some number of steps, given
     
    4344λfx,p,n,i. up_to_nth_step n fx i (exec_inf ?? fx p) E0.
    4445
     46(* A version of exec_up_to that reports the state prior to failure. *)
     47
     48inductive 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
     55let 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) ≝
     56match 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
     75definition exec_up_to' : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → snapshot' (state ?? fx) ≝
     76λfx,p,n,i.
     77match 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
    4582(* Provide an easy way to get a term in proof mode for reduction.
    4683   For example,
Note: See TracChangeset for help on using the changeset viewer.