krauss@37790: (* Author: Alexander Krauss, TU Muenchen
krauss@37790:    Author: Christian Sternagel, University of Innsbruck
krauss@37790: *)
krauss@37790: 
krauss@37790: header {* Monad notation for arbitrary types *}
krauss@37790: 
krauss@37790: theory Monad_Syntax
haftmann@45145: imports Main "~~/src/Tools/Adhoc_Overloading" "~~/src/HOL/Library/More_List"
krauss@37790: begin
krauss@37790: 
krauss@37791: text {*
krauss@37791:   We provide a convenient do-notation for monadic expressions
krauss@37791:   well-known from Haskell.  @{const Let} is printed
krauss@37791:   specially in do-expressions.
krauss@37791: *}
krauss@37791: 
krauss@37790: consts
haftmann@37816:   bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
krauss@37790: 
krauss@37790: notation (xsymbols)
haftmann@37816:   bind (infixr "\<guillemotright>=" 54)
krauss@37790: 
haftmann@37848: notation (latex output)
haftmann@37848:   bind (infixr "\<bind>" 54)
haftmann@37848: 
krauss@37790: abbreviation (do_notation)
haftmann@37816:   bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
krauss@37790: where
haftmann@37816:   "bind_do \<equiv> bind"
krauss@37790: 
krauss@37790: notation (output)
haftmann@37816:   bind_do (infixr ">>=" 54)
krauss@37790: 
krauss@37790: notation (xsymbols output)
haftmann@37816:   bind_do (infixr "\<guillemotright>=" 54)
krauss@37790: 
haftmann@37848: notation (latex output)
haftmann@37848:   bind_do (infixr "\<bind>" 54)
haftmann@37848: 
wenzelm@41229: nonterminal do_binds and do_bind
krauss@37790: 
krauss@37790: syntax
krauss@37790:   "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
krauss@37790:   "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ <-/ _)" 13)
krauss@37790:   "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
krauss@37790:   "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
krauss@37790:   "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
krauss@37790:   "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
krauss@37790:   "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54)
krauss@37790: 
krauss@37790: syntax (xsymbols)
krauss@37790:   "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
krauss@37790:   "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
krauss@37790: 
haftmann@37848: syntax (latex output)
haftmann@37848:   "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<then>" 54)
haftmann@37848: 
krauss@37790: translations
krauss@37790:   "_do_block (_do_cons (_do_then t) (_do_final e))"
haftmann@37816:     == "CONST bind_do t (\<lambda>_. e)"
krauss@37790:   "_do_block (_do_cons (_do_bind p t) (_do_final e))"
haftmann@37816:     == "CONST bind_do t (\<lambda>p. e)"
krauss@37790:   "_do_block (_do_cons (_do_let p t) bs)"
krauss@37790:     == "let p = t in _do_block bs"
krauss@37790:   "_do_block (_do_cons b (_do_cons c cs))"
krauss@37790:     == "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
krauss@37790:   "_do_cons (_do_let p t) (_do_final s)"
krauss@37790:     == "_do_final (let p = t in s)"
krauss@37790:   "_do_block (_do_final e)" => "e"
krauss@37790:   "(m >> n)" => "(m >>= (\<lambda>_. n))"
krauss@37790: 
haftmann@37816: setup {*
haftmann@37816:   Adhoc_Overloading.add_overloaded @{const_name bind}
haftmann@45964:   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Set.bind}
haftmann@37816:   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
krauss@39151:   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
haftmann@45145:   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name More_List.bind}
haftmann@37816: *}
krauss@37790: 
krauss@37790: end