source: src/common/IOMonad.ma @ 1516

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

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File size: 8.3 KB
Line 
1include "utilities/extralib.ma".
2include "common/Errors.ma".
3
4(* IO monad *)
5
6inductive IO (output:Type[0]) (input:output → Type[0]) (T:Type[0]) : Type[0] ≝
7| Interact : ∀o:output. (input o → IO output input T) → IO output input T
8| Value : T → IO output input T
9| Wrong : errmsg → IO output input T.
10
11let rec bindIO (O:Type[0]) (I:O → Type[0]) (T,T':Type[0]) (v:IO O I T) (f:T → IO O I T') on v : IO O I T' ≝
12match v with
13[ Interact out k ⇒ (Interact ??? out (λres. bindIO O I T T' (k res) f))
14| Value v' ⇒ (f v')
15| Wrong m ⇒ Wrong O I T' m
16].
17
18let rec bindIO2 (O:Type[0]) (I:O → Type[0]) (T1,T2,T':Type[0]) (v:IO O I (T1×T2)) (f:T1 → T2 → IO O I T') on v : IO O I T' ≝
19match v with
20[ Interact out k ⇒ (Interact ??? out (λres. bindIO2 ?? T1 T2 T' (k res) f))
21| Value v' ⇒ match v' with [ pair v1 v2 ⇒ f v1 v2 ]
22| Wrong m ⇒ Wrong ?? T' m
23].
24
25definition err_to_io : ∀O,I,T. res T → IO O I T ≝
26λO,I,T,v. match v with [ OK v' ⇒ Value O I T v' | Error m ⇒ Wrong O I T m ].
27coercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???.
28definition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (Sig T P) → IO O I (Sig T P) ≝
29λO,I,T,P,v. match v with [ OK v' ⇒ Value O I (Sig T P) v' | Error m ⇒ Wrong O I (Sig T P) m ].
30(*coercion err_to_io_sig : ∀O,I,A.∀P:A → Prop.∀c:res (Sig A P).IO O I (Sig A P) ≝ err_to_io_sig on _c:res (Sig ??) to IO ?? (Sig ??).*)
31
32
33(* If the original definitions are vague enough, do I need to do this? *)
34notation > "! ident v ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
35notation > "! ident v : ty ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
36notation < "vbox(! \nbsp ident v ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
37notation < "vbox(! \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
38notation > "! 〈ident v1, ident v2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
39notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
40notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
41notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
42interpretation "IO monad bind" 'bindIO e f = (bindIO ???? e f).
43interpretation "IO monad Prod bind" 'bindIO2 e f = (bindIO2 ????? e f).
44(**)
45let rec P_io O I (A:Type[0]) (P:A → Prop) (v:IO O I A) on v : Prop ≝
46match v return λ_.Prop with
47[ Wrong _ ⇒ True
48| Value z ⇒ P z
49| Interact out k ⇒ ∀v'.P_io O I A P (k v')
50].
51
52let rec P_io' O I (A:Type[0]) (P:A → Prop) (v:IO O I A) on v : Prop ≝
53match v return λ_.Prop with
54[ Wrong _ ⇒ False
55| Value z ⇒ P z
56| Interact out k ⇒ ∀v'.P_io' O I A P (k v')
57].
58
59definition P_to_P_option_io : ∀O,I,A.∀P:A → Prop.option (IO O I A) → Prop ≝
60  λO,I,A,P,a.match a with
61   [ None ⇒ False
62   | Some y ⇒ P_io O I A P y
63   ].
64
65let rec io_inject_0 O I (A:Type[0]) (P:A → Prop) (a:IO O I A) (p:P_io O I A P a) on a : IO O I (Sig A P) ≝
66(match a return λa'.P_io O I A P a' → ? with
67 [ Wrong m ⇒ λ_. Wrong O I ? m
68 | Value c ⇒ λp'. Value ??? (dp A P c p')
69 | Interact out k ⇒ λp'. Interact ??? out (λv. io_inject_0 O I A P (k v) (p' v))
70 ]) p.
71
72definition io_inject : ∀O,I,A.∀P:A → Prop.∀a:option (IO O I A).∀p:P_to_P_option_io O I A P a.IO O I (Sig A P) ≝
73  λO,I,A.λP:A → Prop.λa:option (IO O I A).λp:P_to_P_option_io O I A P a.
74  (match a return λa'.P_to_P_option_io O I A P a' → IO O I (Sig A P) with
75   [ None ⇒ λp'.?
76   | Some b ⇒ λp'. io_inject_0 O I A P b p'
77   ]) p.
78elim p'; qed.
79
80let rec io_eject O I (A:Type[0]) (P: A → Prop) (a:IO O I (Sig A P)) on a : IO O I A ≝
81match a with
82[ Wrong m ⇒ Wrong ??? m
83| Value b ⇒ match b with [ dp w p ⇒ Value ??? w]
84| Interact out k ⇒ Interact ??? out (λv. io_eject ?? A P (k v))
85].
86
87coercion io_inject :
88  ∀O,I,A.∀P:A → Prop.∀a.∀p:P_to_P_option_io O I ? P a.IO O I (Sig A P) ≝ io_inject
89  on a:option (IO ???) to IO ?? (Sig ? ?).
90coercion io_eject : ∀O,I,A.∀P:A → Prop.∀c:IO O I (Sig A P).IO O I A ≝ io_eject
91  on _c:IO ?? (Sig ? ?) to IO ???.
92
93definition opt_to_io : ∀O,I,T.errmsg → option T → IO O I T ≝
94λO,I,T,m,v. match v with [ None ⇒ Wrong ?? T m | Some v' ⇒ Value ??? v' ].
95
96lemma sig_bindIO_OK: ∀O,I,A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:IO O I (Sig A P). ∀f:Sig A P → IO O I B.
97  (∀v:A. ∀p:P v. P_io O I ? P' (f (dp A P v p))) →
98  P_io O I ? P' (bindIO O I (Sig A P) B e f).
99#O #I #A #B #P #P' #e #f elim e;
100[ #out #k #IH #IH' whd; #res @IH //;
101| #v0 elim v0; #v #Hv #IH whd; @IH
102| //;
103] qed.
104
105lemma sig_bindIO2_OK: ∀O,I,A,B,C. ∀P:(A×B) → Prop. ∀P':C → Prop. ∀e:IO O I (Sig (A×B) P). ∀f: A → B → IO O I C.
106  (∀vA:A.∀vB:B. ∀p:P 〈vA,vB〉. P_io O I ? P' (f vA vB)) →
107  P_io O I ? P' (bindIO2 O I A B C e f).
108#I #O #A #B #C #P #P' #e #f elim e;
109[ #out #k #IH #IH' whd; #res @IH @IH'
110| #v0 elim v0; #v elim v; #vA #vB #Hv #IH @IH //;
111| //;
112] qed.
113
114lemma opt_bindIO_OK: ∀O,I,A,B,m. ∀P:B → Prop. ∀e:option A. ∀f: A → IO O I B.
115  (∀v:A. e = Some A v → P_io O I ? P (f v)) →
116  P_io O I ? P (bindIO O I A B (opt_to_io ??? m e) f).
117#I #O #A #B #m #P #e elim e; //; #v #f #H @H //;
118qed.
119
120lemma opt_bindIO2_OK: ∀O,I,A,B,C,m. ∀P:C → Prop. ∀e:option (A×B). ∀f: A → B → IO O I C.
121  (∀vA:A.∀vB:B. e = Some (A×B) 〈vA,vB〉 → P_io O I ? P (f vA vB)) →
122  P_io O I ? P (bindIO2 O I A B C (opt_to_io ??? m e) f).
123#I #O #A #B #C #m #P #e elim e; //; #v cases v; #vA #vB #f #H @H //;
124qed.
125
126lemma res_bindIO_OK: ∀O,I,A,B. ∀P:B → Prop. ∀e:res A. ∀f: A → IO O I B.
127  (∀v:A. e = OK A v → P_io O I ? P (f v)) →
128  P_io O I ? P (bindIO O I A B e f).
129#I #O #A #B #P #e elim e; //; #v #f #H @H //;
130qed.
131
132lemma res_bindIO2_OK: ∀O,I,A,B,C. ∀P:C → Prop. ∀e:res (A×B). ∀f: A → B → IO O I C.
133  (∀vA:A.∀vB:B. e = OK (A×B) 〈vA,vB〉 → P_io O I ? P (f vA vB)) →
134  P_io O I ? P (bindIO2 O I A B C e f).
135#I #O #A #B #C #P #e elim e; //; #v cases v; #vA #vB #f #H @H //;
136qed.
137
138lemma bindIO_OK: ∀O,I,A,B. ∀P:B → Prop. ∀e:IO O I A. ∀f: A → IO O I B.
139  (∀v:A. P_io O I ? P (f v)) →
140  P_io O I ? P (bindIO O I A B e f).
141#I #O #A #B #P #e elim e;
142[ #out #k #IH #f #H whd; #res @IH //;
143| #v #f #H @H
144| //;
145] qed.
146
147lemma bindIO2_OK: ∀O,I,A,B,C. ∀P:C → Prop. ∀e:IO O I (A×B). ∀f: A → B → IO O I C.
148  (∀v1:A.∀v2:B. P_io O I ? P (f v1 v2)) →
149  P_io O I ? P (bindIO2 O I A B C e f).
150#I #O #A #B #C #P #e elim e;
151[ #out #k #IH #f #H whd; #res @IH //;
152| #v cases v; #v1 #v2 #f #H @H
153| //;
154] qed.
155
156lemma P_bindIO_OK: ∀O,I,A,B. ∀P':A → Prop. ∀P:B → Prop. ∀e:IO O I A. ∀f: A → IO O I B.
157  P_io … P' e →
158  (∀v:A. P' v → P_io O I ? P (f v)) →
159  P_io O I ? P (bindIO O I A B e f).
160#I #O #A #B #P' #P #e elim e;
161[ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2/;
162| #v #f #He #H @H @He
163| //;
164] qed.
165
166lemma P_bindIO2_OK: ∀O,I,A,B,C. ∀P':A×B → Prop. ∀P:C → Prop. ∀e:IO O I (A×B). ∀f: A → B → IO O I C.
167  P_io … P' e →
168  (∀v1:A.∀v2:B. P' 〈v1,v2〉 → P_io O I ? P (f v1 v2)) →
169  P_io O I ? P (bindIO2 O I A B C e f).
170#I #O #A #B #C #P' #P #e elim e;
171[ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2/;
172| #v cases v; #v1 #v2 #f #He #H @H @He
173| //;
174] qed.
175
176
177(* Is there a way to prove this without extensionality? *)
178
179lemma bind_assoc_r: ∀O,I,A,B,C,e,f,g.
180  ∀ext:(∀T1,T2:Type[0].∀f,f':T1 → T2.(∀x.f x = f' x) → f = f').
181  bindIO O I B C (bindIO O I A B e f) g = bindIO O I A C e (λx.bindIO O I B C (f x) g).
182#O #I #A #B #C #e #f #g #ext elim e;
183[ #o #k #IH whd in ⊢ (??%%); @eq_f
184    @ext @IH
185| #v @refl
186| #m @refl
187] qed.
188
189(*
190lemma extract_subset_pair_io: ∀O,I,A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→IO O I C. ∀R:C→Prop.
191  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → P_io O I ? R (Q a b)) →
192  P_io O I ? R (match eject ?? e with [ pair a b ⇒ Q a b ]).
193#I #O #A #B #C #P #e #Q #R cases e; #e' cases e'; normalize;
194[ *;
195| #e'' cases e''; #a #b #Pab #H normalize; /2/;
196] qed.
197*)
Note: See TracBrowser for help on using the repository browser.