# HG changeset patch # User wenzelm # Date 1702148713 -3600 # Node ID f9d972b464c11b9dbf7143688557344cf7b9899b # Parent 8b371e684acf38363a90bb30f90520383cf73b29 clarified signature: fewer tuples; diff -r 8b371e684acf -r f9d972b464c1 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Sat Dec 09 17:31:10 2023 +0100 +++ b/src/Pure/Proof/extraction.ML Sat Dec 09 20:05:13 2023 +0100 @@ -185,7 +185,8 @@ {oracles = Ord_List.make Proofterm.oracle_ord oracles, thms = Ord_List.make Proofterm.thm_ord thms, zboxes = Proofterm.empty_zboxes, - proof = (prf, ZDummy)}; + zproof = ZDummy, + proof = prf}; in Proofterm.thm_body body end; diff -r 8b371e684acf -r f9d972b464c1 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Sat Dec 09 17:31:10 2023 +0100 +++ b/src/Pure/proofterm.ML Sat Dec 09 20:05:13 2023 +0100 @@ -30,16 +30,15 @@ {oracles: ((string * Position.T) * term option) Ord_List.T, thms: (serial * thm_node) Ord_List.T, zboxes: zboxes, - proof: proof * zproof} - type proofs = proof * zproof + zproof: zproof, + proof: proof} type oracle = (string * Position.T) * term option type thm = serial * thm_node exception MIN_PROOF of unit - val proofs_of: proof_body -> proofs + val zproof_of: proof_body -> zproof val proof_of: proof_body -> proof - val zproof_of: proof_body -> zproof val join_proof: proof_body future -> proof - val map_proofs_of: (proofs -> proofs) -> proof_body -> proof_body + val map_proof_of: (proof -> proof) -> proof_body -> proof_body val thm_header: serial -> Position.T list -> string -> string -> term -> typ list option -> thm_header val thm_body: proof_body -> thm_body @@ -64,8 +63,7 @@ val unions_thms: thm Ord_List.T list -> thm Ord_List.T val empty_zboxes: zboxes val union_zboxes: zboxes -> zboxes -> zboxes - val no_proof: proofs - val no_proof_body: proofs -> proof_body + val no_proof_body: zproof -> proof -> proof_body val no_thm_names: proof -> proof val no_thm_proofs: proof -> proof val no_body_proofs: proof -> proof @@ -237,15 +235,14 @@ {oracles: ((string * Position.T) * term option) Ord_List.T, thms: (serial * thm_node) Ord_List.T, zboxes: zboxes, - proof: proof * zproof} + zproof: zproof, + proof: proof} and thm_body = Thm_Body of {open_proof: proof -> proof, body: proof_body future} and thm_node = Thm_Node of {theory_name: string, name: string, prop: term, body: proof_body future, export: unit lazy, consolidate: unit lazy}; -type proofs = proof * zproof; - 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); @@ -256,13 +253,15 @@ exception MIN_PROOF of unit; -fun proofs_of (PBody {proof, ...}) = proof; -val proof_of = fst o proofs_of; -val zproof_of = snd o proofs_of; +fun proof_of (PBody {proof, ...}) = proof; +fun zproof_of (PBody {zproof, ...}) = zproof; val join_proof = Future.join #> proof_of; -fun map_proofs_of f (PBody {oracles, thms, zboxes, proof}) = - PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = f proof}; +fun map_proof_of f (PBody {oracles, thms, zboxes, zproof, proof}) = + PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = f proof}; + +fun no_proofs (PBody {oracles, thms, zboxes, ...}) = + PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = MinProof, zproof = ZDummy}; fun thm_header serial pos theory_name name prop types : thm_header = {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types}; @@ -347,9 +346,9 @@ val empty_zboxes: zboxes = Inttab.empty; val union_zboxes = curry (Inttab.merge (fn (_: (zterm * zproof future), _) => true)); -val no_proof = (MinProof, ZDummy); -fun no_proof_body proof = PBody {oracles = [], thms = [], zboxes = empty_zboxes, proof = proof}; -val no_thm_body = thm_body (no_proof_body no_proof); +fun no_proof_body zproof proof = + PBody {oracles = [], thms = [], zboxes = empty_zboxes, zproof = zproof, proof = proof}; +val no_thm_body = thm_body (no_proof_body ZDummy MinProof); fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf) | no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf) @@ -372,7 +371,8 @@ | no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2 | no_body_proofs (PThm (header, Thm_Body {open_proof, body})) = let - val body' = Future.value (no_proof_body (proofs_of (Future.join body))); + val PBody {zproof, proof, ...} = Future.join body; + val body' = Future.value (no_proof_body zproof proof); val thm_body' = Thm_Body {open_proof = open_proof, body = body'}; in PThm (header, thm_body') end | no_body_proofs a = a; @@ -402,8 +402,8 @@ ([int_atom serial, theory_name, name], pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) (map Position.properties_of pos, - (prop, (types, map_proofs_of (apfst open_proof) (Future.join body)))))] -and proof_body consts (PBody {oracles, thms, zboxes = _, proof = (prf, _)}) = + (prop, (types, map_proof_of open_proof (Future.join body)))))] +and proof_body consts (PBody {oracles, thms, zboxes = _, zproof = _, proof = prf}) = triple (list (pair (pair string (properties o Position.properties_of)) (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf) and thm consts (a, thm_node) = @@ -471,7 +471,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, zboxes = empty_zboxes, proof = (c, ZDummy)} end + in PBody {oracles = a, thms = b, zboxes = empty_zboxes, zproof = ZDummy, proof = c} end and thm consts x = let val (a, (b, (c, (d, e)))) = @@ -533,7 +533,7 @@ | stripc x = x in stripc (prf, []) end; -fun strip_thm_body (body as PBody {proof = (proof, _), ...}) = +fun strip_thm_body (body as PBody {proof, ...}) = (case fst (strip_combt (fst (strip_combP proof))) of PThm (_, Thm_Body {body = body', ...}) => Future.join body' | _ => body); @@ -1982,7 +1982,7 @@ fun fulfill_norm_proof thy ps body0 = let val _ = consolidate_bodies (map #2 ps @ [body0]); - val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (proof0, zproof)} = body0; + val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof, proof = proof0} = body0; val oracles = unions_oracles (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]); @@ -1991,7 +1991,7 @@ val zboxes = fold (fn (_, PBody {zboxes, ...}) => union_zboxes zboxes) ps zboxes0; val proof = rew_proof thy proof0; in - PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = (proof, zproof)} + PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof} end; fun fulfill_proof_future thy promises (postproc: proof_body -> proof_body) body = @@ -2122,7 +2122,7 @@ fun prune_body body = if Options.default_bool "prune_proofs" - then (Future.map o map_proofs_of) (K no_proof) body + then Future.map no_proofs body else body; fun export_enabled () = Options.default_bool "export_proofs"; @@ -2200,18 +2200,19 @@ val (ucontext, prop1) = Logic.unconstrainT shyps prop; - val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (prf, zprf)} = body; + val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof = zprf, proof = prf} = body; val proofs = get_proofs_level (); val prf' = if proof_enabled proofs then fold_rev implies_intr_proof hyps prf else MinProof; val zprf' = if zproof_enabled proofs then ZTerm.todo_proof zprf else ZDummy; - val body0 = PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (prf', zprf')}; + val body0 = + PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof = zprf', proof = prf'}; fun new_prf () = let val i = serial (); val unconstrainT = unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext; - val postproc = map_proofs_of (apfst (unconstrainT #> named ? rew_proof thy)); + val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy); in (i, fulfill_proof_future thy promises postproc (Future.value body0)) end; val (i, body') = @@ -2224,7 +2225,7 @@ let val Thm_Body {body = body', ...} = thm_body'; val i = if a = "" andalso named then serial () else ser; - in (i, body' |> ser <> i ? Future.map (map_proofs_of (apfst (rew_proof thy)))) end + in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end else new_prf () | _ => new_prf ()); diff -r 8b371e684acf -r f9d972b464c1 src/Pure/thm.ML --- a/src/Pure/thm.ML Sat Dec 09 17:31:10 2023 +0100 +++ b/src/Pure/thm.ML Sat Dec 09 20:05:13 2023 +0100 @@ -744,11 +744,11 @@ (** derivations and promised proofs **) -fun make_deriv promises oracles thms zboxes proof = +fun make_deriv promises oracles thms zboxes zproof proof = Deriv {promises = promises, - body = PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = proof}}; + body = PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof}}; -val empty_deriv = make_deriv [] [] [] Proofterm.empty_zboxes Proofterm.no_proof; +val empty_deriv = make_deriv [] [] [] Proofterm.empty_zboxes ZDummy MinProof; (* inference rules *) @@ -756,12 +756,12 @@ val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i); fun deriv_rule2 (f, g) - (Deriv {promises = ps1, body = body1}) (Deriv {promises = ps2, body = body2}) = + (Deriv {promises = ps1, body = PBody body1}) (Deriv {promises = ps2, body = PBody body2}) = let val ps = Ord_List.union promise_ord ps1 ps2; - val PBody {oracles = oracles1, thms = thms1, zboxes = zboxes1, proof = (prf1, zprf1)} = body1; - val PBody {oracles = oracles2, thms = thms2, zboxes = zboxes2, proof = (prf2, zprf2)} = body2; + val {oracles = oracles1, thms = thms1, zboxes = zboxes1, zproof = zprf1, proof = prf1} = body1; + val {oracles = oracles2, thms = thms2, zboxes = zboxes2, zproof = zprf2, proof = prf2} = body2; val oracles = Proofterm.union_oracles oracles1 oracles2; val thms = Proofterm.union_thms thms1 thms2; @@ -770,7 +770,7 @@ val proofs = Proofterm.get_proofs_level (); val prf = if Proofterm.proof_enabled proofs then f prf1 prf2 else MinProof; val zprf = if Proofterm.zproof_enabled proofs then g zprf1 zprf2 else ZDummy; - in make_deriv ps oracles thms zboxes (prf, zprf) end; + in make_deriv ps oracles thms zboxes zprf prf end; fun deriv_rule1 (f, g) = deriv_rule2 (K f, K g) empty_deriv; @@ -778,14 +778,14 @@ let val proofs = Proofterm.get_proofs_level () in if Proofterm.proof_enabled proofs orelse Proofterm.zproof_enabled proofs then deriv_rule1 (I, I) (make_deriv [] [] [] Proofterm.empty_zboxes - (if Proofterm.proof_enabled proofs then f () else MinProof, - if Proofterm.zproof_enabled proofs then g () else ZDummy)) + (if Proofterm.zproof_enabled proofs then g () else ZDummy) + (if Proofterm.proof_enabled proofs then f () else MinProof)) else empty_deriv end; fun deriv_rule_unconditional (f, g) - (Deriv {promises, body = PBody {oracles, thms, zboxes, proof = (prf, zprf)}}) = - make_deriv promises oracles thms zboxes (f prf, g zprf); + (Deriv {promises, body = PBody {oracles, thms, zboxes, zproof = zprf, proof = prf}}) = + make_deriv promises oracles thms zboxes (g zprf) (f prf); (* fulfilled proofs *) @@ -845,7 +845,7 @@ val i = serial (); val future = future_thm |> Future.map (future_result i cert sorts prop); in - Thm (make_deriv [(i, future)] [] [] Proofterm.empty_zboxes Proofterm.no_proof, + Thm (make_deriv [(i, future)] [] [] Proofterm.empty_zboxes ZDummy MinProof, {cert = cert, tags = [], maxidx = maxidx, @@ -1026,10 +1026,11 @@ raise THEORY ("solve_constraints: bad theories for theorem\n" ^ Syntax.string_of_term_global thy (prop_of thm), thy :: bad_thys); - val Deriv {promises, body = PBody {oracles, thms, zboxes, proof}} = der; + val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der; val (oracles', thms', zboxes') = (oracles, thms, zboxes) |> fold (fold union_digest o constraint_digest) constraints; - val body' = PBody {oracles = oracles', thms = thms', zboxes = zboxes', proof = proof}; + val body' = + PBody {oracles = oracles', thms = thms', zboxes = zboxes', zproof = zproof, proof = proof}; in Thm (Deriv {promises = promises, body = body'}, {constraints = [], cert = cert, tags = tags, maxidx = maxidx, @@ -1134,7 +1135,7 @@ Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy) name_pos shyps hyps prop ps body; val zprf = ZTerm.todo_proof (Proofterm.zproof_of body); - val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes (prf, zprf); + val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes zprf prf; in Thm (der', args) end); fun close_derivation pos = @@ -1173,7 +1174,7 @@ then ZTerm.oracle_proof (Context.certificate_theory cert) name prop else ZDummy; in - Thm (make_deriv [] [oracle] [] Proofterm.empty_zboxes (proof, zproof), + Thm (make_deriv [] [oracle] [] Proofterm.empty_zboxes zproof proof, {cert = cert, tags = [], maxidx = maxidx, @@ -1916,7 +1917,7 @@ Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy) shyps prop ps body; val zprf = ZTerm.todo_proof body; - val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes (prf, zprf); + val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes zprf prf; val prop' = Proofterm.thm_node_prop (#2 pthm); in Thm (der',