```(*  Title:      HOL/Library/Monad_Syntax.thy
Author:     Alexander Krauss, TU Muenchen
Author:     Christian Sternagel, University of Innsbruck
*)

section ‹Monad notation for arbitrary types›

begin

text ‹
We provide a convenient do-notation for monadic expressions
well-known from Haskell.  @{const Let} is printed
specially in do-expressions.
›

consts
bind :: "['a, 'b ⇒ 'c] ⇒ 'd" (infixr "⤜" 54)

notation (ASCII)
bind (infixr ">>=" 54)

abbreviation (do_notation)
bind_do :: "['a, 'b ⇒ 'c] ⇒ 'd"
where "bind_do ≡ bind"

notation (output)
bind_do (infixr "⤜" 54)

notation (ASCII output)
bind_do (infixr ">>=" 54)

nonterminal do_binds and do_bind
syntax
"_do_block" :: "do_binds ⇒ 'a" ("do {//(2  _)//}" [12] 62)
"_do_bind"  :: "[pttrn, 'a] ⇒ do_bind" ("(2_ ←/ _)" 13)
"_do_let" :: "[pttrn, 'a] ⇒ do_bind" ("(2let _ =/ _)" [1000, 13] 13)
"_do_then" :: "'a ⇒ do_bind" ("_" [14] 13)
"_do_final" :: "'a ⇒ do_binds" ("_")
"_do_cons" :: "[do_bind, do_binds] ⇒ do_binds" ("_;//_" [13, 12] 12)
"_thenM" :: "['a, 'b] ⇒ 'c" (infixr "⪢" 54)

syntax (ASCII)
"_do_bind" :: "[pttrn, 'a] ⇒ do_bind" ("(2_ <-/ _)" 13)
"_thenM" :: "['a, 'b] ⇒ 'c" (infixr ">>" 54)

translations
"_do_block (_do_cons (_do_then t) (_do_final e))"
⇌ "CONST bind_do t (λ_. e)"
"_do_block (_do_cons (_do_bind p t) (_do_final e))"
⇌ "CONST bind_do t (λp. e)"
"_do_block (_do_cons (_do_let p t) bs)"
⇌ "let p = t in _do_block bs"
"_do_block (_do_cons b (_do_cons c cs))"
⇌ "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
"_do_cons (_do_let p t) (_do_final s)"
⇌ "_do_final (let p = t in s)"
"_do_block (_do_final e)" ⇀ "e"
"(m ⪢ n)" ⇀ "(m ⤜ (λ_. n))"