--- a/NEWS Mon Mar 16 15:30:00 2015 +0000
+++ b/NEWS Tue Mar 17 12:23:56 2015 +0000
@@ -178,6 +178,14 @@
is invoked). The solution is to specify the case rule explicitly
(e.g. "cases w rule: widget.exhaust").
INCOMPATIBILITY.
+ - Renamed theories:
+ BNF_Comp ~> BNF_Composition
+ BNF_FP_Base ~> BNF_Fixpoint_Base
+ BNF_GFP ~> BNF_Greatest_Fixpoint
+ BNF_LFP ~> BNF_Least_Fixpoint
+ BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions
+ Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions
+ INCOMPATIBILITY.
* Old datatype package:
- The old 'datatype' command has been renamed 'old_datatype', and
--- a/src/HOL/Bali/DeclConcepts.thy Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/Bali/DeclConcepts.thy Tue Mar 17 12:23:56 2015 +0000
@@ -368,7 +368,7 @@
class) to a qualified member declaration: @{text method} *}
definition
- method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
+ "method" :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
where "method sig m = (declclass m, mdecl (sig, mthd m))"
lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
--- a/src/HOL/Codegenerator_Test/Candidates.thy Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Tue Mar 17 12:23:56 2015 +0000
@@ -28,6 +28,13 @@
code_pred sublist .
+lemma [code]: -- {* for the generic factorial function *}
+ fixes XXX :: "'a :: semiring_numeral_div"
+ shows
+ "fact 0 = (1 :: 'a)"
+ "fact (Suc n) = (of_nat (Suc n) * fact n :: 'a)"
+ by simp_all
+
code_reserved SML upto -- {* avoid popular infix *}
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Inequalities.thy Tue Mar 17 12:23:56 2015 +0000
@@ -0,0 +1,97 @@
+(* Title: Inequalities
+ Author: Tobias Nipkow
+ Author: Johannes Hölzl
+*)
+
+theory Inequalities
+ imports Real_Vector_Spaces
+begin
+
+lemma setsum_triangle_reindex:
+ fixes n :: nat
+ shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
+ apply (simp add: setsum.Sigma)
+ apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
+ apply auto
+ done
+
+lemma gauss_sum_div2: "(2::'a::semiring_div) \<noteq> 0 \<Longrightarrow>
+ setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)"
+using gauss_sum[where n=n and 'a = 'a,symmetric] by auto
+
+lemma Setsum_Icc_int: assumes "0 \<le> m" and "(m::int) \<le> n"
+shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
+proof-
+ { fix k::int assume "k\<ge>0"
+ hence "\<Sum> {1..k::int} = k * (k+1) div 2"
+ by (rule gauss_sum_div2[where 'a = int, transferred]) simp
+ } note 1 = this
+ have "{m..n} = {0..n} - {0..m-1}" using `m\<ge>0` by auto
+ hence "\<Sum>{m..n} = \<Sum>{0..n} - \<Sum>{0..m-1}" using assms
+ by (force intro!: setsum_diff)
+ also have "{0..n} = {0} Un {1..n}" using assms by auto
+ also have "\<Sum>({0} \<union> {1..n}) = \<Sum>{1..n}" by(simp add: setsum.union_disjoint)
+ also have "\<dots> = n * (n+1) div 2" by(rule 1[OF order_trans[OF assms]])
+ also have "{0..m-1} = (if m=0 then {} else {0} Un {1..m-1})"
+ using assms by auto
+ also have "\<Sum> \<dots> = m*(m-1) div 2" using `m\<ge>0` by(simp add: 1 mult.commute)
+ also have "n*(n+1) div 2 - m*(m-1) div 2 = (n*(n+1) - m*(m-1)) div 2"
+ apply(subgoal_tac "even(n*(n+1)) \<and> even(m*(m-1))")
+ by (auto (*simp: even_def[symmetric]*))
+ finally show ?thesis .
+qed
+
+lemma Setsum_Icc_nat: assumes "(m::nat) \<le> n"
+shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
+proof -
+ have "m*(m-1) \<le> n*(n + 1)"
+ using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
+ hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
+ by (auto simp add: Setsum_Icc_int[transferred, OF _ assms] zdiv_int int_mult
+ split: zdiff_int_split)
+ thus ?thesis by simp
+qed
+
+lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n"
+shows "\<Sum> {m..<n} = (n*(n-1) - m*(m-1)) div 2"
+proof cases
+ assume "m < n"
+ hence "{m..<n} = {m..n-1}" by auto
+ hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp
+ also have "\<dots> = (n*(n-1) - m*(m-1)) div 2"
+ using assms `m < n` by (simp add: Setsum_Icc_nat mult.commute)
+ finally show ?thesis .
+next
+ assume "\<not> m < n" with assms show ?thesis by simp
+qed
+
+lemma Chebyshev_sum_upper:
+ fixes a b::"nat \<Rightarrow> 'a::linordered_idom"
+ assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j"
+ assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> b i \<ge> b j"
+ shows "of_nat n * (\<Sum>k=0..<n. a k * b k) \<le> (\<Sum>k=0..<n. a k) * (\<Sum>k=0..<n. b k)"
+proof -
+ let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))"
+ have "2 * (of_nat n * (\<Sum>j=0..<n. (a j * b j)) - (\<Sum>j=0..<n. b j) * (\<Sum>k=0..<n. a k)) = ?S"
+ unfolding one_add_one[symmetric] algebra_simps
+ by (simp add: algebra_simps setsum_subtractf setsum.distrib setsum.commute[of "\<lambda>i j. a i * b j"] setsum_right_distrib)
+ also
+ { fix i j::nat assume "i<n" "j<n"
+ hence "a i - a j \<le> 0 \<and> b i - b j \<ge> 0 \<or> a i - a j \<ge> 0 \<and> b i - b j \<le> 0"
+ using assms by (cases "i \<le> j") (auto simp: algebra_simps)
+ } hence "?S \<le> 0"
+ by (auto intro!: setsum_nonpos simp: mult_le_0_iff)
+ (auto simp: field_simps)
+ finally show ?thesis by (simp add: algebra_simps)
+qed
+
+lemma Chebyshev_sum_upper_nat:
+ fixes a b :: "nat \<Rightarrow> nat"
+ shows "(\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> a i \<le> a j) \<Longrightarrow>
+ (\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> b i \<ge> b j) \<Longrightarrow>
+ n * (\<Sum>i=0..<n. a i * b i) \<le> (\<Sum>i=0..<n. a i) * (\<Sum>i=0..<n. b i)"
+using Chebyshev_sum_upper[where 'a=real, of n a b]
+by (simp del: real_of_nat_mult real_of_nat_setsum
+ add: real_of_nat_mult[symmetric] real_of_nat_setsum[symmetric] real_of_nat_def[symmetric])
+
+end
--- a/src/HOL/Library/Extended_Real.thy Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/Library/Extended_Real.thy Tue Mar 17 12:23:56 2015 +0000
@@ -2602,6 +2602,50 @@
(is "?lhs \<longleftrightarrow> ?rhs")
unfolding le_Liminf_iff eventually_sequentially ..
+lemma Liminf_add_le:
+ fixes f g :: "_ \<Rightarrow> ereal"
+ assumes F: "F \<noteq> bot"
+ assumes ev: "eventually (\<lambda>x. 0 \<le> f x) F" "eventually (\<lambda>x. 0 \<le> g x) F"
+ shows "Liminf F f + Liminf F g \<le> Liminf F (\<lambda>x. f x + g x)"
+ unfolding Liminf_def
+proof (subst SUP_ereal_add_left[symmetric])
+ let ?F = "{P. eventually P F}"
+ let ?INF = "\<lambda>P g. INFIMUM (Collect P) g"
+ show "?F \<noteq> {}"
+ by (auto intro: eventually_True)
+ show "(SUP P:?F. ?INF P g) \<noteq> - \<infinity>"
+ unfolding bot_ereal_def[symmetric] SUP_bot_conv INF_eq_bot_iff
+ by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
+ have "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. (SUP P':?F. ?INF P f + ?INF P' g))"
+ proof (safe intro!: SUP_mono bexI[of _ "\<lambda>x. P x \<and> 0 \<le> f x" for P])
+ fix P let ?P' = "\<lambda>x. P x \<and> 0 \<le> f x"
+ assume "eventually P F"
+ with ev show "eventually ?P' F"
+ by eventually_elim auto
+ have "?INF P f + (SUP P:?F. ?INF P g) \<le> ?INF ?P' f + (SUP P:?F. ?INF P g)"
+ by (intro ereal_add_mono INF_mono) auto
+ also have "\<dots> = (SUP P':?F. ?INF ?P' f + ?INF P' g)"
+ proof (rule SUP_ereal_add_right[symmetric])
+ show "INFIMUM {x. P x \<and> 0 \<le> f x} f \<noteq> - \<infinity>"
+ unfolding bot_ereal_def[symmetric] INF_eq_bot_iff
+ by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
+ qed fact
+ finally show "?INF P f + (SUP P:?F. ?INF P g) \<le> (SUP P':?F. ?INF ?P' f + ?INF P' g)" .
+ qed
+ also have "\<dots> \<le> (SUP P:?F. INF x:Collect P. f x + g x)"
+ proof (safe intro!: SUP_least)
+ fix P Q assume *: "eventually P F" "eventually Q F"
+ show "?INF P f + ?INF Q g \<le> (SUP P:?F. INF x:Collect P. f x + g x)"
+ proof (rule SUP_upper2)
+ show "(\<lambda>x. P x \<and> Q x) \<in> ?F"
+ using * by (auto simp: eventually_conj)
+ show "?INF P f + ?INF Q g \<le> (INF x:{x. P x \<and> Q x}. f x + g x)"
+ by (intro INF_greatest ereal_add_mono) (auto intro: INF_lower)
+ qed
+ qed
+ finally show "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. INF x:Collect P. f x + g x)" .
+qed
+
subsubsection {* Tests for code generator *}
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Tue Mar 17 12:23:56 2015 +0000
@@ -429,14 +429,14 @@
fixes G ("\<Gamma>") and Phi ("\<Phi>")
assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"
assumes is_class: "is_class \<Gamma> C"
- and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
+ and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
and m: "m \<noteq> init"
defines start: "s \<equiv> start_state \<Gamma> C m"
assumes s: "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> t"
shows "t \<noteq> TypeError"
proof -
- from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+ from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
unfolding start by (rule BV_correct_initial)
from wt this s show ?thesis by (rule no_type_errors)
qed
@@ -461,12 +461,12 @@
fixes G ("\<Gamma>") and Phi ("\<Phi>")
assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"
assumes is_class: "is_class \<Gamma> C"
- and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
+ and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
and m: "m \<noteq> init"
defines start: "s \<equiv> start_state \<Gamma> C m"
shows "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s \<midarrow>jvm\<rightarrow> t"
proof -
- from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+ from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
unfolding start by (rule BV_correct_initial)
with wt show ?thesis by (rule welltyped_commutes)
qed
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Mar 17 12:23:56 2015 +0000
@@ -811,7 +811,7 @@
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wtprog: "wt_jvm_prog G phi"
- assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
+ assume "method": "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
assume ins: "ins ! pc = Invoke C' mn pTs"
assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
@@ -823,7 +823,7 @@
wfprog: "wf_prog wfmb G"
by (simp add: wt_jvm_prog_def)
- from ins method approx
+ from ins "method" approx
obtain s where
heap_ok: "G\<turnstile>h hp\<surd>" and
prealloc:"preallocated hp" and
@@ -880,7 +880,7 @@
from stk' l_o l
have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp
- with state' method ins no_xcp oX_conf
+ with state' "method" ins no_xcp oX_conf
obtain ref where oX_Addr: "oX = Addr ref"
by (auto simp add: raise_system_xcpt_def dest: conf_RefTD)
@@ -922,7 +922,7 @@
from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def)
- with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp
+ with oX_Addr oX_pos state' "method" ins stk' l_o l loc obj_ty mD no_xcp
have state'_val:
"state' =
Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' undefined,
@@ -972,7 +972,7 @@
show ?thesis by (simp add: correct_frame_def)
qed
- from state'_val heap_ok mD'' ins method phi_pc s X' l mX
+ from state'_val heap_ok mD'' ins "method" phi_pc s X' l mX
frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc and l
show ?thesis
apply (simp add: correct_state_def)
--- a/src/HOL/MicroJava/J/TypeRel.thy Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Mar 17 12:23:56 2015 +0000
@@ -177,7 +177,7 @@
qed
consts
- method :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
+ "method" :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
field :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty )" (* ###curry *)
fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
--- a/src/HOL/NSA/Examples/NSPrimes.thy Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/NSA/Examples/NSPrimes.thy Tue Mar 17 12:23:56 2015 +0000
@@ -13,8 +13,6 @@
text{*These can be used to derive an alternative proof of the infinitude of
primes by considering a property of nonstandard sets.*}
-declare dvd_def [transfer_refold]
-
definition
starprime :: "hypnat set" where
[transfer_unfold]: "starprime = ( *s* {p. prime p})"
--- a/src/HOL/NSA/StarDef.thy Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/NSA/StarDef.thy Tue Mar 17 12:23:56 2015 +0000
@@ -848,6 +848,14 @@
instance star :: (semiring_1) semiring_1 ..
instance star :: (comm_semiring_1) comm_semiring_1 ..
+declare dvd_def [transfer_refold]
+
+instance star :: (semiring_dvd) semiring_dvd
+apply intro_classes
+apply(transfer, rule dvd_add_times_triv_left_iff)
+apply(transfer, erule (1) dvd_addD)
+done
+
instance star :: (no_zero_divisors) no_zero_divisors
by (intro_classes, transfer, rule no_zero_divisors)
@@ -857,6 +865,16 @@
instance star :: (comm_ring) comm_ring ..
instance star :: (ring_1) ring_1 ..
instance star :: (comm_ring_1) comm_ring_1 ..
+instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors ..
+instance star :: (semiring_div) semiring_div
+apply intro_classes
+apply(transfer, rule mod_div_equality)
+apply(transfer, rule div_by_0)
+apply(transfer, rule div_0)
+apply(transfer, erule div_mult_self1)
+apply(transfer, erule div_mult_mult1)
+done
+
instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
instance star :: (idom) idom ..
@@ -924,7 +942,6 @@
instance star :: (linordered_field) linordered_field ..
instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero ..
-
subsection {* Power *}
lemma star_power_def [transfer_unfold]:
@@ -1006,6 +1023,36 @@
instance star :: (ring_char_0) ring_char_0 ..
+instance star :: (semiring_parity) semiring_parity
+apply intro_classes
+apply(transfer, rule odd_one)
+apply(transfer, erule (1) odd_even_add)
+apply(transfer, erule even_multD)
+apply(transfer, erule odd_ex_decrement)
+done
+
+instance star :: (semiring_div_parity) semiring_div_parity
+apply intro_classes
+apply(transfer, rule parity)
+apply(transfer, rule one_mod_two_eq_one)
+apply(transfer, rule zero_not_eq_two)
+done
+
+instance star :: (semiring_numeral_div) semiring_numeral_div
+apply intro_classes
+apply(transfer, erule semiring_numeral_div_class.diff_invert_add1)
+apply(transfer, erule semiring_numeral_div_class.le_add_diff_inverse2)
+apply(transfer, rule semiring_numeral_div_class.mult_div_cancel)
+apply(transfer, erule (1) semiring_numeral_div_class.div_less)
+apply(transfer, erule (1) semiring_numeral_div_class.mod_less)
+apply(transfer, erule (1) semiring_numeral_div_class.div_positive)
+apply(transfer, erule semiring_numeral_div_class.mod_less_eq_dividend)
+apply(transfer, erule semiring_numeral_div_class.pos_mod_bound)
+apply(transfer, erule semiring_numeral_div_class.pos_mod_sign)
+apply(transfer, erule semiring_numeral_div_class.mod_mult2_eq)
+apply(transfer, erule semiring_numeral_div_class.div_mult2_eq)
+apply(transfer, rule discrete)
+done
subsection {* Finite class *}
--- a/src/HOL/NanoJava/TypeRel.thy Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/NanoJava/TypeRel.thy Tue Mar 17 12:23:56 2015 +0000
@@ -108,7 +108,7 @@
done
--{* Methods of a class, with inheritance and hiding *}
-definition method :: "cname => (mname \<rightharpoonup> methd)" where
+definition "method" :: "cname => (mname \<rightharpoonup> methd)" where
"method C \<equiv> class_rec C methods"
lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
--- a/src/HOL/Probability/Probability_Mass_Function.thy Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Mar 17 12:23:56 2015 +0000
@@ -793,6 +793,9 @@
subsection \<open> Conditional Probabilities \<close>
+lemma measure_pmf_zero_iff: "measure (measure_pmf p) s = 0 \<longleftrightarrow> set_pmf p \<inter> s = {}"
+ by (subst measure_pmf.prob_eq_0) (auto simp: AE_measure_pmf_iff)
+
context
fixes p :: "'a pmf" and s :: "'a set"
assumes not_empty: "set_pmf p \<inter> s \<noteq> {}"
@@ -854,32 +857,22 @@
qed
lemma bind_cond_pmf_cancel:
- assumes in_S: "\<And>x. x \<in> set_pmf p \<Longrightarrow> x \<in> S x" "\<And>x. x \<in> set_pmf q \<Longrightarrow> x \<in> S x"
- assumes S_eq: "\<And>x y. x \<in> S y \<Longrightarrow> S x = S y"
- and same: "\<And>x. measure (measure_pmf p) (S x) = measure (measure_pmf q) (S x)"
- shows "bind_pmf p (\<lambda>x. cond_pmf q (S x)) = q" (is "?lhs = _")
+ assumes [simp]: "\<And>x. x \<in> set_pmf p \<Longrightarrow> set_pmf q \<inter> {y. R x y} \<noteq> {}"
+ assumes [simp]: "\<And>y. y \<in> set_pmf q \<Longrightarrow> set_pmf p \<inter> {x. R x y} \<noteq> {}"
+ assumes [simp]: "\<And>x y. x \<in> set_pmf p \<Longrightarrow> y \<in> set_pmf q \<Longrightarrow> R x y \<Longrightarrow> measure q {y. R x y} = measure p {x. R x y}"
+ shows "bind_pmf p (\<lambda>x. cond_pmf q {y. R x y}) = q"
proof (rule pmf_eqI)
- { fix x
- assume "x \<in> set_pmf p"
- hence "set_pmf p \<inter> (S x) \<noteq> {}" using in_S by auto
- hence "measure (measure_pmf p) (S x) \<noteq> 0"
- by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff)
- with same have "measure (measure_pmf q) (S x) \<noteq> 0" by simp
- hence "set_pmf q \<inter> S x \<noteq> {}"
- by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
- note [simp] = this
-
- fix z
- have pmf_q_z: "z \<notin> S z \<Longrightarrow> pmf q z = 0"
- by(erule contrapos_np)(simp add: pmf_eq_0_set_pmf in_S)
-
- have "ereal (pmf ?lhs z) = \<integral>\<^sup>+ x. ereal (pmf (cond_pmf q (S x)) z) \<partial>measure_pmf p"
- by(simp add: ereal_pmf_bind)
- also have "\<dots> = \<integral>\<^sup>+ x. ereal (pmf q z / measure p (S z)) * indicator (S z) x \<partial>measure_pmf p"
- by(rule nn_integral_cong_AE)(auto simp add: AE_measure_pmf_iff pmf_cond same pmf_q_z in_S dest!: S_eq split: split_indicator)
- also have "\<dots> = pmf q z" using pmf_nonneg[of q z]
- by (subst nn_integral_cmult)(auto simp add: measure_nonneg measure_pmf.emeasure_eq_measure same measure_pmf.prob_eq_0 AE_measure_pmf_iff pmf_eq_0_set_pmf in_S)
- finally show "pmf ?lhs z = pmf q z" by simp
+ fix i
+ have "ereal (pmf (bind_pmf p (\<lambda>x. cond_pmf q {y. R x y})) i) =
+ (\<integral>\<^sup>+x. ereal (pmf q i / measure p {x. R x i}) * ereal (indicator {x. R x i} x) \<partial>p)"
+ by (auto simp add: ereal_pmf_bind AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf intro!: nn_integral_cong_AE)
+ also have "\<dots> = (pmf q i * measure p {x. R x i}) / measure p {x. R x i}"
+ by (simp add: pmf_nonneg measure_nonneg zero_ereal_def[symmetric] ereal_indicator
+ nn_integral_cmult measure_pmf.emeasure_eq_measure)
+ also have "\<dots> = pmf q i"
+ by (cases "pmf q i = 0") (simp_all add: pmf_eq_0_set_pmf measure_measure_pmf_not_zero)
+ finally show "pmf (bind_pmf p (\<lambda>x. cond_pmf q {y. R x y})) i = pmf q i"
+ by simp
qed
subsection \<open> Relator \<close>
@@ -891,6 +884,136 @@
map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk>
\<Longrightarrow> rel_pmf R p q"
+lemma rel_pmfI:
+ assumes R: "rel_set R (set_pmf p) (set_pmf q)"
+ assumes eq: "\<And>x y. x \<in> set_pmf p \<Longrightarrow> y \<in> set_pmf q \<Longrightarrow> R x y \<Longrightarrow>
+ measure p {x. R x y} = measure q {y. R x y}"
+ shows "rel_pmf R p q"
+proof
+ let ?pq = "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q {y. R x y}) (\<lambda>y. return_pmf (x, y)))"
+ have "\<And>x. x \<in> set_pmf p \<Longrightarrow> set_pmf q \<inter> {y. R x y} \<noteq> {}"
+ using R by (auto simp: rel_set_def)
+ then show "\<And>x y. (x, y) \<in> set_pmf ?pq \<Longrightarrow> R x y"
+ by auto
+ show "map_pmf fst ?pq = p"
+ by (simp add: map_bind_pmf map_return_pmf bind_return_pmf')
+
+ show "map_pmf snd ?pq = q"
+ using R eq
+ apply (simp add: bind_cond_pmf_cancel map_bind_pmf map_return_pmf bind_return_pmf')
+ apply (rule bind_cond_pmf_cancel)
+ apply (auto simp: rel_set_def)
+ done
+qed
+
+lemma rel_pmf_imp_rel_set: "rel_pmf R p q \<Longrightarrow> rel_set R (set_pmf p) (set_pmf q)"
+ by (force simp add: rel_pmf.simps rel_set_def)
+
+lemma rel_pmfD_measure:
+ assumes rel_R: "rel_pmf R p q" and R: "\<And>a b. R a b \<Longrightarrow> R a y \<longleftrightarrow> R x b"
+ assumes "x \<in> set_pmf p" "y \<in> set_pmf q"
+ shows "measure p {x. R x y} = measure q {y. R x y}"
+proof -
+ from rel_R obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
+ and eq: "p = map_pmf fst pq" "q = map_pmf snd pq"
+ by (auto elim: rel_pmf.cases)
+ have "measure p {x. R x y} = measure pq {x. R (fst x) y}"
+ by (simp add: eq map_pmf_rep_eq measure_distr)
+ also have "\<dots> = measure pq {y. R x (snd y)}"
+ by (intro measure_pmf.finite_measure_eq_AE)
+ (auto simp: AE_measure_pmf_iff R dest!: pq)
+ also have "\<dots> = measure q {y. R x y}"
+ by (simp add: eq map_pmf_rep_eq measure_distr)
+ finally show "measure p {x. R x y} = measure q {y. R x y}" .
+qed
+
+lemma rel_pmf_iff_measure:
+ assumes "symp R" "transp R"
+ shows "rel_pmf R p q \<longleftrightarrow>
+ rel_set R (set_pmf p) (set_pmf q) \<and>
+ (\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y})"
+ by (safe intro!: rel_pmf_imp_rel_set rel_pmfI)
+ (auto intro!: rel_pmfD_measure dest: sympD[OF \<open>symp R\<close>] transpD[OF \<open>transp R\<close>])
+
+lemma quotient_rel_set_disjoint:
+ "equivp R \<Longrightarrow> C \<in> UNIV // {(x, y). R x y} \<Longrightarrow> rel_set R A B \<Longrightarrow> A \<inter> C = {} \<longleftrightarrow> B \<inter> C = {}"
+ using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C]
+ by (auto 0 0 simp: equivp_equiv rel_set_def set_eq_iff elim: equivpE)
+ (blast dest: equivp_symp)+
+
+lemma quotientD: "equiv X R \<Longrightarrow> A \<in> X // R \<Longrightarrow> x \<in> A \<Longrightarrow> A = R `` {x}"
+ by (metis Image_singleton_iff equiv_class_eq_iff quotientE)
+
+lemma rel_pmf_iff_equivp:
+ assumes "equivp R"
+ shows "rel_pmf R p q \<longleftrightarrow> (\<forall>C\<in>UNIV // {(x, y). R x y}. measure p C = measure q C)"
+ (is "_ \<longleftrightarrow> (\<forall>C\<in>_//?R. _)")
+proof (subst rel_pmf_iff_measure, safe)
+ show "symp R" "transp R"
+ using assms by (auto simp: equivp_reflp_symp_transp)
+next
+ fix C assume C: "C \<in> UNIV // ?R" and R: "rel_set R (set_pmf p) (set_pmf q)"
+ assume eq: "\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y}"
+
+ show "measure p C = measure q C"
+ proof cases
+ assume "p \<inter> C = {}"
+ moreover then have "q \<inter> C = {}"
+ using quotient_rel_set_disjoint[OF assms C R] by simp
+ ultimately show ?thesis
+ unfolding measure_pmf_zero_iff[symmetric] by simp
+ next
+ assume "p \<inter> C \<noteq> {}"
+ moreover then have "q \<inter> C \<noteq> {}"
+ using quotient_rel_set_disjoint[OF assms C R] by simp
+ ultimately obtain x y where in_set: "x \<in> set_pmf p" "y \<in> set_pmf q" and in_C: "x \<in> C" "y \<in> C"
+ by auto
+ then have "R x y"
+ using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms
+ by (simp add: equivp_equiv)
+ with in_set eq have "measure p {x. R x y} = measure q {y. R x y}"
+ by auto
+ moreover have "{y. R x y} = C"
+ using assms `x \<in> C` C quotientD[of UNIV ?R C x] by (simp add: equivp_equiv)
+ moreover have "{x. R x y} = C"
+ using assms `y \<in> C` C quotientD[of UNIV "?R" C y] sympD[of R]
+ by (auto simp add: equivp_equiv elim: equivpE)
+ ultimately show ?thesis
+ by auto
+ qed
+next
+ assume eq: "\<forall>C\<in>UNIV // ?R. measure p C = measure q C"
+ show "rel_set R (set_pmf p) (set_pmf q)"
+ unfolding rel_set_def
+ proof safe
+ fix x assume x: "x \<in> set_pmf p"
+ have "{y. R x y} \<in> UNIV // ?R"
+ by (auto simp: quotient_def)
+ with eq have *: "measure q {y. R x y} = measure p {y. R x y}"
+ by auto
+ have "measure q {y. R x y} \<noteq> 0"
+ using x assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp)
+ then show "\<exists>y\<in>set_pmf q. R x y"
+ unfolding measure_pmf_zero_iff by auto
+ next
+ fix y assume y: "y \<in> set_pmf q"
+ have "{x. R x y} \<in> UNIV // ?R"
+ using assms by (auto simp: quotient_def dest: equivp_symp)
+ with eq have *: "measure p {x. R x y} = measure q {x. R x y}"
+ by auto
+ have "measure p {x. R x y} \<noteq> 0"
+ using y assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp)
+ then show "\<exists>x\<in>set_pmf p. R x y"
+ unfolding measure_pmf_zero_iff by auto
+ qed
+
+ fix x y assume "x \<in> set_pmf p" "y \<in> set_pmf q" "R x y"
+ have "{y. R x y} \<in> UNIV // ?R" "{x. R x y} = {y. R x y}"
+ using assms `R x y` by (auto simp: quotient_def dest: equivp_symp equivp_transp)
+ with eq show "measure p {x. R x y} = measure q {y. R x y}"
+ by auto
+qed
+
bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf
proof -
show "map_pmf id = id" by (rule map_pmf_id)
@@ -919,7 +1042,7 @@
and x: "x \<in> set_pmf p"
thus "f x = g x" by simp }
- fix R :: "'a => 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
+ fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
{ fix p q r
assume pq: "rel_pmf R p q"
and qr:"rel_pmf S q r"
@@ -928,8 +1051,8 @@
from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
- def pr \<equiv> "bind_pmf pq (\<lambda>(x, y). bind_pmf (cond_pmf qr {(y', z). y' = y}) (\<lambda>(y', z). return_pmf (x, z)))"
- have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {(y', z). y' = y} \<noteq> {}"
+ def pr \<equiv> "bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\<lambda>yz. return_pmf (fst xy, snd yz)))"
+ have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}"
by (force simp: q')
have "rel_pmf (R OO S) p r"
@@ -940,11 +1063,11 @@
with pq qr show "(R OO S) x z"
by blast
next
- have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {(y', z). y' = y}))"
- by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_return_pmf)
+ have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))"
+ by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_return_pmf map_pmf_comp)
then show "map_pmf snd pr = r"
- unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) auto
- qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf map_pmf_def[symmetric] p) }
+ unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute)
+ qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf map_pmf_def[symmetric] p map_pmf_comp) }
then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
by(auto simp add: le_fun_def)
qed (fact natLeq_card_order natLeq_cinfinite)+
@@ -1137,46 +1260,31 @@
assumes 2: "rel_pmf R q p"
and refl: "reflp R" and trans: "transp R"
shows "rel_pmf (inf R R\<inverse>\<inverse>) p q"
-proof
- let ?E = "\<lambda>x. {y. R x y \<and> R y x}"
- let ?\<mu>E = "\<lambda>x. measure q (?E x)"
- { fix x
- have "measure p (?E x) = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})"
- by(auto intro!: arg_cong[where f="measure p"])
- also have "\<dots> = measure p {y. R x y} - measure p {y. R x y \<and> \<not> R y x}"
- by (rule measure_pmf.finite_measure_Diff) auto
- also have "measure p {y. R x y \<and> \<not> R y x} = measure q {y. R x y \<and> \<not> R y x}"
- using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi)
- also have "measure p {y. R x y} = measure q {y. R x y}"
- using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici)
- also have "measure q {y. R x y} - measure q {y. R x y \<and> ~ R y x} =
- measure q ({y. R x y} - {y. R x y \<and> \<not> R y x})"
- by(rule measure_pmf.finite_measure_Diff[symmetric]) auto
- also have "\<dots> = ?\<mu>E x"
- by(auto intro!: arg_cong[where f="measure q"])
- also note calculation }
- note eq = this
+proof (subst rel_pmf_iff_equivp, safe)
+ show "equivp (inf R R\<inverse>\<inverse>)"
+ using trans refl by (auto simp: equivp_reflp_symp_transp intro: sympI transpI reflpI dest: transpD reflpD)
+
+ fix C assume "C \<in> UNIV // {(x, y). inf R R\<inverse>\<inverse> x y}"
+ then obtain x where C: "C = {y. R x y \<and> R y x}"
+ by (auto elim: quotientE)
- def pq \<equiv> "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q (?E x)) (\<lambda>y. return_pmf (x, y)))"
-
- show "map_pmf fst pq = p"
- by(simp add: pq_def map_bind_pmf map_return_pmf bind_return_pmf')
-
- show "map_pmf snd pq = q"
- unfolding pq_def map_bind_pmf map_return_pmf bind_return_pmf' snd_conv
- by(subst bind_cond_pmf_cancel)(auto simp add: reflpD[OF \<open>reflp R\<close>] eq intro: transpD[OF \<open>transp R\<close>])
-
- fix x y
- assume "(x, y) \<in> set_pmf pq"
- moreover
- { assume "x \<in> set_pmf p"
- hence "measure (measure_pmf p) (?E x) \<noteq> 0"
- by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \<open>reflp R\<close>])
- hence "measure (measure_pmf q) (?E x) \<noteq> 0" using eq by simp
- hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}"
- by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
- ultimately show "inf R R\<inverse>\<inverse> x y"
- by (auto simp add: pq_def)
+ let ?R = "\<lambda>x y. R x y \<and> R y x"
+ let ?\<mu>R = "\<lambda>y. measure q {x. ?R x y}"
+ have "measure p {y. ?R x y} = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})"
+ by(auto intro!: arg_cong[where f="measure p"])
+ also have "\<dots> = measure p {y. R x y} - measure p {y. R x y \<and> \<not> R y x}"
+ by (rule measure_pmf.finite_measure_Diff) auto
+ also have "measure p {y. R x y \<and> \<not> R y x} = measure q {y. R x y \<and> \<not> R y x}"
+ using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi)
+ also have "measure p {y. R x y} = measure q {y. R x y}"
+ using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici)
+ also have "measure q {y. R x y} - measure q {y. R x y \<and> \<not> R y x} =
+ measure q ({y. R x y} - {y. R x y \<and> \<not> R y x})"
+ by(rule measure_pmf.finite_measure_Diff[symmetric]) auto
+ also have "\<dots> = ?\<mu>R x"
+ by(auto intro!: arg_cong[where f="measure q"])
+ finally show "measure p C = measure q C"
+ by (simp add: C conj_commute)
qed
lemma rel_pmf_antisym:
--- a/src/HOL/Series.thy Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/Series.thy Tue Mar 17 12:23:56 2015 +0000
@@ -10,8 +10,8 @@
section {* Infinite Series *}
theory Series
-imports Limits
-begin
+imports Limits Inequalities
+begin
subsection {* Definition of infinite summability *}
@@ -576,14 +576,6 @@
@{url "http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm"}
*}
-lemma setsum_triangle_reindex:
- fixes n :: nat
- shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
- apply (simp add: setsum.Sigma)
- apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
- apply auto
- done
-
lemma Cauchy_product_sums:
fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
assumes a: "summable (\<lambda>k. norm (a k))"
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Mar 17 12:23:56 2015 +0000
@@ -2424,7 +2424,7 @@
forall is_some ctrs')
end
in
- ctrss |> map datatype_of_ctrs |> filter_out (null o #2)
+ ctrss |> map datatype_of_ctrs |> filter #3
end
else
[]
--- a/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Tue Mar 17 12:23:56 2015 +0000
@@ -8,6 +8,8 @@
signature BNF_COMP =
sig
+ val bnf_inline_threshold: int Config.T
+
val ID_bnf: BNF_Def.bnf
val DEADID_bnf: BNF_Def.bnf
@@ -54,6 +56,8 @@
open BNF_Tactics
open BNF_Comp_Tactics
+val bnf_inline_threshold = Attrib.setup_config_int @{binding bnf_inline_threshold} (K 5);
+
val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID");
val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID");
@@ -730,12 +734,12 @@
val mk_abs = mk_abs_or_rep range_type;
val mk_rep = mk_abs_or_rep domain_type;
-val smart_max_inline_type_size = 5; (*FUDGE*)
-
-fun maybe_typedef force_out_of_line (b, As, mx) set opt_morphs tac =
+fun maybe_typedef ctxt force_out_of_line (b, As, mx) set opt_morphs tac =
let
+ val threshold = Config.get ctxt bnf_inline_threshold;
val repT = HOLogic.dest_setT (fastype_of set);
- val out_of_line = force_out_of_line orelse Term.size_of_typ repT > smart_max_inline_type_size;
+ val out_of_line = force_out_of_line orelse
+ (threshold >= 0 andalso Term.size_of_typ repT > threshold);
in
if out_of_line then
typedef (b, As, mx) set opt_morphs tac
@@ -769,7 +773,7 @@
val T_bind = qualify b;
val TA_params = Term.add_tfreesT repTA (if has_live_phantoms then As' else []);
val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
- maybe_typedef has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
+ maybe_typedef lthy has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
(fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
val repTB = mk_T_of_bnf Ds Bs bnf;
@@ -799,7 +803,7 @@
val all_deads = map TFree (fold Term.add_tfreesT Ds []);
val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) =
- maybe_typedef false (bdT_bind, params, NoSyn)
+ maybe_typedef lthy false (bdT_bind, params, NoSyn)
(HOLogic.mk_UNIV bd_repT) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) =
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Mar 17 12:23:56 2015 +0000
@@ -189,12 +189,6 @@
map (cterm_instantiate_pos (map SOME (passives @ actives))) ctor_rec_transfers;
val total_n = Integer.sum ns;
val True = @{term True};
- fun magic eq xs xs' = Subgoal.FOCUS (fn {prems, ...} =>
- let
- val thm = prems
- |> Ctr_Sugar_Util.permute_like eq xs xs'
- |> Library.foldl1 (fn (acc, elem) => elem RS (acc RS @{thm rel_funD}))
- in HEADGOAL (rtac thm) end)
in
HEADGOAL Goal.conjunction_tac THEN
EVERY (map (fn ctor_rec_transfer =>
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Mar 17 12:23:56 2015 +0000
@@ -155,6 +155,7 @@
val mk_Inl: typ -> term -> term
val mk_Inr: typ -> term -> term
+ val mk_sumprod_balanced: typ -> int -> int -> term list -> term
val mk_absumprod: typ -> term -> int -> int -> term list -> term
val dest_sumT: typ -> typ * typ
@@ -414,9 +415,11 @@
val mk_tuple_balanced = mk_tuple1_balanced [];
+fun mk_sumprod_balanced T n k ts = Sum_Tree.mk_inj T n k (mk_tuple_balanced ts);
+
fun mk_absumprod absT abs0 n k ts =
let val abs = mk_abs absT abs0;
- in abs $ Sum_Tree.mk_inj (domain_type (fastype_of abs)) n k (mk_tuple_balanced ts) end;
+ in abs $ mk_sumprod_balanced (domain_type (fastype_of abs)) n k ts end;
fun mk_case_sum (f, g) =
let
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Mar 17 12:23:56 2015 +0000
@@ -44,6 +44,21 @@
fp_nesting_map_comps: thm list,
ctr_specs: corec_ctr_spec list}
+ val fold_rev_let_if_case: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list ->
+ term -> 'a -> 'a
+ val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
+ typ list -> term -> term
+ val massage_nested_corec_call: Proof.context -> (term -> bool) ->
+ (typ list -> typ -> typ -> term -> term) -> typ list -> typ -> term -> term
+ val expand_to_ctr_term: Proof.context -> string -> typ list -> term -> term
+ val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) ->
+ typ list -> term -> term
+ val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
+ typ list -> term -> 'a -> 'a
+ val case_thms_of_term: Proof.context -> term ->
+ thm list * thm list * thm list * thm list * thm list
+ val map_thms_of_type: Proof.context -> typ -> thm list
+
val corec_specs_of: binding list -> typ list -> typ list -> term list ->
(term * term list list) list list -> local_theory ->
corec_spec list * typ list * thm * thm * thm list * thm list * (Token.src list * Token.src list)
@@ -160,7 +175,6 @@
val s_not_conj = conjuncts_s o s_not o mk_conjs;
fun propagate_unit_pos u cs = if member (op aconv) cs u then [@{const False}] else cs;
-
fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs;
fun propagate_units css =
@@ -421,9 +435,9 @@
end)
| _ => not_codatatype ctxt res_T);
-fun map_thms_of_typ ctxt (Type (s, _)) =
+fun map_thms_of_type ctxt (Type (s, _)) =
(case fp_sugar_of ctxt s of SOME {fp_bnf_sugar = {map_thms, ...}, ...} => map_thms | NONE => [])
- | map_thms_of_typ _ _ = [];
+ | map_thms_of_type _ _ = [];
structure GFP_Rec_Sugar_Plugin = Plugin(type T = fp_rec_sugar);
@@ -533,7 +547,7 @@
co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
{T = T, corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec,
exhaust_discs = exhaust_discs, sel_defs = sel_defs,
- fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs,
+ fp_nesting_maps = maps (map_thms_of_type lthy o T_of_bnf) fp_nesting_bnfs,
fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs,
fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs,
ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms corec_discs
@@ -931,7 +945,7 @@
(build_corec_arg_nested_call ctxt has_call sel_eqns sel)) nested_calls'
end);
-fun build_codefs ctxt bs mxs has_call arg_Tss (corec_specs : corec_spec list)
+fun build_defs ctxt bs mxs has_call arg_Tss (corec_specs : corec_spec list)
(disc_eqnss : coeqn_data_disc list list) (sel_eqnss : coeqn_data_sel list list) =
let
val corecs = map #corec corec_specs;
@@ -1104,7 +1118,7 @@
val disc_eqnss = @{map 6} mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss
disc_eqnss0;
val (defs, excludess') =
- build_codefs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
+ build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
val tac_opts =
map (fn {code_rhs_opt, ...} :: _ =>
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Tue Mar 17 12:23:56 2015 +0000
@@ -539,14 +539,13 @@
val defs = build_defs lthy nonexhaustives bs mxs funs_data rec_specs has_call;
- fun prove def_thms' ({ctr_specs, fp_nesting_map_ident0s, fp_nesting_map_comps, ...}
- : rec_spec) (fun_data : eqn_data list) lthy' =
+ fun prove def_thms ({ctr_specs, fp_nesting_map_ident0s, fp_nesting_map_comps, ...} : rec_spec)
+ (fun_data : eqn_data list) lthy' =
let
val js =
find_indices (op = o apply2 (fn {fun_name, ctr, ...} => (fun_name, ctr)))
fun_data eqns_data;
- val def_thms = map (snd o snd) def_thms';
val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
|> fst
|> map_filter (try (fn (x, [y]) =>
@@ -587,7 +586,7 @@
fun_defs = Morphism.fact phi def_thms, fpTs = take actual_nn Ts};
in
map_prod split_list (interpret_lfp_rec_sugar plugins fp_rec_sugar)
- (@{fold_map 2} (prove defs) (take actual_nn rec_specs) funs_data lthy)
+ (@{fold_map 2} (prove (map (snd o snd) defs)) (take actual_nn rec_specs) funs_data lthy)
end),
lthy |> Local_Theory.notes (notes @ common_notes) |> snd)
end;
--- a/src/HOL/Transcendental.thy Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/Transcendental.thy Tue Mar 17 12:23:56 2015 +0000
@@ -16,6 +16,9 @@
lemma real_fact_nat [simp]: "real (fact n :: nat) = fact n"
by (simp add: real_of_nat_def)
+lemma real_fact_int [simp]: "real (fact n :: int) = fact n"
+ by (metis of_int_of_nat_eq of_nat_fact real_of_int_def)
+
lemma root_test_convergence:
fixes f :: "nat \<Rightarrow> 'a::banach"
assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
@@ -4372,7 +4375,6 @@
case False
hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
- thm suminf_eq_arctan_bounded
by (rule suminf_eq_arctan_bounded[where x1="0" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>", symmetric])
(simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
moreover
--- a/src/Pure/GUI/gui.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/GUI/gui.scala Tue Mar 17 12:23:56 2015 +0000
@@ -80,9 +80,10 @@
/* simple dialogs */
- def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
+ def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
: ScrollPane =
{
+ val txt = Output.clean_yxml(raw_txt)
val text = new TextArea(txt)
if (width > 0) text.columns = width
if (height > 0 && split_lines(txt).length > height) text.rows = height
--- a/src/Pure/General/exn.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/General/exn.scala Tue Mar 17 12:23:56 2015 +0000
@@ -13,6 +13,13 @@
/* exceptions as values */
sealed abstract class Result[A]
+ {
+ def user_error: Result[A] =
+ this match {
+ case Exn(ERROR(msg)) => Exn(ERROR(msg))
+ case _ => this
+ }
+ }
case class Res[A](res: A) extends Result[A]
case class Exn[A](exn: Throwable) extends Result[A]
@@ -79,17 +86,18 @@
/* message */
- private val runtime_exception = Class.forName("java.lang.RuntimeException")
-
def user_message(exn: Throwable): Option[String] =
- if (exn.isInstanceOf[java.io.IOException]) {
- val msg = exn.getMessage
- Some(if (msg == null) "I/O error" else "I/O error: " + msg)
- }
- else if (exn.getClass == runtime_exception) {
+ if (exn.getClass == classOf[RuntimeException] ||
+ exn.getClass == classOf[Library.User_Error])
+ {
val msg = exn.getMessage
Some(if (msg == null || msg == "") "Error" else msg)
}
+ else if (exn.isInstanceOf[java.io.IOException])
+ {
+ val msg = exn.getMessage
+ Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
+ }
else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
else None
--- a/src/Pure/General/output.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/General/output.scala Tue Mar 17 12:23:56 2015 +0000
@@ -10,11 +10,15 @@
object Output
{
- def warning_text(msg: String): String = cat_lines(split_lines(msg).map("### " + _))
- def error_text(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
+ def clean_yxml(msg: String): String =
+ try { XML.content(YXML.parse_body(msg)) }
+ catch { case ERROR(_) => msg }
- def writeln(msg: String) { Console.err.println(msg) }
+ def writeln_text(msg: String): String = clean_yxml(msg)
+ def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
+ def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
+
+ def writeln(msg: String) { Console.err.println(writeln_text(msg)) }
def warning(msg: String) { Console.err.println(warning_text(msg)) }
def error_message(msg: String) { Console.err.println(error_text(msg)) }
}
-
--- a/src/Pure/General/position.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/General/position.scala Tue Mar 17 12:23:56 2015 +0000
@@ -21,6 +21,7 @@
val End_Offset = new Properties.Int(Markup.END_OFFSET)
val File = new Properties.String(Markup.FILE)
val Id = new Properties.Long(Markup.ID)
+ val Id_String = new Properties.String(Markup.ID)
val Def_Line = new Properties.Int(Markup.DEF_LINE)
val Def_Offset = new Properties.Int(Markup.DEF_OFFSET)
@@ -102,18 +103,20 @@
/* here: user output */
def here(pos: T): String =
- (Line.unapply(pos), File.unapply(pos)) match {
- case (Some(i), None) => " (line " + i.toString + ")"
- case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
- case (None, Some(name)) => " (file " + quote(name) + ")"
- case _ => ""
- }
+ Markup(Markup.POSITION, pos).markup(
+ (Line.unapply(pos), File.unapply(pos)) match {
+ case (Some(i), None) => " (line " + i.toString + ")"
+ case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
+ case (None, Some(name)) => " (file " + quote(name) + ")"
+ case _ => ""
+ })
def here_undelimited(pos: T): String =
- (Line.unapply(pos), File.unapply(pos)) match {
- case (Some(i), None) => "line " + i.toString
- case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
- case (None, Some(name)) => "file " + quote(name)
- case _ => ""
- }
+ Markup(Markup.POSITION, pos).markup(
+ (Line.unapply(pos), File.unapply(pos)) match {
+ case (Some(i), None) => "line " + i.toString
+ case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
+ case (None, Some(name)) => "file " + quote(name)
+ case _ => ""
+ })
}
--- a/src/Pure/Isar/keyword.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/Isar/keyword.ML Tue Mar 17 12:23:56 2015 +0000
@@ -249,4 +249,3 @@
fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
end;
-
--- a/src/Pure/Isar/keyword.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/Isar/keyword.scala Tue Mar 17 12:23:56 2015 +0000
@@ -39,7 +39,7 @@
val PRF_SCRIPT = "prf_script"
- /* categories */
+ /* command categories */
val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
@@ -50,6 +50,11 @@
val document_raw = Set(DOCUMENT_RAW)
val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
+ val theory_begin = Set(THY_BEGIN)
+ val theory_end = Set(THY_END)
+
+ val theory_load = Set(THY_LOAD)
+
val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
@@ -139,6 +144,12 @@
def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
+ def is_command_kind(name: String, pred: String => Boolean): Boolean =
+ command_kind(name) match {
+ case Some(kind) => pred(kind)
+ case None => false
+ }
+
/* load commands */
@@ -155,4 +166,3 @@
load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
}
}
-
--- a/src/Pure/Isar/outer_syntax.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/Isar/outer_syntax.scala Tue Mar 17 12:23:56 2015 +0000
@@ -123,7 +123,9 @@
}
- /* load commands */
+ /* command categories */
+
+ def is_theory_begin(name: String): Boolean = keywords.is_command_kind(name, Keyword.theory_begin)
def load_command(name: String): Option[List[String]] = keywords.load_command(name)
def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
@@ -235,7 +237,7 @@
case "subsubsection" => Some(3)
case _ =>
keywords.command_kind(command.name) match {
- case Some(kind) if Keyword.theory(kind) && kind != Keyword.THY_END => Some(4)
+ case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(4)
case _ => None
}
}
@@ -284,7 +286,7 @@
/* result structure */
val spans = parse_spans(text)
- spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
+ spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
result()
}
}
--- a/src/Pure/Isar/parse.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/Isar/parse.ML Tue Mar 17 12:23:56 2015 +0000
@@ -69,6 +69,8 @@
val xname: xstring parser
val text: string parser
val path: string parser
+ val theory_name: bstring parser
+ val theory_xname: xstring parser
val liberal_name: xstring parser
val parname: string parser
val parbinding: binding parser
@@ -275,6 +277,9 @@
val path = group (fn () => "file name/path specification") name;
+val theory_name = group (fn () => "theory name") name;
+val theory_xname = group (fn () => "theory name reference") xname;
+
val liberal_name = keyword_with Token.ident_or_symbolic || xname;
val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
--- a/src/Pure/Isar/parse.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/Isar/parse.scala Tue Mar 17 12:23:56 2015 +0000
@@ -25,31 +25,42 @@
if (!filter_proper || in.atEnd || in.first.is_proper) in
else proper(in.rest)
- def token(s: String, pred: Elem => Boolean): Parser[(Elem, Token.Pos)] =
- new Parser[(Elem, Token.Pos)] {
+ private def proper_position: Parser[Position.T] =
+ new Parser[Position.T] {
+ def apply(raw_input: Input) =
+ {
+ val in = proper(raw_input)
+ val pos =
+ in.pos match {
+ case pos: Token.Pos => pos
+ case _ => Token.Pos.none
+ }
+ Success(if (in.atEnd) pos.position() else pos.position(in.first), in)
+ }
+ }
+
+ def position[A](parser: Parser[A]): Parser[(A, Position.T)] =
+ proper_position ~ parser ^^ { case x ~ y => (y, x) }
+
+ def token(s: String, pred: Elem => Boolean): Parser[Elem] =
+ new Parser[Elem] {
def apply(raw_input: Input) =
{
val in = proper(raw_input)
if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
else {
- val pos =
- in.pos match {
- case pos: Token.Pos => pos
- case _ => Token.Pos.none
- }
val token = in.first
- if (pred(token)) Success((token, pos), proper(in.rest))
+ if (pred(token)) Success(token, proper(in.rest))
else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in)
}
}
}
def atom(s: String, pred: Elem => Boolean): Parser[String] =
- token(s, pred) ^^ { case (tok, _) => tok.content }
+ token(s, pred) ^^ (_.content)
- def command(name: String): Parser[Position.T] =
- token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^
- { case (_, pos) => pos.position }
+ def command(name: String): Parser[String] =
+ atom("command " + quote(name), tok => tok.is_command && tok.source == name)
def $$$(name: String): Parser[String] =
atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
@@ -61,8 +72,10 @@
def text: Parser[String] = atom("text", _.is_text)
def ML_source: Parser[String] = atom("ML source", _.is_text)
def document_source: Parser[String] = atom("document source", _.is_text)
+
def path: Parser[String] =
atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
+
def theory_name: Parser[String] =
atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
def theory_xname: Parser[String] =
--- a/src/Pure/Isar/token.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/Isar/token.scala Tue Mar 17 12:23:56 2015 +0000
@@ -157,10 +157,17 @@
object Pos
{
- val none: Pos = new Pos(0, "")
+ val none: Pos = new Pos(0, 0, "", "")
+ val start: Pos = new Pos(1, 1, "", "")
+ def file(file: String): Pos = new Pos(1, 1, file, "")
+ def id(id: String): Pos = new Pos(0, 1, "", id)
}
- final class Pos private[Token](val line: Int, val file: String)
+ final class Pos private[Token](
+ val line: Int,
+ val offset: Symbol.Offset,
+ val file: String,
+ val id: String)
extends scala.util.parsing.input.Position
{
def column = 0
@@ -168,13 +175,27 @@
def advance(token: Token): Pos =
{
- var n = 0
- for (c <- token.content if c == '\n') n += 1
- if (n == 0) this else new Pos(line + n, file)
+ var line1 = line
+ var offset1 = offset
+ for (s <- Symbol.iterator(token.source)) {
+ if (line1 > 0 && Symbol.is_newline(s)) line1 += 1
+ if (offset1 > 0) offset1 += 1
+ }
+ if (line1 == line && offset1 == offset) this
+ else new Pos(line1, offset1, file, id)
}
- def position: Position.T = Position.Line_File(line, file)
- override def toString: String = Position.here_undelimited(position)
+ private def position(end_offset: Symbol.Offset): Position.T =
+ (if (line > 0) Position.Line(line) else Nil) :::
+ (if (offset > 0) Position.Offset(offset) else Nil) :::
+ (if (end_offset > 0) Position.End_Offset(end_offset) else Nil) :::
+ (if (file != "") Position.File(file) else Nil) :::
+ (if (id != "") Position.Id_String(id) else Nil)
+
+ def position(): Position.T = position(0)
+ def position(token: Token): Position.T = position(advance(token).offset)
+
+ override def toString: String = Position.here_undelimited(position())
}
abstract class Reader extends scala.util.parsing.input.Reader[Token]
@@ -186,8 +207,8 @@
def atEnd = tokens.isEmpty
}
- def reader(tokens: List[Token], file: String = ""): Reader =
- new Token_Reader(tokens, new Pos(1, file))
+ def reader(tokens: List[Token], start: Token.Pos): Reader =
+ new Token_Reader(tokens, start)
}
@@ -195,8 +216,7 @@
{
def is_command: Boolean = kind == Token.Kind.COMMAND
def is_command_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean =
- is_command &&
- (keywords.command_kind(source) match { case Some(k) => pred(k) case None => false })
+ is_command && keywords.is_command_kind(source, pred)
def is_keyword: Boolean = kind == Token.Kind.KEYWORD
def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
def is_ident: Boolean = kind == Token.Kind.IDENT
--- a/src/Pure/PIDE/command.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/PIDE/command.ML Tue Mar 17 12:23:56 2015 +0000
@@ -10,14 +10,14 @@
val read_file: Path.T -> Position.T -> Path.T -> Token.file
val read_thy: Toplevel.state -> theory
val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
- blob list -> Token.T list -> Toplevel.transition
+ blob list * int -> Token.T list -> Toplevel.transition
type eval
val eval_eq: eval * eval -> bool
val eval_running: eval -> bool
val eval_finished: eval -> bool
val eval_result_state: eval -> Toplevel.state
val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
- blob list -> Token.T list -> eval -> eval
+ blob list * int -> Token.T list -> eval -> eval
type print
val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
eval -> print list -> print list option
@@ -51,21 +51,19 @@
fun read_file_node file_node master_dir pos src_path =
let
- val _ = Position.report pos Markup.language_path;
val _ =
(case try Url.explode file_node of
NONE => ()
| SOME (Url.File _) => ()
| _ =>
- (Position.report pos (Markup.path file_node);
error ("Prover cannot load remote file " ^
- Markup.markup (Markup.path file_node) (quote file_node) ^ Position.here pos)));
+ Markup.markup (Markup.path file_node) (quote file_node)));
val full_path = File.check_file (File.full_path master_dir src_path);
- val _ = Position.report pos (Markup.path (Path.implode full_path));
val text = File.read full_path;
val lines = split_lines text;
val digest = SHA1.digest text;
- in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end;
+ in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end
+ handle ERROR msg => error (msg ^ Position.here pos);
val read_file = read_file_node "";
@@ -80,27 +78,33 @@
| SOME exec_id => Position.put_id exec_id);
in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
-fun resolve_files keywords master_dir blobs toks =
+fun resolve_files keywords master_dir (blobs, blobs_index) toks =
(case Outer_Syntax.parse_spans toks of
- [span] => span
- |> Command_Span.resolve_files keywords (fn cmd => fn (path, pos) =>
- let
- fun make_file src_path (Exn.Res (file_node, NONE)) =
- Exn.interruptible_capture (fn () =>
- read_file_node file_node master_dir pos src_path) ()
- | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
- (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
- Exn.Res (blob_file src_path lines digest file_node))
- | make_file _ (Exn.Exn e) = Exn.Exn e;
- val src_paths = Keyword.command_files keywords cmd path;
- in
- if null blobs then
- map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
- else if length src_paths = length blobs then
- map2 make_file src_paths blobs
- else error ("Misalignment of inlined files" ^ Position.here pos)
- end)
- |> Command_Span.content
+ [Command_Span.Span (Command_Span.Command_Span (cmd, _), _)] =>
+ (case try (nth toks) blobs_index of
+ SOME tok =>
+ let
+ val pos = Token.pos_of tok;
+ val path = Path.explode (Token.content_of tok)
+ handle ERROR msg => error (msg ^ Position.here pos);
+ fun make_file src_path (Exn.Res (file_node, NONE)) =
+ Exn.interruptible_capture (fn () =>
+ read_file_node file_node master_dir pos src_path) ()
+ | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
+ Exn.Res (blob_file src_path lines digest file_node)
+ | make_file _ (Exn.Exn e) = Exn.Exn e;
+ val src_paths = Keyword.command_files keywords cmd path;
+ val files =
+ if null blobs then
+ map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
+ else if length src_paths = length blobs then
+ map2 make_file src_paths blobs
+ else error ("Misalignment of inlined files" ^ Position.here pos);
+ in
+ toks |> map_index (fn (i, tok) =>
+ if i = blobs_index then Token.put_files files tok else tok)
+ end
+ | NONE => toks)
| _ => toks);
val bootstrap_thy = ML_Context.the_global_context ();
@@ -109,7 +113,7 @@
fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => bootstrap_thy;
-fun read keywords thy master_dir init blobs span =
+fun read keywords thy master_dir init blobs_info span =
let
val command_reports = Outer_Syntax.command_reports thy;
@@ -124,7 +128,7 @@
in
if is_malformed then Toplevel.malformed pos "Malformed command syntax"
else
- (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs span) of
+ (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
[tr] => Toplevel.modify_init init tr
| [] => Toplevel.ignored (#1 (Token.range_of span))
| _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
@@ -221,7 +225,7 @@
in
-fun eval keywords master_dir init blobs span eval0 =
+fun eval keywords master_dir init blobs_info span eval0 =
let
val exec_id = Document_ID.make ();
fun process () =
@@ -230,7 +234,8 @@
val thy = read_thy (#state eval_state0);
val tr =
Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
- (fn () => read keywords thy master_dir init blobs span |> Toplevel.exec_id exec_id) ();
+ (fn () =>
+ read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) ();
in eval_state keywords span tr eval_state0 end;
in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end;
--- a/src/Pure/PIDE/command.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/PIDE/command.scala Tue Mar 17 12:23:56 2015 +0000
@@ -10,13 +10,16 @@
import scala.collection.mutable
import scala.collection.immutable.SortedMap
+import scala.util.parsing.input.CharSequenceReader
object Command
{
type Edit = (Option[Command], Option[Command])
+
type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Symbol.Text_Chunk)])]
-
+ type Blobs_Info = (List[Blob], Int)
+ val no_blobs: Blobs_Info = (Nil, -1)
/** accumulated results from prover **/
@@ -253,15 +256,15 @@
def apply(
id: Document_ID.Command,
node_name: Document.Node.Name,
- blobs: List[Blob],
+ blobs_info: Blobs_Info,
span: Command_Span.Span): Command =
{
val (source, span1) = span.compact_source
- new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
+ new Command(id, node_name, blobs_info, span1, source, Results.empty, Markup_Tree.empty)
}
val empty: Command =
- Command(Document_ID.none, Document.Node.Name.empty, Nil, Command_Span.empty)
+ Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty)
def unparsed(
id: Document_ID.Command,
@@ -270,7 +273,7 @@
markup: Markup_Tree): Command =
{
val (source1, span1) = Command_Span.unparsed(source).compact_source
- new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
+ new Command(id, Document.Node.Name.empty, no_blobs, span1, source1, results, markup)
}
def unparsed(source: String): Command =
@@ -305,13 +308,89 @@
(cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
}
}
+
+
+ /* blobs: inlined errors and auxiliary files */
+
+ private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
+ {
+ def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
+ toks match {
+ case (t1, i1) :: (t2, i2) :: rest =>
+ if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
+ else (t1, i1) :: clean((t2, i2) :: rest)
+ case _ => toks
+ }
+ clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
+ }
+
+ private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
+ tokens match {
+ case (tok, _) :: toks =>
+ if (tok.is_command)
+ toks.collectFirst({ case (t, i) if t.is_name => (t.content, i) })
+ else None
+ case Nil => None
+ }
+
+ def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
+ span.kind match {
+ case Command_Span.Command_Span(name, _) =>
+ syntax.load_command(name) match {
+ case Some(exts) =>
+ find_file(clean_tokens(span.content)) match {
+ case Some((file, i)) =>
+ if (exts.isEmpty) (List(file), i)
+ else (exts.map(ext => file + "." + ext), i)
+ case None => (Nil, -1)
+ }
+ case None => (Nil, -1)
+ }
+ case _ => (Nil, -1)
+ }
+
+ def blobs_info(
+ resources: Resources,
+ syntax: Prover.Syntax,
+ get_blob: Document.Node.Name => Option[Document.Blob],
+ can_import: Document.Node.Name => Boolean,
+ node_name: Document.Node.Name,
+ span: Command_Span.Span): Blobs_Info =
+ {
+ span.kind match {
+ // inlined errors
+ case Command_Span.Command_Span(name, _) if syntax.is_theory_begin(name) =>
+ val header =
+ resources.check_thy_reader("", node_name,
+ new CharSequenceReader(span.source), Token.Pos.id(Markup.COMMAND))
+ val import_errors =
+ for ((imp, pos) <- header.imports if !can_import(imp)) yield {
+ val name = imp.node
+ "Bad theory import " + Markup.Path(name).markup(quote(name)) + Position.here(pos)
+ }
+ ((header.errors ::: import_errors).map(msg => Exn.Exn(ERROR(msg)): Command.Blob), -1)
+
+ // auxiliary files
+ case _ =>
+ val (files, index) = span_files(syntax, span)
+ val blobs =
+ files.map(file =>
+ (Exn.capture {
+ val name =
+ Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
+ val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
+ (name, blob)
+ }).user_error)
+ (blobs, index)
+ }
+ }
}
final class Command private(
val id: Document_ID.Command,
val node_name: Document.Node.Name,
- val blobs: List[Command.Blob],
+ val blobs_info: Command.Blobs_Info,
val span: Command_Span.Span,
val source: String,
val init_results: Command.Results,
@@ -340,6 +419,9 @@
/* blobs */
+ def blobs: List[Command.Blob] = blobs_info._1
+ def blobs_index: Int = blobs_info._2
+
def blobs_names: List[Document.Node.Name] =
for (Exn.Res((name, _)) <- blobs) yield name
--- a/src/Pure/PIDE/command_span.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/PIDE/command_span.ML Tue Mar 17 12:23:56 2015 +0000
@@ -10,8 +10,6 @@
datatype span = Span of kind * Token.T list
val kind: span -> kind
val content: span -> Token.T list
- val resolve_files: Keyword.keywords ->
- (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
end;
structure Command_Span: COMMAND_SPAN =
@@ -23,49 +21,4 @@
fun kind (Span (k, _)) = k;
fun content (Span (_, toks)) = toks;
-
-(* resolve inlined files *)
-
-local
-
-fun clean ((i1, t1) :: (i2, t2) :: toks) =
- if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
- else (i1, t1) :: clean ((i2, t2) :: toks)
- | clean toks = toks;
-
-fun clean_tokens toks =
- ((0 upto length toks - 1) ~~ toks)
- |> filter (fn (_, tok) => Token.is_proper tok)
- |> clean;
-
-fun find_file ((_, tok) :: toks) =
- if Token.is_command tok then
- toks |> get_first (fn (i, tok) =>
- if Token.is_name tok then
- SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
- handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
- else NONE)
- else NONE
- | find_file [] = NONE;
-
-in
-
-fun resolve_files keywords read_files span =
- (case span of
- Span (Command_Span (cmd, pos), toks) =>
- if Keyword.is_theory_load keywords cmd then
- (case find_file (clean_tokens toks) of
- NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
- | SOME (i, path) =>
- let
- val toks' = toks |> map_index (fn (j, tok) =>
- if i = j then Token.put_files (read_files cmd path) tok
- else tok);
- in Span (Command_Span (cmd, pos), toks') end)
- else span
- | _ => span);
-
end;
-
-end;
-
--- a/src/Pure/PIDE/command_span.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/PIDE/command_span.scala Tue Mar 17 12:23:56 2015 +0000
@@ -28,23 +28,24 @@
{
def length: Int = (0 /: content)(_ + _.source.length)
+ def source: String =
+ content match {
+ case List(tok) => tok.source
+ case toks => toks.map(_.source).mkString
+ }
+
def compact_source: (String, Span) =
{
- val source: String =
- content match {
- case List(tok) => tok.source
- case toks => toks.map(_.source).mkString
- }
-
+ val src = source
val content1 = new mutable.ListBuffer[Token]
var i = 0
for (Token(kind, s) <- content) {
val n = s.length
- val s1 = source.substring(i, i + n)
+ val s1 = src.substring(i, i + n)
content1 += Token(kind, s1)
i += n
}
- (source, Span(kind, content1.toList))
+ (src, Span(kind, content1.toList))
}
}
@@ -52,55 +53,4 @@
def unparsed(source: String): Span =
Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
-
-
- /* resolve inlined files */
-
- private def find_file(tokens: List[Token]): Option[String] =
- {
- def clean(toks: List[Token]): List[Token] =
- toks match {
- case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
- case t :: ts => t :: clean(ts)
- case Nil => Nil
- }
- clean(tokens.filter(_.is_proper)) match {
- case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
- case _ => None
- }
- }
-
- def span_files(syntax: Prover.Syntax, span: Span): List[String] =
- span.kind match {
- case Command_Span(name, _) =>
- syntax.load_command(name) match {
- case Some(exts) =>
- find_file(span.content) match {
- case Some(file) =>
- if (exts.isEmpty) List(file)
- else exts.map(ext => file + "." + ext)
- case None => Nil
- }
- case None => Nil
- }
- case _ => Nil
- }
-
- def resolve_files(
- resources: Resources,
- syntax: Prover.Syntax,
- node_name: Document.Node.Name,
- span: Span,
- get_blob: Document.Node.Name => Option[Document.Blob])
- : List[Command.Blob] =
- {
- span_files(syntax, span).map(file_name =>
- Exn.capture {
- val name =
- Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
- val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
- (name, blob)
- })
- }
}
-
--- a/src/Pure/PIDE/document.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/PIDE/document.ML Tue Mar 17 12:23:56 2015 +0000
@@ -19,7 +19,7 @@
val init_state: state
val define_blob: string -> string -> state -> state
type blob_digest = (string * string option) Exn.result
- val define_command: Document_ID.command -> string -> blob_digest list ->
+ val define_command: Document_ID.command -> string -> blob_digest list -> int ->
((int * int) * string) list -> state -> state
val remove_versions: Document_ID.version list -> state -> state
val start_execution: state -> state
@@ -307,8 +307,8 @@
abstype state = State of
{versions: version Inttab.table, (*version id -> document content*)
blobs: (SHA1.digest * string list) Symtab.table, (*raw digest -> digest, lines*)
- commands: (string * blob_digest list * Token.T list lazy) Inttab.table,
- (*command id -> name, inlined files, command span*)
+ commands: (string * blob_digest list * int * Token.T list lazy) Inttab.table,
+ (*command id -> name, inlined files, token index of files, command span*)
execution: execution} (*current execution process*)
with
@@ -359,23 +359,39 @@
blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
(file_node, Option.map (the_blob state) raw_digest));
+fun blob_reports pos (blob_digest: blob_digest) =
+ (case blob_digest of Exn.Res (file_node, _) => [(pos, Markup.path file_node)] | _ => []);
+
(* commands *)
-fun define_command command_id name command_blobs toks =
+fun define_command command_id name blobs_digests blobs_index toks =
map_state (fn (versions, blobs, commands, execution) =>
let
val id = Document_ID.print command_id;
val span =
Lazy.lazy (fn () =>
Position.setmp_thread_data (Position.id_only id)
- (fn () => #1 (fold_map Token.make toks (Position.id id))) ());
+ (fn () =>
+ let
+ val (tokens, _) = fold_map Token.make toks (Position.id id);
+ val _ =
+ if blobs_index < 0
+ then (*inlined errors*)
+ map_filter Exn.get_exn blobs_digests
+ |> List.app (Output.error_message o Runtime.exn_message)
+ else (*auxiliary files*)
+ let val pos = Token.pos_of (nth tokens blobs_index) in
+ Position.reports
+ ((pos, Markup.language_path) :: maps (blob_reports pos) blobs_digests)
+ end;
+ in tokens end) ());
+ val commands' =
+ Inttab.update_new (command_id, (name, blobs_digests, blobs_index, span)) commands
+ handle Inttab.DUP dup => err_dup "command" dup;
val _ =
Position.setmp_thread_data (Position.id_only id)
(fn () => Output.status (Markup.markup_only Markup.accepted)) ();
- val commands' =
- Inttab.update_new (command_id, (name, command_blobs, span)) commands
- handle Inttab.DUP dup => err_dup "command" dup;
in (versions, blobs, commands', execution) end);
fun the_command (State {commands, ...}) command_id =
@@ -405,7 +421,7 @@
SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
val blobs' =
(commands', Symtab.empty) |->
- Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
+ Inttab.fold (fn (_, (_, blobs, _, _)) => blobs |>
fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
in (versions', blobs', commands', execution) end);
@@ -571,13 +587,13 @@
val command_visible = visible_command node command_id';
val command_overlays = overlays node command_id';
- val (command_name, blob_digests, span0) = the_command state command_id';
+ val (command_name, blob_digests, blobs_index, span0) = the_command state command_id';
val blobs = map (resolve_blob state) blob_digests;
val span = Lazy.force span0;
val eval' =
Command.eval keywords (master_directory node)
- (fn () => the_default illegal_init init span) blobs span eval;
+ (fn () => the_default illegal_init init span) (blobs, blobs_index) span eval;
val prints' =
perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
val exec' = (eval', prints');
--- a/src/Pure/PIDE/document.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/PIDE/document.scala Tue Mar 17 12:23:56 2015 +0000
@@ -81,7 +81,7 @@
/* header and name */
sealed case class Header(
- imports: List[Name],
+ imports: List[(Name, Position.T)],
keywords: Thy_Header.Keywords,
errors: List[String])
{
@@ -256,6 +256,8 @@
Node.is_no_perspective_command(perspective) &&
commands.isEmpty
+ def has_header: Boolean = header != Node.no_header
+
def commands: Linear_Set[Command] = _commands.commands
def load_commands: List[Command] = _commands.load_commands
@@ -323,7 +325,7 @@
def + (entry: (Node.Name, Node)): Nodes =
{
val (name, node) = entry
- val imports = node.header.imports
+ val imports = node.header.imports.map(_._1)
val graph1 =
(graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
--- a/src/Pure/PIDE/markup.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/PIDE/markup.scala Tue Mar 17 12:23:56 2015 +0000
@@ -504,4 +504,7 @@
sealed case class Markup(name: String, properties: Properties.T)
-
+{
+ def markup(s: String): String =
+ YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
+}
--- a/src/Pure/PIDE/protocol.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/PIDE/protocol.ML Tue Mar 17 12:23:56 2015 +0000
@@ -30,17 +30,20 @@
Isabelle_Process.protocol_command "Document.define_command"
(fn id :: name :: blobs_yxml :: toks_yxml :: sources =>
let
- val blobs =
+ val (blobs, blobs_index) =
YXML.parse_body blobs_yxml |>
let open XML.Decode in
- list (variant
- [fn ([], a) => Exn.Res (pair string (option string) a),
- fn ([], a) => Exn.Exn (ERROR (string a))])
+ pair
+ (list (variant
+ [fn ([], a) => Exn.Res (pair string (option string) a),
+ fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]))
+ int
end;
val toks =
(YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
in
- Document.change_state (Document.define_command (Document_ID.parse id) name blobs toks)
+ Document.change_state
+ (Document.define_command (Document_ID.parse id) name blobs blobs_index toks)
end);
val _ =
@@ -72,7 +75,7 @@
pair string (pair string (pair (list string)
(pair (list (pair string
(option (pair (pair string (list string)) (list string)))))
- (list string)))) a;
+ (list YXML.string_of_body)))) a;
val imports' = map (rpair Position.none) imports;
val header = Thy_Header.make (name, Position.none) imports' keywords;
in Document.Deps (master, header, errors) end,
--- a/src/Pure/PIDE/protocol.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/PIDE/protocol.scala Tue Mar 17 12:23:56 2015 +0000
@@ -382,7 +382,30 @@
def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
- def define_command(command: Command): Unit =
+ private def resolve_id(id: String, body: XML.Body): XML.Body =
+ {
+ def resolve_property(p: (String, String)): (String, String) =
+ if (p._1 == Markup.ID && p._2 == Markup.COMMAND) (Markup.ID, id) else p
+
+ def resolve_markup(markup: Markup): Markup =
+ Markup(markup.name, markup.properties.map(resolve_property))
+
+ def resolve_tree(t: XML.Tree): XML.Tree =
+ t match {
+ case XML.Wrapped_Elem(markup, ts1, ts2) =>
+ XML.Wrapped_Elem(resolve_markup(markup), ts1.map(resolve_tree _), ts2.map(resolve_tree _))
+ case XML.Elem(markup, ts) =>
+ XML.Elem(resolve_markup(markup), ts.map(resolve_tree _))
+ case text => text
+ }
+ body.map(resolve_tree _)
+ }
+
+ private def resolve_id(id: String, s: String): XML.Body =
+ try { resolve_id(id, YXML.parse_body(s)) }
+ catch { case ERROR(_) => XML.Encode.string(s) }
+
+ def define_command(command: Command)
{
val blobs_yxml =
{ import XML.Encode._
@@ -390,9 +413,9 @@
variant(List(
{ case Exn.Res((a, b)) =>
(Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
- { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
+ { case Exn.Exn(e) => (Nil, resolve_id(command.id.toString, Exn.message(e))) }))
- YXML.string_of_body(list(encode_blob)(command.blobs))
+ YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
}
val toks = command.span.content
@@ -433,7 +456,7 @@
{ case Document.Node.Deps(header) =>
val master_dir = Isabelle_System.posix_path_url(name.master_dir)
val theory = Long_Name.base_name(name.theory)
- val imports = header.imports.map(_.node)
+ val imports = header.imports.map({ case (a, _) => a.node })
val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
(Nil,
pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
--- a/src/Pure/PIDE/prover.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/PIDE/prover.scala Tue Mar 17 12:23:56 2015 +0000
@@ -20,6 +20,7 @@
def ++ (other: Syntax): Syntax
def add_keywords(keywords: Thy_Header.Keywords): Syntax
def parse_spans(input: CharSequence): List[Command_Span.Span]
+ def is_theory_begin(name: String): Boolean
def load_command(name: String): Option[List[String]]
def load_commands_in(text: String): Boolean
}
--- a/src/Pure/PIDE/resources.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/PIDE/resources.ML Tue Mar 17 12:23:56 2015 +0000
@@ -128,7 +128,7 @@
let
fun prepare_span st span =
Command_Span.content span
- |> Command.read keywords (Command.read_thy st) master_dir init []
+ |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
|> (fn tr => Toplevel.put_timing (last_timing tr) tr);
fun element_result span_elem (st, _) =
--- a/src/Pure/PIDE/resources.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/PIDE/resources.scala Tue Mar 17 12:23:56 2015 +0000
@@ -57,7 +57,7 @@
def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
if (syntax.load_commands_in(text)) {
val spans = syntax.parse_spans(text)
- spans.iterator.map(Command_Span.span_files(syntax, _)).flatten.toList
+ spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
}
else Nil
@@ -86,20 +86,21 @@
}
}
- def check_thy_reader(qualifier: String, name: Document.Node.Name, reader: Reader[Char])
- : Document.Node.Header =
+ def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
+ reader: Reader[Char], start: Token.Pos): Document.Node.Header =
{
if (reader.source.length > 0) {
try {
- val header = Thy_Header.read(reader).decode_symbols
+ val header = Thy_Header.read(reader, start).decode_symbols
- val base_name = Long_Name.base_name(name.theory)
- val name1 = header.name
- if (base_name != name1)
+ val base_name = Long_Name.base_name(node_name.theory)
+ val (name, pos) = header.name
+ if (base_name != name)
error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
- " for theory " + quote(name1))
+ " for theory " + quote(name) + Position.here(pos))
- val imports = header.imports.map(import_name(qualifier, name, _))
+ val imports =
+ header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
Document.Node.Header(imports, header.keywords, Nil)
}
catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
@@ -107,8 +108,16 @@
else Document.Node.no_header
}
- def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
- with_thy_reader(name, check_thy_reader(qualifier, name, _))
+ def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos)
+ : Document.Node.Header =
+ with_thy_reader(name, check_thy_reader(qualifier, name, _, start))
+
+ def check_file(file: String): Boolean =
+ try {
+ if (Url.is_wellformed(file)) Url.is_readable(file)
+ else (new JFile(file)).isFile
+ }
+ catch { case ERROR(_) => false }
/* document changes */
--- a/src/Pure/System/options.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/System/options.scala Tue Mar 17 12:23:56 2015 +0000
@@ -93,9 +93,9 @@
{
command(SECTION) ~! text ^^
{ case _ ~ a => (options: Options) => options.set_section(a) } |
- opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ $$$(":") ~ option_type ~
+ opt(command(PUBLIC)) ~ position(command(OPTION)) ~! (option_name ~ $$$(":") ~ option_type ~
$$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
- { case a ~ pos ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
+ { case a ~ ((_, pos)) ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
(options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
}
@@ -110,7 +110,7 @@
{
val toks = Token.explode(syntax.keywords, File.read(file))
val ops =
- parse_all(rep(parser), Token.reader(toks, file.implode)) match {
+ parse_all(rep(parser), Token.reader(toks, Token.Pos.file(file.implode))) match {
case Success(result, _) => result
case bad => error(bad.toString)
}
--- a/src/Pure/Thy/thy_header.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/Thy/thy_header.ML Tue Mar 17 12:23:56 2015 +0000
@@ -103,10 +103,9 @@
local
-val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name);
-val theory_xname = Parse.group (fn () => "theory name reference") (Parse.position Parse.xname);
-
-val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_xname);
+fun imports name =
+ if name = Context.PureN then Scan.succeed []
+ else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname));
val opt_files =
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
@@ -129,8 +128,8 @@
in
val args =
- theory_name :|-- (fn (name, pos) =>
- (if name = Context.PureN then Scan.succeed [] else imports) --
+ Parse.position Parse.theory_name :|-- (fn (name, pos) =>
+ imports name --
Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));
--- a/src/Pure/Thy/thy_header.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/Thy/thy_header.scala Tue Mar 17 12:23:56 2015 +0000
@@ -80,11 +80,10 @@
val header: Parser[Thy_Header] =
{
- val file_name = atom("file name", _.is_name)
-
val opt_files =
$$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
success(Nil)
+
val keyword_spec =
atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
{ case x ~ y ~ z => ((x, y), z) }
@@ -94,17 +93,14 @@
opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
{ case xs ~ y ~ z => xs.map((_, y, z)) }
+
val keyword_decls =
keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
{ case xs ~ yss => (xs :: yss).flatten }
- val file =
- $$$("(") ~! (file_name ~ $$$(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
- file_name ^^ (x => (x, true))
-
val args =
- theory_name ~
- (opt($$$(IMPORTS) ~! (rep1(theory_xname))) ^^
+ position(theory_name) ~
+ (opt($$$(IMPORTS) ~! (rep1(position(theory_xname)))) ^^
{ case None => Nil case Some(_ ~ xs) => xs }) ~
(opt($$$(KEYWORDS) ~! keyword_decls) ^^
{ case None => Nil case Some(_ ~ xs) => xs }) ~
@@ -128,7 +124,7 @@
/* read -- lazy scanning */
- def read(reader: Reader[Char]): Thy_Header =
+ def read(reader: Reader[Char], start: Token.Pos): Thy_Header =
{
val token = Token.Parsers.token(bootstrap_keywords)
val toks = new mutable.ListBuffer[Token]
@@ -144,31 +140,27 @@
}
scan_to_begin(reader)
- parse(commit(header), Token.reader(toks.toList)) match {
+ parse(commit(header), Token.reader(toks.toList, start)) match {
case Success(result, _) => result
case bad => error(bad.toString)
}
}
- def read(source: CharSequence): Thy_Header =
- read(new CharSequenceReader(source))
+ def read(source: CharSequence, start: Token.Pos): Thy_Header =
+ read(new CharSequenceReader(source), start)
}
sealed case class Thy_Header(
- name: String,
- imports: List[String],
+ name: (String, Position.T),
+ imports: List[(String, Position.T)],
keywords: Thy_Header.Keywords)
{
- def map(f: String => String): Thy_Header =
- Thy_Header(f(name), imports.map(f), keywords)
-
def decode_symbols: Thy_Header =
{
val f = Symbol.decode _
- Thy_Header(f(name), imports.map(f),
+ Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }),
keywords.map({ case (a, b, c) =>
(f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) }))
}
}
-
--- a/src/Pure/Thy/thy_info.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/Thy/thy_info.scala Tue Mar 17 12:23:56 2015 +0000
@@ -106,7 +106,7 @@
if (parent_loaded(dep.name.theory)) g
else {
val a = node(dep.name)
- val bs = dep.header.imports.map(node _)
+ val bs = dep.header.imports.map({ case (name, _) => node(name) })
((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
}
}
@@ -134,10 +134,9 @@
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
val header =
- try { resources.check_thy(session, name).cat_errors(message) }
+ try { resources.check_thy(session, name, Token.Pos.file(name.node)).cat_errors(message) }
catch { case ERROR(msg) => cat_error(msg, message) }
- val imports = header.imports.map((_, Position.File(name.node)))
- Dep(name, header) :: require_thys(session, name :: initiators, required1, imports)
+ Dep(name, header) :: require_thys(session, name :: initiators, required1, header.imports)
}
catch {
case e: Throwable =>
--- a/src/Pure/Thy/thy_syntax.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/Thy/thy_syntax.scala Tue Mar 17 12:23:56 2015 +0000
@@ -63,7 +63,7 @@
- /** header edits: structure and outer syntax **/
+ /** header edits: graph structure and outer syntax **/
private def header_edits(
resources: Resources,
@@ -82,7 +82,7 @@
node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header
if (update_header) {
val node1 = node.update_header(header)
- if (node.header.imports != node1.header.imports ||
+ if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) ||
node.header.keywords != node1.header.keywords) syntax_changed0 += name
nodes += (name -> node1)
doc_edits += (name -> Document.Node.Deps(header))
@@ -98,7 +98,7 @@
if (node.is_empty) None
else {
val header = node.header
- val imports_syntax = header.imports.flatMap(a => nodes(a).syntax)
+ val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
}
nodes += (name -> node.update_syntax(syntax))
@@ -143,8 +143,8 @@
@tailrec private def chop_common(
cmds: List[Command],
- blobs_spans: List[(List[Command.Blob], Command_Span.Span)])
- : (List[Command], List[(List[Command.Blob], Command_Span.Span)]) =
+ blobs_spans: List[(Command.Blobs_Info, Command_Span.Span)])
+ : (List[Command], List[(Command.Blobs_Info, Command_Span.Span)]) =
{
(cmds, blobs_spans) match {
case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
@@ -157,14 +157,15 @@
resources: Resources,
syntax: Prover.Syntax,
get_blob: Document.Node.Name => Option[Document.Blob],
- name: Document.Node.Name,
+ can_import: Document.Node.Name => Boolean,
+ node_name: Document.Node.Name,
commands: Linear_Set[Command],
first: Command, last: Command): Linear_Set[Command] =
{
val cmds0 = commands.iterator(first, last).toList
val blobs_spans0 =
- syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
- map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
+ syntax.parse_spans(cmds0.iterator.map(_.source).mkString).map(span =>
+ (Command.blobs_info(resources, syntax, get_blob, can_import, node_name, span), span))
val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
@@ -179,75 +180,13 @@
case cmd :: _ =>
val hook = commands.prev(cmd)
val inserted =
- blobs_spans2.map({ case (blobs, span) => Command(Document_ID.make(), name, blobs, span) })
+ blobs_spans2.map({ case (blobs, span) =>
+ Command(Document_ID.make(), node_name, blobs, span) })
(commands /: cmds2)(_ - _).append_after(hook, inserted)
}
}
- /* recover command spans after edits */
-
- // FIXME somewhat slow
- private def recover_spans(
- resources: Resources,
- syntax: Prover.Syntax,
- get_blob: Document.Node.Name => Option[Document.Blob],
- name: Document.Node.Name,
- perspective: Command.Perspective,
- commands: Linear_Set[Command]): Linear_Set[Command] =
- {
- val visible = perspective.commands.toSet
-
- def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command =
- cmds.iterator(from).dropWhile(cmd => !cmd.is_proper || visible(cmd))
- .find(_.is_proper) getOrElse cmds.last
-
- @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
- cmds.find(_.is_unparsed) match {
- case Some(first_unparsed) =>
- val first = next_invisible_command(cmds.reverse, first_unparsed)
- val last = next_invisible_command(cmds, first_unparsed)
- recover(reparse_spans(resources, syntax, get_blob, name, cmds, first, last))
- case None => cmds
- }
- recover(commands)
- }
-
-
- /* consolidate unfinished spans */
-
- private def consolidate_spans(
- resources: Resources,
- syntax: Prover.Syntax,
- get_blob: Document.Node.Name => Option[Document.Blob],
- reparse_limit: Int,
- name: Document.Node.Name,
- perspective: Command.Perspective,
- commands: Linear_Set[Command]): Linear_Set[Command] =
- {
- if (perspective.commands.isEmpty) commands
- else {
- commands.find(_.is_unfinished) match {
- case Some(first_unfinished) =>
- val visible = perspective.commands.toSet
- commands.reverse.find(visible) match {
- case Some(last_visible) =>
- val it = commands.iterator(last_visible)
- var last = last_visible
- var i = 0
- while (i < reparse_limit && it.hasNext) {
- last = it.next
- i += last.length
- }
- reparse_spans(resources, syntax, get_blob, name, commands, first_unfinished, last)
- case None => commands
- }
- case None => commands
- }
- }
- }
-
-
/* main */
def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
@@ -264,9 +203,35 @@
resources: Resources,
syntax: Prover.Syntax,
get_blob: Document.Node.Name => Option[Document.Blob],
+ can_import: Document.Node.Name => Boolean,
reparse_limit: Int,
node: Document.Node, edit: Document.Edit_Text): Document.Node =
{
+ /* recover command spans after edits */
+ // FIXME somewhat slow
+ def recover_spans(
+ name: Document.Node.Name,
+ perspective: Command.Perspective,
+ commands: Linear_Set[Command]): Linear_Set[Command] =
+ {
+ val is_visible = perspective.commands.toSet
+
+ def next_invisible(cmds: Linear_Set[Command], from: Command): Command =
+ cmds.iterator(from).dropWhile(cmd => !cmd.is_proper || is_visible(cmd))
+ .find(_.is_proper) getOrElse cmds.last
+
+ @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
+ cmds.find(_.is_unparsed) match {
+ case Some(first_unparsed) =>
+ val first = next_invisible(cmds.reverse, first_unparsed)
+ val last = next_invisible(cmds, first_unparsed)
+ recover(
+ reparse_spans(resources, syntax, get_blob, can_import, name, cmds, first, last))
+ case None => cmds
+ }
+ recover(commands)
+ }
+
edit match {
case (_, Document.Node.Clear()) => node.clear
@@ -276,8 +241,7 @@
if (name.is_theory) {
val commands0 = node.commands
val commands1 = edit_text(text_edits, commands0)
- val commands2 =
- recover_spans(resources, syntax, get_blob, name, node.perspective.visible, commands1)
+ val commands2 = recover_spans(name, node.perspective.visible, commands1)
node.update_commands(commands2)
}
else node
@@ -289,11 +253,33 @@
val perspective: Document.Node.Perspective_Command =
Document.Node.Perspective(required, visible_overlay, overlays)
if (node.same_perspective(text_perspective, perspective)) node
- else
- node.update_perspective(text_perspective, perspective).
- update_commands(
- consolidate_spans(resources, syntax, get_blob, reparse_limit,
- name, visible, node.commands))
+ else {
+ /* consolidate unfinished spans */
+ val is_visible = visible.commands.toSet
+ val commands = node.commands
+ val commands1 =
+ if (is_visible.isEmpty) commands
+ else {
+ commands.find(_.is_unfinished) match {
+ case Some(first_unfinished) =>
+ commands.reverse.find(is_visible) match {
+ case Some(last_visible) =>
+ val it = commands.iterator(last_visible)
+ var last = last_visible
+ var i = 0
+ while (i < reparse_limit && it.hasNext) {
+ last = it.next
+ i += last.length
+ }
+ reparse_spans(resources, syntax, get_blob, can_import,
+ name, commands, first_unfinished, last)
+ case None => commands
+ }
+ case None => commands
+ }
+ }
+ node.update_perspective(text_perspective, perspective).update_commands(commands1)
+ }
}
}
@@ -304,10 +290,13 @@
doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text]): Session.Change =
{
+ val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
+
def get_blob(name: Document.Node.Name) =
doc_blobs.get(name) orElse previous.nodes(name).get_blob
- val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
+ def can_import(name: Document.Node.Name): Boolean =
+ resources.loaded_theories(name.theory) || nodes0(name).has_header
val (doc_edits, version) =
if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
@@ -337,14 +326,15 @@
val node1 =
if (reparse_set(name) && commands.nonEmpty)
node.update_commands(
- reparse_spans(resources, syntax, get_blob,
- name, commands, commands.head, commands.last))
+ reparse_spans(resources, syntax, get_blob, can_import, name,
+ commands, commands.head, commands.last))
else node
val node2 =
- (node1 /: edits)(text_edit(resources, syntax, get_blob, reparse_limit, _, _))
+ (node1 /: edits)(
+ text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _))
val node3 =
if (reparse_set.contains(name))
- text_edit(resources, syntax, get_blob, reparse_limit,
+ text_edit(resources, syntax, get_blob, can_import, reparse_limit,
node2, (name, node2.edit_perspective))
else node2
--- a/src/Pure/Tools/build.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/Tools/build.scala Tue Mar 17 12:23:56 2015 +0000
@@ -242,7 +242,7 @@
{ case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
- command(SESSION) ~!
+ position(command(SESSION)) ~!
(session_name ~
(($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
(($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
@@ -253,15 +253,16 @@
rep1(theories) ~
(($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
(rep(document_files) ^^ (x => x.flatten))))) ^^
- { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
+ { case (_, pos) ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
}
def parse_entries(root: Path): List[(String, Session_Entry)] =
{
val toks = Token.explode(root_syntax.keywords, File.read(root))
+ val start = Token.Pos.file(root.implode)
- parse_all(rep(chapter | session_entry), Token.reader(toks, root.implode)) match {
+ parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
case Success(result, _) =>
var chapter = chapter_default
val entries = new mutable.ListBuffer[(String, Session_Entry)]
--- a/src/Pure/library.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/library.scala Tue Mar 17 12:23:56 2015 +0000
@@ -16,9 +16,21 @@
{
/* user errors */
+ class User_Error(message: String) extends RuntimeException(message)
+ {
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: User_Error => message == other.getMessage
+ case _ => false
+ }
+ override def hashCode: Int = message.hashCode
+
+ override def toString: String = "ERROR(" + message + ")"
+ }
+
object ERROR
{
- def apply(message: String): Throwable = new RuntimeException(message)
+ def apply(message: String): User_Error = new User_Error(message)
def unapply(exn: Throwable): Option[String] = Exn.user_message(exn)
}
--- a/src/Pure/raw_simplifier.ML Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Pure/raw_simplifier.ML Tue Mar 17 12:23:56 2015 +0000
@@ -845,8 +845,15 @@
fun check_conv ctxt msg thm thm' =
let
val thm'' = Thm.transitive thm thm' handle THM _ =>
- Thm.transitive thm (Thm.transitive
- (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
+ let
+ val nthm' =
+ Thm.transitive (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm'
+ in Thm.transitive thm nthm' handle THM _ =>
+ let
+ val nthm =
+ Thm.transitive thm (Drule.beta_eta_conversion (Thm.rhs_of thm))
+ in Thm.transitive nthm nthm' end
+ end
val _ =
if msg then cond_tracing ctxt (fn () => print_thm ctxt "SUCCEEDED" ("", thm'))
else ();
--- a/src/Tools/jEdit/src/document_model.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Tools/jEdit/src/document_model.scala Tue Mar 17 12:23:56 2015 +0000
@@ -79,7 +79,8 @@
if (is_theory) {
JEdit_Lib.buffer_lock(buffer) {
Exn.capture {
- PIDE.resources.check_thy_reader("", node_name, JEdit_Lib.buffer_reader(buffer))
+ PIDE.resources.check_thy_reader("", node_name,
+ JEdit_Lib.buffer_reader(buffer), Token.Pos.file(node_name.node))
} match {
case Exn.Res(header) => header
case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
--- a/src/Tools/jEdit/src/jedit_resources.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Tools/jEdit/src/jedit_resources.scala Tue Mar 17 12:23:56 2015 +0000
@@ -79,13 +79,6 @@
}
}
- def check_file(view: View, file: String): Boolean =
- try {
- if (Url.is_wellformed(file)) Url.is_readable(file)
- else (new JFile(file)).isFile
- }
- catch { case ERROR(_) => false }
-
/* file content */
--- a/src/Tools/jEdit/src/plugin.scala Mon Mar 16 15:30:00 2015 +0000
+++ b/src/Tools/jEdit/src/plugin.scala Tue Mar 17 12:23:56 2015 +0000
@@ -216,9 +216,8 @@
} yield (model.node_name, Position.none)
val thy_info = new Thy_Info(PIDE.resources)
- // FIXME avoid I/O on GUI thread!?!
val files = thy_info.dependencies("", thys).deps.map(_.name.node).
- filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file))
+ filter(file => !loaded_buffer(file) && PIDE.resources.check_file(file))
if (files.nonEmpty) {
if (PIDE.options.bool("jedit_auto_load")) {