--- a/NEWS Thu Aug 26 01:03:08 2010 +0200
+++ b/NEWS Thu Aug 26 09:03:18 2010 +0200
@@ -32,6 +32,11 @@
* Diagnostic command 'print_interps' prints interpretations in proofs
in addition to interpretations in theories.
+* Discontinued obsolete 'global' and 'local' commands to manipulate
+the theory name space. Rare INCOMPATIBILITY. The ML functions
+Sign.root_path and Sign.local_path may be applied directly where this
+feature is still required for historical reasons.
+
*** HOL ***
--- a/doc-src/IsarRef/Thy/Spec.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Thu Aug 26 09:03:18 2010 +0200
@@ -1220,8 +1220,6 @@
text {*
\begin{matharray}{rcl}
- @{command_def "global"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "local"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "hide_class"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "hide_type"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "hide_const"} & : & @{text "theory \<rightarrow> theory"} \\
@@ -1241,16 +1239,6 @@
\begin{description}
- \item @{command "global"} and @{command "local"} change the current
- name declaration mode. Initially, theories start in @{command
- "local"} mode, causing all names to be automatically qualified by
- the theory name. Changing this to @{command "global"} causes all
- names to be declared without the theory prefix, until @{command
- "local"} is declared again.
-
- Note that global names are prone to get hidden accidently later,
- when qualified names of the same base name are introduced.
-
\item @{command "hide_class"}~@{text names} fully removes class
declarations from a given name space; with the @{text "(open)"}
option, only the base name is hidden. Global (unqualified) names
--- a/doc-src/IsarRef/Thy/document/Spec.tex Thu Aug 26 01:03:08 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Thu Aug 26 09:03:18 2010 +0200
@@ -1262,8 +1262,6 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\indexdef{}{command}{hide\_class}\hypertarget{command.hide-class}{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\indexdef{}{command}{hide\_type}\hypertarget{command.hide-type}{\hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\indexdef{}{command}{hide\_const}\hypertarget{command.hide-const}{\hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
@@ -1283,14 +1281,6 @@
\begin{description}
- \item \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} change the current
- name declaration mode. Initially, theories start in \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically qualified by
- the theory name. Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} causes all
- names to be declared without the theory prefix, until \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again.
-
- Note that global names are prone to get hidden accidently later,
- when qualified names of the same base name are introduced.
-
\item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class
declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}
option, only the base name is hidden. Global (unqualified) names
--- a/etc/isar-keywords-ZF.el Thu Aug 26 01:03:08 2010 +0200
+++ b/etc/isar-keywords-ZF.el Thu Aug 26 09:03:18 2010 +0200
@@ -73,7 +73,6 @@
"fix"
"from"
"full_prf"
- "global"
"guess"
"have"
"header"
@@ -97,7 +96,6 @@
"lemmas"
"let"
"linear_undo"
- "local"
"local_setup"
"locale"
"method_setup"
@@ -369,7 +367,6 @@
"extract"
"extract_type"
"finalconsts"
- "global"
"hide_class"
"hide_const"
"hide_fact"
@@ -378,7 +375,6 @@
"instantiation"
"judgment"
"lemmas"
- "local"
"local_setup"
"locale"
"method_setup"
--- a/etc/isar-keywords.el Thu Aug 26 01:03:08 2010 +0200
+++ b/etc/isar-keywords.el Thu Aug 26 09:03:18 2010 +0200
@@ -102,7 +102,6 @@
"full_prf"
"fun"
"function"
- "global"
"guess"
"have"
"header"
@@ -128,7 +127,6 @@
"lemmas"
"let"
"linear_undo"
- "local"
"local_setup"
"locale"
"method_setup"
@@ -469,7 +467,6 @@
"fixpat"
"fixrec"
"fun"
- "global"
"hide_class"
"hide_const"
"hide_fact"
@@ -479,7 +476,6 @@
"instantiation"
"judgment"
"lemmas"
- "local"
"local_setup"
"locale"
"method_setup"
--- a/src/FOL/simpdata.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/FOL/simpdata.ML Thu Aug 26 09:03:18 2010 +0200
@@ -81,11 +81,11 @@
end);
val defEX_regroup =
- Simplifier.simproc @{theory}
+ Simplifier.simproc_global @{theory}
"defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
val defALL_regroup =
- Simplifier.simproc @{theory}
+ Simplifier.simproc_global @{theory}
"defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
--- a/src/HOL/Algebra/abstract/Ring2.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Thu Aug 26 09:03:18 2010 +0200
@@ -285,7 +285,7 @@
else SOME rew
end;
in
- val ring_simproc = Simplifier.simproc @{theory} "ring" lhss (K proc);
+ val ring_simproc = Simplifier.simproc_global @{theory} "ring" lhss (K proc);
end;
*}
--- a/src/HOL/Complete_Lattice.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Complete_Lattice.thy Thu Aug 26 09:03:18 2010 +0200
@@ -88,6 +88,26 @@
lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
by (auto intro: Inf_greatest dest: Inf_lower)
+lemma Sup_mono:
+ assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
+ shows "Sup A \<le> Sup B"
+proof (rule Sup_least)
+ fix a assume "a \<in> A"
+ with assms obtain b where "b \<in> B" and "a \<le> b" by blast
+ from `b \<in> B` have "b \<le> Sup B" by (rule Sup_upper)
+ with `a \<le> b` show "a \<le> Sup B" by auto
+qed
+
+lemma Inf_mono:
+ assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
+ shows "Inf A \<le> Inf B"
+proof (rule Inf_greatest)
+ fix b assume "b \<in> B"
+ with assms obtain a where "a \<in> A" and "a \<le> b" by blast
+ from `a \<in> A` have "Inf A \<le> a" by (rule Inf_lower)
+ with `a \<le> b` show "Inf A \<le> b" by auto
+qed
+
definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
"SUPR A f = \<Squnion> (f ` A)"
@@ -144,8 +164,25 @@
lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
by (auto intro: antisym INF_leI le_INFI)
+lemma SUP_mono:
+ "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)"
+ by (force intro!: Sup_mono simp: SUPR_def)
+
+lemma INF_mono:
+ "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n:A. f n) \<le> (INF n:B. g n)"
+ by (force intro!: Inf_mono simp: INFI_def)
+
end
+lemma less_Sup_iff:
+ fixes a :: "'a\<Colon>{complete_lattice,linorder}"
+ shows "a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
+ unfolding not_le[symmetric] Sup_le_iff by auto
+
+lemma Inf_less_iff:
+ fixes a :: "'a\<Colon>{complete_lattice,linorder}"
+ shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
+ unfolding not_le[symmetric] le_Inf_iff by auto
subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
@@ -204,6 +241,18 @@
end
+lemma SUPR_fun_expand:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
+ shows "(SUP y:A. f y) = (\<lambda>x. SUP y:A. f y x)"
+ by (auto intro!: arg_cong[where f=Sup] ext[where 'a='b]
+ simp: SUPR_def Sup_fun_def)
+
+lemma INFI_fun_expand:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
+ shows "(INF y:A. f y) x = (INF y:A. f y x)"
+ by (auto intro!: arg_cong[where f=Inf] ext[where 'a='b]
+ simp: INFI_def Inf_fun_def)
+
lemma Inf_empty_fun:
"\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
by (simp add: Inf_fun_def)
--- a/src/HOL/Decision_Procs/Approximation.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Aug 26 09:03:18 2010 +0200
@@ -3212,8 +3212,8 @@
fun bad t = error ("Bad term: " ^ Syntax.string_of_term_global thy t);
- fun term_of_bool True = @{term True}
- | term_of_bool False = @{term False};
+ fun term_of_bool true = @{term True}
+ | term_of_bool false = @{term False};
fun term_of_float (@{code Float} (k, l)) =
@{term Float} $ HOLogic.mk_number @{typ int} k $ HOLogic.mk_number @{typ int} l;
--- a/src/HOL/Divides.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Divides.thy Thu Aug 26 09:03:18 2010 +0200
@@ -700,7 +700,7 @@
in
-val cancel_div_mod_nat_proc = Simplifier.simproc @{theory}
+val cancel_div_mod_nat_proc = Simplifier.simproc_global @{theory}
"cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
val _ = Addsimprocs [cancel_div_mod_nat_proc];
@@ -1459,7 +1459,7 @@
in
-val cancel_div_mod_int_proc = Simplifier.simproc @{theory}
+val cancel_div_mod_int_proc = Simplifier.simproc_global @{theory}
"cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
val _ = Addsimprocs [cancel_div_mod_int_proc];
--- a/src/HOL/HOL.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/HOL.thy Thu Aug 26 09:03:18 2010 +0200
@@ -57,14 +57,18 @@
False :: bool
Not :: "bool => bool" ("~ _" [40] 40)
-global consts
+setup Sign.root_path
+
+consts
"op &" :: "[bool, bool] => bool" (infixr "&" 35)
"op |" :: "[bool, bool] => bool" (infixr "|" 30)
"op -->" :: "[bool, bool] => bool" (infixr "-->" 25)
"op =" :: "['a, 'a] => bool" (infixl "=" 50)
-local consts
+setup Sign.local_path
+
+consts
The :: "('a => bool) => 'a"
All :: "('a => bool) => bool" (binder "ALL " 10)
Ex :: "('a => bool) => bool" (binder "EX " 10)
@@ -1487,13 +1491,13 @@
map (Simplifier.rewrite_rule (map Thm.symmetric
@{thms induct_rulify_fallback})))
addsimprocs
- [Simplifier.simproc @{theory} "swap_induct_false"
+ [Simplifier.simproc_global @{theory} "swap_induct_false"
["induct_false ==> PROP P ==> PROP Q"]
(fn _ => fn _ =>
(fn _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) =>
if P <> Q then SOME Drule.swap_prems_eq else NONE
| _ => NONE)),
- Simplifier.simproc @{theory} "induct_equal_conj_curry"
+ Simplifier.simproc_global @{theory} "induct_equal_conj_curry"
["induct_conj P Q ==> PROP R"]
(fn _ => fn _ =>
(fn _ $ (_ $ P) $ _ =>
@@ -1793,7 +1797,7 @@
setup {*
Code_Preproc.map_pre (fn simpset =>
- simpset addsimprocs [Simplifier.simproc_i @{theory} "eq" [@{term "op ="}]
+ simpset addsimprocs [Simplifier.simproc_global_i @{theory} "eq" [@{term "op ="}]
(fn thy => fn _ => fn Const (_, T) => case strip_type T
of (Type _ :: _, _) => SOME @{thm equals_eq}
| _ => NONE)])
--- a/src/HOL/Import/shuffler.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Import/shuffler.ML Thu Aug 26 09:03:18 2010 +0200
@@ -421,29 +421,29 @@
val S = mk_free "S" xT
val S' = mk_free "S'" xT
in
-fun beta_simproc thy = Simplifier.simproc_i
+fun beta_simproc thy = Simplifier.simproc_global_i
thy
"Beta-contraction"
[Abs("x",xT,Q) $ S]
beta_fun
-fun equals_simproc thy = Simplifier.simproc_i
+fun equals_simproc thy = Simplifier.simproc_global_i
thy
"Ordered rewriting of meta equalities"
[Const("op ==",xT) $ S $ S']
equals_fun
-fun quant_simproc thy = Simplifier.simproc_i
+fun quant_simproc thy = Simplifier.simproc_global_i
thy
"Ordered rewriting of nested quantifiers"
[Logic.all x (Logic.all y (P $ x $ y))]
quant_rewrite
-fun eta_expand_simproc thy = Simplifier.simproc_i
+fun eta_expand_simproc thy = Simplifier.simproc_global_i
thy
"Smart eta-expansion by equivalences"
[Logic.mk_equals(Q,R)]
eta_expand
-fun eta_contract_simproc thy = Simplifier.simproc_i
+fun eta_contract_simproc thy = Simplifier.simproc_global_i
thy
"Smart handling of eta-contractions"
[Logic.all x (Logic.mk_equals (Q $ x, R $ x))]
--- a/src/HOL/List.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/List.thy Thu Aug 26 09:03:18 2010 +0200
@@ -732,7 +732,7 @@
in
val list_eq_simproc =
- Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
+ Simplifier.simproc_global @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
end;
--- a/src/HOL/NSA/HyperDef.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/NSA/HyperDef.thy Thu Aug 26 09:03:18 2010 +0200
@@ -349,7 +349,7 @@
@{thm star_of_number_of}, @{thm star_of_add}, @{thm star_of_minus},
@{thm star_of_diff}, @{thm star_of_mult}]
#> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})
- #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc @{theory}
+ #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc_global @{theory}
"fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
(K Lin_Arith.simproc)]))
*}
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Aug 26 09:03:18 2010 +0200
@@ -146,7 +146,7 @@
| perm_simproc' thy ss _ = NONE;
val perm_simproc =
- Simplifier.simproc @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
+ Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
val meta_spec = thm "meta_spec";
--- a/src/HOL/Nominal/nominal_inductive.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Aug 26 09:03:18 2010 +0200
@@ -40,7 +40,7 @@
fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
[(perm_boolI_pi, pi)] perm_boolI;
-fun mk_perm_bool_simproc names = Simplifier.simproc_i
+fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
(theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
fn Const ("Nominal.perm", _) $ _ $ t =>
if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Aug 26 09:03:18 2010 +0200
@@ -8,7 +8,8 @@
signature NOMINAL_INDUCTIVE2 =
sig
- val prove_strong_ind: string -> string option -> (string * string list) list -> local_theory -> Proof.state
+ val prove_strong_ind: string -> string option -> (string * string list) list ->
+ local_theory -> Proof.state
end
structure NominalInductive2 : NOMINAL_INDUCTIVE2 =
@@ -43,7 +44,7 @@
fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
[(perm_boolI_pi, pi)] perm_boolI;
-fun mk_perm_bool_simproc names = Simplifier.simproc_i
+fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
(theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
fn Const ("Nominal.perm", _) $ _ $ t =>
if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
--- a/src/HOL/Nominal/nominal_permeq.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Thu Aug 26 09:03:18 2010 +0200
@@ -114,7 +114,7 @@
| _ => NONE
end
-val perm_simproc_app = Simplifier.simproc @{theory} "perm_simproc_app"
+val perm_simproc_app = Simplifier.simproc_global @{theory} "perm_simproc_app"
["Nominal.perm pi x"] perm_simproc_app';
(* a simproc that deals with permutation instances in front of functions *)
@@ -134,7 +134,7 @@
| _ => NONE
end
-val perm_simproc_fun = Simplifier.simproc @{theory} "perm_simproc_fun"
+val perm_simproc_fun = Simplifier.simproc_global @{theory} "perm_simproc_fun"
["Nominal.perm pi x"] perm_simproc_fun';
(* function for simplyfying permutations *)
@@ -214,7 +214,7 @@
end
| _ => NONE);
-val perm_compose_simproc = Simplifier.simproc @{theory} "perm_compose"
+val perm_compose_simproc = Simplifier.simproc_global @{theory} "perm_compose"
["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc';
fun perm_compose_tac ss i =
--- a/src/HOL/Orderings.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Orderings.thy Thu Aug 26 09:03:18 2010 +0200
@@ -566,7 +566,7 @@
fun add_simprocs procs thy =
Simplifier.map_simpset (fn ss => ss
addsimprocs (map (fn (name, raw_ts, proc) =>
- Simplifier.simproc thy name raw_ts proc) procs)) thy;
+ Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
fun add_solver name tac =
Simplifier.map_simpset (fn ss => ss addSolver
mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
@@ -1154,7 +1154,7 @@
have "\<And>y. P y \<Longrightarrow> x \<le> y"
proof (rule classical)
fix y
- assume "P y" and "\<not> x \<le> y"
+ assume "P y" and "\<not> x \<le> y"
with less have "P (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
by (auto simp add: not_le)
with assm have "x < (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
@@ -1181,13 +1181,25 @@
"\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
by (blast intro: LeastI_ex)
+lemma LeastI2_wellorder:
+ assumes "P a"
+ and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
+ shows "Q (Least P)"
+proof (rule LeastI2_order)
+ show "P (Least P)" using `P a` by (rule LeastI)
+next
+ fix y assume "P y" thus "Least P \<le> y" by (rule Least_le)
+next
+ fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2))
+qed
+
lemma not_less_Least: "k < (LEAST x. P x) \<Longrightarrow> \<not> P k"
apply (simp (no_asm_use) add: not_le [symmetric])
apply (erule contrapos_nn)
apply (erule Least_le)
done
-end
+end
subsection {* Order on bool *}
--- a/src/HOL/Probability/Borel.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Probability/Borel.thy Thu Aug 26 09:03:18 2010 +0200
@@ -1238,7 +1238,7 @@
proof safe
fix a
have "{x\<in>space M. a < ?sup x} = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
- by (auto simp: less_Sup_iff SUPR_def[where 'a=pinfreal] SUPR_fun_expand[where 'b=pinfreal])
+ by (auto simp: less_Sup_iff SUPR_def[where 'a=pinfreal] SUPR_fun_expand[where 'c=pinfreal])
then show "{x\<in>space M. a < ?sup x} \<in> sets M"
using assms by auto
qed
--- a/src/HOL/Probability/Lebesgue_Integration.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Thu Aug 26 09:03:18 2010 +0200
@@ -57,7 +57,7 @@
shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f -` {y} \<inter> space M) x)"
(is "?l = ?r")
proof -
- have "?r = (\<Sum>y \<in> f ` space M.
+ have "?r = (\<Sum>y \<in> f ` space M.
(if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))"
by (auto intro!: setsum_cong2)
also have "... = f x * indicator (f -` {f x} \<inter> space M) x"
@@ -222,19 +222,6 @@
by (simp add: if_distrib setsum_cases[OF `finite P`])
qed
-lemma LeastI2_wellorder:
- fixes a :: "_ :: wellorder"
- assumes "P a"
- and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
- shows "Q (Least P)"
-proof (rule LeastI2_order)
- show "P (Least P)" using `P a` by (rule LeastI)
-next
- fix y assume "P y" thus "Least P \<le> y" by (rule Least_le)
-next
- fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2))
-qed
-
lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence:
fixes u :: "'a \<Rightarrow> pinfreal"
assumes u: "u \<in> borel_measurable M"
@@ -399,7 +386,8 @@
let ?N = "max n (natfloor r + 1)"
have "u t < of_nat ?N" "n \<le> ?N"
using ge_natfloor_plus_one_imp_gt[of r n] preal
- by (auto simp: max_def real_Suc_natfloor)
+ using real_natfloor_add_one_gt
+ by (auto simp: max_def real_of_nat_Suc)
from lower[OF this(1)]
have "r < (real (f t ?N) + 1) / 2 ^ ?N" unfolding less_divide_eq
using preal by (auto simp add: power_le_zero_eq zero_le_mult_iff real_of_nat_Suc split: split_if_asm)
@@ -875,7 +863,7 @@
moreover
have "a * (SUP i. simple_integral (?uB i)) \<le> ?S"
unfolding pinfreal_SUP_cmult[symmetric]
- proof (safe intro!: SUP_mono)
+ proof (safe intro!: SUP_mono bexI)
fix i
have "a * simple_integral (?uB i) = simple_integral (\<lambda>x. a * ?uB i x)"
using B `simple_function u`
@@ -890,7 +878,7 @@
qed
finally show "a * simple_integral (?uB i) \<le> positive_integral (f i)"
by auto
- qed
+ qed simp
ultimately show "a * simple_integral u \<le> ?S" by simp
qed
@@ -1056,16 +1044,17 @@
by (auto intro!: borel_measurable_SUP borel_measurable_INF assms)
have "(\<lambda>n. INF m. u (m + n)) \<up> (SUP n. INF m. u (m + n))"
- proof (unfold isoton_def, safe)
- fix i show "(INF m. u (m + i)) \<le> (INF m. u (m + Suc i))"
- by (rule INF_mono[where N=Suc]) simp
- qed
+ proof (unfold isoton_def, safe intro!: INF_mono bexI)
+ fix i m show "u (Suc m + i) \<le> u (m + Suc i)" by simp
+ qed simp
from positive_integral_isoton[OF this] assms
have "positive_integral (SUP n. INF m. u (m + n)) =
(SUP n. positive_integral (INF m. u (m + n)))"
unfolding isoton_def by (simp add: borel_measurable_INF)
also have "\<dots> \<le> (SUP n. INF m. positive_integral (u (m + n)))"
- by (auto intro!: SUP_mono[where N="\<lambda>x. x"] INFI_bound positive_integral_mono INF_leI simp: INFI_fun_expand)
+ apply (rule SUP_mono)
+ apply (rule_tac x=n in bexI)
+ by (auto intro!: positive_integral_mono INFI_bound INF_leI exI simp: INFI_fun_expand)
finally show ?thesis .
qed
@@ -1123,10 +1112,10 @@
have "?I = (SUP i. positive_integral (\<lambda>x. min (of_nat i) (u x) * indicator N x))"
unfolding isoton_def using borel `N \<in> sets M` by (simp add: borel_measurable_indicator)
also have "\<dots> \<le> (SUP i. positive_integral (\<lambda>x. of_nat i * indicator N x))"
- proof (rule SUP_mono, rule positive_integral_mono)
+ proof (rule SUP_mono, rule bexI, rule positive_integral_mono)
fix x i show "min (of_nat i) (u x) * indicator N x \<le> of_nat i * indicator N x"
by (cases "x \<in> N") auto
- qed
+ qed simp
also have "\<dots> = 0"
using `N \<in> null_sets` by (simp add: positive_integral_cmult_indicator)
finally show ?thesis by simp
@@ -1967,46 +1956,37 @@
unfolding finite_measure_space_def finite_measure_space_axioms_def
using assms by simp
-lemma (in finite_measure_space) borel_measurable_finite[intro, simp]:
- fixes f :: "'a \<Rightarrow> real"
- shows "f \<in> borel_measurable M"
+lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M"
unfolding measurable_def sets_eq_Pow by auto
+lemma (in finite_measure_space) simple_function_finite: "simple_function f"
+ unfolding simple_function_def sets_eq_Pow using finite_space by auto
+
+lemma (in finite_measure_space) positive_integral_finite_eq_setsum:
+ "positive_integral f = (\<Sum>x \<in> space M. f x * \<mu> {x})"
+proof -
+ have *: "positive_integral f = positive_integral (\<lambda>x. \<Sum>y\<in>space M. f y * indicator {y} x)"
+ by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space])
+ show ?thesis unfolding * using borel_measurable_finite[of f]
+ by (simp add: positive_integral_setsum positive_integral_cmult_indicator sets_eq_Pow)
+qed
+
lemma (in finite_measure_space) integral_finite_singleton:
shows "integrable f"
and "integral f = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))" (is ?I)
proof -
- have 1: "f \<in> borel_measurable M"
- unfolding measurable_def sets_eq_Pow by auto
-
- have 2: "finite (f`space M)" using finite_space by simp
-
- have 3: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<omega>"
- using finite_measure[unfolded sets_eq_Pow] by simp
-
- show "integrable f"
- by (rule integral_on_finite(1)[OF 1 2 3]) simp
+ have [simp]:
+ "positive_integral (\<lambda>x. Real (f x)) = (\<Sum>x \<in> space M. Real (f x) * \<mu> {x})"
+ "positive_integral (\<lambda>x. Real (- f x)) = (\<Sum>x \<in> space M. Real (- f x) * \<mu> {x})"
+ unfolding positive_integral_finite_eq_setsum by auto
- { fix r let ?x = "f -` {r} \<inter> space M"
- have "?x \<subseteq> space M" by auto
- with finite_space sets_eq_Pow finite_single_measure
- have "real (\<mu> ?x) = (\<Sum>i \<in> ?x. real (\<mu> {i}))"
- using real_measure_setsum_singleton[of ?x] by auto }
- note measure_eq_setsum = this
+ show "integrable f" using finite_space finite_measure
+ by (simp add: setsum_\<omega> integrable_def sets_eq_Pow)
- have "integral f = (\<Sum>r\<in>f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))"
- by (rule integral_on_finite(2)[OF 1 2 3]) simp
- also have "\<dots> = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))"
- unfolding measure_eq_setsum setsum_right_distrib
- apply (subst setsum_Sigma)
- apply (simp add: finite_space)
- apply (simp add: finite_space)
- proof (rule setsum_reindex_cong[symmetric])
- fix a assume "a \<in> Sigma (f ` space M) (\<lambda>x. f -` {x} \<inter> space M)"
- thus "(\<lambda>(x, y). x * real (\<mu> {y})) a = f (snd a) * real (\<mu> {snd a})"
- by auto
- qed (auto intro!: image_eqI inj_onI)
- finally show ?I .
+ show ?I using finite_measure
+ apply (simp add: integral_def sets_eq_Pow real_of_pinfreal_setsum[symmetric]
+ real_of_pinfreal_mult[symmetric] setsum_subtractf[symmetric])
+ by (rule setsum_cong) (simp_all split: split_if)
qed
end
--- a/src/HOL/Probability/Positive_Infinite_Real.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Probability/Positive_Infinite_Real.thy Thu Aug 26 09:03:18 2010 +0200
@@ -6,53 +6,20 @@
imports Complex_Main Nat_Bijection Multivariate_Analysis
begin
-lemma less_Sup_iff:
- fixes a :: "'x\<Colon>{complete_lattice,linorder}"
- shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
- unfolding not_le[symmetric] Sup_le_iff by auto
-
-lemma Inf_less_iff:
- fixes a :: "'x\<Colon>{complete_lattice,linorder}"
- shows "Inf S < a \<longleftrightarrow> (\<exists> x \<in> S. x < a)"
- unfolding not_le[symmetric] le_Inf_iff by auto
-
-lemma SUPR_fun_expand: "(SUP y:A. f y) = (\<lambda>x. SUP y:A. f y x)"
- unfolding SUPR_def expand_fun_eq Sup_fun_def
- by (auto intro!: arg_cong[where f=Sup])
-
-lemma real_Suc_natfloor: "r < real (Suc (natfloor r))"
-proof cases
- assume "0 \<le> r"
- from floor_correct[of r]
- have "r < real (\<lfloor>r\<rfloor> + 1)" by auto
- also have "\<dots> = real (Suc (natfloor r))"
- using `0 \<le> r` by (auto simp: real_of_nat_Suc natfloor_def)
- finally show ?thesis .
-next
- assume "\<not> 0 \<le> r"
- hence "r < 0" by auto
- also have "0 < real (Suc (natfloor r))" by auto
- finally show ?thesis .
+lemma (in complete_lattice) Sup_start:
+ assumes *: "\<And>x. f x \<le> f 0"
+ shows "(SUP n. f n) = f 0"
+proof (rule antisym)
+ show "f 0 \<le> (SUP n. f n)" by (rule le_SUPI) auto
+ show "(SUP n. f n) \<le> f 0" by (rule SUP_leI[OF *])
qed
-lemma (in complete_lattice) Sup_mono:
- assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
- shows "Sup A \<le> Sup B"
-proof (rule Sup_least)
- fix a assume "a \<in> A"
- with assms obtain b where "b \<in> B" and "a \<le> b" by auto
- hence "b \<le> Sup B" by (auto intro: Sup_upper)
- with `a \<le> b` show "a \<le> Sup B" by auto
-qed
-
-lemma (in complete_lattice) Inf_mono:
- assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
- shows "Inf A \<le> Inf B"
-proof (rule Inf_greatest)
- fix b assume "b \<in> B"
- with assms obtain a where "a \<in> A" and "a \<le> b" by auto
- hence "Inf A \<le> a" by (auto intro: Inf_lower)
- with `a \<le> b` show "Inf A \<le> b" by auto
+lemma (in complete_lattice) Inf_start:
+ assumes *: "\<And>x. f 0 \<le> f x"
+ shows "(INF n. f n) = f 0"
+proof (rule antisym)
+ show "(INF n. f n) \<le> f 0" by (rule INF_leI) simp
+ show "f 0 \<le> (INF n. f n)" by (rule le_INFI[OF *])
qed
lemma (in complete_lattice) Sup_mono_offset:
@@ -77,12 +44,18 @@
apply (rule Sup_mono_offset)
by (auto intro!: order.lift_Suc_mono_le[of "op \<le>" "op <" f, OF _ *]) default
-lemma (in complete_lattice) Inf_start:
- assumes *: "\<And>x. f 0 \<le> f x"
- shows "(INF n. f n) = f 0"
+lemma (in complete_lattice) Inf_mono_offset:
+ fixes f :: "'b :: {ordered_ab_semigroup_add,monoid_add} \<Rightarrow> 'a"
+ assumes *: "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x" and "0 \<le> k"
+ shows "(INF n . f (k + n)) = (INF n. f n)"
proof (rule antisym)
- show "(INF n. f n) \<le> f 0" by (rule INF_leI) simp
- show "f 0 \<le> (INF n. f n)" by (rule le_INFI[OF *])
+ show "(INF n. f n) \<le> (INF n. f (k + n))"
+ by (auto intro!: Inf_mono simp: INFI_def)
+ { fix n :: 'b
+ have "0 + n \<le> k + n" using `0 \<le> k` by (rule add_right_mono)
+ with * have "f (k + n) \<le> f n" by simp }
+ thus "(INF n. f (k + n)) \<le> (INF n. f n)"
+ by (auto intro!: Inf_mono exI simp: INFI_def)
qed
lemma (in complete_lattice) isotone_converge:
@@ -99,28 +72,6 @@
ultimately show ?thesis by simp
qed
-lemma (in complete_lattice) Inf_mono_offset:
- fixes f :: "'b :: {ordered_ab_semigroup_add,monoid_add} \<Rightarrow> 'a"
- assumes *: "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x" and "0 \<le> k"
- shows "(INF n . f (k + n)) = (INF n. f n)"
-proof (rule antisym)
- show "(INF n. f n) \<le> (INF n. f (k + n))"
- by (auto intro!: Inf_mono simp: INFI_def)
- { fix n :: 'b
- have "0 + n \<le> k + n" using `0 \<le> k` by (rule add_right_mono)
- with * have "f (k + n) \<le> f n" by simp }
- thus "(INF n. f (k + n)) \<le> (INF n. f n)"
- by (auto intro!: Inf_mono exI simp: INFI_def)
-qed
-
-lemma (in complete_lattice) Sup_start:
- assumes *: "\<And>x. f x \<le> f 0"
- shows "(SUP n. f n) = f 0"
-proof (rule antisym)
- show "f 0 \<le> (SUP n. f n)" by (rule le_SUPI) auto
- show "(SUP n. f n) \<le> f 0" by (rule SUP_leI[OF *])
-qed
-
lemma (in complete_lattice) antitone_converges:
fixes f :: "nat \<Rightarrow> 'a" assumes "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x"
shows "(INF n. SUP m. f (n + m)) = (SUP n. INF m. f (n + m))"
@@ -1657,15 +1608,6 @@
"1 \<le> Real p \<longleftrightarrow> 1 \<le> p"
by (simp_all add: one_pinfreal_def del: Real_1)
-lemma SUP_mono:
- assumes "\<And>n. f n \<le> g (N n)"
- shows "(SUP n. f n) \<le> (SUP n. g n)"
-proof (safe intro!: SUPR_bound)
- fix n note assms[of n]
- also have "g (N n) \<le> (SUP n. g n)" by (auto intro!: le_SUPI)
- finally show "f n \<le> (SUP n. g n)" .
-qed
-
lemma isoton_Sup:
assumes "f \<up> u"
shows "f i \<le> u"
@@ -2563,20 +2505,6 @@
shows "x \<le> (INF n. f n)"
using assms by (simp add: INFI_def le_Inf_iff)
-lemma INF_mono:
- assumes "\<And>n. f (N n) \<le> g n"
- shows "(INF n. f n) \<le> (INF n. g n)"
-proof (safe intro!: INFI_bound)
- fix n
- have "(INF n. f n) \<le> f (N n)" by (auto intro!: INF_leI)
- also note assms[of n]
- finally show "(INF n. f n) \<le> g n" .
-qed
-
-lemma INFI_fun_expand: "(INF y:A. f y) = (\<lambda>x. INF y:A. f y x)"
- unfolding INFI_def expand_fun_eq Inf_fun_def
- by (auto intro!: arg_cong[where f=Inf])
-
lemma LIMSEQ_imp_lim_INF:
assumes pos: "\<And>i. 0 \<le> X i" and lim: "X ----> x"
shows "(SUP n. INF m. Real (X (n + m))) = Real x"
@@ -2596,11 +2524,11 @@
proof safe
fix x y :: nat assume "x \<le> y"
have "Real (r x) \<le> Real (r y)" unfolding r(1)[symmetric] using pos
- proof (safe intro!: INF_mono)
+ proof (safe intro!: INF_mono bexI)
fix m have "x + (m + y - x) = y + m"
using `x \<le> y` by auto
thus "Real (X (x + (m + y - x))) \<le> Real (X (y + m))" by simp
- qed
+ qed simp
thus "r x \<le> r y" using r by auto
qed
show "\<And>n. 0 \<le> r n" by fact
@@ -2646,7 +2574,6 @@
qed
qed
-
lemma real_of_pinfreal_strict_mono_iff:
"real a < real b \<longleftrightarrow> (b \<noteq> \<omega> \<and> ((a = \<omega> \<and> 0 < b) \<or> (a < b)))"
proof (cases a)
--- a/src/HOL/Probability/Product_Measure.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Probability/Product_Measure.thy Thu Aug 26 09:03:18 2010 +0200
@@ -87,22 +87,6 @@
shows "sigma_finite_measure (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"
oops
-lemma (in finite_measure_space) simple_function_finite:
- "simple_function f"
- unfolding simple_function_def sets_eq_Pow using finite_space by auto
-
-lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M"
- unfolding measurable_def sets_eq_Pow by auto
-
-lemma (in finite_measure_space) positive_integral_finite_eq_setsum:
- "positive_integral f = (\<Sum>x \<in> space M. f x * \<mu> {x})"
-proof -
- have *: "positive_integral f = positive_integral (\<lambda>x. \<Sum>y\<in>space M. f y * indicator {y} x)"
- by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space])
- show ?thesis unfolding * using borel_measurable_finite[of f]
- by (simp add: positive_integral_setsum positive_integral_cmult_indicator sets_eq_Pow)
-qed
-
lemma (in finite_measure_space) finite_prod_measure_times:
assumes "finite_measure_space N \<nu>"
and "A1 \<in> sets M" "A2 \<in> sets N"
--- a/src/HOL/Product_Type.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Product_Type.thy Thu Aug 26 09:03:18 2010 +0200
@@ -58,7 +58,7 @@
ML {*
val unit_eq_proc =
let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
- Simplifier.simproc @{theory} "unit_eq" ["x::unit"]
+ Simplifier.simproc_global @{theory} "unit_eq" ["x::unit"]
(fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq)
end;
@@ -550,8 +550,8 @@
| NONE => NONE)
| eta_proc _ _ = NONE;
in
- val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc);
- val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc);
+ val split_beta_proc = Simplifier.simproc_global @{theory} "split_beta" ["split f z"] (K beta_proc);
+ val split_eta_proc = Simplifier.simproc_global @{theory} "split_eta" ["split f"] (K eta_proc);
end;
Addsimprocs [split_beta_proc, split_eta_proc];
--- a/src/HOL/Quotient.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Quotient.thy Thu Aug 26 09:03:18 2010 +0200
@@ -571,7 +571,8 @@
apply metis
done
-lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
+lemma bex1_bexeq_reg:
+ shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
apply (simp add: Ex1_def Bex1_rel_def in_respects)
apply clarify
apply auto
@@ -582,6 +583,23 @@
apply auto
done
+lemma bex1_bexeq_reg_eqv:
+ assumes a: "equivp R"
+ shows "(\<exists>!x. P x) \<longrightarrow> Bex1_rel R P"
+ using equivp_reflp[OF a]
+ apply (intro impI)
+ apply (elim ex1E)
+ apply (rule mp[OF bex1_bexeq_reg])
+ apply (rule_tac a="x" in ex1I)
+ apply (subst in_respects)
+ apply (rule conjI)
+ apply assumption
+ apply assumption
+ apply clarify
+ apply (erule_tac x="xa" in allE)
+ apply simp
+ done
+
subsection {* Various respects and preserve lemmas *}
lemma quot_rel_rsp:
--- a/src/HOL/Set.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Set.thy Thu Aug 26 09:03:18 2010 +0200
@@ -78,7 +78,7 @@
val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
- val defColl_regroup = Simplifier.simproc @{theory}
+ val defColl_regroup = Simplifier.simproc_global @{theory}
"defined Collect" ["{x. P x & Q x}"]
(Quantifier1.rearrange_Coll Coll_perm_tac)
in
@@ -323,9 +323,9 @@
val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
- val defBEX_regroup = Simplifier.simproc @{theory}
+ val defBEX_regroup = Simplifier.simproc_global @{theory}
"defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
- val defBALL_regroup = Simplifier.simproc @{theory}
+ val defBALL_regroup = Simplifier.simproc_global @{theory}
"defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
in
Simplifier.map_simpset (fn ss => ss addsimprocs [defBALL_regroup, defBEX_regroup])
--- a/src/HOL/Statespace/distinct_tree_prover.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Thu Aug 26 09:03:18 2010 +0200
@@ -355,7 +355,7 @@
| NONE => fn i => no_tac)
fun distinct_simproc names =
- Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
+ Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
(fn thy => fn ss => fn (Const (@{const_name "op ="},_)$x$y) =>
case try Simplifier.the_context ss of
SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq])
--- a/src/HOL/Statespace/state_fun.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML Thu Aug 26 09:03:18 2010 +0200
@@ -51,7 +51,7 @@
in
val lazy_conj_simproc =
- Simplifier.simproc @{theory HOL} "lazy_conj_simp" ["P & Q"]
+ Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
(fn thy => fn ss => fn t =>
(case t of (Const (@{const_name "op &"},_)$P$Q) =>
let
@@ -108,7 +108,7 @@
Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));
val lookup_simproc =
- Simplifier.simproc @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
+ Simplifier.simproc_global @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
(fn thy => fn ss => fn t =>
(case t of (Const ("StateFun.lookup",lT)$destr$n$
(s as Const ("StateFun.update",uT)$_$_$_$_$_)) =>
@@ -162,7 +162,7 @@
addcongs @{thms block_conj_cong});
in
val update_simproc =
- Simplifier.simproc @{theory} "update_simp" ["update d c n v s"]
+ Simplifier.simproc_global @{theory} "update_simp" ["update d c n v s"]
(fn thy => fn ss => fn t =>
(case t of ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
let
@@ -263,7 +263,7 @@
end;
in
val ex_lookup_eq_simproc =
- Simplifier.simproc @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
+ Simplifier.simproc_global @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
(fn thy => fn ss => fn t =>
let
val ctxt = Simplifier.the_context ss |>
--- a/src/HOL/Statespace/state_space.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Thu Aug 26 09:03:18 2010 +0200
@@ -235,7 +235,7 @@
| NONE => fn i => no_tac)
val distinct_simproc =
- Simplifier.simproc @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
+ Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
(fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
(case try Simplifier.the_context ss of
SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Aug 26 09:03:18 2010 +0200
@@ -163,7 +163,7 @@
val thy = ProofContext.theory_of ctxt
val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
- val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
+ val simproc = Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
val simpset = (mk_minimal_ss ctxt)
addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
addsimprocs [simproc]
@@ -310,7 +310,7 @@
-(* Injection means to prove that the regularised theorem implies
+(* Injection means to prove that the regularized theorem implies
the abs/rep injected one.
The deterministic part:
@@ -541,8 +541,7 @@
end
-
-(** Tactic for Generalising Free Variables in a Goal **)
+(* Tactic for Generalising Free Variables in a Goal *)
fun inst_spec ctrm =
Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
@@ -649,13 +648,20 @@
(** lifting as a tactic **)
+
(* the tactic leaves three subgoals to be proved *)
fun lift_procedure_tac ctxt rthm =
Object_Logic.full_atomize_tac
THEN' gen_frees_tac ctxt
THEN' SUBGOAL (fn (goal, i) =>
let
- val rthm' = atomize_thm rthm
+ (* full_atomize_tac contracts eta redexes,
+ so we do it also in the original theorem *)
+ val rthm' =
+ rthm |> Drule.eta_contraction_rule
+ |> Thm.forall_intr_frees
+ |> atomize_thm
+
val rule = procedure_inst ctxt (prop_of rthm') goal
in
(rtac rule THEN' rtac rthm') i
@@ -679,18 +685,13 @@
fun lifted ctxt qtys simps rthm =
let
val ss = (mk_minimal_ss ctxt) addsimps simps
+ val rthm' = asm_full_simplify ss rthm
- (* When the theorem is atomized, eta redexes are contracted,
- so we do it both in the original theorem *)
- val rthm' =
- rthm
- |> asm_full_simplify ss
- |> Drule.eta_contraction_rule
val ((_, [rthm'']), ctxt') = Variable.import true [rthm'] ctxt
val goal = derive_qtrm ctxt' qtys (prop_of rthm'')
in
Goal.prove ctxt' [] [] goal
- (K ((asm_full_simp_tac ss THEN' lift_single_tac ctxt' rthm') 1))
+ (K (EVERY1 [asm_full_simp_tac ss, lift_single_tac ctxt' rthm'']))
|> singleton (ProofContext.export ctxt' ctxt)
end
--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Aug 26 09:03:18 2010 +0200
@@ -68,7 +68,7 @@
let
val thy = ProofContext.theory_of ctxt
val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
- val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
+ val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exn
in
Const (mapfun, dummyT)
end
@@ -105,7 +105,7 @@
let
val thy = ProofContext.theory_of ctxt
val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
- val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound => raise exn
+ val qdata = quotdata_lookup thy s handle NotFound => raise exn
in
(#rtyp qdata, #qtyp qdata)
end
@@ -277,7 +277,7 @@
let
val thy = ProofContext.theory_of ctxt
val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
- val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
+ val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exn
in
Const (relmap, dummyT)
end
@@ -301,7 +301,7 @@
val thy = ProofContext.theory_of ctxt
val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
in
- #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
+ #equiv_rel (quotdata_lookup thy s) handle NotFound => raise exn
end
fun equiv_match_err ctxt ty_pat ty =
@@ -436,7 +436,7 @@
if length rtys <> length qtys then false else
forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
else
- (case Quotient_Info.quotdata_lookup_raw thy qs of
+ (case quotdata_lookup_raw thy qs of
SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
| NONE => false)
| _ => false
@@ -446,7 +446,7 @@
- the result might contain dummyTs
- - for regularisation we do not need any
+ - for regularization we do not need any
special treatment of bound variables
*)
fun regularize_trm ctxt (rtrm, qtrm) =
@@ -550,7 +550,7 @@
val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
in
if rel' aconv rel then rtrm
- else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
+ else term_mismatch "regularize (relation mismatch)" ctxt rel rel'
end
| (_, Const _) =>
@@ -563,10 +563,10 @@
else
let
val rtrm' = #rconst (qconsts_lookup thy qtrm)
- handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm
+ handle NotFound => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
in
if Pattern.matches thy (rtrm', rtrm)
- then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm
+ then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
end
end
@@ -751,7 +751,7 @@
let
val thy = ProofContext.theory_of ctxt
in
- Quotient_Info.quotdata_dest ctxt
+ quotdata_dest ctxt
|> map (fn x => (#rtyp x, #qtyp x))
|> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
|> map (if direction then swap else I)
@@ -763,12 +763,12 @@
fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
val const_substs =
- Quotient_Info.qconsts_dest ctxt
+ qconsts_dest ctxt
|> map (fn x => (#rconst x, #qconst x))
|> map (if direction then swap else I)
val rel_substs =
- Quotient_Info.quotdata_dest ctxt
+ quotdata_dest ctxt
|> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
|> map (if direction then swap else I)
in
--- a/src/HOL/Tools/SMT/smt_real.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML Thu Aug 26 09:03:18 2010 +0200
@@ -127,7 +127,7 @@
"x + y = y + x"
by auto}
-val real_linarith_proc = Simplifier.simproc @{theory} "fast_real_arith" [
+val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
"(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Thu Aug 26 09:03:18 2010 +0200
@@ -323,11 +323,11 @@
addsimps @{thms array_rules}
addsimps @{thms z3div_def} addsimps @{thms z3mod_def}
addsimprocs [
- Simplifier.simproc @{theory} "fast_int_arith" [
+ Simplifier.simproc_global @{theory} "fast_int_arith" [
"(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),
- Simplifier.simproc @{theory} "antisym_le" ["(x::'a::order) <= y"]
+ Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"]
(K prove_antisym_le),
- Simplifier.simproc @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
+ Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
(K prove_antisym_less)]
structure Simpset = Generic_Data
--- a/src/HOL/Tools/abel_cancel.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Tools/abel_cancel.ML Thu Aug 26 09:03:18 2010 +0200
@@ -87,7 +87,7 @@
NONE
| solve _ = NONE;
-val simproc = Simplifier.simproc @{theory}
+val simproc = Simplifier.simproc_global @{theory}
"add_ac_proc" ["x + y::'a::ab_semigroup_add"] ((K o K) solve);
val cancel_ss = HOL_basic_ss settermless less_agrp
--- a/src/HOL/Tools/arith_data.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Tools/arith_data.ML Thu Aug 26 09:03:18 2010 +0200
@@ -127,6 +127,6 @@
| trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
fun prep_simproc thy (name, pats, proc) =
- Simplifier.simproc thy name pats proc;
+ Simplifier.simproc_global thy name pats proc;
end;
--- a/src/HOL/Tools/inductive_set.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML Thu Aug 26 09:03:18 2010 +0200
@@ -32,7 +32,7 @@
(**** simplify {(x1, ..., xn). (x1, ..., xn) : S} to S ****)
val collect_mem_simproc =
- Simplifier.simproc @{theory Set} "Collect_mem" ["Collect t"] (fn thy => fn ss =>
+ Simplifier.simproc_global @{theory Set} "Collect_mem" ["Collect t"] (fn thy => fn ss =>
fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
let val (u, _, ps) = HOLogic.strip_psplits t
in case u of
@@ -67,7 +67,7 @@
val anyt = Free ("t", TFree ("'t", []));
fun strong_ind_simproc tab =
- Simplifier.simproc_i @{theory HOL} "strong_ind" [anyt] (fn thy => fn ss => fn t =>
+ Simplifier.simproc_global_i @{theory HOL} "strong_ind" [anyt] (fn thy => fn ss => fn t =>
let
fun close p t f =
let val vs = Term.add_vars t []
@@ -320,7 +320,7 @@
fun to_pred_simproc rules =
let val rules' = map mk_meta_eq rules
in
- Simplifier.simproc_i @{theory HOL} "to_pred" [anyt]
+ Simplifier.simproc_global_i @{theory HOL} "to_pred" [anyt]
(fn thy => K (lookup_rule thy (prop_of #> Logic.dest_equals) rules'))
end;
--- a/src/HOL/Tools/int_arith.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Tools/int_arith.ML Thu Aug 26 09:03:18 2010 +0200
@@ -79,7 +79,7 @@
proc = sproc, identifier = []}
val fast_int_arith_simproc =
- Simplifier.simproc @{theory} "fast_int_arith"
+ Simplifier.simproc_global @{theory} "fast_int_arith"
["(m::'a::{linordered_idom,number_ring}) < n",
"(m::'a::{linordered_idom,number_ring}) <= n",
"(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
--- a/src/HOL/Tools/lin_arith.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Thu Aug 26 09:03:18 2010 +0200
@@ -910,7 +910,7 @@
val setup =
init_arith_data #>
- Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc (@{theory}) "fast_nat_arith"
+ Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc_global (@{theory}) "fast_nat_arith"
["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K simproc)]
(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
useful to detect inconsistencies among the premises for subgoals which are
--- a/src/HOL/Tools/meson.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Tools/meson.ML Thu Aug 26 09:03:18 2010 +0200
@@ -107,7 +107,7 @@
| NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
fun flexflex_first_order th =
- case (tpairs_of th) of
+ case Thm.tpairs_of th of
[] => th
| pairs =>
let val thy = theory_of_thm th
--- a/src/HOL/Tools/nat_arith.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Tools/nat_arith.ML Thu Aug 26 09:03:18 2010 +0200
@@ -91,18 +91,18 @@
end);
val nat_cancel_sums_add =
- [Simplifier.simproc @{theory} "nateq_cancel_sums"
+ [Simplifier.simproc_global @{theory} "nateq_cancel_sums"
["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
(K EqCancelSums.proc),
- Simplifier.simproc @{theory} "natless_cancel_sums"
+ Simplifier.simproc_global @{theory} "natless_cancel_sums"
["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
(K LessCancelSums.proc),
- Simplifier.simproc @{theory} "natle_cancel_sums"
+ Simplifier.simproc_global @{theory} "natle_cancel_sums"
["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
(K LeCancelSums.proc)];
val nat_cancel_sums = nat_cancel_sums_add @
- [Simplifier.simproc @{theory} "natdiff_cancel_sums"
+ [Simplifier.simproc_global @{theory} "natdiff_cancel_sums"
["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
(K DiffCancelSums.proc)];
--- a/src/HOL/Tools/record.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Tools/record.ML Thu Aug 26 09:03:18 2010 +0200
@@ -1172,7 +1172,7 @@
subrecord.
*)
val simproc =
- Simplifier.simproc @{theory HOL} "record_simp" ["x"]
+ Simplifier.simproc_global @{theory HOL} "record_simp" ["x"]
(fn thy => fn _ => fn t =>
(case t of
(sel as Const (s, Type (_, [_, rangeS]))) $
@@ -1246,7 +1246,7 @@
we omit considering further updates if doing so would introduce
both a more update and an update to a field within it.*)
val upd_simproc =
- Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
+ Simplifier.simproc_global @{theory HOL} "record_upd_simp" ["x"]
(fn thy => fn _ => fn t =>
let
(*We can use more-updators with other updators as long
@@ -1366,7 +1366,7 @@
Complexity: #components * #updates #updates
*)
val eq_simproc =
- Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"]
+ Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
(fn thy => fn _ => fn t =>
(case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
(case rec_id ~1 T of
@@ -1386,7 +1386,7 @@
P t = ~1: completely split
P t > 0: split up to given bound of record extensions.*)
fun split_simproc P =
- Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
+ Simplifier.simproc_global @{theory HOL} "record_split_simp" ["x"]
(fn thy => fn _ => fn t =>
(case t of
Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
@@ -1414,7 +1414,7 @@
| _ => NONE));
val ex_sel_eq_simproc =
- Simplifier.simproc @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
+ Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
(fn thy => fn ss => fn t =>
let
fun prove prop =
--- a/src/HOL/Tools/simpdata.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML Thu Aug 26 09:03:18 2010 +0200
@@ -182,11 +182,11 @@
in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
val defALL_regroup =
- Simplifier.simproc @{theory}
+ Simplifier.simproc_global @{theory}
"defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
val defEX_regroup =
- Simplifier.simproc @{theory}
+ Simplifier.simproc_global @{theory}
"defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
--- a/src/HOLCF/Tools/cont_proc.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/HOLCF/Tools/cont_proc.ML Thu Aug 26 09:03:18 2010 +0200
@@ -128,7 +128,7 @@
in Option.map fst (Seq.pull (cont_tac 1 tr)) end
in
fun cont_proc thy =
- Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;
+ Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont;
end;
fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy;
--- a/src/Pure/Isar/element.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Pure/Isar/element.ML Thu Aug 26 09:03:18 2010 +0200
@@ -467,7 +467,7 @@
fun transfer_morphism thy =
let val thy_ref = Theory.check_thy thy
- in Morphism.thm_morphism (fn th => transfer (Theory.deref thy_ref) th) end;
+ in Morphism.thm_morphism (fn th => Thm.transfer (Theory.deref thy_ref) th) end;
--- a/src/Pure/Isar/isar_syn.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Aug 26 09:03:18 2010 +0200
@@ -286,14 +286,6 @@
(* name space entry path *)
-val _ =
- Outer_Syntax.command "global" "disable prefixing of theory name" Keyword.thy_decl
- (Scan.succeed (Toplevel.theory Sign.root_path));
-
-val _ =
- Outer_Syntax.command "local" "enable prefixing of theory name" Keyword.thy_decl
- (Scan.succeed (Toplevel.theory Sign.local_path));
-
fun hide_names name hide what =
Outer_Syntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl
((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
--- a/src/Pure/PIDE/command.scala Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Pure/PIDE/command.scala Thu Aug 26 09:03:18 2010 +0200
@@ -22,22 +22,26 @@
lazy val results = reverse_results.reverse
+ def add_status(st: Markup): State = copy(status = st :: status)
+ def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
- def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
-
- def markup_root_info: Text.Info[Any] =
+ def root_info: Text.Info[Any] =
new Text.Info(command.range,
- XML.Elem(Markup(Markup.STATUS, Nil), status.map(XML.Elem(_, Nil))))
- def markup_root: Markup_Tree = markup + markup_root_info
+ XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
+ def root_markup: Markup_Tree = markup + root_info
/* message dispatch */
def accumulate(message: XML.Tree): Command.State =
message match {
- case XML.Elem(Markup(Markup.STATUS, _), body) => // FIXME explicit body check!?
- copy(status = (for (XML.Elem(markup, _) <- body) yield markup) ::: status)
+ case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
+ (this /: msgs)((state, msg) =>
+ msg match {
+ case XML.Elem(markup, Nil) => state.add_status(markup)
+ case _ => System.err.println("Ignored status message: " + msg); state
+ })
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
@@ -47,7 +51,7 @@
val range = command.decode(Position.get_range(atts).get)
val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
- add_markup(info)
+ state.add_markup(info)
case _ => System.err.println("Ignored report message: " + msg); state
})
case _ => add_result(message)
--- a/src/Pure/PIDE/markup_tree.scala Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Thu Aug 26 09:03:18 2010 +0200
@@ -11,8 +11,6 @@
import javax.swing.tree.DefaultMutableTreeNode
import scala.collection.immutable.SortedMap
-import scala.collection.mutable
-import scala.annotation.tailrec
object Markup_Tree
@@ -30,15 +28,16 @@
})
def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
+ def single(entry: Entry): T = update(empty, entry)
- def overlapping(range: Text.Range, branches: T): T =
+ def overlapping(range: Text.Range, branches: T): T = // FIXME special cases!?
{
val start = Text.Range(range.start)
val stop = Text.Range(range.stop)
+ val bs = branches.range(start, stop)
branches.get(stop) match {
- case Some(end) if range overlaps end._1.range =>
- update(branches.range(start, stop), end)
- case _ => branches.range(start, stop)
+ case Some(end) if range overlaps end._1.range => update(bs, end)
+ case _ => bs
}
}
}
@@ -65,15 +64,18 @@
new Markup_Tree(Branches.update(branches, new_info -> empty))
case Some((info, subtree)) =>
val range = info.range
- if (range != new_range && range.contains(new_range))
+ if (range.contains(new_range))
new Markup_Tree(Branches.update(branches, info -> (subtree + new_info)))
else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
- new Markup_Tree(Branches.update(Branches.empty, (new_info -> this)))
+ new Markup_Tree(Branches.single(new_info -> this))
else {
val body = Branches.overlapping(new_range, branches)
if (body.forall(e => new_range.contains(e._1))) {
- val rest = (Branches.empty /: branches)((rest, entry) =>
- if (body.isDefinedAt(entry._1)) rest else rest + entry)
+ val rest = // branches -- body, modulo workarounds for Redblack in Scala 2.8.0
+ if (body.size > 1)
+ (Branches.empty /: branches)((rest, entry) =>
+ if (body.isDefinedAt(entry._1)) rest else rest + entry)
+ else branches
new Markup_Tree(Branches.update(rest, new_info -> new Markup_Tree(body)))
}
else { // FIXME split markup!?
@@ -84,37 +86,39 @@
}
}
+ private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
+ Branches.overlapping(range, branches).toStream
+
def select[A](root_range: Text.Range)
(result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] =
{
- def stream(parent: Text.Info[A], bs: Branches.T): Stream[Text.Info[A]] =
+ def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
+ : Stream[Text.Info[A]] =
{
- val range = parent.range
- val substream =
- (for ((info_range, (info, subtree)) <- Branches.overlapping(range, bs).toStream) yield {
- if (result.isDefinedAt(info)) {
- val current = Text.Info(info_range.restrict(range), result(info))
- stream(current, subtree.branches)
- }
- else stream(parent.restrict(info_range), subtree.branches)
- }).flatten
+ stack match {
+ case (parent, (range, (info, tree)) #:: more) :: rest =>
+ val subrange = range.restrict(root_range)
+ val subtree = tree.overlapping(subrange)
+ val start = subrange.start
- def padding(last: Text.Offset, s: Stream[Text.Info[A]]): Stream[Text.Info[A]] =
- s match {
- case info #:: rest =>
- val Text.Range(start, stop) = info.range
- if (last < start)
- parent.restrict(Text.Range(last, start)) #:: info #:: padding(stop, rest)
- else info #:: padding(stop, rest)
- case Stream.Empty =>
- if (last < range.stop)
- Stream(parent.restrict(Text.Range(last, range.stop)))
- else Stream.Empty
- }
- if (substream.isEmpty) Stream(parent)
- else padding(range.start, substream)
+ if (result.isDefinedAt(info)) {
+ val next = Text.Info(subrange, result(info))
+ val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
+ if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
+ else nexts
+ }
+ else stream(last, (parent, subtree #::: more) :: rest)
+
+ case (parent, Stream.Empty) :: rest =>
+ val stop = parent.range.stop
+ val nexts = stream(stop, rest)
+ if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
+ else nexts
+
+ case Nil => Stream(Text.Info(Text.Range(last, root_range.stop), default))
+ }
}
- stream(Text.Info(root_range, default), branches)
+ stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
}
def swing_tree(parent: DefaultMutableTreeNode)
--- a/src/Pure/PIDE/text.scala Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Pure/PIDE/text.scala Thu Aug 26 09:03:18 2010 +0200
@@ -32,6 +32,9 @@
def map(f: Offset => Offset): Range = Range(f(start), f(stop))
def +(i: Offset): Range = map(_ + i)
def -(i: Offset): Range = map(_ - i)
+
+ def is_singleton: Boolean = start == stop
+
def contains(i: Offset): Boolean = start == i || start < i && i < stop
def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
--- a/src/Pure/Syntax/parser.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Pure/Syntax/parser.ML Thu Aug 26 09:03:18 2010 +0200
@@ -25,362 +25,373 @@
(** datatype gram **)
-type nt_tag = int; (*production for the NTs are stored in an array
- so we can identify NTs by their index*)
-
-datatype symb = Terminal of Lexicon.token
- | Nonterminal of nt_tag * int; (*(tag, precedence)*)
+(*production for the NTs are stored in a vector
+ so we can identify NTs by their index*)
+type nt_tag = int;
-type nt_gram = ((nt_tag list * Lexicon.token list) *
- (Lexicon.token option * (symb list * string * int) list) list);
- (*(([dependent_nts], [start_tokens]),
- [(start_token, [(rhs, name, prio)])])*)
- (*depent_nts is a list of all NTs whose lookahead
- depends on this NT's lookahead*)
+datatype symb =
+ Terminal of Lexicon.token
+| Nonterminal of nt_tag * int; (*(tag, precedence)*)
+
+type nt_gram =
+ ((nt_tag list * Lexicon.token list) *
+ (Lexicon.token option * (symb list * string * int) list) list);
+ (*(([dependent_nts], [start_tokens]), [(start_token, [(rhs, name, prio)])])*)
+ (*depent_nts is a list of all NTs whose lookahead depends on this NT's lookahead*)
datatype gram =
- Gram of {nt_count: int, prod_count: int,
- tags: nt_tag Symtab.table,
- chains: (nt_tag * nt_tag list) list, (*[(to, [from])]*)
- lambdas: nt_tag list,
- prods: nt_gram Array.array};
- (*"tags" is used to map NT names (i.e. strings) to tags;
- chain productions are not stored as normal productions
- but instead as an entry in "chains";
- lambda productions are stored as normal productions
- and also as an entry in "lambdas"*)
+ Gram of
+ {nt_count: int,
+ prod_count: int,
+ tags: nt_tag Symtab.table,
+ chains: (nt_tag * nt_tag list) list, (*[(to, [from])]*)
+ lambdas: nt_tag list,
+ prods: nt_gram Vector.vector};
+ (*"tags" is used to map NT names (i.e. strings) to tags;
+ chain productions are not stored as normal productions
+ but instead as an entry in "chains";
+ lambda productions are stored as normal productions
+ and also as an entry in "lambdas"*)
-val UnknownStart = Lexicon.eof; (*productions for which no starting token is
- known yet are associated with this token*)
-(* get all NTs that are connected with a list of NTs
- (used for expanding chain list)*)
+(*productions for which no starting token is
+ known yet are associated with this token*)
+val unknown_start = Lexicon.eof;
+
+(*get all NTs that are connected with a list of NTs*)
fun connected_with _ ([]: nt_tag list) relatives = relatives
| connected_with chains (root :: roots) relatives =
- let val branches = subtract (op =) relatives (these (AList.lookup (op =) chains root));
- in connected_with chains (branches @ roots) (branches @ relatives) end;
-
-(* convert productions to grammar;
- N.B. that the chains parameter has the form [(from, [to])];
- prod_count is of type "int option" and is only updated if it is <> NONE*)
-fun add_prods _ chains lambdas prod_count [] = (chains, lambdas, prod_count)
- | add_prods prods chains lambdas prod_count
- ((lhs, new_prod as (rhs, name, pri)) :: ps) =
- let
- val chain_from = case (pri, rhs) of (~1, [Nonterminal (id, ~1)]) => SOME id | _ => NONE;
-
- (*store chain if it does not already exist*)
- val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from =>
- let val old_tos = these (AList.lookup (op =) chains from) in
- if member (op =) old_tos lhs then (NONE, chains)
- else (SOME from, AList.update (op =) (from, insert (op =) lhs old_tos) chains)
- end;
+ let val branches = subtract (op =) relatives (these (AList.lookup (op =) chains root));
+ in connected_with chains (branches @ roots) (branches @ relatives) end;
- (*propagate new chain in lookahead and lambda lists;
- added_starts is used later to associate existing
- productions with new starting tokens*)
- val (added_starts, lambdas') =
- if is_none new_chain then ([], lambdas) else
- let (*lookahead of chain's source*)
- val ((from_nts, from_tks), _) = Array.sub (prods, the new_chain);
-
- (*copy from's lookahead to chain's destinations*)
- fun copy_lookahead [] added = added
- | copy_lookahead (to :: tos) added =
- let
- val ((to_nts, to_tks), ps) = Array.sub (prods, to);
-
- val new_tks = subtract (op =) to_tks from_tks; (*added lookahead tokens*)
- in Array.update (prods, to, ((to_nts, to_tks @ new_tks), ps));
- copy_lookahead tos (if null new_tks then added
- else (to, new_tks) :: added)
- end;
-
- val tos = connected_with chains' [lhs] [lhs];
- in (copy_lookahead tos [],
- union (op =) (if member (op =) lambdas lhs then tos else []) lambdas)
- end;
-
- (*test if new production can produce lambda
- (rhs must either be empty or only consist of lambda NTs)*)
- val (new_lambda, lambdas') =
- if forall (fn (Nonterminal (id, _)) => member (op =) lambdas' id
- | (Terminal _) => false) rhs then
- (true, union (op =) lambdas' (connected_with chains' [lhs] [lhs]))
- else
- (false, lambdas');
+(*convert productions to grammar;
+ N.B. that the chains parameter has the form [(from, [to])];
+ prod_count is of type "int option" and is only updated if it is <> NONE*)
+fun add_prods _ chains lambdas prod_count [] = (chains, lambdas, prod_count)
+ | add_prods prods chains lambdas prod_count ((lhs, new_prod as (rhs, name, pri)) :: ps) =
+ let
+ val chain_from =
+ (case (pri, rhs) of
+ (~1, [Nonterminal (id, ~1)]) => SOME id
+ | _ => NONE);
- (*list optional terminal and all nonterminals on which the lookahead
- of a production depends*)
- fun lookahead_dependency _ [] nts = (NONE, nts)
- | lookahead_dependency _ ((Terminal tk) :: _) nts = (SOME tk, nts)
- | lookahead_dependency lambdas ((Nonterminal (nt, _)) :: symbs) nts =
- if member (op =) lambdas nt then
- lookahead_dependency lambdas symbs (nt :: nts)
- else (NONE, nt :: nts);
-
- (*get all known starting tokens for a nonterminal*)
- fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
-
- val token_union = uncurry (union Lexicon.matching_tokens);
+ (*store chain if it does not already exist*)
+ val (new_chain, chains') =
+ (case chain_from of
+ NONE => (NONE, chains)
+ | SOME from =>
+ let val old_tos = these (AList.lookup (op =) chains from) in
+ if member (op =) old_tos lhs then (NONE, chains)
+ else (SOME from, AList.update (op =) (from, insert (op =) lhs old_tos) chains)
+ end);
- (*update prods, lookaheads, and lambdas according to new lambda NTs*)
- val (added_starts', lambdas') =
- let
- (*propagate added lambda NT*)
- fun propagate_lambda [] added_starts lambdas= (added_starts, lambdas)
- | propagate_lambda (l :: ls) added_starts lambdas =
- let
- (*get lookahead for lambda NT*)
- val ((dependent, l_starts), _) = Array.sub (prods, l);
+ (*propagate new chain in lookahead and lambda lists;
+ added_starts is used later to associate existing
+ productions with new starting tokens*)
+ val (added_starts, lambdas') =
+ if is_none new_chain then ([], lambdas)
+ else
+ let (*lookahead of chain's source*)
+ val ((from_nts, from_tks), _) = Array.sub (prods, the new_chain);
- (*check productions whose lookahead may depend on lambda NT*)
- fun examine_prods [] add_lambda nt_dependencies added_tks
- nt_prods =
- (add_lambda, nt_dependencies, added_tks, nt_prods)
- | examine_prods ((p as (rhs, _, _)) :: ps) add_lambda
- nt_dependencies added_tks nt_prods =
- let val (tk, nts) = lookahead_dependency lambdas rhs [];
+ (*copy from's lookahead to chain's destinations*)
+ fun copy_lookahead [] added = added
+ | copy_lookahead (to :: tos) added =
+ let
+ val ((to_nts, to_tks), ps) = Array.sub (prods, to);
+
+ val new_tks = subtract (op =) to_tks from_tks; (*added lookahead tokens*)
+ val _ = Array.update (prods, to, ((to_nts, to_tks @ new_tks), ps));
in
- if member (op =) nts l then (*update production's lookahead*)
- let
- val new_lambda = is_none tk andalso subset (op =) (nts, lambdas);
-
- val new_tks = subtract (op =) l_starts
- ((if is_some tk then [the tk] else []) @
- Library.foldl token_union ([], map starts_for_nt nts));
-
- val added_tks' = token_union (new_tks, added_tks);
-
- val nt_dependencies' = union (op =) nts nt_dependencies;
-
- (*associate production with new starting tokens*)
- fun copy ([]: Lexicon.token option list) nt_prods = nt_prods
- | copy (tk :: tks) nt_prods =
- let val old_prods = these (AList.lookup (op =) nt_prods tk);
-
- val prods' = p :: old_prods;
- in nt_prods
- |> AList.update (op =) (tk, prods')
- |> copy tks
- end;
-
- val nt_prods' =
- let val new_opt_tks = map SOME new_tks;
- in copy ((if new_lambda then [NONE] else []) @
- new_opt_tks) nt_prods
- end;
- in examine_prods ps (add_lambda orelse new_lambda)
- nt_dependencies' added_tks' nt_prods'
- end
- else (*skip production*)
- examine_prods ps add_lambda nt_dependencies
- added_tks nt_prods
+ copy_lookahead tos (if null new_tks then added else (to, new_tks) :: added)
end;
- (*check each NT whose lookahead depends on new lambda NT*)
- fun process_nts [] added_lambdas added_starts =
- (added_lambdas, added_starts)
- | process_nts (nt :: nts) added_lambdas added_starts =
- let
- val (lookahead as (old_nts, old_tks), nt_prods) =
- Array.sub (prods, nt);
+ val tos = connected_with chains' [lhs] [lhs];
+ in
+ (copy_lookahead tos [],
+ union (op =) (if member (op =) lambdas lhs then tos else []) lambdas)
+ end;
- (*existing productions whose lookahead may depend on l*)
- val tk_prods =
- (these o AList.lookup (op =) nt_prods)
- (SOME (hd l_starts handle Empty => UnknownStart));
+ (*test if new production can produce lambda
+ (rhs must either be empty or only consist of lambda NTs)*)
+ val (new_lambda, lambdas') =
+ if forall
+ (fn Nonterminal (id, _) => member (op =) lambdas' id
+ | Terminal _ => false) rhs
+ then (true, union (op =) lambdas' (connected_with chains' [lhs] [lhs]))
+ else (false, lambdas');
- (*add_lambda is true if an existing production of the nt
- produces lambda due to the new lambda NT l*)
- val (add_lambda, nt_dependencies, added_tks, nt_prods') =
- examine_prods tk_prods false [] [] nt_prods;
+ (*list optional terminal and all nonterminals on which the lookahead
+ of a production depends*)
+ fun lookahead_dependency _ [] nts = (NONE, nts)
+ | lookahead_dependency _ ((Terminal tk) :: _) nts = (SOME tk, nts)
+ | lookahead_dependency lambdas ((Nonterminal (nt, _)) :: symbs) nts =
+ if member (op =) lambdas nt then
+ lookahead_dependency lambdas symbs (nt :: nts)
+ else (NONE, nt :: nts);
- val added_nts = subtract (op =) old_nts nt_dependencies;
+ (*get all known starting tokens for a nonterminal*)
+ fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
+
+ val token_union = uncurry (union Lexicon.matching_tokens);
- val added_lambdas' =
- if add_lambda then nt :: added_lambdas
- else added_lambdas;
- in Array.update (prods, nt,
- ((added_nts @ old_nts, old_tks @ added_tks),
- nt_prods'));
- (*N.B. that because the tks component
- is used to access existing
- productions we have to add new
- tokens at the _end_ of the list*)
+ (*update prods, lookaheads, and lambdas according to new lambda NTs*)
+ val (added_starts', lambdas') =
+ let
+ (*propagate added lambda NT*)
+ fun propagate_lambda [] added_starts lambdas= (added_starts, lambdas)
+ | propagate_lambda (l :: ls) added_starts lambdas =
+ let
+ (*get lookahead for lambda NT*)
+ val ((dependent, l_starts), _) = Array.sub (prods, l);
+
+ (*check productions whose lookahead may depend on lambda NT*)
+ fun examine_prods [] add_lambda nt_dependencies added_tks nt_prods =
+ (add_lambda, nt_dependencies, added_tks, nt_prods)
+ | examine_prods ((p as (rhs, _, _)) :: ps) add_lambda
+ nt_dependencies added_tks nt_prods =
+ let val (tk, nts) = lookahead_dependency lambdas rhs [] in
+ if member (op =) nts l then (*update production's lookahead*)
+ let
+ val new_lambda = is_none tk andalso subset (op =) (nts, lambdas);
- if null added_tks then
- process_nts nts added_lambdas' added_starts
- else
- process_nts nts added_lambdas'
- ((nt, added_tks) :: added_starts)
- end;
+ val new_tks = subtract (op =) l_starts
+ ((if is_some tk then [the tk] else []) @
+ Library.foldl token_union ([], map starts_for_nt nts));
+
+ val added_tks' = token_union (new_tks, added_tks);
+
+ val nt_dependencies' = union (op =) nts nt_dependencies;
- val (added_lambdas, added_starts') =
- process_nts dependent [] added_starts;
-
- val added_lambdas' = subtract (op =) lambdas added_lambdas;
- in propagate_lambda (ls @ added_lambdas') added_starts'
- (added_lambdas' @ lambdas)
- end;
- in propagate_lambda (subtract (op =) lambdas lambdas') added_starts lambdas' end;
+ (*associate production with new starting tokens*)
+ fun copy ([]: Lexicon.token option list) nt_prods = nt_prods
+ | copy (tk :: tks) nt_prods =
+ let
+ val old_prods = these (AList.lookup (op =) nt_prods tk);
+ val prods' = p :: old_prods;
+ in
+ nt_prods
+ |> AList.update (op =) (tk, prods')
+ |> copy tks
+ end;
- (*insert production into grammar*)
- val (added_starts', prod_count') =
- if is_some chain_from then (added_starts', prod_count) (*don't store chain production*)
- else let
- (*lookahead tokens of new production and on which
- NTs lookahead depends*)
- val (start_tk, start_nts) = lookahead_dependency lambdas' rhs [];
-
- val start_tks = Library.foldl token_union
- (if is_some start_tk then [the start_tk] else [],
- map starts_for_nt start_nts);
+ val nt_prods' =
+ let val new_opt_tks = map SOME new_tks in
+ copy
+ ((if new_lambda then [NONE] else []) @ new_opt_tks) nt_prods
+ end;
+ in
+ examine_prods ps (add_lambda orelse new_lambda)
+ nt_dependencies' added_tks' nt_prods'
+ end
+ else (*skip production*)
+ examine_prods ps add_lambda nt_dependencies added_tks nt_prods
+ end;
- val opt_starts = (if new_lambda then [NONE]
- else if null start_tks then [SOME UnknownStart]
- else []) @ (map SOME start_tks);
+ (*check each NT whose lookahead depends on new lambda NT*)
+ fun process_nts [] added_lambdas added_starts =
+ (added_lambdas, added_starts)
+ | process_nts (nt :: nts) added_lambdas added_starts =
+ let
+ val (lookahead as (old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
- (*add lhs NT to list of dependent NTs in lookahead*)
- fun add_nts [] = ()
- | add_nts (nt :: nts) =
- let val ((old_nts, old_tks), ps) = Array.sub (prods, nt);
- in if member (op =) old_nts lhs then ()
- else Array.update (prods, nt, ((lhs :: old_nts, old_tks), ps))
- end;
+ (*existing productions whose lookahead may depend on l*)
+ val tk_prods =
+ these
+ (AList.lookup (op =) nt_prods
+ (SOME (hd l_starts handle Empty => unknown_start)));
+
+ (*add_lambda is true if an existing production of the nt
+ produces lambda due to the new lambda NT l*)
+ val (add_lambda, nt_dependencies, added_tks, nt_prods') =
+ examine_prods tk_prods false [] [] nt_prods;
+
+ val added_nts = subtract (op =) old_nts nt_dependencies;
- (*add new start tokens to chained NTs' lookahead list;
- also store new production for lhs NT*)
- fun add_tks [] added prod_count = (added, prod_count)
- | add_tks (nt :: nts) added prod_count =
- let
- val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
-
- val new_tks = subtract Lexicon.matching_tokens old_tks start_tks;
+ val added_lambdas' =
+ if add_lambda then nt :: added_lambdas
+ else added_lambdas;
+ val _ =
+ Array.update
+ (prods, nt, ((added_nts @ old_nts, old_tks @ added_tks), nt_prods'));
+ (*N.B. that because the tks component
+ is used to access existing
+ productions we have to add new
+ tokens at the _end_ of the list*)
+ in
+ if null added_tks then
+ process_nts nts added_lambdas' added_starts
+ else
+ process_nts nts added_lambdas' ((nt, added_tks) :: added_starts)
+ end;
- (*store new production*)
- fun store [] prods is_new =
- (prods, if is_some prod_count andalso is_new then
- Option.map (fn x => x+1) prod_count
- else prod_count, is_new)
- | store (tk :: tks) prods is_new =
- let val tk_prods = (these o AList.lookup (op =) prods) tk;
+ val (added_lambdas, added_starts') = process_nts dependent [] added_starts;
+ val added_lambdas' = subtract (op =) lambdas added_lambdas;
+ in
+ propagate_lambda (ls @ added_lambdas') added_starts' (added_lambdas' @ lambdas)
+ end;
+ in propagate_lambda (subtract (op =) lambdas lambdas') added_starts lambdas' end;
- (*if prod_count = NONE then we can assume that
- grammar does not contain new production already*)
- val (tk_prods', is_new') =
- if is_some prod_count then
- if member (op =) tk_prods new_prod then (tk_prods, false)
- else (new_prod :: tk_prods, true)
- else (new_prod :: tk_prods, true);
+ (*insert production into grammar*)
+ val (added_starts', prod_count') =
+ if is_some chain_from
+ then (added_starts', prod_count) (*don't store chain production*)
+ else
+ let
+ (*lookahead tokens of new production and on which
+ NTs lookahead depends*)
+ val (start_tk, start_nts) = lookahead_dependency lambdas' rhs [];
- val prods' = prods
- |> is_new' ? AList.update (op =) (tk: Lexicon.token option, tk_prods');
- in store tks prods' (is_new orelse is_new') end;
+ val start_tks =
+ Library.foldl token_union
+ (if is_some start_tk then [the start_tk] else [],
+ map starts_for_nt start_nts);
- val (nt_prods', prod_count', changed) =
- if nt = lhs then store opt_starts nt_prods false
- else (nt_prods, prod_count, false);
- in if not changed andalso null new_tks then ()
- else Array.update (prods, nt, ((old_nts, old_tks @ new_tks),
- nt_prods'));
- add_tks nts (if null new_tks then added
- else (nt, new_tks) :: added) prod_count'
- end;
- in add_nts start_nts;
- add_tks (connected_with chains' [lhs] [lhs]) [] prod_count
- end;
+ val opt_starts =
+ (if new_lambda then [NONE]
+ else if null start_tks then [SOME unknown_start]
+ else []) @ map SOME start_tks;
+
+ (*add lhs NT to list of dependent NTs in lookahead*)
+ fun add_nts [] = ()
+ | add_nts (nt :: nts) =
+ let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in
+ if member (op =) old_nts lhs then ()
+ else Array.update (prods, nt, ((lhs :: old_nts, old_tks), ps))
+ end;
+
+ (*add new start tokens to chained NTs' lookahead list;
+ also store new production for lhs NT*)
+ fun add_tks [] added prod_count = (added, prod_count)
+ | add_tks (nt :: nts) added prod_count =
+ let
+ val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
+
+ val new_tks = subtract Lexicon.matching_tokens old_tks start_tks;
+
+ (*store new production*)
+ fun store [] prods is_new =
+ (prods,
+ if is_some prod_count andalso is_new then
+ Option.map (fn x => x + 1) prod_count
+ else prod_count, is_new)
+ | store (tk :: tks) prods is_new =
+ let
+ val tk_prods = these (AList.lookup (op =) prods tk);
+
+ (*if prod_count = NONE then we can assume that
+ grammar does not contain new production already*)
+ val (tk_prods', is_new') =
+ if is_some prod_count then
+ if member (op =) tk_prods new_prod then (tk_prods, false)
+ else (new_prod :: tk_prods, true)
+ else (new_prod :: tk_prods, true);
- (*associate productions with new lookaheads*)
- val dummy =
- let
- (*propagate added start tokens*)
- fun add_starts [] = ()
- | add_starts ((changed_nt, new_tks) :: starts) =
- let
- (*token under which old productions which
- depend on changed_nt could be stored*)
- val key =
- case find_first (not o member (op =) new_tks)
- (starts_for_nt changed_nt) of
- NONE => SOME UnknownStart
- | t => t;
+ val prods' = prods
+ |> is_new' ? AList.update (op =) (tk: Lexicon.token option, tk_prods');
+ in store tks prods' (is_new orelse is_new') end;
+
+ val (nt_prods', prod_count', changed) =
+ if nt = lhs
+ then store opt_starts nt_prods false
+ else (nt_prods, prod_count, false);
+ val _ =
+ if not changed andalso null new_tks then ()
+ else Array.update (prods, nt, ((old_nts, old_tks @ new_tks), nt_prods'));
+ in
+ add_tks nts
+ (if null new_tks then added else (nt, new_tks) :: added) prod_count'
+ end;
+ val _ = add_nts start_nts;
+ in
+ add_tks (connected_with chains' [lhs] [lhs]) [] prod_count
+ end;
- (*copy productions whose lookahead depends on changed_nt;
- if key = SOME UnknownToken then tk_prods is used to hold
- the productions not copied*)
- fun update_prods [] result = result
- | update_prods ((p as (rhs, _: string, _: nt_tag)) :: ps)
- (tk_prods, nt_prods) =
- let
- (*lookahead dependency for production*)
- val (tk, depends) = lookahead_dependency lambdas' rhs [];
+ (*associate productions with new lookaheads*)
+ val _ =
+ let
+ (*propagate added start tokens*)
+ fun add_starts [] = ()
+ | add_starts ((changed_nt, new_tks) :: starts) =
+ let
+ (*token under which old productions which
+ depend on changed_nt could be stored*)
+ val key =
+ (case find_first (not o member (op =) new_tks) (starts_for_nt changed_nt) of
+ NONE => SOME unknown_start
+ | t => t);
- (*test if this production has to be copied*)
- val update = member (op =) depends changed_nt;
-
- (*test if production could already be associated with
- a member of new_tks*)
- val lambda = length depends > 1 orelse
- not (null depends) andalso is_some tk
- andalso member (op =) new_tks (the tk);
-
- (*associate production with new starting tokens*)
- fun copy ([]: Lexicon.token list) nt_prods = nt_prods
- | copy (tk :: tks) nt_prods =
+ (*copy productions whose lookahead depends on changed_nt;
+ if key = SOME unknown_start then tk_prods is used to hold
+ the productions not copied*)
+ fun update_prods [] result = result
+ | update_prods ((p as (rhs, _: string, _: nt_tag)) :: ps)
+ (tk_prods, nt_prods) =
let
- val tk_prods = these (AList.lookup (op =) nt_prods (SOME tk));
+ (*lookahead dependency for production*)
+ val (tk, depends) = lookahead_dependency lambdas' rhs [];
+
+ (*test if this production has to be copied*)
+ val update = member (op =) depends changed_nt;
- val tk_prods' =
- if not lambda then p :: tk_prods
- else insert (op =) p tk_prods;
- (*if production depends on lambda NT we
- have to look for duplicates*)
- in
- nt_prods
- |> AList.update (op =) (SOME tk, tk_prods')
- |> copy tks
- end;
- val result =
- if update then
- (tk_prods, copy new_tks nt_prods)
- else if key = SOME UnknownStart then
- (p :: tk_prods, nt_prods)
- else (tk_prods, nt_prods);
- in update_prods ps result end;
+ (*test if production could already be associated with
+ a member of new_tks*)
+ val lambda =
+ length depends > 1 orelse
+ not (null depends) andalso is_some tk
+ andalso member (op =) new_tks (the tk);
+
+ (*associate production with new starting tokens*)
+ fun copy ([]: Lexicon.token list) nt_prods = nt_prods
+ | copy (tk :: tks) nt_prods =
+ let
+ val tk_prods = these (AList.lookup (op =) nt_prods (SOME tk));
- (*copy existing productions for new starting tokens*)
- fun process_nts [] added = added
- | process_nts (nt :: nts) added =
- let
- val (lookahead as (old_nts, old_tks), nt_prods) =
- Array.sub (prods, nt);
+ val tk_prods' =
+ if not lambda then p :: tk_prods
+ else insert (op =) p tk_prods;
+ (*if production depends on lambda NT we
+ have to look for duplicates*)
+ in
+ nt_prods
+ |> AList.update (op =) (SOME tk, tk_prods')
+ |> copy tks
+ end;
+ val result =
+ if update then (tk_prods, copy new_tks nt_prods)
+ else if key = SOME unknown_start then (p :: tk_prods, nt_prods)
+ else (tk_prods, nt_prods);
+ in update_prods ps result end;
- val tk_prods = these (AList.lookup (op =) nt_prods key);
-
- (*associate productions with new lookahead tokens*)
- val (tk_prods', nt_prods') =
- update_prods tk_prods ([], nt_prods);
+ (*copy existing productions for new starting tokens*)
+ fun process_nts [] added = added
+ | process_nts (nt :: nts) added =
+ let
+ val (lookahead as (old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
- val nt_prods' =
- nt_prods'
- |> (key = SOME UnknownStart) ? AList.update (op =) (key, tk_prods')
+ val tk_prods = these (AList.lookup (op =) nt_prods key);
+
+ (*associate productions with new lookahead tokens*)
+ val (tk_prods', nt_prods') = update_prods tk_prods ([], nt_prods);
+
+ val nt_prods' =
+ nt_prods'
+ |> (key = SOME unknown_start) ? AList.update (op =) (key, tk_prods');
- val added_tks =
- subtract Lexicon.matching_tokens old_tks new_tks;
- in if null added_tks then
- (Array.update (prods, nt, (lookahead, nt_prods'));
- process_nts nts added)
- else
- (Array.update (prods, nt,
- ((old_nts, added_tks @ old_tks), nt_prods'));
- process_nts nts ((nt, added_tks) :: added))
- end;
+ val added_tks = subtract Lexicon.matching_tokens old_tks new_tks;
+ in
+ if null added_tks then
+ (Array.update (prods, nt, (lookahead, nt_prods'));
+ process_nts nts added)
+ else
+ (Array.update (prods, nt, ((old_nts, added_tks @ old_tks), nt_prods'));
+ process_nts nts ((nt, added_tks) :: added))
+ end;
- val ((dependent, _), _) = Array.sub (prods, changed_nt);
- in add_starts (starts @ process_nts dependent []) end;
- in add_starts added_starts' end;
- in add_prods prods chains' lambdas' prod_count ps end;
+ val ((dependent, _), _) = Array.sub (prods, changed_nt);
+ in add_starts (starts @ process_nts dependent []) end;
+ in add_starts added_starts' end;
+ in add_prods prods chains' lambdas' prod_count ps end;
(* pretty_gram *)
@@ -410,8 +421,8 @@
fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
val nt_prods =
- Library.foldl (uncurry (union (op =))) ([], map snd (snd (Array.sub (prods, tag)))) @
- map prod_of_chain ((these o AList.lookup (op =) chains) tag);
+ Library.foldl (uncurry (union (op =))) ([], map snd (snd (Vector.sub (prods, tag)))) @
+ map prod_of_chain (these (AList.lookup (op =) chains tag));
in map (pretty_prod name) nt_prods end;
in maps pretty_nt (sort_wrt fst (Symtab.dest tags)) end;
@@ -419,85 +430,96 @@
(** Operations on gramars **)
-val empty_gram = Gram {nt_count = 0, prod_count = 0,
- tags = Symtab.empty, chains = [], lambdas = [],
- prods = Array.array (0, (([], []), []))};
+val empty_gram =
+ Gram
+ {nt_count = 0,
+ prod_count = 0,
+ tags = Symtab.empty, chains = [],
+ lambdas = [],
+ prods = Vector.fromList [(([], []), [])]};
(*Invert list of chain productions*)
fun inverse_chains [] result = result
| inverse_chains ((root, branches: nt_tag list) :: cs) result =
- let fun add ([]: nt_tag list) result = result
+ let
+ fun add ([]: nt_tag list) result = result
| add (id :: ids) result =
- let val old = (these o AList.lookup (op =) result) id;
- in add ids (AList.update (op =) (id, root :: old) result) end;
- in inverse_chains cs (add branches result) end;
+ let val old = these (AList.lookup (op =) result id);
+ in add ids (AList.update (op =) (id, root :: old) result) end;
+ in inverse_chains cs (add branches result) end;
(*Add productions to a grammar*)
fun extend_gram [] gram = gram
| extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) =
- let
- (*Get tag for existing nonterminal or create a new one*)
- fun get_tag nt_count tags nt =
- case Symtab.lookup tags nt of
- SOME tag => (nt_count, tags, tag)
- | NONE => (nt_count+1, Symtab.update_new (nt, nt_count) tags,
- nt_count);
+ let
+ (*Get tag for existing nonterminal or create a new one*)
+ fun get_tag nt_count tags nt =
+ (case Symtab.lookup tags nt of
+ SOME tag => (nt_count, tags, tag)
+ | NONE => (nt_count + 1, Symtab.update_new (nt, nt_count) tags, nt_count));
- (*Convert symbols to the form used by the parser;
- delimiters and predefined terms are stored as terminals,
- nonterminals are converted to integer tags*)
- fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
- | symb_of ((Syn_Ext.Delim s) :: ss) nt_count tags result =
- symb_of ss nt_count tags
- (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result)
- | symb_of ((Syn_Ext.Argument (s, p)) :: ss) nt_count tags result =
- let
- val (nt_count', tags', new_symb) =
- case Lexicon.predef_term s of
- NONE =>
- let val (nt_count', tags', s_tag) = get_tag nt_count tags s;
- in (nt_count', tags', Nonterminal (s_tag, p)) end
- | SOME tk => (nt_count, tags, Terminal tk);
- in symb_of ss nt_count' tags' (new_symb :: result) end
- | symb_of (_ :: ss) nt_count tags result =
- symb_of ss nt_count tags result;
+ (*Convert symbols to the form used by the parser;
+ delimiters and predefined terms are stored as terminals,
+ nonterminals are converted to integer tags*)
+ fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
+ | symb_of ((Syn_Ext.Delim s) :: ss) nt_count tags result =
+ symb_of ss nt_count tags
+ (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result)
+ | symb_of ((Syn_Ext.Argument (s, p)) :: ss) nt_count tags result =
+ let
+ val (nt_count', tags', new_symb) =
+ (case Lexicon.predef_term s of
+ NONE =>
+ let val (nt_count', tags', s_tag) = get_tag nt_count tags s;
+ in (nt_count', tags', Nonterminal (s_tag, p)) end
+ | SOME tk => (nt_count, tags, Terminal tk));
+ in symb_of ss nt_count' tags' (new_symb :: result) end
+ | symb_of (_ :: ss) nt_count tags result = symb_of ss nt_count tags result;
- (*Convert list of productions by invoking symb_of for each of them*)
- fun prod_of [] nt_count prod_count tags result =
- (nt_count, prod_count, tags, result)
- | prod_of ((Syn_Ext.XProd (lhs, xsymbs, const, pri)) :: ps)
- nt_count prod_count tags result =
- let val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;
+ (*Convert list of productions by invoking symb_of for each of them*)
+ fun prod_of [] nt_count prod_count tags result =
+ (nt_count, prod_count, tags, result)
+ | prod_of ((Syn_Ext.XProd (lhs, xsymbs, const, pri)) :: ps)
+ nt_count prod_count tags result =
+ let
+ val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;
+ val (nt_count'', tags'', prods) = symb_of xsymbs nt_count' tags' [];
+ in
+ prod_of ps nt_count'' (prod_count + 1) tags''
+ ((lhs_tag, (prods, const, pri)) :: result)
+ end;
- val (nt_count'', tags'', prods) =
- symb_of xsymbs nt_count' tags' [];
- in prod_of ps nt_count'' (prod_count+1) tags''
- ((lhs_tag, (prods, const, pri)) :: result)
- end;
-
- val (nt_count', prod_count', tags', xprods') =
- prod_of xprods nt_count prod_count tags [];
+ val (nt_count', prod_count', tags', xprods') =
+ prod_of xprods nt_count prod_count tags [];
- (*Copy array containing productions of old grammar;
- this has to be done to preserve the old grammar while being able
- to change the array's content*)
- val prods' =
- let fun get_prod i = if i < nt_count then Array.sub (prods, i)
- else (([], []), []);
- in Array.tabulate (nt_count', get_prod) end;
+ (*Copy array containing productions of old grammar;
+ this has to be done to preserve the old grammar while being able
+ to change the array's content*)
+ val prods' =
+ let
+ fun get_prod i =
+ if i < nt_count then Vector.sub (prods, i)
+ else (([], []), []);
+ in Array.tabulate (nt_count', get_prod) end;
+
+ val fromto_chains = inverse_chains chains [];
- val fromto_chains = inverse_chains chains [];
+ (*Add new productions to old ones*)
+ val (fromto_chains', lambdas', _) =
+ add_prods prods' fromto_chains lambdas NONE xprods';
- (*Add new productions to old ones*)
- val (fromto_chains', lambdas', _) =
- add_prods prods' fromto_chains lambdas NONE xprods';
-
- val chains' = inverse_chains fromto_chains' [];
- in Gram {nt_count = nt_count', prod_count = prod_count', tags = tags',
- chains = chains', lambdas = lambdas', prods = prods'}
- end;
+ val chains' = inverse_chains fromto_chains' [];
+ in
+ Gram
+ {nt_count = nt_count',
+ prod_count = prod_count',
+ tags = tags',
+ chains = chains',
+ lambdas = lambdas',
+ prods = Array.vector prods'}
+ end;
fun make_gram xprods = extend_gram xprods empty_gram;
@@ -506,37 +528,40 @@
fun merge_gram (gram_a, gram_b) =
let
(*find out which grammar is bigger*)
- val (Gram {nt_count = nt_count1, prod_count = prod_count1, tags = tags1,
- chains = chains1, lambdas = lambdas1, prods = prods1},
- Gram {nt_count = nt_count2, prod_count = prod_count2, tags = tags2,
- chains = chains2, lambdas = lambdas2, prods = prods2}) =
- let val Gram {prod_count = count_a, ...} = gram_a;
- val Gram {prod_count = count_b, ...} = gram_b;
- in if count_a > count_b then (gram_a, gram_b)
- else (gram_b, gram_a)
+ val
+ (Gram {nt_count = nt_count1, prod_count = prod_count1, tags = tags1,
+ chains = chains1, lambdas = lambdas1, prods = prods1},
+ Gram {nt_count = nt_count2, prod_count = prod_count2, tags = tags2,
+ chains = chains2, lambdas = lambdas2, prods = prods2}) =
+ let
+ val Gram {prod_count = count_a, ...} = gram_a;
+ val Gram {prod_count = count_b, ...} = gram_b;
+ in
+ if count_a > count_b
+ then (gram_a, gram_b)
+ else (gram_b, gram_a)
end;
(*get existing tag from grammar1 or create a new one*)
fun get_tag nt_count tags nt =
- case Symtab.lookup tags nt of
+ (case Symtab.lookup tags nt of
SOME tag => (nt_count, tags, tag)
- | NONE => (nt_count+1, Symtab.update_new (nt, nt_count) tags,
- nt_count)
+ | NONE => (nt_count + 1, Symtab.update_new (nt, nt_count) tags, nt_count));
val ((nt_count1', tags1'), tag_table) =
- let val tag_list = Symtab.dest tags2;
+ let
+ val tag_list = Symtab.dest tags2;
- val table = Array.array (nt_count2, ~1);
+ val table = Array.array (nt_count2, ~1);
- fun store_tag nt_count tags ~1 = (nt_count, tags)
- | store_tag nt_count tags tag =
- let val (nt_count', tags', tag') =
- get_tag nt_count tags
- (fst (the (find_first (fn (n, t) => t = tag) tag_list)));
- in Array.update (table, tag, tag');
- store_tag nt_count' tags' (tag-1)
- end;
- in (store_tag nt_count1 tags1 (nt_count2-1), table) end;
+ fun store_tag nt_count tags ~1 = (nt_count, tags)
+ | store_tag nt_count tags tag =
+ let
+ val (nt_count', tags', tag') =
+ get_tag nt_count tags (fst (the (find_first (fn (n, t) => t = tag) tag_list)));
+ val _ = Array.update (table, tag, tag');
+ in store_tag nt_count' tags' (tag - 1) end;
+ in (store_tag nt_count1 tags1 (nt_count2 - 1), table) end;
(*convert grammar2 tag to grammar1 tag*)
fun convert_tag tag = Array.sub (tag_table, tag);
@@ -544,44 +569,44 @@
(*convert chain list to raw productions*)
fun mk_chain_prods [] result = result
| mk_chain_prods ((to, froms) :: cs) result =
- let
- val to_tag = convert_tag to;
+ let
+ val to_tag = convert_tag to;
- fun make [] result = result
- | make (from :: froms) result = make froms ((to_tag,
- ([Nonterminal (convert_tag from, ~1)], "", ~1)) :: result);
- in mk_chain_prods cs (make froms [] @ result) end;
+ fun make [] result = result
+ | make (from :: froms) result = make froms
+ ((to_tag, ([Nonterminal (convert_tag from, ~1)], "", ~1)) :: result);
+ in mk_chain_prods cs (make froms [] @ result) end;
val chain_prods = mk_chain_prods chains2 [];
(*convert prods2 array to productions*)
fun process_nt ~1 result = result
| process_nt nt result =
- let
- val nt_prods = Library.foldl (uncurry (union (op =)))
- ([], map snd (snd (Array.sub (prods2, nt))));
- val lhs_tag = convert_tag nt;
+ let
+ val nt_prods = Library.foldl (uncurry (union (op =)))
+ ([], map snd (snd (Vector.sub (prods2, nt))));
+ val lhs_tag = convert_tag nt;
- (*convert tags in rhs*)
- fun process_rhs [] result = result
- | process_rhs (Terminal tk :: rhs) result =
- process_rhs rhs (result @ [Terminal tk])
- | process_rhs (Nonterminal (nt, prec) :: rhs) result =
- process_rhs rhs
- (result @ [Nonterminal (convert_tag nt, prec)]);
+ (*convert tags in rhs*)
+ fun process_rhs [] result = result
+ | process_rhs (Terminal tk :: rhs) result =
+ process_rhs rhs (result @ [Terminal tk])
+ | process_rhs (Nonterminal (nt, prec) :: rhs) result =
+ process_rhs rhs (result @ [Nonterminal (convert_tag nt, prec)]);
- (*convert tags in productions*)
- fun process_prods [] result = result
- | process_prods ((rhs, id, prec) :: ps) result =
- process_prods ps ((lhs_tag, (process_rhs rhs [], id, prec))
- :: result);
- in process_nt (nt-1) (process_prods nt_prods [] @ result) end;
+ (*convert tags in productions*)
+ fun process_prods [] result = result
+ | process_prods ((rhs, id, prec) :: ps) result =
+ process_prods ps ((lhs_tag, (process_rhs rhs [], id, prec)) :: result);
+ in process_nt (nt - 1) (process_prods nt_prods [] @ result) end;
- val raw_prods = chain_prods @ process_nt (nt_count2-1) [];
+ val raw_prods = chain_prods @ process_nt (nt_count2 - 1) [];
val prods1' =
- let fun get_prod i = if i < nt_count1 then Array.sub (prods1, i)
- else (([], []), []);
+ let
+ fun get_prod i =
+ if i < nt_count1 then Vector.sub (prods1, i)
+ else (([], []), []);
in Array.tabulate (nt_count1', get_prod) end;
val fromto_chains = inverse_chains chains1 [];
@@ -590,9 +615,14 @@
add_prods prods1' fromto_chains lambdas1 (SOME prod_count1) raw_prods;
val chains' = inverse_chains fromto_chains' [];
- in Gram {nt_count = nt_count1', prod_count = prod_count1',
- tags = tags1', chains = chains', lambdas = lambdas',
- prods = prods1'}
+ in
+ Gram
+ {nt_count = nt_count1',
+ prod_count = prod_count1',
+ tags = tags1',
+ chains = chains',
+ lambdas = lambdas',
+ prods = Array.vector prods1'}
end;
@@ -603,32 +633,33 @@
Tip of Lexicon.token;
type state =
- nt_tag * int * (*identification and production precedence*)
- parsetree list * (*already parsed nonterminals on rhs*)
- symb list * (*rest of rhs*)
- string * (*name of production*)
- int; (*index for previous state list*)
+ nt_tag * int * (*identification and production precedence*)
+ parsetree list * (*already parsed nonterminals on rhs*)
+ symb list * (*rest of rhs*)
+ string * (*name of production*)
+ int; (*index for previous state list*)
-(*Get all rhss with precedence >= minPrec*)
-fun getRHS minPrec = filter (fn (_, _, prec:int) => prec >= minPrec);
+(*Get all rhss with precedence >= min_prec*)
+fun get_RHS min_prec = filter (fn (_, _, prec:int) => prec >= min_prec);
-(*Get all rhss with precedence >= minPrec and < maxPrec*)
-fun getRHS' minPrec maxPrec =
- filter (fn (_, _, prec:int) => prec >= minPrec andalso prec < maxPrec);
+(*Get all rhss with precedence >= min_prec and < max_prec*)
+fun get_RHS' min_prec max_prec =
+ filter (fn (_, _, prec:int) => prec >= min_prec andalso prec < max_prec);
(*Make states using a list of rhss*)
-fun mkStates i minPrec lhsID rhss =
- let fun mkState (rhs, id, prodPrec) = (lhsID, prodPrec, [], rhs, id, i);
- in map mkState rhss end;
+fun mk_states i min_prec lhs_ID rhss =
+ let fun mk_state (rhs, id, prod_prec) = (lhs_ID, prod_prec, [], rhs, id, i);
+ in map mk_state rhss end;
(*Add parse tree to list and eliminate duplicates
saving the maximum precedence*)
fun conc (t: parsetree list, prec:int) [] = (NONE, [(t, prec)])
| conc (t, prec) ((t', prec') :: ts) =
if t = t' then
- (SOME prec', if prec' >= prec then (t', prec') :: ts
- else (t, prec) :: ts)
+ (SOME prec',
+ if prec' >= prec then (t', prec') :: ts
+ else (t, prec) :: ts)
else
let val (n, ts') = conc (t, prec) ts
in (n, (t', prec') :: ts') end;
@@ -644,35 +675,33 @@
(*Replace entry in used*)
fun update_prec (A: nt_tag, prec) used =
- let fun update ((hd as (B, (_, ts))) :: used, used') =
- if A = B
- then used' @ ((A, (prec, ts)) :: used)
- else update (used, hd :: used')
+ let
+ fun update ((hd as (B, (_, ts))) :: used, used') =
+ if A = B
+ then used' @ ((A, (prec, ts)) :: used)
+ else update (used, hd :: used')
in update (used, []) end;
-fun getS A maxPrec Si =
+fun getS A max_prec Si =
+ filter
+ (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec
+ | _ => false) Si;
+
+fun getS' A max_prec min_prec Si =
filter
(fn (_, _, _, Nonterminal (B, prec) :: _, _, _)
- => A = B andalso prec <= maxPrec
+ => A = B andalso prec > min_prec andalso prec <= max_prec
| _ => false) Si;
-fun getS' A maxPrec minPrec Si =
+fun get_states Estate i ii A max_prec =
filter
- (fn (_, _, _, Nonterminal (B, prec) :: _, _, _)
- => A = B andalso prec > minPrec andalso prec <= maxPrec
- | _ => false) Si;
-
-fun getStates Estate i ii A maxPrec =
- filter
- (fn (_, _, _, Nonterminal (B, prec) :: _, _, _)
- => A = B andalso prec <= maxPrec
+ (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec
| _ => false)
(Array.sub (Estate, ii));
fun movedot_term (A, j, ts, Terminal a :: sa, id, i) c =
- if Lexicon.valued_token c then
- (A, j, ts @ [Tip c], sa, id, i)
+ if Lexicon.valued_token c then (A, j, ts @ [Tip c], sa, id, i)
else (A, j, ts, sa, id, i);
fun movedot_nonterm ts (A, j, tss, Nonterminal _ :: sa, id, i) =
@@ -692,18 +721,19 @@
be started by specified token*)
fun prods_for prods chains include_none tk nts =
let
- fun token_assoc (list, key) =
- let fun assoc [] result = result
- | assoc ((keyi, pi) :: pairs) result =
- if is_some keyi andalso Lexicon.matching_tokens (the keyi, key)
- orelse include_none andalso is_none keyi then
- assoc pairs (pi @ result)
- else assoc pairs result;
- in assoc list [] end;
+ fun token_assoc (list, key) =
+ let
+ fun assoc [] result = result
+ | assoc ((keyi, pi) :: pairs) result =
+ if is_some keyi andalso Lexicon.matching_tokens (the keyi, key)
+ orelse include_none andalso is_none keyi then
+ assoc pairs (pi @ result)
+ else assoc pairs result;
+ in assoc list [] end;
- fun get_prods [] result = result
- | get_prods (nt :: nts) result =
- let val nt_prods = snd (Array.sub (prods, nt));
+ fun get_prods [] result = result
+ | get_prods (nt :: nts) result =
+ let val nt_prods = snd (Vector.sub (prods, nt));
in get_prods nts ((token_assoc (nt_prods, tk)) @ result) end;
in get_prods (connected_with chains nts nts) [] end;
@@ -715,66 +745,66 @@
fun processS used [] (Si, Sii) = (Si, Sii)
| processS used (S :: States) (Si, Sii) =
(case S of
- (_, _, _, Nonterminal (nt, minPrec) :: _, _, _) =>
- let (*predictor operation*)
+ (_, _, _, Nonterminal (nt, min_prec) :: _, _, _) =>
+ let (*predictor operation*)
val (used', new_states) =
(case AList.lookup (op =) used nt of
- SOME (usedPrec, l) => (*nonterminal has been processed*)
- if usedPrec <= minPrec then
- (*wanted precedence has been processed*)
+ SOME (used_prec, l) => (*nonterminal has been processed*)
+ if used_prec <= min_prec then
+ (*wanted precedence has been processed*)
(used, movedot_lambda S l)
- else (*wanted precedence hasn't been parsed yet*)
+ else (*wanted precedence hasn't been parsed yet*)
let
val tk_prods = all_prods_for nt;
- val States' = mkStates i minPrec nt
- (getRHS' minPrec usedPrec tk_prods);
- in (update_prec (nt, minPrec) used,
+ val States' = mk_states i min_prec nt
+ (get_RHS' min_prec used_prec tk_prods);
+ in (update_prec (nt, min_prec) used,
movedot_lambda S l @ States')
end
- | NONE => (*nonterminal is parsed for the first time*)
- let val tk_prods = all_prods_for nt;
- val States' = mkStates i minPrec nt
- (getRHS minPrec tk_prods);
- in ((nt, (minPrec, [])) :: used, States') end);
+ | NONE => (*nonterminal is parsed for the first time*)
+ let
+ val tk_prods = all_prods_for nt;
+ val States' = mk_states i min_prec nt (get_RHS min_prec tk_prods);
+ in ((nt, (min_prec, [])) :: used, States') end);
val dummy =
- if not (!warned) andalso
- length (new_states @ States) > (!branching_level) then
+ if not (! warned) andalso
+ length (new_states @ States) > ! branching_level then
(warning "Currently parsed expression could be extremely ambiguous.";
warned := true)
else ();
in
processS used' (new_states @ States) (S :: Si, Sii)
end
- | (_, _, _, Terminal a :: _, _, _) => (*scanner operation*)
+ | (_, _, _, Terminal a :: _, _, _) => (*scanner operation*)
processS used States
(S :: Si,
if Lexicon.matching_tokens (a, c) then movedot_term S c :: Sii else Sii)
- | (A, prec, ts, [], id, j) => (*completer operation*)
+ | (A, prec, ts, [], id, j) => (*completer operation*)
let val tt = if id = "" then ts else [Node (id, ts)] in
- if j = i then (*lambda production?*)
+ if j = i then (*lambda production?*)
let
val (used', O) = update_trees used (A, (tt, prec));
in
- case O of
+ (case O of
NONE =>
- let val Slist = getS A prec Si;
- val States' = map (movedot_nonterm tt) Slist;
+ let
+ val Slist = getS A prec Si;
+ val States' = map (movedot_nonterm tt) Slist;
in processS used' (States' @ States) (S :: Si, Sii) end
| SOME n =>
if n >= prec then processS used' States (S :: Si, Sii)
else
- let val Slist = getS' A prec n Si;
- val States' = map (movedot_nonterm tt) Slist;
- in processS used' (States' @ States) (S :: Si, Sii) end
+ let
+ val Slist = getS' A prec n Si;
+ val States' = map (movedot_nonterm tt) Slist;
+ in processS used' (States' @ States) (S :: Si, Sii) end)
end
else
- let val Slist = getStates Estate i j A prec
- in processS used (map (movedot_nonterm tt) Slist @ States)
- (S :: Si, Sii)
- end
+ let val Slist = get_states Estate i j A prec
+ in processS used (map (movedot_nonterm tt) Slist @ States) (S :: Si, Sii) end
end)
in processS [] states ([], []) end;
@@ -793,14 +823,14 @@
[Pretty.str "\""])))
end
| s =>
- (case indata of
- [] => Array.sub (stateset, i)
- | c :: cs =>
- let val (si, sii) = PROCESSS warned prods chains stateset i c s;
- in Array.update (stateset, i, si);
- Array.update (stateset, i + 1, sii);
- produce warned prods tags chains stateset (i + 1) cs c
- end));
+ (case indata of
+ [] => Array.sub (stateset, i)
+ | c :: cs =>
+ let val (si, sii) = PROCESSS warned prods chains stateset i c s;
+ in Array.update (stateset, i, si);
+ Array.update (stateset, i + 1, sii);
+ produce warned prods tags chains stateset (i + 1) cs c
+ end));
fun get_trees l = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) l;
@@ -814,8 +844,8 @@
val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)];
val s = length indata + 1;
val Estate = Array.array (s, []);
+ val _ = Array.update (Estate, 0, S0);
in
- Array.update (Estate, 0, S0);
get_trees (produce (Unsynchronized.ref false) prods tags chains Estate 0 indata Lexicon.eof)
end;
@@ -835,7 +865,7 @@
fun guess_infix_lr (Gram gram) c = (*based on educated guess*)
let
- fun freeze a = map_range (curry Array.sub a) (Array.length a);
+ fun freeze a = map_range (curry Vector.sub a) (Vector.length a);
val prods = maps snd (maps snd (freeze (#prods gram)));
fun guess (SOME ([Nonterminal (_, k),
Terminal (Lexicon.Token (Lexicon.Literal, s, _)), Nonterminal (_, l)], _, j)) =
--- a/src/Pure/drule.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Pure/drule.ML Thu Aug 26 09:03:18 2010 +0200
@@ -277,7 +277,7 @@
(*Squash a theorem's flexflex constraints provided it can be done uniquely.
This step can lose information.*)
fun flexflex_unique th =
- if null (tpairs_of th) then th else
+ if null (Thm.tpairs_of th) then th else
case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule th)) of
[th] => th
| [] => raise THM("flexflex_unique: impossible constraints", 0, [th])
--- a/src/Pure/meta_simplifier.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Pure/meta_simplifier.ML Thu Aug 26 09:03:18 2010 +0200
@@ -107,9 +107,9 @@
val simp_depth_limit_value: Config.value Config.T
val simp_depth_limit: int Config.T
val clear_ss: simpset -> simpset
- val simproc_i: theory -> string -> term list
+ val simproc_global_i: theory -> string -> term list
-> (theory -> simpset -> term -> thm option) -> simproc
- val simproc: theory -> string -> string list
+ val simproc_global: theory -> string -> string list
-> (theory -> simpset -> term -> thm option) -> simproc
val inherit_context: simpset -> simpset -> simpset
val the_context: simpset -> Proof.context
@@ -631,8 +631,8 @@
proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
(* FIXME avoid global thy and Logic.varify_global *)
-fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
-fun simproc thy name = simproc_i thy name o map (Syntax.read_term_global thy);
+fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
+fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy);
local
--- a/src/Pure/simplifier.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Pure/simplifier.ML Thu Aug 26 09:03:18 2010 +0200
@@ -38,9 +38,9 @@
val context: Proof.context -> simpset -> simpset
val global_context: theory -> simpset -> simpset
val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
- val simproc_i: theory -> string -> term list
+ val simproc_global_i: theory -> string -> term list
-> (theory -> simpset -> term -> thm option) -> simproc
- val simproc: theory -> string -> string list
+ val simproc_global: theory -> string -> string list
-> (theory -> simpset -> term -> thm option) -> simproc
val rewrite: simpset -> conv
val asm_rewrite: simpset -> conv
--- a/src/Pure/thm.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Pure/thm.ML Thu Aug 26 09:03:18 2010 +0200
@@ -59,41 +59,11 @@
exception THM of string * int * thm list
val theory_of_thm: thm -> theory
val prop_of: thm -> term
- val tpairs_of: thm -> (term * term) list
val concl_of: thm -> term
val prems_of: thm -> term list
val nprems_of: thm -> int
val cprop_of: thm -> cterm
val cprem_of: thm -> int -> cterm
- val transfer: theory -> thm -> thm
- val weaken: cterm -> thm -> thm
- val weaken_sorts: sort list -> cterm -> cterm
- val extra_shyps: thm -> sort list
-
- (*meta rules*)
- val assume: cterm -> thm
- val implies_intr: cterm -> thm -> thm
- val implies_elim: thm -> thm -> thm
- val forall_intr: cterm -> thm -> thm
- val forall_elim: cterm -> thm -> thm
- val reflexive: cterm -> thm
- val symmetric: thm -> thm
- val transitive: thm -> thm -> thm
- val beta_conversion: bool -> conv
- val eta_conversion: conv
- val eta_long_conversion: conv
- val abstract_rule: string -> cterm -> thm -> thm
- val combination: thm -> thm -> thm
- val equal_intr: thm -> thm -> thm
- val equal_elim: thm -> thm -> thm
- val flexflex_rule: thm -> thm Seq.seq
- val generalize: string list * string list -> int -> thm -> thm
- val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
- val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
- val trivial: cterm -> thm
- val dest_state: thm * int -> (term * term) list * term list * term * term
- val lift_rule: cterm -> thm -> thm
- val incr_indexes: int -> thm -> thm
end;
signature THM =
@@ -119,8 +89,13 @@
val maxidx_of: thm -> int
val maxidx_thm: thm -> int -> int
val hyps_of: thm -> term list
+ val tpairs_of: thm -> (term * term) list
val no_prems: thm -> bool
val major_prem_of: thm -> term
+ val transfer: theory -> thm -> thm
+ val weaken: cterm -> thm -> thm
+ val weaken_sorts: sort list -> cterm -> cterm
+ val extra_shyps: thm -> sort list
val join_proofs: thm list -> unit
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
@@ -134,21 +109,45 @@
val map_tags: (Properties.T -> Properties.T) -> thm -> thm
val norm_proof: thm -> thm
val adjust_maxidx_thm: int -> thm -> thm
- val varifyT_global: thm -> thm
- val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
+ (*meta rules*)
+ val assume: cterm -> thm
+ val implies_intr: cterm -> thm -> thm
+ val implies_elim: thm -> thm -> thm
+ val forall_intr: cterm -> thm -> thm
+ val forall_elim: cterm -> thm -> thm
+ val reflexive: cterm -> thm
+ val symmetric: thm -> thm
+ val transitive: thm -> thm -> thm
+ val beta_conversion: bool -> conv
+ val eta_conversion: conv
+ val eta_long_conversion: conv
+ val abstract_rule: string -> cterm -> thm -> thm
+ val combination: thm -> thm -> thm
+ val equal_intr: thm -> thm -> thm
+ val equal_elim: thm -> thm -> thm
+ val flexflex_rule: thm -> thm Seq.seq
+ val generalize: string list * string list -> int -> thm -> thm
+ val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
+ val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
+ val trivial: cterm -> thm
val of_class: ctyp * class -> thm
val strip_shyps: thm -> thm
val unconstrainT: thm -> thm
+ val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
+ val varifyT_global: thm -> thm
val legacy_freezeT: thm -> thm
+ val dest_state: thm * int -> (term * term) list * term list * term * term
+ val lift_rule: cterm -> thm -> thm
+ val incr_indexes: int -> thm -> thm
val assumption: int -> thm -> thm Seq.seq
val eq_assumption: int -> thm -> thm
val rotate_rule: int -> int -> thm -> thm
val permute_prems: int -> int -> thm -> thm
val rename_params_rule: string list * int -> thm -> thm
+ val rename_boundvars: term -> term -> thm -> thm
val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
- val rename_boundvars: term -> term -> thm -> thm
val extern_oracles: theory -> xstring list
val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
end;
--- a/src/Tools/Code/code_haskell.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Aug 26 09:03:18 2010 +0200
@@ -395,8 +395,8 @@
end
in
Code_Target.mk_serialization target
- (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
- (write_module (check_destination file)))
+ (fn NONE => K () o map (code_writeln o (fn p => Pretty.block [p, Pretty.fbrk]) o snd)
+ | SOME file => K () o map (write_module (check_destination file)))
(rpair [] o cat_lines o map (code_of_pretty o snd))
(map (uncurry print_module) includes
@ map serialize_module (Symtab.dest hs_program))
--- a/src/Tools/induct.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Tools/induct.ML Thu Aug 26 09:03:18 2010 +0200
@@ -152,7 +152,7 @@
| SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
val rearrange_eqs_simproc =
- Simplifier.simproc
+ Simplifier.simproc_global
(Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
(fn thy => fn ss => fn t =>
mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t));
--- a/src/Tools/jEdit/src/jedit/document_view.scala Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu Aug 26 09:03:18 2010 +0200
@@ -198,7 +198,8 @@
val offset = snapshot.revert(text_area.xyToOffset(x, y))
snapshot.node.command_at(offset) match {
case Some((command, command_start)) =>
- (snapshot.state(command).markup.select(Text.Range(offset) - command_start) {
+ // FIXME Isar_Document.Tooltip extractor
+ (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) {
case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
val typing =
Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body)
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Aug 26 09:03:18 2010 +0200
@@ -48,7 +48,8 @@
val offset = snapshot.revert(buffer_offset)
snapshot.node.command_at(offset) match {
case Some((command, command_start)) =>
- (snapshot.state(command).markup.select(Text.Range(offset) - command_start) {
+ // FIXME Isar_Document.Hyperlink extractor
+ (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) {
case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _),
List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) =>
val Text.Range(begin, end) = snapshot.convert(info_range + command_start)
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Aug 26 01:03:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Aug 26 09:03:18 2010 +0200
@@ -130,22 +130,28 @@
val root = data.root
val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??)
for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
- snapshot.state(command).markup_root.swing_tree(root)((info: Text.Info[Any]) =>
+ snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
{
+ val range = info.range + command_start
val content = command.source(info.range).replace('\n', ' ')
- val id = command.id
+ val info_text =
+ info.info match {
+ case elem @ XML.Elem(_, _) =>
+ Pretty.formatted(List(elem), margin = 40).mkString("\n")
+ case x => x.toString
+ }
new DefaultMutableTreeNode(new IAsset {
override def getIcon: Icon = null
override def getShortString: String = content
- override def getLongString: String = info.info.toString
- override def getName: String = Markup.Long(id)
+ override def getLongString: String = info_text
+ override def getName: String = command.toString
override def setName(name: String) = ()
override def setStart(start: Position) = ()
- override def getStart: Position = command_start + info.range.start
+ override def getStart: Position = range.start
override def setEnd(end: Position) = ()
- override def getEnd: Position = command_start + info.range.stop
- override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
+ override def getEnd: Position = range.stop
+ override def toString = "\"" + content + "\" " + range.toString
})
})
}
--- a/src/ZF/Datatype_ZF.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/ZF/Datatype_ZF.thy Thu Aug 26 09:03:18 2010 +0200
@@ -101,7 +101,7 @@
handle Match => NONE;
- val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc;
+ val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc;
end;
--- a/src/ZF/OrdQuant.thy Thu Aug 26 01:03:08 2010 +0200
+++ b/src/ZF/OrdQuant.thy Thu Aug 26 09:03:18 2010 +0200
@@ -381,9 +381,9 @@
in
-val defREX_regroup = Simplifier.simproc @{theory}
+val defREX_regroup = Simplifier.simproc_global @{theory}
"defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
-val defRALL_regroup = Simplifier.simproc @{theory}
+val defRALL_regroup = Simplifier.simproc_global @{theory}
"defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
end;
--- a/src/ZF/arith_data.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/ZF/arith_data.ML Thu Aug 26 09:03:18 2010 +0200
@@ -77,7 +77,7 @@
end;
fun prep_simproc thy (name, pats, proc) =
- Simplifier.simproc thy name pats proc;
+ Simplifier.simproc_global thy name pats proc;
(*** Use CancelNumerals simproc without binary numerals,
--- a/src/ZF/int_arith.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/ZF/int_arith.ML Thu Aug 26 09:03:18 2010 +0200
@@ -147,7 +147,7 @@
[@{thm zmult_assoc}, @{thm zmult_zminus} RS @{thm sym}, int_minus_mult_eq_1_to_2];
fun prep_simproc thy (name, pats, proc) =
- Simplifier.simproc thy name pats proc;
+ Simplifier.simproc_global thy name pats proc;
structure CancelNumeralsCommon =
struct
--- a/src/ZF/simpdata.ML Thu Aug 26 01:03:08 2010 +0200
+++ b/src/ZF/simpdata.ML Thu Aug 26 09:03:18 2010 +0200
@@ -59,10 +59,10 @@
in
-val defBEX_regroup = Simplifier.simproc (Theory.deref @{theory_ref})
+val defBEX_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
"defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
-val defBALL_regroup = Simplifier.simproc (Theory.deref @{theory_ref})
+val defBALL_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
"defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
end;