|
(* Title: HOL/Library/Monad_Syntax.thy
Author: Alexander Krauss, TU Muenchen
Author: Christian Sternagel, University of Innsbruck
*)
section \<open>Monad notation for arbitrary types\<close>
theory Monad_Syntax
imports Adhoc_Overloading
begin
text \<open>
We provide a convenient do-notation for monadic expressions well-known from Haskell.
const>\<open>Let\<close> is printed specially in do-expressions.
\<close>
consts
bind :: "'a \ ('b \ 'c) \ 'd" (infixl "\" 54)
notation (ASCII)
bind (infixl ">>=" 54)
abbreviation (do_notation)
bind_do :: "'a \ ('b \ 'c) \ 'd"
where "bind_do \ bind"
notation (output)
bind_do (infixl "\" 54)
notation (ASCII output)
bind_do (infixl ">>=" 54)
nonterminal do_binds and do_bind
syntax
"_do_block" :: "do_binds \ 'a" ("do {//(2 _)//}" [12] 62)
"_do_bind" :: "[pttrn, 'a] \ do_bind" ("(2_ \/ _)" 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] \ 'c" (infixl "\" 54)
syntax (ASCII)
"_do_bind" :: "[pttrn, 'a] \ do_bind" ("(2_ <-/ _)" 13)
"_thenM" :: "['a, 'b] \ 'c" (infixl ">>" 54)
translations
"_do_block (_do_cons (_do_then t) (_do_final e))"
\<rightleftharpoons> "CONST bind_do t (\<lambda>_. e)"
"_do_block (_do_cons (_do_bind p t) (_do_final e))"
\<rightleftharpoons> "CONST bind_do t (\<lambda>p. e)"
"_do_block (_do_cons (_do_let p t) bs)"
\<rightleftharpoons> "let p = t in _do_block bs"
"_do_block (_do_cons b (_do_cons c cs))"
\<rightleftharpoons> "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
"_do_cons (_do_let p t) (_do_final s)"
\<rightleftharpoons> "_do_final (let p = t in s)"
"_do_block (_do_final e)" \<rightharpoonup> "e"
"(m \ n)" \ "(m \ (\_. n))"
adhoc_overloading
bind Set.bind Predicate.bind Option.bind List.bind
end
¤ Dauer der Verarbeitung: 0.25 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
