src/HOL/Library/Monad_Syntax.thy
author krauss
Tue Jul 13 00:15:37 2010 +0200 (2010-07-13)
changeset 37790 7fea92005066
child 37791 0d6b64060543
permissions -rw-r--r--
uniform do notation for monads
     1 (* Author: Alexander Krauss, TU Muenchen
     2    Author: Christian Sternagel, University of Innsbruck
     3 *)
     4 
     5 header {* Monad notation for arbitrary types *}
     6 
     7 theory Monad_Syntax
     8 imports Adhoc_Overloading
     9 begin
    10 
    11 consts
    12   bindM :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
    13 
    14 notation (xsymbols)
    15   bindM (infixr "\<guillemotright>=" 54)
    16 
    17 abbreviation (do_notation)
    18   bindM_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
    19 where
    20   "bindM_do \<equiv> bindM"
    21 
    22 notation (output)
    23   bindM_do (infixr ">>=" 54)
    24 
    25 notation (xsymbols output)
    26   bindM_do (infixr "\<guillemotright>=" 54)
    27 
    28 nonterminals
    29   do_binds do_bind
    30 
    31 syntax
    32   "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
    33   "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ <-/ _)" 13)
    34   "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
    35   "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
    36   "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
    37   "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
    38   "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54)
    39 
    40 syntax (xsymbols)
    41   "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
    42   "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
    43 
    44 translations
    45   "_do_block (_do_cons (_do_then t) (_do_final e))"
    46     == "CONST bindM_do t (\<lambda>_. e)"
    47   "_do_block (_do_cons (_do_bind p t) (_do_final e))"
    48     == "CONST bindM_do t (\<lambda>p. e)"
    49   "_do_block (_do_cons (_do_let p t) bs)"
    50     == "let p = t in _do_block bs"
    51   "_do_block (_do_cons b (_do_cons c cs))"
    52     == "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
    53   "_do_cons (_do_let p t) (_do_final s)"
    54     == "_do_final (let p = t in s)"
    55   "_do_block (_do_final e)" => "e"
    56   "(m >> n)" => "(m >>= (\<lambda>_. n))"
    57 
    58 setup {* Adhoc_Overloading.add_overloaded @{const_name bindM} *}
    59 
    60 end