# HG changeset patch # User wenzelm # Date 1681811892 -7200 # Node ID 3bd1aa2f3517a898009f545d81b99752fa4b4598 # Parent 6f7a577a1406ed3d711dae25b5fd7369af18fe9a backout 61f652dd955a; diff -r 6f7a577a1406 -r 3bd1aa2f3517 src/HOL/Tools/Mirabelle/mirabelle.ML --- 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 diff -r 6f7a577a1406 -r 3bd1aa2f3517 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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 diff -r 6f7a577a1406 -r 3bd1aa2f3517 src/Pure/Proof/extraction.ML --- 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; diff -r 6f7a577a1406 -r 3bd1aa2f3517 src/Pure/proofterm.ML --- 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; diff -r 6f7a577a1406 -r 3bd1aa2f3517 src/Pure/thm.ML --- 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', diff -r 6f7a577a1406 -r 3bd1aa2f3517 src/Pure/thm_deps.ML --- 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;