src/HOL/Library/State_Monad.thy
changeset 37791 0d6b64060543
parent 37751 89e16802b6cc
child 37817 71e5546b1965
     1.1 --- a/src/HOL/Library/State_Monad.thy	Tue Jul 13 00:15:37 2010 +0200
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Tue Jul 13 11:50:22 2010 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Combinator syntax for generic, open state monads (single threaded monads) *}
     1.5  
     1.6  theory State_Monad
     1.7 -imports Main
     1.8 +imports Monad_Syntax
     1.9  begin
    1.10  
    1.11  subsection {* Motivation *}
    1.12 @@ -112,86 +112,8 @@
    1.13  
    1.14  lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
    1.15  
    1.16 -
    1.17 -subsection {* Syntax *}
    1.18 -
    1.19 -text {*
    1.20 -  We provide a convenient do-notation for monadic expressions
    1.21 -  well-known from Haskell.  @{const Let} is printed
    1.22 -  specially in do-expressions.
    1.23 -*}
    1.24 -
    1.25 -nonterminals do_expr
    1.26 -
    1.27 -syntax
    1.28 -  "_do" :: "do_expr \<Rightarrow> 'a"
    1.29 -    ("do _ done" [12] 12)
    1.30 -  "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    1.31 -    ("_ <- _;// _" [1000, 13, 12] 12)
    1.32 -  "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    1.33 -    ("_;// _" [13, 12] 12)
    1.34 -  "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    1.35 -    ("let _ = _;// _" [1000, 13, 12] 12)
    1.36 -  "_done" :: "'a \<Rightarrow> do_expr"
    1.37 -    ("_" [12] 12)
    1.38 -
    1.39 -syntax (xsymbols)
    1.40 -  "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    1.41 -    ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
    1.42 -
    1.43 -translations
    1.44 -  "_do f" => "f"
    1.45 -  "_scomp x f g" => "f \<circ>\<rightarrow> (\<lambda>x. g)"
    1.46 -  "_fcomp f g" => "f \<circ>> g"
    1.47 -  "_let x t f" => "CONST Let t (\<lambda>x. f)"
    1.48 -  "_done f" => "f"
    1.49 -
    1.50 -print_translation {*
    1.51 -let
    1.52 -  fun dest_abs_eta (Abs (abs as (_, ty, _))) =
    1.53 -        let
    1.54 -          val (v, t) = Syntax.variant_abs abs;
    1.55 -        in (Free (v, ty), t) end
    1.56 -    | dest_abs_eta t =
    1.57 -        let
    1.58 -          val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
    1.59 -        in (Free (v, dummyT), t) end;
    1.60 -  fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
    1.61 -        let
    1.62 -          val (v, g') = dest_abs_eta g;
    1.63 -        in Const (@{syntax_const "_scomp"}, dummyT) $ v $ f $ unfold_monad g' end
    1.64 -    | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
    1.65 -        Const (@{syntax_const "_fcomp"}, dummyT) $ f $ unfold_monad g
    1.66 -    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
    1.67 -        let
    1.68 -          val (v, g') = dest_abs_eta g;
    1.69 -        in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
    1.70 -    | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
    1.71 -        Const (@{const_syntax "return"}, dummyT) $ f
    1.72 -    | unfold_monad f = f;
    1.73 -  fun contains_scomp (Const (@{const_syntax scomp}, _) $ _ $ _) = true
    1.74 -    | contains_scomp (Const (@{const_syntax fcomp}, _) $ _ $ t) =
    1.75 -        contains_scomp t
    1.76 -    | contains_scomp (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
    1.77 -        contains_scomp t;
    1.78 -  fun scomp_monad_tr' (f::g::ts) = list_comb
    1.79 -    (Const (@{syntax_const "_do"}, dummyT) $
    1.80 -      unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
    1.81 -  fun fcomp_monad_tr' (f::g::ts) =
    1.82 -    if contains_scomp g then list_comb
    1.83 -      (Const (@{syntax_const "_do"}, dummyT) $
    1.84 -        unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
    1.85 -    else raise Match;
    1.86 -  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
    1.87 -    if contains_scomp g' then list_comb
    1.88 -      (Const (@{syntax_const "_do"}, dummyT) $
    1.89 -        unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
    1.90 -    else raise Match;
    1.91 -in
    1.92 - [(@{const_syntax scomp}, scomp_monad_tr'),
    1.93 -  (@{const_syntax fcomp}, fcomp_monad_tr'),
    1.94 -  (@{const_syntax Let}, Let_monad_tr')]
    1.95 -end;
    1.96 +setup {*
    1.97 +  Adhoc_Overloading.add_variant @{const_name bindM} @{const_name scomp}
    1.98  *}
    1.99  
   1.100  text {*