# HG changeset patch # User wenzelm # Date 1248254589 -7200 # Node ID 7913823f14e3e33cd98b779950a568ab3e82696b # Parent 2a0645733185ac93145a2403dc5bce3a419538f4# Parent eff525e07a31a76c611154661d5f8588dbead58c merged, resolving trivial conflict; diff -r 2a0645733185 -r 7913823f14e3 Admin/isatest/isatest-makedist --- 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 diff -r 2a0645733185 -r 7913823f14e3 Admin/isatest/settings/mac-poly-M4 --- 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" diff -r 2a0645733185 -r 7913823f14e3 Admin/isatest/settings/mac-poly-M8 --- 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" diff -r 2a0645733185 -r 7913823f14e3 NEWS --- 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 *** diff -r 2a0645733185 -r 7913823f14e3 src/FOLP/classical.ML --- 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}; diff -r 2a0645733185 -r 7913823f14e3 src/FOLP/ex/Prolog.ML --- 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)); diff -r 2a0645733185 -r 7913823f14e3 src/FOLP/simp.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Import/import.ML --- 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) => diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Import/proof_kernel.ML --- 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)) = diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Import/shuffler.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Nominal/nominal_thmdecls.ML --- 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 ^").") diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/Function/lexicographic_order.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/TFL/casesplit.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/TFL/rules.ML --- 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 *) diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/TFL/tfl.ML --- 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 = diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/atp_minimal.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/atp_wrapper.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/choice_specification.ML --- 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) diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/inductive.ML --- 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); diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/inductive_codegen.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/inductive_realizer.ML --- 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"); diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/lin_arith.ML --- 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 *) diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/meson.ML --- 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)); diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/metis_tools.ML --- 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) diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/recdef.ML --- 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 *) diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/record.ML --- 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); diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/res_atp.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/res_axioms.ML --- 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) = diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/res_reconstruct.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/HOL/Tools/sat_funcs.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/HOL/ex/ROOT.ML --- 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: *) diff -r 2a0645733185 -r 7913823f14e3 src/HOL/ex/predicate_compile.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/Provers/Arith/fast_lin_arith.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Provers/blast.ML --- 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 ***) diff -r 2a0645733185 -r 7913823f14e3 src/Provers/classical.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Concurrent/future.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Concurrent/par_list.ML --- 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); diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Concurrent/task_queue.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/Pure/IsaMakefile --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Isar/args.ML --- 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) diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Isar/calculation.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Isar/code.ML --- 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)) diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Isar/context_rules.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Isar/element.ML --- 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 = [] diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Isar/isar_cmd.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Isar/local_defs.ML --- 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); diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Isar/method.ML --- 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 (); diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Isar/obtain.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Isar/proof.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Isar/proof_context.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Isar/proof_display.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Isar/runtime.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/ML-Systems/exn.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/ML-Systems/multithreading_polyml.ML --- 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 *) diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Proof/reconstruct.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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) diff -r 2a0645733185 -r 7913823f14e3 src/Pure/ROOT.ML --- 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"; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Thy/thy_info.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 diff -r 2a0645733185 -r 7913823f14e3 src/Pure/Tools/find_theorems.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/Pure/display.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/display_goal.ML --- /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; + diff -r 2a0645733185 -r 7913823f14e3 src/Pure/goal.ML --- 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])); diff -r 2a0645733185 -r 7913823f14e3 src/Pure/old_goals.ML --- 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. diff -r 2a0645733185 -r 7913823f14e3 src/Pure/proofterm.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/pure_thy.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/simplifier.ML --- 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]; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/tctical.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Pure/thm.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Sequents/prover.ML --- 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 diff -r 2a0645733185 -r 7913823f14e3 src/Sequents/simpdata.ML --- 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 = diff -r 2a0645733185 -r 7913823f14e3 src/Tools/Code/code_preproc.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Tools/Code/code_printer.ML --- 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 **) diff -r 2a0645733185 -r 7913823f14e3 src/Tools/Code/code_thingol.ML --- 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; diff -r 2a0645733185 -r 7913823f14e3 src/Tools/coherent.ML --- 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)) => diff -r 2a0645733185 -r 7913823f14e3 src/Tools/induct.ML --- 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 *) diff -r 2a0645733185 -r 7913823f14e3 src/ZF/Tools/inductive_package.ML --- 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.*) diff -r 2a0645733185 -r 7913823f14e3 src/ZF/Tools/typechk.ML --- 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;