# HG changeset patch # User wenzelm # Date 1681218182 -7200 # Node ID e3fe192fa4a80fdcc376f7147c75e53f11c2fca2 # Parent e60fe51f6f59a9690559649c963e0c6c357714b4 performance tuning: replace Ord_List by Set(); diff -r e60fe51f6f59 -r e3fe192fa4a8 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Tue Apr 11 13:23:46 2023 +0200 +++ b/src/Doc/Implementation/Logic.thy Tue Apr 11 15:03:02 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 e60fe51f6f59 -r e3fe192fa4a8 src/HOL/Examples/Iff_Oracle.thy --- a/src/HOL/Examples/Iff_Oracle.thy Tue Apr 11 13:23:46 2023 +0200 +++ b/src/HOL/Examples/Iff_Oracle.thy Tue Apr 11 15:03:02 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 e60fe51f6f59 -r e3fe192fa4a8 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Apr 11 13:23:46 2023 +0200 +++ b/src/Pure/Proof/extraction.ML Tue Apr 11 15:03:02 2023 +0200 @@ -182,7 +182,7 @@ | _ => I); val body = PBody - {oracles = Ord_List.make Proofterm.oracle_ord oracles, + {oracles = Oracles.make oracles, thms = Ord_List.make Proofterm.thm_ord thms, proof = prf}; in Proofterm.thm_body body end; diff -r e60fe51f6f59 -r e3fe192fa4a8 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Apr 11 13:23:46 2023 +0200 +++ b/src/Pure/proofterm.ML Tue Apr 11 15:03:02 2023 +0200 @@ -6,6 +6,11 @@ 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) +); + signature PROOFTERM = sig type thm_header = @@ -26,10 +31,9 @@ | 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, + {oracles: Oracles.T, thms: (serial * thm_node) Ord_List.T, proof: proof} - type oracle = (string * Position.T) * term option type thm = serial * thm_node exception MIN_PROOF of unit val proof_of: proof_body -> proof @@ -51,9 +55,7 @@ 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 @@ -217,7 +219,7 @@ | 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, + {oracles: Oracles.T, thms: (serial * thm_node) Ord_List.T, proof: proof} and thm_body = @@ -226,10 +228,6 @@ 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; val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i); @@ -316,10 +314,9 @@ (* 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 = [], 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 +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, 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, @@ -441,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 = a, thms = 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)))) = @@ -1990,8 +1987,9 @@ 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]); + Oracles.merges + (fold (fn (_, PBody {oracles, ...}) => not (Oracles.is_empty oracles) ? cons oracles) + ps [oracles0]); val thms = unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]); val proof = rew_proof thy proof0; diff -r e60fe51f6f59 -r e3fe192fa4a8 src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Apr 11 13:23:46 2023 +0200 +++ b/src/Pure/thm.ML Tue Apr 11 15:03:02 2023 +0200 @@ -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 [] MinProof; (* inference rules *) @@ -752,7 +752,7 @@ (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 oracles = Oracles.merge (oracles1, oracles2); val thms = Proofterm.unions_thms [thms1, thms2]; val prf = (case ! Proofterm.proofs of @@ -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 [] (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 [] 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.unions_thms [thms1, thms2]); fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) = (oracles, thms); @@ -982,11 +982,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 ([], []) 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 ([], [])) (Type.sort_of_atyp T)} + type_variable = fn T => map (pair (Oracles.empty, [])) (Type.sort_of_atyp T)} (typ, sort); in @@ -1114,7 +1114,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 [pthm] proof; in Thm (der', args) end); fun close_derivation pos = @@ -1145,7 +1145,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]) [] prf, {cert = Context.join_certificate (Context.Certificate thy', cert2), tags = [], maxidx = maxidx, @@ -1805,7 +1805,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 [pthm] proof; val prop' = Proofterm.thm_node_prop (#2 pthm); in Thm (der', diff -r e60fe51f6f59 -r e3fe192fa4a8 src/Pure/thm_deps.ML --- a/src/Pure/thm_deps.ML Tue Apr 11 13:23:46 2023 +0200 +++ b/src/Pure/thm_deps.ML Tue Apr 11 15:03:02 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)) #> + (if Oracles.is_empty oracles then I else apfst (cons oracles)) #> (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) in collect body (res, Intset.insert i seen) end)); val bodies = map Thm.proof_body_of thms; - in fold collect bodies ([], Intset.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;