source: src/common/Animation.ma @ 1651

Last change on this file since 1651 was 1231, checked in by campbell, 8 years ago

Change SmallstepExec? so that states can depend on global information.
Use less suggestive names for the transition system so that it's obvious
the global information isn't restricted to Genv.
Separate set up of global environment from initialisation so that it never
fails.
Some minimal changes to get Clight execution working; rest to follow.

File size: 4.6 KB
Line 
1
2include "common/IO.ma".
3include "common/SmallstepExec.ma".
4include "arithmetics/nat.ma".
5
6(* Functions to allow programs to be executed up to some number of steps, given
7   a predetermined set of input values.  Note that we throw away the state if
8   we stop at a continuation - it can be too large to work with. *)
9
10definition get_input : ∀o:io_out. eventval → res (io_in o) ≝
11λo,ev.
12match io_in_typ o return λt. res (eventval_type t) with
13[ ASTint sz _ ⇒ match ev with [ EVint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.OK ? i) (Error ? (msg IllTypedEvent)) | _ ⇒ Error ? (msg IllTypedEvent) ]
14| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
15| ASTptr _ ⇒ Error ? (msg IllTypedEvent)
16].
17
18inductive snapshot (state:Type[0]) : Type[0] ≝
19| running : trace → state → snapshot state
20| finished : trace → int → state → snapshot state
21| input_exhausted : trace → snapshot state.
22
23axiom StoppedMidIO : String.
24
25let rec up_to_nth_step (n:nat) (state:Type[0]) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (snapshot state) ≝
26match n with
27[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s)
28                   | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
29                   | e_interact o k ⇒ Error ? (msg StoppedMidIO)
30                   | e_wrong m ⇒ Error ? m ]
31| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m state input e' (t⧺tr)
32                     | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
33                     | e_interact o k ⇒
34                         match input with
35                         [ nil ⇒ OK ? (input_exhausted ? t)
36                         | cons h tl ⇒ do i ← get_input o h;
37                                       up_to_nth_step m state tl (k i) t
38                         ]
39                     | e_wrong m ⇒ Error ? m
40                     ]
41].
42
43definition exec_up_to : ∀fx:fullexec io_out io_in. ∀p:program ?? fx. nat → list eventval → res (snapshot (state ?? fx (make_global … p))) ≝
44λfx,p,n,i. up_to_nth_step n ? i (exec_inf ?? fx p) E0.
45
46(* A version of exec_up_to that reports the state prior to failure. *)
47
48inductive snapshot' (state:Type[0]) : Type[0] ≝
49| running' : trace → state → snapshot' state
50| finished' : nat → trace → int → state → snapshot' state
51| input_exhausted' : trace → snapshot' state
52| failed' : errmsg → nat → state → snapshot' state
53| init_state_fail' : errmsg → snapshot' state.
54(*
55let rec up_to_nth_step' (n:nat) (total:nat) (ex:execstep io_out io_in) (input:list eventval) (e:execution (state ?? ex) io_out io_in) (prev:state ?? ex) (t:trace) : snapshot' (state ?? ex) ≝
56match n with
57[ O ⇒ match e with [ e_step tr s _ ⇒ running' ? (t⧺tr) s
58                   | e_stop tr r m ⇒ finished' ? total (t⧺tr) r m
59                   | e_interact o k ⇒ failed' ? (msg StoppedMidIO) total prev
60                   | e_wrong m ⇒ failed' ? m total prev ]
61| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step' m total ex input e' s (t⧺tr)
62                     | e_stop tr r m ⇒ finished' ? (minus total n) (t⧺tr) r m
63                     | e_interact o k ⇒
64                         match input with
65                         [ nil ⇒ input_exhausted' ? t
66                         | cons h tl ⇒ match get_input o h with
67                                       [ OK i ⇒ up_to_nth_step' m total ex tl (k i) prev t
68                                       | Error m ⇒ failed' ? m (minus total n) prev
69                                       ]
70                         ]
71                     | e_wrong m ⇒ failed' ? m (minus total n) prev
72                     ]
73].
74
75definition exec_up_to' : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → snapshot' (state ?? fx) ≝
76λfx,p,n,i.
77match make_initial_state ?? fx p with
78[ OK gs ⇒ up_to_nth_step' n n fx i (exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)) (\snd gs) E0
79| Error m ⇒ init_state_fail' ? m
80].
81*)
82(* Provide an easy way to get a term in proof mode for reduction.
83   For example,
84   
85   example exec: result ? (exec_up_to myprog 20 [EVint (repr 12)]).
86   normalize  (* you can examine the result here *)
87   % qed.
88   
89 *)
90
91inductive result (A:Type[0]) : A → Type[0] ≝
92| witness : ∀a:A. result A a.
93
94definition finishes_with : int → ∀S.res (snapshot S) → Prop ≝
95λr,S,s. match s with [ OK s' ⇒ match s' with [ finished t r' _ ⇒ r = r' | _ ⇒ False ] | _ ⇒ False ].
96
97include "common/Mem.ma".
98
99(* Hide the representation of memory to make displaying the results easier. *)
100
101notation < "'MEM'" with precedence 1 for @{ 'mem }.
102interpretation "hide memory" 'mem = (mk_mem ???).
Note: See TracBrowser for help on using the repository browser.