# HG changeset patch # User krauss # Date 1278972937 -7200 # Node ID 7fea92005066fd22aea598fe6e217da66c85b1aa # Parent 93f6dcf9ec02b239362a7792fa64f910e360b71f uniform do notation for monads diff -r 93f6dcf9ec02 -r 7fea92005066 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jul 13 00:15:37 2010 +0200 +++ b/src/HOL/IsaMakefile Tue Jul 13 00:15:37 2010 +0200 @@ -414,8 +414,8 @@ Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \ Library/Lattice_Syntax.thy Library/Library.thy \ Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \ - Library/More_List.thy Library/More_Set.thy Library/Multiset.thy \ - Library/Nat_Bijection.thy Library/Nat_Infinity.thy \ + Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \ + Library/Multiset.thy Library/Nat_Bijection.thy Library/Nat_Infinity.thy \ Library/Nested_Environment.thy Library/Numeral_Type.thy \ Library/OptionalSugar.thy Library/Order_Relation.thy \ Library/Permutation.thy Library/Permutations.thy \ diff -r 93f6dcf9ec02 -r 7fea92005066 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Tue Jul 13 00:15:37 2010 +0200 +++ b/src/HOL/Library/Library.thy Tue Jul 13 00:15:37 2010 +0200 @@ -32,6 +32,7 @@ ListVector Kleene_Algebra Mapping + Monad_Syntax More_List Multiset Nat_Infinity diff -r 93f6dcf9ec02 -r 7fea92005066 src/HOL/Library/Monad_Syntax.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Monad_Syntax.thy Tue Jul 13 00:15:37 2010 +0200 @@ -0,0 +1,60 @@ +(* Author: Alexander Krauss, TU Muenchen + Author: Christian Sternagel, University of Innsbruck +*) + +header {* Monad notation for arbitrary types *} + +theory Monad_Syntax +imports Adhoc_Overloading +begin + +consts + bindM :: "['a, 'b \ 'c] \ 'c" (infixr ">>=" 54) + +notation (xsymbols) + bindM (infixr "\=" 54) + +abbreviation (do_notation) + bindM_do :: "['a, 'b \ 'c] \ 'c" +where + "bindM_do \ bindM" + +notation (output) + bindM_do (infixr ">>=" 54) + +notation (xsymbols output) + bindM_do (infixr "\=" 54) + +nonterminals + do_binds do_bind + +syntax + "_do_block" :: "do_binds \ 'a" ("do {//(2 _)//}" [12] 62) + "_do_bind" :: "[pttrn, 'a] \ do_bind" ("(_ <-/ _)" 13) + "_do_let" :: "[pttrn, 'a] \ do_bind" ("(2let _ =/ _)" [1000, 13] 13) + "_do_then" :: "'a \ do_bind" ("_" [14] 13) + "_do_final" :: "'a \ do_binds" ("_") + "_do_cons" :: "[do_bind, do_binds] \ do_binds" ("_;//_" [13, 12] 12) + "_thenM" :: "['a, 'b] \ 'b" (infixr ">>" 54) + +syntax (xsymbols) + "_do_bind" :: "[pttrn, 'a] \ do_bind" ("(_ \/ _)" 13) + "_thenM" :: "['a, 'b] \ 'b" (infixr "\" 54) + +translations + "_do_block (_do_cons (_do_then t) (_do_final e))" + == "CONST bindM_do t (\_. e)" + "_do_block (_do_cons (_do_bind p t) (_do_final e))" + == "CONST bindM_do t (\p. e)" + "_do_block (_do_cons (_do_let p t) bs)" + == "let p = t in _do_block bs" + "_do_block (_do_cons b (_do_cons c cs))" + == "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))" + "_do_cons (_do_let p t) (_do_final s)" + == "_do_final (let p = t in s)" + "_do_block (_do_final e)" => "e" + "(m >> n)" => "(m >>= (\_. n))" + +setup {* Adhoc_Overloading.add_overloaded @{const_name bindM} *} + +end