37790
|
1 |
(* Author: Alexander Krauss, TU Muenchen
|
|
2 |
Author: Christian Sternagel, University of Innsbruck
|
|
3 |
*)
|
|
4 |
|
|
5 |
header {* Monad notation for arbitrary types *}
|
|
6 |
|
|
7 |
theory Monad_Syntax
|
37823
|
8 |
imports Main "~~/src/Tools/Adhoc_Overloading"
|
37790
|
9 |
begin
|
|
10 |
|
37791
|
11 |
text {*
|
|
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 |
*}
|
|
16 |
|
37790
|
17 |
consts
|
37816
|
18 |
bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
|
37790
|
19 |
|
|
20 |
notation (xsymbols)
|
37816
|
21 |
bind (infixr "\<guillemotright>=" 54)
|
37790
|
22 |
|
|
23 |
abbreviation (do_notation)
|
37816
|
24 |
bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
|
37790
|
25 |
where
|
37816
|
26 |
"bind_do \<equiv> bind"
|
37790
|
27 |
|
|
28 |
notation (output)
|
37816
|
29 |
bind_do (infixr ">>=" 54)
|
37790
|
30 |
|
|
31 |
notation (xsymbols output)
|
37816
|
32 |
bind_do (infixr "\<guillemotright>=" 54)
|
37790
|
33 |
|
|
34 |
nonterminals
|
|
35 |
do_binds do_bind
|
|
36 |
|
|
37 |
syntax
|
|
38 |
"_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2 _)//}" [12] 62)
|
|
39 |
"_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ <-/ _)" 13)
|
|
40 |
"_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
|
|
41 |
"_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
|
|
42 |
"_do_final" :: "'a \<Rightarrow> do_binds" ("_")
|
|
43 |
"_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
|
|
44 |
"_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54)
|
|
45 |
|
|
46 |
syntax (xsymbols)
|
|
47 |
"_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
|
|
48 |
"_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
|
|
49 |
|
|
50 |
translations
|
|
51 |
"_do_block (_do_cons (_do_then t) (_do_final e))"
|
37816
|
52 |
== "CONST bind_do t (\<lambda>_. e)"
|
37790
|
53 |
"_do_block (_do_cons (_do_bind p t) (_do_final e))"
|
37816
|
54 |
== "CONST bind_do t (\<lambda>p. e)"
|
37790
|
55 |
"_do_block (_do_cons (_do_let p t) bs)"
|
|
56 |
== "let p = t in _do_block bs"
|
|
57 |
"_do_block (_do_cons b (_do_cons c cs))"
|
|
58 |
== "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
|
|
59 |
"_do_cons (_do_let p t) (_do_final s)"
|
|
60 |
== "_do_final (let p = t in s)"
|
|
61 |
"_do_block (_do_final e)" => "e"
|
|
62 |
"(m >> n)" => "(m >>= (\<lambda>_. n))"
|
|
63 |
|
37816
|
64 |
setup {*
|
|
65 |
Adhoc_Overloading.add_overloaded @{const_name bind}
|
|
66 |
#> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
|
|
67 |
*}
|
37790
|
68 |
|
|
69 |
end
|