Changeset 764 for src/common/Errors.ma


Ignore:
Timestamp:
Apr 20, 2011, 5:38:58 PM (9 years ago)
Author:
campbell
Message:

Start Cminor to RTLabs phase.

Includes some syntax for matching triples for convenience.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r695 r764  
    6161  ].
    6262
     63definition bind3 ≝ λA,B,C,D: Type[0]. λf: res (A × B × C). λg: A → B → C → res D.
     64  match f with
     65  [ OK v ⇒ match v with [ pair xy z ⇒ match xy with [ pair x y ⇒ g x y z ] ]
     66  | Error (*msg*) => Error ? (*msg*)
     67  ].
     68 
    6369(* Not sure what level to use *)
    6470notation > "vbox('do' ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
     
    7278notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
    7379interpretation "error monad Prod bind" 'bind2 e f = (bind2 ??? e f).
     80notation > "vbox('do' 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}.
     81notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}.
     82notation < "vbox('do' \nbsp 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}.
     83notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}.
     84interpretation "error monad triple bind" 'bind3 e f = (bind3 ???? e f).
    7485(*interpretation "error monad ret" 'ret e = (ret ? e).
    7586notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
Note: See TracChangeset for help on using the changeset viewer.