SSL Monad_Syntax.thy Sprache: Isabelle

(*  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 Main
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 \<open>>>=\<close> 54)

abbreviation (do_notation)
  bind_do :: "'a \ ('b \ 'c) \ 'd"
  where "bind_do \ bind"

notation (output)
  bind_do (infixl \<open>\<bind>\<close> 54)

notation (ASCII output)
  bind_do (infixl \<open>>>=\<close> 54)

nonterminal do_binds and do_bind
syntax
  "_do_block" :: "do_binds \ 'a"
    (\<open>(\<open>open_block notation=\<open>mixfix do block\<close>\<close>do {//(2  _)//})\<close> [12] 62)
  "_do_bind"  :: "[pttrn, 'a] \ do_bind"
    (\<open>(\<open>indent=2 notation=\<open>infix do bind\<close>\<close>_ \<leftarrow>/ _)\<close> 13)
  "_do_let" :: "[pttrn, 'a] \ do_bind"
    (\<open>(\<open>indent=2 notation=\<open>infix do let\<close>\<close>let _ =/ _)\<close> [1000, 13] 13)
  "_do_then" :: "'a \ do_bind" (\_\ [14] 13)
  "_do_final" :: "'a \ do_binds" (\_\)
  "_do_cons" :: "[do_bind, do_binds] \ do_binds"
    (\<open>(\<open>open_block notation=\<open>infix do next\<close>\<close>_;//_)\<close> [13, 12] 12)
  "_thenM" :: "['a, 'b] \ 'c" (infixl \\\ 54)

syntax (ASCII)
  "_do_bind" :: "[pttrn, 'a] \ do_bind"
    (\<open>(\<open>indent=2 notation=\<open>infix do bind\<close>\<close>_ <-/ _)\<close> 13)
  "_thenM" :: "['a, 'b] \ 'c" (infixl \>>\ 54)

syntax_consts
  "_do_block" "_do_cons" "_do_bind" "_do_then" \<rightleftharpoons> bind and
  "_do_let" \<rightleftharpoons> Let

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 \<rightleftharpoons> Set.bind Predicate.bind Option.bind List.bind

end

quality82%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.