src/HOL/Library/Monad_Syntax.thy
author haftmann
Sat, 24 Dec 2011 15:53:08 +0100
changeset 45964 7b3a18670a9f
parent 45145 d5086da3c32d
child 45990 b7b905b23b2a
permissions -rw-r--r--
added monad instance for `set`
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
     1
(* Author: Alexander Krauss, TU Muenchen
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
     2
   Author: Christian Sternagel, University of Innsbruck
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
     3
*)
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
     4
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
     5
header {* Monad notation for arbitrary types *}
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
     6
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
     7
theory Monad_Syntax
45145
d5086da3c32d monadic bind
haftmann
parents: 41229
diff changeset
     8
imports Main "~~/src/Tools/Adhoc_Overloading" "~~/src/HOL/Library/More_List"
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
     9
begin
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    10
37791
0d6b64060543 State_Monad uses Monad_Syntax
krauss
parents: 37790
diff changeset
    11
text {*
0d6b64060543 State_Monad uses Monad_Syntax
krauss
parents: 37790
diff changeset
    12
  We provide a convenient do-notation for monadic expressions
0d6b64060543 State_Monad uses Monad_Syntax
krauss
parents: 37790
diff changeset
    13
  well-known from Haskell.  @{const Let} is printed
0d6b64060543 State_Monad uses Monad_Syntax
krauss
parents: 37790
diff changeset
    14
  specially in do-expressions.
0d6b64060543 State_Monad uses Monad_Syntax
krauss
parents: 37790
diff changeset
    15
*}
0d6b64060543 State_Monad uses Monad_Syntax
krauss
parents: 37790
diff changeset
    16
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    17
consts
37816
e550439d4422 dropped M suffix; added predicate monad bind
haftmann
parents: 37791
diff changeset
    18
  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    19
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    20
notation (xsymbols)
37816
e550439d4422 dropped M suffix; added predicate monad bind
haftmann
parents: 37791
diff changeset
    21
  bind (infixr "\<guillemotright>=" 54)
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    22
37848
a33ecf47f0a0 bind and then latex symbols
haftmann
parents: 37823
diff changeset
    23
notation (latex output)
a33ecf47f0a0 bind and then latex symbols
haftmann
parents: 37823
diff changeset
    24
  bind (infixr "\<bind>" 54)
a33ecf47f0a0 bind and then latex symbols
haftmann
parents: 37823
diff changeset
    25
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    26
abbreviation (do_notation)
37816
e550439d4422 dropped M suffix; added predicate monad bind
haftmann
parents: 37791
diff changeset
    27
  bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    28
where
37816
e550439d4422 dropped M suffix; added predicate monad bind
haftmann
parents: 37791
diff changeset
    29
  "bind_do \<equiv> bind"
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    30
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    31
notation (output)
37816
e550439d4422 dropped M suffix; added predicate monad bind
haftmann
parents: 37791
diff changeset
    32
  bind_do (infixr ">>=" 54)
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    33
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    34
notation (xsymbols output)
37816
e550439d4422 dropped M suffix; added predicate monad bind
haftmann
parents: 37791
diff changeset
    35
  bind_do (infixr "\<guillemotright>=" 54)
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    36
37848
a33ecf47f0a0 bind and then latex symbols
haftmann
parents: 37823
diff changeset
    37
notation (latex output)
a33ecf47f0a0 bind and then latex symbols
haftmann
parents: 37823
diff changeset
    38
  bind_do (infixr "\<bind>" 54)
a33ecf47f0a0 bind and then latex symbols
haftmann
parents: 37823
diff changeset
    39
41229
d797baa3d57c replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents: 39151
diff changeset
    40
nonterminal do_binds and do_bind
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    41
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    42
syntax
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    43
  "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    44
  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ <-/ _)" 13)
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    45
  "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    46
  "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    47
  "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    48
  "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    49
  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54)
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    50
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    51
syntax (xsymbols)
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    52
  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    53
  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    54
37848
a33ecf47f0a0 bind and then latex symbols
haftmann
parents: 37823
diff changeset
    55
syntax (latex output)
a33ecf47f0a0 bind and then latex symbols
haftmann
parents: 37823
diff changeset
    56
  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<then>" 54)
a33ecf47f0a0 bind and then latex symbols
haftmann
parents: 37823
diff changeset
    57
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    58
translations
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    59
  "_do_block (_do_cons (_do_then t) (_do_final e))"
37816
e550439d4422 dropped M suffix; added predicate monad bind
haftmann
parents: 37791
diff changeset
    60
    == "CONST bind_do t (\<lambda>_. e)"
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    61
  "_do_block (_do_cons (_do_bind p t) (_do_final e))"
37816
e550439d4422 dropped M suffix; added predicate monad bind
haftmann
parents: 37791
diff changeset
    62
    == "CONST bind_do t (\<lambda>p. e)"
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    63
  "_do_block (_do_cons (_do_let p t) bs)"
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    64
    == "let p = t in _do_block bs"
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    65
  "_do_block (_do_cons b (_do_cons c cs))"
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    66
    == "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    67
  "_do_cons (_do_let p t) (_do_final s)"
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    68
    == "_do_final (let p = t in s)"
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    69
  "_do_block (_do_final e)" => "e"
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    70
  "(m >> n)" => "(m >>= (\<lambda>_. n))"
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    71
37816
e550439d4422 dropped M suffix; added predicate monad bind
haftmann
parents: 37791
diff changeset
    72
setup {*
e550439d4422 dropped M suffix; added predicate monad bind
haftmann
parents: 37791
diff changeset
    73
  Adhoc_Overloading.add_overloaded @{const_name bind}
45964
7b3a18670a9f added monad instance for `set`
haftmann
parents: 45145
diff changeset
    74
  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Set.bind}
37816
e550439d4422 dropped M suffix; added predicate monad bind
haftmann
parents: 37791
diff changeset
    75
  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
39151
fd179beb8cb3 enabled do notation for option type
krauss
parents: 37848
diff changeset
    76
  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
45145
d5086da3c32d monadic bind
haftmann
parents: 41229
diff changeset
    77
  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name More_List.bind}
37816
e550439d4422 dropped M suffix; added predicate monad bind
haftmann
parents: 37791
diff changeset
    78
*}
37790
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    79
7fea92005066 uniform do notation for monads
krauss
parents:
diff changeset
    80
end