source: src/common/Animation.ma @ 2548

Last change on this file since 2548 was 2533, checked in by campbell, 7 years ago

Some fall out from removing floats.

File size: 4.5 KB
Line 
1
2include "common/IO.ma".
3include "common/SmallstepExec.ma".
4include "arithmetics/nat.ma".
5
6(* Functions to allow programs to be executed up to some number of steps, given
7   a predetermined set of input values.  Note that we throw away the state if
8   we stop at a continuation - it can be too large to work with. *)
9
10definition get_input : ∀o:io_out. eventval → res (io_in o) ≝
11λo,ev.
12match io_in_typ o return λt. res (eventval_type t) with
13[ ASTint sz _ ⇒ match ev with [ EVint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.OK ? i) (Error ? (msg IllTypedEvent)) | _ ⇒ Error ? (msg IllTypedEvent) ]
14| ASTptr ⇒ Error ? (msg IllTypedEvent)
15].
16
17inductive snapshot (state:Type[0]) : Type[0] ≝
18| running : trace → state → snapshot state
19| finished : trace → int → state → snapshot state
20| input_exhausted : trace → snapshot state.
21
22axiom StoppedMidIO : String.
23
24let 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) ≝
25match n with
26[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s)
27                   | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
28                   | e_interact o k ⇒ Error ? (msg StoppedMidIO)
29                   | e_wrong m ⇒ Error ? m ]
30| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m state input e' (t⧺tr)
31                     | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
32                     | e_interact o k ⇒
33                         match input with
34                         [ nil ⇒ OK ? (input_exhausted ? t)
35                         | cons h tl ⇒ do i ← get_input o h;
36                                       up_to_nth_step m state tl (k i) t
37                         ]
38                     | e_wrong m ⇒ Error ? m
39                     ]
40].
41
42definition exec_up_to : ∀fx:fullexec io_out io_in. ∀p:program ?? fx. nat → list eventval → res (snapshot (state ?? fx (make_global … p))) ≝
43λfx,p,n,i. up_to_nth_step n ? i (exec_inf ?? fx p) E0.
44
45(* A version of exec_up_to that reports the state prior to failure. *)
46
47inductive snapshot' (state:Type[0]) : Type[0] ≝
48| running' : trace → state → snapshot' state
49| finished' : nat → trace → int → state → snapshot' state
50| input_exhausted' : trace → snapshot' state
51| failed' : errmsg → nat → state → snapshot' state
52| init_state_fail' : errmsg → snapshot' state.
53
54let 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 ≝
55match n with
56[ O ⇒ match e with [ e_step tr s _ ⇒ running' ? (t⧺tr) s
57                   | e_stop tr r m ⇒ finished' ? total (t⧺tr) r m
58                   | e_interact o k ⇒ failed' ? (msg StoppedMidIO) total prev
59                   | e_wrong m ⇒ failed' ? m total prev ]
60| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step' m total state input e' s (t⧺tr)
61                     | e_stop tr r m ⇒ finished' ? (minus total n) (t⧺tr) r m
62                     | e_interact o k ⇒
63                         match input with
64                         [ nil ⇒ input_exhausted' ? t
65                         | cons h tl ⇒ match get_input o h with
66                                       [ OK i ⇒ up_to_nth_step' m total state tl (k i) prev t
67                                       | Error m ⇒ failed' ? m (minus total n) prev
68                                       ]
69                         ]
70                     | e_wrong m ⇒ failed' ? m (minus total n) prev
71                     ]
72].
73
74definition exec_up_to' : ∀fx:fullexec io_out io_in. ∀p:program ?? fx. nat → list eventval → snapshot' (state ?? fx (make_global … p)) ≝
75λfx,p,n,i.
76match make_initial_state ?? fx p with
77[ OK s ⇒ up_to_nth_step' n n (state ?? fx (make_global … p)) i (exec_inf ?? fx p) s E0
78| Error m ⇒ init_state_fail' ? m
79].
80
81(* Provide an easy way to get a term in proof mode for reduction.
82   For example,
83   
84   example exec: result ? (exec_up_to myprog 20 [EVint (repr 12)]).
85   normalize  (* you can examine the result here *)
86   % qed.
87   
88 *)
89
90inductive result (A:Type[0]) : A → Type[0] ≝
91| witness : ∀a:A. result A a.
92
93inductive finishes_with : int → ∀S.res (snapshot S) → Prop ≝
94fw_ok : ∀r,S,t,s. finishes_with r S (OK ? (finished S t r s)).
95
96include "common/GenMem.ma".
97
98(* Hide the representation of memory to make displaying the results easier. *)
99
100notation < "'MEM'" with precedence 1 for @{ 'mem }.
101interpretation "hide memory" 'mem = (mk_mem ???).
Note: See TracBrowser for help on using the repository browser.