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