source: src/common/SmallstepExec.ma @ 1181

Last change on this file since 1181 was 1181, checked in by mulligan, 10 years ago

changed smallstep exec in order to remove matita bug (superposition.ml on use of auto) when including this file

File size: 4.7 KB
Line 
1
2include "utilities/extralib.ma".
3include "common/IOMonad.ma".
4include "common/Integers.ma".
5include "common/Events.ma".
6include "common/Mem.ma".
7
8record execstep (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
9{ genv  : Type[0]
10; state : Type[0]
11; is_final : state → option int
12; mem_of_state : state → mem
13; step : genv → state → IO outty inty (trace×state)
14}.
15
16let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:execstep outty inty)
17               (g:genv ?? exec) (s:state ?? exec)
18 : IO outty inty (trace × (state ?? exec)) ≝
19match n with
20[ O ⇒ Value ??? 〈E0, s〉
21| S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s;
22         repeat n' ?? exec g s1
23].
24
25let rec trace_map (A,B:Type[0]) (f:A → res (trace × B))
26                  (l:list A) on l : res (trace × (list B)) ≝
27match l with
28[ nil ⇒ OK ? 〈E0, [ ]〉
29| cons h t ⇒
30    do 〈tr,h'〉 ← f h;
31    do 〈tr',t'〉 ← trace_map … f t;
32    OK ? 〈tr ⧺ tr',h'::t'〉
33].
34
35(* A (possibly non-terminating) execution.   *)
36coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
37| e_stop : trace → int → mem → execution state output input
38| e_step : trace → state → execution state output input → execution state output input
39| e_wrong : errmsg → execution state output input
40| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
41
42(* This definition is slightly awkward because of the need to provide resumptions.
43   It records the last trace/state passed in, then recursively processes the next
44   state. *)
45
46let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
47                       (exec:execstep output input) (ge:genv ?? exec)
48                       (s:IO output input (trace×(state ?? exec)))
49                       : execution ??? ≝
50match s with
51[ Wrong m ⇒ e_wrong ??? m
52| Value v ⇒ match v with [ pair t s' ⇒
53    match is_final ?? exec s' with
54    [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
55    | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
56| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
57].
58
59lemma execution_cases: ∀o,i,s.∀e:execution s o i.
60 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
61 | e_step tr s e ⇒ e_step ??? tr s e
62 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
63#o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E %
64 | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto
65  here, used reflexivity instead *)
66
67axiom exec_inf_aux_unfold: ∀o,i,exec,ge,s. exec_inf_aux o i exec ge s =
68match s with
69[ Wrong m ⇒ e_wrong ??? m
70| Value v ⇒ match v with [ pair t s' ⇒
71    match is_final ?? exec s' with
72    [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
73    | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
74| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
75].
76(*
77#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
78[ #o #k
79| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
80| ]
81whd in ⊢ (??%%); //;
82qed.
83*)
84
85record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
86{ es1 :> execstep outty inty
87; program : Type[0]
88; make_initial_state : program → res (genv ?? es1 × (state ?? es1))
89}.
90
91definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx) o i ≝
92λo,i,fx,p.
93  match make_initial_state ?? fx p with
94  [ OK gs ⇒ exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)
95  | Error m ⇒ e_wrong ??? m
96  ].
97
98
99record execstep' (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
100{ es0 :> execstep outty inty
101; initial : state ?? es0 → Prop
102}.
103
104
105alias symbol "and" (instance 2) = "logical and".
106record related_semantics : Type[1] ≝
107{ output : Type[0]
108; input : output → Type[0]
109; sem1 : execstep' output input
110; sem2 : execstep' output input
111; ge1 : genv ?? sem1
112; ge2 : genv ?? sem2
113; match_states : state ?? sem1 → state ?? sem2 → Prop
114; match_initial_states : ∀st1. (initial ?? sem1) st1 → ∃st2. (initial ?? sem2) st2 ∧ match_states st1 st2
115; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final ?? sem1) st1 = Some ? r → (is_final ?? sem2) st2 = Some ? r
116}.
117
118
119
120record simulation : Type[1] ≝
121{ sems :> related_semantics
122; sim : ∀st1,st2,t,st1'.
123        P_io' ?? (trace × (state ?? (sem1 sems))) (λr. r = 〈t,st1'〉) (step ?? (sem1 sems) (ge1 sems) st1) →
124        match_states sems st1 st2 →
125        ∃st2':(state ?? (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state ?? (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n ?? (sem2 sems) (ge2 sems) st2)) ∧
126          match_states sems st1' st2'
127}.
Note: See TracBrowser for help on using the repository browser.