# HG changeset patch # User wenzelm # Date 1481893591 -3600 # Node ID e6aee01da22d3b13e47c1340026283a9998c7272 # Parent cec07f7249cdc33ea459c8084bcfa54322499193 tuned signature -- more abstract type thm_node; diff -r cec07f7249cd -r e6aee01da22d src/HOL/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Mirabelle/Tools/mirabelle.ML Thu Dec 15 22:22:45 2016 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Dec 16 14:06:31 2016 +0100 @@ -165,15 +165,17 @@ fun fold_body_thms f = let - fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => + fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => fn (x, seen) => if Inttab.defined seen i then (x, seen) else let - val body' = Future.join body - val (x', seen') = app (n + (if name = "" then 0 else 1)) body' + val name = Proofterm.thm_node_name thm_node + val prop = Proofterm.thm_node_prop thm_node + val body = Future.join (Proofterm.thm_node_body thm_node) + val (x', seen') = app (n + (if name = "" then 0 else 1)) body (x, Inttab.update (i, ()) seen) - in (x' |> n = 0 ? f (name, prop, body'), seen') end) + in (x' |> n = 0 ? f (name, prop, body), seen') end) in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end in diff -r cec07f7249cd -r e6aee01da22d src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Dec 15 22:22:45 2016 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Dec 16 14:06:31 2016 +0100 @@ -84,8 +84,10 @@ be missing over there; or maybe the two code portions are not doing the same? *) fun fold_body_thm max_thms outer_name (map_plain_name, map_inclass_name) body = let - fun app_thm map_name (_, (name, _, body)) (accum as (num_thms, names)) = + fun app_thm map_name (_, thm_node) (accum as (num_thms, names)) = let + val name = Proofterm.thm_node_name thm_node + val body = Proofterm.thm_node_body thm_node val (anonymous, enter_class) = (* The "name = outer_name" case caters for the uncommon case where the proved theorem occurs in its own proof (e.g., "Transitive_Closure.trancl_into_trancl"). *) diff -r cec07f7249cd -r e6aee01da22d src/Pure/Tools/thm_deps.ML --- a/src/Pure/Tools/thm_deps.ML Thu Dec 15 22:22:45 2016 +0100 +++ b/src/Pure/Tools/thm_deps.ML Fri Dec 16 14:06:31 2016 +0100 @@ -35,7 +35,7 @@ | NONE => []) | _ => ["global"]); val node = make_node name (space_implode "/" (session @ prefix)); - val deps = filter_out (fn s => s = "") (map (#1 o #2) thms'); + val deps = filter_out (fn s => s = "") (map (Proofterm.thm_node_name o #2) thms'); in Symtab.update (name, (node, deps)) end; val entries0 = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) Symtab.empty; val entries1 = diff -r cec07f7249cd -r e6aee01da22d src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Thu Dec 15 22:22:45 2016 +0100 +++ b/src/Pure/proofterm.ML Fri Dec 16 14:06:31 2016 +0100 @@ -10,6 +10,7 @@ sig val proofs: int Unsynchronized.ref + type thm_node datatype proof = MinProof | PBound of int @@ -25,7 +26,7 @@ | PThm of serial * ((string * term * typ list option) * proof_body future) and proof_body = PBody of {oracles: (string * term) Ord_List.T, - thms: (serial * (string * term * proof_body future)) Ord_List.T, + thms: (serial * thm_node) Ord_List.T, proof: proof} val %> : proof * term -> proof @@ -35,9 +36,12 @@ sig include BASIC_PROOFTERM + type pthm = serial * thm_node type oracle = string * term - type pthm = serial * (string * term * proof_body future) val proof_of: proof_body -> proof + val thm_node_name: thm_node -> string + val thm_node_prop: thm_node -> term + val thm_node_body: thm_node -> proof_body future val join_proof: proof_body future -> proof 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) -> @@ -176,16 +180,22 @@ | PThm of serial * ((string * term * typ list option) * proof_body future) and proof_body = PBody of {oracles: (string * term) Ord_List.T, - thms: (serial * (string * term * proof_body future)) Ord_List.T, - proof: proof}; + thms: (serial * thm_node) Ord_List.T, + proof: proof} +and thm_node = Thm_Node of string * term * proof_body future; type oracle = string * term; -type pthm = serial * (string * term * proof_body future); +type pthm = serial * thm_node; fun proof_of (PBody {proof, ...}) = proof; val join_proof = Future.join #> proof_of; -fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms)); +fun thm_node_name (Thm_Node (name, _, _)) = name; +fun thm_node_prop (Thm_Node (_, prop, _)) = prop; +fun thm_node_body (Thm_Node (_, _, body)) = body; + +fun join_thms (thms: pthm list) = + ignore (Future.joins (map (fn (_, Thm_Node (_, _, body)) => body) thms)); (***** proof atoms *****) @@ -208,7 +218,7 @@ fun fold_body_thms f = let fun app (PBody {thms, ...}) = - tap join_thms thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) => + tap join_thms thms |> fold (fn (i, Thm_Node (name, prop, body)) => fn (x, seen) => if Inttab.defined seen i then (x, seen) else let @@ -224,7 +234,7 @@ fun status (PBody {oracles, thms, ...}) x = let val ((oracle, unfinished, failed), seen) = - (thms, x) |-> fold (fn (i, (_, _, body)) => fn (st, seen) => + (thms, x) |-> fold (fn (i, Thm_Node (_, _, body)) => fn (st, seen) => if Inttab.defined seen i then (st, seen) else let val seen' = Inttab.update (i, ()) seen in @@ -246,7 +256,7 @@ (* proof body *) val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord; -fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i); +fun thm_ord ((i, _): pthm, (j, _): pthm) = int_ord (j, i); val unions_oracles = Ord_List.unions oracle_ord; val unions_thms = Ord_List.unions thm_ord; @@ -254,7 +264,7 @@ val all_oracles_of = let fun collect (PBody {oracles, thms, ...}) = - tap join_thms thms |> fold (fn (i, (_, _, body)) => fn (x, seen) => + tap join_thms thms |> fold (fn (i, Thm_Node (_, _, body)) => fn (x, seen) => if Inttab.defined seen i then (x, seen) else let @@ -267,7 +277,7 @@ let val (oracles, thms) = fold_proof_atoms false (fn Oracle (s, prop, _) => apfst (cons (s, prop)) - | PThm (i, ((name, prop, _), body)) => apsnd (cons (i, (name, prop, body))) + | PThm (i, ((name, prop, _), body)) => apsnd (cons (i, Thm_Node (name, prop, body))) | _ => I) [prf] ([], []); in PBody @@ -311,7 +321,7 @@ ([int_atom a, b], triple term (option (list typ)) proof_body (c, d, Future.join body))] and proof_body (PBody {oracles, thms, proof = prf}) = triple (list (pair string term)) (list pthm) proof (oracles, thms, prf) -and pthm (a, (b, c, body)) = +and pthm (a, Thm_Node (b, c, body)) = pair int (triple string term proof_body) (a, (b, c, Future.join body)); in @@ -348,7 +358,7 @@ in PBody {oracles = a, thms = b, proof = c} end and pthm x = let val (a, (b, c, d)) = pair int (triple string term proof_body) x - in (a, (b, c, Future.value d)) end; + in (a, Thm_Node (b, c, Future.value d)) end; in @@ -1606,7 +1616,7 @@ else new_prf () | _ => new_prf ()); val head = PThm (i, ((name, prop1, NONE), body')); - in ((i, (name, prop1, body')), head, args, argsP, args1) end; + in ((i, Thm_Node (name, prop1, body')), head, args, argsP, args1) end; fun thm_proof thy name shyps hyps concl promises body = let val (pthm, head, args, argsP, _) = prepare_thm_proof thy name shyps hyps concl promises body diff -r cec07f7249cd -r e6aee01da22d src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Dec 15 22:22:45 2016 +0100 +++ b/src/Pure/thm.ML Fri Dec 16 14:06:31 2016 +0100 @@ -1309,9 +1309,9 @@ val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); val ps = map (apsnd (Future.map fulfill_body)) promises; - val (pthm as (_, (_, prop', _)), proof) = - Proofterm.unconstrain_thm_proof thy shyps prop ps body; + val (pthm, proof) = Proofterm.unconstrain_thm_proof thy shyps prop ps body; val der' = make_deriv [] [] [pthm] proof; + val prop' = Proofterm.thm_node_prop (#2 pthm); in Thm (der', {cert = cert,