source: C-semantics/IOMonad.ma @ 24

Last change on this file since 24 was 24, checked in by campbell, 9 years ago

Separate out IOMonad from the rest of the executable semantics.
Start adding simulation results.

File size: 5.9 KB
Line 
1include "Plogic/russell_support.ma".
2include "extralib.ma".
3include "Errors.ma".
4
5(* IO monad *)
6
7nrecord interaction : Type[1] ≝
8{ output : Type
9; input : Type
10}.
11
12ninductive IO (IT:interaction) (T:Type) : Type ≝
13| Interact : output IT → (input IT → IO IT T) → IO IT T
14| Value : T → IO IT T
15| Wrong : IO IT T.
16
17nlet rec bindIO (IT:interaction) (T,T':Type) (v:IO IT T) (f:T → IO IT T') on v : IO IT T' ≝
18match v with
19[ Interact out k ⇒ (Interact ?? out (λres. bindIO IT T T' (k res) f))
20| Value v' ⇒ (f v')
21| Wrong ⇒ Wrong IT T'
22].
23
24nlet rec bindIO2 (IT:interaction) (T1,T2,T':Type) (v:IO IT (T1×T2)) (f:T1 → T2 → IO IT T') on v : IO IT T' ≝
25match v with
26[ Interact out k ⇒ (Interact ?? out (λres. bindIO2 ? T1 T2 T' (k res) f))
27| Value v' ⇒ match v' with [ mk_pair v1 v2 ⇒ f v1 v2 ]
28| Wrong ⇒ Wrong ? T'
29].
30
31ndefinition err_to_io : ∀IT,T. res T → IO IT T ≝
32λIT,T,v. match v with [ OK v' ⇒ Value IT T v' | Error ⇒ Wrong IT T ].
33(*ncoercion err_to_io : ∀IT,A.∀c:res A.IO IT A ≝ err_to_io on _c:res ? to IO ??.*)
34ndefinition err_to_io_sig : ∀IT,T.∀P:T → Prop. res (sigma T P) → IO IT (sigma T P) ≝
35λIT,T,P,v. match v with [ OK v' ⇒ Value IT (sigma T P) v' | Error ⇒ Wrong IT (sigma T P) ].
36ncoercion err_to_io_sig : ∀IT,A.∀P:A → Prop.∀c:res (sigma A P).IO IT (sigma A P) ≝ err_to_io_sig on _c:res (sigma ??) to IO ? (sigma ??).
37
38
39(* If the original definitions are vague enough, do I need to do this? *)
40notation "! ident v ← e;: e'" right associative with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
41notation "! 〈ident v1, ident v2〉 ← e;: e'" right associative with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
42interpretation "IO monad bind" 'bindIO e f = (bindIO ??? e f).
43interpretation "IO monad pair bind" 'bindIO2 e f = (bindIO2 ???? e f).
44(**)
45nlet rec P_io (IT:interaction) (A:Type) (P:A → Prop) (v:IO IT A) on v : Prop ≝
46match v return λ_.Prop with
47[ Wrong ⇒ True
48| Value z ⇒ P z
49| Interact out k ⇒ ∀v'.P_io IT A P (k v')
50].
51
52nlet rec P_io' (IT:interaction) (A:Type) (P:A → Prop) (v:IO IT A) on v : Prop ≝
53match v return λ_.Prop with
54[ Wrong ⇒ False
55| Value z ⇒ P z
56| Interact out k ⇒ ∀v'.P_io IT A P (k v')
57].
58
59ndefinition P_to_P_option_io : ∀IT,A.∀P:A → Prop.option (IO IT A) → Prop ≝
60  λIT,A,P,a.match a with
61   [ None ⇒ False
62   | Some y ⇒ P_io IT A P y
63   ].
64
65nlet rec io_inject_0 (IT:interaction) (A:Type) (P:A → Prop) (a:IO IT A) (p:P_io IT A P a) on a : IO IT (sigma A P) ≝
66(match a return λa'.a=a' → ? with
67 [ Wrong ⇒ λ_. Wrong IT ?
68 | Value c ⇒ λe2. Value ?? (sig_intro A P c ?)
69 | Interact out k ⇒ λe2. Interact ?? out (λv. io_inject_0 IT A P (k v) ?)
70 ]) (refl ? a).
71 (* XXX: odd, can't do both cases at once. *)
72##[ nrewrite > e2 in p; nwhd in ⊢ (% → ?); //;
73##| nrewrite > e2 in p; nwhd in ⊢ (% → ?); //;
74##] nqed.
75
76ndefinition io_inject : ∀IT,A.∀P:A → Prop.∀a:option (IO IT A).∀p:P_to_P_option_io IT A P a.IO IT (sigma A P) ≝
77  λIT,A.λP:A → Prop.λa:option (IO IT A).λp:P_to_P_option_io IT A P a.
78  (match a return λa'.a=a' → IO IT (sigma A P) with
79   [ None ⇒ λe1.?
80   | Some b ⇒ λe1. io_inject_0 IT A P b ?
81   ]) (refl ? a).
82##[ nrewrite > e1 in p; nnormalize; *;
83##| nrewrite > e1 in p; nnormalize; //
84##] nqed.
85
86nlet rec io_eject (IT:interaction) (A:Type) (P: A → Prop) (a:IO IT (sigma A P)) on a : IO IT A ≝
87match a with
88[ Wrong ⇒ Wrong ??
89| Value b ⇒ match b with [ sig_intro w p ⇒ Value ?? w]
90| Interact out k ⇒ Interact ?? out (λv. io_eject ? A P (k v))
91].
92
93ncoercion io_inject :
94  ∀IT,A.∀P:A → Prop.∀a.∀p:P_to_P_option_io IT ? P a.IO IT (sigma A P) ≝ io_inject
95  on a:option (IO ??) to IO ? (sigma ? ?).
96ncoercion io_eject : ∀IT,A.∀P:A → Prop.∀c:IO IT (sigma A P).IO IT A ≝ io_eject
97  on _c:IO ? (sigma ? ?) to IO ??.
98
99ndefinition opt_to_io : ∀IT,T.option T → IO IT T ≝
100λIT,T,v. match v with [ None ⇒ Wrong IT T | Some v' ⇒ Value IT T v' ].
101ncoercion opt_to_io : ∀IT,T.∀v:option T. IO IT T ≝ opt_to_io on _v:option ? to IO ??.
102
103nlemma sig_bindIO_OK: ∀IT,A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:IO IT (sigma A P). ∀f:sigma A P → IO IT B.
104  (∀v:A. ∀p:P v. P_io IT ? P' (f (sig_intro A P v p))) →
105  P_io IT ? P' (bindIO IT (sigma A P) B e f).
106#IT A B P P' e f; nelim e;
107##[ #out k IH; #IH'; nwhd; #res; napply IH; //;
108##| #v0; nelim v0; #v Hv IH; nwhd; napply IH;
109##| //;
110##] nqed.
111
112nlemma sig_bindIO2_OK: ∀IT,A,B,C. ∀P:(A×B) → Prop. ∀P':C → Prop. ∀e:IO IT (sigma (A×B) P). ∀f: A → B → IO IT C.
113  (∀vA:A.∀vB:B. ∀p:P 〈vA,vB〉. P_io IT ? P' (f vA vB)) →
114  P_io IT ? P' (bindIO2 IT A B C e f).
115#IT A B C P P' e f; nelim e;
116##[ #out k IH; #IH'; nwhd; #res; napply IH; napply IH';
117##| #v0; nelim v0; #v; nelim v; #vA vB Hv IH; napply IH; //;
118##| //;
119##] nqed.
120
121nlemma opt_bindIO_OK: ∀IT,A,B. ∀P:B → Prop. ∀e:option A. ∀f: A → IO IT B.
122  (∀v:A. e = Some A v → P_io IT ? P (f v)) →
123  P_io IT ? P (bindIO IT A B e f).
124#IT A B P e; nelim e; //; #v f H; napply H; //;
125nqed.
126
127nlemma bindIO_OK: ∀IT,A,B. ∀P:B → Prop. ∀e:IO IT A. ∀f: A → IO IT B.
128  (∀v:A. P_io IT ? P (f v)) →
129  P_io IT ? P (bindIO IT A B e f).
130#IT A B P e; nelim e;
131##[ #out k IH; #f H; nwhd; #res; napply IH; //;
132##| #v f H; napply H;
133##| //;
134##] nqed.
135
136(* TODO: is there a way to prove this without extensionality?
137
138nlemma bind_assoc_r: ∀A,B,C,e,f,g.
139  bindIO B C (bindIO A B e f) g = bindIO A C e (λx.bindIO B C (f x) g).
140#A B C e f g; nelim e;
141##[ #fn args k IH; nwhd in ⊢ (???%);
142nnormalize;
143*)
144
145nlemma extract_subset_pair_io: ∀IT,A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→IO IT C. ∀R:C→Prop.
146  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → P_io IT ? R (Q a b)) →
147  P_io IT ? R (match eject ?? e with [ mk_pair a b ⇒ Q a b ]).
148#IT A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;
149##[ *;
150##| #e''; ncases e''; #a b Pab H; nnormalize; /2/;
151##] nqed.
152
Note: See TracBrowser for help on using the repository browser.