# HG changeset patch # User krauss # Date 1279015211 -7200 # Node ID ba0bc31b90d7503011080908314007142fdcc02c # Parent 0d6b64060543f59bb9f44e336479c40fa8ca59f2 Heap_Monad uses Monad_Syntax diff -r 0d6b64060543 -r ba0bc31b90d7 src/HOL/Imperative_HOL/Array.thy --- a/src/HOL/Imperative_HOL/Array.thy Tue Jul 13 11:50:22 2010 +0200 +++ b/src/HOL/Imperative_HOL/Array.thy Tue Jul 13 12:00:11 2010 +0200 @@ -407,25 +407,25 @@ by (simp add: upd'_def upd_return) lemma [code]: - "map_entry i f a = (do + "map_entry i f a = do { x \ nth a i; upd i (f x) a - done)" + }" by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps) lemma [code]: - "swap i x a = (do + "swap i x a = do { y \ nth a i; upd i x a; return y - done)" + }" by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps) lemma [code]: - "freeze a = (do + "freeze a = do { n \ len a; Heap_Monad.fold_map (\i. nth a i) [0.. len a; Heap_Monad.fold_map (Array.nth a) [0.. len a; Heap_Monad.fold_map (Array.nth a) [0.. ('a \ 'b Heap) \ 'b Heap" (infixl ">>=" 54) where - [code del]: "f >>= g = Heap (\h. case execute f h of +definition bind :: "'a Heap \ ('a \ 'b Heap) \ 'b Heap" where + [code del]: "bind f g = Heap (\h. case execute f h of Some (x, h') \ execute (g x) h' | None \ None)" -notation bind (infixl "\=" 54) +setup {* + Adhoc_Overloading.add_variant + @{const_name Monad_Syntax.bindM} @{const_name Heap_Monad.bind} +*} + lemma execute_bind [execute_simps]: "execute f h = Some (x, h') \ execute (f \= g) h = execute (g x) h'" @@ -314,92 +318,6 @@ lemma raise_bind [simp]: "raise e \= f = raise e" by (rule Heap_eqI) (simp add: execute_simps) -abbreviation chain :: "'a Heap \ 'b Heap \ 'b Heap" (infixl ">>" 54) where - "f >> g \ f >>= (\_. g)" - -notation chain (infixl "\" 54) - - -subsubsection {* do-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] 100) - "_bind" :: "pttrn \ 'a \ do_expr \ do_expr" - ("_ <- _;//_" [1000, 13, 12] 12) - "_chain" :: "'a \ do_expr \ do_expr" - ("_;//_" [13, 12] 12) - "_let" :: "pttrn \ 'a \ do_expr \ do_expr" - ("let _ = _;//_" [1000, 13, 12] 12) - "_nil" :: "'a \ do_expr" - ("_" [12] 12) - -syntax (xsymbols) - "_bind" :: "pttrn \ 'a \ do_expr \ do_expr" - ("_ \ _;//_" [1000, 13, 12] 12) - -translations - "_do f" => "f" - "_bind x f g" => "f \= (\x. g)" - "_chain f g" => "f \ g" - "_let x t f" => "CONST Let t (\x. f)" - "_nil 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 bind}, _) $ f $ g) = - let - val (v, g') = dest_abs_eta g; - val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v []; - val v_used = fold_aterms - (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false; - in if v_used then - Const (@{syntax_const "_bind"}, dummyT) $ v $ f $ unfold_monad g' - else - Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g' - end - | unfold_monad (Const (@{const_syntax chain}, _) $ f $ g) = - Const (@{syntax_const "_chain"}, 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_bind (Const (@{const_syntax bind}, _) $ _ $ _) = true - | contains_bind (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) = - contains_bind t; - fun bind_monad_tr' (f::g::ts) = list_comb - (Const (@{syntax_const "_do"}, dummyT) $ - unfold_monad (Const (@{const_syntax bind}, dummyT) $ f $ g), ts); - fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = - if contains_bind 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 bind}, bind_monad_tr'), - (@{const_syntax Let}, Let_monad_tr')] -end; -*} - subsection {* Generic combinators *} @@ -451,11 +369,11 @@ primrec fold_map :: "('a \ 'b Heap) \ 'a list \ 'b list Heap" where "fold_map f [] = return []" -| "fold_map f (x # xs) = do +| "fold_map f (x # xs) = do { y \ f x; ys \ fold_map f xs; return (y # ys) - done" + }" lemma fold_map_append: "fold_map f (xs @ ys) = fold_map f xs \= (\xs. fold_map f ys \= (\ys. return (xs @ ys)))" @@ -611,7 +529,7 @@ text {* Monad *} code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _") -code_monad "op \=" Haskell +code_monad bind Haskell code_const return (Haskell "return") code_const Heap_Monad.raise' (Haskell "error/ _") diff -r 0d6b64060543 -r ba0bc31b90d7 src/HOL/Imperative_HOL/Mrec.thy --- a/src/HOL/Imperative_HOL/Mrec.thy Tue Jul 13 11:50:22 2010 +0200 +++ b/src/HOL/Imperative_HOL/Mrec.thy Tue Jul 13 12:00:11 2010 +0200 @@ -64,13 +64,12 @@ lemma MREC_rule: "MREC x = - (do y \ f x; + do { y \ f x; (case y of Inl r \ return r | Inr s \ - do z \ MREC s ; - g x s z - done) done)" + do { z \ MREC s ; + g x s z })}" unfolding MREC_def unfolding bind_def return_def apply simp diff -r 0d6b64060543 -r ba0bc31b90d7 src/HOL/Imperative_HOL/Ref.thy --- a/src/HOL/Imperative_HOL/Ref.thy Tue Jul 13 11:50:22 2010 +0200 +++ b/src/HOL/Imperative_HOL/Ref.thy Tue Jul 13 12:00:11 2010 +0200 @@ -48,12 +48,12 @@ [code del]: "update r v = Heap_Monad.heap (\h. ((), set r v h))" definition change :: "('a\heap \ 'a) \ 'a ref \ 'a Heap" where - "change f r = (do + "change f r = do { x \ ! r; let y = f x; r := y; return y - done)" + }" subsection {* Properties *} diff -r 0d6b64060543 -r ba0bc31b90d7 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jul 13 11:50:22 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jul 13 12:00:11 2010 +0200 @@ -12,14 +12,14 @@ definition swap :: "nat array \ nat \ nat \ unit Heap" where - "swap arr i j = ( - do + "swap arr i j = + do { x \ nth arr i; y \ nth arr j; upd i y arr; upd j x arr; return () - done)" + }" lemma crel_swapI [crel_intros]: assumes "i < Array.length a h" "j < Array.length a h" @@ -40,12 +40,12 @@ where "part1 a left right p = ( if (right \ left) then return right - else (do + else do { v \ nth a left; (if (v \ p) then (part1 a (left + 1) right p) - else (do swap a left right; - part1 a left (right - 1) p done)) - done))" + else (do { swap a left right; + part1 a left (right - 1) p })) + })" by pat_completeness auto termination @@ -227,14 +227,14 @@ fun partition :: "nat array \ nat \ nat \ nat Heap" where - "partition a left right = (do + "partition a left right = do { pivot \ nth a right; middle \ part1 a left (right - 1) pivot; v \ nth a middle; m \ return (if (v \ pivot) then (middle + 1) else middle); swap a m right; return m - done)" + }" declare partition.simps[simp del] @@ -402,12 +402,12 @@ where "quicksort arr left right = (if (right > left) then - do + do { pivotNewIndex \ partition arr left right; pivotNewIndex \ assert (\x. left \ x \ x \ right) pivotNewIndex; quicksort arr left (pivotNewIndex - 1); quicksort arr (pivotNewIndex + 1) right - done + } else return ())" by pat_completeness auto @@ -645,11 +645,11 @@ subsection {* Example *} -definition "qsort a = do +definition "qsort a = do { k \ len a; quicksort a 0 (k - 1); return a - done" + }" code_reserved SML upto diff -r 0d6b64060543 -r ba0bc31b90d7 src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Tue Jul 13 11:50:22 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Tue Jul 13 12:00:11 2010 +0200 @@ -11,19 +11,19 @@ hide_const (open) swap rev fun swap :: "'a\heap array \ nat \ nat \ unit Heap" where - "swap a i j = (do + "swap a i j = do { x \ nth a i; y \ nth a j; upd i y a; upd j x a; return () - done)" + }" fun rev :: "'a\heap array \ nat \ nat \ unit Heap" where - "rev a i j = (if (i < j) then (do + "rev a i j = (if (i < j) then do { swap a i j; rev a (i + 1) (j - 1) - done) + } else return ())" notation (output) swap ("swap") diff -r 0d6b64060543 -r ba0bc31b90d7 src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Jul 13 11:50:22 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Jul 13 12:00:11 2010 +0200 @@ -31,10 +31,10 @@ primrec make_llist :: "'a\heap list \ 'a node Heap" where [simp del]: "make_llist [] = return Empty" - | "make_llist (x#xs) = do tl \ make_llist xs; - next \ ref tl; - return (Node x next) - done" + | "make_llist (x#xs) = do { tl \ make_llist xs; + next \ ref tl; + return (Node x next) + }" text {* define traverse using the MREC combinator *} @@ -43,18 +43,18 @@ traverse :: "'a\heap node \ 'a list Heap" where [code del]: "traverse = MREC (\n. case n of Empty \ return (Inl []) - | Node x r \ (do tl \ Ref.lookup r; - return (Inr tl) done)) + | Node x r \ do { tl \ Ref.lookup r; + return (Inr tl) }) (\n tl xs. case n of Empty \ undefined | Node x r \ return (x # xs))" lemma traverse_simps[code, simp]: "traverse Empty = return []" - "traverse (Node x r) = do tl \ Ref.lookup r; - xs \ traverse tl; - return (x#xs) - done" + "traverse (Node x r) = do { tl \ Ref.lookup r; + xs \ traverse tl; + return (x#xs) + }" unfolding traverse_def by (auto simp: traverse_def MREC_rule) @@ -529,25 +529,25 @@ subsection {* Definition of in-place reversal *} definition rev' :: "(('a::heap) node ref \ 'a node ref) \ 'a node ref Heap" -where "rev' = MREC (\(q, p). do v \ !p; (case v of Empty \ (return (Inl q)) - | Node x next \ do +where "rev' = MREC (\(q, p). do { v \ !p; (case v of Empty \ (return (Inl q)) + | Node x next \ do { p := Node x q; return (Inr (p, next)) - done) done) + })}) (\x s z. return z)" lemma rev'_simps [code]: "rev' (q, p) = - do + do { v \ !p; (case v of Empty \ return q | Node x next \ - do + do { p := Node x q; rev' (p, next) - done) - done" + }) + }" unfolding rev'_def MREC_rule[of _ _ "(q, p)"] unfolding rev'_def[symmetric] thm arg_cong2 by (auto simp add: expand_fun_eq intro: arg_cong2[where f = "op \="] split: node.split) @@ -555,7 +555,7 @@ primrec rev :: "('a:: heap) node \ 'a node Heap" where "rev Empty = return Empty" -| "rev (Node x n) = (do q \ ref Empty; p \ ref (Node x n); v \ rev' (q, p); !v done)" +| "rev (Node x n) = do { q \ ref Empty; p \ ref (Node x n); v \ rev' (q, p); !v }" subsection {* Correctness Proof *} @@ -680,7 +680,7 @@ definition merge' :: "(('a::{heap, ord}) node ref * ('a::{heap, ord})) * ('a::{heap, ord}) node ref * ('a::{heap, ord}) node ref \ ('a::{heap, ord}) node ref Heap" where -"merge' = MREC (\(_, p, q). (do v \ !p; w \ !q; +"merge' = MREC (\(_, p, q). do { v \ !p; w \ !q; (case v of Empty \ return (Inl q) | Node valp np \ (case w of Empty \ return (Inl p) @@ -688,8 +688,8 @@ if (valp \ valq) then return (Inr ((p, valp), np, q)) else - return (Inr ((q, valq), p, nq)))) done)) - (\ _ ((n, v), _, _) r. do n := Node v r; return n done)" + return (Inr ((q, valq), p, nq)))) }) + (\ _ ((n, v), _, _) r. do { n := Node v r; return n })" definition merge where "merge p q = merge' (undefined, p, q)" @@ -713,21 +713,21 @@ term "Ref.change" lemma merge_simps [code]: shows "merge p q = -do v \ !p; +do { v \ !p; w \ !q; (case v of node.Empty \ return q | Node valp np \ case w of node.Empty \ return p | Node valq nq \ - if valp \ valq then do r \ merge np q; + if valp \ valq then do { r \ merge np q; p := (Node valp r); return p - done - else do r \ merge p nq; + } + else do { r \ merge p nq; q := (Node valq r); return q - done) -done" + }) +}" proof - {fix v x y have case_return: "(case v of Empty \ return x | Node v n \ return (y v n)) = return (case v of Empty \ x | Node v n \ y v n)" by (cases v) auto @@ -997,11 +997,11 @@ text {* A simple example program *} -definition test_1 where "test_1 = (do ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs done)" -definition test_2 where "test_2 = (do ll_xs <- make_llist [1..(15::int)]; ll_ys <- rev ll_xs; ys <- traverse ll_ys; return ys done)" +definition test_1 where "test_1 = (do { ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs })" +definition test_2 where "test_2 = (do { ll_xs <- make_llist [1..(15::int)]; ll_ys <- rev ll_xs; ys <- traverse ll_ys; return ys })" definition test_3 where "test_3 = - (do + (do { ll_xs \ make_llist (filter (%n. n mod 2 = 0) [2..8]); ll_ys \ make_llist (filter (%n. n mod 2 = 1) [5..11]); r \ ref ll_xs; @@ -1010,7 +1010,7 @@ ll_zs \ !p; zs \ traverse ll_zs; return zs - done)" + })" code_reserved SML upto diff -r 0d6b64060543 -r ba0bc31b90d7 src/HOL/Imperative_HOL/ex/SatChecker.thy --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Jul 13 11:50:22 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Jul 13 12:00:11 2010 +0200 @@ -174,15 +174,15 @@ primrec res_mem :: "Lit \ Clause \ Clause Heap" where "res_mem l [] = raise ''MiniSatChecked.res_thm: Cannot find literal''" -| "res_mem l (x#xs) = (if (x = l) then return xs else (do v \ res_mem l xs; return (x # v) done))" +| "res_mem l (x#xs) = (if (x = l) then return xs else do { v \ res_mem l xs; return (x # v) })" fun resolve1 :: "Lit \ Clause \ Clause \ Clause Heap" where "resolve1 l (x#xs) (y#ys) = (if (x = l) then return (merge xs (y#ys)) - else (if (x < y) then (do v \ resolve1 l xs (y#ys); return (x # v) done) - else (if (x > y) then (do v \ resolve1 l (x#xs) ys; return (y # v) done) - else (do v \ resolve1 l xs ys; return (x # v) done))))" + else (if (x < y) then do { v \ resolve1 l xs (y#ys); return (x # v) } + else (if (x > y) then do { v \ resolve1 l (x#xs) ys; return (y # v) } + else do { v \ resolve1 l xs ys; return (x # v) })))" | "resolve1 l [] ys = raise ''MiniSatChecked.res_thm: Cannot find literal''" | "resolve1 l xs [] = res_mem l xs" @@ -190,9 +190,9 @@ where "resolve2 l (x#xs) (y#ys) = (if (y = l) then return (merge (x#xs) ys) - else (if (x < y) then (do v \ resolve2 l xs (y#ys); return (x # v) done) - else (if (x > y) then (do v \ resolve2 l (x#xs) ys; return (y # v) done) - else (do v \ resolve2 l xs ys; return (x # v) done))))" + else (if (x < y) then do { v \ resolve2 l xs (y#ys); return (x # v) } + else (if (x > y) then do { v \ resolve2 l (x#xs) ys; return (y # v) } + else do { v \ resolve2 l xs ys; return (x # v) })))" | "resolve2 l xs [] = raise ''MiniSatChecked.res_thm: Cannot find literal''" | "resolve2 l [] ys = res_mem l ys" @@ -413,10 +413,10 @@ definition get_clause :: "Clause option array \ ClauseId \ Clause Heap" where "get_clause a i = - (do c \ nth a i; + do { c \ nth a i; (case c of None \ raise (''Clause not found'') | Some x \ return x) - done)" + }" primrec res_thm2 :: "Clause option array \ (Lit * ClauseId) \ Clause \ Clause Heap" @@ -424,9 +424,9 @@ "res_thm2 a (l, j) cli = ( if l = 0 then raise(''Illegal literal'') else - (do clj \ get_clause a j; + do { clj \ get_clause a j; res_thm' l cli clj - done))" + })" primrec foldM :: "('a \ 'b \ 'b Heap) \ 'a list \ 'b \ 'b Heap" @@ -437,27 +437,27 @@ fun doProofStep2 :: "Clause option array \ ProofStep \ Clause list \ Clause list Heap" where "doProofStep2 a (Conflict saveTo (i, rs)) rcs = - (do + do { cli \ get_clause a i; result \ foldM (res_thm2 a) rs cli; upd saveTo (Some result) a; return rcs - done)" -| "doProofStep2 a (Delete cid) rcs = (do upd cid None a; return rcs done)" -| "doProofStep2 a (Root cid clause) rcs = (do upd cid (Some (remdups (sort clause))) a; return (clause # rcs) done)" + }" +| "doProofStep2 a (Delete cid) rcs = do { upd cid None a; return rcs }" +| "doProofStep2 a (Root cid clause) rcs = do { upd cid (Some (remdups (sort clause))) a; return (clause # rcs) }" | "doProofStep2 a (Xstep cid1 cid2) rcs = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" | "doProofStep2 a (ProofDone b) rcs = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''" definition checker :: "nat \ ProofStep list \ nat \ Clause list Heap" where "checker n p i = - (do + do { a \ Array.new n None; rcs \ foldM (doProofStep2 a) p []; ec \ Array.nth a i; (if ec = Some [] then return rcs else raise(''No empty clause'')) - done)" + }" lemma crel_option_case: assumes "crel (case x of None \ n | Some y \ s y) h h' r" @@ -651,10 +651,10 @@ "ldoProofStep (Conflict saveTo (i, rs)) (xs, rcl) = (case (xs ! i) of None \ raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'') - | Some cli \ (do + | Some cli \ do { result \ foldM (lres_thm xs) rs cli ; return ((xs[saveTo:=Some result]), rcl) - done))" + })" | "ldoProofStep (Delete cid) (xs, rcl) = return (xs[cid:=None], rcl)" | "ldoProofStep (Root cid clause) (xs, rcl) = return (xs[cid:=Some (sort clause)], (remdups(sort clause)) # rcl)" | "ldoProofStep (Xstep cid1 cid2) (xs, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" @@ -663,11 +663,11 @@ definition lchecker :: "nat \ ProofStep list \ nat \ Clause list Heap" where "lchecker n p i = - (do + do { rcs \ foldM (ldoProofStep) p ([], []); (if (fst rcs ! i) = Some [] then return (snd rcs) else raise(''No empty clause'')) - done)" + }" section {* Functional version with RedBlackTrees *} @@ -684,10 +684,10 @@ "tdoProofStep (Conflict saveTo (i, rs)) (t, rcl) = (case (RBT_Impl.lookup t i) of None \ raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'') - | Some cli \ (do + | Some cli \ do { result \ foldM (tres_thm t) rs cli; return ((RBT_Impl.insert saveTo result t), rcl) - done))" + })" | "tdoProofStep (Delete cid) (t, rcl) = return ((RBT_Impl.delete cid t), rcl)" | "tdoProofStep (Root cid clause) (t, rcl) = return (RBT_Impl.insert cid (sort clause) t, (remdups(sort clause)) # rcl)" | "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" @@ -696,11 +696,11 @@ definition tchecker :: "nat \ ProofStep list \ nat \ Clause list Heap" where "tchecker n p i = - (do + do { rcs \ foldM (tdoProofStep) p (RBT_Impl.Empty, []); (if (RBT_Impl.lookup (fst rcs) i) = Some [] then return (snd rcs) else raise(''No empty clause'')) - done)" + }" section {* Code generation setup *}