[409] | 1 | |
---|

| 2 | include "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 | |
---|

[487] | 8 | definition get_input : ∀o:io_out. eventval → res (io_in o) ≝ |
---|

[409] | 9 | λo,ev. |
---|

| 10 | match io_in_typ o return λt. res (eventval_type t) with |
---|

[478] | 11 | [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? ] |
---|

| 12 | | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? ] |
---|

[409] | 13 | ]. |
---|

| 14 | |
---|

[693] | 15 | let rec up_to_nth_step (n:nat) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (trace × state) ≝ |
---|

[409] | 16 | match 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 | |
---|

[487] | 32 | definition exec_up_to : clight_program → nat → list eventval → res (trace × state) ≝ |
---|

[409] | 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 | |
---|

[487] | 38 | example exec: result ? (exec_up_to myprog 20 [EVint (repr 12)]). |
---|

| 39 | normalize (* you can examine the result here *) |
---|

| 40 | % qed. |
---|

[409] | 41 | |
---|

| 42 | *) |
---|

| 43 | |
---|

[487] | 44 | inductive result (A:Type[0]) : A → Type[0] ≝ |
---|

[409] | 45 | | witness : ∀a:A. result A a. |
---|

| 46 | |
---|

| 47 | (* Hide the representation of memory to make displaying the results easier. *) |
---|

| 48 | |
---|

| 49 | notation < "'MEM'" with precedence 1 for @{ 'mem }. |
---|

| 50 | interpretation "hide memory" 'mem = (mk_mem ???). |
---|