# HG changeset patch # User paulson # Date 1426595036 0 # Node ID 7fccaeec22f0789c47725b02d85d68dbe31ff465 # Parent b7c394c7a619f37d6bb88b6e3a610eb01a03a977# Parent 6c013328b885371f0ba06f49c18f2c4475337c31 Merge diff -r b7c394c7a619 -r 7fccaeec22f0 NEWS --- 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 diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/Bali/DeclConcepts.thy --- 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 \ (qtname \ methd) \ (qtname \ memberdecl)" + "method" :: "sig \ (qtname \ methd) \ (qtname \ memberdecl)" where "method sig m = (declclass m, mdecl (sig, mthd m))" lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))" diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/Codegenerator_Test/Candidates.thy --- 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 diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/Inequalities.thy --- /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 "(\(i,j)\{(i,j). i+j < n}. f i j) = (\ki\k. f i (k - i))" + apply (simp add: setsum.Sigma) + apply (rule setsum.reindex_bij_witness[where j="\(i, j). (i+j, i)" and i="\(k, i). (i, k - i)"]) + apply auto + done + +lemma gauss_sum_div2: "(2::'a::semiring_div) \ 0 \ + 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 \ m" and "(m::int) \ n" +shows "\ {m..n} = (n*(n+1) - m*(m-1)) div 2" +proof- + { fix k::int assume "k\0" + hence "\ {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\0` by auto + hence "\{m..n} = \{0..n} - \{0..m-1}" using assms + by (force intro!: setsum_diff) + also have "{0..n} = {0} Un {1..n}" using assms by auto + also have "\({0} \ {1..n}) = \{1..n}" by(simp add: setsum.union_disjoint) + also have "\ = 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 "\ \ = m*(m-1) div 2" using `m\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)) \ even(m*(m-1))") + by (auto (*simp: even_def[symmetric]*)) + finally show ?thesis . +qed + +lemma Setsum_Icc_nat: assumes "(m::nat) \ n" +shows "\ {m..n} = (n*(n+1) - m*(m-1)) div 2" +proof - + have "m*(m-1) \ n*(n + 1)" + using assms by (meson diff_le_self order_trans le_add1 mult_le_mono) + hence "int(\ {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) \ n" +shows "\ {m..{m..{m..n-1}" by simp + also have "\ = (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 "\ m < n" with assms show ?thesis by simp +qed + +lemma Chebyshev_sum_upper: + fixes a b::"nat \ 'a::linordered_idom" + assumes "\i j. i \ j \ j < n \ a i \ a j" + assumes "\i j. i \ j \ j < n \ b i \ b j" + shows "of_nat n * (\k=0.. (\k=0..k=0..j=0..j=0..k=0..i j. a i * b j"] setsum_right_distrib) + also + { fix i j::nat assume "i 0 \ b i - b j \ 0 \ a i - a j \ 0 \ b i - b j \ 0" + using assms by (cases "i \ j") (auto simp: algebra_simps) + } hence "?S \ 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 \ nat" + shows "(\i j. \ i\j; j \ a i \ a j) \ + (\i j. \ i\j; j \ b i \ b j) \ + n * (\i=0.. (\i=0..i=0.. ?rhs") unfolding le_Liminf_iff eventually_sequentially .. +lemma Liminf_add_le: + fixes f g :: "_ \ ereal" + assumes F: "F \ bot" + assumes ev: "eventually (\x. 0 \ f x) F" "eventually (\x. 0 \ g x) F" + shows "Liminf F f + Liminf F g \ Liminf F (\x. f x + g x)" + unfolding Liminf_def +proof (subst SUP_ereal_add_left[symmetric]) + let ?F = "{P. eventually P F}" + let ?INF = "\P g. INFIMUM (Collect P) g" + show "?F \ {}" + by (auto intro: eventually_True) + show "(SUP P:?F. ?INF P g) \ - \" + 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)) \ (SUP P:?F. (SUP P':?F. ?INF P f + ?INF P' g))" + proof (safe intro!: SUP_mono bexI[of _ "\x. P x \ 0 \ f x" for P]) + fix P let ?P' = "\x. P x \ 0 \ 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) \ ?INF ?P' f + (SUP P:?F. ?INF P g)" + by (intro ereal_add_mono INF_mono) auto + also have "\ = (SUP P':?F. ?INF ?P' f + ?INF P' g)" + proof (rule SUP_ereal_add_right[symmetric]) + show "INFIMUM {x. P x \ 0 \ f x} f \ - \" + 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) \ (SUP P':?F. ?INF ?P' f + ?INF P' g)" . + qed + also have "\ \ (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 \ (SUP P:?F. INF x:Collect P. f x + g x)" + proof (rule SUP_upper2) + show "(\x. P x \ Q x) \ ?F" + using * by (auto simp: eventually_conj) + show "?INF P f + ?INF Q g \ (INF x:{x. P x \ 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)) \ (SUP P:?F. INF x:Collect P. f x + g x)" . +qed + subsubsection {* Tests for code generator *} diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/MicroJava/BV/BVNoTypeError.thy --- 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 ("\") and Phi ("\") assumes wt: "wt_jvm_prog \ \" assumes is_class: "is_class \ C" - and method: "method (\,C) (m,[]) = Some (C, b)" + and "method": "method (\,C) (m,[]) = Some (C, b)" and m: "m \ init" defines start: "s \ start_state \ C m" assumes s: "\ \ (Normal s) \jvmd\ t" shows "t \ TypeError" proof - - from wt is_class method have "\,\ \JVM s \" + from wt is_class "method" have "\,\ \JVM s \" 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 ("\") and Phi ("\") assumes wt: "wt_jvm_prog \ \" assumes is_class: "is_class \ C" - and method: "method (\,C) (m,[]) = Some (C, b)" + and "method": "method (\,C) (m,[]) = Some (C, b)" and m: "m \ init" defines start: "s \ start_state \ C m" shows "\ \ (Normal s) \jvmd\ (Normal t) = \ \ s \jvm\ t" proof - - from wt is_class method have "\,\ \JVM s \" + from wt is_class "method" have "\,\ \JVM s \" unfolding start by (rule BV_correct_initial) with wt show ?thesis by (rule welltyped_commutes) qed diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- 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 @@ \ G,phi \JVM state'\" 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\h hp\" 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) diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/MicroJava/J/TypeRel.thy --- 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 \ cname => ( sig \ cname \ ty \ 'c)" (* ###curry *) + "method" :: "'c prog \ cname => ( sig \ cname \ ty \ 'c)" (* ###curry *) field :: "'c prog \ cname => ( vname \ cname \ ty )" (* ###curry *) fields :: "'c prog \ cname => ((vname \ cname) \ ty) list" (* ###curry *) diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/NSA/Examples/NSPrimes.thy --- 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})" diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/NSA/StarDef.thy --- 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 *} diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/NanoJava/TypeRel.thy --- 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 \ methd)" where +definition "method" :: "cname => (mname \ methd)" where "method C \ class_rec C methods" lemma method_rec: "\class C = Some m; ws_prog\ \ diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/Probability/Probability_Mass_Function.thy --- 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 \ Conditional Probabilities \ +lemma measure_pmf_zero_iff: "measure (measure_pmf p) s = 0 \ set_pmf p \ 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 \ s \ {}" @@ -854,32 +857,22 @@ qed lemma bind_cond_pmf_cancel: - assumes in_S: "\x. x \ set_pmf p \ x \ S x" "\x. x \ set_pmf q \ x \ S x" - assumes S_eq: "\x y. x \ S y \ S x = S y" - and same: "\x. measure (measure_pmf p) (S x) = measure (measure_pmf q) (S x)" - shows "bind_pmf p (\x. cond_pmf q (S x)) = q" (is "?lhs = _") + assumes [simp]: "\x. x \ set_pmf p \ set_pmf q \ {y. R x y} \ {}" + assumes [simp]: "\y. y \ set_pmf q \ set_pmf p \ {x. R x y} \ {}" + assumes [simp]: "\x y. x \ set_pmf p \ y \ set_pmf q \ R x y \ measure q {y. R x y} = measure p {x. R x y}" + shows "bind_pmf p (\x. cond_pmf q {y. R x y}) = q" proof (rule pmf_eqI) - { fix x - assume "x \ set_pmf p" - hence "set_pmf p \ (S x) \ {}" using in_S by auto - hence "measure (measure_pmf p) (S x) \ 0" - by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) - with same have "measure (measure_pmf q) (S x) \ 0" by simp - hence "set_pmf q \ S x \ {}" - by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) } - note [simp] = this - - fix z - have pmf_q_z: "z \ S z \ pmf q z = 0" - by(erule contrapos_np)(simp add: pmf_eq_0_set_pmf in_S) - - have "ereal (pmf ?lhs z) = \\<^sup>+ x. ereal (pmf (cond_pmf q (S x)) z) \measure_pmf p" - by(simp add: ereal_pmf_bind) - also have "\ = \\<^sup>+ x. ereal (pmf q z / measure p (S z)) * indicator (S z) x \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 "\ = 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 (\x. cond_pmf q {y. R x y})) i) = + (\\<^sup>+x. ereal (pmf q i / measure p {x. R x i}) * ereal (indicator {x. R x i} x) \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 "\ = (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 "\ = 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 (\x. cond_pmf q {y. R x y})) i = pmf q i" + by simp qed subsection \ Relator \ @@ -891,6 +884,136 @@ map_pmf fst pq = p; map_pmf snd pq = q \ \ rel_pmf R p q" +lemma rel_pmfI: + assumes R: "rel_set R (set_pmf p) (set_pmf q)" + assumes eq: "\x y. x \ set_pmf p \ y \ set_pmf q \ R x y \ + measure p {x. R x y} = measure q {y. R x y}" + shows "rel_pmf R p q" +proof + let ?pq = "bind_pmf p (\x. bind_pmf (cond_pmf q {y. R x y}) (\y. return_pmf (x, y)))" + have "\x. x \ set_pmf p \ set_pmf q \ {y. R x y} \ {}" + using R by (auto simp: rel_set_def) + then show "\x y. (x, y) \ set_pmf ?pq \ 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 \ 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: "\a b. R a b \ R a y \ R x b" + assumes "x \ set_pmf p" "y \ set_pmf q" + shows "measure p {x. R x y} = measure q {y. R x y}" +proof - + from rel_R obtain pq where pq: "\x y. (x, y) \ set_pmf pq \ 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 "\ = 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 "\ = 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 \ + rel_set R (set_pmf p) (set_pmf q) \ + (\x\set_pmf p. \y\set_pmf q. R x y \ 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 \symp R\] transpD[OF \transp R\]) + +lemma quotient_rel_set_disjoint: + "equivp R \ C \ UNIV // {(x, y). R x y} \ rel_set R A B \ A \ C = {} \ B \ 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 \ A \ X // R \ x \ A \ 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 \ (\C\UNIV // {(x, y). R x y}. measure p C = measure q C)" + (is "_ \ (\C\_//?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 \ UNIV // ?R" and R: "rel_set R (set_pmf p) (set_pmf q)" + assume eq: "\x\set_pmf p. \y\set_pmf q. R x y \ measure p {x. R x y} = measure q {y. R x y}" + + show "measure p C = measure q C" + proof cases + assume "p \ C = {}" + moreover then have "q \ 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 \ C \ {}" + moreover then have "q \ C \ {}" + using quotient_rel_set_disjoint[OF assms C R] by simp + ultimately obtain x y where in_set: "x \ set_pmf p" "y \ set_pmf q" and in_C: "x \ C" "y \ 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 \ C` C quotientD[of UNIV ?R C x] by (simp add: equivp_equiv) + moreover have "{x. R x y} = C" + using assms `y \ 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: "\C\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 \ set_pmf p" + have "{y. R x y} \ 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} \ 0" + using x assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp) + then show "\y\set_pmf q. R x y" + unfolding measure_pmf_zero_iff by auto + next + fix y assume y: "y \ set_pmf q" + have "{x. R x y} \ 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} \ 0" + using y assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp) + then show "\x\set_pmf p. R x y" + unfolding measure_pmf_zero_iff by auto + qed + + fix x y assume "x \ set_pmf p" "y \ set_pmf q" "R x y" + have "{y. R x y} \ 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 \ set_pmf p" thus "f x = g x" by simp } - fix R :: "'a => 'b \ bool" and S :: "'b \ 'c \ bool" + fix R :: "'a \ 'b \ bool" and S :: "'b \ 'c \ 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: "\y z. (y, z) \ set_pmf qr \ S y z" and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto - def pr \ "bind_pmf pq (\(x, y). bind_pmf (cond_pmf qr {(y', z). y' = y}) (\(y', z). return_pmf (x, z)))" - have pr_welldefined: "\y. y \ q \ qr \ {(y', z). y' = y} \ {}" + def pr \ "bind_pmf pq (\xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\yz. return_pmf (fst xy, snd yz)))" + have pr_welldefined: "\y. y \ q \ qr \ {yz. fst yz = y} \ {}" 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 (\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 (\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 \ 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\\) p q" -proof - let ?E = "\x. {y. R x y \ R y x}" - let ?\E = "\x. measure q (?E x)" - { fix x - have "measure p (?E x) = measure p ({y. R x y} - {y. R x y \ \ R y x})" - by(auto intro!: arg_cong[where f="measure p"]) - also have "\ = measure p {y. R x y} - measure p {y. R x y \ \ R y x}" - by (rule measure_pmf.finite_measure_Diff) auto - also have "measure p {y. R x y \ \ R y x} = measure q {y. R x y \ \ 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 \ ~ R y x} = - measure q ({y. R x y} - {y. R x y \ \ R y x})" - by(rule measure_pmf.finite_measure_Diff[symmetric]) auto - also have "\ = ?\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\\)" + using trans refl by (auto simp: equivp_reflp_symp_transp intro: sympI transpI reflpI dest: transpD reflpD) + + fix C assume "C \ UNIV // {(x, y). inf R R\\ x y}" + then obtain x where C: "C = {y. R x y \ R y x}" + by (auto elim: quotientE) - def pq \ "bind_pmf p (\x. bind_pmf (cond_pmf q (?E x)) (\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 \reflp R\] eq intro: transpD[OF \transp R\]) - - fix x y - assume "(x, y) \ set_pmf pq" - moreover - { assume "x \ set_pmf p" - hence "measure (measure_pmf p) (?E x) \ 0" - by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \reflp R\]) - hence "measure (measure_pmf q) (?E x) \ 0" using eq by simp - hence "set_pmf q \ {y. R x y \ R y x} \ {}" - by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) } - ultimately show "inf R R\\ x y" - by (auto simp add: pq_def) + let ?R = "\x y. R x y \ R y x" + let ?\R = "\y. measure q {x. ?R x y}" + have "measure p {y. ?R x y} = measure p ({y. R x y} - {y. R x y \ \ R y x})" + by(auto intro!: arg_cong[where f="measure p"]) + also have "\ = measure p {y. R x y} - measure p {y. R x y \ \ R y x}" + by (rule measure_pmf.finite_measure_Diff) auto + also have "measure p {y. R x y \ \ R y x} = measure q {y. R x y \ \ 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 \ \ R y x} = + measure q ({y. R x y} - {y. R x y \ \ R y x})" + by(rule measure_pmf.finite_measure_Diff[symmetric]) auto + also have "\ = ?\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: diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/Series.thy --- 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 "(\(i,j)\{(i,j). i+j < n}. f i j) = (\ki\k. f i (k - i))" - apply (simp add: setsum.Sigma) - apply (rule setsum.reindex_bij_witness[where j="\(i, j). (i+j, i)" and i="\(k, i). (i, k - i)"]) - apply auto - done - lemma Cauchy_product_sums: fixes a b :: "nat \ 'a::{real_normed_algebra,banach}" assumes a: "summable (\k. norm (a k))" diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 [] diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/Tools/BNF/bnf_comp.ML --- 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) = diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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 => diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/Tools/BNF/bnf_fp_util.ML --- 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 diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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, ...} :: _ => diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- 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; diff -r b7c394c7a619 -r 7fccaeec22f0 src/HOL/Transcendental.thy --- 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 \ 'a::banach" assumes f: "(\n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup" @@ -4372,7 +4375,6 @@ case False hence "0 < \x\" and "- \x\ < \x\" by auto have "suminf (?c (-\x\)) - arctan (-\x\) = suminf (?c 0) - arctan 0" - thm suminf_eq_arctan_bounded by (rule suminf_eq_arctan_bounded[where x1="0" and a1="-\x\" and b1="\x\", symmetric]) (simp_all only: `\x\ < r` `-\x\ < \x\` neg_less_iff_less) moreover diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/GUI/gui.scala --- 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 diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/General/exn.scala --- 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 diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/General/output.scala --- 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)) } } - diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/General/position.scala --- 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 _ => "" + }) } diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/Isar/keyword.ML --- 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; - diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/Isar/keyword.scala --- 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) }) } } - diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/Isar/outer_syntax.scala --- 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() } } diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/Isar/parse.ML --- 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 --| $$$ ")") ""; diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/Isar/parse.scala --- 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] = diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/Isar/token.scala --- 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 diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/PIDE/command.ML --- 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; diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/PIDE/command.scala --- 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 diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/PIDE/command_span.ML --- 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; - diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/PIDE/command_span.scala --- 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) - }) - } } - diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/PIDE/document.ML --- 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'); diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/PIDE/document.scala --- 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)) diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/PIDE/markup.scala --- 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)))) +} diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/PIDE/protocol.ML --- 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, diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/PIDE/protocol.scala --- 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), diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/PIDE/prover.scala --- 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 } diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/PIDE/resources.ML --- 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, _) = diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/PIDE/resources.scala --- 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 */ diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/System/options.scala --- 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) } diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/Thy/thy_header.ML --- 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)); diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/Thy/thy_header.scala --- 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)) })) } } - diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/Thy/thy_info.scala --- 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 => diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/Thy/thy_syntax.scala --- 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 diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/Tools/build.scala --- 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)] diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/library.scala --- 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) } diff -r b7c394c7a619 -r 7fccaeec22f0 src/Pure/raw_simplifier.ML --- 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 (); diff -r b7c394c7a619 -r 7fccaeec22f0 src/Tools/jEdit/src/document_model.scala --- 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)) diff -r b7c394c7a619 -r 7fccaeec22f0 src/Tools/jEdit/src/jedit_resources.scala --- 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 */ diff -r b7c394c7a619 -r 7fccaeec22f0 src/Tools/jEdit/src/plugin.scala --- 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")) {