source: Deliverables/D3.1/C-semantics/Animation.ma @ 492

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

Port Clight semantics to the new-new matita syntax.

File size: 1.9 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) (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.