src/HOL/Library/Monad_Syntax.thy
author wenzelm
Fri Jul 12 16:19:05 2013 +0200 (2013-07-12)
changeset 52622 e0ff1625e96d
parent 46143 c932c80d3eae
child 53616 ff37dc246b10
permissions -rw-r--r--
localized and modernized adhoc-overloading (patch by Christian Sternagel);
krauss@37790
     1
(* Author: Alexander Krauss, TU Muenchen
krauss@37790
     2
   Author: Christian Sternagel, University of Innsbruck
krauss@37790
     3
*)
krauss@37790
     4
krauss@37790
     5
header {* Monad notation for arbitrary types *}
krauss@37790
     6
krauss@37790
     7
theory Monad_Syntax
haftmann@45990
     8
imports Main "~~/src/Tools/Adhoc_Overloading"
krauss@37790
     9
begin
krauss@37790
    10
krauss@37791
    11
text {*
krauss@37791
    12
  We provide a convenient do-notation for monadic expressions
krauss@37791
    13
  well-known from Haskell.  @{const Let} is printed
krauss@37791
    14
  specially in do-expressions.
krauss@37791
    15
*}
krauss@37791
    16
krauss@37790
    17
consts
haftmann@37816
    18
  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
krauss@37790
    19
krauss@37790
    20
notation (xsymbols)
haftmann@37816
    21
  bind (infixr "\<guillemotright>=" 54)
krauss@37790
    22
haftmann@37848
    23
notation (latex output)
haftmann@37848
    24
  bind (infixr "\<bind>" 54)
haftmann@37848
    25
krauss@37790
    26
abbreviation (do_notation)
haftmann@37816
    27
  bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
krauss@37790
    28
where
haftmann@37816
    29
  "bind_do \<equiv> bind"
krauss@37790
    30
krauss@37790
    31
notation (output)
haftmann@37816
    32
  bind_do (infixr ">>=" 54)
krauss@37790
    33
krauss@37790
    34
notation (xsymbols output)
haftmann@37816
    35
  bind_do (infixr "\<guillemotright>=" 54)
krauss@37790
    36
haftmann@37848
    37
notation (latex output)
haftmann@37848
    38
  bind_do (infixr "\<bind>" 54)
haftmann@37848
    39
wenzelm@41229
    40
nonterminal do_binds and do_bind
krauss@37790
    41
krauss@37790
    42
syntax
krauss@37790
    43
  "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
krauss@37790
    44
  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ <-/ _)" 13)
krauss@37790
    45
  "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
krauss@37790
    46
  "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
krauss@37790
    47
  "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
krauss@37790
    48
  "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
krauss@37790
    49
  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54)
krauss@37790
    50
krauss@37790
    51
syntax (xsymbols)
krauss@37790
    52
  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
krauss@37790
    53
  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
krauss@37790
    54
haftmann@37848
    55
syntax (latex output)
haftmann@37848
    56
  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<then>" 54)
haftmann@37848
    57
krauss@37790
    58
translations
krauss@37790
    59
  "_do_block (_do_cons (_do_then t) (_do_final e))"
haftmann@37816
    60
    == "CONST bind_do t (\<lambda>_. e)"
krauss@37790
    61
  "_do_block (_do_cons (_do_bind p t) (_do_final e))"
haftmann@37816
    62
    == "CONST bind_do t (\<lambda>p. e)"
krauss@37790
    63
  "_do_block (_do_cons (_do_let p t) bs)"
krauss@37790
    64
    == "let p = t in _do_block bs"
krauss@37790
    65
  "_do_block (_do_cons b (_do_cons c cs))"
krauss@37790
    66
    == "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
krauss@37790
    67
  "_do_cons (_do_let p t) (_do_final s)"
krauss@37790
    68
    == "_do_final (let p = t in s)"
krauss@37790
    69
  "_do_block (_do_final e)" => "e"
krauss@37790
    70
  "(m >> n)" => "(m >>= (\<lambda>_. n))"
krauss@37790
    71
wenzelm@52622
    72
adhoc_overloading
wenzelm@52622
    73
  bind Set.bind Predicate.bind Option.bind List.bind
krauss@37790
    74
krauss@37790
    75
end