# HG changeset patch # User wenzelm # Date 1681833867 -7200 # Node ID 864c7c684651be9f3e5623b226a4a8db4218d34f # Parent c404695aaf958596f4654a21da14cd86390eb0fa backout b6aa5eac0a1a; diff -r c404695aaf95 -r 864c7c684651 src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Apr 18 17:50:44 2023 +0200 +++ b/src/Pure/thm.ML Tue Apr 18 18:04:27 2023 +0200 @@ -438,17 +438,9 @@ tpairs: (term * term) list, (*flex-flex pairs*) prop: term} (*conclusion*) and deriv = Deriv of - {promises: thm future Inttab'.table, + {promises: (serial * thm future) Ord_List.T, body: Proofterm.proof_body}; -type promises = thm future Inttab'.table; -val null_promises : promises -> bool = Inttab'.is_empty; -val empty_promises : promises = Inttab'.empty; -val merge_promises : promises * promises -> promises = Inttab'.merge (K true); -val make_promises : (serial * thm future) list -> promises = Inttab'.make; -val dest_promises : promises -> (serial * thm future) list = Inttab'.dest; -fun forall_promises f : promises -> bool = Inttab'.forall (f o fst); - type conv = cterm -> thm; (*errors involving theorems*) @@ -770,19 +762,21 @@ 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 [] [] [] MinProof; (* inference rules *) +val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i); + fun bad_proofs i = error ("Illegal level of detail for proof objects: " ^ string_of_int i); fun deriv_rule2 f - (Deriv {promises = promises1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}}) - (Deriv {promises = promises2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) = + (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}}) + (Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) = let - val ps = merge_promises (promises1, promises2); + val ps = Ord_List.union promise_ord ps1 ps2; val oracles = Proofterm.unions_oracles [oracles1, oracles2]; val thms = Proofterm.unions_thms [thms1, thms2]; val prf = @@ -797,7 +791,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 [] [] [] (make_prf ())); fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) = make_deriv promises oracles thms (f proof); @@ -805,18 +799,15 @@ (* fulfilled proofs *) -fun merge_promises_of (Thm (Deriv {promises, ...}, _)) ps = merge_promises (ps, promises); +fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises; fun join_promises [] = () | join_promises promises = join_promises_of (Future.joins (map snd promises)) -and join_promises_of thms = - join_promises (dest_promises (fold merge_promises_of thms empty_promises)); +and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms)); fun fulfill_body (th as Thm (Deriv {promises, body}, _)) = - let - val pending = dest_promises promises; - val fulfilled = map #1 pending ~~ map fulfill_body (Future.joins (map #2 pending)); - in Proofterm.fulfill_norm_proof (theory_of_thm th) fulfilled body end; + let val fulfilled_promises = map #1 promises ~~ map fulfill_body (Future.joins (map #2 promises)) + in Proofterm.fulfill_norm_proof (theory_of_thm th) fulfilled_promises body end; fun proof_bodies_of thms = (join_promises_of thms; map fulfill_body thms); val proof_body_of = singleton proof_bodies_of; @@ -848,8 +839,8 @@ val _ = null tpairs orelse err "bad flex-flex constraints"; val _ = null hyps orelse err "bad hyps"; val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps"; - val _ = forall_promises (fn j => i <> j) promises orelse err "bad dependencies"; - val _ = join_promises (dest_promises promises); + val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies"; + val _ = join_promises promises; in thm end; fun future future_thm ct = @@ -863,7 +854,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 [(i, future)] [] [] MinProof, {cert = cert, tags = [], maxidx = maxidx, @@ -1122,13 +1113,12 @@ Proofterm.get_id shyps hyps prop (proof_of thm); (*dependencies of PThm node*) -fun thm_deps (thm as Thm (Deriv {promises, body = PBody {thms, ...}, ...}, _)) = - if null_promises promises then +fun thm_deps (thm as Thm (Deriv {promises = [], body = PBody {thms, ...}, ...}, _)) = (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]); + | thm_deps thm = raise THM ("thm_deps: bad promises", 0, [thm]); fun name_derivation name_pos = strip_shyps #> (fn thm as Thm (der, args) => @@ -1140,11 +1130,11 @@ val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]); - val ps = map (apsnd (Future.map fulfill_body)) (dest_promises promises); + val ps = map (apsnd (Future.map fulfill_body)) promises; 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 [] [pthm] proof; + val der' = make_deriv [] [] [pthm] proof; in Thm (der', args) end); fun close_derivation pos = @@ -1175,7 +1165,7 @@ | 0 => (((name, Position.none), NONE), MinProof) | i => bad_proofs i); in - Thm (make_deriv empty_promises [oracle] [] prf, + Thm (make_deriv [] [oracle] [] prf, {cert = Context.join_certificate (Context.Certificate thy', cert2), tags = [], maxidx = maxidx, @@ -1831,11 +1821,11 @@ val tfrees = build_rev (Term.add_tfree_names prop); val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); - val ps = map (apsnd (Future.map fulfill_body)) (dest_promises promises); + val ps = map (apsnd (Future.map fulfill_body)) promises; 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 [] [] [pthm] proof; val prop' = Proofterm.thm_node_prop (#2 pthm); in Thm (der',