Changeset 1881


Ignore:
Timestamp:
Apr 6, 2012, 6:39:32 PM (8 years ago)
Author:
campbell
Message:

Resurrect version of exec_up_to which shows the final state.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Animation.ma

    r1876 r1881  
    5252| failed' : errmsg → nat → state → snapshot' state
    5353| 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)
     54
     55let rec up_to_nth_step' (n:nat) (total:nat) (state:Type[0]) (input:list eventval) (e:execution state io_out io_in) (prev:state) (t:trace) : snapshot' state
    5656match n with
    5757[ O ⇒ match e with [ e_step tr s _ ⇒ running' ? (t⧺tr) s
     
    5959                   | e_interact o k ⇒ failed' ? (msg StoppedMidIO) total prev
    6060                   | 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)
     61| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step' m total state input e' s (t⧺tr)
    6262                     | e_stop tr r m ⇒ finished' ? (minus total n) (t⧺tr) r m
    6363                     | e_interact o k ⇒
     
    6565                         [ nil ⇒ input_exhausted' ? t
    6666                         | cons h tl ⇒ match get_input o h with
    67                                        [ OK i ⇒ up_to_nth_step' m total ex tl (k i) prev t
     67                                       [ OK i ⇒ up_to_nth_step' m total state tl (k i) prev t
    6868                                       | Error m ⇒ failed' ? m (minus total n) prev
    6969                                       ]
     
    7373].
    7474
    75 definition exec_up_to' : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → snapshot' (state ?? fx) ≝
     75definition exec_up_to' : ∀fx:fullexec io_out io_in. ∀p:program ?? fx. nat → list eventval → snapshot' (state ?? fx (make_global … p)) ≝
    7676λfx,p,n,i.
    7777match 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
     78[ OK s ⇒ up_to_nth_step' n n (state ?? fx (make_global … p)) i (exec_inf ?? fx p) s E0
    7979| Error m ⇒ init_state_fail' ? m
    8080].
    81 *)
     81
    8282(* Provide an easy way to get a term in proof mode for reduction.
    8383   For example,
Note: See TracChangeset for help on using the changeset viewer.