source: src/common/SmallstepExec.ma @ 2145

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

Cost labelling doesn't affect interaction.

File size: 6.6 KB
Line 
1include "utilities/extralib.ma".
2include "common/IOMonad.ma".
3include "common/Integers.ma".
4include "common/Events.ma".
5
6record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
7{ global : Type[1]
8; state  : global → Type[0]
9; is_final : ∀g. state g → option int
10; step : ∀g. state g → IO outty inty (trace×(state g))
11}.
12
13let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:trans_system outty inty)
14               (g:global ?? exec) (s:state ?? exec g)
15 : IO outty inty (trace × (state ?? exec g)) ≝
16match n with
17[ O ⇒ Value ??? 〈E0, s〉
18| S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s;
19         repeat n' ?? exec g s1
20].
21
22let rec trace_map (A,B:Type[0]) (f:A → res (trace × B))
23                  (l:list A) on l : res (trace × (list B)) ≝
24match l with
25[ nil ⇒ OK ? 〈E0, [ ]〉
26| cons h t ⇒
27    do 〈tr,h'〉 ← f h;
28    do 〈tr',t'〉 ← trace_map … f t;
29    OK ? 〈tr ⧺ tr',h'::t'〉
30].
31
32(* A (possibly non-terminating) execution.   *)
33coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
34| e_stop : trace → int → state → execution state output input
35| e_step : trace → state → execution state output input → execution state output input
36| e_wrong : errmsg → execution state output input
37| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
38
39(* This definition is slightly awkward because of the need to provide resumptions.
40   It records the last trace/state passed in, then recursively processes the next
41   state. *)
42
43let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
44                       (exec:trans_system output input) (g:global ?? exec)
45                       (s:IO output input (trace×(state ?? exec g)))
46                       : execution ??? ≝
47match s with
48[ Wrong m ⇒ e_wrong ??? m
49| Value v ⇒ let 〈t,s'〉 ≝ v in
50    match is_final ?? exec g s' with
51    [ Some r ⇒ e_stop ??? t r s'
52    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
53| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
54].
55
56lemma execution_cases: ∀o,i,s.∀e:execution s o i.
57 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
58 | e_step tr s e ⇒ e_step ??? tr s e
59 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
60#o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E %
61 | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto
62  here, used reflexivity instead *)
63
64axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s =
65match s with
66[ Wrong m ⇒ e_wrong ??? m
67| Value v ⇒ let 〈t,s'〉 ≝ v in
68    match is_final ?? exec g s' with
69    [ Some r ⇒ e_stop ??? t r s'
70    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
71| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
72].
73(*
74#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
75[ #o #k
76| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
77| ]
78whd in ⊢ (??%%); //;
79qed.
80*)
81
82lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r.
83  exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' →
84  step … ge s = Value … 〈tr, s'〉 ∧
85  is_final … s' = Some ? r.
86#O #I #TS #ge #s #s' #tr #r
87>exec_inf_aux_unfold
88cases (step … ge s)
89[ 1,3: normalize #H1 #H2 try #H3 destruct
90| * #tr' #s''
91  whd in ⊢ (??%? → ?);
92  lapply (refl ? (is_final … s''))
93  cases (is_final … s'') in ⊢ (???% → %);
94  [ #_ whd in ⊢ (??%? → ?); #E destruct
95  | #r' #E1 #E2 whd in E2:(??%?);  destruct % //
96  ]
97] qed.
98
99lemma extract_step : ∀O,I,TS,ge,s,s',tr,e.
100  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
101  step … ge s = Value …  〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s').
102#O #I #TS #ge #s #s' #tr #e
103>exec_inf_aux_unfold
104cases (step … s)
105[ 1,3: normalize #H1 #H2 try #H3 destruct
106| * #tr' #s''
107  whd in ⊢ (??%? → ?);
108  cases (is_final … s'')
109  [ #E normalize in E; destruct /2/
110  | #r #E normalize in E; destruct
111  ]
112] qed.
113
114lemma extract_interact : ∀O,I,TS,ge,s,o,k.
115  exec_inf_aux O I TS ge (step … ge s) = e_interact … o k →
116  ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)).
117#O #I #TS #ge #s #o #k >exec_inf_aux_unfold
118cases (step … s)
119[ #o' #k' normalize #E destruct %{k'} /2/
120| * #x #y normalize cases (is_final ?????) normalize
121  #X try #Y destruct
122| normalize #m #E destruct
123] qed.
124
125lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
126  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
127  is_final … s' = None ?.
128#O #I #TS #ge #s #s' #tr #e
129>exec_inf_aux_unfold
130cases (step … s)
131[ 1,3: normalize #H1 #H2 try #H3 destruct
132| * #tr' #s''
133  whd in ⊢ (??%? → ?);
134  lapply (refl ? (is_final … s''))
135  cases (is_final … s'') in ⊢ (???% → %);
136  [ #F whd in ⊢ (??%? → ?); #E destruct @F
137  | #r' #_ #E whd in E:(??%?);  destruct
138  ]
139] qed.
140
141
142
143record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
144{ program : Type[0]
145; es1 :> trans_system outty inty
146; make_global : program → global ?? es1
147; make_initial_state : ∀p:program. res (state ?? es1 (make_global p))
148}.
149
150definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
151λo,i,fx,p.
152  match make_initial_state ?? fx p with
153  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
154  | Error m ⇒ e_wrong ??? m
155  ].
156
157(* Some preliminary simulation stuff that's not been used yet.
158record execstep' (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
159{ es0 :> execstep outty inty
160; initial : state ?? es0 → Prop
161}.
162
163
164alias symbol "and" (instance 2) = "logical and".
165record related_semantics : Type[1] ≝
166{ output : Type[0]
167; input : output → Type[0]
168; sem1 : execstep' output input
169; sem2 : execstep' output input
170; ge1 : genv ?? sem1
171; ge2 : genv ?? sem2
172; match_states : state ?? sem1 → state ?? sem2 → Prop
173; match_initial_states : ∀st1. (initial ?? sem1) st1 → ∃st2. (initial ?? sem2) st2 ∧ match_states st1 st2
174; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final ?? sem1) st1 = Some ? r → (is_final ?? sem2) st2 = Some ? r
175}.
176
177
178
179record simulation : Type[1] ≝
180{ sems :> related_semantics
181; sim : ∀st1,st2,t,st1'.
182        P_io' ?? (trace × (state ?? (sem1 sems))) (λr. r = 〈t,st1'〉) (step ?? (sem1 sems) (ge1 sems) st1) →
183        match_states sems st1 st2 →
184        ∃st2':(state ?? (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state ?? (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n ?? (sem2 sems) (ge2 sems) st2)) ∧
185          match_states sems st1' st2'
186}.
187*)
Note: See TracBrowser for help on using the repository browser.