--- a/src/Doc/Implementation/Logic.thy Thu Apr 13 15:36:07 2023 +1000
+++ b/src/Doc/Implementation/Logic.thy Thu Apr 13 15:36:30 2023 +1000
@@ -701,7 +701,7 @@
\begin{mldecls}
@{define_ML Theory.add_deps: "Defs.context -> string ->
Defs.entry -> Defs.entry list -> theory -> theory"} \\
- @{define_ML Thm_Deps.all_oracles: "thm list -> Proofterm.oracle list"} \\
+ @{define_ML Thm_Deps.all_oracles: "thm list -> Oracles.T"} \\
\end{mldecls}
\<^descr> \<^ML>\<open>Logic.all\<close>~\<open>a B\<close> produces a Pure quantification \<open>\<And>a. B\<close>, where
--- a/src/HOL/Examples/Iff_Oracle.thy Thu Apr 13 15:36:07 2023 +1000
+++ b/src/HOL/Examples/Iff_Oracle.thy Thu Apr 13 15:36:30 2023 +1000
@@ -36,7 +36,8 @@
ML \<open>iff_oracle (\<^theory>, 10)\<close>
ML \<open>
- \<^assert> (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\<open>iff_oracle\<close>]);
+ \<^assert> (map (#1 o #1) (Oracles.dest (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)])) =
+ [\<^oracle_name>\<open>iff_oracle\<close>]);
\<close>
text \<open>These oracle calls had better fail.\<close>
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Thu Apr 13 15:36:30 2023 +1000
@@ -302,7 +302,7 @@
fun fold_body_thms f =
let
- fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) =>
+ fun app n (PBody {thms, ...}) = thms |> PThms.fold (fn (i, thm_node) =>
fn (x, seen) =>
if Inttab.defined seen i then (x, seen)
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Apr 13 15:36:30 2023 +1000
@@ -104,7 +104,7 @@
else (num_thms + 1, name' :: names)
| NONE => accum)
end
- and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms
+ and app_body map_name (PBody {thms, ...}) = PThms.fold (app_thm map_name) thms
in
snd (app_body map_plain_name body (0, []))
end
--- a/src/Pure/General/name_space.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/Pure/General/name_space.ML Thu Apr 13 15:36:30 2023 +1000
@@ -11,7 +11,7 @@
sig
type entry =
{concealed: bool,
- group: serial option,
+ group: serial,
theory_long_name: string,
pos: Position.T,
serial: serial}
@@ -108,12 +108,12 @@
type entry =
{concealed: bool,
- group: serial option,
+ group: serial,
theory_long_name: string,
pos: Position.T,
serial: serial};
-fun entry_markup def kind (name, {pos, theory_long_name, serial, ...}: entry) =
+fun entry_markup def kind (name, {pos, serial, ...}: entry) =
Position.make_entity_markup def serial kind (name, pos);
fun print_entry_ref kind (name, entry) =
@@ -329,7 +329,7 @@
{scopes: Binding.scope list,
restricted: (bool * Binding.scope) option,
concealed: bool,
- group: serial option,
+ group: serial,
theory_long_name: string,
path: (string * bool) list};
@@ -379,11 +379,11 @@
map_naming (fn (scopes, restricted, concealed, group, _, path) =>
(scopes, restricted, concealed, group, theory_long_name, path));
-fun get_group (Naming {group, ...}) = group;
+fun get_group (Naming {group, ...}) = if group = 0 then NONE else SOME group;
fun set_group group =
map_naming (fn (scopes, restricted, concealed, _, theory_long_name, path) =>
- (scopes, restricted, concealed, group, theory_long_name, path));
+ (scopes, restricted, concealed, the_default 0 group, theory_long_name, path));
fun new_group naming = set_group (SOME (serial ())) naming;
val reset_group = set_group NONE;
@@ -405,7 +405,7 @@
fun qualified_path mandatory binding = map_path (fn path =>
path @ Binding.path_of (Binding.qualify_name mandatory binding ""));
-val global_naming = make_naming ([], NONE, false, NONE, "", []);
+val global_naming = make_naming ([], NONE, false, 0, "", []);
val local_naming = global_naming |> add_path Long_Name.localN;
--- a/src/Pure/General/set.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/Pure/General/set.ML Thu Apr 13 15:36:30 2023 +1000
@@ -16,6 +16,8 @@
val fold: (elem -> 'a -> 'a) -> T -> 'a -> 'a
val fold_rev: (elem -> 'a -> 'a) -> T -> 'a -> 'a
val dest: T -> elem list
+ val min: T -> elem option
+ val max: T -> elem option
val exists: (elem -> bool) -> T -> bool
val forall: (elem -> bool) -> T -> bool
val get_first: (elem -> 'a option) -> T -> 'a option
@@ -25,6 +27,7 @@
val insert: elem -> T -> T
val make: elem list -> T
val merge: T * T -> T
+ val merges: T list -> T
val remove: elem -> T -> T
val subtract: T -> T -> T
end;
@@ -49,7 +52,6 @@
Branch3 of T * elem * T * elem * T |
Size of int * T;
-(*literal copy from table.ML*)
fun make2 (Empty, e, Empty) = Leaf1 e
| make2 (Branch2 (Empty, e1, Empty), e2, right) = make2 (Leaf1 e1, e2, right)
| make2 (left, e1, Branch2 (Empty, e2, Empty)) = make2 (left, e1, Leaf1 e2)
@@ -62,7 +64,6 @@
| make2 (Empty, e1, Leaf2 (e2, e3)) = Leaf3 (e1, e2, e3)
| make2 arg = Branch2 arg;
-(*literal copy from table.ML*)
fun make3 (Empty, e1, Empty, e2, Empty) = Leaf2 (e1, e2)
| make3 (Branch2 (Empty, e1, Empty), e2, mid, e3, right) = make3 (Leaf1 e1, e2, mid, e3, right)
| make3 (left, e1, Branch2 (Empty, e2, Empty), e3, right) = make3 (left, e1, Leaf1 e2, e3, right)
@@ -72,7 +73,6 @@
| make3 (Empty, e1, Empty, e2, Leaf1 e3) = Leaf3 (e1, e2, e3)
| make3 arg = Branch3 arg;
-(*literal copy from table.ML*)
fun unmake (Leaf1 e) = Branch2 (Empty, e, Empty)
| unmake (Leaf2 (e1, e2)) = Branch3 (Empty, e1, Empty, e2, Empty)
| unmake (Leaf3 (e1, e2, e3)) =
@@ -128,33 +128,56 @@
fun fold_set f =
let
- fun fold Empty x = x
- | fold (Leaf1 e) x = f e x
- | fold (Leaf2 (e1, e2)) x = f e2 (f e1 x)
- | fold (Leaf3 (e1, e2, e3)) x = f e3 (f e2 (f e1 x))
- | fold (Branch2 (left, e, right)) x =
- fold right (f e (fold left x))
- | fold (Branch3 (left, e1, mid, e2, right)) x =
- fold right (f e2 (fold mid (f e1 (fold left x))))
- | fold (Size (_, arg)) x = fold arg x;
+ fun fold Empty a = a
+ | fold (Leaf1 e) a = f e a
+ | fold (Leaf2 (e1, e2)) a = f e2 (f e1 a)
+ | fold (Leaf3 (e1, e2, e3)) a = f e3 (f e2 (f e1 a))
+ | fold (Branch2 (left, e, right)) a =
+ fold right (f e (fold left a))
+ | fold (Branch3 (left, e1, mid, e2, right)) a =
+ fold right (f e2 (fold mid (f e1 (fold left a))))
+ | fold (Size (_, arg)) a = fold arg a;
in fold end;
fun fold_rev_set f =
let
- fun fold_rev Empty x = x
- | fold_rev (Leaf1 e) x = f e x
- | fold_rev (Leaf2 (e1, e2)) x = f e1 (f e2 x)
- | fold_rev (Leaf3 (e1, e2, e3)) x = f e1 (f e2 (f e3 x))
- | fold_rev (Branch2 (left, e, right)) x =
- fold_rev left (f e (fold_rev right x))
- | fold_rev (Branch3 (left, e1, mid, e2, right)) x =
- fold_rev left (f e1 (fold_rev mid (f e2 (fold_rev right x))))
- | fold_rev (Size (_, arg)) x = fold_rev arg x;
+ fun fold_rev Empty a = a
+ | fold_rev (Leaf1 e) a = f e a
+ | fold_rev (Leaf2 (e1, e2)) a = f e1 (f e2 a)
+ | fold_rev (Leaf3 (e1, e2, e3)) a = f e1 (f e2 (f e3 a))
+ | fold_rev (Branch2 (left, e, right)) a =
+ fold_rev left (f e (fold_rev right a))
+ | fold_rev (Branch3 (left, e1, mid, e2, right)) a =
+ fold_rev left (f e1 (fold_rev mid (f e2 (fold_rev right a))))
+ | fold_rev (Size (_, arg)) a = fold_rev arg a;
in fold_rev end;
val dest = Library.build o fold_rev_set cons;
+(* min/max entries *)
+
+fun min Empty = NONE
+ | min (Leaf1 e) = SOME e
+ | min (Leaf2 (e, _)) = SOME e
+ | min (Leaf3 (e, _, _)) = SOME e
+ | min (Branch2 (Empty, e, _)) = SOME e
+ | min (Branch3 (Empty, e, _, _, _)) = SOME e
+ | min (Branch2 (left, _, _)) = min left
+ | min (Branch3 (left, _, _, _, _)) = min left
+ | min (Size (_, arg)) = min arg;
+
+fun max Empty = NONE
+ | max (Leaf1 e) = SOME e
+ | max (Leaf2 (_, e)) = SOME e
+ | max (Leaf3 (_, _, e)) = SOME e
+ | max (Branch2 (_, e, Empty)) = SOME e
+ | max (Branch3 (_, _, _, e, Empty)) = SOME e
+ | max (Branch2 (_, _, right)) = max right
+ | max (Branch3 (_, _, _, _, right)) = max right
+ | max (Size (_, arg)) = max arg;
+
+
(* exists and forall *)
fun exists pred =
@@ -321,6 +344,9 @@
fun make elems = build (fold insert elems);
+
+(* merge *)
+
fun merge (set1, set2) =
if pointer_eq (set1, set2) then set1
else if is_empty set1 then set2
@@ -329,6 +355,8 @@
then fold_set insert set2 set1
else fold_set insert set1 set2;
+fun merges sets = Library.foldl merge (empty, sets);
+
(* remove *)
@@ -341,7 +369,6 @@
exception UNDEF of elem;
-(*literal copy from table.ML*)
fun del (SOME k) Empty = raise UNDEF k
| del NONE Empty = raise Match
| del NONE (Leaf1 p) = (p, (true, Empty))
--- a/src/Pure/General/table.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/Pure/General/table.ML Thu Apr 13 15:36:30 2023 +1000
@@ -45,6 +45,9 @@
val join: (key -> 'a * 'a -> 'a) (*exception SAME*) ->
'a table * 'a table -> 'a table (*exception DUP*)
val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUP*)
+ val joins: (key -> 'a * 'a -> 'a) (*exception SAME*) ->
+ 'a table list -> 'a table (*exception DUP*)
+ val merges: ('a * 'a -> bool) -> 'a table list -> 'a table (*exception DUP*)
val delete: key -> 'a table -> 'a table (*exception UNDEF*)
val delete_safe: key -> 'a table -> 'a table
val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool
@@ -80,40 +83,39 @@
datatype 'a table =
Empty |
Leaf1 of key * 'a |
- Leaf2 of (key * 'a) * (key * 'a) |
- Leaf3 of (key * 'a) * (key * 'a) * (key * 'a) |
+ Leaf2 of key * 'a * key * 'a |
+ Leaf3 of key * 'a * key * 'a * key * 'a |
Branch2 of 'a table * (key * 'a) * 'a table |
Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table |
Size of int * 'a table;
-(*literal copy from set.ML*)
fun make2 (Empty, e, Empty) = Leaf1 e
| make2 (Branch2 (Empty, e1, Empty), e2, right) = make2 (Leaf1 e1, e2, right)
| make2 (left, e1, Branch2 (Empty, e2, Empty)) = make2 (left, e1, Leaf1 e2)
- | make2 (Branch3 (Empty, e1, Empty, e2, Empty), e3, right) = make2 (Leaf2 (e1, e2), e3, right)
- | make2 (left, e1, Branch3 (Empty, e2, Empty, e3, Empty)) = make2 (left, e1, Leaf2 (e2, e3))
- | make2 (Leaf1 e1, e2, Empty) = Leaf2 (e1, e2)
- | make2 (Empty, e1, Leaf1 e2) = Leaf2 (e1, e2)
- | make2 (Leaf1 e1, e2, Leaf1 e3) = Leaf3 (e1, e2, e3)
- | make2 (Leaf2 (e1, e2), e3, Empty) = Leaf3 (e1, e2, e3)
- | make2 (Empty, e1, Leaf2 (e2, e3)) = Leaf3 (e1, e2, e3)
+ | make2 (Branch3 (Empty, (k1, x1), Empty, (k2, x2), Empty), e3, right) =
+ make2 (Leaf2 (k1, x1, k2, x2), e3, right)
+ | make2 (left, e1, Branch3 (Empty, (k2, x2), Empty, (k3, x3), Empty)) =
+ make2 (left, e1, Leaf2 (k2, x2, k3, x3))
+ | make2 (Leaf1 (k1, x1), (k2, x2), Empty) = Leaf2 (k1, x1, k2, x2)
+ | make2 (Empty, (k1, x1), Leaf1 (k2, x2)) = Leaf2 (k1, x1, k2, x2)
+ | make2 (Leaf1 (k1, x1), (k2, x2), Leaf1 (k3, x3)) = Leaf3 (k1, x1, k2, x2, k3, x3)
+ | make2 (Leaf2 (k1, x1, k2, x2), (k3, x3), Empty) = Leaf3 (k1, x1, k2, x2, k3, x3)
+ | make2 (Empty, (k1, x1), Leaf2 (k2, x2, k3, x3)) = Leaf3 (k1, x1, k2, x2, k3, x3)
| make2 arg = Branch2 arg;
-(*literal copy from set.ML*)
-fun make3 (Empty, e1, Empty, e2, Empty) = Leaf2 (e1, e2)
+fun make3 (Empty, (k1, x1), Empty, (k2, x2), Empty) = Leaf2 (k1, x1, k2, x2)
| make3 (Branch2 (Empty, e1, Empty), e2, mid, e3, right) = make3 (Leaf1 e1, e2, mid, e3, right)
| make3 (left, e1, Branch2 (Empty, e2, Empty), e3, right) = make3 (left, e1, Leaf1 e2, e3, right)
| make3 (left, e1, mid, e2, Branch2 (Empty, e3, Empty)) = make3 (left, e1, mid, e2, Leaf1 e3)
- | make3 (Leaf1 e1, e2, Empty, e3, Empty) = Leaf3 (e1, e2, e3)
- | make3 (Empty, e1, Leaf1 e2, e3, Empty) = Leaf3 (e1, e2, e3)
- | make3 (Empty, e1, Empty, e2, Leaf1 e3) = Leaf3 (e1, e2, e3)
+ | make3 (Leaf1 (k1, x1), (k2, x2), Empty, (k3, x3), Empty) = Leaf3 (k1, x1, k2, x2, k3, x3)
+ | make3 (Empty, (k1, x1), Leaf1 (k2, x2), (k3, x3), Empty) = Leaf3 (k1, x1, k2, x2, k3, x3)
+ | make3 (Empty, (k1, x1), Empty, (k2, x2), Leaf1 (k3, x3)) = Leaf3 (k1, x1, k2, x2, k3, x3)
| make3 arg = Branch3 arg;
-(*literal copy from set.ML*)
fun unmake (Leaf1 e) = Branch2 (Empty, e, Empty)
- | unmake (Leaf2 (e1, e2)) = Branch3 (Empty, e1, Empty, e2, Empty)
- | unmake (Leaf3 (e1, e2, e3)) =
- Branch2 (Branch2 (Empty, e1, Empty), e2, Branch2 (Empty, e3, Empty))
+ | unmake (Leaf2 (k1, x1, k2, x2)) = Branch3 (Empty, (k1, x1), Empty, (k2, x2), Empty)
+ | unmake (Leaf3 (k1, x1, k2, x2, k3, x3)) =
+ Branch2 (Branch2 (Empty, (k1, x1), Empty), (k2, x2), Branch2 (Empty, (k3, x3), Empty))
| unmake (Size (_, arg)) = arg
| unmake arg = arg;
@@ -167,9 +169,8 @@
let
fun map Empty = Empty
| map (Leaf1 (k, x)) = Leaf1 (k, f k x)
- | map (Leaf2 ((k1, x1), (k2, x2))) = Leaf2 ((k1, f k1 x1), (k2, f k2 x2))
- | map (Leaf3 ((k1, x1), (k2, x2), (k3, x3))) =
- Leaf3 ((k1, f k1 x1), (k2, f k2 x2), (k3, f k3 x3))
+ | map (Leaf2 (k1, x1, k2, x2)) = Leaf2 (k1, f k1 x1, k2, f k2 x2)
+ | map (Leaf3 (k1, x1, k2, x2, k3, x3)) = Leaf3 (k1, f k1 x1, k2, f k2 x2, k3, f k3 x3)
| map (Branch2 (left, (k, x), right)) =
Branch2 (map left, (k, f k x), map right)
| map (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
@@ -179,28 +180,28 @@
fun fold_table f =
let
- fun fold Empty x = x
- | fold (Leaf1 e) x = f e x
- | fold (Leaf2 (e1, e2)) x = f e2 (f e1 x)
- | fold (Leaf3 (e1, e2, e3)) x = f e3 (f e2 (f e1 x))
- | fold (Branch2 (left, e, right)) x =
- fold right (f e (fold left x))
- | fold (Branch3 (left, e1, mid, e2, right)) x =
- fold right (f e2 (fold mid (f e1 (fold left x))))
- | fold (Size (_, arg)) x = fold arg x;
+ fun fold Empty a = a
+ | fold (Leaf1 e) a = f e a
+ | fold (Leaf2 (k1, x1, k2, x2)) a = f (k2, x2) (f (k1, x1) a)
+ | fold (Leaf3 (k1, x1, k2, x2, k3, x3)) a = f (k3, x3) (f (k2, x2) (f (k1, x1) a))
+ | fold (Branch2 (left, e, right)) a =
+ fold right (f e (fold left a))
+ | fold (Branch3 (left, e1, mid, e2, right)) a =
+ fold right (f e2 (fold mid (f e1 (fold left a))))
+ | fold (Size (_, arg)) a = fold arg a;
in fold end;
fun fold_rev_table f =
let
- fun fold_rev Empty x = x
- | fold_rev (Leaf1 e) x = f e x
- | fold_rev (Leaf2 (e1, e2)) x = f e1 (f e2 x)
- | fold_rev (Leaf3 (e1, e2, e3)) x = f e1 (f e2 (f e3 x))
- | fold_rev (Branch2 (left, e, right)) x =
- fold_rev left (f e (fold_rev right x))
- | fold_rev (Branch3 (left, e1, mid, e2, right)) x =
- fold_rev left (f e1 (fold_rev mid (f e2 (fold_rev right x))))
- | fold_rev (Size (_, arg)) x = fold_rev arg x;
+ fun fold_rev Empty a = a
+ | fold_rev (Leaf1 e) a = f e a
+ | fold_rev (Leaf2 (k1, x1, k2, x2)) a = f (k1, x1) (f (k2, x2) a)
+ | fold_rev (Leaf3 (k1, x1, k2, x2, k3, x3)) a = f (k1, x1) (f (k2, x2) (f (k3, x3) a))
+ | fold_rev (Branch2 (left, e, right)) a =
+ fold_rev left (f e (fold_rev right a))
+ | fold_rev (Branch3 (left, e1, mid, e2, right)) a =
+ fold_rev left (f e1 (fold_rev mid (f e2 (fold_rev right a))))
+ | fold_rev (Size (_, arg)) a = fold_rev arg a;
in fold_rev end;
fun dest tab = Library.build (fold_rev_table cons tab);
@@ -211,8 +212,8 @@
fun min Empty = NONE
| min (Leaf1 e) = SOME e
- | min (Leaf2 (e, _)) = SOME e
- | min (Leaf3 (e, _, _)) = SOME e
+ | min (Leaf2 (k, x, _, _)) = SOME (k, x)
+ | min (Leaf3 (k, x, _, _, _, _)) = SOME (k, x)
| min (Branch2 (Empty, e, _)) = SOME e
| min (Branch3 (Empty, e, _, _, _)) = SOME e
| min (Branch2 (left, _, _)) = min left
@@ -221,8 +222,8 @@
fun max Empty = NONE
| max (Leaf1 e) = SOME e
- | max (Leaf2 (_, e)) = SOME e
- | max (Leaf3 (_, _, e)) = SOME e
+ | max (Leaf2 (_, _, k, x)) = SOME (k, x)
+ | max (Leaf3 (_, _, _, _, k, x)) = SOME (k, x)
| max (Branch2 (_, e, Empty)) = SOME e
| max (Branch3 (_, _, _, e, Empty)) = SOME e
| max (Branch2 (_, _, right)) = max right
@@ -236,8 +237,9 @@
let
fun ex Empty = false
| ex (Leaf1 e) = pred e
- | ex (Leaf2 (e1, e2)) = pred e1 orelse pred e2
- | ex (Leaf3 (e1, e2, e3)) = pred e1 orelse pred e2 orelse pred e3
+ | ex (Leaf2 (k1, x1, k2, x2)) = pred (k1, x1) orelse pred (k2, x2)
+ | ex (Leaf3 (k1, x1, k2, x2, k3, x3)) =
+ pred (k1, x1) orelse pred (k2, x2) orelse pred (k3, x3)
| ex (Branch2 (left, e, right)) =
ex left orelse pred e orelse ex right
| ex (Branch3 (left, e1, mid, e2, right)) =
@@ -254,15 +256,15 @@
let
fun get Empty = NONE
| get (Leaf1 e) = f e
- | get (Leaf2 (e1, e2)) =
- (case f e1 of
- NONE => f e2
+ | get (Leaf2 (k1, x1, k2, x2)) =
+ (case f (k1, x1) of
+ NONE => f (k2, x2)
| some => some)
- | get (Leaf3 (e1, e2, e3)) =
- (case f e1 of
+ | get (Leaf3 (k1, x1, k2, x2, k3, x3)) =
+ (case f (k1, x1) of
NONE =>
- (case f e2 of
- NONE => f e3
+ (case f (k2, x2) of
+ NONE => f (k3, x3)
| some => some)
| some => some)
| get (Branch2 (left, e, right)) =
@@ -299,12 +301,12 @@
fun look Empty = NONE
| look (Leaf1 (k, x)) =
if key_eq k then SOME x else NONE
- | look (Leaf2 ((k1, x1), (k2, x2))) =
+ | look (Leaf2 (k1, x1, k2, x2)) =
(case key_ord k1 of
LESS => NONE
| EQUAL => SOME x1
| GREATER => if key_eq k2 then SOME x2 else NONE)
- | look (Leaf3 ((k1, x1), (k2, x2), (k3, x3))) =
+ | look (Leaf3 (k1, x1, k2, x2, k3, x3)) =
(case key_ord k2 of
LESS => if key_eq k1 then SOME x1 else NONE
| EQUAL => SOME x2
@@ -334,12 +336,12 @@
fun look Empty = NONE
| look (Leaf1 (k, x)) =
if key_eq k then SOME (k, x) else NONE
- | look (Leaf2 ((k1, x1), (k2, x2))) =
+ | look (Leaf2 (k1, x1, k2, x2)) =
(case key_ord k1 of
LESS => NONE
| EQUAL => SOME (k1, x1)
| GREATER => if key_eq k2 then SOME (k2, x2) else NONE)
- | look (Leaf3 ((k1, x1), (k2, x2), (k3, x3))) =
+ | look (Leaf3 (k1, x1, k2, x2, k3, x3)) =
(case key_ord k2 of
LESS => if key_eq k1 then SOME (k1, x1) else NONE
| EQUAL => SOME (k2, x2)
@@ -368,12 +370,12 @@
fun def Empty = false
| def (Leaf1 (k, _)) = key_eq k
- | def (Leaf2 ((k1, _), (k2, _))) =
+ | def (Leaf2 (k1, _, k2, _)) =
(case key_ord k1 of
LESS => false
| EQUAL => true
| GREATER => key_eq k2)
- | def (Leaf3 ((k1, _), (k2, _), (k3, _))) =
+ | def (Leaf3 (k1, _, k2, _, k3, _)) =
(case key_ord k2 of
LESS => key_eq k1
| EQUAL => true
@@ -477,23 +479,22 @@
fun if_equal ord x y = if is_equal ord then x else y;
-(*literal copy from set.ML*)
fun del (SOME k) Empty = raise UNDEF k
| del NONE Empty = raise Match
| del NONE (Leaf1 p) = (p, (true, Empty))
- | del NONE (Leaf2 (p, q)) = (p, (false, Leaf1 q))
+ | del NONE (Leaf2 (k1, x1, k2, x2)) = ((k1, x1), (false, Leaf1 (k2, x2)))
| del k (Leaf1 p) =
(case compare k p of
EQUAL => (p, (true, Empty))
| _ => raise UNDEF (the k))
- | del k (Leaf2 (p, q)) =
- (case compare k p of
- EQUAL => (p, (false, Leaf1 q))
+ | del k (Leaf2 (k1, x1, k2, x2)) =
+ (case compare k (k1, x1) of
+ EQUAL => ((k1, x1), (false, Leaf1 (k2, x2)))
| _ =>
- (case compare k q of
- EQUAL => (q, (false, Leaf1 p))
+ (case compare k (k2, x2) of
+ EQUAL => ((k2, x2), (false, Leaf1 (k1, x1)))
| _ => raise UNDEF (the k)))
- | del k (Leaf3 (p, q, r)) = del k (Branch2 (Leaf1 p, q, Leaf1 r))
+ | del k (Leaf3 (k1, x1, k2, x2, k3, x3)) = del k (Branch2 (Leaf1 (k1, x1), (k2, x2), Leaf1 (k3, x3)))
| del k (Branch2 (l, p, r)) =
(case compare k p of
LESS =>
@@ -593,6 +594,9 @@
fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key);
+fun joins f tabs = Library.foldl (join f) (empty, tabs);
+fun merges eq tabs = Library.foldl (merge eq) (empty, tabs);
+
(* list tables *)
--- a/src/Pure/Isar/locale.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/Pure/Isar/locale.ML Thu Apr 13 15:36:30 2023 +1000
@@ -346,23 +346,19 @@
structure Idtab = Table(type key = string * term list val ord = total_ident_ord);
type reg = {morphisms: morphism * morphism, pos: Position.T, serial: serial};
-type regs = reg Idtab.table;
-
-val join_regs : regs * regs -> regs =
- Idtab.join (fn id => fn (reg1, reg2) =>
- if #serial reg1 = #serial reg2 then raise Idtab.SAME else raise Idtab.DUP id);
+val eq_reg: reg * reg -> bool = op = o apply2 #serial;
(* FIXME consolidate with locale dependencies, consider one data slot only *)
structure Global_Registrations = Theory_Data'
(
(*registrations, indexed by locale name and instance;
unique registration serial points to mixin list*)
- type T = regs * mixins;
+ type T = reg Idtab.table * mixins;
val empty: T = (Idtab.empty, Inttab.empty);
fun merge old_thys =
let
fun recursive_merge ((regs1, mixins1), (regs2, mixins2)) : T =
- (join_regs (regs1, regs2), merge_mixins (mixins1, mixins2))
+ (Idtab.merge eq_reg (regs1, regs2), merge_mixins (mixins1, mixins2))
handle Idtab.DUP id =>
(*distinct interpretations with same base: merge their mixins*)
let
--- a/src/Pure/Proof/extraction.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/Pure/Proof/extraction.ML Thu Apr 13 15:36:30 2023 +1000
@@ -180,11 +180,7 @@
(fn Oracle (name, prop, _) => apfst (cons ((name, Position.none), SOME prop))
| PThm (header, thm_body) => apsnd (cons (Proofterm.make_thm header thm_body))
| _ => I);
- val body =
- PBody
- {oracles = Ord_List.make Proofterm.oracle_ord oracles,
- thms = Ord_List.make Proofterm.thm_ord thms,
- proof = prf};
+ val body = PBody {oracles = Oracles.make oracles, thms = PThms.make thms, proof = prf};
in Proofterm.thm_body body end;
--- a/src/Pure/Proof/proof_syntax.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/Pure/Proof/proof_syntax.ML Thu Apr 13 15:36:30 2023 +1000
@@ -224,11 +224,11 @@
fun proof_syntax prf =
let
- val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true
- (fn PThm ({name, ...}, _) => if name <> "" then Symtab.update (name, ()) else I
- | _ => I) [prf] Symtab.empty);
- val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true
- (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty);
+ val thm_names = Symset.dest (Proofterm.fold_proof_atoms true
+ (fn PThm ({name, ...}, _) => if name <> "" then Symset.insert name else I
+ | _ => I) [prf] Symset.empty);
+ val axm_names = Symset.dest (Proofterm.fold_proof_atoms true
+ (fn PAxm (name, _, _) => Symset.insert name | _ => I) [prf] Symset.empty);
in
add_proof_syntax #>
add_proof_atom_consts
--- a/src/Pure/Syntax/parser.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/Pure/Syntax/parser.ML Thu Apr 13 15:36:30 2023 +1000
@@ -51,21 +51,10 @@
(* tokens *)
-structure Tokens = Table(type key = Lexicon.token val ord = Lexicon.tokens_match_ord);
+structure Tokens = Set(type key = Lexicon.token val ord = Lexicon.tokens_match_ord);
-type tokens = Tokens.set;
-val tokens_empty: tokens = Tokens.empty;
-val tokens_merge: tokens * tokens -> tokens = Tokens.merge (K true);
-fun tokens_insert tk : tokens -> tokens = Tokens.insert_set tk;
-fun tokens_remove tk : tokens -> tokens = Tokens.remove_set tk;
-fun tokens_member (tokens: tokens) = Tokens.defined tokens;
-fun tokens_is_empty (tokens: tokens) = Tokens.is_empty tokens;
-fun tokens_fold f (tokens: tokens) = Tokens.fold (f o #1) tokens;
-val tokens_union = tokens_fold tokens_insert;
-val tokens_subtract = tokens_fold tokens_remove;
-fun tokens_find P (tokens: tokens) =
- Tokens.get_first (fn (tok, ()) => if P tok then SOME tok else NONE) tokens;
-fun tokens_add (nt: nt, tokens) = if tokens_is_empty tokens then I else cons (nt, tokens);
+fun tokens_find P tokens = Tokens.get_first (fn tok => if P tok then SOME tok else NONE) tokens;
+fun tokens_add (nt: nt, tokens) = if Tokens.is_empty tokens then I else cons (nt, tokens);
(* productions *)
@@ -74,17 +63,18 @@
Terminal of Lexicon.token |
Nonterminal of nt * int; (*(tag, prio)*)
-type prods = (symb list * string * int) list Tokens.table; (*start_token ~> [(rhs, name, prio)]*)
+structure Prods = Table(Tokens.Key);
+type prods = (symb list * string * int) list Prods.table; (*start_token ~> [(rhs, name, prio)]*)
-val prods_empty: prods = Tokens.empty;
-fun prods_lookup (prods: prods) = Tokens.lookup_list prods;
-fun prods_update entry : prods -> prods = Tokens.update entry;
-fun prods_content (prods: prods) = distinct (op =) (maps #2 (Tokens.dest prods));
+val prods_empty: prods = Prods.empty;
+fun prods_lookup (prods: prods) = Prods.lookup_list prods;
+fun prods_update entry : prods -> prods = Prods.update entry;
+fun prods_content (prods: prods) = distinct (op =) (maps #2 (Prods.dest prods));
-type nt_gram = (nts * tokens) * prods; (*dependent_nts, start_tokens, prods*)
+type nt_gram = (nts * Tokens.T) * prods; (*dependent_nts, start_tokens, prods*)
(*depent_nts is a set of all NTs whose lookahead depends on this NT's lookahead*)
-val nt_gram_empty: nt_gram = ((nts_empty, tokens_empty), prods_empty);
+val nt_gram_empty: nt_gram = ((nts_empty, Tokens.empty), prods_empty);
type chains = unit Int_Graph.T;
fun chains_preds (chains: chains) = Int_Graph.immediate_preds chains;
@@ -116,7 +106,7 @@
fun get_start tks =
(case Tokens.min tks of
- SOME (tk, _) => tk
+ SOME tk => tk
| NONE => unknown_start);
fun add_production prods (lhs, new_prod as (rhs, _, pri)) (chains, lambdas) =
@@ -149,8 +139,8 @@
let
val ((to_nts, to_tks), ps) = Array.sub (prods, to);
- val new_tks = tokens_subtract to_tks from_tks; (*added lookahead tokens*)
- val to_tks' = tokens_merge (to_tks, new_tks);
+ 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));
in tokens_add (to, new_tks) end;
@@ -204,12 +194,12 @@
is_none tk andalso nts_subset (nts, lambdas);
val new_tks =
- tokens_empty
- |> fold tokens_insert (the_list tk)
- |> nts_fold (tokens_union o starts_for_nt) nts
- |> tokens_subtract l_starts;
+ Tokens.empty
+ |> fold Tokens.insert (the_list tk)
+ |> nts_fold (curry Tokens.merge o starts_for_nt) nts
+ |> Tokens.subtract l_starts;
- val added_tks' = tokens_merge (added_tks, new_tks);
+ val added_tks' = Tokens.merge (added_tks, new_tks);
val nt_dependencies' = nts_merge (nt_dependencies, nts);
@@ -218,7 +208,7 @@
prods_update (tk, p :: prods_lookup nt_prods tk) nt_prods;
val nt_prods' = nt_prods
- |> tokens_fold copy new_tks
+ |> Tokens.fold copy new_tks
|> new_lambda ? copy Lexicon.dummy;
in
examine_prods ps (add_lambda orelse new_lambda)
@@ -239,10 +229,10 @@
(*add_lambda is true if an existing production of the nt
produces lambda due to the new lambda NT l*)
val (add_lambda, nt_dependencies, added_tks, nt_prods') =
- examine_prods tk_prods false nts_empty tokens_empty nt_prods;
+ examine_prods tk_prods false nts_empty Tokens.empty nt_prods;
val new_nts = nts_merge (old_nts, nt_dependencies);
- val new_tks = tokens_merge (old_tks, added_tks);
+ 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'));
@@ -276,14 +266,14 @@
val (start_tk, start_nts) = lookahead_dependency lambdas' rhs nts_empty;
val start_tks =
- tokens_empty
- |> fold tokens_insert (the_list start_tk)
- |> nts_fold (tokens_union o starts_for_nt) start_nts;
+ Tokens.empty
+ |> fold Tokens.insert (the_list start_tk)
+ |> nts_fold (curry Tokens.merge o starts_for_nt) start_nts;
val start_tks' =
start_tks
- |> (if is_some new_lambdas then tokens_insert Lexicon.dummy
- else if tokens_is_empty start_tks then tokens_insert unknown_start
+ |> (if is_some new_lambdas then Tokens.insert Lexicon.dummy
+ else if Tokens.is_empty start_tks then Tokens.insert unknown_start
else I);
(*add lhs NT to list of dependent NTs in lookahead*)
@@ -302,7 +292,7 @@
let
val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
- val new_tks = tokens_subtract old_tks start_tks;
+ val new_tks = Tokens.subtract old_tks start_tks;
(*store new production*)
fun store tk (prods, _) =
@@ -313,12 +303,12 @@
in (prods', true) end;
val (nt_prods', changed) = (nt_prods, false)
- |> nt = lhs ? tokens_fold store start_tks';
+ |> nt = lhs ? Tokens.fold store start_tks';
val _ =
- if not changed andalso tokens_is_empty new_tks then ()
+ 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'));
+ (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;
@@ -333,7 +323,7 @@
(*token under which old productions which
depend on changed_nt could be stored*)
val key =
- tokens_find (not o tokens_member new_tks) (starts_for_nt changed_nt)
+ tokens_find (not o Tokens.member new_tks) (starts_for_nt changed_nt)
|> the_default unknown_start;
(*copy productions whose lookahead depends on changed_nt;
@@ -354,7 +344,7 @@
val lambda =
not (nts_is_unique depends) orelse
not (nts_is_empty depends) andalso is_some tk
- andalso tokens_member new_tks (the tk);
+ andalso Tokens.member new_tks (the tk);
(*associate production with new starting tokens*)
fun copy tk nt_prods =
@@ -367,7 +357,7 @@
have to look for duplicates*)
in prods_update (tk, tk_prods') nt_prods end;
val result =
- if update then (tk_prods, tokens_fold copy new_tks nt_prods)
+ if update then (tk_prods, Tokens.fold copy new_tks nt_prods)
else if key = unknown_start then (p :: tk_prods, nt_prods)
else (tk_prods, nt_prods);
in update_prods ps result end;
@@ -387,8 +377,8 @@
prods_update (key, tk_prods') nt_prods'
else nt_prods';
- val added_tks = tokens_subtract tks new_tks;
- val tks' = tokens_merge (tks, added_tks);
+ val added_tks = Tokens.subtract tks new_tks;
+ val tks' = Tokens.merge (tks, added_tks);
val _ = Array.update (prods, nt, ((nts, tks'), nt_prods''));
in tokens_add (nt, added_tks) end;
--- a/src/Pure/proofterm.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/Pure/proofterm.ML Thu Apr 13 15:36:30 2023 +1000
@@ -6,6 +6,16 @@
infix 8 % %% %>;
+structure Oracles = Set(
+ type key = (string * Position.T) * term option
+ val ord = prod_ord (prod_ord fast_string_ord Position.ord) (option_ord Term_Ord.fast_term_ord)
+);
+
+structure PThms = Table(
+ type key = serial
+ val ord = rev_order o int_ord
+);
+
signature PROOFTERM =
sig
type thm_header =
@@ -26,11 +36,12 @@
| Oracle of string * term * typ list option
| PThm of thm_header * thm_body
and proof_body = PBody of
- {oracles: ((string * Position.T) * term option) Ord_List.T,
- thms: (serial * thm_node) Ord_List.T,
+ {oracles: Oracles.T,
+ thms: thm_node PThms.table,
proof: proof}
- type oracle = (string * Position.T) * term option
type thm = serial * thm_node
+ type thms = thm_node PThms.table
+ val merge_thms: thms * thms -> thms
exception MIN_PROOF of unit
val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
@@ -44,17 +55,13 @@
val thm_node_name: thm_node -> string
val thm_node_prop: thm_node -> term
val thm_node_body: thm_node -> proof_body future
- val thm_node_thms: thm_node -> thm list
- val join_thms: thm list -> proof_body list
+ val thm_node_thms: thm_node -> thms
+ val join_thms: thms -> proof_body list
val make_thm: thm_header -> thm_body -> thm
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
val fold_body_thms:
({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
proof_body list -> 'a -> 'a
- val oracle_ord: oracle ord
- val thm_ord: thm ord
- val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
- val unions_thms: thm Ord_List.T list -> thm Ord_List.T
val no_proof_body: proof -> proof_body
val no_thm_names: proof -> proof
val no_thm_proofs: proof -> proof
@@ -217,8 +224,8 @@
| Oracle of string * term * typ list option
| PThm of thm_header * thm_body
and proof_body = PBody of
- {oracles: ((string * Position.T) * term option) Ord_List.T,
- thms: (serial * thm_node) Ord_List.T,
+ {oracles: Oracles.T,
+ thms: thm_node PThms.table,
proof: proof}
and thm_body =
Thm_Body of {open_proof: proof -> proof, body: proof_body future}
@@ -226,13 +233,10 @@
Thm_Node of {theory_name: string, name: string, prop: term,
body: proof_body future, export: unit lazy, consolidate: unit lazy};
-type oracle = (string * Position.T) * term option;
-val oracle_ord: oracle ord =
- prod_ord (prod_ord fast_string_ord Position.ord) (option_ord Term_Ord.fast_term_ord);
+type thm = serial * thm_node;
-type thm = serial * thm_node;
-val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
-
+type thms = thm_node PThms.table;
+val merge_thms: thms * thms -> thms = PThms.merge (K true);
exception MIN_PROOF of unit;
@@ -258,11 +262,11 @@
val thm_node_export = #export o rep_thm_node;
val thm_node_consolidate = #consolidate o rep_thm_node;
-fun join_thms (thms: thm list) =
- Future.joins (map (thm_node_body o #2) thms);
+fun join_thms (thms: thms) =
+ Future.joins (PThms.fold_rev (cons o thm_node_body o #2) thms []);
val consolidate_bodies =
- maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
+ maps (fn PBody {thms, ...} => PThms.fold_rev (cons o thm_node_consolidate o #2) thms [])
#> Lazy.consolidate #> map Lazy.force #> ignore;
fun make_thm_node theory_name name prop body export =
@@ -291,35 +295,32 @@
| app (prf % _) = app prf
| app (prf1 %% prf2) = app prf1 #> app prf2
| app (prf as PThm ({serial = i, ...}, Thm_Body {body, ...})) = (fn (x, seen) =>
- if Inttab.defined seen i then (x, seen)
+ if Intset.member seen i then (x, seen)
else
let val (x', seen') =
- (if all then app (join_proof body) else I) (x, Inttab.update (i, ()) seen)
+ (if all then app (join_proof body) else I) (x, Intset.insert i seen)
in (f prf x', seen') end)
| app prf = (fn (x, seen) => (f prf x, seen));
- in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end;
+ in fn prfs => fn x => #1 (fold app prfs (x, Intset.empty)) end;
fun fold_body_thms f =
let
fun app (PBody {thms, ...}) =
- tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
- if Inttab.defined seen i then (x, seen)
+ tap join_thms thms |> PThms.fold (fn (i, thm_node) => fn (x, seen) =>
+ if Intset.member seen i then (x, seen)
else
let
val name = thm_node_name thm_node;
val prop = thm_node_prop thm_node;
val body = Future.join (thm_node_body thm_node);
- val (x', seen') = app body (x, Inttab.update (i, ()) seen);
+ val (x', seen') = app body (x, Intset.insert i seen);
in (f {serial = i, name = name, prop = prop, body = body} x', seen') end);
- in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
+ in fn bodies => fn x => #1 (fold app bodies (x, Intset.empty)) end;
(* proof body *)
-val unions_oracles = Ord_List.unions oracle_ord;
-val unions_thms = Ord_List.unions thm_ord;
-
-fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof};
+fun no_proof_body proof = PBody {oracles = Oracles.empty, thms = PThms.empty, proof = proof};
val no_thm_body = thm_body (no_proof_body MinProof);
fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf)
@@ -375,7 +376,8 @@
(map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
and proof_body consts (PBody {oracles, thms, proof = prf}) =
triple (list (pair (pair string (properties o Position.properties_of))
- (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
+ (option (term consts)))) (list (thm consts)) (proof consts)
+ (Oracles.dest oracles, PThms.dest thms, prf)
and thm consts (a, thm_node) =
pair int (pair string (pair string (pair (term consts) (proof_body consts))))
(a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
@@ -441,7 +443,7 @@
val (a, b, c) =
triple (list (pair (pair string (Position.of_properties o properties))
(option (term consts)))) (list (thm consts)) (proof consts) x;
- in PBody {oracles = a, thms = b, proof = c} end
+ in PBody {oracles = Oracles.make a, thms = PThms.make b, proof = c} end
and thm consts x =
let
val (a, (b, (c, (d, e)))) =
@@ -1990,10 +1992,8 @@
val _ = consolidate_bodies (map #2 ps @ [body0]);
val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
val oracles =
- unions_oracles
- (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
- val thms =
- unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
+ fold (fn (_, PBody {oracles, ...}) => fn acc => Oracles.merge (acc, oracles)) ps oracles0;
+ val thms = fold (fn (_, PBody {thms, ...}) => fn acc => merge_thms (acc, thms)) ps thms0;
val proof = rew_proof thy proof0;
in PBody {oracles = oracles, thms = thms, proof = proof} end;
@@ -2142,9 +2142,9 @@
else
boxes
|> Inttab.update (i, thm_node_export thm_node)
- |> fold export_thm (thm_node_thms thm_node);
+ |> PThms.fold export_thm (thm_node_thms thm_node);
- fun export_body (PBody {thms, ...}) = fold export_thm thms;
+ fun export_body (PBody {thms, ...}) = PThms.fold export_thm thms;
val exports = Inttab.build (fold export_body bodies) |> Inttab.dest;
in List.app (Lazy.force o #2) exports end;
--- a/src/Pure/term_items.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/Pure/term_items.ML Thu Apr 13 15:36:30 2023 +1000
@@ -8,6 +8,7 @@
signature TERM_ITEMS =
sig
+ structure Key: KEY
type key
type 'a table
val empty: 'a table
@@ -38,32 +39,32 @@
functor Term_Items(Key: KEY): TERM_ITEMS =
struct
+(* keys *)
+
+structure Key = Key;
+type key = Key.key;
+
+
(* table with length *)
structure Table = Table(Key);
-type key = Table.key;
-datatype 'a table = Items of int * 'a Table.table;
+datatype 'a table = Table of 'a Table.table;
-fun size (Items (n, _)) = n;
-fun table (Items (_, tab)) = tab;
-
-val empty = Items (0, Table.empty);
+val empty = Table Table.empty;
fun build (f: 'a table -> 'a table) = f empty;
-fun is_empty items = size items = 0;
+fun is_empty (Table tab) = Table.is_empty tab;
-fun dest items = Table.dest (table items);
-fun keys items = Table.keys (table items);
-fun exists pred = Table.exists pred o table;
-fun forall pred = Table.forall pred o table;
-fun get_first get = Table.get_first get o table;
-fun lookup items = Table.lookup (table items);
-fun defined items = Table.defined (table items);
+fun size (Table tab) = Table.size tab;
+fun dest (Table tab) = Table.dest tab;
+fun keys (Table tab) = Table.keys tab;
+fun exists pred (Table tab) = Table.exists pred tab;
+fun forall pred (Table tab) = Table.forall pred tab;
+fun get_first get (Table tab) = Table.get_first get tab;
+fun lookup (Table tab) = Table.lookup tab;
+fun defined (Table tab) = Table.defined tab;
-fun add (key, x) (items as Items (n, tab)) =
- if Table.defined tab key then items
- else Items (n + 1, Table.update_new (key, x) tab);
-
+fun add entry (Table tab) = Table (Table.default entry tab);
fun make entries = build (fold add entries);
@@ -71,22 +72,21 @@
type set = int table;
-fun add_set x (items as Items (n, tab)) =
- if Table.defined tab x then items
- else Items (n + 1, Table.update_new (x, n) tab);
+fun add_set x (Table tab) =
+ Table (if Table.defined tab x then tab else Table.update_new (x, Table.size tab + 1) tab);
fun make_set xs = build (fold add_set xs);
fun subset (A: set, B: set) = forall (defined B o #1) A;
fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B);
-fun list_set_ord ord items = Table.dest (table items) |> sort (ord o apply2 #2) |> map #1
+fun list_set_ord ord (Table tab) = tab |> Table.dest |> sort (ord o apply2 #2) |> map #1;
val list_set = list_set_ord int_ord;
val list_set_rev = list_set_ord (rev_order o int_ord);
-fun map f (Items (n, tab)) = Items (n, Table.map f tab);
-fun fold f = Table.fold f o table;
-fun fold_rev f = Table.fold_rev f o table;
+fun map f (Table tab) = Table (Table.map f tab);
+fun fold f (Table tab) = Table.fold f tab;
+fun fold_rev f (Table tab) = Table.fold_rev f tab;
end;
--- a/src/Pure/term_sharing.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/Pure/term_sharing.ML Thu Apr 13 15:36:30 2023 +1000
@@ -25,8 +25,8 @@
val tycon = perhaps (Option.map #1 o Name_Space.lookup_key types);
val const = perhaps (try (#1 o Consts.the_const (Sign.consts_of thy)));
- val typs = Unsynchronized.ref (Typtab.empty: unit Typtab.table);
- val terms = Unsynchronized.ref (Syntax_Termtab.empty: unit Syntax_Termtab.table);
+ val typs = Unsynchronized.ref (Typtab.empty: Typtab.set);
+ val terms = Unsynchronized.ref (Syntax_Termtab.empty: Syntax_Termtab.set);
fun typ T =
(case Typtab.lookup_key (! typs) T of
@@ -38,7 +38,7 @@
Type (a, Ts) => Type (tycon a, map typ Ts)
| TFree (a, S) => TFree (a, map class S)
| TVar (a, S) => TVar (a, map class S));
- val _ = Unsynchronized.change typs (Typtab.update (T', ()));
+ val _ = Unsynchronized.change typs (Typtab.insert_set T');
in T' end);
fun term tm =
@@ -54,7 +54,7 @@
| Bound i => Bound i
| Abs (x, T, t) => Abs (x, typ T, term t)
| t $ u => term t $ term u);
- val _ = Unsynchronized.change terms (Syntax_Termtab.update (tm', ()));
+ val _ = Unsynchronized.change terms (Syntax_Termtab.insert_set tm');
in tm' end);
fun check eq f x =
--- a/src/Pure/thm.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/Pure/thm.ML Thu Apr 13 15:36:30 2023 +1000
@@ -107,7 +107,7 @@
val expose_proofs: theory -> thm list -> unit
val expose_proof: theory -> thm -> unit
val future: thm future -> cterm -> thm
- val thm_deps: thm -> Proofterm.thm Ord_List.T
+ val thm_deps: thm -> Proofterm.thms
val extra_shyps: thm -> Sortset.T
val strip_shyps: thm -> thm
val derivation_closed: thm -> bool
@@ -739,7 +739,7 @@
fun make_deriv promises oracles thms proof =
Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
-val empty_deriv = make_deriv empty_promises [] [] MinProof;
+val empty_deriv = make_deriv empty_promises Oracles.empty PThms.empty MinProof;
(* inference rules *)
@@ -752,8 +752,8 @@
(Deriv {promises = promises2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) =
let
val ps = merge_promises (promises1, promises2);
- val oracles = Proofterm.unions_oracles [oracles1, oracles2];
- val thms = Proofterm.unions_thms [thms1, thms2];
+ val oracles = Oracles.merge (oracles1, oracles2);
+ val thms = Proofterm.merge_thms (thms1, thms2);
val prf =
(case ! Proofterm.proofs of
2 => f prf1 prf2
@@ -766,7 +766,7 @@
fun deriv_rule0 make_prf =
if ! Proofterm.proofs <= 1 then empty_deriv
- else deriv_rule1 I (make_deriv empty_promises [] [] (make_prf ()));
+ else deriv_rule1 I (make_deriv empty_promises Oracles.empty PThms.empty (make_prf ()));
fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
make_deriv promises oracles thms (f proof);
@@ -832,7 +832,7 @@
val i = serial ();
val future = future_thm |> Future.map (future_result i cert sorts prop);
in
- Thm (make_deriv (make_promises [(i, future)]) [] [] MinProof,
+ Thm (make_deriv (make_promises [(i, future)]) Oracles.empty PThms.empty MinProof,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -974,7 +974,7 @@
local
fun union_digest (oracles1, thms1) (oracles2, thms2) =
- (Proofterm.unions_oracles [oracles1, oracles2], Proofterm.unions_thms [thms1, thms2]);
+ (Oracles.merge (oracles1, oracles2), Proofterm.merge_thms (thms1, thms2));
fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) =
(oracles, thms);
@@ -982,11 +982,12 @@
fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) =
Sorts.of_sort_derivation (Sign.classes_of thy)
{class_relation = fn _ => fn _ => fn (digest, c1) => fn c2 =>
- if c1 = c2 then ([], []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
+ if c1 = c2 then (Oracles.empty, PThms.empty)
+ else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
type_constructor = fn (a, _) => fn dom => fn c =>
let val arity_digest = thm_digest (the_arity thy (a, (map o map) #2 dom, c))
in (fold o fold) (union_digest o #1) dom arity_digest end,
- type_variable = fn T => map (pair ([], [])) (Type.sort_of_atyp T)}
+ type_variable = fn T => map (pair (Oracles.empty, PThms.empty)) (Type.sort_of_atyp T)}
(typ, sort);
in
@@ -1093,12 +1094,13 @@
(*dependencies of PThm node*)
fun thm_deps (thm as Thm (Deriv {promises, body = PBody {thms, ...}, ...}, _)) =
- if null_promises promises then
- (case (derivation_id thm, thms) of
- (SOME {serial = i, ...}, [(j, thm_node)]) =>
- if i = j then Proofterm.thm_node_thms thm_node else thms
- | _ => thms)
- else raise THM ("thm_deps: bad promises", 0, [thm]);
+ if not (null_promises promises) then raise THM ("thm_deps: bad promises", 0, [thm])
+ else if PThms.size thms = 1 then
+ (case (derivation_id thm, PThms.dest thms) of
+ (SOME {serial = i, ...}, [(j, thm_node)]) =>
+ if i = j then Proofterm.thm_node_thms thm_node else thms
+ | _ => thms)
+ else thms;
fun name_derivation name_pos =
strip_shyps #> (fn thm as Thm (der, args) =>
@@ -1114,7 +1116,7 @@
val (pthm, proof) =
Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
name_pos shyps (Termset.dest hyps) prop ps body;
- val der' = make_deriv empty_promises [] [pthm] proof;
+ val der' = make_deriv empty_promises Oracles.empty (PThms.make [pthm]) proof;
in Thm (der', args) end);
fun close_derivation pos =
@@ -1145,7 +1147,7 @@
| 0 => (((name, Position.none), NONE), MinProof)
| i => bad_proofs i);
in
- Thm (make_deriv empty_promises [oracle] [] prf,
+ Thm (make_deriv empty_promises (Oracles.make [oracle]) PThms.empty prf,
{cert = Context.join_certificate (Context.Certificate thy', cert2),
tags = [],
maxidx = maxidx,
@@ -1805,7 +1807,7 @@
val (pthm, proof) =
Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy)
shyps prop ps body;
- val der' = make_deriv empty_promises [] [pthm] proof;
+ val der' = make_deriv empty_promises Oracles.empty (PThms.make [pthm]) proof;
val prop' = Proofterm.thm_node_prop (#2 pthm);
in
Thm (der',
--- a/src/Pure/thm_deps.ML Thu Apr 13 15:36:07 2023 +1000
+++ b/src/Pure/thm_deps.ML Thu Apr 13 15:36:30 2023 +1000
@@ -7,7 +7,7 @@
signature THM_DEPS =
sig
- val all_oracles: thm list -> Proofterm.oracle list
+ val all_oracles: thm list -> Oracles.T
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
@@ -23,17 +23,17 @@
fun all_oracles thms =
let
fun collect (PBody {oracles, thms, ...}) =
- (if null oracles then I else apfst (cons oracles)) #>
- (tap Proofterm.join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) =>
- if Inttab.defined seen i then (res, seen)
+ (if Oracles.is_empty oracles then I else apfst (cons oracles)) #>
+ (tap Proofterm.join_thms thms |> PThms.fold (fn (i, thm_node) => fn (res, seen) =>
+ if Intset.member seen i then (res, seen)
else
let val body = Future.join (Proofterm.thm_node_body thm_node)
- in collect body (res, Inttab.update (i, ()) seen) end));
+ in collect body (res, Intset.insert i seen) end));
val bodies = map Thm.proof_body_of thms;
- in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end;
+ in fold collect bodies ([], Intset.empty) |> #1 |> Oracles.merges end;
fun has_skip_proof thms =
- all_oracles thms |> exists (fn ((name, _), _) => name = \<^oracle_name>\<open>skip_proof\<close>);
+ all_oracles thms |> Oracles.exists (fn ((name, _), _) => name = \<^oracle_name>\<open>skip_proof\<close>);
fun pretty_thm_oracles ctxt thms =
let
@@ -44,7 +44,7 @@
prt_ora ora @ [Pretty.str ":", Pretty.brk 1, Syntax.pretty_term_global thy prop];
val oracles =
(case try all_oracles thms of
- SOME oracles => oracles
+ SOME oracles => Oracles.dest oracles
| NONE => error "Malformed proofs")
in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) oracles) end;
@@ -63,11 +63,11 @@
Inttab.update (i, SOME (thm_id, thm_name)) res
| NONE =>
Inttab.update (i, NONE) res
- |> fold deps (Proofterm.thm_node_thms thm_node))
+ |> PThms.fold deps (Proofterm.thm_node_thms thm_node))
end;
in
fn thms =>
- (Inttab.build (fold (fold deps o Thm.thm_deps o Thm.transfer thy) thms), [])
+ (Inttab.build (fold (PThms.fold deps o Thm.thm_deps o Thm.transfer thy) thms), [])
|-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I)
end;
@@ -112,33 +112,26 @@
val used =
Proofterm.fold_body_thms
- (fn {name = a, ...} => a <> "" ? Symtab.update (a, ()))
+ (fn {name = a, ...} => a <> "" ? Symset.insert a)
(map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
- Symtab.empty;
+ Symset.empty;
- fun is_unused a = not (Symtab.defined used a);
+ fun is_unused a = not (Symset.member used a);
(*groups containing at least one used theorem*)
val used_groups =
- Inttab.build (new_thms |> fold (fn (a, (_, _, group)) =>
- if is_unused a then I
- else
- (case group of
- NONE => I
- | SOME grp => Inttab.update (grp, ()))));
+ Intset.build (new_thms |> fold (fn (a, (_, _, group)) =>
+ if is_unused a orelse group = 0 then I else Intset.insert group));
val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
if not concealed andalso
(* FIXME replace by robust treatment of thm groups *)
Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a
then
- (case group of
- NONE => ((a, th) :: thms, seen_groups)
- | SOME grp =>
- if Inttab.defined used_groups grp orelse
- Inttab.defined seen_groups grp then q
- else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
- else q) new_thms ([], Inttab.empty);
+ (if group = 0 then ((a, th) :: thms, seen_groups)
+ else if Intset.member used_groups group orelse Intset.member seen_groups group then q
+ else ((a, th) :: thms, Intset.insert group seen_groups))
+ else q) new_thms ([], Intset.empty);
in rev thms' end;
end;