source: src/common/Animation.ma @ 3367

Last change on this file since 3367 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 4.5 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| ASTptr ⇒ Error ? (msg IllTypedEvent)
15].
16
17inductive snapshot (state:Type[0]) : Type[0] ≝
18| running : trace → state → snapshot state
19| finished : trace → int → state → snapshot state
20| input_exhausted : trace → snapshot state.
21
22let 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) ≝
23match n with
24[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s)
25                   | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
26                   | e_interact o k ⇒ Error ? (msg StoppedMidIO)
27                   | e_wrong m ⇒ Error ? m ]
28| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m state input e' (t⧺tr)
29                     | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
30                     | e_interact o k ⇒
31                         match input with
32                         [ nil ⇒ OK ? (input_exhausted ? t)
33                         | cons h tl ⇒ do i ← get_input o h;
34                                       up_to_nth_step m state tl (k i) t
35                         ]
36                     | e_wrong m ⇒ Error ? m
37                     ]
38].
39
40definition exec_up_to : ∀fx:fullexec io_out io_in. ∀p:program ?? fx. nat → list eventval → res (snapshot (state ?? fx (make_global … p))) ≝
41λfx,p,n,i. up_to_nth_step n ? i (exec_inf ?? fx p) E0.
42
43(* A version of exec_up_to that reports the state prior to failure. *)
44
45inductive snapshot' (state:Type[0]) : Type[0] ≝
46| running' : trace → state → snapshot' state
47| finished' : nat → trace → int → state → snapshot' state
48| input_exhausted' : trace → snapshot' state
49| failed' : errmsg → nat → state → snapshot' state
50| init_state_fail' : errmsg → snapshot' state.
51
52let rec up_to_nth_step' (n:nat) (total:nat) (state:Type[0]) (input:list eventval) (e:execution state io_out io_in) (prev:state) (t:trace) : snapshot' state ≝
53match n with
54[ O ⇒ match e with [ e_step tr s _ ⇒ running' ? (t⧺tr) s
55                   | e_stop tr r m ⇒ finished' ? total (t⧺tr) r m
56                   | e_interact o k ⇒ failed' ? (msg StoppedMidIO) total prev
57                   | e_wrong m ⇒ failed' ? m total prev ]
58| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step' m total state input e' s (t⧺tr)
59                     | e_stop tr r m ⇒ finished' ? (minus total n) (t⧺tr) r m
60                     | e_interact o k ⇒
61                         match input with
62                         [ nil ⇒ input_exhausted' ? t
63                         | cons h tl ⇒ match get_input o h with
64                                       [ OK i ⇒ up_to_nth_step' m total state tl (k i) prev t
65                                       | Error m ⇒ failed' ? m (minus total n) prev
66                                       ]
67                         ]
68                     | e_wrong m ⇒ failed' ? m (minus total n) prev
69                     ]
70].
71
72definition exec_up_to' : ∀fx:fullexec io_out io_in. ∀p:program ?? fx. nat → list eventval → snapshot' (state ?? fx (make_global … p)) ≝
73λfx,p,n,i.
74match make_initial_state ?? fx p with
75[ OK s ⇒ up_to_nth_step' n n (state ?? fx (make_global … p)) i (exec_inf ?? fx p) s E0
76| Error m ⇒ init_state_fail' ? m
77].
78
79(* Provide an easy way to get a term in proof mode for reduction.
80   For example,
81   
82   example exec: result ? (exec_up_to myprog 20 [EVint (repr 12)]).
83   normalize  (* you can examine the result here *)
84   % qed.
85   
86 *)
87
88inductive result (A:Type[0]) : A → Type[0] ≝
89| witness : ∀a:A. result A a.
90
91inductive finishes_with : int → ∀S.res (snapshot S) → Prop ≝
92fw_ok : ∀r,S,t,s. finishes_with r S (OK ? (finished S t r s)).
93
94include "common/GenMem.ma".
95
96(* Hide the representation of memory to make displaying the results easier. *)
97
98notation < "'MEM'" with precedence 1 for @{ 'mem }.
99interpretation "hide memory" 'mem = (mk_mem ???).
Note: See TracBrowser for help on using the repository browser.