--- a/Admin/isatest/settings/mac-poly-M4 Thu Jul 23 15:59:14 2009 +0200
+++ b/Admin/isatest/settings/mac-poly-M4 Thu Jul 23 16:53:15 2009 +0200
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-experimental"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="--mutable 600 --immutable 1800"
+ ML_OPTIONS="--mutable 800 --immutable 2000"
ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
--- a/Admin/isatest/settings/mac-poly-M8 Thu Jul 23 15:59:14 2009 +0200
+++ b/Admin/isatest/settings/mac-poly-M8 Thu Jul 23 16:53:15 2009 +0200
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-experimental"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="--mutable 600 --immutable 1800"
+ ML_OPTIONS="--mutable 800 --immutable 2000"
ISABELLE_HOME_USER=~/isabelle-mac-poly-M8
--- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 23 15:59:14 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 23 16:53:15 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_Goal.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
+ Display_Goal.pretty_goals ctxt Markup.none (true, false) (Thm.nprems_of st) st
|> Pretty.chunks
|> Pretty.string_of
--- a/src/Pure/Isar/proof.ML Thu Jul 23 15:59:14 2009 +0200
+++ b/src/Pure/Isar/proof.ML Thu Jul 23 16:53:15 2009 +0200
@@ -318,8 +318,6 @@
val show_main_goal = ref false;
val verbose = ProofContext.verbose;
-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 (Display.pretty_thm ctxt) ths), Pretty.str ""];
@@ -346,7 +344,7 @@
(if mode <> Backward orelse null using then NONE else SOME using) @
[Pretty.str ("goal" ^
description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
- pretty_goals_local ctxt Markup.subgoal
+ Display_Goal.pretty_goals ctxt Markup.subgoal
(true, ! show_main_goal) (! Display.goals_limit) goal @
(map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
| prt_goal NONE = [];
@@ -368,7 +366,7 @@
fun pretty_goals main state =
let val (ctxt, (_, goal)) = get_goal state
- in pretty_goals_local ctxt Markup.none (false, main) (! Display.goals_limit) goal end;
+ in Display_Goal.pretty_goals ctxt Markup.none (false, main) (! Display.goals_limit) goal end;
@@ -474,7 +472,8 @@
val ngoals = Thm.nprems_of goal;
val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
- (pretty_goals_local ctxt Markup.none (true, ! show_main_goal) (! Display.goals_limit) goal @
+ (Display_Goal.pretty_goals ctxt Markup.none
+ (true, ! show_main_goal) (! Display.goals_limit) goal @
[Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
val extra_hyps = Assumption.extra_hyps ctxt goal;
--- a/src/Pure/Isar/proof_display.ML Thu Jul 23 15:59:14 2009 +0200
+++ b/src/Pure/Isar/proof_display.ML Thu Jul 23 16:53:15 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_raw (Syntax.pp_global thy) flags [] th end;
+ in Display.pretty_thm_raw (Syntax.init_pretty_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;
--- a/src/Pure/Proof/reconstruct.ML Thu Jul 23 15:59:14 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML Thu Jul 23 16:53:15 2009 +0200
@@ -255,7 +255,7 @@
let
fun search env [] = error ("Unsolvable constraints:\n" ^
Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
- Display_Goal.pretty_flexpair (Syntax.pp_global thy) (pairself
+ Display_Goal.pretty_flexpair (Syntax.init_pretty_global thy) (pairself
(Envir.norm_term bigenv) p)) cs)))
| search env ((u, p as (t1, t2), vs)::ps) =
if u then
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Jul 23 15:59:14 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Jul 23 16:53:15 2009 +0200
@@ -655,11 +655,8 @@
text=[XML.Elem("pgml",[],
maps YXML.parse_body strings)] })
- 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)
-
- fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
+ fun strings_of_thm (thy, name) =
+ map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
val string_of_thy = Pretty.string_of o ProofDisplay.pretty_full_theory false
in
--- a/src/Pure/display.ML Thu Jul 23 15:59:14 2009 +0200
+++ b/src/Pure/display.ML Thu Jul 23 16:53:15 2009 +0200
@@ -16,8 +16,8 @@
signature DISPLAY =
sig
include BASIC_DISPLAY
- val pretty_thm_raw: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
- term list -> thm -> Pretty.T
+ val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool, show_status: bool} ->
+ thm -> Pretty.T
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
@@ -68,7 +68,7 @@
else ""
end;
-fun pretty_thm_raw pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
+fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps', show_status} raw_th =
let
val th = Thm.strip_shyps raw_th;
val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
@@ -76,8 +76,9 @@
val tags = Thm.get_tags th;
val q = if quote then Pretty.quote else I;
- val prt_term = q o Pretty.term pp;
+ val prt_term = q o Syntax.pretty_term ctxt;
+ val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
val status = display_status show_status th;
@@ -86,8 +87,8 @@
if hlen = 0 andalso status = "" then []
else if ! show_hyps orelse show_hyps' then
[Pretty.brk 2, Pretty.list "[" "]"
- (map (q o Display_Goal.pretty_flexpair pp) tpairs @ map prt_term hyps' @
- map (Pretty.sort pp) xshyps @
+ (map (q o Display_Goal.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
+ map (Syntax.pretty_sort ctxt) xshyps @
(if status = "" then [] else [Pretty.str status]))]
else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
val tsymbs =
@@ -95,18 +96,14 @@
else [Pretty.brk 1, pretty_tags tags];
in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
-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;
-
+fun pretty_thm_aux ctxt show_status =
+ pretty_thm_raw ctxt {quote = false, show_hyps = true, show_status = show_status};
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_global thy =
+ pretty_thm_raw (Syntax.init_pretty_global thy)
+ {quote = false, show_hyps = false, show_status = true};
fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
--- a/src/Pure/display_goal.ML Thu Jul 23 15:59:14 2009 +0200
+++ b/src/Pure/display_goal.ML Thu Jul 23 16:53:15 2009 +0200
@@ -9,10 +9,10 @@
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
+ val pretty_flexpair: Proof.context -> term * term -> Pretty.T
+ val pretty_goals: Proof.context -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
+ val pretty_goals_without_context: int -> thm -> Pretty.T list
+ val print_goals_without_context: int -> thm -> unit
end;
structure Display_Goal: DISPLAY_GOAL =
@@ -21,8 +21,8 @@
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];
+fun pretty_flexpair ctxt (t, u) = Pretty.block
+ [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
@@ -56,31 +56,35 @@
in
-fun pretty_goals_aux pp markup (msg, main) maxgoals state =
+fun pretty_goals ctxt markup (msg, main) maxgoals state =
let
+ val prt_sort = Syntax.pretty_sort ctxt;
+ val prt_typ = Syntax.pretty_typ ctxt;
+ val prt_term = Syntax.pretty_term ctxt;
+
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_var (x, ~1) = prt_term (Syntax.free x)
+ | prt_var xi = prt_term (Syntax.var xi);
- fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
- | prt_varT xi = Pretty.typ pp (TVar (xi, []));
+ fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
+ | prt_varT xi = prt_typ (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);
+ val prt_consts = prt_atoms (prt_term o Const) prt_typ;
+ val prt_vars = prt_atoms prt_var prt_typ;
+ val prt_varsT = prt_atoms prt_varT prt_sort;
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];
+ [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term 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_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
@@ -92,7 +96,7 @@
val ngoals = length As;
fun pretty_gs (types, sorts) =
- (if main then [Pretty.term pp B] else []) @
+ (if main then [prt_term B] else []) @
(if ngoals = 0 then [Pretty.str "No subgoals!"]
else if ngoals > maxgoals then
pretty_subgoals (Library.take (maxgoals, As)) @
@@ -110,10 +114,11 @@
(! 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;
+fun pretty_goals_without_context n th =
+ pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
-val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
+val print_goals_without_context =
+ (Pretty.writeln o Pretty.chunks) oo pretty_goals_without_context;
end;
--- a/src/Pure/goal.ML Thu Jul 23 15:59:14 2009 +0200
+++ b/src/Pure/goal.ML Thu Jul 23 16:53:15 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_Goal.pretty_goals n th)) ^
+ Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals_without_context n th)) ^
("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
--- a/src/Pure/old_goals.ML Thu Jul 23 15:59:14 2009 +0200
+++ b/src/Pure/old_goals.ML Thu Jul 23 16:53:15 2009 +0200
@@ -135,7 +135,8 @@
(*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_Goal.pretty_goals (!goals_limit) state @
+ Pretty.str "Bad final proof state:" ::
+ Display_Goal.pretty_goals_without_context (!goals_limit) state @
[Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
val result_error_fn = ref result_error_default;
@@ -277,7 +278,7 @@
(if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
(if ngoals <> 1 then "s" else "") ^ ")"
else ""))] @
- Display_Goal.pretty_goals m th
+ Display_Goal.pretty_goals_without_context m th
end |> Pretty.chunks |> Pretty.writeln;
(*Printing can raise exceptions, so the assignment occurs last.
--- a/src/Pure/tctical.ML Thu Jul 23 15:59:14 2009 +0200
+++ b/src/Pure/tctical.ML Thu Jul 23 16:53:15 2009 +0200
@@ -191,12 +191,11 @@
(*** Tracing tactics ***)
(*Print the current proof state and pass it on.*)
-fun print_tac msg =
- (fn st =>
- (tracing msg;
- tracing ((Pretty.string_of o Pretty.chunks o
- Display_Goal.pretty_goals (! Display_Goal.goals_limit)) st);
- Seq.single st));
+fun print_tac msg st =
+ (tracing (msg ^ "\n" ^
+ Pretty.string_of (Pretty.chunks
+ (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st)));
+ Seq.single st);
(*Pause until a line is typed -- if non-empty then fail. *)
fun pause_tac st =
@@ -232,10 +231,10 @@
(*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_Goal.print_goals (! Display_Goal.goals_limit) st;
- tracing "** Press RETURN to continue:";
- exec_trace_command flag (tac,st))
+ if !flag andalso not (!suppress_tracing) then
+ (Display_Goal.print_goals_without_context (! Display_Goal.goals_limit) st;
+ tracing "** Press RETURN to continue:";
+ exec_trace_command flag (tac, st))
else tac st;
(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
--- a/src/Pure/type_infer.ML Thu Jul 23 15:59:14 2009 +0200
+++ b/src/Pure/type_infer.ML Thu Jul 23 16:53:15 2009 +0200
@@ -40,7 +40,9 @@
fun param i (x, S) = TVar (("?" ^ x, i), S);
val paramify_vars =
- perhaps (Term_Subst.map_atypsT_option (fn TVar ((x, i), S) => SOME (param i (x, S)) | _ => NONE));
+ Same.commit
+ (Term_Subst.map_atypsT_same
+ (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME));
val paramify_dummies =
let
@@ -90,9 +92,10 @@
(* utils *)
-fun deref tye (T as Param (i, S)) = (case Inttab.lookup tye i of
- NONE => T
- | SOME U => deref tye U)
+fun deref tye (T as Param (i, S)) =
+ (case Inttab.lookup tye i of
+ NONE => T
+ | SOME U => deref tye U)
| deref tye T = T;
fun fold_pretyps f (PConst (_, T)) x = f T x
@@ -194,32 +197,35 @@
(* add_parms *)
-fun add_parmsT tye T = case deref tye T of
+fun add_parmsT tye T =
+ (case deref tye T of
PType (_, Ts) => fold (add_parmsT tye) Ts
| Param (i, _) => insert (op =) i
- | _ => I;
+ | _ => I);
fun add_parms tye = fold_pretyps (add_parmsT tye);
(* add_names *)
-fun add_namesT tye T = case deref tye T of
+fun add_namesT tye T =
+ (case deref tye T of
PType (_, Ts) => fold (add_namesT tye) Ts
| PTFree (x, _) => Name.declare x
| PTVar ((x, _), _) => Name.declare x
- | Param _ => I;
+ | Param _ => I);
fun add_names tye = fold_pretyps (add_namesT tye);
(* simple_typ/term_of *)
-fun simple_typ_of tye f T = case deref tye T of
+fun simple_typ_of tye f T =
+ (case deref tye T of
PType (a, Ts) => Type (a, map (simple_typ_of tye f) Ts)
| PTFree v => TFree v
| PTVar v => TVar v
- | Param (i, S) => TVar (f i, S);
+ | Param (i, S) => TVar (f i, S));
(*convert types, drop constraints*)
fun simple_term_of tye f (PConst (c, T)) = Const (c, simple_typ_of tye f T)
@@ -282,7 +288,8 @@
fun occurs_check tye i (Param (i', S)) =
if i = i' then raise NO_UNIFIER ("Occurs check!", tye)
- else (case Inttab.lookup tye i' of
+ else
+ (case Inttab.lookup tye i' of
NONE => ()
| SOME T => occurs_check tye i T)
| occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts
@@ -297,14 +304,15 @@
(* unification *)
- fun unif (T1, T2) (tye_idx as (tye, idx)) = case (deref tye T1, deref tye T2) of
+ fun unif (T1, T2) (tye_idx as (tye, idx)) =
+ (case (deref tye T1, deref tye T2) of
(Param (i, S), T) => assign i T S tye_idx
| (T, Param (i, S)) => assign i T S tye_idx
| (PType (a, Ts), PType (b, Us)) =>
if a <> b then
raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b, tye)
else fold unif (Ts ~~ Us) tye_idx
- | (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye);
+ | (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye));
in unif end;
@@ -396,7 +404,7 @@
let val (T, tye_idx') = inf bs t tye_idx in
(T,
unif (T, U) tye_idx'
- handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U)
+ handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U)
end;
in inf [] end;