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