# HG changeset patch # User wenzelm # Date 1236378308 -3600 # Node ID 9afd9a9d0812f1c0eadf6b9ff9364ba61a3602db # Parent 6a02238da8e9a63c61691a9993e98c2c0d14474d# Parent 5f859035331f27e8b64a4a7e122074d0ac6ec1ee merged diff -r 6a02238da8e9 -r 9afd9a9d0812 src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Mar 06 22:06:33 2009 +0100 +++ b/src/Provers/blast.ML Fri Mar 06 23:25:08 2009 +0100 @@ -643,13 +643,13 @@ (*Print tracing information at each iteration of prover*) fun tracing (State {thy, fullTrace, ...}) brs = - let fun printPairs (((G,_)::_,_)::_) = Output.immediate_output(traceTerm thy G) - | printPairs (([],(H,_)::_)::_) = Output.immediate_output(traceTerm thy H ^ "\t (Unsafe)") + let fun printPairs (((G,_)::_,_)::_) = Output.tracing (traceTerm thy G) + | printPairs (([],(H,_)::_)::_) = Output.tracing (traceTerm thy H ^ "\t (Unsafe)") | printPairs _ = () fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) = (fullTrace := brs0 :: !fullTrace; - List.app (fn _ => Output.immediate_output "+") brs; - Output.immediate_output (" [" ^ Int.toString lim ^ "] "); + List.app (fn _ => Output.tracing "+") brs; + Output.tracing (" [" ^ Int.toString lim ^ "] "); printPairs pairs; writeln"") in if !trace then printBrs (map normBr brs) else () @@ -662,10 +662,10 @@ if !trace then (case !ntrail-ntrl of 0 => () - | 1 => Output.immediate_output"\t1 variable UPDATED:" - | n => Output.immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:"); + | 1 => Output.tracing "\t1 variable UPDATED:" + | n => Output.tracing ("\t" ^ Int.toString n ^ " variables UPDATED:"); (*display the instantiations themselves, though no variable names*) - List.app (fn v => Output.immediate_output(" " ^ string_of thy 4 (the (!v)))) + List.app (fn v => Output.tracing (" " ^ string_of thy 4 (the (!v)))) (List.take(!trail, !ntrail-ntrl)); writeln"") else (); @@ -674,9 +674,9 @@ fun traceNew prems = if !trace then case length prems of - 0 => Output.immediate_output"branch closed by rule" - | 1 => Output.immediate_output"branch extended (1 new subgoal)" - | n => Output.immediate_output("branch split: "^ Int.toString n ^ " new subgoals") + 0 => Output.tracing "branch closed by rule" + | 1 => Output.tracing "branch extended (1 new subgoal)" + | n => Output.tracing ("branch split: "^ Int.toString n ^ " new subgoals") else (); @@ -1005,7 +1005,7 @@ NONE => closeF Ls | SOME tac => let val choices' = - (if !trace then (Output.immediate_output"branch closed"; + (if !trace then (Output.tracing "branch closed"; traceVars state ntrl) else (); prune state (nbrs, nxtVars, @@ -1136,9 +1136,9 @@ clearTo state ntrl; raise NEWBRANCHES) else traceNew prems; - if !trace andalso dup then Output.immediate_output" (duplicating)" + if !trace andalso dup then Output.tracing " (duplicating)" else (); - if !trace andalso recur then Output.immediate_output" (recursive)" + if !trace andalso recur then Output.tracing " (recursive)" else (); traceVars state ntrl; if null prems then nclosed := !nclosed + 1 diff -r 6a02238da8e9 -r 9afd9a9d0812 src/Pure/General/output.ML --- a/src/Pure/General/output.ML Fri Mar 06 22:06:33 2009 +0100 +++ b/src/Pure/General/output.ML Fri Mar 06 23:25:08 2009 +0100 @@ -32,7 +32,6 @@ val escape: output -> string val std_output: output -> unit val std_error: output -> unit - val immediate_output: string -> unit val writeln_default: output -> unit val writeln_fn: (output -> unit) ref val priority_fn: (output -> unit) ref @@ -89,8 +88,6 @@ fun std_error s = NAMED_CRITICAL "IO" (fn () => (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr)); -val immediate_output = std_output o output; - fun writeln_default "" = () | writeln_default s = std_output (suffix "\n" s); diff -r 6a02238da8e9 -r 9afd9a9d0812 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri Mar 06 22:06:33 2009 +0100 +++ b/src/Pure/Thy/thy_info.ML Fri Mar 06 23:25:08 2009 +0100 @@ -383,7 +383,12 @@ fun schedule_seq tasks = Graph.topological_order tasks - |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () () | _ => ())); + |> List.app (fn name => + (case Graph.get_node tasks name of + Task body => + let val after_load = body () + in after_load () handle exn => (kill_thy name; raise exn) end + | _ => ())); in diff -r 6a02238da8e9 -r 9afd9a9d0812 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Fri Mar 06 22:06:33 2009 +0100 +++ b/src/Pure/Tools/find_theorems.ML Fri Mar 06 23:25:08 2009 +0100 @@ -168,8 +168,7 @@ fun etacn thm i = Seq.take (! tac_limit) o etac thm i; fun try_thm thm = if Thm.no_prems thm then rtac thm 1 goal - else (etacn thm THEN_ALL_NEW - (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal; + else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal; in fn (_, thm) => if (is_some o Seq.pull o try_thm) thm @@ -181,11 +180,10 @@ fun filter_simp ctxt t (_, thm) = let - val (_, {mk_rews = {mk, ...}, ...}) = - Simplifier.rep_ss (Simplifier.local_simpset_of ctxt); + val mksimps = Simplifier.mksimps (Simplifier.local_simpset_of ctxt); val extract_simp = - (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl); - val ss = is_matching_thm extract_simp ctxt false t thm + (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); + val ss = is_matching_thm extract_simp ctxt false t thm; in if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE end; diff -r 6a02238da8e9 -r 9afd9a9d0812 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Fri Mar 06 22:06:33 2009 +0100 +++ b/src/Pure/meta_simplifier.ML Fri Mar 06 23:25:08 2009 +0100 @@ -59,6 +59,7 @@ val delcongs: simpset * thm list -> simpset val addsimprocs: simpset * simproc list -> simpset val delsimprocs: simpset * simproc list -> simpset + val mksimps: simpset -> thm -> thm list val setmksimps: simpset * (thm -> thm list) -> simpset val setmkcong: simpset * (thm -> thm) -> simpset val setmksym: simpset * (thm -> thm option) -> simpset @@ -547,6 +548,7 @@ fun add_simp thm ss = ss addsimps [thm]; fun del_simp thm ss = ss delsimps [thm]; + (* congs *) fun cong_name (Const (a, _)) = SOME a @@ -694,6 +696,8 @@ in +val mksimps = #mk o #mk_rews o #2 o rep_ss; + fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) => (mk, mk_cong, mk_sym, mk_eq_True, reorient)); diff -r 6a02238da8e9 -r 9afd9a9d0812 src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Fri Mar 06 22:06:33 2009 +0100 +++ b/src/Tools/eqsubst.ML Fri Mar 06 23:25:08 2009 +0100 @@ -128,8 +128,7 @@ (* changes object "=" to meta "==" which prepares a given rewrite rule *) fun prep_meta_eq ctxt = - let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt) - in mk #> map Drule.zero_var_indexes end; + Simplifier.mksimps (Simplifier.local_simpset_of ctxt) #> map Drule.zero_var_indexes; (* a type abriviation for match information *)