Changeset 1640 for src/common/IOMonad.ma
 Timestamp:
 Jan 11, 2012, 5:41:45 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/IOMonad.ma
r1601 r1640 8 8  Value : T → IO output input T 9 9  Wrong : errmsg → IO output input T. 10 11 include "utilities/proper.ma". 12 (* a weak form of extensionality *) 13 axiom interact_proper : 14 ∀O,I,T,o.∀f,g : I o → IO O I T.(∀i. f i = g i) → Interact … o f = Interact … o g. 10 15 11 16 let 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' ≝ … … 16 21 ]. 17 22 18 let 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' ≝ 19 match v with 20 [ Interact out k ⇒ (Interact ??? out (λres. bindIO2 ?? T1 T2 T' (k res) f)) 21  Value v' ⇒ let 〈v1,v2〉 ≝ v' in f v1 v2 22  Wrong m ⇒ Wrong ?? T' m 23 ]. 23 include "utilities/monad.ma". 24 25 definition IOMonad ≝ λO,I. 26 MakeMonad (mk_MonadDefinition 27 (* the monad *) 28 (IO O I) 29 (* return *) 30 (λX.Value … X) 31 (* bind *) 32 (bindIO O I) 33 ???). / by / 34 [(* bind_bind *) 35 #X#Y#Z#m#f#g elim m normalize [2,3://] 36 (* Interact *) 37 #o#f #Hi @interact_proper // 38 (* bind_ret *) 39 #X#m elim m normalize // #o#f#Hi @interact_proper // 40 ] 41 qed. 42 43 definition bindIO2 ≝ λO,I. m_bind2 (IOMonad O I). 44 45 include "hints_declaration.ma". 46 47 unification hint 0 ≔ O, I, T; 48 N ≟ IOMonad O I, M ≟ m_def N 49 (*******************************************) ⊢ 50 IO O I T ≡ monad M T 51 . 52 24 53 25 54 definition err_to_io : ∀O,I,T. res T → IO O I T ≝ 26 55 λO,I,T,v. match v with [ OK v' ⇒ Value O I T v'  Error m ⇒ Wrong O I T m ]. 56 27 57 coercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???. 58 28 59 definition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (Sig T P) → IO O I (Sig T P) ≝ 29 60 λ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 61 (*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 62 32 33 (* If the original definitions are vague enough, do I need to do this? *)34 notation > "! ident v ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.35 notation > "! ident v : ty ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.36 notation < "vbox(! \nbsp ident v ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.37 notation < "vbox(! \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.38 notation > "! 〈ident v1, ident v2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.39 notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.40 notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.41 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.42 interpretation "IO monad bind" 'bindIO e f = (bindIO ???? e f).43 interpretation "IO monad Prod bind" 'bindIO2 e f = (bindIO2 ????? e f).44 (**)45 63 let rec P_io O I (A:Type[0]) (P:A → Prop) (v:IO O I A) on v : Prop ≝ 46 64 match v return λ_.Prop with … … 176 194 177 195 (* Is there a way to prove this without extensionality? *) 178 196 (* 179 197 lemma bind_assoc_r: ∀O,I,A,B,C,e,f,g. 180 198 ∀ext:(∀T1,T2:Type[0].∀f,f':T1 → T2.(∀x.f x = f' x) → f = f'). … … 186 204  #m @refl 187 205 ] qed. 206 *) 207 definition bind_assoc_r ≝ λO,I.m_bind_bind (IOMonad O I). 188 208 189 209 (*
Note: See TracChangeset
for help on using the changeset viewer.