source: src/common/SmallstepExec.ma @ 762

Last change on this file since 762 was 751, checked in by campbell, 9 years ago

Initial version of the Cminor syntax and semantics.

File size: 4.5 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 : 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 ⇒ e_wrong ???
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 ⇒ e_wrong ??? | e_interact o k ⇒ e_interact ??? o k ].
63#o #i #s #e cases e; //; qed.
64
65axiom exec_inf_aux_unfold: ∀o,i,exec,ge,s. exec_inf_aux o i exec ge s =
66match s with
67[ Wrong ⇒ e_wrong ???
68| Value v ⇒ match v with [ pair t s' ⇒
69    match is_final ?? exec s' with
70    [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
71    | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
72| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
73].
74(*
75#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
76[ #o #k
77| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
78| ]
79whd in ⊢ (??%%); //;
80qed.
81*)
82
83record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
84{ es1 :> execstep outty inty
85; program : Type[0]
86; make_initial_state : program → res (genv ?? es1 × (state ?? es1))
87}.
88
89definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx) o i ≝
90λo,i,fx,p.
91  match make_initial_state ?? fx p with
92  [ OK gs ⇒ exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)
93  | _ ⇒ e_wrong ???
94  ].
95
96
97record execstep' (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
98{ es0 :> execstep outty inty
99; initial : state ?? es0 → Prop
100}.
101
102
103alias symbol "and" (instance 2) = "logical and".
104record related_semantics : Type[1] ≝
105{ output : Type[0]
106; input : output → Type[0]
107; sem1 : execstep' output input
108; sem2 : execstep' output input
109; ge1 : genv ?? sem1
110; ge2 : genv ?? sem2
111; match_states : state ?? sem1 → state ?? sem2 → Prop
112; match_initial_states : ∀st1. (initial ?? sem1) st1 → ∃st2. (initial ?? sem2) st2 ∧ match_states st1 st2
113; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final ?? sem1) st1 = Some ? r → (is_final ?? sem2) st2 = Some ? r
114}.
115
116
117
118record simulation : Type[1] ≝
119{ sems :> related_semantics
120; sim : ∀st1,st2,t,st1'.
121        P_io' ?? (trace × (state ?? (sem1 sems))) (λr. r = 〈t,st1'〉) (step ?? (sem1 sems) (ge1 sems) st1) →
122        match_states sems st1 st2 →
123        ∃st2':(state ?? (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state ?? (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n ?? (sem2 sems) (ge2 sems) st2)) ∧
124          match_states sems st1' st2'
125}.
Note: See TracBrowser for help on using the repository browser.