1 | |
---|
2 | include "common/IO.ma". |
---|
3 | include "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 | |
---|
9 | definition get_input : ∀o:io_out. eventval → res (io_in o) ≝ |
---|
10 | λo,ev. |
---|
11 | match io_in_typ o return λt. res (eventval_type t) with |
---|
12 | [ ASTint _ _ ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? (msg IllTypedEvent) ] |
---|
13 | | ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ] |
---|
14 | | ASTptr _ ⇒ Error ? (msg IllTypedEvent) |
---|
15 | ]. |
---|
16 | |
---|
17 | inductive 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 | |
---|
22 | axiom StoppedMidIO : String. |
---|
23 | |
---|
24 | let 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)) ≝ |
---|
25 | match n with |
---|
26 | [ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s) |
---|
27 | | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m) |
---|
28 | | e_interact o k ⇒ Error ? (msg StoppedMidIO) |
---|
29 | | e_wrong m ⇒ Error ? m ] |
---|
30 | | S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m ex input e' (t⧺tr) |
---|
31 | | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m) |
---|
32 | | e_interact o k ⇒ |
---|
33 | match input with |
---|
34 | [ nil ⇒ OK ? (input_exhausted ? t) |
---|
35 | | cons h tl ⇒ do i ← get_input o h; |
---|
36 | up_to_nth_step m ex tl (k i) t |
---|
37 | ] |
---|
38 | | e_wrong m ⇒ Error ? m |
---|
39 | ] |
---|
40 | ]. |
---|
41 | |
---|
42 | definition exec_up_to : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → res (snapshot (state ?? fx)) ≝ |
---|
43 | λfx,p,n,i. up_to_nth_step n fx i (exec_inf ?? fx p) E0. |
---|
44 | |
---|
45 | (* Provide an easy way to get a term in proof mode for reduction. |
---|
46 | For example, |
---|
47 | |
---|
48 | example exec: result ? (exec_up_to myprog 20 [EVint (repr 12)]). |
---|
49 | normalize (* you can examine the result here *) |
---|
50 | % qed. |
---|
51 | |
---|
52 | *) |
---|
53 | |
---|
54 | inductive result (A:Type[0]) : A → Type[0] ≝ |
---|
55 | | witness : ∀a:A. result A a. |
---|
56 | |
---|
57 | definition finishes_with : int → ∀S.res (snapshot S) → Prop ≝ |
---|
58 | λr,S,s. match s with [ OK s' ⇒ match s' with [ finished t r' _ ⇒ r = r' | _ ⇒ False ] | _ ⇒ False ]. |
---|
59 | |
---|
60 | (* Hide the representation of memory to make displaying the results easier. *) |
---|
61 | |
---|
62 | notation < "'MEM'" with precedence 1 for @{ 'mem }. |
---|
63 | interpretation "hide memory" 'mem = (mk_mem ???). |
---|