source: src/common/SmallstepExec.ma @ 1233

Last change on this file since 1233 was 1233, checked in by sacerdot, 8 years ago

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

File size: 4.8 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 ⇒ match v with [ pair t s' ⇒
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 ⇒ match v with [ pair t s' ⇒
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
82record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
83{ program : Type[0]
84; es1 :> trans_system outty inty
85; make_global : program → global ?? es1
86; make_initial_state : ∀p:program. res (state ?? es1 (make_global p))
87}.
88
89definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
90λo,i,fx,p.
91  match make_initial_state ?? fx p with
92  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
93  | Error m ⇒ e_wrong ??? m
94  ].
95
96(* Some preliminary simulation stuff that's not been used yet.
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}.
126*)
Note: See TracBrowser for help on using the repository browser.