State_Monad uses Monad_Syntax
authorkrauss
Tue Jul 13 11:50:22 2010 +0200 (2010-07-13)
changeset 377910d6b64060543
parent 37790 7fea92005066
child 37792 ba0bc31b90d7
State_Monad uses Monad_Syntax
src/HOL/Extraction/Higman.thy
src/HOL/Library/Monad_Syntax.thy
src/HOL/Library/State_Monad.thy
     1.1 --- a/src/HOL/Extraction/Higman.thy	Tue Jul 13 00:15:37 2010 +0200
     1.2 +++ b/src/HOL/Extraction/Higman.thy	Tue Jul 13 11:50:22 2010 +0200
     1.3 @@ -350,15 +350,14 @@
     1.4  end
     1.5  
     1.6  function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
     1.7 -  "mk_word_aux k = (do
     1.8 +  "mk_word_aux k = (do {
     1.9       i \<leftarrow> Random.range 10;
    1.10       (if i > 7 \<and> k > 2 \<or> k > 1000 then return []
    1.11 -     else do
    1.12 +     else do {
    1.13         let l = (if i mod 2 = 0 then A else B);
    1.14         ls \<leftarrow> mk_word_aux (Suc k);
    1.15         return (l # ls)
    1.16 -     done)
    1.17 -   done)"
    1.18 +     })})"
    1.19  by pat_completeness auto
    1.20  termination by (relation "measure ((op -) 1001)") auto
    1.21  
    1.22 @@ -367,10 +366,10 @@
    1.23  
    1.24  primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
    1.25    "mk_word_s 0 = mk_word"
    1.26 -  | "mk_word_s (Suc n) = (do
    1.27 +  | "mk_word_s (Suc n) = (do {
    1.28         _ \<leftarrow> mk_word;
    1.29         mk_word_s n
    1.30 -     done)"
    1.31 +     })"
    1.32  
    1.33  definition g1 :: "nat \<Rightarrow> letter list" where
    1.34    "g1 s = fst (mk_word_s s (20000, 1))"
     2.1 --- a/src/HOL/Library/Monad_Syntax.thy	Tue Jul 13 00:15:37 2010 +0200
     2.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Tue Jul 13 11:50:22 2010 +0200
     2.3 @@ -8,6 +8,12 @@
     2.4  imports Adhoc_Overloading
     2.5  begin
     2.6  
     2.7 +text {*
     2.8 +  We provide a convenient do-notation for monadic expressions
     2.9 +  well-known from Haskell.  @{const Let} is printed
    2.10 +  specially in do-expressions.
    2.11 +*}
    2.12 +
    2.13  consts
    2.14    bindM :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
    2.15  
     3.1 --- a/src/HOL/Library/State_Monad.thy	Tue Jul 13 00:15:37 2010 +0200
     3.2 +++ b/src/HOL/Library/State_Monad.thy	Tue Jul 13 11:50:22 2010 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Combinator syntax for generic, open state monads (single threaded monads) *}
     3.5  
     3.6  theory State_Monad
     3.7 -imports Main
     3.8 +imports Monad_Syntax
     3.9  begin
    3.10  
    3.11  subsection {* Motivation *}
    3.12 @@ -112,86 +112,8 @@
    3.13  
    3.14  lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
    3.15  
    3.16 -
    3.17 -subsection {* Syntax *}
    3.18 -
    3.19 -text {*
    3.20 -  We provide a convenient do-notation for monadic expressions
    3.21 -  well-known from Haskell.  @{const Let} is printed
    3.22 -  specially in do-expressions.
    3.23 -*}
    3.24 -
    3.25 -nonterminals do_expr
    3.26 -
    3.27 -syntax
    3.28 -  "_do" :: "do_expr \<Rightarrow> 'a"
    3.29 -    ("do _ done" [12] 12)
    3.30 -  "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    3.31 -    ("_ <- _;// _" [1000, 13, 12] 12)
    3.32 -  "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    3.33 -    ("_;// _" [13, 12] 12)
    3.34 -  "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    3.35 -    ("let _ = _;// _" [1000, 13, 12] 12)
    3.36 -  "_done" :: "'a \<Rightarrow> do_expr"
    3.37 -    ("_" [12] 12)
    3.38 -
    3.39 -syntax (xsymbols)
    3.40 -  "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    3.41 -    ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
    3.42 -
    3.43 -translations
    3.44 -  "_do f" => "f"
    3.45 -  "_scomp x f g" => "f \<circ>\<rightarrow> (\<lambda>x. g)"
    3.46 -  "_fcomp f g" => "f \<circ>> g"
    3.47 -  "_let x t f" => "CONST Let t (\<lambda>x. f)"
    3.48 -  "_done f" => "f"
    3.49 -
    3.50 -print_translation {*
    3.51 -let
    3.52 -  fun dest_abs_eta (Abs (abs as (_, ty, _))) =
    3.53 -        let
    3.54 -          val (v, t) = Syntax.variant_abs abs;
    3.55 -        in (Free (v, ty), t) end
    3.56 -    | dest_abs_eta t =
    3.57 -        let
    3.58 -          val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
    3.59 -        in (Free (v, dummyT), t) end;
    3.60 -  fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
    3.61 -        let
    3.62 -          val (v, g') = dest_abs_eta g;
    3.63 -        in Const (@{syntax_const "_scomp"}, dummyT) $ v $ f $ unfold_monad g' end
    3.64 -    | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
    3.65 -        Const (@{syntax_const "_fcomp"}, dummyT) $ f $ unfold_monad g
    3.66 -    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
    3.67 -        let
    3.68 -          val (v, g') = dest_abs_eta g;
    3.69 -        in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
    3.70 -    | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
    3.71 -        Const (@{const_syntax "return"}, dummyT) $ f
    3.72 -    | unfold_monad f = f;
    3.73 -  fun contains_scomp (Const (@{const_syntax scomp}, _) $ _ $ _) = true
    3.74 -    | contains_scomp (Const (@{const_syntax fcomp}, _) $ _ $ t) =
    3.75 -        contains_scomp t
    3.76 -    | contains_scomp (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
    3.77 -        contains_scomp t;
    3.78 -  fun scomp_monad_tr' (f::g::ts) = list_comb
    3.79 -    (Const (@{syntax_const "_do"}, dummyT) $
    3.80 -      unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
    3.81 -  fun fcomp_monad_tr' (f::g::ts) =
    3.82 -    if contains_scomp g then list_comb
    3.83 -      (Const (@{syntax_const "_do"}, dummyT) $
    3.84 -        unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
    3.85 -    else raise Match;
    3.86 -  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
    3.87 -    if contains_scomp g' then list_comb
    3.88 -      (Const (@{syntax_const "_do"}, dummyT) $
    3.89 -        unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
    3.90 -    else raise Match;
    3.91 -in
    3.92 - [(@{const_syntax scomp}, scomp_monad_tr'),
    3.93 -  (@{const_syntax fcomp}, fcomp_monad_tr'),
    3.94 -  (@{const_syntax Let}, Let_monad_tr')]
    3.95 -end;
    3.96 +setup {*
    3.97 +  Adhoc_Overloading.add_variant @{const_name bindM} @{const_name scomp}
    3.98  *}
    3.99  
   3.100  text {*