source: src/common/SmallstepExec.ma @ 1598

Last change on this file since 1598 was 1233, checked in by sacerdot, 9 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
RevLine 
[700]1include "utilities/extralib.ma".
2include "common/IOMonad.ma".
3include "common/Integers.ma".
4include "common/Events.ma".
[24]5
[1233]6record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
7{ global : Type[1]
[1231]8; state  : global → Type[0]
9; is_final : ∀g. state g → option int
10; step : ∀g. state g → IO outty inty (trace×(state g))
[24]11}.
12
[1231]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)) ≝
[24]16match n with
[25]17[ O ⇒ Value ??? 〈E0, s〉
[731]18| S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s;
19         repeat n' ?? exec g s1
[24]20].
21
[751]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
[693]32(* A (possibly non-terminating) execution.   *)
33coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
[1213]34| e_stop : trace → int → state → execution state output input
[693]35| e_step : trace → state → execution state output input → execution state output input
[797]36| e_wrong : errmsg → execution state output input
[693]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
[731]43let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
[1231]44                       (exec:trans_system output input) (g:global ?? exec)
45                       (s:IO output input (trace×(state ?? exec g)))
[693]46                       : execution ??? ≝
47match s with
[797]48[ Wrong m ⇒ e_wrong ??? m
[693]49| Value v ⇒ match v with [ pair t s' ⇒
[1231]50    match is_final ?? exec g s' with
[1213]51    [ Some r ⇒ e_stop ??? t r s'
[1231]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))
[693]54].
55
[731]56lemma execution_cases: ∀o,i,s.∀e:execution s o i.
[693]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
[797]59 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
[1181]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 *)
[693]63
[1231]64axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s =
[693]65match s with
[797]66[ Wrong m ⇒ e_wrong ??? m
[693]67| Value v ⇒ match v with [ pair t s' ⇒
[1231]68    match is_final ?? exec g s' with
[1213]69    [ Some r ⇒ e_stop ??? t r s'
[1231]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))
[693]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
[1233]82record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
[1231]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))
[702]87}.
[693]88
[1231]89definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
[731]90λo,i,fx,p.
91  match make_initial_state ?? fx p with
[1231]92  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
[797]93  | Error m ⇒ e_wrong ??? m
[731]94  ].
[693]95
[1231]96(* Some preliminary simulation stuff that's not been used yet.
[731]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}.
[1233]126*)
Note: See TracBrowser for help on using the repository browser.