# HG changeset patch # User wenzelm # Date 1394489031 -3600 # Node ID f78b4c3e8e843e61aaa947b2119a07c76398f56e # Parent e0c9d76c2a6de8028e96f07aee21fc0cc3698151# Parent 0b25c3d34b77425282c7b197b4ba404afc5b21ef merged diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/FOL/ex/Locale_Test/Locale_Test1.thy --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Mar 10 20:16:13 2014 +0100 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Mar 10 23:03:51 2014 +0100 @@ -150,7 +150,8 @@ ML {* fun check_syntax ctxt thm expected = let - val obtained = Print_Mode.setmp [] (Display.string_of_thm ctxt) thm; + val obtained = + Print_Mode.setmp [] (Display.string_of_thm (Config.put show_markup false ctxt)) thm; in if obtained <> expected then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.") diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Mar 10 20:16:13 2014 +0100 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Mar 10 23:03:51 2014 +0100 @@ -10,7 +10,7 @@ subsection{* Datatype of polynomial expressions *} -datatype poly = C Num| Bound nat| Add poly poly|Sub poly poly +datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \ C (0\<^sub>N)" @@ -142,7 +142,7 @@ fun polymul :: "poly \ poly \ poly" (infixl "*\<^sub>p" 60) where - "polymul (C c) (C c') = C (c*\<^sub>Nc')" + "polymul (C c) (C c') = C (c *\<^sub>N c')" | "polymul (C c) (CN c' n' p') = (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))" | "polymul (CN c n p) (C c') = @@ -556,7 +556,7 @@ let ?d1 = "degreen ?cnp m" let ?d2 = "degreen ?cnp' m" let ?eq = "?d = (if ?cnp = 0\<^sub>p \ ?cnp' = 0\<^sub>p then 0 else ?d1 + ?d2)" - have "n' n < n' \ n' = n" by auto + have "n' < n \ n < n' \ n' = n" by auto moreover { assume "n' < n \ n < n'" @@ -570,10 +570,16 @@ from "4.hyps"(16,18)[of n n' n] "4.hyps"(13,14)[of n "Suc n'" n] np np' nn' - have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n" - "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" - "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" - "?cnp *\<^sub>p p' \ 0\<^sub>p" by (auto simp add: min_def) + have norm: + "isnpolyh ?cnp n" + "isnpolyh c' (Suc n)" + "isnpolyh (?cnp *\<^sub>p c') n" + "isnpolyh p' n" + "isnpolyh (?cnp *\<^sub>p p') n" + "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" + "?cnp *\<^sub>p c' = 0\<^sub>p \ c' = 0\<^sub>p" + "?cnp *\<^sub>p p' \ 0\<^sub>p" + by (auto simp add: min_def) { assume mn: "m = n" from "4.hyps"(17,18)[OF norm(1,4), of n] @@ -627,7 +633,8 @@ case (2 n0 n1) then have np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1" - and m: "m \ min n0 n1" by simp_all + and m: "m \ min n0 n1" + by simp_all then have mn: "m \ n" by simp let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')" { @@ -700,10 +707,17 @@ assume pz: "p \ 0\<^sub>p" { assume hz: "INum ?h = (0::'a)" - from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" by simp_all - from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" by simp - with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast} - then show "INum (headconst p) = (0::'a) \ \p\\<^sub>p\<^bsup>bs\<^esup> = 0" by blast + from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" + by simp_all + from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" + by simp + with headconst_zero[OF np] have "p = 0\<^sub>p" + by blast + with pz have False + by blast + } + then show "INum (headconst p) = (0::'a) \ \p\\<^sub>p\<^bsup>bs\<^esup> = 0" + by blast qed @@ -755,33 +769,42 @@ "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field_inverse_zero}) ^ n" proof (induct n rule: polypow.induct) case 1 - then show ?case by simp + then show ?case + by simp next case (2 n) let ?q = "polypow ((Suc n) div 2) p" let ?d = "polymul ?q ?q" - have "odd (Suc n) \ even (Suc n)" by simp + have "odd (Suc n) \ even (Suc n)" + by simp moreover - { assume odd: "odd (Suc n)" + { + assume odd: "odd (Suc n)" have th: "(Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0)))) = Suc n div 2 + Suc n div 2 + 1" by arith - from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" by (simp add: Let_def) - also have "\ = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2)*(Ipoly bs p)^(Suc n div 2)" + from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" + by (simp add: Let_def) + also have "\ = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2) * (Ipoly bs p)^(Suc n div 2)" using "2.hyps" by simp also have "\ = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)" by (simp only: power_add power_one_right) simp also have "\ = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))" by (simp only: th) finally have ?case - using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp } + using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp + } moreover - { assume even: "even (Suc n)" + { + assume even: "even (Suc n)" have th: "(Suc (Suc 0)) * (Suc n div Suc (Suc 0)) = Suc n div 2 + Suc n div 2" by arith - from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" by (simp add: Let_def) + from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" + by (simp add: Let_def) also have "\ = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)" - using "2.hyps" apply (simp only: power_add) by simp - finally have ?case using even_nat_div_two_times_two[OF even] by (simp only: th)} + using "2.hyps" by (simp only: power_add) simp + finally have ?case using even_nat_div_two_times_two[OF even] + by (simp only: th) + } ultimately show ?case by blast qed @@ -789,14 +812,21 @@ assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" shows "isnpolyh p n \ isnpolyh (polypow k p) n" proof (induct k arbitrary: n rule: polypow.induct) + case 1 + then show ?case by auto +next case (2 k n) let ?q = "polypow (Suc k div 2) p" let ?d = "polymul ?q ?q" - from 2 have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+ - from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp - from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n" by simp - from dn on show ?case by (simp add: Let_def) -qed auto + from 2 have th1: "isnpolyh ?q n" and th2: "isnpolyh p n" + by blast+ + from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" + by simp + from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n" + by simp + from dn on show ?case + by (simp add: Let_def) +qed lemma polypow_norm: assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" @@ -830,12 +860,12 @@ lemma shift1_nz[simp]:"shift1 p \ 0\<^sub>p" by (simp add: shift1_def) -lemma funpow_shift1_isnpoly: - "\ isnpoly p ; p \ 0\<^sub>p\ \ isnpoly (funpow n shift1 p)" + +lemma funpow_shift1_isnpoly: "isnpoly p \ p \ 0\<^sub>p \ isnpoly (funpow n shift1 p)" by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1) lemma funpow_isnpolyh: - assumes f: "\ p. isnpolyh p n \ isnpolyh (f p) n" + assumes f: "\p. isnpolyh p n \ isnpolyh (f p) n" and np: "isnpolyh p n" shows "isnpolyh (funpow k f p) n" using f np by (induct k arbitrary: p) auto @@ -845,7 +875,7 @@ Ipoly bs (Mul (Pw (Bound 0) n) p)" by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1) -lemma shift1_isnpolyh: "isnpolyh p n0 \ p\ 0\<^sub>p \ isnpolyh (shift1 p) 0" +lemma shift1_isnpolyh: "isnpolyh p n0 \ p \ 0\<^sub>p \ isnpolyh (shift1 p) 0" using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def) lemma funpow_shift1_1: @@ -900,7 +930,7 @@ lemma decrpoly_normh: "isnpolyh p n0 \ polybound0 p \ isnpolyh (decrpoly p) (n0 - 1)" apply (induct p arbitrary: n0) apply auto - apply (atomize) + apply atomize apply (erule_tac x = "Suc nat" in allE) apply auto done @@ -924,7 +954,7 @@ lemma decrpoly: assumes nb: "polybound0 t" - shows "Ipoly (x#bs) t = Ipoly bs (decrpoly t)" + shows "Ipoly (x # bs) t = Ipoly bs (decrpoly t)" using nb by (induct t rule: decrpoly.induct) simp_all lemma polysubst0_polybound0: @@ -935,7 +965,8 @@ lemma degree0_polybound0: "isnpolyh p n \ degree p = 0 \ polybound0 p" by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0) -primrec maxindex :: "poly \ nat" where +primrec maxindex :: "poly \ nat" +where "maxindex (Bound n) = n + 1" | "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))" | "maxindex (Add p q) = max (maxindex p) (maxindex q)" @@ -948,7 +979,7 @@ definition wf_bs :: "'a list \ poly \ bool" where "wf_bs bs p \ length bs \ maxindex p" -lemma wf_bs_coefficients: "wf_bs bs p \ \ c \ set (coefficients p). wf_bs bs c" +lemma wf_bs_coefficients: "wf_bs bs p \ \c \ set (coefficients p). wf_bs bs c" proof (induct p rule: coefficients.induct) case (1 c p) show ?case @@ -961,7 +992,7 @@ { assume "x = c" then have "wf_bs bs x" - using "1.prems" unfolding wf_bs_def by simp + using "1.prems" unfolding wf_bs_def by simp } moreover { @@ -976,7 +1007,7 @@ qed qed simp_all -lemma maxindex_coefficients: "\c\ set (coefficients p). maxindex c \ maxindex p" +lemma maxindex_coefficients: "\c \ set (coefficients p). maxindex c \ maxindex p" by (induct p rule: coefficients.induct) auto lemma wf_bs_I: "wf_bs bs p \ Ipoly (bs @ bs') p = Ipoly bs p" @@ -992,7 +1023,7 @@ unfolding wf_bs_def by simp then have wf': "wf_bs ?tbs p" unfolding wf_bs_def by simp - have eq: "bs = ?tbs @ (drop ?ip bs)" + have eq: "bs = ?tbs @ drop ?ip bs" by simp from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis using eq by simp @@ -1007,26 +1038,24 @@ lemma wf_bs_insensitive': "wf_bs (x#bs) p = wf_bs (y#bs) p" unfolding wf_bs_def by simp - - lemma wf_bs_coefficients': "\c \ set (coefficients p). wf_bs bs c \ wf_bs (x#bs) p" by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def) + lemma coefficients_Nil[simp]: "coefficients p \ []" by (induct p rule: coefficients.induct) simp_all - lemma coefficients_head: "last (coefficients p) = head p" by (induct p rule: coefficients.induct) auto lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \ wf_bs (x#bs) p" unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto -lemma length_le_list_ex: "length xs \ n \ \ ys. length (xs @ ys) = n" +lemma length_le_list_ex: "length xs \ n \ \ys. length (xs @ ys) = n" apply (rule exI[where x="replicate (n - length xs) z"]) apply simp done -lemma isnpolyh_Suc_const:"isnpolyh p (Suc n) \ isconstant p" +lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \ isconstant p" apply (cases p) apply auto apply (case_tac "nat") @@ -1052,16 +1081,17 @@ unfolding wf_bs_def by (induct p rule: polyneg.induct) auto lemma wf_bs_polysub: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p -\<^sub>p q)" - unfolding polysub_def split_def fst_conv snd_conv using wf_bs_polyadd wf_bs_polyneg by blast + unfolding polysub_def split_def fst_conv snd_conv + using wf_bs_polyadd wf_bs_polyneg by blast -subsection{* Canonicity of polynomial representation, see lemma isnpolyh_unique*} +subsection {* Canonicity of polynomial representation, see lemma isnpolyh_unique *} definition "polypoly bs p = map (Ipoly bs) (coefficients p)" -definition "polypoly' bs p = map ((Ipoly bs o decrpoly)) (coefficients p)" -definition "poly_nate bs p = map ((Ipoly bs o decrpoly)) (coefficients (polynate p))" +definition "polypoly' bs p = map (Ipoly bs \ decrpoly) (coefficients p)" +definition "poly_nate bs p = map (Ipoly bs \ decrpoly) (coefficients (polynate p))" -lemma coefficients_normh: "isnpolyh p n0 \ \ q \ set (coefficients p). isnpolyh q n0" +lemma coefficients_normh: "isnpolyh p n0 \ \q \ set (coefficients p). isnpolyh q n0" proof (induct p arbitrary: n0 rule: coefficients.induct) case (1 c p n0) have cp: "isnpolyh (CN c 0 p) n0" @@ -1072,44 +1102,51 @@ by simp qed auto -lemma coefficients_isconst: - "isnpolyh p n \ \q\set (coefficients p). isconstant q" - by (induct p arbitrary: n rule: coefficients.induct) - (auto simp add: isnpolyh_Suc_const) +lemma coefficients_isconst: "isnpolyh p n \ \q \ set (coefficients p). isconstant q" + by (induct p arbitrary: n rule: coefficients.induct) (auto simp add: isnpolyh_Suc_const) lemma polypoly_polypoly': assumes np: "isnpolyh p n0" - shows "polypoly (x#bs) p = polypoly' bs p" -proof- + shows "polypoly (x # bs) p = polypoly' bs p" +proof - let ?cf = "set (coefficients p)" from coefficients_normh[OF np] have cn_norm: "\ q\ ?cf. isnpolyh q n0" . - {fix q assume q: "q \ ?cf" - from q cn_norm have th: "isnpolyh q n0" by blast - from coefficients_isconst[OF np] q have "isconstant q" by blast - with isconstant_polybound0[OF th] have "polybound0 q" by blast} + { + fix q + assume q: "q \ ?cf" + from q cn_norm have th: "isnpolyh q n0" + by blast + from coefficients_isconst[OF np] q have "isconstant q" + by blast + with isconstant_polybound0[OF th] have "polybound0 q" + by blast + } then have "\q \ ?cf. polybound0 q" .. - then have "\q \ ?cf. Ipoly (x#bs) q = Ipoly bs (decrpoly q)" + then have "\q \ ?cf. Ipoly (x # bs) q = Ipoly bs (decrpoly q)" using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs] by auto - then show ?thesis unfolding polypoly_def polypoly'_def by simp + then show ?thesis + unfolding polypoly_def polypoly'_def by simp qed lemma polypoly_poly: - assumes np: "isnpolyh p n0" - shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x" - using np + assumes "isnpolyh p n0" + shows "Ipoly (x # bs) p = poly (polypoly (x # bs) p) x" + using assms by (induct p arbitrary: n0 bs rule: coefficients.induct) (auto simp add: polypoly_def) lemma polypoly'_poly: - assumes np: "isnpolyh p n0" + assumes "isnpolyh p n0" shows "\p\\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x" - using polypoly_poly[OF np, simplified polypoly_polypoly'[OF np]] . + using polypoly_poly[OF assms, simplified polypoly_polypoly'[OF assms]] . lemma polypoly_poly_polybound0: - assumes np: "isnpolyh p n0" and nb: "polybound0 p" + assumes "isnpolyh p n0" + and "polybound0 p" shows "polypoly bs p = [Ipoly bs p]" - using np nb unfolding polypoly_def + using assms + unfolding polypoly_def apply (cases p) apply auto apply (case_tac nat) @@ -1119,13 +1156,13 @@ lemma head_isnpolyh: "isnpolyh p n0 \ isnpolyh (head p) n0" by (induct p rule: head.induct) auto -lemma headn_nz[simp]: "isnpolyh p n0 \ (headn p m = 0\<^sub>p) = (p = 0\<^sub>p)" +lemma headn_nz[simp]: "isnpolyh p n0 \ headn p m = 0\<^sub>p \ p = 0\<^sub>p" by (cases p) auto lemma head_eq_headn0: "head p = headn p 0" by (induct p rule: head.induct) simp_all -lemma head_nz[simp]: "isnpolyh p n0 \ (head p = 0\<^sub>p) = (p = 0\<^sub>p)" +lemma head_nz[simp]: "isnpolyh p n0 \ head p = 0\<^sub>p \ p = 0\<^sub>p" by (simp add: head_eq_headn0) lemma isnpolyh_zero_iff: @@ -1269,7 +1306,8 @@ and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p *\<^sub>p q = q *\<^sub>p p" - using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a::{field_char_0,field_inverse_zero, power}"] + using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], + where ?'a = "'a::{field_char_0,field_inverse_zero, power}"] by simp declare polyneg_polyneg [simp] @@ -1278,7 +1316,9 @@ assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" and np: "isnpolyh p n0" shows "polynate p = p" - using isnpolyh_unique[where ?'a= "'a::{field_char_0,field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0,field_inverse_zero}"] + using isnpolyh_unique[where ?'a= "'a::{field_char_0,field_inverse_zero}", + OF polynate_norm[of p, unfolded isnpoly_def] np] + polynate[where ?'a = "'a::{field_char_0,field_inverse_zero}"] by simp lemma polynate_idempotent[simp]: @@ -1301,16 +1341,18 @@ by (induct p rule: degree.induct) simp_all lemma degree_polyneg: - assumes n: "isnpolyh p n" + assumes "isnpolyh p n" shows "degree (polyneg p) = degree p" - apply (induct p arbitrary: n rule: polyneg.induct) - using n apply simp_all + apply (induct p rule: polyneg.induct) + using assms + apply simp_all apply (case_tac na) apply auto done lemma degree_polyadd: - assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" + assumes np: "isnpolyh p n0" + and nq: "isnpolyh q n1" shows "degree (p +\<^sub>p q) \ max (degree p) (degree q)" using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp @@ -1320,13 +1362,17 @@ and nq: "isnpolyh q n1" shows "degree (p -\<^sub>p q) \ max (degree p) (degree q)" proof- - from nq have nq': "isnpolyh (~\<^sub>p q) n1" using polyneg_normh by simp - from degree_polyadd[OF np nq'] show ?thesis by (simp add: polysub_def degree_polyneg[OF nq]) + from nq have nq': "isnpolyh (~\<^sub>p q) n1" + using polyneg_normh by simp + from degree_polyadd[OF np nq'] show ?thesis + by (simp add: polysub_def degree_polyneg[OF nq]) qed lemma degree_polysub_samehead: assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" - and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" + and np: "isnpolyh p n0" + and nq: "isnpolyh q n1" + and h: "head p = head q" and d: "degree p = degree q" shows "degree (p -\<^sub>p q) < degree p \ (p -\<^sub>p q = 0\<^sub>p)" unfolding polysub_def split_def fst_conv snd_conv diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/HOL/Mutabelle/mutabelle.ML --- a/src/HOL/Mutabelle/mutabelle.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/HOL/Mutabelle/mutabelle.ML Mon Mar 10 23:03:51 2014 +0100 @@ -32,11 +32,11 @@ fun consts_of thy = let - val (namespace, const_table) = #constants (Consts.dest (Sign.consts_of thy)) - val consts = Symtab.dest const_table + val {const_space, constants, ...} = Consts.dest (Sign.consts_of thy) + val consts = Symtab.dest constants in map_filter (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE) - (filter_out (fn (s, _) => Name_Space.is_concealed namespace s) consts) + (filter_out (fn (s, _) => Name_Space.is_concealed const_space s) consts) end; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Mar 10 23:03:51 2014 +0100 @@ -223,7 +223,7 @@ val dummy_thm = Thm.transfer thy Drule.dummy_thm val pointer = Outer_Syntax.scan Position.none bundle_name val restore_lifting_att = - ([dummy_thm], [Args.src (("Lifting.lifting_restore_internal", pointer), Position.none)]) + ([dummy_thm], [Args.src ("Lifting.lifting_restore_internal", Position.none) pointer]) in lthy |> Local_Theory.declaration {syntax = false, pervasive = true} @@ -954,17 +954,14 @@ fun pointer_of_bundle_name bundle_name ctxt = let - val bundle_name = Bundle.check ctxt bundle_name - val bundle = Bundle.the_bundle ctxt bundle_name + val bundle = Bundle.get_bundle_cmd ctxt bundle_name in case bundle of [(_, [arg_src])] => - (let - val ((_, tokens), _) = Args.dest_src arg_src - in - (fst (Args.name tokens)) - handle _ => error "The provided bundle is not a lifting bundle." - end) + let + val (name, _) = Args.syntax (Scan.lift Args.name) arg_src ctxt + handle ERROR _ => error "The provided bundle is not a lifting bundle." + in name end | _ => error "The provided bundle is not a lifting bundle." end diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/HOL/Tools/inductive.ML Mon Mar 10 23:03:51 2014 +0100 @@ -230,7 +230,7 @@ [Pretty.block (Pretty.breaks (Pretty.str "(co)inductives:" :: - map (Pretty.mark_str o #1) (Name_Space.extern_table ctxt (space, infos)))), + map (Pretty.mark_str o #1) (Name_Space.extern_table' ctxt space infos))), Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)] end |> Pretty.chunks |> Pretty.writeln; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/HOL/Tools/recdef.ML Mon Mar 10 23:03:51 2014 +0100 @@ -164,7 +164,7 @@ val ctxt = (case opt_src of NONE => ctxt0 - | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0)); + | SOME src => #2 (Args.syntax (Method.sections recdef_modifiers) src ctxt0)); val {simps, congs, wfs} = get_hints ctxt; val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong}; in (ctxt', rev (map snd congs), wfs) end; @@ -290,7 +290,8 @@ val hints = @{keyword "("} |-- - Parse.!!! (Parse.position (@{keyword "hints"} -- Args.parse) --| @{keyword ")"}) >> Args.src; + Parse.!!! (Parse.position @{keyword "hints"} -- Args.parse --| @{keyword ")"}) + >> uncurry Args.src; val recdef_decl = Scan.optional diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/HOL/Tools/try0.ML diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/General/completion.scala Mon Mar 10 23:03:51 2014 +0100 @@ -211,13 +211,13 @@ private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r - private val word_regex = "[a-zA-Z0-9_']+".r + private val word_regex = "[a-zA-Z0-9_'.]+".r private def word: Parser[String] = word_regex - private def word3: Parser[String] = "[a-zA-Z0-9_']{3,}".r + private def word3: Parser[String] = "[a-zA-Z0-9_'.]{3,}".r private def underscores: Parser[String] = "_*".r def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches - def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) + def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.' def extend_word(text: CharSequence, offset: Text.Offset): Text.Offset = { diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/General/long_name.ML --- a/src/Pure/General/long_name.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/General/long_name.ML Mon Mar 10 23:03:51 2014 +0100 @@ -13,6 +13,7 @@ val implode: string list -> string val explode: string -> string list val append: string -> string -> string + val qualification: string -> int val qualify: string -> string -> string val qualifier: string -> string val base_name: string -> string @@ -35,6 +36,9 @@ | append "" name2 = name2 | append name1 name2 = name1 ^ separator ^ name2; +fun qualification "" = 0 + | qualification name = fold_string (fn s => s = separator ? Integer.add 1) name 1; + fun qualify qual name = if qual = "" orelse name = "" then name else qual ^ separator ^ name; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/General/name_space.ML Mon Mar 10 23:03:51 2014 +0100 @@ -54,17 +54,26 @@ val naming_of: Context.generic -> naming val map_naming: (naming -> naming) -> Context.generic -> Context.generic val declare: Context.generic -> bool -> binding -> T -> string * T - type 'a table = T * 'a Symtab.table + type 'a table + val space_of_table: 'a table -> T val check_reports: Context.generic -> 'a table -> xstring * Position.T list -> (string * Position.report list) * 'a val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a + val lookup_key: 'a table -> string -> (string * 'a) option val get: 'a table -> string -> 'a val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table + val alias_table: naming -> binding -> string -> 'a table -> 'a table + val hide_table: bool -> string -> 'a table -> 'a table + val del_table: string -> 'a table -> 'a table + val map_table_entry: string -> ('a -> 'a) -> 'a table -> 'a table + val fold_table: (string * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b val empty_table: string -> 'a table val merge_tables: 'a table * 'a table -> 'a table val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) -> 'a table * 'a table -> 'a table - val dest_table: Proof.context -> 'a table -> (string * 'a) list + val dest_table': Proof.context -> T -> 'a Symtab.table -> ((string * xstring) * 'a) list + val dest_table: Proof.context -> 'a table -> ((string * xstring) * 'a) list + val extern_table': Proof.context -> T -> 'a Symtab.table -> ((Markup.T * xstring) * 'a) list val extern_table: Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list end; @@ -90,10 +99,10 @@ quote (Markup.markup (entry_markup false kind (name, entry)) name); fun err_dup kind entry1 entry2 pos = - error ("Duplicate " ^ kind ^ " declaration " ^ + error ("Duplicate " ^ plain_words kind ^ " declaration " ^ print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos); -fun undefined kind name = "Undefined " ^ kind ^ ": " ^ quote name; +fun undefined kind name = "Undefined " ^ plain_words kind ^ ": " ^ quote name; (* datatype T *) @@ -207,6 +216,10 @@ fun completion context space (xname, pos) = if Position.is_reported pos andalso xname <> "" andalso xname <> "_" then let + fun result_ord ((s, _), (s', _)) = + (case int_ord (pairself Long_Name.qualification (s, s')) of + EQUAL => string_ord (s, s') + | ord => ord); val x = Name.clean xname; val Name_Space {kind, internals, ...} = space; val ext = extern_shortest (Context.proof_of context) space; @@ -214,9 +227,12 @@ Symtab.fold (fn (a, (name :: _, _)) => if String.isPrefix x a andalso not (is_concealed space name) - then cons (ext name, (kind, name)) else I + then + let val a' = ext name + in if a = a' then cons (a', (kind, name)) else I end + else I | _ => I) internals [] - |> sort_distinct (string_ord o pairself #1); + |> sort_distinct result_ord; in Completion.names pos names end else Completion.none; @@ -448,9 +464,11 @@ (* definition in symbol table *) -type 'a table = T * 'a Symtab.table; +datatype 'a table = Table of T * 'a Symtab.table; -fun check_reports context (space, tab) (xname, ps) = +fun space_of_table (Table (space, _)) = space; + +fun check_reports context (Table (space, tab)) (xname, ps) = let val name = intern space xname in (case Symtab.lookup tab name of SOME x => @@ -474,31 +492,61 @@ val _ = Position.reports reports; in (name, x) end; -fun get (space, tab) name = - (case Symtab.lookup tab name of - SOME x => x - | NONE => error (undefined (kind_of space) name)); +fun lookup_key (Table (_, tab)) name = Symtab.lookup_key tab name; + +fun get table name = + (case lookup_key table name of + SOME (_, x) => x + | NONE => error (undefined (kind_of (space_of_table table)) name)); -fun define context strict (binding, x) (space, tab) = - let val (name, space') = declare context strict binding space - in (name, (space', Symtab.update (name, x) tab)) end; +fun define context strict (binding, x) (Table (space, tab)) = + let + val (name, space') = declare context strict binding space; + val tab' = Symtab.update (name, x) tab; + in (name, Table (space', tab')) end; + + +(* derived table operations *) + +fun alias_table naming binding name (Table (space, tab)) = + Table (alias naming binding name space, tab); + +fun hide_table fully name (Table (space, tab)) = + Table (hide fully name space, tab); -fun empty_table kind = (empty kind, Symtab.empty); +fun del_table name (Table (space, tab)) = + let + val space' = hide true name space handle ERROR _ => space; + val tab' = Symtab.delete_safe name tab; + in Table (space', tab') end; -fun merge_tables ((space1, tab1), (space2, tab2)) = - (merge (space1, space2), Symtab.merge (K true) (tab1, tab2)); +fun map_table_entry name f (Table (space, tab)) = + Table (space, Symtab.map_entry name f tab); + +fun fold_table f (Table (_, tab)) = Symtab.fold f tab; -fun join_tables f ((space1, tab1), (space2, tab2)) = - (merge (space1, space2), Symtab.join f (tab1, tab2)); +fun empty_table kind = Table (empty kind, Symtab.empty); + +fun merge_tables (Table (space1, tab1), Table (space2, tab2)) = + Table (merge (space1, space2), Symtab.merge (K true) (tab1, tab2)); -fun ext_table ctxt (space, tab) = +fun join_tables f (Table (space1, tab1), Table (space2, tab2)) = + Table (merge (space1, space2), Symtab.join f (tab1, tab2)); + + +(* present table content *) + +fun dest_table' ctxt space tab = Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab [] |> Library.sort_wrt (#2 o #1); -fun dest_table ctxt table = map (apfst #1) (ext_table ctxt table); +fun dest_table ctxt (Table (space, tab)) = dest_table' ctxt space tab; -fun extern_table ctxt (space, tab) = - map (fn ((name, xname), x) => ((markup space name, xname), x)) (ext_table ctxt (space, tab)); +fun extern_table' ctxt space tab = + dest_table' ctxt space tab + |> map (fn ((name, xname), x) => ((markup space name, xname), x)); + +fun extern_table ctxt (Table (space, tab)) = extern_table' ctxt space tab; end; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/Isar/args.ML Mon Mar 10 23:03:51 2014 +0100 @@ -8,10 +8,12 @@ signature ARGS = sig type src - val src: (string * Token.T list) * Position.T -> src - val dest_src: src -> (string * Token.T list) * Position.T + val src: xstring * Position.T -> Token.T list -> src + val name_of_src: src -> string * Position.T + val range_of_src: src -> Position.T + val unparse_src: src -> string list val pretty_src: Proof.context -> src -> Pretty.T - val map_name: (string -> string) -> src -> src + val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a val transform_values: morphism -> src -> src val init_assignable: src -> src val closure: src -> src @@ -65,8 +67,8 @@ val opt_attribs: (xstring * Position.T -> string) -> src list parser val thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser val opt_thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser - val syntax: string -> 'a context_parser -> src -> Context.generic -> 'a * Context.generic - val context_syntax: string -> 'a context_parser -> src -> Proof.context -> 'a * Proof.context + val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic + val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context end; structure Args: ARGS = @@ -74,15 +76,31 @@ (** datatype src **) -datatype src = Src of (string * Token.T list) * Position.T; +datatype src = + Src of + {name: string * Position.T, + args: Token.T list, + output_info: (string * Markup.T) option}; + +fun src name args = Src {name = name, args = args, output_info = NONE}; -val src = Src; -fun dest_src (Src src) = src; +fun name_of_src (Src {name, ...}) = name; + +fun range_of_src (Src {name = (_, pos), args, ...}) = + if null args then pos + else Position.set_range (pos, #2 (Token.range_of args)); + +fun unparse_src (Src {args, ...}) = map Token.unparse args; fun pretty_src ctxt src = let + val Src {name = (name, _), args, output_info} = src; + val prt_name = + (case output_info of + NONE => Pretty.str name + | SOME (_, markup) => Pretty.mark_str (markup, name)); val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; - fun prt arg = + fun prt_arg arg = (case Token.get_value arg of SOME (v as Token.Literal s) => Pretty.marks_str (Token.value_markup v, s) | SOME (Token.Text s) => Pretty.str (quote s) @@ -90,15 +108,25 @@ | SOME (Token.Term t) => Syntax.pretty_term ctxt t | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg)); - val (s, args) = #1 (dest_src src); - in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end; + in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end; + + +(* check *) -fun map_name f (Src ((s, args), pos)) = Src ((f s, args), pos); -fun map_args f (Src ((s, args), pos)) = Src ((s, map f args), pos); +fun check_src ctxt table (Src {name = (xname, pos), args, output_info}) = + let + val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos); + val space = Name_Space.space_of_table table; + val kind = Name_Space.kind_of space; + val markup = Name_Space.markup space name; + in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end; (* values *) +fun map_args f (Src {name, args, output_info}) = + Src {name = name, args = map f args, output_info = output_info}; + fun transform_values phi = map_args (Token.map_value (fn Token.Typ T => Token.Typ (Morphism.typ phi T) | Token.Term t => Token.Term (Morphism.term phi t) @@ -265,7 +293,7 @@ let fun intern tok = check (Token.content_of tok, Token.pos_of tok); val attrib_name = internal_text || (symbolic || named) >> evaluate Token.Text intern; - val attrib = Parse.position (attrib_name -- Parse.!!! parse) >> src; + val attrib = Parse.position attrib_name -- Parse.!!! parse >> uncurry src; in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end; fun opt_attribs check = Scan.optional (attribs check) []; @@ -284,7 +312,7 @@ (** syntax wrapper **) -fun syntax kind scan (Src ((s, args0), pos)) context = +fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context = let val args1 = map Token.init_assignable args0; fun reported_text () = @@ -295,14 +323,23 @@ else ""; in (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (context, args1) of - (SOME x, (context', [])) => (Output.report (reported_text ()); (x, context')) + (SOME x, (context', [])) => + let val _ = Output.report (reported_text ()) + in (x, context') end | (_, (_, args2)) => - error ("Bad arguments for " ^ kind ^ " " ^ quote s ^ Position.here pos ^ - (if null args2 then "" else ":\n " ^ space_implode " " (map Token.print args2)) ^ - Markup.markup_report (reported_text ()))) + let + val print_name = + (case output_info of + NONE => quote name + | SOME (kind, markup) => plain_words kind ^ " " ^ quote (Markup.markup markup name)); + val print_args = + if null args2 then "" else ":\n " ^ space_implode " " (map Token.print args2); + in + error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^ + Markup.markup_report (reported_text ())) + end) end; -fun context_syntax kind scan src = - apsnd Context.the_proof o syntax kind scan src o Context.Proof; +fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof; end; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/Isar/attrib.ML Mon Mar 10 23:03:51 2014 +0100 @@ -12,7 +12,6 @@ val is_empty_binding: binding -> bool val print_attributes: Proof.context -> unit val check_name_generic: Context.generic -> xstring * Position.T -> string - val check_src_generic: Context.generic -> src -> src val check_name: Proof.context -> xstring * Position.T -> string val check_src: Proof.context -> src -> src val pretty_attribs: Proof.context -> src list -> Pretty.T list @@ -109,6 +108,8 @@ |> Pretty.chunks |> Pretty.writeln end; +val attribute_space = Name_Space.space_of_table o get_attributes o Context.Proof; + fun add_attribute name att comment thy = thy |> Attributes.map (Name_Space.define (Context.Theory thy) true (name, (att, comment)) #> snd); @@ -116,43 +117,30 @@ (* check *) fun check_name_generic context = #1 o Name_Space.check context (get_attributes context); +val check_name = check_name_generic o Context.Proof; -fun check_src_generic context src = - let - val ((xname, toks), pos) = Args.dest_src src; - val name = check_name_generic context (xname, pos); - in Args.src ((name, toks), pos) end; - -val check_name = check_name_generic o Context.Proof; -val check_src = check_src_generic o Context.Proof; +fun check_src ctxt src = + (Context_Position.report ctxt (Args.range_of_src src) Markup.language_attribute; + #1 (Args.check_src ctxt (get_attributes (Context.Proof ctxt)) src)); (* pretty printing *) -fun extern ctxt = Name_Space.extern ctxt (#1 (get_attributes (Context.Proof ctxt))); - fun pretty_attribs _ [] = [] - | pretty_attribs ctxt srcs = - [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)]; + | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt) srcs)]; (* get attributes *) fun attribute_generic context = - let val (_, tab) = get_attributes context in - fn src => - let val ((name, _), pos) = Args.dest_src src in - (case Symtab.lookup tab name of - NONE => error ("Undefined attribute: " ^ quote name ^ Position.here pos) - | SOME (att, _) => att src) - end - end; + let val table = get_attributes context + in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end; val attribute = attribute_generic o Context.Proof; val attribute_global = attribute_generic o Context.Theory; fun attribute_cmd ctxt = attribute ctxt o check_src ctxt; -fun attribute_cmd_global thy = attribute_global thy o check_src_generic (Context.Theory thy); +fun attribute_cmd_global thy = attribute_global thy o check_src (Proof_Context.init_global thy); (* attributed declarations *) @@ -183,11 +171,10 @@ (* attribute setup *) -fun syntax scan = Args.syntax "attribute" scan; - fun setup name scan = add_attribute name - (fn src => fn (ctxt, th) => let val (a, ctxt') = syntax scan src ctxt in a (ctxt', th) end); + (fn src => fn (ctxt, th) => + let val (a, ctxt') = Args.syntax_generic scan src ctxt in a (ctxt', th) end); fun attribute_setup name source cmt = Context.theory_map (ML_Context.expression (#pos source) @@ -200,7 +187,7 @@ (* internal attribute *) -fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none); +fun internal att = Args.src ("Pure.attribute", Position.none) [Token.mk_attribute att]; val _ = Theory.setup (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form) @@ -272,7 +259,7 @@ in (src2, result) end; fun err msg src = - let val ((name, _), pos) = Args.dest_src src + let val (name, pos) = Args.name_of_src src in error (msg ^ " " ^ quote name ^ Position.here pos) end; fun eval src ((th, dyn), (decls, context)) = @@ -349,8 +336,8 @@ Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="), Pretty.brk 1, Pretty.str (Config.print_value value)] end; - val space = #1 (get_attributes (Context.Proof ctxt)); - val configs = Name_Space.extern_table ctxt (space, Configs.get (Proof_Context.theory_of ctxt)); + val space = attribute_space ctxt; + val configs = Name_Space.extern_table' ctxt space (Configs.get (Proof_Context.theory_of ctxt)); in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/Isar/bundle.ML Mon Mar 10 23:03:51 2014 +0100 @@ -7,8 +7,9 @@ signature BUNDLE = sig type bundle = (thm list * Args.src list) list - val the_bundle: Proof.context -> string -> bundle val check: Proof.context -> xstring * Position.T -> string + val get_bundle: Proof.context -> string -> bundle + val get_bundle_cmd: Proof.context -> xstring * Position.T -> bundle val bundle: binding * (thm list * Args.src list) list -> (binding * typ option * mixfix) list -> local_theory -> local_theory val bundle_cmd: binding * (Facts.ref * Args.src list) list -> @@ -45,12 +46,10 @@ val get_bundles = Data.get o Context.Proof; -fun the_bundle ctxt name = - (case Symtab.lookup (#2 (get_bundles ctxt)) name of - SOME bundle => bundle - | NONE => error ("Unknown bundle " ^ quote name)); +fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt); -fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt); +val get_bundle = Name_Space.get o get_bundles; +fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt; (* define bundle *) @@ -85,17 +84,17 @@ local -fun gen_includes prep args ctxt = - let val decls = maps (the_bundle ctxt o prep ctxt) args +fun gen_includes get args ctxt = + let val decls = maps (get ctxt) args in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end; -fun gen_context prep_bundle prep_decl raw_incls raw_elems gthy = +fun gen_context get prep_decl raw_incls raw_elems gthy = let val (after_close, lthy) = gthy |> Context.cases (pair Local_Theory.exit o Named_Target.theory_init) (pair I o Local_Theory.assert); val ((_, _, _, lthy'), _) = lthy - |> gen_includes prep_bundle raw_incls + |> gen_includes get raw_incls |> prep_decl ([], []) I raw_elems; in lthy' |> Local_Theory.open_target @@ -104,8 +103,8 @@ in -val includes = gen_includes (K I); -val includes_cmd = gen_includes check; +val includes = gen_includes get_bundle; +val includes_cmd = gen_includes get_bundle_cmd; fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts; fun include_cmd bs = @@ -114,8 +113,8 @@ fun including bs = Proof.assert_backward #> Proof.map_context (includes bs); fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs); -val context = gen_context (K I) Expression.cert_declaration; -val context_cmd = gen_context check Expression.read_declaration; +val context = gen_context get_bundle Expression.cert_declaration; +val context_cmd = gen_context get_bundle_cmd Expression.read_declaration; end; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/Isar/locale.ML Mon Mar 10 23:03:51 2014 +0100 @@ -160,19 +160,20 @@ val merge = Name_Space.join_tables (K merge_locale); ); -val intern = Name_Space.intern o #1 o Locales.get; +val locale_space = Name_Space.space_of_table o Locales.get; +val intern = Name_Space.intern o locale_space; fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy); -fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy)); +fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (locale_space thy); fun markup_extern ctxt = - Name_Space.markup_extern ctxt (#1 (Locales.get (Proof_Context.theory_of ctxt))); + Name_Space.markup_extern ctxt (locale_space (Proof_Context.theory_of ctxt)); fun markup_name ctxt name = markup_extern ctxt name |-> Markup.markup; fun pretty_name ctxt name = markup_extern ctxt name |> Pretty.mark_str; -val get_locale = Symtab.lookup o #2 o Locales.get; -val defined = Symtab.defined o #2 o Locales.get; +val get_locale = Option.map #2 oo (Name_Space.lookup_key o Locales.get); +val defined = is_some oo get_locale; fun the_locale thy name = (case get_locale thy name of @@ -189,7 +190,7 @@ (* FIXME Morphism.identity *) fun change_locale name = - Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd; + Locales.map o Name_Space.map_table_entry name o map_locale o apsnd; (** Primitive operations **) @@ -680,6 +681,7 @@ {name = name, parents = map (fst o fst) (dependencies_of thy name), body = pretty_locale thy false name}; - in map make_node (Symtab.keys (#2 (Locales.get thy))) end; + val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []); + in map make_node names end; end; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/Isar/method.ML Mon Mar 10 23:03:51 2014 +0100 @@ -67,7 +67,6 @@ val check_src: Proof.context -> src -> src val method: Proof.context -> src -> Proof.context -> method val method_cmd: Proof.context -> src -> Proof.context -> method - val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory type modifier = (Proof.context -> Proof.context) * attribute @@ -300,7 +299,7 @@ fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r); val succeed_text = Basic (K succeed); -val default_text = Source (Args.src (("default", []), Position.none)); +val default_text = Source (Args.src ("default", Position.none) []); val this_text = Basic (K this); val done_text = Basic (K (SIMPLE_METHOD all_tac)); fun sorry_text int = Basic (fn ctxt => cheating ctxt int); @@ -340,36 +339,23 @@ (* check *) fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt); - -fun check_src ctxt src = - let - val ((xname, toks), pos) = Args.dest_src src; - val name = check_name ctxt (xname, pos); - in Args.src ((name, toks), pos) end; +fun check_src ctxt src = #1 (Args.check_src ctxt (get_methods ctxt) src); (* get methods *) fun method ctxt = - let val (_, tab) = get_methods ctxt in - fn src => - let val ((name, _), pos) = Args.dest_src src in - (case Symtab.lookup tab name of - NONE => error ("Undefined method: " ^ quote name ^ Position.here pos) - | SOME (meth, _) => meth src) - end - end; + let val table = get_methods ctxt + in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end; fun method_cmd ctxt = method ctxt o check_src ctxt; (* method setup *) -fun syntax scan = Args.context_syntax "method" scan; - fun setup name scan = add_method name - (fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end); + (fn src => fn ctxt => let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end); fun method_setup name source cmt = Context.theory_map (ML_Context.expression (#pos source) @@ -457,9 +443,9 @@ local fun meth4 x = - (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) || + (Parse.position Parse.xname >> (fn name => Source (Args.src name [])) || Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok => - Source (Args.src (("cartouche", [tok]), Token.pos_of tok))) || + Source (Args.src ("cartouche", Token.pos_of tok) [tok])) || Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x and meth3 x = (meth4 -- Parse.position (Parse.$$$ "?") @@ -472,7 +458,7 @@ Select_Goals (combinator_info [pos1, pos2], n, m)) || meth4) x and meth2 x = - (Parse.position (Parse.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) || + (Parse.position Parse.xname -- Args.parse1 is_symid_meth >> (Source o uncurry Args.src) || meth3) x and meth1 x = (Parse.enum1_positions "," meth2 diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/Isar/parse_spec.ML --- a/src/Pure/Isar/parse_spec.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/Isar/parse_spec.ML Mon Mar 10 23:03:51 2014 +0100 @@ -37,7 +37,7 @@ (* theorem specifications *) -val attrib = Parse.position (Parse.liberal_name -- Parse.!!! Args.parse) >> Args.src; +val attrib = Parse.position Parse.liberal_name -- Parse.!!! Args.parse >> uncurry Args.src; val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]"; val opt_attribs = Scan.optional attribs []; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Mon Mar 10 23:03:51 2014 +0100 @@ -441,7 +441,7 @@ fun check_type_name {proper, strict} ctxt (c, pos) = if Lexicon.is_tid c then - if proper then error ("Not a type constructor: " ^ c ^ Position.here pos) + if proper then error ("Not a type constructor: " ^ quote c ^ Position.here pos) else let val reports = @@ -1152,16 +1152,14 @@ (** cases **) fun dest_cases ctxt = - Symtab.fold (fn (a, (c, i)) => cons (i, (a, c))) (#2 (cases_of ctxt)) [] + Name_Space.fold_table (fn (a, (c, i)) => cons (i, (a, c))) (cases_of ctxt) [] |> sort (int_ord o pairself #1) |> map #2; local fun update_case _ _ ("", _) res = res - | update_case _ _ (name, NONE) ((space, tab), index) = - let - val tab' = Symtab.delete_safe name tab; - in ((space, tab'), index) end + | update_case _ _ (name, NONE) (cases, index) = + (Name_Space.del_table name cases, index) | update_case context is_proper (name, SOME c) (cases, index) = let val (_, cases') = cases |> Name_Space.define context false @@ -1179,7 +1177,7 @@ let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming); val cases = cases_of ctxt; - val index = Symtab.fold (fn _ => Integer.add 1) (#2 cases) 0; + val index = Name_Space.fold_table (fn _ => Integer.add 1) cases 0; val (cases', _) = fold (update_case context is_proper) args (cases, index); in map_cases (K cases') ctxt end; @@ -1230,14 +1228,15 @@ fun pretty_abbrevs show_globals ctxt = let - val ((space, consts), (_, globals)) = + val space = const_space ctxt; + val (constants, globals) = pairself (#constants o Consts.dest) (#consts (rep_data ctxt)); fun add_abbr (_, (_, NONE)) = I | add_abbr (c, (T, SOME t)) = if not show_globals andalso Symtab.defined globals c then I else cons (c, Logic.mk_equals (Const (c, T), t)); val abbrevs = - Name_Space.extern_table ctxt (space, Symtab.make (Symtab.fold add_abbr consts [])); + Name_Space.extern_table' ctxt space (Symtab.make (Symtab.fold add_abbr constants [])); in if null abbrevs then [] else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)] @@ -1294,18 +1293,18 @@ else [Binding.pretty b, Pretty.str ":"]) @ map (Pretty.quote o prt_term) ts)); fun prt_sect _ _ _ [] = [] - | prt_sect s sep prt xs = - [Pretty.block (Pretty.breaks (Pretty.str s :: + | prt_sect head sep prt xs = + [Pretty.block (Pretty.breaks (head :: flat (separate sep (map (single o prt) xs))))]; in Pretty.block (Pretty.fbreaks (Pretty.str (name ^ ":") :: - prt_sect "fix" [] (Pretty.str o Binding.name_of o fst) fixes @ - prt_sect "let" [Pretty.str "and"] prt_let + prt_sect (Pretty.keyword1 "fix") [] (Pretty.str o Binding.name_of o fst) fixes @ + prt_sect (Pretty.keyword1 "let") [Pretty.keyword2 "and"] prt_let (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @ (if forall (null o #2) asms then [] - else prt_sect "assume" [Pretty.str "and"] prt_asm asms) @ - prt_sect "subcases:" [] (Pretty.str o fst) cs)) + else prt_sect (Pretty.keyword1 "assume") [Pretty.keyword2 "and"] prt_asm asms) @ + prt_sect (Pretty.str "subcases:") [] (Pretty.str o fst) cs)) end; in diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/Isar/specification.ML Mon Mar 10 23:03:51 2014 +0100 @@ -376,14 +376,14 @@ fun merge data : T = Library.merge (eq_snd op =) data; ); -fun gen_theorem schematic prep_bundle prep_att prep_stmt +fun gen_theorem schematic bundle_includes prep_att prep_stmt kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy = let val _ = Local_Theory.assert lthy; val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy)); val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy - |> Bundle.includes (map (prep_bundle lthy) raw_includes) + |> bundle_includes raw_includes |> prep_statement (prep_att lthy) prep_stmt elems raw_concl; val atts = more_atts @ map (prep_att lthy) raw_atts; @@ -419,13 +419,15 @@ in -val theorem = gen_theorem false (K I) (K I) Expression.cert_statement; +val theorem = + gen_theorem false Bundle.includes (K I) Expression.cert_statement; val theorem_cmd = - gen_theorem false Bundle.check Attrib.check_src Expression.read_statement; + gen_theorem false Bundle.includes_cmd Attrib.check_src Expression.read_statement; -val schematic_theorem = gen_theorem true (K I) (K I) Expression.cert_statement; +val schematic_theorem = + gen_theorem true Bundle.includes (K I) Expression.cert_statement; val schematic_theorem_cmd = - gen_theorem true Bundle.check Attrib.check_src Expression.read_statement; + gen_theorem true Bundle.includes_cmd Attrib.check_src Expression.read_statement; fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ())); diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/ML/ml_context.ML Mon Mar 10 23:03:51 2014 +0100 @@ -115,10 +115,8 @@ fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt); fun antiquotation src ctxt = - let - val ((xname, _), pos) = Args.dest_src src; - val (_, scan) = Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt) (xname, pos); - in Args.context_syntax Markup.ML_antiquotationN scan src ctxt end; + let val (src', scan) = Args.check_src ctxt (get_antiqs ctxt) src + in Args.syntax scan src' ctxt end; (* parsing and evaluation *) @@ -127,7 +125,7 @@ val antiq = Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof) - >> (fn ((x, pos), y) => Args.src ((x, y), pos)); + >> uncurry Args.src; val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n"; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/PIDE/command.ML Mon Mar 10 23:03:51 2014 +0100 @@ -91,6 +91,7 @@ fun read_file master_dir pos src_path = let + val _ = Position.report pos Markup.language_path; 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; @@ -117,7 +118,7 @@ fun make_file src_path (Exn.Res (_, NONE)) = Exn.interruptible_capture (fn () => read_file master_dir pos src_path) () | make_file src_path (Exn.Res (file, SOME (digest, lines))) = - (Position.report pos (Markup.path file); + (Position.reports [(pos, Markup.language_path), (pos, Markup.path file)]; Exn.Res (blob_file src_path lines digest file)) | make_file _ (Exn.Exn e) = Exn.Exn e; val src_paths = Keyword.command_files cmd path; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/PIDE/markup.ML Mon Mar 10 23:03:51 2014 +0100 @@ -27,6 +27,7 @@ val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T val language_method: T + val language_attribute: T val language_sort: bool -> T val language_type: bool -> T val language_term: bool -> T @@ -36,6 +37,7 @@ val language_antiquotation: T val language_text: bool -> T val language_rail: T + val language_path: T val bindingN: string val binding: T val entityN: string val entity: string -> string -> T val get_entity_kind: T -> string option @@ -277,6 +279,8 @@ val language_method = language {name = "method", symbols = true, antiquotes = false, delimited = false}; +val language_attribute = + language {name = "attribute", symbols = true, antiquotes = false, delimited = false}; val language_sort = language' {name = "sort", symbols = true, antiquotes = false}; val language_type = language' {name = "type", symbols = true, antiquotes = false}; val language_term = language' {name = "term", symbols = true, antiquotes = false}; @@ -287,6 +291,7 @@ language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true}; val language_text = language' {name = "text", symbols = true, antiquotes = false}; val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true}; +val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true}; (* formal entities *) diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/Thy/term_style.ML --- a/src/Pure/Thy/term_style.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/Thy/term_style.ML Mon Mar 10 23:03:51 2014 +0100 @@ -6,46 +6,38 @@ signature TERM_STYLE = sig - val setup: string -> (Proof.context -> term -> term) parser -> theory -> theory + val setup: binding -> (Proof.context -> term -> term) parser -> theory -> theory val parse: (term -> term) context_parser end; structure Term_Style: TERM_STYLE = struct -(* style data *) - -fun err_dup_style name = - error ("Duplicate declaration of antiquote style: " ^ quote name); +(* theory data *) -structure Styles = Theory_Data +structure Data = Theory_Data ( - type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table; - val empty = Symtab.empty; + type T = (Proof.context -> term -> term) parser Name_Space.table; + val empty : T = Name_Space.empty_table "antiquotation_style"; val extend = I; - fun merge data : T = Symtab.merge (eq_snd (op =)) data - handle Symtab.DUP dup => err_dup_style dup; + fun merge data : T = Name_Space.merge_tables data; ); - -(* accessors *) +val get_data = Data.get o Proof_Context.theory_of; +val get_style = Name_Space.get o get_data; -fun the_style thy name = - (case Symtab.lookup (Styles.get thy) name of - NONE => error ("Unknown antiquote style: " ^ quote name) - | SOME (style, _) => style); - -fun setup name style thy = - Styles.map (Symtab.update_new (name, (style, stamp ()))) thy - handle Symtab.DUP _ => err_dup_style name; +fun setup binding style thy = + Data.map (#2 o Name_Space.define (Context.Theory thy) true (binding, style)) thy; (* style parsing *) -fun parse_single ctxt = Parse.position (Parse.xname -- Args.parse) - >> (fn x as ((name, _), _) => fst (Args.context_syntax "style" - (Scan.lift (the_style (Proof_Context.theory_of ctxt) name)) - (Args.src x) ctxt |>> (fn f => f ctxt))); +fun parse_single ctxt = + Parse.position Parse.xname -- Args.parse >> (fn (name, args) => + let + val (src, parse) = Args.check_src ctxt (get_data ctxt) (Args.src name args); + val (f, _) = Args.syntax (Scan.lift parse) src ctxt; + in f ctxt end); val parse = Args.context :|-- (fn ctxt => Scan.lift (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt)) @@ -61,7 +53,7 @@ Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t) in (case concl of - (_ $ l $ r) => proj (l, r) + _ $ l $ r => proj (l, r) | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)) end); @@ -92,10 +84,10 @@ | sub_term t = t; val _ = Theory.setup - (setup "lhs" (style_lhs_rhs fst) #> - setup "rhs" (style_lhs_rhs snd) #> - setup "prem" style_prem #> - setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #> - setup "sub" (Scan.succeed (K sub_term))); + (setup (Binding.name "lhs") (style_lhs_rhs fst) #> + setup (Binding.name "rhs") (style_lhs_rhs snd) #> + setup (Binding.name "prem") style_prem #> + setup (Binding.name "concl") (Scan.succeed (K Logic.strip_imp_concl)) #> + setup (Binding.name "sub") (Scan.succeed (K sub_term))); end; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/Thy/thy_load.ML Mon Mar 10 23:03:51 2014 +0100 @@ -194,6 +194,8 @@ fun file_antiq strict ctxt (name, pos) = let + val _ = Context_Position.report ctxt pos Markup.language_path; + val dir = master_directory (Proof_Context.theory_of ctxt); val path = Path.append dir (Path.explode name) handle ERROR msg => error (msg ^ Position.here pos); diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/Thy/thy_output.ML Mon Mar 10 23:03:51 2014 +0100 @@ -92,11 +92,8 @@ fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)); fun command src state ctxt = - let - val ((xname, _), pos) = Args.dest_src src; - val (name, f) = - Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) (xname, pos); - in f src state ctxt end; + let val (src', f) = Args.check_src ctxt (#1 (get_antiquotations ctxt)) src + in f src' state ctxt end; fun option ((xname, pos), s) ctxt = let @@ -118,7 +115,7 @@ fun antiquotation name scan out = add_command name (fn src => fn state => fn ctxt => - let val (x, ctxt') = Args.context_syntax "document antiquotation" scan src ctxt + let val (x, ctxt') = Args.syntax scan src ctxt in out {source = src, state = state, context = ctxt'} x end); @@ -155,7 +152,7 @@ val antiq = Parse.!!! (Parse.position Parse.liberal_name -- properties -- Args.parse --| Scan.ahead Parse.eof) - >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos))); + >> (fn ((name, props), args) => (props, Args.src name args)); end; @@ -529,7 +526,7 @@ (* default output *) -val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src; +val str_of_source = space_implode " " o Args.unparse_src; fun maybe_pretty_source pretty ctxt src xs = map (pretty ctxt) xs (*always pretty in order to exhibit errors!*) @@ -615,12 +612,11 @@ val _ = Theory.setup (antiquotation (Binding.name "lemma") - (Args.prop -- + (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop -- Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse)) - (fn {source, context = ctxt, ...} => fn (prop, (((_, by_pos), m1), m2)) => + (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) => let - val prop_src = - (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos)); + val prop_src = Args.src (Args.name_of_src source) [prop_token]; val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2); val _ = Context_Position.reports ctxt reports; @@ -679,6 +675,7 @@ val _ = Theory.setup (antiquotation (Binding.name "url") (Scan.lift (Parse.position Parse.name)) (fn {context = ctxt, ...} => fn (name, pos) => - (Context_Position.report ctxt pos (Markup.url name); enclose "\\url{" "}" name))); + (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)]; + enclose "\\url{" "}" name))); end; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/Tools/find_consts.ML Mon Mar 10 23:03:51 2014 +0100 @@ -58,8 +58,8 @@ fun pretty_const ctxt (c, ty) = let val ty' = Logic.unvarifyT_global ty; - val consts_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt)); - val markup = Name_Space.markup consts_space c; + val const_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt)); + val markup = Name_Space.markup const_space c; in Pretty.block [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1, @@ -103,13 +103,13 @@ val criteria = map make_criterion raw_criteria; val consts = Sign.consts_of thy; - val (_, consts_tab) = #constants (Consts.dest consts); + val {constants, ...} = Consts.dest consts; fun eval_entry c = fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking); val matches = Symtab.fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) - consts_tab [] + constants [] |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst)) |> map (apsnd fst o snd); in diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/Tools/find_theorems.ML Mon Mar 10 23:03:51 2014 +0100 @@ -330,7 +330,7 @@ val index_ord = option_ord (K EQUAL); val hidden_ord = bool_ord o pairself Long_Name.is_hidden; -val qual_ord = int_ord o pairself (length o Long_Name.explode); +val qual_ord = int_ord o pairself Long_Name.qualification; val txt_ord = int_ord o pairself size; fun nicer_name (x, i) (y, j) = diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/consts.ML --- a/src/Pure/consts.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/consts.ML Mon Mar 10 23:03:51 2014 +0100 @@ -11,8 +11,9 @@ val eq_consts: T * T -> bool val retrieve_abbrevs: T -> string list -> term -> (term * term) list val dest: T -> - {constants: (typ * term option) Name_Space.table, - constraints: typ Name_Space.table} + {const_space: Name_Space.T, + constants: (typ * term option) Symtab.table, + constraints: typ Symtab.table} val the_const: T -> string -> string * typ (*exception TYPE*) val the_abbreviation: T -> string -> typ * term (*exception TYPE*) val type_scheme: T -> string -> typ (*exception TYPE*) @@ -80,17 +81,18 @@ (* dest consts *) -fun dest (Consts {decls = (space, decls), constraints, ...}) = - {constants = (space, - Symtab.fold (fn (c, ({T, ...}, abbr)) => - Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty), - constraints = (space, constraints)}; +fun dest (Consts {decls, constraints, ...}) = + {const_space = Name_Space.space_of_table decls, + constants = + Name_Space.fold_table (fn (c, ({T, ...}, abbr)) => + Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty, + constraints = constraints}; (* lookup consts *) -fun the_entry (Consts {decls = (_, tab), ...}) c = - (case Symtab.lookup_key tab c of +fun the_entry (Consts {decls, ...}) c = + (case Name_Space.lookup_key decls c of SOME entry => entry | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], [])); @@ -118,10 +120,10 @@ (* name space and syntax *) -fun space_of (Consts {decls = (space, _), ...}) = space; +fun space_of (Consts {decls, ...}) = Name_Space.space_of_table decls; -fun alias naming binding name = map_consts (fn ((space, decls), constraints, rev_abbrevs) => - ((Name_Space.alias naming binding name space, decls), constraints, rev_abbrevs)); +fun alias naming binding name = map_consts (fn (decls, constraints, rev_abbrevs) => + ((Name_Space.alias_table naming binding name decls), constraints, rev_abbrevs)); val is_concealed = Name_Space.is_concealed o space_of; @@ -219,7 +221,7 @@ (* name space *) fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs) => - (apfst (Name_Space.hide fully c) decls, constraints, rev_abbrevs)); + (Name_Space.hide_table fully c decls, constraints, rev_abbrevs)); (* declarations *) diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/display.ML --- a/src/Pure/display.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/display.ML Mon Mar 10 23:03:51 2014 +0100 @@ -145,33 +145,34 @@ fun pretty_restrict (const, name) = Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); - val axioms = (Theory.axiom_space thy, Theory.axiom_table thy); val defs = Theory.defs_of thy; val {restricts, reducts} = Defs.dest defs; val tsig = Sign.tsig_of thy; val consts = Sign.consts_of thy; - val {constants, constraints} = Consts.dest consts; - val extern_const = Name_Space.extern ctxt (#1 constants); + val {const_space, constants, constraints} = Consts.dest consts; + val extern_const = Name_Space.extern ctxt const_space; val {classes, default, types, ...} = Type.rep_tsig tsig; val (class_space, class_algebra) = classes; val classes = Sorts.classes_of class_algebra; val arities = Sorts.arities_of class_algebra; val clsses = - Name_Space.dest_table ctxt (class_space, - Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))); - val tdecls = Name_Space.dest_table ctxt types; - val arties = Name_Space.dest_table ctxt (Type.type_space tsig, arities); + Name_Space.dest_table' ctxt class_space + (Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))) + |> map (apfst #1); + val tdecls = Name_Space.dest_table ctxt types |> map (apfst #1); + val arties = Name_Space.dest_table' ctxt (Type.type_space tsig) arities |> map (apfst #1); fun prune_const c = not verbose andalso Consts.is_concealed consts c; - val cnsts = Name_Space.extern_table ctxt (#1 constants, - Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants)))); + val cnsts = + Name_Space.extern_table' ctxt const_space + (Symtab.make (filter_out (prune_const o fst) (Symtab.dest constants))); val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; - val cnstrs = Name_Space.extern_table ctxt constraints; + val cnstrs = Name_Space.extern_table' ctxt const_space constraints; - val axms = Name_Space.extern_table ctxt axioms; + val axms = Name_Space.extern_table ctxt (Theory.axiom_table thy); val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts |> map (fn (lhs, rhs) => diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/facts.ML --- a/src/Pure/facts.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/facts.ML Mon Mar 10 23:03:51 2014 +0100 @@ -140,8 +140,7 @@ fun facts_of (Facts {facts, ...}) = facts; -val space_of = #1 o facts_of; -val table_of = #2 o facts_of; +val space_of = Name_Space.space_of_table o facts_of; val is_concealed = Name_Space.is_concealed o space_of; @@ -157,16 +156,16 @@ val intern = Name_Space.intern o space_of; fun extern ctxt = Name_Space.extern ctxt o space_of; -val defined = Symtab.defined o table_of; +val defined = is_some oo (Name_Space.lookup_key o facts_of); fun lookup context facts name = - (case Symtab.lookup (table_of facts) name of + (case Name_Space.lookup_key (facts_of facts) name of NONE => NONE - | SOME (Static ths) => SOME (true, ths) - | SOME (Dynamic f) => SOME (false, f context)); + | SOME (_, Static ths) => SOME (true, ths) + | SOME (_, Dynamic f) => SOME (false, f context)); fun fold_static f = - Symtab.fold (fn (name, Static ths) => f (name, ths) | _ => I) o table_of; + Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of; (* content difference *) @@ -221,13 +220,10 @@ (* remove entries *) -fun del name (Facts {facts = (space, tab), props}) = - let - val space' = Name_Space.hide true name space handle ERROR _ => space; - val tab' = Symtab.delete_safe name tab; - in make_facts (space', tab') props end; +fun del name (Facts {facts, props}) = + make_facts (Name_Space.del_table name facts) props; -fun hide fully name (Facts {facts = (space, tab), props}) = - make_facts (Name_Space.hide fully name space, tab) props; +fun hide fully name (Facts {facts, props}) = + make_facts (Name_Space.hide_table fully name facts) props; end; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/library.ML --- a/src/Pure/library.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/library.ML Mon Mar 10 23:03:51 2014 +0100 @@ -146,6 +146,7 @@ val cat_lines: string list -> string val space_explode: string -> string -> string list val split_lines: string -> string list + val plain_words: string -> string val prefix_lines: string -> string -> string val prefix: string -> string -> string val suffix: string -> string -> string @@ -745,6 +746,8 @@ val split_lines = space_explode "\n"; +fun plain_words s = space_explode "_" s |> space_implode " "; + fun prefix_lines "" txt = txt | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/sign.ML --- a/src/Pure/sign.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/sign.ML Mon Mar 10 23:03:51 2014 +0100 @@ -192,7 +192,7 @@ fun mk_const thy (c, Ts) = Const (c, const_instance thy (c, Ts)); -val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of; +fun declared_tyname ctxt c = can (Type.the_decl (tsig_of ctxt)) (c, Position.none); val declared_const = can o the_const_constraint; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/term_sharing.ML --- a/src/Pure/term_sharing.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/term_sharing.ML Mon Mar 10 23:03:51 2014 +0100 @@ -19,10 +19,10 @@ fun init thy = let - val {classes = (_, algebra), types = (_, types), ...} = Type.rep_tsig (Sign.tsig_of thy); + val {classes = (_, algebra), types, ...} = Type.rep_tsig (Sign.tsig_of thy); val class = perhaps (try (#1 o Graph.get_entry (Sorts.classes_of algebra))); - val tycon = perhaps (Option.map #1 o Symtab.lookup_key types); + val tycon = perhaps (Option.map #1 o Name_Space.lookup_key types); val const = perhaps (try (#1 o Consts.the_const (Sign.consts_of thy))); val typs = Unsynchronized.ref (Typtab.empty: unit Typtab.table); diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/theory.ML --- a/src/Pure/theory.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/theory.ML Mon Mar 10 23:03:51 2014 +0100 @@ -17,8 +17,8 @@ val requires: theory -> string -> string -> unit val setup: (theory -> theory) -> unit val get_markup: theory -> Markup.T + val axiom_table: theory -> term Name_Space.table val axiom_space: theory -> Name_Space.T - val axiom_table: theory -> term Symtab.table val axioms_of: theory -> (string * term) list val all_axioms_of: theory -> (string * term) list val defs_of: theory -> Defs.T @@ -139,10 +139,10 @@ (* basic operations *) -val axiom_space = #1 o #axioms o rep_theory; -val axiom_table = #2 o #axioms o rep_theory; +val axiom_table = #axioms o rep_theory; +val axiom_space = Name_Space.space_of_table o axiom_table; -val axioms_of = Symtab.dest o #2 o #axioms o rep_theory; +fun axioms_of thy = rev (Name_Space.fold_table cons (axiom_table thy) []); fun all_axioms_of thy = maps axioms_of (nodes_of thy); val defs_of = #defs o rep_theory; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/thm.ML --- a/src/Pure/thm.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/thm.ML Mon Mar 10 23:03:51 2014 +0100 @@ -584,8 +584,8 @@ fun axiom theory name = let fun get_ax thy = - Symtab.lookup (Theory.axiom_table thy) name - |> Option.map (fn prop => + Name_Space.lookup_key (Theory.axiom_table thy) name + |> Option.map (fn (_, prop) => let val der = deriv_rule0 (Proofterm.axm_proof name prop); val maxidx = maxidx_of_term prop; @@ -602,7 +602,7 @@ (*return additional axioms of this theory node*) fun axioms_of thy = - map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy)); + map (fn (name, _) => (name, axiom thy name)) (Theory.axioms_of thy); (* tags *) diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/type.ML --- a/src/Pure/type.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/type.ML Mon Mar 10 23:03:51 2014 +0100 @@ -177,7 +177,7 @@ fun build_tsig (classes, default, types) = let val log_types = - Symtab.fold (fn (c, LogicalType n) => cons (c, n) | _ => I) (snd types) [] + Name_Space.fold_table (fn (c, LogicalType n) => cons (c, n) | _ => I) types [] |> Library.sort (int_ord o pairself snd) |> map fst; in make_tsig (classes, default, types, log_types) end; @@ -237,17 +237,17 @@ (* types *) -val type_space = #1 o #types o rep_tsig; +val type_space = Name_Space.space_of_table o #types o rep_tsig; -fun type_alias naming binding name = map_tsig (fn (classes, default, (space, types)) => - (classes, default, (Name_Space.alias naming binding name space, types))); +fun type_alias naming binding name = map_tsig (fn (classes, default, types) => + (classes, default, (Name_Space.alias_table naming binding name types))); val is_logtype = member (op =) o logical_types; fun undecl_type c = "Undeclared type constructor: " ^ quote c; -fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types; +fun lookup_type (TSig {types, ...}) = Option.map #2 o Name_Space.lookup_key types; fun check_decl context (TSig {types, ...}) (c, pos) = Name_Space.check_reports context types (c, [pos]); @@ -639,14 +639,15 @@ fun map_types f = map_tsig (fn (classes, default, types) => let - val (space', tab') = f types; - val _ = Name_Space.intern space' "dummy" = "dummy" orelse - error "Illegal declaration of dummy type"; - in (classes, default, (space', tab')) end); + val types' = f types; + val _ = + Name_Space.intern (Name_Space.space_of_table types') "dummy" = "dummy" orelse + error "Illegal declaration of dummy type"; + in (classes, default, types') end); -fun syntactic types (Type (c, Ts)) = - (case Symtab.lookup types c of SOME Nonterminal => true | _ => false) - orelse exists (syntactic types) Ts +fun syntactic tsig (Type (c, Ts)) = + (case lookup_type tsig c of SOME Nonterminal => true | _ => false) + orelse exists (syntactic tsig) Ts | syntactic _ _ = false; in @@ -669,14 +670,14 @@ (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of [] => [] | extras => err ("Extra variables on rhs: " ^ commas_quote extras)); - in types |> new_decl context (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end); + in types |> new_decl context (a, Abbreviation (vs, rhs', syntactic tsig rhs')) end); fun add_nonterminal context = map_types o new_decl context o rpair Nonterminal; end; -fun hide_type fully c = map_tsig (fn (classes, default, (space, types)) => - (classes, default, (Name_Space.hide fully c space, types))); +fun hide_type fully c = map_tsig (fn (classes, default, types) => + (classes, default, Name_Space.hide_table fully c types)); (* merge type signatures *) diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Pure/variable.ML --- a/src/Pure/variable.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Pure/variable.ML Mon Mar 10 23:03:51 2014 +0100 @@ -175,7 +175,7 @@ val names_of = #names o rep_data; val fixes_of = #fixes o rep_data; -val fixes_space = #1 o fixes_of; +val fixes_space = Name_Space.space_of_table o fixes_of; val binds_of = #binds o rep_data; val type_occs_of = #type_occs o rep_data; val maxidx_of = #maxidx o rep_data; @@ -342,8 +342,8 @@ in if is_fixed ctxt x' then SOME x' else NONE end; fun revert_fixed ctxt x = - (case Symtab.lookup (#2 (fixes_of ctxt)) x of - SOME x' => if intern_fixed ctxt x' = x then x' else x + (case Name_Space.lookup_key (fixes_of ctxt) x of + SOME (_, x') => if intern_fixed ctxt x' = x then x' else x | NONE => x); fun markup_fixed ctxt x = @@ -351,8 +351,8 @@ |> Markup.name (revert_fixed ctxt x); fun dest_fixes ctxt = - let val (space, tab) = fixes_of ctxt - in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end; + Name_Space.fold_table (fn (x, y) => cons (y, x)) (fixes_of ctxt) [] + |> sort (Name_Space.entry_ord (fixes_space ctxt) o pairself #2); (* collect variables *) @@ -383,8 +383,8 @@ let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming) in ctxt |> map_fixes - (Name_Space.define context true (Binding.make (x', pos), x) #> snd #>> - Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x') + (Name_Space.define context true (Binding.make (x', pos), x) #> snd #> + Name_Space.alias_table Name_Space.default_naming (Binding.make (x, pos)) x') |> declare_fixed x |> declare_constraints (Syntax.free x') end; @@ -450,8 +450,8 @@ val still_fixed = not o newly_fixed inner outer; val gen_fixes = - Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y) - (#2 (fixes_of inner)) []; + Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? cons y) + (fixes_of inner) []; val type_occs_inner = type_occs_of inner; fun gen_fixesT ts = diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/Tools/Code/code_thingol.ML Mon Mar 10 23:03:51 2014 +0100 @@ -877,7 +877,7 @@ let val thy = Proof_Context.theory_of ctxt; fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I) - ((snd o #constants o Consts.dest o Sign.consts_of) thy') []; + (#constants (Consts.dest (Sign.consts_of thy'))) []; fun belongs_here thy' c = forall (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy'); fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy'); diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/ZF/Tools/ind_cases.ML --- a/src/ZF/Tools/ind_cases.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/ZF/Tools/ind_cases.ML Mon Mar 10 23:03:51 2014 +0100 @@ -48,7 +48,7 @@ let val ctxt = Proof_Context.init_global thy; val facts = args |> map (fn ((name, srcs), props) => - ((name, map (Attrib.attribute_cmd_global thy) srcs), + ((name, map (Attrib.attribute_cmd ctxt) srcs), map (Thm.no_attributes o single o smart_cases ctxt) props)); in thy |> Global_Theory.note_thmss "" facts |> snd end; diff -r e0c9d76c2a6d -r f78b4c3e8e84 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Mon Mar 10 20:16:13 2014 +0100 +++ b/src/ZF/Tools/inductive_package.ML Mon Mar 10 23:03:51 2014 +0100 @@ -560,7 +560,7 @@ val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT) #> Syntax.check_terms ctxt; - val intr_atts = map (map (Attrib.attribute_cmd_global thy) o snd) intr_srcs; + val intr_atts = map (map (Attrib.attribute_cmd ctxt) o snd) intr_srcs; val sintrs = map fst intr_srcs ~~ intr_atts; val rec_tms = read_terms srec_tms; val dom_sum = singleton read_terms sdom_sum;