src/HOL/Library/Monad_Syntax.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 62189 116f41763b2b
child 66263 466d8e7ed170
permissions -rw-r--r--
executable domain membership checks
     1 (* Author: Alexander Krauss, TU Muenchen
     2    Author: Christian Sternagel, University of Innsbruck
     3 *)
     4 
     5 section \<open>Monad notation for arbitrary types\<close>
     6 
     7 theory Monad_Syntax
     8 imports Main "~~/src/Tools/Adhoc_Overloading"
     9 begin
    10 
    11 text \<open>
    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 \<close>
    16 
    17 consts
    18   bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr "\<bind>" 54)
    19 
    20 notation (ASCII)
    21   bind (infixr ">>=" 54)
    22 
    23 
    24 abbreviation (do_notation)
    25   bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd"
    26   where "bind_do \<equiv> bind"
    27 
    28 notation (output)
    29   bind_do (infixr "\<bind>" 54)
    30 
    31 notation (ASCII output)
    32   bind_do (infixr ">>=" 54)
    33 
    34 
    35 nonterminal do_binds and do_bind
    36 syntax
    37   "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
    38   "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
    39   "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
    40   "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
    41   "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
    42   "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
    43   "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)
    44 
    45 syntax (ASCII)
    46   "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
    47   "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
    48 
    49 translations
    50   "_do_block (_do_cons (_do_then t) (_do_final e))"
    51     \<rightleftharpoons> "CONST bind_do t (\<lambda>_. e)"
    52   "_do_block (_do_cons (_do_bind p t) (_do_final e))"
    53     \<rightleftharpoons> "CONST bind_do t (\<lambda>p. e)"
    54   "_do_block (_do_cons (_do_let p t) bs)"
    55     \<rightleftharpoons> "let p = t in _do_block bs"
    56   "_do_block (_do_cons b (_do_cons c cs))"
    57     \<rightleftharpoons> "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
    58   "_do_cons (_do_let p t) (_do_final s)"
    59     \<rightleftharpoons> "_do_final (let p = t in s)"
    60   "_do_block (_do_final e)" \<rightharpoonup> "e"
    61   "(m \<then> n)" \<rightharpoonup> "(m \<bind> (\<lambda>_. n))"
    62 
    63 adhoc_overloading
    64   bind Set.bind Predicate.bind Option.bind List.bind
    65 
    66 end