# HG changeset patch # User wenzelm # Date 1681283916 -7200 # Node ID 69ee23f83884e5bff9119cb2cce5c15957282af0 # Parent fb3d81bd9803b04e6bde98c839b52ef67d69c293# Parent 6fae9f5157b5a05e6f85de591a2b08b508a370cf merged diff -r fb3d81bd9803 -r 69ee23f83884 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Tue Apr 11 11:59:06 2023 +0000 +++ b/src/Doc/Implementation/Logic.thy Wed Apr 12 09:18:36 2023 +0200 @@ -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>\Logic.all\~\a B\ produces a Pure quantification \\a. B\, where diff -r fb3d81bd9803 -r 69ee23f83884 src/HOL/Examples/Iff_Oracle.thy --- a/src/HOL/Examples/Iff_Oracle.thy Tue Apr 11 11:59:06 2023 +0000 +++ b/src/HOL/Examples/Iff_Oracle.thy Wed Apr 12 09:18:36 2023 +0200 @@ -36,7 +36,8 @@ ML \iff_oracle (\<^theory>, 10)\ ML \ - \<^assert> (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\iff_oracle\]); + \<^assert> (map (#1 o #1) (Oracles.dest (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)])) = + [\<^oracle_name>\iff_oracle\]); \ text \These oracle calls had better fail.\ diff -r fb3d81bd9803 -r 69ee23f83884 src/HOL/Tools/Mirabelle/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/mirabelle.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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 diff -r fb3d81bd9803 -r 69ee23f83884 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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 diff -r fb3d81bd9803 -r 69ee23f83884 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/Pure/General/name_space.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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; diff -r fb3d81bd9803 -r 69ee23f83884 src/Pure/General/set.ML --- a/src/Pure/General/set.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/Pure/General/set.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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)) diff -r fb3d81bd9803 -r 69ee23f83884 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/Pure/General/table.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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 *) diff -r fb3d81bd9803 -r 69ee23f83884 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/Pure/Isar/locale.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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 diff -r fb3d81bd9803 -r 69ee23f83884 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/Pure/Proof/extraction.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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; diff -r fb3d81bd9803 -r 69ee23f83884 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/Pure/Proof/proof_syntax.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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 diff -r fb3d81bd9803 -r 69ee23f83884 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/Pure/Syntax/parser.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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; diff -r fb3d81bd9803 -r 69ee23f83884 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/Pure/proofterm.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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; diff -r fb3d81bd9803 -r 69ee23f83884 src/Pure/term_items.ML --- a/src/Pure/term_items.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/Pure/term_items.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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; diff -r fb3d81bd9803 -r 69ee23f83884 src/Pure/term_sharing.ML --- a/src/Pure/term_sharing.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/Pure/term_sharing.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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 = diff -r fb3d81bd9803 -r 69ee23f83884 src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/Pure/thm.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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', diff -r fb3d81bd9803 -r 69ee23f83884 src/Pure/thm_deps.ML --- a/src/Pure/thm_deps.ML Tue Apr 11 11:59:06 2023 +0000 +++ b/src/Pure/thm_deps.ML Wed Apr 12 09:18:36 2023 +0200 @@ -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>\skip_proof\); + all_oracles thms |> Oracles.exists (fn ((name, _), _) => name = \<^oracle_name>\skip_proof\); 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;