--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Tue Apr 18 11:45:04 2023 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Tue Apr 18 11:58:12 2023 +0200
@@ -302,7 +302,7 @@
fun fold_body_thms f =
let
- fun app n (PBody {thms, ...}) = thms |> PThms.fold (fn (i, thm_node) =>
+ fun app n (PBody {thms, ...}) = thms |> 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 Tue Apr 18 11:45:04 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Apr 18 11:58:12 2023 +0200
@@ -104,7 +104,7 @@
else (num_thms + 1, name' :: names)
| NONE => accum)
end
- and app_body map_name (PBody {thms, ...}) = PThms.fold (app_thm map_name) thms
+ and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms
in
snd (app_body map_plain_name body (0, []))
end
--- a/src/Pure/Proof/extraction.ML Tue Apr 18 11:45:04 2023 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Apr 18 11:58:12 2023 +0200
@@ -180,7 +180,11 @@
(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 = Oracles.make oracles, thms = PThms.make thms, proof = prf};
+ val body =
+ PBody
+ {oracles = Oracles.make oracles,
+ thms = Ord_List.make Proofterm.thm_ord thms,
+ proof = prf};
in Proofterm.thm_body body end;
--- a/src/Pure/proofterm.ML Tue Apr 18 11:45:04 2023 +0200
+++ b/src/Pure/proofterm.ML Tue Apr 18 11:58:12 2023 +0200
@@ -11,11 +11,6 @@
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 =
@@ -37,12 +32,9 @@
| PThm of thm_header * thm_body
and proof_body = PBody of
{oracles: Oracles.T,
- thms: thm_node PThms.table,
+ thms: (serial * thm_node) Ord_List.T,
proof: proof}
type thm = serial * thm_node
- type thms = thm_node PThms.table
- val union_thms: thms * thms -> thms
- val unions_thms: thms list -> thms
exception MIN_PROOF of unit
val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
@@ -56,13 +48,15 @@
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 -> thms
- val join_thms: thms -> proof_body list
+ val thm_node_thms: thm_node -> thm list
+ val join_thms: thm list -> 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 thm_ord: thm ord
+ 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
@@ -226,7 +220,7 @@
| PThm of thm_header * thm_body
and proof_body = PBody of
{oracles: Oracles.T,
- thms: thm_node PThms.table,
+ thms: (serial * thm_node) Ord_List.T,
proof: proof}
and thm_body =
Thm_Body of {open_proof: proof -> proof, body: proof_body future}
@@ -235,10 +229,8 @@
body: proof_body future, export: unit lazy, consolidate: unit lazy};
type thm = serial * thm_node;
+val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
-type thms = thm_node PThms.table;
-val union_thms: thms * thms -> thms = PThms.merge (K true);
-val unions_thms: thms list -> thms = PThms.merges (K true);
exception MIN_PROOF of unit;
@@ -264,11 +256,11 @@
val thm_node_export = #export o rep_thm_node;
val thm_node_consolidate = #consolidate o rep_thm_node;
-fun join_thms (thms: thms) =
- Future.joins (PThms.fold_rev (cons o thm_node_body o #2) thms []);
+fun join_thms (thms: thm list) =
+ Future.joins (map (thm_node_body o #2) thms);
val consolidate_bodies =
- maps (fn PBody {thms, ...} => PThms.fold_rev (cons o thm_node_consolidate o #2) thms [])
+ maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
#> Lazy.consolidate #> map Lazy.force #> ignore;
fun make_thm_node theory_name name prop body export =
@@ -308,7 +300,7 @@
fun fold_body_thms f =
let
fun app (PBody {thms, ...}) =
- tap join_thms thms |> PThms.fold (fn (i, thm_node) => fn (x, seen) =>
+ tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
if Intset.member seen i then (x, seen)
else
let
@@ -322,7 +314,9 @@
(* proof body *)
-fun no_proof_body proof = PBody {oracles = Oracles.empty, thms = PThms.empty, proof = proof};
+val unions_thms = Ord_List.unions thm_ord;
+
+fun no_proof_body proof = PBody {oracles = Oracles.empty, thms = [], 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)
@@ -378,8 +372,7 @@
(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.dest oracles, PThms.dest thms, prf)
+ (option (term consts)))) (list (thm consts)) (proof consts) (Oracles.dest oracles, 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,
@@ -445,7 +438,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 = Oracles.make a, thms = PThms.make b, proof = c} end
+ in PBody {oracles = Oracles.make a, thms = b, proof = c} end
and thm consts x =
let
val (a, (b, (c, (d, e)))) =
@@ -1998,9 +1991,7 @@
(fold (fn (_, PBody {oracles, ...}) => not (Oracles.is_empty oracles) ? cons oracles)
ps [oracles0]);
val thms =
- unions_thms
- (fold (fn (_, PBody {thms, ...}) => not (PThms.is_empty thms) ? cons thms)
- ps [thms0]);
+ unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
val proof = rew_proof thy proof0;
in PBody {oracles = oracles, thms = thms, proof = proof} end;
@@ -2149,9 +2140,9 @@
else
boxes
|> Inttab.update (i, thm_node_export thm_node)
- |> PThms.fold export_thm (thm_node_thms thm_node);
+ |> fold export_thm (thm_node_thms thm_node);
- fun export_body (PBody {thms, ...}) = PThms.fold export_thm thms;
+ fun export_body (PBody {thms, ...}) = 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/thm.ML Tue Apr 18 11:45:04 2023 +0200
+++ b/src/Pure/thm.ML Tue Apr 18 11:58:12 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.thms
+ val thm_deps: thm -> Proofterm.thm Ord_List.T
val extra_shyps: thm -> Sortset.T
val strip_shyps: thm -> thm
val derivation_closed: thm -> bool
@@ -742,7 +742,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 Oracles.empty PThms.empty MinProof;
+val empty_deriv = make_deriv empty_promises Oracles.empty [] MinProof;
(* inference rules *)
@@ -756,7 +756,7 @@
let
val ps = merge_promises (promises1, promises2);
val oracles = Oracles.merge (oracles1, oracles2);
- val thms = Proofterm.union_thms (thms1, thms2);
+ val thms = Proofterm.unions_thms [thms1, thms2];
val prf =
(case ! Proofterm.proofs of
2 => f prf1 prf2
@@ -769,7 +769,7 @@
fun deriv_rule0 make_prf =
if ! Proofterm.proofs <= 1 then empty_deriv
- else deriv_rule1 I (make_deriv empty_promises Oracles.empty PThms.empty (make_prf ()));
+ else deriv_rule1 I (make_deriv empty_promises Oracles.empty [] (make_prf ()));
fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
make_deriv promises oracles thms (f proof);
@@ -835,7 +835,7 @@
val i = serial ();
val future = future_thm |> Future.map (future_result i cert sorts prop);
in
- Thm (make_deriv (make_promises [(i, future)]) Oracles.empty PThms.empty MinProof,
+ Thm (make_deriv (make_promises [(i, future)]) Oracles.empty [] MinProof,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -976,7 +976,7 @@
local
fun union_digest (oracles1, thms1) (oracles2, thms2) =
- (Oracles.merge (oracles1, oracles2), Proofterm.union_thms (thms1, thms2));
+ (Oracles.merge (oracles1, oracles2), Proofterm.unions_thms [thms1, thms2]);
fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) =
(oracles, thms);
@@ -984,12 +984,11 @@
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 (Oracles.empty, PThms.empty)
- else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
+ if c1 = c2 then (Oracles.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 (Oracles.empty, PThms.empty)) (Type.sort_of_atyp T)}
+ type_variable = fn T => map (pair (Oracles.empty, [])) (Type.sort_of_atyp T)}
(typ, sort);
in
@@ -1096,13 +1095,12 @@
(*dependencies of PThm node*)
fun thm_deps (thm as Thm (Deriv {promises, body = PBody {thms, ...}, ...}, _)) =
- 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;
+ 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]);
fun name_derivation name_pos =
strip_shyps #> (fn thm as Thm (der, args) =>
@@ -1118,7 +1116,7 @@
val (pthm, proof) =
Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
name_pos shyps hyps prop ps body;
- val der' = make_deriv empty_promises Oracles.empty (PThms.make [pthm]) proof;
+ val der' = make_deriv empty_promises Oracles.empty [pthm] proof;
in Thm (der', args) end);
fun close_derivation pos =
@@ -1149,7 +1147,7 @@
| 0 => (((name, Position.none), NONE), MinProof)
| i => bad_proofs i);
in
- Thm (make_deriv empty_promises (Oracles.make [oracle]) PThms.empty prf,
+ Thm (make_deriv empty_promises (Oracles.make [oracle]) [] prf,
{cert = Context.join_certificate (Context.Certificate thy', cert2),
tags = [],
maxidx = maxidx,
@@ -1809,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 Oracles.empty (PThms.make [pthm]) proof;
+ val der' = make_deriv empty_promises Oracles.empty [pthm] proof;
val prop' = Proofterm.thm_node_prop (#2 pthm);
in
Thm (der',
--- a/src/Pure/thm_deps.ML Tue Apr 18 11:45:04 2023 +0200
+++ b/src/Pure/thm_deps.ML Tue Apr 18 11:58:12 2023 +0200
@@ -24,7 +24,7 @@
let
fun collect (PBody {oracles, thms, ...}) =
(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) =>
+ (tap Proofterm.join_thms thms |> 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)
@@ -63,11 +63,11 @@
Inttab.update (i, SOME (thm_id, thm_name)) res
| NONE =>
Inttab.update (i, NONE) res
- |> PThms.fold deps (Proofterm.thm_node_thms thm_node))
+ |> fold deps (Proofterm.thm_node_thms thm_node))
end;
in
fn thms =>
- (Inttab.build (fold (PThms.fold deps o Thm.thm_deps o Thm.transfer thy) thms), [])
+ (Inttab.build (fold (fold deps o Thm.thm_deps o Thm.transfer thy) thms), [])
|-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I)
end;