source: src/common/Animation.ma @ 961

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

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 2.7 KB
Line 
1
2include "common/IO.ma".
3include "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
9definition get_input : ∀o:io_out. eventval → res (io_in o) ≝
10λo,ev.
11match io_in_typ o return λt. res (eventval_type t) with
12[ ASTint sz _ ⇒ match ev with [ EVint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.OK ? i) (Error ? (msg IllTypedEvent)) | _ ⇒ Error ? (msg IllTypedEvent) ]
13| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
14| ASTptr _ ⇒ Error ? (msg IllTypedEvent)
15].
16
17inductive 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
22axiom StoppedMidIO : String.
23
24let 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)) ≝
25match 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
42definition 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
54inductive result (A:Type[0]) : A → Type[0] ≝
55| witness : ∀a:A. result A a.
56
57definition 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
62notation < "'MEM'" with precedence 1 for @{ 'mem }.
63interpretation "hide memory" 'mem = (mk_mem ???).
Note: See TracBrowser for help on using the repository browser.