--- a/NEWS Thu Dec 05 19:44:53 2024 +0100
+++ b/NEWS Fri Dec 06 21:27:07 2024 +0100
@@ -119,6 +119,10 @@
unbundle no datatype_record_syntax
+* Printing of constants and bound variables is more careful to avoid
+free variables, and fixed variables with mixfix syntax (including
+'structure'). Rare INCOMPATIBILITY, e.g. in "subgoal_tac", "rule_tac".
+
*** Isabelle/jEdit Prover IDE ***
@@ -241,6 +245,17 @@
*** ML ***
+* Term.variant_bounds replaces former Term.variant_frees for logical
+manipulation of terms, without inner-syntax operations (e.g. reading a
+term in the context of goal parameters). In contrast, former
+Term.variant_frees made some attempts to work with constants as well,
+but without taking the formal name space or abbreviations into account.
+The existing operations Logic.goal_params, Logic.concl_of_goal,
+Logic.prems_of_goal are now based on Term.variant_bounds, and thus
+change their semantics silently! Rare INCOMPATIBILITY, better use
+Variable.variant_names or Variable.focus_params, instead of
+Logic.goal_params etc.
+
* Antiquotation \<^bundle>\<open>name\<close> inlines a formally checked bundle name.
* The new operation Pattern.rewrite_term_yoyo alternates top-down,
--- a/src/FOL/IFOL.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/FOL/IFOL.thy Fri Dec 06 21:27:07 2024 +0100
@@ -105,7 +105,7 @@
syntax_consts "_Uniq" \<rightleftharpoons> Uniq
translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
typed_print_translation \<open>
- [(\<^const_syntax>\<open>Uniq\<close>, fn _ => Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Uniq\<close>)]
+ [(\<^const_syntax>\<open>Uniq\<close>, Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Uniq\<close>)]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
--- a/src/HOL/Auth/Guard/Proto.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy Fri Dec 06 21:27:07 2024 +0100
@@ -464,7 +464,7 @@
apply (frule Guard_safe, simp)
apply (frule Crypt_guard_invKey, simp)
apply (frule ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.b" in Crypt_guard_invKey, simp)
apply (frule_tac R=ns1 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
apply (simp add: secret_def, simp add: secret_def, force, force)
apply (simp add: secret_def keys_def, blast)
@@ -475,7 +475,7 @@
apply (frule Guard_safe, simp)
apply (frule Crypt_guard_invKey, simp)
apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.a" in Crypt_guard_invKey, simp)
apply (frule_tac R=ns1 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
apply (simp add: secret_def, simp add: secret_def, force, force)
apply (simp add: secret_def, rule No_Nonce, simp)
@@ -493,7 +493,7 @@
apply (frule Guard_safe, simp)
apply (frule Crypt_guard_invKey, simp)
apply (frule ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.b" in Crypt_guard_invKey, simp)
apply (frule_tac R=ns2 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
apply (simp add: secret_def, simp add: secret_def, force, force)
apply (simp add: secret_def, rule No_Nonce, simp)
@@ -503,7 +503,7 @@
apply (frule Guard_safe, simp)
apply (frule Crypt_guard_invKey, simp)
apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.a" in Crypt_guard_invKey, simp)
apply (frule_tac R=ns2 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
apply (simp add: secret_def, simp add: secret_def, force, force)
apply (simp add: secret_def keys_def, blast)
--- a/src/HOL/HOL.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/HOL.thy Fri Dec 06 21:27:07 2024 +0100
@@ -135,7 +135,7 @@
translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
typed_print_translation \<open>
- [(\<^const_syntax>\<open>Uniq\<close>, fn _ => Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Uniq\<close>)]
+ [(\<^const_syntax>\<open>Uniq\<close>, Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Uniq\<close>)]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
@@ -150,7 +150,7 @@
translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)"
typed_print_translation \<open>
- [(\<^const_syntax>\<open>Ex1\<close>, fn _ => Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Ex1\<close>)]
+ [(\<^const_syntax>\<open>Ex1\<close>, Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Ex1\<close>)]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
@@ -183,8 +183,8 @@
syntax_consts "_The" \<rightleftharpoons> The
translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
print_translation \<open>
- [(\<^const_syntax>\<open>The\<close>, fn _ => fn [Abs abs] =>
- let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
+ [(\<^const_syntax>\<open>The\<close>, fn ctxt => fn [Abs abs] =>
+ let val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs
in Syntax.const \<^syntax_const>\<open>_The\<close> $ x $ t end)]
\<close> \<comment> \<open>To avoid eta-contraction of body\<close>
--- a/src/HOL/HOLCF/Cfun.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/HOLCF/Cfun.thy Fri Dec 06 21:27:07 2024 +0100
@@ -39,8 +39,8 @@
\<close>
print_translation \<open>
- [(\<^const_syntax>\<open>Abs_cfun\<close>, fn _ => fn [Abs abs] =>
- let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
+ [(\<^const_syntax>\<open>Abs_cfun\<close>, fn ctxt => fn [Abs abs] =>
+ let val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs
in Syntax.const \<^syntax_const>\<open>_cabs\<close> $ x $ t end)]
\<close> \<comment> \<open>To avoid eta-contraction of body\<close>
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Dec 06 21:27:07 2024 +0100
@@ -142,29 +142,29 @@
print_translation \<open>
let
- fun dest_LAM (Const (\<^const_syntax>\<open>Rep_cfun\<close>,_) $ Const (\<^const_syntax>\<open>unit_when\<close>,_) $ t) =
+ fun dest_LAM _ (Const (\<^const_syntax>\<open>Rep_cfun\<close>,_) $ Const (\<^const_syntax>\<open>unit_when\<close>,_) $ t) =
(Syntax.const \<^syntax_const>\<open>_noargs\<close>, t)
- | dest_LAM (Const (\<^const_syntax>\<open>Rep_cfun\<close>,_) $ Const (\<^const_syntax>\<open>csplit\<close>,_) $ t) =
+ | dest_LAM ctxt (Const (\<^const_syntax>\<open>Rep_cfun\<close>,_) $ Const (\<^const_syntax>\<open>csplit\<close>,_) $ t) =
let
- val (v1, t1) = dest_LAM t;
- val (v2, t2) = dest_LAM t1;
+ val (v1, t1) = dest_LAM ctxt t;
+ val (v2, t2) = dest_LAM ctxt t1;
in (Syntax.const \<^syntax_const>\<open>_args\<close> $ v1 $ v2, t2) end
- | dest_LAM (Const (\<^const_syntax>\<open>Abs_cfun\<close>,_) $ t) =
+ | dest_LAM ctxt (Const (\<^const_syntax>\<open>Abs_cfun\<close>,_) $ t) =
let
val abs =
case t of Abs abs => abs
| _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
- val (x, t') = Syntax_Trans.atomic_abs_tr' abs;
+ val (x, t') = Syntax_Trans.atomic_abs_tr' ctxt abs;
in (Syntax.const \<^syntax_const>\<open>_variable\<close> $ x, t') end
- | dest_LAM _ = raise Match; (* too few vars: abort translation *)
+ | dest_LAM _ _ = raise Match; (* too few vars: abort translation *)
- fun Case1_tr' [Const(\<^const_syntax>\<open>branch\<close>,_) $ p, r] =
- let val (v, t) = dest_LAM r in
+ fun Case1_tr' ctxt [Const(\<^const_syntax>\<open>branch\<close>,_) $ p, r] =
+ let val (v, t) = dest_LAM ctxt r in
Syntax.const \<^syntax_const>\<open>_Case1\<close> $
(Syntax.const \<^syntax_const>\<open>_match\<close> $ p $ v) $ t
end;
- in [(\<^const_syntax>\<open>Rep_cfun\<close>, K Case1_tr')] end
+ in [(\<^const_syntax>\<open>Rep_cfun\<close>, Case1_tr')] end
\<close>
translations
--- a/src/HOL/Hilbert_Choice.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Hilbert_Choice.thy Fri Dec 06 21:27:07 2024 +0100
@@ -29,8 +29,8 @@
"SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
print_translation \<open>
- [(\<^const_syntax>\<open>Eps\<close>, fn _ => fn [Abs abs] =>
- let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
+ [(\<^const_syntax>\<open>Eps\<close>, fn ctxt => fn [Abs abs] =>
+ let val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs
in Syntax.const \<^syntax_const>\<open>_Eps\<close> $ x $ t end)]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Fri Dec 06 21:27:07 2024 +0100
@@ -117,11 +117,11 @@
apply simp
apply clarify
apply simp
- apply(subgoal_tac "xa=0")
+ apply(subgoal_tac "x=0")
apply simp
apply arith
apply clarify
- apply(case_tac xaa, simp, simp)
+ apply(case_tac xa, simp, simp)
apply clarify
apply simp
apply(erule_tac x=0 in all_dupE)
--- a/src/HOL/Library/FSet.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Library/FSet.thy Fri Dec 06 21:27:07 2024 +0100
@@ -216,8 +216,8 @@
"\<exists>!x|\<in>|A. P" \<rightharpoonup> "\<exists>!x. x |\<in>| A \<and> P"
typed_print_translation \<open>
- [(\<^const_syntax>\<open>fBall\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_fBall\<close>),
- (\<^const_syntax>\<open>fBex\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_fBex\<close>)]
+ [(\<^const_syntax>\<open>fBall\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_fBall\<close>),
+ (\<^const_syntax>\<open>fBex\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_fBex\<close>)]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
syntax
--- a/src/HOL/Library/Multiset.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Dec 06 21:27:07 2024 +0100
@@ -181,8 +181,8 @@
"\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
typed_print_translation \<open>
- [(\<^const_syntax>\<open>Multiset.Ball\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_MBall\<close>),
- (\<^const_syntax>\<open>Multiset.Bex\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_MBex\<close>)]
+ [(\<^const_syntax>\<open>Multiset.Ball\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_MBall\<close>),
+ (\<^const_syntax>\<open>Multiset.Bex\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_MBex\<close>)]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
lemma count_eq_zero_iff:
--- a/src/HOL/Library/conditional_parametricity.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Library/conditional_parametricity.ML Fri Dec 06 21:27:07 2024 +0100
@@ -246,7 +246,7 @@
val i = maxidx_of_term t + 1;
fun tvar_to_tfree ((name, _), sort) = (name, sort);
val tvars = Term.add_tvars t [];
- val new_frees = map TFree (Term.variant_frees t (map tvar_to_tfree tvars));
+ val new_frees = map TFree (Term.variant_bounds t (map tvar_to_tfree tvars));
val u = subst_atomic_types ((map TVar tvars) ~~ new_frees) t;
val T = fastype_of t;
val U = fastype_of u;
--- a/src/HOL/Library/refute.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Library/refute.ML Fri Dec 06 21:27:07 2024 +0100
@@ -1186,7 +1186,7 @@
(a, T) :: strip_all_vars t
| strip_all_vars _ = [] : (string * typ) list
val strip_t = strip_all_body ex_closure
- val frees = Term.variant_frees strip_t (strip_all_vars ex_closure)
+ val frees = Term.variant_bounds strip_t (strip_all_vars ex_closure)
val subst_t = Term.subst_bounds (map Free (rev frees), strip_t)
in
find_model ctxt (actual_params ctxt params) assm_ts subst_t true
--- a/src/HOL/Nominal/Examples/Class2.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Nominal/Examples/Class2.thy Fri Dec 06 21:27:07 2024 +0100
@@ -4671,7 +4671,7 @@
apply(drule_tac pi="[(x,za)]" and x="(x):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
-apply(drule_tac pi="[(x,za)]" and x="(x):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,za)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(drule_tac pi="[(x,za)]" and x="(x):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
@@ -4679,17 +4679,17 @@
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "x=ya")
apply(simp)
-apply(drule_tac pi="[(ya,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(ya,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(case_tac "za=ya")
apply(simp)
-apply(drule_tac pi="[(x,ya)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,ya)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
-apply(drule_tac pi="[(x,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "x=xa")
@@ -4707,7 +4707,7 @@
apply(drule_tac pi="[(x,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
-apply(drule_tac pi="[(x,za)]" and x="(x):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,za)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "x=xa")
@@ -4727,17 +4727,17 @@
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "x=ya")
apply(simp)
-apply(drule_tac pi="[(ya,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(ya,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(case_tac "za=ya")
apply(simp)
-apply(drule_tac pi="[(x,ya)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,ya)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
-apply(drule_tac pi="[(x,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
done
@@ -4800,7 +4800,7 @@
apply(drule_tac pi="[(x,y)]" and x="<aa>:Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
-apply(drule_tac pi="[(x,y)]" and x="(x):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,y)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(drule_tac pi="[(x,y)]" and x="<aa>:Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
@@ -4808,17 +4808,17 @@
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "x=xa")
apply(simp)
-apply(drule_tac pi="[(xa,y)]" and x="(xa):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(xa,y)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(case_tac "y=xa")
apply(simp)
-apply(drule_tac pi="[(x,xa)]" and x="(xa):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,xa)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
-apply(drule_tac pi="[(x,y)]" and x="(xa):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,y)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
done
--- a/src/HOL/Nominal/nominal_inductive.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Dec 06 21:27:07 2024 +0100
@@ -245,7 +245,7 @@
if null (preds_of ps prem) then prem
else lift_prem prem) prems,
HOLogic.mk_Trueprop (lift_pred p ts));
- val vs = map (Var o apfst (rpair 0)) (Term.variant_frees prem params')
+ val vs = map (Var o apfst (rpair 0)) (Term.variant_bounds prem params')
in
(Logic.list_all (params', prem), (vs, subst_bounds (rev vs, prem)))
end) prems);
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Dec 06 21:27:07 2024 +0100
@@ -146,7 +146,7 @@
in Option.map prove (map_term f prop (the_default prop opt)) end;
fun abs_params params t =
- let val vs = map (Var o apfst (rpair 0)) (Term.variant_frees t params)
+ let val vs = map (Var o apfst (rpair 0)) (Term.variant_bounds t params)
in (Logic.list_all (params, t), (vs, subst_bounds (rev vs, t))) end;
fun inst_params thy (vs, p) th cts =
--- a/src/HOL/Nominal/nominal_primrec.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Fri Dec 06 21:27:07 2024 +0100
@@ -156,7 +156,7 @@
let
val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs);
val rargs = map (rpair dummyT o fst o fst) recs;
- val subs = Term.variant_frees rhs rargs;
+ val subs = Term.variant_bounds rhs rargs;
val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
(Free x, (Old_Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss')
handle RecError s => primrec_eq_err lthy s eq
--- a/src/HOL/Probability/Probability_Measure.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Fri Dec 06 21:27:07 2024 +0100
@@ -283,7 +283,7 @@
end
| unnest_tuples pat = pat
- fun tr' [sig_alg, Const (\<^const_syntax>\<open>Collect\<close>, _) $ t] =
+ fun tr' ctxt [sig_alg, Const (\<^const_syntax>\<open>Collect\<close>, _) $ t] =
let
val bound_dummyT = Const (\<^syntax_const>\<open>_bound\<close>, dummyT)
@@ -300,7 +300,7 @@
end
| go pattern elem (Abs abs) =
let
- val (x as (_ $ tx), t) = Syntax_Trans.atomic_abs_tr' abs
+ val (x as (_ $ tx), t) = Syntax_Trans.atomic_abs_tr' ctxt abs
in
go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t
end
@@ -313,7 +313,7 @@
go [] [] t
end
in
- [(\<^const_syntax>\<open>Sigma_Algebra.measure\<close>, K tr')]
+ [(\<^const_syntax>\<open>Sigma_Algebra.measure\<close>, tr')]
end
\<close>
--- a/src/HOL/Product_Type.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Product_Type.thy Fri Dec 06 21:27:07 2024 +0100
@@ -315,34 +315,34 @@
typed_print_translation \<open>
let
- fun case_prod_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
- | case_prod_guess_names_tr' T [Abs (x, xT, t)] =
+ fun case_prod_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
+ | case_prod_guess_names_tr' ctxt T [Abs (x, xT, t)] =
(case (head_of t) of
Const (\<^const_syntax>\<open>case_prod\<close>, _) => raise Match
| _ =>
let
val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
- val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
- val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
+ val (y, t') = Syntax_Trans.atomic_abs_tr' ctxt ("y", yT, incr_boundvars 1 t $ Bound 0);
+ val (x', t'') = Syntax_Trans.atomic_abs_tr' ctxt (x, xT, t');
in
Syntax.const \<^syntax_const>\<open>_abs\<close> $
(Syntax.const \<^syntax_const>\<open>_pattern\<close> $ x' $ y) $ t''
end)
- | case_prod_guess_names_tr' T [t] =
+ | case_prod_guess_names_tr' ctxt T [t] =
(case head_of t of
Const (\<^const_syntax>\<open>case_prod\<close>, _) => raise Match
| _ =>
let
val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
val (y, t') =
- Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
- val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
+ Syntax_Trans.atomic_abs_tr' ctxt ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
+ val (x', t'') = Syntax_Trans.atomic_abs_tr' ctxt ("x", xT, t');
in
Syntax.const \<^syntax_const>\<open>_abs\<close> $
(Syntax.const \<^syntax_const>\<open>_pattern\<close> $ x' $ y) $ t''
end)
- | case_prod_guess_names_tr' _ _ = raise Match;
- in [(\<^const_syntax>\<open>case_prod\<close>, K case_prod_guess_names_tr')] end
+ | case_prod_guess_names_tr' _ _ _ = raise Match;
+ in [(\<^const_syntax>\<open>case_prod\<close>, case_prod_guess_names_tr')] end
\<close>
text \<open>Reconstruct pattern from (nested) \<^const>\<open>case_prod\<close>s,
@@ -351,39 +351,39 @@
print_translation \<open>
let
- fun case_prod_tr' [Abs (x, T, t as (Abs abs))] =
+ fun case_prod_tr' ctxt [Abs (x, T, t as (Abs abs))] =
(* case_prod (\<lambda>x y. t) \<Rightarrow> \<lambda>(x, y) t *)
let
- val (y, t') = Syntax_Trans.atomic_abs_tr' abs;
- val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
+ val (y, t') = Syntax_Trans.atomic_abs_tr' ctxt abs;
+ val (x', t'') = Syntax_Trans.atomic_abs_tr' ctxt (x, T, t');
in
Syntax.const \<^syntax_const>\<open>_abs\<close> $
(Syntax.const \<^syntax_const>\<open>_pattern\<close> $ x' $ y) $ t''
end
- | case_prod_tr' [Abs (x, T, (s as Const (\<^const_syntax>\<open>case_prod\<close>, _) $ t))] =
+ | case_prod_tr' ctxt [Abs (x, T, (s as Const (\<^const_syntax>\<open>case_prod\<close>, _) $ t))] =
(* case_prod (\<lambda>x. (case_prod (\<lambda>y z. t))) \<Rightarrow> \<lambda>(x, y, z). t *)
let
val Const (\<^syntax_const>\<open>_abs\<close>, _) $
(Const (\<^syntax_const>\<open>_pattern\<close>, _) $ y $ z) $ t' =
- case_prod_tr' [t];
- val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
+ case_prod_tr' ctxt [t];
+ val (x', t'') = Syntax_Trans.atomic_abs_tr' ctxt (x, T, t');
in
Syntax.const \<^syntax_const>\<open>_abs\<close> $
(Syntax.const \<^syntax_const>\<open>_pattern\<close> $ x' $
(Syntax.const \<^syntax_const>\<open>_patterns\<close> $ y $ z)) $ t''
end
- | case_prod_tr' [Const (\<^const_syntax>\<open>case_prod\<close>, _) $ t] =
+ | case_prod_tr' ctxt [Const (\<^const_syntax>\<open>case_prod\<close>, _) $ t] =
(* case_prod (case_prod (\<lambda>x y z. t)) \<Rightarrow> \<lambda>((x, y), z). t *)
- case_prod_tr' [(case_prod_tr' [t])]
+ case_prod_tr' ctxt [(case_prod_tr' ctxt [t])]
(* inner case_prod_tr' creates next pattern *)
- | case_prod_tr' [Const (\<^syntax_const>\<open>_abs\<close>, _) $ x_y $ Abs abs] =
+ | case_prod_tr' ctxt [Const (\<^syntax_const>\<open>_abs\<close>, _) $ x_y $ Abs abs] =
(* case_prod (\<lambda>pttrn z. t) \<Rightarrow> \<lambda>(pttrn, z). t *)
- let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in
+ let val (z, t) = Syntax_Trans.atomic_abs_tr' ctxt abs in
Syntax.const \<^syntax_const>\<open>_abs\<close> $
(Syntax.const \<^syntax_const>\<open>_pattern\<close> $ x_y $ z) $ t
end
- | case_prod_tr' _ = raise Match;
- in [(\<^const_syntax>\<open>case_prod\<close>, K case_prod_tr')] end
+ | case_prod_tr' _ _ = raise Match;
+ in [(\<^const_syntax>\<open>case_prod\<close>, case_prod_tr')] end
\<close>
--- a/src/HOL/Set.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Set.thy Fri Dec 06 21:27:07 2024 +0100
@@ -324,8 +324,8 @@
\<close>
typed_print_translation \<open>
- [(\<^const_syntax>\<open>Ball\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Ball\<close>),
- (\<^const_syntax>\<open>Bex\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Bex\<close>)]
+ [(\<^const_syntax>\<open>Ball\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Ball\<close>),
+ (\<^const_syntax>\<open>Bex\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Bex\<close>)]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
print_translation \<open>
@@ -348,7 +348,7 @@
if check (P, 0) then tr' P
else
let
- val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs;
+ val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' ctxt abs;
val M = Syntax.const \<^syntax_const>\<open>_Coll\<close> $ x $ t;
in
case t of
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Dec 06 21:27:07 2024 +0100
@@ -391,10 +391,10 @@
|> map_filter (try (apsnd (fn Nested_Rec p => p)));
fun ensure_unique frees t =
- if member (op =) frees t then Free (the_single (Term.variant_frees t [dest_Free t])) else t;
+ if member (op =) frees t then Free (the_single (Term.variant_bounds t [dest_Free t])) else t;
val args = replicate n_args ("", dummyT)
- |> Term.variant_frees t
+ |> Term.variant_bounds t
|> rev
|> map Free
|> fold (fn (ctr_arg_idx, (arg_idx, _)) =>
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Fri Dec 06 21:27:07 2024 +0100
@@ -477,7 +477,7 @@
map (pair "x") (drop j (take i (binder_types (fastype_of t)))), [])
else chop i zs;
val u = fold_rev Term.abs ys (strip_abs_body t);
- val xs' = map Free (Name.variant_names (Term.declare_term_names u used) xs);
+ val xs' = map Free (Name.variant_names (Term.declare_free_names u used) xs);
val (xs1, xs2) = chop j xs'
in (xs', list_comb (subst_bounds (rev xs1, u), xs2)) end;
fun is_dependent i t =
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Fri Dec 06 21:27:07 2024 +0100
@@ -149,7 +149,7 @@
let
val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs);
val rargs = map (rpair dummyT o fst o fst) recs;
- val subs = Term.variant_frees rhs rargs;
+ val subs = Term.variant_bounds rhs rargs;
val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
(Free x, (Old_Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss')
handle PrimrecError (s, NONE) => primrec_error_eqn s eq
--- a/src/Provers/preorder.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Provers/preorder.ML Fri Dec 06 21:27:07 2024 +0100
@@ -555,7 +555,7 @@
fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
val thy = Proof_Context.theory_of ctxt;
- val rfrees = map Free (rev (Term.variant_frees A (Logic.strip_params A)));
+ val rfrees = map Free (rev (Term.variant_bounds A (Logic.strip_params A)));
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
val lesss = flat (map_index (mkasm_trans thy o swap) Hs);
@@ -578,7 +578,7 @@
fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
val thy = Proof_Context.theory_of ctxt
- val rfrees = map Free (rev (Term.variant_frees A (Logic.strip_params A)));
+ val rfrees = map Free (rev (Term.variant_bounds A (Logic.strip_params A)));
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
val lesss = flat (map_index (mkasm_quasi thy o swap) Hs);
--- a/src/Pure/General/name_space.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/General/name_space.ML Fri Dec 06 21:27:07 2024 +0100
@@ -28,7 +28,7 @@
val names_long: bool Config.T
val names_short: bool Config.T
val names_unique: bool Config.T
- val extern_generic: Context.generic -> T -> string -> xstring
+ val extern_if: (xstring -> bool) -> Proof.context -> T -> string -> xstring
val extern: Proof.context -> T -> string -> xstring
val extern_ord: Proof.context -> T -> string ord
val extern_shortest: Proof.context -> T -> string -> xstring
@@ -292,16 +292,17 @@
val names_short = Config.declare_option_bool ("names_short", \<^here>);
val names_unique = Config.declare_option_bool ("names_unique", \<^here>);
-fun extern_generic context space name =
+fun extern_if ok ctxt space name =
let
- val names_long = Config.get_generic context names_long;
- val names_short = Config.get_generic context names_short;
- val names_unique = Config.get_generic context names_unique;
+ val names_long = Config.get ctxt names_long;
+ val names_short = Config.get ctxt names_short;
+ val names_unique = Config.get ctxt names_unique;
fun extern_chunks require_unique a chunks =
let val {full_name = c, unique, ...} = intern_chunks space chunks in
- if (not require_unique orelse unique) andalso is_alias space c a
- then SOME (Long_Name.implode_chunks chunks)
+ if (not require_unique orelse unique) andalso is_alias space c a then
+ let val x = Long_Name.implode_chunks chunks
+ in if ok x then SOME x else NONE end
else NONE
end;
@@ -322,7 +323,7 @@
else extern_names (get_aliases space name)
end;
-val extern = extern_generic o Context.Proof;
+val extern = extern_if (K true);
fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space);
--- a/src/Pure/General/table.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/General/table.ML Fri Dec 06 21:27:07 2024 +0100
@@ -68,6 +68,7 @@
val make_set: key list -> set
type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int}
val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
+ val apply_unsynchronized_cache: (key -> 'a) -> key -> 'a
end;
functor Table(Key: KEY): TABLE =
@@ -610,6 +611,8 @@
fun total_size () = size (! cache1) + size (! cache2);
in {apply = apply, reset = reset, size = total_size} end;
+fun apply_unsynchronized_cache f = #apply (unsynchronized_cache f);
+
(* ML pretty-printing *)
--- a/src/Pure/Isar/expression.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/Isar/expression.ML Fri Dec 06 21:27:07 2024 +0100
@@ -66,7 +66,7 @@
(** Internalise locale names in expr **)
-fun check_expr thy instances = map (apfst (Locale.check thy)) instances;
+fun check_expr ctxt instances = map (apfst (Locale.check ctxt)) instances;
(** Parameters of expression **)
@@ -378,7 +378,7 @@
let
val thy = Proof_Context.theory_of ctxt1;
- val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
+ val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr ctxt1) raw_import);
fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) =
let
--- a/src/Pure/Isar/interpretation.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/Isar/interpretation.ML Fri Dec 06 21:27:07 2024 +0100
@@ -215,7 +215,7 @@
gen_global_sublocale (K I) cert_interpretation expression;
fun global_sublocale_cmd raw_expression =
- gen_global_sublocale Locale.check read_interpretation raw_expression;
+ gen_global_sublocale Locale.check_global read_interpretation raw_expression;
end;
--- a/src/Pure/Isar/locale.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/Isar/locale.ML Fri Dec 06 21:27:07 2024 +0100
@@ -44,8 +44,9 @@
(string * morphism) list -> theory -> theory
val locale_space: theory -> Name_Space.T
val intern: theory -> xstring -> string
- val check: theory -> xstring * Position.T -> string
- val extern: theory -> string -> xstring
+ val check_global: theory -> xstring * Position.T -> string
+ val check: Proof.context -> xstring * Position.T -> string
+ val extern: Proof.context -> string -> xstring
val markup_name: Proof.context -> string -> string
val pretty_name: Proof.context -> string -> Pretty.T
val defined: theory -> string -> bool
@@ -192,15 +193,20 @@
val locale_space = Name_Space.space_of_table o Locales.get;
val intern = Name_Space.intern o locale_space;
-fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy);
+
+fun check_global thy =
+ #1 o Name_Space.check (Context.Theory thy) (Locales.get thy);
+
+fun check ctxt =
+ #1 o Name_Space.check (Context.Proof ctxt) (Locales.get (Proof_Context.theory_of ctxt));
val _ = Theory.setup
(ML_Antiquotation.inline_embedded \<^binding>\<open>locale\<close>
- (Args.theory -- Scan.lift Parse.embedded_position >>
+ (Args.context -- Scan.lift Parse.embedded_position >>
(ML_Syntax.print_string o uncurry check)));
-fun extern thy =
- Name_Space.extern_generic (Context.Theory thy) (locale_space thy);
+fun extern ctxt =
+ Name_Space.extern ctxt (locale_space (Proof_Context.theory_of ctxt));
fun markup_extern ctxt =
Name_Space.markup_extern ctxt (locale_space (Proof_Context.theory_of ctxt));
--- a/src/Pure/Isar/proof_context.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Dec 06 21:27:07 2024 +0100
@@ -42,6 +42,9 @@
val class_space: Proof.context -> Name_Space.T
val type_space: Proof.context -> Name_Space.T
val const_space: Proof.context -> Name_Space.T
+ val lookup_free: Proof.context -> string -> string option
+ val printable_const: Proof.context -> string -> bool
+ val exclude_consts: Symset.T -> Proof.context -> Proof.context
val defs_context: Proof.context -> Defs.context
val intern_class: Proof.context -> xstring -> string
val intern_type: Proof.context -> xstring -> string
@@ -53,6 +56,8 @@
val markup_type: Proof.context -> string -> string
val pretty_type: Proof.context -> string -> Pretty.T
val extern_const: Proof.context -> string -> xstring
+ val extern_fixed: Proof.context -> string -> string
+ val extern_entity: Proof.context -> string -> string
val markup_const: Proof.context -> string -> string
val pretty_const: Proof.context -> string -> Pretty.T
val transfer: theory -> Proof.context -> Proof.context
@@ -248,7 +253,8 @@
{mode: mode, (*inner syntax mode*)
syntax: Local_Syntax.T, (*local syntax*)
tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
- consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
+ consts: Symset.T * Consts.T * Consts.T,
+ (*exclude consts, local/global consts -- local name space / abbrevs only*)
facts: Facts.T, (*local facts, based on initial global facts*)
cases: cases}; (*named case contexts*)
@@ -262,7 +268,7 @@
make_data (mode_default,
Local_Syntax.init thy,
(Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy),
- (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
+ (Symset.empty, Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
Global_Theory.facts_of thy,
empty_cases);
);
@@ -299,6 +305,8 @@
map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
(mode, syntax, tsig, f consts, facts, cases));
+fun map_local_consts f = map_consts (fn (a, b, c) => (a, f b, c));
+
fun map_facts_result f =
map_data_result (fn (mode, syntax, tsig, consts, facts, cases) =>
let val (res, facts') = f facts
@@ -323,7 +331,8 @@
fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt);
-val consts_of = #1 o #consts o rep_data;
+val exclude_consts_of = #1 o #consts o rep_data;
+val consts_of = #2 o #consts o rep_data;
val cases_of = #cases o rep_data;
@@ -351,11 +360,37 @@
val concealed = map_naming Name_Space.concealed;
+(* const vs. free *)
+
+val const_space = Consts.space_of o consts_of;
+
+fun is_const_declared ctxt x =
+ let val space = const_space ctxt
+ in Name_Space.declared space (Name_Space.intern space x) end;
+
+fun lookup_free ctxt x =
+ if Variable.is_const ctxt x then NONE
+ else
+ (case Variable.lookup_fixed ctxt x of
+ NONE =>
+ let
+ val is_const = Long_Name.is_qualified x orelse is_const_declared ctxt x;
+ val is_free_declared = is_some (Variable.default_type ctxt x);
+ in if not is_const orelse is_free_declared then SOME x else NONE end
+ | fixed => fixed);
+
+fun printable_const ctxt x =
+ is_none (lookup_free ctxt x) andalso
+ not (Symset.member (exclude_consts_of ctxt) x);
+
+fun exclude_consts names2 =
+ map_consts (fn (names1, consts, thy_consts) => (Symset.union names1 names2, consts, thy_consts));
+
+
(* name spaces *)
val class_space = Type.class_space o tsig_of;
val type_space = Type.type_space o tsig_of;
-val const_space = Consts.space_of o consts_of;
fun defs_context ctxt = (ctxt, (const_space ctxt, type_space ctxt));
@@ -365,7 +400,16 @@
fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt);
fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt);
-fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt);
+fun extern_const ctxt = Name_Space.extern_if (printable_const ctxt) ctxt (const_space ctxt);
+fun extern_fixed ctxt x = if Name.is_skolem x then Variable.revert_fixed ctxt x else x;
+
+fun extern_entity ctxt =
+ Lexicon.unmark
+ {case_class = extern_class ctxt,
+ case_type = extern_type ctxt,
+ case_const = extern_const ctxt,
+ case_fixed = extern_fixed ctxt,
+ case_default = I};
fun markup_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |-> Markup.markup;
fun markup_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |-> Markup.markup;
@@ -391,10 +435,10 @@
if Type.eq_tsig (thy_tsig, global_tsig) then tsig
else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*)
end) |>
- map_consts (fn consts as (local_consts, global_consts) =>
+ map_consts (fn consts as (exclude_consts, local_consts, global_consts) =>
let val thy_consts = Sign.consts_of thy in
if Consts.eq_consts (thy_consts, global_consts) then consts
- else (Consts.merge (local_consts, thy_consts), thy_consts) (*historic merge order*)
+ else (exclude_consts, Consts.merge (local_consts, thy_consts), thy_consts) (*historic merge order*)
end)
end;
@@ -434,7 +478,7 @@
in (markups, xname) end;
fun pretty_thm_name ctxt (name, i) =
- Facts.pretty_thm_name (Context.Proof ctxt) (facts_of_fact ctxt name) (name, i);
+ Facts.pretty_thm_name ctxt (facts_of_fact ctxt name) (name, i);
val print_thm_name = Pretty.string_of oo pretty_thm_name;
@@ -571,24 +615,28 @@
Name.reject_internal (c, ps) handle ERROR msg =>
error (msg ^ consts_completion_message ctxt (c, ps));
fun err msg = error (msg ^ Position.here_list ps);
+
+ val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
+ val const = Variable.lookup_const ctxt c;
val consts = consts_of ctxt;
- val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
+
val (t, reports) =
- (case (fixed, Variable.lookup_const ctxt c) of
- (SOME x, NONE) =>
- let
- val reports = ps
- |> filter (Context_Position.is_reported ctxt)
- |> map (fn pos => (pos, Markup.name x (Variable.markup ctxt x)));
- in (Free (x, infer_type ctxt (x, dummyT)), reports) end
- | (_, SOME d) =>
- let
- val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
- val reports = ps
- |> filter (Context_Position.is_reported ctxt)
- |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d));
- in (Const (d, T), reports) end
- | _ => Consts.check_const (Context.Proof ctxt) consts (c, ps));
+ if is_some fixed andalso is_none const then
+ let
+ val x = the fixed;
+ val reports = ps
+ |> filter (Context_Position.is_reported ctxt)
+ |> map (fn pos => (pos, Markup.name x (Variable.markup ctxt x)));
+ in (Free (x, infer_type ctxt (x, dummyT)), reports) end
+ else if is_some const then
+ let
+ val d = the const;
+ val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
+ val reports = ps
+ |> filter (Context_Position.is_reported ctxt)
+ |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d));
+ in (Const (d, T), reports) end
+ else Consts.check_const (Context.Proof ctxt) consts (c, ps);
val _ =
(case (strict, t) of
(true, Const (d, _)) =>
@@ -1206,7 +1254,7 @@
(* aliases *)
fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
-fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
+fun const_alias b c ctxt = map_local_consts (Consts.alias (naming_of ctxt) b c) ctxt;
(* local constants *)
@@ -1216,7 +1264,7 @@
fun prepT raw_T =
let val T = cert_typ ctxt raw_T
in cert_term ctxt (Const (c, T)); T end;
- in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end;
+ in ctxt |> map_local_consts (Consts.constrain (c, Option.map prepT opt_T)) end;
fun add_abbrev mode (b, raw_t) ctxt =
let
@@ -1227,12 +1275,12 @@
|> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t);
in
ctxt
- |> (map_consts o apfst) (K consts')
+ |> map_local_consts (K consts')
|> Variable.declare_term rhs
|> pair (lhs, rhs)
end;
-fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c);
+fun revert_abbrev mode c = map_local_consts (Consts.revert_abbrev mode c);
fun generic_add_abbrev mode arg =
Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg);
@@ -1471,9 +1519,9 @@
fun pretty_abbrevs verbose show_globals ctxt =
let
val space = const_space ctxt;
- val (constants, global_constants) =
- apply2 (#constants o Consts.dest) (#consts (rep_data ctxt));
- val globals = Symtab.make global_constants;
+ val (_, consts, global_consts) = #consts (rep_data ctxt);
+ val constants = #constants (Consts.dest consts);
+ val globals = Symtab.make (#constants (Consts.dest global_consts));
fun add_abbr (_, (_, NONE)) = I
| add_abbr (c, (T, SOME t)) =
if not show_globals andalso Symtab.defined globals c then I
--- a/src/Pure/Isar/subgoal.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/Isar/subgoal.ML Fri Dec 06 21:27:07 2024 +0100
@@ -171,7 +171,7 @@
val subgoal = #1 (Logic.dest_implies (Thm.prop_of st));
val subgoal_params =
map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
- |> Term.variant_frees subgoal |> map #1;
+ |> Syntax_Trans.variant_bounds ctxt subgoal |> map #1;
val n = length subgoal_params;
val m = length raw_param_specs;
--- a/src/Pure/Isar/target_context.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/Isar/target_context.ML Fri Dec 06 21:27:07 2024 +0100
@@ -25,7 +25,7 @@
fun context_begin_named_cmd raw_includes ("-", _) thy =
Named_Target.init (prep_includes thy raw_includes) "" thy
| context_begin_named_cmd raw_includes name thy =
- Named_Target.init (prep_includes thy raw_includes) (Locale.check thy name) thy;
+ Named_Target.init (prep_includes thy raw_includes) (Locale.check_global thy name) thy;
val end_named_cmd = Context.Theory o Local_Theory.exit_global;
--- a/src/Pure/Proof/extraction.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/Proof/extraction.ML Fri Dec 06 21:27:07 2024 +0100
@@ -505,6 +505,8 @@
fun extract thm_vss thy =
let
val thy' = add_syntax thy;
+ val global_ctxt = Syntax.init_pretty_global thy';
+ val print_thm_name = Global_Theory.print_thm_name global_ctxt;
val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
ExtractionData.get thy;
@@ -640,8 +642,7 @@
let
val _ = T = nullT orelse error "corr: internal error";
val _ =
- msg d ("Building correctness proof for " ^
- quote (Global_Theory.print_thm_name thy thm_name) ^
+ msg d ("Building correctness proof for " ^ quote (print_thm_name thm_name) ^
(if null vs' then ""
else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
@@ -670,8 +671,8 @@
| SOME rs => (case find vs' rs of
SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs')
| NONE => error ("corr: no realizer for instance of theorem " ^
- quote (Global_Theory.print_thm_name thy' thm_name) ^ ":\n" ^
- Syntax.string_of_term_global thy'
+ quote (print_thm_name thm_name) ^ ":\n" ^
+ Syntax.string_of_term global_ctxt
(Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))))
end
@@ -686,7 +687,7 @@
SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye),
defs)
| NONE => error ("corr: no realizer for instance of axiom " ^
- quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
+ quote s ^ ":\n" ^ Syntax.string_of_term global_ctxt (Envir.beta_norm
(Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))
end
@@ -738,7 +739,7 @@
NONE =>
let
val _ =
- msg d ("Extracting " ^ quote (Global_Theory.print_thm_name thy' thm_name) ^
+ msg d ("Extracting " ^ quote (print_thm_name thm_name) ^
(if null vs' then ""
else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
@@ -790,8 +791,8 @@
| SOME rs => (case find vs' rs of
SOME (t, _) => (subst_TVars tye' t, defs)
| NONE => error ("extr: no realizer for instance of theorem " ^
- quote (Global_Theory.print_thm_name thy' thm_name) ^ ":\n" ^
- Syntax.string_of_term_global thy' (Envir.beta_norm
+ quote (print_thm_name thm_name) ^ ":\n" ^
+ Syntax.string_of_term global_ctxt (Envir.beta_norm
(Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))))
end
@@ -803,7 +804,7 @@
case find vs' (Thm_Name.Table.lookup_list realizers (s, 0)) of
SOME (t, _) => (subst_TVars tye' t, defs)
| NONE => error ("extr: no realizer for instance of axiom " ^
- quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
+ quote s ^ ":\n" ^ Syntax.string_of_term global_ctxt (Envir.beta_norm
(Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))
end
@@ -817,7 +818,7 @@
val name = Thm.derivation_name thm;
val _ = if Thm_Name.is_empty name then error "extraction: unnamed theorem" else ();
val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
- quote (Global_Theory.print_thm_name thy' name) ^ " has no computational content")
+ quote (print_thm_name name) ^ " has no computational content")
in Proofterm.reconstruct_proof thy' prop prf end;
val defs =
--- a/src/Pure/Proof/proof_checker.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/Proof/proof_checker.ML Fri Dec 06 21:27:07 2024 +0100
@@ -72,7 +72,10 @@
end;
fun thm_of_proof thy =
- let val lookup = lookup_thm thy in
+ let
+ val global_ctxt = Syntax.init_pretty_global thy;
+ val lookup = lookup_thm thy;
+ in
fn prf =>
let
val prf_names =
@@ -96,9 +99,9 @@
if is_equal prop prop' then ()
else
error ("Duplicate use of theorem name " ^
- quote (Global_Theory.print_thm_name thy thm_name) ^ Position.here thm_pos
- ^ "\n" ^ Syntax.string_of_term_global thy prop
- ^ "\n\n" ^ Syntax.string_of_term_global thy prop');
+ quote (Global_Theory.print_thm_name global_ctxt thm_name) ^ Position.here thm_pos
+ ^ "\n" ^ Syntax.string_of_term global_ctxt prop
+ ^ "\n\n" ^ Syntax.string_of_term global_ctxt prop');
in thm_of_atom thm Ts end
| thm_of _ _ (PAxm (name, _, SOME Ts)) =
--- a/src/Pure/Pure.thy Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/Pure.thy Fri Dec 06 21:27:07 2024 +0100
@@ -1210,7 +1210,8 @@
Toplevel.keep (fn state =>
let
val thy = Toplevel.theory_of state;
- val name = Locale.check thy raw_name;
+ val ctxt = Toplevel.context_of state;
+ val name = Locale.check ctxt raw_name;
in Pretty.writeln (Locale.pretty_locale thy show_facts name) end)));
val _ =
@@ -1219,9 +1220,9 @@
(Parse.name_position >> (fn raw_name =>
Toplevel.keep (fn state =>
let
+ val thy = Toplevel.theory_of state;
val ctxt = Toplevel.context_of state;
- val thy = Toplevel.theory_of state;
- val name = Locale.check thy raw_name;
+ val name = Locale.check ctxt raw_name;
in Pretty.writeln (Locale.pretty_registrations ctxt name) end)));
val _ =
@@ -1257,12 +1258,16 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>locale_deps\<close> "visualize locale dependencies"
- (Scan.succeed
- (Toplevel.keep (Toplevel.theory_of #> (fn thy =>
+ (Scan.succeed (Toplevel.keep (fn state =>
+ let
+ val thy = Toplevel.theory_of state;
+ val ctxt = Toplevel.context_of state;
+ in
Locale.pretty_locale_deps thy
|> map (fn {name, parents, body} =>
- ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
- |> Graph_Display.display_graph_old))));
+ ((name, Graph_Display.content_node (Locale.extern ctxt name) [body]), parents))
+ |> Graph_Display.display_graph_old
+ end)));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_term_bindings\<close>
@@ -1373,10 +1378,8 @@
"print theorem dependencies (immediate non-transitive)"
(Parse.thms1 >> (fn args =>
Toplevel.keep (fn st =>
- let
- val thy = Toplevel.theory_of st;
- val ctxt = Toplevel.context_of st;
- in Pretty.writeln (Thm_Deps.pretty_thm_deps thy (Attrib.eval_thms ctxt args)) end)));
+ let val ctxt = Toplevel.context_of st
+ in Pretty.writeln (Thm_Deps.pretty_thm_deps ctxt (Attrib.eval_thms ctxt args)) end)));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>thm_oracles\<close>
--- a/src/Pure/Syntax/syntax_phases.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Dec 06 21:27:07 2024 +0100
@@ -65,15 +65,14 @@
Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps;
fun markup_entity_cache ctxt =
- Symtab.unsynchronized_cache (fn c =>
+ Symtab.apply_unsynchronized_cache (fn c =>
Syntax.get_consts (Proof_Context.syntax_of ctxt) c
|> maps (Lexicon.unmark
{case_class = markup_class ctxt,
case_type = markup_type ctxt,
case_const = markup_const ctxt,
case_fixed = markup_free ctxt,
- case_default = K []}))
- |> #apply;
+ case_default = K []}));
@@ -265,26 +264,10 @@
Proof_Context.check_const {proper = true, strict = false} ctxt (c, ps)
|>> dest_Const_name;
-local
-
-fun get_free ctxt x =
- let
- val fixed = Variable.lookup_fixed ctxt x;
- val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
- val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
- in
- if Variable.is_const ctxt x then NONE
- else if is_some fixed then fixed
- else if not is_const orelse is_declared then SOME x
- else NONE
- end;
-
-in
-
fun decode_term ctxt =
let
- val markup_free_cache = #apply (Symtab.unsynchronized_cache (markup_free ctxt));
- val markup_const_cache = #apply (Symtab.unsynchronized_cache (markup_const ctxt));
+ val markup_free_cache = Symtab.apply_unsynchronized_cache (markup_free ctxt);
+ val markup_const_cache = Symtab.apply_unsynchronized_cache (markup_const ctxt);
fun decode (result as (_: Position.report_text list, Exn.Exn _)) = result
| decode (reports0, Exn.Res tm) =
@@ -319,7 +302,7 @@
| decode ps _ _ (Free (a, T)) =
((Name.reject_internal (a, ps) handle ERROR msg =>
error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
- (case get_free ctxt a of
+ (case Proof_Context.lookup_free ctxt a of
SOME x => (report ps markup_free_cache x; Free (x, T))
| NONE =>
let
@@ -337,8 +320,6 @@
in decode end;
-end;
-
(** parse **)
@@ -731,11 +712,8 @@
local
-fun extern_fixed ctxt x =
- if Name.is_skolem x then Variable.revert_fixed ctxt x else x;
-
fun extern_cache ctxt =
- Symtab.unsynchronized_cache (fn c =>
+ Symtab.apply_unsynchronized_cache (fn c =>
(case Syntax.get_consts (Proof_Context.syntax_of ctxt) c of
[b] => b
| bs =>
@@ -743,41 +721,52 @@
[] => c
| [b] => b
| _ => error ("Multiple logical entities for " ^ quote c ^ ": " ^ commas_quote bs)))
- |> Lexicon.unmark
- {case_class = Proof_Context.extern_class ctxt,
- case_type = Proof_Context.extern_type ctxt,
- case_const = Proof_Context.extern_const ctxt,
- case_fixed = extern_fixed ctxt,
- case_default = I})
- |> #apply;
+ |> Proof_Context.extern_entity ctxt);
val var_or_skolem_cache =
- Symtab.unsynchronized_cache (fn s =>
+ Symtab.apply_unsynchronized_cache (fn s =>
(case Lexicon.read_variable s of
SOME (x, i) =>
(case try Name.dest_skolem x of
SOME x' => (Markup.skolem, Term.string_of_vname (x', i))
| NONE => (Markup.var, s))
- | NONE => (Markup.var, s)))
- |> #apply;
+ | NONE => (Markup.var, s)));
val typing_elem = YXML.output_markup_elem Markup.typing;
val sorting_elem = YXML.output_markup_elem Markup.sorting;
-fun unparse_t t_to_ast pretty_flags language_markup ctxt t =
+fun exclude_consts ast ctxt =
let
+ val s = the_default "" (Syntax_Trans.default_struct ctxt);
+
+ fun exclude (Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]) = Symset.insert s
+ | exclude (Ast.Constant c) =
+ if Lexicon.is_fixed c then Symset.insert (Lexicon.unmark_fixed c) else I
+ | exclude (Ast.Appl [Ast.Constant "_bound", Ast.Variable x]) = Symset.insert x
+ | exclude (Ast.Appl [Ast.Constant "_free", Ast.Variable x]) = Symset.insert x
+ | exclude (Ast.Appl asts) = fold exclude asts
+ | exclude _ = I;
+ in Proof_Context.exclude_consts (Symset.build (exclude ast)) ctxt end;
+
+fun unparse_t t_to_ast pretty_flags language_markup ctxt0 t =
+ let
+ val syn = Proof_Context.syntax_of ctxt0;
+ val prtabs = Syntax.print_mode_tabs syn;
+ val trf = Syntax.print_ast_translation syn;
+
+ val ast = t_to_ast ctxt0 (Syntax.print_translation syn) t;
+ val ctxt = exclude_consts ast ctxt0;
+
val show_markup = Config.get ctxt show_markup;
val show_sorts = Config.get ctxt show_sorts;
val show_types = Config.get ctxt show_types orelse show_sorts;
- val syn = Proof_Context.syntax_of ctxt;
- val prtabs = Syntax.print_mode_tabs syn;
- val trf = Syntax.print_ast_translation syn;
val markup = markup_entity_cache ctxt;
val extern = extern_cache ctxt;
val free_or_skolem_cache =
- #apply (Symtab.unsynchronized_cache (fn x => (markup_free ctxt x, extern_fixed ctxt x)));
+ Symtab.apply_unsynchronized_cache (fn x =>
+ (markup_free ctxt x, Proof_Context.extern_fixed ctxt x));
val cache1 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table);
val cache2 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table);
@@ -829,8 +818,7 @@
in Unsynchronized.change cache (Ast.Table.update (A, block)); block end)
end;
in
- t_to_ast ctxt (Syntax.print_translation syn) t
- |> Ast.normalize ctxt {permissive_constraints = true} (Syntax.print_rules syn)
+ Ast.normalize ctxt {permissive_constraints = true} (Syntax.print_rules syn) ast
|> pretty_ast pretty_flags language_markup
end;
--- a/src/Pure/Syntax/syntax_trans.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML Fri Dec 06 21:27:07 2024 +0100
@@ -31,13 +31,14 @@
val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val mark_bound_abs: string * typ -> term
val mark_bound_body: string * typ -> term
- val bound_vars: (string * typ) list -> term -> term
+ val variant_bounds: Proof.context -> term -> (string * 'a) list -> (string * 'a) list
+ val bound_vars: Proof.context -> (string * typ) list -> term -> term
val abs_tr': Proof.context -> term -> term
- val atomic_abs_tr': string * typ * term -> term * term
+ val atomic_abs_tr': Proof.context -> string * typ * term -> term * term
val const_abs_tr': term -> term
val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
- val preserve_binder_abs_tr': string -> typ -> term list -> term
- val preserve_binder_abs2_tr': string -> typ -> term list -> term
+ val preserve_binder_abs_tr': string -> Proof.context -> typ -> term list -> term
+ val preserve_binder_abs2_tr': string -> Proof.context -> typ -> term list -> term
val print_abs: string * typ * term -> string * term
val dependent_tr': string * string -> term list -> term
val antiquote_tr': string -> term -> term
@@ -47,6 +48,7 @@
val update_name_tr': term -> term
val get_idents: Proof.context -> {structs: string list, fixes: string list}
val put_idents: {structs: string list, fixes: string list} -> Proof.context -> Proof.context
+ val default_struct: Proof.context -> string option
val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
val pure_parse_translation: (string * (Proof.context -> term list -> term)) list
val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
@@ -75,7 +77,6 @@
(print_mode_value ()) <> SOME type_bracketsN;
-
(** parse (ast) translations **)
(* strip_positions *)
@@ -224,6 +225,8 @@
val get_idents = Idents.get;
val put_idents = Idents.put;
+val default_struct = try hd o #structs o get_idents;
+
fun indexdefault_ast_tr [] =
Ast.Appl [Ast.Constant "_index",
Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]]
@@ -239,9 +242,9 @@
| index_tr ts = raise TERM ("index_tr", ts);
fun struct_tr ctxt [Const ("_indexdefault", _)] =
- (case #structs (get_idents ctxt) of
- x :: _ => Syntax.const (Lexicon.mark_fixed x)
- | _ => error "Illegal reference to implicit structure")
+ (case default_struct ctxt of
+ SOME x => Syntax.const (Lexicon.mark_fixed x)
+ | NONE => error "Illegal reference to implicit structure")
| struct_tr _ ts = raise TERM ("struct_tr", ts);
@@ -301,14 +304,27 @@
fun mark_bound_abs (x, T) = Const ("_bound", T --> T) $ Free (x, T);
fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T);
-fun bound_vars vars body =
- subst_bounds (map mark_bound_abs (rev (Term.variant_frees body vars)), body);
+fun variant_bounds ctxt t =
+ let
+ val s = the_default "" (default_struct ctxt);
-fun strip_abss vars_of body_of tm =
+ fun declare (Const ("_struct", _) $ Const ("_indexdefault", _)) = Name.declare s
+ | declare (Const (c, _)) =
+ if Lexicon.is_fixed c then Name.declare (Lexicon.unmark_fixed c) else I
+ | declare (Free (x, _)) = Name.declare x
+ | declare (t $ u) = declare t #> declare u
+ | declare (Abs (_, _, t)) = declare t
+ | declare _ = I;
+ in Name.variant_names_build (declare t) end;
+
+fun bound_vars ctxt vars body =
+ subst_bounds (map mark_bound_abs (rev (variant_bounds ctxt body vars)), body);
+
+fun strip_abss ctxt vars_of body_of tm =
let
val vars = vars_of tm;
val body = body_of tm;
- val new_vars = Term.variant_frees body vars;
+ val new_vars = variant_bounds ctxt body vars;
fun subst (x, T) b =
if Name.is_internal x andalso not (Term.is_dependent b)
then (Const ("_idtdummy", T), incr_boundvars ~1 b)
@@ -319,10 +335,10 @@
fun abs_tr' ctxt tm =
uncurry (fold_rev (fn x => fn t => Syntax.const "_abs" $ x $ t))
- (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
+ (strip_abss ctxt strip_abs_vars strip_abs_body (eta_contr ctxt tm));
-fun atomic_abs_tr' (x, T, t) =
- let val xT = singleton (Term.variant_frees t) (x, T)
+fun atomic_abs_tr' ctxt (x, T, t) =
+ let val xT = singleton (variant_bounds ctxt t) (x, T)
in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;
fun abs_ast_tr' asts =
@@ -346,21 +362,21 @@
| mk_idts [idt] = idt
| mk_idts (idt :: idts) = Syntax.const "_idts" $ idt $ mk_idts idts;
- fun tr' t =
+ fun tr' ctxt t =
let
- val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
+ val (xs, bd) = strip_abss ctxt (strip_qnt_vars name) (strip_qnt_body name) t;
in Syntax.const syn $ mk_idts xs $ bd end;
- fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts)
- | binder_tr' [] = raise Match;
- in (name, fn _ => binder_tr') end;
+ fun binder_tr' ctxt (t :: ts) = Term.list_comb (tr' ctxt (Syntax.const name $ t), ts)
+ | binder_tr' _ [] = raise Match;
+ in (name, binder_tr') end;
-fun preserve_binder_abs_tr' syn ty (Abs abs :: ts) =
- let val (x, t) = atomic_abs_tr' abs
+fun preserve_binder_abs_tr' syn ctxt ty (Abs abs :: ts) =
+ let val (x, t) = atomic_abs_tr' ctxt abs
in list_comb (Const (syn, ty) $ x $ t, ts) end;
-fun preserve_binder_abs2_tr' syn ty (A :: Abs abs :: ts) =
- let val (x, t) = atomic_abs_tr' abs
+fun preserve_binder_abs2_tr' syn ctxt ty (A :: Abs abs :: ts) =
+ let val (x, t) = atomic_abs_tr' ctxt abs
in list_comb (Const (syn, ty) $ x $ A $ t, ts) end;
@@ -389,7 +405,7 @@
(* dependent / nondependent quantifiers *)
fun print_abs (x, T, b) =
- let val x' = #1 (Name.variant x (Name.build_context (Term.declare_term_names b)))
+ let val x' = #1 (Name.variant x (Name.build_context (Term.declare_free_names b)))
in (x', subst_bound (mark_bound_abs (x', T), b)) end;
fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
@@ -449,9 +465,9 @@
| index_ast_tr' _ = raise Match;
fun struct_ast_tr' ctxt [Ast.Constant "_indexdefault"] =
- (case #structs (get_idents ctxt) of
- x :: _ => Ast.Appl [Ast.Constant "_free", Ast.Variable x]
- | _ => raise Match)
+ (case default_struct ctxt of
+ SOME x => Ast.Appl [Ast.Constant "_free", Ast.Variable x]
+ | NONE => raise Match)
| struct_ast_tr' _ _ = raise Match;
--- a/src/Pure/Thy/document_antiquotations.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Fri Dec 06 21:27:07 2024 +0100
@@ -47,8 +47,7 @@
in Proof_Context.pretty_term_abbrev ctxt' eq end;
fun pretty_locale ctxt (name, pos) =
- let val thy = Proof_Context.theory_of ctxt
- in Pretty.str (Locale.extern thy (Locale.check thy (name, pos))) end;
+ Pretty.str (Locale.extern ctxt (Locale.check ctxt (name, pos)));
fun pretty_bundle ctxt (name, pos) =
Pretty.str (Bundle.extern ctxt (Bundle.check ctxt (name, pos)));
--- a/src/Pure/consts.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/consts.ML Fri Dec 06 21:27:07 2024 +0100
@@ -313,7 +313,7 @@
fun rev_abbrev lhs rhs =
let
val (xs, body) = strip_abss (Envir.beta_eta_contract rhs);
- val vars = map (fn (x, T) => Var ((x, 0), T)) (Term.variant_frees body xs);
+ val vars = map (fn (x, T) => Var ((x, 0), T)) (Term.variant_bounds body xs);
in (Term.subst_bounds (rev vars, body), Term.list_comb (lhs, vars)) end;
in
--- a/src/Pure/facts.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/facts.ML Fri Dec 06 21:27:07 2024 +0100
@@ -30,7 +30,7 @@
val intern: T -> xstring -> string
val extern: Proof.context -> T -> string -> xstring
val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
- val pretty_thm_name: Context.generic -> T -> Thm_Name.T -> Pretty.T
+ val pretty_thm_name: Proof.context -> T -> Thm_Name.T -> Pretty.T
val defined: T -> string -> bool
val is_dynamic: T -> string -> bool
val lookup: Context.generic -> T -> string -> {dynamic: bool, thms: thm list} option
@@ -174,9 +174,9 @@
fun extern ctxt = Name_Space.extern ctxt o space_of;
fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of;
-fun pretty_thm_name context facts thm_name =
+fun pretty_thm_name ctxt facts thm_name =
let
- val prfx = Thm_Name.print_prefix context (space_of facts) thm_name;
+ val prfx = Thm_Name.print_prefix ctxt (space_of facts) thm_name;
val sffx = Thm_Name.print_suffix thm_name;
in Pretty.block [Pretty.mark_str prfx, Pretty.str sffx] end;
--- a/src/Pure/global_theory.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/global_theory.ML Fri Dec 06 21:27:07 2024 +0100
@@ -14,8 +14,8 @@
val alias_fact: binding -> string -> theory -> theory
val hide_fact: bool -> string -> theory -> theory
val dest_thms: bool -> theory list -> theory -> (Thm_Name.P * thm) list
- val pretty_thm_name: theory -> Thm_Name.T -> Pretty.T
- val print_thm_name: theory -> Thm_Name.T -> string
+ val pretty_thm_name: Proof.context -> Thm_Name.T -> Pretty.T
+ val print_thm_name: Proof.context -> Thm_Name.T -> string
val get_thm_names: theory -> Thm_Name.P Inttab.table
val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.P) list
val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.P option
@@ -88,7 +88,9 @@
Facts.dest_static verbose (map facts_of prev_thys) (facts_of thy)
|> maps (fn (name, thms) => Thm_Name.list (name, Position.none) thms);
-fun pretty_thm_name thy = Facts.pretty_thm_name (Context.Theory thy) (facts_of thy);
+fun pretty_thm_name ctxt =
+ Facts.pretty_thm_name ctxt (facts_of (Proof_Context.theory_of ctxt));
+
val print_thm_name = Pretty.string_of oo pretty_thm_name;
@@ -108,9 +110,11 @@
else
(case Inttab.lookup thm_names serial of
SOME (thm_name', thm_pos') =>
- raise THM ("Duplicate use of derivation identity for " ^
- print_thm_name thy thm_name ^ Position.here thm_pos ^ " vs. " ^
- print_thm_name thy thm_name' ^ Position.here thm_pos', 0, [thm])
+ let val thy_ctxt = Proof_Context.init_global thy in
+ raise THM ("Duplicate use of derivation identity for " ^
+ print_thm_name thy_ctxt thm_name ^ Position.here thm_pos ^ " vs. " ^
+ print_thm_name thy_ctxt thm_name' ^ Position.here thm_pos', 0, [thm])
+ end
| NONE => Inttab.update (serial, (thm_name, thm_pos)) thm_names)));
fun lazy_thm_names thy =
--- a/src/Pure/logic.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/logic.ML Fri Dec 06 21:27:07 2024 +0100
@@ -667,7 +667,7 @@
(*reverses parameters for substitution*)
fun goal_params st i =
let val gi = get_goal st i
- val rfrees = map Free (rev (Term.variant_frees gi (strip_params gi)))
+ val rfrees = map Free (rev (Term.variant_bounds gi (strip_params gi)))
in (gi, rfrees) end;
fun concl_of_goal st i =
--- a/src/Pure/primitive_defs.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/primitive_defs.ML Fri Dec 06 21:27:07 2024 +0100
@@ -31,7 +31,7 @@
val eq_body = Term.strip_all_body eq;
val display_terms =
- commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars);
+ commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars ctxt eq_vars);
val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)";
@@ -77,7 +77,7 @@
fun abs_def eq =
let
val body = Term.strip_all_body eq;
- val vars = map Free (Term.variant_frees body (Term.strip_all_vars eq));
+ val vars = map Free (Term.variant_bounds body (Term.strip_all_vars eq));
val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (rev vars, body));
val (lhs', args) = Term.strip_comb lhs;
val rhs' = fold_rev (absfree o dest_Free) args rhs;
--- a/src/Pure/raw_simplifier.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/raw_simplifier.ML Fri Dec 06 21:27:07 2024 +0100
@@ -481,10 +481,9 @@
fun print_thm ctxt msg (name, th) =
let
- val thy = Proof_Context.theory_of ctxt;
val sffx =
if Thm_Name.is_empty name then ""
- else " " ^ quote (Global_Theory.print_thm_name thy name) ^ ":";
+ else " " ^ quote (Global_Theory.print_thm_name ctxt name) ^ ":";
in print_term ctxt (msg ^ sffx) (Thm.full_prop_of th) end;
fun print_thm0 ctxt msg th = print_thm ctxt msg (Thm_Name.empty, th);
--- a/src/Pure/term.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/term.ML Fri Dec 06 21:27:07 2024 +0100
@@ -157,6 +157,7 @@
val declare_tvar_names: (int -> bool) -> term -> Name.context -> Name.context
val declare_free_names: term -> Name.context -> Name.context
val declare_var_names: (int -> bool) -> term -> Name.context -> Name.context
+ val variant_bounds: term -> (string * 'a) list -> (string * 'a) list
val hidden_polymorphism: term -> (indexname * sort) list
val declare_term_names: term -> Name.context -> Name.context
val variant_frees: term -> (string * 'a) list -> (string * 'a) list
@@ -583,6 +584,8 @@
val declare_free_names = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
fun declare_var_names pred = fold_aterms (fn Var ((x, i), _) => pred i ? Name.declare x | _ => I);
+fun variant_bounds t = Name.variant_names_build (declare_free_names t);
+
(*extra type variables in a term, not covered by its type*)
fun hidden_polymorphism t =
let
--- a/src/Pure/term_items.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/term_items.ML Fri Dec 06 21:27:07 2024 +0100
@@ -36,6 +36,7 @@
val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int};
val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
+ val apply_unsynchronized_cache: (key -> 'a) -> key -> 'a
type set = int table
val add_set: key -> set -> set
val make_set: key list -> set
@@ -89,6 +90,7 @@
type 'a cache_ops = 'a Table.cache_ops;
val unsynchronized_cache = Table.unsynchronized_cache;
+val apply_unsynchronized_cache = Table.apply_unsynchronized_cache;
(* set with order of addition *)
--- a/src/Pure/thm.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/thm.ML Fri Dec 06 21:27:07 2024 +0100
@@ -1095,8 +1095,8 @@
SOME T' => T'
| NONE => raise Fail "strip_shyps: bad type variable in proof term"));
val map_ztyp =
- #apply (ZTypes.unsynchronized_cache
- (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar)));
+ ZTypes.apply_unsynchronized_cache
+ (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));
val zproof' = ZTerm.map_proof_types {hyps = true} map_ztyp zproof;
val proof' = Proofterm.map_proof_types (Term.map_atyps_same map_atyp) proof;
--- a/src/Pure/thm_deps.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/thm_deps.ML Fri Dec 06 21:27:07 2024 +0100
@@ -11,7 +11,7 @@
val has_skip_proof: thm list -> bool
val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list
- val pretty_thm_deps: theory -> thm list -> Pretty.T
+ val pretty_thm_deps: Proof.context -> thm list -> Pretty.T
val unused_thms_cmd: theory list * theory list -> (Thm_Name.T * thm) list
end;
@@ -71,10 +71,11 @@
|-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I)
end;
-fun pretty_thm_deps thy thms =
+fun pretty_thm_deps ctxt thms =
let
+ val thy = Proof_Context.theory_of ctxt;
val facts = Global_Theory.facts_of thy;
- val extern_fact = Name_Space.extern_generic (Context.Theory thy) (Facts.space_of facts);
+ val extern_fact = Name_Space.extern ctxt (Facts.space_of facts);
val deps =
(case try (thm_deps thy) thms of
SOME deps => deps
@@ -83,7 +84,7 @@
deps
|> map (fn (_, thm_name as (name, _)) => (extern_fact name, thm_name))
|> sort_by #1
- |> map (fn (_, thm_name) => Pretty.item [Global_Theory.pretty_thm_name thy thm_name])
+ |> map (fn (_, thm_name) => Pretty.item [Global_Theory.pretty_thm_name ctxt thm_name])
in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end;
--- a/src/Pure/thm_name.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/thm_name.ML Fri Dec 06 21:27:07 2024 +0100
@@ -23,7 +23,7 @@
val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list
val parse: string -> T
- val print_prefix: Context.generic -> Name_Space.T -> T -> Markup.T * string
+ val print_prefix: Proof.context -> Name_Space.T -> T -> Markup.T * string
val print_suffix: T -> string
val print: T -> string
val print_pos: P -> string
@@ -99,9 +99,9 @@
(* print *)
-fun print_prefix context space ((name, _): T) =
+fun print_prefix ctxt space ((name, _): T) =
if name = "" then (Markup.empty, "")
- else (Name_Space.markup space name, Name_Space.extern_generic context space name);
+ else (Name_Space.markup space name, Name_Space.extern ctxt space name);
fun print_suffix (name, index) =
if name = "" orelse index = 0 then ""
--- a/src/Pure/type_infer_context.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/type_infer_context.ML Fri Dec 06 21:27:07 2024 +0100
@@ -248,7 +248,7 @@
val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts);
val (Ts', Ts'') = chop (length Ts) Ts_bTs';
fun prep t =
- let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
+ let val xs = rev (Syntax_Trans.variant_bounds ctxt t (rev (map fst bs ~~ Ts'')))
in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end;
in (map prep ts', Ts') end;
--- a/src/Pure/variable.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/variable.ML Fri Dec 06 21:27:07 2024 +0100
@@ -326,7 +326,7 @@
[] => t
| bounds =>
let
- val names = Term.declare_term_names t (names_of ctxt);
+ val names = Term.declare_free_names t (names_of ctxt);
val xs = rev (Name.variants names (rev (map #2 bounds)));
fun substs (((b, T), _), x') =
let fun subst U = (Free (b, U), Syntax_Trans.mark_bound_abs (x', U))
@@ -705,7 +705,7 @@
fun focus_params bindings t ctxt =
let
- val ps = Term.variant_frees t (Term.strip_all_vars t); (*as they are printed :-*)
+ val ps = Syntax_Trans.variant_bounds ctxt t (Term.strip_all_vars t);
val (xs, Ts) = split_list ps;
val (xs', ctxt') =
(case bindings of
--- a/src/Pure/zterm.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Pure/zterm.ML Fri Dec 06 21:27:07 2024 +0100
@@ -548,7 +548,7 @@
fun instantiate_type_same instT =
if ZTVars.is_empty instT then Same.same
- else #apply (ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT))));
+ else ZTypes.apply_unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT)));
fun instantiate_term_same typ inst =
subst_term_same typ (Same.function (ZVars.lookup inst));
@@ -863,9 +863,7 @@
let
val lookup =
if Vartab.is_empty tenv then K NONE
- else
- #apply (ZVars.unsynchronized_cache
- (apsnd typ_of #> Envir.lookup envir #> Option.map zterm));
+ else ZVars.apply_unsynchronized_cache (apsnd typ_of #> Envir.lookup envir #> Option.map zterm);
val normT = norm_type_same ztyp tyenv;
@@ -1008,8 +1006,8 @@
val typ_operation = #typ_operation ucontext {strip_sorts = true};
val unconstrain_typ = Same.commit typ_operation;
val unconstrain_ztyp =
- #apply (ZTypes.unsynchronized_cache
- (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of)));
+ ZTypes.apply_unsynchronized_cache
+ (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of));
val unconstrain_zterm = zterm o Term.map_types typ_operation;
val unconstrain_proof = Same.commit (map_proof_types {hyps = true} unconstrain_ztyp);
@@ -1226,10 +1224,10 @@
val typ =
if Names.is_empty tfrees then Same.same
else
- #apply (ZTypes.unsynchronized_cache
+ ZTypes.apply_unsynchronized_cache
(subst_type_same (fn ((a, i), S) =>
if i = ~1 andalso Names.defined tfrees a then ZTVar ((a, idx), S)
- else raise Same.SAME)));
+ else raise Same.SAME));
val term =
subst_term_same typ (fn ((x, i), T) =>
if i = ~1 andalso Names.defined frees x then ZVar ((x, idx), T)
@@ -1251,10 +1249,10 @@
let
val tab = ZTVars.build (names |> fold (fn ((a, S), b) => ZTVars.add (((a, ~1), S), b)));
val typ =
- #apply (ZTypes.unsynchronized_cache (subst_type_same (fn v =>
+ ZTypes.apply_unsynchronized_cache (subst_type_same (fn v =>
(case ZTVars.lookup tab v of
NONE => raise Same.SAME
- | SOME w => ZTVar w))));
+ | SOME w => ZTVar w)));
in map_proof_types {hyps = false} typ prf end;
fun legacy_freezeT_proof t prf =
@@ -1263,7 +1261,7 @@
| SOME f =>
let
val tvar = ztyp_of o Same.function f;
- val typ = #apply (ZTypes.unsynchronized_cache (subst_type_same tvar));
+ val typ = ZTypes.apply_unsynchronized_cache (subst_type_same tvar);
in map_proof_types {hyps = false} typ prf end);
@@ -1297,7 +1295,7 @@
if inc = 0 then Same.same
else
let fun tvar ((a, i), S) = if i >= 0 then ZTVar ((a, i + inc), S) else raise Same.SAME
- in #apply (ZTypes.unsynchronized_cache (subst_type_same tvar)) end;
+ in ZTypes.apply_unsynchronized_cache (subst_type_same tvar) end;
fun incr_indexes_proof inc prf =
let
@@ -1437,8 +1435,8 @@
val typ_cache = typ_cache thy;
val typ =
- #apply (ZTypes.unsynchronized_cache
- (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of));
+ ZTypes.apply_unsynchronized_cache
+ (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of);
val typ_sort = #typ_operation ucontext {strip_sorts = false};
--- a/src/Tools/induct.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Tools/induct.ML Fri Dec 06 21:27:07 2024 +0100
@@ -607,7 +607,7 @@
let
val maxidx = Thm.maxidx_of st;
val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*)
- val params = Term.variant_frees goal (Logic.strip_params goal);
+ val params = Syntax_Trans.variant_bounds ctxt goal (Logic.strip_params goal);
in
if not (null params) then
(warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
--- a/src/Tools/subtyping.ML Thu Dec 05 19:44:53 2024 +0100
+++ b/src/Tools/subtyping.ML Fri Dec 06 21:27:07 2024 +0100
@@ -244,7 +244,7 @@
val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts);
val (Ts', Ts'') = chop (length Ts) Ts_bTs';
fun prep t =
- let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
+ let val xs = rev (Syntax_Trans.variant_bounds ctxt t (rev (map fst bs ~~ Ts'')))
in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end;
in (map prep ts', Ts') end;