src/HOL/Library/Monad_Syntax.thy
author wenzelm
Tue May 01 20:40:27 2018 +0200 (14 months ago)
changeset 68061 81d90f830f99
parent 66608 f3e7a1418979
child 69593 3dda49e08b9d
permissions -rw-r--r--
clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
tuned headers;
wenzelm@68061
     1
(*  Title:      HOL/Library/Monad_Syntax.thy
wenzelm@68061
     2
    Author:     Alexander Krauss, TU Muenchen
wenzelm@68061
     3
    Author:     Christian Sternagel, University of Innsbruck
krauss@37790
     4
*)
krauss@37790
     5
wenzelm@60500
     6
section \<open>Monad notation for arbitrary types\<close>
krauss@37790
     7
krauss@37790
     8
theory Monad_Syntax
wenzelm@68061
     9
  imports Adhoc_Overloading
krauss@37790
    10
begin
krauss@37790
    11
wenzelm@60500
    12
text \<open>
krauss@37791
    13
  We provide a convenient do-notation for monadic expressions
krauss@37791
    14
  well-known from Haskell.  @{const Let} is printed
krauss@37791
    15
  specially in do-expressions.
wenzelm@60500
    16
\<close>
krauss@37791
    17
krauss@37790
    18
consts
wenzelm@62026
    19
  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr "\<bind>" 54)
krauss@37790
    20
wenzelm@61955
    21
notation (ASCII)
wenzelm@61955
    22
  bind (infixr ">>=" 54)
krauss@37790
    23
wenzelm@61955
    24
krauss@37790
    25
abbreviation (do_notation)
Christian@53616
    26
  bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd"
wenzelm@61955
    27
  where "bind_do \<equiv> bind"
krauss@37790
    28
krauss@37790
    29
notation (output)
wenzelm@62026
    30
  bind_do (infixr "\<bind>" 54)
krauss@37790
    31
wenzelm@61955
    32
notation (ASCII output)
wenzelm@61955
    33
  bind_do (infixr ">>=" 54)
krauss@37790
    34
wenzelm@61955
    35
wenzelm@41229
    36
nonterminal do_binds and do_bind
krauss@37790
    37
syntax
krauss@37790
    38
  "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
wenzelm@61955
    39
  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
krauss@37790
    40
  "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
krauss@37790
    41
  "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
krauss@37790
    42
  "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
krauss@37790
    43
  "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
wenzelm@62026
    44
  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)
krauss@37790
    45
wenzelm@61955
    46
syntax (ASCII)
wenzelm@61955
    47
  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
wenzelm@61955
    48
  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
krauss@37790
    49
krauss@37790
    50
translations
krauss@37790
    51
  "_do_block (_do_cons (_do_then t) (_do_final e))"
wenzelm@62035
    52
    \<rightleftharpoons> "CONST bind_do t (\<lambda>_. e)"
krauss@37790
    53
  "_do_block (_do_cons (_do_bind p t) (_do_final e))"
wenzelm@62035
    54
    \<rightleftharpoons> "CONST bind_do t (\<lambda>p. e)"
krauss@37790
    55
  "_do_block (_do_cons (_do_let p t) bs)"
wenzelm@62035
    56
    \<rightleftharpoons> "let p = t in _do_block bs"
krauss@37790
    57
  "_do_block (_do_cons b (_do_cons c cs))"
wenzelm@62035
    58
    \<rightleftharpoons> "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
krauss@37790
    59
  "_do_cons (_do_let p t) (_do_final s)"
wenzelm@62035
    60
    \<rightleftharpoons> "_do_final (let p = t in s)"
wenzelm@62189
    61
  "_do_block (_do_final e)" \<rightharpoonup> "e"
wenzelm@62035
    62
  "(m \<then> n)" \<rightharpoonup> "(m \<bind> (\<lambda>_. n))"
krauss@37790
    63
wenzelm@52622
    64
adhoc_overloading
wenzelm@66608
    65
  bind Set.bind Predicate.bind Option.bind List.bind
krauss@37790
    66
wenzelm@66608
    67
end