improved syntax
authorhaftmann
Fri Nov 10 07:37:35 2006 +0100 (2006-11-10)
changeset 21283b15355b9a59d
parent 21282 dd647b4d7952
child 21284 36613fe4cf05
improved syntax
src/HOL/Library/State_Monad.thy
     1.1 --- a/src/HOL/Library/State_Monad.thy	Fri Nov 10 00:46:00 2006 +0100
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Fri Nov 10 07:37:35 2006 +0100
     1.3 @@ -68,19 +68,23 @@
     1.4  
     1.5  definition
     1.6    mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
     1.7 -    (infixl "\<guillemotright>=" 60)
     1.8 -  "f \<guillemotright>= g = split g \<circ> f"
     1.9 +    (infixl ">>=" 60)
    1.10 +  "f >>= g = split g \<circ> f"
    1.11    fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    1.12 -    (infixl "\<guillemotright>" 60)
    1.13 -  "f \<guillemotright> g = g \<circ> f"
    1.14 +    (infixl ">>" 60)
    1.15 +  "f >> g = g \<circ> f"
    1.16    run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.17    "run f = f"
    1.18  
    1.19 -syntax (input)
    1.20 +print_ast_translation {*[
    1.21 +  (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
    1.22 +]*}
    1.23 +
    1.24 +syntax (xsymbols)
    1.25    mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    1.26 -    (infixl ">>=" 60)
    1.27 +    (infixl "\<guillemotright>=" 60)
    1.28    fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    1.29 -    (infixl ">>" 60)
    1.30 +    (infixl "\<guillemotright>" 60)
    1.31  
    1.32  abbreviation (input)
    1.33    "return \<equiv> Pair"
    1.34 @@ -109,7 +113,7 @@
    1.35    \begin{itemize}
    1.36      \item The monad model does not state anything about
    1.37         the kind of state; the model for the state is
    1.38 -       completely orthogonal and has (or may) be
    1.39 +       completely orthogonal and has to (or may) be
    1.40         specified completely independent.
    1.41      \item There is no distinguished type constructor
    1.42         encapsulating away the state transformation, i.e.~transformations
    1.43 @@ -225,6 +229,7 @@
    1.44          else t
    1.45      | unfold_monad (Const ("Let", _) $ f $ g) =
    1.46          let
    1.47 +          
    1.48            val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
    1.49          in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
    1.50      | unfold_monad (Const ("Pair", _) $ f) =
    1.51 @@ -237,10 +242,6 @@
    1.52  ] end;
    1.53  *}
    1.54  
    1.55 -print_ast_translation {*[
    1.56 -  (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
    1.57 -]*}
    1.58 -
    1.59  text {*
    1.60    For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
    1.61  *}