State_Monad uses Monad_Syntax

--- a/src/HOL/Extraction/Higman.thy	Tue Jul 13 00:15:37 2010 +0200
+++ b/src/HOL/Extraction/Higman.thy	Tue Jul 13 11:50:22 2010 +0200
@@ -350,15 +350,14 @@
 end
 
 function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
-  "mk_word_aux k = (do
+  "mk_word_aux k = (do {
      i \<leftarrow> Random.range 10;
      (if i > 7 \<and> k > 2 \<or> k > 1000 then return []
-     else do
+     else do {
        let l = (if i mod 2 = 0 then A else B);
        ls \<leftarrow> mk_word_aux (Suc k);
        return (l # ls)
-     done)
-   done)"
+     })})"
 by pat_completeness auto
 termination by (relation "measure ((op -) 1001)") auto
 
@@ -367,10 +366,10 @@
 
 primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
   "mk_word_s 0 = mk_word"
-  | "mk_word_s (Suc n) = (do
+  | "mk_word_s (Suc n) = (do {
        _ \<leftarrow> mk_word;
        mk_word_s n
-     done)"
+     })"
 
 definition g1 :: "nat \<Rightarrow> letter list" where
   "g1 s = fst (mk_word_s s (20000, 1))"

--- a/src/HOL/Library/Monad_Syntax.thy	Tue Jul 13 00:15:37 2010 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy	Tue Jul 13 11:50:22 2010 +0200
@@ -8,6 +8,12 @@
 imports Adhoc_Overloading
 begin
 
+text {*
+  We provide a convenient do-notation for monadic expressions
+  well-known from Haskell.  @{const Let} is printed
+  specially in do-expressions.
+*}
+
 consts
   bindM :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
 

--- a/src/HOL/Library/State_Monad.thy	Tue Jul 13 00:15:37 2010 +0200
+++ b/src/HOL/Library/State_Monad.thy	Tue Jul 13 11:50:22 2010 +0200
@@ -5,7 +5,7 @@
 header {* Combinator syntax for generic, open state monads (single threaded monads) *}
 
 theory State_Monad
-imports Main
+imports Monad_Syntax
 begin
 
 subsection {* Motivation *}
@@ -112,86 +112,8 @@
 
 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
 
-
-subsection {* Syntax *}
-
-text {*
-  We provide a convenient do-notation for monadic expressions
-  well-known from Haskell.  @{const Let} is printed
-  specially in do-expressions.
-*}
-
-nonterminals do_expr
-
-syntax
-  "_do" :: "do_expr \<Rightarrow> 'a"
-    ("do _ done" [12] 12)
-  "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
-    ("_ <- _;// _" [1000, 13, 12] 12)
-  "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
-    ("_;// _" [13, 12] 12)
-  "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
-    ("let _ = _;// _" [1000, 13, 12] 12)
-  "_done" :: "'a \<Rightarrow> do_expr"
-    ("_" [12] 12)
-
-syntax (xsymbols)
-  "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
-    ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
-
-translations
-  "_do f" => "f"
-  "_scomp x f g" => "f \<circ>\<rightarrow> (\<lambda>x. g)"
-  "_fcomp f g" => "f \<circ>> g"
-  "_let x t f" => "CONST Let t (\<lambda>x. f)"
-  "_done f" => "f"
-
-print_translation {*
-let
-  fun dest_abs_eta (Abs (abs as (_, ty, _))) =
-        let
-          val (v, t) = Syntax.variant_abs abs;
-        in (Free (v, ty), t) end
-    | dest_abs_eta t =
-        let
-          val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
-        in (Free (v, dummyT), t) end;
-  fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
-        let
-          val (v, g') = dest_abs_eta g;
-        in Const (@{syntax_const "_scomp"}, dummyT) $ v $ f $ unfold_monad g' end
-    | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
-        Const (@{syntax_const "_fcomp"}, dummyT) $ f $ unfold_monad g
-    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
-        let
-          val (v, g') = dest_abs_eta g;
-        in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
-    | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
-        Const (@{const_syntax "return"}, dummyT) $ f
-    | unfold_monad f = f;
-  fun contains_scomp (Const (@{const_syntax scomp}, _) $ _ $ _) = true
-    | contains_scomp (Const (@{const_syntax fcomp}, _) $ _ $ t) =
-        contains_scomp t
-    | contains_scomp (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
-        contains_scomp t;
-  fun scomp_monad_tr' (f::g::ts) = list_comb
-    (Const (@{syntax_const "_do"}, dummyT) $
-      unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
-  fun fcomp_monad_tr' (f::g::ts) =
-    if contains_scomp g then list_comb
-      (Const (@{syntax_const "_do"}, dummyT) $
-        unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
-    else raise Match;
-  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
-    if contains_scomp g' then list_comb
-      (Const (@{syntax_const "_do"}, dummyT) $
-        unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
-    else raise Match;
-in
- [(@{const_syntax scomp}, scomp_monad_tr'),
-  (@{const_syntax fcomp}, fcomp_monad_tr'),
-  (@{const_syntax Let}, Let_monad_tr')]
-end;
+setup {*
+  Adhoc_Overloading.add_variant @{const_name bindM} @{const_name scomp}
 *}
 
 text {*