source: src/common/SmallstepExec.ma @ 1167

Last change on this file since 1167 was 797, checked in by campbell, 10 years ago

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File size: 4.5 KB
RevLine 
[24]1
[700]2include "utilities/extralib.ma".
3include "common/IOMonad.ma".
4include "common/Integers.ma".
5include "common/Events.ma".
6include "common/Mem.ma".
[24]7
[731]8record execstep (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
[693]9{ genv  : Type[0]
10; state : Type[0]
11; is_final : state → option int
12; mem_of_state : state → mem
[731]13; step : genv → state → IO outty inty (trace×state)
[24]14}.
15
[731]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)) ≝
[24]19match n with
[25]20[ O ⇒ Value ??? 〈E0, s〉
[731]21| S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s;
22         repeat n' ?? exec g s1
[24]23].
24
[751]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
[693]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
[797]39| e_wrong : errmsg → execution state output input
[693]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
[731]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)))
[693]49                       : execution ??? ≝
50match s with
[797]51[ Wrong m ⇒ e_wrong ??? m
[693]52| Value v ⇒ match v with [ pair t s' ⇒
[731]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))
[693]57].
58
[731]59lemma execution_cases: ∀o,i,s.∀e:execution s o i.
[693]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
[797]62 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
[731]63#o #i #s #e cases e; //; qed.
[693]64
[731]65axiom exec_inf_aux_unfold: ∀o,i,exec,ge,s. exec_inf_aux o i exec ge s =
[693]66match s with
[797]67[ Wrong m ⇒ e_wrong ??? m
[693]68| Value v ⇒ match v with [ pair t s' ⇒
[731]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))
[693]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
[731]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))
[702]87}.
[693]88
[731]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〉)
[797]93  | Error m ⇒ e_wrong ??? m
[731]94  ].
[693]95
[731]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
[24]103alias symbol "and" (instance 2) = "logical and".
[693]104record related_semantics : Type[1] ≝
[731]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
[24]114}.
115
116
117
[693]118record simulation : Type[1] ≝
[24]119{ sems :> related_semantics
120; sim : ∀st1,st2,t,st1'.
[731]121        P_io' ?? (trace × (state ?? (sem1 sems))) (λr. r = 〈t,st1'〉) (step ?? (sem1 sems) (ge1 sems) st1) →
[24]122        match_states sems st1 st2 →
[731]123        ∃st2':(state ?? (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state ?? (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n ?? (sem2 sems) (ge2 sems) st2)) ∧
[24]124          match_states sems st1' st2'
125}.
Note: See TracBrowser for help on using the repository browser.