--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Fri Sep 05 11:50:35 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-structure Nat =
-struct
-
-datatype nat = Suc of nat | Zero_nat;
-
-val one_nat : nat = Suc Zero_nat;
-
-fun nat_case f1 f2 Zero_nat = f1
- | nat_case f1 f2 (Suc nat) = f2 nat;
-
-fun plus_nat (Suc m) n = plus_nat m (Suc n)
- | plus_nat Zero_nat n = n;
-
-fun times_nat (Suc m) n = plus_nat n (times_nat m n)
- | times_nat Zero_nat n = Zero_nat;
-
-end; (*struct Nat*)
-
-structure Codegen =
-struct
-
-fun fac n =
- (case n of Nat.Zero_nat => Nat.one_nat
- | Nat.Suc m => Nat.times_nat n (fac m));
-
-end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Fri Sep 05 11:50:35 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-structure Nat =
-struct
-
-datatype nat = Suc of nat | Zero_nat;
-
-fun less_nat m (Suc n) = less_eq_nat m n
- | less_nat n Zero_nat = false
-and less_eq_nat (Suc m) n = less_nat m n
- | less_eq_nat Zero_nat n = true;
-
-fun minus_nat (Suc m) (Suc n) = minus_nat m n
- | minus_nat Zero_nat n = Zero_nat
- | minus_nat m Zero_nat = m;
-
-end; (*struct Nat*)
-
-structure Codegen =
-struct
-
-fun pick ((k, v) :: xs) n =
- (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
-
-end; (*struct Codegen*)
--- a/src/HOL/Library/Array.thy Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/Library/Array.thy Sat Sep 06 14:02:36 2008 +0200
@@ -57,7 +57,7 @@
obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')"
by (cases "Heap_Monad.execute (Array.length a) h")
then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h"
- by (auto simp add: upd_def bindM_def run_drop split: sum.split)
+ by (auto simp add: upd_def bindM_def split: sum.split)
qed
--- a/src/HOL/Library/Heap_Monad.thy Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/Library/Heap_Monad.thy Sat Sep 06 14:02:36 2008 +0200
@@ -56,10 +56,6 @@
by (simp add: heap_def)
definition
- run :: "'a Heap \<Rightarrow> 'a Heap" where
- run_drop [code del]: "run f = f"
-
-definition
bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
[code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
(Inl x, h') \<Rightarrow> execute (g x) h'
@@ -129,7 +125,7 @@
"return" ("\<^raw:{\textsf{return}}>")
translations
- "_do f" => "CONST run f"
+ "_do f" => "f"
"_bindM x f g" => "f \<guillemotright>= (\<lambda>x. g)"
"_chainM f g" => "f \<guillemotright> g"
"_let x t f" => "CONST Let t (\<lambda>x. f)"
@@ -140,18 +136,19 @@
fun dest_abs_eta (Abs (abs as (_, ty, _))) =
let
val (v, t) = Syntax.variant_abs abs;
- in ((v, ty), t) end
+ in (Free (v, ty), t) end
| dest_abs_eta t =
let
val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
- in ((v, dummyT), t) end
+ in (Free (v, dummyT), t) end;
fun unfold_monad (Const (@{const_syntax bindM}, _) $ f $ g) =
let
- val ((v, ty), g') = dest_abs_eta g;
+ 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 v = w) | _ => I) g' false;
+ (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
in if v_used then
- Const ("_bindM", dummyT) $ Free (v, ty) $ f $ unfold_monad g'
+ Const ("_bindM", dummyT) $ v $ f $ unfold_monad g'
else
Const ("_chainM", dummyT) $ f $ unfold_monad g'
end
@@ -159,33 +156,28 @@
Const ("_chainM", dummyT) $ f $ unfold_monad g
| unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
let
- val ((v, ty), g') = dest_abs_eta g;
- in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
+ val (v, g') = dest_abs_eta g;
+ in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
| unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
- Const ("return", dummyT) $ f
+ Const (@{const_syntax return}, dummyT) $ f
| unfold_monad f = f;
- fun tr' (f::ts) =
- list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
-in [(@{const_syntax "run"}, tr')] end;
+ fun contains_bindM (Const (@{const_syntax bindM}, _) $ _ $ _) = true
+ | contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
+ contains_bindM t;
+ fun bindM_monad_tr' (f::g::ts) = list_comb
+ (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
+ fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_bindM g' then list_comb
+ (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
+ else raise Match;
+in [
+ (@{const_syntax bindM}, bindM_monad_tr'),
+ (@{const_syntax Let}, Let_monad_tr')
+] end;
*}
subsection {* Monad properties *}
-subsubsection {* Superfluous runs *}
-
-text {* @{term run} is just a doodle *}
-
-lemma run_simp [simp]:
- "\<And>f. run (run f) = run f"
- "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
- "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
- "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
- "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
- "\<And>f. f = run g \<longleftrightarrow> f = g"
- "\<And>f. run f = g \<longleftrightarrow> f = g"
- unfolding run_drop by rule+
-
subsubsection {* Monad laws *}
lemma return_bind: "return x \<guillemotright>= f = f x"
@@ -293,7 +285,6 @@
code_type Heap (SML "unit/ ->/ _")
code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
-code_const run (SML "_")
code_const return (SML "!(fn/ ()/ =>/ _)")
code_const "Heap_Monad.Fail" (SML "Fail")
code_const "Heap_Monad.raise_exc" (SML "!(fn/ ()/ =>/ raise/ _)")
@@ -301,7 +292,6 @@
code_type Heap (OCaml "_")
code_const Heap (OCaml "failwith/ \"bare Heap\"")
code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
-code_const run (OCaml "_")
code_const return (OCaml "!(fun/ ()/ ->/ _)")
code_const "Heap_Monad.Fail" (OCaml "Failure")
code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
@@ -416,7 +406,7 @@
code_type Heap (Haskell "ST/ RealWorld/ _")
code_const Heap (Haskell "error/ \"bare Heap\"")
-code_monad run "op \<guillemotright>=" Haskell
+code_monad "op \<guillemotright>=" Haskell
code_const return (Haskell "return")
code_const "Heap_Monad.Fail" (Haskell "_")
code_const "Heap_Monad.raise_exc" (Haskell "error")
--- a/src/HOL/Library/Relational.thy Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/Library/Relational.thy Sat Sep 06 14:02:36 2008 +0200
@@ -77,7 +77,7 @@
from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y"
and crel_mapM: "crel (mapM f xs) h1 h' ys"
and r_def: "r = y#ys"
- unfolding mapM.simps run_drop
+ unfolding mapM.simps
by (auto elim!: crelE crel_return)
from Cons(1)[OF crel_mapM] crel_mapM crel_f assms(3) r_def
show ?case by auto
@@ -109,14 +109,14 @@
assumes "crel (nth a i) h h' r"
obtains "r = (get_array a h) ! i" "h = h'" "i < Heap.length a h"
using assms
- unfolding nth_def run_drop
+ unfolding nth_def
by (auto elim!: crelE crel_if crel_raise crel_length crel_heap)
lemma crel_upd[consumes 1]:
assumes "crel (upd i v a) h h' r"
obtains "r = a" "h' = Heap.upd a i v h"
using assms
- unfolding upd_def run_drop
+ unfolding upd_def
by (elim crelE crel_if crel_return crel_raise
crel_length crel_heap) auto
@@ -132,14 +132,14 @@
assumes "crel (Array.map_entry i f a) h h' r"
obtains "r = a" "h' = Heap.upd a i (f (get_array a h ! i)) h"
using assms
- unfolding Array.map_entry_def run_drop
+ unfolding Array.map_entry_def
by (elim crelE crel_upd crel_nth) auto
lemma crel_swap:
assumes "crel (Array.swap i x a) h h' r"
obtains "r = get_array a h ! i" "h' = Heap.upd a i x h"
using assms
- unfolding Array.swap_def run_drop
+ unfolding Array.swap_def
by (elim crelE crel_upd crel_nth crel_return) auto
(* Strong version of the lemma for this operation is missing *)
@@ -175,7 +175,7 @@
with Suc(2) obtain r where
crel_mapM: "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' r"
and xs_def: "xs = get_array a h ! (Heap.length a h - Suc n) # r"
- by (auto simp add: run_drop elim!: crelE crel_nth crel_return)
+ by (auto elim!: crelE crel_nth crel_return)
from Suc(3) have "Heap.length a h - n = Suc (Heap.length a h - Suc n)"
by arith
with Suc.hyps[OF crel_mapM] xs_def show ?case
@@ -188,7 +188,7 @@
obtains "h = h'" "xs = get_array a h"
proof
from assms have "crel (mapM (Array.nth a) [0..<Heap.length a h]) h h' xs"
- unfolding freeze_def run_drop
+ unfolding freeze_def
by (auto elim: crelE crel_length)
hence "crel (mapM (Array.nth a) [(Heap.length a h - Heap.length a h)..<Heap.length a h]) h h' xs"
by simp
@@ -211,7 +211,7 @@
by (simp add: upt_conv_Cons')
from Suc(2) this obtain r where
crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
- by (auto simp add: run_drop elim!: crelE crel_map_entry crel_return)
+ by (auto simp add: elim!: crelE crel_map_entry crel_return)
have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
by simp
@@ -236,7 +236,7 @@
by (simp add: upt_conv_Cons')
from Suc(2) this obtain r where
crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
- by (auto simp add: run_drop elim!: crelE crel_map_entry crel_return)
+ by (auto simp add: elim!: crelE crel_map_entry crel_return)
have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
from Suc(3) have less: "Heap.length a h - Suc n < Heap.length a h - n" by arith
from Suc(3) have less2: "Heap.length a h - Suc n < Heap.length a h" by arith
@@ -264,7 +264,7 @@
by (simp add: upt_conv_Cons')
from Suc(2) this obtain r where
crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
- by (auto simp add: run_drop elim!: crelE crel_map_entry crel_return)
+ by (auto elim!: crelE crel_map_entry crel_return)
have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
by simp
@@ -287,10 +287,10 @@
obtains "r = a" "get_array a h' = List.map f (get_array a h)"
proof
from assms crel_mapM_map_entry show "get_array a h' = List.map f (get_array a h)"
- unfolding Array.map_def run_drop
+ unfolding Array.map_def
by (fastsimp elim!: crelE crel_length crel_return)
from assms show "r = a"
- unfolding Array.map_def run_drop
+ unfolding Array.map_def
by (elim crelE crel_return)
qed
@@ -351,7 +351,7 @@
assumes "crel (Ref.change f ref) h h' r"
obtains "h' = set_ref ref (f (get_ref ref h)) h" "r = f (get_ref ref h)"
using assms
-unfolding Ref.change_def run_drop Let_def
+unfolding Ref.change_def Let_def
by (auto elim!: crelE crel_lookup crel_update crel_return)
subsection {* Elimination rules for the assert command *}
@@ -446,14 +446,14 @@
assumes "i < Heap.length a h"
shows "crel (nth a i) h h ((get_array a h) ! i)"
using assms
- unfolding nth_def run_drop
+ unfolding nth_def
by (auto intro!: crelI crel_ifI crel_raiseI crel_lengthI crel_heapI')
lemma crel_updI:
assumes "i < Heap.length a h"
shows "crel (upd i v a) h (Heap.upd a i v h) a"
using assms
- unfolding upd_def run_drop
+ unfolding upd_def
by (auto intro!: crelI crel_ifI crel_returnI crel_raiseI
crel_lengthI crel_heapI')
@@ -481,7 +481,7 @@
lemma crel_changeI:
shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
-unfolding change_def Let_def run_drop by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
+unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
subsection {* Introduction rules for the assert command *}
@@ -562,7 +562,7 @@
next
case (Cons x xs)
thus ?case
- unfolding mapM.simps run_drop
+ unfolding mapM.simps
by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
qed
@@ -585,14 +585,14 @@
assumes "i < Heap.length a h"
shows "noError (Array.upd i v a) h"
using assms
- unfolding upd_def run_drop
+ unfolding upd_def
by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
lemma noError_nth:
assumes "i < Heap.length a h"
shows "noError (Array.nth a i) h"
using assms
- unfolding nth_def run_drop
+ unfolding nth_def
by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
lemma noError_of_list:
@@ -603,14 +603,14 @@
assumes "i < Heap.length a h"
shows "noError (map_entry i f a) h"
using assms
- unfolding map_entry_def run_drop
+ unfolding map_entry_def
by (auto elim: crel_nth intro!: noErrorI noError_nth noError_upd)
lemma noError_swap:
assumes "i < Heap.length a h"
shows "noError (swap i x a) h"
using assms
- unfolding swap_def run_drop
+ unfolding swap_def
by (auto elim: crel_nth intro!: noErrorI noError_return noError_nth noError_upd)
lemma noError_make:
@@ -625,7 +625,7 @@
lemma noError_freeze:
shows "noError (freeze a) h"
-unfolding freeze_def run_drop
+unfolding freeze_def
by (auto intro!: noErrorI noError_length noError_mapM[of _ _ _ "\<lambda>x. get_array a h ! x"]
noError_nth crel_nthI elim: crel_length)
@@ -641,13 +641,13 @@
from Suc.prems have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
by (simp add: upt_conv_Cons')
with Suc.hyps[of "(Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h)"] Suc.prems show ?case
- by (auto simp add: run_drop intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
+ by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
qed
lemma noError_map:
shows "noError (Array.map f a) h"
using noError_mapM_map_entry[of "Heap.length a h" a h]
-unfolding Array.map_def run_drop
+unfolding Array.map_def
by (auto intro: noErrorI noError_length noError_return elim!: crel_length)
subsection {* Introduction rules for the reference commands *}
@@ -666,7 +666,7 @@
lemma noError_change:
shows "noError (Ref.change f ref) h"
- unfolding Ref.change_def run_drop Let_def by (intro noErrorI noError_lookup noError_update noError_return)
+ unfolding Ref.change_def Let_def by (intro noErrorI noError_lookup noError_update noError_return)
subsection {* Introduction rules for the assert command *}
--- a/src/HOL/Library/State_Monad.thy Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/Library/State_Monad.thy Sat Sep 06 14:02:36 2008 +0200
@@ -56,31 +56,23 @@
we use a set of monad combinators:
*}
-notation fcomp (infixl ">>" 60)
-notation (xsymbols) fcomp (infixl "\<guillemotright>" 60)
-notation scomp (infixl ">>=" 60)
-notation (xsymbols) scomp (infixl "\<guillemotright>=" 60)
+notation fcomp (infixl "o>" 60)
+notation (xsymbols) fcomp (infixl "o>" 60)
+notation scomp (infixl "o->" 60)
+notation (xsymbols) scomp (infixl "o\<rightarrow>" 60)
abbreviation (input)
"return \<equiv> Pair"
-definition
- run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
- "run f = f"
-
-print_ast_translation {*
- [(@{const_syntax "run"}, fn (f::ts) => Syntax.mk_appl f ts)]
-*}
-
text {*
Given two transformations @{term f} and @{term g}, they
- may be directly composed using the @{term "op \<guillemotright>"} combinator,
- forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}.
+ may be directly composed using the @{term "op o>"} combinator,
+ forming a forward composition: @{prop "(f o> g) s = f (g s)"}.
After any yielding transformation, we bind the side result
immediately using a lambda abstraction. This
- is the purpose of the @{term "op \<guillemotright>="} combinator:
- @{prop "(f \<guillemotright>= (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
+ is the purpose of the @{term "op o\<rightarrow>"} combinator:
+ @{prop "(f o\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
For queries, the existing @{term "Let"} is appropriate.
@@ -88,8 +80,6 @@
it to the state from the left; we introduce the
suggestive abbreviation @{term return} for this purpose.
- The @{const run} ist just a marker.
-
The most crucial distinction to Haskell is that we do
not need to introduce distinguished type constructors
for different kinds of state. This has two consequences:
@@ -107,22 +97,6 @@
*}
-subsection {* Obsolete runs *}
-
-text {*
- @{term run} is just a doodle and should not occur nested:
-*}
-
-lemma run_simp [simp]:
- "\<And>f. run (run f) = run f"
- "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
- "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
- "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
- "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
- "\<And>f. f = run f \<longleftrightarrow> True"
- "\<And>f. run f = f \<longleftrightarrow> True"
- unfolding run_def by rule+
-
subsection {* Monad laws *}
text {*
@@ -130,66 +104,14 @@
as normalization rules for monadic expressions:
*}
-lemma
- return_scomp [simp]: "return x \<guillemotright>= f = f x"
- unfolding scomp_def by (simp add: expand_fun_eq)
-
-lemma
- scomp_return [simp]: "x \<guillemotright>= return = x"
- unfolding scomp_def by (simp add: expand_fun_eq split_Pair)
-
-lemma
- id_fcomp [simp]: "id \<guillemotright> f = f"
- unfolding fcomp_def by simp
-
-lemma
- fcomp_id [simp]: "f \<guillemotright> id = f"
- unfolding fcomp_def by simp
-
-lemma
- scomp_scomp [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
- unfolding scomp_def by (simp add: split_def expand_fun_eq)
-
-lemma
- scomp_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
- unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)
-
-lemma
- fcomp_scomp [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
- unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)
-
-lemma
- fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
- unfolding fcomp_def o_assoc ..
-
-lemmas monad_simp = run_simp return_scomp scomp_return id_fcomp fcomp_id
- scomp_scomp scomp_fcomp fcomp_scomp fcomp_fcomp
+lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
+ scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc
text {*
Evaluation of monadic expressions by force:
*}
-lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
- scomp_def fcomp_def run_def
-
-subsection {* ML abstract operations *}
-
-ML {*
-structure StateMonad =
-struct
-
-fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
-fun liftT' sT = sT --> sT;
-
-fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
-
-fun scomp T1 T2 sT f g = Const (@{const_name scomp},
- liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
-
-fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT)) $ f;
-
-end;
-*}
+lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
subsection {* Syntax *}
@@ -211,7 +133,7 @@
("_;// _" [13, 12] 12)
"_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
("let _ = _;// _" [1000, 13, 12] 12)
- "_nil" :: "'a \<Rightarrow> do_expr"
+ "_done" :: "'a \<Rightarrow> do_expr"
("_" [12] 12)
syntax (xsymbols)
@@ -219,95 +141,55 @@
("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
translations
- "_do f" => "CONST run f"
- "_scomp x f g" => "f \<guillemotright>= (\<lambda>x. g)"
- "_fcomp f g" => "f \<guillemotright> g"
+ "_do f" => "f"
+ "_scomp x f g" => "f o\<rightarrow> (\<lambda>x. g)"
+ "_fcomp f g" => "f o> g"
"_let x t f" => "CONST Let t (\<lambda>x. f)"
- "_nil f" => "f"
+ "_done f" => "f"
print_translation {*
let
fun dest_abs_eta (Abs (abs as (_, ty, _))) =
let
val (v, t) = Syntax.variant_abs abs;
- in ((v, ty), t) end
+ in (Free (v, ty), t) end
| dest_abs_eta t =
let
val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
- in ((v, dummyT), t) end
+ in (Free (v, dummyT), t) end;
fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
let
- val ((v, ty), g') = dest_abs_eta g;
- in Const ("_scomp", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
+ val (v, g') = dest_abs_eta g;
+ in Const ("_scomp", dummyT) $ v $ f $ unfold_monad g' end
| unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
Const ("_fcomp", dummyT) $ f $ unfold_monad g
| unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
let
- val ((v, ty), g') = dest_abs_eta g;
- in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
+ val (v, g') = dest_abs_eta g;
+ in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
| unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
Const ("return", dummyT) $ f
| unfold_monad f = f;
- fun tr' (f::ts) =
- list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
-in [(@{const_syntax "run"}, tr')] end;
+ 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 ("_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 ("_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 ("_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;
*}
-
-subsection {* Combinators *}
-
-definition
- lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where
- "lift f x = return (f x)"
-
-primrec
- list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
- "list f [] = id"
-| "list f (x#xs) = (do f x; list f xs done)"
-
-primrec
- list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
- "list_yield f [] = return []"
-| "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
-
-definition
- collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
- "collapse f = (do g \<leftarrow> f; g done)"
-
-text {* combinator properties *}
-
-lemma list_append [simp]:
- "list f (xs @ ys) = list f xs \<guillemotright> list f ys"
- by (induct xs) (simp_all del: id_apply)
-
-lemma list_cong [fundef_cong, recdef_cong]:
- "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
- \<Longrightarrow> list f xs = list g ys"
-proof (induct xs arbitrary: ys)
- case Nil then show ?case by simp
-next
- case (Cons x xs)
- from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
- then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
- with Cons have "list f xs = list g xs" by auto
- with Cons have "list f (x # xs) = list g (x # xs)" by auto
- with Cons show "list f (x # xs) = list g ys" by auto
-qed
-
-lemma list_yield_cong [fundef_cong, recdef_cong]:
- "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
- \<Longrightarrow> list_yield f xs = list_yield g ys"
-proof (induct xs arbitrary: ys)
- case Nil then show ?case by simp
-next
- case (Cons x xs)
- from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
- then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
- with Cons have "list_yield f xs = list_yield g xs" by auto
- with Cons have "list_yield f (x # xs) = list_yield g (x # xs)" by auto
- with Cons show "list_yield f (x # xs) = list_yield g ys" by auto
-qed
-
text {*
For an example, see HOL/ex/Random.thy.
*}
--- a/src/HOL/ex/ImperativeQuicksort.thy Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/ex/ImperativeQuicksort.thy Sat Sep 06 14:02:36 2008 +0200
@@ -4,7 +4,6 @@
text {* We prove QuickSort correct in the Relational Calculus. *}
-
definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
where
"swap arr i j = (
@@ -21,7 +20,7 @@
shows "multiset_of (get_array a h')
= multiset_of (get_array a h)"
using assms
- unfolding swap_def run_drop
+ unfolding swap_def
by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
@@ -49,7 +48,7 @@
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
case (1 a l r p h h' rs)
thus ?case
- unfolding part1.simps [of a l r p] run_drop
+ unfolding part1.simps [of a l r p]
by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes)
qed
@@ -65,7 +64,7 @@
proof (cases "r \<le> l")
case True (* Terminating case *)
with cr `l \<le> r` show ?thesis
- unfolding part1.simps[of a l r p] run_drop
+ unfolding part1.simps[of a l r p]
by (elim crelE crel_if crel_return crel_nth) auto
next
case False (* recursive case *)
@@ -76,7 +75,7 @@
case True
with cr False
have rec1: "crel (part1 a (l + 1) r p) h h' rs"
- unfolding part1.simps[of a l r p] run_drop
+ unfolding part1.simps[of a l r p]
by (elim crelE crel_nth crel_if crel_return) auto
from rec_condition have "l + 1 \<le> r" by arith
from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
@@ -86,7 +85,7 @@
with rec_condition cr
obtain h1 where swp: "crel (swap a l r) h h1 ()"
and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
- unfolding part1.simps[of a l r p] run_drop
+ unfolding part1.simps[of a l r p]
by (elim crelE crel_nth crel_if crel_return) auto
from rec_condition have "l \<le> r - 1" by arith
from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
@@ -106,12 +105,12 @@
proof (cases "r \<le> l")
case True (* Terminating case *)
with cr show ?thesis
- unfolding part1.simps[of a l r p] run_drop
+ unfolding part1.simps[of a l r p]
by (elim crelE crel_if crel_return crel_nth) auto
next
case False (* recursive case *)
with cr 1 show ?thesis
- unfolding part1.simps [of a l r p] swap_def run_drop
+ unfolding part1.simps [of a l r p] swap_def
by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp
qed
qed
@@ -128,7 +127,7 @@
proof (cases "r \<le> l")
case True (* Terminating case *)
with cr show ?thesis
- unfolding part1.simps[of a l r p] run_drop
+ unfolding part1.simps[of a l r p]
by (elim crelE crel_if crel_return crel_nth) auto
next
case False (* recursive case *)
@@ -139,7 +138,7 @@
case True
with cr False
have rec1: "crel (part1 a (l + 1) r p) h h' rs"
- unfolding part1.simps[of a l r p] run_drop
+ unfolding part1.simps[of a l r p]
by (elim crelE crel_nth crel_if crel_return) auto
from 1(1)[OF rec_condition True rec1]
show ?thesis by fastsimp
@@ -148,11 +147,11 @@
with rec_condition cr
obtain h1 where swp: "crel (swap a l r) h h1 ()"
and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
- unfolding part1.simps[of a l r p] run_drop
+ unfolding part1.simps[of a l r p]
by (elim crelE crel_nth crel_if crel_return) auto
from swp rec_condition have
"\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
- unfolding swap_def run_drop
+ unfolding swap_def
by (elim crelE crel_nth crel_upd crel_return) auto
with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
qed
@@ -173,7 +172,7 @@
proof (cases "r \<le> l")
case True (* Terminating case *)
with cr have "rs = r"
- unfolding part1.simps[of a l r p] run_drop
+ unfolding part1.simps[of a l r p]
by (elim crelE crel_if crel_return crel_nth) auto
with True
show ?thesis by auto
@@ -186,7 +185,7 @@
case True
with lr cr
have rec1: "crel (part1 a (l + 1) r p) h h' rs"
- unfolding part1.simps[of a l r p] run_drop
+ unfolding part1.simps[of a l r p]
by (elim crelE crel_nth crel_if crel_return) auto
from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
by fastsimp
@@ -198,10 +197,10 @@
with lr cr
obtain h1 where swp: "crel (swap a l r) h h1 ()"
and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
- unfolding part1.simps[of a l r p] run_drop
+ unfolding part1.simps[of a l r p]
by (elim crelE crel_nth crel_if crel_return) auto
from swp False have "get_array a h1 ! r \<ge> p"
- unfolding swap_def run_drop
+ unfolding swap_def
by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
by fastsimp
@@ -232,7 +231,7 @@
= multiset_of (get_array a h)"
proof -
from assms part_permutes swap_permutes show ?thesis
- unfolding partition.simps run_drop
+ unfolding partition.simps
by (elim crelE crel_return crel_nth crel_if crel_upd) auto
qed
@@ -241,7 +240,7 @@
shows "Heap.length a h = Heap.length a h'"
proof -
from assms part_length_remains show ?thesis
- unfolding partition.simps run_drop swap_def
+ unfolding partition.simps swap_def
by (elim crelE crel_return crel_nth crel_if crel_upd) auto
qed
@@ -251,7 +250,7 @@
shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
proof -
from assms part_outer_remains part_returns_index_in_bounds show ?thesis
- unfolding partition.simps swap_def run_drop
+ unfolding partition.simps swap_def
by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp
qed
@@ -263,7 +262,7 @@
from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
else middle)"
- unfolding partition.simps run_drop
+ unfolding partition.simps
by (elim crelE crel_return crel_nth crel_if crel_upd) simp
from `l < r` have "l \<le> r - 1" by arith
from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
@@ -280,17 +279,17 @@
and swap: "crel (swap a rs r) h1 h' ()"
and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
else middle)"
- unfolding partition.simps run_drop
+ unfolding partition.simps
by (elim crelE crel_return crel_nth crel_if crel_upd) simp
from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
(Heap.upd a rs (get_array a h1 ! r) h1)"
- unfolding swap_def run_drop
+ unfolding swap_def
by (elim crelE crel_return crel_nth crel_upd) simp
from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
- unfolding swap_def run_drop
+ unfolding swap_def
by (elim crelE crel_return crel_nth crel_upd) simp
from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
- unfolding swap_def run_drop by (elim crelE crel_return crel_nth crel_upd) auto
+ unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
from `l < r` have "l \<le> r - 1" by simp
note middle_in_bounds = part_returns_index_in_bounds[OF part this]
from part_outer_remains[OF part] `l < r`
@@ -298,7 +297,7 @@
by fastsimp
with swap
have right_remains: "get_array a h ! r = get_array a h' ! rs"
- unfolding swap_def run_drop
+ unfolding swap_def
by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
from part_partitions [OF part]
show ?thesis
@@ -414,7 +413,7 @@
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
case (1 a l r h h' rs)
with partition_permutes show ?case
- unfolding quicksort.simps [of a l r] run_drop
+ unfolding quicksort.simps [of a l r]
by (elim crel_if crelE crel_assert crel_return) auto
qed
@@ -425,7 +424,7 @@
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
case (1 a l r h h' rs)
with partition_length_remains show ?case
- unfolding quicksort.simps [of a l r] run_drop
+ unfolding quicksort.simps [of a l r]
by (elim crel_if crelE crel_assert crel_return) auto
qed
@@ -463,7 +462,7 @@
ultimately have "get_array a h ! i= get_array a h' ! i" by simp
}
with cr show ?thesis
- unfolding quicksort.simps [of a l r] run_drop
+ unfolding quicksort.simps [of a l r]
by (elim crel_if crelE crel_assert crel_return) auto
qed
qed
@@ -472,7 +471,7 @@
assumes "crel (quicksort a l r) h h' rs"
shows "r \<le> l \<longrightarrow> h = h'"
using assms
- unfolding quicksort.simps [of a l r] run_drop
+ unfolding quicksort.simps [of a l r]
by (elim crel_if crel_return) auto
lemma quicksort_sorts:
@@ -544,7 +543,7 @@
by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
}
with True cr show ?thesis
- unfolding quicksort.simps [of a l r] run_drop
+ unfolding quicksort.simps [of a l r]
by (elim crel_if crel_return crelE crel_assert) auto
qed
qed
@@ -577,7 +576,7 @@
proof (induct a l r p arbitrary: h rule: part1.induct)
case (1 a l r p)
thus ?case
- unfolding part1.simps [of a l r] swap_def run_drop
+ unfolding part1.simps [of a l r] swap_def
by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
qed
@@ -585,7 +584,7 @@
assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
shows "noError (partition a l r) h"
using assms
-unfolding partition.simps swap_def run_drop
+unfolding partition.simps swap_def
apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
apply (frule part_length_remains)
apply (frule part_returns_index_in_bounds)
@@ -604,7 +603,7 @@
proof (induct a l r arbitrary: h rule: quicksort.induct)
case (1 a l ri h)
thus ?case
- unfolding quicksort.simps [of a l ri] run_drop
+ unfolding quicksort.simps [of a l ri]
apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
apply (frule partition_returns_index_in_bounds)
apply auto
@@ -614,7 +613,7 @@
apply (subgoal_tac "Suc r \<le> ri \<or> r = ri")
apply (erule disjE)
apply auto
- unfolding quicksort.simps [of a "Suc ri" ri] run_drop
+ unfolding quicksort.simps [of a "Suc ri" ri]
apply (auto intro!: noError_if noError_return)
done
qed
--- a/src/HOL/ex/Quickcheck.thy Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy Sat Sep 06 14:02:36 2008 +0200
@@ -27,6 +27,25 @@
text {* Datatypes *}
+definition
+ collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+ "collapse f = (do g \<leftarrow> f; g done)"
+
+ML {*
+structure StateMonad =
+struct
+
+fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
+fun liftT' sT = sT --> sT;
+
+fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
+
+fun scomp T1 T2 sT f g = Const (@{const_name scomp},
+ liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
+
+end;
+*}
+
lemma random'_if:
fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
assumes "random' 0 j = undefined"
@@ -62,7 +81,7 @@
mk_scomp_split thy ty this_ty random)
args return;
val is_rec = exists (snd o fst) args;
- in (is_rec, StateMonad.run (term_ty this_ty) @{typ seed} t) end;
+ in (is_rec, t) end;
fun mk_conss thy ty [] = NONE
| mk_conss thy ty [(_, t)] = SOME t
| mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $
--- a/src/HOL/ex/Random.thy Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/ex/Random.thy Sat Sep 06 14:02:36 2008 +0200
@@ -55,18 +55,6 @@
"(if b then f x else f y) = f (if b then x else y)"
by (cases b) simp_all
-(*lemma seed_invariant:
- assumes "seed_invariant (index_of_nat v, index_of_nat w)"
- and "(index_of_nat z, (index_of_nat v', index_of_nat w')) = next (index_of_nat v, index_of_nat w)"
- shows "seed_invariant (index_of_nat v', index_of_nat w')"
-using assms
-apply (auto simp add: seed_invariant_def)
-apply (auto simp add: minus_shift_def Let_def)
-apply (simp_all add: if_same cong del: if_cong)
-apply safe
-unfolding not_less
-oops*)
-
definition
split_seed :: "seed \<Rightarrow> seed \<times> seed"
where
@@ -109,7 +97,7 @@
"range_aux (log 2147483561 k) 1 s = (v, w)"
by (cases "range_aux (log 2147483561 k) 1 s")
with assms show ?thesis
- by (simp add: range_def run_def scomp_def split_def del: range_aux.simps log.simps)
+ by (simp add: monad_collapse range_def del: range_aux.simps log.simps)
qed
definition
@@ -130,7 +118,7 @@
then have
"nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
then show ?thesis
- by (auto simp add: select_def run_def scomp_def split_def)
+ by (auto simp add: monad_collapse select_def)
qed
definition
@@ -143,7 +131,7 @@
lemma select_default_zero:
"fst (select_default 0 x y s) = y"
- by (simp add: run_def scomp_def split_def select_default_def)
+ by (simp add: monad_collapse select_default_def)
lemma select_default_code [code]:
"select_default k x y = (if k = 0 then do
@@ -157,7 +145,7 @@
case False then show ?thesis by (simp add: select_default_def)
next
case True then show ?thesis
- by (simp add: run_def scomp_def split_def select_default_def expand_fun_eq range_def)
+ by (simp add: monad_collapse select_default_def range_def)
qed
@@ -192,3 +180,4 @@
*}
end
+
--- a/src/Tools/code/code_haskell.ML Fri Sep 05 11:50:35 2008 +0200
+++ b/src/Tools/code/code_haskell.ML Sat Sep 06 14:02:36 2008 +0200
@@ -425,50 +425,45 @@
(** optional monad syntax **)
-fun implode_monad c_bind t =
- let
- fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
- if c = c_bind
- then case Code_Thingol.split_abs t2
- of SOME (((v, pat), ty), t') =>
- SOME ((SOME (((SOME v, pat), ty), true), t1), t')
- | NONE => NONE
- else NONE
- | dest_monad t = case Code_Thingol.split_let t
- of SOME (((pat, ty), tbind), t') =>
- SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
- | NONE => NONE;
- in Code_Thingol.unfoldr dest_monad t end;
-
fun pretty_haskell_monad c_bind =
let
- fun pretty pr thm pat vars fxy [(t, _)] =
- let
- val pr_bind = pr_haskell_bind (K (K pr)) thm;
- fun pr_monad (NONE, t) vars =
- (semicolon [pr vars NOBR t], vars)
- | pr_monad (SOME (bind, true), t) vars = vars
- |> pr_bind NOBR bind
- |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
- | pr_monad (SOME (bind, false), t) vars = vars
- |> pr_bind NOBR bind
- |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
- val (binds, t) = implode_monad c_bind t;
- val (ps, vars') = fold_map pr_monad binds vars;
- in (brackify fxy o single o Pretty.enclose "do {" "}") (ps @| pr vars' NOBR t) end;
- in (1, pretty) end;
+ fun dest_bind t1 t2 = case Code_Thingol.split_abs t2
+ of SOME (((v, pat), ty), t') =>
+ SOME ((SOME (((SOME v, pat), ty), true), t1), t')
+ | NONE => NONE;
+ fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
+ if c = c_bind then dest_bind t1 t2
+ else NONE
+ | dest_monad t = case Code_Thingol.split_let t
+ of SOME (((pat, ty), tbind), t') =>
+ SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
+ | NONE => NONE;
+ val implode_monad = Code_Thingol.unfoldr dest_monad;
+ fun pr_monad pr_bind pr (NONE, t) vars =
+ (semicolon [pr vars NOBR t], vars)
+ | pr_monad pr_bind pr (SOME (bind, true), t) vars = vars
+ |> pr_bind NOBR bind
+ |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
+ | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
+ |> pr_bind NOBR bind
+ |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
+ fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
+ of SOME (bind, t') => let
+ val (binds, t'') = implode_monad t'
+ val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K (K pr)) thm) pr) (bind :: binds) vars;
+ in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
+ | NONE => brackify_infix (1, L) fxy
+ [pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]
+ in (2, pretty) end;
-fun add_monad target' raw_c_run raw_c_bind thy =
+fun add_monad target' raw_c_bind thy =
let
- val c_run = Code_Unit.read_const thy raw_c_run;
val c_bind = Code_Unit.read_const thy raw_c_bind;
val c_bind' = Code_Name.const thy c_bind;
in if target = target' then
thy
- |> Code_Target.add_syntax_const target c_run
+ |> Code_Target.add_syntax_const target c_bind
(SOME (pretty_haskell_monad c_bind'))
- |> Code_Target.add_syntax_const target c_bind
- (Code_Printer.simple_const_syntax (SOME (Code_Printer.parse_infix fst (L, 1) ">>=")))
else error "Only Haskell target allows for monad syntax" end;
@@ -482,9 +477,8 @@
val _ =
OuterSyntax.command "code_monad" "define code syntax for monads" OuterKeyword.thy_decl (
- OuterParse.term_group -- OuterParse.term_group -- OuterParse.name
- >> (fn ((raw_run, raw_bind), target) => Toplevel.theory
- (add_monad target raw_run raw_bind))
+ OuterParse.term_group -- OuterParse.name >> (fn (raw_bind, target) =>
+ Toplevel.theory (add_monad target raw_bind))
);
val setup =