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

Simplify the IO monad a little.

File size:
1.4 KB

Line  

1  

2  include "extralib.ma". 

3  include "IOMonad.ma". 

4  include "Integers.ma". 

5  include "Events.ma". 

6  

7  nrecord execstep : Type[1] ≝ 

8  { genv : Type 

9  ; state : Type 

10  ; input : Type 

11  ; output : Type 

12  ; initial : state → Prop 

13  ; final : state → int → Prop 

14  ; step : genv → state → IO input output (trace×state) 

15  }. 

16  

17  nlet rec repeat (n:nat) (exec:execstep) (g:genv exec) (s:state exec) 

18  : IO (input exec) (output exec) (trace × (state exec)) ≝ 

19  match n with 

20  [ O ⇒ Value ??? 〈E0, s〉 

21   S n' ⇒ ! 〈t1,s1〉 ← step exec g s;: 

22  repeat n' exec g s1 

23  ]. 

24  

25  alias symbol "and" (instance 2) = "logical and". 

26  nrecord related_semantics : Type[1] ≝ 

27  { sem1 : execstep 

28  ; sem2 : execstep 

29  ; ge1 : genv sem1 

30  ; ge2 : genv sem2 

31  ; match_states : state sem1 → state sem2 → Prop 

32  ; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2 

33  ; match_final_states : ∀st1,st2,r. match_states st1 st2 → (final sem1) st1 r → (final sem2) st2 r 

34  }. 

35  

36  

37  

38  nrecord simulation : Type[1] ≝ 

39  { sems :> related_semantics 

40  ; sim : ∀st1,st2,t,st1'. 

41  P_io' ?? (trace × (state (sem1 sems))) (λr. r = 〈t,st1'〉) (step (sem1 sems) (ge1 sems) st1) → 

42  match_states sems st1 st2 → 

43  ∃st2':(state (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n (sem2 sems) (ge2 sems) st2)) ∧ 

44  match_states sems st1' st2' 

45  }. 

Note: See
TracBrowser
for help on using the repository browser.