76 |
76 |
77 definition |
77 definition |
78 run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where |
78 run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where |
79 "run f = f" |
79 "run f = f" |
80 |
80 |
81 print_ast_translation {*[ |
|
82 (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts) |
|
83 ]*} |
|
84 |
|
85 syntax (xsymbols) |
81 syntax (xsymbols) |
86 mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" |
82 mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" |
87 (infixl "\<guillemotright>=" 60) |
83 (infixl "\<guillemotright>=" 60) |
88 fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" |
84 fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" |
89 (infixl "\<guillemotright>" 60) |
85 (infixl "\<guillemotright>" 60) |
90 |
86 |
91 abbreviation (input) |
87 abbreviation (input) |
92 "return \<equiv> Pair" |
88 "return \<equiv> Pair" |
|
89 |
|
90 print_ast_translation {*[ |
|
91 (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts) |
|
92 ]*} |
93 |
93 |
94 text {* |
94 text {* |
95 Given two transformations @{term f} and @{term g}, they |
95 Given two transformations @{term f} and @{term g}, they |
96 may be directly composed using the @{term "op \<guillemotright>"} combinator, |
96 may be directly composed using the @{term "op \<guillemotright>"} combinator, |
97 forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}. |
97 forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}. |