--- a/Admin/isatest/isatest-makedist Wed Jul 22 10:49:26 2009 +0200
+++ b/Admin/isatest/isatest-makedist Wed Jul 22 11:23:09 2009 +0200
@@ -110,8 +110,8 @@
sleep 15
$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly"
sleep 15
-$SSH macbroy6 "$MAKEALL $HOME/settings/at-mac-poly-5.1-para"
-sleep 15
+#$SSH macbroy6 "$MAKEALL $HOME/settings/at-mac-poly-5.1-para"
+#sleep 15
$SSH atbroy51 "$HOME/admin/isatest/isatest-annomaly"
echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
--- a/Admin/isatest/settings/mac-poly-M4 Wed Jul 22 10:49:26 2009 +0200
+++ b/Admin/isatest/settings/mac-poly-M4 Wed Jul 22 11:23:09 2009 +0200
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-experimental"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="--mutable 800 --immutable 2000"
+ ML_OPTIONS="--mutable 600 --immutable 1800"
ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
@@ -25,4 +25,4 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4"
-HOL_USEDIR_OPTIONS="-p 2 -q 1"
+HOL_USEDIR_OPTIONS="-p 2 -q 0"
--- a/Admin/isatest/settings/mac-poly-M8 Wed Jul 22 10:49:26 2009 +0200
+++ b/Admin/isatest/settings/mac-poly-M8 Wed Jul 22 11:23:09 2009 +0200
@@ -25,4 +25,4 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -M 8"
-HOL_USEDIR_OPTIONS="-p 2 -q 1"
+HOL_USEDIR_OPTIONS="-p 2 -q 0"
--- a/NEWS Wed Jul 22 10:49:26 2009 +0200
+++ b/NEWS Wed Jul 22 11:23:09 2009 +0200
@@ -123,6 +123,11 @@
cominators for "args". INCOMPATIBILITY, need to use simplified
Attrib/Method.setup introduced in Isabelle2009.
+* Display.pretty_thm now requires a proper context (cf. former
+ProofContext.pretty_thm). May fall back on Display.pretty_thm_global
+or even Display.pretty_thm_without_context as last resort.
+INCOMPATIBILITY.
+
*** System ***
--- a/src/FOLP/classical.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/FOLP/classical.ML Wed Jul 22 11:23:09 2009 +0200
@@ -124,11 +124,11 @@
val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};
fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
- (writeln"Introduction rules"; Display.prths hazIs;
- writeln"Safe introduction rules"; Display.prths safeIs;
- writeln"Elimination rules"; Display.prths hazEs;
- writeln"Safe elimination rules"; Display.prths safeEs;
- ());
+ writeln (cat_lines
+ (["Introduction rules"] @ map Display.string_of_thm_without_context hazIs @
+ ["Safe introduction rules"] @ map Display.string_of_thm_without_context safeIs @
+ ["Elimination rules"] @ map Display.string_of_thm_without_context hazEs @
+ ["Safe elimination rules"] @ map Display.string_of_thm_without_context safeEs));
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
--- a/src/FOLP/ex/Prolog.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/FOLP/ex/Prolog.ML Wed Jul 22 11:23:09 2009 +0200
@@ -13,7 +13,7 @@
by (resolve_tac [appNil,appCons] 1);
by (resolve_tac [appNil,appCons] 1);
by (resolve_tac [appNil,appCons] 1);
-prth (result());
+result();
Goal "app(?x, c:d:Nil, a:b:c:d:Nil)";
by (REPEAT (resolve_tac [appNil,appCons] 1));
--- a/src/FOLP/simp.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/FOLP/simp.ML Wed Jul 22 11:23:09 2009 +0200
@@ -113,7 +113,7 @@
let fun norm thm =
case lhs_of(concl_of thm) of
Const(n,_)$_ => n
- | _ => (Display.prths normE_thms; error"No constant in lhs of a norm_thm")
+ | _ => error "No constant in lhs of a norm_thm"
in map norm normE_thms end;
fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of
@@ -122,7 +122,7 @@
val refl_tac = resolve_tac refl_thms;
fun find_res thms thm =
- let fun find [] = (Display.prths thms; error"Check Simp_Data")
+ let fun find [] = error "Check Simp_Data"
| find(th::thms) = thm RS th handle THM _ => find thms
in find thms end;
@@ -249,8 +249,8 @@
fun insert_thm_warn th net =
Net.insert_term Thm.eq_thm_prop (concl_of th, th) net
handle Net.INSERT =>
- (writeln"\nDuplicate rewrite or congruence rule:"; Display.print_thm th;
- net);
+ (writeln ("Duplicate rewrite or congruence rule:\n" ^
+ Display.string_of_thm_without_context th); net);
val insert_thms = fold_rev insert_thm_warn;
@@ -275,8 +275,8 @@
fun delete_thm_warn th net =
Net.delete_term Thm.eq_thm_prop (concl_of th, th) net
handle Net.DELETE =>
- (writeln"\nNo such rewrite or congruence rule:"; Display.print_thm th;
- net);
+ (writeln ("No such rewrite or congruence rule:\n" ^
+ Display.string_of_thm_without_context th); net);
val delete_thms = fold_rev delete_thm_warn;
@@ -290,9 +290,9 @@
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
let fun find((p as (th,ths))::ps',ps) =
if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
- | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
- Display.print_thm thm;
- ([],simps'))
+ | find([],simps') =
+ (writeln ("No such rewrite or congruence rule:\n" ^
+ Display.string_of_thm_without_context thm); ([], simps'))
val (thms,simps') = find(simps,[])
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
simps = simps', simp_net = delete_thms thms simp_net }
@@ -311,8 +311,9 @@
fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps);
fun print_ss(SS{congs,simps,...}) =
- (writeln"Congruences:"; Display.prths congs;
- writeln"Rewrite Rules:"; Display.prths (map #1 simps); ());
+ writeln (cat_lines
+ (["Congruences:"] @ map Display.string_of_thm_without_context congs @
+ ["Rewrite Rules:"] @ map (Display.string_of_thm_without_context o #1) simps));
(* Rewriting with conditionals *)
@@ -435,7 +436,8 @@
val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
val anet' = List.foldr lhs_insert_thm anet rwrls
in if !tracing andalso not(null new_rws)
- then (writeln"Adding rewrites:"; Display.prths new_rws; ())
+ then writeln (cat_lines
+ ("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws))
else ();
(ss,thm,anet',anet::ats,cs)
end;
--- a/src/HOL/Import/import.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Import/import.ML Wed Jul 22 11:23:09 2009 +0200
@@ -44,9 +44,9 @@
val thm = equal_elim rew thm
val prew = ProofKernel.rewrite_hol4_term prem thy
val prem' = #2 (Logic.dest_equals (prop_of prew))
- val _ = message ("Import proved " ^ Display.string_of_thm thm)
+ val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)
val thm = ProofKernel.disambiguate_frees thm
- val _ = message ("Disambiguate: " ^ Display.string_of_thm thm)
+ val _ = message ("Disambiguate: " ^ Display.string_of_thm ctxt thm)
in
case Shuffler.set_prop thy prem' [("",thm)] of
SOME (_,thm) =>
--- a/src/HOL/Import/proof_kernel.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Wed Jul 22 11:23:09 2009 +0200
@@ -243,7 +243,7 @@
val smart_string_of_thm = smart_string_of_cterm o cprop_of
-fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th)
+fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th)
fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ());
fun pth (HOLThm(ren,thm)) =
--- a/src/HOL/Import/shuffler.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Import/shuffler.ML Wed Jul 22 11:23:09 2009 +0200
@@ -40,7 +40,7 @@
case e of
THM (msg,i,thms) =>
(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
- List.app Display.print_thm thms)
+ List.app (writeln o Display.string_of_thm_global sign) thms)
| THEORY (msg,thys) =>
(writeln ("Exception THEORY raised:\n" ^ msg);
List.app (writeln o Context.str_of_thy) thys)
@@ -56,7 +56,7 @@
(*Prints an exception, then fails*)
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
-val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
+val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
fun mk_meta_eq th =
@@ -84,7 +84,7 @@
fun print_shuffles thy =
Pretty.writeln (Pretty.big_list "Shuffle theorems:"
- (map Display.pretty_thm (ShuffleData.get thy)))
+ (map (Display.pretty_thm_global thy) (ShuffleData.get thy)))
val weaken =
let
--- a/src/HOL/Nominal/nominal_thmdecls.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Wed Jul 22 11:23:09 2009 +0200
@@ -156,7 +156,7 @@
fold (fn thm => Data.map (flag thm)) thms_to_be_added context
end
handle EQVT_FORM s =>
- error (Display.string_of_thm orig_thm ^
+ error (Display.string_of_thm (Context.proof_of context) orig_thm ^
" does not comply with the form of an equivariance lemma (" ^ s ^").")
--- a/src/HOL/Tools/Function/lexicographic_order.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Wed Jul 22 11:23:09 2009 +0200
@@ -140,7 +140,7 @@
fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
fun pr_goals ctxt st =
- Display.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
+ Display_Goal.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
|> Pretty.chunks
|> Pretty.string_of
--- a/src/HOL/Tools/TFL/casesplit.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Wed Jul 22 11:23:09 2009 +0200
@@ -269,9 +269,9 @@
fun split th =
(case find_thms_split splitths 1 th of
NONE =>
- (writeln "th:";
- Display.print_thm th; writeln "split ths:";
- Display.print_thms splitths; writeln "\n--";
+ (writeln (cat_lines
+ (["th:", Display.string_of_thm_without_context th, "split ths:"] @
+ map Display.string_of_thm_without_context splitths @ ["\n--"]));
error "splitto: cannot find variable to split on")
| SOME v =>
let
--- a/src/HOL/Tools/TFL/rules.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Wed Jul 22 11:23:09 2009 +0200
@@ -552,7 +552,7 @@
fun say s = if !tracing then writeln s else ();
fun print_thms s L =
- say (cat_lines (s :: map Display.string_of_thm L));
+ say (cat_lines (s :: map Display.string_of_thm_without_context L));
fun print_cterms s L =
say (cat_lines (s :: map Display.string_of_cterm L));
@@ -677,7 +677,7 @@
val cntxt = Simplifier.prems_of_ss ss
val dummy = print_thms "cntxt:" cntxt
val dummy = say "cong rule:"
- val dummy = say (Display.string_of_thm thm)
+ val dummy = say (Display.string_of_thm_without_context thm)
val dummy = thm_ref := (thm :: !thm_ref)
val dummy = ss_ref := (ss :: !ss_ref)
(* Unquantified eliminate *)
--- a/src/HOL/Tools/TFL/tfl.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Jul 22 11:23:09 2009 +0200
@@ -529,9 +529,8 @@
val f = #lhs(S.dest_eq proto_def)
val (extractants,TCl) = ListPair.unzip extracta
val dummy = if !trace
- then (writeln "Extractants = ";
- Display.prths extractants;
- ())
+ then writeln (cat_lines ("Extractants =" ::
+ map (Display.string_of_thm_global thy) extractants))
else ()
val TCs = List.foldr (gen_union (op aconv)) [] TCl
val full_rqt = WFR::TCs
@@ -551,8 +550,9 @@
|> PureThy.add_defs false
[Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
val def = Thm.freezeT def0;
- val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)
- else ()
+ val dummy =
+ if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
+ else ()
(* val fconst = #lhs(S.dest_eq(concl def)) *)
val tych = Thry.typecheck theory
val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
@@ -560,7 +560,7 @@
val baz = R.DISCH_ALL
(fold_rev R.DISCH full_rqt_prop
(R.LIST_CONJ extractants))
- val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm baz)
+ val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm_global theory baz)
else ()
val f_free = Free (fid, fastype_of f) (*'cos f is a Const*)
val SV' = map tych SV;
@@ -909,7 +909,7 @@
fun trace_thms s L =
- if !trace then writeln (cat_lines (s :: map Display.string_of_thm L))
+ if !trace then writeln (cat_lines (s :: map Display.string_of_thm_without_context L))
else ();
fun trace_cterms s L =
--- a/src/HOL/Tools/atp_minimal.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/atp_minimal.ML Wed Jul 22 11:23:09 2009 +0200
@@ -125,7 +125,8 @@
println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: "
^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds")
val _ = debug_fn (fn () => app (fn (n, tl) =>
- (debug n; app (fn t => debug (" " ^ Display.string_of_thm t)) tl)) name_thms_pairs)
+ (debug n; app (fn t =>
+ debug (" " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs)
val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
fun test_thms filtered thms =
case test_thms_fun filtered thms of (Success _, _) => true | _ => false
--- a/src/HOL/Tools/atp_wrapper.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML Wed Jul 22 11:23:09 2009 +0200
@@ -62,7 +62,7 @@
val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
handle THM ("assume: variables", _, _) =>
error "Sledgehammer: Goal contains type variables (TVars)"
- val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
+ val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
val the_filtered_clauses =
case filtered_clauses of
NONE => relevance_filter goal goal_cls
--- a/src/HOL/Tools/choice_specification.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/choice_specification.ML Wed Jul 22 11:23:09 2009 +0200
@@ -183,7 +183,7 @@
fun add_final (arg as (thy, thm)) =
if name = ""
then arg |> Library.swap
- else (writeln (" " ^ name ^ ": " ^ (Display.string_of_thm thm));
+ else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
PureThy.store_thm (Binding.name name, thm) thy)
in
args |> apsnd (remove_alls frees)
--- a/src/HOL/Tools/inductive.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Jul 22 11:23:09 2009 +0200
@@ -140,7 +140,7 @@
val space = Consts.space_of (ProofContext.consts_of ctxt);
in
[Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
- Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)]
+ Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
|> Pretty.chunks |> Pretty.writeln
end;
@@ -179,7 +179,8 @@
[dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac [le_funI, le_boolI'])) thm))]
| _ => [thm]
- end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm thm);
+ end handle THM _ =>
+ error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono);
val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono);
--- a/src/HOL/Tools/inductive_codegen.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Wed Jul 22 11:23:09 2009 +0200
@@ -39,7 +39,7 @@
fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
- Display.string_of_thm thm);
+ Display.string_of_thm_without_context thm);
fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
--- a/src/HOL/Tools/inductive_realizer.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Jul 22 11:23:09 2009 +0200
@@ -19,7 +19,7 @@
(case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
[Thm.proof_of thm] [] of
[name] => name
- | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
+ | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
--- a/src/HOL/Tools/lin_arith.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML Wed Jul 22 11:23:09 2009 +0200
@@ -286,7 +286,7 @@
(* checks if splitting with 'thm' is implemented *)
-fun is_split_thm (thm : thm) : bool =
+fun is_split_thm thm =
case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (
(* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
case head_of lhs of
@@ -298,10 +298,10 @@
"Divides.div_class.mod",
"Divides.div_class.div"] a
| _ => (warning ("Lin. Arith.: wrong format for split rule " ^
- Display.string_of_thm thm);
+ Display.string_of_thm_without_context thm);
false))
| _ => (warning ("Lin. Arith.: wrong format for split rule " ^
- Display.string_of_thm thm);
+ Display.string_of_thm_without_context thm);
false);
(* substitute new for occurrences of old in a term, incrementing bound *)
--- a/src/HOL/Tools/meson.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/meson.ML Wed Jul 22 11:23:09 2009 +0200
@@ -127,10 +127,10 @@
fun forward_res nf st =
let fun forward_tacf [prem] = rtac (nf prem) 1
| forward_tacf prems =
- error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
- Display.string_of_thm st ^
- "\nPremises:\n" ^
- ML_Syntax.print_list Display.string_of_thm prems)
+ error (cat_lines
+ ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
+ Display.string_of_thm_without_context st ::
+ "Premises:" :: map Display.string_of_thm_without_context prems))
in
case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
of SOME(th,_) => th
@@ -342,7 +342,7 @@
and cnf_nil th = cnf_aux (th,[])
val cls =
if too_many_clauses (SOME ctxt) (concl_of th)
- then (warning ("cnf is ignoring: " ^ Display.string_of_thm th); ths)
+ then (warning ("cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
else cnf_aux (th,ths)
in (cls, !ctxtr) end;
@@ -545,7 +545,7 @@
| skolemize_nnf_list (th::ths) =
skolemize th :: skolemize_nnf_list ths
handle THM _ => (*RS can fail if Unify.search_bound is too small*)
- (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
+ (warning ("Failed to Skolemize " ^ Display.string_of_thm_without_context th);
skolemize_nnf_list ths);
fun add_clauses (th,cls) =
@@ -628,19 +628,17 @@
ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
fun iter_deepen_meson_tac ths = MESON make_clauses
- (fn cls =>
- case (gocls (cls@ths)) of
- [] => no_tac (*no goal clauses*)
- | goes =>
- let val horns = make_horns (cls@ths)
- val _ =
- Output.debug (fn () => ("meson method called:\n" ^
- ML_Syntax.print_list Display.string_of_thm (cls@ths) ^
- "\nclauses:\n" ^
- ML_Syntax.print_list Display.string_of_thm horns))
- in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
- end
- );
+ (fn cls =>
+ (case (gocls (cls @ ths)) of
+ [] => no_tac (*no goal clauses*)
+ | goes =>
+ let
+ val horns = make_horns (cls @ ths)
+ val _ = Output.debug (fn () =>
+ cat_lines ("meson method called:" ::
+ map Display.string_of_thm_without_context (cls @ ths) @
+ ["clauses:"] @ map Display.string_of_thm_without_context horns))
+ in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end));
fun meson_claset_tac ths cs =
SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
--- a/src/HOL/Tools/metis_tools.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Wed Jul 22 11:23:09 2009 +0200
@@ -270,7 +270,7 @@
fun print_thpair (fth,th) =
(Output.debug (fn () => "=============================================");
Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth);
- Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm th));
+ Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
fun lookth thpairs (fth : Metis.Thm.thm) =
valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
@@ -310,7 +310,7 @@
in SOME (cterm_of thy (Var v), t) end
handle Option =>
(Output.debug (fn() => "List.find failed for the variable " ^ x ^
- " in " ^ Display.string_of_thm i_th);
+ " in " ^ Display.string_of_thm ctxt i_th);
NONE)
fun remove_typeinst (a, t) =
case Recon.strip_prefix ResClause.schematic_var_prefix a of
@@ -318,7 +318,7 @@
| NONE => case Recon.strip_prefix ResClause.tvar_prefix a of
SOME _ => NONE (*type instantiations are forbidden!*)
| NONE => SOME (a,t) (*internal Metis var?*)
- val _ = Output.debug (fn () => " isa th: " ^ Display.string_of_thm i_th)
+ val _ = Output.debug (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst)
val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs)
val tms = infer_types ctxt rawtms;
@@ -350,8 +350,8 @@
let
val thy = ProofContext.theory_of ctxt
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
- val _ = Output.debug (fn () => " isa th1 (pos): " ^ Display.string_of_thm i_th1)
- val _ = Output.debug (fn () => " isa th2 (neg): " ^ Display.string_of_thm i_th2)
+ val _ = Output.debug (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
+ val _ = Output.debug (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
in
if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
else if is_TrueI i_th2 then i_th1
@@ -428,7 +428,7 @@
val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
- val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm subst')
+ val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
val eq_terms = map (pairself (cterm_of thy))
(ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
in cterm_instantiate eq_terms subst' end;
@@ -456,7 +456,7 @@
val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
val th = Meson.flexflex_first_order (step ctxt isFO thpairs (fol_th, inf))
- val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm th)
+ val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = Output.debug (fn () => "=============================================")
val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
in
@@ -576,9 +576,9 @@
val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
val ths = List.concat (map #2 th_cls_pairs)
val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
- val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) cls
+ val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) cls
val _ = Output.debug (fn () => "THEOREM CLAUSES")
- val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) ths
+ val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) ths
val {isFO,axioms,tfrees} = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (Output.debug (fn () => "TFREE CLAUSES");
@@ -604,14 +604,14 @@
val result = translate isFO ctxt' axioms proof
and used = List.mapPartial (used_axioms axioms) proof
val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
- val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) used
+ val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) used
val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
in
if null unused then ()
else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
case result of
(_,ith)::_ =>
- (Output.debug (fn () => "success: " ^ Display.string_of_thm ith);
+ (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith);
[ith])
| _ => (Output.debug (fn () => "Metis: no result");
[])
@@ -623,7 +623,7 @@
fun metis_general_tac mode ctxt ths i st0 =
let val _ = Output.debug (fn () =>
- "Metis called with theorems " ^ cat_lines (map Display.string_of_thm ths))
+ "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
then (warning "Proof state contains the empty sort"; Seq.empty)
--- a/src/HOL/Tools/recdef.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/recdef.ML Wed Jul 22 11:23:09 2009 +0200
@@ -48,9 +48,9 @@
fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
fun pretty_hints ({simps, congs, wfs}: hints) =
- [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm simps),
- Pretty.big_list "recdef cong hints:" (map Display.pretty_thm (map snd congs)),
- Pretty.big_list "recdef wf hints:" (map Display.pretty_thm wfs)];
+ [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm_without_context simps),
+ Pretty.big_list "recdef cong hints:" (map Display.pretty_thm_without_context (map snd congs)),
+ Pretty.big_list "recdef wf hints:" (map Display.pretty_thm_without_context wfs)];
(* congruence rules *)
--- a/src/HOL/Tools/record.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/record.ML Wed Jul 22 11:23:09 2009 +0200
@@ -105,7 +105,7 @@
(* messages *)
fun trace_thm str thm =
- tracing (str ^ (Pretty.string_of (Display.pretty_thm thm)));
+ tracing (str ^ (Pretty.string_of (Display.pretty_thm_without_context thm)));
fun trace_thms str thms =
(tracing str; map (trace_thm "") thms);
--- a/src/HOL/Tools/res_atp.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Wed Jul 22 11:23:09 2009 +0200
@@ -401,8 +401,9 @@
(List.foldl add_single_names (List.foldl add_multi_names [] mults) singles)
end;
-fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false)
- | check_named (_,th) = true;
+fun check_named ("", th) =
+ (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
+ | check_named (_, th) = true;
(* get lemmas from claset, simpset, atpset and extra supplied rules *)
fun get_clasimp_atp_lemmas ctxt =
@@ -538,7 +539,7 @@
val extra_cls = white_cls @ extra_cls
val axcls = white_cls @ axcls
val ccls = subtract_cls goal_cls extra_cls
- val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
+ val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm_global thy th)) ccls
val ccltms = map prop_of ccls
and axtms = map (prop_of o #1) extra_cls
val subs = tfree_classes_of_terms ccltms
--- a/src/HOL/Tools/res_axioms.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Wed Jul 22 11:23:09 2009 +0200
@@ -227,8 +227,9 @@
val eqth = combinators_aux (cprop_of th)
in equal_elim eqth th end
handle THM (msg,_,_) =>
- (warning ("Error in the combinator translation of " ^ Display.string_of_thm th);
- warning (" Exception message: " ^ msg);
+ (warning (cat_lines
+ ["Error in the combinator translation of " ^ Display.string_of_thm_without_context th,
+ " Exception message: " ^ msg]);
TrueI); (*A type variable of sort {} will cause make abstraction fail.*)
(*cterms are used throughout for efficiency*)
@@ -280,7 +281,7 @@
fun assert_lambda_free ths msg =
case filter (not o lambda_free o prop_of) ths of
[] => ()
- | ths' => error (msg ^ "\n" ^ cat_lines (map Display.string_of_thm ths'));
+ | ths' => error (cat_lines (msg :: map Display.string_of_thm_without_context ths'));
(*** Blacklisting (duplicated in ResAtp?) ***)
@@ -336,7 +337,7 @@
fun name_or_string th =
if Thm.has_name_hint th then Thm.get_name_hint th
- else Display.string_of_thm th;
+ else Display.string_of_thm_without_context th;
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
fun skolem_thm (s, th) =
--- a/src/HOL/Tools/res_reconstruct.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Wed Jul 22 11:23:09 2009 +0200
@@ -31,7 +31,7 @@
fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
else ();
-val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
+fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
(*For generating structured proofs: keep every nth proof line*)
val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1;
@@ -445,8 +445,9 @@
val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
val ccls = map forall_intr_vars ccls
- val _ = if !Output.debugging then app (fn th => trace ("\nccl: " ^ string_of_thm th)) ccls
- else ()
+ val _ =
+ if !Output.debugging then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
+ else ()
val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
val _ = trace "\ndecode_tstp_file: finishing\n"
in
--- a/src/HOL/Tools/sat_funcs.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Wed Jul 22 11:23:09 2009 +0200
@@ -119,7 +119,7 @@
(* (Thm.thm * (int * Thm.cterm) list) list -> Thm.thm * (int * Thm.cterm) list *)
fun resolve_raw_clauses [] =
- raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
+ raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
| resolve_raw_clauses (c::cs) =
let
(* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
@@ -134,9 +134,9 @@
(* find out which two hyps are used in the resolution *)
(* (int * Thm.cterm) list * (int * Thm.cterm) list -> (int * Thm.cterm) list -> bool * Thm.cterm * Thm.cterm * (int * Thm.cterm) list *)
fun find_res_hyps ([], _) _ =
- raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
+ raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
| find_res_hyps (_, []) _ =
- raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
+ raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
| find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
(case (lit_ord o pairself fst) (h1, h2) of
LESS => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
@@ -154,9 +154,12 @@
(* Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list *)
fun resolution (c1, hyps1) (c2, hyps2) =
let
- val _ = if !trace_sat then
- tracing ("Resolving clause: " ^ Display.string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
- ^ ")\nwith clause: " ^ Display.string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
+ val _ =
+ if ! trace_sat then
+ tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
+ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
+ ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
+ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
else ()
(* the two literals used for resolution *)
@@ -172,8 +175,9 @@
Thm.instantiate ([], [(cP, cLit)]) resolution_thm
end
- val _ = if !trace_sat then
- tracing ("Resolution theorem: " ^ Display.string_of_thm res_thm)
+ val _ =
+ if !trace_sat then
+ tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm)
else ()
(* Gamma1, Gamma2 |- False *)
@@ -181,8 +185,11 @@
(Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
(if hyp1_is_neg then c1' else c2')
- val _ = if !trace_sat then
- tracing ("Resulting clause: " ^ Display.string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
+ val _ =
+ if !trace_sat then
+ tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
+ " (hyps: " ^ ML_Syntax.print_list
+ (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
else ()
val _ = inc counter
in
--- a/src/HOL/ex/ROOT.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/ex/ROOT.ML Wed Jul 22 11:23:09 2009 +0200
@@ -83,6 +83,7 @@
(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
(* installed: *)
try use_thy "SAT_Examples";
+Future.shutdown ();
(* requires zChaff (or some other reasonably fast SAT solver) to be *)
(* installed: *)
--- a/src/HOL/ex/predicate_compile.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Wed Jul 22 11:23:09 2009 +0200
@@ -236,11 +236,11 @@
val _ = writeln ("predicate: " ^ pred)
val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred))
val _ = writeln ("introrules: ")
- val _ = fold (fn thm => fn u => writeln (Display.string_of_thm thm))
+ val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm))
(rev (intros_of thy pred)) ()
in
if (has_elim thy pred) then
- writeln ("elimrule: " ^ Display.string_of_thm (the_elim_of thy pred))
+ writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred))
else
writeln ("no elimrule defined")
end
--- a/src/Provers/Arith/fast_lin_arith.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Jul 22 11:23:09 2009 +0200
@@ -417,8 +417,8 @@
(* Translate back a proof. *)
(* ------------------------------------------------------------------------- *)
-fun trace_thm msg th =
- (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
+fun trace_thm ctxt msg th =
+ (if !trace then (tracing msg; tracing (Display.string_of_thm ctxt th)) else (); th);
fun trace_term ctxt msg t =
(if !trace then tracing (cat_lines [msg, Syntax.string_of_term ctxt t]) else (); t)
@@ -472,7 +472,7 @@
NONE =>
(the (try_add ([thm2] RL inj_thms) thm1)
handle Option =>
- (trace_thm "" thm1; trace_thm "" thm2;
+ (trace_thm ctxt "" thm1; trace_thm ctxt "" thm2;
sys_error "Linear arithmetic: failed to add thms"))
| SOME thm => thm)
| SOME thm => thm);
@@ -511,24 +511,25 @@
else mult n thm;
fun simp thm =
- let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
+ let val thm' = trace_thm ctxt "Simplified:" (full_simplify simpset' thm)
in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end;
- fun mk (Asm i) = trace_thm ("Asm " ^ string_of_int i) (nth asms i)
- | mk (Nat i) = trace_thm ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i))
- | mk (LessD j) = trace_thm "L" (hd ([mk j] RL lessD))
- | mk (NotLeD j) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
- | mk (NotLeDD j) = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
- | mk (NotLessD j) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
- | mk (Added (j1, j2)) = simp (trace_thm "+" (add_thms (mk j1) (mk j2)))
- | mk (Multiplied (n, j)) = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (mult_thm (n, mk j)))
+ fun mk (Asm i) = trace_thm ctxt ("Asm " ^ string_of_int i) (nth asms i)
+ | mk (Nat i) = trace_thm ctxt ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i))
+ | mk (LessD j) = trace_thm ctxt "L" (hd ([mk j] RL lessD))
+ | mk (NotLeD j) = trace_thm ctxt "NLe" (mk j RS LA_Logic.not_leD)
+ | mk (NotLeDD j) = trace_thm ctxt "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
+ | mk (NotLessD j) = trace_thm ctxt "NL" (mk j RS LA_Logic.not_lessD)
+ | mk (Added (j1, j2)) = simp (trace_thm ctxt "+" (add_thms (mk j1) (mk j2)))
+ | mk (Multiplied (n, j)) =
+ (trace_msg ("*" ^ string_of_int n); trace_thm ctxt "*" (mult_thm (n, mk j)))
in
let
val _ = trace_msg "mkthm";
- val thm = trace_thm "Final thm:" (mk just);
+ val thm = trace_thm ctxt "Final thm:" (mk just);
val fls = simplify simpset' thm;
- val _ = trace_thm "After simplification:" fls;
+ val _ = trace_thm ctxt "After simplification:" fls;
val _ =
if LA_Logic.is_False fls then ()
else
@@ -536,15 +537,15 @@
if count > warning_count_max then ()
else
(tracing (cat_lines
- (["Assumptions:"] @ map Display.string_of_thm asms @ [""] @
- ["Proved:", Display.string_of_thm fls, ""] @
+ (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
+ ["Proved:", Display.string_of_thm ctxt fls, ""] @
(if count <> warning_count_max then []
else ["\n(Reached maximal message count -- disabling future warnings)"])));
warning "Linear arithmetic should have refuted the assumptions.\n\
\Please inform Tobias Nipkow (nipkow@in.tum.de).")
end;
in fls end
- handle FalseE thm => trace_thm "False reached early:" thm
+ handle FalseE thm => trace_thm ctxt "False reached early:" thm
end;
end;
@@ -775,8 +776,9 @@
fn state =>
let
val ctxt = Simplifier.the_context ss;
- val _ = trace_thm ("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^
- string_of_int (length justs) ^ " justification(s)):") state
+ val _ = trace_thm ctxt
+ ("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^
+ string_of_int (length justs) ^ " justification(s)):") state
val {neqE, ...} = get_data ctxt;
fun just1 j =
(* eliminate inequalities *)
@@ -784,7 +786,7 @@
REPEAT_DETERM (eresolve_tac neqE i)
else
all_tac) THEN
- PRIMITIVE (trace_thm "State after neqE:") THEN
+ PRIMITIVE (trace_thm ctxt "State after neqE:") THEN
(* use theorems generated from the actual justifications *)
METAHYPS (fn asms => rtac (mkthm ss asms j) 1) i
in
@@ -792,7 +794,7 @@
DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
(* user-defined preprocessing of the subgoal *)
DETERM (LA_Data.pre_tac ctxt i) THEN
- PRIMITIVE (trace_thm "State after pre_tac:") THEN
+ PRIMITIVE (trace_thm ctxt "State after pre_tac:") THEN
(* prove every resulting subgoal, using its justification *)
EVERY (map just1 justs)
end state;
@@ -881,7 +883,7 @@
val (Falsethm, _) = fwdproof ss tree js
val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
val concl = implies_intr cnTconcl Falsethm COMP contr
- in SOME (trace_thm "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end
+ in SOME (trace_thm ctxt "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end
(*in case concl contains ?-var, which makes assume fail:*) (* FIXME Variable.import_terms *)
handle THM _ => NONE;
--- a/src/Provers/blast.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Provers/blast.ML Wed Jul 22 11:23:09 2009 +0200
@@ -492,7 +492,9 @@
end;
-fun TRACE rl tac st i = if !trace then (Display.prth rl; tac st i) else tac st i;
+fun TRACE rl tac st i =
+ if !trace then (writeln (Display.string_of_thm_without_context rl); tac st i)
+ else tac st i;
(*Resolution/matching tactics: if upd then the proof state may be updated.
Matching makes the tactics more deterministic in the presence of Vars.*)
@@ -509,14 +511,16 @@
THEN
rot_subgoals_tac (rot, #2 trl) i
in Option.SOME (trl, tac) end
- handle ElimBadPrem => (*reject: prems don't preserve conclusion*)
- (warning("Ignoring weak elimination rule\n" ^ Display.string_of_thm rl);
- Option.NONE)
- | ElimBadConcl => (*ignore: conclusion is not just a variable*)
- (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^
- "conclusion should be a variable\n" ^ Display.string_of_thm rl))
- else ();
- Option.NONE);
+ handle
+ ElimBadPrem => (*reject: prems don't preserve conclusion*)
+ (warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm_global thy rl);
+ Option.NONE)
+ | ElimBadConcl => (*ignore: conclusion is not just a variable*)
+ (if !trace then
+ (warning ("Ignoring ill-formed elimination rule:\n" ^
+ "conclusion should be a variable\n" ^ Display.string_of_thm_global thy rl))
+ else ();
+ Option.NONE);
(*** Conversion of Introduction Rules ***)
--- a/src/Provers/classical.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Provers/classical.ML Wed Jul 22 11:23:09 2009 +0200
@@ -256,7 +256,7 @@
xtra_netpair = empty_netpair};
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
- let val pretty_thms = map Display.pretty_thm in
+ let val pretty_thms = map Display.pretty_thm_without_context in
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
@@ -313,14 +313,18 @@
(*Warn if the rule is already present ELSEWHERE in the claset. The addition
is still allowed.*)
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
- if mem_thm safeIs th then
- warning ("Rule already declared as safe introduction (intro!)\n" ^ Display.string_of_thm th)
+ if mem_thm safeIs th then
+ warning ("Rule already declared as safe introduction (intro!)\n" ^
+ Display.string_of_thm_without_context th)
else if mem_thm safeEs th then
- warning ("Rule already declared as safe elimination (elim!)\n" ^ Display.string_of_thm th)
+ warning ("Rule already declared as safe elimination (elim!)\n" ^
+ Display.string_of_thm_without_context th)
else if mem_thm hazIs th then
- warning ("Rule already declared as introduction (intro)\n" ^ Display.string_of_thm th)
+ warning ("Rule already declared as introduction (intro)\n" ^
+ Display.string_of_thm_without_context th)
else if mem_thm hazEs th then
- warning ("Rule already declared as elimination (elim)\n" ^ Display.string_of_thm th)
+ warning ("Rule already declared as elimination (elim)\n" ^
+ Display.string_of_thm_without_context th)
else ();
@@ -330,8 +334,8 @@
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm safeIs th then
- (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ Display.string_of_thm th);
- cs)
+ (warning ("Ignoring duplicate safe introduction (intro!)\n" ^
+ Display.string_of_thm_without_context th); cs)
else
let val th' = flat_rule th
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
@@ -356,10 +360,10 @@
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm safeEs th then
- (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ Display.string_of_thm th);
- cs)
+ (warning ("Ignoring duplicate safe elimination (elim!)\n" ^
+ Display.string_of_thm_without_context th); cs)
else if has_fewer_prems 1 th then
- error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
+ error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
else
let
val th' = classical_rule (flat_rule th)
@@ -386,7 +390,7 @@
fun make_elim th =
if has_fewer_prems 1 th then
- error("Ill-formed destruction rule\n" ^ Display.string_of_thm th)
+ error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
else Tactic.make_elim th;
fun cs addSDs ths = cs addSEs (map make_elim ths);
@@ -398,8 +402,8 @@
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm hazIs th then
- (warning ("Ignoring duplicate introduction (intro)\n" ^ Display.string_of_thm th);
- cs)
+ (warning ("Ignoring duplicate introduction (intro)\n" ^
+ Display.string_of_thm_without_context th); cs)
else
let val th' = flat_rule th
val nI = length hazIs + 1
@@ -418,16 +422,16 @@
xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
end
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
- error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
+ error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
fun addE w th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm hazEs th then
- (warning ("Ignoring duplicate elimination (elim)\n" ^ Display.string_of_thm th);
- cs)
+ (warning ("Ignoring duplicate elimination (elim)\n" ^
+ Display.string_of_thm_without_context th); cs)
else if has_fewer_prems 1 th then
- error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
+ error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
else
let
val th' = classical_rule (flat_rule th)
@@ -519,7 +523,7 @@
end
else cs
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
- error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
+ error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
fun delE th
@@ -548,7 +552,7 @@
mem_thm hazIs th orelse mem_thm hazEs th orelse
mem_thm safeEs th' orelse mem_thm hazEs th'
then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
- else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm th); cs)
+ else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs)
end;
fun cs delrules ths = fold delrule ths cs;
--- a/src/Pure/Concurrent/future.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Wed Jul 22 11:23:09 2009 +0200
@@ -30,6 +30,7 @@
type task = Task_Queue.task
type group = Task_Queue.group
val is_worker: unit -> bool
+ val worker_group: unit -> Task_Queue.group option
type 'a future
val task_of: 'a future -> task
val group_of: 'a future -> group
@@ -40,7 +41,6 @@
val fork_group: group -> (unit -> 'a) -> 'a future
val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
val fork_pri: int -> (unit -> 'a) -> 'a future
- val fork_local: int -> (unit -> 'a) -> 'a future
val join_results: 'a future list -> 'a Exn.result list
val join_result: 'a future -> 'a Exn.result
val join: 'a future -> 'a
@@ -76,6 +76,7 @@
end;
val is_worker = is_some o thread_data;
+val worker_group = Option.map #3 o thread_data;
(* datatype future *)
@@ -93,7 +94,7 @@
fun value x = Future
{task = Task_Queue.new_task 0,
- group = Task_Queue.new_group (),
+ group = Task_Queue.new_group NONE,
result = ref (SOME (Exn.Result x))};
@@ -134,18 +135,43 @@
(* worker activity *)
-fun trace_active () =
+fun count_active ws =
+ fold (fn (_, active) => fn i => if active then i + 1 else i) ws 0;
+
+fun trace_active () = Multithreading.tracing 1 (fn () =>
let
val ws = ! workers;
val m = string_of_int (length ws);
- val n = string_of_int (length (filter #2 ws));
- in Multithreading.tracing 2 (fn () => "SCHEDULE: " ^ m ^ " workers, " ^ n ^ " active") end;
+ val n = string_of_int (count_active ws);
+ in "SCHEDULE: " ^ m ^ " workers, " ^ n ^ " active" end);
fun change_active active = (*requires SYNCHRONIZED*)
change workers (AList.update Thread.equal (Thread.self (), active));
+fun overloaded () =
+ count_active (! workers) > Multithreading.max_threads_value ();
-(* execute jobs *)
+
+(* execute future jobs *)
+
+fun future_job group (e: unit -> 'a) =
+ let
+ val result = ref (NONE: 'a Exn.result option);
+ fun job ok =
+ let
+ val res =
+ if ok then
+ Exn.capture
+ (Multithreading.with_attributes Multithreading.restricted_interrupts
+ (fn _ => fn () => e ())) ()
+ else Exn.Exn Exn.Interrupt;
+ val _ = result := SOME res;
+ in
+ (case res of
+ Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
+ | Exn.Result _ => true)
+ end;
+ in (result, job) end;
fun do_cancel group = (*requires SYNCHRONIZED*)
change canceled (insert Task_Queue.eq_group group);
@@ -153,7 +179,7 @@
fun execute name (task, group, jobs) =
let
val _ = trace_active ();
- val valid = Task_Queue.is_valid group;
+ val valid = not (Task_Queue.is_canceled group);
val ok = setmp_thread_data (name, task, group) (fn () =>
fold (fn job => fn ok => job valid andalso ok) jobs true) ();
val _ = SYNCHRONIZED "execute" (fn () =>
@@ -176,13 +202,14 @@
change workers (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
notify_all ();
NONE)
+ else if overloaded () then (worker_wait (); worker_next ())
else
(case change_result queue Task_Queue.dequeue of
NONE => (worker_wait (); worker_next ())
| some => some);
fun worker_loop name =
- (case SYNCHRONIZED name worker_next of
+ (case SYNCHRONIZED name (fn () => worker_next ()) of
NONE => ()
| SOME work => (execute name work; worker_loop name));
@@ -204,26 +231,31 @@
end);
(*worker threads*)
+ val ws = ! workers;
val _ =
- (case List.partition (Thread.isActive o #1) (! workers) of
- (_, []) => ()
- | (active, inactive) =>
- (workers := active; Multithreading.tracing 0 (fn () =>
- "SCHEDULE: disposed " ^ string_of_int (length inactive) ^ " dead worker threads")));
+ if forall (Thread.isActive o #1) ws then ()
+ else
+ (case List.partition (Thread.isActive o #1) ws of
+ (_, []) => ()
+ | (active, inactive) =>
+ (workers := active; Multithreading.tracing 0 (fn () =>
+ "SCHEDULE: disposed " ^ string_of_int (length inactive) ^ " dead worker threads")));
val _ = trace_active ();
val m = if ! do_shutdown then 0 else Multithreading.max_threads_value ();
- val l = length (! workers);
- val _ = excessive := l - m;
+ val mm = (m * 3) div 2;
+ val l = length ws;
+ val _ = excessive := l - mm;
val _ =
- if m > l then funpow (m - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) ()
+ if mm > l then
+ funpow (mm - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) ()
else ();
(*canceled groups*)
- val _ = change canceled (filter_out (Task_Queue.cancel (! queue)));
+ val _ = change canceled (filter_out (Task_Queue.cancel (! queue)));
(*shutdown*)
- val continue = not (! do_shutdown andalso null (! workers));
+ val continue = not (! do_shutdown andalso null ws);
val _ = if continue then () else scheduler := NONE;
val _ = notify_all ();
@@ -233,7 +265,7 @@
in continue end;
fun scheduler_loop () =
- while SYNCHRONIZED "scheduler" scheduler_next do ();
+ while SYNCHRONIZED "scheduler" (fn () => scheduler_next ()) do ();
fun scheduler_active () = (*requires SYNCHRONIZED*)
(case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
@@ -248,32 +280,16 @@
(** futures **)
-(* future job: fill result *)
-
-fun future_job group (e: unit -> 'a) =
- let
- val result = ref (NONE: 'a Exn.result option);
- val job = Multithreading.with_attributes Multithreading.restricted_interrupts
- (fn _ => fn ok =>
- let
- val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt;
- val _ = result := SOME res;
- val res_ok =
- (case res of
- Exn.Result _ => true
- | Exn.Exn Exn.Interrupt => (Task_Queue.invalidate_group group; true)
- | _ => false);
- in res_ok end);
- in (result, job) end;
-
-
(* fork *)
fun fork_future opt_group deps pri e =
let
val _ = scheduler_check "future check";
- val group = (case opt_group of SOME group => group | NONE => Task_Queue.new_group ());
+ val group =
+ (case opt_group of
+ SOME group => group
+ | NONE => Task_Queue.new_group (worker_group ()));
val (result, job) = future_job group e;
val task = SYNCHRONIZED "future" (fn () =>
change_result queue (Task_Queue.enqueue group deps pri job) before notify_all ());
@@ -283,17 +299,25 @@
fun fork_group group e = fork_future (SOME group) [] 0 e;
fun fork_deps deps e = fork_future NONE (map task_of deps) 0 e;
fun fork_pri pri e = fork_future NONE [] pri e;
-fun fork_local pri e = fork_future (Option.map #3 (thread_data ())) [] pri e;
(* join *)
local
-fun get_result x = the_default (Exn.Exn (SYS_ERROR "unfinished future")) (peek x);
+fun get_result x =
+ (case peek x of
+ NONE => Exn.Exn (SYS_ERROR "unfinished future")
+ | SOME (Exn.Exn Exn.Interrupt) =>
+ Exn.Exn (Exn.EXCEPTIONS (Exn.flatten_list (Task_Queue.group_status (group_of x))))
+ | SOME res => res);
+
+fun join_next deps = (*requires SYNCHRONIZED*)
+ if overloaded () then (worker_wait (); join_next deps)
+ else change_result queue (Task_Queue.dequeue_towards deps);
fun join_deps deps =
- (case SYNCHRONIZED "join" (fn () => change_result queue (Task_Queue.dequeue_towards deps)) of
+ (case SYNCHRONIZED "join" (fn () => join_next deps) of
NONE => ()
| SOME (work, deps') => (execute "join" work; join_deps deps'));
@@ -308,12 +332,12 @@
error "Cannot join future values within critical section";
val worker = is_worker ();
+ val _ = if worker then join_deps (map task_of xs) else ();
+
fun join_wait x =
if SYNCHRONIZED "join_wait" (fn () =>
is_finished x orelse (if worker then worker_wait () else wait (); false))
then () else join_wait x;
-
- val _ = if worker then join_deps (map task_of xs) else ();
val _ = List.app join_wait xs;
in map get_result xs end) ();
@@ -331,7 +355,7 @@
val _ = scheduler_check "map_future check";
val task = task_of x;
- val group = Task_Queue.new_group ();
+ val group = Task_Queue.new_group (SOME (group_of x));
val (result, job) = future_job group (fn () => f (join x));
val extended = SYNCHRONIZED "map_future" (fn () =>
@@ -340,7 +364,7 @@
| NONE => false));
in
if extended then Future {task = task, group = group, result = result}
- else fork_future NONE [task] (Task_Queue.pri_of_task task) (fn () => f (join x))
+ else fork_future (SOME group) [task] (Task_Queue.pri_of_task task) (fn () => f (join x))
end;
--- a/src/Pure/Concurrent/par_list.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Concurrent/par_list.ML Wed Jul 22 11:23:09 2009 +0200
@@ -28,11 +28,8 @@
fun raw_map f xs =
if Future.enabled () then
- let
- val group = Task_Queue.new_group ();
- val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
- val _ = List.app (ignore o Future.join_result) futures;
- in Future.join_results futures end
+ let val group = Task_Queue.new_group (Future.worker_group ())
+ in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
else map (Exn.capture f) xs;
fun map f xs = Exn.release_first (raw_map f xs);
--- a/src/Pure/Concurrent/task_queue.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Wed Jul 22 11:23:09 2009 +0200
@@ -13,9 +13,8 @@
type group
val group_id: group -> int
val eq_group: group * group -> bool
- val new_group: unit -> group
- val is_valid: group -> bool
- val invalidate_group: group -> unit
+ val new_group: group option -> group
+ val group_status: group -> exn list
val str_of_group: group -> string
type queue
val empty: queue
@@ -28,6 +27,8 @@
(((task * group * (bool -> bool) list) * task list) option * queue)
val interrupt: queue -> task -> unit
val interrupt_external: queue -> string -> unit
+ val is_canceled: group -> bool
+ val cancel_group: group -> exn -> unit
val cancel: queue -> group -> bool
val cancel_all: queue -> group list
val finish: task -> queue -> queue
@@ -48,20 +49,37 @@
structure Task_Graph = Graph(type key = task val ord = task_ord);
-(* groups *)
+(* nested groups *)
+
+datatype group = Group of
+ {parent: group option,
+ id: serial,
+ status: exn list ref};
-datatype group = Group of serial * bool ref;
+fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
-fun group_id (Group (gid, _)) = gid;
-fun eq_group (Group (gid1, _), Group (gid2, _)) = gid1 = gid2;
+fun new_group parent = make_group (parent, serial (), ref []);
+
+fun group_id (Group {id, ...}) = id;
+fun eq_group (group1, group2) = group_id group1 = group_id group2;
-fun new_group () = Group (serial (), ref true);
+fun group_ancestry (Group {parent, id, ...}) =
+ id :: (case parent of NONE => [] | SOME group => group_ancestry group);
+
+
+fun cancel_group (Group {status, ...}) exn = CRITICAL (fn () =>
+ (case exn of
+ Exn.Interrupt => if null (! status) then status := [exn] else ()
+ | _ => change status (cons exn)));
-fun is_valid (Group (_, ref ok)) = ok;
-fun invalidate_group (Group (_, ok)) = ok := false;
+fun group_status (Group {parent, status, ...}) = (*non-critical*)
+ ! status @ (case parent of NONE => [] | SOME group => group_status group);
-fun str_of_group (Group (i, ref ok)) =
- if ok then string_of_int i else enclose "(" ")" (string_of_int i);
+fun is_canceled (Group {parent, status, ...}) = (*non-critical*)
+ not (null (! status)) orelse (case parent of NONE => false | SOME group => is_canceled group);
+
+fun str_of_group group =
+ (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
(* jobs *)
@@ -95,7 +113,7 @@
fun is_empty (Queue {jobs, ...}) = Task_Graph.is_empty jobs;
-(* status *)
+(* queue status *)
fun status (Queue {jobs, ...}) =
let
@@ -108,14 +126,38 @@
in {ready = x, pending = y, running = z} end;
+(* cancel -- peers and sub-groups *)
+
+fun cancel (Queue {groups, jobs, ...}) group =
+ let
+ val _ = cancel_group group Exn.Interrupt;
+ val tasks = Inttab.lookup_list groups (group_id group);
+ val running =
+ fold (get_job jobs #> (fn Running t => insert Thread.equal t | _ => I)) tasks [];
+ val _ = List.app SimpleThread.interrupt running;
+ in null running end;
+
+fun cancel_all (Queue {jobs, ...}) =
+ let
+ fun cancel_job (group, job) (groups, running) =
+ (cancel_group group Exn.Interrupt;
+ (case job of Running t => (insert eq_group group groups, insert Thread.equal t running)
+ | _ => (groups, running)));
+ val (groups, running) = Task_Graph.fold (cancel_job o #1 o #2) jobs ([], []);
+ val _ = List.app SimpleThread.interrupt running;
+ in groups end;
+
+
(* enqueue *)
-fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, cache}) =
+fun enqueue group deps pri job (Queue {groups, jobs, cache}) =
let
val task = new_task pri;
- val groups' = Inttab.cons_list (gid, task) groups;
+ val groups' = groups
+ |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group);
val jobs' = jobs
- |> Task_Graph.new_node (task, (group, Job [job])) |> fold (add_job task) deps;
+ |> Task_Graph.new_node (task, (group, Job [job]))
+ |> fold (add_job task) deps;
val cache' =
(case cache of
Result last =>
@@ -159,25 +201,33 @@
fun ready task =
(case Task_Graph.get_node jobs task of
(group, Job list) =>
- if null (Task_Graph.imm_preds jobs task) then SOME (task, group, rev list)
+ if null (Task_Graph.imm_preds jobs task)
+ then SOME (task, group, rev list)
else NONE
| _ => NONE);
+
val tasks = filter (can (Task_Graph.get_node jobs)) deps;
+ fun result (res as (task, _, _)) =
+ let
+ val jobs' = set_job task (Running (Thread.self ())) jobs;
+ val cache' = Unknown;
+ in (SOME (res, tasks), make_queue groups jobs' cache') end;
in
- (case get_first ready (Task_Graph.all_preds jobs tasks) of
- NONE => (NONE, queue)
- | SOME (result as (task, _, _)) =>
- let
- val jobs' = set_job task (Running (Thread.self ())) jobs;
- val cache' = Unknown;
- in (SOME (result, tasks), make_queue groups jobs' cache') end)
+ (case get_first ready tasks of
+ SOME res => result res
+ | NONE =>
+ (case get_first ready (Task_Graph.all_preds jobs tasks) of
+ SOME res => result res
+ | NONE => (NONE, queue)))
end;
(* sporadic interrupts *)
fun interrupt (Queue {jobs, ...}) task =
- (case try (get_job jobs) task of SOME (Running thread) => SimpleThread.interrupt thread | _ => ());
+ (case try (get_job jobs) task of
+ SOME (Running thread) => SimpleThread.interrupt thread
+ | _ => ());
fun interrupt_external (queue as Queue {jobs, ...}) str =
(case Int.fromString str of
@@ -190,28 +240,11 @@
(* termination *)
-fun cancel (Queue {groups, jobs, ...}) (group as Group (gid, _)) =
- let
- val _ = invalidate_group group;
- val tasks = Inttab.lookup_list groups gid;
- val running = fold (get_job jobs #> (fn Running t => insert Thread.equal t | _ => I)) tasks [];
- val _ = List.app SimpleThread.interrupt running;
- in null running end;
-
-fun cancel_all (Queue {jobs, ...}) =
- let
- fun cancel_job (group, job) (groups, running) =
- (invalidate_group group;
- (case job of Running t => (insert eq_group group groups, insert Thread.equal t running)
- | _ => (groups, running)));
- val (groups, running) = Task_Graph.fold (cancel_job o #1 o #2) jobs ([], []);
- val _ = List.app SimpleThread.interrupt running;
- in groups end;
-
fun finish task (Queue {groups, jobs, cache}) =
let
- val Group (gid, _) = get_group jobs task;
- val groups' = Inttab.remove_list (op =) (gid, task) groups;
+ val group = get_group jobs task;
+ val groups' = groups
+ |> fold (fn gid => Inttab.remove_list (op =) (gid, task)) (group_ancestry group);
val jobs' = Task_Graph.del_node task jobs;
val cache' =
if null (Task_Graph.imm_succs jobs task) then cache
--- a/src/Pure/IsaMakefile Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/IsaMakefile Wed Jul 22 11:23:09 2009 +0200
@@ -90,13 +90,13 @@
Tools/find_theorems.ML Tools/named_thms.ML Tools/xml_syntax.ML \
assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \
consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \
- drule.ML envir.ML facts.ML goal.ML interpretation.ML item_net.ML \
- library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML \
- name.ML net.ML old_goals.ML old_term.ML pattern.ML primitive_defs.ML \
- proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML \
- simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML \
- term_ord.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML \
- unify.ML variable.ML
+ display_goal.ML drule.ML envir.ML facts.ML goal.ML interpretation.ML \
+ item_net.ML library.ML logic.ML meta_simplifier.ML more_thm.ML \
+ morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML \
+ primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML \
+ sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML \
+ term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML \
+ type_infer.ML unify.ML variable.ML
@./mk
--- a/src/Pure/Isar/args.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Isar/args.ML Wed Jul 22 11:23:09 2009 +0200
@@ -88,7 +88,7 @@
fun pretty_src ctxt src =
let
- val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
+ val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
fun prt arg =
(case T.get_value arg of
SOME (T.Text s) => Pretty.str (quote s)
--- a/src/Pure/Isar/calculation.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Isar/calculation.ML Wed Jul 22 11:23:09 2009 +0200
@@ -40,8 +40,8 @@
fun print_rules ctxt =
let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
[Pretty.big_list "transitivity rules:"
- (map (ProofContext.pretty_thm ctxt) (Item_Net.content trans)),
- Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
+ (map (Display.pretty_thm ctxt) (Item_Net.content trans)),
+ Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
|> Pretty.chunks |> Pretty.writeln
end;
--- a/src/Pure/Isar/code.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Isar/code.ML Wed Jul 22 11:23:09 2009 +0200
@@ -243,7 +243,7 @@
(*default flag, theorems with proper flag (perhaps lazy)*)
fun pretty_lthms ctxt r = case Lazy.peek r
- of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
+ of SOME thms => map (Display.pretty_thm ctxt o fst) (Exn.release thms)
| NONE => [Pretty.str "[...]"];
fun certificate thy f r =
@@ -263,7 +263,8 @@
Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
fun drop (thm', proper') = if (proper orelse not proper')
andalso matches_args (args_of thm') then
- (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true)
+ (warning ("Code generator: dropping redundant code equation\n" ^
+ Display.string_of_thm_global thy thm'); true)
else false;
in (thm, proper) :: filter_out drop thms end;
@@ -567,16 +568,16 @@
fun gen_assert_eqn thy is_constr_pat (thm, proper) =
let
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
- handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
- | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
+ handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm_global thy thm)
+ | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm_global thy thm);
fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
| Free _ => bad_thm ("Illegal free variable in equation\n"
- ^ Display.string_of_thm thm)
+ ^ Display.string_of_thm_global thy thm)
| _ => I) t [];
fun tvars_of t = fold_term_types (fn _ =>
fold_atyps (fn TVar (v, _) => insert (op =) v
| TFree _ => bad_thm
- ("Illegal free type variable in equation\n" ^ Display.string_of_thm thm))) t [];
+ ("Illegal free type variable in equation\n" ^ Display.string_of_thm_global thy thm))) t [];
val lhs_vs = vars_of lhs;
val rhs_vs = vars_of rhs;
val lhs_tvs = tvars_of lhs;
@@ -584,47 +585,48 @@
val _ = if null (subtract (op =) lhs_vs rhs_vs)
then ()
else bad_thm ("Free variables on right hand side of equation\n"
- ^ Display.string_of_thm thm);
+ ^ Display.string_of_thm_global thy thm);
val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
then ()
else bad_thm ("Free type variables on right hand side of equation\n"
- ^ Display.string_of_thm thm) val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
+ ^ Display.string_of_thm_global thy thm)
+ val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
val (c, ty) = case head
of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
- | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
+ | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm_global thy thm);
fun check _ (Abs _) = bad_thm
("Abstraction on left hand side of equation\n"
- ^ Display.string_of_thm thm)
+ ^ Display.string_of_thm_global thy thm)
| check 0 (Var _) = ()
| check _ (Var _) = bad_thm
("Variable with application on left hand side of equation\n"
- ^ Display.string_of_thm thm)
+ ^ Display.string_of_thm_global thy thm)
| check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
| check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty
then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty)
then ()
else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n"
- ^ Display.string_of_thm thm)
+ ^ Display.string_of_thm_global thy thm)
else bad_thm
("Partially applied constant " ^ quote c ^ " on left hand side of equation\n"
- ^ Display.string_of_thm thm);
+ ^ Display.string_of_thm_global thy thm);
val _ = map (check 0) args;
val _ = if not proper orelse is_linear thm then ()
else bad_thm ("Duplicate variables on left hand side of equation\n"
- ^ Display.string_of_thm thm);
+ ^ Display.string_of_thm_global thy thm);
val _ = if (is_none o AxClass.class_of_param thy) c
then ()
else bad_thm ("Polymorphic constant as head in equation\n"
- ^ Display.string_of_thm thm)
+ ^ Display.string_of_thm_global thy thm)
val _ = if not (is_constr thy c)
then ()
else bad_thm ("Constructor as head in equation\n"
- ^ Display.string_of_thm thm)
+ ^ Display.string_of_thm_global thy thm)
val ty_decl = Sign.the_const_type thy c;
val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
then () else bad_thm ("Type\n" ^ string_of_typ thy ty
^ "\nof equation\n"
- ^ Display.string_of_thm thm
+ ^ Display.string_of_thm_global thy thm
^ "\nis incompatible with declared function type\n"
^ string_of_typ thy ty_decl)
in (thm, proper) end;
@@ -657,7 +659,7 @@
let
fun cert (eqn as (thm, _)) = if c = const_eqn thy thm
then eqn else error ("Wrong head of code equation,\nexpected constant "
- ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
+ ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)
in map (cert o assert_eqn thy) eqns end;
fun common_typ_eqns thy [] = []
@@ -674,7 +676,7 @@
fun unify ty env = Sign.typ_unify thy (ty1, ty) env
handle Type.TUNIFY =>
error ("Type unificaton failed, while unifying code equations\n"
- ^ (cat_lines o map Display.string_of_thm) thms
+ ^ (cat_lines o map (Display.string_of_thm_global thy)) thms
^ "\nwith types\n"
^ (cat_lines o map (string_of_typ thy)) (ty1 :: tys));
val (env, _) = fold unify tys (Vartab.empty, maxidx)
@@ -796,17 +798,17 @@
let
val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm)
of SOME ofclass_eq => ofclass_eq
- | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
+ | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
val (T, class) = case try Logic.dest_of_class ofclass
of SOME T_class => T_class
- | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
+ | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
val tvar = case try Term.dest_TVar T
of SOME (tvar as (_, sort)) => if null (filter (can (AxClass.get_info thy)) sort)
then tvar
- else error ("Bad sort: " ^ Display.string_of_thm thm)
- | _ => error ("Bad type: " ^ Display.string_of_thm thm);
+ else error ("Bad sort: " ^ Display.string_of_thm_global thy thm)
+ | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm);
val _ = if Term.add_tvars eqn [] = [tvar] then ()
- else error ("Inconsistent type: " ^ Display.string_of_thm thm);
+ else error ("Inconsistent type: " ^ Display.string_of_thm_global thy thm);
val lhs_rhs = case try Logic.dest_equals eqn
of SOME lhs_rhs => lhs_rhs
| _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
@@ -815,7 +817,7 @@
| _ => error ("Not an equation with two constants: "
^ Syntax.string_of_term_global thy eqn);
val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then ()
- else error ("Inconsistent class: " ^ Display.string_of_thm thm);
+ else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);
in thy |>
(map_exec_purge NONE o map_aliasses) (fn (alias, classes) =>
((c_c', thm) :: alias, insert (op =) class classes))
--- a/src/Pure/Isar/context_rules.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Isar/context_rules.ML Wed Jul 22 11:23:09 2009 +0200
@@ -116,7 +116,7 @@
fun prt_kind (i, b) =
Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
(map_filter (fn (_, (k, th)) =>
- if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
+ if k = (i, b) then SOME (Display.pretty_thm ctxt th) else NONE)
(sort (int_ord o pairself fst) rules));
in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
--- a/src/Pure/Isar/element.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Isar/element.ML Wed Jul 22 11:23:09 2009 +0200
@@ -163,7 +163,7 @@
let
val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
- val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
+ val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
val prt_name_atts = pretty_name_atts ctxt;
fun prt_mixfix NoSyn = []
--- a/src/Pure/Isar/isar_cmd.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Jul 22 11:23:09 2009 +0200
@@ -442,8 +442,7 @@
|> Pretty.chunks2 |> Pretty.string_of;
fun string_of_thms state args =
- Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state)
- (Proof.get_thmss state args));
+ Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss state args));
fun string_of_prfs full state arg =
Pretty.string_of (case arg of
--- a/src/Pure/Isar/local_defs.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Isar/local_defs.ML Wed Jul 22 11:23:09 2009 +0200
@@ -196,7 +196,7 @@
fun print_rules ctxt =
Pretty.writeln (Pretty.big_list "definitional transformations:"
- (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
+ (map (Display.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
--- a/src/Pure/Isar/method.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Isar/method.ML Wed Jul 22 11:23:09 2009 +0200
@@ -220,7 +220,7 @@
fun trace ctxt rules =
if ! trace_rules andalso not (null rules) then
- Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules)
+ Pretty.big_list "rules:" (map (Display.pretty_thm ctxt) rules)
|> Pretty.string_of |> tracing
else ();
--- a/src/Pure/Isar/obtain.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Isar/obtain.ML Wed Jul 22 11:23:09 2009 +0200
@@ -180,9 +180,9 @@
[prem] =>
if Thm.concl_of th aconv thesis andalso
Logic.strip_assums_concl prem aconv thesis then th
- else error ("Guessed a different clause:\n" ^ ProofContext.string_of_thm ctxt th)
+ else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
| [] => error "Goal solved -- nothing guessed."
- | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th));
+ | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
fun result tac facts ctxt =
let
@@ -218,7 +218,7 @@
val string_of_typ = Syntax.string_of_typ ctxt;
val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
- fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
+ fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1;
val rule = Thm.incr_indexes (maxidx + 1) raw_rule;
--- a/src/Pure/Isar/proof.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Isar/proof.ML Wed Jul 22 11:23:09 2009 +0200
@@ -318,11 +318,11 @@
val show_main_goal = ref false;
val verbose = ProofContext.verbose;
-val pretty_goals_local = Display.pretty_goals_aux o Syntax.pp;
+val pretty_goals_local = Display_Goal.pretty_goals_aux o Syntax.pp;
fun pretty_facts _ _ NONE = []
| pretty_facts s ctxt (SOME ths) =
- [Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""];
+ [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""];
fun pretty_state nr state =
let
@@ -470,7 +470,7 @@
let
val thy = ProofContext.theory_of ctxt;
val string_of_term = Syntax.string_of_term ctxt;
- val string_of_thm = ProofContext.string_of_thm ctxt;
+ val string_of_thm = Display.string_of_thm ctxt;
val ngoals = Thm.nprems_of goal;
val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
--- a/src/Pure/Isar/proof_context.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Jul 22 11:23:09 2009 +0200
@@ -36,13 +36,8 @@
val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
val extern_fact: Proof.context -> string -> xstring
val pretty_term_abbrev: Proof.context -> term -> Pretty.T
- val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
- val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
- val pretty_thm: Proof.context -> thm -> Pretty.T
- val pretty_thms: Proof.context -> thm list -> Pretty.T
val pretty_fact: Proof.context -> string * thm list -> Pretty.T
- val string_of_thm: Proof.context -> thm -> string
val read_typ: Proof.context -> string -> typ
val read_typ_syntax: Proof.context -> string -> typ
val read_typ_abbrev: Proof.context -> string -> typ
@@ -293,31 +288,18 @@
fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
-fun pretty_thm_aux ctxt show_status th =
- let
- val flags = {quote = false, show_hyps = true, show_status = show_status};
- val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
- in Display.pretty_thm_aux (Syntax.pp ctxt) flags asms th end;
-
-fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
- | pretty_thms_aux ctxt flag ths =
- Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
-
fun pretty_fact_name ctxt a = Pretty.block
[Pretty.markup (Markup.fact a) [Pretty.str (extern_fact ctxt a)], Pretty.str ":"];
-fun pretty_fact_aux ctxt flag ("", ths) = pretty_thms_aux ctxt flag ths
+fun pretty_fact_aux ctxt flag ("", ths) =
+ Display.pretty_thms_aux ctxt flag ths
| pretty_fact_aux ctxt flag (a, [th]) = Pretty.block
- [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm_aux ctxt flag th]
+ [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm_aux ctxt flag th]
| pretty_fact_aux ctxt flag (a, ths) = Pretty.block
- (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm_aux ctxt flag) ths));
+ (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm_aux ctxt flag) ths));
-fun pretty_thm ctxt = pretty_thm_aux ctxt true;
-fun pretty_thms ctxt = pretty_thms_aux ctxt true;
fun pretty_fact ctxt = pretty_fact_aux ctxt true;
-val string_of_thm = Pretty.string_of oo pretty_thm;
-
(** prepare types **)
@@ -1369,7 +1351,7 @@
val suppressed = len - ! prems_limit;
val prt_prems = if null prems then []
else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @
- map (pretty_thm ctxt) (Library.drop (suppressed, prems)))];
+ map (Display.pretty_thm ctxt) (Library.drop (suppressed, prems)))];
in prt_structs @ prt_fixes @ prt_prems end;
--- a/src/Pure/Isar/proof_display.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Isar/proof_display.ML Wed Jul 22 11:23:09 2009 +0200
@@ -35,7 +35,7 @@
let
val thy = Thm.theory_of_thm th;
val flags = {quote = true, show_hyps = false, show_status = true};
- in Display.pretty_thm_aux (Syntax.pp_global thy) flags [] th end;
+ in Display.pretty_thm_raw (Syntax.pp_global thy) flags [] th end;
val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
val pp_term = Pretty.quote oo Syntax.pretty_term_global;
@@ -68,7 +68,7 @@
fun pretty_rule ctxt s thm =
Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
- Pretty.fbrk, ProofContext.pretty_thm_aux ctxt false thm];
+ Pretty.fbrk, Display.pretty_thm_aux ctxt false thm];
val string_of_rule = Pretty.string_of ooo pretty_rule;
--- a/src/Pure/Isar/runtime.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Isar/runtime.ML Wed Jul 22 11:23:09 2009 +0200
@@ -75,7 +75,7 @@
| exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
(if detailed then if_context ctxt Syntax.string_of_term ts else []))
| exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
- (if detailed then if_context ctxt ProofContext.string_of_thm thms else []))
+ (if detailed then if_context ctxt Display.string_of_thm thms else []))
| exn_msg _ exn = raised exn (General.exnMessage exn) [];
in exn_msg NONE e end;
--- a/src/Pure/ML-Systems/exn.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/ML-Systems/exn.ML Wed Jul 22 11:23:09 2009 +0200
@@ -13,6 +13,8 @@
val release: 'a result -> 'a
exception Interrupt
exception EXCEPTIONS of exn list
+ val flatten: exn -> exn list
+ val flatten_list: exn list -> exn list
val release_all: 'a result list -> 'a list
val release_first: 'a result list -> 'a list
end;
@@ -43,19 +45,15 @@
exception Interrupt = Interrupt;
exception EXCEPTIONS of exn list;
-fun plain_exns (Result _) = []
- | plain_exns (Exn Interrupt) = []
- | plain_exns (Exn (EXCEPTIONS exns)) = List.concat (map (plain_exns o Exn) exns)
- | plain_exns (Exn exn) = [exn];
-
+fun flatten Interrupt = []
+ | flatten (EXCEPTIONS exns) = flatten_list exns
+ | flatten exn = [exn]
+and flatten_list exns = List.concat (map flatten exns);
fun release_all results =
if List.all (fn Result _ => true | _ => false) results
then map (fn Result x => x) results
- else
- (case List.concat (map plain_exns results) of
- [] => raise Interrupt
- | exns => raise EXCEPTIONS exns);
+ else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
fun release_first results = release_all results
handle EXCEPTIONS (exn :: _) => reraise exn;
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Wed Jul 22 11:23:09 2009 +0200
@@ -92,10 +92,12 @@
val _ = Thread.setAttributes orig_atts;
in Exn.release result end;
-fun interruptible f = with_attributes regular_interrupts (fn _ => f);
+fun interruptible f =
+ with_attributes regular_interrupts (fn _ => fn x => f x);
fun uninterruptible f =
- with_attributes no_interrupts (fn atts => f (fn g => with_attributes atts (fn _ => g)));
+ with_attributes no_interrupts (fn atts => fn x =>
+ f (fn g => with_attributes atts (fn _ => fn y => g y)) x);
(* execution with time limit *)
--- a/src/Pure/Proof/reconstruct.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML Wed Jul 22 11:23:09 2009 +0200
@@ -255,7 +255,7 @@
let
fun search env [] = error ("Unsolvable constraints:\n" ^
Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
- Display.pretty_flexpair (Syntax.pp_global thy) (pairself
+ Display_Goal.pretty_flexpair (Syntax.pp_global thy) (pairself
(Envir.norm_term bigenv) p)) cs)))
| search env ((u, p as (t1, t2), vs)::ps) =
if u then
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Jul 22 11:23:09 2009 +0200
@@ -655,7 +655,7 @@
text=[XML.Elem("pgml",[],
maps YXML.parse_body strings)] })
- fun string_of_thm th = Pretty.string_of (Display.pretty_thm_aux
+ fun string_of_thm th = Pretty.string_of (Display.pretty_thm_raw
(Syntax.pp_global (Thm.theory_of_thm th))
{quote = false, show_hyps = false, show_status = true} [] th)
--- a/src/Pure/ROOT.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/ROOT.ML Wed Jul 22 11:23:09 2009 +0200
@@ -115,17 +115,18 @@
use "more_thm.ML";
use "facts.ML";
use "pure_thy.ML";
-use "display.ML";
use "drule.ML";
use "morphism.ML";
use "variable.ML";
use "conv.ML";
+use "display_goal.ML";
use "tctical.ML";
use "search.ML";
use "tactic.ML";
use "meta_simplifier.ML";
use "conjunction.ML";
use "assumption.ML";
+use "display.ML";
use "goal.ML";
use "axclass.ML";
--- a/src/Pure/Thy/thy_info.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Jul 22 11:23:09 2009 +0200
@@ -23,6 +23,7 @@
val get_parents: string -> string list
val touch_thy: string -> unit
val touch_child_thys: string -> unit
+ val thy_ord: theory * theory -> order
val remove_thy: string -> unit
val kill_thy: string -> unit
val provide_file: Path.T -> string -> unit
@@ -33,7 +34,6 @@
val use_thys: string list -> unit
val use_thy: string -> unit
val time_use_thy: string -> unit
- val thy_ord: theory * theory -> order
val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
val end_theory: theory -> unit
val register_thy: string -> unit
@@ -231,17 +231,36 @@
end;
-(* manage pending proofs *)
+(* management data *)
+
+structure Management_Data = TheoryDataFun
+(
+ type T =
+ Task_Queue.group option * (*worker thread group*)
+ int; (*abstract update time*)
+ val empty = (NONE, 0);
+ val copy = I;
+ fun extend _ = empty;
+ fun merge _ _ = empty;
+);
+
+val thy_ord = int_ord o pairself (#2 o Management_Data.get);
+
+
+(* pending proofs *)
fun join_thy name =
(case lookup_theory name of
- NONE => []
+ NONE => ()
| SOME thy => PureThy.join_proofs thy);
fun cancel_thy name =
(case lookup_theory name of
NONE => ()
- | SOME thy => PureThy.cancel_proofs thy);
+ | SOME thy =>
+ (case #1 (Management_Data.get thy) of
+ NONE => ()
+ | SOME group => Future.cancel_group group));
(* remove theory *)
@@ -374,8 +393,7 @@
val exns = tasks |> maps (fn (name, _) =>
let
val after_load = Future.join (the (Symtab.lookup futures name));
- val proof_exns = join_thy name;
- val _ = null proof_exns orelse raise Exn.EXCEPTIONS proof_exns;
+ val _ = join_thy name;
val _ = after_load ();
in [] end handle exn => (kill_thy name; [exn]));
@@ -509,20 +527,6 @@
end;
-(* update_time *)
-
-structure UpdateTime = TheoryDataFun
-(
- type T = int;
- val empty = 0;
- val copy = I;
- fun extend _ = empty;
- fun merge _ _ = empty;
-);
-
-val thy_ord = int_ord o pairself UpdateTime.get;
-
-
(* begin / end theory *)
fun begin_theory name parents uses int =
@@ -542,7 +546,7 @@
val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
val update_time = if update_time > 0 then update_time else serial ();
val theory' = theory
- |> UpdateTime.put update_time
+ |> Management_Data.put (Future.worker_group (), update_time)
|> Present.begin_theory update_time dir uses;
val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
@@ -569,7 +573,7 @@
val _ = check_unfinished error name;
val _ = touch_thy name;
val master = #master (ThyLoad.deps_thy Path.current name);
- val upd_time = UpdateTime.get thy;
+ val upd_time = #2 (Management_Data.get thy);
in
CRITICAL (fn () =>
(change_deps name (Option.map
--- a/src/Pure/Tools/find_theorems.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML Wed Jul 22 11:23:09 2009 +0200
@@ -408,7 +408,7 @@
fun pretty_thm ctxt (thmref, thm) = Pretty.block
[Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
- ProofContext.pretty_thm ctxt thm];
+ Display.pretty_thm ctxt thm];
fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
let
--- a/src/Pure/display.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/display.ML Wed Jul 22 11:23:09 2009 +0200
@@ -1,34 +1,32 @@
(* Title: Pure/display.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Author: Makarius
-Printing of theorems, goals, results etc.
+Printing of theorems, results etc.
*)
signature BASIC_DISPLAY =
sig
val goals_limit: int ref
+ val show_consts: bool ref
val show_hyps: bool ref
val show_tags: bool ref
- val show_consts: bool ref
end;
signature DISPLAY =
sig
include BASIC_DISPLAY
- val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
- val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
+ val pretty_thm_raw: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
term list -> thm -> Pretty.T
- val pretty_thm: thm -> Pretty.T
- val string_of_thm: thm -> string
- val pretty_thms: thm list -> Pretty.T
- val pretty_thm_sg: theory -> thm -> Pretty.T
- val pretty_thms_sg: theory -> thm list -> Pretty.T
- val print_thm: thm -> unit
- val print_thms: thm list -> unit
- val prth: thm -> thm
- val prthq: thm Seq.seq -> thm Seq.seq
- val prths: thm list -> thm list
+ val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
+ val pretty_thm: Proof.context -> thm -> Pretty.T
+ val pretty_thm_global: theory -> thm -> Pretty.T
+ val pretty_thm_without_context: thm -> Pretty.T
+ val string_of_thm: Proof.context -> thm -> string
+ val string_of_thm_global: theory -> thm -> string
+ val string_of_thm_without_context: thm -> string
+ val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
+ val pretty_thms: Proof.context -> thm list -> Pretty.T
val pretty_ctyp: ctyp -> Pretty.T
val string_of_ctyp: ctyp -> string
val print_ctyp: ctyp -> unit
@@ -37,27 +35,26 @@
val print_cterm: cterm -> unit
val print_syntax: theory -> unit
val pretty_full_theory: bool -> theory -> Pretty.T list
- val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
- val pretty_goals: int -> thm -> Pretty.T list
- val print_goals: int -> thm -> unit
end;
structure Display: DISPLAY =
struct
+(** options **)
+
+val goals_limit = Display_Goal.goals_limit;
+val show_consts = Display_Goal.show_consts;
+
+val show_hyps = ref false; (*false: print meta-hypotheses as dots*)
+val show_tags = ref false; (*false: suppress tags*)
+
+
(** print thm **)
-val goals_limit = ref 10; (*max number of goals to print*)
-val show_hyps = ref false; (*false: print meta-hypotheses as dots*)
-val show_tags = ref false; (*false: suppress tags*)
-
fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
-fun pretty_flexpair pp (t, u) = Pretty.block
- [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
-
fun display_status false _ = ""
| display_status true th =
let
@@ -71,7 +68,7 @@
else ""
end;
-fun pretty_thm_aux pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
+fun pretty_thm_raw pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
let
val th = Thm.strip_shyps raw_th;
val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
@@ -89,7 +86,7 @@
if hlen = 0 andalso status = "" then []
else if ! show_hyps orelse show_hyps' then
[Pretty.brk 2, Pretty.list "[" "]"
- (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
+ (map (q o Display_Goal.pretty_flexpair pp) tpairs @ map prt_term hyps' @
map (Pretty.sort pp) xshyps @
(if status = "" then [] else [Pretty.str status]))]
else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
@@ -98,27 +95,33 @@
else [Pretty.brk 1, pretty_tags tags];
in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
-fun pretty_thm th =
- pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th))
- {quote = true, show_hyps = false, show_status = true} [] th;
-
-val string_of_thm = Pretty.string_of o pretty_thm;
-
-fun pretty_thms [th] = pretty_thm th
- | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
-
-val pretty_thm_sg = pretty_thm oo Thm.transfer;
-val pretty_thms_sg = pretty_thms oo (map o Thm.transfer);
+fun pretty_thm_aux ctxt show_status th =
+ let
+ val flags = {quote = false, show_hyps = true, show_status = show_status};
+ val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
+ in pretty_thm_raw (Syntax.pp ctxt) flags asms th end;
-(* top-level commands for printing theorems *)
+fun pretty_thm ctxt = pretty_thm_aux ctxt true;
+
+fun pretty_thm_global thy th =
+ pretty_thm_raw (Syntax.pp_global thy)
+ {quote = false, show_hyps = false, show_status = true} [] th;
+
+fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
-val print_thm = Pretty.writeln o pretty_thm;
-val print_thms = Pretty.writeln o pretty_thms;
+val string_of_thm = Pretty.string_of oo pretty_thm;
+val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
+val string_of_thm_without_context = Pretty.string_of o pretty_thm_without_context;
+
-fun prth th = (print_thm th; th);
-fun prthq thq = (Seq.print (K print_thm) 100000 thq; thq);
-fun prths ths = (prthq (Seq.of_list ths); ths);
+(* multiple theorems *)
+
+fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
+ | pretty_thms_aux ctxt flag ths =
+ Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
+
+fun pretty_thms ctxt = pretty_thms_aux ctxt true;
(* other printing commands *)
@@ -242,109 +245,7 @@
Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]]
end;
-
-
-(** print_goals **)
-
-(* print_goals etc. *)
-
-val show_consts = ref false; (*true: show consts with types in proof state output*)
-
-
-(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
-
-local
-
-fun ins_entry (x, y) =
- AList.default (op =) (x, []) #>
- AList.map_entry (op =) x (insert (op =) y);
-
-val add_consts = Term.fold_aterms
- (fn Const (c, T) => ins_entry (T, (c, T))
- | _ => I);
-
-val add_vars = Term.fold_aterms
- (fn Free (x, T) => ins_entry (T, (x, ~1))
- | Var (xi, T) => ins_entry (T, xi)
- | _ => I);
-
-val add_varsT = Term.fold_atyps
- (fn TFree (x, S) => ins_entry (S, (x, ~1))
- | TVar (xi, S) => ins_entry (S, xi)
- | _ => I);
-
-fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
-fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
-
-fun consts_of t = sort_cnsts (add_consts t []);
-fun vars_of t = sort_idxs (add_vars t []);
-fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
-
-in
-
-fun pretty_goals_aux pp markup (msg, main) maxgoals state =
- let
- fun prt_atoms prt prtT (X, xs) = Pretty.block
- [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
- Pretty.brk 1, prtT X];
-
- fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x)
- | prt_var xi = Pretty.term pp (Syntax.var xi);
-
- fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
- | prt_varT xi = Pretty.typ pp (TVar (xi, []));
-
- val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp);
- val prt_vars = prt_atoms prt_var (Pretty.typ pp);
- val prt_varsT = prt_atoms prt_varT (Pretty.sort pp);
-
-
- fun pretty_list _ _ [] = []
- | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
-
- fun pretty_subgoal (n, A) = Pretty.markup markup
- [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A];
- fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
-
- val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
-
- val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
- val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
- val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
-
-
- val {prop, tpairs, ...} = Thm.rep_thm state;
- val (As, B) = Logic.strip_horn prop;
- val ngoals = length As;
-
- fun pretty_gs (types, sorts) =
- (if main then [Pretty.term pp B] else []) @
- (if ngoals = 0 then [Pretty.str "No subgoals!"]
- else if ngoals > maxgoals then
- pretty_subgoals (Library.take (maxgoals, As)) @
- (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
- else [])
- else pretty_subgoals As) @
- pretty_ffpairs tpairs @
- (if ! show_consts then pretty_consts prop else []) @
- (if types then pretty_vars prop else []) @
- (if sorts then pretty_varsT prop else []);
- in
- setmp show_no_free_types true
- (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
- (setmp show_sorts false pretty_gs))
- (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
- end;
-
-fun pretty_goals n th =
- pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
-
-val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
-
end;
-
-end;
-
-structure BasicDisplay: BASIC_DISPLAY = Display;
-open BasicDisplay;
+structure Basic_Display: BASIC_DISPLAY = Display;
+open Basic_Display;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/display_goal.ML Wed Jul 22 11:23:09 2009 +0200
@@ -0,0 +1,121 @@
+(* Title: Pure/display_goal.ML
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Makarius
+
+Display tactical goal state.
+*)
+
+signature DISPLAY_GOAL =
+sig
+ val goals_limit: int ref
+ val show_consts: bool ref
+ val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
+ val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
+ val pretty_goals: int -> thm -> Pretty.T list
+ val print_goals: int -> thm -> unit
+end;
+
+structure Display_Goal: DISPLAY_GOAL =
+struct
+
+val goals_limit = ref 10; (*max number of goals to print*)
+val show_consts = ref false; (*true: show consts with types in proof state output*)
+
+fun pretty_flexpair pp (t, u) = Pretty.block
+ [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
+
+
+(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
+
+local
+
+fun ins_entry (x, y) =
+ AList.default (op =) (x, []) #>
+ AList.map_entry (op =) x (insert (op =) y);
+
+val add_consts = Term.fold_aterms
+ (fn Const (c, T) => ins_entry (T, (c, T))
+ | _ => I);
+
+val add_vars = Term.fold_aterms
+ (fn Free (x, T) => ins_entry (T, (x, ~1))
+ | Var (xi, T) => ins_entry (T, xi)
+ | _ => I);
+
+val add_varsT = Term.fold_atyps
+ (fn TFree (x, S) => ins_entry (S, (x, ~1))
+ | TVar (xi, S) => ins_entry (S, xi)
+ | _ => I);
+
+fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
+fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
+
+fun consts_of t = sort_cnsts (add_consts t []);
+fun vars_of t = sort_idxs (add_vars t []);
+fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
+
+in
+
+fun pretty_goals_aux pp markup (msg, main) maxgoals state =
+ let
+ fun prt_atoms prt prtT (X, xs) = Pretty.block
+ [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
+ Pretty.brk 1, prtT X];
+
+ fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x)
+ | prt_var xi = Pretty.term pp (Syntax.var xi);
+
+ fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
+ | prt_varT xi = Pretty.typ pp (TVar (xi, []));
+
+ val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp);
+ val prt_vars = prt_atoms prt_var (Pretty.typ pp);
+ val prt_varsT = prt_atoms prt_varT (Pretty.sort pp);
+
+
+ fun pretty_list _ _ [] = []
+ | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
+
+ fun pretty_subgoal (n, A) = Pretty.markup markup
+ [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A];
+ fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
+
+ val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
+
+ val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
+ val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
+ val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
+
+
+ val {prop, tpairs, ...} = Thm.rep_thm state;
+ val (As, B) = Logic.strip_horn prop;
+ val ngoals = length As;
+
+ fun pretty_gs (types, sorts) =
+ (if main then [Pretty.term pp B] else []) @
+ (if ngoals = 0 then [Pretty.str "No subgoals!"]
+ else if ngoals > maxgoals then
+ pretty_subgoals (Library.take (maxgoals, As)) @
+ (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
+ else [])
+ else pretty_subgoals As) @
+ pretty_ffpairs tpairs @
+ (if ! show_consts then pretty_consts prop else []) @
+ (if types then pretty_vars prop else []) @
+ (if sorts then pretty_varsT prop else []);
+ in
+ setmp show_no_free_types true
+ (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
+ (setmp show_sorts false pretty_gs))
+ (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
+ end;
+
+fun pretty_goals n th =
+ pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
+
+val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
+
+end;
+
+end;
+
--- a/src/Pure/goal.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/goal.ML Wed Jul 22 11:23:09 2009 +0200
@@ -78,7 +78,7 @@
(case Thm.nprems_of th of
0 => conclude th
| n => raise THM ("Proof failed.\n" ^
- Pretty.string_of (Pretty.chunks (Display.pretty_goals n th)) ^
+ Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals n th)) ^
("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
--- a/src/Pure/old_goals.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/old_goals.ML Wed Jul 22 11:23:09 2009 +0200
@@ -135,7 +135,7 @@
(*Default action is to print an error message; could be suppressed for
special applications.*)
fun result_error_default state msg : thm =
- Pretty.str "Bad final proof state:" :: Display.pretty_goals (!goals_limit) state @
+ Pretty.str "Bad final proof state:" :: Display_Goal.pretty_goals (!goals_limit) state @
[Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
val result_error_fn = ref result_error_default;
@@ -199,7 +199,7 @@
case e of
THM (msg,i,thms) =>
(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
- List.app Display.print_thm thms)
+ List.app (writeln o Display.string_of_thm_global thy) thms)
| THEORY (msg,thys) =>
(writeln ("Exception THEORY raised:\n" ^ msg);
List.app (writeln o Context.str_of_thy) thys)
@@ -277,7 +277,7 @@
(if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
(if ngoals <> 1 then "s" else "") ^ ")"
else ""))] @
- Display.pretty_goals m th
+ Display_Goal.pretty_goals m th
end |> Pretty.chunks |> Pretty.writeln;
(*Printing can raise exceptions, so the assignment occurs last.
--- a/src/Pure/proofterm.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/proofterm.ML Wed Jul 22 11:23:09 2009 +0200
@@ -37,10 +37,8 @@
type oracle = string * term
type pthm = serial * (string * term * proof_body future)
- val join_body: proof_body future ->
- {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
+ val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
- val proof_of: proof_body -> 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
@@ -152,10 +150,8 @@
type oracle = string * term;
type pthm = serial * (string * term * proof_body future);
-val join_body = Future.join #> (fn PBody args => args);
-val join_proof = #proof o join_body;
-
fun proof_of (PBody {proof, ...}) = proof;
+val join_proof = Future.join #> proof_of;
(***** proof atoms *****)
@@ -177,13 +173,15 @@
fun fold_body_thms f =
let
- fun app (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => 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);
+ fun app (PBody {thms, ...}) =
+ (Future.join_results (map (#3 o #2) thms);
+ thms |> fold (fn (i, (name, prop, body)) => 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));
in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
@@ -223,13 +221,14 @@
val all_oracles_of =
let
fun collect (PBody {oracles, thms, ...}) =
+ (Future.join_results (map (#3 o #2) thms);
thms |> fold (fn (i, (_, _, body)) => 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);
- in (merge_oracles oracles x', seen') end);
+ in (merge_oracles oracles x', seen') end));
in fn body => #1 (collect body ([], Inttab.empty)) end;
fun approximate_proof_body prf =
@@ -1342,5 +1341,5 @@
end;
-structure BasicProofterm : BASIC_PROOFTERM = Proofterm;
-open BasicProofterm;
+structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm;
+open Basic_Proofterm;
--- a/src/Pure/pure_thy.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/pure_thy.ML Wed Jul 22 11:23:09 2009 +0200
@@ -10,8 +10,7 @@
val intern_fact: theory -> xstring -> string
val defined_fact: theory -> string -> bool
val hide_fact: bool -> string -> theory -> theory
- val join_proofs: theory -> exn list
- val cancel_proofs: theory -> unit
+ val join_proofs: theory -> unit
val get_fact: Context.generic -> theory -> Facts.ref -> thm list
val get_thms: theory -> xstring -> thm list
val get_thm: theory -> xstring -> thm
@@ -59,11 +58,11 @@
structure FactsData = TheoryDataFun
(
- type T = Facts.T * (unit lazy list * Task_Queue.group Inttab.table);
- val empty = (Facts.empty, ([], Inttab.empty));
+ type T = Facts.T * thm list;
+ val empty = (Facts.empty, []);
val copy = I;
- fun extend (facts, _) = (facts, ([], Inttab.empty));
- fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], Inttab.empty));
+ fun extend (facts, _) = (facts, []);
+ fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
);
@@ -79,14 +78,9 @@
(* proofs *)
-fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
+fun register_proofs (thy, thms) = (FactsData.map (apsnd (append thms)) thy, thms);
-fun join_proofs thy =
- map_filter (Exn.get_exn o Lazy.force_result) (rev (#1 (#2 (FactsData.get thy))));
-
-fun cancel_proofs thy =
- Inttab.fold (fn (_, group) => fn () => Future.cancel_group group)
- (#2 (#2 (FactsData.get thy))) ();
+fun join_proofs thy = Thm.join_proofs (rev (#2 (FactsData.get thy)));
@@ -146,24 +140,15 @@
(* enter_thms *)
-val pending_groups =
- Thm.promises_of #> fold (fn (_, future) =>
- if Future.is_finished future then I
- else Inttab.update (`Task_Queue.group_id (Future.group_of future)));
-
-fun enter_proofs (thy, thms) =
- (FactsData.map (apsnd (fn (proofs, groups) =>
- (fold (cons o lazy_proof) thms proofs, fold pending_groups thms groups))) thy, thms);
-
fun enter_thms pre_name post_name app_att (b, thms) thy =
if Binding.is_empty b
- then swap (enter_proofs (app_att (thy, thms)))
+ then swap (register_proofs (app_att (thy, thms)))
else
let
val naming = Sign.naming_of thy;
val name = NameSpace.full_name naming b;
val (thy', thms') =
- enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
+ register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
val thms'' = map (Thm.transfer thy') thms';
val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
in (thms'', thy'') end;
--- a/src/Pure/simplifier.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/simplifier.ML Wed Jul 22 11:23:09 2009 +0200
@@ -79,7 +79,7 @@
fun pretty_ss ctxt ss =
let
val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
- val pretty_thm = ProofContext.pretty_thm ctxt;
+ val pretty_thm = Display.pretty_thm ctxt;
fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss);
fun pretty_cong (name, thm) =
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
--- a/src/Pure/tctical.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/tctical.ML Wed Jul 22 11:23:09 2009 +0200
@@ -195,7 +195,7 @@
(fn st =>
(tracing msg;
tracing ((Pretty.string_of o Pretty.chunks o
- Display.pretty_goals (! Display.goals_limit)) st);
+ Display_Goal.pretty_goals (! Display_Goal.goals_limit)) st);
Seq.single st));
(*Pause until a line is typed -- if non-empty then fail. *)
@@ -233,7 +233,7 @@
(*Extract from a tactic, a thm->thm seq function that handles tracing*)
fun tracify flag tac st =
if !flag andalso not (!suppress_tracing)
- then (Display.print_goals (! Display.goals_limit) st;
+ then (Display_Goal.print_goals (! Display_Goal.goals_limit) st;
tracing "** Press RETURN to continue:";
exec_trace_command flag (tac,st))
else tac st;
--- a/src/Pure/thm.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Pure/thm.ML Wed Jul 22 11:23:09 2009 +0200
@@ -141,10 +141,9 @@
val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
val rename_boundvars: term -> term -> thm -> thm
+ val join_proofs: thm list -> unit
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
- val join_proof: thm -> unit
- val promises_of: thm -> (serial * thm future) list
val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
val future: thm future -> cterm -> thm
val get_name: thm -> string
@@ -1612,18 +1611,18 @@
fun raw_body (Thm (Deriv {body, ...}, _)) = body;
fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
- let val ps = map (apsnd (fulfill_body o Future.join)) promises
- in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
+ Pt.fulfill_proof (Theory.deref thy_ref)
+ (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
+and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
+
+val join_proofs = Pt.join_bodies o map fulfill_body;
fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
val proof_of = Pt.proof_of o proof_body_of;
-val join_proof = ignore o proof_body_of;
(* derivation status *)
-fun promises_of (Thm (Deriv {promises, ...}, _)) = promises;
-
fun status_of (Thm (Deriv {promises, body}, _)) =
let
val ps = map (Future.peek o snd) promises;
@@ -1652,7 +1651,7 @@
val _ = null hyps orelse err "bad hyps";
val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
- val _ = List.app (ignore o fulfill_body o Future.join o #2) promises;
+ val _ = fulfill_bodies (map #2 promises);
in thm end;
fun future future_thm ct =
@@ -1743,5 +1742,5 @@
end;
-structure BasicThm: BASIC_THM = Thm;
-open BasicThm;
+structure Basic_Thm: BASIC_THM = Thm;
+open Basic_Thm;
--- a/src/Sequents/prover.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Sequents/prover.ML Wed Jul 22 11:23:09 2009 +0200
@@ -27,7 +27,8 @@
fun warn_duplicates [] = []
| warn_duplicates dups =
- (warning (cat_lines ("Ignoring duplicate theorems:" :: map Display.string_of_thm dups));
+ (warning (cat_lines ("Ignoring duplicate theorems:" ::
+ map Display.string_of_thm_without_context dups));
dups);
fun (Pack(safes,unsafes)) add_safes ths =
@@ -50,8 +51,9 @@
fun print_pack (Pack(safes,unsafes)) =
- (writeln "Safe rules:"; Display.print_thms safes;
- writeln "Unsafe rules:"; Display.print_thms unsafes);
+ writeln (cat_lines
+ (["Safe rules:"] @ map Display.string_of_thm_without_context safes @
+ ["Unsafe rules:"] @ map Display.string_of_thm_without_context unsafes));
(*Returns the list of all formulas in the sequent*)
fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
--- a/src/Sequents/simpdata.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Sequents/simpdata.ML Wed Jul 22 11:23:09 2009 +0200
@@ -40,7 +40,7 @@
| (Const("Not",_)$_) => th RS @{thm iff_reflection_F}
| _ => th RS @{thm iff_reflection_T})
| _ => error ("addsimps: unable to use theorem\n" ^
- Display.string_of_thm th));
+ Display.string_of_thm_without_context th));
(*Replace premises x=y, X<->Y by X==Y*)
val mk_meta_prems =
--- a/src/Tools/Code/code_preproc.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML Wed Jul 22 11:23:09 2009 +0200
@@ -214,7 +214,7 @@
|> map (fn (s, thms) =>
(Pretty.block o Pretty.fbreaks) (
Pretty.str s
- :: map (Display.pretty_thm o fst) thms
+ :: map (Display.pretty_thm_global thy o fst) thms
))
|> Pretty.chunks;
@@ -529,7 +529,7 @@
in
Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
error ("could not construct evaluation proof:\n"
- ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
+ ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
end;
in gen_eval thy I conclude_evaluation end;
--- a/src/Tools/Code/code_printer.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Tools/Code/code_printer.ML Wed Jul 22 11:23:09 2009 +0200
@@ -82,7 +82,7 @@
open Code_Thingol;
-fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
+fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm);
(** assembling text pieces **)
--- a/src/Tools/Code/code_thingol.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML Wed Jul 22 11:23:09 2009 +0200
@@ -469,7 +469,7 @@
let
val err_class = Sorts.class_error (Syntax.pp_global thy) e;
val err_thm = case thm
- of SOME thm => "\n(in code equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
+ of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")" | NONE => "";
val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
^ Syntax.string_of_sort_global thy sort;
in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
--- a/src/Tools/coherent.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Tools/coherent.ML Wed Jul 22 11:23:09 2009 +0200
@@ -177,7 +177,7 @@
fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
let
val _ = message (fn () => space_implode "\n"
- ("asms:" :: map Display.string_of_thm asms) ^ "\n\n");
+ ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
val th' = Drule.implies_elim_list
(Thm.instantiate
(map (fn (ixn, (S, T)) =>
--- a/src/Tools/induct.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Tools/induct.ML Wed Jul 22 11:23:09 2009 +0200
@@ -124,7 +124,7 @@
fun pretty_rules ctxt kind rs =
let val thms = map snd (Item_Net.content rs)
- in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
+ in Pretty.big_list kind (map (Display.pretty_thm ctxt) thms) end;
(* context data *)
--- a/src/ZF/Tools/inductive_package.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed Jul 22 11:23:09 2009 +0200
@@ -247,8 +247,7 @@
(intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
|> ListPair.map (fn (t, tacs) =>
Goal.prove_global thy1 [] [] t
- (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
- handle MetaSimplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
+ (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)));
(********)
val dummy = writeln " Proving the elimination rule...";
@@ -318,11 +317,12 @@
val ind_prems = map (induct_prem (map (rpair pred) rec_tms))
intr_tms;
- val dummy = if !Ind_Syntax.trace then
- (writeln "ind_prems = ";
- List.app (writeln o Syntax.string_of_term ctxt1) ind_prems;
- writeln "raw_induct = "; Display.print_thm raw_induct)
- else ();
+ val dummy =
+ if ! Ind_Syntax.trace then
+ writeln (cat_lines
+ (["ind_prems:"] @ map (Syntax.string_of_term ctxt1) ind_prems @
+ ["raw_induct:", Display.string_of_thm ctxt1 raw_induct]))
+ else ();
(*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
@@ -351,9 +351,10 @@
ORELSE' bound_hyp_subst_tac)),
ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
- val dummy = if !Ind_Syntax.trace then
- (writeln "quant_induct = "; Display.print_thm quant_induct)
- else ();
+ val dummy =
+ if ! Ind_Syntax.trace then
+ writeln ("quant_induct:\n" ^ Display.string_of_thm ctxt1 quant_induct)
+ else ();
(*** Prove the simultaneous induction rule ***)
@@ -426,9 +427,10 @@
REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))
else (writeln " [ No mutual induction rule needed ]"; @{thm TrueI});
- val dummy = if !Ind_Syntax.trace then
- (writeln "lemma = "; Display.print_thm lemma)
- else ();
+ val dummy =
+ if ! Ind_Syntax.trace then
+ writeln ("lemma: " ^ Display.string_of_thm ctxt1 lemma)
+ else ();
(*Mutual induction follows by freeness of Inl/Inr.*)
--- a/src/ZF/Tools/typechk.ML Wed Jul 22 10:49:26 2009 +0200
+++ b/src/ZF/Tools/typechk.ML Wed Jul 22 11:23:09 2009 +0200
@@ -27,7 +27,8 @@
fun add_rule th (tcs as TC {rules, net}) =
if member Thm.eq_thm_prop rules th then
- (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm th); tcs)
+ (warning ("Ignoring duplicate type-checking rule\n" ^
+ Display.string_of_thm_without_context th); tcs)
else
TC {rules = th :: rules,
net = Net.insert_term (K false) (Thm.concl_of th, th) net};
@@ -36,7 +37,8 @@
if member Thm.eq_thm_prop rules th then
TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
rules = remove Thm.eq_thm_prop th rules}
- else (warning ("No such type-checking rule\n" ^ Display.string_of_thm th); tcs);
+ else (warning ("No such type-checking rule\n" ^
+ Display.string_of_thm_without_context th); tcs);
(* generic data *)
@@ -60,7 +62,7 @@
fun print_tcset ctxt =
let val TC {rules, ...} = tcset_of ctxt in
Pretty.writeln (Pretty.big_list "type-checking rules:"
- (map (ProofContext.pretty_thm ctxt) rules))
+ (map (Display.pretty_thm ctxt) rules))
end;