Changeset 4 for C-semantics/Errors.ma


Ignore:
Timestamp:
Jun 2, 2010, 7:11:14 PM (10 years ago)
Author:
campbell
Message:

Some experimental work on executable Clight semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Errors.ma

    r3 r4  
    5858  | Error (*msg*) => Error ? (*msg*)
    5959  ].
     60
     61(* Not sure what level to use *)
     62notation "ident v ← e;: e'" right associative with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
     63interpretation "error monad bind" 'bind e f = (bind ? ? e f).
     64notation "〈ident v1, ident v2〉 ← e;: e'" right associative with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     65interpretation "error monad pair bind" 'bind2 e f = (bind2 ??? e f).
     66(*interpretation "error monad ret" 'ret e = (ret ? e).
     67notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
     68
    6069(*
    6170(** The [do] notation, inspired by Haskell's, keeps the code readable. *)
Note: See TracChangeset for help on using the changeset viewer.