source: src/Clight/Animation.ma @ 718

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

Add an AST type (i.e., intermediate language type) for pointers.

File size: 2.0 KB
Line 
1
2include "Clight/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| ASTptr _ ⇒ Error ?
14].
15
16let rec up_to_nth_step (n:nat) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (trace × state) ≝
17match n with
18[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? 〈t⧺tr, s〉
19                   | e_stop tr r m ⇒ OK ? 〈t⧺tr, Returnstate (Vint r) Kstop m〉
20                   | _ ⇒ Error ? ]
21| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m input e' (t⧺tr)
22                     | e_stop tr r m ⇒ OK ? 〈t⧺tr, Returnstate (Vint r) Kstop m〉
23                     | e_interact o k ⇒
24                         match input with
25                         [ nil ⇒ Error ?
26                         | cons h tl ⇒ do i ← get_input o h;
27                                       up_to_nth_step m tl (k i) t
28                         ]
29                     | e_wrong ⇒ Error ?
30                     ]
31].
32
33definition exec_up_to : clight_program → nat → list eventval → res (trace × state) ≝
34λp,n,i. up_to_nth_step n i (exec_inf p) E0.
35
36(* Provide an easy way to get a term in proof mode for reduction.
37   For example,
38   
39   example exec: result ? (exec_up_to myprog 20 [EVint (repr 12)]).
40   normalize  (* you can examine the result here *)
41   % qed.
42   
43 *)
44
45inductive result (A:Type[0]) : A → Type[0] ≝
46| witness : ∀a:A. result A a.
47
48(* Hide the representation of memory to make displaying the results easier. *)
49
50notation < "'MEM'" with precedence 1 for @{ 'mem }.
51interpretation "hide memory" 'mem = (mk_mem ???).
Note: See TracBrowser for help on using the repository browser.