src/HOL/Library/Monad_Syntax.thy
author wenzelm
Sat Jan 02 13:29:34 2016 +0100 (2016-01-02)
changeset 62035 b3cda398a5b1
parent 62026 ea3b1b0413b4
child 62189 116f41763b2b
permissions -rw-r--r--
more symbols;
krauss@37790
     1
(* Author: Alexander Krauss, TU Muenchen
krauss@37790
     2
   Author: Christian Sternagel, University of Innsbruck
krauss@37790
     3
*)
krauss@37790
     4
wenzelm@60500
     5
section \<open>Monad notation for arbitrary types\<close>
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
wenzelm@60500
    11
text \<open>
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.
wenzelm@60500
    15
\<close>
krauss@37791
    16
krauss@37790
    17
consts
wenzelm@62026
    18
  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr "\<bind>" 54)
krauss@37790
    19
wenzelm@61955
    20
notation (ASCII)
wenzelm@61955
    21
  bind (infixr ">>=" 54)
krauss@37790
    22
wenzelm@61955
    23
krauss@37790
    24
abbreviation (do_notation)
Christian@53616
    25
  bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd"
wenzelm@61955
    26
  where "bind_do \<equiv> bind"
krauss@37790
    27
krauss@37790
    28
notation (output)
wenzelm@62026
    29
  bind_do (infixr "\<bind>" 54)
krauss@37790
    30
wenzelm@61955
    31
notation (ASCII output)
wenzelm@61955
    32
  bind_do (infixr ">>=" 54)
krauss@37790
    33
wenzelm@61955
    34
wenzelm@41229
    35
nonterminal do_binds and do_bind
krauss@37790
    36
syntax
krauss@37790
    37
  "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
wenzelm@61955
    38
  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
krauss@37790
    39
  "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
krauss@37790
    40
  "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
krauss@37790
    41
  "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
krauss@37790
    42
  "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
wenzelm@62026
    43
  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)
krauss@37790
    44
wenzelm@61955
    45
syntax (ASCII)
wenzelm@61955
    46
  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
wenzelm@61955
    47
  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
krauss@37790
    48
krauss@37790
    49
translations
krauss@37790
    50
  "_do_block (_do_cons (_do_then t) (_do_final e))"
wenzelm@62035
    51
    \<rightleftharpoons> "CONST bind_do t (\<lambda>_. e)"
krauss@37790
    52
  "_do_block (_do_cons (_do_bind p t) (_do_final e))"
wenzelm@62035
    53
    \<rightleftharpoons> "CONST bind_do t (\<lambda>p. e)"
krauss@37790
    54
  "_do_block (_do_cons (_do_let p t) bs)"
wenzelm@62035
    55
    \<rightleftharpoons> "let p = t in _do_block bs"
krauss@37790
    56
  "_do_block (_do_cons b (_do_cons c cs))"
wenzelm@62035
    57
    \<rightleftharpoons> "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
krauss@37790
    58
  "_do_cons (_do_let p t) (_do_final s)"
wenzelm@62035
    59
    \<rightleftharpoons> "_do_final (let p = t in s)"
krauss@37790
    60
  "_do_block (_do_final e)" => "e"
wenzelm@62035
    61
  "(m \<then> n)" \<rightharpoonup> "(m \<bind> (\<lambda>_. n))"
krauss@37790
    62
wenzelm@52622
    63
adhoc_overloading
wenzelm@52622
    64
  bind Set.bind Predicate.bind Option.bind List.bind
krauss@37790
    65
krauss@37790
    66
end