uniform do notation for monads
authorkrauss
Tue Jul 13 00:15:37 2010 +0200 (2010-07-13)
changeset 377907fea92005066
parent 37789 93f6dcf9ec02
child 37791 0d6b64060543
uniform do notation for monads
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Monad_Syntax.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Jul 13 00:15:37 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jul 13 00:15:37 2010 +0200
     1.3 @@ -414,8 +414,8 @@
     1.4    Library/LaTeXsugar.thy Library/Lattice_Algebras.thy			\
     1.5    Library/Lattice_Syntax.thy Library/Library.thy			\
     1.6    Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy	\
     1.7 -  Library/More_List.thy Library/More_Set.thy Library/Multiset.thy	\
     1.8 -  Library/Nat_Bijection.thy Library/Nat_Infinity.thy			\
     1.9 +  Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy	\
    1.10 +  Library/Multiset.thy Library/Nat_Bijection.thy Library/Nat_Infinity.thy	\
    1.11    Library/Nested_Environment.thy Library/Numeral_Type.thy		\
    1.12    Library/OptionalSugar.thy Library/Order_Relation.thy			\
    1.13    Library/Permutation.thy Library/Permutations.thy			\
     2.1 --- a/src/HOL/Library/Library.thy	Tue Jul 13 00:15:37 2010 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Tue Jul 13 00:15:37 2010 +0200
     2.3 @@ -32,6 +32,7 @@
     2.4    ListVector
     2.5    Kleene_Algebra
     2.6    Mapping
     2.7 +  Monad_Syntax
     2.8    More_List
     2.9    Multiset
    2.10    Nat_Infinity
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Tue Jul 13 00:15:37 2010 +0200
     3.3 @@ -0,0 +1,60 @@
     3.4 +(* Author: Alexander Krauss, TU Muenchen
     3.5 +   Author: Christian Sternagel, University of Innsbruck
     3.6 +*)
     3.7 +
     3.8 +header {* Monad notation for arbitrary types *}
     3.9 +
    3.10 +theory Monad_Syntax
    3.11 +imports Adhoc_Overloading
    3.12 +begin
    3.13 +
    3.14 +consts
    3.15 +  bindM :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
    3.16 +
    3.17 +notation (xsymbols)
    3.18 +  bindM (infixr "\<guillemotright>=" 54)
    3.19 +
    3.20 +abbreviation (do_notation)
    3.21 +  bindM_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
    3.22 +where
    3.23 +  "bindM_do \<equiv> bindM"
    3.24 +
    3.25 +notation (output)
    3.26 +  bindM_do (infixr ">>=" 54)
    3.27 +
    3.28 +notation (xsymbols output)
    3.29 +  bindM_do (infixr "\<guillemotright>=" 54)
    3.30 +
    3.31 +nonterminals
    3.32 +  do_binds do_bind
    3.33 +
    3.34 +syntax
    3.35 +  "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
    3.36 +  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ <-/ _)" 13)
    3.37 +  "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
    3.38 +  "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
    3.39 +  "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
    3.40 +  "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
    3.41 +  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54)
    3.42 +
    3.43 +syntax (xsymbols)
    3.44 +  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
    3.45 +  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
    3.46 +
    3.47 +translations
    3.48 +  "_do_block (_do_cons (_do_then t) (_do_final e))"
    3.49 +    == "CONST bindM_do t (\<lambda>_. e)"
    3.50 +  "_do_block (_do_cons (_do_bind p t) (_do_final e))"
    3.51 +    == "CONST bindM_do t (\<lambda>p. e)"
    3.52 +  "_do_block (_do_cons (_do_let p t) bs)"
    3.53 +    == "let p = t in _do_block bs"
    3.54 +  "_do_block (_do_cons b (_do_cons c cs))"
    3.55 +    == "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
    3.56 +  "_do_cons (_do_let p t) (_do_final s)"
    3.57 +    == "_do_final (let p = t in s)"
    3.58 +  "_do_block (_do_final e)" => "e"
    3.59 +  "(m >> n)" => "(m >>= (\<lambda>_. n))"
    3.60 +
    3.61 +setup {* Adhoc_Overloading.add_overloaded @{const_name bindM} *}
    3.62 +
    3.63 +end