--- a/src/HOL/Library/Extended_Nat.thy Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Thu Dec 08 09:10:54 2011 +0100
@@ -489,6 +489,78 @@
qed
+subsection {* Cancellation simprocs *}
+
+lemma enat_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b = c"
+ unfolding plus_enat_def by (simp split: enat.split)
+
+lemma enat_add_left_cancel_le: "a + b \<le> a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b \<le> c"
+ unfolding plus_enat_def by (simp split: enat.split)
+
+lemma enat_add_left_cancel_less: "a + b < a + c \<longleftrightarrow> a \<noteq> (\<infinity>::enat) \<and> b < c"
+ unfolding plus_enat_def by (simp split: enat.split)
+
+ML {*
+structure Cancel_Enat_Common =
+struct
+ (* copied from src/HOL/Tools/nat_numeral_simprocs.ML *)
+ fun find_first_t _ _ [] = raise TERM("find_first_t", [])
+ | find_first_t past u (t::terms) =
+ if u aconv t then (rev past @ terms)
+ else find_first_t (t::past) u terms
+
+ val mk_sum = Arith_Data.long_mk_sum
+ val dest_sum = Arith_Data.dest_sum
+ val find_first = find_first_t []
+ val trans_tac = Numeral_Simprocs.trans_tac
+ val norm_ss = HOL_basic_ss addsimps
+ @{thms add_ac semiring_numeral_0_eq_0 add_0_left add_0_right}
+ fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
+ fun simplify_meta_eq ss cancel_th th =
+ Arith_Data.simplify_meta_eq @{thms semiring_numeral_0_eq_0} ss
+ ([th, cancel_th] MRS trans)
+ fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
+end
+
+structure Eq_Enat_Cancel = ExtractCommonTermFun
+(open Cancel_Enat_Common
+ val mk_bal = HOLogic.mk_eq
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} @{typ enat}
+ fun simp_conv _ _ = SOME @{thm enat_add_left_cancel}
+)
+
+structure Le_Enat_Cancel = ExtractCommonTermFun
+(open Cancel_Enat_Common
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} @{typ enat}
+ fun simp_conv _ _ = SOME @{thm enat_add_left_cancel_le}
+)
+
+structure Less_Enat_Cancel = ExtractCommonTermFun
+(open Cancel_Enat_Common
+ val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} @{typ enat}
+ fun simp_conv _ _ = SOME @{thm enat_add_left_cancel_less}
+)
+*}
+
+simproc_setup enat_eq_cancel
+ ("(l::enat) + m = n" | "(l::enat) = m + n") =
+ {* fn phi => fn ss => fn ct => Eq_Enat_Cancel.proc ss (term_of ct) *}
+
+simproc_setup enat_le_cancel
+ ("(l::enat) + m \<le> n" | "(l::enat) \<le> m + n") =
+ {* fn phi => fn ss => fn ct => Le_Enat_Cancel.proc ss (term_of ct) *}
+
+simproc_setup enat_less_cancel
+ ("(l::enat) + m < n" | "(l::enat) < m + n") =
+ {* fn phi => fn ss => fn ct => Less_Enat_Cancel.proc ss (term_of ct) *}
+
+text {* TODO: add regression tests for these simprocs *}
+
+text {* TODO: add simprocs for combining and cancelling numerals *}
+
+
subsection {* Well-ordering *}
lemma less_enatE:
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Dec 08 09:10:54 2011 +0100
@@ -303,20 +303,28 @@
cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
"cball x e = {y. dist x y \<le> e}"
-lemma mem_ball[simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" by (simp add: ball_def)
-lemma mem_cball[simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" by (simp add: cball_def)
-
-lemma mem_ball_0 [simp]:
+lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
+ by (simp add: ball_def)
+
+lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e"
+ by (simp add: cball_def)
+
+lemma mem_ball_0:
fixes x :: "'a::real_normed_vector"
shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e"
by (simp add: dist_norm)
-lemma mem_cball_0 [simp]:
+lemma mem_cball_0:
fixes x :: "'a::real_normed_vector"
shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
by (simp add: dist_norm)
-lemma centre_in_cball[simp]: "x \<in> cball x e \<longleftrightarrow> 0\<le> e" by simp
+lemma centre_in_ball: "x \<in> ball x e \<longleftrightarrow> 0 < e"
+ by simp
+
+lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
+ by simp
+
lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq)
lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq)
lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" by (simp add: subset_eq)
@@ -344,7 +352,6 @@
apply (erule_tac x="xa" in allE)
by arith
-lemma centre_in_ball[simp]: "x \<in> ball x e \<longleftrightarrow> e > 0" by (metis mem_ball dist_self)
lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..
--- a/src/HOL/Probability/Binary_Product_Measure.thy Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Thu Dec 08 09:10:54 2011 +0100
@@ -315,12 +315,9 @@
subsection {* Binary products of $\sigma$-finite measure spaces *}
-locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2
+locale pair_sigma_finite = pair_sigma_algebra M1 M2 + M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2
for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme"
-sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2
- by default
-
lemma (in pair_sigma_finite) measure_cut_measurable_fst:
assumes "Q \<in> sets P" shows "(\<lambda>x. measure M2 (Pair x -` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _")
proof -
@@ -919,10 +916,7 @@
show "a \<in> A" and "b \<in> B" by auto
qed
-locale pair_finite_sigma_algebra = M1: finite_sigma_algebra M1 + M2: finite_sigma_algebra M2
- for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme"
-
-sublocale pair_finite_sigma_algebra \<subseteq> pair_sigma_algebra by default
+locale pair_finite_sigma_algebra = pair_sigma_algebra M1 M2 + M1: finite_sigma_algebra M1 + M2: finite_sigma_algebra M2 for M1 M2
lemma (in pair_finite_sigma_algebra) finite_pair_sigma_algebra:
shows "P = \<lparr> space = space M1 \<times> space M2, sets = Pow (space M1 \<times> space M2), \<dots> = algebra.more P \<rparr>"
@@ -933,20 +927,16 @@
qed
sublocale pair_finite_sigma_algebra \<subseteq> finite_sigma_algebra P
- apply default
- using M1.finite_space M2.finite_space
- apply (subst finite_pair_sigma_algebra) apply simp
- apply (subst (1 2) finite_pair_sigma_algebra) apply simp
- done
+proof
+ show "finite (space P)"
+ using M1.finite_space M2.finite_space
+ by (subst finite_pair_sigma_algebra) simp
+ show "sets P = Pow (space P)"
+ by (subst (1 2) finite_pair_sigma_algebra) simp
+qed
-locale pair_finite_space = M1: finite_measure_space M1 + M2: finite_measure_space M2
- for M1 M2
-
-sublocale pair_finite_space \<subseteq> pair_finite_sigma_algebra
- by default
-
-sublocale pair_finite_space \<subseteq> pair_sigma_finite
- by default
+locale pair_finite_space = pair_sigma_finite M1 M2 + pair_finite_sigma_algebra M1 M2 +
+ M1: finite_measure_space M1 + M2: finite_measure_space M2 for M1 M2
lemma (in pair_finite_space) pair_measure_Pair[simp]:
assumes "a \<in> space M1" "b \<in> space M2"
@@ -964,6 +954,10 @@
using pair_measure_Pair assms by (cases x) auto
sublocale pair_finite_space \<subseteq> finite_measure_space P
- by default (auto simp: space_pair_measure)
+proof unfold_locales
+ show "measure P (space P) \<noteq> \<infinity>"
+ by (subst (2) finite_pair_sigma_algebra)
+ (simp add: pair_measure_times)
+qed
end
\ No newline at end of file
--- a/src/HOL/Probability/Finite_Product_Measure.thy Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Thu Dec 08 09:10:54 2011 +0100
@@ -240,7 +240,7 @@
locale finite_product_sigma_algebra = product_sigma_algebra M
for M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme" +
fixes I :: "'i set"
- assumes finite_index: "finite I"
+ assumes finite_index[simp, intro]: "finite I"
definition
"product_algebra_generator I M = \<lparr> space = (\<Pi>\<^isub>E i \<in> I. space (M i)),
@@ -508,22 +508,15 @@
finally show "(\<lambda>x. \<lambda>i\<in>I. X i x) -` E \<inter> space M \<in> sets M" .
qed
-locale product_sigma_finite =
- fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme"
+locale product_sigma_finite = product_sigma_algebra M
+ for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" +
assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
-locale finite_product_sigma_finite = product_sigma_finite M
- for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" +
- fixes I :: "'i set" assumes finite_index'[intro]: "finite I"
-
sublocale product_sigma_finite \<subseteq> M: sigma_finite_measure "M i" for i
by (rule sigma_finite_measures)
-sublocale product_sigma_finite \<subseteq> product_sigma_algebra
- by default
-
-sublocale finite_product_sigma_finite \<subseteq> finite_product_sigma_algebra
- by default (fact finite_index')
+locale finite_product_sigma_finite = finite_product_sigma_algebra M I + product_sigma_finite M
+ for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" and I :: "'i set"
lemma (in finite_product_sigma_finite) product_algebra_generator_measure:
assumes "Pi\<^isub>E I F \<in> sets G"
--- a/src/HOL/Probability/Independent_Family.thy Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Probability/Independent_Family.thy Thu Dec 08 09:10:54 2011 +0100
@@ -845,8 +845,8 @@
moreover
have "D.prob A = P.prob A"
proof (rule prob_space_unique_Int_stable)
- show "prob_space ?D'" by default
- show "prob_space (Pi\<^isub>M I ?M)" by default
+ show "prob_space ?D'" by unfold_locales
+ show "prob_space (Pi\<^isub>M I ?M)" by unfold_locales
show "Int_stable P.G" using M'.Int
by (intro Int_stable_product_algebra_generator) (simp add: Int_stable_def)
show "space P.G \<in> sets P.G"
@@ -963,13 +963,13 @@
unfolding space_pair_measure[simplified pair_measure_def space_sigma]
using X.top Y.top by (auto intro!: pair_measure_generatorI)
- show "prob_space ?J" by default
+ show "prob_space ?J" by unfold_locales
show "space ?J = space ?P"
by (simp add: pair_measure_generator_def space_pair_measure)
show "sets ?J = sets (sigma ?P)"
by (simp add: pair_measure_def)
- show "prob_space XY.P" by default
+ show "prob_space XY.P" by unfold_locales
show "space XY.P = space ?P" "sets XY.P = sets (sigma ?P)"
by (simp_all add: pair_measure_generator_def pair_measure_def)
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Thu Dec 08 09:10:54 2011 +0100
@@ -41,36 +41,11 @@
qed
qed
-locale product_prob_space =
- fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" and I :: "'i set"
- assumes prob_spaces: "\<And>i. prob_space (M i)"
- and I_not_empty: "I \<noteq> {}"
-
-locale finite_product_prob_space = product_prob_space M I
- for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" and I :: "'i set" +
- assumes finite_index'[intro]: "finite I"
-
-sublocale product_prob_space \<subseteq> M: prob_space "M i" for i
- by (rule prob_spaces)
-
-sublocale product_prob_space \<subseteq> product_sigma_finite
- by default
-
-sublocale finite_product_prob_space \<subseteq> finite_product_sigma_finite
- by default (fact finite_index')
-
-sublocale finite_product_prob_space \<subseteq> prob_space "Pi\<^isub>M I M"
-proof
- show "measure P (space P) = 1"
- by (simp add: measure_times measure_space_1 setprod_1)
-qed
-
lemma (in product_prob_space) measure_preserving_restrict:
assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
shows "(\<lambda>f. restrict f J) \<in> measure_preserving (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i)" (is "?R \<in> _")
proof -
- interpret K: finite_product_prob_space M K
- by default (insert assms, auto)
+ interpret K: finite_product_prob_space M K by default fact
have J: "J \<noteq> {}" "finite J" using assms by (auto simp add: finite_subset)
interpret J: finite_product_prob_space M J
by default (insert J, auto)
@@ -297,7 +272,7 @@
definition (in product_prob_space) infprod_algebra :: "('i \<Rightarrow> 'a) measure_space" where
"infprod_algebra = sigma generator \<lparr> measure :=
(SOME \<mu>. (\<forall>s\<in>sets generator. \<mu> s = \<mu>G s) \<and>
- measure_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>)\<rparr>"
+ prob_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>)\<rparr>"
syntax
"_PiP" :: "[pttrn, 'i set, ('b, 'd) measure_space_scheme] => ('i => 'b, 'd) measure_space_scheme" ("(3PIP _:_./ _)" 10)
@@ -314,13 +289,13 @@
translations
"PIP x:I. M" == "CONST Pi\<^isub>P I (%x. M)"
-sublocale product_prob_space \<subseteq> G!: algebra generator
+lemma (in product_prob_space) algebra_generator:
+ assumes "I \<noteq> {}" shows "algebra generator"
proof
let ?G = generator
show "sets ?G \<subseteq> Pow (space ?G)"
by (auto simp: generator_def emb_def)
- from I_not_empty
- obtain i where "i \<in> I" by auto
+ from `I \<noteq> {}` obtain i where "i \<in> I" by auto
then show "{} \<in> sets ?G"
by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"]
simp: product_algebra_def sigma_def sigma_sets.Empty generator_def emb_def)
@@ -343,42 +318,54 @@
using XA XB by (auto intro!: generatorI')
qed
-lemma (in product_prob_space) positive_\<mu>G: "positive generator \<mu>G"
-proof (intro positive_def[THEN iffD2] conjI ballI)
- from generatorE[OF G.empty_sets] guess J X . note this[simp]
- interpret J: finite_product_sigma_finite M J by default fact
- have "X = {}"
- by (rule emb_injective[of J I]) simp_all
- then show "\<mu>G {} = 0" by simp
-next
- fix A assume "A \<in> sets generator"
- from generatorE[OF this] guess J X . note this[simp]
- interpret J: finite_product_sigma_finite M J by default fact
- show "0 \<le> \<mu>G A" by simp
+lemma (in product_prob_space) positive_\<mu>G:
+ assumes "I \<noteq> {}"
+ shows "positive generator \<mu>G"
+proof -
+ interpret G!: algebra generator by (rule algebra_generator) fact
+ show ?thesis
+ proof (intro positive_def[THEN iffD2] conjI ballI)
+ from generatorE[OF G.empty_sets] guess J X . note this[simp]
+ interpret J: finite_product_sigma_finite M J by default fact
+ have "X = {}"
+ by (rule emb_injective[of J I]) simp_all
+ then show "\<mu>G {} = 0" by simp
+ next
+ fix A assume "A \<in> sets generator"
+ from generatorE[OF this] guess J X . note this[simp]
+ interpret J: finite_product_sigma_finite M J by default fact
+ show "0 \<le> \<mu>G A" by simp
+ qed
qed
-lemma (in product_prob_space) additive_\<mu>G: "additive generator \<mu>G"
-proof (intro additive_def[THEN iffD2] ballI impI)
- fix A assume "A \<in> sets generator" with generatorE guess J X . note J = this
- fix B assume "B \<in> sets generator" with generatorE guess K Y . note K = this
- assume "A \<inter> B = {}"
- have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)"
- using J K by auto
- interpret JK: finite_product_sigma_finite M "J \<union> K" by default fact
- have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
- apply (rule emb_injective[of "J \<union> K" I])
- apply (insert `A \<inter> B = {}` JK J K)
- apply (simp_all add: JK.Int emb_simps)
- done
- have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)"
- using J K by simp_all
- then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
- by (simp add: emb_simps)
- also have "\<dots> = measure (Pi\<^isub>M (J \<union> K) M) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
- using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq JK.Un)
- also have "\<dots> = \<mu>G A + \<mu>G B"
- using J K JK_disj by (simp add: JK.measure_additive[symmetric])
- finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
+lemma (in product_prob_space) additive_\<mu>G:
+ assumes "I \<noteq> {}"
+ shows "additive generator \<mu>G"
+proof -
+ interpret G!: algebra generator by (rule algebra_generator) fact
+ show ?thesis
+ proof (intro additive_def[THEN iffD2] ballI impI)
+ fix A assume "A \<in> sets generator" with generatorE guess J X . note J = this
+ fix B assume "B \<in> sets generator" with generatorE guess K Y . note K = this
+ assume "A \<inter> B = {}"
+ have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)"
+ using J K by auto
+ interpret JK: finite_product_sigma_finite M "J \<union> K" by default fact
+ have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
+ apply (rule emb_injective[of "J \<union> K" I])
+ apply (insert `A \<inter> B = {}` JK J K)
+ apply (simp_all add: JK.Int emb_simps)
+ done
+ have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)"
+ using J K by simp_all
+ then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
+ by (simp add: emb_simps)
+ also have "\<dots> = measure (Pi\<^isub>M (J \<union> K) M) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
+ using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq JK.Un)
+ also have "\<dots> = \<mu>G A + \<mu>G B"
+ using J K JK_disj by (simp add: JK.measure_additive[symmetric])
+ finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
+ qed
qed
lemma (in product_prob_space) finite_index_eq_finite_product:
@@ -386,7 +373,7 @@
shows "sets (sigma generator) = sets (Pi\<^isub>M I M)"
proof safe
interpret I: finite_product_sigma_algebra M I by default fact
- have [simp]: "space generator = space (Pi\<^isub>M I M)"
+ have space_generator[simp]: "space generator = space (Pi\<^isub>M I M)"
by (simp add: generator_def product_algebra_def)
{ fix A assume "A \<in> sets (sigma generator)"
then show "A \<in> sets I.P" unfolding sets_sigma
@@ -396,19 +383,32 @@
with `finite I` have "emb I J X \<in> sets I.P" by auto
with `emb I J X = A` show "A \<in> sets I.P" by simp
qed auto }
- { fix A assume "A \<in> sets I.P"
- moreover with I.sets_into_space have "emb I I A = A" by (intro emb_id) auto
- ultimately show "A \<in> sets (sigma generator)"
- using `finite I` I_not_empty unfolding sets_sigma
- by (intro sigma_sets.Basic generatorI[of I A]) auto }
+ { fix A assume A: "A \<in> sets I.P"
+ show "A \<in> sets (sigma generator)"
+ proof cases
+ assume "I = {}"
+ with I.P_empty[OF this] A
+ have "A = space generator \<or> A = {}"
+ unfolding space_generator by auto
+ then show ?thesis
+ by (auto simp: sets_sigma simp del: space_generator
+ intro: sigma_sets.Empty sigma_sets_top)
+ next
+ assume "I \<noteq> {}"
+ note A this
+ moreover with I.sets_into_space have "emb I I A = A" by (intro emb_id) auto
+ ultimately show "A \<in> sets (sigma generator)"
+ using `finite I` unfolding sets_sigma
+ by (intro sigma_sets.Basic generatorI[of I A]) auto
+ qed }
qed
lemma (in product_prob_space) extend_\<mu>G:
"\<exists>\<mu>. (\<forall>s\<in>sets generator. \<mu> s = \<mu>G s) \<and>
- measure_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>"
+ prob_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>"
proof cases
assume "finite I"
- interpret I: finite_product_sigma_finite M I by default fact
+ interpret I: finite_product_prob_space M I by default fact
show ?thesis
proof (intro exI[of _ "measure (Pi\<^isub>M I M)"] ballI conjI)
fix A assume "A \<in> sets generator"
@@ -422,13 +422,20 @@
have "\<lparr>space = space generator, sets = sets (sigma generator), measure = measure I.P\<rparr>
= I.P" (is "?P = _")
by (auto intro!: measure_space.equality simp: finite_index_eq_finite_product[OF `finite I`])
- then show "measure_space ?P" by simp default
+ show "prob_space ?P"
+ proof
+ show "measure_space ?P" using `?P = I.P` by simp default
+ show "measure ?P (space ?P) = 1"
+ using I.measure_space_1 by simp
+ qed
qed
next
let ?G = generator
assume "\<not> finite I"
+ then have I_not_empty: "I \<noteq> {}" by auto
+ interpret G!: algebra generator by (rule algebra_generator) fact
note \<mu>G_mono =
- G.additive_increasing[OF positive_\<mu>G additive_\<mu>G, THEN increasingD]
+ G.additive_increasing[OF positive_\<mu>G[OF I_not_empty] additive_\<mu>G[OF I_not_empty], THEN increasingD]
{ fix Z J assume J: "J \<noteq> {}" "finite J" "J \<subseteq> I" and Z: "Z \<in> sets ?G"
@@ -488,7 +495,9 @@
note this fold le_1 merge_in_G(3) }
note fold = this
- show ?thesis
+ have "\<exists>\<mu>. (\<forall>s\<in>sets ?G. \<mu> s = \<mu>G s) \<and>
+ measure_space \<lparr>space = space ?G, sets = sets (sigma ?G), measure = \<mu>\<rparr>"
+ (is "\<exists>\<mu>. _ \<and> measure_space (?ms \<mu>)")
proof (rule G.caratheodory_empty_continuous[OF positive_\<mu>G additive_\<mu>G])
fix A assume "A \<in> sets ?G"
with generatorE guess J X . note JX = this
@@ -503,7 +512,7 @@
proof (rule ccontr)
assume "(INF i. \<mu>G (A i)) \<noteq> 0" (is "?a \<noteq> 0")
moreover have "0 \<le> ?a"
- using A positive_\<mu>G by (auto intro!: INF_greatest simp: positive_def)
+ using A positive_\<mu>G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def)
ultimately have "0 < ?a" by auto
have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = measure (Pi\<^isub>M J M) X"
@@ -659,7 +668,7 @@
moreover
from w have "?a / 2 ^ (k + 1) \<le> ?q k k (w k)" by auto
then have "?M (J k) (A k) (w k) \<noteq> {}"
- using positive_\<mu>G[unfolded positive_def] `0 < ?a` `?a \<le> 1`
+ using positive_\<mu>G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \<le> 1`
by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq)
then obtain x where "x \<in> ?M (J k) (A k) (w k)" by auto
then have "merge (J k) (w k) (I - J k) x \<in> A k" by auto
@@ -713,28 +722,42 @@
qed
ultimately show "(\<lambda>i. \<mu>G (A i)) ----> 0"
using LIMSEQ_ereal_INFI[of "\<lambda>i. \<mu>G (A i)"] by simp
+ qed fact+
+ then guess \<mu> .. note \<mu> = this
+ show ?thesis
+ proof (intro exI[of _ \<mu>] conjI)
+ show "\<forall>S\<in>sets ?G. \<mu> S = \<mu>G S" using \<mu> by simp
+ show "prob_space (?ms \<mu>)"
+ proof
+ show "measure_space (?ms \<mu>)" using \<mu> by simp
+ obtain i where "i \<in> I" using I_not_empty by auto
+ interpret i: finite_product_sigma_finite M "{i}" by default auto
+ let ?X = "\<Pi>\<^isub>E i\<in>{i}. space (M i)"
+ have X: "?X \<in> sets (Pi\<^isub>M {i} M)"
+ by auto
+ with `i \<in> I` have "emb I {i} ?X \<in> sets generator"
+ by (intro generatorI') auto
+ with \<mu> have "\<mu> (emb I {i} ?X) = \<mu>G (emb I {i} ?X)" by auto
+ with \<mu>G_eq[OF _ _ _ X] `i \<in> I`
+ have "\<mu> (emb I {i} ?X) = measure (M i) (space (M i))"
+ by (simp add: i.measure_times)
+ also have "emb I {i} ?X = space (Pi\<^isub>P I M)"
+ using `i \<in> I` by (auto simp: emb_def infprod_algebra_def generator_def)
+ finally show "measure (?ms \<mu>) (space (?ms \<mu>)) = 1"
+ using M.measure_space_1 by (simp add: infprod_algebra_def)
+ qed
qed
qed
lemma (in product_prob_space) infprod_spec:
- shows "(\<forall>s\<in>sets generator. measure (Pi\<^isub>P I M) s = \<mu>G s) \<and> measure_space (Pi\<^isub>P I M)"
-proof -
- let ?P = "\<lambda>\<mu>. (\<forall>A\<in>sets generator. \<mu> A = \<mu>G A) \<and>
- measure_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>"
- have **: "measure infprod_algebra = (SOME \<mu>. ?P \<mu>)"
- unfolding infprod_algebra_def by simp
- have *: "Pi\<^isub>P I M = \<lparr>space = space generator, sets = sets (sigma generator), measure = measure (Pi\<^isub>P I M)\<rparr>"
- unfolding infprod_algebra_def by auto
- show ?thesis
- apply (subst (2) *)
- apply (unfold **)
- apply (rule someI_ex[where P="?P"])
- apply (rule extend_\<mu>G)
- done
-qed
+ "(\<forall>s\<in>sets generator. measure (Pi\<^isub>P I M) s = \<mu>G s) \<and> prob_space (Pi\<^isub>P I M)"
+ (is "?Q infprod_algebra")
+ unfolding infprod_algebra_def
+ by (rule someI2_ex[OF extend_\<mu>G])
+ (auto simp: sigma_def generator_def)
-sublocale product_prob_space \<subseteq> P: measure_space "Pi\<^isub>P I M"
- using infprod_spec by auto
+sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^isub>P I M"
+ using infprod_spec by simp
lemma (in product_prob_space) measure_infprod_emb:
assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)"
@@ -745,22 +768,6 @@
with \<mu>G_eq[OF assms] infprod_spec show ?thesis by auto
qed
-sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^isub>P I M"
-proof
- obtain i where "i \<in> I" using I_not_empty by auto
- interpret i: finite_product_sigma_finite M "{i}" by default auto
- let ?X = "\<Pi>\<^isub>E i\<in>{i}. space (M i)"
- have "?X \<in> sets (Pi\<^isub>M {i} M)"
- by auto
- from measure_infprod_emb[OF _ _ _ this] `i \<in> I`
- have "\<mu> (emb I {i} ?X) = measure (M i) (space (M i))"
- by (simp add: i.measure_times)
- also have "emb I {i} ?X = space (Pi\<^isub>P I M)"
- using `i \<in> I` by (auto simp: emb_def infprod_algebra_def generator_def)
- finally show "\<mu> (space (Pi\<^isub>P I M)) = 1"
- using M.measure_space_1 by simp
-qed
-
lemma (in product_prob_space) measurable_component:
assumes "i \<in> I"
shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>P I M) (M i)"
@@ -821,7 +828,8 @@
assume "J = {}"
then have "emb I J (Pi\<^isub>E J X) = space infprod_algebra"
by (auto simp: infprod_algebra_def generator_def sigma_def emb_def)
- then show ?thesis using `J = {}` prob_space by simp
+ then show ?thesis using `J = {}` P.prob_space
+ by simp
next
assume "J \<noteq> {}"
interpret J: finite_product_prob_space M J by default fact+
--- a/src/HOL/Probability/Information.thy Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Probability/Information.thy Thu Dec 08 09:10:54 2011 +0100
@@ -198,7 +198,7 @@
proof -
interpret \<nu>: prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact
have ms: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default
- have fms: "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" by default
+ have fms: "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" by unfold_locales
note RN = RN_deriv[OF ms ac]
from real_RN_deriv[OF fms ac] guess D . note D = this
@@ -460,7 +460,7 @@
proof -
interpret information_space M by default fact
interpret v: finite_prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact
- have ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)" by default
+ have ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)" by unfold_locales
from KL_ge_0[OF this ac v.integral_finite_singleton(1)] show ?thesis .
qed
@@ -558,7 +558,7 @@
have eq: "\<forall>A\<in>sets XY.P. (ereal \<circ> joint_distribution X Y) A = XY.\<mu> A"
proof (rule XY.KL_eq_0_imp)
- show "prob_space ?J" by default
+ show "prob_space ?J" by unfold_locales
show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)"
using ac by (simp add: P_def)
show "integrable ?J (entropy_density b XY.P (ereal\<circ>joint_distribution X Y))"
@@ -624,7 +624,7 @@
have "prob_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)"
using X Y by (auto intro!: distribution_prob_space random_variable_pairI)
then show "measure_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)"
- unfolding prob_space_def by simp
+ unfolding prob_space_def finite_measure_def sigma_finite_measure_def by simp
qed auto
qed
@@ -654,7 +654,7 @@
note rv = assms[THEN finite_random_variableD]
show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)"
proof (rule XY.absolutely_continuousI)
- show "finite_measure_space (XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default
+ show "finite_measure_space (XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales
fix x assume "x \<in> space XY.P" and "XY.\<mu> {x} = 0"
then obtain a b where "x = (a, b)"
and "distribution X {a} = 0 \<or> distribution Y {b} = 0"
@@ -684,8 +684,8 @@
interpret P: finite_prob_space "XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>"
using assms by (auto intro!: joint_distribution_finite_prob_space)
- have P_ms: "finite_measure_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default
- have P_ps: "finite_prob_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default
+ have P_ms: "finite_measure_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales
+ have P_ps: "finite_prob_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales
show ?sum
unfolding Let_def mutual_information_def
--- a/src/HOL/Probability/Measure.thy Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Probability/Measure.thy Thu Dec 08 09:10:54 2011 +0100
@@ -1175,13 +1175,21 @@
finally show ?thesis by simp
qed
-locale finite_measure = measure_space +
+locale finite_measure = sigma_finite_measure +
assumes finite_measure_of_space: "\<mu> (space M) \<noteq> \<infinity>"
-sublocale finite_measure < sigma_finite_measure
-proof
- show "\<exists>A. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<infinity>)"
- using finite_measure_of_space by (auto intro!: exI[of _ "\<lambda>x. space M"])
+lemma finite_measureI[Pure.intro!]:
+ assumes "measure_space M"
+ assumes *: "measure M (space M) \<noteq> \<infinity>"
+ shows "finite_measure M"
+proof -
+ interpret measure_space M by fact
+ show "finite_measure M"
+ proof
+ show "measure M (space M) \<noteq> \<infinity>" by fact
+ show "\<exists>A. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<infinity>)"
+ using * by (auto intro!: exI[of _ "\<lambda>x. space M"])
+ qed
qed
lemma (in finite_measure) finite_measure[simp, intro]:
@@ -1222,22 +1230,19 @@
assumes "S \<in> sets M"
shows "finite_measure (restricted_space S)"
(is "finite_measure ?r")
- unfolding finite_measure_def finite_measure_axioms_def
-proof (intro conjI)
+proof
show "measure_space ?r" using restricted_measure_space[OF assms] .
-next
show "measure ?r (space ?r) \<noteq> \<infinity>" using finite_measure[OF `S \<in> sets M`] by auto
qed
lemma (in measure_space) restricted_to_finite_measure:
assumes "S \<in> sets M" "\<mu> S \<noteq> \<infinity>"
shows "finite_measure (restricted_space S)"
-proof -
- have "measure_space (restricted_space S)"
+proof
+ show "measure_space (restricted_space S)"
using `S \<in> sets M` by (rule restricted_measure_space)
- then show ?thesis
- unfolding finite_measure_def finite_measure_axioms_def
- using assms by auto
+ show "measure (restricted_space S) (space (restricted_space S)) \<noteq> \<infinity>"
+ by simp fact
qed
lemma (in finite_measure) finite_measure_Diff:
@@ -1357,66 +1362,43 @@
section "Finite spaces"
-locale finite_measure_space = measure_space + finite_sigma_algebra +
- assumes finite_single_measure[simp]: "\<And>x. x \<in> space M \<Longrightarrow> \<mu> {x} \<noteq> \<infinity>"
+locale finite_measure_space = finite_measure + finite_sigma_algebra
+
+lemma finite_measure_spaceI[Pure.intro!]:
+ assumes "finite (space M)"
+ assumes sets_Pow: "sets M = Pow (space M)"
+ and space: "measure M (space M) \<noteq> \<infinity>"
+ and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> measure M {x}"
+ and add: "\<And>A. A \<subseteq> space M \<Longrightarrow> measure M A = (\<Sum>x\<in>A. measure M {x})"
+ shows "finite_measure_space M"
+proof -
+ interpret finite_sigma_algebra M
+ proof
+ show "finite (space M)" by fact
+ qed (auto simp: sets_Pow)
+ interpret measure_space M
+ proof (rule finite_additivity_sufficient)
+ show "sigma_algebra M" by default
+ show "finite (space M)" by fact
+ show "positive M (measure M)"
+ by (auto simp: add positive_def intro!: setsum_nonneg pos)
+ show "additive M (measure M)"
+ using `finite (space M)`
+ by (auto simp add: additive_def add
+ intro!: setsum_Un_disjoint dest: finite_subset)
+ qed
+ interpret finite_measure M
+ proof
+ show "\<mu> (space M) \<noteq> \<infinity>" by fact
+ qed default
+ show "finite_measure_space M"
+ by default
+qed
lemma (in finite_measure_space) sum_over_space: "(\<Sum>x\<in>space M. \<mu> {x}) = \<mu> (space M)"
using measure_setsum[of "space M" "\<lambda>i. {i}"]
by (simp add: sets_eq_Pow disjoint_family_on_def finite_space)
-lemma finite_measure_spaceI:
- assumes "finite (space M)" "sets M = Pow(space M)" and space: "measure M (space M) \<noteq> \<infinity>"
- and add: "\<And>A B. A\<subseteq>space M \<Longrightarrow> B\<subseteq>space M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M B"
- and "measure M {} = 0" "\<And>A. A \<subseteq> space M \<Longrightarrow> 0 \<le> measure M A"
- shows "finite_measure_space M"
- unfolding finite_measure_space_def finite_measure_space_axioms_def
-proof (intro allI impI conjI)
- show "measure_space M"
- proof (rule finite_additivity_sufficient)
- have *: "\<lparr>space = space M, sets = Pow (space M), \<dots> = algebra.more M\<rparr> = M"
- unfolding assms(2)[symmetric] by (auto intro!: algebra.equality)
- show "sigma_algebra M"
- using sigma_algebra_Pow[of "space M" "algebra.more M"]
- unfolding * .
- show "finite (space M)" by fact
- show "positive M (measure M)" unfolding positive_def using assms by auto
- show "additive M (measure M)" unfolding additive_def using assms by simp
- qed
- then interpret measure_space M .
- show "finite_sigma_algebra M"
- proof
- show "finite (space M)" by fact
- show "sets M = Pow (space M)" using assms by auto
- qed
- { fix x assume *: "x \<in> space M"
- with add[of "{x}" "space M - {x}"] space
- show "\<mu> {x} \<noteq> \<infinity>" by (auto simp: insert_absorb[OF *] Diff_subset) }
-qed
-
-sublocale finite_measure_space \<subseteq> finite_measure
-proof
- show "\<mu> (space M) \<noteq> \<infinity>"
- unfolding sum_over_space[symmetric] setsum_Pinfty
- using finite_space finite_single_measure by auto
-qed
-
-lemma finite_measure_space_iff:
- "finite_measure_space M \<longleftrightarrow>
- finite (space M) \<and> sets M = Pow(space M) \<and> measure M (space M) \<noteq> \<infinity> \<and>
- measure M {} = 0 \<and> (\<forall>A\<subseteq>space M. 0 \<le> measure M A) \<and>
- (\<forall>A\<subseteq>space M. \<forall>B\<subseteq>space M. A \<inter> B = {} \<longrightarrow> measure M (A \<union> B) = measure M A + measure M B)"
- (is "_ = ?rhs")
-proof (intro iffI)
- assume "finite_measure_space M"
- then interpret finite_measure_space M .
- show ?rhs
- using finite_space sets_eq_Pow measure_additive empty_measure finite_measure
- by auto
-next
- assume ?rhs then show "finite_measure_space M"
- by (auto intro!: finite_measure_spaceI)
-qed
-
lemma (in finite_measure_space) finite_measure_singleton:
assumes A: "A \<subseteq> space M" shows "\<mu>' A = (\<Sum>x\<in>A. \<mu>' {x})"
using A finite_subset[OF A finite_space]
--- a/src/HOL/Probability/Probability_Measure.thy Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Thu Dec 08 09:10:54 2011 +0100
@@ -9,12 +9,20 @@
imports Lebesgue_Measure
begin
-locale prob_space = measure_space +
+locale prob_space = finite_measure +
assumes measure_space_1: "measure M (space M) = 1"
-sublocale prob_space < finite_measure
-proof
- from measure_space_1 show "\<mu> (space M) \<noteq> \<infinity>" by simp
+lemma prob_spaceI[Pure.intro!]:
+ assumes "measure_space M"
+ assumes *: "measure M (space M) = 1"
+ shows "prob_space M"
+proof -
+ interpret finite_measure M
+ proof
+ show "measure_space M" by fact
+ show "measure M (space M) \<noteq> \<infinity>" using * by simp
+ qed
+ show "prob_space M" by default fact
qed
abbreviation (in prob_space) "events \<equiv> sets M"
@@ -31,9 +39,10 @@
lemma (in prob_space) prob_space_cong:
assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "space N = space M" "sets N = sets M"
shows "prob_space N"
-proof -
- interpret N: measure_space N by (intro measure_space_cong assms)
- show ?thesis by default (insert assms measure_space_1, simp)
+proof
+ show "measure_space N" by (intro measure_space_cong assms)
+ show "measure N (space N) = 1"
+ using measure_space_1 assms by simp
qed
lemma (in prob_space) distribution_cong:
@@ -201,18 +210,17 @@
assumes S: "sigma_algebra S"
assumes T: "T \<in> measure_preserving M S"
shows "prob_space S"
-proof -
+proof
interpret S: measure_space S
using S and T by (rule measure_space_vimage)
- show ?thesis
- proof
- from T[THEN measure_preservingD2]
- have "T -` space S \<inter> space M = space M"
- by (auto simp: measurable_def)
- with T[THEN measure_preservingD, of "space S", symmetric]
- show "measure S (space S) = 1"
- using measure_space_1 by simp
- qed
+ show "measure_space S" ..
+
+ from T[THEN measure_preservingD2]
+ have "T -` space S \<inter> space M = space M"
+ by (auto simp: measurable_def)
+ with T[THEN measure_preservingD, of "space S", symmetric]
+ show "measure S (space S) = 1"
+ using measure_space_1 by simp
qed
lemma prob_space_unique_Int_stable:
@@ -539,12 +547,14 @@
joint_distribution (\<lambda>x. (X x, Y x)) Z {((x, y), z)}"
unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
-locale pair_prob_space = M1: prob_space M1 + M2: prob_space M2 for M1 M2
-
-sublocale pair_prob_space \<subseteq> pair_sigma_finite M1 M2 by default
+locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2
sublocale pair_prob_space \<subseteq> P: prob_space P
-by default (simp add: pair_measure_times M1.measure_space_1 M2.measure_space_1 space_pair_measure)
+proof
+ show "measure_space P" ..
+ show "measure P (space P) = 1"
+ by (simp add: pair_measure_times M1.measure_space_1 M2.measure_space_1 space_pair_measure)
+qed
lemma countably_additiveI[case_names countably]:
assumes "\<And>A. \<lbrakk> range A \<subseteq> sets M ; disjoint_family A ; (\<Union>i. A i) \<in> sets M\<rbrakk> \<Longrightarrow>
@@ -557,20 +567,21 @@
shows "prob_space ((MX \<Otimes>\<^isub>M MY) \<lparr> measure := ereal \<circ> joint_distribution X Y\<rparr>)"
using random_variable_pairI[OF assms] by (rule distribution_prob_space)
+locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme" +
+ fixes I :: "'i set"
+ assumes prob_space: "\<And>i. prob_space (M i)"
-locale finite_product_prob_space =
- fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme"
- and I :: "'i set"
- assumes prob_space: "\<And>i. prob_space (M i)" and finite_index: "finite I"
-
-sublocale finite_product_prob_space \<subseteq> M: prob_space "M i" for i
+sublocale product_prob_space \<subseteq> M: prob_space "M i" for i
by (rule prob_space)
-sublocale finite_product_prob_space \<subseteq> finite_product_sigma_finite M I
- by default (rule finite_index)
+locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I
sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^isub>M i\<in>I. M i"
- proof qed (simp add: measure_times M.measure_space_1 setprod_1)
+proof
+ show "measure_space P" ..
+ show "measure P (space P) = 1"
+ by (simp add: measure_times M.measure_space_1 setprod_1)
+qed
lemma (in finite_product_prob_space) prob_times:
assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets (M i)"
@@ -667,7 +678,7 @@
interpret MX: finite_sigma_algebra MX using assms by simp
interpret MY: finite_sigma_algebra MY using assms by simp
interpret P: pair_finite_sigma_algebra MX MY by default
- show "finite_sigma_algebra (MX \<Otimes>\<^isub>M MY)" by default
+ show "finite_sigma_algebra (MX \<Otimes>\<^isub>M MY)" ..
have sa: "sigma_algebra M" by default
show "(\<lambda>x. (X x, Y x)) \<in> measurable M (MX \<Otimes>\<^isub>M MY)"
unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def)
@@ -754,25 +765,9 @@
using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"]
using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp
-locale pair_finite_prob_space = M1: finite_prob_space M1 + M2: finite_prob_space M2 for M1 M2
-
-sublocale pair_finite_prob_space \<subseteq> pair_prob_space M1 M2 by default
-sublocale pair_finite_prob_space \<subseteq> pair_finite_space M1 M2 by default
-sublocale pair_finite_prob_space \<subseteq> finite_prob_space P by default
+locale pair_finite_prob_space = pair_prob_space M1 M2 + pair_finite_space M1 M2 + M1: finite_prob_space M1 + M2: finite_prob_space M2 for M1 M2
-locale product_finite_prob_space =
- fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme"
- and I :: "'i set"
- assumes finite_space: "\<And>i. finite_prob_space (M i)" and finite_index: "finite I"
-
-sublocale product_finite_prob_space \<subseteq> M!: finite_prob_space "M i" using finite_space .
-sublocale product_finite_prob_space \<subseteq> finite_product_sigma_finite M I by default (rule finite_index)
-sublocale product_finite_prob_space \<subseteq> prob_space "Pi\<^isub>M I M"
-proof
- show "\<mu> (space P) = 1"
- using measure_times[OF M.top] M.measure_space_1
- by (simp add: setprod_1 space_product_algebra)
-qed
+sublocale pair_finite_prob_space \<subseteq> finite_prob_space P by default
lemma funset_eq_UN_fun_upd_I:
assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
@@ -815,7 +810,12 @@
using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
qed
-lemma (in product_finite_prob_space) singleton_eq_product:
+locale finite_product_finite_prob_space = finite_product_prob_space M I for M I +
+ assumes finite_space: "\<And>i. finite_prob_space (M i)"
+
+sublocale finite_product_finite_prob_space \<subseteq> M!: finite_prob_space "M i" using finite_space .
+
+lemma (in finite_product_finite_prob_space) singleton_eq_product:
assumes x: "x \<in> space P" shows "{x} = (\<Pi>\<^isub>E i\<in>I. {x i})"
proof (safe intro!: ext[of _ x])
fix y i assume *: "y \<in> (\<Pi> i\<in>I. {x i})" "y \<in> extensional I"
@@ -823,7 +823,7 @@
by (cases "i \<in> I") (auto simp: extensional_def)
qed (insert x, auto)
-sublocale product_finite_prob_space \<subseteq> finite_prob_space "Pi\<^isub>M I M"
+sublocale finite_product_finite_prob_space \<subseteq> finite_prob_space "Pi\<^isub>M I M"
proof
show "finite (space P)"
using finite_index M.finite_space by auto
@@ -844,23 +844,18 @@
then show "X \<in> sets P" by simp
qed
with space_closed show [simp]: "sets P = Pow (space P)" ..
-
- { fix x assume "x \<in> space P"
- from this top have "\<mu> {x} \<le> \<mu> (space P)" by (intro measure_mono) auto
- then show "\<mu> {x} \<noteq> \<infinity>"
- using measure_space_1 by auto }
qed
-lemma (in product_finite_prob_space) measure_finite_times:
+lemma (in finite_product_finite_prob_space) measure_finite_times:
"(\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)) \<Longrightarrow> \<mu> (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.\<mu> i (X i))"
by (rule measure_times) simp
-lemma (in product_finite_prob_space) measure_singleton_times:
+lemma (in finite_product_finite_prob_space) measure_singleton_times:
assumes x: "x \<in> space P" shows "\<mu> {x} = (\<Prod>i\<in>I. M.\<mu> i {x i})"
unfolding singleton_eq_product[OF x] using x
by (intro measure_finite_times) auto
-lemma (in product_finite_prob_space) prob_finite_times:
+lemma (in finite_product_finite_prob_space) prob_finite_times:
assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)"
shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))"
proof -
@@ -873,13 +868,13 @@
finally show ?thesis by simp
qed
-lemma (in product_finite_prob_space) prob_singleton_times:
+lemma (in finite_product_finite_prob_space) prob_singleton_times:
assumes x: "x \<in> space P"
shows "prob {x} = (\<Prod>i\<in>I. M.prob i {x i})"
unfolding singleton_eq_product[OF x] using x
by (intro prob_finite_times) auto
-lemma (in product_finite_prob_space) prob_finite_product:
+lemma (in finite_product_finite_prob_space) prob_finite_product:
"A \<subseteq> space P \<Longrightarrow> prob A = (\<Sum>x\<in>A. \<Prod>i\<in>I. M.prob i {x i})"
by (auto simp add: finite_measure_singleton prob_singleton_times
simp del: space_product_algebra
@@ -1010,11 +1005,12 @@
assumes "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M"
and "\<And>A. A \<in> sets N \<Longrightarrow> measure N A = \<mu> A"
shows "prob_space N"
-proof -
+proof
interpret N: measure_space N
by (rule measure_space_subalgebra[OF assms])
- show ?thesis
- proof qed (insert assms(4)[OF N.top], simp add: assms measure_space_1)
+ show "measure_space N" ..
+ show "measure N (space N) = 1"
+ using assms(4)[OF N.top] by (simp add: assms measure_space_1)
qed
lemma (in prob_space) prob_space_of_restricted_space:
@@ -1028,44 +1024,76 @@
by (rule A.sigma_algebra_cong) auto
show "prob_space ?P"
proof
+ show "measure_space ?P"
+ proof
+ show "positive ?P (measure ?P)"
+ proof (simp add: positive_def, safe)
+ show "0 / \<mu> A = 0" using `\<mu> A \<noteq> 0` by (cases "\<mu> A") (auto simp: zero_ereal_def)
+ fix B assume "B \<in> events"
+ with real_measure[of "A \<inter> B"] real_measure[OF `A \<in> events`] `A \<in> sets M`
+ show "0 \<le> \<mu> (A \<inter> B) / \<mu> A" by (auto simp: Int)
+ qed
+ show "countably_additive ?P (measure ?P)"
+ proof (simp add: countably_additive_def, safe)
+ fix B and F :: "nat \<Rightarrow> 'a set"
+ assume F: "range F \<subseteq> op \<inter> A ` events" "disjoint_family F"
+ { fix i
+ from F have "F i \<in> op \<inter> A ` events" by auto
+ with `A \<in> events` have "F i \<in> events" by auto }
+ moreover then have "range F \<subseteq> events" by auto
+ moreover have "\<And>S. \<mu> S / \<mu> A = inverse (\<mu> A) * \<mu> S"
+ by (simp add: mult_commute divide_ereal_def)
+ moreover have "0 \<le> inverse (\<mu> A)"
+ using real_measure[OF `A \<in> events`] by auto
+ ultimately show "(\<Sum>i. \<mu> (F i) / \<mu> A) = \<mu> (\<Union>i. F i) / \<mu> A"
+ using measure_countably_additive[of F] F
+ by (auto simp: suminf_cmult_ereal)
+ qed
+ qed
show "measure ?P (space ?P) = 1"
using real_measure[OF `A \<in> events`] `\<mu> A \<noteq> 0` by auto
- show "positive ?P (measure ?P)"
- proof (simp add: positive_def, safe)
- show "0 / \<mu> A = 0" using `\<mu> A \<noteq> 0` by (cases "\<mu> A") (auto simp: zero_ereal_def)
- fix B assume "B \<in> events"
- with real_measure[of "A \<inter> B"] real_measure[OF `A \<in> events`] `A \<in> sets M`
- show "0 \<le> \<mu> (A \<inter> B) / \<mu> A" by (auto simp: Int)
- qed
- show "countably_additive ?P (measure ?P)"
- proof (simp add: countably_additive_def, safe)
- fix B and F :: "nat \<Rightarrow> 'a set"
- assume F: "range F \<subseteq> op \<inter> A ` events" "disjoint_family F"
- { fix i
- from F have "F i \<in> op \<inter> A ` events" by auto
- with `A \<in> events` have "F i \<in> events" by auto }
- moreover then have "range F \<subseteq> events" by auto
- moreover have "\<And>S. \<mu> S / \<mu> A = inverse (\<mu> A) * \<mu> S"
- by (simp add: mult_commute divide_ereal_def)
- moreover have "0 \<le> inverse (\<mu> A)"
- using real_measure[OF `A \<in> events`] by auto
- ultimately show "(\<Sum>i. \<mu> (F i) / \<mu> A) = \<mu> (\<Union>i. F i) / \<mu> A"
- using measure_countably_additive[of F] F
- by (auto simp: suminf_cmult_ereal)
- qed
qed
qed
lemma finite_prob_spaceI:
assumes "finite (space M)" "sets M = Pow(space M)"
- and "measure M (space M) = 1" "measure M {} = 0" "\<And>A. A \<subseteq> space M \<Longrightarrow> 0 \<le> measure M A"
- and "\<And>A B. A\<subseteq>space M \<Longrightarrow> B\<subseteq>space M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M B"
+ and 1: "measure M (space M) = 1" and "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> measure M {x}"
+ and add: "\<And>A B. A \<subseteq> space M \<Longrightarrow> measure M A = (\<Sum>x\<in>A. measure M {x})"
shows "finite_prob_space M"
- unfolding finite_prob_space_eq
-proof
- show "finite_measure_space M" using assms
- by (auto intro!: finite_measure_spaceI)
- show "measure M (space M) = 1" by fact
+proof -
+ interpret finite_measure_space M
+ proof
+ show "measure M (space M) \<noteq> \<infinity>" using 1 by simp
+ qed fact+
+ show ?thesis by default fact
+qed
+
+lemma (in finite_prob_space) distribution_eq_setsum:
+ "distribution X A = (\<Sum>x\<in>A \<inter> X ` space M. distribution X {x})"
+proof -
+ have *: "X -` A \<inter> space M = (\<Union>x\<in>A \<inter> X ` space M. X -` {x} \<inter> space M)"
+ by auto
+ then show "distribution X A = (\<Sum>x\<in>A \<inter> X ` space M. distribution X {x})"
+ using finite_space unfolding distribution_def *
+ by (intro finite_measure_finite_Union)
+ (auto simp: disjoint_family_on_def)
+qed
+
+lemma (in finite_prob_space) distribution_eq_setsum_finite:
+ assumes "finite A"
+ shows "distribution X A = (\<Sum>x\<in>A. distribution X {x})"
+proof -
+ note distribution_eq_setsum[of X A]
+ also have "(\<Sum>x\<in>A \<inter> X ` space M. distribution X {x}) = (\<Sum>x\<in>A. distribution X {x})"
+ proof (intro setsum_mono_zero_cong_left ballI)
+ fix i assume "i\<in>A - A \<inter> X ` space M"
+ then have "X -` {i} \<inter> space M = {}" by auto
+ then show "distribution X {i} = 0"
+ by (simp add: distribution_def)
+ next
+ show "finite A" by fact
+ qed simp_all
+ finally show ?thesis .
qed
lemma (in finite_prob_space) finite_measure_space:
@@ -1075,11 +1103,9 @@
proof (rule finite_measure_spaceI, simp_all)
show "finite (X ` space M)" using finite_space by simp
next
- fix A B :: "'x set" assume "A \<inter> B = {}"
- then show "distribution X (A \<union> B) = distribution X A + distribution X B"
- unfolding distribution_def
- by (subst finite_measure_Union[symmetric])
- (auto intro!: arg_cong[where f=\<mu>'] simp: sets_eq_Pow)
+ fix A assume "A \<subseteq> X ` space M"
+ then show "distribution X A = (\<Sum>x\<in>A. distribution X {x})"
+ by (subst distribution_eq_setsum) (simp add: Int_absorb2)
qed
lemma (in finite_prob_space) finite_prob_space_of_images:
@@ -1095,11 +1121,9 @@
show "finite (s1 \<times> s2)"
using assms by auto
next
- fix A B :: "('x*'y) set" assume "A \<inter> B = {}"
- then show "joint_distribution X Y (A \<union> B) = joint_distribution X Y A + joint_distribution X Y B"
- unfolding distribution_def
- by (subst finite_measure_Union[symmetric])
- (auto intro!: arg_cong[where f=\<mu>'] simp: sets_eq_Pow)
+ fix A assume "A \<subseteq> (s1 \<times> s2)"
+ with assms show "joint_distribution X Y A = (\<Sum>x\<in>A. joint_distribution X Y {x})"
+ by (intro distribution_eq_setsum_finite) (auto dest: finite_subset)
qed
lemma (in finite_prob_space) finite_product_measure_space_of_images:
@@ -1140,7 +1164,10 @@
by (simp add: pborel_def)
interpretation pborel: prob_space pborel
- by default (simp add: one_ereal_def pborel_def)
+proof
+ show "measure pborel (space pborel) = 1"
+ by (simp add: one_ereal_def pborel_def)
+qed default
lemma pborel_prob: "pborel.prob A = (if A \<in> sets borel \<and> A \<subseteq> {0 ..< 1} then real (lborel.\<mu> A) else 0)"
unfolding pborel.\<mu>'_def by (auto simp: pborel_def)
--- a/src/HOL/Probability/Radon_Nikodym.thy Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Thu Dec 08 09:10:54 2011 +0100
@@ -427,35 +427,38 @@
have f_le_\<nu>: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. ?F A x \<partial>M) \<le> \<nu> A"
using `f \<in> G` unfolding G_def by auto
have fmM: "finite_measure ?M"
- proof (default, simp_all add: countably_additive_def positive_def, safe del: notI)
- fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "disjoint_family A"
- have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. (\<Sum>n. ?F (A n) x) \<partial>M)"
- using `range A \<subseteq> sets M` `\<And>x. 0 \<le> f x`
- by (intro positive_integral_suminf[symmetric]) auto
- also have "\<dots> = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)"
- using `\<And>x. 0 \<le> f x`
- by (intro positive_integral_cong) (simp add: suminf_cmult_ereal suminf_indicator[OF `disjoint_family A`])
- finally have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)" .
- moreover have "(\<Sum>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
- using M'.measure_countably_additive A by (simp add: comp_def)
- moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<infinity>" using M'.finite_measure A by (simp add: countable_UN)
- moreover {
- have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<le> \<nu> (\<Union>i. A i)"
- using A `f \<in> G` unfolding G_def by (auto simp: countable_UN)
- also have "\<nu> (\<Union>i. A i) < \<infinity>" using v_fin by simp
- finally have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<noteq> \<infinity>" by simp }
- moreover have "\<And>i. (\<integral>\<^isup>+x. ?F (A i) x \<partial>M) \<le> \<nu> (A i)"
- using A by (intro f_le_\<nu>) auto
- ultimately
- show "(\<Sum>n. ?t (A n)) = ?t (\<Union>i. A i)"
- by (subst suminf_ereal_minus) (simp_all add: positive_integral_positive)
+ proof
+ show "measure_space ?M"
+ proof (default, simp_all add: countably_additive_def positive_def, safe del: notI)
+ fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "disjoint_family A"
+ have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. (\<Sum>n. ?F (A n) x) \<partial>M)"
+ using `range A \<subseteq> sets M` `\<And>x. 0 \<le> f x`
+ by (intro positive_integral_suminf[symmetric]) auto
+ also have "\<dots> = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)"
+ using `\<And>x. 0 \<le> f x`
+ by (intro positive_integral_cong) (simp add: suminf_cmult_ereal suminf_indicator[OF `disjoint_family A`])
+ finally have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)" .
+ moreover have "(\<Sum>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
+ using M'.measure_countably_additive A by (simp add: comp_def)
+ moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<infinity>" using M'.finite_measure A by (simp add: countable_UN)
+ moreover {
+ have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<le> \<nu> (\<Union>i. A i)"
+ using A `f \<in> G` unfolding G_def by (auto simp: countable_UN)
+ also have "\<nu> (\<Union>i. A i) < \<infinity>" using v_fin by simp
+ finally have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<noteq> \<infinity>" by simp }
+ moreover have "\<And>i. (\<integral>\<^isup>+x. ?F (A i) x \<partial>M) \<le> \<nu> (A i)"
+ using A by (intro f_le_\<nu>) auto
+ ultimately
+ show "(\<Sum>n. ?t (A n)) = ?t (\<Union>i. A i)"
+ by (subst suminf_ereal_minus) (simp_all add: positive_integral_positive)
+ next
+ fix A assume A: "A \<in> sets M" show "0 \<le> \<nu> A - \<integral>\<^isup>+ x. ?F A x \<partial>M"
+ using f_le_\<nu>[OF A] `f \<in> G` M'.finite_measure[OF A] by (auto simp: G_def ereal_le_minus_iff)
+ qed
next
- fix A assume A: "A \<in> sets M" show "0 \<le> \<nu> A - \<integral>\<^isup>+ x. ?F A x \<partial>M"
- using f_le_\<nu>[OF A] `f \<in> G` M'.finite_measure[OF A] by (auto simp: G_def ereal_le_minus_iff)
- next
- show "\<nu> (space M) - (\<integral>\<^isup>+ x. ?F (space M) x \<partial>M) \<noteq> \<infinity>" (is "?a - ?b \<noteq> _")
+ show "measure ?M (space ?M) \<noteq> \<infinity>"
using positive_integral_positive[of "?F (space M)"]
- by (cases rule: ereal2_cases[of ?a ?b]) auto
+ by (cases rule: ereal2_cases[of "\<nu> (space M)" "\<integral>\<^isup>+ x. ?F (space M) x \<partial>M"]) auto
qed
then interpret M: finite_measure ?M
where "space ?M = space M" and "sets ?M = sets M" and "measure ?M = ?t"
@@ -498,11 +501,14 @@
interpret b: sigma_algebra ?Mb by (intro sigma_algebra_cong) auto
have Mb: "finite_measure ?Mb"
proof
- show "positive ?Mb (measure ?Mb)"
- using `0 \<le> b` by (auto simp: positive_def)
- show "countably_additive ?Mb (measure ?Mb)"
- using `0 \<le> b` measure_countably_additive
- by (auto simp: countably_additive_def suminf_cmult_ereal subset_eq)
+ show "measure_space ?Mb"
+ proof
+ show "positive ?Mb (measure ?Mb)"
+ using `0 \<le> b` by (auto simp: positive_def)
+ show "countably_additive ?Mb (measure ?Mb)"
+ using `0 \<le> b` measure_countably_additive
+ by (auto simp: countably_additive_def suminf_cmult_ereal subset_eq)
+ qed
show "measure ?Mb (space ?Mb) \<noteq> \<infinity>"
using b by auto
qed
@@ -772,7 +778,6 @@
(is "finite_measure ?R") by (rule restricted_finite_measure[OF Q_sets[of i]])
then interpret R: finite_measure ?R .
have fmv: "finite_measure (restricted_space (Q i) \<lparr> measure := \<nu>\<rparr>)" (is "finite_measure ?Q")
- unfolding finite_measure_def finite_measure_axioms_def
proof
show "measure_space ?Q"
using v.restricted_measure_space Q_sets[of i] by auto
@@ -849,8 +854,8 @@
let ?MT = "M\<lparr> measure := ?T \<rparr>"
interpret T: finite_measure ?MT
where "space ?MT = space M" and "sets ?MT = sets M" and "measure ?MT = ?T"
- unfolding finite_measure_def finite_measure_axioms_def using borel finite nn
- by (auto intro!: measure_space_density cong: positive_integral_cong)
+ using borel finite nn
+ by (auto intro!: measure_space_density finite_measureI cong: positive_integral_cong)
have "T.absolutely_continuous \<nu>"
proof (unfold T.absolutely_continuous_def, safe)
fix N assume "N \<in> sets M" "(\<integral>\<^isup>+x. h x * indicator N x \<partial>M) = 0"
@@ -1000,7 +1005,7 @@
using h_borel h_nn by (rule measure_space_density) simp
then interpret h: measure_space ?H .
interpret h: finite_measure "M\<lparr> measure := \<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x \<partial>M) \<rparr>"
- by default (simp cong: positive_integral_cong add: fin)
+ by (intro H finite_measureI) (simp cong: positive_integral_cong add: fin)
let ?fM = "M\<lparr>measure := \<lambda>A. (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)\<rparr>"
interpret f: measure_space ?fM
using f by (rule measure_space_density) simp
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Thu Dec 08 09:10:54 2011 +0100
@@ -22,11 +22,8 @@
by (simp_all add: M_def)
sublocale finite_space \<subseteq> finite_measure_space M
-proof (rule finite_measure_spaceI)
- fix A B :: "'a set" assume "A \<inter> B = {}" "A \<subseteq> space M" "B \<subseteq> space M"
- then show "measure M (A \<union> B) = measure M A + measure M B"
- by (simp add: M_def card_Un_disjoint finite_subset[OF _ finite] field_simps)
-qed (auto simp: M_def divide_nonneg_nonneg)
+ by (rule finite_measure_spaceI)
+ (simp_all add: M_def real_of_nat_def)
sublocale finite_space \<subseteq> information_space M 2
by default (simp_all add: M_def one_ereal_def)
--- a/src/HOL/Quotient.thy Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Quotient.thy Thu Dec 08 09:10:54 2011 +0100
@@ -747,6 +747,15 @@
{* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
{* set up the three goals for the decending theorems *}
+method_setup partiality_descending =
+ {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_tac ctxt []))) *}
+ {* decend theorems to the raw level *}
+
+method_setup partiality_descending_setup =
+ {* Scan.succeed (fn ctxt =>
+ SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))) *}
+ {* set up the three goals for the decending theorems *}
+
method_setup regularize =
{* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
{* prove the regularization goals from the quotient lifting procedure *}
--- a/src/HOL/Tools/ATP/atp_translate.ML Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Dec 08 09:10:54 2011 +0100
@@ -127,10 +127,9 @@
val hybrid_lamsN = "hybrid_lams"
val keep_lamsN = "keep_lams"
-(* TFF1 is still in development, and it is still unclear whether symbols will be
- allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
- ghost type variables. *)
-val avoid_first_order_ghost_type_vars = true
+(* It's still unclear whether all TFF1 implementations will support type
+ signatures such as "!>[A : $tType] : $o", with ghost type variables. *)
+val avoid_first_order_ghost_type_vars = false
val bound_var_prefix = "B_"
val all_bound_var_prefix = "BA_"
@@ -1946,8 +1945,12 @@
fun decl_line_for_class order s =
let val name as (s, _) = `make_type_class s in
Decl (sym_decl_prefix ^ s, name,
- if order = First_Order andalso avoid_first_order_ghost_type_vars then
- ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype))
+ if order = First_Order then
+ ATyAbs ([tvar_a_name],
+ if avoid_first_order_ghost_type_vars then
+ AFun (a_itself_atype, bool_atype)
+ else
+ bool_atype)
else
AFun (atype_of_types, bool_atype))
end
@@ -2263,24 +2266,27 @@
fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
+fun rationalize_decls ctxt (decls as decl :: (decls' as _ :: _)) =
+ let
+ val T = result_type_of_decl decl
+ |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
+ in
+ if forall (type_generalization ctxt T o result_type_of_decl) decls' then
+ [decl]
+ else
+ decls
+ end
+ | rationalize_decls _ decls = decls
+
fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
(s, decls) =
case type_enc of
Simple_Types _ =>
- decls |> map (decl_line_for_sym ctxt format mono type_enc s)
+ decls |> rationalize_decls ctxt
+ |> map (decl_line_for_sym ctxt format mono type_enc s)
| Guards (_, level) =>
let
- val decls =
- case decls of
- decl :: (decls' as _ :: _) =>
- let val T = result_type_of_decl decl in
- if forall (type_generalization ctxt T o result_type_of_decl)
- decls' then
- [decl]
- else
- decls
- end
- | _ => decls
+ val decls = decls |> rationalize_decls ctxt
val n = length decls
val decls =
decls |> filter (should_encode_type ctxt mono level
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Dec 08 09:10:54 2011 +0100
@@ -14,6 +14,9 @@
val descend_procedure_tac: Proof.context -> thm list -> int -> tactic
val descend_tac: Proof.context -> thm list -> int -> tactic
+ val partiality_descend_procedure_tac: Proof.context -> thm list -> int -> tactic
+ val partiality_descend_tac: Proof.context -> thm list -> int -> tactic
+
val lift_procedure_tac: Proof.context -> thm list -> thm -> int -> tactic
val lift_tac: Proof.context -> thm list -> thm list -> int -> tactic
@@ -580,13 +583,22 @@
the Quot_True premise in 2nd records the lifted theorem
*)
-val lifting_procedure_thm =
+val procedure_thm =
@{lemma "[|A;
A --> B;
Quot_True D ==> B = C;
C = D|] ==> D"
by (simp add: Quot_True_def)}
+(* in case of partial equivalence relations, this form of the
+ procedure theorem results in solvable proof obligations
+*)
+val partiality_procedure_thm =
+ @{lemma "[|B;
+ Quot_True D ==> B = C;
+ C = D|] ==> D"
+ by (simp add: Quot_True_def)}
+
fun lift_match_error ctxt msg rtrm qtrm =
let
val rtrm_str = Syntax.string_of_term ctxt rtrm
@@ -611,7 +623,7 @@
[SOME (cterm_of thy rtrm'),
SOME (cterm_of thy reg_goal),
NONE,
- SOME (cterm_of thy inj_goal)] lifting_procedure_thm
+ SOME (cterm_of thy inj_goal)] procedure_thm
end
@@ -655,6 +667,56 @@
end
+(** descending for partial equivalence relations **)
+
+fun partiality_procedure_inst ctxt rtrm qtrm =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val rtrm' = HOLogic.dest_Trueprop rtrm
+ val qtrm' = HOLogic.dest_Trueprop qtrm
+ val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
+ handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
+ val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
+ handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
+ in
+ Drule.instantiate' []
+ [SOME (cterm_of thy reg_goal),
+ NONE,
+ SOME (cterm_of thy inj_goal)] partiality_procedure_thm
+ end
+
+
+fun partiality_descend_procedure_tac ctxt simps =
+ let
+ val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
+ in
+ full_simp_tac ss
+ THEN' Object_Logic.full_atomize_tac
+ THEN' gen_frees_tac ctxt
+ THEN' SUBGOAL (fn (goal, i) =>
+ let
+ val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
+ val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
+ val rule = partiality_procedure_inst ctxt rtrm goal
+ in
+ rtac rule i
+ end)
+ end
+
+fun partiality_descend_tac ctxt simps =
+ let
+ val mk_tac_raw =
+ partiality_descend_procedure_tac ctxt simps
+ THEN' RANGE
+ [Object_Logic.rulify_tac THEN' (K all_tac),
+ all_injection_tac ctxt,
+ clean_tac ctxt]
+ in
+ Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
+ end
+
+
+
(** lifting as a tactic **)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 08 09:10:44 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 08 09:10:54 2011 +0100
@@ -441,7 +441,7 @@
fun filter_used_facts used = filter (member (op =) used o fst)
-fun play_one_line_proof mode debug verbose timeout ths state i preferred
+fun play_one_line_proof mode debug verbose timeout pairs state i preferred
reconstrs =
let
val _ =
@@ -449,6 +449,7 @@
Output.urgent_message "Preplaying proof..."
else
()
+ val ths = pairs |> sort_wrt (fst o fst) |> map snd
fun get_preferred reconstrs =
if member (op =) reconstrs preferred then preferred
else List.last reconstrs
@@ -802,12 +803,11 @@
(used_facts,
fn () =>
let
- val used_ths =
+ val used_pairs =
facts |> map untranslated_fact |> filter_used_facts used_facts
- |> map snd
in
- play_one_line_proof mode debug verbose preplay_timeout used_ths
- state subgoal (hd reconstrs) reconstrs
+ play_one_line_proof mode debug verbose preplay_timeout
+ used_pairs state subgoal (hd reconstrs) reconstrs
end,
fn preplay =>
let
@@ -978,15 +978,15 @@
val num_facts = length facts
val facts = facts ~~ (0 upto num_facts - 1)
|> map (smt_weighted_fact ctxt num_facts)
- val {outcome, used_facts, run_time} =
+ val {outcome, used_facts = used_pairs, run_time} =
smt_filter_loop ctxt name params state subgoal smt_filter facts
- val (used_facts, used_ths) = used_facts |> ListPair.unzip
+ val used_facts = used_pairs |> map fst
val outcome = outcome |> Option.map failure_from_smt_failure
val (preplay, message, message_tail) =
case outcome of
NONE =>
(fn () =>
- play_one_line_proof mode debug verbose preplay_timeout used_ths
+ play_one_line_proof mode debug verbose preplay_timeout used_pairs
state subgoal SMT
(bunch_of_reconstructors false
(fn plain =>
@@ -1023,11 +1023,11 @@
SMT
else
raise Fail ("unknown reconstructor: " ^ quote name)
- val (used_facts, used_ths) =
- facts |> map untranslated_fact |> ListPair.unzip
+ val used_pairs = facts |> map untranslated_fact
+ val used_facts = used_pairs |> map fst
in
case play_one_line_proof (if mode = Minimize then Normal else mode) debug
- verbose timeout used_ths state subgoal reconstr
+ verbose timeout used_pairs state subgoal reconstr
[reconstr] of
play as Played (_, time) =>
{outcome = NONE, used_facts = used_facts, run_time = time,
--- a/src/Tools/Metis/README Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/README Thu Dec 08 09:10:54 2011 +0100
@@ -6,7 +6,7 @@
1. The files "Makefile" and "script/mlpp" and the directory "src/"
must reflect the corresponding files in Joe Hurd's official Metis
package. The package that was used when these notes where written
- was Metis 2.3 (31 May 2011).
+ was Metis 2.3 (release 20110926).
2. The license in each source file will probably not be something we
can use in Isabelle. The "fix_metis_license" script can be run to
@@ -19,7 +19,8 @@
Isabelle BSD license.
3. Some modifications might have to be done manually to the source
- files. The ultimate way to track them down is to use Mercurial.
+ files (but probably not). The ultimate way to track them down is
+ to use Mercurial.
4. Isabelle itself cares only about "metis.ML", which is generated
from the files in "src/" by the script "make_metis". The script
@@ -46,4 +47,4 @@
Good luck!
Jasmin Blanchette
- 8 June 2011
+ 1 December 2011
--- a/src/Tools/Metis/metis.ML Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/metis.ML Thu Dec 08 09:10:54 2011 +0100
@@ -718,7 +718,7 @@
| z l (x :: xs) (y :: ys) = z (f x y :: l) xs ys
| z _ _ _ = raise Error "zipWith: lists different lengths";
in
- fn xs => fn ys => rev (z [] xs ys)
+ fn xs => fn ys => List.rev (z [] xs ys)
end;
fun zip xs ys = zipWith pair xs ys;
@@ -726,7 +726,7 @@
local
fun inc ((x,y),(xs,ys)) = (x :: xs, y :: ys);
in
- fun unzip ab = List.foldl inc ([],[]) (rev ab);
+ fun unzip ab = List.foldl inc ([],[]) (List.rev ab);
end;
fun cartwith f =
@@ -737,15 +737,15 @@
aux xsCopy (f x y :: res) xt ys
in
fn xs => fn ys =>
- let val xs' = rev xs in aux xs' [] xs' (rev ys) end
+ let val xs' = List.rev xs in aux xs' [] xs' (List.rev ys) end
end;
fun cart xs ys = cartwith pair xs ys;
fun takeWhile p =
let
- fun f acc [] = rev acc
- | f acc (x :: xs) = if p x then f (x :: acc) xs else rev acc
+ fun f acc [] = List.rev acc
+ | f acc (x :: xs) = if p x then f (x :: acc) xs else List.rev acc
in
f []
end;
@@ -760,8 +760,8 @@
fun divideWhile p =
let
- fun f acc [] = (rev acc, [])
- | f acc (l as x :: xs) = if p x then f (x :: acc) xs else (rev acc, l)
+ fun f acc [] = (List.rev acc, [])
+ | f acc (l as x :: xs) = if p x then f (x :: acc) xs else (List.rev acc, l)
in
f []
end;
@@ -772,15 +772,15 @@
case l of
[] =>
let
- val acc = if List.null row then acc else rev row :: acc
- in
- rev acc
+ val acc = if List.null row then acc else List.rev row :: acc
+ in
+ List.rev acc
end
| h :: t =>
let
val (eor,x) = f (h,x)
in
- if eor then group (rev row :: acc) [h] x t
+ if eor then group (List.rev row :: acc) [h] x t
else group acc (h :: row) x t
end
in
@@ -831,7 +831,7 @@
fun revDivide l = revDiv [] l;
end;
-fun divide l n = let val (a,b) = revDivide l n in (rev a, b) end;
+fun divide l n = let val (a,b) = revDivide l n in (List.rev a, b) end;
fun updateNth (n,x) l =
let
@@ -860,28 +860,28 @@
local
fun inc (v,x) = if mem v x then x else v :: x;
in
- fun setify s = rev (List.foldl inc [] s);
+ fun setify s = List.rev (List.foldl inc [] s);
end;
fun union s t =
let
fun inc (v,x) = if mem v t then x else v :: x
in
- List.foldl inc t (rev s)
+ List.foldl inc t (List.rev s)
end;
fun intersect s t =
let
fun inc (v,x) = if mem v t then v :: x else x
in
- List.foldl inc [] (rev s)
+ List.foldl inc [] (List.rev s)
end;
fun difference s t =
let
fun inc (v,x) = if mem v t then x else v :: x
in
- List.foldl inc [] (rev s)
+ List.foldl inc [] (List.rev s)
end;
fun subset s t = List.all (fn x => mem x t) s;
@@ -925,13 +925,13 @@
fun sort cmp =
let
- fun findRuns acc r rs [] = rev (rev (r :: rs) :: acc)
+ fun findRuns acc r rs [] = List.rev (List.rev (r :: rs) :: acc)
| findRuns acc r rs (x :: xs) =
case cmp (r,x) of
- GREATER => findRuns (rev (r :: rs) :: acc) x [] xs
+ GREATER => findRuns (List.rev (r :: rs) :: acc) x [] xs
| _ => findRuns acc x (r :: rs) xs
- fun mergeAdj acc [] = rev acc
+ fun mergeAdj acc [] = List.rev acc
| mergeAdj acc (xs as [_]) = List.revAppend (acc,xs)
| mergeAdj acc (x :: y :: xs) = mergeAdj (merge cmp x y :: acc) xs
@@ -1072,7 +1072,7 @@
[] => []
| h :: t => if Char.isSpace h then chop t else l;
in
- val trim = String.implode o chop o rev o chop o rev o String.explode;
+ val trim = String.implode o chop o List.rev o chop o List.rev o String.explode;
end;
val join = String.concatWith;
@@ -1089,11 +1089,11 @@
let
val pat = String.explode sep
- fun div1 prev recent [] = stringify [] (rev recent :: prev)
+ fun div1 prev recent [] = stringify [] (List.rev recent :: prev)
| div1 prev recent (l as h :: t) =
case match pat l of
NONE => div1 prev (h :: recent) t
- | SOME rest => div1 (rev recent :: prev) [] rest
+ | SOME rest => div1 (List.rev recent :: prev) [] rest
in
fn s => div1 [] [] (String.explode s)
end;
@@ -1302,7 +1302,7 @@
val () = OS.FileSys.closeDir dirStrm
in
- rev filenames
+ List.rev filenames
end;
fun readTextFile {filename} =
@@ -3146,6 +3146,10 @@
type key
+val compareKey : key * key -> order
+
+val equalKey : key -> key -> bool
+
(* ------------------------------------------------------------------------- *)
(* A type of finite maps. *)
(* ------------------------------------------------------------------------- *)
@@ -5298,6 +5302,10 @@
type element
+val compareElement : element * element -> order
+
+val equalElement : element -> element -> bool
+
(* ------------------------------------------------------------------------- *)
(* A type of finite sets. *)
(* ------------------------------------------------------------------------- *)
@@ -5488,6 +5496,10 @@
type element = KM.key;
+val compareElement = KM.compareKey;
+
+val equalElement = KM.equalKey;
+
(* ------------------------------------------------------------------------- *)
(* A type of finite sets. *)
(* ------------------------------------------------------------------------- *)
@@ -6353,7 +6365,7 @@
| concatList (h :: t) = append h (fn () => concatList t);
local
- fun toLst res Nil = rev res
+ fun toLst res Nil = List.rev res
| toLst res (Cons (x, xs)) = toLst (x :: res) (xs ());
in
fun toList s = toLst [] s;
@@ -6529,41 +6541,12 @@
val escapeString : {escape : char list} -> string -> string
(* ------------------------------------------------------------------------- *)
-(* A type of strings annotated with their size. *)
-(* ------------------------------------------------------------------------- *)
-
-type stringSize = string * int
-
-val mkStringSize : string -> stringSize
-
-(* ------------------------------------------------------------------------- *)
(* A type of pretty-printers. *)
(* ------------------------------------------------------------------------- *)
-datatype breakStyle = Consistent | Inconsistent
-
-datatype step =
- BeginBlock of breakStyle * int
- | EndBlock
- | AddString of stringSize
- | AddBreak of int
- | AddNewline
-
-type ppstream = step Metis_Stream.stream
-
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printer primitives. *)
-(* ------------------------------------------------------------------------- *)
-
-val beginBlock : breakStyle -> int -> ppstream
-
-val endBlock : ppstream
-
-val addString : stringSize -> ppstream
-
-val addBreak : int -> ppstream
-
-val addNewline : ppstream
+type ppstream
+
+type 'a pp = 'a -> ppstream
val skip : ppstream
@@ -6575,28 +6558,75 @@
val stream : ppstream Metis_Stream.stream -> ppstream
-val block : breakStyle -> int -> ppstream -> ppstream
-
-val blockProgram : breakStyle -> int -> ppstream list -> ppstream
-
-(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers to generate lines. *)
-(* ------------------------------------------------------------------------- *)
-
-val execute :
- {lineLength : int} -> ppstream ->
- {indent : int, line : string} Metis_Stream.stream
+val ppPpstream : ppstream pp
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing blocks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype style = Consistent | Inconsistent
+
+datatype block =
+ Block of
+ {style : style,
+ indent : int}
+
+val styleBlock : block -> style
+
+val indentBlock : block -> int
+
+val block : block -> ppstream -> ppstream
+
+val consistentBlock : int -> ppstream list -> ppstream
+
+val inconsistentBlock : int -> ppstream list -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Words are unbreakable strings annotated with their effective size. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype word = Word of {word : string, size : int}
+
+val mkWord : string -> word
+
+val emptyWord : word
+
+val charWord : char -> word
+
+val ppWord : word pp
+
+val space : ppstream
+
+val spaces : int -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Possible line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype break = Break of {size : int, extraIndent : int}
+
+val mkBreak : int -> break
+
+val ppBreak : break pp
+
+val break : ppstream
+
+val breaks : int -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Forced line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+val newline : ppstream
+
+val newlines : int -> ppstream
(* ------------------------------------------------------------------------- *)
(* Pretty-printer combinators. *)
(* ------------------------------------------------------------------------- *)
-type 'a pp = 'a -> ppstream
-
val ppMap : ('a -> 'b) -> 'b pp -> 'a pp
-val ppString : string pp
-
val ppBracket : string -> string -> 'a pp -> 'a pp
val ppOp : string -> ppstream
@@ -6615,6 +6645,8 @@
val ppChar : char pp
+val ppString : string pp
+
val ppEscapeString : {escape : char list} -> string pp
val ppUnit : unit pp
@@ -6641,12 +6673,6 @@
val ppTriple : 'a pp -> 'b pp -> 'c pp -> ('a * 'b * 'c) pp
-val ppBreakStyle : breakStyle pp
-
-val ppStep : step pp
-
-val ppPpstream : ppstream pp
-
val ppException : exn pp
(* ------------------------------------------------------------------------- *)
@@ -6676,15 +6702,29 @@
('a * bool) pp -> ('a * bool) pp
(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers with a global line length. *)
+(* Pretty-printer rendering. *)
+(* ------------------------------------------------------------------------- *)
+
+val render :
+ {lineLength : int option} -> ppstream ->
+ {indent : int, line : string} Metis_Stream.stream
+
+val toStringWithLineLength :
+ {lineLength : int option} -> 'a pp -> 'a -> string
+
+val toStreamWithLineLength :
+ {lineLength : int option} -> 'a pp -> 'a -> string Metis_Stream.stream
+
+val toLine : 'a pp -> 'a -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer rendering with a global line length. *)
(* ------------------------------------------------------------------------- *)
val lineLength : int Unsynchronized.ref
val toString : 'a pp -> 'a -> string
-val toLine : 'a pp -> 'a -> string
-
val toStream : 'a pp -> 'a -> string Metis_Stream.stream
val trace : 'a pp -> string -> 'a -> unit
@@ -6721,7 +6761,7 @@
fun revConcat strm =
case strm of
Metis_Stream.Nil => Metis_Stream.Nil
- | Metis_Stream.Cons (h,t) => revAppend h (revConcat o t);
+ | Metis_Stream.Cons (h,t) => revAppend h (fn () => revConcat (t ()));
local
fun calcSpaces n = nChars #" " n;
@@ -6757,56 +6797,127 @@
end;
(* ------------------------------------------------------------------------- *)
-(* A type of strings annotated with their size. *)
-(* ------------------------------------------------------------------------- *)
-
-type stringSize = string * int;
-
-fun mkStringSize s = (s, size s);
-
-val emptyStringSize = mkStringSize "";
+(* Pretty-printing blocks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype style = Consistent | Inconsistent;
+
+datatype block =
+ Block of
+ {style : style,
+ indent : int};
+
+fun toStringStyle style =
+ case style of
+ Consistent => "Consistent"
+ | Inconsistent => "Inconsistent";
+
+fun isConsistentStyle style =
+ case style of
+ Consistent => true
+ | Inconsistent => false;
+
+fun isInconsistentStyle style =
+ case style of
+ Inconsistent => true
+ | Consistent => false;
+
+fun mkBlock style indent =
+ Block
+ {style = style,
+ indent = indent};
+
+val mkConsistentBlock = mkBlock Consistent;
+
+val mkInconsistentBlock = mkBlock Inconsistent;
+
+fun styleBlock (Block {style = x, ...}) = x;
+
+fun indentBlock (Block {indent = x, ...}) = x;
+
+fun isConsistentBlock block = isConsistentStyle (styleBlock block);
+
+fun isInconsistentBlock block = isInconsistentStyle (styleBlock block);
+
+(* ------------------------------------------------------------------------- *)
+(* Words are unbreakable strings annotated with their effective size. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype word = Word of {word : string, size : int};
+
+fun mkWord s = Word {word = s, size = String.size s};
+
+val emptyWord = mkWord "";
+
+fun charWord c = mkWord (str c);
+
+fun spacesWord i = Word {word = nSpaces i, size = i};
+
+fun sizeWord (Word {size = x, ...}) = x;
+
+fun renderWord (Word {word = x, ...}) = x;
+
+(* ------------------------------------------------------------------------- *)
+(* Possible line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype break = Break of {size : int, extraIndent : int};
+
+fun mkBreak n = Break {size = n, extraIndent = 0};
+
+fun sizeBreak (Break {size = x, ...}) = x;
+
+fun extraIndentBreak (Break {extraIndent = x, ...}) = x;
+
+fun renderBreak b = nSpaces (sizeBreak b);
+
+fun updateSizeBreak size break =
+ let
+ val Break {size = _, extraIndent} = break
+ in
+ Break
+ {size = size,
+ extraIndent = extraIndent}
+ end;
+
+fun appendBreak break1 break2 =
+ let
+(*BasicDebug
+ val () = warn "merging consecutive pretty-printing breaks"
+*)
+ val Break {size = size1, extraIndent = extraIndent1} = break1
+ and Break {size = size2, extraIndent = extraIndent2} = break2
+
+ val size = size1 + size2
+ and extraIndent = Int.max (extraIndent1,extraIndent2)
+ in
+ Break
+ {size = size,
+ extraIndent = extraIndent}
+ end;
(* ------------------------------------------------------------------------- *)
(* A type of pretty-printers. *)
(* ------------------------------------------------------------------------- *)
-datatype breakStyle = Consistent | Inconsistent;
-
datatype step =
- BeginBlock of breakStyle * int
+ BeginBlock of block
| EndBlock
- | AddString of stringSize
- | AddBreak of int
+ | AddWord of word
+ | AddBreak of break
| AddNewline;
type ppstream = step Metis_Stream.stream;
-fun breakStyleToString style =
- case style of
- Consistent => "Consistent"
- | Inconsistent => "Inconsistent";
-
-fun stepToString step =
+type 'a pp = 'a -> ppstream;
+
+fun toStringStep step =
case step of
BeginBlock _ => "BeginBlock"
| EndBlock => "EndBlock"
- | AddString _ => "AddString"
- | AddBreak _ => "AddBreak"
- | AddNewline => "AddNewline";
-
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printer primitives. *)
-(* ------------------------------------------------------------------------- *)
-
-fun beginBlock style indent = Metis_Stream.singleton (BeginBlock (style,indent));
-
-val endBlock = Metis_Stream.singleton EndBlock;
-
-fun addString s = Metis_Stream.singleton (AddString s);
-
-fun addBreak spaces = Metis_Stream.singleton (AddBreak spaces);
-
-val addNewline = Metis_Stream.singleton AddNewline;
+ | AddWord _ => "Word"
+ | AddBreak _ => "Break"
+ | AddNewline => "Newline";
val skip : ppstream = Metis_Stream.Nil;
@@ -6815,735 +6926,90 @@
local
fun dup pp n () = if n = 1 then pp else Metis_Stream.append pp (dup pp (n - 1));
in
- fun duplicate n pp = if n = 0 then skip else dup pp n ();
+ fun duplicate n pp : ppstream =
+ let
+(*BasicDebug
+ val () = if 0 <= n then () else raise Bug "Metis_Print.duplicate"
+*)
+ in
+ if n = 0 then skip else dup pp n ()
+ end;
end;
val program : ppstream list -> ppstream = Metis_Stream.concatList;
val stream : ppstream Metis_Stream.stream -> ppstream = Metis_Stream.concat;
-fun block style indent pp = program [beginBlock style indent, pp, endBlock];
-
-fun blockProgram style indent pps = block style indent (program pps);
-
-(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers to generate lines. *)
-(* ------------------------------------------------------------------------- *)
-
-datatype blockBreakStyle =
- InconsistentBlock
- | ConsistentBlock
- | BreakingBlock;
-
-datatype block =
- Block of
- {indent : int,
- style : blockBreakStyle,
- size : int,
- chunks : chunk list}
-
-and chunk =
- StringChunk of {size : int, string : string}
- | BreakChunk of int
- | BlockChunk of block;
-
-datatype state =
- State of
- {blocks : block list,
- lineIndent : int,
- lineSize : int};
-
-val initialIndent = 0;
-
-val initialStyle = Inconsistent;
-
-fun liftStyle style =
- case style of
- Inconsistent => InconsistentBlock
- | Consistent => ConsistentBlock;
-
-fun breakStyle style =
- case style of
- ConsistentBlock => BreakingBlock
- | _ => style;
-
-fun sizeBlock (Block {size,...}) = size;
-
-fun sizeChunk chunk =
- case chunk of
- StringChunk {size,...} => size
- | BreakChunk spaces => spaces
- | BlockChunk block => sizeBlock block;
-
-val splitChunks =
- let
- fun split _ [] = NONE
- | split acc (chunk :: chunks) =
- case chunk of
- BreakChunk _ => SOME (rev acc, chunks)
- | _ => split (chunk :: acc) chunks
- in
- split []
- end;
-
-val sizeChunks = List.foldl (fn (c,z) => sizeChunk c + z) 0;
-
-local
- fun flatten acc chunks =
- case chunks of
- [] => rev acc
- | chunk :: chunks =>
- case chunk of
- StringChunk {string = s, ...} => flatten (s :: acc) chunks
- | BreakChunk n => flatten (nSpaces n :: acc) chunks
- | BlockChunk (Block {chunks = l, ...}) =>
- flatten acc (List.revAppend (l,chunks));
-in
- fun renderChunks indent chunks =
- {indent = indent,
- line = String.concat (flatten [] (rev chunks))};
-end;
-
-fun renderChunk indent chunk = renderChunks indent [chunk];
-
-fun isEmptyBlock block =
- let
- val Block {indent = _, style = _, size, chunks} = block
-
- val empty = List.null chunks
-
-(*BasicDebug
- val _ = not empty orelse size = 0 orelse
- raise Bug "Metis_Print.isEmptyBlock: bad size"
-*)
- in
- empty
- end;
-
-(*BasicDebug
-fun checkBlock ind block =
- let
- val Block {indent, style = _, size, chunks} = block
- val _ = indent >= ind orelse raise Bug "Metis_Print.checkBlock: bad indents"
- val size' = checkChunks indent chunks
- val _ = size = size' orelse raise Bug "Metis_Print.checkBlock: wrong size"
- in
- size
- end
-
-and checkChunks ind chunks =
- case chunks of
- [] => 0
- | chunk :: chunks => checkChunk ind chunk + checkChunks ind chunks
-
-and checkChunk ind chunk =
- case chunk of
- StringChunk {size,...} => size
- | BreakChunk spaces => spaces
- | BlockChunk block => checkBlock ind block;
-
-val checkBlocks =
- let
- fun check ind blocks =
- case blocks of
- [] => 0
- | block :: blocks =>
- let
- val Block {indent,...} = block
- in
- checkBlock ind block + check indent blocks
- end
- in
- check initialIndent o rev
- end;
-*)
-
-val initialBlock =
- let
- val indent = initialIndent
- val style = liftStyle initialStyle
- val size = 0
- val chunks = []
- in
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
- end;
-
-val initialState =
- let
- val blocks = [initialBlock]
- val lineIndent = initialIndent
- val lineSize = 0
- in
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- end;
-
-(*BasicDebug
-fun checkState state =
- (let
- val State {blocks, lineIndent = _, lineSize} = state
- val lineSize' = checkBlocks blocks
- val _ = lineSize = lineSize' orelse
- raise Error "wrong lineSize"
- in
- ()
- end
- handle Error err => raise Bug err)
- handle Bug bug => raise Bug ("Metis_Print.checkState: " ^ bug);
-*)
-
-fun isFinalState state =
- let
- val State {blocks,lineIndent,lineSize} = state
- in
- case blocks of
- [] => raise Bug "Metis_Print.isFinalState: no block"
- | [block] => isEmptyBlock block
- | _ :: _ :: _ => false
- end;
-
-local
- fun renderBreak lineIndent (chunks,lines) =
- let
- val line = renderChunks lineIndent chunks
-
- val lines = line :: lines
- in
- lines
- end;
-
- fun renderBreaks lineIndent lineIndent' breaks lines =
- case rev breaks of
- [] => raise Bug "Metis_Print.renderBreaks"
- | c :: cs =>
- let
- val lines = renderBreak lineIndent (c,lines)
- in
- List.foldl (renderBreak lineIndent') lines cs
- end;
-
- fun splitAllChunks cumulatingChunks =
- let
- fun split chunks =
- case splitChunks chunks of
- SOME (prefix,chunks) => prefix :: split chunks
- | NONE => [List.concat (chunks :: cumulatingChunks)]
- in
- split
- end;
-
- fun mkBreak style cumulatingChunks chunks =
- case splitChunks chunks of
- NONE => NONE
- | SOME (chunks,broken) =>
- let
- val breaks =
- case style of
- InconsistentBlock =>
- [List.concat (broken :: cumulatingChunks)]
- | _ => splitAllChunks cumulatingChunks broken
- in
- SOME (breaks,chunks)
- end;
-
- fun naturalBreak blocks =
- case blocks of
- [] => Right ([],[])
- | block :: blocks =>
- case naturalBreak blocks of
- Left (breaks,blocks,lineIndent,lineSize) =>
- let
- val Block {size,...} = block
-
- val blocks = block :: blocks
-
- val lineSize = lineSize + size
- in
- Left (breaks,blocks,lineIndent,lineSize)
- end
- | Right (cumulatingChunks,blocks) =>
- let
- val Block {indent,style,size,chunks} = block
-
- val style = breakStyle style
- in
- case mkBreak style cumulatingChunks chunks of
- SOME (breaks,chunks) =>
- let
- val size = sizeChunks chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
-
- val lineIndent = indent
-
- val lineSize = size
- in
- Left (breaks,blocks,lineIndent,lineSize)
- end
- | NONE =>
- let
- val cumulatingChunks = chunks :: cumulatingChunks
-
- val size = 0
-
- val chunks = []
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
- in
- Right (cumulatingChunks,blocks)
- end
- end;
-
- fun forceBreakBlock cumulatingChunks block =
- let
- val Block {indent, style, size = _, chunks} = block
-
- val style = breakStyle style
-
- val break =
- case mkBreak style cumulatingChunks chunks of
- SOME (breaks,chunks) =>
- let
- val lineSize = sizeChunks chunks
- val lineIndent = indent
- in
- SOME (breaks,chunks,lineIndent,lineSize)
- end
- | NONE => forceBreakChunks cumulatingChunks chunks
- in
- case break of
- SOME (breaks,chunks,lineIndent,lineSize) =>
- let
- val size = lineSize
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
- in
- SOME (breaks,block,lineIndent,lineSize)
- end
- | NONE => NONE
- end
-
- and forceBreakChunks cumulatingChunks chunks =
- case chunks of
- [] => NONE
- | chunk :: chunks =>
- case forceBreakChunk (chunks :: cumulatingChunks) chunk of
- SOME (breaks,chunk,lineIndent,lineSize) =>
- let
- val chunks = [chunk]
- in
- SOME (breaks,chunks,lineIndent,lineSize)
- end
- | NONE =>
- case forceBreakChunks cumulatingChunks chunks of
- SOME (breaks,chunks,lineIndent,lineSize) =>
- let
- val chunks = chunk :: chunks
-
- val lineSize = lineSize + sizeChunk chunk
- in
- SOME (breaks,chunks,lineIndent,lineSize)
- end
- | NONE => NONE
-
- and forceBreakChunk cumulatingChunks chunk =
- case chunk of
- StringChunk _ => NONE
- | BreakChunk _ => raise Bug "Metis_Print.forceBreakChunk: BreakChunk"
- | BlockChunk block =>
- case forceBreakBlock cumulatingChunks block of
- SOME (breaks,block,lineIndent,lineSize) =>
- let
- val chunk = BlockChunk block
- in
- SOME (breaks,chunk,lineIndent,lineSize)
- end
- | NONE => NONE;
-
- fun forceBreak cumulatingChunks blocks' blocks =
- case blocks of
- [] => NONE
- | block :: blocks =>
- let
- val cumulatingChunks =
- case cumulatingChunks of
- [] => raise Bug "Metis_Print.forceBreak: null cumulatingChunks"
- | _ :: cumulatingChunks => cumulatingChunks
-
- val blocks' =
- case blocks' of
- [] => raise Bug "Metis_Print.forceBreak: null blocks'"
- | _ :: blocks' => blocks'
- in
- case forceBreakBlock cumulatingChunks block of
- SOME (breaks,block,lineIndent,lineSize) =>
- let
- val blocks = block :: blocks'
- in
- SOME (breaks,blocks,lineIndent,lineSize)
- end
- | NONE =>
- case forceBreak cumulatingChunks blocks' blocks of
- SOME (breaks,blocks,lineIndent,lineSize) =>
- let
- val blocks = block :: blocks
-
- val Block {size,...} = block
-
- val lineSize = lineSize + size
- in
- SOME (breaks,blocks,lineIndent,lineSize)
- end
- | NONE => NONE
- end;
-
- fun normalize lineLength lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
- in
- if lineIndent + lineSize <= lineLength then (lines,state)
- else
- let
- val break =
- case naturalBreak blocks of
- Left break => SOME break
- | Right (c,b) => forceBreak c b blocks
- in
- case break of
- SOME (breaks,blocks,lineIndent',lineSize) =>
- let
- val lines = renderBreaks lineIndent lineIndent' breaks lines
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent',
- lineSize = lineSize}
- in
- normalize lineLength lines state
- end
- | NONE => (lines,state)
- end
- end;
-
-(*BasicDebug
- val normalize = fn lineLength => fn lines => fn state =>
- let
- val () = checkState state
- in
- normalize lineLength lines state
- end
- handle Bug bug =>
- raise Bug ("Metis_Print.normalize: before normalize:\n" ^ bug)
-*)
-
- fun executeBeginBlock (style,ind) lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val Block {indent,...} =
- case blocks of
- [] => raise Bug "Metis_Print.executeBeginBlock: no block"
- | block :: _ => block
-
- val indent = indent + ind
-
- val style = liftStyle style
-
- val size = 0
-
- val chunks = []
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- (lines,state)
- end;
-
- fun executeEndBlock lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val (lineSize,blocks) =
- case blocks of
- [] => raise Bug "Metis_Print.executeEndBlock: no block"
- | topBlock :: blocks =>
- let
- val Block
- {indent = topIndent,
- style = topStyle,
- size = topSize,
- chunks = topChunks} = topBlock
- in
- case topChunks of
- [] => (lineSize,blocks)
- | headTopChunks :: tailTopChunks =>
- let
- val (lineSize,topSize,topChunks) =
- case headTopChunks of
- BreakChunk spaces =>
- let
- val lineSize = lineSize - spaces
- and topSize = topSize - spaces
- and topChunks = tailTopChunks
- in
- (lineSize,topSize,topChunks)
- end
- | _ => (lineSize,topSize,topChunks)
-
- val topBlock =
- Block
- {indent = topIndent,
- style = topStyle,
- size = topSize,
- chunks = topChunks}
- in
- case blocks of
- [] => raise Error "Metis_Print.executeEndBlock: no block"
- | block :: blocks =>
- let
- val Block {indent,style,size,chunks} = block
-
- val size = size + topSize
-
- val chunks = BlockChunk topBlock :: chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
- in
- (lineSize,blocks)
- end
- end
- end
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- (lines,state)
- end;
-
- fun executeAddString lineLength (s,n) lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val blocks =
- case blocks of
- [] => raise Bug "Metis_Print.executeAddString: no block"
- | Block {indent,style,size,chunks} :: blocks =>
- let
- val size = size + n
-
- val chunk = StringChunk {size = n, string = s}
-
- val chunks = chunk :: chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
- in
- blocks
- end
-
- val lineSize = lineSize + n
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- normalize lineLength lines state
- end;
-
- fun executeAddBreak lineLength spaces lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val (blocks,lineSize) =
- case blocks of
- [] => raise Bug "Metis_Print.executeAddBreak: no block"
- | Block {indent,style,size,chunks} :: blocks' =>
- case chunks of
- [] => (blocks,lineSize)
- | chunk :: chunks' =>
- let
- val spaces =
- case style of
- BreakingBlock => lineLength + 1
- | _ => spaces
-
- val size = size + spaces
-
- val chunks =
- case chunk of
- BreakChunk k => BreakChunk (k + spaces) :: chunks'
- | _ => BreakChunk spaces :: chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks'
-
- val lineSize = lineSize + spaces
- in
- (blocks,lineSize)
- end
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- normalize lineLength lines state
- end;
-
- fun executeBigBreak lineLength lines state =
- executeAddBreak lineLength (lineLength + 1) lines state;
-
- fun executeAddNewline lineLength lines state =
- let
- val (lines,state) =
- executeAddString lineLength emptyStringSize lines state
-
- val (lines,state) =
- executeBigBreak lineLength lines state
- in
- executeAddString lineLength emptyStringSize lines state
- end;
-
- fun final lineLength lines state =
- let
- val lines =
- if isFinalState state then lines
- else
- let
- val (lines,state) = executeBigBreak lineLength lines state
-
-(*BasicDebug
- val _ = isFinalState state orelse raise Bug "Metis_Print.final"
-*)
- in
- lines
- end
- in
- if List.null lines then Metis_Stream.Nil else Metis_Stream.singleton lines
- end;
-in
- fun execute {lineLength} =
- let
- fun advance step state =
- let
- val lines = []
- in
- case step of
- BeginBlock style_ind => executeBeginBlock style_ind lines state
- | EndBlock => executeEndBlock lines state
- | AddString s => executeAddString lineLength s lines state
- | AddBreak spaces => executeAddBreak lineLength spaces lines state
- | AddNewline => executeAddNewline lineLength lines state
- end
-
-(*BasicDebug
- val advance = fn step => fn state =>
- let
- val (lines,state) = advance step state
- val () = checkState state
- in
- (lines,state)
- end
- handle Bug bug =>
- raise Bug ("Metis_Print.advance: after " ^ stepToString step ^
- " command:\n" ^ bug)
-*)
- in
- revConcat o Metis_Stream.maps advance (final lineLength []) initialState
- end;
-end;
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing blocks. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun beginBlock b = Metis_Stream.singleton (BeginBlock b);
+
+ val endBlock = Metis_Stream.singleton EndBlock;
+in
+ fun block b pp = program [beginBlock b, pp, endBlock];
+end;
+
+fun consistentBlock i pps = block (mkConsistentBlock i) (program pps);
+
+fun inconsistentBlock i pps = block (mkInconsistentBlock i) (program pps);
+
+(* ------------------------------------------------------------------------- *)
+(* Words are unbreakable strings annotated with their effective size. *)
+(* ------------------------------------------------------------------------- *)
+
+fun ppWord w = Metis_Stream.singleton (AddWord w);
+
+val space = ppWord (mkWord " ");
+
+fun spaces i = ppWord (spacesWord i);
+
+(* ------------------------------------------------------------------------- *)
+(* Possible line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+fun ppBreak b = Metis_Stream.singleton (AddBreak b);
+
+fun breaks i = ppBreak (mkBreak i);
+
+val break = breaks 1;
+
+(* ------------------------------------------------------------------------- *)
+(* Forced line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+val newline = Metis_Stream.singleton AddNewline;
+
+fun newlines i = duplicate i newline;
(* ------------------------------------------------------------------------- *)
(* Pretty-printer combinators. *)
(* ------------------------------------------------------------------------- *)
-type 'a pp = 'a -> ppstream;
-
fun ppMap f ppB a : ppstream = ppB (f a);
fun ppBracket' l r ppA a =
let
- val (_,n) = l
- in
- blockProgram Inconsistent n
- [addString l,
+ val n = sizeWord l
+ in
+ inconsistentBlock n
+ [ppWord l,
ppA a,
- addString r]
- end;
-
-fun ppOp' s = sequence (addString s) (addBreak 1);
+ ppWord r]
+ end;
+
+fun ppOp' w = sequence (ppWord w) break;
fun ppOp2' ab ppA ppB (a,b) =
- blockProgram Inconsistent 0
+ inconsistentBlock 0
[ppA a,
ppOp' ab,
ppB b];
fun ppOp3' ab bc ppA ppB ppC (a,b,c) =
- blockProgram Inconsistent 0
+ inconsistentBlock 0
[ppA a,
ppOp' ab,
ppB b,
@@ -7555,7 +7021,7 @@
fun ppOpA a = sequence (ppOp' s) (ppA a)
in
fn [] => skip
- | h :: t => blockProgram Inconsistent 0 (ppA h :: List.map ppOpA t)
+ | h :: t => inconsistentBlock 0 (ppA h :: List.map ppOpA t)
end;
fun ppOpStream' s ppA =
@@ -7564,30 +7030,30 @@
in
fn Metis_Stream.Nil => skip
| Metis_Stream.Cons (h,t) =>
- blockProgram Inconsistent 0
+ inconsistentBlock 0
[ppA h,
Metis_Stream.concat (Metis_Stream.map ppOpA (t ()))]
end;
-fun ppBracket l r = ppBracket' (mkStringSize l) (mkStringSize r);
-
-fun ppOp s = ppOp' (mkStringSize s);
-
-fun ppOp2 ab = ppOp2' (mkStringSize ab);
-
-fun ppOp3 ab bc = ppOp3' (mkStringSize ab) (mkStringSize bc);
-
-fun ppOpList s = ppOpList' (mkStringSize s);
-
-fun ppOpStream s = ppOpStream' (mkStringSize s);
+fun ppBracket l r = ppBracket' (mkWord l) (mkWord r);
+
+fun ppOp s = ppOp' (mkWord s);
+
+fun ppOp2 ab = ppOp2' (mkWord ab);
+
+fun ppOp3 ab bc = ppOp3' (mkWord ab) (mkWord bc);
+
+fun ppOpList s = ppOpList' (mkWord s);
+
+fun ppOpStream s = ppOpStream' (mkWord s);
(* ------------------------------------------------------------------------- *)
(* Pretty-printers for common types. *)
(* ------------------------------------------------------------------------- *)
-fun ppChar c = addString (str c, 1);
-
-fun ppString s = addString (mkStringSize s);
+fun ppChar c = ppWord (charWord c);
+
+fun ppString s = ppWord (mkWord s);
fun ppEscapeString escape = ppMap (escapeString escape) ppString;
@@ -7644,9 +7110,9 @@
end;
local
- val left = mkStringSize "["
- and right = mkStringSize "]"
- and sep = mkStringSize ",";
+ val left = mkWord "["
+ and right = mkWord "]"
+ and sep = mkWord ",";
in
fun ppList ppX xs = ppBracket' left right (ppOpList' sep ppX) xs;
@@ -7663,9 +7129,9 @@
end;
local
- val left = mkStringSize "("
- and right = mkStringSize ")"
- and sep = mkStringSize ",";
+ val left = mkWord "("
+ and right = mkWord ")"
+ and sep = mkWord ",";
in
fun ppPair ppA ppB =
ppBracket' left right (ppOp2' sep ppA ppB);
@@ -7674,42 +7140,65 @@
ppBracket' left right (ppOp3' sep sep ppA ppB ppC);
end;
-val ppBreakStyle = ppMap breakStyleToString ppString;
-
-val ppStep = ppMap stepToString ppString;
-
-val ppStringSize =
- let
- val left = mkStringSize "\""
- and right = mkStringSize "\""
- and escape = {escape = [#"\""]}
-
- val pp = ppBracket' left right (ppEscapeString escape)
- in
- fn (s,n) => if size s = n then pp s else ppPair pp ppInt (s,n)
- end;
-
-fun ppStep step =
- blockProgram Inconsistent 2
- (ppStep step ::
- (case step of
- BeginBlock style_indent =>
- [addBreak 1,
- ppPair ppBreakStyle ppInt style_indent]
- | EndBlock => []
- | AddString s =>
- [addBreak 1,
- ppStringSize s]
- | AddBreak n =>
- [addBreak 1,
- ppInt n]
- | AddNewline => []));
-
-val ppPpstream = ppStream ppStep;
-
fun ppException e = ppString (exnMessage e);
(* ------------------------------------------------------------------------- *)
+(* A type of pretty-printers. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ val ppStepType = ppMap toStringStep ppString;
+
+ val ppStyle = ppMap toStringStyle ppString;
+
+ val ppBlockInfo =
+ let
+ val sep = mkWord " "
+ in
+ fn Block {style = s, indent = i} =>
+ program [ppStyle s, ppWord sep, ppInt i]
+ end;
+
+ val ppWordInfo =
+ let
+ val left = mkWord "\""
+ and right = mkWord "\""
+ and escape = {escape = [#"\""]}
+
+ val pp = ppBracket' left right (ppEscapeString escape)
+ in
+ fn Word {word = s, size = n} =>
+ if size s = n then pp s else ppPair pp ppInt (s,n)
+ end;
+
+ val ppBreakInfo =
+ let
+ val sep = mkWord "+"
+ in
+ fn Break {size = n, extraIndent = k} =>
+ if k = 0 then ppInt n else program [ppInt n, ppWord sep, ppInt k]
+ end;
+
+ fun ppStep step =
+ inconsistentBlock 2
+ (ppStepType step ::
+ (case step of
+ BeginBlock b =>
+ [break,
+ ppBlockInfo b]
+ | EndBlock => []
+ | AddWord w =>
+ [break,
+ ppWordInfo w]
+ | AddBreak b =>
+ [break,
+ ppBreakInfo b]
+ | AddNewline => []));
+in
+ val ppPpstream = ppStream ppStep;
+end;
+
+(* ------------------------------------------------------------------------- *)
(* Pretty-printing infix operators. *)
(* ------------------------------------------------------------------------- *)
@@ -7815,13 +7304,13 @@
end
in
fn tm_t_a_b_r as (_,t,_,_,_) =>
- if isLayer t then block Inconsistent 0 (ppLayer tm_t_a_b_r)
+ if isLayer t then inconsistentBlock 0 [ppLayer tm_t_a_b_r]
else ppLower tm_t_a_b_r
end;
local
- val leftBrack = mkStringSize "("
- and rightBrack = mkStringSize ")";
+ val leftBrack = mkWord "("
+ and rightBrack = mkWord ")";
in
fun ppInfixes ops =
let
@@ -7855,37 +7344,947 @@
end;
(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers with a global line length. *)
-(* ------------------------------------------------------------------------- *)
-
-val lineLength = Unsynchronized.ref initialLineLength;
+(* A type of output lines. *)
+(* ------------------------------------------------------------------------- *)
+
+type line = {indent : int, line : string};
+
+val emptyLine =
+ let
+ val indent = 0
+ and line = ""
+ in
+ {indent = indent,
+ line = line}
+ end;
+
+fun addEmptyLine lines = emptyLine :: lines;
+
+fun addLine lines indent line = {indent = indent, line = line} :: lines;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer rendering. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype chunk =
+ WordChunk of word
+ | BreakChunk of break
+ | FrameChunk of frame
+
+and frame =
+ Frame of
+ {block : block,
+ broken : bool,
+ indent : int,
+ size : int,
+ chunks : chunk list};
+
+datatype state =
+ State of
+ {lineIndent : int,
+ lineSize : int,
+ stack : frame list};
+
+fun blockFrame (Frame {block = x, ...}) = x;
+
+fun brokenFrame (Frame {broken = x, ...}) = x;
+
+fun indentFrame (Frame {indent = x, ...}) = x;
+
+fun sizeFrame (Frame {size = x, ...}) = x;
+
+fun chunksFrame (Frame {chunks = x, ...}) = x;
+
+fun styleFrame frame = styleBlock (blockFrame frame);
+
+fun isConsistentFrame frame = isConsistentBlock (blockFrame frame);
+
+fun breakingFrame frame = isConsistentFrame frame andalso brokenFrame frame;
+
+fun sizeChunk chunk =
+ case chunk of
+ WordChunk w => sizeWord w
+ | BreakChunk b => sizeBreak b
+ | FrameChunk f => sizeFrame f;
+
+local
+ fun add (c,acc) = sizeChunk c + acc;
+in
+ fun sizeChunks cs = List.foldl add 0 cs;
+end;
+
+local
+ fun flattenChunks acc chunks =
+ case chunks of
+ [] => acc
+ | chunk :: chunks => flattenChunk acc chunk chunks
+
+ and flattenChunk acc chunk chunks =
+ case chunk of
+ WordChunk w => flattenChunks (renderWord w :: acc) chunks
+ | BreakChunk b => flattenChunks (renderBreak b :: acc) chunks
+ | FrameChunk f => flattenFrame acc f chunks
+
+ and flattenFrame acc frame chunks =
+ flattenChunks acc (chunksFrame frame @ chunks);
+in
+ fun renderChunks chunks = String.concat (flattenChunks [] chunks);
+end;
+
+fun addChunksLine lines indent chunks =
+ addLine lines indent (renderChunks chunks);
+
+local
+ fun add baseIndent ((extraIndent,chunks),lines) =
+ addChunksLine lines (baseIndent + extraIndent) chunks;
+in
+ fun addIndentChunksLines lines baseIndent indent_chunks =
+ List.foldl (add baseIndent) lines indent_chunks;
+end;
+
+fun isEmptyFrame frame =
+ let
+ val chunks = chunksFrame frame
+
+ val empty = List.null chunks
+
+(*BasicDebug
+ val () =
+ if not empty orelse sizeFrame frame = 0 then ()
+ else raise Bug "Metis_Print.isEmptyFrame: bad size"
+*)
+ in
+ empty
+ end;
+
+local
+ fun breakInconsistent blockIndent =
+ let
+ fun break chunks =
+ case chunks of
+ [] => NONE
+ | chunk :: chunks =>
+ case chunk of
+ BreakChunk b =>
+ let
+ val pre = chunks
+ and indent = blockIndent + extraIndentBreak b
+ and post = []
+ in
+ SOME (pre,indent,post)
+ end
+ | _ =>
+ case break chunks of
+ SOME (pre,indent,post) =>
+ let
+ val post = chunk :: post
+ in
+ SOME (pre,indent,post)
+ end
+ | NONE => NONE
+ in
+ break
+ end;
+
+ fun breakConsistent blockIndent =
+ let
+ fun break indent_chunks chunks =
+ case breakInconsistent blockIndent chunks of
+ NONE => (chunks,indent_chunks)
+ | SOME (pre,indent,post) =>
+ break ((indent,post) :: indent_chunks) pre
+ in
+ break []
+ end;
+in
+ fun breakFrame frame =
+ let
+ val Frame
+ {block,
+ broken = _,
+ indent = _,
+ size = _,
+ chunks} = frame
+
+ val blockIndent = indentBlock block
+ in
+ case breakInconsistent blockIndent chunks of
+ NONE => NONE
+ | SOME (pre,indent,post) =>
+ let
+ val broken = true
+ and size = sizeChunks post
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = post}
+ in
+ case styleBlock block of
+ Inconsistent =>
+ let
+ val indent_chunks = []
+ in
+ SOME (pre,indent_chunks,frame)
+ end
+ | Consistent =>
+ let
+ val (pre,indent_chunks) = breakConsistent blockIndent pre
+ in
+ SOME (pre,indent_chunks,frame)
+ end
+ end
+ end;
+end;
+
+fun removeChunksFrame frame =
+ let
+ val Frame
+ {block,
+ broken,
+ indent,
+ size = _,
+ chunks} = frame
+ in
+ if broken andalso List.null chunks then NONE
+ else
+ let
+ val frame =
+ Frame
+ {block = block,
+ broken = true,
+ indent = indent,
+ size = 0,
+ chunks = []}
+ in
+ SOME (chunks,frame)
+ end
+ end;
+
+val removeChunksFrames =
+ let
+ fun remove frames =
+ case frames of
+ [] =>
+ let
+ val chunks = []
+ and frames = NONE
+ and indent = 0
+ in
+ (chunks,frames,indent)
+ end
+ | top :: rest =>
+ let
+ val (chunks,rest',indent) = remove rest
+
+ val indent = indent + indentFrame top
+
+ val (chunks,top') =
+ case removeChunksFrame top of
+ NONE => (chunks,NONE)
+ | SOME (topChunks,top) => (topChunks @ chunks, SOME top)
+
+ val frames' =
+ case (top',rest') of
+ (NONE,NONE) => NONE
+ | (SOME top, NONE) => SOME (top :: rest)
+ | (NONE, SOME rest) => SOME (top :: rest)
+ | (SOME top, SOME rest) => SOME (top :: rest)
+ in
+ (chunks,frames',indent)
+ end
+ in
+ fn frames =>
+ let
+ val (chunks,frames',indent) = remove frames
+
+ val frames = Option.getOpt (frames',frames)
+ in
+ (chunks,frames,indent)
+ end
+ end;
+
+local
+ fun breakUp lines lineIndent frames =
+ case frames of
+ [] => NONE
+ | frame :: frames =>
+ case breakUp lines lineIndent frames of
+ SOME (lines_indent,lineSize,frames) =>
+ let
+ val lineSize = lineSize + sizeFrame frame
+ and frames = frame :: frames
+ in
+ SOME (lines_indent,lineSize,frames)
+ end
+ | NONE =>
+ case breakFrame frame of
+ NONE => NONE
+ | SOME (frameChunks,indent_chunks,frame) =>
+ let
+ val (chunks,frames,indent) = removeChunksFrames frames
+
+ val chunks = frameChunks @ chunks
+
+ val lines = addChunksLine lines lineIndent chunks
+
+ val lines = addIndentChunksLines lines indent indent_chunks
+
+ val lineIndent = indent + indentFrame frame
+
+ val lineSize = sizeFrame frame
+
+ val frames = frame :: frames
+ in
+ SOME ((lines,lineIndent),lineSize,frames)
+ end;
+
+ fun breakInsideChunk chunk =
+ case chunk of
+ WordChunk _ => NONE
+ | BreakChunk _ => raise Bug "Metis_Print.breakInsideChunk"
+ | FrameChunk frame =>
+ case breakFrame frame of
+ SOME (pathChunks,indent_chunks,frame) =>
+ let
+ val pathIndent = 0
+ and breakIndent = indentFrame frame
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame)
+ end
+ | NONE => breakInsideFrame frame
+
+ and breakInsideChunks chunks =
+ case chunks of
+ [] => NONE
+ | chunk :: chunks =>
+ case breakInsideChunk chunk of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) =>
+ let
+ val pathChunks = pathChunks @ chunks
+ and chunks = [FrameChunk frame]
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks)
+ end
+ | NONE =>
+ case breakInsideChunks chunks of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) =>
+ let
+ val chunks = chunk :: chunks
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks)
+ end
+ | NONE => NONE
+
+ and breakInsideFrame frame =
+ let
+ val Frame
+ {block,
+ broken = _,
+ indent,
+ size = _,
+ chunks} = frame
+ in
+ case breakInsideChunks chunks of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) =>
+ let
+ val pathIndent = pathIndent + indent
+ and broken = true
+ and size = sizeChunks chunks
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame)
+ end
+ | NONE => NONE
+ end;
+
+ fun breakInside lines lineIndent frames =
+ case frames of
+ [] => NONE
+ | frame :: frames =>
+ case breakInsideFrame frame of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) =>
+ let
+ val (chunks,frames,indent) = removeChunksFrames frames
+
+ val chunks = pathChunks @ chunks
+ and indent = indent + pathIndent
+
+ val lines = addChunksLine lines lineIndent chunks
+
+ val lines = addIndentChunksLines lines indent indent_chunks
+
+ val lineIndent = indent + breakIndent
+
+ val lineSize = sizeFrame frame
+
+ val frames = frame :: frames
+ in
+ SOME ((lines,lineIndent),lineSize,frames)
+ end
+ | NONE =>
+ case breakInside lines lineIndent frames of
+ SOME (lines_indent,lineSize,frames) =>
+ let
+ val lineSize = lineSize + sizeFrame frame
+ and frames = frame :: frames
+ in
+ SOME (lines_indent,lineSize,frames)
+ end
+ | NONE => NONE;
+in
+ fun breakFrames lines lineIndent frames =
+ case breakUp lines lineIndent frames of
+ SOME ((lines,lineIndent),lineSize,frames) =>
+ SOME (lines,lineIndent,lineSize,frames)
+ | NONE =>
+ case breakInside lines lineIndent frames of
+ SOME ((lines,lineIndent),lineSize,frames) =>
+ SOME (lines,lineIndent,lineSize,frames)
+ | NONE => NONE;
+end;
+
+(*BasicDebug
+fun checkChunk chunk =
+ case chunk of
+ WordChunk t => (false, sizeWord t)
+ | BreakChunk b => (false, sizeBreak b)
+ | FrameChunk b => checkFrame b
+
+and checkChunks chunks =
+ case chunks of
+ [] => (false,0)
+ | chunk :: chunks =>
+ let
+ val (bk,sz) = checkChunk chunk
+
+ val (bk',sz') = checkChunks chunks
+ in
+ (bk orelse bk', sz + sz')
+ end
+
+and checkFrame frame =
+ let
+ val Frame
+ {block = _,
+ broken,
+ indent = _,
+ size,
+ chunks} = frame
+
+ val (bk,sz) = checkChunks chunks
+
+ val () =
+ if size = sz then ()
+ else raise Bug "Metis_Print.checkFrame: wrong size"
+
+ val () =
+ if broken orelse not bk then ()
+ else raise Bug "Metis_Print.checkFrame: deep broken frame"
+ in
+ (broken,size)
+ end;
+
+fun checkFrames frames =
+ case frames of
+ [] => (true,0)
+ | frame :: frames =>
+ let
+ val (bk,sz) = checkFrame frame
+
+ val (bk',sz') = checkFrames frames
+
+ val () =
+ if bk' orelse not bk then ()
+ else raise Bug "Metis_Print.checkFrame: broken stack frame"
+ in
+ (bk, sz + sz')
+ end;
+*)
+
+(*BasicDebug
+fun checkState state =
+ (let
+ val State {lineIndent,lineSize,stack} = state
+
+ val () =
+ if not (List.null stack) then ()
+ else raise Error "no stack"
+
+ val (_,sz) = checkFrames stack
+
+ val () =
+ if lineSize = sz then ()
+ else raise Error "wrong lineSize"
+ in
+ ()
+ end
+ handle Error err => raise Bug err)
+ handle Bug bug => raise Bug ("Metis_Print.checkState: " ^ bug);
+*)
+
+fun isEmptyState state =
+ let
+ val State {lineSize,stack,...} = state
+ in
+ lineSize = 0 andalso List.all isEmptyFrame stack
+ end;
+
+fun isFinalState state =
+ let
+ val State {stack,...} = state
+ in
+ case stack of
+ [] => raise Bug "Metis_Print.isFinalState: empty stack"
+ | [frame] => isEmptyFrame frame
+ | _ :: _ :: _ => false
+ end;
+
+local
+ val initialBlock =
+ let
+ val indent = 0
+ and style = Inconsistent
+ in
+ Block
+ {indent = indent,
+ style = style}
+ end;
+
+ val initialFrame =
+ let
+ val block = initialBlock
+ and broken = false
+ and indent = 0
+ and size = 0
+ and chunks = []
+ in
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+ end;
+in
+ val initialState =
+ let
+ val lineIndent = 0
+ and lineSize = 0
+ and stack = [initialFrame]
+ in
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ end;
+end;
+
+fun normalizeState lineLength lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val within =
+ case lineLength of
+ NONE => true
+ | SOME len => lineIndent + lineSize <= len
+ in
+ if within then (lines,state)
+ else
+ case breakFrames lines lineIndent stack of
+ NONE => (lines,state)
+ | SOME (lines,lineIndent,lineSize,stack) =>
+ let
+(*BasicDebug
+ val () = checkState state
+*)
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ normalizeState lineLength lines state
+ end
+ end
+(*BasicDebug
+ handle Bug bug => raise Bug ("Metis_Print.normalizeState:\n" ^ bug)
+*)
+
+local
+ fun executeBeginBlock block lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val broken = false
+ and indent = indentBlock block
+ and size = 0
+ and chunks = []
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+
+ val stack = frame :: stack
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ (lines,state)
+ end;
+
+ fun executeEndBlock lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val (lineSize,stack) =
+ case stack of
+ [] => raise Bug "Metis_Print.executeEndBlock: empty stack"
+ | topFrame :: stack =>
+ let
+ val Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks} = topFrame
+
+ val (lineSize,topSize,topChunks,topFrame) =
+ case topChunks of
+ BreakChunk break :: chunks =>
+ let
+(*BasicDebug
+ val () =
+ let
+ val mesg =
+ "ignoring a break at the end of a " ^
+ "pretty-printing block"
+ in
+ warn mesg
+ end
+*)
+ val n = sizeBreak break
+
+ val lineSize = lineSize - n
+ and topSize = topSize - n
+ and topChunks = chunks
+
+ val topFrame =
+ Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks}
+ in
+ (lineSize,topSize,topChunks,topFrame)
+ end
+ | _ => (lineSize,topSize,topChunks,topFrame)
+ in
+ if List.null topChunks then (lineSize,stack)
+ else
+ case stack of
+ [] => raise Error "Metis_Print.execute: too many end blocks"
+ | frame :: stack =>
+ let
+ val Frame
+ {block,
+ broken,
+ indent,
+ size,
+ chunks} = frame
+
+ val size = size + topSize
+
+ val chunk = FrameChunk topFrame
+
+ val chunks = chunk :: chunks
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+
+ val stack = frame :: stack
+ in
+ (lineSize,stack)
+ end
+ end
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ (lines,state)
+ end;
+
+ fun executeAddWord lineLength word lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val n = sizeWord word
+
+ val lineSize = lineSize + n
+
+ val stack =
+ case stack of
+ [] => raise Bug "Metis_Print.executeAddWord: empty stack"
+ | frame :: stack =>
+ let
+ val Frame
+ {block,
+ broken,
+ indent,
+ size,
+ chunks} = frame
+
+ val size = size + n
+
+ val chunk = WordChunk word
+
+ val chunks = chunk :: chunks
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+
+ val stack = frame :: stack
+ in
+ stack
+ end
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ normalizeState lineLength lines state
+ end;
+
+ fun executeAddBreak lineLength break lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val (topFrame,restFrames) =
+ case stack of
+ [] => raise Bug "Metis_Print.executeAddBreak: empty stack"
+ | topFrame :: restFrames => (topFrame,restFrames)
+
+ val Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks} = topFrame
+ in
+ case topChunks of
+ [] => (lines,state)
+ | topChunk :: restTopChunks =>
+ let
+ val (topChunks,n) =
+ case topChunk of
+ BreakChunk break' =>
+ let
+ val break = appendBreak break' break
+
+ val chunk = BreakChunk break
+
+ val topChunks = chunk :: restTopChunks
+ and n = sizeBreak break - sizeBreak break'
+ in
+ (topChunks,n)
+ end
+ | _ =>
+ let
+ val chunk = BreakChunk break
+
+ val topChunks = chunk :: topChunks
+ and n = sizeBreak break
+ in
+ (topChunks,n)
+ end
+
+ val lineSize = lineSize + n
+
+ val topSize = topSize + n
+
+ val topFrame =
+ Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks}
+
+ val stack = topFrame :: restFrames
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+
+ val lineLength =
+ if breakingFrame topFrame then SOME ~1 else lineLength
+ in
+ normalizeState lineLength lines state
+ end
+ end;
+
+ fun executeBigBreak lines state =
+ let
+ val lineLength = SOME ~1
+ and break = mkBreak 0
+ in
+ executeAddBreak lineLength break lines state
+ end;
+
+ fun executeAddNewline lineLength lines state =
+ if isEmptyState state then (addEmptyLine lines, state)
+ else executeBigBreak lines state;
+
+ fun executeEof lineLength lines state =
+ if isFinalState state then (lines,state)
+ else
+ let
+ val (lines,state) = executeBigBreak lines state
+
+(*BasicDebug
+ val () =
+ if isFinalState state then ()
+ else raise Bug "Metis_Print.executeEof: not a final state"
+*)
+ in
+ (lines,state)
+ end;
+in
+ fun render {lineLength} =
+ let
+ fun execute step state =
+ let
+ val lines = []
+ in
+ case step of
+ BeginBlock block => executeBeginBlock block lines state
+ | EndBlock => executeEndBlock lines state
+ | AddWord word => executeAddWord lineLength word lines state
+ | AddBreak break => executeAddBreak lineLength break lines state
+ | AddNewline => executeAddNewline lineLength lines state
+ end
+
+(*BasicDebug
+ val execute = fn step => fn state =>
+ let
+ val (lines,state) = execute step state
+
+ val () = checkState state
+ in
+ (lines,state)
+ end
+ handle Bug bug =>
+ raise Bug ("Metis_Print.execute: after " ^ toStringStep step ^
+ " command:\n" ^ bug)
+*)
+
+ fun final state =
+ let
+ val lines = []
+
+ val (lines,state) = executeEof lineLength lines state
+
+(*BasicDebug
+ val () = checkState state
+*)
+ in
+ if List.null lines then Metis_Stream.Nil else Metis_Stream.singleton lines
+ end
+(*BasicDebug
+ handle Bug bug => raise Bug ("Metis_Print.final: " ^ bug)
+*)
+ in
+ fn pps =>
+ let
+ val lines = Metis_Stream.maps execute final initialState pps
+ in
+ revConcat lines
+ end
+ end;
+end;
local
fun inc {indent,line} acc = line :: nSpaces indent :: acc;
fun incn (indent_line,acc) = inc indent_line ("\n" :: acc);
in
- fun toLines len ppA a =
- case execute {lineLength = len} (ppA a) of
+ fun toStringWithLineLength len ppA a =
+ case render len (ppA a) of
Metis_Stream.Nil => ""
| Metis_Stream.Cons (h,t) =>
let
val lines = Metis_Stream.foldl incn (inc h []) (t ())
in
- String.concat (rev lines)
+ String.concat (List.rev lines)
end;
end;
-fun toString ppA a = toLines (!lineLength) ppA a;
-
-fun toLine ppA a = toLines 100000 ppA a;
+local
+ fun renderLine {indent,line} = nSpaces indent ^ line ^ "\n";
+in
+ fun toStreamWithLineLength len ppA a =
+ Metis_Stream.map renderLine (render len (ppA a));
+end;
+
+fun toLine ppA a = toStringWithLineLength {lineLength = NONE} ppA a;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer rendering with a global line length. *)
+(* ------------------------------------------------------------------------- *)
+
+val lineLength = Unsynchronized.ref initialLineLength;
+
+fun toString ppA a =
+ let
+ val len = {lineLength = SOME (!lineLength)}
+ in
+ toStringWithLineLength len ppA a
+ end;
fun toStream ppA a =
- Metis_Stream.map (fn {indent,line} => nSpaces indent ^ line ^ "\n")
- (execute {lineLength = !lineLength} (ppA a));
-
-local
- val sep = mkStringSize " =";
+ let
+ val len = {lineLength = SOME (!lineLength)}
+ in
+ toStreamWithLineLength len ppA a
+ end;
+
+local
+ val sep = mkWord " =";
in
fun trace ppX nameX x =
Metis_Useful.trace (toString (ppOp2' sep ppString ppX) (nameX,x) ^ "\n");
@@ -8079,7 +8478,7 @@
let
fun sparser l = parser >> (fn x => x :: l)
in
- mmany sparser [] >> rev
+ mmany sparser [] >> List.rev
end;
fun atLeastOne p = (p ++ many p) >> op::;
@@ -8240,7 +8639,7 @@
| [(t,y)] => mk (t,x,y)
| _ => raise NoParse)
| Metis_Print.RightAssoc =>
- (case rev txs of
+ (case List.rev txs of
[] => x
| tx :: txs =>
let
@@ -8530,7 +8929,7 @@
(* ------------------------------------------------------------------------- *)
fun pp (n,i) =
- Metis_Print.blockProgram Metis_Print.Inconsistent 0
+ Metis_Print.inconsistentBlock 0
[Metis_Name.pp n,
Metis_Print.ppString "/",
Metis_Print.ppInt i];
@@ -8931,7 +9330,7 @@
let
fun f (n,arg) = (n :: path, arg)
- val acc = (rev path, tm) :: acc
+ val acc = (List.rev path, tm) :: acc
in
case tm of
Var _ => subtms rest acc
@@ -8960,7 +9359,7 @@
let
fun search [] = NONE
| search ((path,tm) :: rest) =
- if pred tm then SOME (rev path)
+ if pred tm then SOME (List.rev path)
else
case tm of
Var _ => search rest
@@ -9072,7 +9471,7 @@
Var _ => subtms rest acc
| Fn _ =>
let
- val acc = (rev path, tm) :: acc
+ val acc = (List.rev path, tm) :: acc
val rest = (0 :: path, t) :: rest
in
subtms rest acc
@@ -9083,7 +9482,7 @@
val (_,args) = func
- val acc = (rev path, tm) :: acc
+ val acc = (List.rev path, tm) :: acc
val rest = List.map f (enumerate args) @ rest
in
@@ -9220,7 +9619,7 @@
Metis_Print.program
[(if tok = "," then Metis_Print.skip else Metis_Print.ppString " "),
Metis_Print.ppString tok,
- Metis_Print.addBreak 1];
+ Metis_Print.break];
val iPrinter = Metis_Print.ppInfixes iOps destI iToken
@@ -9286,14 +9685,14 @@
fun functionArgument bv tm =
Metis_Print.sequence
- (Metis_Print.addBreak 1)
+ Metis_Print.break
(if isBrack tm then customBracket bv tm
else if isVar tm orelse isConst tm then basic bv tm
else bracket bv tm)
and basic bv (Var v) = varName bv v
| basic bv (Fn (f,args)) =
- Metis_Print.blockProgram Metis_Print.Inconsistent 2
+ Metis_Print.inconsistentBlock 2
(functionName bv f :: List.map (functionArgument bv) args)
and customBracket bv tm =
@@ -9312,21 +9711,21 @@
[Metis_Print.ppString q,
varName bv v,
Metis_Print.program
- (List.map (Metis_Print.sequence (Metis_Print.addBreak 1) o varName bv) vs),
+ (List.map (Metis_Print.sequence Metis_Print.break o varName bv) vs),
Metis_Print.ppString ".",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
innerQuant bv tm]
end
and quantifier bv tm =
if not (isQuant tm) then customBracket bv tm
- else Metis_Print.block Metis_Print.Inconsistent 2 (innerQuant bv tm)
+ else Metis_Print.inconsistentBlock 2 [innerQuant bv tm]
and molecule bv (tm,r) =
let
val (n,tm) = stripNeg tm
in
- Metis_Print.blockProgram Metis_Print.Inconsistent n
+ Metis_Print.inconsistentBlock n
[Metis_Print.duplicate n (Metis_Print.ppString neg),
if isI tm orelse (r andalso isQuant tm) then bracket bv tm
else quantifier bv tm]
@@ -10626,11 +11025,11 @@
(* Conjunctions *)
fun listMkConj fms =
- case rev fms of [] => True | fm :: fms => List.foldl And fm fms;
+ case List.rev fms of [] => True | fm :: fms => List.foldl And fm fms;
local
fun strip cs (And (p,q)) = strip (p :: cs) q
- | strip cs fm = rev (fm :: cs);
+ | strip cs fm = List.rev (fm :: cs);
in
fun stripConj True = []
| stripConj fm = strip [] fm;
@@ -10649,11 +11048,11 @@
(* Disjunctions *)
fun listMkDisj fms =
- case rev fms of [] => False | fm :: fms => List.foldl Or fm fms;
+ case List.rev fms of [] => False | fm :: fms => List.foldl Or fm fms;
local
fun strip cs (Or (p,q)) = strip (p :: cs) q
- | strip cs fm = rev (fm :: cs);
+ | strip cs fm = List.rev (fm :: cs);
in
fun stripDisj False = []
| stripDisj fm = strip [] fm;
@@ -10672,11 +11071,11 @@
(* Equivalences *)
fun listMkEquiv fms =
- case rev fms of [] => True | fm :: fms => List.foldl Iff fm fms;
+ case List.rev fms of [] => True | fm :: fms => List.foldl Iff fm fms;
local
fun strip cs (Iff (p,q)) = strip (p :: cs) q
- | strip cs fm = rev (fm :: cs);
+ | strip cs fm = List.rev (fm :: cs);
in
fun stripEquiv True = []
| stripEquiv fm = strip [] fm;
@@ -10706,7 +11105,7 @@
local
fun strip vs (Forall (v,b)) = strip (v :: vs) b
- | strip vs tm = (rev vs, tm);
+ | strip vs tm = (List.rev vs, tm);
in
val stripForall = strip [];
end;
@@ -10725,7 +11124,7 @@
local
fun strip vs (Exists (v,b)) = strip (v :: vs) b
- | strip vs tm = (rev vs, tm);
+ | strip vs tm = (List.rev vs, tm);
in
val stripExists = strip [];
end;
@@ -11030,7 +11429,7 @@
local
fun add_asms asms goal =
- if List.null asms then goal else Imp (listMkConj (rev asms), goal);
+ if List.null asms then goal else Imp (listMkConj (List.rev asms), goal);
fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
@@ -11810,7 +12209,7 @@
(List.map Metis_Literal.toFormula (Metis_LiteralSet.toList (clause th)));
in
fun pp th =
- Metis_Print.blockProgram Metis_Print.Inconsistent 3
+ Metis_Print.inconsistentBlock 3
[Metis_Print.ppString "|- ",
Metis_Formula.pp (toFormula th)];
end;
@@ -12015,43 +12414,43 @@
| inferenceType (Equality _) = Metis_Thm.Equality;
local
- fun ppAssume atm = Metis_Print.sequence (Metis_Print.addBreak 1) (Metis_Atom.pp atm);
+ fun ppAssume atm = Metis_Print.sequence Metis_Print.break (Metis_Atom.pp atm);
fun ppSubst ppThm (sub,thm) =
- Metis_Print.sequence (Metis_Print.addBreak 1)
- (Metis_Print.blockProgram Metis_Print.Inconsistent 1
+ Metis_Print.sequence Metis_Print.break
+ (Metis_Print.inconsistentBlock 1
[Metis_Print.ppString "{",
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Subst.pp ("sub",sub),
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_Print.ppOp2 " =" Metis_Print.ppString ppThm ("thm",thm),
Metis_Print.ppString "}"]);
fun ppResolve ppThm (res,pos,neg) =
- Metis_Print.sequence (Metis_Print.addBreak 1)
- (Metis_Print.blockProgram Metis_Print.Inconsistent 1
+ Metis_Print.sequence Metis_Print.break
+ (Metis_Print.inconsistentBlock 1
[Metis_Print.ppString "{",
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Atom.pp ("res",res),
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_Print.ppOp2 " =" Metis_Print.ppString ppThm ("pos",pos),
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_Print.ppOp2 " =" Metis_Print.ppString ppThm ("neg",neg),
Metis_Print.ppString "}"]);
- fun ppRefl tm = Metis_Print.sequence (Metis_Print.addBreak 1) (Metis_Term.pp tm);
+ fun ppRefl tm = Metis_Print.sequence Metis_Print.break (Metis_Term.pp tm);
fun ppEquality (lit,path,res) =
- Metis_Print.sequence (Metis_Print.addBreak 1)
- (Metis_Print.blockProgram Metis_Print.Inconsistent 1
+ Metis_Print.sequence Metis_Print.break
+ (Metis_Print.inconsistentBlock 1
[Metis_Print.ppString "{",
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Literal.pp ("lit",lit),
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Term.ppPath ("path",path),
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Term.pp ("res",res),
Metis_Print.ppString "}"]);
@@ -12059,21 +12458,20 @@
let
val infString = Metis_Thm.inferenceTypeToString (inferenceType inf)
in
- Metis_Print.block Metis_Print.Inconsistent 2
- (Metis_Print.sequence
- (Metis_Print.ppString infString)
- (case inf of
- Axiom cl => ppAxiom cl
- | Assume x => ppAssume x
- | Metis_Subst x => ppSubst ppThm x
- | Resolve x => ppResolve ppThm x
- | Refl x => ppRefl x
- | Equality x => ppEquality x))
+ Metis_Print.inconsistentBlock 2
+ [Metis_Print.ppString infString,
+ (case inf of
+ Axiom cl => ppAxiom cl
+ | Assume x => ppAssume x
+ | Metis_Subst x => ppSubst ppThm x
+ | Resolve x => ppResolve ppThm x
+ | Refl x => ppRefl x
+ | Equality x => ppEquality x)]
end;
fun ppAxiom cl =
Metis_Print.sequence
- (Metis_Print.addBreak 1)
+ Metis_Print.break
(Metis_Print.ppMap
Metis_LiteralSet.toList
(Metis_Print.ppBracket "{" "}" (Metis_Print.ppOpList "," Metis_Literal.pp)) cl);
@@ -12103,17 +12501,17 @@
val s = thmString n
in
Metis_Print.sequence
- (Metis_Print.blockProgram Metis_Print.Consistent (1 + size s)
+ (Metis_Print.consistentBlock (1 + size s)
[Metis_Print.ppString (s ^ " "),
Metis_Thm.pp th,
- Metis_Print.addBreak 2,
+ Metis_Print.breaks 2,
Metis_Print.ppBracket "[" "]" (ppInf (K Metis_Print.skip) ppThm) inf])
- Metis_Print.addNewline
- end
- in
- Metis_Print.blockProgram Metis_Print.Consistent 0
+ Metis_Print.newline
+ end
+ in
+ Metis_Print.consistentBlock 0
[Metis_Print.ppString "START OF PROOF",
- Metis_Print.addNewline,
+ Metis_Print.newline,
Metis_Print.program (List.map ppStep prf),
Metis_Print.ppString "END OF PROOF"]
end
@@ -12215,7 +12613,7 @@
val path = i :: path
in
if Metis_Term.equal tm s andalso Metis_Term.equal tm' t then
- SOME (rev path)
+ SOME (List.rev path)
else
case (tm,tm') of
(Metis_Term.Fn f_a, Metis_Term.Fn f_a') => sync s t path f_a f_a'
@@ -12377,7 +12775,7 @@
val () = Metis_Print.trace Metis_Print.ppInt "Metis_Proof.proof: unnecessary clauses" (Metis_LiteralSetMap.size ths)
*)
in
- rev acc
+ List.rev acc
end;
in
fun proof th =
@@ -14502,7 +14900,7 @@
fun prove acc proved ths =
case ths of
- [] => rev acc
+ [] => List.rev acc
| th :: ths' =>
if isProved proved th then prove acc proved ths'
else
@@ -14934,7 +15332,7 @@
let
val (cls,_) = List.foldl add ([],initialCnf) ths
in
- rev cls
+ List.rev cls
end;
end;
@@ -15502,12 +15900,12 @@
fun mkList tag m = List.map (mkEntry tag) (Metis_NameArityMap.toList m);
fun ppEntry (tag,source_arity,target) =
- Metis_Print.blockProgram Metis_Print.Inconsistent 2
+ Metis_Print.inconsistentBlock 2
[Metis_Print.ppString tag,
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_NameArity.pp source_arity,
Metis_Print.ppString " ->",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_Name.pp target];
in
fun ppFixedMap fixMap =
@@ -15517,9 +15915,9 @@
case mkList "function" fnMap @ mkList "relation" relMap of
[] => Metis_Print.skip
| entry :: entries =>
- Metis_Print.blockProgram Metis_Print.Consistent 0
+ Metis_Print.consistentBlock 0
(ppEntry entry ::
- List.map (Metis_Print.sequence Metis_Print.addNewline o ppEntry) entries)
+ List.map (Metis_Print.sequence Metis_Print.newline o ppEntry) entries)
end;
end;
@@ -18300,9 +18698,9 @@
Metis_Print.ppOp2 (" " ^ toStringOrientOption ort) Metis_Term.pp Metis_Term.pp x_y;
fun ppField f ppA a =
- Metis_Print.blockProgram Metis_Print.Inconsistent 2
+ Metis_Print.inconsistentBlock 2
[Metis_Print.ppString (f ^ " ="),
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppA a];
val ppKnown =
@@ -18326,21 +18724,21 @@
(Metis_Print.ppMap (Metis_IntSet.toList) (Metis_Print.ppList Metis_Print.ppInt));
in
fun pp (Metis_Rewrite {known,redexes,subterms,waiting,...}) =
- Metis_Print.blockProgram Metis_Print.Inconsistent 2
+ Metis_Print.inconsistentBlock 2
[Metis_Print.ppString "Metis_Rewrite",
- Metis_Print.addBreak 1,
- Metis_Print.blockProgram Metis_Print.Inconsistent 1
+ Metis_Print.break,
+ Metis_Print.inconsistentBlock 1
[Metis_Print.ppString "{",
ppKnown known,
(*MetisTrace5
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppRedexes redexes,
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppSubterms subterms,
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppWaiting waiting,
*)
Metis_Print.skip],
@@ -19924,9 +20322,9 @@
(*MetisDebug
local
fun ppField f ppA a =
- Metis_Print.blockProgram Metis_Print.Inconsistent 2
+ Metis_Print.inconsistentBlock 2
[Metis_Print.ppString (f ^ " ="),
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppA a];
val ppClauses =
@@ -19945,18 +20343,18 @@
Metis_Term.pp)));
in
fun pp (Metis_Active {clauses,rewrite,subterms,...}) =
- Metis_Print.blockProgram Metis_Print.Inconsistent 2
+ Metis_Print.inconsistentBlock 2
[Metis_Print.ppString "Metis_Active",
- Metis_Print.addBreak 1,
- Metis_Print.blockProgram Metis_Print.Inconsistent 1
+ Metis_Print.break,
+ Metis_Print.inconsistentBlock 1
[Metis_Print.ppString "{",
ppClauses clauses,
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppRewrite rewrite,
(*MetisTrace5
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppSubterms subterms,
*)
Metis_Print.skip],
@@ -20194,7 +20592,7 @@
val acc = Metis_LiteralSet.foldl (deduceResolution literals cl) acc lits
val acc = List.foldl (deduceParamodulationWith subterms cl) acc eqns
val acc = List.foldl (deduceParamodulationInto equations cl) acc subtms
- val acc = rev acc
+ val acc = List.rev acc
(*MetisTrace5
val () = Metis_Print.trace (Metis_Print.ppList Metis_Clause.pp) "Metis_Active.deduce: acc" acc
@@ -20442,7 +20840,7 @@
List.foldl factor_add active_subsume_acc cls
end;
- fun factor' active acc [] = (active, rev acc)
+ fun factor' active acc [] = (active, List.rev acc)
| factor' active acc cls =
let
val cls = sort_utilitywise cls
--- a/src/Tools/Metis/src/Active.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Active.sml Thu Dec 08 09:10:54 2011 +0100
@@ -320,9 +320,9 @@
(*MetisDebug
local
fun ppField f ppA a =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString (f ^ " ="),
- Print.addBreak 1,
+ Print.break,
ppA a];
val ppClauses =
@@ -341,18 +341,18 @@
Term.pp)));
in
fun pp (Active {clauses,rewrite,subterms,...}) =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString "Active",
- Print.addBreak 1,
- Print.blockProgram Print.Inconsistent 1
+ Print.break,
+ Print.inconsistentBlock 1
[Print.ppString "{",
ppClauses clauses,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppRewrite rewrite,
(*MetisTrace5
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppSubterms subterms,
*)
Print.skip],
@@ -590,7 +590,7 @@
val acc = LiteralSet.foldl (deduceResolution literals cl) acc lits
val acc = List.foldl (deduceParamodulationWith subterms cl) acc eqns
val acc = List.foldl (deduceParamodulationInto equations cl) acc subtms
- val acc = rev acc
+ val acc = List.rev acc
(*MetisTrace5
val () = Print.trace (Print.ppList Clause.pp) "Active.deduce: acc" acc
@@ -838,7 +838,7 @@
List.foldl factor_add active_subsume_acc cls
end;
- fun factor' active acc [] = (active, rev acc)
+ fun factor' active acc [] = (active, List.rev acc)
| factor' active acc cls =
let
val cls = sort_utilitywise cls
--- a/src/Tools/Metis/src/ElementSet.sig Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/ElementSet.sig Thu Dec 08 09:10:54 2011 +0100
@@ -12,6 +12,10 @@
type element
+val compareElement : element * element -> order
+
+val equalElement : element -> element -> bool
+
(* ------------------------------------------------------------------------- *)
(* A type of finite sets. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/ElementSet.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/ElementSet.sml Thu Dec 08 09:10:54 2011 +0100
@@ -16,6 +16,10 @@
type element = KM.key;
+val compareElement = KM.compareKey;
+
+val equalElement = KM.equalKey;
+
(* ------------------------------------------------------------------------- *)
(* A type of finite sets. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Formula.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Formula.sml Thu Dec 08 09:10:54 2011 +0100
@@ -145,11 +145,11 @@
(* Conjunctions *)
fun listMkConj fms =
- case rev fms of [] => True | fm :: fms => List.foldl And fm fms;
+ case List.rev fms of [] => True | fm :: fms => List.foldl And fm fms;
local
fun strip cs (And (p,q)) = strip (p :: cs) q
- | strip cs fm = rev (fm :: cs);
+ | strip cs fm = List.rev (fm :: cs);
in
fun stripConj True = []
| stripConj fm = strip [] fm;
@@ -168,11 +168,11 @@
(* Disjunctions *)
fun listMkDisj fms =
- case rev fms of [] => False | fm :: fms => List.foldl Or fm fms;
+ case List.rev fms of [] => False | fm :: fms => List.foldl Or fm fms;
local
fun strip cs (Or (p,q)) = strip (p :: cs) q
- | strip cs fm = rev (fm :: cs);
+ | strip cs fm = List.rev (fm :: cs);
in
fun stripDisj False = []
| stripDisj fm = strip [] fm;
@@ -191,11 +191,11 @@
(* Equivalences *)
fun listMkEquiv fms =
- case rev fms of [] => True | fm :: fms => List.foldl Iff fm fms;
+ case List.rev fms of [] => True | fm :: fms => List.foldl Iff fm fms;
local
fun strip cs (Iff (p,q)) = strip (p :: cs) q
- | strip cs fm = rev (fm :: cs);
+ | strip cs fm = List.rev (fm :: cs);
in
fun stripEquiv True = []
| stripEquiv fm = strip [] fm;
@@ -225,7 +225,7 @@
local
fun strip vs (Forall (v,b)) = strip (v :: vs) b
- | strip vs tm = (rev vs, tm);
+ | strip vs tm = (List.rev vs, tm);
in
val stripForall = strip [];
end;
@@ -244,7 +244,7 @@
local
fun strip vs (Exists (v,b)) = strip (v :: vs) b
- | strip vs tm = (rev vs, tm);
+ | strip vs tm = (List.rev vs, tm);
in
val stripExists = strip [];
end;
@@ -549,7 +549,7 @@
local
fun add_asms asms goal =
- if List.null asms then goal else Imp (listMkConj (rev asms), goal);
+ if List.null asms then goal else Imp (listMkConj (List.rev asms), goal);
fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
--- a/src/Tools/Metis/src/KeyMap.sig Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/KeyMap.sig Thu Dec 08 09:10:54 2011 +0100
@@ -12,6 +12,10 @@
type key
+val compareKey : key * key -> order
+
+val equalKey : key -> key -> bool
+
(* ------------------------------------------------------------------------- *)
(* A type of finite maps. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Model.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Model.sml Thu Dec 08 09:10:54 2011 +0100
@@ -271,12 +271,12 @@
fun mkList tag m = List.map (mkEntry tag) (NameArityMap.toList m);
fun ppEntry (tag,source_arity,target) =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString tag,
- Print.addBreak 1,
+ Print.break,
NameArity.pp source_arity,
Print.ppString " ->",
- Print.addBreak 1,
+ Print.break,
Name.pp target];
in
fun ppFixedMap fixMap =
@@ -286,9 +286,9 @@
case mkList "function" fnMap @ mkList "relation" relMap of
[] => Print.skip
| entry :: entries =>
- Print.blockProgram Print.Consistent 0
+ Print.consistentBlock 0
(ppEntry entry ::
- List.map (Print.sequence Print.addNewline o ppEntry) entries)
+ List.map (Print.sequence Print.newline o ppEntry) entries)
end;
end;
--- a/src/Tools/Metis/src/NameArity.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/NameArity.sml Thu Dec 08 09:10:54 2011 +0100
@@ -44,7 +44,7 @@
(* ------------------------------------------------------------------------- *)
fun pp (n,i) =
- Print.blockProgram Print.Inconsistent 0
+ Print.inconsistentBlock 0
[Name.pp n,
Print.ppString "/",
Print.ppInt i];
--- a/src/Tools/Metis/src/Normalize.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Normalize.sml Thu Dec 08 09:10:54 2011 +0100
@@ -942,7 +942,7 @@
fun prove acc proved ths =
case ths of
- [] => rev acc
+ [] => List.rev acc
| th :: ths' =>
if isProved proved th then prove acc proved ths'
else
@@ -1374,7 +1374,7 @@
let
val (cls,_) = List.foldl add ([],initialCnf) ths
in
- rev cls
+ List.rev cls
end;
end;
--- a/src/Tools/Metis/src/Options.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Options.sml Thu Dec 08 09:10:54 2011 +0100
@@ -6,8 +6,6 @@
structure Options :> Options =
struct
-infix ##
-
open Useful;
(* ------------------------------------------------------------------------- *)
@@ -227,19 +225,21 @@
val (r,f) = findOption x
val (ys,xs) = getArgs x r xs
val () = f (x,ys)
+
+ val (xys,xs) = process xs
in
- (cons (x,ys) ## I) (process xs)
+ ((x,ys) :: xys, xs)
end
in
fn l =>
- let
- val (a,b) = process l
+ let
+ val (a,b) = process l
- val a = List.foldl (fn ((x,xs),ys) => x :: xs @ ys) [] (rev a)
- in
- (a,b)
- end
- handle OptionExit x => exit allopts x
+ val a = List.foldl (fn ((x,xs),ys) => x :: xs @ ys) [] (List.rev a)
+ in
+ (a,b)
+ end
+ handle OptionExit x => exit allopts x
end;
end
--- a/src/Tools/Metis/src/Parse.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Parse.sml Thu Dec 08 09:10:54 2011 +0100
@@ -65,7 +65,7 @@
let
fun sparser l = parser >> (fn x => x :: l)
in
- mmany sparser [] >> rev
+ mmany sparser [] >> List.rev
end;
fun atLeastOne p = (p ++ many p) >> op::;
@@ -226,7 +226,7 @@
| [(t,y)] => mk (t,x,y)
| _ => raise NoParse)
| Print.RightAssoc =>
- (case rev txs of
+ (case List.rev txs of
[] => x
| tx :: txs =>
let
--- a/src/Tools/Metis/src/PortableMosml.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/PortableMosml.sml Thu Dec 08 09:10:54 2011 +0100
@@ -77,7 +77,8 @@
and implode = ()
and map = ()
and null = ()
-and print = ();
+and print = ()
+and rev = ();
*)
(* ------------------------------------------------------------------------- *)
@@ -121,7 +122,7 @@
fn [] => ""
| x :: xs =>
let
- val xs = List.foldl add [] (rev xs)
+ val xs = List.foldl add [] (List.rev xs)
in
String.concat (x :: xs)
end
--- a/src/Tools/Metis/src/Print.sig Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Print.sig Thu Dec 08 09:10:54 2011 +0100
@@ -13,41 +13,12 @@
val escapeString : {escape : char list} -> string -> string
(* ------------------------------------------------------------------------- *)
-(* A type of strings annotated with their size. *)
-(* ------------------------------------------------------------------------- *)
-
-type stringSize = string * int
-
-val mkStringSize : string -> stringSize
-
-(* ------------------------------------------------------------------------- *)
(* A type of pretty-printers. *)
(* ------------------------------------------------------------------------- *)
-datatype breakStyle = Consistent | Inconsistent
-
-datatype step =
- BeginBlock of breakStyle * int
- | EndBlock
- | AddString of stringSize
- | AddBreak of int
- | AddNewline
-
-type ppstream = step Stream.stream
+type ppstream
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printer primitives. *)
-(* ------------------------------------------------------------------------- *)
-
-val beginBlock : breakStyle -> int -> ppstream
-
-val endBlock : ppstream
-
-val addString : stringSize -> ppstream
-
-val addBreak : int -> ppstream
-
-val addNewline : ppstream
+type 'a pp = 'a -> ppstream
val skip : ppstream
@@ -59,28 +30,75 @@
val stream : ppstream Stream.stream -> ppstream
-val block : breakStyle -> int -> ppstream -> ppstream
+val ppPpstream : ppstream pp
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing blocks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype style = Consistent | Inconsistent
-val blockProgram : breakStyle -> int -> ppstream list -> ppstream
+datatype block =
+ Block of
+ {style : style,
+ indent : int}
+
+val styleBlock : block -> style
+
+val indentBlock : block -> int
+
+val block : block -> ppstream -> ppstream
+
+val consistentBlock : int -> ppstream list -> ppstream
+
+val inconsistentBlock : int -> ppstream list -> ppstream
(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers to generate lines. *)
+(* Words are unbreakable strings annotated with their effective size. *)
(* ------------------------------------------------------------------------- *)
-val execute :
- {lineLength : int} -> ppstream ->
- {indent : int, line : string} Stream.stream
+datatype word = Word of {word : string, size : int}
+
+val mkWord : string -> word
+
+val emptyWord : word
+
+val charWord : char -> word
+
+val ppWord : word pp
+
+val space : ppstream
+
+val spaces : int -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Possible line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype break = Break of {size : int, extraIndent : int}
+
+val mkBreak : int -> break
+
+val ppBreak : break pp
+
+val break : ppstream
+
+val breaks : int -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Forced line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+val newline : ppstream
+
+val newlines : int -> ppstream
(* ------------------------------------------------------------------------- *)
(* Pretty-printer combinators. *)
(* ------------------------------------------------------------------------- *)
-type 'a pp = 'a -> ppstream
-
val ppMap : ('a -> 'b) -> 'b pp -> 'a pp
-val ppString : string pp
-
val ppBracket : string -> string -> 'a pp -> 'a pp
val ppOp : string -> ppstream
@@ -99,6 +117,8 @@
val ppChar : char pp
+val ppString : string pp
+
val ppEscapeString : {escape : char list} -> string pp
val ppUnit : unit pp
@@ -125,12 +145,6 @@
val ppTriple : 'a pp -> 'b pp -> 'c pp -> ('a * 'b * 'c) pp
-val ppBreakStyle : breakStyle pp
-
-val ppStep : step pp
-
-val ppPpstream : ppstream pp
-
val ppException : exn pp
(* ------------------------------------------------------------------------- *)
@@ -160,15 +174,29 @@
('a * bool) pp -> ('a * bool) pp
(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers with a global line length. *)
+(* Pretty-printer rendering. *)
+(* ------------------------------------------------------------------------- *)
+
+val render :
+ {lineLength : int option} -> ppstream ->
+ {indent : int, line : string} Stream.stream
+
+val toStringWithLineLength :
+ {lineLength : int option} -> 'a pp -> 'a -> string
+
+val toStreamWithLineLength :
+ {lineLength : int option} -> 'a pp -> 'a -> string Stream.stream
+
+val toLine : 'a pp -> 'a -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer rendering with a global line length. *)
(* ------------------------------------------------------------------------- *)
val lineLength : int ref
val toString : 'a pp -> 'a -> string
-val toLine : 'a pp -> 'a -> string
-
val toStream : 'a pp -> 'a -> string Stream.stream
val trace : 'a pp -> string -> 'a -> unit
--- a/src/Tools/Metis/src/Print.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Print.sml Thu Dec 08 09:10:54 2011 +0100
@@ -26,7 +26,7 @@
fun revConcat strm =
case strm of
Stream.Nil => Stream.Nil
- | Stream.Cons (h,t) => revAppend h (revConcat o t);
+ | Stream.Cons (h,t) => revAppend h (fn () => revConcat (t ()));
local
fun calcSpaces n = nChars #" " n;
@@ -62,56 +62,127 @@
end;
(* ------------------------------------------------------------------------- *)
-(* A type of strings annotated with their size. *)
+(* Pretty-printing blocks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype style = Consistent | Inconsistent;
+
+datatype block =
+ Block of
+ {style : style,
+ indent : int};
+
+fun toStringStyle style =
+ case style of
+ Consistent => "Consistent"
+ | Inconsistent => "Inconsistent";
+
+fun isConsistentStyle style =
+ case style of
+ Consistent => true
+ | Inconsistent => false;
+
+fun isInconsistentStyle style =
+ case style of
+ Inconsistent => true
+ | Consistent => false;
+
+fun mkBlock style indent =
+ Block
+ {style = style,
+ indent = indent};
+
+val mkConsistentBlock = mkBlock Consistent;
+
+val mkInconsistentBlock = mkBlock Inconsistent;
+
+fun styleBlock (Block {style = x, ...}) = x;
+
+fun indentBlock (Block {indent = x, ...}) = x;
+
+fun isConsistentBlock block = isConsistentStyle (styleBlock block);
+
+fun isInconsistentBlock block = isInconsistentStyle (styleBlock block);
+
+(* ------------------------------------------------------------------------- *)
+(* Words are unbreakable strings annotated with their effective size. *)
(* ------------------------------------------------------------------------- *)
-type stringSize = string * int;
+datatype word = Word of {word : string, size : int};
+
+fun mkWord s = Word {word = s, size = String.size s};
+
+val emptyWord = mkWord "";
+
+fun charWord c = mkWord (str c);
+
+fun spacesWord i = Word {word = nSpaces i, size = i};
+
+fun sizeWord (Word {size = x, ...}) = x;
+
+fun renderWord (Word {word = x, ...}) = x;
+
+(* ------------------------------------------------------------------------- *)
+(* Possible line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype break = Break of {size : int, extraIndent : int};
+
+fun mkBreak n = Break {size = n, extraIndent = 0};
+
+fun sizeBreak (Break {size = x, ...}) = x;
+
+fun extraIndentBreak (Break {extraIndent = x, ...}) = x;
-fun mkStringSize s = (s, size s);
+fun renderBreak b = nSpaces (sizeBreak b);
+
+fun updateSizeBreak size break =
+ let
+ val Break {size = _, extraIndent} = break
+ in
+ Break
+ {size = size,
+ extraIndent = extraIndent}
+ end;
-val emptyStringSize = mkStringSize "";
+fun appendBreak break1 break2 =
+ let
+(*BasicDebug
+ val () = warn "merging consecutive pretty-printing breaks"
+*)
+ val Break {size = size1, extraIndent = extraIndent1} = break1
+ and Break {size = size2, extraIndent = extraIndent2} = break2
+
+ val size = size1 + size2
+ and extraIndent = Int.max (extraIndent1,extraIndent2)
+ in
+ Break
+ {size = size,
+ extraIndent = extraIndent}
+ end;
(* ------------------------------------------------------------------------- *)
(* A type of pretty-printers. *)
(* ------------------------------------------------------------------------- *)
-datatype breakStyle = Consistent | Inconsistent;
-
datatype step =
- BeginBlock of breakStyle * int
+ BeginBlock of block
| EndBlock
- | AddString of stringSize
- | AddBreak of int
+ | AddWord of word
+ | AddBreak of break
| AddNewline;
type ppstream = step Stream.stream;
-fun breakStyleToString style =
- case style of
- Consistent => "Consistent"
- | Inconsistent => "Inconsistent";
+type 'a pp = 'a -> ppstream;
-fun stepToString step =
+fun toStringStep step =
case step of
BeginBlock _ => "BeginBlock"
| EndBlock => "EndBlock"
- | AddString _ => "AddString"
- | AddBreak _ => "AddBreak"
- | AddNewline => "AddNewline";
-
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printer primitives. *)
-(* ------------------------------------------------------------------------- *)
-
-fun beginBlock style indent = Stream.singleton (BeginBlock (style,indent));
-
-val endBlock = Stream.singleton EndBlock;
-
-fun addString s = Stream.singleton (AddString s);
-
-fun addBreak spaces = Stream.singleton (AddBreak spaces);
-
-val addNewline = Stream.singleton AddNewline;
+ | AddWord _ => "Word"
+ | AddBreak _ => "Break"
+ | AddNewline => "Newline";
val skip : ppstream = Stream.Nil;
@@ -120,735 +191,90 @@
local
fun dup pp n () = if n = 1 then pp else Stream.append pp (dup pp (n - 1));
in
- fun duplicate n pp = if n = 0 then skip else dup pp n ();
+ fun duplicate n pp : ppstream =
+ let
+(*BasicDebug
+ val () = if 0 <= n then () else raise Bug "Print.duplicate"
+*)
+ in
+ if n = 0 then skip else dup pp n ()
+ end;
end;
val program : ppstream list -> ppstream = Stream.concatList;
val stream : ppstream Stream.stream -> ppstream = Stream.concat;
-fun block style indent pp = program [beginBlock style indent, pp, endBlock];
-
-fun blockProgram style indent pps = block style indent (program pps);
-
-(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers to generate lines. *)
(* ------------------------------------------------------------------------- *)
-
-datatype blockBreakStyle =
- InconsistentBlock
- | ConsistentBlock
- | BreakingBlock;
-
-datatype block =
- Block of
- {indent : int,
- style : blockBreakStyle,
- size : int,
- chunks : chunk list}
-
-and chunk =
- StringChunk of {size : int, string : string}
- | BreakChunk of int
- | BlockChunk of block;
-
-datatype state =
- State of
- {blocks : block list,
- lineIndent : int,
- lineSize : int};
-
-val initialIndent = 0;
-
-val initialStyle = Inconsistent;
-
-fun liftStyle style =
- case style of
- Inconsistent => InconsistentBlock
- | Consistent => ConsistentBlock;
-
-fun breakStyle style =
- case style of
- ConsistentBlock => BreakingBlock
- | _ => style;
-
-fun sizeBlock (Block {size,...}) = size;
-
-fun sizeChunk chunk =
- case chunk of
- StringChunk {size,...} => size
- | BreakChunk spaces => spaces
- | BlockChunk block => sizeBlock block;
-
-val splitChunks =
- let
- fun split _ [] = NONE
- | split acc (chunk :: chunks) =
- case chunk of
- BreakChunk _ => SOME (rev acc, chunks)
- | _ => split (chunk :: acc) chunks
- in
- split []
- end;
-
-val sizeChunks = List.foldl (fn (c,z) => sizeChunk c + z) 0;
-
-local
- fun flatten acc chunks =
- case chunks of
- [] => rev acc
- | chunk :: chunks =>
- case chunk of
- StringChunk {string = s, ...} => flatten (s :: acc) chunks
- | BreakChunk n => flatten (nSpaces n :: acc) chunks
- | BlockChunk (Block {chunks = l, ...}) =>
- flatten acc (List.revAppend (l,chunks));
-in
- fun renderChunks indent chunks =
- {indent = indent,
- line = String.concat (flatten [] (rev chunks))};
-end;
-
-fun renderChunk indent chunk = renderChunks indent [chunk];
-
-fun isEmptyBlock block =
- let
- val Block {indent = _, style = _, size, chunks} = block
-
- val empty = List.null chunks
-
-(*BasicDebug
- val _ = not empty orelse size = 0 orelse
- raise Bug "Print.isEmptyBlock: bad size"
-*)
- in
- empty
- end;
-
-(*BasicDebug
-fun checkBlock ind block =
- let
- val Block {indent, style = _, size, chunks} = block
- val _ = indent >= ind orelse raise Bug "Print.checkBlock: bad indents"
- val size' = checkChunks indent chunks
- val _ = size = size' orelse raise Bug "Print.checkBlock: wrong size"
- in
- size
- end
-
-and checkChunks ind chunks =
- case chunks of
- [] => 0
- | chunk :: chunks => checkChunk ind chunk + checkChunks ind chunks
-
-and checkChunk ind chunk =
- case chunk of
- StringChunk {size,...} => size
- | BreakChunk spaces => spaces
- | BlockChunk block => checkBlock ind block;
-
-val checkBlocks =
- let
- fun check ind blocks =
- case blocks of
- [] => 0
- | block :: blocks =>
- let
- val Block {indent,...} = block
- in
- checkBlock ind block + check indent blocks
- end
- in
- check initialIndent o rev
- end;
-*)
-
-val initialBlock =
- let
- val indent = initialIndent
- val style = liftStyle initialStyle
- val size = 0
- val chunks = []
- in
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
- end;
-
-val initialState =
- let
- val blocks = [initialBlock]
- val lineIndent = initialIndent
- val lineSize = 0
- in
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- end;
-
-(*BasicDebug
-fun checkState state =
- (let
- val State {blocks, lineIndent = _, lineSize} = state
- val lineSize' = checkBlocks blocks
- val _ = lineSize = lineSize' orelse
- raise Error "wrong lineSize"
- in
- ()
- end
- handle Error err => raise Bug err)
- handle Bug bug => raise Bug ("Print.checkState: " ^ bug);
-*)
-
-fun isFinalState state =
- let
- val State {blocks,lineIndent,lineSize} = state
- in
- case blocks of
- [] => raise Bug "Print.isFinalState: no block"
- | [block] => isEmptyBlock block
- | _ :: _ :: _ => false
- end;
+(* Pretty-printing blocks. *)
+(* ------------------------------------------------------------------------- *)
local
- fun renderBreak lineIndent (chunks,lines) =
- let
- val line = renderChunks lineIndent chunks
-
- val lines = line :: lines
- in
- lines
- end;
-
- fun renderBreaks lineIndent lineIndent' breaks lines =
- case rev breaks of
- [] => raise Bug "Print.renderBreaks"
- | c :: cs =>
- let
- val lines = renderBreak lineIndent (c,lines)
- in
- List.foldl (renderBreak lineIndent') lines cs
- end;
-
- fun splitAllChunks cumulatingChunks =
- let
- fun split chunks =
- case splitChunks chunks of
- SOME (prefix,chunks) => prefix :: split chunks
- | NONE => [List.concat (chunks :: cumulatingChunks)]
- in
- split
- end;
-
- fun mkBreak style cumulatingChunks chunks =
- case splitChunks chunks of
- NONE => NONE
- | SOME (chunks,broken) =>
- let
- val breaks =
- case style of
- InconsistentBlock =>
- [List.concat (broken :: cumulatingChunks)]
- | _ => splitAllChunks cumulatingChunks broken
- in
- SOME (breaks,chunks)
- end;
-
- fun naturalBreak blocks =
- case blocks of
- [] => Right ([],[])
- | block :: blocks =>
- case naturalBreak blocks of
- Left (breaks,blocks,lineIndent,lineSize) =>
- let
- val Block {size,...} = block
-
- val blocks = block :: blocks
+ fun beginBlock b = Stream.singleton (BeginBlock b);
- val lineSize = lineSize + size
- in
- Left (breaks,blocks,lineIndent,lineSize)
- end
- | Right (cumulatingChunks,blocks) =>
- let
- val Block {indent,style,size,chunks} = block
-
- val style = breakStyle style
- in
- case mkBreak style cumulatingChunks chunks of
- SOME (breaks,chunks) =>
- let
- val size = sizeChunks chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
-
- val lineIndent = indent
+ val endBlock = Stream.singleton EndBlock;
+in
+ fun block b pp = program [beginBlock b, pp, endBlock];
+end;
- val lineSize = size
- in
- Left (breaks,blocks,lineIndent,lineSize)
- end
- | NONE =>
- let
- val cumulatingChunks = chunks :: cumulatingChunks
-
- val size = 0
-
- val chunks = []
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
- in
- Right (cumulatingChunks,blocks)
- end
- end;
-
- fun forceBreakBlock cumulatingChunks block =
- let
- val Block {indent, style, size = _, chunks} = block
-
- val style = breakStyle style
+fun consistentBlock i pps = block (mkConsistentBlock i) (program pps);
- val break =
- case mkBreak style cumulatingChunks chunks of
- SOME (breaks,chunks) =>
- let
- val lineSize = sizeChunks chunks
- val lineIndent = indent
- in
- SOME (breaks,chunks,lineIndent,lineSize)
- end
- | NONE => forceBreakChunks cumulatingChunks chunks
- in
- case break of
- SOME (breaks,chunks,lineIndent,lineSize) =>
- let
- val size = lineSize
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
- in
- SOME (breaks,block,lineIndent,lineSize)
- end
- | NONE => NONE
- end
-
- and forceBreakChunks cumulatingChunks chunks =
- case chunks of
- [] => NONE
- | chunk :: chunks =>
- case forceBreakChunk (chunks :: cumulatingChunks) chunk of
- SOME (breaks,chunk,lineIndent,lineSize) =>
- let
- val chunks = [chunk]
- in
- SOME (breaks,chunks,lineIndent,lineSize)
- end
- | NONE =>
- case forceBreakChunks cumulatingChunks chunks of
- SOME (breaks,chunks,lineIndent,lineSize) =>
- let
- val chunks = chunk :: chunks
-
- val lineSize = lineSize + sizeChunk chunk
- in
- SOME (breaks,chunks,lineIndent,lineSize)
- end
- | NONE => NONE
-
- and forceBreakChunk cumulatingChunks chunk =
- case chunk of
- StringChunk _ => NONE
- | BreakChunk _ => raise Bug "Print.forceBreakChunk: BreakChunk"
- | BlockChunk block =>
- case forceBreakBlock cumulatingChunks block of
- SOME (breaks,block,lineIndent,lineSize) =>
- let
- val chunk = BlockChunk block
- in
- SOME (breaks,chunk,lineIndent,lineSize)
- end
- | NONE => NONE;
+fun inconsistentBlock i pps = block (mkInconsistentBlock i) (program pps);
- fun forceBreak cumulatingChunks blocks' blocks =
- case blocks of
- [] => NONE
- | block :: blocks =>
- let
- val cumulatingChunks =
- case cumulatingChunks of
- [] => raise Bug "Print.forceBreak: null cumulatingChunks"
- | _ :: cumulatingChunks => cumulatingChunks
-
- val blocks' =
- case blocks' of
- [] => raise Bug "Print.forceBreak: null blocks'"
- | _ :: blocks' => blocks'
- in
- case forceBreakBlock cumulatingChunks block of
- SOME (breaks,block,lineIndent,lineSize) =>
- let
- val blocks = block :: blocks'
- in
- SOME (breaks,blocks,lineIndent,lineSize)
- end
- | NONE =>
- case forceBreak cumulatingChunks blocks' blocks of
- SOME (breaks,blocks,lineIndent,lineSize) =>
- let
- val blocks = block :: blocks
-
- val Block {size,...} = block
-
- val lineSize = lineSize + size
- in
- SOME (breaks,blocks,lineIndent,lineSize)
- end
- | NONE => NONE
- end;
+(* ------------------------------------------------------------------------- *)
+(* Words are unbreakable strings annotated with their effective size. *)
+(* ------------------------------------------------------------------------- *)
- fun normalize lineLength lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
- in
- if lineIndent + lineSize <= lineLength then (lines,state)
- else
- let
- val break =
- case naturalBreak blocks of
- Left break => SOME break
- | Right (c,b) => forceBreak c b blocks
- in
- case break of
- SOME (breaks,blocks,lineIndent',lineSize) =>
- let
- val lines = renderBreaks lineIndent lineIndent' breaks lines
+fun ppWord w = Stream.singleton (AddWord w);
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent',
- lineSize = lineSize}
- in
- normalize lineLength lines state
- end
- | NONE => (lines,state)
- end
- end;
-
-(*BasicDebug
- val normalize = fn lineLength => fn lines => fn state =>
- let
- val () = checkState state
- in
- normalize lineLength lines state
- end
- handle Bug bug =>
- raise Bug ("Print.normalize: before normalize:\n" ^ bug)
-*)
+val space = ppWord (mkWord " ");
- fun executeBeginBlock (style,ind) lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val Block {indent,...} =
- case blocks of
- [] => raise Bug "Print.executeBeginBlock: no block"
- | block :: _ => block
-
- val indent = indent + ind
-
- val style = liftStyle style
-
- val size = 0
-
- val chunks = []
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- (lines,state)
- end;
-
- fun executeEndBlock lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
+fun spaces i = ppWord (spacesWord i);
- val (lineSize,blocks) =
- case blocks of
- [] => raise Bug "Print.executeEndBlock: no block"
- | topBlock :: blocks =>
- let
- val Block
- {indent = topIndent,
- style = topStyle,
- size = topSize,
- chunks = topChunks} = topBlock
- in
- case topChunks of
- [] => (lineSize,blocks)
- | headTopChunks :: tailTopChunks =>
- let
- val (lineSize,topSize,topChunks) =
- case headTopChunks of
- BreakChunk spaces =>
- let
- val lineSize = lineSize - spaces
- and topSize = topSize - spaces
- and topChunks = tailTopChunks
- in
- (lineSize,topSize,topChunks)
- end
- | _ => (lineSize,topSize,topChunks)
-
- val topBlock =
- Block
- {indent = topIndent,
- style = topStyle,
- size = topSize,
- chunks = topChunks}
- in
- case blocks of
- [] => raise Error "Print.executeEndBlock: no block"
- | block :: blocks =>
- let
- val Block {indent,style,size,chunks} = block
+(* ------------------------------------------------------------------------- *)
+(* Possible line breaks. *)
+(* ------------------------------------------------------------------------- *)
- val size = size + topSize
-
- val chunks = BlockChunk topBlock :: chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
- in
- (lineSize,blocks)
- end
- end
- end
+fun ppBreak b = Stream.singleton (AddBreak b);
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- (lines,state)
- end;
-
- fun executeAddString lineLength (s,n) lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val blocks =
- case blocks of
- [] => raise Bug "Print.executeAddString: no block"
- | Block {indent,style,size,chunks} :: blocks =>
- let
- val size = size + n
-
- val chunk = StringChunk {size = n, string = s}
-
- val chunks = chunk :: chunks
+fun breaks i = ppBreak (mkBreak i);
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
- in
- blocks
- end
-
- val lineSize = lineSize + n
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- normalize lineLength lines state
- end;
-
- fun executeAddBreak lineLength spaces lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val (blocks,lineSize) =
- case blocks of
- [] => raise Bug "Print.executeAddBreak: no block"
- | Block {indent,style,size,chunks} :: blocks' =>
- case chunks of
- [] => (blocks,lineSize)
- | chunk :: chunks' =>
- let
- val spaces =
- case style of
- BreakingBlock => lineLength + 1
- | _ => spaces
-
- val size = size + spaces
-
- val chunks =
- case chunk of
- BreakChunk k => BreakChunk (k + spaces) :: chunks'
- | _ => BreakChunk spaces :: chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks'
-
- val lineSize = lineSize + spaces
- in
- (blocks,lineSize)
- end
+val break = breaks 1;
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- normalize lineLength lines state
- end;
-
- fun executeBigBreak lineLength lines state =
- executeAddBreak lineLength (lineLength + 1) lines state;
-
- fun executeAddNewline lineLength lines state =
- let
- val (lines,state) =
- executeAddString lineLength emptyStringSize lines state
-
- val (lines,state) =
- executeBigBreak lineLength lines state
- in
- executeAddString lineLength emptyStringSize lines state
- end;
-
- fun final lineLength lines state =
- let
- val lines =
- if isFinalState state then lines
- else
- let
- val (lines,state) = executeBigBreak lineLength lines state
+(* ------------------------------------------------------------------------- *)
+(* Forced line breaks. *)
+(* ------------------------------------------------------------------------- *)
-(*BasicDebug
- val _ = isFinalState state orelse raise Bug "Print.final"
-*)
- in
- lines
- end
- in
- if List.null lines then Stream.Nil else Stream.singleton lines
- end;
-in
- fun execute {lineLength} =
- let
- fun advance step state =
- let
- val lines = []
- in
- case step of
- BeginBlock style_ind => executeBeginBlock style_ind lines state
- | EndBlock => executeEndBlock lines state
- | AddString s => executeAddString lineLength s lines state
- | AddBreak spaces => executeAddBreak lineLength spaces lines state
- | AddNewline => executeAddNewline lineLength lines state
- end
+val newline = Stream.singleton AddNewline;
-(*BasicDebug
- val advance = fn step => fn state =>
- let
- val (lines,state) = advance step state
- val () = checkState state
- in
- (lines,state)
- end
- handle Bug bug =>
- raise Bug ("Print.advance: after " ^ stepToString step ^
- " command:\n" ^ bug)
-*)
- in
- revConcat o Stream.maps advance (final lineLength []) initialState
- end;
-end;
+fun newlines i = duplicate i newline;
(* ------------------------------------------------------------------------- *)
(* Pretty-printer combinators. *)
(* ------------------------------------------------------------------------- *)
-type 'a pp = 'a -> ppstream;
-
fun ppMap f ppB a : ppstream = ppB (f a);
fun ppBracket' l r ppA a =
let
- val (_,n) = l
+ val n = sizeWord l
in
- blockProgram Inconsistent n
- [addString l,
+ inconsistentBlock n
+ [ppWord l,
ppA a,
- addString r]
+ ppWord r]
end;
-fun ppOp' s = sequence (addString s) (addBreak 1);
+fun ppOp' w = sequence (ppWord w) break;
fun ppOp2' ab ppA ppB (a,b) =
- blockProgram Inconsistent 0
+ inconsistentBlock 0
[ppA a,
ppOp' ab,
ppB b];
fun ppOp3' ab bc ppA ppB ppC (a,b,c) =
- blockProgram Inconsistent 0
+ inconsistentBlock 0
[ppA a,
ppOp' ab,
ppB b,
@@ -860,7 +286,7 @@
fun ppOpA a = sequence (ppOp' s) (ppA a)
in
fn [] => skip
- | h :: t => blockProgram Inconsistent 0 (ppA h :: List.map ppOpA t)
+ | h :: t => inconsistentBlock 0 (ppA h :: List.map ppOpA t)
end;
fun ppOpStream' s ppA =
@@ -869,30 +295,30 @@
in
fn Stream.Nil => skip
| Stream.Cons (h,t) =>
- blockProgram Inconsistent 0
+ inconsistentBlock 0
[ppA h,
Stream.concat (Stream.map ppOpA (t ()))]
end;
-fun ppBracket l r = ppBracket' (mkStringSize l) (mkStringSize r);
+fun ppBracket l r = ppBracket' (mkWord l) (mkWord r);
-fun ppOp s = ppOp' (mkStringSize s);
+fun ppOp s = ppOp' (mkWord s);
-fun ppOp2 ab = ppOp2' (mkStringSize ab);
+fun ppOp2 ab = ppOp2' (mkWord ab);
-fun ppOp3 ab bc = ppOp3' (mkStringSize ab) (mkStringSize bc);
+fun ppOp3 ab bc = ppOp3' (mkWord ab) (mkWord bc);
-fun ppOpList s = ppOpList' (mkStringSize s);
+fun ppOpList s = ppOpList' (mkWord s);
-fun ppOpStream s = ppOpStream' (mkStringSize s);
+fun ppOpStream s = ppOpStream' (mkWord s);
(* ------------------------------------------------------------------------- *)
(* Pretty-printers for common types. *)
(* ------------------------------------------------------------------------- *)
-fun ppChar c = addString (str c, 1);
+fun ppChar c = ppWord (charWord c);
-fun ppString s = addString (mkStringSize s);
+fun ppString s = ppWord (mkWord s);
fun ppEscapeString escape = ppMap (escapeString escape) ppString;
@@ -949,9 +375,9 @@
end;
local
- val left = mkStringSize "["
- and right = mkStringSize "]"
- and sep = mkStringSize ",";
+ val left = mkWord "["
+ and right = mkWord "]"
+ and sep = mkWord ",";
in
fun ppList ppX xs = ppBracket' left right (ppOpList' sep ppX) xs;
@@ -968,9 +394,9 @@
end;
local
- val left = mkStringSize "("
- and right = mkStringSize ")"
- and sep = mkStringSize ",";
+ val left = mkWord "("
+ and right = mkWord ")"
+ and sep = mkWord ",";
in
fun ppPair ppA ppB =
ppBracket' left right (ppOp2' sep ppA ppB);
@@ -979,40 +405,63 @@
ppBracket' left right (ppOp3' sep sep ppA ppB ppC);
end;
-val ppBreakStyle = ppMap breakStyleToString ppString;
+fun ppException e = ppString (exnMessage e);
-val ppStep = ppMap stepToString ppString;
+(* ------------------------------------------------------------------------- *)
+(* A type of pretty-printers. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ val ppStepType = ppMap toStringStep ppString;
+
+ val ppStyle = ppMap toStringStyle ppString;
-val ppStringSize =
- let
- val left = mkStringSize "\""
- and right = mkStringSize "\""
- and escape = {escape = [#"\""]}
+ val ppBlockInfo =
+ let
+ val sep = mkWord " "
+ in
+ fn Block {style = s, indent = i} =>
+ program [ppStyle s, ppWord sep, ppInt i]
+ end;
- val pp = ppBracket' left right (ppEscapeString escape)
- in
- fn (s,n) => if size s = n then pp s else ppPair pp ppInt (s,n)
- end;
+ val ppWordInfo =
+ let
+ val left = mkWord "\""
+ and right = mkWord "\""
+ and escape = {escape = [#"\""]}
-fun ppStep step =
- blockProgram Inconsistent 2
- (ppStep step ::
- (case step of
- BeginBlock style_indent =>
- [addBreak 1,
- ppPair ppBreakStyle ppInt style_indent]
- | EndBlock => []
- | AddString s =>
- [addBreak 1,
- ppStringSize s]
- | AddBreak n =>
- [addBreak 1,
- ppInt n]
- | AddNewline => []));
+ val pp = ppBracket' left right (ppEscapeString escape)
+ in
+ fn Word {word = s, size = n} =>
+ if size s = n then pp s else ppPair pp ppInt (s,n)
+ end;
+
+ val ppBreakInfo =
+ let
+ val sep = mkWord "+"
+ in
+ fn Break {size = n, extraIndent = k} =>
+ if k = 0 then ppInt n else program [ppInt n, ppWord sep, ppInt k]
+ end;
-val ppPpstream = ppStream ppStep;
-
-fun ppException e = ppString (exnMessage e);
+ fun ppStep step =
+ inconsistentBlock 2
+ (ppStepType step ::
+ (case step of
+ BeginBlock b =>
+ [break,
+ ppBlockInfo b]
+ | EndBlock => []
+ | AddWord w =>
+ [break,
+ ppWordInfo w]
+ | AddBreak b =>
+ [break,
+ ppBreakInfo b]
+ | AddNewline => []));
+in
+ val ppPpstream = ppStream ppStep;
+end;
(* ------------------------------------------------------------------------- *)
(* Pretty-printing infix operators. *)
@@ -1120,13 +569,13 @@
end
in
fn tm_t_a_b_r as (_,t,_,_,_) =>
- if isLayer t then block Inconsistent 0 (ppLayer tm_t_a_b_r)
+ if isLayer t then inconsistentBlock 0 [ppLayer tm_t_a_b_r]
else ppLower tm_t_a_b_r
end;
local
- val leftBrack = mkStringSize "("
- and rightBrack = mkStringSize ")";
+ val leftBrack = mkWord "("
+ and rightBrack = mkWord ")";
in
fun ppInfixes ops =
let
@@ -1160,37 +609,947 @@
end;
(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers with a global line length. *)
+(* A type of output lines. *)
+(* ------------------------------------------------------------------------- *)
+
+type line = {indent : int, line : string};
+
+val emptyLine =
+ let
+ val indent = 0
+ and line = ""
+ in
+ {indent = indent,
+ line = line}
+ end;
+
+fun addEmptyLine lines = emptyLine :: lines;
+
+fun addLine lines indent line = {indent = indent, line = line} :: lines;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer rendering. *)
(* ------------------------------------------------------------------------- *)
-val lineLength = ref initialLineLength;
+datatype chunk =
+ WordChunk of word
+ | BreakChunk of break
+ | FrameChunk of frame
+
+and frame =
+ Frame of
+ {block : block,
+ broken : bool,
+ indent : int,
+ size : int,
+ chunks : chunk list};
+
+datatype state =
+ State of
+ {lineIndent : int,
+ lineSize : int,
+ stack : frame list};
+
+fun blockFrame (Frame {block = x, ...}) = x;
+
+fun brokenFrame (Frame {broken = x, ...}) = x;
+
+fun indentFrame (Frame {indent = x, ...}) = x;
+
+fun sizeFrame (Frame {size = x, ...}) = x;
+
+fun chunksFrame (Frame {chunks = x, ...}) = x;
+
+fun styleFrame frame = styleBlock (blockFrame frame);
+
+fun isConsistentFrame frame = isConsistentBlock (blockFrame frame);
+
+fun breakingFrame frame = isConsistentFrame frame andalso brokenFrame frame;
+
+fun sizeChunk chunk =
+ case chunk of
+ WordChunk w => sizeWord w
+ | BreakChunk b => sizeBreak b
+ | FrameChunk f => sizeFrame f;
+
+local
+ fun add (c,acc) = sizeChunk c + acc;
+in
+ fun sizeChunks cs = List.foldl add 0 cs;
+end;
+
+local
+ fun flattenChunks acc chunks =
+ case chunks of
+ [] => acc
+ | chunk :: chunks => flattenChunk acc chunk chunks
+
+ and flattenChunk acc chunk chunks =
+ case chunk of
+ WordChunk w => flattenChunks (renderWord w :: acc) chunks
+ | BreakChunk b => flattenChunks (renderBreak b :: acc) chunks
+ | FrameChunk f => flattenFrame acc f chunks
+
+ and flattenFrame acc frame chunks =
+ flattenChunks acc (chunksFrame frame @ chunks);
+in
+ fun renderChunks chunks = String.concat (flattenChunks [] chunks);
+end;
+
+fun addChunksLine lines indent chunks =
+ addLine lines indent (renderChunks chunks);
+
+local
+ fun add baseIndent ((extraIndent,chunks),lines) =
+ addChunksLine lines (baseIndent + extraIndent) chunks;
+in
+ fun addIndentChunksLines lines baseIndent indent_chunks =
+ List.foldl (add baseIndent) lines indent_chunks;
+end;
+
+fun isEmptyFrame frame =
+ let
+ val chunks = chunksFrame frame
+
+ val empty = List.null chunks
+
+(*BasicDebug
+ val () =
+ if not empty orelse sizeFrame frame = 0 then ()
+ else raise Bug "Print.isEmptyFrame: bad size"
+*)
+ in
+ empty
+ end;
+
+local
+ fun breakInconsistent blockIndent =
+ let
+ fun break chunks =
+ case chunks of
+ [] => NONE
+ | chunk :: chunks =>
+ case chunk of
+ BreakChunk b =>
+ let
+ val pre = chunks
+ and indent = blockIndent + extraIndentBreak b
+ and post = []
+ in
+ SOME (pre,indent,post)
+ end
+ | _ =>
+ case break chunks of
+ SOME (pre,indent,post) =>
+ let
+ val post = chunk :: post
+ in
+ SOME (pre,indent,post)
+ end
+ | NONE => NONE
+ in
+ break
+ end;
+
+ fun breakConsistent blockIndent =
+ let
+ fun break indent_chunks chunks =
+ case breakInconsistent blockIndent chunks of
+ NONE => (chunks,indent_chunks)
+ | SOME (pre,indent,post) =>
+ break ((indent,post) :: indent_chunks) pre
+ in
+ break []
+ end;
+in
+ fun breakFrame frame =
+ let
+ val Frame
+ {block,
+ broken = _,
+ indent = _,
+ size = _,
+ chunks} = frame
+
+ val blockIndent = indentBlock block
+ in
+ case breakInconsistent blockIndent chunks of
+ NONE => NONE
+ | SOME (pre,indent,post) =>
+ let
+ val broken = true
+ and size = sizeChunks post
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = post}
+ in
+ case styleBlock block of
+ Inconsistent =>
+ let
+ val indent_chunks = []
+ in
+ SOME (pre,indent_chunks,frame)
+ end
+ | Consistent =>
+ let
+ val (pre,indent_chunks) = breakConsistent blockIndent pre
+ in
+ SOME (pre,indent_chunks,frame)
+ end
+ end
+ end;
+end;
+
+fun removeChunksFrame frame =
+ let
+ val Frame
+ {block,
+ broken,
+ indent,
+ size = _,
+ chunks} = frame
+ in
+ if broken andalso List.null chunks then NONE
+ else
+ let
+ val frame =
+ Frame
+ {block = block,
+ broken = true,
+ indent = indent,
+ size = 0,
+ chunks = []}
+ in
+ SOME (chunks,frame)
+ end
+ end;
+
+val removeChunksFrames =
+ let
+ fun remove frames =
+ case frames of
+ [] =>
+ let
+ val chunks = []
+ and frames = NONE
+ and indent = 0
+ in
+ (chunks,frames,indent)
+ end
+ | top :: rest =>
+ let
+ val (chunks,rest',indent) = remove rest
+
+ val indent = indent + indentFrame top
+
+ val (chunks,top') =
+ case removeChunksFrame top of
+ NONE => (chunks,NONE)
+ | SOME (topChunks,top) => (topChunks @ chunks, SOME top)
+
+ val frames' =
+ case (top',rest') of
+ (NONE,NONE) => NONE
+ | (SOME top, NONE) => SOME (top :: rest)
+ | (NONE, SOME rest) => SOME (top :: rest)
+ | (SOME top, SOME rest) => SOME (top :: rest)
+ in
+ (chunks,frames',indent)
+ end
+ in
+ fn frames =>
+ let
+ val (chunks,frames',indent) = remove frames
+
+ val frames = Option.getOpt (frames',frames)
+ in
+ (chunks,frames,indent)
+ end
+ end;
+
+local
+ fun breakUp lines lineIndent frames =
+ case frames of
+ [] => NONE
+ | frame :: frames =>
+ case breakUp lines lineIndent frames of
+ SOME (lines_indent,lineSize,frames) =>
+ let
+ val lineSize = lineSize + sizeFrame frame
+ and frames = frame :: frames
+ in
+ SOME (lines_indent,lineSize,frames)
+ end
+ | NONE =>
+ case breakFrame frame of
+ NONE => NONE
+ | SOME (frameChunks,indent_chunks,frame) =>
+ let
+ val (chunks,frames,indent) = removeChunksFrames frames
+
+ val chunks = frameChunks @ chunks
+
+ val lines = addChunksLine lines lineIndent chunks
+
+ val lines = addIndentChunksLines lines indent indent_chunks
+
+ val lineIndent = indent + indentFrame frame
+
+ val lineSize = sizeFrame frame
+
+ val frames = frame :: frames
+ in
+ SOME ((lines,lineIndent),lineSize,frames)
+ end;
+
+ fun breakInsideChunk chunk =
+ case chunk of
+ WordChunk _ => NONE
+ | BreakChunk _ => raise Bug "Print.breakInsideChunk"
+ | FrameChunk frame =>
+ case breakFrame frame of
+ SOME (pathChunks,indent_chunks,frame) =>
+ let
+ val pathIndent = 0
+ and breakIndent = indentFrame frame
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame)
+ end
+ | NONE => breakInsideFrame frame
+
+ and breakInsideChunks chunks =
+ case chunks of
+ [] => NONE
+ | chunk :: chunks =>
+ case breakInsideChunk chunk of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) =>
+ let
+ val pathChunks = pathChunks @ chunks
+ and chunks = [FrameChunk frame]
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks)
+ end
+ | NONE =>
+ case breakInsideChunks chunks of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) =>
+ let
+ val chunks = chunk :: chunks
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks)
+ end
+ | NONE => NONE
+
+ and breakInsideFrame frame =
+ let
+ val Frame
+ {block,
+ broken = _,
+ indent,
+ size = _,
+ chunks} = frame
+ in
+ case breakInsideChunks chunks of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) =>
+ let
+ val pathIndent = pathIndent + indent
+ and broken = true
+ and size = sizeChunks chunks
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame)
+ end
+ | NONE => NONE
+ end;
+
+ fun breakInside lines lineIndent frames =
+ case frames of
+ [] => NONE
+ | frame :: frames =>
+ case breakInsideFrame frame of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) =>
+ let
+ val (chunks,frames,indent) = removeChunksFrames frames
+
+ val chunks = pathChunks @ chunks
+ and indent = indent + pathIndent
+
+ val lines = addChunksLine lines lineIndent chunks
+
+ val lines = addIndentChunksLines lines indent indent_chunks
+
+ val lineIndent = indent + breakIndent
+
+ val lineSize = sizeFrame frame
+
+ val frames = frame :: frames
+ in
+ SOME ((lines,lineIndent),lineSize,frames)
+ end
+ | NONE =>
+ case breakInside lines lineIndent frames of
+ SOME (lines_indent,lineSize,frames) =>
+ let
+ val lineSize = lineSize + sizeFrame frame
+ and frames = frame :: frames
+ in
+ SOME (lines_indent,lineSize,frames)
+ end
+ | NONE => NONE;
+in
+ fun breakFrames lines lineIndent frames =
+ case breakUp lines lineIndent frames of
+ SOME ((lines,lineIndent),lineSize,frames) =>
+ SOME (lines,lineIndent,lineSize,frames)
+ | NONE =>
+ case breakInside lines lineIndent frames of
+ SOME ((lines,lineIndent),lineSize,frames) =>
+ SOME (lines,lineIndent,lineSize,frames)
+ | NONE => NONE;
+end;
+
+(*BasicDebug
+fun checkChunk chunk =
+ case chunk of
+ WordChunk t => (false, sizeWord t)
+ | BreakChunk b => (false, sizeBreak b)
+ | FrameChunk b => checkFrame b
+
+and checkChunks chunks =
+ case chunks of
+ [] => (false,0)
+ | chunk :: chunks =>
+ let
+ val (bk,sz) = checkChunk chunk
+
+ val (bk',sz') = checkChunks chunks
+ in
+ (bk orelse bk', sz + sz')
+ end
+
+and checkFrame frame =
+ let
+ val Frame
+ {block = _,
+ broken,
+ indent = _,
+ size,
+ chunks} = frame
+
+ val (bk,sz) = checkChunks chunks
+
+ val () =
+ if size = sz then ()
+ else raise Bug "Print.checkFrame: wrong size"
+
+ val () =
+ if broken orelse not bk then ()
+ else raise Bug "Print.checkFrame: deep broken frame"
+ in
+ (broken,size)
+ end;
+
+fun checkFrames frames =
+ case frames of
+ [] => (true,0)
+ | frame :: frames =>
+ let
+ val (bk,sz) = checkFrame frame
+
+ val (bk',sz') = checkFrames frames
+
+ val () =
+ if bk' orelse not bk then ()
+ else raise Bug "Print.checkFrame: broken stack frame"
+ in
+ (bk, sz + sz')
+ end;
+*)
+
+(*BasicDebug
+fun checkState state =
+ (let
+ val State {lineIndent,lineSize,stack} = state
+
+ val () =
+ if not (List.null stack) then ()
+ else raise Error "no stack"
+
+ val (_,sz) = checkFrames stack
+
+ val () =
+ if lineSize = sz then ()
+ else raise Error "wrong lineSize"
+ in
+ ()
+ end
+ handle Error err => raise Bug err)
+ handle Bug bug => raise Bug ("Print.checkState: " ^ bug);
+*)
+
+fun isEmptyState state =
+ let
+ val State {lineSize,stack,...} = state
+ in
+ lineSize = 0 andalso List.all isEmptyFrame stack
+ end;
+
+fun isFinalState state =
+ let
+ val State {stack,...} = state
+ in
+ case stack of
+ [] => raise Bug "Print.isFinalState: empty stack"
+ | [frame] => isEmptyFrame frame
+ | _ :: _ :: _ => false
+ end;
+
+local
+ val initialBlock =
+ let
+ val indent = 0
+ and style = Inconsistent
+ in
+ Block
+ {indent = indent,
+ style = style}
+ end;
+
+ val initialFrame =
+ let
+ val block = initialBlock
+ and broken = false
+ and indent = 0
+ and size = 0
+ and chunks = []
+ in
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+ end;
+in
+ val initialState =
+ let
+ val lineIndent = 0
+ and lineSize = 0
+ and stack = [initialFrame]
+ in
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ end;
+end;
+
+fun normalizeState lineLength lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val within =
+ case lineLength of
+ NONE => true
+ | SOME len => lineIndent + lineSize <= len
+ in
+ if within then (lines,state)
+ else
+ case breakFrames lines lineIndent stack of
+ NONE => (lines,state)
+ | SOME (lines,lineIndent,lineSize,stack) =>
+ let
+(*BasicDebug
+ val () = checkState state
+*)
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ normalizeState lineLength lines state
+ end
+ end
+(*BasicDebug
+ handle Bug bug => raise Bug ("Print.normalizeState:\n" ^ bug)
+*)
+
+local
+ fun executeBeginBlock block lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val broken = false
+ and indent = indentBlock block
+ and size = 0
+ and chunks = []
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+
+ val stack = frame :: stack
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ (lines,state)
+ end;
+
+ fun executeEndBlock lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val (lineSize,stack) =
+ case stack of
+ [] => raise Bug "Print.executeEndBlock: empty stack"
+ | topFrame :: stack =>
+ let
+ val Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks} = topFrame
+
+ val (lineSize,topSize,topChunks,topFrame) =
+ case topChunks of
+ BreakChunk break :: chunks =>
+ let
+(*BasicDebug
+ val () =
+ let
+ val mesg =
+ "ignoring a break at the end of a " ^
+ "pretty-printing block"
+ in
+ warn mesg
+ end
+*)
+ val n = sizeBreak break
+
+ val lineSize = lineSize - n
+ and topSize = topSize - n
+ and topChunks = chunks
+
+ val topFrame =
+ Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks}
+ in
+ (lineSize,topSize,topChunks,topFrame)
+ end
+ | _ => (lineSize,topSize,topChunks,topFrame)
+ in
+ if List.null topChunks then (lineSize,stack)
+ else
+ case stack of
+ [] => raise Error "Print.execute: too many end blocks"
+ | frame :: stack =>
+ let
+ val Frame
+ {block,
+ broken,
+ indent,
+ size,
+ chunks} = frame
+
+ val size = size + topSize
+
+ val chunk = FrameChunk topFrame
+
+ val chunks = chunk :: chunks
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+
+ val stack = frame :: stack
+ in
+ (lineSize,stack)
+ end
+ end
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ (lines,state)
+ end;
+
+ fun executeAddWord lineLength word lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val n = sizeWord word
+
+ val lineSize = lineSize + n
+
+ val stack =
+ case stack of
+ [] => raise Bug "Print.executeAddWord: empty stack"
+ | frame :: stack =>
+ let
+ val Frame
+ {block,
+ broken,
+ indent,
+ size,
+ chunks} = frame
+
+ val size = size + n
+
+ val chunk = WordChunk word
+
+ val chunks = chunk :: chunks
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+
+ val stack = frame :: stack
+ in
+ stack
+ end
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ normalizeState lineLength lines state
+ end;
+
+ fun executeAddBreak lineLength break lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val (topFrame,restFrames) =
+ case stack of
+ [] => raise Bug "Print.executeAddBreak: empty stack"
+ | topFrame :: restFrames => (topFrame,restFrames)
+
+ val Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks} = topFrame
+ in
+ case topChunks of
+ [] => (lines,state)
+ | topChunk :: restTopChunks =>
+ let
+ val (topChunks,n) =
+ case topChunk of
+ BreakChunk break' =>
+ let
+ val break = appendBreak break' break
+
+ val chunk = BreakChunk break
+
+ val topChunks = chunk :: restTopChunks
+ and n = sizeBreak break - sizeBreak break'
+ in
+ (topChunks,n)
+ end
+ | _ =>
+ let
+ val chunk = BreakChunk break
+
+ val topChunks = chunk :: topChunks
+ and n = sizeBreak break
+ in
+ (topChunks,n)
+ end
+
+ val lineSize = lineSize + n
+
+ val topSize = topSize + n
+
+ val topFrame =
+ Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks}
+
+ val stack = topFrame :: restFrames
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+
+ val lineLength =
+ if breakingFrame topFrame then SOME ~1 else lineLength
+ in
+ normalizeState lineLength lines state
+ end
+ end;
+
+ fun executeBigBreak lines state =
+ let
+ val lineLength = SOME ~1
+ and break = mkBreak 0
+ in
+ executeAddBreak lineLength break lines state
+ end;
+
+ fun executeAddNewline lineLength lines state =
+ if isEmptyState state then (addEmptyLine lines, state)
+ else executeBigBreak lines state;
+
+ fun executeEof lineLength lines state =
+ if isFinalState state then (lines,state)
+ else
+ let
+ val (lines,state) = executeBigBreak lines state
+
+(*BasicDebug
+ val () =
+ if isFinalState state then ()
+ else raise Bug "Print.executeEof: not a final state"
+*)
+ in
+ (lines,state)
+ end;
+in
+ fun render {lineLength} =
+ let
+ fun execute step state =
+ let
+ val lines = []
+ in
+ case step of
+ BeginBlock block => executeBeginBlock block lines state
+ | EndBlock => executeEndBlock lines state
+ | AddWord word => executeAddWord lineLength word lines state
+ | AddBreak break => executeAddBreak lineLength break lines state
+ | AddNewline => executeAddNewline lineLength lines state
+ end
+
+(*BasicDebug
+ val execute = fn step => fn state =>
+ let
+ val (lines,state) = execute step state
+
+ val () = checkState state
+ in
+ (lines,state)
+ end
+ handle Bug bug =>
+ raise Bug ("Print.execute: after " ^ toStringStep step ^
+ " command:\n" ^ bug)
+*)
+
+ fun final state =
+ let
+ val lines = []
+
+ val (lines,state) = executeEof lineLength lines state
+
+(*BasicDebug
+ val () = checkState state
+*)
+ in
+ if List.null lines then Stream.Nil else Stream.singleton lines
+ end
+(*BasicDebug
+ handle Bug bug => raise Bug ("Print.final: " ^ bug)
+*)
+ in
+ fn pps =>
+ let
+ val lines = Stream.maps execute final initialState pps
+ in
+ revConcat lines
+ end
+ end;
+end;
local
fun inc {indent,line} acc = line :: nSpaces indent :: acc;
fun incn (indent_line,acc) = inc indent_line ("\n" :: acc);
in
- fun toLines len ppA a =
- case execute {lineLength = len} (ppA a) of
+ fun toStringWithLineLength len ppA a =
+ case render len (ppA a) of
Stream.Nil => ""
| Stream.Cons (h,t) =>
let
val lines = Stream.foldl incn (inc h []) (t ())
in
- String.concat (rev lines)
+ String.concat (List.rev lines)
end;
end;
-fun toString ppA a = toLines (!lineLength) ppA a;
+local
+ fun renderLine {indent,line} = nSpaces indent ^ line ^ "\n";
+in
+ fun toStreamWithLineLength len ppA a =
+ Stream.map renderLine (render len (ppA a));
+end;
+
+fun toLine ppA a = toStringWithLineLength {lineLength = NONE} ppA a;
-fun toLine ppA a = toLines 100000 ppA a;
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer rendering with a global line length. *)
+(* ------------------------------------------------------------------------- *)
+
+val lineLength = ref initialLineLength;
+
+fun toString ppA a =
+ let
+ val len = {lineLength = SOME (!lineLength)}
+ in
+ toStringWithLineLength len ppA a
+ end;
fun toStream ppA a =
- Stream.map (fn {indent,line} => nSpaces indent ^ line ^ "\n")
- (execute {lineLength = !lineLength} (ppA a));
+ let
+ val len = {lineLength = SOME (!lineLength)}
+ in
+ toStreamWithLineLength len ppA a
+ end;
local
- val sep = mkStringSize " =";
+ val sep = mkWord " =";
in
fun trace ppX nameX x =
Useful.trace (toString (ppOp2' sep ppString ppX) (nameX,x) ^ "\n");
--- a/src/Tools/Metis/src/Proof.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Proof.sml Thu Dec 08 09:10:54 2011 +0100
@@ -34,43 +34,43 @@
| inferenceType (Equality _) = Thm.Equality;
local
- fun ppAssume atm = Print.sequence (Print.addBreak 1) (Atom.pp atm);
+ fun ppAssume atm = Print.sequence Print.break (Atom.pp atm);
fun ppSubst ppThm (sub,thm) =
- Print.sequence (Print.addBreak 1)
- (Print.blockProgram Print.Inconsistent 1
+ Print.sequence Print.break
+ (Print.inconsistentBlock 1
[Print.ppString "{",
Print.ppOp2 " =" Print.ppString Subst.pp ("sub",sub),
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppOp2 " =" Print.ppString ppThm ("thm",thm),
Print.ppString "}"]);
fun ppResolve ppThm (res,pos,neg) =
- Print.sequence (Print.addBreak 1)
- (Print.blockProgram Print.Inconsistent 1
+ Print.sequence Print.break
+ (Print.inconsistentBlock 1
[Print.ppString "{",
Print.ppOp2 " =" Print.ppString Atom.pp ("res",res),
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppOp2 " =" Print.ppString ppThm ("pos",pos),
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppOp2 " =" Print.ppString ppThm ("neg",neg),
Print.ppString "}"]);
- fun ppRefl tm = Print.sequence (Print.addBreak 1) (Term.pp tm);
+ fun ppRefl tm = Print.sequence Print.break (Term.pp tm);
fun ppEquality (lit,path,res) =
- Print.sequence (Print.addBreak 1)
- (Print.blockProgram Print.Inconsistent 1
+ Print.sequence Print.break
+ (Print.inconsistentBlock 1
[Print.ppString "{",
Print.ppOp2 " =" Print.ppString Literal.pp ("lit",lit),
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppOp2 " =" Print.ppString Term.ppPath ("path",path),
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppOp2 " =" Print.ppString Term.pp ("res",res),
Print.ppString "}"]);
@@ -78,21 +78,20 @@
let
val infString = Thm.inferenceTypeToString (inferenceType inf)
in
- Print.block Print.Inconsistent 2
- (Print.sequence
- (Print.ppString infString)
- (case inf of
- Axiom cl => ppAxiom cl
- | Assume x => ppAssume x
- | Subst x => ppSubst ppThm x
- | Resolve x => ppResolve ppThm x
- | Refl x => ppRefl x
- | Equality x => ppEquality x))
+ Print.inconsistentBlock 2
+ [Print.ppString infString,
+ (case inf of
+ Axiom cl => ppAxiom cl
+ | Assume x => ppAssume x
+ | Subst x => ppSubst ppThm x
+ | Resolve x => ppResolve ppThm x
+ | Refl x => ppRefl x
+ | Equality x => ppEquality x)]
end;
fun ppAxiom cl =
Print.sequence
- (Print.addBreak 1)
+ Print.break
(Print.ppMap
LiteralSet.toList
(Print.ppBracket "{" "}" (Print.ppOpList "," Literal.pp)) cl);
@@ -122,17 +121,17 @@
val s = thmString n
in
Print.sequence
- (Print.blockProgram Print.Consistent (1 + size s)
+ (Print.consistentBlock (1 + size s)
[Print.ppString (s ^ " "),
Thm.pp th,
- Print.addBreak 2,
+ Print.breaks 2,
Print.ppBracket "[" "]" (ppInf (K Print.skip) ppThm) inf])
- Print.addNewline
+ Print.newline
end
in
- Print.blockProgram Print.Consistent 0
+ Print.consistentBlock 0
[Print.ppString "START OF PROOF",
- Print.addNewline,
+ Print.newline,
Print.program (List.map ppStep prf),
Print.ppString "END OF PROOF"]
end
@@ -234,7 +233,7 @@
val path = i :: path
in
if Term.equal tm s andalso Term.equal tm' t then
- SOME (rev path)
+ SOME (List.rev path)
else
case (tm,tm') of
(Term.Fn f_a, Term.Fn f_a') => sync s t path f_a f_a'
@@ -396,7 +395,7 @@
val () = Print.trace Print.ppInt "Proof.proof: unnecessary clauses" (LiteralSetMap.size ths)
*)
in
- rev acc
+ List.rev acc
end;
in
fun proof th =
--- a/src/Tools/Metis/src/Rewrite.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Rewrite.sml Thu Dec 08 09:10:54 2011 +0100
@@ -85,9 +85,9 @@
Print.ppOp2 (" " ^ toStringOrientOption ort) Term.pp Term.pp x_y;
fun ppField f ppA a =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString (f ^ " ="),
- Print.addBreak 1,
+ Print.break,
ppA a];
val ppKnown =
@@ -111,21 +111,21 @@
(Print.ppMap (IntSet.toList) (Print.ppList Print.ppInt));
in
fun pp (Rewrite {known,redexes,subterms,waiting,...}) =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString "Rewrite",
- Print.addBreak 1,
- Print.blockProgram Print.Inconsistent 1
+ Print.break,
+ Print.inconsistentBlock 1
[Print.ppString "{",
ppKnown known,
(*MetisTrace5
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppRedexes redexes,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppSubterms subterms,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppWaiting waiting,
*)
Print.skip],
--- a/src/Tools/Metis/src/Stream.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Stream.sml Thu Dec 08 09:10:54 2011 +0100
@@ -188,7 +188,7 @@
| concatList (h :: t) = append h (fn () => concatList t);
local
- fun toLst res Nil = rev res
+ fun toLst res Nil = List.rev res
| toLst res (Cons (x, xs)) = toLst (x :: res) (xs ());
in
fun toList s = toLst [] s;
--- a/src/Tools/Metis/src/Term.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Term.sml Thu Dec 08 09:10:54 2011 +0100
@@ -160,7 +160,7 @@
let
fun f (n,arg) = (n :: path, arg)
- val acc = (rev path, tm) :: acc
+ val acc = (List.rev path, tm) :: acc
in
case tm of
Var _ => subtms rest acc
@@ -189,7 +189,7 @@
let
fun search [] = NONE
| search ((path,tm) :: rest) =
- if pred tm then SOME (rev path)
+ if pred tm then SOME (List.rev path)
else
case tm of
Var _ => search rest
@@ -301,7 +301,7 @@
Var _ => subtms rest acc
| Fn _ =>
let
- val acc = (rev path, tm) :: acc
+ val acc = (List.rev path, tm) :: acc
val rest = (0 :: path, t) :: rest
in
subtms rest acc
@@ -312,7 +312,7 @@
val (_,args) = func
- val acc = (rev path, tm) :: acc
+ val acc = (List.rev path, tm) :: acc
val rest = List.map f (enumerate args) @ rest
in
@@ -449,7 +449,7 @@
Print.program
[(if tok = "," then Print.skip else Print.ppString " "),
Print.ppString tok,
- Print.addBreak 1];
+ Print.break];
val iPrinter = Print.ppInfixes iOps destI iToken
@@ -515,14 +515,14 @@
fun functionArgument bv tm =
Print.sequence
- (Print.addBreak 1)
+ Print.break
(if isBrack tm then customBracket bv tm
else if isVar tm orelse isConst tm then basic bv tm
else bracket bv tm)
and basic bv (Var v) = varName bv v
| basic bv (Fn (f,args)) =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
(functionName bv f :: List.map (functionArgument bv) args)
and customBracket bv tm =
@@ -541,21 +541,21 @@
[Print.ppString q,
varName bv v,
Print.program
- (List.map (Print.sequence (Print.addBreak 1) o varName bv) vs),
+ (List.map (Print.sequence Print.break o varName bv) vs),
Print.ppString ".",
- Print.addBreak 1,
+ Print.break,
innerQuant bv tm]
end
and quantifier bv tm =
if not (isQuant tm) then customBracket bv tm
- else Print.block Print.Inconsistent 2 (innerQuant bv tm)
+ else Print.inconsistentBlock 2 [innerQuant bv tm]
and molecule bv (tm,r) =
let
val (n,tm) = stripNeg tm
in
- Print.blockProgram Print.Inconsistent n
+ Print.inconsistentBlock n
[Print.duplicate n (Print.ppString neg),
if isI tm orelse (r andalso isQuant tm) then bracket bv tm
else quantifier bv tm]
--- a/src/Tools/Metis/src/Thm.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Thm.sml Thu Dec 08 09:10:54 2011 +0100
@@ -110,7 +110,7 @@
(List.map Literal.toFormula (LiteralSet.toList (clause th)));
in
fun pp th =
- Print.blockProgram Print.Inconsistent 3
+ Print.inconsistentBlock 3
[Print.ppString "|- ",
Formula.pp (toFormula th)];
end;
--- a/src/Tools/Metis/src/Tptp.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Tptp.sml Thu Dec 08 09:10:54 2011 +0100
@@ -631,13 +631,13 @@
case length tms of
0 => ppConst mapping f
| a =>
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[ppFnName mapping (f,a),
Print.ppString "(",
Print.ppOpList "," term tms,
Print.ppString ")"]
in
- Print.block Print.Inconsistent 0 o term
+ fn tm => Print.inconsistentBlock 0 [term tm]
end;
fun ppRelName mapping ra = Print.ppString (relToTptp mapping ra);
@@ -648,14 +648,14 @@
case length tms of
0 => ppProp mapping r
| a =>
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[ppRelName mapping (r,a),
Print.ppString "(",
Print.ppOpList "," (ppTerm mapping) tms,
Print.ppString ")"];
local
- val neg = Print.sequence (Print.ppString "~") (Print.addBreak 1);
+ val neg = Print.sequence (Print.ppString "~") Print.break;
fun fof mapping fm =
case fm of
@@ -683,7 +683,7 @@
let
val (n,fm) = Formula.stripNeg fm
in
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.duplicate n neg,
unitary mapping fm]
end)
@@ -692,7 +692,7 @@
SOME a_b => Print.ppOp2 " =" (ppTerm mapping) (ppTerm mapping) a_b
| NONE => ppAtom mapping atm)
| _ =>
- Print.blockProgram Print.Inconsistent 1
+ Print.inconsistentBlock 1
[Print.ppString "(",
fof mapping fm,
Print.ppString ")"]
@@ -701,18 +701,18 @@
let
val mapping = addVarListMapping mapping vs
in
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString q,
Print.ppString " ",
- Print.blockProgram Print.Inconsistent (String.size q)
+ Print.inconsistentBlock (String.size q)
[Print.ppString "[",
Print.ppOpList "," (ppVar mapping) vs,
Print.ppString "] :"],
- Print.addBreak 1,
+ Print.break,
unitary mapping fm]
end;
in
- fun ppFof mapping fm = Print.block Print.Inconsistent 0 (fof mapping fm);
+ fun ppFof mapping fm = Print.inconsistentBlock 0 [fof mapping fm];
end;
(* ------------------------------------------------------------------------- *)
@@ -1036,7 +1036,7 @@
val ppProofPath = Term.ppPath;
fun ppProof mapping inf =
- Print.blockProgram Print.Inconsistent 1
+ Print.inconsistentBlock 1
[Print.ppString "[",
(case inf of
Proof.Axiom _ => Print.skip
@@ -1048,10 +1048,10 @@
Print.program
[ppProofLiteral mapping lit,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppProofPath path,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppProofTerm mapping tm]),
Print.ppString "]"];
@@ -1077,15 +1077,15 @@
val name = nameStrip inference
in
- Print.blockProgram Print.Inconsistent (size gen + 1)
+ Print.inconsistentBlock (size gen + 1)
[Print.ppString gen,
Print.ppString "(",
Print.ppString name,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppBracket "[" "]" (ppStrip mapping) inference,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppList ppParent parents,
Print.ppString ")"]
end
@@ -1095,15 +1095,15 @@
val name = nameNormalize inference
in
- Print.blockProgram Print.Inconsistent (size gen + 1)
+ Print.inconsistentBlock (size gen + 1)
[Print.ppString gen,
Print.ppString "(",
Print.ppString name,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppBracket "[" "]" (ppNormalize mapping) inference,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppList ppParent parents,
Print.ppString ")"]
end
@@ -1125,27 +1125,27 @@
List.map (fn parent => (parent,sub)) parents
end
in
- Print.blockProgram Print.Inconsistent (size gen + 1)
+ Print.inconsistentBlock (size gen + 1)
([Print.ppString gen,
Print.ppString "("] @
(if isTaut then
[Print.ppString "tautology",
Print.ppString ",",
- Print.addBreak 1,
- Print.blockProgram Print.Inconsistent 1
+ Print.break,
+ Print.inconsistentBlock 1
[Print.ppString "[",
Print.ppString name,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppProof mapping inference,
Print.ppString "]"]]
else
[Print.ppString name,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppProof mapping inference,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppList (ppProofParent mapping) parents]) @
[Print.ppString ")"])
end
@@ -1248,23 +1248,23 @@
CnfFormulaBody _ => "cnf"
| FofFormulaBody _ => "fof"
in
- Print.blockProgram Print.Inconsistent (size gen + 1)
+ Print.inconsistentBlock (size gen + 1)
([Print.ppString gen,
Print.ppString "(",
ppFormulaName name,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppRole role,
Print.ppString ",",
- Print.addBreak 1,
- Print.blockProgram Print.Consistent 1
+ Print.break,
+ Print.consistentBlock 1
[Print.ppString "(",
ppFormulaBody mapping body,
Print.ppString ")"]] @
(if isNoFormulaSource source then []
else
[Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppFormulaSource mapping source]) @
[Print.ppString ")."])
end;
@@ -1645,7 +1645,7 @@
(* ------------------------------------------------------------------------- *)
fun ppInclude i =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString "include('",
Print.ppString i,
Print.ppString "')."];
@@ -1686,7 +1686,7 @@
IncludeDeclaration i => (i :: il, fl)
| FormulaDeclaration f => (il, f :: fl)
in
- fn l => List.foldl part ([],[]) (rev l)
+ fn l => List.foldl part ([],[]) (List.rev l)
end;
local
@@ -1888,15 +1888,15 @@
List.foldl partitionFormula ([],[],[],[]) fms
val goal =
- case (rev cnfGoals, rev fofGoals) of
+ case (List.rev cnfGoals, List.rev fofGoals) of
([],[]) => NoGoal
| (cnfGoals,[]) => CnfGoal cnfGoals
| ([],fofGoals) => FofGoal fofGoals
| (_ :: _, _ :: _) =>
raise Error "TPTP problem has both cnf and fof conjecture formulas"
in
- {cnfAxioms = rev cnfAxioms,
- fofAxioms = rev fofAxioms,
+ {cnfAxioms = List.rev cnfAxioms,
+ fofAxioms = List.rev fofAxioms,
goal = goal}
end;
@@ -1956,7 +1956,7 @@
let
val {problem,sources} = norm
val {axioms,conjecture} = problem
- val problem = {axioms = rev axioms, conjecture = rev conjecture}
+ val problem = {axioms = List.rev axioms, conjecture = List.rev conjecture}
in
{subgoal = subgoal,
problem = problem,
@@ -2051,11 +2051,11 @@
fun stripLineComments acc strm =
case strm of
- Stream.Nil => (rev acc, Stream.Nil)
+ Stream.Nil => (List.rev acc, Stream.Nil)
| Stream.Cons (line,rest) =>
case total destLineComment line of
SOME s => stripLineComments (s :: acc) (rest ())
- | NONE => (rev acc, Stream.filter (not o isLineComment) strm);
+ | NONE => (List.rev acc, Stream.filter (not o isLineComment) strm);
fun advanceBlockComment c state =
case state of
@@ -2270,7 +2270,7 @@
val (names,ths) =
List.foldl (collectProofDeps sources) (names,[]) proof
- val normalization = Normalize.proveThms (rev ths)
+ val normalization = Normalize.proveThms (List.rev ths)
val (fofs,defs) =
List.foldl collectNormalizeDeps (fofs,defs) normalization
@@ -2554,7 +2554,7 @@
val formulas =
List.foldl (addSubgoalProofFormulas avoid fmNames) formulas proofs
in
- rev formulas
+ List.rev formulas
end
(*MetisDebug
handle Error err => raise Bug ("Tptp.fromProof: shouldn't fail:\n" ^ err);
--- a/src/Tools/Metis/src/Useful.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/Useful.sml Thu Dec 08 09:10:54 2011 +0100
@@ -213,7 +213,7 @@
| z l (x :: xs) (y :: ys) = z (f x y :: l) xs ys
| z _ _ _ = raise Error "zipWith: lists different lengths";
in
- fn xs => fn ys => rev (z [] xs ys)
+ fn xs => fn ys => List.rev (z [] xs ys)
end;
fun zip xs ys = zipWith pair xs ys;
@@ -221,7 +221,7 @@
local
fun inc ((x,y),(xs,ys)) = (x :: xs, y :: ys);
in
- fun unzip ab = List.foldl inc ([],[]) (rev ab);
+ fun unzip ab = List.foldl inc ([],[]) (List.rev ab);
end;
fun cartwith f =
@@ -232,15 +232,15 @@
aux xsCopy (f x y :: res) xt ys
in
fn xs => fn ys =>
- let val xs' = rev xs in aux xs' [] xs' (rev ys) end
+ let val xs' = List.rev xs in aux xs' [] xs' (List.rev ys) end
end;
fun cart xs ys = cartwith pair xs ys;
fun takeWhile p =
let
- fun f acc [] = rev acc
- | f acc (x :: xs) = if p x then f (x :: acc) xs else rev acc
+ fun f acc [] = List.rev acc
+ | f acc (x :: xs) = if p x then f (x :: acc) xs else List.rev acc
in
f []
end;
@@ -255,8 +255,8 @@
fun divideWhile p =
let
- fun f acc [] = (rev acc, [])
- | f acc (l as x :: xs) = if p x then f (x :: acc) xs else (rev acc, l)
+ fun f acc [] = (List.rev acc, [])
+ | f acc (l as x :: xs) = if p x then f (x :: acc) xs else (List.rev acc, l)
in
f []
end;
@@ -267,15 +267,15 @@
case l of
[] =>
let
- val acc = if List.null row then acc else rev row :: acc
+ val acc = if List.null row then acc else List.rev row :: acc
in
- rev acc
+ List.rev acc
end
| h :: t =>
let
val (eor,x) = f (h,x)
in
- if eor then group (rev row :: acc) [h] x t
+ if eor then group (List.rev row :: acc) [h] x t
else group acc (h :: row) x t
end
in
@@ -326,7 +326,7 @@
fun revDivide l = revDiv [] l;
end;
-fun divide l n = let val (a,b) = revDivide l n in (rev a, b) end;
+fun divide l n = let val (a,b) = revDivide l n in (List.rev a, b) end;
fun updateNth (n,x) l =
let
@@ -355,28 +355,28 @@
local
fun inc (v,x) = if mem v x then x else v :: x;
in
- fun setify s = rev (List.foldl inc [] s);
+ fun setify s = List.rev (List.foldl inc [] s);
end;
fun union s t =
let
fun inc (v,x) = if mem v t then x else v :: x
in
- List.foldl inc t (rev s)
+ List.foldl inc t (List.rev s)
end;
fun intersect s t =
let
fun inc (v,x) = if mem v t then v :: x else x
in
- List.foldl inc [] (rev s)
+ List.foldl inc [] (List.rev s)
end;
fun difference s t =
let
fun inc (v,x) = if mem v t then x else v :: x
in
- List.foldl inc [] (rev s)
+ List.foldl inc [] (List.rev s)
end;
fun subset s t = List.all (fn x => mem x t) s;
@@ -420,13 +420,13 @@
fun sort cmp =
let
- fun findRuns acc r rs [] = rev (rev (r :: rs) :: acc)
+ fun findRuns acc r rs [] = List.rev (List.rev (r :: rs) :: acc)
| findRuns acc r rs (x :: xs) =
case cmp (r,x) of
- GREATER => findRuns (rev (r :: rs) :: acc) x [] xs
+ GREATER => findRuns (List.rev (r :: rs) :: acc) x [] xs
| _ => findRuns acc x (r :: rs) xs
- fun mergeAdj acc [] = rev acc
+ fun mergeAdj acc [] = List.rev acc
| mergeAdj acc (xs as [_]) = List.revAppend (acc,xs)
| mergeAdj acc (x :: y :: xs) = mergeAdj (merge cmp x y :: acc) xs
@@ -567,7 +567,7 @@
[] => []
| h :: t => if Char.isSpace h then chop t else l;
in
- val trim = String.implode o chop o rev o chop o rev o String.explode;
+ val trim = String.implode o chop o List.rev o chop o List.rev o String.explode;
end;
val join = String.concatWith;
@@ -584,11 +584,11 @@
let
val pat = String.explode sep
- fun div1 prev recent [] = stringify [] (rev recent :: prev)
+ fun div1 prev recent [] = stringify [] (List.rev recent :: prev)
| div1 prev recent (l as h :: t) =
case match pat l of
NONE => div1 prev (h :: recent) t
- | SOME rest => div1 (rev recent :: prev) [] rest
+ | SOME rest => div1 (List.rev recent :: prev) [] rest
in
fn s => div1 [] [] (String.explode s)
end;
@@ -797,7 +797,7 @@
val () = OS.FileSys.closeDir dirStrm
in
- rev filenames
+ List.rev filenames
end;
fun readTextFile {filename} =
--- a/src/Tools/Metis/src/metis.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/metis.sml Thu Dec 08 09:10:54 2011 +0100
@@ -13,7 +13,7 @@
val VERSION = "2.3";
-val versionString = PROGRAM^" "^VERSION^" (release 20110531)"^"\n";
+val versionString = PROGRAM^" "^VERSION^" (release 20110926)"^"\n";
(* ------------------------------------------------------------------------- *)
(* Program options. *)
@@ -373,7 +373,7 @@
let
val seen = StringSet.empty
- val includes = rev includes
+ val includes = List.rev includes
val formulas = readIncludes mapping seen formulas includes
in
@@ -454,7 +454,7 @@
val () =
if !TEST then ()
- else display_proof filename tptp (rev acc)
+ else display_proof filename tptp (List.rev acc)
in
true
end
--- a/src/Tools/Metis/src/selftest.sml Thu Dec 08 09:10:44 2011 +0100
+++ b/src/Tools/Metis/src/selftest.sml Thu Dec 08 09:10:54 2011 +0100
@@ -626,7 +626,7 @@
val fm = LiteralSet.disjoin cl
in
- Print.blockProgram Print.Consistent ind
+ Print.consistentBlock ind
[Print.ppString p,
Print.ppString (nChars #" " (ind - size p)),
Formula.pp fm]