source: src/common/SmallstepExec.ma @ 1213

Last change on this file since 1213 was 1213, checked in by sacerdot, 9 years ago

1) New values (joint/BEValues.ma) and memory model for the back-ends

(joint/BEMem.ma) where all values are Byte-valued.

2) Improved joint semantics for the back-end languages based on the new

memory model (work in progress).

3) SmallStepExec? made more general to accomodate states with an arbitrary

memory inside.

4) New files common/Pointers.ma and common/GenMem.ma shared between the

front-end and the back-end. GenMem?.ma, at the moment, is not used in Mem.ma
(cut&paste code).

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