source: src/common/Animation.ma @ 731

Last change on this file since 731 was 731, checked in by campbell, 9 years ago

Common definition for animation semantics, and factor out IO definitions.

File size: 2.5 KB
Line 
1
2include "common/IO.ma".
3include "common/SmallstepExec.ma".
4
5(* Functions to allow programs to be executed up to some number of steps, given
6   a predetermined set of input values.  Note that we throw away the state if
7   we stop at a continuation - it can be too large to work with. *)
8
9definition get_input : ∀o:io_out. eventval → res (io_in o) ≝
10λo,ev.
11match io_in_typ o return λt. res (eventval_type t) with
12[ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? ]
13| ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? ]
14| ASTptr _ ⇒ Error ?
15].
16
17inductive snapshot (state:Type[0]) : Type[0] ≝
18| running : trace → state → snapshot state
19| finished : trace → int → mem → snapshot state
20| input_exhausted : trace → snapshot state.
21
22let 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)) ≝
23match n with
24[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s)
25                   | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
26                   | _ ⇒ Error ? ]
27| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m ex input e' (t⧺tr)
28                     | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
29                     | e_interact o k ⇒
30                         match input with
31                         [ nil ⇒ OK ? (input_exhausted ? t)
32                         | cons h tl ⇒ do i ← get_input o h;
33                                       up_to_nth_step m ex tl (k i) t
34                         ]
35                     | e_wrong ⇒ Error ?
36                     ]
37].
38
39definition exec_up_to : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → res (snapshot (state ?? fx)) ≝
40λfx,p,n,i. up_to_nth_step n fx i (exec_inf ?? fx p) E0.
41
42(* Provide an easy way to get a term in proof mode for reduction.
43   For example,
44   
45   example exec: result ? (exec_up_to myprog 20 [EVint (repr 12)]).
46   normalize  (* you can examine the result here *)
47   % qed.
48   
49 *)
50
51inductive result (A:Type[0]) : A → Type[0] ≝
52| witness : ∀a:A. result A a.
53
54definition finishes_with : int → ∀S.res (snapshot S) → Prop ≝
55λr,S,s. match s with [ OK s' ⇒ match s' with [ finished t r' _ ⇒ r = r' | _ ⇒ False ] | _ ⇒ False ].
56
57(* Hide the representation of memory to make displaying the results easier. *)
58
59notation < "'MEM'" with precedence 1 for @{ 'mem }.
60interpretation "hide memory" 'mem = (mk_mem ???).
Note: See TracBrowser for help on using the repository browser.