--- 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.")
--- 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 \<equiv> C (0\<^sub>N)"
@@ -142,7 +142,7 @@
fun polymul :: "poly \<Rightarrow> poly \<Rightarrow> 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 \<or> ?cnp' = 0\<^sub>p then 0 else ?d1 + ?d2)"
- have "n'<n \<or> n < n' \<or> n' = n" by auto
+ have "n' < n \<or> n < n' \<or> n' = n" by auto
moreover
{
assume "n' < n \<or> 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' \<noteq> 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 \<longleftrightarrow> c' = 0\<^sub>p"
+ "?cnp *\<^sub>p p' \<noteq> 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 \<le> min n0 n1" by simp_all
+ and m: "m \<le> min n0 n1"
+ by simp_all
then have mn: "m \<le> n" by simp
let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
{
@@ -700,10 +707,17 @@
assume pz: "p \<noteq> 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) \<longrightarrow> \<lparr>p\<rparr>\<^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) \<longrightarrow> \<lparr>p\<rparr>\<^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) \<or> even (Suc n)" by simp
+ have "odd (Suc n) \<or> 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 "\<dots> = (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 "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2) * (Ipoly bs p)^(Suc n div 2)"
using "2.hyps" by simp
also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"
by (simp only: power_add power_one_right) simp
also have "\<dots> = (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 "\<dots> = (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 \<Longrightarrow> 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 \<noteq> 0\<^sub>p"
by (simp add: shift1_def)
-lemma funpow_shift1_isnpoly:
- "\<lbrakk> isnpoly p ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> isnpoly (funpow n shift1 p)"
+
+lemma funpow_shift1_isnpoly: "isnpoly p \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> isnpoly (funpow n shift1 p)"
by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
lemma funpow_isnpolyh:
- assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n"
+ assumes f: "\<And>p. isnpolyh p n \<Longrightarrow> 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 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
+lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> 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 \<Longrightarrow> polybound0 p \<Longrightarrow> 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 \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0)
-primrec maxindex :: "poly \<Rightarrow> nat" where
+primrec maxindex :: "poly \<Rightarrow> 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 \<Rightarrow> poly \<Rightarrow> bool"
where "wf_bs bs p \<longleftrightarrow> length bs \<ge> maxindex p"
-lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall> c \<in> set (coefficients p). wf_bs bs c"
+lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall>c \<in> 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: "\<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p"
+lemma maxindex_coefficients: "\<forall>c \<in> set (coefficients p). maxindex c \<le> maxindex p"
by (induct p rule: coefficients.induct) auto
lemma wf_bs_I: "wf_bs bs p \<Longrightarrow> 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': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x#bs) p"
by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def)
+
lemma coefficients_Nil[simp]: "coefficients p \<noteq> []"
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) \<Longrightarrow> wf_bs (x#bs) p"
unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto
-lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists> ys. length (xs @ ys) = n"
+lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists>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) \<Longrightarrow> isconstant p"
+lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \<Longrightarrow> 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 \<Longrightarrow> wf_bs bs q \<Longrightarrow> 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 \<circ> decrpoly) (coefficients p)"
+definition "poly_nate bs p = map (Ipoly bs \<circ> decrpoly) (coefficients (polynate p))"
-lemma coefficients_normh: "isnpolyh p n0 \<Longrightarrow> \<forall> q \<in> set (coefficients p). isnpolyh q n0"
+lemma coefficients_normh: "isnpolyh p n0 \<Longrightarrow> \<forall>q \<in> 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 \<Longrightarrow> \<forall>q\<in>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 \<Longrightarrow> \<forall>q \<in> 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: "\<forall> q\<in> ?cf. isnpolyh q n0" .
- {fix q assume q: "q \<in> ?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 \<in> ?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 "\<forall>q \<in> ?cf. polybound0 q" ..
- then have "\<forall>q \<in> ?cf. Ipoly (x#bs) q = Ipoly bs (decrpoly q)"
+ then have "\<forall>q \<in> ?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 "\<lparr>p\<rparr>\<^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 \<Longrightarrow> isnpolyh (head p) n0"
by (induct p rule: head.induct) auto
-lemma headn_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (headn p m = 0\<^sub>p) = (p = 0\<^sub>p)"
+lemma headn_nz[simp]: "isnpolyh p n0 \<Longrightarrow> headn p m = 0\<^sub>p \<longleftrightarrow> 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 \<Longrightarrow> (head p = 0\<^sub>p) = (p = 0\<^sub>p)"
+lemma head_nz[simp]: "isnpolyh p n0 \<Longrightarrow> head p = 0\<^sub>p \<longleftrightarrow> 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) \<le> 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) \<le> 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 \<or> (p -\<^sub>p q = 0\<^sub>p)"
unfolding polysub_def split_def fst_conv snd_conv
--- 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;
--- 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
--- 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;
--- 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
--- 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 =
{
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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
--- 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 [];
--- 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
--- 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 ()));
--- 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";
--- 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;
--- 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 *)
--- 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;
--- 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);
--- 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;
--- 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
--- 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) =
--- 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 *)
--- 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) =>
--- 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;
--- 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;
--- 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;
--- 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);
--- 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;
--- 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 *)
--- 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 *)
--- 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 =
--- 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');
--- 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;
--- 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;