# HG changeset patch # User wenzelm # Date 1481914246 -3600 # Node ID d44f0b714e13b15803399ca7f7a3bd031e44548f # Parent a7664ca9ffc5b70dc660a20bf495e98292d3efc5# Parent 1134e4d5e5b711b573e9f3775aa2ae2c0a93f244 merged diff -r a7664ca9ffc5 -r d44f0b714e13 src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Dec 16 19:50:46 2016 +0100 @@ -167,7 +167,7 @@ assms |> map (apsnd (rewrite ctxt eqs')) |> map (apsnd (Conv.fconv_rule Thm.eta_conversion)) - |> Old_Z3_Proof_Tools.thm_net_of snd + |> Old_Z3_Proof_Tools.thm_net_of snd fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion @@ -183,14 +183,14 @@ if exact then (Thm.implies_elim thm1 th, ctxt) else assume thm1 ctxt val thms' = if exact then thms else th :: thms - in + in ((insert (op =) i is, thms'), (ctxt', Inttab.update (idx, Thm thm) ptab)) end fun add (idx, ct) (cx as ((is, thms), (ctxt, ptab))) = let - val thm1 = + val thm1 = Thm.trivial ct |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt)) val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1 @@ -218,7 +218,7 @@ val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp} in fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p) - | mp p_q p = + | mp p_q p = let val pq = thm_of p_q val thm = comp iffD1_c pq handle THM _ => comp mp_c pq @@ -509,7 +509,7 @@ (case lookup (Logic.mk_equals (apply2 Thm.term_of cp)) of SOME eq => eq | NONE => if exn then raise MONO else prove_refl cp) - + val prove_exn = prove_eq true and prove_safe = prove_eq false @@ -752,7 +752,9 @@ fun check_after idx r ps ct (p, (ctxt, _)) = if not (Config.get ctxt Old_SMT_Config.trace) then () else - let val thm = thm_of p |> tap (Thm.join_proofs o single) + let + val thm = thm_of p + val _ = Thm.consolidate thm in if (Thm.cprop_of thm) aconvc ct then () else @@ -852,7 +854,7 @@ fun discharge_assms_tac ctxt rules = REPEAT (HEADGOAL (resolve_tac ctxt rules ORELSE' SOLVED' (discharge_sk_tac ctxt))) - + fun discharge_assms ctxt rules thm = if Thm.nprems_of thm = 0 then Goal.norm_result ctxt thm else @@ -881,7 +883,7 @@ if Config.get ctxt2 Old_SMT_Config.filter_only_facts then (is, @{thm TrueI}) else (Thm @{thm TrueI}, cxp) - |> fold (prove simpset vars) steps + |> fold (prove simpset vars) steps |> discharge rules outer_ctxt |> pair [] end diff -r a7664ca9ffc5 -r d44f0b714e13 src/HOL/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Mirabelle/Tools/mirabelle.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Dec 16 19:50:46 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 a7664ca9ffc5 -r d44f0b714e13 src/HOL/Proofs/ex/Proof_Terms.thy --- a/src/HOL/Proofs/ex/Proof_Terms.thy Thu Dec 15 15:05:35 2016 +0100 +++ b/src/HOL/Proofs/ex/Proof_Terms.thy Fri Dec 16 19:50:46 2016 +0100 @@ -30,7 +30,7 @@ (*all theorems used in the graph of nested proofs*) val all_thms = Proofterm.fold_body_thms - (fn (name, _, _) => insert (op =) name) [body] []; + (fn {name, ...} => insert (op =) name) [body] []; \ text \ diff -r a7664ca9ffc5 -r d44f0b714e13 src/HOL/ROOT --- a/src/HOL/ROOT Thu Dec 15 15:05:35 2016 +0100 +++ b/src/HOL/ROOT Fri Dec 16 19:50:46 2016 +0100 @@ -18,10 +18,9 @@ description {* HOL-Main with explicit proof terms. *} - options [document = false, quick_and_dirty = false] + options [document = false, quick_and_dirty = false, parallel_proofs = 0] theories Proofs (*sequential change of global flag!*) - theories List - theories [checkpoint] "~~/src/HOL/Library/Old_Datatype" + theories "~~/src/HOL/Library/Old_Datatype" files "Tools/Quickcheck/Narrowing_Engine.hs" "Tools/Quickcheck/PNF_Narrowing_Engine.hs" diff -r a7664ca9ffc5 -r d44f0b714e13 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Dec 16 19:50:46 2016 +0100 @@ -293,7 +293,7 @@ | SOME _ => error ("Cannot associate a type with " ^ s ^ "\nsince it is no record or enumeration type"); -fun check_enum [] [] = NONE +fun check_enum [] [] = NONE | check_enum els [] = SOME ("has no element(s) " ^ commas els) | check_enum [] cs = SOME ("has extra element(s) " ^ commas (map (Long_Name.base_name o fst) cs)) @@ -305,7 +305,7 @@ fun invert_map [] = I | invert_map cmap = map (apfst (the o AList.lookup (op =) (map swap cmap))); - + fun add_type_def prfx (s, Basic_Type ty) (ids, thy) = (check_no_assoc thy prfx s; (ids, @@ -677,7 +677,7 @@ "+", "-", "*", "/", "div", "mod", "**"]); fun complex_expr (Number _) = false - | complex_expr (Ident _) = false + | complex_expr (Ident _) = false | complex_expr (Funct (s, es)) = not (Symtab.defined builtin s) orelse exists complex_expr es | complex_expr (Quantifier (_, _, _, e)) = complex_expr e @@ -959,7 +959,7 @@ | SOME {vcs, path, ...} => let val (proved, unproved) = partition_vcs vcs; - val _ = Thm.join_proofs (maps (#2 o snd) proved); + val _ = List.app Thm.consolidate (maps (#2 o snd) proved); val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) => exists (#oracle o Thm.peek_status) thms) proved; @@ -1117,7 +1117,7 @@ [(term_of_rule thy' prfx types pfuns ids rl, [])])) other_rules), Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])] - + in set_env ctxt defs' types funs ids vcs' path prfx thy' end; diff -r a7664ca9ffc5 -r d44f0b714e13 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Dec 16 19:50:46 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 a7664ca9ffc5 -r d44f0b714e13 src/Pure/Concurrent/multithreading.ML --- a/src/Pure/Concurrent/multithreading.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/Pure/Concurrent/multithreading.ML Fri Dec 16 19:50:46 2016 +0100 @@ -61,7 +61,7 @@ val trace = ref 0; fun tracing level msg = - if level > ! trace then () + if ! trace < level then () else Thread_Attributes.uninterruptible (fn _ => fn () => (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr) handle _ (*sic*) => ()) (); @@ -79,20 +79,27 @@ fun synchronized name lock e = Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () => - let - val immediate = - if Mutex.trylock lock then true - else - let - val _ = tracing 5 (fn () => name ^ ": locking ..."); - val timer = Timer.startRealTimer (); - val _ = Mutex.lock lock; - val time = Timer.checkRealTimer timer; - val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time); - in false end; - val result = Exn.capture (restore_attributes e) (); - val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ..."); - val _ = Mutex.unlock lock; - in result end) ()); + if ! trace > 0 then + let + val immediate = + if Mutex.trylock lock then true + else + let + val _ = tracing 5 (fn () => name ^ ": locking ..."); + val timer = Timer.startRealTimer (); + val _ = Mutex.lock lock; + val time = Timer.checkRealTimer timer; + val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time); + in false end; + val result = Exn.capture (restore_attributes e) (); + val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ..."); + val _ = Mutex.unlock lock; + in result end + else + let + val _ = Mutex.lock lock; + val result = Exn.capture (restore_attributes e) (); + val _ = Mutex.unlock lock; + in result end) ()); end; diff -r a7664ca9ffc5 -r d44f0b714e13 src/Pure/Concurrent/thread_attributes.ML --- a/src/Pure/Concurrent/thread_attributes.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/Pure/Concurrent/thread_attributes.ML Fri Dec 16 19:50:46 2016 +0100 @@ -88,14 +88,20 @@ val w'' = Word.andb (w, Word.notb interrupt_state); in Attributes (if w' = interrupt_asynch then Word.orb (w'', interrupt_asynch_once) else w) end; -end; - fun with_attributes new_atts e = let - val orig_atts = safe_interrupts (get_attributes ()); - val result = Exn.capture (fn () => (set_attributes (safe_interrupts new_atts); e orig_atts)) (); - val _ = set_attributes orig_atts; - in Exn.release result end; + val atts1 = safe_interrupts (get_attributes ()); + val atts2 = safe_interrupts new_atts; + in + if atts1 = atts2 then e atts1 + else + let + val result = Exn.capture (fn () => (set_attributes atts2; e atts1)) (); + val _ = set_attributes atts1; + in Exn.release result end + end; + +end; fun uninterruptible f x = with_attributes no_interrupts (fn atts => diff -r a7664ca9ffc5 -r d44f0b714e13 src/Pure/General/source.ML --- a/src/Pure/General/source.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/Pure/General/source.ML Fri Dec 16 19:50:46 2016 +0100 @@ -14,9 +14,8 @@ val map_filter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source val of_list: 'a list -> ('a, 'a list) source + val of_string: string -> (string, string list) source val exhausted: ('a, 'b) source -> ('a, 'a list) source - val of_string: string -> (string, string list) source - val of_string_limited: int -> string -> (string, substring) source val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) -> ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source val source: 'a Scan.stopper -> ('a list -> 'b list * 'a list) -> @@ -84,20 +83,9 @@ fun of_list xs = make_source [] xs (fn xs => (xs, [])); -fun exhausted src = of_list (exhaust src); - - -(* string source *) - val of_string = of_list o raw_explode; -fun of_string_limited limit str = - make_source [] (Substring.full str) - (fn s => - let - val (s1, s2) = Substring.splitAt (s, Int.min (Substring.size s, limit)); - val cs = map String.str (Substring.explode s1); - in (cs, s2) end); +fun exhausted src = of_list (exhaust src); diff -r a7664ca9ffc5 -r d44f0b714e13 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/Pure/Isar/proof.ML Fri Dec 16 19:50:46 2016 +0100 @@ -522,8 +522,7 @@ fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal); val th = - (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal) - handle THM _ => err_lost ()) + (Goal.conclude (Thm.close_derivation goal) handle THM _ => err_lost ()) |> Drule.flexflex_unique (SOME ctxt) |> Thm.check_shyps ctxt |> Thm.check_hyps (Context.Proof ctxt); diff -r a7664ca9ffc5 -r d44f0b714e13 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/Pure/Thy/thy_info.ML Fri Dec 16 19:50:46 2016 +0100 @@ -159,7 +159,7 @@ (*toplevel proofs and diags*) val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek exec_id)); (*fully nested proofs*) - val res = Exn.capture Thm.join_theory_proofs theory; + val res = Exn.capture Thm.consolidate_theory theory; in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end; datatype task = diff -r a7664ca9ffc5 -r d44f0b714e13 src/Pure/Tools/thm_deps.ML --- a/src/Pure/Tools/thm_deps.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/Pure/Tools/thm_deps.ML Fri Dec 16 19:50:46 2016 +0100 @@ -20,8 +20,8 @@ fun make_node name directory = Graph_Display.session_node {name = Long_Name.base_name name, directory = directory, unfold = false, path = ""}; - fun add_dep ("", _, _) = I - | add_dep (name, _, PBody {thms = thms', ...}) = + fun add_dep {name = "", ...} = I + | add_dep {name = name, body = PBody {thms = thms', ...}, ...} = let val prefix = #1 (split_last (Long_Name.explode name)); val session = @@ -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 = @@ -73,7 +73,7 @@ val used = Proofterm.fold_body_thms - (fn (a, _, _) => a <> "" ? Symtab.update (a, ())) + (fn {name = a, ...} => a <> "" ? Symtab.update (a, ())) (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms))) Symtab.empty; diff -r a7664ca9ffc5 -r d44f0b714e13 src/Pure/goal.ML --- a/src/Pure/goal.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/Pure/goal.ML Fri Dec 16 19:50:46 2016 +0100 @@ -232,7 +232,7 @@ (Thm.term_of stmt); in res - |> length props > 1 ? Thm.close_derivation + |> Thm.close_derivation |> Conjunction.elim_balanced (length props) |> map (Assumption.export false ctxt' ctxt) |> Variable.export ctxt' ctxt diff -r a7664ca9ffc5 -r d44f0b714e13 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/Pure/more_thm.ML Fri Dec 16 19:50:46 2016 +0100 @@ -111,7 +111,7 @@ val untag: string -> attribute val kind: string -> attribute val register_proofs: thm list -> theory -> theory - val join_theory_proofs: theory -> unit + val consolidate_theory: theory -> unit val show_consts_raw: Config.raw val show_consts: bool Config.T val show_hyps_raw: Config.raw @@ -452,8 +452,7 @@ (* close_derivation *) fun close_derivation thm = - if Thm.derivation_name thm = "" then Thm.name_derivation "" thm - else thm; + if Thm.derivation_closed thm then thm else Thm.name_derivation "" thm; (* user renaming of parameters in a subgoal *) @@ -645,8 +644,8 @@ fun register_proofs more_thms = Proofs.map (fold (cons o Thm.trim_context) more_thms); -fun join_theory_proofs thy = - Thm.join_proofs (map (Thm.transfer thy) (rev (Proofs.get thy))); +fun consolidate_theory thy = + List.app (Thm.consolidate o Thm.transfer thy) (rev (Proofs.get thy)); diff -r a7664ca9ffc5 -r d44f0b714e13 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/Pure/proofterm.ML Fri Dec 16 19:50:46 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,13 +36,17 @@ 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: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a - val join_bodies: proof_body list -> unit + val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) -> + proof_body list -> 'a -> 'a + val consolidate: proof_body -> unit val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool} val oracle_ord: oracle * oracle -> order @@ -60,6 +65,8 @@ (** primitive operations **) val proofs_enabled: unit -> bool + val atomic_proof: proof -> bool + val compact_proof: proof -> bool val proof_combt: proof * term list -> proof val proof_combt': proof * term option list -> proof val proof_combP: proof * proof list -> proof @@ -173,16 +180,35 @@ | 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 {name: string, prop: term, body: proof_body future, consolidate: unit lazy}; 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 rep_thm_node (Thm_Node args) = args; +val thm_node_name = #name o rep_thm_node; +val thm_node_prop = #prop o rep_thm_node; +val thm_node_body = #body o rep_thm_node; +val thm_node_consolidate = #consolidate o rep_thm_node; + +fun join_thms (thms: pthm list) = + Future.joins (map (thm_node_body o #2) thms); + +fun consolidate (PBody {thms, ...}) = + List.app (Lazy.force o thm_node_consolidate o #2) thms; + +fun make_thm_node name prop body = + Thm_Node {name = name, prop = prop, body = body, + consolidate = + Lazy.lazy (fn () => + let val PBody {thms, ...} = Future.join body + in List.app consolidate (join_thms thms) end)}; (***** proof atoms *****) @@ -205,27 +231,27 @@ 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) => fn (x, seen) => if Inttab.defined seen i then (x, seen) else let - val body' = Future.join body; - val (x', seen') = app body' (x, Inttab.update (i, ()) seen); - in (f (name, prop, body') x', seen') end); + val name = thm_node_name thm_node; + val prop = thm_node_prop thm_node; + val body = Future.join (thm_node_body thm_node); + val (x', seen') = app body (x, Inttab.update (i, ()) seen); + in (f {serial = i, name = name, prop = prop, body = body} x', seen') end); in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end; -fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies (); - fun peek_status bodies = let 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) => fn (st, seen) => if Inttab.defined seen i then (st, seen) else let val seen' = Inttab.update (i, ()) seen in - (case Future.peek body of + (case Future.peek (thm_node_body thm_node) of SOME (Exn.Res body') => status body' (st, seen') | SOME (Exn.Exn _) => let val (oracle, unfinished, _) = st @@ -243,7 +269,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; @@ -251,12 +277,12 @@ 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) => fn (x, seen) => if Inttab.defined seen i then (x, seen) else let - val body' = Future.join body; - val (x', seen') = collect body' (x, Inttab.update (i, ()) seen); + val body = Future.join (thm_node_body thm_node); + val (x', seen') = collect body (x, Inttab.update (i, ()) seen); in (if null oracles then x' else oracles :: x', seen') end); in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end; @@ -264,7 +290,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, make_thm_node name prop body)) | _ => I) [prf] ([], []); in PBody @@ -308,8 +334,9 @@ ([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)) = - pair int (triple string term proof_body) (a, (b, c, Future.join body)); +and pthm (a, thm_node) = + pair int (triple string term proof_body) + (a, (thm_node_name thm_node, thm_node_prop thm_node, Future.join (thm_node_body thm_node))); in @@ -345,7 +372,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, make_thm_node b c (Future.value d)) end; in @@ -357,6 +384,19 @@ (***** proof objects with different levels of detail *****) +fun atomic_proof prf = + (case prf of + Abst _ => false + | AbsP _ => false + | op % _ => false + | op %% _ => false + | Promise _ => false + | _ => true); + +fun compact_proof (prf % _) = compact_proof prf + | compact_proof (prf1 %% prf2) = atomic_proof prf2 andalso compact_proof prf1 + | compact_proof prf = atomic_proof prf; + fun (prf %> t) = prf % SOME t; val proof_combt = Library.foldl (op %>); @@ -533,11 +573,13 @@ prf_add_loose_bnos plev tlev prf2 (prf_add_loose_bnos plev tlev prf1 p) | prf_add_loose_bnos plev tlev (prf % opt) (is, js) = - prf_add_loose_bnos plev tlev prf (case opt of + prf_add_loose_bnos plev tlev prf + (case opt of NONE => (is, insert (op =) ~1 js) | SOME t => (is, add_loose_bnos (t, tlev, js))) | prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) = - prf_add_loose_bnos (plev+1) tlev prf (case opt of + prf_add_loose_bnos (plev+1) tlev prf + (case opt of NONE => (is, insert (op =) ~1 js) | SOME t => (is, add_loose_bnos (t, tlev, js))) | prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p = @@ -635,7 +677,7 @@ handle Same.SAME => prf % Same.map_option (subst' lev) t) | subst _ _ = raise Same.SAME and substh lev prf = (subst lev prf handle Same.SAME => prf); - in case args of [] => prf | _ => substh 0 prf end; + in (case args of [] => prf | _ => substh 0 prf) end; fun prf_subst_pbounds args prf = let @@ -651,7 +693,7 @@ | subst (prf % t) Plev tlev = subst prf Plev tlev % t | subst _ _ _ = raise Same.SAME and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf) - in case args of [] => prf | _ => substh prf 0 0 end; + in (case args of [] => prf | _ => substh prf 0 0) end; (**** Freezing and thawing of variables in proof terms ****) @@ -992,7 +1034,7 @@ | Var _ => SOME (remove_types t) | _ => NONE) % (case head_of g of - Abs _ => SOME (remove_types u) + Abs _ => SOME (remove_types u) | Var _ => SOME (remove_types u) | _ => NONE) %% prf1 %% prf2 | _ => prf % NONE % NONE %% prf1 %% prf2) @@ -1105,7 +1147,8 @@ add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t) | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t) | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t) -and add_npvars' Ts (vs, t) = (case strip_comb t of +and add_npvars' Ts (vs, t) = + (case strip_comb t of (Var (ixn, _), ts) => if test_args [] ts then vs else Library.foldl (add_npvars' Ts) (AList.update (op =) (ixn, @@ -1115,19 +1158,20 @@ fun prop_vars (Const ("Pure.imp", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q) | prop_vars (Const ("Pure.all", _) $ Abs (_, _, t)) = prop_vars t - | prop_vars t = (case strip_comb t of - (Var (ixn, _), _) => [ixn] | _ => []); + | prop_vars t = (case strip_comb t of (Var (ixn, _), _) => [ixn] | _ => []); fun is_proj t = let - fun is_p i t = (case strip_comb t of + fun is_p i t = + (case strip_comb t of (Bound _, []) => false | (Bound j, ts) => j >= i orelse exists (is_p i) ts | (Abs (_, _, u), _) => is_p (i+1) u | (_, ts) => exists (is_p i) ts) - in (case strip_abs_body t of - Bound _ => true - | t' => is_p 0 t') + in + (case strip_abs_body t of + Bound _ => true + | t' => is_p 0 t') end; fun needed_vars prop = @@ -1196,7 +1240,8 @@ val (ts', ts'') = chop (length vs) ts; val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts'; val nvs = Library.foldl (fn (ixns', (ixn, ixns)) => - insert (op =) ixn (case AList.lookup (op =) insts ixn of + insert (op =) ixn + (case AList.lookup (op =) insts ixn of SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns' | _ => union (op =) ixns ixns')) (needed prop ts'' prfs, add_npvars false true [] ([], prop)); @@ -1250,12 +1295,12 @@ fun mtch Ts i j (pinst, tinst) (Hyp (Var (ixn, _)), prf) = if i = 0 andalso j = 0 then ((ixn, prf) :: pinst, tinst) - else (case apfst (flt i) (apsnd (flt j) - (prf_add_loose_bnos 0 0 prf ([], []))) of + else + (case apfst (flt i) (apsnd (flt j) (prf_add_loose_bnos 0 0 prf ([], []))) of ([], []) => ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst) - | ([], _) => if j = 0 then - ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst) - else raise PMatch + | ([], _) => + if j = 0 then ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst) + else raise PMatch | _ => raise PMatch) | mtch Ts i j inst (prf1 % opt1, prf2 % opt2) = optmatch (matcht Ts j) (mtch Ts i j inst (prf1, prf2)) (opt1, opt2) @@ -1389,45 +1434,57 @@ | rew0 Ts hs prf = rew Ts hs prf; fun rew1 _ _ (Hyp (Var _)) _ = NONE - | rew1 Ts hs skel prf = (case rew2 Ts hs skel prf of - SOME prf1 => (case rew0 Ts hs prf1 of - SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2)) - | NONE => SOME prf1) - | NONE => (case rew0 Ts hs prf of - SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1)) - | NONE => NONE)) + | rew1 Ts hs skel prf = + (case rew2 Ts hs skel prf of + SOME prf1 => + (case rew0 Ts hs prf1 of + SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2)) + | NONE => SOME prf1) + | NONE => + (case rew0 Ts hs prf of + SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1)) + | NONE => NONE)) - and rew2 Ts hs skel (prf % SOME t) = (case prf of + and rew2 Ts hs skel (prf % SOME t) = + (case prf of Abst (_, _, body) => let val prf' = prf_subst_bounds [t] body in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end - | _ => (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of - SOME prf' => SOME (prf' % SOME t) - | NONE => NONE)) + | _ => + (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of + SOME prf' => SOME (prf' % SOME t) + | NONE => NONE)) | rew2 Ts hs skel (prf % NONE) = Option.map (fn prf' => prf' % NONE) (rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf) - | rew2 Ts hs skel (prf1 %% prf2) = (case prf1 of + | rew2 Ts hs skel (prf1 %% prf2) = + (case prf1 of AbsP (_, _, body) => let val prf' = prf_subst_pbounds [prf2] body in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end | _ => - let val (skel1, skel2) = (case skel of - skel1 %% skel2 => (skel1, skel2) - | _ => (no_skel, no_skel)) - in case rew1 Ts hs skel1 prf1 of - SOME prf1' => (case rew1 Ts hs skel2 prf2 of + let + val (skel1, skel2) = + (case skel of + skel1 %% skel2 => (skel1, skel2) + | _ => (no_skel, no_skel)) + in + (case rew1 Ts hs skel1 prf1 of + SOME prf1' => + (case rew1 Ts hs skel2 prf2 of SOME prf2' => SOME (prf1' %% prf2') | NONE => SOME (prf1' %% prf2)) - | NONE => (case rew1 Ts hs skel2 prf2 of + | NONE => + (case rew1 Ts hs skel2 prf2 of SOME prf2' => SOME (prf1 %% prf2') - | NONE => NONE) + | NONE => NONE)) end) - | rew2 Ts hs skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) hs + | rew2 Ts hs skel (Abst (s, T, prf)) = + (case rew1 (the_default dummyT T :: Ts) hs (case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of SOME prf' => SOME (Abst (s, T, prf')) | NONE => NONE) - | rew2 Ts hs skel (AbsP (s, t, prf)) = (case rew1 Ts (t :: hs) - (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of + | rew2 Ts hs skel (AbsP (s, t, prf)) = + (case rew1 Ts (t :: hs) (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of SOME prf' => SOME (AbsP (s, t, prf')) | NONE => NONE) | rew2 _ _ _ _ = NONE; @@ -1476,6 +1533,8 @@ fun fulfill_norm_proof thy ps body0 = let + val _ = List.app (consolidate o #2) ps; + val _ = consolidate body0; val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0; val oracles = unions_oracles @@ -1573,15 +1632,14 @@ 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, make_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 in (pthm, proof_combP (proof_combt' (head, args), argsP)) end; fun unconstrain_thm_proof thy shyps concl promises body = - let - val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body + let val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body in (pthm, proof_combt' (head, args)) end; diff -r a7664ca9ffc5 -r d44f0b714e13 src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Dec 15 15:05:35 2016 +0100 +++ b/src/Pure/thm.ML Fri Dec 16 19:50:46 2016 +0100 @@ -86,9 +86,10 @@ val proof_bodies_of: thm list -> proof_body list val proof_body_of: thm -> proof_body val proof_of: thm -> proof - val join_proofs: thm list -> unit + val consolidate: thm -> unit val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool} val future: thm future -> cterm -> thm + val derivation_closed: thm -> bool val derivation_name: thm -> string val name_derivation: string -> thm -> thm val axiom: theory -> string -> thm @@ -584,21 +585,14 @@ 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}, _)) = - Proofterm.fulfill_norm_proof (theory_of_thm th) (fulfill_promises promises) body -and fulfill_promises promises = - map fst promises ~~ map fulfill_body (Future.joins (map snd promises)); + 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 = - let - val _ = join_promises_of thms; - val bodies = map fulfill_body thms; - val _ = Proofterm.join_bodies bodies; - in bodies end; - +fun proof_bodies_of thms = (join_promises_of thms; map fulfill_body thms); val proof_body_of = singleton proof_bodies_of; val proof_of = Proofterm.proof_of o proof_body_of; -val join_proofs = ignore o proof_bodies_of; +val consolidate = ignore o proof_bodies_of o single; (* derivation status *) @@ -655,6 +649,10 @@ (* closed derivations with official name *) (*non-deterministic, depends on unknown promises*) +fun derivation_closed (Thm (Deriv {body, ...}, _)) = + Proofterm.compact_proof (Proofterm.proof_of body); + +(*non-deterministic, depends on unknown promises*) fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = Proofterm.get_name shyps hyps prop (Proofterm.proof_of body); @@ -1305,9 +1303,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,