# HG changeset patch # User wenzelm # Date 1237754894 -3600 # Node ID 94b74365ceb92446e8cdc83613d878700073d06f # Parent 226c91456e5435c0c2d1bb643b43fd7a64a57fae# Parent d26ad4576d5cd1b9a8fc90228dd15034869b5c78 merged diff -r d26ad4576d5c -r 94b74365ceb9 doc-src/IsarOverview/Isar/Induction.thy --- a/doc-src/IsarOverview/Isar/Induction.thy Sun Mar 22 21:30:21 2009 +0100 +++ b/doc-src/IsarOverview/Isar/Induction.thy Sun Mar 22 21:48:14 2009 +0100 @@ -143,14 +143,14 @@ universally quantifies all \emph{vars} before the induction. Hence they can be replaced by \emph{arbitrary} values in the proof. -The nice thing about generalization via @{text"arbitrary:"} is that in -the induction step the claim is available in unquantified form but +Generalization via @{text"arbitrary"} is particularly convenient +if the induction step is a structured proof as opposed to the automatic +example above. Then the claim is available in unquantified form but with the generalized variables replaced by @{text"?"}-variables, ready -for instantiation. In the above example the -induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"}. +for instantiation. In the above example, in the @{const[source] Cons} case the +induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"} (available +under the name @{const[source] Cons}). -For the curious: @{text"arbitrary:"} introduces @{text"\"} -behind the scenes. \subsection{Inductive proofs of conditional formulae} \label{sec:full-Ind} diff -r d26ad4576d5c -r 94b74365ceb9 doc-src/IsarOverview/Isar/Logic.thy --- a/doc-src/IsarOverview/Isar/Logic.thy Sun Mar 22 21:30:21 2009 +0100 +++ b/doc-src/IsarOverview/Isar/Logic.thy Sun Mar 22 21:48:14 2009 +0100 @@ -30,8 +30,8 @@ show A by(rule a) qed -text{*\noindent Single-identifier formulae such as @{term A} need not -be enclosed in double quotes. However, we will continue to do so for +text{*\noindent As you see above, single-identifier formulae such as @{term A} +need not be enclosed in double quotes. However, we will continue to do so for uniformity. Instead of applying fact @{text a} via the @{text rule} method, we can diff -r d26ad4576d5c -r 94b74365ceb9 doc-src/IsarOverview/Isar/document/Induction.tex --- a/doc-src/IsarOverview/Isar/document/Induction.tex Sun Mar 22 21:30:21 2009 +0100 +++ b/doc-src/IsarOverview/Isar/document/Induction.tex Sun Mar 22 21:48:14 2009 +0100 @@ -342,14 +342,14 @@ universally quantifies all \emph{vars} before the induction. Hence they can be replaced by \emph{arbitrary} values in the proof. -The nice thing about generalization via \isa{arbitrary{\isacharcolon}} is that in -the induction step the claim is available in unquantified form but +Generalization via \isa{arbitrary} is particularly convenient +if the induction step is a structured proof as opposed to the automatic +example above. Then the claim is available in unquantified form but with the generalized variables replaced by \isa{{\isacharquery}}-variables, ready -for instantiation. In the above example the -induction hypothesis is \isa{itrev\ xs\ {\isacharquery}ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharquery}ys}. +for instantiation. In the above example, in the \isa{Cons} case the +induction hypothesis is \isa{itrev\ xs\ {\isacharquery}ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharquery}ys} (available +under the name \isa{Cons}). -For the curious: \isa{arbitrary{\isacharcolon}} introduces \isa{{\isasymAnd}} -behind the scenes. \subsection{Inductive proofs of conditional formulae} \label{sec:full-Ind} diff -r d26ad4576d5c -r 94b74365ceb9 doc-src/IsarOverview/Isar/document/Logic.tex --- a/doc-src/IsarOverview/Isar/document/Logic.tex Sun Mar 22 21:30:21 2009 +0100 +++ b/doc-src/IsarOverview/Isar/document/Logic.tex Sun Mar 22 21:48:14 2009 +0100 @@ -93,8 +93,8 @@ \endisadelimproof % \begin{isamarkuptext}% -\noindent Single-identifier formulae such as \isa{A} need not -be enclosed in double quotes. However, we will continue to do so for +\noindent As you see above, single-identifier formulae such as \isa{A} +need not be enclosed in double quotes. However, we will continue to do so for uniformity. Instead of applying fact \isa{a} via the \isa{rule} method, we can diff -r d26ad4576d5c -r 94b74365ceb9 doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Sun Mar 22 21:30:21 2009 +0100 +++ b/doc-src/TutorialI/Documents/Documents.thy Sun Mar 22 21:48:14 2009 +0100 @@ -617,7 +617,7 @@ same types as they have in the main goal statement. \medskip Several further kinds of antiquotations and options are - available \cite{isabelle-sys}. Here are a few commonly used + available \cite{isabelle-isar-ref}. Here are a few commonly used combinations: \medskip diff -r d26ad4576d5c -r 94b74365ceb9 doc-src/TutorialI/Documents/document/Documents.tex --- a/doc-src/TutorialI/Documents/document/Documents.tex Sun Mar 22 21:30:21 2009 +0100 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Sun Mar 22 21:48:14 2009 +0100 @@ -691,7 +691,7 @@ same types as they have in the main goal statement. \medskip Several further kinds of antiquotations and options are - available \cite{isabelle-sys}. Here are a few commonly used + available \cite{isabelle-isar-ref}. Here are a few commonly used combinations: \medskip diff -r d26ad4576d5c -r 94b74365ceb9 doc-src/TutorialI/Rules/rules.tex --- a/doc-src/TutorialI/Rules/rules.tex Sun Mar 22 21:30:21 2009 +0100 +++ b/doc-src/TutorialI/Rules/rules.tex Sun Mar 22 21:48:14 2009 +0100 @@ -2138,11 +2138,11 @@ \index{*insert (method)|(}% The \isa{insert} method -inserts a given theorem as a new assumption of the current subgoal. This +inserts a given theorem as a new assumption of all subgoals. This already is a forward step; moreover, we may (as always when using a theorem) apply \isa{of}, \isa{THEN} and other directives. The new assumption can then -be used to help prove the subgoal. +be used to help prove the subgoals. For example, consider this theorem about the divides relation. The first proof step inserts the distributive law for diff -r d26ad4576d5c -r 94b74365ceb9 doc-src/TutorialI/Sets/sets.tex --- a/doc-src/TutorialI/Sets/sets.tex Sun Mar 22 21:30:21 2009 +0100 +++ b/doc-src/TutorialI/Sets/sets.tex Sun Mar 22 21:48:14 2009 +0100 @@ -299,7 +299,7 @@ \isa{UN x:A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law: \begin{isabelle} (b\ \isasymin\ -(\isasymUnion x\isasymin A. B\ x) =\ (\isasymexists x\isasymin A.\ +(\isasymUnion x\isasymin A. B\ x)) =\ (\isasymexists x\isasymin A.\ b\ \isasymin\ B\ x) \rulenamedx{UN_iff} \end{isabelle} @@ -414,12 +414,12 @@ $k$-element subsets of~$A$ is \index{binomial coefficients} $\binom{n}{k}$. -\begin{warn} -The term \isa{finite\ A} is defined via a syntax translation as an -abbreviation for \isa{A {\isasymin} Finites}, where the constant -\cdx{Finites} denotes the set of all finite sets of a given type. There -is no constant \isa{finite}. -\end{warn} +%\begin{warn} +%The term \isa{finite\ A} is defined via a syntax translation as an +%abbreviation for \isa{A {\isasymin} Finites}, where the constant +%\cdx{Finites} denotes the set of all finite sets of a given type. There +%is no constant \isa{finite}. +%\end{warn} \index{sets|)} diff -r d26ad4576d5c -r 94b74365ceb9 doc-src/TutorialI/Types/Overloading2.thy --- a/doc-src/TutorialI/Types/Overloading2.thy Sun Mar 22 21:30:21 2009 +0100 +++ b/doc-src/TutorialI/Types/Overloading2.thy Sun Mar 22 21:48:14 2009 +0100 @@ -15,7 +15,7 @@ size xs = size ys \ (\i real n * x + ?N s" by simp finally have "?N (Floor s) \ real n * x + ?N s" . moreover - {from mult_strict_left_mono[OF x1] np - have "real n *x + ?N s < real n + ?N s" by simp + {from x1 np have "real n *x + ?N s < real n + ?N s" by simp also from real_of_int_floor_add_one_gt[where r="?N s"] have "\ < real n + ?N (Floor s) + 1" by simp finally have "real n *x + ?N s < ?N (Floor s) + real (n+1)" by simp} @@ -3809,8 +3808,7 @@ moreover from mult_left_mono_neg[OF xp] nn have "?N s \ real n * x + ?N s" by simp ultimately have "?N (Floor s) + 1 > real n * x + ?N s" by arith moreover - {from mult_strict_left_mono_neg[OF x1, where c="real n"] nn - have "real n *x + ?N s \ real n + ?N s" by simp + {from x1 nn have "real n *x + ?N s \ real n + ?N s" by simp moreover from real_of_int_floor_le[where r="?N s"] have "real n + ?N s \ real n + ?N (Floor s)" by simp ultimately have "real n *x + ?N s \ ?N (Floor s) + real n" by (simp only: algebra_simps)} diff -r d26ad4576d5c -r 94b74365ceb9 src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Sun Mar 22 21:30:21 2009 +0100 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Sun Mar 22 21:48:14 2009 +0100 @@ -1494,8 +1494,7 @@ have thy: "norm (y' - y) * norm x' < e / (2 * norm x + 2 * norm y + 2) * (1 + norm x)" using mult_strict_mono'[OF h(4) * norm_ge_zero norm_ge_zero] by auto also have "\ \ e/2" apply simp unfolding divide_le_eq - using th1 th0 `e>0` apply auto - unfolding mult_assoc and real_mult_le_cancel_iff2[OF `e>0`] by auto + using th1 th0 `e>0` by auto finally have "norm x' * norm (y' - y) + norm (x' - x) * norm y < e" using thx and e by (simp add: field_simps) } @@ -3558,7 +3557,7 @@ { fix y assume "dist y (c *s x) < e * \c\" hence "norm ((1 / c) *s y - x) < e" unfolding dist_def using norm_mul[of c "(1 / c) *s y - x", unfolded vector_ssub_ldistrib, unfolded vector_smult_assoc] assms(1) - mult_less_imp_less_left[of "abs c" "norm ((1 / c) *s y - x)" e, unfolded real_mult_commute[of "abs c" e]] assms(1)[unfolded zero_less_abs_iff[THEN sym]] by simp + assms(1)[unfolded zero_less_abs_iff[THEN sym]] by (simp del:zero_less_abs_iff) hence "y \ op *s c ` s" using rev_image_eqI[of "(1 / c) *s y" s y "op *s c"] e[THEN spec[where x="(1 / c) *s y"]] assms(1) unfolding dist_def vector_smult_assoc by auto } ultimately have "\e>0. \x'. dist x' (c *s x) < e \ x' \ op *s c ` s" apply(rule_tac x="e * abs c" in exI) by auto } thus ?thesis unfolding open_def by auto diff -r d26ad4576d5c -r 94b74365ceb9 src/HOL/Rational.thy --- a/src/HOL/Rational.thy Sun Mar 22 21:30:21 2009 +0100 +++ b/src/HOL/Rational.thy Sun Mar 22 21:48:14 2009 +0100 @@ -691,7 +691,6 @@ \ Fract a b < Fract c d" using not_zero `b * d > 0` by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult) - (auto intro: mult_strict_right_mono mult_right_less_imp_less) qed lemma of_rat_less_eq: diff -r d26ad4576d5c -r 94b74365ceb9 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Sun Mar 22 21:30:21 2009 +0100 +++ b/src/HOL/Ring_and_Field.thy Sun Mar 22 21:48:14 2009 +0100 @@ -1136,6 +1136,27 @@ "c * a \ c * b \ (0 < c \ a \ b) \ (c < 0 \ b \ a)" by (simp add: not_less [symmetric] mult_less_cancel_left_disj) +lemma mult_le_cancel_left_pos: + "0 < c \ c * a \ c * b \ a \ b" +by (auto simp: mult_le_cancel_left) + +lemma mult_le_cancel_left_neg: + "c < 0 \ c * a \ c * b \ b \ a" +by (auto simp: mult_le_cancel_left) + +end + +context ordered_ring_strict +begin + +lemma mult_less_cancel_left_pos: + "0 < c \ c * a < c * b \ a < b" +by (auto simp: mult_less_cancel_left) + +lemma mult_less_cancel_left_neg: + "c < 0 \ c * a < c * b \ b < a" +by (auto simp: mult_less_cancel_left) + end text{*Legacy - use @{text algebra_simps} *} diff -r d26ad4576d5c -r 94b74365ceb9 src/HOL/Series.thy --- a/src/HOL/Series.thy Sun Mar 22 21:30:21 2009 +0100 +++ b/src/HOL/Series.thy Sun Mar 22 21:48:14 2009 +0100 @@ -557,7 +557,6 @@ apply (induct_tac "na", auto) apply (rule_tac y = "c * norm (f (N + n))" in order_trans) apply (auto intro: mult_right_mono simp add: summable_def) -apply (simp add: mult_ac) apply (rule_tac x = "norm (f N) * (1/ (1 - c)) / (c ^ N)" in exI) apply (rule sums_divide) apply (rule sums_mult) diff -r d26ad4576d5c -r 94b74365ceb9 src/HOL/Tools/int_factor_simprocs.ML --- a/src/HOL/Tools/int_factor_simprocs.ML Sun Mar 22 21:30:21 2009 +0100 +++ b/src/HOL/Tools/int_factor_simprocs.ML Sun Mar 22 21:48:14 2009 +0100 @@ -218,9 +218,30 @@ val simplify_one = Arith_Data.simplify_meta_eq [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}]; -fun cancel_simplify_meta_eq cancel_th ss th = +fun cancel_simplify_meta_eq ss cancel_th th = simplify_one ss (([th, cancel_th]) MRS trans); +local + val Tp_Eq = Thm.reflexive(Thm.cterm_of (@{theory HOL}) HOLogic.Trueprop) + fun Eq_True_elim Eq = + Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI} +in +fun sign_conv pos_th neg_th ss t = + let val T = fastype_of t; + val zero = Const(@{const_name HOL.zero}, T); + val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT); + val pos = less $ zero $ t and neg = less $ t $ zero + fun prove p = + Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p) + handle THM _ => NONE + in case prove pos of + SOME th => SOME(th RS pos_th) + | NONE => (case prove neg of + SOME th => SOME(th RS neg_th) + | NONE => NONE) + end; +end + structure CancelFactorCommon = struct val mk_sum = long_mk_prod @@ -231,6 +252,7 @@ val trans_tac = K Arith_Data.trans_tac val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) + val simplify_meta_eq = cancel_simplify_meta_eq end; (*mult_cancel_left requires a ring with no zero divisors.*) @@ -239,7 +261,27 @@ val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" Term.dummyT - val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_cancel_left} + val simp_conv = K (K (SOME @{thm mult_cancel_left})) +); + +(*for ordered rings*) +structure LeCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT + val simp_conv = sign_conv + @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg} +); + +(*for ordered rings*) +structure LessCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT + val simp_conv = sign_conv + @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg} ); (*zdiv_zmult_zmult1_if is for integer division (div).*) @@ -248,7 +290,7 @@ val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.div} val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT - val simplify_meta_eq = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if} + val simp_conv = K (K (SOME @{thm zdiv_zmult_zmult1_if})) ); structure IntModCancelFactor = ExtractCommonTermFun @@ -256,7 +298,7 @@ val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT - val simplify_meta_eq = cancel_simplify_meta_eq @{thm zmod_zmult_zmult1} + val simp_conv = K (K (SOME @{thm zmod_zmult_zmult1})) ); structure IntDvdCancelFactor = ExtractCommonTermFun @@ -264,7 +306,7 @@ val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT - val simplify_meta_eq = cancel_simplify_meta_eq @{thm dvd_mult_cancel_left} + val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left})) ); (*Version for all fields, including unordered ones (type complex).*) @@ -273,7 +315,7 @@ val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT - val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if} + val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if})) ); val cancel_factors = @@ -281,7 +323,15 @@ [("ring_eq_cancel_factor", ["(l::'a::{idom}) * m = n", "(l::'a::{idom}) = m * n"], - K EqCancelFactor.proc), + K EqCancelFactor.proc), + ("ordered_ring_le_cancel_factor", + ["(l::'a::ordered_ring) * m <= n", + "(l::'a::ordered_ring) <= m * n"], + K LeCancelFactor.proc), + ("ordered_ring_less_cancel_factor", + ["(l::'a::ordered_ring) * m < n", + "(l::'a::ordered_ring) < m * n"], + K LessCancelFactor.proc), ("int_div_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m * n)"], K IntDivCancelFactor.proc), diff -r d26ad4576d5c -r 94b74365ceb9 src/HOL/Tools/nat_simprocs.ML --- a/src/HOL/Tools/nat_simprocs.ML Sun Mar 22 21:30:21 2009 +0100 +++ b/src/HOL/Tools/nat_simprocs.ML Sun Mar 22 21:48:14 2009 +0100 @@ -352,7 +352,7 @@ val simplify_one = Arith_Data.simplify_meta_eq [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}]; -fun cancel_simplify_meta_eq cancel_th ss th = +fun cancel_simplify_meta_eq ss cancel_th th = simplify_one ss (([th, cancel_th]) MRS trans); structure CancelFactorCommon = @@ -365,6 +365,7 @@ val trans_tac = K Arith_Data.trans_tac val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) + val simplify_meta_eq = cancel_simplify_meta_eq end; structure EqCancelFactor = ExtractCommonTermFun @@ -372,7 +373,7 @@ val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT - val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_eq_cancel_disj} + val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj})) ); structure LessCancelFactor = ExtractCommonTermFun @@ -380,7 +381,7 @@ val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT - val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj} + val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj})) ); structure LeCancelFactor = ExtractCommonTermFun @@ -388,7 +389,7 @@ val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT - val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj} + val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj})) ); structure DivideCancelFactor = ExtractCommonTermFun @@ -396,7 +397,7 @@ val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.div} val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT - val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj} + val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj})) ); structure DvdCancelFactor = ExtractCommonTermFun @@ -404,7 +405,7 @@ val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT - val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj} + val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj})) ); val cancel_factor = diff -r d26ad4576d5c -r 94b74365ceb9 src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Sun Mar 22 21:30:21 2009 +0100 +++ b/src/HOL/Word/WordArith.thy Sun Mar 22 21:48:14 2009 +0100 @@ -701,6 +701,7 @@ apply (erule (2) udvd_decr0) done +ML{*Delsimprocs cancel_factors*} lemma udvd_incr2_K: "p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==> 0 < K ==> p <= p + K & p + K <= a + s" @@ -716,6 +717,7 @@ apply arith apply simp done +ML{*Delsimprocs cancel_factors*} (* links with rbl operations *) lemma word_succ_rbl: diff -r d26ad4576d5c -r 94b74365ceb9 src/Provers/Arith/extract_common_term.ML --- a/src/Provers/Arith/extract_common_term.ML Sun Mar 22 21:30:21 2009 +0100 +++ b/src/Provers/Arith/extract_common_term.ML Sun Mar 22 21:48:14 2009 +0100 @@ -25,7 +25,8 @@ (*proof tools*) val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option val norm_tac: simpset -> tactic (*proves the result*) - val simplify_meta_eq: simpset -> thm -> thm (*simplifies the result*) + val simplify_meta_eq: simpset -> thm -> thm -> thm (*simplifies the result*) + val simp_conv: simpset -> term -> thm option (*proves simp thm*) end; @@ -58,6 +59,9 @@ and terms2 = Data.dest_sum t2 val u = find_common (terms1,terms2) + val simp_th = + case Data.simp_conv ss u of NONE => raise TERM("no simp", []) + | SOME th => th val terms1' = Data.find_first u terms1 and terms2' = Data.find_first u terms2 and T = Term.fastype_of u @@ -66,7 +70,7 @@ Data.prove_conv [Data.norm_tac ss] ctxt prems (t', Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2'))) in - Option.map (export o Data.simplify_meta_eq ss) reshape + Option.map (export o Data.simplify_meta_eq ss simp_th) reshape end (* FIXME avoid handling of generic exceptions *) handle TERM _ => NONE diff -r d26ad4576d5c -r 94b74365ceb9 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Sun Mar 22 21:30:21 2009 +0100 +++ b/src/Pure/General/table.ML Sun Mar 22 21:48:14 2009 +0100 @@ -383,3 +383,6 @@ structure Inttab = TableFun(type key = int val ord = int_ord); structure Symtab = TableFun(type key = string val ord = fast_string_ord); +structure Symreltab = TableFun(type key = string * string + val ord = prod_ord fast_string_ord fast_string_ord); + diff -r d26ad4576d5c -r 94b74365ceb9 src/Tools/code/code_haskell.ML --- a/src/Tools/code/code_haskell.ML Sun Mar 22 21:30:21 2009 +0100 +++ b/src/Tools/code/code_haskell.ML Sun Mar 22 21:48:14 2009 +0100 @@ -42,18 +42,18 @@ of [] => [] | classbinds => Pretty.enum "," "(" ")" ( map (fn (v, class) => - str (class_name class ^ " " ^ Code_Name.lookup_var tyvars v)) classbinds) + str (class_name class ^ " " ^ Code_Printer.lookup_var tyvars v)) classbinds) @@ str " => "; fun pr_typforall tyvars vs = case map fst vs of [] => [] | vnames => str "forall " :: Pretty.breaks - (map (str o Code_Name.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; + (map (str o Code_Printer.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; fun pr_tycoexpr tyvars fxy (tyco, tys) = brackify fxy (str tyco :: map (pr_typ tyvars BR) tys) and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys) | SOME (i, pr) => pr (pr_typ tyvars) fxy tys) - | pr_typ tyvars fxy (ITyVar v) = (str o Code_Name.lookup_var tyvars) v; + | pr_typ tyvars fxy (ITyVar v) = (str o Code_Printer.lookup_var tyvars) v; fun pr_typdecl tyvars (vs, tycoexpr) = Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr); fun pr_typscheme tyvars (vs, ty) = @@ -69,7 +69,7 @@ pr_term tyvars thm vars BR t2 ]) | pr_term tyvars thm vars fxy (IVar v) = - (str o Code_Name.lookup_var vars) v + (str o Code_Printer.lookup_var vars) v | pr_term tyvars thm vars fxy (t as _ `|-> _) = let val (binds, t') = Code_Thingol.unfold_abs t; @@ -127,7 +127,7 @@ | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\""; fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) = let - val tyvars = Code_Name.intro_vars (map fst vs) init_syms; + val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; val n = (length o fst o Code_Thingol.unfold_fun) ty; in Pretty.chunks [ @@ -150,7 +150,7 @@ | pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = let val eqs = filter (snd o snd) raw_eqs; - val tyvars = Code_Name.intro_vars (map fst vs) init_syms; + val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; fun pr_eq ((ts, t), (thm, _)) = let val consts = map_filter @@ -158,8 +158,8 @@ then NONE else (SOME o Long_Name.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = init_syms - |> Code_Name.intro_vars consts - |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) + |> Code_Printer.intro_vars consts + |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) (insert (op =)) ts []); in semicolon ( @@ -182,7 +182,7 @@ end | pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) = let - val tyvars = Code_Name.intro_vars (map fst vs) init_syms; + val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; in semicolon [ str "data", @@ -191,7 +191,7 @@ end | pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) = let - val tyvars = Code_Name.intro_vars (map fst vs) init_syms; + val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; in semicolon ( str "newtype" @@ -204,7 +204,7 @@ end | pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) = let - val tyvars = Code_Name.intro_vars (map fst vs) init_syms; + val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; fun pr_co (co, tys) = concat ( (str o deresolve_base) co @@ -222,7 +222,7 @@ end | pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) = let - val tyvars = Code_Name.intro_vars [v] init_syms; + val tyvars = Code_Printer.intro_vars [v] init_syms; fun pr_classparam (classparam, ty) = semicolon [ (str o deresolve_base) classparam, @@ -234,7 +234,7 @@ Pretty.block [ str "class ", Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]), - str (deresolve_base name ^ " " ^ Code_Name.lookup_var tyvars v), + str (deresolve_base name ^ " " ^ Code_Printer.lookup_var tyvars v), str " where {" ], str "};" @@ -244,7 +244,7 @@ let val split_abs_pure = (fn (v, _) `|-> t => SOME (v, t) | _ => NONE); val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure; - val tyvars = Code_Name.intro_vars (map fst vs) init_syms; + val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam of NONE => semicolon [ (str o deresolve_base) classparam, @@ -259,8 +259,8 @@ val proto_rhs = Code_Thingol.eta_expand k (c_inst, []); val (vs, rhs) = unfold_abs_pure proto_rhs; val vars = init_syms - |> Code_Name.intro_vars (the_list const) - |> Code_Name.intro_vars vs; + |> Code_Printer.intro_vars (the_list const) + |> Code_Printer.intro_vars vs; val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs; (*dictionaries are not relevant at this late stage*) in @@ -288,20 +288,20 @@ let val module_alias = if is_some module_name then K module_name else raw_module_alias; val reserved_names = Name.make_context reserved_names; - val mk_name_module = Code_Name.mk_name_module reserved_names module_prefix module_alias program; + val mk_name_module = Code_Printer.mk_name_module reserved_names module_prefix module_alias program; fun add_stmt (name, (stmt, deps)) = let - val (module_name, base) = Code_Name.dest_name name; + val (module_name, base) = Code_Printer.dest_name name; val module_name' = mk_name_module module_name; val mk_name_stmt = yield_singleton Name.variants; fun add_fun upper (nsp_fun, nsp_typ) = let val (base', nsp_fun') = - mk_name_stmt (if upper then Code_Name.first_upper base else base) nsp_fun + mk_name_stmt (if upper then Code_Printer.first_upper base else base) nsp_fun in (base', (nsp_fun', nsp_typ)) end; fun add_typ (nsp_fun, nsp_typ) = let - val (base', nsp_typ') = mk_name_stmt (Code_Name.first_upper base) nsp_typ + val (base', nsp_typ') = mk_name_stmt (Code_Printer.first_upper base) nsp_typ in (base', (nsp_fun, nsp_typ')) end; val add_name = case stmt of Code_Thingol.Fun _ => add_fun false @@ -330,7 +330,7 @@ (Graph.get_node program name, Graph.imm_succs program name)) (Graph.strong_conn program |> flat)) Symtab.empty; fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the - o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Name.dest_name) name))) name + o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Printer.dest_name) name))) name handle Option => error ("Unknown statement name: " ^ labelled_name name); in (deresolver, hs_program) end; @@ -357,7 +357,7 @@ andalso forall (deriv' tycos) tys | deriv' _ (ITyVar _) = true in deriv [] tyco end; - val reserved_names = Code_Name.make_vars reserved_names; + val reserved_names = Code_Printer.make_vars reserved_names; fun pr_stmt qualified = pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const reserved_names (if qualified then deresolver else Long_Name.base_name o deresolver) diff -r d26ad4576d5c -r 94b74365ceb9 src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Sun Mar 22 21:30:21 2009 +0100 +++ b/src/Tools/code/code_ml.ML Sun Mar 22 21:48:14 2009 +0100 @@ -50,8 +50,8 @@ val pr_label_classparam = Long_Name.base_name o Long_Name.qualifier; fun pr_dicts fxy ds = let - fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_" - | pr_dictvar (v, (i, _)) = Code_Name.first_upper v ^ string_of_int (i+1) ^ "_"; + fun pr_dictvar (v, (_, 1)) = Code_Printer.first_upper v ^ "_" + | pr_dictvar (v, (i, _)) = Code_Printer.first_upper v ^ string_of_int (i+1) ^ "_"; fun pr_proj [] p = p | pr_proj [p'] p = @@ -87,7 +87,7 @@ fun pr_term is_closure thm vars fxy (IConst c) = pr_app is_closure thm vars fxy (c, []) | pr_term is_closure thm vars fxy (IVar v) = - str (Code_Name.lookup_var vars v) + str (Code_Printer.lookup_var vars v) | pr_term is_closure thm vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t of SOME c_ts => pr_app is_closure thm vars fxy c_ts @@ -182,7 +182,7 @@ then NONE else (SOME o Long_Name.base_name o deresolve) c) (Code_Thingol.fold_constnames (insert (op =)) t []); val vars = reserved_names - |> Code_Name.intro_vars consts; + |> Code_Printer.intro_vars consts; in concat [ str "val", @@ -207,8 +207,8 @@ then NONE else (SOME o Long_Name.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = reserved_names - |> Code_Name.intro_vars consts - |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) + |> Code_Printer.intro_vars consts + |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) (insert (op =)) ts []); in concat ( @@ -266,7 +266,7 @@ in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = let - val w = Code_Name.first_upper v ^ "_"; + val w = Code_Printer.first_upper v ^ "_"; fun pr_superclass_field (class, classrel) = (concat o map str) [ pr_label_classrel classrel, ":", "'" ^ v, deresolve class @@ -362,8 +362,8 @@ let fun pr_dicts fxy ds = let - fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Name.first_upper v - | pr_dictvar (v, (i, _)) = "_" ^ Code_Name.first_upper v ^ string_of_int (i+1); + fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Printer.first_upper v + | pr_dictvar (v, (i, _)) = "_" ^ Code_Printer.first_upper v ^ string_of_int (i+1); fun pr_proj ps p = fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p fun pr_dict fxy (DictConst (inst, dss)) = @@ -395,7 +395,7 @@ fun pr_term is_closure thm vars fxy (IConst c) = pr_app is_closure thm vars fxy (c, []) | pr_term is_closure thm vars fxy (IVar v) = - str (Code_Name.lookup_var vars v) + str (Code_Printer.lookup_var vars v) | pr_term is_closure thm vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t of SOME c_ts => pr_app is_closure thm vars fxy c_ts @@ -468,8 +468,8 @@ val x = Name.variant (map_filter I fished1) "x"; val fished2 = map_index (fillup_param x) fished1; val (fished3, _) = Name.variants fished2 Name.context; - val vars' = Code_Name.intro_vars fished3 vars; - in map (Code_Name.lookup_var vars') fished3 end; + val vars' = Code_Printer.intro_vars fished3 vars; + in map (Code_Printer.lookup_var vars') fished3 end; fun pr_stmt (MLExc (name, n)) = let val exc_str = @@ -491,7 +491,7 @@ then NONE else (SOME o Long_Name.base_name o deresolve) c) (Code_Thingol.fold_constnames (insert (op =)) t []); val vars = reserved_names - |> Code_Name.intro_vars consts; + |> Code_Printer.intro_vars consts; in concat [ str "let", @@ -511,8 +511,8 @@ then NONE else (SOME o Long_Name.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = reserved_names - |> Code_Name.intro_vars consts - |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) + |> Code_Printer.intro_vars consts + |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) (insert (op =)) ts []); in concat [ (Pretty.block o Pretty.commas) @@ -527,8 +527,8 @@ then NONE else (SOME o Long_Name.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = reserved_names - |> Code_Name.intro_vars consts - |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) + |> Code_Printer.intro_vars consts + |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) (insert (op =)) ts []); in concat ( @@ -556,7 +556,7 @@ ((fold o Code_Thingol.fold_constnames) (insert (op =)) (map (snd o fst) eqs) []); val vars = reserved_names - |> Code_Name.intro_vars consts; + |> Code_Printer.intro_vars consts; val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs; in Pretty.block ( @@ -623,7 +623,7 @@ in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = let - val w = "_" ^ Code_Name.first_upper v; + val w = "_" ^ Code_Printer.first_upper v; fun pr_superclass_field (class, classrel) = (concat o map str) [ deresolve classrel, ":", "'" ^ v, deresolve class @@ -765,11 +765,11 @@ let val (x, nsp_typ') = f nsp_typ in (x, (nsp_fun, nsp_typ')) end; - val mk_name_module = Code_Name.mk_name_module reserved_names NONE module_alias program; + val mk_name_module = Code_Printer.mk_name_module reserved_names NONE module_alias program; fun mk_name_stmt upper name nsp = let - val (_, base) = Code_Name.dest_name name; - val base' = if upper then Code_Name.first_upper base else base; + val (_, base) = Code_Printer.dest_name name; + val base' = if upper then Code_Printer.first_upper base else base; val ([base''], nsp') = Name.variants [base'] nsp; in (base'', nsp') end; fun rearrange_fun name (tysm as (vs, ty), raw_eqs) = @@ -853,7 +853,7 @@ [] |> fold (fold (insert (op =)) o Graph.imm_succs program) names |> subtract (op =) names; - val (module_names, _) = (split_list o map Code_Name.dest_name) names; + val (module_names, _) = (split_list o map Code_Printer.dest_name) names; val module_name = (the_single o distinct (op =) o map mk_name_module) module_names handle Empty => error ("Different namespace prefixes for mutual dependencies:\n" @@ -863,7 +863,7 @@ val module_name_path = Long_Name.explode module_name; fun add_dep name name' = let - val module_name' = (mk_name_module o fst o Code_Name.dest_name) name'; + val module_name' = (mk_name_module o fst o Code_Printer.dest_name) name'; in if module_name = module_name' then map_node module_name_path (Graph.add_edge (name, name')) else let @@ -891,7 +891,7 @@ (rev (Graph.strong_conn program))); fun deresolver prefix name = let - val module_name = (fst o Code_Name.dest_name) name; + val module_name = (fst o Code_Printer.dest_name) name; val module_name' = (Long_Name.explode o mk_name_module) module_name; val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name'); val stmt_name = @@ -914,7 +914,7 @@ val module_name = if null stmt_names then raw_module_name else SOME "Code"; val (deresolver, nodes) = ml_node_of_program labelled_name module_name reserved_names raw_module_alias program; - val reserved_names = Code_Name.make_vars reserved_names; + val reserved_names = Code_Printer.make_vars reserved_names; fun pr_node prefix (Dummy _) = NONE | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse diff -r d26ad4576d5c -r 94b74365ceb9 src/Tools/code/code_name.ML --- a/src/Tools/code/code_name.ML Sun Mar 22 21:30:21 2009 +0100 +++ b/src/Tools/code/code_name.ML Sun Mar 22 21:48:14 2009 +0100 @@ -6,45 +6,20 @@ signature CODE_NAME = sig - structure StringPairTab: TABLE - val first_upper: string -> string - val first_lower: string -> string - val dest_name: string -> string * string - val purify_var: string -> string val purify_tvar: string -> string - val purify_sym: string -> string - val purify_base: bool -> string -> string + val purify_base: string -> string val check_modulename: string -> string - type var_ctxt - val make_vars: string list -> var_ctxt - val intro_vars: string list -> var_ctxt -> var_ctxt - val lookup_var: var_ctxt -> string -> string - val read_const_exprs: theory -> string list -> string list * string list - val mk_name_module: Name.context -> string option -> (string -> string option) - -> 'a Graph.T -> string -> string end; structure Code_Name: CODE_NAME = struct -(** auxiliary **) - -structure StringPairTab = - TableFun(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord); - -val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; -val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; - -val dest_name = - apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode; - - (** purification **) -fun purify_name upper lower = +fun purify_name upper = let fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'"; val is_junk = not o is_valid andf Symbol.is_regular; @@ -55,9 +30,8 @@ --| junk)) ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk)); fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs - else if lower then (if forall Symbol.is_ascii_upper cs - then map else nth_map 0) Symbol.to_ascii_lower cs - else cs; + else (if forall Symbol.is_ascii_upper cs + then map else nth_map 0) Symbol.to_ascii_lower cs; in explode #> scan_valids @@ -68,7 +42,7 @@ end; fun purify_var "" = "x" - | purify_var v = purify_name false true v; + | purify_var v = purify_name false v; fun purify_tvar "" = "'a" | purify_tvar v = @@ -81,52 +55,29 @@ (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular)) #> implode #> Long_Name.explode - #> map (purify_name true false); + #> map (purify_name true); (*FIMXE non-canonical function treating non-canonical names*) -fun purify_base _ "op &" = "and" - | purify_base _ "op |" = "or" - | purify_base _ "op -->" = "implies" - | purify_base _ "{}" = "empty" - | purify_base _ "op :" = "member" - | purify_base _ "op Int" = "intersect" - | purify_base _ "op Un" = "union" - | purify_base _ "*" = "product" - | purify_base _ "+" = "sum" - | purify_base lower s = if String.isPrefix "op =" s - then "eq" ^ purify_name false lower s - else purify_name false lower s; - -val purify_sym = purify_base false; +fun purify_base "op &" = "and" + | purify_base "op |" = "or" + | purify_base "op -->" = "implies" + | purify_base "op :" = "member" + | purify_base "*" = "product" + | purify_base "+" = "sum" + | purify_base s = if String.isPrefix "op =" s + then "eq" ^ purify_name false s + else purify_name false s; fun check_modulename mn = let val mns = Long_Name.explode mn; - val mns' = map (purify_name true false) mns; + val mns' = map (purify_name true) mns; in if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n" ^ "perhaps try " ^ quote (Long_Name.implode mns')) end; -(** variable name contexts **) - -type var_ctxt = string Symtab.table * Name.context; - -fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty, - Name.make_context names); - -fun intro_vars names (namemap, namectxt) = - let - val (names', namectxt') = Name.variants names namectxt; - val namemap' = fold2 (curry Symtab.update) names names' namemap; - in (namemap', namectxt') end; - -fun lookup_var (namemap, _) name = case Symtab.lookup namemap name - of SOME name' => name' - | NONE => error ("Invalid name in context: " ^ quote name); - - (** misc **) fun read_const_exprs thy = @@ -150,22 +101,4 @@ else ([Code_Unit.read_const thy s], []); in pairself flat o split_list o map read_const_expr end; -fun mk_name_module reserved_names module_prefix module_alias program = - let - fun mk_alias name = case module_alias name - of SOME name' => name' - | NONE => name - |> Long_Name.explode - |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names)) - |> Long_Name.implode; - fun mk_prefix name = case module_prefix - of SOME module_prefix => Long_Name.append module_prefix name - | NONE => name; - val tab = - Symtab.empty - |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name)) - o fst o dest_name o fst) - program - in the o Symtab.lookup tab end; - end; diff -r d26ad4576d5c -r 94b74365ceb9 src/Tools/code/code_printer.ML --- a/src/Tools/code/code_printer.ML Sun Mar 22 21:30:21 2009 +0100 +++ b/src/Tools/code/code_printer.ML Sun Mar 22 21:48:14 2009 +0100 @@ -16,6 +16,13 @@ val semicolon: Pretty.T list -> Pretty.T val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T + val first_upper: string -> string + val first_lower: string -> string + type var_ctxt + val make_vars: string list -> var_ctxt + val intro_vars: string list -> var_ctxt -> var_ctxt + val lookup_var: var_ctxt -> string -> string + type lrx val L: lrx val R: lrx @@ -42,14 +49,14 @@ -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T) -> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option - val gen_pr_app: (thm -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list) - -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T) + val gen_pr_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list) + -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T) -> (string -> const_syntax option) -> Code_Thingol.naming - -> thm -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T + -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T) - -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T) + -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T) -> thm -> fixity - -> (string option * iterm option) * itype -> Code_Name.var_ctxt -> Pretty.T * Code_Name.var_ctxt + -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt type literals val Literals: { literal_char: string -> string, literal_string: string -> string, @@ -60,6 +67,10 @@ val literal_numeral: literals -> bool -> int -> string val literal_list: literals -> Pretty.T list -> Pretty.T val infix_cons: literals -> int * string + + val mk_name_module: Name.context -> string option -> (string -> string option) + -> 'a Graph.T -> string -> string + val dest_name: string -> string * string end; structure Code_Printer : CODE_PRINTER = @@ -83,6 +94,27 @@ | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs; +(** names and variable name contexts **) + +type var_ctxt = string Symtab.table * Name.context; + +fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty, + Name.make_context names); + +fun intro_vars names (namemap, namectxt) = + let + val (names', namectxt') = Name.variants names namectxt; + val namemap' = fold2 (curry Symtab.update) names names' namemap; + in (namemap', namectxt') end; + +fun lookup_var (namemap, _) name = case Symtab.lookup namemap name + of SOME name' => name' + | NONE => error ("Invalid name in context: " ^ quote name); + +val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; +val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; + + (** syntax printer **) (* binding priorities *) @@ -125,8 +157,8 @@ type tyco_syntax = int * ((fixity -> itype -> Pretty.T) -> fixity -> itype list -> Pretty.T); -type const_syntax = int * ((Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T) - -> Code_Thingol.naming -> thm -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T); +type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T) + -> Code_Thingol.naming -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T); fun simple_const_syntax x = (Option.map o apsnd) (fn pretty => fn pr => fn naming => fn thm => fn vars => pretty (pr vars)) x; @@ -150,9 +182,9 @@ val vs = case pat of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat [] | NONE => []; - val vars' = Code_Name.intro_vars (the_list v) vars; - val vars'' = Code_Name.intro_vars vs vars'; - val v' = Option.map (Code_Name.lookup_var vars') v; + val vars' = intro_vars (the_list v) vars; + val vars'' = intro_vars vs vars'; + val v' = Option.map (lookup_var vars') v; val pat' = Option.map (pr_term thm vars'' fxy) pat; in (pr_bind ((v', pat'), ty), vars'') end; @@ -239,4 +271,28 @@ val literal_list = #literal_list o dest_Literals; val infix_cons = #infix_cons o dest_Literals; + +(** module name spaces **) + +val dest_name = + apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode; + +fun mk_name_module reserved_names module_prefix module_alias program = + let + fun mk_alias name = case module_alias name + of SOME name' => name' + | NONE => name + |> Long_Name.explode + |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names)) + |> Long_Name.implode; + fun mk_prefix name = case module_prefix + of SOME module_prefix => Long_Name.append module_prefix name + | NONE => name; + val tab = + Symtab.empty + |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name)) + o fst o dest_name o fst) + program + in the o Symtab.lookup tab end; + end; (*struct*) diff -r d26ad4576d5c -r 94b74365ceb9 src/Tools/code/code_target.ML --- a/src/Tools/code/code_target.ML Sun Mar 22 21:30:21 2009 +0100 +++ b/src/Tools/code/code_target.ML Sun Mar 22 21:48:14 2009 +0100 @@ -82,11 +82,9 @@ (** theory data **) -structure StringPairTab = Code_Name.StringPairTab; - datatype name_syntax_table = NameSyntaxTable of { class: string Symtab.table, - instance: unit StringPairTab.table, + instance: unit Symreltab.table, tyco: tyco_syntax Symtab.table, const: const_syntax Symtab.table }; @@ -99,7 +97,7 @@ NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) = mk_name_syntax_table ( (Symtab.join (K snd) (class1, class2), - StringPairTab.join (K snd) (instance1, instance2)), + Symreltab.join (K snd) (instance1, instance2)), (Symtab.join (K snd) (tyco1, tyco2), Symtab.join (K snd) (const1, const2)) ); @@ -194,7 +192,7 @@ thy |> (CodeTargetData.map o apfst oo Symtab.map_default) (target, mk_target ((serial (), seri), (([], Symtab.empty), - (mk_name_syntax_table ((Symtab.empty, StringPairTab.empty), (Symtab.empty, Symtab.empty)), + (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)), Symtab.empty)))) ((map_target o apfst o apsnd o K) seri) end; @@ -262,11 +260,11 @@ in if add_del then thy |> (map_name_syntax target o apfst o apsnd) - (StringPairTab.update (inst, ())) + (Symreltab.update (inst, ())) else thy |> (map_name_syntax target o apfst o apsnd) - (StringPairTab.delete_safe inst) + (Symreltab.delete_safe inst) end; fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy = @@ -407,7 +405,7 @@ |>> map_filter I; val (names_class, class') = distill_names Code_Thingol.lookup_class class; val names_inst = map_filter (Code_Thingol.lookup_instance naming) - (StringPairTab.keys instance); + (Symreltab.keys instance); val (names_tyco, tyco') = distill_names Code_Thingol.lookup_tyco tyco; val (names_const, const') = distill_names Code_Thingol.lookup_const const; val names_hidden = names_class @ names_inst @ names_tyco @ names_const; diff -r d26ad4576d5c -r 94b74365ceb9 src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Sun Mar 22 21:30:21 2009 +0100 +++ b/src/Tools/code/code_thingol.ML Sun Mar 22 21:48:14 2009 +0100 @@ -242,7 +242,7 @@ fun namify thy get_basename get_thyname name = let val prefix = get_thyname thy name; - val base = (Code_Name.purify_base true o get_basename) name; + val base = (Code_Name.purify_base o get_basename) name; in Long_Name.append prefix base end; in @@ -261,13 +261,11 @@ (* data *) -structure StringPairTab = Code_Name.StringPairTab; - datatype naming = Naming of { class: class Symtab.table * Name.context, - classrel: string StringPairTab.table * Name.context, + classrel: string Symreltab.table * Name.context, tyco: string Symtab.table * Name.context, - instance: string StringPairTab.table * Name.context, + instance: string Symreltab.table * Name.context, const: string Symtab.table * Name.context } @@ -275,9 +273,9 @@ val empty_naming = Naming { class = (Symtab.empty, Name.context), - classrel = (StringPairTab.empty, Name.context), + classrel = (Symreltab.empty, Name.context), tyco = (Symtab.empty, Name.context), - instance = (StringPairTab.empty, Name.context), + instance = (Symreltab.empty, Name.context), const = (Symtab.empty, Name.context) }; @@ -334,22 +332,22 @@ val lookup_class = add_suffix suffix_class oo Symtab.lookup o fst o #class o dest_Naming; val lookup_classrel = add_suffix suffix_classrel - oo StringPairTab.lookup o fst o #classrel o dest_Naming; + oo Symreltab.lookup o fst o #classrel o dest_Naming; val lookup_tyco = add_suffix suffix_tyco oo Symtab.lookup o fst o #tyco o dest_Naming; val lookup_instance = add_suffix suffix_instance - oo StringPairTab.lookup o fst o #instance o dest_Naming; + oo Symreltab.lookup o fst o #instance o dest_Naming; val lookup_const = add_suffix suffix_const oo Symtab.lookup o fst o #const o dest_Naming; fun declare_class thy = declare thy map_class lookup_class Symtab.update_new namify_class; fun declare_classrel thy = declare thy map_classrel - lookup_classrel StringPairTab.update_new namify_classrel; + lookup_classrel Symreltab.update_new namify_classrel; fun declare_tyco thy = declare thy map_tyco lookup_tyco Symtab.update_new namify_tyco; fun declare_instance thy = declare thy map_instance - lookup_instance StringPairTab.update_new namify_instance; + lookup_instance Symreltab.update_new namify_instance; fun declare_const thy = declare thy map_const lookup_const Symtab.update_new namify_const;