Changeset 1640 for src/common/IOMonad.ma


Ignore:
Timestamp:
Jan 11, 2012, 5:41:45 PM (8 years ago)
Author:
tranquil
Message:
  • finished fork of semantics.ma
  • unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r1601 r1640  
    88| Value : T → IO output input T
    99| Wrong : errmsg → IO output input T.
     10
     11include "utilities/proper.ma".
     12(* a weak form of extensionality *)
     13axiom 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.
    1015
    1116let 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' ≝
     
    1621].
    1722
    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 ].
     23include "utilities/monad.ma".
     24
     25definition 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]
     41qed.
     42
     43definition bindIO2 ≝ λO,I. m_bind2 (IOMonad O I).
     44
     45include "hints_declaration.ma".
     46
     47unification 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
    2453
    2554definition err_to_io : ∀O,I,T. res T → IO O I T ≝
    2655λO,I,T,v. match v with [ OK v' ⇒ Value O I T v' | Error m ⇒ Wrong O I T m ].
     56
    2757coercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???.
     58
    2859definition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (Sig T P) → IO O I (Sig T P) ≝
    2960λ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 ].
    3061(*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 ??).*)
    3162
    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 (**)
    4563let rec P_io O I (A:Type[0]) (P:A → Prop) (v:IO O I A) on v : Prop ≝
    4664match v return λ_.Prop with
     
    176194
    177195(* Is there a way to prove this without extensionality? *)
    178 
     196(*
    179197lemma bind_assoc_r: ∀O,I,A,B,C,e,f,g.
    180198  ∀ext:(∀T1,T2:Type[0].∀f,f':T1 → T2.(∀x.f x = f' x) → f = f').
     
    186204| #m @refl
    187205] qed.
     206*)
     207definition bind_assoc_r ≝ λO,I.m_bind_bind (IOMonad O I).
    188208
    189209(*
Note: See TracChangeset for help on using the changeset viewer.