# HG changeset patch # User krauss # Date 1279014622 -7200 # Node ID 0d6b64060543f59bb9f44e336479c40fa8ca59f2 # Parent 7fea92005066fd22aea598fe6e217da66c85b1aa State_Monad uses Monad_Syntax diff -r 7fea92005066 -r 0d6b64060543 src/HOL/Extraction/Higman.thy --- 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 \ Random.seed \ letter list \ Random.seed" where - "mk_word_aux k = (do + "mk_word_aux k = (do { i \ Random.range 10; (if i > 7 \ k > 2 \ k > 1000 then return [] - else do + else do { let l = (if i mod 2 = 0 then A else B); ls \ 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 \ Random.seed \ letter list \ Random.seed" where "mk_word_s 0 = mk_word" - | "mk_word_s (Suc n) = (do + | "mk_word_s (Suc n) = (do { _ \ mk_word; mk_word_s n - done)" + })" definition g1 :: "nat \ letter list" where "g1 s = fst (mk_word_s s (20000, 1))" diff -r 7fea92005066 -r 0d6b64060543 src/HOL/Library/Monad_Syntax.thy --- 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 \ 'c] \ 'c" (infixr ">>=" 54) diff -r 7fea92005066 -r 0d6b64060543 src/HOL/Library/State_Monad.thy --- 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 \ 'a" - ("do _ done" [12] 12) - "_scomp" :: "pttrn \ 'a \ do_expr \ do_expr" - ("_ <- _;// _" [1000, 13, 12] 12) - "_fcomp" :: "'a \ do_expr \ do_expr" - ("_;// _" [13, 12] 12) - "_let" :: "pttrn \ 'a \ do_expr \ do_expr" - ("let _ = _;// _" [1000, 13, 12] 12) - "_done" :: "'a \ do_expr" - ("_" [12] 12) - -syntax (xsymbols) - "_scomp" :: "pttrn \ 'a \ do_expr \ do_expr" - ("_ \ _;// _" [1000, 13, 12] 12) - -translations - "_do f" => "f" - "_scomp x f g" => "f \\ (\x. g)" - "_fcomp f g" => "f \> g" - "_let x t f" => "CONST Let t (\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 {*