Changeset 208 for C-semantics/IOMonad.ma


Ignore:
Timestamp:
Nov 1, 2010, 11:10:46 AM (9 years ago)
Author:
campbell
Message:

Fix up IO monad syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/IOMonad.ma

    r189 r208  
    3333
    3434(* If the original definitions are vague enough, do I need to do this? *)
    35 notation > "! ident v ← e;: e'" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
    36 notation > "! ident v : ty ← e;: e'" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
    37 notation < "vbox(! \nbsp ident v ← e;: e')" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
    38 notation < "vbox(! \nbsp ident v : ty ← e;: e')" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
    39 notation > "! 〈ident v1, ident v2〉 ← e;: e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
    40 notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e;: e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
    41 notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e;: e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
    42 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e;: e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty2}.λ${ident v2} : ${ty2}.${e'})}.
     35notation > "! ident v ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
     36notation > "! ident v : ty ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
     37notation < "vbox(! \nbsp ident v ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
     38notation < "vbox(! \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
     39notation > "! 〈ident v1, ident v2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     40notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
     41notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     42notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
    4343interpretation "IO monad bind" 'bindIO e f = (bindIO ???? e f).
    4444interpretation "IO monad pair bind" 'bindIO2 e f = (bindIO2 ????? e f).
Note: See TracChangeset for help on using the changeset viewer.