# HG changeset patch # User Christian Urban # Date 1323273968 0 # Node ID 3e8a2464f6071f1a7b8cc6b28f2859351b49a271 # Parent f82020ca32482c3be10d5f17dda2b31ac15e42cb# Parent fc2c368b5f54317c86c2eb1a332d138d1e0cc1d5 merged diff -r f82020ca3248 -r 3e8a2464f607 src/HOL/Probability/Binary_Product_Measure.thy --- a/src/HOL/Probability/Binary_Product_Measure.thy Wed Dec 07 14:00:02 2011 +0000 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Wed Dec 07 16:06:08 2011 +0000 @@ -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 \ pair_sigma_algebra M1 M2 - by default - lemma (in pair_sigma_finite) measure_cut_measurable_fst: assumes "Q \ sets P" shows "(\x. measure M2 (Pair x -` Q)) \ borel_measurable M1" (is "?s Q \ _") proof - @@ -919,10 +916,7 @@ show "a \ A" and "b \ 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 \ 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 = \ space = space M1 \ space M2, sets = Pow (space M1 \ space M2), \ = algebra.more P \" @@ -933,20 +927,16 @@ qed sublocale pair_finite_sigma_algebra \ 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 \ pair_finite_sigma_algebra - by default - -sublocale pair_finite_space \ 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 \ space M1" "b \ space M2" @@ -964,6 +954,10 @@ using pair_measure_Pair assms by (cases x) auto sublocale pair_finite_space \ finite_measure_space P - by default (auto simp: space_pair_measure) +proof unfold_locales + show "measure P (space P) \ \" + by (subst (2) finite_pair_sigma_algebra) + (simp add: pair_measure_times) +qed end \ No newline at end of file diff -r f82020ca3248 -r 3e8a2464f607 src/HOL/Probability/Finite_Product_Measure.thy --- a/src/HOL/Probability/Finite_Product_Measure.thy Wed Dec 07 14:00:02 2011 +0000 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Wed Dec 07 16:06:08 2011 +0000 @@ -240,7 +240,7 @@ locale finite_product_sigma_algebra = product_sigma_algebra M for M :: "'i \ ('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 = \ space = (\\<^isub>E i \ I. space (M i)), @@ -508,22 +508,15 @@ finally show "(\x. \i\I. X i x) -` E \ space M \ sets M" . qed -locale product_sigma_finite = - fixes M :: "'i \ ('a,'b) measure_space_scheme" +locale product_sigma_finite = product_sigma_algebra M + for M :: "'i \ ('a,'b) measure_space_scheme" + assumes sigma_finite_measures: "\i. sigma_finite_measure (M i)" -locale finite_product_sigma_finite = product_sigma_finite M - for M :: "'i \ ('a,'b) measure_space_scheme" + - fixes I :: "'i set" assumes finite_index'[intro]: "finite I" - sublocale product_sigma_finite \ M: sigma_finite_measure "M i" for i by (rule sigma_finite_measures) -sublocale product_sigma_finite \ product_sigma_algebra - by default - -sublocale finite_product_sigma_finite \ 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 \ ('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 \ sets G" diff -r f82020ca3248 -r 3e8a2464f607 src/HOL/Probability/Independent_Family.thy --- a/src/HOL/Probability/Independent_Family.thy Wed Dec 07 14:00:02 2011 +0000 +++ b/src/HOL/Probability/Independent_Family.thy Wed Dec 07 16:06:08 2011 +0000 @@ -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 \ 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) diff -r f82020ca3248 -r 3e8a2464f607 src/HOL/Probability/Infinite_Product_Measure.thy --- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Dec 07 14:00:02 2011 +0000 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Dec 07 16:06:08 2011 +0000 @@ -41,36 +41,11 @@ qed qed -locale product_prob_space = - fixes M :: "'i \ ('a,'b) measure_space_scheme" and I :: "'i set" - assumes prob_spaces: "\i. prob_space (M i)" - and I_not_empty: "I \ {}" - -locale finite_product_prob_space = product_prob_space M I - for M :: "'i \ ('a,'b) measure_space_scheme" and I :: "'i set" + - assumes finite_index'[intro]: "finite I" - -sublocale product_prob_space \ M: prob_space "M i" for i - by (rule prob_spaces) - -sublocale product_prob_space \ product_sigma_finite - by default - -sublocale finite_product_prob_space \ finite_product_sigma_finite - by default (fact finite_index') - -sublocale finite_product_prob_space \ 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 \ {}" "J \ K" "finite K" shows "(\f. restrict f J) \ measure_preserving (\\<^isub>M i\K. M i) (\\<^isub>M i\J. M i)" (is "?R \ _") 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 \ {}" "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 \ 'a) measure_space" where "infprod_algebra = sigma generator \ measure := (SOME \. (\s\sets generator. \ s = \G s) \ - measure_space \space = space generator, sets = sets (sigma generator), measure = \\)\" + prob_space \space = space generator, sets = sets (sigma generator), measure = \\)\" 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 \ G!: algebra generator +lemma (in product_prob_space) algebra_generator: + assumes "I \ {}" shows "algebra generator" proof let ?G = generator show "sets ?G \ Pow (space ?G)" by (auto simp: generator_def emb_def) - from I_not_empty - obtain i where "i \ I" by auto + from `I \ {}` obtain i where "i \ I" by auto then show "{} \ sets ?G" by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\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_\G: "positive generator \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 "\G {} = 0" by simp -next - fix A assume "A \ 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 \ \G A" by simp +lemma (in product_prob_space) positive_\G: + assumes "I \ {}" + shows "positive generator \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 "\G {} = 0" by simp + next + fix A assume "A \ 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 \ \G A" by simp + qed qed -lemma (in product_prob_space) additive_\G: "additive generator \G" -proof (intro additive_def[THEN iffD2] ballI impI) - fix A assume "A \ sets generator" with generatorE guess J X . note J = this - fix B assume "B \ sets generator" with generatorE guess K Y . note K = this - assume "A \ B = {}" - have JK: "J \ K \ {}" "J \ K \ I" "finite (J \ K)" - using J K by auto - interpret JK: finite_product_sigma_finite M "J \ K" by default fact - have JK_disj: "emb (J \ K) J X \ emb (J \ K) K Y = {}" - apply (rule emb_injective[of "J \ K" I]) - apply (insert `A \ B = {}` JK J K) - apply (simp_all add: JK.Int emb_simps) - done - have AB: "A = emb I (J \ K) (emb (J \ K) J X)" "B = emb I (J \ K) (emb (J \ K) K Y)" - using J K by simp_all - then have "\G (A \ B) = \G (emb I (J \ K) (emb (J \ K) J X \ emb (J \ K) K Y))" - by (simp add: emb_simps) - also have "\ = measure (Pi\<^isub>M (J \ K) M) (emb (J \ K) J X \ emb (J \ K) K Y)" - using JK J(1, 4) K(1, 4) by (simp add: \G_eq JK.Un) - also have "\ = \G A + \G B" - using J K JK_disj by (simp add: JK.measure_additive[symmetric]) - finally show "\G (A \ B) = \G A + \G B" . +lemma (in product_prob_space) additive_\G: + assumes "I \ {}" + shows "additive generator \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 \ sets generator" with generatorE guess J X . note J = this + fix B assume "B \ sets generator" with generatorE guess K Y . note K = this + assume "A \ B = {}" + have JK: "J \ K \ {}" "J \ K \ I" "finite (J \ K)" + using J K by auto + interpret JK: finite_product_sigma_finite M "J \ K" by default fact + have JK_disj: "emb (J \ K) J X \ emb (J \ K) K Y = {}" + apply (rule emb_injective[of "J \ K" I]) + apply (insert `A \ B = {}` JK J K) + apply (simp_all add: JK.Int emb_simps) + done + have AB: "A = emb I (J \ K) (emb (J \ K) J X)" "B = emb I (J \ K) (emb (J \ K) K Y)" + using J K by simp_all + then have "\G (A \ B) = \G (emb I (J \ K) (emb (J \ K) J X \ emb (J \ K) K Y))" + by (simp add: emb_simps) + also have "\ = measure (Pi\<^isub>M (J \ K) M) (emb (J \ K) J X \ emb (J \ K) K Y)" + using JK J(1, 4) K(1, 4) by (simp add: \G_eq JK.Un) + also have "\ = \G A + \G B" + using J K JK_disj by (simp add: JK.measure_additive[symmetric]) + finally show "\G (A \ B) = \G A + \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 \ sets (sigma generator)" then show "A \ sets I.P" unfolding sets_sigma @@ -396,19 +383,32 @@ with `finite I` have "emb I J X \ sets I.P" by auto with `emb I J X = A` show "A \ sets I.P" by simp qed auto } - { fix A assume "A \ sets I.P" - moreover with I.sets_into_space have "emb I I A = A" by (intro emb_id) auto - ultimately show "A \ 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 \ sets I.P" + show "A \ sets (sigma generator)" + proof cases + assume "I = {}" + with I.P_empty[OF this] A + have "A = space generator \ 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 \ {}" + note A this + moreover with I.sets_into_space have "emb I I A = A" by (intro emb_id) auto + ultimately show "A \ 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_\G: "\\. (\s\sets generator. \ s = \G s) \ - measure_space \space = space generator, sets = sets (sigma generator), measure = \\" + prob_space \space = space generator, sets = sets (sigma generator), measure = \\" 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 \ sets generator" @@ -422,13 +422,20 @@ have "\space = space generator, sets = sets (sigma generator), measure = measure I.P\ = 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 "\ finite I" + then have I_not_empty: "I \ {}" by auto + interpret G!: algebra generator by (rule algebra_generator) fact note \G_mono = - G.additive_increasing[OF positive_\G additive_\G, THEN increasingD] + G.additive_increasing[OF positive_\G[OF I_not_empty] additive_\G[OF I_not_empty], THEN increasingD] { fix Z J assume J: "J \ {}" "finite J" "J \ I" and Z: "Z \ sets ?G" @@ -488,7 +495,9 @@ note this fold le_1 merge_in_G(3) } note fold = this - show ?thesis + have "\\. (\s\sets ?G. \ s = \G s) \ + measure_space \space = space ?G, sets = sets (sigma ?G), measure = \\" + (is "\\. _ \ measure_space (?ms \)") proof (rule G.caratheodory_empty_continuous[OF positive_\G additive_\G]) fix A assume "A \ sets ?G" with generatorE guess J X . note JX = this @@ -503,7 +512,7 @@ proof (rule ccontr) assume "(INF i. \G (A i)) \ 0" (is "?a \ 0") moreover have "0 \ ?a" - using A positive_\G by (auto intro!: INF_greatest simp: positive_def) + using A positive_\G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def) ultimately have "0 < ?a" by auto have "\n. \J X. J \ {} \ finite J \ J \ I \ X \ sets (Pi\<^isub>M J M) \ A n = emb I J X \ \G (A n) = measure (Pi\<^isub>M J M) X" @@ -659,7 +668,7 @@ moreover from w have "?a / 2 ^ (k + 1) \ ?q k k (w k)" by auto then have "?M (J k) (A k) (w k) \ {}" - using positive_\G[unfolded positive_def] `0 < ?a` `?a \ 1` + using positive_\G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \ 1` by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq) then obtain x where "x \ ?M (J k) (A k) (w k)" by auto then have "merge (J k) (w k) (I - J k) x \ A k" by auto @@ -713,28 +722,42 @@ qed ultimately show "(\i. \G (A i)) ----> 0" using LIMSEQ_ereal_INFI[of "\i. \G (A i)"] by simp + qed fact+ + then guess \ .. note \ = this + show ?thesis + proof (intro exI[of _ \] conjI) + show "\S\sets ?G. \ S = \G S" using \ by simp + show "prob_space (?ms \)" + proof + show "measure_space (?ms \)" using \ by simp + obtain i where "i \ I" using I_not_empty by auto + interpret i: finite_product_sigma_finite M "{i}" by default auto + let ?X = "\\<^isub>E i\{i}. space (M i)" + have X: "?X \ sets (Pi\<^isub>M {i} M)" + by auto + with `i \ I` have "emb I {i} ?X \ sets generator" + by (intro generatorI') auto + with \ have "\ (emb I {i} ?X) = \G (emb I {i} ?X)" by auto + with \G_eq[OF _ _ _ X] `i \ I` + have "\ (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 \ I` by (auto simp: emb_def infprod_algebra_def generator_def) + finally show "measure (?ms \) (space (?ms \)) = 1" + using M.measure_space_1 by (simp add: infprod_algebra_def) + qed qed qed lemma (in product_prob_space) infprod_spec: - shows "(\s\sets generator. measure (Pi\<^isub>P I M) s = \G s) \ measure_space (Pi\<^isub>P I M)" -proof - - let ?P = "\\. (\A\sets generator. \ A = \G A) \ - measure_space \space = space generator, sets = sets (sigma generator), measure = \\" - have **: "measure infprod_algebra = (SOME \. ?P \)" - unfolding infprod_algebra_def by simp - have *: "Pi\<^isub>P I M = \space = space generator, sets = sets (sigma generator), measure = measure (Pi\<^isub>P I M)\" - unfolding infprod_algebra_def by auto - show ?thesis - apply (subst (2) *) - apply (unfold **) - apply (rule someI_ex[where P="?P"]) - apply (rule extend_\G) - done -qed + "(\s\sets generator. measure (Pi\<^isub>P I M) s = \G s) \ prob_space (Pi\<^isub>P I M)" + (is "?Q infprod_algebra") + unfolding infprod_algebra_def + by (rule someI2_ex[OF extend_\G]) + (auto simp: sigma_def generator_def) -sublocale product_prob_space \ P: measure_space "Pi\<^isub>P I M" - using infprod_spec by auto +sublocale product_prob_space \ P: prob_space "Pi\<^isub>P I M" + using infprod_spec by simp lemma (in product_prob_space) measure_infprod_emb: assumes "J \ {}" "finite J" "J \ I" "X \ sets (Pi\<^isub>M J M)" @@ -745,22 +768,6 @@ with \G_eq[OF assms] infprod_spec show ?thesis by auto qed -sublocale product_prob_space \ P: prob_space "Pi\<^isub>P I M" -proof - obtain i where "i \ I" using I_not_empty by auto - interpret i: finite_product_sigma_finite M "{i}" by default auto - let ?X = "\\<^isub>E i\{i}. space (M i)" - have "?X \ sets (Pi\<^isub>M {i} M)" - by auto - from measure_infprod_emb[OF _ _ _ this] `i \ I` - have "\ (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 \ I` by (auto simp: emb_def infprod_algebra_def generator_def) - finally show "\ (space (Pi\<^isub>P I M)) = 1" - using M.measure_space_1 by simp -qed - lemma (in product_prob_space) measurable_component: assumes "i \ I" shows "(\x. x i) \ 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 \ {}" interpret J: finite_product_prob_space M J by default fact+ diff -r f82020ca3248 -r 3e8a2464f607 src/HOL/Probability/Information.thy --- a/src/HOL/Probability/Information.thy Wed Dec 07 14:00:02 2011 +0000 +++ b/src/HOL/Probability/Information.thy Wed Dec 07 16:06:08 2011 +0000 @@ -198,7 +198,7 @@ proof - interpret \: prob_space "M\measure := \\" by fact have ms: "measure_space (M\measure := \\)" by default - have fms: "finite_measure (M\measure := \\)" by default + have fms: "finite_measure (M\measure := \\)" 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\measure := \\" by fact - have ps: "prob_space (M\measure := \\)" by default + have ps: "prob_space (M\measure := \\)" by unfold_locales from KL_ge_0[OF this ac v.integral_finite_singleton(1)] show ?thesis . qed @@ -558,7 +558,7 @@ have eq: "\A\sets XY.P. (ereal \ joint_distribution X Y) A = XY.\ 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\joint_distribution X Y)" using ac by (simp add: P_def) show "integrable ?J (entropy_density b XY.P (ereal\joint_distribution X Y))" @@ -624,7 +624,7 @@ have "prob_space (P.P\ measure := ereal\joint_distribution X Y\)" using X Y by (auto intro!: distribution_prob_space random_variable_pairI) then show "measure_space (P.P\ measure := ereal\joint_distribution X Y\)" - 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\joint_distribution X Y)" proof (rule XY.absolutely_continuousI) - show "finite_measure_space (XY.P\ measure := ereal\joint_distribution X Y\)" by default + show "finite_measure_space (XY.P\ measure := ereal\joint_distribution X Y\)" by unfold_locales fix x assume "x \ space XY.P" and "XY.\ {x} = 0" then obtain a b where "x = (a, b)" and "distribution X {a} = 0 \ distribution Y {b} = 0" @@ -684,8 +684,8 @@ interpret P: finite_prob_space "XY.P\measure := ereal\joint_distribution X Y\" using assms by (auto intro!: joint_distribution_finite_prob_space) - have P_ms: "finite_measure_space (XY.P\measure := ereal\joint_distribution X Y\)" by default - have P_ps: "finite_prob_space (XY.P\measure := ereal\joint_distribution X Y\)" by default + have P_ms: "finite_measure_space (XY.P\measure := ereal\joint_distribution X Y\)" by unfold_locales + have P_ps: "finite_prob_space (XY.P\measure := ereal\joint_distribution X Y\)" by unfold_locales show ?sum unfolding Let_def mutual_information_def diff -r f82020ca3248 -r 3e8a2464f607 src/HOL/Probability/Measure.thy --- a/src/HOL/Probability/Measure.thy Wed Dec 07 14:00:02 2011 +0000 +++ b/src/HOL/Probability/Measure.thy Wed Dec 07 16:06:08 2011 +0000 @@ -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: "\ (space M) \ \" -sublocale finite_measure < sigma_finite_measure -proof - show "\A. range A \ sets M \ (\i. A i) = space M \ (\i. \ (A i) \ \)" - using finite_measure_of_space by (auto intro!: exI[of _ "\x. space M"]) +lemma finite_measureI[Pure.intro!]: + assumes "measure_space M" + assumes *: "measure M (space M) \ \" + shows "finite_measure M" +proof - + interpret measure_space M by fact + show "finite_measure M" + proof + show "measure M (space M) \ \" by fact + show "\A. range A \ sets M \ (\i. A i) = space M \ (\i. \ (A i) \ \)" + using * by (auto intro!: exI[of _ "\x. space M"]) + qed qed lemma (in finite_measure) finite_measure[simp, intro]: @@ -1222,22 +1230,19 @@ assumes "S \ 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) \ \" using finite_measure[OF `S \ sets M`] by auto qed lemma (in measure_space) restricted_to_finite_measure: assumes "S \ sets M" "\ S \ \" shows "finite_measure (restricted_space S)" -proof - - have "measure_space (restricted_space S)" +proof + show "measure_space (restricted_space S)" using `S \ 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)) \ \" + 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]: "\x. x \ space M \ \ {x} \ \" +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) \ \" + and pos: "\x. x \ space M \ 0 \ measure M {x}" + and add: "\A. A \ space M \ measure M A = (\x\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 "\ (space M) \ \" by fact + qed default + show "finite_measure_space M" + by default +qed lemma (in finite_measure_space) sum_over_space: "(\x\space M. \ {x}) = \ (space M)" using measure_setsum[of "space M" "\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) \ \" - and add: "\A B. A\space M \ B\space M \ A \ B = {} \ measure M (A \ B) = measure M A + measure M B" - and "measure M {} = 0" "\A. A \ space M \ 0 \ 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 *: "\space = space M, sets = Pow (space M), \ = algebra.more M\ = 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 \ space M" - with add[of "{x}" "space M - {x}"] space - show "\ {x} \ \" by (auto simp: insert_absorb[OF *] Diff_subset) } -qed - -sublocale finite_measure_space \ finite_measure -proof - show "\ (space M) \ \" - 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 \ - finite (space M) \ sets M = Pow(space M) \ measure M (space M) \ \ \ - measure M {} = 0 \ (\A\space M. 0 \ measure M A) \ - (\A\space M. \B\space M. A \ B = {} \ measure M (A \ 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 \ space M" shows "\' A = (\x\A. \' {x})" using A finite_subset[OF A finite_space] diff -r f82020ca3248 -r 3e8a2464f607 src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Wed Dec 07 14:00:02 2011 +0000 +++ b/src/HOL/Probability/Probability_Measure.thy Wed Dec 07 16:06:08 2011 +0000 @@ -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 "\ (space M) \ \" 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) \ \" using * by simp + qed + show "prob_space M" by default fact qed abbreviation (in prob_space) "events \ sets M" @@ -31,9 +39,10 @@ lemma (in prob_space) prob_space_cong: assumes "\A. A \ sets M \ measure N A = \ 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 \ 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 \ 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 \ 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 (\x. (X x, Y x)) Z {((x, y), z)}" unfolding distribution_def by (auto intro!: arg_cong[where f=\']) -locale pair_prob_space = M1: prob_space M1 + M2: prob_space M2 for M1 M2 - -sublocale pair_prob_space \ 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 \ 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 "\A. \ range A \ sets M ; disjoint_family A ; (\i. A i) \ sets M\ \ @@ -557,20 +567,21 @@ shows "prob_space ((MX \\<^isub>M MY) \ measure := ereal \ joint_distribution X Y\)" using random_variable_pairI[OF assms] by (rule distribution_prob_space) +locale product_prob_space = product_sigma_finite M for M :: "'i \ ('a, 'b) measure_space_scheme" + + fixes I :: "'i set" + assumes prob_space: "\i. prob_space (M i)" -locale finite_product_prob_space = - fixes M :: "'i \ ('a,'b) measure_space_scheme" - and I :: "'i set" - assumes prob_space: "\i. prob_space (M i)" and finite_index: "finite I" - -sublocale finite_product_prob_space \ M: prob_space "M i" for i +sublocale product_prob_space \ M: prob_space "M i" for i by (rule prob_space) -sublocale finite_product_prob_space \ 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 \ prob_space "\\<^isub>M i\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: "\i. i \ I \ X i \ 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 \\<^isub>M MY)" by default + show "finite_sigma_algebra (MX \\<^isub>M MY)" .. have sa: "sigma_algebra M" by default show "(\x. (X x, Y x)) \ measurable M (MX \\<^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 "\ space = UNIV, sets = Pow UNIV \" "\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 \ pair_prob_space M1 M2 by default -sublocale pair_finite_prob_space \ pair_finite_space M1 M2 by default -sublocale pair_finite_prob_space \ 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 \ ('a,'b) measure_space_scheme" - and I :: "'i set" - assumes finite_space: "\i. finite_prob_space (M i)" and finite_index: "finite I" - -sublocale product_finite_prob_space \ M!: finite_prob_space "M i" using finite_space . -sublocale product_finite_prob_space \ finite_product_sigma_finite M I by default (rule finite_index) -sublocale product_finite_prob_space \ prob_space "Pi\<^isub>M I M" -proof - show "\ (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 \ finite_prob_space P by default lemma funset_eq_UN_fun_upd_I: assumes *: "\f. f \ F (insert a A) \ f(a := d) \ 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: "\i. finite_prob_space (M i)" + +sublocale finite_product_finite_prob_space \ M!: finite_prob_space "M i" using finite_space . + +lemma (in finite_product_finite_prob_space) singleton_eq_product: assumes x: "x \ space P" shows "{x} = (\\<^isub>E i\I. {x i})" proof (safe intro!: ext[of _ x]) fix y i assume *: "y \ (\ i\I. {x i})" "y \ extensional I" @@ -823,7 +823,7 @@ by (cases "i \ I") (auto simp: extensional_def) qed (insert x, auto) -sublocale product_finite_prob_space \ finite_prob_space "Pi\<^isub>M I M" +sublocale finite_product_finite_prob_space \ 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 \ sets P" by simp qed with space_closed show [simp]: "sets P = Pow (space P)" .. - - { fix x assume "x \ space P" - from this top have "\ {x} \ \ (space P)" by (intro measure_mono) auto - then show "\ {x} \ \" - 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: "(\i. i \ I \ X i \ space (M i)) \ \ (\\<^isub>E i\I. X i) = (\i\I. M.\ 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 \ space P" shows "\ {x} = (\i\I. M.\ 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: "\i. i \ I \ X i \ space (M i)" shows "prob (\\<^isub>E i\I. X i) = (\i\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 \ space P" shows "prob {x} = (\i\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 \ space P \ prob A = (\x\A. \i\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 \ sets M" "space N = space M" and "\A. A \ sets N \ measure N A = \ 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 / \ A = 0" using `\ A \ 0` by (cases "\ A") (auto simp: zero_ereal_def) + fix B assume "B \ events" + with real_measure[of "A \ B"] real_measure[OF `A \ events`] `A \ sets M` + show "0 \ \ (A \ B) / \ A" by (auto simp: Int) + qed + show "countably_additive ?P (measure ?P)" + proof (simp add: countably_additive_def, safe) + fix B and F :: "nat \ 'a set" + assume F: "range F \ op \ A ` events" "disjoint_family F" + { fix i + from F have "F i \ op \ A ` events" by auto + with `A \ events` have "F i \ events" by auto } + moreover then have "range F \ events" by auto + moreover have "\S. \ S / \ A = inverse (\ A) * \ S" + by (simp add: mult_commute divide_ereal_def) + moreover have "0 \ inverse (\ A)" + using real_measure[OF `A \ events`] by auto + ultimately show "(\i. \ (F i) / \ A) = \ (\i. F i) / \ 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 \ events`] `\ A \ 0` by auto - show "positive ?P (measure ?P)" - proof (simp add: positive_def, safe) - show "0 / \ A = 0" using `\ A \ 0` by (cases "\ A") (auto simp: zero_ereal_def) - fix B assume "B \ events" - with real_measure[of "A \ B"] real_measure[OF `A \ events`] `A \ sets M` - show "0 \ \ (A \ B) / \ A" by (auto simp: Int) - qed - show "countably_additive ?P (measure ?P)" - proof (simp add: countably_additive_def, safe) - fix B and F :: "nat \ 'a set" - assume F: "range F \ op \ A ` events" "disjoint_family F" - { fix i - from F have "F i \ op \ A ` events" by auto - with `A \ events` have "F i \ events" by auto } - moreover then have "range F \ events" by auto - moreover have "\S. \ S / \ A = inverse (\ A) * \ S" - by (simp add: mult_commute divide_ereal_def) - moreover have "0 \ inverse (\ A)" - using real_measure[OF `A \ events`] by auto - ultimately show "(\i. \ (F i) / \ A) = \ (\i. F i) / \ 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" "\A. A \ space M \ 0 \ measure M A" - and "\A B. A\space M \ B\space M \ A \ B = {} \ measure M (A \ B) = measure M A + measure M B" + and 1: "measure M (space M) = 1" and "\x. x \ space M \ 0 \ measure M {x}" + and add: "\A B. A \ space M \ measure M A = (\x\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) \ \" using 1 by simp + qed fact+ + show ?thesis by default fact +qed + +lemma (in finite_prob_space) distribution_eq_setsum: + "distribution X A = (\x\A \ X ` space M. distribution X {x})" +proof - + have *: "X -` A \ space M = (\x\A \ X ` space M. X -` {x} \ space M)" + by auto + then show "distribution X A = (\x\A \ 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 = (\x\A. distribution X {x})" +proof - + note distribution_eq_setsum[of X A] + also have "(\x\A \ X ` space M. distribution X {x}) = (\x\A. distribution X {x})" + proof (intro setsum_mono_zero_cong_left ballI) + fix i assume "i\A - A \ X ` space M" + then have "X -` {i} \ 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 \ B = {}" - then show "distribution X (A \ B) = distribution X A + distribution X B" - unfolding distribution_def - by (subst finite_measure_Union[symmetric]) - (auto intro!: arg_cong[where f=\'] simp: sets_eq_Pow) + fix A assume "A \ X ` space M" + then show "distribution X A = (\x\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 \ s2)" using assms by auto next - fix A B :: "('x*'y) set" assume "A \ B = {}" - then show "joint_distribution X Y (A \ 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=\'] simp: sets_eq_Pow) + fix A assume "A \ (s1 \ s2)" + with assms show "joint_distribution X Y A = (\x\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 \ sets borel \ A \ {0 ..< 1} then real (lborel.\ A) else 0)" unfolding pborel.\'_def by (auto simp: pborel_def) diff -r f82020ca3248 -r 3e8a2464f607 src/HOL/Probability/Radon_Nikodym.thy --- a/src/HOL/Probability/Radon_Nikodym.thy Wed Dec 07 14:00:02 2011 +0000 +++ b/src/HOL/Probability/Radon_Nikodym.thy Wed Dec 07 16:06:08 2011 +0000 @@ -427,35 +427,38 @@ have f_le_\: "\A. A \ sets M \ (\\<^isup>+x. ?F A x \M) \ \ A" using `f \ 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 \ 'a set" assume A: "range A \ sets M" "disjoint_family A" - have "(\n. (\\<^isup>+x. ?F (A n) x \M)) = (\\<^isup>+x. (\n. ?F (A n) x) \M)" - using `range A \ sets M` `\x. 0 \ f x` - by (intro positive_integral_suminf[symmetric]) auto - also have "\ = (\\<^isup>+x. ?F (\n. A n) x \M)" - using `\x. 0 \ f x` - by (intro positive_integral_cong) (simp add: suminf_cmult_ereal suminf_indicator[OF `disjoint_family A`]) - finally have "(\n. (\\<^isup>+x. ?F (A n) x \M)) = (\\<^isup>+x. ?F (\n. A n) x \M)" . - moreover have "(\n. \ (A n)) = \ (\n. A n)" - using M'.measure_countably_additive A by (simp add: comp_def) - moreover have v_fin: "\ (\i. A i) \ \" using M'.finite_measure A by (simp add: countable_UN) - moreover { - have "(\\<^isup>+x. ?F (\i. A i) x \M) \ \ (\i. A i)" - using A `f \ G` unfolding G_def by (auto simp: countable_UN) - also have "\ (\i. A i) < \" using v_fin by simp - finally have "(\\<^isup>+x. ?F (\i. A i) x \M) \ \" by simp } - moreover have "\i. (\\<^isup>+x. ?F (A i) x \M) \ \ (A i)" - using A by (intro f_le_\) auto - ultimately - show "(\n. ?t (A n)) = ?t (\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 \ 'a set" assume A: "range A \ sets M" "disjoint_family A" + have "(\n. (\\<^isup>+x. ?F (A n) x \M)) = (\\<^isup>+x. (\n. ?F (A n) x) \M)" + using `range A \ sets M` `\x. 0 \ f x` + by (intro positive_integral_suminf[symmetric]) auto + also have "\ = (\\<^isup>+x. ?F (\n. A n) x \M)" + using `\x. 0 \ f x` + by (intro positive_integral_cong) (simp add: suminf_cmult_ereal suminf_indicator[OF `disjoint_family A`]) + finally have "(\n. (\\<^isup>+x. ?F (A n) x \M)) = (\\<^isup>+x. ?F (\n. A n) x \M)" . + moreover have "(\n. \ (A n)) = \ (\n. A n)" + using M'.measure_countably_additive A by (simp add: comp_def) + moreover have v_fin: "\ (\i. A i) \ \" using M'.finite_measure A by (simp add: countable_UN) + moreover { + have "(\\<^isup>+x. ?F (\i. A i) x \M) \ \ (\i. A i)" + using A `f \ G` unfolding G_def by (auto simp: countable_UN) + also have "\ (\i. A i) < \" using v_fin by simp + finally have "(\\<^isup>+x. ?F (\i. A i) x \M) \ \" by simp } + moreover have "\i. (\\<^isup>+x. ?F (A i) x \M) \ \ (A i)" + using A by (intro f_le_\) auto + ultimately + show "(\n. ?t (A n)) = ?t (\i. A i)" + by (subst suminf_ereal_minus) (simp_all add: positive_integral_positive) + next + fix A assume A: "A \ sets M" show "0 \ \ A - \\<^isup>+ x. ?F A x \M" + using f_le_\[OF A] `f \ G` M'.finite_measure[OF A] by (auto simp: G_def ereal_le_minus_iff) + qed next - fix A assume A: "A \ sets M" show "0 \ \ A - \\<^isup>+ x. ?F A x \M" - using f_le_\[OF A] `f \ G` M'.finite_measure[OF A] by (auto simp: G_def ereal_le_minus_iff) - next - show "\ (space M) - (\\<^isup>+ x. ?F (space M) x \M) \ \" (is "?a - ?b \ _") + show "measure ?M (space ?M) \ \" using positive_integral_positive[of "?F (space M)"] - by (cases rule: ereal2_cases[of ?a ?b]) auto + by (cases rule: ereal2_cases[of "\ (space M)" "\\<^isup>+ x. ?F (space M) x \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 \ b` by (auto simp: positive_def) - show "countably_additive ?Mb (measure ?Mb)" - using `0 \ 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 \ b` by (auto simp: positive_def) + show "countably_additive ?Mb (measure ?Mb)" + using `0 \ b` measure_countably_additive + by (auto simp: countably_additive_def suminf_cmult_ereal subset_eq) + qed show "measure ?Mb (space ?Mb) \ \" 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) \ measure := \\)" (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\ measure := ?T \" 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 \" proof (unfold T.absolutely_continuous_def, safe) fix N assume "N \ sets M" "(\\<^isup>+x. h x * indicator N x \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\ measure := \A. (\\<^isup>+x. h x * indicator A x \M) \" - by default (simp cong: positive_integral_cong add: fin) + by (intro H finite_measureI) (simp cong: positive_integral_cong add: fin) let ?fM = "M\measure := \A. (\\<^isup>+x. f x * indicator A x \M)\" interpret f: measure_space ?fM using f by (rule measure_space_density) simp diff -r f82020ca3248 -r 3e8a2464f607 src/HOL/Probability/ex/Dining_Cryptographers.thy --- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Wed Dec 07 14:00:02 2011 +0000 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Wed Dec 07 16:06:08 2011 +0000 @@ -22,11 +22,8 @@ by (simp_all add: M_def) sublocale finite_space \ finite_measure_space M -proof (rule finite_measure_spaceI) - fix A B :: "'a set" assume "A \ B = {}" "A \ space M" "B \ space M" - then show "measure M (A \ 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 \ information_space M 2 by default (simp_all add: M_def one_ereal_def) diff -r f82020ca3248 -r 3e8a2464f607 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Dec 07 14:00:02 2011 +0000 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Dec 07 16:06:08 2011 +0000 @@ -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 diff -r f82020ca3248 -r 3e8a2464f607 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 07 14:00:02 2011 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 07 16:06:08 2011 +0000 @@ -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, diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/README --- a/src/Tools/Metis/README Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/README Wed Dec 07 16:06:08 2011 +0000 @@ -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 diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/metis.ML --- a/src/Tools/Metis/metis.ML Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/metis.ML Wed Dec 07 16:06:08 2011 +0000 @@ -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 diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Active.sml --- a/src/Tools/Metis/src/Active.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Active.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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 diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/ElementSet.sig --- a/src/Tools/Metis/src/ElementSet.sig Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/ElementSet.sig Wed Dec 07 16:06:08 2011 +0000 @@ -12,6 +12,10 @@ type element +val compareElement : element * element -> order + +val equalElement : element -> element -> bool + (* ------------------------------------------------------------------------- *) (* A type of finite sets. *) (* ------------------------------------------------------------------------- *) diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/ElementSet.sml --- a/src/Tools/Metis/src/ElementSet.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/ElementSet.sml Wed Dec 07 16:06:08 2011 +0000 @@ -16,6 +16,10 @@ type element = KM.key; +val compareElement = KM.compareKey; + +val equalElement = KM.equalKey; + (* ------------------------------------------------------------------------- *) (* A type of finite sets. *) (* ------------------------------------------------------------------------- *) diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Formula.sml --- a/src/Tools/Metis/src/Formula.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Formula.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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)); diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/KeyMap.sig --- a/src/Tools/Metis/src/KeyMap.sig Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/KeyMap.sig Wed Dec 07 16:06:08 2011 +0000 @@ -12,6 +12,10 @@ type key +val compareKey : key * key -> order + +val equalKey : key -> key -> bool + (* ------------------------------------------------------------------------- *) (* A type of finite maps. *) (* ------------------------------------------------------------------------- *) diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Model.sml --- a/src/Tools/Metis/src/Model.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Model.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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; diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/NameArity.sml --- a/src/Tools/Metis/src/NameArity.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/NameArity.sml Wed Dec 07 16:06:08 2011 +0000 @@ -44,7 +44,7 @@ (* ------------------------------------------------------------------------- *) fun pp (n,i) = - Print.blockProgram Print.Inconsistent 0 + Print.inconsistentBlock 0 [Name.pp n, Print.ppString "/", Print.ppInt i]; diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Normalize.sml --- a/src/Tools/Metis/src/Normalize.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Normalize.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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; diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Options.sml --- a/src/Tools/Metis/src/Options.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Options.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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 diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Parse.sml --- a/src/Tools/Metis/src/Parse.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Parse.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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 diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/PortableMosml.sml --- a/src/Tools/Metis/src/PortableMosml.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/PortableMosml.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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 diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Print.sig --- a/src/Tools/Metis/src/Print.sig Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Print.sig Wed Dec 07 16:06:08 2011 +0000 @@ -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 diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Print.sml --- a/src/Tools/Metis/src/Print.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Print.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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"); diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Proof.sml --- a/src/Tools/Metis/src/Proof.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Proof.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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 = diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Rewrite.sml --- a/src/Tools/Metis/src/Rewrite.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Rewrite.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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], diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Stream.sml --- a/src/Tools/Metis/src/Stream.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Stream.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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; diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Term.sml --- a/src/Tools/Metis/src/Term.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Term.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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] diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Thm.sml --- a/src/Tools/Metis/src/Thm.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Thm.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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; diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Tptp.sml --- a/src/Tools/Metis/src/Tptp.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Tptp.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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); diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/Useful.sml --- a/src/Tools/Metis/src/Useful.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/Useful.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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} = diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/metis.sml --- a/src/Tools/Metis/src/metis.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/metis.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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 diff -r f82020ca3248 -r 3e8a2464f607 src/Tools/Metis/src/selftest.sml --- a/src/Tools/Metis/src/selftest.sml Wed Dec 07 14:00:02 2011 +0000 +++ b/src/Tools/Metis/src/selftest.sml Wed Dec 07 16:06:08 2011 +0000 @@ -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]