# HG changeset patch # User wenzelm # Date 1681812281 -7200 # Node ID 686a7d71ed7b8dbf7090bf45b036320a62908b6c # Parent 3bd1aa2f3517a898009f545d81b99752fa4b4598 backout e3fe192fa4a8; diff -r 3bd1aa2f3517 -r 686a7d71ed7b src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Tue Apr 18 11:58:12 2023 +0200 +++ b/src/Doc/Implementation/Logic.thy Tue Apr 18 12:04:41 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 -> Oracles.T"} \\ + @{define_ML Thm_Deps.all_oracles: "thm list -> Proofterm.oracle list"} \\ \end{mldecls} \<^descr> \<^ML>\Logic.all\~\a B\ produces a Pure quantification \\a. B\, where diff -r 3bd1aa2f3517 -r 686a7d71ed7b src/HOL/Examples/Iff_Oracle.thy --- a/src/HOL/Examples/Iff_Oracle.thy Tue Apr 18 11:58:12 2023 +0200 +++ b/src/HOL/Examples/Iff_Oracle.thy Tue Apr 18 12:04:41 2023 +0200 @@ -36,8 +36,7 @@ ML \iff_oracle (\<^theory>, 10)\ ML \ - \<^assert> (map (#1 o #1) (Oracles.dest (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)])) = - [\<^oracle_name>\iff_oracle\]); + \<^assert> (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\iff_oracle\]); \ text \These oracle calls had better fail.\ diff -r 3bd1aa2f3517 -r 686a7d71ed7b src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Apr 18 11:58:12 2023 +0200 +++ b/src/Pure/Proof/extraction.ML Tue Apr 18 12:04:41 2023 +0200 @@ -182,7 +182,7 @@ | _ => I); val body = PBody - {oracles = Oracles.make oracles, + {oracles = Ord_List.make Proofterm.oracle_ord oracles, thms = Ord_List.make Proofterm.thm_ord thms, proof = prf}; in Proofterm.thm_body body end; diff -r 3bd1aa2f3517 -r 686a7d71ed7b src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Apr 18 11:58:12 2023 +0200 +++ b/src/Pure/proofterm.ML Tue Apr 18 12:04:41 2023 +0200 @@ -6,11 +6,6 @@ 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 = @@ -31,9 +26,10 @@ | Oracle of string * term * typ list option | PThm of thm_header * thm_body and proof_body = PBody of - {oracles: Oracles.T, + {oracles: ((string * Position.T) * term option) Ord_List.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 @@ -55,7 +51,9 @@ 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 @@ -219,7 +217,7 @@ | Oracle of string * term * typ list option | PThm of thm_header * thm_body and proof_body = PBody of - {oracles: Oracles.T, + {oracles: ((string * Position.T) * term option) Ord_List.T, thms: (serial * thm_node) Ord_List.T, proof: proof} and thm_body = @@ -228,6 +226,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; val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i); @@ -314,9 +316,10 @@ (* 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 = Oracles.empty, thms = [], proof = proof}; +fun no_proof_body proof = PBody {oracles = [], 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) @@ -372,7 +375,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, thms, prf) + (option (term consts)))) (list (thm consts)) (proof consts) (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, @@ -438,7 +441,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 = b, proof = c} end + in PBody {oracles = a, thms = b, proof = c} end and thm consts x = let val (a, (b, (c, (d, e)))) = @@ -1987,9 +1990,8 @@ val _ = consolidate_bodies (map #2 ps @ [body0]); val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0; val oracles = - Oracles.merges - (fold (fn (_, PBody {oracles, ...}) => not (Oracles.is_empty oracles) ? cons oracles) - ps [oracles0]); + 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]); val proof = rew_proof thy proof0; diff -r 3bd1aa2f3517 -r 686a7d71ed7b src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Apr 18 11:58:12 2023 +0200 +++ b/src/Pure/thm.ML Tue Apr 18 12:04:41 2023 +0200 @@ -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 [] MinProof; +val empty_deriv = make_deriv empty_promises [] [] MinProof; (* inference rules *) @@ -755,7 +755,7 @@ (Deriv {promises = promises2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) = let val ps = merge_promises (promises1, promises2); - val oracles = Oracles.merge (oracles1, oracles2); + val oracles = Proofterm.unions_oracles [oracles1, oracles2]; val thms = Proofterm.unions_thms [thms1, thms2]; val prf = (case ! Proofterm.proofs of @@ -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 [] (make_prf ())); + else deriv_rule1 I (make_deriv empty_promises [] [] (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 [] MinProof, + Thm (make_deriv (make_promises [(i, future)]) [] [] MinProof, {cert = cert, tags = [], maxidx = maxidx, @@ -976,7 +976,7 @@ local fun union_digest (oracles1, thms1) (oracles2, thms2) = - (Oracles.merge (oracles1, oracles2), Proofterm.unions_thms [thms1, thms2]); + (Proofterm.unions_oracles [oracles1, oracles2], Proofterm.unions_thms [thms1, thms2]); fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) = (oracles, thms); @@ -984,11 +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, []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))), + if c1 = c2 then ([], []) 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, [])) (Type.sort_of_atyp T)} + type_variable = fn T => map (pair ([], [])) (Type.sort_of_atyp T)} (typ, sort); in @@ -1116,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 [pthm] proof; + val der' = make_deriv empty_promises [] [pthm] proof; in Thm (der', args) end); fun close_derivation pos = @@ -1147,7 +1147,7 @@ | 0 => (((name, Position.none), NONE), MinProof) | i => bad_proofs i); in - Thm (make_deriv empty_promises (Oracles.make [oracle]) [] prf, + Thm (make_deriv empty_promises [oracle] [] prf, {cert = Context.join_certificate (Context.Certificate thy', cert2), tags = [], maxidx = maxidx, @@ -1807,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 [pthm] proof; + val der' = make_deriv empty_promises [] [pthm] proof; val prop' = Proofterm.thm_node_prop (#2 pthm); in Thm (der', diff -r 3bd1aa2f3517 -r 686a7d71ed7b src/Pure/thm_deps.ML --- a/src/Pure/thm_deps.ML Tue Apr 18 11:58:12 2023 +0200 +++ b/src/Pure/thm_deps.ML Tue Apr 18 12:04:41 2023 +0200 @@ -7,7 +7,7 @@ signature THM_DEPS = sig - val all_oracles: thm list -> Oracles.T + val all_oracles: thm list -> Proofterm.oracle list 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 Oracles.is_empty oracles then I else apfst (cons oracles)) #> + (if null 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 |> Oracles.merges end; + in fold collect bodies ([], Intset.empty) |> #1 |> Proofterm.unions_oracles end; fun has_skip_proof thms = - all_oracles thms |> Oracles.exists (fn ((name, _), _) => name = \<^oracle_name>\skip_proof\); + all_oracles thms |> 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.dest oracles + SOME oracles => oracles | NONE => error "Malformed proofs") in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) oracles) end;