Ignore:
Timestamp:
Sep 20, 2011, 7:11:41 PM (9 years ago)
Author:
campbell
Message:

Change SmallstepExec? so that states can depend on global information.
Use less suggestive names for the transition system so that it's obvious
the global information isn't restricted to Genv.
Separate set up of global environment from initialisation so that it never
fails.
Some minimal changes to get Clight execution working; rest to follow.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Animation.ma

    r1213 r1231  
    2323axiom StoppedMidIO : String.
    2424
    25 let 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)) ≝
     25let rec up_to_nth_step (n:nat) (state:Type[0]) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (snapshot state) ≝
    2626match n with
    2727[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s)
     
    2929                   | e_interact o k ⇒ Error ? (msg StoppedMidIO)
    3030                   | e_wrong m ⇒ Error ? m ]
    31 | S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m ex input e' (t⧺tr)
     31| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m state input e' (t⧺tr)
    3232                     | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
    3333                     | e_interact o k ⇒
     
    3535                         [ nil ⇒ OK ? (input_exhausted ? t)
    3636                         | cons h tl ⇒ do i ← get_input o h;
    37                                        up_to_nth_step m ex tl (k i) t
     37                                       up_to_nth_step m state tl (k i) t
    3838                         ]
    3939                     | e_wrong m ⇒ Error ? m
     
    4141].
    4242
    43 definition exec_up_to : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → res (snapshot (state ?? fx)) ≝
    44 λfx,p,n,i. up_to_nth_step n fx i (exec_inf ?? fx p) E0.
     43definition exec_up_to : ∀fx:fullexec io_out io_in. ∀p:program ?? fx. nat → list eventval → res (snapshot (state ?? fx (make_global … p))) ≝
     44λfx,p,n,i. up_to_nth_step n ? i (exec_inf ?? fx p) E0.
    4545
    4646(* A version of exec_up_to that reports the state prior to failure. *)
     
    5252| failed' : errmsg → nat → state → snapshot' state
    5353| init_state_fail' : errmsg → snapshot' state.
    54 
     54(*
    5555let 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) ≝
    5656match n with
     
    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.