source: src/Clight/Animation.ma @ 694

Last change on this file since 694 was 693, checked in by campbell, 10 years ago

Separate out whole program executions from the clight semantics and start
setting it up for RTLabs too.

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