--- a/src/HOL/Analysis/measurable.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Analysis/measurable.ML Sat Apr 22 10:22:41 2023 +0200
@@ -34,82 +34,73 @@
structure Measurable : MEASURABLE =
struct
-type preprocessor = thm -> Proof.context -> (thm list * Proof.context)
+type preprocessor = thm -> Proof.context -> thm list * Proof.context
datatype level = Concrete | Generic;
-fun eq_measurable_thms ((th1, d1), (th2, d2)) =
+type measurable_thm = thm * (bool * level);
+
+fun eq_measurable_thm ((th1, d1): measurable_thm, (th2, d2): measurable_thm) =
d1 = d2 andalso Thm.eq_thm_prop (th1, th2) ;
-fun merge_dups (xs:(string * preprocessor) list) ys =
- xs @ (filter (fn (name, _) => is_none (find_first (fn (name', _) => name' = name) xs)) ys)
+fun merge_preprocessors (xs: (string * preprocessor) list, ys) =
+ xs @ (filter (fn (name, _) => is_none (find_first (fn (name', _) => name' = name) xs)) ys)
structure Data = Generic_Data
(
- type T = {
- measurable_thms : (thm * (bool * level)) Item_Net.T,
- dest_thms : thm Item_Net.T,
- cong_thms : thm Item_Net.T,
- preprocessors : (string * preprocessor) list }
- val empty: T = {
- measurable_thms = Item_Net.init eq_measurable_thms (single o Thm.prop_of o fst),
- dest_thms = Thm.item_net,
- cong_thms = Thm.item_net,
- preprocessors = [] };
- fun merge ({measurable_thms = t1, dest_thms = dt1, cong_thms = ct1, preprocessors = i1 },
- {measurable_thms = t2, dest_thms = dt2, cong_thms = ct2, preprocessors = i2 }) : T = {
- measurable_thms = Item_Net.merge (t1, t2),
- dest_thms = Item_Net.merge (dt1, dt2),
- cong_thms = Item_Net.merge (ct1, ct2),
- preprocessors = merge_dups i1 i2
- };
+ type T =
+ measurable_thm Item_Net.T *
+ (*dest_thms*) thm Item_Net.T *
+ (*cong_thms*) thm Item_Net.T *
+ (string * preprocessor) list
+ val empty: T =
+ (Item_Net.init eq_measurable_thm (single o Thm.full_prop_of o fst), Thm.item_net, Thm.item_net, [])
+ fun merge
+ ((measurable_thms1, dest_thms1, cong_thms1, preprocessors1),
+ (measurable_thms2, dest_thms2, cong_thms2, preprocessors2)) : T =
+ (Item_Net.merge (measurable_thms1, measurable_thms2),
+ Item_Net.merge (dest_thms1, dest_thms2),
+ Item_Net.merge (cong_thms1, cong_thms2),
+ merge_preprocessors (preprocessors1, preprocessors2))
);
-val debug =
- Attrib.setup_config_bool \<^binding>\<open>measurable_debug\<close> (K false)
-
-val split =
- Attrib.setup_config_bool \<^binding>\<open>measurable_split\<close> (K true)
+val map_measurable_thms = Data.map o @{apply 4(1)}
+val map_dest_thms = Data.map o @{apply 4(2)}
+val map_cong_thms = Data.map o @{apply 4(3)}
+val map_preprocessors = Data.map o @{apply 4(4)}
-fun map_data f1 f2 f3 f4
- {measurable_thms = t1, dest_thms = t2, cong_thms = t3, preprocessors = t4 } =
- {measurable_thms = f1 t1, dest_thms = f2 t2, cong_thms = f3 t3, preprocessors = f4 t4}
-
-fun map_measurable_thms f = map_data f I I I
-fun map_dest_thms f = map_data I f I I
-fun map_cong_thms f = map_data I I f I
-fun map_preprocessors f = map_data I I I f
+val debug = Attrib.setup_config_bool \<^binding>\<open>measurable_debug\<close> (K false)
+val split = Attrib.setup_config_bool \<^binding>\<open>measurable_split\<close> (K true)
fun generic_add_del map : attribute context_parser =
Scan.lift
(Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >>
- (fn f => Thm.declaration_attribute (Data.map o map o f))
+ (fn f => Thm.declaration_attribute (map o f o Thm.trim_context))
val dest_thm_attr = generic_add_del map_dest_thms
-
val cong_thm_attr = generic_add_del map_cong_thms
fun del_thm th net =
let
- val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm (th, th'))
+ val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm_prop (th, th'))
in fold Item_Net.remove thms net end ;
fun measurable_thm_attr (do_add, d) = Thm.declaration_attribute
- (Data.map o map_measurable_thms o (if do_add then Item_Net.update o rpair d else del_thm))
-
-val get_dest = Item_Net.content o #dest_thms o Data.get;
+ (map_measurable_thms o (if do_add then Item_Net.update o rpair d else del_thm) o Thm.trim_context)
-val get_cong = Item_Net.content o #cong_thms o Data.get;
-val add_cong = Data.map o map_cong_thms o Item_Net.update;
-val del_cong = Data.map o map_cong_thms o Item_Net.remove;
+fun get_dest context = map (Thm.transfer'' context) (Item_Net.content (#2 (Data.get context)));
+fun get_cong context = map (Thm.transfer'' context) (Item_Net.content (#3 (Data.get context)));
+
+val add_cong = map_cong_thms o Item_Net.update o Thm.trim_context;
+val del_cong = map_cong_thms o Item_Net.remove o Thm.trim_context;
fun add_del_cong_thm true = add_cong
| add_del_cong_thm false = del_cong
-fun add_preprocessor name f = Data.map (map_preprocessors (fn xs => xs @ [(name, f)]))
-fun del_preprocessor name = Data.map (map_preprocessors (filter (fn (n, _) => n <> name)))
+fun add_preprocessor name f = map_preprocessors (fn xs => xs @ [(name, f)])
+fun del_preprocessor name = map_preprocessors (filter (fn (n, _) => n <> name))
val add_local_cong = Context.proof_map o add_cong
-val get_preprocessors = Context.Proof #> Data.get #> #preprocessors ;
+val get_preprocessors = Context.Proof #> Data.get #> #4;
fun is_too_generic thm =
let
@@ -117,9 +108,10 @@
val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
in is_Var (head_of concl') end
-val get_thms = Data.get #> #measurable_thms #> Item_Net.content ;
+fun get_thms context =
+ map (apfst (Thm.transfer'' context)) (Item_Net.content (#1 (Data.get context)));
-val get_all = get_thms #> map fst ;
+val get_all = get_thms #> map fst;
fun debug_tac ctxt msg f =
if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
--- a/src/HOL/Library/refute.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Library/refute.ML Sat Apr 22 10:22:41 2023 +0200
@@ -2375,7 +2375,7 @@
val result = fold (fn arg_i => fn i =>
interpretation_apply (i, arg_i)) arg_intrs intr
(* update 'REC_OPERATORS' *)
- val _ = Array.update (arr, elem, (true, result))
+ val _ = Array.upd arr elem (true, result)
in
result
end
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sat Apr 22 10:22:41 2023 +0200
@@ -239,7 +239,7 @@
let val consts = Term.add_const_names (Thm.prop_of th) [] in
exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse
exists (member (op =) forbidden_consts) consts orelse
- length (Long_Name.explode s) <> 2 orelse
+ Long_Name.count s <> 2 orelse
String.isPrefix "type_definition" (List.last (Long_Name.explode s)) orelse
String.isSuffix "_def" s orelse
String.isSuffix "_raw" s orelse
@@ -331,7 +331,7 @@
fun thms_of all thy =
filter
- (fn th => (all orelse Thm.theory_name th = Context.theory_name thy)
+ (fn th => (all orelse Thm.theory_long_name th = Context.theory_long_name thy)
(* andalso is_executable_thm thy th *))
(map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false)))
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Sat Apr 22 10:22:41 2023 +0200
@@ -144,7 +144,7 @@
val mono_timeout = seconds 1.0
fun is_forbidden_theorem name =
- length (Long_Name.explode name) <> 2 orelse
+ Long_Name.count name <> 2 orelse
String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse
String.isPrefix "arity_" (List.last (Long_Name.explode name)) orelse
String.isSuffix "_def" name orelse
@@ -153,7 +153,7 @@
fun theorems_of thy =
filter (fn (name, th) =>
not (is_forbidden_theorem name) andalso
- Thm.theory_name th = Context.theory_name thy)
+ Thm.theory_long_name th = Context.theory_long_name thy)
(Global_Theory.all_thms_of thy true)
fun check_formulas tsp =
@@ -175,7 +175,7 @@
fun check_theory thy =
let
- val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
+ val path = File.tmp_path (Context.theory_base_name thy ^ ".out" |> Path.explode)
val _ = File.write path ""
fun check_theorem (name, th) =
let
--- a/src/HOL/TPTP/mash_export.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/TPTP/mash_export.ML Sat Apr 22 10:22:41 2023 +0200
@@ -58,7 +58,7 @@
| _ => ("", []))
fun has_thm_thy th thy =
- Context.theory_name thy = Thm.theory_name th
+ Context.theory_base_name thy = Thm.theory_base_name th
fun has_thys thys th = exists (has_thm_thy th) thys
@@ -98,7 +98,7 @@
fun do_fact ((_, stature), th) =
let
val name = nickname_of_thm th
- val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
+ val feats = features_of ctxt (Thm.theory_base_name th) stature [Thm.prop_of th]
val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n"
in
File.append path s
@@ -187,14 +187,14 @@
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
val isar_deps = isar_dependencies_of name_tabs th
val do_query = not (is_bad_query ctxt step j th isar_deps)
- val goal_feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
+ val goal_feats = features_of ctxt (Thm.theory_base_name th) stature [Thm.prop_of th]
val access_facts = filter_accessible_from th new_facts @ old_facts
val (marker, deps) =
smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps
fun extra_features_of (((_, stature), th), weight) =
[Thm.prop_of th]
- |> features_of ctxt (Thm.theory_name th) stature
+ |> features_of ctxt (Thm.theory_base_name th) stature
|> map (rpair (weight * extra_feature_factor))
val query =
@@ -261,7 +261,7 @@
val suggs =
old_facts
|> filter_accessible_from th
- |> mepo_or_mash_suggested_facts ctxt (Thm.theory_name th)
+ |> mepo_or_mash_suggested_facts ctxt (Thm.theory_base_name th)
params max_suggs hyp_ts concl_t
|> map (nickname_of_thm o snd)
in
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Sat Apr 22 10:22:41 2023 +0200
@@ -16,7 +16,7 @@
fun thms_of thy thy_name =
Global_Theory.all_thms_of thy false
- |> filter (fn (_, th) => Thm.theory_name th = thy_name)
+ |> filter (fn (_, th) => Thm.theory_base_name th = thy_name)
fun do_while P f s list =
if P s then
@@ -71,7 +71,7 @@
val thy = Proof_Context.theory_of ctxt
val all_thms =
thms_of thy thy_name
- |> filter (fn (name, _) => length (Long_Name.explode name) = 2) (* FIXME !? *)
+ |> filter (fn (name, _) => Long_Name.count name = 2) (* FIXME !? *)
|> sort_by #1
val check = check_unused_assms ctxt
in rev (Par_List.map check all_thms) end
@@ -95,7 +95,8 @@
fun print_unused_assms ctxt opt_thy_name =
let
- val thy_name = the_default (Context.theory_name (Proof_Context.theory_of ctxt)) opt_thy_name
+ val thy_name =
+ the_default (Context.theory_base_name (Proof_Context.theory_of ctxt)) opt_thy_name
val results = find_unused_assms ctxt thy_name
val total = length results
val with_assumptions = length (filter (is_some o snd) results)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Apr 22 10:22:41 2023 +0200
@@ -484,7 +484,7 @@
let
val n = length ths
val collection = n > 1
- val dotted_name = length (Long_Name.explode name0) > 2 (* ignore theory name *)
+ val dotted_name = Long_Name.count name0 > 2 (* ignore theory name *)
fun check_thms a =
(case try (Proof_Context.get_thms ctxt) a of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Apr 22 10:22:41 2023 +0200
@@ -796,7 +796,7 @@
(* There must be a better way to detect local facts. *)
(case Long_Name.dest_local hint of
SOME suf =>
- Long_Name.implode [Thm.theory_name th, suf, crude_printed_term 25 (Thm.prop_of th)]
+ Long_Name.implode [Thm.theory_base_name th, suf, crude_printed_term 25 (Thm.prop_of th)]
| NONE => hint)
end
else
@@ -820,9 +820,9 @@
fun crude_thm_ord ctxt =
let
val ancestor_lengths =
- fold (fn thy => Symtab.update (Context.theory_name thy, length (Context.ancestors_of thy)))
+ fold (fn thy => Symtab.update (Context.theory_base_name thy, length (Context.ancestors_of thy)))
(Theory.nodes_of (Proof_Context.theory_of ctxt)) Symtab.empty
- val ancestor_length = Symtab.lookup ancestor_lengths o Context.theory_id_name
+ val ancestor_length = Symtab.lookup ancestor_lengths o Context.theory_id_name {long = false}
fun crude_theory_ord p =
if Context.eq_thy_id p then EQUAL
@@ -832,9 +832,9 @@
(case apply2 ancestor_length p of
(SOME m, SOME n) =>
(case int_ord (m, n) of
- EQUAL => string_ord (apply2 Context.theory_id_name p)
+ EQUAL => string_ord (apply2 (Context.theory_id_name {long = false}) p)
| ord => ord)
- | _ => string_ord (apply2 Context.theory_id_name p))
+ | _ => string_ord (apply2 (Context.theory_id_name {long = false}) p))
in
fn p =>
(case crude_theory_ord (apply2 Thm.theory_id p) of
@@ -1125,7 +1125,7 @@
val chunks = app_hd (cons th) chunks
val chunks_and_parents' =
if thm_less_eq (th, th') andalso
- Thm.theory_name th = Thm.theory_name th'
+ Thm.theory_base_name th = Thm.theory_base_name th'
then (chunks, [nickname_of_thm th])
else chunks_and_parents_for chunks th'
in
@@ -1172,11 +1172,11 @@
val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts
- fun fact_has_right_theory (_, th) = thy_name = Thm.theory_name th
+ fun fact_has_right_theory (_, th) = thy_name = Thm.theory_base_name th
fun chained_or_extra_features_of factor (((_, stature), th), weight) =
[Thm.prop_of th]
- |> features_of ctxt (Thm.theory_name th) stature
+ |> features_of ctxt (Thm.theory_base_name th) stature
|> map (rpair (weight * factor))
in
(case get_state ctxt of
@@ -1283,7 +1283,7 @@
launch_thread timeout (fn () =>
let
val thy = Proof_Context.theory_of ctxt
- val feats = features_of ctxt (Context.theory_name thy) (Local, General) [t]
+ val feats = features_of ctxt (Context.theory_base_name thy) (Local, General) [t]
in
map_state ctxt
(fn {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =>
@@ -1395,7 +1395,7 @@
(learns, (num_nontrivial, next_commit, _)) =
let
val name = nickname_of_thm th
- val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
+ val feats = features_of ctxt (Thm.theory_base_name th) stature [Thm.prop_of th]
val deps = these (deps_of status th)
val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
val learns = (name, parents, feats, deps) :: learns
@@ -1544,7 +1544,7 @@
[("", [])]
else
let
- val thy_name = Context.theory_name (Proof_Context.theory_of ctxt)
+ val thy_name = Context.theory_base_name (Proof_Context.theory_of ctxt)
fun maybe_launch_thread exact min_num_facts_to_learn =
if not (Async_Manager_Legacy.has_running_threads MaShN) andalso
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Sat Apr 22 10:22:41 2023 +0200
@@ -220,7 +220,7 @@
t
fun theory_const_prop_of fudge th =
- theory_constify fudge (Thm.theory_name th) (Thm.prop_of th)
+ theory_constify fudge (Thm.theory_base_name th) (Thm.prop_of th)
fun pair_consts_fact thy fudge fact =
(case fact |> snd |> theory_const_prop_of fudge |> pconsts_in_fact thy of
@@ -546,7 +546,7 @@
[]
else
relevance_filter ctxt thres0 decay max_facts fudge facts hyp_ts
- (concl_t |> theory_constify fudge (Context.theory_name thy)))
+ (concl_t |> theory_constify fudge (Context.theory_base_name thy)))
|> map fact_of_lazy_fact
end
--- a/src/HOL/Tools/sat.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Tools/sat.ML Sat Apr 22 10:22:41 2023 +0200
@@ -216,7 +216,7 @@
handle TERM _ => NONE; (* 'chyp' is not a literal *)
fun prove_clause id =
- (case Array.sub (clauses, id) of
+ (case Array.nth clauses id of
RAW_CLAUSE clause => clause
| ORIG_CLAUSE thm =>
(* convert the original clause *)
@@ -226,7 +226,7 @@
val hyps = sort (lit_ord o apply2 fst) (map_filter (fn chyp =>
Option.map (rpair chyp) (index_of_literal chyp)) (Thm.chyps_of raw))
val clause = (raw, hyps)
- val _ = Array.update (clauses, id, RAW_CLAUSE clause)
+ val _ = Array.upd clauses id (RAW_CLAUSE clause)
in
clause
end
@@ -236,7 +236,7 @@
val _ = cond_tracing ctxt (fn () => "Proving clause #" ^ string_of_int id ^ " ...")
val ids = the (Inttab.lookup clause_table id)
val clause = resolve_raw_clauses ctxt (map prove_clause ids)
- val _ = Array.update (clauses, id, RAW_CLAUSE clause)
+ val _ = Array.upd clauses id (RAW_CLAUSE clause)
val _ =
cond_tracing ctxt
(fn () => "Replay chain successful; clause stored at #" ^ string_of_int id)
@@ -358,7 +358,7 @@
val max_idx = fst (the (Inttab.max clause_table))
val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
val _ =
- fold (fn thm => fn i => (Array.update (clause_arr, i, ORIG_CLAUSE thm); i + 1))
+ fold (fn thm => fn i => (Array.upd clause_arr i (ORIG_CLAUSE thm); i + 1))
cnf_clauses 0
(* replay the proof to derive the empty clause *)
(* [c_1 && ... && c_n] |- False *)
--- a/src/HOL/Tools/sat_solver.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/Tools/sat_solver.ML Sat Apr 22 10:22:41 2023 +0200
@@ -667,7 +667,7 @@
fun init_array (Prop_Logic.And (fm1, fm2), n) =
init_array (fm2, init_array (fm1, n))
| init_array (fm, n) =
- (Array.update (clauses, n, clause_to_lit_list fm); n+1)
+ (Array.upd clauses n (clause_to_lit_list fm); n+1)
val _ = init_array (cnf, 0)
(* optimization for the common case where MiniSat "R"s clauses in their *)
(* original order: *)
@@ -682,7 +682,7 @@
original_clause_id_from 0
(* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
(* testing for equality should suffice -- barring duplicate literals *)
- else if Array.sub (clauses, index) = lits then (
+ else if Array.nth clauses index = lits then (
(* success *)
last_ref_clause := index;
SOME index
--- a/src/HOL/ex/Join_Theory.thy Wed Apr 19 18:22:37 2023 +0000
+++ b/src/HOL/ex/Join_Theory.thy Sat Apr 22 10:22:41 2023 +0200
@@ -35,7 +35,7 @@
setup \<open>
fn thy =>
let val forked_thys = Par_List.map (fn i => Named_Target.theory_map (spec i) thy) (1 upto 10)
- in Theory.join_theory forked_thys end
+ in Context.join_thys forked_thys end
\<close>
term test1
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/array.ML Sat Apr 22 10:22:41 2023 +0200
@@ -0,0 +1,33 @@
+(* Title: Pure/General/array.ML
+ Author: Makarius
+
+Additional operations for structure Array, following Isabelle/ML conventions.
+*)
+
+signature ARRAY =
+sig
+ include ARRAY
+ val nth: 'a array -> int -> 'a
+ val upd: 'a array -> int -> 'a -> unit
+ val forall: ('a -> bool) -> 'a array -> bool
+ val member: ('a * 'a -> bool) -> 'a array -> 'a -> bool
+ val fold: ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
+ val fold_rev: ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
+end;
+
+structure Array: ARRAY =
+struct
+
+open Array;
+
+fun nth arr i = sub (arr, i);
+fun upd arr i x = update (arr, i, x);
+
+val forall = all;
+
+fun member eq arr x = exists (fn y => eq (x, y)) arr;
+
+fun fold f arr x = foldl (fn (a, b) => f a b) x arr;
+fun fold_rev f arr x = foldr (fn (a, b) => f a b) x arr;
+
+end;
--- a/src/Pure/General/sha1.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/General/sha1.ML Sat Apr 22 10:22:41 2023 +0200
@@ -101,12 +101,12 @@
(*hash result -- 5 words*)
val hash_array : Word32.word Array.array =
Array.fromList [0wx67452301, 0wxEFCDAB89, 0wx98BADCFE, 0wx10325476, 0wxC3D2E1F0];
- fun hash i = Array.sub (hash_array, i);
- fun add_hash x i = Array.update (hash_array, i, hash i + x);
+ val hash = Array.nth hash_array;
+ fun add_hash x i = Array.upd hash_array i (hash i + x);
(*current chunk -- 80 words*)
val chunk_array = Array.array (80, 0w0: Word32.word);
- fun chunk i = Array.sub (chunk_array, i);
+ val chunk = Array.nth chunk_array;
fun init_chunk pos =
Array.modifyi (fn (i, _) =>
if i < 16 then text (pos + i)
--- a/src/Pure/Isar/locale.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Isar/locale.ML Sat Apr 22 10:22:41 2023 +0200
@@ -355,8 +355,9 @@
unique registration serial points to mixin list*)
type T = reg Idtab.table * mixins;
val empty: T = (Idtab.empty, Inttab.empty);
- fun merge old_thys =
+ fun merge args =
let
+ val ctxt0 = Syntax.init_pretty_global (#1 (hd args));
fun recursive_merge ((regs1, mixins1), (regs2, mixins2)) : T =
(Idtab.merge eq_reg (regs1, regs2), merge_mixins (mixins1, mixins2))
handle Idtab.DUP id =>
@@ -373,9 +374,9 @@
val _ =
warning ("Removed duplicate interpretation after retrieving its mixins" ^
Position.here_list [#pos reg1, #pos reg2] ^ ":\n " ^
- Pretty.string_of (pretty_reg_inst (Syntax.init_pretty_global (#1 old_thys)) [] id));
+ Pretty.string_of (pretty_reg_inst ctxt0 [] id));
in recursive_merge ((regs1, mixins1), (regs2', mixins2')) end;
- in recursive_merge end;
+ in Library.foldl1 recursive_merge (map #2 args) end;
);
structure Local_Registrations = Proof_Data
--- a/src/Pure/Isar/named_target.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Isar/named_target.ML Sat Apr 22 10:22:41 2023 +0200
@@ -97,7 +97,7 @@
theory_registration = Generic_Target.theory_registration,
locale_dependency = fn _ => error "Not possible in theory target",
pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
- Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]}
+ Pretty.str (Context.theory_base_name (Proof_Context.theory_of ctxt))]]}
| operations (Locale locale) =
{define = Generic_Target.define (locale_foundation locale),
notes = Generic_Target.notes (Generic_Target.locale_target_notes locale),
--- a/src/Pure/Isar/outer_syntax.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Isar/outer_syntax.ML Sat Apr 22 10:22:41 2023 +0200
@@ -112,7 +112,7 @@
(* maintain commands *)
fun add_command name cmd thy =
- if member (op =) Thy_Header.bootstrap_thys (Context.theory_name thy) then thy
+ if member (op =) Thy_Header.bootstrap_thys (Context.theory_base_name thy) then thy
else
let
val _ =
--- a/src/Pure/Isar/proof_context.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Isar/proof_context.ML Sat Apr 22 10:22:41 2023 +0200
@@ -10,7 +10,7 @@
sig
val theory_of: Proof.context -> theory
val init_global: theory -> Proof.context
- val get_global: theory -> string -> Proof.context
+ val get_global: {long: bool} -> theory -> string -> Proof.context
type mode
val mode_default: mode
val mode_pattern: mode
--- a/src/Pure/Isar/toplevel.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Isar/toplevel.ML Sat Apr 22 10:22:41 2023 +0200
@@ -162,7 +162,7 @@
Toplevel =>
(case previous_theory_of state of
NONE => "at top level"
- | SOME thy => "at top level, result theory " ^ quote (Context.theory_name thy))
+ | SOME thy => "at top level, result theory " ^ quote (Context.theory_base_name thy))
| Theory (Context.Theory _) => "in theory mode"
| Theory (Context.Proof _) => "in local theory mode"
| Proof _ => "in proof mode"
--- a/src/Pure/ML/ml_antiquotations.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/ML/ml_antiquotations.ML Sat Apr 22 10:22:41 2023 +0200
@@ -65,7 +65,7 @@
ML_Antiquotation.value_embedded \<^binding>\<open>theory_context\<close>
(Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
(Theory.check {long = false} ctxt (name, pos);
- "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
+ "Proof_Context.get_global {long = false} (Proof_Context.theory_of ML_context) " ^
ML_Syntax.print_string name))) #>
ML_Antiquotation.inline \<^binding>\<open>context\<close>
--- a/src/Pure/ROOT.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/ROOT.ML Sat Apr 22 10:22:41 2023 +0200
@@ -21,6 +21,7 @@
ML_file "General/basics.ML";
ML_file "General/string.ML";
ML_file "General/vector.ML";
+ML_file "General/array.ML";
ML_file "General/symbol_explode.ML";
ML_file "Concurrent/multithreading.ML";
--- a/src/Pure/Syntax/parser.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Syntax/parser.ML Sat Apr 22 10:22:41 2023 +0200
@@ -132,16 +132,16 @@
if not new_chain then ([], lambdas)
else
let (*lookahead of chain's source*)
- val ((_, from_tks), _) = Array.sub (prods, the chain);
+ val ((_, from_tks), _) = Array.nth prods (the chain);
(*copy from's lookahead to chain's destinations*)
fun copy_lookahead to =
let
- val ((to_nts, to_tks), ps) = Array.sub (prods, to);
+ val ((to_nts, to_tks), ps) = Array.nth prods to;
val new_tks = Tokens.subtract to_tks from_tks; (*added lookahead tokens*)
val to_tks' = Tokens.merge (to_tks, new_tks);
- val _ = Array.update (prods, to, ((to_nts, to_tks'), ps));
+ val _ = Array.upd prods to ((to_nts, to_tks'), ps);
in tokens_add (to, new_tks) end;
val tos = chains_all_succs chains' [lhs];
@@ -170,7 +170,7 @@
else (NONE, nts_insert nt nts);
(*get all known starting tokens for a nonterminal*)
- fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
+ fun starts_for_nt nt = snd (fst (Array.nth prods nt));
(*update prods, lookaheads, and lambdas according to new lambda NTs*)
val (added_starts', lambdas') =
@@ -180,7 +180,7 @@
| propagate_lambda (l :: ls) added_starts lambdas =
let
(*get lookahead for lambda NT*)
- val ((dependent, l_starts), _) = Array.sub (prods, l);
+ val ((dependent, l_starts), _) = Array.nth prods l;
(*check productions whose lookahead may depend on lambda NT*)
fun examine_prods [] add_lambda nt_dependencies added_tks nt_prods =
@@ -221,7 +221,7 @@
(*check each NT whose lookahead depends on new lambda NT*)
fun process_nts nt (added_lambdas, added_starts) =
let
- val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
+ val ((old_nts, old_tks), nt_prods) = Array.nth prods nt;
(*existing productions whose lookahead may depend on l*)
val tk_prods = prods_lookup nt_prods (get_start l_starts);
@@ -235,7 +235,7 @@
val new_tks = Tokens.merge (old_tks, added_tks);
val added_lambdas' = added_lambdas |> add_lambda ? cons nt;
- val _ = Array.update (prods, nt, ((new_nts, new_tks), nt_prods'));
+ val _ = Array.upd prods nt ((new_nts, new_tks), nt_prods');
(*N.B. that because the tks component
is used to access existing
productions we have to add new
@@ -279,9 +279,9 @@
(*add lhs NT to list of dependent NTs in lookahead*)
fun add_nts nt initial =
(if initial then
- let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in
+ let val ((old_nts, old_tks), ps) = Array.nth prods nt in
if nts_member old_nts lhs then ()
- else Array.update (prods, nt, ((nts_insert lhs old_nts, old_tks), ps))
+ else Array.upd prods nt ((nts_insert lhs old_nts, old_tks), ps)
end
else (); false);
@@ -290,7 +290,7 @@
fun add_tks [] added = added
| add_tks (nt :: nts) added =
let
- val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
+ val ((old_nts, old_tks), nt_prods) = Array.nth prods nt;
val new_tks = Tokens.subtract old_tks start_tks;
@@ -306,9 +306,7 @@
|> nt = lhs ? Tokens.fold store start_tks';
val _ =
if not changed andalso Tokens.is_empty new_tks then ()
- else
- Array.update
- (prods, nt, ((old_nts, Tokens.merge (old_tks, new_tks)), nt_prods'));
+ else Array.upd prods nt ((old_nts, Tokens.merge (old_tks, new_tks)), nt_prods');
in add_tks nts (tokens_add (nt, new_tks) added) end;
val _ = nts_fold add_nts start_nts true;
in add_tks (chains_all_succs chains' [lhs]) [] end;
@@ -365,7 +363,7 @@
(*copy existing productions for new starting tokens*)
fun process_nts nt =
let
- val ((nts, tks), nt_prods) = Array.sub (prods, nt);
+ val ((nts, tks), nt_prods) = Array.nth prods nt;
val tk_prods = prods_lookup nt_prods key;
@@ -379,10 +377,10 @@
val added_tks = Tokens.subtract tks new_tks;
val tks' = Tokens.merge (tks, added_tks);
- val _ = Array.update (prods, nt, ((nts, tks'), nt_prods''));
+ val _ = Array.upd prods nt ((nts, tks'), nt_prods'');
in tokens_add (nt, added_tks) end;
- val ((dependent, _), _) = Array.sub (prods, changed_nt);
+ val ((dependent, _), _) = Array.nth prods changed_nt;
in add_starts (starts @ nts_fold process_nts dependent []) end;
in add_starts added_starts' end;
in (chains', lambdas') end;
@@ -574,7 +572,7 @@
filter
(fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec
| _ => false)
- (Array.sub (Estate, j));
+ (Array.nth Estate j);
fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) =
@@ -652,7 +650,7 @@
fun produce gram stateset i indata prev_token =
- (case Array.sub (stateset, i) of
+ (case Array.nth stateset i of
[] =>
let
val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata;
@@ -677,8 +675,8 @@
| c :: cs =>
let
val (si, sii) = PROCESSS gram stateset i c s;
- val _ = Array.update (stateset, i, si);
- val _ = Array.update (stateset, i + 1, sii);
+ val _ = Array.upd stateset i si;
+ val _ = Array.upd stateset (i + 1) sii;
in produce gram stateset (i + 1) cs c end));
@@ -693,7 +691,7 @@
val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)];
val s = length indata + 1;
val Estate = Array.array (s, []);
- val _ = Array.update (Estate, 0, S0);
+ val _ = Array.upd Estate 0 S0;
in
get_trees (produce gram Estate 0 indata Lexicon.eof)
end;
--- a/src/Pure/Thy/export_theory.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Thy/export_theory.ML Sat Apr 22 10:22:41 2023 +0200
@@ -414,7 +414,7 @@
get_dependencies parents thy |> map_index (fn (i, dep) =>
let
val xname = string_of_int (i + 1);
- val name = Long_Name.implode [Context.theory_name thy, xname];
+ val name = Long_Name.implode [Context.theory_base_name thy, xname];
val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep));
val body = encode_locale_dependency dep;
in XML.Elem (markup, body) end)
--- a/src/Pure/Thy/thy_info.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Thy/thy_info.ML Sat Apr 22 10:22:41 2023 +0200
@@ -65,7 +65,7 @@
else
let
val keywords = Thy_Header.get_keywords thy;
- val thy_name = Context.theory_name thy;
+ val thy_name = Context.theory_base_name thy;
val latex = Document_Output.present_thy options keywords thy_name segments;
in
if Options.string options "document" = "false" then ()
--- a/src/Pure/Tools/named_theorems.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Tools/named_theorems.ML Sat Apr 22 10:22:41 2023 +0200
@@ -59,7 +59,7 @@
fun clear name = map_entry name (K Thm.item_net);
-fun add_thm name th = map_entry name (Item_Net.update (Thm.trim_context th));
+fun add_thm name = map_entry name o Item_Net.update o Thm.trim_context;
fun del_thm name = map_entry name o Item_Net.remove;
val add = Thm.declaration_attribute o add_thm;
--- a/src/Pure/Tools/named_thms.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Tools/named_thms.ML Sat Apr 22 10:22:41 2023 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/Tools/named_thms.ML
Author: Makarius
-Named collections of theorems in canonical order.
+Named collections of theorems in canonical (reverse) order: OLD VERSION.
*)
signature NAMED_THMS =
@@ -27,10 +27,10 @@
val member = Item_Net.member o Data.get o Context.Proof;
-val content = Item_Net.content o Data.get;
+fun content context = map (Thm.transfer'' context) (Item_Net.content (Data.get context));
val get = content o Context.Proof;
-val add_thm = Data.map o Item_Net.update;
+val add_thm = Data.map o Item_Net.update o Thm.trim_context;
val del_thm = Data.map o Item_Net.remove;
val add = Thm.declaration_attribute add_thm;
--- a/src/Pure/Tools/thy_deps.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/Tools/thy_deps.ML Sat Apr 22 10:22:41 2023 +0200
@@ -27,8 +27,8 @@
SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs)
| NONE => K true);
fun node thy =
- ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []),
- map Context.theory_name (filter pred (Theory.parents_of thy)));
+ ((Context.theory_base_name thy, Graph_Display.content_node (Context.theory_base_name thy) []),
+ map Context.theory_base_name (filter pred (Theory.parents_of thy)));
in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
val thy_deps =
--- a/src/Pure/axclass.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/axclass.ML Sat Apr 22 10:22:41 2023 +0200
@@ -74,6 +74,8 @@
(*constant name ~> type constructor ~> (constant name, equation)*)
(string * string) Symtab.table (*constant name ~> (constant name, type constructor)*)};
+fun rep_data (Data args) = args;
+
fun make_data (axclasses, params, inst_params) =
Data {axclasses = axclasses, params = params, inst_params = inst_params};
@@ -81,22 +83,23 @@
(
type T = data;
val empty = make_data (Symtab.empty, [], (Symtab.empty, Symtab.empty));
- fun merge old_thys
- (Data {axclasses = axclasses1, params = params1, inst_params = inst_params1},
- Data {axclasses = axclasses2, params = params2, inst_params = inst_params2}) =
+ fun merge args =
let
- val old_ctxt = Syntax.init_pretty_global (fst old_thys);
+ val ctxt0 = Syntax.init_pretty_global (#1 (hd args));
- val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
- val params' =
+ fun merge_params (params1, params2) =
if null params1 then params2
else
- fold_rev (fn p => if member (op =) params1 p then I else add_param old_ctxt p)
+ fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt0 p)
params2 params1;
- val inst_params' =
+ fun merge_inst_params (inst_params1, inst_params2) =
(Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),
Symtab.merge (K true) (#2 inst_params1, #2 inst_params2));
+
+ val axclasses' = Library.foldl1 (Symtab.merge (K true)) (map (#axclasses o rep_data o #2) args);
+ val params' = Library.foldl1 merge_params (map (#params o rep_data o #2) args);
+ val inst_params' = Library.foldl1 merge_inst_params (map (#inst_params o rep_data o #2) args);
in make_data (axclasses', params', inst_params') end;
);
@@ -116,11 +119,11 @@
map_data (fn (axclasses, params, inst_params) =>
(axclasses, params, f inst_params));
-val rep_data = Data.get #> (fn Data args => args);
+val rep_theory_data = Data.get #> rep_data;
-val axclasses_of = #axclasses o rep_data;
-val params_of = #params o rep_data;
-val inst_params_of = #inst_params o rep_data;
+val axclasses_of = #axclasses o rep_theory_data;
+val params_of = #params o rep_theory_data;
+val inst_params_of = #inst_params o rep_theory_data;
(* axclasses with parameters *)
--- a/src/Pure/context.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/context.ML Sat Apr 22 10:22:41 2023 +0200
@@ -20,26 +20,29 @@
sig
val theory_of: Proof.context -> theory
val init_global: theory -> Proof.context
- val get_global: theory -> string -> Proof.context
+ val get_global: {long: bool} -> theory -> string -> Proof.context
end
end;
signature CONTEXT =
sig
include BASIC_CONTEXT
+ (*theory data*)
+ type data_kind = int
+ val data_kinds: unit -> (data_kind * Position.T) list
(*theory context*)
+ type id = int
type theory_id
val theory_id: theory -> theory_id
val timing: bool Unsynchronized.ref
val parents_of: theory -> theory list
val ancestors_of: theory -> theory list
val theory_id_ord: theory_id ord
- val theory_id_long_name: theory_id -> string
- val theory_id_name: theory_id -> string
+ val theory_id_name: {long: bool} -> theory_id -> string
val theory_long_name: theory -> string
- val theory_name: theory -> string
- val theory_name': {long: bool} -> theory -> string
- val theory_identifier: theory -> serial
+ val theory_base_name: theory -> string
+ val theory_name: {long: bool} -> theory -> string
+ val theory_identifier: theory -> id
val PureN: string
val pretty_thy: theory -> Pretty.T
val pretty_abbrev_thy: theory -> Pretty.T
@@ -52,7 +55,7 @@
val subthy: theory * theory -> bool
val trace_theories: bool Unsynchronized.ref
val theories_trace: unit -> {active_positions: Position.T list, active: int, total: int}
- val join_thys: theory * theory -> theory
+ val join_thys: theory list -> theory
val begin_thy: string -> theory list -> theory
val finish_thy: theory -> theory
val theory_data_sizeof1: theory -> (Position.T * int) list
@@ -96,15 +99,15 @@
include CONTEXT
structure Theory_Data:
sig
- val declare: Position.T -> Any.T -> (theory * theory -> Any.T * Any.T -> Any.T) -> serial
- val get: serial -> (Any.T -> 'a) -> theory -> 'a
- val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory
+ val declare: Position.T -> Any.T -> ((theory * Any.T) list -> Any.T) -> data_kind
+ val get: data_kind -> (Any.T -> 'a) -> theory -> 'a
+ val put: data_kind -> ('a -> Any.T) -> 'a -> theory -> theory
end
structure Proof_Data:
sig
- val declare: (theory -> Any.T) -> serial
- val get: serial -> (Any.T -> 'a) -> Proof.context -> 'a
- val put: serial -> ('a -> Any.T) -> 'a -> Proof.context -> Proof.context
+ val declare: (theory -> Any.T) -> data_kind
+ val get: data_kind -> (Any.T -> 'a) -> Proof.context -> 'a
+ val put: data_kind -> ('a -> Any.T) -> 'a -> Proof.context -> Proof.context
end
end;
@@ -113,24 +116,39 @@
(*** theory context ***)
+(* theory data *)
+
(*private copy avoids potential conflict of table exceptions*)
structure Datatab = Table(type key = int val ord = int_ord);
+type data_kind = int;
+val data_kind = Counter.make ();
+
(** datatype theory **)
-type stage = int * int Synchronized.var;
-fun init_stage () : stage = (0, Synchronized.var "Context.stage" 1);
-fun next_stage ((_, state): stage) = (Synchronized.change_result state (fn n => (n, n + 1)), state);
+(* implicit state *)
+
+type state = {stage: int} Synchronized.var;
+
+fun make_state () : state =
+ Synchronized.var "Context.state" {stage = 0};
+
+fun next_stage (state: state) =
+ Synchronized.change_result state (fn {stage} => (stage + 1, {stage = stage + 1}));
+
+
+(* theory_id *)
+
+type id = int;
+val new_id = Counter.make ();
abstype theory_id =
Theory_Id of
- (*identity*)
- {id: serial, (*identifier*)
- ids: Intset.T} * (*cumulative identifiers -- symbolic body content*)
- (*history*)
- {name: string, (*official theory name*)
- stage: stage option} (*index and counter for anonymous updates*)
+ {id: id, (*identifier*)
+ ids: Intset.T, (*cumulative identifiers -- symbolic body content*)
+ name: string, (*official theory name*)
+ stage: int} (*index for anonymous updates*)
with
fun rep_theory_id (Theory_Id args) = args;
@@ -138,8 +156,13 @@
end;
+
+(* theory *)
+
datatype theory =
Theory of
+ (*allocation state*)
+ state *
(*identity*)
{theory_id: theory_id,
token: Position.T Unsynchronized.ref} *
@@ -153,26 +176,28 @@
fun rep_theory (Theory args) = args;
-val theory_identity = #1 o rep_theory;
+val state_of = #1 o rep_theory;
+val theory_identity = #2 o rep_theory;
val theory_id = #theory_id o theory_identity;
-val identity_of_id = #1 o rep_theory_id;
-val identity_of = identity_of_id o theory_id;
-val history_of_id = #2 o rep_theory_id;
-val history_of = history_of_id o theory_id;
-val ancestry_of = #2 o rep_theory;
-val data_of = #3 o rep_theory;
+val identity_of = rep_theory_id o theory_id;
+val ancestry_of = #3 o rep_theory;
+val data_of = #4 o rep_theory;
-fun make_identity id ids = {id = id, ids = ids};
-fun make_history name = {name = name, stage = SOME (init_stage ())};
fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
-val theory_id_ord = int_ord o apply2 (#id o identity_of_id);
-val theory_id_long_name = #name o history_of_id;
-val theory_id_name = Long_Name.base_name o theory_id_long_name;
-val theory_long_name = #name o history_of;
-val theory_name = Long_Name.base_name o theory_long_name;
-fun theory_name' {long} = if long then theory_long_name else theory_name;
-val theory_identifier = #id o identity_of_id o theory_id;
+fun stage_final stage = stage = 0;
+
+val theory_id_stage = #stage o rep_theory_id;
+val theory_id_final = stage_final o theory_id_stage;
+val theory_id_ord = int_ord o apply2 (#id o rep_theory_id);
+fun theory_id_name {long} thy_id =
+ let val name = #name (rep_theory_id thy_id)
+ in if long then name else Long_Name.base_name name end;
+
+val theory_long_name = #name o identity_of;
+val theory_base_name = Long_Name.base_name o theory_long_name;
+fun theory_name {long} = if long then theory_long_name else theory_base_name;
+val theory_identifier = #id o identity_of;
val parents_of = #parents o ancestry_of;
val ancestors_of = #ancestors o ancestry_of;
@@ -183,9 +208,10 @@
val PureN = "Pure";
fun display_name thy_id =
- (case history_of_id thy_id of
- {name, stage = NONE} => name
- | {name, stage = SOME (i, _)} => name ^ ":" ^ string_of_int i);
+ let
+ val name = theory_id_name {long = false} thy_id;
+ val final = theory_id_final thy_id;
+ in if final then name else name ^ ":" ^ string_of_int (theory_id_stage thy_id) end;
fun display_names thy =
let
@@ -205,31 +231,24 @@
in Pretty.str_list "{" "}" abbrev end;
fun get_theory long thy name =
- if theory_name' long thy <> name then
- (case find_first (fn thy' => theory_name' long thy' = name) (ancestors_of thy) of
+ if theory_name long thy <> name then
+ (case find_first (fn thy' => theory_name long thy' = name) (ancestors_of thy) of
SOME thy' => thy'
| NONE => error ("Unknown ancestor theory " ^ quote name))
- else if is_none (#stage (history_of thy)) then thy
+ else if theory_id_final (theory_id thy) then thy
else error ("Unfinished theory " ^ quote name);
-(* build ids *)
+(* identity *)
-val merge_ids =
- apply2 (theory_id #> rep_theory_id #> #1) #>
- (fn ({id = id1, ids = ids1, ...}, {id = id2, ids = ids2, ...}) =>
- Intset.merge (ids1, ids2)
- |> Intset.insert id1
- |> Intset.insert id2);
+fun merge_ids thys =
+ fold (identity_of #> (fn {id, ids, ...} => fn acc => Intset.merge (acc, ids) |> Intset.insert id))
+ thys Intset.empty;
-
-(* equality and inclusion *)
-
-val eq_thy_id = op = o apply2 (#id o identity_of_id);
+val eq_thy_id = op = o apply2 (#id o rep_theory_id);
val eq_thy = op = o apply2 (#id o identity_of);
-val proper_subthy_id =
- apply2 (rep_theory_id #> #1) #> (fn ({id, ...}, {ids, ...}) => Intset.member ids id);
+val proper_subthy_id = apply2 rep_theory_id #> (fn ({id, ...}, {ids, ...}) => Intset.member ids id);
val proper_subthy = proper_subthy_id o apply2 theory_id;
fun subthy_id p = eq_thy_id p orelse proper_subthy_id p;
@@ -240,7 +259,7 @@
fun eq_thy_consistent (thy1, thy2) =
eq_thy (thy1, thy2) orelse
- (theory_name thy1 = theory_name thy2 andalso
+ (theory_base_name thy1 = theory_base_name thy2 andalso
raise THEORY ("Duplicate theory name", [thy1, thy2]));
fun extend_ancestors thy thys =
@@ -250,6 +269,11 @@
val merge_ancestors = merge eq_thy_consistent;
+val eq_ancestry =
+ apply2 ancestry_of #>
+ (fn ({parents, ancestors}, {parents = parents', ancestors = ancestors'}) =>
+ eq_list eq_thy (parents, parents') andalso eq_list eq_thy (ancestors, ancestors'));
+
(** theory data **)
@@ -263,33 +287,53 @@
type kind =
{pos: Position.T,
empty: Any.T,
- merge: theory * theory -> Any.T * Any.T -> Any.T};
+ merge: (theory * Any.T) list -> Any.T};
val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
-fun invoke name f k x =
+fun the_kind k =
(case Datatab.lookup (Synchronized.value kinds) k of
- SOME kind =>
- if ! timing andalso name <> "" then
- Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
- (fn () => f kind x)
- else f kind x
+ SOME kind => kind
| NONE => raise Fail "Invalid theory data identifier");
in
-fun invoke_pos k = invoke "" (K o #pos) k ();
-fun invoke_empty k = invoke "" (K o #empty) k ();
-fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys);
+fun data_kinds () =
+ Datatab.fold_rev (fn (k, {pos, ...}) => cons (k, pos)) (Synchronized.value kinds) [];
+
+val invoke_pos = #pos o the_kind;
+val invoke_empty = #empty o the_kind;
-fun declare_theory_data pos empty merge =
+fun invoke_merge kind args =
+ if ! timing then
+ Timing.cond_timeit true ("Theory_Data.merge" ^ Position.here (#pos kind))
+ (fn () => #merge kind args)
+ else #merge kind args;
+
+fun declare_data pos empty merge =
let
- val k = serial ();
+ val k = data_kind ();
val kind = {pos = pos, empty = empty, merge = merge};
val _ = Synchronized.change kinds (Datatab.update (k, kind));
in k end;
-fun merge_data thys = Datatab.join (invoke_merge thys);
+fun lookup_data k thy = Datatab.lookup (data_of thy) k;
+
+fun get_data k thy =
+ (case lookup_data k thy of
+ SOME x => x
+ | NONE => invoke_empty k);
+
+fun merge_data [] = Datatab.empty
+ | merge_data [thy] = data_of thy
+ | merge_data thys =
+ let
+ fun merge (k, kind) data =
+ (case map_filter (fn thy => lookup_data k thy |> Option.map (pair thy)) thys of
+ [] => data
+ | [(_, x)] => Datatab.default (k, x) data
+ | args => Datatab.update (k, invoke_merge kind args) data);
+ in Datatab.fold merge (Synchronized.value kinds) (data_of (hd thys)) end;
end;
@@ -331,11 +375,11 @@
total = length trace}
end;
-fun create_thy ids history ancestry data =
+fun create_thy state ids name stage ancestry data =
let
- val theory_id = make_theory_id (make_identity (serial ()) ids, history);
- val token = make_token ();
- in Theory ({theory_id = theory_id, token = token}, ancestry, data) end;
+ val theory_id = make_theory_id {id = new_id (), ids = ids, name = name, stage = stage};
+ val identity = {theory_id = theory_id, token = make_token ()};
+ in Theory (state, identity, ancestry, data) end;
end;
@@ -343,102 +387,80 @@
(* primitives *)
val pre_pure_thy =
- create_thy Intset.empty (make_history PureN) (make_ancestry [] []) Datatab.empty;
+ let
+ val state = make_state ();
+ val stage = next_stage state;
+ in create_thy state Intset.empty PureN stage (make_ancestry [] []) Datatab.empty end;
local
fun change_thy finish f thy =
let
- val ({id, ids}, {name, stage}) = rep_theory_id (theory_id thy);
- val Theory (_, ancestry, data) = thy;
+ val {name, stage, ...} = identity_of thy;
+ val Theory (state, _, ancestry, data) = thy;
val ancestry' =
- if is_none stage
+ if stage_final stage
then make_ancestry [thy] (extend_ancestors thy (ancestors_of thy))
else ancestry;
- val history' = {name = name, stage = if finish then NONE else Option.map next_stage stage};
- val ids' = Intset.insert id ids;
+ val ids' = merge_ids [thy];
+ val stage' = if finish then 0 else next_stage state;
val data' = f data;
- in create_thy ids' history' ancestry' data' end;
+ in create_thy state ids' name stage' ancestry' data' end;
in
val update_thy = change_thy false;
-val extend_thy = change_thy false I;
val finish_thy = change_thy true I;
end;
-(* join: anonymous theory nodes *)
-
-local
-
-fun bad_join (thy1, thy2) = raise THEORY ("Cannot join theories", [thy1, thy2]);
+(* join: unfinished theory nodes *)
-fun join_history thys =
- apply2 history_of thys |>
- (fn ({name, stage}, {name = name', stage = stage'}) =>
- if name = name' andalso is_some stage andalso is_some stage' then
- {name = name, stage = Option.map next_stage stage}
- else bad_join thys);
+fun join_thys [] = raise List.Empty
+ | join_thys thys =
+ let
+ val thy0 = hd thys;
+ val name0 = theory_long_name thy0;
+ val state0 = state_of thy0;
-fun join_ancestry thys =
- apply2 ancestry_of thys |>
- (fn (ancestry as {parents, ancestors}, {parents = parents', ancestors = ancestors'}) =>
- if eq_list eq_thy (parents, parents') andalso eq_list eq_thy (ancestors, ancestors')
- then ancestry else bad_join thys);
-
-in
+ fun ok thy =
+ not (theory_id_final (theory_id thy)) andalso
+ theory_long_name thy = name0 andalso
+ eq_ancestry (thy0, thy);
+ val _ =
+ (case filter_out ok thys of
+ [] => ()
+ | bad => raise THEORY ("Cannot join theories", bad));
-fun join_thys thys =
- let
- val ids = merge_ids thys;
- val history = join_history thys;
- val ancestry = join_ancestry thys;
- val data = merge_data thys (apply2 data_of thys);
- in create_thy ids history ancestry data end;
-
-end;
+ val stage = next_stage state0;
+ val ids = merge_ids thys;
+ val data = merge_data thys;
+ in create_thy state0 ids name0 stage (ancestry_of thy0) data end;
-(* merge: named theory nodes *)
-
-local
+(* merge: finished theory nodes *)
-fun merge_thys thys =
- let
- val ids = merge_ids thys;
- val history = make_history "";
- val ancestry = make_ancestry [] [];
- val data = merge_data thys (apply2 data_of thys);
- in create_thy ids history ancestry data end;
-
-fun maximal_thys thys =
- thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys);
-
-in
+fun make_parents thys =
+ let val thys' = distinct eq_thy thys
+ in thys' |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys') end;
fun begin_thy name imports =
if name = "" then error ("Bad theory name: " ^ quote name)
+ else if null imports then error "Missing theory imports"
else
let
- val parents = maximal_thys (distinct eq_thy imports);
+ val parents = make_parents imports;
val ancestors =
- Library.foldl merge_ancestors ([], map ancestors_of parents)
+ Library.foldl1 merge_ancestors (map ancestors_of parents)
|> fold extend_ancestors parents;
+ val ancestry = make_ancestry parents ancestors;
- val thy0 =
- (case parents of
- [] => error "Missing theory imports"
- | [thy] => extend_thy thy
- | thy :: thys => Library.foldl merge_thys (thy, thys));
- val ({ids, ...}, _) = rep_theory_id (theory_id thy0);
-
- val history = make_history name;
- val ancestry = make_ancestry parents ancestors;
- in create_thy ids history ancestry (data_of thy0) |> tap finish_thy end;
-
-end;
+ val state = make_state ();
+ val stage = next_stage state;
+ val ids = merge_ids parents;
+ val data = merge_data parents;
+ in create_thy state ids name stage ancestry data |> tap finish_thy end;
(* theory data *)
@@ -446,14 +468,11 @@
structure Theory_Data =
struct
-val declare = declare_theory_data;
+val declare = declare_data;
-fun get k dest thy =
- (case Datatab.lookup (data_of thy) k of
- SOME x => x
- | NONE => invoke_empty k) |> dest;
+fun get k dest thy = dest (get_data k thy);
-fun put k mk x = update_thy (Datatab.update (k, mk x));
+fun put k make x = update_thy (Datatab.update (k, make x));
fun sizeof1 k thy =
Datatab.lookup (data_of thy) k |> Option.map ML_Heap.sizeof1;
@@ -509,7 +528,7 @@
struct
fun theory_of (Proof.Context (_, thy)) = thy;
fun init_global thy = Proof.Context (init_data thy, thy);
- fun get_global thy name = init_global (get_theory {long = false} thy name);
+ fun get_global long thy name = init_global (get_theory long thy name);
end;
structure Proof_Data =
@@ -517,7 +536,7 @@
fun declare init =
let
- val k = serial ();
+ val k = data_kind ();
val _ = Synchronized.change kinds (Datatab.update (k, init));
in k end;
@@ -526,8 +545,8 @@
SOME x => x
| NONE => init_fallback k thy) |> dest;
-fun put k mk x (Proof.Context (data, thy)) =
- Proof.Context (Datatab.update (k, mk x) data, thy);
+fun put k make x (Proof.Context (data, thy)) =
+ Proof.Context (Datatab.update (k, make x) data, thy);
end;
@@ -633,7 +652,7 @@
sig
type T
val empty: T
- val merge: theory * theory -> T * T -> T
+ val merge: (theory * T) list -> T
end;
signature THEORY_DATA_ARGS =
@@ -662,7 +681,7 @@
Context.Theory_Data.declare
pos
(Data Data.empty)
- (fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2)))
+ (Data o Data.merge o map (fn (thy, Data x) => (thy, x)))
end;
val get = Context.Theory_Data.get kind (fn Data x => x);
@@ -676,7 +695,7 @@
(
type T = Data.T;
val empty = Data.empty;
- fun merge _ = Data.merge;
+ fun merge args = Library.foldl (fn (a, (_, b)) => Data.merge (a, b)) (#2 (hd args), tl args)
);
--- a/src/Pure/cterm_items.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/cterm_items.ML Sat Apr 22 10:22:41 2023 +0200
@@ -19,6 +19,8 @@
end;
+structure Ctermset = Set(Ctermtab.Key);
+
structure Cterms:
sig
@@ -54,3 +56,5 @@
fun thm_cache f = Cache.create empty lookup update f;
end;
+
+structure Thmset = Set(Thmtab.Key);
--- a/src/Pure/global_theory.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/global_theory.ML Sat Apr 22 10:22:41 2023 +0200
@@ -172,9 +172,9 @@
let
val theories =
Symtab.build (Theory.nodes_of thy |> fold (fn thy' =>
- Symtab.update (Context.theory_name thy', thy')));
+ Symtab.update (Context.theory_long_name thy', thy')));
fun transfer th =
- Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name th))) th;
+ Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_long_name th))) th;
in transfer end;
fun all_thms_of thy verbose =
--- a/src/Pure/morphism.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/morphism.ML Sat Apr 22 10:22:41 2023 +0200
@@ -22,6 +22,7 @@
typ: (typ -> typ) list,
term: (term -> term) list,
fact: (thm list -> thm list) list} -> morphism
+ val is_identity: morphism -> bool
val pretty: morphism -> Pretty.T
val binding: morphism -> binding -> binding
val binding_prefix: morphism -> (string * bool) list
@@ -82,6 +83,10 @@
term = map (pair a) term,
fact = map (pair a) fact};
+(*syntactic test only!*)
+fun is_identity (Morphism {names, binding, typ, term, fact}) =
+ null names andalso null binding andalso null typ andalso null term andalso null fact;
+
fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
--- a/src/Pure/proofterm.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/proofterm.ML Sat Apr 22 10:22:41 2023 +0200
@@ -2137,7 +2137,7 @@
fun export_standard_enabled () = Options.default_bool "export_standard_proofs";
fun export_proof_boxes_required thy =
- Context.theory_name thy = Context.PureN orelse
+ Context.theory_long_name thy = Context.PureN orelse
(export_enabled () andalso not (export_standard_enabled ()));
fun export_proof_boxes bodies =
--- a/src/Pure/sign.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/sign.ML Sat Apr 22 10:22:41 2023 +0200
@@ -129,24 +129,23 @@
tsig: Type.tsig, (*order-sorted signature of types*)
consts: Consts.T}; (*polymorphic constants*)
+fun rep_sign (Sign args) = args;
fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
structure Data = Theory_Data'
(
type T = sign;
val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
- fun merge old_thys (sign1, sign2) =
+ fun merge args =
let
- val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
- val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;
-
- val syn = Syntax.merge_syntax (syn1, syn2);
- val tsig = Type.merge_tsig (Context.Theory (fst old_thys)) (tsig1, tsig2);
- val consts = Consts.merge (consts1, consts2);
- in make_sign (syn, tsig, consts) end;
+ val context0 = Context.Theory (#1 (hd args));
+ val syn' = Library.foldl1 Syntax.merge_syntax (map (#syn o rep_sign o #2) args);
+ val tsig' = Library.foldl1 (Type.merge_tsig context0) (map (#tsig o rep_sign o #2) args);
+ val consts' = Library.foldl1 Consts.merge (map (#consts o rep_sign o #2) args);
+ in make_sign (syn', tsig', consts') end;
);
-fun rep_sg thy = Data.get thy |> (fn Sign args => args);
+val rep_sg = rep_sign o Data.get;
fun map_sign f = Data.map (fn Sign {syn, tsig, consts} => make_sign (f (syn, tsig, consts)));
@@ -514,7 +513,7 @@
val mandatory_path = map_naming o Name_Space.mandatory_path;
val qualified_path = map_naming oo Name_Space.qualified_path;
-fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
+fun local_path thy = thy |> root_path |> add_path (Context.theory_base_name thy);
fun init_naming thy =
let
--- a/src/Pure/theory.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/theory.ML Sat Apr 22 10:22:41 2023 +0200
@@ -22,7 +22,6 @@
val defs_of: theory -> Defs.T
val at_begin: (theory -> theory option) -> theory -> theory
val at_end: (theory -> theory option) -> theory -> theory
- val join_theory: theory list -> theory
val begin_theory: string * Position.T -> theory list -> theory
val end_theory: theory -> theory
val add_axiom: Proof.context -> binding * term -> theory -> theory
@@ -83,6 +82,8 @@
defs: Defs.T,
wrappers: wrapper list * wrapper list};
+fun rep_thy (Thy args) = args;
+
fun make_thy (pos, id, axioms, defs, wrappers) =
Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
@@ -90,19 +91,22 @@
(
type T = thy;
val empty = make_thy (Position.none, 0, Name_Space.empty_table Markup.axiomN, Defs.empty, ([], []));
- fun merge old_thys (thy1, thy2) =
+ fun merge args =
let
- val Thy {pos, id, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
- val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
+ val thy0 = #1 (hd args);
+ val {pos, id, ...} = rep_thy (#2 (hd args));
- val axioms' = Name_Space.merge_tables (axioms1, axioms2);
- val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
- val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
- val ens' = Library.merge (eq_snd op =) (ens1, ens2);
+ val merge_defs = Defs.merge (Defs.global_context thy0);
+ val merge_wrappers = Library.merge (eq_snd op =);
+
+ val axioms' = Library.foldl1 Name_Space.merge_tables (map (#axioms o rep_thy o #2) args);
+ val defs' = Library.foldl1 merge_defs (map (#defs o rep_thy o #2) args);
+ val bgs' = Library.foldl1 merge_wrappers (map (#1 o #wrappers o rep_thy o #2) args);
+ val ens' = Library.foldl1 merge_wrappers (map (#2 o #wrappers o rep_thy o #2) args);
in make_thy (pos, id, axioms', defs', (bgs', ens')) end;
);
-fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
+val rep_theory = rep_thy o Thy.get;
fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) =>
make_thy (f (pos, id, axioms, defs, wrappers)));
@@ -143,7 +147,7 @@
val completion_report =
Completion.make_report (name, pos)
(fn completed =>
- map (Context.theory_name' long) (ancestors_of thy)
+ map (Context.theory_name long) (ancestors_of thy)
|> filter (completed o Long_Name.base_name)
|> sort_strings
|> map (fn a => (a, (Markup.theoryN, a))));
@@ -162,13 +166,6 @@
val defs_of = #defs o rep_theory;
-(* join theory *)
-
-fun join_theory [] = raise List.Empty
- | join_theory [thy] = thy
- | join_theory thys = foldl1 Context.join_thys thys;
-
-
(* begin/end theory *)
val begin_wrappers = rev o #1 o #wrappers o rep_theory;
--- a/src/Pure/thm.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Pure/thm.ML Sat Apr 22 10:22:41 2023 +0200
@@ -66,7 +66,9 @@
val terms_of_tpairs: (term * term) list -> term list
val full_prop_of: thm -> term
val theory_id: thm -> Context.theory_id
- val theory_name: thm -> string
+ val theory_name: {long: bool} -> thm -> string
+ val theory_long_name: thm -> string
+ val theory_base_name: thm -> string
val maxidx_of: thm -> int
val maxidx_thm: thm -> int -> int
val shyps_of: thm -> sort Ord_List.T
@@ -177,7 +179,7 @@
val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} ->
bool * thm * int -> int -> thm -> thm Seq.seq
val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
- val thynames_of_arity: theory -> string * class -> string list
+ val theory_names_of_arity: {long: bool} -> theory -> string * class -> string list
val add_classrel: thm -> theory -> theory
val add_arity: thm -> theory -> theory
end;
@@ -494,7 +496,10 @@
val cert_of = #cert o rep_thm;
val theory_id = Context.certificate_theory_id o cert_of;
-val theory_name = Context.theory_id_name o theory_id;
+
+fun theory_name long = Context.theory_id_name long o theory_id;
+val theory_long_name = theory_name {long = true};
+val theory_base_name = theory_name {long = false};
val maxidx_of = #maxidx o rep_thm;
fun maxidx_thm th i = Int.max (maxidx_of th, i);
@@ -2338,10 +2343,10 @@
(* type arities *)
-fun thynames_of_arity thy (a, c) =
+fun theory_names_of_arity {long} thy (a, c) =
build (get_arities thy |> Aritytab.fold
(fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser)))
- |> sort (int_ord o apply2 #2) |> map #1;
+ |> sort (int_ord o apply2 #2) |> map (if long then #1 else Long_Name.base_name o #1);
fun insert_arity_completions thy ((t, Ss, c), (th, thy_name, ser)) (finished, arities) =
let
@@ -2399,7 +2404,7 @@
val th' = th |> unconstrainT |> tap (expose_proof thy) |> trim_context;
val prop = plain_prop_of th;
val (t, Ss, c) = Logic.dest_arity prop;
- val ar = ((t, Ss, c), (th', Context.theory_name thy, serial ()));
+ val ar = ((t, Ss, c), (th', Context.theory_long_name thy, serial ()));
in
thy
|> Sign.primitive_arity (t, Ss, [c])
--- a/src/Tools/Code/code_runtime.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Tools/Code/code_runtime.ML Sat Apr 22 10:22:41 2023 +0200
@@ -718,7 +718,7 @@
val code_binding = Path.map_binding Code_Target.code_path binding;
val preamble =
"(* Generated from " ^
- Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^
+ Path.implode (Resources.thy_path (Path.basic (Context.theory_base_name thy))) ^
"; DO NOT EDIT! *)";
val thy' = Code_Target.export code_binding (Bytes.string (preamble ^ "\n\n" ^ code)) thy;
val _ = Code_Target.code_export_message thy';
--- a/src/Tools/Code/code_symbol.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Tools/Code/code_symbol.ML Sat Apr 22 10:22:41 2023 +0200
@@ -99,7 +99,7 @@
local
val thyname_of_type = Name_Space.the_entry_theory_name o Sign.type_space;
val thyname_of_class = Name_Space.the_entry_theory_name o Sign.class_space;
- fun thyname_of_instance thy inst = case Thm.thynames_of_arity thy inst
+ fun thyname_of_instance thy inst = case Thm.theory_names_of_arity {long = false} thy inst
of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^ snd inst))
| thyname :: _ => thyname;
fun thyname_of_const thy c = case Axclass.class_of_param thy c
--- a/src/Tools/Code/code_thingol.ML Wed Apr 19 18:22:37 2023 +0000
+++ b/src/Tools/Code/code_thingol.ML Sat Apr 22 10:22:41 2023 +0200
@@ -1009,7 +1009,7 @@
let
val thy = Proof_Context.theory_of ctxt;
fun this_theory name =
- if Context.theory_name thy = name then thy
+ if Context.theory_base_name thy = name then thy
else Context.get_theory {long = false} thy name;
fun consts_of thy' =