Theory HOL-Library.Monad_Syntax

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

section ‹Monad notation for arbitrary types›

theory Monad_Syntax
  imports Main
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" (infixl ‹⤜› 54)

notation (ASCII)
  bind (infixl ‹>>=› 54)


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

notation (output)
  bind_do (infixl ‹⤜› 54)

notation (ASCII output)
  bind_do (infixl ‹>>=› 54)


nonterminal do_binds and do_bind
syntax
  "_do_block" :: "do_binds ⇒ 'a"
    (‹(‹open_block notation=‹mixfix do block››do {//(2  _)//})› [12] 62)
  "_do_bind"  :: "[pttrn, 'a] ⇒ do_bind"
    (‹(‹indent=2 notation=‹infix do bind››_ ←/ _)› 13)
  "_do_let" :: "[pttrn, 'a] ⇒ do_bind"
    (‹(‹indent=2 notation=‹infix do let››let _ =/ _)› [1000, 13] 13)
  "_do_then" :: "'a ⇒ do_bind"  (‹_› [14] 13)
  "_do_final" :: "'a ⇒ do_binds"  (‹_›)
  "_do_cons" :: "[do_bind, do_binds] ⇒ do_binds"
    (‹(‹open_block notation=‹infix do next››_;//_)› [13, 12] 12)
  "_thenM" :: "['a, 'b] ⇒ 'c"  (infixl ‹⪢› 54)

syntax (ASCII)
  "_do_bind" :: "[pttrn, 'a] ⇒ do_bind"
    (‹(‹indent=2 notation=‹infix do bind››_ <-/ _)› 13)
  "_thenM" :: "['a, 'b] ⇒ 'c"  (infixl ‹>>› 54)

syntax_consts
  "_do_block" "_do_cons" "_do_bind" "_do_then" ⇌ bind and
  "_do_let" ⇌ Let

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))"

adhoc_overloading
  bind ⇌ Set.bind Predicate.bind Option.bind List.bind

end