--- 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 {*